6.4 Interfacing nondeterministic code with the real world

Normally, attempting to call a nondet or multi mode of a predicate from a predicate declared as semidet or det will cause a determinism error. So how can we call nondeterministic code from deterministic code? There are several alternative possibilities.

If you just want to see if a nondeterministic goal is satisfiable or not, without needing to know what variable bindings it produces, then there is no problem - determinism analysis considers nondet and multi goals with no non-local output variables to be semidet and det respectively.

If you want to use the values of output variables, then you need to ask yourself which one of possibly many solutions to a goal do you want? If you want all of them, you need to one of the predicates in the standard library module ‘solutions’, such as ‘solutions/2’ itself, which collects all of the solutions to a goal into a list — see Higher-order.

If you just want one solution from a predicate and don’t care which, you should declare the relevant mode of the predicate to have determinism cc_nondet or cc_multi (depending on whether you are guaranteed at least one solution or not). This tells the compiler that this mode of this predicate may have more than one solution when viewed as a statement in logic, but the implementation should stop after generating the first solution. In other words, the implementation should commit to the first solution.

The commit to the first solution means that a piece of cc_nondet or cc_multi code can never be asked to generate a second solution. If e.g. a cc_nondet call is in a conjunction, then no later goal in that conjunction (after mode reordering) may fail, because that would ask the committed choice goal for a second solution. The compiler enforces this rule.

In the declarative semantics, which solution will be the first is unpredictable, but in the operational semantics, you can predict which solution will be the first, since Mercury does depth-first search with left-to-right execution of clause bodies, though that is not on the source code form of each clause body, but on its form after mode analysis reordering to put the producer of each variable before all its consumers.

The ‘committed choice nondeterminism’ of a predicate has to be propagated up the call tree, making its callers, its callers’ callers, and so on, also cc_nondet or cc_multi, until either you get to main/2 at the top of the call tree, or you get to a location where you don’t have to propagate the committed choice context upward anymore.

While main/2 is usually declared to have determinism det, it may also be declared cc_multi. In the latter case, while the program’s declarative semantics may admit more than one solution, the implementation will stop after the first, so alternative solutions to main/2 (and hence also to cc_nondet or cc_multi predicates called directly or indirectly from ‘main/2’) are implicitly pruned away. This is similar to the “don’t care” nondeterminism of committed choice logic programming languages such as GHC.

One way to stop propagating committed choice nondeterminism is the one mentioned above: if a goal has no non-local output variables (i.e. none of the goal’s outputs are visible from outside the goal), then the goal’s solutions are indistinguishable from the outside, and the implementation will only attempt to satisfy the goal once, whether or not the goal is committed choice. Therefore if a cc_multi goal has all its outputs ignored, then the compiler considers it to be a det goal, while if a cc_nondet goal has all its outputs ignored, then the compiler considers it to be a semidet goal.

The other way to stop propagating committed choice nondeterminism is applicable when you know that all the solutions returned will be equivalent in all the ways that your program cares about. For example, you might want to find the maximum element in a set by iterating over the elements in the set. Iterating over the elements in a set in an unspecified order is a nondeterministic operation, but no matter which order you iterate over them, the maximum value in the set should be the same.

If this condition is satisfied, i.e. if you know that there will only ever be at most one distinct solution under your equality theory of the output variables, then you can use a ‘promise_equivalent_solutions’ determinism cast. If goal ‘G’ is a cc_multi goal whose outputs are X and Y, then promise_equivalent_solutions [X, Y] ( G ) promises the compiler that all solutions of G are equivalent, so that regardless of which solution of G the implementation happens to commit to, the rest of the program will compute either identical or (similarly) equivalent results. This allows the compiler to consider promise_equivalent_solutions [X, Y] ( G ) to have determinism det. Likewise, the compiler will consider promise_equivalent_solutions [X, Y] ( G ) where G is cc_nondet to have determinism semidet.

Note that specifying a user-defined equivalence relation as the equality predicate for user-defined types (see User-defined equality and comparison) means that ‘promise_equivalent_solutions’ can be used to express more general forms of equivalence. For example, if you define a set type which represents sets as unsorted lists, you would want to define a user-defined equivalence relation for that type, which could sort the lists before comparing them. The ‘promise_equivalent_solutions’ determinism cast could then be used for sets even though the lists used to represent the sets might not be in the same order in every solution.