Complexity theory refines computability theory by characterizing classes of algorithmic problems that can be solved under some time or memory constraints. Such classes are for instance PTIME (problems solvable in a polynomial number of elementary steps with respect to the size of the input) or LOGSPACE (problems solvable with memory usage logarithmic in the size of the input).

From its inception in the 1960s, complexity theory has generally been studied through Turing or RAM machines. Indeed, while the λ-calculus is historically recognized as a model of computation, equivalent to Turing and other machines, its relevance for the study of complexity has long been unclear. Its central operation, β-reduction, seems at first sight too rich and complex to be considered as an appropriate, atomic unit of computation. Yet, starting in the 1990s it became progressively known that the natural complexity measures (number of β-reductions for time, size of terms for space) were actually ‘’reasonable’’ measures, defining the same complexity classes as the Turing standard.

In this talk I will address two of the problems that remain in a λ-calculus-based theory of algorithmic complexity.

• The simple notion of space complexity based on the size of terms cannot measure any sublinear space, meaning it is adequate for characterizing PSPACE but not LOGSPACE. I will propose a refined —but still simple and natural— definition of space complexity for the λ-calculus solving this issue.
• Many implementations of the λ-calculus are adequate either for time or for space, but not for both simultaneously. I will present an implementation model reconciling these two aspects.