Logic in Computer Science (LICS 1988)

Paper: Computational foundations of basic recursive function theory (at LICS 1988)

Authors: Robert L. Constable Scott F. Smith

Abstract

The theory of computability often called basic recursive function theory is usually motivated and developed using Church's thesis. It is shown 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 serves to distinguish between classical and constructive type theories

BibTeX

  @InProceedings{ConstableSmith-Computationalfounda,
    author = 	 {Robert L. Constable and Scott F. Smith},
    title = 	 {Computational foundations of basic recursive function theory},
    booktitle =  {Proceedings of the Third Annual IEEE Symp. on Logic in Computer Science, {LICS} 1988},
    year =	 1988,
    editor =	 {Yuri Gurevich},
    month =	 {July}, 
    pages =      {360--371},
    location =   {Edinburgh, Scotland, UK}, 
    publisher =	 {IEEE Computer Society Press}
  }