Decidability of fourth-order matching
Vincent Padovani · Mathematical Structures in Computer Science · 2000
Higher Order Matching consists of solving finite sets of equations of the form u =βηv, where u, v are simply typed terms of λ-calculus, and v is a closed term. Whether this problem is decidable is an open question. In this paper its decidability is proved when the free variables of all equations are of order at most 4 – we actually extend this result to a more general situation in which in addition to equations, disequations are also considered.