dif with occurs check

159 views Asked by At

Is there a dif with occurs check? This here works:

Welcome to SWI-Prolog (threaded, 64 bits, version 8.3.7)

?- set_prolog_flag(occurs_check, true). 
true.

?- dif(X,f(Y)), X = Y.
X = Y.

But the above is not feasible, since occurs check is a global flag, I get the following:

SWI-Prolog console for thread 3

?- X=f(X).
false.
2

There are 2 answers

0
AudioBubble On

In my system, I made a new predicate dif_with_occurs_check/2. As the name says, it is dif/2 with occurs check, so no need to set a flag. But there is an additional benefit, dif/2 is optimized to listen to fewer variables:

/* listens only to changes in X */
?- dif(X, f(Y)).
/* listens to changes in X and Y */
?- dif_with_occurs_check(X, f(Y)).

This is necessary, so that we can wake up dif_with_occurs_check/2 when change the variable Y for example to Y = X. dif_with_occurs_check/2 will then remove its own constraint X = f(Y) which has become X = f(X) and therefore obsolete.

?- dif(X,f(Y)), X = Y.
X = Y,
dif(Y, f(Y))
?- dif_with_occurs_check(X,f(Y)), X = Y.
X = Y

Open Source: Module "herbrand"
https://github.com/jburse/jekejeke-devel/blob/master/jekmin/headless/jekmin/reference/term/herbrand.p

4
false On

Now, Scryer supports dif/2 with occurs-check when the corresponding flag is set:

?- use_module(library(dif)).
   true.
?- set_prolog_flag(occurs_check, true).
   true.
?- dif(-X,X).
   true.
?- dif(-X,Y).
   dif:dif(- X,Y).
?- dif(-X,X), X = a.
   X = a.