Higher-order unification

Question

I'm working on a higher-order theorem prover, of which unification seems to be the most difficult subproblem.

If Huet's algorithm is still considered state-of-the-art, does anyone have any links to explanations of it that are written to be understood by a programmer rather than a mathematician?

Or even any examples of where it works and the usual first-order algorithm doesn't?

Answer 1

State of the art — yes, so far as I know all algorithms more or less take the same shape as Huet's (I follow theory of logic programming, although my expertise is tangential) provided you need full higher-order matching: subproblems such as higher-order matching (unification where one term is closed), and Dale Miller's pattern calculus, are decidable.

Note that Huet's algorithm is the best in the following sense — it is like a semi-decision algorithm, in that it will find the unifiers if they exist, but it is not guaranteed to terminate if they do not. Since we know that higher-order unification (indeed, second-order unification) is undecidable, you can't do better than that.

Explanations: The first four chapters of Conal Elliott's PhD thesis, Extensions and Applications of Higher-Order Unification should fit the bill. That part weighs almost 80 pages, with some dense type theory, but its well motivated, and is the most readable account I've seen.

Examples: Huet's algorithm will come up with the goods for this example: [X(o), Y(succ(0))]; which of necessity will perplex a first-order unification algorithm.

Answer 2

An example of higher-order unification (really second-order matching) is: f 3 == 3 + 3, where == is modulo alpha, beta, and eta-conversion (but not assigning any meaning to "+"). There are four solutions:

\ x -> x + x \ x -> x + 3 \ x -> 3 + x \ x -> 3 + 3 

In contrast, first-order unification/matching would give no solution.

HOU is very handy when used with HOAS (higher-order abstract syntax), to encode languages with variable binding while avoiding the complexity of variable capture etc.

My first exposure to the topic was the paper "Proving and Applying Program Transformations Expressed with Second Order Patterns" by Gerard Huet and Bernard Lang. As I recall, this paper was "written to be understood by a programmer". And once you understand second-order matching, HOU isn't much further to go. A key result of Huet's is that the flexible/flexible case (variables as head of a term, and the only case not appearing in matching) is always solvable.