# Inlining as a space optimization: a simple time- and space-invariant implementation of the weak lambda-calculus

Thibaut Balabonski

► To cite this version:

Thibaut Balabonski. Inlining as a space optimization: a simple time- and space-invariant implementation of the weak lambda-calculus. 2026. hal-05524931

HAL Id: hal-05524931

https://hal.science/hal-05524931v1

Preprint submitted on 24 Feb 2026

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
# Inlining as a space optimization: a simple time- and space-invariant implementation of the weak lambda-calculus

THIBAUT BALABONSKI, Université Paris-Saclay, LMF, France

We propose an implementation model for the evaluation of the weak $\lambda$-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 $\lambda$-calculus reduction sequence, whose time complexity is polynomial in the number of simulated $\beta$-steps, and 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 $\lambda$-calculus.

CCS Concepts: • *Theory of computation* → *Lambda calculus*; *Complexity classes*.

Additional Key Words and Phrases: Lambda-calculus, Complexity, Time, Space, Weak reduction

## 1 Introduction

The $\lambda$-calculus is born as a model of computability in the 1930s [11], together with Turing machines and equivalent to them in terms of expressive power [22, 23]. These two models are deeply different, with complementary strengths: Turing machines focus on elementary operations on low-level representation of data, while the $\lambda$-calculus emphasizes higher-level and compositional computation mechanisms. Their difference is a strength of computability theory: it multiplies the available points of view and proof techniques.

However, when computability theory started being refined into complexity theory in the 1960s/1970s, the $\lambda$-calculus disappeared from the picture. Foundational papers [12, 15] as well as reference textbooks [7, 16, 19] mostly use Turing or RAM machines, and derivatives thereof. In a sense, increased preciseness came at the cost of a narrower range of available tools.

### 1.1 Invariance

An important contribution of complexity theory is the characterization of classes of algorithmic problems, that can be solved with constrained time or memory resources, like PTIME (problems solvable in a polynomial number of elementary steps with respect to the size of the input) or LOGSPACE (problems solvable with memory space logarithmic in the size of the input). A key that makes these classes robust and theoretically meaningful is Slot and van Emde Boas' notion of *reasonable* computation models [21], described as “machines that can simulate each other within a polynomially-bounded overhead in time and a constant-factor overhead in space”. This reasonability criterion, also called *invariance*, is what ensures that complexity classes are universal, and not tied to a particular computational device. So if we want to reintroduce the $\lambda$-calculus in the picture, make it an appropriate tool for expressing complexity classes, and allow complexity theory to benefit from its specific properties and techniques, an essential step is to connect the $\lambda$-calculus with this reasonability criterion.

*Is the $\lambda$-calculus a reasonable model?* There are straightforward ways of expressing the complexity of a computation in the $\lambda$-calculus. First, $\beta$-reduction defines a notion of computation step which makes a natural unit of time. Second, the size of a $\lambda$-term gives a convenient basis for expressing space, dubbed “ink space” by reference to the quantity of ink used for writing down a term. The question is whether these natural measures of space and time, or variants thereof, can be related to known reasonable measures like Turing complexity.

Author's Contact Information: Thibaut Balabonski, Université Paris-Saclay, LMF, 91190, Gif-sur-Yvette, France, thibaut.balabonski@lmf.cnrs.fr.
This is not straightforward [14] and might even be seen as counter-intuitive, as $\beta$-reduction is a non-atomic computation operation expressed using a subtle capture-avoiding term substitution operation. Can it really be an appropriate “unit”? Or do we need an implementation model before saying anything about complexity?

Yet the model is now known to be reasonable. First positive results about the adequacy of the natural cost measures for the $\lambda$-calculus came in the 1990s, for time [10] as well as ink space [18], and have been recently improved. Concerning time, the number of $\beta$-reductions has first been proved to be an adequate time complexity measure in the context of weak reduction strategies: strategies that never reduce inside $\lambda$-abstractions, and correspond to usual programming language semantics [10, 17, 20]. This has been extended in the 2010s to strong strategies allowing full normalization [4]. Concerning space, the ink space model is simple but intrinsically unable to measure any sublinear space complexity. This has been improved very recently with two different ways of measuring sublinear space, down to LOGSPACE [5, 8].

*An apparent tension between time-invariance and space-invariance.* Despite the above invariance results for a natural time measure (the number of $\beta$-steps) and for a natural space measure (ink space), some disturbing facts remain. In particular, there are simple examples of computations in the $\lambda$-calculus that build a term of exponential size in a linear number of steps [1], which is utterly impossible in a Turing-like model and suggest a tension between time-reasonability and space-reasonability in the $\lambda$-calculus.

Here is one such example. Write $c_n$ for the Church encoding of the natural number $n$, defined as $c_n = \lambda x.f(f(f...(f x)...))$ with $n$ nested applications of $f$. Define $\text{Id} = \lambda z.z$ the identity function. Then the term $c_n c_2 \text{Id}$ reduces in $\Theta(n)$ call-by-value steps to a term of size $\Omega(2^n)$.

This well-known *size-explosion* problem comes from the fact that substitution can duplicate in one step a term of any size. It also tells us that implementing such a reduction sequence by actually performing the substitutions would require an exponential time. A simple solution to this problem consists in not doing the substitutions, and instead switching to a shared presentation of terms, using an explicit heap and pointers to the elements stored in the heap. However, this sharing comes with a non-negligible cost: the pointers themselves have a cost, which may grow with the number of elements stored in the heap and finally outweigh the benefits of sharing.

Here is one such example, adapted from [13], in which the phenomenon is called *pointer explosion*. Define $e = (\lambda xy.xx) \text{Id}$, and $p_n = e(e...(e \text{Id})...))$ with $n$ nested applications of $e$. Then we have the following call-by-value reduction sequence: $p_n \rightarrow_{\beta}^{n} (\lambda y.\text{Id} \ \text{Id})...( (\lambda y.\text{Id} \ \text{Id}) \ \text{Id})... ) \rightarrow_{\beta}^{2n} \text{Id}$, in which the biggest intermediate term has a size $\Theta(n)$. However, if this reduction is implemented with sharing, by the $n$th step we have $n$ independent entries in the heap (one created by each step), which means that pointers must have at least $\log(n)$ bits for correctly identifying each used location of the heap, thus giving a space cost $\Omega(n \times \log(n))$.

The puzzling problem of having a single implementation model reasonable for both space and time has been solved for the first time in 2020 for the weak call-by-value $\lambda$-calculus [13]. The idea in this first solution consisted in interleaving two distinct machines: a substitution-based machine which is reasonable for space but may suffer from size explosion, and a heap-based machine which is reasonable for time but may suffer from pointer explosion. The interleaving strategy then consists in repeatedly executing one of the machines for increasing numbers of steps, possibly aborting and switching to the other machine depending on the observed sizes of terms.

While this interleaving strategy technically solves the problem, it is a quite frustrating solution. In a sense, it can be seen as a dynamic choice between two partial solutions, and thus falls short of proposing a simple way of understanding how time-invariance and space-invariance may cohabit.
*Research question: is there a simple implementation model of the λ-calculus that is both time- and space-invariant for the natural complexity measures?*

## 1.2 Contribution

In this paper we propose an implementation model for the weak λ-calculus, which is time- and space-invariant under both call-by-name and call-by-value evaluation strategies. The model is simple, and based on a single principle: it is generally desirable to avoid substitution and use pointers instead, except when the substituted term is smaller than a pointer.

*Advantages of our solutions.* Our model thus chooses for each β-reduction step whether to substitute the argument or store it in a heap, depending on how the size of the argument compares to the size of the available pointers. Contrarily to what happens in the interleaving strategy of [13], this choice is greedy: the decision is made based on a local criterion, and we never backtrack.

Our simple and principled approach also brings some byproducts. First, rather than a specific machine, we describe first a core implementation model which contains the main ideas but is not tied to a specific evaluation strategy. This central model is then instantiated on both call-by-name and call-by-value and provides invariance results for both strategies. Second, the machine is simple enough to be combined in a readable way with the log-sensitive space-cost measure proposed in [8], enlarging the set of captured complexity classes.

*Challenges.* The main idea of our implementation model (do not use the heap to store a term that costs less than a pointer) is simple. The main difficulty of this work is in analyzing the invariance properties that this simple idea offers.

Space invariance is relatively simple, since the space cost in our machine is always bounded by the space cost of the represented terms, up to a constant factor.

Time invariance however is far more subtle. In particular, time-invariance results often critically rely on a subterm property [4] ensuring that terms duplicated in a reduction sequence $t_0 \to \beta t_1 \to \beta \dots$ are always subterms of the initial term $t_0$. This implies that the size of duplicated terms is bounded by the size of the initial term, and globally this allows controlling the growth of the terms along a reduction sequence. In our model, this subterm property does not hold: initial subterms will possibly grow before being substituted and duplicated and we will need new, finer invariants to control the growth of the configurations of our machine.

*Outline.* In Section 2 we recall basic definitions of the λ-calculus and introduce tools such as positions and the descendance relation, which will be useful in the analysis of our model. We then define a general model of graph reduction for the λ-calculus in Section 3, that provides the framework in which we define our abstract machine in Section 4. Time- and space-invariance of our model is proved in Section 5, and we finally discuss alternatives, extensions, and relation to some existing machines in Section 6.

## 2 The weak lambda-calculus

We take the usual definition of the λ-calculus [9], with terms defined by this grammar.

$$t ::= x \mid t t \mid \lambda x.t$$

Terms are considered modulo α-renaming of bound variables. We write $fv(t)$ for the set of free variables of the term $t$. A term is closed if it has no free variable. The only computation rule is β-reduction.

$$(\lambda x.t) u \to \beta \quad t^{\{x \leftarrow u\}}$$
It is based on a capture-avoiding substitution operation $t^{\{x \leftarrow u\}}$ that replaces every free occurrence of $x$ in $t$ by $u$. In weak reduction, this reduction rule can be applied anywhere except in the body $t$ of a $\lambda$-abstraction $\lambda x.t$. We write $t \to_w t'$ when the term $t$ reduces to the term $t'$ in one weak step, and $t \to_w^* t'$ (resp. $t \to^n_w t'$) when $t$ reduces to $t'$ by a possibly empty sequence of successive weak steps (resp. a sequence of $n$ steps).

## 2.1 Metrics

A $\lambda$-term has a syntax tree which is the basis of some simple metrics on the terms.

**DEFINITION 2.1 (SIZE AND HEIGHT).** The size $|t|$ of a $\lambda$-term $t$ is the number of nodes in its syntax tree. Its height $\text{ht}(t)$ is the height of that tree.

$$ 
\begin{array}{lclcl}
|x| & = & 1 & \text{ht}(x) & = & 1 \\
|t u| & = & 1 + |t| + |u| & \text{ht}(t u) & = & 1 + \max(\text{ht}(t), \text{ht}(u)) \\
|\lambda x.t| & = & 1 + |t| & \text{ht}(\lambda x.t) & = & 1 + \text{ht}(t)
\end{array}
$$

The space cost of a term gives is a more precise version of its size, which takes into account the actual cost of representing variables. In the definition below we propose to fix a constant $c_v$, describing the number of bits required for distinguishing the variables of the considered term, and to assign this space cost to each variable occurrence.

**DEFINITION 2.2 (SPACE COST).** Let $t$ be a term, and $d$ the maximal number of binders between a variable occurrence and its binder in $t$ (equivalently, $d$ would be the maximal index in the de Bruijn notation for $t$). Let $c_v$ be the number of bits required for representing $d$. Then the space cost $\|t\|_{c_v}$ of $t$ is defined as follows.

$$ 
\begin{align*}
\|x\|_{c_v} &= c_v \\
\|t u\|_{c_v} &= 1 + \|t\|_{c_v} + \|u\|_{c_v} \\
\|\lambda x.t\|_{c_v} &= 1 + \|t\|_{c_v}
\end{align*}
$$

A critical aspect of working on weak reduction is that the variable cost $c_v$ remains valid along any reduction sequence starting from the term $t$ with respect to which $c_v$ has been defined. Note that, everywhere in this paper, we could remove this constant $c_v$ and count as space cost of a variable occurrence the size of its de Bruijn index. We keep this uniform cost $c_v$ since we do not think using explicit de Bruijn indices improve the clarity of the development.

## 2.2 Positions and contexts

We formally characterize each subterm $s$ in a term $t$ by its *position* in the syntax tree of $t$, described as a sequence of directions from the root of the term.

**DEFINITION 2.3 (SEQUENCES).** Let $\Sigma$ be a set of symbols. A sequence is an ordered list $S = c_0; c_1; \dots; c_{n-1}$ of elements of $\Sigma$, its length $|S| = n$ is the number of elements. We write $';'$ for the associative operator concatenating symbols and sequences of symbols. Its neutral element (the empty sequence) is written $\varepsilon$. A sequence $S_1$ is a prefix of a sequence $S_2$ if $S_2$ can be written as $S_1; S_3$, with $S_3$ possibly empty. We write $\Sigma^*$ for the set of all sequences, and $\Sigma^n$ for the set of sequences of length $n$.

Remark that for any $c \in \Sigma$, the notation $c$ can denote either the element itself, or a sequence of one element. The context usually makes clear which one is meant. In some contexts, $\Sigma$ is also called alphabet, symbols $c \in \Sigma$ are called characters, and sequences are called strings.
**DEFINITION 2.4 (POSITIONS OF A TERM).** A position is a sequence on the set $\{0, 1, 2\}$, that describes a path in the syntax tree of a $\lambda$-term. The set $\mathcal{P}(t)$ of the positions of a $\lambda$-term $t$ is defined as follows:

$$ 
\begin{align*}
\mathcal{P}(x) &= \{\epsilon\} \\
\mathcal{P}(\lambda x.t) &= \{\epsilon\} \cup \{0; p \mid p \in \mathcal{P}(t)\} \\
\mathcal{P}(t u) &= \{\epsilon\} \cup \{1; p \mid p \in \mathcal{P}(t)\} \cup \{2; p \mid p \in \mathcal{P}(u)\}
\end{align*}
$$

The position of a reduction step is the position of the reduced redex. A weak position is a position that does not contain 0. Two positions are disjoint if neither is a prefix of the other.

**DEFINITION 2.5 (SUBTERM AT POSITION p).** Assuming $p \in \mathcal{P}(t)$, the subterm at position $p$ in $t$, written $t|_p$, is defined as follows.

$$ 
\begin{align*}
t|_{\epsilon} &= t \\
(\lambda x.t)|_{0;p} &= t|_{p} \\
(t u)|_{1;p} &= t|_{p} \\
(t u)|_{2;p} &= u|_{p}
\end{align*}
$$

*Example 2.6 (Positions/subterms).* Let $t = (\lambda xy.x(xy)) (\lambda z.z)$. The then set of positions of $t$ is $\mathcal{P}(t) = \{\epsilon, 1, 10, 100, 1001, 1002, 10021, 10022, 2, 20\}$, and we have $t|_2 = \lambda z.z$ and $t|_{10} = \lambda y.x(xy)$.

A context describes the part of a term $t$ which is the complement of a subterm $t|_p$.

**DEFINITION 2.7 (CONTEXT).** A context $C$ is a term with one occurrence of a special symbol $\square$ called hole, defined by the following grammar.

$$ C ::= \square | C t | t C | \lambda x.C $$

Given a context $C$ and a term $t$, we write $C[t]$ for the term obtained by replacing the unique hole of $C$ by $t$. This operation is not capture-avoiding.

The positions $\mathcal{P}(C)$ of a context $C$ are the positions of each of its elements except the hole. We write $\mathcal{H}(C)$ for the position of the unique hole of the context $C$.

$$ 
\begin{align*}
\mathcal{P}(\Box) &= \emptyset & \mathcal{H}(\Box) &= \epsilon \\
\mathcal{P}(C t) &= \{\epsilon\} \cup \{1; p \mid p \in \mathcal{P}(C)\} \cup \{2; p \mid p \in \mathcal{P}(t)\} & \mathcal{H}(C t) &= 1; \mathcal{H}(C) \\
\mathcal{P}(t C) &= \{\epsilon\} \cup \{1; p \mid p \in \mathcal{P}(t)\} \cup \{2; p \mid p \in \mathcal{P}(C)\} & \mathcal{H}(t C) &= 2; \mathcal{H}(C) \\
\mathcal{P}(\lambda x.C) &= \{\epsilon\} \cup \{0; p \mid p \in \mathcal{P}(C)\} & \mathcal{H}(\lambda x.C) &= 0; \mathcal{H}(C)
\end{align*}
$$

A context $C$ is weak if its hole is not inside a $\lambda$-abstraction, that is if $\emptyset$ does not appear in $\mathcal{H}(C)$. A $\beta$-reduction at position $p$ is a reduction $C[(\lambda x.u) s] \to_{\beta} C[u^{x \leftrightarrow s}]$ with $\mathcal{H}(C) = p$.

## 2.3 Descendance relation and shape preservation

Each reduction step $t \to_{\beta} t'$ builds a new term $t'$ using parts of the source term $t$. These parts can be tracked by a *descendance relation*.

**DEFINITION 2.8 (DESCENDANTS).** Let $\rho: t = C[(\lambda x.u) s] \to_w C[u^{x \leftrightarrow s}] = t'$, be a weak $\beta$-reduction step at position $p$ in $t$. Let $q \in \mathcal{P}(t)$ be a position in $t$. The set $q/\rho$ of the descendants of $q$ after $\rho$ is the set of positions of $t'$ defined as follows.

* If $q \in \mathcal{P}(C)$, then $q/\rho = \{q\}$.

* If $q = p; 10; q'$ and $u|_{q'} \neq x$, then $q/\rho = \{p; q'\}$.

* If $q = P; 2; q'$, then $q/\rho = \{p; p_x; q' \mid u|_{p_x} = x\}$.

* Otherwise, $q/\rho = \emptyset$.
In the second and third points, using usual hygienic conditions on variable names [9] we assume $x$ denotes an occurrence of the variable bound by the $\lambda$-abstraction of the redex. The position $q$ is called ancestor of the positions in $q/\rho$. The notion of descendance extends transitively to sequences of reduction, and reflexively for the empty sequence.

**Example 2.9 (Descendance).** Consider the reduction step

$$t = (\lambda xy.x(xy))(\lambda z.z)(\lambda z.z) \rightarrow \beta \quad (\lambda y.(\lambda z.z)((\lambda z.z)y))(\lambda z.z) = t'$$

The positions $\varepsilon$ and 2 of $t'$ respectively descend from the positions $\varepsilon$ and 2 of $t$. The position 12 of $t$ has two descendants 101 and 1021 in $t'$. The positions 1 and 11 of $t$ have no descendant in $t'$.

There are some degrees of freedom when defining descendants. We could in particular define that the position of a reduced redex has itself as descendant, meaning the reduct descends from the redex, or similarly for substituted variables. The stricter version defined here, in which these positions have no descendants, offers the nice invariant that any subterm and its descendants have the same superficial shape.

**DEFINITION 2.10 (SHAPE).** The shape of a $\lambda$-term is a symbol in the set $\{\mathcal{X}, @, \Lambda\}$, representing its main constructor.

$$\text{shape}(x) = \mathcal{X}$$

$$\text{shape}(t u) = @$$

$$\text{shape}(\lambda x.t) = \Lambda$$

**LEMMA 2.11 (SHAPE PRESERVATION).** Let $\rho : t \rightarrow_w t'$ be a reduction step, and $p \in \mathcal{P}(t)$, $p' \in \mathcal{P}(t')$ two positions such that $p' \in p/\rho$. Then

$$\text{shape}(t|_p) = \text{shape}(t'|_{p'})$$

# 3 A framework for graph reduction

We define here a framework of *graph of terms*, describing $\lambda$-calculus reduction in a graph form, which allows reasoning on shared subterms. This framework is the base in which we develop our abstract machine in the next section.

## 3.1 Syntax

A graph of terms is formalized as a main term $t$ together with an acyclic heap $H$ containing closed terms. The usual syntax of $\lambda$-terms is extended with a notation $\underline{a}$, where $a \in \mathbb{N}$ is an *address*: a natural number denoting a location in the heap.

**DEFINITION 3.1 (GRAPH OF TERMS).** Terms are defined by the following grammar. A heap is a finite mapping from addresses (natural numbers) to terms. A graph of terms is a pair of a term and a heap.

$$\begin{array}{l@{\hspace{2em}}l@{\hspace{2em}}l}
t & ::= & x \mid t \mid \lambda x.t \mid \underline{a} & \text{terms} \\
H & ::= & \{a_1 \mapsto t_1, \dots, a_n \mapsto t_n\} & \text{heaps} \\
G & ::= & \langle t \mid H \rangle & \text{graphs}
\end{array}$$

In any graph of terms $\langle t \mid H \rangle$, it is assumed that no address is defined twice in the heap $H$, and that both the main term $t$ and the terms in $H$ are closed. If the heap $H$ contains a mapping $a \mapsto t$, then we write $H(a) = t$, and $H \setminus a$ the heap obtained by removing this mapping from $H$. The domain of a heap $H = \{a_1 \mapsto t_1, \dots, a_n \mapsto t_n\}$ is the set $\text{dom}(H) = \{a_1, \dots, a_n\}$ of addresses it defines. We write $\text{next}(H) = \min(\mathbb{N} \setminus \text{dom}(H))$ the smallest address not defined by $H$.

Alternatively we could define a graph of terms as a single heap, in which a predefined address (for instance $\emptyset$) contains the main term. We keep the main term apart here to emphasize its particular role: it will have different rules and different invariants.
The notions of free variables and of substitution are naturally extended to the terms with addresses.

**DEFINITION 3.2 (FREE VARIABLES, CLOSED TERMS, SUBSTITUTION).**

$$
\begin{align*}
fv(x) &= \{x\} & y^{\{x \leftarrow s\}} &= \begin{cases} s & y = x \\ y & y \neq x \end{cases} \\
fv(t \ u) &= fv(t) \cup fv(u) & (t \ u)^{\{x \leftarrow s\}} &= t^{\{x \leftarrow s\}} u^{\{x \leftarrow s\}} \\
fv(\lambda x.t) &= fv(t) \setminus \{x\} & (\lambda y.t)^{\{x \leftarrow s\}} &= \lambda y.t^{\{x \leftarrow s\}} \quad y \neq x, y \notin fv(s) \\
fv(\underline{a}) &= \emptyset & \underline{a}^{\{x \leftarrow s\}} &= \underline{a}
\end{align*}
$$

A term $t$ is closed if $fv(t) = \emptyset$. A heap $H$ is closed if for every $a \mapsto t \in H$ we have $t$ closed.

A graph of terms is valid if any address used is defined exactly once in the heap, and the underlying graph is acyclic. These are formalized with the definitions below.

**DEFINITION 3.3 (ADDRESSES).** The addresses used in a term, a heap, and a graph of terms are defined by the following equations.

$$
\begin{align*}
\operatorname{addr}(x) &= \emptyset & \operatorname{addr}(H) &= \bigcup_{a \mapsto t \in H} \operatorname{addr}(t) \\
\operatorname{addr}(t \ u) &= \operatorname{addr}(t) \cup \operatorname{addr}(u) & & \\
\operatorname{addr}(\lambda x.t) &= \operatorname{addr}(t) & & \\
\operatorname{addr}(\underline{a}) &= \{a\} & \operatorname{addr}(\langle t \mid H \rangle) &= \operatorname{addr}(t) \cup \operatorname{addr}(H)
\end{align*}
$$

A term $t$ is pure if $addr(t) = \emptyset$.

**DEFINITION 3.4 (UNDERLYING GRAPH, ACYCLOSITY).** The underlying graph graph($\langle t | H \rangle$) of a graph of terms $\langle t | H \rangle = \langle t | \{a_1 \mapsto t_1, \dots, a_n \mapsto t_n\} \rangle$ is the directed graph defined as follows:

* its vertices are the addresses $\{a_1, \dots, a_n\}$ in the domain of $H$, plus a special vertex $r$ called root,

* there is a directed edge $a \to a'$ from source $a$ to target $a'$ if $a' \in addr(H(a))$, and there is an edge $r \to a$ when $a \in addr(t)$.

A graph of terms $\langle t | H \rangle$ is acyclic if the underlying graph graph($H$) is acyclic.

**DEFINITION 3.5 (VALID GRAPH OF TERMS).** A graph of terms $\langle t | H \rangle$ is valid if:

* no address is defined twice in $H$: if $a \mapsto t \in H$ and $a' \mapsto t' \in H$ then $t = t'$;

* any address used is defined: $addr(\langle t | H \rangle) \subseteq \operatorname{dom}(H)$;

* it is acyclic;

* the main term $t$ is closed, and any term $H(a)$ in the heap is closed.

**DEFINITION 3.6 (INITIAL CONFIGURATION, FINAL CONFIGURATION).** An initial configuration is $\langle t | \emptyset \rangle$ with $t$ a pure term. A final configuration is $\langle \lambda x.t | H \rangle$ such that $\operatorname{dom}(H) = \operatorname{addr}(\langle \lambda x.t | H \rangle)$.

A valid graph of terms represents a $\lambda$-term, that is obtained by inlining all mappings of the heap in the main term.

**DEFINITION 3.7 (UNFOLDING).** Let $\langle t | H \rangle$ be a valid graph of terms. Its unfolding $t^H$ is the closed term obtained by repeatedly substituting all elements stored in the heap for their respective addresses.

$$
\begin{align*}
x^H &= x \\
(t \ u)^H &= t^H u^H \\
(\lambda x.t)^H &= \lambda x.t^H \\
\underline{a}^H &= (H(a))^H
\end{align*}
$$
*Example 3.8 (Graph of terms and unfolding).* Consider the graph of terms

$$G = \langle (\lambda x.\underline{1}x\underline{0}) (\lambda z.\underline{1}) | 0 \mapsto \lambda w.w, 1 \mapsto \lambda y.y\underline{0} \rangle$$

Its unfolding is the term

$$t_G = (\lambda x.(\lambda y.(\lambda w.w))x(\lambda w.w)) (\lambda z.y.(\lambda w.w))$$

The notion of position naturally extends to terms with addresses.

**DEFINITION 3.9 (POSITIONS OF A TERM).** A term position is a sequence on the set $\{0, 1, 2\}$, that describes a path in the syntax tree of a $\lambda$-term. The set $\mathcal{P}(t)$ of the positions of a $\lambda$-term $t$ is defined as follows:

$$\begin{align*}
\mathcal{P}(x) &= \{\epsilon\} \\
\mathcal{P}(\lambda x.t) &= \{\epsilon\} \cup \{0; p \mid p \in \mathcal{P}(t)\} \\
\mathcal{P}(t u) &= \{\epsilon\} \cup \{1; p \mid p \in \mathcal{P}(t)\} \cup \{2; p \mid p \in \mathcal{P}(u)\} \\
\mathcal{P}(\underline{a}) &= \{\epsilon\}
\end{align*}$$

The positions of a graph of terms comprise the positions of the main term, as well as the positions of each term in the heap, the latter begin prefixed by the address of the term. Each syntactic element has exactly one position.

**DEFINITION 3.10 (POSITIONS OF A GRAPH OF TERMS).** A graph position is a sequence on the set $\{0, 1, 2, 3\} \cup \mathbb{N}$, that describes a path in the representation of a graph of terms. The set $\mathcal{P}(\langle t | H \rangle)$ of the positions of a graph of terms $\langle t | H \rangle$ is defined as follows:

$$\mathcal{P}(\langle t | H \rangle) = \mathcal{P}(t) \cup \{3; a; p \mid a \in \text{dom}(H), p \in \mathcal{P}(H(a))\}$$

In this extended definition, we include the heap addresses as elements of the alphabet. The symbol 3 distinguishes positions of elements stored in the heap, and indicates that the next symbol is interpreted as an address. At any other place, the symbols 0, 1 and 2 from term positions are interpreted as usual. We could also assume these three symbols are distinct from the integers possibly used as addresses. Then a position would start with an address $a$ for an element of the heap, and with nothing or a special symbol $a_0$ for the main term. It would also be possible to keep a finite alphabet by replacing $a$ in 3; $a$ by its binary representation, but this does not help in any way the coming development.

**DEFINITION 3.11 (SUBTERM AT POSITION $p$ IN A GRAPH OF TERMS).** Assuming $p \in \mathcal{P}(\langle t | H \rangle)$, the subterm at position $p$ in $\langle t | H \rangle$, written $\langle t | H \rangle|_p$, is defined as follows.

$$\begin{align*}
\langle t | H \rangle|_{3;a:p} &= H(a)|_p \\
\langle t | H \rangle|_p &= t|_p \quad \text{otherwise}
\end{align*}$$

Assuming a constant $c_v$ representing the cost of representing a variable occurrence, the cost $\|t\|_{c_v}$ of a term is defined as follows. The notion extends to heaps and graphs of terms. Typically, $c_v$ can be defined as the logarithm of an upper bound of the indices in the de Bruijn notation, or of the number of distinct variable names. Thanks to our restriction to closed reduction, any such upper bound chosen on an initial term remains valid along reduction.

$$\begin{align*}
\|x\|_{c_v} &= c_v & \|H\|_{c_v} &= \sum_{a \to t \in H} \|\underline{a}\|_{c_v} + \|t\|_{c_v} \\
\|t u\|_{c_v} &= 1 + \|t\|_{c_v} + \|u\|_{c_v} & & \\
\|\lambda x.t\|_{c_v} &= 1 + \|t\|_{c_v} & & \\
\|\underline{a}\|_{c_v} &= \min(1, \lceil \log(a) \rceil) & & \|\langle t | H \rangle\|_{c_v} &= \|t\|_{c_v} + \|H\|_{c_v}
\end{align*}$$

The space cost measure extends the one of the $\lambda$-calculus. The space cost of a pointer $\underline{a}$ is the size of its binary representation. Each entry in the heap adds both the cost of its term and the cost of its address to the total.
## 3.2 Closed reduction

The reduction semantics of graphs of terms describes the elementary computation rules that can be applied on a valid graph of terms $\langle t | H \rangle$. It is defined by four rules, which mostly focus on the main term $t$.

The two main rules, $\rightarrow_{f\beta}$ and $\rightarrow_{s\beta}$, both implement $\beta$-reduction, each in a different way: full $\beta$ rule $\rightarrow_{f\beta}$ is the usual $\beta$-reduction substituting the argument in the body of the function, while sharing $\beta$ rule $\rightarrow_{s\beta}$ is a sharing variant which stores the argument at a new location in the heap (thus creating a new node in the graph of terms) and only substitutes a pointer in the body of the function. In both cases we require the argument to be closed, which allows the configuration to remain valid and also ensures that no $\alpha$-renaming is required. As a consequence of the latter, a constant $c_v$ bounding the numbers of bits required to represent a variable in a term or a graph of terms remains valid along reduction.

The two other rules manage the heap: a linear substitution rule $\rightarrow_{ls}$ replaces one occurrence of a pointer in the main term by the corresponding term stored in the heap, and a garbage collection rule $\rightarrow_{gc}$ removes an unused mapping from the heap.

**DEFINITION 3.12 (REDUCTION RULES).** The reduction relation $\langle t | H \rangle \rightarrow \langle t' | H' \rangle$ on graphs of terms is defined by the union of the four cases below.

$$
\begin{align*}
\langle C[(\lambda x.t) u] | H \rangle & \rightarrow_{f\beta} \langle C[t^{\{x \leftarrow u\}}] | H \rangle & u \text{ closed} \\
\langle C[(\lambda x.t) u] | H \rangle & \rightarrow_{s\beta} \langle C[t^{\{x \leftarrow a\}}] | H, a \mapsto u \rangle & u \text{ closed, } a \notin \text{addr}(\langle C[(\lambda x.t) u] | H \rangle) \\
\langle C[a] | H \rangle & \rightarrow_{ls} \langle C[H(a)] | H \rangle \\
\langle t | H \rangle & \rightarrow_{gc} \langle t | H \setminus \{a\} \rangle & a \in \text{dom}(H) \setminus \text{addr}(\langle t | H \rangle)
\end{align*}
$$

The position of a reduction step is $\mathcal{H}(C)$ in the first three cases, and 3; a in the last case.

**Example 3.13 (Graph reduction).** The graph of terms $G$ from example 3.8 can be further reduced as follows.

$$
\begin{align*}
& \langle (\lambda x.\underline{1}x0) (\lambda z.\underline{1}) | 0 \mapsto \lambda w.w, 1 \mapsto \lambda y.y0 \rangle \\
\rightarrow_{s\beta} & \langle \underline{1} \underline{2} \underline{0} | 0 \mapsto \lambda w.w, 1 \mapsto \lambda y.y0, 2 \mapsto \lambda z.\underline{1} \rangle \\
\rightarrow_{ls} & \langle (\lambda y.y0) \underline{2} \underline{0} | 0 \mapsto \lambda w.w, 1 \mapsto \lambda y.y0, 2 \mapsto \lambda z.\underline{1} \rangle \\
\rightarrow_{f\beta} & \langle \underline{2} \underline{0} \underline{0} | 0 \mapsto \lambda w.w, 1 \mapsto \lambda y.y0, 2 \mapsto \lambda z.\underline{1} \rangle \\
\rightarrow_{ls} & \langle (\lambda z.\underline{1}) \underline{0} \underline{0} | 0 \mapsto \lambda w.w, 1 \mapsto \lambda y.y0, 2 \mapsto \lambda z.\underline{1} \rangle \\
\rightarrow_{gc} & \langle (\lambda z.\underline{1}) \underline{0} \underline{0} | 0 \mapsto \lambda w.w, 1 \mapsto \lambda y.y0 \rangle \\
\rightarrow & \dots
\end{align*}
$$

Remark that full $\beta$-reduction $\rightarrow_{f\beta}$ can be simulated by a combination of sharing $\beta$-reduction $\rightarrow_{s\beta}$ and heap management. This implies in particular that the choice of reducing a $\beta$-redex using $\rightarrow_{f\beta}$ or $\rightarrow_{s\beta}$ is only a matter of how much sharing is used in the computation or in the representation of the result, and does not change the underlying terms.

**LEMMA 3.14 (SIMULATION OF FULL $\beta$-REDUCTION).** Let $\langle C[(\lambda x.t) u] | H \rangle$ be a valid graph of terms with $u$ closed. Then

$$
\langle C[(\lambda x.t) u] | H \rangle \rightarrow_{s\beta,ls,gc} \langle C[t^{\{x \leftarrow u\}}] | H \rangle
$$

**PROOF.** Since $u$ is closed we can trigger a sharing $\beta$-step, creating a new address $a$. Then each occurrence of $a$ in $t^{\{x \leftarrow a\}}$ can be linearly substituted by $u$ before the entry $a \mapsto u$ is removed from the heap.

$$
\begin{align*}
\langle C[(\lambda x.t) u] | H \rangle & \rightarrow_{s\beta} \langle C[t^{\{x \leftarrow a\}}] | H, a \mapsto u \rangle \\
& \rightarrow_{ls} \ast \langle C[t^{\{x \leftarrow u\}}] | H, a \mapsto u \rangle \\
& \rightarrow_{gc} \langle C[t^{\{x \leftarrow u\}}] | H \rangle
\end{align*}
$$

□
**LEMMA 3.15 (TERMINATION AND CONFLUENCE OF $\rightarrow_{gc}$).** The garbage collection rule $\rightarrow_{gc}$ is:

* strongly terminating: there is no graph of terms $\langle t | H \rangle$ from which an infinite reduction sequence $\langle t | H \rangle \rightarrow_{gc} \rightarrow_{gc} \rightarrow_{gc} \dots$ using only $\rightarrow_{gc}$-steps is possible;

* strongly confluent: if $\langle t | H \rangle \rightarrow_{gc} \langle t | H_1 \rangle$ and $\langle t | H \rangle \rightarrow_{gc} \langle t | H_2 \rangle$, then either $H_1 = H_2$ or there is $H_3$ such that $\langle t | H_1 \rangle \rightarrow_{gc} \langle t | H_3 \rangle$ and $\langle t | H_2 \rangle \rightarrow_{gc} \langle t | H_3 \rangle$.

**PROOF.** Termination can be proved by taking the number of entries in $H$ as a decreasing measure. Confluence comes from the fact two co-existing $\rightarrow_{gc}$-redexes affect disjoint parts of the graph of terms. $\square$

This lemma allows us to define the normalization of a graph of terms by $\rightarrow_{gc}$-reduction.

**DEFINITION 3.16 ($\rightarrow_{gc}$-NORMALIZATION).** Let $\langle t | H \rangle$ be a graph of terms. Its $\rightarrow_{gc}$-normalization, written $\langle t | H \rangle_{gc}$, is the graph of terms obtained by maximally applying $\rightarrow_{gc}$-reduction.

**LEMMA 3.17 (SOUNDNESS).** Reduction $\rightarrow$ is sound with respect to $\beta$-reduction in the $\lambda$-calculus.

* If $\langle t | H \rangle \rightarrow_{ls} \langle t' | H \rangle$, then $t^H = t'^H$.

* If $\langle t | H \rangle \rightarrow_{gc} \langle t | H' \rangle$, then $t^H = t'^H$.

* If $\langle t | H \rangle \rightarrow_{s\beta} \langle t' | H' \rangle$, then $t^H \rightarrow \beta t'^H$.

* If $\langle t | H \rangle \rightarrow_{f\beta} \langle t' | H \rangle$, then $t^H \rightarrow \beta t'^H$.

Moreover, in the last two points the graph of terms step $\rightarrow_{s\beta}$ or $\rightarrow_{f\beta}$ has the same position than the corresponding $\beta$-step $\rightarrow \beta$. In particular, one of these step is a weak step if and only the other is as well.

**PROOF.** For the first two points: remark that unfolding is equivalent to normalization by $\rightarrow_{ls}$ and $\rightarrow_{gc}$. For the last two points: unfolding does not affect the positions of the main term, which determine $\rightarrow_{s\beta}$ and $\rightarrow_{f\beta}$ steps. $\square$

The descendance relation extends to the extended positions of a graph of terms along graph reduction steps.

**DEFINITION 3.18 (EXTENDED DESCENDANCE).** The descendance relation on graphs of terms is defined by case on the reduction rule.

* If $\rho : \langle C[a] | H \rangle \rightarrow_{ls} \langle C[H(a)] | H \rangle$ with $H(C) = p$, then for any position $q \in \mathcal{P}(\langle C[a] | H \rangle)$,

- if $q \in \mathcal{P}(C)$, then $q/\rho = \{q\}$,

- if $q = 3$; $a$; $q'$, then $q/\rho = \{p$; $q'$\} $\cup$ $\{q\}$,

- if $q = 3$; $b$; $q'$ with $a \neq b$, then $q/\rho = \{q\}$,

- otherwise ($q = p$) we have $q/\rho = \emptyset$.

* If $\rho : \langle t | H \rangle \rightarrow_{gc} \langle t | H \setminus \{a\} \rangle$, then for any position $q \in \mathcal{P}(\langle t | H \rangle)$,

- if $q = 3$; $a$; $q'$, then $q/\rho = \emptyset$,

- otherwise $q/\rho = \{q\}$.

* If $\rho : \langle C[(\lambda x.t) u] | H \rangle \rightarrow_{s\beta} \langle C[t^{\{x \leftarrow \underline{a}\}}] | H, a \mapsto u \rangle$ with $H(\mathcal{E}) = p$, then for any position $q \in \mathcal{P}(\langle C[(\lambda x.t) u] | H \rangle)$,

- If $q \in \mathcal{P}(C)$ or $q = 3$; $a$; $q'$, then $q/\rho = \{q\}$.

- If $q = p$; $10$; $q'$ and $u|_{q'} \neq x$, then $q/\rho = \{p$; $q'$\}.

- If $q = p$; $2$; $q'$, then $q/\rho = \{3$; $a$; $q\}$.

- Otherwise, $q/\rho = \emptyset$.

* If $\rho : \langle C[(\lambda x.t) u] | H \rangle \rightarrow_{f\beta} \langle C[t^{\{x \leftarrow u\}}] | H \rangle$ with $H(\mathcal{E}) = p$, then for any position $q \in \mathcal{P}(\langle C[(\lambda x.t) u] | H \rangle)$,

- If $q \in \mathcal{P}(C)$ or $q = 3$; $a$; $q'$, then $q/\rho = \{q\}$.

- If $q = p$; $10$; $q'$ and $u|_{q'} \neq x$, then $q/\rho = \{p$; $q'$\}.
- If $q = p; 2; q'$, then $q/\rho = \{p; p_x; q' | u|_{p_x} = x\}$.

- Otherwise, $q/\rho = \emptyset$.

The notion of shape of a term is also naturally extended, and still preserved by the descendance relation.

**DEFINITION 3.19 (SHAPE).** The shape of an extended $\lambda$-term is a symbol in the set $\{\mathcal{X}, @, \Lambda, \mathcal{A}\}$, representing its main constructor.

$\mathrm{shape}(x) = \mathcal{X}$

$\mathrm{shape}(t u) = @$

$\mathrm{shape}(\lambda x.t) = \Lambda$

$\mathrm{shape}(a) = \mathcal{A}$

**LEMMA 3.20 (SHAPE PRESERVATION).** Let $\rho : C \to C'$ be a graph reduction step, and $p \in \mathcal{P}(C)$, $p' \in \mathcal{P}(C')$ two positions such that $p' \in p/\rho$. Then

$$ \mathrm{shape}(C|_p) = \mathrm{shape}(C'|_{p'}) $$

Moreover, if $p = 3$; $a$; $q$ is a position in the heap, then we have more precisely $C|_p = C'|_{p'}$.

Our definition of graph of terms reduction contains both the usual dynamics of the weak $\lambda$-calculus, and the dynamics of a graph-based machine. As such, it may exhibit both term-size explosion and pointer explosion behaviours seen in the introduction. However, we will see in the next section that the ability to choose for each $\beta$-redex whether to use full $\beta$-reduction or sharing $\beta$-reduction allows implementing both call-by-name and call-by-value evaluation in a time- and space-invariant manner.

# 4 A reasonable graph-based machine

We will now define a family of abstract machines for the evaluation of the weak $\lambda$-calculus, based on graphs of terms and their reduction rules. The main mechanisms of the machine are independent from the evaluation strategy of the $\lambda$-calculus we want to implement. We thus provide a parametric definition of the abstract machine, and then detail two instantiations on call-by-name and call-by-value. In both cases, the machine provides an implementation that is both time- and space-invariant.

Considering a weak reduction step $\rho : t \to_w t'$ in the $\lambda$-calculus, and a graph of terms $\langle u | H \rangle$ such that $u^H = t$, we want to implement the step $\rho$ by a sequence $\langle u | H \rangle \to^* \langle u' | H' \rangle$ such that $u'^H = t'$, with good complexity properties. Our implementation strategy is based on the following principles:

(1) use $\to_{\beta}$ if the space-cost of the argument of the $\beta$-redex is less than the space-cost of the first available pointer, and use $\to_{\beta}$ otherwise;

(2) use $\to_{ls}$ only as much as required to make the target $\beta$-redex visible in the main term;

(3) apply $\to_{gc}$ eagerly.

The third point is a classical requirement for reasoning on space complexity, and already plays a major role for instance in [5]. The second point is a criterion of “useful substitution”, corresponding to the same idea of “useful sharing” used in a series of recent work on invariance [3, 4, 6]. The first point looks like an overly simple idea. Yet, it seems to be the only one in this list that has not been exploited in recent work on the invariance of the $\lambda$-calculus, and it is the key of our time- and space-invariant implementation.

Remark that this implementation strategy describes how to implement an arbitrary weak $\beta$-step: it is independent from the choice of which weak $\beta$-redex is being reduced. As a consequence, our implementation strategy can be combined with any underlying $\lambda$-calculus evaluation strategy, and
we will show that call-by-name and call-by-value both yield good complexity properties (although some other strategies do not).

## 4.1 A parametric abstract machine

A configuration of our abstract machine is a graph of terms satisfying an additional compactness property.

**DEFINITION 4.1 (COMPACT GRAPHS / MACHINE CONFIGURATIONS).** Fix a constant $c_v$ for the cost of variables. A valid graph of terms $\langle t | H \rangle$ is compact if it satisfies the two following conditions:

(1) $\text{dom}(H) = \text{addr}(\langle t | H \rangle)$, meaning that no $\rightarrow_{gc}$-step is possible;

(2) for any $a \in \text{dom}(H)$ we have $\|a\|_{c_v} \le \|H(a)\|_{c_v}$.

These compact graphs of terms are the configurations of our abstract machine.

A reduction step of our abstract machine is a sequence of graph of terms reduction steps comprising one main step and possible garbage collection steps, in order to ensure that the obtained graph of terms is still compact, and thus a legit machine configuration. We make our implementation parametric in the underlying $\lambda$-calculus evaluation strategy.

**DEFINITION 4.2 (MACHINE STEPS).** Let $\mathcal{E}$ be a set of weak evaluation contexts, and $\mathcal{R}$ a property on $\lambda$-terms characterizing valid $\beta$-redexes. The $\mathcal{E},\mathcal{R}$-machine reduction steps are defined by the three following rules.

$$ \langle \mathcal{E}[(\lambda x.t) u] | H \rangle \rightarrow_{[f\beta]} \langle \mathcal{E}[t^{\{x \leftarrow u\}}] | H \rangle_{gc} \quad \mathcal{R}((\lambda x.t)u) \wedge a = \text{next}(H) \wedge \|u\|_{c_v} < \|a\|_{c_v} $$

$$ \langle \mathcal{E}[(\lambda x.t) u] | H \rangle \rightarrow_{[\beta]} \langle \mathcal{E}[t^{\{x \leftarrow a\}}] | H, a \mapsto u \rangle_{gc} \quad \mathcal{R}((\lambda x.t)u) \wedge a = \text{next}(H) \wedge \|u\|_{c_v} \ge \|a\|_{c_v} $$

$$ \langle \mathcal{E}[a] | H \rangle \rightarrow_{[ls]} \langle \mathcal{E}[H(a)] | H \rangle_{gc} $$

Remark that our parametric machine reduction may or may not be deterministic, depending on the choice of parameters $\mathcal{E}$ and $\mathcal{R}$. However, its instantiations implementing call-by-name and call-by-value, presented below, are deterministic.

As advertised, the machine steps go from machine configurations to machine configurations.

**LEMMA 4.3 (COMPACTNESS PRESERVATION).** If $\langle t | H \rangle$ is a compact graph of terms and $\langle t | H \rangle \rightarrow_{[Y]} \langle t' | H' \rangle$, then $\langle t' | H' \rangle$ is also a compact graph of terms.

**PROOF.** By definition of $\rightarrow_{[Y]}$, the target graph of terms $\langle t' | H' \rangle$ is irreducible by $\rightarrow_{gc}$ and satisfies condition (1). Condition (2) also holds, by case on the $\rightarrow_{[Y]}$ rule:

* if $\rightarrow_{[Y]} = \rightarrow_{[f\beta]}$ or $\rightarrow_{[Y]} = \rightarrow_{[ls]}$, then $H' \subseteq H$, and the condition holds by hypothesis;

* if $\rightarrow_{[Y]} = \rightarrow_{[\beta]}$ then $H' \subseteq (H, a \mapsto u)$, with $\|a\|_{c_v} \le \|u\|_{c_v}$ by hypothesis, which allows us to conclude. $\square$

## 4.2 Call-by-value and call-by-name strategies

We define our evaluation strategies using dedicated evaluation contexts, and possible restrictions on the reduction rules. The same contexts and restrictions will describe the usual call-by-value and call-by-name in the weak $\lambda$-calculus and in our abstract machine.

**DEFINITION 4.4 (CALL-BY-NAME).** Call-by-name evaluation never evaluates the right member of an application: the left member of an application is evaluated until it becomes an $\lambda$-abstraction, and then the application of this abstraction is $\beta$-reduced by substituting the argument as-is. Moreover call-by-name evaluation never takes place inside a $\lambda$-abstraction, as any weak reduction strategy. Evaluation contexts $\mathcal{E}_{cbn}$ for call-by-name evaluation are defined as follow.

$$ \mathcal{E}_{cbn} ::= \square | \mathcal{E}_{cbn} t \quad \text{call-by-name evaluation contexts} $$
Call-by-name evaluation in the λ-calculus consists in applying β-reduction only in $\mathcal{E}_{cbn}$ contexts.

Call-by-name computation in our abstract machine is the $\mathcal{E}_{cbn},\mathcal{B}$-reduction, where $\mathcal{B}$ is the property that is true for any term of shape $(\lambda x.t)u$.

**DEFINITION 4.5 (CALL-BY-VALUE)** Call-by-value evaluation evaluates both the left and the right member of an application before applying the β-reduction rule. It relies on a syntactic notion of value (a λ-abstraction) describing terms that have been sufficiently evaluated.

$$ \begin{array}{lclcl} v & ::= & \lambda x.t & \quad \text{values} \\ (\lambda x.t) v & \to_{\beta v} & t^{\{x \leftarrow v\}} & \quad \text{if } v \text{ value} \end{array} $$

Evaluation of the two members of an application can be performed in any order without changing much the properties of the strategy. Here we define evaluations contexts $\mathcal{E}_{cbv}$ for call-by-value evaluation from right to left.

$$ \mathcal{E}_{cbv} ::= \Box | t \mathcal{E}_{cbv} | \mathcal{E}_{cbv} v \quad \text{call-by-value evaluation contexts} $$

Call-by-value evaluation in the λ-calculus consists in applying βv-reduction in $\mathcal{E}_{cbv}$ contexts.

Call-by-value evaluation in our abstract machine is the $\mathcal{E}_{cbv},\mathcal{V}$-reduction, where $\mathcal{V}((\lambda x.t)v)$ is true if and only if $v$ is a value.

**LEMMA 4.6 (DETERMINISM).** Call-by-name and right-to-left call-by-value reduction are both deterministic: for any compact configuration $\langle t | H \rangle$, there is at most one applicable rule $\to_{[Y]}$ and one $\langle t' | H' \rangle$ such that $\langle t | H \rangle \to_{[Y]} \langle t' | H' \rangle$.

**PROOF.** Straightforward, knowing determinism of these strategies in the weak λ-calculus. $\square$

<figure><img src="image_2.png" /></figure>

## 4.3 Examples

We show here how our abstract machine manages the examples of size explosion and pointer explosion seen in the introduction

*Avoiding size explosion.* Consider the term $c_n c_2 \text{ ld}$ seen in the introduction, where $c_n$ and $c_2$ are Church integers. Call-by-value evaluation in our machine goes as follows.

$$ \begin{align*} \langle c_n c_2 \text{ ld} | \emptyset \rangle &\to_{[s\beta]} \langle (\lambda x.(\underline{a}(\underline{a}(\dots(\underline{a} x)\dots)))) \text{ ld} | a \mapsto c_2 \rangle \\ &\to_{[s\beta]} \langle \underline{a}(\underline{a}(\dots(\underline{a} \underline{b})\dots)) | a \mapsto c_2, b \mapsto \text{ld} \rangle \\ &\to_{[ls]} \langle \underline{a}(\underline{a}(\dots(\underline{a} \text{ ld})\dots)) | a \mapsto c_2 \rangle \\ &\to_{[ls]} \langle \underline{a}(\underline{a}(\dots(\underline{c_2} \text{ ld})\dots)) | a \mapsto c_2 \rangle \\ &\to_{[s\beta]} \langle \underline{a}(\underline{a}(\dots(\lambda x.\underline{b_1}(\underline{b_1}x))\dots)) | a \mapsto c_2, b_1 \mapsto \text{ld} \rangle \\ &\to_{[ls]} \langle \underline{a}(\underline{a}(\dots(\lambda x.\underline{b_1}(\underline{b_1}x))\dots)) | a \mapsto c_2, b_1 \mapsto \text{ld} \rangle \\ &\to_{[s\beta]} \langle \underline{a}(\underline{a}(\dots(\lambda x.\underline{b_2}(\underline{b_2}x))\dots)) | a \mapsto c_2, b_1 \mapsto \text{ld}, b_2 \mapsto \lambda x.\underline{b_1}(\underline{b_1}x) \rangle \\ &\vdots \\ &\to_{[s\beta]} \langle \lambda x.\underline{b_n}(\underline{b_n}x) | b_1 \mapsto \text{ld}, \dots, b_n \mapsto \lambda x.\underline{b_{n-1}}(\underline{b_{n-1}}x) \rangle \end{align*} $$

*Avoiding pointer explosion.* Consider the terms below, seen in the introduction.

$$ \begin{align*} e &= (\lambda xy.xx) \text{ ld} \\ p_n &= e(\dots(e \text{ ld})\dots) \quad \text{n occurrences of } e \end{align*} $$
The evaluation of $p_n$ in our machine goes as follows.

$$ \begin{aligned} & \langle p_n | \emptyset \rangle \\ \rightarrow^{[s\beta]} & \langle (\lambda y.a_1 a_1) p_{n-1} | a_1 \mapsto \text{Id} \rangle \\ \rightarrow^{3} & \langle (\lambda y.a_1 a_1)(\dots((\lambda y.a_4 a_4) p_{n-4})\dots) | a_1 \mapsto \text{Id}, \dots, a_4 \mapsto \text{Id} \rangle \\ \rightarrow^{n-4} & \langle (\lambda y.a_1 a_1)(\dots((\lambda y.a_4 a_4)((\lambda y.\text{Id }\text{Id})(\dots((\lambda y.\text{Id }\text{Id})\text{Id})\dots))) | a_1 \mapsto \text{Id}, \dots, a_4 \mapsto \text{Id} \rangle \\ \rightarrow^{[f\beta]} & \langle (\lambda y.a_1 a_1)(\dots((\lambda y.a_4 a_4)((\lambda y.\text{Id }\text{Id})(\dots(\text{Id }\text{Id})\dots)))\dots) | a_1 \mapsto \text{Id}, \dots, a_4 \mapsto \text{Id} \rangle \\ \rightarrow^{[f\beta]} & \langle (\lambda y.a_1 a_1)(\dots((\lambda y.a_4 a_4)((\lambda y.\text{Id }\text{Id})(\dots(\lambda y.\text{Id})\dots)))\dots) | a_1 \mapsto \text{Id}, \dots, a_4 \mapsto \text{Id} \rangle \\ \rightarrow^{[s\beta]} & \langle (\lambda y.a_1 a_1)(\dots((\lambda y.a_4 a_4)((\lambda y.\text{Id }\text{Id})(\dots(\text{Id }\text{Id})\dots)))\dots) | a_1 \mapsto \text{Id}, \dots, a_4 \mapsto \text{Id} \rangle \\ \rightarrow^* & \langle (\lambda y.a_1 a_1)(\dots((\lambda y.a_4 a_4)(\lambda y.\text{Id}))\dots) | a_1 \mapsto \text{Id}, \dots, a_4 \mapsto \text{Id} \rangle \\ \rightarrow^{[s\beta]} & \langle (\lambda y.a_1 a_1)(\dots(\underline{a_4 a_4})\dots) | a_1 \mapsto \text{Id}, \dots, a_4 \mapsto \text{Id} \rangle \\ \rightarrow^{[ls]} & \langle (\lambda y.a_1 a_1)(\dots(\underline{\text{Id }a_4})\dots) | a_1 \mapsto \text{Id}, \dots, a_4 \mapsto \text{Id} \rangle \\ \rightarrow^{[ls]} & \langle (\lambda y.a_1 a_1)(\dots(\text{Id }\text{Id})\dots) | a_1 \mapsto \text{Id}, \dots, a_3 \mapsto \text{Id} \rangle \\ \rightarrow^{[s\beta]} & \langle (\lambda y.a_1 a_1)(\dots(\lambda y.\underline{b})\dots) | a_1 \mapsto \text{Id}, \dots, a_3 \mapsto \text{Id}, b \mapsto \text{Id} \rangle \\ \rightarrow^{[s\beta]} & \langle (\lambda y.a_1 a_1)(\dots(\underline{a_3 a_3})\dots) | a_1 \mapsto \text{Id}, \dots, a_3 \mapsto \text{Id} \rangle \\ \rightarrow^* & \langle \lambda y.\underline{b} | b \mapsto \text{Id} \rangle \end{aligned} $$

After a bounded number of steps, the cost of a pointer is higher than the space cost of the term $\text{Id}$. The reduction then switches from $\rightarrow^{s\beta}$ to $\rightarrow^{f\beta}$, and the global space cost remains linear. On the other hand, using only $\rightarrow^{s\beta}$ we would create a linear number of heap entries, resulting in a linearithmic space cost.

# 5 Time- and space-invariance

We show that our implementation model is reasonable for both time and space by combining two elements:

(1) any call-by-name or call-by-value reduction sequence of length $n$ and space cost $c$ in the weak $\lambda$-calculus can be performed by our respective machine with a number of machine steps polynomial in $n$ (Section 5.4) and space cost proportional to $c$ (Section 5.1);

(2) any such computation sequence of our machine can be implemented on a Turing machine with a polynomial overhead in time and a constant-factor overhead in space (Section 5.5).

While space soundness is easily obtained, time soundness is much more involved and comes only after a detailed analysis of how terms and machine configurations grow.

## 5.1 Space soundness of the machine

The space soundness of our abstract machine is immediate, and independent from the evaluation strategy: it only comes from the combination of eager garbage collection and of the space-aware choice between $\rightarrow^{f\beta}$ and $\rightarrow^{s\beta}$ for implementing each $\beta$-step. This is formalized by the fact that machine configurations (compact graphs of terms) have a space cost that is bounded by the space cost of the corresponding unfolded term, up to a constant factor.

**LEMMA 5.1 (SPACE COST OF MACHINE CONFIGURATIONS).** For any constant $c_v$ and any machine configuration $\langle t | H \rangle$, we have

$$ \|\langle t | H \rangle\|_{c_v} \le 3 \times \|t^H\|_{c_v} $$

**PROOF.** Since $\langle t | H \rangle$ is compact we know that for any $a \in \text{dom}(H)$ we have $\|a\|_{c_v} \le \|H(a)\|_{c_v}$. In particular, this implies that $\|t\|_{c_v} \le \|t^H\|_{c_v}$ and $\|H\|_{c_v} = \sum_{a \to u \in H} \|a\|_{c_v} + \|u\|_{c_v} \le 2 \times \sum_{a \to u \in H} \|u\|_{c_v}$. Moreover, still since $\langle t | H \rangle$ is compact, we know that for any $a \in \text{dom}(H)$ there is at least one occurrence of $H(a)$ in $t^H$. Thus $\sum_{a \to u \in H} \|u\|_{c_v} \le \|t^H\|_{c_v}$. Finally, $\|\langle t | H \rangle\|_{c_v} = \|t\|_{c_v} + \|H\|_{c_v} \le 3 \times \|t^H\|_{c_v}$ □
## 5.2 Heap growth

**LEMMA 5.2 (HEAP GROWTH).** Let $\langle t | \emptyset \rangle \to_{[Y]}^* \langle t' | H' \rangle$ and $n$ be the number of $\to^{\downarrow s_\beta}$ machine steps in the sequence. Then the number $|\text{dom}(H)|$ of elements in the domain of $H$ satisfies $|\text{dom}(H)| \le n$.

**PROOF.** Each $\to^{\downarrow s_\beta}$ machine step adds at most one entry in the heap (due to garbage collection, this entry can also immediately disappear). No other rule can add an entry. $\square$

**LEMMA 5.3 (EVOLUTION OF VALUES IN WEAK REDUCTION).** Consider a reduction sequence $\langle t | \emptyset \rangle \to_{[Y]}^n \langle t' | H' \rangle$. Any value $\lambda x.u'$ in $\langle t' | H' \rangle$ is a descendant from a value $\lambda x.u$ in $\langle t | \emptyset \rangle$. Moreover, $u' = u^{\{x_i \leftarrow u_i\}}$ where each $u_i$ has a space cost $\|u_i\|_{c_v} \le \log(n)$.

**PROOF.** By induction on the number $n$ of steps. The initialization at $n=0$ is immediate. Assume the property holds for the reduction sequence $\langle t_0 | \emptyset \rangle \to_{[Y]}^n \langle t | H \rangle$ and consider a reduction step $\langle t | H \rangle \to_{[Y]} \langle t' | H' \rangle$. By case on the step.

* Step $\to_{ls} \rho: \langle \mathcal{E}[\underline{a}] | H \rangle \to_{ls} \langle \mathcal{E}[H(a)] | H \rangle$ with $\mathcal{H}(C) = p$. Consider a value $v$ at position $q$ in $\langle \mathcal{E}[H(a)] | H \rangle$.

- If $q = p; q'$, then $v$ descends from an identical subterm in $\langle \mathcal{E}[\underline{a}] | H \rangle$ at position 3; $a; q'$.

- If $q$ is disjoint from $p$, then $v$ descends from an identical subterm in $\langle \mathcal{E}[\underline{a}] | H \rangle$ at the same position.

- By weak reduction, $q$ cannot be a prefix of $p$.

* Step $\to^{\downarrow gc}$. Straightforward: any subterm in $\langle t' | H' \rangle$ descends from an identical subterm at the same position in $\langle t | H \rangle$.

* Step $\to^{\downarrow s_\beta} \rho: \langle \mathcal{E}[(\lambda x.t) u] | H \rangle \to^{\downarrow s_\beta} \langle \mathcal{E}[t^{\{x \leftarrow \underline{a}\}}] | H, a \mapsto u \rangle$ with $\mathcal{H}(\mathcal{E}) = p$, and $a$ the smallest address not allocated in $H$. Consider a value $v$ at position $q$ in $\langle \mathcal{E}[t^{\{x \leftarrow \underline{a}\}}] | H, a \mapsto u \rangle$.

- If $q = 3; a; q'$, then $v$ descends from an identical value at position $p$; $2; q'$ in $\langle \mathcal{E}[(\lambda x.t) u] | H \rangle$.

- If $q$ is any other position disjoint from $p$, then $v$ descends from an identical subterm at the same position.

By weak reduction, $q$ cannot be a prefix of $p$. Otherwise, $q = p; q'$ and $v$ descends from a value $v'$ in $\langle \mathcal{E}[(\lambda x.t) u] | H \rangle$ such that $v = (v')^{\{x \leftarrow \underline{a}\}}$. Since $|H| \le n$ and $a$ is the smallest address not allocated in $H$ we have $a \le n+1$ and $\|\underline{a}\|_{c_v} \le \log(n+1)$.

* Step $\to^{\downarrow f_\beta} \rho: \langle \mathcal{E}[(\lambda x.t) u] | H \rangle \to^{\downarrow f_\beta} \langle \mathcal{E}[t^{\{x \leftarrow u\}}] | H \rangle$ with $\mathcal{H}(\mathcal{E}) = p$ and $\|u\|_{c_v} \le \log(a)$ for $a$ the first address not allocated in $H$.

- If $q$ is any position disjoint from $p$, then $v$ descends from an identical subterm at the same position. By weak reduction, $q$ cannot be a prefix of $p$.

- Otherwise, $q = p; q'$ and $v$ descends from a value $v'$ in $\langle \mathcal{E}[(\lambda x.t) u] | H \rangle$ such that $v = (v')^{\{x \leftarrow u\}}$.

Since $|H| \le n$ and $a$ is the smallest address not allocated in $H$ we have $a \le n+1$ and $\|u\|_{c_v} \le \|\underline{a}\|_{c_v} \le \log(n+1)$. $\square$

**COROLLARY 5.4 (SPACE COST OF VALUES).** Since the number of substituted variable occurrences in $u^{\{x_i \leftarrow u_i\}}$ is less than the size of $u$, we deduce that $\|u'\|_{c_v} \le \|u\|_{c_v} + |u| \times \log(n) \le \|u\|_{c_v} (1 + \log(n)) \le \|\langle t | H \rangle\|_{c_v} (1 + \log(n))$.

**LEMMA 5.5 (EVOLUTION OF RIGHT MEMBERS OF APPLICATIONS IN CALL-BY-NAME).** Consider a call-by-name machine reduction sequence $\langle t | H \rangle \to_{cbn}^{\downarrow n} \langle t' | H' \rangle$. The property stated in Lemma 5.3 for value also hold for any right member of an application in $\langle t' | H' \rangle$.
PROOF. Similar. Call-by-name forbids reduction in a right member of an application. Any right member either descends from an identical right member, or is the result of applying a small substitution to a right member. □

LEMMA 5.6 (HEAP COST). Assume a sequence $\rho : \langle t_0 | \emptyset \rangle \to^*_{[\gamma]} \langle t | H \rangle$, either call-by-name or call-by-value, containing $n \beta$-reduction steps. Then for any address $a \in \text{dom}(H)$ we have

$$ \|H(a)\|_{c_v} \le \|t_0\|_{c_v} + |t_0| \times \log(n) $$

Moreover

$$ \text{ht}(H(a)) \le \text{ht}(t_0) + \log(n) $$

PROOF. First remark that a term stored in the heap is never modified. Thus we are only interested in what is stored in the heap by the rule $\to_{s\beta}$. In the case of call-by-value, the stored argument is necessarily a value. It respects the cost bound by Corollary 5.4. The argument stored in the heap is also the right member of the application. In the case of call-by-name, it also respects the cost bound by Lemma 5.5. The additional property on the height of heap terms is proved similarly. □

## 5.3 A bound on the number of linear substitution steps.

The time soundness of our abstract machine is the fact that the number of machine steps required for implementing a weak $\beta$-reduction sequence $t \to^n_w t'$ of length $n$ is polynomial in $n$. We already know by Lemma 3.17 that the set of $\to_{[f\beta]} / \to_{[s\beta]}$ steps is in bijective correspondence with the set of $\beta$-steps of the corresponding sequence. The goal now is to provide a polynomial bound on the number of $\to_{[ls]}$ steps that can be performed between to $\to_{[f\beta]} / \to_{[s\beta]}$ steps. This is quite simple in the case of call-by-name, and more subtle in the case of call-by-value.

We start with lemmas on the structure of sequences of substitutions steps that are independent from the evaluation strategy.

DEFINITION 5.7 (EVALUATION POSITION). Let $t$ be a $\lambda$-term. Let $\mathcal{E}$ be a family of evaluation contexts. An $\mathcal{E}$-evaluation position of $t$ is a position $p \in \mathcal{P}(t)$ such that there is an evaluation context $\mathcal{E}$ and a subterm $u$ satisfying $t = \mathcal{E}[u]$ and $\mathcal{H}(\mathcal{E}) = p$.

LEMMA 5.8 (STRUCTURE OF SUBSTITUTION SEQUENCES). Let $\langle t | H \rangle \to^*_{[ls]} \langle t' | H' \rangle$ be a $\mathcal{E}, \mathcal{R}$-machine reduction sequence performing only linear substitution steps. Let $p_i$ be the position of the $i$th step in the sequence. Then $p_i$ is an $\mathcal{E}$-evaluation position of $t^H$.

PROOF. Let $\langle t_i | H_i \rangle$ be the machine configuration to which the $i$th $\to_{[ls]}$ step applies. Then by definition $p_i \in \mathcal{P}(t_i)$ and there are $\mathcal{E}_i$ and $a_i$ such that $t_i = \mathcal{E}_i[a_i]$ and $\mathcal{H}(\mathcal{E}_i) = p_i$. Moreover, since the positions and evaluation contexts of $t_i$ are preserved by unfolding we know that $p_i \in \mathcal{P}(t_i^{H_i})$ and there is $u_i$ such that $t^H = \mathcal{E}_i[u_i]$. Finally, by Lemma 3.17 we have $t^H = t_i^{H_i}$, which allows us to conclude. □

LEMMA 5.9 (BOUND ON NESTED SUBSTITUTIONS). Let $\langle t_0 | H_0 \rangle$ be a machine configuration, and $\langle t_0 | H_0 \rangle \to_{[ls]} \langle t_1 | H_1 \rangle \to_{[ls]} \dots \to_{[ls]} \langle t_n | H_n \rangle$ be a $\mathcal{E}, \mathcal{R}$-machine reduction sequence of linear substitution steps. Let $p_i$ be the position of the step $\langle t_i | H_i \rangle \to_{[ls]} \langle t_{i+1} | H_{i+1} \rangle$, and $a_i$ the address substituted in this step.

If $p_i$ is a strict prefix of $p_j$, then $i < j$. Moreover, any ascending sequence $i_1, \dots, i_k$ such that $p_{i_j}$ is a prefix of $p_{i_{j+1}}$ has length at most $\text{dom}(H_0)$.

PROOF. First remark that the only possible modifications of the heap in this sequence come from the $\to_{gc}$-normalization included in each step. In particular, any heap $H_i$ in this sequence is such that $H_i \subseteq H_0$. If $p$ is the position of a $\to_{[ls]}$ step in a configuration $\langle t | H_0 \rangle$, then $t|_p = a$, and there
is no position in *t* of which *p* is a strict prefix. Let *i*₁, ..., *i*ₖ be a maximal ascending sequence such that *p*ᵢⱼ is a prefix of *p*ᵢⱼ₊₁ for all *j*. By maximality there is no *j*, *j*' such that *i*ⱼ < *j*' < *i*ⱼ₊₁ and *p*ᵢⱼ is a prefix of *p*ᵢⱼ', which is a prefix of *p*ᵢⱼ₊₁.

For each $j \in [1, k)$, we know that $t_{ij} | p_{ij} = a_{ij}$ and $p_{i_j+1} = p_{ij}; p'$ with $H_0(a_{ij})|_{p'} = a_{i_j+1}$. Thus there is an edge from $a_{ij}$ to $a_{i_j+1}$ in the graph underlying $H_0$. Since the graph is acyclic, there can be at most $\text{dom}(H_0) - 1$ such edges, and thus at most $\text{dom}(H_0)$ elements in the ascending sequence. $\square$

**LEMMA 5.10 (EVALUATION POSITIONS).** Let $t$ be a $\lambda$-term.

* The $\mathcal{E}_{\text{cbn}}$-evaluation positions of $t$ are precisely the positions of $t$ containing only the symbol 1.

* The $\mathcal{E}_{\text{cbv}}$-evaluation positions of $t$ are the positions of $t$ containing only the symbols 1 and 2, with the constraint that a position $p$; 1; $q$ can be an $\mathcal{E}_{\text{cbv}}$-evaluation position only if $t|_{p;2}$ is a value.

**PROOF.** By inspection of the definitions of $\mathcal{E}_{\text{cbn}}$ and $\mathcal{E}_{\text{cbv}}$ evaluation contexts. $\square$

**LEMMA 5.11 (USEFUL SUBSTITUTION: CALL-BY-NAME).** Consider a call-by-name machine reduction sequence $\bar{\rho} : \langle t \mid H \rangle \rightarrow_{[Y]}^{*} \langle v \mid \emptyset \rangle$ reaching a final configuration. Then the position $p$ of any $\rightarrow_{[ls]}$ step $\rho_{ls}$ in $\bar{\rho}$, satisfies the following.

(1) If there is a $\rightarrow_{[s\beta]}$ or a $\rightarrow_{[f\beta]}$ after $\rho_{ls}$ in $\bar{\rho}$, then write $q$ the position of the first such reduction coming after $\rho_{ls}$. Then either $p$ is a prefix of $q$, or $p = q$; 1.

(2) Otherwise, $p = \varepsilon$.

**PROOF.** Consequence of Lemma 5.10. If there is a $\beta$-redex in the focus of a $\mathcal{E}_{\text{cbn}}$ evaluation context at position $q = 1; 1; \dots; 1$ in a given machine configuration $C$, then each step in the sequence of $\rightarrow_{[ls]}$-steps that immediately precedes configuration $C$ has a position $p = 1; 1; \dots; 1$ of same shape, which is either a prefix of $q$ (and the step participated in bringing the redex from the heap to the main term) or exactly $q$; 1 (and the step participated in bringing the $\lambda$-abstraction of the redex from the heap to the main term).

Otherwise, the only possible possible $\rightarrow_{[ls]}$ steps are at position $\varepsilon$, and contribute to bringing the final value of the computation from the heap to the main term. $\square$

**COROLLARY 5.12 (BOUND ON SUBSTITUTION STEPS: CALL-BY-NAME).** Starting from a compact configuration $\langle t \mid H \rangle$, a sequence of linear substitution steps $\langle t \mid H \rangle \rightarrow_{[ls]}^{n} \langle t' \mid H' \rangle$ can contain at most $|\text{dom}(H)|$ steps.

**PROOF.** By Lemma 5.11, all these steps have positions that are prefixes of some position of shape 1; 1; ...; 1. By Lemma 5.9 these steps are ordered in a way that is compatible with the prefix order on their positions, and their number is bounded by $|\text{dom}(H)|$. $\square$

**LEMMA 5.13 (USEFUL SUBSTITUTION: CALL-BY-VALUE).** Consider a call-by-name machine reduction sequence $\bar{\rho} : \langle t \mid H \rangle \rightarrow_{[Y]}^{*} \langle v \mid \emptyset \rangle$ reaching a final configuration. Then the position $p$ of any $\rightarrow_{[ls]}$ step $\rho_{ls}$ in $\bar{\rho}$, satisfies the following.

(1) If there is a $\rightarrow_{[s\beta]}$ or a $\rightarrow_{[f\beta]}$ after $\rho_{ls}$ in $\bar{\rho}$, then write $q$ the position of the first such reduction coming after $\rho_{ls}$. Then either $p$ is a prefix of $q$, or $p = q$; 1, or $p = q'$; 2 with $q'$ a prefix of $q$.

(2) Otherwise, $p = \varepsilon$.

**PROOF.** Similar to Lemma 5.11, with the additional feature that when a $\beta$-redex is in the focus of a $\mathcal{E}_{\text{cbv}}$ evaluation context at position $p$; 1; $p'$ in configuration $C$, then we know that $C|_{p;2}$ is a value, and $\rightarrow_{[ls]}$ steps may have been necessary at this position to make this value appear. $\square$
**COROLLARY 5.14 (BOUND ON SUBSTITUTION STEPS: CALL-BY-VALUE).** Starting from a compact configuration $\langle t | H \rangle$, a sequence of linear substitution steps $\langle t | H \rangle \to^{n}_{[ls]} \langle t' | H' \rangle$ can contain at most $|dom(H)| \times ht(t^H)$ steps.

**PROOF.** By Lemma 5.13, all these steps have positions that are prefixes of the same position $p$, or have a position $q$; 2 for a strict prefix $q$ of $p$. By Lemma 5.9 there cannot be more than $|dom(H)|$ steps at each position $q$; 2, and there are at most $ht(t^H) - 1$ such positions $q$; 2. By Lemma 5.9 again, there cannot be more than $|dom(H)|$ on the path $p$. Finally, the total number of $\to_{[ls]}$ steps in this sequence is bounded by $|dom(H)| \times ht(t^H)$. $\square$

Corollary 5.12 ensures that our call-by-name machine implements a reduction sequence with $n$ $\beta$-steps in a number of steps that is polynomial in $n$. In order to ensure that the bound given by Corollary 5.14 has the same property, we have however to bound the size of the terms seen in a sequence of machine steps. This is the focus of the next section.

**LEMMA 5.15 (BOUND ON HEIGHT GROWTH BY SUBSTITUTION STEPS).** Let $\langle t | H \rangle \to^{*}_{[ls]} \langle t' | H' \rangle$ be an $\mathcal{E},\mathcal{R}$-machine reduction sequence consisting only of linear substitution steps. Then

$$ht(t') \le ht(t) + \sum_{a \to u \in H} ht(u)$$

**PROOF.** The height increase is bounded by the sum of the heights of terms substituted by $\to_{[ls]}$-steps on a single path of $t^H$. By lemma 5.9 each entry $a \mapsto u$ of the heap can be substituted only once on a given path. $\square$

**LEMMA 5.16 (HEIGHT GROWTH).** There is a polynomial $P_h$ such that, for any call-by-name or call-by-value machine reduction sequence $\rho : \langle t_0 | \emptyset \rangle \to^{*}_{[Y]} \langle t | H \rangle$ containing $n$ $\beta$-reduction steps,

$$ht(t) \le ht(t_0) \times P_h(n)$$

As a consequence, there is also a polynomial $P'_h$ such that, under the same conditions,

$$ht(t^H) \le ht(t_0) \times P'_h(n)$$

**PROOF.** At any configuration in such a sequence, the heap contains at most $n$ elements of height bounded by $ht(t_0) + \log(n)$. Thus any sequence of $\to_{[ls]}$-steps between two $\beta$-steps (or after the last $\beta$-step) increments the height of the main term by at most $n \times (ht(t_0) + \log(n))$. Moreover, a $\to_{s\beta}$-step cannot increment the height, and a $\to_{f\beta}$-step increments the height by at most $(ht(t_0) + \log(n))$. Thus after a sequence containing $n$ $\beta$-steps and intermediate $\to_{[ls]}$-sequences, the height of the obtained main term $t$ is at most $ht(t_0) + n(n+1)(ht(t_0) + \log(n))$. $\square$

## 5.4 Term growth and time soundness of the machine

**LEMMA 5.17 (TIME SOUNDNESS).** There is a polynomial $P_t$ such that, for any call-by-name or call-by-value reduction sequence $t \to^{n}_w t'$ of $n$ steps in the weak $\lambda$-calculus, our respective call-by-name or call-by-value abstract machine produces a reduction sequence $\langle t | \emptyset \rangle \to^{m}_{[Y]} \langle u | H \rangle$ with $u^H = t'$ and

$$m \le |t| \times P_t(n)$$

**PROOF.** Soundness of the abstract machine ensures the existence of a reduction sequence $\langle t | \emptyset \rangle \to^{m}_{[Y]} \langle u | H \rangle$ with $u^H = t'$, containing exactly $n \to_{f\beta}$ or $\to_{s\beta}$ steps, and $n$ sequences of consecutive $\to_{[ls]}$ steps. By Lemmas 5.14 and 5.12 each of these sequences of $\to_{[ls]}$ steps contains at most $|dom(H')| \times ht(u'^{H'})$ steps, where $\langle u' | H' \rangle$ is the configuration to which the sequence
applies. By Lemma 5.16 there is a polynomial $P'_h$ such that $ht(v'H') \le ht(t) \times P'_h(n)$. Since moreover $ht(t) \le |t|$ and $\text{dom}(H') \le n$ we conclude that the total number $m$ of steps is such that $m \le n(1+n \times |t| \times P'_h(n))$. $\square$

**LEMMA 5.18 (TERM GROWTH).** There is a polynomial $P_c$ such that, for any call-by-name or call-by-value machine reduction sequence $\rho: \langle t_0 | \emptyset \rangle \stackrel{\ast}{\to}_{[Y]} \langle t | H \rangle$ containing $n$ $\beta$-reduction steps,

$$ \|t\|_{c_v} \le \|t_0\|_{c_v} \times P_c(n) $$

*PROOF.* By Lemma 5.6, at any point in this sequence, any term $s$ stored in the heap is such that $\|s\|_{c_v} \le \|t_0\|_{c_v} + |t_0| \times \log(n)$. Thus, each $\to_{[|s|]}$ in the sequence increases the space cost of the main term by at most $\|t_0\|_{c_v} + |t_0| \times \log(n)$, which is itself bounded by $\|t_0\|_{c_v} (1 + \log(n))$.

Moreover, any $\to_{\beta}$ or $\to_{\beta\sigma}$ step in the sequence substitutes a pointer or subterm whose space cost is not more than $\log(n) + 1$ (the worst-case cost of a pointer), in the body of a $\lambda$-abstraction which, by Lemma 5.3, contains at most $|t_0|$ variable occurrences. Thus such a step increases the space cost of the main term by at most $|t_0| \times \log(n)$, which is itself bounded by $\|t_0\|_{c_v} \times \log(n)$.

Finally, by Lemma 5.17 we know that the total number of steps is bounded by $P_t(n)$, and we conclude that $\|t\|_{c_v} \le \|t_0\|_{c_v} + P_t(n) \times \|t_0\|_{c_v} (1 + \log(n))$. $\square$

## 5.5 Implementation on a Turing machine

In this section we provide hints for implementing our abstract machine on a Turing machines and justifying that this implementations has the required complexity properties.

*Representation of a configuration.* A machine configuration is represented on a Turing tape in two segments:

* the representation of the main term,

* a representation of the heap in the form of a sequence of triples $(a, t, r)$ where $a$ is an address, $t$ is the representation of the associated term, and $r$ is an integer.

Terms are represented fully parenthesized (and even better, with two different kinds of parentheses respectively for applications and abstractions), and variables are represented as de Bruijn indices. Addresses and other integers are represented in binary notation. The integer $r$ in a triple $(a, t, r)$ in the heap is a counter for the implementation of $\to_{gc}$-normalization by reference counting: it represents the number of occurrences of $a$ in the configuration.

The length of the representation of the configuration $\langle t | H \rangle$ is bounded by a constant $c$ times the space cost $\|\langle t | H \rangle\|_{c_v}$, where $c_v$ is defined as the logarithm of the highest de Bruijn index in $\langle t | H \rangle$. The only non-straightforward aspect of this bound concerns the representation of the reference counters in the heap. However, remark that the sum $R$ of all these counters is equal to the total number of pointers in $\langle t | H \rangle$, and thus $R \le |\langle t | H \rangle| \le \|\langle t | H \rangle\|_{c_v}$.

Auxiliary information for the various operations is kept in a third segment.

*Parsing.* Several operations require identifying a segment of the tape representing a subterm. Since the terms represented on the tape are assumed to be well-formed, we do not try to check their syntactic validity: it is enough to locate the appropriate segment. This is done by counting parenthesis, in time linear and space logarithmic with respect to the length of the parsed fragment.

*Redex search.* Both call-by-name and right-to-left call-by-value enjoy evaluation contexts with simple shapes and simple search procedures:

* for call-by-name, scans the main term from left to right, ignoring the contents of abstractions, and apply a reduction step on the first pointer or the first applied abstraction;
* for right-to-left call-by-value, scans the main term from right to left, similarly ignoring the contents of abstractions and applying a reduction step on the first pointer or the first applied abstraction.

Remark that in call-by-value, the right-to-left discipline ensures that when we find an applied abstraction, its argument has already been evaluated. This scanning operation is done in time linear and space logarithmic with respect to the length of the main term.

*Linear substitution.* Substitution of a pointer of the main term by the corresponding term from the heap comprises: locating the appropriate triple in the heap; copying the associated term in place of the pointer, while shifting any element of the tape as required to make room for the substituted term; decrementing the reference counter of the substituted term; incrementing the reference counter corresponding to any duplicated pointer. These operations are done in time polynomial in the length of the tape and constant space.

*$\beta$-reduction.* Finding the first available address is done in time polynomial in the length of the tape, and logarithmic space, by checking each address in order, starting from 0. Checking the cost of the argument is a simple scan. In case of a $\rightarrow_{[s\beta]}$ reduction, the creation of a new heap entry is a copy of the argument, similar to the one done for linear substitution, and a scan of the body of the function for determining the initial value of the reference counter. The substitution of a small argument or of a pointer is also similar to linear substitution applied at several positions, and remains polynomial. As above, these operations also imply updating reference counters, and shifting some parts of the tape.

*Garbage collection.* Each time a reference counter is decremented, check whether its new value is zero. In that case, remove the corresponding heap entry and decrements the reference counters of its pointers. This is done in time polynomial in the length of the tape, and linear space (worst case, if maintaining a work list of heap entries to be collected).

Remark that, since our heap is acyclic, garbage collection by reference counting indeed collects every unused heap entry.

*Wrapping up.* We described how to implement the basic operations of our abstract machine in polynomial time and linear space with respect to the size of the tape. Moreover, we described a tape representation that directly relates to the actual space cost of the underlying configuration, and by Lemmas 5.2, 5.6 and 5.18, we know that the space cost of a configuration is polynomial in the number of computation steps. By composing these, we conclude that all the operations of our abstract machine run in polynomial time with respect to the length of the original $\beta$-reduction sequence, and linear space.

## 5.6 Main result

THEOREM 5.19 (INVARIANCE). There are two Turing machines $T_{cbv}$ and $T_{cbn}$ such that:

* any call-by-value $\lambda$-calculus reduction sequence $t \rightarrow^{*}_w t'$ with $n$ steps and space cost $c$ is simulated by the machine $T_{cbv}$ simulates in time polynomial in $n$ and $|t|$, and space cost proportional to $c$;

* any call-by-name $\lambda$-calculus reduction sequence $t \rightarrow^{*}_w t'$ with $n$ steps and space cost $c$ is simulated by the machine $T_{cbn}$ in time polynomial in $n$ and $|t|$, and space cost proportional to $c$.
# 6 Discussion

In this paper we provide a simple implementation model for the weak $\lambda$-calculus, which is time- and space-invariant under both the call-by-name and the call-by-value strategies.

## 6.1 Other weak strategies

*Call-by-value.* In the body of the paper, we chose a right-to-left direction for call-by-value evaluation. This direction has nothing special, and the same results would hold as well for left-to-right call-by-value. The choice of a direction does not even need to be uniform. However our invariance proof relies on the fact that $\rightarrow_{ls}$-steps are restricted to the steps that contribute to the next $\rightarrow_{s\beta}$ or $\rightarrow_{f\beta}$ step. Without this restriction, the bound on the number of substitution steps is not valid anymore.

*Size explosion.* A key element of our invariance result is that elements stored in the heap are never too big. This holds in call-by-name because an argument is never reduced before being put in the heap, and in call-by-value because an argument is reduced to a value before being put in the heap, and we never reduce inside values. In other words: in these scenarios the argument of a function is either not reduced, or fully evaluated. We show below that if we consider an arbitrary reduction sequence, that reduces partially the argument of a function, then we can produce a size explosion.

Let $(t_n)_{n \in \mathbb{N}}$ be a family of terms such that $t_0 = \lambda x.x$ and $t_n \to_w t_{n-1}$ for all $n > 0$ (for instance, $t_0 = \lambda x.x$ and $t_{n+1} = (\lambda y.t_n) (\lambda x.x)$). Then consider the families $(u_n^k)_{k,n \in \mathbb{N}}$ and $(v_n^k)_{k,n \in \mathbb{N}}$ defined by

$$ \begin{cases} u_n^0 = t_n \\ u_n^{k+1} = (\lambda x.xx) u_n^k \end{cases} \quad \begin{cases} v_n^1 = t_{n-1} \\ v_n^k = t_{n-k} v_n^1 \dots v_n^{k-1} \end{cases} $$

We have

$$ v_n^k v_n^k = (t_{n-k} v_n^1 \dots v_n^{k-1}) v_n^k \to_w t_{n-k-1} v_n^1 \dots v_n^{k-1} v_n^k = v_n^{k+1} $$

and we can prove by induction on $k$ that there is a constant $c$ such that

$$ \langle u_n^k | \emptyset \rangle \rightarrow^{ck} \langle v_n^k v_n^k | \emptyset \rangle $$

This means that we produced a configuration of exponential size in a linear number of steps.

*Call-by-need.* The call-by-need strategy cannot be expressed in the pure $\lambda$-calculus: it requires either sharing or parallel reduction. It could however be implemented in the machine, thanks to the heap, using the following ideas.

* Always apply $\rightarrow_{s\beta}$ when the argument is not already value.

* Apply $\rightarrow_{ls}$ only if the target term is a value.

* Allow reduction in the heap when the value of the stored term is needed.

In particular, reduction in the heap corresponds exactly to shared evaluation of a thunk. However, contrarily to what happens in the rest of the paper, here we store in the heap any term that is not yet evaluated, even if this means using a pointer that costs more than the shared term.

Reasoning about the invariance of our machine for this strategy is not immediate, since it would first require fixing an abstract cost model for call-by-need.

## 6.2 Relation to other machines

*The interleaving machine* [13]. Our machine obviously has the same goal as the interleaving machine presented in [13]. It also shares the idea of having two reduction modes: substitution-based and heap-based. However, while the interleaving machine keeps the two modes separate under the form of two distinct submachines that run in alternation and do not share any of their work, we
integrate the two modes as two reduction rules of the same machine. This has two consequences. First, the two rules operate on the same configurations and we have only one execution thread. Second, the choice between the two modes is made locally at each step, following a criterion that explains the behaviour of the machine in a simple way.

*The Split Abstract Machine* [2]. In retrospect, the machine we know from the literature that is the closest to ours is the Split Abstract Machine [2]. This abstract machine combines local renaming environments and a global heap, which may seem quite different to our machine, but has significant similarities: the Split Abstract Machine uses a global heap in the same way as ours to store shared subterms, and the renaming implemented as the environment part of closures in [2] is isomorphic to the operation of substitution by an address performed by our shared $\beta$ rule $\rightarrow_{s\beta}$. Actually, we can derive a machine very similar to ours by applying the following operations to the Split Abstract Machine:

* replace each closure, which in this machine is a term plus a renaming environment, by the term obtained by applying the renaming;

* apply maximally garbage collection at each step;

* store a term in the global environment only when it costs more than a new address.

## 6.3 Combination with a log-sensitive machine

In [8], the authors define an abstract machine with two components: an input term and a main term, where the input part is immutable, and the main term may contain pointers to subterms of the input. By measuring space cost only on the main term, this machine allows observing sublinear space complexity, and in particular LOGSPACE. This machine in [8], and the one presented here, both seem simple enough to be merged into a single machine that would be both time- and space-invariant for a wider range of complexity classes.

We sketch such machine below. The syntax of terms is extended with a second kind of pointer $\bar{b}$, targeting the input.

$$ t ::= x \mid t \mid \lambda x.t \mid \underline{a} \mid \bar{b} $$

The pointer $\bar{b}$ is a number between 0 and the size of the input term $t_i$, and we fix a bijective correspondence between $\mathcal{P}(t_i)$ and $[0, |t_i|)$ (for instance, prefix order as the left addresses of [5], which is also the lexicographic order on positions). Write $\varphi(b)$ the position of $\mathcal{P}(t_i)$ number $b$. The cost of such a pointer is thus logarithmic in the size of the input term.

A machine configuration is now a triple $\langle t_i | t | H \rangle$ where:

* $t_i$ is the input term (read-only),

* $t$ and $H$ are the main term and the heap as in our machine.

The reduction rules are the rules from our machine, with an additional rule $\rightarrow_{\delta}$ for fetching input terms taken from [8].

$$ \begin{array}{l@{\quad}l@{\quad}l} \langle t_i | \mathcal{E}[\bar{b}] | H \rangle & \rightarrow_{\delta} & \langle t_i | \mathcal{E}[t_i | \varphi(b)] | H \rangle \\ \langle t_i | \mathcal{E}[\underline{a}] | H \rangle & \rightarrow_{\mathrm{ls}} & \langle t_i | \mathcal{E}[H(a)] | H \rangle \\ \langle t_i | t | H \rangle & \rightarrow_{\mathrm{gc}} & \langle t_i | t | H \setminus \{a\} \rangle & a \in \mathrm{dom}(H) \setminus \mathrm{addr}(\langle t | H \rangle) \\ \langle t_i | \mathcal{E}[(\lambda x.t) u] | H \rangle & \rightarrow_{\mathrm{s}\beta} & \langle t_i | \mathcal{E}[t^{(x \leftarrow \underline{a})}] | H, a \mapsto u \rangle & a \notin \mathrm{addr}(\langle \mathcal{E}[(\lambda x.t) u] | H \rangle) \\ \langle t_i | \mathcal{E}[(\lambda x.t) u] | H \rangle & \rightarrow_{\mathrm{f}\beta} & \langle t_i | \mathcal{E}[t^{(x \leftarrow u)}] | H \rangle & a \notin \mathrm{addr}(\langle \mathcal{E}[(\lambda x.t) u] | H \rangle) \end{array} $$
The space cost of a term is parameterized by two constants: the cost $c_v$ of a variable, and the cost $c_p$ of a pointer to the input.

$$ 
\begin{align*}
\|\bar{b}\|_{c_v, c_p} &= c_p \\
\|x\|_{c_v, c_p} &= c_v \\
\|t \ u\|_{c_v, c_p} &= 1 + \|t\|_{c_v, c_p} + \|u\|_{c_v, c_p} \\
\|\lambda x.t\|_{c_v, c_p} &= 1 + \|t\|_{c_v, c_p} \\
\|a\|_{c_v, c_p} &= \min(1, \lceil \log(a) \rceil)
\end{align*}
$$

Finally, the cost of a configuration is defined as

$$ \|\langle t_i | t | H \rangle\| = \|t\|_{c_v, c_p} + \|H\|_{c_v, c_p} $$

where $c_v$ is the logarithm of the number of distinct variable names in the input term $t_i$, and $c_p$ is the logarithm of the size $|t_i|$ of the input term.

By this we obtain an implementation that is time- and space-invariant for any call-by-name or call-by-value computation of logarithmic or higher space complexity, relative to number of $\beta$-steps for time, and the log-sensitive space cost from [8].

## 6.4 Open problems

*Call-by-need.* As discussed above, beyond the call-by-name and call-by-value strategies treated in the paper, our machine seems also able to implement a call-by-need evaluation strategy. However, we have not proved that this implementation was invariant.

*Strong reduction.* While our implementation model covers more than one evaluation strategy, both its definition and the proof of its invariance rely in several places either on the restriction to weak reduction, or on the absence of $\alpha$-renaming (which is a convenient consequence of weak reduction). To name a few: the model of graph of terms require that terms stored in the heap are closed; the cost model requires the cost of any variable to be bounded by an input-dependent constant; several growth lemmas require that the body of a $\lambda$-abstraction is not modify in any other manner than by substitution of a “small” term... Thus, the question of finding a time- and space-invariant implementation of a strong reduction strategy remains fully open.

## References

[1] Beniamino Accattoli. 2016. The Complexity of Abstract Machines. In Proceedings Third International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE@FSCD 2016, Porto, Portugal, 23rd June 2016 (EPTCS, Vol. 235), Horatiu Cirstea and Santiago Escobar (Eds.). 1–15. doi:10.4204/EPTCS.235.1

[2] Beniamino Accattoli and Bruno Barras. 2017. Environments and the complexity of abstract machines. In Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming, Namur, Belgium, October 09 - 11, 2017, Wim Vanhoof and Brigitte Pientka (Eds.). ACM, 4–16. doi:10.1145/3131851.3131855

[3] Beniamino Accattoli and Giulio Guerrieri. 2019. Abstract machines for Open Call-by-Value. Science of Computer Programming 184 (2019), 102275. doi:10.1016/j.scico.2019.03.002

[4] Beniamino Accattoli and Ugo Dal Lago. 2016. (Leftmost-Outermost) Beta Reduction is Invariant, Indeed. Log. Methods Comput. Sci. 12, 1 (2016). doi:10.2168/LMCS-12(1:4)2016

[5] Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. 2024. Reasonable Space for the $\lambda$-Calculus, Logarithmically. Log. Methods Comput. Sci. 20, 4 (2024). doi:10.46298/LMCS-20(4:15)2024

[6] Beniamino Accattoli and Maico Leberle. 2022. Useful Open Call-By-Need. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 216), Florin Manea and Alex Simpson (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 4:1–4:21. doi:10.4230/LIPIcs.CSL.2022.4

[7] Sanjeev Arora and Boaz Barak. 2009. Computational Complexity: A Modern Approach. Cambridge University Press.

[8] Thibaut Balabonski. 2025. A Machine-Independent, Log-Sensitive Space-Cost Measure for the Weak Lambda-Calculus. (Oct. 2025). https://hal.science/hal-05322360 working paper or preprint.
[9] Hendrik P. Barendregt. 1984. *The Lambda Calculus – Its Syntax and Semantics*. North-Holland Publishing Company, Amsterdam, revised edition.

[10] Guy E. Blelloch and John Greiner. 1995. Parallelism in Sequential Functional Languages. In *Proceedings of the seventh international conference on Functional programming languages and computer architecture, FPCA 1995, La Jolla, California, USA, June 25-28, 1995*, John Williams (Ed.). ACM, 226–237. doi:10.1145/224164.224210

[11] Alonzo Church. 1936. An Unsolvable Problem of Elementary Number Theory. *American Journal of Mathematics* 58, 2 (1936), 345–363. http://www.jstor.org/stable/2371045

[12] Alan Cobham. 1965. The Intrinsic Computational Difficulty of Functions. In *Logic, Methodology and Philosophy of Science: Proceedings of the 1964 International Congress (Studies in Logic and the Foundations of Mathematics)*, Yehoshua Bar-Hillel (Ed.). North-Holland Publishing, 24–30.

[13] Yannick Forster, Fabian Kunze, and Marc Roth. 2020. The weak call-by-value λ-calculus is reasonable for both time and space. *Proc. ACM Program. Lang.* 4, POPL (2020), 27:1–27:23. doi:10.1145/3371095

[14] Gudmund S. Frandsen and Carl Sturtivant. 1991. What is an efficient implementation of the λ-calculus?. In *Functional Programming Languages and Computer Architecture*, John Hughes (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 289–312.

[15] Juris Hartmanis and Richard E. Stearns. 1965. On the Computational Complexity of Algorithms. *Transactions of the American Mathematical Society* - TRANS AMER MATH SOC 117 (05 1965), 285–285. doi:10.2307/1994208

[16] John E. Hopcroft and Jeffrey D. Ullman. 1969. *Formal Languages and Their Relation to Automata*. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA.

[17] Ugo Dal Lago and Simone Martini. 2008. The weak lambda calculus as a reasonable machine. *Theor. Comput. Sci.* 398, 1-3 (2008), 32–50. doi:10.1016/j.tcs.2008.01.044

[18] Julia L. Lawall and Harry G. Mairson. 1996. Optimality and Inefficiency: What Isn't a Cost Model of the Lambda Calculus?. In *Proceedings of the 1996 ACM SIGPLAN International Conference on Functional Programming, ICFP 1996*, Philadelphia, Pennsylvania, USA, May 24-26, 1996, Robert Harper and Richard L. Wexelblat (Eds.). ACM, 92–101. doi:10.1145/232627.232639

[19] Christos H. Papadimitriou. 1994. *Computational Complexity*. Addison-Wesley, Reading, MA.

[20] David Sands, Jörgen Gustavsson, and Andrew Moran. 2002. Lambda Calculi and Linear Speedups. In *The Essence of Computation, Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones [on occasion of his 60th birthday] (Lecture Notes in Computer Science, Vol. 2566)*, Torben Æ. Mogensen, David A. Schmidt, and Ivan Hal Sudborough (Eds.). Springer, 60–84. doi:10.1007/3-540-36377-7_4

[21] Cees F. Slot and Peter van Emde Boas. 1985. On Tape Versus Core; an Application of Space Efficient Perfect Hash Functions to the Invariance of Space. *J. Inf. Process. Cybern.* 21, 4/5 (1985), 246–253.

[22] Alan M. Turing. 1937. Computability and λ-definability. *Journal of Symbolic Logic* 2, 4 (1937), 153–163. doi:10.2307/2268280

[23] Alan M. Turing. 1937. On Computable Numbers, with an Application to the Entscheidungsproblem. *Proceedings of the London Mathematical Society* s2-42, 1 (01 1937), 230–265. doi:10.1112/plms/s2-42.1.230 arXiv:https://academic.oup.com/plms/article-pdf/s2-42/1/230/4317544/s2-42-1-230.pdf