Type Theoretic Constructions for Naming and Classifying Numeric Gadgets

Harold Simmons

(University of Manchester)

There is a standard hierarchy of sets numeric functions
E0, E2, E3,...Ealpha...
indexed by the ordinals. Ordinal 2 corresponds (roughly) to the polynomially bounded functions (sometimes called the feasible functions), 3 to the Kalmar elementary functions, omega to the primitive recursive functions, and epsilon0 to the functions that are handled by Peano arithmetic. Larger ordinals correspond to more sophisticated descriptions of arithmetic. I will show how all of these fit into a common framework of descriptions (specifications) of functions.

Gödel's T(erm calculus) lambdaG is an applied lambda-calculus for naming those numeric gadgets which occur before epsilon0. It includes many interesting subsystems. For instance, Primitive Recursive Arithmetic sits at the bottom of lambdaG. It can be seen how the complexity of a numeric gadget is directly related to the syntactic description in this system. We do not need any reference to a model of computation.

In recent years a technique known as tiering (or ramifying) has been applied to lambda-calculi. When this is done to lambdaG the overall strength drops from epsilon0 to 3, and thus we get a much finer classification of the Kalmar elementary functions. This tiering collapses Primitive Recursive Arithmetic down to level 2, and thus we get a much finer classification of the feasible functions. It is this result that has prompted the interest of some computer scientists.

I will describe some of the historical background to this topic, some of the more recent views of what is going on, and I will try to indicate what tiering is doing.
Tuesday 27th October 1998, 15:00
Seminar Room 322
Department of Computer Science