Next: Replacing compile-time checking with run-time checking, Previous: Determinism categories, Up: Determinism
The determinism of goals is inferred from the determinism of their component parts, according to the rules below. The inferred determinism of a procedure is just the inferred determinism of the procedure's body.
For procedures that are local to a module,
the determinism annotations may be omitted;
in that case, their determinism will be inferred.
(To be precise, the determinism of procedures without a determinism annotation
is defined as the least fixpoint of the transformation which,
given an initial assignment
of the determinism
det to all such procedures,
applies those rules to infer
a new determinism assignment for those procedures.)
It is an error to omit the determinism annotation for procedures that are exported from their containing module.
If a determinism annotation is supplied for a procedure, the declared determinism is compared against the inferred determinism. If the declared determinism is greater than or not comparable to the inferred determinism (in the partial ordering above), it is an error. If the declared determinism is less than the inferred determinism, it is not an error, but the implementation may issue a warning.
The determinism category of each goal is inferred according to the following rules. These rules work with the two components of determinism category: whether the goal can fail without producing a solution, and the maximum number of solutions of the goal (0, 1, or more). If the inference process below reports that a goal can succeed more than once, but the goal generates no outputs that are visible from outside the goal, and the goal is not impure (see Impurity), then the final determinism of the goal will be based on the goal succeeding at most once, since the compiler will implicitly prune away any duplicate solutions.
failure, depending on its mode.
A unification that assigns the value of one variable to another is deterministic. A unification that constructs a structure and assigns it to a variable is also deterministic. A unification that tests whether a variable has a given top function symbol is semideterministic, unless the compiler knows the top function symbol of that variable, in which case its determinism is either det or failure depending on whether the two function symbols are the same or not. A unification that tests two variables for equality is semideterministic, unless the compiler knows that the two variables are aliases for one another, in which case the unification is deterministic, or unless the compiler knows that the two variables have different function symbols in the same position, in which case the unification has a determinism of failure.
The compiler knows the top function symbol of a variable
if the previous part of the procedure definition
contains a unification of the variable with a function symbol,
or if the variable's type has only one function symbol.
det. The conjunction ‘(A, B)’ can fail if either A can fail, or if A can succeed at least once, and B can fail. The conjunction can succeed at most zero times if either A or B can succeed at most zero times. The conjunction can succeed more than once if either A or B can succeed more than once and both A and B can succeed at least once. (If e.g. A can succeed at most zero times, then even if B can succeed many times the maximum number of solutions of the conjunction is still zero.) Otherwise, i.e. if both A and B succeed at most once, the conjunction can succeed at most once.
( L = , empty(Out) ; L = [H|T], nonempty(H, T, Out) )
If L is input to the disjunction, then the disjunction is a switch on L.
If two variables are unified with each other, then whatever function symbol one variable is unified with, the other variable is considered to be unified with the same function symbol. In the following example, since K is unified with L, the second disjunct unifies L as well as K with cons, and thus the disjunction is recognized as a switch.
( L = , empty(Out) ; K = L, K = [H|T], nonempty(H, T, Out) )
A switch can fail if the various arms of the switch do not cover all the function symbols in the type of the switched-on variable, or if the code in some arms of the switch can fail, bearing in mind that in each arm of the switch, the unification that tests the switched-on variable against the function symbol of that arm is considered to be deterministic. A switch can succeed several times if some arms of the switch can succeed several times, possibly because there are multiple disjuncts that test the switched-on variable against the same function symbol. A switch can succeed at most zero times only if all arms of the switch can succeed at most zero times.
Only unifications may occur before the test of the switched-on variable in each disjunct. Tests of the switched-on variable may occur within existential quantification goals.
The following example is a switch.
( Out = 1, L =  ; some [H, T] ( L = [H|T], nonempty(H, T, Out) ) )
The following example is not a switch because the call in the first disjunct occurs before the test of the switched-on variable.
( empty(Out), L =  ; L = [H|T], nonempty(H, T, Out) )
The unification of the switched-on variable with a function symbol may occur inside a nested disjunction in a given disjunct, provided that unification is preceded only by other unifications, both inside the nested disjunction and before the nested disjunction. The following example is a switch on X, provided X is bound beforehand.
( X = f p(Out) ; Y = X, ( Y = g, Intermediate = 42 ; Z = Y, Z = h(Arg), q(Arg, Intermediate) ), r(Intermediate, Out) )
failure. A disjunction ‘(A ; B)’ that is not a switch can fail if both A and B can fail. It can succeed at most zero times if both A and B can succeed at most zero times. It can succeed at most once if one of A and B can succeed at most once and the other can succeed at most zero times. Otherwise, i.e. if either A or B can succeed more than once, or if both A and B can succeed at least once, it can succeed more than once.
erroneous, then the determinism of the negation is
erroneous. If the determinism of the negated goal is
failure, the determinism of the negation is
det. If the determinism of the negated goal is
multi, the determinism of the negation is
failure. Otherwise, the determinism of the negation is