A Bisimulation for Type Abstraction and Recursion

EIJIRO SUMII Tohoku University and BENJAMIN C. PIERCE University of Pennsylvania

We present a bisimulation method for proving the contextual equivalence of packages in λ-calculus with full existential and recursive types. Unlike traditional logical relations (either semantic or syntactic), our development is “elementary,” using only sets and relations and avoiding advanced machinery such as domain theory, admissibility, and ⊤⊤-closure. Unlike other bisimulations, ours is complete even for existential types. The key idea is to consider sets of relations—instead of just relations—as bisimulations.

Categories and Subject Descriptors: D.3.3 [Programming Languages]: Language Constructs and Features—Abstract data types; F.3.3 [Logics and Meanings of Programs]: Studies of Program Constructs—Type structure

General Terms: Theory, Languages Additional Key Words and Phrases: Lambda-Calculus, Contextual Equivalence, Bisimulations, Logical Relations, Existential Types, Recursive Types

1. INTRODUCTION

Proving the equivalence of computer programs is important not only for verifying the correctness of program transformations such as compiler optimizations, but also for showing the compatibility (substitutability) of program modules. Consider two modules M and M′ implementing the same interface I; if these different implementations are equivalent under this common interface, then they are indeed compatible, correctly hiding their differences from outside view.

Contextual equivalence is a natural definition of program equivalence: two programs are called contextually equivalent if they exhibit the same observable behavior when put in any legitimate context of the language. However, direct proofs of contextual equivalence are typically infeasible, because its definition involves a universal quantification over an infinite number of contexts (and naive approaches such as structural induction on the syntax of contexts do not work). This has led to a search for alternative methods for proving contextual equivalence, whose fruits can be grouped into two categories: logical relations and bisimulations.

An extended abstract of this article has appeared in Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 63–74, 2005. Permission to make digital/hard copy of all or part of this material without fee for personal or classroom use provided that the copies are not made or distributed for profit or commercial advantage, the ACM copyright/server notice, the title of the publication, and its date appear, and notice is given that copying is by permission of the ACM, Inc. To copy otherwise, to republish, to post on servers, or to redistribute to lists requires prior specific permission and/or a fee. \begin{matrix}c \\ ◯ \end{matrix} 20YY ACM 0004-5411/20YY/0100-0001 $5.00

Journal of the ACM, Vol. V, No. N, Month 20YY, Pages 1–43.

2 · E. Sumii and B. C. Pierce

Logical relations. Logical relations were first developed for denotational semantics of typed λ-calculi (see, e.g., [Mitchell 1996, Chapter 8] for details) and can also be adapted [Pitts 2000; 2005] to their term models; this adaptation is sometimes called syntactic logical relations [Crary and Harper 2007]. Logical relations are relations on terms defined by induction on their types: for instance, two pairs are related when their elements are pairwise related; two tagged terms in_{i}(M) and in_{j}(N) of a sum type are related when the tags i and j are equal and the contents M and N are also related; and, crucially, two functions are related when they map related arguments to related results. The soundness of logical relations is proved via the Fundamental Property (or Basic Lemma), which states that any well-typed term is related to itself.

Logical relations are pleasantly straightforward, as long as we stick to the simply typed λ-calculus (or even the polymorphic λ-calculus) without recursion. However, their extension with recursion is challenging. Recursive functions cause a problem in the proof of the fundamental property that must be addressed by introducing additional “unwinding properties” [Pitts 2000; 2005; Birkedal and Harper 1999; Crary and Harper 2007]. Recursive types are even more difficult (in particular with negative occurrences): since logical relations are defined by induction on types, recursive types (with negative occurrences) require topological properties in the definition of logical relations [Birkedal and Harper 1999; Crary and Harper 2007]. These difficulties are not confined to meta-theorems, but are visible to the users of logical relations: in order to prove contextual equivalence using logical relations, one often has to prove the admissibility, compute the limit, or calculate the ⊤⊤-closure of particular relations.^{1}

Bisimulations. Bisimulations were originally developed for process calculi [Milner 1980; 1989; 1999] and state transition systems in general. Abramsky [1990] adapted bisimulations to untyped λ-calculus and called them applicative bisimulations. Briefly, two functions λx. M and λx. M′ are bisimilar when (λx. M)N ⇓ ⟺ (λx. M′)N ⇓ for any N and the results are also bisimilar if these evaluations converge. Gordon [1995a; 1995b] and Gordon and Rees [1996; 1995] extended applicative bisimulations to calculi with objects, subtyping, universal polymorphism, and recursive types. Sangiorgi [1992] defined context bisimulation, which is a variant of applicative bisimulation for higher-order π-calculus.

Unlike logical relations, bisimulations have no difficulty with recursion (or even concurrency). However, existing bisimulation methods for typed λ-calculi are too weak in the presence of existential polymorphism; that is, they are not able to prove interesting equivalence properties of existential packages. For instance, consider the two packages

                M = pack int, ⟨1, λx: int. x =^{int} 0⟩ as τ
                M′ = pack bool, ⟨true, λx: bool. ¬x⟩ as τ

where τ = ∃α. α × (α → bool). Existing bisimulation methods cannot prove the contextual equivalence ⊢ M ≡ M′ : τ of these simple packages, because they do not

1Recently, Ahmed [2006] proposed syntactic logical relations based on evaluation step indices. See Section 7 for its relationship to our bisimulations.

Journal of the ACM, Vol. V, No. N, Month 20YY.

A Bisimulation for Type Abstraction and Recursion · 3

capture the fact that the only values of type α are 1 in the “left-hand world” and true in the right-hand world. The same observation applies to context bisimulation.

The only exceptions to the problem above are bisimulations for polymorphic π-calculi [Pierce and Sangiorgi 2000; Berger et al. 2003]. However, π-calculus is name-based and low-level. As a result, it is rather difficult to encode polymorphic λ-calculus into polymorphic π-calculus while preserving equivalence (though there are some results [Berger et al. 2003] for the case without recursion), so it is at least as difficult to use π-calculus for reasoning about abstraction in λ-calculus or similar languages with (in particular higher-order) functions and recursion. In addition to the problem of encoding, existing bisimulations for polymorphic π-calculi are incomplete [Pierce and Sangiorgi 2000] and complex [Berger et al. 2003].

Encoding existential polymorphism in terms of universal polymorphism does not help either. Consider the following encodings of M and M′

N = λf : σ. f[int]⟨1, λx: int. x =^{int} 0⟩
N′ = λf : σ. f[bool]⟨true, λx: bool. ¬x⟩

where σ = ∀α. α × (α → bool) → ans and ans is some answer type. In order to establish the bisimulation between N and N′, one has at least to prove

f[int]⟨1, λx: int. x =^{int} 0⟩ ⇓
⟺ f[bool]⟨true, λx: bool. ¬x⟩ ⇓

for any observer function f of type σ, which is almost the same as the definition of ⊢ M ≡ M′ : τ.

Our solution. We address these problems—and thereby obtain a sound and complete bisimulation for existential types (as well as universal and recursive types)—by adapting key ideas from our previous work [Sumii and Pierce 2004] on bisimulation for sealing [Morris 1973a; 1973b], a dynamic form of data abstraction. The crucial insight is that we should define bisimulations as sets of relations—rather than just relations—annotated with type information.

For instance, a bisimulation X showing the contextual equivalence of M and M′ above can be defined (roughly) as

X = {(∅, R_{0}), (Δ, R_{1}), (Δ, R_{2}), (Δ, R_{3})}

where

R_{0} = {(M, M′, τ)}
R_{1} = R_{0} ∪ {(⟨1, λx: int. x =^{int} 0⟩,

⟨true, λx: bool. ¬x⟩, α × (α → bool))}

R_{2} = R_{1} ∪ {(1, true, α),

(λx: int. x =^{int} 0,

λx: bool. ¬x,

                               α → bool)}

                   R_{3} = R_{2} ∪ {(false, false, bool)}

Journal of the ACM, Vol. V, No. N, Month 20YY.

Δ = {(α, int, bool)}.

Because we are ultimately interested in the equivalence of M and M′, we begin by including (∅, R_{0}) in X. (The role of the first element ∅ of this pair will be explained in a moment.) Next, since a context can open those packages and examine their contents, we add (Δ, R_{1}) to X, where Δ is a concretion environment mapping the abstract type α to its respective concrete types in the left-hand side and the righthand side. Then, since the contents of the packages are pairs, a context can examine their elements, so we add (Δ, R_{2}) to X. Last, since the second elements of the pairs are functions of type α → bool, a context can apply them to any arguments of type α; the only such arguments are, in fact, 1 in the left-hand world and true in the right-hand world, so we add (Δ, R_{3}) to X. Since the results of these applications are equal as booleans, there is nothing else that a context can do to distinguish the values in R_{3}.

Conceptually, each R occurring in a pair (Δ, R) ∈ X represents the knowledge of a context at some point in time, which increases via new observations by the context. In order to prove contextual equivalence, it suffices to find a bisimulation X that is closed under this increase of contexts’ knowledge. (Thus, in fact, not only X but also the singleton set {(Δ, R_{3})} is a bisimulation in our definition.)

Why do we consider a bisimulation X to be a set of Rs (with corresponding Δs) instead of taking their union in the first place? Because the latter does not exist in general! In other words, the union of two “valid” Rs is not always a valid R. For instance, consider the union of R_{3} and its inverse R_{3}^{−1} = {(V′, V, τ) | (V, V′, τ) ∈ R_{3}}. Although each of them makes perfect sense by itself, taking their union is nonsensical because it confuses two different worlds (which, in fact, is not even typesafe). This observation is absolutely fundamental in the presence of type abstraction (or other forms of information hiding such as sealing), and it forms the basis of many technicalities in the present work (as in our previous work [Sumii and Pierce 2004]). By considering a set of relations instead of taking their union, it becomes straightforward to define bisimilarity to be the largest bisimulation and thereby apply standard co-inductive arguments (to prove the completeness of bisimilarity, for instance). In addition, this also gives a natural account of the generativity of existential types, i.e., of the fact that opening the same package twice gives incompatible contents.

This decision does not incur any significant difficulty for users of our bisimulation: we devise a trick—explained below, in the definition of bisimulation for packages— that keeps the set of relations finite in many cases; even where this trick does not apply, it is not very difficult to define the infinite set of relations (e.g., by set comprehension or by induction) and check it against our definition of bisimulation (as we will do in Section 5.3 for generative functors, or as we did in previous work [Sumii and Pierce 2004, Examples 4.7 and 4.8] for security protocols).

Contributions. This is an “elementary” (i.e., not using domain theory or its variants) characterization and proof method of contextual equivalence in a language with full existential and recursive types. As discussed above, previous results in this area were (1) limited to recursive types with no negative occurrence, (2) incomplete for existential types, and/or (3) apt to be technically involved in general.

Many of the ideas used here are drawn from our previous work [Sumii and Pierce

Journal of the ACM, Vol. V, No. N, Month 20YY.

2004] on a sound and complete bisimulation for untyped λ-calculus with dynamic sealing (also known as perfect encryption). This form of information hiding is very different from static type abstraction. Given the difference, it is surprising (and interesting) in itself to find that similar ideas can be adapted to both settings. Furthermore, the language in the present paper is typed (unlike in our previous work), requiring many refinements to take type information into account throughout the technical development. In general, typed equivalence is much coarser than untyped equivalence—in particular with polymorphism—because not only terms but also contexts have to respect types. Accordingly, our bisimulation keeps careful track of the mapping of abstract type variables to concrete types, substituting the former with the latter if and only if appropriate.

Overview. The rest of this paper is structured as follows. Section 2 presents our language and its contextual equivalence, generalized in a non-trivial way for open types as required by the technicalities which follow. Section 3 defines our bisimulation. Section 4 proves soundness and completeness of the bisimulation with respect to the generalized contextual equivalence and Section 5 gives examples to illustrate its uses. Section 6 generalizes these results, which have been restricted to closed values for simplicity, to non-values and open terms. Section 7 discusses an extension of our bisimulation concerning higher-order functions and an “up-to context” technique. Section 8 discusses related work, and Section 9 concludes with future work.

Throughout the paper, we use overbars as shorthands for sequences—e.g., we write \overline{x}, [\overline{V} /\overline{x}], (\overline{α}, \overline{σ}, \overline{σ}′) and \overline{x}: \overline{τ} instead of x_{1}, …, x_{n}, [V_{1}, …, V_{n}/x_{1}, …, x_{n}], (α_{1}, σ_{1}, σ′_{1}), …, (α_{n}, σ_{n}, σ′_{n}) and x_{1} : τ_{1}, …, x_{n}: τ_{n} where n ≥ 0.

2. GENERALIZED CONTEXTUAL EQUIVALENCE

Our language is call-by-value λ-calculus with polymorphic and recursive types. (We conjecture that it would also be straightforward to adapt our method to a call-by-name setting.) Its syntax, semantics, and typing rules are given in Figures 1, 2, and 3. We include recursive functions fix f(x: τ) : σ = M as a primitive for the sake of exposition; alternatively, they can be implemented in terms of a fixed-point operator, which is typable using recursive types. We adopt the standard notion of variable binding with implicit α-conversion and write λx: τ. M for fix f(x: τ) : σ = M when f is not free in M. We will write let x: τ = M in N for (λx: τ. N)M. We sometimes omit type annotations—as in λx. M and let x = M in N—when they are obvious from the context. The semantics is defined by the evaluation M ⇓ V of term M to value V. We choose not to evaluate under Λ (unlike [Pitts 2005], for example), though this choice is not essential for our developments. As is often the case in polymorphic λ-calculus, a type environment Γ is the union of (1) a finite set of type variables and (2) a finite map from variables to types. We write Γ, α for Γ ∪ {α} when α ∉ Γ, and Γ, x : τ for Γ ∪ {(x, τ)} when x ∉ dom(Γ), where dom(Γ) denotes \{\overline{x}\} for Γ = \{\overline{α}, (\overline{x}, \overline{τ})\}.

For simplicity, we consider the equivalence of closed values only. (This restriction entails no loss of generality: see Section 6.) However, in order to formalize the soundness and completeness of our bisimulation with respect to contextual equivalence, it helps to extend the definition of contextual equivalence to values

Journal of the ACM, Vol. V, No. N, Month 20YY.

M, N, C, D ::=  term
x  variable
fix f(x: τ) : σ = M  recursive function
MN  application
Λα. M  type function
M[τ]  type application
pack τ, M as ∃α. σ  packing
open M as α, x in N  opening
⟨M_{1}, …, M_{n}⟩  tupling
#_{i}(M)  projection
in_{i}(M)  injection
case M of in_{1}(x_{1}) ⇒ M_{1} [] … [] in_{n}(x_{n}) ⇒ M_{n}

case branch

fold(M)  folding
unfold(M)  unfolding
U, V, W ::=  value
fix f(x: τ) : σ = M  recursive function
Λα. M  type function
pack τ, V as ∃α. σ  package
⟨V_{1}, …, V_{n}⟩  tuple
in_{i}(V)  injected value
fold(V)  folded value
π, ρ, σ, τ ::=  type
α  type variable
τ → σ  function type
∀α. τ  universal type
∃α. τ  existential type
τ_{1} × … × τ_{n}  product type
τ_{1} + … + τ_{n}  sum type
μα. τ  recursive type

Fig. 1. Syntax

of open types. For instance, we will have to consider whether λx: int. x is contextually equivalent to λx: int. x − 1 at type α → int, where the implementation of abstract type α is int in fact. But this clearly depends on what values of type α (or, more generally, what values involving type α) exist in the context: for instance, if the only values of type α are 2 in the left-hand world and 3 in the right-hand world, then the equivalence does hold; however, if some integers i on the left and j on the right have type α where i ≠ j − 1, then it does not hold. In order to capture at once all such values in the context involving type α, we consider the equivalence of multiple pairs of values—annotated with their types— such as {(2, 3, α), ((λx: int. x), (λx: int. x − 1), α → int)} and {(i, j, α), ((λx: int. x), (λx: int. x − 1), α → int)}; the former should be included in the equivalence while the latter should not, provided that i ≠ j − 1. For this reason, we define a generalized form of contextual equivalence as follows.

Definition 2.1. A concretion environment Δ is a finite set of triples of the form (α, σ, σ′) with σ, σ′ closed types and (α, τ, τ′) ∈ Δ∧(α, σ, σ′) ∈ Δ ⇒ τ = σ∧τ′ = σ′.

The intuition is that, under Δ, abstract type α is implemented by concrete type σ in the left-hand side and by another concrete type σ′ in the right-hand side (of an equivalence). For instance, in the example in Section 1, the concrete imple-

Journal of the ACM, Vol. V, No. N, Month 20YY.

\overline{(fix f(x: τ) : σ = M) ⇓ (fix f(x: τ) : σ = M)} (E-Fix)

\frac{M ⇓ (fix f(x: τ) : σ = M_{0}) N ⇓ V [V/x][(fix f(x: τ) : σ = M_{0})/f]M ⇓ W}{MN ⇓ W} (E-App)

\overline{Λα. M ⇓ Λα. M} (E-TAbs) \frac{M ⇓ Λα. N [τ/α]N ⇓ V}{M[τ] ⇓ V} (E-TApp)

\frac{M ⇓ V}{pack τ, M as ∃α. σ ⇓ pack τ, V as ∃α. σ} (E-Pack)

\frac{M ⇓ pack σ, V as ∃α. τ [V/x][σ/α]N ⇓ W}{open M as α, x in N ⇓ W} (E-Open)

\frac{M_{1} ⇓ V_{1} … M_{n} ⇓ V_{n}}{⟨M_{1}, …, M_{n}⟩ ⇓ ⟨V_{1}, …, V_{n}⟩} (E-Tuple) \frac{M ⇓ ⟨V_{1}, …, V_{i}, …, V_{n}⟩}{#_{i}(M) ⇓ V_{i}} (E-Proj)

\frac{M ⇓ V}{in_{i}(M) ⇓ in_{i}(V)} (E-Inj)

\frac{M ⇓ in_{i}(V) [V/x_{i}]M_{i} ⇓ W}{case M of in_{1}(x_{1}) ⇒ M_{1} [] … [] in_{i}(x_{i}) ⇒ M_{i} [] … [] in_{n}(x_{n}) ⇒ M_{n} ⇓ W} (E-Case)

\frac{M ⇓ V}{fold(M) ⇓ fold(V)} (E-Fold) \frac{M ⇓ fold(V)}{unfold(M) ⇓ V} (E-Unfold)

Fig. 2. Semantics

mentations of abstract type α were int in the left-hand world and bool in the right-hand world, so Δ was {(α, int, bool)}. We write dom(Δ) for {α_{1}, …, α_{n}} when Δ = {(α_{1}, σ_{1}, σ′_{1}), …, (α_{n}, σ_{n}, σ′_{n})} and write Δ_{1} ⊎ Δ_{2} for Δ_{1} ∪ Δ_{2} when dom(Δ_{1}) ∩ dom(Δ_{2}) = ∅.

Definition 2.2. A typed value relation R is a (either finite or infinite) set of triples of the form (V, V′, τ).

The intuition is that R relates value V in the left-hand side and value V′ in the right-hand side at type τ.

Definition 2.3. Let Δ = {(α_{1}, σ_{1}, σ′_{1}), …, (α_{m}, σ_{m}, σ′_{m})}. We write Δ ⊢ R if, for any (V, V′, τ) ∈ R, we have ⊢ V : [\overline{σ}/\overline{α}]τ and ⊢ V′ : [\overline{σ}′/\overline{α}]τ.

Definition 2.4 Typed Value Relation in Context. We write (Δ, R)^{∘} for the relation

\{([\overline{U}/\overline{y}][\overline{σ}/\overline{α}]D, [\overline{U}′/\overline{y}][\overline{σ}′/\overline{α}]D, τ) |
Δ = {(α_{1}, σ_{1}, σ′_{1}), …, (α_{m}, σ_{m}, σ′_{m})},
(U_{1}, U′_{1}, ρ_{1}), …, (U_{n}, U′_{n}, ρ_{n}) ∈ R,
α_{1}, …, α_{m}, y_{1} : ρ_{1}, …, y_{n}: ρ_{n} ⊢ D : τ}.

Intuitively, this relation represents contexts D into which values \overline{U} and \overline{U}′, which are related by R, have been put.

Journal of the ACM, Vol. V, No. N, Month 20YY.

\frac{(x, τ) ∈ Γ}{Γ ⊢ x : τ} (T-Var)

\frac{FTV (τ) ⊆ Γ Γ, f : τ → σ, x: τ ⊢ M : σ}{Γ ⊢ (fix f(x: τ) : σ = M) : τ → σ} (T-Fix) \frac{Γ ⊢ M : τ → σ Γ ⊢ N : τ}{Γ ⊢ MN : σ} (T-App)

\frac{Γ, α ⊢ M : τ}{Γ ⊢ Λα. M : ∀α. τ} (T-TAbs) \frac{Γ ⊢ M : ∀α. σ FTV (τ) ⊆ Γ}{Γ ⊢ M[τ] : [τ/α]σ} (T-TApp)

\frac{FTV (τ) ⊆ Γ Γ ⊢ M : [τ/α]σ}{Γ ⊢ pack τ, M as ∃α. σ : ∃α. σ} (T-Pack)

\frac{Γ ⊢ M : ∃α. τ Γ, α, x: τ ⊢ N : σ α ∉ FTV (σ)}{Γ ⊢ open M as α, x in N : σ} (T-Open)

\frac{Γ ⊢ M_{1} : τ_{1} … Γ ⊢ M_{n} : τ_{n}}{Γ ⊢ ⟨M_{1}, …, M_{n}⟩ : τ_{1} × … × τ_{n}} (T-Tuple) \frac{Γ ⊢ M : τ_{1} × … × τ_{i} × … × τ_{n}}{Γ ⊢ #_{i}(M) : τ_{i}} (T-Proj)

\frac{Γ ⊢ M : τ_{i} FTV (τ_{1}) ⊆ Γ … FTV (τ_{n}) ⊆ Γ}{Γ ⊢ in_{i}(M) : τ_{1} + … + τ_{i} + … + τ_{n}} (T-Inj)

\frac{Γ ⊢ M : τ_{1} + … + τ_{n} Γ, x_{1} : τ_{1} ⊢ M_{1} : τ … Γ, x_{n}: τ_{n} ⊢ M_{n} : τ}{Γ ⊢ case M of in_{1}(x_{1}) ⇒ M_{1} [] … [] in_{n}(x_{n}) ⇒ M_{n} : τ} (T-Case)

\frac{Γ ⊢ M : [μα. τ/α]τ}{Γ ⊢ fold(M) : μα. τ} (T-Fold) \frac{Γ ⊢ M : μα. τ}{Γ ⊢ unfold(M) : [μα. τ/α]τ} (T-Unfold)

Fig. 3. Typing Rules

Definition 2.5. Generalized contextual equivalence is the set ≡ of all pairs (Δ, R) such that:

A. Δ ⊢ R. B. For any (M, M′, τ) ∈ (Δ, R)^{∘}, we have M ⇓ ⟺ M′ ⇓.

Note that the standard contextual equivalence—between two closed values of a closed type—is subsumed by the case where each Δ is empty and each R is a singleton. Conversely, the standard contextual equivalence is implied by the generalized one in the following sense: if (V, V′, τ) ∈ R for some (Δ, R) ∈ ≡ where V, V′, and τ are closed, then it is immediate by definition that K[V] ⇓ ⟺ K[V′] ⇓ for any context K with a hole [ ] for terms of type τ. More generally, if (Δ, R) ∈ ≡ for Δ = \{(\overline{α}, \overline{σ}, \overline{σ}′)\} and R = \{(\overline{V} , \overline{V}′, \overline{τ})\}, then

pack \overline{σ}, (V_{1}, …, V_{n}) as ∃\overline{α}. τ_{1} × … × τ_{n}

and

pack \overline{σ}′, (V′_{1}, …, V′_{n}) as ∃\overline{α}. τ_{1} × … × τ_{n}

are contextually equivalent in the standard sense. (A formal proof of this can be given by observing that the packages above are bisimilar as defined in Section 3.) See also Section 6 for discussions on non-values and open terms.

Journal of the ACM, Vol. V, No. N, Month 20YY.

We write

Δ ⊢ V_{1}, V_{2}, … ≡ V′_{1}, V′_{2}, …: τ_{1}, τ_{2}, …

for

(Δ, {(V_{1}, V′_{1}, τ_{1}), (V_{2}, V′_{2}, τ_{2}), …}) ∈ ≡.

We also write Δ ⊢ V ≡_{R} V′ : τ for (V, V′, τ) ∈ R with (Δ, R) ∈ ≡. Intuitively, this can be read, “values V and V′ have type τ under concretion environment Δ and are contextually equivalent under knowledge R.”

The following properties follow immediately from the definition above.

Corollary 2.6 Reflexivity. If ⊢ V_{1} : [\overline{σ}/\overline{α}]τ_{1}, ⊢ V_{2} : [\overline{σ}/\overline{α}]τ_{2}, …, then

\{(\overline{α}, \overline{σ}, \overline{σ})\} ⊢ V_{1}, V_{2}, … ≡ V_{1}, V_{2}, …: τ_{1}, τ_{2}, ….

Corollary 2.7 Symmetry. If

\{(\overline{α}, \overline{σ}, \overline{σ}′)\} ⊢ V_{1}, V_{2}, … ≡ V′_{1}, V′_{2}, …: τ_{1}, τ_{2}, …

then

\{(\overline{α}, \overline{σ}′, \overline{σ})\} ⊢ V′_{1}, V′_{2}, … ≡ V_{1}, V_{2}, …: τ_{1}, τ_{2}, ….

Corollary 2.8 Transitivity. If

\{(\overline{α}, \overline{σ}, \overline{σ}′)\} ⊢ V_{1}, V_{2}, … ≡ V′_{1}, V′_{2}, …: τ_{1}, τ_{2}, …

and

\{(\overline{α}, \overline{σ}′, \overline{σ}′′)\} ⊢ V′_{1}, V′_{2}, … ≡ V′′_{1}, V′′_{2}, …: τ_{1}, τ_{2}, …

then

\{(\overline{α}, \overline{σ}, \overline{σ}′′)\} ⊢ V_{1}, V_{2}, … ≡ V′′_{1}, V′′_{2}, …: τ_{1}, τ_{2}, ….

Example 2.9. Suppose that our language is extended in the obvious way with integers and booleans (these are, of course, definable in the language we have already given, but we prefer not to clutter examples with encodings), and let Δ = {(α, int, int)}. Then we shall have:

Δ ⊢ 2, (λx: int. x)
≡ 3, (λx: int. x − 1)
: α, (α → int)

More generally,

Δ ⊢ i, (λx: int. x)
≡ j, (λx: int. x − 1)
: α, (α → int)

if and only if i = j − 1. Formal proofs of these equivalences can be given by using the bisimulation method presented in the following sections. Intuitively, these equivalences should hold because the only way to use the values of type α is to apply the functions of type α → int.

Journal of the ACM, Vol. V, No. N, Month 20YY.

Example 2.10. Let Δ = {(α, int, bool)}. We have

Δ ⊢ 1, (λx: int. x =^{int} 0)
≡ true, (λx: bool. ¬x)
: α, (α → bool)
Δ ⊢ 1, (λx: int. x =^{int} 0)

                          ≡ false, (λx: bool. x)

: α, (α → bool)

but

Δ ⊢ 1, (λx: int. x =^{int} 0), 1, (λx: int. x =^{int} 0)
≢ true, (λx: bool. ¬x), false, (λx: bool. x)
: α, (α → bool), α, (α → bool).

Again, the first two equivalences can be proved by means of bisimulations, defined in the next section. The last inequivalence can be proved by taking D = if y_{4}y_{1} then ⊥ else 0 (or, alternatively, D = if y_{2}y_{3} then ⊥ else 0) in Definition 2.4 (and 2.5), where ⊥ is any divergent term, e.g., (fix f(x: int) : int = f x) 0.

The last example shows that, even if (Δ, R_{1}) ∈ ≡ and (Δ, R_{2}) ∈ ≡, the union (Δ, R_{1} ∪ R_{2}) does not always belong to ≡. In other words, one should not confuse two different implementations of an abstract type, even if each of them is correct in itself.

3. BISIMULATION

Contextual equivalence is difficult to prove directly, because it involves a universal quantification over arbitrary contexts. Fortunately, we can avoid considering all contexts by observing that only a few “primitive” operations can actually be performed on the values that contexts have access to: for instance, if a context is comparing a pair ⟨v, w⟩ with another pair ⟨v′, w′⟩, all it can do is to project the first elements v and v′ or the second elements w and w′ (and add them to its knowledge for later use). Similarly, in order to compare functions λx. M and λx. M′, a context has to apply them to some arguments it can make up from its knowledge. Intuitively, our bisimulations are sets of relations representing such contextual knowledge, closed under increase of knowledge via primitive operations like projection and application.

Based on the ideas above, our bisimulation is defined as follows. More detailed technical intuitions will be given after the definition.

Definition 3.1 Bisimulation. A bisimulation is a set X of pairs (Δ, R) such that:

(1 ) Δ ⊢ R. (2 ) For each

(fix f(x: π) : ρ = M, fix f(x: π′) : ρ′ = M′, τ → σ) ∈ R

Journal of the ACM, Vol. V, No. N, Month 20YY.

and for any (V, V′, τ) ∈ (Δ, R)^{∘}, we have
(fix f(x: π) : ρ = M)V ⇓
⟺ (fix f(x: π′) : ρ′ = M′)V′ ⇓.

Furthermore, if (fix f(x: π) : ρ = M)V ⇓ W and (fix f(x: π′) : ρ′ = M′)V′ ⇓

W′, then
(Δ, R ∪ {(W, W′, σ)}) ∈ X.

(3 ) Let Δ = {(α_{1}, σ_{1}, σ′_{1}), …, (α_{m}, σ_{m}, σ′_{m})}. For each

(Λα. M, Λα. M′, ∀α. τ) ∈ R

and for any ρ with FTV (ρ) ⊆ dom(Δ), we have

(Λα. M)[[\overline{σ}/\overline{α}]ρ] ⇓ ⟺ (Λα. M′)[[\overline{σ}′/\overline{α}]ρ] ⇓.

Furthermore, if (Λα. M)[[\overline{σ}/\overline{α}]ρ] ⇓ W and (Λα. M′)[[\overline{σ}′/\overline{α}]ρ] ⇓ W′, then

(Δ, R ∪ {(W, W′, [ρ/α]τ)}) ∈ X.

(4 ) For each

(pack σ, V as ∃α. τ, pack σ′, V′ as ∃α. τ′, ∃α. τ′′) ∈ R,

we have either

(Δ ⊎ {(α, σ, σ′)}, R ∪ {(V, V′, τ′′)}) ∈ X,

or else (β, σ, σ′) ∈ Δ and (V, V′, [β/α]τ′′) ∈ R for some β. (5 ) For each (⟨V_{1}, …, V_{n}⟩, ⟨V′_{1}, …, V′_{n}⟩, τ_{1} × … × τ_{n}) ∈ R and for any 1 ≤ i ≤ n,

we have (Δ, R ∪ {(V_{i}, V′_{i}, τ_{i})}) ∈ X. (6 ) For each (in_{i}(V), in_{j}(V′), τ_{1} + … + τ_{n}) ∈ R, we have i = j and (Δ, R ∪

{(V, V′, τ_{i})}) ∈ X. (7 ) For each (fold(V), fold(V′), μα. τ) ∈ R, we have (Δ, R∪{(V, V′, [μα. τ/α]τ)}) ∈

X.

As usual, bisimilarity, written ∼, is the largest bisimulation (which is the union of all bisimulations); it exists because the union of any bisimulations is again a bisimulation.

We write

Δ ⊢ V_{1}, …, V_{n} X V′_{1}, … V′_{n} : τ_{1}, …, τ_{n}

for

(Δ, {(V_{1}, V′_{1}, τ_{1}), …, (V_{n}, V′_{n}, τ_{n})}) ∈ X.

We also write Δ ⊢ V X_{R} V′ : τ for (V, V′, τ) ∈ R with (Δ, R) ∈ X. Intuitively, it can be read: values V and V′ of type τ with concretion environment Δ are bisimilar under knowledge R. (This may be reminiscent of Kripke logical relations [Mitchell 1996, page 590], but our bisimulation is not monotone about R as discussed in the introduction.)

We now elaborate the intuitions behind the definition of bisimulation. Condition 1 ensures that bisimilar values V and V′ are well typed under the concretion

Journal of the ACM, Vol. V, No. N, Month 20YY.

environment Δ. The other conditions require that the bisimulation is closed under the increase of a context’s knowledge via primitive operations, as explained below.

Condition 2 deals with the case where a context applies two functions it knows (fix f(x: π) : ρ = M and fix f(x: π′) : ρ′ = M′) to some arguments V and V′. To make up these arguments, the context can make use of any values it already knows (\overline{U} and \overline{U}′ in Definition 2.4) and assemble them using a term D with free variables \overline{y}, where the abstract types \overline{α} (in Definition 2.4) are kept abstract.

The crucial observation here is that it suffices to consider value arguments only, i.e., only the cases where the assembled terms [\overline{U}/\overline{y}][\overline{σ}/\overline{α}]D and [\overline{U}′/\overline{y}][\overline{σ}′/\overline{α}]D′ are values. This simplification is essential for proving the bisimilarity of functions. Intuitively, it can be understood via the fact that any terms of the form [\overline{U}/\overline{y}][\overline{σ}/\overline{α}]D and [\overline{U}′/\overline{y}][\overline{σ}′/\overline{α}]D evaluate to values of the same form, as proved in Lemma 4.3 below.

Then, to avoid exhibiting an observable difference in behaviors, the function applications should either both diverge or else both converge; in the latter case, the resulting values become part of the context’s knowledge and can be used for further experiments.^{2}

Condition 3 is similar to Condition 2, but for type application rather than term application.

Condition 4 is for packages defining an abstract type α. Essentially, a context can open the two packages and examine their contents only abstractly, as expressed in the first half of this condition. However, if the context happens to know another abstract type β whose implementations coincide with α’s, there is no need for us to consider them twice. The second half of the condition expresses this simplification. It is not so crucial as the previous simplification in Condition 2, but it is useful for proving the bisimulation of packages, keeping X finite in many cases despite the generativity of open, as we mentioned in the introduction.

Conditions 5, 6, and 7 are for tuples, injected values, and folded values, respectively. They capture the straightforward increase of the context’s knowledge via projection, case branch, or unfolding.

4. SOUNDNESS AND COMPLETENESS

We prove that bisimilarity coincides with contextual equivalence (in the generalized form presented in Section 2). That is, two values can be proved to be bisimilar if and only if they are contextually equivalent.

First, we prove the “if” part, i.e., that contextual equivalence is included in bisimilarity. This direction is easier because our bisimulation is defined co-inductively: it suffices simply to prove that contextual equivalence is a bisimulation.

Lemma 4.1 Completeness of Bisimulation. ≡ ⊆ ∼.

Proof. By checking that ≡ satisfies each condition of bisimulation. Details can

2Another technical point may deserve mentioning here: instead of (Δ, R ∪ {(W, W′, σ)}) ∈ X, we could require (W, W′, σ) ∈ R to reduce the number of Rs required to be in X by “predicting” the increase of contexts’ knowledge a priori. We rejected this alternative for the sake of uniformity with Condition 4, which anyway requires the concretion environment Δ to be extended. This decision does not make it difficult to construct a bisimulation, as we will see soon in the examples.

Journal of the ACM, Vol. V, No. N, Month 20YY.

be found in Appendix A.

Next, we show that bisimilarity is included in contextual equivalence. To do so, we need to consider the question: When we put bisimilar values into a context and evaluate them, what changes? The answer is: Nothing! I.e., evaluating a pair of expressions, each consisting of some set of bisimilar values placed in some context, results again in a pair of expressions that can be described by some set of bisimilar values placed in some context. Furthermore, this evaluation converges in the lefthand side if and only if it converges in the right-hand side. Since the proof of the latter property requires the former property, we formalize the observations above in the following order.

Definition 4.2 Bisimilarity in Context. We write Δ ⊢ N ∼_{R}^{∘} N′ : τ if (N, N′, τ) ∈ (Δ, R)^{∘} and (Δ, R) ∈ ∼.

The intuition is that ∼^{∘} relates bisimilar values put in contexts.

Lemma 4.3 Fundamental Property, Part I. Suppose Δ_{0} ⊢ N ∼_{R_{0}}^{∘} N′ : τ. If N ⇓ W and N′ ⇓ W′, then Δ ⊢ W ∼_{R}^{∘} W′ : τ for some Δ ⊇ Δ_{0} and R ⊇ R_{0}.

Proof. By induction on the derivation of N ⇓ W. Details are found in Appendix B.

Lemma 4.4 Fundamental Property, Part II. If Δ_{0} ⊢ N ∼_{R_{0}}^{∘} N′ : τ then N ⇓ ⟺ N′ ⇓.

Proof. By induction on the derivation of N ⇓ together with Lemma 4.3. Details are in Appendix C.

Corollary 4.5 Soundness of Bisimilarity. ∼ ⊆ ≡.

Proof. By the definitions of ≡ and ∼^{∘} together with Lemma 4.4.

Combining soundness and completeness, we obtain the main theorem about our bisimulation: that bisimilarity coincides with contextual equivalence.

Theorem 4.6. ∼ = ≡.

Proof. By Corollary 4.5 and Lemma 4.1.

Note that these proofs are much simpler than soundness proofs of applicative bisimulations in previous work [Howe 1996; Gordon 1995a; Gordon and Rees 1996; Gordon 1995b; Gordon and Rees 1995; Abramsky 1990] thanks to the generalized condition on functions (Condition 2), which is anyway required in the presence of existential polymorphism (i.e., we cannot just apply bisimilar functions to identical arguments).

5. EXAMPLES

We develop several examples illustrating concrete applications of the bisimulation method. The first three examples involve existential packages, whose equivalence cannot be proved by other bisimulations for λ-calculi. The fourth example involves recursive types with negative occurrences, for which traditional logical relations have difficulties. The last example uses higher-order functions (continuation passing style) and universal types in place of existential packages. Our bisimulation technique yields a straightforward proof of equivalence for each of the examples.

Journal of the ACM, Vol. V, No. N, Month 20YY.

5.1 Warm-Up

Consider the following simple packages

                 U = pack int, ⟨1, λx: int. x =^{int} 0⟩ as τ
                U′ = pack bool, ⟨true, λx: bool. ¬x⟩ as τ

where τ = ∃α. α × (α → bool). We aim to prove that U and U′ are contextually equivalent at type τ. To this end, let

X = {(∅, R_{0}), (Δ, R_{1}), (Δ, R_{2}), (Δ, R_{3}), (Δ, R_{4}), (Δ, R_{5})}

where

                    Δ = (α, int, bool)

R_{0} = {(U, U′, τ)}
R_{1} = R_{0} ∪ {(⟨1, λx: int. x =^{int} 0⟩,
⟨true, λx: bool. ¬x⟩,
α × (α → bool))}
R_{2} = R_{1} ∪ {(1, true, α)}
R_{3} = R_{1} ∪ {(λx: int. x =^{int} 0,
λx: bool. ¬x,

                               α → bool)}

R_{4} = R_{2} ∪ R_{3}

                   R_{5} = R_{4} ∪ {(false, false, bool)}.

Then, X is a bisimulation. To prove it, we must check each condition in Definition 3.1 for every (Δ, R) ∈ X. Most of the checks are trivial, except the following cases:

—Condition 4 on (U, U′, τ) ∈ R_{i} for i ≥ 1, where the second half of the condition

holds. —Condition 2 on

(λx: int. x =^{int} 0, λx: bool. ¬x, α → bool) ∈ R_{i}

for i ≥ 3. Since V and V′ are values with (V, V′, α) ∈ (Δ, R_{i})^{∘}, the D in Definition 2.4 is either a value or a variable. However, if D is a value, it can never satisfy the assumption α, y_{1} : ρ_{1}, …, y_{n}: ρ_{n} ⊢ D : α (easy case analysis on the syntax of D). Thus, D must be a variable. Without loss of generality, let D = y_{1}. Then, by inversion of (T-Var), ρ_{1} = α. Since (U_{1}, U′_{1}, ρ_{1}) ∈ R_{i}, we have U_{1} = 1 and U′_{1} = true. Thus, V = 1 and V′ = true, from which the rest of this condition is obvious.

Alternatively, in this particular example, we can just take X = {(Δ, R_{5})} in the first place and prove it to be a bisimulation by the same arguments as above. Since (U, U′, τ) ∈ R_{5}, this still suffices for showing the contextual equivalence of U and U′, thanks to the soundness of bisimilarity (Corollary 4.5) and the generalized definition of contextual equivalence (Definition 2.5). Simplifications like this (i.e.,

Journal of the ACM, Vol. V, No. N, Month 20YY.

taking the maximum union in the first place) are possible when the example does not involve generativity (cf. Section 5.3).

5.2 Complex Numbers

Suppose now that we have real numbers and operations in the language. Then the following two implementations U and U′ of complex numbers should be contextually equivalent at type ∃α. τ.

U = pack (real × real), ⟨id, id, cmul⟩ as ∃α. τ
U′ = pack (real × real), ⟨ctop, ptoc, pmul⟩ as ∃α. τ
τ = (real × real → α) × (α → real × real) × (α → α → α)
id = λc: real × real. c
cmul = λc_{1} : real × real. λc_{2} : real × real.
⟨#_{1}(c_{1}) × #_{1}(c_{2}) − #_{2}(c_{1}) × #_{2}(c_{2}),
#_{2}(c_{1}) × #_{1}(c_{2}) + #_{1}(c_{1}) × #_{2}(c_{2})⟩
ctop = λc: real × real.
⟨\sqrt{(#_{1}(c))^{2} + (#_{2}(c))^{2}}, atan2(#_{2}(c), #_{1}(c))⟩
ptoc = λp: real × real.
⟨#_{1}(p) × cos(#_{2}(p)), #_{1}(p) × sin(#_{2}(p))⟩
pmul = λp_{1} : real × real. λp_{2} : real × real.
⟨#_{1}(p_{1}) × #_{1}(p_{2}), #_{2}(p_{1}) + #_{2}(p_{2})⟩

The first functions in these packages make a complex number from its real and imaginary parts, and the second functions perform the converse conversion. The third functions multiply complex numbers.

To prove the contextual equivalence of U and U′, consider X = {(Δ, R)} where

               Δ = {(α, real × real, real × real)}

R = {(U, U′, ∃α. τ),

(⟨id, id, cmul⟩, ⟨ctop, ptoc, pmul⟩, τ), (id, ctop, real × real → α), (id, ptoc, α → real × real), (cmul, pmul, α → α → α)}

∪ {(v, w, α) | w = ⟨r, t⟩,
⟨r × cos(t), r × sin(t)⟩ ⇓ v,
r ≥ 0}

                  ∪ {(c, c, real × real) | ⊢ c : real × real}

∪ {(r, r, real) | ⊢ r : real}.

Then X is a bisimulation, as can be checked in the same manner as in the previous example.

Journal of the ACM, Vol. V, No. N, Month 20YY.

5.3 Functions Generating Packages

The following functions U and U′ generate packages. (I.e., they behave a bit like functors in ML-style module systems.)

U = λy: real. M
U′ = λy: real. M′

              M = pack real, ⟨y, λx: real. x⟩ as τ

M′ = pack real, ⟨y + 1.0, λx: real. x − 1.0⟩ as τ
τ = ∃α. α × (α → real)

To prove that U is contextually equivalent to U′ at type real → τ, it suffices to consider the following infinite bisimulation.

X = {(Δ, R) |
⊢ r_{i} : real for i = 0, 1, 2, ..., n,
Δ = {(β_{i}, real, real) | i = 0, 1, 2, ..., n},
R ⊆ ∪{R(i, r_{i}) | i = 0, 1, 2, ..., n}}
R(i, r) = {(U, U′, real → τ),
([r/y]M, [r/y]M′, τ),
(⟨r, λx: real. x⟩, ⟨r + 1.0, λx: real. x − 1.0⟩, β_{i} × (β_{i} → real)),
(r, r + 1.0, β_{i}),
(λx: real. x, λx: real. x − 1.0, β_{i} → real),
(r, r, real)}

The generativity of U and U′ is given a simple account by having a different abstract type β_{i} for each instantiation of U and U′ with y = r_{i}. Unlike the example in Section 5.1, we cannot take the union of all R(i, r), because it would require an uncountably infinite number of type variables in Δ.

The inclusion of all R ⊆ ∪{R(i, r_{i}) | …} in the definition of X simplifies the definition of this bisimulation; although it admits some Rs that are not strictly relevant to the proof (such as those with only the elements of tuples, but without the tuples themselves), they are not a problem since they do not violate any of the conditions of bisimulation. In other words, to prove the contextual equivalence of two values, one has only to find some bisimulation including the values rather than the minimal one.

5.4 Recursive Types with Negative Occurrence

Consider the packages C and C′ implementing counter objects as follows: each counter is implemented as a pair of its state part (of abstract type st) and its method part; the latter is implemented as a function that takes a state and returns the tuple of methods^{3}; in this example, there are two methods in the tuple: one

3This implementation can be viewed as a variant of the so-called recursive existential encoding of objects (see [Bruce et al. 1999] for details), but our goal here is to illustrate the power of our bisimulation with existential recursive types, rather than to discuss the object encoding itself.

Journal of the ACM, Vol. V, No. N, Month 20YY.

returns a new counter object with the state incremented (or, in the second implementation, decremented) by 1, while the other tells whether another counter object has been incremented (or decremented) the same number of times as the present one.

τ = ∃st. σ
σ = μself. st × (st → ρ)

ρ = self × (self → bool)
C = pack int, fold(⟨0, M ⟩) as τ
C′ = pack int, fold(⟨0, M′⟩) as τ

M = fix f(s: int) : [int/st][σ/self]ρ =
⟨fold(⟨s + 1, f)⟩,
λc: [int/st]σ. (s =^{int} #_{1}(unfold(c)))⟩
M′ = fix f(s: int) : [int/st][σ/self]ρ =
⟨fold(⟨s − 1, f⟩),
λc: [int/st]σ. (s =^{int} #_{1}(unfold(c)))⟩

Let us prove the contextual equivalence of C and C′ at type τ. To do so, we consider the bisimulation X = {(Δ, R)} where:

Δ = {(st, int, int)}

R = {(C, C′, τ),

(fold(⟨n, M⟩), fold(⟨−n, M′⟩), σ), (⟨n, M⟩, ⟨−n, M′⟩, st × (st → [σ/self]ρ)), (n, −n, st), (M, M′, st → [σ/self]ρ), (⟨fold(⟨n + 1, M⟩), λc: [int/st]σ. (n =^{int} #_{1}(unfold(c)))⟩, ⟨fold(⟨−n − 1, M′⟩), λc: [int/st]σ. (−n =^{int} #_{1}(unfold(c)))⟩, σ × (σ → bool)), (λc: [int/st]σ. (n =^{int} #_{1}(unfold(c))), λc: [int/st]σ. (−n =^{int} #_{1}(unfold(c))),

 σ → bool),
(true, true, bool),
(false, false, bool) |

n = 0, 1, 2, …}

Journal of the ACM, Vol. V, No. N, Month 20YY.

It can indeed be shown to be a bisimulation just as the bisimulations in previous examples. That is, our bisimulation incurs no difficulty for recursive functions or recursive types (with negative occurrence).

5.5 Dual of Existential Packages

The following higher-order functions represent the CPS-converted version of the example in Section 5.1.

U = λk: σ. k[int]⟨1, λx: int. x =^{int} 0⟩
U′ = λk: σ. k[bool]⟨true, λx: bool. ¬x⟩
σ = ∀α. α × (α → bool) → unit

It is straightforward to prove the contextual equivalence of U and U′ at type σ → unit, i.e.,

[U/x]C ⇓ ⟺ [U′/x]C ⇓

for any x : σ → unit ⊢ C : τ. Since

[U/x]C = [1, (λx: int. x =^{int} 0)/y, z][int/β]D_{0}
[U′/x]C = [true, (λx: bool. ¬x)/y, z][bool/β]D_{0}

for D_{0} = [(λk: σ. k[β]⟨y, z⟩)/x]C, it suffices to prove

[1, (λx: int. x =^{int} 0)/y, z][int/β]D ⇓
⟺ [true, (λx: bool. ¬x)/y, z][bool/β]D ⇓

for every β, y: β, z: β → bool ⊢ D : τ. (Note that D_{0} has the same typing as D thanks to the standard substitution lemma.) However, this follows immediately from the bisimulation {(Δ, R)} where

Δ = {(β, int, bool)}
R = {(1, true, β),

(λx: int. x =^{int} 0, λx: bool. ¬x, β → bool),

                   (false, false, bool)}

along with the soundness of bisimilarity in the previous section.

6. NON-VALUES AND OPEN TERMS

So far, we have restricted ourselves to the equivalence of closed values for the sake of simplicity. In this section, we show how our method can be used for proving the standard contextual equivalence of non-values and open terms as well. (For other studies on equivalences of open terms, see [Pitts 2000; 2005] for instance.)

A context K in the standard sense is a term with some subterm replaced by a hole [ ]. Unlike terms, (standard) contexts are not identified up to α-conversion of bound variables.

K ::= [ ] | fix f(x: τ) : σ = K | KN | MK | Λα. K | K[τ] | pack τ, K as ∃α. σ |
open K as α, x in N | open M as α, x in K | ⟨M_{1}, …, K, …, M_{n}⟩ |

Journal of the ACM, Vol. V, No. N, Month 20YY.

#_{i}(K) | in_{i}(K) | case K of in_{1}(x_{1}) ⇒ M_{1} [] … [] in_{n}(x_{n}) ⇒ M_{n} | case M of in_{1}(x_{1}) ⇒ M_{1} [] … [] in_{i}(x_{i}) ⇒ K [] … [] in_{n}(x_{n}) ⇒ M_{n} |

       fold(K) | unfold(K)

We write K[M] for the term obtained by substituting the hole in K with M (which does not apply α-conversion and may capture free variables). Then, the standard contextual equivalence

α_{1}, …, α_{m}, x_{1} : τ_{1}, …, x_{n}: τ_{n} ⊢ M ≡^{std} M′ : τ

for well-typed terms \overline{α}, \overline{x}: \overline{τ} ⊢ M : τ and \overline{α}, \overline{x}: \overline{τ} ⊢ M′ : τ can be defined as: K[M] ⇓ ⟺ K[M′] ⇓ for every context K with ⊢ K[M] : unit and ⊢ K[M′] : unit, where unit is the nullary product type. (In fact, any closed, non-empty type works in place of unit.)

We will show that the standard contextual equivalence above holds if and only if the closed values V = Λ\overline{α}. λ\overline{x}: \overline{τ}. M and V′ = Λ\overline{α}. λ\overline{x}: \overline{τ}. M′ are bisimilar, i.e.,

∅ ⊢ Λα_{1}…. Λα_{m}. λx_{1} : τ_{1}…. λx_{n}: τ_{n}. M
∼ Λα_{1}…. Λα_{m}. λx_{1} : τ_{1}…. λx_{n}: τ_{n}. M′
: ∀α_{1}…. ∀α_{m}. τ_{1} → … → τ_{n} → τ.

(If M and M′ have no free term/type variables at all, it suffices just to take V = Λα. M and V′ = Λα. M′ for any type variable α.) The “only if” direction is obvious from the definitions of contextual equivalences—both the standard one above and the generalized one in Section 2—and from the completeness of bisimulation. To prove the “if” direction, suppose ∅ ⊢ V ∼ V′ : ∀\overline{α}. \overline{τ} → τ. By the soundness of bisimulation, we have ∅ ⊢ V ≡ V′ : ∀\overline{α}. \overline{τ} → τ. Given any K with ⊢ K[M] : unit and ⊢ K[M′] : unit, take C = K[z[α_{1}] … [α_{m}]x_{1} … x_{n}] for fresh z. Then, it suffices to prove K[M] ⇓ ⟺ [V/z]C ⇓ and K[M′] ⇓ ⟺ [V′/z]C ⇓.

To this end, we prove the more general lemma below in order for induction to work. The intuition is that a term M and its β-expanded version (Λ\overline{α}. λ\overline{x}: \overline{τ}. M)[\overline{α}]\overline{x} should behave equivalently under any context. Since the free type/term variables \overline{α} and \overline{x} are to be substituted by some types/values during evaluation under a context, this “β-expansion” relation needs to be generalized to allow nesting. Thus, we define:

Definition 6.1 β-Expansion. Γ ⊢ M ⪯ M′ : τ is the smallest (typed and substitution-closed) congruence relation between λ-terms that satisfies:

\frac{Γ ⊢ M ⪯ M′ : ρ \{\overline{α}\} ⊆ dom(Γ) Γ ⊢ \overline{x} : \overline{τ}}{Γ ⊢ M ⪯ (Λ\overline{α}. λ\overline{x}: \overline{τ}. M′)[\overline{α}]\overline{x} : ρ} (B-Exp)

Then, we can prove:

Lemma 6.2. For any

α_{1}, …, α_{m}, x_{1} : τ_{1}, …, x_{n}: τ_{n} ⊢ M ⪯ M′ : τ,

for any closed σ_{1}, …, σ_{m}, and for any (⊢ V_{1} ⪯ V′_{1} : [\overline{σ}/\overline{α}]τ_{1}) ∧ … ∧ (⊢ V_{n} ⪯ V′_{n} : [\overline{σ}/\overline{α}]τ_{n}), we have

[\overline{V} /\overline{x}][\overline{σ}/\overline{α}]M ⇓ ⟺ [\overline{V}′/\overline{x}][\overline{σ}/\overline{α}]M′ ⇓.

Journal of the ACM, Vol. V, No. N, Month 20YY.

Furthermore, if [\overline{V} /\overline{x}][\overline{σ}/\overline{α}]M ⇓ W and [\overline{V}′/\overline{x}][\overline{σ}/\overline{α}]M′ ⇓ W′, then ⊢ W ⪯ W′ : [\overline{σ}/\overline{α}]τ.

Proof. By induction on the derivations of \overline{α}, \overline{x}: \overline{τ} ⊢ M ⪯ M′ : τ and [\overline{V} /\overline{x}][\overline{σ}/\overline{α}]M ⇓ W (or [\overline{V}′/\overline{x}][\overline{σ}/\overline{α}]M′ ⇓ W′).

Lemma 6.3. For any Γ ⊢ M : τ,

(1 ) Γ ⊢ M ⪯ M : τ, (2 ) Γ ⊢ M ⪯ (Λ\overline{α}. λ\overline{x}. M)[\overline{α}]\overline{x} : τ, and (3 ) ⊢ K[M] ⪯ K[(Λ\overline{α}. λ\overline{x}. M)[\overline{α}]\overline{x}] : unit for any K with ⊢ K[M] : unit.

Proof. Immediate from Definition 6.1.

Theorem 6.4. For any \overline{α}, \overline{x}: \overline{τ} ⊢ M : τ and \overline{α}, \overline{x}: \overline{τ} ⊢ M′ : τ, if ⊢ Λ\overline{α}. λ\overline{x}: \overline{τ}.

M ∼ Λ\overline{α}. λ\overline{x}: \overline{τ}. M′ : ∀\overline{α}. \overline{τ} → τ, then \overline{α}, \overline{x}: \overline{τ} ⊢ M ≡^{std} M′ : τ.

Proof. By the soundness of bisimulation, we have [(Λ\overline{α}. λ\overline{x}: \overline{τ}. M)/z]C ⇓ ⟺ [(Λ\overline{α}. λ\overline{x}: \overline{τ}. M′)/z]C for any well-typed C. Thus, given K, take C = K[z[\overline{α}]\overline{x}] and we get K[(Λ\overline{α}. λ\overline{x}: \overline{τ}. M)[\overline{α}]\overline{x}] ⇓ ⟺ K[(Λ\overline{α}. λ\overline{x}: \overline{τ}. M′)[\overline{α}]\overline{x}] ⇓. Meanwhile, by Lemma 6.3 (3), we have ⊢ K[M] ⪯ K[(Λ\overline{α}. λ\overline{x}: \overline{τ}. M)[\overline{α}]\overline{x}] : unit and ⊢ K[M′] ⪯ K[(Λ\overline{α}. λ\overline{x}: \overline{τ}. M′)[\overline{α}]\overline{x}] : unit. By Lemma 6.2, we obtain K[M] ⇓ ⟺ K[(Λ\overline{α}. λ\overline{x}: \overline{τ}. M)[\overline{α}]\overline{x}] ⇓ and K[M′] ⇓ ⟺ K[(Λ\overline{α}. λ\overline{x}: \overline{τ}. M′)[\overline{α}]\overline{x}] ⇓. Hence K[M] ⇓ ⟺ K[M′] ⇓.

Example 6.5. We have x: int ⊢ x + 1 ≡^{std} 1 + x : int. That is, x + 1 and 1 + x are contextually equivalent (in the standard sense above) at type int provided that x has type int. To show this, it suffices to prove ∅ ⊢ λx: int. x + 1 ∼ λx: int. 1 + x : int → int, which is trivial.

Example 6.6. The packages

              M = pack real, ⟨y, λx: real. x⟩ as τ

M′ = pack real, ⟨y + 1.0, λx: real. x − 1.0⟩ as τ

are contextually equivalent (again in the standard sense above) at type

τ = ∃α. α × (α → real)

provided that y has type real. This follows from the bisimilarity of λy: real. M and λy: real. M′, shown in Section 5.3.

Although these examples are trivial, other examples of open terms can be treated in the same way, i.e., by means of closing abstractions.

7. EXTENSION FOR HIGHER-ORDER FUNCTIONS AND “UP-TO CONTEXT”

Although the contextual equivalence proof of higher-order functions in Section 5.5 was particularly simple, the trick used there (i.e., factoring out the common part λk: σ. k[β]⟨y, z⟩ of the two terms U, U′ into context D) does not apply in general. For example, consider the following implementations of integer multisets with a

Journal of the ACM, Vol. V, No. N, Month 20YY.

higher-order function to compute a weighed sum of all elements. (We assume standard definitions of lists and binary trees.)

       IntSet = pack intList, (Nil, add, weigh) as ∃α. τ
       IntSet′ = pack intTree, (Leaf, add′, weigh′) as ∃α. τ

τ = α × (int → α → α) × ((int → real) → α → real)

          add = λi: int. λs: intList. Cons(i, s)
          add′ = λi: int. fix f(s: intTree) : intTree =

                   case s of Leaf ⇒ Node(i, Leaf, Leaf)

[] Node(j, s_{1}, s_{2}) ⇒ if i < j then Node(j, fs_{1}, s_{2})

else Node(j, s_{1}, fs_{2})

        weigh = λg: int → real. fix f(s: intList) : real =

case s of Nil ⇒ 0 [] Cons(j, s_{0}) ⇒ gj + fs_{0}

        weigh′ = λg: int → real. fix f(s: intTree) : real =

case s of Leaf ⇒ 0 [] Node(j, s_{1}, s_{2}) ⇒ gj + fs_{1} + fs_{2}

Unlike the previous example, these implementations have no syntactic similarity, which disables the simple proof. Instead, we have to put the whole packages into the bisimulation along with their elements. Then, by Condition 2 of bisimulation, we need at least to prove weigh V W ⇓ ⟺ weigh′ V′ W′ ⇓ for a certain class of V, W, V′, and W′. In particular, V and V′ can be of the forms λz: int. [IntSet/y]D and λz: int. [IntSet′/y]D for any D of appropriate type. Thus, because of the function application gj in weigh and weigh′, we must prove

[IntSet, j/y, z]D ⇓ ⟺ [IntSet′, j/y, z]D ⇓

for every D (and j). We are stuck, however, since this subsumes the definition of IntSet ≡ IntSet′ and is harder to prove!

Resolving this problem requires weakening Condition 2. Recall that the fundamental properties of our bisimulations—that evaluation preserves ∼^{∘} and that ∼^{∘} respects convergence—were proved by structural induction on the evaluation derivations. Specifically, Condition 2 was used in sub-case M_{4} = x_{1_{i}} of case E-App in the proof of Lemma 4.3 (and 4.4). By further exploiting the induction hypothesis in this proof, we obtain the following weaker yet sound condition. (Difference from Condition 2 is shown in bold.)

(2′) Take any

(fix f(x: π) : ρ = M, fix f(x: π′) : ρ′ = M′, τ → σ) ∈ R

and any (V, V′, τ) ∈ (Δ, R)^{∘}. Assume that, for any

N ⊏ (fix f(x: π) : ρ = M)V
N′ ⊏ (fix f(x: π′) : ρ′ = M′)V′

with (N, N′, σ) ∈ (Δ_{0}, R_{0})^{∘} and (Δ_{0}, R_{0}) ∈ X, we have N ⇓ ⟺ N′ ⇓. Assume furthermore that, if N ⇓ U and N′ ⇓ U′, then (U, U′, σ) ∈ (Δ_{1}, R_{1})^{∘} for some Δ_{1} ⊇ Δ_{0} and R_{1} ⊇ R_{0} with (Δ_{1}, R_{1}) ∈ X. Then, we

Journal of the ACM, Vol. V, No. N, Month 20YY.

have

(fix f(x: π) : ρ = M)V ⇓
⟺ (fix f(x: π′) : ρ′ = M′)V′ ⇓.

Furthermore, if (fix f(x: π) : ρ = M)V ⇓ W and (fix f(x: π′) : ρ′ = M′)V ⇓ W′, then (W, W′, σ) ∈ (Δ_{2}, R_{2})^{∘} for some Δ_{2} ⊇ Δ and R_{2} ⊇ R with (Δ_{2}, R_{2}) ∈ X.

Here, N_{1} ⊏ N_{2} means that, if N_{2} ⇓, then N_{1} ⇓ and the evaluation derivation for N_{2} is strictly taller than that for N_{1}. (This is reminiscent of indexed models and indexed logical relations [Appel and McAllester 2001; Ahmed et al. 2003; Ahmed 2006]. However, we consider the height of derivation only in the case of higherorder functions, while they carry indices throughout the definitions—in particular for recursive types—and proofs.)

This generalization seems quite powerful: for instance, it allows us to conclude that gj in weigh and weigh′ gives the same result when g is substituted by V or V′. Although the condition above has X in a negative position ((Δ_{1}, R_{1}) ∈ X) and breaks the monotonicity property (the union of two bisimulations may no longer be a bisimulation), we still have soundness^{4} and completeness (≡ is still a bisimulation because Condition 2′ is weaker than Condition 2). In fact, thanks to these soundness and completeness properties, ≡ is the largest bisimulation.

Coincidentally, the last part of Condition 2′—that is, (W, W′, σ) ∈ (Δ_{2}, R_{2})^{∘} with (Δ_{2}, R_{2}) ∈ X, in place of (Δ, R ∪ {(W, W′, σ)}) ∈ X—also simplifies some bisimulation proofs for first-order functions. Intuitively, this is an “up-to context” technique: instead of (W, W′, σ) ∈ R_{2} for some (Δ_{2}, R_{2}) ∈ X, one only needs to prove (W, W′, σ) ∈ (Δ_{2}, R_{2})^{∘}, which reduces the size of X as in the following example:

Example 7.1. Let τ = μα. unit + int × α. Then the function

M = fix f(x: τ) : τ =

                   case unfold(x) of in_{1}( ) ⇒ fold(in_{1}(⟨⟩))

[] in_{2}(y) ⇒ fold(in_{2}(#_{1}(y), f(#_{2}(y))))

is bisimilar to the identity M′ = λx: τ. x at type τ → τ. To prove this, take X = {(∅, R)} with R = {(M, M′, τ → τ)}. To prove Condition 2′ (other conditions are trivial), let (V, V′, τ) ∈ (∅, R)^{∘}, i.e., V = [M/z]D and V′ = [M′/z]D for z: τ → τ ⊢ D : τ. By easy induction on the syntax of D, we have that D has no free variable, so V = V′ = D with ⊢ D : τ in fact. Again by straightforward induction on the syntax of V, we have MV ⇓ V for any ⊢ V : τ. This concludes the proof since (V, V, τ) ∈ (∅, R)^{∘} by Definition 2.4.

If the up-to context technique were not available, we would have to include in R the identity relation at type τ, because of the original requirement in Condition 2 that

4The proofs of Lemma 4.3 and 4.4 remain valid just by replacing the phrase “by induction on the derivation” with “by induction on the height of the derivation.” In fact, as stated above, Condition 2′ is derived by analyzing these proofs, so that it is sound by construction. See also Koutavas and Wand [2006b] for a more detailed presentation of this derivation.

Journal of the ACM, Vol. V, No. N, Month 20YY.

(V, V, τ) ∈ R. Worse, we would also have to include identities at unit + int × τ, int × τ, int and unit because of other conditions of bisimulation for values of recursive, product, sum, and primitive types. “Up-to context” liberates us from these (easy but boring) burdens.

The following examples are similar to Example 7.1 in essence, but more nontrivial.

Example 7.2. Let τ = μα. unit → int × α and

            ones = fold(fix f( : unit) : int × τ = ⟨1, fold(f)⟩)
            twos = fold(fix f( : unit) : int × τ = ⟨2, fold(f)⟩)

succ = fix f(s: τ) : τ =

                     let c: int × τ = unfold(s)⟨⟩ in

fold(λ : unit. ⟨1 + #_{1}(c), f(#_{2}(c))⟩).

Then twos is bisimilar to twos′ for succ ones ⇓ twos′. To prove this, take X = {(∅, R)} for R = {(twos, twos′, τ), (M, M′, unit → int × τ)} with

M = fix f( : unit) : int × τ = ⟨2, fold(f)⟩
M′ = λ : unit. ⟨1 + #_{1}(⟨1, ones⟩), succ(#_{2}(⟨1, ones⟩))⟩.

Condition 7 (bisimulation for values of recursive types) is immediate from the definition of R. For Condition 2′, we apply M and M’ to ⟨⟩, obtaining ⟨2, twos⟩ and ⟨2, twos′⟩, respectively. These values are again in (∅, R)^{∘}, which concludes the proof.

Example 7.3. Let τ = μα. unit + (α → α) and

M = fix f(x: τ) : τ =

                   case unfold(x) of in_{1}( ) ⇒ fold(in_{1}(⟨⟩))

[] in_{2}(g) ⇒ fold(in_{2}(λy: τ. f(g(fy)))).

We prove that M is bisimilar to an identify function M′ = λx: τ. x. Let X = {(∅, R)}, where R is the smallest set such that (M, M′, τ → τ) ∈ R and (λy: τ. M(U(My)), U′, τ → τ) ∈ R for any (U, U′, τ → τ) ∈ (∅, R)^{∘}.

First, by Condition 2′, we must apply M and M′ to V and V′, respectively, for any (V, V′, τ) ∈ (∅, R)^{∘}. By an easy case analysis as in Example 7.1, we have either V = V′ = fold(in_{1}(⟨⟩)), or else V = fold(in_{2}(U)) and V′ = fold(in_{2}(U′)) for (U, U′, τ → τ) ∈ (∅, R)^{∘}. The former case is trivial. In the latter case, MV and M′V′ evaluate to fold(in_{2}(λy: τ. M(U(My)))) and fold(in_{2}(U′)), respectively. We are done since these values are already in (∅, R)^{∘}.

Second, again by Condition 2′, we must apply λy: τ. M(U(My)) and U′ to V and V′, respectively, for any (U, U′, τ → τ), (V, V′, τ) ∈ (∅, R)^{∘}. Again, the non-trivial case is when V = fold(in_{2}(W)) and V′ = fold(in_{2}(W′)) for (W, W′, τ → τ) ∈ (∅, R)^{∘}. Then, MV ⇓ fold(in_{2}(λy: τ. M(W (My)))). Let this value be V′′. Let furthermore U = λx: τ. N and U′ = λx: τ. N′. Then, (V′′, V′, τ), (N, N′, τ) ∈ (∅, R)^{∘}, so [V′′/x]N and [V′/x]N′ are also in (∅, R)^{∘}. Thus, by the assumption of Condition 2′, we have [V′′/x]N ⇓ V_{0} and [V′/x]N′ ⇓ V′_{0} with (V_{0}, V′_{0}, τ) ∈ (∅, R)^{∘} (or both evaluations diverge). The rest of the proof—that MV_{0} and V′_{0} evaluate to values in (∅, R)^{∘}—is the same as the first case above.

Journal of the ACM, Vol. V, No. N, Month 20YY.

8. RELATED WORK

Variants of our bisimulation. Recently, Koutavas and Wand adapted our bisimulation to λ-calculus with ML-like references and store [Koutavas and Wand 2006b]. In addition, they gave a clearer account of our condition for higher-order functions in Section 7. They furthermore applied this approach to an untyped imperative object calculus [Koutavas and Wand 2006a] and a Java-like language with private members [Koutavas and Wand 2007]. These results give a new solution to the classical problem of proving contextual equivalence in such languages [Meyer and Sieber 1988; Pitts and Stark 1993; 1998]. They also showed that our bisimulation can be adapted for languages with small-step semantics [Koutavas and Wand 2007].

Sangiorgi, Kobayashi and Sumii [2007] developed various up-to techniques for our style of bisimulations (e.g., bisimulations that apply bisimilar functions to arguments of the forms C[\overline{V}] and C[\overline{V}′] for bisimilar \overline{V} and \overline{V}′), which simplifies contextual equivalence proofs of higher-order functions as well. They applied those techniques to pure call-by-name λ-calculus, imperative call-by-value λ-calculus, and pure higher-order π-calculus. Although their languages are untyped, it would be straightforward to combine their techniques into typed languages like ours, as their developments do not depend on the type system (or lack of it).

Semantic logical relations. Originally, logical relations were devised in denotational semantics for relating models of λ-calculus. Although they are indeed useful for this purpose (e.g., relating CPS semantics and direct-style semantics), they are not as useful for proving contextual equivalence or abstraction properties, for the following reasons. First, denotational semantics tend to require more complex mathematics (such as CPOs and categories) than operational semantics. Second, it is hard—though not impossible [Hughes 1997]—to define a model of polymorphic λ-calculus that preserves equivalence.

Logical relations for polymorphic λ-calculus are also useful for proving parametricity properties [Wadler 1989], e.g., that all functions of type ∀α. α → α behave like the polymorphic identity function (or diverge, if there is recursion in the language). Our bisimulation can also derive such properties for existential types. For example, any package p = pack σ, v as τ of type τ = ∃α. α can be proved contextually equivalent to p′ = pack unit, ⟨⟩ as τ, by taking X = {(∅, R_{1}), (Δ, R_{2})} where R_{1} = {(p, p′, τ)}, Δ = {(α, σ, unit)} and R_{2} = R_{1} ∪ {(v, ⟨⟩, α)}. However, for universal types, we would have to change Condition 3 to something like

(3′) Let Δ = {(α_{1}, σ_{1}, σ′_{1}), …, (α_{m}, σ_{m}, σ′_{m})}. For each

(Λα. M, Λα. M′, ∀α. τ) ∈ R

and for any ρ and ρ′ with FTV (ρ) ⊆ dom(Δ) and FTV (ρ′) ⊆ dom(Δ), we have

(Λα. M)[[\overline{σ}/\overline{α}]ρ] ⇓ ⟺ (Λα. M′)[[\overline{σ}′/\overline{α}]ρ′] ⇓.

Furthermore, if (Λα. M)[[\overline{σ}/\overline{α}]ρ] ⇓ W and (Λα. M′)[[\overline{σ}′/\overline{α}]ρ′] ⇓ W′, then

(Δ ∪ \{(α, [\overline{σ}/\overline{α}]ρ, [\overline{σ}′/\overline{α}]ρ′)\}, R ∪ R_{1} ∪ \{(W, W′, τ)\}) ∈ X

for any R_{1} ⊆ \{([\overline{σ}/\overline{α}]W_{1}, [\overline{σ}′/\overline{α}]W′_{1}, α) | \overline{α} ⊢ W_{1} : ρ ∧ \overline{α} ⊢ W′_{1} : ρ′\}.

Journal of the ACM, Vol. V, No. N, Month 20YY.

in order to keep track of all the values of type α, as in logical relations for universal types. We conjecture that soundness (and completeness) of such a condition would be just as difficult to establish as those for logical relations. In particular, reflexivity would be a main challenge (like the fundamental theorem for logical relations).

Syntactic logical relations. Pitts [2000] proposed syntactic logical relations, which use only the term model of polymorphic λ-calculus to prove contextual equivalence. He introduced the notion of ⊤⊤-closure—based on a Galois connection between terms and contexts (for a term relation r, stack relation r^{⊤} denotes the set of pairs of stacks that behave equivalently for all the pairs of terms in r, and for a stack relation s, term relation s^{⊤} denotes the set of pairs of terms that behave equivalently for all the pairs of stacks in s)—in order to treat recursive functions without using denotational semantics. He proved that his syntactic logical relations are complete with respect to contextual equivalence in call-by-name polymorphic λ-calculus with recursive functions and universal types (and lists).

Pitts [2005] also proposed syntactic logical relations for call-by-value λ-calculus with recursive functions, universal types, and existential types. Although he showed (by a counter-example) that his proof principles based on logical relations are incomplete [Pitts 2005, Remark 7.7.4] and attributed the incompleteness to the presence of divergence, we have shown that a similar counter-example can be given without using divergence [Pitts 2005, Remark 7.7.7]. Recently, Derek Dreyer [personal communication, February 2006] suggested yet another counter-example

          ⊢ (pack bool, λf. f true ∧ ¬(f false) as τ)

≡^{?} (pack int, λf. f 1 =^{int} 1 ∧ f 2 =^{int} 2 ∧ f 3 =^{int} 3 as τ) : τ

where τ = ∃α. (α → α) → bool. The contextual equivalences in these examples are hard to prove, either with logical relations or with our bisimulations. Pitts gave a “brute force” proof of contextual equivalence for the first example [Pitts 2005, page 283, line 23], while no formal proof has been published for the other examples. (Although our bisimulations are complete in the sense that the bisimilarity coincides with generalized contextual equivalence, this does not mean an automatic proof for every instance of contextual equivalence, which is an undecidable problem.)

Birkedal and Harper [1999] and Crary and Harper [2007] extended syntactic logical relations with recursive types by proving certain unwinding properties. The latter work treated existential types via encoding into universal types (though this treatment is still incomplete and cannot prove the examples above [Crary and Harper 2007, Section 6.4]).

Melliés and Vouillon [2005] developed an operational model of λ-calculus with (semantic versions of) universal, existential, and recursive types, using a form of ⊤⊤-closure (biorthogonality) and interpreting types as the limits of converging sequences of partial types (interval types). They also outlined relational versions of the model, which characterizes contextual equivalence of (syntactically) typed λ-terms. They leave state and concurrency to future work.

Applicative bisimulations. Abramsky [1990] proposed applicative bisimulations for proving contextual equivalence of untyped λ-terms. Gordon [1995a; 1995b] and Gordon and Rees [1996; 1995] adapted applicative bisimulations to calculi with

Journal of the ACM, Vol. V, No. N, Month 20YY.

objects, subtyping, universal polymorphism, and recursive types. As discussed in Section 1, however, these results do not apply to type abstraction using existential types. We solved this issue by considering sets of relations as bisimulations.

As a byproduct, it has become much easier to prove the soundness of our bisimulation (than the standard method for proving the soundness of applicative bisimulations [Howe 1996]). Technically, this simplification is due to the generalization for functions (Condition 2 in Definition 3.1), where we allow different arguments C[\overline{V}] and C[\overline{V}′] while applicative bisimulation requires them to be the same.

Bisimulations for polymorphic π-calculi. Pierce and Sangiorgi [2000] developed a bisimulation proof technique for polymorphic π-calculus, using a separate environment for representing contexts’ knowledge. In a sense, our bisimulation unifies the environmental knowledge with the bisimulation itself by generalizing the latter as a set of relations. Because of the imperative nature of π-calculus, their bisimulation is far from complete—in particular, aliasing of names is problematic.

Berger et al. [2003] defined two equivalence proof methods for linear π-calculi, one based on the syntactic logical relations of Pitts [2005; 2000] and the other based on the bisimulations of Pierce and Sangiorgi [2000]. Their main goal is to give a generic account for various features such as functions, state and concurrency by encoding them into appropriate versions of linear π-calculi. They proved soundness and completeness of their logical relations for one of the linear π-calculi, which directly corresponds to polymorphic λ-calculus (without recursion). They also proved full abstraction of the call-by-value and call-by-name encodings of the polymorphic λcalculus to this version of linear π-calculus. However, for the other settings (e.g., with recursive functions or types), full abstraction of encodings and completeness of their logical relations are unclear. Completeness of their bisimulations is not discussed either. In addition, their developments are much heavier than ours for the purpose of just proving the equivalence of typed λ-terms.

Bisimulations for cryptographic calculi. Various bisimulations [Abadi and Gordon 1998; Abadi and Fournet 2001; Boreale et al. 2002; Borgström and Nestmann 2002] have been proposed for extensions of π-calculus with cryptographic primitives [Abadi and Gordon 1999; Abadi and Fournet 2001]. Their main idea is similar to Pierce and Sangiorgi’s: using a separate environment to represent attackers’ knowledge. In previous work [Sumii and Pierce 2004], we have applied our idea of using sets of relations as bisimulations to an extension of λ-calculus with perfect encryption (also known as dynamic sealing) and obtained a sound and complete characterization of contextual equivalence in this setting. Although this extension was untyped, it is straightforward to combine the present work with the previous one and obtain a bisimulation for typed λ-calculus with perfect encryption. The fact that our idea applies to such apparently different forms of information hiding as encryption and type abstraction might suggest that it is successful in capturing the essence of “information hiding” in programming languages and computation models.

Journal of the ACM, Vol. V, No. N, Month 20YY.

9. CONCLUSION

We have presented a (characterization and) proof method for contextual equivalence of existential packages in λ-calculus with full recursive types, based on bisimulations generalized as sets of relations.

Although full automation is impossible because equivalence of λ-terms (with recursion) is undecidable, some mechanical support would be useful.

Another direction of future work is to extend the calculus with more complex features such as state (cf. [Pitts and Stark 1998; Bierman et al. 2000; Koutavas and Wand 2006b]). For example, it would be possible to treat state by passing around the state throughout the evaluation of terms and their bisimulation. More ambitiously, one could imagine generalizing this state-passing approach to more general “monadic bisimulation” by formalizing effects via monads [Moggi 1991].

Yet another possibility is to adopt our idea of “sets of relations as bisimulations” to other higher-order calculi with information hiding—such as higherorder π-calculus [Sangiorgi 1992], where restriction hides names and complicates equivalence—and compare the outcome with context bisimulation. Sangiorgi et al.

[2007] gives a first result in this course.

Finally, as suggested in the previous section, the idea of considering sets of relations as bisimulations may be useful for other forms of information hiding such as secrecy typing [Heintze and Riecke 1998]. It would be interesting to see whether such an adaptation is indeed possible and, furthermore, to consider if these variations can be generalized into a unified theory of information hiding.

APPENDIX

A. PROOF OF LEMMA 4.1

The lemma to prove was: ≡ ⊆ ∼.

Since ∼ is the greatest bisimulation, it suffices to check that ≡ is a bisimulation by checking each condition of bisimulation. Take any (Δ, R) ∈ ≡ with Δ = \{(\overline{α}, \overline{σ}, \overline{σ}′)\}. Then, from the definition of ≡, we have:

A_{0}. ⊢ V_{0} : [\overline{σ}/\overline{α}]τ_{0} and ⊢ V′_{0} : [\overline{σ}′/\overline{α}]τ_{0} for any (V_{0}, V′_{0}, τ_{0}) ∈ R, and

B_{0}. [\overline{V}_{0}/\overline{x}_{0}][\overline{σ}/\overline{α}]C_{0} ⇓ ⟺ [\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′/\overline{α}]C_{0} ⇓ for any (\overline{V}_{0}, \overline{V} ′_{0}, \overline{τ}_{0}) ∈ R and for any \overline{α}, \overline{x}_{0} : \overline{τ}_{0} ⊢ C_{0} : τ_{0}.

We now check the conditions in the definition of bisimulation.

Condition 1: Immediate, since it is just the same as A_{0}.

Condition 2: Suppose that

((fix f(x: π) : ρ = M), (fix f(x: π′) : ρ′ = M′), τ → σ) ∈ R

and that V = [\overline{U}/\overline{y}][\overline{σ}/\overline{α}]D and V′ = [\overline{U}′/\overline{y}][\overline{σ}′/\overline{α}]D with (\overline{U}, \overline{U}′, \overline{ρ}) ∈ R and \overline{α}, \overline{y}: \overline{ρ} ⊢ D : τ. Then,

(fix f(x: π) : ρ = M)V ⇓ ⟺ (fix f(x: π′) : ρ′ = M′)V′ ⇓

follows from B_{0} by taking (for fresh g):

C_{0} = gD
\overline{x}_{0} = g, \overline{y}

Journal of the ACM, Vol. V, No. N, Month 20YY.

\overline{τ}_{0} = τ → σ, \overline{ρ}
\overline{V}_{0} = (fix f(x: π) : ρ = M), \overline{U}
\overline{V} ′_{0} = (fix f(x: π′) : ρ′ = M′), \overline{U}′

Suppose furthermore that (fix f(x: π) : ρ = M)V ⇓ W and (fix f(x: π′) : ρ′ = M′)V′ ⇓ W′. Then

(Δ, R ∪ {(W, W′, σ)}) ∈ ≡

will follow from the definition of ≡ if we can prove:

A_{2}. ⊢ V_{2} : [\overline{σ}/\overline{α}]τ_{2} and ⊢ V′_{2} : [\overline{σ}′/\overline{α}]τ_{2} for any (V_{2}, V′_{2}, τ_{2}) ∈ R ∪ \{(W, W′, σ)\}, and

B_{2}. [\overline{V}_{2}/\overline{x}_{2}][\overline{σ}/\overline{α}]C_{2} ⇓ ⟺ [\overline{V} ′_{2}/\overline{x}_{2}][\overline{σ}′/α]C_{2} ⇓ for any (\overline{V}_{2}, \overline{V} ′_{2}, \overline{τ}_{2}) ∈ R∪\{(W, W′, σ)\} and for any \overline{α}, \overline{x}_{2} : \overline{τ}_{2} ⊢ C_{2} : τ_{2}.

But A_{2} follows from A_{0} in the case where (V_{2}, V′_{2}, τ_{2}) is drawn from R and from type preservation in the case where (V_{2}, V′_{2}, τ_{2}) = (W, W′, σ). B_{2} holds as follows: without loss of generality, let (V_{2_{1}}, V′_{2_{1}}, τ_{2_{1}}) = (W, W′, σ) and (V_{2_{i}}, V′_{2_{i}}, τ_{2_{i}}) ∈ R for 2 ≤ i ≤ n; then, it suffices to take in B_{0} (for fresh g)

C_{0} = let x_{2_{1}} = gD in C_{2}
\overline{x}_{0} = g, \overline{y}, x_{2_{2}}, …, x_{2_{n}}
\overline{τ}_{0} = τ → σ, \overline{ρ}, τ_{2_{2}}, …, τ_{2_{n}}
\overline{V}_{0} = (fix f(x: π) : ρ = M), \overline{U}, V_{2_{2}}, …, V_{2_{n}}
\overline{V} ′_{0} = (fix f(x: π′) : ρ′ = M′), \overline{U}′, V′_{2_{2}}, …, V′_{2_{n}}

so that the evaluations of [\overline{V}_{0}/\overline{x}_{0}][\overline{σ}/\overline{α}]C_{0} and [\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′/\overline{α}]C_{0} amount to the evaluations of [\overline{V}_{2}/\overline{x}_{2}][\overline{σ}/\overline{α}]C_{2} and [\overline{V} ′_{2}/\overline{x}_{2}][\overline{σ}′/\overline{α}]C_{2} as below.

\frac{\begin{matrix}[(fix f(x: π) : ρ = M), \overline{U}/g, \overline{y}][\overline{σ}/\overline{α}](gD) ⇓ W \\ [W, V_{2_{2}}, …, V_{2_{n}}/x_{2_{1}}, x_{2_{2}}, …, x_{2_{n}}][\overline{σ}/\overline{α}]C_{2} ⇓ \end{matrix}}{[(fix f(x: π) : ρ = M), \overline{U}, V_{2_{2}}, …, V_{2_{n}}/g, \overline{y}, x_{2_{2}}, …, x_{2_{n}}][\overline{σ}/\overline{α}](let x_{2_{1}} = gD in C_{2}) ⇓}

\frac{\begin{matrix}[(fix f(x: π′) : ρ′ = M′), \overline{U}′/g, \overline{y}][\overline{σ}′/\overline{α}](gD) ⇓ W′ \\ [W′, V′_{2_{2}}, …, V′_{2_{n}}/x_{2_{1}}, x_{2_{2}}, …, x_{2_{n}}][\overline{σ}′/\overline{α}]C_{2} ⇓ \end{matrix}}{[(fix f(x: π′) : ρ′ = M′), \overline{U}′, V′_{2_{2}}, …, V′_{2_{n}}/g, \overline{y}, x_{2_{2}}, …, x_{2_{n}}][\overline{σ}′/\overline{α}](let x_{2_{1}} = gD in C_{2}) ⇓}

Condition 3: Suppose that

(Λα. M, Λα. M′, ∀α. τ) ∈ R

and that FTV (ρ) ⊆ dom(Δ). Then

(Λα. M)[[\overline{σ}/\overline{α}]ρ] ⇓ ⟺ (Λα. M′)[[\overline{σ}′/\overline{α}]ρ] ⇓

follows from B_{0} by taking (for fresh g):

C_{0} = g[ρ]
\overline{x}_{0} = g
\overline{τ}_{0} = ∀α. τ

Journal of the ACM, Vol. V, No. N, Month 20YY.

\overline{V}_{0} = Λα. M
\overline{V} ′_{0} = Λα. M′

Suppose furthermore that (Λα. M)[[\overline{σ}/\overline{α}]ρ] ⇓ W and (Λα. M′)[[\overline{σ}′/\overline{α}]ρ] ⇓ W′. Then

(Δ, R ∪ {(W, W′, [ρ/α]τ)}) ∈ ≡

will follow from the definition of ≡ if we can prove:

A_{3}. ⊢ V_{3} : [\overline{σ}/\overline{α}]τ_{3} and ⊢ V′_{3} : [\overline{σ}′/\overline{α}]τ_{3} for any (V_{3}, V′_{3}, τ_{3}) ∈ R ∪ \{(W, W′, [ρ/α]τ)\},

and B_{3}. [\overline{V}_{3}/\overline{x}_{3}][\overline{σ}/\overline{α}]C_{3} ⇓ ⟺ [\overline{V} ′_{3}/\overline{x}_{3}][\overline{σ}′/\overline{α}]C_{3} ⇓ for any (\overline{V}_{3}, \overline{V} ′_{3}, \overline{τ}_{3}) ∈ R∪\{(W, W′, [ρ/α]τ)\}

and for any \overline{α}, \overline{x}_{3} : \overline{τ}_{3} ⊢ C_{3} : τ_{3}.

But A_{3} follows from A_{0} in the case where (V_{3}, V′_{3}, τ_{3}) is drawn from R and from type preservation in the case where (V_{3}, V′_{3}, τ_{3}) = (W, W′, [ρ/α]τ). B_{3} holds as follows: without loss of generality, let (V_{3_{1}}, V′_{3_{1}}, τ_{3_{1}}) = (W, W′, [ρ/α]τ) and (V_{3_{i}}, V′_{3_{i}}, τ_{3_{i}}) ∈ R for 2 ≤ i ≤ n; then, it suffices to take in B_{0} (for fresh g)

C_{0} = let x_{3_{1}} = g[ρ] in C_{3}
\overline{x}_{0} = g, x_{3_{2}}, …, x_{3_{n}}
\overline{τ}_{0} = ∀α. τ, τ_{3_{2}}, …, τ_{3_{n}}
\overline{V}_{0} = Λα. M, V_{3_{2}}, …, V_{3_{n}}
\overline{V} ′_{0} = Λα. M′, V′_{3_{2}}, …, V′_{3_{n}}

so that the evaluations of [\overline{V}_{0}/\overline{x}_{0}][\overline{σ}/\overline{α}]C_{0} and [\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′/\overline{α}]C_{0} amount to the evaluations of [\overline{V}_{3}/\overline{x}_{3}][\overline{σ}/\overline{α}]C_{3} and [\overline{V} ′_{3}/\overline{x}_{3}][\overline{σ}′/\overline{α}]C_{3} as below.

\frac{\begin{matrix}[Λα. M/g][\overline{σ}/\overline{α}](g[ρ]) ⇓ W \\ [W, V_{3_{2}}, …, V_{3_{n}}/x_{3_{1}}, x_{3_{2}}, …, x_{3_{n}}][\overline{σ}/\overline{α}]C_{3} ⇓ \end{matrix}}{[Λα. M, V_{3_{2}}, …, V_{3_{n}}/g, x_{3_{2}}, …, x_{3_{n}}][\overline{σ}/\overline{α}](let x_{3_{1}} = g[ρ] in C_{3}) ⇓}

\frac{\begin{matrix}[Λα. M′/g][\overline{σ}′/\overline{α}](g[ρ]) ⇓ W′ \\ [W′, V′_{3_{2}}, …, V′_{3_{n}}/x_{3_{1}}, x_{3_{2}}, …, x_{3_{n}}][\overline{σ}′/\overline{α}]C_{3} ⇓ \end{matrix}}{[Λα. M′, V′_{3_{2}}, …, V′_{3_{n}}/g, x_{3_{2}}, …, x_{3_{n}}][\overline{σ}′/\overline{α}](let x_{3_{1}} = g[ρ] in C_{3}) ⇓}

Condition 4: Suppose that

((pack σ, V as ∃α. τ), (pack σ′, V′ as ∃α. τ′), ∃α. τ′′) ∈ R.

Then,

(Δ ⊎ {(α, σ, σ′)}, R ∪ {(V, V′, τ′′)}) ∈ ≡

follows from the definition of ≡ if we prove:

A_{4}. ⊢ V_{4} : [\overline{σ}, σ/\overline{α}, α]τ_{4} and ⊢ V′_{4} : [\overline{σ}′, σ′/\overline{α}, α]τ_{4} for any (V_{4}, V′_{4}, τ_{4}) ∈ R ∪ {(V, V′, τ′′)}, and

B_{4}. [\overline{V}_{4}/\overline{x}_{4}][\overline{σ}, σ/\overline{α}, α]C_{4} ⇓ ⟺ [\overline{V} ′_{4}/\overline{x}_{4}][\overline{σ}′, σ/\overline{α}, α]C_{4} ⇓ for any (\overline{V}_{4}, \overline{V} ′_{4}, \overline{τ}_{4}) ∈

R ∪ \{(V, V′, τ′′)\} and for any \overline{α}, α, \overline{x}_{4} : \overline{τ}_{4} ⊢ C_{4} : τ_{4}.

Journal of the ACM, Vol. V, No. N, Month 20YY.

But A_{4} follows from A_{0} in the case where (V_{4}, V′_{4}, τ_{4}) is drawn from R and, in the case where (V_{4}, V′_{4}, τ_{4}) = (V, V′, τ′′), by inversion of (T-Pack) with

⊢ pack σ, V as ∃α. τ : [\overline{σ}/\overline{α}](∃α. τ′′)

and

⊢ pack σ′, V′ as ∃α. τ′ : [\overline{σ}′/\overline{α}](∃α. τ′′),

which follow from A_{0} with

((pack σ, V as ∃α. τ), (pack σ′, V′ as ∃α. τ′), ∃α. τ′′) ∈ R.

B_{4} holds as follows: without loss of generality, let (V_{4_{1}}, V′_{4_{1}}, τ_{4_{1}}) = (V, V′, τ′′) and (V_{4_{i}}, V′_{4_{i}}, τ_{4_{i}}) ∈ R for 2 ≤ i ≤ n; then, it suffices to take in B_{0} (for fresh p)

C_{0} = open p as α, x_{4_{1}} in C_{4}
\overline{x}_{0} = p, x_{4_{2}}, …, x_{4_{n}}
\overline{τ}_{0} = ∃α. τ′′, τ_{4_{2}}, …, τ_{4_{n}}
\overline{V}_{0} = pack σ, V as ∃α. τ, V_{4_{2}}, …, V_{4_{n}}
\overline{V} ′_{0} = pack σ′, V′ as ∃α. τ′, V′_{4_{2}}, …, V′_{4_{n}}

so that the evaluations of [\overline{V}_{0}/\overline{x}_{0}][\overline{σ}/\overline{α}]C_{0} and [\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′/\overline{α}]C_{0} amount to the evaluations of [\overline{V}_{4}/\overline{x}_{4}][\overline{σ}, σ/\overline{α}, α]C_{4} and [\overline{V} ′_{4}/\overline{x}_{4}][\overline{σ}′, σ′/\overline{α}, α]C_{4} as below.

\frac{[V, V_{4_{2}}, …, V_{4_{n}}/x_{4_{1}}, x_{4_{2}}, …, x_{4_{n}}][\overline{σ}, σ/\overline{α}, α]C_{4} ⇓}{[pack σ, V as ∃α. τ, V_{4_{2}}, …, V_{4_{n}}/p, x_{4_{2}}, …, x_{4_{n}}][\overline{σ}/\overline{α}](open p as α, x_{4_{1}} in C_{4}) ⇓}

\frac{[V′, V′_{4_{2}}, …, V′_{4_{n}}/x_{4_{1}}, x_{4_{2}}, …, x_{4_{n}}][\overline{σ}′, σ′/\overline{α}, α]C_{4} ⇓}{[pack σ′, V′ as ∃α. τ, V′_{4_{2}}, …, V′_{4_{n}}/p, x_{4_{2}}, …, x_{4_{n}}][\overline{σ}′/\overline{α}](open p as α, x_{4_{1}} in C_{4}) ⇓}

Proofs of the other conditions are similar. □

B. PROOF OF LEMMA 4.3

The lemma to prove was: Suppose Δ_{0} ⊢ N ∼_{R_{0}}^{∘} N′ : τ. If N ⇓ W and N′ ⇓ W′, then Δ ⊢ W ∼_{R}^{∘} W′ : τ for some Δ ⊇ Δ_{0} and R ⊇ R_{0}.

The proof is by induction on the derivation of N ⇓ W.

By the definition of ∼^{∘}, we have

N = [\overline{V}_{0}/\overline{x}_{0}][\overline{σ}_{0}/\overline{α}_{0}]M_{0}

and

N′ = [\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′_{0}/\overline{α}_{0}]M_{0}

for some

Δ_{0} ⊢ \overline{V}_{0} ∼_{R_{0}} \overline{V} ′_{0} : \overline{τ}_{0}

and

\overline{α}_{0}, \overline{x}_{0} : \overline{τ}_{0} ⊢ M_{0} : τ

with Δ_{0} = \{(\overline{α}_{0}, \overline{σ}_{0}, \overline{σ}′_{0})\}. If N is a value, then N′ is also a value (easy case analysis on the syntax of M_{0}) and the result is immediate, because every value evaluates

Journal of the ACM, Vol. V, No. N, Month 20YY.

only to itself. We consider the remaining possibilities—where M_{0} is neither a value nor a variable—in detail; there is one case for each of the non-value evaluation rules. Case (E-Open). Then M_{0} has the form

M_{0} = open M_{1} as α, y in M_{2}

and the given evaluation derivations have the forms:

\frac{\begin{matrix}[\overline{V}_{0}/\overline{x}_{0}][\overline{σ}_{0}/\overline{α}_{0}]M_{1} ⇓ pack ρ_{1}, W_{1} as ∃α. ρ_{2} \\ [W_{1}/y][ρ_{1}/α][\overline{V}_{0}/\overline{x}_{0}][\overline{σ}_{0}/\overline{α}_{0}]M_{2} ⇓ W \end{matrix}}{[\overline{V}_{0}/\overline{x}_{0}][\overline{σ}_{0}/\overline{α}_{0}](open M_{1} as α, y in M_{2}) ⇓ W}

\frac{\begin{matrix}[\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′_{0}/\overline{α}_{0}]M_{1} ⇓ pack ρ′_{1}, W′_{1} as ∃α. ρ′_{2} \\ [W′_{1}/y][ρ′_{1}/α][\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′_{0}/\overline{α}_{0}]M_{2} ⇓ W′ \end{matrix}}{[\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′_{0}/\overline{α}_{0}](open M_{1} as α, y in M_{2}) ⇓ W′}

By inversion of (T-Open), we have

\overline{α}_{0}, \overline{x}_{0} : \overline{τ}_{0} ⊢ M_{1} : ∃α. ρ′′_{2}

and

\overline{α}_{0}, \overline{x}_{0} : \overline{τ}_{0}, α, y: ρ′′_{2} ⊢ M_{2} : τ

with α ∉ FTV (τ). Thus, by the definition of ∼^{∘}, we have

Δ_{0} ⊢ [\overline{V}_{0}/\overline{x}_{0}][\overline{σ}_{0}/\overline{α}]M_{1} ∼_{R_{0}}^{∘} [\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′_{0}/\overline{α}]M_{1} : ∃α. ρ′′_{2}.

Therefore, by the induction hypothesis, we have

Δ_{1} ⊢ pack ρ_{1}, W_{1} as ∃α. ρ_{2} ∼_{R_{1}}^{∘} pack ρ′_{1}, W′_{1} as ∃α. ρ′_{2} : ∃α. ρ′′_{2}

for some Δ_{1} ⊇ Δ_{0} and R_{1} ⊇ R_{0}. Then, by the definition of ∼^{∘}, we have

pack ρ_{1}, W_{1} as ∃α. ρ_{2} = [\overline{V}_{1}/\overline{x}_{1}][\overline{σ}_{1}/\overline{α}_{1}]M_{3}

and

pack ρ′_{1}, W′_{1} as ∃α. ρ′_{2} = [\overline{V} ′_{1}/\overline{x}_{1}][\overline{σ}′_{1}/\overline{α}_{1}]M_{3}

for some

Δ_{1} ⊢ \overline{V}_{1} ∼_{R_{1}} \overline{V} ′_{1} : \overline{τ}_{1}

and

\overline{α}_{1}, \overline{x}_{1} : \overline{τ}_{1} ⊢ M_{3} : ∃α. ρ′′_{2}

with Δ_{1} = \{(\overline{α}_{1}, \overline{σ}_{1}, \overline{σ}′_{1})\}. Sub-case M_{3} = (pack ρ′′_{1}, M_{4} as ∃α. ρ′′_{2}). Then

W_{1} = [\overline{V}_{1}/\overline{x}_{1}][\overline{σ}_{1}/\overline{α}_{1}]M_{4}
W′_{1} = [\overline{V} ′_{1}/\overline{x}_{1}][\overline{σ}′_{1}/α_{1}]M_{4}

and

ρ_{1} = [\overline{σ}_{1}/\overline{α}_{1}]ρ′′_{1}
ρ′_{1} = [\overline{σ}′_{1}/\overline{α}_{1}]ρ′′_{1}.

Journal of the ACM, Vol. V, No. N, Month 20YY.

Since we have

\overline{α}_{1}, \overline{x}_{1} : \overline{τ}_{1} ⊢ M_{4} : [ρ′′_{1}/α]ρ′′_{2}

by inversion of (T-Pack), we have

\overline{α}_{1}, \overline{x}_{0} : \overline{τ}_{0}, \overline{x}_{1} : \overline{τ}_{1} ⊢ [M_{4}/y][ρ′′_{1}/α]M_{2} : τ

by weakening and the substitution lemmas for types and terms. Therefore, by the definition of ∼^{∘}, we have

Δ_{1} ⊢ [\overline{V}_{0}, \overline{V}_{1}/\overline{x}_{0}, \overline{x}_{1}][\overline{σ}_{1}/\overline{α}_{1}][M_{4}/y][ρ′′_{1}/α]M_{2} ∼_{R_{1}}^{∘} [\overline{V} ′_{0}, \overline{V}_{1}/\overline{x}_{0}, \overline{x}_{1}][\overline{σ}′_{1}/\overline{α}_{1}][M_{4}/y][ρ′′_{1}/α]M_{2} : τ.

Since

[\overline{V}_{0}, \overline{V}_{1}/\overline{x}_{0}, \overline{x}_{1}][\overline{σ}_{1}/\overline{α}_{1}][M_{4}/y][ρ′′_{1}/α]M_{2}
= [([\overline{V}_{1}/\overline{x}_{1}][\overline{σ}_{1}/\overline{α}_{1}]M_{4})/y][([\overline{σ}_{1}/\overline{α}_{1}]ρ′′_{1})/α][\overline{V}_{0}/\overline{x}_{0}][\overline{σ}_{0}/\overline{α}_{0}]M_{2}
= [W_{1}/y][ρ_{1}/α][\overline{V}_{0}/\overline{x}_{0}][\overline{σ}_{0}/\overline{α}_{0}]M_{2}

and

[\overline{V} ′_{0}, \overline{V} ′_{1}/\overline{x}_{0}, \overline{x}_{1}][\overline{σ}′_{1}/\overline{α}_{1}][M_{4}/y][ρ′′_{1}/α]M_{2}
= [([\overline{V} ′_{1}/\overline{x}_{1}][\overline{σ}′_{1}/\overline{α}_{1}]M_{4})/y][([\overline{σ}′_{1}/\overline{α}_{1}]ρ′′_{1})/α][\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′_{0}/\overline{α}_{0}]M_{2}
= [W′_{1}/y][ρ′_{1}/α][\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′_{0}/\overline{α}_{0}]M_{2},

we have

Δ_{2} ⊢ W ∼_{R_{2}}^{∘} W′ : τ

for some Δ_{2} ⊇ Δ_{1} and R_{2} ⊇ R_{1} by the induction hypothesis.

Sub-case M_{3} = x_{1_{i}}. Then

V_{1_{i}} = pack ρ_{1}, W_{1} as ∃α. ρ_{2}
V′_{1_{i}} = pack ρ′_{1}, W′_{1} as ∃α. ρ′_{2}.

Since

Δ_{1} ⊢ V_{1_{i}} ∼_{R_{1}} V′_{1_{i}} : τ_{1_{i}},

we have the following two possibilities by Condition 4 of bisimulation.

Sub-sub-case (β, ρ_{1}, ρ′_{1}) ∈ Δ_{1} and (W_{1}, W′_{1}, [β/α]ρ′′_{2}) ∈ R_{1}. Since we have

\overline{α}_{0}, \overline{x}_{0} : \overline{τ}_{0}, α, y: ρ′′_{2} ⊢ M_{2} : τ

with α ∉ FTV (τ), we have

\overline{α}_{0}, \overline{x}_{0} : \overline{τ}_{0}, β, y: [β/α]ρ′′_{2} ⊢ [β/α]M_{2} : τ.

Then, we have

Δ_{1} ⊢ [\overline{V}_{0}, W_{1}/\overline{x}_{0}, y][\overline{σ}_{1}/\overline{α}_{1}][β/α]M_{2} ∼_{R_{1}}^{∘} [\overline{V} ′_{0}, W′_{1}/\overline{x}_{0}, y][\overline{σ}′_{1}/\overline{α}_{1}][β/α]M_{2} : τ

by the definition of ∼^{∘}. Since we have β = α_{1_{i}} with ρ_{1} = σ_{1_{i}} and ρ′_{1} = σ′_{1_{i}} for some i, we have

[\overline{V}_{0}, W_{1}/\overline{x}_{0}, y][\overline{σ}_{1}/\overline{α}_{1}][β/α]M_{2} = [W_{1}/y][ρ_{1}/α][\overline{V}_{0}/\overline{x}_{0}][\overline{σ}_{0}/\overline{α}_{0}]M_{2}

Journal of the ACM, Vol. V, No. N, Month 20YY.

A Bisimulation for Type Abstraction and Recursion · 33

and

[\overline{V} ′_{0}, W′_{1}/\overline{x}_{0}, y][\overline{σ}′_{1}/\overline{α}_{1}][β/α]M_{2} = [W′_{1}/y][ρ′_{1}/α][\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′_{0}/\overline{α}_{0}]M_{2},

so we have

Δ_{2} ⊢ W ∼_{R_{2}}^{∘} W′ : τ

for some Δ_{2} ⊇ Δ_{1} and R_{2} ⊇ R_{1} by the induction hypothesis. Sub-sub-case (Δ_{1} ⊎ {(α, ρ_{1}, ρ′_{1})}, R_{1} ∪ {(W_{1}, W′_{1}, ρ′′_{2})}) ∈ ∼. Then we have

Δ_{2} ⊢ [\overline{V}_{0}, W_{1}/\overline{x}_{0}, y][\overline{σ}_{0}, ρ_{1}/\overline{α}_{0}, α]M_{2} ∼_{R_{2}}^{∘} [\overline{V} ′_{0}, W′_{1}/\overline{x}_{0}, y][\overline{σ}′_{0}, ρ′_{1}/\overline{α}_{0}, α]M_{2} : τ

for Δ_{2} = Δ_{1} ∪ {(α, ρ_{1}, ρ′_{1})} and R_{2} = R_{1} ∪ {(W_{1}, W′_{1}, ρ′′_{2})} by the definition of ∼^{∘}. Since we have

[\overline{V}_{0}, W_{1}/\overline{x}_{0}, y][\overline{σ}_{0}, ρ_{1}/\overline{α}_{0}, α]M_{2} = [W_{1}/y][ρ_{1}/α][\overline{V}_{0}/\overline{x}_{0}][\overline{σ}_{0}/\overline{α}_{0}]M_{2}

and

[\overline{V} ′_{0}, W′_{1}/\overline{x}_{0}, y][\overline{σ}′_{0}, ρ′_{1}/\overline{α}_{0}, α]M_{2} = [W′_{1}/y][ρ′_{1}/α][\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′_{0}/\overline{α}_{0}]M_{2},

we have

Δ_{3} ⊢ W ∼_{R_{3}}^{∘} W′ : τ

for some Δ_{3} ⊇ Δ_{2} and R_{3} ⊇ R_{2} by the induction hypothesis. Case (E-Pack). Then M_{0} has the form

M_{0} = pack ρ_{1}, M_{1} as ∃α. ρ_{2}

and the given evaluation derivations have the forms

\frac{[\overline{V}_{0}/\overline{x}_{0}][\overline{σ}_{0}/\overline{α}_{0}]M_{1} ⇓ W_{1}}{[\overline{V}_{0}/\overline{x}_{0}][\overline{σ}_{0}/\overline{α}_{0}](pack ρ_{1}, M_{1} as ∃α. ρ_{2}) ⇓ pack [\overline{σ}_{0}/\overline{α}_{0}]ρ_{1}, W_{1} as [\overline{σ}_{0}/\overline{α}_{0}](∃α. ρ_{2})}

\frac{[\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′_{0}/\overline{α}_{0}]M_{1} ⇓ W′_{1}}{[\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′_{0}/\overline{α}_{0}](pack ρ_{1}, M_{1} as ∃α. ρ_{2}) ⇓ pack [\overline{σ}′_{0}/\overline{α}_{0}]ρ_{1}, W′_{1} as [\overline{σ}′_{0}/\overline{α}_{0}](∃α. ρ_{2})}

where

W = pack [\overline{σ}_{0}/\overline{α}_{0}]ρ_{1}, W_{1} as [\overline{σ}_{0}/\overline{α}_{0}](∃α. ρ_{2})

and

W′ = pack [\overline{σ}′_{0}/\overline{α}_{0}]ρ_{1}, W′_{1} as [\overline{σ}′_{0}/\overline{α}_{0}](∃α. ρ_{2}).

By inversion of (T-Pack), we have

\overline{α}_{0}, \overline{x}_{0} : \overline{τ}_{0} ⊢ M_{1} : [ρ_{1}/α]ρ_{2}

with τ = ∃α. ρ_{2}. Thus, by the definition of ∼^{∘}, we have

Δ_{0} ⊢ [\overline{V}_{0}/\overline{x}_{0}][\overline{σ}_{0}/\overline{α}_{0}]M_{1} ∼_{R_{0}}^{∘} [\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′_{0}/\overline{α}_{0}]M_{1} : [ρ_{1}/α]ρ_{2}.

Then, by the induction hypothesis, we have

Δ_{1} ⊢ W_{1} ∼_{R_{1}}^{∘} W′_{1} : [ρ_{1}/α]ρ_{2}

Journal of the ACM, Vol. V, No. N, Month 20YY.

34 · E. Sumii and B. C. Pierce

for some Δ_{1} ⊇ Δ_{0} and R_{1} ⊇ R_{0}. Therefore, by the definition of ∼^{∘}, we have

W_{1} = [\overline{V}_{1}/\overline{x}_{1}][\overline{σ}_{1}/\overline{α}_{1}]M_{2}
W′_{1} = [\overline{V} ′_{1}/\overline{x}_{1}][\overline{σ}′_{1}/\overline{α}_{1}]M_{2}

for some

Δ_{1} ⊢ \overline{V}_{1} ∼_{R_{1}} \overline{V} ′_{1} : \overline{τ}_{1}

and

\overline{α}_{1}, \overline{x}_{1} : \overline{τ}_{1} ⊢ M_{2} : [ρ_{1}/α]ρ_{2}

with Δ_{1} = \{(\overline{α}_{1}, \overline{σ}_{1}, \overline{σ}′_{1})\}. Thus, by (T-Pack), we have

\overline{α}_{1}, \overline{x}_{1} : \overline{τ}_{1} ⊢ M_{3} : ∃α. ρ_{2}

for

M_{3} = pack ρ_{1}, M_{2} as ∃α. ρ_{2}.

Then, by the definition of ∼^{∘}, we have

Δ_{1} ⊢ [\overline{V}_{1}/\overline{x}_{1}][\overline{σ}_{1}/\overline{α}_{1}]M_{3} ∼_{R_{1}}^{∘} [\overline{V} ′_{1}/\overline{x}_{1}][\overline{σ}′_{1}/\overline{α}_{1}]M_{3} : ∃α. ρ_{2},

i.e.,

Δ_{1} ⊢ W ∼_{R_{1}}^{∘} W′ : τ.

Case (E-TApp). Then M_{0} has the form

M_{0} = M_{1}[ρ_{1}]

and the given evaluation derivations have the forms:

\frac{\begin{matrix}[\overline{V}_{0}/\overline{x}_{0}][\overline{σ}_{0}/\overline{α}_{0}]M_{1} ⇓ Λα. M_{2} \\ [([\overline{σ}_{0}/\overline{α}_{0}]ρ_{1})/α]M_{2} ⇓ W \end{matrix}}{[\overline{V}_{0}/\overline{x}_{0}][\overline{σ}_{0}/\overline{α}_{0}](M_{1}[ρ_{1}]) ⇓ W} ; \frac{\begin{matrix}[\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′_{0}/\overline{α}_{0}]M_{1} ⇓ Λα. M′_{2} \\ [([\overline{σ}′_{0}/\overline{α}_{0}]ρ_{1})/α]M′_{2} ⇓ W′ \end{matrix}}{[\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′_{0}/\overline{α}_{0}](M_{1}[ρ_{1}]) ⇓ W′}

By inversion of (T-TApp), we have

\overline{α}_{0}, \overline{x}_{0} : \overline{τ}_{0} ⊢ M_{1} : ∀α. ρ_{2}

with τ = [ρ_{1}/α]ρ_{2}. Thus, by the definition of ∼^{∘}, we have

Δ_{0} ⊢ [\overline{V}_{0}/\overline{x}_{0}][\overline{σ}_{0}/\overline{α}_{0}]M_{1} ∼_{R_{0}}^{∘} [\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′_{0}/\overline{α}_{0}]M_{1} : ∀α. ρ_{2}.

Then, by the induction hypothesis, we have

Δ_{1} ⊢ Λα. M_{2} ∼_{R_{1}}^{∘} Λα. M′_{2} : ∀α. ρ_{2}

Journal of the ACM, Vol. V, No. N, Month 20YY.

for some Δ_{1} ⊇ Δ_{0} and R_{1} ⊇ R_{0}. Therefore, by the definition of ∼^{∘}, we have

Λα. M_{2} = [\overline{V}_{1}/\overline{x}_{1}][\overline{σ}_{1}/\overline{α}_{1}]M_{3}
Λα. M′_{2} = [\overline{V} ′_{1}/\overline{x}_{1}][\overline{σ}′_{1}/\overline{α}_{1}]M_{3}

for some

Δ_{1} ⊢ \overline{V}_{1} ∼_{R_{1}} \overline{V} ′_{1} : \overline{τ}_{1}

and

\overline{α}_{1}, \overline{x}_{1} : \overline{τ}_{1} ⊢ M_{3} : ∀α. ρ_{2}

with Δ_{1} = \{(\overline{α}_{1}, \overline{σ}_{1}, \overline{σ}′_{1})\}. Sub-case M_{3} = Λα. M′′_{2}. Then, by inversion of (T-TAbs), we have

\overline{α}_{1}, \overline{x}_{1} : \overline{τ}_{1}, α ⊢ M′′_{2} : ρ_{2}.

By the substitution lemma for types, we have

\overline{α}_{1}, \overline{x}_{1} : \overline{τ}_{1} ⊢ [ρ_{1}/α]M′′_{2} : [ρ_{1}/α]ρ_{2}.

By the definition of ∼^{∘}, we have

Δ_{1} ⊢ [\overline{V}_{1}/\overline{x}_{1}][\overline{σ}_{1}/\overline{α}_{1}][ρ_{1}/α]M′′_{2} ∼_{R_{1}}^{∘} [\overline{V} ′_{1}/\overline{x}_{1}][\overline{σ}′_{1}/\overline{α}_{1}][ρ_{1}/α]M′′_{2} : [ρ_{1}/α]ρ_{2},

i.e.,

Δ_{1} ⊢ [([\overline{σ}_{0}/\overline{α}_{0}]ρ_{1})/α]M_{2} ∼_{R_{1}}^{∘} [([\overline{σ}′_{0}/\overline{α}_{0}]ρ_{1})/α]M′_{2} : τ.

(Recall FTV (ρ_{1}) ⊆ \{\overline{α}_{0}\} and Δ_{1} = \{(\overline{α}_{1}, \overline{σ}_{1}, \overline{σ}′_{1})\} ⊇ Δ_{0} = \{(\overline{α}_{0}, \overline{σ}_{0}, \overline{σ}′_{0})\}.) Again by the induction hypothesis, we have

Δ_{2} ⊢ W ∼_{R_{2}}^{∘} W′ : τ

for some Δ_{2} ⊇ Δ_{1} and R_{2} ⊇ R_{1}. Sub-case M_{3} = x_{1_{i}}. Then

V_{1_{i}} = Λα. M_{2}
V′_{1_{i}} = Λα. M′_{2}

and τ_{1_{i}} = ∀α. ρ_{2}. Since we have

(Λα. M_{2})[[\overline{σ}_{1}/\overline{α}_{1}]ρ_{1}] ⇓ W

and

(Λα. M′_{2})[[\overline{σ}′_{1}/\overline{α}_{1}]ρ_{1}] ⇓ W′

with

Δ_{1} ⊢ Λα. M_{2} ∼_{R_{1}} Λα. M′_{2} : ∀α. ρ_{2},

we have

(Δ_{1}, R_{1} ∪ {(W, W′, τ)}) ∈ ∼

by Condition 3 of bisimulation. (Recall τ = [ρ_{1}/α]ρ_{2}.) Thus, we have

Δ_{1} ⊢ W ∼_{R_{2}}^{∘} W′ : τ

for R_{2} = R_{1} ∪ {(W, W′, τ)} by the definition of ∼^{∘}.

Journal of the ACM, Vol. V, No. N, Month 20YY.

36 · E. Sumii and B. C. Pierce

Case (E-App). Then M_{0} has the form

M_{0} = M_{1}M_{2}

and the given evaluation derivations have the forms:

\frac{\begin{matrix}[\overline{V}_{0}/\overline{x}_{0}][\overline{σ}_{0}/\overline{α}_{0}]M_{1} ⇓ (fix f(x: π) : ρ = M_{3}) \\ [\overline{V}_{0}/\overline{x}_{0}][\overline{σ}_{0}/\overline{α}_{0}]M_{2} ⇓ W_{1} \\ [W_{1}/x][(fix f(x: π) : ρ = M_{3})/f]M_{3} ⇓ W \end{matrix}}{[\overline{V}_{0}/\overline{x}_{0}][\overline{σ}_{0}/\overline{α}_{0}](M_{1}M_{2}) ⇓ W}

\frac{\begin{matrix}[\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′_{0}/\overline{α}_{0}]M_{1} ⇓ (fix f(x: π′) : ρ′ = M′_{3}) \\ [\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′_{0}/\overline{α}_{0}]M_{2} ⇓ W′_{1} \\ [W′_{1}/x][(fix f(x: π′) : ρ′ = M′_{3})/f]M′_{3} ⇓ W′ \end{matrix}}{[\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′_{0}/\overline{α}_{0}](M_{1}M_{2}) ⇓ W′}

By inversion of (T-App), we have

\overline{α}_{0}, \overline{x}_{0} : \overline{τ}_{0} ⊢ M_{1} : σ → τ

and

\overline{α}_{0}, \overline{x}_{0} : \overline{τ}_{0} ⊢ M_{2} : σ

for some σ. Thus, by the definition of ∼^{∘}, we have

Δ_{0} ⊢ [\overline{V}_{0}/\overline{x}_{0}][\overline{σ}_{0}/\overline{α}_{0}]M_{1} ∼_{R_{0}}^{∘} [\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′_{0}/\overline{α}_{0}]M_{1} : σ → τ.

Then, by the induction hypothesis, we have

Δ_{1} ⊢ fix f(x: π) : ρ = M_{3} ∼_{R_{1}}^{∘} fix f(x: π′) : ρ′ = M′_{3} : σ → τ

for some Δ_{1} ⊇ Δ_{0} and R_{1} ⊇ R_{0}. Therefore, by the definition of ∼^{∘}, we have

fix f(x: π) : ρ = M_{3} = [\overline{V}_{1}/\overline{x}_{1}][\overline{σ}_{1}/\overline{α}_{1}]M_{4}
fix f(x: π′) : ρ′ = M′_{3} = [\overline{V} ′_{1}/\overline{x}_{1}][\overline{σ}′_{1}/\overline{α}_{1}]M_{4}

for some

Δ_{1} ⊢ \overline{V}_{1} ∼_{R_{1}} \overline{V} ′_{1} : \overline{τ}_{1}

and

\overline{α}_{1}, \overline{x}_{1} : \overline{τ}_{1} ⊢ M_{4} : σ → τ

with Δ_{1} = \{(\overline{α}_{1}, \overline{σ}_{1}, \overline{σ}′_{1})\}.

Meanwhile, by weakening, we have

\overline{α}_{1}, \overline{x}_{0} : \overline{τ}_{0} ⊢ M_{2} : σ.

Thus, by the definition of ∼^{∘}, we have

Δ_{1} ⊢ [\overline{V}_{0}/\overline{x}_{0}][\overline{σ}_{0}/\overline{α}_{0}]M_{2} ∼_{R_{1}}^{∘} [\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′_{0}/\overline{α}_{0}]M_{2} : σ

since Δ_{1} ⊇ Δ_{0} and R_{1} ⊇ R_{0}. Then, by the induction hypothesis, we have

Δ_{2} ⊢ W_{1} ∼_{R_{2}}^{∘} W′_{1} : σ

Journal of the ACM, Vol. V, No. N, Month 20YY.

for some Δ_{2} ⊇ Δ_{1} and R_{2} ⊇ R_{1}. Therefore, by the definition of ∼^{∘}, we have

W_{1} = [\overline{V}_{2}/\overline{x}_{2}][\overline{σ}_{2}/\overline{α}_{2}]M_{5}
W′_{1} = [\overline{V} ′_{2}/\overline{x}_{2}][\overline{σ}′_{2}/\overline{α}_{2}]M_{5}

for some

Δ_{2} ⊢ \overline{V}_{2} ∼_{R_{2}} \overline{V} ′_{2} : \overline{τ}_{2}

and

\overline{α}_{2}, \overline{x}_{2} : \overline{τ}_{2} ⊢ M_{5} : σ

with Δ_{2} = \{(\overline{α}_{2}, \overline{σ}_{2}, \overline{σ}′_{2})\}. Sub-case M_{4} = (fix f(x: σ) : τ = M′′_{3}). By inversion of (T-Fix), we have

\overline{α}_{1}, \overline{x}_{1} : \overline{τ}_{1}, f : σ → τ, x: σ ⊢ M′′_{3} : τ.

Thus, by weakening and the substitution lemma for values, we have

\overline{α}_{2}, \overline{x}_{1} : \overline{τ}_{1}, \overline{x}_{2} : \overline{τ}_{2} ⊢ [(fix f(x: σ) : τ = M′′_{3})/f][M_{5}/x]M′′_{3} : τ.

Then, by the definition of ∼^{∘}, we have

\begin{aligned}Δ_{2} & ⊢ & [\overline{V}_{1}, \overline{V}_{2}/\overline{x}_{1}, \overline{x}_{2}][\overline{σ}_{2}/\overline{α}_{2}][(fix f(x: σ) : τ = M′′_{3})/f][M_{5}/x]M′′_{3} \\ & ∼_{R_{2}}^{∘} & [\overline{V} ′_{1}, \overline{V} ′_{2}/\overline{x}_{1}, \overline{x}_{2}][\overline{σ}′_{2}/\overline{α}_{2}][(fix f(x: σ) : τ = M′′_{3})/f][M_{5}/x]M′′_{3} & : & τ, \end{aligned}

i.e.,

Δ_{2} ⊢ [W_{1}/x][(fix f(x: π) : ρ = M_{3})/f]M_{3} ∼_{R_{2}}^{∘} [W′_{1}/x][(fix f(x: π′) : ρ′ = M′_{3})/f]M′_{3} : τ.

Again by the induction hypothesis, we obtain

Δ_{3} ⊢ W ∼_{R_{3}}^{∘} W′ : τ

for some Δ_{3} ⊇ Δ_{2} and R_{3} ⊇ R_{2}. Sub-case M_{4} = x_{1_{i}}. Then

V_{1_{i}} = fix f(x: π) : ρ = M_{3}
V′_{1_{i}} = fix f(x: π′) : ρ′ = M′_{3}

and τ_{1_{i}} = σ → τ. Since we have

(fix f(x: π) : ρ = M_{3})([\overline{V}_{2}/\overline{x}_{2}][\overline{σ}_{2}/\overline{α}_{2}]M_{5}) ⇓ W

and

(fix f(x: π′) : ρ′ = M′_{3})([\overline{V} ′_{2}/\overline{x}_{2}][\overline{σ}′_{2}/\overline{α}_{2}]M_{5}) ⇓ W′

with

Δ_{2} ⊢ fix f(x: π) : ρ = M_{3} ∼_{R_{2}} fix f(x: π′) : ρ′ = M′_{3} : σ → τ,

we have

(Δ_{2}, R_{2} ∪ {(W, W′, τ)}) ∈ ∼

by Condition 2 of bisimulation. Thus, we have

Δ_{2} ⊢ W ∼_{R_{3}}^{∘} W′ : τ

Journal of the ACM, Vol. V, No. N, Month 20YY.

for R_{3} = R_{2} ∪ {(W, W′, τ)} by the definition of ∼^{∘}.

Proofs of the other cases are similar. □

C. PROOF OF LEMMA 4.4

The lemma to prove was: If Δ_{0} ⊢ N ∼_{R_{0}}^{∘} N′ : τ then N ⇓ ⟺ N′ ⇓.

We assume N ⇓ W and prove N′ ⇓ by induction on the derivation of N ⇓ W. (The other direction follows by symmetry.) The argument is similar to the proof of Lemma 4.3, except that we are proving the existence of an evaluation derivation for N′ by using the given evaluation derivation for N, instead of proving a property of given evaluation derivations for N and N′. We show just the most interesting case: the one for (E-Open).

By the definition of ∼^{∘}, we have

N = [\overline{V}_{0}/\overline{x}_{0}][\overline{σ}_{0}/\overline{α}_{0}]M_{0}

and

N′ = [\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′_{0}/\overline{α}_{0}]M_{0}

for some

Δ_{0} ⊢ \overline{V}_{0} ∼_{R_{0}} \overline{V} ′_{0} : \overline{τ}_{0}

and

\overline{α}_{0}, \overline{x}_{0} : \overline{τ}_{0} ⊢ M_{0} : τ

with Δ_{0} = \{(\overline{α}_{0}, \overline{σ}_{0}, \overline{σ}′_{0})\}. In the case of (E-Open), M_{0} has the form

M_{0} = open M_{1} as α, y in M_{2}

and the given evaluation derivation for N has the following form:

\frac{\begin{matrix}[\overline{V}_{0}/\overline{x}_{0}][\overline{σ}_{0}/\overline{α}_{0}]M_{1} ⇓ pack ρ_{1}, W_{1} as ∃α. ρ_{2} \\ [W_{1}/y][ρ_{1}/α][\overline{V}_{0}/\overline{x}_{0}][\overline{σ}_{0}/\overline{α}_{0}]M_{2} ⇓ \end{matrix}}{[\overline{V}_{0}/\overline{x}_{0}][\overline{σ}_{0}/\overline{α}_{0}](open M_{1} as α, y in M_{2}) ⇓}

We aim to derive an evaluation of N′ of a similar form:

\frac{\begin{matrix}[\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′_{0}/\overline{α}_{0}]M_{1} ⇓ pack ρ′_{1}, W′_{1} as ∃α. ρ′_{2} \\ [W′_{1}/y][ρ′_{1}/α][\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′_{0}/\overline{α}_{0}]M_{2} ⇓ \end{matrix}}{[\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′_{0}/\overline{α}_{0}](open M_{1} as α, y in M_{2}) ⇓}

By inversion of (T-Open), we have

\overline{α}_{0}, \overline{x}_{0} : \overline{τ}_{0} ⊢ M_{1} : ∃α. ρ′′_{2}

and

\overline{α}_{0}, \overline{x}_{0} : \overline{τ}_{0}, α, y: ρ′′_{2} ⊢ M_{2} : τ

with α ∉ FTV (τ). Thus, by the definition of ∼^{∘}, we have

Δ_{0} ⊢ [\overline{V}_{0}/\overline{x}_{0}][\overline{σ}_{0}/\overline{α}]M_{1} ∼_{R_{0}}^{∘} [\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′_{0}/\overline{α}]M_{1} : ∃α. ρ′′_{2}.

Journal of the ACM, Vol. V, No. N, Month 20YY.

A Bisimulation for Type Abstraction and Recursion · 39

Therefore, by the induction hypothesis and Lemma 4.3, we have

[\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′_{0}/\overline{α}_{0}]M_{1} ⇓ W′_{2}

for some

Δ_{1} ⊢ pack ρ_{1}, W_{1} as ∃α. ρ_{2} ∼_{R_{1}}^{∘} W′_{2} : ∃α. ρ′′_{2}

with Δ_{1} ⊇ Δ_{0} and R_{1} ⊇ R_{0}. Then, by the definition of ∼^{∘}, we have

pack ρ_{1}, W_{1} as ∃α. ρ_{2} = [\overline{V}_{1}/\overline{x}_{1}][\overline{σ}_{1}/\overline{α}_{1}]M_{3}

and

W′_{2} = [\overline{V} ′_{1}/\overline{x}_{1}][\overline{σ}′_{1}/\overline{α}_{1}]M_{3}

for some

Δ_{1} ⊢ \overline{V}_{1} ∼_{R_{1}} \overline{V} ′_{1} : \overline{τ}_{1}

and

\overline{α}_{1}, \overline{x}_{1} : \overline{τ}_{1} ⊢ M_{3} : ∃α. ρ′′_{2}

with Δ_{1} = \{(\overline{α}_{1}, \overline{σ}_{1}, \overline{σ}′_{1})\}. Sub-case M_{3} = (pack ρ′′_{1}, M_{4} as ∃α. ρ′′_{2}). Then W′_{2} has the form

W′_{2} = pack ρ′_{1}, W′_{1} as ∃α. ρ′_{2}

where

W_{1} = [\overline{V}_{1}/\overline{x}_{1}][\overline{σ}_{1}/\overline{α}_{1}]M_{4}
W′_{1} = [\overline{V} ′_{1}/\overline{x}_{1}][\overline{σ}′_{1}/α_{1}]M_{4}

and

ρ_{1} = [\overline{σ}_{1}/\overline{α}_{1}]ρ′′_{1}
ρ′_{1} = [\overline{σ}′_{1}/\overline{α}_{1}]ρ′′_{1}.

Since we have

\overline{α}_{1}, \overline{x}_{1} : \overline{τ}_{1} ⊢ M_{4} : [ρ′′_{1}/α]ρ′′_{2}

by inversion of (T-Pack), we have

\overline{α}_{1}, \overline{x}_{0} : \overline{τ}_{0}, \overline{x}_{1} : \overline{τ}_{1} ⊢ [M_{4}/y][ρ′′_{1}/α]M_{2} : τ

by weakening and the substitution lemmas for types and terms. Therefore, by the definition of ∼^{∘}, we have

Δ_{1} ⊢ [\overline{V}_{0}, \overline{V}_{1}/\overline{x}_{0}, \overline{x}_{1}][\overline{σ}_{1}/\overline{α}_{1}][M_{4}/y][ρ′′_{1}/α]M_{2} ∼_{R_{1}}^{∘} [\overline{V} ′_{0}, \overline{V}_{1}/\overline{x}_{0}, \overline{x}_{1}][\overline{σ}′_{1}/\overline{α}_{1}][M_{4}/y][ρ′′_{1}/α]M_{2} : τ.

Since

[\overline{V}_{0}, \overline{V}_{1}/\overline{x}_{0}, \overline{x}_{1}][\overline{σ}_{1}/\overline{α}_{1}][M_{4}/y][ρ′′_{1}/α]M_{2}
= [([\overline{V}_{1}/\overline{x}_{1}][\overline{σ}_{1}/\overline{α}_{1}]M_{4})/y][([\overline{σ}_{1}/\overline{α}_{1}]ρ′′_{1})/α][\overline{V}_{0}/\overline{x}_{0}][\overline{σ}_{0}/\overline{α}_{0}]M_{2}
= [W_{1}/y][ρ_{1}/α][\overline{V}_{0}/\overline{x}_{0}][\overline{σ}_{0}/\overline{α}_{0}]M_{2}

Journal of the ACM, Vol. V, No. N, Month 20YY.

40 · E. Sumii and B. C. Pierce

and

[\overline{V} ′_{0}, \overline{V} ′_{1}/\overline{x}_{0}, \overline{x}_{1}][\overline{σ}′_{1}/\overline{α}_{1}][M_{4}/y][ρ′′_{1}/α]M_{2}
= [([\overline{V} ′_{1}/\overline{x}_{1}][\overline{σ}′_{1}/\overline{α}_{1}]M_{4})/y][([\overline{σ}′_{1}/\overline{α}_{1}]ρ′′_{1})/α][\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′_{0}/\overline{α}_{0}]M_{2}
= [W′_{1}/y][ρ′_{1}/α][\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′_{0}/\overline{α}_{0}]M_{2},

we have

[W′_{1}/y][ρ′_{1}/α][\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′_{0}/\overline{α}_{0}]M_{2} ⇓

by the induction hypothesis, i.e., N′ ⇓. Sub-case M_{3} = x_{1_{i}}. Then W′_{2} = V′_{1_{i}} where

V_{1_{i}} = pack ρ_{1}, W_{1} as ∃α. ρ_{2}

and τ_{1_{i}} = ∃α. ρ′′_{2}. By Condition 1 of bisimulation, V′_{1_{i}} is a value of the existential type [\overline{σ}′_{1}/\overline{α}_{1}]τ_{1_{i}} = ∃α. ([\overline{σ}′_{1}/\overline{α}_{1}]ρ′′_{2}), so it has the form

V′_{1_{i}} = pack ρ′_{1}, W′_{1} as ∃α. ρ′_{2}.

Since

Δ_{1} ⊢ V_{1_{i}} ∼_{R_{1}} V′_{1_{i}} : τ_{1_{i}},

we have the following two possibilities by Condition 4 of bisimulation. Sub-sub-case (β, ρ_{1}, ρ′_{1}) ∈ Δ_{1} and (W_{1}, W′_{1}, [β/α]ρ′′_{2}) ∈ R_{1}. Since we have

\overline{α}_{0}, \overline{x}_{0} : \overline{τ}_{0}, α, y: ρ′′_{2} ⊢ M_{2} : τ

with α ∉ FTV (τ), we have

\overline{α}_{0}, \overline{x}_{0} : \overline{τ}_{0}, β, y: [β/α]ρ′′_{2} ⊢ [β/α]M_{2} : τ.

Then, we have

Δ_{1} ⊢ [\overline{V}_{0}, W_{1}/\overline{x}_{0}, y][\overline{σ}_{1}/\overline{α}_{1}][β/α]M_{2} ∼_{R_{1}}^{∘} [\overline{V} ′_{0}, W′_{1}/\overline{x}_{0}, y][\overline{σ}′_{1}/\overline{α}_{1}][β/α]M_{2} : τ

by the definition of ∼^{∘}. Since we have β = α_{1_{i}} with ρ_{1} = σ_{1_{i}} and ρ′_{1} = σ′_{1_{i}} for some i, we have

[\overline{V}_{0}, W_{1}/\overline{x}_{0}, y][\overline{σ}_{1}/\overline{α}_{1}][β/α]M_{2} = [W_{1}/y][ρ_{1}/α][\overline{V}_{0}/\overline{x}_{0}][\overline{σ}_{0}/\overline{α}_{0}]M_{2}

and

[\overline{V} ′_{0}, W′_{1}/\overline{x}_{0}, y][\overline{σ}′_{1}/\overline{α}_{1}][β/α]M_{2} = [W′_{1}/y][ρ′_{1}/α][\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′_{0}/\overline{α}_{0}]M_{2},

so we have

[W′_{1}/y][ρ′_{1}/α][\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′_{0}/\overline{α}_{0}]M_{2} ⇓

by the induction hypothesis, i.e., N′ ⇓. Sub-sub-case (Δ_{1} ⊎ {(α, ρ_{1}, ρ′_{1})}, R_{1} ∪ {(W_{1}, W′_{1}, ρ′′_{2})}) ∈ ∼. Then we have

Δ_{2} ⊢ [\overline{V}_{0}, W_{1}/\overline{x}_{0}, y][\overline{σ}_{0}, ρ_{1}/\overline{α}_{0}, α]M_{2} ∼_{R_{2}}^{∘} [\overline{V} ′_{0}, W′_{1}/\overline{x}_{0}, y][\overline{σ}′_{0}, ρ′_{1}/\overline{α}_{0}, α]M_{2} : τ

Journal of the ACM, Vol. V, No. N, Month 20YY.

for Δ_{2} = Δ_{1} ∪ {(α, ρ_{1}, ρ′_{1})} and R_{2} = R_{1} ∪ {(W_{1}, W′_{1}, ρ′′_{2})} by the definition of ∼^{∘}. Since we have

[\overline{V}_{0}, W_{1}/\overline{x}_{0}, y][\overline{σ}_{0}, ρ_{1}/\overline{α}_{0}, α]M_{2} = [W_{1}/y][ρ_{1}/α][\overline{V}_{0}/\overline{x}_{0}][\overline{σ}_{0}/\overline{α}_{0}]M_{2}

and

[\overline{V} ′_{0}, W′_{1}/\overline{x}_{0}, y][\overline{σ}′_{0}, ρ′_{1}/\overline{α}_{0}, α]M_{2} = [W′_{1}/y][ρ′_{1}/α][\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′_{0}/\overline{α}_{0}]M_{2},

we have

[W′_{1}/y][ρ′_{1}/α][\overline{V} ′_{0}/\overline{x}_{0}][\overline{σ}′_{0}/\overline{α}_{0}]M_{2} ⇓

by the induction hypothesis, i.e., N′ ⇓. □

ACKNOWLEDGMENTS

We would like to thank Karl Crary, Andy Gordon, Bob Harper, Vassileios Koutavas, and Andrew Pitts for information and discussions on their work and its relationship to ours. Comments from anonymous reviewers, the members of the PL Club at the University of Pennsylvania, and Naoki Kobayashi helped us to sharpen the presentation. Reviewer 2 of JACM suggested the examples in Section 7.

REFERENCES

Abadi, M. and Fournet, C. 2001. Mobile values, new names, and secure communication. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 104–115.

Abadi, M. and Gordon, A. D. 1998. A bisimulation method for cryptographic protocols. Nordic Journal of Computing 5, 267–303. Preliminary version appeared in 7th European Symposium on Programming, Lecture Notes in Computer Science, Springer-Verlag, vol. 1381, pp. 12–26, 1998.

Abadi, M. and Gordon, A. D. 1999. A calculus for cryptographic protocols: The spi calculus. Information and Computation 148, 1, 1–70. Preliminary version appeared in Proceedings of the 4th ACM Conference on Computer and Communications Security, pp. 36–47, 1997.

Abramsky, S. 1990. The lazy lambda calculus. In Research Topics in Functional Programming,

D. A. Turner, Ed. Addison-Wesley, 65–117. Ahmed, A. 2006. Step-indexed syntactic logical relations for recursive and quantified types. In

15th European Symposium on Programming. 69–83. Ahmed, A., Appel, A. W., and Virga, R. 2003. An indexed model of impredicative polymor-

phism and mutable references. http://www.cs.princeton.edu/~amal/papers/impred.pdf.

Appel, A. W. and McAllester, D. 2001. An indexed model of recursive types for foundational proof-carrying code. ACM Transactions on Programming Languages and Systems 23, 5, 657– 683.

Berger, M., Honda, K., and Yoshida, N. 2003. Genericity and the pi-calculus. In Foundations of Software Science and Computation Structures. Lecture Notes in Computer Science, vol. 2620. Springer-Verlag, 103–119.

Bierman, G. M., Pitts, A. M., and Russo, C. V. 2000. Operational properties of Lily, a polymorphic linear lambda calculus with recursion. In Higher Order Operational Techniques in Semantics. Electronic Notes in Theoretical Computer Science, vol. 41. Elsevier Science.

Birkedal, L. and Harper, R. 1999. Relational interpretations of recursive types in an operational setting. Information and Computation 155, 1–2, 3–63. Summary appeared in Theoretical Aspects of Computer Software, Lecture Notes in Computer Science, Springer-Verlag, vol. 1281, pp. 458–490, 1997.

Boreale, M., De Nicola, R., and Pugliese, R. 2002. Proof techniques for cryptographic processes. SIAM Journal on Computing 31, 3, 947–986. Preliminary version appeared in 14th Annual IEEE Symposium on Logic in Computer Science, pp. 157–166, 1999.

Borgström, J. and Nestmann, U. 2002. On bisimulations for the spi calculus. In 9th International Conference on Algebraic Methodology and Software Technology. Lecture Notes in Computer Science, vol. 2422. Springer-Verlag, 287–303.

Bruce, K. B., Cardelli, L., and Pierce, B. C. 1999. Comparing object encodings. Information and Computation 155, 1–2, 108–133. Extended abstract appeared in Theoretical Aspects of Computer Software, Springer-Verlag, vol. 1281, pp. 415–338, 1997.

Crary, K. and Harper, R. 2007. Syntactic logical relations for polymorphic and recursive types. In Computation, Meaning, and Logic: Articles dedicated to Gordon Plotkin. Electronic Notes in Theoretical Computer Science, vol. 172. Elsevier Science, 259–299.

Gordon, A. D. 1995a. Bisimilarity as a theory of functional programming. mini-course. http:

//research.microsoft.com/~adg/Publications/BRICS-NS-95-3.dvi.gz.

Gordon, A. D. 1995b. Operational equivalences for untyped and polymorphic object calculi. In

Higher Order Operational Techniques in Semantics. Cambridge University Press, 9–54. Gordon, A. D. and Rees, G. D. 1995. Bisimilarity for F_{<:}. Draft. Gordon, A. D. and Rees, G. D. 1996. Bisimilarity for a first-order calculus of objects with

subtyping. In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 386–395.

Heintze, N. and Riecke, J. G. 1998. The SLam calculus: Programming with secrecy and integrity. In Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.

Howe, D. J. 1996. Proving congruence of bisimulation in functional programming languages.

Information and Computation 124, 2, 103–112. Hughes, D. J. 1997. Games and definability for System F. In Twelfth Annual IEEE Symposium

on Logic in Computer Science. 76–86. Koutavas, V. and Wand, M. 2006a. Bisimulations for untyped imperative objects. In 15th

European Symposium on Programming. 146–161. Koutavas, V. and Wand, M. 2006b. Small bisimulations for reasoning about higher-order imper-

ative programs. In Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 141–152.

Koutavas, V. and Wand, M. 2007. Reasoning about class behavior. In 2007 International Workshop on Foundations and Developments of Object-Oriented Languages. http://foolwood07.

cs.uchicago.edu/program/koutavas.pdf.

Melliés, P.-A. and Vouillon, J. 2005. Recursive polymorphic types and parametricity in an

operational framework. In 20th Annual IEEE Symposium on Logic in Computer Science. 82–91. Meyer, A. R. and Sieber, K. 1988. Towards fully abstract semantics for local variables: Prelim-

inary report. In Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 191–203.

Milner, R. 1980. A Calculus of Communicating Systems. Number 92 in Lecture Notes in

Computer Science. Springer-Verlag. Milner, R. 1989. Communication and Concurrency. Prentice Hall. Milner, R. 1999. Communicating and Mobile Systems: The π-Calculus. Cambridge University

Press. Mitchell, J. C. 1996. Foundations for Programming Languages. MIT Press. Moggi, E. 1991. Notions of computation and monads. Information and Computation 93, 1,

55–92. Morris, Jr., J. H. 1973a. Protection in programming languages. Communications of the

ACM 16, 1, 15–21. Morris, Jr., J. H. 1973b. Types are not sets. In Proceedings of the 1st Annual ACM SIGACT-

SIGPLAN Symposium on Principles of Programming Languages. 120–124.

Journal of the ACM, Vol. V, No. N, Month 20YY.

Pierce, B. C. and Sangiorgi, D. 2000. Behavioral equivalence in the polymorphic pi-calculus. Journal of the ACM 47, 3, 531–586. Extended abstract appeared in Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1997, pp. 531–584.

Pitts, A. 2005. Typed operational reasoning. In Advanced Topics in Types and Programming Languages, B. C. Pierce, Ed. MIT Press, Chapter 7, 245–289. Preliminary version appeared as Existential Types: Logical Relations and Operational Equivalence in Automata, Languages and Programming, Lecture Notes in Computer Science, Springer-Verlag, vol. 1443, pp. 309–326, 1998.

Pitts, A. M. 2000. Parametric polymorphism and operational equivalence. Mathematical Structures in Computer Science 10, 321–359. Preliminary version appeared in HOOTS II Second Workshop on Higher-Order Operational Techniques in Semantics, Electronic Notes in Theoretical Computer Science, vol. 10, 1998.

Pitts, A. M. and Stark, I. 1993. Observable properties of higher order functions that dynamically create local names, or: what’s new? In Mathematical Foundations of Computer Science. Lecture Notes in Computer Science, vol. 711. Springer-Verlag, 122–141.

Pitts, A. M. and Stark, I. 1998. Operational reasoning for functions with local state. In Higher

Order Operational Techniques in Semantics. Cambridge University Press, 227–273. Sangiorgi, D. 1992. Expressing mobility in process algebras: First-order and higher-order

paradigm. Ph.D. thesis, University of Edinburgh. Sangiorgi, D., Kobayashi, N., and Sumii, E. 2007. Environmental bisimulations for higher-

order languages. In Twenty-Second Annual IEEE Symposium on Logic in Computer Science. 293–302.

Sumii, E. and Pierce, B. C. 2004. A bisimulation for dynamic sealing. In Proceedings of the 31st

ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 161–172. Wadler, P. 1989. Theorems for free! In Proceedings of the Fourth ACM SIGPLAN International

Conference on Functional Programming Languages and Computer Architecture. ACM, 347– 359.

Received Month Year; revised Month Year; accepted Month Year