BRICS RS-97-35 Cattani et al.: A Theory of Recursive Domains with Applications to Concurrency BRICS

Basic Research in Computer Science

A Theory of Recursive Domains with Applications to Concurrency

Gian Luca Cattani Marcelo P. Fiore Glynn Winskel BRICS Report Series RS-97-35 ISSN 0909-0878 December 1997 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1997, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

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

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

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

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

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

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

This document in subdirectory RS/97/35/

A Theory of Recursive Domains with Applications to Concurrency

(Extended Abstract)

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

(1) BRICS^{∗}, University of Aarhus, Denmark (2) LFCS, University of Edinburgh, Scotland

December 1997

Abstract

We develop a 2-categorical theory for recursively defined domains. In particular, we generalise the traditional approach based on ordertheoretic structures to category-theoretic 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.

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

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 [33]. 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 [14].

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 [13]. Presheaf models can be assembled together in the bicategory of profunctors [2] 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 [4]; the 2-category is rich in constructions which can be summarised as those we expect from a model of classical linear logic [32, 3]; open maps are closed under a wide range of constructions [12, 13]. 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.

The generalisation of domain theory from order-theoretic structures to category-theoretic ones has been considered before [18, 19, 30, 1]. In particular, Paul Taylor [30] investigated the limit-colimit coincidence for categories with filtered colimits. 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, 24, 9, 10]. Conceptually, the categorical theory of domains that we put forward may be seen as the traditional theory of Smyth and Plotkin [28] 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.

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 [15]). 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 ‘⇒’ with composition denoted by ‘·’. Invertible 2-cells are called pseudo cells. The paradigmatical 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 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 bicategorical (co)limits [29]. We exemplify this notion with the most basic example.

Bicategorical (or pseudo) initial object. An object 0 in a 2-category is said to be pseudo initial if, for every object C, there exists a morphism ⊥ : 0 → C such that for every morphism c : 0 → C, we have that ⊥ ≅ c via a unique pseudo cell.

The reason for considering this level of generality is that our applications range naturally within the class of bicategories [2] —see Section 8 for discussions. And, as remarked in [29, (1.18)], there are important 2-categories which admit certain bicategorical 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 seems possible using the coherence result stating that every bicategory is biequivalent to a 2-category.

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 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 [28] which yields the limit-colimit coincidence [26]. 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 (c.f. [30, 27]). Next, for the reasons exposed above, we consider bicategorical and 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 (τσ) · η = η′ and ε′ · (στ) = ε. 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 will 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}; g_{n}γ_{n+1}φ_{n+1}f_{n}; g_{n+2,n}γ_{n+2}φ_{n+2}f_{n,n+2}; ⋯]

[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.

Bicategorical 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 bicategorical (pseudo) colimit [29] 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 μ_{n} · (uΦ_{n}) = Ψ_{n} · (μ_{n+1}f_{n}) : uφ_{n+1}f_{n} ⇒ ψ_{n}.

2. For every pair of arrows u, v : A → X and every ω-indexed family of 2-cells (pseudo-cells) ⟨ξ_{n} : uφ_{n} ⇒ vφ_{n}⟩ satisfying ξ_{n} · (uΦ_{n}) = (vΦ_{n}) · (ξ_{n+1}f_{n}) : uφ_{n+1}f_{n} ⇒ vφ_{n} : A_{n} → X, there exists a unique 2-cell (pseudo-cell) ξ : u ⇒ v such that ξ_{n} = ξφ_{n}.

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

Theorem 2.1 (Local characterisation) In an ωCat-category, 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 bicategorical colimit for ⟨f_{n} : A_{n} → A_{n+1}⟩.

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

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 ωCat-category, 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 bicategorical colimit for ⟨f_{n} : A_{n} → A_{n+1}⟩.

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

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}}, and let E_{n}^{∗} : ˆ \overline{𝔸_{n}} ⟶^{≃} 𝔸̂_{n} denote the induced equivalence of categories. It is known (see, for example, [17, 2]) that there exist functors H_{n} : \overline{𝔸_{n}} → \overline{𝔸_{n+1}} such that F_{n} can be seen as a left Kan extension 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 same construction yields pseudo colimits in Prof_{M}.

3 Pseudo-algebraic compactness

Algebraic compactness is a universal property due to Freyd [7] that provides canonical interpretations of recursive domains. In this section we show this property for so-called Kcats; these may be seen as a 2-categorical analogue of ω-cppos (ω-complete pointed partial orders). Following [5], our approach is to obtain the result from the Local-Characterisation and Limit-Colimit Coincidence Theorems, together with the Basic Lemma [28]. 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 T : K → K′ between 2-categories is given by a mapping T : | K | → | K′ | and functors T_{A,B} : K(A, B) → K′(T A, T B) 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 such that for every algebra x : T X → X there exists (it, ι) as in

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

such that whenever

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

we have a unique pseudo cell ξ : it ≅ u for which

\xymatrix{T A \ar[r]_{≅^{μ}}_{≅^{T ξ}}^{a} \ar[d]^{T u} \ar[d]_{T (it)} & A \ar[d]^{u} \\ T X \ar[r]_{x} & X} = [figure: T A; ≅^{ι}; a; T (it); A; it; u; ≅^{ξ}; T X; 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 (c.f. [6, Definition 7.3.11]) is an ωCat_{0}-category with pseudo initial object and pseudo colimits of ω-chains of coreflections.

As examples of Kcats we have: 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}.

From Theorem 2.1, Corollary 2.2, and Lemma 3.1, we can deduce pseudoalgebraic compactness (see [8, 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 (D, D) ≃ D characterised by the following universal property: for every A′ → T (A, A′) and T (A′, A) → A, we have

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

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

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

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 functor + : Prof × Prof → Prof that takes two categories to their disjoint union. Arbitrary sums ∑_{i∈I} t_{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 functor, ⊗ : Prof × Prof → Prof mapping two categories to their product. Dualizer: The dualizer (−)^{∗} is the pseudo functor Prof^{op} → Prof that associates a category with its dual. Exponential: Our choice for the ! operator (see [32, 3] for motivations) is the pseudo functor Prof → Prof sending a category to its free finite-colimit completion. Variables: Are interpreted as projections. Lifting: The pseudo 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 algebras (see [6]).

5 Relational structures

Following [20, 22], we consider relational structures in the spirit of categorical logic [16] (c.f. [11]). A relational structure R on an ωCat_{0}-category K induces a ω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 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 [22]).

Examples. We have the following admissible relational structures.

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

For every small category ℂ, E(ℂ) 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 E on morphisms is by inverse image.

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

For every small category ℂ, I(ℂ) 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 \atop (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 I on morphisms is by inverse image.

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 ⊂_{E} S (where R ∈ E(𝔸) and S ∈ E(𝔹)) if and only if (X, Y) ∈ R implies (F X, F Y) ∈ S, and

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

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} |E} and {Prof |I} are Kcats.

6 Coinduction property

As an application of Theorem 5.1, we present a mixed induction/coinduction principle for recursive domains, à la Pitts [22]. From it, we derive a coinduction property based on bisimulation which will be important in Section 7.

Proposition 6.1 Let R be an admissible relational structure on a Kcat K, and let T and T^{#} be ωCat-functors as in

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

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

fold : T (D, D) ≃ D : unfold

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

fold : T^{#}({D |Δ}, {D |Δ}) ≃ {D |Δ} : unfold

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

Coinduction and bisimulation. In the situation of the above proposition, let

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

Then, Δ ∈ R(D) satisfies the following rule [22]

\frac{unfold : R′ ⊂ T_{R}(R, R′) fold : T_{R}(R′, R) ⊂ R}{R′ ⊂ Δ ⊂ R}

for all R′, R ∈ R(D).

Define a T_{R}-bisimulation to be an R ∈ R(D) such that

unfold : R ⊂ T_{R}(Δ, R) .

Clearly, Δ is a T_{R}-bisimulation. Moreover, if

T_{R}(R, Δ) = T_{R}(Δ, Δ)  (3)

for all R ∈ R(D), then free pseudo dialgebras satisfy the following coinduction property (c.f. [21, 22, 5, 11]):

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

Notice that the requirement (3) is vacuous when T^{#} is essentially covariant; that is, when it factors through an endofunctor on {K | R} via the projection {K|R}^{op} × {K|R} → {K|R}.

7 Open-map bisimulation

We provide models of part of the type theory of Section 4 in the Kcats of relations {Prof_{M} | E} and {Prof | I}. In these models, the denotation of a type provides a model for concurrency (in the form of a presheaf category [4]) 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 openmap bisimulation.

7.1 Extensional relations

In constructing relations within the relational structure E 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 [[Θ ⊢ t]]^{#} : {Prof_{M} | E}^{|Θ|} → {Prof_{M} | E}; 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 [32], 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 E(𝔸). 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} |E}. 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}^{E} ∈ E([[t]]). Recursive types μϑ.t are interpreted as parameterised free pseudo dialgebras in the Kcat {Prof_{M} | E}; specialising the pseudo-colimit construction of the Pseudo Basic Lemma (using Theorem 5.1).

The relation ≈_{t}^{E} 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}^{E} 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 | E} 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

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

in the environment where we assume

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

The relation is a pseudo colimit {𝔻 | R} of an ω-chain {𝔻_{n} | R_{n}} where

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

{𝔻_{n+1} |R_{n+1}} =^{def} [[ϑ_{1}, ⋯, ϑ_{k}, ϑ ⊢ t]]{𝔸_{1} |S_{1}} ⋯ {𝔸_{k} |S_{k}}{𝔻_{n} |R_{n}} .

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). 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 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 Section 6 we obtain the following characterisation.

Corollary 7.4 Let ϑ ⊢ t be a type in the grammar (4), and let

[[ϑ ⊢ t]]^{#} : {Prof_{M} |E} → {Prof_{M} |E}

be its interpretation as sketched above. Then, for presheaves X, Y over [[μϑ.t]], the following are equivalent:

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

• X and Y are [[ϑ ⊢ t]]_{E}-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 ≈_{ℙ}^{E} 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_{E}-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_{E}-bisimulation between locally finite presheaves is a late bisimulation on presheaves in the sense of [32] which is there shown to coincide with open-map bisimulation. Here this result follows from Corollary 7.4. Fortuitously the process language of [32] allows only guarded recursive definitions of processes, so that all process terms denote locally finite presheaves over ℙ. Consequently the relation ≈_{ℙ}^{E} holds between denotations of closed terms iff they are late-bisimilar 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 [23]. 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 give an interpretation of these types in {Prof | I}. Again, it suffices to show how sums, lifting, discrete function space, and tensor extend to pseudo ωCat-functors. Sums: Consider an I-indexed family of relations ⟨R_{i} ∈ I(𝔸_{i})⟩. Then, a span X ⇐ W ⇒ Y in ; ∑_{i∈I} 𝔸_{i} is defined to be in ∑_{i∈I} R_{i} iff for every i ∈ I, the restriction (X)_{i} ⇐ (W)_{i} ⇒ (Y)_{i} is in 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 ∈ I(𝔸), we define X ⟸^{p} W ⟹^{q} Y to be 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.

Discrete function space: Analogous to the extensional case. For R ∈ I(𝔸), a span X ⇐ W ⇒ Y is in 𝕍 ⊸ R if, for every v ∈ 𝕍, the span Xv ⇐ W v ⇒ Y v is in R. Tensor: Let R ∈ I(𝔸) and S ∈ I(𝔹). A span X ⇐ W ⇒ Y in { \atop 𝔸 ⊗ 𝔹} is defined to be in R ⊗ S if, 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 .

Thus every closed type t in the grammar (6) is associated with an intensional relation ≈_{t}^{I} ∈ I([[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}^{I} = 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

[[ϑ ⊢ t]]^{#} : {Prof |I} → {Prof |I}

be its interpretation as sketched above. Then,

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

Strong bisimulation revisited. Recall that presheaves over ℙ = μϑ.(ϑ)_{⊥} correspond to trees. The intensional relation ≈_{ℙ}^{I} captures strong bisimulation precisely. Indeed, two trees are connected by a span in ≈_{ℙ}^{I} iff they are strongly bisimilar. As far as we know, this is the first domain-theoretic 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 ωCat-categories. Our motivating example is the 2-category Prof that we have used to define so-called presheaf models [4, 32, 3]. The 2-category Prof can also be presented as the bicategory of Setbimodules [17, 15]. 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 seems to be possible via a coherence result. In this way we will be able to deal with, for instance, the extended class of examples given by V-bimodules [15]. Among these, we find Lawvere’s generalised metric spaces [17] 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 [25, 31] 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 full function space (− ⊸ +) as well as the exponential (!), and in particular allow for constructions on relations when there is contravariance at play. 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 general function space. The question seems related to that of giving an operational account of open-map bisimulation when constructions like full 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 (allowing some extra tagging of terms or transitions—as some preliminary success suggests).

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

References

[1] J. Adámek. A categorical generalisation of Scott domains. MSCS, 7(5):419– 443, 1997.

[2] F. Borceux. Handbook of Categorical Algebra, vol. 1. CUP, 1994.

[3] G. L. Cattani, I. Stark, and G. Winskel. Presheaf Models for the π-Calculus. In CTCS’97, LNCS 1290, pages 106–126, 1997.

[4] G. L. Cattani and G. Winskel. Presheaf Models for Concurrency. In CSL’96, LNCS 1258, pages 58–75, 1997.

[5] M. P. Fiore. A Coinduction Principle for Recursive Data Types Based on Bisimulation. Inf. & Comp., 127:186–198, 1996.

[6] M. P. Fiore. Axiomatic Domain Theory in Categories of Partial Maps. CUP, 1996.

[7] P. Freyd. Algebraically complete categories. LNM 1488, pages 131–156, 1991.

[8] P. Freyd. Remarks on Algebraically Compact Categories. LMS vol. 177, pages 95–106, 1992.

[9] M. P. Fiore and G. D. Plotkin. An Extension of Models of Axiomatic Domain Theory to Models of Synthetic Domain Theory. In CSL’96, LNCS 1258, pages 129–149, 1997.

[10] M. Fiore, G. Plotkin, and J. Power. Complete Cuboidal Sets in Axiomatic Domain Theory. In 12^{th} LICS Conf., pages 268–279, 1997.

[11] C. Hermida and B. Jacobs. Induction and Coinduction via Subset Types and Quotient Types. In Proc. CLICS-TYPES Workshop on Categories and Type Theory, 1995.

[12] A. Joyal and I. Moerdijk. A completeness theorem for open maps. Ann. Pure App. Logic, 70:51–86, 1994.

[13] A. Joyal and I. Moerdijk. Algebraic Set Theory. CUP, 1995.

[14] A. Joyal, M. Nielsen, and G. Winskel. Bisimulation from open maps. Inf. & Comp., 127:164–185, 1996.

[15] G. M. Kelly. Basic Concepts of Enriched Category Theory. CUP, 1982.

[16] F.W. Lawvere. Equality in hyperdoctrines and the comprehension schema as an adjoint functor. In Applications of Categorical Algebra, pages 1–14, Amer. Math. Soc., 1970.

[17] F.W. Lawvere. Metric Spaces, generalised logic and closed categories. Rendiconti del Seminario Matematico e Fisico di Milano, vol. XLIII, pages 135–166, 1973.

[18] D. J. Lehmann. Categories for fixpoint semantics. Ph.D. Thesis, University of Warwick, 1976.

[19] D. J. Lehmann and M. B. Smyth. Algebraic Specification of Data Types: A Synthetic Approach. Math. System Theory 14, pages 97–139, 1981.

[20] P. O’Hearn and R. D. Tennent. Relational Parametricity and Local Variables. In 20^{th} POPL Conf., pages 171–184, 1993.

[21] A. M. Pitts. A Co-induction Principle for Recursively Defined Domains. TCS, 124:195–219, 1994.

[22] A. M. Pitts. Relational Properties of Domains. Inf. & Comp., 127:66–90, 1996.

[23] G. D. Plotkin. A powerdomain for countable non-determinism, In ICALP’82, LNCS 140, pages 418–428, 1982.

[24] G. D. Plotkin. Algebraic Completeness and Compactness in an Enriched Setting. Invited Lecture given at the LDPL Workshop, 1995.

[25] D. Sangiorgi. Bisimulation for Higher-Order Process Calculi. Inf. & Comp., 131:141–178, 1996.

[26] D. S. Scott. Continuous Lattices. LNM 274, pages 97–136, 1972.

[27] H. Simmons. The glueing construction and lax limits. MSCS, 4(4):393–431, 1994.

[28] M. B. Smyth and G. D. Plotkin. The Category-Theoretic Solution of Recursive Domain Equations. SIAM J. Comput., vol. II-4, pages 761–783, 1982.

[29] R. Street. Fibrations in Bicategories. Cahiers de Topologie et Geometrie Differentielle, vol. XXI-2, pages 111-160, 1980.

[30] P. Taylor. The limit-colimit coincidence for categories. Manuscript, 1992.

[31] B. Thomsen. Plain CHOCS, a second generation calculus for higher-order processes. Acta Informatica, 30:1–59, 1993.

[32] G. Winskel. A presheaf semantics of value-passing processes. In CONCUR’96, LNCS 1119, pages 98–114, 1996.

[33] G. Winskel and M. Nielsen. Models for concurrency. In the Handbook of Logic in Computer Science, vol.IV, OUP, 1995.

Recent BRICS Report Series Publications

RS-97-35 Gian Luca Cattani, Marcelo P. Fiore, and Glynn Winskel. A Theory of Recursive Domains with Applications to Concurrency. December 1997. ii+23 pp.

RS-97-34 Gian Luca Cattani, Ian Stark, and Glynn Winskel. Presheaf Models for the π-Calculus. December 1997. ii+27 pp. Appears in Moggi and Rosolini, editors, Category Theory and Computer Science: 7th International Conference, CTCS ’97 Proceedings, LNCS 1290, 1997, pages 106–126.

RS-97-33 Anders Kock and Gonzalo E. Reyes. A Note on Frame Distributions. December 1997. 15 pp.

RS-97-32 Thore Husfeldt and Theis Rauhe. Hardness Results for Dynamic Problems by Extensions of Fredman and Saks’ Chronogram Method. November 1997. i+13 pp.

RS-97-31 Klaus Havelund, Arne Skou, Kim G. Larsen, and Kristian Lund. Formal Modeling and Analysis of an Audio/Video Protocol: An Industrial Case Study Using Uppaal. November 1997. 23 pp. To appear in The 18th IEEE Real-Time Systems Symposium, RTSS ’97 Proceedings.

RS-97-30 Ulrich Kohlenbach. Proof Theory and Computational Analysis. November 1997. 38 pp.

RS-97-29 Luca Aceto, Augusto Burgueño, and Kim G. Larsen. Model Checking via Reachability Testing for Timed Automata. November 1997. 29 pp.

RS-97-28 Ronald Cramer, Ivan B. Damgård, and Ueli Maurer. Span Programs and General Secure Multi-Party Computation. November 1997. 27 pp.

RS-97-27 Ronald Cramer and Ivan B. Damgård. Zero-Knowledge Proofs for Finite Field Arithmetic or: Can Zero-Knowledge be for Free? November 1997. 33 pp.

RS-97-26 Luca Aceto and Anna Ingólfsdóttir. A Characterization of Finitary Bisimulation. October 1997. 9 pp. To appear in Information Processing Letters.