Title:	Computational Foundations of Basic Recursive Function Theory
Authors:	Constable, Robert L. Smith, Scott Fraser
Keywords:	computer science technical report
Issue Date:	Mar-1988
Publisher:	Cornell University
Citation:	http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR88-904
Abstract:	The theory of computability, or basic recursive function theory as it is often called, is usually motivated and developed using Church's Thesis. Here we show that there is an alternative computability theory in which some of the basic results on unsolvability become more absolute, results on completeness become simpler, and many of the central concepts become more abstract. In this approach computations are viewed as mathematical objects, and the major theorems in recursion theory may be classified according to which axioms about computation are needed to prove them. The theory is a typed theory of functions over the natural numbers, and there are unsolvable problems in this setting independent of the existence of indexings. The unsolvability results are interpreted to show that the partial function concept, so important in computer science, serves to distinguish between classical and constructive type theories (in a different way than does the decidability concept as expressed in the law of excluded middle). The implications of these ideas for the logical foundations of computer science are discussed, particularly in the context of recent interest in using constructive type theory in programming.
URI:	http://hdl.handle.net/1813/6744
Appears in Collections:	Computer Science Technical Reports

Files in This Item: File Description Size Format 88-904.pdf 1.6 MB Adobe PDF View/Open 88-904.ps 337.14 kB Postscript View/Open

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.