Lambda Calculus Characterizations of Poly-Time

Article type: Research Article

Authors: Leivant, Daniel | Marion, Jean-Yves

Affiliations: Department of Computer Science, Indiana University, Bloomington, IN 47405

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.

DOI: 10.3233/FI-1993-191-207

Journal: Fundamenta Informaticae, vol. 19, no. 1-2, pp. 167-184, 1993