Beniamino Accattoli
email: beniamino.accattoli@inria.fr

Claudio Sacerdoti Coen

On the Relative Usefulness of Fireballs

showed that there is an implementation of the ordinary (i.e. strong, pure, call-by-name) λ-calculus into models like RAM machines which is polynomial in the number of β-steps, answering a long-standing question. The key ingredient was the use of a calculus with useful sharing, a new notion whose complexity was shown to be polynomial, but whose implementation was not explored. This paper, meant to be complementary, studies useful sharing in a call-by-value scenario and from a practical point of view. We introduce the Fireball Calculus, a natural extension of call-by-value to open terms, that is an intermediary step towards the strong case, and we present three results. First, we adapt useful sharing, refining the meta-theory. Then, we introduce the GLAMOUr, a simple abstract machine implementing the Fireball Calculus extended with useful sharing. Its key feature is that usefulness of a step is tested-surprisingly-in constant time. Third, we provide a further optimisation that leads to an implementation having only a linear overhead with respect to the number of β-steps.

I. INTRODUCTION

The λ-calculus is an interesting computational model because it is machine-independent, simple to define, and it compactly models functional programming languages. Its definition has only one rule, the β rule, and no data structures. The catch is the fact that the β-rule-which by itself is Turingcomplete-is not atomic. Its action, namely (λx.t)u → β t{x u}, can make many copies of an arbitrarily big subprogram u. In other computational models like Turing or RAM machines, an atomic operation can only move the head on the ribbon or access a register. Is β atomic in that sense? Can one count the number of β-steps to the result and then claim that it is a reasonable bound on the complexity of the term? Intuition says no, because β can be nasty, and make the program grow at an exponential rate. This is the size explosion problem.

Useful Sharing: nonetheless, it is possible to take the number of β-steps as an invariant cost model, i.e. as a complexity measure polynomially related to RAM or Turing machines. While this was known for some notable sub-calculi [START_REF] Blelloch | Parallelism in sequential functional languages[END_REF]- [START_REF] Accattoli | On the invariance of the unitary cost model for head reduction[END_REF], the first proof for the general case is a recent result by Accattoli and Dal Lago [START_REF] Accattoli | Beta Reduction is Invariant, Indeed[END_REF]. Similarly to the literature, they circumvent size explosion by factoring the problem via an intermediary model in between λ-calculus and machines. Their model is the linear substitution calculus (LSC) [START_REF] Accattoli | Beta Reduction is Invariant, Indeed[END_REF], [START_REF] Accattoli | A nonstandard standardization theorem[END_REF], that is a simple λ-calculus with sharing annotations (also known as explicit substitutions) where the substitution process is decomposed in micro steps, replacing one occurrence at a time. In contrast with the literature, the general case is affected by a stronger form of size explosion, requiring an additional and sophisticated layer of sharing, called useful sharing. Roughly, a micro substitution step is useful if it contributes somehow to the creation of a β-redex, and useless otherwise. Useful reduction then selects only useful substitution steps, avoiding the useless ones. In [START_REF] Accattoli | Beta Reduction is Invariant, Indeed[END_REF], the Useful LSC is shown to be polynomially related to both λ-calculus (in a quadratic way) and RAM machines (with polynomial overhead, conjectured linear). It therefore follows that there is a polynomial relationship λ → RAM. Pictorially: Coming back to our questions, the answer of [START_REF] Accattoli | Beta Reduction is Invariant, Indeed[END_REF] is yes, β is atomic, up to a polynomial overhead. It is natural to wonder how big this overhead is. Is β reasonably atomic? Or is the degree of the polynomial big and does the invariance result only have a theoretical value? In particular, in [START_REF] Accattoli | Beta Reduction is Invariant, Indeed[END_REF] the definition of useful steps relies on a separate and global test for usefulness, that despite being tractable might not be feasible in practice. Is there an efficient way to implement the Useful LSC? Does useful sharing-i.e. the avoidance of useless duplications-bring a costly overhead? This paper answers these questions. But, in order to stress the practical value of the study, it shifts to a slightly different setting.

The Fireball Calculus: we recast the problem in terms of the new fireball calculus (FBC), essentially the weak callby-value λ-calculus generalised to handle open terms. It is an intermediary step towards a strong call-by-value λ-calculus, that can be seen as iterated open weak evaluation. A similar approach to strong evaluation is followed also by Grégoire and Leroy in [START_REF] Grégoire | A compiled implementation of strong reduction[END_REF]. It avoids some of the complications of the strong case, and at the same time exposes all the subtleties of dealing with open terms.

Free variables are actually formalised using a distinguished syntactic class, that of symbols, noted a, b, c. This approach is technically convenient because it allows restricting to closed terms, so that any variable occurrence x is bound, while still having free variables, represented as symbols.

The basic idea is that-in the presence of symbolsrestricting β-redex to fire only in presence of values is problematic. Consider indeed the following term: t := ((λx.λy.u)(aa))w where w is normal. For the usual call-by-value operational semantics t is normal (because aa is not a value) while for theoretical reasons (see [START_REF] Paolini | Call-by-value solvability[END_REF]- [START_REF] Carraro | A semantical and operational account of call-by-value solvability[END_REF]) one would like to be able to fire the blocked redex, reducing to (λy.u{x aa})w, so that a new redex is created and the computation can continue. According to the standard classification of redex creations due to Lévy [START_REF] Lévy | Réductions correctes et optimales dans le lambda-calcul[END_REF], this is a creation of type 1 1 .

The solution we propose here is to relax the constraint about values, allowing β-redexes to fire whenever the argument is a more general structure, a so-called fireball, defined recursively by extending values with inert terms, i.e. applications of symbols to fireballs. In particular, aa is inert, so that e.g. t → (λy.u{x aa})w, as desired.

Functional languages are usually modelled by weak and closed calculi, so it is natural to wonder about the practical relevance of the FBC. Applications are along two axes. On the one hand, the evaluation mechanism at work in proof assistants has to deal with open terms for comparison and unification. For instance, Grégoire and Leroy's [START_REF] Grégoire | A compiled implementation of strong reduction[END_REF], meant to improve the implementation of Coq, relies on inert terms (therein called accumulators). On the other hand, symbols may also be interpreted as constructors, meant to represent data as lists or trees. The dynamics of fireballs is in fact consistent with the way constructors are handled by Standard ML [START_REF] Milner | The Definition of Standard ML -Revised[END_REF] and in several formalisation of core ML, as in [START_REF] Clément | A simple applicative language: Mini-ml[END_REF]. In this paper we omit destructors, whose dynamics is orthogonal to the one of β-reduction, and we expect all results presented here to carry-over with minor changes to a calculus with destructors. Therefore firing redexes involving inert terms is also justified from a practical perspective.

The Relative Usefulness of Fireballs: as we explained, the generalisation of values to fireballs is motivated by creations of type 1 induced by the firing of inert terms. There is a subtlety, however. While substituting a value can create a new redex (e.g. as in (λx.(xI))I → (xI){x I} = II, where I is the identity-these are called creations of type 3)-substituting a inert term can not. Said differently, duplicating inert terms is useless, and leads to size explosion. Note the tension between different needs: redexes involving inert terms have to be fired (for creations of type 1), and yet the duplication and the substitution of inert terms should be avoided (since they do not give rise to creations of type 3). We solve the tension by turning to sharing, and use the simplicity of the framework to explore the implementation of useful sharing. Both values and inert terms (i.e. fireballs) in argument position will trigger reduction, and both will be shared just after, but only the substitution of values might be useful, because inert terms are useless. This is what we call the relative usefulness of fireballs. It is also why-in contrast to Grégoire and Leroy-we do not identify fireballs and values.

The Result: our main result is an implementation of FBC relying on useful sharing and such that it has only a linear overhead with respect to the number of β-steps. To be precise, the overhead is bilinear, i.e. linear in the number of β-steps and in the size of the initial term (roughly the size of the input). The dependency from the size of the initial term is induced by the action of β on whole subterms, rather than on atomic pieces of data as in RAM or Turing machines. Therefore, β is not exactly as atomic as accessing a register or moving the head of a Turing machine, and this is the price for embracing higher-order computations. Bilinearity, however, guarantees that such a price is mild and that the number of β steps-i.e. of function calls in a functional program-is a faithful measure of the complexity of a program. To sum up, our answer is yes, β is also reasonably atomic.

A Recipe for Bilinearity, with Three Ingredients: our proof technique is a tour de force progressively combining together and adapting to the FBC three recent works involving the LSC, namely the already cited invariance of useful sharing of [START_REF] Accattoli | Beta Reduction is Invariant, Indeed[END_REF], the tight relationship with abstract machines developed by Accattoli, Barenbaum, and Mazza in [START_REF] Accattoli | Distilling abstract machines[END_REF], and the optimisation of the substitution process studied by the present authors in [START_REF] Accattoli | On the value of variables[END_REF]. The next section will give an overview of these works and of how they are here combined, stressing how the proof is more than a simple stratification of techniques. In particular, it was far from evident that the orthogonal solutions introduced by these works could be successfully combined together.

This Paper: the paper is meant to be self-contained, and mostly follows a didactic style. For the first half we warm up by discussing design choices, the difficulty of the problem, and the abstract architecture. The second half focuses on the results. We also suggest reading the introductions of [START_REF] Accattoli | Beta Reduction is Invariant, Indeed[END_REF], [START_REF] Accattoli | Distilling abstract machines[END_REF], [START_REF] Accattoli | On the value of variables[END_REF], as they provide intuitions about concepts that here are only hinted at. Although not essential, they will certainly soften the reading of this work. Omitted proofs are in the companion technical report [START_REF]On the Relative Usefullness of Fireballs[END_REF] and related work is discussed in Sect. III.

II. A RECIPE WITH THREE INGREDIENTS

This section gives a sketch of how the bilinear implementation is built by mixing together tools from three different studies on the LSC.

1) Useful Fireballs: we start by introducing the Useful Fireball Calculus (Useful FBC), akin to the Useful LSC, and provide the proof that the relationship FBC → Useful FBC, analogously to the arrow λ → Useful LSC, has a quadratic overhead. Essentially, this step provides us with the following diagram:

FBC RAM

Useful FBC quadratic

We go beyond simply adapting the study of [START_REF] Accattoli | Beta Reduction is Invariant, Indeed[END_REF], as the use of evaluation contexts (typical of call-by-value scenarios) leads to the new notion of useful evaluation context, that simplifies the technical study of useful sharing. Another key point is the relative usefulness of fireballs, according to their nature: only values are properly subject to the useful discipline, i.e. are duplicated only when they contribute somehow to β-redexes, while inert terms are never duplicated.

2) Distilling Useful Fireballs: actually, we do not follow [START_REF] Accattoli | Beta Reduction is Invariant, Indeed[END_REF] for the study of the arrow Useful FBC → RAM. We rather refine the whole picture, by introducing a further intermediary model, an abstract machine, mediating between the Useful FBC and RAM. We adopt the distillation technique of [START_REF] Accattoli | Distilling abstract machines[END_REF], that establishes a fine-grained and modular view of abstract machines as strategies in the LSC up to a notion of structural equivalence on terms. The general pattern arising from [START_REF] Accattoli | Distilling abstract machines[END_REF] is that for call-by-name/value/need weak and closed calculi the abstract machine adds only a bilinear overhead with respect to the shared evaluation within the LSC:

λ-Calculus RAM LSC Abstract Machine bilinear bilinear
Distilleries owe their name to the fact that the LSC retains only part of the dynamics of a machine. Roughly, it isolates the relevant part of the computation, distilling it away from the search for the next redex implemented by abstract machines.

The search for the redex is mapped to a notion of structural equivalence, a particular trait of the LSC, whose key property is that it can be postponed. Additionally, the transitions implementing the search for the next redex are proved to be bilinear in those simulated by the LSC: the LSC then turns out to be a complexity-preserving abstraction of abstract machines.

The second ingredient for the recipe is then a new abstract machine, called GLAMOUr, that we prove implements the Useful FBC within a bilinear overhead. Moreover, the GLAM-OUr itself can be implemented within a bilinear overhead. Therefore, we obtain the following diagram: 3) Unchaining Substitutions: at this point, it is natural to wonder if the bottleneck given by the side of the diagram FBC → Useful FBC, due to the overhead of the decomposition of substitutions, can be removed. The bound on the overhead is in fact tight, and yet the answer is yes, if one refines the actors of the play. Our previous work [START_REF] Accattoli | On the value of variables[END_REF], showed that (in ordinary weak and closed settings) the quadratic overhead is due to malicious chains of renamings, i.e. of substitutions of variables for variables, and that the substitution overhead reduces to linear if the evaluation is modified so that variables are never substituted, i.e. if values do not include variables.

For the fireball calculus the question is tricky. First of all a disclaimer: with variables we refer to occurrences of bound variables and not to symbols/free variables. Now, our initial definition of the calculus will exclude variables from fireballs, but useful sharing will force us to somehow reintroduce them. Our way out is an optimised form of substitution that unchains renaming chains, and whose overhead is proved linear by a simple amortised analysis. Such a third ingredient is first mixed with both the Useful FBC and the GLAMOUr, obtaining the Unchaining FBC and the Unchaining GLAMOUr, and then used to prove our main result, an implementation FBC → RAM having an overhead linear in the number of β steps and in the size of the initial term: In this step, the original content is that the unchaining optimisation-while inspired by [START_REF] Accattoli | On the value of variables[END_REF]-is subtler to define than in [START_REF] Accattoli | On the value of variables[END_REF], as bound variables cannot be simply removed from the definition of fireballs, because of usefulness. Moreover, we also show how such an optimisation can be implemented at the machine level.

The next section discusses related work. Then there will be a long preliminary part providing basic definitions, an abstract decomposition of the implementation, and a quick study of both a calculus, the Explicit FBC, and a machine, the Open GLAM, without useful sharing. Both the calculus and the machine will not have any good asymptotical property, but they will be simple enough to familiarise the reader with the framework and with the many involved notions.

III. RELATED WORK

In the literature, invariance results for the weak call-byvalue λ-calculus have been proved three times, independently. First, by Blelloch and Greiner [START_REF] Blelloch | Parallelism in sequential functional languages[END_REF], while studying cost models for parallel evaluation. Then by Sands, Gustavsson and Moran [START_REF] Sands | Lambda calculi and linear speedups[END_REF], while studying speedups for functional languages, and finally by Dal Lago and Martini [START_REF] Lago | The weak lambda calculus as a reasonable machine[END_REF], who addressed the invariance thesis for λ-calculus. Among them, [START_REF] Sands | Lambda calculi and linear speedups[END_REF] is the closest one, as it also provides an abstract machine and bounds its overhead. These works however concern closed terms, and so they deal with a much simpler case. Other simple call-byname cases are studied in [START_REF]On constructor rewrite systems and the lambda calculus[END_REF] and [START_REF] Accattoli | On the invariance of the unitary cost model for head reduction[END_REF]. The difficult case of the strong λ-calculus has been studied in [START_REF] Accattoli | Beta Reduction is Invariant, Indeed[END_REF], which is also the only reference for useful sharing.

The LSC is a variation over a λ-calculus with ES by Robin Milner [START_REF] Milner | Local bigraphs and confluence: Two conjectures[END_REF], [START_REF] Kesner | Milner's lambda calculus with partial substitutions[END_REF], obtained by plugging in some of the ideas of the structural λ-calculus by Accattoli and Kesner [START_REF] Accattoli | The structural λ-calculus[END_REF], introduced as a syntactic reformulation of linear logic proof nets. The LSC is similar to calculi studied by De Bruijn [START_REF] De Bruijn | Generalizing Automath by Means of a Lambda-Typed Lambda Calculus[END_REF] and Nederpelt [START_REF] Nederpelt | The fine-structure of lambda calculus[END_REF]. Its first appearances are in [START_REF] Accattoli | On the invariance of the unitary cost model for head reduction[END_REF], [START_REF] Accattoli | An abstract factorization theorem for explicit substitutions[END_REF], but its inception is actually due to Accattoli and Kesner.

Many abstract machines can be rephrased as strategies in λcalculi with explicit substitutions (ES), see at least [START_REF] Curien | An abstract framework for environment machines[END_REF]- [START_REF] Ariola | Sequent calculi and abstract machines[END_REF].

The related work that is by far closer to ours is the already cited study by Grégoire and Leroy of an abstract machine for call-by-value weak and open reduction in [START_REF] Grégoire | A compiled implementation of strong reduction[END_REF]. We developed our setting independently, and yet the FBC is remarkably close to their calculus, in particular our inert terms are essentially their accumulators. The difference is that our work is complexity-oriented while theirs is implementationoriented. On the one hand they do not recognise the relative usefulness of fireballs, and so their machine is not invariant, i.e. our machine is more efficient and on some terms even exponentially faster. On the other hand, they extend the language up to the calculus of constructions, present a compilation to bytecode, and certify in Coq the correctness of the implementation.

The abstract machines in this paper use global environments, an approach followed only by a minority of authors (e.g. [START_REF] Sands | Lambda calculi and linear speedups[END_REF], [START_REF] Accattoli | Distilling abstract machines[END_REF], [START_REF] Fernández | New developments in environment machines[END_REF], [START_REF] Danvy | A synthetic operational account of call-by-need evaluation[END_REF]) and essentially identifying the environment with a store. The distillation technique was developed to better understand the relationship between the KAM and weak linear head reduction pointed out by Danos & Regnier [START_REF] Danos | Head linear reduction[END_REF]. The idea of distinguishing between operational content and search for the redex in an abstract machine is not new, as it underlies in particular the refocusing semantics of Danvy and Nielsen [START_REF] Danvy | Refocusing in reduction semantics[END_REF]. Distilleries however bring an original refinement where logic, rewriting, and complexity enlighten the picture, leading to formal bounds on machine overheads.

Our unchaining optimisation is a lazy variant of an optimisation that repeatedly appeared in the literature, often with reference to space consumption and space leaks, for instance in [START_REF] Sands | Lambda calculi and linear speedups[END_REF] as well as in Wand's [START_REF] Wand | On the correctness of the krivine machine[END_REF] (section 2), Friedman et al.'s [START_REF] Friedman | Improving the lazy krivine machine[END_REF] (section 4), and Sestoft's [START_REF] Sestoft | Deriving a lazy abstract machine[END_REF] (section 4).

IV. THE FIREBALL CALCULUS

The setting is the one of the call-by-value λ-calculus extended with symbols a, b, c, meant to denote free variables (or constructors). The syntax is:

Terms t, u, w, r ::= x | a | λx.t | tu Values v, v ::= λx.t
with the usual notions of free and bound variables, captureavoiding substitution t{x u}, and closed (i.e. without free variables) term. We will often restrict to consider closed terms, the idea being that an open term as x(λy.zy) is rather represented as the closed term a(λy.by).

The ordinary (i.e. without symbols) call-by-value λ-calculus has a nice operational characterisation of values: closed normal forms are values Now, the introduction of symbols breaks this property, because there are closed normal forms as a(λx.x) that are not values. In order to restore the situation, we generalise values to fireballs2 , that are either values v or inert terms A, i.e. symbols possibly applied to fireballs. Associating to the left, fireballs and inerts are compactly defined by Fireballs f, g, h

::= v | A Inert Terms A, B, C ::= af 1 . . . f n n ≥ 0
For instance, λx.y and a are fireballs, as well as a(λx.x), ab, and (a(λx.x))(bc)(λy.(zy)). Fireballs can also be defined more atomically by mixing values and inert terms as follows:

f ::= v | A A ::= a | Af
Note that AB and AA are always inert. Next, we generalise the call-by-value rule (λx.t)v → βv t{x v} to substitute fireballs f rather than values v. First of all, we define a notion of evaluation context (noted F rather than E, reserved to forthcoming global environments), mimicking right-to-left CBV evaluation:

Evaluation Contexts F ::= • | tF | F f note the case F f , that in CBV would be F v. Last, we define the f(fireball) rule → f as follows RULE AT TOP LEVEL CONTEXTUAL CLOSURE (λx.t)f → f t{x f } F t → f F u if t → f u
Our definitions lead to:

Theorem 1. 1) Closed normal forms are fireballs.

2) → f is deterministic.

In the introduction we motivated the notion of fireball both from theoretical and practical points of view. Theorem 1.1 provides a further, strong justification: it expresses a sort of internal harmony of the FBC, allowing to see it as the canonical completion of call-by-value to the open setting.

V. SIZE EXPLOSION

Size explosion is the side effect of a discrepancy between the dynamics and the representation of terms. The usual substitution t{x u} makes copies of u for all the occurrences of x, even if u is useless, i.e. it is normal and it does not create redexes after substitution. These copies are the burden leading to the exponential growth of the size. To illustrate the problem, let's build a size exploding family of terms.

Note that a inert term A, when applied to itself still is a inert term AA. In particular, it still is a fireball, and so it can

:= x | a | λx.t | tu | t[x u] v, v ::= λx.t L, L ::= • | L[x t] A, B, C ::= a | L A L f f, g, h ::= v | A F ::= • | tF | F L f | F [x t] RULE AT TOP LEVEL CONTEXTUAL CLOSURE L λx.t L f →m L t[x L f ] F t m F u if t →m u F x [x L f ] →e L F f [x f ] F t e F u if t →e u t[x u][y w] ≡com t[y w][x u] if y / ∈ fv(u) and x / ∈ fv(w) (tw)[x u] ≡ @r tw[x u] if x ∈ fv(t) (tw)[x u] ≡ @l t[x u]w if x ∈ fv(w) t[x u][y w] ≡ [•] t[x u[y w]] if y ∈ fv(t)
be used as an argument for redexes. We can then easily build a term of size linear in n that in n steps evaluates a complete binary tree A 2 n . Namely, define the family of terms t n for n ≥ 1:

t 1 := λx 1 .(x 1 x 1 ) t n+1 := λx n+1 .(t n (x n+1 x n+1 ))
Now consider t n A, that for a fixed A has size linear in n. The next proposition shows that t n A reduces in n steps to A 2 n , causing size explosion.

Proposition 1 (Size Explosion in the FBC).

t n A → n f A 2 n . Proof: by induction on n. Let B := A 2 = AA. Cases: t 1 = (λx 1 .(x 1 x 1 ))A → f A 2 t n+1 = (λx n+1 .(t n (x n+1 x n+1 )))A → f t n A 2 = t n B → n f (i.h.) B 2 n = A 2 n+1

VI. FIREBALLS AND EXPLICIT SUBSTITUTIONS

In a ordinary weak scenario, sharing of subterms prevents size explosion. In the FBC however this is no longer true, as we show in this section. Sharing of subterms is here represented in a variation over the Linear Substitution Calculus, a formalism with explicit substitutions coming from a linear logic interpretation of the λ-calculus. At the dynamic level, the small-step operational semantics of the FBC is refined into a micro-step one, where explicit substitutions replace one variable occurrence at a time, similarly to abstract machines.

The terms of the Explicit Fireball Calculus (Explicit FBC) are:

t, u, w, r

::= x | a | λx.t | tu | t[x u]
where t[x u] is the explicit substitution (ES) of u for x in t, that is an alternative notation for let x = u in t, and where x becomes bound (in t). We silently work modulo α-equivalence of these bound variables, e.g.

(xy)[y t]{x y} = (yz)[z t].
We use fv(t) for the set of free variables of t. Contexts: the dynamics of explicit substitutions is defined using (one-hole) contexts. Weak contexts subsume all the kinds of context in the paper, and are defined by

W, W ::= • | tW | W t | W [x t] | t[x W ]
The plugging W t of a term t into a context W is defined as • t := t, (λx.W ) t := λx.(W t ), and so on. As usual, plugging in a context can capture variables, e.g.

(( • y)[y t]) y = (yy)[y t].
The plugging W W of a context W into a context W is defined analogously. Since all kinds of context we will deal with will be weak, the definition of plugging applies uniformly to all of them.

A special and frequently used class of contexts is that of substitution contexts

L ::= • | L[x t].
Switching from the FBC to the Explicit FBC the syntactic categories of inert terms A, fireballs f , and evaluation contexts F are generalised in Table I as to include substitution contexts L. Note that fireballs may now contain substitutions, but not at top level, because it is technically convenient to give a separate status to a fireball f in a substitution context L: terms of the form L f are called answers. An initial term is a closed term with no explicit substitutions.

Rewriting Rules: the fireball rule → f is replaced by f , defined as the union of the two rules m and e in Table I: 1) Multiplicative m : is a version of → f where λx.t and f can have substitution contexts L and L around, and the substitution is delayed. 2) Exponential e : the substitution or exponential rule e replaces exactly one occurrence of a variable x currently under evaluation (in F ) with its definiendum f given by the substitution. Note the apparently strange position of L in the reduct. It is correct: L has to commute outside to bind both copies of f , otherwise the rule would create free variables. The name of the rules are due to the linear logic interpretation of the LSC.

Unfolding: the shared representation is related to the usual one via the crucial notion of unfolding, producing the λ-term t → denoted by t and defined by:

x → := x (tu) → := t → u → (λx.t) → := λx.t → t[x u] → := t → {x u → } Note that r n → = A 2 n
. As for the FBC, evaluation is well-defined:

Theorem 2.
1) Closed normal forms are answers, i.e. fireballs in substitution contexts.

2)

f is deterministic. Structural Equivalence: the calculus is endowed with a structural equivalence, noted ≡, whose property is to be a strong bisimulation with respect to f . It is the least equivalence relation closed by weak contexts defined by the axioms in Table I.

Proposition 2 (≡ is a Strong Bisimulation wrt f ). Let x ∈ {sm, se}. Then, t ≡ u and t x t implies that there exists u such that u x u and t ≡ u .

Size Explosion, Again: coming back to the size explosion example, the idea is that-to circumvent it-t n should better m -evaluate to:

r n := (x 0 x 0 )[x 0 x 2 1 ][x 1 x 2 2 ] . . . [x n-1 x 2 n ][x n A]
which is an alternative, compact representation of A 2 n , of size linear in n, and with just one occurrence of A. Without symbols, ES are enough to circumvent size explosion [START_REF] Blelloch | Parallelism in sequential functional languages[END_REF]- [START_REF] Lago | The weak lambda calculus as a reasonable machine[END_REF]. In our case however they fail. The evaluation we just defined indeed does not stop on the desired compact representation, and in fact a linear number of steps (namely 3n) may still produce an exponential output (in a substitution context).

Proposition 3 (Size Explosion in the Explicit FBC).

t n A( m 2 e ) n L A 2 n .
Proof: by induction on n. Let B := A 2 = AA. Cases:

t 1 = (λx 1 .(x 1 x 1 ))A m (x 1 x 1 )[x 1 A] e (x 1 A)[x 1 A] e (AA)[x 1 A] = A 2 [x 1 A] t n+1 = (λx n+1 .(t n (x n+1 x n+1 )))A m 2 e (t n A 2 )[x 1 A] = L t n B ( m 2 e ) n (i.h.) L B 2 n = L A 2 n+1
Before introducing useful evaluation-that will liberate us from size explosion-we are going to fully set up the architecture of the problem, by explaining 1) how ES implement a calculus, 2) how an abstract machine implements a calculus with ES, and 3) how to define an abstract machine for the inefficient Explicit FBC. Only by then (Sect. XI) we will start optimising the framework, first with useful sharing and then by eliminating renaming chains.

VII. TWO LEVELS IMPLEMENTATION

Here we explain how the the small-step strategy → f of the FBC is implemented by a micro-step strategy . We are looking for an appropriate strategy with ES which is polynomially related to both → f and an abstract machine. Then we need two theorems:

1) High-Level Implementation: → f terminates iff terminates. Moreover, → f is implemented by with only a polynomial overhead. Namely,

t k u iff t → h f u → with k polynomial in h; 2) Low-Level Implementation:
is implemented on an abstract machine with an overhead in time which is polynomial in both k and the size of t. We will actually be more accurate, giving linear or quadratic bounds, but this is the general setting.

A. High-Level Implementation

First, terminology and notations. Derivations d, e, . . . are sequences of rewriting steps. With |d|, |d| m , and |d| e we denote respectively the length, the number of multiplicative, and exponential steps of d. Definition 1. Let → f be a deterministic strategy on FBC-terms and a deterministic strategy for terms with ES. The pair (→ f , ) is a high-level implementation system if whenever t is a λ-term and d : t * u then: The high-level part can now be proved abstractly.

1) Normal Form: if u is a -normal form then u → is a → f -normal form. 2) Projection: d → : t → → * f u → and |d → | = |d| m . Moreover,
Theorem 3 (High-Level Implementation). Let t be an ordinary λ-term and (→ f , ) a high-level implementation system. 1) Normalisation: Let us see our framework at work:

t is → f -normalising iff it is - normalising. 2) Projection: if d : t * u then d → : t → * f u → . Moreover,
Theorem 4. (→ f , f ) is a high-level implementation system.
Note the absence of complexity bounds. In fact, (→ f , f ) is not even locally bounded. Let t n here be defined by t 1 = t and t n+1 = t n t, and

u n := (λx.x n )A. Then d : u n m n e A n [x A
] is a counter-example to local boundedness. Moreover, the Explicit FBC also suffers of size explosion, i.e. implementing a single step may take exponential time. In Sect. XI useful sharing will solve these issues.

B. Low-Level Implementation: Abstract Machines

Introducing Distilleries: an abstract machine M is meant to implement a strategy via a distillation, i.e. a decoding function • . A machine has a state s, given by a code t, i.e. a λterm t without ES and not considered up to α-equivalence, and some data-structures like stacks, dumps, environments, and eventually heaps. The data-structures are used to implement the search of the next -redex and some form of parsimonious substitution, and they distill to evaluation contexts for . Every state s decodes to a term s, having the shape F t , where t is a λ-term and F is some kind of evaluation context.

A machine computes using transitions, whose union is noted , of two types. The principal one, noted p , corresponds to the firing of a rule defining . In doing so, the machine can differ from the calculus implemented by a transformation of the evaluation context to an equivalent one, up to structural equivalence ≡. The commutative transitions, noted c , implement the search for the next redex to be fired by rearranging the data-structures to single out a new evaluation context, and they are invisible on the calculus. The names reflect a prooftheoretical view, as machine transitions can be seen as cutelimination steps [START_REF] Accattoli | Distilling abstract machines[END_REF], [START_REF] Ariola | Sequent calculi and abstract machines[END_REF]. Garbage collection is here simply ignored, as in the LSC it can always be postponed.

To preserve correctness, structural equivelance ≡ is required to commute with evaluation , i.e. to satisfy

t u r ≡ ⇒ ∃q s.t. t u r q ≡ ≡
for each of the rules of , preserving the kind of rule. In fact, this means that ≡ is a strong bisimulation (i.e. one step to one step) with respect to . Strong bisimulations formalise transformations which are transparent with respect to the behaviour, even at the level of complexity, because they can be retarded without affecting the length of evaluation: Lemma 1 (≡ Postponement). If ≡ is a strong bisimulation and t (→ ∪ ≡) * u then t → * ≡ u and the number and kind of steps of in the two reduction sequences is the same.

We can finally introduce distilleries, i.e. systems where a strategy simulates a machine M up to structural equivalence ≡ (via the decoding • ). Definition 2. A distillery D = (M, , ≡, • ) is given by: 1) An abstract machine M, given by a) a deterministic labeled transition system on states s; b) a distinguished class of states deemed initial, in bijection with closed λ-terms and from which one obtains the reachable states by applying * ; c) a partition of the labels of the transition system as:

• principal transitions, noted p ,

• commutative transitions, noted c ; 2) a deterministic strategy ; 3) a structural equivalence ≡ on terms s.t. it is a strong bisimulation with respect to ; 4) a distillation • , i.e. a decoding function from states to terms, s.t. on reachable states:

• Principal: s p s implies s ≡ s , • Commutative: s c s implies s ≡ s .

We will soon prove that a distillery implies a simulation theorem, but we want a stronger form of relationship. Additional hypothesis are required to obtain the converse simulation, handle explicit substitution, and talk about complexity bounds. Some terminology first. An execution ρ is a sequence of transition from an initial state. With |ρ|, |ρ| p , and |ρ| c we denote respectively the length, the number of principal, and commutative transitions of ρ. The size of a term is noted |t|.

Definition 3 (Distillation Qualities). A distillery is

• Reflective when on reachable states:

-Termination: c terminates; -Progress: if s reduces then s is not final.

:= • [x t] : E := • [x t] E φ : π := • φ π Fs := D π E (t, π) := t π s := Fs t D : (t, π) := D t π where s = (D, t, π, E) D tu π E c 1 D : (t, π) u E D λx.t u : π E m D t π [x u]E D : (t, π) λx.u E c 2 D t λx.u : π E D : (t, π) a π E c 3 D t (a, π ) : π E D x π E 1 [x u]E 2 e D u α π E 1 [x u]E 2
where u α is any code α-equivalent to u that preserves well-naming of the machine, i.e. such that any bound name in u α is fresh with respect to those in D, π and

E 1 [x u]E 2 .
of RAM steps to implement ρ is the sum of the number for the commutative and the principal transitions. By bilinearity, |ρ| c = O((1 + |ρ| p ) • |t|) and so all the commutative transitions in ρ require O((1+|ρ| p )•|t|) steps, because a single one takes a constant number of steps. Again by bilinearity, each principal one requires O(|t|) steps, and so all the principal transitions together require O(|ρ| p • |t|) steps.

We will discuss three distilleries, summarised in Table IV (page 11), and two of them will be bilinear. The machines will be sophisticated, so that we will first present a machine for the inefficient Explicit FBC (Sect. VIII, called Open GLAM), that we will later refine with useful sharing (Sect. XII, GLAMOUr) and with renaming chains elimination (Sect. XIV, Unchaining GLAMOUr).

Let us point out an apparent discrepancy with the literature. For the simpler case without symbols, the number of commutative steps of the abstract machine studied in [START_REF] Sands | Lambda calculi and linear speedups[END_REF] is truly linear (and not bilinear), i.e. it does not dependent on the size of the initial term. Three remarks:

1) Complete Evaluation: it is true only for evaluation to normal form, while our theorems are also valid for prefixes of the evaluation and diverging evaluations. 2) Normal Form Recognition: it relies on the fact that closed normal forms (i.e. values) can be recognised in constant time, by simply checking the topmost constructor. With symbols checking if a term is normal requires time linear in its size; linearity is simply not possible. 3) Asymptotically Irrelevant: the dependency from the initial term disappears from the number of commutative transitions but still affects the cost of the principal ones, because every exponentials transition copies a subterm of the initial term, and thus it takes O(|t|) time.

VIII. AN INEFFICIENT DISTILLERY: THE OPEN GLAM

In this section we introduce the Open GLAM machine and show that it distills to the Explicit FBC. The distillery is inefficient, because the Explicit FBC suffers of size explosion, but it is a good case study to present distilleries before the optimisations. Moreover, it allows to show an unexpected fact: while adding useful sharing to the calculus will be a quite tricky and technical affair (Sect. XI), adding usefulness to the Open GLAM will be surprisingly simple (Sect. XII), and yet tests of usefulness will only require constant time.

Open GLAM stays for Open Global LAM, in turn referring to a similar machine, based on local environments, introduced in [START_REF] Accattoli | Distilling abstract machines[END_REF] and called LAM-standing for Leroy Abstract Machine. The Open GLAM differs from the LAM in two respects: 1) it uses global rather than local environments, and 2) it has an additional rule ( c3 ) to handle open terms (i.e. symbols).

Data-Structures: at the machine level, terms are replaced by codes, i.e. terms not considered up to α-equivalence. To distinguish codes from terms, we over-line codes like in t.

States (noted s, s , . . .) of the abstract machine are made out of a context dump D, a code t, an argument stack π, and a global environment E, defined by the grammars in Table II. To save space, sometimes we write [x t]E for [x t] : E. Note that stacks may contain pairs (t, π) of a code and a stack, used to code the application of t to the stack π. This representation allows to implement commutative rules in constant time.

The Machine: the machine transitions are given in Table II. Note that the multiplicative one m puts a new entry in the environment, while the exponential one e performs a clashing-avoiding substitution from the environment. The idea is that the principal transitions m and e implement m and e while the commutative transitions c1 , c2 , and c3 locate and expose the next redex following a right-to-left strategy.

The commutative rule c1 forces evaluation to be right-toleft on applications: the machine processes first the argument u, saving the left sub term t on the dump together with its current stack π. The role of c2 and c3 is to backtrack to the saved subterm. Indeed, when the argument, i.e. the current code, is finally put in normal form, encoded by a stack item φ, the stack item is pushed on the stack, and the machine backtracks to the pair on the dump.

The Distillery: machines start an execution on initial states defined as ( , t, , ), i.e. obtained by taking the term, seen now as the code t, and setting to the other machine components. A state represents a term-given by the codeand an evaluation context, that for the Open GLAM is obtained by decoding D, π, and E. The decoding • (or distillation) function is defined in Table II. Note that stacks are decoded

→ := • (tS) → := t → S → (St) → := S → t → S[x t] → := S → {x t → } t → • := t → t → uS := t → S t → Su := t → S t → S[x u] := t → S {x u → } S → • := S → S → uS := S → S S → Su := S → S S → S[x u] := S → S {x u → }
to contest in postfix notation for plugging. To improve readability, when we decode machines, we will denote W t with t W , if the component occurs on the right of t in the machine representation.

A machine state is closed when all free variables in any component of the state are bound in E or, equivalently, when s is closed in the usual sense. It is well-named when all variables bound in the state are distinct. We require well-namedness as a machine invariant to allow every environment entry [x t] to be global (i.e. to bind x everywhere in the machine state). From now on, the initial state associated to a term t has as code the term obtained α-converting t to make it well-named.

For every machine we will have invariants, in order to prove the properties of a distillery. They are always proved by induction over the length of the execution, by a simple inspection of the transitions. For the Open GLAM: Lemma 2 (Open GLAM Invariants). Let s = (D, u, π, E) be a state reachable from an initial code t. Then:

1) Closure: s is closed and well-named;

2) Value: values in components of s are subterms of t;

3) Fireball: every term in π, in E, and in every stack in D is a fireball; 4) Contextual Decoding: E, D, π, and F s are evaluation contexts;

The invariants are used to prove the following theorem.

Theorem 7 (Open GLAM Distillation). (Open GLAM, f , ≡ • ) is a reflective explicit distillery. In particular, let s be a reachable state reachable:

1) Commutative: if s c1,2,3 s then s = s ; 2) Multiplicative: if s m s then s m ≡ s ;

3) Exponential: if s e s then s e s .

Since the Explicit FBC suffers of size explosion, an exponential step (and thus an exponential transition) may duplicate a subterm that is exponentially bigger than the input. Then (Open GLAM, f , ≡, • ) does not satisfy bilinearity, for which every exponential transition has to be linear in the input.

IX. INTERLUDE: RELATIVE UNFOLDINGS

Now we define some notions for weak contexts that will be implicitly instantiated to all kind of contexts in the paper. In particular, we define substitution over contexts, and then use it to define the unfolding of a context, and the more general notion of relative unfolding.

Implicit substitution on weak contexts W is defined by

• {x u} := • (tW ){x u} := t{x u}W {x u} (W t){x u} := W {x u}t{x u} W [y t]{x u} := W {x u}[y t{x u}] t[y W ]{x u} := t{x u}[y W {x u}]
Lemma 3. Let t be a term and W a weak context. Then W t {x u} = W {x u} t{x u} . Now, we would like to extend the unfolding to contexts, but in order to do so we have to restrict the notion of context. Indeed, whenever the hole of a context is inside an ES, the unfolding may erase or duplicate the hole, producing a term or a multi-context, which we do not want. Thus, we turn to (weak) shallow contexts, defined by: S, S , S ::

= • | St | tS | S[x t].
(note the absence of the production t[x S]). Relative unfoldings have a number of properties, summed up in the companion technical report [START_REF]On the Relative Usefullness of Fireballs[END_REF]. Last, a definition that will be important in the next section.

Now, we define in

Definition 4 (Applicative Context).

A shallow context S is applicative when its hole is applied to a sub term u, i.e. if S = S Lu .

X. INTRODUCING USEFUL SHARING

Beware: this and the next sections will heavily use contexts and notions about them as defined in Sect. VI and Sect. IX, in particular the notions of shallow context, applicative context, and relative unfolding.

Introducing Useful Reduction: note that the substitution steps in the size exploding family do not create redexes. We want to restrict the calculus so that these useless steps are avoided. The idea of useful sharing, is to trigger an exponential redex only if it will somehow contribute to create a multiplicative redex. Essentially, one wants only the exponential steps

F x [x L f ] e L F f [x f ] s.t.
F is applicative and f is a value, so that the firing creates a multiplicative redex. Such a change of approach, however, has consequences on the whole design of the system. Indeed, since some substitutions are delayed, the present requirements for the rules might not be met. Consider:

(λx.t)y[y ab]
we want to avoid substituting ab for the argument y, but we also want that evaluation does not stop, i.e. that (λx.

t)y[y ab] → m t[x y[y ab]].

To accomodate such a dynamics, our definitions have to be up to unfolding, i.e. fireballs have to be replaced by terms unfolding to fireballs. There are 4 subtle things about useful reduction.

1) Multiplicatives and Variables: the idea is that the multiplicative rule becomes

L λx.t L u → m L t[x L u ]
where it is the unfolding L u → of the argument L u that is a fireball, and not necessarily L u itself. Note that sometimes variables are valid arguments of multiplicative redexes, and consequently substitutions may contain variables.

2) Exponentials and Future Creations: the exponential rule involves contexts, and is trickier to make it useful. A first approximation of useful exponential step is

F x [x L u ] → e L F u [x u]
where L u → is a value (i.e. it is not inert) and F is applicative, so that-after eventually many substitution steps, when x becomes u → -a multiplicative redex will pop out. Note that an useful exponential step does not always immediately create a multiplicative redex. Consider the following step (where I is the identity):

(xI)[x y][y I] e (yI)[x y][y I] (1)
No multiplicative redex has been created yet, but step ( 1) is useful because the next exponential step creates a multiplicative redex (note how such lookahead is captured by working up to unfoldings):

(yI)[x y][y I] e (II)[x y][y I]
3) Evaluation and Evaluable Contexts: the delaying of useless substitutions impacts also on the notion of evaluation context F , used in the exponential rule. For instance, the following exponential step should be useful

((xI)y)[x I][y ab] e ((II)y)[x I][y ab]

but the context (( • I)y)[x I][y ab] isolating x is not an evaluation context, it only unfolds to one. We then need a notion of evaluation context up to unfolding. The intuition is that a shallow context S is evaluable if S → is an evaluation context (see Sect. IX for the definition of context unfolding), and it is useful if it is evaluable and applicative. The exponential rule then should rather be:

S x [x L u ] → e L S u [x u]
where u → is a value and S is useful.

4) Context Closure vs Global Rules: such a definition, while close to the right one, still misses a fundamental point, i.e. the global nature of useful steps. Evaluation rules are indeed defined by a further closure by contexts, i.e. a step takes place in a certain shallow context S . Of course, S has to be evaluable, but there is more. Such a context, in fact, may also give an essential contribution to the usefulness of a step. Let us give an example. Consider the exponential step

(xx)[x y] e (yx)[x y]
By itself it is not useful, since y is not a value nor unfolds to one. If we plug that redex in the context S := • [y I], however, then y unfolds to a value in S, as y → S = y → • [y λz.z] = λz.z, and the step becomes:

(xx)[x y][y λz.z] e (yx)[x y][y λz.z] (2)
As before, no multiplicative redex has been created yet, but step ( 2) is useful because it is essential for the creation given by the next exponential step:

(yx)[x y][y λz.z] e ((λz.z)x)[x y][y λz.z]
Note, indeed, that (λz.z)x gives a useful multiplicative redex, because x unfolds to a fireball in its context

• [x y][y λz.z].
Summing up, the useful or useless character of a step depends crucially on the surrounding context. Therefore useful rules have to be global: rather than given as axioms closed by evaluable contexts, they will involve the surrounding context itself and impose conditions about it.

The Useful FBC, presented in the next section, formalises these ideas. We will prove it to be a locally bounded implementation of → f , obtaining our fist high-level implementation theorem.

XI. THE USEFUL FIREBALL CALCULUS

For the Useful FBC, terms, values, and substitution contexts are unchanged (with respect to the Explicit FBC), and we use shallow contexts S as defined in Sect. IX. An initial term is still a closed term with no explicit substitutions.

The new key notion is that of evaluable context.

Definition 5 (Evaluable and Useful Contexts). Evaluable (shallow) contexts are defined by the inference system in Table V. A context is useful if it is evaluable and applicative (being applicative is easily seen to be preserved by unfolding).

Point 1 of the following Lemma 4 guarantees that evaluable contexts capture the intended semantics suggested in the previous section. Point 2 instead provides an equivalent inductive formulation that does not mention relative unfoldings. The definition in Table V can be thought has been from the outside, while the lemma give a characterisation from the inside, relating subterms to their surrounding sub-context.

Lemma 4. 1) If S is evaluable then S → is an evaluation context. 2) S is evaluable iff u → S is a fireball whenever S = S S u or S = S S [x u] .
S S x [x L u ] ue S L S u [x u] S S [x L u ] is useful u = u [y w] and u → S L = v Table V EVALUABLE SHALLOW CONTEXTS • is evaluable S is eval. t → is a fireball St is evaluable S is evaluable tS is evaluable S{x t → } is eval. t → is a fireball S[x t] is evaluable
Rewriting Rules: the two rewriting rules um and ue are defined in Table IV, and we use uf for um ∪ ue . The rules are global, i.e. they do not factor as a rule followed by a contextual closure. As already explained, the context has to be taken into account, to understand if the step is useful to multiplicative redexes.

In rule um , the requirement that the whole context around the abstraction is useful guarantees that the argument u unfolds to a fireball in its context. Note also that in ue this is not enough, as such an unfolding has to be a value, otherwise it will not be useful to multiplicative redexes. Moreover, the rule requires u = u [y w], to avoid copying substitutions.

A detailed study of useful evaluation in the companion technical report [START_REF]On the Relative Usefullness of Fireballs[END_REF] shows that: Theorem 8 (Quadratic High-Level Implementation). (→ f , uf ) is a locally bounded high-level implementation system, and so it has a quadratic overhead wrt → f . Moreover, the structural equivalence ≡ is a strong bisimulation also with respect to uf . Proposition 4 (≡ is a Strong Bisimulation wrt uf ). Let x ∈ {um, ue}. Then, t ≡ u and t

x t implies that there exists u such that u x u and t ≡ u .

XII. THE GLAMOUR MACHINE

Here we refine the Open GLAM with a very simple tagging of stacks and environments, in order to implement useful sharing. The idea is that every term in the stack or in the environment carries a label l ∈ {v, A} indicating if it unfolds (relatively to the environment) to a value or to a inert term.

The grammars are identical to the Open GLAM, up to labels:

l ::= v | A E, E ::= | [x φ l ] : E π, π ::= | φ l : π
The decoding of the various machine components is identical to that for the Open GLAM, up to labels that are ignored. The state context, however, now is noted S s , as it is not necessarily an evaluation context, but only an evaluable one.

The transitions are in Table VI. They are obtained from those of the Open GLAM by: 1) Backtracking instead of performing a useless substitution: there are two new backtracking cases c4 and c5 (that in the Open GLAM were handled by the exponential transition), corresponding to avoided useless duplications: c4 backtracks when the entry φ to substitute is marked A (as it unfolds to a inert term) and c5 backtracks when the term is marked v but the stack is empty (i.e. the context is not applicative).

2) Substituting only when it is useful: the exponential transition is applied only when the term to substitute has label v and the stack is non-empty.

Lemma 5 (GLAMOUr Invariants). Let s = (D, u, π, E) be a state reachable from an initial code t. Then: In fact, the distillery is even bilinear, as we now show. The proof employs the following definition of size of a state. Proof: by induction over the length of the derivation. The property trivially holds for the empty derivation. Case analysis over the last machine transition. Commutative rule c1 : the rule splits the code tu between the dump and the code, and the measure-as well as the rhs of the formula-decreases by 1 because the rule consumes the application node. Commutative rules c2,3,4,5 : these rules consume the current code, so they

D t π [x φ l ]E D : (t, π) λx.u E c 2 D t (λx.u) v : π E D : (t, π) a π E c 3 D t (a, π ) A : π E D : (t, π) x π E 1 [x φ A ]E 2 c 4 D t (x, π ) A : π E 1 [x φ A ]E 2 D : (t, π) x E 1 [x u v ]E 2 c 5 D t x v : π E 1 [x u v ]E 2 D x φ l : π E 1 [x u v ]E 2 ue D u α φ l : π E 1 [x u v ]E 2
where u α is any code α-equivalent to u that preserves well-naming of the machine. XIII. THE UNCHAINING FBC In this section we start by analysing why the Useful FBC has a quadratic overhead. We then refine it, obtaining the Unchaining FBC, that we will prove to have only a linear overhead wrt the FBC. The optimisation has to do with the order in which chains of useful substitutions are performed.

:= • | I x [x I ] | I[x t] C, C ::= S x [x I] | C x [x I] | S C ← ------- S y [y I] x := S[y I x ] ← ------- C y [y I] x := ← - C y [y I x ] ← --- S C x := S ← - C x RULE (ALREADY CLOSED BY CONTEXTS) SIDE CONDITION S L λx.t u om S L t[x u] S • u is useful S S x [x L v ] oes S L S v [x v] S S [x L v ] is useful S C x [x L v ] oec S L C v [x v] S ← - C x [x L v ] is
Analysis of Useful Substitution Chains: in the Useful FBC, whenever there is a situation like

(x 1 A)[x 1 x 2 ] . . . [x n-1 x n ][x n v]
the uf strategy performs n + 1 exponential steps ue replacing x 1 with x 2 , then x 2 with x 3 , and so on, until v is finally substituted on the head

(x n A)[x 1 x 2 ] . . . [x n-1 x n ][x n v] ue (vA)[x 1 x 2 ] . . . [x n-1 x n ][x n v]
and a multiplicative redex can be fired. Any later occurrence of x 1 will trigger the same chain of exponential steps again.

Because the length n of the chain is bounded by the number of previous multiplicative steps (local bound property), the overall complexity of the machine is quadratic in the number of multiplicative steps. In our previous work [START_REF] Accattoli | On the value of variables[END_REF], we showed that to reduce the complexity to linear it is enough to perform substitution steps in reverse order, modifying the chains while traversing them. The idea is that in the previous example one should rather have a smart reduction oe (o stays for optimised, as u is already used for useful reduction) following the chain of substitutions and performing:

(x 1 A)[x 1 x 2 ] . . . [x n-1 x n ][x n v] oe (x 1 A)[x 1 x 2 ] . . . [x n-1 v][x n v] oe . . . (x 1 A)[x 1 v] . . . [x n-1 v][x n v] oe (vA)[x 1 v] . . . [x n-1 v][x n v]
Later occurrences of x 1 will no longer trigger the chain, because it has been unchained by traversing it the first time.

Unfortunately, introducing such an optimisation for useful reduction is hard. In the shown example, that has a very simple form, it is quite easy to define what following the chain means. For the distillation machinery to work, however, we need our rewriting rules to be stable by structural equivalence, whose action is a rearrangement of substitutions through the term structure. Then the substitutions [x i x i+1 ] of the example can be spread all over the term, interleaved by applications and other substitutions, and even nested one into the other (like in [x i x i+1 [x i+1 x i+2 ]]). This makes the specification of unchaining useful reduction a quite technical affair.

Chain Contexts: reconsider a term like in the example,

(xA)[x 1 x 2 ][x 2 x 3 ][x 3 x 4 ][x 4 v].
We want the next step to substitute on x 4 so we should give a status to the context

C := (xA)[x 1 x 2 ][x 2 x 3 ][x 3 • ].
The problem is that C can be deformed by structural equivalence ≡ as

C := (x[x 1 x 2 [x 2 x 3 ]]A)[x 3 • ]
and so this context has to be caught too. We specify these context in Table VII as chain contexts C, defined using the auxiliary notion of identity context I, that captures a simpler form of chain (note that both notions are not shallow).

Given a chain context C, we will need to retrieve the point where the chain started, i.e. the shallow context isolating the variable at the left end of the chain (x 1 in the example). We are now going to define an operation associating to every chain context its chain-starting (shallow) context. To see the two as contexts of a same term, we need also to provide the subterm that we will put in C (that will always be a variable). The chain-starting context ← -C x associated to the chain context C (with respect to x) is defined in Table VII.

For our example

C := (xA)[x 1 x 2 ][x 2 x 3 ][x 3 • ] we have ← - C x4 = ( • A)[x 1 x 2 ][x 2 x 3 ][x 3 x 4 ], as expected.
Rewriting Rules: the rules of the Unchaining FBC are in Table VII. Note that the exponential rule splits in two, the ordinary shallow case oes (now constrained to values) and the chain case oec (where the new definition play a role). They could be merged, but for the complexity analysis and the relationship with the next machine is better to distinguish them. We use oe for oes ∪ oec , and of for om ∪ oe . Note the use of ← -C x in the third side condition.

A. Linearity: Multiplicative vs Exponential Analysis

To prove that of implements → f with a global bound, and thus with a linear overhead, we need to show that the global number of exponential steps ( oe ) in a of -derivation is bound by the number of multiplicative steps ( om ). We need the following invariant.

Lemma 7 (Subterm Invariant). Let t be a λ-term and d : t * u. Then every value in u is a value in t. We presented the interesting bit of the proof of our improved high-level implementation theorem, which follows. The remaining details are in [START_REF]On the Relative Usefullness of Fireballs[END_REF].

Theorem 12 (Linear High-Level Implementation). (→ f , of ) is a globally bounded high-level implementation system, and so it has a linear overhead wrt → f . Last, the structural equivalence ≡ is a strong bisimulation also for the Unchaining FBC.

Proposition 5 (≡ is a Strong Bisimulation). Let x ∈ {om, oms, omc}. Then, t ≡ u and t x t implies that there exists u such that u x u and t ≡ u .

XIV. UNCHAINING GLAMOUR

The Unchaining GLAMOUr machine, in Table VIII, behaves like the GLAMOUr machine until the code is a variable x 1 that is hereditarily bound in the global environment to a value via the chain

[x 1 x 2 ] v . . . [x n v] v ,
and the stack is not empty (i.e. evaluation is in an applicative context). At this point the machine needs to traverse the chain until it finds the final binding [x n v] v , and then traverse again the chain in the opposite direction replacing every

[x i x i+1 ] v entry with [x i v] v .
The forward traversal of the chain is implemented by a new commutative rule c6 that pushes the variables encountered in the chain on a new machine component, called the chain heap. The backward traversal is driven by the next variable popped from the heap, and it is implemented by a new exponential rule (the chain exponential rule, corresponding to that of the calculus). Most of the analyses of the GLAMOUr carry over to the Unchaining GLAMOUr.

D t π [x φ l ]E D : (t, π) λx.u E c 2 D t (λx.u) v : π E D : (t, π) a π E c 3 D t (a, π ) A : π E D : (t, π) x π E 1 [x φ A ]E 2 c 4 D t (x, π ) A : π E 1 [x φ A ]E 2 D : (t, π) x E 1 [x u v ]E 2 c 5 D t x v : π E 1 [x u v ]E 2 D x φ l : π E 1 [x v v ]E 2 oes D v α φ l : π E 1 [x v v ]E 2 D H x φ l : π E 1 [x y v ]E 2 c 6 D H : x y φ l : π E 1 [x y v ]E 2 D H : y x φ l : π E • oec D H y φ l : π E • with E • := E 1 [x v v ]E 2 [y x v ]E 3 , E • := E 1 [x v v ]E 2 [y v αv ]E 3 ,
and where v α is any code α-equivalent to v that preserves well-naming of the machine.

Every old grammar is as before, and heaps are simply lists of variables, i.e. they are defined by H ::= | H : x.

Decoding and Invariants: because of chain heaps and chain contexts, the decoding is involved.

First of all, note that there is a correlation between the chain and the environment, as the variables of a chain heap H = x 1 : . . . : x n need to have corresponding entries [x i x v i+1 ]. More precisely, we will show that the following notion of compatibility is an invariant of the machine.

Definition 7 (Compatibility Heap-Environment). Let E be an environment and H = x 1 : . . . : x n be a heap. We say that H is compatible with E if either H is empty or [x i x v i+1 ] ∈ E for i < n, [x n x v ] ∈ E, and [x φ v ] ∈ E for some φ v . Given a state s = (D, H, t, π, E), the dump, the stack and the environment provide a shallow context S s := D π E that will be shown to be evaluable, as for the GLAMOUr.

If the chain heap H is not empty, the current code t is somewhere in the middle of a chain inside the environment, and it is not apt to fill the state context S s . The right code is the variable x 1 starting the chain heap H = x 1 : . . . : x n . Thus, the term to plug in the state context is t H , given by: t := t t x1:...:xn

:= x 1
Finally, a state decodes to a term as follows: s := S s t H .

Lemma 11 (Unchaining GLAMOUr Invariants). Let s = (D, H, u, π, E) be a state reachable from an initial code t. We need additional decodings to retrieve the chainstarting context C in the side-condition of oec rule, thatunsurprisingly-is given by the chain heap. Let s = (D, H : y, t, π, E) be a state s.t. H : y is compatible with E. Note that compatibility gives E = E 1 [y t v ]E 2 . Define the chain context C s and the substitution context L s as:

C s := D y H π E 1 [y • ] L s := E 2
The first point of the following lemma guarantees that C s and L s are well defined. The second point proves that filling L s C s with the current term gives exactly the decoding of the state s = S s y H , and moreover the chain starts exactly on the evaluable context given by the state, i.e. that S s = L s ← -C s x .

Lemma We can now sum up.

Theorem 13 (Unchaining GLAMOUr Distillation).

(Unchaining GLAMOUr, of , ≡, • ) is a reflective explicit distillery. In particular, let s be a reachable state: 1) Commutative: if s c1,2,3,4,5,6 s then s = s ; 2) Multiplicative: if s om s then s om ≡ s ;

3) Shallow Exponential: if s oes s then s oes s ; 4) Chain Exponential: if s oec s then s oec s .

A. Bilinearity: Principal vs Commutative Analysis

Bilinearity wrt c1,2,3,4,5 is identical to that of the GLAM-OUr, thus we omit it and focus on c6 .

The size |H| of a chain heap is its length as a list.

Lemma 13 (Linearity of c6 ). Let s = (D, H, t, π, E) be a state reached by an execution ρ. Then Let us conclude with a remark. Our result requires a compact representation of terms via ES. Because unfolding may exponentially increase the size of a term, it is important to show that common operations like equality checking (up to α-conversion) can be implemented efficiently on the compact representation. In other words, ES are succinct data structures, in the sense of Jacobson [START_REF] Jacobson | Succinct static data structures[END_REF].

Despite quadratic and quasi-linear recent algorithms [START_REF] Accattoli | On the invariance of the unitary cost model for head reduction[END_REF], [START_REF] Grabmayer | Maximal sharing in the lambda calculus with letrec[END_REF] for testing equality of terms with ES, we discovered that a linear algorithm can be obtained by slightly modifying an algorithm already known quite some time before (1976!): the Paterson-Wegman linear unification algorithm [START_REF] Paterson | Linear unification[END_REF] (better explained in [START_REF] De Champeaux | About the Paterson-Wegman linear unification algorithm[END_REF]). The algorithm works on first order terms represented as DAGs, and unification boils down to equality checking when no metavariable occurs in the involved terms.

Our terms with ES can not be fed directly to the Paterson-Wegmar algorithm: we represent shared terms via occurrences of variables bound in substitutions, whereas Paterson-Wegmar uses a simple DAG representation. The change of representation can be easily done in linear time in the size of the input.

Moreover, the Paterson-Wegmar algorithm works with standard equality, whereas we are interested in α-equivalence. Therefore the algorithm needs to be adapted so that two λbound variables are considered equivalent when they point to binding nodes that have already been determined to be candidates for equality. The details of the adaptation of Paterson-Wegmar are left to a forthcoming publication.

Definition 6 .

 6 The size of codes and states is defined by:|x| = |a| := 1 |tu| := |t| + |u| + 1 |λx.t| := |t| + 1 |(D, t, π, E)| := |t| + Σ (u,π)∈D |u| Lemma 6 (Size Bounded). Let s = (D, u, π, E) be a state reached by an execution ρ of initial code t. Then |s| ≤ (1 + |ρ| ue )|t| -|ρ| c .

A 1 ) 3 )Lemma 9 .

 139 substitution t[x u] is basic if u has the form L y . The basic size |t| b of t is the number of its basic substitutions. Lemma 8 (Steps and Basic Size). If t oes u then |u| b = |t| b ; 2) If t oec u then |t| b > 0 and |u| b = |t| b -1; If t om u then |u| b = |t| b or |u| b = |t| b + 1. Let t be initial and d : t * of u. Then |u| b ≤ |d| om -|d| oec . Proof: by induction on |d|. If |d| = 0 the statement holds. If |d| > 0 consider the last step w of u of d and the prefix e : t * of w of d. By i.h., |w| b ≤ |e| om -|e| oec . Cases of w of u. Shallow Exponential Step oes : |u| b ≤ L.

1 )Proof: 1 )

 11 |ρ| c6 = |H| + |ρ| oec . 2) |H| ≤ |ρ| m . 3) |ρ| c6 ≤ |ρ| m + |ρ| oec = O(|ρ| p ). By induction over |ρ| and analysis of the last machine transition. The c6 steps increment the size of the heap. The oec steps decrement it. All other steps do not change the heap. 2) By the compatible heap invariant (Lemma 11.6), |H| ≤ |E|. By the environment size invariant (Lemma 11.5), |E| ≤ |ρ| m . Then |H| ≤ |ρ| m . 3) Plugging Point 2 into Point 1. Corollary 3 (Bilinearity of c ). Let s be a state reached by an execution ρ of initial code t. Then |ρ| c ≤ (1 + |ρ| e )|t| + |ρ| m + |ρ| oec = O((1 + |ρ| p ) • |t|).

Finally

  , we obtain the main result of the paper. Theorem 14 (Useful Implementation). 1) Low-Level Bilinear Implementation: a of -derivation d is implementable on RAM in O((1 + |d|) • |t|) steps. 2) Low + High Bilinear Implementation: a → f -derivation d is implementable on RAM in O((1 + |d|) • |t|) steps.

Table I

 I SYNTAX, REWRITING RULES, AND STRUCTURAL EQUIVALENCE OF THE EXPLICIT FBC t, u, w, r :

  it is 1) locally bounded: if the length of a sequence of substitution e-steps from u is linear in the number |d| m of m-steps in d; 2) globally bounded: if |d| e is linear in |d| m . The normal form and projection properties address the qualitative part, i.e. the part about termination. The normal form property guarantees that does not stop prematurely, so that when terminates → f cannot keep going. The projection property guarantees that termination of → f implies termination of . The two properties actually state a stronger fact: → f steps can be identified with the m -steps of the strategy. The local and global bounds allow to bound the overhead introduced by the Explicit FBC wrt the FBC, because by relating m and e steps, they relate |d| and |d → |, since → f and m steps can be identified.

  Partition: principal transitions are partitioned into multiplicative m and exponential e , like for the strategy . -Explicit decoding: the partition is preserved by the decoding, i.e. With |ρ| m and |ρ| e we denote respectively the number of multiplicative and exponential transitions of ρ. Theorem 5 (Correctness and Completeness). Let D be a reflective distillery and s an initial state. 1) Strong Simulation: for every execution ρ : s * s there is a derivation d : s * ≡ s s.t. |ρ| p = |d|. 2) Reverse Strong Simulation: for every derivation d : s * t there is an execution ρ : s * s s.t. t ≡ s and |ρ| p = |d|. Moreover, if D is explicit then |ρ| m = |d| m and |ρ| e = |d| e . Bilinearity, instead, is crucial for the low-level theorem. + |d|) • |t|) steps, i.e. bilinear in the size of the initial term t and the length of the derivation |d|.

	-Commutative: c is implementable on RAM in a
	constant number of steps;
	-Principal: p is implementable on RAM in O(|t|)
	steps.
	A reflective distillery is enough to obtain a bisimulation
	between the strategy	and the machine M, that is strong
	up to structural equivalence ≡. Theorem 6 (Low-Level Implementation Theorem). Let	be
	a strategy on terms with ES and D = (M, , ≡, • ) a bilinear
	distillery. Then a	-derivation d is implementable on RAM
	machines in O((1

• Explicit when -* Multiplicative: s m s implies s m ≡ s ; * Exponential: s e s implies s e ≡ s ; • Bilinear when it is reflective and -Execution Length: given an execution ρ from an initial term t, the number of commutative steps |ρ| c is linear in both |t| and |ρ| p (with a slightly stronger dependency on |t|, due to the time needed to recognise a normal form), i.e. if |ρ| c = O((1 + |ρ| p ) • |t|). Proof: given d : t n u by Theorem 5.2 there is an execution ρ : s * s s.t. u ≡ s and |ρ| p = |d|. The number

Table IV DISTILLERIES

 IV IN THE PAPER + REWRITING RULES FOR THE USEFUL FBC

	Calculus	Machine	RULE (ALREADY CLOSED BY CONTEXTS)	SIDE CONDITIONS
	FBC →f		S L λx.t u	um S L t[x u]	S Lu is useful
	Explicit FBC f	Open GLAM
	Useful FBC uf	GLAMOUr
	Unchaining FBC of	Unchaining GLAMOUr

  Multiplicative: if s um s then s um ≡ s ; 3) Exponential: if s ue s then s ue s .

	1) Closure: s is closed and well named;
	2) Value: values in components of s are subterms of t; 3) Fireball: t → E is a fireball (of kind l) for every code t l in
	π, E, and in every stack of D;
	4) Evaluability: E, D → E , π → E , and S s are evaluable con-
	texts;
	5) Environment Size: the length of the global environment
	E is bound by |ρ| m .
	Theorem 9 (GLAMOUr Distillation). (GLAMOUr, uf , ≡
	, • ) is a reflective explicit distillery. In particular, let s be a
	reachable state:
	1) Commutative: if s c1,2,3,4,5 s then s = s ;
	2)

  useful decrease the measure of at least 1. Multiplicative: it consumes the lambda abstraction. Exponential: it modifies the current code by replacing a variable (of size 1) with a value v coming from the environment. Because of Lemma 5.2, v is a subterm of t and the dump size increment is bounded by |t|. Corollary 1 (Bilinearity of c ). Let s be a state reached by an execution ρ of initial code t. Then |ρ| c ≤ (1 + |ρ| e )|t|. High Quadratic Implementation: a → f -derivation d is implementable on RAM in O((1 + |d| 2 ) • |t|) steps, i.e. linear in the size of the initial term t and quadratic in the length of the derivation |d|.

	Finally, we obtain our first implementation theorem.
	Theorem 10 (Useful Implementation).
	1) Low-Level Bilinear Implementation: a	uf -derivation
	d is implementable on RAM in O((1 + |d|) • |t|) (i.e.
	bilinear) steps.
	2) Low +

  8.1 |w| b -1 ≤ i.h. |e| om -|e| oec -1 = |e| om -(|e| oec + 1) = |d| om -|d| oec Chain Exponential Step oec : |u| b = L.8.2 |w| b ≤ i.h. |e| om -|e| oec = |d| om -|d| oec Multiplicative Step om : |u| b ≤ L.8.3 |w| b + 1 ≤ i.h. |e| om -|e| oec + 1 = e + 1 -|e| oec = |d| om -|d| oec Corollary 2 (Linear Bound on Chain Exponential Steps). Let t be initial and d : t * of u. Then |d| oec ≤ |d| om . Next, we bound shallow steps. Lemma 10 (Linear Bound on Shallow Exponential Steps). Let t be initial and d : t * of u. Then |d| oes ≤ |d| om . Proof: first note that if t oes u then u om w, because by definition oes can fire only if it creates a om -redex. Such a fact and determinism of of together imply |d| oes ≤ |d| om + 1, because every oes step is matched by the eventual om steps that follows it immediately. However, note that in t there are no explicit substitutions so that the first step is necessarily an unmatched om step. Thus |d| oes ≤ |d| om . Theorem 11 (Linear Bound on Exponential Steps). Let t be initial and d : t * of u. Then |d| oe ≤ 2 • |d| om . Proof: by definition, |d| oe = |d| oec + |d| oes . By Corollary 2, |d| oec ≤ |d| om and by Lemma 10 |d| oes ≤ |d| om , and so |d| oe ≤ 2 • |d| om .

  1) Closure: s is closed and s is well named; 2) Value: values in components of s are subterms of t; 3) Fireball: t → E is a fireball (of kind l) for every code t l in π and E; 4) Evaluability: E, D → E , π → E , and S s are evaluable cont.; 5) Environment Size: the length of the global environment E is bound by |ρ| m . 6) Compatible Heap: if H = then the stack is not empty, u = x, and H is compatible with E.

  12 (Heaps and Contexts). Let s = (D, H : y, x, π, E) be a state s.t. H : y is compatible with E. Then: 1) L s is a substitution context and C s is a chain context 2) s. t. s = S s y H = L s C s x with S s = L s

	← -C s	x

The reader unfamiliar with redex creations should not worry. Creations are a key concept in the study of usefulness-which is why we mention thembut for the present discussion it is enough to know that there exists two kinds of creations (type 1 and the forthcoming type 3, other types will not play a role), no expertise on creations is required.

About fireball: the first choice was fire-able, but then the spell checker suggested fireball.

ACKNOWLEDGEMENTS

A special acknowledgement to Ugo Dal Lago, to whom we owe the intuition that using labels may lead to a local and efficient implementation of useful sharing. We are also grateful to Franc ¸ois Pottier, whose comments on a draft helped to improve the terminology and the presentation.