11

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.

Erik Kaplun
  • 37,128
  • 15
  • 99
  • 111
Paul Hollingsworth
  • 13,124
  • 12
  • 51
  • 68

2 Answers2

9

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

Frank Shearar
  • 17,012
  • 8
  • 67
  • 94
starblue
  • 55,348
  • 14
  • 97
  • 151
  • Do you know of a document that describes it? Is it basically the same as is described in SICP? – Paul Hollingsworth May 14 '09 at 11:06
  • Yes, the simple algorithm is essentially the same as described in SICP. The usual presentation uses rules like decomposition, clash, occurs check, ..., so you might want to search for that. – starblue May 15 '09 at 17:29
5

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.

Frank Shearar
  • 17,012
  • 8
  • 67
  • 94