prolog - Prolog中的平等和统一我错过了什么？

Question

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

适用于 x86_64-linux 的 SWI-Prolog 版本 7.2.3

无论如何，我在练习 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).

（再次，考虑到必要的额外事实）我得到

谁=爱德华；

谁=爱丽丝；

错误的

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

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

谁能解释为什么会这样，以及为什么我的 diff 实现不能按我预期的方式工作，在我要求从该查询中进行额外统一的情况下？

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

任何帮助深表感谢。

标签： prologprolog-dif

Answer 1

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

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