So here's the unification algorithm. It takes (a `source' number of variables n and) two terms (with at most n variables). The return type is made with option to allow for the possibility of failure. A successful return is, in fact, a pair: the `target' number of variables and a source-to-target substitution. Since the former is inferrable from the latter, I casually omit it.

Of course, the main function just calls its bounded cousin with the most optimistic guess it can think of.

I've grouped the lines of bmgu behaviourally as follows:

• passing on a failure
• splitting the rigid-rigid step case; notice that the conjunction of unification sub-problems becomes a composition of recursive calls, passing the accumulator along; they're structural, see?
• if we've hit a variable and the accumulator is iota, then we've got a genuine flex-rigid or flex-flex base case: see next slide
• otherwise, strip off the front knockout, apply it, unify the results, and glue the knockout back on if successful

Now, the fourth of these is apparently non-structural, in that it blows up the terms. Aha, but it is structural! It decreases the source number of variables! The nested recursion structure goes as follows (outer to inner):

• recursion on the source number of variables: this entitles me to unify recursively anything I like, once I've eliminated a variable
• recursion on the first tree: in the step case, this entitles me to unify the branches with anything I like, and with any accumulator I like; I use this privilege in the Ackermann style: unification is an expensive business
• case analysis on the second tree
• case analysis on the accumulator (by the way, it's slightly inaccurate to write only one failure-passing clause, when this happens at the innermost match: I don't want to write one line for each case, you don't want to read one line for each case, and my program will happily generate them automatically)

Do I really need the induction on the source number of variables? I don't believe I can get away with just an outer structural recursion on the accumulator. Think what happens to the rigid-rigid case when the accumulator is iota: I can only make recursive calls with accumulator iota, so I can't pass the accumulator from one branch to the other. Induction on the source number allows me any substitution descending from that set of variables.

This is a key question if we are to understand the status of dependently typed programming, relative to programming with, say, nested types. In this program, I make computational use of type indices: I exploit directly the dependency of types on terms. If this index recursion is critical (and I suspect it is), then this program shows that terms-in-types really buys us something.

Certainly, simply-typed versions require general recursion. There's plenty of technology supporting proofs of such programs these days, including neat separation of partial correctness from termination. There is still an overhead in attaching an appropriate well-founded ordering externally and proving that it is respected by the program. I get termination for free, and I get a bona fide LEGO term which provably computes most general unifiers, with no need of propositional jiggery-pokery to sustain its recursive behaviour.

Next: base cases | Prev: embeddings | Up: contents