×

A simple proof of the undecidability of inhabitation in \(\lambda P\). (English) Zbl 0872.68035

Summary: It has been known that the simplest system with dependent types, \(\lambda P\), is undecidable, in that sense that the set \(\{(A,\Gamma) \mid \exists p\Gamma \vdash_{\lambda P} p:A\}\) is non-computable. The proof runs as follows. First, there is an obvious embedding of predicate logic into \(\lambda P\). This is the principle idea of one of the basic members of the AUTOMATH family, AUT-QE, and also later of Edinburgh LF. It can be shown that this embedding is conservative (Berardi; Barendsen and Geuvers). This is not completely obvious, since \(\lambda P\) has functions of arbitrarily high type at its disposal. Now it follows from Gödel’s technique (proving the incompleteness theorems) that arithmetic and even a finitely axiomatizable part of it (Robinson’s arithmetic) is essentially undecidable. Therefore \(\lambda P\) is also undecidable. This is quite a long path to the result – admittedly quite beautiful, passing along classical details like the Chinese remainder theorem – but almost too much. Fortunately, the authors of this paper have given a very direct argument showing the same result, by a surprisingly straightforward encoding of a register machine.

MSC:

68Q05 Models of computation (Turing machines, etc.) (MSC2010)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] DOI: 10.1145/321160.321170 · Zbl 0118.25401 · doi:10.1145/321160.321170
[2] Barendregt, Handbook of Logic in Computer Science 2 pp 117– (1992)
[3] Geuvers, Proceedings of the 1 pp 79– (1993)
[4] DOI: 10.2307/2272390 · Zbl 0358.02012 · doi:10.2307/2272390
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.