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

Issue title: Typed Lambda Calculi and Applications 2003, Selected Papers

Article type: Research Article

Authors: Joly, Thierry

Affiliations: Équipe Preuves, Programmes et Systèmes, Université Paris VII, 2, place Jussieu, 75251 Paris cedex 05, France. joly@pps.jussieu.fr

Note: [] Address for correspondence: Équipe Preuves, Programmes et Systèmes, Université Paris VII, 2, place Jussieu, 75251 Paris cedex 05, France.

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].

Journal: Fundamenta Informaticae, vol. 65, no. 1-2, pp. 135-151, 2005