这是过去考试中关于 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 一直查找直到找到解决方案？
【问题讨论】：
标签： prolog unification
是的，它确实统一了，而且它这样做是因为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，在统一过程之后，仍然是未绑定的。统一是在未绑定的变量上执行的，这意味着：
h(c, d) = h(W, d) 的统一返回 h(_) = h(_)，这允许统一继续，因为 h 是一个术语，而不是未绑定的 var；
d = d 的统一是术语的匹配，不构成归属——或绑定；
c = W 的统一形成一个属性，变量W 绑定到术语c，因为它之前没有绑定——否则会进行比较；
X = g(Y) 的统一只是将未绑定变量X 绑定到术语g(Y)，而g(Y) 是一个具有未绑定变量的术语，因为没有可用的统一到g(Y)。
问候！
【讨论】：