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

推荐答案

这是另一个更简单的解决方法:

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.

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