什么是最优的“最一般统一器”算法？

Question

11

问题

什么是最高效的MGU算法？它的时间复杂度是多少？它是否简单到足以在Stack Overflow回答中描述？

我一直在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}和{z ↦ 1}，这样也会使e1和e2等价，但这样会更加具体。

SICP文章似乎暗示这是相当昂贵的。

顺便提一下，我之所以问这个问题，是因为我知道类型推断也涉及到这个“合一”算法，我想理解它。

- Paul Hollingsworth

2个回答

5

Baader和Snyder 发布了几个统一算法，分别用于语法统一和等式统一。

他们指出，他们的第三个语法统一算法（在第2.3节中）的运行时间为 O(n×α(n))，其中 α(n) 是反阿克曼函数 - 在实际情况下它相当于一个小常数。

- Frank Shearar

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- starblue · Accepted Answer

实际应用中使用的简单算法（例如在Prolog中）对于病态情况是指数级的。理论上更有效的算法由[Martelli和Montanari][1]提出（如果我没记错，它是线性的），但对于实际中出现的简单情况，它要慢得多，因此很少使用。