6.1 Determinism categories

For each mode of a predicate or function, we categorise that mode according to how many times it can succeed, and whether or not it can fail before producing its first solution.

If all possible calls to a particular mode of a predicate or function which return to the caller (calls which terminate, do not throw an exception and do not cause a fatal runtime error)

• have exactly one solution, then that mode is deterministic (det);
• either have no solutions or have one solution, then that mode is semideterministic (semidet);
• have at least one solution but may have more, then that mode is multisolution (multi);
• have zero or more solutions, then that mode is nondeterministic (nondet);
• fail without producing a solution, then that mode has a determinism of failure.

If no possible calls to a particular mode of a predicate or function can return to the caller, then that mode has a determinism of erroneous.

The determinism annotation erroneous is used on the library predicates ‘require.error/1’ and ‘exception.throw/1’, but apart from that, determinism annotations erroneous and failure are generally not needed.

To summarize:

                Maximum number of solutions
Can fail?       0               1               > 1
no              erroneous       det             multi
yes             failure         semidet         nondet

(Note: the “Can fail?” column here indicates only whether the procedure can fail before producing at least one solution; attempts to find a second solution to a particular call, e.g. for a procedure with determinism multi, are always allowed to fail.)

The determinism of each mode of a predicate or function is indicated by an annotation on the mode declaration. For example:

:- pred append(list(T), list(T), list(T)).
:- mode append(in, in, out) is det.
:- mode append(out, out, in) is multi.
:- mode append(in, in, in) is semidet.

:- func length(list(T)) = int.
:- mode length(in) = out is det.
:- mode length(in(list_skel)) = out is det.
:- mode length(in) = in is semidet.

An annotation of det or multi is an assertion that for every value each of the inputs, there exists at least one value of the outputs for which the predicate is true, or (in the case of functions) for which the function term is equal to the result term. Conversely, an annotation of det or semidet is an assertion that for every value each of the inputs, there exists at most one value of the outputs for which the predicate is true, or (in the case of functions) for which the function term is equal to the result term. These assertions are called the mode-determinism assertions; they can play a role in the semantics, because in certain circumstances, they may allow an implementation to perform optimizations that would not otherwise be allowed, such as optimizing away a goal with no outputs even though it might infinitely loop.

If the mode of the predicate is given in the :- pred declaration rather than in a separate :- mode declaration, then the determinism annotation goes on the :- pred declaration (and similarly for functions). In particular, this is necessary if a predicate does not have any argument variables. If the determinism declaration is given on a :- func declaration without the mode, the function is assumed to have the default mode (see Modes for more information on default modes of functions).

For example:

:- pred loop(int::in) is erroneous.
loop(X) :- loop(X).

:- pred p is det.
p.

:- pred q is failure.
q :- fail.

If there is no mode declaration for a function, then the default mode for that function is considered to have been declared as det. If you want to write a partial function, i.e. one whose determinism is semidet, then you must explicitly declare the mode and determinism.

In Mercury, a function is supposed to be a true mathematical function of its arguments; that is, the value of the function’s result should be determined only by the values of its arguments. Hence, for any mode of a function that specifies that all the arguments are fully input (i.e. for which the initial inst of all the arguments is a ground inst), the determinism of that mode can only be det, semidet, erroneous, or failure.

The determinism categories form this lattice:

             erroneous
              /     \
          failure   det
             \     /   \
             semidet  multi
                 \     /
                  nondet

The higher up this lattice a determinism category is, the more the compiler knows about the number of solutions of procedures of that determinism.