最佳的“最通用的统一器”是什么？ 算法？
问题
什么是最有效的 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} 和 {z ↦ 1} 这也将使 e1 和 e2 等效，但会更具体。
SICP 文章似乎暗示它相当昂贵。
作为信息，我问的原因是因为我知道类型推断也涉及这种“统一”算法，我想了解它。
The Question
What is the most efficient MGU algorithm? What is its time complexity? Is it simple enough to describe in a stack overflow answer?
I've been trying to find the answer on Google but keep finding private PDFs that I can only access via an ACM subscription.
I found one discussion in SICP: here
Explanation of what a "most general unification algorithm" is:
Take two expression trees containing "free variables" and "constants"... e.g.
e1 = (+ x? (* y? 3) 5) e2 = (+ z? q? r?)
Then the Most General Unifier algorithm returns the most general set of bindings that makes the two expressions equivalent. For example:
mgu(e1, e2) = { x ↦ z,
q ↦ (* y 3),
y ↦ unbound,
r ↦ 5 }
By "most general," what is meant is that you could instead bind {x ↦ 1} and {z ↦ 1} and that would also make e1 and e2 equivalent but it would be more specific.
The SICP article appears to imply that it is reasonably expensive.
For info, the reason I'm asking is because I know that type inference also involves this "unification" algorithm and I'd like to understand it.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（2）
实践中使用的简单算法（例如在 Prolog 中）对于病理情况是指数级的。
[Martelli 和 Montanari][1] 有一种理论上更有效的算法（IIRC 它是线性的），但对于实际中发生的简单情况要慢得多，因此使用不多。
[1] http://www.nsl.com/misc/papers/martelli -montanari.pdf
The simple algorithm that is used in practice (e.g. in Prolog) is exponential for pathological cases.
There is a theoretically more efficient algorithm by [Martelli and Montanari][1] (IIRC it is linear), but it is much slower for the simple cases which occur in practice, so it is not used much.
[1] http://www.nsl.com/misc/papers/martelli-montanari.pdf
Baader 和 Snyder 发布了几种统一算法，用于句法统一和方程统一。
他们指出，他们的第三个句法统一算法（第 2.3 节）的运行时间为
O(n×α(n))，其中α(n)是反阿克曼函数 - 在实际情况下它相当于一个小常数。Baader and Snyder published several unification algorithms, for both syntactic unification and equational unification.
They state that their third syntactic unification algorithm (in section 2.3) runs in
O(n×α(n))whereα(n)is the inverse Ackermann function - in practical situations it's equivalent to a small constant.