Dariusz Biernacki

Sergueï Lenglet

Applicative Bisimulations for Delimited-Control Operators

We develop a behavioral theory for the untyped call-by-value λ-calculus extended with the delimited-control operators shift and reset. For this calculus, we discuss the possible observable behaviors and we define an applicative bisimilarity that characterizes contextual equivalence. We then compare the applicative bisimilarity and the CPS equivalence, a relation on terms often used in studies of control operators. In the process, we illustrate how bisimilarity can be used to prove equivalence of terms with delimited-control effects.

Introduction

Morris-style contextual equivalence [START_REF] Morris | Lambda Calculus Models of Programming Languages[END_REF] is usually regarded as the most natural behavioral equivalence for functional languages based on λ-calculi. Roughly, two terms are equivalent if we can exchange one for the other in a bigger program without affecting its behavior (i.e., whether it terminates or not). The quantification over program contexts makes contextual equivalence hard to use in practice and, therefore, it is common to look for more effective characterizations of this relation. One approach is to rely on coinduction, by searching for an appropriate notion of bisimulation. The bisimulation has to be defined in such a way that its resulting behavioral equivalence, called bisimilarity, is sound and complete with respect to contextual equivalence (i.e., it is included and contains contextual equivalence, respectively).

The problem of finding a sound and complete bisimilarity in the λ-calculus has been well studied and usually leads to the definition of an applicative bisimilarity [START_REF] Abramsky | Full abstraction in the lazy lambda calculus[END_REF][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] (or, more recently, environmental bisimilarity [START_REF] Sangiorgi | Environmental bisimulations for higherorder languages[END_REF]). The situation is more complex in λ-calculi extended with control operators for first-class continuations-so far, only a few works have been conducted on the behavioral theory of such calculi. A first step can be found for the λµ-calculus (a calculus that mimics abortive control operators such as call/cc [START_REF] Parigot | λµ-calculus: an algorithmic interpretation of classical natural deduction[END_REF]) in [START_REF] Bierman | A computational interpretation of the λµ-calculus[END_REF] and [START_REF] David | λµ-calculus and Böhm's theorem[END_REF], where it is proved that the definition of contextual equivalence can be slightly simplified by quantifying over evaluation contexts only; such a result is usually called a context lemma. In [START_REF] Støvring | A complete, co-inductive syntactic theory of sequential control and state[END_REF], Støvring and Lassen define an eager normal form bisimilarity (based on the notion of Lévy-Longo tree equivalence) [START_REF] Lassen | Eager normal form bisimulation[END_REF][START_REF] Lassen | Normal form simulation for McCarthy's amb[END_REF][START_REF] Lassen | Typed normal form bisimulation for parametric polymorphism[END_REF] which is sound for the λµ-calculus, and which becomes sound and complete when a

The author is supported by the Alain Bensoussan Fellowship Programme.

notion of state is added to the λµ-calculus. 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. As for the λ-calculus extended with control only, however, no sound and complete bisimilarities have been defined.

In this article, we present a sound and complete applicative bisimilarity for a λ-calculus extended with Danvy and Filinski's static delimited-control operators shift and reset [START_REF] Danvy | Abstracting control[END_REF]. In contrast to abortive control operators, delimited-control operators allow to delimit access to the current continuation and to compose continuations. The operators shift and reset were introduced as a direct-style realization of the traditional success/failure continuation model of backtracking otherwise expressible only in continuation-passing style. The numerous theoretical and practical applications of shift and reset (see, e.g., [START_REF] Biernacka | An operational foundation for delimited continuations in the CPS hierarchy[END_REF] for an extensive list) include the seminal result by Filinski showing that a programming language endowed with shift and reset is monadically complete [START_REF] Filinski | Representing monads[END_REF].

The λ-calculi with static delimited-control operators have been an active research topic from the semantics as well as type-and proof-theoretic point of view (see, e.g., [START_REF] Biernacka | An operational foundation for delimited continuations in the CPS hierarchy[END_REF][START_REF] Biernacka | Context-based proofs of termination for typed delimited-control operators[END_REF][START_REF] Ariola | A type-theoretic foundation of delimited continuations[END_REF]). However, to our knowledge, no work has been carried out on the behavioral theory of such λ-calculi. In order to fill this void, we present a study of the behavioral theory of an untyped, call-by-value λ-calculus extended with shift and reset [START_REF] Danvy | Abstracting control[END_REF], called λ S . In Section 2, we give the syntax and reduction semantics of λ S , and discuss the possible observable behaviors for the calculus. In Section 3, we define an applicative bisimilarity, based on a labelled transition semantics, and prove it characterizes contextual equivalence, using an adaptation of Howe's congruence proof method [START_REF] Howe | Proving congruence of bisimulation in functional programming languages[END_REF]. As a byproduct, we also prove a context lemma for λ S . In Section 4, we study the relationship between applicative bisimilarity and an equivalence based on translation into continuation-passing style (CPS), a relation often used in works on control operators and CPS. In the process, we show how applicative bisimilarity can be used to prove equivalence of terms. Section 5 concludes the article and gives ideas for future work. Most of the proofs missing from the article are avalaible in [START_REF] Biernacki | Applicative bisimulations for delimited-control operators[END_REF].

The Language λ S

In this section, we present the syntax, reduction semantics, and contextual equivalence of the language λ S used throughout this article.

Syntax

The language λ S extends the call-by-value λ-calculus with the delimited-control operators shift and reset [START_REF] Danvy | Abstracting control[END_REF]. We assume we have a set of term variables, ranged over by x and k. We use two metavariables to distinguish term variables bound with a λ-abstraction from variables bound with a shift; we believe such distinction helps to understand examples and reduction rules. The syntax of terms and values is given by the following grammars:

Terms: t ::= x | λx.t | t t | Sk.t | t Values: v ::= λ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 is closed if it does not contain any free variable. Because we work mostly with closed terms, we consider only λ-abstractions as values.

We distinguish several kinds of contexts, defined below, which all can be seen as terms with a hole.

Pure evaluation 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

Reduction Semantics

Let us first briefly describe the intuitive semantics of shift and reset by means of an example written in SML using Filinski's implementation of shift and reset [START_REF] Filinski | Representing monads[END_REF].

Example 1. The following function copies a list [START_REF] Biernacki | A dynamic continuation-passing style for dynamic delimited continuations[END_REF] Formally, the call-by-value reduction semantics of λ S is defined by the following rules, where t{v/x} is the usual capture-avoiding substitution of v for x in t:

(β v ) F [(λx.t) v] → v F [t{v/x}] (shift) F [ E [Sk.t] ] → v F [ t{λx. E [x] /k} ] with x / ∈ fv(E ) (reset) F [ v ] → v F [v]
The term (λx. Example 2. Let i = λx.x and ω = λx.x x. 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 = ( (ω ω)) Sk 2
.ω (remember that we represent contexts insideout), 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] becomes clearer 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 untouched.

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.

There exist terms which are not values and which cannot be reduced any further; these are called stuck terms.

Definition 1. A closed 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, closed stuck terms are easy to characterize.

Lemma 1. A closed term t is stuck iff t = E [Sk.t ]
for some E , k, and t .

We call redexes (ranged over by r) the terms of the form (λx.t) v, E [Sk.t] , and v . Thanks to the following unique-decomposition property, the reduction → v is deterministic.

Lemma 2. For all closed terms t, either t is a value, or it is a stuck term, or there exist a unique redex r and a unique context F such that t

= F [r].
Given a relation R on terms, we write R * for the transitive and reflexive closure of R. We define the evaluation relation of λ S as follows.

Definition 2. We write t ⇓ v t if t → * v t and t → v . The result of the evaluation of a closed term, if it exists, is either a value or a stuck term. If a term t admits an infinite reduction sequence, we say it diverges, written t ⇑ v . In the rest of the article, we use extensively Ω = (λx.x x) (λx.x x) as an example of such a term.

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 iff they cannot be distinguished when put in an arbitrary context. The question is then what kind of behavior we want to observe. As in the regular λ-calculus we could observe only termination (i.e., does a term reduce to a value or not), leading to the following relation. Definition 3. Let t 0 , t 1 be closed terms. We write

t 0 ≈ 1 c t 1 if for all closed C , C [t 0 ] ⇓ v v 0 implies C [t 1 ] ⇓ v v 1 , and conversely for C [t 1 ].
This definition does not mention stuck terms; as a result, they can be equated with diverging terms. For example, let t 0 = (Sk.k λx.x) Ω, t 1 = Ω, and C be a closed context. If C [t 0 ] ⇓ v v 0 , then we can prove that for all closed t, there exists v such that C [t] ⇓ v v (roughly, because t is never evaluated; see [START_REF] Biernacki | Applicative bisimulations for delimited-control operators[END_REF] for further details). In particular, we have

C [t 1 ] ⇓ v v 1 . Hence, we have t 0 ≈ 1 c t 1 .
A more fine-grained analysis is possible, by observing stuck terms. Definition 4. Let t 0 , t 1 be closed terms. We write 3 Bisimilarity for λ S

t 0 ≈ 2 c t 1 if for all closed C , -C [t 0 ] ⇓ v v 0 implies C [t 1 ] ⇓ v v 1 ; -C [t 0 ] ⇓ v t 0 , where t 0 is stuck, implies C [t 1 ] ⇓ v t 1 ,
In this section, we define an applicative bisimilarity and prove it equal to contextual equivalence.

Labelled Transition System

To define the bisimilarity for λ S , we propose a labelled transition system (LTS), where the possible interactions of a term with its environment are encoded in the labels. Figure 1 defines a LTS t 0 α -→ t 1 with three kinds of transitions. An internal action t τ -→ t is an evolution from t to t without any help from the surrounding context; it corresponds to a reduction step from t to t . The transition v 0 v1 -→ 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 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 .

Most rules for internal actions (Fig. 1) 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 stuck term t to reduce to t . Hence, the transition t

E -→ t (λx.t) v τ -→ t{v/x} (βv) v τ -→ v (reset) t0 τ -→ t 0 t0 t1 τ -→ t 0 t1 (leftτ ) t τ -→ t v t τ -→ v t (right τ ) 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) t0 E t 1 ---→ t 0 t0 t1 E -→ t 0 (leftS ) t v E --→ t v t E -→ t (right S )
Fig. 1 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 an operator shift. 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 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 capture of E by t 0 t 1 . The rule (right S ) follows the same pattern. Finally, a 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 τ -→ t by letting t capture the empty context, i.e., by considering the transition t -→ t .

Example 3. With the same notations as in Example 2, we illustrate how the LTS handles capture by considering the transition from (i Sk.ω) (ω ω) .

Sk.ω i ( (ω ω)) -------→ ω (shift) i Sk.ω (ω ω) -----→ ω (right S ) (i Sk.ω) (ω ω) -→ ω (leftS ) (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.

The LTS corresponds to the reduction semantics and exhibits the observable terms (values and stuck terms) of the language in the following way. Lemma 3. The following hold:

-We have τ -→ = → v . -If t E -→ t , then t is a stuck term, and E [t] τ -→ t . -If t v -→ t ,
then t is a value, and t v τ -→ t .

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 delay2 transition α = ⇒ as ⇒ if α = τ and as ⇒ α -→ otherwise. The definition of the (weak delay) bisimilarity is then straightforward. Definition 6. 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 simulations. Applicative bisimilarity ≈ 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.

Lemma 4. If t τ -→ t (respectively t ⇓ v t ) then t ≈ t .
Lemma 4 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 7. 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. Big-step applicative bisimilarity . ≈ is the largest big-step applicative bisimulation.

Henceforth, we drop the adjective "applicative" and refer to the two kinds of relations simply as "bisimulation" and "big-step bisimulation". Lemma 5. We have ≈ = .

≈.

The proof is by showing that ≈ is a big step bisimulation, and that . ≈ is a bisimulation (using a variant of Lemma 4 involving . ≈). As a result, if R is a big-step bisimulation, then R ⊆ . ≈ ⊆ ≈. We work with both styles (small-step and big-step), depending on which one is easier to use in a given proof.

Example 4. Assuming we add lists and recursion to the calculus, we informally prove that the function copy defined in Example 1 is bisimilar to its effect-free variant, defined below. To this end, we define the relations (where we let l range over lists, and e over their elements) R 1 = {( e 1 :: e 2 :: . . . e n :: visit l , e 1 :: (e 2 :: . . . e n :: (copy2 l)))} R 2 = {( e 1 :: e 2 :: . . . e n :: l , e 1 :: (e 2 :: . . . e n :: l))} and we prove that

R 1 ∪ R 2 ∪{(l, l)} is a bisimulation. First, let t 0 R 1 t 1 .
If l is empty, then both visit l and copy2 l reduce to the empty list, and we obtain two terms related by R 2 . Otherwise, we have l = e n+1 :: l , visit l reduces to e n+1 :: visit l , copy2 l reduces to e n+1 :: (copy2 l ), and therefore t 0 and t 1 reduce to terms that are still in R 1 . Now, consider t 0 R 2 t 1 ; the transition from t 0 removes the delimiter surrounding l, giving a term related by R 2 to t 1 if there are still some delimiters left, or equal to t 1 if all the delimiters are removed. Finally, two identical lists are clearly bisimilar.

Soundness

To prove soundness of ≈ w.r.t. contextual equivalence, we show that ≈ 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 sketch the method and explain how we apply it to ≈; the complete proof can be found in [START_REF] Biernacki | Applicative bisimulations for delimited-control operators[END_REF].

The idea of the method is as follows: first, prove some basic properties of Howe's closure ≈ • , a relation which contains ≈ and is a congruence by construction. Then, prove a simulation-like property for ≈ • . From this result, prove that ≈ • and ≈ coincide on closed terms. Because ≈ • is a congruence, it shows that ≈ is a congruence as well. The definition of ≈ • 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 ≈ • is inductively defined as the smallest congruence containing ≈ • and closed under right composition with ≈ • . Definition 8. Howe's closure ≈ • is the smallest relation satisfying:

t 0 ≈ • t 1 t 0 ≈ • t 1 t 0 ≈ • ≈ • t 1 t 0 ≈ • t 1 t 0 ≈ • t 1 t 0 ≈ • t 1
By construction, ≈ • is a congruence (by the third rule of the definition), and composing on the right with ≈ • gives some transitivity properties to ≈ • . In particular, it helps in proving the following classical results (see [START_REF] Gordon | Bisimilarity as a theory of functional programming[END_REF] for the proofs).

Lemma 6 (Basic properties of ≈ • ). The following hold:

-For all t 0 , t 1 , v 0 , and

v 1 , t 0 ≈ • t 1 and v 0 ≈ • v 1 implies t 0 {v 0 /x} ≈ • t 1 {v 1 /x}. -The relation (≈ • ) * is symmetric.
The first item states that ≈ • is substitutive. This property helps in establishing the simulation-like property of ≈ • (second step of the method). Let (≈ • ) c be the restriction of ≈ • to closed terms. We cannot prove directly that (≈ • ) c is a bisimulation, so we prove a stronger result instead. We extend ≈ • to labels, by defining E ≈ • E as the smallest congruence extending ≈ • with the relation ≈ • , and by adding the relation τ ≈ • τ .

Lemma 7 (Simulation-like property).

If t 0 (≈ • ) c t 1 and t 0 α -→ t 0 , then for all α (≈ • ) c α , there exists t 1 such that t 1 α = ⇒ t 1 and t 0 (≈ • ) c t 1 .
Using Lemma 7 and the fact that ((≈ • ) c ) * is symmetric (by the second item of Lemma 6), we can prove that ((≈ • ) c ) * is a bisimulation. Therefore, we have

((≈ • ) c ) * ⊆ ≈, and because ≈ ⊆ (≈ • ) c ⊆ ((≈ • ) c ) * holds by construction, we can deduce ≈ = (≈ • ) c . Because (≈ •
) c is a congruence, we have the following result.

Theorem 1. The relation ≈ is a congruence.

As a corollary, ≈ is sound w.r.t. contextual equivalence.

Theorem 2. We have ≈ ⊆ ≈ c .

Completeness and Context Lemma

In this section, we prove that ≈ is complete w.r.t. ≈ c . To this end, we use an auxiliary relation .

≈ c , defined below, which refines contextual equivalence by testing terms with evaluation contexts only. While proving completeness, we also prove . ≈ c = ≈ c , which means that testing with evaluation contexts is as discriminative 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]. Definition 9. Let t 0 , t 1 be closed terms. We write t 0 . The proof of Theorem 3 is the same as in λ-calculus [START_REF] Gordon | Bisimilarity as a theory of functional programming[END_REF]; we prove that . ≈ c is a big-step bisimulation, using Lemmas 3, 4, and Theorem 2. The complete proof can be found in [START_REF] Biernacki | Applicative bisimulations for delimited-control operators[END_REF]. We can now prove that all the relations defined so far coincide. ≈ c (by definition). In this section we study the relationship between our bisimilarity (and thus contextual equivalence) and an equivalence relation based on translating terms with shift and reset into continuation-passing style (CPS). Such an equivalence has been characterized in terms of direct-style equations by Kameyama and Hasegawa who developed an axiomatization of shift and reset [START_REF] Kameyama | A sound and complete axiomatization of delimited continuations[END_REF]. We show that all but one of their axioms are validated by the bisimilarity of this article, which also provides several examples of use of the bisimilarity. We also pinpoint where the two relations differ.

≈ c t 1 if for all closed F , -F [t 0 ] ⇓ v v 0 implies F [t 1 ] ⇓ v v 1 ; -F [t 0 ] ⇓ v t 0 , where t 0 is stuck, implies F [t 1 ] ⇓ v t 1 ,
x = λk1k2.k1 x k2 λx.t = λk1k2.k1 (λx.t) k2 t0 t1 = λk1k2.t0 (λx0k 2 .t1 (λx1k 2 .x0 x1 k1 k 2 ) k 2 ) k2 t = λk1k2.t θ (λx.k1 x k2) Sk.t = λk1k2.t{(λx1k 1 k 2 .k1 x1 (λx2.k 1 x2 k 2 ))/k} θ k2 with θ = λxk2.k2 x

Axiomatization of Delimited Continuations

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 Fig. 2. 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.

It is natural to relate any other theory of shift and reset to their definitional CPS translation. For example, the reduction rules t → v t given in Section 2.2 are sound w.r.t. the CPS because CPS translating t and t yields βη-convertible terms in the λ-calculus. More generally, the CPS translation for shift and reset induces the following notion of equivalence on terms: Definition 10. Terms t and t are CPS equivalent if their CPS translations are βη-convertible.

In order to relate the bisimilarity of this article and the CPS equivalence, we use Kameyama and Hasegawa's axioms [START_REF] Kameyama | A sound and complete axiomatization of delimited continuations[END_REF], which characterize the CPS equivalence in a sound and complete way: two terms are CPS equivalent iff one can derive their equality using the equations of Fig. 3. Kameyama and Hasegawa's axioms relate not only closed, but arbitrary terms and they assume variables as values.

Kameyama and Hasegawa's Axioms through Bisimilarity

We show that closed terms related by all the axioms except for S elim are bisimilar. In the following, we write I for the bisimulation {(t, t)}. Proof (Sketch). The complete proof, quite technical, can be found in [START_REF] Biernacki | Applicative bisimulations for delimited-control operators[END_REF]. Let E 0 be such that fv(E 0 ) = ∅. Given two families of contexts (E

(λ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} • S (λx.t0) t1 = (λx. t0 ) t1 • 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(
i 1 ) i , (E i 2 ) i , we write σ E0 i (resp. σ λx.E0 [x] i ) the substitution mapping k i to λy. E i 1 [E 0 [E i 2 [y]]] (resp. λy. E i 1 [(λx.E 0 [x]) E i 2 [y]] ). We define R 1 = {(F [(λx.E 0 [x]) t]σ λx.E0 [x] 0 . . . σ λx.E0 [x] n , F [E 0 [t]]σ E0 0 . . . σ E0 n ), fv(t, F ) ⊆ {k 0 . . . k n }} R 2 = {(tσ λx.E0 [x] 0 . . . σ λx.E0 [x] n , tσ E0 0 . . . σ E0 n ), fv (
[E 0 [E i 2 [y]]] (resp. λy. E i 1 [(λx.E 0 [x]) E i 2 [y]]
) is applied to a value (i.e., if t = F [k i v]). In this case, the β-reduction generates terms in R 1 .

Bisimilarity and CPS Equivalence

In Section 4.2, we have considered all the axioms of Fig. 3, except S elim. The terms Sk.k t (with k / ∈ fv(t)) and t are not bisimilar in general, as we can see in the following result. Proposition 6. We have Sk.k v ≈ v.

The E -→ transition from Sk.k v cannot be matched by v. In terms of contextual equivalence, it is not possible to equate a stuck term and a value (it is also forbidden by the relation ≈ 1 c of Section 2.3). The CPS equivalence cannot distinguish between stuck terms and values, because the CPS translation turns all λ S terms into λ-calculus terms of the form λk 1 k 2 .t, where k 1 is the continuation up to the first enclosing reset, and k 2 is the continuation beyond this reset. Therefore, the CPS translation (and CPS equivalence) assumes that there is always an enclosing reset, while contextual equivalence does not. To be in accordance with CPS, the contextual equivalence should be changed, so that it tests terms only in contexts with an outermost delimiter. We conjecture that the CPS equivalence is included in such a modified contextual equivalence. Note that stuck terms can no longer be observed in such modified relation, because a term within a reset cannot become stuck (see the proof of Proposition 3). Therefore, the bisimilarity of this article is too discriminative w.r.t. to this modified equivalence, and a new complete bisimilarity has to be found.

Conversely, there exist bisimilar terms that are not CPS equivalent:

Proposition 7. 1. We have Ω ≈ Ω Ω, but Ω and Ω Ω are not CPS equivalent. 2. Let Θ = θ θ, where θ = λxy.y (λz.x x y z), and ∆ = λx.δ x δ x , where δ x = λy.x (λz.y y z). We have Θ ≈ ∆, but Θ and ∆ are not CPS equivalent.

Contextual equivalence puts 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.

Conclusion

In this article, we propose a first study of the behavioral theory of a λ-calculus with delimited-control operators. We discuss various definitions of contextual equivalence, and we define an LTS-based applicative bisimilarity which is sound and complete w.r.t. the chosen contextual equivalence. Finally, we point out some differences between bisimilarity and CPS equivalence. We believe this work can be pursued in the following directions.

Up-to techniques. 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 higherorder languages[END_REF] have been introduced to simplify the use of bisimulation in proofs of program equivalences. The idea is to prove terms equivalences using relations that are usually not bisimulations, but are included in bisimulations. The validity of some applicative bisimilarities up-to context remains an open problem in the λ-calculus [START_REF] Lassen | Relational reasoning about contexts[END_REF]; nevertheless, we want to see if some up-to techniques can be applied to the bisimulations of this article.

Other forms of bisimilarity. Applicative bisimilarity is simpler to prove than contextual equivalence, but its definition still involves some quantification over values and pure contexts in labels. Normal bisimilarities are easier to use because their definitions do not feature such quantification. Lassen has developed a notion of normal bisimilarity, sound in various λ-calculi [START_REF] Lassen | Eager normal form bisimulation[END_REF][START_REF] Lassen | Normal form simulation for McCarthy's amb[END_REF][START_REF] Lassen | Typed normal form bisimulation for parametric polymorphism[END_REF], and also complete in the λµ-calculus with state [START_REF] Støvring | A complete, co-inductive syntactic theory of sequential control and state[END_REF]. It would be interesting to see if this equivalence can be defined in a calculus with delimited control, and if it is complete in this setting. Another kind of equivalence worth exploring is environmental bisimilarity [START_REF] Sangiorgi | Environmental bisimulations for higherorder languages[END_REF].

Other calculi with control. Defining an applicative bisimilarity for the call-byname variant of λ S and for the hierarchy of delimited-control operators [START_REF] Danvy | Abstracting control[END_REF] should be straightforward. We plan to investigate applicative bisimilarities for a typed λ S as well [START_REF] Biernacka | Context-based proofs of termination for typed delimited-control operators[END_REF]. The problem seems more complex in calculi with abortive operators, such as call/cc. Because there is no delimiter for capture, these languages are not compositional (i.e., t → v t does not imply

E [t] → v E [t ]
), which makes the definition of a compositional LTS more difficult.

  fun copy2 nil = nil | copy2 (x::xs) = x::(copy2 xs)

with t 1

 1 stuck as well; and conversely for F [t 1 ]. Clearly we have ≈ c ⊆ . ≈ c by definition. The relation ≈ is complete w.r.t. . ≈ c . Theorem 3. We have . ≈ c ⊆ ≈.

Theorem 4 .

 4 We have ≈ c = . ≈ c = ≈. Indeed, we have . ≈ c ⊆ ≈ (Theorem 3), ≈ ⊆ ≈ c (Theorem 2), and ≈ c ⊆

.

Fig. 2 :

 2 Fig. 2: CPS translation

  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.

  with t 1 stuck as well; and conversely for C [t 1 ]. The relation ≈ 2 c distinguishes the terms t 0 and t 1 defined above. We believe ≈ 2 c is more interesting because it gives more information on the behavior of terms; consequently, we use it as the contextual equivalence for λ S . Henceforth, we simply write ≈ c for ≈ 2 c . The relation ≈ c , like the other equivalences on terms defined in this article, can be extended to open terms in the following way. Definition 5. Let R be a relation on closed terms. The open extension of R, written R • , is defined on open terms as: 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 1. Contextual equivalence can be defined directly on open terms by requiring that the context C binds the free variables of the related terms. The resulting relation would be equal to ≈ c

•

[START_REF] Gordon | Bisimilarity as a theory of functional programming[END_REF]

.

  For example, in the rule (shift), the result of the capture of E by Sk.t is t{λx. E [x] /k} .

: Labelled Transition System means that we have E [t] τ -→ t by context capture.

  Proposition 1. We have (λx.t) v ≈ t{v/x}, E [Sk.t] ≈ t{λx. E [x] /k} , and v ≈ v. Proof. We prove that R = {(λx.(λy.t) x, λy.t), x / ∈ fv(t)}∪ ≈ is a bisimulation. To this end, we have to check that λx.(λy.t)x /y}, i.e., that (λy.t) v 0 R t{v 0 /y} holds for all v 0 . We have (λy.t) v 0 Proposition 3. We have Sk. t ≈ Sk.t. Proof. Let R = {( t , t )}. We prove that {(Sk. t , Sk.t)}∪ R ∪ I is a bigstep bisimulation. The transition Sk. t We have (λx.t 0 ) t 1 ≈ (λx. t 0 ) t 1 .Proof. We prove that {( (λx.t 0 ) t 1 , (λx. t 0 ) t 1 )}∪ I is a big-step bisimulation. A transition (λx.t 0 ) t 1 α = ⇒ t (with α = τ ) is possible only if t 1 evaluates to some value v. In this case, we have (λx.t 0 ) t 1 = ⇒ t 0 {v/x} . From this, it is easy to see that (λx.t 0 ) t 1

						t)	S elim
			Fig. 3: Axiomatization of λ S
	Proof. These are direct consequences of the fact that	τ -→ ⊆ ≈ (Lemma 4).
	Proposition 2. If x / ∈ fv(v), then λx.v x ≈ v.
	v0 -→ (λy.t)v 0 is matched by λy.t t{v 0 τ v0 -→ -→ t{v 0 /y}, and because τ -→ ⊆ ≈ ⊆ R, we have the required result.
					E -→ t{λx. E [x] /k} is matched by
	Sk.t	E -→ t{λx. E [x] /k} , and conversely. Let t R t . It is straightforward
	to check that t	v0 = ⇒ v iff t	v0 = ⇒ v iff t	v0 = ⇒ v. Therefore, any	v = ⇒ transition from
	t is matched by t , and conversely. If t	τ -→ t , then t is a value or t = t
	for some t ; consequently, neither t nor t can perform a	E -→ transition.
	Proposition 4. τ = ⇒ (λx.t 0 ) v and (λx. t 0 ) t 1 τ	τ -→ t 0 {v/x} α = ⇒ t
	(with α = τ ) implies (λx. t 0 ) t 1

α = ⇒ t , and conversely.

Proposition 5. If x / ∈ fv(E ), then (λx.E [x]) t ≈ E [t].

  t) ⊆ {k 0 . . . k n }} and we prove that R 1 ∪ R 2 is a bisimulation. The relation R 1 contains the terms related by Proposition 5. The transitions from terms in R 1 give terms in R 1 , except if a capture happens in t; in this case, we obtain terms in R 2 . Similarly, most transitions from terms in R 2 give terms in R 2 , except if a term λy. E i 1

This terminology comes from Kameyama (e.g., in[START_REF] Kameyama | A sound and complete axiomatization of delimited continuations[END_REF]).

where internal steps are allowed before, but not after a visible action

Acknowledgments: We thank Ma lgorzata Biernacka, Daniel Hirschkoff, Damien Pous, and the anonymous referees for many helpful comments on the presentation of this work.


Dariusz Biernacki

Sergueï Lenglet

Normal Form Bisimulations for Delimited-Control Operators

We define a notion of normal form bisimilarity for the untyped call-by-value λ-calculus extended with the delimited-control operators shift and reset. Normal form bisimilarities are simple, easy-to-use behavioral equivalences which relate terms without having to test them within all contexts (like contextual equivalence), or by applying them to function arguments (like applicative bisimilarity). We prove that the normal form bisimilarity for shift and reset is sound but not complete w.r.t. contextual equivalence and we define up-to techniques that aim at simplifying bisimulation proofs. Finally, we illustrate the simplicity of the techniques we develop by proving several equivalences on terms.

Introduction

Morris-style contextual equivalence [START_REF] Morris | Lambda Calculus Models of Programming Languages[END_REF] is usually considered as the most natural behavioral equivalence for functional languages based on λ-calculi. Roughly, two terms are equivalent if we can exchange one for the other in a bigger program without affecting its behavior (i.e., whether it terminates or not). The quantification over program contexts makes contextual equivalence hard to use in practice and, therefore, it is common to look for easier-to-use behavioral equivalences, such as bisimilarities.

Several kinds of bisimilarity relations have been defined so far, such as applicative bisimilarity [START_REF] Abramsky | Full abstraction in the lazy lambda calculus[END_REF], 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), and environmental bisimilarity [START_REF] Sangiorgi | Environmental bisimulations for higherorder languages[END_REF]. Applicative and environmental bisimilarities usually compare terms by applying them to function arguments; as a result, we obtain relations which completely characterize contextual equivalence, but still contain a universal quantification over arguments in their definitions. In contrast, normal form bisimilarity does not need such quantification; it equates terms by reducing them to normal form, and by requiring the sub-terms of these normal forms to be bisimilar. Normal form relations are convenient in practice, but they are usually not complete w.r.t. contextual equivalence, i.e., 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], where normal form bisimilarity completely characterizes contextual equivalence. However, it has not yet been defined for calculi with delimited-control operators, such as shift and reset [START_REF] Danvy | Abstracting control[END_REF]programming constructs rapidly gaining currency in the recent years. Unlike abortive control operators (such as call/cc), delimited-control operators allow to delimit access to the current continuation and to compose continuations. The operators shift and reset were introduced as a direct-style realization of the traditional success/failure continuation model of backtracking otherwise expressible only in continuation-passing style [START_REF] Danvy | Abstracting control[END_REF]. The numerous theoretical and practical applications of shift and reset (see, e.g., [START_REF] Biernacka | An operational foundation for delimited continuations in the CPS hierarchy[END_REF] for an extensive list) include the seminal result by Filinski showing that a programming language endowed with shift and reset is monadically complete [START_REF] Filinski | Representing monads[END_REF].

Up to now, only an applicative bisimilarity has been defined for a calculus with shift and reset [START_REF] Biernacki | Applicative bisimulations for delimited-control operators[END_REF]. In this paper, we define several notions of normal form bisimilarity for such a calculus, more tractable than contextual equivalence or applicative bisimilarity. We prove they are sound w.r.t. contextual equivalence (i.e., included in contextual equivalence), but fail to be complete. We also develop up-to techniques that are helpful when proving equivalences with normal form bisimulations.

In Section 2, we define the λ-calculus with delimited control that we use in this paper, and we recall the definition of contextual equivalence of [START_REF] Biernacki | Applicative bisimulations for delimited-control operators[END_REF] for this calculus. We then define in Section 3 the main notion of normal form bisimilarity and we prove its properties. In Section 4, we refine the definition of normal form bisimilarity to relate more contextually equivalent terms, at the cost of extra complexity in bisimulation proofs. We also propose several up-to techniques which simplify the proofs of equivalence of terms. In Section 5, we illustrate the simplicity of use (compared to applicative bisimilarity) of the notions we define by employing them in the proofs of several equivalences of terms. Section 6 concludes the paper. The extended version of this article [START_REF] Biernacki | Normal form bisimulations for delimited-control operators[END_REF] contains the congruence proofs of the considered normal form bisimilarities.

The Calculus λ S

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

Syntax

The language λ S extends the call-by-value λ-calculus with the delimited-control 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 term variables representing a continuation (e.g., when bound with a shift), while x, y, and z stand for any values; we believe such distinction helps to understand examples and reduction rules. The syntax of terms and values is given by the following grammars:

Terms: t ::= x | λx.t | t t | Sk.t | t Values: v ::= λx.t | x
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 is closed if it does not contain free variables.

We distinguish several kinds of contexts, 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

Reduction Semantics

Before we present the reduction semantics for λ S , let us briefly describe an intuitive semantics of shift and reset by means of an example written in SML, using Filinski's implementation of shift and reset [START_REF] Filinski | Representing monads[END_REF].

Example 1. The following function copies a list [START_REF] Biernacki | A dynamic continuation-passing style for dynamic delimited continuations[END_REF], where the SML expression shift (fn k => t) corresponds to Sk.t and reset (fn () => t) corresponds to t : This simple function illustrates the main ideas of programming with shift and reset:

• The control delimiter reset delimits continuations. Any control effects occurring in the subsequent calls to function visit are local to function copy. • The control operator shift captures delimited continuations. Each but last recursive call to visit abstracts the continuation that can be represented as a function fn v => reset (fn () => visit v) and binds it to k. • Captured continuations are composed statically. When applied, in the expression x :: (k xs), the captured continuation becomes the current delimited continuation that is isolated from the rest of the program, and in particular from the expression x ::, by a control delimiter-witness the control delimiter in the expression fn v => reset (fn () => visit v) representing the captured continuation.

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

(β v ) F [(λx.t) v] → v F [t{v/x}] (shift) F [ E [Sk.t] ] → v F [ t{λx. E [x] /k} ] with x / ∈ fv(E ) (reset) F [ v ] → v F [v]
The term (λx.

.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 untouched.

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.

There exist terms which are not values and which cannot be reduced any further; these are called stuck terms.

Definition 1. 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.

Lemma 1. 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 terms of the form E [Sk.t] and open stuck terms the terms of the form F [x v].

Definition 2. 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.

Lemma 2. 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 write → * v for the transitive and reflexive closure of → v , and we define the evaluation relation of λ S as follows.

Definition 3. We write t ⇓ v t if t → * v t and t → v .
The result of the evaluation of a term, if it exists, is a normal form. If a term t admits an infinite reduction sequence, we say it diverges, written t ⇑ v . In the rest of the article, we use extensively Ω = (λx.x x) (λx.x x) as an example of such a term.

Contextual Equivalence

In this paper, we use the same contextual equivalence as in [START_REF] Biernacki | Applicative bisimulations for delimited-control operators[END_REF], where control stuck terms can be observed. Note that this relation is a bit more discriminative than simply observing termination, as pointed out in [START_REF] Biernacki | Applicative bisimulations for delimited-control operators[END_REF]. Definition 4. Let t 0 , t 1 be terms. We write t 0 ≈ c t 1 if for all C such that C [t 0 ] and C [t 1 ] are closed, the following hold: We can simplify the proofs of contextual equivalence of terms by relying on the following context lemma [START_REF] Milner | Fully abstract models of typed λ-calculi[END_REF] for λ S (for a proof see Definition 5 and Section 3.4 in [START_REF] Biernacki | Applicative bisimulations for delimited-control operators[END_REF]). Instead of testing terms with (free-variables capturing) general contexts, we can simply first close them (using closed values) and then put them within (closed) evaluation contexts.

-C [t 0 ] ⇓ v v 0 implies C [t 1 ] ⇓ v v 1 ; -C [t 0 ] ⇓ v t 0 , where t 0 is control stuck, implies C [t 1 ] ⇓ v t 1 ,
Lemma 3 (Context Lemma). We have t 0 ≈ c t 1 iff for all closed contexts F and for all substitutions σ (mapping variables to closed values) such that t 0 σ and t 1 σ are closed, the following hold:

- In the rest of the paper, when proving that terms are contextually equivalent, we implicitly use Lemma 3.

F [t 0 σ] ⇓ v v 0 implies F [t 1 σ] ⇓ v v 1 ; -F [t 0 σ] ⇓ v t 0 , where t 0 is control stuck, implies F [t 1 σ] ⇓ v t 1 ,

Normal Form Bisimilarity

In this section, we discuss a notion of bisimulation based on the evaluation of terms to normal forms. The difficulties are mainly in the handling of control stuck terms and in the definition of the relation on non-pure evaluation contexts. We propose here a first way to deal with control stuck terms, that will be refined in the next section. In any definitions or proofs, we say a variable is fresh if it does not occur free in the terms or contexts under consideration.

Definition

Following Lassen's approach [START_REF] Lassen | Eager normal form bisimulation[END_REF], we define a normal form bisimulation where we relate terms by comparing the results of their evaluation (if they exist). As we need to compare terms as well as evaluation contexts, we extend a relation R on terms to contexts in the following way: we write

F 0 R F 1 if F 0 = F 0 [ E 0 ], F 1 = F 1 [ E 1 ], F 0 [x] R F 1 [x]
, and

E 0 [x] R E 1 [x] for a fresh x, or if F 0 = E 0 , F 1 = E 1 , and E 0 [x] R E 1 [x]
for a fresh x. The rationale behind this definition is explained later. Following [START_REF] Lassen | Eager normal form bisimulation[END_REF], we define the application v y as x y if v = x, and as t{y/x} if v = λx.t. Finally, given a relation R on terms, we write R -1 for its inverse, and we inductively define a relation R NF on normal forms as follows: Henceforth, we often drop the "normal form" attribute when talking about bisimulations for brevity. 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.

v 0 x R v 1 x x fresh v 0 R NF v 1 E 0 R E 1 t 0 R t 1 E 0 [Sk.t 0 ] R NF E 1 [Sk.t 1 ] F 0 R F 1 v 0 R NF v 1 F 0 [x v 0 ] R NF F 1 [x v 1 ] Definition 5. A relation R
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 an 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 the two contextually equivalent terms Sk. t and Sk.t. 2 Indeed, without reset, we would have to relate t and t, which are not equivalent in general (take t = Sk .v for some v), while Definition 5 requires t and t to be related (which holds for all t; see Example 3).

Two normal forms F 0 [xv 0 ] and F 1 [xv 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 xv 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 extension of bisimulation to contexts (given before Definition 5) 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 .

Example 3. We prove that t ≈ t by showing that R= {( t , t Similarly, it is easy to check that the evaluations of t are matched by t .

)}∪ ≈ is a bisimulation. If t ⇓ v v, then t ⇓ v v,
Example 4. In [START_REF] Danvy | A functional abstraction of typed contexts[END_REF], the authors propose variants of Curry's and Turing's call-byvalue fixed point combinators using shift and reset. Let θ = λxy.y (λz.x x y z).

We prove that Turing's combinator t 0 = θ θ is bisimilar to its shift and reset variant t 1 = θ Sk.k k . We build the candidate relation R incrementally, starting from (t 0 , t 1 ). Evaluating t 0 and t 1 , we obtain t 0 ⇓ v λy.y (λz.θ θ y z) = v 0 and t 1 ⇓ v λy.y (λz.(λx. θ x ) (λx. θ x ) y z) = v 1 ; we have to add (v 0 y, v 1 y) (for a fresh y) to R. To relate these terms, we must add (v 0 z, v 1 z) and (z, z) for a fresh z to R, where v 0 = λz.θ θ y z and v 1 = λz.(λx. θ x ) (λx. θ x ) y z.

Evaluating v 0 z and v 1 z, we obtain respectively y v 0 z and y v 1 z; to relate these two normal forms, 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 . One can check that the constructed relation R is a normal form bisimulation. In contrast, Curry's combinator t 0 = λx.δ x δ x , where δ x = λy.x (λz.y y z), is not bisimilar to its delimited-control variant t 1 = λ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 ≈ . In fact, t 0 and t 1 are distinguished by the context λx.Sk.Ω. Finally, we can prove that the two original combinators θ θ and λx.δ x δ x 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], and proofs based on continuation-passing style (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 the eager normal form bisimilarity and the Böhm trees equivalence [START_REF] Lassen | Eager normal form bisimulation[END_REF].

Because shift and reset have been originally defined in terms of CPS [START_REF] Danvy | Abstracting control[END_REF], one can expect the CPS approach to be successful. However, the CPS translation of shift and reset assumes that λ S terms are executed within an outermost reset, and therefore they cannot evaluate to a control stuck term. For the normal form bisimilarity to be sound w.r.t. CPS, we would have to restrict its definition to terms of the form t . This does not seem possible while keeping Definition 5 without quantification over contexts. For example, to relate values v 0 and v 1 , we would have to execute v 0 x and v 1 x (where x is fresh) under reset. However, requiring simply v 0 x and v 1 x to be related would be unsound; such a definition would relate λy.Sk.k y and λy.Sk.(λz.z) y, which can be distinguished by the context (λz.z) Ω . To be sound, we would have to require E [v 0 x] to be related to E [v 1 x] for every E ; we then introduce a quantification over contexts that we want to avoid in the first place. Because normal forms may contain control stuck terms as sub-terms, normal form bisimilarity has to be able to handle them, and, therefore, it cannot be restricted to terms of the form t only.

Since CPS cannot help us in proving congruence, we follow a more direct approach, by relying on a context closure. Given a relation R, we define its substitutive, reflexive, and context closure R by the rules of Fig. 1. The main lemma of the congruence proof is then as follows: Lemma 4. If R is a normal form bisimulation, then so is R.

More precisely, we prove that if t 0 R t 1 and t 0 evaluates to some normal form t 0 in m steps, then t 1 evaluates to a normal form t 1 such that t

0 R NF t 1 . The t R t t0 R t1 t0 R t1 t0 R t1 v0 R NF v1 t0{v0/x} R t1{v1/x} t0 R t1 F0 R F1 F0 [t0] R F1 [t1] t0 R t1 λx.t0 R λx.t1 t0 R t1 Sk.t0 R Sk.t1
Fig. 1: Substitutive, reflexive, and context closure of a relation R proof is by nested induction on m and on the definition of R; it can be found in [START_REF] Biernacki | Normal form bisimulations for delimited-control operators[END_REF]. Congruence of ≈ then follows immediately.

Corollary 1. The relation ≈ is a congruence

We can then easily prove that ≈ is sound w.r.t. contextual equivalence.

Theorem 1. We have ≈ ⊆ ≈ c .

The following counter-example shows that the inclusion is in fact strict; normal form bisimilarity is not complete.

Proposition 1. Let i = λy.y. We have

x i Sk.i ≈ c x i ( x i Sk.i) , but x i Sk.i ≈ x i ( x i Sk.i) .
Proof. Replacing x by a closed value v, we get v i Sk.i and v i ( v i Sk.i) , which both evaluate to i if the evaluation of v i terminates (otherwise, they both diverge). With this observation, it is easy to prove that x i Sk.i and x i ( x i Sk.i) are contextually equivalent. They are not 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).

Refined Bisimilarity and Up-to Techniques

In this section, we propose an improvement of the definition of normal form bisimilarity, and we discuss some proof techniques which aim at simplifying equivalence proofs.

Refined Bisimilarity

Normal form bisimilarity could better deal with control stuck terms. To illustrate this, consider the following terms.

Proposition 2. Let i = λx.x. We have Sk.i ≈ c (Sk.i) Ω, but Sk.i ≈ (Sk.i) Ω.
Proof. If Sk.i and (Sk.i) Ω are put within a pure context, then we obtain two control stuck terms, and if we put these two terms within a context F [ E ], then they both reduce to F [i]. Therefore, Sk.i and (Sk.i) Ω are contextually equivalent. They are not normal form bisimilar, since the contexts and Ω are not bisimilar (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 is defined the same way as R NF on values and open stuck terms, and is defined on control stuck terms as follows: In the control stuck terms case, Definition 6 simulates the capture of E 0 (respectively E 1 ) by Sk.t 0 (respectively Sk.t 1 ). However, if t 0 is 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 using a variable k in the definition of R RNF , which represents the context that can be captured beyond E 0 and E 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 ] Definition 6. A relation R on terms is a refined normal form simulation if t 0 R t 1 and t 0 ⇓ v t 0 implies t 1 ⇓ v t 1 and t 0 R RNF t 1 . A relation R
Refined bisimilarity contains the regular bisimilarity.

Proposition 3. We have ≈ ⊂ • ≈.
Indeed, for control stuck terms, we have

t 0 ⇓ v E 0 [Sk.t 0 ], t 1 ⇓ v E 1 [Sk.t 1 ], E 0 ≈ E 1 , and t 0 ≈ t 1 . Because ≈ is a congruence (Corollary 1), it is easy to see that t 0 {λx. k E 0 [x] /k} ≈ t 1 {λx. k E 1 [x]
/k} holds for fresh k and x. Therefore, ≈ is a refined bisimulation, and is included in

• ≈.
The inclusion is strict, because • ≈ relates the terms of Proposition 2, while ≈ does not. Proving that • ≈ is sound requires some adjustments to the congruence proof of ≈. First, given a relation R on terms, we define its substitutive, bisimilar, and context closure R by extending the rules of Fig. 1 with the following one.

t 0 • ≈ t 0 t 0 R t 1 t 1 • ≈ t 1 t 0 R t 1
Henceforth, we simply write

• ≈ R
• ≈ for the composition of the three relations.

Our goal is to prove that • ≈ is a refined bisimilarity. To this end, we need a few lemmas.

Lemma 5. If x / ∈ fv(E ), then (λx.E [x]) t ≈ E [t].
One can prove that {((λx.E [x]) t, E [t]), x / ∈ fv(E )} ∪ {(t, t)} is a bisimulation, by a straightforward case analysis on the result of the evaluation of t (if it exists). Note that Lemma 5, known as the β Ω axiom in [START_REF] Kameyama | A sound and complete axiomatization of delimited continuations[END_REF], has also been proved in [START_REF] Biernacki | Applicative bisimulations for delimited-control operators[END_REF] using applicative bisimulation. We can see that the proof is much simpler using normal form bisimulation. With Lemma 5, congruence of ≈, and Proposition 3, we then prove the following result.

Lemma 6. If x / ∈ fv(E 0 ) ∪ fv(E 1 ) and y / ∈ fv(E 1 ) then t{λx. E 1 [E 0 [x]] /k} • ≈ t{λx. (λy.E 1 [y]) E 0 [x] /k} .
The main lemma of the congruence proof of • ≈ is as follows.

Lemma 7. If R is a refined bisimulation, then so is R.

The proof is an adaptation of the proof of Lemma 4. We sketch one sub-case of the proof, to illustrate why we need R (instead of R) and Lemma 6.

Proof (Sketch). Assume we are in the case where

E 0 [t 0 ] R E 1 [t 1 ] with E 0 [y] R E 1 [
y] for a fresh y, and t 0 R t 1 . Moreover, suppose t 0 ⇓ v E 0 [Sk.t 0 ]. Then by the induction hypothesis, we know that there exist

E 1 , 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 . Hence, we have E 0 [t 0 ] ⇓ v E 0 [E 0 [Sk.t 0 ]] and t 1 ⇓ v E 1 [E 1 [Sk.t 1 ]
], and we want to prove that

t 0 {λx. k E 0 [E 0 [x]] /k} R t 1 {λx. k E 1 [E 1 [x]] /k} holds. Be- cause E 0 [y] R E 1 [y], we have λy.k E 0 [y] R RNF λy.k E 1 [
y] (**). Using (*) and (**), we obtain

t 0 {λx. (λy.k E 0 [y]) E 0 [x] /k} R t 1 {λx. (λy.k E 1 [y]) E 1 [x] /k} ,
because R is substitutive. By Lemma 6, we know that

t 0 {λx. k E 0 [E 0 [x]] /k} • ≈ t 0 {λx. (λy.k E 0 [y]) E 0 [x] /k} t 1 {λx. k E 1 [E 1 [x]] /k} • ≈ t 1 {λx. (λy.k E 1 [y]) E 1 [x] /k} , which means that t 0 {λx. k E 0 [E 0 [x]] /k} • ≈ R • ≈ t 1 {λx. k E 1 [E 1 [x]
] /k} holds. The required result then holds because

• ≈ R • ≈ ⊆ R.
We can then conclude that • ≈ is a congruence, and is sound w.r.t. ≈ c .

Corollary 2. The relation

• ≈ is a congruence. Theorem 2. We have • ≈ ⊂ ≈ c .
The inclusion is strict, because the terms of Proposition 1 are still not related by • ≈. We would like to stress that even though • ≈ equates more contextually equivalent terms than ≈, the latter is still useful, since it leads to very simple proofs of equivalence, as we can see with Lemma 5 (and with the examples of Section 5). Therefore,

• ≈ does not disqualify ≈ as a proof technique.

Examples

We now illustrate the usefulness of the relations and techniques defined in this paper, by proving some terms equivalences derived from the axiomatization of λ S [START_REF] Kameyama | A sound and complete axiomatization of delimited continuations[END_REF]. The relationship between contextual equivalence and Kameyama and Hasegawa's axioms has been studied in [START_REF] Biernacki | Applicative bisimulations for delimited-control operators[END_REF], using applicative bisimilarity. In particular, we show that terms equated by all the axioms except for S elim (Sk.k t = t if k / ∈ fv(t)) are applicative bisimilar. The same result can be obtained for normal form bisimilarity, using the same candidate relations as for applicative bisimilarity (see Propositions 1 to 4 in [START_REF] Biernacki | Applicative bisimulations for delimited-control operators[END_REF]), except for the β Ω axiom, where the equivalence proof becomes much simpler (see Lemma 5). The terms Sk.k v v (equated by S elim) are not (applicative or normal form) bisimilar, because the former is control stuck while the latter is not. Conversely, there exist bisimilar terms that are not related by the axiomatization, such as Ω Ω and Ω, or Curry's and Turing's combinators (Example 4).

In this section, we propose several terms equivalences, the proofs of which are quite simple using normal form bisimulation, especially compared to applicative bisimulation. In the following, we write I for the identity bisimulation {(t, t)}.

Proposition 4. If x / ∈ fv(E ), then E [(λx.t 0 ) t 1 ] ≈ (λx.E [t 0 ]) t 1 . Proof. By showing that {(E [(λx.t 0 ) t 1 ], (λx.E [t 0 ]) t 1 ), x / ∈ fv(E )}∪ I is a normal form bisimulation.
The proof is straightforward by case analysis on the result of the evaluation of t 1 (if it exists).

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

Proposition 5. If x / ∈ fv(E ), then (λx. E [x] ) t ≈ E [t] . Proof. Let R= {( (λx. E [x] ) t , E [t] ),
x / ∈ fv(E )}. We prove that R ∪ ≈ is a small-step bisimulation up to context, by case analysis on t.

-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 3 that E [v] ≈ E [v] . -If t = F [y v], then we have to relate (λx. E [x] ) F and E [F ] (we clearly have v ≈ NF v). If F = F [ E ], then we have (λx. E [x] ) F [z] R E [F [z]] and E [z] ≈ E [z] for a fresh z. If F = E , then (λx. E [x] ) E [z] R E [E [z]] holds for a fresh z. -If t = E [Sk.t ], then (λx. E [x] ) t → v t {λy. (λx. E [x] ) E [y] /k} , and E [t] → v t {λy. E [E [y]] /k} . We have (λx. E [x] ) E [y] R E [E [y]] , therefore t {λy. (λx. E [x] ) E [y] /k} R t {λy. E [E [y]
] /k} holds, as wished.

Without using small-step bisimulation, the definition of R as well as the bisimulation proof would be much more complex, since we would have to compute the results of the evaluations of (λx. • ≈ (λy. k y ) E [x] directly, using a small-step refined bisimulation up to context. Proving Proposition 6 with the regular normal form bisimilarity would require us to equate E [y] and y (where y is fresh), which is not possible if E = (λz.Ω) .

Conclusion

In this paper, we propose several normal formal bisimilarities for a λ-calculus with shift and reset, and we demonstrate their usefulness on several examples. Proving equivalences with the regular normal form bisimilarity generates minimal proof obligations, especially when used with up-to techniques. If the regular bisimilarity fails to relate the tested terms, then the refined bisimilarity can be of help. If they both fail, then we may have to use the applicative bisimilarity [START_REF] Biernacki | Applicative bisimulations for delimited-control operators[END_REF], which, unlike the bisimilarities of this paper, is complete.

We believe this work can easily be adapted to other delimited-control operators as well as the CPS hierarchy [START_REF] Danvy | Abstracting control[END_REF]. It might also be interesting to extend this work to the typed setting. Another possible future work would be to define environmental bisimulations [START_REF] Sangiorgi | Environmental bisimulations for higherorder languages[END_REF] for λ S . When comparing two terms, environmental relations use an additional component, the environment, which represents the current knowledge of the observer. E.g., in the pure λ-calculus, when two tested terms reduce to values, they become known to the observer and are added to the environment. The observer can then challenge two λ-abstractions by applying them to two related arguments built from the environment. Environmental bisimilarities are usually sound and complete, and also allow for up-to techniques.

Another issue is to find a characterization of contextual equivalence for λcalculi with abortive control operators. Normal form bisimilarities have been defined for extensions of the λµ-calculus [START_REF] Lassen | Head normal form bisimulation for pairs and the λµ-calculus[END_REF], but they are usually not complete, except in the presence of a store construct [START_REF] Støvring | A complete, co-inductive syntactic theory of sequential control and state[END_REF]. It might be possible to reach completeness with applicative or environmental bisimilarities.

  fun copy xs = let fun visit nil = nil | visit (x::xs) = visit (shift (fn k => x :: (k xs))) in reset (fn () => visit xs) end

  v, and we have to prove that F R F 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 ≈⊆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 [y] R E [y] (true because ≈⊆R).

•≈

  t{λx. (λy. k y ) E [x] /k} for a fresh k . We know that k E [x] ≈ (λy. k y ) E [x] holds by Proposition 5. Consequently, we have k E [x] • ≈ (λy. k y ) E [x] by Proposition 3. We can then conclude by congruence of • ≈. Without Proposition 5, we would have to prove k E [x]

  F [t]); the free variables of t may be captured in the process. A context is closed if it contains only closed terms.

1

(abbreviated as pure contexts), 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 (respectively E , F ) with a term t produces a term, written C [t] (respectively E [t],

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

	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.
	Example 2.

((Sk 1

  is a refined normal form bisimulation if both R and R -1 are refined normal form simulations. Refined normal form bisimilarity, written

• ≈, is the largest refined normal form bisimulation.

  E [x] ) t and of E [t] , which is particularly difficult if t is a control stuck term. For the next example, we have to use refined bisimilarity. Proposition 6. If k / ∈ fv(E ) ∪ fv(t) and x / ∈ fv(E ), then we have E [Sk.t] Sk .t{λx. k E [x] /k}. Proof. The two terms are control stuck terms, therefore, we have to prove t{λx. k E [x] /k}

• ≈

This terminology comes from Kameyama (e.g., in[START_REF] Kameyama | A sound and complete axiomatization of delimited continuations[END_REF]).

The equivalence Sk. t ≡ Sk.t comes from Kameyama and Hasegawa's axiomatization of shift and reset[START_REF] Kameyama | A sound and complete axiomatization of delimited continuations[END_REF] and has been proved using applicative bisimilarity in[START_REF] Biernacki | Applicative bisimulations for delimited-control operators[END_REF].

Acknowledgments: We thank Ma lgorzata Biernacka and the anonymous referees for insightful comments on the presentation of this work.

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 higherorder 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. As pointed out in [START_REF] Lassen | Relational reasoning about contexts[END_REF], using a direct approach to prove congruence of the normal form bisimilarity (as in Sections 3.2 and 4.1) makes up-to techniques based on the context closure easy to define and to prove valid. For example, we define bisimulation up to substitutive, reflexive, and context closure (in short, up to context) as follows.

Consequently, if R is a bisimulation up to context, and if

Example 5. We can simplify the proof of bisimilarity between Turing's fixed point combinator and its delimited-control variant (cf. Example 4); indeed, it is enough to prove that R= {(θ θ, θ Sk.k k ), (θ θ, (λx. θ x ) (λx. θ x ))} is a bisimulation up to context.

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 the following small-step notion. Definition 8. A relation R on terms is a small-step 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 bisimulation up to context if both R and R -1 are small-step simulations up to context.

Similarly, we can define the refined variant. Again, it is easy to check the validity of these two proof techniques. Lemma 9. If R is a small-step bisimulation up to context, then R is a bisimulation. If R is a refined small-step bisimulation up to context, then R is a refined bisimulation.

In the next section we show how these relations can be used (Proposition 5).


H Failache

L Amy

S Villalba

L Lenci

A Laliotis

A Lezama

Spectroscopy of atoms confined to micrometric pores in glass

We present two-photon spectroscopy of rubidium vapor contained in the interstitial cavities of porous glass. We report on the first observation of Rydberg atoms under 3D spatial confinement in these micrometric size dielectric cavities.

Introduction

With the initial motivation of studying atomic vapors under a 3D spatial confinement, during the last few years we have been studying atomic spectroscopy of alkali atoms in the micrometric interstices of porous glass. Porous glass is a highly scattering medium for light which can appear as detrimental for many applications. However, randomness and disorder could be sometimes a welcome property for some applications as random lasers or alignment insensitive spectroscopical references [START_REF] Villalba | Sub-Doppler resonances in the backscattered light from random porous media infused with Rb vapor[END_REF].

The light field interacting with atoms contained in pores deep inside the sample has a speckle structure in which the polarization, amplitude and phase have rapid fluctuations over distances of the order of one wavelength. Due to the atomic thermal velocity, an atom explores large variations of the light field during its interaction time with the light. As a consequence of this motion induced field averaging, coherence effects are difficult to observe in the porous samples while unusual spectral lineshapes are observed for incoherent processes.

The transmission spectrum of Rb contained in the porous glass is unusual since for low enough atomic density and low confinement, the expected Rb absorption lines are highly suppressed. This is a consequence of the diffusive propagation of light that makes indistinguishable the detection of photons directly coming from the laser from those emitted as fluorescence. However, when the atomic vapor is spatially confined, the probability for an excited atom to collide with the dielectric surface and decay non-radiativelly is not negligible. Thus confinement favors a non-radiative de-excitation channel that restores the absorption lines in the transmission spectrum [START_REF] Villalba | Rb optical resonance in a random porous medium[END_REF]. Moreover, at higher atomic densities, radiation trapping increases the probability to excite an atom close to a surface and consequently the probability for non-radiative de-excitation.

Different spectral structures are observed in the light back-scattered by the porous sample in the direction of the incident laser beam. Sub-Doppler saturated absorption resonances are observed. In this configuration the incoming beam saturates the atomic medium and the back-scattered field acts as a probe field. The sub-Doppler resonances width are essentially determined by the probe wave-vector dispersion which is mainly determined by detection solid angle [START_REF] Villalba | Sub-Doppler resonances in the backscattered light from random porous media infused with Rb vapor[END_REF]. This experiment shows that, as would be expected, for the pores close to the incidence surface the light field has not a diffuse nature but partially preserves the direction of propagation as well as its polarization and phase [4].

Unusual spectral shapes were also observed in pump-probe spectroscopy performed with two different lasers (tuned around the D1 transitions of Rb) that are essentially due to the diffusive nature of light fields. A simple model neglecting coherent effects and considering completely randomized wave-vectors satisfactorily reproduce the full variety of lineshapes observed [START_REF] Villalba | Nonlinear atomic spectroscopy inside a random porous medium[END_REF].

Highly excited energy levels

Using two-photon excitation, one can reach atomic states whose lifetime exceeds the mean time of flight of atoms in the pores. The level 5D 3/2 of Rb (mean lifetime of around 240 ns) was excited using a probe laser resonant with the D2 line (780 nm) and a second coupling laser at 776 nm resonant with the transition 5P 3/2 → 5D 3/2 . The 5D level can decay through the 6P 1/2 level resulting in blue fluorescence at 420 nm (Fig. 1.c). We have detected the blue fluorescence through the porous medium as a measurement of the population of the 5D level. Typical spectra are shown in Fig. 1.a. obtained by scanning the frequency of the probe laser (D2), for different frequencies of the coupling laser. Notice that when the coupling laser is resonant, the predicted spectra is narrower than the Doppler width. However, for a detuned coupling laser, the shape of these spectra has two remarkable properties, a flat top and symmetry around resonance.

The symmetry of the spectra can be explained if the contribution of coherent effects are neglected in the two-photon absorption since this results in spectral profiles centred on the atomic transition. Neglecting the coherence contribution is consistent with the phase randomization of the two fields. The flat top of the spectra is also a consequence of the diffuse nature of the optical fields. Satisfactory predictions of the measured spectra shapes (Fig. 1.b) is obtained with a simplified model based on the assumptions of two-step (incoherent) two-photon excitation and isotropic distribution of the wave-vectors of the two laser fields.

It is worth mentioning that when the pore dimensions are reduced to about 10 µm, introducing then a spatial confinement that limits the mean time of flight of atoms to around 50 ns, much shorter than 5D level lifetime, no significant modifications of the spectral shapes were observed in comparison with samples with larger pores ( ∼ 100µm). This is in contrast with the observation in thin cells with with 1D confinement and light beams propagating perpendicular to the cell windows where a narrowing of the fluorescence spectrum was observed as a consequence of the spatial confinement. For 1D confinement, the contribution of resonant atoms flying nearly parallel to the windows is favored over those that have large velocities in the direction perpendicular to the windows and consequently a short time of flight [START_REF] Sarkisyan | Sub-Doppler spectroscopy by sub-micron thin Cs vapor layer[END_REF]. We interpret the non observation of such narrowing in the porous material as resulting from the 3D confinement in which the time of flight is mainly determined by the mean velocity modulus which is only loosely selected by the laser frequency (except for very large detunings).

Rydberg atoms under 3D confinement

We are currently exploring the excitation of Rb Rydberg atoms under a 3D confinement in micrometric pores in glass. 1D and 2D confined Rydberg atoms were previously studied in thin cells [START_REF] Kübler | Coherent excitation of Rydberg atoms in micrometre-sized atomic vapour cells[END_REF] and in hollow fibers [START_REF] Epple | Rydberg atoms in hollow-core photonic crystal fibres[END_REF]. In our experiment we excite Rydberg atoms using a probe laser resonant with the D1 transition of Rb, and a second coupling laser at around 476 nm that can excite nS and nD 3/2 levels with principal quantum numbers n ranging from 30 to 40. Both lasers are superposed and focalized to a spot of 50 µm in diameter at the porous medium surface, and the backscattered light of the probe field is detected with a photodiode. The probe backscattered light was recorded scanning the coupling laser while keeping the probe laser locked to the D1 transition. Two different porous media were used having 100 µm and 10 µm pore sizes approximately. The atomic density was approximately 10 14 atomes/cm 3 . Some spectra are shown at Fig. 2. The spectra recorded for 100µm pores (Fig. 2.a,b) have a Doppler width most probably due to the diffuse nature of light. However they have a clear asymmetry that suggest that they are also broadened by the Casimir-Polder interaction of the atoms with the dielectric walls of the pores [START_REF] Kübler | Coherent excitation of Rydberg atoms in micrometre-sized atomic vapour cells[END_REF]. This interaction is usually attractive (when it is not a resonant interaction [START_REF] Failache | Resonant van der Waals repulsion between excited Cs atoms and sapphire surface[END_REF]), introducing then a shift in the atomic level to lower frequencies. This suggestion is consistent with the measurement performed for the Rydberg atoms confined to 10µm cavities. The spectrum shown in Fig. 2.c for the same Rydberg level as in Fig. 2.b has an important increase in the red wing of the spectra. Also shown in Fig- 2.b,c is a fit with a theoretical model using the coefficient of a Casimir-Polder atom-surface interaction as the only free parameter. The model predicts a potential corresponding to a 32 D 3/2 level shift of 4 MHz at 10 µm distance, a value consistent with a non-resonant interaction. The level dependent interaction is evidenced by comparing spectra Fig. 2.c-d. Further work is underway.

ȞȞR--*+]-

Fig. 1 .

 1 Fig. 1. (Color online) a) Measured spectra scanning the probe laser (D2) around the transition 85 Rb(F=2 → F') at different frequencies for the coupling laser in 100 µm pores. b) Simplified model for the same conditions as a), (not considering the full hyperfine structure of level 5P 3/2 ). The dashed curve is a Gaussian with Doppler width for comparison.

Fig. 2 .

 2 Fig. 2. (Color online) Registered spectra for 100µm pores (a,b), for 10µm pores (c,d) and for different Rydberg levels 33 D 3/2 (a), 32 D 3/2 (b),(c) and 31 D 3/2 (d). The frequency axis is centered at the resonance frequency of the corresponding level (provided by an external reference). Continuous line: theoretical model.