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?

  • $\begingroup$ 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). $\endgroup$
    – MaiaVictor
    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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.