Polynomial time operations in explicit mathematics

Publisher: Cambridge University Press

E-ISSN: 1943-5886|62|2|575-594

ISSN: 0022-4812

Source: The Journal of Symbolic Logic, Vol.62, Iss.2, 1997-06, pp. : 575-594

Disclaimer: Any content in publications that violate the sovereignty, the constitution or regulations of the PRC is not accepted or approved by CNPIEC.

Previous Menu Next

Abstract

In this paper we study (self-)applicative theories of operations and binary words in the context of polynomial time computability. We propose a first order theory PTO which allows full self-application and whose provably total functions on = {0, 1}* are exactly the polynomial time computable functions. Our treatment of PTO is proof-theoretic and very much in the spirit of reductive proof theory.