Inlining as a Space Optimization: A Simple Time- and Space-Invariant Implementation of the Weak Lambda-Calculus
Abstract
We propose an implementation model for the evaluation of the weak λ -calculus, which is invariant for both time and space complexity, in both call-by-name and call-by-value strategies. In other words, this model provides an implementation of any weak call-by-name or weak call-by-value λ -calculus reduction sequence, whose time complexity is polynomial in the number of simulated β -steps, and whose space complexity is linear in the size of the largest intermediate term. This solves in an elegant way the well-known tension between time-invariance and space-invariance in the implementation of the λ -calculus.
Fields of Study & Subjects
Logic
programming
and type systems
Computability
AI Algorithms
semigroups and automata theory
Publication details
- Journal / source
- Proceedings of the ACM on Programming Languages
- Volume
- 10
- Issue
- ICFP
- Pages
- 950–978
- Publication date
- 17 August 2026
- Language
- EN