Computational foundations of basic recursive function theory
type: Item
instance of: scholarly article
title: Computational foundations of basic recursive function theory
zbMATH Open document ID: 0798.03046
DOI: 10.1016/0304-3975(93)90085-8
author: Robert Constable
author: Scott F. Smith
published in: Theoretical Computer Science
publication date: 1994-11-03T00:00:00Z
full work available at URL: https://hdl.handle.net/1813/6744
review text: The authors present a variant of indexing-free theory of computing, in which computations ``can be treated as objects and typed''. The family of base types consists of three types: the nonnegative integers, a one- element type unit and a two-element type Boolean. One of the generating rules is very strong: it is the fixed point rule. The axiomatic rules of the theory are constructive. The authors show parallels between recursive function theory over natural numbers and this new theory, particularly concerning unsolvability results. A variant of Rice's theorem is proved. A ``dovetailing constructor'' is defined to make possible parallel computing. The notions of reducibility, completeness, acceptability (a generalization of recursive enumerability) are introduced. The authors show that Markov's principle implies a generalization of Post's theorem concerning r.e. sets with r.e. complement. The theory is deeply connected with Nuprl [\textit{R. Constable} et al., Implementing, mathematics with the Nuprl proof development system, Prentice-Hall, Englewood Cliffs, NJ (1986)].
Mathematics Subject Classification ID: 03D75
Mathematics Subject Classification ID: 03F65
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 501165
zbMATH Keywords: constructive type theory
zbMATH Keywords: indexing-free theory of computing
zbMATH Keywords: fixed point rule
zbMATH Keywords: unsolvability
zbMATH Keywords: parallel computing
zbMATH Keywords: Nuprl
reviewed by: Hrant B. Marandjian
describes a project that uses: Nuprl
describes a project that uses: LCF
MaRDI profile type: Publication
OpenAlex ID: W2103838550
cites work: Q4100066
cites work: Q3805962
cites work: Q3703866
cites work: Q3855168
cites work: Q3880831
cites work: Q5625124
cites work: Edinburgh LCF. A mechanized logic of computation
cites work: Q4722037
cites work: Q5681533
cites work: Q5812175
cites work: Recursive Functionals and Quantifiers of Finite Types I
cites work: Q3679149
cites work: Constructive mathematics and computer programming
cites work: Q3734395
cites work: Domain interpretations of Martin-Löf's partial type theory
cites work: Shorter Notes: A Note on the Failure of the Relativized Enumeration Theorem in Recursive Function Theory
cites work: LCF considered as a programming language
cites work: Q5573961
cites work: A type-theoretical alternative to ISWIM, CUCH, OWHY
cites work: Data Types as Lattices
cites work: Q3819052
cites work: Algebraically Generalized Recursive Function Theory
cites work: Uniformly Reflexive Structures: On the Nature of Godelizations and Relative Computability
description: scientific article; zbMATH DE number 501165