什么是最佳"最通用的统一者"算法？

Question

问题

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

我一直试图在谷歌找到答案,但继续寻找我只能通过ACM订阅访问的私人.PDF.

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

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

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

然后,Most General Unifier算法返回最通用的绑定集,使两个表达式等效.

即

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

通过"最一般",您可以改为绑定(x = 1)和(z = 1),这也会使e1和e2等效,但它会更具体.

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

有关信息,我问的原因是因为我知道类型推断也涉及这种"统一"算法,我想了解它.

Answer 1

在实践中使用的简单算法(例如在Prolog中)对于病理情况是指数的.

Martelli和Montanari(IIRC它是线性的)理论上有一个更有效的算法,但是对于在实践中出现的简单情况来说它要慢得多,因此它的用处不多.

Answer 2

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

他们指出，他们的第三个句法合一算法（2.3节）运行在O(n×?(n))其中?(n)的逆阿克曼功能-在实际情况下，它是相当于一个小的常数。