问题描述
有这种奇怪的行为.我正在运行这些测试用例:
Got this strange behaviour. I was running these test cases:
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
成功:
Now I get these results, where the outcome of s2
is wrong. The outcome is wrong in two respects, first _3434
gets triggered and second unify_with_occurs_check
succeeds:
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 中出现时传播.
That _3434
shouldn't get triggered follows from 7.3.2 Herband Algorithm in ISO core standard. According to clause 7.3.2 f) 1) an instantiation of variable X to a term t is only propagated when it X does not occur in t.
统一应该失败遵循条款 7.3.2 g).因此,在 SWI-Prolog 中,诸如 freeze/2、dif/2 等各种化身中的属性变量似乎会干扰 unify_with_occurs_check.
That the unification should fail follows from clause 7.3.2 g). So it seems in SWI-Prolog, attributed variables in various incarnations such as freeze/2, dif/2, etc… seem to interfer with unify_with_occurs_check.
有什么解决方法吗?
编辑 06.02.2021:
bug 已在 SWI-Prolog 8.3.17 (devel) 和
也向后移植到 SWI-Prolog 8.2.4(稳定版).
Edit 06.02.2021:
The bug has been fixed in SWI-Prolog 8.3.17 (devel) and
was backported to SWI-Prolog 8.2.4 (stable) as well.
推荐答案
一种解决方法可能是推出自己的 unify_with_occurs_check/2.对于没有 unify_with_occurs_check/2 的 Prolog 系统,我们可以像过去那样在 Prolog 本身中编写它:
One way out could be to roll your own unify_with_occurs_check/2. We can write it in Prolog itself, as was done in the past, for Prolog systems that did not have unify_with_occurs_check/2:
R.A.O'Keefe,1984 年 9 月 15 日
http://www.picat-lang.org/bprolog/publib/metutl.html
这是使用 (=..)/2 和 term_variables/2 的替代方法:
Here is an alternative take that uses (=..)/2 and 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).
我现在得到了预期的结果:
I now get the expected result:
?- s1.
false.
?- s2.
false.
这篇关于SWI-Prolog 中正确的 unify_with_occurs_check/2 ?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持!