Lambda Calculus Characterizations of Poly-Time

Abstract

We consider typed λ-calculi with pairing over the algebra W of words over {0, 1}, with a destructor and discriminator function. We show that the poly-time functions are precisely the functions (1) λ-representable using simple types, with abstract input (represented by Church-like terms) and concrete output (represented by algebra terms); (2) λ-representable using simple types, with abstract input and output, but with the input and output representations differing slightly; (3) λ-representable using polymorphic typing with type quantification ranging over multiplicative types only; (4) λ-representable using simple and list types (akin to ML style) with abstract input and output; and (5) λ-representable over the algebra of flat lists (in place of W), using simple types, with abstract input and output.