Higher Order β Matching is Undecidable
Ralph Loader · Logic Journal of IGPL · 2003
Abstract We show that the solvability of matching problems in the simply typed λ-calculus, up to β equivalence, is not decidable. This decidability question was raised by Huet [4]. Note that there are two variants of the question: that concerning β equivalence (dealt with here), and that concerning βη equivalence. The second of these is perhaps more interesting; unfortunately the work below sheds no light on it, except perhaps to illustrate the subtlety and difficulty of the problem.