Next: , Previous: , Up: Top   [Contents]


7 Determinism

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

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 (and hence deterministic) if they are distinguished by the unification of a variable (possibly renamed) with distinct functors in the different clauses (or disjuncts), so long as the unifications take place before the first call in the clause (or disjunct). In these cases, the Mercury compiler generates a switch (see the earlier section on indexing). If a switch has a branch for every functor on the type of the switching variable, then the switch cannot fail (though one or more of its arms may do so).

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 “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 the call to ‘>/2’ can fail.

The general solution to such problems is to use an if-then-else:

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

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

Next: , Previous: , Up: Top   [Contents]