Proper unify_with_occurs_check/2 in SWI-Prolog?

Admin 1
Viewed 247

Got this strange behaviour. I was running these test cases:

s1 :-
   Q=[[lambda,symbol(_3026),[cons,[quote,_3434],
     [quote,_3514]]],[quote,_3206]],
   P=[_3434|_3514],
   freeze(_3434, (write(foo), nl)),
   unify_with_occurs_check(P, Q).

s2 :-
   Q=[[lambda,symbol(_3026),[cons,[quote,_3434],
     [quote,_3514]]],[quote,_3206]],
   P=[_3434|_3514],
   freeze(_3434, (write(foo), nl)),
   freeze(_3514, (write(bar), nl)),
   unify_with_occurs_check(P, Q).

Now I get these results, where the outcome of s2 is wrong. The outcome is wrong in two respects, first _3434 gets triggered and second unify_with_occurs_check succeeds:

SWI-Prolog (threaded, 64 bits, version 8.3.16)

?- s1.
false.

?- s2.
foo
bar
true.

That _3434 shouldn't get triggered follows from 7.3.2 Herband Algorithm in ISO core standard. According to clause 7.3.2 f) 1) an instantiation of variable X to a term t is only propagated when it X does not occur in t.

That the unification should fail follows from clause 7.3.2 g). So it seems in SWI-Prolog, attributed variables in various incarnations such as freeze/2, dif/2, etc… seem to interfer with unify_with_occurs_check.

Any workaround?

Edit 06.02.2021:
The bug has been fixed in SWI-Prolog 8.3.17 (devel) and
was backported to SWI-Prolog 8.2.4 (stable) as well.

occurs-check logical-purity swi-prolog prolog
2 Answers

Here is another somewhat simpler workaround:

unify(X,X) :-
   acyclic_term(X).

Certainly, this only works as expected if the two arguments are finite from the very start, but at least it does not loop in this case.

user_7728680

One way out could be to roll your own unify_with_occurs_check/2. We can write it in Prolog itself, as was done in the past, for Prolog systems that did not have unify_with_occurs_check/2:

R.A.O'Keefe, 15 September 1984
http://www.picat-lang.org/bprolog/publib/metutl.html

Here is an alternative take that uses (=..)/2 and term_variables/2:

unify(X, Y) :- var(X), var(Y), !, X = Y.
unify(X, Y) :- var(X), !, notin(X, Y), X = Y.
unify(X, Y) :- var(Y), !, notin(Y, X), X = Y.
unify(X, Y) :- functor(X, F, A), functor(Y, G, B),
   F/A = G/B,
   X =.. [_|L],
   Y =.. [_|R],
   maplist(unify, L, R).

notin(X, Y) :-
   term_variables(Y, L),
   maplist(\==(X), L).

I now get the expected result:

?- s1.
false.

?- s2.
false.
Admin1
Related