SpringerLink - Book Chapter

Formalizing the Halting Problem in a Constructive Type Theory

Book Series

Lecture Notes in Computer Science

Publisher

Springer Berlin / Heidelberg

ISSN

0302-9743 (Print) 1611-3349 (Online)

Volume

Volume 2277/2002

Book

Types for Proofs and Programs

DOI

10.1007/3-540-45842-5

2002

ISBN

978-3-540-43287-6

DOI

10.1007/3-540-45842-5_10

Page

724

Subject Collection

Computer Science

SpringerLink Date

Tuesday, January 01, 2002

Formalizing the Halting Problem in a Constructive Type Theory

Kristofer Johannisson⁶

(6)	Department of Computing Science, Chalmers University of Technology, SE-412 96 Göteborg, Sweden

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.

Kristofer Johannisson
Email: krijo@cs.chalmers.se

Formalizing the Halting Problem in a Constructive Type Theory

Fulltext Preview (Small, Large)