BRICS

Basic Research in Computer Science

A Complete, Co-Inductive Syntactic Theory of Sequential Control and State

Kristian Støvring Søren B. Lassen BRICS Report Series RS-07-4 ISSN 0909-0878 February 2007 BRICS RS-07-4 Støvring & Lassen: A Complete, Co-Inductive Syntactic Theory of Sequential Control and State Copyright \begin{matrix}c \\ ◯ \end{matrix} 2007, Kristian Støvring & Søren B. Lassen.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus IT-parken, Aabogade 34 DK–8200 Aarhus N Denmark

Telephone: +45 8942 9300
Telefax: +45 8942 5601
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/07/4/

A Complete, Co-Inductive Syntactic Theory of Sequential Control and State

Kristian Støvring Department of Computer Science

University of Aarhus

         kss@brics.dk

Soren B. Lassen Google, Inc.

                                 soren@google.com

February 8, 2007

Abstract

We present a new co-inductive syntactic theory, eager normal form bisimilarity, for the untyped call-by-value lambda calculus extended with continuations and mutable references.

We demonstrate that the associated bisimulation proof principle is easy to use and that it is a powerful tool for proving equivalences between recursive imperative higher-order programs.

The theory is modular in the sense that eager normal form bisimilarity for each of the calculi extended with continuations and/or mutable references is a fully abstract extension of eager normal form bisimilarity for its sub-calculi. For each calculus, we prove that eager normal form bisimilarity is a congruence and is sound with respect to contextual equivalence. Furthermore, for the calculus with both continuations and mutable references, we show that eager normal form bisimilarity is complete: it coincides with contextual equivalence.

1 Introduction

Program equivalence is a fundamental concept in programming language semantics, and new and better frameworks and techniques for reasoning about program equivalence are continually being developed. Nonetheless, there are still no general and easy to use methods that capture the features and subtleties of actual programs in languages that combine general recursion, higherorder functions and objects, mutable state, and non-local control flow.

Denotational semantics and domain theory cover many programming language features but straightforward models fail to capture certain important aspects of program equivalence, especially concerning mutable state. The solutions to these “full abstraction” problems, including game semantics, are complex.

Syntactic reduction calculi and equational theories are easy to use but they exclude many important program equivalences.

The broadest notion of program equivalence is Morris-style contextual equivalence which equates two terms if they behave the same in all program contexts. The quantification over all program contexts makes it impractical to use the definition directly to prove programs contextually equivalent.

Syntactic methods based on operational semantics—context lemmas, applicative bisimulation, and operationally-based logical relations—generally incur modest “mathematical overhead” and are easy to use for certain classes of program equivalences. For instance, applicative bisimulation is very useful for proving the equivalence of programs that output infinite data structures. However, all these proof principles are weak for program equivalences involving general higher-order functions because, somewhat like the definition of contextual equivalence, they involve universal quantifications over all continuations, stores, and/or function arguments.

For example, fixed-point combinators are higher-order functions that make essential use of higher-order arguments. What does it take to prove the equivalence of two different fixed-point combinators? A proof obligation that involves a universal quantification over all possible arguments to the fixed-point combinators is about as difficult as proving that the fixed-point combinators are contextually equivalent from first principles.

This example is easily solved using a different class of syntactic theories which originate from the theories of Böhm tree equivalence and Lévy–Longo tree equivalence. They can be presented as bisimulation theories, called normal form bisimulation (originally introduced by Sangiorgi under the name “open applicative bisimulation”), without explicit reference to trees. Normal form bisimulation is based on symbolic evaluation of open terms to normal forms. It does not involve any universal quantification over function arguments and is therefore, in some respects, a more powerful proof principle for proving equivalences between recursive higher-order functions than other operationally-based syntactic methods. However, normal form bisimulation has only been developed for state-less λ-calculi and is, in general, not fully abstract.

In this article we address these shortcomings by extending eager normal form bisimulation, a variant of normal form bisimulation for the call-by-value λ-calculus. We present new syntactic bisimulation theories for the untyped call-by-value λ-calculus extended with continuations and mutable references.

1. The theories all extend eager normal form (enf) bisimulation for the pure call-by-value λ-calculus [19].

2. The extension with continuations, namely an untyped call-by-value version of Parigot’s λμ-calculus [26], is based on the second author’s normal form bisimulation theory for the untyped λμ-calculus [21].

3. The extension with mutable references, which we call the λρ-calculus (essentially Felleisen and Hieb’s λ-calculus with state [8]; their “ρapplication” is a primitive in our calculus hence we name it “λρ”), is based on bisimulations as sets of relations. This idea of “relation-sets bisimulation” is adapted from bisimulation theories for imperative calculi [13, 16] and existential types [32].

4. Finally, we extend the theories to a combined λμρ-calculus.

The resulting bisimulation proof principle for proving semantical equivalences between terms inherits the best properties of normal form bisimulation and relation-sets bisimulation, namely

• like other kinds of normal form bisimulation, the enf bisimulation proof obligations for continuations and mutable references require no universal quantifications over function arguments or continuations or stores, and

• the relation-set structure represents the “possible worlds” necessary to capture the behaviour of mutable references.

We demonstrate the power and ease of use of the resulting enf bisimulation proof principle for continuations and mutable references by proving the correctness of Friedman and Haynes’s encoding of call/cc in terms of “one-shot” continuations [9]. Despite the subtlety of their encoding and the mix of higherorder functions, first-class continuations, and mutable references, the bisimulation proof is remarkably straightforward, as we hope the reader will appreciate.

The enf bisimulation theories for the pure λ-calculus and the extensions with continuations and/or mutable references are modular: enf bisimilarity for each of the extended calculi is a fully abstract extension of enf bisimilarity for its sub-calculi. This is similar to the relationship between Felleisen and Hieb’s syntactic theories for control and state [8] but contrasts the situation for contextual equivalence because each language extension makes contextual equivalence more discriminative on terms of the sub-calculi.

One of the main technical contributions of the work behind this article is a proof that enf bisimilarity for the calculus extended with continuations and/or mutable references is a congruence. As an immediate consequence of congruence, enf bisimilarity is included in contextual equivalence for each calculus. For the pure λ-calculus as well as the two extensions with only continuations and only mutable references, enf bisimilarity is strictly smaller than contextual equivalence, that is, enf bisimulation is a sound but incomplete method for proving contextual equivalence. However, for the full calculus with both continuations and mutable references, we prove that enf bisimilarity is fully abstract in the sense that it coincides with contextual equivalence.

In summary, we present a complete, co-inductive syntactic theory for a calculus with higher-order functions, continuations, and mutable references, and we demonstrate the power and ease-of-use of the bisimulation proof method for proving equivalences between recursive programs.

Our results provide further illustration of the promise of normal form bisimulation as a basis for syntactic theories and proof principles, demonstrated by earlier results for other pure and extended λ-calculi in the literature (Sangiorgi [31] and Lassen [18, 20, 21]). However, we note one caveat: Although our theory for the combined λμρ-calculus captures key functional and imperative aspects of the programming language Scheme, it lacks constants such as nil, cons, numerals, and arithmetic operators. These constants need to be encoded in our calculus, e.g., using standard λ-calculus encodings [4], but such encodings are in general not faithful to the constants’ equational properties. For instance, addition of values should be commutative, up to contextual equivalence—that is, the representations of the Scheme terms (lambda (x y) (+ x y)) and (lambda (x y) (+ y x)) in the λμρ-calculus should be equivalent— but this fails for encodings of arithmetic in the λμρ-calculus, hence the resulting proof principles are only sound, not complete. There does not seem to be a satisfactory direct definition of normal form bisimulation (or Böhm-tree equivalence) for untyped calculi with constants. In future joint work with Paul Blain Levy we plan, instead, to address this shortcoming in extensions of normal form bisimulation to typed calculi with recursive types. This work is related to recent game models by Levy [22].

1.1 Related work

There exists a large body of work on syntactic theories and semantic models (domains and games) for λ-calculi with continuations and mutable references.

We only survey a few works on syntactic theories most closely related to the results in this article.

As mentioned in the introduction, our results build directly on recent work on normal form bisimulation for call-by-value [19] and the λμ-calculus [21] and on relation-sets bisimulation for existential types [32] and untyped imperative λ-calculus [13, 16].

One particular inspiration for the work presented in this article is the seminal research by Felleisen et al. on syntactic theories for sequential control and state [8]. The calculi in op.cit. are enriched with constants and δ-reduction but otherwise the state calculus is essentially what we call the λρ-calculus in this article. The control calculus differs from the λμ-calculus but they are comparable. (Their relationship is analyzed by de Groote [12] and by Ariola and Herbelin [3]. We found that it was easiest to define eager reduction on open terms, enfs, and enf bisimilarity for the λμ-calculus.) The syntactic theories of successive λ-calculus extensions by Felleisen et al. [8] are modular (conservative extensions), like our syntactic theories. An important difference is that the syntactic theories in op.cit. are inductive in the sense that all equations are derived inductively from equational axioms and inference rules, whereas our bisimulation theories are co-inductive and therefore equate many more programs.

Another body of related work is Mason and Talcott’s CIU (“closed instantiations of uses”) characterizations of contextual equivalence for functional languages with mutable references and continuations [23, 33]. (The context lemmas for the λμ-calculus by Bierman [5] and by David and Py [6] are essentially CIU characterizations.) The CIU equivalences are complete syntactic theories but the resulting proof methods are in many cases weaker than normal form bisimulation.

Most co-inductive syntactic programming language theories in the literature are variants and extensions of Abramsky’s applicative bisimulation [1]. However, there are no fully abstract applicative bisimulation theories for general λ-calculi with continuations and/or mutable references.

Ritter and Pitts [30] define a form of applicative bisimilarity for a functional language with mutable references. It is sound but not complete. In fact, it does not equate many of the well-known, subtle contextual equivalences between programs with state [25].

Wand and Sullivan [34] define a CPS language with mutable references and show that applicative bisimilarity is both sound and complete. They use the CPS language as a semantic meta-language and CPS translate a source language with state into the CPS language. But they do not give an independent characterization of the induced syntactic theory on source terms via the CPS transform.

Koutavas and Wand’s relation-sets bisimulation theory [13] is complete for a general “direct-style” imperative calculus. However, it involves a universal quantification over closed function arguments, unlike our normal form bisimulation theories.

Merro and Biasi [24] present a complete bisimulation theory for a CPS calculus. It can be viewed as a kind of applicative bisimulation, presented as a labelled transition system in the style of Gordon [10], and also leads to a context lemma.

Pitts and Stark [28, 29] develop syntactic theories based on operationallybased logical relations that address many of the subtleties of contextual equivalences between programs with mutable references. The relation-sets bisimulation theories for mutable state, in general, are alternative approaches with a very different meta-theory. For logical relations the key proof obligation is existence, whereas the key proof obligation for the bisimulation theories is congruence.

Finally, we note that the modularity of the enf bisimilarity theories for control and state resembles the modularity of game semantics for control and state [2, 14].

2 Eager normal form bisimulation

Let us briefly reintroduce the definition of enf bisimulation for the pure callby-value λ-calculus [19]. Consider a variant of the call-by-value λ-calculus in which computations must be explicitly sequenced by means of a let-construct:

Variables x, y, z

Values v ::= x | λx. t

Terms t ::= v | let x=t_{1} in t_{2} | v_{1} v_{2}

We identify terms up to renaming of bound variables.

Reduction is defined by means of evaluation contexts:

Evaluation contexts E ::= [ ] | E[let x=[ ] in t]

Eager normal forms (enfs) e ::= v | E[x v]

(R1) E[let x=v in t] ↦ E[t[v/x]]

(R2) E[(λx. t) v] ↦ E[t[v/x]]

The reflexive-transitive closure of the reduction relation ↦ is written ↦^{∗}. For every term t, there are two possibilities: either t diverges in the sense that there is an infinite reduction sequence starting from t, or else t converges in the sense that t ↦^{∗} e for some (unique) eager normal form e. The notation t ↦^{ω} means that t diverges. Eager normal forms are truly normal forms with respect to reduction: they do not reduce to anything.

For a syntactic phrase ϕ, let fv(ϕ) denote the set of free variables of ϕ (the formal definitions are omitted).

Definition 1. A binary relation S on terms is an enf bisimulation if S ⊆ B(S), where

B(S) = \{(t, t′)|\begin{matrix}either t ↦^{ω} and t′ ↦^{ω}, \\ or t ↦^{∗} e and t′ ↦^{∗} e′ where (e, e′) ∈ M(S)\} \end{matrix}
M(S) = {(v, v′) | (v, v′) ∈ V (S)}

∪ \{(E[x v], E′[x v′]) | \begin{matrix}(E, E′) ∈ K(S) & \\ (v, v′) ∈ V (S)\} \end{matrix}

V (S) = \{(x, x)\} ∪ \{(v, v′) | \begin{matrix}∃y ∉ fv(v) ∪ fv(v′). \\ (v ⋆ y, v′ ⋆ y) ∈ S\} \end{matrix}
K(S) = \{([ ], [ ])\} ∪ \{(E, E′) | \begin{matrix}∃y ∉ fv(E) ∪ fv(E′). \\ (E ⋆ y, E′ ⋆ y) ∈ S\} \end{matrix}

with x ⋆ y = x y, (λy. t) ⋆ x = t[x/y], [ ] ⋆ y = y, and E[let y=[ ] in t] ⋆ x = E[t[x/y]].

The intuition behind enf bisimulation is that two related open terms either (1) both diverge, or (2) reduce to matching eager normal forms whose components are again related. As an example, define the Curry call-by-value fixed-point combinator Y_{v}:

Ψ[f] = λg. f (λx. let z=g g in z x)
Y_{v} = λf. Ψ[f] Ψ[f]

and the Turing call-by-value fixed-point combinator Θ_{v}:

Ξ = λg.λf.f (λx. let z_{1}=g g in let z_{2}=z_{1} f in z_{2} x)
Θ_{v} = Ξ Ξ.

These two fixed-point combinators are enf bisimilar, i.e., there exists an enf bisimulation S such that (Y_{v}, Θ_{v}) ∈ S [19]. We invite the reader to try to prove this equivalence by constructing such an S: one starts with the singleton {(Y_{v}, Θ_{v})} and then iteratively adds pairs in order to satisfy the definition of an enf bisimulation above. (In Section 5, a similar, but more complicated, equivalence between Y_{v} and a store-based fixed-point combinator is shown.) Remark. The following construction, derived from the Turing call-by-value fixed-point combinator, is convenient for defining functions by recursion: For all values v, v_{1}, and v_{2}, define

D[v_{1}, v_{2}] = let z_{1}=Θ_{v} in let z_{2}=z_{1} v_{1} in z_{2} v_{2}
fix[v] = λx.D[v, x]

Then fix[v] x ↦^{∗} let z=v fix[v] in z x.

Contextual equivalence is defined in the standard way. Informally, two terms t and t′ are contextually equivalent if for every many-holed term context C[ ] such that C[t] and C[t′] are closed terms, C[t] converges if and only if C[t′] converges.

Theorem 2 ([19]). If (t, t′) ∈ S for some enf bisimulation S, then t and t′ are contextually equivalent.

Remark. The definition of an enf bisimulation is slightly different from the one in the original presentation [19]. In particular, the variant defined here is equivalent to what is called an enf bisimulation up to η in the original presentation.

In the sequel we omit the “enf” qualifier for bisimulations and instead qualify them by calculi. We will refer to the bisimulations for the pure λ-calculus in Definition 1 as “λ-bisimulations”.

3 The λμ-calculus

We now extend enf bisimulation to the λμ-calculus. This extension is new, but based on head normal form bisimulation for the λμ-calculus [21].

Variables x, y, z

Names a, b

Values v ::= x | λx. t

Named terms nt ::= [a]t

Terms t ::= v | let x=t_{1} in t_{2} | v_{1} v_{2} | μa. nt

We identify syntactic phrases up to renaming of bound variables and names. For a syntactic phrase ϕ, let fn(ϕ) denote the set of free names of ϕ.

Names in the λμ-calculus represent continuations. Names are not firstclass, but we will represent a name a as the first-class value â = λx. μb. [a]x. The familiar call/cc control operator can be encoded in the λμ-calculus as

call/cc = λf. μa. [a]f â.

The operational semantics of the λμ-calculus is defined by a reduction relation on named terms:

Named eval. contexts NE ::= [a][ ] | NE[let x=[ ] in t]

Named enfs ne ::= [a]v | NE[x v]

(Rμ1) NE[let x=v in t] ↦ NE[t[v/x]] (Rμ2) NE[(λx. t) v] ↦ NE[t[v/x]]

(Rμ3) NE[μa. nt] ↦ nt[NE/a]

Here ϕ[NE/a] denotes capture-avoiding substitution of named evaluation contexts for names: for example, if b ∉ fn(NE), then (μb. [a]t)[NE/a] = μb. NE[t].

Definition 3. A binary relation S on named λμ-terms is a λμ-bisimulation if S ⊆ B_{μ}(S), where

B_{μ}(S) = \{(nt, nt′) | \begin{matrix}either nt ↦^{ω} and nt′ ↦^{ω}, \\ or nt ↦^{∗} ne and nt′ ↦^{∗} ne′ \\ where (ne, ne′) ∈ M_{μ}(S)\} \end{matrix}

M_{μ}(S) = {([a]v, [a]v′) | (v, v′) ∈ V_{μ}(S)}

∪ \{(NE[x v], NE′[x v′]) | \begin{matrix}(NE, NE′) ∈ K_{μ}(S) & \\ (v, v′) ∈ V_{μ}(S)\} \end{matrix}

V_{μ}(S) = {(x, x)}

∪ \{(v, v′) | \begin{matrix}∃y ∉ fv(v) ∪ fv(v′). \\ (v ⋆ y, v′ ⋆ y) ∈ T_{μ}(S)\} \end{matrix}

K_{μ}(S) = {([a][ ], [a][ ])}

∪ \{(NE, NE′) | \begin{matrix}∃y ∉ fv(NE) ∪ fv(NE′). \\ (NE ⋆ y, NE′ ⋆ y) ∈ T_{μ}(S)\} \end{matrix}

T_{μ}(S) = \{(t, t′) | \begin{matrix}∃a ∉ fn(t) ∪ fn(t′). \\ ([a]t, [a]t′) ∈ S\} \end{matrix}

with [a][ ] ⋆ y = [a]y and NE[let x=[ ] in t] ⋆ y = NE[t[y/x]].

Definition 4. Say that t and t′ are λμ-bisimilar, written t ≂_{μ} t′, if there exists a λμ-bisimulation S such that (t, t′) ∈ T_{μ}(S).

We show in Section 10 that λμ-bisimilar terms are contextually equivalent. Recall that â = λx. μb. [a]x. To illustrate λμ-bisimilarity we define the

term ψ = fix[P], where

P = λf. λx. μa. [a] let y=x â in f y.

The term ψ takes a function x as argument and applies x to successive arguments

x â_{1} â_{2} …

until x applies one of the â_{i} to an argument v, in which case v is returned as the result of ψ x. On the other hand, ψ x diverges if x never applies any of its arguments, e.g., if x = λy. Ω or x = fix[λf. λy. f].

Remark. A term with the behavior of ψ cannot be expressed in the pure callby-value λ-calculus. To see this, consider the two functions

v = λy. let z=y y in Ω and v′ = λy. Ω.

where Ω = (λx.x x)(λx.x x). They are contextually equivalent in the pure call-by-value λ-calculus. (This can be established using the operational extensionality property of the pure call-by-value λ-calculus [7, 27], because the term let z=v_{0} v_{0} in Ω diverges if v_{0} is any closed pure value.) But ψ can tell them apart: ψ v converges while ψ v′ diverges.

A potential optimization of ψ is the following variant ψ′ which returns straight to its final “return address” when x applies an argument (rather than returning from all the recursive invocations of the recursive function): ψ′ = λx. μa. [a] fix[P′] x, where

P′ = λf. λx. let y=x â in f y

The optimization is correct up to enf bisimilarity, that is, ψ ≂_{μ} ψ′, because

S = {([a]ψ, [a]ψ′), ([a]D[P, x], [a]μa. [a]fix[P′] x),
([b]μb. [a]x, μb. [a]x), ([a]fix[P] y, [a]fix[P′] y)}

is a λμ-bisimulation.

4 The λρ-calculus

The λρ-calculus is obtained from the pure call-by-value λ-calculus by adding constructs for allocating a number of new reference cells, for storing a value in a reference cell, and for fetching the value from a reference cell.

Variables x, y, z

References ı, ȷ

Values v ::= x | λx. t

Terms t ::= v | let x=t_{1} in t_{2} | v_{1} v_{2} | ρs. t | ı:=v; t | !ı

Stores s ::= {ı_{1}:=v_{1}, …, ı_{n}:=v_{n}} (ı_{1}, …, ı_{n} are distinct)

Stores are identified up to reordering, and therefore a store can be considered as a finite map from references to values. Terms are identified up to renaming of bound variables and references: in the term ρs. t, the references in the domain of s are considered bound in the range of s and in t. For a syntactic phrase ϕ, let fr(ϕ) be the set of references occurring free in ϕ. A syntactic phrase is reference-closed if it contains no free references. Write dom(s) for the domain of the store s. If s and s′ have disjoint domains, s·s′ denotes their disjoint union. If s = {ı:=v}·s′, let s(ı) = v and s[ı:=v′] = {ı:=v′}·s′.

Reduction is defined on configurations, which are pairs (s, t) of stores and terms such that fr(t) ⊆ dom(s). (Configurations are not identified up to renaming of the domains of the stores, hence a configuration (s, t) should not be thought of as a term ρs. t.)

Evaluation contexts E ::= [ ] | E[let x=[ ] in t]

Eager normal forms (enfs) e ::= v | E[x v]

(Rρ1) (s, E[let x=v in t]) ↦ (s, E[t[v/x]])

(Rρ2) (s, E[(λx. t) v]) ↦ (s, E[t[v/x]])

(Rρ3) (s, E[ρs′. t]) ↦ (s·s′, E[t]), if (dom(s) ∪ fr(s) ∪ fr(E)) ∩ dom(s′) = ∅

(Rρ4) (s, E[ı:=v; t]) ↦ (s[ı:=v], E[t]) if ı ∈ dom(s)

(Rρ5) (s, E[!ı]) ↦ (s, E[s(ı)]) if ı ∈ dom(s)

Eager normal form bisimulation for the λρ-calculus is based on the relationsets bisimulation idea [13, 16, 32]. Briefly, instead of defining a bisimulation as a single binary relation on terms, one defines a bisimulation as a set of such relations, each associated with a “world”: here, a pair of stores. The requirement is that if two terms are related in a certain world, then the eager normal forms (if any) of these two terms are related in a “future world” where the two stores may have changed. Moreover, everything that was related in the old world must still be related in the new world.

Now for the formal definitions. Let X, Y, Z range over finite sets of variables and let J range over finite sets of references. We write X·Y for the disjoint union of X and Y. When the meaning is clear from the context, we write a singleton set {x} as just x. We use the same notational conventions for finite sets of references.

Notation X, J ⊢ ϕ, ϕ′, ... means the syntactic phrases ϕ, ϕ′, ... have free variables in X and free references in J. We omit X and/or J on the left of ⊢ if it is empty.

Let R range over sets of triples (X|t, t′), more specifically subsets of Rel(Y, J, J′) for some Y, J and J′, where

\begin{matrix}Rel(Y, J, J′) = \\ \{(X|t, t′) | X ∩ Y = ∅ & X·Y, J ⊢ t & X·Y, J′ ⊢ t′\} \end{matrix}

We identify triples that differ only up to renaming of the variables from the first component X: in the triple (X|t, t′), the variables in X are considered bound in t and t’. A triple (∅|t, t′) where the first component is empty is also written (|t, t′).

A term relation tuple is a quadruple (X|s, s′, R) where X ⊢ s, s′ and R ⊆ Rel(X, dom(s), dom(s′)). We identify term relation tuples that differ only up to renaming of the variables from the first component X and up to renaming of references. Let Q range over term relation sets, that is, sets of term relation tuples.

Definition 5. Q is a λρ-bisimulation iff Q ⊆ B_{ρ}(Q), where

B_{ρ}(Q) = \{(X|s_{0}, s′_{0}, R_{0}) | for all (Y |t, t′) ∈ R_{0}, either (s_{0}, t) ↦^{ω} & (s′_{0}, t′) ↦^{ω}, or ∃s_{1}, s′_{1}, e, e′, R_{1} ⊇ R_{0}, X_{1} ⊇ X·Y. \begin{matrix}(s_{0}, t) ↦^{∗} (s_{1}, e) & (s′_{0}, t′) ↦^{∗} (s′_{1}, e′) & \\ (e, e′) ∈ M_{ρ}(R_{1}) & (X_{1}|s_{1}, s′_{1}, R_{1}) ∈ Q\} \end{matrix}

M_{ρ}(R) = \begin{cases}(v, v′), (E[x v], E′[x v′]) | \\ (v, v′) ∈ V_{ρ}(R) & (E, E′) ∈ K_{ρ}(R)\} \end{cases}
V_{ρ}(R) = {(x, x)}

∪ \{(v, v′) | \begin{matrix}∃y ∉ fv(v) ∪ fv(v′). \\ (y|v ⋆ y, v′ ⋆ y) ∈ R\} \end{matrix}

K_{ρ}(R) = {([ ], [ ])}

∪ \{(E, E′) | \begin{matrix}∃y ∉ fv(E) ∪ fv(E′). \\ (y|E ⋆ y, E′ ⋆ y) ∈ R\} \end{matrix}

Definition 6. Reference-closed λρ-terms t and t′ are λρ-bisimilar, written t ≂_{ρ} t′, iff there exists a λρ-bisimulation Q which contains a quadruple (X|{}, {}, R) with (|t, t′) ∈ R.

We show in Section 9 that λρ-bisimilarity is a congruence. Therefore, as explained in Section 10, λρ-bisimilar terms are contextually equivalent.

5 Example: imperative fixed-point combinator

It is well-known that a store that may contain functional values can be used to define functions by recursion. Abbreviate

Π[f, ı] = λx. let z_{1}=!ı in let z_{2}=f z_{1} in z_{2} x

and consider the term:

Y_{ρ} = λf. ρ{ı:=Π[f, ı]}. f Π[f, ı].

Y_{ρ} can be used to define functions by recursion in the λρ-calculus. The technique of defining recursive functions by means of a “circular store” is due to Landin [15].

We now show that the fixed-point combinator Y_{ρ} is λρ-bisimilar to the Curry call-by-value fixed-point combinator Y_{v} (defined in Section 2 above). This equivalence can be shown directly from the definition of a λρ-bisimulation, but it is more convenient to apply the following general lemma:

Lemma 7. Define ρ̂s. t = ρs. t for s ≠ {}, and ρ̂{}. t = t. Assume that there exists a λρ-bisimulation containing a tuple (X|s, s′, R) where (|t, t′) ∈ R, and let x_{1}, …, x_{n} ∈ X. Then λx_{1}… λx_{n}. ρ̂s. t ≂_{ρ} λx_{1}… λx_{n}. ρ̂s′. t′.

The lemma follows from Corollary 36 in Section 9.

Proposition 8. Y_{ρ} ≂_{ρ} Y_{v}.

Proof. By definition, Y_{ρ} = λf. ρ{ı:=Π[f, ı]}. f Π[f, ı] and Y_{v} = λf. Ψ[f] Ψ[f]. The proof therefore consists of constructing a λρ-bisimulation Q containing a tuple ({f}|{ı:=Π[f, ı]}, {}, R) where (|f Π[f, ı], Ψ[f] Ψ[f]) ∈ R, and then using Lemma 7.

Instead of specifying Q right away, we show how one would in practice construct Q: by starting from the two configurations ({ı:=Π[f, ı]}, f Π[f, ı]) and ({}, Ψ[f] Ψ[f]) and iteratively adding tuples in order to satisfy the conditions in the definition of a λρ-bisimulation. In that way, the main part of the equivalence proof consists in a number of calculations of reduction sequences.

Abbreviate D[f] = λx. let z=Ψ[f] Ψ[f] in z x. Now calculate:

({ı:=Π[f, ı]}, f Π[f, ı]) ↦^{∗} ({ı:=Π[f, ı]}, f Π[f, ı])
({}, Ψ[f] Ψ[f]) ↦^{∗} ({}, f D[f]).

The two resulting eager normal forms are f Π[f, ı] and f D[f]. The variables in function position match (both are f), so consider the arguments, Π[f, ı] and D[f]. Since

Π[f, ı] = λx. let z_{1}=!ı in let z_{2}=f z_{1} in z_{2} x

and

D[f] = λx. let z=Ψ[f] Ψ[f] in z x,

the definition of a λρ-bisimulation indicates that one should continue by reducing the bodies of these two λ-abstractions:

({ı:=Π[f, ı]}, let z_{1}=!ı in let z_{2}=f z_{1} in z_{2} x)
↦^{∗} ({ı:=Π[f, ı]}, let z_{2}=f Π[f, ı] in z_{2} x)

and

({}, let z=Ψ[f] Ψ[f] in z x) ↦^{∗}({}, let z=f D[f] in z x)
= ({}, let z_{2}=f D[f] in z_{2} x)

The resulting two eager normal forms are

let z_{2}=f Π[f, ı] in z_{2} x and let z_{2}=f D[f] in z_{2} x.

Again, the variables in function position match (both are f), and the evaluation contexts are identical (both are let z_{2}=[ ] in z_{2} x). The function arguments, Π[f, i] and D[f], are λ-abstractions, and therefore one should continue reducing the bodies of these two λ-abstractions. But this is exactly what was already done in the previous two reduction sequences.

Using the results of these calculations it is possible to construct the required bisimulation Q. First, define

R = {(|f Π[f, ı], Ψ[f] Ψ[f]),

(x| \begin{matrix}let z_{1}=!ı in let z_{2}=f z_{1} in z_{2} x, \\ let z=Ψ[f] Ψ[f] in z x)\}. \end{matrix}

Let x_{1}, x_{2}, … be distinct variables, and define, for every n ≥ 0,

S_{n} = {(z_{2}|z_{2} x_{k}, z_{2} x_{k}) | 1 ≤ k ≤ n}.

Finally, define Q as the set of all tuples

({f, x_{1}, …, x_{n}}|{ı:=Π[f, ı]}, {}, R ∪ S_{n})

where n ≥ 0. Then Q is a λρ-bisimulation, as can be verified using the calculations above.

Note that Q contains the tuple ({f}|{ı:=Π[f, ı]}, {}, R) where

(|f Π[f, ı], Ψ[f] Ψ[f]) ∈ R.

Therefore, Lemma 7 implies that Y_{ρ} ≂_{ρ} Y_{v}.

6 The λμρ-calculus

The λμρ-calculus combines the control aspects of the λμ-calculus with the state aspects of the λρ-calculus. The definition of λμρ-bisimilarity is a natural combination of the definitions of λμ-bisimilarity and of λρ-bisimilarity. However, unlike the cases for the calculi considered previously in the article, λμρ-bisimilarity is not only contained in contextual equivalence, it coincides with contextual equivalence, as will be shown in Section 10.

Variables x, y, z Names a, b References ı, ȷ Values v ::= x | λx. t Named terms nt ::= [a]t

Terms t ::= \begin{matrix}v | let x=t_{1} in t_{2} | v_{1} v_{2} | μa. nt | \\ ρs. t | ı:=v; t | !ı \end{matrix}

Stores s ::= {ı_{1}:=v_{1}, …, ı_{n}:=v_{n}} Reduction is defined on configurations, which are now pairs (s, nt) of stores and named terms such that fr(nt) ⊆ dom(s). Named eval. contexts NE ::= [a][ ] | NE[let x=[ ] in t] Named enfs ne ::= [a]v | NE[x v]

(Rμρ1) (s, NE[let x=v in t]) ↦ (s, NE[t[v/x]]) (Rμρ2) (s, NE[(λx. t) v]) ↦ (s, NE[t[v/x]]) (Rμρ3) (s, NE[μa. nt]) ↦ (s, nt[NE/a]) (Rμρ4) (s, NE[ρs′. t]) ↦ (s·s′, NE[t]),

if (dom(s) ∪ fr(s) ∪ fr(NE)) ∩ dom(s′) = ∅

(Rμρ5) (s, NE[ı:=v; t]) ↦ (s[ı:=v], NE[t]) if ı ∈ dom(s) (Rμρ6) (s, NE[!ı]) ↦ (s, NE[s(ı)]) if ı ∈ dom(s)

Now X, Y, Z range over finite sets of variables and names. Let NR range over sets of triples (X|nt, nt′), more specifically subsets of NRel(Y, J, J′) for some Y, J and J′, where

\begin{matrix}NRel(Y, J, J′) = \\ \{(X|nt, nt′) | X ∩ Y = ∅ & X·Y, J ⊢ nt & X·Y, J′ ⊢ nt′\} \end{matrix}

We identify triples that differ only up to renaming of the variables and names from the first component X.

A named term relation tuple is a quadruple (X|s, s′, NR) where X ⊢ s, s′ and NR ⊆ NRel(X, dom(s), dom(s′)). We identify named term relation tuples that differ only up to renaming of the variables and names from the first component X and up to renaming of references. A named term relation set is a set of named term relation tuples. Let NQ range over named term relations sets.

Definition 9. NQ is a λμρ-bisimulation iff NQ ⊆ B_{μρ}(NQ), where

B_{μρ}(NQ) = \{(X|s_{0}, s′_{0}, NR_{0}) | for all (Y |nt, nt′) ∈ NR_{0}, either (s_{0}, nt) ↦^{ω} & (s′_{0}, nt′) ↦^{ω}, or ∃s_{1}, s′_{1}, ne, ne′, NR_{1} ⊇ NR_{0}, X_{1} ⊇ X·Y. \begin{matrix}(s_{0}, nt) ↦^{∗} (s_{1}, ne) & \\ (s′_{0}, nt′) ↦^{∗} (s′_{1}, ne′) & \\ (ne, ne′) ∈ M_{μρ}(NR_{1}) & \\ (X_{1}|s_{1}, s′_{1}, NR_{1}) ∈ NQ\} \end{matrix}

M_{μρ}(NR) = \begin{cases}([a]v, [a]v′), (NE[x v], NE′[x v′]) | \\ (v, v′) ∈ V_{μρ}(NR) & (NE, NE′) ∈ K_{μρ}(NR)\} \end{cases}
V_{μρ}(NR) = {(x, x)}

∪ \{(v, v′) | \begin{matrix}∃y ∉ fv(v) ∪ fv(v′). \\ ∃a ∉ fn(v) ∪ fn(v′). \\ (a·y|[a](v ⋆ y), [a](v′ ⋆ y)) ∈ NR\} \end{matrix}

K_{μρ}(NR) = {([a][ ], [a][ ])}

∪ \{(NE, NE′) | \begin{matrix}∃y ∉ fv(NE) ∪ fv(NE′). \\ (y|NE ⋆ y, NE′ ⋆ y) ∈ NR\} \end{matrix}

Definition 10. Reference-closed named terms nt and nt′ are λμρ-bisimilar, written nt ≂_{μρ} nt′, iff there exists a λμρ-bisimulation NQ which contains a quadruple (X|{}, {}, NR) with (|nt, nt′) ∈ NR. Reference-closed terms t and t′ are λμρ-bisimilar, written t ≂_{μρ} t′, iff there exists a λμρ-bisimulation NQ which contains a quadruple (X|{}, {}, NR) with (t, t′) ∈ T_{μρ}(NR), where

T_{μρ}(NR) = {(t, t′) | ∃a ∉ fn(t) ∪ fn(t′). (a|[a]t, [a]t′) ∈ NR}.

We show in Section 9 that λμρ-bisimilarity is a congruence.

7 Example: one-shot continuations

As an extended example, we show the correctness of Friedman and Haynes’s encoding of call/cc in terms of “one-shot continuations” [9].

A one-shot continuation is a continuation which may be applied at most once. Friedman and Haynes showed that, perhaps surprisingly, call/cc can be encoded in terms of its restricted one-shot variant. They did this by exhibiting an “extraordinarily difficult program” [9, p.248] together with an informal equivalence argument. We confirm the correctness of this program by a formal proof using the enf bisimulation method. The equivalence proof below can be viewed as a formalization of Friedman and Haynes’s informal argument.

One cannot directly use the λμρ-calculus to prove correctness of this encoding of call/cc, since the λμρ-calculus does not contain one-shot continuations as a primitive. Instead, we define one-shot continuations in terms of unrestricted continuations using another, but simpler, construction due to Friedman and Haynes. We then show the correctness of the encoding of call/cc by means of one-shot continuations relative to this encoding of one-shot continuations.

First, we need to encode a conditional operator in the λμρ-calculus. Since the evaluation order in the λμρ-calculus is call-by-value, the encoding is done using “thunks”:

T = λx. λy. x I
F = λx. λy. y I
if[t_{1}, t_{2}, t_{3}] = let z_{1}=t_{1}in
let z_{2}=z_{1} (λz. t_{2})in
z_{2}(λz. t_{3})

where I = λx. x, and where z_{1} and z_{2} are not free in t_{1}, t_{2}, or t_{3}.

Recall the definition of call/cc:

call/cc = λf. μa. [a]f â

where â = λx. μb. [a]x. Now define the one-shot variant of call/cc:

call/cc1 = λf. (\begin{matrix}call/cc \\ (λk. ρ\{ı:=T\}. f (λx. if[!ı, (ı:=F; k x), Ω]))) \end{matrix}

The requirement that every captured continuation k is applied at most once is enforced by means of the local reference ı.

Now for the encoding of unrestricted continuations by means of one-shot continuations. For every reference ȷ, define

Φ_{ȷ} = λg. λf. let y=call/cc1 (λk. (ȷ:=k; f (λx. \begin{matrix}let y=!ȷ \\ in y x))) \end{matrix} in call/cc1 (λk′. g (λk.k′y)).

Then define

call/cc∗ = λf. ρ{ȷ:=I}. fix[Φ_{ȷ}] f.

(See the original presentation of the encoding [9] for an informal explanation of how it works.)

The aim of this section is to show that

call/cc ≂_{μρ} call/cc∗.

It follows that call/cc and call/cc∗ are contextually equivalent, and hence that call/cc∗ is as an encoding of call/cc by means of one-shot continuations.

As in Section 5, the equivalence could be shown directly from the definition of a bisimulation, but it is more convenient to use the following generalization of Lemma 7 to the λμρ-calculus:

Lemma 11. Define ρ̂s. t=ρs. t for s ≠ {}, and ρ̂{}. t = t. Assume that there exists a λμρ-bisimulation containing a tuple (X|s, s′, NR) where (|[a]t, [a]t′) ∈ NR, and let x_{1}, …, x_{n} ∈ X. If a ∈ X does not occur free in any of s, s′, t, and t′, then λx_{1}… λx_{n}. ρ̂s. t ≂_{μρ} λx_{1}… λx_{n}. ρ̂s′. t′.

The lemma follows from Corollary 36 in Section 9.

Proposition 12. call/cc ≂_{μρ} call/cc∗.

Proof. By definition,

call/cc = λf. μa. [a]f â
call/cc∗ = λf. ρ{ȷ:=I}. fix[Φ_{ȷ}] f.

We therefore construct a bisimulation containing a tuple

(f·a|{}, {ȷ:=I}, NR)

where (|[a]μa. [a]f â, [a]fix[Φ_{ȷ}] f) ∈ NR. The conclusion then follows from Lemma 11.

The main part of the proof consists in a number of calculations of reduction sequences. One starts from the two configurations ({}, [a]μa. [a]f â) and ({ȷ:=I}, [a]fix[Φ_{ȷ}] f) and iteratively tries to add tuples in order to satisfy the conditions in the definition of a λμρ-bisimulation.

First, define the named evaluation context

NE_{0} = [a] let x=[ ] in call/cc1 (λk′. fix[Φ_{ȷ}] (λk.k′x))

and for every reference ı, define the term

C[ı] = λx. if[!ı, (ı:=F; (λx. μb. NE_{0}[x]) x), Ω].

Now calculate, for any store s and any value v:

(1) (s·{ȷ:=v}, [a]fix[Φ_{ȷ}] f)

↦^{∗}

(s·{ȷ:=C[ı], ı:=T}, NE_{0}[f (λx. let y=!ȷ in y x)]).

(2) (s·{ȷ:=C[ı], ı:=T}, [b] let y=!ȷ in y x)

↦^{∗}

(s·{ȷ:=C[ı], ı:=F}, [a]call/cc1 (λk′. fix[Φ_{ȷ}] (λk.k′x))).

(3) (s·{ȷ:=C[ı]}, [a]call/cc1 (λk′. fix[Φ_{ȷ}] (λk.k′x)))

↦^{∗}

(s·{ȷ:=C[ı′], ı_{0}:=F, ı′:=T}, [a]x).

These calculations dictate the following construction of a λμρ-bisimulation: let

NR_{0} =\begin{cases}(|[a]μa. [a]f â, [a]fix[Φ_{ȷ}] f), \\ (y | [a]y, [a]call/cc1 (λk′. fix[Φ_{ȷ}] (λk.k′y))), \\ (y·b | [b]μb.[a]y, [b] let z=!ȷ in z y)\} \end{cases}

and let NQ consist of the tuple

(f·a|{}, {ȷ:=I}, {(|[a]μa. [a]f â, [a]fix[Φ_{ȷ}] f)})

together with all named term relation tuples of the form

(X|{}, s, NR_{0})

where {f, a} ⊆ X, where s is a store such that ȷ ∈ dom(s), and where there exists an ı ∈ dom(s) such that

s(ȷ) = C[ı] and s(ı) = T.

Then NQ is a λμρ-bisimulation, as can be verified using the calculations (1)-(3) above. By Lemma 11, call/cc ≂_{μρ} call/cc∗.

8 Enf bisimulation for terms with free references

So far in this article, eager normal form bisimulation has been used as a proof principle for proving equivalence of reference-closed terms. In this section it is shown how to extend eager normal form bisimulation to terms which may contain free references. Besides allowing one to prove equivalences about terms with free references, this extension is also used in the congruence proof for enf bisimilarity in Section 9. As a part of that proof, it must be shown that the following holds: If t ≂_{μρ} t′ and v ≂_{μρ} v′, then ρ{ı:=v}. t ≂_{μρ} ρ{ı:=v′}. t′ and ı:=v; t ≂_{μρ} ı:=v′; t′. Here the reference ı will in general occur free in the terms t, t′, v, and v′, and, of course, in the terms ı:=v; t and ı:=v′; t′.

The modification needed to take free references into account can be explained as follows. Suppose that the free references of the terms t and t′ are contained in J, and that one wants to prove that t and t′ are equivalent. According to the previous definition, one requirement is that [a]t and [a]t′ should either both diverge, or reduce to matching named eager normal forms. But one cannot reduce [a]t and [a]t′ without providing values for the references in J, i.e., the references which are free in t and t′. The solution is to initialize the references in J with a number of fresh variables z_{ȷ}^{ȷ∈J}. This initialization takes care of the “input” aspect of the free references; the “output” aspect is taken care of by an extra requirement: if both ({ȷ :=z_{ȷ}^{ȷ∈J}}, [a]t) and ({ȷ :=z_{ȷ}^{ȷ∈J}}, [a]t′) reduce to named eager normal forms, then in the two resulting stores, the references from J must contain values which are pairwise related.

Now for the formal definitions. Named term relation sets are generalized as follows: let

NU_{J} = {(X|s, s′, NR) | X, J ⊢ s, s′ & NR ⊆ NRel(X, J·dom(s), J·dom(s′))}.

We identify quadruples that differ only up to renaming of the variables and names from the first component X and up to renaming of references from dom(s) and dom(s′). Notice that NU_{∅} = NU.

Definition 13. NQ ⊆ NU_{J} is a J-bisimulation iff NQ ⊆ B_{J}(NQ), where

B_{J}(NQ) =
{(X|s_{0}, s′_{0}, NR_{0}) ∈ NU_{J} | for all distinct variables z_{ı}^{ı∈J} and all (Y |nt, nt′) ∈ NR_{0}, either ({ı:=z_{ı}^{ı∈J}}·s_{0}, nt) ↦^{ω} & ({ı:=z_{ı}^{ı∈J}}·s′_{0}, nt′) ↦^{ω}, or ∃ne, ne′, (v_{ı}, v′_{ı})^{ı∈J}, s_{1}, s′_{1}, NR_{1} ⊇ NR_{0}, X_{1} ⊇ X·Y ·z_{ı}^{ı∈J}. ({ı:=z_{ı}^{ı∈J}}·s_{0}, nt) ↦^{∗} ({ı:=v_{ı}^{ı∈J}}·s_{1}, ne) & ({ı:=z_{ı}^{ı∈J}}·s′_{0}, nt′) ↦^{∗} ({ı:=v′_{ı}^{ı∈J}}·s′_{1}, ne′) & (ne, ne′) ∈ M_{μρ}(NR_{1}) & ∀ı ∈ J. (v_{ı}, v′_{ı}) ∈ V_{μρ}(NR_{1}) & (X_{1}|s_{1}, s′_{1}, NR_{1}) ∈ NQ}

Say that two terms t and t′ are J-bisimilar if there exists a J-bisimulation containing a tuple (X|{}, {}, NR) where (t, t′) ∈ T_{μρ}(NR).

We now generalize the previously given definition of enf bisimilarity for reference-closed terms:

Definition 14. Let t and t′ be λμρ-terms. Say that t and t′ are λμρ-bisimilar, written t ≂_{μρ} t′, if there exists a finite set J of references such that t and t′ are J-bisimilar.

Example 15. It is easy to show that

let z=!ȷ in (ȷ:=I; ȷ:=z; f x) ≂_{μρ} f x

while on the other hand

let z=!ȷ in (ȷ:=I; let y=f x in (ȷ:=z; y)) ≂̸_{μρ} f x.

The proofs of this equivalence and this non-equivalence illustrate a basic sequentiality property of the calculi considered in this article: in order for two terms to be equivalent, it is enough that the contents of the free references are equivalent at certain “synchronization points”, but in-between these points the contents of the free references can be modified arbitrarily.

Proposition 16. Let J_{0} and J be finite sets of references such that J_{0} ⊆ J. Any two terms which are J_{0}-bisimilar are also J-bisimilar.

9 Congruence

This section contains an outline of the proof that λμρ-bisimilarity is a congruence: it is an equivalence relation which is furthermore compatible. A binary relation S on terms and named terms of the λμρ-calculus is compatible if it is closed under the term formation rules of the λμρ-calculus. For example, if t_{1} S t′_{1} and t_{2} S t′_{2}, then also (let x=t_{1} in t_{2}) S (let x=t′_{1} in t′_{2}), and if nt S nt′, then μa. nt S μa. nt′. The straightforward formal definition is omitted.

Proposition 17. For every finite set J of references, there exists a greatest J-bisimulation B_{J}.

Proof. The definition of B_{J} immediately implies that the union of an arbitrary family of J-bisimulations is also a J-bisimulation. In particular, the union of all J-bisimulations is the greatest J-bisimulation.

At this point it is useful to change the definitions of a λμρ-bisimulation and of a J-bisimulation slightly: in those definitions, replace the operators V_{μρ} and K_{μρ} with V′_{μρ} and K′_{μρ}:

V′_{μρ}(NR) = \{(v, v′) | \begin{matrix}∃y ∉ fv(v) ∪ fv(v′). \\ ∃a ∉ fn(v) ∪ fn(v′). \\ (a·y|[a]v y, [a]v′ y) ∈ NR\}. \end{matrix}

K′_{μρ}(NR) = \{(NE, NE′) | \begin{matrix}∃y ∉ fv(NE) ∪ fv(NE′). \\ (y|NE[y], NE′[y]) ∈ NR\}. \end{matrix}

These modifications do not change the relation of λμρ-bisimilarity; in fact, the greatest J-bisimulation is unchanged. The two operators V′_{μρ} and K′_{μρ} are more convenient in the congruence proof below, while the other two operators are more convenient when using λμρ-bisimulation as a proof principle.

We first show that λμρ-bisimilarity is an equivalence relation.

Definition 18. Let NQ ⊆ NU_{J}.

1. NQ is closed under weakening if whenever (X_{0}|s, s′, NR) ∈ NQ and X_{0} ⊆ X for some finite set X of names and variables, also (X|s, s′, NR) ∈ NQ.

2. NQ is closed under context extrusion if (X|s, s′, NR) ∈ NQ and (Z_{1}·Z_{2}|nt, nt′) ∈ NR imply that there exists NR′ ⊇ NR ∪ {(Z_{2}|nt, nt′)} such that (X·Z_{1}|s, s′, NR′) ∈ NQ.

Lemma 19. The greatest J-bisimulation is closed under weakening and context extrusion.

Lemma 20. λμρ-bisimilarity is an equivalence relation.

Proof sketch. Reflexivity and symmetry follow easily from the definition of B_{J}. As for transitivity, assume that t ≂_{μρ} t′ and that t′ ≂_{μρ} t′′; we must show that t ≂_{μρ} t′′ (and similarly for named terms). Proposition 16 implies that there exists some J such that t and t′ are J-bisimilar and t′ and t′′ are J-bisimilar. Now consider a general composition construction on named term relation sets. Given NR_{1} ⊆ NRel(Y, J, J_{1}) and NR_{2} ⊆ NRel(Y, J, J_{2}), define their composition as

NR_{1}; NR_{2} = \{(X|nt_{1}, nt_{2}) | ∃nt.\begin{matrix}(X|nt_{1}, nt) ∈ NR_{1} & \\ (X|nt, nt_{2}) ∈ NR_{2}\}, \end{matrix}

and given NQ_{1}, NQ_{2} ⊆ NU_{J}, define

NQ_{1}; NQ_{2} = \begin{cases}(X|s_{1}, s_{2}, NR_{1}; NR_{2}) | \\ ∃s.(X|s_{1}, s, NR_{1}) ∈ NQ_{1} & (X|s, s_{2}, NR_{2}) ∈ NQ_{2}\}. \end{cases}

Then the following property holds: if NQ_{1} and NQ_{2} are J-bisimulations closed under weakening, then so is NQ_{1}; NQ_{2}.

It remains to show that λμρ-bisimilarity is compatible. The proof of this fact is structured as follows:

• First, we show that a restricted variant of λμρ-bisimilarity is substitutive in a sense defined below. (The restricted variant does not validate certain common extensionality rules for call-by-value calculi.)

• Second, we use a syntactic translation to show that full λμρ-bisimilarity is substitutive. It follows that λμρ-bisimilarity is compatible.

9.1 Substitutions

A substitution is a finite map σ with a domain consisting of variables and names, and such that σ maps each variable in its domain to a λμρ-calculus value, and each name in its domain to a λμρ-calculus named evaluation context. Let σ range over substitutions. When ϕ is a syntactic phrase (store, value, term, or named term), ϕσ denotes the result of “carrying out the substitution” σ on ϕ (we omit the formal definitions). Also, define

NR(σ, σ′) = {(Z|ntσ, nt′σ′) | (Z|nt, nt′) ∈ NR}

(where the variables and names occurring free in the ranges of σ and σ′ are not in Z).

Let dom(σ) denote the domain of σ. Say that

X ⊢ σ Σ(NR) σ′ : Y

when dom(σ) = dom(σ′) = Y, and:

1. For every variable x ∈ Y, (σ(x), σ′(x)) ∈ V′_{μρ}(NR).

2. For every name a ∈ Y, (σ(a), σ′(a)) ∈ K′_{μρ}(NR).

3. The free variables and names in the ranges of σ and σ′ are contained in X.

Say that two substitutions σ and σ′ are λμρ-bisimilar (notation: σ ≂_{μρ} σ′) if there exists a J-bisimulation containing a tuple (X · Y |{}, {}, NR) such that X ⊢ σ Σ(NR) σ′ : Y. In the next sections we show that λμρ-bisimilarity is substitutive in the following sense:

1. If t ≂_{μρ} t′ and σ ≂_{μρ} σ′, then tσ ≂_{μρ} t′σ′.

2. If nt ≂_{μρ} nt′ and σ ≂_{μρ} σ′, then ntσ ≂_{μρ} nt′σ′.

9.2 Non-η bisimulation

In order to show that λμρ-bisimilarity is substitutive, we first show the analogous result for a certain restricted variant of λμρ-bisimilarity. The variation consists in a change in the definition of the operators V and K (which are used to define relations on values and named evaluation contexts, respectively).

Definition 21. Let NR be a named term relation.

M^{†}(NR) = \begin{cases}([a]v, [a]v′), (NE[x v], NE′[x v′]) | \\ (v, v′) ∈ V^{†}(NR) & (NE, NE′) ∈ K^{†}(NR)\} \end{cases}
V^{†}(NR) = {(x, x) | x is a variable}

∪ \{(λx. t, λx. t′) | \begin{matrix}∃a ∉ fn(t) ∪ fn(t′). \\ (x·a|[a]t, [a]t′) ∈ NR\} \end{matrix}

K^{†}(NR) = {([a][ ], [a][ ]) | a is a name}

∪ {(NE[let x=[ ] in t], NE′[let x=[ ] in t′]) | x ∉ fv(NE) ∪ fv(NE′) & (x|NE[t], NE′[t′]) ∈ NR}

Definition 22.

1. For every named term relation set NQ ⊆ NU_{J}, the named term relation set B_{J}^{†}(NQ) is defined in the same way as B_{J}(NQ), except that M^{†} and V^{†} are used instead of M_{μρ} and V_{μρ}.

2. NQ is a non-η J-bisimulation if NQ ⊆ B_{J}^{†}(NQ).

3. Two reference-closed λμρ-terms t and t′ are non-η bisimilar (notation: t ≂^{†} t′) if there exist a finite set of references J and a non-η J-bisimulation containing a tuple (X|{}, {}, NR) such that (t, t′) ∈ T_{μρ}(NR). Non-η bisimilarity of named terms is defined similarly.

Remark. The reason for the name “non-η” is that non-η bisimilarity does not satisfy two common extensionality rules for call-by-value calculi, namely the η_{v}-rule and the let_{η}-rule: λx. y x ≂̸^{†} y and (let x=y z in x) ≂̸^{†} y z.

Let B_{J}^{†} be the greatest non-η J-bisimulation. The key to showing that nonη bisimilarity is substitutive is to show that B_{J}^{†} is closed under substitutions in the sense defined next.

Definition 23.

1. For every NQ ⊆ NU_{J}, let

F^{†}(NQ) = \begin{cases}(X|sσ, s′σ′, NR(σ, σ′)) | \\ ∃Y. (X·Y |s, s′, NR) ∈ NQ & \\ X ⊢ σ Σ^{†}(NR) σ′ : Y \} \end{cases}

where Σ^{†}(NR) is defined in the same way as Σ(NR), except that V^{†} and K^{†} are used in place of V′_{μρ} and K′_{μρ} in the definition.

2. A named term relation set NQ ⊆ NU_{J} is closed under substitutions if F^{†}(NQ) ⊆ NQ.

We now proceed to show that for every J, the greatest non-η J-bisimulation is closed under substitutions. Define the substitutive closure of NQ as

S^{†}(NQ) = ⋃_{n<ω}(F^{†})^{n}(NQ).

It is the least fixed point of F^{†} containing NQ.

Main Lemma. Let NQ ⊆ NU_{J} be a non-η J-bisimulation which is closed under context extrusion. Let (X|s, s′, NR) ∈ (F^{†})^{n}(NQ) and (Z|nt, nt′) ∈ NR and (v_{ȷ}, v′_{ȷ}) ∈ V^{†}(NR) for all ȷ ∈ J.

1. Assume that ({ȷ:=v_{ȷ}^{ȷ∈J}}·s, nt) ↦^{⋆} ({ȷ:=w_{ȷ}^{ȷ∈J}}·s_{1}, ne_{1}) in m or fewer steps. Then there exist X_{1} ⊇ X·Z, s′_{1}, ne′_{1}, w′_{ȷ}^{ȷ∈J}, and NR_{1} ⊇ NR such that

({ȷ:=v_{ȷ}^{′ȷ∈J}}·s′, nt′) ↦^{⋆} ({ȷ:=w′_{ȷ}^{ȷ∈J}}·s′_{1}, ne′_{1}),

(X_{1}|s_{1}, s′_{1}, NR_{1}) ∈ S^{†}(NQ), (ne_{1}, ne′_{1}) ∈ M^{†}(NR_{1}), and (w_{ȷ}, w′_{ȷ}) ∈ V^{†}(NR_{1}) for all ȷ ∈ J.

2. Conversely, assume that

({ȷ:=v_{ȷ}^{′ȷ∈J}}·s′, nt′) ↦^{⋆} ({ȷ:=w′_{ȷ}^{ȷ∈J}}·s′_{1}, ne′_{1})

in m or fewer steps. Then there exist X_{1} ⊇ X·Z, s_{1}, ne_{1}, w_{ȷ}^{ȷ∈J}, and NR_{1} ⊇ NR such that

({ȷ:=v_{ȷ}^{ȷ∈J}}·s, nt) ↦^{⋆} ({ȷ:=w_{ȷ}^{ȷ∈J}}·s_{1}, ne_{1})

etc.

Proof sketch. By induction on the pairs (m, n), ordered lexicographically.

Corollary 24. The greatest non-η J-bisimulation B_{J}^{†} is closed under substitutions.

Proof sketch. The Main Lemma implies that

(F^{†})^{n}(B_{J}^{†}) ⊆ B_{J}^{†}(S^{†}(B_{J}^{†}))

for all n ≥ 0. By definition of S^{†} and the fact that non-η bisimulations are closed under unions, S^{†}(B_{J}^{†}) ⊆ B_{J}^{†}(S^{†}(B_{J}^{†})). This means that S^{†}(B_{J}^{†}) is a nonη J-bisimulation, and therefore F^{†}(B_{J}^{†}) ⊆ S^{†}(B_{J}^{†}) ⊆ B_{J}^{†}, since B_{J}^{†} is the largest non-η J-bisimulation.

9.3 Non-η bisimilarity is substitutive

In order to show that non-η bisimilarity is substitutive, one needs the following construction for combining named term relation sets:

Definition 25. Given NQ_{1}, NQ_{2} ⊆ NU_{J}, define

NQ_{1} + NQ_{2} = {(X|s_{1}·s_{2}, s′_{1}·s′_{2}, NR_{1} ∪ NR_{2}) | (X|s_{1}, s′_{1}, NR_{1}) ∈ NQ_{1} & (X|s_{2}, s′_{2}, NR_{2}) ∈ NQ_{2} & dom(s_{1}) ∩ dom(s_{2}) = dom(s′_{1}) ∩ dom(s′_{2}) = ∅}.

Lemma 26. If NQ_{1} and NQ_{2} are non-η J-bisimulations closed under weakening, then so is NQ_{1} + NQ_{2}.

Corollary 27. The greatest non-η J-bisimulation B_{J}^{†} satisfies that

B_{J}^{†} = B_{J}^{†} + B_{J}^{†}.

Finally, non-η bisimilarity is substitutive:

Theorem 28.

1. If t ≂^{†} t′ and σ ≂^{†} σ′, then tσ ≂^{†} t′σ′.

2. If nt ≂^{†} nt′ and σ ≂^{†} σ′, then ntσ ≂^{†} nt′σ′.

Proof sketch. We show the second implication—the first is completely similar. Assume that nt ≂^{†} nt′ and σ ≂^{†} σ′, and let J be the set of free references in nt, nt′, σ, and σ′. Then the greatest non-η J-bisimulation B_{J}^{†} contains a tuple (X_{1}|{}, {}, NR_{1}) such that (|nt, nt′) ∈ NR_{1} and a tuple (X_{2} · Y |{}, {}, NR_{2}) such that X_{2} ⊢ σ Σ^{†}(NR_{2}) σ′ : Y. Then by Corollary 27, B_{J}^{†} also contains the tuple (X_{1} ∪ X_{2} ∪ Y |{}, {}, NR_{1} ∪ NR_{2}). Finally, since B_{J}^{†} is closed under substitutions, it also contains the tuple ((X_{1} \ Y) ∪ X_{2}|{}, {}, NR_{1}(σ, σ′) ∪ NR_{2}(σ, σ′)) where (|ntσ, ntσ′) ∈ NR_{1}(σ, σ′). Hence ntσ ≂^{†} nt′σ′.

9.4 λμρ-bisimilarity is substitutive

The fact that λμρ-bisimilarity is substitutive can be derived from the analogous result for non-η bisimilarity, Theorem 28, by means of a syntactic translation involving an “infinite η-expansion” combinator H.

Fix a finite set of references J = {ȷ_{1}, … ȷ_{n}}. For every value v and every term t, define the term

app[v, t] = let x_{1}=!ȷ_{1} in … let x_{n}=!ȷ_{n} in let y_{1}=v x_{1} in … let y_{n}=v x_{n} in (ȷ_{1}:=y_{1}; … ȷ_{n}:=y_{n}; t)

(where x_{1}, … x_{n}, y_{1}, …, y_{n} are not free in v or t). The operational behavior of app[v, t] is to “apply v to every reference in J” and then continue according to t. Now define

H_{0} = λz.λf.λx.let y_{1}=z x in app[z, let y_{2}=f y_{1} in app[z, z y_{2}]]
H = fix[H_{0}].

The combinator H originates from a generalization of a “syntactic minimal invariance” equation [17, 29].

Also, for every value v and every named evaluation context NE, define

G[v] = λx. let y_{1}=H x in app[H, let y_{2}=v y_{1} in app[H, H y_{2}]]
G[NE] = NE[let x=[ ] in app[H, H x]].

Definition 29.

1. For every term t, let t^{‡} be the result of substituting G[x] for every free variable x in t, and substituting G[[a][ ]] for every free name a in t. For every named term nt, define nt^{‡} similarly.

2. For every term t, define

t^{†} = app[H, let x=t^{‡} in app[H, H x]].

3. For every named term nt = [a]t, define nt^{†} = [a]t^{†}.

Using the above syntactic constructs, λμρ-bisimilarity can be characterized in terms of non-η bisimilarity:

Proposition 30. Let the free references of t, t′, v, and v′ be contained in J.

1. t ≂_{μρ} t′ iff t^{†} ≂^{†} t^{′†}.

2. v ≂_{μρ} v′ iff G[v^{‡}] ≂^{†} G[v^{′‡}].

3. nt ≂_{μρ} nt′ iff nt^{†} ≂^{†} nt^{′†}.

If v is a value such that the free references of v are contained in J, then v ≂_{μρ} G[v] (but in general v ≂̸^{†} G[v]). As will be shown next, a more general version of that property holds.

Definition 31. The binary relation R on terms, named evaluation contexts, and named terms is defined inductively by means of the inference rules in Figure 1.

Two stores s and s′ are related by R if they have the same domain J_{0} and if s(ȷ) R s′(ȷ) for all ȷ ∈ J_{0}.

t R t  {v R v′ \atop v R G[v′]}  {t R t′ \atop λx. t R λx. t′}
\begin{matrix}v_{1} R v′_{1} & v_{2} R v′_{2} \\ v_{1} v_{2} R v′_{1} v′_{2} \end{matrix}  \begin{matrix}v R v′ & t R t′ \\ (ı:=v; t) R (ı:=v′; t′) \end{matrix}
t R t′  ∀ȷ ∈ J_{0}.s(ȷ) R s′(ȷ) \begin{matrix}dom(s) = dom(s′) = J_{0}, \\ J_{0} ∩ J = ∅ \end{matrix}

ρs. t R ρs′. t′

{nt R nt′ \atop μa. nt R μa. nt′} NE R NE NE R NE′ ; NE R G[NE′]
t R t′  NE R NE′

NE[let x=[ ] in t] R NE′[let x=[ ] in t′]

NE R NE′  t R t′
NE[t] R NE′[t′]

Figure 1: The relation R.

Proposition 32. Let J′ ⊆ J. The named term relation set

\begin{cases}(X|s, s′, NR) ∈ NU_{J′} | \\ s R s′ & NR ⊆ \{(Z|nt, nt′) | nt R nt′\}\} \end{cases}

is a J′-bisimulation.

In particular, taking J′ = J: Corollary 33. Let the free references of t, t′, nt, and nt′ be contained in J.

1. t R t′ implies t ≂_{μρ} t′.

2. nt R nt′ implies nt ≂_{μρ} nt′.

It follows that λμρ-bisimilarity is substitutive: Theorem 34.

1. If t ≂_{μρ} t′ and σ ≂_{μρ} σ′, then tσ ≂_{μρ} t′σ′.

2. If nt ≂_{μρ} nt′ and σ ≂_{μρ} σ′, then ntσ ≂_{μρ} nt′σ′. Proof sketch. As a simple example, assume that t ≂_{μρ} t′ and v ≂_{μρ} v′; it must be shown that t[v/x] ≂_{μρ} t′[v′/x]. By Corollary 33, t[v/x] ≂_{μρ} t[G[G[v]]/x]. Hence by Proposition 30 and the fact that non-η bisimilarity is substitutive:

(t[v/x])^{†} ≂^{†} (t[G[G[v]]/x])^{†} = t^{†}[G[v^{‡}]/x]
≂^{†} t^{′†}[G[v^{′‡}]/x]
≂^{†} (t′[v′/x])^{†}.

By Proposition 30 again, t[v/x] ≂_{μρ} t′[v′/x].

9.5 λμρ-bisimilarity is a congruence

Now it is shown that λμρ-bisimilarity is compatible, using the fact that it is substitutive.

Proposition 35. B_{J} = B_{J} + B_{J}.

Corollary 36. Let fr(nt) ∪ fr(nt′) ⊆ J, and let y_{ȷ}^{ȷ∈J} be distinct variables not free in nt or nt′. Suppose that

({ȷ:=y_{ȷ}^{ȷ∈J}}, nt) ↦^{∗} ({ȷ:=v_{ȷ}^{ȷ∈J}}·s_{1}, ne_{1}),
({ȷ:=y_{ȷ}^{ȷ∈J}}, nt′) ↦^{∗} ({ȷ:=v′_{ȷ}^{ȷ∈J}}·s′_{1}, ne′_{1}),

and (X_{1}|s_{1}, s′_{1}, NR_{1}) ∈ B_{J} with (ne_{1}, ne′_{1}) ∈ M_{μρ}(NR_{1}) and (v_{ȷ}, v′_{ȷ}) ∈V_{μρ}(NR_{1}) for all ȷ ∈ J. Then nt ≂_{μρ} nt′.

Theorem 37. λμρ-bisimilarity is compatible.

Proof sketch. The most complicated case to show is that λμρ-bisimilarity is closed under ρ-abstraction: if t ≂_{μρ} t′ and also v_{ȷ} ≂_{μρ} v′_{ȷ} for all ȷ ∈ J_{0}, then

ρ{ȷ:=v_{ȷ}^{ȷ∈J_{0}}}. t ≂_{μρ} ρ{ȷ:=v′_{ȷ}^{ȷ∈J_{0}}}. t′.

Here one proceeds in three steps:

1. If z ∉ fv(t), then ρs. t ≂_{μρ} let x=ρs. λz. t in x I.

2. If v ≂_{μρ} v′ and v_{ȷ} ≂_{μρ} v′_{ȷ} for all ȷ ∈ J_{0}, and if the free references of all these values are contained in J ⊇ J_{0}, then

ρ{ȷ:=G[v_{ȷ}^{‡}]^{ȷ∈J_{0}}}. G[v^{‡}] ≂_{μρ} ρ{ȷ:=G[v′_{ȷ}^{‡}]^{ȷ∈J_{0}}}. G[v′^{‡}].

3. If the free references of v and v_{ȷ}^{ȷ∈J_{0}} are contained in J ⊇ J_{0}, then ρ{ȷ:=v_{ȷ}^{ȷ∈J_{0}}}. v ≂_{μρ} ρ{ȷ:=G[v_{ȷ}^{‡}]^{ȷ∈J_{0}}}. G[v^{‡}].

The third part follows from Proposition 32 and Corollary 36. The proof of the second part uses Corollary 36 and the following construction: for every NQ ⊆ NU_{J} with J_{0} ⊆ J, let NQ\J_{0} be the subset of NU_{J\J_{0}} defined by

NQ\J_{0} = {(X_{1}|{ȷ :=w_{ȷ}^{ȷ∈J_{0}}}·s, {ȷ :=w′_{ȷ}^{ȷ∈J_{0}}}·s′, NR) | (X|s, s′, NR) ∈ NQ & X ⊆ X_{1} & ∀ȷ ∈ J_{0}. (w_{ȷ}, w′_{ȷ}) ∈ V^{†}(NR)}.

The Main Lemma implies that B_{J}^{†}\J_{0} ⊆ B_{J\J_{0}}^{†}.

The other cases of the proof are simpler and use Theorem 34 and Corollary 36.

In summary, the main result of this section:

Theorem 38. λμρ-bisimilarity is a congruence: an equivalence relation which is furthermore compatible.

Corollary 39. Each of λ-bisimilarity, λμ-bisimilarity, and λρ-bisimilarity is a congruence.

Proof. It is easy to see that two λμ-terms are λμ-bisimilar if and only if they are λμρ-bisimilar, and similarly for the other inclusions between the four calculi considered in this article. (Each extension is “fully abstract”). The statement of the corollary immediately follows. Suppose for example that v_{1} ≂_{μ} v′_{1} and v_{2} ≂_{μ} v′_{2}. Then v_{1} ≂_{μρ} v′_{1} and v_{2} ≂_{μρ} v′_{2}. Therefore, since λμρ-bisimilarity is a congruence, v_{1} v_{2} ≂_{μρ} v′_{1} v′_{2}. Finally, since v_{1} v_{2} and v′_{1} v′_{2} are λμ-terms, v_{1} v_{2} ≂_{μ} v′_{1} v′_{2}.

Remark. Non-η bisimilarity is also a congruence. The relation between non-η bisimilarity and λμρ-bisimilarity is analogous to the relation between Böhm tree equivalence and Böhm tree equivalence up to η for the pure λ-calculus.

10 Full abstraction

In this section we show that λμρ-bisimilarity coincides with contextual equivalence for the λμρ-calculus.

First, let us say that a variable-closed and reference-closed named term nt terminates, written nt⇓, iff ∃s, ne. ({}, nt) ↦^{∗} (s, ne). Then we define that terms t and t′ are contextually equivalent, written t ≅_{μρ} t′, iff for all names a and term contexts C such that C[t] and C[t′] are variable-closed and reference-closed, [a]C[t]⇓ ⇔ [a]C[t′]⇓. It is easy to see that ≅_{μρ} is a congruence and, moreover, it is the largest congruence relation which satisfies that t ≅_{μρ} t′ implies [a]t⇓ ⇔ [a]t′⇓ for all names a and variable-closed and reference-closed terms t and t′. Since λμρ-bisimilarity is a congruence, it is immediate from its definition that it is included in contextual equivalence, viz. that λμρ-bisimilarity is sound with respect to contextual equivalence.

Theorem 40 (Soundness). ≂_{μρ} ⊆ ≅_{μρ}.

Similarly, λ-bisimilarity, λμ-bisimilarity, and λρ-bisimilarity are included in contextual equivalence for their respective calculi.

To prove the converse of Theorem 40, we will form a bisimulation which relates all contextually equivalent terms. The task is similar to the Böhmout proof of the separability theorem in the call-by-name λ-calculus. For readers familiar with the Böhm-out proof, we briefly compare our approach: The Böhm-out proof substitutes, for each free variable, a function that takes many arguments. This makes it possible to control the function’s behaviour separately each time it is called. We need the same level of control over the behaviour of the functions and continuations that are substituted for the free variables and names in the contextually equivalent terms we want to prove bisimilar. However, instead of using functions that take many arguments, we use stateful functions and continuations. They use mutable references to execute pre-programmed strategies that specify how they will behave each time they are invoked. Moreover, we use the expressive power of the λμcalculus to capture not only the argument when a function substituted for a free variable is invoked but also the continuation. The presence of mutable references introduces one complication, namely it requires us to store every argument and continuation we see so that we can invoke them multiple times to expose stateful behaviour.

We will need to accumulate values in lists and random access list entries. We encode the empty list as the identity function I and we encode the list v with elements v_{1}, …, v_{n} appended as:

⟨v|v_{1}, …, v_{n}⟩ =
λz. let x_{0}=v z in let x_{1}=x_{0} v_{1} in … in x_{n−1} v_{n}

where z, x_{0}, …, x_{n−1} are not free in v, v_{1}, …, v_{n}. When v = I, we write just ⟨v_{1}, …, v_{n}⟩. We access the q’th element in the list v with

v#q = μa. [a]v λx_{1} … λx_{q−1}. â

where a is not free in v.

We use a designated reference ȷ_{0} to store a list with all the arguments v and continuations NE we see along the way (each NE is stored as the value λx. μa. NE[x] with x, a not free in NE). We let w range over both pairs of values and pairs of named evaluation contexts. Given such a pair, let w^{V} be the pair of values and let w^{NR} be the singleton named term relation defined as:

w^{V} = \{ \begin{matrix}(v_{1}, v_{2}) & if w = (v_{1}, v_{2}) \\ (λx. μa. NE_{1}[x], λx. μa. NE_{2}[x]) & if w = (NE_{1}, NE_{2}) \end{matrix}

w^{NR} = \{ \begin{matrix}(a·x|[a](v_{1} ⋆ x), [a](v_{2} ⋆ x)) & if w = (v_{1}, v_{2}) \\ (x|NE_{1} ⋆ x, NE_{2} ⋆ x) & if w = (NE_{1}, NE_{2}) \end{matrix}

where x and a are not free in v_{1}, v_{2}, NE_{1}, NE_{2}.

For each free variable x_{i} and name a_{j}, we associate a reference ı_{i} and ȷ_{j}, respectively. Each reference stores a strategy p which is a sequence of moves m, one for each successive invocation of the variable x_{i} or name a_{j}, ending in “success” ⊤ or “failure” ⊥:

Strategies p ::= ⊤ | ⊥ | m; p

Moves m ::= move(q, p_{1}, p_{2}) (q ≥ 1)

A move move(q, p_{1}, p_{2}) “plays” the q’th value or continuation from the list stored in ȷ_{0} and associates the strategy p_{1} with a variable, which is used as argument, and p_{2} with a name, which is used as continuation. These ideas are expressed in the following encodings. Given a reference ı and a strategy p, we define the function [[p]](ı), which takes a function argument x and a continuation y as arguments, and for every move m, we define the term [[m]], as follows.

[[⊤]](ı) = λx. λy. I
[[⊥]](ı) = λx. λy. Ω
[[m; p]](ı) = λx. λy. let z=!ȷ_{0} in ȷ_{0}:=⟨z|x, y⟩; ı:=[[p]](ı); [[m]]
[[move(q, p_{1}, p_{2})]] =
let z=!ȷ_{0} in let x=z#q in ρ{ı:=[[p_{1}]](ı), ȷ:=[[p_{2}]](ȷ)}. ǰ[x î]

where î and ǰ denote the value and the evaluation context

î = λx. μa. [a_{0}] let y=!ı in let z=y x in z â
ǰ = let x=[ ] in let y=!ȷ in let z=y x in z â_{0}

and where a_{0} is a designated “top-level” name.

These are the building blocks we use to “separate” terms. As in [21], our separation proof is co-inductive. We define:

W = \{(x_{1}, …, x_{m}, a_{1}, …, a_{n}|s_{1}, s_{2}, \{w_{1}^{NR}, …, w_{q}^{NR}\}) | \begin{matrix}∀ strategies p_{1}, …, p_{m}, p′_{1}, …, p′_{n}. \\ ∀ distinct references \begin{matrix}ı_{1}, …, ı_{m}, ȷ_{1}, …, ȷ_{n} \\ ∉ dom(s_{1}) ∪ dom(s_{2}). \end{matrix} \\ ∀ moves m. \\ [a_{0}]ρs·s′_{1}σ. [[m]]⇓ ⇔ [a_{0}]ρs·s′_{2}σ. [[m]]⇓ \\ where & \begin{matrix}s = \begin{cases}ı_{1}:=[[p_{1}]](ı_{1}), …, ı_{m}:=[[p_{m}]](ı_{m}), \\ ȷ_{1}:=[[p′_{1}]](ȷ_{1}), …, ȷ_{n}:=[[p′_{n}]](ȷ_{n})\}, \end{cases} \\ σ = [î_{1}/x_{1}, …, î_{m}/x_{m}, [a^{0}]ǰ_{1}/a_{1}, …, [a^{0}]ǰ_{n}/a_{n}], \\ s′_{i} = s_{i}·\{ȷ_{0}:=⟨v_{i1}, …, v_{iq}⟩\}, \\ (v_{11}, v_{21}) = w_{1}^{V}, …, (v_{1q}, v_{2q}) = w_{q}^{V}\} \end{matrix} \end{matrix}

Lemma 41. W is a λμρ-bisimulation.

Proof. By detailed analysis of the possible operational behaviours of the named terms in each w_{i}^{NR} triple.

Lemma 42. t_{1} ≅_{μρ} t_{2} implies t_{1} ≂_{μρ} t_{2} if fr(t_{1}) ∪ fr(t_{2}) = ∅.

Proof. Suppose t_{1} and t_{2} are reference-closed terms, t_{1} ≅_{μρ} t_{2}, and X ⊢ t_{1}, t_{2}. Then, by the definition of W and contextual equivalence, t_{1} ≅_{μρ} t_{2} implies (X|{}, {}, {w^{NR}}) ∈ W where w = (λx. t_{1}, λx. t_{2}) and x ∉ X. Observe that w^{NR} = (a·x|[a]t_{1}, [a]t_{2}). We conclude t_{1} ≂_{μρ} t_{2} by Lemmas 41 and 19.

To extend this result to general terms, we define a term context L_{J} that “translates” any term t with fv(t) ⊆ J = {ı_{1}, … ı_{n}} to the reference-closed closed term

L_{J}[t] = λx. ρ{ı_{1}:=I, …, ı_{n}:=I}. ⟨λx. t, get(ı_{1}), set(ı_{1}), …, get(ı_{n}), set(ı_{n})⟩

where x ∉ fv(t), get(ı_{i}) = λx.!ı_{i}, and set(ı_{i}) = λx. (ı_{i}:=x; I).

Lemma 43. t_{1} ≂_{μρ} t_{2} iff L_{J}[t_{1}] ≂_{μρ} L_{J}[t_{2}].

Theorem 44 (Completeness). ≂_{μρ} ⊇ ≅_{μρ}.

Proof. Suppose J = fr(t_{1}) ∪ fr(t_{2}). Then

t_{1} ≅_{μρ} t_{2} ⇒ L_{J}[t_{1}] ≅_{μρ} L_{J}[t_{2}] ≅_{μρ} is a congruence
⇒ L_{J}[t_{1}] ≂_{μρ} L_{J}[t_{2}] Lemma 42
⇒ t_{1} ≂_{μρ} t_{2}  Lemma 43.

Acknowledgements

We thank Olivier Danvy and Andrzej Filinski for guidance and comments on this work. We also thank Matthias Felleisen and the anonymous referees for comments and suggestions, and Radha Jagadeesan, Paul Levy, and Corin Pitcher for discussions.

The first author is supported by BRICS (Basic Research in Computer Science, funded by the Danish National Research Foundation).

References

[1] S. Abramsky. The lazy lambda calculus. In D. Turner, editor, Research Topics in Functional Programming, pages 65–116. Addison-Wesley, 1990.

[2] S. Abramsky, K. Honda, and G. McCusker. A fully abstract game semantics for general references. In Proc. 13th Annual IEEE Symposium on Logic in Computer Science, pages 334–344, 1998.

[3] Z. M. Ariola and H. Herbelin. Minimal classical logic and control operators. In ICALP, volume 2719 of Lecture Notes in Computer Science, pages 871–885. Springer-Verlag, 2003.

[4] H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. Number 103 in Studies in Logic and the Foundations of Mathematics. North-Holland, revised edition, 1984.

[5] G. M. Bierman. A computational interpretation of the lambda-mu calculus. In L. Brim, J. Gruska, and J. Zlatuska, editors, Proc. 23rd Mathematical Foundations of Computer Science, Brno, Czech Republic, volume 1450, pages 336–345. Springer-Verlag, 1998.

[6] R. David and W. Py. λμ-calculus and Böhm’s theorem. Journal of Symbolic Logic, 66(1):407–413, 2001.

[7] L. Egidi, F. Honsell, and S. Ronchi della Rocca. Operational, denotational and logical descriptions: a case study. Fundamenta Informaticae, 16(2):149–169, 1992.

[8] M. Felleisen and R. Hieb. The revised report on the syntactic theories of sequential control and state. Theoretical Computer Science, 103:235–271, 1992.

[9] D. P. Friedman and C. T. Haynes. Constraining control. In Proc. 12th ACM Symposium on Principles of Programming Languages, pages 245– 254, 1985.

[10] A. D. Gordon. Bisimilarity as a theory of functional programming. Theoretical Computer Science, 228(1–2):5–47, 1999.

[11] A. D. Gordon and A. M. Pitts, editors. Higher Order Operational Techniques in Semantics. Publications of the Newton Institute. Cambridge University Press, 1998.

[12] P. de Groote. On the relation between the lambda-mu-calculus and the syntactic theory of sequential control. In LPAR ’94, volume 822 of Lecture Notes in Artificial Intelligence, pages 31–43. Springer-Verlag, 1994.

[13] V. Koutavas and M. Wand. Small bisimulations for reasoning about higher-order imperative programs. In Proc. 33rd ACM Symposium on Principles of Programming Languages, pages 141–152, 2006.

[14] J. Laird. Full abstraction for functional languages with control. In Proc. 12th Annual IEEE Symposium on Logic in Computer Science, pages 58– 67, 1997.

[15] P. J. Landin. The mechanical evaluation of expressions. The Computer Journal, 6(4):308–320, 1964.

[16] S. B. Lassen. Bisimulation up to context for imperative lambda calculus. Unpublished note. Presented at The Semantic Challenge of Object-Oriented Programming, Schloss Dagstuhl, 1998.

[17] S. B. Lassen. Relational reasoning about contexts. In Gordon and Pitts [11], pages 91–135.

[18] S. B. Lassen. Bisimulation in untyped lambda calculus: Böhm trees and bisimulation up to context. In MFPS XV, volume 20 of Electronic Notes in Theoretical Computer Science, pages 346–374. Elsevier, 1999.

[19] S. B. Lassen. Eager normal form bisimulation. In Proc. 20th Annual IEEE Symposium on Logic in Computer Science, pages 345–354, 2005.

[20] S. B. Lassen. Normal form simulation for McCarty’s amb. In MFPS XXI, volume 155 of Electronic Notes in Theoretical Computer Science, pages 445–465. Elsevier, 2005.

[21] S. B. Lassen. Head normal form bisimulation for pairs and the λμ-calculus (extended abstract). In Proc. 21th Annual IEEE Symposium on Logic in Computer Science, 2006.

[22] P. B. Levy. Game semantics using function inventories. Talk given at Geometry of Computation 2006, Marseille, 2006.

[23] I. A. Mason and C. L. Talcott. Equivalence in functional languages with effects. Journal of Functional Programming, 1(3):297–327, 1991.

[24] M. Merro and C. Biasi. On the observational theory of the CPS-calculus (extended abstract). In Proc. 22nd Conference on Mathematical Foundations of Programming Semantics, volume 158 of Electronic Notes in Theoretical Computer Science, pages 307–330. Elsevier, 2006.

[25] A. R. Meyer and K. Sieber. Towards fully abstract semantics for local variables: Preliminary report. In Proc. 15th ACM Symposium on Principles of Programming Languages, San Diego, CA, 1988.

[26] M. Parigot. λμ-calculus: An algorithmic interpretation of classical natural deduction. In A. Voronkov, editor, Proceedings Intl. Conf. on Logic Programming and Automated Reasoning, LPAR’92, St Petersburg, volume 624 of Lecture Notes in Computer Science, pages 190–201. Springer-Verlag, 1992.

[27] R. P. Perez. An extensional partial combinatory algebra based on λ-terms. In A. Tarlecki, editor, Proc. Mathematical Foundations of Computer Science, volume 520 of Lecture Notes in Computer Science, pages 387–396. Springer-Verlag, 1991.

[28] A. M. Pitts. Reasoning about local variables with operationally-based logical relations. In P. W. O’Hearn and R. D. Tennent, editors, Algol-Like Languages, volume 2, chapter 17, pages 173–193. Birkhauser, 1997. Reprinted from Proceedings Eleventh Annual IEEE Symposium on Logic in Computer Science, 1996, pp 152–163.

[29] A. M. Pitts and I. D. B. Stark. Operational reasoning for functions with local state. In Gordon and Pitts [11], pages 227–273.

[30] E. Ritter and A. M. Pitts. A fully abstract translation between a λcalculus with reference types and Standard ML. In Proc. 2nd International Conference on Typed Lambda Calculus and Applications, Edinburgh, volume 902 of Lecture Notes in Computer Science. Springer-Verlag, 1995.

[31] D. Sangiorgi. The lazy lambda calculus in a concurrency scenario. Information and Computation, 111(1):120–153, 1994.

[32] E. Sumii and B. C. Pierce. A bisimulation for type abstraction and recursion. In Proc. 32nd ACM Symposium on Principles of Programming Languages, pages 63–74, 2005.

[33] C. Talcott. Reasoning about functions with effects. In Gordon and Pitts [11], pages 347–390.

[34] M. Wand and G. T. Sullivan. Denotational semantics using an operationally-based term model. In Proc. 24th ACM Symposium on Principles of Programming Languages, pages 386–399, 1997.

Recent BRICS Report Series Publications

RS-07-4 Kristian Støvring and Søren B. Lassen. A Complete, Co-Inductive Syntactic Theory of Sequential Control and State. February 2007. 36 pp. Appears in the proceedings of POPL 2007, p. 161–172.

RS-07-3 Luca Aceto, Willem Jan Fokkink, and Anna Ingólfsdóttir. Ready To Preorder: Get Your BCCSP Axiomatization for Free! February 2007. 37 pp.

RS-07-2 Luca Aceto and Anna Ingólfsdóttir. Characteristic Formulae: From Automata to Logic. January 2007. 18 pp.

RS-07-1 Daniel Andersson. HIROIMONO is NP-complete. January 2007. 8 pp.

RS-06-19 Michael David Pedersen. Logics for The Applied π Calculus. December 2006. viii+111 pp.

RS-06-18 Ma�gorzata Biernacka and Olivier Danvy. A Syntactic Correspondence between Context-Sensitive Calculi and Abstract Machines. dec 2006. iii+39 pp. Extended version of an article to appear in TCS. Revised version of BRICS RS-05-22.

RS-06-17 Olivier Danvy and Kevin Millikin. A Rational Deconstruction of Landin’s J Operator. December 2006. ii+37 pp. Revised version of BRICS RS-06-4. A preliminary version appears in the proceedings of IFL 2005, LNCS 4015:55–73.

RS-06-16 Anders Møller. Static Analysis for Event-Based XML Processing. October 2006. 16 pp.

RS-06-15 Dariusz Biernacki, Olivier Danvy, and Kevin Millikin. A Dynamic Continuation-Passing Style for Dynamic Delimited Continuations. October 2006. ii+28 pp. Revised version of BRICS RS-05-16.

RS-06-14 Giorgio Delzanno, Javier Esparza, and Jiří Srba. Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols. July 2006. 31 pp. To appear in ATVA ’06.

RS-06-13 Jiří Srba. Visibly Pushdown Automata: From Language Equivalence to Simulation and Bisimulation. July 2006. 21 pp. To appear in CSL ’06.