Crumbling Abstract Machines

TL;DR

This paper investigates how sharing-based term representations in lambda-calculus influence the design and efficiency of call-by-value abstract machines, demonstrating no slowdown and scalability to open terms.

Contribution

It introduces a sharing-based term representation that simplifies machine design and proves it scales efficiently to open terms, unlike continuation-passing style transformations.

Findings

No slowdown in evaluation performance.

Simplifies abstract machine design by removing environment structures.

Scales effectively to open terms used in proof assistants.

Abstract

Extending the lambda-calculus with a construct for sharing, such as let expressions, enables a special representation of terms: iterated applications are decomposed by introducing sharing points in between any two of them, reducing to the case where applications have only values as immediate subterms. This work studies how such a crumbled representation of terms impacts on the design and the efficiency of abstract machines for call-by-value evaluation. About the design, it removes the need for data structures encoding the evaluation context, such as the applicative stack and the dump, that get encoded in the environment. About efficiency, we show that there is no slowdown, clarifying in particular a point raised by Kennedy, about the potential inefficiency of such a representation. Moreover, we prove that everything smoothly scales up to the delicate case of open terms, needed to implement proof assistants. Along the way, we also point out that continuation-passing style transformations--that may be alternatives to our representation--do not scale up to the open case.

Tables

Table 1. Table 1 . Data structures

⬇ type var = { dummy : unit } type node = { mutable content : term ; mutable copying : bool ; mutable prev : node option } and env = (node * node) option and crumblep = term * env and term = | Err | True | False | Var of var | Lam of var * crumblep | App of term * term | IfThenElse of term * crumblep * crumblep | Shared of node let mk_node content = { content ; copying = false ; prev = None } let push n e = n.prev <- Some e

Equations

$$(w^{\prime \prime }y)[w^{\prime \prime }\text{shortleftarrow}{w}^{\prime }w][w^{\prime }\text{shortleftarrow}(\lambda x.(x{x}^{\prime })[x^{\prime }\text{shortleftarrow}xx])y][w\text{shortleftarrow}(\lambda z.z)y]$$

$$s[x\text{shortleftarrow}(\mathsf{if}v\mathsf{then}t\mathsf{else}u)]\to \mathsf{if}v\mathsf{then}(s[x\text{shortleftarrow}t])\mathsf{else}(s[x\text{shortleftarrow}u])$$

$$\mathsf{if}true\mathsf{then}((x+1)[x\text{shortleftarrow}0])\mathsf{else}(\underline{(x+1)[x\text{shortleftarrow}\text{false}]})$$

$$\begin{array}[]{rcllllll}t&\rightarrow_{{\beta_{v}}}&((\lambda y.yy)I)(II)&\rightarrow_{{\beta_{v}}}&((\lambda y.yy)I)I\\ &\rightarrow_{{\beta_{v}}}&(II)I&\rightarrow_{{\beta_{v}}}&II&\rightarrow_{{\beta_{v}}}&I\end{array}$$

$$\underline{t}$$

$$\begin{array}[]{llllllllll}\underline{t}&\rightarrow_{{\beta_{v}}}&\lx@intercol(wz)[w{\shortleftarrow}(\lambda y.yy)I][z{\shortleftarrow}xI][x{\shortleftarrow}I]\hfil\lx@intercol\\ &\rightarrow_{[\ ]}&\lx@intercol(wz)[w{\shortleftarrow}(\lambda y.yy)I][z{\shortleftarrow}II]\hfil\lx@intercol\\ &\rightarrow_{{\beta_{v}}}&\lx@intercol(wz)[w{\shortleftarrow}(\lambda y.yy)I][z{\shortleftarrow}I]\hfil\lx@intercol\\ &\rightarrow_{[\ ]}&(wI)[w{\shortleftarrow}(\lambda y.yy)I]\par&\rightarrow_{{\beta_{v}}}&(wI)[w{\shortleftarrow}II]\\ &\rightarrow_{{\beta_{v}}}&(wI)[w{\shortleftarrow}I]&\rightarrow_{[\ ]}&II\ \ \ \ \rightarrow_{{\beta_{v}}}\ \ \ \ I\end{array}$$

$$\small\begin{array}[]{llll}(wz)[w{\shortleftarrow}(\lambda y.yy)I]&\rightarrow_{{\beta_{v}}}&(wz)[w{\shortleftarrow}yy][y{\shortleftarrow}I]&\rightarrow_{[\ ]}\\ (wz)[w{\shortleftarrow}yI][y{\shortleftarrow}I]&\rightarrow_{[\ ]}&(wz)[w{\shortleftarrow}II][y{\shortleftarrow}I]&\rightarrow_{{\beta_{v}}}\\ (wz)[w{\shortleftarrow}x][x{\shortleftarrow}I][y{\shortleftarrow}I]&\rightarrow_{[\ ]}&(wz)[w{\shortleftarrow}I][x{\shortleftarrow}I][y{\shortleftarrow}I]&\rightarrow_{[\ ]}\\ (Iz)[w{\shortleftarrow}I][x{\shortleftarrow}I][y{\shortleftarrow}I]\end{array}$$

$$\underline{u}=((\lambda x.((yz)[y\text{shortleftarrow}xx][z\text{shortleftarrow}xx]))w)[w\text{shortleftarrow}II]$$

$$(yz)[y\text{shortleftarrow}xx][z\text{shortleftarrow}xx][x\text{shortleftarrow}I][w\text{shortleftarrow}I][w^{\prime }\text{shortleftarrow}I].$$

$$\begin{array}[]{rrcl}\textsc{Bite{}s}&b,b^{\prime}&\Coloneqq&v\mid vw\mid\mathsf{if}\,v\,\mathsf{then}\,c\,\mathsf{else}\,d\\ \textsc{Crumbled values }&v,w&\Coloneqq&x\mid\lambda x.c\mid\mathsf{true}\mid\mathsf{false}\mid\mathsf{err}\\ \textsc{Environments }&e,e^{\prime}&\Coloneqq&\epsilon\mid e[x{\shortleftarrow}b]\\ \textsc{Crumble{s} }&c,d&\Coloneqq&(b,e)\end{array}$$

$$\begin{array}[]{rcl \colspace rcl}\mathsf{dom}(e[x{\shortleftarrow}b])&\coloneqq&\mathsf{dom}(e)\cup\{x\}&\mathsf{dom}(\epsilon)&\coloneqq&\emptyset\\ \mathsf{dom}((b,e))&\coloneqq&\mathsf{dom}(e)&{\sf fv}(\epsilon)&\coloneqq&\emptyset\\ {\sf fv}(e[x{\shortleftarrow}b])&\coloneqq&\lx@intercol({\sf fv}(e)\smallsetminus\{x\})\cup{\sf fv}(b)\hfil\lx@intercol\\ {\sf fv}((b,e))&\coloneqq&\lx@intercol({\sf fv}(b)\smallsetminus\mathsf{dom}(e))\cup{\sf fv}(e).\hfil\lx@intercol\end{array}$$

$$\begin{array}[]{c\colspace\colspace c\colspace\colspace c}\overline{x}\coloneqq x&\overline{\mathsf{true}}\coloneqq\mathsf{true}&\overline{\mathsf{false}}\coloneqq\mathsf{false}\\ \overline{\mathsf{err}}\coloneqq\mathsf{err}&\overline{\lambda x.t}\coloneqq\lambda x.{\underline{t}}\end{array}$$

$$\begin{array}[]{rcl\colspace\colspace c\colspace\colspace c\colspace\colspace c \colspace\colspace cccccccccc}\underline{v}&\coloneqq&(\overline{v},\epsilon)\\ \underline{vv^{\prime}}&\coloneqq&(\overline{v}\overline{v^{\prime}},\epsilon)\\ \underline{tv}&\coloneqq&(x\overline{v},[x{\shortleftarrow}b]e)&(*)\\ \underline{ut}&\coloneqq&\underline{ux}\mathrel{@}([x{\shortleftarrow}b]e)&(*)\\ \underline{\mathsf{if}\,v\,\mathsf{then}\,u\,\mathsf{else}\,s}&\coloneqq&(\mathsf{if}\,\overline{v}\,\mathsf{then}\,\underline{u}\,\mathsf{else}\,\underline{s},\epsilon)\\ \underline{\mathsf{if}\,t\,\mathsf{then}\,u\,\mathsf{else}\,s}&\coloneqq&(\mathsf{if}\,x\,\mathsf{then}\,\underline{u}\,\mathsf{else}\,\underline{s},[x{\shortleftarrow}b]e)&(*)\end{array}$$

$$\begin{array}[]{rclccc}\underline{\delta\delta I}&=&(z\overline{I},[z{\shortleftarrow}\bar{\delta}\bar{\delta}])\\ &=&(z\lambda x.{(x,\epsilon)},[z{\shortleftarrow}(\lambda x.{(xx,\epsilon)})\lambda x.{(xx,\epsilon)}])\\[5.69046pt] \underline{\delta\delta(xx)}&=&(zw,[z{\shortleftarrow}\bar{\delta}\bar{\delta}][w{\shortleftarrow}xx])\\ &=&(zw,[z{\shortleftarrow}(\lambda x.{(xx,\epsilon)})\lambda x.{(xx,\epsilon)}][w{\shortleftarrow}xx]).\end{array}$$

$$\begin{array}[]{rcl\colspace\colspace rcl}x_{\downarrow}&\coloneqq&x&(\lambda x.{c})_{\downarrow}&\coloneqq&\lambda x.{c_{\downarrow}}\\ \mathsf{true}_{\downarrow}&\coloneqq&\mathsf{true}&\mathsf{false}_{\downarrow}&\coloneqq&\mathsf{false}\\ \mathsf{err}_{\downarrow}&\coloneqq&\mathsf{err}&(vw)_{\downarrow}&\coloneqq&v_{\downarrow}w_{\downarrow}\\ (\mathsf{if}\,v\,\mathsf{then}\,c\,\mathsf{else}\,d)_{\downarrow}&\coloneqq&\lx@intercol\mathsf{if}\,v_{\downarrow}\,\mathsf{then}\,c_{\downarrow}\,\mathsf{else}\,d_{\downarrow}\hfil\lx@intercol\\ (b,\epsilon)_{\downarrow}&\coloneqq&b_{\downarrow}\\ (b,e{[x{\shortleftarrow}b^{\prime}]})_{\downarrow}&\coloneqq&\lx@intercol(b,e)_{\downarrow}\{x{\shortleftarrow}b^{\prime}_{\downarrow}\}\hfil\lx@intercol\end{array}$$

$$E:=e[x\text{shortleftarrow}⟨\cdot ⟩]$$

$$C:=⟨\cdot ⟩\mid (b,E)$$

$$(e[x\text{shortleftarrow}⟨\cdot ⟩])⟨(b^{\prime },e^{\prime })⟩:=e[x\text{shortleftarrow}{b}^{\prime }]e^{\prime }$$

$$⟨\cdot ⟩⟨c⟩:=c(b,E)⟨c⟩:=(b,E⟨c⟩)$$

$$\begin{array}[]{lrcll}\textsc{$v$-environment{}s}&e_{v}&\Coloneqq&\epsilon\mid e_{v}[x{\shortleftarrow}v_{\neg x}]\\ \textsc{$v$-crumble{}s}&c_{v}&\Coloneqq&(v_{\neg x},e_{v})\end{array}$$

$$((\lambda x.c)v,e_v)$$

$$(\mathsf{if}\mathsf{true}\mathsf{then}c\mathsf{else}d,e_v)$$

$$(\mathsf{if}\mathsf{false}\mathsf{then}c\mathsf{else}d,e_v)$$

$$(\mathsf{if}v\mathsf{then}c\mathsf{else}d,e_v)$$

$$(vw,e_v)$$

$$(x,e_v)$$

$$(xv,e_v)$$

$$(\mathsf{if}x\mathsf{then}c\mathsf{else}d,e_v)$$

$$\begin{array}[]{rcllllll}\underline{\delta\delta}&\rightarrow_{{\beta_{v}}}&(xx,[x{\shortleftarrow}\overline{\delta}])&\rightarrow_{\mathsf{sub}_{l}}&(\overline{\delta}\,x,[x{\shortleftarrow}\overline{\delta}])\\ &\rightarrow_{{\beta_{v}}}&(yy,[y{\shortleftarrow}x][x{\shortleftarrow}\overline{\delta}])\\ &\rightarrow_{\mathsf{sub}_{\mathit{var}}}&(yy,[y{\shortleftarrow}\overline{\delta}][x{\shortleftarrow}\overline{\delta}])&\rightarrow_{\mathsf{sub}_{l}}\ldots\end{array}$$

$$\begin{array}[]{clcccc}\underline{\delta\delta I}&\rightarrow_{{\beta_{v}}}(z\,\overline{I},[z{\shortleftarrow}xx][x{\shortleftarrow}\overline{\delta}])\rightarrow_{\mathsf{sub}_{l}}(z\,\overline{I},[z{\shortleftarrow}\overline{\delta}\,x][x{\shortleftarrow}\overline{\delta}])\\ &\rightarrow_{{\beta_{v}}}(z\,\overline{I},[z{\shortleftarrow}yy][y{\shortleftarrow}x][x{\shortleftarrow}\overline{\delta}])\\ &\rightarrow_{\mathsf{sub}_{l}}(z\,\overline{I},[z{\shortleftarrow}yy][y{\shortleftarrow}\overline{\delta}][x{\shortleftarrow}\overline{\delta}])\rightarrow_{\mathsf{sub}_{l}}\ldots\end{array}$$

$$c:=\underline{\delta \delta (xx)}=(zw,[z\text{shortleftarrow}\overline{\delta }\overline{\delta }][w\text{shortleftarrow}xx]).$$

$$\begin{array}[]{rcl\colspace\colspace rclcccc}\lx@intercol\hfil|b|_{\textup{var}}\coloneqq 0\ \ \ \ \mbox{if $b\neq x$}\hfil\lx@intercol\\ |x|_{\textup{var}}&\coloneqq&1&|(b,e)|_{\textup{var}}&\coloneqq&|b|_{\textup{var}}+|e|_{\textup{var}}&\\ |\epsilon|_{\textup{var}}&\coloneqq&0&|e[x{\shortleftarrow}b]|_{\textup{var}}&\coloneqq&|e|_{\textup{var}}+|b|_{\textup{var}}\\ \end{array}$$

$$((\lambda x.(xx,ϵ))y,[y\text{shortleftarrow}\lambda z.z]){\to }_{{\beta }_v}(xx,[x\text{shortleftarrow}y][y\text{shortleftarrow}\lambda z.z])$$

$$f$$

$$((\lambda x.c)v,e_f)$$

Full text

This work studies how such a crumbled representation of terms impacts on the design and the efficiency of abstract machines for call-by-value evaluation. About the design, it removes the need for data structures encoding the evaluation context, such as the applicative stack and the dump, that get encoded in the environment. About efficiency, we show that there is no slowdown, clarifying in particular a point raised by Kennedy, about the potential inefficiency of such a representation.

Moreover, we prove that everything smoothly scales up to the delicate case of open terms, needed to implement proof assistants. Along the way, we also point out that continuation-passing style transformations—that may be alternatives to our representation—do not scale up to the open case.

abstract machine, complexity, explicit substitution, lambda-calculus

1. Introduction

This paper is about the extension of $\lambda$-calculus with explicit constructors for sharing. The simplest such construct is a ${\sf let}\ x=u\ {\sf in}\ t$ expression, standing for $t$ where $x$ will be substituted by $u$, that we also write more concisely as $t[x{\shortleftarrow}u]$ and call ES (for explicit sharing, or explicit subsitution111$\mathsf{let}$ expressions and explicit substitutions usually come with different operational semantics: $\mathsf{let}$ expressions substitute in just one step, while explicit substitutions substitute in many micro steps, percolating through the term structure. They follow however the same typing principles. Moreover, explicit substitutions have many different formulations. In this paper we see $\mathsf{let}$ expressions as yet another form of explicit substitutions, and thus conflate the two terminologies.). Thanks to ES, $\beta$-reduction can be decomposed into more atomic steps. The simplest decomposition splits $\beta$-reduction as $(\lambda x.t)u\rightarrow_{\beta_{\textsf{ES}}}t[x{\shortleftarrow}u]\rightarrow_{\textsf{ES}}t\{x{\shortleftarrow}u\}$.

It is well-known that ES are somewhat redundant, as they can always be removed, by simply coding them as $\beta$-redexes. They are however more than syntactic sugar, as they provide a simple and yet remarkably effective tool to understand, implement, and program with $\lambda$-calculi and functional programming languages.

From a logical point of view, ES are the proof terms corresponding to the extension of natural deduction with a cut rule, and the cut rule is the rule representing computation, according to Curry-Howard. From an operational semantics point of view, they allow elegant formulations of subtle strategies such as call-by-need evaluation—various presentations of call-by-need use ES (Wadsworth, 1971; Launchbury, 1993; Maraist et al., 1998; Ariola et al., 1995; Sestoft, 1997; Kutzner and Schmidt-Schauß, 1998) and a particularly simple one is by Accattoli, Barenbaum, and Mazza in (Accattoli et al., 2014). From a programming point of view, they are part of most functional languages we are aware of. From a rewriting point of view, they enable proof techniques not available within the $\lambda$-calculus (e.g. reducing a global rewriting properties such as standardization to a local form, see Accattoli (2012)). Finally, sharing is used in all implementations of tools based on the $\lambda$-calculus to circumvent size explosion, the degenerate behaviour for which the size of $\lambda$-terms may grow exponentially with the number of $\beta$-steps.

Crumbled Forms

Once sharing is added to the $\lambda$-calculus, it enables a representation of terms where a sharing point is associated with every constructor of the term. Such a special form, roughly, is obtained by (recursively) decomposing iterated applications by introducing an ES in between any two of them. For instance, the representation of the term $(((\lambda x.x(xx))y)((\lambda z.z)y))y$ is

[TABLE]

Note that the transformation involves also function bodies (i.e. $\lambda x.x(xx)$ turns into $\lambda x.(xx^{\prime})[x^{\prime}{\shortleftarrow}xx]$), that ES are grouped together unless forbidden by abstractions, and that ES are flattened out, i.e. they are not nested unless nesting is forced by abstractions.

This work studies such a representation, called crumbled as it crumbles a term by means of ES. Our crumbling transformation closely resembles—while not being exactly the same—the transformation into a(dministrative) normal form (shortened to ANF), introduced by Flanagan et al. (1993), building on work by Sabry and Felleisen (1993), itself a variant of the continuation-passing style (CPS) transformation.

A delicate point is to preserve crumbled forms during evaluation. ES often come together with commutation rules to move them around the term structure. These rules are often used to unveil redexes during evaluation or to preserve specific syntactic forms. They may introduce significant overhead that, if not handled carefully, can even lead to asymptotic slowdowns as shown by Kennedy (2007). One of the contributions of this work is to show that crumbled forms can be evaluated and preserved with no need of commutation rules, therefore avoiding Kennedy’s potential slowdown.

This Paper

The focus of our work is on the impact of crumbled forms on the design and asymptotic overhead of abstract machines with weak evaluation (i.e. out of abstractions) on closed terms, and the scalability to (possibly) open terms. Bounding the overhead of abstract machines is a new trend, according to which the machine overhead has to be proved polynomial or even linear in the number of $\beta$-steps (Accattoli et al., 2014, 2015; Accattoli and Sacerdoti Coen, 2015; Accattoli, 2016; Accattoli and Guerrieri, 2017; Accattoli and Barras, 2017). Open terms—that are not needed to implement functional languages—are used to implement the more general and subtle case of proof assistants. The two topics actually motivate each other: the naive handling of open terms with the techniques for functional languages gives abstract machines with exponential overhead (Accattoli and Sacerdoti Coen, 2015; Accattoli and Guerrieri, 2017) which then pushes to develop more efficient machines.

We anticipate here the main results of the paper: crumbled forms induce abstract machines for weak evaluation with less data structures and the transformation does not introduce any asymptotic overhead. Moreover, these facts smoothly scale up to open terms.

Why study crumbled forms.

Our interest in studying crumbled forms comes precisely from the fact that they remove some data structures from the design of abstract machines. The relevance of this fact becomes evident when one tries to design abstract machines for strong evaluation (that is, evaluating under abstraction). The study of such machines is extremely technical (see also section Sect. 7) because they have more data structures and more transitions than in the closed and open cases. The many additional transitions are in particular due to the handling of the various data structures. In call-by-name, the situation is still manageable (Crégut, 1990; García-Pérez et al., 2013; Accattoli et al., 2015; Accattoli, 2016), but in call-by-value/need the situation becomes quickly desperate—it is not by chance that there is not a single strong abstract machine for call-by-value/need in the literature.

This work is then preliminary to a detailed study of strong abstract machines for call-by-value and call-by-need. The aim is to explore the subtleties in frameworks that are well understood, such as the closed and open call-by-value cases, and show that there are no slow downs in turning to a crumbled representation.

The next sub-sections continue the introduction with a lengthy overview of the role of environments, the content of the paper, the relationship with the ANF, the asymptotic study of abstract machines, and related work.

1.1. Environments

ES are often grouped together instead of being scattered all over the term, in finite sequences called environments. Abstract machines typically rely on environments. Crumbled forms also rely on packing ES together, as pointed out before, but depart from the ordinary case as environments may appear also under abstractions.

Crumbled Environments.

The notion of environment induced by crumbled forms, named here crumbled environments, is peculiar. Crumbled environments indeed play a double role: they both store delayed substitutions, as also do ordinary environments, and encode evaluation contexts. In ordinary abstract machines, the evaluation context is usually stored in data structures such as the applicative stack or the dump. Roughly, they implement the search for the redex in the ordinary applicative structure of terms. For crumbled forms, the evaluation context is encoded in the crumbled environment, and so the other structures disappear.

Operations on Crumbled Environments.

There are two subtle implementative aspects of crumbled environments, that set them apart from ordinary ones. Ordinary environments are presented with a sequential structure but they are only accessed randomly (that is, not sequentially)—in other words, their sequential structure does not play a role. Crumbled environments, as the ordinary ones, are accessed randomly, to retrieve delayed substitutions, but they are also explored sequentially—since they encode evaluation contexts—in order to search for redexes. Therefore, their implementation has to reflect the sequential structure.

The second subtlety is that crumbled machines also have to concatenate environments, that is an operation never performed by ordinary machines, and that has to be concretely implemented as efficiently as possible, i.e. in constant time. That this point is subtle is proved by the fact that Kennedy’s slowdown (Kennedy, 2007) amounts to a quadratic overhead in evaluating terms in ANF due to the concatenation of environments.

To address these points, we provide a prototype OCaml implementation of crumbled environments in Appendix F (p. F), to be compared with the one of global environments in Accattoli and Barras (2017), that does not concretely implement the sequential structure. In particular, our implementation concatenates environments in constant time and does not suffer from Kennedy’s slowdown. Essentially, Kennedy’s slowdown amounts to the fact that his implementation concatenates ANF environments in linear rather than constant time (see Appendix A).

1.2. Content of the Paper

The Closed Case.

First, we define crumbled forms and an abstract machine evaluating them, the Crumble GLAM, and show that it implements Plotkin’s closed small-step call-by-value (CbV for short) $\lambda$-calculus (extended with conditionals, see below). Moreover, we study the overhead of the machine, and show that it is linear in the number of $\beta$-steps and in the size of the initial term, exactly as the best machines for CbV executing ordinary terms. Therefore, the crumbling transformation does not introduce any asymptotic overhead. The study is detailed and based on a careful and delicate spelling of the invariants of the machine. In particular, our approach does not suffer from Kennedy’s potential slowdown.

Open Terms.

The second ingredient of the new trend of abstract machines (Accattoli et al., 2014, 2015; Accattoli and Sacerdoti Coen, 2015; Accattoli, 2016; Accattoli and Guerrieri, 2017; Accattoli and Barras, 2017)—the first being complexity analyses—is studying evaluation in presence of (possibly) open terms or even strong evaluation (i.e. under abstraction), which is required in order to implement proof assistants. Apart from few exceptions—Crégut (1990), Grégoire and Leroy (2002), and García-Pérez et al. (2013)—the literature before the new wave mostly neglected these subtle cases, and none of those three papers addressed complexity.

The open case, in which evaluation is weak but terms are possibly open is strictly harder than the closed one, and close in spirit to the strong case, but easier to study—it is for instance the one studied by Grégoire and Leroy (2002) when modelling (an old version of) the abstract machine of the kernel of Coq.

Open Call-by-Value.

Open evaluation for CbV—shortened Open CbV—is particularly subtle because, as it is well-known, Plotkin’s operational semantics is not adequate when dealing with open terms—see Accattoli and Guerrieri (2016, 2018). Open CbV has been studied deeply by Accattoli and Sacerdoti Coen (2015); Accattoli and Guerrieri (2016, 2017, 2018), exploring different presentations, their rewriting, cost models, abstract machines, and denotational semantics. One of the motivations of this work is to add a new piece to the puzzle, by lifting the crumbling technique to the open case.

Our second contribution is to show that the crumbling technique smoothly scales up to Open CbV. We provide an abstract machine, the Open Crumble GLAM, and we show that it implements the fireball calculus—the simplest presentation of Open CbV—and that, as in the closed case, it only has a linear overhead. Two aspects of this study are worth pointing out. First, the technical development follows almost identically the one for the closed case, once the subtler invariants of the new machine have been found. Second, the substitution of abstractions on demand, a technical optimisations typical of open/strong cases (introduced in Accattoli and Dal Lago (2016) and further studied in Accattoli and Sacerdoti Coen (2015); Accattoli and Guerrieri (2017)), becomes superfluous as it is subsumed by the crumbling transformation.

1.3. The Relationship with ANF

As long as one sticks to the untyped $\lambda$-calculus, crumbled forms coincide with ANF. The ANF, we said, is a variant of the CPS transformation. Roughly, the difference is that the ANF does not change the type, when terms are typed (here we work without types).

Kennedy (2007) pointed out two problems with the ANF. One is the already discussed quadratic overhead, that does not affect our approach. The second one is the fact that the ANF does not smoothly scale up when the $\lambda$-calculus is extended to further constructs such as conditionals or pattern matching. Essentially, the ANF requires conditionals and pattern matching to be out of ES, that is, to never have an expression such as $s[x{\shortleftarrow}(\mathsf{if}\,v\,\mathsf{then}\,t\,\mathsf{else}\,u)]$. Unfortunately, these configurations can be created during evaluation. To preserve the ANF, one is led to add so-called commuting conversions such as:

[TABLE]

Clearly, there is an efficiency issue: the commutation causes the duplication of the subterm $s$. A way out is to use a continuation-like technique, which makes Kennedy conclude that then there is no point in preferring ANF to CPS.

This is where our crumble representation departs from the ANF, as we do not require conditionals and pattern matching to be out of ES. Kennedy only studies the closed case. Our interest in open and strong evaluation is to explore the theory of implementation needed for proof assistants. In these settings, commutations of conditionals and pattern matching such as those hinted at by Kennedy are not valid, as they are not validated by dependent type systems like those of Coq or Agda. For example, adding the CC rule above when the conditional is dependently typed breaks the property of subject reduction, as typed terms reduce to ill-typed terms. Consider the term:

$(x+1)[x\colon(\mathsf{if}\,true\,\mathsf{then}\,nat\,\mathsf{else}\,bool){\shortleftarrow}\mathsf{if}\,true\,\mathsf{then}\,0\,\mathsf{else}\,\textit{false}]\colon nat$

that has type $nat$ because the type of $x$ is convertible to $nat$. By applying rule CC, we obtain:

[TABLE]

which is clearly ill-typed.

The problem in the open case is actually more general, as not even the CPS would work: its properties do not scale up to open terms. In Appendix A, indeed, we provide a counter-example to the simulation property in the open case.222Danvy and Filinski (1992) claim that the CPS transformation scales up to open terms (their Theorem 2). However, as we discuss in Appendix A, they consider only Plotkin’s operational semantics, which is not adequate for open terms.

To sum up, neither commuting conversions nor the CPS transformation can be used in our framework. Therefore, we accept that conditionals and pattern matching may appear in ES (in contrast to Kennedy) and so depart from the ANF.

In the paper we treat the cases of the closed and open CbV calculi extended with conditionals. The essence of the study is the crumbling of $\beta$-reduction, not the conditionals. Conditionals are included only to stress the difference with respect to the ANF (pattern matching can be handled analogously), but they do not require a special treatment.

1.4. The Complexity of Abstract Machines

Asymptotic Bounds $vs$ Benchmarking

The study of asymptotic bounds for abstract machines is meant to complement the use of benchmarking, by covering all possible cases, that certainly cannot be covered via benchmarking.

The relevance of such a study is particularly evident when one considers open terms or strong evaluation. For strong evaluation, for instance, for more than 25 years in the literature there has been only Cregut’s abstract machines (Crégut, 1990), which on size exploding families of terms actually has exponential overhead (in the number of $\beta$-steps and the size of the initial term). A polynomial machine, developed via a careful asymptotic study, is in Accattoli (2016). Similarly, the abstract machine for open terms described in Grégoire and Leroy (2002) suffers of exponential overhead on size exploding families (even if the authors then in practice implement a slightly different machine with polynomial overhead). The asymptotic study of this case is in Accattoli and Sacerdoti Coen (2015); Accattoli and Guerrieri (2017).

Abstract machines vs compilation

Abstract machines and compilation to machine language are two distinct techniques to execute a program. Compilation is typically more efficient, but it only handles the case where terms are closed and evaluation is weak, that is, the one of functional languages. Strong evaluation is sometimes employed during compilation to optimise the compiled code, but typically only on linear redexes where size and time explosions are not an issue. Abstract machines are the only execution technique implemented in interactive theorem provers based on dependent types, that need strong evaluation.

Kennedy (2007) argues that CPS-based translations are superior to ANF also because the CPS makes join points explicit as continuations, so that invocation of the continuation can be compiled efficiently using jumps. The argument is only valid for compilation and it does not affect abstract machines.

Garbage collection

We study abstract machines, that on purpose ignore many details of concrete implementations, such as garbage collection, that is an orthogonal topic. In particular, garbage collection is always at most polynomial, if not linear, and so its omission does not hide harmful blowups. As far as we know, no abstract machine implemented in interactive provers performs garbage collection.

1.5. Related Work

Environments.

In a recent work, Accattoli and Barras (2017) compare various kinds of environments, namely, global, local, and split, from implementative and complexity points of view. The crumbling transformation can be studied with respect to every style of environment. Here we focus on crumbled global environments because they are simpler and because we also consider the open case, where all kinds of environment induce the same complexity.

Administrative Normal Forms.

The literature on ANF is scarce. Beyond the already cited original papers, Danvy has also studied them and their relationship to CPS, but usually calling them monadic normal forms (Danvy, 1994; Hatcliff and Danvy, 1994; Danvy, 2003) because of their relationship with Moggi’s monadic $\lambda$-calculus (Moggi, 1991). That terminology however sometimes describes a more liberal notion of terms, for instance in Kennedy (2007). Kennedy’s paper is also another relevant piece in the literature on ANF.

2. The Pif Calculus

The grammars and the small-step operational semantics of the Pif calculus $\lambda_{\mathsf{Plot}}^{\mathsf{if}}$, that is, Plotkin’s calculus $\lambda_{\mathsf{Plot}}$ (Plotkin, 1975) for Closed CbV evaluation extended with booleans and an $\mathsf{if}\mbox{-}\mathsf{then}\mbox{-}\mathsf{else}$ construct, plus error handling for clashing constructs, are in Fig. 1.

A term is either an application of two terms, an $\mathsf{if}\mbox{-}\mathsf{then}\mbox{-}\mathsf{else}$, or a value, which is in turn either a variable, a ($\lambda$-)abstraction, $\mathsf{true}$, $\mathsf{false}$, or an error $\mathsf{err}$. We distinguish values that are not variables, noted $v_{\neg x}$ and called practical values, following Accattoli and Sacerdoti Coen (2017). The body of an abstraction $\lambda x.t$ is $t$ and the bodies of a conditional $\mathsf{if}\,t\,\mathsf{then}\,u\,\mathsf{else}\,s$ are its two branches $u$ and $s$. Terms are always identified up to $\alpha$-equivalence and the set of free variables of a term $t$ is denoted by ${\sf fv}(t)$; $t$ is closed if ${\sf fv}(t)=\emptyset$, open otherwise. We use $t\{x{\shortleftarrow}u\}$ for the term obtained by the capture-avoiding substitution of $u$ for each free occurrence of $x$ in $t$.

Contexts

In general, contexts are denoted by $C$ and are terms with exactly one occurrence of a special constant $\langle\cdot\rangle$ called the hole, that is a placeholder for a removed subterm. In the paper we use various notions of contexts in different calculi—for $\lambda_{\mathsf{Plot}}^{\mathsf{if}}$ the relevant notion is right (evaluation) v-context $R$ (see Fig. 1). The basic operation on (whatever notion of) contexts is the plugging $C\langle t\rangle$ of a term $t$ for the hole $\langle\cdot\rangle$ in $C$: simply the hole is removed and replaced by $t$, possibly capturing variables.

Evaluation

According to the definition of right v-context, CbV evaluation $\rightarrow_{\mathsf{pif}}$ in $\lambda_{\mathsf{Plot}}^{\mathsf{if}}$ is weak, i.e. it does not reduce under $\lambda$-abstractions and in the branches of an $\mathsf{if}\mbox{-}\mathsf{then}\mbox{-}\mathsf{else}$. CbV evaluation is defined for any (possibly open) term. But it is well-known that this operational semantics is adequate only for closed terms, as first noticed by Paolini and Ronchi Della Rocca (Ronchi Della Rocca and Paolini, 2004), see also Accattoli and Guerrieri (Accattoli and Guerrieri, 2016, 2018). When restricted to closed terms, $\lambda_{\mathsf{Plot}}^{\mathsf{if}}$ is called Closed (Conditional) CbV: in this setting, evaluation can fire a $\beta$-redex $(\lambda x.t)u$ only if the argument $u$ is a closed value, i.e. a closed $\lambda$-abstraction, a boolean, or $\mathsf{err}$; and in the production $Rv$ for the definition of right v-contexts, $v$ is always a closed value. Note that we work with right-to-left evaluation—this is forced by the production $Rv$ in the definition of right evaluation v-contexts. In the closed case one could as well work with left-to-right evaluation, the choice is inessential.

The error constant $\mathsf{err}$ is generated during evaluation by the two cases of construct clashes: when the condition for an $\mathsf{if}\mbox{-}\mathsf{then}\mbox{-}\mathsf{else}$ is an abstraction and when a boolean is applied to a term. Both cases would be excluded by typing, but in our untyped setting they are possible, and handled via errors. Similarly, errors are also propagated when they appear as conditions for $\mathsf{if}\mbox{-}\mathsf{then}\mbox{-}\mathsf{else}$ and as left terms of an application. These cases are handled by rules $\rightarrow_{\textsf{ife}}$ and $\rightarrow_{\textsf{@e}}$. Note that errors do not propagate when they occur as arguments of applications: if the left sub-term of the application becomes an abstraction that erases the error then the error is handled and it is not observable.

A key property of Plotkin’s Closed CbV is harmony: a closed term is ${\beta_{v}}$-normal if and only if it is a (closed) value i.e. a (closed) $\lambda$-abstraction. Therefore, every closed term either diverges or it evaluates to a (closed) $\lambda$-abstraction. Harmony extends to $\lambda_{\mathsf{Plot}}^{\mathsf{if}}$.

Proposition 2.1 (Pif harmony).

††margin:

Proof p. Proof of

Let $t$ be a closed term. $t$ is $\rightarrow_{\mathsf{pif}}$-normal if and only if $t$ is a value.

3. Crumbled Evaluation, Informally

Decomposing applications.

The idea is to forbid the nesting of non-value constructs such as applications and $\mathsf{if}\mbox{-}\mathsf{then}\mbox{-}\mathsf{else}$ without losing expressive power. To ease the explanation, we focus on nested applications and forget about $\mathsf{if}\mbox{-}\mathsf{then}\mbox{-}\mathsf{else}$—they do not pose any difficulty. Terms such as $(tu)s$ or $t(us)$ are then represented as $(\lambda x.(xs))(tu)$ and $(\lambda x.(tx))(us)$ where $x$ is a fresh variable. It is usually preferred to use $\mathsf{let}$ expressions rather than introducing $\beta$-redexes, so that one would rather write ${\sf let}\ x=tu\ {\sf in}\ (xs)$ and ${\sf let}\ x=us\ {\sf in}\ (tx)$, or, with ES (aka environment entries), rather write

$(xs)[x{\shortleftarrow}tu]$    and    $(tx)[x{\shortleftarrow}us]$

If the crumbling transformation $\underline{\,\cdot\,}$ is applied to the whole term—recursively on $t$, $u$ and $s$ in our examples—all applications have the form $vv^{\prime}$, i.e. they only involve values. If moreover CbV evaluation is adopted, then such a crumbled form is stable by evaluation (reduction steps are naturally defined so that a crumbled form reduces to a crumbled form), as variables can only be replaced by values.

Simulation and no evaluation contexts.

Let us now have a look at a slightly bigger example and discuss the recursive part of the crumbling transformation. Let $I=\lambda x.x$ be the identity and consider the term $t\coloneqq((\lambda y.yy)I)((II)I)$ whose right-to-left evaluation is

[TABLE]

The crumbling transformation decomposes all applications, taking special care of grouping all the environment entries together, flattening them out (that is, avoiding having them nested one into the other), and reflecting the evaluation order in the arrangement of the environment. For instance, the crumbled representation $\underline{t}$ of the term $t$ above is

[TABLE]

and evaluation takes always place at the end of the environment, as follows:

[TABLE]

where the $\rightarrow_{{\beta_{v}}}$ steps correspond exactly to steps in the ordinary evaluation of $t$ and $\rightarrow_{[\ ]}$ steps simply eliminate the explicit substitution when its content is a value. Note how the transformation makes the redex always appear at the end of the environment, so that the need for searching for it—together with the notion of evaluation context—disappears.

Let us also introduce some terminology. Values and applications of values are bites. The transformation, called crumbling translation, turns a term into a bite with an environment—such a pair is called a crumble.

Turning to micro-step evaluation.

The previous example covers what happens when the crumbling transformation is paired with small-step evaluation. Abstract machines, however, employ a finer mechanism that we like to call micro-step evaluation, where the substitutions due to $\beta$-redexes are delayed and represented as new environment entries, and moreover substitution is decomposed as to act on one variable occurrence at a time. In particular, such a more parsimonious evaluation never removes environment entries because they might be useful later on—garbage collection is assumed to be an orthogonal and independent process. To give an idea of how micro steps work, let’s focus on the evaluation of the subterm $(wz)[w{\shortleftarrow}(\lambda y.yy)I]$ of our example (because micro-step evaluations are long and tedious), that proceeds as follows:

[TABLE]

where $\rightarrow_{{\beta_{v}}}$ steps now introduce new environment entries. Now the redex is not always at the end of the environment, but it is always followed on the right by an environment whose entries are all abstractions, so that the search for the next redex becomes a straightforward visit from right to left of the environment—the evaluation context has been coded inside the sequential structure of the environment.

Abstraction bodies and the concatenation of environments.

There is a last point to explain. We adopt weak evaluation—that only evaluates out of abstractions—but the crumbling transformation also transforms the bodies of abstractions and the branches of $\mathsf{if}\mbox{-}\mathsf{then}\mbox{-}\mathsf{else}$ into crumbles. Let us see another example. The crumbled representation of $u\coloneqq(\lambda x.((xx)(xx)))(II)$ then is

[TABLE]

Micro-step evaluation goes as follows:

\begin{array}[]{lllllllllllll}\underline{u}&\rightarrow_{{\beta_{v}}}&((\lambda x.((yz)[y{\shortleftarrow}xx][z{\shortleftarrow}xx]))w)[w{\shortleftarrow}w^{\prime}][w^{\prime}{\shortleftarrow}I]\\ &\rightarrow_{[\ ]}&((\lambda x.((yz)[y{\shortleftarrow}xx][z{\shortleftarrow}xx]))w)[w{\shortleftarrow}I][w^{\prime}{\shortleftarrow}I]\\ &\rightarrow_{[\ ]}&((\lambda x.((yz)[y{\shortleftarrow}xx][z{\shortleftarrow}xx]))I)[w{\shortleftarrow}I][w^{\prime}{\shortleftarrow}I].\end{array}

At this point, the reduction of the $\beta$-redex (involving $\lambda x$) has to combine the crumble of the redex itself with the one of the body of the abstraction, by concatenating the environment of the former (here $[w{\shortleftarrow}I][w^{\prime}{\shortleftarrow}I]$) at the end of the environment of the latter ($[y{\shortleftarrow}xx][z{\shortleftarrow}xx]$), interposing the entry created by the redex itself ($[x{\shortleftarrow}I]$), thus producing the new crumble:

[TABLE]

The key conclusion is that evaluation needs to concatenate crumbled environments, which is an operation that ordinary abstract machines instead never perform.

Note that transforming abstraction bodies may produce nested ES, if the abstraction occurs in an ES. This is the only kind of nesting of ES that is allowed.

4. The Crumbling Transformation

In this section we formally define the language of crumbled forms and the crumbling transformation.

Crumbled forms.

Terms are replaced by crumbles, which are formed by a bite and an environment, where in turn

• •

a bite is either a crumbled value (i.e. a variable, a boolean, an error, or an abstraction over a crumble), an application of crumbled values, or a $\mathsf{if}\mbox{-}\mathsf{then}\mbox{-}\mathsf{else}$ on a crumbled value whose alternatives are crumbles, and

• •

an environment is a finite sequence of explicit substitutions of bites for variables.

Formally, the definition is by mutual induction:

[TABLE]

• •

Bodies: the bodies of abstractions and $\mathsf{if}\mbox{-}\mathsf{then}\mbox{-}\mathsf{else}$ are themselves crumbles—the forthcoming crumbling transformation is indeed strong, as it also transforms bodies.

• •

Crumbles are not closures: the definition of crumbles may remind one of closures in abstract machines with local environments, but the two concepts are different. The environment $e$ of a crumble $(b,e)$, indeed, does not in general bind all the free variables of the bite $b$.

We freely consider environments as lists extendable on both ends, and whose concatenation is obtained by simple juxtaposition. Given a crumble $(b,e)$ and an environment $e^{\prime}$ the appending of $e^{\prime}$ to $(b,e)$ is $(b,e)\mathrel{@}e^{\prime}\coloneqq(b,ee^{\prime})$.

Free variables, $\alpha$-renaming, and all that.

All syntactic expressions are not considered up to $\alpha$-equivalence. Free variables are defined as expected for bites. For environments and crumbles they are defined as follows (via the auxiliary notion of domain of environments; this is because global environments are used here):

[TABLE]

Let $e=[x_{1}{\shortleftarrow}b_{1}]\dots[x_{k}{\shortleftarrow}b_{k}]$ be an environment: we denote the lookup of $x_{i}$ in $e$ by $e(x_{i})\coloneqq b_{i}$. We say that a crumble $c$ or an environment $e$ are well-named if all the variables occurring on the lhs of ES outside abstractions in $c$ or $e$ are pairwise distinct.

The crumbling translation.

A term is turned into a crumble via the following crumbling translation $\underline{\,\cdot\,}\,$, which uses an auxiliary translation $\overline{\,\cdot\,}$ from values into crumbled values.

[TABLE]

[TABLE]

$(*)$ if $t$ is not a value and $\underline{t}=(b,e)$, and $x$ is fresh.

According to the definition, if $u$ and $t$ are not values, $\underline{ut}=(yx,[y{\shortleftarrow}b^{\prime}]e^{\prime}[x{\shortleftarrow}e])$ with $\underline{t}=(b,e)$, $\underline{u}=(b^{\prime},e^{\prime})$ and $x,y$ fresh.

Example 4.1.

Let $\delta\coloneqq\lambda x.{xx}$ and $I\coloneqq\lambda x.x$: $\overline{I}=\lambda x.\underline{x}=\lambda x.{(x,\epsilon)}$, $\overline{\delta}=\lambda x.{\underline{xx}}=\lambda x.{(xx,\epsilon)}$ (as $\underline{xx}=(xx,\epsilon)$), and $\underline{\delta\delta}=(\bar{\delta}\bar{\delta},\epsilon)$. So,

[TABLE]

The crumbling translation $\underline{\,\cdot\,}$ is not surjective: the crumble $c\coloneqq(xx,[x{\shortleftarrow}y])$ is such that $\underline{t}\neq c$ for any term $t$.

Read back.

There is a left inverse for the crumbling translation, called read-back and defined by:

[TABLE]

Proposition 4.2 (Read-back and the crumbling translation).

††margin:

Proof p. Proof of

For every term $t$ and every value $v$, one has $\underline{t}_{\downarrow}=t$ and $\overline{v}_{\downarrow}=v$.

Remark 4.1 (Crumbling translation, free variables).

1. (1)

For any term $t$ and any value $v$, one has ${\sf fv}(t)={\sf fv}(\underline{t})$ and ${\sf fv}(v)={\sf fv}(\overline{v})$; in particular, $t$ is closed if and only if $\underline{t}$ is so. 2. (2)

For any bite $b$ and any crumble $c$, ${\sf fv}(b_{\downarrow})={\sf fv}(b)$ and ${\sf fv}(c_{\downarrow})={\sf fv}(c)$. 3. (3)

The crumbling translation commutes with the renaming of free variables. 4. (4)

The crumbling translation and the read-back map values to values.

Crumbled contexts.

For crumbled forms, we need contexts both for environments and crumbles:

[TABLE]

Crumbles can be plugged into both notions of contexts. Let us point out that the following definition of plugging is slightly unusual as it does a little bit more than just replacing the hole, because simply replacing would not provide a well-formed syntactic object: plugging indeed extracts the environment from the plugged crumble and concatenates it with the environment of the context. Such an unusual operation—that may seem ad-hoc—is actually one of the key technical points in order to obtain a clean proof of the implementation theorem.

Definition 4.3 (Plugging in crumbled contexts).

Let $E=e[x{\shortleftarrow}\langle\cdot\rangle]$ be an environment context, $C$ be a crumble context, and $c=(b^{\prime},e^{\prime})$ be a crumble. The plugging $E\langle c\rangle$ of $c$ in $E$ and the plugging $C\langle c\rangle$ of $c$ in $C$ are defined by

[TABLE]

Example 4.4.

In Ex. 4.1 we have seen that $\underline{\delta\delta I}=(z\lambda x.{x_{\epsilon}},[z{\shortleftarrow}(\lambda x.{(xx)_{\epsilon}})\lambda x.{(xx)_{\epsilon}}])$, where we set $b_{\epsilon}\coloneqq(b,\epsilon)$ for any bite $b$. We have that $\underline{\delta\delta I}=C\langle c\rangle$ with $C\coloneqq(z\lambda x.{x_{\epsilon}},[z{\shortleftarrow}\langle\cdot\rangle])$ and $c\coloneqq((\lambda x.{(xx)_{\epsilon}})\lambda x.{(xx)_{\epsilon}},\epsilon)$

The notions of well-named, ${\sf fv}(\cdot)$, and $\mathsf{dom}(\cdot)$ can be naturally extended to crumble contexts. The definition of read back is extended to crumble contexts by setting $\langle\cdot\rangle_{\downarrow}\coloneqq\langle\cdot\rangle$ and $(b,e{[x{\shortleftarrow}\langle\cdot\rangle]})_{\downarrow}\coloneqq(b,e)_{\downarrow}\{x{\shortleftarrow}\langle\cdot\rangle\}$. Note however that the unfolding of a crumble context is not necessarily a context, because the hole can be duplicated or erased by the unfolding. For instance, let $C\coloneqq(x\,x,[x{\shortleftarrow}\langle\cdot\rangle])$. Then $C_{\downarrow}=\langle\cdot\rangle\langle\cdot\rangle$ is not a context.

Lemma 4.5 provides the properties of the translation needed to prove the invariants of machines in the next sections.

Lemma 4.5 (Properties of crumbling).

††margin:

Proof p. Proof of

For every term $t$:

1. (1)

Freshness:* $\underline{t}$ is well-named.* 2. (2)

Closure:* if $t$ is closed, then ${\sf fv}(\underline{t})=\emptyset$.* 3. (3)

Disjointedness*: $\mathsf{dom}(C)\cap{\sf fv}(b)=\emptyset$ if $\underline{t}=C\langle(b,e)\rangle$.* 4. (4)

Bodies:* every body in $\underline{t}$ is the translation of a term.* 5. (5)

Contextual decoding:* if $\underline{t}=C\langle c\rangle$, then $C_{\downarrow}$ is a right v-context.*

5. The Closed Case

Here we show how to evaluate crumbled forms with a micro-step operational semantics. We builds over the work of Accattoli and co-authors, who employ the following terminology:

• •

Calculus: for a small-step semantics where both substitution and search for the redex are meta-level operations;

• •

Linear calculus: for a micro-step semantics where substitution is decomposed—the calculus has ES and possibly a notion of environment if the ES are grouped together—but the search for the redex is still meta-level and expressed via evaluation contexts;

• •

Abstract machine: for a micro-step semantics where both substitution and search for the redex are decomposed. The search for redexes is handled via one or more stacks called applicative stack, dump, frame, and so on; the management of names is also explicit, i.e. not up-to $\alpha$-equivalence.

The crumbling transformation blurs the distinction between a linear calculus and an abstract machine because it allows using the sequential structure of the environment as the only stack needed to search for redexes.

The operational semantics for crumbled forms that we present next is in the style of a linear calculus, because spelling out the straightforward search for redexes is not really informative. Nonetheless, we do call it an abstract machine, because of the blurred distinction in the crumble case and because we manage names explicitly. In Appendix D.4 (p. D.4) we spell out the actual abstract machine.

5.1. The Crumble GLAM

Transitions.

To introduce the Crumble GLAM (GLAM stands for Global Leroy Abstract Machine) we need some definitions. First, environments and crumbles made out of practical values only are defined and noted as follows:

[TABLE]

Essentially, a $v$-environment stands for the already evaluated coda of the environment described in the paragraph about micro-steps in Sect. 3, while $v$-crumbles are fully evaluated crumbles (i.e. final states of the machine), as we show below.

Second, given a crumble $c$ we use $c^{\alpha}$ for a crumble obtained by $\alpha$-renaming the names in the domain of $c$ with fresh ones so that $c^{\alpha}$ is well-named.

The transitions act on crumbles whose environments are $v$-environments. The top level transitions are:

[TABLE]

1. (1)

if $v=\lambda x.e$ or $v=\mathsf{err}$ 2. (2)

if $v\in\{\mathsf{true},\mathsf{false},\mathsf{err}\}$ 3. (3)

if $x\in\mathsf{dom}(e_{v})$

Transitions are then closed by crumble contexts: for every $a\in\{{\beta_{v}},\textsf{ift},\textsf{iff},\textsf{ife},\textsf{@e},\mathsf{sub}_{\mathit{var}},\mathsf{sub}_{l},\mathsf{sub}_{\mathsf{if}}\}$ define $C\langle c\rangle\rightarrow_{a}C\langle d\rangle$ if $c\mapsto_{a}d$. The transition relation $\rightarrow_{\mathsf{Cr}}$ of the Crumble GLAM is defined as the union of all these rules. Let us explain each transition:

• •

$\rightarrow_{{\beta_{v}}}$: (forget about the $\alpha$-renaming for the moment—see the next paragraph) the rule removes a $\beta$-redex and introduces an ES $[x{\shortleftarrow}v]$ instead of performing the meta-level substitution. Moreover, the environment of the body $c$ of the abstraction and the external environment $e_{v}$ are concatenated (via the appending operation $\mathrel{@}$) interposing $[x{\shortleftarrow}v]$.

• •

Conditional and error transitions $\rightarrow_{\textsf{ift}},\rightarrow_{\textsf{iff}},\rightarrow_{\textsf{ife}},\rightarrow_{\textsf{@e}}$: these transitions simply mimics the analogous rules on the Pif calculus, with no surprises.

• •

Substitution transitions $\rightarrow_{\mathsf{sub}_{l}},\rightarrow_{\mathsf{sub}_{y}},\rightarrow_{\mathsf{sub}_{\mathsf{if}}}$: the variable $x$ is substituted by the corresponding crumbled value in the environment $e_{v}$, if any. In the closed case, a forthcoming invariant guarantees that $e_{v}(x)$ is always defined so that side-condition (3) is actually always satisfied. There are no rules to substitute on the right of an application, we explain this below.

Note that, according to the definitions of plugging and top level transitions, the transition relation follows right-to-left evaluation, since the environment on the right of a redex is a $v$-environment, i.e. it is made of practical values only, which means that it has already been evaluated (see the harmony property for Crumble GLAM in Prop. 5.3 below). Adopting right-to-left evaluation implies that the Crumble GLAM does not need a rule $\rightarrow_{\mathsf{sub}_{r}}$ symmetrical to $\rightarrow_{\mathsf{sub}_{l}}$, whose top level shape would be $(vx,e_{v})\mapsto_{{\mathsf{e}}_{r}}(v\,e_{v}(x),e_{v})$ with $x\in\mathsf{dom}(e_{v})$: indeed, if $v$ is a variable then $\rightarrow_{\mathsf{sub}_{l}}$ applies to the same redex $(vx,e_{v})$, otherwise $v$ is an abstraction and then $\rightarrow_{{\beta_{v}}}$ applies to $(vx,e_{v})$.

The cost and the place of $\alpha$-renaming.

Abstract machines with global environments have to $\alpha$-rename at some point, this is standard333Local environments do allow to avoid renamings, but the simplification is an illusion, as the price is payed elsewhere—see Accattoli and Barras (2017)—there is no real way out.. In our implementation, renaming is implemented as a copy function. And the cost of renaming is under control because of forthcoming invariants of the machine. This is all standard (Accattoli and Barras, 2017). Often the burden of renaming/copying is put on the substitution rules. It is less standard to put it on the ${\beta_{v}}$-transition, as we do here, but nothing changes. Last, a technical remark: in rule $\rightarrow_{{\beta_{v}}}$ the $\alpha$-renaming at top level has to pick names that are fresh also with respect to the crumble context enclosing it. This point may seem odd but it is necessary to avoid name clashes, and it is trivially obtained in our concrete implementation, where variable names are memory locations and picking a fresh name amounts to allocating a new location, that is of course new globally.

Definition 5.1 (Reachable crumble).

A crumble is reachable (by the Crumble GLAM) if it is obtained by a sequence of transitions starting from the translation $\underline{t}$ of a closed term $t$.

Unchaining abstractions.

The substitution performed by the rule $\rightarrow_{\mathsf{sub}_{\mathit{var}}}$ may seem an unneeded optimization; quite the opposite, it fixes an issue causing quadratic overhead in the machine. The culprits are malicious chains of renamings, i.e. environments of the form $[x_{1}{\shortleftarrow}x_{2}][x_{2}{\shortleftarrow}x_{3}]\cdots[x_{n}{\shortleftarrow}\lambda y.c]$ substituting variables for variables and finally leading to an abstraction. Accattoli and Sacerdoti Coen (2015) showed that the key to linear overhead is to perform substitution steps while going through the chain from right to left.

Example 5.2.

Consider the crumble $\underline{\delta\delta}=(\overline{\delta}\,\overline{\delta},\epsilon)$, where $\overline{\delta}=\lambda x.{(xx,\epsilon)}$; then:

[TABLE]

In Ex. 4.1 we introduced the crumble $\underline{\delta\delta I}=(z\,\overline{I},[z{\shortleftarrow}\overline{\delta}\,\overline{\delta}])$ where $\overline{I}=(\lambda x.{(x,\epsilon)})$; in accordance with the crumble decomposition shown in Ex. 4.4, we have:

[TABLE]

Consider now the open crumble

[TABLE]

The crumble $c$ is normal because its only possible decomposition of the form $C\langle(b,e_{v})\rangle$ is for $e_{v}=\epsilon$ (as $xx$ is not a practical value), and no transitions apply to the rightmost entry $[w{\shortleftarrow}xx]$ since $x$ is free.

The Crumble GLAM satisfies a harmony property.

Proposition 5.3 (Harmony for the Crumble GLAM).

††margin:

Proof p. Proof of

A closed crumble $c$ is normal if and only if it is a $v$-crumble.

5.2. The Implementation Theorem

To show that the Crumble GLAM correctly implements the Pif calculus, we apply an abstract approach introduced by Accattoli and Guerrieri (2017), which we reuse as well in the following sections for other crumble abstract machines and other evaluation strategies of the $\lambda$-calculus.

The implementation theorem, abstractly.

In Accattoli and Guerrieri (2017) it is proven that, given

• •

a generic abstract machine ${\sf M}$, which is a transitions relation $\leadsto_{{\sf M}}$ over a set of states that splits into

• –

principal transitions $\leadsto_{{\mathsf{p}}}$, that corresponds to the evaluation steps on the calculus, and

• –

overhead transitions $\leadsto_{{\mathsf{o}}}$, that are specific of the machine,

• •

an evaluation strategy $\to$ in the $\lambda$-calculus, and

• •

a decoding $(\cdot)_{\downarrow}$ of states of ${\sf M}$ into terms,

${\sf M}$ correctly implements $\rightarrow$ via $(\cdot)_{\downarrow}$ whenever $({\sf M},\rightarrow,(\cdot)_{\downarrow})$ forms an implementation system, i.e. whenever the following conditions are fulfilled (where $s$ and $s^{\prime}$ stand for generic states of ${\sf M}$):

1. (1)

Initialization: there is an encoding $\underline{\cdot}$ of terms such that $\underline{t}_{\downarrow}=t$; 2. (2)

Principal projection: $s\leadsto_{{\mathsf{p}}}s^{\prime}$ implies $s_{\downarrow}\rightarrow s^{\prime}_{\downarrow}$; 3. (3)

Overhead transparency: $s\leadsto_{{\mathsf{o}}}s^{\prime}$ implies $s_{\downarrow}=s^{\prime}_{\downarrow}$; 4. (4)

Determinism: $\leadsto_{{\sf M}}$ is deterministic; 5. (5)

Halt: ${\sf M}$ final states (to which no transition applies) decode to $\rightarrow$-normal terms; 6. (6)

Overhead Termination: $\leadsto_{{\mathsf{o}}}$ terminates.

Our notion of implementation, tuned towards complexity analyses, requires a perfect match between the number of steps of the strategy and the number of principal transitions of the execution.

Theorem 5.4 (Machine Implementation, (Accattoli and

Guerrieri, 2017)).

If a machine ${\sf M}$, a strategy $\rightarrow$ on $\lambda$-terms and a decoding $\cdot_{\downarrow}$ form an implementation system then:

1. (1)

Executions to derivations*: for any ${\sf M}$-execution $\rho\colon\underline{t}\leadsto_{{\sf M}}^{*}s$ there is a $\rightarrow$-derivation $d\colon t\rightarrow^{*}s_{\downarrow}$.* 2. (2)

Derivations to executions*: for every $\rightarrow$-derivation $d\colon t\rightarrow^{*}u$ there is an ${\sf M}$-execution $\rho\colon\underline{t}\leadsto_{{\sf M}}^{*}s$ such that $s_{\downarrow}=u$.* 3. (3)

Principal matching*: in both previous points the number $|\rho|_{{\mathsf{p}}}$ of principal transitions in $\rho$ is exactly the length $|d|$ of the derivation $d$, i.e. $|d|=|\rho|_{{\mathsf{p}}}$.*

The crumbling implementation system.

The states of the Crumble GLAM are crumbles. Its principal transitions are those labeled with $\{{\beta_{v}},\textsf{ift},\textsf{iff},\textsf{ife},\textsf{@e}\}$, while the overhead transitions are those labeled with $\{\mathsf{sub}_{\mathit{var}},\mathsf{sub}_{l},\mathsf{sub}_{\mathsf{if}}\}$. We can now show that the Crumble GLAM, Pif evaluation $\rightarrow_{\mathsf{pif}}$ and the read-back $(\cdot)_{\downarrow}$ form an implementation system, that is, that the Crumble GLAM implements the Pif calculus.

We are going to provide five of the six sufficient conditions required by the implementation theorem (Thm. 5.4); the sixth one, the termination of overhead transitions, is subsumed by the finer complexity analysis in Subsect. 5.3.

The sufficient conditions, as usual, are proved by means of a few invariants of the machine, given by Lemma 5.5 below. These invariants are essentially the properties of the translation in Lemma 4.5 extended to all reachable crumbles. One of them—namely contextual decoding—however, is weaker because reachable crumbles do not necessarily have the same nice structure as the initial crumbles obtained by translation of a term, as the next remark explains.

Remark 5.1.

Even though not all crumble contexts unfold to contexts, crumble contexts obtained by decomposing crumbles given by the translation of terms do (Lemma 4.5.5)—this is the contextual decoding property. Unfortunately, it is not preserved by evaluation. Consider the crumble $c\coloneqq\underline{(\lambda x.x(xx))\,I}=((\lambda x.(xy,[y{\shortleftarrow}xx]))\overline{I},\epsilon)$ with $\overline{I}=\lambda z.{(z,\epsilon)}$. Clearly, $c=\langle\underline{(\lambda x.x(xx))\,I}\rangle$ where $\langle\cdot\rangle_{\downarrow}=\langle\cdot\rangle$ is a context. After one ${\beta_{v}}$ step, the crumble $c$ reaches $(xy,[y{\shortleftarrow}xx][x{\shortleftarrow}\overline{I}])=C\langle(\overline{I},\epsilon)\rangle$ for $C\coloneqq(xy,[y{\shortleftarrow}xx][x{\shortleftarrow}\langle\cdot\rangle])$. But $C$ unfolds to $C_{\downarrow}=\langle\cdot\rangle(\langle\cdot\rangle\langle\cdot\rangle)$, which is not a $\lambda$-context.

Lemma 5.5 (Invariants for the Crumble GLAM).

††margin:

Proof p. Proof of

For every reachable crumble $c$ in the Crumble GLAM:

1. (1)

Freshness:* $c$ is well-named.* 2. (2)

Closure:* ${\sf fv}(c)=\emptyset$.* 3. (3)

Bodies:* every body occurring in $c$ is a subterm (up to renaming) of the initial crumble.* 4. (4)

Weak contextual decoding:* for every decomposition $C\langle(b,e_{v})\rangle$ where $b$ is not a crumbled value, if $C^{\prime\prime}$ is a prefix of $C$ then $C^{\prime\prime}_{\downarrow}$ is a right v-context.*

Freshness and closure are invariants needed to ensure the basic functioning of the machine. The bodies invariant corresponds to what is sometimes called subterm invariant. It is the key invariant for complexity analyses, as it allows to bound the size of duplicated subterms (that are always abstractions) using the size of the initial term. Usually, it is only needed for complexity analyses, while here it is needed for the implementation theorem as well (namely, only for the proof of the weak contextual decoding invariant). The weak contextual decoding invariant, finally, is essential to show that principal transitions of the Crumble GLAM project on evaluation steps in $\lambda_{\mathsf{Plot}}^{\mathsf{if}}$.

Theorem 5.6 (Implementation).

††margin:

Proof p. Proof of

Let $c$ be a crumble reachable by the Crumble GLAM.

1. (1)

Initialization: ** $\underline{t}_{\downarrow}=t$ for every term $t$. 2. (2)

Principal projection: ** if $c\rightarrow_{a}d$ then $c_{\downarrow}\rightarrow_{a}d_{\downarrow}$, for any rule $a\in\{{\beta_{v}},\textsf{ift},\textsf{iff},\textsf{ife},\textsf{@e}\}$. 3. (3)

Overhead transparency: ** if $c\rightarrow_{a}d$ then $c_{\downarrow}=d_{\downarrow}$ for any rule $a\in\{\mathsf{sub}_{\mathit{var}},\mathsf{sub}_{l},\mathsf{sub}_{\mathsf{if}}\}$. 4. (4)

Determinism: ** the transition $\rightarrow_{\mathsf{Cr}}$ is deterministic. 5. (5)

Halt: ** if $c$ is $\mathsf{Cr}$-normal then $c_{\downarrow}$ is $Pif$-normal. 6. (6)

Overhead termination: ** $\rightarrow_{a}$ terminates, for any rule $a\in\{\mathsf{sub}_{\mathit{var}},\mathsf{sub}_{l},\mathsf{sub}_{\mathsf{if}}\}$.

Therefore, the Crumble GLAM, Pif evaluation $\rightarrow_{\mathsf{pif}}$, and the read-back $(\cdot)_{\downarrow}$ form an implementation system.

5.3. Complexity for the closed case

To estimate the cost of the Crumble GLAM, we provide first an upper bound on the number of overhead transitions—namely the substitution ones $\mathsf{sub}_{\mathit{var}}$, $\mathsf{sub}_{l}$, and $\mathsf{sub}_{\mathsf{if}}$—in an execution $\rho$ as a function of the number $|\rho|_{{\mathsf{p}}}$ of principal transitions. Then we discuss the cost of implementing single transitions. Last, by composing the two analyses we obtain the total cost, that is linear in the number of principal transitions and in the size of the initial term/crumble, that is, the machine is bilinear.

Number of transitions: non-renaming substitutions

Let $\rho:c_{0}\rightarrow_{\mathsf{Cr}}^{*}c$ be an execution (i.e. a sequence of transitions) in the Crumble GLAM and let $|\rho|_{{\mathsf{p}}},|\rho|_{\mathsf{sub}_{\mathit{var}}},|\rho|_{\mathsf{sub}_{l}},|\rho|_{\mathsf{sub}_{\mathsf{if}}}$ be the number of principal, $\mathsf{sub}_{\mathit{var}}$, $\mathsf{sub}_{l}$, and $\mathsf{sub}_{\mathsf{if}}$ transitions in $\rho$, respectively. Clearly, a $\mathsf{sub}_{l}$ transition can only be immediately followed by a ${\beta_{v}}$ or a @e transition (since $\rightarrow_{\mathsf{Cr}}$ is deterministic), and so $|\rho|_{\mathsf{sub}_{l}}\leq|\rho|_{{\beta_{v}}}+|\rho|_{\textsf{@e}}+1$. Similarly, a $\mathsf{sub}_{\mathsf{if}}$ transition is immediately followed by a ift, a iff or a ife transition. Therefore, $|\rho|_{\mathsf{sub}_{l}}+|\rho|_{\mathsf{sub}_{\mathsf{if}}}\leq|\rho|_{{\mathsf{p}}}+1$.

Number of transitions: renaming steps

The analysis of $|\rho|_{\mathsf{sub}_{\mathit{var}}}$ steps is subtler. A variable crumble is a crumble of the form $(x,e)$. The number of $\mathsf{sub}_{\mathit{var}}$ transitions is bounded by the number of variable crumbles out of bodies appearing in evaluation position along an execution $\rho\colon c_{0}\to^{*}c$. These can be due to the following reasons:

1. (1)

Static: variable crumbles out of bodies in the initial state $c_{0}$; 2. (2)

Dynamic: variable crumbles obtained dynamically. In turn, these are divided into (see also the discussion after Prop. 5.7):

1. (a)

Copy: variable crumbles occurring in the bodies of abstractions and $\mathsf{if}\mbox{-}\mathsf{then}\mbox{-}\mathsf{else}$ (and thus frozen) that become active because the construct is evaluated and the body exposed; 2. (b)

Creation: variable crumbles that cannot be traced back to variable crumbles appearing in prefixes of the execution.

We now show that the crumbling translation does not produce any variable crumbles out of bodies, but one, if the original term is itself a variable. Therefore, the contribution of point 1 is at most 1. We need a measure, counting variable crumbles out of bodies. Note that a variable crumble $(x,e)$ appearing in a crumble context $C$ rather takes the form $[y{\shortleftarrow}x]e$, which is why the following measure counts the substitutions containing only a variable.

[TABLE]

Proposition 5.7.

††margin:

Proof p. Proof of

Let $t$ be a term and $v$ a value. Then:

1. (1)

$|\underline{t}|_{\textup{var}}\leq 1$; and $|\underline{t}|_{\textup{var}}=1$ if and only if $t$ is a variable; 2. (2)

$|\overline{v}|_{\textup{var}}\leq 1$; and $|\overline{v}|_{\textup{var}}=1$ if and only if $v$ is a variable.

Let us now discuss the variable crumbles of point 2.a (dynamic copy). By the bodies invariant (Lemma 5.5.3), these pairs appear in a body of the initial crumble. By the bodies property of the crumbling translation (Lemma 4.5.4), all these bodies are the translation of a term, and—by using Prop. 5.7 again—we obtain that each such body contributes at most with one variable crumble. Since each body is exposed by one $\rightarrow_{{\beta_{v}}}$ or $\rightarrow_{\textsf{ift}}$ or $\rightarrow_{\textsf{iff}}$ transition, we have that the variable crumbles of point 2.a are bounded by $|\rho|_{{\mathsf{p}}}$.

Last, we bound the number of variable crumbles at point 2.b (dynamic creation). There is only one rule that can create a new variable crumble (and exactly one), namely $\rightarrow_{{\beta_{v}}}$ when the argument of the $\beta$-redex is a variable. For instance,

[TABLE]

where the created variable crumble is $(y,[y{\shortleftarrow}\lambda z.z])$. Then the number of variable crumbles at point 2.b is bounded by the number of $\rightarrow_{{\beta_{v}}}$ transitions, itself bounded by $|\rho|_{{\mathsf{p}}}$.

The following lemma sums up the previous discusssions.

Lemma 5.8.

Let $\rho:c_{0}\rightarrow_{\mathsf{Cr}}^{*}c$ be a Crumble GLAM execution.

1. (1)

Linear number of non-renamings substitutions*: $|\rho|_{\mathsf{sub}_{l}}+|\rho|_{\mathsf{sub}_{\mathsf{if}}}\leq|\rho|_{{\mathsf{p}}}+1$.* 2. (2)

Linear number of renamings*: $|\rho|_{\mathsf{sub}_{\mathit{var}}}\leq 2|\rho|_{{\mathsf{p}}}+1$.* 3. (3)

Linear number of substitutions*: $|\rho|_{\mathsf{sub}_{l}}+|\rho|_{\mathsf{sub}_{\mathit{var}}}+|\rho|_{\mathsf{sub}_{\mathsf{if}}}\leq 3|\rho|_{{\mathsf{p}}}+2$.*

Cost of single transitions

Performing a single transition $\to$ in the Crumble GLAM consists of four operations:

1. (1)

Search: locating the next redex; 2. (2)

Unplugging: splitting the crumble to be reduced into a crumble context $C$ and the crumble $c$ that is the redex at top level; 3. (3)

Rewriting: applying a rewriting rule to the crumble $c$, obtaining a new crumble $d$; 4. (4)

Plugging: putting the new crumble back into the crumble context obtaining $C\langle d\rangle$.

The search for redexes is embedded into the definition of the rules, via the contextual closure. The technical definition of plugging and unplugging of crumbles into a crumble context is quite involved and, if implemented literally, is not constant time.

To ease the reasoning, in this section we assume that search and (un)plugging have negligible cost and show that the total cost of rewriting is bilinear. In Appendix D.4 (p. D.4) we introduce a slight variant of the Crumble GLAM, the Pointed Crumble GLAM, that adds a transition for searching redexes and removes the need for plugging and unplugging. A further analysis of the Pointed Crumble GLAM shows that the total cost of search and (un)plugging is bilinear and thus negligible, justifying the results of this section.

Cost of single transitions: ${\beta_{v}}$ transitions

We denote by $|t|$, $|c|$, $|e|$ and $|b|$ the size of terms, crumbles, environments and bites, respectively, defined as follows:

\begin{array}[]{rcl\colspace rcl\colspace rcl}|x|=|\mathsf{true}|=|\mathsf{false}|=|\mathsf{err}|&\coloneqq&1\\ |\lambda x.{t}|&\coloneqq&|t|+1\\ |tu|&\coloneqq&|t|+|u|+1\\ |\mathsf{if}\,t\,\mathsf{then}\,u\,\mathsf{else}\,s|&\coloneqq&\lx@intercol|t|+|u|+|s|+1\hfil\lx@intercol\\ |\epsilon|&\coloneqq&0\\ |e[x{\shortleftarrow}b]|&\coloneqq&|e|+|b|\\ |(b,e)|&\coloneqq&|b|+|e|\end{array}

The cost of each ${\beta_{v}}$ transition (that needs to perform a copy of the crumble in the abstraction in order $\alpha$-rename it) is bound by the size of the copied crumble. By the bodies invariant (Lemma 5.5.3) the abstraction is the $\alpha$-renaming of one the abstractions already present in the initial crumble. Therefore the cost of a ${\beta_{v}}$ transition is bound by the size of the initial crumble. The next lemma shows that the size of the initial crumble is linear in the size of the initial term translating to the crumble. Therefore, the cost of a ${\beta_{v}}$ transition is linear by the size of the initial term.

Lemma 5.9 (Size of translated terms).

††margin:

Proof p. Proof of

Let $t$ be a term and $v$ a value. Then $|\underline{t}|\leq 5|t|$ and $|\overline{v}|\leq 5|v|$.

Cost of single transitions: substitutions

The cost of $\mathsf{sub}_{l}$, $\mathsf{sub}_{\mathit{var}}$, and $\mathsf{sub}_{\mathsf{if}}$ transitions depends on the choice of data structures for implementing the machine. Following the literature on global environment machines (Accattoli and Barras, 2017), we assume the global environment to be implemented as a store and variable occurrences to be implemented as pointers into the store, so that lookup in the environment can be performed in constant time on a Random Access Machine (RAM). As for the cost of actually performing the replacement of $x$ with $e_{v}(x)$ in the $\mathsf{sub}_{\mathit{var}},\mathsf{sub}_{l}$ and $\mathsf{sub}_{\mathsf{if}}$ rules, it can be done in constant time by copying the pointer to $e_{v}(x)$. This is possible because the actual copy, corresponding to $\alpha$-renaming, is done in the ${\beta_{v}}$ step. Thus, single substitution transitions have constant cost.

Cost of single transitions: conditionals and errors

It is immediate that—if one excludes plugging and unplugging—these transitions have constant cost.

Cost of executions.

Summing up all the analyses in this section we obtain the following theorem.

Theorem 5.10 (The Crumble GLAM is bilinear up to search and (un)plugging).

††margin:

Proof p. Proof of

For any closed term $t$ and any Crumble GLAM execution $\rho\colon\underline{t}\rightarrow_{\mathsf{Cr}}^{*}c$, the cost of implementing $\rho$ on a RAM is $O((|\rho|_{{\mathsf{p}}}+1)\cdot|t|)$ plus the cost of plugging and unplugging.

OCaml implementation.

In Section D.4 we introduce the Pointed Crumble GLAM, a refinement of the Crumble GLAM making explicit the search for redexes and removing the need for (un)plugging, and having the same complexity: the cost for searching redexes and (un)plugging is negligible. Moreover, an implementation in OCaml of the Pointed Crumble GLAM can be found in Appendix F (p. F), together with the code that implements the crumbling translation. The Appendix also discusses in detail a parsimonious choice of data structures for the implementation of pointed environments.

6. The Open Case

6.1. The Fireball Calculus

In this section we recall the fireball calculus $\lambda_{\mathsf{fire}}$, the simplest presentation of Open CbV, and extend it with conditionals. The extension is completely modular. For the issues of Plotkin’s setting with respect to open terms and for alternative presentations of Open CbV, we refer the reader to Accattoli and Guerrieri (2016, 2018).

The fireball calculus was introduced without a name and studied first by Paolini and Ronchi Della Rocca (1999); Ronchi Della Rocca and Paolini (2004). It has then been rediscovered by Grégoire and Leroy (2002) to improve the implementation of Coq, and later by Accattoli and Sacerdoti Coen (2015) to study cost models, where it was also named. We present it following Accattoli and Sacerdoti Coen (2015), changing only inessential, cosmetic details.

The fireball calculus.

The conditional fireball calculus $\lambda_{\mathsf{fire}}^{\mathsf{if}}$ is defined in Fig. 2. The conditional part is exactly as in the closed case. The idea is that the values of the Pif calculus are generalised to fireballs, by adding inert terms. Fireballs (noted $f$) and inert terms (noted $i$) are defined by mutual induction (in Fig. 2). For instance, $x$ and $\lambda x.y$ are fireballs as values, while $y(\lambda x.x)$, $xy$, and $(z(\lambda x.x))(zz)(\lambda y.(zy))$ are fireballs as inert terms.

The main feature of inert terms is that they are open, normal, and that when plugged in a context they cannot create a redex, hence the name “inert”. Essentially, they are the neutral terms of Open CbV. In Grégoire and Leroy’s presentation (Grégoire and Leroy, 2002), inert terms are called accumulators and fireballs are simply called values. Variables are, morally, both values and inert terms. In Accattoli and Sacerdoti Coen (2015) they were considered as inert terms, while here, for minor technical reasons we prefer to consider them as values and not as inert terms—the change is inessential.

Evaluation rules.

First, CbV $\beta$-reduction is replaced by call-by-fireball $\beta$-reduction $\rightarrow_{\beta_{\!f}}$: the $\beta$-rule can fire, lighting the argument, only if the argument is a fireball (fireball is a catchier version of fire-able term). We actually distinguish two sub-rules: the usual one that lights values, noted $\rightarrow_{{\beta_{v}}}$, and a new one that lights inert terms, noted $\rightarrow_{\beta_{i}}$ (see Fig. 2). Second, we include all the rules about conditionals and errors, exactly as before, obtaining the evaluation relation $\rightarrow_{\mathsf{c}\beta_{\!f}}$. Note that evaluation is weak: it does not reduce in abstraction nor $\mathsf{if}\mbox{-}\mathsf{then}\mbox{-}\mathsf{else}$ bodies.

We endow the calculus with the (deterministic) right-to-left evaluation strategy, defined via right f-contexts $R$—note the production $Rf$, forcing the right-to-left order. A more general calculus (without conditionals) is defined in Accattoli and Guerrieri (2016), for which the right-to-left strategy is shown to be complete. We omit details about the rewriting theory of the fireball calculus because our focus here is on implementations.

Example 6.1.

Let $t\coloneqq(\lambda z.{z(yz)})(\lambda x.{x})$. Then, $t\rightarrow_{\beta_{\!f}}(\lambda x.{x})(y\,(\lambda x.{x}))\rightarrow_{\beta_{\!f}}y\,(\lambda x.{x})$, where the final term $y\,(\lambda x.{x})$ is a fireball (and $\beta_{\!f}$-normal).

Properties.

As discussed in Sect. 5, Closed CbV enjoys harmony (Prop. 2.1). The fireball calculus $\lambda_{\mathsf{fire}}$ satisfies an analogous property in the open setting by replacing abstractions with fireballs; we here further extend it to conditionals (Prop. 6.2.1 below). The key property of inert terms is summarised by Prop. 6.2.2: substitution of inert terms does not create or erase $\mathsf{c}\beta_{\!f}$-redexes, and hence can always be avoided. It plays a role in the design of the open abstract machine of the next section.

Proposition 6.2 (Properties of $\lambda_{\mathsf{fire}}^{\mathsf{if}}$).

††margin:

Proof p. Proof of

Let $t,u$ be terms.

1. (1)

Open harmony:* $t$ is $\mathsf{c}\beta_{\!f}$-normal if and only if $t$ is a fireball.* 2. (2)

Inert substitutions and evaluation commute:* Let $i$ be an inert term. Then $t\rightarrow_{\mathsf{c}\beta_{\!f}}u$ if and only if $t\{x{\shortleftarrow}i\}\rightarrow_{\mathsf{c}\beta_{\!f}}u\{x{\shortleftarrow}i\}$.*

6.2. The Open Crumble GLAM

Here we extend the Crumble GLAM defined in Sect. 5 to the case of open terms, implementing Open (Conditional) CbV, i.e. the conditional fireball calculus $\lambda_{\mathsf{fire}}^{\mathsf{if}}$: in this way we obtain the Open Crumble GLAM. The extension impacts on the core $\lambda$-calculus, while conditionals are essentially orthogonal to the issues of open terms.

Evaluated environments.

First, we need to discuss the environments under which evaluation takes place. In the open case, $v$-crumbles and $v$-environments generalize to $f$-crumbles and $f$-environments, and are denoted as follows:

[TABLE]

Recall that in the Crumble GLAM the already evaluated coda of the environment is made out only of practical values. Unfortunately, a syntactic characterisation of $f$-environments (and $f$-crumbles) is more involved than the simple definition of $v$-environments.

In the Crumble GLAM, to check whether a bite $b$ is in normal form with respect to a $v$-environment $e_{v}$, it suffices to check whether $b$ is a practical value. In the open case, looking at the syntactic structure of the term is not enough: some applications are now normal, for example the bite $y\,x$ is normal with respect to the environment $e\coloneqq[x{\shortleftarrow}I]$, but not all of them are normal, for instance $(x\,y,[x{\shortleftarrow}I])\rightarrow_{\mathsf{sub}_{l}}(I\,y,[x{\shortleftarrow}I])$ as in the closed case (exact definitions are given below). Because of this additional complication, we are going to define $f$-environments directly in terms of their ’semantics’, i.e. of their read-back to terms. Intuitively, fully evaluated $f$-environments should correspond to substitutions of fully evaluated terms in $\lambda_{\mathsf{fire}}^{\mathsf{if}}$. And since by harmony normal forms in $\lambda_{\mathsf{fire}}^{\mathsf{if}}$ are simply fireballs, it suffices to request that the read-back of every entry in a $f$-environment is a fireball.

Let us now define $f$-environments formally: $e_{\!f}$ is a $f$-environment (resp. $c_{\!f}$ is a $f$-crumble) if for any environment context $E$ (resp. any crumble context $C$) and any crumble $c$ such that $e_{\!f}=E\langle c\rangle$ (resp. $c_{\!f}=C\langle c\rangle$) the following two conditions hold:

1. (1)

Read-back to fireballs: $c_{\downarrow}$ is a fireball, and 2. (2)

Unchaining practical values: if $c_{\downarrow}$ is a practical value, then $c=(v,e)$ for some practical value $v$ and some $e$.

The second requirement forbids $v$ to be a variable and is crucial for capturing the correct behaviour of the substitution rule $\rightarrow_{\mathsf{sub}_{\mathit{var}}}$, which removes the malicious chains of substitutions (of variables for variables) discussed in Sect. 5.

Transitions.

The transitions of the Open Crumble GLAM:

[TABLE]

1. (1)

if $v=\lambda x.e$ or $v=\mathsf{err}$ 2. (2)

if $v\in\{\mathsf{true},\mathsf{false},\mathsf{err}\}$ 3. (3)

if $x\in\mathsf{dom}(e_{\!f})$

Top level transitions are then closed by crumble contexts by setting $C\langle c\rangle\rightarrow_{a}C\langle d\rangle$ if $c\mapsto_{a}d$ for $a\in\{{\beta_{v}},\mathsf{sub}_{\mathit{var}},\mathsf{sub}_{l},\mathsf{sub}_{\mathsf{if}},\textsf{ift},\textsf{iff},\textsf{ife},\textsf{@e}\}$. The transition relation $\rightarrow_{\mathsf{oCr}}$ of the Open Crumble GLAM is defined as the union of all these rules. A principal transition of the Open Crumble GLAM is a transition $\rightarrow_{a}$ for any rule $a\in\{\beta_{\!f},\textsf{ift},\textsf{iff},\textsf{ife},\textsf{@e}\}$.

There are only two differences with the transitions of the Crumble GLAM. First, $\rightarrow_{{\beta_{v}}}$ is now noted $\mapsto_{\beta_{\!f}}$ and yet it is identical to the one in the closed case (the comments about $\alpha$-renaming given in Sect. 5 still hold). This is because there is a subtle difference: the argument of the $\beta$-redex may be a variable (which is a value) substituted by a inert term in the environment, thus becoming a $\rightarrow_{\beta_{i}}$ step (and not a $\rightarrow_{{\beta_{v}}}$ step) when read-back in $\lambda_{\mathsf{fire}}^{\mathsf{if}}$. Second, there is a slightly different side condition for the substitution transitions: it requires not only that a variable is defined in $e_{\!f}$ (like in the closed case), but also that the corresponding term in the environment is a practical value (and not an inert term nor a variable).

Note that the substitution transitions substitute values only. The environment $e_{\!f}$ may contain also bites that are variables or applications, but these bites are not substituted: this choice is justified by the property of $\lambda_{\mathsf{fire}}^{\mathsf{if}}$ stated in Prop. 6.2.2. Besides, avoiding the substitution of inert terms is a prerequisite for efficiency of the machine, that would otherwise be subjected to an exponential overhead due to size explosion, see for example Accattoli and Sacerdoti Coen (2015); Accattoli and Guerrieri (2017).

The harmony between evaluation rules and the syntactic definition of normal forms is witnessed by the following property.

Proposition 6.3 (Harmony for the Open Crumble GLAM).

††margin:

Proof p. Proof of

A crumble $c$ is $\mathsf{oCr}$-normal if and only if it is a $f$-crumble.

Example 6.4.

Recall that $\overline{\delta}=(\lambda x.xx,\epsilon)$. In Ex. 5.2 we noted that the (open) crumble $\underline{\delta\delta(xx)}$ was stuck in the Crumble GLAM. Now instead it correctly reduces, never reaching a normal form:

[TABLE]

Implementation Theorem

The proof of the implementation theorem for the Open Crumble GLAM follows the same structure as for the Crumble GLAM in Subsect. 5.2, relying on similar but subtler invariants that can be found in the appendix, Lemma E.9.

Theorem 6.5 (Implementation).

††margin:

Proof p. Proof of

Let $c$ be a crumble that is reachable by the Open Crumble GLAM.

1. (1)

Initialization: ** $\underline{t}_{\downarrow}=t$ 2. (2)

Principal projection: ** if $c\rightarrow_{a}d$ then $c_{\downarrow}\rightarrow_{a}d_{\downarrow}$ for $a\in\{\beta_{\!f},\textsf{ift},\textsf{iff},\textsf{ife},\textsf{@e}\}$. 3. (3)

Overhead transparency: ** if $c\rightarrow_{a}d$ then $c_{\downarrow}=d_{\downarrow}$ for any rule $a\in\{\mathsf{sub}_{\mathit{var}},\mathsf{sub}_{l},\mathsf{sub}_{\mathsf{if}}\}$. 4. (4)

Determinism: ** the transition $\rightarrow_{\mathsf{oCr}}$ is deterministic. 5. (5)

Halt: ** if $c$ is $\mathsf{oCr}$-normal then $c_{\downarrow}$ is $\mathsf{c}\beta_{\!f}$-normal. 6. (6)

Overhead termination: ** $\rightarrow_{a}$ terminates, for any rule $a\in\{\mathsf{sub}_{\mathit{var}},\mathsf{sub}_{l},\mathsf{sub}_{\mathsf{if}}\}$.

Therefore, the Open Crumble GLAM, the right-to-left conditional fireball evaluation $\rightarrow_{\mathsf{c}\beta_{\!f}}$ and the read-back $(\cdot)_{\downarrow}$ form an implementation system.

Complexity

The complexity analysis is identical to the one in Subsect. 5.3. Indeed, once the search for the next redex and (un)plugging are neglected, the two machines only differ by the additional $O(1)$ side condition for the substitution transitions.

Theorem 6.6 (The Open Crumble GLAM is bilinear up to search and (un)plugging).

For any term $t$ and any Open Crumble GLAM execution $d\colon\underline{t}\rightarrow_{\mathsf{oCr}}^{*}c$, the cost of implementing $\rho$ on a RAM is $O((|\rho|_{{\mathsf{p}}}+1)\cdot|t|)$ plus the cost of plugging and unplugging.

OCaml implementation

Following the same pattern of the closed case, in Appendix E.3 (p. E.3) we introduce a machine making explicit the search for redexes and removing the need of (un)plugging, so as to show that their cost is negligible. The OCaml code implementing this further machine is in Appendix F (p. F), together with a detailed discussion of the adopted data structures. The code for the open and closed machines is identical but for five lines: three implement the additional check for practical values in the substitution transitions, the others consider also inert terms in the search transition.

7. Extensions

Left-to-right CbV

The (right-to-left) Crumble GLAM can also implement a left-to-right strategy for the Pif calculus. The only change concerns the crumbling transformation, that on applications has to put the environment coming from the (transformation of the) left subterm on the right of the one coming from the right subterm.

Call-by-need

The crumbling technique applies also to call-by-need machines. There are however a few differences. First, the machine does no longer explore sequentially the environment from right-to-left, it rather starts on the left and then jumps back and forth, by need. Then the definition of evaluation contexts is trickier, especially in the open case.

Strong CbV

Simply designing an abstract machine for strong reduction is relatively easy. However the easy machines are not bilinear, and not even polynomial.

The needed optimisations to make them reasonable (i.e. polynomial or bilinear) are clear, they are the same at work in the open case (or in the call-by-name case):

1. (1)

substitute only abstraction and not inert terms, and 2. (2)

do not substitute abstractions on variable occurrences that are not applied.

These principles however have different consequences in different settings. In particular, 2 implies that some abstraction are kept shared forever, and a strong CbV approach has to evaluate them (while the open setting does not) and only once, thus it has to evaluate them while they are shared, adding a call-by-need flavor.

There are two difficulties. First, the specification of the search for redexes, that becomes involved and requires many machine transitions—the crumbling technique is meant to help here. Second, the proof of correctness of the machine.

All proofs of correctness in the literature (including those in this paper) are simulations up to sharing based on a bijection of $\beta$-redexes (or principal steps) between the abstract machine and the $\lambda$-calculus strategy (one half of the bijection is the principal projection property of implementation systems in Subsect. 5.2, the other half is implied by the other properties).

The evaluation under shared abstraction required by CbV strong evaluation breaks the usual bijection of $\beta$-redexes (as one $\beta$-transition of the machine is mapped to many $\beta$-steps on the calculus, and not necessarily those of a standard strategy), thus forbidding to employ the standard technique for proving correctness.

The new proof technique for correctness for reasonable strong CbV and the intricacies of the search for redexes in the strong case, do deserve to be studied carefully, and are thus left to future work.

8. Conclusions

This paper studies abstract machines working on crumbled forms with respect to design, efficiency, scalability, and implementations, putting emphasis on the role played by environments and providing a detailed technical development. In particular, we study the crumble setting on top of global environments—in future work we would like to explore the more technical case of local environments.

At the level of design, switching to crumbled forms removes the need for machine data structures such as the applicative stack or the dump, as they are encoded in crumbled environments.

At the level of efficiency, the evaluation of crumbled forms does not require any overhead: crumble abstract machines are linear in the number of steps of the calculus and in the size of the initial term, exactly as ordinary abstract machines with global environments.

At the level of scalability, everything—including the complexity—smoothly scales up from the closed case, relevant for programming languages, to the more delicate case of open terms, needed to implement proof assistants. As shown in Appendix A, CPS translations do not smoothly scale up to the open case (contrary to what claimed by Danvy and Filinski (1992)), so that our work shows an advantage of the crumbling transformation in this setting.

At the level of implementations, we stress the different operations on crumbled environments (sequential access and concatenation) and provide a concrete implementation, which does not suffer from the potential slowdown of crumbled forms pointed out by Kennedy (2007) (see Appendix A).

In future work we plan to apply our results to the design of abstract machines for strong call-by-value and call-by-need evaluation. Preliminary results suggest that the simplification to the code noticed in the open case is preserved and even amplified in the harder case of strong evaluation.

Acknowledgments

This work has been partially funded by the ANR JCJC grant COCA HOLA (ANR-16-CE40-004-01) and by the EPSRC grant EP/R029121/1 “Typed Lambda-Calculi with Sharing and Unsharing”.

Technical Appendix

Appendix A Comments on Related Works

Here we discuss in detail Kennedy’s potential slowdown and provide a counter-example to the scalability of the CPS transformation to open terms.

Kennedy

Kennedy (2007) compares three different calculi: a monadic calculus, which has ES, a calculus of administrative normal forms (ANFs) and the image of a CPS transformation. In the monadic calculus ${\beta_{v}}$-redexes can be hidden by ES which need to be commuted to reveal the ${\beta_{v}}$-redex. Kennedy shows an example (see Fig. 3) where the number of commutations is not bounded linearly by the number of ${\beta_{v}}$-steps and blames the inefficiency of his compiler on that. In his example, the number of commutations is quadratic in the number of ${\beta_{v}}$-steps, since the $i^{\textup{th}}$ ${\beta_{v}}$-step is immediately followed by $i$ commutation steps.

ANFs are just canonical shapes of monadic terms where the topmost term and the body of each abstraction is a crumble, i.e. a term together with a list of ES that map variables to terms (instead of crumbles). Kennedy rightly observes that ANFs are not preserved by standard ${\beta_{v}}$-reduction and thus, after each ${\beta_{v}}$-step, some commutative steps are required to reach the ANF shape. The quadratic example by Kennedy stands in the ANF fragment. So, Kennedy too hastily concludes that the quadratic blowup also affects the ANF calculus.

However, Kennedy misses the fact that the ES in ANFs form a list and that the commutations steps altogether just implement the append function of two lists. Since append can be implemented in constant time, the complexity of evaluation in the ANF calculus is just linear (and not quadratic) in the number of ${\beta_{v}}$-steps. This is the same complexity we achieved for the Crumble and Open Crumble GLAM.

Danvy and Filinski

In Danvy and Filinski (1992) the CPS transformation is shown to scale up to open terms (their Theorem 2). On open terms, however, they consider Plotkin’s CbV operational semantics $\lambda_{\mathsf{Plot}}$, which is not adequate (it is adequate only for closed terms, see Accattoli and Guerrieri (2016, 2018)). When one considers one of the equivalent adequate CbV semantics in Accattoli and Guerrieri (2016, 2018) for the open case, for instance the fireball calculus $\lambda_{\mathsf{fire}}$, then the properties of the CPS no longer hold, in particular it does not commute with evaluation, as the following example shows. Take the following open term $t\coloneqq(\lambda x.{\lambda y.y})(zz)v$, where $v$ is a value, say a distinguished variable. In $\lambda_{\mathsf{Plot}}$ the term $t$ is ${\beta_{v}}$-normal, but in $\lambda_{\mathsf{fire}}$ we have:

[TABLE]

Now, consider the CPS translation $\mathtt{cps}(t)$ of $t$, according to the definition in Danvy and Filinski (1992). We use $\lambda$ for standard (“dynamic”, in Danvy’s terminology) abstraction, and $\Lambda$ and $@$ for “static” abstraction and application, respectively. If a generalized version of Theorem 2 in Danvy and Filinski (1992) held in the open case, one would expect that $@(\mathtt{cps}(t))I$ (where $I\coloneqq\lambda z.z$) evaluates to $v$, as $v$ is a value. But, even using an unrestricted $\beta$-reduction that goes under abstraction as evaluation, we obtain (we reduce all static redexes first, followed by all dynamic redexes):

[TABLE]

where $(zz)(\lambda x.v)$ is not even $\beta$-equivalent to $v$. The CPS translation—like Plotkin’s calculus—gets stuck trying to evaluate $zz$, whereas the term reduces to $v$ in the fireball calculus.

Summing up, we are not claiming that Theorem 2 in Danvy and Filinski (1992) is false, but just that it does not mean that their CPS transformation scale up to open terms: to prove scalability, one should use an adequate CbV evaluation for open terms (such as the one of the fireball calculus), instead of Plotkin’s one. Our counter-example shows that Danvy’s and Filinski’s CPS does not scale up to open terms with an adequate CbV operational semantics for them.

It is worth noting that this problem affects also other CPS translations, such as the ones defined by Plotkin (1975) or by Lassen (2005). Likely, this is the reason why Lassen (2005) states his Theorem 4.6 (the analogous of Theorem 2 in Danvy and Filinski (1992)) only for closed terms.

Appendix B Proofs of Sect. 2 (Pif Calculus)

Proof of 0 (Prop. 2.1).

“??”

Proof.

$(\Rightarrow)$**: **

Proof by induction on the structure of $t$.

• **•: **

Case $t$ value: trivial.

• **•: **

Case $t=us$ for some terms $u$ and $s$: we show that this case is not possible by deriving a contradiction. Since $t$ is $\rightarrow_{\mathsf{pif}}$normal, then $s$ is $\rightarrow_{\mathsf{pif}}$normal, and hence by i.h. $s$ is a value. Since $t$ is $\rightarrow_{\mathsf{pif}}$normal and $s$ is a value, then also $u$ must be $\rightarrow_{\mathsf{pif}}$normal, and hence a value. We proceed by cases on $u$, showing that no case is possible. $u$ cannot be a variable, because $t$ is closed; it cannot be an abstraction (because otherwise the rule $\rightarrow_{{\beta_{v}}}$ may be applied, contradicting the hypothesis that $t$ is $\rightarrow_{\mathsf{pif}}$normal); it cannot be a boolean or $\mathsf{err}$ (because otherwise the rule $\rightarrow_{\textsf{@e}}$ may be applied).

• **•: **

Case $t=\mathsf{if}\,u\,\mathsf{then}\,s\,\mathsf{else}\,r$ for some terms $u,s,r$: we show that this case is not possible by deriving a contradiction. Since $t$ is $\rightarrow_{\mathsf{pif}}$normal, then $u$ is $\rightarrow_{\mathsf{pif}}$normal, and hence by i.h. $u$ is a value. We proceed by cases on $u$, showing that no case is possible. $u$ cannot be a variable, because $t$ is closed; it cannot be an abstraction or $\mathsf{err}$ (because otherwise the rule $\rightarrow_{\textsf{ife}}$ may be applied, contradicting the hypothesis that $t$ is $\rightarrow_{\mathsf{pif}}$normal); it cannot be a boolean (because otherwise one of the rules $\rightarrow_{\textsf{ift}}$ or $\rightarrow_{\textsf{iff}}$ may be applied).

$(\Leftarrow)$**: **

By hypothesis, $t$ is a value. We proceed by cases on $t$. $t$ cannot be a variable, because by hypothesis $t$ is closed. If $t$ is an abstraction, then it is $\rightarrow_{\mathsf{pif}}$normal since $\rightarrow_{\mathsf{pif}}$ does not reduce under $\lambda$’s. Otherwise $t$ is a either a boolean or $\mathsf{err}$, which clearly are $\rightarrow_{\mathsf{pif}}$normal.

∎

Lemma B.1 (Composition of right v-contexts).

Let $R$ and $R^{\prime}$ be right v-contexts. Then their composition $R\langle R^{\prime}\rangle$ is a right v-context.

Proof.

By induction on the right v-context $R$. Cases:

• •

Hole, i.e. $R\coloneqq\langle\cdot\rangle$: then, $R\langle R^{\prime}\rangle=R^{\prime}$ is a right v-context by hypothesis.

• •

Right, i.e. $R\coloneqq tR^{\prime\prime}$: then, $R\langle R^{\prime}\rangle=tR^{\prime\prime}\langle R^{\prime}\rangle$ is a right v-context because $R^{\prime\prime}\langle R^{\prime}\rangle$ is a right v-context by i.h.

• •

Left, i.e. $R\coloneqq R^{\prime\prime}v$: then, $R\langle R^{\prime}\rangle=R^{\prime\prime}\langle R^{\prime}\rangle v$ is a right v-context because $R^{\prime\prime}\langle R^{\prime}\rangle$ is a right v-context by i.h.

• •

$\mathsf{if}\mbox{-}\mathsf{then}\mbox{-}\mathsf{else}$, i.e. $R\coloneqq(\mathsf{if}\,R^{\prime\prime}\,\mathsf{then}\,t\,\mathsf{else}\,u)$: then, $R\langle R^{\prime}\rangle=(\mathsf{if}\,R^{\prime\prime}\langle R^{\prime}\rangle\,\mathsf{then}\,t\,\mathsf{else}\,u)$ is a right v-context because $R^{\prime\prime}\langle R^{\prime}\rangle$ is a right v-context by i.h. ∎

Appendix C Proofs of Sect. 4 (preliminaries)

Lemma C.1.

Let $e\coloneqq[x_{1}{\shortleftarrow}b_{1}]\dots[x_{n}{\shortleftarrow}b_{n}]$ a well-named environment. If ${\sf fv}(t_{i})\cap\{x_{1},\dots,x_{i}\}=\emptyset$ for all $1\leq i\leq n$, then ${\sf fv}(e)=\bigcup_{i=1}^{n}{\sf fv}(b_{i})\smallsetminus\mathsf{dom}(e)$ and ${\sf fv}((b,e))=({\sf fv}(b)\cup{\sf fv}(e))\smallsetminus\mathsf{dom}(e)$.

Definition C.2 (Disjointedness).

Let $P$ and $P^{\prime}$ be two crumbles or environments: $P$ and $P^{\prime}$ are disjoint (noted $P\mathrel{\#}P^{\prime}$) if ${\sf fv}(P)\cap\mathsf{dom}(P^{\prime})=\emptyset$.

Definition C.3 (Composition of crumble contexts).

It is also possible to plug a crumble context $C^{\prime}$ into another crumble context $C$, as follows:

[TABLE]

The appending of an environment context $E$ to a crumble $(b,e^{\prime})$ is defined as $(b,e^{\prime})\mathrel{@}E\coloneqq(b,e^{\prime}E)$.

The notions of ${\sf fv}(\cdot)$ and $\mathsf{dom}(\cdot)$ are extended to crumble contexts by:

[TABLE]

An environment context $E$ is well-named if $E\langle x\rangle$ is well-named (for $x$ fresh) and a crumble context $C$ is well-named if $C\coloneqq\langle\cdot\rangle$ or $C\coloneqq(b,E)$ and $E$ is well-named.

Lemma C.4 (Decomposition of read back, auxiliary).

Let $e$ be an environment, and $x$ be a variable such that $x\notin\mathsf{dom}(e)\cup{\sf fv}(e)$. Then $(c\mathrel{@}[x{\shortleftarrow}b]e)_{\downarrow}=(c\mathrel{@}e)_{\downarrow}\{x{\shortleftarrow}(b,e)_{\downarrow}\}$ for every crumble $c$ and bite $b$.

Proof.

Let $c=(b^{\prime},e^{\prime})$. We proceed by structural induction on $e$:

• •

If $e=\epsilon$, then $(b,e)_{\downarrow}=b_{\downarrow}$ and hence $(b^{\prime},e^{\prime}[x{\shortleftarrow}b]e)_{\downarrow}=(b^{\prime},e^{\prime}[x{\shortleftarrow}b])_{\downarrow}=(b^{\prime},e^{\prime})_{\downarrow}\{x{\shortleftarrow}b_{\downarrow}\}=(b^{\prime},e^{\prime}e)_{\downarrow}[x{\shortleftarrow}(b,e)_{\downarrow}]$.

• •

Otherwise $e=e^{\prime\prime}[z{\shortleftarrow}b^{\prime\prime}]$ and then $(b,e)_{\downarrow}=(b,e^{\prime\prime})_{\downarrow}\{z{\shortleftarrow}b^{\prime\prime}_{\downarrow}\}$, so

[TABLE]

where $x\notin{\sf fv}(b^{\prime\prime}_{\downarrow})={\sf fv}(b^{\prime\prime})$ by Remark 4.1 and the hypothesis that $x\notin{\sf fv}(e)$. ∎

Lemma C.5 (Read-back vs. disjointedness).

For every crumble $c$ and environment $e$: if $c\mathrel{\#}e$, then $(c\mathrel{@}e)_{\downarrow}=c_{\downarrow}$.

Proof.

By structural induction on $e$:

• •

If $e\coloneqq\epsilon$ then $c\mathrel{@}e=c$ and hence $(c\mathrel{@}e)_{\downarrow}=c_{\downarrow}$.

• •

Otherwise $e\coloneqq e^{\prime}[x{\shortleftarrow}b]$. By i.h. (which can be applied since $c\mathrel{\#}e$ implies $c\mathrel{\#}e^{\prime}$, because $\mathsf{dom}(e^{\prime})\subseteq\mathsf{dom}(e)$), $(c\mathrel{@}e^{\prime})_{\downarrow}=c_{\downarrow}$. From $c\mathrel{\#}e$ it follows that $x\notin{\sf fv}(c)={\sf fv}(c_{\downarrow})$ (by Remark 4.1), so $c_{\downarrow}\{x{\shortleftarrow}b_{\downarrow}\}=c_{\downarrow}$. Therefore, $(c\mathrel{@}e)_{\downarrow}=c\mathrel{@}e^{\prime}_{\downarrow}\{x{\shortleftarrow}b_{\downarrow}\}=c_{\downarrow}\{x{\shortleftarrow}b_{\downarrow}\}=c_{\downarrow}$. ∎

Lemma C.6 (Decomposition of read back).

Let $c$ be a crumble and $e$ be an environment such that $c\mathrel{\#}e$. Then $(c\mathrel{@}[x{\shortleftarrow}b]e)_{\downarrow}\allowbreak=c_{\downarrow}\{x{\shortleftarrow}(b,e)_{\downarrow}\}$ for every bite $b$.

Note that Lemma C.6 does not hold without the hypothesis $c\mathrel{\#}e$. Indeed, take $c\coloneqq(y,\epsilon)$ and $e\coloneqq[y{\shortleftarrow}zz]$ with $x\neq y$: for any term $b$, one has $(c\mathrel{@}[x{\shortleftarrow}b]e)_{\downarrow}=zz\neq y=c_{\downarrow}\{x{\shortleftarrow}(b,e)_{\downarrow}\}$.

Proof.

According to Lemma C.4,

[TABLE]

where the last equality holds by Lemma C.5, since $c\mathrel{\#}e$. ∎

Proof of 0 (Prop. 4.2).

“??”

Proof.

By mutual induction on the term $t$ and the value $v$. Cases:

• •

Variable, i.e. $t\coloneqq x\eqqcolon v$; then, $\underline{t}=(x,\epsilon)$ and $\overline{v}=x$, thus $\underline{t}_{\downarrow}=x=t$ and $\overline{v}_{\downarrow}=x=v$.

• •

Error or Boolean: similar to the case Variable above.

• •

Abstraction, i.e. $t\coloneqq\lambda x.u\eqqcolon v$; then, $\underline{t}=(\lambda x.{\underline{u}},\epsilon)$ and $\overline{v}=\lambda x.{\underline{u}}$; by i.h., $\underline{u}_{\downarrow}=u$, hence $\underline{t}_{\downarrow}=\lambda x.{\underline{u}_{\downarrow}}=t$ and $\overline{v}_{\downarrow}=\lambda x.{\underline{u}_{\downarrow}}=v$.

• •

Conditional, case $t\coloneqq(\mathsf{if}\,v\,\mathsf{then}\,u\,\mathsf{else}\,s)$. Then $\underline{t}=(\mathsf{if}\,\overline{v}\,\mathsf{then}\,\underline{u}\,\mathsf{else}\,\underline{s},\epsilon)$. Since $\underline{t}_{\downarrow}=(\mathsf{if}\,\overline{v}_{\downarrow}\,\mathsf{then}\,\underline{u}_{\downarrow}\,\mathsf{else}\,\underline{s}_{\downarrow})$, we can conclude by using the i.h.

• •

Conditional, case $t\coloneqq(\mathsf{if}\,u\,\mathsf{then}\,s\,\mathsf{else}\,r)$ with $u$ not a value. Then $\underline{t}=(\mathsf{if}\,x\,\mathsf{then}\,\underline{s}\,\mathsf{else}\,\underline{r},\epsilon)\mathrel{@}[x{\shortleftarrow}q]e$ where $\underline{u}=(q,e)$. By i.h., $\underline{s}_{\downarrow}=s$ and $\underline{r}_{\downarrow}=r$. We can suppose that $(\{x\}\cup{\sf fv}(s)\cup{\sf fv}(r))\cap\mathsf{dom}(e)=\emptyset$ by the freshness condition in the definition of the transformation, and hence we can apply Lemma C.6 so that $\underline{t}_{\downarrow}=(\mathsf{if}\,x\,\mathsf{then}\,\underline{s}_{\downarrow}\,\mathsf{else}\,\underline{r}_{\downarrow})\{x{\shortleftarrow}\underline{u}_{\downarrow}\}=t$.

• •

Application of two values, i.e. $t=vv^{\prime}$; then, $\underline{t}=(\overline{v}\overline{v^{\prime}},\epsilon)$; by i.h., $\overline{v}_{\downarrow}=v$ and $\overline{v^{\prime}}_{\downarrow}=v^{\prime}$, so $\underline{t}_{\downarrow}=\overline{v}_{\downarrow}\overline{v^{\prime}}_{\downarrow}=t$.

• •

Application of a non-value to a value, i.e. $t\coloneqq uv$ where $u$ is not a value; then, $\underline{t}=(x\overline{v},[x{\shortleftarrow}s]e)=(x\overline{v},\epsilon)\mathrel{@}[x{\shortleftarrow}s]e$ where $\underline{u}=(s,e)$; we can suppose without loss of generality that $({\sf fv}(v)\cup\{x\})\cap\mathsf{dom}(e)=\emptyset$. By i.h., $\underline{u}_{\downarrow}=u$ and $\overline{v}_{\downarrow}=v$. By the freshness condition for $x$, we can apply Lemmas C.4 and C.5 so that $\underline{t}_{\downarrow}=(x\overline{v}\mathrel{@}e)_{\downarrow}\{x{\shortleftarrow}(s,e)_{\downarrow}\}=x\overline{v}_{\downarrow}\{x{\shortleftarrow}\underline{u}_{\downarrow}\}=t$.

• •

Application of a term to a non-value, i.e. $t\coloneqq us$ where $s$ is not a value; then, $\underline{t}=\underline{ux}\mathrel{@}([x{\shortleftarrow}r]e)$ where $\underline{s}=(r,e)$ and $\underline{ux}=(yx,[y{\shortleftarrow}q]e^{\prime})=(yx,\epsilon)\mathrel{@}([y{\shortleftarrow}q]e^{\prime})$ with $\underline{u}=(q,e^{\prime})$; we can suppose without loss of generality that $({\sf fv}(u)\cup\{x\})\cap\mathsf{dom}(e)=\emptyset$ and $\{x,y\}\cap\mathsf{dom}(e^{\prime})=\emptyset$. By i.h., $\underline{u}_{\downarrow}=u$ and $\underline{s}_{\downarrow}=s$. By the freshness condition for $x$ and $y$, we can apply Lemmas C.4 and C.5 so that $\underline{ux}_{\downarrow}=(yx\mathrel{@}e^{\prime})_{\downarrow}\{y{\shortleftarrow}(q,e^{\prime})_{\downarrow}\}=yx\{y{\shortleftarrow}\underline{u}_{\downarrow}\}=ux$ and $\underline{t}_{\downarrow}=(\underline{ux}\mathrel{@}e)_{\downarrow}\{x{\shortleftarrow}(r,e)_{\downarrow}\}=\underline{ux}_{\downarrow}\{x{\shortleftarrow}\underline{s}_{\downarrow}\}=ux\{x{\shortleftarrow}s\}=t$. ∎

Lemma C.7.

Let $c,d$ be crumbles, and $e$ be an environment. If $c_{\downarrow}=d_{\downarrow}$, then $(c\mathrel{@}e)_{\downarrow}=(d\mathrel{@}e)_{\downarrow}$.

Proof.

By induction on $e$:

• •

if $e\coloneqq\epsilon$, then we conclude because $c\mathrel{@}e=c$ and $d\mathrel{@}e=d$;

• •

if $e\coloneqq e^{\prime}[x{\shortleftarrow}b]$, by i.h. $(c\mathrel{@}e^{\prime})_{\downarrow}=(d\mathrel{@}e^{\prime})_{\downarrow}$, and we conclude because $(c\mathrel{@}e)_{\downarrow}=(c\mathrel{@}e^{\prime})_{\downarrow}\{x{\shortleftarrow}b_{\downarrow}\}$ and $(d\mathrel{@}e)_{\downarrow}=(d\mathrel{@}e^{\prime})_{\downarrow}\{x{\shortleftarrow}b_{\downarrow}\}$. ∎

Proposition C.8.

Let $e$ be a crumbled environment. Then:

1. (1)

$(x\,v,e)_{\downarrow}=(x,e)_{\downarrow}(v,e)_{\downarrow}$* for every variable $x$ and crumbled value $v$.* 2. (2)

$(\mathsf{if}\,x\,\mathsf{then}\,c\,\mathsf{else}\,d,e)_{\downarrow}=\mathsf{if}\,(x,e)_{\downarrow}\,\mathsf{then}\,(c\mathrel{@}e)_{\downarrow}\,\mathsf{else}\,(d\mathrel{@}e)_{\downarrow}$* for every variable $x$ and crumbles $c,d$.*

Proof.

By induction on $e$:

• •

Case $e=\epsilon$:

1. (1)

$(x\,v,\epsilon)_{\downarrow}=(x\,v)_{\downarrow}=x_{\downarrow}\,v_{\downarrow}=(x,\epsilon)_{\downarrow}(v,\epsilon)_{\downarrow}$. 2. (2)

$(\mathsf{if}\,x\,\mathsf{then}\,c\,\mathsf{else}\,d,\epsilon)_{\downarrow}=(\mathsf{if}\,x\,\mathsf{then}\,c\,\mathsf{else}\,d)_{\downarrow}=(\mathsf{if}\,x_{\downarrow}\,\mathsf{then}\,c_{\downarrow}\,\mathsf{else}\,d_{\downarrow})=(\mathsf{if}\,((x,\epsilon))_{\downarrow}\,\mathsf{then}\,((c\mathrel{@}\epsilon))_{\downarrow}\,\mathsf{else}\,((d\mathrel{@}\epsilon))_{\downarrow})$.

• •

Case $e=e^{\prime}[y{\shortleftarrow}b]$ for some $e^{\prime},y,b$:

1. (1)

By the definition of $(\cdot)_{\downarrow}$, $(x\,v,e^{\prime}[y{\shortleftarrow}b])_{\downarrow}=(x\,v,e^{\prime})_{\downarrow}\{y{\shortleftarrow}b_{\downarrow}\}$. By i.h. $(x\,v,e^{\prime})_{\downarrow}\{y{\shortleftarrow}b_{\downarrow}\}=((x,e^{\prime})_{\downarrow}(v,e^{\prime})_{\downarrow})\{y{\shortleftarrow}b_{\downarrow}\}$. By the definition of substitution, $((x,e^{\prime})_{\downarrow}(v,e^{\prime})_{\downarrow})\{y{\shortleftarrow}b_{\downarrow}\}=((x,e^{\prime})_{\downarrow}\{y{\shortleftarrow}b_{\downarrow}\})((v,e^{\prime})_{\downarrow}\{y{\shortleftarrow}b_{\downarrow}\})$. Again by the definition of $(\cdot)_{\downarrow}$, $((x,e^{\prime})_{\downarrow}\{y{\shortleftarrow}b_{\downarrow}\})((v,e^{\prime})_{\downarrow}\{y{\shortleftarrow}b_{\downarrow}\})=(x,e)_{\downarrow}(v,e)_{\downarrow}$ and we conclude. 2. (2)

By the definition of $(\cdot)_{\downarrow}$, $(\mathsf{if}\,x\,\mathsf{then}\,c\,\mathsf{else}\,d,e^{\prime}[y{\shortleftarrow}b])_{\downarrow}=(\mathsf{if}\,x\,\mathsf{then}\,c\,\mathsf{else}\,d,e^{\prime})_{\downarrow}\{y{\shortleftarrow}b_{\downarrow}\}$. By i.h. $(\mathsf{if}\,x\,\mathsf{then}\,c\,\mathsf{else}\,d,e^{\prime})_{\downarrow}\{y{\shortleftarrow}b_{\downarrow}\}=(\mathsf{if}\,(x,e^{\prime})_{\downarrow}\,\mathsf{then}\,(c\mathrel{@}e^{\prime})_{\downarrow}\,\mathsf{else}\,(d\mathrel{@}e^{\prime})_{\downarrow})\{y{\shortleftarrow}b_{\downarrow}\}$. By the definition of substitution, $(\mathsf{if}\,(x,e^{\prime})_{\downarrow}\,\mathsf{then}\,(c\mathrel{@}e^{\prime})_{\downarrow}\,\mathsf{else}\,(d\mathrel{@}e^{\prime})_{\downarrow})\{y{\shortleftarrow}b_{\downarrow}\}=(\mathsf{if}\,(x,e^{\prime})_{\downarrow}\{y{\shortleftarrow}b_{\downarrow}\}\,\mathsf{then}\,(c\mathrel{@}e^{\prime})_{\downarrow}\{y{\shortleftarrow}b_{\downarrow}\}\,\mathsf{else}\,(d\mathrel{@}e^{\prime})_{\downarrow}\{y{\shortleftarrow}b_{\downarrow}\})$. Again by the definition of $(\cdot)_{\downarrow}$, $(\mathsf{if}\,(x,e^{\prime})_{\downarrow}\{y{\shortleftarrow}b_{\downarrow}\}\,\mathsf{then}\,(c\mathrel{@}e^{\prime})_{\downarrow}\{y{\shortleftarrow}b_{\downarrow}\}\,\mathsf{else}\,(d\mathrel{@}e^{\prime})_{\downarrow}\{y{\shortleftarrow}b_{\downarrow}\})=\mathsf{if}\,(x,e)_{\downarrow}\,\mathsf{then}\,(c\mathrel{@}e)_{\downarrow}\,\mathsf{else}\,(d\mathrel{@}e)_{\downarrow}$ and we conclude. ∎

Lemma C.9.

Let $e$ be an environment such that $x\not\in\mathsf{dom}(e)$. Then $(x,e[x{\shortleftarrow}b]e^{\prime})_{\downarrow}=(b,e^{\prime})_{\downarrow}$ for every $b,e^{\prime}$.

Proof.

By Lemma C.5, $(x,e)_{\downarrow}=(x,\epsilon)_{\downarrow}$ because $x\notin\mathsf{dom}(e)$. By Lemma C.7, $(x,e[x{\shortleftarrow}b])_{\downarrow}=(x,[x{\shortleftarrow}b])_{\downarrow}=x\{x{\shortleftarrow}b_{\downarrow}\}=b_{\downarrow}=(b,\epsilon)_{\downarrow}$. Again by Lemma C.7, $(x,e[x{\shortleftarrow}b]e^{\prime})_{\downarrow}=(b,e^{\prime})_{\downarrow}$. ∎

Lemma C.10.

For all crumble context $C$, crumble $c$, and environment $e$, one has $C\langle c\rangle\mathrel{@}e=C\langle c\mathrel{@}e\rangle$.

Proof.

By cases according to the definition of the crumble context $C$.

If $C\coloneqq\langle\cdot\rangle$, then $C\langle c\rangle\mathrel{@}e=c\mathrel{@}e=C\langle c\mathrel{@}e\rangle$.

Otherwise $C\coloneqq(b,e^{\prime}[x{\shortleftarrow}\langle\cdot\rangle])$; let $c\coloneqq(b^{\prime},e^{\prime\prime})$; then, $c\mathrel{@}e=(b^{\prime},e^{\prime\prime}e)$ and hence $C\langle c\rangle\mathrel{@}e=(b,e^{\prime}[x{\shortleftarrow}b^{\prime}]e^{\prime\prime})\mathrel{@}e=(b,e^{\prime}[x{\shortleftarrow}b^{\prime}]e^{\prime\prime}e)=(b,e^{\prime}[x{\shortleftarrow}b^{\prime}])\mathrel{@}e^{\prime\prime}e=C\langle c\mathrel{@}e\rangle$. ∎

Corollary C.11 (Read back vs. crumble contexts).

Let $c$ be a crumble and $C,C^{\prime}$ be crumble contexts.

1. (1)

Plugging:* If $C\mathrel{\#}c$ and $C_{\downarrow}$ is a $\lambda$-context and $C\langle c\rangle$ is well-named, then $C\langle c\rangle_{\downarrow}=C_{\downarrow}\langle c_{\downarrow}\rangle$.* 2. (2)

Composition:* If $C\mathrel{\#}C^{\prime}$ and $C\langle C^{\prime}\rangle$ is well-named, where $C_{\downarrow}$ and $C^{\prime}_{\downarrow}$ are contexts, then $C\langle C^{\prime}\rangle_{\downarrow}=C_{\downarrow}\langle C^{\prime}_{\downarrow}\rangle$, which is a context.*

Proof.

1. (1)

If $C\coloneqq\langle\cdot\rangle$, then $C_{\downarrow}=\langle\cdot\rangle$ and so $C\langle c\rangle_{\downarrow}=c_{\downarrow}=C_{\downarrow}\langle c_{\downarrow}\rangle$. Otherwise $C\coloneqq(b,e[x{\shortleftarrow}\langle\cdot\rangle])$ with $c=(b^{\prime},e^{\prime})$; since $C\langle c\rangle=(b,e[x{\shortleftarrow}b^{\prime}]e^{\prime})$ is well-named, then $x\notin\mathsf{dom}(e^{\prime})$; therefore, from $C\mathrel{\#}c$ it follows that $(b,e)\mathrel{\#}e^{\prime}$; we have $C\langle c\rangle_{\downarrow}=(b,e)_{\downarrow}\{x{\shortleftarrow}(b^{\prime},e^{\prime})_{\downarrow}\}\allowbreak=C_{\downarrow}\langle c_{\downarrow}\rangle$ by Lemma C.6 and because by hypothesis $C$ unfolds to a context. 2. (2)

The composition of two contexts is a context, thus $C_{\downarrow}\langle C^{\prime}_{\downarrow}\rangle$ is a context since $C_{\downarrow}$ and $C^{\prime}_{\downarrow}$ are so.

If $C\coloneqq\langle\cdot\rangle$, then $C_{\downarrow}=\langle\cdot\rangle$ and $C\langle C^{\prime}\rangle=C^{\prime}$, thus $C\langle C^{\prime}\rangle_{\downarrow}=C^{\prime}_{\downarrow}=C_{\downarrow}\langle C^{\prime}_{\downarrow}\rangle$.

If $C^{\prime}\coloneqq\langle\cdot\rangle$, then $C^{\prime}_{\downarrow}=\langle\cdot\rangle$ and $C\langle C^{\prime}\rangle=C$, so $C\langle C^{\prime}\rangle_{\downarrow}=C_{\downarrow}=C_{\downarrow}\langle C^{\prime}_{\downarrow}\rangle$.

Finally, if $C\coloneqq(b,e[x{\shortleftarrow}\langle\cdot\rangle])$ and $C^{\prime}=(b^{\prime},e^{\prime}[y{\shortleftarrow}\langle\cdot\rangle])$, then $C\langle C^{\prime}\rangle=(b,e[x{\shortleftarrow}b^{\prime}]e^{\prime}[y{\shortleftarrow}\langle\cdot\rangle])$ and so

[TABLE]

where Lemma C.6 can be applied because $(b,e)\mathrel{\#}e^{\prime}$, since $C\mathrel{\#}C^{\prime}$ and $x\notin\mathsf{dom}(e^{\prime})$ (as $C\langle C^{\prime}\rangle$ is well-named); and $y\notin{\sf fv}((b,e)_{\downarrow})$ because $C\mathrel{\#}C^{\prime}$. ∎

Lemma C.12.

Let $c=C\langle(b,e)\rangle$ be a crumble. Then ${\sf fv}(b),{\sf fv}(C)\subseteq\mathsf{dom}(e)\cup{\sf fv}(c)$.

Proof.

By cases according to the definition of the crumble context $C$.

If $C\coloneqq\langle\cdot\rangle$ then ${\sf fv}(C)=\emptyset\subseteq\mathsf{dom}(e)\cup{\sf fv}(c)$ and $c=(b,e)$, so ${\sf fv}(c)=({\sf fv}(b)\smallsetminus\mathsf{dom}(e))\cup{\sf fv}(e)$ and hence ${\sf fv}(b)\subseteq({\sf fv}(c)\smallsetminus{\sf fv}(e))\cup\mathsf{dom}(e)\subseteq{\sf fv}(c)\cup\mathsf{dom}(e)$.

Otherwise $C\coloneqq(b,e^{\prime}[x{\shortleftarrow}\langle\cdot\rangle])$ and then ${\sf fv}(C)={\sf fv}(b^{\prime})\cup(\mathsf{dom}(e^{\prime})\smallsetminus\{x\})$ and $c=(u,e^{\prime}[x{\shortleftarrow}b]e)$; therefore, ${\sf fv}(c)={\sf fv}(C)\cup({\sf fv}(b)\smallsetminus\mathsf{dom}(e))\cup{\sf fv}(e)$ and hence ${\sf fv}(C)\subseteq\mathsf{dom}(e)\cup{\sf fv}(c)$ and ${\sf fv}(b)\subseteq\mathsf{dom}(e)\cup{\sf fv}(c)$. ∎

Remark C.1.

For every crumble $c$, one has $c\mathrel{@}[x{\shortleftarrow}\langle\cdot\rangle]_{\downarrow}=c_{\downarrow}\{x{\shortleftarrow}\langle\cdot\rangle\}$. Indeed, let $c\coloneqq(b,e)$: then, $(b,e)\mathrel{@}[x{\shortleftarrow}\langle\cdot\rangle]_{\downarrow}=(b,e[x{\shortleftarrow}\langle\cdot\rangle])_{\downarrow}=(b,e)_{\downarrow}\{x{\shortleftarrow}\langle\cdot\rangle\}$.

Proof of 0 (Lemma 4.5).

“??”

Proof.

1. (1)

It follows immediately from the freshness condition in the definition of translation. 2. (2)

By Remark 4.1. 3. (3)

It follows immediately from the freshness condition in the definition of translation. 4. (4)

By induction on $t$ and by cases on the rules defining the translation. 5. (5)

By induction on the size of $t$. Cases:

• •

$\lambda$-Value, i.e. $t=v$. Then $\underline{t}=(\overline{v},\epsilon)$ and so the only possible crumble context $C$ such that $\underline{t}=C\langle c\rangle$ for some crumble $c$ is $C=\langle\cdot\rangle$ and so $C_{\downarrow}=\langle\cdot\rangle$, which is a right v-context.

• •

$\lambda$-Value applied to value, i.e. $t=vv^{\prime}$. As in the previous case.

• •

Application applied to a value, i.e. $t=uv$ with $u$ not a $\lambda$-value. Then, $\underline{t}=(x\overline{v},[x{\shortleftarrow}s]e)$ with $\underline{u}=(s,e)$ and $x$ fresh. Cases for $C$:

• –

Empty, i.e. $C=\langle\cdot\rangle$: as for values (see above).

• –

Non-empty, i.e. $C=(x\overline{v},[x{\shortleftarrow}\langle\cdot\rangle])\langle C^{\prime}\rangle$ where $C^{\prime}$ is a crumble context of $\underline{u}$, i.e. $\underline{u}=C^{\prime}\langle c\rangle$. The read-back of the crumble context $C^{\prime\prime}\coloneqq(x\overline{v},[x{\shortleftarrow}\langle\cdot\rangle])$ is $C^{\prime\prime}_{\downarrow}=x\overline{v}_{\downarrow}\{x{\shortleftarrow}\langle\cdot\rangle\}=\langle\cdot\rangle\overline{v}_{\downarrow}$, which is a right v-context because $\overline{v}_{\downarrow}$ is a $\lambda$-value by Remark 4.1val-to-val. By i.h., $C^{\prime}_{\downarrow}$ is a right v-context. By the freshness conditions in the definition of translation, $C^{\prime\prime}\mathrel{\#}C^{\prime}$; according to Corollary C.11.2, $C_{\downarrow}=C^{\prime\prime}\langle C^{\prime}\rangle_{\downarrow}=C^{\prime\prime}_{\downarrow}\langle C^{\prime}_{\downarrow}\rangle$, which is a right v-context since the composition of right v-context is a right v-context (Lemma B.1).

• •

$\lambda$-Term applied to application, i.e. $t=us$ with $s$ not a $\lambda$-value. Then, $\underline{t}=\underline{ux}\mathrel{@}[x{\shortleftarrow}b]e$ where $\underline{s}=(b,e)$ and $x$ is fresh. Cases for $C$:

• –

$C$ is a crumble context of $\underline{ux}$, i.e. $\underline{ux}=C\langle c\rangle$, then $C_{\downarrow}$ is a right v-context by i.h. (the size of the term $ux$ is strictly less than the size of $us$ because $s$ is not a value).

• –

$C=C^{\prime\prime}\langle C^{\prime}\rangle$ where $C^{\prime\prime}\coloneqq\underline{ux}\mathrel{@}[x{\shortleftarrow}\langle\cdot\rangle]$ and $C^{\prime}$ is a crumble context of $s$ i.e. $\underline{s}=C^{\prime}\langle c\rangle$. By the freshness condition in the definition of translation and according to Remark C.1, $C^{\prime\prime}_{\downarrow}=\underline{ux}_{\downarrow}\{x{\shortleftarrow}\langle\cdot\rangle\}=\underline{u}_{\downarrow}\langle\cdot\rangle$, which is a right v-context. By i.h., $C^{\prime}_{\downarrow}$ is a right v-context. According to Corollary C.11.2, $C_{\downarrow}=C^{\prime\prime}\langle C^{\prime}\rangle_{\downarrow}=C^{\prime\prime}_{\downarrow}\langle C^{\prime}_{\downarrow}\rangle$, which is a right v-context since the composition of right v-contexts is a right v-context (Lemma B.1).

• •

Conditional, case $t\coloneqq(\mathsf{if}\,v\,\mathsf{then}\,u\,\mathsf{else}\,s)$. Then $\underline{t}=(\mathsf{if}\,\overline{v}\,\mathsf{then}\,\underline{u}\,\mathsf{else}\,\underline{s},\epsilon)$. Necessarily $C=\langle\cdot\rangle$, and hence $C_{\downarrow}$ is a right v-context.

• •

Conditional, case $t\coloneqq(\mathsf{if}\,u\,\mathsf{then}\,s\,\mathsf{else}\,r)$ with $u$ not a value. Then $\underline{t}=(\mathsf{if}\,x\,\mathsf{then}\,\underline{s}\,\mathsf{else}\,\underline{r},[x{\shortleftarrow}q]e)$ where $\underline{u}\eqqcolon(q,e)$. We proceed by cases on $C$:

• –

Case $C=\langle\cdot\rangle$. Then clearly $C_{\downarrow}$ is a right v-context.

• –

Case $C=C^{\prime\prime}\langle C^{\prime}\rangle$, where $C^{\prime\prime}\coloneqq(\mathsf{if}\,x\,\mathsf{then}\,\underline{s}\,\mathsf{else}\,\underline{r},[x{\shortleftarrow}\langle\cdot\rangle])$ and $C^{\prime}$ is a crumble context of $\underline{u}$. By the freshness condition in the definition of translation and according to Remark C.1, $C^{\prime\prime}_{\downarrow}=(\mathsf{if}\,\langle\cdot\rangle\,\mathsf{then}\,s\,\mathsf{else}\,r)$, which is a right v-context. By i.h., $C^{\prime}_{\downarrow}$ is a right v-context. According to Corollary C.11.2, $C_{\downarrow}=C^{\prime\prime}\langle C^{\prime}\rangle_{\downarrow}=C^{\prime\prime}_{\downarrow}\langle C^{\prime}_{\downarrow}\rangle=(\mathsf{if}\,C^{\prime}_{\downarrow}\,\mathsf{then}\,s\,\mathsf{else}\,r)$, which is a right v-context. ∎

Appendix D Proofs of Sect. 5 (closed case)

D.1. Proofs of Subsect. 5.1

Lemma D.1 (Closure under substitution).

Let $v$ and $v^{\prime}$ be values. Then $v\{x{\shortleftarrow}v^{\prime}\}$ is a value. If moreover $v$ is a $\lambda$-abstraction, then $v\{x{\shortleftarrow}v^{\prime}\}$ is so.

Proof.

By cases on the definition of value:

• •

Variable, i.e. either $v\coloneqq x$ and then $v\{x{\shortleftarrow}v^{\prime}\}=v^{\prime}$ which is a value by hypothesis; or $v\coloneqq y\neq x$ and then $v\{x{\shortleftarrow}v^{\prime}\}=y$ which is a value.

• •

Abstraction, i.e. $v\coloneqq\lambda y.{u}$ and we can suppose without loss of generality that $y\notin{\sf fv}(v)\cup\{x\}$; therefore, $v\{x{\shortleftarrow}v^{\prime}\}=\lambda y.{(u\{x{\shortleftarrow}v^{\prime}\})}$ which is a $\lambda$-abstraction and hence a value.

• •

Booleans and errors, i.e. $v\in\{\mathsf{true},\mathsf{false},\mathsf{err}\}$. Trivial since $v\{x{\shortleftarrow}v^{\prime}\}=v$. ∎

Lemma D.2 (Read-back to value).

For every crumbled value $v$ and $v$-environment $e_{v}$, one has that $(v,e_{v})_{\downarrow}$ is a value. If moreover $v$ is an abstraction, then $(v,e_{v})_{\downarrow}$ is a $\lambda$-abstraction.

Proof.

By induction on the length of $e_{v}$. We proceed by cases on the shape of $v$.

• •

Abstraction: If $e_{v}\coloneqq\epsilon$, then clearly $(v,e_{v})_{\downarrow}=v_{\downarrow}$ is a $\lambda$-abstraction and hence a value. Otherwise $e_{v}\coloneqq e^{\prime}_{v}[x{\shortleftarrow}b]$ where $b$ is a crumbled value (and hence $b_{\downarrow}$ is a value): thus, $(v,e_{v})_{\downarrow}=(v,e^{\prime}_{v})_{\downarrow}\{x{\shortleftarrow}b_{\downarrow}\}$; by i.h., $(v,e^{\prime}_{v})_{\downarrow}$ is a $\lambda$-abstraction, thus $(v,e_{v})_{\downarrow}$ is a $\lambda$-abstraction (and so a value) by Lemma D.1.

• •

Booleans and errors: the proof is identical to the previous case.

• •

Variable: If $v\coloneqq x\notin\mathsf{dom}(e_{v})$, then $(v,e_{v})_{\downarrow}=x$ which is a value; otherwise $v\coloneqq x\in\mathsf{dom}(e_{v})$ with $e_{v}\coloneqq e^{\prime}_{v}[x{\shortleftarrow}\lambda y.c]e^{\prime\prime}_{v}$, and then $(x,e_{v})_{\downarrow}=(\lambda y.c,e^{\prime\prime}_{v})_{\downarrow}$ (since $x\notin\mathsf{dom}(e^{\prime}_{v})$) is a value by i.h., according to the previous point. ∎

Lemma D.3.

Let $c=(b,e_{v})$ be a well-named closed crumble, and $b$ have the following property: $b$ is a value, or $b$ is $x$ or $xv$ or $\mathsf{if}\,x\,\mathsf{then}\,c\,\mathsf{else}\,d$ but $x$ is not defined in $e_{v}$. Then $c$ is a $v$-crumble.

Proof.

Let $c=(b,e_{v})$ as above: it suffices to prove that $b$ is a value. This follows easily from the hypothesis that $c$ is closed, since the cases where $b$ is $x$ or $xv$ or $\mathsf{if}\,x\,\mathsf{then}\,c\,\mathsf{else}\,d$ but $x$ is not defined in $e_{v}$ are impossible. ∎

Corollary D.4.

If the well-named closed crumble $(b,e_{v})$ is normal, then it is a $v$-crumble.

Proof of 0 (Prop. 5.3).

“??”

Proof.

• $(\Rightarrow)$

Let $c=(b,e)$ be well-named, closed, and normal. We proceed by structural induction on $e$:

• –

if $e=\epsilon$, then $(b,\epsilon)$ is a $v$-crumble by Cor. D.4;

• –

if $e=[x{\shortleftarrow}b^{\prime}]e^{\prime}$, then also the crumble $(b^{\prime},e^{\prime})$ is normal. By i.h. $(b^{\prime},e^{\prime})$ is a $v$-crumble, and therefore $e=[x{\shortleftarrow}b^{\prime}]e^{\prime}$ is a $v$-environment. By Cor. D.4, $c=b,e$ is a $v$-crumble.

• $(\Leftarrow)$

Let $c=c_{v}$, we need to prove that $c_{v}$ is normal. Let $c_{v}=C\langle(v_{\neg x},e_{v})\rangle$ for some $C,v_{\neg x},e_{v}$. Clearly no reduction rule is applicable, because $v_{\neg x}$ is not a variable or an application. ∎

D.2. Proofs of Subsect. 5.2

Proof of 0 (Lemma 5.5).

“??”

Proof.

By induction on the length of the reduction sequence leading to the crumble. The base cases hold by Lemma 4.5 (by noting that for Point 4, Lemma 4.5.5 implies the weaker statement Lemma 5.5.4). As for the inductive cases, we inspect each transition:

• 1.

The substitution transitions $\mathsf{sub}_{\mathit{var}},\mathsf{sub}_{l},\mathsf{sub}_{\mathsf{if}}$ do not change the set of variables occurring on the lhs of substitutions outside abstractions because they copy a value that does not contain any. Hence the claim follows from the i.h.. For transition ${\beta_{v}}$ the claim follows from the side condition. For the remaining rules $\textsf{ift},\textsf{iff},\textsf{ife},\textsf{@e}$ the claim follows from the fact that all substitutions outside abstractions in the rhs alredy occur in the lhs.

• 2.

The substitution transitions $\mathsf{sub}_{\mathit{var}},\mathsf{sub}_{l},\mathsf{sub}_{\mathsf{if}}$ do not change the domain of the crumble and only copy to the left a value from the environment, and the claim follows from the i.h..

Transition ${\beta_{v}}$ copies to the top level and renames the body of an abstraction. By the properties of $\alpha$-renaming ${\sf fv}((c\mathrel{@}[x{\shortleftarrow}v])^{\alpha})={\sf fv}(c\mathrel{@}[x{\shortleftarrow}v])={\sf fv}(\lambda x.c)$, and since by i.h. ${\sf fv}(\lambda x.c)\subseteq\mathsf{dom}(e_{v})$, we can conclude with ${\sf fv}((c\mathrel{@}[x{\shortleftarrow}v])^{\alpha})\subseteq\mathsf{dom}(e_{v})$.

The terms in the rhs of the remaining transitions $\textsf{ift},\textsf{iff},\textsf{ife},\textsf{@e}$ already occur in the lhs under the same environment. Therefore the claim follows from the i.h..

• 3.

The rules $\mathsf{sub}_{\mathit{var}},\mathsf{sub}_{l},\mathsf{sub}_{\mathsf{if}}$ may copy an abstraction, but the abstraction was already in the environment, and the claim follows from the i.h.. The rule ${\beta_{v}}$ copies and renames the body of an abstraction that was already in the environment, and the claim follows from the i.h. since the translation commutes with the renaming of free variables (Remark 4.1.3). All the bodies in the rhs of the remaning rules $\textsf{ift},\textsf{iff},\textsf{ife},\textsf{@e}$ already occur in the lhs and therefore the claim follows from the i.h..

• 4.

Let $\underline{b^{\prime\prime}}\rightarrow^{n}C^{\prime}\langle(b^{\prime},e^{\prime}_{v})\rangle\rightarrow_{a}C\langle(b,e_{v})\rangle$ (where $b$ is not a practical value). Cases of the reduction step $C^{\prime}\langle(b^{\prime},e^{\prime}_{v})\rangle\rightarrow_{a}C\langle(b,e_{v})\rangle$:

• –

Case ${\beta_{v}}$: $C^{\prime}\langle((\lambda x.c)v,e_{v})\rangle\rightarrow_{{\beta_{v}}}C^{\prime}\langle c^{\alpha}\mathrel{@}([x^{\alpha}{\shortleftarrow}v]e_{v})\rangle$.

Let $C^{\prime\prime}$ be a prefix of $C$. There are two sub-cases:

$C^{\prime\prime}$ is a prefix of $C^{\prime}$: by i.h. $C^{\prime\prime}_{\downarrow}$ is a right v-context.

• *

$C^{\prime}$ is a prefix of $C^{\prime\prime}$, i.e. $C^{\prime\prime}=C^{\prime}\langle C^{\prime\prime\prime}\rangle$ and $c^{\alpha}=C^{\prime\prime\prime}\langle c^{\prime}\rangle$. By Lemma 4.5.4 and Lemma 5.5.3 $c$ is the translation of a $\lambda$-term, by Remark 4.1.3 $c^{\alpha}$ is so, and thus by Lemma 4.5.5 $C^{\prime\prime\prime}_{\downarrow}$ is a right v-context. By i.h., $C^{\prime}_{\downarrow}$ is a right v-context as well. Since $C^{\prime\prime}_{\downarrow}=C^{\prime}_{\downarrow}\langle C^{\prime\prime\prime}_{\downarrow}\rangle$ according to Corollary C.11.2, we obtain that $C^{\prime\prime}_{\downarrow}$ is a right v-context as composition of right v-contexts (Lemma B.1).

• –

Case ift: $C^{\prime}\langle(\mathsf{if}\,\mathsf{true}\,\mathsf{then}\,c\,\mathsf{else}\,d,e_{v})\rangle\rightarrow_{{\beta_{v}}}C^{\prime}\langle c\mathrel{@}e_{v}\rangle$. Let $C^{\prime\prime}$ be a prefix of $C$. There are two sub-cases:

$C^{\prime\prime}$ is a prefix of $C^{\prime}$: by i.h. $C^{\prime\prime}_{\downarrow}$ is a right v-context.

• *

$C^{\prime}$ is a prefix of $C^{\prime\prime}$, i.e. $C^{\prime\prime}=C^{\prime}\langle C^{\prime\prime\prime}\rangle$ and $c=C^{\prime\prime\prime}\langle c^{\prime}\rangle$. By Lemma 4.5.4 and Lemma 5.5.3 $c$ is the translation of a $\lambda$-term and thus by Lemma 4.5.5 $C^{\prime\prime\prime}_{\downarrow}$ is a right v-context. By i.h., $C^{\prime}_{\downarrow}$ is a right v-context as well. Since $C^{\prime\prime}_{\downarrow}=C^{\prime}_{\downarrow}\langle C^{\prime\prime\prime}_{\downarrow}\rangle$ according to Corollary C.11.2, we obtain that $C^{\prime\prime}_{\downarrow}$ is a right v-context as composition of right v-contexts (Lemma B.1).

• –

Case iff: identical to the previous case.

• –

Cases $\mathsf{sub}_{\mathit{var}},\textsf{ife},\textsf{@e}$: they follow from the i.h. since $C$ is necessarily a prefix of $C^{\prime}$ because $b$ is a practical value.

• –

Cases $\mathsf{sub}_{l}$ and $\mathsf{sub}_{\mathsf{if}}$: they follow from the i.h., since $e^{\prime}_{v}=e_{v}$ and $C=C^{\prime}$. ∎

Lemma D.5 (Determinism).

$\rightarrow_{\mathsf{Cr}}$* is deterministic.*

Proof.

Assume that there exists a crumble that may be decomposed in two ways $C\langle(b,e_{v})\rangle=C^{\prime}\langle b^{\prime},e^{\prime}_{v}\rangle$ such that they reduce respectively $C\langle(b,e_{v})\rangle\rightarrow_{a}C\langle c\rangle$ and $C^{\prime}\langle(b^{\prime},e^{\prime}_{v})\rangle\rightarrow_{b}C^{\prime}\langle d\rangle$ with rules $a,b\in\{{\beta_{v}},\textsf{ift},\textsf{iff},\textsf{ife},\textsf{@e},\mathsf{sub}_{\mathit{var}},\mathsf{sub}_{l},\mathsf{sub}_{\mathsf{if}}\}$.

We prove that it must necessarily be $a=b$, $C=C^{\prime}$, and $c=d$ (up to alpha). Three cases:

• •

$C$ strict initial segment of $C^{\prime}$, i.e. $C^{\prime}=C\langle C^{\prime\prime}\rangle$ for some $C^{\prime\prime}\neq\langle\cdot\rangle$. We show that this case is not possible: in fact, it follows that $e_{v}=E\langle(b^{\prime},e^{\prime}_{v})\rangle$ for some $E$, thus $(b^{\prime},e^{\prime}_{v})$ is a $v$-crumble, and by Prop. 5.3 it must be normal, contradicting the hypothesis that $(b^{\prime},e^{\prime}_{v})$ and $c$ reduce with rule $b$.

• •

$C=C^{\prime}$. By inspection of the reduction rules, $a=b$: in fact the rule ${\beta_{v}}$ applies only when $b$ is the application of an abstraction to a crumbled value, the rule $\mathsf{sub}_{\mathit{var}}$ only when $b$ is a variable, and the rule $\mathsf{sub}_{l}$ only when $b$ is the application of a variable to a crumbled value, etc. It remains to show that $c=d$ (up to alpha): this follows from the determinism of the lookup in the environment during $\mathsf{sub}_{\mathit{var}},\mathsf{sub}_{l}$ and $\mathsf{sub}_{\mathsf{if}}$ reductions.

• •

$C^{\prime}$ initial segment of $C$, i.e. $C=C^{\prime}\langle C^{\prime\prime}\rangle$. Symmetric to the first case. ∎

Lemma D.6.

In every reachable crumble $C\langle(b,e)\rangle$ one has ${\sf fv}(b)\cap\mathsf{dom}(C)=\emptyset$.

Proof.

By Lemma C.12 and Lemmas 5.5.1-2. ∎

Proposition D.7 (Overhead transparency).

Let $c$ be a reachable crumble, and let $a\in\{\mathsf{sub}_{\mathit{var}},\mathsf{sub}_{l},\mathsf{sub}_{\mathsf{if}}\}$. If $c\rightarrow_{a}d$ then $c_{\downarrow}=d_{\downarrow}$.

Proof.

Let $c\coloneqq C\langle(b,e_{v})\rangle\rightarrow_{a}C\langle(b^{\prime},e_{v})\rangle\eqqcolon d$, and let $e^{\prime}_{v},e^{\prime\prime}_{v}$ such that $e_{v}=e^{\prime}_{v}[x{\shortleftarrow}e_{v}(x)]e^{\prime\prime}_{v}$, noting that $x$ does not occur in $e^{\prime\prime}_{v}$ by Lemma 5.5.1 and Lemma D.6. We first prove that $(b,e_{v})_{\downarrow}=(b^{\prime},e_{v})_{\downarrow}$:

• •

Case $\mathsf{sub}_{\mathit{var}}$, i.e. $b\coloneqq x$ and $b^{\prime}=e_{v}(x)$. By Lemma C.4, $(x,e^{\prime}_{v}[x{\shortleftarrow}e_{v}(x)]e^{\prime\prime}_{v})_{\downarrow}=(x,e^{\prime}_{v}e^{\prime\prime}_{v})_{\downarrow}\{x{\shortleftarrow}(e_{v}(x),e^{\prime\prime}_{v})_{\downarrow}\}=(e_{v}(x),e^{\prime\prime}_{v})_{\downarrow}$ as $c$ is well-named (Lemma 5.5.1). By Lemma D.6, ${\sf fv}(e_{v}(x))\cap\mathsf{dom}(e^{\prime}_{v}[x{\shortleftarrow}e_{v}(x)])=\emptyset$, therefore $(e_{v}(x),e^{\prime\prime}_{v})_{\downarrow}=(e_{v}(x),e_{v})_{\downarrow}$, and we conclude with $(x,e_{v})_{\downarrow}=(e_{v}(x),e_{v})_{\downarrow}$.

• •

Case $\mathsf{sub}_{l}$, i.e. $b\coloneqq x\,v$ and $b^{\prime}=e_{v}(x)\,v$. Since $(x\,v,e_{v})_{\downarrow}=(x,e_{v})_{\downarrow}(v,e_{v})_{\downarrow}$ (Prop. C.8), we can use the point above to conclude.

• •

Case $\mathsf{sub}_{\mathsf{if}}$, i.e. $b\coloneqq\mathsf{if}\,x\,\mathsf{then}\,c\,\mathsf{else}\,d$ and $b^{\prime}=\mathsf{if}\,e_{v}(x)\,\mathsf{then}\,c\,\mathsf{else}\,d$. Since $(\mathsf{if}\,x\,\mathsf{then}\,c\,\mathsf{else}\,d,e_{v})_{\downarrow}=\mathsf{if}\,(x,e_{v})_{\downarrow}\,\mathsf{then}\,(c\mathrel{@}e_{v})_{\downarrow}\,\mathsf{else}\,(d\mathrel{@}e_{v})_{\downarrow}$ (Prop. C.8), we can use the point above to conclude.

We now prove that $C\langle(b,e_{v})\rangle_{\downarrow}=C\langle(b^{\prime},e_{v})\rangle_{\downarrow}$ under the hypothesis that $(b,e_{v})_{\downarrow}=(b^{\prime},e_{v})_{\downarrow}$. By cases on $C$: if $C\coloneqq\langle\cdot\rangle$ just use the hypothesis. Otherwise $C\coloneqq(b^{\prime\prime},e[x{\shortleftarrow}\langle\cdot\rangle])$ and so $(b^{\prime\prime},e[x{\shortleftarrow}b]e_{v})_{\downarrow}=(b^{\prime\prime},ee_{v})_{\downarrow}\{x{\shortleftarrow}(b,e_{v})_{\downarrow}\}=(b^{\prime\prime},ee_{v})_{\downarrow}\{x{\shortleftarrow}(b^{\prime},e_{v})_{\downarrow}\}\allowbreak=(b^{\prime\prime},e[x{\shortleftarrow}b^{\prime}]e_{v})_{\downarrow}$ by Lemma C.4. ∎

Lemma D.8 (Substitution).

Let $t$ and $u$ be terms, and $v$ be a value. If $t\rightarrow_{\mathsf{pif}}u$ then $t\{x{\shortleftarrow}v\}\allowbreak\rightarrow_{\mathsf{pif}}u\{x{\shortleftarrow}v\}$.

Proof.

By induction on the definition of $t\rightarrow_{\mathsf{pif}}u$. Cases:

• •

Root-step.

• –

${\beta_{v}}$-step, i.e. $t\coloneqq(\lambda y.{s})v^{\prime}\mapsto_{{\beta_{v}}}s\{y{\shortleftarrow}v^{\prime}\}\eqqcolon u$ and we can suppose without loss of generality that $y\notin{\sf fv}(v)\cup\{x\}$. According to Lemma D.1, $v^{\prime}\{x{\shortleftarrow}v\}$ is a value. As a consequence, $t\{x{\shortleftarrow}v\}=\allowbreak(\lambda y.{s\{x{\shortleftarrow}v\}})(v^{\prime}\{x{\shortleftarrow}v\})\rightarrow_{{\beta_{v}}}s\{y{\shortleftarrow}v^{\prime}\{x{\shortleftarrow}v\}\}=s\{y{\shortleftarrow}v^{\prime}\}\{x{\shortleftarrow}v\}=u\{x{\shortleftarrow}v\}$.

• –

the $\textsf{ift},\textsf{iff},\textsf{ife},\textsf{@e}$ steps are similar to the ${\beta_{v}}$-step. Lemma D.1 is used in the proof of the ife-step to prove that a ife-redex where the guard is an abstraction is mapped to a ife-redex of the same kind.

• •

Application right, i.e. $t\coloneqq sr\rightarrow_{\mathsf{pif}}sq\eqqcolon u$ with $r\rightarrow_{\mathsf{pif}}q$; by i.h. $r\{x{\shortleftarrow}v\}\rightarrow_{\mathsf{pif}}q\{x{\shortleftarrow}v\}$, and therefore $t\{x{\shortleftarrow}v\}=s\{x{\shortleftarrow}v\}(r\{x{\shortleftarrow}v\})\rightarrow_{\mathsf{pif}}s\{x{\shortleftarrow}v\}(q\{x{\shortleftarrow}v\})=u\{x{\shortleftarrow}v\}$.

• •

Application left, i.e. $t\coloneqq sv^{\prime}\rightarrow_{\mathsf{pif}}rv^{\prime}\eqqcolon u$ with $s\rightarrow_{\mathsf{pif}}r$; by i.h., $s\{x{\shortleftarrow}v\}\rightarrow_{\mathsf{pif}}r\{x{\shortleftarrow}v\}$; according to Lemma D.1, $v^{\prime}\{x{\shortleftarrow}v\}$ is a value and hence $t\{x{\shortleftarrow}v\}=s\{x{\shortleftarrow}v\}(v^{\prime}\{x{\shortleftarrow}v\})\rightarrow_{\mathsf{pif}}r\{x{\shortleftarrow}v\}(v^{\prime}\{x{\shortleftarrow}v\})=u\{x{\shortleftarrow}v\}$.

• •

If-then-else guard, i.e. $t\coloneqq\mathsf{if}\,r\,\mathsf{then}\,s\,\mathsf{else}\,p\rightarrow_{\mathsf{pif}}\mathsf{if}\,q\,\mathsf{then}\,s\,\mathsf{else}\,p\eqqcolon u$ with $r\rightarrow_{\mathsf{pif}}q$; by i.h. $r\{x{\shortleftarrow}v\}\rightarrow_{\mathsf{pif}}q\{x{\shortleftarrow}v\}$, and therefore $t\{x{\shortleftarrow}v\}=\mathsf{if}\,r\{x{\shortleftarrow}v\}\,\mathsf{then}\,s\{x{\shortleftarrow}v\}\,\mathsf{else}\,p\{x{\shortleftarrow}v\}\rightarrow_{\mathsf{pif}}\mathsf{if}\,q\{x{\shortleftarrow}v\}\,\mathsf{then}\,s\{x{\shortleftarrow}v\}\,\mathsf{else}\,p\{x{\shortleftarrow}v\}=u\{x{\shortleftarrow}v\}$. ∎

Lemma D.9.

Let $c,d$ be crumbles, and let $e_{v}$ be a $v$-environment. If $c_{\downarrow}\rightarrow_{\mathsf{pif}}{}d_{\downarrow}$, then $(c\mathrel{@}e_{v})_{\downarrow}\rightarrow_{\mathsf{pif}}(d\mathrel{@}e_{v})_{\downarrow}$.

Proof.

By induction on the length of $e_{v}$. If $e_{v}\coloneqq\epsilon$ then $(c\mathrel{@}e_{v})_{\downarrow}=c_{\downarrow}\rightarrow_{\mathsf{pif}}d_{\downarrow}=(d\mathrel{@}e_{v})_{\downarrow}$. Otherwise $e_{v}\coloneqq e^{\prime}_{v}[x{\shortleftarrow}v]$ where $v$ is a practical value (and hence $v_{\downarrow}$ is a value); by i.h., $(c\mathrel{@}e^{\prime}_{v})_{\downarrow}\rightarrow_{\mathsf{pif}}(d\mathrel{@}e^{\prime}_{v})_{\downarrow}$ and hence $(c\mathrel{@}e_{v})_{\downarrow}=(c\mathrel{@}e^{\prime}_{v})_{\downarrow}\{x{\shortleftarrow}v_{\downarrow}\}\rightarrow_{\mathsf{pif}}(d\mathrel{@}e^{\prime}_{v})_{\downarrow}\{x{\shortleftarrow}v_{\downarrow}\}=(d\mathrel{@}e_{v})_{\downarrow}$ according to Lemma D.8. ∎

Proposition D.10 (Principal projection).

Let $c$ be a reachable crumble. If $c\rightarrow_{a}d$ for $a\in\{{\beta_{v}},\textsf{ift},\textsf{iff},\textsf{ife},\textsf{@e}\}$ then $c_{\downarrow}\rightarrow_{a}d_{\downarrow}$.

Proof.

Note that for every $b,e_{v}$, $(b,e_{v})=(b,\epsilon)\mathrel{@}e_{v}$. Therefore all steps can be written in the form $C\langle(b,e_{v})\rangle\rightarrow_{a}C\langle c\mathrel{@}e_{v}\rangle$ where $b$ is not a crumbled value. The crumble context $C$ unfolds to a right v-context by Lemma 5.5.4. We need to prove that $C\langle(b,e_{v})\rangle_{\downarrow}\rightarrow_{a}(C\langle c\mathrel{@}e_{v}\rangle)_{\downarrow}$. By Lemma C.10 and Lemma D.9, it suffices to prove that $C\langle(b,\epsilon)\rangle_{\downarrow}\rightarrow_{a}C\langle c\rangle_{\downarrow}$.

We proceed by cases on the rule $\rightarrow_{a}$.

• •

Rule ${\beta_{v}}$: we need to prove that $C\langle((\lambda x.c)\,v,\epsilon)\rangle_{\downarrow}\rightarrow_{{\beta_{v}}}{}C\langle e\mathrel{@}[y{\shortleftarrow}v]\rangle_{\downarrow}$ where $e\mathrel{@}[y{\shortleftarrow}v]\coloneqq(c\mathrel{@}[x{\shortleftarrow}v])^{\alpha}$.

[TABLE]

Note that the second use of Corollary C.11.1 requires that $C\mathrel{\#}(e\mathrel{@}[y{\shortleftarrow}v])$ i.e. that ${\sf fv}(C)\cap\mathsf{dom}(e\mathrel{@}[y{\shortleftarrow}v])=\emptyset$, which follows from the side condition about $\alpha$-renaming in the ${\beta_{v}}$ rule.

• •

Rules $\textsf{ift},\textsf{iff},\textsf{ife},\textsf{@e}$: a quick check by cases over $(b,e_{v})\mapsto_{a}c\mathrel{@}e_{v}$ shows that $b_{\downarrow}\rightarrow_{a}c_{\downarrow}$.

For example, $(\mathsf{if}\,\mathsf{true}\,\mathsf{then}\,c\,\mathsf{else}\,d,e_{v})\mapsto_{\textsf{ift}}c\mathrel{@}e_{v}$ and

$(\mathsf{if}\,\mathsf{true}\,\mathsf{then}\,c\,\mathsf{else}\,d)_{\downarrow}=\mathsf{if}\,\mathsf{true}\,\mathsf{then}\,c_{\downarrow}\,\mathsf{else}\,d_{\downarrow}\rightarrow_{\textsf{ift}}c_{\downarrow}$. The other cases are all similar.

Thus

[TABLE]

Note that the second use of Corollary C.11.1 requires that $C\mathrel{\#}c$. The property holds because all substitutions outside abstractions in the rhs of the rules $\rightarrow_{a}$ under consideration were such in the lhs, and because reachable crumbles are well-named (Lemma 5.5.1). ∎

Lemma D.11 (Halt).

Let $c$ be a closed crumble. If $c$ is $\mathsf{Cr}$​-normal then $c_{\downarrow}$ is $Pif$-normal.

Proof.

By Prop. 5.3, if $c$ is normal then it is a $v$-crumble i.e. $c=c_{v}$. By Lemma D.2, $c_{\downarrow}$ is a value. By Pif harmony (Prop. 2.1), $c_{\downarrow}$ is $\rightarrow_{\mathsf{pif}}$-normal. ∎

Proof of 0 (Thm. 5.6).

“??”

Proof.

1. (1)

See Prop. 4.2. 2. (2)

See Prop. D.10. 3. (3)

See Prop. D.7. 4. (4)

See Lemma D.5. 5. (5)

See Lemma D.11, since $c$ is closed by Lemma 5.5.2. 6. (6)

Immediate consequence of Lemma 5.8 (proved independently). ∎

D.3. Proofs of Subsect. 5.3

Proof of 0 (Prop. 5.7).

“??”

Proof.

By mutual induction on $t$ and $v$:

• •

Variable, i.e. $v=t\coloneqq x$ : then $\overline{v}=x$ and $\underline{t}=(x,\epsilon)$, hence $|\overline{v}|_{\textup{var}}=|\underline{t}|_{\textup{var}}=1$.

• •

Boolean or error, i.e. $v=t\in\{\mathsf{true},\mathsf{false},\mathsf{err}\}$: then $\overline{v}=v$ and $\underline{t}=(v,\epsilon)$, hence $|\overline{v}|_{\textup{var}}=|\underline{t}|_{\textup{var}}=0$.

• •

Abstraction, i.e. $v\coloneqq\lambda x.{u}\eqqcolon t$ : then $\overline{v}=\lambda x.{\underline{u}}$ and $\underline{t}=(\lambda x.{\underline{u}},\epsilon)$; by i.h., $|\underline{u}|_{\textup{var}}\leq 1$. We have $|\overline{v}|_{\textup{var}}=|\underline{t}|_{\textup{var}}=0$ by definition.

• •

Application of two $\lambda$-values, i.e. $t\coloneqq v^{\prime}v^{\prime\prime}$ : then, $\underline{t}=(\overline{v^{\prime}}\,\overline{v^{\prime\prime}},\epsilon)$. We have $|\underline{t}|_{\textup{var}}=0$ by definition.

• •

Conditional on a value, i.e. $t\coloneqq\mathsf{if}\,v^{\prime}\,\mathsf{then}\,u\,\mathsf{else}\,s$ : then, $\underline{t}=(\mathsf{if}\,\overline{v^{\prime}}\,\mathsf{then}\,\underline{u}\,\mathsf{else}\,\underline{s},\epsilon)$. We have $|\underline{t}|_{\textup{var}}=0$ by definition.

• •

Application of a non-$\lambda$-value to a $\lambda$-value, i.e. $t\coloneqq uv$ where $u$ is not a value: then, $\underline{t}=(x\overline{v},[x{\shortleftarrow}b]e)$ where $\underline{u}=(b,e)$; by i.h., $|\underline{u}|_{\textup{var}}=0$. Note that $|\underline{t}|_{\textup{var}}=|(x\overline{v},[x{\shortleftarrow}b]e)|_{\textup{var}}=|b|_{\textup{var}}+|e|_{\textup{var}}=|(b,e)|_{\textup{var}}=|\underline{u}|_{\textup{var}}=_{\textit{i.h.}}0$.

• •

Application of a term to a non-value, i.e. $t\coloneqq us$ where $s$ is not a value: then, $\underline{t}=\underline{ux}\mathrel{@}([x{\shortleftarrow}b]e)=(yx,[y{\shortleftarrow}b^{\prime}]e^{\prime}[x{\shortleftarrow}b]e)$ where $\underline{s}=(b,e)$ and $\underline{ux}=(yx,[y{\shortleftarrow}b^{\prime}]e^{\prime})$ with $\underline{u}=(b^{\prime},e^{\prime})$. By i.h., $|\underline{ux}|_{\textup{var}}=|\underline{s}|_{\textup{var}}=0$. Since $|\underline{t}|_{\textup{var}}=|\underline{u}|_{\textup{var}}+|\underline{s}|_{\textup{var}}$, we have $|\underline{t}|_{\textup{var}}=0$.

• •

Conditional on a non-value, i.e. $t\coloneqq\mathsf{if}\,u\,\mathsf{then}\,s\,\mathsf{else}\,r$ where $u$ is not a value  : then, $\underline{t}=(\mathsf{if}\,x\,\mathsf{then}\,\underline{s}\,\mathsf{else}\,\underline{r},[x{\shortleftarrow}b]e)$ with $\underline{u}=(b,e)$. By i.h., $|\underline{u}|_{\textup{var}}=0$. Then

[TABLE]

∎

We define the size $|\cdot|$ of crumbled forms, crumbles and environments as expected:

[TABLE]

[TABLE]

Proof of 0 (Lemma 5.9).

“??”

Proof.

By mutual induction on $t$ and $v$:

• •

Variable, i.e. $v\coloneqq x\eqqcolon t$ : then $\overline{v}=x$ and $\underline{t}=(x,\epsilon)$, hence $|\overline{v}|=1\leq 5|v|$ and $|\underline{t}|=|x|+|\epsilon|=1\leq 5\,|t|$.

• •

Error or Boolean: similar to the case above.

• •

Abstraction, i.e. $v\coloneqq\lambda x.{u}\eqqcolon t$ : then $\overline{v}=\lambda x.{\underline{u}}$ and $\underline{t}=(\lambda x.{\underline{u}},\epsilon)$; by i.h., $|\underline{u}|\leq 5|u|$ and hence $|\overline{v}|=|\underline{u}|+1\leq 5|u|+1\leq 5(|u|+1)=5|v|$ and $|\underline{t}|=|\lambda x.\underline{u}|+|\epsilon|=|\underline{u}|+1\leq 5|u|+1\leq 5(|u|+1)=5\,|t|$.

• •

Application of two $\lambda$-values, i.e. $t\coloneqq vv^{\prime}$ : then, $\underline{t}=(\overline{v}\,\overline{v^{\prime}},\epsilon)$; by i.h., $|\overline{v}|\leq 5|v|$ and $|\overline{v^{\prime}}|\leq 5|v^{\prime}|$; hence $|\underline{t}|=|\overline{v}\,\overline{v^{\prime}}|+|\epsilon|=|\overline{v}|+|\overline{v^{\prime}}|+1\leq 5|v|+5\cdot|v^{\prime}|+1\leq 5(|v|+|v^{\prime}|+1)=5\,|t|$.

• •

Application of a non-$\lambda$-value to a $\lambda$-value, i.e. $t\coloneqq uv$ where $u$ is not a value: then, $\underline{t}=(x\overline{v},[x{\shortleftarrow}b]e)$ where $\underline{u}=(b,e)$; by i.h., $|\overline{v}|\leq 5|v|$ and $|\underline{u}|=|b|+|e|\leq 5|u|$; hence $|\underline{t}|=|x|+|\overline{v}|+1+|b|+|e|+1=|\overline{v}|+|\underline{u}|+3\leq 5|v|+5|u|+3\leq 5(|v|+|u|+1)=5\,|t|$.

• •

Application of a term to a non-value, i.e. $t\coloneqq us$ where $s$ is not a value: then, $\underline{t}=\underline{ux}\mathrel{@}([x{\shortleftarrow}b]e)=(yx,[y{\shortleftarrow}b^{\prime}]e^{\prime}[x{\shortleftarrow}b]e)$ where $\underline{s}=(b,e)$ and $\underline{ux}=(yx,[y{\shortleftarrow}b^{\prime}]e^{\prime})$ with $\underline{u}=(b^{\prime},e^{\prime})$. By i.h., $|\underline{s}|=|b|+|e|\leq 5|s|$ and $|\underline{u}|=|b^{\prime}|+|e^{\prime}|\leq 5|u|$. Therefore, $|\underline{t}|=|yx|+|b^{\prime}|+|e^{\prime}|+1+|b|+|e|+1=|\underline{u}|+|\underline{s}|+5\leq 5|u|+5|s|+5\leq 5(|u|+|s|+1)=5|t|$.

• •

Conditional, case $t\coloneqq(\mathsf{if}\,v\,\mathsf{then}\,u\,\mathsf{else}\,s)$. Then $\underline{t}=(\mathsf{if}\,\overline{v}\,\mathsf{then}\,\underline{u}\,\mathsf{else}\,\underline{s},\epsilon)$ and $|\underline{t}|=1+|\overline{v}|+|\underline{u}|+|\underline{s}|$. Conclude by i.h.

• •

Conditional, case $t\coloneqq(\mathsf{if}\,u\,\mathsf{then}\,s\,\mathsf{else}\,r)$ with $u$ not a value. Then $\underline{t}=(\mathsf{if}\,x\,\mathsf{then}\,\underline{s}\,\mathsf{else}\,\underline{r},[x{\shortleftarrow}q]e)$ where $\underline{u}\eqqcolon(q,e)$. Then $|\underline{t}|=1+1+|\underline{s}|+|\underline{r}|+1+|\underline{u}|$. Conclude by i.h. ∎

Proof of 0 (Thm. 5.10).

“??”

Proof.

By Lemma 5.8 and the discussion in the body about costs. ∎

D.4. The Pointed Crumble GLAM

As discussed at the beginning of Sect. 5, we call the Crumble GLAM a machine even though it does not satisfy the usual requirements for abstract machines. One of these requirements is the presence of rules that guide evaluation to the next redex: in the Crumble GLAM the search for the next redex is instead left implicit in the evaluation rules, because it corresponds to going through the environment from right to left.

In order to implement the Crumble GLAM while respecting the complexity analysis that we just presented in Subsect. 5.3, we introduce a variant of the Crumble GLAM called Pointed Crumble GLAM, where the search for the next redex is decomposed into $O(1)$ steps of a new search transition. The other steps of the machine are in one-to-one correspondence with the ones of the Crumble GLAM. Finally, we prove that the overall number of the search transitions is bilinear in the number of principal transitions and the size of the initial term, establishing bilinearity of the Pointed Crumble GLAM. To improve the readability of this section, all proofs are moved to Section D.5.

Pointed crumbles and pointed environments.

The key idea to turn the Crumble GLAM into the Pointed Crumble GLAM is to avoid plugging and unplugging in the rules by letting them act on pointed crumbles, i.e. on crumbles where the beginning of the evaluated coda is explicitly marked using a pointer. For example, the crumble $(b,ee_{v})$ could be represented as $(b,e\mathrel{\!\textnormal{{¦}}\!}e_{v})$ where “$\mathrel{\!\textnormal{{¦}}\!}$” is the explicit separator that must be followed by $v$-environments only. A pointed crumble $(b,e[x{\shortleftarrow}b^{\prime}]\mathrel{\!\textnormal{{¦}}\!}e_{v})$ is the machine state that is attempting to evaluate the crumble $C\langle(b^{\prime},e_{v})\rangle$, where $C=(b,e[x{\shortleftarrow}\langle\cdot\rangle])$. If $(b^{\prime},e_{v})$ is a Crumble GLAM $a$-redex, the Pointed Crumble GLAM will evaluate according to the corresponding $a$-transition that also takes care of setting (in $O(1)$) the pointer to the rightmost unevaluated crumble. Otherwise, by harmony (Prop. 5.3), $b^{\prime}$ must be a crumbled value $v$ and therefore the pointer is moved (in $O(1)$) one step to the left, looking for the next redex: $(b,e[x{\shortleftarrow}v]\mathrel{\!\textnormal{{¦}}\!}e_{v})\rightarrow_{\mathsf{sea}}(b,e\mathrel{\!\textnormal{{¦}}\!}[x{\shortleftarrow}v]e_{v})$.

Not all pointed crumble configurations are of the form $(b,[x{\shortleftarrow}b^{\prime}]\mathrel{\!\textnormal{{¦}}\!}e_{v})$: the configurations $(b,\mathrel{\!\textnormal{{¦}}\!}e_{v})$ must be also taken into account and evaluated if $b$ is not a crumbled value. However, there is no simple way to describe machine transitions that act uniformly on configurations $(b,\mathrel{\!\textnormal{{¦}}\!}e_{v})$ and $(b,e[x{\shortleftarrow}b^{\prime}]\mathrel{\!\textnormal{{¦}}\!}e_{v})$ without duplicating the rules or without re-introducing a notion of contextual closure. To solve the issue, we abandon pointed crumbles and adopt pointed environments instead.

A pointed environment $([x{\shortleftarrow}b]e\mathrel{\!\textnormal{{¦}}\!}e_{v})$ is just a representation of a pointed crumble $(b,e\mathrel{\!\textnormal{{¦}}\!}e_{v})$. The leftmost variable $x$ in a pointed environment can be understood as the name given to the machine output. It plays a role similar to the outermost $\lambda$-abstraction introduced by CPS transformations, that binds the continuation that is fed with the output of the evaluation. In particular, a normal pointed environment $(\mathrel{\!\textnormal{{¦}}\!}[x{\shortleftarrow}v]e_{v})$ represents the normal crumble $(v,e_{v})$.

Formal definition of pointed environments and read-back.

Pointed environments are defined as $e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}\coloneqq e\mathrel{\!\textnormal{{¦}}\!}e^{\prime}$ for any non-pointed environments $e$ and $e^{\prime}$ such that either $e$ or $e^{\prime}$ is non-empty. The environment on the left of the cursor $\mathrel{\!\textnormal{{¦}}\!}$ is the unevaluated environment; the one on the right is the evaluated environment.

The translation $\iota(\cdot)$ embeds crumbles into pointed environments:

[TABLE]

where $x$ is any variable name fresh in $b$ and $e$.

The left inverse of $\iota(\cdot)$ is the read-back function $(\cdot)_{\Downarrow}$ (from pointed environments to crumbles):

[TABLE]

Evaluation.

The transition rules of the Pointed Crumble GLAM are (the adaptation of) those of the Crumble GLAM plus the new search transition $\rightarrow_{\mathsf{sea}}$, and they are all defined only at top level, without a contextual closure—their union is noted $\rightarrow_{\mathsf{pCr}}$:

[TABLE]

where

1. i.

$\lambda z.{(b,e^{\prime})}\coloneqq(\lambda y.c)^{\alpha}$ such that $(e[x{\shortleftarrow}b]e^{\prime}[z{\shortleftarrow}v]\mathrel{\!\textnormal{{¦}}\!}e_{v})$ is well-named. 2. ii.

where $c\eqqcolon(b,e^{\prime})$ 3. iii.

where $d\eqqcolon(b,e^{\prime})$ 4. iv.

if $v=\lambda x.e$ or $v=\mathsf{err}$. 5. v.

if $v\in\{\mathsf{true},\mathsf{false},\mathsf{err}\}$. 6. vi.

if $x\in\mathsf{dom}(e_{v})$. 7. vii.

if none of the other rules is applicable, i.e. when $b$ is a practical value $v_{\neg x}$ or when $b$ is $x$, $xv$, or $\mathsf{if}\,x\,\mathsf{then}\,c\,\mathsf{else}\,d$ but $x$ is not defined in $e_{v}$.

A principal transition of the Pointed Crumble GLAM is a transition $\rightarrow_{a}$ for any rule $a\in\{{\beta_{v}},\textsf{ift},\textsf{iff},\textsf{ife},\textsf{@e}\}$.

Proposition D.12 (Harmony for the Pointed Crumble GLAM).

††margin:

Proof p. Proof of

A reachable pointed environment $e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}$ is normal iff it has the form $(\epsilon\mathrel{\!\textnormal{{¦}}\!}e_{v})$ for some non-empty $v$-environment $e_{v}$.

Implementation.

We prove that that the Pointed Crumble GLAM simulates the Crumble GLAM following the standard schema introduced in Subsect. 5.2 and that we have already employed for the Crumble GLAM in Subsect. 5.3. We only state the machine invariants and the statement of the implementation theorem; the details of the proof can be found in the Appendix D.5 (p. D.5).

Definition D.13 (Reachable state).

A pointed environment is said to be reachable if it is obtained from evaluation steps starting from the translation $\iota(c)$ of a well-named closed crumble $c$.

Lemma D.14 (Invariants for the Pointed Crumble GLAM).

††margin:

Proof p. Proof of

Let $e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}$ be a reachable pointed environment in the Pointed Crumble GLAM:

1. (1)

Freshness:* $e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}$ is well-named.* 2. (2)

Closure:* $e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}$ is closed.* 3. (3)

Rightmost:* $e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}=(e\mathrel{\!\textnormal{{¦}}\!}e_{v})$ for some environment $e$ and some $v$-environment $e_{v}$.*

Theorem D.15 (Implementation).

††margin:

Proof p. Proof of

Let $e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}$ be a reachable pointed environment in the Pointed Crumble GLAM.

1. (1)

Initialisation: ** $(\iota(c))_{\Downarrow}=c$ for every crumble $c$. 2. (2)

Principal projection: ** if $e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}\to_{a}e^{\prime}_{{\,\mathrel{\!\textnormal{{¦}}\!}}}$ then $(e_{{\,\mathrel{\!\textnormal{{¦}}\!}}})_{\Downarrow}\to_{a}(e^{\prime}_{{\,\mathrel{\!\textnormal{{¦}}\!}}})_{\Downarrow}$ for any rule $a\neq\mathsf{sea}$. 3. (3)

Overhead transparency: ** if $e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}\rightarrow_{\mathsf{sea}}e^{\prime}_{{\,\mathrel{\!\textnormal{{¦}}\!}}}$ then $(e_{{\,\mathrel{\!\textnormal{{¦}}\!}}})_{\Downarrow}=(e^{\prime}_{{\,\mathrel{\!\textnormal{{¦}}\!}}})_{\Downarrow}$. 4. (4)

Determinism: ** the transition function $\rightarrow_{\mathsf{pCr}}$ is deterministic. 5. (5)

Halt: ** if $e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}$ is normal then $(e_{{\,\mathrel{\!\textnormal{{¦}}\!}}})_{\Downarrow}$ is normal. 6. (6)

Overhead termination*: $\rightarrow_{\mathsf{sea}}$ terminates.*

Therefore, the Pointed Crumble GLAM (with its transition function $\rightarrow_{\mathsf{pCr}}$), the Crumble GLAM (with $\rightarrow_{\mathsf{Cr}}$), and the read-back $(\cdot)_{\Downarrow}$ form an implementation system.

Complexity

We reuse the measures introduced in Subsect. 5.3. The only difference here is that we need to bound also the number of $\mathsf{sea}$ steps, which intuitively depends on the length of the pointed environment that is being evaluated. We define the new measure $|\cdot|_{\textup{len}}$ on environments and crumbles, that simply counts the number of entries:

[TABLE]

After each ${\beta_{v}}/\textsf{ift}/\textsf{iff}$ step, the measure increases by the length of the body that is being concatenated. For every environment $e$, we define the constant $L(e)$ that bounds the length of the bodies occurring anywhere in $e$:

[TABLE]

We extend the definitions above to pointed environments and crumbles in the expected way:

[TABLE]

Remark D.1.

For any crumble $c$ and term $t$: $|c|_{\textup{len}}=|\iota(c)|_{\textup{len}}$, $L(\underline{t})\leq|t|$ and $|\underline{t}|_{\textup{len}}\leq|t|$.

As usual, an execution $\rho$ is a sequence of evaluation steps, and we use $|\rho|_{a}$ to count the number of $a$-evaluation steps in $\rho$.

By Thm. D.15, all transition steps but $\mathsf{sea}$ steps are mapped one-to-one to corresponding transition steps in the Crumble GLAM. As for the number of $\mathsf{sea}$ transitions:

Lemma D.16 (Number of $\mathsf{sea}$-transitions).

††margin:

Proof p. Proof of

Let $c$ be a well-named crumble, and let $\rho\colon\iota(c)\rightarrow_{\mathsf{pCr}}^{*}e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}=(e\mathrel{\!\textnormal{{¦}}\!}e_{v})$ an execution in the Pointed Crumble GLAM. Then $|e|_{\textup{len}}\leq|c|_{\textup{len}}+(|\rho|_{{\beta_{v}}}+|\rho|_{\textsf{ift}}+|\rho|_{\textsf{iff}})\cdot L(c)-|\rho|_{\mathsf{sea}}$.

Corollary D.17.

Let $t$ be a term. For a normalizing execution $\rho$ in the Pointed Crumble GLAM starting from $\iota(\underline{t})$, we have $|\rho|_{\mathsf{sea}}\leq(|\rho|_{{\mathsf{p}}}+1)\cdot|t|$.

Cost of evaluation.

The cost of all transitions but $\mathsf{sea}$ was already discussed in Subsect. 5.3. The cost of a $\mathsf{sea}$ transition is clearly $O(1)$.

Theorem D.18 (The Pointed Crumble GLAM is bilinear).

††margin:

Proof p. Proof of

For any closed term $t$ and any Pointed Crumble GLAM execution $\rho\colon\iota(\underline{t})\rightarrow_{\mathsf{pCr}}^{*}e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}$, the cost of implementing $\rho$ on a RAM is $O((|\rho|_{{\mathsf{p}}}+1)\cdot|t|)$.

The previous theorem also has a consequence for the non-pointed case. Since the theorem shows that the cost of searching for redexes and the (un)plugging operations can indeed be realised in bilinear time, it is also true that the Crumble GLAM can be implemented in bilinear time, improving Thm. 5.10 by removing the up to search and (un)plugging side condition.

Corollary D.19 (The Crumble GLAM is bilinear).

For any closed term $t$ and any Crumble GLAM execution $\rho\colon\underline{t}\rightarrow_{\mathsf{Cr}}^{*}c$, the cost of implementing $\rho$ on a RAM is $O((|\rho|_{{\mathsf{p}}}+1)\cdot|t|)$.

D.5. Proofs of Appendix D.4 (p. D.4)

Lemma D.20.

Let $b$ be a bite and $e$ an environment. $[x{\shortleftarrow}b]e$ is an $v$-environment if and only if $(b,e)$ is a $v$-crumble.

Proof.

Obvious from the definition of $v$-environment and $v$-crumble. ∎

Proof of 0 (Lemma D.14).

“??”

Proof.

By induction on the length of the evaluation sequence leading to $e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}$. The base cases hold by the definition of reachability and by the definition of $\iota(\cdot)$. As for the inductive cases, we proceed by cases on the transition rules:

1. (1)

For ${\beta_{v}}$ the claim follows from the side condition. The rules in $\{\textsf{ift},\textsf{iff},\textsf{ife},\textsf{@e},\mathsf{sea}\}$ do not increase the number of explicit substitutions occuring in $e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}$ outside of abstractions, hence the claim follows from the i.h.. The rules in $\{\mathsf{sub}_{\mathit{var}},\mathsf{sub}_{l},\mathsf{sub}_{\mathsf{if}}\}$ copy a practical value from the environment $e_{v}$: note that $e_{v}(x)$ is either an abstraction (which does not influence well-namedness) or a boolean or an error (which do not contain explicit substitutions). 2. (2)

Similar to the discussion in Lemma 5.5. 3. (3)

The rules in $\{{\beta_{v}},\textsf{ift},\textsf{iff},\textsf{ife},\textsf{@e},\mathsf{sub}_{\mathit{var}},\mathsf{sub}_{l},\mathsf{sub}_{\mathsf{if}}\}$ do not change the evaluated part, hence the claim follows from the i.h.. As for the $\mathsf{sea}$ rule, by Lemma D.20 it suffices to prove that $(b,e_{v})$ is a $v$-crumble, knowing that the other transition rules cannot be applied. This follows from the side condition of the $\mathsf{sea}$ rule: the crumble $b$ is necessarily a practical value, as the other cases in which the free variable $x$ occurs are not possible because $e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}$ is a closed pointed environment. ∎

Proof of 0 (Prop. D.12).

“??”

Proof.

The proof of the implication from right to left is trivial. Let us now prove the other direction. Let $e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}$ be a reachable normal pointed environment. By Lemma D.14, $e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}$ has the form $(e\mathrel{\!\textnormal{{¦}}\!}e_{v})$. $e$ cannot be non-empty, because otherwise one of the transition rules in $\{{\beta_{v}},\textsf{ift},\textsf{iff},\textsf{ife},\textsf{@e},\mathsf{sub}_{\mathit{var}},\mathsf{sub}_{l},\mathsf{sub}_{\mathsf{if}},\mathsf{sea}\}$ could be applied, contradicting the hypothesis that $e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}$ is normal. ∎

Lemma D.21.

For every pointed environment $(e[x{\shortleftarrow}b]\mathrel{\!\textnormal{{¦}}\!}e^{\prime})$: $(e[x{\shortleftarrow}b]\mathrel{\!\textnormal{{¦}}\!}e^{\prime})_{\Downarrow}=(C\langle b,e^{\prime}\rangle)_{\Downarrow}$ where $C$ is:

[TABLE]

Proof.

Easy by the definition of $(\cdot)_{\Downarrow}$. ∎

Proof of 0 (Thm. D.15).

“??”

Proof.

1. (1)

Let $c=(b,e)$: by the definitions, $(\iota(c))_{\Downarrow}=([x{\shortleftarrow}b]e\mathrel{\!\textnormal{{¦}}\!}\epsilon)_{\Downarrow}=(b,e\epsilon)=c$. 2. (2)

There is a clear one-to-one correspondence between the transitions of the Pointed Crumble GLAM and the Crumble GLAM (apart from $\mathsf{sea}$). In order to prove it, one may proceed by cases on each transition rule, but we just show the case of ${\beta_{v}}$ as the others are similar.

Suppose $e[x{\shortleftarrow}(\lambda y.c)\,v]\mathrel{\!\textnormal{{¦}}\!}e_{v}\rightarrow_{{\beta_{v}}}e[x{\shortleftarrow}b]e^{\prime}[z{\shortleftarrow}v]\mathrel{\!\textnormal{{¦}}\!}e_{v}$. By Lemma D.21, $(e[x{\shortleftarrow}(\lambda y.c)\,v]\mathrel{\!\textnormal{{¦}}\!}e_{v})_{\Downarrow}=C\langle((\lambda y.c)\,v,e_{v})\rangle$ and $(e[x{\shortleftarrow}b]e^{\prime}[z{\shortleftarrow}v]\mathrel{\!\textnormal{{¦}}\!}e_{v})_{\Downarrow}=C\langle b,e^{\prime}[z{\shortleftarrow}v]e_{v}\rangle$ for some crumble context $C$. Clearly also $C\langle((\lambda y.c)\,v,e_{v})\rangle\rightarrow_{{\beta_{v}}}C\langle(b,e^{\prime}[z{\shortleftarrow}v]e_{v})\rangle$. 3. (3)

By inspection of the rule $\mathsf{sea}$. We need to prove that $(e[x{\shortleftarrow}b]\mathrel{\!\textnormal{{¦}}\!}e_{v})_{\Downarrow}=(e\mathrel{\!\textnormal{{¦}}\!}[x{\shortleftarrow}b]e_{v})_{\Downarrow}$. By cases on the structure of $e$: if $e=\epsilon$, then $(\epsilon[x{\shortleftarrow}b]\mathrel{\!\textnormal{{¦}}\!}e_{v})_{\Downarrow}=(b,e_{v})=(\epsilon\mathrel{\!\textnormal{{¦}}\!}[x{\shortleftarrow}b]e_{v})_{\Downarrow}$. If instead $e=[y{\shortleftarrow}b^{\prime}]e^{\prime}$, then $(e[x{\shortleftarrow}b]\mathrel{\!\textnormal{{¦}}\!}e_{v})_{\Downarrow}=(b^{\prime},e^{\prime}[x{\shortleftarrow}b]e_{v})=(e\mathrel{\!\textnormal{{¦}}\!}[x{\shortleftarrow}b]e_{v})_{\Downarrow}$. 4. (4)

The rule $\mathsf{sea}$ can be applied by definition only when the other rules cannot be applied. The remaining rules apply to a pointed environment of the form $(e[x{\shortleftarrow}b]\mathrel{\!\textnormal{{¦}}\!}e_{v})$, for distinct shapes of $b$:

• •

The rules $\{{\beta_{v}},\textsf{@e},\mathsf{sub}_{l}\}$ apply when $b$ is an application, and respectively the application of an abstraction to a crumbled value, of a boolean/error to a crumbled value, and of a variable to a crumbled value.

• •

The rule $\mathsf{sub}_{\mathit{var}}$ applies when $b$ is a variable.

• •

The rules in $\{\textsf{ift},\textsf{iff},\textsf{ife},\mathsf{sub}_{\mathsf{if}}\}$ apply when $b$ is a $\mathsf{if}\mbox{-}\mathsf{then}\mbox{-}\mathsf{else}$, and in clearly disjoint cases according to the structure of the condition: respectively, when the condition is $\mathsf{true}$, $\mathsf{false}$, an abstraction or an error, and a variable.

• •

Finally, note that no single rule in $\{\mathsf{sub}_{\mathit{var}},\mathsf{sub}_{l},\mathsf{sub}_{\mathsf{if}}\}$ can transition to different pointed environments due to the lookup of a variable which has multiple occurrences in the environment: the lookup is deterministic because the environment is well-named (Lemma D.14.1). 5. (5)

By Prop. D.12, $e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}$ is normal iff it has the form $(\epsilon\mathrel{\!\textnormal{{¦}}\!}e_{v})$ for some non-empty $v$-environment $e_{v}$. Then $(e_{{\,\mathrel{\!\textnormal{{¦}}\!}}})_{\Downarrow}=(\epsilon\mathrel{\!\textnormal{{¦}}\!}e_{v})_{\Downarrow}$ which is a $v$-crumble by Lemma D.20. By Prop. 5.3, $(e_{{\,\mathrel{\!\textnormal{{¦}}\!}}})_{\Downarrow}$ is normal. 6. (6)

Immediate consequence of forthcoming Cor. D.17 (proved independently). ∎

Proof of 0 (Lemma D.16).

“??”

Proof.

By induction on the length of $\rho$. In the base case $|e|_{\textup{len}}=|c|_{\textup{len}}$ and $|\rho|_{{\beta_{v}}}=|\rho|_{\textsf{ift}}=|\rho|_{\textsf{iff}}=|\rho|_{\mathsf{sea}}=0$. In the inductive case, use the i.h. and proceed by cases on the transition rules. The transitions $\mathsf{sub}_{\mathit{var}},\mathsf{sub}_{l},\mathsf{sub}_{\mathsf{if}}$ do not change the measure of the unevaluated environment because $e_{v}(x)$ is a value, whose measure is 0 by definition. A $\mathsf{sea}$ transition decreases by 1 the measure of the unevaluated part. A ${\beta_{v}}/\textsf{ift}$ transition increases the measure of the unevaluated part by a number bound by $L(c)$. A iff transition increases the measure of the unevaluated part by a number bound by $L(d)$. All remaining transitions do not increase the measure of the unevaluated environment. ∎

Proof of 0 (Thm. D.18).

“??”

Proof.

The cost $|\rho|$ of $\rho$ is the the total cost of principal transitions (which was proved in Subsect. 5.3 to be bilinear in the number of principal steps (plus one) and the size of the initial crumble when starting from terms) plus the total cost of $\mathsf{sea}$ transitions. The cost of $\mathsf{sea}$ transitions in $\rho$ is linear in the number of $\mathsf{sea}$ transitions, and therefore by Cor. D.17, again bilinear in the number of principal steps (plus one) and the size of the initial term. ∎

Appendix E Proofs of Sect. 6 (open case)

E.1. Proofs of Subsect. 6.1

Lemma E.1 (Composition of right f-contexts).

Let $R$ and $R^{\prime}$ be right f-contexts. Then their composition $R\langle R^{\prime}\rangle$ is a right f-context.

Proof.

By induction on the right f-context $R$. Cases:

• •

Hole, i.e. $R\coloneqq\langle\cdot\rangle$: then, $R\langle R^{\prime}\rangle=R^{\prime}$ is a right f-context by hypothesis.

• •

Right, i.e. $R\coloneqq tR^{\prime\prime}$: then, $R\langle R^{\prime}\rangle=t(R^{\prime\prime}\langle R^{\prime}\rangle)$ is a right f-context because $R^{\prime\prime}\langle R^{\prime}\rangle$ is a right f-context by i.h.

• •

Left, i.e. $R\coloneqq R^{\prime\prime}f$: then, $R\langle R^{\prime}\rangle=R^{\prime\prime}\langle R^{\prime}\rangle f$ is a right f-context because $R^{\prime\prime}\langle R^{\prime}\rangle$ is a right f-context by i.h.

• •

$\mathsf{if}\mbox{-}\mathsf{then}\mbox{-}\mathsf{else}$, i.e. $R\coloneqq(\mathsf{if}\,R^{\prime\prime}\,\mathsf{then}\,t\,\mathsf{else}\,u)$: then, $R\langle R^{\prime}\rangle\allowbreak=\allowbreak(\mathsf{if}\,R^{\prime\prime}\langle R^{\prime}\rangle\,\mathsf{then}\,t\,\mathsf{else}\,u)$ is a right f-context because $R^{\prime\prime}\langle R^{\prime}\rangle$ is a right f-context by i.h. ∎

Proof of 0 (Prop. 6.2).

“??”

Proof.

1. (1)

We show separately the two implications:

$(\Rightarrow)$**: **

Proof by induction on the structure of $t$.

• **•: **

Case $t$ value: trivial.

• **•: **

Case $t=us$ for some terms $u$ and $s$: we show that then $t$ is an inert term (and hence a fireball). Since $t$ is $\mathsf{c}\beta_{\!f}$-normal, then $s$ is $\mathsf{c}\beta_{\!f}$-normal, and hence by i.h. $s$ is a fireball. Since $t$ is $\mathsf{c}\beta_{\!f}$-normal and $s$ is a fireball, then also $u$ must be $\mathsf{c}\beta_{\!f}$-normal, and hence a fireball by i.h. We proceed by cases on $u$, showing that the only possible cases are when $u$ is a variable or an inert term (and so $t$ is a fireball). Indeed, $u$ cannot be an abstraction (because otherwise the rule $\rightarrow_{\beta_{\!f}}$ may be applied, contradicting the hypothesis that $t$ is $\mathsf{c}\beta_{\!f}$-normal); it cannot be a boolean or $\mathsf{err}$ (because otherwise the rule $\rightarrow_{\textsf{@e}}$ may be applied).

• **•: **

Case $t=\mathsf{if}\,u\,\mathsf{then}\,s\,\mathsf{else}\,r$ for some terms $u,s,r$: we show that the only possible cases are when $u$ is a variable or a inert term (and hence $t$ is a fireball). Since $t$ is $\mathsf{c}\beta_{\!f}$-normal, then $u$ is $\mathsf{c}\beta_{\!f}$-normal, and hence by i.h. $u$ is a fireball. $u$ it cannot be an abstraction or $\mathsf{err}$ (because otherwise the rule $\rightarrow_{\textsf{ife}}$ may be applied, contradicting the hypothesis that $t$ is $\mathsf{c}\beta_{\!f}$-normal); it cannot be a boolean (because otherwise one of the rules $\rightarrow_{\textsf{ift}}$ or $\rightarrow_{\textsf{iff}}$ may be applied).

$(\Leftarrow)$**: **

By hypothesis, $t$ is a fireball, i.e. either a value or an inert term.

• **•: **

Value: We proceed by cases on the definition of value. If $t$ is a variable, then it is clearly $\mathsf{c}\beta_{\!f}$-normal. If $t$ is an abstraction, then it is $\mathsf{c}\beta_{\!f}$-normal since $\rightarrow_{\mathsf{c}\beta_{\!f}}$ does not reduce under $\lambda$’s. Otherwise $t$ is a either a boolean or $\mathsf{err}$, which clearly are $\mathsf{c}\beta_{\!f}$-normal.

• **•: **

Inert term: We proceed by cases on the definition of inert term. If $t=xf$ for some variable $x$ and some fireball $f$, then $f$ is $\mathsf{c}\beta_{\!f}$-normal by i.h., and $x$ is clearly $\mathsf{c}\beta_{\!f}$-normal and different from abstractions, booleans and $\mathsf{err}$; therefore, no reduction rule can be applied to $t$, i.e. $t$ is $\mathsf{c}\beta_{\!f}$-normal. If $t=xf$ or $t=if$ for some inert term $i$ and some fireball $f$, then $i$ and $f$ are $\mathsf{c}\beta_{\!f}$-normal by i.h.; moreover, $i$ is not an abstraction or boolean or $\mathsf{err}$; therefore, no reduction rule can be applied to $t$, i.e. $t$ is $\mathsf{c}\beta_{\!f}$-normal. Otherwise, $t=\mathsf{if}\,u\,\mathsf{then}\,s\,\mathsf{else}\,r$ for some terms $u,s,r$ where $u$ is either a variable or a inert term; since $u$ is $\mathsf{c}\beta_{\!f}$-normal (if $u$ is a inert term, this holds by i.h.), then no reduction rule can be applied to $t$, i.e. $t$ is $\mathsf{c}\beta_{\!f}$-normal. ∎ 2. (2)

The direction ($\Leftarrow$) is exactly Lemma E.3. The direction ($\Rightarrow$) is proved by induction on the definition of $t\rightarrow_{\mathsf{c}\beta_{\!f}}u$, in a way that is analogue to the proof of Lemma E.3.

Lemma E.2 (Fireballs are closed under substitution and anti-substitution of inert terms).

Let $t$ be a term and $i$ be an inert term. Then, $t\{x{\shortleftarrow}i\}$ is a fireball (resp. an abstraction) if and only if $t$ is a fireball (resp. an abstraction). Moreover, $t\{x{\shortleftarrow}i\}=\mathsf{true}$ (resp. $t\{x{\shortleftarrow}i\}=\mathsf{false}$; $t\{x{\shortleftarrow}i\}=\mathsf{err}$) if and only if $t=\mathsf{true}$ (resp. $t=\mathsf{false}$; $t=\mathsf{err}$).

Proof.

The left-to-right direction ($\Rightarrow$) is proved by a simple induction on the fireball structure of $t\{x{\shortleftarrow}i\}$. Conversely, the right-to-left direction ($\Leftarrow$) is proved by a simple induction on the inert structure of $t$. ∎

Lemma E.3 (Substitution of inert terms does not create redexes).

Let $t,u$ be terms and $i$ be an inert term. There is a term $s$ such that, if $t\{x{\shortleftarrow}i\}\rightarrow_{\mathsf{c}\beta_{\!f}}u$ then $t\rightarrow_{\mathsf{c}\beta_{\!f}}s$ and $u=s\{x{\shortleftarrow}i\}$.

Proof.

By induction on the right fireball context closing the redex. Cases:

• •

Step at the root: Sub-cases:

1. (1)

Beta-step, i.e. $t\{x{\shortleftarrow}i\}=(\lambda y.r\{x{\shortleftarrow}i\})q\{x{\shortleftarrow}i\}\rightarrow_{\beta_{\!f}}r\{x{\shortleftarrow}i\}\{y{\shortleftarrow}q\{x{\shortleftarrow}i\}\}\allowbreak\eqqcolon u$ where $t\coloneqq(\lambda x.r)q$ and $q\{x{\shortleftarrow}i\}$ is a fireball. By Lemma E.2, $q$ is a fireball and hence $t=(\lambda x.r)q\rightarrow_{\mathsf{c}\beta_{\!f}}r\{y{\shortleftarrow}q\}$. So, $s\coloneqq r\{y{\shortleftarrow}q\}$ satisfies the statement, as $s\{x{\shortleftarrow}i\}=r\{y{\shortleftarrow}q\}\{x{\shortleftarrow}i\}=u$. 2. (2)

Conditional step with $\mathsf{true}$, i.e. $t\{x{\shortleftarrow}i\}=\mathsf{if}\,\allowbreak\mathsf{true}\,\mathsf{then}\,s\{x{\shortleftarrow}i\}\,\mathsf{else}\,q\{x{\shortleftarrow}i\}\allowbreak\rightarrow_{\textsf{ift}}s\{x{\shortleftarrow}i\}\eqqcolon u$ where $t\coloneqq\mathsf{if}\,r\,\mathsf{then}\,s\,\mathsf{else}\,q$ for some term $r$ such that $r\{x{\shortleftarrow}i\}=\mathsf{true}$. By Lemma E.2, $r=\mathsf{true}$ and hence $t=\mathsf{if}\,\mathsf{true}\,\mathsf{then}\,s\,\mathsf{else}\,q\rightarrow_{\textsf{ift}}s$. 3. (3)

Conditional step with $\mathsf{false}$, i.e. $t\{x{\shortleftarrow}i\}=\mathsf{if}\,\allowbreak\mathsf{true}\,\mathsf{then}\,q\{x{\shortleftarrow}i\}\,\mathsf{else}\,s\{x{\shortleftarrow}i\}\allowbreak\rightarrow_{\textsf{iff}}s\{x{\shortleftarrow}i\}\eqqcolon u$ where $t\coloneqq\mathsf{if}\,r\,\mathsf{then}\,q\,\mathsf{else}\,s$ for some term $r$ such that $r\{x{\shortleftarrow}i\}=\mathsf{false}$. By Lemma E.2, $r=\mathsf{false}$ and hence $t=\mathsf{if}\,\mathsf{false}\,\mathsf{then}\,q\,\mathsf{else}\,s\rightarrow_{\textsf{iff}}s$. 4. (4)

Conditional step to error, i.e. $t\{x{\shortleftarrow}i\}=\mathsf{if}\,r\,\mathsf{then}\,q\{x{\shortleftarrow}i\}\,\mathsf{else}\,m\{x{\shortleftarrow}i\}\allowbreak\rightarrow_{\textsf{ife}}\mathsf{err}\eqqcolon u$ where $r\coloneqq\lambda y.{r^{\prime}}$ or $r=\mathsf{err}$, and $t\coloneqq\mathsf{if}\,p\,\mathsf{then}\,q\,\mathsf{else}\,m$ for some term $p$ such that $p\{x{\shortleftarrow}i\}=r$. By Lemma E.2, $p$ is either an abstraction or $\mathsf{err}$ and hence $t=\mathsf{if}\,r\,\mathsf{then}\,q\,\mathsf{else}\,m\allowbreak\rightarrow_{\textsf{ife}}\mathsf{err}$. So, $s\coloneqq\mathsf{err}$ satisfies the statement, as $s\{x{\shortleftarrow}i\}=\mathsf{err}=u$. 5. (5)

Application step to error, i.e. $t\{x{\shortleftarrow}i\}=r\{x{\shortleftarrow}i\}q\{x{\shortleftarrow}i\}\rightarrow_{\textsf{@e}}\mathsf{err}\eqqcolon u$ where $r\{x{\shortleftarrow}i\}\in\{\mathsf{true},\mathsf{false},\mathsf{err}\}$ and $t\coloneqq rq$. By Lemma E.2, $r\in\{\mathsf{true},\mathsf{false},\mathsf{err}\}$ and hence $t=rq\rightarrow_{\textsf{@e}}\mathsf{err}$. So, $s\coloneqq\mathsf{err}$ satisfies the statement, as $s\{x{\shortleftarrow}i\}=\mathsf{err}=u$.

• •

Application left, i.e. $t\{x{\shortleftarrow}i\}=r\{x{\shortleftarrow}i\}f\{x{\shortleftarrow}i\}\rightarrow_{\mathsf{c}\beta_{\!f}}pf\{x{\shortleftarrow}i\}\eqqcolon u$ where $t\coloneqq rf$ and $r\{x{\shortleftarrow}i\}\rightarrow_{\mathsf{c}\beta_{\!f}}p$. By i.h. there is a term $s^{\prime}$ such that $p=s^{\prime}\{x{\shortleftarrow}i\}$ and $r\rightarrow_{\mathsf{c}\beta_{\!f}}s^{\prime}$. Then $s\coloneqq s^{\prime}f$ satisfies the statement, as $s\{x{\shortleftarrow}i\}=s^{\prime}\{x{\shortleftarrow}i\}f{x}{i}=u$.

• •

Application right, i.e. $t\{x{\shortleftarrow}i\}=q\{x{\shortleftarrow}i\}r\{x{\shortleftarrow}i\}\rightarrow_{\mathsf{c}\beta_{\!f}}q\{x{\shortleftarrow}i\}p\eqqcolon u$ where $t\coloneqq qr$ and $r\{x{\shortleftarrow}i\}\rightarrow_{\mathsf{c}\beta_{\!f}}p$. Analogous to the application left case, just switch left and right.

• •

If-then-else, i.e. $t\{x{\shortleftarrow}i\}=\mathsf{if}\,r\{x{\shortleftarrow}i\}\,\mathsf{then}\,q\{x{\shortleftarrow}i\}\,\mathsf{else}\,p\{x{\shortleftarrow}i\}\rightarrow_{\mathsf{c}\beta_{\!f}}\mathsf{if}\,m\,\mathsf{then}\,q\{x{\shortleftarrow}i\}\,\mathsf{else}\,p\{x{\shortleftarrow}i\}\eqqcolon u$ where $t\coloneqq\mathsf{if}\,r\,\mathsf{then}\,q\,\mathsf{else}\,p$ and $r\{x{\shortleftarrow}i\}\rightarrow_{\mathsf{c}\beta_{\!f}}m$. By i.h. there is a term $s^{\prime}$ such that $m=s^{\prime}\{x{\shortleftarrow}i\}$ and $r\rightarrow_{\mathsf{c}\beta_{\!f}}s^{\prime}$. Then $s\coloneqq\mathsf{if}\,s^{\prime}\,\mathsf{then}\,q\,\mathsf{else}\,p$ satisfies the statement, as $s\{x{\shortleftarrow}i\}=\mathsf{if}\,s^{\prime}\{x{\shortleftarrow}i\}\,\mathsf{then}\,q\{x{\shortleftarrow}i\}\,\mathsf{else}\,p\{x{\shortleftarrow}i\}=u$. ∎

E.2. Proofs of Subsect. 6.2

E.2.1. Evaluated environments.

Given the terms $t_{1},\dots,t_{n}$ and pairwise distinct variables $x_{1},\dots,x_{n}$, let $\sigma\coloneqq\{x_{1}{\shortleftarrow}t_{1},\ldots,x_{n}{\shortleftarrow}t_{n}\}$ be the simultaneous capture-avoiding substitution of $t_{i}$ for $x_{i}$, for all $1\leq i\leq n$. In particular, if $n=0$ then $\sigma=\{\}$, the identity (or empty) substitution. If $u$ is a term and $y\neq x_{i}$ for all $1\leq i\leq n$, we set $\{y{\shortleftarrow}u\}\cup\sigma\coloneqq\{y{\shortleftarrow}u,x_{1}{\shortleftarrow}t_{1},\dots,x_{n}{\shortleftarrow}t_{n}\}$.

Given an environment $e$, the simultaneous substitution $\sigma(e)$ associated with $e$ is defined by induction on the length of $e$:

[TABLE]

Lemma E.4 (Semi-closure under substitution).

Let $v$ be a value, $x_{1},\dots,x_{n}$ be pairwise distinct variables, and $f_{1},\dots,f_{n}$ be fireballs. Then $v\{x_{1}{\shortleftarrow}f_{1},\ldots,x_{n}{\shortleftarrow}f_{n}\}$ is a fireball. If moreover $v$ is a $\lambda$-abstraction, then $v\{x_{1}{\shortleftarrow}f_{1},\ldots,x_{n}{\shortleftarrow}f_{n}\}$ is a $\lambda$-abstraction.

Proof.

Let $\sigma\coloneqq\{x_{1}{\shortleftarrow}f_{1},\ldots,x_{n}{\shortleftarrow}f_{n}\}$. By cases on the definition of value:

• •

Variable, i.e. either $v\coloneqq x_{i}$ for some $1\leq i\leq n$ and then $v\sigma=f_{i}$ which is a fireball by hypothesis; or $v\coloneqq y\neq x_{i}$ for all $1\leq i\leq n$ and then $v\sigma=y$ which is a fireball.

• •

Abstraction, i.e. $v\coloneqq\lambda y.{u}$ and we can suppose without loss of generality that $y\notin\bigcup_{i=1}^{n}{\sf fv}(f_{i})\cup\{x_{1},\dots,x_{n}\}$; therefore, $v\sigma=\lambda y.{(u\sigma)}$ which is a $\lambda$-abstraction and hence a fireball.

• •

Booleans and errors, i.e. $v\in\{\mathsf{true},\mathsf{false},\mathsf{err}\}$. Trivial since $v\sigma=v$. ∎

Lemma E.5 (Read-back to fireball).

For every crumbled value $v$ and $f$-environment $e_{\!f}$, one has that $(v,e_{\!f})_{\downarrow}$ is a fireball. If moreover $v$ is a practical value, then $(v,e_{\!f})_{\downarrow}$ is a practical value.

Proof.

By induction on the length of $e_{\!f}$. We proceed by cases on the shape of $v$.

• •

Abstraction: If $e_{\!f}\coloneqq\epsilon$, then clearly $(v,e_{\!f})_{\downarrow}=v_{\downarrow}$ is a $\lambda$-abstraction and hence a fireball. Otherwise $e_{\!f}\coloneqq e^{\prime}_{\!f}[x{\shortleftarrow}b]$ where $b$ is a bite such that $b_{\downarrow}$ is a fireball: thus, $(v,e_{\!f})_{\downarrow}=(v,e^{\prime}_{\!f})_{\downarrow}\{x{\shortleftarrow}b_{\downarrow}\}$; by i.h., $(v,e^{\prime}_{\!f})_{\downarrow}$ is a $\lambda$-abstraction, thus $(v,e_{\!f})_{\downarrow}$ is a $\lambda$-abstraction (and so a fireball) by Lemma E.4.

• •

Booleans and errors: the proof is identical to the previous case.

• •

Variable: If $v\coloneqq x\notin\mathsf{dom}(e_{\!f})$, then $(v,e_{\!f})_{\downarrow}=x$ which is a fireball; otherwise $v\coloneqq x\in\mathsf{dom}(e_{\!f})$ with $e_{\!f}\coloneqq e^{\prime}_{\!f}[x{\shortleftarrow}b]e^{\prime\prime}_{\!f}$, and then $(x,e_{\!f})_{\downarrow}=(b,e^{\prime\prime}_{\!f})_{\downarrow}$ (since $x\notin\mathsf{dom}(e^{\prime}_{\!f})$) is a fireball by definition of $f$-environment, as the $f$-environment $[x{\shortleftarrow}b]e^{\prime\prime}_{\!f}=E\langle(b,e^{\prime\prime}_{\!f})\rangle$ with $E\coloneqq[x{\shortleftarrow}\langle\cdot\rangle]$. ∎

Lemma E.6.

Let $e_{\!f}$ well-named. If $(x,e_{\!f})_{\downarrow}$ is a practical value, then $e_{\!f}(x)$ is a practical value.

Proof.

Assume by contradiction that $x$ is not defined in $e_{\!f}$: then by Lemma C.5 $(x,e_{\!f})_{\downarrow}=(x,\epsilon)_{\downarrow}=x$, contradicting the hypothesis that $(x,e_{\!f})_{\downarrow}$ is a practical value. Therefore $x$ must be defined in $e_{\!f}$, i.e. $e_{\!f}\coloneqq e^{\prime}_{\!f}[x{\shortleftarrow}b]e^{\prime\prime}_{\!f}$ with $b\coloneqq e_{\!f}(x)$. By the hypothesis that $e_{\!f}$ is well-named, $x\not\in\mathsf{dom}(e^{\prime}_{\!f})$; therefore $(x,e_{\!f})_{\downarrow}=(b,e^{\prime\prime}_{\!f})_{\downarrow}$ by Lemma C.9. By the definition of $e_{\!f}$, since $(b,e^{\prime\prime}_{\!f})_{\downarrow}$ is a practical value, then also $b$ is a practical value, and we conclude. ∎

Lemma E.7.

Let $c=(b,e_{\!f})$ be a well-named crumble, and let $b$ have the following property: either $b$ is a practical value, or $b$ is $x$ or $xv$ or $\mathsf{if}\,x\,\mathsf{then}\,c\,\mathsf{else}\,d$ but $x$ is not defined in $e_{\!f}$ or $e_{\!f}(x)$ is not a practical value. Then $c$ is a $f$-crumble.

Proof.

Let $c=(b,e_{\!f})$ as above: it suffices to prove that $(b,e_{\!f})_{\downarrow}$ is a fireball, and that if $(b,e_{\!f})_{\downarrow}$ is a practical value, then also $b$ is a practical value. By cases on the property about $b$ in the hypothesis:

• •

Abstraction: nothing to prove because $(b,e_{\!f})_{\downarrow}$ is an abstraction by Lemma E.5 and thus a fireball.

• •

Booleans and errors: nothing to prove because $(b,e_{\!f})_{\downarrow}$ is a boolean or an error and thus a fireball.

• •

Variable, i.e. $b=x$ for some $x$ when $x$ is not defined in $e_{\!f}$ or $e_{\!f}(x)$ is not a practical value. $(b,e_{\!f})_{\downarrow}$ is a fireball by Lemma E.5. Let us now assume that $(b,e_{\!f})_{\downarrow}$ is a practical value, and show that it is not possible: in fact by Lemma E.6 $e_{\!f}(x)$ must then be defined and a practical value, contradicting the hypothesis.

• •

Application of a variable to a crumbled value, i.e. $b=xv$ when $x$ is not defined in $e_{\!f}$ or $e_{\!f}(x)$ is not a practical value. Note that $(b,e_{\!f})_{\downarrow}=(x,e_{\!f})_{\downarrow}(v,e_{\!f})_{\downarrow}$, where both $(x,e_{\!f})_{\downarrow}$ and $(v,e_{\!f})_{\downarrow}$ are fireballs by Lemma E.5. If $(x,e_{\!f})_{\downarrow}$ is inert there is nothing else to prove, because then $(b,e_{\!f})_{\downarrow}$ is a fireball, and clearly not a practical value. The case when $(x,e_{\!f})_{\downarrow}$ is a practical value is not possible: again by Lemma E.6 $e_{\!f}(x)$ should be defined and a practical value, contradicting the hypothesis.

• •

$\mathsf{if}\mbox{-}\mathsf{then}\mbox{-}\mathsf{else}$ where the guard is a variable, i.e. $b=\mathsf{if}\,x\,\mathsf{then}\,c\,\mathsf{else}\,d$ when $x$ is not defined in $e_{\!f}$ or $e_{\!f}(x)$ is not a practical value. Note that $(b,e_{\!f})_{\downarrow}=\mathsf{if}\,(x,e_{\!f})_{\downarrow}\,\mathsf{then}\,(c\mathrel{@}e_{\!f})_{\downarrow}\,\mathsf{else}\,(d\mathrel{@}e_{\!f})_{\downarrow}$, where $(x,e_{\!f})_{\downarrow}$ is a fireball by Lemma E.5. If $(x,e_{\!f})_{\downarrow}$ is inert there is nothing else to prove, because then $(b,e_{\!f})_{\downarrow}$ is a fireball, and clearly not a practical value. The case when $(x,e_{\!f})_{\downarrow}$ is a practical value is not possible: again by Lemma E.6 $e_{\!f}(x)$ should be defined and a practical value, contradicting the hypothesis. ∎

Corollary E.8.

If the well-named crumble $(b,e_{\!f})$ is normal, then it is a $f$-crumble.

Proof of 0 (Prop. 6.3).

“??”

Proof.

• $(\Rightarrow)$

Let $c=(b,e)$ be well-named and normal. We proceed by structural induction on $e$:

• –

if $e=\epsilon$, then $(b,\epsilon)$ is a $f$-crumble by Cor. E.8;

• –

if $e=[x{\shortleftarrow}b^{\prime}]e^{\prime}$, then also the crumble $(b^{\prime},e^{\prime})$ is normal. By i.h. $(b^{\prime},e^{\prime})$ is a $f$-crumble, and therefore $e=[x{\shortleftarrow}b^{\prime}]e^{\prime}$ is a $f$-environment. By Cor. E.8, $c=(b,e)$ is a $f$-crumble.

• $(\Leftarrow)$

Let $c=c_{v}$, we need to prove that $c_{v}$ is normal. Let $c_{v}=C\langle(b,e_{\!f})\rangle$ for some $C,b,e_{\!f}$. First of all, note that by the definition of $c_{v}$, $(b,e_{\!f})_{\downarrow}$ is a fireball, and that if $(b,e_{\!f})_{\downarrow}$ is a practical value, then also $b$ is a practical value. We prove that no reduction rule is applicable to $C\langle(b,e_{\!f})\rangle$:

• –

Rule $\beta_{\!f}$ can be applied only if $b=(\lambda x.b^{\prime})\,v$, but this contradicts the hypothesis that $(b,e_{\!f})_{\downarrow}$ is a fireball, since $((\lambda x.b^{\prime})\,v,e_{\!f})_{\downarrow}=(\lambda x.b^{\prime},e_{\!f})_{\downarrow}\,(v,e_{\!f})_{\downarrow}$ and $(\lambda x.b^{\prime},e_{\!f})_{\downarrow}$ is an abstraction by Lemma E.5.

• –

The analysis for the rules $\textsf{ift},\textsf{iff},\textsf{ife},\textsf{@e}$ is similar to the previous case: in all cases the read-back of the lhs of the rule is not a fireball, contradicting the hypothesis.

• –

Rule $\mathsf{sub}_{\mathit{var}}$ can be applied only if $b$ is some variable $x$ and $e_{\!f}(x)$ is defined and a practical value. This contradicts the hypothesis that if $(b,e_{\!f})_{\downarrow}$ is a practical value, then also $b$ is a practical value.

• –

Rule $\mathsf{sub}_{l}$ can be applied only if $b=xv$ for some $x,v$, and $e_{\!f}(x)$ is defined and a practical value. This contradicts the hypothesis that $(b,e_{\!f})_{\downarrow}$ is a fireball, since $(xv,e_{\!f})_{\downarrow}=(x,e_{\!f})_{\downarrow}(v,e_{\!f})_{\downarrow}$ and $(x,e_{\!f})_{\downarrow}$ is a practical value by Lemma E.5 because $e_{\!f}(x)$ is a practical value.

• –

Rule $\mathsf{sub}_{\mathsf{if}}$ can be applied only if $b=\mathsf{if}\,x\,\mathsf{then}\,c\,\mathsf{else}\,d$ for some $x,c,d$, and $e_{\!f}(x)$ is defined and a practical value. This contradicts the hypothesis that $(b,e_{\!f})_{\downarrow}$ is a fireball, since $(\mathsf{if}\,x\,\mathsf{then}\,c\,\mathsf{else}\,d,e_{\!f})_{\downarrow}=\mathsf{if}\,(x,e_{\!f})_{\downarrow}\,\mathsf{then}\,(c\mathrel{@}e_{\!f})_{\downarrow}\,\mathsf{else}\,(d\mathrel{@}e_{\!f})_{\downarrow}$ and $(x,e_{\!f})_{\downarrow}$ is a practical value by Lemma E.5 because $e_{\!f}(x)$ is a practical value. ∎

E.2.2. The implementation theorem for the Open Crumble GLAM

Lemma E.9 (Invariants for the Open Crumble GLAM).

For every reachable crumble $c$:

1. (1)

Freshness:* $c$ is well-named.* 2. (2)

Disjointedness*: if $c=C\langle(b,e)\rangle$ then $\mathsf{dom}(C)\cap{\sf fv}(b)=\emptyset$.* 3. (3)

Bodies:* any body in $c$ is a subterm (up to renaming) of the initial crumble.* 4. (4)

Weak contextual decoding:* for every decomposition $C\langle(b,e_{\!f})\rangle$ where $(b,e_{\!f})_{\downarrow}$ is not a fireball, if $C^{\prime\prime}$ is a prefix of $C$ then $C^{\prime\prime}_{\downarrow}$ is a right v-context.*

Proof.

By induction on the length of the reduction sequence leading to the crumble $c$. The base cases hold by Lemma 4.5 (by noting that for Point 4, Lemma 4.5.5 implies the weaker statement Lemma E.9.4). As for the inductive cases, we inspect each reduction rule:

• 1.

The substitution transitions $\mathsf{sub}_{\mathit{var}},\mathsf{sub}_{l},\mathsf{sub}_{\mathsf{if}}$ do not change the set of variables occurring on the lhs of substitutions outside abstractions because they copy a value that does not contain any. Hence the claim follows from the i.h.. For the rule $\beta_{\!f}$ the claim follows from the side condition. For the remaining rules $\textsf{ift},\textsf{iff},\textsf{ife},\textsf{@e}$ the claim follows from the fact that all substitutions outside abstractions in the rhs alredy occur in the lhs.

• 2.

The substitution transitions $\mathsf{sub}_{\mathit{var}},\mathsf{sub}_{l},\mathsf{sub}_{\mathsf{if}}$ do not change the domain of the crumble and only copy to the left a value $v$ such that $c=C^{\prime}\langle(v,e^{\prime})\rangle$ and $C$ is a prefix of $C^{\prime}$. Thus the claim follows from the i.h. because $\mathsf{dom}(C)\subseteq\mathsf{dom}(C^{\prime})$ and the free variables of the rhs are a subset of the union of the free variables of the lhs with ${\sf fv}(v)$.

Transition $\beta_{\!f}$ copies to the toplevel and renames the body of an abstraction. By the properties of $\alpha$-renaming ${\sf fv}((c\mathrel{@}[x{\shortleftarrow}v])^{\alpha})={\sf fv}(c\mathrel{@}[x{\shortleftarrow}v])={\sf fv}(\lambda x.c)$. If the $b$ is chosen to be in the crumble context (say $C^{\prime\prime}$) or in $e_{\!f}$ of the reduction rule, then the claim follows from the i.h.. Let instead $(c\mathrel{@}[x{\shortleftarrow}v])^{\alpha}\eqqcolon C^{\prime}\langle(b,e^{\prime})\rangle$ with $C=C^{\prime\prime}\langle C^{\prime}\rangle$: then ${\sf fv}(C^{\prime}\langle(b,e^{\prime})\rangle)={\sf fv}(\lambda x.c)$ and ${\sf fv}(b)\subseteq\mathsf{dom}(e^{\prime})\cup{\sf fv}(\lambda x.c)$. $\mathsf{dom}(e^{\prime})\cap\mathsf{dom}(C)=\emptyset$ by the side condition of $\beta_{\!f}$, and ${\sf fv}(\lambda x.c)\cap\mathsf{dom}(C)=\emptyset$ by i.h., therefore we conclude with ${\sf fv}(b)\cap\mathsf{dom}(C)=\emptyset$.

• 3.

Transitions $\mathsf{sub}_{\mathit{var}},\mathsf{sub}_{l},\mathsf{sub}_{\mathsf{if}}$ may copy an abstraction, but the abstraction was already in the environment, and the claim follows from the i.h.. Transition $\beta_{\!f}$ copies and renames the body of an abstraction that was already in the environment, and the claim follows from the i.h. since the translation commutes with the renaming of free variables (Remark 4.1.3). All the bodies in the rhs of the remaning transitions $\textsf{ift},\textsf{iff},\textsf{ife},\textsf{@e}$ already occur in the lhs and therefore the claim follows from the i.h..

• 4.

Let $\underline{b^{\prime\prime}}\rightarrow^{n}C^{\prime}\langle(b^{\prime},e^{\prime}_{v})\rangle\rightarrow_{a}C\langle(b,e_{v})\rangle$ (where $b$ is not a practical value). Cases of the transition $C^{\prime}\langle(b^{\prime},e^{\prime}_{v})\rangle\rightarrow_{a}C\langle(b,e_{v})\rangle$:

• –

Case $\beta_{\!f}$: $C^{\prime}\langle((\lambda x.c)v,e_{v})\rangle\rightarrow_{{\beta_{v}}}C^{\prime}\langle c^{\alpha}\mathrel{@}([x^{\alpha}{\shortleftarrow}v]e_{v})\rangle$.

Let $C^{\prime\prime}$ be a prefix of $C$. There are two sub-cases:

$C^{\prime\prime}$ is a prefix of $C^{\prime}$: by i.h. $C^{\prime\prime}_{\downarrow}$ is a right v-context.

• *

$C^{\prime}$ is a prefix of $C^{\prime\prime}$, i.e. $C^{\prime\prime}=C^{\prime}\langle C^{\prime\prime\prime}\rangle$ and $c^{\alpha}=C^{\prime\prime\prime}\langle c^{\prime}\rangle$. By Lemma 4.5.4 and Lemma E.9.3 $c$ is the translation of a $\lambda$-term, by Remark 4.1.3 $c^{\alpha}$ is so, and thus by Lemma 4.5.5 $C^{\prime\prime\prime}_{\downarrow}$ is a right v-context. By i.h., $C^{\prime}_{\downarrow}$ is a right v-context as well. Since $C^{\prime\prime}_{\downarrow}=C^{\prime}_{\downarrow}\langle C^{\prime\prime\prime}_{\downarrow}\rangle$ according to Corollary C.11.2, we obtain that $C^{\prime\prime}_{\downarrow}$ is a right v-context as composition of right v-contexts (Lemma B.1).

• –

Case ift: $C^{\prime}\langle(\mathsf{if}\,\mathsf{true}\,\mathsf{then}\,c\,\mathsf{else}\,d,e_{v})\rangle\rightarrow_{{\beta_{v}}}C^{\prime}\langle c\mathrel{@}e_{v}\rangle$. Let $C^{\prime\prime}$ be a prefix of $C$. There are two sub-cases:

$C^{\prime\prime}$ is a prefix of $C^{\prime}$: by i.h. $C^{\prime\prime}_{\downarrow}$ is a right v-context.

• *

$C^{\prime}$ is a prefix of $C^{\prime\prime}$, i.e. $C^{\prime\prime}=C^{\prime}\langle C^{\prime\prime\prime}\rangle$ and $c=C^{\prime\prime\prime}\langle c^{\prime}\rangle$. By Lemma 4.5.4 and Lemma E.9.3 $c$ is the translation of a $\lambda$-term and thus by Lemma 4.5.5 $C^{\prime\prime\prime}_{\downarrow}$ is a right v-context. By i.h., $C^{\prime}_{\downarrow}$ is a right v-context as well. Since $C^{\prime\prime}_{\downarrow}=C^{\prime}_{\downarrow}\langle C^{\prime\prime\prime}_{\downarrow}\rangle$ according to Corollary C.11.2, we obtain that $C^{\prime\prime}_{\downarrow}$ is a right v-context as composition of right v-contexts (Lemma B.1).

• –

Case iff: identical to the previous case.

• –

Cases $\mathsf{sub}_{\mathit{var}},\textsf{ife},\textsf{@e}$: they follow from the i.h. since $C$ is necessarily a prefix of $C^{\prime}$ because $b$ is a practical value.

• –

Cases $\mathsf{sub}_{l}$ and $\mathsf{sub}_{\mathsf{if}}$: they follow from the i.h., since $e^{\prime}_{v}=e_{v}$ and $C=C^{\prime}$. ∎

Lemma E.10 (Determinism).

$\rightarrow_{\mathsf{oCr}}$* is deterministic.*

Proof.

Assume that there exists a crumble that may be decomposed in two ways $C\langle(b,e_{\!f})\rangle=C^{\prime}\langle(b^{\prime},e^{\prime}_{\!f})\rangle$ such that they reduce respectively $C\langle(b,e_{\!f})\rangle\rightarrow_{a}C\langle c\rangle$ and $C^{\prime}\langle(b^{\prime},e^{\prime}_{\!f})\rangle\rightarrow_{b}C^{\prime}\langle d\rangle$ with rules $a,b\in\{\beta_{\!f},\textsf{ift},\textsf{iff},\textsf{ife},\textsf{@e},\mathsf{sub}_{\mathit{var}},\mathsf{sub}_{l},\mathsf{sub}_{\mathsf{if}}\}$.

We prove that it must necessarily be $a=b$, $C=C^{\prime}$, and $c=d$ (up to $\alpha$-equivalence). Three cases:

• •

$C$ strict initial segment of $C^{\prime}$, i.e. $C^{\prime}=C\langle C^{\prime\prime}\rangle$ for some $C^{\prime\prime}\neq\langle\cdot\rangle$. We show that this case is not possible: in fact, it follows that $e_{\!f}=E\langle(b^{\prime},e^{\prime}_{\!f})\rangle$ for some $E$, thus $(b^{\prime},e^{\prime}_{\!f})$ is a $f$-crumble, and by Prop. 6.3 it must be normal, contradicting the hypothesis that $(b^{\prime},e^{\prime}_{\!f})$ and $c$ reduce with rule $b$.

• •

$C=C^{\prime}$. By inspection of the reduction rules, $a=b$: in fact the rule $\beta_{\!f}$ applies only when $b$ is the application of an abstraction to a crumbled value, the rule $\mathsf{sub}_{\mathit{var}}$ only when $b$ is a variable, and the rule $\mathsf{sub}_{l}$ only when $b$ is the application of a variable to a crumbled value, etc. It remains to show that $c=d$ (up to alpha): this follows from the determinism of the lookup in the environment during $\mathsf{sub}_{\mathit{var}},\mathsf{sub}_{l}$ and $\mathsf{sub}_{\mathsf{if}}$ reductions.

• •

$C^{\prime}$ initial segment of $C$, i.e. $C=C^{\prime}\langle C^{\prime\prime}\rangle$. Symmetric to the first case. ∎

Proposition E.11 (Overhead transparency).

Let $c$ be a reachable crumble, and let $a\in\{\mathsf{sub}_{\mathit{var}},\mathsf{sub}_{l},\mathsf{sub}_{\mathsf{if}}\}$. If $c\rightarrow_{a}d$ then $c_{\downarrow}=d_{\downarrow}$.

Proof.

Let $c\coloneqq C\langle(b,e_{\!f})\rangle\rightarrow_{a}C\langle(b^{\prime},e_{\!f})\rangle\eqqcolon d$, and let $e^{\prime}_{\!f},e^{\prime\prime}_{\!f}$ be such that $e_{\!f}=e^{\prime}_{\!f}[x{\shortleftarrow}e_{\!f}(x)]e^{\prime\prime}_{\!f}$, noting that $x$ does not occur in $e^{\prime\prime}_{\!f}$ by Lemma E.9.1 and Lemma E.9.2. We first prove that $(b,e_{\!f})_{\downarrow}=(b^{\prime},e_{\!f})_{\downarrow}$:

• •

Case $\mathsf{sub}_{\mathit{var}}$, i.e. $b\coloneqq x$ and $b^{\prime}=e_{\!f}(x)$. By Lemma C.4, $(x,e^{\prime}_{\!f}[x{\shortleftarrow}e_{\!f}(x)]e^{\prime\prime}_{\!f})_{\downarrow}=(x,e^{\prime}_{\!f}e^{\prime\prime}_{\!f})_{\downarrow}\{x{\shortleftarrow}(e_{\!f}(x),e^{\prime\prime}_{\!f})_{\downarrow}\}=(e_{\!f}(x),e^{\prime\prime}_{\!f})_{\downarrow}$ as $c$ is well-named (Lemma E.9.1). By Lemma E.9.2, ${\sf fv}(e_{\!f}(x))\cap\mathsf{dom}(e^{\prime}_{\!f}[x{\shortleftarrow}e_{\!f}(x)])=\emptyset$, therefore $(e_{\!f}(x),e^{\prime\prime}_{\!f})_{\downarrow}=(e_{\!f}(x),e_{\!f})_{\downarrow}$, and we conclude with $(x,e_{\!f})_{\downarrow}=(e_{\!f}(x),e_{\!f})_{\downarrow}$.

• •

Case $\mathsf{sub}_{l}$, i.e. $b\coloneqq xv$ and $b=e_{\!f}(x)\,v$. Since $(xv,e_{\!f})_{\downarrow}=(x,e_{\!f})_{\downarrow}(v,e_{\!f})_{\downarrow}$ (Prop. C.8), we can use the point above to conclude.

• •

Case $\mathsf{sub}_{\mathsf{if}}$, i.e. $b\coloneqq\mathsf{if}\,x\,\mathsf{then}\,c\,\mathsf{else}\,d$ and $b^{\prime}=\mathsf{if}\,e_{v}(x)\,\mathsf{then}\,c\,\mathsf{else}\,d$. Since $(\mathsf{if}\,x\,\mathsf{then}\,c\,\mathsf{else}\,d,e_{v})_{\downarrow}=\mathsf{if}\,(x,e_{v})_{\downarrow}\,\mathsf{then}\,(c\mathrel{@}e_{v})_{\downarrow}\,\mathsf{else}\,(d\mathrel{@}e_{v})_{\downarrow}$ (Prop. C.8), we can use the point above to conclude.

We now prove that $C\langle(b,e_{\!f})\rangle_{\downarrow}=C\langle(b^{\prime},e_{\!f})\rangle_{\downarrow}$ under the hypothesis that $(b,e_{\!f})_{\downarrow}=(b^{\prime},e_{\!f})_{\downarrow}$. By cases on $C$: if $C\coloneqq\langle\cdot\rangle$ just use the hypothesis. Otherwise $C\coloneqq(b^{\prime\prime},e[x{\shortleftarrow}\langle\cdot\rangle])$ and so $(b^{\prime\prime},e[x{\shortleftarrow}b]e_{\!f})_{\downarrow}=(b^{\prime\prime},ee_{\!f})_{\downarrow}\{x{\shortleftarrow}(b,e_{\!f})_{\downarrow}\}=(b^{\prime\prime},ee_{\!f})_{\downarrow}\{x{\shortleftarrow}(b^{\prime},e_{\!f})_{\downarrow}\}\allowbreak=(b^{\prime\prime},e[x{\shortleftarrow}b^{\prime}]e_{\!f})_{\downarrow}$ by Lemma C.4. ∎

Lemma E.12 (Substitution).

Let $t$ and $u$ be terms, $x_{1},\dots,x_{n}$ pairwise distinct variables, and $f_{1},\dots,f_{n}$ be fireballs. If $t\rightarrow_{a}u$ for $a\in\{{\beta_{v}},\textsf{ift},\textsf{iff},\textsf{ife},\textsf{@e}\}$, then $t\{x_{1}{\shortleftarrow}f_{1},\ldots,x_{n}{\shortleftarrow}f_{n}\}\allowbreak\rightarrow_{\mathsf{c}\beta_{\!f}}u\{x_{1}{\shortleftarrow}f_{1},\ldots,x_{n}{\shortleftarrow}f_{n}\}$.

Proof.

Let $\sigma\coloneqq\{x_{1}{\shortleftarrow}f_{1},\ldots,x_{n}{\shortleftarrow}f_{n}\}$. By induction on the definition of $t\rightarrow_{{\beta_{v}}}u$. Cases:

• •

Top level:.

• –

${\beta_{v}}$-step, i.e. $t\coloneqq(\lambda y.{s})v^{\prime}\mapsto_{{\beta_{v}}}s\{y{\shortleftarrow}v^{\prime}\}\eqqcolon u$ and we can suppose without loss of generality that $y\notin\bigcup_{i=1}{\sf fv}(f_{i})\cup\{x_{1},\dots,x_{n}\}$. According to Lemma E.4, $v^{\prime}\sigma$ is a fireball. As a consequence, $t\sigma=\allowbreak(\lambda y.{s\sigma})(v^{\prime}\sigma)\rightarrow_{\beta_{\!f}}s\sigma\{y{\shortleftarrow}v^{\prime}\sigma\}=s\{y{\shortleftarrow}v^{\prime}\}\sigma=u\sigma$.

• –

the $\textsf{ift},\textsf{iff},\textsf{ife},\textsf{@e}$ steps are similar to the ${\beta_{v}}$-step. Lemma E.4 is used in the proof of the ife-step to prove that a ife-redex where the guard is an abstraction is mapped to a ife-redex of the same kind.

• •

Application right, i.e. $t\coloneqq sr\rightarrow_{a}sq\eqqcolon u$ with $r\rightarrow_{a}q$; by i.h. $r\sigma\rightarrow_{\mathsf{c}\beta_{\!f}}q\sigma$, and therefore $t\sigma=s\sigma(r\sigma)\rightarrow_{\mathsf{c}\beta_{\!f}}s\sigma(q\sigma)=u\sigma$.

• •

Application left, i.e. $t\coloneqq sv^{\prime}\rightarrow_{a}rv^{\prime}\eqqcolon u$ with $s\rightarrow_{a}r$; by i.h., $s\sigma\rightarrow_{\mathsf{c}\beta_{\!f}}r\sigma$; according to Lemma E.4, $v^{\prime}\sigma$ is a fireball and hence $t\sigma=s\sigma(v^{\prime}\sigma)\rightarrow_{\mathsf{c}\beta_{\!f}}r\sigma(v^{\prime}\sigma)=u\sigma$.

• •

If-then-else guard, i.e. $t\coloneqq\mathsf{if}\,r\,\mathsf{then}\,s\,\mathsf{else}\,p\rightarrow_{a}\mathsf{if}\,q\,\mathsf{then}\,s\,\mathsf{else}\,p\eqqcolon u$ with $r\rightarrow_{a}q$; by i.h. $r\sigma\rightarrow_{\mathsf{c}\beta_{\!f}}q\sigma$, and therefore $t\sigma=\mathsf{if}\,r\sigma\,\mathsf{then}\,s\sigma\,\mathsf{else}\,p\sigma\rightarrow_{\mathsf{c}\beta_{\!f}}\mathsf{if}\,q\sigma\,\mathsf{then}\,s\sigma\,\mathsf{else}\,p\sigma=u\sigma$. ∎

Lemma E.13 (Substitution of fireballs).

If $e_{\!f}\coloneqq[x_{1}{\shortleftarrow}b_{1}]\ldots[x_{n}{\shortleftarrow}b_{n}]$ is a $f$-environment, then $\sigma(e_{\!f})=\{x_{1}{\shortleftarrow}u_{1},\ldots,x_{n}{\shortleftarrow}u_{n}\}$ where all the $u_{i}$​’s are fireballs.

Proof.

By induction on the length of $e$. If $e_{\!f}\coloneqq\epsilon$, then $\sigma(e_{\!f})=\{\}$ and the statement is vacuously true. Otherwise $e_{\!f}\coloneqq[x{\shortleftarrow}b]e^{\prime}_{\!f}$ with $e^{\prime}_{\!f}\coloneqq[x_{1}{\shortleftarrow}b_{1}]\ldots[x_{n}{\shortleftarrow}b_{n}]$ and then $\sigma(e_{\!f})=\{x{\shortleftarrow}(b,e^{\prime}_{\!f})_{\downarrow}\}\cup\sigma(e^{\prime}_{\!f})$; by i.h. (since $e^{\prime}_{\!f}$ is a $f$-environment), $\sigma(e^{\prime}_{\!f})=\{x_{1}{\shortleftarrow}u_{1},\ldots,x_{n}{\shortleftarrow}u_{n}\}$ where all the $u_{i}$​’s are fireballs; also $(b,e^{\prime}_{\!f})_{\downarrow}$ is a fireball by definition of $f$-environment, as $e_{\!f}=E\langle(b,e^{\prime})\rangle$ with $E\coloneqq[x{\shortleftarrow}\langle\cdot\rangle]$; therefore, $\sigma(e_{\!f})=\{x{\shortleftarrow}(b,e^{\prime}_{\!f})_{\downarrow},x_{1}{\shortleftarrow}u_{1},\dots,x_{n}{\shortleftarrow}u_{n}\}$ satisfies the statement. ∎

Lemma E.14 (Read-back vs. append).

For any crumble $c$ and $f$-environment $e_{\!f}$, $(c\mathrel{@}e_{\!f})_{\downarrow}=c_{\downarrow}\sigma(e_{\!f})$.

Proof.

By induction on the length of $e_{\!f}$. If $e_{\!f}\coloneqq\epsilon$ then $\sigma(e_{\!f})=\{\}$ and hence $(c\mathrel{@}e_{\!f})_{\downarrow}=c_{\downarrow}=c_{\downarrow}\{\}=c_{\downarrow}\sigma(e_{\!f})$. Otherwise $e_{\!f}\coloneqq[x{\shortleftarrow}b]e^{\prime}_{\!f}$ where $x\notin\mathsf{dom}(e^{\prime}_{\!f})$; by i.h. (since $e^{\prime}_{\!f}$ is a fireball environment), $((c\mathrel{@}[x{\shortleftarrow}b])\mathrel{@}e^{\prime}_{\!f})_{\downarrow}=(c\mathrel{@}[x{\shortleftarrow}b])_{\downarrow}\sigma(e^{\prime}_{\!f})$ and $(b,e^{\prime}_{\!f})_{\downarrow}=((b,\epsilon)\mathrel{@}e^{\prime}_{\!f})_{\downarrow}=(b,\epsilon)_{\downarrow}\sigma(e^{\prime}_{\!f})=b_{\downarrow}\sigma(e^{\prime}_{\!f})$; by the definitions of append and read-back, $(c\mathrel{@}[x{\shortleftarrow}b])_{\downarrow}=c_{\downarrow}\{x{\shortleftarrow}b_{\downarrow}\}$; therefore, $(c\mathrel{@}e_{\!f})_{\downarrow}=((c\mathrel{@}[x{\shortleftarrow}b])\mathrel{@}e^{\prime}_{\!f})_{\downarrow}=(c\mathrel{@}[x{\shortleftarrow}b])_{\downarrow}\sigma(e^{\prime}_{\!f})=(c_{\downarrow}\{x{\shortleftarrow}b_{\downarrow}\})\sigma(e^{\prime}_{\!f})=c_{\downarrow}(\{x{\shortleftarrow}b_{\downarrow}\sigma(e^{\prime}_{\!f})\}\cup\sigma(e^{\prime}_{\!f}))=c_{\downarrow}\{x{\shortleftarrow}(b,e^{\prime}_{\!f})_{\downarrow}\}\cup\sigma(e^{\prime}_{\!f})=c_{\downarrow}\sigma(e_{\!f})$. ∎

Lemma E.15.

If $c_{\downarrow}\rightarrow_{a}d_{\downarrow}$ for $a\in\{{\beta_{v}},\textsf{ift},\textsf{iff},\textsf{ife},\textsf{@e}\}$, then $(c\mathrel{@}e_{\!f})_{\downarrow}\rightarrow_{\beta_{\!f}}{}(d\mathrel{@}e_{\!f})_{\downarrow}$.

Proof.

According to Lemma E.13, $\sigma(e_{\!f})=\{x_{1}{\shortleftarrow}f_{1},\ldots,x_{n}{\shortleftarrow}f_{n}\}$ where $f_{1},\dots,f_{n}$ are fireballs. By Lemma E.14 and Lemma E.12, $(c\mathrel{@}e_{\!f})_{\downarrow}=c_{\downarrow}\sigma(e_{\!f})\rightarrow_{\beta_{\!f}}d_{\downarrow}\sigma(e_{\!f})=(d\mathrel{@}e_{\!f})_{\downarrow}$ ∎

Note that Lemma E.15 does not hold if we let $\rightarrow_{a}$ be $\rightarrow_{\beta_{i}}$ in the hypothesis. Indeed, take $c\coloneqq((\lambda x.{(x,\epsilon)})y,[y{\shortleftarrow}(zz,\epsilon)])$ and $d\coloneqq(y,[y{\shortleftarrow}zz])$ and $e_{\!f}\coloneqq[z{\shortleftarrow}\lambda x.{(xx,\epsilon)}]$: then, $c_{\downarrow}=(\lambda x.x)(zz)\rightarrow_{\beta_{i}}zz=d_{\downarrow}$ but $(c\mathrel{@}e_{\!f})_{\downarrow}=(\lambda x.x)((\lambda x.xx)\lambda x.xx)\not\rightarrow_{\beta_{\!f}}(\lambda x.xx)\lambda x.xx=(d\mathrel{@}e_{\!f})_{\downarrow}$. The problem is essentially due to the fact that fireballs, contrary to values, are not closed by substitution: this a notable difference between the closed case (where the normal forms coincide with closed values) and the open case (where the normal forms coincide with fireballs).

Proposition E.16 (Principal projection).

Let $c$ be a reachable crumble. If $c\rightarrow_{a}d$ for $a\in\{\beta_{\!f},\textsf{ift},\textsf{iff},\textsf{ife},\textsf{@e}\}$ then $c_{\downarrow}\rightarrow_{a}d_{\downarrow}$.

Proof.

Note that for every $b,e_{v}$, $(b,e_{v})=(b,\epsilon)\mathrel{@}e_{v}$. Therefore all steps can be written in the form $C\langle(b,e_{v})\rangle\rightarrow_{a}C\langle c\mathrel{@}e_{v}\rangle$ where $b$ is not a crumbled value. The crumble context $C$ unfolds to a right v-context by Lemma E.9.4. We need to prove that $C\langle(b,e_{v})\rangle_{\downarrow}\rightarrow_{a}(C\langle c\mathrel{@}e_{v}\rangle)_{\downarrow}$. By Lemma C.10 and Lemma E.15, it suffices to prove that $C\langle(b,\epsilon)\rangle_{\downarrow}\rightarrow_{b}C\langle c\rangle_{\downarrow}$ for all $a\neq\beta_{\!f}$ and $b=a$ or for $a=\beta_{\!f}$ and $b={\beta_{v}}$.

We proceed by cases on the rule $\rightarrow_{a}$.

• •

Rule $\beta_{\!f}$: we need to prove that $C\langle((\lambda x.c)\,v,\epsilon)\rangle_{\downarrow}\rightarrow_{{\beta_{v}}}{}C\langle e\mathrel{@}[y{\shortleftarrow}v]\rangle_{\downarrow}$ where $e\mathrel{@}[y{\shortleftarrow}v]\coloneqq(c\mathrel{@}[x{\shortleftarrow}v])^{\alpha}$.

[TABLE]

Note that the second use of Corollary C.11.1 requires that $C\mathrel{\#}(e\mathrel{@}[y{\shortleftarrow}v])$ i.e. that ${\sf fv}(C)\cap\mathsf{dom}(e\mathrel{@}[y{\shortleftarrow}v])=\emptyset$, which follows from the side condition about $\alpha$-renaming in the $\beta_{\!f}$ rule.

• •

Rules $\textsf{ift},\textsf{iff},\textsf{ife},\textsf{@e}$: a quick check by cases over $(b,e_{v})\mapsto_{a}c\mathrel{@}e_{v}$ shows that $b_{\downarrow}\rightarrow_{a}c_{\downarrow}$.

For example, $(\mathsf{if}\,\mathsf{true}\,\mathsf{then}\,c\,\mathsf{else}\,d,e_{v})\mapsto_{\textsf{ift}}c\mathrel{@}e_{v}$ and

$(\mathsf{if}\,\mathsf{true}\,\mathsf{then}\,c\,\mathsf{else}\,d)_{\downarrow}=\mathsf{if}\,\mathsf{true}\,\mathsf{then}\,c_{\downarrow}\,\mathsf{else}\,d_{\downarrow}\rightarrow_{\textsf{ift}}c_{\downarrow}$. The other cases are all similar.

Thus

[TABLE]

Note that the second use of Corollary C.11.1 requires that $C\mathrel{\#}c$. The property holds because all substitutions outside abstractions in the rhs of the rules $\rightarrow_{a}$ under consideration were such in the lhs, and because reachable crumbles are well-named (Lemma E.9.1). ∎

Lemma E.17 (Halt).

If $c$ is $\mathsf{oCr}$-normal then $c_{\downarrow}$ is $\rightarrow_{\mathsf{c}\beta_{\!f}}$-normal.

Proof.

By Prop. 6.3, if $c$ is normal then it is a $f$-crumble i.e. $c=c_{\!f}$. By definition of $c_{\!f}$, $c_{\downarrow}$ is a fireball. By harmony for $\lambda_{\mathsf{fire}}^{\mathsf{if}}$, $c_{\downarrow}$ is $\mathsf{c}\beta_{\!f}$-normal. ∎

Proof of 0 (Thm. 6.5).

“??”

Proof.

1. (1)

See Prop. 4.2. 2. (2)

See Prop. E.16. 3. (3)

See Prop. E.11. 4. (4)

See Lemma E.10. 5. (5)

See Lemma E.17. 6. (6)

Immediate consequence of the equivalent of Lemma 5.8 for the Open Crumble GLAM. ∎

E.3. The Open Pointed Crumble GLAM

The design of a machine, called Open Pointed Crumble GLAM, for the open case that decomposes the search for the next redex and (un)plugging in $O(1)$ transitions follows the same pattern as for the Pointed Crumble GLAM in Appendix D.4 (p. D.4) for the closed case. In particular, the definitions of pointed environment, translation $\iota(\cdot)$ (from crumbles to pointed environments) and read-back $(\cdot)_{\Downarrow}$ (from pointed environments to crumbles) are the same. The transitions of the Open Pointed Crumble GLAM (whose union is noted $\rightarrow_{\mathsf{poCr}}$) differ from the ones of the Pointed Crumble GLAM exactly as the transitions of Open Crumble GLAM differ from the ones of the Crumble GLAM.

E.3.1. Implementation.

Pointed environments.

For the Open Pointed Crumble GLAM, the definitions of pointed environment, translation $\iota(\cdot)$ (from crumbles to pointed environments) and read-back $(\cdot)_{\Downarrow}$ (from pointed environments to crumbles) are the same as for the Pointed Crumble GLAM, see Appendix D.4 (p. D.4).

Evaluation.

The transition rules of the Open Pointed Crumble GLAM are:

[TABLE]

where

1. i.

$\lambda z.{(b,e^{\prime})}\coloneqq(\lambda y.c)^{\alpha}$ such that $(e[x{\shortleftarrow}b]e^{\prime}[z{\shortleftarrow}v]\mathrel{\!\textnormal{{¦}}\!}e_{\!f})$ is well-named. 2. ii.

where $c\eqqcolon(b,e^{\prime})$ 3. iii.

where $d\eqqcolon(b,e^{\prime})$ 4. iv.

if $v=\lambda x.e$ or $v=\mathsf{err}$. 5. v.

if $v\in\{\mathsf{true},\mathsf{false},\mathsf{err}\}$. 6. vi.

if $x\in\mathsf{dom}(e_{\!f})$. 7. vii.

if none of the other rules is applicable, i.e. when $b$ is a practical value $v_{\neg x}$ or when $b$ is $x$, $xv$, or $\mathsf{if}\,x\,\mathsf{then}\,c\,\mathsf{else}\,d$ but $x$ is not defined in $e_{\!f}$.

The transition function $\rightarrow_{\mathsf{poCr}}$ of the Open Pointed Crumble GLAM is then defined as the union of the rules above. A principal transition of the Open Pointed Crumble GLAM is a transition $\rightarrow_{a}$ for any rule $a\in\{\beta_{\!f},\textsf{ift},\textsf{iff},\textsf{ife},\textsf{@e}\}$.

Definition E.18 (Reachable state).

A pointed environment is said to be reachable (in the Open Pointed Crumble GLAM) if it is obtained from evaluation steps starting from the translation $\iota(c)$ of a well-named crumble $c$.

Lemma E.19 (Invariants).

Let $e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}$ be a reachable pointed environment:

1. (1)

Freshness:* $e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}$ is well-named;* 2. (2)

Rightmost:* $e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}=(e\mathrel{\!\textnormal{{¦}}\!}e_{\!f})$ for some $e$ and some $f$-environment $e_{\!f}$.*

Proof.

By induction on the length of the evaluation sequence leading to $e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}$. The base cases hold by the definition of reachability and by the definition of $\iota(\cdot)$. As for the inductive step, we proceed by cases on the transitions:

1. (1)

For $\beta_{\!f}$ the claim follows from the side condition. The rules in $\{\textsf{ift},\textsf{iff},\textsf{ife},\textsf{@e},\mathsf{sea}\}$ do not increase the number of explicit substitutions occuring in $e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}$ outside of abstractions, hence the claim follows from the i.h.. The rules in $\{\mathsf{sub}_{\mathit{var}},\mathsf{sub}_{l},\mathsf{sub}_{\mathsf{if}}\}$ copy a practical value from the environment $e_{\!f}$: note that $e_{\!f}(x)$ is either an abstraction (which does not influence well-namedness) or a boolean or an error (which do not contain explicit substitutions). 2. (2)

The rules in $\{\beta_{\!f},\textsf{ift},\textsf{iff},\textsf{ife},\textsf{@e},\mathsf{sub}_{\mathit{var}},\mathsf{sub}_{l},\mathsf{sub}_{\mathsf{if}}\}$ do not change the evaluated part, hence the claim follows from the i.h.. As for the $\mathsf{sea}$ rule, by Lemma E.21 it suffices to prove that $(b,e_{\!f})$ is a $f$-crumble, knowing that the other transition rules cannot be applied: this follows from Lemma E.7. ∎

Lemma E.20 (Harmony for the Open Pointed Crumble GLAM).

Let $e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}$ be a reachable pointed environment in the Open Pointed Crumble GLAM: $e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}$ is normal if and only if it has the form $(\epsilon\mathrel{\!\textnormal{{¦}}\!}e_{\!f})$ for some non-empty $f$-environment $e_{\!f}$.

Proof.

The proof of the implication from right to left is trivial. As for the other direction, let $e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}$ be a reachable normal pointed environment. By Lemma E.19, $e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}$ has the form $(e\mathrel{\!\textnormal{{¦}}\!}e_{\!f})$. Note that $e$ must be empty; otherwise one of the transitions in $\{\beta_{\!f},\textsf{ift},\textsf{iff},\textsf{ife},\textsf{@e},\mathsf{sub}_{\mathit{var}},\mathsf{sub}_{l},\mathsf{sub}_{\mathsf{if}},\mathsf{sea}\}$ could be applied, contradicting the hypothesis that $e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}$ is normal. ∎

Lemma E.21.

If $[x{\shortleftarrow}b]e$ is a $f$-environment, then $(b,e)$ is a $f$-crumble.

Proof.

Assume that $[x{\shortleftarrow}b]e$ is a $f$-environment, and let $(b,e)=C\langle(b^{\prime},e^{\prime})\rangle$ for some $C,b^{\prime},e^{\prime}$. Then $[x{\shortleftarrow}b]e=E\langle C\langle b^{\prime},e^{\prime}\rangle\rangle$ for $E\coloneqq[x{\shortleftarrow}\langle\cdot\rangle]$. The requirements for a $f$-crumble follow from the definition of $f$-environment for $[x{\shortleftarrow}b]e$. ∎

Theorem E.22 (Implementation).

Let $e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}$ a pointed environment that is reachable by the Open Pointed Crumble GLAM.

1. (1)

Initialization: ** $(\iota(c))_{\Downarrow}=c$ for every crumble $c$. 2. (2)

Principal Projection: ** if $e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}\to_{a}e^{\prime}_{{\,\mathrel{\!\textnormal{{¦}}\!}}}$ then $(e_{{\,\mathrel{\!\textnormal{{¦}}\!}}})_{\Downarrow}\to_{a}(e^{\prime}_{{\,\mathrel{\!\textnormal{{¦}}\!}}})_{\Downarrow}$ for any rule $a\neq\mathsf{sea}$. 3. (3)

Overhead Transparency: ** if $e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}\rightarrow_{\mathsf{sea}}e^{\prime}_{{\,\mathrel{\!\textnormal{{¦}}\!}}}$, then $(e_{{\,\mathrel{\!\textnormal{{¦}}\!}}})_{\Downarrow}=(e^{\prime}_{{\,\mathrel{\!\textnormal{{¦}}\!}}})_{\Downarrow}$. 4. (4)

Determinism: ** the transition function $\rightarrow_{\mathsf{poCr}}$ is deterministic. 5. (5)

Halt: ** if $e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}$ is normal, then $(e_{{\,\mathrel{\!\textnormal{{¦}}\!}}})_{\Downarrow}$ is normal. 6. (6)

Overhead Termination: ** $\rightarrow_{\mathsf{sea}}$ terminates.

Therefore, the Open Pointed Crumble GLAM (with its transition function $\rightarrow_{\mathsf{poCr}}$), the Open Crumble GLAM (with $\rightarrow_{\mathsf{oCr}}$), and the read-back $(\cdot)_{\Downarrow}$ form an implementation system.

Proof.

1. (1)

Let $c=(b,e)$: by the definitions, $(\iota(c))_{\Downarrow}=([x{\shortleftarrow}b]e\mathrel{\!\textnormal{{¦}}\!}\epsilon)_{\Downarrow}=(b,e\epsilon)=c$. 2. (2)

There is a clear one-to-one correspondence between the transitions of the Open Pointed Crumble GLAM and the Open Crumble GLAM (apart from $\mathsf{sea}$). The proof is similar to the one of Thm. D.15. 3. (3)

By inspection of the rule $\mathsf{sea}$. We need to prove that $(e[x{\shortleftarrow}b]\mathrel{\!\textnormal{{¦}}\!}e_{\!f})_{\Downarrow}=(e\mathrel{\!\textnormal{{¦}}\!}[x{\shortleftarrow}b]e_{\!f})_{\Downarrow}$. By cases on the structure of $e$: if $e=\epsilon$, then $(\epsilon[x{\shortleftarrow}b]\mathrel{\!\textnormal{{¦}}\!}e_{\!f})_{\Downarrow}=(b,e_{\!f})=(\epsilon\mathrel{\!\textnormal{{¦}}\!}[x{\shortleftarrow}b]e_{\!f})_{\Downarrow}$. If instead $e=[y{\shortleftarrow}b^{\prime}]e^{\prime}$, then $(e[x{\shortleftarrow}b]\mathrel{\!\textnormal{{¦}}\!}e_{\!f})_{\Downarrow}=(b^{\prime},e^{\prime}[x{\shortleftarrow}b]e_{\!f})=(e\mathrel{\!\textnormal{{¦}}\!}[x{\shortleftarrow}b]e_{\!f})_{\Downarrow}$. 4. (4)

The rule $\mathsf{sea}$ can be applied by definition only when the other rules cannot be applied. The remaining rules apply to a pointed environment of the form $(e[x{\shortleftarrow}b]\mathrel{\!\textnormal{{¦}}\!}e_{\!f})$, for distinct shapes of $b$:

• •

The rules $\{\beta_{\!f},\textsf{@e},\mathsf{sub}_{l}\}$ apply when $b$ is an application, and respectively the application of an abstraction to a crumbled value, of a boolean/error to a crumbled value, and of a variable to a crumbled value.

• •

The rule $\mathsf{sub}_{\mathit{var}}$ applies when $b$ is a variable.

• •

The rules in $\{\textsf{ift},\textsf{iff},\textsf{ife},\mathsf{sub}_{\mathsf{if}}\}$ apply when $b$ is a $\mathsf{if}\mbox{-}\mathsf{then}\mbox{-}\mathsf{else}$, and in clearly disjoint cases according to the structure of the condition: respectively, when the condition is $\mathsf{true}$, $\mathsf{false}$, an abstraction or an error, and a variable.

• •

Finally, note that no single rule in $\{\mathsf{sub}_{\mathit{var}},\mathsf{sub}_{l},\mathsf{sub}_{\mathsf{if}}\}$ can transition to different pointed environments due to the lookup of a variable which has multiple occurrences in the environment: the lookup is deterministic because the environment is well-named (Lemma E.19.1). 5. (5)

By Lemma E.20, $e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}$ is normal iff it has the form $(\epsilon\mathrel{\!\textnormal{{¦}}\!}e_{\!f})$ for some non-empty $f$-environment $e_{\!f}$. Then $(e_{{\,\mathrel{\!\textnormal{{¦}}\!}}})_{\Downarrow}=(\epsilon\mathrel{\!\textnormal{{¦}}\!}e_{\!f})_{\Downarrow}$ which is a $f$-crumble by Lemma E.21. By Prop. 6.3, $(e_{{\,\mathrel{\!\textnormal{{¦}}\!}}})_{\Downarrow}$ is normal. 6. (6)

Immediate consequence of forthcoming Cor. E.24 (proved independently). ∎

E.3.2. Complexity

The complexity analysis for the Open Pointed Crumble GLAM is analogue to the one for the Pointed Crumble GLAM. More precisely, following the same approach and notations as in Section D.4 and in Section D.5, we can prove:

Lemma E.23 (Number of $\mathsf{sea}$-transitions).

Let $c$ be a well-named crumble, and let $\rho\colon\iota(c)\rightarrow_{\mathsf{poCr}}^{*}e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}=(e\mathrel{\!\textnormal{{¦}}\!}e_{v})$ an execution in the Open Pointed Crumble GLAM. Then $|e|_{\textup{len}}\leq|c|_{\textup{len}}+(|\rho|_{\beta_{\!f}}+|\rho|_{\textsf{ift}}+|\rho|_{\textsf{iff}})\cdot L(c)-|\rho|_{\mathsf{sea}}$.

Corollary E.24.

Let $t$ be a term. For a normalizing execution $\rho$ in the Open Pointed Crumble GLAM starting from $\iota(\underline{t})$, we have $|\rho|_{\mathsf{sea}}\leq(|\rho|_{{\mathsf{p}}}+1)\cdot|t|$.

Theorem E.25 (The Open Pointed Crumble GLAM is bilinear).

For any term $t$ and any Open Pointed Crumble GLAM execution $\rho\colon\iota(\underline{t})\rightarrow_{\mathsf{poCr}}^{*}e_{{\,\mathrel{\!\textnormal{{¦}}\!}}}$, the cost of implementing $\rho$ on a RAM is $O((|\rho|_{{\mathsf{p}}}+1)\cdot|t|)$.

Proof.

Essentially the same proof as the one of Thm. D.18. ∎

Analogously to the closed case, the previous theorem also has a consequence for the non-pointed case. Since the theorem shows that the cost of searching for redexes and the (un)plugging operations can indeed be realised in bilinear time, it is also true that the Open Crumble GLAM can be implemented in bilinear time, improving Thm. 6.6 by removing the up to search and (un)plugging side condition.

Corollary E.26 (The Open Crumble GLAM is bilinear).

For any term $t$ and any Open Crumble GLAM execution $\rho\colon\underline{t}\rightarrow_{\mathsf{oCr}}^{*}c$, the cost of implementing $\rho$ on a RAM is $O((|\rho|_{{\mathsf{p}}}+1)\cdot|t|)$.

Appendix F Implementation in OCaml

The goal of this section is implementing in OCaml the Pointed Crumble GLAM and Open Pointed Crumble GLAM presented in Appendix D.4 (p. D.4) and Appendix E.3 (p. E.3). We are going to describe the abstract requirements of the data structures, before picking a concrete implementation. The two machines share the same data structures and auxiliary functions, and only differ by five lines of code.

Data structures.

The machine works on pointed environments of the form $(e\mathrel{\!\textnormal{{¦}}\!}e_{v})$. The unevaluated part of the environment $e$ and the evaluated part $e_{v}$ are subject to different requirements:

• •

The unevaluated part $e$ is extended only on the right by the transitions ${\beta_{v}},\textsf{ift},\textsf{iff}$ by concatenating an unevaluated environment. Only the rightmost entry is inspected by every reduction rule. The $\mathsf{sea}$ transition removes the rightmost entry, moving it to the evaluated part. Therefore the unevaluated environment must implement the catenable stack interface, allowing to perform catenation, pop, and topmost inspection in constant time.

• •

As for the evaluated part $e_{v}$, transitions never exploit the sequential structure of $e_{v}$. On the contrary, the $\mathsf{sub}_{\mathit{var}},\mathsf{sub}_{l},\mathsf{sub}_{\mathsf{if}}$ transitions need to access the entry associated with a variable $x$ in constant time. The only other operation required (by the $\mathsf{sea}$ rule) is to add an entry to it in constant time.

To satisfy lookup in constant time for $e_{v}$, we implement $e_{v}$ as a store, thus ignoring its list structure. In turn, this choice impacts on the data structure for terms, because it forces (occurrences of) variables to be implemented as pointers to memory locations. More explicitly, an entry $[x{\shortleftarrow}b]$ is represented as a node $n$ which is a record containing a field content holding $b$ together with additional fields soon to be described. If $\alpha$ is the address of $n$, occurrences of $x$ are represented in OCaml as $\mathtt{Shared}(n)$, which means a memory cell tagged as Shared and holding the pointer $\alpha$.

Occurrences of $\lambda$-bound variables are instead presented as $\texttt{Var}(v)$ where $v$ is a unique identifier for that variable. Thus the data structure for terms is:

⬇

...

and term =

| Err

| True

| False

| Var of var

| Lam of var * crumblep

| App of term * term

| IfThenElse of term * crumblep * crumblep

| Shared of node

...

A crumble is a term coupled with an unevaluated environment. As discussed above, the unevaluated environment implements a catenable stack interface. The simplest implementation, which we adopted, is a linked list of nodes, referenced by two pointers to the first and the last entries of the stack, or a special value to represent the empty stack. Concretely, in OCaml we use an option type for that.

⬇

...

and env = (node * node) option

and crumblep = term * env

...

Each node has a field prev used to point to the previous entry in the environment. An additional field copying and mutability of all fields are required to implement $\alpha$-renaming in linear time; we explain their use later. Therefore a node is:

⬇

type node =

{ mutable content : term

; mutable copying : bool

; mutable prev : node option }

...

Unreachable nodes can be garbage-collected by the runtime of OCaml. Because the evaluator holds a pointer to the unevaluated environment, only evaluated nodes can be garbage-collected.

Finally, we implement the datatype of unique $\lambda$-bound variable identifiers var as the address of an OCaml record that holds no useful information. Thus comparing variables can be achieved using pointer equality ==. Concrete implementations can add fields to the record, for example to associate the name of the variable as a string.

⬇

type var = {dummy: unit} (no empty records in OCaml)

A summary of the data structures can be found in Table 1.

Implementation of transitions.

The code that implements evaluation in the closed and open cases can be found in Table 4. For the same reason as it is discussed in Appendix D.4 (p. D.4), the input of the evaluation functions eval_c/eval_o is not a crumble, but a crumbled unevaluated environment $\iota(b,e)=[x{\shortleftarrow}b]e$ where $x$ is a fresh variable. More precisely, the evaluation functions take in input just a node n, which is the rightmost entry of the crumbled unevaluated environment that has to be evaluated.

The code that implements the transition ${\beta_{v}}$ for $(\lambda y.c)v$ is the most complex because it must:

1. (1)

$\alpha$-rename $\lambda y.c$ to $\lambda y^{\prime}.{(b^{\prime},e^{\prime})}$; 2. (2)

change the top of the unevaluated environment (stack) from $[\texttt{n}{\shortleftarrow}(\lambda y.c)v]$ to $[\texttt{n}{\shortleftarrow}b^{\prime}]$ and append $e^{\prime}$ to it; 3. (3)

push $[y^{\prime}{\shortleftarrow}v]$ on top of the unevaluated environment.

To implement the previous steps efficiently, the code creates the node $y^{\prime}$ containing $v$ and then calls a function copy_crumbp $y\,y^{\prime}\,c$ that performs step 1 in linear time, returning the new unevaluated crumble $c^{\prime}$. Then $n\mathrel{@}c^{\prime}$ performs step 2 in constant time by concatenating $c^{\prime}$ to the unevaluated environment (and therefore to $n$, its topmost element). The code of $\_\_\mathrel{@}$ is given in Table 2.

Finally, push $y^{\prime}\,(n\mathrel{@}c^{\prime})$ performs step 3 in constant time by pushing $y^{\prime}$ on the new top of the unevaluated environment.

The transitions $\mathsf{sub}_{l},\mathsf{sub}_{\mathit{var}},\mathsf{sub}_{\mathsf{if}},\textsf{@e},\textsf{ife}$ rules just update the content of the top of the unevaluated environment in the required way.

The transitions ift and iff perform in constant time the plugging of the crumble $c$ to the unevaluted environment, then call the evaluation function on the new topmost entry of the unevaluated environment.

The transition $\mathsf{sea}$ is implemented by the function pop that pops the top of the unevaluated environment and calls evaluation on the new top (if present):

⬇

...

and pop n =

match n.prev with

| None -> n.content

| Some p ->

n.prev <- None;

eval_c/o p

...

When a node is popped, its prev pointer is unset to facilitate garbage-collection of unreferenced nodes.

Otherwise a normal form is reached, and evaluation returns the term that, pointing to the evaluated environment, consists of the normal crumble.

Let us remark that the implementation is tail-recursive444when the pop function is inlined; since OCaml optimizes tail-recursion, the machine only consumes constant space on the process execution stack.

As a minor optimization to the expected code, our implementation merges execution of rule $\mathsf{sub}_{\mathit{var}}$ with that of the $\mathsf{sea}$ step which always follows the former. The merging is obtained calling pop in place of eval_c/eval_o.

The complexity of each case is $O(1)$, but for the ${\beta_{v}}$ rule which requires a renaming of crumble (copy_crumbp). It remains to see how this operation can be implemented with linear complexity.

Implementation of $\alpha$-renaming.

We implement $\alpha$-renaming of unevaluated environments by creating a copy of the environment. The representation in memory of the environment is a DAG because terms in the nodes of the environment contain occurrences of Shared nodes defined in the same environment. Therefore we need to implement a copy algorithm over DAGs that runs in linear time.

The algorithm consists in using the content field of nodes to perform the renaming. When a node is being copied, it is temporarily put in the copying=true status, and its content field is changed to point to the corresponding new node. Then, the rest of the environment is copied recursively. When an occurrence of a node that is being copied is found in the term being copied, it is replaced with the new node stored in the content field of the old one. Finally, when the copy is over, the copying status of every node is reset to false and the previous value of content is restored, yielding the original environment.

The auxiliary copying_node y y’ f function, where y is the node to be copied to y’, implements the idea above by temporarily putting y in copying=true status, until f is executed.

⬇

let copying_node y y’ f =

let saved = y.content in

y.content <- Shared y’ ;

y.copying <- true ;

let res = f () in

y.content <- saved ;

y.copying <- false ;

res

The copy_crumbp v n p function (Table 2) not only implements the algorithm above by copying p, but it also replaces occurrences of Var v (the bound variable in a $\rightarrow_{{\beta_{v}}}$ redex) with Shared n (the new node pointing to the argument of the redex), i.e.: let $c\coloneqq b_{0},[x_{1}{\shortleftarrow}b_{1}]\ldots[x_{k}{\shortleftarrow}b_{k}]$; then copy_crumbp v n p $=b_{0}^{\prime},[y_{1}^{\prime}{\shortleftarrow}b_{1}^{\prime}]\ldots[y_{k}^{\prime}{\shortleftarrow}b_{k}^{\prime}]$, where $b_{i}^{\prime}\coloneqq b_{i}\{v{\shortleftarrow}n\}\{x_{i+1}{\shortleftarrow}x_{i+1}^{\prime}\}\ldots\{x_{k}{\shortleftarrow}x_{k}^{\prime}\}$.

The implementation of copy_crumbp v n p uses an auxiliary function copy_env that iterates over the environment copying it. The function copy copies a bite.

Crumbling.

The code in Table 3 takes an unevaluated environment and returns the corresponding crumbled unevaluated environment. It generalizes the function $\underline{\cdot}$ in the paper that turns terms into crumbles. It mainly consists of three mutually recursive functions:

1. (1)

aux_term c e translates c to $d=(b^{\prime},e^{\prime})$, appends $e^{\prime}$ to e and returns the obtained crumble. 2. (2)

aux_value c e checks whether c is a value, computing either $\overline{\cdot}$, or $\underline{\cdot}$ by calling aux_term c e. 3. (3)

aux_env c e creates a copy of (c, e) in crumbled form in linear time reusing the same trick of the copying flag as in $\alpha$-renaming.