8 Determinism

The Mercury language requires the determinism of all predicates exported by a module to be declared. The determinism of predicates that are local to a module may be declared but don’t have to be; if they are not declared, they will be inferred. By default, the compiler issues a warning message where such declarations are omitted, but if you want to use determinism inference, you can disable this warning using the ‘--no-warn-missing-det-decls’ option.

Determinism checking and inference is an undecidable problem in the general case, so it is possible to write programs that are deterministic, and have the compiler fail to prove the fact. The most important aspect of this problem is that the Mercury compiler only detects the clauses of a predicate (or the arms of a disjunction, in the general case) to be mutually exclusive, allowing the execution of at most one disjunct at runtime, if the clauses or disjuncts each unify the same variable (or a copy of that variable) with distinct functors, with these unifications all taking place before the first call in the clause or disjunct. For such disjunctions, the Mercury compiler generates a switch (see the earlier section on indexing). If a switch has a branch for every functor in the type of the switched-on variable, then the switch guarantees that exactly one of its arms will be executed. If all the arms are deterministic goals, then the switch itself is deterministic.

The Mercury compiler does not do any range checking of integers, so code such as:

factorial(0, 1).
factorial(N, F) :-
    N > 0,
    N1 is N - 1,
    factorial(N1, F1),
    F is F1 * N.

would be inferred to be “nondeterministic”. The compiler would infer that the two clauses are not mutually exclusive, because it does not know about the semantics of >/2, and it would infer that the predicate as a whole could fail because (a) the unification of the first argument with 0 can fail, so the first clause is not guaranteed to generate a solution, and (b) the call to >/2 can fail, and so the second clause is not guaranteed to generate a solution either.

The general solution to such problems is to use a chain of one or more if-then-elses.

:- pred factorial(int::in, int::out) is det.

factorial(N, F) :-
    ( N < 0 ->
        unexpected($pred, "negative N")
    ; N = 0 ->
        F = 1
    ;
        N1 is N - 1,
        factorial(N1, F1),
        F is F1 * N
    ).

The unexpected predicate is defined in the require module of the Mercury standard library. Calls to it throw an exception, and unless that exception is caught, it aborts the program. The terms $pred is automatically replaced by the compiler with the (module-qualified) name of the predicate in which it appears.