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)
If no possible calls to a particular mode of a predicate or
function can return to the caller, then that mode has a
The determinism annotation
erroneous is used on the library
predicates ‘require.error/1’ and ‘exception.throw/1’,
but apart from that determinism annotations
failure are generally not needed.
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).
:- 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.