Next: Committed choice nondeterminism, Previous: Replacing compile-time checking with run-time checking, Up: Determinism
Normally, attempting to call
multi mode of a predicate
from a predicate declared as
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
with no non-local output variables to be
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 use the predicate ‘solutions/2’ in the standard library module ‘solutions’, which collects all of the solutions to a goal into a list — see Higher-order.
If you just want one solution and don't care which,
the calling predicate should be declared
The nondeterminism should then be propagated up the call tree
to the point at which it can be pruned.
In Mercury, pruning can be achieved in several ways.
The first way is the one mentioned above: if a goal has no non-local output variables then the implementation will only attempt to satisfy the goal once. Any potential duplicate solutions will be implicitly pruned away.
The second way is to rely on the fact that
the implementation will only seek a single solution to ‘main/2’,
so alternative solutions to ‘main/2’
(and hence also to
called directly or indirectly from ‘main/2’)
are implicitly pruned away.
This is one way to achieve “don't care” style nondeterminism in Mercury.
The other situation in which you may want pruning and committed choice style nondeterminism is when you know that all the solutions returned will be equivalent. 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 remove them, the maximum value in the set should be the same.
If you know that there will only ever be at most one distinct solution under the equality theory of the output variables, then you can use a ‘promise_equivalent_solutions’ determinism cast.
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.