2

这是过去考试中关于 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 = g(Y) 因为大写 X 一直查找直到找到解决方案？

4

1 回答 1

4

是的，它确实统一了，它这样做是因为这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)。

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

统一后返回答案，通常false在无法匹配/进一步匹配时返回。

正如 CapelliC 所指出的Y，在统一过程之后，变量 仍然是未绑定的。统一是在未绑定的变量上执行的，这意味着：

  • h(c, d) = h(W, d)return的统一h(_) = h(_)，这允许统一继续，因为h是一个术语，而不是一个未绑定的 var；

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

  • 统一c = W形成一个属性，并且变量W绑定到术语c，因为它之前没有绑定 - 否则将执行比较；

  • 的统一X = g(Y)只是将未绑定的变量绑定X到 term g(Y)，并且g(Y)是具有未绑定变量的术语，因为没有可用的统一g(Y)。

问候！

于 2012-12-13T22:29:33.617 回答