What is the optimal "most general unifier" algorithm?

Question

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.

Answer 1

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

Answer 2

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.