Needs text improvement
Finally, if A and B can unify, goals are delayed that prevent A and B to become equal.
This doesn't really make sense to me. There is nothing that is "delayed" really, it's just that a background check is done if A and B are involved in a unification. That description really threw me off.
(With hindsight and after getting into the jargon one realizes that "goals are delayed" might well mean "a procedure will be run asynchronously" ... "to make sure that A and B do not become equal". But a reference manual should not be a grimoire.)
The text in
library(dif) is much clearer:
Among the most important coroutining predicates is dif/2, which expresses disequality of terms in a sound way. The actual test is delayed until the terms are sufficiently different, or have become identical.
I prefer to look at it this way:
dif(A,B) call, any unification involving A or B or subterms thereof
that would make A and B identical (
A == B) will fail (and this applies to unification in clause heads, too).
If A and B are already identical at call time,
dif(A,B) fails at once.
I made a writeup, including examples, here:
That has turned into a lot of text, hopefully clear.
Note the printing of the "residual goal"
?- dif(X,a),(X=1;Y=2). X = 1 ; % dif/2 constraint cleared Y = 2, % dif/2 constraint still live dif(X, a). % the residual goal