Committed choice nondeterminism

Reply to a question regarding semantics of committed choice nondeterminism on the mercury-users mailing list.

Date: Tue, 06 Nov 2018 09:10:15 +1100
From: Zoltan Somogyi <[email protected]>
Subject: Re: [m-users.] Performance of solutions module
Message-Id: <[email protected]>

---

There are two kinds of semantics that are relevant here. One is the declarative semantics: what a piece of code is supposed to mean. The other is the operational semantics: what the compiled version of that code actually does. Mercury is a declarative language because in almost all cases, the compiler is required to ensure that the operational semantics matches the declarative semantics.

Committed choice code is one of the main exceptions.

Consider a predicate that may have more than one solution in a given mode according to its declarative semantics. In the usual case of that mode of the predicate being declared to be nondet or multi, the compiler is required to generate code that returns every one of those solutions, one at a time. In this case, the declarative and operational semantics match.

If that mode of the predicate is instead declared cc_nondet or cc_multi, then the compiler will generate code that returns at most one solution. The fact that the rest of the solutions will not be returned is in this case a deliberate difference between the operational semantics and the usual declarative semantics.

The one solution that will be returned will be the one that is computed first. The declarative semantics works in terms of sets of solutions and has no notion of an order between solutions, but the operational semantics works in terms of resolution steps, and it does know about order. The order implemented by the Mercury compiler is the standard logic programming order, with earlier disjuncts being executed before later disjuncts.

There are several kinds of situations in which this difference (and therefore committed choice determinisms) are useful.

The first is when the piece of code whose determinism we are talking about may have more than one solution, but we do not care about the differences between solutions. For example, it is fairly common to have code that looks like this:

    ( if
        some [Item] (
            list.member(Item, Items),
            item_has_property_x(Item)
        )
    then
        ...
    else
        ...
    )

In this case, all solutions of the code inside the existential quantification are equivalent, since the code outside the quantification cannot access the solution; all that this code cares about is the existence or nonexistence of a solution.

A more subtle version of this is abstract data types with nonstandard equality theories. Consider a predicate that converts a list of ints to a binary search tree (BST) containing those ints. Given any nontrivial list of ints, there will be more than one BST containing those ints. The standard declarative semantics would require the conversion predicate to return every one of those forms one at a time. Mercury allows programmers to use user-defined equality and committed choice determinisms to tell the compiler that in the user's intended declarative semantics, all the BSTs whose in-order traversal yields the original list are equivalent, so having the conversion predicate returning just one such BST is fine. (I mention this only for completeness; most Mercury users won't use user defined equality.)

Another situation is when the job of the predicate is inherently operational. The benchmarking predicates in the benchmarking module of the Mercury standard library invoke the predicate being benchmarked and return not just its output, but also a number giving the time taken to execute that predicate. In the declarative semantics, the benchmarking predicate has infinite number of solutions, with each solution pairing the actual result of the predicate under test with all the possible times. Actually implementing that declarative semantics would therefore yield an infinite loop, and would also be totally useless: the user knows the set of possible execution times is infinite (it can be 0 milliseconds, 1 ms, 2 ms etc), and he/she calls the benchmarking predicate because he/she wants to know which is the actual execution time of this invocation. (Other invocations may take a different amount of time.) So the benchmarking predicate is cc_multi; it returns exactly one of the possible times, the one that this invocation took. Mercury's rules about what sorts of contexts may contain committed choice code are intended to prevent such inherently operational choices affecting the computation of solutions for non-committed-choice predicates.