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.
In my system, I made a new predicate
dif_with_occurs_check/2
. As the name says, it isdif/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:This is necessary, so that we can wake up
dif_with_occurs_check/2
when change the variableY
for example toY = X
.dif_with_occurs_check/2
will then remove its own constraintX = f(Y)
which has becomeX = f(X)
and therefore obsolete.Open Source: Module "herbrand"
https://github.com/jburse/jekejeke-devel/blob/master/jekmin/headless/jekmin/reference/term/herbrand.p