## Martin Hofmann

Technische Hochschule Darmstadt

Cook and Urquhart's system *PV*_{omega} 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 *PV*_{omega}. 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
*PV*_{omega}.
We propose a new method for proving that the type 1 sections of
systems like *PV*_{omega} equals *PTIME* based on a
category-theoretic semantics. Roughly, our proof goes as follows. We
interpret the system in the functor category **Â=A**^{op}->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 *X*_{n} indexed
by *n* in *omega* and for each *PTIME*-function
*f*:**N**^{k}->**N**^{n} a
function
*X*_{f}:*X*_{n}*-*>X_{k} 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
*PV*_{omega} in this category by letting the base type
*o* be the representable presheaf given by *o*_{n}
= {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 *PV*_{omega}-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
*PV*_{omega} 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 *BC*_{omega} provides safe composition at all types and no
primitive functions other than those of *BC*.

A draft paper on this subject is available here.

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

Back to the list of talks