SWI-Prolog 中的正确 unify_with_occurs_check/2 ？答案

【问题标题】：Proper unify_with_occurs_check/2 in SWI-Prolog?SWI-Prolog 中的正确 unify_with_occurs_check/2 ？
【发布时间】：2021-01-01 19:21:15
【问题描述】：

得到了这个奇怪的行为。我正在运行这些测试用例：

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（开发）和
中修复也被向后移植到 SWI-Prolog 8.2.4（稳定版）。

【问题讨论】：

如何减少示例的大小并提高其可读性？
在 Scryer 和 SICStus 中工作。
跟可怜的dif/2无关：freeze(A,true),freeze(B,true),unify_with_occurs_check(A-B,s(A,B)-n).
@false 那么这是一个错误吗？
@MaxB：确实，这是一个错误。最简单的论点（不涉及任何细节）是：获取上述查询并将其与相同的查询进行比较，但没有冻结目标之一。删除目标不应使查询失败，但确实如此。

标签： prolog swi-prolog logical-purity occurs-check

【解决方案1】：

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

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

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

【讨论】：

问题中没有说明这一特殊要求。
此解决方案将违反 ISO 核心标准的 7.3.2 f) 1)。

【解决方案2】：

一种出路可能是推出自己的 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, 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).

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

?- s1.
false.

?- s2.
false.

【讨论】：