SWI-Prolog 中正确的 unify_with_occurs_check/2 ? [英] Proper unify_with_occurs_check/2 in SWI-Prolog?

问题描述

有这种奇怪的行为.我正在运行这些测试用例:

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).

现在我得到了这些结果，其中 s2 的结果是错误的.结果在两个方面是错误的，第一个 _3434 被触发，第二个 unify_with_occurs_check 成功:

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.

_3434 不应该被触发遵循 ISO 核心标准中的 7.3.2 Herband 算法.根据条款 7.3.2 f) 1) 变量 X 到项 t 的实例化仅在 X 不在 t 中出现时传播.

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.

统一应该失败遵循条款 7.3.2 g).因此，在 SWI-Prolog 中，诸如 freeze/2、dif/2 等各种化身中的属性变量似乎会干扰 unify_with_occurs_check.

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.

有什么解决方法吗?

编辑 06.02.2021:
bug 已在 SWI-Prolog 8.3.17 (devel) 和
也向后移植到 SWI-Prolog 8.2.4(稳定版).

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.

推荐答案

一种解决方法可能是推出自己的 unify_with_occurs_check/2.对于没有 unify_with_occurs_check/2 的 Prolog 系统，我们可以像过去那样在 Prolog 本身中编写它:

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，1984 年 9 月 15 日
http://www.picat-lang.org/bprolog/publib/metutl.html

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

这是使用 (=..)/2 和 term_variables/2 的替代方法:

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.

这篇关于SWI-Prolog 中正确的 unify_with_occurs_check/2 ?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！