On the Elementary Affine Lambda-Calculus with and Without Fixed Points

Lê Thành Dũng Nguyen
(LIPN, Université Paris 13)

The elementary affine lambda-calculus was introduced as a polyvalent setting for implicit computational complexity, allowing for characterizations of polynomial time and hyperexponential time predicates. But these results rely on type fixpoints (a.k.a. recursive types), and it was unknown whether this feature of the type system was really necessary. We give a positive answer by showing that without type fixpoints, we get a characterization of regular languages instead of polynomial time. The proof uses the semantic evaluation method. We also propose an aesthetic improvement on the characterization of the function classes FP and k-FEXPTIME in the presence of recursive types.

In Thomas Seiller and Steffen Jost: Proceedings Third Joint Workshop on Developments in Implicit Computational complExity and Foundational & Practical Aspects of Resource Analysis (DICE-FOPARA 2019), Prague, Czech Republic, 6.4.2019 - 7.4.2019, Electronic Proceedings in Theoretical Computer Science 298, pp. 15–29.
Published: 14th August 2019.

ArXived at: https://dx.doi.org/10.4204/EPTCS.298.2 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org