2003 | OriginalPaper | Buchkapitel
Encoding of the Halting Problem into the Monster Type and Applications
verfasst von : Thierry Joly
Erschienen in: Typed Lambda Calculi and Applications
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
The question whether a given functional of a full type structure (FTS for short) is λ-definable by a closed λ-term, raised by G. Huet in [Hue75] and known as the Definability Problem, was proved to be undecidable by R. Loader in 1993. More precisely, R. Loader proved that the problem is undecidable for every FTS over at least 7 ground elements (cf [Loa01]).We solve here the remaining non trivial cases and show that the problem is undecidable whenever there are more than one ground element. 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 $$ \mathbb{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. Another consequence of the latter fact, besides the result stated above, is the undecidability of the β-Pattern Matching Problem, recently established by R. Loader in [Loa03].