什么是统一术语顺序有关系吗？

Posted 2023-05-08

【中文标题】什么是统一术语顺序有关系吗？

【英文标题】：Does it matter what is unification terms sequence?

【发布时间】：2020-02-28 10:45:12

【问题描述】：

假设我有两个术语 T1 和 T2。我统一了两个术语并得到了结果。

我的问题是：如果我改变术语的位置并统一术语 T2 和 T1 - 结果会相同还是不同？

我尝试更改条款并得到相同的结果。但理论上我可以读到：在 Prolog 中序列很重要。

那么你怎么看 - 结果是相同的还是不同的，为什么？

【参考方案1】：

仅通过将X = Y 替换为Y = X 即可显示出差异是极不可能的。

只要您考虑句法统一（使用发生检查）或理性树统一，唯一的区别可能是一些最小的性能差异。

当超出这些明确定义的关系时，会出现更多明显的差异：

混合两者时，统一可能不会终止。我只能在 SWI 中给你一些相关的例子：

.

?- X = s(X), unify_with_occurs_check(X, s(X)).
X = s(X).

?- unify_with_occurs_check(X, s(X)), X = s(X).
false.

上面，目标的交换性被破坏了。但是，我们正在将两种互不相容的理论相互混合。所以，我们真的不能抱怨。

?- Y = s(Y), unify_with_occurs_check(X-X,s(X)-Y).
false.

?- Y = s(Y), unify_with_occurs_check(X-X,Y-s(X)).
Y = X, X = s(X).

在这里我们只是交换参数的顺序。一般的直觉是，交换（一致地）函子的参数不应该产生差异，但是，这里再次不兼容的混合是罪魁祸首。

涉及约束和副作用时。尽管如此，我还是无法产生这样的案例，只是将X = Y 替换为Y = X。