Beniamino Accattoli
email: accattoli@inria.fr

Giulio Guerrieri
email: giulio.guerrieri@univ-amu.fr

Open Call-by-Value

come

Introduction

Plotkin's call-by-value λ-calculus [START_REF] Plotkin | Call-by-Name, Call-by-Value and the lambda-Calculus[END_REF] is at the heart of programming languages such as OCaml and proof assistants such as Coq. In the study of programming languages, call-by-value (CBV) evaluation is usually weak, i.e. it does not reduce under abstractions, and terms are assumed to be closed. These constraints give rise to a beautiful theory-let us call it Closed CBV -having the following harmony property, that relates rewriting and normal forms:

Closed normal forms are values (and values are normal forms) where values are variables and abstractions. Harmony expresses a form of internal completeness with respect to unconstrained β-reduction: the restriction to CBV β-reduction (referred to as β v -reduction, according to which a β-redex can be fired only when the argument is a value) has an impact on the order in which redexes are evaluated, but evaluation never gets stuck, as every β-redex will eventually become a β v -redex and be fired, unless evaluation diverges.

It often happens, however, that one needs to go beyond the perfect setting of Closed CBV by considering Strong CBV, where reduction under abstractions is allowed and terms may be open, or the intermediate setting of Open CBV, where evaluation is weak but terms are not necessarily closed. The need arises, most notably, when trying to describe the implementation model of Coq [START_REF] Grégoire | A compiled implementation of strong reduction[END_REF], but also from other motivations, as denotational semantics [START_REF] Paolini | Call-by-value Solvability[END_REF][START_REF] Della Rocca | The Parametric λ-Calculus[END_REF][START_REF] Accattoli | Call-by-Value Solvability, revisited[END_REF][START_REF] Carraro | A Semantical and Operational Account of Call-by-Value Solvability[END_REF], monad and CPS translations and the associated equational theories [START_REF] Moggi | Computational λ-Calculus and Monads[END_REF][START_REF] Sabry | Reasoning about Programs in Continuation-Passing Style[END_REF][START_REF] Sabry | A Reflection on Call-by-Value[END_REF][START_REF] Dyckhoff | Call-by-Value lambda-calculus and LJQ[END_REF][START_REF] Herbelin | An operational account of Call-by-Value Minimal and Classical λ-calculus in Natural Deduction form[END_REF], bisimulations [START_REF] Lassen | Eager Normal Form Bisimulation[END_REF], partial evaluation [START_REF] Jones | Partial Evaluation and Automatic Program Generation[END_REF], linear logic proof nets [2], or cost models [START_REF] Accattoli | On the Relative Usefulness of Fireballs[END_REF].

Naïve Open CBV. In call-by-name (CBN) turning to open terms or strong evaluation is harmless because CBN does not impose any special form to the arguments of β-redexes. On the contrary, turning to Open or Strong CBV is delicate. If one simply considers Plotkin's weak β v -reduction on open terms-let us call it Naïve Open CBV -then harmony does no longer hold, as there are open β-normal forms that are not values, e.g. xx, x(λy.y), x(yz) or xyz. As a consequence, there are stuck β-redexes such as (λy.t)(xx), i.e. β-redexes that will never be fired because their argument is normal, but it is not a value, nor will it ever become one. Such stuck β-redexes are a disease typical of (Naïve) Open CBV, but they spread to Strong CBV as well (also in the closed case), because evaluating under abstraction forces to deal with locally open terms: e.g. the variable x is locally open with respect to (λy.t)(xx) in s = λx.((λy.t)(xx)).

The real issue with stuck β-redexes is that they prevent the creation of other redexes, and provide premature β v -normal forms. The issue is serious, as it can affect termination, and thus impact on notions of observational equivalence. Let δ := λx.(xx). The problem is exemplified by the terms t and u in Eq. ( 1) below.

t := ((λy.δ)(zz))δ u := δ((λy.δ)(zz))

In Naïve Open CBV, t and u are premature β v -normal forms because they both have a stuck β-redex forbidding evaluation to keep going, while one would expect them to behave like the divergent term Ω := δδ (see [START_REF] Paolini | Call-by-value Solvability[END_REF][START_REF] Della Rocca | The Parametric λ-Calculus[END_REF][START_REF] Accattoli | Call-by-Value Solvability, revisited[END_REF]2,[START_REF] Carraro | A Semantical and Operational Account of Call-by-Value Solvability[END_REF][START_REF] Guerrieri | Standardization of a Call-By-Value Lambda-Calculus[END_REF] and pp. [START_REF] Blelloch | Parallelism in Sequential Functional Languages[END_REF][START_REF] Carraro | A Semantical and Operational Account of Call-by-Value Solvability[END_REF][START_REF] Curien | The duality of computation[END_REF][START_REF] Curien | The Duality of Computation under Focus[END_REF][START_REF] Dal Lago | The weak lambda calculus as a reasonable machine[END_REF][START_REF] Dyckhoff | Call-by-Value lambda-calculus and LJQ[END_REF].

Open CBV. In his seminal work, Plotkin already pointed out an asymmetry between CBN and CBV: his CPS translation is sound and complete for CBN, but only sound for CBV. This fact led to a number of studies about monad, CPS, and logical translations [START_REF] Moggi | Computational λ-Calculus and Monads[END_REF][START_REF] Sabry | Reasoning about Programs in Continuation-Passing Style[END_REF][START_REF] Sabry | A Reflection on Call-by-Value[END_REF][START_REF] Maraist | Call-by-name, Call-by-value, Call-by-need and the Linear λ-Calculus[END_REF][START_REF] Dyckhoff | Call-by-Value lambda-calculus and LJQ[END_REF][START_REF] Herbelin | An operational account of Call-by-Value Minimal and Classical λ-calculus in Natural Deduction form[END_REF] that introduced many proposals of improved calculi for CBV. Starting with the seminal work of Paolini and Ronchi Della Rocca [START_REF] Paolini | Call-by-value Solvability[END_REF]23,[START_REF] Della Rocca | The Parametric λ-Calculus[END_REF], the dissonance between open terms and CBV has been repeatedly pointed out and studied per se via various calculi [START_REF] Grégoire | A compiled implementation of strong reduction[END_REF][START_REF] Accattoli | Call-by-Value Solvability, revisited[END_REF]2,[START_REF] Carraro | A Semantical and Operational Account of Call-by-Value Solvability[END_REF][START_REF] Guerrieri | Standardization of a Call-By-Value Lambda-Calculus[END_REF][START_REF] Guerrieri | Head reduction and normalization in a call-by-value lambda-calculus[END_REF][START_REF] Accattoli | On the Relative Usefulness of Fireballs[END_REF]. A further point of view on CBV comes from the computational interpretation of sequent calculus due to Curien and Herbelin [START_REF] Curien | The duality of computation[END_REF]. An important point is that the focus of most of these works is on Strong CBV. These solutions inevitably extend β v -reduction with some other rewriting rule(s) or constructor (as let-expressions) to deal with stuck β-redexes, or even go as far as changing the applicative structure of terms, as in the sequent calculus approach. They arise from different perspectives and each one has its pros and cons. By design, these calculi (when looked at in the context of Open CBV) are never observationally equivalent to Naïve Open CBV, as they all manage to (re)move stuck β-redexes and may diverge when Naïve Open CBV is instead stuck. Each one of these calculi, however, has its own notion of evaluation and normal form, and their mutual relationships are not evident.

The aim of this paper is to draw the attention of the community on Open CBV. We believe that it is somewhat deceiving that the mainstream operational theory of CBV, however elegant, has to rely on closed terms, because it restricts the modularity of the framework, and raises the suspicion that the true essence of CBV has yet to be found. There is a real gap, indeed, between Closed and Strong CBV, as Strong CBV cannot be seen as an iteration of Closed CBV under abstractions because such an iteration has to deal with open terms. To improve the implementation of Coq [START_REF] Grégoire | A compiled implementation of strong reduction[END_REF], Grégoire and Leroy see Strong CBV as the iteration of the intermediate case of Open CBV, but they do not explore its theory. Here we exalt their point of view, providing a thorough operational study of Open CBV. We insist on Open CBV rather than Strong CBV because: 1. Stuck β-redexes and premature β v -normal forms already affect Open CBV; 2. Open CBV has a simpler rewriting theory than Strong CBV; 3. Our previous studies of Strong CBV in [START_REF] Accattoli | Call-by-Value Solvability, revisited[END_REF] and [START_REF] Carraro | A Semantical and Operational Account of Call-by-Value Solvability[END_REF] naturally organized themselves as properties of Open CBV that were lifted to Strong CBV by a simple iteration under abstractions.

Our contributions are along two axes: 1. Termination Equivalence of the Proposals: we show that the proposed generalizations of Naïve Open CBV are all equivalent, in the sense that they have exactly the same sets of normalizing and diverging terms. So, there is just one notion of Open CBV, independently of its specific syntactic incarnation. 2. Quantitative Analyses and Cost Models: the termination results are complemented with quantitative analyses establishing precise relationships between the number of steps needed to evaluate a given term in the various calculi. In particular, we relate the cost models of the various proposals.

The Fab Four. We focus on four proposals for Open CBV, as other solutions, e.g. Moggi's [START_REF] Moggi | Computational λ-Calculus and Monads[END_REF] or Herbelin and Zimmerman's [START_REF] Herbelin | An operational account of Call-by-Value Minimal and Classical λ-calculus in Natural Deduction form[END_REF], are already known to be equivalent to these ones (see the end of Sect. 2):

1. The Fireball Calculus λ fire , that extends values to fireballs by adding so-called inert terms in order to restore harmony-it was introduced without a name by Paolini and Ronchi Della Rocca [START_REF] Paolini | Call-by-value Solvability[END_REF][START_REF] Della Rocca | The Parametric λ-Calculus[END_REF], then rediscovered independently first by Leroy and Grégoire [START_REF] Grégoire | A compiled implementation of strong reduction[END_REF] to improve the implementation of Coq, and then by Accattoli and Sacerdoti Coen [START_REF] Accattoli | On the Relative Usefulness of Fireballs[END_REF] to study cost models; 2. The Value Substitution Calculus λ vsub , coming from the linear logic interpretation of CBV and using explicit substitutions and contextual rewriting rules to circumvent stuck β-redexes-it was introduced by Accattoli and Paolini [START_REF] Accattoli | Call-by-Value Solvability, revisited[END_REF] and it is a graph-free presentation of proof nets for the CBV λ-calculus [2]; 3. The Shuffling Calculus λ shuf , that has rules to shuffle constructors, similar to Regnier's σ-rules for CBN [START_REF] Regnier | Une équivalence sur les lambda-termes[END_REF], as an alternative to explicit substitutions-it was introduced by Carraro and Guerrieri [START_REF] Carraro | A Semantical and Operational Account of Call-by-Value Solvability[END_REF] (and further analyzed in [START_REF] Guerrieri | Standardization of a Call-By-Value Lambda-Calculus[END_REF][START_REF] Guerrieri | Head reduction and normalization in a call-by-value lambda-calculus[END_REF]) to study the adequacy of Open/Strong CBV with respect to denotational semantics related to linear logic. 4. The Value Sequent Calculus λ vseq , i.e. the intuitionistic fragment of Curien and Herbelin's λμ-calculus [START_REF] Curien | The duality of computation[END_REF], that is a CBV calculus for classical logic providing a computational interpretation of sequent calculus rather than natural deduction (in turn a fragment of the λµμ-calculus [START_REF] Curien | The duality of computation[END_REF], further studied in e.g. [START_REF] Ariola | Sequent calculi and abstract machines[END_REF][START_REF] Curien | The Duality of Computation under Focus[END_REF]).

A Robust Cost Model for Open CBV. The number of β v -steps is the canonical time cost model of Closed CBV, as first proved by Blelloch and Greiner [START_REF] Blelloch | Parallelism in Sequential Functional Languages[END_REF][START_REF] Sands | Lambda Calculi and Linear Speedups[END_REF][START_REF] Dal Lago | The weak lambda calculus as a reasonable machine[END_REF].

In [START_REF] Accattoli | On the Relative Usefulness of Fireballs[END_REF], Accattoli and Sacerdoti Coen generalized this result: the number of steps in λ fire is a reasonable cost model for Open CBV. Here we show that the number of steps in λ vsub and λ vseq are linearly related to the steps in λ fire , thus providing reasonable cost models for these incarnations of Open CBV. As a consequence, complexity analyses can now be smoothly transferred between λ fire , λ vsub , and λ vseq . Said differently, our results guarantee that the number of steps is a robust cost model for Open CBV, in the sense that it does not depend on the chosen incarnation. For λ shuf we obtain a similar but strictly weaker result, due to some structural difficulties suggesting that λ shuf is less apt to complexity analyses.

On the Value of The Paper. While the equivalences showed here are new, they might not be terribly surprising. Nonetheless, we think they are interesting, for the following reasons: A longer version of this paper is available on Arxiv [3]. It contains two Appendices, one with a glossary of rewriting theory and one with omitted proofs. Naïve Open CBV: Plotkin's calculus λ Plot [START_REF] Plotkin | Call-by-Name, Call-by-Value and the lambda-Calculus[END_REF]. Naïve Open CBV is Plotkin's weak CBV λ-calculus λ Plot on possibly open terms, defined in Fig. 1. Our presentation of the rewriting is unorthodox because we split β v -reduction into two rules, according to the kind of value (abstraction or variable). The set of terms is denoted by Λ. Terms (in Λ) are always identified up to α-equivalence and the set of the free variables of a term t is denoted by fv(t). We use t{x u} for the term obtained by the capture-avoiding substitution of u for each free occurrence of x in t. Evaluation → βv is weak and non-deterministic, since in the case of an application there is no fixed order in the evaluation of the left and right subterms.

As it is well-known, non-determinism is only apparent: the system is strongly confluent (see the appendix in [3] for a glossary of rewriting theory).

Proposition 1. → βy , → β λ and → βv are strongly confluent.

Strong confluence is a remarkable property, much stronger than plain confluence. It implies that, given a term, all derivations to its normal form (if any) have the same length, and that normalization and strong normalization coincide, i.e. if there is a normalizing derivation then there are no diverging derivations. Strong confluence will also hold for λ fire , λ vsub and λ vseq , not for λ shuf .

Let us come back to the splitting of → βv . In Closed CBV it is well-known that → βy is superfluous, at least as long as small-step evaluation is considered, see [START_REF] Accattoli | On the Value of Variables[END_REF]. For Open CBV, → βy is instead necessary, but-as we explained in the introduction-it is not enough, which is why we shall consider extensions of λ Plot . The main problem of Naïve Open CBV is that there are stuck β-redexes breaking the harmony of the system. There are three kinds of solution: those restoring a form of harmony (λ fire ), to be thought as more semantical approaches; those removing stuck β-redexes (λ vsub and λ shuf ), that are more syntactical in nature; those changing the applicative structure of terms (λ vseq ), inspired by sequent calculus.

Terms and Values

As in Plotkin's Open CBV (Fig. 1) The Fireball Calculus λ fire , defined in Fig. 2, was introduced without a name by Paolini and Ronchi Della Rocca in [START_REF] Paolini | Call-by-value Solvability[END_REF] and [START_REF] Della Rocca | The Parametric λ-Calculus[END_REF]Def. 3.1.4,p. 36] where its basic properties are also proved. We give here a presentation inspired by Accattoli and Sacerdoti Coen's [START_REF] Accattoli | On the Relative Usefulness of Fireballs[END_REF], departing from it only for inessential, cosmetic details. Terms, values and evaluation contexts are the same as in λ Plot .

Fireballs f, f , f ::= λx.t | i Inert Terms i, i , i ::= xf1 . . . fn n ≥ 0 Evaluation Contexts E ::= • | tE | Et Rule at Top Level Contextual closure (λx.t)(λy.u) →β λ t{x λy.u} E t →β λ E u if t →β λ u (λx.t)i →β i t{x i} E t →β i E u if t →β i u Reduction →β f := →β λ ∪ →β i
The idea is to restore harmony by generalizing → βy to fire when the argument is a more general inert term-the new rule is noted → βi . The generalization of values as to include inert terms is called fireballs. Actually fireballs and inert terms are defined by mutual induction (in Fig. 2). For instance, λx.y is a fireball as an abstraction, while x, y(λx.x), xy, and (z(λx.x))(zz)(λy.(zy)) are fireballs as inert terms. Note that ii is an inert term for all inert terms i and i . Inert terms can be equivalently defined as i ::= x | if . The main feature of an inert term is that it is open, normal and that when plugged in a context it cannot create a redex, hence the name (it is not a so-called neutral term because it might have redexes under abstractions). In Grégoire and Leroy's presentation [START_REF] Grégoire | A compiled implementation of strong reduction[END_REF], inert terms are called accumulators and fireballs are simply called values.

Evaluation is given by the fireball rule → β f , that is the union of → β λ and → βi . For instance, consider t := ((λy.δ)(zz))δ and u := δ((λy.δ)(zz)) as in Eq. (1), p. 2: t and u are β v -normal but they diverge when evaluated in λ fire , as desired:

t → βi δδ → β λ δδ → β λ . . . and u → βi δδ → β λ δδ → β λ . . . .
The distinguished, key property of λ fire is (for any t ∈ Λ):

Proposition 2 (Open Harmony). t is β f -normal iff t is a fireball.
The advantage of λ fire is its simple notion of normal form, i.e. fireballs, that have a clean syntactic description akin to that for call-by-name. The other calculi will lack a nice, natural notion of normal form. The drawback of the fireball calculus-and probably the reason why its importance did not emerge before-is the fact that as a strong calculus it is not confluent: this is due to the fact that fireballs are not closed by substitution (see [28, p. 37]). Indeed, if evaluation is strong, the following critical pair cannot be joined, where t := (λy.I)(δδ) and I := λz.z is the identity combinator:

I β λ ← (λx.I)δ βi ← (λx.(λy.I)(xx))δ → β λ t → β λ t → β λ . . . (2)
On the other hand, as long as evaluation is weak (that is the case we consider) everything works fine-the strong case can then be caught by repeatedly iterating the weak one under abstraction, once a weak normal form has been obtained (thus forbidding the left part of ( 2)). In fact, the weak evaluation of λ fire has a simple rewriting theory, as next proposition shows. In particular it is strongly confluent. where the redex involving λy and s has been created by the β-step. In Naïve Open CBV if r is a normal form and not a value then the creation cannot take place, blocking evaluation. This is the problem concerning the term t in Eq. ( 1), p. 2.

In CBV there is another form of creation-of type 4 -not considered by Lévy:

(λx.t)((λy.v)v ) → βv (λx.t)(v{y v })
i.e. a reduction in the argument turns the argument itself into a value, creating a β v -redex. As before, in an open setting v may be replaced by a normal form that is not a value, blocking the creation of type 4. This is exactly the problem concerning the term u in Eq. (1), p. 2. The proposals of this and the next sections introduce some way to enable creations of type 1 and 4, without substituting stuck β-redexes nor inert terms.

The value substitution calculus λ vsub of Accattoli and Paolini [START_REF] Accattoli | Call-by-Value Solvability, revisited[END_REF]2] was introduced as a calculus for Strong CBV inspired by linear logic proof nets. In Fig. 3 we present its adaptation to Open CBV, obtained by simply removing abstractions from evaluation contexts. It extends the syntax of terms with the constructor [x u], called explicit substitution (shortened ES, to not be confused with the meta-level substitution {x u}). A vsub-term t[x u] represents the delayed substitution of u for x in t, i.e. stands for let x = u in t. So, t[x u] binds the free occurrences of x in t. The set of vsub-terms-identified up to α-equivalence-is denoted by Λ vsub (clearly Λ Λ vsub ).

ES are used to remove stuck β-redexes: the idea is that β-redexes can be fired whenever-even if the argument is not a (vsub-)value-by means of the vsub-Terms t, u, s The drawback of λ vsub is that it requires explicit substitutions. The advantage of λ vsub is its simple and well-behaved rewriting theory, even simpler than the rewriting for λ fire , since every rule terminates separately (while β λ does not)-in particular strong confluence holds. Moreover, the theory has a sort of flexible second level given by a notion of structural equivalence, coming up next. Structural Equivalence. The theory of λ vsub comes with a notion of structural equivalence ≡, that equates vsub-terms that differ only for the position of ES. The basic idea is that the action of an ES via the exponential rule depends on the position of the ES itself only for inessential details (as long as the scope of binders is respected), namely the position of other ES, and thus can be abstracted away. A strong justification for the equivalence comes from the linear logic interpretation of λ vsub , in which structurally equivalent vsub-terms translate to the same (recursively typed) proof net, see [2].

::= v | tu | t[x u] vsub-Values v ::= x | λx.t Evaluation Contexts E ::= • | tE | Et | E[x u] | t[x E] Substitution Contexts L ::= • | L[x u]
Structural equivalence ≡ is defined as the least equivalence relation on Λ vsub closed by evaluation contexts (see Fig. 3) and generated by the following axioms:

t[y s][x u] ≡ com t[x u][y s] if y / ∈ fv(u) and x / ∈ fv(s) t s[x u] ≡ @r (ts)[x u] if x ∈ fv(t) t[x u]s ≡ @l (ts)[x u] if x ∈ fv(s) t[x u[y s]] ≡ [•] t[x u][y s] if y ∈ fv(t)
We set → vsub≡ := ≡→ vsub ≡ (i.e. for all t, r ∈ Λ vsub : t → vsub≡ r iff t ≡ u → vsub s ≡ r for some u, s ∈ Λ vsub ). The notation → + vsub≡ keeps its usual meaning, while → * vsub≡ stands for ≡ ∪ → + vsub≡ , i.e. a vsub ≡ -derivation of length zero can apply ≡ and is not just the identity. As ≡ is reflexive, → vsub → vsub≡ .

The rewriting theory of λ vsub enriched with structural equivalence ≡ is remarkably simple, as next lemma shows. In fact, ≡ commutes with evaluation, and can thus be postponed. Additionally, the commutation is strong, as it preserves the number and kind of steps-one says that it is a strong bisimulation (with respect to → vsub ). In particular, the equivalence is not needed to compute and it does not break, or make more complex, any property of λ vsub . On the contrary, it enhances the flexibility of the system: it will be essential to establish simple and clean relationships with the other calculi for Open CBV.

Lemma 5 (Basic Properties of Structural Equivalence ≡, [START_REF] Accattoli | Call-by-Value Solvability, revisited[END_REF]). Let t, u ∈ Λ vsub and x ∈ {m, e λ , e y , e, vsub}.

Open Call-by-Value 3: The Shuffling Calculus λ shuf

The calculus introduced by Carraro and Guerrieri in [START_REF] Carraro | A Semantical and Operational Account of Call-by-Value Solvability[END_REF], and here deemed Shuffling Calculus, has the same syntax of terms as Plotkin's calculus. Two additional commutation rules help → βv to deal with stuck β-redexes, by shuffling constructors so as to enable creations of type 1 and 4. As for λ vsub , λ shuf was actually introduced, and then used in [START_REF] Carraro | A Semantical and Operational Account of Call-by-Value Solvability[END_REF][START_REF] Guerrieri | Head reduction and normalization in a call-by-value lambda-calculus[END_REF][START_REF] Guerrieri | Standardization of a Call-By-Value Lambda-Calculus[END_REF], to study Strong CBV. In Fig. 4 we present its adaptation to Open CBV, based on balanced contexts, a special notion of evaluation contexts. The reductions → σ and → β v are non-deterministic and-because of balanced contexts-can reduce under abstractions, but they are morally weak: they reduce under a λ only when the λ is applied to an argument. Note that the condition x / ∈ fv(s) (resp. x / ∈ fv(v)) in the definition of the shuffling rule → σ1 (resp. → σ3 ) can always be fulfilled by α-conversion.

The rewriting (shuffling) rules → σ 1 and → σ 3 unblock stuck β-redexes. For instance, consider the terms t := ((λy.δ)(zz))δ and u := δ((λy.δ)(zz)) where

Terms and Values

As in Plotkin's Open CBV (Fig. 1) Balanced Contexts The advantage of λ shuf is with respect to denotational investigations. In [START_REF] Carraro | A Semantical and Operational Account of Call-by-Value Solvability[END_REF], λ shuf is indeed used to prove various semantical results in connection to linear logic, resource calculi, and the notion of Taylor expansion due to Ehrhard. In particular, in [START_REF] Carraro | A Semantical and Operational Account of Call-by-Value Solvability[END_REF] it has been proved the adequacy of λ shuf with respect to the relational model induced by linear logic: a by-product of our paper is the extension of this adequacy result to all incarnations of Open CBV. The drawback of λ shuf is its technical rewriting theory. We summarize some properties of λ shuf : Proposition 6 (Basic Properties of λ shuf , [START_REF] Carraro | A Semantical and Operational Account of Call-by-Value Solvability[END_REF]). 1. Let t, u, s ∈ Λ. If t → β v u and t → σ s then u = s. 2. → σ is strongly normalizing and (not strongly) confluent. 3. → shuf is (not strongly) confluent. 4. Let t ∈ Λ: t is strongly shuf-normalizable iff t is shuf-normalizable.

B ::= • | tB | Bt | (λx.B)t Rule at Top Level Contextual closure ((λx.t)u)s →σ 1 (λx.ts)u, x / ∈ fv(s) B t → σ 1 B u if t →σ 1 u v((λx.s)u) →σ 3 (λx.vs)u, x / ∈ fv(v) B t → σ 3 B u if t →σ 3 u (λx.t)v →β v t{x v} B t → β v B u if t →β v u Reductions → σ := → σ 1 ∪ → σ 3 , →shuf := → β v ∪ → σ Fig. 4.
In contrast to λ fire and λ vsub , λ shuf is not strongly confluent and not all shufnormalizing derivations (if any) from a given term have the same length (consider, for instance, all shuf-normalizing derivations from (λy.z)(δ(zz))δ). Nonetheless, normalization and strong normalization still coincide in λ shuf (Prop. 6.4), and Cor. 18 in Sect. 3 will show that the discrepancy is encapsulated inside the additional shuffling rules, since all shuf-normalizing derivations (if any) from a given term have the same number of β v -steps.

Open Call-by-Value 4: The Value Sequent Calculus λ vseq

A more radical approach to the removal of stuck β-redexes is provided by what is here called the Value Sequent Calculus λ vseq , defined in Fig. 5. In λ vseq , it is the applicative structure of terms that is altered, by replacing the application constructor with more constructs, namely commands c and environments e. Morally, λ vseq looks at a sequence of applications from the head, that is the value on the left of a command v | e rather than from the tail as in natural deduction. In fact, λ vseq is a handy presentation of the intuitionistic fragment of λμ, that in turn is the CBV fragment of λµμ, a calculus obtained as the computational interpretation of a sequent calculus for classical logic. Both λμ and λµμ are due to Curien and Herbelin [START_REF] Curien | The duality of computation[END_REF], see [START_REF] Ariola | Sequent calculi and abstract machines[END_REF][START_REF] Curien | The Duality of Computation under Focus[END_REF] for further investigations about these systems.

A peculiar trait of the sequent calculus approach is the environment constructor μx.c, that is a binder for the free occurrences of x in c. It is often said that it is a sort of explicit substitution-we will see exactly in which sense, in Sect. 4.

The change of the intuitionistic variant λ vseq with respect to λμ is that λ vseq does not need the syntactic category of co-variables α, as there can be only one of them, denoted here by . From a logical viewpoint, this is due to the fact that in intuitionistic sequent calculus the right-hand-side of has exactly one formula, that is neither contraction nor weakening are allowed on the right. Consequently, the binary abstraction λ(x, α).c of λμ is replaced by a more traditional unary one λx.c, and substitution on co-variables is replaced by a notion of appending of environments, defined by mutual induction on commands and environments as follows:

v | e @e := v | e @e @e := e (v•e )@e := v•(e @e) (μx.c)@e := μy.(c{x y}@e) with y / ∈ fv(c) ∪ fv(e)

Essentially, c@e is a capture-avoiding substitution of e for the only occurrence of in c that is out of all abstractions, standing for the output of the term. The append operation is used in the rewrite rule →λ of λ vseq (Fig. 5). Strong CBV can be obtained by simply extending the grammar of evaluation contexts to commands under abstractions.

We will provide a translation from λ vsub to λ vseq that, beyond termination equivalence, will show that switching to a sequent calculus representation is equivalent to a transformation in administrative normal form [START_REF] Sabry | Reasoning about Programs in Continuation-Passing Style[END_REF].

The advantage of λ vseq is that it avoids both rules at a distance and shuffling rules. The drawback of λ vseq is that, syntactically, it requires to step out of the λ-calculus. We will show in Sect. 4 how to reformulate it as a fragment of λ vsub , i.e. in natural deduction. However, it will still be necessary to restrict the application constructor, thus preventing the natural way of writing terms.

The rewriting of λ vseq is very well-behaved, in particular it is strongly confluent and every rewriting rule terminates separately. [START_REF] Paolini | Call-by-value Solvability[END_REF]23,[START_REF] Della Rocca | The Parametric λ-Calculus[END_REF][START_REF] Paolini | Lazy strong normalization[END_REF][START_REF] Paolini | Strong Normalization from an unusual point of view[END_REF] gave several operational, logical, and semantical characterizations of potentially valuable terms in Naïve Open CBV. In particular, in [START_REF] Paolini | Call-by-value Solvability[END_REF][START_REF] Della Rocca | The Parametric λ-Calculus[END_REF] it is proved that a term is potentially valuable in Plotkin's Naïve Open CBV iff its normalizable in λ fire .

Potentially valuable terms can be defined for every incarnation of Open CBV: it is enough to update the notions of evaluation and values in the above definition to the considered calculus. This has been done for λ shuf in [START_REF] Carraro | A Semantical and Operational Account of Call-by-Value Solvability[END_REF], and for λ vsub in [START_REF] Accattoli | Call-by-Value Solvability, revisited[END_REF]. For both calculi it has been proved that, in the weak setting, potentially valuable terms coincides with normalizable terms. In [START_REF] Guerrieri | Standardization of a Call-By-Value Lambda-Calculus[END_REF], it has been proved that Plotkin's potentially valuable terms coincide with shuf-potentially valuable terms (which coincide in turn with shuf-normalizable terms). Our paper makes a further step: proving that termination coincides for λ fire , λ vsub , λ shuf , and λ vseq it implies that all their notions of potential valuability coincide with Plotkin's, i.e. there is just one notion of potential valuability for Open (and Strong) CBV.

Open CBV 5, 6, 7, . . . The literature contains many other calculi for CBV, usually presented for Strong CBV and easily adaptable to Open CBV. Some of them have let-expressions (avatars of ES) and all of them have rules permuting constructors, therefore they lie somewhere in between λ vsub and λ shuf . Often, they have been developed for other purposes, usually to investigate the relationship with monad or CPS translations. Moggi's equational theory [START_REF] Moggi | Computational λ-Calculus and Monads[END_REF] is a classic standard of reference, known to coincide with that of Sabry and Felleisen [START_REF] Sabry | Reasoning about Programs in Continuation-Passing Style[END_REF], Sabry and Wadler [START_REF] Sabry | A Reflection on Call-by-Value[END_REF], Dychoff and Lengrand [START_REF] Dyckhoff | Call-by-Value lambda-calculus and LJQ[END_REF], Herbelin and Zimmerman [START_REF] Herbelin | An operational account of Call-by-Value Minimal and Classical λ-calculus in Natural Deduction form[END_REF] and Maraist et al's λ let in [START_REF] Maraist | Call-by-name, Call-by-value, Call-by-need and the Linear λ-Calculus[END_REF]. In [START_REF] Accattoli | Call-by-Value Solvability, revisited[END_REF], λ vsub modulo ≡ is shown to be termination equivalent to Herbelin and Zimmerman's calculus, and to strictly contain its equational theory, and thus Moggi's. At the level of rewriting these presentations of Open CBV are all more involved than those that we consider here. Their equivalence to our calculi can be shown along the lines of that of λ shuf with λ vsub .

3 Quantitative Equivalence of λ fire , λ vsub , and λ shuf Here we show the equivalence with respect to termination of λ fire , λ vsub , and λ shuf , enriched with quantitative information on the number of steps.

On the Proof Technique. We show that termination in λ vsub implies termination in λ fire and λ shuf by studying simulations of λ fire and λ shuf into λ vsub . To prove the converse implications we do not use inverse simulations. Alternatively, we show that β f -and shuf-normal forms are essentially projected into vsub-normal forms, so that if evaluation terminates in λ fire or λ shuf then it also terminates on λ vsub .

Such a simple technique works because in the systems under study normalization and strong normalization coincide: if there is a normalizing derivation from a given term t then there are no diverging derivations from t (for λ vsub and λ fire it follows from strong confluence, for λ shuf is given by Prop. 6.4). This fact is also the reason why the statements of our equivalences (forthcoming Cor. 13 and Cor. 17) address a single derivation from t rather than considering all derivations from t. Moreover, for any calculus, all normalizing derivations from t have the same number of steps (in λ shuf it holds for β v -steps, see Cor. 18), hence also the quantitative claims of Cor. 13 and Cor. 17 hold actually for all normalizing derivations from t.

In both simulations, the structural equivalence ≡ of λ vsub plays a role.

Equivalence of λ fire and λ

vsub A single β v -step (λx.t)v → βv t{x v} is simulated in λ vsub by two steps: (λx.t)v → m t[x v
] → e t{x v}, i.e. a m-step that creates a ES, and a e-step that turns the ES into the meta-level substitution performed by the β v -step. The simulation of an inert step of λ fire is instead trickier, because in λ vsub there is no rule to substitute an inert term, if it is not a variable. The idea is that an inert step (λx.t)i → βi t{x i} is simulated only by (λx.t)i → m t[x i], i.e. only by the m-step that creates the ES, and such a ES will never be fired-so the simulation is up to the unfolding of substitutions containing inert terms (defined right next).

Everything works because of the key property of inert terms: they are normal and their substitution cannot create redexes, so it is useless to substitute them. The unfolding of a vsub-term t is the term t → obtained from t by turning ES into meta-level substitutions; it is defined by:

x → := x (tu) → := t → u → (λx.t) → := λx.t → (t[x u]) → := t → {x u → } For all t, u ∈ Λ vsub , t ≡ u implies t → = u → . Also, t → = t iff t ∈ Λ.
In the simulation we are going to show, structural equivalence ≡ plays a role. It is used to clean the vsub-terms (with ES) obtained by simulation, putting them in a canonical form where ES do not appear among other constructors.

A vsub-term is clean if it has the form u[

x 1 i 1 ] . . . [x n i n ] (with n ∈ N), u ∈ Λ is called
the body, and i 1 , . . . , i n ∈ Λ are inert terms. Clearly, any term (as it is without ES) is clean. We first show how to simulate a single fireball step.

Lemma 8 (Simulation of a β

f -Step in λ vsub ). Let t, u ∈ Λ. 1. If t → β λ u then t → m → e λ u. 2. If t → βi u then t → m ≡ s, with s ∈ Λ vsub clean and s → = u.
We cannot simulate derivations by iterating Lemma 8, because the starting term t has no ES but the simulation of inert steps introduces ES. Hence, we have to generalize Lemma 8 up to the unfolding of ES. In general, unfolding ES is a dangerous operation with respect to (non-)termination, as it may erase a diverging subterm (e.g. t := x[y δδ] is vsub-divergent and t → = x is normal). In our case, however, the simulation produces clean vsub-terms, so the unfolding is safe since it can erase only inert terms and cannot create, erase, nor carry redexes.

By means of a technical lemma (see the appendix in [3]) we obtain:

Lemma 9 (Projection of a β f -Step on → vsub via Unfolding). Let t be a clean vsub-term and u be a term. The number of β f -steps in λ fire is a reasonable cost model for Open CBV [START_REF] Accattoli | On the Relative Usefulness of Fireballs[END_REF]. Our result implies that also the number of m-steps in λ vsub is a reasonable cost model, since the number of m-steps is exactly the number of β f -steps . This fact is quite surprising: in λ fire arguments of β f -redexes are required to be fireballs, while for m-redexes there are no restrictions on arguments, and yet in any normalizing derivation their number coincide. Note, moreover, that e-steps are linear in m-steps, but only because the initial term has no ES: in general, this is not true.

Equivalence of λ shuf and λ vsub

A derivation d : t → * shuf u in λ shuf is simulated via a projection on multiplicative normal forms in λ vsub , i.e. as a derivation m(t) → * vsub≡ m(u) (for any vsub-term t, its multiplicative and exponential normal forms, denoted by m(t) and e(t) respectively, exist and are unique by Prop. 4). Indeed, a β v -step of λ shuf is simulated in λ vsub by a e-step followed by some m-steps to reach the m-normal form. Shuffling rules → σ of λ shuf are simulated by structural equivalence ≡ in λ vsub : applying m(•) to ((λx.t)u)s → σ 1 (λx.(ts))u we obtain exactly an instance of the axiom ≡ @l defining ≡: m(t)[x m(u)]m(s) ≡ @l (m(t)m(s))[x m(u)] (with the side conditions matching exactly). Similarly, → σ 3 projects to ≡ @r or ≡ [•] (depending on whether v in → σ 3 is a variable or an abstraction). Therefore,

Lemma 14 (Projecting a shuf-Step on → vsub≡ via m-NF). Let t, u ∈ Λ. 1. If t → σ u then m(t) ≡ m(u). 2. If t → β v u then m(t) → e → *
m m(u). In contrast to the simulation of λ fire in λ vsub , here the projection of a single step can be extended to derivations without problems, obtaining that the number of β v -steps in λ shuf matches exactly the number of e-steps in λ vsub . Additionally, we apply the postponement of ≡ (Lemma 5.2), factoring out the use of ≡ (i.e. of shuffling rules) without affecting the number of e-steps.

To obtain the termination equivalence we also need to study normal forms. Luckily, the case of λ shuf is simpler than that of λ fire , as next lemma shows.

Lemma 15 (Projection Preserves Normal Forms

). Let t ∈ Λ. If t is shuf- normal then m(t) is vsub-normal.
The next theorem puts all the pieces together (for any shuf-derivation d, |d| β v is the number of β v -steps in d: this notion is well defined by Prop. 6.1). The obtained quantitative equivalence has an interesting corollary that shows some light on why λ shuf is not strongly confluent. Our simulation maps β v -steps in λ shuf to exponential steps in λ vsub , that are strongly confluent, and thus in equal number in all normalizing derivations (if any) from a given term. Therefore, Corollary 18 (Number of β v -Steps is Invariant). All shuf-normalizing derivations from t ∈ Λ (if any) have the same number of β v -steps.

Said differently, in λ shuf normalizing derivations may have different lengths but the difference is encapsulated inside the shuffling rules → σ 1 and → σ 3 .

Concerning the cost model, things are subtler for λ shuf . Note that the relationship between λ shuf and λ vsub uses the number of e-steps, while the cost model (inherited from λ fire ) is the number of m-steps. Do e-steps provide a reasonable cost model? Probably not, because there is a family of terms that evaluate in exponentially more m-steps than e-steps. Details are left to a longer version.

4 Quantitative Equivalence of λ vsub and λ vseq , via λ vsub k

The quantitative termination equivalence of λ vsub and λ vseq is shown in two steps: first, we identify a sub-calculus λ vsub k of λ vsub equivalent to the whole of λ vsub , and then show that λ vsub k and λ vseq are equivalent (actually isomorphic). Both steps reuse the technique of Sect. 3, i.e. simulation plus study of normal forms.

Equivalence of λ vsubk and λ vsub

The kernel λ vsub k of λ vsub is the sublanguage of λ vsub obtained by replacing the application constructor tu with the restricted form tv where the right subterm can only be a value v-i.e., λ vsub k is the language of so-called administrative normal forms [START_REF] Sabry | Reasoning about Programs in Continuation-Passing Style[END_REF] of λ vsub . The rewriting rules are the same of λ vsub . It is easy to see that λ vsub k is stable by vsub-reduction. For lack of space, more details about λ vsub k are in the appendix of [3].

The translation (•) + of λ vsub into λ vsub k , which simply places the argument of an application into an ES, is defined by (note that fv(t) = fv(t + ) for all t ∈ Λ vsub ): As expected, has, with respect to λ vseq , all the properties of ≡ (see Lemma 5). They are formally stated in the appendix of [3], for lack of space.

x + := x (tu) + := (t + x)[x u + ]

Conclusions and Future Work

This paper proposes Open CBV as a setting halfway between Closed CBV, the simple framework used to model programming languages such as OCaml, and Strong CBV, the less simple setting underling proof assistants such as Coq. Open CBV is a good balance: its rewriting theory is simple-in particular it is strongly confluent, as the one of Closed CBV-and it can be iterated under abstractions to recover Strong CBV, which is not possible with Closed CBV.

We compared four representative calculi for Open CBV, developed with different motivations, and showed that they share the same qualitative (termination/divergence) and quantitative (number of steps) properties with respect to termination. Therefore, they can be considered as different incarnations of the same immaterial setting, justifying the slogan Open CBV.

The qualitative equivalences carry semantical consequences: the adequacy of relational semantics for the shuffling calculus proved in [START_REF] Carraro | A Semantical and Operational Account of Call-by-Value Solvability[END_REF] actually gives a semantic (and type-theoretical, since the relational model can be seen as a non-idempotent intersection type system) characterization of normalizable terms for Open CBV, i.e. it extends to the other three calculi. Similarly, the notion of potential valuability for Plotkin's CBV λ-calculus, well-studied in [START_REF] Paolini | Call-by-value Solvability[END_REF]23,[START_REF] Della Rocca | The Parametric λ-Calculus[END_REF][START_REF] Paolini | Lazy strong normalization[END_REF][START_REF] Paolini | Strong Normalization from an unusual point of view[END_REF] and recalled at the end of Sect. 2, becomes a robust notion characterizing the same terms in Open (and Strong) CBV.

Quantitatively, we showed that in three out of four calculi for Open CBV, namely λ fire , λ vsub and λ vseq , evaluation takes exactly the same number of β f -steps, m-steps and λ-steps, respectively. Since such a number is known to be a reasonable time cost model for λ fire [START_REF] Accattoli | On the Relative Usefulness of Fireballs[END_REF], the cost model lifts to λ vsub and λ vseq , showing that the cost model is robust, i.e. incarnation-independent. For the shuffling calculus λ shuf we obtain a weaker quantitative relationship that does not allow to transfer the cost model. The β v -steps in λ shuf , indeed, match e-steps in λ vsub , but not msteps. Unfortunately, the two quantities are not necessarily polynomially related, since there is a family of terms that evaluate in exponentially more m-steps than e-steps (details are left to a longer version). Consequently, λ shuf is an incarnation more apt to semantical investigations rather than complexity analyses.

Future Work. This paper is just the first step towards a new, finer understanding of CBV. We plan to purse at the least the following research directions:

1. Equational Theories. The four incarnations are termination equivalent but their rewriting rules do not induce the same equational theory. In particular, λ fire equates more than the others, and probably too much because its theory is not a congruence, i.e. it is not stable by context closure. The goal is to establish the relationships between the theories and understand how to smooth the calculi as to make them both equational and termination equivalent. 2. Abstract Machines. Accattoli and Sacerdoti Coen introduce in [START_REF] Accattoli | On the Relative Usefulness of Fireballs[END_REF] reasonable abstract machines for Open CBV, that is, implementation schemas whose overhead is proven to be polynomial, and even linear. Such machines are quite complex, especially the linear one. Starting from a fine analysis of the overhead, we are currently working on a simpler approach providing cost equivalent but much simpler abstract machines. 3. From Open CBV to Strong CBV. We repeatedly said that Strong CBV can be seen as an iteration of Open CBV under abstractions. This is strictly true for λ vsub , λ shuf , and λ vseq , for which the simulations studied here lift to the strong setting. On the contrary, the definition of a good strong λ fire is a subtle open issue. The natural candidate, indeed, is not confluent (but enjoys uniqueness of normal forms) and normalizes more terms than the other calculi for Strong CBV. Another delicate point is the design and the analysis of abstract machines for Strong CBV, of which there are no examples in the literature (both Grégoire and Leroy's [START_REF] Grégoire | A compiled implementation of strong reduction[END_REF] and Accattoli and Sacerdoti Coen's [START_REF] Accattoli | On the Relative Usefulness of Fireballs[END_REF] study machines for Open CBV only). 4. Open Bisimulations. In [START_REF] Lassen | Eager Normal Form Bisimulation[END_REF] Lassen studies open (or normal form) bisimulations for CBV. He points out that his bisimilarity is not fully abstract with respect to contextual equivalence, and his counterexamples are all based on stuck β-redexes in Naïve Open CBV. An interesting research direction is to recast his study in Open CBV and see whether full abstraction holds or not.

Fig. 2 .

 2 Fig. 2. The Fireball Calculus λ fire

Fig. 5 .

 5 Fig. 5. The Value Sequent Calculus λvseq

Different Worlds: while λ fire is related to Coq and implementations, λ vsub and λ shuf have a linear logic background, and λ vseq is rooted in

  Road Map. Sect. 2 provides an overview of the different presentations of Open CBV. Sect. 3 proves the termination equivalences for λ vsub , λ fire and λ shuf , enriched with quantitative information. Sect. 4 proves the quantitative termination equivalence of λ vsub and λ vseq , via an intermediate calculus λ vsub k .

	1. Quantitative Relationships: λ-calculi are usually related only qualitatively,
	while our relationships are quantitative and thus stronger: not only we show
	simulations, but we also relate the number of steps.
	2. Uniform View : we provide a new uniform view on a known problem, that will
	hopefully avoid further proliferations of CBV calculi for open/strong settings.
	3. Expected but Non-Trivial : while the equivalences are more or less expected,
	establishing them is informative, because it forces to reformulate and connect
	concepts among the different settings, and often tricky.
	4. Simple Rewriting Theory: the relationships between the systems are developed
	using basic rewriting concepts. The technical development is simple, according
	to the best tradition of the CBV λ-calculus, and yet it provides a sharp and
	detailed decomposition of Open CBV evaluation.
	5. Connecting sequent
	calculus. With respect to linear logic, λ vsub has been used for syntactical
	studies while λ shuf for semantical ones. Our results therefore establish bridges
	between these different (sub)communities.
	Finally, an essential contribution of this work is the recognition of Open CBV
	as a simple and yet rich framework in between Closed and Strong CBV.

  Here we recall Naïve Open CBV, noted λ Plot , and introduce the four forms of Open CBV that will be compared (λ fire , λ vsub , λ shuf , and λ vseq ) together with a semantic notion (potential valuability) reducing Open CBV to Closed CBV. In this paper terms are always possibly open. Moreover, we focus on Open CBV and avoid on purpose to study Strong CBV (we hint at how to define it, though).

	Terms	t, u, s, r ::= v | tu
	Values	v, v ::= x | λx.t
	Evaluation Contexts	E ::= • | tE | Et
	Rule at Top Level	Contextual closure
	(λx.t)λy.u →β λ t{x λy.u}	E t →β λ E u if t →β λ u
	(λx.t)y →β y t{x y}	E t →β y E u if t →β y u
	Reduction	→β v := →β λ ∪ →β y
	Fig. 1. Naïve Open CBV λ Plot
	2 Incarnations of Open Call-by-Value

  Proposition 3 (Basic Properties of λ fire ). 1. → βi is strongly normalizing and strongly confluent. 2. → β λ and → βi strongly commute. 3. → β f is strongly confluent, and all β f -normalizing derivations d from t ∈ Λ (if any) have the same length |d| β f , the same number |d| β λ of β λ -steps, and the same number |d| βi of β i -steps. 2.2 Open Call-by-Value 2: The Value Substitution Calculus λ vsub

Rewriting Preamble: Creations of Type 1 and 4. The problem with stuck βredexes can be easily understood at the rewriting level as an issue about creations. According to Lévy

[START_REF] Lévy | Réductions correctes et optimales dans le lambda-calcul[END_REF]

, in the ordinary CBN λ-calculus redexes can be created in 3 ways. Creations of type 1 take the following form ((λx.λy.t)r)s → β (λy.t{x r})s

  ] →e λ L t{x λy.u} E t →e λ E u if t →e λ u t[x L y ] →e y L t{x y} E t →e y E u if t →e y u Reductions →e := →e λ ∪ →e y , →vsub := →m ∪ →e Fig. 3. The Value Substitution Calculus λ vsub multiplicative rule → m ; however the argument is not substituted but placed in a ES. The actual substitution is done only when the content of the ES is a vsubvalue, by means of the exponential rule → e . These two rules are sometimes noted →

	Rule at Top Level	Contextual closure
	L λx.t u →m L t[x u]	E t →m E u	if t →m u
	t[x L λy.u

dB (β at a distance) and → vs (substitution by value)-the names we use here are due to the interpretation of the calculus into linear logic proof-nets, see

[2]

. A characteristic feature coming from such an interpretation is that the rewriting rules are contextual, or at a distance: they are generalized as to act up to a list of substitutions (noted L, from List). Essentially, stuck β-redexes are turned into ES and then ignored by the rewriting rules-this is how creations of type 1 and 4 are enabled. For instance, the terms t := ((λy.δ)(zz))δ and u := δ((λy.δ)(zz)) (as in Eq. (

1

), p. 2) are e-normal but t → m δ[y zz]δ → m (xx)[x δ][y zz] → e (δδ)[y zz] → m (xx)[x δ][y zz] → e (δδ)[y zz] → m . . . and similarly for u.

  Proposition 4 (Basic Properties of λ vsub , [4]). 1. → m and → e are strongly normalizing and strongly confluent (separately). 2. → m and → e strongly commute. 3. → vsub is strongly confluent, and all vsub-normalizing derivations d from t ∈ Λ vsub (if any) have the same length |d| vsub , the same number |d| e of e-steps, and the same number |d| m of m-steps 4. Let t ∈ Λ. For any vsub-derivation d from t, |d| e ≤ |d| m .

  1. Strong Bisimulation of ≡ wrt → vsub : if t ≡ u and t → x t then there exists u ∈ Λ vsub such that u → x u and t ≡ u . 2. Postponement of ≡ wrt → vsub : if d : t → * vsub≡ u then there are s ≡ u and e : t → * vsub s such that |d| = |e|, |d| e λ = |e| e λ , |d| ey = |e| ey and |d| m = |e| m . 3. Normal Forms: if t ≡ u then t is x-normal iff u is x-normal. 4. Strong confluence: → vsub≡ is strongly confluent.

  The Shuffling Calculus λ shuf δ := λx.xx (as in Eq. (1), p. 2): t and u areβ v -normal but t → σ 1 (λy.δδ)(zz) → β v (λy.δδ)(zz) → β v . . . and u → σ 3 (λy.δδ)(zz) → β v (λx.δδ)(zz) → β v . . . .The similar shuffling rules in CBN, better known as Regnier's σ-rules[START_REF] Regnier | Une équivalence sur les lambda-termes[END_REF], are contained in CBN β-equivalence, while in Open (and Strong) CBV they are more interesting because they are not contained into (i.e. they enrich) β v -equivalence.

  Proposition 7 (Basic properties of λ vseq ). 1. →λ and → μ are strongly normalizing and strongly confluent (separately). 2. →λ and → μ strongly commute. 3. → vseq is strongly confluent, and all vseq-normalizing derivations d from a command c (if any) have the same length |d|, the same number |d| μ of μ-steps, and the same number |d|λ of λ-steps. 2.5 Variations on a Theme Reducing Open to Closed Call-by-Value: Potential Valuability. Potential valuability relates Naïve Open CBV to Closed CBV via a meta-level substitution closing open terms: a (possibly open) term t is potentially valuable if there is a substitution of (closed) values for its free variables, for which it β v -evaluates to a (closed) value. 3 In Naïve Open CBV, potentially valuable terms do not coincide with normalizable terms because of premature β v -normal forms-such as t and u in Eq. (1) at p. 2-which are not potentially valuable. Paolini, Ronchi Della Rocca and, later, Pimentel

  1. If t → → β λ u then t → m → e λ s, with s ∈ Λ vsub clean and s → = u. 2. If t → → βi u then t → m ≡ s, with s ∈ Λ vsub clean and s → = u.Via Lemma 9 we can now simulate whole derivations (in forthcoming Thm. 12). and Normal Forms. The next step towards the equivalence is to relate normal forms in λ fire (aka fireballs) to those in λ vsub . The relationship is not perfect, since the simulation does not directly map the former to the latter-we have to work a little bit more. First of all, let us characterize the terms in λ vsub obtained by projecting normalizing derivations (that always produce a fireball). Let t be a clean vsub-term. If t → is a fireball, then t is {m, e λ }-normal and its body is a fireball. Now, a {m, e λ }-normal form t morally is vsub-normal, as → ey terminates (Prop. 4.1) and it cannot create {m, e λ }-redexes. The part about creations is better expressed as a postponement property. Lemma 11 (Linear Postponement of → ey ). Let t, u ∈ Λ vsub . If d : t → * vsub u then e : t → * m,e λ → * ey u with |e| vsub = |d| vsub , |e| m = |d| m , |e| e = |d| e and |e| e λ ≥ |d| e λ . The next theorem puts all the pieces together. Theorem 12 (Quantitative Simulation of λ fire in λ vsub ). Let t, u ∈ Λ. If d : t → * β f u then there are s, r ∈ Λ vsub and e : t → * Multiplicative Steps: |d| β f = |e| m ; 2. Exponential (Abstraction) Steps: |d| β λ = |e| e λ = |e| e .3. Normal Forms: if u is β f -normal then there exists g : r → * ey q such that q is a vsub-normal form and |g| ey ≤ |e| m -|e| e λ .Corollary 13 (Linear Termination Equivalence of λ vsub and λ fire ). Let t ∈ Λ. There is a β f -normalizing derivation d from t iff there is a vsub-normalizing derivation e from t. Moreover, |d| β f ≤ |e| vsub ≤ 2|d| β f , i.e. they are linearly related.

	Simulation Lemma 10. vsub r such that
	1. Qualitative Relationship: r ≡ s, u = s →	= r →	and s is clean;
	2. Quantitative Relationship:
	1.

  Theorem 16 (Quantitative Simulation of λ shuf in λ vsub ). Let t, u ∈ Λ. If d : t → * shuf u then there are s ∈ Λ vsub and e : t → * vsub s such that 1. Qualitative Relationship: s ≡ m(u); 2. Quantitative Relationship (Exponential Steps): |d| β v = |e| e ; 3. Normal Form: if u is shuf-normal then s and m(u) are vsub-normal. Corollary 17 (Termination Equivalence of λ vsub and λ shuf ). Let t ∈ Λ. There is a shuf-normalizing derivation d from t iff there is a vsub-normalizing derivation e from t. Moreover, |d| β v = |e| e .

  Multiplicative: if t → m u then t + → m → ey ≡ u + ; 2. Exponential: if t → e λ u then t + → e λ u + , and if t → ey u then t + → ey u + . 3. Structural Equivalence: t ≡ u implies t + ≡ u + . The translation of a vsub-normal form is not vsub k -normal (e.g. (xy) + = (xz)[z y]) but a further exponential normalization provides a vsub k -normal form. Theorem 20 (Quantitative Simulation of λ vsub in λ vsub k ). Let t, u ∈ Λ vsub . If d : t → * vsub u then there are s ∈ Λ vsub k and e : t + → * vsub k s such that Structural Equivalence for λ vseq . The equivalence of λ vsub and λ vsub k relies on the structural equivalence ≡ of λ vsub , so it is natural to wonder how does ≡ look on λ vseq . The structural equivalence of λ vseq is defined as the closure by evaluation contexts of the following axiom

	D μx.D μy.c	μμ D μy.D μx.c	where x / ∈ fv(D ) and y / ∈ fv(D).

where x is fresh

(λx.t) + := λx.t + t[x u] + := t + [x u + ]

Lemma 19 (Simulation). Let t, u ∈ Λ vsub . 1.

Potential valuability for Plotkin's CBV λ-calculus can be equivalently defined using weak or strong βv-reduction: it is the same notion for Naïve Open and Strong CBV.

Acknowledgment. Work partially supported by the A*MIDEX project ANR-11-IDEX-0001-02 funded by the "Investissements d'Avenir" French Government program, managed by the French National Research Agency (ANR), and by ANR projects ANR-12-JS02-006-01 (CoQuaS) and ANR-11-IS02-0002 (Locali).

Corollary 21 (Termination and Cost Equivalence of λ vsub and λ vsub k ). Let t ∈ Λ vsub . There exists a vsub-normalizing derivation d from t iff there exists a vsub k -normalizing derivation e from t + . Moreover, |d| m = |e| m .

Equivalence of λ vsubk and λ vseq

The translation • of λ vsub k into λ vseq relies on an auxiliary translation (•) • of values and it is defined as follows:

x

Note the subtle mapping of ES to μ: ES correspond to appendings of μ to the output of the term u to be substituted, and not of the term t where to substitute. It is not hard to see that λ vsub k and λ vseq are actually isomorphic, where the converse translation (•) , that maps values and commands to terms, and environments to evaluation contexts, is given by:

For the sake of uniformity, we follow the same structure of the other weaker equivalences (i.e. simulation plus mapping of normal forms, here working smoothly) rather than proving the isomorphism formally. The simulation maps multiplicative steps to λ steps, whose number, then, is a reasonable cost model for λ vseq .


Can Risk Aversion

Keywords:

  L'archive ouverte pluridisciplinaire

GATE

Can Risk Aversion Explain Schooling

Attainments?

Evidence From Italy

Christian Belzil, Marco Leonardi


S Awali

M.-A Gaveau

M Briant

J.-M Mestdagh

B Soep

O Gobert

R Maksimenka

L Poisson

Multipronged mapping to the dynamics of a barium atom deposited on argon

Keywords:

HAL is

We have seen in Sec. 3.2 of the main paper that when reversing the acceleration voltages of the VMI, photoions can be imaged on the detector instead of photoelectrons. By gating the polarization voltage of the VMI, Ba + ions are detected selectively. This was performed in the frequency resolved experiment. The resulting photoion images were analyzed in the same way as described in the main paper for the photoelectron images. The corresponding results are shown in Fig. S1 as a 3D-plot, where the Ba + signal intensity is plotted as a function of both the velocity of the Ba + ions and the wavenumber of the pump laser. The dip observed in the signal intensity across Fig. S1 at 180 m.s -1 is due to a dark region of the detector.

FIG. S1: Ba + photoion signal as a function of both the photoion velocity (vertical axis) and wavenumber of the pump laser (horizontal axis). The signal intensity is represented using the same colormap as in the main paper for photoelectrons. * Electronic address: lionel.poisson@cea.fr

EJECTED BARIUM FOR CLUSTERS

We have discussed in section 4.1 of the main paper that all the barium atoms which are present in the beam are bound to the argon clusters.

As a results, the signal which is reported in Fig. S1 find their origin in barium atoms that are carried by the argon cluster. Since this signal corresponds to Ba + ions, either it is due to barium atoms that have been ejected off the cluster prior ionization by the probe laser (i.e. to barium atoms that have been ejected after they have been excited by the pump laser), or to Ba + ion that have desorbed after ionization. Such situation was encountered in the case of Ba atom deposited on helium droplets [1].

ACTION SPECTRA

The important point to observe in Fig. S1 is that the action spectrum is not the same wether low or high and middle velocities are considered. The optimum laser wavenumber is indeed observed between 18 600 and 18 800 cm -1 for velocities smaller than 100 ms -1 , whereas for higher velocities the action spectrum is broad and covers the 18 400-18 750 cm -1 range. For this reason, the velocity distribution of the Ba + ions was fitted as the sum of two Gaussian distributions, one centered at 98 m.s -1 and the other at 286 m.s -1 plotted.

The top panel of Fig. S2 shows the measured velocity distribution (full blue curve) obtained when integrating the Ba + ion signal of Fig. S1 Intensity (arb.u.)

1 8 2 0 0 1 8 3 0 0 1 8 4 0 0 1 8 5 0 0 1 8 6 0 0 1 8 7 0 0 1 8 8 0 0 1 8 9 0 0 1 9 0 0 0 Wavenumber (cm

tribution).

The action spectrum shown in blue in the present Fig. S2 is that shown in Fig. 2 of the main paper. The corresponding atoms have an average velocity of 98 m.s -1 , i.e. an average kinetic energy of 0.007 eV. This action spectrum is discussed in the main paper (Sec. 4.3) as documenting barium atoms that are ejected out of the cluster after they have been excited on the cluster by the pump laser in a one-photon process.

The other action spectrum, shown in red in the present Fig. S2) documents barium atoms which are ejected with a much larger velocity (286 m.s -1 ). Its shape is very close to that of the Σ-like band, which is shown in Fig. 5 (top panel) of the main paper. This signal is therefore associated with the excitation of Ba atoms that are bound to the argon cluster, but unlike those documented by the blue action spectrum they are not ejected off the cluster prior ionization in a one photon process. Two very different processes may be invoke to interpret the red action spectrum.

The first possible interpretation of the red action spectrum follows the observation reported by Loginov and Drabbels where Ba + ions are ejected after ionization of Ba on the droplet [1]. Here, because of unfavorable energetics, a 2-photon ionization by the probe laser is required. As in the helium droplet experiment, the exact nature of the ejection process is not clearly identified yet.

The second possible interpretation of the red action spectrum involves a sequential 3-step process. In the first step, barium is excited to the Σ-like state by the pump laser. Then it undergoes a non-adiabatic energy transfer to a lower electronic state and its recoil energy is large enough to push it off the cluster. Such a process where the initial excitation of barium is transferred to the 6s6p 3 P 0,1,2 triplet has been documented already [2]. Absorption of a single probe photon (3.50 eV) by Ba(6s6p 3 P 2 ) provides barium with 5.18 eV energy, not enough for ionization. The observation of Ba + ions thus require a 2-photon ionization. The corresponding photoelectrons are expected with a 3.45 eV energy. Unfortunately the latter is too large to be detected in the present experiment. This precludes discriminating between the two processes that have just been proposed to interpret the action spectrum shown in red in Fig. S2).

  over the wavenumber of the pump laser. The two Gaussian distributions which fit this velocity are shown in the same panel as dashed blue and red curves together with the fit (full green curve). When the Ba + ion signal of Fig.S1is integrated over the two Gaussian distributions, action spectra are obtained. They are shown in the bottom panel of of Fig.S2(full curves with the color of the corresponding velocity dis-