Predicative recurrence in finite types

Abstract

We consider the functionals defined using an extension to higher types of predicative recurrence, introduced in [Lei90b, BC92, Lei93b]. Three styles of predicative recurrence over a free algebra A are examined: equational recurrence, applicative programs with recurrence operators, and purely applicative higher-type programs. We show that, for every free algebra A and each one of these styles, the functions defined by predicative recurrence in finite types are precisely the functions over 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 ℕ, which yields all provably recursive functions of first order arithmetic [Göd58]. The same equivalences holds 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 predicative recurrence. Among such functionals are natural generalizations of recurrence, such as recurrence with parameter substitution. This generalizes a result of [Sim88].