BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TN-98-77
       ENTRY:: July 7, 1998
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: A Linguistic Characterization of Bounded Oracle Computation and 
Probabilistic Polynomial Time
        TYPE:: Technical Note 
      AUTHOR:: Mitchell, J.
      AUTHOR:: Mitchell, M.
      AUTHOR:: Scedrov, A.
        DATE:: May 4, 1998
       PAGES:: 12 
    ABSTRACT:: 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. 
       NOTES:: [Adminitrivia V1/Prg/19980612]
         END:: STAN//CS-TN-98-77