An Application of Category-Theoretic Semantics to the Characterisation of Complexity Classes Using Higher-Order Function Algebras
Hofmann, Martin
Bull. Symbolic Logic, Tome 3 (1997) no. 1, p. 469-486 / Harvested from Project Euclid
We use the category of presheaves over PTIME-functions in order to show that Cook and Urquhart's higher-order function algebra $PV^{\omega}$ defines exactly the PTIME-functions. 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 $\sum_{1}^{b}$-induction over $PV^{\omega}$ 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.
Publié le : 1997-12-14
Classification: 
@article{1182353537,
     author = {Hofmann, Martin},
     title = {An Application of Category-Theoretic Semantics to the Characterisation of Complexity Classes Using Higher-Order Function Algebras},
     journal = {Bull. Symbolic Logic},
     volume = {3},
     number = {1},
     year = {1997},
     pages = { 469-486},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1182353537}
}
Hofmann, Martin. An Application of Category-Theoretic Semantics to the Characterisation of Complexity Classes Using Higher-Order Function Algebras. Bull. Symbolic Logic, Tome 3 (1997) no. 1, pp.  469-486. http://gdmltest.u-ga.fr/item/1182353537/