Computational foundations of basic recursive function theory (Q1314348)

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)].