Unification, part 2

Last time on FAIC I defined unification as a fancy word for taking a system of statements that contain placeholder variables and finding values for those variables which make the statements all true. We've seen that we can do that with mathematical statements (also known as "equations") and that the type unification algorithm described in Milner's paper does so for type assumptions. Last time I posed the question: what about arbitrary expressions in a programming language?

Sure, why not? Let's look at an example typical to functional languages.

In many functional languages we have the binary operator head :: tail, which takes two values; the head of a list, say, a number, and the tail, say, a list of numbers, possibly empty. The result is a new list of numbers. nil is an expression that is used for the empty list. Suppose we make this equation

h0 :: h0 :: nil = 2 :: h1

Again, h0 and h1 are variables in the mathematical sense, not in the sense of elements of a programming language, and similarly, the equality is logical equality, not an operator in any programming language. From now on I'm going to label these "holes" with the letter h and a number to disambiguate them, so that it is clear when I am talking about a hole that needs something filled into it.

What we're looking for here is "what expressions could we put into h0 and h1 that would make these two program fragments mean the same thing?" The only values are to substitute 2 for h0 and 2 :: nil for h1, which gives us 2 :: 2 :: nil on both sides.

Maybe the answer was immediately obvious to you, and maybe it was not, but regardless it is not 100% clear whether there is a straightforward algorithm that gives you values for the holes when presented with such a unification problem.

The syntax might be throwing us off a bit, and it's not very general. What if instead of an operator :: we just called a function like we do in C#, a function that took a head and a tail? Such a function is traditionally called "cons", because it constructs a list:

cons(h0, cons(h0, nil)) = cons(2, h1)

Again, remember that we are looking for expressions that we can sub in for the holes that make the equality true.

In this form it is a bit easier to see the algorithm. The first argument to cons on the left is h0, the first argument on the right is 2, so h0 must be 2, and perhaps you see how it goes from there.

We could also model this as a parse tree.

 cons cons / \ / \h0 cons = 2 h1 / \ h0 nil

I find that with the tree diagram it becomes much easier to see what the solution is. I'm not going to go through the whole algorithm here, but maybe you see how it goes. Basically, we recurse through the tree, solving unification problems on the children, and then we check the results to see if there were any contradictions.

This algorithm that I've failed to adequately describe is called the first-order unification algorithm, and it can solve any simple unification problem in linear time; it produces a substitution if one exists or fails if it does not.

What do I mean by "simple" unification problem? Well, notice that this simple algorithm would fail if given the problem

add(h0, 10) = add(13, 1)

Because h0 would unify with 13, but 10 would not unify with 1, and we'd get a unification failure, even though obviously there is a value for h0 that makes the equation true. Unification algorithms that understand additional facts about arithmetic or other domains are "unification modulo theory".

Similarly, unification algorithms that involve the lambda abstraction are "higher order unification" algorithms. The higher-order unification problem is in general not solvable, but that's a topic for another day.

Similarly, it is I hope easy to see how unifying one equation generalizes to multiple equations; you just unify on each equation, and then check to see if you deduced contradictions, and then combine the solutions together.

All of this was meant to introduce what I really want to talk about, which is antiunification. If unification is the process of finding values of variables that induce certain statements to be all true, what on earth could the opposite of that be?

Next time on FAIC: We'll find out.