Computability in HOL: A Model for Computation in Formal Logic

Research output: Book/Report/clinical guidelinesReportResearch

Abstract

This paper describes the implementation of a formal model for computability theory in the logical system HOL. The computability is modeled through an imperative language formally defined with the use of the Backus-Naur form and natural semantics. I will define the concepts of computable functions, recursive sets, and decidable or partially decidable predicates, and show how they relate to each other. A central subject will be that of the use of only a finite amount of space by any single statement. This leads to a theorem about the computability of the composition of computable functions. The report will then evolve in two directions: The first subject is the reduction of recursive sets, leading to the unsolvability of the halting problem. The other is two general results of computability theory: The s-m-n theorem and Kleene's version of the 2nd recursion theorem. The use of the HOL system implies that the theory must be proven with the absence of Church's thesis, and, in fact, all proofs have to be done in detail. The paper will show how the HOL system is used to define the modeling language, as well as demonstrating the interaction between the HOL system and the theory. At some points the HOL system will strongly influence the actual definitions and lemmas in the theory.
Original languageEnglish
Number of pages122
Publication statusPublished - 1994

Cite this