Did you know ... Search Documentation:
Predicate dif/2
Availability::- use_module(library(dif)).(can be autoloaded)
Sourcedif(@A, @B)
The dif/2 predicate is a constraint that is true if and only if A and B are different terms. If A and B can never unify, dif/2 succeeds deterministically. If A and B are identical, it fails immediately. Finally, if A and B can unify, goals are delayed that prevent A and B to become equal. It is this last property that makes dif/2 a more general and more declarative alternative for \=/2 and related predicates.

This predicate behaves as if defined by dif(X, Y) :- when(?=(X,Y), X \== Y). See also ?=/2. The implementation can deal with cyclic terms.

The dif/2 predicate is realised using attributed variables associated with the module dif. It is an autoloaded predicate that is defined in the library library(dif).

Tags are associated to your profile if you are logged in|Report abuse
Tags:
  • doc-needs-help
LogicalCaptain said (2020-06-09T16:43:03):0 upvotes 0 0 downvotes
Picture of user LogicalCaptain.

Needs text improvement

We read:

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:

After a 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.

Writeup on dif

I made a writeup, including examples, here:

About dif/2.

That has turned into a lot of text, hopefully clear.

Note the printing of the "residual goal"

dif/2 prints the "delayed goal" if it is still "live" at query success (the technical for this is "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