prolog - 关于 Prolog 中的平等和统一，我缺少什么？

Question

我正在通过 Clocksin 和 Mellish 努力尝试并最终超越仅仅涉足 Prolog。 FWIW，我正在运行 SWI-Prolog:

SWI-Prolog version 7.2.3 for x86_64-linux

无论如何，我在练习 1.4 中实现了一个 diff/2 谓词。谓词非常简单:

diff(X,Y) :- X \== Y.

它在 sister_of 谓词中使用时有效，如下所示:

sister_of(X,Y) :- 
    female(X),
    diff(X,Y),
    parents(X, Mum, Dad ),
    parents(Y, Mum, Dad ).

在那里，假设必要的额外事实，这样做:

?- sister_of(alice,alice).

按预期返回 false。但这就是问题所在。如果我改为这样做:

?- sister_of(alice, Who).

(同样，考虑到必要的额外事实)我明白了

Who = edward ;

Who = alice;

false

尽管如前所述，谓词 sister_of 并未将 alice 视为自己的姐妹。

另一方面，如果我使用 SWI 提供的 dif/2 谓词，那么一切都会按照我天真地期望的方式进行。

谁能解释为什么会这样，以及为什么我的 diff 实现没有按照我期望的方式工作，如果我从该查询中请求额外的统一？

可以找到我正在使用的整个源文件here

非常感谢任何帮助。

Answer 1

如您所见，问题源于平等(或更确切地说，不平等)与统一之间的相互作用。观察在 sister_of 的定义中，您首先找到 X 的候选值，然后尝试约束 Y有所不同，但是 Y 仍然是一个未实例化的逻辑变量，并且检查总是会成功，就像 diff(alice, Y) 一样。以下约束(包括最后一个为 Y 赋予具体值的约束)来得太晚了。

一般来说，您需要做的是确保在您到达不等式时检查所有变量都已实例化。否定是 Prolog 的非逻辑特征，因此具有潜在危险，但检查两个基本项是否不相等是安全的。