Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Abstract: Formalizing the Halting Problem...
Formalizing the Halting Problem in a Constructive Type Theory
Abstract
We present a formalization of the halting problem in Agda, a language based on Martin-Löf'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.
This paper is published in LNCS 2277.