The Question
What is the most efficient MGU algorithm? What is its time complexity? Is it simple enough to describe as 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.
i.e.
mgu(e1,e2) = (x = z), q = (* y 3), y = unbound, r = 5
By "most general", 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.