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
Technische Hochschule Darmstadt
Schlossgartenstrasse 7
64289 Darmstadt
Germany
Email:
mh@mathematik.th-darmstadt.de
Home page:
http://www.mathematik.th-darmstadt.de/ags/ag14/mitglieder/hofmann-e.html