A linguistic characterization of bounded oracle computation and probabilistic polynomial time
- 27 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- Vol. 5 (02725428) , 725-733
- https://doi.org/10.1109/sfcs.1998.743523
Abstract
We present a higher-order functional notation for polynomial-time computation with an arbitrary 0, 1-valued oracle. This formulation 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 typed lambda calculus with complexity bounds enforced by a type system. The type system uses a modal operator to distinguish between two sorts of numerical expressions. Recursion can take place on only one of these sorts. The proof that the language captures precisely oracle polynomial time is model-theoretic, using adaptations of various techniques from category theory.Keywords
This publication has 10 references indexed in Scilit:
- Modal types as staging specifications for run-time code generationACM Computing Surveys, 1998
- A mixed modal/linear lambda calculus with applications to bellantoni-cook safe recursionPublished by Springer Nature ,1998
- A calculus for cryptographic protocolsPublished by Association for Computing Machinery (ACM) ,1997
- A new Characterization of Type-2 FeasibilitySIAM Journal on Computing, 1996
- A modal analysis of staged computationPublished by Association for Computing Machinery (ACM) ,1996
- Predicative Recursion and The Polytime HierarchyPublished by Springer Nature ,1995
- A new recursion-theoretic characterization of the polytime functionscomputational complexity, 1992
- Computability and Complexity of Higher Type FunctionsPublished by Springer Nature ,1992
- Notions of computation and monadsInformation and Computation, 1991
- Linear logicTheoretical Computer Science, 1987