|Did you know ...||Search Documentation:|
Think of zcompare/3 as reifying an arithmetic comparison of two
integers. This means that we can explicitly reason about the
different cases within our programs. As in compare/3, the atoms
= denote the different cases of the
trichotomy. In contrast to compare/3 though, zcompare/3 works
correctly for all modes, also if only a subset of the arguments is
instantiated. This allows you to make several predicates over
integers deterministic while preserving their generality and
completeness. For example:
n_factorial(N, F) :- zcompare(C, N, 0), n_factorial_(C, N, F). n_factorial_(=, _, 1). n_factorial_(>, N, F) :- F #= F0*N, N1 #= N - 1, n_factorial(N1, F0).
This version of n_factorial/2 is deterministic if the first argument is instantiated, because argument indexing can distinguish the different clauses that reflect the possible and admissible outcomes of a comparison of N against 0. Example:
?- n_factorial(30, F). F = 265252859812191058636308480000000.
Since there is no clause for
<, the predicate automatically
fails if N is less than 0. The predicate can still be used in
all directions, including the most general query:
?- n_factorial(N, F). N = 0, F = 1 ; N = F, F = 1 ; N = F, F = 2 .
In this case, all clauses are tried on backtracking, and zcompare/3 ensures that the respective ordering between N and 0 holds in each case.
The truth value of a comparison can also be reified with (#<==>)/2 in combination with one of the arithmetic constraints. See reification. However, zcompare/3 lets you more conveniently distinguish the cases.