A Theory of Recursive Domains with Applications to Concurrency

(Extended Abstract)

Gian Luca Cattani^{1}, Marcelo Fiore^{2,}^{∗}, Glynn Winskel^{1}

1BRICS^{†}, University of Aarhus, Denmark 2COGS, University of Sussex, UK

Abstract

We develop a 2-categorical theory for recursively defined domains. In particular, we generalise the traditional approach based on order-theoretic structures to categorytheoretic ones. A motivation for this development is the need of a domain theory for concurrency, with an account of bisimulation. Indeed, the leading examples throughout the paper are provided by recursively defined presheaf models for concurrent process calculi. Further, we use the framework to study (open-map) bisimulation.

Introduction

A motivation for this work comes from concurrency where it has become pressing to lift domain theory from its traditional treatment of partial orders of information to categories. The models used in concurrency have too intricate a structure to fit comfortably within partial orders; only within categories can we see the constructions of process languages as universal and exploit the preservation properties of adjoints in relating models [37]. The presentation of models for concurrency as categories makes possible a general definition of bisimulation based on open maps, once a distinguished subcategory of paths is given [15].

This definition of bisimulation suggested a much broader class of models for concurrency built directly from the categories of paths—presheaf models. The Yoneda embedding provides each presheaf category with a canonical choice of path category and so of open maps and bisimulation [14]. Presheaf models can be assembled together in the bicategory of profunctors [3] or its equivalent presentation as the 2-category Prof of colimit-preserving functors between presheaf categories (with natural transformations as 2-cells). The key facts here are: open maps and so bisimulation are preserved by such functors [5]; the 2-category is rich in constructions which can be summarised as those we expect from a model of classical linear logic [36, 4]; open maps are closed under a wide range of constructions [13, 14]. We have the basics of a domain theory for concurrency with a compositional account of bisimulation, though at a cost; we have to move domain theory up a level to handle categories rather than just partial orders and the theory has not yet been set in place. This is the intended rôle of the work described here, where we show how to solve domain equations beyond the traditional Cpo-enriched setting and make a start on applications to concurrency. For example, we provide the first domain-theoretic characterisation of strong bisimulation for arbitrary trees.

The generalisation of domain theory from ordertheoretic structures to category-theoretic ones has been considered before [19, 20, 1, 33, 2]. In particular, Lehmann [19, Chapter III] studied the solution of domain equations in a category of small categories with colimits of ω-chains, and noted that a version of the limit-colimit coincidence holds. Adámek [2] obtained similar results for a category of categorical analogue of Scott domains. In more generality and closer to our concerns here, Paul Taylor [33] proved the limit-colimit coincidence in the 2-category of small categories with filtered colimits, functors preserving these, and natural transformations. In some respects his work is a precursor to ours; however, we take a step further and develop an axiomatic theory in accordance with the approach to Axiomatic Domain Theory adopted in [6, 26, 8, 9]. Conceptually, the categorical theory of domains that we put forward maybe seen as the traditional theory of Smyth and Plotkin [30] where ω-cpos (ω-complete partial orders) are replaced with their categorical analogue (viz. small categories with colimits of ω-chains). Technically, this is not straightforward. For example, the consideration of categorical notions up to equivalence and coherent isomorphism has to be taken care of.

∗Research supported by BRICS and by EPSRC grant GR/J84205, Frameworks for Programming Language Semantics and Logic at LFCS, University of Edinburgh.

†Basic Research in Computer Science, Centre of the Danish National Research Foundation.

Organisation of the paper. In Section 1 we review some basic elements of 2-category theory. In Sections 2 and 3 we develop a 2-categorical theory of recursive domains. We present a generalisation of the limit-colimit coincidence and study algebraic compactness in a 2-categorical setting. In Section 4 we give an interpretation in Prof of recursive domains for concurrency. In Sections 5 and 6 we consider relational structures and provide a coinduction property based on bisimulation. In Section 7 we apply our theory to the study of open-map bisimulation. Finally, in Section 8, we discuss plans for future work.

1 Background

The theory developed in this paper is a theory for solving domain equations in certain 2-categories.

Enriched categories. A 2-category K consists of a collection of objects | K | and hom-categories K(A, B) for every A, B ∈ | K |, equipped with identity functors 1 → K(C, C) for every C ∈ | K |, and composition functors K(B, C) × K(A, B) → K(A, C) for every A, B, C ∈ |K|, subject to the usual laws (see [16]). As a convention, the action of the composition functors is denoted by juxtaposition. Also, for objects A, B ∈ | K |, objects and morphisms of the hom-category K(A, B) are respectively called morphisms and 2-cells of K; the latter are typically indicated by ‘⇒’. Invertible 2-cells are called pseudo cells. The paradigmatic example of a 2-category is Cat: the objects are small categories, the morphisms are functors, and the 2-cells are natural transformations.

We will be particularly interested in ωCat-categories (and ωCat_{0}-categories). These are 2-categories with the property that every hom-category has colimits of ω-chains (and an initial object) which are preserved by the composition functors. Examples of ωCat-categories are: Cpo (Cppo_{⊥}) —the objects are ω-cpos (ω-cppos), the morphisms are (strict) ω-continuous functions, and the 2-cells are given by the pointwise order— and ωCat (ωCat_{0}) — the objects are small categories with colimits of ω-chains (and an initial object), the morphisms are functors that preserve these colimits, and the 2-cells are natural transformations.

Concerning exactness properties in 2-categories we will focus on pseudo (co)limits (elsewhere bi(co)limits [31]). We exemplify this notion with the most basic example.

Pseudo initial object. An object 0 in a 2-category is said to be pseudo initial if it satisfies the following universal property:

1. For every object X, there exists an arrow 0 → X.

2. For every pair of arrows u, v : 0 → X there exists a unique 2-cell ξ : u ⇒ v.

The reason for considering this level of generality is that our applications range naturally within the class of bicategories [3] —see Section 8 for discussions. And, as remarked in [31, (1.18)], there are important 2-categories which admit certain pseudo colimits which are not 2-colimits. Even though the results presented here are in a 2-categorical setting, we aim at generalising them to a bicategorical one. This is possible using the coherence result stating that every bicategory is biequivalent to a 2-category; details will appear elsewhere.

Profunctors. We conclude this section with the definition of the ωCat_{0}-categories that will serve as our source of examples throughout the paper: Prof (Prof_{M}) has small categories ℂ as objects, morphisms 𝔸 [figure: +] 𝔹 are colimit (and mono) preserving functors 𝔸̂ → 𝔹̂ between the corresponding presheaf categories, and 2-cells are (monomorphic) natural transformations.

2 Local-characterisation theorem

We present a central result of the paper, namely a generalisation of the local characterisation of colimits of ω-chains of embeddings in Cpo-categories [30] which yields the limit-colimit coincidence [28]. We generalise in two directions. First, we move from the notion of embedding-projection pair in a Cpo-category (viz. coreflection, in the categorical jargon) to consider adjunctions in an ωCat-category (cf. [33, 29]). Next, for the reasons exposed above, we consider pseudo colimits rather than strict ones.

We start by recalling some definitions and fixing notation.

Adjunctions. Let K be a 2-category. We define K^{adj} to be the 2-category of adjunctions as follows. The objects of K^{adj} are those of K; whilst K^{adj}(A, B) is the category whose objects are tuples (η, ε : f ⊣ g : B → A), where f ⊣ g is an adjunction in K with unit η and counit ε, and a 2-cell (η, ε : f ⊣ g) ⇒ (η′, ε′ : f′ ⊣ g′) is given by a pair of 2-cells σ : f ⇒ f′ : A → B and τ : g ⇒ g′ : B → A in K, such that the diagrams

\xymatrix{1_{A} \ar@{=>}[r]^{η} \ar@{=>}[dr]_{η′} & gf \ar@{=>}[d]^{τσ} & fg \ar@{=>}[dr]^{ε} \ar@{=>}[d]_{στ} \\  & g′f′ & f′g′ \ar@{=>}[r]_{ε′} & 1_{B}}

commute. We write K^{cor} for the full sub-2-category of K^{adj} consisting of coreflections; i.e. tuples (η, ε : f ⊣ g) where η is a pseudo cell.

Pseudo cones. Let K be a 2-category. An ω-chain in K is given by an ω-indexed family of arrows ⟨f_{n} : A_{n} → A_{n+1}⟩. For l ≥ n, we write f_{n,l} : A_{n} → A_{l} for the inductively defined arrow f_{n,l+1} =^{def} f_{l}f_{n,l}, where f_{n,n} =^{def} 1_{A_{n}}. Similar definitions, with all arrows and indexes reversed, apply to ω^{op}-chains.

A pseudo cone for an ω-chain ⟨f_{n} : A_{n} → A_{n+1}⟩ is given by the following data: an object A, an ω-indexed family of arrows ⟨φ_{n} : A_{n} → A⟩, and an ω-indexed family of pseudo cells ⟨Φ_{n} : φ_{n+1}f_{n} ⟹^{∼} φ_{n}⟩. The dual definition describes pseudo cones for ω^{op}-chains.

Canonical cones. Let us spell out in elementary terms the notion of pseudo cone for an ω-chain in K^{adj}. A pseudo cone for the ω-chain ⟨η_{n}, ε_{n} : f_{n} ⊣ g_{n} : A_{n+1} ⟶ A_{n}⟩ in K^{adj} consists of: an object A, an ω-indexed family ⟨ι_{n}, ȷ_{n} : φ_{n} ⊣ γ_{n}⟩, and an ω-indexed family ⟨Φ_{n}, Γ_{n}⟩ of pseudo

cells Φ_{n} : φ_{n+1}f_{n} ⟹^{∼} φ_{n} and Γ_{n} : g_{n}γ_{n+1} ⟹^{∼} γ_{n} such

that the squares

I_{n} : \xymatrix{1_{A_{n}} \ar@{=>}[r]^{η_{n}} \ar@{=>}[d]_{ι_{n}} & g_{n}f_{n} \ar@{=>}[d]^{g_{n}ι_{n+1}f_{n}} \\ γ_{n}φ_{n} & g_{n}γ_{n+1}φ_{n+1}f_{n} \ar@{=>}[l]^{Γ_{n}Φ_{n}}}  (1)

J_{n} : \xymatrix{φ_{n}γ_{n} \ar@{=>}[d]_{ȷ_{n}} \ar@{=>}[r]^{Φ_{n}^{−1}Γ_{n}^{−1}} & φ_{n+1}f_{n}g_{n}γ_{n+1} \ar@{=>}[d]^{φ_{n+1}ε_{n}γ_{n+1}} \\ 1_{A} & φ_{n+1}γ_{n+1} \ar@{=>}[l]^{ȷ_{n+1}}} (2)

commute for all n.

It is important to observe that a pseudo cone for an ω-chain of adjunctions induces ω-chains in K(A_{n}, A_{n}) and K(A, A) with associated canonical cones. Indeed, let ⟨Φ_{n}, Γ_{n}⟩ be as above. Then we have the following cones

[figure: 1_{A_{n}}; I_{n}; g_{n}f_{n}; g_{n}I_{n+1}f_{n}; g_{n+2,n}f_{n,n+2}; ···; ⋯; γ_{n}φ_{n}; ⋯]

[figure: φ_{0}γ_{0}; J_{0}; φ_{1}γ_{1}; J_{1}; φ_{2}γ_{2}; ···; ⋯; 1_{A}]

obtained from the diagrams (1) and (2). We will indicate these cones as the canonical cones ⟨g_{l,n}f_{n,l}⟩_{l} \underrightarrow{.} γ_{n}φ_{n} and ⟨φ_{n}γ_{n}⟩ \underrightarrow{.} 1_{A}, respectively.

Pseudo colimits. A pseudo cone ⟨Φ_{n} : φ_{n+1}f_{n} ⟹^{∼} φ_{n} : A_{n} → A⟩ for an ω-chain ⟨f_{n} : A_{n} → A_{n+1}⟩ is said to be a pseudo colimit (elsewhere bicolimit [31]) if it satisfies the following universal property:

1. For every pseudo cone ⟨Ψ_{n} : ψ_{n+1}f_{n} ⟹^{∼} ψ_{n} : A_{n} → X⟩ there exists an arrow u : A → X and an ω-indexed family of pseudo cells ⟨μ_{n} : uφ_{n} ⟹^{∼} ψ_{n}⟩ such that the square

\xymatrix{uφ_{n+1}f_{n} \ar@{=>}[r]^{μ_{n+1}f_{n}} \ar@{=>}[d]_{uΦ_{n}} & ψ_{n+1}f_{n} \ar@{=>}[d]^{Ψ_{n}} \\ uφ_{n} \ar@{=>}[r]_{μ_{n}} & ψ_{n}}

commutes.

2. For every pair of arrows u, v : A → X and every ω-indexed family of 2-cells ⟨ξ_{n} : uφ_{n} ⇒ vφ_{n}⟩ satisfying

\xymatrix{uφ_{n+1}f_{n} \ar@{=>}[r]^{ξ_{n+1}f_{n}} \ar@{=>}[d]_{uΦ_{n}} & vφ_{n+1}f_{n} \ar@{=>}[d]^{vΦ_{n}} \\ uφ_{n} \ar@{=>}[r]_{ξ_{n}} & vφ_{n} & ,}

there exists a unique 2-cell ξ : u ⇒ v such that ξ_{n} = ξφ_{n}.

Central results. A generalisation of [30, Theorem 2] follows.

For a 2-category K, we define K≅ to be the sub-2-category of K consisting of the objects and morphisms of K with 2-cells given by the pseudo cells of K.

Theorem 2.1 (Local characterisation) In an ωCatcategory K, for an ω-chain of coreflections (adjunctions) ⟨f_{n} ⊣ g_{n} : A_{n+1} → A_{n}⟩ and a pseudo cone

⟨Φ_{n} : φ_{n+1}f_{n} ⟹^{∼} φ_{n} : A_{n} → A⟩ for the ω-chain

⟨f_{n} : A_{n} → A_{n+1}⟩, the following are equivalent:

1. ⟨Φ_{n} : φ_{n+1}f_{n} ⟹^{∼} φ_{n} : A_{n} → A⟩ is a pseudo colimit for ⟨f_{n} : A_{n} → A_{n+1}⟩ in K.

2. ⟨Φ_{n} : φ_{n+1}f_{n} ⟹^{∼} φ_{n} : A_{n} → A⟩ is a pseudo colimit for ⟨f_{n} : A_{n} → A_{n+1}⟩ in K≅.

3. There is a pseudo cone of coreflections (adjunctions)

(Φ_{n}, Γ_{n}) : (φ_{n+1} ⊣ γ_{n+1})(f_{n} ⊣ g_{n}) ⟹^{∼} (φ_{n} ⊣ γ_{n})

such that the canonical cone(s) ⟨φ_{n}γ_{n}⟩ \underrightarrow{.} id_{A} (and ⟨g_{l,n}f_{n,l}⟩_{l} \underrightarrow{.} γ_{n}φ_{n}) is (are) colimiting.

The above theorem and its dual, yield the following.

Corollary 2.2 (Limit-colimit coincidence) In an ωCatcategory, for an ω-chain of coreflections (adjunctions) ⟨f_{n} ⊣ g_{n} : A_{n+1} → A_{n}⟩ and a pseudo cone of coreflections (adjunctions) (Φ_{n}, Γ_{n}) : (φ_{n+1} ⊣ γ_{n+1})(f_{n} ⊣ g_{n}) ⟹^{∼} (φ_{n} ⊣ γ_{n}) the following are equivalent:

1. ⟨Φ_{n} : φ_{n+1}f_{n} ⟹^{∼} φ_{n} : A_{n} → A⟩ is a pseudo colimit for ⟨f_{n} : A_{n} → A_{n+1}⟩.

2. ⟨Γ_{n} : g_{n}γ_{n+1} ⟹^{∼} γ_{n} : A → A_{n}⟩ is a pseudo limit for ⟨g_{n} : A_{n+1} → A_{n}⟩.

This corollary seems to be part of the categorical folklore [32, 38].

Example. In Prof pseudo colimits of ω-chains of coreflections (adjunctions) can be calculated as follows. Let F_{n} :

𝔸_{n} [figure: ⊥; +; +] 𝔸_{n+1} : G_{n} be an ω-chain in Prof^{cor} (Prof^{adj}).

For every n, write E_{n} : 𝔸_{n} ↪ \overline{𝔸_{n}} for the embedding of the category 𝔸_{n} into its Cauchy completion \overline{𝔸_{n}} [18], and let E_{n}^{∗} : ˆ \overline{𝔸_{n}} ⟶^{≃} 𝔸̂_{n} denote the induced equivalence of categories. It is known (see, for example, [18, 3]) that there exist functors H_{n} : \overline{𝔸_{n}} → \overline{𝔸_{n+1}} such that F_{n} can be seen as a left Kan extension [21, 3, 16] as follows:

F_{n} ≅ Lan_{y_{n}}(E_{n+1}^{∗}H_{n}E_{n}) .

Let φ_{n} : \overline{𝔸_{n}} → 𝔸 be a colimit of the ω-chain ⟨H_{n} : \overline{𝔸_{n}} → \overline{𝔸_{n+1}}⟩ in Cat. Then, a pseudo colimit in Prof of the chain F_{n} : 𝔸_{n} [figure: +] 𝔸_{n+1} is given by a choice of left Kan extensions, along Yoneda embeddings, of the functors

𝔸_{n} [figure: E_{n}] \overline{𝔸_{n}} ⟶^{φ_{n}} 𝔸 ⟶^{y_{𝔸}} 𝔸̂.

The above construction also yields pseudo colimits of ω-chains of coreflections in Prof_{M}.

3 Pseudo-algebraic compactness

Algebraic compactness is a universal property due to Freyd [10] that provides canonical interpretations of recursive types. In this section we show this property for socalled Kcats; these may be seen as a 2-categorical analogue of ω-cppos (ω-complete pointed partial orders). Following [6], our approach is to obtain the result from the Local-Characterisation and Limit-Colimit Coincidence Theorems, together with the Basic Lemma [30]. Recall that the Basic Lemma provides conditions under which an initial algebra (and hence a fixed-point, by a lemma due to Lambek) of an endofunctor can be obtained as a colimit of the ω-chain constructed by iterating the endofunctor on an initial object.

We start by providing a version of the Basic Lemma for pseudo endofunctors on 2-categories.

Pseudo functors. Roughly speaking, pseudo functors between 2-categories are 2-categorical mappings for which functoriality is only required to hold up to coherent isomorphism. More precisely, a pseudo functor (pseudo ωCatfunctor) T : K → K′ between 2-categories (ωCatcategories) is given by a mapping T : | K | → | K′ | and actions T_{A,B} : K(A, B) → K′(T A, T B) in Cat (ωCat) for all A, B ∈ | K | together with coherent pseudo cells 1_{T C} ⟹^{∼} T_{C,C}(1_{C}) for all C ∈ | K |, and

T_{B,C}(g)T_{A,B}(f) ⟹^{∼} T_{A,C}(gf) for all A ⟶^{f} B ⟶^{g} C in

K.

Pseudo initial algebra. By a pseudo initial algebra for a pseudo functor T on a 2-category K, we mean an algebra a : T A → A satisfying the following universal property:

1. For every algebra x : T X → X there exists (it(x), ι)

as in

\xymatrix{T A \ar[r]_{≅^{ι}}^{a} \ar[d]_{T (it(x))} & A \ar[d]^{it(x)} \\ T X \ar[r]_{x} & X & .}

2. For every

\xymatrix{T A \ar[r]_{≅^{μ}}^{a} \ar[d]_{T u} & A \ar[d]^{u} & T A \ar[r]_{≅^{ν}}^{a} \ar[d]_{T v} & A \ar[d]^{v} \\ T X \ar[r]_{x} & X & T X \ar[r]_{x} & X}

there exists a unique 2-cell ξ : u ⇒ v such that

[figure: T A; ≅^{μ}; a; T u; A; u; v; ⇒^{ξ}; T X; x; X] = \xymatrix{T A \ar[r]_{≅^{ν}}_{⇒^{T ξ}}^{a} \ar[d]^{T v} \ar[d]_{T u} & A \ar[d]^{v} \\ T X \ar[r]_{x} & X}

Notice that pseudo initial algebras are equivalences.

Lemma 3.1 (Pseudo basic lemma) Let K be a 2-category with pseudo initial object 0 and let T : K → K be a pseudo functor. For ⊥ : 0 → T 0 consider the ω-chain ⟨T^{n}⊥ :

T^{n}0 → T^{n+1}0⟩ and let Φ_{n} : φ_{n+1}f_{n} ⟹^{∼} φ_{n} : T^{n}0 → A

be a pseudo colimit for it.

If Φ′_{n} : T (φ_{n+1})T (f_{n}) ⟹^{∼} T (φ_{n+1}f_{n}) ⟹^{T Φ_{n}} T φ_{n} :

T^{n+1}0 → T A is a pseudo colimit of the ω-chain ⟨T^{n+1}⊥ : T^{n+1}0 → T^{n+2}0⟩ and a : T A → A mediates between the pseudo cones ⟨Φ′_{n}⟩ and ⟨Φ_{n+1}⟩, then a is a pseudo initial T -algebra.

Kcats. A Kcat (cf. [6, Definition 7.3.11]) is an ωCat_{0}- category with pseudo initial object and pseudo colimits of ω-chains of coreflections.

There are a plentiful of Kcats. For example, Pfn (the category of sets and partial functions, with hom-sets ordered by graph inclusion), Rel (the category of sets and relations, with hom-sets ordered by inclusion), pCpo (the category of ω-cpos and partial ω-continuous functions, with hom-sets ordered pointwise), Prof, and Prof_{M}. Moreover, Kcats are closed under duals and products.

From Theorem 2.1, Corollary 2.2, and Lemma 3.1, we can deduce pseudo-algebraic compactness (see [11, 6]).

Corollary 3.2 (Pseudo-algebraic compactness) Kcats are pseudo-algebraically compact with respect to pseudo ωCat-functors.

Thus, every pseudo ωCat-functor T : K^{op} × K → K on a Kcat K has a free pseudo dialgebra T (A, A) ≃ A characterised by the following universal property: for every x′ : X′ → T (X, X′) and x : T (X′, X) → X, we have

\xymatrix{X′ \ar[r]_{≅}^{x′} \ar[d]_{coit(x′,x)} & T (X, X′) \ar[d]^{T (it(x′,x),coit(x′,x))} \\ A \ar[r]^{≃} & T (A, A) \\ T (A, A) \ar[r]_{≅}^{≃} \ar[d]_{T (coit(x′,x),it(x′,x))} & A \ar[d]^{it(x′,x)} \\ T (X′, X) \ar[r]_{x} & X}

given uniquely up to canonical coherent isomorphism (as defined for pseudo initial algebras).

4 Recursive domains for concurrency

As an application of the theory of Sections 2 and 3, we sketch the interpretation in Prof of types given by the following grammar

\begin{aligned}t & ::= & 0 | 1 | t ⊕ t′ | t ⊗ t′ | t^{∗} | !t | \\ & & ϑ | ∑_{i∈I} t_{i} | t_{⊥} | μϑ.t . \end{aligned}

These types are that of compact closed categories extended with type variables (ϑ), arbitrary sums (∑), a lifting operator ((−)_{⊥}), and a recursive-type constructor (μ).

As usual in compact closed categories, linear implication is definable from ⊗ and (−)^{∗} as t ⊸ t′ =^{def} t^{∗} ⊗ t′.

Interpretation. For a list of distinct type variables Θ, we write Θ ⊢ t to indicate that t is a well-formed type with free type variables amongst those in Θ. Type judgements Θ ⊢ t are interpreted as pseudo ωCat-functors

[[Θ ⊢ t]] : (Prof^{op} × Prof)^{|Θ|} → Prof ,

where |Θ| is the length of the list Θ, according to the following interpretation of constants and type constructors. Zero: 0, the initial category. One: 1, the terminal category.

Sum: ⊕ is interpreted by the pseudo ωCat-functor + : Prof × Prof → Prof that takes two categories to their disjoint union. Arbitrary sums ∑_{I}, indexed by a set I, are defined similarly —the binary sum ⊕ and the empty sum 0 are special cases. Tensor: ⊗ is interpreted by the pseudo ωCat-functor, ⊗ : Prof × Prof → Prof mapping two categories to their product. Dualizer: The dualizer (−)^{∗} is the pseudo ωCat-functor Prof^{op} → Prof that associates a category with its dual. Exponential: Our choice for the ! operator (see [36, 4] for motivations) is the pseudo ωCat-functor Prof → Prof sending a category to its free finite-colimit completion. Variables: Are interpreted as projections. Lifting: The pseudo ωCat-functor (−)_{⊥} : Prof → Prof extends any small category by adding a new strict initial object (typically denoted ⊥) to it. Recursive-type constructor: We use the results of Section 3, and take parameterised free pseudo dialgebras (see [6]).

We remark that the interpretation of zero, one, sums, tensors, duals, lifting, and recursive types in Prof restricts to Prof_{M}. This fact will be used in Subsection 7.1.

5 Relational structures

We consider relational structures [22, 24] in the spirit of categorical logic [17] (cf. [12]). A relational structure R on an ωCat_{0}-category K induces an ωCat_{0}-category of relations {K | R} with objects {C | R} given by an object C of K together with a relation R on it, maps are required to be parametric (i.e. relation preserving). Our main result here is that the category of relations {K|R} on a Kcat K is a again a Kcat.

Our intent is to consider relational structures on Prof_{M} and Prof, and use the induced categories of relations to study bisimulation. This is carried out in Section 7, after a brief study of coinduction and bisimulation in relational structures done in Section 6.

Relational structures. A relational structure on a category C is a functor C^{op} → (CPPO_{⊥})^{∘}, where (CPPO_{⊥})^{∘} is the category of possibly large posets P such that P^{op} is pointed and ω-complete, and monotone functions f : P → Q such that f^{op} : P^{op} → Q^{op} is strict and ω-continuous.

An admissible relational structure R on an ωCat_{0}- category K is a relational structure on the ordinary category underlying K, such that

1. for a pair of morphisms f, g : A → B, if f ≅ g then R(f) = R(g);

2. for a morphism f : A → B and an element S ∈ R(B), if f is initial in K(A, B) then R(f)(S) = ⊤_{R(A)}; 3. for an ω-chain ⟨f_{n}⟩ in K(A, B) with colimit f : A →

B,

R ⊂ R(f_{n})(S), for all n, implies R ⊂ R(f)(S)

for all R ∈ R(A) and S ∈ R(B).

Our admissible relational structures on a Cppo_{⊥}- category are (slightly weaker than) Pitts’ relational structures admitting inverse images and intersections in which every relation is admissible (as defined in [24]).

Examples. We have the following admissible relational structures.

1. Admissible extensional relations on Prof_{M}: Ext is defined as follows.

For every small category ℂ, Ext(ℂ) is the complete meet semilattice of relations R ⊆ |ℂ̂^{2} | such that

(a) X′ ≅ X R Y ≅ Y′ implies X′ R Y′;

(b) 0 R 0;

(c) for every pair of ω-chains of monomorphisms X⃗ and Y⃗ with colimits X and Y respectively,

if X⃗_{n} R Y⃗_{n}, for all n, then X R Y.

These relations are ordered by inclusion.

The action of Ext on morphisms is by inverse image.

2. Admissible intensional relations on Prof: Int is defined as follows.

For every small category ℂ, Int(ℂ) is the complete meet semilattice of intensional relations R ⊆ |ℂ̂^{↙↘} | such that

(a) for every triple of isomorphisms W ≅ W′, X ≅ X′, and Y ≅ Y′,

(X ← W → Y) ∈ R implies (X′ ≅

X ← W ⟵^{≅} W′ ⟶^{≅} W → Y ≅ Y′) ∈

R;

(b) (0 ← 0 → 0) ∈ R;

(c) for every span of natural transformations X⃗ ⟸^{p} W⃗ ⟹^{q} Y⃗ where X⃗, W⃗, and Y⃗ are ω-chains with colimits X, W, and Y respectively,

if (X⃗_{n} ⟵^{p_{n}} W⃗_{n} ⟶^{q_{n}} Y⃗_{n}) ∈ R, for all n,

then \xymatrix{(X & W \ar[l]_{colim p} \ar[r]^{colim q} & Y) ∈ R.}

These intensional relations are ordered by inclusion.

The action of Int on morphisms is by inverse image.

3. Every relational structure R on Prof induces a relational structure R^{∗} on Prof^{op} with

R^{∗}(ℂ) =^{def} R(ℂ^{∗}) and R^{∗}(F) =^{def} R(F^{∗}) .  (3)

With respect to a relational structure R, for f : A → B, we write f : R ⊂ S (where R ∈ R(A) and S ∈ R(B)) whenever R ⊂ R(f)(S). Hence, for the above examples we have that, for F ∈ Prof(𝔸, 𝔹),

1. F : R ⊂_{Ext} S (where R ∈ Ext(𝔸) and S ∈ Ext(𝔹)) if and only if (X, Y) ∈ R implies (F X, F Y) ∈ S;

2. F : R ⊂_{Int} S (where R ∈ Int(𝔸) and S ∈ Int(𝔹)) if and only if (X ← W → Y) ∈ R implies (F X ← F W → F Y) ∈ S; and

3. F : S ⊂_{Int}^{∗} R (where S ∈ Int(𝔹^{op}) and R ∈ Int(𝔸^{op})) if and only if (X ← W → Y) ∈ S implies (F^{∗}X ← F^{∗}W → F^{∗}Y) ∈ R.

Category of relations. Let R be an admissible relational structure on an ωCat_{0}-category K. The ωCat_{0}-category of relations {K | R} has: objects given by pairs {C | R} with C ∈ | K | and R ∈ R(C); hom-categories {K | R}({A | R}, {B | S}) defined as the full subcategory of K(A, B) consisting of all those f such that f : R ⊂ S; and identities and compositions given as in K.

The forgetful functor {K | R} → K is faithful and ωCat_{0}-enriched.

Theorem 5.1 Let R be an admissible relational structure on an ωCat_{0}-category K. The forgetful ωCat_{0}-functor {K | R} → K creates pseudo initial objects and pseudo colimits of ω-chains of coreflections.

Proof: Let 0 be a pseudo initial object in K. Then, the object {0 | ⊤_{R(0)}} is pseudo initial in {K | R} because {K|R}({0|⊤_{R(0)}}, {C |R}) = K(0, C).

Let f_{n} : {C_{n} | R_{n}} [figure: ⊥]{C_{n+1} | R_{n+1}} : g_{n} be an ω-chain of coreflections in {K | R}, and let Φ_{n} : φ_{n+1}f_{n} ⟹^{∼} φ_{n} : C_{n} → C be a pseudo colimit of f_{n} : C_{n} → C_{n+1} in K.

Since f_{n} : C_{n} [figure: ⊥]C_{n+1} : g_{n} is an ω-chain of coreflections in K, it follows by the local-characterisation theorem (in K) that there exists a pseudo cone of coreflections

(Φ_{n}, Γ_{n}) : (φ_{n+1} ⊣ γ_{n+1})(f_{n} ⊣ g_{n}) ⟹^{∼} (φ_{n} ⊣ γ_{n}) such

that the associated canonical cone ⟨φ_{n}γ_{n}⟩ \underrightarrow{.} 1_{A} is colimiting.

Thus, to show that the forgetful ωCat_{0}-functor {K | R} → K creates ω-chains of coreflections it is enough, by the local-characterisation theorem (in {K | R}), to find an R ∈ R(C) such that, for all n, φ_{n} : R_{n} ⊂ R and γ_{n} : R ⊂ R_{n}.

To conclude the proof we observe that {R(γ_{n})(R_{n})} is an ω^{op}-chain in R(C), and that R = ⋀⟨R(γ_{n})(R_{n})⟩ satisfies the above requirements. □

Corollary 5.2 For an admissible relational structure R on a Kcat K, the category of relations {K|R} is a Kcat.

It follows that {Prof_{M} | Ext}, {Prof^{op} | Int^{∗}}, and {Prof |Int} are Kcats.

6 Coinduction and bisimulation

As an application of Theorem 5.1, we present induction and coinduction principles for recursive domains [24, 12]. From it, we derive a coinduction property based on bisimulation which will be important in Section 7.

6.1 Covariant case

Proposition 6.1 Let R be an admissible relational structure on a Kcat K. Consider pseudo ωCat-functors T and T^{#} such that the diagram

\xymatrix{\{K|R\} \ar[d]_{U} \ar[r]^{T^{#}} & \{K|R\} \ar[d]^{U} \\ K \ar[r]_{T} & K}

commutes, where U denotes the forgetful ωCat_{0}-functor. Then, for every free pseudo T -algebra

fd : T (D) ≃ D : ud

there exists (a necessarily unique) Δ ∈ R(D) such that

fd : T^{#}({D |Δ}) ≃ {D |Δ} : ud

is a free pseudo T^{#}-algebra.

Induction and coinduction. In the situation of the above proposition, let

T^{#}({A|R}) = (T (A), T_{R}(R)) .

Then, Δ ∈ R(D) satisfies the following rules [24, 12]:

• For a : T A → A and R ∈ R(A),

\frac{a : T_{R}(R) ⊂ R}{it(a) : Δ ⊂ R}

• For z : Z → T Z and R ∈ R(Z),

\frac{z : R ⊂ T_{R}(R)}{coit(z) : R ⊂ Δ}

Bisimulation. Define a T^{#}-bisimulation to be an R ∈ R(D) such that

ud : R ⊂ T_{R}(R) .

Then, Δ is a T^{#}-bisimulation. Moreover, free pseudo algebras satisfy the following coinduction property (cf. [23, 24, 7, 12]):

Δ = ⋁{R ∈ R(D) | R is a T^{#}-bisimulation} .

6.2 Mixed-variance case

To treat the mixed-variance case we consider involutory 2-categories (viz. 2-categories which are self dual via an involution —see [6]). Formally, these are 2-categories K equipped with a pseudo functor O : K^{op} → K such that O ∘ O^{op} ≅ Id_{K}.

Let (K, O) be an involutory Kcat. Every admissible relational structure R on K induces an admissible relational structure R^{O} on K^{op} with R^{O}(C) =^{def} R(OC) and

R^{O}(f) =^{def} R(Of) (cf. (3)).

Proposition 6.2 Let (K, O) be an involutory Kcat, and let R be an admissible relational structure on K. Consider pseudo ωCat-functors T : K^{op} × K → K and T^{#} such that the diagram

\xymatrix{\{K^{op} |R^{O}\} × \{K|R\} \ar[r]^{T^{#}} \ar[d]_{U′×U} & \{K^{op} |R^{O}\} × \{K|R\} \ar[d]^{U′×U} \\ K^{op} × K \ar[r]_{T̆} & K^{op} × K}

commutes, where T̆(C′, C) =^{def} (T (C, C′), T (C′, C)) and U′, U denote forgetful ωCat_{0}-functors. Then, for every free pseudo T -dialgebra

fd : T (D, D) ≃ D : ud

there exist (necessarily unique) Δ′ ∈ R(OD) and Δ ∈ R(D) such that

(ud, fd) : T^{#}({D |Δ′}, {D |Δ}) ≃ ({D |Δ′}, {D |Δ}) : (fd, ud)

is a free pseudo T^{#}-algebra.

Induction and coinduction. In the situation of the above proposition, let

\begin{matrix}T^{#}(\{A′ |R′\}, \{A|R\}) \\ = (\{T (A, A′)|T′_{R}(R′, R)\}, \{T (A′, A)|T_{R}(R′, R)\}) . \end{matrix}

Then, Δ′ ∈ R(OD) and Δ ∈ R(D) satisfy the following rules:

• For a′ : A′ → T (A, A′), a : T (A′, A) → A, R′ ∈ R(OA′), R ∈ R(A),

\frac{O(a′) : T′_{R}(R′, R) ⊂ R′ a : T_{R}(R′, R) ⊂ R}{O(coit(a′, a)) : Δ′ ⊂ R′ it(a′, a) : Δ ⊂ R}

• For z′ : T (Z, Z′) → Z′, z : Z → T (Z′, Z), R′ ∈ R(OZ′), R ∈ R(Z),

\frac{O(z′) : R′ ⊂ T′_{R}(R′, R) z : R ⊂ T_{R}(R′, R)}{O(it(z, z′)) : R′ ⊂ Δ′ coit(z, z′) : R ⊂ Δ}

Bisimulation. Define a T^{#}-bisimulation to be a pair (R′, R) ∈ R(OD) × R(D) such that

O(fd) : R′ ⊂ T′_{R}(R′, R) and ud : R ⊂ T_{R}(R′, R) .

Then, the pair (Δ′, Δ) is a T^{#}-bisimulation. Moreover, free pseudo algebras satisfy the following coinduction property:

(Δ′, Δ) = ⋁{(R′, R) | (R′, R) is a T^{#}-bisimulation} .

7 Open-map bisimulation

We provide models of parts of the type theory of Section 4 in the Kcats of relations {Prof_{M} |Ext} and {Prof | Int}. In these models, the denotation of a type provides a model for concurrency (in the form of a presheaf category [5]) equipped with a relation. The presheaf models so obtained coincide with those of Section 4, whilst the relations will be shown to be in accordance with open-map bisimulation (viz. the relation holding between presheaves that are connected by a surjective open span). Thus, by the results of the previous section, we may use coinduction principles to reason about open-map bisimulation.

7.1 Extensional relations

In constructing relations within the relational structure Ext we restrict to the types built up from arbitrary sums, lifting, discrete function space, and recursion, as follows:

t ::= ϑ | ∑_{i∈I} t_{i} | t_{⊥} | 𝕍 ⊸ t | μϑ.t .  (4)

The constant 𝕍 ranges over discrete small categories. I is an indexing set, possibly empty, in which case the sum is understood as the zero object 0. The interpretation of a type Θ ⊢ t determines a pseudo ωCat-functor

[[Θ ⊢ t]] : Prof_{M}^{|Θ|} → Prof_{M} .

Each such pseudo ωCat-functor extends to a pseudo ωCat-functor on extensional relations

E[[Θ ⊢ t]] : {Prof_{M} |Ext}^{|Θ|} → {Prof_{M} |Ext} ;

it suffices to show how sum, lifting, and discrete function space extend.

Sums: Consider a presheaf X over ∑_{i∈I} 𝔸_{i}. Its projection (X)_{i}, for i ∈ I, is the presheaf obtained as the restriction of X to 𝔸_{i}. Define

∑_{i∈I}{𝔸_{i} |R_{i}} =^{def} {∑_{i∈I} 𝔸_{i} |R}

where

X R Y ⟺^{def} ∀i ∈ I. (X)_{i} R_{i} (Y)_{i} .

It is easy to check that this extension is well-defined and that

(∀i ∈ I. F_{i} : R_{i} ⊂ S_{i}) ⇒ ∑_{i∈I} F_{i} : ∑_{i∈I} R_{i} ⊂ ∑_{i∈I} S_{i} .

Lifting: Consider a presheaf X over 𝔸_{⊥}. It decomposes into a sum

X ≅ ∑_{x∈X(⊥)} u_{∗}(X_{|x})  (5)

where each presheaf X_{|x} in 𝔸̂ is the component subtended from the element x as detailed in [36], and u_{∗} is the functor that puts a root to a presheaf. For X′ ∈ 𝔸̂, write

X ^{\underline{⊥}}→ X′

when there is x ∈ X(⊥) such that X′ = X_{|x}.

The “obvious” way to extend lifting to relations is, given a relation R between presheaves over 𝔸 to define (R)_{⊥}^{0} a relation between presheaves over 𝔸_{⊥} by taking: X (R)_{⊥}^{0} Y iff

\begin{matrix}∀X′. X ^{\underline{⊥}}→ X′ ⇒ ∃Y′. Y ^{\underline{⊥}}→ Y′ & X′ R Y′, \\ ∀Y′. Y ^{\underline{⊥}}→ Y′ ⇒ ∃X′. X ^{\underline{⊥}}→ X′ & X′ R Y′ . \end{matrix}

But, unfortunately, the relation (R)_{⊥}^{0} may fail to satisfy the ω-admissibility requirement (c) in the definition of admissible extensional relations even though R lies in Ext(𝔸). We thus define X (R)_{⊥} Y iff there are ω-chains of monomorphisms X⃗, Y⃗ with colimits X and Y respectively for which X⃗_{n} (R)_{⊥}^{0} Y⃗_{n} for all n ∈ ω. Finally we define

({𝔸|R})_{⊥} =^{def} {𝔸_{⊥} |(R)_{⊥}} .

Suppose F : R ⊂ S in {Prof_{M} | Ext}. Then from F being colimit, and so sum, preserving, it follows that (F)_{⊥} : (R)_{⊥} ⊂ (S)_{⊥}.

Locally-finite presheaves. A presheaf X over a small category ℂ is said to be locally finite if, for every object C of ℂ, the set X(C) is finite.

On locally finite presheaves, open-map bisimilarity satisfies an ω-admissibility property.

Lemma 7.1 Let ℂ be a small category. Let X⃗ and Y⃗ be two ω-chains of monomorphisms in ℂ̂ with colimits X and Y respectively. For locally finite X and Y, if X⃗_{n} and Y⃗_{n} are open-map bisimilar, for all n, then so are X and Y.

This result generalises to larger cardinals, in the sense that the statement is still valid if, for any n ∈ ω, one replaces ω-chains with ω_{n+1}-chains and assumes X and Y to be locally of size ω_{n}. We remark that the assumption that the ω-chains consist of monomorphisms is crucial; hence our restriction to Prof_{M} when considering extensional relations.

By a proof reminiscent of Lemma 7.1, we can show that the two relations (R)_{⊥}^{0} and (R)_{⊥} coincide on locally finite presheaves.

Lemma 7.2 Let X, Y be locally finite presheaves over 𝔸_{⊥}. Suppose the ω-chains of monomorphisms X⃗, Y⃗ have colimits X and Y respectively. Then,

(∀n ∈ ω. X⃗_{n} (R)_{⊥}^{0} Y⃗_{n}) ⇒ X (R)_{⊥}^{0} Y .

Consequently,

X (R)_{⊥}^{0} Y ⇔ X (R)_{⊥} Y .

Discrete function space: A presheaf X over 𝕍 ⊸ 𝔸 corresponds to a functor 𝕍 → 𝔸̂, and we write Xv for the presheaf in 𝔸 resulting from the functor’s application to v ∈ 𝕍. Define

(𝕍 ⊸ {𝔸|R}) =^{def} {(𝕍 ⊸ 𝔸)|(𝕍 ⊸ R)}

where

X (𝕍 ⊸ R) Y ⟺^{def} (∀v ∈ 𝕍. (Xv) R (Y v)) .

This extension is well-defined and such that

F : R ⊂ S ⇒ (𝕍 ⊸ F) : (𝕍 ⊸ R) ⊂ (𝕍 ⊸ S) .

Thus by structural induction any closed type t in the grammar (4) is associated with an extensional relation ≈_{t}^{Ext} ∈ Ext([[t]]). Recursive types μϑ.t are interpreted as parameterised free pseudo algebras in the Kcat {Prof_{M} | Ext}; specialising the pseudo-colimit construction of the Pseudo Basic Lemma (using Theorem 5.1).

The relation ≈_{t}^{Ext} coincides with open-map bisimulation on locally finite presheaves.

Theorem 7.3 Let t be a closed type in the grammar (4). Let X, Y be locally finite presheaves over [[t]]. Then, X ≈_{t}^{Ext} Y iff X and Y are open-map bisimilar.

Proof: The proof proceeds by structural induction on t. Write OK{𝔸 | S} when a relation {𝔸 | S} in {Prof_{M} | Ext} satisfies the condition that on locally finite presheaves X, Y over 𝔸

X S Y ⇔ X, Y are open-map bisimilar .

As the induction hypothesis, on type judgement ϑ_{1}, ⋯, ϑ_{k} ⊢ t, we take

\begin{matrix}OK\{𝔸_{1} |S_{1}\} & ⋯ & OK\{𝔸_{k} |S_{k}\} \\ ⇒ OK([[ϑ_{1}, ⋯, ϑ_{k} ⊢ t]]\{𝔸_{1} |S_{1}\} ⋯ \{𝔸_{k} |S_{k}\}) . \end{matrix}

It can be checked that each of the constructions lifting, sum, and discrete function space preserve the OK property on relations. This covers all cases of the induction but for recursive types.

Consider the relation interpreting a recursively-defined type

[[Θ ⊢ μϑ.t]]{𝔸_{1} |S_{1}} ⋯ {𝔸_{|Θ|} |S_{|Θ|}}

in the environment where we assume

OK{𝔸_{1} |S_{1}} & ⋯ & OK{𝔸_{|Θ|} |S_{|Θ|}} .

The relation is a pseudo colimit {𝔻 | R} of the ω-chain

{𝔻_{n} |R_{n}} where {𝔻_{0} |R_{0}} =^{def} {0|{(0, 0)}} and

\begin{matrix}\{𝔻_{n+1} |R_{n+1}\} \\ =^{def} [[Θ, ϑ ⊢ t]]\{𝔸_{1} |S_{1}\} ⋯ \{𝔸_{|Θ|} |S_{|Θ|}\}\{𝔻_{n} |R_{n}\} . \end{matrix}

Using the structural induction hypothesis, an induction on n shows that OK{𝔻_{n} | R_{n}} at each stage n. Suppose X R Y. Projecting, we have γ_{n}X R_{n} γ_{n}Y at each n. Each γ_{n}X, γ_{n}Y is also locally finite (γ_{n} being part of a coreflection in Prof_{M}). Thus γ_{n}X, γ_{n}Y are open-map bisimilar over 𝔻_{n}. Injecting, we obtain ω-chains of monomorphisms ⟨X_{n}⟩, ⟨Y_{n}⟩ in 𝔻̂ with pseudo colimits X and Y. But maps in Prof_{M} preserve open-map bisimilarity, so X_{n} and Y_{n} are open-map bisimilar for each n. We now meet the conditions of Lemma 7.1, from which we conclude that X and Y are open-map bisimilar. □

From the above and the results of Subsection 6.1 we obtain the following characterisation.

Corollary 7.4 Let ϑ ⊢ t be a type in the grammar (4), and let E[[ϑ ⊢ t]] : {Prof_{M} | Ext} → {Prof_{M} | Ext} be its interpretation as sketched above. Then, for presheaves X, Y over [[μϑ.t]], the following are equivalent:

• X ≈_{μϑ.t}^{Ext} Y.

• X and Y are E[[ϑ ⊢ t]]-bisimilar.

Thus, for locally finite X and Y, a further equivalent statement is:

• X and Y are open-map bisimilar.

Strong bisimulation. Let ℙ = μϑ.T where T ϑ = (ϑ)_{⊥}. Presheaves over ℙ correspond to trees and ≈_{ℙ}^{Ext} to an ω-admissible version of Park and Milner’s strong bisimulation. It specialises to the usual strong bisimulation on locally finite presheaves (i.e. finitely branching trees). Further, by Corollary 7.4, a T_{Ext}-bisimulation between locally finite presheaves is a strong bisimulation.

Late bisimulation. A domain for value-passing with “late” semantics is obtained as ℙ = μϑ.T where

T ϑ = ϑ_{⊥} + ∑_{a∈Chan, v∈𝕍} ϑ_{⊥} + ∑_{a∈Chan}(𝕍 ⊸ ϑ)_{⊥}

with sums over channels Chan and values 𝕍. A T_{Ext}- bisimulation between locally finite presheaves is a late bisimulation on presheaves in the sense of [36] which is there shown to coincide with open-map bisimulation. Here this result follows from Corollary 7.4. Fortuitously the process language of [36] allows only guarded recursive definitions of processes, so that all process terms denote locally finite presheaves over ℙ. Consequently the relation ≈_{ℙ}^{Ext} holds between denotations of closed terms iff they are latebisimilar in the traditional sense.

Remark. Our treatment thus coincides with that usually adopted in operational semantics of process languages provided we restrict to “finitely branching” processes whose denotations are locally finite presheaves. We expect that we could extend the treatment to “countably branching” processes whose denotations are locally countable presheaves if we generalise the results here from ω-colimits to ω_{1}-colimits. This would follow the pioneering work on countable nondeterminism described in [25]. Of course an even greater degree of branching would require even larger cardinals.

7.2 Intensional relations

We consider the following extension of the grammar in (4):

t ::= ϑ | ∑_{i∈I} t_{i} | t_{⊥} | μϑ.t | t ⊗ t′ | t^{∗}  (6)

obtained by adding tensors and duals, and give an interpretation of these types as pseudo ωCat-functors

I[[Θ ⊢ t]] : ({Prof^{op} |Int^{∗}} × {Prof |Int})^{|Θ|} → {Prof^{op} |Int^{∗}} × {Prof |Int} .

Again, it suffices to show how sums, lifting, tensor, and the dualizer extend to pseudo ωCat-functors.

Sums: For an I-indexed family of relations ⟨R_{i} ∈ Int(𝔸_{i})⟩ we define ∑_{i∈I} R_{i} ∈ Int(∑_{i∈I} 𝔸_{i}) as follows. A span X ⇐ W ⇒ Y is in ∑_{i∈I} R_{i} iff, for every i ∈ I, the restriction (X)_{i} ⇐ (W)_{i} ⇒ (Y)_{i} is in R_{i}.

The interpretation of ∑_{I} is the pseudo ωCat-functor ({Prof^{op} | Int^{∗}} × {Prof | Int})^{|I|} → {Prof^{op} | Int^{∗}} × {Prof | Int} sending ⟨{𝔸′_{i} | R′_{i}}, {𝔸_{i} | R_{i}}⟩ to {∑_{i∈I} 𝔸′_{i} | ∑_{i∈I} R′_{i}}, {∑_{i∈I} 𝔸_{i} |∑_{i∈I} R_{i}}.

Lifting: Consider presheaves W and X over 𝔸_{⊥}. As we have already remarked in (5), they decompose as W ≅ ∑_{w∈W (⊥)} u_{∗}(W_{|w}) and X ≅ ∑_{x∈X(⊥)} u_{∗}(X_{|x}), where the W_{|w}’s and X_{|x}’s are presheaves over 𝔸. It follows that to give a natural transformation p : W ⇒ X in 𝔸̂_{⊥} is to give a W (⊥)-indexed family of natural transformations ⟨p_{|w} : W_{|w} ⇒ X_{|p_{⊥}(w)}⟩ in 𝔸̂. Then, for R ∈ Int(𝔸), we define (R)_{⊥} ∈ Int(𝔸_{⊥}) as follows. A span X ⟸^{p} W ⟹^{q} Y is in (R)_{⊥} iff the span X(⊥) ⟵^{p_{⊥}} W (⊥) ⟶^{q_{⊥}} Y (⊥) consists of surjections and, for every w ∈ W (⊥), the span

X_{|p_{⊥}(w)} ⟸^{p_{|w}} W_{|w} ⟹^{q_{|w}} Y_{|q_{⊥}(w)} is in R.

Moreover, for R ∈ Int(𝔸^{op}), we define (R)^{⊤} ∈ Int((𝔸_{⊥})^{op}) as follows. A span X ⇐ W ⇒ Y is in (R)^{⊤} iff, writing N for the canonical inclusion 𝔸 ↪ 𝔸_{⊥}, the span XN ⇐ W N ⇒ Y N is in R and if, for all A ∈ | 𝔸 |, the commutative squares

\xymatrix{X(⊥) \ar[d] & W (⊥) \ar[l] \ar[d] & W (⊥) \ar[d] \ar[r] & Y (⊥) \ar[d] \\ X(A) & W (A) \ar[l] & W (A) \ar[r] & W (A)}

are quasi-pullbacks.

Finally, the interpretation of (−)_{⊥} is the pseudo ωCatendofunctor on {Prof^{op} | Int^{∗}} × {Prof | Int} sending {𝔸′ |R′}, {𝔸|R} to {𝔸′_{⊥} |(R′)^{⊤}}, {𝔸_{⊥} |(R)_{⊥}}. Tensor: Let R ∈ Int(𝔸) and S ∈ Int(𝔹). A span X ⇐ W ⇒ Y in { \atop 𝔸 ⊗ 𝔹} is defined to be in R ⊗ S iff, for every A ∈ |𝔸|,

X(A, −) ⇐ W (A, −) ⇒ Y (A, −) is in S

and, for every B ∈ |𝔹|,

X(−, B) ⇐ W (−, B) ⇒ Y (−, B) is in R .

The interpretation of ⊗ is the pseudo ωCat-functor ({Prof^{op} | Int^{∗}} × {Prof | Int})^{2} → {Prof^{op} | Int^{∗}} × {Prof | Int} sending {𝔸′ | R′}, {𝔸 | R}; {𝔹′ | S′}, {𝔹 | S} to {𝔸′ ⊗ 𝔹′ |R′ ⊗ S′}, {𝔸 ⊗ 𝔹|R ⊗ S}.

Dualizer: The interpretation of (−)^{∗} is the pseudo ωCatendofunctor on {Prof^{op} | Int^{∗}} × {Prof | Int} sending {𝔸′ |R′}, {𝔸|R} to {𝔸^{∗} |R}, {𝔸^{′∗} |R′}.

Thus every closed type t in the grammar (6) is associated with intensional relations ≈_{t}^{′ Int} ∈ Int([[t]]^{op}) and ≈_{t}^{Int} ∈ Int([[t]]), which can be shown to coincide with open-map bisimulation.

Theorem 7.5 Let t be a closed type in the grammar (6). Then,

≈_{t}^{′ Int} = sOs_{[[t]]}^{op} and ≈_{t}^{Int} = sOs_{[[t]]}

where sOs_{ℂ} denotes the class of surjective open spans in ℂ̂.

Corollary 7.6 Let ϑ ⊢ t be a type in the grammar (6), and let I[[ϑ ⊢ t]] : {Prof^{op} |Int^{∗}}×{Prof |Int} → {Prof^{op} | Int^{∗}}×{Prof |Int} be its interpretation as sketched above. Then,

≈_{μϑ.t}^{Int} = sOs_{[[μϑ.t]]}
= ⋃ {R | (R′, R) is a I[[μϑ.t]]-bisimulation} .

Strong bisimulation revisited. Recall that presheaves over ℙ = μϑ.(ϑ)_{⊥} correspond to trees. The intensional relation ≈_{ℙ}^{Int} captures strong bisimulation precisely. Indeed, two trees are connected by a span in ≈_{ℙ}^{Int} iff they are strongly bisimilar. As far as we know, this is the first domaintheoretic characterisation of strong bisimulation for arbitrary trees.

8 Further work

In this paper we have concentrated on solving recursive domain equations for pseudo ωCat-functors on ωCatcategories. Our motivating example is the 2-category Prof that we have used to define so-called presheaf models [5, 36, 4]. The 2-category Prof can also be presented as the bicategory of Set-bimodules [18, 16]. From this viewpoint a natural development of our work is to generalise the results of Section 2 and 3 to handle enriched pseudo-functors between ‘enriched’ bicategories. This is possible via a coherence result; details will appear elsewhere. In this way we will be able to deal with, for instance, the extended class of examples given by V-bimodules [16]. Among these, we find Lawvere’s generalised metric spaces [18] for V = ℜ^{+}, and Set^{I}-bimodules where I is the category of finite cardinals and injections. The latter is a promising setting for working out a theory of presheaf models for higher-order process calculi [27, 34] with features of local name creation and name passing as in the π-calculus.

Aiming at a general treatment of higher order concurrent process calculi, a clear next step is to extend the intensional relations of Section 7.2 to include a treatment of the intuitionistic function space (− → +) as well as the exponential (!). As presented the two accounts of bisimulation, via extensional and intensional relations are rather separate. It is far from straightforward to generalise the extensional account of open-map bisimulation in the presence of tensor and intuitionistic function space. The question seems related to that of giving an operational account of open-map bisimulation when constructions like full linear function space (− ⊸ +) and exponential are involved. By “operational account” is meant a traditional, coinductive characterisation of open-map bisimulation on process terms based on an operational semantics.

Acknowledgements. We thank Robin Cockett for a crucial tip and John Power for discussions.

References

[1] S. Abramsky. On semantic foundations for applicative multiprogramming. In Proceedings of the ICALP’83 Conf., volume 154 of Lecture Notes in Computer Science, pages 1–14. Springer-Verlag, 1983.

[2] J. Adámek. A categorical generalisation of scott domains. Mathematical Structures in Computer Science, 7(5):419–443, 1997.

[3] F. Borceux. Handbook of categorical algebra I, volume 50 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1994.

[4] G. L. Cattani, I. Stark, and G. Winskel. Presheaf models for the π-calculus. In Proceedings of CTCS ’97, number 1290 in Lecture Notes in Computer Science, pages 106–126. Springer-Verlag, 1997.

[5] G. L. Cattani and G. Winskel. Presheaf models for concurrency. In [35], pages 58–75, 1997.

[6] M. Fiore. Axiomatic Domain Theory in Categories of Partial Maps. Distinguished Dissertations in Computer Science. Cambridge University Press, 1996.

[7] M. Fiore. A coinduction principle for recursive data types based on bisimulation. Inform. and Comput., 127(2):186–198, 1996.

[8] M. Fiore and G. Plotkin. An extension of models of axiomatic domain theory to models of synthetic domain theory. In [35], pages 129–149, 1997.

[9] M. Fiore, G. Plotkin, and A. Power. Complete cuboidal sets in axiomatic domain theory. In 12^{th} LICS Conf., pages 268–279. Computer Society Press, 1997.

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

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

[12] 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, 1995.

[13] A. Joyal and I. Moerdijk. A completeness theorem for open maps. Ann. Pure Appl. Logic, 70(1):51–86, 1994.

[14] A. Joyal and I. Moerdijk. Algebraic set theory, volume 220 of London Mathematical Society Lecture Note Series. Cambridge University Press, 1995.

[15] A. Joyal, M. Nielsen, and G. Winskel. Bisimulation from open maps. Inform. and Comput., 127(2):164– 185, 1996.

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

[17] F. Lawvere. Equality in hyperdoctrines and comprehension schema as an adjoint functor. In Applications of Categorical Algebra (Proc. Sympos. Pure Math., Vol. XVII, New York, 1968), pages 1–14. Amer. Math. Soc., 1970.

[18] F. W. Lawvere. Metric spaces, generalized logic, and closed categories. Rend. Sem. Mat. Fis. Milano, 43:135–166, 1973.

[19] D. Lehmann. Categories for fixpoint semantics. PhD thesis, University of Warwick, 1976.

[20] D. Lehmann and M. Smyth. Algebraic specification of data types: A synthetic approach. Math. Systems Theory, 14:97–139, 1981.

[21] S. MacLane. Categories for the Working Mathematician. Springer-Verlag, 1971.

[22] P. W. O’Hearn and R. D. Tennent. Relational parametricity and local variables. In 20^{th} POPL Conf., pages 171–184. ACM, 1993.

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

[24] A. Pitts. Relational properties of domains. Inform. and Comput., 127(2):66–90, 1996.

[25] G. Plotkin. A powerdomain for countable nondeterminism. In Proceedings of the ICALP’82 Conf., Lecture Notes in Computer Science, pages 418–428. Springer-Verlag, 1982.

[26] G. Plotkin. Algebraic completeness and compactness in an enriched setting. Invited lecture given at the Workshop on Logic, Domains, and Programming Languages. Darmstadt, 1995.

[27] D. Sangiorgi. Bisimulation for higher-order process calculi. Inform. and Comput., 131(2):141–178, 1996.

[28] D. Scott. Continuous lattices. In F. Lawvere, editor, Toposes, Algebraic Geometry and Logic, volume 274 of Lecture Notes in Mathematics, pages 97–136. Springer-Verlag, 1972.

[29] H. Simmons. The glueing construction and lax limits. Mathematical Structures in Computer Science, 4(4):393–431, 1994.

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

[31] R. Street. Fibrations in bicategories. Cahiers Topologie Géom. Différentielle Catégoriques, 21(2):111– 160, 1980.

[32] R. Street. Cauchy characterization of enriched categories. Rend. Sem. Mat. Fis. Milano, 51:217–233, 1981.

[33] P. Taylor. The limit-colimit coincidence for categories. Manuscript, 1988.

[34] B. Thomsen. Plain CHOCS: A second generation calculus for higher order processes. Acta Inform., 30(1):1–59, 1993.

[35] D. van Dalen and M. Bezem, editors. Proceedings of the CSL’96 Conf., volume 1258 of Lecture Notes in Computer Science. Springer-Verlag, 1997.

[36] G. Winskel. A presheaf semantics of value-passing processes (extended abstract). In Proceedings of the CONCUR’96 Conf., volume 1119 of Lecture Notes in Computer Science, pages 98–114. Springer-Verlag, 1996.

[37] G. Winskel and M. Nielsen. Models for concurrency. In Handbook of logic in computer science, Vol. 4, Oxford Sci. Publ., pages 1–148. Oxford Univ. Press, 1995.

[38] R. J. Wood. Proarrows II. Cahiers Topologie Géom. Différentielle Catégoriques, 26(2):135–168, 1985.