A Linguistic Characterization of Bounded Oracle Computation and Probabilistic Polynomial Time

We present a higher-order functional notation for polynomial-time computation with arbitrary 0; 1-valued oracle. This provides a linguistic characterization for classes such as np and bpp, as well as a notation for probabilistic polynomial-time functions. The language is derived from Hofmann's adaptation of Bellantoni-Cook safe recursion, extended to oracle computation via work derived from that of Kapron and Cook. Like Hofmann's language, ours is an applied version of typed lambda calculus with complexity bounds enforced by a type system. The type system uses a modal operator to distinguish between two types of numerical expressions, only one of which is allowed in recursion indices. The proof that the language captures precisely oracle polynomial time is model-theoretic, using adaptations of various techniques from category theory.

• Type: Conference
• Year: 1998
• Where: FOCS
• Authors: John C. Mitchell, Mark Mitchell, Andre Scedrov
• Keywords: FOCS 1998, Polynomial-time Computation, Probabilistic Polynomial-time Functions, Theoretical Computer Science, Type System