(Leeds)

This is an extension of work with G. Ostrin which I've spoken about before. If the induction variables are separated from the quantified variables in arithmetic, then the provably recursive functions become much more feasible. The $\Sigma_1$ inductive fragment corresponds to polynomial time (but of course in "unary" notation) and the next level of induction corresponds to exponential time. The whole theory only proves totality of elementary functions. Exponential time is particularly interesting because it includes good, informative examples (from the proof theoretic viewpoint). Factorial, suggested by H. Jervell, is a specially good one, and I'll use it to illustrate how our theory (closely related to earlier work of Leivant) ticks.Robert Recorde Room

Department of Computer Science