key: cord-0060358-luxovgr0 authors: Faggian, Claudia; Guerrieri, Giulio title: Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic date: 2021-03-23 journal: Foundations of Software Science and Computation Structures DOI: 10.1007/978-3-030-71995-1_11 sha: 3b7c432e7a0a52e4d6ce671d47f3c4bcf528e857 doc_id: 60358 cord_uid: luxovgr0 In each variant of the [Formula: see text] -calculus, factorization and normalization are two key properties that show how results are computed. Instead of proving factorization/normalization for the call-by-name (CbN) and call-by-value (CbV) variants separately, we prove them only once, for the bang calculus (an extension of the [Formula: see text] -calculus inspired by linear logic and subsuming CbN and CbV), and then we transfer the result via translations, obtaining factorization/normalization for CbN and CbV. The approach is robust: it still holds when extending the calculi with operators and extra rules to model some additional computational features. The λ-calculus is the model of computation underlying functional programming languages and proof assistants. Actually there are many λ-calculi, depending on the evaluation mechanism (for instance, call-by-name and call-by-value-CbN and CbV for short) and computational features that the calculus aims to model. In λ-calculi, a rewriting relation formalizes computational steps in program execution, and normal forms are the results of computations. In each calculus, a key question is to define a normalizing strategy: How to compute a result? Is there a reduction strategy which is guaranteed to output a result, if any exists? Proving that a calculus admits a normalizing strategy is complex, and many techniques have been developed. A well-known method first proves factorization [4, 32, 19, 2] . Given a calculus with a rewriting relation − →, a strategy → l ⊆ − → factorizes if − → * ⊆ → l * · → ¬l * ( → ¬l is the dual of → l ), i.e. any reduction sequence can be rearranged so as to perform → l -steps first and then the other steps. If, moreover, the strategy satisfies some "good properties", we can conclude that the strategy is normalizing. Factorization is important also because it is commonly used as a building block in the proof of other properties of the how-to-compute kind. For instance, standardization, which generalizes factorization: every reduction sequences can be rearranged according to a predefined order between redexes. Two for One. CbN and CbV λ-calculi are two distinct rewriting systems. Quoting from Levy [20] : the existence of two separate paradigms (CbN and CbV) is troubling because to prove a certain property-such as factorization or normalizationfor both systems we always need to do it twice. The first aim of our paper is to develop a technique for deriving factorization for both the CbN [4] and CbV [27] λ-calculi as corollaries of a single factorization theorem, and similarly for normalization. A key tool in our study is the bang calculus [11, 15] , a calculus inspired by linear logic in which CbN and CbV embed. The Bang Calculus. The bang calculus is a variant of the λ-calculus where an operator ! plays the role of a marker for non-linear management: duplicability and discardability of resources. The bang calculus is nothing but Simpson's linear λcalculus [31] without linear abstraction, or the untyped version of the implicative fragment of Levy's Call-by-Push-Value [20] , as first observed by Ehrhard [10] . The motivation to study the bang calculus is to have a general framework where both CbN and CbV λ-calculi can be simulated, via two distinct translations inspired by Girard's embeddings [14] of the intuitionistic arrow into linear logic. So, a certain property can be studied in the bang calculus and then automatically transferred to the CbN and CbV settings by translating back. This approach has so far mainly be exploited semantically [21, 10, 11, 15, 9, 7] , but can be used it also to study operational properties [15, 30, 13] . In this paper, we push forward this operational direction. The Least-Level Strategy. We study a strategy from the literature of linear logic [8] , namely least-level reduction → l , which fires a redex at minimal level-the level of a redex is the number of ! under which the redex occurs. We prove that the least-level reduction factorizes and normalizes in the bang calculus, and then we transfer the same results to CbN and CbV λ-calculi (for suitable definitions of least-level in CbN and CbV), by exploiting properties of their translations into the bang calculus. A single proof suffices. It is two-for-one! Or even better, three-for-one. The rewriting study of the least level strategy in the bang calculus is based on simple techniques for factorization and normalization we developed recently with Accattoli [2] , which simplify and generalize Takahashi's method [32] . Subtleties of the Embeddings. Transferring factorization and normalization results via translation is highly non-trivial, e.g. in CPS translations [27] . This applies also to transferring least-level factorization from the bang calculus to the CbN and CbV λ-calculi. To transfer the property smoothly, the translations should preserve levels and normal forms, which is delicate, in particular for CbV. For instance, the embedding of CbV into the bang calculus defined in [15, 30] does not preserve levels and normal forms. As a consequence, the CbV translation studied in [15, 30] cannot be used to derive least-level factorization or any normalization result in a CbV setting from the corresponding result in the bang calculus. Here we adopt the refined CbV embedding of Bucciarelli et al. [7] , which does preserve levels and normal forms. While the preservation of normal forms is already stressed in [7] , the preservation of levels is proved here for the first time, and it is based on non-trivial properties of the embedding. Beyond pure. Our second aim is to show that the developed technique for the joined factorization and normalization of CbN and CbV via the bang calculus is robust. We do so, by studying extensions of all three calculi with operators (or, in general, with extra rules) which model some additional computational features, such as non-deterministic or probabilistic choice. We then show that the technique scales up smoothly, under mild assumptions on the extension. A Motivating Example. Let us illustrate our approach on a simple case, which we will use as a running example. De' Liguoro and Piperno's CbN non-deterministic λ-calculus Λ cbn ⊕ [23] extends the CbN λ-calculus with an operator ⊕ whose reduction → ⊕ models non-deterministic choice: t ⊕ s rewrites to either t or s. It admits a standardization result, from which it follows that the leftmostoutermost reduction strategy (noted → lo β⊕ ) is complete: if t has a normal form u then t → lo β⊕ * u. In [22] , de' Liguoro considers also a CbV variant Λ cbv ⊕ , extending Plotkin CbV λ-calculus [27] with an operator ⊕. One may prove standardization and completeness-again-from scratch, even though the proofs are similar. The approach we propose here is to work in the bang calculus enriched with the operator ⊕. We show that the calculus satisfies least-level factorization, from which it follows that the least-level strategy (noted → l β ! ⊕ ) is complete, i.e. if t has a normal form u, then t → l β ! ⊕ * u. The translation then guarantees that analogous results hold also in Λ cbn ⊕ and Λ cbv ⊕ , without proving them again. The Importance of Being Modular. The bang calculus with operators is actually a general formalism for several calculi, one calculus for each kind of computational feature modeled by operators. Concretely, the reduction → consists of − → β ! (which subsumes CbN − → β and CbV − → βv ) and other reduction rules − → ρ . We decompose the proof of factorization of → in modules, by using the modular approach we recently introduced together with Accattoli [3] . The key module is the least-level factorization of → β ! , because it is where the higher-order comes into play-this is done, once and for all. Then, we consider a generic reduction rule − → ρ to add to − → β ! . Our general result is that if − → ρ has "good properties" and interacts well with − → β ! (which amounts to an easy test, combinatorial in nature), then we have least-level factorization for − → β ! ∪ − → ρ . Putting all together, when − → ρ is instantiated to a concrete reduction (such as → ⊕ ), the user of our method only has to verify a simple test (namely Proposition 34), to conclude that − → β ! ∪ − → ρ has least-level factorization. In particular, factorization for − → β ! is a ready-to-use black box the user need not to worry about-our proof is robust enough to hold whatever the other rules are. Finally, the embeddings automatically give least-level factorization for the corresponding CbV and CbN calculi. Section 7 illustrates our method in the case − → ρ = → ⊕ . Subtleties of the Modular Extensions. To adopt the modular approach for factorization presented in [3] , we have to face an important difficulty that arises when dealing with normalizing strategies, and which is not studied in [3] . A normalizing strategy cannot overlook redexes and it usually selects the redex r to fire through a property that r minimizes with respect to the redexes in the whole term, such as being a least level redex or being the leftmost-outermost (shortened to LO) redex-normalizing strategies are positional. The problem is that, in general, if → = → β ∪ → ρ , then → lo reduction is not the union of → lo β and → lo ρ : the normalizing strategy of the compound system is not obtained putting together the normalizing strategies of the components. Let us explain the issue on our running example → β⊕ , in the familiar case of leftmost-outermost reduction. Example 1. Consider head reductions for → β and for → β⊕ = → β ∪ → ⊕ , noted → h β and → h β⊕ , respectively. In the term s = (II)(x⊕y) where I = λx.x, the subterm II (a β-redex) is in head position for both the reduction → β and its extension → β⊕ . So, s → h β I(x ⊕ y) and s → h β⊕ I(x ⊕ y). And in the term t = (x ⊕ y)(II), the head position is occupied by x ⊕ y, which is a ⊕-redex. Therefore, II is not the head redex in t, neither for β nor for β⊕. In general, → h β⊕ = → h β ∪ → h ⊕ . In contrast, for leftmost-outermost reduction → lo β⊕ , which reduces the lo- The least-level factorization for → β ! , → β , and → βv we prove here is robust enough to make it ready to be used as a module in a larger proof, where it may combine with operators and other rules. The key point is to define the least-level reduction from the very beginning as a reduction firing a redex at minimal level with respect to a general set of redexes (including β ! , β or β v , respectively), so that it is "ready" to be extended with other reduction rules (see Section 4). Proofs. All proofs are available in [12] , the long version of this paper. An (abstract) rewriting system, [33, Ch. 1] is a pair (A, − →) consisting of a set A and a binary relation − → ⊆ A × A (called reduction) whose pairs are written t − → s and called steps. A − →-sequence from t is a sequence of − →-steps. As usual, → * (resp. → = ) denotes the transitive-reflexive (resp. reflexive) closure of →. We say that u is →-normal (or a →-normal form) if there is no t such that u → t. In general, a term may or may not reduce to a normal form. If it does, not all reduction sequences necessarily lead to normal form. A term is weakly or strongly normalizing, depending on if it may or must reduce to normal form. More precisely, a term t is strongly →-normalizing if every maximal →-sequence from t ends in a − →-normal form: any choice of →-steps will eventually lead to a normal form. A term t is weakly →-normalizing if t − → * u for some u →-normal. If t is weakly but not strongly normalizing, how do we compute a normal form? This is the problem tackled by normalization: by repeatedly performing only specific steps, a normal form is eventually reached, provided that t can − →-reduce to any. Definition 2 (Normalizing and complete strategy). A reduction → e ⊆ → is a strategy for → if it has the same normal forms as →. A strategy → e for → is: complete if t → e * u whenever t − → * u with u →-normal; normalizing if every weakly − →-normalizing term is strongly → e -normalizing. Note that if the strategy → e is complete and deterministic (i.e. for every t ∈ A, t → e s for at most one s ∈ A), then → e is a normalizing strategy for →. Informally, a strategy for − → is a way to control the fact that in a term there are different possible choices of a − →-step. A normalizing strategy for → is a strategy that is guaranteed to reach a →-normal form, if it exists, from any term. This provides a useful tool to show that a term is not weakly →-normalizing. Proving Normalization. Factorization means that any →-sequence from a term to another can be rearranged by performing a certain kind of steps first. It provides a simple technique to establish that a strategy is normalizing. Lemma 4 (Normalization [2] ). Let → = → e ∪ → ¬e , and → e be a strategy for →. The strategy → e is complete for → if the following conditions hold: The strategy → e is normalizing for → if it is complete and the following holds: 3. ( uniformity) every weakly → e -normalizing term is strongly → e -normalizing. A sufficient condition for uniformity (and confluence) is the quasi-diamond. Proving Factorization. Hindley [17] first noted that a local property implies factorization. Let → = → e ∪ → i . We say that → i strongly postpones after → e if SP(→ e , → i ) : Lemma 6 (Hindley [17] ). SP(→ e , → i ) implies Fact(→ e , → i ). Strong postponement can rarely be used directly, because several interesting reductions-including β-reduction-do not satisfy it. However, it is at the heart of Takahashi's method [32] to prove head factorization of − → β , via the following immediate property that can also be used to prove other factorizations (see [2] ). The core of Takahashi's method [32] to prove head factorization in the λcalculus is to introduce a relation ⇒ i , called internal parallel reduction, which verifies the conditions of Property 7. We will follow a similar path in Section 6.1, to prove least-level factorization in the bang calculus. Compound systems: proving factorization in a modular way. In this paper, we will consider compound rewriting systems that are obtained by extending the λ-calculus with extra rules to model advanced computational features. In an abstract setting, let us consider a rewrite system (A, →) where → = → ξ ∪ → ρ . Under which condition → admits factorization, assuming that both → ξ and → ρ do? To deal with this question, a technique for proving factorization for compound systems in a modular way has been introduced in [3] . The approach can be seen as an analogous for factorization of the classical technique for confluence based on Hindley-Rosen lemma [4] : if → ξ , → ρ are e-factorizing reductions, their union → ξ ∪ → ρ also is, provided that two local conditions of commutation hold. Lemma 8 (Modular factorization [3] ). Let → ξ = → e ξ ∪ → i ξ and → ρ = → e ρ ∪ → i ρ be e-factorizing relations. Let → e := → e ξ ∪ → e ρ and → i := → i ξ ∪ → i ρ . The reduction → ξ ∪ → ρ fulfills factorization Fact(→ e , → i ) if the following swaps hold: The subtlety here is to set → e ξ and → e ρ so that → e = → e ξ ∪ → e ρ . As already shown in Example 1, when dealing with normalizing strategies one needs extra care. We present here a generic syntax for λ-calculi, possibly containing operators. All the variants of the λ-calculus we shall study use this language. We assume some familiarity with the λ-calculus, and refer to [4, 18] for details. Given a countable set Var of variables, denoted by x, y, z, . . . , terms and values (whose sets are denoted by Λ O and Val, respectively) are defined as follows: where o ranges over a set O of function symbols called operators, each one with its own arity k ∈ N. If the operators are o 1 , . . . , o n , the set of terms is indicated as Λ o1...on . When the set O of operators is empty, the calculus is called pure, and the sets of terms is denoted by Λ; otherwise, the calculus is applied. Terms are identified up to renaming of bound variables, where abstraction is the only binder. We denote by t{s/x} the capture-avoiding substitution of s for the free occurrences of x in t. Contexts (with exactly one hole · ) are generated by the grammar below, and c t stands for the term obtained from the context c by replacing the hole with the term t (possibly capturing free variables). A rule ρ is a binary relation on Λ O ; we also call it ρ-rule and denote it by Given a set of rules Rules, the relation → = ρ − → ρ (for ρ ∈ Rules) can equivalently be defined as the contextual closure of → = ρ → ρ . Pure CbN and Pure CbV λ-calculi. The pure call-by-name (CbN for short) λcalculus [4, 18] is (Λ, → β ), the set of terms Λ together with the β-reduction → β , defined as the contextual closure of the usual β-rule, which we recall in (1) below. The pure call-by-value (CbV for short) λ-calculus [27] is the set Λ endowed with the reduction − → βv , defined as the contextual closure of the β v -rule in (2) . CbN and CbV λ-calculi. A CbN (resp. CbV ) λ-calculus is the set of terms endowed with a reduction − → which extends → β (resp. → βv ). In particular, the applied setting with operators (when O = ∅) models in the λ-calculus richer computational features, allowing o-reductions as the contextual closure of o-rules of the form o(t 1 , . . . , t k ) → o s. where ⊕ is a binary operator; let → ⊕ be the contextual closure of the (non-deterministic) rule below: The non-deterministic CbN λ-calculus Λ cbn The bang calculus [11, 15] is a variant of the λ-calculus inspired by linear logic. An operator ! plays the role of a marker for duplicability and discardability. Here we allow also the presence of operators other than !, ranging over a set O. So, terms and contexts of the bang calculus (denoted by capital letters) are: Terms of the form !T are called boxes and their set is denoted by !Λ !O . When there are no operators other than ! (i.e. O = ∅), the set of terms and the set of boxes are denoted by Λ ! and !Λ ! , respectively. This syntax can be expressed in the one at the beginning of Section 3, where ! is an unary operator called bang. The pure bang calculus. The pure bang calculus (Λ ! , → β ! ) is the set of terms Λ ! endowed with reduction − → β ! , the closure under contexts in C ! of the β ! -rule: Intuitively, in the bang calculus the bang-operator ! marks the only terms that can be erased and duplicated. Indeed, a β-like redex (λx.T )S can be fired by → β ! only when its argument S is a box, i.e. S = !R: if it is so, the content R of the box S (and not S itself) replaces any free occurrence of x in T . 3 A proof of confluence of β ! -reduction − → β ! is in [15] . We use the following notations to denote some notable terms. Remark 11 (Notable terms). The term I = λx.!x plays the role of the identity in the bang calculus: I !T − → β ! !(x{T /x}) = !T for any term T . Instead, the term ι = λx.x, when applied to a box !T , opens the box, i.e. returns its content T : Our motivation to study the bang calculus is to have a general framework where both CbN [4] and CbV [27] λ-calculi can be embedded, via two distinct translations. Here we show how these translations work. We extend the simulation results in [15, 30, 7] for the pure case to the case with operators (Proposition 13). Following [7] , the CbV translation defined here differs from [15, 30] in the application case. Section 5 will show why this optimization is crucial. CbN and CbV translations are two maps (·) n : respectively, translating terms of the λ-calculus into terms of the bang calculus: . . . , t k )) n = o(t n 1 , . . . , t n k ) (ts) n = t n !s n ; Example 12. Consider the λ-term ω := δδ: then, δ n = ∆, δ v = !∆ and ω n = ∆ !∆ = ω v (δ and ∆ are defined in Notation 10). The λ-term ω is diverging in CbN and CbV λ-calculi, and so is ω n = ω v in the bang calculus, see Remark 11. For any term t ∈ Λ O , t n and t v are just different decorations of t by means of the bang-operator ! (recall that ι = λx.x). The translation (·) n puts the argument of any application into a box: in CbN any term is duplicable or discardable. On the other hand, only values (i.e. abstractions and variables) are translated by (·) v into boxes, as they are the only terms duplicable or discardable in CbV. As in [15, 30] , we prove that the CbN translation (·) n (resp. CbV translation (·) v ) from the pure CbN (resp. CbV) λ-calculus into the bang calculus is sound and complete: it maps β-reductions (resp. β v -reductions) of the λ-calculus into β !reductions of the bang calculus, and conversely β ! -reductions -when restricted to the image of the translation -into β-reductions (resp. Proposition 13 (Simulation of CbN and CbV). Let t ∈ Λ O and o ∈ O. CbN completeness: CbV completeness: The bang calculus Λ ! has a natural normalizing strategy, derived from linear logic [8] , namely the least-level reduction. It reduces only redexes at least level, where the level of a redex R in a term T is the number of bangs ! in which R is nested. Least-level reduction is easily extended to a general bang calculus (Λ !O , − →). The level of a redex R is then the number of bangs ! and operators o in which R is nested; intuitively, least-level reduction fires a redex which is minimally nested. Below, we formalize the reduction in a way that is independent of the specific shape of the redexes, and even of specific definition of level one chooses. The interest of least-level reduction is in the properties it satisfies. All our developments will rely on such properties, rather than the specific definition of least level. In this section, → = ρ − → ρ for ρ ∈ Rules (for a generic set of rules Rules). We write R = ρ R ρ (again, with ρ ∈ Rules) for the set of all redexes. The level of a redex occurrence R in a term T is a measure of its depth. Formally, we indicate the occurrence of a subterm R in T with the context C such that C R = T . Its level is then the level (C) ∈ N of the hole in C. The definition of level for contexts in a bang calculus Λ !O is formalized as follows. Note that the level increases by 1 in the scope of !, and of any operator o ∈ O. A reduction step T − → ρ S is at level k if it fires a ρ-redex at level k ∈ N; it is least-level if it reduces a redex whose level is minimal. The least level (T ) of a term T expresses the minimal level of any redex occurrences in T ; if no redex is in T , we set (T ) = ∞. Formally: Definition 15 (Least-level reduction). Let → = ρ → ρ (for ρ ∈ Rules) and R = ρ R ρ the set of redexes. Given a function (·) from contexts to N: -The least level of a term T is defined as 4 (T ) := inf{ (C) | T = C R for some R ∈ R} ∈ (N ∪ {∞}). -A ρ-reduction step T − → ρ S is: -Internal reduction is → ¬l = ρ → ¬l ρ (for ρ ∈ Rules). Note that → = → l ∪ → ¬l and that our definitions solve the issue of Example 1. Indeed, the definition of least level (T ) of a term, and hence the definition of → l ρ , depend on the whole set R = ρ R ρ of redexes associated with →. 5 4 Recall that inf ∅ = ∞, when ∅ is seen as the empty subset of N with the usual order. 5 We should write R (T ), lR and → l R ρ, but we avoid it for the sake of readability. Normal Forms. It is immediate that → l → is a strategy for →. Indeed, → l and → have the same normal forms because → l ⊆ → and if a term has a →-redex, it has a redex at least-level, i.e. it has a → l -redex. is →-normal, because (C) ∈ N for all contexts C. A good least-level reduction. The beauty of least-level reduction for the bang calculus, is that it satisfies some elegant properties, which allow for neat proofs, in particular monotonicity and internal invariance (in Definition 17). The developments in the rest of the paper rely on such properties, and in fact will apply to any calculus whose reduction → has the properties described below. Point 1 states that no step can decrease the least level of a term. Point 2 says that internal steps cannot change the least level of a term. Therefore, only leastlevel steps may increase the least level. Together, they imply persistence: only least-level steps can approach normal forms. If → has a good least-level, then T → ¬l S implies that S is not →-normal. Reduction → β ! in the pure bang calculus (Λ ! , → β ! ) has a good least-level. More in general, the same holds when extending the reduction with operators. has a redex of shape o(P 1 , . . . , P k ). The reduction → has a good least-level. Let us see more closely the least-level reduction for a bang calculus (Λ !O , − →). For concreteness, we consider Rules = {β ! , o | o ∈ O}, hence the set of redexes is We observe that the least level (T ) of a term T ∈ Λ !O can be easily defined in a direct way, by induction on T : Intuitively, least-level reduction fires a redex that is minimally nested, where a redex is any subterm whose form is in R = R β ! ∪ R O . Note that least-level reduction can choose to fire one among possibly several redexes at minimal level. . In (λz.S)!S, two least-level steps are possible (the fired β ! -redex is underlined): (λz.S)!S → l β ! ι !(S !S), and (λz.S)!S → l β ! (λz.z !z)!S. But (λz.S)!S → l β ! (λz.S)!(z !z) although (λz.S)!S → β ! (λz.S)!(z !z). The definition of least-level reduction in Section 4.1 is independent of the specific notion of level chosen, and of the specific calculus. The idea is that the reduction strategy persistently fires a redex at minimal level, once such a notion is set. Least-level reduction can indeed be defined also for the CbN and CbV λcalculi, given an opportune definition of level. In CbN, we count the number of nested arguments and operators containing the redex occurrence. In CbV, we count the number of nested operators and unapplied abstractions containing the redex occurrence, where an abstraction is unapplied if it is not the right-hand side of an application. Formally, a redex occurrence is identified by a context (as explained in Section 4.1), and we define the level CbN (c) ∈ N and CbV (c) ∈ N of a context c in CbN and CbV λ-calculi, respectively, as follows. In both CbN and CbV λ-calculi, the least level of a term (denoted by CbN (·) and CbV (·)) and least-level and internal reductions are given by Definition 15 (replace (·) with CbN (·) for CbN, and with CbV (·) for CbV). In Section 5 we will see that the definitions of CbN and CbV least level are not arbitrary, but induced by the CbN and CbV translations defined in Section 3.3. Here we refine the analysis of the CbN and CbV translations given in Section 3.3, by showing two new results: translations preserve normal forms (Proposition 22) and least-level (Proposition 25), back and forth. This way, to obtain least-level factorization or least-level normalization results, it suffices to prove them in the bang calculus. The translation transfers the results into the CbN and CbV λ-calculi (Theorem 26). We use here the expression "translate" in a strong sense: the results for CbN and CbV λ-calculi are obtained from the corresponding results in the bang calculus almost for free, just via CbN and CbV translations. Preservation of normal forms. The targets of the CbN translation (·) n and CbV translation (·) v into the bang calculus can be characterized syntactically. A fine analysis of these fragments of the bang calculus (see [12] for details) proves that both CbN and CbV translations preserve normal forms, back and forth. Proposition 22 (Preservation of normal forms). Let t, s ∈ Λ O and o ∈ O. By Remark 16, Proposition 22 can be seen as the fact that CbN and CbV translations preserve the least-level of a term, back and forth, when the least-level is infinite. Actually, this holds more in general for any value of the least-level. Preservation of levels. We aim to show that least-level steps in CbN and CbV λ-calculi correspond to least-level steps in the bang calculus-back and forth-via CbN and CbV translations, respectively (Proposition 25). This result is subtle, one of the main technical contributions of this paper. First, we extend the definition of translations to contexts. The CbN and CbV translations for contexts are two functions (·) n : C − → C ! and (·) v : C − → C ! , respectively, mapping contexts of the λ-calculus into contexts of the bang calculus: (o(t1, ..., c, ..., t k )) n = o(t n 1 , ..., c n , ..., t n k ) (o(t1, ..., c, .. Note that CbN (resp. CbV) level of a context defined in Section 4.3 increases by 1 whenever the CbN (resp. CbV) translation for contexts adds a !. Thus, CbN and CbV translations preserve, back and forth, the level of a redex and the least-level of a term. Said differently, the level for CbN and CbV is defined in Section 4.3 so as to enable the preservation of level via CbN and CbV translations. For least-level of a term: For any term t ∈ Λ O , one has CbN (t) = (t n ). 1. For contexts: For any context c ∈ C, one has CbV (c) = (c v ). From the two lemmas above it follows that CbN and CbV translations preserve least-level and internal reductions, back and forth. Let t ∈ Λ O and o ∈ O. As a consequence, least-level reduction induces factorization in CbN and CbV λ-calculi as soon as it does in the bang calculus. And, by Proposition 22, it is a normalizing strategy in CbN and CbV as soon as it is so in the bang calculus. A similar result will hold also when extending the pure calculi with a rule → ρ other than → o , as long as the translation preserves ρ-redexes, back and forth. Remark 27 (Preservation of least-level and of normal forms). Preservation of normal form and least-level is delicate. For instance, it does not hold with the definition CbV translation (·) v in [15, 30] . There, the translation t = rs ∈ Λ would be t v = (ι !(r v ))s v and then Proposition 22 and Proposition 25 would not hold: Remark 11) and hence t v would not be normal even though so is t, and (t v ) = 0 even though CbV (t) = 0. This is why we defined two distinct case when defining (·) v for applications, akin to Bucciarelli et al. [7] . We have shown that least-level factorization in a bang calculus Λ !O implies leastlevel factorization in the corresponding CbN and CbV calculi, via forth-and-back translation. The central question now is how to prove least-level factorization for a bang calculus: this section is devoted to that, in the pure and applied cases. Overview. Let us overview our approach by considering O = {o}, and → = → β ! ∪ → o . Since by definition → l = → l β ! ∪ → l o (and → ¬l = → ¬l β ! ∪ → ¬l o ), Lemma 8 states that we can decompose least-level factorization of → in three modules: prove the two linear swaps of Lemma 8. Note that, for each of → l β ! and → l o , the least level is defined with respect to the set of all redexes R = R β ! ∪ R o , so as to have → l = → l β ! ∪ → l o . This approach solves the issue we mentioned in Example 1. Clearly, Points 2 and 3 depend on the specific rule → o . However, the beauty of a modular approach is that Point 1 can be established in general: we do not need to know → o , only the shape of its redexes given by R o . In Section 6.1 we provide a general result of least-level factorization for → β ! (Theorem 28). In fact, we shall show a bit more: the way of decomposing the study of factorization that we have sketched, can be applied to study least-level factorization of any reduction → = → β ! ∪ → ρ , as long as → has a good least-level. Once (1) is established (once and for all), to prove factorization of a reduction → β ! ∪ → o we are only left with (2) and (3). In Section 6.3 we show that the proof of the two linear swaps can be reduced to a single, simple test, involving only the → o step (Proposition 34). In Section 7, we will illustrate how all elements play together on a concrete case, applying them to non-deterministic λ-calculi. We show that → β ! factorizes via least-level reduction (Theorem 28). This holds for a definition of → l β ! (as in Section 4) where the set of redexes R contains R β ! ∪ R O -this generalization has essentially no cost, and allows us to use Theorem 28 as a module in the factorization of larger reductions containing → β ! . We prove factorization via Takahashi's parallel reduction method [32] . We define a reflexive reduction ⇒ ¬l β ! (called parallel internal β ! -reduction) which fulfills the conditions of Property 7, i.e. The tricky point is to prove that ⇒ ¬l β ! · → l β ! ⊆ → l β ! * · ⇒ ¬l β ! We adapt the proof technique in [2] . All details are in [12] . Here we just give the definition of ⇒ ¬l β ! . We first introduce ⇒ β ! :n with n ∈ N ∪ {∞} (the parallel version of − → β ! :n ), which fires simultaneously a number of β ! -redexes at level at least n ∈ N, and ⇒ β ! :∞ does not reduce any β ! -redex: T ⇒ β ! :∞ S implies T = S. The parallel internal β ! -reduction ⇒ ¬l β ! is the parallel version of → ¬l β ! , which fires simultaneously a number of β ! -redexes that are not at minimal level. Formally, T ⇒ ¬l β ! S if T ⇒ β ! :n S with n = ∞ or n > (T ). Theorem 28 (Least-level factorization of → β ! ). Let → ρ be the contextual closure of a rule → ρ , and assume that → = → β ! ∪ → ρ has good least-level in Λ !O . In particular, as − → β ! has a good least-level (Proposition 19) in Λ ! , we have: Corollary 29 (Least-level factorization in the pure bang calculus). In the pure bang calculus Surface Digression. According to Definition 15, β ! -reduction − → β ! :0 at level 0 (called surface reduction in Simpson [31] ) can only fire redexes at level 0, i.e., redexes that are not inside boxes or other operators. It can be equivalently defined as the closure of → β ! under contexts S defined by S : Least-level factorization of → β ! implies in particular least-level factorization for → β and → βv . As a consequence, least-level reduction is a normalizing strategy for all three pure calculi: the bang calculus, the CbN, and the CbV λ-calculi. The pure bang calculus. The least-level reduction → l β ! is a normalizing strategy for → β ! . Indeed, it satisfies all ingredients in Lemma 4. Since we have least-level factorization (Corollary 29), same normal forms, and persistence (Proposition 19), → l β ! is a complete strategy for → β ! : if T → * β ! S and S is β ! -normal, then T → l β ! * S. We already observed (Example 21) that the least-level reduction → l β ! is non-deterministic, because several redexes at least level may be available. Such non-determinism is however harmless and inessential, because → l β ! is uniform. Lemma 31 (Quasi-Diamond). In the pure bang calculus (Λ ! , − → β ! ), the reduction → l β ! is quasi-diamond (Property 5), and therefore uniform. Putting all the ingredients together, we have (by Lemma 4): Theorem 32 (Least-level normalization). In the pure bang calculus (Λ ! , − → β ! ), the least-level reduction → l β ! is a normalizing strategy for → β ! . Theorem 32 means not only that if T is weakly β ! -normalizing then T can reach its normal form by just performing least-level steps, but also that performing whatever least-level steps eventually leads to the normal form, if any. Pure CbV and CbN λ-calculi. By forth-and-back translation (Theorem 26) the least-level factorization and normalization results for the pure bang calculus immediately transfers to the (pure) CbN and CbV settings. Theorem 33 (CbV and CbN least-level normalization). -CbN: In (Λ, → β ), → l β is a normalizing strategy for → β . -CbV: In (Λ, → βv ), → l βv is a normalizing strategy for → βv . Least-level factorization of → β ! (Theorem 28) can be used to prove factorization for a more complex calculus. Indeed, a simple and modular test establishes least-level factorization of a reduction → β ! ∪ → ρ (→ ρ is a reduction added to → β ! ), by adapting a similar result in [3] . The test relies on the fact that we have already proved Theorem 28, and it simplifies Lemma 8: the proof of the two linear swaps of Lemma 8 is reduced to a single, easier check, which only involves the rule → ρ . As usual, the least level in → l β ! and → l ρ is defined with respect to the set R = R β ! ∪ R ρ of redexes. An example of the use of this test is in Section 7. Proposition 34 (Modular test for least-level factorization). Let → ρ be the contextual closure of a rule → ρ , and assume that → = → β ! ∪ → ρ has a good least-level in Λ !O . Then → factorizes via → l = → l β ! ∪ → l ρ if the following hold: 2. ( substitutivity of → ρ ) R → ρ R implies R{T /x} → ρ R {T /x}; 3. ( root linear swap) → ¬l β ! · → ρ ⊆ → ρ · → * β ! . To show how to use our framework, we apply the tools we have developed on our running example (see Examples 1 and 9). We extend the bang calculus with a nondeterministic binary operator ⊕, that is, (Λ !⊕ , → β ! ⊕ ) where → β ! ⊕ = → β ! ∪ → ⊕ , and → ⊕ is the contextual closure of the (non-deterministic) rules: First step: non-deterministic bang calculus. We analyze Λ !⊕ . We use our modular test to prove least-level factorization for Λ !⊕ : if T → * β ! ⊕ U then T → l β ! ⊕ * · → ¬l β ! ⊕ * U . By Lemma 4, an immediate consequence of the factorization result is that the least-level strategy is complete: if U is normal, T → * β ! ⊕ U implies T → l β⊕ * U . Second step: CbN and CbV non-deterministic calculi. By translation, we have for free, that the analogous results hold in Λ cbn ⊕ and Λ cbv ⊕ , as defined in Example 9. So, least-level factorization holds for both calculi, and moreover -CbN completeness: in Λ cbn ⊕ , if u is normal, t → * β⊕ u implies t → l β⊕ * u. -CbV completeness: in Λ cbv ⊕ , if u is normal, t → * βv⊕ u implies t → l βv⊕ * u. What do we really need to prove? The only result we need to prove is leastlevel factorization of → β ! ⊕ . Completeness then follows by Lemma 4 and the translations will automatically take care of transferring the results. To prove factorization of → β ! ⊕ , most of the work is done, since least-level factorization of → β ! is already established; we then use our test (Proposition 34) to extend → β ! with → ⊕ . The only ingredients we need are substitutivity of → ⊕ (which is an obvious property), and the following easy lemma. Lemma 35 (Roots). Let ρ ∈ {β ! , ⊕}. If T → ¬l ρ R → ⊕ S then T → ⊕ · → = ρ S. Theorem 36 (Least-level factorization in non-deterministic calculi). 1. In (Λ !⊕ , − →), Fact(→ l , → ¬l ) holds for → = → ⊕ ∪ → β ! . 2. Least-level factorization holds in (Λ cbn ⊕ , → ⊕ ∪ → β ), and in (Λ cbv ⊕ , → ⊕ ∪ → βv ). Completeness is the best that can be achieved in these calculi, because of the true non-determinism of → ⊕ and hence of least-level reduction and of any other complete strategy for − →. For instance, in Λ cbn ⊕ there is no normalizing strategy for ⊕(x, δδ) in the sense of Definition 2, since x ← l ⊕ ⊕(x, δδ) → l ⊕ δδ → l β . . . . Combining translations (Theorem 26), least-level factorization for → β ! (Theorem 28), and modularity (Proposition 34), gives us a powerful method to analyze factorization in various λ-calculi that extend the pure CbN and CbV calculi. The main novelty is transferring the results from a calculus to another via translations. Related Work. Many calculi inspired by linear logic subsume CbN and CbV, such as [5, 6, 29, 24] (other than the ones already cited). We chose the bang calculus for its simplicity, which eases the analysis of the CbN and CbV translations. To study CbN and CbV in a uniform way, an approach orthogonal to ours is given by Ronchi della Rocca and Paolini's parametric λ-calculus [28] . It is a meta-calculus, where the reduction rule is parametric with respect to a subset of terms (called values) with suitable properties. Different choices for the set of values define different calculi-that is, different reductions. This allows for a uniform presentation of proof arguments, such as the proof of standardization, which is actually a meta-proof that can be instantiated in both CbN and CbV. Least-level reduction is studied for calculi based on linear-logic in [34, 1] and for linear logic proof-nets in [8, 26] . It is studied for pure CbN λ-calculus in [2] . An Abstract Factorization Theorem for Explicit Substitutions Leibniz International Proceedings in Informatics (LIPIcs) Factorization and normalization, essentially Factorize factorization The Lambda Calculus: Its Syntax and Semantics A term calculus for intuitionistic linear logic Linear logic, monads and the lambda calculus The bang calculus revisited A semantic measure of the execution time in linear logic Taylor expansion for Call-By-Push-Value Call-by-push-value from a linear logic point of view The bang calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value Factorization in call-by-name and call-by-value calculi via linear logic (long version) Lambda calculus and probabilistic computation Linear logic The bang calculus and the two Girard's translations Categorifying non-idempotent intersection types The Church-Rosser Property and a Result in Combinatory Logic Introduction to Combinators and Lambda-Calculus Leftmost Outermost Revisited Leibniz International Proceedings in Informatics (LIPIcs) Call-by-push-value: A subsuming paradigm Call-by-push-value: Decomposing call-by-value and call-by-name Non-deterministic untyped λ-calculus. A study about explicit non determinism in higher-order functional calculi Call-by-name, call-by-value, call-by-need and the linear lambda calculus On theories with a combinatorial definition of equivalence The conservation theorem for differential nets Call-by-name, call-by-value and the lambda-calculus The Parametric Lambda Calculus -A Metamodel for Computation Lambda calculus and intuitionistic linear logic Modal embeddings and calling paradigms Reduction in a linear lambda-calculus with applications to operational semantics Parallel reductions in lambda-calculus Term Rewriting Systems Light affine lambda calculus and polynomial time strong normalization ), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use Acknowledgments. The authors thank Beniamino Accattoli for insightful comments and discussions. This work was partially supported by EPSRC Project EP/R029121/1 Typed Lambda-Calculi with Sharing and Unsharing.