5

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.
MWB
  • 11,740
  • 6
  • 46
  • 91
  • 2
    [Here](https://github.com/mthom/scryer-prolog/issues/135#issuecomment-488348886) is a sketch of an implementation that would. – false Sep 29 '20 at 21:27
  • Shouldn't this be considered a bug in SWI? – MWB Dec 20 '20 at 15:51
  • My point is that `(=)/2` is equivalent to `unify_with_occurs_check/2` when OC is `true`. – MWB Dec 27 '20 at 12:49

2 Answers2

2

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.
false
  • 10,264
  • 13
  • 101
  • 209
  • 1
    Good. In addition to that, a dedicated `dif_with_occurs_check/2` would be nice, too - parallels `unify_with_occurs_check/2` nicely... – repeat Mar 11 '21 at 09:10
  • 1
    @repeat: And unify_without_occurs_check/2 as well? Would be the best for subsumes_term/2 – false Mar 11 '21 at 09:14
  • OK, but there may be systems that cannot implement `unify_without_occurs_check/2` without looping. And `subsumes_term/2` might be implemented differently internally. – repeat Mar 11 '21 at 12:06
  • @repeat: Systems with a looping algorithm would have to implement it differently. But yes, it might only work for systems with rational trees. BTW, did you understand what exactly is happening in Tau, when the occurs check is turned off? – false Mar 11 '21 at 14:07
1

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