prolog - 为什么这个表达不统一

Question

我定义了以下知识库：

leaf(_).
tree(X) :- leaf(X).

并期待查询：

leaf(X) = tree(X).

返回true .，因为每个定义的任何叶子都应该是一棵树。

不幸的是，激活跟踪不会产生任何有用的结果。如果您想使用它，这里是这个最小示例的链接。

标签： prologunification

Answer 1

简短的回答：你在这里检查这个词是否leaf(X)可以统一tree(X)。由于这些是由不同函子组成的术语，因此这将失败。

您的陈述中的tree/1and不是谓词。你基本上在这里写的是：leaf/1leaf(X) = tree(X)

=(leaf(X), tree(X))

因此，您调用(=)/2谓词、withleaf(X)和tree(X)术语。

现在在 Prolog 中，两个术语是统一的，如果：

1. 这些是同一个原子；或者
2. 它是一个具有相同函子和元数的术语，并且参数是元素可统一的。

由于 functorleaf/1不等于 functor tree/1，这意味着leaf(X)和tree(X)不能相等。

即使我们定义一个谓词以检查两个谓词在语义上是否相同，这也会失败。在这里，您基本上旨在解决无法确定的等价问题。这意味着，一般来说，一个人无法构建一种算法来验证两台图灵机是否决定了相同的语言。Prolog 是图灵完备的语言，我们基本上可以翻译图灵机中的任何谓词，反之亦然。这意味着我们无法计算两个谓词是否接受相同的输入。