SWI-Prolog 中正确的 unify_with_occurs_check/2 ？

如何解决SWI-Prolog 中正确的 unify_with_occurs_check/2 ？

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

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

s2 :-
   Q=[[lambda,freeze(_3514,(write(bar),Q).

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

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

?- s1.
false.

?- s2.
foo
bar
true.

根据 ISO 核心标准中的 7.3.2 Herband 算法，不应触发 _3434。根据条款 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（稳定版）。

解决方法

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

R.A.O'Keefe，1984 年 9 月 15 日
http://www.picat-lang.org/bprolog/publib/metutl.html

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

unify(X,Y) :- var(X),var(Y),!,X = Y.
unify(X,notin(X,Y),Y) :- var(Y),notin(Y,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).

我现在得到了预期的结果：

?- s1.
false.

?- s2.
false.

,

这是另一种更简单的解决方法：

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

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