为什么这个表达不统一答案

【问题标题】：Why does this expression not unifiy为什么这个表达不统一
【发布时间】：2019-05-04 00:50:12
【问题描述】：

我定义了以下知识库：

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

并且期待查询：

leaf(X) = tree(X).

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

不幸的是，激活跟踪不会产生任何有用的结果。如果您想尝试一下，这里是这个最小示例的link。

【问题讨论】：

如果你解释你得出这个结论的逻辑in your question，而不仅仅是because for any arbitrary value X this equation should hold.，这会有所帮助，就像对不了解Prolog的人一样解释它。我可以很容易地想到很多方法来回答这个问题，但除非我帮助你纠正你对 Prolog 如何执行目标的理解的错误，否则我只会随机猜测。这是一个很好的问题，但目前你的问题可能会引发一场讨论，这将浪费我和你的时间。
@GuyCoder 非常感谢您的反馈。我希望我已经澄清了我的推理。
感谢您的澄清。这种可能性甚至不在我的清单上。
谓词不是返回值的函数。所以leaf(X) = tree(X) 不会评估leaf(X) 和tree(X) 并尝试比较它们或统一某种结果。一个合理的查询可能是leaf(X), tree(Y), X = Y。但是，您的事实并不完全有意义。 leaf(_). 表示 anything 是一片叶子。例如，leaf([a,b,foo(x,y),2,3]) 成功。
@lurker 我知道谓词不返回值，但我希望统一算法能够找出它可以用tree 代替leaf，然后统一leaf(X)=leaf(X)。跨度>

标签： prolog unification

【解决方案1】：

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

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

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

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

现在在 Prolog 中，两个术语是 unifiable 如果：

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

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

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

【讨论】：

或者更具体地说，我会说“...在 Prolog 中，两个术语是 unifiable 如果：（1）术语是相同的 atom，或 (2) 术语具有相同的函子/数量，并且参数是元素方面的unifiable”。否则，您必须定义“等效”术语的含义。
@lurker：同意，这是一种更好的指定方式:)