Reasonable Space for the ${\lambda}$-Calculus, Logarithmically

TL;DR

This paper introduces a new space cost model for the λ-calculus capable of handling logarithmic space, based on a variant of the Krivine machine, and analyzes its time behavior and applicability to call-by-value evaluation.

Contribution

It proposes the first reasonable space cost model for λ-calculus that includes logarithmic space, extending the understanding of resource measurement in this computational model.

Findings

The model can accommodate logarithmic space complexity.

The time behavior of the machine is analyzed.

Results are applicable to call-by-value λ-calculus.

Abstract

Can the $\lambda$-calculus be considered a reasonable computational model? Can we use it for measuring the time $\textit{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 $\lambda$-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 $\lambda$-calculus.