Dariusz Biernacki

Sergueï Lenglet

Piotr Polesiuk

Bisimulations for Delimited-Control Operators

Keywords: behavioral equivalences, λ-calculus, delimited continuation, control operators

We propose a survey of the behavioral theory of an untyped lambda-calculus extended with the delimited-control operators shift and reset. We define a contextual equivalence for this calculus, that we then aim to characterize with coinductively defined relations, called bisimilarities. We study different styles of bisimilarities (namely applicative, normal-form, and environmental), and we give several examples to illustrate their respective strengths and weaknesses. We also discuss how to extend this work to other delimited-control operators.

Bisimulations pour les opérateurs de contrôle délimité

Résumé : Nous proposons un panorama de la théorie comportementale d'un lambda-calcul non typé étendu avec les opérateurs de contrôle délimité shift et reset. Nous définissons une équivalence contextuelle, que nous cherchons à caractériser avec des bisimilarités définies coinductivement. Nous étudions plusieurs styles de bisimilarité (applicative, de forme normale, environmentale) et donnons plusieurs exemples pour illustrer leurs forces et faiblesses respectives.

Nous discutons également de comment étendre ce travail à d'autres opérateurs de contrôle délimité.

Mots-clés : Équivalences comportementales, λ-calcul, continuation délimitée, opérateurs de contrôle

Introduction

Delimited-control operators. Control operators for delimited continuations enrich a programming language with the ability to delimit the current continuation, to capture such a delimited continuation, and to compose delimited continuations. Such operators have been originally proposed independently by Felleisen [START_REF] Felleisen | The theory and practice of first-class prompts[END_REF] and by Danvy and Filinski [START_REF] Danvy | Abstracting control[END_REF], with numerous variants designed subsequently [START_REF] Hieb | [END_REF][START_REF] Moreau | Partial continuations as the difference of continuations, a duumvirate of control operators[END_REF][START_REF] Gunter | A generalization of exceptions and control in ML-like languages[END_REF][START_REF] Dybvig | A monadic framework for delimited continuations[END_REF]. The applications of delimited-control operators range from non-deterministic programming [START_REF] Danvy | Abstracting control[END_REF][START_REF] Kiselyov | Backtracking, interleaving, and terminating monad transformers[END_REF], partial evaluation [START_REF] Danvy | Type-directed partial evaluation[END_REF], and normalization by evaluation [START_REF] Dybjer | Normalization and partial evaluation[END_REF] to concurrency [START_REF] Hieb | [END_REF], mobile code [START_REF] Sumii | An implementation of transparent migration on standard Scheme[END_REF], linguistics [START_REF] Shan | Delimited continuations in natural language: quantification and polarity sensitivity[END_REF], operating systems [START_REF] Kiselyov | Delimited continuations in operating systems[END_REF], and probabilistic programming [START_REF] Kiselyov | Embedded probabilistic programming[END_REF]. Several variants of delimited-control operators are nowadays available in mainstream functional languages such as Haskell [START_REF] Dybvig | A monadic framework for delimited continuations[END_REF], Ocaml [START_REF] Kiselyov | Delimited control in OCaml, abstractly and concretely: System description[END_REF], Scala [START_REF] Rompf | Implementing first-class polymorphic delimited continuations by a type-directed selective cps-transform[END_REF], Scheme [START_REF] Flatt | Adding delimited and composable control to a production programming environment[END_REF],

and SML [START_REF] Filinski | Representing monads[END_REF].

The control operators shift and reset [START_REF] Danvy | Abstracting control[END_REF] were designed to account for the traditional model of non-deterministic programming based on success and failure continuations, and their semantics as well as pragmatics take advantage of an extended continuation-passing style (CPS), where the continuation of the computation is represented by the current delimited continuation and a metacontinuation. In his seminal articles [START_REF] Filinski | Representing monads[END_REF][START_REF] Filinski | Representing layered monads[END_REF], Filinski showed that because the continuation monad can express any other monad, shift and reset can express any monadic effect in direct style (DS), which gives them a special position among all the control operators considered in the literature. In particular, the control operator call/cc known from Scheme and SML of New Jersey requires the presence of mutable state to obtain the expressive power of shift and reset.

Relying on the CPS translation to a pure language is helpful and inspiring when programming with shift and reset, but it is arguably more convenient to reason directly about the code with control operators. To facilitate such reasoning, Kameyama et al. devised direct-style axiomatizations for a number of delimited-control calculi [START_REF] Kameyama | A sound and complete axiomatization of delimited continuations[END_REF][START_REF] Kameyama | Axioms for control operators in the CPS hierarchy[END_REF][START_REF] Kameyama | Equational axiomatization of call-by-name delimited control[END_REF] that are sound and complete with respect to the corresponding CPS translations. Numerous other results concerning equational reasoning in various calculi for delimited continuations [START_REF] Sabry | Note on axiomatizing the semantics of control operators[END_REF][START_REF] Ariola | A proof-theoretic foundation of abortive continuations[END_REF][START_REF] Herbelin | An approach to call-by-name delimited continuations[END_REF][START_REF] Materzok | Axiomatizing subtyped delimited continuations[END_REF] show that it has been a topic of active research.

While the CPS-based equational theories are a natural consequence of the denotational or translational semantics of control operators such as shift and reset, they are not strong enough to verify the equivalences of programs that have unrelated images through the CPS translation, but that operationally cannot be distinguished (e.g., take two different fixed-point combinators). In order to build a stronger theory of program equivalence for delimited control, we turn to the operational foundations of shift and reset [START_REF] Biernacka | An operational foundation for delimited continuations in the CPS hierarchy[END_REF], and consider operationally-phrased criteria for program equivalence.

Behavioral equivalences. Because of the complex nature of control effects, it can be difficult to determine if two programs that use shift and reset are equivalent (i.e., behave in the same way) or not. Contextual equivalence [START_REF] Morris | Lambda Calculus Models of Programming Languages[END_REF] is widely considered as the most natural equivalence on terms in languages based on the λ-calculus. The intuition behind this relation is that two programs are equivalent if replacing one by the other in a bigger program does not change the behavior of this bigger program. The behavior of a program has to be made formal by defining the observable actions we want to take into account for the calculus we consider. It can be, e.g., inputs and outputs for communicating systems [START_REF] Sangiorgi | The Pi-Calculus: A Theory of Mobile Processes[END_REF], memory reads and writes, etc. For the plain λ-calculus [START_REF] Abramsky | Full abstraction in the lazy lambda calculus[END_REF], it is usually whether the term terminates or not. The "bigger program" can be seen as a context (a term with a hole) and, therefore, two terms t 0 and t 1 are contextually equivalent if we cannot tell them apart when executed within any context C , i.e., if C [t 0 ] and C [t 1 ] produce the same observable actions.

The latter quantification over contexts C makes contextual equivalence hard to use in practice to prove that two given terms are equivalent. As a result, one usually looks for more tractable alternatives to contextual equivalence, such as logical relations (see, e.g., [START_REF] Pitts | Parametric polymorphism and operational equivalence[END_REF]), axiomatizations (see, e.g., [START_REF] Lanese | On the expressiveness and decidability of higher-order process calculi[END_REF]), or bisimulations. A bisimulation relates two terms t 0 and t 1 by asking them to mimic each other in a coinductive way, e.g., if t 0 reduces to a term t 0 , then t 1 has to reduce to a term t 1 so that t 0 and t 1 are still in the bisimulation, and conversely for the reductions of t 1 . An equivalence on terms, called bisimilarity can be derived from a notion of bisimulation: two terms are bisimilar if there exists a bisimulation which relates them. Finding an appropriate notion of bisimulation consists in finding the conditions on which two terms are related, so that the resulting notion of bisimilarity is sound and complete w.r.t. contextual equivalence, (i.e., it is included in and it contains contextual equivalence, respectively).

Different styles of bisimulations have been proposed for calculi similar to the λ-calculus. For example, applicative bisimilarity [START_REF] Abramsky | Full abstraction in the lazy lambda calculus[END_REF] relates terms by reducing them to values (if possible), and the resulting values have to be themselves applicative bisimilar when applied to an arbitrary argument. As we can see, applicative bisimilarity still contains some quantification over arguments to compare values, but is nevertheless easier to use than contextual equivalence because of its coinductive nature, and also because we do not have to consider all forms of contexts. Applicative bisimilarity is usually sound and complete w.r.t. contextual equivalence, at least for deterministic languages such as the plain λ-calculus [START_REF] Abramsky | Full abstraction in the lazy lambda calculus[END_REF].

In contrast with applicative bisimilarity, normal-form bisimilarity [START_REF] Lassen | Eager normal form bisimulation[END_REF] (also called open bisimilarity in [START_REF] Sangiorgi | The lazy lambda calculus in a concurrency scenario[END_REF]) does not contain any quantification over arguments or contexts in its definition. The principle is to reduce the compared terms to normal forms (if possible), and then to decompose the resulting normal forms into sub-components that have to be themselves bisimilar. Unlike applicative bisimilarity, normal-form bisimilarity is usually not complete, i.e., there exist contextually equivalent terms that are not normal-form bisimilar. But because of the lack of quantification over contexts, proving that two terms are normal-form bisimilar is usually quite simple, and the proofs can be further simplified with the help of up-to techniques. The idea behind up-to techniques is to define relations that are not exactly bisimulations but are included in bisimulations. Finding an up-to relation equating two given terms is usually simpler than finding a regular bisimulation relating these terms.

Finally, environmental bisimilarity [START_REF] Sangiorgi | Environmental bisimulations for higher-order languages[END_REF] is quite similar to applicative bisimilarity, as it compares terms by reducing them to values, and then requires the resulting values to be bisimilar when applied to some arguments. However, the arguments are no longer arbitrary, but built using an environment, which represents the knowledge accumulated so far by an outside observer on the tested terms. Like applicative bisimilarity, environmental bisimilarity is usually sound and complete, but it also allows for up-to techniques (like normal-form bisimilarity) to simplify its equivalence proofs. In contrast, the definition of useful up-to techniques for applicative bisimilarity remains an open problem. This work. In this article, we propose a survey of the behavioral theory of a λ-calculus extended with the operators shift and reset, called λ S . In previous works, we defined applicative [START_REF] Biernacki | Applicative bisimulations for delimited-control operators[END_REF], normal-form [START_REF] Biernacki | Normal form bisimulations for delimitedcontrol operators[END_REF], and environmental [START_REF] Biernacki | Environmental bisimulations for delimitedcontrol operators[END_REF] bisimilarities for this calculus. We present here these results in a systematic and uniform way, with examples allowing for comparisons between the different styles of bisimulation. In particular, we compare bisimilarities to Kameyama and Hasegawa's direct style axiomatization of λ S [START_REF] Kameyama | A sound and complete axiomatization of delimited continuations[END_REF], and we use these axioms as examples throughout the paper. We consider two semantics for λ S , one that is faithful to its defining CPS translation, where terms are executed within an outermost reset (we call it the "original semantics"), and another one where this requirement is lifted (we call it the "relaxed semantics"). Finally, we discuss how this work can be extended to other delimited-control operators.

Structure of the article. Section 2 presents the syntax and semantics of the calculus λ S with shift and reset that we use in this paper. In this section, we also recall the definition of CPS equivalence, a CPS-based equivalence between terms, and its axiomatization. Section 3 discusses the definition of a contextual equivalence for λ S , and its relationship with CPS equivalence. We look for (at least sound) alternatives of this contextual equivalence by considering several styles of bisimilarities: normal-form in Section 4, applicative in Section 5, and environmental in Section 6. Section 7 discusses the possible extensions of our work to other semantics and other calculi with delimited control, and Section 8 concludes this paper. The appendices contain the proofs too long to be included in the body of the paper.

We discuss related work along the way in the relevant sections, e.g., related work on normal-form bisimilarities for control operators is discussed at the beginning of Section 4. Section 4 develops on results presented in [START_REF] Biernacki | Normal form bisimulations for delimitedcontrol operators[END_REF], except for the part about the original semantics (Section 4.6), which is new. Section 5 expands on results in [START_REF] Biernacki | Applicative bisimulations for delimited-control operators[END_REF], and Section 6 on results in [START_REF] Biernacki | Environmental bisimulations for delimitedcontrol operators[END_REF], except that the definition of environmental bisimulation for the relaxed semantics has been changed.

Notations and basic definitions. We define here some notations frequently used throughout the paper. We write for (m, m ) ∈ R, R -1 for its inverse, defined as

R -1 def = {(m , m) | m R m },
and R * for its transitive and reflexive closure, defined as

R * def = {(m, m ) | ∃m 1 , . . . , m k , k ≥ 0 ∧ m = m 0 ∧ m k = m ∧ ∀0 ≤ i < k, m i R m i+1 }.
Further, given two binary relations R and S we use juxtaposition RS for their composition, defined as RS= {(m, m ) | ∃m , m R m ∧ m S m }. Finally, a relation R is compatible if it is preserved by all the operators of the language, e.g., t 0 R t 1 implies λx.t 0 R λx.t 1 ; a relation is a congruence if it is a compatible equivalence relation.

The Calculus

In this section, we present the syntax, reduction semantics, and CPS equivalence for the language λ S studied throughout this article.

Syntax

The language λ S extends the call-by-value λ-calculus with the delimitedcontrol operators shift and reset [START_REF] Danvy | Abstracting control[END_REF]. We assume we have a set of term variables, ranged over by x, y, z, and k. We use the metavariable k for shift-bound variables representing a continuation, while x, y, and z stand for the usual lambda-bound variables representing any values; we believe such a distinction helps to understand examples and reduction rules.

The syntax of terms (T ) and values (V) is given by the following grammars:

Terms: t ::= v | t t | Sk.t | t Values: v ::= x | λx.t
The operator shift (Sk.t) is a capture operator, the extent of which is determined by the delimiter reset ( • ). A λ-abstraction λx.t binds x in t and a shift construct Sk.t binds k in t; terms are equated up to α-conversion of their bound variables. The set of free variables of t is written fv(t); a term t is closed if fv(t) = ∅. The set of closed terms (values) is noted T c (V c , respectively). We distinguish several kinds of contexts, represented outside-in, as follows:

Pure contexts:

E ::= | v E | E t Evaluation contexts: F ::= | v F | F t | F Contexts: C ::= | λx.C | t C | C t | Sk.C | C
Regular contexts are ranged over by C . The pure evaluation contexts (PC) (abbreviated as pure contexts), 1 ranged over by E , represent delimited continuations and can be captured by the shift operator. The call-by-value evaluation contexts, ranged over by F , represent arbitrary continuations and encode the chosen reduction strategy. Filling a context C (E , F ) with a term t produces a term, written C [t] (E [t], F [t], respectively); the free variables of t may be captured in the process. We extend the notion of free variables to contexts (with fv( ) = ∅), and we say a context C (E , F ) is closed if fv(C ) = ∅ (fv(E ) = ∅, fv(F ) = ∅, respectively). The set of closed pure contexts is noted PC c . In any definitions or proofs, we say a variable is fresh if it does not occur free in the terms or contexts under consideration.

Reduction Semantics

The call-by-value left-to-right reduction semantics of λ S is defined as follows, where t{v/x} is the usual capture-avoiding substitution of v for x in t:

F [(λx.t) v] → v F [t{v/x}] (β v ) F [ E [Sk.t] ] → v F [ t{λx. E [x] /k} ] with x / ∈ fv(E ) (shift) F [ v ] → v F [v] (reset)
The term (λx.t) v is the usual call-by-value redex for β-reduction (rule (β v )). The operator Sk.t captures its surrounding context E up to the dynamically nearest enclosing reset, and substitutes λx. E [x] for k in t (rule (shift)). If a reset is enclosing a value, then it has no purpose as a delimiter for a potential capture, and it can be safely removed (rule (reset)). All these reductions may occur within a metalevel context F . The chosen call-by-value evaluation strategy is encoded in the grammar of the evaluation contexts. Furthermore, the reduction relation → v is compatible with evaluation contexts F , i.e., F [t] → v F [t ] whenever t → v t . We write t → v when there is a t such that t → v t and we write t → v when no such t exists.

Example 2.1. Let i def = λx.x and ω def = λx.xx. We present the sequence of reductions initiated by ((Sk 1 .i (k 1 i)) Sk 2 .ω) (ω ω) . The term Sk 1 .i (k 1 i) is within the pure context E def = ( Sk 2 .ω) (ω ω), enclosed in a delimiter • , so E is captured according to rule (shift):

((Sk 1 .i (k 1 i)) Sk 2 .ω) (ω ω) → v i ((λx. (x Sk 2 .ω) (ω ω) ) i)
The role of reset in λx. E [x] is more clear after reduction of the

β v -redex (λx. E [x] ) i: i ((λx. (x Sk 2 .ω) (ω ω) ) i) → v i (i Sk 2 .ω) (ω ω)
When the captured context E is reactivated, it is not merged with the context i , but composed thanks to the reset enclosing E . As a result, the capture triggered by Sk 2 .ω leaves the term i outside the first enclosing reset intact:

i (i Sk 2 .ω) (ω ω) → v i ω
Because k 2 does not occur in ω, the context (i ) (ω ω) is discarded when captured by Sk 2 .ω. Finally, we remove the useless delimiter i ω → v i ω with rule (reset), and we then β v -reduce and remove the last delimiter i ω → v ω → v ω. Note that while the reduction strategy is call-by-value, some function arguments are not evaluated, like the non-terminating term ω ω in this example. and ∆ def = λx.δ x δ x is Curry's call-by-value fixed-point combinator. In [START_REF] Danvy | A functional abstraction of typed contexts[END_REF], the authors propose variants of these combinators using shift and reset. They write Turing's combinator as θ Sk.k k and Curry's combinator as λx. δ x Sk.k k . For an example, the following reduction sequence demonstrates the behavior of the former: θ Sk.k k → v (λx. θ x ) (λx. θ x ) → * v λy.y (λz.(λx. θ x ) (λx. θ x ) y z)

We use the combinators and their delimited-control variants as examples throughout the paper, and, in particular, we study the equivalences between them in Example 4.4.

Remark 2.3. The context capture can also be written using local reduction rules [START_REF] Felleisen | The theory and practice of first-class prompts[END_REF], where the context is consumed piece by piece. We discuss these reduction rules and their consequences on the results of this article in Section 7.1.

There exist terms which are not values and which cannot be reduced any further; these are called stuck terms. Definition 2.4. A term t is stuck if t is not a value and t → v .

For example, the term E [Sk.t] is stuck because there is no enclosing reset; the capture of E by the shift operator cannot be triggered. In fact, stuck terms are easy to characterize. Proposition 2.5. A term t is stuck iff

• t = E [Sk.t ]
for some E , k, and t , or

• t = F [x v]
for some F , x, and v.

We call control stuck terms the terms of the form E [Sk.t] and open stuck terms the terms of the form F [x v]. Definition 2.6. A term t is a normal form, if t is a value or a stuck term.

We call redexes (ranged over by r) terms of the form (λx.t) v, E [Sk.t] , and v . Thanks to the following unique-decomposition property, the reduction relation → v is deterministic. Proposition 2.7. For all terms t, either t is a normal form, or there exist a unique redex r and a unique context F such that t = F [r].

Finally, we define the evaluation relation of λ S as follows.

Definition 2.8. We write t ⇓ v t if t → * v t and t is a normal form.

If a term t admits an infinite reduction sequence, we say it diverges, written t ⇑ v . As an example of such a term, we use extensively Ω def = (λx.x x) (λx.x x). In the rest of the paper, we use the following results on the reduction (or evaluation) of terms. First, a control stuck term cannot be obtained from a term of the form t . Proposition 2.9. If t ⇓ v t then t is a value or an open stuck term of the form F [x v] . (If t is closed then t can only be a closed value.)

Proof. By induction on the number of reduction steps in t ⇓ v t .

We then show that reduction is preserved by substitution.

Proposition 2.10. If t → v t , then t{v/x} → v t {v/x}.

Proof. By case analysis on t → v t .

The original reduction semantics

Let us notice that the reduction semantics we have introduced does not require terms to be evaluated within a top-level reset-a requirement that is commonly relaxed in practical implementations of shift and reset [START_REF] Dybvig | A monadic framework for delimited continuations[END_REF][START_REF] Filinski | Representing monads[END_REF], but also in some other studies of these operators [START_REF] Asai | Polymorphic delimited continuations[END_REF][START_REF] Kameyama | Axioms for control operators in the CPS hierarchy[END_REF]. This is in contrast to the original reduction semantics for shift and reset [START_REF] Biernacka | An operational foundation for delimited continuations in the CPS hierarchy[END_REF] that has been obtained from the 2-layered continuation-passing-style (CPS) semantics [START_REF] Danvy | Abstracting control[END_REF], discussed in Section 2.4. A consequence of the correspondence with the CPS-based semantics is that terms in the original reduction semantics are treated as complete programs and are decomposed into triples consisting of a subterm (a value or a redex), a delimited context, and a meta-context (a list of delimited contexts), resembling abstract machine configurations. Such a decomposition imposes the existence of an implicit top-level reset, hard-wired in the decomposition, surrounding any term to be evaluated.

The two semantics, therefore, differ in that in the original semantics there are no control stuck terms. However, it can be easily seen that operationally the difference is not essential-they are equivalent when it comes to terms of the form t . In the rest of the article we call such terms delimited terms and we use the relaxed semantics when analyzing their behavior.

The top-level reset requirement, imposed by the original semantics, does not lend itself naturally to the notion of applicative bisimulation that we propose for the relaxed semantics in Section 5. We show, however, that the requirement can be successfully treated in the framework of normal-form and environmental bisimulations, presented in Sections 4 and 6.

CPS Equivalence

The operators shift and reset have been originally defined by a translation into continuation-passing style [START_REF] Danvy | Abstracting control[END_REF] that we present in Figure 1. Translated terms expect two continuations: the delimited continuation representing the rest of the computation up to the dynamically nearest enclosing delimiter, and the metacontinuation representing the rest of the computation beyond this delimiter. In the first three equations the metacontinuation k 2 could be η-reduced, yielding Plotkin's familiar CBV CPS translation [START_REF] Plotkin | Call-by-name, call-by-value and the λ-calculus[END_REF]. In the equation for reset, the current delimited continuation k 1 is moved to the metacontinuation and the delimited term receives the initial delimited continuation. In the equation for shift, the current continuation is captured (and reinitialized) as a lambda abstraction that when applied pushes the then-current delimited continuation on the metacontinuation, and applies the captured continuation to the argument. A CPS-transformed program is run with the initial delimited continuation γ and the identity metacontinuation. For example, CPS translating the term x y Sk.z (k x ) and β-reducing the administrative redexes [START_REF] Danvy | Representing control, a study of the CPS transformation[END_REF] to avoid clutter, we obtain

RR n°9096 x = λk 1 k 2 .k 1 x k 2 λx.t = λk 1 k 2 .k 1 (λx.t) k 2 t 0 t 1 = λk 1 k 2 .t 0 (λx 0 k 2 .t 1 (λx 1 k 2 .x 0 x 1 k 1 k 2 ) k 2 ) k 2 t = λk 1 k 2 .t γ (λx.k 1 x k 2 ) Sk.t = λk 1 k 2 .t{(λx 1 k 1 k 2 .k 1 x 1 (λx 2 .k 1 x 2 k 2 ))/k} γ k 2 with γ = λxk 2 .k 2 x Figure 1: Definitional CPS translation of λ S (λx.t) v = t{v/x} β v (λx.E [x]) t = E [t] if x / ∈ fv(E ) β Ω E [Sk.t] = t{λx. E [x] /k} if x / ∈ fv(E ) • S (λx.t 0 ) t 1 = (λx. t 0 ) t 1 • lift v = v • val Sk. t = Sk.t S • λx.v x = v if x / ∈ fv(v) η v Sk.k t = t if k / ∈ fv(t) S elim
λk 1 k 2 .(λx 2 k 1 k 2 .y x 2 γ (λx 3 .k 1 x 3 k 2 )) x (λx 1 k 2 .z x 1 γ k 2 ) (λx 0 .x x 0 k 1 k 2 )
where the computations are sequentialized according to the evaluation strategy in the source calculus.

The CPS translation for shift and reset induces the following notion of equivalence on λ S terms. Definition 2.11. Terms t and t are CPS equivalent, written t ≡ t , if their CPS translations are βη-convertible, where βη-convertibility is the smallest congru-ence containing the relations → β and → η :

(λx.t) t → β t{t /x} λx.t x → η t if x / ∈ fv(t)
For example, the reduction rules t → v t given in Section 2.2 are sound w.r.t. CPS because CPS translating t and t yields βη-convertible terms in the λcalculus.

The CPS equivalence has been characterized in terms of direct-style equations by Kameyama and Hasegawa, who developed a sound and complete axiomatization of shift and reset [START_REF] Kameyama | A sound and complete axiomatization of delimited continuations[END_REF]: two λ S terms are CPS equivalent iff one can derive their equality using the equations of Figure 2.

The axiomatization is a source of examples for the bisimulation techniques that we study in Sections 4, 5 and 6, and it allows us to relate the notion of CPS equivalence to the notions of contextual equivalence that we introduce in Section 3. In particular, we show that all but one axiom are validated by the bisimilarities for the relaxed semantics, and that all the axioms are validated by the equivalences of the original semantics. The discriminating axiom that confirms the discrepancy between the two semantics is S elim -the only equation that hinges on the existence of the top-level reset.

It might be possible to consider alternative CPS translations for shift and reset, e.g., as given in [START_REF] Materzok | Subtyping delimited continuations[END_REF], that correspond to the relaxed semantics. Such CPS translations require a recursive structure of continuations, which makes it hard to reason about the image of the translations, and, moreover, the operational correspondence between the relaxed semantics and such CPS translations is not as tight as between the original semantics and the original CPS translation considered in this section. Devising a respective axiomatization to be validated by the bisimilarity theories presented in this work is a research path beyond the scope of the present article.

Contextual Equivalence

In this section, we discuss the possible definitions of a Morris-style contextual equivalence for the calculus λ S . As usual, the idea is to express that two terms are equivalent if and only if they cannot be distinguished when put in an arbitrary context. The question is then what kind of behavior we want to observe. We discuss this issue for the two semantics considered in this paper.

Definition for the Relaxed Semantics

We first discuss the definition of contextual equivalence for closed terms, before extending it to open terms. As in the regular λ-calculus, we could observe only if a term reduces to a value or not, leading to the following relation. Definition 3.1. Let t 0 , t 1 be closed terms. We write

t 0 C 1 t 1 if for all closed C , C [t 0 ] ⇓ v v 0 for some v 0 implies C [t 1 ] ⇓ v v 1 for some v 1 , and conversely for C [t 1 ].

RR n°9096

But in λ S , the evaluation of closed terms generates not only values, but also control stuck terms. Taking this into account, a more fine-grained definition of contextual equivalence would be as follows.

Definition 3.2. Let t 0 , t 1 be closed terms. We write

t 0 C 2 t 1 if for all closed C , • C [t 0 ] ⇓ v v 0 for some v 0 iff C [t 1 ] ⇓ v v 1 for some v 1 ; • C [t 0 ] ⇓ v t 0 for some control stuck term t 0 iff C [t 1 ] ⇓ v t 1 for some control stuck term t 1 .
This definition can actually be formulated in a simpler way, where we do not distinguish cases based on the possible normal forms.

Proposition 3.3. We have t 0 C 2 t 1 iff for all closed C , C [t 0 ] ⇓ v iff C [t 1 ] ⇓ v . Proof. Suppose that C [t 0 ] ⇓ v iff C [t 1 ] ⇓ v holds.
We prove that we have t 0 C 2 t 1 (the reverse implication is immediate). Assume there exists C such that C [t 0 ] ⇓ v t 0 with t 0 control stuck, and

C [t 1 ] ⇓ v v 1 . Then C [t 0 ] Ω ⇓ v t 0 Ω (t 0 Ω is control stuck), and C [t 1 ] Ω → * v v 1 Ω ⇑ v .
The context C Ω distinguishes t 0 and t 1 , hence a contradiction. Therefore, if C [t 0 ] evaluates to a control stuck term, then so does C [t 1 ], and similarly for evaluation to values.

By the definitions, it is clear that C 2 ⊆ C 1 . The inclusion is strict, because of terms such as Sk.Ω, which are control stuck terms but diverge when unstuck. Indeed, we have Sk.Ω C 2 Ω, because Sk.Ω is a stuck term, but not Ω and, therefore, the second item of Definition 3.2 is violated. However, they are related by C 1 . Proposition 3.4. We have Sk.Ω C 1 Ω.

Proof. Let C be such that C [Sk.Ω] ⇓ v v 0 for some v 0 . Then we prove that C [Ω] reduces to a value as well; in fact, C does not evaluate the term that fills its hole. We define multi-holes contexts H by the following grammar

H ::= | x | λx.H | H H | Sk.H | H
and we write H [t] for the plugging of t in all the holes of H . By case analysis on → v , we can see that if

C [Sk.Ω] → v t , then there exists a multi-hole context H such that t = H [Sk.Ω] and C [Ω] → v H [Ω]. In particular, we can- not have C = F [ E ], otherwise we would have C [Sk.Ω] ⇑ v . Consequently, C [Sk.Ω] ⇓ v v 0 implies that there exists a mutli-hole context H such that v 0 = λx.H [Sk.Ω], and C [Ω] ⇓ v λx.H [Ω]. Conversely, if C [Ω] ⇓ v v 1 , we can prove that C [Sk.Ω] ⇓ v v
for some v using the same reasoning. Therefore, we have Sk.Ω C 1 Ω.

The relation C 2 is more precise than C 1 about the behavior of terms. Therefore, we chose to work with C 2 as the main contextual equivalence for the relaxed semantics. Henceforth, we simply write C for C 2 .

RR n°9096

The relation C is defined on closed terms, but can be extended to open terms using closing substitutions: we say σ closes t if it maps the free variables of t to closed values. The open extension of a relation, written R • , is defined as follows.

Definition 3.5. Let R be a relation on closed terms, and t 0 and t 1 be open terms. We write t 0 R • t 1 if for every substitution σ which closes t 0 and t 1 , t 0 σ R t 1 σ holds.

Remark 3.6. Contextual equivalence can be defined directly on open terms by requiring that the context C binds the free variables of the related terms. We prove the resulting relation is equal to C • in Section 5.4.

To prove completeness of bisimilarities, we use a variant of C which takes into account only evaluation contexts to compare terms. Definition 3.7. Let t 0 , t 1 be closed terms. We write

t 0 D t 1 if for all closed F , • F [t 0 ] ⇓ v v 0 for some v 0 iff F [t 1 ] ⇓ v v 1 for some v 1 ; • F [t 0 ] ⇓ v t 0 for some control stuck term t 0 iff F [t 1 ] ⇓ v t 1 for some control stuck term t 1 .
The definitions imply C ⊆ D. While proving completeness of applicative bisimilarity in Section 5, we also prove D = C, which means that testing with evaluation contexts is as discriminating as testing with any contexts. Such a simplification result is similar to Milner's context lemma [START_REF] Milner | Fully abstract models of typed λ-calculi[END_REF].

The relations C 1 and C 2 are not suitable for the original semantics, because they distinguish terms that should be equated according to Kameyama and Hasegawa's axiomatization. Indeed, according to these relations, Sk.k v (where k / ∈ fv(v)) cannot be related to v (axiom S elim in Figure 2), because a stuck term cannot be related to a value. In the next section, we discuss a definition of contextual equivalence for the original semantics.

Definition for the Original Semantics

To reflect the fact that in the original semantics terms are evaluated within an enclosing reset, the contextual equivalence we consider for the original semantics tests terms in contexts of the form C only. Because delimited terms cannot reduce to stuck terms (Proposition 2.9), the only possible observable action is evaluation to values. We, therefore, define contextual equivalence for the original semantics as follows.

Definition 3.8. Let t 0 , t 1 be closed terms. We write

t 0 P t 1 if for all closed C , C [t 0 ] ⇓ v v 0 for some v 0 iff C [t 1 ] ⇓ v v 1 for some v 1 .
The relation P is defined on all (closed) terms, not just delimited ones. The resulting relation is less discriminating than C, because P uses contexts of a particular form, while C tests with all contexts. Proposition 3.9. We have C ⊆ P.

As a result, any equivalence between terms we prove for the relaxed semantics also holds in the original semantics, and any bisimilarity sound w.r.t. C (like the bisimilarities we define in Sections 4, 5, and 6.1) is also sound w.r.t. P. However, to reach completeness, we have to design a bisimilarity suitable for delimited terms (see Section 6.5). As for the relaxed semantics, we extend P to open terms using Definition 3.5.

The inclusion of Proposition 3.9 is strict; in particular, P verifies the axiom S elim , while C does not. In fact, we prove in Section 4.7 that P contains the CPS equivalence ≡. The reverse inclusion holds neither for P nor C: there exist contextually equivalent terms that are not CPS equivalent. Proposition 3.10.

1. We have Ω P ΩΩ (respectively

Ω C ΩΩ), but Ω ≡ ΩΩ. 2. We have Θ P ∆ (respectively Θ C ∆), but Θ ≡ ∆.
The contextual equivalences C and P put all diverging terms in one equivalence class, while CPS equivalence is more discriminating. Furthermore, as is usual with equational theories for λ-calculi, CPS equivalence is not strong enough to equate Turing's and Curry's (call-by-value) fixed-point combinators.

As explained in the introduction, contextual equivalence is difficult to prove in practice for two given terms because of the quantification over contexts. We look for a suitable replacement (that is, an equivalence that is at least sound w.r.t. C or P) by studying different styles of bisimulation in the next sections.

Normal-Form Bisimilarity

Normal-form bisimilarity [START_REF] Lassen | Eager normal form bisimulation[END_REF] (originally defined in [START_REF] Sangiorgi | The lazy lambda calculus in a concurrency scenario[END_REF], where it was called open bisimilarity) equates (open) terms by reducing them to normal form, and then requiring the sub-terms of these normal forms to be bisimilar. Unlike applicative and environmental bisimilarities (studied in the next sections), normalform bisimilarity usually does not contain a universal quantification over testing terms or contexts in its definition, and is therefore easier to use than the former two. However, it is also usually not complete w.r.t. contextual equivalence, meaning that there exist contextually equivalent terms that are not normal-form bisimilar.

A notion of normal-form bisimulation has been defined in various calculi, including the pure λ-calculus [START_REF] Lassen | Bisimulation in untyped lambda calculus: Böhm trees and bisimulation up to context[END_REF][START_REF] Lassen | Eager normal form bisimulation[END_REF], the λ-calculus with ambiguous choice [START_REF] Lassen | Normal form simulation for McCarthy's amb[END_REF], the λµ-calculus [START_REF] Lassen | Head normal form bisimulation for pairs and the λµ-calculus[END_REF], and the λµρ-calculus [START_REF] Støvring | A complete, co-inductive syntactic theory of sequential control and state[END_REF], a calculus with control and store, where normal-form bisimilarity characterizes contextual equivalence. It has also been defined for typed languages [START_REF] Lassen | Typed normal form bisimulation[END_REF][START_REF] Lassen | Typed normal form bisimulation for parametric polymorphism[END_REF]. In this section, we discuss how we can define normal-form bisimilarity for the relaxed semantics of λ S , and then propose up-to techniques and other improvements. We then define a normal-form bisimilarity dedicated to the original semantics.

Definition of on values:

x y def = x y λx.t y def = t{y/x}
Definitions of R NFη on normal forms and of R C on contexts

E 0 [x] R E 1 [x]
x fresh

E 0 R C E 1 E 0 [x] R E 1 [x] F 0 [x] R F 1 [x]
x fresh

F 0 [ E 0 ] R C F 1 [ E 1 ] v 0 x R v 1 x x fresh v 0 R NFη v 1 E 0 R C E 1 t 0 R t 1 E 0 [Sk.t 0 ] R NFη E 1 [Sk.t 1 ] F 0 R C F 1 v 0 R NFη v 1 F 0 [x v 0 ] R NFη F 1 [x v 1 ]
Figure 3: Definitions of the operator and of the relations R NFη and R C

Definition

In the λ-calculus [START_REF] Sangiorgi | The lazy lambda calculus in a concurrency scenario[END_REF][START_REF] Lassen | Eager normal form bisimulation[END_REF], the definition of normal-form bisimilarity has to take into account only values and open stuck terms. In λ S with the relaxed semantics, we have to relate also control stuck terms; we propose here a first way to deal with these terms, that will be refined in the next subsection. Deconstructing normal forms leads to comparing contexts as well as terms. Given a relation R on terms, we define in Figure 3 an extension of R to normal forms, written R NFη , which relies on an application operator for values and on a relation R C on contexts. The rationale behind these definitions becomes clear when we explain our notion of normal-form bisimilarity, defined below. Definition 4.1. A relation R on terms is a normal-form simulation if t 0 R t 1 and t 0 ⇓ v t 0 implies that there exists t 1 such that t 1 ⇓ v t 1 and t 0 R NFη t 1 . A relation R is a normal-form bisimulation if both R and R -1 are normal-form simulations. Normal-form bisimilarity, written N, is the largest normal-form bisimulation.

In this section, we often drop the "normal-form" attribute when it does not cause confusion. Two terms t 0 and t 1 are bisimilar if their evaluations lead to matching normal forms (e.g., if t 0 evaluates to a control stuck term, then so does t 1 ) with bisimilar sub-components. We now detail the different cases.

Normal-form bisimilarity does not distinguish between evaluation to a variable and evaluation to a λ-abstraction. Instead, we relate terms evaluating to any values v 0 and v 1 by comparing v 0 x and v 1 x, where x is fresh. As originally pointed out by Lassen [START_REF] Lassen | Eager normal form bisimulation[END_REF], this is necessary for the bisimilarity to be sound w.r.t. η-expansion; otherwise it would distinguish η-equivalent terms such as λy.x y and x. Using instead of regular application avoids the introduction of unnecessary β-redexes, which could reveal themselves problematic in proofs.

For a control stuck term E 0 [Sk.t 0 ] to be executed, it has to be plugged into a pure evaluation context surrounded by a reset; by doing so, we obtain a term of the form t 0 {λx. E 0 [x] /k} for some context E 0 . Notice that the resulting term is within a reset; similarly, when comparing E 0 [Sk.t 0 ] and E 1 [Sk.t 1 ], we ask for the shift bodies t 0 and t 1 to be related when surrounded by a reset. We also compare E 0 and E 1 , which amounts to executing E 0 [x] and E 1 [x] for a fresh x, since the two contexts are pure. Comparing t 0 and t 1 without reset would be too discriminating, as it would distinguish contextually equivalent terms such as Sk.

[x v 0 ] and F 1 [x v 1 ]
are bisimilar if the values v 0 and v 1 as well as the contexts F 0 and F 1 are related. We have to be careful when defining bisimilarity on (possibly non pure) evaluation contexts. We cannot simply relate F 0 and F 1 by executing F 0 [y] and F 1 [y] for a fresh y. Such a definition would equate the contexts and , which in turn would relate the terms x v and x v , which are not contextually equivalent: they are distinguished by the context (λx. ) λy.Sk.Ω. A context containing a reset enclosing the hole should be related only to contexts with the same property. However, we do not want to precisely count the number of delimiters around the hole; doing so would distinguish and , and, therefore, it would discriminate the contextually equivalent terms x v and x v . Hence, the definition of R C (Figure 3) checks that if one of the contexts contains a reset surrounding the hole, then so does the other; then it compares the contexts beyond the first enclosing delimiter by simply evaluating them using a fresh variable. As a result, it rightfully distinguishes and , but it relates and . As a first basic result about normal-form bisimilarity, we show that → v (and hence,

⇓ v ) is included in N. Proposition 4.2. If t → v t , then t N t .
Proof. Because the calculus is deterministic, t ⇓ v t iff t ⇓ v t , and it is easy to check that the identity relation {(t, t) | t ∈ T } is a normal-form bisimulation.

We now give some examples to show how to prove equivalences using normalform bisimulation.

Example 4.3 (double reset). We prove that t N t by showing that

R def = {( t , t ) | t ∈ T } ∪ N is a bisimulation. First, note that the case t ⇓ v E [Sk.t ] is not possible because of Proposition 2.9. Then, we prove that t ⇓ v v iff t ⇓ v v. If t ⇓ v v, then t → * v v → v v. Conversely, if t ⇓ v v
[y] R E [y] (true because N ⊆ R). Similarly, if t ⇓ v F [x v],
then by Proposition 2.9, there exists F such that F = F . Then t cannot evaluate to a control stuck term (because it is a delimited term), and it cannot evaluate to a value (otherwise, t would evaluate to this value). Therefore, we have t ⇓ v F [x v]. In turn, this implies that there exists F such that F = F (using Proposition 2.9 again). Consequently, we have t ⇓ v F [x v] and t ⇓ v F [x v] , so we can conclude as in the previous case.

The relation R is therefore a bisimulation, meaning that R ⊆ N. Because we have t R t , we also have t N t , as wished.

Example 4.4 (fixed-point combinators). We study here the relationships between Turing's and Curry's fixed-point combinator and their respective variants with delimited control [START_REF] Danvy | A functional abstraction of typed contexts[END_REF] (see Example 2.2 for the definitions). First, we prove that Turing's combinator Θ is bisimilar to its variant Θ S def = θ Sk.k k . We build the candidate relation R incrementally, starting from (Θ, Θ S ). Evaluating these two terms, we obtain Θ ⇓ v λy.y (λz.θ θ y z) def = v 0 , and

Θ S ⇓ v λy.y (λz.(λx. θ x ) (λx. θ x ) y z) def = v 1 .
We, therefore, extend R with (v 0 y, v 1 y), where y is fresh. These two new terms are open stuck, so we add their decomposition to R. Let v 0 def = λz.θ θ y z and v 1 def = λz.(λx. θ x ) (λx. θ x ) y z; then we add (v 0 z, v 1 z) and (z, z) for a fresh z to R. Evaluating v 0 z and v 1 z, we obtain respectively y v 0 z and y v 1 z; to relate these two open stuck terms, we just need to add (x z, x z) (for a fresh x) to R, since we already have v 0 R NFη v 1 . The constructed relation R we obtain is a normal-form bisimulation.

In contrast, Curry's combinator ∆ is not bisimilar to its delimited-control variant ∆ S def = λx. δ x Sk.k k . Indeed, evaluating the bodies of the two values, we obtain respectively x (λz.δ x δ x z) and x (λz.(λy. δ x y ) (λy. δ x y ) z) , and these open stuck terms are not bisimilar, because is not related to by N C . In fact, ∆ and ∆ S are not contextually equivalent, as they are distinguished by the context λx.Sk.Ω. Finally, we can prove that the two original combinators Θ and ∆ are bisimilar, using the same bisimulation as in [START_REF] Lassen | Eager normal form bisimulation[END_REF].

Soundness and Completeness

Usual congruence proofs for normal-form bisimilarities include direct proofs, where a context and/or substitutive closure of the bisimilarity is proved to be itself a bisimulation [START_REF] Lassen | Bisimulation in untyped lambda calculus: Böhm trees and bisimulation up to context[END_REF][START_REF] Lassen | Normal form simulation for McCarthy's amb[END_REF][START_REF] Støvring | A complete, co-inductive syntactic theory of sequential control and state[END_REF], or proofs based on CPS translations [START_REF] Lassen | Eager normal form bisimulation[END_REF][START_REF] Lassen | Head normal form bisimulation for pairs and the λµ-calculus[END_REF]. The CPS approach consists in proving a CPS-based correspondence between the bisimilarity R 1 we want to prove sound and a relation R 2 that we already know is a congruence. Because CPS translations are usually themselves compatible, we can then conclude that R 1 is a congruence. For example, for the λ-calculus, Lassen proved a CPS-correspondence between eager normal-form bisimilarity and Böhm trees equivalence [START_REF] Lassen | Eager normal form bisimulation[END_REF]. In this section, we use the relaxed semantics, but the CPS translation corresponds to the original one; we, therefore, cannot rely on a CPS-based proof method.

Instead, we follow a direct approach and define a closure that we prove to be a bisimulation. We only sketch the proof here, because the complete proof (available in Appendix A.1) requires a lot of auxiliary notations and definitions. The idea is to consider pairs of terms of the form (

-→ F 0 [t 0 ] -→ σ 0 , -→ F 1 [t 1 ] -→ σ 1 )
, where -→ F 0 , -→ F 1 , (respectively t 0 , t 1 , and -→ σ 0 , -→ σ 1 ) are contexts (respectively terms, and substitutions) pairwise related by N (with some extra conditions), and show that they are normal-form bisimilar. This implies that N is substitutive and compatible w.r.t. evaluation contexts. We can then prove separately compatibility w.r.t. λ-abstraction and shift easily. We deduce that N is sound w.r.t. contextual equivalence. Theorem 4.6. We have N ⊆ C. The following counter-example shows that the inclusion is in fact strict; normalform bisimilarity is not complete. Proposition 4.7. Let i def = λy.y. We have x i Sk.i C • x i ( x i Sk.i) , but x i Sk.i N x i ( x i Sk.i) .

Proof. We prove that x i Sk.i C • x i ( x i Sk.i) holds using applicative bisimilarity in Proposition 5.19. They are not normal-form bisimilar, because the terms y Sk.i and y ( x i Sk.i) (where y is fresh) are not bisimilar: the former evaluates to i while the latter is in normal form (but is not a value). Remark 4.8. Following Filinski's simulation of shift and reset in terms of call/cc and a single reference cell [START_REF] Filinski | Representing monads[END_REF], one can express the terms of the λ S -calculus in the λµρ-calculus [START_REF] Støvring | A complete, co-inductive syntactic theory of sequential control and state[END_REF]. Yet, Støvring and Lassen's normal-form bisimilarity is sound and complete with respect to the contextual equivalence of λµρ [START_REF] Støvring | A complete, co-inductive syntactic theory of sequential control and state[END_REF] (a calculus with store and a construct similar to call/cc), while our relation is only sound. It shows that λµρ is more expressive and can distinguish more terms than λ S . For example, the encodings of the two terms of Proposition 4.7 in λµρ would not be contextually equivalent in λµρ, since substituting for x a value that, e.g., increments a value of some reference cell, would lead to two different states that can be easily distinguished observationally. A more general and precise characterization of the relation between the two calculi is an interesting question, but it falls out of the scope of the present article.

Up-to Techniques

The idea behind up-to techniques [START_REF] Sangiorgi | The Pi-Calculus: A Theory of Mobile Processes[END_REF][START_REF] Lassen | Relational reasoning about contexts[END_REF][START_REF] Sangiorgi | Environmental bisimulations for higher-order languages[END_REF] is to define relations that are not exactly bisimulations but are included in bisimulations. It usually leads to definitions of simpler candidate relations and to simpler bisimulation proofs. Here, we discuss only bisimulation up to context (with also some limited form of up to reduction), one of the most powerful up-to technique, which allows to abstract away a common context during a bisimulation proof.

In contrast with normal-form bisimulation, the notion of bisimulation up to context we introduce does not respect η-expansion; we discuss why in Remark 4.14. To simplify the soundness proof, we also introduce some limited use of up to reduction in the definition. Given a relation R on terms, we write t 0 R t 1 if there exist t 0 , t 1 such that t 0 → * v t 0 , t 1 → * v t 1 , and t 0 R t 1 . We also define relations R NF and normal forms and R C on contexts as follows:

E 0 [x] R E 1 [x]
x fresh

E 0 R C E 1 E 0 [x] R E 1 [x] F 0 [x] R F 0 [x]
x fresh

F 0 [ E 0 ] R C F 1 [ E 1 ] E 0 R C E 1 t 0 R t 1 E 0 [Sk.t 0 ] R NF E 1 [Sk.t 1 ] F 0 R C F 1 v 0 R NF v 1 F 0 [x v 0 ] R NF F 1 [x v 1 ] x R NF x t 0 R t 1 λx.t 0 R NF λx.t 1
The definitions of R C and R NF are the same as R C and R NFη on pure contexts, and on control and open stuck terms, respectively. Values are related without using , which means that two η-equivalent values can no longer be related. Finally, the clause for general evaluation contexts uses up to reduction in one of the premises. Next, we define the substitutive, reflexive, and context closure R of a relation R by the rules of Figure 4. Note that we have two rules for compatibility w.r.t. evaluation contexts: two terms that are not both delimited can be plugged only in contexts F 0 , F 1 related by R C . Two delimited terms may in addition be put into contexts F 0 , F 1 verifying F 0 [x] R F 0 [x] for a fresh x, which is a weaker constraint than F 0 R C F 1 . This extra case for delimited terms helps in the proof of soundness of the technique, and we remind it would not be sound to put any terms in contexts verifying only F 0 [x] R F 0 [x], as explained in Section 4.1.

We can now define bisimulation up to substitutive, reflexive, and context closure (in short, up to context) as follows.

t R t t 0 R t 1 t 0 R t 1 t 0 R t 1 v 0 R NF v 1 t 0 {v 0 /x} R t 1 {v 1 /x} t 0 R t 1 F 0 R C F 1 F 0 [t 0 ] R F 1 [t 1 ] t 0 R t 1 t 0 , t 1 delimited F 0 [x] R F 1 [x]
x fresh In a bisimulation up to context R, the results of the evaluations of two terms are compared using the closure R, instead of using simply R itself. Because R is larger than R, it is easier to obtain terms related by R rather than R. For example, we can simplify the proof of bisimilarity between Turing's fixed point combinator Θ and its delimited-control variant Θ S (cf. Example 4.4).

F 0 [t 0 ] R F 1 [t 1 ] t 0 R t 1 λx.t 0 R λx.t 1 t 0 R
Θ S ⇓ v λy.y (λz.(λx. θ x ) (λx. θ x ) y z) def = v 1 .
The bodies of v 0 and v 1 share the common context y (λz. y z), and the two terms filling the holes (respectively Θ and (λx. θ x ) (λx. θ x )) are in R, so we have v 0 R NF v 1 . The terms Θ and (λx. θ x ) (λx. θ x ) also reduce respectively to v 0 and v 1 , hence the result holds.

We now prove the soundness of the up to context technique. For this, we define non-η bisimulation up to reduction, an up-to relation which uses R NF instead of R NFη . Definition 4.11. A relation R on terms is a non-η simulation up to reduction if t 0 R t 1 and t 0 ⇓ v t 0 implies that there exists t 1 such that t 1 ⇓ v t 1 and t 0 R NF t 1 . A relation R is a non-η bisimulation up to reduction if both R and R -1 are non-η simulations up to reduction. Lemma 4.12. If R is a non-η bisimulation up to reduction, then R ⊆ N.

Proof. By showing that {(t 0 , t 1 ) | ∃t 0 , t 1 , t 0 → * v t 0 ∧ t 1 → * v t 1 ∧ t 0 R t 1 } is a normal-form bisimulation. Proposition 4.13. If R is a normal-form bisimulation up to context, then R is a non-η bisimulation.
More precisely, we prove in Appendix A.2 that if t 0 R t 1 and t 0 ⇓ v t 0 in m steps or less, then there exists t 1 such that t 1 ⇓ v t 1 and t 0 R NF t 1 . The proof is by induction on m and the definition of t 0 R t 1 , ordered lexicographically. As a result, if R is a bisimulation up to context, and if

t 0 R t 1 , then t 0 N t 1 , because R ⊆ R ⊆ N.
Remark 4.14 (η-expansion). We cannot prove Proposition 4.13 if we use in R NF , as in R NFη . With η-expansion, one of the inductive cases of the proof would require a result stating that x y R t implies t ⇓ v t and x y R NFη t . But proving this result is as difficult as proving Proposition 4.13 directly. This issue is not specific to the calculus, as it arises in the plain λ-calculus as well, but to the proof technique. The only proof of soundness of an up to context technique which respects η-expansion can be found in [START_REF] Lassen | Eager normal form bisimulation[END_REF], where the author uses a CPS translation, not a direct proof (see our discussion about CPS translations vs direct proofs in Section 4.2).

When proving equivalence of terms, it is sometimes easier to reason in a small-step fashion instead of trying to evaluate terms completely. To allow this kind of reasoning, we define small-step bisimulation up to context as follows.

Definition 4.15. A relation R on terms is a small-step normal-form simulation up to context if t 0 R t 1 implies:

• if t 0 → v t 0 , then there exists t 1 such that t 1 → * v t 1 and t 0 R t 1 ;
• if t 0 is a normal form, then there exists t 1 such that t 1 ⇓ v t 1 and t 0 R NF t 1 .

A relation R is a small-step normal-form bisimulation up to context if both R and R -1 are small-step normal-form simulations up to context.

Note that the small step style is not specific to up to context, and can be used also with Definition 4.1. We can easily adapt the proof of Proposition 4.13 to prove the soundness of small step bisimulation up to context. Proposition 4.16. If R is a small-step normal-form bisimulation up to context, then R is a non-η bisimulation up to reduction.

The next example demonstrates how useful small-step relations can be.

Example 4.17. We prove that if x / ∈ fv(E ), then (λx.

E [x] ) t N E [t] . Let R def = {( (λx. E [x] ) t , E [t] ) | t ∈ T , E ∈ PC, x / ∈ fv(E )}.
We prove that R ∪ N is a small-step bisimulation up to context, by case analysis on t.

RR n°9096

• If t → v t , then (λx. E [x] ) t → v (λx. E [x] ) t , E [t] → v E [t ] , and
we have (λx. E [x] ) t R E [t ] , as required.

• If t = v, then (λx. E [x] ) v → v E [v] . We have proved in Example 4.3 that E [v] N E [v] . • If t = F [yv], then we have to relate (λx. E [x] ) F and E [F ] (we already have v N NF v). If F = F [ E ], then we have (λx. E [x] ) F [z] R E [F [z]] and E [z] N E [z] for a fresh z. If F = E , then we have (λx. E [x] ) E [z] R E [E [z]
] for a fresh z. Without using small-step bisimulation, the definition of R as well as the above bisimulation proof would be much more complex, since we would have to compute the results of the evaluations of (λx. E [x] ) t and of E [t] , which is particularly difficult if t is a control stuck term.

• If t = E [Sk.t ], then (λx. E [x] ) t → v t

Refined Normal-Form Bisimilarity

We propose in this subsection a refinement of the definition of normal-form bisimilarity. Indeed, Definition 4.1 is too discriminating with control stuck terms, as we can see with the following terms. Proof. We can easily prove that Sk.i C (Sk.i) Ω holds with applicative bisimilarity or Definition 4.19. They are not normal-form bisimilar, since the contexts and Ω are not related by N NFη (x converges while x Ω diverges).

When comparing control stuck terms, normal-form bisimilarity considers contexts and shift bodies separately, while they are combined if the control stuck terms are put under a reset and the capture goes through. To fix this issue, we consider another notion of bisimulation. Given a relation R on terms, we define R RNFη on normal forms, which changes the way R NFη operates on control stuck terms:

t 0 R NFη t 1 t 0 , t 1 not control stuck t 0 R RNFη t 1 t 0 {λx. k E 0 [x] /k} R t 1 {λx. k E 1 [x] /k} k , x fresh E 0 [Sk.t 0 ] R RNFη E 1 [Sk.t 1 ]
The rule for control stuck terms simulates the capture of E 0 (respectively E

⇓ v E 0 [Sk.t 0 ], then t 1 ⇓ v E 1 [Sk.t 1 ]
, with E 0 N NFη E 1 , and t 0 N t 1 . Because N is a congruence (Theorem 4.5) and substitutive, it is easy to see that

t 0 {λx. k E 0 [x] /k} N t 1 {λx. k E 1 [x] /k}
holds for fresh k and x. Therefore, N is a refined bisimulation, and is included in R. The inclusion is strict, because R relates the terms of Proposition 4.18, while N does not.

Soundness. Proving that R is sound requires some adjustments to the congruence proof of N. We introduce a special kind of substitution (called context substitution) t{E /k}, which replaces a variable in function position with a pure context. This operation is the same as the replacement of names with contexts in the λµ-calculus [START_REF] Parigot | λµ-calculus: an algorithmic interpretation of classical natural deduction[END_REF]. Proof. By case analysis on the reduction rules.

x{E /k} def = x if x = k (λx.
Henceforth, when we write t{E /k}, we assume that wf k (t) holds. To prove the congruence of R, we proceed as in Section 4.2, and consider pairs of terms of the form (

-→ F 0 [t 0 ] -→ σ 0 , -→ F 1 [t 1 ] -→ σ 1 )
, except now sequences of substitutions -→ σ range over value and context substitutions. When these terms reduce to control stuck terms, we use context substitution to conclude. The complete congruence proof can be found in Appendix A.3. The inclusion is strict, because the terms of Proposition 4.7 are still not related by R. We would like to stress that even though R equates more contextually equivalent terms than N, the latter is still useful, since it leads to very simple proofs of equivalence, as we can see, e.g., with the examples of Section 4.5. Therefore, R does not disqualify N as a proof technique. Proving this result with the regular normal-form bisimulation would require us to equate E [y] and y (where y is fresh), which is clearly not true in general (take, for instance, E = (λz.Ω) ).

Example 4.25. We prove that if k / ∈ fv(E ) ∪ fv(t) and x / ∈ fv(E ), then E [Sk.t] R Sk .t{λx. k E [x] /k}.
Bisimulation up to context. We can also define a notion of bisimulation up to context sound w.r.t. refined bisimilarity. As in the regular case, our proof technique fails with a refined up-to technique which respects η-expansion. Given a relation R on terms, we, therefore, define R RNF as follows

t 0 R NF t 1 t 0 , t 1 not control stuck t 0 R RNF t 1 t 0 {λx. k E 0 [x] /k} R t 1 {λx. k E 1 [x] /k} k , x fresh E 0 [Sk.t 0 ] R RNF E 1 [Sk.t 1 ]
We can then define refined non-η bisimulation up to reduction as in Definition 4.11, replacing R NF with R RNF . Finally, we define the closure R by the rules in Figure 5, which are basically the same as in Figure 4, with an extra rule for context substitution. In this rule, we relate the contexts E 0 , E 1 within an enclosing reset, because we substitute them for variables that are in subterms of the form k t ; consequently, we know that they will be executed with a surrounding reset. We then define refined bisimulation up to context as follows.

t R t t 0 R t 1 t 0 R t 1 t 0 R t 1 v 0 R RNF v 1 t 0 {v 0 /x} R t 1 {v 1 /x} t 0 R t 1 E 0 R C E 1 t 0 {E 0 /k} R t 1 {E 1 /k} t 0 R t 1 F 0 R C F 1 F 0 [t 0 ] R F 1 [t 1 ] t 0 R t 1 t 0 , t 1 delimited F 0 [x] R F 1 [x]
x fresh In the cases featuring control stuck terms, we rely on context substitution to conclude (see Appendix A.3 for more details).

F 0 [t 0 ] R F 1 [t 1 ] t 0 R t 1 λx.t 0 R λx.t 1 t 0 R t 1 Sk.t 0 R Sk.t 1 Figure 5: Refined closure of a relation R Definition 4.26. A relation R on terms is a refined normal-form simulation up to context if t 0 R t 1 and t 0 ⇓ v t 0 implies that there exists t 1 such that t 1 ⇓ v t 1 and t 0 R RNF t 1 . A relation R is a refined normal-form

Proving the Axioms

We now show how the axioms can be proved using normal-form bisimulation. Because we have so far been working with the relaxed semantics, we remind that the S elim axiom does not hold, as discussed in Section 3.1. We show how to prove the S elim axiom with the delimited normal-form bisimulation of the next section. The η-equivalence axiom (η v axiom) holds by definition of N NFη . Proposition 4.28 (β v , • S , and • val axioms). We have

(λx.t) v N t{v/x}, E [Sk.t] N t{λx. E [x] /k} (x fresh), and v N v.
Proof. These are direct consequences of Proposition 4.2. Proposition 4.29 (S • axiom). We have Sk. t N Sk.t.

RR n°9096

Proof. We want to relate two stuck terms, so using normal-form bisimulation, we have to show t N t (proved in Example 4.3) and N C (a consequence of the fact that N is reflexive).

Proposition 4.30 ( • lift axiom). We have (λx.t 0 ) t 1 N (λx. t 0 ) t 1 . Proof. We prove that R def = {( (λx.t 0 ) t 1 , (λx. t 0 ) t 1 ) | (t 0 , t 1 ) ∈ T 2 } ∪ {(t, t) | t ∈ T } is a normal-form bisimulation.
The terms (λx.t 0 ) t 1 and (λx. t 0 ) t 1 reduce to a normal form iff t 1 reduces to a normal form, and according to Proposition 2.9, we have two cases.

If

t 1 ⇓ v v, then (λx.t 0 ) t 1 → * v t 0 {v/x} and (λx. t 0 ) t 1 → * v t 0 {v/x} . Therefore, (λx.t 0 ) t 1 ⇓ v t iff (λx. t 0 ) t 1 ⇓ v t ,
) t 1 ⇓ v (λx.t 0 ) F [y v] and also (λx. t 0 ) t 1 ⇓ v (λx. t 0 ) F [y v] . We have v R NFη v, and it is easy to check that (λx.t 0 ) F R C (λx. t 0 ) F holds, whether F is pure or not. Proposition 4.31 (β Ω axiom). If x / ∈ fv(E ), then (λx.E [x]) t N E [t].
Proof. We prove that

R def = {((λx.E [x]) t, E [t]) | t ∈ T , E ∈ PC, x / ∈ fv(E )} ∪ {(t, t) | t ∈ T } is a normal-form bisimulation. If (λx.E [x]
) t evaluates to some normal form, then t evaluates to some normal form as well. We distinguish three cases.

If t ⇓ v v, then (λx.E [x]) t → * v E [v] (because x / ∈ fv(E ))
, and

E [t] → * v E [v]
. We obtain the same term in both cases, and from there, it is easy to conclude.

If

t ⇓ v F [y v], then (λx.E [x]) t ⇓ v (λx.E [x]) F [y v],
and

E [t] ⇓ v E [F [x v]]. We have to prove v R NFη v, which is obvious, and (λx.E [x]) F R C E [F ]. Let z be a fresh variable. If F is a pure context E , we have to prove (λx.E [x]) E [z] R E [E [z]], which is clearly true. Otherwise F = F [ E ], and we have to prove (λx.E [x]) F [z] R E [F [z]], which is clearly true, and E [z] R E [z] , which is true as well because R contains the identity relation. If t ⇓ v E [Sk.t ], then we have (λx.E [x]) t ⇓ v (λx.E [x]) E [Sk.t ],
and

E [t] ⇓ v E [E [Sk.t ]]. Let y be a fresh variable. We have to prove (λx.E [x]) E [y] R E [E [y]],
which is clearly true, and t R t , which is true as well.

Normal-Form Bisimulation for the Original Semantics

The relations defined so far are tailored for the relaxed semantics. We now propose a normal-form bisimulation for the original semantics, where a control stuck term can be equivalent to a term which does not evaluate to a stuck term. To do so, a simple idea would be to relate two terms t 0 and t 1 that are not delimited by comparing t 0 and t 1 : any potentially control stuck term would be "unstuck" by the surrounding reset. However, such a solution would not be sound, as it would relate Sk.k y and Sk.(λz.z) y, terms that can be distinguished by the context Ω .

To take into account the fact that t 0 and t 1 can be put in a context before being surrounded by a reset, we use the same technique as for refined bisimulation (Section 4.4): we compare k t 0 and k t 1 , where k is a fresh variable which stands for a potential (pure) evaluation context. As a result, we define delimited normal-form bisimulation as follows.

Definition 4.32. A relation R on terms is a delimited normal-form simulation if t 0 R t 1 implies:

• if t 0 , t 1 are not both delimited, then k t 0 R k t 1 holds for a fresh k; • otherwise, if t 0 ⇓ v t 0 , then there exists t 1 such that t 1 ⇓ v t 1 and t 0 R NFη t 1 .
A relation R is a delimited normal-form bisimulation if both R and R -1 are delimited normal-form simulations. Delimited normal-form bisimilarity, written M, is the largest delimited normal-form bisimulation.

Pairs of delimited terms are treated as in Definition 4.1, by reducing them to normal forms, which are then compared using R NFη . Note that delimited terms cannot reduce to control stuck terms (Proposition 2.9), therefore, the control stuck term case of the definition of R NFη becomes useless with delimited bisimulation. So, in fact, we use the restriction of R NFη to values and open stuck terms in Definition 4.32.

Example 4.33 (double reset). The terms t and t are delimited, therefore, we can prove they are delimited bisimilar by using the same bisimulation as in Example 4.3. In contrast, to equate Sk.t and Sk. t (S • axiom), we have to relate k Sk.t and k Sk. t for a fresh k . These two terms reduce to, respectively, t{λx. k x /k} and t{λx. k x /k} -two terms of the form t and t for some t ; they are, therefore, delimited bisimilar.

Actually, the regular and refined normal-form bisimulations can be used as proof techniques for delimited bisimilarity. Proof. We prove that N is a delimited normal-form bisimulation. For terms t 0 N t 1 which are both delimited, the definitions of N and M coincide. If t 0 N t 1 with t 0 or t 1 not delimited, we have to prove that k t 0 N k t 1 holds, which is true because N is a congruence. The reasoning is the same for R.

As a result, any terms already proved normal-form or refined bisimilar are delimited bisimilar, like, e.g., the axioms (Section 4.5). In particular, we have → v ⊆ M (and, therefore, ⇓ v ⊆ M).

RR n°9096

Soundness. We prove that M is a congruence in two steps: first, we show congruence on delimited terms, from which we can deduce congruence for all terms. For delimited terms, we proceed as in Sections 4.2 and 4.4, by considering terms of the form (

-→ F 0 [t 0 ] -→ σ 0 , -→ F 1 [t 1 ] -→ σ 1 )
, where t 0 and t 1 are delimited. As with refined bisimilarity, the above sequences of substitutions -→ σ contain value and context substitutions.

Because delimited bisimilarity compares two non-delimited terms t 0 , t 1 by turning them into delimited terms k t 0 , k t 1 , we can deduce compatibility w.r.t. evaluation contexts (application, reset) for all terms by considering k t 0 and k t 1 , and then substitute the appropriate contexts for k. Compatibility w.r.t. shift and λ-abstraction can then easily be proved separately. The complete proofs can be found in Appendix A.4. We deduce that M is sound w.r.t. P. Theorem 4.35. We have M ⊆ P.

However, M is not complete, since the terms of Proposition 4.7 are still related by P but not by M.

Bisimulation up to context. A notion of bisimulation up to context can be defined for the original semantics, which does not respect η-expansion (as in the relaxed semantics). Given a relation R, we consider R NF without its clause for control stuck terms, and we use the same closure R as with refined bisimulation up to context (Section 4.4); we remind that R contains a clause for context substitution. We define delimited bisimulation up to context as follows.

Definition 4.36. A relation R on terms is a delimited normal-form simulation up to context if t 0 R t 1 implies:

• if t 0 , t 1 are not both delimited, then k t 0 R k t 1 holds for a fresh k; • otherwise, if t 0 ⇓ v t 0 , then there exists t 1 such that t 1 ⇓ v t 1 and t 0 R NF t 1 .
A relation R is a delimited normal-form bisimulation up to context if both R and R -1 are delimited normal-form simulations up to context. It would not be sound to have k t 0 R k t 1 in the first item, because t 0 R t 1 implies k t 0 R k t 1 for any relation R. We prove that delimited bisimulation up to context is sound the same way as for the relaxed semantics, by defining a notion of delimited non-η bisimulation up to reduction, and we show the following result (see Appendix A.5). Lemma 4.37. Let R be a delimited bisimulation up to context. Let t 0 R t 1 .

1. If t 0 , t 1 are not both delimited, then for all fresh k, if k t 0 ⇓ v t 0 , there

exists t 1 such that k t 1 ⇓ v t 1 and t 0 R NF t 1 (and conversely if k t 1 ⇓ v t 1 ) .
2. If t 0 , t 1 are both delimited and t 0 ⇓ v t 0 , there exists t 1 such that t 1 ⇓ v t 1 and t 0 R NF t 1 (and conversely if t 1 ⇓ v t 1 ).

RR n°9096

This proves that if R is a delimited bisimulation up to context, then R is a delimited non-η bisimulation up to reduction, and is therefore contained in M. We can also define a small-step delimited bisimulation up to context and prove its soundness the same way. In the next section, we use delimited bisimulation up to context to prove the S elim axiom.

Examples

We illustrate the differences between the equivalences of the relaxed and original semantics by giving some examples of terms related by M (and, therefore, by P), but not by the contextual equivalence of the relaxed semantics C. First, note that M relates non-terminating terms with stuck non-terminating terms. As wished, M satisfies the only axiom of [START_REF] Kameyama | A sound and complete axiomatization of delimited continuations[END_REF] not satisfied by C.

Proposition 4.39 (S elim axiom). If k / ∈ fv(t), then t M Sk.k t.
Proof. The relation

{(t, Sk.k t), ( k t , k Sk.k t ), ( k t , (λx. k x ) t ) | t ∈ T , {k, k , x} ∩ fv(t) = ∅} ∪ M
is a small-step delimited bisimulation up to context. We have k Sk.k t → v (λx. k x ) t , and we can relate k t and (λx. k x ) t with up-to context as in Example 4.17.

Consequently, M is complete w.r.t. ≡.

Corollary 4.40. We have ≡ ⊆ M.

As a result, we can use ≡ as a proof technique for M (and, therefore, for P). E.g., the following equivalence can be derived from the axioms [START_REF] Kameyama | A sound and complete axiomatization of delimited continuations[END_REF].

Proposition 4.41. If k / ∈ fv(t 1 ), then (λx.Sk.t 0 ) t 1 M Sk.((λx.t 0 ) t 1 ).
• If t 1 = F 1 [y v 1 ], then we want to relate the contexts k ((λx.Sk.t 0 ) F 1 )
and (λx.t 0 {λy. k y /k}) F 1 (we already have

v 1 M NF v 1 ). If F 1 = F 1 [ E 1 ], then k ((λx.Sk.t 0 ) F 1 [z]) R (λx.t 0 {λy. k y /k}) F 1 [z] and E 1 [z] M E 1 [z] hold for a fresh z. If F 1 = E 1 , then we also have k ((λx.Sk.t 0 ) E 1 [z]) R (λx.t 0 {λy. k y /k}) E 1 [z]
for a fresh z.

• If t 1 = E 1 [Sk .t 1 ], then k ((λx.Sk.t 0 ) t 1 ) → v t 1 {λz. k ((λx.Sk.t 0 ) E 1 [z]) /k } and (λx.t 0 {λy. k y /k}) t 1 → v t 1 {λz. (λx.t 0 {λy. k y /k}) E 1 [z] /k } Because we have k ((λx.Sk.t 0 ) E 1 [z]) R (λx.t 0 {λy. k y /k}) E 1 [z] ,
we obtain two terms in R, as wished.

Finally, there exist also terminating terms in P but not in C which are not CPS equivalent. For example, if we combine Turing and Curry fixed-point combinators (see Example 2.2) with the S elim axiom, we obtain the following result.

Proposition 4.42. We have Sk.k Θ M ∆.

The bisimulation proof is the same as for Proposition 4.39.

Conclusion

In this section, we propose several definitions of normal-form bisimilarities as well as up-to techniques for the relaxed and original semantics of λ S . The first definition of normal-form bisimulation (Definition 4.1) separates the contexts and bodies of shift operators when testing control stuck terms, while refined bisimulation (Definition 4.19) consider the contexts and bodies combined. Building a candidate relation to prove the equivalence of two given terms and proving it is a bisimulation is easier to do with the first definition compared to the refined one, but the refined one relates strictly more terms.

The bisimulation for the original semantics (Definition 4.32) has to be able to relate a control stuck term with a term which reduces to, e.g., a value, as in the S elim axiom. To do so, we transform the pairs where at least one term is not delimited into pairs of delimited terms, by putting them inside a context k , where k is a fresh variable. We then treat pairs of delimited terms as before, except these terms cannot reduce to control stuck terms. In Section 4.7, we illustrate the differences between the relaxed and the original semantics by providing examples of terms that are equivalent with the original semantics but not with the relaxed one, like, in particular, the S elim axiom.

In the relaxed as well as in the original semantics, the proof obligations can be simplified further by using up-to techniques, in particular bisimulation up to context. We can see that the resulting equivalence proofs are quite simple, by looking at the proofs of the examples throughout the section. However, the bisimilarities are not complete w.r.t. contextual equivalence C (respectively P), as witnessed with the terms of Proposition 4.7.

Applicative Bisimilarity

Applicative bisimilarity has been originally defined for the lazy λ-calculus [START_REF] Abramsky | Full abstraction in the lazy lambda calculus[END_REF]. The main idea is to reduce (closed) terms to values, and then compare the resulting λ-abstractions by applying them to an arbitrary argument. Applicative bisimilarity for deterministic languages is usually sound and complete (see, e.g., [START_REF] Gordon | Bisimilarity for a first-order calculus of objects with subtyping[END_REF][START_REF] Tiuryn | Untyped lambda-calculus with input-output[END_REF][START_REF] Gordon | Bisimilarity as a theory of functional programming[END_REF]); in particular, proving soundness relies on a systematic proof technique called Howe's method [START_REF] Howe | Proving congruence of bisimulation in functional programming languages[END_REF][START_REF] Gordon | Bisimilarity as a theory of functional programming[END_REF]. However, the definition of up-to techniques remains an open issue for applicative bisimilarity.

Very few works have proposed a definition of applicative bisimilarity in a calculus with control. In [START_REF] Merro | On the observational theory of the CPS-calculus: (extended abstract)[END_REF], Merro and Biasi define an applicative bisimilarity which characterizes contextual equivalence in the CPS calculus [START_REF] Thielecke | Categorical Structure of Continuation Passing Style[END_REF], a minimal calculus which models the control features of functional languages with imperative jumps. In the λµ-calculus, Lassen [START_REF] Lassen | Bisimulation for pure untyped λµ-caluclus (extended abstract)[END_REF] defines a sound but not complete applicative bisimilarity in call-by-name. In a recent work, we improve this result by defining a sound and complete applicative bisimilarity in both call-by-name and call-by-value [START_REF] Biernacki | Applicative bisimilarities for call-by-name and call-by-value λµ-calculus[END_REF]. In this section, we define a sound and complete applicative bisimilarity for the relaxed semantics of λ S . Our definition of applicative bisimilarity relies on a labeled transition system, introduced first. We then define the relation itself, prove its soundness and completeness, before showing how it can be used on some examples.

Unlike with normal-form bisimilarity, we work primarily with closed terms, and we then extend the equivalence definitions to open terms with open extension (Definition 3.5). Besides, this section deals only with the relaxed semantics. We conjecture an applicative bisimilarity can also be defined for the original semantics, but we do not know how to prove it sound. We discuss this issue in the next section (see Remark 6.37).

Labeled Transition System

One possible way to define an applicative bisimilarity is to rely on a labeled transition system (LTS), where the possible interactions of a term with its environment are encoded in the labels (see, e.g., [START_REF] Gordon | Bisimilarity for a first-order calculus of objects with subtyping[END_REF][START_REF] Gordon | Bisimilarity as a theory of functional programming[END_REF]). Using a LTS simplifies the definition of the bisimilarity and makes it easier to use some techniques in proofs, such as diagram chasing. In Figure 6, we define a LTS t 0 α -→ t 1 with three kinds of transitions, where we assume all the terms to be closed. An internal action t τ -→ t is an evolution from t to t without any help from the surrounding RR n°9096 -→ t expresses the fact that v 0 needs to be applied to another value v 1 to evolve, reducing to t. Finally, the transition t E -→ t means that t is control stuck, and when t is put in a context E enclosed in a reset, the capture can be triggered, the result of which being t . We do not have a case for open stuck terms, because we work with closed terms only.

(λx.t) v τ -→ t{v/x} (βv) t 0 τ -→ t 0 t 0 t 1 τ -→ t 0 t 1 (left τ ) t τ -→ t v t τ -→ v t (right τ ) v τ -→ v (reset) t τ -→ t t τ -→ t ( • τ ) t -→ t t τ -→ t ( • S ) λx.t v -→ t{v/x} (val ) x / ∈ fv(E ) Sk.t E -→ t{λx. E [x] /k} (shift) t 0 E [ t1] -----→ t 0 t 0 t 1 E -→ t 0 (left S ) t E [v ] ----→ t v t E -→ t (right S )
Most rules for internal actions (Figure 6) are straightforward; the rules (β v ) and (reset) mimic the corresponding reduction rules, and the compositional rules (right τ ), (left τ ), and ( • τ ) allow internal actions to happen within any evaluation context. The rule ( • S ) for context capture is explained later. Rule (val ) defines the only possible transition for values. Note that while both rules (β v ) and (val ) encode β-reduction, they are quite different in nature; in the former, the term (λx.t) v can evolve by itself, without any help from the surrounding context, while the latter expresses the possibility for λx.t to evolve only if a value v is provided by the environment.

The rules for context capture are built following the principles of complementary semantics developed in [START_REF] Lenglet | Howe's method for calculi with passivation[END_REF]. The label of the transition t E -→ t contains what the environment needs to provide (a context E , but also an enclosing reset, left implicit) for the control stuck term t to reduce to t . Hence, the transition t E -→ t means that we have E [t] τ -→ t by context capture. For example, in the rule (shift), the result of the capture of E by Sk.t is t{λx. E [x] /k} .

In rule (left S ), we want to know the result of the capture of E by the term t 0 t 1 , assuming t 0 contains a shift ready to perform the capture. Under this hypothesis, the capture of E by t 0 t 1 comes from the capture of E [ t 1 ] by t 0 . Therefore, as a premise of the rule (left S ), we check that t 0 is able to capture E [ t 1 ], and the result t 0 of this transition is exactly the result we want for the

RR n°9096

capture of E by t 0 t 1 . The rule (right S ) follows the same pattern. Finally, a control stuck term t enclosed in a reset is able to perform an internal action (rule ( • S )); we obtain the result t of the transition t Sk.ω

(i ) (ω ω) -------→ ω (shift) i Sk.ω (ω ω) -----→ ω (right S ) (i Sk.ω) (ω ω) -→ ω (left S ) (i Sk.ω) (ω ω) τ -→ ω ( • S )
Reading the tree from bottom to top, we see that the rules ( • S ), (left S ), and (right S ) build the captured context in the label by deconstructing the initial term. Indeed, the rule ( • S ) removes the outermost reset and initiates the context in the label with . The rules (left S ) and (right S ) then successively remove the outermost application and store it in the context. The process continues until a shift operator is found; then we know the captured context is completed, and the rule (shift) computes the result of the capture. This result is then simply propagated from top to bottom by the other rules.

We now prove that the LTS corresponds to the reduction semantics → v and exhibits the observable terms (values and control stuck terms) of the language. The only difficulty is in the treatment of control stuck terms. The next lemma makes the correspondence between E -→ and control stuck terms explicit. Proposition 5.3. The following hold: s{λx. E [x] /k} holds, as wished. For the opposite direction, if

• We have τ -→ = → v . • If t E -→ t , then t is a stuck term, and E [t] τ -→ t . • If t v -→ t ,
F [ E [Sk.s] ] → v F [ s{λx. E [x] /k} ], then F [ E [Sk.s] ] τ -→ F [ s{λx. E [x]
/k} ] holds by reasoning by induction on F .

The second and third results are straightforward, either by using Lemma 5.2, or by examining the LTS rules.

Applicative Bisimilarity

We now define the notion of applicative bisimilarity for λ S . We write ⇒ for the reflexive and transitive closure of τ -→. We define the weak delay transition2 α = ⇒ as ⇒ if α = τ and as ⇒ α -→ otherwise. The definition of (weak delay) bisimilarity is then straightforward. Definition 5.4. A relation R on closed terms is an applicative simulation if t 0 R t 1 implies that for all t 0 α -→ t 0 , there exists t 1 such that t 1 α = ⇒ t 1 and t 0 R t 1 . A relation R on closed terms is an applicative bisimulation if R and R -1 are applicative simulations. Applicative bisimilarity A is the largest applicative bisimulation.

In words, two terms are equivalent if any transition from one is matched by a weak transition with the same label from the other. As in the λ-calculus [START_REF] Abramsky | Full abstraction in the lazy lambda calculus[END_REF][START_REF] Gordon | Bisimilarity as a theory of functional programming[END_REF], it is not mandatory to test the internal steps when proving that two terms are bisimilar, because of the following result.

Proposition 5.5. If t τ -→ t (respectively t ⇓ v t ) then t A t . Proposition 5.5 holds because {(t, t ) | t τ -→ t } is an applicative bisimulation.
Consequently, applicative bisimulation can be defined in terms of big-step transitions as follows.

Definition 5.6. A relation R on closed terms is a big-step applicative simulation if t 0 R t 1 implies that for all t 0 α = ⇒ t 0 with α = τ , there exists t 1 such that t 1 α = ⇒ t 1 and t 0 R t 1 . A relation R on closed terms is a big-step applicative bisimulation if R and R -1 are big-step applicative simulations.

Proposition 5.7. If R is a big-step applicative bisimulation, then R ⊆ A.
In this section, we drop the adjective "applicative" and refer to the two kinds of relations simply as "bisimulation" and "big-step bisimulation" where it does not cause confusion. We work with both styles (small-step and big-step), depending on which one is easier to use in a given proof.

Example 5.8 (double reset). We show that t A • t holds by proving that

R def = {( t , t ) | t ∈ T c } ∪ {(t, t) | t ∈ T c } is a big-step applicative bisimulation.
If t and/or t is open, then t σ = tσ (and similarly with t ), for all closing substitution σ, so we still have terms in R. With closed terms, the only possible (big-step) transition is Example 5.9 (Turing's combinator). We now consider Turing's combinator Θ and its variant Θ S def = θ Sk.k k . The two terms can perform the following transitions:

t v = ⇒ t , which means t ⇓ v v v -→ t . But we have proved in Example 4.3 that t ⇓ v v iff t ⇓ v v . Consequently, we have t v = ⇒ t iff t v = ⇒ t ,
Θ v = ⇒ v (λz.θ θ v z) Θ S v = ⇒ v (λz.(λx. θ x ) (λx. θ x ) v z) Assuming v = λx.t,
• if t 0 is a stuck term E 0 [Sk.t 0 ], then there exist t 1 and E 1 such that t 1 → * v E 1 [Sk.t 1 ]
, and for all closed E , we have

t 0 {λx. E [E 0 [x]] /k} R t 1 {λx. E [E 1 [x]] /k} .

Soundness

To prove the soundness of A w.r.t. the contextual equivalence C, we show that A is a congruence using Howe's method, a well-known congruence proof method initially developed for the λ-calculus [START_REF] Howe | Proving congruence of bisimulation in functional programming languages[END_REF][START_REF] Gordon | Bisimilarity as a theory of functional programming[END_REF]. We briefly explain how we apply it to A; the complete proof can be found in Appendix B. The idea of the method is as follows: first, define the Howe's closure of A, written A • , a relation which contains A and is compatible by construction. Then, prove a simulation-like property for A • ; from this result, prove that A • and A coincide on closed terms. Because A • is compatible, it shows that A is compatible as well, and therefore a congruence.

The definition of A • relies on the notion of compatible refinement; given a relation R on open terms, the compatible refinement R relates two terms iff they have the same outermost operator and their immediate subterms are related by R. Formally, it is inductively defined by the following rules:

x R x t 0 R t 1 λx.t 0 R λx.t 1 t 0 R t 1 t 0 R t 1 t 0 t 0 R t 1 t 1 t 0 R t 1 Sk.t 0 R Sk.t 1 t 0 R t 1 t 0 R t 1
Howe's closure A • is inductively defined as the smallest compatible relation containing A • and closed under right composition with A • .

Definition 5.11. Howe's closure A • is the smallest relation satisfying:

t 0 A • t 1 t 0 A • t 1 t 0 A • A • t 1 t 0 A • t 1 t 0 A • t 1 t 0 A • t 1
By construction, A • is compatible (by the third rule of the definition), and composing on the right with A • gives some transitivity properties to A • . In particular, we can prove

A • is substitutive: if t 0 A • t 1 and v 0 A • v 1 , then t 0 {v 0 /x} A • t 1 {v 1 /x}.
Let (A • ) c be the restriction of A • to closed terms. We cannot prove directly that (A • ) c is a bisimulation, so we prove a stronger result. Suppose we have t 0 (A • ) c t 1 ; instead of simply requiring t 0 α -→ t 0 to be matched by t 1 with the same label α, we ask t 1 to be able to respond for any label α related to α by (A • ) c . We, therefore, extend A • to all labels, by adding the relation τ A • τ , and by defining E A • E as follows:

A • E 0 A • E 1 t 0 A • t 1 E 0 t 0 A • E 1 t 1 E 0 A • E 1 v 0 A • v 1 v 0 E 0 A • v 1 E 1 Lemma 5.12 (Simulation-like property). If t 0 (A • ) c t 1 and t 0 α -→ t 0 , then for all α (A • ) c α , there exists t 1 such that t 1 α = ⇒ t 1 and t 0 (A • ) c t 1 .
The main difficulty when applying Howe's method is to prove this simulationlike property. The proof (in Appendix B) is by induction on t 0 (A • ) c t 1 , and then by case analysis on the transition t 0 α -→ t 0 . Lemma 5.12 allows us to prove that (A • ) c is a simulation, by choosing α = α. We cannot directly deduce that (A • ) c is a bisimulation, however we can prove that its transitive and reflexive closure ((A • ) c ) * is a bisimulation, because of the following classical property of the Howe's closure (for the proof of this result, see, e.g., [START_REF] Gordon | Bisimilarity as a theory of functional programming[END_REF]).

Lemma 5.13. The relation (A • ) * is symmetric.

The fact that ((A

• ) c ) * is a bisimulation implies that ((A • ) c ) * ⊆ A. Because A ⊆ (A • ) c ⊆ ((A • ) c ) * holds by construction, we can deduce A = (A • ) c . Since (A • ) c
is compatible, and we can easily show that A is transitive and reflexive, we have the following result. Proof. Let t 0 A t 1 , and C be a closed context. Because A is a congruence, we have

C [t 0 ] A C [t 1 ]. If C [t 0 ] ⇓ v v 0 , then we have C [t 0 ] τ = ⇒ v 0 v -→ t 0 for some t 0 ; by bisimilarity, there exist v 1 , t 1 such that C [t 1 ] τ = ⇒ v 1 v -→ t 1 . Therefore, we have C [t 1 ] ⇓ v v 1 .
The reasoning is the same if C [t 0 ] ⇓ v t 0 with t 0 control stuck, and for the evaluations of C [t 1 ].

Completeness and Context Lemma

We now prove that A is complete w.r.t. C, and deduce some results about C in the process, such as a context lemma showing that testing terms with evaluation contexts is as discriminating as testing with any contexts. We remind that we write D for the contextual equivalence which tests with contexts F only (see Definition 3.7). We already have C ⊆ D by definition. We first prove that A is complete w.r.t. D. Theorem 5.16. We have D ⊆ A.

Proof. Because D is symmetric, it is enough to prove that D is a big-step simulation. Let t 0 D t 1 . We have two cases to consider. Suppose t 0 v = ⇒ t 0 . Then we have t 0 ⇓ v v 0 for some v 0 . By definition of D, there exists v 1 such that t 1 ⇓ v v 1 . Therefore, we have t 1 v = ⇒ t 1 for some t 1 and t 0 v τ = ⇒ t 0 and t 1 v τ = ⇒ t 1 by Proposition 5.3. Hence, we have t 0 v A t 0 and t 1 v A t 1 by Proposition 5.5. Because t 0 D t 1 , we have t 0 v D t 1 v. Finally, we have t 0 A t 0 v D t 1 v A t 1 and t 0 D t 1 by Theorem 5.15 and transitivity of D.

Suppose t 0 E = ⇒ t 0 . Then we have t 0 ⇓ v t 0 for some t 0 . By definition of D, there exists t 1 such that t 1 ⇓ v t 1 . Therefore, by definition of the LTS, we have t 1 This equality also allows us to prove that we can formulate the open extension of C using capturing contexts. Proposition 5.18. We have t 0 C • t 1 iff for all C capturing the variables of t 0 and t 1 , the following holds:

E = ⇒ t 1 for some t 1 . We then have E [t 0 ] τ = ⇒ t 0 and E [t 1 ] τ = ⇒ t 1 by Proposition 5.3. Hence, we have E [t 0 ] A t 0 and E [t 1 ] A t 1 by Proposition 5.5. Because t 0 D t 1 , we have E [t 0 ] D E [t 1 ] . Finally, we have t 0 A E [t 0 ] D E [t 1 ] A t
• C [t 0 ] ⇓ v v 0 iff C [t 1 ] ⇓ v v 1 ; • C [t 0 ] ⇓ v t 0 , where t 0 is control stuck, iff C [t 1 ] ⇓ v t 1 , with t 1 control stuck as well.
Proof. Suppose t 0 C • t 1 . Then t 0 A • t 1 , and because A • is a congruence, for all C capturing the variables of t 0 and t 1 , we have For the reverse implication, suppose that for all C capturing the variables of t 0 and t 1 , the two items of the proposition hold. Let σ = {v 1 /x 1 . . . v n /x n } be a substitution closing t 0 and t 1 . Let C be a closed context. We want to prove that

C [t 0 ] A C [t 1 ]. We have C [t 0 ] ⇓ v v 0 iff C [t 1 ] ⇓ v v 1 by
C [t 0 σ] → * v v iff C [t 1 σ] → * v v
for some v and v , and similarly for control stuck terms. But the context

C def = C [(λx 1 . . . x n . ) v 1 . . . v n ]
is a context capturing the variables of t 0 and t 1 , and we have

C [t 0 ] → * v C [t 0 σ] and C [t 1 ] → * v C [t 1 σ]. Consequently, C [t 0 σ] → * v v iff C [t 0 ] → * v v iff C [t 0 ] → * v v (first item of the proposition) iff C [t 1 σ] → * v v
for some v and v . The reasoning is the same for control stuck terms.

The next example completes the proof of Proposition 4.7: we show that the terms which cannot be equated with normal-form bisimulation are applicative bisimilar and, therefore, contextually equivalent.

Proposition 5.19. Let i def = λx.x; then x i Sk.i C • x i ( x i Sk.i) . Proof. We prove that R def = {( t Sk.i , t ( t Sk.i) ) | t ∈ T c } ∪ {(t, t) | t ∈ T c }
is a big-step bisimulation. The term t can either diverge or reduce to a value (according to Proposition 2.9). If it diverges, then both t Sk.i and t ( t Sk.i) diverge, otherwise, they both evaluate to i. For all v , we, therefore, have t Sk.i v = ⇒ v and t ( t Sk.i) v = ⇒ v , and v R v holds, as wished.

Proving the Axioms

As with normal-form bisimulation (Section 4.5), we show how to prove Kameyama and Hasegawa's axioms (Section 2.4) except for S elim using applicative bisimulation. In the following propositions, we assume the terms to be closed, since the proofs for open terms can be deduced directly from the results for closed terms. First, note that the β v , • S , and • val axioms are direct consequences of Proposition 5.5.

Proposition 5.20 (η v axiom). If x / ∈ fv(v), then λx.v x A v.
Proof = ⇒ t (with α = τ ) is possible only if t 1 evaluates to some value v (evaluation to a control stuck terms is not possible according to Proposition 2.9). In this case, we have (λx.t

0 ) t 1 τ = ⇒ (λx.t 0 ) v τ -→ t 0 {v/x} and (λx. t 0 ) t 1 τ = ⇒ t 0 {v/x} . Therefore, we have (λx.t 0 ) t 1 α = ⇒ t (with α = τ ) iff (λx. t 0 ) t 1 α = ⇒ t .
From there, it is easy to conclude.

Proposition 5.23 (β Ω axiom). If x / ∈ fv(E ), then (λx.E [x]) t A E [t].
Proof (Sketch). We first give some intuitions on why the proof of this result is harder with applicative bisimulation than with normal-form bisimulation.

(λx.E [x]) t E1 --→ t {λy. E 1 [(λx.E [x]) E 0 [y]] /k} E [t] E1 --→ t {λy. E 1 [E [E 0 [y]]] /k}
We obtain terms of the form t σ and t σ (where σ and σ are the above substitutions). We now have to consider the transitions from these terms, and the interesting case is when

t = F [k v]. t σ τ -→ F σ[ E 1 [(λx.E [x]) E 0 [vσ]] ] def = t 0 t σ τ -→ F σ [ E 1 [E [E 0 [vσ ]]] ] def = t 1
We obtain terms that are similar to the initial terms (λx.E [x])t and E [t], except for the extra contexts F and E 1 , and the substitutions σ and σ . Again, the interesting cases are when E 0 [v] is either a control stuck term, or a term of the form

F [k v ].
Looking at these cases, we see that the bisimulation we have to define has to relate terms similar to t 0 and t 1 , except with an arbitrary number of contexts F and substitutions similar to σ and σ . Formally, given a sequence of (continuation) variables k 1 , . . . , k n and a sequence

-→ E k of triples of contexts E i , E i , E i such that fv(E i ) ∪ fv(E i ) ∪ fv(E i ) ⊆ {k 1 , . . . , k i-1 } for 1 ≤ i ≤ n ( ) RR n°9096
we define two families of sequences of substitutions as follows:

σ - → E i = {λx. E i [(λy.E i [y]) E i [x]] /k i } δ - → E i = {λx. E i [E i [E i [x]]] /k i }
Additionally, given a term t, a sequence of pure contexts -→ E = E 1 , . . . , E m and a sequence of evaluation contexts -→ F = F 1 , . . . , F m , we inductively define two sequences of terms, s 0 , . . . , s m and u 0 , . . . , u m , as follows:

s t, - → E , - → F 0 = t s t, - → E , - → F i+1 = F i+1 [(λx.E i+1 [x]) s i ] u t, - → E , - → F 0 = t u t, - → E , - → F i+1 = F i+1 [E i+1 [u i ]]
Then the following relation R is a bisimulation:

R = {(s t, - → E , - → F i σ -→ E k n . . . σ -→ E k 1 , u t, - → E , - → F i δ -→ E k n . . . δ -→ E k 1 ) | - → k = k 1 , . . . , k n , n ≥ 0, -→ E k satisfies ( ), - → E = E 1 , . . . , E m , - → F = F 1 , . . . , F m , m ≥ 0, fv(t) ∪ fv( - → E ) ∪ fv( - → F ) ⊆ {k 1 , . . . , k n }, 0 ≤ i ≤ m}
We omit the complete bisimulation proof, as it is similar to the one in Appendix C.3: we proceed by case analysis on the transitions the related terms can perform.

Conclusion

In this section, we define an applicative bisimilarity for the relaxed semantics of λ S . As in the plain λ-calculus, our definition compares λ-abstractions by passing them a random value as argument. For control stuck terms, we run them in an arbitrary context E surrounded by a reset. Unlike normal-form bisimilarity, applicative bisimilarity is complete w.r.t. contextual equivalence, and we can easily prove equivalence of the terms in Proposition 4.7 with an applicative bisimulation.

Equivalence proofs can be simpler with applicative bisimulation than with normal-form bisimulation, because in the applicative case, we reason mainly on closed terms. As a result, a term cannot evaluate to an open stuck term, and we do not have to deal with this case, making the proofs shorter than with normal-form bisimulation (compare, e.g., Example 5.8 with Example 4.3, or Proposition 5.22 with Proposition 4.30). However, in general, the proofs are much simpler with normal-form bisimulation, because there is no quantification over arguments (values or contexts) in the λ-abstraction and control stuck terms cases. We can see the difference when comparing the proofs for fixed-point combinators (Example 4.4 and Example 5.9) and for the β Ω axiom (Proposition 4.31 and Proposition 5.23). The lack of powerful up-to techniques such as bisimulation up to context makes also applicative bisimulation harder to use than the normal-form one.

Environmental Bisimilarity

Like applicative bisimilarity, environmental bisimilarity reduces closed terms to normal forms, which are then compared using some particular contexts (e.g., λ-abstractions are tested by passing them arguments). However, the testing contexts are not arbitrary, but built from an environment, which represents the knowledge acquired so far by an outside observer. The idea originally comes from languages with strict isolation or data abstraction [START_REF] Koutavas | Small bisimulations for reasoning about higherorder imperative programs[END_REF][START_REF] Sumii | A bisimulation for type abstraction and recursion[END_REF][START_REF] Koutavas | Bisimulations for untyped imperative objects[END_REF][START_REF] Sumii | A bisimulation for dynamic sealing[END_REF], where environments are used to handle information hiding. The term "environmental bisimulation" has then been introduced in [START_REF] Sangiorgi | Environmental bisimulations for higher-order languages[END_REF][START_REF] Sangiorgi | Environmental bisimulations for higher-order languages[END_REF], and such a bisimilarity has been since defined in various higher-order languages (see, e.g., [START_REF] Sato | The higher-order, call-by-value applied Pi-calculus[END_REF][START_REF] Sumii | A bisimulation-like proof method for contextual properties in untyped lambda-calculus with references and deallocation[END_REF][START_REF] Piérard | A higher-order distributed calculus with name creation[END_REF]). Environmental bisimilarity usually characterizes contextual equivalence, but is harder to use than applicative bisimilarity to prove that two given terms are equivalent. Nonetheless, one can define powerful up-to techniques [START_REF] Sangiorgi | Environmental bisimulations for higher-order languages[END_REF] to simplify the equivalence proofs and deal with this extra difficulty. Besides, the authors of [START_REF] Koutavas | From applicative to environmental bisimulation[END_REF] argue that the additional complexity is necessary to handle more realistic features, like local state or exceptions. In addition, environmental bisimilarity does not require a particular proof technique, such as Howe's method, to prove its soundness; this will be helpful when considering the original semantics.

In what follows, we first give the definition of environmental bisimilarity for the relaxed semantics. We then discuss up-to techniques, and explain why they are not as helpful as, e.g., in the plain λ-calculus [START_REF] Sangiorgi | Environmental bisimulations for higher-order languages[END_REF]. Finally, we propose a definition of environmental bisimilarity which we can prove complete for the original semantics. In this section, we focus on closed terms, before extending the relations we define to open terms.

Definition for the Relaxed Semantics

Environmental bisimulations use an environment E to accumulate knowledge about two tested terms. For the λ-calculus [START_REF] Sangiorgi | Environmental bisimulations for higher-order languages[END_REF], E records the values (v 0 , v 1 ) the tested terms reduce to, if they exist. We can then compare v 0 and v 1 at any time by passing them arguments built from E. Even though in the relaxed semantics of λ S control stuck terms are also normal forms, we do not store them in environments (like values), but we instead compare them during the bisimulation game, still using the environment. The rationale behind this change with our previous work [START_REF] Biernacki | Environmental bisimulations for delimitedcontrol operators[END_REF], is explained in Remark 6.2.

As a result, an environment E is a relation on values; e.g., we define the identity environment I as {(v, v) | v ∈ T c }. We build terms and evaluation contexts from an environment E with the help of two closures, defined in Figure 7. Given a relation R on terms, we write Ṙ for the term generating closure and R for the context generating closure. Even if R is defined only on closed terms, Ṙ and R are defined on open terms and open contexts, respectively. In this section, we consider the restrictions of Ṙ and R to respectively closed terms and closed contexts unless stated otherwise.

An environmental relation X is a set of environments E, and triples (E, t 0 , t 1 ), where t 0 and t 1 are closed. We write t 0 X E t 1 as a shorthand for (E, t 0 , t 1 ) ∈ X ; roughly, it means that we test t 0 and t 1 with the knowledge E. We define environmental bisimulation as follows.

Term generating closure. t R t t Ṙ t x Ṙ x t Ṙ t λx.t Ṙ λx.t t 0 Ṙ t 0 t 1 Ṙ t 1 t 0 t 1 Ṙ t 0 t 1 t Ṙ t Sk.t Ṙ Sk.t t Ṙ t t Ṙ t Context generating closure. R F 0 R F 1 v 0 Ṙ v 1 v 0 F 0 R v 1 F 1 F 0 R F 1 t 0 Ṙ t 1 F 0 t 0 R F 1 t 1 F 0 R F 1 F 0 R F 1
Definition 6.1. A relation X is an environmental bisimulation if 1. t 0 X E t 1 implies: (a) if t 0 → v t 0 , then there exists t 1 such that t 1 → * v t 1 and t 0 X E t 1 ; (b) if t 0 is a control stuck term E 0 [Sk.t 0 ], then there exists E 1 [Sk.t 1 ] such that t 1 ⇓ v E 1 [Sk.t 1 ]
, and for all

E 0 Ë E 1 , t 0 {λx. E 0 [E 0 [x]] /k} X E t 1 {λx. E 1 [E 1 [x]
] /k} holds for a fresh x; (c) if t 0 is a value, then there exists v 1 such that t 1 ⇓ v v 1 and E ∪ {(t 0 , v 1 )} ∈ X ; (d) the converse of the above conditions on t 1 ; 2. for all E ∈ X , if λx.t 0 E λx.t 1 and v 0 Ė v 1 , then t 0 {v 0 /x} X E t 1 {v 1 /x}.

Environmental bisimilarity, written ≈, is the largest environmental bisimulation. To prove that two terms t 0 and t 1 are equivalent, we want to relate them without any predefined knowledge, i.e., we want to prove that t 0 ≈ ∅ t 1 holds; we also write E for ≈ ∅ . The relation E will be the candidate to characterize contextual equivalence.

The first part of the definition makes the bisimulation game explicit for t 0 and t 1 , while the second part focuses on environments E. If t 0 is a value, then t 1 has to evaluate to a value, and we extend the environment with the newly acquired knowledge. We then compare values in E (clause (2)) by applying them to arguments built from E, as in the λ-calculus [START_REF] Sangiorgi | Environmental bisimulations for higher-order languages[END_REF]. If t 0 is a control stuck term, then t 1 has to evaluate to a control stuck term as well, and we trigger the capture by putting them within contexts E 0 , E 1 built from E (clause (1b)). This is similar to the way we test values and stuck terms with applicative bisimilarity (Section 5), except that applicative bisimilarity tests both values or stuck terms with the same argument or context. Using different entities (as in Definition 6.1) makes bisimulation proofs harder, but it simplifies the proof of congruence of the environmental bisimilarity. Remark 6.2. The definition of environmental bisimulation in [START_REF] Biernacki | Environmental bisimulations for delimitedcontrol operators[END_REF] treats control stuck terms the same way it deals with values, by storing them in an environment before testing them. As explained in [START_REF] Koutavas | From applicative to environmental bisimulation[END_REF], accumulating values in an environment to apply them to different arguments is justified (and, for some languages, necessary), because a value can be saved by a testing context and applied several times, like, e.g., in the context (λx.(x v 0 ) (x v 1 )) . Such a behavior is not possible with a control stuck term, since stuck terms are not values and cannot be saved. A testing context can, therefore, trigger the capture of a control stuck term only once, and not several times in different evaluation contexts. Consequently, we believe that control stuck terms should not be saved in environments.

Definition 6.1 is also easier to use than the definition of [START_REF] Biernacki | Environmental bisimulations for delimitedcontrol operators[END_REF], because environments now contain only values, and control stuck terms are tested only once. For example, we can prove the β Ω axiom with Definition 6.1 (and some basic up-to techniques; see Proposition 6.26), while we do not know how to prove it with the definition of [START_REF] Biernacki | Environmental bisimulations for delimitedcontrol operators[END_REF] (even though we know it is possible, since the environmental bisimilarity of [START_REF] Biernacki | Environmental bisimulations for delimitedcontrol operators[END_REF] is complete).

Unlike applicative bisimilarity or contextual equivalence, environmental bisimilarity tests terms with different arguments (built from the environment); we have to take this into account when extending environmental relations to open terms. If -→ x = fv(t 0 ) ∪ fv(t 1 ), then we write

t 0 X E • t 1 if λ - → x .t 0 X E λ - → x .t 1 holds.
Note that to relate λ -→ x .t 0 and λ -→ x .t 1 , Definition 6.1 replaces each variable with distinct closed values built from E, while Definition 3.5, replaces each variable in both terms with the same arbitrary closed value.

As with the other styles of bisimilarity, we define a big-step variant of Definition 6.1, where we reason on the results of the evaluation directly.

Definition 6.3. A relation X is a big-step environmental bisimulation if 1. t 0 X E t 1 implies: (a) if t 0 ⇓ v v 0 , then there is v 1 such that t 1 ⇓ v v 1 and E ∪ {(v 0 , v 1 )} ∈ X ; (b) if t 0 ⇓ v E 0 [Sk.t 0 ], then there is E 1 [Sk.t 1 ] such that t 1 ⇓ v E 1 [Sk.t 1 ],
and

t 0 {λx. E 0 [E 0 [x]] /k} X E t 1 {λx. E 1 [E 1 [x]
] /k} holds for all E 0 Ë E 1 and a fresh x; (c) the converse of the above conditions on t

1 ; 2. for all E ∈ X , if λx.t 0 E λx.t 1 and v 0 Ė v 1 , then t 0 {v 0 /x} X E t 1 {v 1 /x}. Proposition 6.4. If X is a big-step environmental bisimulation, then X ⊆ ≈.
We use the following results in the rest of the paper.

Proposition 6.5 (Weakening). If t 0 ≈ E t 1 and E ⊆ E then t 0 ≈ E t 1 .
A smaller environment is a weaker constraint, because we can build fewer arguments and contexts to test the normal forms in E. The proof is as in [START_REF] Sangiorgi | Environmental bisimulations for higher-order languages[END_REF]. Proposition 6.6 states that reduction (and, therefore, evaluation) is included in E. Proposition 6.6. If t 0 → v t 0 , then t 0 E t 0 .

We now give some examples showing how the notion of environmental bisimulation can be used. Example 6.7 (double reset). We have t E t , because for a given t the relation Therefore, we have to put (v 0 , v 1 ) in an environment E. When we then test v 0 and v 1 , we use arguments v 0 and v 1 such that v 0 Ė v 1 , and we compare v 0 (λz.θ θ v 0 z) with v 1 (λz.(λx. θ x ) (λx. θ x ) v 1 z). Because we have two different terms v 0 and v 1 , we can no longer do a case analysis as suggested in Example 5.9. To conclude with environmental bisimulation, we need bisimulation up-to context (see Example 6.22).

{(∅, t , t )} ∪ {(E, t , t ) | E ⊆ I, t ∈ T c } ∪ {E | E ⊆ I} is a big-step environmental bisimulation. Indeed, we know that t ⇓ v v iff t ⇓ v v,
As usual with environmental relations, the candidate relation in Example 6.7 could be made simpler with the help of basic up-to techniques. In bisimulation up-to environment, one can use bigger environments than needed by Definition 6.1. As a result, instead of making the environment grow at each bisimulation step, we can directly use the largest possible environment. Definition 6.9. A relation X is an environmental bisimulation up to environment if

1. t 0 X E t 1 implies: (a) if t 0 → v t 0 , then there exist t 1 and E ∈ X such that t 1 → * v t 1 , t 0 X E t 1 , and E ⊆ E ; (b) if t 0 is a stuck term E 0 [Sk.t 0 ], then there exists E 1 [Sk.t 1 ] such that t 1 ⇓ v E 1 [Sk.t 1 ]
, and for all E 0 Ë E 1 , there exists E such that E ⊆ E and t 0 {λx. Proof. As in [START_REF] Sangiorgi | Environmental bisimulations for higher-order languages[END_REF].

E 0 [E 0 [x]] /k} X E t 1 {λx. E 1 [E 1 [x]] /k}
In the following example we use the notion of a big-step environmental bisimulation up to environment that can be defined in an expected way by combining Definition 6.3 and 6.9.

Example 6.11 (double reset). We can simplify the proof of Example 6.7 by showing that for a given t the relation

{(∅, t , t )} ∪ {(I, t , t ) | t ∈ T c } ∪ {I} is a big-step bisimulation up to environment.
Next, we define bisimulation up-to bisimilarity that allows one to simplify definitions of candidate relations by factoring out inessential bisimilar terms. Definition 6.12. A relation X is an environmental bisimulation up to bisimilarity if

1. t 0 X E t 1 implies: (a) if t 0 → v t 0 , then there exists t 1 such that t 1 → * v t 1 and t 0 X E E t 1 ; (b) if t 0 is a stuck term E 0 [Sk.t 0 ], then there exists E 1 [Sk.t 1 ] such that t 1 ⇓ v E 1 [Sk.t 1 ]
, and for all

E 0 Ë E 1 , t 0 {λx. E 0 [E 0 [x]] /k} X E E t 1 {λx. E 1 [E 1 [x]] /k} holds for a fresh x; (c) if t 0 is a value, then there exist v 1 , v 1 such that t 1 → * v v 1 , v 1 E v 1 , and E ∪ {(t 0 , v 1 )} ∈ X ; (d) the converse of the above conditions on t 1 ; 2. for all E ∈ X , if λx.t 0 E λx.t 1 and v 0 Ė v 1 , then t 0 {v 0 /x} EX E E t 1 {v 1 /x}.
Proposition 6.13. If X is an environmental bisimulation up to bisimilarity, then X ⊆ ≈.

Proof. As in [START_REF] Sangiorgi | Environmental bisimulations for higher-order languages[END_REF].

As usual for up-to bisimilarity with small-step relations, we cannot compose on the left-hand side of X in clause (1) of Definition 6.12 [START_REF] Sangiorgi | Environmental bisimulations for higher-order languages[END_REF].

Soundness and Completeness

We now prove soundness and completeness of E w.r.t. contextual equivalence. Because the proofs follow the same steps as for the λ-calculus [START_REF] Sangiorgi | Environmental bisimulations for higher-order languages[END_REF], we only give here the main lemmas and sketch their proofs. The complete proofs can be found in Appendix C.1. For a relation R on terms, we write R v for its restriction to closed values. The first step consists in proving compatibility for values, and also for any terms but only w.r.t. evaluation contexts. Lemma 6.14.

If v 0 ≈ E v 1 , then C [v 0 ] ≈ E C [v 1 ]. Lemma 6.15. If t 0 ≈ E t 1 , then F [t 0 ] ≈ E F [t 1 ].
Lemmas 6.14 and 6.15 are proved simultaneously by showing that, for any environmental bisimulation Y, the relation

X def = {( Ė v , F 0 [t 0 ], F 1 [t 1 ]) | t 0 Y E t 1 , F 0 Ë F 1 } ∪ {( Ė v , t 0 , t 1 ) | E ∈ Y, t 0 Ė t 1 } ∪ { Ė v | E ∈ Y}
is a bisimulation up-to environment. Informally, the elements of the first set of X reduce to elements of the second set of X , and we then prove the bisimulation property for these elements by induction on t 0 Ė t 1 . We can then prove the main compatibility lemma.

Theorem 6.16.

If t 0 E t 1 , then C [t 0 ] ≈ Ė v C [t 1 ].
We show that {( Ė v , t 0 , t 1 ) | t 0 Ė t 1 } ∪ { Ė v } is a bisimulation up-to bisimilarity by induction on t 0 Ė t 1 . By weakening (Proposition 6.5), we can deduce from Theorem 6.16 that E is a compatible and, therefore, is sound w.r.t. C. Corollary 6.17 (Soundness). We have E ⊆ C.

The relation E is also complete w.r.t. contextual equivalence. Theorem 6.18 (Completeness). We have C ⊆ E.

Proof. We prove that

X def = {(C v , t 0 , t 1 ) | t 0 C t 1 } ∪ {C v } is a big-step envi- ronmental bisimulation. Let t 0 X C v t 1 . If t 0 ⇓ v v 0 ,
then by definition of C, there exists v 1 such that t 1 ⇓ v v 1 . By Proposition 6.6, we have t 0 E v 0 and t 1 E v 1 , which implies t 0 C v 0 and t 1 C v 1 by Corollary 6.17. Transitivity of C gives v 0 C v 1 , hence we have

C v ∪ {(v 0 , v 1 )} = C v ∈ X , as wished. If t 0 ⇓ v E 0 [Sk.t 0 ], then by definition of C, there exists E 1 [Sk.t 1 ] such that t 1 ⇓ v E 1 [Sk.t 1 ]. Let E 0 C v E 1 . By congruence of C, we have E 0 [E 0 [Sk.t 0 ]] C E 1 [E 1 [Sk.t 1 ]] . Because we have E 0 [E 0 [Sk.t 0 ]] → v t 0 {λx. E 0 [E 0 [x]] /k} , E 1 [E 1 [Sk.t 1 ]] → v t 1 {λx. E 1 [E 1 [x]] /k} , and also → v ⊆ E ⊆ C, we obtain t 0 {λx. E 0 [E 0 [x]] /k} C t 1 {λx. E 1 [E 1 [x]] /k} (using transitivity of C), which in turn implies t 0 {λx. E 0 [E 0 [x]] /k} X C v t 1 {λx. E 1 [E 1 [x]] /k} ,

Bisimulation up to context

Equivalence proofs based on environmental bisimilarity can be simplified by using up-to techniques, such as up to reduction, up to expansion, and up to context [START_REF] Sangiorgi | Environmental bisimulations for higher-order languages[END_REF]. We only discuss the last, since the first two can be defined and proved sound in λ S without issues. Bisimulations up to context may factor out a common context from the tested terms. Formally, two terms t 0 , t 1 are related by the context closure of X , written t 0 X E t 1 , if

• either t 0 = F 0 [t 0 ], t 1 = F 1 [t 1 ], t 0 X E t 1 , and F 0 Ë F 1 ; • or t 0 Ė t 1 .
We then define environmental bisimulation up to context as follows.

Definition 6.19. A relation X is a bisimulation up to context if 1. t 0 X E t 1 implies: (a) if t 0 → v t 0 , then there exists t 1 such that t 1 → * v t 1 and t 0 X E t 1 ; (b) if t 0 is a stuck term E 0 [Sk.t 0 ], then there exists E 1 [Sk.t 1 ] such that t 1 ⇓ v E 1 [Sk.t 1 ] and for all E 0 Ë E 1 , t 0 {λx. E 0 [E 0 [x]] /k} X E t 1 {λx. E 1 [E 1 [x]
] /k} holds for a fresh x; (c) if t 0 is a value, then there exist v 1 and E ∈ X such that t 1 ⇓ v v 1 and E ∪ {(t 0 , v 1 )} ⊆ Ė v ; (d) the converse of the above conditions on t 1 ; 2. for all E ∈ X , if λx.t 0 E λx.t 1 and v 0 Ė v 1 , then t 0 {v 0 /x} X E t 1 {v 1 /x}. Proposition 6.20. If X is a bisimulation up to context, then X ⊆ ≈.

Proof. As in [START_REF] Sangiorgi | Environmental bisimulations for higher-order languages[END_REF].

Note that in the definition of context closure X E , terms related by X E can be put into evaluation contexts, while values (related by E) can be put in any contexts. This restriction to evaluation contexts in the first case is usual in the definition of up-to context techniques for environmental relations [START_REF] Sangiorgi | Environmental bisimulations for higher-order languages[END_REF][START_REF] Sumii | A bisimulation-like proof method for contextual properties in untyped lambda-calculus with references and deallocation[END_REF][START_REF] Sato | The higher-order, call-by-value applied Pi-calculus[END_REF][START_REF] Piérard | A higher-order distributed calculus with name creation[END_REF], and is in fact necessary for the technique to be sound, as pointed out by Madiot [START_REF] Madiot | Higher-order languages: dualities and bisimulation enhancements[END_REF]. Indeed, assume terms can be put in any context, and let X def = {(E, Ω, Ω), (E, (λx.x) (λy.Ω), (λx.x) (λy.Ω))} where E is any environment. Then X is a bisimulation up to context, because (λx.x) (λy.Ω) → v λy.Ω, and (λy.Ω) ẊE (λy.Ω) holds, since Ω X E Ω. Then Proposition 6.20 implies (λx.x) (λy.Ω) ≈ E (λx.x) (λy.Ω), which in turn implies E ∪ {(λy.Ω, λy.Ω)} ⊆ ≈ for any E, including any unsound environment such as {(λx.Ω, λx.x)}, hence a contradiction.

The above reasoning does not depend on the calculus, as it holds for the plain λ-calculus; environments are what makes the restriction to evaluation contexts necessary. This is not problematic for the λ-calculus, because when a term t reduces within an evaluation context, the context is not affected. It is not the case in λ S , as (a part of) the evaluation context can be captured. As a result, bisimulation up to context is not as helpful in λ S as in the λ-calculus. To illustrate this, suppose we want to construct a candidate relation X to prove the β Ω axiom, starting from (∅, E [t], (λx.E [x]) t) (with x / ∈ fv(E )). The problematic case is when t is a stuck term E 0 [Sk.t 0 ]: for X to be a bisimulation, we would have to add (∅, [y]] can be put in any context, not necessarily in an evaluation one. Therefore, Definition 6.19 cannot be used here, a new kind of up-to technique is required. During the review process of this paper, we managed to define in [START_REF] Aristizábal | Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation[END_REF] an environmental bisimulation up to context able to prove the β Ω axiom for a richer calculus, using a completely different framework. We believe these ideas can be applied to λ S , and we leave this as a future work.

t 0 {λy. E [(λx.E [x]) E 0 [y]] /k} , t 0 {λy. E [E [E 0 [y]]] /k} ) to
Note that we do not have such issues with normal-form bisimilarity (Section 4), because normal-form bisimulation up to context is not restricted to evaluation contexts only, since we do not have environments to cause problems. But even if environmental bisimulation up to context is not as helpful as wished, it still simplifies equivalence proofs, as we can see with the next examples, where the notion of a big-step environmental bisimulation is equipped with the up to context technique (we omit a formal definition that is a straightforward combination of Definition 6.3 and 6.19). Example 6.21 (double reset). We can simplify further the proof of equivalence between t and t by showing that {(∅, t , t ), ∅} is a big-step bisimulation up to context. Indeed, the couple (v, v) belongs to the closure of the empty environment, so clause (1c) of Definition 6.19 is verified. Example 6.22 (Turing's combinator). We prove that Θ is bisimilar to Θ S using bisimulation up to context. We define θ def = λx. θ x , v 0 def = λy.y (λz.θ θ y z), and v 1 def = λy.y (λz.θ θ y z). We define E inductively by the following rules:

v 0 E v 1 v Ė v λz.θ θ v z E λz.θ θ v z Then X def = {(E, Θ, Θ S )
, (E, Θ, θ θ ), E} is a (big-step) bisimulation up to context. Indeed, we have Θ ⇓ v v 0 , Θ S ⇓ v v 1 , and θ θ ⇓ v v 1 ; therefore, clause (1c) of Definition 6.19 is checked for both pairs. We now verify clause (2) on the environment E. Let v 0 Ė v 1 . In the case v 0 E v 1 , we have to check that v 0 (λz.θ θ v 0 z) X E v 1 (λz.θ θ v 1 z) holds. From λz.θ θ v 0 z E λz.θ θ v 1 z and v 0 Ė v 1 , we deduce v 0 (λz.θ θ v 0 z) Ė v 1 (λz.θ θ v 1 z), and Ė ⊆ X E , hence the result holds. In the other subcase, we have λz.θ θ v z E λz.θ θ v z with v Ė v . We have to check that θ θ v v 0 X E θ θ v v 1 holds. From v Ė v and v 0 Ė v 1 , we deduce v v 0 Ë v v 1 , and we have θ θ X E θ θ , hence the result holds.

Bisimulation up to context can be combined with the other up-to techniques, such as up to reduction [START_REF] Sangiorgi | Environmental bisimulations for higher-order languages[END_REF] (which allows extra reduction steps before relating the terms), as we can see with the following examples.

Proving the axioms

We discuss Kameyama and Hasegawa's axioms (Section 2.4) in the context of environmental bisimulation. The β v , • S , and • val axioms are direct consequences of Proposition 6.6. We now prove the remaining axioms (except for S elim , because we use the relaxed semantics). Proof. The bisimulation R defined in the proof of Proposition 5.23 can be changed into an environmental relation X by considering that the terms in R are related with the empty environment ∅. We can then prove that X is an environmental bisimulation up to context, following the same scheme as in the proof of Proposition 5.23.

Proposition 6.23 (η v axiom). If x / ∈ fv(v), then λx.v x E v. Proof. Let E def = {(λx.v x, v) | v ∈ T c , x / ∈ fv(v)}. Then {(∅, λx.v x, v) | v ∈ T c , x / ∈ fv(v)} ∪ {E}

Environmental Relations for the Original Semantics

The bisimilarities introduced so far are sound and complete w.r.t. the contextual equivalence C of the relaxed semantics, but only sound w.r.t. the contextual equivalence P of the original semantics (cf. Proposition 3.9). We now propose a definition of environmental bisimulation adapted to delimited terms (but defined on all terms, like P). Definition 6.27. A relation X is a delimited environmental bisimulation if 1. if t 0 X E t 1 and t 0 and t 1 are not both delimited terms, then for all closed

E 0 , E 1 such that E 0 Ë E 1 , we have E 0 [t 0 ] X E E 1 [t 1 ] ; 2. p 0 X E p 1 implies (a) if p 0 → v p 0 , then there exists p 1 such that p 1 → * v p 1 and p 0 X E p 1 ; (b) if p 0 → v v 0 , then there exists v 1 such that p 1 → * v v 1 , and {(v 0 , v 1 )} ∪ E ∈ X ; (c) the converse of the above conditions on p 1 ; 3. for all E ∈ X , if λx.t 0 E λx.t 1 and v 0 Ė v 1 , then t 0 {v 0 /x} X E t 1 {v 1 /x}.
Delimited environmental bisimilarity, written , is the largest delimited environmental bisimulation. As before, the relation ∅ , also written F, is candidate to characterize P.

Clauses ( 2) and (3) of Definition 6.27 deal with delimited terms and environments in a classical way (as in plain λ-calculus). The problematic case is when relating terms t 0 and t 1 that are not both delimited terms (clause (1)). Indeed, one of them may be control stuck and, therefore, we have to test them within some contexts E 0 , E 1 (built from E) to potentially trigger a capture that otherwise would not happen. We cannot require both terms to be control stuck, as in clause (1b) of Definition 6.1, because a control stuck term can be equivalent to a term free from control effect. E.g., we will see that v F Sk.k v, provided that k / ∈ fv(v).

Example 6.28. Suppose we want to prove (λx.t 0 ) t 1 F (λx. t 0 ) t 1 (as in Proposition 6.25). Because (λx. t 0 ) t 1 is not delimited, we have to put both terms into a context first: we have to change the candidate relation of Proposition 6.25 into

{(∅, (λx.t 0 ) t 1 , (λx. t 0 ) t 1 ), ∅} ∪ {(∅, E [ (λx.t 0 ) t 1 ] , E [(λx. t 0 ) t 1 ] ) | E ∈ PC c }.
In contrast, to prove t F t , we do not have to change the candidate relation of Example 6.7, since both terms are delimited.

We can give a definition of big-step bisimulation by removing clause (2a) and changing → v into ⇓ v in clause (2b). Propositions 6.5 and 6.6 can also be extended to and F. Proposition 6.29. If t 0 E t 1 and E ⊆ E then t 0 E t 1 .

RR n°9096

Proposition 6.30. If t 0 → v t 0 , then t 0 F t 0 .

The next proposition states that E is more discriminating than F. Proposition 6.31. We have E ⊆ F.

A consequence of Proposition 6.31 is that we can use Definition 6.1 as a proof technique for F. E.g., we have directly (λx.t

0 ) t 1 F (λx. t 0 ) t 1 , because (λx.t 0 ) t 1 E (λx. t 0 ) t 1 .

Soundness and Completeness

We sketch the proofs of soundness and completeness of F w.r.t. P; see Appendix C.2 for the complete proofs. The soundness proof follows the same scheme as in Section 6.2, with some necessary adjustments. As before, we need up-to environment and up-to bisimilarity techniques to prove the following lemmas. Lemma 6.32.

If v 0 E v 1 , then C [v 0 ] E C [v 1 ]. Lemma 6.33. If t 0 E t 1 , then F [t 0 ] E F [t 1 ].
We prove Lemmas 6.32 and 6.33 by showing that a relation similar to the relation X defined in Section 6.2 is a bisimulation up to environment. We then want to prove the main compatibility lemma, akin to Theorem 6. [START_REF] Danvy | Type-directed partial evaluation[END_REF], by showing that

Y def = {( Ḟ v , t 0 , t 1 ) | t 0 Ḟ t 1 } ∪ { Ḟ v
} is a bisimulation up to bisimilarity. However, we can no longer proceed by induction on t 0 Ḟ t 1 , as for Theorem 6.16. Indeed, if p 0 = t 0 , p 1 = t 1 with t 0 Ḟ t 1 , and if t 0 is a control stuck term, then p 0 reduces to some term, but the induction hypothesis does not tell us anything about t 1 . To circumvent this, we decompose related delimited terms into related subcomponents. Lemma 6.34. If p 0 Ḟ p 1 , then either p 0 F p 1 , or one of the following holds:

• p 0 = v 0 ; • p 0 = F 0 [ E 0 [t 0 ] ], p 1 = F 1 [ E 1 [t 1 ] ] , F 0 F F 1 , E 0 F E 1 , t 0 F t 1 and t 0 → v t 0 or t 0 is stuck; • p 0 = F 0 [ E 0 [r 0 ] ], p 1 = F 1 [ E 1 [t 1 ] ] , F 0 F F 1 , E 0 F E 1 , r 0 Ḟ t 1 but r 0 F t 1 .
Lemma 6.34 generalizes Proposition 2.7 to related delimited terms: we know p 0 can be decomposed into contexts F , E , and a redex r, and we relate these subterms to p 1 . We can then prove that Y (defined above) is a bisimulation up to bisimilarity, by showing that, in each case described by Lemma 6.34, p 0 and p 1 reduce to terms related by Y. From this, we deduce F is a congruence, and is sound w.r.t. P.

Theorem 6.35. If t 0 F t 1 , then C [t 0 ] Ḟ v C [t 1 ].

RR n°9096

Corollary 6.36 (Soundness). We have F ⊆ P.

Remark 6.37. Following the ideas behind Definition 6.27, one can define an applicative bisimilarity B for delimited terms. A relation R on closed terms is a delimited applicative simulation if the following conditions are met:

• if t 0 R t 1 and t 0 and t 1 are not both delimited terms, then for all closed E , we have We conjecture B to be sound w.r.t. P, but we do not know how to apply Howe's method to B. To prove that the Howe's closure B • is a delimited applicative bisimulation, we need a version of Lemma 6.34 which decomposes terms related by B • . The clause B • B ⊆ B • in the definition of the Howe's closure makes writing such a decomposition lemma difficult. We believe a new proof technique is necessary to show the soundness of B.

E [t 0 ] R E [t 1 ] ; • p 0 R p 1 implies -if p 0 → v p 0 ,
We prove that F is complete by showing that P is a big-step bisimulation. Theorem 6.38 (Completeness). We have P ⊆ F.

Proof. We prove that X = {(P v , t 0 , t 1 ) | t 0 P t 1 }∪{P v } is a delimited big-step environmental bisimulation.

Let t 0 X P v t 1 such that t 0 and t 1 are not both delimited terms. Because P is a congruence, we have E 0

[t 0 ] P E 1 [t 1 ] for all E 0 P v E 1 , i.e., E 0 [t 0 ] X P v E 1 [t 1 ] as wished. Let p 0 X P v p 1 such that p 0 → * v v 0 .
We have p 0 → * v v 0 , so by definition of P, there exists v 1 such that p 1 → * v v 1 , which implies p 1 → * v v 1 (because p 1 is delimited). By Proposition 6.30, we have p 0 F v 0 and p 1 F v 1 , which implies p 0 P v 0 and p 1 P v 1 by soundness of F. Transitivity of P gives v 0 P v 1 , hence we have We can also define up-to techniques adapted to delimited terms, but we have the same limitations as in Section 6.3 for bisimulation up to context.

P v ∪ {(v 0 , v 1 )} = P v ∈ X ,

RR n°9096

Examples

Because delimited environmental bisimilarity is sound and complete, and delimited normal-form bisimulation is sound, any equivalence proved in Section 4.7 also holds with delimited environmental bisimilarity; in particular, we also have ≡ ⊆ F • . However, as in relaxed semantics, the lack of tractable enough environmental bisimulation up to context makes the equivalence proofs more difficult with environmental than with normal-form bisimulation. Combining the proof techniques can help, e.g., for the S elim axiom. with nested contexts. We define inductively two sequences of terms which represent all these possible nestings, and we prove they are delimited bisimilar. The complete proof can be found in Appendix C.3.

Conclusion

In the relaxed semantics, the environmental bisimilarity E tests λ-abstractions and control stuck terms by, respectively, applying them to values, and putting them into a pure evaluation context (surrounded by a reset). The testing arguments and contexts are generated from an environment, which represents the current knowledge of an outside observer about the tested terms. The resulting relation is sound and complete w.r.t. C. Plain environmental bisimulation is harder to use than applicative bisimulation, but it is supposed to be used in conjunction with up-to techniques. With up-to techniques (and their combination, as in Section 6.4), the proofs can be simpler than with applicative bisimilarity (compare, e.g., Example 6.22 with Example 5.9), and the candidate relations can be very small (see, e.g., Example 6.21). However, the bisimulation up to context that we define here is not as helpful as we could hope (see Section 6.3), and cannot be used when proving, e.g., the β Ω axiom. A different framework seems to be required, like the one we use in [START_REF] Aristizábal | Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation[END_REF].

We also define an environmental bisimilarity F for the original semantics, which is complete w.r.t. the contextual equivalence P. The difference with E is that we put terms that are not delimited into a context E before comparing them. Unlike applicative bisimilarity (see Remark 6.37), the soundness proof technique for the environmental bisimilarity is flexible enough to be adapted to this setting. Note that the definition of F (Definition 6.27) is only a small improvement over the definition of P, as it contains a quantification over (pure) contexts for a large class of terms (the non-delimited terms), and the resulting equivalence proof technique is much more difficult to use than delimited normalform bisimilarity (compare the proof of Proposition 4.41 to Appendix C.3). A future work would be to restrict the class of terms on which such a quantification over contexts is necessary.

Extensions

In this section, we discuss how our results are affected if we consider other semantics for λ S , or if we study other delimited-control operators.

Local Reduction Rules

In the semantics of Section 2, contexts are captured in one reduction step. Another usual way of computing capture is to use local reduction rules, where the context is consumed piece by piece [START_REF] Felleisen | The theory and practice of first-class prompts[END_REF]. Formally, we introduce elementary contexts, defined as follows:

Elementary contexts:

D ::= v | t
The reduction rule (shift) is then replaced with the next two rules.

F [D[Sk.t]] → v F [Sk .t{λx. k D[x] /k}] with x, k / ∈ fv(D) ∪ fv(t) (shift D ) F [ Sk.t ] → v F [ t{λx.x/k} ] (shift I )
As we can see in rule (shift D ), the capture of an elementary context does not require a reset, and it leaves the operator shift in place to continue the capture process. The process stops when a reset is encountered, in which case the rule (shift I ) applies: the shift operator is removed, and its variable k is replaced with the function representing the delimited empty context.

Note that with local reduction rules, control stuck terms are of the form Sk.t (without any surrounding context). This has major consequences on the definition of normal-form bisimulations. Indeed, Definition 4.1 extracts from control stuck terms their surrounding pure contexts and the bodies of their shift operator, and then relates these sub-components. Without surrounding contexts, normal-form bisimilarity can only compare the shift bodies. As a result, there is no point in distinguishing Definition 4. The theory for applicative and environmental bisimulations is not affected by using local rules; in particular, we still have to compare control stuck terms with a pure context E for these two relations. However, a proof using a smallstep bisimulation of any kind becomes tedious with local rules. Indeed, these rules introduce a lot of redexes (first to capture a whole pure context, and then to reduce all the produced β-redexes), and a reduction of each redex has to be matched in a small-step relation. We, therefore, believe that the reduction rules of Section 2 are better suited to proving the equivalence of two λ S terms.

Call-by-Name Reduction Semantics

In call-by-name, arguments are not reduced to values before β-reduction takes place. Such a semantics can be achieved by changing the syntax of (pure) evaluation contexts as follows:

CBN pure contexts:

E ::= | E t CBN evaluation contexts: F ::= | F t | F
and by turning the β-reduction rule into

F [(λx.t 0 ) t 1 ] → n F [t 0 {t 1 /x}] (β n )
The rules (shift) and (reset) are the same as in call-by-value, but their meanings change because of the new syntax for call-by-name contexts. We still distinguish the relaxed semantics (without outermost enclosing reset) from the original semantics.

The results of this paper can be adapted to call-by-name by transforming values used as arguments into arbitrary terms, for example when comparing λabstractions with applicative bisimilarity, or when building testing terms from the environment in environmental bisimilarity. We can also relate the bisimilarities to the call-by-name CPS equivalence, which has been axiomatized by Kameyama and Tanaka [START_REF] Kameyama | Equational axiomatization of call-by-name delimited control[END_REF]. The axioms for call-by-name are the same or simpler than in call-by-value: the axioms • S , • val , and S • can be proved in call-by-name using bisimulations with the same proofs as in call-by-value. The call-by-value axioms β v , β Ω , and • lift are replaced by a single axiom for call-by-name β-reduction

(λx.t 0 ) t 1 = KT t 0 {t 1 /x},
which is straightforward to prove since the three bisimilarities contain reduction. Finally, the axiom S elim still holds only for the original semantics.

RR n°9096

CPS-based Equivalences

It is possible to go beyond CPS equivalence and use the CPS definition of shift and reset to define behavioral equivalences in terms of it: t 0 and t 1 are bisimilar in λ S if their translations t 0 and t 1 are bisimilar in the plain λcalculus. As an example, we can define CPS applicative bisimilarity A CPS as follows: given two closed terms t 0 and t 1 of λ S , we have t 0 A CPS t 1 if t 0 and t 1 are applicative bisimilar in the call-by-value λ-calculus [START_REF] Abramsky | Full abstraction in the lazy lambda calculus[END_REF]. We compare here this equivalence to the contextual equivalence P for the original semantics, since the CPS of Figure 1 is valid for that semantics only.

We conjecture that A CPS is sound w.r.t. P, but we show it is not complete. A CPS translated term is of the form λk 1 k 2 .t, where k 1 and k 2 stand for, respectively, the continuation and the metacontinuation of the term, which are λ-abstractions of a special shape. But applicative bisimilarity in λ-calculus compares terms with any λ-abstraction, not just a continuation or metacontinuation, making A CPS over-discriminating compared to P. Indeed, let i def = λy.y, v 0 def = λx.Ω and v 1 def = λx. x i Ω. We have v 0 P v 1 , roughly because v 0 diverges as soon as it is applied to a value v, and so does v 1 , either because v i diverges, or because v i converges and Ω then diverges (more formally, the relation

{(λx.Ω, λx. x i Ω)} ∪ {(Ω, t Ω) | t ∈ T c } ∪ {(Ω, v Ω) | v ∈ V c
} is an applicative bisimulation, included in C and, therefore, in P). The CPS translation of these terms, after some administrative reductions, yields

v 0 = λk 1 k 2 .k 1 (λx.Ω) k 2 ,
and

v 1 = λk 1 k 2 .k 1 (λxk 1 k 2 .x (λy.y) γ (λz.Ω v k 2 )) k 2
where γ is defined in Figure 1 and v is some value, the precise definition of which is not important. If

v def = λzk 2 .z (λx k 1 k 2 .i) i i, then v 0 v i → * v Ω and v 1 v i → * v i; the diverging part in v 1 , namely λz.Ω v k 2
, is thrown away by v instead of being eventually applied, as it should be if v was a continuation (the term λx k 1 k 2 .i is not in the 2-layer CPS).

A possible way to get completeness for A CPS could be to restrict the target language of the CPS translation to a CPS calculus, i.e., a subcalculus where the grammar of terms enforces the correct shape of arguments passed as values, continuations, or metacontinuations (as in, e.g., [START_REF] Kameyama | A sound and complete axiomatization of delimited continuations[END_REF]). However, even with completeness, we believe it is more tractable to work in direct style with the relations we define in this paper, than on CPS translations of terms: as we can see with v 0 and v 1 above, translating even relatively simple source terms leads to voluminous terms in CPS. Besides, A CPS compares all translated terms with a continuation (which corresponds to a context E ) and a metacontinuation (which corresponds to a metacontext F ), while bisimilarities in direct style need at most a context E to compare stuck terms.

Nonetheless, we believe that studying fully the relationship between CPSbased behavioral equivalences and direct-style equivalences is an interesting future work. We would like to consider other CPS translations, including a CPS translation for the relaxed semantics [START_REF] Materzok | Subtyping delimited continuations[END_REF], or the 1-layer CPS translation for the original semantics [START_REF] Danvy | Abstracting control[END_REF]. We would also like to know if it is possible to obtain a CPS-based soundness proof for normal-form bisimilarity, as described at the beginning of Section 4.2, to have a complete picture of the interactions between CPS and behavioral equivalences.

The λµ tp-Calculus

The λµ-calculus [START_REF] Parigot | λµ-calculus: an algorithmic interpretation of classical natural deduction[END_REF] contains a µ-construct that can be seen as an abortive control operator. In this calculus, we evaluate named terms of the form [α]t, and the names α are used as placeholders for evaluation contexts. Roughly, a µ term µα.[β]t is able to capture its whole (named) evaluation context [γ]E , and substitutes α with [γ]E in [β]t. Context substitution is the same as the one presented in Section 4.4. In particular, it is capture-free, e.g., in [β]t{[γ]E /α}, the free names of [γ]E (such as γ) cannot be bound by the µ constructs in t.

The λµ tp-calculus [START_REF] Herbelin | An approach to call-by-name delimited continuations[END_REF] extends the λµ-calculus by adding a special name tp which can be dynamically bound during a context substitution. Besides, the µ-operator no longer captures the whole context, but only up to the nearest enclosing µ-binding of tp. As a result, a µ-binding of tp can be seen as a delimiter, and in fact, the λµ tp-calculus simulates λ S [START_REF] Herbelin | An approach to call-by-name delimited continuations[END_REF]. In particular, their CPS equivalences coincide. However, defining bisimilarities in λµ tp may lead to relations similar to the λµ-calculus ones [START_REF] Biernacki | Applicative bisimilarities for call-by-name and call-by-value λµ-calculus[END_REF] because of names. Indeed, we have to compare named values [α]v in λµ tp, which requires substituting α with some named context, as in the λµ-calculus [START_REF] Biernacki | Applicative bisimilarities for call-by-name and call-by-value λµ-calculus[END_REF]. Similarly, control stuck terms are of the form [α]F [µ tp.[β]v], and a way to relate them would be by replacing β with a context [γ]E or [ tp]E . It would be interesting to compare the behavioral theories of λ S and λµ tp to see if the encoding of the former into the latter is fully abstract (i.e., preserves contextual equivalence).

Typed Setting

Applicative, normal-form, and environmental bisimilarities have been studied in various typed settings, with different issues arising for each style of bisimilarity. In [START_REF] Gordon | Bisimilarity as a theory of functional programming[END_REF], Gordon points out that in a typed call-by-name λ-calculus, a context cannot distinguish a non-terminating term t from λx.t when they are both given a type of the form A → B. As a result, the untyped definition of applicative bisimilarity is no longer suited in this case. Gordon fixed this issue in [START_REF] Gordon | Bisimilarity as a theory of functional programming[END_REF] by distinguishing passive from active types in its labeled transition system: a term with a passive type (such as a function type A → B) can make a transition whether it converges or not, while terms of active type (such as int, . . . ) can make a transition only if it converges. Such a distinction is not necessary in call-by-value (all types are active). Applicative bisimilarity has also been defined for a typed object calculus in [START_REF] Gordon | Bisimilarity for a first-order calculus of objects with subtyping[END_REF].

Normal-form bisimulation has been defined for a calculus with recursive types [START_REF] Lassen | Typed normal form bisimulation[END_REF], a result then extended to existential types [START_REF] Lassen | Typed normal form bisimulation for parametric polymorphism[END_REF]. The difficulty here is to compare functions of type A → B, when A is an empty type, such as µX.bool × X. These functions should be equivalent in call-by-value, and with applicative bisimilarity, we can relate them by simply arguing that there are no argument values of type A. But normal-form bisimilarity does not have any quantification over arguments. In [START_REF] Lassen | Typed normal form bisimulation[END_REF], the authors propose a normal-form bisimilarity which decomposes values using ultimate patterns which describe the structure of a value along with some type information: values are then equated if their ultimate patterns can be related.

Environmental bisimulation has also been defined for a calculus with recursive and existential types in [START_REF] Sumii | A bisimulation for type abstraction and recursion[END_REF], a result extended to a store construct in [START_REF] Sumii | A complete characterization of observational equivalence in polymorphic lambda-calculus with general references[END_REF]. Existential types restrict the way terms can be tested. Indeed, suppose we have two pairs t 0 def = 1, λx int .x = 0 and t 1 def = true, λx bool .¬x , both typed ∃A.A × (A → bool). A context cannot distinguish t 0 and t 1 , because the only term of type A a context has access to is 1 from t 0 and true from t 1 , and when these values are passed to respectively λx int .x = 0 and λx bool .¬x, we obtain the same result. However, the authors of [START_REF] Koutavas | From applicative to environmental bisimulation[END_REF] argue that applicative bisimilarity cannot relate these terms, because it tests λ-abstractions with arbitrary values. Therefore, more evolved relations are required, such as environmental bisimilarity. Indeed, environmental bisimilarity can store in its environment the values 1 and true with type A, and then use them to compare the λ-abstractions in t 0 and t 1 .

Danvy and Filinski propose a simply typed calculus with shift and reset in [START_REF] Danvy | A functional abstraction of typed contexts[END_REF], and parametric polymorphism has then been added to the language by Asai and Kamayema in [START_REF] Asai | Polymorphic delimited continuations[END_REF]. In such systems, types are assigned not only to terms, but also to contexts. Pure contexts E are given types of the form A B, where A is the type of the hole and B is the answer type, and evaluation contexts (also called metacontexts) F are assigned types of the form ¬A, where A is the type of the hole. A typing judgment Γ | B t : A | C roughly means that under the typing context Γ, the term t can be plugged into a pure context E of type A B and a metacontext F of type ¬C, producing a well-typed term

F [ E [t] ].
In general, the evaluation of t may capture the surrounding context of type A B to produce a value of type C, with B = C. Function types also contain extra information about the contexts the terms are plugged into: a term of type A C → D B can be applied to an argument of type A within a pure context of type B C and a metacontext of type ¬D.

The complexity of the type systems for shift and reset (compared to, e.g., plain λ-calculus) may have some consequences on the definition of a typed bisimilarity for the language. In particular, we wonder how the extra type annotations for pure contexts and metacontexts should be factored in the bisimilarities. It seems natural to include types for the pure contexts for control stuck terms, since pure contexts already occur in the definitions of applicative and environmental bisimilarities in that case; it is not clear if and how the types for the metacontexts should be mentioned. The study of a typed λ S can be interesting also to see how the types modify the equivalences between terms, in particular we wonder if the equivalences proved in this paper still hold in the presence of types. We leave this as a future work.

A related and unexplored topic is defining logical relations to characterize contextual equivalence for typed calculi with delimited continuations. So far, Asai introduced logical relation to prove the correctness of a partial evaluator for shift and reset [START_REF] Asai | Logical relations for call-by-value delimited continuations[END_REF], whereas Biernacka et al. in a series of articles proposed logical predicates for proving termination of evaluation in several calculi of delimited control [START_REF] Biernacka | Context-based proofs of termination for typed delimited-control operators[END_REF][START_REF] Biernacka | Typing control operators in the CPS hierarchy[END_REF][START_REF] Biernacka | Proving termination of evaluation for system F with control operators[END_REF]. We expect such logical relations to exploit the notion of context and metacontext and, therefore, to be biorthogonal [START_REF] Krivine | Classical logic, storage operators and second-order lambdacalculus[END_REF][START_REF] Pitts | Operational reasoning for functions with local state[END_REF]. Biorthogonal and step-indexed Kripke logical relations have been proposed for an ML-like language with call/cc by Dreyer et al. [START_REF] Dreyer | The impact of higher-order state and control effects on local relational reasoning[END_REF] and adapting this approach to a similar language based on Asai and Kameyama's polymorphic type system for shift and reset [START_REF] Asai | Polymorphic delimited continuations[END_REF] presents itself as an interesting topic of future research. An alternative to step-indexed Kripke logical relations that also have been shown to account for abortive continuations are parametric bisimulations [START_REF] Hur | A logical step forward in parametric bisimulations[END_REF], built on relation transition systems of Hur et al. [START_REF] Hur | The marriage of bisimulations and Kripke logical relations[END_REF]. Whether such hybrids of logical relations and bisimulations can effectively support reasoning about delimited continuations is an open question.

7.6. Other Delimited-Control Operators CPS hierarchy. The operator shift and reset are just an instance of a more general construct called the CPS hierarchy [START_REF] Danvy | Abstracting control[END_REF]. As explained in Section 2.4, shift and reset have been originally defined by a translation into CPS. When iterated, the CPS translation leads to a hierarchy of continuations, in which it is possible to define a hierarchy of control operators shift i and reset i (i ≥ 1) that generalize shift and reset, and that make it possible to separate computational effects that should exist independently in a program. For example, in order to collect the solutions found by a backtracking algorithm implemented with shift 1 and reset 1 , one has to employ shift 2 and reset 2 , so that there is no interference between searching and emitting the results of the search. The CPS hierarchy was also envisaged to account for nested computations in hierarchical structures. Indeed, as shown in [START_REF] Biernacka | An operational foundation for delimited continuations in the CPS hierarchy[END_REF], the hierarchy naturally accounts for normalization by evaluation algorithms for hierarchical languages of units and products, generalizing the problem of computing disjunctive or conjunctive normal forms in propositional logic.

In the hierarchy, a shift operator of level i captures the context up to the first enclosing reset i or reset j with j > i. So for example in

E 1 [ E 0 [S 1 k.t] 2 ] 1 , the S 1 captures only E 0 , not E 1 .
We believe the results of this paper generalize to the CPS hierarchy without issues. The notions of pure context and control stuck term now depend on the hierarchy level: a pure context of level i does not contain a reset j (for j ≥ i) encompassing its hole, and can be captured by an operator shift i . A control stuck term of level i is an operator shift i in a pure context of level i. The definitions of bisimulations have to be generalized to deal with control stuck terms of level i the same way we treat stuck terms of level 1. For example, two control stuck terms of level i are applicative bisimilar if they are bisimilar when put in an arbitrary level i pure context surrounded by a reset i . The proofs for i = 1 should carry through to any i. shift 0 . The operator shift 0 (S 0 ) allows a term to capture a pure context with its enclosing delimiter [START_REF] Danvy | Abstracting control[END_REF]. The capture reduction rule for this operator is thus as follows:

F

[ E [S 0 k.t] ] → v F [t{λx. E [x] /k}], with x / ∈ fv(E ) Note that there is no reset around t in F [t{λx. E [x] /k}].
Consequently, a term is able to directly decompose an evaluation context F into pure contexts through successive captures with S 0 ; this is not possible in λ S .

The definitions of bisimilarities of this paper should extend to a calculus with shift 0 as far as the relaxed semantics is concerned. Since a term is able to access the context beyond the first enclosing reset, contextual equivalence is more discriminating with shift 0 than in λ S . For example, t is no longer equivalent to t , as we can see by taking t = S 0 k.S 0 k.Ω.

For the original semantics (that in the case of shift 0 assumes a persistent top-level reset), the definitions have to take into account the fact that a delimited term t may evaluate to a control stuck term (like, e.g., S 0 k.S 0 k.t for any t) and that, therefore, it is not sufficient to compare values with values only. For instance, in order to validate the following equation taken from the axiomatization of shift 0 [START_REF] Materzok | Axiomatizing subtyped delimited continuations[END_REF]:

S 0 k. (λx.S 0 k .k x) t = M t, with k / ∈ fv(t)
we would have to be able to compare normal forms of different kinds, which can be achieved by putting the normal forms in a context E for any E .

control and prompt. The control operator (F) captures a pure context up to the first enclosing prompt (#), but the captured context does not include the delimiter [START_REF] Felleisen | The theory and practice of first-class prompts[END_REF]. Formally, the capture reduction rule is as follows:

F [#E [Fk.t]] → v F [#t{λx.E [x]/k}], with x / ∈ fv(E )
Unlike with shift and reset where continuation composition is static, with control and prompt it is dynamic, in the sense that the extent of control operations in the captured context comprises the context of the resumption of the captured context [START_REF] Biernacki | On the static and dynamic extents of delimited continuations[END_REF]. A control 0 variant also exists [START_REF] Shan | A static simulation of dynamic delimited control[END_REF], where the delimiter is captured with the context but not kept: as a result, no delimiter is present in the righthand side of the capture reduction rule. The theory of this paper should extend to control and prompt with minor changes. However, studying this calculus would still be interesting to pinpoint the differences between the equivalences of shift/reset and control/prompt. For example, ##t is equivalent to #t, the same way t is equivalent to t . In fact, we conjecture the axioms can still be proved equivalent if we replace shift and reset with control and prompt (with the same restriction for S elim ). In

contrast, t 0 def = (Sk 1 .k 1 (λx.Sk 2 .t) Ω) v (where k 1 , k 2 , x / ∈ fv(t)) is equivalent to Sk.Ω (because t 0 E -→→ * v E [Sk 2 .t
] Ω , and this term always diverges), but

the term t 0 def = (Fk 1 .k 1 (λx.Fk 2 .t) Ω) v is equivalent to #t (because t 0 E -→→ * v #E [Sk 2 .t] Ω → v #t).
Maybe we can find (general enough) laws which hold with control and prompt but not with shift and reset, and conversely.

Multiple prompts. In languages with (named) multiple prompts [START_REF] Gunter | A generalization of exceptions and control in ML-like languages[END_REF][START_REF] Dybvig | A monadic framework for delimited continuations[END_REF][START_REF] Downen | A systematic approach to delimited control with multiple prompts[END_REF] control delimiters (prompts) as well as control operators are tagged with names, so that the control operator captures the evaluation context up to the dynamically nearest delimiter with the matching name. In a calculus with tagged shift (S a ) and reset ( • a ) the operational semantics of shift is given by the following rule:

F [ F [S a k.t] a ] → v F [ t{λx. F [x] a /k} a ], with a / ∈ #(F ) and x / ∈ fv(E )
where #(F ) is the set of the prompts guarding the hole of F . Such calculi resemble the CPS hierarchy, already considered in this section, however there are differences in their semantics. In contrast to the CPS hierarchy, where evaluation contexts form a hierarchy3 and the extent of control operations of level i is limited by control delimiters of any level j ≥ i, in the calculus with multiple prompts the evaluation context is a list of the standard CBV evaluation contexts separated by named prompts and the control operations reach across any prompts up to a matching one. Moreover, the salient and unique feature of such calculi is dynamic name generation that allows one, e.g., to eliminate unwanted interactions between the control operations used to implement some control structure (e.g., coroutines) and the control operations of the code that uses the control structure.

Even without dynamic name generation, which gives an additional expressive power to such calculi, calculi with multiple prompts generalize, e.g., simple exceptions [START_REF] Gunter | A generalization of exceptions and control in ML-like languages[END_REF] and the catch/throw constructs [START_REF] Crolard | A confluent lambda-calculus with a catch/throw mechanism[END_REF]. The results of this article can be seamlessly adapted to these calculi and most, if not all, of the presented techniques should carry over without surprises.

However, when dynamic name generation is included in the calculus, comparing two terms becomes more difficult, as prompts with the same purpose can be generated with different names. With environmental bisimilarity, we can use environments to remember the relationships between generated prompts. We do so in [START_REF] Aristizábal | Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation[END_REF] and define sound and complete environmental bisimilarities and their up-to techniques for a calculus with dynamically generated prompt names. Resource generation makes the definition of a sound applicative bisimilarity difficult for such a calculus, as argued in [START_REF] Koutavas | From applicative to environmental bisimulation[END_REF].

Other Constructs

Here, we briefly discuss what happens when λ S is extended with constructs that can be found in usual programming languages.

Constants. While adding constants (such as numerals, booleans, . . . ) to the language does not raise any issue for applicative [START_REF] Gordon | Bisimilarity as a theory of functional programming[END_REF] and environmental bisimilarities, defining a satisfactory normal-form bisimilarity in the presence of constants raises some difficulties. On one hand, we do not have to tweak the definition of normal-form bisimilarity to validate the η law (with the operator), as it does no longer hold with constants. However, as pointed out in [START_REF] Støvring | A complete, co-inductive syntactic theory of sequential control and state[END_REF], the difficulty is in relating open terms featuring constant expressions: e.g., it is not clear how to define a normal-form bisimulation which equates x + y and y + x. Relying on encodings of constants into plain λ-calculus is not enough, as these encodings usually do not respect the properties of the constants, like, for example, commutativity of +.

Store. Bisimilarities for languages with store are usually of the environmental kind [START_REF] Sangiorgi | Environmental bisimulations for higher-order languages[END_REF][START_REF] Koutavas | Small bisimulations for reasoning about higherorder imperative programs[END_REF][START_REF] Sumii | A complete characterization of observational equivalence in polymorphic lambda-calculus with general references[END_REF], and [START_REF] Koutavas | From applicative to environmental bisimulation[END_REF] argues that the usual form of applicative bisimilarity is not sound in presence of store. An exception is Støvring and Lassen's study of λµρ [START_REF] Støvring | A complete, co-inductive syntactic theory of sequential control and state[END_REF] (a calculus with store and an abortive control construct inspired by Parigot's λµ [START_REF] Parigot | λµ-calculus: an algorithmic interpretation of classical natural deduction[END_REF]), where normal-form bisimilarity is sound and complete. But the work in [START_REF] Støvring | A complete, co-inductive syntactic theory of sequential control and state[END_REF] relies on the fact that in λµ-calculus (and in λµρ as well), terms are of the form [a]t, where the name a acts as a placeholder for an evaluation context. These names are also essential to be able to define a sound and complete applicative bisimilarity for λµ [START_REF] Biernacki | Applicative bisimilarities for call-by-name and call-by-value λµ-calculus[END_REF]. We do not have such names in λ S , so it is not clear that adding store to the calculus would lead to a sound and complete normal-form bisimilarity as in λµρ. We leave this study as a future work.

Exceptions. Like for store, Koutavas et al. give examples in [START_REF] Koutavas | From applicative to environmental bisimulation[END_REF] showing that applicative bisimilarity is not sound for a calculus with exceptions, and environmental bisimilarity should instead be used. Studying an extension of λ S with exceptions would be interesting to compare the encoding of exceptions using shift and reset [START_REF] Filinski | Representing monads[END_REF] to the native constructs. We leave this as a future work.

Conclusion and Future Work

In our study of the behavioral theory of a calculus with shift and reset, we consider two semantics: the original one, where terms are executed within an outermost reset, and the relaxed one, where this requirement is lifted. For each, we define a contextual equivalence (respectively P and C), that we try to characterize with different kinds of bisimilarities (normal-form N, R, M, applicative A, and environmental E, F). We also compare our relations to CPS equivalence ≡, a relation which equates terms with βη-equivalent CPS translations. We summarize in Figure 8 the relationships we proved in this paper between these relations.

When comparing term equivalence proofs, we can see that each bisimulation style has its strengths and weaknesses. Normal-form bisimulation arguably leads to the simplest proofs of equivalence in most cases, as it does not contain any quantification over arguments or testing contexts in its definition. For example, the β Ω axiom can be easily proved using normal-form bisimulation (Proposition 4.31); the proof with applicative or environmental bisimulations are much more complex (Propositions 5.23 and 6.26). Normal-form bisimulation can also be combined with up-to techniques, leading to minimal proof obligations. Indeed, proving that Turing's fixed-point combinator is bisimilar to its shift/reset variant can be done with a normal-form bisimulation up to context with two pairs only (Example 4.10). Proving the same result with applicative bisimulation requires more work (see Example 5.9), since the definition of up-to techniques remains an open problem for that style. With environmental bisimulation up to context, we also need only two pairs of terms (see Example 6.22), but one has to find the (not completely obvious) environment under which to compare them.

However, normal-form bisimulation cannot be used to prove all equivalences, since its corresponding bisimilarity is not complete. It can be too discriminating to relate very simple terms, like those in Propositions 4.18 and 4.7, even though refined normal-form bisimulation (Section 4.4) can help. Besides, normal-form bisimulation operates on open terms by definition, which requires to consider an extra normal form (open stuck terms) in the bisimulation proofs. Applicative and environmental bisimulations do not have these issues: their corresponding bisimilarities are complete, and they operate on closed terms. As a result, the proof that t is equivalent to t is shorter with applicative bisimulation than with normal-form bisimulation (compare Example 4.3 and Example 5.8), and even shorter if we use environmental bisimulation up to context (see Example 6.21). This is also true, e.g., for the • lift axiom (compare Proposition 4.30, 5.22, and 6.25).

To summarize, to prove that two given terms are equivalent, we would suggest to first try normal-form bisimulation and its up-to techniques, and if it fails, try applicative bisimulation, and next, environmental bisimulation (with its up-to techniques). The relations defined for the relaxed semantics can also be used as equivalence proof techniques for the original semantics, except if one wants to relate a control stuck term with a term which does not necessarily evaluate to a control stuck term, like, e.g., in the S elim axiom. In that case, only the normal-form and environmental bisimulations dedicated to the original semantics can be used.

Future work. Among the extensions discussed in Section 7, we believe that CPSbased behavioral equivalences (Section 7.3), the λµ tp calculus (Section 7.4), typed setting (Section 7.5), control and prompt (Section 7.6), and store (Section 7.7) are worth exploring.

The behavioral theory of abortive control operators is also interesting to look at, as it is more challenging than for delimited-control operators. Although our results for shift and reset carry over to delimited versions of abortive control operators call/cc and abort, where the computation can be aborted up to the nearest enclosing control delimiter [START_REF] Filinski | Representing monads[END_REF][START_REF] Kameyama | A sound and complete axiomatization of delimited continuations[END_REF], they do not cater for the undelimited abortive control operators such as, e.g., call/cc in Scheme, even if we restrict ourselves to an implicit top-level reset. First, our notions of program equivalence are based on multi-layered contexts, which can be too discriminating for one-layer aware abortive operators. Second, with an abortive control operator reduction is not preserved by evaluation contexts: t -→ t does not necessarily imply E [t] -→ E [t ] (e.g., if a capture happens in the first reduction), whereas the properties of the calculus we consider critically depend on the compatibility of the reduction relation.

The situation is a bit better in the λµ-calculus [START_REF] Parigot | λµ-calculus: an algorithmic interpretation of classical natural deduction[END_REF], because names allow us to see if a context is captured or not. As a result, some work has been carried out for variants of the λµ-calculus [START_REF] Lassen | Bisimulation for pure untyped λµ-caluclus (extended abstract)[END_REF][START_REF] Lassen | Head normal form bisimulation for pairs and the λµ-calculus[END_REF][START_REF] Støvring | A complete, co-inductive syntactic theory of sequential control and state[END_REF][START_REF] Biernacki | Applicative bisimilarities for call-by-name and call-by-value λµ-calculus[END_REF]. But as far as we know, the behavioral theory of a language similar to the λ-calculus extended with call/cc has not been established.

A. Normal-Form Bisimilarity

A.1. Normal-form bisimilarity

For this proof, we use a (very limited) version of bisimulation up to reduction. Given a relation R, we write t 0 R t 1 if there exist t 0 , t 1 such that t 0 → * v t 0 , t 1 → * v t 1 , and t 0 R t 1 . We define R C the same way as R C except on contexts of the form F [ E ], where we define it as follows:

E 0 [x] R E 1 [x] F 0 [x] R F 1 [x]
x fresh

F 0 [ E 0 ] C F 1 [ E 1 ]
and we define R NFη as R NFη except it uses R C to relate contexts.

Definition A.1. A relation R on terms is a normal-form simulation up to reduction if t 0 R t 1 implies:

• if t 0 → v t 0 , then there exists t 1 such that t 1 → * v t 1 , and there exist t 0 , t 1 such that t 0 → * v t 0 , t 1 → * v t 1 , and t 0 R t 1 ; • if t 0 is a normal form, then there exists t 1 such that t 1 ⇓ v t 1 and t 0 R NFη t 1 .
A relation R is a normal-form bisimulation up to reduction if both R and R -1 are normal-form simulations up to reduction.

Lemma A.2. If R is a bisimulation up to reduction, then R ⊆ N.

We write -→ F for a sequence of contexts

F 1 . . . F n , - → F [t] for F 1 [. . . F n [t]],
∅ for an empty sequence, and -→ F [ ] for the context represented by the sequence. For a relation R on contexts, we write

-→ F 0 R -→ F 1 if -→ F 0 = F 1 0 . . . F m 0 , -→ F 1 = F 1 1 . . . F m 1 , and for each 1 ≤ i ≤ m, F i 0 R F i 1 .
We define the relation (

-→ F 0 , t 0 ) [N] ( -→ F 1 , t 1 ) as: t 0 N t 1 (∅, t 0 ) [N] (∅, t 1 ) ( -→ F 0 , t 0 ) [N] ( -→ F 1 , t 1 ) F 0 N C F 1 (F 0 -→ F 0 , t 0 ) [N] (F 1 -→ F 1 , t 1 ) ( -→ F 0 , t 0 ) [N] ( -→ F 1 , t 1 ) -→ F 0 [t 0 ], -→ F 1 [t 1 ] delimited F 0 [x] N F 1 [t 1 ] x fresh (F 0 -→ F 0 , t 0 ) [N] (F 1 -→ F 1 , t 1 )
We write

-→ F 0 [N] -→ F 1 , if ( -→ F 0 , x) [N] ( -→ F 1 , x) holds for a fresh x. Lemma A.3. If -→ F 0 [N] -→ F 1 and -→ F 0 [ ]
is pure, then all the contexts in -→ F 0 and -→ F 1 are pure and pairwise related by N NFη .

Proof. By induction on the derivation of (

-→ F 0 , x) [N] ( -→ F 1 , x) (x fresh).
The rule which requires delimited terms in its premise can never be applied.

We define v 0 N v 1 as

v 0 N NFη v 1 v 0 N v 1 -→ E 0 N C -→ E 1 E 0 N C E 1 x fresh λx. E 0 [ -→ E 0 [x]] N λx. E 1 [ -→ E 1 [x]]
We write -→ σ for a sequence of substitutions σ 1 . . . σ n , where each σ i is of the form {v i /x i }, such that:

1.

x i = x j for i = j, 2. if i ≤ j then x i ∈ fv(v j ).
We write t σ for (. . .

(tσ 0 )σ 1 . . . )σ n . The set {x 1 , . . . , x n } is the domain of - → σ noted dom( - → σ ). When x ∈ dom( - → σ )
and, therefore, is equal to some x i , we write -→ σ (x) for the value v i . We also write -→ σ -→ σ for the concatenation of two sequences of substitutions -→ σ and -→ σ , if the resulting sequence satisfies the two conditions. We will often implicitly use the following lemma.

Lemma A.4. If - → σ (x) = v, then x - → σ = v - → σ .
Proof. Follows directly from the two conditions on sequences of substitutions.

We write -→

σ 0 N -→ σ 1 if σ 0 = {v 0 1 /x 1 } . . . {v 0 n /x n }, σ 1 = {v 1 1 /x 1 } . . . {v 1 n /x n }, and for each i, v 0 i N v 1 i . We define R def = {( -→ F 0 [t 0 ] -→ σ 0 , -→ F 1 [t 1 ] -→ σ 1 ) | ( -→ F 0 , t 0 ) [N] ( -→ F 1 , t 1 ), -→ σ 0 N -→ σ 1 } Lemma A.5. If v 0 N NFη v 1 and -→ σ 0 N -→ σ 1 , then v 0 -→ σ 0 R NFη v 1 -→ σ 1 .
Proof. Immediate by the definition of R.

Lemma A.6. If ( -→ F 0 F 0 , t 0 ) [N] ( -→ F 1 F 1 , t 1 ) with F 0 [x] N F 1 [x]
for a fresh x and some delimited terms t 0 , t 1 , then for all v 0 N NFη v 1 , there exist t 0 , t 1 such that

-→ F 0 [F 0 [v 0 ]] → * v t 0 , -→ F 1 [F 1 [v 1 ]] → * v t 1 , and t 0 R t 1 .
Proof. By induction on the size of

-→ F 0 , -→ F 1 . If -→ F 0 = -→ F 1 = ∅, then we have (∅, F 0 [x]) [N] (∅, F 1 [x]), which implies F 0 [x]{v 0 /x} R F 1 [x]{v 1 /x}, hence the result holds. Suppose -→ F 0 = --→ F (3) 0 F 0 , -→ F 1 = --→ F (3) 1 F 1 . If F 0 N C F 1 , then ( -→ F 0 , F 0 [x]) [N] ( -→ F 1 , F 1 [x]), which implies -→ F 0 [F 0 [x]]{v 0 /x} R -→ F 1 [F 1 [x]
]{v 1 /x}, hence the result holds. Otherwise, we have F 0 [y] N F 1 [y] for a fresh y, and F 0 [t 0 ], F 1 [t 1 ] are delimited, which is possible only if either F 0 and F 1 are both delimited, or F 0 = F 1 = , or if one is delimited and the other is . In the first case, we have (

-→ F 0 , F 0 [x]) [N] ( -→ F 1 , F 1 [x]), which implies -→ F 0 [F 0 [x]]{v 0 /x} R -→ F 1 [F 1 [x]]{v 1 /x}. If F 0 = F 1 = ∅, then we have ( --→ F (3) 0 F 0 , t 0 ) [N] ( --→ F (3)
1 F 1 , t 1 ), and the induction hypothesis gives us the required result.

RR n°9096

In the last case, we assume (without loss of generality) that F 0 = and F 1 is delimited. Since we have

F 0 [x] N F 1 [x], there exists v 1 such that F 1 [x] ⇓ v v 1 and x N NFη v 1 . We have ( --→ F (3) 0 F 0 , t 0 ) [N] ( --→ F (3) 1 F 1 , F 1 [t 1 ]
), so by the induction hypothesis, for a fresh y, there exists t 0 , t 1 such that

--→ F (3) 0 [F 0 [y]] → * v t 0 , --→ F (3) 1 [F 1 [y]] → * v t 1
, and t 0 R t 1 . Hence, we have

-→ F 0 [F 0 [v 0 ]] = --→ F (3) 0 [F 0 [v 0 ]] → * v t 0 {x/y}{v 0 /x}, and -→ F 1 [F 1 [v 1 ]] → * v --→ F (3) 1 [F 1 [v 1 ]] → * v t 1 {v 1 /y}{v 1 /x},
with the resulting terms related by R, as wished.

Lemma A.7. If -→ F 0 [N] -→ F 1 and -→ σ 0 N -→ σ 1 then -→ F 0 [ ] -→ σ 0 R C -→ F 1 [ ] -→ σ 1 . Proof. If -→ F 0 [ ] is pure, then -→ F 1 [
] is pure by Lemma A.3, and we have (

-→ F 0 , x) [N] ( -→ F 1 , x
) by definition, hence the result holds.

Otherwise, we have

-→ F 0 = -→ F 0 F 0 [ E 0 ] -→ E 0 , -→ F 1 = -→ F 1 F 1 [ E 1 ] -→ E 1 , with F 0 [x] N F 1 [x] and E 0 [x] N E 1 [x] for a fresh x. We have to prove E 0 [ -→ E 0 [x]] -→ σ 0 R E 1 [ -→ E 1 [x]] -→ σ 1 , and -→ F 0 [F 0 [x]] -→ σ 0 → * v t 0 , -→ F 1 [F 1 [x]] -→ σ 1 → * v t 1 for some t 0 , t 1 such that t 0 R t 1 .
The former is easy to check, because we necessarily have (

-→ E 0 , x) [N] ( -→ E 1 , x). The latter is a consequence of Lemma A.6, by taking v 0 = v 1 = x. Lemma A.8. If y 0 , . . . , y m is a sequence of variables such that - → σ (y i ) = v i+1
for 0 ≤ i ≤ m -1 with y i N NFη v i for 1 ≤ i ≤ m, then for any sequence of fresh variables z 1 , . . . , z m and a value v, there exist a sequence of contexts E 1 , . . . , E m and a sequence of values v 0 , . . . , v m such that

(y 0 v) - → σ → * v E 1 . . . E m [y m v m ]{v m-1 /z m } . . . {v 0 /z 1 } - → σ
where for 1 ≤ i ≤ k, N C E i and z i N NFη v i , and also v 0 = v.

Proof. By induction on m.

Lemma A.9. Let -→ F 0 [N] -→ F 1 , v 0 N NFη v 1 , -→ σ 0 N -→ σ 1 , and v = x -→ σ 0 .
• If v is a variable, then there exists t 1 such that

-→ F 1 [x v 1 ] -→ σ 1 ⇓ v t 1 and -→ F 0 [x v 0 ] -→ σ 0 R NFη t 1 .
• If v is a λ-abstraction, then there exist t 0 , t 1 such that

-→ F 0 [x v 0 ] -→ σ 0 → v t 0 , -→ F 1 [x v 1 ] -→ σ 1 → * v t 1 , and t 0 R t 1 .
Proof. There exists a sequence of variables y 0 = x, . . . , y m such that -→ σ 0 (y

i ) = y i+1 for 0 ≤ i ≤ m -1 and -→ σ 0 (y m ) = v. But then -→ σ 1 (y i ) = v 1 i for 0 ≤ i ≤ m with y i N NFη v 1 i-1 for 1 ≤ i ≤ m,
i N NFη w 1 i for 1 ≤ i ≤ m and w 1 0 = v 1 , with -→ F 1 [x v 1 ] -→ σ 1 → * v -→ F 1 -→ E 1 [v 1 m z m+1 ]{w 1 m /z m+1 }{w 1 m-1 /z m } . . . {w 1 0 /z 1 } -→ σ 1 , RR n°9096
where z 1 , . . . , z m+1 are fresh variables. We now distinguish cases based on v.

If v = y, then because y N NFη v 1 m , there exists E 1 m+1 , w 1 m+1 such that v 1 m z m+1 ⇓ v E 1 m+1 [y w 1 m+1 ], N C E 1 m+1
, and z m+1 N NFη w 1 m+1 . Consequently, we have

-→ F 1 [x v 1 ] -→ σ 1 → * v -→ F 1 -→ E 1 [y w 1 m+1 ]{w 1 m /z m+1 }{w 1 m-1 /z m } . . . {w 1 0 /z 1 } -→ σ 1 ,
but we also have

-→ F 0 [x v 0 ] -→ σ 0 = -→ F 0 - → [y z m+1 ]{z m /z m+1 } . . . {v 0 /z 1 } -→ σ 0
We can then conclude by Lemmas A.5, and A.7.

If v = λy.t, then -→ F 0 [t 0 ] -→ σ 0 → v -→ F 0 [t{v 0 /y}] -→ σ 0 .
The obtained term can be represented as

-→ F 0 - → [λy.t z m+1 ]{z m /z m+1 }{z m-1 /z m } . . . {v 0 /z 1 } -→ σ 0 .
If λy.t N NFη v 1 m , then the obtained terms are related by R.

If t = E 0 [ -→ E 0 [y]] and v 1 m = λy. E 1 [ -→ E 1 [y]] where -→ E 0 N C -→ E 1 and E 0 N C E 1 ,
we also obtained two terms related by R.

Lemma A.10. If -→ E 0 [N] -→ E 1 , t 0 N t 1 , and -→ σ 0 N -→ σ 1 then -→ E 0 [Sk.t 0 ] -→ σ 0 R NFη -→ E 1 [Sk.t 1 ] -→ σ 1 .
Proof. From the definition of R, by Lemma A.7.

Lemma A.11.

If - → E = E 1 .
. . E m is a sequence of pure contexts such that for each 1 ≤ i ≤ m, E i N C , then for any fresh variables z 1 , . . . , z m and value v there exist v 0 . . . v m such that

- → E [v] ⇓ v v 0 {v 1 /z 1 } . . . {v m /z m } with z i N NFη v i-1 for 1 ≤ i ≤ m and v m = v.
Proof. By induction on m.

Lemma A.12. If -→ F 0 [N] -→ F 1 , - → [N] -→ E 1 , v 0 N NFη v 1 and -→ σ 0 N -→ σ 1 , then for a fresh z, there exist -→ σ 0 , -→ σ 1 such that -→ F 1 [ -→ E 1 [v 1 ]] -→ σ 1 → * v -→ F 1 [z] -→ σ 1 , -→ σ 0 N -→ σ 1 , and -→ F 0 [v 0 ] -→ σ 0 = -→ F 0 [z] -→ σ 0 R -→ F 1 [z] -→ σ 1 . Proof. By Lemma A.11, -→ E 1 [v 1 ] -→ σ 1 ⇓ v v 1 0 {v 1 1 /z 1 } . . . {v 1 m-1 /z m-1 }{v 1 /z m } -→ σ 1
where

z i N NFη v 1 i-1 for 1 ≤ i ≤ m.
The resulting term can be represented as

z{v 1 0 /z}{v 1 1 /z 1 } . . . {v 1 m-1 /z m-1 }{v 1 /z m } -→ σ 1 .
We also have v 0 -→ σ 0 = z{z 1 /z}{z 2 /z 1 } . . . {z m /z m-1 }{v 0 /z m } -→ σ 0 which allows us to conclude. Lemma A.13. R is a normal-form bisimulation up to reduction.

Proof. By case analysis on

-→ F 0 [t 0 ] -→ σ 0 .

Case:

-→ F 0 [t 0 ] -→ σ 0 is a normal form. There are several subcases:

Subcase: t 0 = F 0 [x v 0 ] and x -→ σ 0 = y. There exist F 1 and v 1 such that t 1 ⇓ v F 1 [x v 1 ] with F 0 N C F 1 and v 0 N NFη v 1 . Therefore, -→ F 1 [t 1 ] -→ σ 1 → * v -→ F 1 F 1 [x v 1 ] -→ σ 1 .
We conclude by Lemma A.9.

Subcase: t 0 = E 0 [Sk.t 0 ]. Then -→ F 1 = -→ E 1 and there exist E 1 and t 1 such that t 1 ⇓ v E 1 [Sk.t 1 ] with E 0 N C E 1 and t 0 N t 1 . Therefore, -→ E 1 [t 1 ] -→ σ 1 → * v -→ E 1 E 1 [Sk.t 1 ] -→ σ 1 .
We conclude by Lemma A.10.

Subcase: t 0 = v 0 . Then there exists v 1 so that t 1 ⇓ v v 1 and v 0 N NFη v 1 . We also have

-→ F 1 [t 1 ] -→ σ 1 → * v -→ F 1 [v 1 ] -→ σ 1 . If -→ F 0 = - →
, then we can conclude directly with Lemma A.12. Otherwise, we have

-→ F 0 = -→ F 0 F 0 - → , with F 0 not ; then -→ F 0 = -→ F 1 F 1 -→ E 1 , with -→ F 0 [N] -→ F 1 , F 0 N C F 1 , and - → [N]
-→ E 1 . By Lemma A.12, for a fresh z, there exist

-→ σ 0 , -→ σ 1 such that -→ F 1 F 1 [ -→ E 1 [v 1 ]] -→ σ 1 → * v -→ F 1 F 1 [z] -→ σ 1 , -→ σ 0 N -→ σ 1 , and -→ F 0 F 0 [v 0 ] -→ σ 0 = -→ F 0 F 0 [z] -→ σ 0 R -→ F 1 F 1 [z] -→ σ 1 . If F 0 [z]
is an open stuck term, we conclude by Lemma A.9; otherwise, F 0 [z] is a control stuck term (and the contexts in -→ F 0 , -→ F 1 are pure), and we conclude with Lemma A.10.

Case:

-→ F 0 [t 0 ] -→ σ 0 makes a transition. We have

-→ F 0 [t 0 ] -→ σ 0 → v t 0 .
For each of the following subcases, we prove that there exists t 1 such that -→

F 1 [t 1 ] -→ σ 1 → * v t 1 and t 0 R t 1 .
Subcase: t 0 → v t 0 . We have two possibilities. First, suppose

-→ F 0 = -→ F 0 F 0 - → , -→ F 1 = -→ F 1 F 1 - → , F 0 [x] N F 1 [x]
for a fresh x, t 0 , t 1 delimited, and t 0 → v v 0 .

Because t 0 N t 1 , there exists v 1 such that t 1 ⇓ v v 1 and v 0 N NFη v 1 . We have

-→ F 1 [t 1 ] → * v -→ F 1 [v 1 ]
, and we can conclude using Lemma A.6. Otherwise, we have

t 1 N t 0 (because → v ⊆ N), therefore -→ F 0 [t 0 ] -→ σ 0 R -→ F 1 [t 1 ] -→ σ 1 holds directly. Subcase: t 0 = E 0 [Sk.t 0 ] and -→ F 0 = F [ E ]. Then -→ F 0 = -→ F 0 F 0 [ E 0 ] -→ E 0 and -→ F 0 [t 0 ] -→ σ 0 → v -→ F 0 F 0 [ t 0 {λx. E 0 -→ E 0 E 0 [x] /k} ] -→ σ 0 = -→ F 0 F 0 [ t 0 ]{λx. E 0 -→ E 0 E 0 [x] /k} -→ σ 0 .
By bisimilarity, we know that

t 1 ⇓ v E 1 [Sk.t 1 ] with E 0 N C E 1 and t 0 N t 1 .
We also know that

-→ F 1 = -→ F 1 F 1 [ E 1 ] -→ E 1 where F 0 [y] N F 1 [y] for a fresh y, E 0 N C E 1 , and -→ E 0 [N] -→ E 1 . Since - → F 1 [t 1 ] -→ σ 1 → * v -→ F 1 F 1 [ t 1 {λx. E 1 -→ E 1 E 1 [x] /k} ] -→ σ 1 = -→ F 1 F 1 [ t 1 ]{λx. E 1 -→ E 1 E 1 [x] /k} -→ σ 1 ,
we obtain terms in R, as wished.

RR n°9096

Subcase:

t 0 = F 0 [x v 0 ] and x -→ σ 0 = λy.t 0 . By bisimilarity, t 1 ⇓ v F 1 [x v 1 ] with F 0 N C F 1 and v 0 N NFη v 1 .
By Lemma A.9, we know that we obtain terms in R, as wished.

Subcase: t 0 = v 0 . By bisimilarity, there exists v 1 such that t 1 ⇓ v v 1 with v 0 N NFη v 1 , and we also have

-→ F 1 [t 1 ] -→ σ 1 → * v -→ F 1 [v 1 ] -→ σ 1 . Suppose -→ F 0 = -→ F 0 F 0 - → ; then -→ F 1 = -→ F 1 F 1 -→ E 1 , with - → [N] -→ E 1 and necessarily F 0 N C F 1 . By Lemma A.11, we have -→ F 1 [v 1 ] -→ σ 1 → * v -→ F 1 F 1 [z 0 ]{v 1 0 /z 0 }{v 1 1 /z 1 } . . . {v 1 k /z k } -→ σ 1
where z 0 , . . . , z k are fresh variables,

z i N NFη v 1 i-1 for 1 ≤ i ≤ k, and v 1 k = v 1 . But the term - → F 0 [v 0 ] -→
σ 0 can also be represented as

-→ F 0 F 0 [z 0 ]{z 1 /z 0 }{z 2 /z 1 } . . . {v 0 /z k } -→ σ 0 . Suppose F 0 = F (3) 0 [ E 0 ]; then F 1 = F (3) 1 [ E 1 ], with F (3) 0 [z 0 ] N F (3) 1 [z 0 ] and E 0 [z 0 ] N E 1 [z 0 ] . We distinguish cases based on E 0 [z 0 ] . • If E 0 [z 0 ] → v t 0 with t 0 delimited, then we have t 0 N E 1 [z 0 ] , because → v ⊆ N. Therefore, we have -→ F 0 F (3) 0 [t 0 ]{z 1 /z 0 }{z 2 /z 1 } . . . {v 0 /z k } -→ σ 0 R -→ F 1 F (3) 1 [ E 1 [z 0 ] ]{v 1 0 /z 0 }{v 1 1 /z 1 } . . . {v 1 k /z k } -→ σ 1
as wished.

•

If E 0 [z 0 ] → v v 0 , then there exists v 1 such that E 1 [z 0 ] ⇓ v v 1 and v 0 N NFη v 1 .
We conclude by using Lemma A.6.

• If E 0 [z 0 ] is an open stuck term t 0 , then there exists t 1 such that E 1 [z 0 ] ⇓ v t 1 and t 0 N NFη t 1 . We conclude by using Lemma A.9.

Suppose F 0 is a pure context E 0 ; then

F 1 = E 1 , with E 0 [z 0 ] N E 1 [z 0 ]. We distinguish cases based on E 0 [z 0 ]. If E 0 [z 0 ] → v t 0 or if E 0 [z 0 ]
is an open stuck term, then we conclude as in the previous case.

If E 0 [z 0 ] is a control stuck term E 0 [Sk.t 0 ], then there exist E 1 , t 1 such that E 1 [z 0 ] ⇓ v E 1 [Sk.t 0 ], E 0 N C E 1 ,
and t 0 N t 1 . We conclude as in the case where t 0 is a control stuck term. This gives compatibility of N w.r.t. evaluation contexts. We can then prove easily compatibility w.r.t. λ-abstraction and shift.

A.2. Bisimulation up to context t R t t 0 R t 1 t 0 R t 1 t 0 R t 1 v 0 R NF v 1 t 0 {v 0 /x} R t 1 {v 1 /x} t 0 R t 1 F 0 R C F 1 F 0 [t 0 ] R F 1 [t 1 ] t 0 R t 1 t 0 , t 1 delimited F 0 [x] R F 1 [x]
x fresh

F 0 [t 0 ] R F 1 [t 1 ] t 0 R t 1 λx.t 0 R λx.t 1 t 0 R t 1 Sk.t 0 R Sk.t 1 Lemma A.14. If F 0 R C F 1 and v 0 R NF v 1 , then F 0 {v 0 /x} R C F 1 {v 1 /x}. Proof. By definition of R NF . Lemma A.15. If t 0 R NF t 1 , v 0 R NF v 1 ,
If F 0 R C F 1 and F 0 R C F 1 , then F 0 [F 0 ] R C F 1 [F 1 ]. Proof. By definition of R C . Lemma A.17. If F 0 R C F 1 , t 0 R NF t 1 , and F 0 [t 0 ] and F 1 [t 1 ] are normal form, then F 0 [t 0 ] R NF F 1 [t 1 ].
Proof. By case analysis on F 0 R C F 1 and t 0 R NF t 1 , using Lemma A. [START_REF] Danvy | Type-directed partial evaluation[END_REF] in the (open and control) stuck term cases.

Lemma A.18. If R is a bisimulation up to context and v 0 R t 1 , then there

exists v 1 such that t 1 ⇓ v v 1 and v 0 R NF v 1 .
Proof. By induction on the derivation of v 0 R t 1 . If v 0 = t 1 , then the result is direct. If v 0 R t 1 , then the result is a consequence of R being a bisimulation up to context. The result is also direct in the case of compatibility w.r.t. λ-

abstraction. The case v 0 = v 0 {v 0 /x}, t 1 = t 1 {v 1 /x} with v 0 R t 1 and v 0 R NF v 1 is straightforward by induction. If t 1 = E 1 [t 1 ] with v 0 R t 1 and x R E 1 [x],
then by the induction hypothesis, there exists v 1 such that t 1 ⇓ v v 1 with v 0 R NF v 1 , and we also have

E 1 [x] ⇓ v x.
As a result, we have

t 1 ⇓ v v 1 with v 0 R NF v 1 , as wished.

RR n°9096

The other possibility is

t 0 ⇓ v F 0 [x v 0 ] with F 0 {v 0 /x}[v 0 v 0 {v 0 /x}] ⇓ v t 0 .
By the induction hypothesis, there exist

F 1 , v 1 such that t 1 ⇓ v F 1 [xv 1 ], F 0 R C F 1 ,
and • If v 0 and v 1 are λ-abstractions λy.s 0 and λy.s 1 , then by definition of R NF , we have s 0 R s 1 . We have the following reductions.

v 0 R NF v 1 . From F 0 R C F 1 , v 0 R NF v 1 ,
F 0 {v 0 /x}[v 0 v 0 {v 0 /x}] → v F 0 {v 0 /x}[s 0 {v 0 {v 0 /x}/y}] F 1 {v 1 /x}[v 1 v 1 {v 1 /x}] → v F 1 {v 1 /x}[s 1 {v 1 {v 1 /x}/y}]
From (**) and s 0 R s 1 , we deduce s 0 {v 0 {v 0 /x}/y} R s 1 {v 1 {v 1 /x}/y} by definition of R. This result and (*) implies F 0 {v 0 /x}[s 0 {v 0 {v 0 /x}/y}] R F 1 {v 1 /x}[s 1 {v 1 {v 1 /x}/y}] by definition of R. We know that the term F 0 {v 0 /x}[s 0 {v 0 {v 0 /x}/y}] evaluates to t 0 in less than m -1 steps, therefore we can apply the induction hypothesis: there exists t 1 such that

F 1 {v 1 /x}[s 1 {v 1 {v 1 /x}/y}] ⇓ v t 1 and t 0 R NF t 1 .
One can check that we have t 1 {v 1 /x} ⇓ v t 1 , hence the result holds.

Case:

E 0 [t 0 ] R E 1 [t 1 ] with t 0 R t 1 and E 0 R C E 1 . We distinguish cases based on how E 0 [t 0 ] reduces to a normal form t 0 .
The first possibility is t 0 ⇓ v v 0 and E 0 [v 0 ] ⇓ v t 0 . By the induction hypothesis, there exists v 1 such that t 1 ⇓ v v 1 , and

v 0 R NF v 1 . Because E 0 [v 0 ] ⇓ v t 0 ,
[t 0 ] → * v t 0 {v 0 /x} ⇓ v t 0 , and E 1 [t 1 ] → * v t 1 {v 1 /x}. From t 0 R NF t 1 , v 0 R NF v 1
, and t 0 {v 0 /x} ⇓ v t 0 , we can conclude exactly as in the previous case about substituvity.

The other possibility is t 0 ⇓ v t 0 , t 0 is a normal form but not a value, and t 0 = E 0 [t 0 ]. By the induction hypothesis, there exists t 1 such that t 1 ⇓ v t 1 and

RR n°9096 t 0 R NF t 1 ; t 1 is also not a value. We have E 0 [t 0 ] ⇓ v E 0 [t 0 ], E 1 [t 1 ] ⇓ v E 1 [t 1 ],
and

E 0 [t 0 ] R NF E 1 [t 1
] by Lemma A.17, hence the result holds.

Case: F 0 [ E 0 [t 0 ] ] R F 1 [ E 1 [t 1 ] ] with F 0 [x] R F 1 [x], E 0 [x] R E 1 [x] (x fresh)
, and t 0 R t 1 . We distinguish cases based on how F 0 [ E 0 [t 0 ] ] reduces to a normal form t 0 .

1. Suppose t 0 ⇓ v t 0 , so that t 0 is an open stuck term. Therefore, we have

t 0 = F 0 [ E 0 [t 0 ] ]
. By the induction hypothesis, there exists an open stuck term

t 1 such that t 1 ⇓ v t 1 and t 0 R NF t 1 . We therefore have F 1 [ E 1 [t 1 ] ] → * v F 1 [ E 1 [t 1 ] ], F 1 [ E 1 [t 1 ]
] is an open stuck term, and

F 0 [ E 0 [t 0 ] ] R NF F 1 [ E 1 [t 1 ]
] holds by Lemma A.17. We therefore have the required result. 2. Suppose t 0 ⇓ v v 0 . By the induction hypothesis, there exists v 1 such that

t 1 ⇓ v v 1 and v 0 R NF v 1 .
We know that E 0 [v 0 ] must reduce to a normal form t 0 , which is either a value or an open stuck term. We have

E 0 [x] R E 1 [x]
for a fresh x, and v 0 R NF v 1 , so with the same reasoning as in the substitutivity case, we know there exists

t 1 such that E 1 [v 1 ] ⇓ v t 1
and t 0 R NF t 1 . We now distinguish cases based on the kind of t 0 , t 1 .

(a) Suppose t 0 and t 1 are values v 0 and v 1 . We have

F 0 [x] R F 1 [x] for a fresh x, v 0 R NF v 1 ,
and F 0 [v 0 ] ⇓ v t 0 , so using the same reasoning as in the substitutivity case, we know there exists t 1 such that F

1 [v 1 ] ⇓ v t 1 and t 0 R NF t 1 . We have F 1 [ E 1 [t 1 ] ] → * v F 1 [ E 1 [v 1 ] ] → * v F 1 [v 1 ] ⇓ v t 1 ,
hence the result holds. (b) Suppose t 0 and t 1 are open stuck terms. Then t 0 = F 0 [t 0 ]. We have

F 1 [ E 1 [t 1 ] ] ⇓ v F 1 [t 1 ], and F 0 [t 0 ] R NF F 1 [t 1 ] holds by Lemma A.19. 3. Suppose t 0 ⇓ v E 0 [Sk.t 0 ]
. By the induction hypothesis, there exists a con-

trol stuck term E 1 [Sk.t 1 ] such that t 1 ⇓ v E 1 [Sk.t 1 ] and E 0 [Sk.t 0 ] R NF E 1 [Sk.t 1 ]. We know E 0 [E 0 [Sk.t 0 ]
] must reduce to a normal form s 0 , and we have

E 0 [E 0 [Sk.t 0 ]] → v t 0 {λx. E 0 [E 0 [x]] /k} . Consequently, t 0 {λx. E 0 [E 0 [x]] /k} reduces to s 0 in m -1 steps or less. Because t 0 {λx. E 0 [E 0 [x]] /k} R t 1 {λx. E 1 [E 1 [x]
] /k} holds, using the induction hypothesis on m, we know there exists a normal form s 1 such that

t 1 {λx. E 1 [E 1 [x]] /k} ⇓ v s 1 and s 0 R NF s 1 . We have F 0 [ E 0 [t 0 ] ] → * v F 0 [s 0 ] and F 1 [ E 1 [t 1 ] ] → * v F 1 [s 1 ].
From there, we conclude as before by case analysis on the kind of s 0 and s 1 (either value or open stuck term).

Case: F 0 [t 0 ] R F 1 [t 1 ] with F 0 [x] R F 1 [x] (x fresh), t 0 R t 1 ,
and t 0 , t 1 delimited. We distinguish cases based on how t 0 reduces to a normal form.

If t 0 ⇓ v v 0 , then by the induction hypothesis, there exists v 1 such that

t 1 ⇓ v v 1 and v 0 R NF v 1 . By definition of R , there exist t 0 , t 1 such that F 0 [x] → * v t 0 , F 1 [x] → * v t 1 , and t 0 R t 1 . We have F 0 [t 0 ] → * v t 0 {v 0 /x}, F 1 [t 1 ] → * v t 1 {v 1 /x}, RR n°9096
with t 0 {v 0 /x} R t 1 {v 1 /x}, so from there we can conclude as in the substitutivity case.

If t 0 ⇓ v t 0 with t 0 an open stuck term, then by the induction hypothesis, there exists t 1 such that t 1 ⇓ v t 1 and t 0 R NF t 1 . We have

F 1 [t 1 ] ⇓ v F 1 [t 1 ],
and

F 0 [t 0 ] R NF F 1 [t 1 ]
holds by Lemma A.19.

A.3. Refined bisimilarity and refined bisimulation up to context

The proof of soundness of refined bisimilarity is an adaptation of the proofs of Section A.1 and Section A.4. We only point the main differences with these two proofs. We let σ range over regular and context substitutions. We define R as

v 0 R RNFη v 1 v 0 R v 1 -→ E 0 R C -→ E 1 E 0 R C E 1 E 0 -→ E 0 R E 1 -→ E 1
We use the same notations and constraints on sequences of substitutions and contexts as in Section A.1, and we define R as

R def = {( -→ F 0 [t 0 ] -→ σ 0 , -→ F 1 [t 1 ] -→ σ 1 ) | (t 0 , -→ F 0 ) [R] (t 1 , -→ F 1 ), -→ σ 0 R -→ σ 1 } Lemma A.22.
R is a refined bisimulation up to reduction.

Proof. By case analysis on -→ F 0 [t 0 ] -→ σ 0 . We only sketch the subcases where the proof differ from the proofs of Lemma A.13 and Lemma A. [START_REF] Hieb | [END_REF].

The first two subcases are in the case where -→ F 0 [t 0 ] -→ σ 0 is a normal form.

Subcase:

t 0 = E 0 [Sk.t 0 ], and
-→ F 0 = -→ E 0 . Then -→ F 1 = -→ E 1
, and there exist E 1 and t 1 such that t

1 ⇓ v E 1 [Sk.t 1 ] with t 0 {λx. k E 0 [x] /k} R t 1 {λx. k E 1 [x] /k} for a fresh k . Therefore, -→ E 1 [t 1 ] -→ σ 1 → * v -→ E 1 E 1 [Sk.t 1 ] -→ σ 1
, and we have

t 0 {λx. k -→ E 0 E 0 [x] /k} -→ σ 0 = t 0 {λx. k E 0 [x] /k} {k -→ E 0 /k } -→ σ 0 R t 1 {λx. k E 1 [x] /k} {k -→ E 1 /k } -→ σ 1 = t 1 {λx. k -→ E 1 E 1 [x] /k} -→ σ 1
for a fresh k , hence the result holds.

Subcase: t 0 = F 0 [ k v 0 ]
, and k -→ σ 0 = k . Similar to the corresponding subcase in the proof of Lemma A.33.

The next subcases are in the case where -→ F 0 [t 0 ] -→ σ 0 reduces (in one step) to a term t 0 , and we prove that -→ F 1 [t 1 ] -→ σ 1 reduces (in 0 or more steps) to a t 1 such that t 0 R t 1 .

Subcase: t 0 = E 0 [Sk.t 0 ] and -→ F 0 = F [ E ]. Then -→ F 0 = -→ F 0 F 0 [ E 0 ] -→ E 0 and -→ F 0 [t 0 ] -→ σ 0 → v -→ F 0 F 0 [ t 0 {λx. E 0 -→ E 0 E 0 [x] /k} ] -→ σ 0 = -→ F 0 F 0 [ t 0 {λx. k E 0 [x] /k} ]{E 0 -→ E 0 /k } -→ σ 0
for a fresh k . By bisimilarity, we know there exists

E 1 [Sk.t 1 ] such that t 1 ⇓ v E 1 [Sk.t 1 ] with t 0 {λx. k E 0 [x] /k} R t 1 {λx. k E 1 [x] /k} . We also know that -→ F 1 = -→ F 1 F 1 [ E 1 ] -→ E 1 where F 0 [y] R F 1 [y] for a fresh y, E 0 R C E 1 , and -→ E 0 R C -→ E 1 . Since - → F 1 [t 1 ] -→ σ 1 → * v -→ F 1 F 1 [ t 1 {λx. E 1 -→ E 1 E 1 [x] /k} ] -→ σ 1 = -→ F 1 F 1 [ t 1 {λx. k E 1 [x] /k} ]{E 1 -→ E 1 /k } -→ σ 1 ,
we get terms in R, as wished.

Subcase t 0 = F 0 [ k v 0 ] and k -→ σ 0 = E 0 .
Similar to the corresponding subcase in the proof of Lemma A.33.

We now adapt the proof of Section A.2 to refined bisimulation up to context. We remind that R is defined as R but we add the following rule:

t 0 R t 1 E 0 R C E 1 t 0 {E 0 /k} R t 1 {E 1 /k} Lemma A.23.
If R is a refined bisimulation up to context, then R is a non-eta refined bisimulation up to reduction.

Proof. We consider t 0 R t 1 with t 0 evaluating to t 0 in m steps; we prove that t 1 evaluates to a term t 1 so that t 0 R RNF t 1 . We proceed by induction on m, and on the derivation of t 0 R t 1 , ordered lexicographically. We only discuss the cases where the proof differs from the proof of Lemma A.21.

Case: Sk.t 0 R Sk.t 1 with t 0 R t 1 . We have to prove that t 0 {λx. k x /k} R t 1 {λx. k x /k} holds for a fresh k . Because R is reflexive, we have λx. k x R λx. k x ; we can then conclude using substitutivity and compatibility w.r.t. . .

Case: E 0 [t 0 ] R E 1 [t 1 ] with E 0 R C E 1 and t 0 R t 1 .
We discuss only the case where t

0 ⇓ v E 0 [Sk.t 0 ]. By the induction hypothesis, there exists E 1 [Sk.t 1 ] such that t 1 ⇓ v E 1 [Sk.t 1 ] and t 0 {λx. k E 0 [x] /k} R t 1 {λx. k E 1 [x] /k} for a fresh k . This implies t 0 {λx. k E 0 [x] /k} {k E 0 /k } R t 1 {λx. k E 1 [x] /k} {k E 1 /k } for a fresh k , i.e., t 0 {λx. k E 0 [E 0 [x]] /k} R t 1 {λx. k E 1 [E 1 [x]] /k} . Be- cause we have E 0 [t 0 ] ⇓ v E 0 [E 0 [Sk.t 0 ]] and E 1 [t 1 ] ⇓ v E 1 [E 1 [Sk.t 1 ]], we have the required result. Case: F 0 [ E 0 [t 0 ] ] R F 1 [ E 1 [t 1 ] ] with F 0 [x] R F 1 [x], E 0 [x] R E 1 [x] (x fresh)
, and t 0 R t 1 . We discuss only the case where t

0 ⇓ v E 0 [Sk.t 0 ]. By the induction hypothesis, there exists E 1 [Sk.t 1 ] such that t 1 ⇓ v E 1 [Sk.t 1 ] and t 0 {λx. k E 0 [x] /k} R t 1 {λx. k E 1 [x]
/k} for a fresh k . This implies

t 0 {λx. k E 0 [x] /k} {E 0 /k } R t 1 {λx. k E 1 [x] /k} {E 1 /k }, which in turn implies F 0 [ t 0 {λx. E 0 [E 0 [x]] /k} ] R F 1 [ t 1 {λx. E 1 [E 1 [x]] /k} ]. We also have F 0 [ E 0 [t 0 ] ] → * v F 0 [ t 0 {λx. E 0 [E 0 [x]] /k} ] and F 1 [ E 1 [t 1 ] ] → * v F 1 [ t 1 {λx. E 1 [E 1 [x]] /k} ].
From there, we can conclude as in the proof of Lemma A.21.

Case: t 0 {E 0 /k} R t 1 {E 1 /k} with t 0 R t 1 and E 0 R C E 1 .
We distinguish two cases. First, suppose t 0 ⇓ v t 0 , where t 0 is a normal form distinct from F 0 [ k v 0 ]. Then by the induction hypothesis, there exists t 1 such that t

1 ⇓ v t 1 and t 0 R RNF t 1 . We therefore have t 0 {E 0 /k} ⇓ v t 0 {E 0 /k}, t 1 {E 1 /k} ⇓ v t 1 {E 1 /k}, and t 0 {E 0 /k} R RNF t 1 {E 1 /k}, as required. Next, suppose t 0 ⇓ v F 0 [ k v 0 ]. Then by the induction hypothesis, there exists F 1 [ k v 1 ] such that t 1 ⇓ v F 1 [ k v 1 ], F 0 [ ] R C F 1 [ ], and v 0 R RNF v 1 . Therefore, we have t 0 {E 0 /k} → * v F 0 {E 0 /k}[ E 0 [v 0 {E 0 /k}] ] as well as t 1 {E 1 /k} → * v F 1 {E 1 /k}[ E 1 [v 1 {E 1 /k}] ]. Because F 0 {E 0 /k}[ E 0 [v 0 {E 0 /k}] ] R F 1 {E 1 /k}[ E 1 [v 1 {E 1 /k}] ],
we can conclude from there by case analysis on how F 0 {E 0 /k}[ E 0 [v 0 {E 0 /k}] ] reduces to a normal form.

A.4. Delimited normal-form bisimilarity

The proof is an adaptation of the one for the relaxed semantics. We let σ range over regular and context substitutions. We use the same notations on sequences of contexts as in Section A.1, and we define ( -→ F 0 , t 0 ) [M] ( -→ F 1 , t 1 ) by the following rules:

t 0 M t 1 t 0 , t 1 delimited (∅, t 0 ) [M] (∅, t 1 ) F 0 [x] M F 1 [x] x fresh ( -→ F 0 , t 0 ) [M] ( -→ F 1 , t 1 ) F 0 -→ F 0 [t 0 ], F 1 -→ F 1 [t 1 ] delimited (F 0 -→ F 0 , t 0 ) [M] (F 1 -→ F 1 , t 1 ) We write -→ F 0 [M] -→ F 1 if ( -→ F 0 , x ) [M] ( -→ F 1 , x
) holds for a fresh x. We implicitly use the following properties when manipulating contexts.

Lemma A.24. Let -→ F 0 = F 1 0 . . . F m 0 , -→ F 1 = F 1 1 . . . F m 1 . • ( -→ F 0 , t 0 ) [M] ( -→ F 1 , t 1
) holds for some delimited t 0 , t 1 iff for all 1 ≤ i ≤ m, either F i 0 = F i 1 = , or F i 0 , F i 1 are both delimited, or one of them is delimited and the other is .

•

-→ F 0 [M] -→ F 1 iff for all 1 ≤ i ≤ m, F i 0 [M] F i 1 .

RR n°9096

Proof. By induction on m.

We write

{E 0 /k} M {E 1 /k} (resp. {v 0 /x} M {v 1 /x}) if E 0 M C E 1 (resp. v 0 M NFη v 1 )
. We use the same notations and constraints on sequences of substitutions as in Section A.1, and we define R as

R def = {( -→ F 0 [t 0 ] -→ σ 0 , -→ F 1 [t 1 ] -→ σ 1 ) | ( -→ F 0 , t 0 ) [M] ( -→ F 1 , t 1 ), -→ σ 0 M -→ σ 1 } ∪ {(v 0 -→ σ 0 , v 1 -→ σ 1 ) | v 0 M NFη v 1 , -→ σ 0 M -→ σ 1 } Lemma A.25. If v 0 M v 1 , then v 0 M NFη v 1 .
Proof. Straightforward by unfolding the definition of v 0 M v 1 .

Lemma A.26. If t 0 M t 1 , then for any fresh k, we have k t 0 M k t 1 .

Proof. The result is obvious if t 0 and t 1 are not both delimited. For delimited terms, we prove that R def = {( k t 0 , k t 1 ) | t 0 M t 1 , t 0 , t 1 delimited} ∪ M is a delimited bisimulation. We proceed by case analysis on t 0 .

If t 0 ⇓ v v 0 , then by bisimilarity, there exists v 1 such that t

1 ⇓ v v 1 and v 0 M NFη v 1 . Consequently, we have k t 0 ⇓ v k v 0 , k t 1 ⇓ v k v 1 , with k R C k , and v 0 R NFη v 1 , as wished. If t 0 ⇓ v F 0 [x v 0 ], then by definition of M, there exist F 1 , v 1 , such that t 1 ⇓ v F 1 [x v 1 ], F 0 M C F 1 , and v 0 M NFη v 1 .
Because F 0 and F 1 are delimited (they are resulting from the evaluation of delimited terms), we have

F 0 = F 0 [ E 0 ], F 1 = F 1 [ E 1 ], and F 0 M C F 1 implies F 0 [y] M F 1 [y] and E 0 [y] M E 1 [y]
for any fresh y. As a result, we have we have k t

0 ⇓ v k F 0 [ E 0 [x v 0 ] ] , k t 1 ⇓ v k F 1 [ E 1 [x v 1 ] ] ,
and what remains to prove is that k F 0 [y] R k F 1 [y] holds for some fresh y. This is a consequence of F 0 [y] M F 1 [y], whether F 0 [y] and

F 1 [y] are both delimited (then k F 0 [y] R k F 1 [y] holds by definition of R) or not (then we have k F 0 [y] M k F 1 [y] ).
Lemma A.27. If x M NFη v, then for all fresh y, k, there exist F , E , and v such that k

(v y) ⇓ v F [ E [x v ] ], v M NFη y, [M] F , and E M C k . Proof. Unfolding the definition of x M NFη v, we know there exist F , v such that k (v y) ⇓ v F [x v ] , v M NFη y, and F M C k (we know there is a reset surrounding F because k (v y) is delimited). From F M C k , we deduce that F = F [ E ] with F [z] M z and E M C k .
Either there is only one reset surrounding the hole in F , and F = , F = E , or there are more than one, and F is delimited. In both cases, we have F [M] , as required.

Lemma A.28. If y 0 , . . . , y m is a sequence of variables such that -

→ σ (y i ) = v i+1 for 0 ≤ i ≤ m -1 with y i M NFη v i for 1 ≤ i ≤ m,
v] - → σ → * v F 1 . . . F m [ E m [y m v m ] ]{E m-1 /k m }{v m-1 /z m } . . . {E 0 /k 1 }{v 0 /z 1 } - → σ RR n°9096 Lemma A.32. Let -→ F 0 [M] -→ F 1 , -→ σ 0 M -→ σ 1 , E 0 M C E 1 . • If x -→ σ 0 = y, then there exists t 1 such that -→ F 1 [ E 1 [x v 1 ] ] -→ σ 1 ⇓ v t 1 and -→ F 0 [ E 0 [x v 0 ] ] -→ σ 0 R NFη t 1 . • If x -→ σ 0 is a λ-abstraction, then there exist t 0 , t 1 such that -→ F 0 [ E 0 [x v 0 ] ] -→ σ 0 → v t 0 , -→ F 1 [ E 1 [x v 1 ] ] -→ σ 1 → * v t 1 , and t 0 R t 1 .
Proof. There is a sequence of variables y 0 . . . y m such that y

0 = x, -→ σ 0 (y i ) = y i+1 for 0 ≤ i ≤ m -1, -→ σ 0 (y m ) = v, v is a λ-abstraction or v is a variable not in the domain of -→ σ 0 . For 0 ≤ i ≤ m, we write -→ σ 1 (y i ) = v i 1 ,

and we have y

i M NFη v i-1 1 for 1 ≤ i ≤ m, and v M NFη v m 1 . Let z 1 , . . . , z m , k 1 .
. . k m be fresh variables. By Lemma A.28, there exist contexts E 0 1 , . . . , E m 1 ,

-→ F 1 = F 1 1 , . . . , F 1 m , and values v 1 0 , . . . , v 1 m such that -→ F 1 [ E 1 [x v 1 ] ] -→ σ 1 → * v -→ F 1 [ -→ F 1 [ E m 1 [y m v 1 m ] ]]{E m-1 1 /k m }{v 1 m-1 /z m } . . . {E 0 1 /k 1 }{v 1 0 /z 1 } -→ σ 1 where for 1 ≤ i ≤ m, [M] F 1 i , z i M NFη v 1 i , k i M C E i 1 and also v 1 0 = v 1 , E 0 1 = E 1 . We now distinguish cases based on v. If v is a variable y, then -→ F 0 [ E 0 [x v 0 ] ] -→ σ 0 is
(v m 1 z m+1 ) ⇓ v F 1 m+1 [ E m+1 1 [y v 1 m+1 ] ], z m+1 M NFη v 1 m+1 , [M] F 1 m+1 , k m+1 M C E m+1 1 . As a result, we have -→ F 1 [ E 1 [x v 1 ] ] -→ σ 1 → * v -→ F 1 [ -→ F 1 [F 1 m+1 [ E m+1 1 [y v 1 m+1 ] ]]]{E m 1 /k m+1 }{v 1 m /z m+1 } {E m-1 1 /k m }{v 1 m-1 /z m } . . . {E 0 1 /k 1 }{v 1 0 /z 1 } -→ σ 1
We can also write

-→ F 0 [ E 0 [x v 0 ] ] -→ σ 0 as -→ F 0 [ - → [ k m+1 (y z m+1 ) ]]{k m /k m+1 }{z m /z m+1 } {k m-1 /k m }{z m-1 /z m } . . . {E 0 /k 1 }{v 0 /z 1 } -→ σ 0
The resulting open stuck terms are related by R , as wished.

If v is a λ-abstraction λy.t, then -→ F 0 [ E 0 [x v 0 ] ] -→ σ 0 is able to reduce. From λy.t M NFη v m 1 , we deduce t M v m 1
y (assuming y fresh enough, which is always possible with α-conversion), which in turn implies k m+1 t M k m+1 (v m 1 y) for any fresh k m+1 (using Lemma A.26). As a result, we have

-→ F 1 [ E 1 [x v 1 ] ] -→ σ 1 → * v -→ F 1 [ -→ F 1 [ k m+1 (v m 1 y) ]]{E m 1 /k m+1 }{v 1 m /y} {E m-1 1 /k m }{v 1 m-1 /z m } . . . {E 0 1 /k 1 }{v 1 0 /z 1 } -→ σ 1 RR n°9096
and we also have

-→ F 0 [ E 0 [x v 0 ] ] -→ σ 0 → v -→ F 0 [ - → [ k m+1 t ]]{k m /k m+1 }{z m /y} {k m-1 /k m }{z m-1 /z m } . . . {E 0 /k 1 }{v 0 /z 1 } -→ σ 0
The two resulting terms are related by R , as required.

Lemma A.33. R is a delimited normal-form bisimulation.

Proof. By case analysis on the terms in R . For terms of the form v

0 -→ σ 0 , v 1 -→ σ 1 , we have to prove that k v 0 -→ σ 0 R k v 1 -→ σ 1 holds for a fresh k. By definition, we have v 0 M v 1 , which implies k v 0 M k v 1 . We obtain delimited terms, therefore we have k v 0 -→ σ 0 R k v 1 -→ σ 1 , which is the same as k v 0 -→ σ 0 R k v 1 -→ σ 1 , as wished.
We now consider terms of the form

-→ F 0 [t 0 ] -→ σ 0 , -→ F 1 [t 1 ] -→ σ 1 .
Note that by definition of R and [M], these terms are delimited. We distinguish cases based on t 0 .

Case: t 0 → v t 0 , with t 0 delimited. Then -→ F 0 [t 0 ] -→ σ 0 → v -→ F 0 [t 0 ] -→ σ 0 . Because → v ⊆ M, we have -→ F 0 [t 0 ] -→ σ 0 R -→ F 1 [t 1 ] -→ σ 1 , as required. Case: t 0 → v v 0 . Then -→ F 0 [t 0 ] -→ σ 0 → v -→ F 0 [v 0 ] -→ σ 0 .
By bisimilarity, there exists v 1 such that t 1 ⇓ v v 1 and v 0 M NFη v 1 . We can conclude by Lemma A.31.

Case: t 0 = F 0 [x v 0 ] . Since t 0 M t 1 , there exist F 1 , v 1 such that t 1 ⇓ v F 1 [x v 1 ], F 0 M C F 1 and v 0 M NFη v 1 .
We know that F 1 is delimited, as (part of) the result of the evaluation of the delimited term t 1 . The relation

F 0 M C F 1 implies that F 0 = F 0 [ E 0 ], F 1 = F 1 [ E 1 ], F 0 [M] F 1 , and E 0 M C E 1 .
We can conclude by Lemma A.32.

Case: t 0 = F 0 [ k v 0 ]. Since t 0 M t 1 , there exists F 1 , v 1 , such that t 1 ⇓ v F 1 [ k v 1 ], F 0 [ ] M C F 1 [
] and v 0 M NFη v 1 . Note that we know there is a reset surrounding k v 1 because t 1 is well formed w.r.t. k and by applying Proposition 4.22. Because t 0 , t 1 are delimited, and

F 0 [ ] M C F 1 [ ], we also have F 0 [M] F 1 .
There is a sequence of variables k

0 . . . k m such that k 0 = k, -→ σ 0 (k i ) = k i+1 for 0 ≤ i ≤ m -1 and -→ σ 0 (k i ) = E so that if E = k , k is not in the domain of -→ σ 0 . For 0 ≤ i ≤ m, we write -→ σ 1 (k i ) = E i 1 , and we have k i M C E i-1 1 for 1 ≤ i ≤ m, and E M C E m 1 . Let x 1 .
. . x m be fresh variables. By Lemma A.30, there exist -→

F 1 = F 1 1 . . . F 1 m , v 0 1 . . . v m 1 such that -→ F 1 [t 1 ] -→ σ 1 → * v -→ F 1 [F 1 [ -→ F 1 [ k m v m 1 ]]]{v m-1 1 /x m } . . . {v 1 1 /x 2 }{v 0 1 /x 1 } -→ σ 1 with for 1 ≤ i ≤ m, [M] F 1 i , x i M NFη v i 1 , and v 0 1 = v 1 .
We distinguish cases based on E [x] , where x is a fresh variable.

Theorem A.34. The relation M is a congruence.

Proof. Let t 0 M t 1 . We first prove compatibility w.r.t. application and reset. For a fresh k, we have k t 0 M k t 1 by Lemma A.26, which in turn implies k t 0 σ 0 M k t 1 σ 1 for σ 0 M σ 1 according to Lemma A. [START_REF] Hieb | [END_REF]. By taking σ 0 = σ 1 = { /k}, we obtain t 0 M t 1 , which gives us compatibility w.r.t. reset. By taking σ 0 = σ 1 = {k ( t)/k} where k fresh, we obtain k (t 0 t) M k (t 1 t) , which implies t 0 t M t 1 t.

To prove that we also have t t 0 M t t 1 , let k , x be fresh variables. By taking σ 0 = σ 1 = {k (x )/k}, we obtain k (x t 0 ) M k (x t 1 ) , which implies {k ( t 0 )/k } [M] {k ( t 1 )/k } for all k . We therefore have k t {k ( t 0 )/k } M k t {k ( t 1 )/k } (k fresh), i.e., k (t t 0 ) M k (t t 1 ) , which means that t t 0 M t t 1 holds, as wished.

We now prove compatibility w.r.

⇓ v v 1 and v 0 R NF v 1 .
Proof. By induction on the derivation of v 0 R t 1 . If v 0 = t 1 , then the result is direct. The result is also direct in the case of compatibility w.r.t. λ-abstraction.

If v 0 R t 1 , then k v 0 R k t 1 holds for a fresh k, and there exists t 1 such

that k t 1 ⇓ v t 1 and k v 0 R NF t 1 . But t 1 is delimited, so the only possibility is t 1 = k v 1 for some v 1 with t 1 ⇓ v v 1 and v 0 R NF v 1 , hence the result holds. The cases v 0 = v 0 {v 0 /x}, t 1 = t 1 {v 1 /x} with v 0 R t 1 , v 0 R NF v 1 , and
v 0 = v 0 {E 0 /k}, t 1 = t 1 {E 1 /k} with v 0 R t 1 , E 0 R C E 1 are straightforward by induction. If t 1 = E 1 [t 1 ] with v 0 R t 1 and x R E 1 [x]
, then in fact E 1 = and t 1 is delimited, otherwise t 1 would not be delimited. Therefore, by the induction hypothesis, there exists v 1 such that t Proof. As in the proof of Lemma A.21, we proceed by induction on the number of steps m it takes for t 0 or k t 0 to reduce to a normal form, and on the derivation of t 0 R t 1 , ordered lexicographically. We only detail the differences with the original proof of Lemma A.21.

1 ⇓ v v 1 with v 0 R NF v 1 . As a result, we have t 1 ⇓ v v 1 with v 0 R NF v 1 , as wished. Lemma A.36. If R is a bisimulation up to context, F 0 [x] R F 1 [x] for a fresh x, t 0 R NF t 1 ,
We suppose first that m = 0. The cases t 0 R t 1 and t 0 = t 1 are immediate. We detail the other cases.

Case: t 0 {v 0 /x} R t 1 {v 1 /x} with t 0 R t 1 and v 0 R NF v 1 .
The terms t 0 {v 0 /x} or k t 0 {v 0 /x} (k fresh) are normal forms if t 0 or k t 0 are themselves normal forms. We can conclude by using the induction hypothesis on t 0 R t 1 , and then apply the substitutions on the resulting normal forms.

Case: t 0 {E 0 /k} R t 1 {E 1 /k} with t 0 R t 1 and E 0 [x] R E 1 [x] (x fresh

Case

: F 0 [t 0 ] R F 1 [t 1 ] with F 0 R C F 1 and t 0 R t 1 . The term F 0 [t 0 ] is a normal form if t 0 is value v 0 and F 0 =
or if t 0 is an open stuck term. For the former case, we know by induction that for any fresh k, there exist

F 1 , v 1 such that k t 1 ⇓ v F 1 [ k v 1 ], R C F 1 [ ], and v 0 R NF v 1 . Let k be a fresh variable. From R C F 1 , we deduce that F 1 is a pure context E 1 , and for a fresh x, we have k E 1 [x] ⇓ v F 1 [ k x ] with R C F 1 [
] (by using the induction hypothesis). Consequently we have the transitions

k E 1 [t 1 ] → * v F 1 {k E 1 /k}[ k E 1 [v 1 {k E 1 /k}] ] → * v F 1 {k E 1 /k}[F 1 {v 1 {k E 1 /k}/x}[ k v 1 {k E 1 /k} ]] From v 0 R NF v 1 , we deduce v 0 R NF v 1 {k E 1 /
= F 0 [ E 0 ], then F 1 = F 1 [ E 1 ] with F 0 [z] R F 1 [z] and E 0 [z] R E 1 [z]
for a fresh z. We assume F 0 , F 1 are both delimited, the case where they are not is similar (just replace F 0 , F 1 with k F 0 , k F 1 for a fresh k ). The evaluation k t 1 ⇓ v t 1 implies F 1 [t 1 ] ⇓ v F 1 [t 1 {E 1 /k}], and

k t 0 R NF t 1 implies F 0 [ E 0 [t 0 ] ] R NF F 1 [t 1 {E 1 /
k}], hence the result holds.

Case: F 0 [t 0 ] R F 1 [t 1 ] with F 0 [x] R F 1 [x] (x
fresh), t 0 R t 1 , and t 0 , t 1 delimited. The term F 0 [t 0 ] is a normal form if t 0 is an open stuck term. We assume F 0 [x] and F 1 [x] are both delimited, the case where they are not is treated similarly (by replacing F 0 , F 1 with k F 0 , k F 1 for a fresh k). The terms t 0 and t 1 are both delimited, so by the induction hypothesis, there exists an open term t 1 such that t 1 ⇓ v t 1 and t 0 R NF t 1 . Consequently, we have

F 1 [t 1 ] ⇓ v F 1 [t 1 ] with F 0 [t 0 ] R NF F 1 [t 1
] by Lemma A.36, hence the result holds.

We now suppose m > 0. The cases t 0 R t 1 and t 0 = t 1 are still straightforward.

Case: Sk.t 0 R Sk.t 1 with t 0 R t 1 . Let k be a fresh variable. Then k Sk.t 0 → v t 0 {λx. k x /k} ⇓ v t 0 , and k Sk.t 1 → v t 1 {λx. k x /k} . The two terms t 0 {λx. k x /k} and t 1 {λx. k x /k} are related by R, and the former evaluates to a normal form in m -1 steps or less, therefore we can conclude by using the induction hypothesis.

Case: t 0 {v 0 /x} R t 1 {v 1 /x} with t 0 R t 1 and v 0 R NF v 1 . The reasoning is the same as in the corresponding case of the proof of Lemma A.21. If t 0 and t 1 are not both delimited, the reasoning is applied to k t 0 , k t 1 (k fresh) instead of t 0 , t 1 .

Case: t 0 {E 0 /k} R t 1 {E 1 /k} with t 0 R t 1 and E 0 [x] R E 1 [x] (x fresh). The reasoning is the same as in the corresponding case of the proof of Lemma A.23 (again, eventually applied to k t 0 , k t 1 with k fresh instead of t 0 , t 1 ).

Case: F 0 [t 0 ] R F 1 [t 1 ] with F 0 [x] R F 1 [x] (x
fresh), t 0 R t 1 , and t 0 , t 1 delimited. We assume F 0 [x] and F 1 [x] are both delimited, the proof is the same if they are not (by replacing F 0 and F 1 with k F 0 and k F 1 ).

Because F 0 [t 0 ] evaluates to a normal form t 0 , we also have t 0 ⇓ v t 0 . If t 0 is an open stuck term, then by the induction hypothesis, there exists an open t 0 (A • ) c t 1 , as required.

If t 0 A • t 1 , then we distinguish several cases, depending on the outermost operator.

Suppose t 0 = λx.s 0 and t 1 = λx.s 1 with s 0 Suppose t 0 = t 1 0 t 2 0 and t 1 = t 1 1 t 2 1 with t 1 0 (A • ) c t 1 1 and t 2 0 (A • ) c t 2 1 . We have two possible cases. First, suppose t 0 E -→ t 0 , where t 1 0 We now prove the bisimulation property (up to environment) for elements in X 1 . Let F 0 [t 0 ] X Ė v F 1 [t 1 ], so that t 0 Y E t 1 and F 0 Ë F 1 . If F 0 [t 0 ] and F 1 [t 1 ] are not both delimited terms, then for all E 0 Ë E 1 , we have Proof. Similar to the proof of Lemma C.6.

E [ t 2 0 ] -----→ t 0 . Let E such that E (A • ) c E ; then E [ t 2 0 ] (A • ) c E [ t 2
E 0 [F 0 [t 0 ]] X Ė v E 1 [F 1 [t 1 ]] ,
→ v F 0 [p 0 ], p 1 → v F 1 [p 1 ], and F 0 [p 0 ] X Ė v F 1 [p 1 ] hold, as wished. If E 0 [t 0 ] → v v 0 , then there exists v 1 such that E 1 [t 1 ] → * v v 1 and E def = {(v 0 , v 1 )} ∪ E ⊆ Y. Therefore we have p 0 → v F 0 [v 0 ], p 1 → v F 1 [v 1 ], and F 0 [v 0 ] X Ė v F 1 [v 1 ],
Lemma C.14. If p 0 Ḟ p 1 then we have one of the following cases:

• p 0 F p 1 ;

• p 0 = v 0 ;

• p 0 = F 0 [ E 0 [t 0 ] ], p 1 = F 1 [ E 1 [t 1 ] ] , F 0 F F 1 , E 0 F E 1
, t 0 F t 1 and t 0 → v t 0 or t 0 is stuck;

• p 0 = F 0 [ E 0 [r 0 ] ], p 1 = F 1 [ E 1 [t 1 ] ] , F 0 F F 1 , E 0 F E 1 , r 0 Ḟ t 1 but r 0 F t 1 .
Proof. We prove a more general result on t 0 Ḟ t 1 . We have either

• t 0 F t 1 ;

• t 0 = v 0 ; RR n°9096 such that t 1 → * v v 1 and v 0 Ḟ v 1 . Then we have p 0 → v F 0 [ E 0 [v 0 ] ] and

p 1 → * v F 1 [ E 1 [v 1 ] ] with F 0 [ E 0 [v 0 ] ] Ḟ F 1 [ E 1 [v 1 ]
], hence the result holds. If r 0 = v 1 0 v 2 0 , then t 1 = t Proof. To make the proof easier to follow, we introduce some notations. We write -→ • for a sequence of entities (e.g., -→ E for a sequence of contexts). We write E for E [(λx.Sk.t 0 ) ] and E for (λx.t 0 {λy. E [y] /k}) , so the problem becomes relating E [t 1 ] and E [t 1 ] .

Next, given a sequence E 0 . . . E i of contexts such that fv(E j ) ⊆ {k 0 . . . k j-1 } for all 0 ≤ j ≤ i, we inductively define families of substitutions σ

- → E 0 . . . σ - → E i , δ - → E 0 . . . δ - → E i as follows: σ - → E 0 = •{λy. E [E 0 [y]] /k 0 } δ - → E 0 = •{λy. E [E 0 [y]] /k 0 } σ - → E j = •{λy. E [E j σ - → E 0 . . . σ - → E j-1 [y]] /k j } if j > 0 δ - → E j = •{λy. E [E j δ - → E 0 . . . δ - → E j-1 [y]] /k j } if j > 0
s t, - → F 0 = F 0 [ E [t] ] s t, - → F j = F j [ E [s t, - → F j-1 ] ] if j > 0 u t, - → F 0 = F 0 [ E [t] ] u t, - → F 0 = F j [ E [u t, - → F j-1 ] ] if j > 0
Note that the term we want to relate are s t1, for some E , -→ E . With some renumbering and rewriting, we have E 0 [tσ

- → E 0 . . . σ - → E i ] = E [t] σ - → E , -→ E 0 . . . σ - → E , -→ E i+j+1 and E 1 [tσ - → E 0 . . . σ - → E i ] = E [t] δ - → E , -→ E 0 . . . δ - → E ,
-→ E i+j+1 : the two terms are in X , as wished.

- → E i = F σ - → E 0 . . . σ - → E i [λy. E [E j σ - → E 0 . . . σ - → E j-1 [y]] vσ - → E 0 . . . σ - → E i ] t δ - → E 0 . . . δ - → E i = F δ - → E 0 . . . δ - → E i [λy. E [E j δ - → E 0 . . . δ - → E j-1 [y]] vδ - → E 0 . . . δ - → E i ]
Reducing the β-redex in both terms, we obtain t σ

- → E 0 . . . σ - → E i → v F σ - → E 0 . . . σ - → E i [ E [E j σ - → E 0 . . . σ - → E j-1 [vσ - → E 0 . . . σ - → E i ]] ] t δ - → E 0 . . . δ - → E i → v F δ - → E 0 . . . δ - → E i [ E [E j δ - → E 0 . . . δ - → E j-1 [vδ - → E 0 . . . δ - → E i ]] ]
The resulting terms can be written s t ,F

→ F i σ -→ E 0 . . . σ -→ E j → v s F0[t ] , -→ F i-1 σ -→ E 0 . . . σ -→ E j
and we also

have u v, - → F i δ -→ E 0 . . . δ -→ E j → v u F0[t ] , -→ F i-1 δ -→ E 0 . . . δ
-→ E j , where -→ F = F 1 . . . F i (the first context F 0 is removed from the sequence). We obtain terms that are in the second set of X . In both cases, the resulting terms are in X . The reasoning is the same if t = k l for some 0 ≤ l ≤ j.

If t = E j+1 [Sk j+1 .t ], then

s t, - → F 0 σ -→ E 0 . . . σ -→ E j = F 0 [ E [E j+1 [Sk j+1 .t ]] ] σ -→ E 0 . . . σ -→ E j → v F 0 [ t ] σ -→ E 0 . . . σ -→ E j σ -→ E ,E j+1 j+1 RR n°9096 and u t, - → F 0 δ -→ E 0 . . . δ -→ E j = F 0 [ E [E j+1 [Sk j+1 .t ]] ] δ -→ E 0 . . . δ -→ E j → v F 0 [ t ] δ -→ E 0 . . . δ -→ E j δ -→ E ,
→ F i σ -→ E 0 . . . σ -→ E j → v s F0[t ] , -→ F i-1 σ -→ E 0 . . . σ -→ E j+1 and also u t, - → F i δ -→ E 0 . . . δ -→ E j → v u F0[t ] , -→ F i-1 δ -→ E 0 . . . δ -→ E j+1
, where -→ F = F 1 . . . F i , so the resulting terms are in X E . If t = F i+1 [k l v] (with 1 ≤ l ≤ j), then

s t, - → F 0 σ -→ E 0 . . . σ -→ E j = F 0 [ E [F i+1 [(λy. E [E l [y]] ) v]] ] σ -→ E 0 . . . σ -→ E j → v F 0 [ E [F i+1 [ E [E l [v]] ]] ] σ -→ E 0 . . . σ -→ E j = s E l [v], -→ F 1 σ -→ E 0 . . . σ -→ E j and u t, - → F 0 δ -→ E 0 . . . δ -→ E j = F 0 [ E [F i+1 [(λy. E [E l [y]] ) v]] ] δ -→ E 0 . . . δ -→ E j → v F 0 [ E [F i+1 [ E [E l [v]] ]] ] δ -→ E 0 . . . δ -→ E j = u E l [v], -→ F 1 δ -→ E 0 . . . δ -→ E j

with

-→ F = F i+1 , F 0 , . . . F i , so the resulting terms are in X E . If i > 0, then

s t, - → F 0 σ -→ E 0 . . . σ -→ E j → v s E l [v],
-→ F i+1 σ -→ E 0 . . . σ -→ E j , and we have also u t, -

→ F 0 δ -→ E i . . . δ -→ E j → v u E l [v],
-→ F i+1 δ -→ E 0 . . . δ -→ E j , so the resulting terms are in X E , as required.

def=

  for a defining equality, i.e., m def = e means that m is defined as the expression e. Given a metavariable m, we write -→ m for a sequence of entities denoted by m. Given a binary relation R, we write m R m RR n°9096

Example 2 . 2 (

 22 fixed-point combinators). We recall the definition of Turing's and Curry's fixed-point combinators. Let θ def = λxy.y (λz.x x y z) and δ x def = λy.x(λz.yyz); then Θ def = θθ is Turing's call-by-value fixed-point combinator,

Figure 2 :

 2 Figure 2: Kameyama and Hasegawa's axiomatization of λ S

Theorem 4 . 5 .

 45 The relation N is a congruence.

Example 4 .

 4 10 (fixed-point combinators). The relation R def = {(Θ, Θ S ), (Θ, (λx. θ x ) (λx. θ x ))} is a bisimulation up to context. Indeed, we remind that Θ ⇓ v λy.y (λz.Θ y z) def = v 0 , and

Proposition 4 . 18 .

 418 Let i def = λx.x. We have Sk.i C (Sk.i)Ω, but Sk.i N (Sk.i)Ω.

Theorem 4 . 23 .

 423 The relation R is a congruence. Theorem 4.24. We have R ⊂ C.

  The two terms are control stuck terms, therefore, we have to prove that t{λx. k E [x] /k} R t{λx. (λy. k y ) E [x] /k} holds for a fresh k . We know that k E [x] N (λy. k y ) E [x] holds by Example 4.17. Consequently, we have k E [x] R (λy. k y ) E [x] by Proposition 4.20. We can then conclude by congruence of R.

  bisimulation up to context if both R and R -1 are refined normal-form simulations up to context. We can adapt the proof of Proposition 4.13 to prove the soundness of refined bisimulation up to context w.r.t. R. Proposition 4.27. If R is a refined bisimulation up to context, then R is a refined non-η bisimulation.

Proposition 4 . 34 .

 434 We have N ⊆ M and R ⊆ M.

Proposition 4 . 38 .

 438 We have Ω M Sk.Ω. The relation {(Ω, Sk.Ω), ( k Ω , k Sk.Ω )} (where k = k) is a delimited bisimulation. Proposition 4.38 does not hold with C because Ω is not stuck.

Figure 6 :

 6 Figure 6: Labeled Transition System

  τ -→ t by letting t capture the empty context, i.e., by considering the transition t -→ t . Example 5.1. With the same notations as in Example 2.1, we illustrate how the LTS handles capture by considering the transition from (i Sk.ω) (ω ω) .

Lemma 5 . 2 .

 52 If t E -→ t , then there exist E , k, and s such that t = E [Sk.s] and t= s{λx. E [E [x]] /k} .The proof is direct by induction on t E -→ t . From this lemma, we can deduce the correspondence between τ -→ and → v , and between α -→ (for α = τ ) and the observable actions of the language.

Theorem 5 . 14 .

 514 The relation A is a congruence.As a corollary, A is sound w.r.t. contextual equivalence.Theorem 5.15. We have A ⊆ C.

  1 and, therefore, we have t 0 D t 1 by Theorem 5.15 and transitivity of D. As a result, the relations C, D, and A coincide, which means that A is complete w.r.t. C Corollary 5.17. We have C = D = A. Indeed, we have D ⊆ A (Theorem 5.16), A ⊆ C (Theorem 5.15), and C ⊆ D (by definition).

Figure 7 :

 7 Figure 7: Term and context generating closures

Example 6 . 8 (

 68 Turing's combinator). Proving that Turing's combinator Θ is bisimilar to its variant Θ S def = θ Sk.k k using the basic definition of environmental bisimulation is harder than with applicative bisimulation (Example 5.9). We remind that Θ ⇓ v λy.y (λz.θ θ y z) def = v 0 , and Θ S ⇓ v λy.y (λz.(λx. θ x ) (λx. θ x ) y z) def = v 1 .

Figure 8 :

 8 Figure 8: Relationships between the equivalences of λ S

and v 0 R NF v 1 ,F 1

 11 we deduce F 0 {v 0 /x} R C {v 1 /x} (*) and v 0 {v 0 /x} R NF v 1 {v 1 /x} (**) by Lemmas A.14 and A.15. We now distinguish cases, based on the kinds of the values v 0 and v 1 .• If v 0 and v 1 are variables, then they are equal since we havev 0 R NF v 1 . Let y = v 0 = v 1 . Then we have t 0 {v 0 /x} ⇓ v F 0 {y/x}[y v 0 {y/x}] t 1 {v 1 /x} ⇓ v F 1 {y/x}[y v 1 {y/x}]We obtain two open stuck terms, and we have F 0 {y/x} R C F 1 {y/x} and v 0 {y/x} R NF v 1 {y/x} according to (*) and (**), hence the required result holds.

1 τ= ⇒ v 1 , 1 τ= 1 τ= ⇒ v 1 , we can deduce t 1 τ= 1 τ= ⇒ v 1 1 τ= 1 E 1 E 1 E= ⇒ s 1 , hence we have t 1 τ= ⇒ v 1 s 1 E= 1 E= ⇒ s 1 ,

 11111111111111111 λx.s 0 (A • ) c λx.s 1 , and v 0 (A • ) c v 1 . From t 1 ⇒ λx.s 1 and t 2 ⇒ s 1 {v 1 /x}, and from λx.s 0 (A• ) c λx.s 1 and v 0 (A • ) c v 1 , we have s 0 {v 0 /x} A • s 1 {v 1 /x} by Lemma B.[START_REF] Aristizábal | Environmental Bisimulations for Delimited-Control Operators with Dynamic Prompt Generation[END_REF]. Hence, we have the required result.Suppose t 0 = v 0 s 0 and t 1 = t 1 1 s 1 with v 0 (A • ) c t 1 1 and s 0 (A • ) c s 1 . By Lemma B.4, there exists v 1 such that t 1 and v 0 (A • ) c v 1 . We have two possible cases; in the first one, we have t 0 τ -→ v 0 s 0 , where s 0 τ -→ s 0 . By the induction hypothesis, there exists s 1 such that s 1 τ = ⇒ s 1 and s 0 (A • ) c s 1 . Therefore we have t ⇒ v 1 s 1 , and because (A • ) c is compatible, we have v 0 s 0 (A • ) c v 1 s 1 , hence the result holds. In the second case, we have t 0 E -→ s 0 , where s 0E [v0 ] -----→ s 0 . Let E such that E (A • ) c E ; then E [v 0 ] (A • ) c E [v 1 ] holds.Therefore, by the induction hypothesis, there exists s 1 such that s [v1 ] = ==== ⇒ s 1 and s 0 (A • ) c s 1 . The transition s [v1 ]= ==== ⇒ s 1 implies v 1 s ⇒ s 1 , i.e., t Because s 0 (A • ) c s 1 holds, we have the required result.

  Finally, given a term t and a sequence of contexts F 0 . . . F i , we inductively define families of terms s t,

0 and u t1, 0 .i

 0 We let E ranges over environments of the form{(vσ fv(v) ⊆ {k 0 . . . k i }}∪ {(k j σ -→ E j , k j δ -→ E j )}. We prove that the relation X = {(E, tσ ) | fv(t) ⊆ {k 0 . . . k i }}∪ {(E, s t,j ) | fv(t) ∪ fv( -→ F ) ⊆ {k 0 . . . k j }} ∪ {E}is a delimited bisimulation. Let tσ where t is not delimited. Let E 0 Ë E 1 ; by definition of E, we have E 0 = E σ

  t = E j [v], therefore we obtain terms in X E . Let s t, can check that the reductions from terms of the form s t, the transitions from these two terms come from t. We have several cases for t. If t → v t , then we still haves t , t = v, then s v, j = F 0 [ E [v] ] δ -→ E 0 . . . δ -→ E j . It is easy to check that E [v] and E [v]reduce to the same term t 0 {λy. E [y] /k}{v/x} , written t . Then we have s v, two resulting terms are in the first set of X . If i > 0, one can check that s v, -

  are in X E . If i > 0, then one can check that s t, -

Finally, let

  λx.t 0 E λx.t 1 and v 0 Ė v 1 . It is easy to check that by definition of E, the two terms t 0 {v 0 /x} and t 1 {v 1 /x} are of the form t σ

  , then t cannot diverge or cannot reduce to an open stuck term (otherwise, t would also diverge or reduce to an open stuck term). Hence, we have t⇓ v v , which entails t → * v v → v v , which in turn implies v = v because normal forms are unique. Consequently, we have t ⇓ v v iff t ⇓ v v, and v N NFη v holds. If t ⇓ v F [x v],then by Proposition 2.9, there exists F such that F = F . Therefore, we have t⇓ v F [x v] . We have v N NFηv, and we have to prove that F R C F holds to conclude. If F is a pure context E , then we have to prove E [y] R E [y] and y R y for a fresh y, which are both true because N ⊆ R. If F = F [ E ], then given a fresh y, we have to prove F [y] R F [y] (clear by the definition of R), and E

  t 1 Definition 4.9. A relation R on terms is a normal-form simulation up to context if t 0 R t 1 and t 0 ⇓ v t 0 implies that there exists t 1 such that t 1 ⇓ v t 1 and

	Sk.t 0 R Sk.t 1
	Figure 4: Substitutive, reflexive, and context closure of a relation R
	t 0 R and R -1 are normal-form simulations up to context. NF t 1 . A relation R is a normal-form bisimulation up to context if both R

  1 ) by Sk.t 0 (respectively Sk.t 1 ), but with an additional k . Indeed, if E 0 [Sk.t 0 ] is R t 1 and t 0 ⇓ v t 0 implies that there exists t 1 such that t 1 ⇓ v t 1 and t 0 R RNFη t 1 . A relation R is a refined normal-form bisimulation if both R and R -1 are refined normal-form simulations. Refined normal-form bisimilarity, written R, is the largest refined normal-form bisimulation. Indeed, for control stuck terms, if t 0 N t 1 and t 0

	put into a context E , then Sk.t 0 captures a context bigger than E 0 , namely
	E [E 0 ]. We take such possibility into account by introducing the variable k in the definition of R RNFη , which represents the context that can be captured
	beyond E 0 and E 1 . Such a technique was introduced by Felleisen et al. to define
	a syntactic theory of control with local reduction rules [24, 25].
	Definition 4.19. A relation R on terms is a refined normal-form simulation
	if t 0 Refined bisimilarity contains regular bisimilarity.
	Proposition 4.20. We have N ⊂ R.
	RR n°9096

  and we have t R NFη t , as required. If t 1 reduces to an open stuck term, then t 1 ⇓ v F [y v] by Proposition 2.9. In this case, we have (λx.t 0

  If t 1 → v t 1 , then we have k ((λx.Sk.t 0 ) t 1 ) → v k ((λx.Sk.t 0 ) t 1 ) and (λx.t 0 {λy. k y /k}) t 1 → v (λx.t 0 {λy. k y /k}) t 1 , therefore, we obtain two terms in R. • If t 1 = v 1 , then we have k ((λx.Sk.t 0 ) v 1 ) → 2 v t 0 {λy. k y /k}{v 1 /x} and (λx.t 0 {λy. k y /k}) t 1 → v t 0 {λy. k y /k}{v 1 /x} ; we obtain two identical terms.

This equivalence does not hold with C, because the term on the right is stuck, but the term on the left may not evaluate to a stuck term (if t 1 does not terminate). A direct proof of Proposition 4.41 (which does not rely on ≡) is given below, as a use case for bisimulation up to context.

Proof. We want to relate k ((λx.Sk.t 0 ) t 1 ) with k Sk.((λx.t 0 ) t 1 ) for a fresh k . We have k Sk.((λx.t 0 ) t 1 ) → v (λx.t 0 {λy. k y /k}) t 1 , therefore, we prove that R def = {( k ((λx.Sk.t 0 ) t 1 ) , (λx.t 0 {λy. k y /k}) t 1 ) | (t 0 , t 1 ) ∈ T 2 , k / ∈ fv(t 1 ), {k , y} ∩ fv(t 0 , t 1 ) = ∅} ∪ M is a small-step bisimulation up to context, by case analysis on t 1 .

•

  then t is a value, and t v For the first result, the only difficult transition to check is the capture by shift. If t

τ -→ t . Proof. τ -→ t with t -→ t , then by Lemma 5.2, there exists E , s such that t = E [Sk.s] and t = s{λx. E [x] /k} ; therefore, E [Sk.s] → v RR n°9096

  and we have t R t , as wished. The structure of the proof is simpler than in Example 4.3 because we do not have to consider open stuck terms.

  we have to study the behavior of t{(λz.θ θ v z)/x}, and t{(λz.(λx. θ x ) (λx. θ x ) v z)/x}. A way to proceed is by case analysis on t, the interesting case being t = F [x v ]. The resulting applicative bisimulation one can write to relate Θ and Θ S is much more complex than the normal-form bisimulation of Example 4.4.Remark 5.10. Applicative simulation can be formulated in a more classic, but equivalent, way (without labeled transitions), as follows. A relation R on closed terms is an applicative simulation if t 0 R t 1 implies:• if t 0 → v t 0 ,then there exists t 1 such that t 1 → * v t 1 and t 0 R t 1 ; • if t 0 is a value λx.t 0 , then there exists t 1 such that t 1 → * v λx.t 1 , and for all closed v, we have t 0 {v/x} R t 1 {v/x};

  bisimilarity definition, and similarly with C [t 0 ] ⇓ v t 0 , where t 0 is control stuck.

  . We prove that R ⊆ {y}} ∪ A is a bisimulation. To this end, we have to check that λx.(λy.t) x t{v 0 /y}, i.e., that (λy.t) v 0 R t{v 0 /y} holds for all v 0 . Proposition 5.21 (S • axiom). We have Sk. t A Sk.t. t{λx. E [x] /k} and Sk.t E -→ t{λx. E [x] /k} for all E . We obtain terms of the form t and t , and we have proved in Example 5.8 that t A t holds for all t . Proposition 5.22 ( • lift axiom). We have (λx.t 0 ) t 1 A (λx. t 0 ) t 1 . Proof. A transition (λx.t 0 ) t 1

			v0 -→ (λy.t) v 0
	is matched by λy.t
	We have (λy.t) v 0	τ -→ t{v 0 /y}, and because	τ -→ ⊆ A ⊆ R, we have the required
	result.
	Proof. We have Sk. t
		α

def = {(λx.(λy.t) x, λy.t) | t ∈ T , fv(t) v0 -→ E -→

  so we have to consider environments E built out of pairs of values of the form (v, v). Then, testing such E, suppose we take λx.t E λx.t and some arguments v 0 Ė v 1 , and we need to relate t{v 0 /x} with t{v 1 /x}. Since the terms related by E are the same, we have in fact v 0 = v 1 , so we have to relate t{v 0 /x} with itself, hence the second set in the definition of the bisimulation.

  RR n°9096(c) if t 0 is a value, then there exist v 1 and E ∈ X such that t 1 ⇓ v v 1 and E ∪ {(t 0 , t 1 )} ⊆ E ; (d) the converse of the above conditions on t 1 ; 2. for all E ∈ X , if λx.t 0 E λx.t 1 and v 0 Ė v 1 , then there exists E such that E ⊆ E and t 0 {v 0 /x} X E t 1 {v 1 /x}.

	Proposition 6.10. If X is an environmental bisimulation up to environment,
	then X ⊆ ≈.

for a fresh x;

  as required. Let λx.t 0 C λx.t 1 and v 0 Ċ v v 1 . By congruence of C, we have v 0 C v 1 , and

also (λx.t 0 ) v 0 C (λx.t 1 ) v 1 . Because (λx.t 0 ) v 0 → v t 0 {v 0 /x}, (λx.t 1 ) v 1 → v t 1 {v 1 /x},

and → v ⊆ E ⊆ C, we have t 0 {v 0 /x} C t 1 {v 1 /x}, i.e., t 0 {v 0 /x} X C v t 1 {v 1 /x}, as wished. RR n°9096

  X for all E . At this point, we would like to use the up-to context technique, because the subterms (λx.E [x]) E 0 [y] and E [E 0 [y]] are similar to the terms we want to relate (they can be written (λx.E [x]) t and E [t ] with t = E 0 [y]). However, we have at best t 0 {λy. E 1 [(λx.E [x]) E 0 [y]] /k} ẊE t 0 {λy. E 2 [E [E 0 [y]]] /k} (and not X E ), because t 0 can be any term, so (λx.E [x]) E 0 [y] and E [E 0

  is a bisimulation up to context up to reduction. Suppose v = λy.t, and let v 0 Ė v 1 . We have to relate v v 0 and t{v 1 /y}, but v v 0 → v t{v 0 /y} Ė t{v 1 /y}, hence the result holds. Proposition 6.24 (S • axiom). We have Sk. t E Sk.t. Sk.t), (∅, t , t ) | t ∈ T c } ∪ {∅} is a bisimulation up to context. Let Sk. t X ∅ Sk.t. We have to check that for all E , t{λx. E [x] /k} X ∅ t{λx. E [x] /k} holds (for a fresh x), but we obtain two terms of the form t and t , which are related by X ∅ by definition of X . Bisimulation up to context holds on the latter terms as pointed out in Example 6.21. Proposition 6.25 ( • lift axiom). We have (λx.t 0 ) t 1 E (λx. t 0 ) t 1 . Proof. The relation {(∅, (λx.t) t , (λx. t ) t ), ∅} is a big-step bisimulation up to context (the argument is the same as for Example 6.21).

	Proof. The relation X
	Proposition 6.26 (β

def = {(∅, Sk. t , Ω axiom). If x / ∈ fv(E ), then (λx.E [x]) t E E [t].

  then there exists p 1 such that p 1 → * v p 1 and p 0 R p 1 ; if p 0 → v λx.t 0 , then there exists t 1 such that p 1 → * v λx.t 1 , and for all v, we have t 0 {v/x} R t 1 {v/x}. A relation R is a delimited applicative bisimulation if R and R -1 are delimited applicative simulation. Delimited applicative bisimilarity B is the largest delimited applicative bisimulation.

  as wished. Let λx.t 0 P λx.t 1 and v 0 Ṗ v v 1 . By congruence of P, we have v 0 P v 1 , and also (λx.t 0 ) v 0 P (λx.t 1 ) v 1 . Because (λx.t 0 ) v 0 → v t 0 {v 0 /x}, (λx.t 1 ) v 1 → v t 1 {v 1 /x} and → v ⊆ F ⊆ P, we have t 0 {v 0 /x} P t 1 {v 1 /x}, i.e., t 0 {v 0 /x} X P v t 1 {v 1 /x}, as wished.

  Proposition 6.39 (S elim axiom). If k / ∈ fv(t), then t F Sk.k t. F is a delimited bisimulation. We have E [Sk.k t] → v (λx. E [x] ) t , and from Example 4.17, we know that (λx. E [x] ) t N E [t] holds. Because we have N⊆ C = E ⊆ F, we can deduce (λx. E [x] ) t F E [t]. Without Example 4.17, the proof would be as difficult as the proof of the next result, which is also taken from Section 4.7.

The relation {(∅, t, Sk.k t), (∅,

E [t] , E [Sk.k t] ) | t ∈ T , E ∈ PC, k / ∈ fv(

t)} ∪ Proposition 6.40. If k / ∈ fv(t 1 ), then (λx.Sk.t 0 ) t 1 F Sk.((λx.t 0 ) t 1 ). Putting the terms above in a context E , we want to relate E [(λx.Sk.t 0 ) t 1 ] with E [Sk.((λx.t 0 ) t 1 )] . The second term reduces to (λx.t 0 {λy. E [y] /k}) t 1 , so we can conclude by showing E [(λx.Sk.t 0 ) t 1 ] F (λx.t 0 {λy. E [y] /k}) t 1 . If t 1 performs successive captures, we can obtain terms like E [(λx.Sk.t 0 ) F [ E [(λx.Sk.t 0 ) t 1 ] ]] and (λx.t 0 {λy. E [y] /k}) F [ (λx.t 0 {λy. E [y] /k}) t 1 ]

  1 from refined bisimilarity (Definition 4.19): with local rules, two stuck terms Sk.t 0 and Sk.t 1 are normal-form bisimilar if t 0 and t 1 are normal-form bisimilar. The resulting bisimulation proofs are arguably more difficult than with the semantics of Section 2, as we can see with the next example. Example 7.1 (β Ω axiom). Assume we want to prove that (λx.E [x]) t N E [t] (x / ∈ fv(E )) with local rules. If t is a control stuck term Sk.t , we have to relate t {λy. k (λx.E [x]) y /k} (y, k fresh) with t -→ σ , where -→ σ are the substitutions we obtain as a result of the progressive capture of E by Sk.t . To do so, one has to see what happens when k is applied to a value v (i.e., if t = F [k v]). The proof is doable using bisimulation up to context, while the proof with the semantics of Section 2 uses only plain normal-form bisimulation (Proposition 4.31).

  and v N v 1 m . By Lemma A.8, there exist a sequence of pure contexts E 1 . . . E m , such that N C E i for 1 ≤ i ≤ m, and a sequence of values w 1 0 , . . . , w 1 m , such that z

  and t 0 {v 0 /x} and t 1 {v 1 /x} are normal forms, then t 0 {v 0 /x} R

	Proof. By case analysis on t 0 R	NF	t 1 , and using Lemma A.14 in the (open
	and control) stuck term cases.
	Lemma A.16.

NF t 1 {v 1 /x}.

  there exists a normal form t 0 such that E 0 [x] ⇓ v t 0 for a fresh x. From E 0 R , using the induction hypothesis, we deduce that there exists a normal form t 1such that E 1 [x] ⇓ v t 1 and t 0 R NF t 1 . By Proposition 2.10, we have E 0 [t 0 ] → * v t 0 {v 0 /x} and E 1 [t 1 ] → * v t 1 {v 1 /x}.So far, we have E 0

C E 1

  then for any sequences of fresh variables z 1 , . . . , z m , k 1 . . . k m , value v, and context E , there exist contexts E 0 , . . . , E m , F 1 , . . . , F m , and values v 0 , . . . , v m such that

E [y 0

  an open stuck term. Let z m+1 , k m+1 be fresh variables. From y M NFη v m

	ist contexts F 1	m+1 , E m+1 1	1 and Lemma A.27, we know there ex-, and a value v 1 m+1 such that k m+1

  t. λ-abstraction. From t 0 M t 1 , we obtain λx.t 0 M NFη λx.t 1 , which in turn implies k λx.t 0 M k λx.t 0 (k fresh), which finally gives us λx.t 0 M λx.t 1 , as required. Finally, we prove compatibility w.r.t. shift. Let k be a fresh variable. From t 0 M t 1 , we obtain t 0 {λx. k x /k} M t 1 {λx. k x /k} (x fresh). One can then prove that {(Sk.t 0 , Sk.t 1 ), ( k Sk.t 0 , k Sk.t 1 ) | k / ∈ fv(t 0 ) ∪ fv(t 1 )} ∪ M is a delimited normal-form bisimulation. A.5. Delimited bisimulation up to context Lemma A.35. If R is a delimited bisimulation up to context, v 0 R t 1 , and t 1 is delimited, then there exists v 1 such that t 1

  and t 0 , t 1 are delimited open stuck terms, then F 0 [t 0 ] R Proof. Same as for Lemma A.19, except we use Lemma A.35. Lemma A.37. Let R be a delimited bisimulation up to context. Let t 0 R t 1 . If t 0 , t 1 are not both delimited, then for all fresh k, if k t 0 ⇓ v t 0 , there exists t 1 such that k t 1 ⇓ v t 1 and t 0 R NF t 1 (and conversely if k t 1 ⇓ v t 1 ) . 2. If t 0 , t 1 are both delimited and t 0 ⇓ v t 0 , there exists t 1 such that t 1 ⇓ v t 1 and t 0 R NF t 1 (and conversely if t 1 ⇓ v t 1 ).

	1.
	NF	F 1 [t 1 ].
	RR n°9096

  ). Similar to the previous case.Case: λx.t 0 R λx.t 1 with t 0 R t 1 . We have to prove k λx.t 0 R

	NF	k λx.t 1 ,
	i.e., λx.t 0 R

NF

λx.t 1 , which is true since t 0 R t 1 .

  k} (because k is fresh w.r.t. [ ], we get z R F 1 {k E 1 /k}[z] and z R F 1 {v 1 {k E 1 /k}/x}[z] for a fresh z. The latter and Lemma A.35imply that F 1 {v 1 {k E 1 /k}/x}[z] ⇓ v z, from which we can deduce z R F 1 {k E 1 /k}[F 1 {v 1 {k E 1 /k}/x}[z]]. Consequently, we obtain k v 0 R NF F 1 {k E 1 /k}[F 1 {v 1 {k E 1 /k}/x}[ k v 1 {k E 1 /k} ]], as required.We now suppose t 0 is an open stuck term. If both t 0 and t 1 are delimited, then by the induction hypothesis, there exists an open stuck term t 1 such thatt 1 ⇓ v t 1 and t 0 R NF t 1 . It is then easy to prove that F 0 [t 0 ] R NF F 1 [t 1 ] or k F 0 [t 0 ] R NF k F 1 [t 1 ], depending on whether F 0 and F 1 are both delimited or not. Otherwise, for a fresh k, there exists t 1 such that k t 1 ⇓ v t 1 andk t 0 R NF t 1 . If F 0 = E 0 , then F 1 = E 1 ,and for any fresh k and x, we havek E 0 [x] R k E 1 [x] , and also k E 1 [t 1 ] ⇓ v t 1 {k E 1 /k}. We therefore have k t 0 {k E 0 /k} R NF t 1 {k E 1 /k}, i.e., k E 0 [t 0 ] R NF t 1 {k E 1 /k}, hence the result holds. If F 0

	v 0 ). From	R C	F 1 [	] and	R

C

F 1

  A • s 1 . The only possible transition is t 0 v -→ s 0 {v/x}. We have t 1 v -→ s 1 {v /x}. By substitutivity of A • , we have s 0 {v/x} A • s 1 {v /x}, and because x is the only free variable of s 0 and s 1 , we have s 0 {v/x} (A • ) c s 1 {v /x}, as required. Suppose t 0 = Sk.s 0 and t 1 = Sk.s 1 with s 0 A • s 1 . The only possible transition is t 0 E -→ s 0 {λx. E [x] /k} . We have t 1 E -→ s 1 {λx. E [x] /k} . Because A • is compatible and by Lemma B.5, we have λx. E [x] (A • ) c λx. E [x] . Therefore, by substitutivity of A • , we have s 0 {λx. E [x] /k} A • s 1 {λx. E [x] /k}, and because k is the only free variable of s 0 and s 1 , we have s 0 {λx. E [x] /k} (A • ) c s 1 {λx. E [x] /k} , as required. Suppose t 0 = (λx.s 0 ) v 0 and t 1 = t 1 1 t 2 1 with λx.s 0 (A • ) c t 1 1 and v 0 (A • ) c t 2 1 . The only possible transition is t 0 τ -→ s 0 {v 0 /x}. By Lemma B.4, there exists λx.s 1 , v 1 such that t 1 1 τ = ⇒ λx.s 1 , t 2

  1 ] holds. Therefore, by the induction hypothesis, there exists t 1 such that t 1= ==== ⇒ t 1 and t 0 (A • ) c t 1 . The • ) c is compatible, we have t 1 0 t 2 0 (A • ) c t 1 1 t 2 1, hence the result holds. Suppose t 0 = v 0 and t 1 = s 1 with v 0 (A • ) c s 1 . The only possible transition is t 0 τ -→ v 0 . By Lemma B.4, there exists v 1 such that s 1

	E [ t 2 1 ]
	1
	transition t 1 1 Next, suppose t 0 E [ t 2 1 ] = ==== ⇒ t 1 implies t 1 1 t 2 1 τ -→ t 1 0 t 2 0 , where t 1 0 exists t 1 1 such that t 1 1 τ = ⇒ t 1 1 and t 1 0 (A • ) c t 1 E = ⇒ t 1 , hence we have the required result. τ -→ t 1 0 . By the induction hypothesis, there 1 . Therefore we have t 1 τ = ⇒ t 1 1 t 2 1 , and
	because (A RR n°9096

τ = ⇒ v 1 and

  as wished. Suppose F 0 [t 0 ], F 1 [t 1 ] are delimited terms p 0 , p 1 . We distinguish two cases. First, suppose t 0 and t 1 are themselves delimited terms. If t 0 → v p 0 , thenp 0 → v F 0 [p 0 ]. Because t 0 Y E t 1 , there exists p 1 such that t 1 → * v p 1 and p 0 Y E p 1 . We have F 0 [p 0 ] X Ė v F 1 [p 1 ] and p 1 → * v F 1 [p 1 ], as wished. If t 0 → v v 0 , then p 0 → v F 0 [v 0 ]. Because t 0 Y E t 1 , there exists v 1 such that t 1 → * v v 1 and E def = {(v 0 , v 1 )} ∪ E ∈ Y. Hence we have p 1 → * v F 1 [v 1 ] and F 0 [v 0 ] X Ė v F 1 [v 1 ], as wished.In the second case, t 0 and t 1 are not both delimited terms. Then we can writep 0 = F 0 [ E 0 [t 0 ] ] and p 1 = F 1 [ E 1 [t 1 ] ] for some F 0 Ë F 1 and E 0 Ë E 1 . Because t 0 Y E t 1 and since Y is an environmental bisimulation, we have E 0 [t 0 ] Y E E 1 [t 1 ] . If E 0 [t 0 ] → v p 0 ,then there exists p 1 such that E 1 [t 1 ] → * v p 1 and p 0 Y E p 1 . Therefore, p 0

  as wished. Finally we prove the clause about environments. Let λx.t 0 Ė v λx.t 1 and v 0 Ė v v 1 . By Lemma C.11, we have t 0 {v 0 /x} X Ė v t 1 {v 1 /x}, as wished. Lemma C.12. If λx.t 0 F λx.t 1 , then t 0 {v/x} F t 1 {v/x}. Proof. It follows from the definition of the bisimulation and weakening. Lemma C.13. If λx.t 0 Ḟ λx.t F λx.t 1 and v 0 Ḟ v F v 1 then t 0 {v 0 /x} ḞF t 1 {v 1 /x}.

  1 1 t2 1 with v 1 0 Ḟ t 1 1 , and v 2 0 Ḟ t 2 1 . By Lemma C.17, there exist p 0 , p 1 such that E 0[r 0 ] → v p 0 , E 1 [t 1 ] → * v p 1 , and p 0 ḞF p 1 . Therefore we have p 0 → v F 0 [p 0 ], p 1 → * v F 1 [p 1 ], with F 0 [p 0 ] ḞF F 1 [p 1 ](by Lemma C.10 and definition of Ḟ), hence the result holds. The last case isr 0 = E [Sk.t 0 ] ; then t 1 = t 1 with E [Sk.t 0 ] Ḟ t 1 . By Lemma C.18, there exist p 0 , p 1 such that r 0 → v p 0 , t 1 → * v p 1 and p 0 ḞF p 1 . Therefore we have p 0 → v F 0 [ E 0 [p 0 ] ], p 1 → * v F 1 [ E 1 [p 1 ] ], with F 0 [ E 0 [p 0 ] ] ḞF F 1 [ E 1 [p 1 ] ] (by Lemma C.10 and definition of Ḟ), hence the result holds. Finally, we check the clause for environments. let λx.t 0 Ḟ λx.t 1 and v 0 Ḟ v 1 . By Lemma C.13, we get t 0 {v 0 /x} ḞF t 1 {v 1 /x}, hence the required result holds. C.3. Proof of Proposition 6.40 Let t 0 and t 1 such that k / ∈ fv(t 1 ). We want to show that (λx.Sk.t 0 ) t 1 F Sk.((λx.t 0 ) t 1 ). To this end, we need to plug both terms in some context E , and compare E [(λx.Sk.t 0 ) t 1 ] with E [Sk.((λx.t 0 ) t 1 )] . The second term reduces to (λx.t 0 {λy. E [y] /k}) t 1 , so we in fact prove the following result. Lemma C.20. We have E [(λx.Sk.t 0 ) t 1 ] F (λx.t 0 {λy. E [y] /k}) t 1 .

  . We have three cases for t. If t → v t , we still have t σ . If t → v v or t = k j , then both terms reduce to values that are in E, by definition of E. If t = F [k j v], then t σ

	Let t σ	-→ E 0 . . . σ i X E t δ -→ E	-→ E 0 . . . δ	-→ E	-→ E 0 . . . σ i X E t δ -→ E	-→ E 0 . . . δ	-→ E
	-→ E 0 . . . σ

i i

RR n°9096

This terminology comes from Kameyama (e.g., in[START_REF] Kameyama | A sound and complete axiomatization of delimited continuations[END_REF]); note that we use the metavariables of[START_REF] Biernacka | An operational foundation for delimited continuations in the CPS hierarchy[END_REF] for evaluation contexts, which are reversed compared to[START_REF] Kameyama | A sound and complete axiomatization of delimited continuations[END_REF].RR n°9096

A transition where internal steps are allowed before, but not after a visible action.RR n°9096

In the original semantics, the evaluation context of level i + 1 is a list (a stack, really) of evaluation contexts of level i separated by control delimiters of level i (contexts of level 1 are just the standard CBV evaluation contexts.) and the number of context layers is fixed[START_REF] Biernacka | An operational foundation for delimited continuations in the CPS hierarchy[END_REF].RR n°9096

Lemma A. [START_REF] Danvy | Representing control, a study of the CPS transformation[END_REF]. If R is a bisimulation up to context, F 0 [x] R F 1 [x] for a fresh x, t 0 R NF t 1 , and t 0 , t 1 are delimited open stuck terms, then

Proof. Because t 0 and t 1 are delimited open stuck terms, we have

for a fresh z, and v 0 R NF v 1 . To conclude, we have to prove that F 0 [F 0 [z]] R F 1 [F 1 [z]] holds. We know there exist t 0 , t 1 , such that F 0 [y] → * v t 0 , F 1 [y] → * v t 1 , and t 0 R t 1 . Note that F 0 and F 1 are either delimited or , therefore t 0 and t 1 are either delimited or values. If t 0 and t 1 are both delimited or both values, then we have F 0 [t 0 ] R F 1 [t 1 ], as wished. Otherwise, we can assume without loss of generality that t 0 is a value v 0 and t 1 is delimited. By Lemma A.18, there exists

Lemma A.20. Let R be a bisimulation up to context, and t 0 R t 1 such that t 0 is a normal form. There exists t 1 such that t 1 ⇓ v t 1 and t 0 R NF t 1 .

Proof. By induction on the derivation of t 0 R t 1 . The identity, bisimulation, compatibility w.r.t. λ-abstraction and shift cases are straightforward. The substitutivity case is a consequence of Lemma A. [START_REF] Crolard | A confluent lambda-calculus with a catch/throw mechanism[END_REF], and the two cases of compatibility w.r.t. context are consequences of Lemmas A.17 and A.19.

Lemma A. [START_REF] Dreyer | The impact of higher-order state and control effects on local relational reasoning[END_REF]. If R is a bisimulation up to context, then R is a non-η bisimulation up to reduction.

Proof. Because R is symmetric, we only have to prove that it is a non-η simulation up to reduction. We consider t 0 R t 1 with t 0 evaluating to t 0 in m steps; we prove that t 1 evaluates to a term t 1 so that t 0 R NF t 1 . We proceed by induction on m, and on the derivation of t 0 R t 1 , ordered lexicographically. Normal forms (i.e., m = 0) are dealt with Lemma A.20. Suppose m > 0.

Case: t 0 = t 1 , i.e., t 0 R t 0 . The result holds directly.

Case: t 0 R t 1 . The result follows from the definition of bisimulation up to context.

Case: t 0 {v 0 /x} R t 1 {v 1 /x} with t 0 R t 1 and v 0 R NF v 1 . We distinguish cases based on how t 0 {v 0 /x} reduces to a normal form t 0 .

First, assume t 0 itself reduces to a normal form t 0 so that t 0 = t 0 {v 0 /x}. Note that if t 0 is an open stuck term F 0 [y v 0 ], then necessarily y = x. By the induction hypothesis, there exists a normal form t 1 such that t 1 ⇓ v t 1 and t 0 R NF t 1 . In particular, if t 1 is an open stuck term F 1 [z v 1 ], then z = y = x, and therefore t 1 {v 1 /x} is a normal form. By Proposition 2.10, we have t 1 {v 1 /x} ⇓ v t 1 {v 1 /x}, and t 0 {v 0 /x} R NF t 1 {v 1 /x} holds by Lemma A. [START_REF] Crolard | A confluent lambda-calculus with a catch/throw mechanism[END_REF]. Therefore, we have the required result.

RR n°9096

where for

Proof. By induction on m, using Lemma A.27.

[M] F i , then for any fresh variables z 1 , . . . , z m and value v there exist values v

Proof. By induction on m, using Lemma A.25.

then for any sequence of fresh variables x 1 , . . . , x m , and value v, there exist contexts F 1 , . . . , F m , and values v 0 , . . . , v m such that

where for

Proof. By induction on m.

1 . Therefore, by Lemma A.29, for any fresh variables z 1 , . . . , z m , there exist values v 0 . . . v m such that

σ 0 , so we obtain terms in (the second set of) R .

Otherwise, we have

But these two resulting terms can be rewritten into respectively

for a fresh z, and since F 0 is not and also

and these two terms are delimited. Consequently, the terms A.1 and A.2 are related by R .

and on the other hand, we have

The two resulting terms are related by R , as wished.

From there, we can conclude using Lemma A. [START_REF] Gunter | A generalization of exceptions and control in ML-like languages[END_REF].

1 , and v 0 M NFη v 1 . The context F 0 is delimited, therefore it can be written

1 , we know there exists

for a fresh z. As a result, we have

We can therefore conclude with Lemma A. [START_REF] Herbelin | An approach to call-by-name delimited continuations[END_REF].

1 , and x M NFη v 1 . Consequently, we have

and also

We obtain two open stuck terms related by R NFη , as required.

RR n°9096

stuck term t 1 such that t 1 ⇓ v t 1 and t 0 R NF t 1 . We have

, and because t 0 and t 1 are delimited, t 0 and t 1 are also delimited. We can apply Lemma A.36, which gives us

Finally, if t 0 is a value v 0 , then by the induction hypothesis, there exists

{v 0 /x}, and from there we conclude as in the substitutivity case.

Case:

Let k be a fresh variable. If t 0 and t 1 are both delimited, then t 0 evaluates to a value or an open stuck term. We can then conclude the same way as in the corresponding case of the proof of Lemma A.21.

Suppose t 0 and t 1 are not both delimited, and let k be a fresh variable. Because k E 0 [t 0 ] evaluates to a normal form t 0 , k t 0 also evaluates to a normal form t 0 . By the induction hypothesis, there exists

] in at least one step, then we can conclude using the induction hypothesis, because we have

we can conclude as in the substituvity case, because we have

, and t 0 R t 1 . If t 0 and t 1 are both delimited, then the proof is the same as in the corresponding case of the proof of Lemma A.21. Otherwise, the proof is the same as in the previous case (with an extra layer of context).

B. Applicative Bisimilarity

Lemma B.1. If t 0 A • t 1 , then there exists a substitution σ which closes t 0 and t 1 such that t 0 σ (A • ) c t 1 σ, and the size of the derivation of t 0 σ (A • ) c t 1 σ is equal to the size of the derivation of t 0 A • t 1 .

Proof. By induction on t 0 A • t 1 . Suppose we have t 0 A • t 1 . Let σ be a substitution which closes t 0 and t 1 ; we have t 0 σ A • t 1 σ. The remaining cases are easy using induction. Lemma B.2. Let t be a closed term. If t α -→ t , then for all α (A • ) c α , there exists t such that t α -→ t and t (A • ) c t .

RR n°9096

Proof. Easy by induction on t The case v 0 A • A t 1 relies on induction and a similar reasoning as in the first case. If v 0 A • t 1 , then t 1 is a value and we can conclude directly.

Proof. By induction on v

Proof. Easy by induction on E

Lemma B.6 (Lemma 5.12 in the article). If t 0 (A • ) c t 1 and t 0 α -→ t 0 , then for all α (A • ) c α , there exists t 1 such that t 1 α = ⇒ t 1 and t 0 (A • ) c t 1 .

Proof. By induction on the size of the derivation of t

and the size of the derivation of t 0 σ (A • ) c t 2 σ is the same as for t 0 (A

hence the result holds. The case t 0 = s 0 , where s 0 is not a value, is easy using the induction hypothesis and compatibility of (A

We prove by induction on i ∈ 1 . . . k that there exists t i 0 such that

We have α (A • ) c α so by Lemma B.6, there exists t 1 0 such that t 1 0 α = ⇒ t 1 0 and t 0 (A • ) c t 1 0 , as wished. The case 1 < i ≤ k is easy by induction. In particular, for i = k, we have

We have the required result because

C. Environmental Bisimilarity

Proof. By induction on t 0 Ṙ t 1 .

Lemma C.2. Let E be an environment. Suppose t 0 Ė t 1 . If t 0 is a value, then so is t 1 .

Proof. Easy by induction on t 0 Ė t 1 .

Lemma C.3. Let E be an environment

Let Y be an environmental bisimulation. We define

In X 2 , we build the closed terms (t 0 , t 1 ) out of pairs of values. We first prove a preliminary lemma about X .

RR n°9096

Proof. We have two cases. If λx.t 0 E λx.t 1 , then t 0 {v 0 /x} Y E t 1 {v 1 /x} (because Y is a bisimulation), which implies t 0 {v 0 /x} X Ė v t 1 {v 1 /x} (more precisely, the terms are in X 1 ). If t 0 Ė t 1 with fv(t 0 ) ∪ fv(t 1 ) ⊆ {x}, then we have t 0 {v 0 /x} Ė t 1 {v 1 /x} by Lemma C.1, which implies t 0 {v 0 /x} X Ė v t 1 {v 1 /x} (more precisely, the terms are in X 2 ).

We now prove Lemma C.3 by showing that X is a bisimulation up to environment.

Proof. We first prove the bisimulation for the elements in X 2 (for these, we do not need the "up to environment"). Let t 0 Ė t 1 , with E ∈ Y. If t 0 is a value, then t 1 is a value (by Lemma C.2), and we have Ė v ∪ {(t 0 , t 1 )} = Ė v ∈ X . We now consider the case where t 0 is not a value. We proceed by induction on t 0 Ė t 1 .

Suppose t 0 = t 1 0 t 2 0 and t 1 = t 1 1 t 2 1 with t 1 0 Ė t 1 1 and t 2 0 Ė t 2 1 . We have several cases to consider.

. By the induction hypothesis, there exists

, hence the result holds.

• Assume t 1 0 = v 0 and t 2 0 → v t 2 0 , so that t 0 → v v 0 t 2 0 . Then t 1 1 is also a value v 1 according to Lemma C.2. By the induction hypothesis, there exists t 2

1 by definition of X . We also have t 1 → * v v 1 t 2 1 , hence the result holds.

Suppose t 0 = t 0 , t 1 = t 1 with t 0 Ė t 1 . We have two possibilities.

• Assume t 0 → v t 0 , so that t 0 → v t 0 . By the induction hypothesis, there exists t 1 such that t 1 → * v t 1 and t 0 X Ė v t 1 . By definition of X , we have t 0 X Ė v t 1 , and furthermore t 0 → * v t 1 , we therefore have the required result.

/k} by Lemma C.1 and compatibility of Ė. We therefore have the required result.

We now prove the bisimulation property (up to environment) for elements in

, and the terms

are similar to the one of X 2 . We can prove the bisimulation property with F 0 [v 0 ], F 1 [v 1 ] the same way we did with the terms in X 2 , except that we reason up to environment, because E ⊆ E . Suppose t 0 → v t 0 , and so

Suppose t 0 is a control stuck term E 0 [Sk.t 0 ]. We distinguish two cases. If F 0 is a pure context E 0 , then F 1 is also a pure context E 1 (as one can easily check by induction on

, and for all E 0 Ë E 1 , we have

Proof. We proceed by induction on

, and for all context E 1 , we have

. By the induction hypothesis, there exists

and

Proof. We prove that

is a bisimulation up-to bisimilarity. Note that by definition of X , we have

We prove the bisimulation clauses by induction on t 0 Ė t 1 . The case t 0 E t 1 holds because E is an environmental bisimulation. Suppose t 0 = λx.t 0 , t 1 = λx.t 1 with t 0 Ė t 1 and fv(t 0 ) ∪ fv(t 1 ) ⊆ {x}. We have to prove that ( Ė v ∪{(t 0 , t 1 )}) ∈ X , i.e., Ė v ∈ X , which is true. Suppose t 0 = t 1 0 t 2 0 , t 1 = t 1 1 t 2 0 with t 1 0 Ė t 1 1 and t 2 0 Ė t 2 1 . We distinguish several cases.

. By definition of Ė, we have t 1 0 t 2 0 Ė t 1 1 t 2 1 , and by Lemma C.3, we have

. By definition of Ė, we have v 0 t 2 0 Ė v 1 t 2 1 , and by Lemma C.3, we have

, and v 0 Ė v 1 , which implies t 0 {v 0 /x} ĖE t 1 {v 1 /x} by the same lemma. Because we also have t 1 → * v t 1 {v 1 /x}, the result holds.

, the result holds. The reasoning is the same if

Suppose t 0 = t 0 and t 1 = t 1 with t 0 Ė t 1 . We have three cases to consider.

C.2. Soundness Proof for the Original Semantics

The proof scheme is the same as for the relaxed semantics. We point out the main differences between the two proofs.

Lemma C.10. Let E be an environment

Let Y be an environmental bisimulation. We define

Proof. Similar to the proof of Lemma C.4.

We prove Lemma C.10 by showing that X is a bisimulation up to environment.

Proof. We first prove the bisimulation for the elements in X 2 . Let t 0 Ė t 1 , with E ∈ Y. If t 0 or t 1 is not delimited, then for all

Suppose t 0 , t 1 are delimited terms p 0 , p 1 . If p 0 → v v 0 , then p 0 = v 0 , and therefore p 1 = v 1 with v 0 Ẋ v 1 . We have p 1 → v v 1 , and also {(v 0 , v 1 )}∪ Ė v = Ė v ∈ X , as wished.

Otherwise p 0 → v p 0 . Then p 0 = F 0 [r 0 ]. Because E relates only values, we can prove there exist F 1 , r 1 such that p 1 = F 1 [r 1 ], F 0 Ë F 1 , and r 0 Ė r 1 . We distinguish several cases, depending on the redexes.

and t 0 → v t 0 or t 0 is stuck;

and t 0 → v t 0 or t 0 is stuck;

The proof is straightforward by induction on t 0 Ḟ t 1 .

Lemma C. [START_REF] Crolard | A confluent lambda-calculus with a catch/throw mechanism[END_REF].

Proof. If v 0 F t 1 , then we can conclude using the definition of the bisimilarity. Otherwise, t 1 is a value v 1 , and the result holds trivially.

Lemma C.16. Let t 0 F t 1 so that t 0 → v t 0 or t 0 is stuck, and

Proof. If t 0 and t 1 are both delimited terms, then t 0 cannot be stuck, and we conclude using bisimilarity and the definition of Ḟ. Suppose t 0 and t 1 are not both delimited terms. Because t 0 → v t 0 or t 0 is stuck, we know there exist p 0 , p 0 such that E 0 Proof. We prove that

is a bisimulation up to bisimilarity. By definition of X , we have t X Ḟ v t iff t Ḟ t . Let t 0 X Ḟ v t 1 . Suppose t 0 and t 1 are not both delimited terms. Then for all E 0 F E 1 , we have E 0 [t 0 ] X Ḟ v E 1 [t 1 ] , as required.

Suppose t 0 and t 1 are both delimited terms p 0 , p 1 . By Lemma C.14, we have several possibilities. If p 0 F p 1 , then the result holds trivially. Suppose p 0 = v 0 , p 1 = t 1 with v 0 Ḟ t 1 . By Lemma C.15, there exists v 1 such that t 1 → * v v 1 and v 0 Ḟ v 1 . We have {(v 0 , v 1 )}∪ Ḟ v = Ḟ v ∈ X , hence the result holds.

Suppose p 0 = F 0 [ E 0 [t 0 ] ] and

r 0 Ḟ t 1 , and r 0 F t 1 . We discuss the three possible redexes. If r 0 = v 0 , then t 1 = t 1 with v 0 Ḟ t 1 . By Lemma C.15, there exists v 1 RR n°9096