algorithm - 什么是最佳的“最通用的统一器”算法？

Question

问题

什么是最有效的 MGU 算法？它的时间复杂度是多少？在堆栈溢出答案中描述是否足够简单？

我一直试图在 Google 上找到答案，但一直在寻找我只能通过 ACM 订阅访问的私人 PDF。

我在 SICP 中找到了一个讨论：这里

解释什么是“最通用的统一算法”：采用两个包含“自由变量”和“常量”的表达式树......例如

e1 = (+ x? (* y? 3) 5)
 e2 = (+ z?q?r?)

然后最通用统一器算法返回使两个表达式等效的最通用绑定集。例如：

mgu(e1, e2) = { x ↦ z,
                q ↦ (* y 3),
                y ↦ unbound,
                r ↦ 5 }

“最一般”的意思是您可以改为绑定{x ↦ 1}and{z ↦ 1}并且这也可以使e1和e2等效，但它会更具体。

SICP 文章似乎暗示它相当昂贵。

对于信息，我问的原因是因为我知道类型推断也涉及这种“统一”算法，我想了解它。

score 9 · Accepted Answer

在实践中使用的简单算法（例如在 Prolog 中）对于病理病例是指数级的。

[Martelli and Montanari][1] 有一个理论上更有效的算法（IIRC 它是线性的），但是对于实际发生的简单情况来说它的速度要慢得多，因此使用得不多。

score 5 · Accepted Answer

Baader 和 Snyder发表了几种统一算法，用于句法统一和等式统一。

他们声明他们的第三个句法统一算法（在第 2.3 节中）运行在O(n×α(n))哪里α(n)是逆阿克曼函数 - 在实际情况下它相当于一个小常数。

2 回答 2