AbstractWe use the category of presheaves over PTIME-functions in order to show that Cook and Urquhart's higher-order function algebra PVω defines exactly the PTIME-iunctions. As a byproduct we obtain a syntax-free generalisation of PTIME-computability to higher types.By restricting to sheaves for a suitable topology we obtain a model for intuitionistic predicate logic with -induction over PVω and use this to re-establish that the provably total functions in this system are polynomial time computable. Finally, we apply the category-theoretic approach to a new higher-order extension of Bellantoni-Cook's system BC of safe recursion.
Characterizing complexity classes by general recursive definitions in higher types
