A category-theoretic proof that PVomega = PTIME

Cook and Urquhart's system PVomega is a simply-typed lambda calculus providing constants to denote natural numbers and an operator for bounded recursion on notation like in Cobham's characterisation of PTIME. Although arbitrary functionals can be defined in this system one can show that their presence does not increase the complexity of the definable type 1 functions: They remain PTIME. Cook and Urquhart prove this by appealing to the strong normalisation theorem and reading off a ``Cobham definition'' of a function from the normal form of a type 1 terms of PVomega. Although the idea is straightforward, the proof requires some messy details and it's not clear whether it can be generalised to other systems in the spirit of PVomega.

We propose a new method for proving that the type 1 sections of systems like PVomega equals PTIME based on a category-theoretic semantics. Roughly, our proof goes as follows. We interpret the system in the functor category Â=Aop->Sets; where A is the category which has as objects powers of N and (tuples of) PTIME functions as morphisms. An object X in Â consists of a family of sets Xn indexed by n in omega and for each PTIME-function f:Nk->Nn a function Xf:Xn->Xk such that the usual functor laws are valid. It is well-known that these ``variable sets'' form a model of the simply-typed lambda-calculus and in fact of intutionistic higher-order logic. We interpret PVomega in this category by letting the base type o be the representable presheaf given by on = {n-ary PTIME-functions}. The Yoneda lemma then tells us that the Â-morphisms from o to o are in bijective correspondence with the 1-place PTIME functions. Some work has to be done to interpret the recursor.

By this interpretation every PVomega-term t of type o->o gives rise to a PTIME-function. A category-theoretic trick called ``glueing'' or ``Freyd cover'' has to be applied in order show that this PTIME function coincides with the one denoted by t but then the desired property of PVomega comes out without any appeal to normalisation.

Preliminary investigation has shown that using a different category the same argument can be carried out for a higher-order version of Bellantoni's system BC which unlike his system BComega provides safe composition at all types and no primitive functions other than those of BC.

A draft paper on this subject is available here.

Martin Hofmann

Fachbereich Mathematik