Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Reasonable Space for the $λ$-Calculus, Logarithmically

Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni

TL;DR

A new reasonable space cost model for the λ-calculus, based on a variant over the Krivine abstract machine, is presented, for the first time, able to accommodate logarithmic space.

Abstract

Can the $λ$-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 $λ$-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.

Reasonable Space for the $λ$-Calculus, Logarithmically

TL;DR

A new reasonable space cost model for the λ-calculus, based on a variant over the Krivine abstract machine, is presented, for the first time, able to accommodate logarithmic space.

Abstract

Can the -calculus be considered a reasonable computational model? Can we use it for measuring the time 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.
Paper Structure (88 sections, 31 theorems, 43 equations, 10 figures)

This paper contains 88 sections, 31 theorems, 43 equations, 10 figures.

Table of Contents

  1. Introduction
  2. Space and the $\lambda$-Calculus.
  3. Logarithmic Space and the $\lambda$-Calculus.
  4. Contribution
  5. Key Ingredients
  6. Looking Back
  7. A Wrong Positive Belief: the Geometry of Interaction
  8. A Wrong Negative Belief: The Space Cost of Environments
  9. Pointers, Abstract Machines, and Abstract Implementations
  10. Encoding of TMs and Call-by-Value
  11. Sub-Term Property
  12. Related Work: Safe for (Reasonable Logarithmic) Space
  13. Related Work
  14. The Theory of Reasonable Cost Models for the λ-Calculus, and How Our Result Fits in It
  15. Reasonable Cost Models
  16. ...and 73 more sections

Key Result

Theorem 7.1

The Outlined KAM implements Closed CbN, that is, there is a complete $\rightarrow_{wh}$-sequence $t \rightarrow_{wh}^{n} u$ if and only if there is a complete run $\rho: \mathsf{init}(t) \mathrm{\rightarrow_{NaKAM\xspace}}^{*} q$ such that $q\hbox{o}rigin=c]{-90}{$→$} = u$ and $|\rho|_{\beta} = n$.

Figures (10)

  • Figure 1: Data structures and transitions of the Outlined KAM.
  • Figure 2: Data structures and transitions of the Linked KAM.
  • Figure 3: Sub-Term KAM.
  • Figure 4: Naive KAM = Outlined KAM + Naive Abstract Implementation.
  • Figure 5: Transitions of the Collecting KAM, which is the abstract layer of the Space KAM.
  • ...and 5 more figures

Theorems & Definitions (58)

  • Definition 4.1: Tree addresses
  • Definition 4.2: Left address
  • Definition 5.1: Reasonable cost model for the $\lambda$-calculus
  • Definition 6.1: Abstract implementation
  • Definition 6.2: Space and time of runs
  • Theorem 7.1: Implementation
  • Lemma 8.1: Environment domain invariant
  • Definition 8.2: Space KAM
  • Definition 8.3: Closure space
  • Lemma 8.4
  • ...and 48 more