Ordinal bounds for programs

Stan Wainer

(University of Leeds)

This is joint work with H. Schwichtenberg (Munich), due to appear in the forth- coming volume "Feasible Mathematics II" edited by P.Clote and J.Remmel and published by Birkhauser. We use methods of Proof Theory and Subrecursive Hierarchies to assign ordinals to classes of terminating programs, the idea being that the ordinal assignment provides a uniform way of measuring complexity "in the large". We are not concerned with placing prior, e.g., polynomial, bounds on computation length, but with general methods of assessing complexity of natural classes of functional programs. The crucial idea is supplied by the Omega-+ rule of Buchholz which gives a method of describing computational uniformity in terms of uncountable "tree ordinals" which are then "collapsed" in a now-standard way to give sub-recursive bounds in terms of the Slow Growing Hierarchy. As an example the machinery is applied to a large class of higher order programs based on Plotkin's PCF but with "bounded fixed point operators" controlled by given well-orderings. If the given well-ordering is just N, the Howard ordinal arises as a natural upper bound.
Tuesday 1st March 1994, 14:30
Seminar Room 322
Department of Computer Science