prolog - Prolog 中的统一

Question

这是一个关于 Prolog 统一的过去考试中的问题。 我们应该说它们是否统一，然后是实例化。

f(a,g(b,a)) and f(X,g(Y,X))

这统一了 a = X, g(b,a) = g(Y,X) 并且非常简单

f(g(Y),h(c,d)) and f(X,h(W,d)) 

我不认为这个统一是因为 g(Y) =/X，尽管 h(c,d) 确实与 h(W,d) 统一。尽管大写的 X 会一直查找直到找到解决方案，所以 X = g(Y) 有可能吗？

Answer 1

是的，它确实统一了，这样做是因为 g(Y)是一个要评估的术语，以及 a -- 在您指出的第一个示例中。

您可以在 prolog 解释器中检查评估:

?- f(g(Y),h(c,d)) = f(X,h(W,d)).
X = g(Y),
W = c.

统一过程以深度优先的方式进行，统一成员并返回每个可用的答案，直到不可能进行进一步的组合。

这意味着 f(g(Y),h(c,d)) = f(X,h(W,d)) 需要统一方法 ，找出可用的匹配:g(Y) = X, h(c, d) = h(W, d) .

然后对 g(Y) = X 进行统一，由于没有进一步可能的减少，因此返回 X = g(Y) .

然后，在匹配的h(c, d) = h(W, d)上调用相同的方法。 ，这给你 c = W ，并且没有其他匹配，因此，结果为 W = c .

统一后返回答案，一般返回false指出何时无法匹配/进一步匹配。

正如 CapelliC 所指出的，变量 Y ，在统一过程之后，仍然不受约束。统一是在未绑定(bind)变量上执行的，这意味着:

• h(c, d) = h(W, d)的统一返回h(_) = h(_) ，这使得统一得以继续，因为 h是一个术语，而不是一个未绑定(bind)的变量；

• d = d的统一是术语匹配，并不形成归属或约束力；

• c = W的统一形成归因，变量 W绑定(bind)到术语 c ，因为它之前没有绑定(bind)——否则将执行比较；

• X = g(Y)的统一只是绑定(bind)未绑定(bind)变量 X到术语g(Y) ，和g(Y)是一个带有未绑定(bind)变量的术语，因为 g(Y) 没有可用的统一.

问候!