Proof Theory and Complexity

Stan Wainer

(University of Leeds)

This talk will describe some joint work with my students G. Ostrin and N. Cagman, on the proof theory of low subrecursive classes. The basis is "A new recursion theoretic characterization of the polytime functions" by Bellantoni and Cook 1992, in which it is shown that a natural two-sorted re-interpretation of the usual primitive recursion schemes characterizes polynomially bounded computation. We show that if Peano Arithmetic is instead formulated in this two-sorted fashion, with quantification allowed only over one sort ("safe" variables) and induction allowed only over the other sort ("normal" variables), then the provably terminating computable functions are exactly the Kalmar elementary functions E(3). The provably terminating functions of the Sigma_1 Inductive fragment turn out to be exactly the Grzegorczyk E(2) functions, which are the same as the ones computable in Linear Space (on a Turing Machine working in binary). This work is related to other results of Buss, Bellantoni, Beckmann and Leivant, but in addition it clearly illustrates the use of classical ordinal analysis techniques at this low level. The difference is that the bounding functions are now the Slow Growing ones rather than the Fast Growing functions which bound computations in the usual single-sorted versions of Peano Arithmetic.
Thursday 18th February 1999, 15:00
Seminar Room 322
Department of Computer Science