prolog - SWI-Prolog 中正确的 unify_with_occurs_check/2？

Question

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

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 成功:

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 中时传播。

根据第 7.3.2 g) 条，统一应该失败。因此，在 SWI-Prolog 中，各种形式的属性变量(如 freeze/2、dif/2 等)似乎会干扰 unify_with_occurs_check。

任何解决方法？

编辑 06.02.2021:
bug已在 SWI-Prolog 8.3.17 (devel) 和
中修复也被反向移植到 SWI-Prolog 8.2.4(稳定版)。

Answer 1

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

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

当然，如果两个参数从一开始就是有限的，这只会按预期工作，但至少在这种情况下它不会循环。