We present a formalization of the halting problem in Agda, a language based on Martin-Lof's intuitionistic type theory. The key features are: -We give a constructive proof of the halting problem. The "constructive halting problem" is a natural reformulation of the classic variant. -A new abstract model of computation is introduced, in type theory. -The undecidability of the halting problem is proved via a theorem similar to Rice's theorem. The central idea of the formalization is to abstract from the details of specific models of computation. This is accomplished by formulating a number of axioms which describe an abstract model of computation, and proving that the halting problem is undecidable in any model described by these axioms.
展开▼
