Prolog - 证明树错过了可能性

Question

我有以下 Prolog 程序:

p(f(X), Y) :- p(g(X), g(Y)).
p(g(X), Y) :- p(f(Y), f(X)).
p(f(a), g(b)).

必须为谓词 p(X, Y) 绘制序言证明树。

问题:

• 为什么 Y 匹配到 Y1/Y 而不是 Y/Y1 以及为什么使用 Y更进一步？
• 如果我匹配一个谓词(例如 p(X, Y))，我会得到一个新的谓词(例如 p(g(X1), g(Y)))) - 为什么只包含 p(g(X1), g(Y)) 一个子树？我的意思是，它不应该有 3 个，因为知识库包含 3 个陈述 - 而不是只有 1 个？
• 为什么树的每一层都与 X2/X1 等匹配？而不是之前的谓词？ 不应该是 g(X1)/fX5, g(Y1)/Y5 吗？

注意:可能好像没做过教程什么的。但我做到了......我感谢每一个帮助。

Answer 1

老实说，我很少见过比您在此处展示的方法更更糟糕的 Prolog 解释方法。

是，我希望作者在这两种情况下都指的是 Y/Y1 而不是 Y1/Y，否则符号会很不一致.

关于您的其他问题:您正面临着从 Prolog 的极端可操作性角度来看时出现的常见问题。核心问题是此方法无法扩展:您没有实现此方法的心智能力。不要把这个当成个人的:一般来说，人类不善于记住呈指数增长的执行树的所有细节。这使得整个方法极其繁琐且容易出错。相比之下，想想为什么人类大师在很多年前就已经停止与国际象棋计算机竞争。在这个具体案例中，请注意例如最右边的分支甚至不会出现在实际的 Prolog 执行中，但图表错误地表明它出现了!

这里的部分问题是术语的混淆:请注意 Prolog 使用统一(不是“匹配”，这是单方面的统一)。当您使用子句head统一目标并且统一成功时，您将获得变量的绑定(bind)。您继续这些绑定(bind)。

要使整个方法远程可行，请考虑程序的片段。

例如，假设我只给你以下事实:

p(f(a), g(b)).

然后你查询:

?- p(X, Y).
X = f(a),
Y = g(b).

此答案显示了 X 和 Y 的绑定(bind)。首先确保您了解这一点，并了解这些绑定(bind)与“新谓词”(不会出现!)之间的区别。

此外，没有“陈述”，而是 3 个子句，它们是逻辑替代词。

现在，再次简化整个任务，考虑您程序的以下片段，其中我仅查看两个规则 :

p(f(X), Y) :- p(g(X), g(Y)).
p(g(X), Y) :- p(f(Y), f(X)).

已经有了这个程序，我们得到:

?- p(X, Y).
nontermination

添加一个进一步的纯子句不能阻止这种不终止。因此，我建议您从程序的这个简化版本开始，并更深入地考虑它。

从那里，您可以再次添加剩余的事实，并考虑差异。