Commentary by Chris Pressey

This work is distributed under a CC-BY-ND-4.0 license, with the following explicit exception: the ratings may be freely used for any purpose with no limitations.

Unification

Unification: A Multidisciplinary Survey

• rating: 1

Gives a pretty good historical overview.

Has a simple example of resolution.

Has a basic example of parsing with unification-based grammar.

Says some things about unification modulo equational theories. Under commutivity, there can be more than one MGU, but at most there will be a finite number. Under associativity, though, there can be an infinite number. Under associativity AND idempotency, no complete set of GUs exists; for every two unifiable terms s and t, for every unifier u, there exists a more general unifier v.

I'm not really sure how it is that you can obtain more and more GUs without bound, but OK!

Correcting a Widespread Error in Unification Algorithms

• rating: 1

Basically it seems easy to forget to remember that unification is symmetric; if we are unifying some variable X on the LHS with something on the RHS, we do that; but if we are unifying something (non-variable) on the LHS, we forget to check if the thing on the RHS is a variable, and unify with it.

Imperative implementations don't have the problem as much, probably because when destructively updating the thing, it's more obvious if you haven't covered all cases in testing.

When this error is in unification used in backward chaining (Prolog) it's rare for it to show up, which is probably why it's so widespread.

Norvig gives some good test cases for any implementation of unification, in particular:

unify(
  p(X, Y, a),
  p(Y, X, X)
)

which does have a valid unification (X = Y = a) but causes either a failure or a hang (depending on occurs check or not) on implementations with the error.

Notes: Unification

• rating: 1

.

mrocklin/unification

• rating: 1

.

parsonsmatt/unification: implementation of the first order logic unification algorithm in Haskell

• rating: 1

.

jozefg/higher-order-unification: A small implementation of higher-order unification

• rating: 1

The explanation.md file in there has a very good explanation of what's going on. What is remarkable to me is that Huet's higher-order unification algorithm is not guaranteed to terminate. It's basically trying to complete two incomplete programs so that they evaluate to the same value, which "of course" is an undecidable problem. So the algorithm is only a semi-decision procedure. But in practice it does very well at terminating in the cases that are of interest.