×

Predicative recurrence in finite types. (English) Zbl 0947.03065

Nerode, A. (ed.) et al., LFCS ’94, Logical foundations of computer science. 3rd International Symposium, St. Petersburg, Russia, July 11-14, 1994. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 813, 227-239 (1994).
Summary: We consider the functionals defined using an extension to higher types of predicative recurrence, introduced in papers of the author [“Subrecursion and lambda representation over free algebras”, in: Feasible mathematics, Prog. Comput. Sci. Appl. Log. 9, 281-291 (1990; Zbl 0772.03020)], S. Bellantoni and S. Cook [Comput. Complexity 2, No. 2, 97-110 (1992; Zbl 0766.68037)] and the author [“Stratified functional programs and computational complexity”, in: Conference Record of the Twentieth Annual ACM Symposium on Principles of Programming Languages (ACM, New York) (1993)]. Three styles of predicative recurrence over a free algebra \({\mathbf A}\) are examined: equational recurrence, applicative programs with recurrence operators, and purely applicative higher-type programs. We show that, for every free algebra \({\mathbf A}\) and each one of these styles, the functions defined by predicative recurrence in finite types are precisely the functions over \({\mathbf A}\) that are computable in a number of steps elementary in the size of the input. This should be contrasted with unrestricted higher-type recurrence over \({\mathbf N}\), which yields all provably recursive functions of first-order arithmetic.
The same equivalences hold for natural notions of computing relative to a class of functions (as oracles). This shows that every class of functions closed under composition with elementary functions is closed under any higher-order functional defined by predictive recurrence. Among such functionals are natural generalizations or recurrence, such as recurrence with parameter substitution. This generalizes a result of H. Simmons [Arch. Math. Logic 27, No. 2, 177-188 (1988; Zbl 0659.03025)].
For the entire collection see [Zbl 0865.00034].

MSC:

03D65 Higher-type and set recursion theory