BRICS NS-95-3 A. D. Gordon: Bisimilarity as a Theory of Functional Programming

BRICS

Basic Research in Computer Science

Bisimilarity as a Theory of Functional Programming

Mini-Course

Andrew D. Gordon

BRICS Notes Series NS-95-3 ISSN 0909-3206 July 1995 See back inner page for a list of recent publications in the BRICS Notes Series. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@daimi.aau.dk

BRICS publications are in general accessible through WWW and anonymous FTP:

http://www.brics.aau.dk/BRICS/
ftp ftp.brics.aau.dk (cd pub/BRICS)

Bisimilarity as a Theory of Functional Programming. Mini-Course.^{∗}

Andrew D. Gordon University of Cambridge Computer Laboratory

June 1995

Abstract

Operational intuition is central to computer science. These notes introduce functional programmers to operational semantics and operational equivalence. We show how the idea of bisimilarity from CCS may be applied to deterministic functional languages. On elementary operational grounds it justifies equational reasoning and proofs about infinite streams.

∗Notes to accompany graduate lectures at BRICS in the Computer Science Department of Aarhus University, March 1995. \begin{matrix}c \\ ◯ \end{matrix} A. D. Gordon, 1995. Earlier versions of part of this material appeared in the proceedings of the Glasgow FP’94 (Gordon 1995b) and MFPS’95 (Gordon 1995a) conferences. This version of November 24, 1995 fixes minor errors in the version printed as number NS–95–3 in the BRICS Notes Series. If you find any mistakes or have any comments please email adg@cl.cam.ac.uk.

ii

Contents

1 Objectives 1

2 Bisimilarity for PCF plus Streams 4 2.1 Definition of PCF plus Streams . . . . . . . . . . . . . . . . . 4 2.2 Induction and Co-induction . . . . . . . . . . . . . . . . . . . 9 2.3 Divergence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.4 Bisimilarity . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.5 The Map/Iterate Example . . . . . . . . . . . . . . . . . . . . 16 2.6 Theory of Bisimilarity . . . . . . . . . . . . . . . . . . . . . . 17

3 Congruence of Bisimilarity 22 3.1 Congruence and Precongruence . . . . . . . . . . . . . . . . . 22 3.2 Similarity is a Precongruence . . . . . . . . . . . . . . . . . . 25 3.3 Bisimilarity equals Contextual Equivalence . . . . . . . . . . . 28 3.4 Experimental Equivalence . . . . . . . . . . . . . . . . . . . . 31

4 Refining Bisimulation 34 4.1 Bisimulations up to ∼ . . . . . . . . . . . . . . . . . . . . . . 34 4.2 Matching Values . . . . . . . . . . . . . . . . . . . . . . . . . 34 4.3 The Map/Filter Example . . . . . . . . . . . . . . . . . . . . . 36 4.4 Matching Reductions . . . . . . . . . . . . . . . . . . . . . . . 38 4.5 Proof of Monad Laws . . . . . . . . . . . . . . . . . . . . . . . 41 4.6 Bird and Wadler’s Take Lemma . . . . . . . . . . . . . . . . . 45

5 Variations 47 5.1 The Active/Passive Distinction . . . . . . . . . . . . . . . . . 47 5.2 Convergence Testing and Call-by-Value . . . . . . . . . . . . . 48 5.3 FPC: Sums, Pairs, Recursive Types . . . . . . . . . . . . . . . 49 5.4 Matching Value Contexts . . . . . . . . . . . . . . . . . . . . . 52

6 Summary and Related Work 54

References 56 iv

List of Tables

1 Δ_{→}: functions . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2 Δ_{A}: arithmetic . . . . . . . . . . . . . . . . . . . . . . . . . . 7 3 Δ_{[−]}: streams . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 4 Δ_{μ→}: recursive functions . . . . . . . . . . . . . . . . . . . . . 8 5 Observations on PCF plus streams . . . . . . . . . . . . . . . 14 6 Properties Specific to PCF plus Streams . . . . . . . . . . . . 20 7 The compatible refinement of a relation . . . . . . . . . . . . . 23 8 Δ_{+}: sums . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 9 Δ_{×}: pairs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 10 Δ_{μ}: recursive types . . . . . . . . . . . . . . . . . . . . . . . . 51 vi

1 Objectives

The object of these notes is to offer a new perspective on the behaviour of functional programs based on CCS-style labelled transitions and bisimilarity. Apart from this new material, these notes are intended to introduce functional programmers to the basic ideas of operational semantics and coinductive definitions. We have in mind a reader familiar with programming in lazy functional languages, such as Miranda or Haskell, but use a simpler language, PCF plus streams, as the vehicle for developing our theory. PCF is simply-typed lambda-calculus plus arithmetic (Plotkin 1977). Streams are one of the key ingredients of lazy functional programming (Hughes 1989). They unify many ideas: both infinite and finite lists, co-routines, multiple outcomes, standard input and output, files and so on. PCF plus streams is probably the minimal functional language that admits interesting coinductive proofs of program equivalence. Operational intuition is central to computer science. These notes show how operational semantics, together with the elementary mathematics of inductive and co-inductive definitions, is enough to build from first principles an expressive theory of functional programming.

Morris-style contextual equivalence is widely accepted as the natural notion of operational equivalence for PCF-like languages. Two programs are contextually equivalent if they may be interchanged for one another in any larger program of ground type, without affecting whether evaluation of the whole program converges or not. The quantification over program contexts makes contextual equivalence hard to prove directly. One approach to this difficulty is to characterise contextual equivalence independently of the syntax and operational semantics of PCF, typically using some form of domain theory. This is the ‘full abstraction’ problem for PCF; see Ong (1994) for a discussion and review of the literature.

Instead, our approach is to characterise contextual equivalence as a form of bisimilarity, and to exploit operationally-based co-inductive proofs. Our point of departure is Milner’s (1989) entirely operational theory of CCS, based on labelled transitions and bisimilarity. A labelled transition takes the form a ⟶^{α} b, where a and b are programs, and α is an action; the intended meaning of such a transition is that the atomic observation α can be made of program a to yield a successor b. In CCS, the actions represent possible communications. Given a definition of the possible labelled transitions for a language, any program gives rise to a (possibly infinite) derivation tree, whose nodes are programs and whose arcs are transitions, labelled by actions. Bisimilarity is based on the intuition that a derivation tree represents the behaviour of a program. We say two programs are bisimilar if their derivation trees are the same when one ignores the syntactic structure at the nodes. Hence bisimilarity is a way to compare behaviour, represented by actions, whilst discarding syntactic structure. Park (1981) showed how bisimilarity could be defined co-inductively; the theory of CCS is heavily dependent on proofs by co-induction.

Bisimilarity has been applied to deterministic functional programming before, notably by Abramsky in his study of applicative bisimulation and lazy lambda-calculus (Abramsky and Ong 1993) and by Howe (1989), who invented a powerful method of showing that bisimilarity is a congruence. Both showed that their untyped forms of bisimilarity equalled contextual equivalence. If Ω is a divergent lambda-term, both these untyped formulations of bisimilarity distinguish λ(x)Ω from Ω, because one converges and the other diverges. But in a typed call-by-name setting, contextual equivalence would identify these two functions, because they have the same behaviour on all arguments. Hence Turner (1990, Preface) expressed concern that applicative bisimulation would fall short of contextual equivalence for languages such as Miranda or Haskell.

We answer Turner’s concern by showing that by defining a labelled transition system for PCF plus streams and then defining bisimilarity exactly as in CCS, we can prove it equals contextual equivalence. In particular, in the call-by-name variant we have Ω^{A→B} bisimilar to λ(x:A)Ω^{B}. This is the first new result presented in these notes. The second is the investigation in Section 4 of refinements of bisimulation that exploit determinacy.

Here is the structure of these notes.

• Section 2 begins by introducing PCF plus streams, and defining contextual equivalence. The problem then is to characterise contextual equivalence co-inductively. After explaining how principles of induction and co-induction follow from Tarski’s theorem, we do so by giving a labelled transition system, and replaying the definition of bisimilarity from CCS. We conclude the section by illustrating bisimulation proofs about stream-processing programs and deriving basic properties of bisimilarity.

• Section 3 falls into two halves. In the first we prove bisimilarity equals contextual equivalence. Howe proved congruence of bisimilarity for a general class of lazy computation systems. We rework his method for our form of bisimilarity, based on a labelled transition system. In the second half we adapt Milner’s context lemma (1977) to construct another co-inductive characterisation of contextual equivalence, which we call ‘experimental equivalence.’ The congruence proof for experimental equivalence is unrelated to Howe’s. We find that the associated co-induction principle is weaker than bisimulation.

• In Section 4 we exploit the determinacy of reduction in PCF plus streams to obtain refinements of bisimulation, analogous to the idea of ‘bisimulation up to ∼’ in CCS. In particular we obtain a new coinductive characterisation of contextual equivalence based on reduction behaviour and production of values.

• We sketch in Section 5 how the results of the previous sections extend to richer languages than PCF plus streams. In particular, our theory holds for a language of sums, products and recursive types (Gunter 1992; Winskel 1993), and for call-by-value variations.

• Section 6 concludes by reviewing related work and discussing the significance of these results.

2 Bisimilarity for PCF plus Streams

This section explains the central ideas of this operational theory. The language we work with, PCF plus streams, is given in a series of fragments in separate tables. In fact all the results of these notes hold for a richer language, FPC, which includes sums, products and recursive types. We will prove properties only for PCF plus streams. FPC is defined in Section 5, and call-by-value variants are described, but we leave extension of all the proofs as exercises.

2.1 Definition of PCF plus Streams

Definition 2.1 Here is the syntax of types, A, and expressions, e,

A ::= Bool | Num | A → A | [A]
e ::= x | λ(x:A)e | e(e) | rec(f:A → B, x:A)e | \underline{n}(n ∈ ℕ) | \underline{bv}(bv ∈ \{tt, ff \})

    | if e then e else e | succ(e) | pred(e) | zero(e)

| nil | e:: e | scase(e, e, e)

Here are our metavariable conventions.

variables closed possibly-open
Types  X, Y  A, B
Expressions x, y  a, b  e
Values  –  v  –

We usually write true and false for \underline{tt} and \underline{ff} respectively, and allow metavariable ℓ to range over all literals, ℕ ∪ {tt, ff }. We identify phrases up to alphaconversion, that is, consistent renaming of bound variables. We use ≡ for syntactic identity. We write ϕ[ψ/x] for the substitution of phrases ψ for each occurrence of variable x in phrase ϕ. We write fv(e) for the set of variables free in expression e.

Our syntax of PCF plus streams uses separate syntactic constructors, such as, succ(−), pred(−), rec(f, x)(−), …, for arithmetic, recursion and so on. Instead, PCF can be presented as a simply typed lambda-calculus with function constants for arithmetic and recursion (Scott 1993; Plotkin 1977). By using separate forms of syntax we simplify the presentation here of the operational semantics. But this is an issue of form rather than content. Elsewhere we present a call-by-value form of PCF using function constants (Crole and Gordon 1995).

We present the rules that define the semantics of call-by-name PCF plus streams as a collection of fragments: Δ_{→} (functions, Table 1), Δ_{A} (arithmetic, Table 2), Δ_{[−]} (streams, Table 3) and Δ_{μ→} (recursive functions, Table 4). PCF itself is given by

PCF = Δ_{→} ∪ Δ_{A} ∪ Δ_{μ→}

and PCF plus streams is PCF ∪ Δ_{[−]}. For any of these languages, the static semantics is given as follows.

Definition 2.2 (Static Semantics) The type assignment relation Γ ⊢ e: A is given inductively by the (Exp −) rules of the language, where Γ is an environment, a finite map from variables to types, of form x_{1}:A_{1}, …, x_{n}:A_{n}. We assume implicitly that environments appearing in the rules of static semantics are well-formed. In general we define

a, b ∈ Prog(A) =^{def} {e | ∅ ⊢ e: A}
Prog =^{def} ⋃{Prog(A) | A is a type}
Rel(A) =^{def} {(a, b) | a ∈ Prog(A) & b ∈ Prog(A)}
R, S ⊆ Rel =^{def} ⋃{Rel(A) | A is a type}

and we write a_{1}, …, a_{n}:A to mean that {a_{1}, …, a_{n}} ⊆ Prog(A).

Proposition 2.3

(1) If Γ ⊢ e: A and Γ ⊢ e: B then A ≡ B.

(2) If Γ, x:A_{2} ⊢ e_{1} : A_{1} and Γ ⊢ e_{2} : A_{2} then Γ ⊢ e_{1}[e^{2}/x] : A_{1}.

Proof

(1) By rule induction on the derivation of Γ ⊢ e: A.

(2) By rule induction on the derivation of Γ, x:A_{2} ⊢ e_{1} : A_{1}.

■

To define the dynamic semantics, we need the notion of a context, an expression-with-a-hole. It is enough for our purposes for the hole to be represented by a distinguished variable.

Definition 2.4 (Contexts) Suppose there is some arbitrary variable, −, used to stand for a hole in an expression. Let a context be an expression e such that fv(e) ⊆ {−}. If e is a context, we write e[e′] short for e[e′/−].

Statics

Γ, x:A, Γ′ ⊢ x: A (Exp x)

Γ, x:B ⊢ e: A x ∉ Dom(Γ)

\overline{(Exp Fun)}
Γ ⊢ λ(x:B)e: B → A
Γ ⊢ e_{1} : B → A Γ ⊢ e_{2} : B
\overline{(Exp Appl)}
Γ ⊢ e_{1}(e_{2}) : A

Lazy Dynamics

v ::= λ(x:A)e  (Value Fun)
(λ(x:A)e)(a) ↦ e[a/x] (Red Beta)
E ::= −(a)  (Exper Rator)

Table 1: Δ_{→}: functions

The dynamic semantics is based on a small-step reduction relation, ↦. Its reduction strategy is determined by a set of experiments, with metavariable E, the set of contexts under which reduction is closed.

Definition 2.5 (Dynamic Semantics) The experiments and values are the contexts and programs, respectively, given by the (Exper −) and (Value −) rules of the language. The small-step reduction relation a ↦ b is given inductively by the (Red −) rules of the language together with the generic rule

a ↦ b

(Red Experiment)

E[a] ↦ E[b]

We define the usual notions of evaluation, convergence and divergence as follows.

a ↦ =^{def} ∃b(a ↦ b)  ‘a reduces’
a ⇓ b =^{def} a ↦^{∗} b & ¬(b ↦)  ‘a evaluates to b’
a⇓ =^{def} ∃b(a ⇓ b)  ‘a converges’
a⇑ =^{def} whenever a ↦^{∗} b, b ↦ ‘a diverges’

Γ ⊢ \underline{n}: Num (Exp Num) Γ ⊢ \underline{bv} : Bool (Exp Bool)

Γ ⊢ e: Num

\overline{(Exp Succ)}

Γ ⊢ succ(e) : Num

Γ ⊢ e: Num

\overline{(Exp Pred)}

     Γ ⊢ pred(e) : Num

Γ ⊢ e_{1} : Bool  Γ ⊢ e_{2} : A  Γ ⊢ e_{3} : A
\overline{(Exp If)}

Γ ⊢ if e_{1} then e_{2} else e_{3} : A

Γ ⊢ e: Num

\overline{(Exp Zero)}

Γ ⊢ zero(e) : Bool

Dynamics

v ::= \underline{bv} | \underline{n} (Value Arith)

if\underline{bv} then a_{tt} else a_{ff} ↦ a_{bv} (Red If) succ(\underline{n}) ↦ \underline{n + 1} (Red Succ) pred(\underline{0}) ↦ \underline{0} (Red Pred 0) pred(\underline{n + 1}) ↦ \underline{n} (Red Pred Succ) zero(\underline{0}) ↦ \underline{tt} (Red Zero 0) zero(\underline{n + 1}) ↦ \underline{ff} (Red Zero Succ) E ::= if − then a else a | succ(−) | pred(−) | zero(−) (Exper Arith)

Table 2: Δ_{A}: arithmetic

Statics Γ ⊢ nil : [A] (Exp Nil)

Γ ⊢ e_{1} : A Γ ⊢ e_{2} : [A]

\overline{(Exp Cons)}

Γ ⊢ e_{1} :: e_{2} : [A]

Γ ⊢ e_{1} : [A] Γ ⊢ e_{2} : B Γ ⊢ e_{3} : A → [A] → B

\overline{(Exp Scase)}

Γ ⊢ scase(e_{1}, e_{2}, e_{3}) : B

Lazy Dynamics

v ::= nil | (a:: a)  (Value Stm)
scase(nil, b, c) ↦ b  (Red Scase Nil)
scase(a_{1} :: a_{2}, b, c) ↦ c(a_{1})(a_{2}) (Red Scase Cons)
E ::= scase(−, a, a)  (Exper Stm)

Table 3: Δ_{[−]}: streams

Statics

Γ, f:A → B, x:A ⊢ e: B

\overline{(Exp Rec)}

Γ ⊢ rec(f:A → B, x:A)e: A → B

Lazy Dynamics

v ::= rec(f, x)e  (Value Rec)
(rec(f, x)e)(a) ↦ e[rec(f, x)e, a/f, x] (Red Rec)

Table 4: Δ_{μ→}: recursive functions An evaluation context is a context of the form E⃗[−], that is, E_{1}[… E_{n}[−] …], where E⃗ is a list of experiments E_{1}, …, E_{n} with n ≥ 0. Felleisen and Friedman (1986) pioneered the use of evaluation contexts (though they originally used the term ‘reduction contexts’). Taking experiments—atomic evaluation contexts—as primitive helps our discussion of experimental equivalence in Sections 3.4 and 5.1.

For all the languages considered in these notes, reduction is deterministic and preserves types.

Proposition 2.6

(1) Whenever a ↦ b and a ↦ c, b ≡ c.

(2) If a:A and a ↦ b then b:A too.

A corollary of (1) is that a⇑ iff ¬(a⇓). It is not hard to check that a program a is a value iff it is ↦-normal, which is to say that ¬(a ↦). Hence the set of values is exactly the image of the evaluation relation, that is, {b | ∃a(a ⇓ b)}.

Given the dynamic semantics, we can state a form of Morris (1968) contextual equivalence.

Definition 2.7 Contextual order, ⊏ ∼ ⊆ Rel, and contextual equivalence, ≃ ⊆ Rel, are given by:

a ⊏ ∼ b iff whenever a, b:A and −:A ⊢ e: Bool, that e[a]⇓ implies e[b]⇓ too.
a ≃ b iff a ⊏ ∼ b and b ⊏ ∼ a.

The idea is that two programs are equivalent if no amount of programming can tell them apart. This is also known as ‘observational congruence’ (Meyer and Cosmadakis 1988). Two programs are distinct if there is a context that distinguishes them. The central theme of these notes is to establish contextual equivalences by characterising contextual equivalence as a form of bisimilarity. It would be equivalent but less wieldy to formulate contextual equivalence in terms of convergence to true or to false, or to an integer. Another common variation is to define contextual equivalence on open expressions using variable-capturing contexts; we will show in Proposition 3.14 that this variation makes no difference.

2.2 Induction and Co-induction

This section recalls the dual foundations of induction and co-induction. We derive strong versions of both. Let U be some universal set and F : ℘(U) → ℘(U) be a monotone function (that is, F (X) ⊆ F (Y) whenever X ⊆ Y).

Induction and co-induction are dual proof principles that derive from the definition of a set to be the least or greatest solution, respectively, of equations of the form X = F (X).

First some definitions. A set X ⊆ U is F -closed iff F (X) ⊆ X. Dually, a set X ⊆ U is F -dense iff X ⊆ F (X). A fixpoint of F is a solution of the equation X = F (X). Let μX. F (X) and νX. F (X) be the following subsets of U.

\begin{matrix}μX. F (X) & =^{def} & ⋂\{X | F (X) ⊆ X\} \\ νX. F (X) & =^{def} & ⋃\{X | X ⊆ F (X)\} \end{matrix}

Lemma 2.8

(1) μX. F (X) is the least F -closed set.

(2) νX. F (X) is the greatest F -dense set.

Proof We prove (2); (1) follows by a dual argument. Since νX. F (X) contains every F -dense set by construction, we need only show that it is itself F -dense, for which the following lemma suffices.

If every X_{i} is F -dense, so is the union ⋃_{i} X_{i}.

Since X_{i} ⊆ F (X_{i}) for every i, ⋃_{i} X_{i} ⊆ ⋃_{i} F (X_{i}). Since F is monotone, F (X_{i}) ⊆ F (⋃_{i} X_{i}) for each i. Therefore ⋃_{i} F (X_{i}) ⊆ F (⋃_{i} X_{i}), and so we have ⋃_{i} X_{i} ⊆ F (⋃_{i} X_{i}) by transitivity, that is, ⋃_{i} X_{i} is F -dense. ■

Theorem 2.9 (Tarski)

(1) μX. F (X) is the least fixpoint of F.

(2) νX. F (X) is the greatest fixpoint of F.

Proof Again we prove (2) alone; (1) follows by a dual argument. Let ν = νX. F (X). We have ν ⊆ F (ν) by Lemma 2.8. So F (ν) ⊆ F (F (ν)) by monotonicity of F. But then F (ν) is F -dense, and therefore F (ν) ⊆ ν. Combining the inequalities we have ν = F (ν); it is the greatest fixpoint because any other is F -dense, and hence contained in ν. ■

We say that μX. F (X), the least solution of X = F (X), is the set inductively defined by F, and dually, that νX. F (X), the greatest solution of X = F (X), is the set co-inductively defined by F. We obtain two dual proof principles associated with these definitions.

Induction:  μX. F (X) ⊆ X if X is F -closed.
Co-induction: X ⊆ νX. F (X) if X is F -dense.

Mathematical induction is a special case. Suppose there is an element 0 ∈ U and an injective function S : U → U. If we define a monotone function F : ℘(U) → ℘(U) by

F (X) =^{def} {0} ∪ {S(x) | x ∈ X}

and set ℕ =^{def} μX. F (X), the associated principle of induction is that ℕ ⊆ X if F (X) ⊆ X, which is to say that

ℕ ⊆ X if both 0 ∈ X and ∀x ∈ X(S(x) ∈ X).

We can refine co-induction (and dually induction) using the following equations.

Proposition 2.10 Let U be an arbitrary universal set and let F : ℘(U) → ℘(U) be some monotone function. If ν =^{def} νX. F (X) we have:

ν = νX. F (X) ∪ ν  (ν.I)
= νX. F (X ∪ ν)  (ν.II)
= νX. F (X ∪ ν) ∪ ν (ν.III)

Proof Make the following definitions.

ν_{1} =^{def} νX. F (X) ∪ ν
ν_{2} =^{def} νX. F (X ∪ ν)
ν_{3} =^{def} νX. F (X ∪ ν) ∪ ν

We must show that each ν_{i} equals ν. Since ν ⊆ F (ν) it follows by coinduction that ν ⊆ ν_{i} for each i. The reverse inclusions take a little more work.

ν_{2} ⊆ ν. Since ν is a fixpoint of F, which is monotone, we have ν = F (ν) ⊆ F (ν_{2} ∪ ν). Now ν_{2} ⊆ F (ν_{2} ∪ ν) so ν_{2} ∪ ν ⊆ F (ν_{2} ∪ ν), and therefore

ν_{2} ∪ ν ⊆ ν by co-induction. Hence ν_{2} ⊆ ν.

ν_{1} ⊆ ν_{2}. We have ν_{1} = F (ν_{1}) ∪ ν = F (ν_{1}) ∪ F (ν) ⊆ F (ν_{1} ∪ ν). So ν_{1} ⊆ νX. F (X ∪ ν).

ν_{3} ⊆ ν_{2}. We have ν_{3} = F (ν_{3} ∪ ν) ∪ ν = F (ν_{3} ∪ ν) ∪ F (ν) = F (ν_{3} ∪ ν) since F (ν) ⊆ F (ν_{3} ∪ ν). Hence ν_{3} ⊆ νX. F (X ∪ ν). ■

Paulson (1993) implements co-induction principles based on these equations in Isabelle. Dual equations strengthen induction; for instance, the dual of (ν.II), μ = μX. F (X ∩μ), corresponds to the strong induction of Camilleri and Melham (1992) in HOL: μ ⊆ X if F (X ∩ μ) ⊆ X. Equation (ν.III) and its dual justify the following principles, where μ and ν are the least and greatest fixpoints, respectively, of monotone F.

Strong Induction:  μ ⊆ X if F (X ∩ μ) ∩ μ ⊆ X.
Strong Co-induction: X ⊆ ν if X ⊆ F (X ∪ ν) ∪ ν.

For numbers, our strong induction yields ℕ ⊆ X if {0} ∪ {S(x) ∈ ℕ | x ∈ X & x ∈ ℕ} ⊆ X.

Aczel (1977) is the standard reference on inductive definitions. Davey and Priestley (1990) give a more recent account of fixpoint theory, including Tarski’s theorem. Both Winskel (1993) and Pitts (1994b) explain how sets of rules give rise to inductive definitions of operational semantics, with associated principles of rule induction. Our use of ‘closed’ and ‘dense’ differs slightly from Aczel’s; if R is a set of rules, he says a set is ‘R-closed’ or ‘R-dense’ to mean it is in our sense F -closed or F -dense, respectively, where F is the functional determined by the rule set R. Aczel mentions the dual of induction in passing, but ‘co-induction’ seems first to have been used by Milner and Tofte (1991).

The standard theory of inductive and co-inductive definitions is nonconstructive in that it relies on Tarski’s impredicative definitions of μX. F (X) and νX. F (X). They are formed by quantifying over classes of sets, the sets of F -closed and F -dense sets respectively, that include themselves. Cousot and Cousot (1979) develop a constructive version of fixpoint theory. Coquand (1993) is developing a predicative type theory that explains seemingly impredicative definitions—for instance of infinite streams—in purely inductive terms.

2.3 Divergence

We can characterise divergence co-inductively in terms of unbounded reduction. Let function D : ℘(Prog) → ℘(Prog) be such that

D(X) =^{def} {a | ∃b(a ↦ b & b ∈ X)}.

We can easily see that D is monotone. Hence it possesses a greatest fixpoint, νX. D(X), which is the greatest D-dense set. We can show that this coinductive definition matches the one from Definition 2.5, that a⇑ iff whenever a ↦^{∗} b, then b ↦.

Theorem 2.11 ⇑ = νX. D(X).

Proof Let ν be νX. D(X).

ν ⊆ ⇑. Suppose that a ∈ ν. We must show whenever a ↦^{∗} b, that b ↦. If a ∈ ν, then a ∈ D(ν) so there is an a′ with a ↦ a′ and a′ ∈ ν. Furthermore since reduction is deterministic, a′ is unique. By iterating this argument, whenever a ∈ ν and a ↦^{∗} b it must be that b ∈ ν. Therefore b ↦.

⇑ ⊆ ν. By co-induction it suffices to prove that set ⇑ is D-dense. Suppose that a⇑. Since a ↦^{∗} a, we have a ↦, that is, a ↦ b for some b. But whenever b ↦^{∗} b′ it must be that a ↦^{∗} b′ too. In fact b′ ↦ since a⇑. Hence b⇑ too, a ∈ D(⇑) and therefore ⇑ is D-dense.

■

PCF plus streams includes divergent programs, but only because of recursive functions, Δ_{μ→} in Table 4. Reduction in Δ_{→}∪Δ_{A}∪Δ_{[−]} can be shown to be normalising by standard methods (see Girard, Taylor, and Lafont (1989), for instance). Given recursive functions, we can define a program Ω^{A} at any type A to be (rec(f:Num → A, x:Num)f(x))(\underline{0}) and we have

(rec(f:Num → A, x:Num)f(x))(\underline{0}) ↦ (rec(f:Num → A, x:Num)f(x))(\underline{0})

by (Red Rec). Hence the set {Ω^{A}} is D-dense, that is, {Ω^{A}} ⊆ D({Ω^{A}}). So {Ω^{A}} ⊆ ⇑ by co-induction, and therefore Ω^{A}⇑.

It is convenient in Section 4.4 to have a co-inductive characterisation of divergence in terms of many-step reductions. Recall that R^{+} is the transitive closure of relation R. If map D_{+} : ℘(Prog) → ℘(Prog) is

D_{+}(X) =^{def} {a | ∃b(a ↦^{+} b & b ∈ X)}

it is straightforward to prove the following.

Proposition 2.12 ⇑ = νX. D_{+}(X).

Proof Let ν be νX. D_{+}(X). By co-induction it suffices to show that ⇑ ⊆ D_{+}(⇑) and that ν ⊆ D(ν). The former is the easy inclusion, as ⇑ = D(⇑). As for the latter, suppose that a ∈ ν. Since ν = D_{+}(ν) there is b such that a ↦^{n+1} b and b ∈ ν. If n = 0 then a ∈ D(ν) immediately. Otherwise there is c with a → c and c →^{+} b. So c ∈ D_{+}(ν) by definition, and hence a ∈ D(ν). In either case a ∈ D(ν), as required. ■

Observations

α ::= @a  (A → B passive)

                    | n | true | false (Num, Bool active)

| nil | hd | tl  ([A] active)

a:A  A active  a ↦ a′  a′ ⟶^{α} b
\overline{(Trans Red)}

a ⟶^{α} b

a ⟶^{@b} a(b) if a:B → A and b:B (Trans Fun)
\underline{n} ⟶^{n} 0  (Trans Num)

                true ⟶^{true} 0  false ⟶^{false} 0 (Trans Bool)

nil ⟶^{nil} 0  (Trans Nil)
a:: b ⟶^{hd} a  (Trans Hd)
a:: b ⟶^{tl} b  (Trans Tl)

Table 5: Observations on PCF plus streams

Experiments propagate divergence. Using the fact that reduction is closed under any under experiment, we can easily check the following.

Proposition 2.13 Suppose −:A ⊢ E : B and a:A. If a⇑ then E[a]⇑ too.

Hughes and Moran (1995) give an alternative, ‘big-step’, co-inductive formulation of divergence.

2.4 Bisimilarity

To characterise contextual equivalence co-inductively, we begin with a labelled transition system that characterises the immediate observations one can make of a program.

Definition 2.14 (Labelled Transition System) Table 5 specifies a set Act of actions, ranged over by α, and a partition of the types into two kinds, active and passive. Let 0 be some arbitrary divergent program of some active type. The labelled transition system is a family of relations (⟶^{α} ⊆ Prog × Prog | α ∈ Act), given inductively by the (Trans -) rules in Table 5.

The transitions are designed to correspond to the observations contexts can make of programs. Programs of active type have transitions iff they converge. Programs of passive type unconditionally have transitions. We discuss the active/passive distinction further in Section 5.1.

Lemma 2.15 Suppose a:A and A is active. Then a⇓ iff ∃α, b(a ⟶^{α} b).

Proof We can easily prove by rule induction on transition a ⟶^{α} b that a⇓. On the other hand, any value has a transition, so if a ⇓ v, a has a transition too, by iterating (Trans Red). ■

The labelled transition system is image-singular in the following sense.

Lemma 2.16 Whenever a ⟶^{α} b and a ⟶^{α} c then b ≡ c.

Proof Suppose a:A. If A is passive, then only one rule can derive either a ⟶^{α} b or a ⟶^{α} c and by inspection b ≡ c. If A is active, by rule induction on their derivations there are values u and v such that a ⇓ u and u ⟶^{α} b, and a ⇓ v and v ⟶^{α} c. By determinacy of ⇓, a consequence of Proposition 2.6(1), u ≡ v, and then by inspection it follows that b ≡ c. ■

The derivation tree of a program a is the potentially infinite tree whose nodes are programs, whose arcs are labelled transitions, and which is rooted at a. Following Milner (1989), we wish to regard two programs as behaviourally equivalent iff their derivation trees are the same when we ignore the syntactic structure of the programs labelling the nodes. We formalise this idea by requiring our behavioural equivalence to be a relation ∼ ⊆ Rel that satisfies property (∗): whenever (a, b) ∈ Rel, a ∼ b iff

(1) whenever a ⟶^{α} a′ ∃b′ with b ⟶^{α} b′ and a′ ∼ b′;

(2) whenever b ⟶^{α} b′ ∃a′ with a ⟶^{α} a′ and a′ ∼ b′.

In fact there are many such relations; the empty set is one. We are after the largest or most generous such relation. We can define it co-inductively as follows. First define two functions [−], ⟨−⟩ : ℘(Rel) → ℘(Rel) by

[S] =^{def} {(a, b) | whenever a ⟶^{α} a′ there is b′ with b ⟶^{α} b′ and a′ S b′}
⟨S⟩ =^{def} [S] ∩ [S^{op}]^{op}

where S ⊆ Rel. By examining element-wise expansions of these definitions, it is not hard to check that a relation satisfies property (∗) iff it is a fixpoint of function ⟨−⟩. One can easily check that both functions [−] and ⟨−⟩ are monotone. Hence what we seek, the greatest relation to satisfy (∗), does exist, and equals νS. ⟨S⟩, the greatest fixpoint of ⟨−⟩. We make the following standard definitions (Milner 1989).

• Bisimilarity, ∼ ⊆ Rel, is νS. ⟨S⟩.

• A bisimulation is a ⟨−⟩-dense relation.

Bisimilarity is the greatest bisimulation and ∼ = ⟨∼⟩. Again by expanding the definitions we can see that relation S ⊆ Rel is a bisimulation iff a S b implies

• Whenever a ⟶^{α} a′ there is b′ with b ⟶^{α} b′ and a′ S b′;

• Whenever b ⟶^{α} b′ there is a′ with a ⟶^{α} a′ and a′ S b′.

An asymmetric version of bisimilarity is of interest too. Let a simulation be a [−]-dense relation. Let similarity, ≲ ⊆ Rel, be νS. [S], the greatest simulation.

From Lemma 2.15 we know that if A is an active type, the derivation tree of the combinator Ω^{A} is empty. In particular, the tree of 0 is empty. We used 0 in defining the transition system to indicate that after observing the value of a literal there is nothing more to observe.

2.5 The Map/Iterate Example

To motivate study of bisimilarity, let us see how straightforward it is to use co-induction to establish that two lazy streams are bisimilar. Suppose map and iterate are a couple of builtin constants specified by the following equations.

    map f nil = nil
    map f (x :: xs) = f x :: map f xs
    iterate f x = x :: iterate f (f x)

These could easily be turned into formal definitions of two combinators, with each equation being a valid series of reductions, but we omit the details. Pattern matching on streams would be accomplished using scase. Intuitively the streams

             iterate f (f x) and map f (iterate f x)

are equal, because they both consist of the sequence

f x:: f^{2} x:: f^{3} x:: f^{4} x:: ⋯

We cannot directly prove this equality by induction, because there is no argument to induct on. Instead we can easily prove it by co-induction, via the following lemma.

Lemma 2.17 If S ⊆ Rel is

{(iterate f (f x), map f (iterate f x)) | ∃A(x:A & f:A → A)}

then S ⊆ ⟨S ∪ ∼⟩.

Proof To show S ⊆ ⟨S ∪ ∼⟩ we must consider any pair (a, b) ∈ S and check that each transition a ⟶^{α} a′ is matched by a transition b ⟶^{α} b′, such that either a′ S b′ or a′ ∼ b′, and vice versa. Suppose then that a is iterate f (f x), and b is map f (iterate f x). We can calculate the following reductions.

a ↦^{+} f(x) :: (iterate f (f (f x)))
b ↦^{+} f(x) :: (map f (iterate f (f x)))

Using the reductions above we can enumerate all the transitions of a and b.

a ⟶^{hd} f x  (1)
a ⟶^{tl} iterate f (f (f x))  (2)
b ⟶^{hd} f x  (3)
b ⟶^{tl} map f (iterate f (f x))  (4)

Now it is plain that (a, b) ∈ ⟨S ∪∼⟩. Transition (1) is matched by (3), and vice versa, with f x ∼ f x (since ∼ is reflexive). Transition (2) is matched by (4), and vice versa, with iterate f (f (f x)) S map f (iterate f (f x)). ■

Hence S ⊆ ∼ by strong co-induction (Section 2.2). A corollary then is that

               iterate f (f x) ∼ map f (iterate f x)

for any suitable f and x, what we set out to show.

2.6 Theory of Bisimilarity

We postpone till Section 3 the lengthy proof that bisimilarity is a congruence. We finish this section by proving a good many properties of bisimilarity mainly by easy co-inductions. First some general facts; we prove them for PCF plus streams but in fact they hold for all the languages considered in these notes.

Proposition 2.18

(1) ≲ is a preorder and ∼ an equivalence relation.

(2) ↦⊆ ∼

(3) ⇓ ⊆ ∼

(4) ∼ ⊆ ≲

(5) ≲ ∩ ≲^{op} ⊆ ∼

(6) {(a, b) ∈ Rel | a⇑ & b⇑} ⊆ ∼

Proof

(1) Similar to Proposition 4.2 of Milner (1989).

(2) If S is {(a, b) | a ↦ b}, it is enough by strong co-induction to show that S ⊆ ⟨S ∪ ∼⟩. It suffices to consider the transitions of any a, b:A with a ↦ b. We first consider any arbitrary transition a ⟶^{α} a′. If A is active, then by determinacy of ↦ it must be that b ⟶^{α} a′ and we have a′ ∼ a′ by reflexivity. Otherwise we must analyse the transition rules for functions, the one passive type.

(Trans Fun) Here α is @c and a′ is a(c). We can derive b ⟶^{α} b(c) and we have a(c) S b(c).

Dually, we must consider any arbitrary transition b ⟶^{α} b′. If A is active by (Trans Red) it must be that a ⟶^{α} b′ too, and b′ Id b′. If A is passive, by a similar case analysis as before we can exhibit a′ such that

a ⟶^{α} a′ and a′ S b′.

(3) Combine (2) and the fact that ∼ is a preorder.

(4) Since ∼ = ⟨∼⟩ = [∼] ∩ [∼^{op}]^{op}, ∼ ⊆ [∼] and hence ∼ ⊆ ≲.

(5) Let S = ≲ ∪ ≲^{op}. By showing that S is a bisimulation, we will have that ≲ ∪ ≲^{op} ⊆ ∼. Since S = S^{op}, it suffices to show that S ⊆ [S]. Consider any (a, b) ∈ S and any transition a ⟶^{α} a′. Since a ≲ b there is b′ with b ⟶^{α} b′ and a′ ≲ b′. Then since b ≲ a there must be an a′′ with a ⟶^{α} a′′ and b ≲ a′′. But since the transition relation is imagesingular, Lemma 2.16, a′ ≡ a′′ and hence we have a′ S b′ and therefore S ⊆ [S].

(6) It is easy to check that {(a, b) ∈ Rel | a⇑ & b⇑} is a bisimulation. ■

Since ∼ is symmetric, (4) and (5) imply the equation ∼ = ≲ ∩ ≲^{op}. The latter relation is sometimes called ‘mutual similarity’. In a nondeterministic calculus such as CCS, the transition system fails to be image singular and mutual similarity strictly contains bisimilarity, that is, property (5) fails.

For any type A define the following.

Total(A) =^{def} ∀a:A∃b:A(b ⇓ b & a ∼ b)
Ω_{∼}^{A} =^{def} {a | a:A & a ∼ Ω^{A}}

Total(A) asserts that every program of type A equals a value. Ω_{∼}^{A} is the ∼- equivalence class of Ω^{A}. A corollary of (6) above is that ⇑^{A} ⊆ Ω_{∼}^{A} irrespective of the type A, where ⇑^{A} = {a:A | a⇑}. The converse depends on A.

Proposition 2.19 For any type A, the following are equivalent.

(1) Ω_{∼}^{A} ⊆ ⇑^{A}, that is, ∀a:A(a ∼ Ω^{A} ⇒ a⇑)

(2) ∀a:A(a⇓ ⇒ a ≁ Ω^{A})

(3) ∀a, b:A(a⇓ & a ∼ b ⇒ b⇓)

(4) ¬Total(A)

Proof

(1) ⇔ (2) Contrapositives of one another.

(2) ⇒ (3) For a contradiction, suppose a⇓, a ∼ b and b⇑. Since ⇑^{A} ⊆ Ω_{∼}^{A}, b ∼ Ω^{A}, and a ∼ Ω^{A} by transitivity. But since a⇓ applying (2) yields a ≁ Ω^{A}. Contradiction.

(3) ⇒ (2) Again for a contradiction, suppose a⇓ and a ∼ Ω^{A}. Applying (3) yields Ω^{A}⇓, but Ω^{A}⇑ by definition.

(4) ⇒ (1) Property (4) means there is an a such that ¬∃b:A(b⇓ & a ∼ b), that is, a equals no convergent term. So a⇑ in particular, since a ∼ a. Therefore a ∼ Ω^{A}, since ⇑^{A} ⊆ Ω_{∼}^{A}. By transitivity, Ω^{A} equals no convergent term, that is, property (1), Ω_{∼}^{A} ⊆ ⇑^{A}.

¬(4) ⇒ ¬(1) Property Total(A) applied to Ω^{A} yields ∃b(Ω^{A} ∼ b & b⇓), contradicting (1). ■

A corollary is that every type A satisfies one of Total(A) or Ω_{∼}^{A} ⊆ ⇑^{A}, but not both. It is easy to see that every active type, A, satisfies Ω_{∼}^{A} ⊆ ⇑^{A}.

If a:A → B then a ∼ λ(x)a(x)  (Fun Eta)
If a, b:A → B then a ∼ b if ∀c:A(a(c) ∼ b(c))  (Fun Ext)
If as:[A], then as ∼ scase(as, nil, λ(x)λ(xs)x:: xs). (Stm Eta)
If \underline{ℓ} ∼ \underline{ℓ}′ then ℓ = ℓ′.  (Inj Lit)
If λ(x:A)e ∼ λ(x:A)e′ then e[a/x] ∼ e′[a/x] for any a:A. (Inj Fun)
If a:: as ∼ b:: bs then a ∼ b and as ∼ bs.  (Inj Stm)

Table 6: Properties Specific to PCF plus Streams

Proposition 2.20 If A active, Ω_{∼}^{A} ⊆ ⇑^{A}.

Proof Suppose a:A and that A is active. From Lemma 2.15 it follows that if a ∼ Ω, a has no transitions, and hence that it diverges. ■

Now we turn to properties specific to PCF plus streams.

Proposition 2.21 All the properties in Table 6 hold.

Proof We examine each property in turn.

(Fun Eta) If S = {(a, λ(x)a(x)) | a:A → B} we can show that S ⊆ ⟨∼⟩ and hence that S ⊆ ∼. The only transitions of a and λ(x)a(x) are of the form a ⟶^{@c} a(c) and λ(x)a(x) ⟶^{@c} (λ(x)a(x))(c) for arbitrary c. But by (Red Beta) we have (λ(x)a(x))(c) ↦ a(c), which establishes that S ⊆ ⟨∼⟩.

(Fun Ext) Suppose that a(c) ∼ b(c) for any c. Clearly then (a, b) ∈ ⟨∼⟩.

(Stm Eta) Consider any as:[A]. Either as⇑, as ⇓ nil or as ⇓ b:: bs. In any case we can check that as is bisimilar to scase(a, nil, λ(x)λ(xs)x::xs). In the first case both diverge; in the other cases both evaluate to the same thing.

Finally (Inj Lit), (Inj Fun) and (Inj Stm) follow trivially. ■

The converses of (Fun Ext), (Inj Lit), (Inj Fun) and (Inj Stm) hold, and are instances of the congruence property of ∼ that we shall prove in the next section. In fact, these particular instances can be proved directly. A corollary of (Fun Eta) is that Total(A → B) holds for any function type A → B. In PCF plus streams, then, Total(A) ⇔ A passive.

For instance, we can prove λ(x:A)Ω^{B} ∼ Ω^{A→B}, which are distinguished by the standard form of applicative bisimulation. Consider any a:A. We have (λ(x:A)Ω^{B}) a ∼ Ω^{B} by (Red Beta) and Ω^{A→B} a ∼ Ω^{B} since ⇑^{B} ⊆ Ω_{∼}^{B}. Hence λ(x:A)Ω^{B} ∼ Ω^{A→B} by (Fun Ext).

3 Congruence of Bisimilarity

Here the main objective is to introduce Howe’s method for proving that similarity is a precongruence, and the consequences that bisimilarity is a congruence, and that bisimilarity equals contextual equivalence. We also consider experimental equivalence, another co-inductive characterisation of contextual equivalence suggested by a generalisation of Milner’s context lemma. But we show that co-induction based on experimental equivalence is a weaker principle than co-induction using bisimilarity.

3.1 Congruence and Precongruence

A congruence relation is an equivalence that is preserved by all contexts. To state this formally requires a little preliminary work.

Definition 3.1 Let a proved expression be a triple (Γ, e, A) such that Γ ⊢ e: A. If Γ = x_{1}:A_{1}, …, x_{n}:A_{n}, a Γ-closure is a substitution ·[a⃗/x⃗] where each a_{i}:A_{i}. Now if R ⊆ Rel, let its open extension, R^{∘}, be the relation between proved expressions such that

(Γ, e, A) R^{∘} (Γ, e′, A) iff e[a⃗/x⃗] R e′[a⃗/x⃗] for any Γ-closure [a⃗/x⃗].

For instance, relation Rel^{∘} holds between any two proved expressions (Γ, e, A) and (Γ′, e′, A′) provided only that Γ = Γ′ and A = A′. As a matter of notation we shall write Γ ⊢ e R e′ : A to mean that (Γ, e, A) R (Γ, e′, A) and, in fact, we shall usually omit the type information.

We need the following notion, of compatible refinement, to characterise what it means for a relation on open expressions to be a precongruence.

Definition 3.2 If R ⊆ Rel^{∘}, its compatible refinement, R̂ ⊆ Rel^{∘}, is defined inductively for PCF plus streams by the rules in Table 7. Define a relation R ⊆ Rel^{∘} to be a precongruence iff it contains its own compatible refinement, that is, R̂ ⊆ R. Let a congruence be an equivalence relation that is a precongruence.

The rules in Table 7 formalise the intention that two expressions are related by R̂ when they have the same outermost form and their immediate subexpressions are related by R.

The following lemma shows that this definition is equivalent to the more common one based on variable-capturing contexts. Let C stand for a variablecapturing context, that is, an expression, not identified up to alpha-conversion,

\overline{(Comp x)} ; Γ ⊢ x R̂ x Γ ⊢ e_{1} R e′_{1} Γ ⊢ e_{2} R e′_{2} \overline{(Comp Appl)}

Γ ⊢ e_{1}(e_{2}) R̂ e′_{1}(e′_{2})

Γ, x:A ⊢ e R e′

\overline{(Comp Fun)}

Γ ⊢ λ(x:A)e R̂ λ(x:A)e′

\overline{(Comp Lit)} ; Γ ⊢ \underline{ℓ} R̂ \underline{ℓ}

  Γ ⊢ e R e′  κ ∈ {succ, pred, zero}

\overline{(Comp κ)}

Γ ⊢ κ(e) R̂ κ(e′)

Γ ⊢ e_{1} R e′_{1} Γ ⊢ e_{2} R e′_{2} Γ ⊢ e_{3} R e′_{3}

\overline{(Comp If)}

Γ ⊢ if e_{1} then e_{2} else e_{3} R̂ if e′_{1} then e′_{2} else e′_{3}

Γ, f:A → B, x:A ⊢ e R e′

\overline{(Comp Rec)}

Γ ⊢ rec(f:A → B, x:A)e R̂ rec(f:A → B, x:A)e′

Γ ⊢ e_{1} R e′_{1} Γ ⊢ e_{2} R e′_{2} Γ ⊢ e_{3} R e′_{3} (Comp Scase)

Γ ⊢ scase(e_{1}, e_{2}, e_{3}) R̂ scase(e′_{1}, e′_{2}, e′_{3})

Γ ⊢ e_{1} R e′_{1} Γ ⊢ e_{2} R e′_{2}

\overline{(Comp Cons)}

Γ ⊢ e_{1} :: e_{2} R̂ e′_{1} :: e′_{2}

\overline{(Comp Nil)}

                              Γ ⊢ nil R̂ nil

Table 7: The compatible refinement of a relation whose bound variables are distinct, containing a single typed hole denoted by ‘−_{A}’ and subject to the extra type assignment rule Γ ⊢ −_{A}: A. We write C[e] for the outcome of filling the hole in the context C with the expression e. Free variables of e may be bound by this process.

Lemma 3.3 Assume that R ⊆ Rel^{∘} is a preorder. R is a precongruence iff (Cong R) holds. (Cong R) is given by

Γ ⊢ C[−_{A}] : B Γ, Γ′ ⊢ e R e′ : A
\overline{(Cong R)}
Γ ⊢ C[e] R C[e′] : B

where Γ′ is the list of bound variables in C whose scope includes the hole.

Proof

(Only If) Suppose that preorder R satisfies R̂ ⊆ R. We prove by induction on the derivation of Γ ⊢ C[−_{A}] : B that if Γ′ is the environment bound in C, then Γ, Γ′ ⊢ e R e′ implies Γ ⊢ C[e] R C[e′].

C is −_{A}. Such a context binds no variables, so Γ′ = ∅. We have Γ ⊢ e R e′ by assumption.

C is a variable Impossible because C has to contain a hole.

C is an application. Either C is C_{0} e_{0} or e_{0} C_{0}, where C_{0} is a smaller context and e_{0} is an ordinary expression (with no hole). In the first case we have Γ ⊢ C_{0} : C → B and Γ ⊢ e_{0} : C for some type C. By induction hypothesis we have Γ ⊢ C_{0}[e] R C_{0}[e′] : C → B since C_{0} binds the same variables as C. By (Comp Appl) and reflexivity we have Γ ⊢ C_{0}[e] e_{0} R C_{0}[e′] e_{0} : B, that is, Γ ⊢ C[e_{0}] R C[e′] : B. The second case, when the context is e_{0} C_{0}, is similar.

C is λ(x:C_{1})C′. The environment Γ′ of variables bound by C must be x:C_{1}, Γ′′ with Γ, x:C_{1} ⊢ C′: C_{2} where B ≡ C_{1} → C_{2}. By induction hypothesis we have Γ, x:C_{1} ⊢ C′[e] R C′[e′] : C_{2} since Γ, x:C_{1}, Γ′′ ⊢ e R e′ and Γ′′ is the variables bound in C′. Rule (Comp Fun) now yields Γ ⊢ C[e] R C[e′] : B.

Cases for the other forms of contexts follow similarly.

(If) Suppose that preorder R satisfies (Cong R). We must show that R̂ ⊆ R. We need to consider all the rules of compatible refinement from Table 7.

(Comp x) R is reflexive.

(Comp Lit) R is a reflexive.

(Comp Appl) Suppose that Γ ⊢ e_{1} R e′_{1} and Γ ⊢ e_{2} R e′_{2}. By (Cong R) we have Γ ⊢ e_{1}(e_{2}) R e′_{1}(e_{2}) and Γ ⊢ e′_{1}(e_{2}) R e′_{1}(e′_{2}) and therefore

by transitivity that Γ ⊢ e_{1}(e_{2}) R e′_{1}(e′_{2}).

(Comp Fun) Suppose that Γ, x:A ⊢ e R e′. Using context λ(x:A)− we have Γ ⊢ λ(x:A)e R̂ λ(x:A)e′ from (Cong R).

The other cases are similar. ■

3.2 Similarity is a Precongruence

In this section we shall prove that similarity is a precongruence, that is, ˆ≲^{∘} ⊆ ≲^{∘}. Since ∼ equals the symmetrisation of ≲, it follows that bisimilarity is a congruence (a precongruence that is an equivalence). Howe (1989) originally proved that similarity was a precongruence for a broad class of lazy computation systems. These were untyped and based on an evaluation relation. As in earlier work (Crole and Gordon 1995), we recast his proof in a typed setting and using labelled transitions.

Definition 3.4 Inductively define relation ≲^{•} ⊆ Rel^{∘} by the following rule.

Γ ⊢ e ˆ≲^{•} e′′ Γ ⊢ e′′ ≲^{∘} e′
\overline{(Cand Def)}
Γ ⊢ e ≲^{•} e′

We can present some basic properties of ≲^{•} from Howe’s paper as follows.

Lemma 3.5 ≲^{•} is reflexive and the following rules are valid.

Γ ⊢ e ˆ≲^{•} e′ ; \overline{(Cand Cong)} ; Γ ⊢ e ≲^{•} e′  Γ ⊢ e ≲^{∘} e′ ; \overline{(Cand Sim)} ; Γ ⊢ e ≲^{•} e′
Γ ⊢ e ≲^{•} e′′ Γ ⊢ e′′ ≲^{∘} e′
\overline{(Cand Right)}
Γ ⊢ e ≲^{•} e′
Γ, x:A ⊢ e_{1} ≲^{•} e′_{1} Γ ⊢ e_{2} ≲^{•} e′_{2} : A
\overline{(Cand Subst)}
Γ ⊢ e_{1}[e^{2}/x] ≲^{•} e′_{1}[e′_{2}/x]

Moreover, ≲^{•} is the least relation closed under (Cand Cong) and (Cand Right).

Proof First note that ≲^{∘} is a preorder, since similarity is a preorder and by definition of open extension. Given then that ≲^{∘} is reflexive, reflexivity of ≲^{•} follows by proving Γ ⊢ e ≲^{•} e by structural induction on e. Rule (Cand Cong) follows at once from (Cand Def). Now the reflexivity of ≲^{•} means that Id^{∘} ⊆ ≲^{•}. Compatible refinement is monotone, so if Id = {(a, b) ∈ Rel | a ≡ b} we have Îd^{∘} ⊆ ˆ≲^{•}, which is to say Id^{∘} ⊆ ˆ≲^{•}. Thus we have Γ ⊢ eˆ≲^{•}e whenever Γ ⊢ e, and hence (Cand Sim) follows from (Cand Def).

For (Cand Right), suppose that Γ ⊢ e ≲^{•} e′′ and Γ ⊢ e′′ ≲^{∘} e′. By (Cand Def) there must be an e′′′ with Γ ⊢ eˆ≲^{•}e′′′ and Γ ⊢ e′′′ ≲^{∘} e′′. By transitivity of ≲^{∘} we have Γ ⊢ e′′′ ≲^{∘} e′, and hence by (Cand Def) that Γ ⊢ e ≲^{•} e′ as required.

(Cand Subst) follows by a routine rule induction on the judgment Γ, x:B ⊢ e_{1} ≲^{•} e′_{1}.

Finally suppose that R is another relation to satisfy both (Cand Cong) and (Cand Right). We must show that ≲^{•} ⊆ R. We prove by rule induction that Γ ⊢ e ≲^{•} e′ implies Γ ⊢ e R e′. Suppose then that Γ ⊢ e ≲^{•} e′, and hence by (Cand Def) that there is e′′ with Γ ⊢ eˆ≲^{•}e′′ and Γ ⊢ e′′ ≲^{∘} e′. By the induction hypothesis we have Γ ⊢ eR̂e′′. So by (Cand Cong) for R we have Γ ⊢ e R e′′, and then by (Cand Right) for R that Γ ⊢ e R e′. ■

The proof strategy is to show that ≲^{∘} = ≲^{•}, and then since ≲^{•} is a precongruence, (Cand Cong) it follows that ≲^{∘} is too, as desired. We have ≲^{∘} ⊆ ≲^{•} already, so it remains to prove the reverse inclusion. We do so by coinduction. Here are the key lemmas. Let relation S be {(a, b) | ∅ ⊢ a ≲^{•} b}, the restriction of ≲^{•} to programs.

Lemma 3.6 Whenever a S b and a ↦ a′ then a′ S b.

Proof By rule induction on the relation a ↦ a′. In any case we know from a S b and (Cand Def) there is a program c with ∅ ⊢ a ˆ≲^{•} c ≲^{∘} b. We examine each rule in turn.

(Red Beta) Here a is (λ(x:A)e)(a_{2}) and a′ is e[a^{2}/x]. We start with an analysis of ∅ ⊢ (λ(x)e)(a_{2}) ˆ≲^{•} c.

• From (Comp Appl), c must be of the form c_{1}(c_{2}) with ∅ ⊢ λ(x)e≲^{•} c_{1} and ∅ ⊢ a_{2} ≲^{•} c_{2}.

• From (Cand Def) and (Comp Fun), there must be an intermediate λ(x)e′ with ∅ ⊢ λ(x)e ˆ≲^{•} λ(x)e′ ≲^{∘} c_{1} and indeed x:A ⊢ e ≲^{•} e′.

We can fill in the diagram below starting from the similarity λ(x)e′≲c_{1}, and using (Red Beta), Proposition 2.18(2) and (Cand Subst).

\begin{aligned}& λ(x)e′ & ≲ & c_{1} \\ e[a^{2}/x] ≲^{•} e′[c^{2}/x] & ≲ & (λ(x)e′)(c_{2}) & ^{@c_{2}↓} & ≲ & c_{1}(c_{2}) & ^{↓@c_{2}} & ≲ b \end{aligned}

Now we have a′ S b from (Cand Right).

(Red Rec) Here a is a_{1}(a_{2}) where a_{1} is rec(f, x)e, and a′ is e[a^{1}, a^{2}/f, x].

• From (Comp Appl), c takes the form c_{1}(c_{2}) with a_{1} ≲^{•} c_{1} and a_{2} ≲^{•} c_{2}.

• From (Cand Def) and (Comp Rec), there must be an intermediate d ≡ rec(f, x)e′ with ∅ ⊢ a_{1} ˆ≲^{•} d ≲^{∘} c_{1}.

As in the previous case we can fill in the following diagram.

\begin{aligned}& d & ≲ & c_{1} \\ e[a^{1}, a^{2}/f, x] ≲^{•} e′[d, c^{2}/f, x] & ≲ & d(c_{2}) & ^{@c_{2}↓} & ≲ & c_{1}(c_{2}) & ^{↓@c_{2}} & ≲ b \end{aligned}

Hence a′ S b from (Cand Right).

(Red If) Here a is if\underline{bv} then a_{tt} else a_{ff} , with bv ∈ \{tt, ff \}, and a′ is a_{bv}. As before we analyse ∅ ⊢ if\underline{bv} then a_{tt} else a_{ff} ˆ≲^{•} c.

• From (Comp If), c takes the form if c_{1} then c_{tt} else c_{ff} with ∅ ⊢ \underline{bv} ≲^{•} c_{1}, ∅ ⊢ a_{tt} ≲^{•} c_{tt} and ∅ ⊢ a_{ff} ≲^{•} c_{ff} .

• From (Cand Def) and (Comp Lit) it follows that c_{1} ∼ \underline{bv}. Hence c_{1} ⇓ \underline{bv} and c ↦^{∗} c_{bv}.

We have ∅ ⊢ a′ ≡ a_{bv} ≲^{•} c_{bv} ≲ c ≲ b, and so a′ S b by (Cand Right).

(Red Experiment) Here a is E[a_{1}], such that a_{1} ↦ a′_{1} and a′ is E[a′_{1}]. Given ∅ ⊢ E[a_{1}] ˆ≲^{•} c, whatever the form of E we can decompose c into the form E′[c_{1}] with ∅ ⊢ a_{1} ≲^{•} c_{1} and ∅ ⊢ E ˆ≲^{•}E′. Since a_{1} ↦ a′_{1} and a_{1}Sc_{1} we have a′_{1} S c_{1} by induction hypothesis. By considering the possible forms of E, we have ∅ ⊢ a′ ≡ E[a′_{1}] ˆ≲^{•} E′[c_{1}], and hence ∅ ⊢ a′ ˆ≲^{•} c ≲^{∘} b, that is, a′ S b as required.

The other cases, for streams and arithmetic, are similar. ■

Lemma 3.7 If a S b and a ⟶^{α} a′ there is b′ with b ⟶^{α} b′ and a′ S b′.

Proof By rule induction on the derivation of a ⟶^{α} a′. In any case we know from a S b and (Cand Def) there is a program c with ∅ ⊢ a ˆ≲^{•} c ≲^{∘} b.

(Trans Lit) Here a is \underline{ℓ}, α is ℓ, and a′ is 0. From (Comp ℓ) c must equal \underline{ℓ}, and then from \underline{ℓ} ≲ b it follows that b ⟶^{α} 0 too, and certainly 0 S 0, as S is reflexive.

(Trans Fun) Here a is of function type, α is @c and a′ is a(c). Since b is of the same function type, (Trans Fun Passive) admits the transition b ⟶^{α} b(c), and since ≲^{•} is a precongruence, (Cand Cong), we have a(c) S b(c) as required.

(Trans Red) Here a ⟶^{α} a′ was derived from a ↦ a′′ and a′′ ⟶^{α} a′. By Lemma 3.6 we have a′′ S b, so by induction hypothesis we have b ⟶^{α} b′ with a′ S b′, as required.

All cases considered, the result follows. ■

Theorem 3.8 The open extension of similarity is a precongruence.

Proof By Lemma 3.7, S is a simulation, and hence S ⊆ ≲ by co-induction. Open extension is monotone, so S^{∘} ⊆ ≲^{∘}. Now ≲^{•} ⊆ S^{∘} follows from the substitution lemma (Cand Subst) and the reflexivity of ≲^{•} (Lemma 3.5). Hence we have ≲^{•} ⊆ ≲^{∘}. Since (Cand Sim) furnishes the reverse inclusion, we have ≲^{•} = ≲^{∘} and hence ≲^{∘} is a precongruence. ■

3.3 Bisimilarity equals Contextual Equivalence

Given that bisimilarity and similarity are precongruences, it is now easy to show that bisimilarity equals contextual equivalence.

Lemma 3.9 Both ≲ ⊆ ⊏ ∼ and ∼ ⊆ ≃.

Proof First we shall prove ≲ ⊆ ⊏ ∼. Suppose that a ≲ b:A. To see that a ⊏ ∼ b we must consider an arbitrary expression e such that −:A ⊢ e : Bool and show that e[a]⇓ implies e[b]⇓. By supposition we have ∅ ⊢ a≲^{∘} b:A, and so by the congruence property of ≲^{∘} (in fact just (Cand Subst)) it follows that ∅ ⊢ e[a] ≲^{∘} e[b] : Bool. In fact we have e[a] ≲ e[b]. Now e[a] ⇓ \underline{bv} with bv ∈ {tt, ff }. So e[a] ⟶^{bv} 0. Since e[a] ≲ e[b] it must be that e[b] ⟶^{bv} 0 too, and therefore e[b]⇓, as required, by Lemma 2.15. Having now shown that ≲ ⊆ ⊏ ∼, ∼ ⊆ ≃ follows by symmetry. ■

Lemma 3.10 If type A is active there is a Boolean context −:A ⊢ e: Bool such that for any a:A, e[a]⇓ iff a⇓.

Proof Witness the following contexts.

               Bool  −
                Num            zero(−)
                [A]  scase(−, true, λ(x)λ(xs)true)

■

Lemma 3.11 Suppose a:A and A is active. If a ⊏ ∼ b and a ⇓ u there is v with b ⇓ v and u ⊏ ∼ v.

Proof A corollary of Lemma 3.10 is that b⇓ follows from a ⊏ ∼ b and a⇓. The result then follows from ⇓ ⊆ ∼ and Lemma 3.9. ■

Lemma 3.12 Contextual order is a simulation.

Proof Suppose then that a:A, a ⊏ ∼ b and that a ⟶^{α} a′. To show that ⊏ ∼ is a simulation we must find some b′ such that b ⟶^{α} b′ with a′ ⊏ ∼ b′.

Suppose first that A is active. So there must be an intermediate value v such that a ⇓ v and v ⟶^{α} a′. By Lemma 3.11 there is a program u such that b ⇓ u and v ⊏ ∼ u. We proceed to analyse the derivation of v ⟶^{α} b. It suffices to show that u ⟶^{α} b′ with a′ ⊏ ∼ b′, for then we can infer that b ⟶^{α} b′ too. We examine some typical cases.

(Trans Lit) Here v is a literal \underline{ℓ}, α is ℓ and a′ is 0. We know \underline{ℓ} ⊏ ∼ u. It must be that u is \underline{ℓ} or we could tell them apart using a conditional or an equality test. So setting b′ to be 0, we have u ⟶^{α} b′ and a′ ⊏ ∼ b′.

(Trans Hd) Here v is a_{1} :: a_{2}, α is hd and a′ is a_{1}. We know a_{1} :: a_{2} ⊏ ∼ u so using scase to test both sides we can establish that u must be b_{1} :: b_{2} with a_{i} ⊏ ∼ b_{i} for each i. Let b′ be b_{1} and we have u ⟶^{α} b′ with a′ ⊏ ∼ b′.

Secondly we must consider the ways a ⟶^{α} a′ can be derived if A is passive. In PCF plus streams only one rule applies.

(Trans Fun) Here a and b are of function type, α is @c and a′ is a(c). (Trans Fun) admits the transition b ⟶^{α} b(c) too. Now contextual order is closed under contexts, so by appeal to the context −(c) we have a(c) ⊏ ∼ b(c), as required.

All cases considered, it follows that contextual order is a simulation. ■

By combining Lemmas 3.12 and 3.9 we have that bisimilarity equals contextual equivalence.

Theorem 3.13 ∼ = ≃.

Here is a simple application. In Definition 2.7, we defined contextual equivalence on programs using expressions with a single variable, ‘−’, as contexts. A common variation is to define it on open expressions using variable-binding contexts. We can use Theorem 3.13 to show the two versions are one.

Proposition 3.14 Supposing that

(1) ≃^{∘} is a congruence

(2) ↦⊆ ≃

then Γ ⊢ e_{1} ≃^{∘} e_{2} iff for any variable-capturing context C with C[e_{1}], C[e_{2}]:Bool that C[e_{1}]⇓ iff C[e_{2}]⇓.

Proof

(Only If) Suppose that Γ ⊢ e_{1} ≃^{∘} e_{2}. By Lemma 3.3, (1) and (Cong ≃^{∘}), ∅ ⊢ C[e_{1}] ≃^{∘} C[e_{2}] : Bool and therefore C[e_{1}]⇓ iff C[e_{2}]⇓.

(If) Suppose that [a^{1}, …, a^{n}/x_{1}, …, x_{n}] is an arbitrary Γ-closure. We must establish that e_{1}[a⃗/x⃗] ≃ e_{2}[a⃗/x⃗]. Let variable-binding context C be

(λ(x_{1}) ⋯ λ(x_{n})−)(a_{1}) ⋯ (a_{n}).

We have C[e_{i}] ↦^{n} e_{i}[a⃗/x⃗] for each i, and hence by (2) that C[e_{i}] ≃ e_{i}[a⃗/x⃗] for each i. Suppose then that e[e_{1}[a⃗/x⃗]]⇓ for some (closed) context e. We must show that e[e_{2}[a⃗/x⃗]]⇓ too. We have e[e_{1}[a⃗/x⃗]] ≃ e[C[e_{1}] since ≃ is certainly preserved by a closed context such as e, so e[C[e_{1}]⇓. Since e[C] is itself a variable-capturing context of Bool type, we have e[C[e_{2}]⇓ by hypothesis. Now e[C[e_{2}]] ≃ e[e_{2}[a⃗/x⃗]], and therefore e[e_{2}[a⃗/x⃗]]⇓, as required. ■

Hypotheses (1) and (2) follow from Theorem 3.13.

3.4 Experimental Equivalence

We rework Milner’s context lemma for FPC and show it yields yet another co-inductive characterisation of contextual equivalence, but one that is less wieldly than bisimilarity. Milner (1977) showed that contextual equivalence on a combinatory-logic form of PCF is unchanged if we restrict attention to ‘applicative contexts’ of the form − a_{1} … a_{n}. Berry (1981) extended Milner’s proof to the lambda-calculus form of PCF. Here the analogue of an applicative context is an evaluation context of the form E⃗[−], where if E⃗ = E_{1}, …, E_{n} then E⃗[−] is the context E_{1}[⋯ E_{n}[−] ⋯]. Let experimental equivalence, ≈ ⊆ Rel be the relation such that

a ≈ b:A iff whenever −:A ⊢ E⃗[−] : Bool, that E⃗[a]⇓ iff E⃗[b]⇓.

By a straightforward modification of Milner’s argument, we can prove the following context lemma by induction on n.

Lemma 3.15 Suppose a ≈ b:A and that −:A ⊢ e: Bool. If e[a]⇓ in n steps, then e[b]⇓ too.

Proof Similar to Lemma 4.17 on page 46 of Gordon (1994). ■

This property of a language, that experimental equivalence implies contextual equivalence, was named operational extensionality by Bloom (1988). (Bloom called ≈ ‘applicative congruence’.) An easy corollary is that ≈ = ≃. Evaluation contexts make the same distinctions as full-blown contexts. Since it is straightforward to prove that ↦⊆ ≈, for instance, experimental equivalence is a useful definition for establishing equational properties of contextual equivalence, independently of bisimilarity.

Lemma 3.16 ↦⊆ ≈

Proof Suppose that a ↦ b. We must show for any evaluation context E⃗ that if E⃗[a]⇓ then so does E⃗[b]⇓, and the converse. Suppose that E⃗[a] ⇓ v, that is, E⃗[a] ↦^{∗} v. Program E⃗[a] cannot be a value, so there must be a′ with E⃗[a] ↦ a′ ↦^{∗} v. But because E⃗[−] is an evaluation context and reduction is deterministic, it must be that a′ ≡ E⃗[b], and a′ converges. The converse follows easily. ■

Lemma 3.17 If a, b:Bool or Num then a ≈ b iff ∀ℓ(a ⇓ \underline{ℓ} ⇔ b ⇓ \underline{ℓ}).

Proof

(Only If) Suppose that a ≈ b and a ⇓ \underline{ℓ}. For a contradiction, suppose either that b⇑ or b ⇓ \underline{ℓ}′ with ℓ ≠ ℓ′. The former gives rise to a contradiction immediately. For the latter, we may construct an evaluation context E⃗, coding literal equality using pred, zero and if, such that E⃗[c]⇓ iff c ⇓ \underline{ℓ}. So E⃗[a]⇓ while E⃗[b]⇑. Contradiction.

(If) Either a⇑ and b⇑, or a ⇓ \underline{ℓ} and b ⇓ \underline{ℓ} for some literal ℓ. In the former case a ≈ b easily. In the latter case, suppose that E⃗[a]⇓. So E⃗[\underline{ℓ}]⇓ too, and hence E⃗[b]⇓. ■

Furthermore, we can co-inductively characterise experimental equivalence as follows. If S ⊆ Rel, define functional^{1}F (S) ⊆ Rel such that (a, b) ∈ F (S) iff

(1) if a, b:Bool that a⇓ iff b⇓;

(2) whenever E[a] and E[b] are well-typed, (E[a], E[b]) ∈ S.

Proposition 3.18 ≈ = νS. F (S).

Proof Let ν = νS. F (S). It is easy to see that ≈ is F -dense and so ≈ ⊆ ν by co-induction. For the reverse inclusion, first note that since ν = F (ν), it follows that whenever (a, b) ∈ ν and E[a] and E[b] are well-typed, that (E[a], E[b]) ∈ ν too. Suppose then that (a, b) ∈ ν, E⃗[a], E⃗[b]:Bool and E⃗[a]⇓. Since ν = F (ν) it follows by induction on the size of E⃗ that (E⃗[a], E⃗[b]) ∈ ν. Hence if E⃗[a]⇓ it must be that E⃗[b]⇓, by clause (1) of the definition of F. Hence ν ⊆ ≈. ■

This yields a co-induction principle for contextual equivalence but we can improve it as follows.

Proposition 3.19 ≈ = νS. F (≈S≈).

Proof Let ν be νS. F (≈S≈). Since ≈ = νS. F (S) it follows that ≈ ⊆ F (≈) ⊆ F (≈≈≈) (by transitivity of ≈ and monotonicity of F) and so ≈ ⊆ ν by co-induction.

For the other direction, we shall show that ≈ν≈ is F -dense, and hence that ≈ν≈ ⊆ ≈, and hence that ν ⊆ ≈, since Id ⊆ ≈. Suppose then that a≈ν≈b, that is, there are a′ and b′ with a ≈ a′ ν b′ ≈ b.

1We took atomic experiments as primitive—rather than compound evaluation contexts—to allow a simple presentation of this functional.

(1) Suppose that a, b:Bool and a⇓. We must show that b⇓ too. It must be that a′, b′:Bool too, so since a ≈ a′, a′⇓. Now since ν ⊆ F (≈ν≈) it follows that b′⇓ too, and therefore b⇓.

(2) Suppose that E[a] and E[b] are well-typed. We have E[a] ≈ E[a′] from a ≈ b, then E[a′]≈ν≈E[b′], since ν ⊆ F (≈ν≈), and E[b′] ≈ E[b], as b′ ≈ b. In all E[a]≈ν≈E[b].

Hence (a, b) ∈ F (≈ν≈). ■

The proof is a variation on the proof that in CCS a ‘bisimulation up to ∼’ is contained in bisimilarity (see Proposition 4.1). On the face of it, this yields a useful co-induction principle, intuitively via ‘matching experiments.’ To show S is contained in experimental equivalence, it suffices to show that S ⊆ F (≈S≈). For instance, if our candidate relation S contains a pair (a, b) of function type, we must show for every experiment E of form − c that E[a] ≡ a c ≈S≈ b c ≡ E[b], which is equivalent to the bisimulation condition. But suppose S contains a pair (a_{1} :: a_{2}, b_{1} :: b_{2}); we must show that E[a_{1} :: a_{2}] ≈S≈ E[b_{1} :: b_{2}] for all suitable experiments, E, which include the following

scase(−, b, λ(x)λ(xs)e).

Hence we must show e[a^{1}, a^{2}/x, xs] ≈S≈ e[b^{1}, b^{2}/x, xs] which, because of the quantification over the arbitrary expression e is almost as hard as proving contextual equivalence directly, and certainly harder than proving each (a_{i}, b_{i}) ∈ S, the condition for S to be a bisimulation. This is evidence that although the context lemma justifies a certain co-inductive characterisation of contextual equivalence, it is harder to apply than bisimilarity.

4 Refining Bisimulation

In the theory of CCS, there are various forms of ‘bisimulation up to ∼’ that allow simpler proofs by co-induction than plain bisimulation. Our main objective here is to develop co-induction principles that simplify co-induction proofs by exploitation of the determinacy of PCF plus streams. There are two ideas: matching values (Section 4.2) and matching reductions (Section 4.4). Taken together they admit a co-inductive characterisation of bisimilarity without mention of transitions, only equations and reductions.

The Take Lemma of Bird and Wadler (1988) is a well-known technique for proving equivalence of two streams by inducting over their finite approximations. We derive the Take Lemma in Section 4.6 but show that it is less useful than the method of matching values and reductions.

4.1 Bisimulations up to ∼

Milner’s idea of ‘bisimulation up to ∼’ works for any labelled transition system. Suppose S ⊆ Rel. Let S be a bisimulation up to ∼ iff a S b implies

(1) whenever a ⟶^{α} a′ there is b′ such that b ⟶^{α} b′ and a′ ∼S∼ b′; and

(2) whenever b ⟶^{α} b′ there is a′ such that a ⟶^{α} a′ and a′ ∼S∼ b′.

In relational terms, S ⊆ ⟨∼S∼⟩. See Milner (1989, p93) for the standard proof of the following.

Proposition 4.1 (Milner) If S is a bisimulation up to ∼ then ∼S∼ ⊆ ⟨∼S∼⟩, that is, ∼S∼ is a bisimulation.

Corollaries are that ∼S∼ ⊆ ∼ and S ⊆ ∼. Since bisimilarity is trivially a bisimulation up to ∼ it follows that ∼ = νS. ⟨∼S∼⟩. Milner’s result is a coinductive characterisation of bisimilarity. In the theory of CCS it often results in simpler proofs than plain bisimulation. But proofs via a bisimulation up to ∼ still require calculation of transitions.

4.2 Matching Values

In our functional programming context, it is tedious to check all the transitions of an expression, as in the proof of the map/iterate example, Lemma 2.17, because, in Strachey’s (1967) wonderful phrase, the “characteristic feature of an expression is its value.” All that matters about an expression is its value. We want a proof principle that for each pair (a, b) in the candidate relation S requires us just to find values for each of a and b—rather than find their transitions—such that the values have the same outermost form (both :: for instance) and have immediate subexpressions related by S.

We begin by restricting compatible refinement to values. Let Value be the set of values, that is, closed programs given by the (Value −) rules. If S ⊆ Rel, we define \overline{S}, ⟨S⟩ and ν_{V}, all subsets of Rel, as follows.

\overline{S} =^{def} \{(u, v) ∈ Value × Value | ∅ ⊢ u Ŝ^{∘} v\}
⟨S⟩_{V} =^{def} ∼\overline{S}∼
ν_{V} =^{def} νS. ⟨S⟩_{V}

In elementwise terms, we have that ν_{V} equals the greatest binary relation S ⊆ Rel such that

a S b ⇔ ∃u, v(a ∼ u Ŝ^{∘} v ∼ b).

Intuitively (a, b) ∈ ν_{V} iff a and b are bisimilar, and they both have a value, and so do their immediate subterms, ‘all the way down’. We can prove that ν_{V} approximates bisimilarity. As a notational convenience, if R ⊆ Rel we shall write R_{∼} to mean the composition ∼R∼.

Lemma 4.2 For any S ⊆ Rel, \overline{S} ⊆ [S_{∼} ∪ Id].

Proof If a \overline{S} b we must show that whenever a ⟶^{α} a′ there is b′ such that b ⟶^{α} b′ and (a′, b′) ∈ S_{∼} ∪ Id. In fact a and b must be values satisfying ∅ ⊢ u Ŝ^{∘} v, that is, with the same outermost form and their immediate subexpressions related by S^{∘}. We consider the various kinds of values.

(Value Arith) Here both a and b are \underline{ℓ}. The only transition of a is a ⟶^{ℓ} 0, which is matched by b ⟶^{ℓ} 0 and we have (0, 0) ∈ Id.

(Value Fun) Here a is λ(x:A)e and b is λ(x:A)e′, such that e[c/x] S e′[c/x] for any c:A. Each transition of a takes the form a ⟶^{@c} a(c), which can be matched by b ⟶^{@c} b(c). We can calculate a(c) ∼ e[c/x] S e′[c/x] ∼ b(c) and so (a(c), b(c)) ∈ S_{∼}.

In the other possibilities, (Value Stm) and (Value Rec), we can argue similarly. ■

Lemma 4.3 If S ⊆ ⟨S⟩_{V}, then S_{∼} ⊆ ∼.

Proof If (a, b) ∈ S_{∼}, there must be a_{0} and b_{0} with a ∼ a_{0} S b_{0} ∼ b. If we suppose S ⊆ ⟨S⟩_{V} there must be u and v with a_{0} ∼ u \overline{S} v ∼ b_{0}. For any transition a ⟶^{α} a′, given Lemma 4.2, we can fill in the following diagram from left to right.

\begin{aligned}a & ∼ & a_{0} & ∼ & u & \overline{S} & v & ∼ & b_{0} & ∼ & b \\ a′ & \begin{matrix}α \\ ↓ \end{matrix} & ∼ & a′_{0} & \begin{matrix}α \\ ↓ \end{matrix} & ∼ & a′′ & \begin{matrix}α \\ ↓ \end{matrix} & (S_{∼} ∪ Id) & b′′ & ^{↓α} & ∼ & b′_{0} & ^{↓α} & ∼ & b′ & ^{↓α} \end{aligned}

We have (a′, b′) ∈ (S_{∼} ∪ ∼), from which (a, b) ∈ [S_{∼} ∪ ∼]. Indeed by a symmetric argument we have (a, b) ∈ ⟨S_{∼} ∪ ∼⟩. By strong co-induction we have S_{∼} ⊆ ∼ as required. ■

Proposition 4.4 ν_{V} ⊂ ∼

Proof Since ν_{V} is ⟨−⟩_{V} dense, we have ∼ν_{V} ∼ ⊆ ∼ by Lemma 4.3. In fact ν_{V} ⊆ ∼ since Id ⊆∼. The inclusion is strict because, for instance, 0 ∼ 0, although (0, 0) ∉ ν_{V} because no value is bisimilar to 0. ■

We can use ν_{V} to refine the proof of Lemma 2.17. Our original proof explicitly considered all the transitions of the programs in relation S. If we make the assumption that (f^{n}(c), (f^{n}(c)) ∈ ν_{V}, it is not hard to check that S ⊆ ⟨S ∪ ν_{V} ⟩_{V}, and hence by strong co-induction that S ⊆ ν_{V} ⊆ ∼. This proof avoids having to explicitly calculate transitions. The reason for the restriction on each f^{n} c is essentially that ν_{V} is an incomplete co-inductive characterisation of ∼.

4.3 The Map/Filter Example

The idea of matching values is a step forward but it has shortcomings. Suppose filter is the usual function that deletes the elements of a stream that fail a predicate.

  filter f nil = nil
  filter f (x::xs) = if f x then x :: filter f xs
                           else      filter f xs

For any functions f:B → Bool and g:A → B, filter ought to commute with map as follows, where o function composition.

           filter f omap g ∼ map g ofilter (f o g) (∗)

For arbitrary f and g make the following definitions.

                   e ≡ filter f (map g, −)

e′ ≡ map g (filter (f o g) −)
S = {(e[cs], e′[cs]) | cs:[A]}

Equation (∗) will follow by (Fun Ext) if we can show that S ⊆ ∼.

Lemma 4.5 Whenever e[cs] S e′[cs] and e[cs] ⇓ v in n steps, there is u with e′[cs] ⇓ u and v \overline{S′} u if S′ = S ∪ ∼.

Proof By mathematical induction on n. Suppose that e[cs] S e′[cs] and that e[cs] ⇓ v in n steps. Consider the evaluation behaviour of cs. Either (A) cs⇑, (B) cs ⇓ nil or (C) cs ⇓ c:: cs′. Case (A) contradicts our assumption e[cs] ⇓ v. In case (B) both e[cs] ⇓ nil and e′[cs] ⇓ nil so the hypothesis holds. In case (C) e[cs] and e′[cs] reduce as follows.

e[cs] ↦^{+} if f(g c) then g(c) :: e[cs′] else e[cs′]
e′[cs] ↦^{+} if f(g c) then g(c) :: e′[cs′] else e′[cs′]

Consider the evaluation behaviour of f(g(c)). Either (CA) f(g c)⇑, (CB) f(g c) ⇓ true and (CC) f(g c) ⇓ false. Again (CA) is contradictory. In case (CB) let

u ≡ g(c) :: e[cs′]
v ≡ g(c) :: e′[cs′]

and we have e[cs] ⇓ u, e′[cs] ⇓ v and v \overline{S′} u as required. In case (CC) we have

e[cs] ↦^{+} e[cs′]
e′[cs] ↦^{+} e′[cs′].

By induction hypothesis there are values u and v with e[cs′] ⇓ u, e′[cs′] ⇓ v and v \overline{S′} u. But e[cs] ⇓ u and e′[cs] ⇓ v too. ■

A symmetric argument shows that the lemma holds for S^{op} too. We can deduce that S ⊆ ⟨S ∪∼⟩_{V} ∪∼. We cannot apply strong co-induction though, because ∼ ≠ ν_{V}. But by calculating transitions we can see that S ⊆ ⟨S ∪ ∼⟩ ∪ ∼ and then (∗) does follow by strong co-induction.

Applying the matching values idea to a candidate relation such as S is problematic because not all the programs in S have a value, and furthermore, as in case (CC) not all of them immediately produce a value. Other examples also require an induction on the evaluation of a program. The next idea, matching reductions, caters for divergence in the candidate relation and in a sense incorporates the induction used in Lemma 4.5 into a co-induction principle, once and for all.

4.4 Matching Reductions

We begin with another functional, ⟨−⟩_{+}.

a ⟨S⟩_{+} b ⇔ ∃a′, b′(a ↦^{+} a′, b ↦^{+} b′ & a′ S b′)

These are both monotone maps. If S ⊆ ⟨S⟩_{+}, starting from any pair in S we can make reductions in both programs to end up back in S.

Proposition 4.6 Let ν_{+} =^{def} νS. ⟨S⟩_{+}.

(1) (a, b) ∈ ν_{+} iff a⇑ and b⇑.

(2) ν_{+} ⊂ ∼.

Proof Recall the divergence functionals D and D_{+} from Section 2.3. Consider the following three sets.

X =^{def} {a | ∃b((a, b) ∈ ν_{+})}
Y =^{def} {b | ∃a((a, b) ∈ ν_{+})}
S =^{def} {(a, b) | a ∈ νX. D_{+}(X) & b ∈ νX. D_{+}(X)}

One can easily check that X and Y are both D dense, and that S is ⟨−⟩_{+} dense. Hence by co-induction we have X ⊆ ⇑, Y ⊆ ⇑ and S ⊆ ν_{+}. Part (1) then follows. Inclusion ν_{+} ⊆ ∼ follows from (1); it is strict because of convergent programs: if a⇓ then (a, a) ∉ ν_{+} although a ∼ a. ■

The rest of this section is devoted to the proof that bisimilarity equals νS. ⟨S⟩_{V} ∪ ⟨S⟩_{+}. The proof applies to all the languages considered in this paper. It depends on bisimilarity being an equivalence and general facts from Section 2.6. The point of combining matching values and matching reductions in this equation is to simplify earlier proofs.

• Consider the map/iterate example, Lemma 2.17. We can easily check that S ⊆ ⟨S ∪ ∼⟩_{V}. So S ⊆ ∼ follows by strong co-induction with no restriction on each f^{n} c.

• Consider the map/filter example from Section 4.3. A simple modification of the argument in Lemma 4.5 shows that S ⊆ ⟨S ∪∼⟩∪⟨S⟩_{+}∪∼ but with no need for an induction on n. Hence S ⊆ ∼. In case (CC) we have that (e[cs], e′[cs]) ∈ ⟨S⟩_{+}.

Lemma 4.7 Suppose F is a monotone function on ℘(Rel). Then νX. F (X) = νX. F (X) ∪ F (F (X)).

Proof Let ν_{1} = νX. F (X) and ν_{2} = νX. F (X) ∪ F (F (X)). Since ν_{1} = F (ν_{1}) we have ν_{1} ⊆ F (ν_{1})∪F (F (ν_{1})) and therefore ν_{1} ⊆ ν_{2}. Since F (ν_{2}) ⊆ ν_{2} (as ν_{2} = F (ν_{2}) ∪ F (F (ν_{2}))) we have F (F (ν_{2})) ⊆ F (ν_{2}) by monotonicity. So ν_{2} = F (ν_{2}) ∪ F (F (ν_{2})) = F (ν_{2}) and therefore ν_{2} ⊆ ν_{1}. Hence ν_{1} = ν_{2}. ■

Lemma 4.8 Suppose F is a monotone function on ℘(Rel). If

ν_{1} =^{def} νS. F (S) ∪ ⟨S⟩_{+}
ν_{2} =^{def} νS. F (S) ∪ ⟨F (S)⟩_{+} ∪ ν_{+}

then ν_{1} = ν_{2}.

Proof We begin with the easier inclusion, ν_{2} ⊆ ν_{1}. First note that ν_{+} ⊆ ν_{1}, because ν_{+} ⊆ ⟨ν_{+}⟩_{+}. By Lemma 4.7, ν_{1} unwinds to

ν_{1} = νS. F (S) ∪ ⟨S⟩_{+} ∪ F (F (S) ∪ ⟨F (S)⟩_{+}) ∪ ⟨F (S) ∪ ⟨F (S)⟩_{+}⟩_{+}.

We shall show that ν_{2} is dense with respect to the functional on the righthand side. Starting from

ν_{2} ⊆ F (ν_{2}) ∪ ⟨F (ν_{2})⟩_{+} ∪ ν_{+}

we obtain

ν_{2} ⊆ F (ν_{2}) ∪ ⟨F (ν_{2}) ∪ ⟨F (ν_{2})⟩_{+}⟩_{+} ∪ ν_{1}

from monotonicity of ⟨−⟩_{+} and ν_{+} ⊆ ν_{1}. From this inequation it follows by strong co-induction that ν_{2} ⊆ ν_{1}. For the other direction we shall prove that

(i) S_{Ω} =^{def} {(a, b) ∈ ν_{1} | a⇑ & b⇑} ⊆ ν_{+}

(ii) S_{1} =^{def} {(a, b) ∈ ν_{1} | a⇓} ⊆ F (ν_{1}) ∪ ⟨F (ν_{1})⟩_{+}

(iii) S_{2} =^{def} {(a, b) ∈ ν_{1} | b⇓} ⊆ F (ν_{1}) ∪ ⟨F (ν_{1})⟩_{+}

and hence it will follow that

ν_{1} = S_{Ω} ∪ S_{1} ∪ S_{2} ⊆ F (ν_{1}) ∪ ⟨F (ν_{1})⟩_{+} ∪ ν_{+}

and hence by co-induction that ν_{1} ⊆ ν_{2}.

(i) If a⇑ and b⇑ then (a, b) ∈ ν_{+} by Proposition 4.6.

(ii) We prove by induction on n that

if (a, b) ∈ S_{1} and a⇓ in n steps, (a, b) ∈ F (ν_{1}) ∪ ⟨F (ν_{1})⟩_{+}.

Suppose then that (a, b) ∈ S_{1} and a⇓ in n steps. From ν_{1} = F (ν_{1}) ∪ ⟨ν_{1}⟩_{+} there are two cases to consider. If (a, b) ∈ F (ν_{1}) there is nothing more to say. Suppose, on the other hand, that (a, b) ∈ ⟨ν_{1}⟩_{+}, which is to say there are a′ and b′ with a ↦^{+} a′, b ↦^{+} b′ and (a′, b′) ∈ ν_{1}. Since a converges, (a′, b′) ∈ S_{1} as a′ must converge, and it does so in fewer steps than n. Therefore by induction hypothesis we have (a′, b′) ∈ F (ν_{1}) ∪ ⟨F (ν_{1})⟩_{+}. But then (a, b) ∈ ⟨F (ν_{1}) ∪ ⟨F (ν_{1})⟩_{+}⟩_{+} = ⟨F (ν_{1})⟩_{+} ∪ ⟨⟨F (ν_{1})⟩_{+}⟩_{+} ⊆ ⟨F (ν_{1})⟩_{+}, as required.

Finally case (iii) follows by a symmetric argument. Via the two inclusions, then, we have ν_{1} = ν_{2}. ■

Lemma 4.9 ∼ = νS. ⟨S⟩ ∪ ⟨S⟩_{V} ∪ ⟨S⟩_{+}.

Proof Let F (S) be ⟨S⟩∪⟨S⟩_{V} and ν be νS. F (S)∪⟨S⟩_{+}, that is, νS. ⟨S⟩∪ ⟨S⟩_{V} ∪ ⟨S⟩_{+}. The easy inclusion is ∼ ⊆ ν, which follows from ∼ = ⟨∼⟩. For the reverse inclusion, we shall prove

(1) ∼ = νS. F (S)

(2) ν_{∼} ⊆ F (ν_{∼}) ∪ ∼

From (2) ν_{∼} ⊆ νS. F (S) follows by strong co-induction from (1). Hence ν ⊆ ∼ follows.

(1) Let ν_{1} = νS. F (S). Inclusion ∼ ⊆ ν_{1} follows from ∼ = ⟨∼⟩. It remains to show ν_{1} ⊆ ∼. Whenever S ⊆ ⟨S⟩ ∪ ⟨S⟩_{V} we can show that S_{∼} ⊆ ∼ by a simple modification of the argument for Lemma 4.3. Hence ∼ν_{1}∼ ⊆ ∼ and indeed ν_{1} ⊆ ∼.

(2) Finally, suppose that (a, b) ∈ ν_{∼}, that is, a ∼ a_{0}νb_{0} ∼ b. We must show either that a ∼ b or (a, b) ∈ F (ν_{∼}). Since ν = νS. F (S)∪⟨F (S)⟩_{+} ∪ν_{+}, by Lemma 4.8, either (a_{0}, b_{0}) ∈ ν_{+} or there is a pair (a_{1}, b_{1}) ∈ F (ν) with a_{0} ↦^{∗} a_{1} and b_{0} ↦^{∗} b_{1}. In the first case we have a_{0} ∼ b_{0}, since ν_{+} ⊂ ∼, and so a ∼ b too. In the second case, pair (a_{1}, b_{1}) is either in (i) ⟨ν⟩_{V} or (ii) ⟨ν⟩. If (i), we have (a, b) ∈ ⟨ν⟩_{V} ⊆ ⟨ν_{∼}⟩_{V} ⊆ F (ν_{∼}). Otherwise, suppose (ii), and that a ⟶^{α} a′. Then we can fill in the following diagram

\begin{aligned}a & ∼ & a_{1} & ⟨ν⟩ & b_{1} & ∼ & a \\ a′ & \begin{matrix}α \\ ↓ \end{matrix} & ∼ & a′_{1} & \begin{matrix}α \\ ↓ \end{matrix} & ν & b′_{1} & ^{↓α} & ∼ & a′ & ^{↓α} \end{aligned}

and a symmetric one to show that (a, b) ∈ ⟨ν_{∼}⟩ ⊆ F (ν_{∼}). In any case, then, we have (a, b) ∈ F (ν_{∼}) ∪ ∼ as required. ■

Lemma 4.10 ∼ ⊆ ⟨∼⟩_{V} ∪ ν_{+}

Proof Suppose a ∼ b:A. Either (A) a⇑ and A is active or (B) there is a value v with a ∼ v. In case (A), b⇑ too, so (a, b) ∈ ν_{+}. In case (B), b ∼ v too, we have a ∼ v\overline{∼}v ∼ b, so (a, b) ∈ ⟨∼⟩_{V}. In any case (a, b) ∈ ⟨∼⟩_{V} ∪ ν_{+}.

■

The greatest fixpoints of both ⟨−⟩_{V} and ⟨−⟩_{+} fall short of bisimilarity, but combining them we exactly match bisimilarity.

Theorem 4.11 ∼ = νS. ⟨S⟩_{V} ∪ ⟨S⟩_{+}.

Proof Let ν be the right-hand side, νS. ⟨S⟩_{V} ∪ ⟨S⟩_{+}. From the following inclusion,

∼ ⊆ ⟨∼⟩_{V} ∪ ν_{+} Lemma 4.10
⊆ ⟨∼⟩_{V} ∪ ν  since ν_{+} ⊆ ν

it follows by strong co-induction ∼ ⊆ ν. Clearly ν ⊆ νS. ⟨S⟩ ∪ ⟨S⟩_{V} ∪ ⟨S⟩_{+}, and the latter by Lemma 4.9 equals ∼. So ∼ = ν. ■

The significance of this equation is that it is a complete co-inductive characterisation of bisimilarity (and hence contextual equivalence) without mentioning labelled transitions.

4.5 Proof of Monad Laws

Our final example is a proof of the monad laws for streams (Wadler 1992). Define the following combinators.

(++) =^{def} rec(f, xs)λ(ys)scase(xs, ys, λ(x)λ(xs′)x:: f xs′ ys)
join  =^{def} rec(f, xss)scase(xss, nil, λ(xs)λ(xss′)xs ++ fxss′)
id  =^{def} λ(x)x
unit  =^{def} λ(x)x:: nil

Strictly speaking these are families of monomorphic combinators indexed by types, but we will skate over the details of typing.

Proposition 4.12

(1) mapid ∼ id
(2) map (f o g) ∼ map f omap g
(3) map f ounit ∼ unito f
(4) map f ojoin ∼ joinomap (map f)
(5) joinounit ∼ id
(6) joinomapunit ∼ id
(7) joinomapjoin ∼ joinojoin

Proof (3,5) Easy equational reasoning. (1, 2, 6) For these three parts it suffices by extensionality to show that each

of the following relations is contained in ∼.

S_{1} = {(mapid as, id as) | as:[A]}
S_{2} = {(map (f o g) as,  (map f omap g) as) | as:[A]}
S_{6} = {((joinomapunit) as, id as)  | as:[A]}

For each S_{i} we can easily check that S_{i} ⊆ ⟨S_{i} ∪ ∼⟩_{V} ∪ ∼, and hence by strong co-induction that S_{i} ⊆ ∼.

(4) Again by extensionality it suffices to show that S_{4} ⊆ ∼.

S_{4} = {(map f (join ass), join (map (map f) ass)) | ass:[[A]]}

Suppose that a S_{4} b. Take cases according to the operational behaviour of ass: (A) ass⇑, (B) ass ⇓ nil or (C) ass ⇓ as:: ass′. In case (A) we have a ∼ Ω ∼ b and in case (B), a ∼ nil ∼ b. In case (C) we have the following reductions.

a ↦^{+} map f (as ++join ass′)
map (map f) ass ↦^{+} map f as:: map (map f) ass′
b ↦^{+} (map f as) ++join (map (map f) ass′)

We examine the three possible behaviours of as: (CA) as⇑, (CB) as ⇓ nil or (CC) as ⇓ a_{0} :: as′. In case (CA) we have a ∼ Ω ∼ b. In case (CB) let

a′ ≡ map f (join ass′)
b′ ≡ join (map (map f) ass′)

and then we have a ↦^{+} a′ and b ↦^{+} b′ and a′ S b′, that is, a⟨S⟩_{+}b. Finally, in case (CC) let

a′ ≡ map f (join (as′ :: ass′))
b′ ≡ join (map (map f) (as′ :: ass′))

and we have the following bisimilarities.

a ∼ map f (a_{0} :: (as′ ++join ass′))
∼ (f a_{0}) :: map f (as′ ++join ass′)
∼ (f a_{0}) :: a′
b ∼ (f a_{0}) :: ((map f as′) ++join (map (map f) ass′))
∼ (f a_{0}) :: join (map f as′ :: map (map f) ass′)
∼ (f a_{0}) :: b′

Since a′ S_{4} b′ we have (a, b) ∈ ⟨S_{4} ∪ ∼⟩_{V}. In all cases, then, we have established that (a, b) ∈ ⟨S_{4} ∪ ∼⟩_{V} ∪ ⟨S_{4}⟩_{+}. Hence S_{4} ⊆ ∼ by strong co-induction.

(7) The hardest. The most obvious co-inductive proof fails. Instead we can prove that S_{7} below is a subset of ∼. First we extract the following expressions from the definitions of ++ and join respectively.

\overline{append}[as, bs] =^{def} scase(as, bs, λ(x)λ(xs)x:: (xs ++ bs))
\overline{join}[ass] =^{def} scase(ass, nil, λ(xs)λ(xss)xs ++join(xss′))

Note that as ++ bs ↦^{+} \overline{append}[as, bs] and join(ass) ↦^{+} \overline{join}[ass]. Now let

e_{L}[ass, asss] =^{def} \overline{append}[\overline{join}[ass], join (mapjoin asss)]
e_{R}[ass, asss] =^{def} \overline{join}[ass ++join asss]

and define S_{7} to be

{(e_{L}[ass, asss], e_{R}[ass, asss]) | ass:[[A]] & asss:[[[A]]]}.

Suppose that e_{L}[ass, asss] S_{7} e_{R}[ass, asss]. We shall establish the following property

(e_{L}[ass, asss], e_{R}[ass, asss]) ∈ ⟨S_{7} ∪ ∼⟩_{V} ∪ ⟨S_{7}⟩_{+} ∪ ∼ (∗).

and then S_{7} ⊆ ∼ follows from (∗) by strong co-induction. Part (7) follows easily (take ass ≡ nil). Consider then the three possible evaluation behaviours of ass: (A) ass⇑, (B) ass ⇓ nil or (C) ass ⇓ as::ass′. In case (A) we have that e_{L}[ass, asss] ∼ Ω ∼ e_{R}[ass, asss]. In case (B) we have the following reductions.

e_{L}[ass, asss] ↦^{+} join (mapjoin asss)
e_{R}[ass, asss] ↦^{+} \overline{join}[join asss]

Now consider cases of the behaviour of asss: (BA) asss⇑, (BB) asss ⇓ nil and (BC) asss ⇓ ass′::asss′. In case (BA) we have e_{L}[ass, asss] ∼ Ω ∼ e_{R}[ass, asss] and in case (BB) e_{L}[ass, asss] ∼ nil ∼ e_{R}[ass, asss]. In case (BC),

e_{L}[ass, asss] ↦^{+} \overline{join}[join ass′ :: mapjoin asss′]

                  ↦^{+} join ass′ ++join (mapjoin asss′)

↦^{+} e_{L}[ass′, asss′]
e_{R}[ass, asss] ↦^{+} \overline{join}[\overline{join}[ass′] :: asss′)]
↦^{+} \overline{join}[ass′ ++join asss′]
≡ e_{R}[ass′, asss′]

so (e_{L}[ass, asss], e_{R}[ass, asss]) ∈ ⟨S_{7}⟩_{+}.

Returning to the original case analysis, in the final case, (C), we have the following reductions.

e_{L}[ass, asss] ↦^{+} \overline{append}[as ++join ass′, join (mapjoin asss)]
e_{R}[ass, asss] ↦^{+} \overline{join}[as:: (ass′ ++join asss)]
↦^{+} as ++join (ass′ ++join asss)

There are three behaviours of as to consider: (CA) as⇑, (CB) as ⇓ nil and (CC) as ⇓ a:: as′. In case (CA) both sides diverge. In case (CB),

e_{L}[ass, asss] ↦^{+} \overline{append}[\overline{join}[ass′], join (mapjoin asss)]
e_{R}[ass, asss] ↦^{+} \overline{join} [ass′ ++join asss]

so (e_{L}[ass, asss], e_{R}[ass, asss]) ∈ ⟨S_{7}⟩_{+}. Finally, in case (CC), set a′ and b′ to be

a′ ≡ join (as′ :: ass′) ++join (mapjoin asss)
b′ ≡ join((as:: ass′) ++join asss)

and we can easily check that e_{L}[ass, asss] ∼ a_{0} :: a′, e_{R}[ass, asss] ∼ a_{0} :: b′ and a′ ∼S_{7}∼ b′, and hence that (e_{L}[ass, asss], e_{R}[ass, asss]) ∈ ⟨S_{7} ∪ ∼⟩_{V}. In all cases we have established property (∗) and hence (7) follows. ■

4.6 Bird and Wadler’s Take Lemma

We derive the Take Lemma of Bird and Wadler (1988) to illustrate how a proof principle usually derived by domain-theoretic fixpoint induction follows also from co-induction. We begin with the take function, which returns a finite approximation to an infinite list.

take 0 xs = nil
take n nil = nil
take (n+1) (x :: xs) = x :: (take n xs)

Here is the key lemma.

Lemma 4.13 Define S ⊆ Rel by aSb iff ∀n ∈ ℕ (take\underline{n + 1} a ∼ take\underline{n + 1} b).

(1) Whenever a S b and a ⇓ nil, b ⇓ nil too.

(2) Whenever aS b and a ⇓ a′::a′′ there are b′ and b′′ with b ⇓ b′::b′′, a′ ∼ b′ and a′′ S b′′.

(3) S ⊆ ⟨S ∪ ∼⟩.

Proof

(1) Using a S b and n = 0 we have take \underline{1} a ∼ take \underline{1} b. Since a ⇓ nil, we have a ∼ nil, and in fact that nil ∼ take \underline{1} b by definition of take. We know that either b ∼ Ω, b ⇓ nil or b ⇓ b′ :: b′′. The first and third possibilities would contradict nil ∼ take\underline{1} b, so it must be that

b ⇓ nil.

(2) We have

take\underline{n + 1} (a′ :: a′′) ∼ take\underline{n + 1} b.

With n = 0 we have

                          a′ :: nil ∼ take\underline{1} b

which rules out the possibilities that b ∼ Ω or b ⇓ nil, so it must be that b ⇓ b′ :: b′′. So we have

a′ :: (take\underline{n} a′′) ∼ b′ :: (take\underline{n} b′′)

for any n, and hence a′ ∼ b′ and a′′ S b′′ by (Inj Stm).

(3) As before it suffices to prove that S ⊆ ⟨S ∪ ∼⟩. Suppose that a S b. For each transition a ⟶^{α} a′ we must exhibit b′ satisfying b ⟶^{α} b′ and either a′ S b′ or a′ ∼ b′. Since a and b are streams, there are three possible actions α to consider.

(a) Action α is nil. Hence a ⇓ nil and a′ is 0. By part (1), b ⇓ nil too. Hence b ⟶^{nil} 0, and 0 ∼ 0 as required.

(b) Action α is hd. Hence a ⇓ a′:: a′′. By part (2), there are b′ and b′′ with b ⇓ b′ :: b′′, hence b ⟶^{hd} b′, and in fact a′ ∼ b′ by part (2).

(c) Action α is tl. Hence a ⇓ a′:: a′′. By part (2), there are b′ and b′′ with b ⇓ b′ :: b′′, hence b ⟶^{tl} b′′, and in fact a′′ S b′′ by part (2). ■

The Take Lemma follows from (3) by strong co-induction.

Theorem 4.14 (Take Lemma) Suppose a, b:[A]. Then a ∼ b iff ∀n ∈ ℕ (take\underline{n + 1} a ∼ take\underline{n + 1} b).

See Bird and Wadler (1988) and Sander (1992), for instance, for examples of how the Take Lemma reduces a proof of equality of infinite streams to an induction over all their finite approximations. We can use the Take Lemma to prove the map/filter example of Section 4.3 but as in Lemma 4.5 we need an induction on the length of evaluation. Co-induction based on the equation ∼ = νS. ⟨S⟩_{V} ∪ ⟨S⟩_{+} is more useful than the Take Lemma, in the sense that it avoids the induction on evaluation.

5 Variations

5.1 The Active/Passive Distinction

We distinguished between active and passive types when creating our labelled transition system for PCF plus streams. Programs of active types had to converge to a value before they would admit a transition. Programs of passive type had transitions whether or not they converged. We showed in Section 2.6 that Total(A) ⇔ A passive. But this need not be so in every labelled transition system that generates a co-inductive characterisation of contextual equivalence. Recall experimental equivalence from Section 3.4. Consider the following labelled transition system for PCF plus streams,

a:A −:A ⊢ E : B

(Trans Exper)

a ⟶^{E} E[b]

a:Bool a⇓ ; \overline{(Trans Val)} ; a ⟶^{val} 0

where an action is either an experiment, E, or val, and 0 is disjoint from the set of programs. Clearly two programs are bisimilar according to this labelled transition system iff they are experimentally equivalent. In effect every type apart from Bool is passive. So there are types which do not satisfy Total(−) that are passive.

The active/passive distinction is best seen as a device to optimise a labelled transition system for co-inductive bisimulation proofs. The generic system above would work for any operationally extensional calculus. We can view the transition rule for function types (the only passive types in PCF plus streams) as an instance of (Trans Exper). This rule is contingent only on the type of the observed program, not on whether it terminates or on the shape of its value. In contrast our rules for active types do depend on such information, and as we discussed in the case of streams, lead to simpler proofs. At least one rule must depend on termination behaviour or the shape of values. Without (Trans Val) the system above would be useless. On the other hand, if there are convergence testing contexts at all types—as in a call-by-value language—we can dispense with passive types and (Trans Exper) completely. But suppose a type A satisfies Total(A). There is a value v contextually equivalent to Ω^{A}. If our transition system distinguishes between convergent and divergent programs—by making A active, for instance—bisimilarity would fall short of contextual equivalence. Although v ≃ Ω^{A} we would have v ≁ Ω^{A}.

5.2 Convergence Testing and Call-by-Value

Our presentation of PCF plus streams was lazy in the sense that functions were call-by-name and cons, ::, did not evaluate its arguments. There are two important variations.

• Suppose we add a convergence testing operation seq such that seq(a, b) diverges if a diverges, but if a converges, seq(a, b) ↦^{+} b. Programs a and b may be of any type and seq(a, b) has the same type as b. Every type A, now satisfies Ω_{∼}^{A} ⊆ ⇑^{A}. In particular, Ω^{A→B} ≄ λ(x:A)Ω^{B}. If we make function types active—so that every type is active—and replace (Trans Fun) from Table 5 by the following rule

{v:B → A b:B \atop v ⟶^{@b} v(b)}

we can rework Section 3 to show that bisimilarity equals contextual equivalence. This is sometimes known as a ‘lazy’ variation (Riecke 1993), though implementations of call-by-name using lazy evaluation do not depend on convergence testing. The presence or absence of seq is controversial amongst lazy functional programmers: it is desirable on grounds of efficiency but its presence puts awkward side-conditions on (Fun Eta) and (Fun Ext).

• Suppose we make evaluation eager in the sense that functions are callby-value and cons evaluates its arguments.

v ::= λ(x:A)e | rec(f, x)e | nil | (v :: v)
(λ(x:A)e)(v) ↦ e[v/x]
(rec(f, x)e)(v) ↦ e[rec(f, x)e, v/f, x]

                    scase(nil, b, c) ↦ b

scase(u:: v, b, c) ↦ c(u)(v)
E ::= −(a) | v(−) | scase(−, a, a) | (−:: a) | (v :: −)

Arithmetic is unchanged. If we make all types active, then the following rules

{v:B → A u:B \atop v ⟶^{@u} v(u)}

nil ⟶^{nil} 0 u:: v ⟶^{hd} u u:: v ⟶^{tl} v

together with (Trans Red) and the rules for literals from Table 5 lead to a definition of bisimilarity that equals contextual equivalence. Variables only stand for values. We must modify the definition of Γ-closure to only substitute values for variables.

Γ ⊢ e_{1} : A
\overline{(Exp Inl)}

Γ ⊢ inl[A + B](e_{1}) : A + B

Γ ⊢ e_{2} : B
\overline{(Exp Inr)}
Γ ⊢ inr[A + B](e_{2}) : A + B
Γ ⊢ e_{0} : A + B  Γ, x_{1}:A ⊢ e_{1} : C  Γ, x_{2}:B ⊢ e_{2} : C
\overline{(Exp Case)}
Γ ⊢ case e_{0} ofinl(x_{1}) ⇒ e_{1} orinr(x_{2}) ⇒ e_{2} : C

Lazy Dynamics

v ::= inl(a) | inr(a)  (Value Sum)
(caseinl(a) ofinl(x_{1}) ⇒ e_{1} orinr(x_{2}) ⇒ e_{2}) ↦ e_{1}[a/x_{1}] (Red Inl)
(caseinr(a) ofinl(x_{1}) ⇒ e_{1} orinr(x_{2}) ⇒ e_{2}) ↦ e_{2}[a/x_{2}] (Red Inr)
E ::= case − ofinl(x_{1}) ⇒ e_{1} orinr(x_{2}) ⇒ e_{2}  (Exper Sum)

Active Observations

α ::= inl | inr (Act Sum)
inl(a) ⟶^{inl} a (Trans Inl)
inr(a) ⟶^{inr} a (Trans Inr)

Table 8: Δ_{+}: sums

5.3 FPC: Sums, Pairs, Recursive Types

We have presented a theory of bisimilarity in detail for PCF plus streams. All the results extend routinely to the usual first-order extensions of PCF. Tables 8, 9 and 10 show the rules for sums, Δ_{+}, pairs, Δ_{×}, and recursive types Δ_{μ}. The obvious rules of compatible refinement, ˆ−, are omitted. We let X range over a countable set of type variables. The new types are given by

A ::= X | rec(X)A | A + A | A × A.

Recursive types and pairs are passive; sums are active. The language

Δ_{→} ∪ Δ_{+} ∪ Δ_{×} ∪ Δ_{μ}

corresponds to the lazy forms of Gunter’s (1992) FPC and Winskel’s (1993) language of recursive types. As discussed in these textbooks, arithmetic, Δ_{A},

Statics

Γ ⊢ e_{1} : A Γ ⊢ e_{2} : B

\overline{(Exp Pair)}

Γ ⊢ (e_{1}, e_{2}) : A × B

Γ ⊢ e: A × B

\overline{(Exp Fst)}

Γ ⊢ fst(e) : A

Γ ⊢ e: A × B
\overline{(Exp Snd)}
Γ ⊢ snd(e) : B

Lazy Dynamics

v ::= (a, b)  (Value Pair)
fst((a, b)) ↦ a  (Red Fst)
snd((a, b)) ↦ b  (Red Snd)
E ::= fst(−) | snd(−) (Exper Pair)

Passive Observations

α ::= fst | snd  (Act Pair)
a ⟶^{fst}fst(a) if a:A × B (Trans Fst)
a ⟶^{snd}snd(a) if a:A × B (Trans Snd)

Table 9: Δ_{×}: pairs

Statics

Γ ⊢ e: A[μ/X] μ ≡ rec(X)A

\overline{(Exp Intro)}

Γ ⊢ intro[μ](e) : μ Γ ⊢ e: μ μ ≡ rec(X)A

\overline{(Exp Elim)}

Γ ⊢ elim[μ](e) : A[μ/X]

Lazy Dynamics

v ::= intro(a)  (Value Rec)
elim(intro(a)) ↦ a (Red Elim)
E ::= elim(−)  (Exper Rec)

Passive Observations

α ::= elim  (Act Rec)
a ⟶^{elim}elim[rec(X)A](a) if a:rec(X)A (Trans Elim)

Table 10: Δ_{μ}: recursive types recursive functions, Δ_{μ→}, and streams, Δ_{[−]}, can all be encoded. As with PCF plus streams we have Total(A) ⇔ A passive. We can prove the following eta laws by co-inductive arguments similar to those in Proposition 2.21.

(fst(a), snd(a)) ∼ a if a:A → B
(intro(elim(a))) ∼ a if a:rec(X)A

Call-by-name plus convergence testing and call-by-value variants exist for FPC also. We omit the details. There is one subtlety. As Gunter (1992, p238) shows, in call-by-value FPC there are no values of the recursive type rec(X)X. (In our form of call-by-name FPC, there are, because intro(−) is not an experiment.) In fact there are many such types with no values. Hence to avoid equating convergent and divergent functions at any type A → B where there are no values of type A, we introduce the following variant of (Trans Val) at (all) function types.

{v:A → B \atop v ⟶^{val} 0}

5.4 Matching Value Contexts

Consider the following encoding of infinite streams in (lazy) FPC.

Stm(X) =^{def} rec(Y)(X × Y)
cons(a, b) =^{def} intro[Stm(X)]((a, b))

Co-inductive proofs similar to those developed in Section 4 work well with this encoding. But we need to generalise the idea of matching values (via ⟨−⟩_{V}) to allow matching of value contexts.

H(S) =^{def} μR. S ∪ \overline{R}
⟨S⟩_{V ∗} =^{def} ⟨H(S)⟩_{V}

These are all monotone functions. Let ν_{V ∗} be νS. ⟨S⟩_{V ∗}. Roughly speaking, unwinding the inner inductive definition permits arbitrary nesting of value constructors. To justify this generalisation, suppose that S is {(a, a′), (b, b′)}. Then (cons(a, b), cons(a′, b′)) ∉ ⟨S⟩_{V} because cons is encoded by two value constructors, but we do have (cons(a, b), cons(a′, b′)) ∈ ⟨S⟩_{V ∗}. We need the next few lemmas to show that ν_{V} = ν_{V ∗}.

Lemma 5.1 For any S, S ⊆ H(S). Proof H(S) = μR. S ∪ \overline{R} = S ∪ \overline{H(S)}. ■ Lemma 5.2 H(ν_{V ∗}) ⊆ ν_{V ∗} Proof Since H(ν_{V ∗}) is the least set closed under R ↦ ν_{V ∗} ∪ \overline{R}, H(ν_{V ∗}) ⊆ ν_{V ∗} will follow by induction if ν_{V ∗} ∪ \overline{ν_{V ∗}} ⊆ ν_{V ∗}. It is enough to show that \overline{ν_{V ∗}} ⊆ ν_{V ∗}.

\overline{ν_{V ∗}} ⊆ ∼\overline{ν_{V ∗}}∼  because Id reflexive
= ⟨ν_{V ∗}⟩_{V}
⊆ ⟨H(ν_{V ∗})⟩_{V} because ν_{V ∗} ⊆ H(ν_{V ∗}) and ⟨−⟩_{V} monotone
= ν_{V ∗}

Hence H(ν_{V ∗}) ⊆ ν_{V ∗} by induction. ■ Proposition 5.3 ν_{V} = ν_{V ∗}. Proof We prove inclusions in both directions by co-induction. First, ν_{V} ⊆ ν_{V ∗} follows from ν_{V} ⊆ ⟨H(ν_{V})⟩_{V}, which holds because ν_{V} ⊆ ⟨ν_{V} ⟩_{V} ⊆ ⟨H(ν_{V})⟩_{V}, using Lemma 5.1. For the reverse inclusion, we have

ν_{V ∗} = ∼\overline{H(ν_{V ∗})}∼
⊆ ∼\overline{ν_{V ∗}}∼  by Lemma 5.2
= ⟨ν_{V ∗}⟩_{V}

and hence ν_{V ∗} ⊆ ν_{V} by co-induction. ■

We can generalise Theorem 4.11 as follows. The proof is a routine modification of the original proof. Theorem 5.4 ∼ = νS. ⟨S⟩_{V ∗} ∪ ⟨S⟩_{+}. This theorem is useful for co-inductive proofs about Stm types and other encodings in FPC. See Gordon (1995a) for an application.

6 Summary and Related Work

We have developed a ‘CCS-view of lambda-calculus.’ Using a novel labelled transition system we replayed the definition of bisimilarity from CCS and proved that it equals contextual equivalence. Hence we answered Turner’s (1990, Preface) concern that in a typed, call-by-name setting, Abramsky’s applicative bisimulation makes more distinctions than observable by well-typed contexts. We developed refinements of the bisimulation proof technique that take advantage of the determinacy of our language, and demonstrated their utility on a series of stream-processing examples. We generalised Milner’s context lemma to yield another co-inductive form of contextual equivalence, but offered evidence that it yields a weaker co-induction principle than bisimilarity.

Although our particular formulation is new, bisimilarity for functional languages is not. Often it is usually known as ‘applicative bisimulation’ and is based on a natural semantics style evaluation relation. The earliest reference I can find is to Abramsky’s unpublished 1984 work on Martin-Löf’s type theory, which eventually led to his study of lazy lambda-calculus^{2} (Abramsky and Ong 1993). Other work includes papers by Howe (1989), Smith (1991), Sands (1992, 1995), Ong (1993), Pitts and Stark (1993), Rees (1994), Ritter and Pitts (1995), Crole and Gordon (1995) and my book (1994). The main novelty of the present work is our use of a labelled transition system to match contextual equivalence exactly in a typed setting, and our refinements of bisimulation in Section 4. It would be possible to rephrase our construction of ∼ directly in terms of ⇓, without using a labelled transition system, and still match contextual equivalence. We prefer the construction based on labels because it admits convenient proofs by diagram chasing, and emphasises the connection to CCS.

Bernstein and Stark (1995) also use a labelled transition system for a functional language. Their system is more complex than the one of this paper in that they represent substitutions explicitly using labels. Their objective was to study debugging rather than to model contextual equivalence. In fact their form of bisimilarity is finer grained than contextual equivalence because individual reduction steps are observable. Mason, Smith, and Talcott (1994) also advocate operational methods for functional programming. Their work is based on a form of the context lemma, indeed they derive a form of fixpoint induction, but they do not emphasise co-induction. Felleisen and Friedman (1989) also develop syntactic approaches to reasoning about programs.

2The earliest presentation of lazy lambda-calculus appears to be Abramsky’s thesis (1987, Chapter 6), in which he explains that the “main results of Chapter 6 were obtained in the setting of Martin-Löf’s Domain Interpretation of his Type Theory, during and shortly after a visit to Chalmers in March 1984.”

Domain theory is the classical foundation of languages such as FPC, and indeed Pitts (1994a) shows how to derive a co-induction principle for recursively defined domains. In contrast our approach is based on the operational definition of our language. Working directly with program texts rather than with abstract denotations has some modest rewards. For instance the idea of matching reductions, which formalises a simple intensional intuition, has no counterpart in Pitts’ work. But there are certain properties, such as showing that a Y combinator in PCF returns the least fixpoint of its argument, that are more simply proved from a denotational than an operational semantics. The purpose of these notes is to show that much can be done from elementary operational foundations. No doubt more operational results will follow. Though purely operational methods are enough for many purposes, an adequate domain-theoretic denotational semantics is useful too. See Pitts’ recent notes (1994b), for instance, for proofs of operational properties via denotational semantics.

Sangiorgi (1994) presents a refinement of co-induction, based on the notion of ‘respectful functionals’ on relations. Hopefully connections can be made with the present work, though ⟨−⟩_{V ∗} and ⟨−⟩_{+} of this paper do not directly take the form of respectful functionals.

Acknowledgements

The idea of defining bisimilarity on a deterministic functional language via a labelled transition system arose in joint work with Roy Crole (Crole and Gordon 1995). I am grateful for many conversations with colleagues at Cambridge and Chalmers, and for the opportunities to develop this material in lectures at Glasgow and Aarhus. I thank Glynn Winskel for the invitation to lecture at Aarhus, and Simon Peyton Jones and Phil Wadler for the invitation to Glasgow. Martin Coen suggested the map/filter example. John Hatcliff and Søren Bøgh Lassen pointed out errors in earlier versions of these notes. I began this work while a member of the Programming Methodology Group at Chalmers University in Gothenburg. At Cambridge I have been supported by the TYPES BRA and a University Research Fellowship from the Royal Society. Paul Taylor’s prooftree and commutative diagrams packages helped typeset these notes.

References

Abramsky, S. (1987, October 5). Domain Theory and the Logic of Observable Properties. Ph. D. thesis, Queen Mary College, University of London.

Abramsky, S. and L. Ong (1993). Full abstraction in the lazy lambda calculus. Information and Computation 105, 159–267. Available as Technical Report 259, University of Cambridge Computer Laboratory.

Aczel, P. (1977). An introduction to inductive definitions. In J. Barwise (Ed.), Handbook of Mathematical Logic, pp. 739–782. North-Holland.

Bernstein, K. L. and E. W. Stark (1995). Operational semantics of a focusing debugger. In Eleventh Annual Conference on Mathematical Foundations of Programming Semantics, Volume 1 of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers B.V.

Berry, G. (1981). Some syntactic and categorical constructions of lambda-

calculus models. Technical Report 80, INRIA. Bird, R. and P. Wadler (1988). Introduction to Functional Program-

ming. Prentice-Hall International. Bloom, B. (1988). Can LCF be topped? Flat lattice models of typed

lambda calculus. In Proceedings of the 3rd IEEE Symposium on Logic in Computer Science, pp. 282–295. IEEE Computer Society Press.

Camilleri, J. and T. Melham (1992, August). Reasoning with inductively defined relations in the HOL theorem prover. Technical Report 265, University of Cambridge Computer Laboratory.

Coquand, T. (1993). Infinite objects in type theory. In Types of Proofs and Programs, Volume 806 of Lecture Notes in Computer Science, pp. 62–78. Springer-Verlag.

Cousot, P. and R. Cousot (1979). Constructive versions of Tarski’s fixed

point theorems. Pacific Journal of Mathematics 82(1), 43–57. Crole, R. L. and A. D. Gordon (1995, June). A sound metalogical seman-

tics for input/output effects. In Computer Science Logic’94, Kazimierz, Poland, September 1994, Volume 933 of Lecture Notes in Computer Science. Springer-Verlag.

Davey, B. A. and H. A. Priestley (1990). Introduction to Lattices and Order. Cambridge University Press.

Felleisen, M. and D. Friedman (1986). Control operators, the SECDmachine, and the λ-calculus. In Formal Description of Programming Concepts III, pp. 193–217. North-Holland.

Felleisen, M. and D. P. Friedman (1989). A syntactic theory of sequential state. Theoretical Computer Science 69, 243–287.

Girard, J.-Y., P. Taylor, and Y. Lafont (1989). Proofs and Types. Cambridge University Press.

Gordon, A. D. (1994). Functional Programming and Input/Output. Cambridge University Press.

Gordon, A. D. (1995a). Bisimilarity as a theory of functional programming. In Eleventh Annual Conference on Mathematical Foundations of Programming Semantics, Volume 1 of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers B.V.

Gordon, A. D. (1995b). A tutorial on co-induction and functional programming. In Functional Programming, Glasgow 1994, Workshops in Computing, pp. 78–95. Springer-Verlag.

Gunter, C. A. (1992). Semantics of Programming Languages: Structures and Techniques. MIT Press, Cambridge, Mass.

Howe, D. J. (1989). Equality in lazy computation systems. In Proceedings of the 4th IEEE Symposium on Logic in Computer Science, pp. 198–203.

Hughes, J. (1989, April). Why functional programming matters. The Computer Journal 32(2), 98–107.

Hughes, J. and A. Moran (1995, June). Making choices lazily. In FPCA’95, La Jolla. ACM Press.

Mason, I. A., S. F. Smith, and C. L. Talcott (1994). From operational semantics to domain theory. Submitted for publication.

Meyer, A. R. and S. S. Cosmadakis (1988, July). Semantical paradigms: Notes for an invited lecture. In Proceedings of the 3rd IEEE Symposium on Logic in Computer Science, pp. 236–253.

Milner, R. (1977). Fully abstract models of typed lambda-calculi. Theoretical Computer Science 4, 1–23.

Milner, R. (1989). Communication and Concurrency. Prentice-Hall International.

Milner, R. and M. Tofte (1991). Co-induction in relational semantics. Theoretical Computer Science 87, 209–220.

Morris, J. H. (1968, December). Lambda-Calculus Models of Programming Languages. Ph. D. thesis, MIT.

Ong, C.-H. L. (1993, June). Non-determinism in a functional setting (extended abstract). In Proceedings of the 8th IEEE Symposium on Logic in Computer Science, pp. 275–286.

Ong, C.-H. L. (1994, January). Correspondence between operational and denotational semantics: The full abstraction problem for PCF. Submitted to Handbook of Logic in Computer Science Volume 3, OUP 1994.

Park, D. (1981, March). Concurrency and automata on infinite sequences. In P. Deussen (Ed.), Theoretical Computer Science: 5th GI-Conference, Karlsruhe, Volume 104 of Lecture Notes in Computer Science, pp. 167–183. Springer-Verlag.

Paulson, L. C. (1993). Co-induction and co-recursion in higher-order logic. Technical Report 304, University of Cambridge Computer Laboratory.

Pitts, A. and I. Stark (1993, June). On the observable properties of higher order functions that dynamically create local names (preliminary report). In SIPL’93: ACM SIGPLAN Workshop on State in Programming Languages, pp. 31–45.

Pitts, A. M. (1994a). A co-induction principle for recursively defined domains. Theoretical Computer Science 124, 195–219.

Pitts, A. M. (1994b, December). Some notes on inductive and co-inductive techniques in the semantics of functional programs. BRICS Notes Series NS–94–5, BRICS, Aarhus University.

Plotkin, G. D. (1977). LCF considered as a programming language. Theoretical Computer Science 5, 223–255.

Rees, G. (1994, April). Observational equivalence for a polymorphic lambda calculus. University of Cambridge Computer Laboratory. Available from the author.

Riecke, J. G. (1993). Fully abstract translations between functional languages. Mathematical Structures in Computer Science 3, 387– 415.

Ritter, E. and A. M. Pitts (1995). A fully abstract translation between a λ-calculus with reference types and Standard ML. In Proceedings TLCA’95, Edinburgh.

Sander, H. (1992). A Logic of Functional Programs with an Application to Concurrency. Ph. D. thesis, Programming Methodology Group, Chalmers University of Technology and University of Gothenburg.

Sands, D. (1992). Operational theories of improvement in functional languages (extended abstract). In Functional Programming, Glasgow 1991, Workshops in Computing, pp. 298–311. Springer-Verlag.

Sands, D. (1995, January). Total correctness by local improvement in program transformation. In Proceedings of the 22nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM Press.

Sangiorgi, D. (1994, August). On the bisimulation proof method. Technical Report ECS–LFCS–94–299, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh.

Scott, D. S. (1993). A type-theoretical alternative to ISWIM, CUCH, OWHY. Theoretical Computer Science 121, 411–440. Annotated reprint of Scott’s 1969 manuscript.

Smith, S. F. (1991). From operational to denotational semantics. In MFPS VII, Pittsburgh, Volume 598 of Lecture Notes in Computer Science, pp. 54–76. Springer-Verlag.

Strachey, C. (1967, August). Fundamental concepts in programming languages. Unpublished lectures given at the International Summer School in Computer Programming, Copenhagen.

Turner, D. (Ed.) (1990). Research Topics in Functional Programming. Addison-Wesley.

Wadler, P. (1992). Comprehending monads. Mathematical Structures in Computer Science 2, 461–493.

Winskel, G. (1993). The Formal Semantics of Programming Languages. MIT Press, Cambridge, Mass.

Recent Publications in the BRICS Notes Series

NS-95-3 Andrew D. Gordon. Bisimilarity as a Theory of Functional Programming. Mini-Course. July 1995. iv+59 pp.

NS-95-2 Uffe H. Engberg, Kim G. Larsen, and Arne Skou, editors. Proceedings of the Workshop on Tools and Algorithms for The Construction and Analysis of Systems, TACAS (Aarhus, Denmark, 19�20 May, 1995), May 1995. vi+334 pp.

NS-95-1 Igor Walukiewicz. Notes on the Propositional μ-calculus: Completeness and Related Results. February 1995. 54 pp.

NS-94-6 Uffe H. Engberg, Kim G. Larsen, and Peter D. Mosses, editors. Proceedings of the 6th Nordic Workshop on Programming Theory (Aarhus, Denmark, 17�19 October, 1994), December 1994. v+483pp.

NS-94-5 Andrew M. Pitts. Some Notes on Inductive and Co-Inductive Techniques in the Semantics of Functional Programs, DRAFT VERSION. December 1994. vi+135 pp.

NS-94-4 Peter D. Mosses, editor. Abstracts of the 6th Nordic Workshop on PROGRAMMING THEORY (Aarhus, Denmark, 17�19 October, 1994), October 1994. v+52 pp.

NS-94-3 Sven Skyum, editor. Complexity Theory: Present and Future (Aarhus, Denmark, 15�18 August, 1994), September 1994. v+213 pp.

NS-94-2 David Basin. Induction Based on Rippling and Proof Planning. Mini-Course. August 1994. 62 pp.

NS-94-1 Peter D. Mosses, editor. Proc. 1st International Workshop on Action Semantics (Edinburgh, 14 April, 1994), May 1994. 145 pp.