Higher-order matching is the problem given t = u where t, u are terms of simply typed λ-calculus and u is closed, is there a substitution θ such that t θ and u have the same normal form with respect to βη-equality: can t be pattern matched to u? The problem was conjectured to be decidable by Huet . Loader showed that it is undecidable when β-equality is the same normal form by encoding λ-definability as matching .
|Title of host publication||Automated Deduction|
|Subtitle of host publication||CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings|
|Publisher||Springer Berlin Heidelberg|
|Number of pages||2|
|Publication status||Published - 2007|