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?
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.