问题描述
有这种奇怪的行为。我正在运行这些测试用例:
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).
当然,这只有在两个参数从一开始就是有限的情况下才能按预期工作,但至少在这种情况下它不会循环。