A Coinduction Principle for Recursive Data Types Based on Bisimulation

Marcelo P. Fiore^{∗} Department of Computer Science Laboratory for Foundations of Computer Science University of Edinburgh, The King’s Buildings Edinburgh EH9 3JZ, Scotland

                      <mf@dcs.ed.ac.uk>

Synopsis

The concept of bisimulation from concurrency theory [Par81, Mil89] is used to reason about recursively defined data types. From two strong-extensionality theorems stating that the equality (resp. inequality) relation is maximal among all bisimulations, a proof principle for the final coalgebra of an endofunctor on a category of data types (resp. domains) is obtained. As an application of the theory developed, an internal full abstraction result (in the sense of [AO93]) for the canonical model of the untyped call-by-value λ-calculus is proved.

Also, the operational notion of bisimulation and the denotational notion of final semantics are related by means of conditions under which both coincide.

Introduction

This paper provides foundations for a reasoning principle (coinduction) for establishing the equality of potentially infinite elements of self-referencing (or circular) data types. As it is well-known, such data types not only form the core of the denotational approach to the semantics of programming languages [SS71], but also arise explicitly as recursive data types in functional programming languages like Standard ML [MTH90] or Haskell [HPJW92]. In the latter context, the coinduction principle provides a powerful technique for establishing the equality of programs with values in recursive data types (see examples herein and in [Pit94]).

Our analysis is exclusively denotational in that the proof principle is derived from the characterising property of the mathematical interpretation (as final coalgebras) of the recursive data types. To do this we borrow the notion of bisimulation from concurrency [Par80, Par81, Mil89] and apply it to data types.

∗Research partially supported by Fundación Antorchas and The British Council grant ARG 2281/14/6.

In concurrency theory, the concept of bisimulation (in its various forms) plays two main roles:

1. it provides an appropriate notion of equivalence between processes, and

2. it induces a proof method (coinduction) due to Park which reads: “to prove two processes observationally equivalent, show that they are bisimilar”.

In the theory of data types, we will see that bisimulation is useful for proving two elements of a recursive data type equal. Let us think of a bisimulation on a recursive data type as relating observationally equivalent elements of that type. As such relations, bisimulations have enough closure properties to guarantee that related elements are equal. Thus, the following coinduction principle is intuitively valid:

If R is a bisimulation on the recursive data type U, and u and u′ are elements of U for which u R u′, then u = u′.

We illustrate the previous discussion and the applicability of the coinduction principle with an example. The Haskell data type IntStream of integer streams (i.e. infinite lists of elements of the built-in type Int of integers) with constructor Cons,

     data IntStream = Cons Int IntStream,

and selectors

     headS ::  IntStream -> Int
     headS (Cons h t) = h
     tailS ::  IntStream -> IntStream
     tailS (Cons h t) = t

can be given a denotational semantics using the final coalgebra of the endofunctor ℤ × : Set → Set where ℤ is the set of integers, × is the cartesian product functor, and Set is the category of small sets and functions. By this we mean that the interpretations of IntStream, headS and tailS, say ℤ^{ω}, h and t, are characterised by the following universal property: for every set T equipped with a map τ : T → ℤ × T, there exists a unique map [[ ]] : T → ℤ^{ω} such that

ℤ^{ω} ⟨h, t⟩ ℤ × ℤ^{ω} [[ ]]  id × [[ ]] ℤ × T T τ

commutes (i.e. such that ⟨h, t⟩∘[[ ]] = (id×[[ ]])∘τ). We henceforth call any τ : T → ℤ×T a structure map as it endows T with a stream-like structure with a head-like selector π_{1} ∘ τ : T → ℤ and a tail-like selector π_{2} ∘ τ : T → T that can be used to successively read-off integers from any element of T; the canonical way to read-off a stream of integers from s ∈ T is given by [[s]] ∈ IntStream. For example, consider T = ℕ (the set of natural numbers) with structure map τ : ℕ → ℤ × ℕ given by τ(n) =^{def} (f(n), g(n)) where f : ℕ → ℤ and g : ℕ → ℕ; then, for n ∈ ℕ, [[n]] ∈ IntStream is the stream f(n), f(g(n)), …, f(g^{k}(n)), . . ..

The universal property of streams provides a canonical interpretation (final semantics, see [RT93]) for certain operations on streams. For example, consider the operation

     jump ::  Int -> Int -> IntStream
     -- jump n m counts by m's from n
     -- e.g. jump 2 3 = 2, 5, 8, 11, ...
     jump n m = Cons n (jump (n+m) m)

The set of terms T = {jump n m | n, m ∈ ℤ} can be given a structure map τ : T → ℤ × T by orienting the defining equation for jump from left to right. That is, setting τ(jump n m) = (n, jump (n + m) m). Then, by the above universal property, it follows that there exists a unique interpretation [[ ]] : T → ℤ^{ω} such that for every n, m ∈ ℤ,

h [[jump n m]] = n,

and

t [[jump n m]] = [[jump (n + m) m]].

Hence, jump n m denotes the stream n, n + m, n + 2m, …, n + km, . . ..

Now consider the perfect (or alternate) shuffle [HU79] of two streams

     shuffle ::  IntStream -> IntStream -> IntStream
     shuffle s1 s2 = Cons (headS s1) (shuffle s2 (tailS s1))

and the values nat = jump 0 1, even = jump 0 2, and odd = jump 1 2. Intuitively, nat = shuffleevenodd. But, how do we prove it?

For comparison we offer proofs by induction and coinduction (identifying programs with their denotations):

1. Inductive proof.

By induction on ℕ one can prove the following two lemmas:

       • For n ∈ ℕ, tailS^{n} nat = jump n 1.
       • For n ∈ ℕ, tailS^{n} (shuffleevenodd) = shuffle (jump n 2) (jump (n + 1) 2).

from which it follows that, for n ∈ ℕ,

        headS (tailS^{n} nat) = headS (tailS^{n} (shuffleevenodd)).

Appealing to the following extensionality principle

(η) [∀ n ∈ ℕ. headS ( tailS ^{n}s) = headS ( tailS ^{n}s′)] ⇒ s = s′

we are done.

2. Coinductive proof.

A bisimulation on ℤ^{ω} is a relation R ⊆ ℤ^{ω} × ℤ^{ω} for which

s R s′ ⇒ [ headS (s) = headS (s′)] ∧ [ tailS (s) R tailS (s′)].

By the coinduction principle, we need to find a bisimulation relating nat and

shuffleevenodd.

We show that

R = {( jump k 1 , shuffle (jump k 2) (jump (k + 1) 2) ) | k ∈ ℕ}

is a bisimulation.

Let k ∈ ℕ. First observe that,

    headS (jump k 1) = k = headS (shuffle (jump k 2) (jump (k + 1) 2)).

Second,

      tailS (jump k 1) R tailS (shuffle (jump k 2) (jump (k + 1) 2))

because

                   tailS (jump k 1) = jump (k + 1) 1

and

       tailS (shuffle (jump k 2) (jump (k + 1) 2))

               = shuffle (jump (k + 1) 2) (tailS (jump k 2))
               = shuffle (jump (k + 1) 2) (jump (k + 2) 2).

Hence we are done.

The above inductive proof does not only involve more calculations than the coinductive one but, more fundamentally, appeals to the extensionality principle (η). However, how is extensionality justified? One possibility, is to represent ℤ^{ω} as ℕ ⇒ ℤ (the set of functions from ℕ to ℤ) with structure map given by h(s) = s(0) and t(s) = λn ∈ ℕ. s(n + 1), and invoke extensionality for them. Another justification, without committing the interpretation of IntStream to any particular representation, follows from the coinduction principle: assuming the antecedent of (η), the relation

{( tailS ^{n}(s), tailS ^{n}(s′)) | n ∈ ℕ}

is a bisimulation (as the reader should check) and therefore s = s′.

Thus, for some data types coinduction seems to be a more appealing proof principle than induction. This is even more noticeable when reasoning about infinite trees, where the extensionality principle is not as neat as the one for streams.

Further applications of coinduction in computer science can be found in relational semantics [MT88].

To model recursive data types we adopt a non-standard approach recently revived in the work of Peter Freyd [Fre91, Fre92]. The meaning of a recursive data type will be a final coalgebra. We recall the basic definitions. Let C be a category (which we think of as the universe of denotations for the data types) and let F be an endofunctor on it (which we think of as the denotation of a data type constructor with a free type variable). An F -coalgebra (or simply, coalgebra when F is clear from the context) is a pair (T, τ) consisting of an object T ∈ | C | together with a structure map τ : T → F T in C; a coalgebra homomorphism h : (T, τ) → (U, μ) is a morphism h : T → U such that

h  F h U  F U μ T  F T τ

commutes. Moreover, a coalgebra (U, μ) is said to be final if for every coalgebra (T, τ) there exists a unique homomorphism (T, τ) → (U, μ); i.e. if it is terminal in the category of coalgebras and homomorphims.

Observe again that, in this view, IntStream has been interpreted as the final coalgebra for the endofunctor ℤ × on Set. Other examples of data types naturally arising as coalgebras can be found in [AM82].

It has been customary to interpret recursive types as initial algebras (the notion dual to that of final coalgebra). We remark that in certain categories of domains this traditional view and the viewpoint adopted here coincide for initial algebras and final coalgebras are canonically isomorphic (see e.g. [Fre90, Smy91, Fre92, FP92, Fio94]).

The mysterious definition of bisimulation in our example is an instance of an abstract notion of bisimulation on a coalgebra (taken from [AM89]) motivated by concurrency theory. This has two important methodological consequences.

1. We are able to provide bisimulations for recursive data types by characterising the abstract notion for concrete examples; this is done for (finite and/or infinite) trees in Section 1, and for natural numbers, Cantor space and languages in Section 4.

2. We are able to test whether a relation satisfying certain closure properties can be regarded as a bisimulation; this is exemplified in the proof of the internal full abstraction result in Section 8.

A central result of the paper (Principle 6.9) is an abstract coinduction principle (along the lines of the one presented above) for proving that one element of a recursively defined domain approximates another. We begin in Section 1 presenting our theory in the light of an example. This section aims at a general audience and is mainly intended to serve as a guide for the subsequent abstract development. Sections 2–4 assume some familiarity with basic category theory (as, for example, in [Pie91, LS94]). In Section 2 an abstract definition of bisimulation is introduced. Examples of bisimulation are presented by characterising the abstract notion for various data type constructors. Section 3 concentrates on final semantics (i.e. the interpretation induced by the unique homomorphism into the final coalgebra) and analyses its relation with bisimulation. In Section 4 we state the strong-extensionality theorem from which the proof principle is derived. Sections 5–7 rework the theory to adapt it to recursive domain equations; generalising the previous treatment to the setting of order-enriched categories. In particular, ordered categorical bisimulations are defined and an order strong-extensionality theorem for them is proved. In Section 8 we apply the theory to obtain an internal full abstraction result for the canonical model of the untyped call-by-value λ-calculus. This section is technically involved; in particular the technique used to solve recursive type equations of mixed-variance functors, namely via algebraic compactness, is merely sketched (for a thorough treatment consult [Fio94, Chapters 6 and 7]). Finally, in Section 9 we indicate plans for future work.

There are some relationships between this and the work of [RT93] and [Pit94, Pit93]. In [RT93], Rutten and Turi study final semantics and strong extensionality for the cat-

egories of non-well-founded sets, complete metric spaces and ω-complete pointed partial orders (cppos). In the case of cppos, they define ordered bisimulations and prove an order strong-extensionality theorem for them. Our treatment generalises theirs in two respects: first, we work with order-enriched categories (though we remark that their approach could easily be accommodated in this setting); second, as Rutten pointed out, every ordered bisimulation in the sense of [RT93] is an ordered categorical bisimulation in our sense (Definition 5.1) whilst the converse does not hold (Example 5.4 gives a counterexample).

In [Pit94], Pitts considered domains recursively defined using the cartesian product, disjoint union, partial function space, and convex powerdomain constructors; introduced a notion of simulation over these domains; and used it to characterise their approximation order. In this way he provided a coinductive proof principle for proving that an element of these recursively defined domains approximates another; viz. by exhibiting a simulation relating the two elements. Later, in [Pit93], he generalised the previous result by establishing a mixed induction/coinduction property of relations on a recursive domain. This he achieved by working with a category of domains equipped with a relational structure (a general framework for relations on domains) and by drawing upon the simultaneous initiality/finality property of recursive domains. In this context the notion of (bi)simulation is induced by an extension of the data type endofunctor to the relational structure, which is subject to conditions but is not prescribed by the data type. Our approach differs from his in a couple of points. First, we do not just concentrate on categories of domains but rather study the coinduction principle for recursive data types in arbitrary categories (to encompass domains we develop an order-enriched theory). Second, as we follow [AM89], we consider bisimulations on recursive data types as relations (within the category of data types) with closure properties solely determined by the action of the data type constructor.

Recently, in [HJ95], Hermida and Jacobs have provided an abstract analysis of induction and coinduction in the spirit of categorical logic. Roughly, in a rich setting given by a category of data types equipped with a category of predicates/relations over it (i.e. a fibration with structure) they express induction/coinduction principles categorically as preservation of initial-algebras/final-coalgebras. This work has unified aspects of our approach and that of [Pit93] in that the action of the type constructors on predicates/relations is determined by the endofunctor defining the data type (as we do here), whereas their setting of predicates/relations in a fibration refines Pitts’ relational structures.

1 A coinduction principle based on bisimulation: an example

An instance of our main theorem is presented in the view of an example. For this purpose we consider (one-sorted) signatures. A signature Ω is an ℕ-indexed set ⟨Ω_{n}⟩_{n∈ℕ} of (disjoint) operator symbols where the intended meaning of o ∈ Ω_{n} is that o is an operator symbol of arity n.

Every signature Ω induces the endofunctor F_{Ω}( ) = ∐_{n∈ℕ} Ω_{n} × ( )^{n} on Set where ∐ and × are respectively the coproduct and product functors. In passing, notice that F_{Ω}-coalgebras (T, τ) can be regarded as guarded substitutions where every x ∈ T (thought of as a variable) is assign to the term o(x_{1}, …, x_{n}) whenever τ(x) = (o, (x_{1}, …, x_{n})) ∈ Ω_{n} × T^{n}.

We introduce the notion of bisimulation on F_{Ω}-coalgebras:

Definition 1.1 A relation R ⊆ T ×T is a categorical F_{Ω}-bisimulation on the F_{Ω}-coalgebra (T, τ) if there exists an F_{Ω}-coalgebra structure ρ on R such that

R  F_{Ω}R ρ R F_{Ω}R ρ  π_{2} π_{1}  τ T F_{Ω}T F_{Ω}π_{1}  F_{Ω}π_{2}

commutes (i.e. such that the projections π_{1}, π_{2} : R → T become homomorphisms (R, ρ) → (T, τ)). □

In order to describe categorical bisimulations in more elementary terms we need some operations induced by a coalgebra τ : T → F_{Ω}T. For t ∈ T with τ(t) = (o, (t_{1}, …, t_{n})) ∈ Ω_{n} × T^{n}, we set

• root_{τ}(t) =^{def} o; and

• for 1 ≤ i ≤ n, subtree_{τ}(t, i) =^{def} t_{i}.

Proposition 1.2 A relation R ⊆ T × T is a categorical bisimulation on τ : T → F_{Ω}T if and only if t R t′ implies

[root_{τ}(t) = root_{τ}(t′) ∈ Ω_{n}] ∧ [∀ 1 ≤ i ≤ n. subtree_{τ}(t, i) R subtree_{τ}(t′, i)].

Proof:

(⇒) Let ρ : R → F_{Ω}R be such that, for i = 1, 2, τ ∘ π_{i} = (F_{Ω}π_{i}) ∘ ρ.

Assume t R t′ and let ρ(t, t′) = (r, ((s_{1}, s′_{1}), …, (s_{n}, s′_{n}))). Since,

τt = (F_{Ω}π_{1})(ρ(t, t′)) = (r, (s_{1}, …, s_{n})) and τt′ = (F_{Ω}π_{2})(ρ(t, t′)) = (r, (s′_{1}, …, s′_{n})),

it follows that root_{τ}(t) = r = root_{τ}(t′) and subtree_{τ}(t, i) = s_{i} R s′_{i} = subtree_{τ}(t′, i) for 1 ≤ i ≤ n.

(⇐) For t, t′ ∈ T, let ρ(t, t′) = (root_{τ}(t), ⟨(subtree_{τ}(t, i), subtree_{τ}(t′, i))⟩_{1≤i≤n}). The mapping ρ makes R into an F_{Ω}-coalgebra (i.e. a map R → ∐_{n∈ℕ} Ω_{n}×R^{n}) because

for every t R t′, subtree_{τ}(t, i) R subtree_{τ}(t′, i).

Moreover, by construction, τ ∘ π_{1} = (F_{Ω}π_{1}) ∘ ρ; whilst τ ∘ π_{2} = (F_{Ω}π_{2}) ∘ ρ because for every t R t′, root_{τ}(t) = root_{τ}(t′). □

Corollary 1.3 For every F_{Ω}-coalgebra, the equality relation is a categorical F_{Ω}-bisimulation. □

The coalgebras for which equality reduces to bisimulation are identified:

Definition 1.4 (c.f. [Acz88]) A coalgebra is strongly extensional if the equality relation is maximal among all its categorical bisimulations. □

Theorem 1.5 Final F_{Ω}-coalgebras are strongly extensional.

Proof: By Corollary 1.3, the equality relation is a categorical bisimulation. Moreover, if μ : U → F_{Ω}U is a final coalgebra and R ⊆ U ×U is a categorical bisimulation then there exists a coalgebra ρ : R → F_{Ω}R such that π_{1} and π_{2} are homomorphisms (R, ρ) → (U, μ). By the universal property of final coalgebras, it follows that π_{1} = π_{2}, and hence u R u′ implies u = u′. □

As a corollary the following proof principle holds:

Principle 1.6 If R is a categorical F_{Ω}-bisimulation on the final coalgebra U, and u and u′ are elements of U for which u R u′, then u = u′. □

The final F_{Ω}-coalgebra can be described as the set of finite and/or infinite trees generated by the signature Ω. Explicitly, an Ω-tree (see [Cou83, AM82]) is a partial function t : ℕ_{>0}^{∗} ⇀ ∐_{n∈ℕ} Ω_{n} such that its domain of definition, dom(t), satisfies the following conditions:

1. dom(t) is non-empty and prefix-closed (i.e. αi ∈ dom(t) ⇒ α ∈ dom(t));

2. for α ∈ dom(t), if t(α) ∈ Ω_{n} then, for i ∈ ℕ, αi ∈ dom(t) ⟺ 1 ≤ i ≤ n.

And, the final F_{Ω}-coalgebra is the set of Ω-trees, T_{Ω}^{ω}, with structure map

T_{Ω}^{ω} → ∐_{n∈ℕ}Ω_{n} × (T_{Ω}^{ω})^{n} : t ↦ (t(ϵ), ⟨λα ∈ ℕ_{>0}^{∗}. t(iα)⟩_{1≤i≤n}).

Hence, the coinduction principle reads:

Coinduction principle for finite and/or infinite trees:

Suppose that R is a binary relation on T_{Ω}^{ω} satisfying

t R t′ ⇒ [root(t) = root(t′) ∈ Ω_{n}] ∧ [∀ 1 ≤ i ≤ n. subtree(t, i) R subtree(t′, i)]

Then, t R t′ ⇒ t = t′.

2 Categorical bisimulation

Interleaving models of concurrent computation are generally based on transition systems. A transition system is a triple (A, S, →) where A is a set of actions, S is a set of states, and → ⊆ S × A × S is the transition relation. In general, we write p →^{a} q for (p, a, q) ∈ → and read it as “after performing the action a, the state p evolves to the state q”. Transition systems with a set of actions A can equivalently be defined as coalgebras for the endofunctor P(A × ) on Set (where P denotes the powerset endofunctor), since the map sending a transition system (A, S, →) to the coalgebra σ : p ↦ {(a, q) | p →^{a} q} establishes a bijection.

The notion of bisimulation is introduced in order to identify observationally equivalent states. Here we are only concerned with what is known as strong bisimulation. A relation R ⊆ S × S is called a bisimulation if p R q implies that

• for every p →^{a} p′, there exists a state q′ such that q →^{a} q′ and p′ R q′, and

• for every q →^{a} q′, there exists a state p′ such that p →^{a} p′ and p′ R q′.

Any relation R ⊆ S ×S can be given a coalgebra structure ρ : R → P(A×R) mapping (p, q) ↦ {(a, (p′, q′)) | p →^{a} p′, q →^{a} q′, p′ R q′}. Moreover, if R is a bisimulation then the projections from R to S are coalgebra homomorphisms from (R, ρ) to (S, σ). Conversely, every relation with a coalgebra structure making the projections into coalgebra homomorphisms is a bisimulation. This fact motivates the definition of bisimulation below.

Remark. Unless otherwise stated we assume our category of discourse to be a partial cartesian category of partial maps. This concept is defined in Appendix A; but, on a first reading, the reader may skip such details as long as he keeps in mind that this includes all cartesian categories (i.e. categories with finite products) and the usual categories of sets with structure and partial functions equipped with finite cartesian products.

Convention. Monos (i.e. morphisms m : A → B such that for every x, y : X → A, m ∘ x = m ∘ y implies x = y) are denoted with ↣.

Definition 2.1 A relation r : R ↣ S × S is a categorical bisimulation on the coalgebra (S, σ) if there exists a coalgebra structure ρ on R such that π_{i} ∘ r : (R, ρ) → (S, σ) for i = 1, 2. □

The above definition generalises that of [AM89] in that we consider endofunctors over arbitrary (partial) cartesian categories (of partial maps). This will allow us to discuss examples and establish theorems in wide generality. Concerning examples of bisimulations we have:

Convention. Pfn denotes the category of small sets and partial functions, and 1 and 2 denote canonical one and two-element sets.

Example 2.2 (Type constructor for natural numbers, 1 + : Pfn → Pfn) R ⊆ N × N is a categorical bisimulation on p : N ⇀ 1 + N if and only if n R n′ implies

• p(n) and p(n′) are both undefined, or

• p(n) and p(n′) are both defined, and either p(n) ∈ 1 ∋ p(n′), or p(n) ∈ N ∋ p(n′) and p(n) R p(n′). □

Example 2.3 (Type constructor for cantor space, 2 × : Set → Set) R ⊆ S × S is a categorical bisimulation on ⟨h, t⟩ : S → 2 × S if and only if s R s′ implies h(s) = h(s′) and t(s) R t(s′). □

More generally, for a signature Ω = ⟨Ω_{n}⟩_{n∈ℕ} (see Section 1) we can consider Ω-coalgebras and partial Ω-coalgebras:

Example 2.4 (Type constructor for infinite trees, F_{Ω}( ) : Set → Set) R ⊆ T × T is a categorical bisimulation on τ : T → F_{Ω}T if and only if t R t′ implies

τt = (r, s) ∈ Ω_{n} × T^{n} ∋ (r′, s′) = τt′

with r = r′ and s_{i} R s′_{i} for every 1 ≤ i ≤ n. □

Example 2.5 (Type constructor for finite trees, F_{Ω}( ) : Pfn → Pfn) R ⊆ T × T is a categorical bisimulation on τ : T ⇀ F_{Ω}T if and only if t R t′ implies

• τt and τt′ are both undefined, or • τt and τt′ are both defined, and

τt = (r, s) ∈ Ω_{n} × T^{n} ∋ (r′, s′) = τt′

with r = r′ and s_{i} R s′_{i} for every 1 ≤ i ≤ n. □

Example 2.6 (Type constructor for deterministic automata, 2 × (A ⇒ ) : Set → Set) A deterministic automaton [HU79] consist of a set of states and a set of transitions from state to state that occur on input symbols chosen from an alphabet. For each input symbol there is exactly one transition out of each state. Some states are designated as accepting states.

Deterministic automata with input alphabet A can be formally described as coalgebras for the functor 2×(A ⇒ ) : Set → Set. For example, ⟨α, δ⟩ : S → 2×(A ⇒ S) describes the automaton with set of states S, accepting predicate α and transition function δ.

R ⊆ S×S is a categorical bisimulation on ⟨α, δ⟩ if and only if p R q implies α(p) = α(q) and δ(p)(a) R δ(q)(a) for every a ∈ A. □

3 Final semantics

As mentioned in the introduction, recursive data types can be modelled by final coalgebras. This automatically provides a final semantics since every coalgebra can be canonically interpreted in the final one via the unique homomorphism (denoted as [[ ]]). As a step towards understanding the scope of the abstract notion of bisimulation (Definition 2.1) its relation with final semantics is studied.

Remark. The proofs of Propositions 3.1 and 3.3 below are omitted as they are, respectively, instances of Propositions 7.1 and 7.3.

Two elements are said to be bisimilar whenever there exists a bisimulation relating them.

Proposition 3.1 Bisimilar elements have the same final semantics. □

For a deterministic automaton, the final semantics corresponds to the language accepted by the automaton. The final coalgebra is

P(A^{∗}) → 2 × (A ⇒ P(A^{∗}))
L ↦ (ϵ ∈ L, λa.{w | a.w ∈ L})

and, for ⟨α, δ⟩ : S → 2 × (A ⇒ S) and p ∈ S,

• ϵ ∈ [[p]] ⟺ α(p), and

• a.w ∈ [[p]] ⟺ w ∈ [[δ(p)(a)]].

Then, applying Proposition 3.1, we conclude that bisimilar states in a deterministic automaton accept the same language. As is well-known the converse also holds. In fact, since 2×(A ⇒ ) : Set → Set preserves pullbacks, it follows from very general considerations:

Definition 3.2 The pair r_{1}, r_{2} : R → S is a weak kernel pair (kernel pair) of f : S → U if f ∘ r_{1} = f ∘ r_{2} and, for every p, q : T → S, whenever f ∘ p = f ∘ q there exists (a unique) r such that r_{1} ∘ r = p and r_{2} ∘ r = q. □

Proposition 3.3 Consider a category with kernel pairs and an endofunctor on it mapping kernel pairs to weak kernel pairs. Then, for every coalgebra, elements with the same final semantics are bisimilar. □

In general, the converse of Proposition 3.1 does not hold. To provide a counterexample, consider a simple kind of machine whose states have one of the following three capabilities: they are in deadlock (i.e. no capabilities), they can evolve to another state, or they can produce an observation. These machines can be represented as coalgebras σ : S ⇀ 1 + S where S is the set of states, and for p ∈ S, we have that σ(p) is undefined if and only if p is in deadlock, p evolves to q if and only if σ(p) = q and σ(p) ∈ 1 if and only if p produces an observation. The final machine is pred : ℕ → 1 + ℕ and, for every element p ∈ S, the final semantics is [[p]] = μn[σ^{n+1}(p) ∈ 1] where μ is the minimisation operator of recursion theory. For the machine whose set of states is {nil, loop} where nil is in deadlock and loop evolves to itself we have that [[nil]] = [[loop]]. But, by the characterisation of bisimulations given in Example 2.2, nil and loop cannot be bisimilar.

This should be interpreted as the inability of the final semantics to discriminate between some different operational behaviours. This happens because the final semantics is very abstract. As will be shown, the final coalgebra does not have distinct bisimilar elements.

4 Strong-extensionality theorem

The theorem justifying the coinduction principle is stated. We start by internalising the notion of equality.

Definition 4.1 The equality relation e_{S} : =_{S}↣ S × S is defined as the equaliser of π_{1}, π_{2} : S × S → S. □

Remark. The equality relation could have been defined to be ⟨id_{S}, id_{S}⟩ : S ↣ S × S. However, the previous definition was chosen for two reasons: it generalises to categories of partial maps and it provides the intuition for the generalisation we carry out in Section 6.

Proposition 4.2 For every coalgebra, the equality relation is a categorical bisimulation. □

Theorem 4.3 (Strong extensionality) Final coalgebras are strongly extensional (according to Definition 1.4). □

Remark. The proofs of Proposition 4.2 and Theorem 4.3 are omitted as they are instances of Proposition 6.3 and Theorem 6.8.

Convention. Given monos m : D ↣ A and n : E ↣ A, we write m ⊆ n (or even D ⊆ E) whenever m factors through n.

A map p : 1 ↣ S is said to be an element of S. Given a relation r : R ↣ S × S and elements p, q : 1 ↣ S we write p r q (or even p R q) whenever ⟨p, q⟩ ⊆ r.

As a corollary the following proof principle holds:

Principle 4.4 If R is a categorical bisimulation on the final coalgebra U, and u and u′ are elements of U for which u R u′, then u = u′. □

This abstract formulation instantiated to the examples of Section 2 yields the following coinduction principles:

Finite and/or infinite trees:

Recalling that for a signature Ω, the final coalgebra of F_{Ω}( ) : Set → Set is T_{Ω}^{ω}, the set of (finite and infinite) Ω-trees and that the final coalgebra of F_{Ω}( ) : Pfn → Pfn is T_{Ω}, the Ω-word algebra; the principle reads:

Suppose that R is a binary relation on T_{Ω} or T_{Ω}^{ω} satisfying

t R t′ ⇒ [root(t) = root(t′) ∈ Ω_{n}] ∧ [∀ 1 ≤ i ≤ n. subtree(t, i) R subtree(t′, i)]

Then, t R t′ ⇒ t = t′.

Taking

Ω = ⟨Ω_{0} = {0}, Ω_{1} = {succ}, Ω_{n} = ∅ for n ≥ 2⟩ in Pfn

and

Ω = ⟨Ω_{0} = ∅, Ω_{1} = 2, Ω_{n} = ∅ for n ≥ 2⟩ in Set

we obtain the principles provided in [Smy91] (though derived there in a more indirect fashion) for ℕ and 2^{ω}.

Natural numbers:

Suppose that R is a binary relation on ℕ satisfying

n R n′ ⇒ [n = 0 = n′] ∨ [pred(n) R pred(n′)]

Then, n R n′ ⇒ n = n′.

Cantor space:

Suppose that R is a binary relation on 2^{ω} such that

s R s′ ⇒ [head(s) = head(s′)] ∧ [tail(s) R tail(s′)]

Then, s R s′ ⇒ s = s′.

The following coinduction principle seems to be new (though its usefulness is still to be proved).

Languages:

Suppose that R is a binary relation on P(A^{∗}) for which

L R L′ ⇒ [ϵ ∈ L ⟺ ϵ ∈ L′] ∧ [∀ a ∈ A. {w | a.w ∈ L} R {w | a.w ∈ L′}]

Then, L R L′ ⇒ L = L′.

So far we have demonstrated that coinduction principles are not exclusive to a particular category of data types. Next, the approach is extended to categories of domains as solutions to recursive data types are more frequently encountered in this setting.

5 Ordered categorical bisimulation

In the vein of [SP82, Fre90, FP92, Fio94] our analysis is not committed to a particular category of domains (i.e. certain kind of partial orders) but based on the structure such a category should have. In this respect, (order-)enriched category theory is fundamental and so it is adopted as the main mathematical tool.

To keep the paper self contained, the enriched notions used throughout are provided. (For a thorough treatment of enriched category theory consult [Kel82].)

Let Poset (Cpo) be the category of small posets (cpos —posets, possibly without a least element, closed under lubs of ω-chains) and monotone (continuous) functions.

A Poset-category (Cpo-category) C is a category whose hom-sets C(A, B) come equipped with a partial order (ω-complete partial order) ≤_{A,B} with respect to which composition of morphisms ∘ : C(B, C) × C(A, B) → C(A, C) is a monotone (continuous) operation.

The immediate examples of Poset-categories are Poset and Cpo where each hom-set is ordered pointwise; even more, Cpo is a Cpo-category. More examples are obtained from the observation that every category freely induces a Poset-category (Cpo-category) by discretely ordering each hom-set.

For Poset-categories (Cpo-categories) A and B, a Poset-functor (Cpo-functor) F : A → B is a functorial mapping such that for every A, A′ ∈ | A | the assignment F_{A,A′} : A(A, A′) → B(F A, F A′) is monotone (continuous).

Categorical bisimulation is adapted to the order-enriched setting:

Definition 5.1 In a Poset-category, a relation r : R ↣ S × S is called an ordered categorical bisimulation on the F -coalgebra (S, σ) if there exists a coalgebra structure ρ on R such that

F R  F Sσ R ρ  ≥  F R S  Rρ r_{1}  r_{2} F r_{1}  F r_{2}

where r_{i} =^{def} π_{i} ∘ r (i = 1, 2). □

Remark. When considering (partial) products in Poset-categories, the pairing of morphisms is assumed to be monotone.

Convention. A morphism f : A → B is called a lax-homomorphism from the F -coalgebra (A, α) to the F -coalgebra (B, β) whenever F f ∘ α ≥ β ∘ f. (Thus, r_{1} in the definition above is a lax-homomorphism from (R, ρ) to (S, σ).)

For examples, consider:

Example 5.2 (1 + : Pfn → Pfn) R ⊆ N × N is an ordered categorical bisimulation on p : N ⇀ 1 + N if and only if n R m implies

• if p(n) is defined then so is p(m) and either p(n) ∈ 1 ∋ p(m), or p(n) ∈ N ∋ p(m) and p(n) R p(m), and

• if p(n) is undefined then, whenever p(m) ∈ N, there exists k such that k R p(m).□

Example 5.3 (P_{A}( ) : SFP_{⊥} → SFP_{⊥}, c.f. [Pit94, Section 5]) For a set A, let P_{A}( ) be the functor {∅}_{⊥} ⊕ P^{♮}(A_{⊥} ⊗ ), where ( )_{⊥}, ⊕, ⊗ and P^{♮}( ) are the lifting, coalesced sum, smash product and convex powerdomain [Plo76] functors.

Then, for every set S, the (strict) coalgebras S_{⊥} ∘→ P_{A}(S_{⊥}) can be viewed as those transition systems with divergence [Abr91] (S, → ⊆ S ×A×S, ↑ ⊆ S) such that, for every p ∈ S, if {(a, q) | p →^{a} q} is infinite then p ∈ ↑. This is because the map sending (S, →, ↑) to

σ : p ↦ \{ \begin{matrix}⊥ & if p = ⊥ \\ \{(a, q) | p →^{a} q\} ∪ \{⊥ | p ∈ ↑\} & if p ≠ ⊥ \end{matrix}

establishes a bijective correspondence.

For R ⊆ S × S, if R_{⊥} ↣ S_{⊥} ⊗ S_{⊥} is an ordered categorical bisimulation on σ then R is a partial bisimulation [Abr91] on (S, →, ↑); that is, p R q implies

∀ p →^{a} p′. ∃ q′. q →^{a} q′ ∧ p′ R q′

∧

p ↓ ⇒ q ↓ ∧ ∀ q →^{a} q′. ∃ p′. p →^{a} p′ ∧ p′ R q′,

where p ↓⟺ p ∉ ↑. □

Ordered categorical bisimulations resemble the notion of ‘bisimulation up to’ [Mil89]:

Example 5.4 Let ω^{⊤} be ω with a top element and let ( )_{⊥} : Cpo → Cpo be the lifting functor.

R ⊆ ω^{⊤} × ω^{⊤} (viewed as a discrete cpo) is an ordered categorical bisimulation on the coalgebra pred : ω^{⊤} → (ω^{⊤})_{⊥} if and only if n R m implies n = 0 = m, or both m > 0 and there exists k for which pred(n) ≤ k R pred(m). □

6 Order strong-extensionality theorem

An order-enriched version of the strong-extensionality theorem is obtained. To internalise the inequality, the 2-categorical notion of inserter is used in the context of order-enriched categories.

Definition 6.1 In a Poset-category, x : X → A is an inserter of the ordered pair (f : A → B, g : A → B) if f ∘ x ≤ g ∘ x and for every y : Y → A such that f ∘ y ≤ g ∘ y, there exists a unique u for which y = x ∘ u. □

Inserters behave like equalisers where equality has been replaced by inequality. For example, essentially the same proof that shows equalisers to be monos shows inserters to be monos as well.

For a cpo D, define ≤_{D} to be the subcpo of D×D with underlying set {(x, y) | x ≤ y}. In Cpo and in pCpo, the category of cpos and partial continuous functions [Plo85] (i.e. partial functions whose domain of definition is Scott-open and such that its restriction to the domain of definition is continuous), ≤_{D}↣ D × D is the inserter of (π_{1}, π_{2}). This motivates the abstract definition of inequality:

Definition 6.2 In a Poset-category, the inequality relation l_{S} : ≤_{S}↣ S × S is defined as the inserter of (π_{1}, π_{2}). □

Proposition 6.3 For every coalgebra, the inequality relation is an ordered categorical bisimulation.

Proof: For a coalgebra (S, σ), let δ : S ↣≤_{S} be the unique morphism, given by the universal property of inserters, for which l_{S} ∘ δ = ⟨id_{S}, id_{S}⟩; and give ≤_{S} the following coalgebra structure, F δ ∘ σ ∘ π_{2} ∘ l_{S}. □

Definition 6.4 A coalgebra is order strongly extensional if the inequality relation is maximal among all its ordered categorical bisimulations. □

In the Poset-enriched setting, final coalgebras need not be order strongly extensional. Thus, a stronger notion is needed:

Definition 6.5 In a Poset-category, a coalgebra is maximally-final if it is final and the unique homomorphism from any other coalgebra is maximal among all lax-homomorphisms.

□ Proposition 6.6 Maximally-final coalgebras are order strongly extensional.

Proof: If r is a categorical ordered bisimulation on a maximally-final coalgebra U, then r_{1} ≤ r_{2}. And, by the universal property of inserters, it follows that r ⊆ l_{U}. □

The above proposition is useful only if there are simple criteria to recognise maximallyfinal coalgebras. In particular, the best one can hope for is that final coalgebras of Posetendofunctors are automatically maximally-final. Unfortunately, this is not the case. For example, let Z be the Poset-category induced by the ordered monoid (ℤ, 0, +, ≤). The Poset-endofunctor 2 : Z → Z that multiplies morphisms by 2, has 0 as a final coalgebra. In fact, −n : n → 0 is the unique mediating homomorphism. If 0 were to be maximally final, then for every lax-homomorphism m : n → 0 the inequality m ≤ −n should hold. But, on the contrary, m : n → 0 is a lax-homomorphism if and only if m ≥ −n. It then seems inevitable to abandon Poset-enrichment and move onto the more comfortable Cpo-enriched case:

Proposition 6.7 ([Plo91]) Final coalgebras of Cpo-endofunctors are maximally-final.

Proof: Let K be a Cpo-category and let F be a Cpo-endofunctor on it. Let (U, μ) be a final coalgebra and let f be a lax-homomorphism from a coalgebra (S, σ) to (U, μ).

Define Φ : K(S, U) → K(S, U) as the continuous mapping x ↦ μ^{−1} ∘ (F x) ∘ σ. Then, ⟨Φ^{n}(f)⟩ is an ω-chain and

⨆ Φ^{n+1}(f) = ⨆ μ^{−1} ∘ F(Φ^{n}(f)) ∘ σ
= μ^{−1} ∘ F( ⨆ Φ^{n}(f)) ∘ σ.

Thus, ⨆ Φ^{n}(f) is the mediating morphism from (S, σ) to (U, μ) and f ≤ ⨆ Φ^{n}(f). □

Propositions 6.6 and 6.7 imply:

Theorem 6.8 (Order strong extensionality) Final coalgebras on a Cpo-endofunctor are order strongly extensional. □

Finally, the proof principle reads as follows:

Principle 6.9 For a Cpo-endofunctor, if R is an ordered categorical bisimulation on the final coalgebra U, and u and u′ are elements of U for which u R u′, then u ≤ u′. □

7 Final semantics in the order-enriched setting

We establish generalisations of Propositions 3.1 and 3.3 in the order-enriched setting.

Proposition 7.1 The final semantics into maximally-final coalgebras transforms ordered bisimilarity into inequality.

Proof: Let U be a maximally-final coalgebra, and let p and q be elements of a coalgebra S.

If R is an ordered categorical bisimulation on S then, by the universal property of maximally-final coalgebras, it follows that [[ ]] ∘ π_{1} ∘ R ≤ [[ ]] ∘ π_{2} ∘ R. Moreover, if p R q then, writing ⟨⟨p, q⟩⟩ for the unique element of R such that ⟨p, q⟩ = R ∘ ⟨⟨p, q⟩⟩, it follows that [[p]] = [[ ]] ∘ π_{1} ∘ R ∘ ⟨⟨p, q⟩⟩ ≤ [[ ]] ∘ π_{2} ∘ R ∘ ⟨⟨p, q⟩⟩ = [[q]]. □

Definition 7.2 In a Poset-category, the ordered pair (r_{1} : R → S, r_{2} : R → S) is a (right-strict) bistrict lax-kernel pair of f : S → U if f ∘ r_{1} ≤ f ∘ r_{2} and, for every p, q : T → S, whenever f ∘ p ≤ f ∘ q there exists a unique r such that (r_{1} ∘ r ≥ p) r_{1} ∘ r = p and r_{2} ∘ r = q. □

Proposition 7.3 Consider a Poset-category with bistrict lax-kernel pairs and a Poset-endofunctor on it mapping bistrict lax-kernel pairs to weak right-strict lax-kernel pairs. Then, for every coalgebra, elements with less than or equal final semantics are ordered bisimilar.

Proof: Let (U, μ) be a final F -coalgebra. For an F -coalgebra (S, σ) let (r_{1} : R → S, r_{2} : R → S) be a bistrict lax-kernel pair of [[ ]] : S → U. Then R is a relation (i.e. ⟨r_{1}, r_{2}⟩ : R ↣ S × S). Let us see that it is an ordered bisimulation,

F [[ ]] ∘ σ ∘ r_{1} = μ ∘ [[ ]] ∘ r_{1} ≤ μ ∘ [[ ]] ∘ r_{2} = F [[ ]] ∘ σ ∘ r_{2}

and, since (F r_{1}, F r_{2}) is a weak right-strict lax-kernel pair of F [[ ]], it follows that there exists a ρ such that F r_{1} ∘ ρ ≥ σ ∘ r_{1} and F r_{2} ∘ ρ = σ ∘ r_{2}.

Finally, by the universal property of bistrict lax-kernel pairs, for two elements p and q of S, if [[p]] ≤ [[q]] then p R q. □

Remark. For categories of partial maps the above argument breaks down since we know that R is a subobject of the categorical product in the category of partial maps (if it exists) but we cannot guarantee that R is a subobject of the categorical product in the subcategory of total maps (see remark after Definition 2.1 and Appendix A).

For examples of final semantics for applicative and non-deterministic languages see [TJ93].

8 Applicative bisimulation for the untyped λ_{V} -calculus

As another application of the theory developed, an internal full abstraction result for the canonical model of the untyped call-by-value λ-calculus is proved.

In [AO93], and in [Pit94], as an example of coinduction for recursively defined domains, such a result is provided for the untyped lazy λ-calculus. Their proof relies on the way the model is constructed, namely as the colimit of a certain ω-chain of approximations. Instead, in accordance with [Pit93], it is shown that this kind of result follows from the universal property of the model.

First, the theory needed to solve domain equations for bifunctors in the spirit of [Fre91] is sketched (for details see [Fio94, Chapters 6 and 7]). Along the way, it is observed that a coinduction principle is also available for bifunctors.

Definition 8.1 (c.f. [Fre91]) A category is said to be (Cpo-)algebraically compact if every (Cpo-)endofunctor F on it has a free algebra α : F A → A, in the sense that is an initial algebra such that α^{−1} : A → F A is a final coalgebra. □

Examples of algebraically compact categories can be found in [Fre92]. Here we just recall that pCpo is Cpo-algebraically compact and therefore so is pCpo^{op} × pCpo (see [FP92, Fio94]).

Next we consider parameterised free algebras. Let K be a category and let L be an algebraically compact category. Given G : K × L → L, for every K ∈ | K | let ι_{K}^{G} : G(K, G^{†}K) → G^{†}K be a free G(K, )-algebra. Then, G^{†} extends to a functor from K to L where for every f : K → A, we define G^{†}f to be the unique morphism making

G(K, G^{†}K) G(A, G^{†}A)  G^{†}K G^{†}AG^{†}f G(f, G^{†}f)  ι_{A}^{G} ι_{K}^{G}

commute.

The key lemma (specifically item 2) that allows us to apply the strong-extensionality theorem to bifunctors follows:

Lemma 8.2 Let K and L be algebraically compact categories, and let F : K × L → K and G : K × L → L be functors.

1. (Bekic̆’s lemma for algebraically compact categories [Fre92]) If (A, α) is a free F ( , G^{†} )-algebra then ((A, G^{†}A), (α, ι_{A}^{G})) is a free ⟨F, G⟩-algebra.

2. If ((K, L), (κ, λ)) is a free ⟨F, G⟩-algebra then (L, λ) is a free G(K, )-algebra.

Proof: (2) Let (A, α) be a free F ( , G^{†} )-algebra.

By Bekic̆’s lemma, there exists an isomorphism (k, l) ∈ K × L such that

F (A, G^{†}A)  A F (K, L)  K  G(A, G^{†}A)  G^{†}A G(K, L)  L G(k, l) F (k, l)  k  l λ ι_{A}^{G} α κ

Then, l ∘ G^{†}(k^{−1}) is a G(K, )-algebra isomorphism from (G^{†}K, ι_{K}^{G}) to (L, λ). □

Convention. We write K̆ for K^{op} × K and for a bifunctor F : K̆ → K we define F̆ : K̆ → K̆ : (f′, f) ↦ (F (f, f′), F (f′, f)).

Also, ⇀ ⇀ is defined to be the bifunctor pCpo( , ) : p̆Cpo → pCpo.

The canonical model of the untyped call-by-value λ-calculus is specified next:

Proposition 8.3 In pCpo, there exists an isomorphism δ : D → D⇀ ⇀D such that (D, δ) is a free D⇀ ⇀ -coalgebra.

Proof: Since p̆Cpo is Cpo-algebraically compact it follows that ˘ ⇀ ⇀ : p̆Cpo → p̆Cpo has a free algebra of the form ((D, D), (δ, δ^{−1})) —see [Fio94]— and, by Lemma 8.2 (2), (D, δ) is a free D⇀ ⇀ -coalgebra. □

Remark. D (as in the above proposition) can be obtained as the colimit in pCpo of the ω-chain ⟨δ_{n} : D_{n} → D_{n+1}⟩ defined as

D_{n} = \{ \begin{matrix}∅ & if n = 0 \\ D_{n−1}⇀ ⇀D_{n−1} & if n ≥ 1 \end{matrix}  δ_{n} = \{ \begin{matrix}∅ & if n = 0 \\ δ_{n−1}^{R}⇀ ⇀δ_{n−1} & if n ≥ 1 \end{matrix}

where (δ_{n}, δ_{n}^{R}) is an embedding-projection pair.

Let P be a cpo. For the endofunctor P ⇀ ⇀ : pCpo → pCpo, a relation R ⊆ S × S (viewed as a discrete cpo) is a categorical bisimulation on the coalgebra σ : S ⇀ P ⇀ ⇀S if and only if s R s′ implies that for every p ∈ P, either σ(s)(p) and σ(s′)(p) are both undefined, or they are both defined and σ(s)(p) R σ(s′)(p). The notion of bisimulation for the applicative structures considered here is obtained by making the notion of categorical bisimulation asymmetric (in the same way that Kleene’s equality is generalised to Kleene’s inequality).

Definition 8.4 A relation R ⊆ S × S is an applicative bisimulation on σ : S ⇀ P ⇀ ⇀S if s R s′ implies that for every p ∈ P, if σ(s)(p) is defined then so is σ(s′)(p) and σ(s)(p) R σ(s′)(p). □

Convention. For a subset X of a cpo P we write \overline{X} for its closure under lubs of ω-chains and X̂ for {⨆ x_{n} | ⟨x_{n}⟩ is an ω-chain in X}.

Proposition 8.5 1. If R ⊆ S × S is an applicative bisimulation on σ : S ⇀ P ⇀ ⇀S then so is R̂.

2. If {R_{i} ⊆ S × S | i ∈ I} is a family of applicative bisimulations on σ : S ⇀ P ⇀ ⇀S then ⋃_{i∈I} R_{i} is an applicative bisimulation on σ.

Proof:

(1) Let s R̂ s′ and let ⟨x_{n}, x_{n}′⟩ be an ω-chain in R with ⨆ x_{n} = s and ⨆ x_{n}′ = s′.

For p ∈ P, if σ(s)(p) = σ(⨆ x_{n})(p) is defined then there exists n_{0} such that for all n ≥ n_{0}, σ(x_{n})(p) is defined and ⨆_{n≥n_{0}} σ(x_{n})(p) = σ(⨆ x_{n})(p). Then, since R is an applicative bisimulation, for all n ≥ n_{0}, σ(x_{n}′)(p) is defined and σ(x_{n})(p) R σ(x_{n}′)(p). Thus, ⨆_{n≥n_{0}} σ(x_{n}′)(p) = σ(⨆ x_{n}′)(p) is defined and

σ(s)(p) = ⨆_{n≥n_{0}} σ(x_{n})(p) R̂ ⨆_{n≥n_{0}} σ(x_{n}′)(p) = σ(s′)(p).

(2) Straightforward. □

Corollary 8.6 If R ⊆ S × S is an applicative bisimulation on σ : S ⇀ P ⇀ ⇀S then so is \overline{R}.

Proof: Define

R_{0} = R,
R_{k+1} = R̂_{k}  for k an ordinal,
R_{l} = ⋃_{k<l} R_{k} for l a limit ordinal.

Then, by transfinite induction using Proposition 8.5, R_{k} is an applicative bisimulation for every k. The result follows because \overline{R} = R_{k} for some (sufficiently large) k. □

Every applicative bisimulation on a cppo induces an ordered categorical bisimulation containing it:

Proposition 8.7 If R ⊆ S_{⊥} × S_{⊥} is an applicative bisimulation on σ : S_{⊥} ⇀ P ⇀ ⇀S_{⊥} then \overline{R} ∪ (\{⊥\} × S_{⊥}) ↣ S_{⊥} × S_{⊥} is an ordered categorical bisimulation on (S_{⊥}, σ).

Proof: Writing R′ for \overline{R} ∪ (\{⊥\}×S_{⊥}), the continuous function ρ : R′ → P ⇀ ⇀R′, where ρ(s, s′) is the partial continuous function mapping

p ↦ \{ \begin{matrix}(σ(s)(p), σ(s′)(p)) & if σ(s)(p) ↓ and σ(s′)(p) ↓ \\ (⊥, σ(s′)(p)) & if σ(s)(p) ↑ and σ(s′)(p) ↓ \end{matrix}

shows that R′ is an ordered categorical bisimulation. □

The definition of applicative bisimulation straightforwardly implies:

Proposition 8.8 For every σ : S ⇀ P ⇀ ⇀S, the inequality relation ≤_{S} is an applicative bisimulation. □

Finally, the result is stated and proved.

Theorem 8.9 (Internal full abstraction) The inequality relation ≤_{D} is maximal among all applicative bisimulations on δ : D → D⇀ ⇀D as in Proposition 8.3.

Proof: By Proposition 8.8, ≤_{D} is an applicative bisimulation. It is the maximal such because if R is an applicative bisimulation on (D, δ) then, by Proposition 8.7 and the order strong-extensionality theorem, \overline{R} ∪ (\{⊥\} × D) ↣ ≤_{D}. Thus, R ⊆ ≤_{D}. □

9 Concluding remarks and future work

We have concentrated on the impact of one of the fundamental concepts in concurrency theory, namely bisimulation, on the theory of data types. We have related an abstract formulation of bisimulation and the final coalgebra approach to the semantics of data types: we established conditions under which the operational notion of bisimulation and the denotational notion of final semantics coincide and provided a coinduction principle for recursive data types.

Further study of the relationship between order strong-extensionality and finality in Cppo_{⊥} can be found in [Rut93]. There, final coalgebras of Cpo-endofunctors mapping bistrict lax-kernel pairs to weak right-strict lax-kernel pairs are characterised as order strongly-extensional dense-epis.

In view of the ideas exposed throughout, one of the more important open issues is whether the theory of data types can provide some feedback into the theory of concurrency. In this respect, for example, the study of the category of P(A × )-coalgebras (regarded as a category of transition systems with set of actions A) might provide new insight into models for concurrency. To a certain extent, this has already occurred since this category of transition systems has the interesting property of having bisimulationpreserving maps, it differs from the one considered in [WN94] and, as far as we know, it has not yet been studied.

Another intriguing connection appears with the work of Amadio and Cardelli [AC93]. They considered a simply-typed λ-calculus with recursive types and define two recursive types to be equal if they induce the same infinite tree obtained by unfolding the recursive type. This is a form of final semantics and testing for equality reduces to finding a bisimulation. This might not be completely surprising since on page 25 of the paper, while presenting the most interesting rule (contractiveness) for characterising equality, they point out that it “was also inspired by a standard proof technique for bisimulation”. It would be interesting to investigate the precise relation between bisimulation and contractiveness in the context of type equality and subtyping.

Acknowledgements

This work was done under the supervision of Gordon Plotkin and Barry Jay. I would like to thank them both for their involvement and guidance. I would also like to thank Andy Pitts and Jan Rutten for comments on previous drafts, to one of the LICS referees for providing useful comments, and to Thomas Streicher for detecting an error in a previous version. Finally, I am grateful to the IC referees for their detailed comments that led to a much better presentation.

A Categories of partial maps

For a thorough treatment of categories of partial maps consult [RR88] and [Fio94, Chapter 3].

A.1 Partial maps

Definition A.1 ([Mog86, Ros86]) A domain structure is a pair (K, D) consisting of a category K and a well-powered category D, such that D is a full-on-objects subcategory of K all of whose morphisms are monos in K, with the following closure property: every diagram X ⟶^{f} A ↢^{n} D with f ∈ K and n ∈ D has a pullback in K and if

X ↢^{f^{−1}(n)} f^{−1}(D) ⟶^{n^{∗}f} D is any such pullback then f^{−1}(n) ∈ D. □

Convention. K is called the category of total maps, and D is called the category of admissible monos.

Definition A.2 The category of partial maps p(K, D) induced by a domain structure (K, D) has the same objects as K; a partial map [m, f] : A ⇀ B is an equivalence class of spans A ↢^{m} D ⟶^{f} B in D × K, where two spans A ↢^{m} D ⟶^{f} B and A ↢^{n} E ⟶^{g} B are equivalent if and only if m = n ∘ i and f = g ∘ i for some isomorphism i : D ≅ E. Composition of partial maps is given as for relations, by pullback; identities have the form [id_{A}, id_{A}]. □

Convention. Whenever we write p(K, D) it is assumed that (K, D) is a domain structure; when D is clear from the context we simply write pK.

To distinguish total maps (i.e. morphisms in K) from partial maps (i.e. morphisms in pK) we denote the former with → and the latter with ⇀.

The motivating example of a domain structure is (Cpo, Σ) where Σ is the subcategory of Cpo consisting of all those order-reflecting monos whose subobjects are Scott-open. We have: p(Cpo, Σ) ≅ pCpo.

A.2 Binary partial products

Let K have binary products. The partial pairing of u = [m, f] : B ⇀ A_{1} and v = [n, g] : B ⇀ A_{2} is the partial map B ⇀ A_{1} × A_{2} defined by

⟨u, v⟩ = [m ∩ n, (f ∘ m^{−1}(n), g ∘ n^{−1}(m))]

where ( , ) is the pairing of total maps. The product functor on K extends to a partial product functor × : pK × pK → pK sending a pair of objects (A, B) to A × B and a pair of partial maps (u, v) to ⟨u ∘ π_{1}, v ∘ π_{2}⟩.

Definition A.3 A category of partial maps p(K, D) is partial cartesian if its subcategory of total maps K is cartesian. □

References

[Abr91] S. Abramsky. A domain equation for bisimulation. Information and Computation, 92:161–218, 1991.

[AC93] R.M. Amadio and L. Cardelli. Subtyping recursive types. ACM Transactions on Programming Languages and Systems, 15(4):575–631, 1993.

[Acz88] P. Aczel. Non-well-founded Sets. C.S.L.I. Lecture Notes; no. 14, 1988.

[AM82] M. Arbib and E. Manes. Parametrized data types do not need highly constrained parameters. Information and Control, 52:139–158, 1982.

[AM89] P. Aczel and P.F. Mendler. A final coalgebra theorem. In D.H. Pitt, D.E. Rydeheard, P. Dybjer, A.M. Pitts, and A. Poigné, editors, Category Theory and Computer Science, volume 389 of Springer-Verlag, pages 357–365, September 1989.

[AO93] S. Abramsky and C.-H. L. Ong. Full abstraction in the lazy lambda calculus. Information and Computation, 105:159–267, 1993.

[Cou83] B. Courcelle. Fundamental properties of infinite trees. Theoretical Computer Science, 25:95–169, 1983.

[Fio94] M.P. Fiore. Axiomatic Domain Theory in Categories of Partial Maps. PhD thesis, University of Edinburgh, 1994. To be published by Cambridge University Press in the Distinguished Dissertations Series.

[FP92] M.P. Fiore and G.D. Plotkin. On compactness and Cpo-enriched categories. In G. Winskel, editor, Proceedings of the CLICS Workshop (23-27 March 1992), volume 397-II of DAIMI PB, pages 571–584. Computer Science Department, Aarhus University, May 1992.

[Fre90] P.J. Freyd. Recursive types reduced to inductive types. In 5^{th} LICS Conf., pages 498–507. IEEE, Computer Society Press, 1990.

[Fre91] P.J. Freyd. Algebraically complete categories. In A. Carboni, M. C. Pedicchio, and G. Rosolini, editors, Category Theory, volume 1488 of Lecture Notes in Mathematics, pages 131–156. Springer-Verlag, 1991.

[Fre92] P.J. Freyd. Remarks on algebraically compact categories. In M.P. Fourman, P.T. Johnstone, and A.M. Pitts, editors, Applications of Categories in Computer Science, volume 177 of London Mathematical Society Lecture Note Series, pages 95–106. Cambridge University Press, 1992.

[Gor80] M.J.C. Gordon. The denotational semantics of sequential machines. Information Processing Letters, 10(1):1–3, February 1980.

[HJ95] C. Hermida and B. Jacobs. Induction and coinduction via subset types and quotient types. In P. Dybjer and R. Pollack, editors, Informal proceedings of the Joint CLICS-TYPES Workshop on Categories and Type Theory, May 1995. (Available as Technical Report 85, Programming Methodology Group, Göteborg University and Chalmers University of Technology).

[HPJW92] P. Huday, S. Peyton Jones, and P. Wadler. Report on the functional programming language Haskell, Version 1.2. SIGPLAN Notices, 27(5), May 1992.

[HU79] J.E. Hopcroft and J.D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979.

[Kel82] G.M. Kelly. Basic Concepts of Enriched Category Theory. Cambridge University Press, 1982.

[LS94] F.W. Lawvere and S.H. Schanuel. Conceptual Mathematics: A first introduction to categories. Buffalo Workshop Press, 1994.

[Mil89] R. Milner. Communication and Concurrency. Prentice Hall, 1989.

[Mog86] E. Moggi. Categories of partial morphisms and the partial lambda-calculus. In Proceedings Workshop on Category Theory and Computer Programming, Guildford 1985, volume 240 of Lecture Notes in Computer Science, pages 242– 251. Springer-Verlag, 1986.

[MT88] R. Milner and M. Tofte. Co-induction in relational semantics. Technical Report ECS-LFCS-88-65, University of Edinburgh, Department of Computer Science, October 1988.

[MTH90] R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. MIT Press, 1990.

[Par80] D.M. Park. On the semantics of fair parallelism. In D. Bjørner, editor, Abstract Software Specifications, volume 86 of Lecture Notes in Computer Science, pages 504–526. Springer-Verlag, 1980.

[Par81] D.M. Park. Concurrency and automata on infinite sequences. Lecture Notes in Computer Science, 104:167–183, 1981.

[Pie91] B.C. Pierce. Basic Category Theory for Computer Scientists. MIT Press, 1991.

[Pit93] A.M. Pitts. Relational properties of recursively defined datatypes. In 8^{th} LICS Conf. IEEE, Computer Society Press, 1993.

[Pit94] A.M. Pitts. A co-induction principle for recursively defined domains. Theoretical Computer Science, 124:195–219, 1994.

[Plo76] G.D. Plotkin. A powerdomain construction. SIAM Journal of Computing, 5(3):452–487, 1976.

[Plo85] G.D. Plotkin. Denotational semantics with partial functions. Lecture at C.S.L.I. Summer School, 1985.

[Plo91] G.D. Plotkin. Some notes on recursive domain equations. Handwritten notes for the Domain Theory PG Course. University of Edinburgh, 1991.

[Ros86] G. Rosolini. Continuity and Effectiveness in Topoi. PhD thesis, University of Oxford, 1986.

[RR88] E. Robinson and G. Rosolini. Categories of partial maps. Information and Computation, 79:95–130, 1988.

[RT93] J. Rutten and D. Turi. On the foundations of final semantics: Non-standard sets, metric spaces, partial orders. In J.W. de Bakker, W.P. de Roever, and Rozenberg, editors, Proc. of the REX workshop, Semantics: Foundations and Applications, volume 666 of Lecture Notes in Computer Science. Springer-Verlag, 1993.

[Rut93] J. Rutten. A structural co-induction theorem. In Proc. of the 9^{th} Conference on the Mathematical Foundations of Programming Semantics, Lecture Notes in Computer Science. Springer-Verlag, 1993. To appear.

[Smy91] M.B. Smyth. I-categories and duality. In M.P. Fourman, P.T. Johnstone, and A.M. Pitts, editors, Applications of Categories in Computer Science, volume 177 of London Mathematical Society Lecture Note Series, pages 270–287. Cambridge University Press, 1991.

[SP82] M.B. Smyth and G.D. Plotkin. The category-theoretic solution of recursive domain equations. SIAM Journal of Computing, 11(4):761–783, November 1982.

[SS71] D.S. Scott and C. Strachey. Towards a mathematical semantics for computer languages. Technical Report PRG-6, Oxford Univ. Computing Lab., 1971.

[TJ93] D. Turi and B. Jacobs. On final semantics for applicative and nondeterministic languages. In CTCS-5 (Category Theory and Computer Science Fifth Biennial Meeting), pages 52–57. CWI, September 1993.

[WN94] G. Winskel and M. Nielsen. Models for concurrency. Technical Report RS-94-12, BRICS Research Series, May 1994. To appear as a chapter in the Handbook of Logic in Computer Science.