On λ-Definability I: the Fixed Model Problem and Generalizations of the Matching Problem

Abstract

The question whether a given functional of some full type structure (FTS for short) is λ-definable by a closed λ-term, known as the Definability Problem, was proved to be undecidable by R. Loader in 1993 (cf [Loa01a]). Later on, R. Loader refined his first result by establishing that the problem is undecidable for every FTS over at least 3 ground elements (cf [Loa01b]).

We solve here the remaining non trivial case and show that the problem is undecidable whenever there are at least two ground elements. The proof is based on a direct encoding of the Halting Problem for register machines into the Definability Problem restricted to the functionals of the Monster type M=(((o→o)→o)→o)→(o→o). It follows that this new restriction of the Definability Problem, which is orthogonal to the ones considered so far, is also undecidable. The latter fact yields a particularly simple proof of the undecidability of the -Pattern Matching Problem, recently established by R. Loader in [Loa03].