# What algorithm solves high-order unification for untyped terms in most cases?

High-order pattern matching is an undecidable problem. That means there is no algorithm that, given an equation a => b, where a and b are terms on the simply typed lambda calculus, a containing free variables, finds a substitution S such that aS => b, where => stands for "has the same beta normal form" (up to variable renaming). For example, given the following problem:

a = (λt . t
(F (λ f x . (f (f (f x)))))
(F (λ f x . (f (f x)))))
b = (λ t . t
(λ f x . (f (f (f (f (f (f x)))))))
(λ f x . (f (f (f (f x))))))


One can come with the solution:

 F = (λ a b c . (a b (a b c)))


Since that substitution makes a = b hold. My question is: what's an efficient (i.e., polytime) algorithm that solves this problem for as many cases as possible?

• What I tried: I've googled and read many papers about high order unification, but most of them are restricted for the simply typed case and even for those I didn't manage to find a comprehensible explanation (most resources are often in the shape of a whole book dedicated to the issue, which often require a broad knowledge of many topics I'm not even aware of). Sep 30 '15 at 15:19

Maybe you should try nominal unification. In the paper nominal unification, it gives 4 examples which are untyped $\lambda$-terms.