3

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

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：
该错误已在 SWI-Prolog 8.3.17 (devel) 中修复，并且
也向后移植到 SWI-Prolog 8.2.4 (stable)。

4

2 回答 2

3

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

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

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

于 2021-01-01T21:08:04.163 回答
2

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

RAO'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.
于 2021-01-01T19:50:09.623 回答