Reasonable Space for the λ-Calculus, Logarithmically

2024/11/20 by Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni · 1 voice
Computer Science · #Advanced Database Systems and Queries #Computability, Logic, AI Algorithms #Parallel Computing and Optimization Techniques

paper · pdf · doi:10.46298/lmcs-20(4:15)2024

openalex publication_date 2024/11/20 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/03

Abstract

Can the λ-calculus be considered a reasonable computational model? Can we use it for measuring the time and space consumption of algorithms? While the literature contains positive answers about time, much less is known about space. This paper presents a new reasonable space cost model for the λ-calculus, based on a variant over the Krivine abstract machine. For the first time, this cost model is able to accommodate logarithmic space. Moreover, we study the time behavior of our machine and show how to transport our results to the call-by-value λ-calculus.

Discussions

• In the past few years there have been some developments on space complexity for the λ-calculus by Accattoli, Dal Lago and Vanoni: the Geometry of Interaction (mentioned in Damiano's answer) is actuall [stackexchange, 2 points]

Related

• Multi Types and Reasonable Space (Long Version)
• An Invariant Cost Model for the Lambda Calculus
• Reduction Strategies in the Lambda Calculus and Their Implementation through Derivable Abstract Machines: Introduction
• A Log-Sensitive Encoding of Turing Machines in the λ-Calculus
• Strong Call-by-Value is Reasonable, Implosively