The Cost of Skeletal Call-By-Need, Smoothly

CbNeed was introduced together with a further optimization usually called fully lazy sharing and here rather referred to as Skeletal CbNeed (because fully lazy sharing is not really descriptive). The idea is to refine the duplication of a value $v$ so as to duplicate only the skeleton of $v$ while keeping its flesh shared, thus ending up sharing more than in ordinary call-by-need. As an example, if $v=\lambda x.\lambda y.zzx(yz)$ then the skeleton of $v$ is $\mathrm{𝚜𝚔𝚎𝚕}(v):=\lambda x.\lambda y.wx(yz)$ and its flesh is the context $\mathrm{𝚏𝚕𝚎𝚜𝚑}(v):=\mathrm{𝗅𝖾𝗍}w=zz\mathrm{𝗂𝗇}⟨\cdot ⟩$. That is, the flesh collects and removes the maximal (non-variable) sub-terms of $v$ that are free, i.e. such that none of their free variables is captured in $v$.

Skeletal CbNeed is less studied than CbNeed because it is even trickier to define, as it requires to compute the skeletal decomposition of a value (that is, the split into skeleton and flesh). Early works by Turner [40], Hughes [30], and Peyton Jones [36] focus on implementative aspects. In the last ten years or so, various works provided operational insights. Balabonski developed an impressive theoretical analysis of Skeletal CbNeed, showing the equivalence of various presentations [22] and studying the relationship with Lévy’s optimality [23]. Soon after that, Gundersen et al. showed that the atomic $\lambda$-calculus, a $\lambda$-calculus with sharing issued from deep inference technology, naturally specifies the duplication of the skeleton [29]. Next, Kesner et al. [32] merged the insights of the CbNeed LSC and the atomic $\lambda$-calculus obtaining a Skeletal CbNeed LSC, that is, a presentation at a distance of Skeletal CbNeed.

The present work extends the operational research line of Balabonski, Gundersen et al., and Kesner et al. with cost analyses of Kesner et al.’s Skeletal CbNeed LSC, aiming at closing the gap with some of the earlier implementative studies at the same time. Generally speaking, we aim at adding Skeletal CbNeed to the list of concepts covered by the theory of cost-based analyses of abstract machines and sharing mechanisms by Accattoli and co-authors [4, 10, 19, 5, 7, 27, 12, 11, 8, 15]. We provide two analyses.

The first analysis shows that in some cases Skeletal CbNeed is considerably more efficient than CbNeed. For that, we exhibit a family of $\lambda$-terms ${\{t_n\}}_{n\in \mathbb{N}}$ such that $t_n$ evaluates in $\mathrm{\Omega }(2^n)$ time and space in CbNeed, while requiring only $𝒪(n)$ space and time in Skeletal CbNeed. The literature only shows examples of single $\lambda$-terms where Skeletal CbNeed takes a few steps less than CbNeed, but never proves any asymptotic speed-up nor deals with space. Lastly, proving that our family evaluates within the given bounds requires a fine, non-trivial analysis of evaluation sequences.

The second analysis shows that Skeletal CbNeed can be implemented efficiently, with an overhead that is bi-linear, i.e. linear in both the number of $\beta$-steps and the size of the initial term. This time, the same is true for CbNeed. The insight is that computing skeletons does require additional implementative efforts, but it comes at no asymptotic price. This work was indeed triggered by showing that the operational reconstruction of the skeleton at work in Gundersen et al. [29] and Kesner et al. [32] can be implemented in linear time. Their specifications rest on side conditions about variables in sub-terms that lead to non-linear overhead, if implemented literally. In fact, the linear time reconstruction of skeletons by Shivers and Wand [39], from 2010, avoids the side conditions and pre-dates the recent works. The insightful study in [39], however, is technical and not well-known. Here we simplify it, recasting it in the context of abstract machines.

Shivers and Wand present their ideas using graph-reduction for $\lambda$-terms. They reconstruct the skeletal decomposition via a visit of the value to skeletonize seen as a graph, based on two key points:

1. 1.

   Bi-directional edges: all the edges of their graphs can be traversed in both directions. When term graphs are seen as mathematical objects, edges are often directed but the theoretical study can also look at edges in reverse. At the implementative level, however, things are different. For a parsimonious use of space, most graph-based implementations (e.g. the proof nets inspired ones in [5, 8, 20]) indeed restrict some edges to be traversed in one direction only (namely, parent to children), thus sparing some pointers. Therefore, bi-directional edges are an unusual approach, usually considered redundant.

2. 2.

   Abstractions, occurrences, and upward reconstruction: in most graphical representations, there are edges between abstractions and the occurrences of their bound variables, usually directed only from the occurrences to the abstraction. Shivers and Wand’s insight is that, with bi-directional edges, one can move from the abstraction back to the occurrences of the variable and then reconstruct the skeleton by visiting upward from the occurrences.

Shivers and Wand’s study is graph-based and low-level, interleaved with code snippets. Here, we provide a new neat presentation of their algorithm as a simple high-level rewriting system over terms, circumventing graphs and low-level details. The reformulation of their study is the main technical innovation of this paper. While the key concepts are due to Shivers and Wand, we believe that our new presentation is a notable contribution in that it allows their concepts to blossom, simplifying their study and making them more widely accessible.

We then smoothly lift the distillation-based study of CbNeed by Accattoli et al. [4] to Skeletal CbNeed, providing an abstract machines using the reloaded algorithm for skeletal decompositions as a black-box. The new abstract machine is then shown to be implementable within a bi-linear overhead, completing the second analysis.

The overall insight is that the apparently linear space inefficiency of adding pointers for bi-directional traversals of terms/graphs enables optimizations – namely, skeletal duplications – that can bring, in some cases, exponential speed-ups for both time and space.

We provide an OCaml implementation of the abstract machine, and in particular of the reloaded skeleton reconstruction algorithm it rests upon. The implementation is there to validate the complexity analyses, as well as to integrate the low-level aspect of Shivers and Wand’s study. The implementation is discussed in Appendix A.

A long version with proofs in the Appendix is on arXiv [18].

The set of terms of the $\lambda$-calculus is noted $\mathrm{\Lambda }$. The CbNeed LSC is defined in Fig. 1. The set of terms of the CbNeed LSC is noted ${\mathrm{\Lambda }}_{\mathrm{𝚎𝚜}}$. They add explicit substitutions $t[x\leftarrow u]$ (shortened to ESs) to $\lambda$-terms, that is a more compact notation for $\mathrm{𝗅𝖾𝗍}x=u\mathrm{𝗂𝗇}t$, but where the order of evaluation between $t$ and $u$ is a priori not fixed; evaluation contexts shall fix it. The set $\mathrm{𝚏𝚟}(t)$ of free variables is defined as expected, in particular, $\mathrm{𝚏𝚟}(t[x\leftarrow u]):=(\mathrm{𝚏𝚟}(t)\setminus \{x\})\cup \mathrm{𝚏𝚟}(u)$. Both $\lambda x.t$ and $t[x\leftarrow u]$ bind $x$ in $t$, and terms are identified up to $\alpha$-renaming. A term $t$ is closed if $\mathrm{𝚏𝚟}(t)=\mathrm{\varnothing }$, open otherwise. Meta-level capture-avoiding substitution is noted $t\{x\leftarrow u\}$. The size $|t|$ of $t$ is the number of its constructs.

Note that values are only abstractions; this choice is standard in the literature on CbNeed. Note that, moreover, their bodies are $\lambda$-terms without ESs. This is in order to avoid dealing with calculating the skeleton of ESs in the next section. It is a harmless choice because evaluation (that creates ESs) never enters inside abstractions.

Contexts are terms with exactly one occurrence of the hole $⟨\cdot ⟩$, an additional constant, standing for a removed sub-term. We shall heavily use two notions of contexts: substitution contexts $S$, that are lists of ESs, and evaluation contexts $E$.

The main operation about contexts is plugging $E⟨t⟩$ where the hole $⟨\cdot ⟩$ in context $E$ is replaced by $t$. Plugging, as usual with contexts, can capture variables; for instance $((⟨\cdot ⟩t)[x\leftarrow u])⟨x⟩=(xt)[x\leftarrow u]$. We write $E⟨⟨t⟩⟩$ when we want to stress that the context $E$ does not capture the free variables of $t$.

The reduction rules of the CbNeed LSC are slightly unusual as they use contexts both to allow one to reduce redexes located in sub-terms (via evaluation contexts $E$), which is standard, and to define the redexes themselves (via both substitution $S$ and evaluation contexts $E$), which is less standard. This approach is called at a distance and related to cut-elimination on proof nets; see Accattoli [2, 3] for the link with proof nets. The notion of evaluation context $E$ used for CbNeed is exactly the one by Ariola et al. [21], that extend call-by-name evaluation contexts with the production $E⟨⟨x⟩⟩[x\leftarrow E^{\prime }]$, which – by enterings ESs – is what enables the memoization aspect of CbNeed.

The distant beta rule ${\mapsto }_{\mathrm{𝚍𝙱}}$ is essentially the $\beta$-rule, except that the argument goes into a new ES, rather then being immediately substituted, and that there can be a substitution context $S$ in between the abstraction and the argument. Example: $(\lambda x.y)[y\leftarrow t]u{\mapsto }_{𝚖}y[x\leftarrow u][y\leftarrow t]$. One with on-the-fly $\alpha$-renaming is $(\lambda x.y)[y\leftarrow t]y{\mapsto }_{𝚖}z[x\leftarrow y][z\leftarrow t]$.

The linear substitution rule by need ${\mapsto }_{\mathrm{𝚗𝚍}\cdot \mathrm{𝚕𝚜}}$ replaces a single variable occurrence by a copy of the value in the ES, commuting the substitution context around the value (if any) out of the ES. Example: $(xx)[x\leftarrow 𝙸[y\leftarrow t]]{\mapsto }_{\mathrm{𝚗𝚍}\cdot \mathrm{𝚕𝚜}}(𝙸x)[x\leftarrow 𝙸][y\leftarrow t]$.

The use of substitution contexts $S$ in the root rules is what allows one to avoid the two commuting rules of Ariola et al. [21], namely (rephrasing their $\mathrm{𝗅𝖾𝗍}$-expressions as ESs) $t[x\leftarrow s]u{\mapsto }_{let\text{-}C}(tu)[x\leftarrow s]$ and $t[y\leftarrow u[x\leftarrow s]]{\mapsto }_{let\text{-}A}t[y\leftarrow u][x\leftarrow s]$.

The two root rules ${\mapsto }_{\mathrm{𝚍𝙱}}$ and ${\mapsto }_{\mathrm{𝚗𝚍}\cdot \mathrm{𝚕𝚜}}$ are then closed by evaluation contexts $E$. In Fig. 1, we use the compact notation ${\to }_{\mathrm{𝚍𝙱}}:=ℰ⟨{\mapsto }_{\mathrm{𝚍𝙱}}⟩$ to denote that ${\to }_{\mathrm{𝚍𝙱}}$ is defined as $E⟨t⟩{\to }_{\mathrm{𝚍𝙱}}E⟨u⟩$ if $t{\mapsto }_{\mathrm{𝚍𝙱}}u$, and similarly for the other rule.

Extractable sub-terms are called free sub-terms, defined next. We actually need a parametrized notion of free sub-term, which is relative to a set of variables $𝚅$ that are supposed not to occur in the sub-term.

The skeletal decomposition of a term $t$ is the splitting of $t$ into its maximal free sub-terms on one side, collected as a substitution context $S$ called the flesh, and what is left of $t$ after the removal, that is, its skeleton. As for free sub-terms, we rather define parametrized notions of skeletal decomposition and skeleton. Then, we specialize the definitions for values.

We adopt the presentation of skeletal CbNeed by Kesner et al. [32] (refered to as fully lazy CbNeed by them), that adds a new skeletal (explicit) substitution $t⟨x\leftarrow v⟩$ containing skeletal values, that is, values that are equal to their skeleton. The language of terms and the strategy is defined in Fig. 2. The new set of terms is noted ${\mathrm{\Lambda }}_{\mathrm{𝚜𝚔}}$.

Notation: when we need to treat explicit and skeletal substitution together, we use the notation $[[x\leftarrow t]]$, which stands for either $[x\leftarrow t]$ or (with a slight abuse) $⟨x\leftarrow v⟩$.

The CbNeed substitution rule ${\to }_{\mathrm{𝚗𝚍}\cdot \mathrm{𝚕𝚜}}$ for a redex $E⟨⟨x⟩⟩[x\leftarrow S⟨v⟩]$ is refined via two rules. The first skeletonization rule ${\to }_{\mathrm{𝚜𝚔}}$ does three further mini tasks at once: firstly, it decomposes $v$ in its skeleton $v^{\prime }$ and its flesh $S^{\prime }$ (thus obtaining $E⟨⟨x⟩⟩[x\leftarrow S⟨S^{\prime }⟨v⟩⟩]$); secondly, it re-organizes the term commuting $S$ and $S^{\prime }$ out of the ES (obtaining $S⟨S^{\prime }⟨E⟨⟨x⟩⟩[x\leftarrow v^{\prime }]⟩⟩$); thirdly, it turns the ES into a skeletal substitutions, finally producing $S⟨S^{\prime }⟨E⟨⟨x⟩⟩⟨x\leftarrow v^{\prime }⟩⟩⟩$.

The second skeletal substitution rule ${\to }_{\mathrm{𝚜𝚜}}$ simply replaces $x$ with $v^{\prime }$.

Note that evaluation contexts $E$ are adapted to include skeletal substitutions, but that they do not enter inside them, since their content is always a value. The distant $\beta$ rule for Skeletal CbNeed is noted ${\to }_{\mathrm{𝚜𝚔}\cdot \mathrm{𝚍𝙱}}$ to distinguish it from the one for CbNeed. The Skeletal CbNeed reduction ${\to }_{\mathrm{𝚜𝚔}\cdot \mathrm{𝚗𝚎𝚎𝚍}}$ is the union of ${\to }_{\mathrm{𝚜𝚔}\cdot \mathrm{𝚍𝙱}}$, ${\to }_{\mathrm{𝚜𝚔}}$, and ${\to }_{\mathrm{𝚜𝚜}}$.

The next proposition is an easy adaptation of the one for CbNeed in Accattoli et al. [4].

To study the relationship with abstract machines, we shall need the concept of structural equivalence, defined in Fig. 3. The concept is standard for $\lambda$-calculi with ESs at a distance, and it also standard to use it in relationship with abstract machines, as systematically done by Accattoli et al. [4]. Intuitively, structural equivalence allows one to move explicit/skeletal substitutions around because the move does not change the behaviour of the term. This fact is captured by the following strong bisimulation property, proved by an immediate adaptation of the similar property in [4].

There is a small difference between our definition of Skeletal CbNeed and Kesner et al.’s, namely in the definition of skeletons. For us, the skeletal decomposition of, say, $v:=\lambda x.yx(zz)$ is $(\lambda x.yxw,⟨\cdot ⟩[w\leftarrow zz])$, while for them it is $(\lambda x.y^{\prime }xw,⟨\cdot ⟩[y^{\prime }\leftarrow y][w\leftarrow zz])$, that is, they flesh-out also single variable occurrences while we do not, obtaining a slightly more parsimonious decomposition.

This difference, however, has essentially no impact on the theory, nor on the asymptotic costs. In particular, the operational equivalence of Skeletal CbNeed with respect to CbNeed and CbN is preserved. The proof of Kesner et al., indeed, works for all decompositions such that substituting the flesh into the skeleton recovers the original value; our decomposition has this property. Therefore, we can import the following result.

We shall use the abbreviations $𝙸:=\lambda x.x$ and $\gamma :=\lambda y.\lambda z.y𝙸(y𝙸)z$. Next, we define an auxiliary family ${\{u_n\}}_{n\in \mathbb{N}}$ as follows: $u_0:=𝙸$ and $u_{n+1}:=\gamma u_n$. Lastly, the actual family is defined as $t_n:=(\lambda x.x𝙸(x𝙸))u_n$.

Our result is that the term $t_n$ evaluates in $𝒪(n)$ ${\to }_{\mathrm{𝚜𝚔}\cdot \mathrm{𝚍𝙱}}$-steps (namely $6n+4$ steps) with skeletal CbNeed and $\mathrm{\Omega }(2^n)$ ${\to }_{\mathrm{𝚍𝙱}}$-steps (namely $8\times 2^n+n-4$ steps) with CbNeed. This is shown via quite technical statements. Firstly, note that $t_n{\to }_{\mathrm{𝚍𝙱}}(x𝙸(x𝙸))[x\leftarrow u_n]$; it is actually for $(x𝙸(x𝙸))[x\leftarrow u_n]$ that we shall prove bounds. These bounds are expressed stating that there are families of evaluation contexts $S_n^{\mathrm{𝚗𝚍}}$ and $S_n^{\mathrm{𝚜𝚔}}$ (one for CbNeed and one for Skeletal CbNeed) such that $(x𝙸(x𝙸))[x\leftarrow u_n]$ reduces to $S_n^{\mathrm{𝚗𝚍}}⟨𝙸⟩$ and $S_n^{\mathrm{𝚜𝚔}}⟨𝙸⟩$ (which is a normal form in both cases) in $6n+3$ and $8\times 2^n+n-3$ steps respectively. The results about space are obtained by showing that $S_n^{\mathrm{𝚗𝚍}}$ has size exponential in $n$, while $S_n^{\mathrm{𝚜𝚔}}$ is linear in $n$.

The skeletal case is, perhaps surprisingly, the easiest case for which one can find an inductive invariant leading to the bound.

For the non-skeletal case, the bound is formulated via two families of substitution contexts. For $n\in \mathbb{N}$, the first family is given by $S_0:=⟨\cdot ⟩[x_0\leftarrow 𝙸]$ and $S_{n+1}:=S_n⟨⟨\cdot ⟩[x_{n+1}\leftarrow s_{n+1}]⟩$ with $s_{n+1}:=\lambda y_n.x_n𝙸(x_n𝙸)y_n$. The second family $S_n^{\mathrm{𝚗𝚍}}$ is defined in the proof of the lemma, itself relying on an auxiliary lemma in the technical report [18]. The statement is parametrized by an evaluation context $E$ for the induction to go through, but the relevant case is the one with $E$ empty.

The next statement sums up the results, and is based on the result at the end of the paper stating that Skeletal CbNeed can be implemented in bilinear time, that is, linear in the size $|t_n|$ of the initial term and in the number of $\mathrm{𝚜𝚔}\cdot \mathrm{𝚍𝙱}$ steps (Theorem 31).

• $\mathrm{■}$

  For CbNeed, by Lemma 7 there is an evaluation sequence:

  $$t_n=(\lambda x.x𝙸(x𝙸))u_n{\to }_{\mathrm{𝚍𝙱}}(x𝙸(x𝙸))[x\leftarrow u_n]{\to }_{\mathrm{𝚗𝚎𝚎𝚍}}^{\ast }{S}_n⟨S_n^{\mathrm{𝚗𝚍}}⟨𝙸⟩⟩$$

  taking $k_n:=8\times 2^n+n-4=\mathrm{\Omega }(2^n)$ $\mathrm{𝚍𝙱}$-steps and such that $|S_n^{\mathrm{𝚗𝚍}}|=\mathrm{\Omega }(2^n)$.

• $\mathrm{■}$

  For Skeletal CbNeed, by Lemma 6 there is an evaluation sequence:

  $$t_n=(\lambda x.x𝙸(x𝙸))u_n{\to }_{\mathrm{𝚜𝚔}\cdot \mathrm{𝚍𝙱}}(x𝙸(x𝙸))[x\leftarrow u_n]{\to }_{\mathrm{𝚜𝚔}\cdot \mathrm{𝚗𝚎𝚎𝚍}}^{\ast }{S}_n^{\mathrm{𝚜𝚔}}⟨𝙸⟩$$

  taking $k_n:=6n+4=𝒪(n)$ $\mathrm{𝚜𝚔}\cdot \mathrm{𝚍𝙱}$-steps and such that $|S_n^{\mathrm{𝚜𝚔}}|=𝒪(n)$. Note that the calculus has no garbage collection rule, so the size of terms diminishes only by $\mathrm{𝚜𝚔}\cdot \mathrm{𝚍𝙱}$ steps, and of a constant amount (a $\mathrm{𝚜𝚔}\cdot \mathrm{𝚍𝙱}$ step removes two constructs and adds one). Therefore, the maximum size of terms is bounded by the size of the final term plus the number of steps. That is, the space cost is $𝒪(n)$.

$◀$

Marked terms and contexts are defined in Fig. 4. The idea is to incrementally mark with a tag $\circ$ the constructs belonging to the skeleton during a visit of the term which is allowed to jump from an abstraction to the occurrences of the variables, since these are usually connected in a graphical representation.

Constructs of the $\lambda$ calculus are then either the usual ones (referred to as unmarked) or marked with $\circ$, which means that the constructor is part of the skeleton. Additionally, there is an extra up construct ${\overline{t}}^{\Uparrow }$ that shall be used to indicate the frontier of the visit of the term.

In the marked setting, we can recast skeletal decompositions by marking as white the constructs belonging to the skeleton and leaving unmarked all the constructs of the flesh.

Example: for $v:=\lambda x.\lambda y.zzx(yz)$, one has $\mathrm{𝚖𝚜𝚔𝚎𝚕}(v)={\lambda }^{\circ }x.{\lambda }^{\circ }y.(zz)\circ x^{\circ }\circ (y^{\circ }\circ z)$.

Next, we turn marked skeletons into skeletal decompositions, by extracting unmarked sub-terms and turning them into the flesh, while removing the marks from the skeleton. We shall do this via a splitting function, defined below, which operates on (parametrized) marked skeletons. For that, we give a lemma guaranteeing that the unmarked sub-terms of marked skeletons can be recognized from their top constructor, that is in $𝒪(1)$, thus removing the need to inspect them.

The lemma implies the correctness of the first clause of the following definition, as it ensures that in that case $m$ has no marks.

Example: $\mathrm{𝚜𝚙𝚕𝚒𝚝}({\lambda }^{\circ }x.{\lambda }^{\circ }y.(zz)\circ x^{\circ }\circ (y^{\circ }\circ z))=(\lambda x.\lambda y.wx(yz),⟨\cdot ⟩[w\leftarrow zz])$.

We can now prove that the marked notions allow one to retrieve the standard ones.

We shall now define a parallel algorithm for computing the marked skeleton via a rewriting system on marked terms. The definition is in Fig. 5. The algorithm shall be applied to abstractions, say to $\lambda x.t$. The algorithm is described by inserting the up symbols $\Uparrow$, denoting where the algorithm is operating, and propagating through the term. At the beginning, there is exactly one $\Uparrow$, as the algorithm starts on $\lambda x.{\overline{t}}^{\Uparrow }$.

The algorithm has two sets of rules. Propagation rules turn the encountered unmarked constructs into marked ones. The interesting rule is ${\to }_{\mathrm{𝚙𝚛}3}$ for abstractions, that is also the very first one to be applied on the initial term $\lambda x.{\overline{t}}^{\Uparrow }$. Its effect is that $\lambda x$ is marked as ${\lambda }^{\circ }x$ and all the occurrences of $x$ in $t$ are also marked, obtaining ${\lambda }^{\circ }x.t\{x\leftarrow x^{\circ }\}$; this is how we recast the role played by Shivers and Wand’s bi-directional edges connecting abstractions and variables. Essentially, propagation rules move $\Uparrow$ upwards but they also add $\Uparrow$ at the bottom of the syntax tree on the variable occurrences associated to marked abstractions.

Absorption rules, instead, remove the $\Uparrow$ symbol when it encounters a marked construct, as it means that the concerned thread of the algorithm is passing where another thread already passed before, thus the concerned thread becomes redundant and can be terminated.

Intuitively, the set of $\Uparrow$-sub-terms is the frontier of where the parallel algorithm is operating. When the algorithm is over, no internal node is marked with $\Uparrow$.

The algorithm is parallel in that the initial substitution $t\{x\leftarrow x^{\circ }\}$ and rule ${\mapsto }_{\mathrm{𝚙𝚛}3}$ might introduce many occurrences of $\Uparrow$, which can be propagated independently.

As an example, consider $v:=\lambda x.\lambda y.zzx(yz)$, for which one has, for instance:

1. 1.

   Strong normalization. Let $m$ be a marked term. As terminating measure, consider $({|m|}_{\neg \circ },{|m|}_{\Uparrow })$ where ${|m|}_{\neg \circ }$ and ${|m|}_{\Uparrow }$ are the number of unmarked and $\Uparrow$ constructs in $m$. Note that the propagation rules decrease ${|m|}_{\neg \circ }$ while the absorption rules decrease ${|m|}_{\Uparrow }$ and leave ${|m|}_{\neg \circ }$ unchanged. Then ${\to }_{\mathrm{𝚊𝚕𝚐}}$ is strongly normalizing.

2. 2.

   Diamond. We prove the diamond property, which implies confluence. Clearly, redexes cannot duplicate or erase each other. There are only two critical pairs, namely:

$◀$

To state the correctness of the algorithm and give a bound on the number of its steps, we need two definitions.

The following lemma is the key step in the proof of correctness of the algorithm. It is a technical lemma, the statement of which is more easily understood by looking at the proof of the following theorem.

By definition $\mathrm{𝗂𝗇𝗂𝗍}(\lambda x.t)=\lambda x.{\overline{t}}^{\Uparrow }{\to }_{\mathrm{𝚙𝚛}3}{\overline{{\lambda }^{\circ }x.t\{x\leftarrow {\overline{x^{\circ }}}^{\Uparrow }\}}}^{\Uparrow }={\overline{{\lambda }^{\circ }x.{\mathrm{𝚖𝚜𝚔𝚎𝚕}}^{\mathrm{\varnothing }}(t)\{x\leftarrow {\overline{x^{\circ }}}^{\Uparrow }\}}}^{\Uparrow }$, while $\mathrm{𝚖𝚜𝚔𝚎𝚕}(\lambda x.t)={\lambda }^{\circ }x.{\mathrm{𝚖𝚜𝚔𝚎𝚕}}^{\{x\}}(t)$. We consider two cases.

• $\mathrm{■}$

  Case $x\mathbf{\notin }\mathrm{𝚏𝚟}\mathbf{(}t\mathbf{)}$. Then ${\mathrm{𝚖𝚜𝚔𝚎𝚕}}^{\{x\}}(t)=t$ and $t\{x\leftarrow {\overline{x^{\circ }}}^{\Uparrow }\}=t$, so ${\lambda }^{\circ }x.t\{x\leftarrow {\overline{x^{\circ }}}^{\Uparrow }\}={\lambda }^{\circ }x.t={\lambda }^{\circ }x.{\mathrm{𝚖𝚜𝚔𝚎𝚕}}^{\{x\}}(t)=\mathrm{𝚖𝚜𝚔𝚎𝚕}(\lambda x.t)$. Thus, $\mathrm{𝗂𝗇𝗂𝗍}(\lambda x.t){\to }_{\mathrm{𝚙𝚛}3}{\overline{\mathrm{𝚖𝚜𝚔𝚎𝚕}(\lambda x.t)}}^{\Uparrow }$. Moreover, $n=1=|\mathrm{𝚖𝚜𝚔𝚎𝚕}(\lambda x.t){|}_{\circ }$, since the only white construct of $\mathrm{𝚖𝚜𝚔𝚎𝚕}(\lambda x.t)$ is the root abstraction.

• $\mathrm{■}$

  Case $x\mathbf{\in }\mathrm{𝚏𝚟}\mathbf{(}t\mathbf{)}$. By Lemma 15, ${\lambda }^{\circ }x.t\{x\leftarrow {\overline{x^{\circ }}}^{\Uparrow }\}{\to }_{\mathrm{𝚊𝚕𝚐}}^k{\lambda }^{\circ }x.{\overline{{\mathrm{𝚖𝚜𝚔𝚎𝚕}}^{\{x\}}(t)}}^{\Uparrow }$, where $k={|{\mathrm{𝚖𝚜𝚔𝚎𝚕}}^{\{x\}}(t)|}_{\circ }-{|t|}_{\circ }-1={|{\mathrm{𝚖𝚜𝚔𝚎𝚕}}^{\{x\}}(t)|}_{\circ }-1$. Therefore:

  Now, $n=k+2=|{\mathrm{𝚖𝚜𝚔𝚎𝚕}}^{\{x\}}(t){|}_{\circ }-1+2=|{\mathrm{𝚖𝚜𝚔𝚎𝚕}}^{\{x\}}(t){|}_{\circ }+1=|\mathrm{𝚖𝚜𝚔𝚎𝚕}(\lambda x.t){|}_{\circ }$.

$◀$

Abstract machines manipulate pre-terms, that is, terms without implicit $\alpha$-renaming. In this paper, an abstract machine is a quadruple $𝙼=(\mathrm{𝚂𝚝𝚊𝚝𝚎𝚜},\rightsquigarrow ,\cdot ⊲\cdot ,\underset{¯}{\cdot })$ the components of which are as follows.

• $\mathrm{■}$

  States. A state $𝚀\in \mathrm{𝚂𝚝𝚊𝚝𝚎𝚜}$ is a quadruple $(𝙲,t,𝚂,𝙴)$ composed by the active term $t$, plus three data structure, namely the chain $𝙲$, the (applicative) stack $𝚂$, and the (global) environment $𝙴$. Terms in states are actually pre-terms.

• $\mathrm{■}$

  Transitions. The pair $(\mathrm{𝚂𝚝𝚊𝚝𝚎𝚜},\rightsquigarrow )$ is a transition system with transitions $\rightsquigarrow$ partitioned into principal transitions, whose union is noted ${\rightsquigarrow }_{\mathrm{𝚙𝚛}}$ and that are meant to correspond to steps on the calculus, and search transitions, whose union is noted ${\rightsquigarrow }_{\mathrm{𝚜𝚎𝚊}}$, that take care of searching for (principal) redexes.

• $\mathrm{■}$

  Initialization. The component $⊲\subseteq \mathrm{\Lambda }\times \mathrm{𝚂𝚝𝚊𝚝𝚎𝚜}$ is the initialization relation associating closed terms without ESs to initial states. It is a relation and not a function because $t⊲𝚀$ maps a closed $\lambda$-term $t$ (considered modulo $\alpha$) to a state $𝚀$ having a pre-term representant of $t$ (which is not modulo $\alpha$) as active term. Intuitively, any two states $𝚀$ and ${𝚀}^{\prime }$ such that $t⊲𝚀$ and $t⊲{𝚀}^{\prime }$ are $\alpha$-equivalent. A state $𝚀$ is reachable if it can be reached starting from an initial state, that is, if ${𝚀}^{\prime }{\rightsquigarrow }^{\ast }𝚀$ where $t⊲{𝚀}^{\prime }$ for some $t$ and ${𝚀}^{\prime }$, shortened as $t⊲{𝚀}^{\prime }{\rightsquigarrow }^{\ast }𝚀$.

• $\mathrm{■}$

  Read-back. The read-back function $\underset{¯}{\cdot }:\mathrm{𝚂𝚝𝚊𝚝𝚎𝚜}\to \mathrm{𝚃𝚎𝚛𝚖𝚜}$ turns reachable states into terms (possibly with ESs, that is, $\mathrm{𝚃𝚎𝚛𝚖𝚜}={\mathrm{\Lambda }}_{\mathrm{𝚎𝚜}}$ or $\mathrm{𝚃𝚎𝚛𝚖𝚜}={\mathrm{\Lambda }}_{\mathrm{𝚜𝚔}}$) and satisfies the initialization constraint: if $t⊲𝚀$ then $\underset{¯}{𝚀}{=}_{\alpha }t$.

A state is final if no transitions apply. A run $r:𝚀{\rightsquigarrow }^{\ast }{𝚀}^{\prime }$ is a possibly empty finite sequence of transitions, the length of which is noted $|r|$; note that the first and the last states of a run are not necessarily initial and final. If $a$ and $b$ are transitions labels (that is, ${\rightsquigarrow }_a\subseteq \rightsquigarrow$ and ${\rightsquigarrow }_b\subseteq \rightsquigarrow$) then ${\rightsquigarrow }_{a,b}:={\rightsquigarrow }_a\cup {\rightsquigarrow }_b$ and ${|r|}_a$ is the number of $a$ transitions in $r$, ${|r|}_{a,b}:={|r|}_a+{|r|}_b$, and similarly for more than two labels.

For the machines at work in this paper, the pre-terms in initial states shall be well-bound, that is, they have pairwise distinct bound names; for instance $(\lambda x.x)\lambda y.y$ is well-bound while $(\lambda x.x)\lambda x.x$ is not. We shall also write $t^{\alpha }$ in a state $𝚀$ for a fresh well-bound renaming of $t$, i.e. $t^{\alpha }$ is $\alpha$-equivalent to $t$, well-bound, and its bound variables are fresh with respect to those in $t$ and in the other components of $𝚀$.

Machines are usually showed to be correct with respect to a strategy via some form of bisimulation relating terms and machine states. The notion that we adopt is here dubbed mechanical bisimulation, and it should not be confused with the strong bisimulation property of structural equivalence (which actually plays a role in mechanical bisimulations). The definition, tuned towards complexity analyses, requires a perfect match between the steps of the evaluation sequence and the principal transitions of the machine run. Terminology: a structural strategy $({\to }_{\mathrm{𝚜𝚝𝚛}},\equiv )$ is a strategy ${\to }_{\mathrm{𝚜𝚝𝚛}}$ plus a relation $\equiv$ that is a strong bisimulation with respect to ${\to }_{\mathrm{𝚜𝚝𝚛}}$ (see Prop. 4).