Beniamino Accattoli
email: beniamino.accattoli@inria.fr

Pablo Barenbaum
email: pbarenbaum@dc.uba.ar

Damiano Mazza
email: damiano.mazza@lipn.univ-paris13.fr

A Strong Distillery

machines for the strong evaluation of λ-terms (that is, under abstractions) are a mostly neglected topic, despite their use in the implementation of proof assistants and higher-order logic programming languages. This paper introduces a machine for the simplest form of strong evaluation, leftmost-outermost (call-by-name) evaluation to normal form, proving it correct, complete, and bounding its overhead. Such a machine, deemed Strong Milner Abstract Machine, is a variant of the KAM computing normal forms and using just one global environment. Its properties are studied via a special form of decoding, called a distillation, into the Linear Substitution Calculus, neatly reformulating the machine as a standard micro-step strategy for explicit substitutions, namely linear leftmost-outermost reduction, i.e. the extension to normal form of linear head reduction. Additionally, the overhead of the machine is shown to be linear both in the number of steps and in the size of the initial term, validating its design. The study highlights two distinguished features of strong machines, namely backtracking phases and their interactions with abstractions and environments.

Introduction

The computational model behind functional programming is the weak λ-calculus, where weakness is the fact that evaluation stops as soon as an abstraction is obtained. Evaluation is usually defined in a small-step way, specifying a strategy for the selection of weak β-redexes. Both the advantage and the drawback of λ-calculus is the lack of a machine in the definition of the model. Unsurprisingly implementations of functional languages have been explored for decades.

Implementation schemes are called abstract machines, and usually account for two tasks. First, they switch from small-step to micro-step evaluation, delaying the costly meta-level substitution used in small-step operational semantics and replacing it with substitutions of one occurrence at a time, when required. Second, they also search the next redex to reduce, walking through the program according to some evaluation strategy. Abstract machines are machines because they are deterministic and the complexity of their steps can easily be measured, and are abstract because they omit many details of a real implementation, like the actual representation of terms and data-structures or the garbage collector.

Historically, the theory of λ-calculus and the implementation of functional languages have followed orthogonal approaches. The former rather dealt with strong evaluation, and it is only since the seminal work of Abramsky and Ong [1] that the theory took weak evaluation seriously. Dually, practical studies mostly ignored strong evaluation, with the notable exception of Crégut [START_REF] Crégut | An abstract machine for lambda-terms normalization[END_REF][START_REF] Crégut | Strongly reducing variants of the Krivine abstract machine[END_REF] (1990) and, more recently, the semi-strong approach of Grégoire and Leroy [START_REF] Grégoire | A compiled implementation of strong reduction[END_REF] (2002)see also the related work paragraph below. Strong evaluation is nonetheless essential in the implementation of proof assistants or higher-order logic programming, typically for type-checking in frameworks with dependent types as the Edinburgh Logical Framework or the Calculus of Constructions, as well as for unification modulo βη in simply typed frameworks like λ-prolog.

The aim of this paper is to move the first steps towards a systematic and theoretical exploration of the implementation of strong evaluation. Here we deal with the simplest possible case, call-by-name evaluation to strong normal form, implemented by a variant of the Krivine Abstract Machine. The study is carried out according to the distillation methodology, a new approach recently introduced by the authors and previously applied only to weak evaluation [START_REF] Accattoli | Distilling abstract machines[END_REF].

Distilling Abstract Machines. Many abstract machines can be rephrased as strategies in λ-calculi with explicit substitutions (ES for short), see at least [START_REF] Curien | An abstract framework for environment machines[END_REF][START_REF] Hardin | Functional runtime systems within the lambda-sigma calculus[END_REF][START_REF] Crégut | Strongly reducing variants of the Krivine abstract machine[END_REF][START_REF] Biernacka | A concrete framework for environment machines[END_REF][START_REF] Lang | Explaining the lazy Krivine machine using explicit substitution and addresses[END_REF][START_REF] Ariola | Sequent calculi and abstract machines[END_REF]. The Linear Substitution Calculus (LSC)-a variation over a λcalculus with ES by Robin Milner [START_REF] Milner | Local bigraphs and confluence: Two conjectures[END_REF] developed by Accattoli and Kesner [2,[START_REF] Accattoli | A nonstandard standardization theorem[END_REF]-provides more than a simple reformulation: it disentangles the two tasks carried out by abstract machines, retaining the micro-step operational semantics and omitting the search for the next redex. Such a neat disentangling, that we prefer to call a distillation, is a decoding based on the following key points:

1. Partitioning: the machine transitions are split in two classes. Principal transitions are mapped to the rewriting rules of the calculus, while commutative transitions-responsible for the search for the redex-are mapped on a notion of structural equivalence, specific to the LSC. 2. Rewriting: structural equivalence accounts both for the search for the redex and garbage collection, and commutes with evaluation. It can thus be postponed, isolating the micro-step strategy in the rewriting of the LSC. 3. Logic: the LSC itself has only two rules, corresponding to cut-elimination in linear logic proof nets. A distillation then provides a logical reading of an abstract machine (see [START_REF] Accattoli | Distilling abstract machines[END_REF] for more details). 4. Complexity: by design, a principal transition has to take linear time in the input, while a commutative transition has to be constant.

A distillery is then given by a machine, a strategy, a structural equivalence, and a decoding function satisfying the above points. In bilinear distilleries, the number of commutative transitions is linear in both the number of principal transitions and the size of the initial term. Bilinearity guarantees that distilling away the commutative part by switching to the LSC preserves the asymptotical behavior, i.e. it does not forget too much. At the same time, the bound on the commutative overhead justifies the design of the abstract machine, providing a provably bounded implementation scheme.

A Strong Distillery. Our machine is a strong version of the Milner Abstract Machine (MAM), a variant with just one global environment of the Krivine Abstract Machine (KAM), introduced in [START_REF] Accattoli | Distilling abstract machines[END_REF].

The first result of the paper is the design of a distillery relating the Strong MAM to linear leftmost-outermost reduction in the LSC [START_REF] Accattoli | A nonstandard standardization theorem[END_REF][START_REF] Accattoli | Beta Reduction is Invariant, Indeed[END_REF]-that is at the same time a refinement of leftmost-outermost (LO) β-reduction and an extension of linear head reduction [START_REF] Mascari | Head linear reduction and pure proof net extraction[END_REF][START_REF] Danos | Head linear reduction[END_REF]2] to normal form-together with the proof of correctness and completeness of the implementation. Moreover, the linear LO strategy is standard and normalizing [START_REF] Accattoli | A nonstandard standardization theorem[END_REF], and thus we provide an instance of Plotkin's approach of mapping abstract machines to such strategies [START_REF] Plotkin | Call-by-name, call-by-value and the lambda-calculus[END_REF].

The second result is the complexity analysis showing that the distillery is bilinear, i.e. that the cost of the additional search for the next redex specific to the machine is negligible. The analysis is simple, and yet subtle and robust. It is subtle because it requires a global analysis of executions, and it is robust because the overhead is bilinear for any evaluation sequence, not necessarily to normal form, and even for diverging ones.

For the design of the Strong MAM we make various choices:

1. Global Environment: we employ a global environment, which is in opposition to having closures (pairing subterms with local environments), and it models a store-based implementation scheme. The choice is motivated by future extensions to more efficient strategies as call-by-need, where the global environment allows to integrate sharing with a form of memoization [START_REF] Danvy | A synthetic operational account of call-by-need evaluation[END_REF][START_REF] Accattoli | Distilling abstract machines[END_REF]. 2. Sequential Exploration and Backtracking: we fix a sequential exploration of the term (according to the leftmost-outermost order), in opposition to the parallel evaluation of the arguments (once a head normal form has been reached). This choice internalizes the handling of the recursive iterations, that would be otherwise left to the meta-level, providing a finer study of the data-structures needed by a strong machine. On the other hand, it forces to have backtracking transitions, activated when the current subterm has been checked to be normal and evaluation needs to retrieve the next subterm on the stack. Call-by-value machines usually have a similar but simpler backtracking mechanism, realized via an additional component, the dump. 3. (Almost) No Garbage Collection: we focus on time complexity, and thus ignore space issues, that is, our machine does not account for garbage collection. In particular, we keep the global environment completely unstructured, similarly to the (weak) MAM. Strong evaluation however is subtler, as to establish a precise relationship between the machine and the calculus with ES, garbage collection cannot be completely ignored. Our approach is to isolate it within the meta-level: we use a system of parenthesized markers, to delimit subenvironments created under abstractions that could be garbage collected once the machine backtracks outside those abstraction. These labels are not inspected by the transitions, and play a role only for the proof of the distillation theorem. Garbage collection then is somewhat accounted for by the analysis, but there are no dedicated transitions nor rewriting rules, it is rather encapsulated in the decoding and in the structural equivalence.

Efficiency? It is known that LO evaluation is not efficient. Improvements are possible along three axis: refining the strategy (by turning to strong call-byvalue/need, partially done in [START_REF] Grégoire | A compiled implementation of strong reduction[END_REF][START_REF] Crégut | Strongly reducing variants of the Krivine abstract machine[END_REF][START_REF] Accattoli | On the relative usefulness of fireballs[END_REF]), speeding up the substitution process (by forbidding the substitution of variables, see [START_REF] Accattoli | On the value of variables[END_REF][START_REF] Accattoli | On the relative usefulness of fireballs[END_REF]), and avoiding useless substitutions (by adding useful sharing, see [START_REF] Accattoli | Beta Reduction is Invariant, Indeed[END_REF][START_REF] Accattoli | On the relative usefulness of fireballs[END_REF]). These improvements however require sophisticated machines, left to future work. LO evaluation is nonetheless a good first case study, as it allows to isolate the analysis of backtracking phases and their subtle interactions with abstractions and environments. We expect that the mentioned optimizations can be added in a quite modular way, as they have all been addressed in the complementary study in [START_REF] Accattoli | On the relative usefulness of fireballs[END_REF], based on the same technology (i.e. LSC and distilleries).

(Scarce) Related Work. Beyond Crégut's [START_REF] Crégut | An abstract machine for lambda-terms normalization[END_REF][START_REF] Crégut | Strongly reducing variants of the Krivine abstract machine[END_REF], we are aware of only two other similar works on strong abstract machines, García-Pérez, Nogueira and Moreno-Navarro's [START_REF] García-Pérez | Deriving the full-reducing krivine machine from the small-step operational semantics of normal order[END_REF] (2013), and Smith's [START_REF] Smith | Abstract machines for higher-order term sharing[END_REF] (unpublished, 2014). Two further studies, de Carvalho's [START_REF] De Carvalho | Execution time of lambda-terms via denotational semantics and intersection types[END_REF] and Ehrhard and Regnier's [START_REF] Ehrhard | Böhm trees, Krivine's machine and the Taylor expansion of lambda-terms[END_REF], introduce strong versions of the KAM but for theoretical purposes; in particular, their design choices are not tuned towards implementations (e.g. rely on a naïve parallel exploration of the term). Semi-strong machines for call-by-value (i.e. dealing with weak evaluation but on open terms) are studied by Grégoire and Leroy [START_REF] Grégoire | A compiled implementation of strong reduction[END_REF] and in a recent work by Accattoli and Sacerdoti Coen [START_REF] Accattoli | On the relative usefulness of fireballs[END_REF] (see [START_REF] Accattoli | On the relative usefulness of fireballs[END_REF] for a comparison with [START_REF] Grégoire | A compiled implementation of strong reduction[END_REF]). More recent work by Dénès [START_REF] Dénès | Étude formelle d'algorithmes efficaces en algèbre linéaire[END_REF] and Boutiller [START_REF] Boutiller | De nouveaus outils pour manipuler les inductif en Coq[END_REF] appeared in the context of term evaluation in Coq. These works, which do offer the nice perspective of concretely dealing with proof assistants, are focused on quite specific Coq-related tasks (such as term simplification) and the difference in reduction strategy and underlying motivations makes a comparison difficult. Of all the above, the closest to ours is Crégut's work, because it defines an implementation-oriented strong KAM, thus also addressing leftmost-outermost reduction. His machine uses local environments, sequential exploration and backtracking, scope markers akin to ours, and a calculus with ES to establish the correctness of the implementation. His calculus, however, has no less than 13 rewriting rules, while ours just 2, and so our approach is simpler by an order of magnitude. Moreover, we want to stress that our contribution does not lie in the machine per se, or the chosen reduction strategy (as long as it is strong), but in the combined presence of a robust and simple abstraction of the machine, provided by the LSC, and the complexity analysis showing that such an abstraction does not miss too much. In this respect, none of the above works comes with an analysis of the overhead of the machine nor with the logical and rewriting perspective we provide. In fact, our approach offers general guidelines for the design of (strong) abstract machines. The choice of leftmost-outermost reduction showcases the idea while keeping technicalities to a minimum, but it is by no means a limitation. The development of strong distilleries for call-by-value or lazy strategies, which may be more attractive from a programming languages perspective, are certainly possible and will be the object of future work (again, an intermediary step has already been taken in [START_REF] Accattoli | On the relative usefulness of fireballs[END_REF]).

Global environments are explored by Fernández and Siafakas in [START_REF] Fernández | New developments in environment machines[END_REF], and used in a minority of works, e.g. [START_REF] Sands | Lambda calculi and linear speedups[END_REF][START_REF] Danvy | A synthetic operational account of call-by-need evaluation[END_REF]. We introduced the distillation technique in [START_REF] Accattoli | Distilling abstract machines[END_REF] to revisit the relationship between the KAM and weak linear head reduction pointed out by Danos and Regnier [START_REF] Danos | Head linear reduction[END_REF]. Distilleries have also been used in [START_REF] Accattoli | On the relative usefulness of fireballs[END_REF]. The idea to distinguish 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]. The LSC, with its roots in linear logic proof nets, allows to see this distinction as an avatar of the principal/commutative divide in cut-elimination, because machine transitions may be seen as cut-elimination steps [START_REF] Ariola | Sequent calculi and abstract machines[END_REF][START_REF] Accattoli | Distilling abstract machines[END_REF]. Hence, it is fair to say that distilleries bring an original refinement where logic, rewriting, and complexity enlighten the picture, leading to formal bounds on machine overheads.

Omitted proofs may be found in [4].

Linear Leftmost-Outermost Reduction

The language of the linear substitution calculus (LSC for short) is given by the following term grammar: The operational semantics of the LSC is parametric in a notion of (one-hole) context. General contexts, that simply extend the contexts for λ-terms with the two cases for ES, and the special case of substitution contexts are defined by:

LSC Terms t, u, w, r ::= x | λx.t | tu | t[x u].
Contexts C, C ::= • | λx.C | Ct | tC | C[x t] | t[x C]; Substitution Contexts L, L ::= • | L[x t].
The plugging C t of a term t into a context C is defined as • t := t, (λx.C) t := λx.(C t ), and so on. As usual, plugging in a context can capture variables, e.g.

(( • y)[y t]) y = (yy)[y t]. The plugging C C of a context C into a context C is defined analogously. We write C ≺ p t if there is a term u s.t. C u = t, call it the prefix relation.
The rewriting relation is →:=→ m ∪ → e where → m and → e are the multiplicative and exponential rules, defined by

Rule at Top Level Contextual closure Multiplicative L λx.t u → m L t[x u] C t → m C u if t → m u Exponential C x [x u] → e C u [x u] C t → e C u if t → e u
The rewriting rules are assumed to use on-the-fly α-equivalence to avoid variable capture. For instance, (λx. The above operational semantics ignores garbage collection. In the LSC, this may be realized by an additional rule which may always be postponed, see [2].

Taking the external context into account, an exponential step has the form

C C x [x u] → e C C u [x u] .
We shall often use a compact form:

Exponential Rule in Compact Form C x → e C u if C = C C[x u] Definition 1 (Redex Position). Given a → m -step C t → m C u with t → m u or a compact → e -step C
x → e C t , the position of the redex is the context C.

We identify a redex with its position, thus using C, C , C for redexes, and use d : t → k u for derivations, i.e. for possibly empty sequences of rewriting steps. We write |t| [•] for the number of substitutions in t, and use |d|, |d| m , and |d| e for the number of steps, m-steps, and e-steps in d, respectively.

Linear Leftmost-Outermost Reduction, Two Definitions. We give two definitions of linear LO reduction → LO , a traditional one based on ordering redexes and a new contextual one not mentioning the order, apt to work with LSC and relate it to abstract machines. We start by defining the LO order on contexts.

Definition 2 (LO Order). The outside-in order C ≺ O C is defined by 1. Root: • ≺ O C for every context C = • ; 2. Contextual closure: if C ≺ O C then C C ≺ O C C for any context C .
Note that ≺ O can be seen as the prefix relation ≺ p on contexts. The left-to-right order C ≺ L C is defined by

1. Application: if C ≺ p t and C ≺ p u then Cu ≺ L tC ; 2. Substitution: if C ≺ p t and C ≺ p u then C[x u] ≺ L t[x C ]; 3. Contextual closure: if C ≺ L C then C C ≺ L C C for any context C .
Last, the left-to-right outside-in order is defined by

C ≺ LO C if C ≺ O C or C ≺ L C .
Two examples of the outside-in order are (λx.

• )t ≺ O (λx.( • [y u]))t and t[x • ] ≺ O t[x uC],
and an example of the left-to-right order is t[x C]u ≺ L t[x w] • . The next immediate lemma guarantees that we defined a total order.

Lemma 1 (Totality of ≺ LO ). If C ≺ p t and C ≺ p t then either C ≺ LO C or C ≺ LO C or C = C .
Remember that we identify redexes with their position context and write C ≺ LO C . We can now define linear LO reduction, first considered in [START_REF] Accattoli | A nonstandard standardization theorem[END_REF], where it is proved that it is standard and normalizing, and then in [START_REF] Accattoli | Beta Reduction is Invariant, Indeed[END_REF], extending linear head reduction [START_REF] Mascari | Head linear reduction and pure proof net extraction[END_REF][START_REF] Danos | Head linear reduction[END_REF]2] to normal form. Definition 3 (Linear LO Reduction → LO ). Let t be a term. C is the leftmostoutermost (LO for short) redex of t if C ≺ LO C for every other redex C of t. We write t → LO u if a step reduces the LO redex.

We now define LO contexts and prove that the position of a linear LO step is always a LO context. We need two notions.

Definition 4 (Neutral Term). A term is neutral if it is →-normal and it is not of the form L λx.t .
Neutral terms are such that their plugging in a context cannot create a multiplicative redex. We also need the notion of left free variable of a context, i.e. of a variable occurring free at the left of the hole. Structural Equivalence. A peculiar trait of the LSC is that the rewriting rules do not propagate ES. Therefore, evaluation is usually stable by structural equivalences moving ES around. In this paper we use the following equivalence, including garbage collection (≡ gc ), that we prove to be a strong bisimulation.

Definition 7 (Structural equivalence). The structural equivalence ≡ is the symmetric, reflexive, transitive, and contextual closure of the following axioms:

(λx.t)[y u] ≡ λ λx.t[y u] if x ∈ fv(u) (t u)[x w] ≡ @l t[x w] u if x ∈ fv(u) (t u)[x w] ≡ @r t u[x w] if x ∈ fv(t) t[x u][y w] ≡ com t[y w][x u] if y ∈ fv(u) and x ∈ fv(w) t[x u][y w] ≡ [•] t[x u[y w]] if y ∈ fv(t) t[x u] ≡ gc t if x ∈ fv(t) t[x u] ≡ dup t [y]x [x u][y u]
In ≡ dup , t [y]x denotes a term obtained from t by renaming some (possibly none) occurrences of x as y, with y a fresh variable.

Proposition 1 (Structural Equivalence ≡ is a Strong Bisimulation). If t ≡ u → LO w then exists r s.t. t → LO r ≡ w and the steps are either both multiplicative or both exponential.

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 heaps. The data-structures are used to implement the search for the next -redex and some form of substitution, and they decode to evaluation contexts for . Every state s decodes to a term s, having the shape C s t , where t is the code currently under evaluation and C s is the evaluation context given by the data-structures.

A machine computes using transitions, whose union is denoted by , of two types. The principal one, denoted by p , corresponds to the firing of a rule defining , up to structural equivalence ≡. The commutative transitions, denoted by c , only rearrange the data structures, and on the calculus are either invisible or mapped to ≡. The terminology reflects a proof-theoretic view, as machine transitions can be seen as cut-elimination steps [START_REF] Ariola | Sequent calculi and abstract machines[END_REF][START_REF] Accattoli | Distilling abstract machines[END_REF]. The transformation of evaluation contexts is formalized in the LSC as a structural equivalence ≡, which 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 , that is what we proved in Proposition 1 for the equivalence at work in this paper. Strong bisimulations formalize transformations which are transparent with respect to the behavior, even at the level of complexity, because they can be delayed without affecting the length of evaluation:

Lemma 3 (Postponement of ≡). If ≡ is a strong bisimulation, t ( ∪ ≡) * u implies t * ≡ u and the number and kind of steps of in the two reduction sequences is exactly 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 8. A distillery D = (M, , ≡, • ) is given by:

1. An abstract machine M, given by (a) a deterministic labeled transition system (lts) over states s, with labels in {m, e, c}; the transitions labelled by m, e are called principal, the others commutative; (b) a distinguished class of states deemed initial, in bijection with closed λ-terms; from these, the reachable states are obtained by applying * ; 2. a deterministic strategy , i.e., a deterministic lts over the terms of the LSC induced by some strategy on its reduction rules, with labels in {m, e}.

3. a structural equivalence ≡ on terms which is a strong bisimulation with respect to ; 4. a decoding function • from states to terms whose graph, when restricted to reachable states, is a weak simulation up to ≡ (the commutative transitions are considered as τ actions). More explicitly, for all reachable states: projection of principal transitions: s p s implies s p ≡ s for all p ∈ {m, e}; distillation of commutative transitions: s c s implies s ≡ s .

The simulation property is a minimum requirement, but a stronger form of relationship is usually desirable. Additional hypotheses are required in order to obtain the converse simulation and provide complexity bounds.

Terminology: an execution ρ is a sequence of transitions from an initial state. With |ρ|, |ρ| p and |ρ| c we denote respectively the length, the number of principal and commutative transitions of ρ, whereas |t| denotes the size of a term t.

Definition 9 (Distillation Qualities). A distillery is

-Reflective when on reachable states:

• Termination: c terminates;

• Progress: if s is final then s is a -normal form. -Bilinear when, given an execution ρ from an initial term t:

• A reflective distillery is enough to obtain a weak bi simulation between the strategy and the machine M, up to structural equivalence ≡ (again, the weakness is with respect to commutative transitions). With |ρ| m and |ρ| e we denote respectively the number of multiplicative and exponential transitions of ρ.

Theorem 1 (Correctness and Completeness). Let D be a reflective distillery and s an initial state.

Strengthening the MAM

The machine we are about to introduce implements leftmost-outermost reduction and may therefore be seen as a strong version of the Krivine abstract machine (KAM). However, it differs from the KAM in the fundamental point of using global, as opposed to local, environments. It is therefore more appropriate to say that it is a strong version of the machine we introduced in [START_REF] Accattoli | Distilling abstract machines[END_REF], which we called MAM (Milner abstract machine). Let us briefly recall its definition:

tu π E c 1 t u : π E λx.t u : π E m t π [x u] : E x π E e t α π E if E(x) = t
Note that the stack and the environment of the MAM contain codes, not closures as in the KAM. A global environment indeed circumvents the complex mutually recursive notions of local environment and closure, at the price of the explicit αrenaming t α which is applied on the fly in e . The price however is negligible, at least theoretically, as the asymptotic complexity of the machine is not affected, see [START_REF] Accattoli | Distilling abstract machines[END_REF] (the same can be said of variable names vs de Bruijn indexes/levels). We know that the MAM performs weak head reduction, whose reduction contexts are (informally) of the form • π. This justifies the presence of the stack. It is immediate to extend the MAM so that it performs full head reduction, i.e., so that the head redex is reduced even if it is under an abstraction. Since head contexts are of the form Λ. • π (with Λ a list of abstractions), we simply add a stack of abstractions Λ and augment the machine with the following transition:

Abs Code Stack Env Abs Code Stack Env Λ λx.t E c 2 x : Λ t E
The other transitions do not touch the Λ stack. LO reduction is nothing but iterated head reduction. LO reduction contexts, which we formally introduced in Definition 6, when restricted to the pure λ-calculus (without ES) are of the form Λ.rCπ, where: Λ and π are as above; r, if present, is a neutral term; and C is either • or, inductively, a LO context. Then LO contexts may be represented by stacks of triples of the form (Λ, r, π), where r is a neutral term. These stacks of triples will be called dumps.

The states of the machine for full LO reduction are as above but augmented with a dump and a phase ϕ, indicating whether we are executing head reduction ( ) or whether we are backtracking to find the starting point of the next iteration ( ). To the above transitions (which do not touch the dump and are always in the phase), we add the following:

Abs Code Stack Env Dump Ph Abs Code Stack Env Dump Ph Λ x π E D c 3 Λ x π E D if E(x) = ⊥ x : Λ t E D c 5 Λ λx.t E D u E (Λ, t, π) : D c 7 Λ tu π E D Λ t u : π E D c 6 u E (Λ, t, π) : D
where E(x) = ⊥ means that the variable x is undefined in the environment E.

In the machine we actually use we join the dump and the Λ stack into the frame F , to reduce the number of machine components (the analysis will however somewhat reintroduce the distinction). In the sequel, the reader should bear in mind that a state of the Strong MAM introduced below corresponds to a state of the machine just discussed according to the following correspondence: 4Discussed Machine:

Abs Code Stack Env Dump Ph Λ0 t π E (Λ1, t1, π1) : • • • : (Λn, tn, πn) ϕ
Strong MAM:

Frame Code Stack Env Ph Λ0 : (t1, π1) : Λ1 : • • • : (tn, πn) : Λn t π E ϕ

The Strong Milner Abstract Machine

The components and the transitions of the Strong MAM are given by the first two boxes in Fig. 1. As above, we use t, u, . . . to denote codes, i.e., terms not containing ES and well-named, by which mean that distinct binders bind distinct variables and that the sets of free and bound variables are disjoint (codes are not considered up to α-equivalence). The Strong MAM has two phases: evaluation ( ) and backtracking ( ).

Initial states. The initial states of the Strong MAM are of the form | t | | | , where t is a closed code called the initial term. In the sequel, we abusively say that a state is reachable from a term meaning that it is reachable from the corresponding initial state.

Scope Markers. The two transitions to evaluate and backtrack on abstractions, c2 and c4 , add markers to delimit subenvironments associated to scopes. The marker x is introduced when the machine starts evaluating under an abstraction λx, while x marks the end of such a subenvironment.

Slight Notation Abuse. The data structures we are going to use are defined as lists, using for the empty list and ":" for both the cons and append operation. The overloading of : means that in the case of, e.g., an environment E we have E : = E = : E, and in particular : = . Such an abuse will be used thoughout the whole paper.

© Frames F ::= | (t, π) : F | x : F Stacks π ::= | t : π Environments E ::= | [x t] : E | x : E | x : E Phases ϕ ::= | 9 8 6 7 Frame Code Stack Env Ph Frame Code Stack Env Ph F tu π E c 1 F t u : π E F λx.t u : π E m F t π [x u] : E F λx.t E c 2 x : F t x : E F x π E e F t α π E if E(x) = t F x π E c 3 F x π E if E(x) = x : F t E c 4 F λx.t x : E (t, π) : F u E c 5 F tu π E F t u : π E c 6 (t, π) : F u E # " !
Frames (Ordinary, Weak, Trunk)

F ::= Fw | Ft | Fw : Ft Fw ::= | (t, π) : F Ft ::= | x : F Environments (Well-Formed, Weak, Trunk) E ::= Ew | Et | Ew : Et Ew ::= | [x t] : Ew | x : Ew : x : E w Et ::= | x : E Fig. 1. The Strong MAM.
Weak and Trunk Frames. A frame F may be uniquely decomposed into F = F w : F t , where F w = (t 1 , π 1 ) : • • • : (t n , π n ) (with n possibly null) is a weak frame, i.e. where no abstracted variable appear, and F t is a trunk frame, i.e. not of the form (t, π) : F (it either starts a variable entry or it is empty). More precisely, we rely on the alternative grammar in the third box of Fig. 1. We denote by Λ(F ) the set of variables in F , i.e. the set of x s.t. F = F : x : F .

Weak, Trunk, and Well-Formed Environments. Similarly to the frame, the environment of a reachable state has a weak/trunk structure. In contrast to frames, however, not every environment can be seen this way, but only the well-formed ones (reachable environments will be shown to be well-formed). A weak environment E w does not contain any open scope, i.e. whenever in E w there is a scope opener marker ( x) then one can also find the scope closer marker ( x), and (globally) the closed scopes of E w are well-parenthesized. A trunk environment E t may instead also contain open scopes that have no closing marker in E t (but not unmatched closing markers x). Formally, weak E w , trunk E t , and well-formed environments E (all the environments that we will consider will be well-formed, that is why we note them E) are defined in the third box in Fig. 1.

Closed Scopes and Meta-level Garbage Collection. Fragments of the form x : E w : x within an environment will essentially be ignored; this is how a simple form of garbage collection is encapsulated at the meta-level in the decoding. In

Backtracking Free Variables:

(1) Backtracking Code: if ϕ = then fv(u) ⊆ Λ(F );

(2) Pairs in the Frame: if F = F : (w, π ) : F then fv(w) ⊆ Λ(F ). 4. Name:

(1) Substitutions: if E = E : [x t] : E then x is fresh wrt t and E ;

(2) Markers: if E = E : x : E and F = F : x : F then x is fresh wrt E and F , and E (y) = ⊥ for any free variable y in F ; (3) Abstractions: if λx.t is a subterm of F , u, π, or E then x may occur only in t and in the closed subenvironment x : E w : x of E, if it exists. 5. Closure:

(1) Environment: if E = E : [x t] : E then E (y) = ⊥ for all y ∈ fv(t);

(2) Code, Stack, and Frame: E(x) = ⊥ for any free variable in u and in any code of π and F .

Since the statement of the invariants is rather technical, let us summarize the dependencies (or lack thereof) of the various points and their use in the distillation proof of the next section.

-The compatibility, normal form and backtracking free variables invariants are independent of each other and of the subsequent invariants. -The name invariant relies on the compatibility invariant only.

-The closure invariant relies on the compatibility, name and backtracking free variable invariants only. It is crucial for the progress property (because in the variable case at least one among e and c4 applies). The proof of every invariant is by induction on the number of transitions leading to the reachable state. In this respect, the various points of the statement of each invariant (e.g. points 5.1 and 5.2) are entangled, in the sense that each point needs to use the induction hypothesis of one of the other points, and thus they cannot be proved separately.

Implementing Environments. Note that substitutions in closed scopes are never used by the machine, because the operation E(x) is defined by ignoring them. Moreover, the name invariant guarantees that if E(x) = x then E does not contain a substitution on x. These two facts imply that the scope markers x and x are not really needed in an actual implementation: the test E(x) = x in c3 can indeed be replaced-in the variant without markers (also redifining E(x) as simple look-up in E)-by a test of undefinedness. The markers are in fact needed only for the analysis, as they structure the frame and the environment of a reachable state into weak and trunk parts, allowing a simple decoding towards terms with ES.

Moreover, variables are meant to be implemented as memory locations, so that the environment is simply a store, and the list structure of environments is not necessary either. Such an assumption allows to access the environment in constant time on RAM, and will be essential for the proof of the bilinearity of the distillery (to be defined).

Therefore, the structure of environments-given by the scope markers and the list structure-is an artifice used to define the decoding and develop the analysis, but it is not meant to be part of the actual implementation.

-Case s = (F, λx.t, u : π, E, ) m (F, t, π, [x u] : E, ) = s . Note that C s = F ∝ E π is LO by the LO decoding invariant (Lemma 8). Moreover by the closure invariant (Lemma 6.5) x does not occur in F nor π, justifying the use of Lemma 9 in:

(F, λx.t, u : π, E, ) = F ∝ E u : π λx.t = F ∝ E π (λx.t)u → m F ∝ E π t[x u] ≡ L.9.1 F ∝ E π t [x u] ≡ L.9.2 F ∝ ([x u] : E) π t = (F, t, π, [x u] : E, ) -Case s = (F, x, π, E, ) e (F, t α , π, E, ) = s with E(x) = t.
) ∝ E = (x : F ) ∝ (E w : x : E ) = (x : F ) ∝ ( x : E ) E w
Since we are in a backtracking phase ( ), the backtracking free variables invariant (Lemma 6.3.1) and the open scopes matching property (Lemma 5.3) give fv(t) ⊆ L.6.3.1 Λ(F ) = L.5.3 Λ(E w : x : E ) = L.4 Λ( x : E ), i.e. E w does not bind any variable in fv(t). Then E w t ≡ * gc t, and

(x : F, t, , E, ) = (x : F ) ∝ E t = (x : F ) ∝ (E w : x : E ) t = (x : F ) ∝ ( x : E ) E w t ≡ * gc (x : F ) ∝ ( x : E ) t = F ∝ E λx.t = L.7 F ∝ ( x : E w : x : E ) λx.t = F ∝ ( x : E) λx.t = (F, λx.t, , x : E, ) -Case (F, tu, π, E, ) c1 (F, t, u : π, E, ). (F, tu, π, E, ) = F ∝ E π tu = F ∝ E u : π t = (F, t, u : π, E, ) -Case (F, λx.t, , E, ) c2 (x : F, t, , x : E, ). (F, λx.t, , E, ) = F ∝ E λx.t = (x : F ) ∝ ( x : E) t = (x : F, t, , x : E, ) -Case (F, x, π, E, ) c3 (F, x, π, E, ). (F, x, π, E, ) = F ∝ E π x = (F, x, π, E, ) -Case ((t, π) : F, u, , E, ) c5 (F, tu, π, E, ). ((t, π) : F, u, , E, ) = (t, π) : F ∝ E u = F ∝ E π t u = (F, tu, π, E, ) -Case (F, t, u : π, E, ) c6 ((t, π) : F, u, , E, ). (F, t, u : π, E, ) = F ∝ E u : π t = F ∝ E π t u = ((t, π) : F ) ∝ E u = ((t, π) : F, u, , E, )
For what concerns reflectiveness, termination of commutative transitions is subsumed by bilinearity (Theorem 4 below). For progress, note that

Complexity Analysis

The complexity analysis requires a further invariant, bounding the size of the duplicated subterms. For us, u is a subterm of t if it does so up to variable names, both free and bound. More precisely: define t -as t in which all variables (including those appearing in binders) are replaced by a fixed symbol * . Then, we will consider u to be a subterm of t whenever u -is a subterm of t -in the usual sense. The key property ensured by this definition is that the size |u| of u is bounded by |t|.

Lemma 10 (Subterm Invariant). Let ρ be an execution from an initial code t. Every code duplicated along ρ using e is a subterm of t.

Via the distillation theorem (Theorem 3), the invariant provides a new proof of the subterm property of linear LO reduction (first proved in [START_REF] Accattoli | Beta Reduction is Invariant, Indeed[END_REF]).

Lemma 11 (Subterm Property for → LO ). Let d be a → LO -derivation from an initial term t. Every term duplicated along d using → e is a subterm of t.

The next theorem is our second main result, from which the low-level implementation theorem (Theorem 2) follows. Let us stress that, despite the simplicity of the reasoning, the analysis is subtle as the length of backtracking phases (Point 2) can be bound only globally, by the whole previous evaluation work.

Theorem 4 (Bilinearity). The Strong MAM is bilinear, i.e. given an execution ρ : s * s from an initial state of code t then: Last, every transition but e takes a constant time on a RAM.The renaming in a e step is instead linear in |t|, by the subterm invariant (Lemma 10).

  t)[y u]y → m t{y z}[x y][z u] for z / ∈ fv(t), and (λy.(xy))[x y] → e (λz.(yz))[x y]. Moreover, in → e the context C is assumed to not capture x, in order to have (λx.x)[x y] → e (λx.y)[x y].

Definition 5 ( 1 .

 51 Left Free Variables). The set lfv(C) of left free variables of C is defined by:lfv( • ) := ∅ lfv(tC) := fv(t) ∪ lfv(C) lfv(λx.C) := lfv(C) \ {x} lfv(C[x t]) := lfv(C) \ {x} lfv(Ct) := lfv(C) lfv(t[x C]) := (fv(t) \ {x}) ∪ lfv(C) Definition 6 (LO Contexts). A context C is LO if Right Application: whenever C = C tC then tis neutral, and 2. Left Application: whenever C = C C t then C = L λx.C . 3. Substitution: whenever C = C C [x u] then x / ∈ lfv(C ). Lemma 2 (LO Reduction and LO Contexts). Let t → u by reducing a redex C. Then C is a → LO step iff C is LO.

1 .

 1 Simulation up to ≡: for every execution ρ : s * s there is a derivation d : s * ≡ s s.t. |ρ| m = |d| m and |ρ| e = |d| e . 2. Reverse Simulation up to ≡: for every derivation d : s * t there is an execution ρ : s * s s.t. t ≡ s and |ρ| m = |d| m and |ρ| e = |d| e . Bilinearity, instead, is crucial for the low-level theorem. Theorem 2 (Low-Level Implementation Theorem). Let be a strategy on terms with ES s.t. there exists a bilinear reflective distillery D = (M, , ≡ , • ). Then a derivation d : t * u is implementable on RAM machines in O((1 + |d|) • |t|) steps, i.e. bilinear in the size |t| of the initial term and the length |d| of the derivation. Proof. Given d : t n u by Theorem 1.2 there is an execution ρ : s * s s.t. u ≡ s and |ρ| p = |d|. The cost of implementing ρ is the sum of the costs of implementing 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 takes O(|t|), and so all the principal transitions together require O(|ρ| p • |t|) steps.

1 .

 1 Commutative Evaluation Steps are Bilinear: |ρ| c ≤ (1 + |ρ| e ) • |t|. 2. Commutative Evaluation Bounds Backtracking: |ρ| c ≤ 2 • |ρ| c . 3. Commutative Steps are Bilinear: |ρ| c ≤ 3 • (1 + |ρ| e ) • |t|. Proof. 1. We prove a slightly stronger statement, namely |ρ| c + |ρ| m ≤ (1 + |ρ| e ) • |t|, by means of the following notion of size for stacks/frames/states: | | := 0 |x : F | := |F | |t : π| := |t| + |π| |(t, π) : F | := |π| + |F | |(F, t, π, E, )| := |F | + |π| + |t| |(F, t, π, E, )| := |F | + |π| By direct inspection of the rules of the machine it can be checked that: -Exponentials Increase the Size: if s e s is an exponential transition, then |s | ≤ |s| + |t| where |t| is the size of the initial term; this is a consequence of the fact that exponential steps retrieve a piece of code from the environment, which is a subterm of the initial term by Lemma 10; -Non-Exponential Evaluation Transitions Decrease the Size: if s a s with a ∈ {m, c 1 , c 2 , c 3 } then |s | < |s|; -Backtracking Transitions do not Change the Size: if s a s with a ∈ { c 4 , c 5 , c 6 } then |s | = |s|. Then a straightforward induction on |ρ| shows that |s | ≤ |s| + |ρ| e • |t| -|ρ| c -|ρ| m i.e. that |ρ| c + |ρ| m ≤ |s| + |ρ| e • |t| -|s |. Now note that | • | is always non-negative and that since s is initial we have |s| = |t|. We can then conclude with |ρ| c + |ρ| m ≤ |s| + |ρ| e • |t| -|s | ≤ |s| + |ρ| e • |t| = |t| + |ρ| e • |t| = (1 + |ρ| e ) • |t| 2. We have to estimate |ρ| c = |ρ| c4 + |ρ| c5 + |ρ| c6 . Note that (a) |ρ| c4 ≤ |ρ| c2 , as c4 pops variables from F , pushed only by c2 ; (b) |ρ| c5 ≤ |ρ| c6 , as c5 pops pairs (t, π) from F , pushed only by c6 ; (c) |ρ| c6 ≤ |ρ| c3 , as c6 ends backtracking phases, started only by c3 . Then |ρ| c ≤ |ρ| c2 + 2|ρ| c3 ≤ 2|ρ| c . 3. We have |ρ| c = |ρ| c + |ρ| c ≤ P.2 |ρ| c + 2|ρ| c = P.1 3 • (1 + |ρ| e ) • |t|.

  As before, C s is LO by Lemma 8. Moreover, E(x) = t guarantees that E, and thus C s , have a substitution binding x to t. Finally, C s = C s . Then s = C s x → e C s t

α = s -Case s = (x : F, t, , E, ) c4 (F, λx.t, , x : E, ) = s . By Lemma 6.1 x : F ∝ E, and by Lemma 5.2 E = E w : x : E . Then (x : F

  1. the machine cannot get stuck during the evaluation phase: for applications and abstractions it is evident and for variables one among e and

				c3
	always applies, because of the closure invariant (Lemma 6.5).
	2. final states have the form ( , t, , E, ), because
	(a) by the previous consideration they are in a backtracking phase,
	(b) if the stack is non-empty then	c6 applies,
	(c) otherwise if the frame is not empty then either	c4 or	c5 applies.

[START_REF] Accattoli | Distilling abstract machines[END_REF]

. final states decode to normal terms: a final state s = ( , t, , E, ) decodes to s = E t which is normal and closed by the normal form (Lemma 6.2.1) and backtracking free variables (Lemma 6.3.1) invariants.

Modulo the presence of markers of the form x and x in the environment, which are needed for bookkeeping purposes and were omitted here.

Acknowledgments. This work was partially supported by projects Logoi ANR-2010-BLAN-0213-02, Coquas ANR-12-JS02-006-01, Elica ANR-14-CE25-0005, the Saint-Exupéry program funded by the French embassy and the Ministry of Education in Argentina, and the French-Argentinian laboratory in Computer Science INFINIS.

Code

Stack Env Code Stack Env

particular, for a well-formed environment E we define E(x) as: Note that the only potential source of non-determinism for the Strong MAM is the choice among e and c4 in the variable case. The operation E(x), however, is a function, and so the machine is deterministic.

We write Λ(E) to denote the set of variables bound to by an environment E, i.e. those variables whose scope is not closed with .

Lemma 4 (Weak Environments Contain only Closed Scopes). If E w is a weak environment then Λ(E w ) = ∅.

Compatibility. In the Strong MAM, both the frame and the environment record information about the abstractions in which evaluation is currently taking place. Clearly, such information has to be coherent, otherwise the decoding of a state becomes impossible. The following compatibility predicate captures the correlation between the structure of the frame and that of the environment. Compatible Pairs:

Weak Frames: Stacks:

States:

The following lemmas sum up the properties of the decoding.

Lemma 7 (Closed Scopes Disappear). Let F ∝ E be a compatible pair. Then F ∝ ( x :

The next theorem is our first main result. By the abstract approach presented in Sect. 3 (Theorem 1), it implies that the Strong MAM is a correct and complete implementation of linear LO evaluation to normal form. Theorem 3 (Distillation). (Strong MAM, → LO , ≡, • ) is an explicit and reflective distillery. In particular: