dif/2¶

dif( X, Y)*

Succeed if the two arguments do not unify. A call to dif//22 will suspend if unification may still succeed or fail, anxd will fail if they always unify.

Dif is tricky because we need to wake up on the two variables being bound together, or on any variable of the term being bound to another. Also, the day YAP fully supports infinite rational trees, dif should work for them too. Hence, term comparison should not be implemented in Prolog.

This is the way dif works. The '$constraining_variables' predicate does not know anything about dif semantics, it just compares two terms for equaility and is based on compare. If it succeeds without generating a list of variables, the terms are equal and dif fails. If it fails, dif succeeds.

If it succeeds but it creates a list of variables, dif creates suspension records for all these variables on the '$redo_dif'(X, Y, V) goal. V is a flag that says whether dif has completed or not, X and Y are the original goals. Whenever one of these variables is bound, it calls '$redo_dif' again. '$redo_dif' will then check whether V was bound. If it was, dif has succeeded and redo_dif just exits. Otherwise, '$redo_dif' will call dif again to see what happened.

Dif needs two extensions from the suspension engine:

First, it needs for the engine to be careful when binding two suspended j variables. Basically, in this case the engine must be sure to wake up one of the goals, as they may make dif fail. The way the engine does so is by searching the list of suspended variables, and search whether they share a common suspended goal. If they do, that suspended goal is added to the WokenList.

Second, thanks to dif we may try to suspend on the same variable several times. dif calls a special version of freeze that checks whether that is in fact the case.