Towards a Categorical Axiomatics of Bisimulation

Gian Luca Cattani^{1}

Computer Laboratory, University of Cambridge, UK

A. John Power^{2}

LFCS, University of Edinburgh, UK

Glynn Winskel

BRICS, University of Aarhus, DK ^{3}

Abstract

We give an axiomatic category theoretic account of bisimulation in process algebras based on the idea of functional bisimulations as open maps. The axiomatisation centres on 2-monads, T, on Cat. Operations on processes, such as nondeterministic sum, prefixing and parallel composition are modelled using functors in the Kleisli category for the 2-monad T. We may define the notion of open map for any such 2-monad; in examples of interest, the definition agrees exactly with the usual notion of functional bisimulation. Under a condition on T, namely that it be a dense KZmonad, which we define, it follows that functors in Kl(T) preserve open maps, i.e., they respect functional bisimulation. We further investigate structures on Kl(T) that exist for axiomatic reasons, primarily because T is a dense KZ-monad, and we study how those structures help to model operations on processes. We outline how this analysis gives ideas for modelling higher order processes. We conclude by making comparison with the use of presheaves and profunctors to model process calculi.

1 This author is supported by EPSRC grant GR/L62290: Calculi for Interactive Systems: Theory and Experiment. 2 This author is supported by EPSRC grant GR/J84205: Frameworks for programming language semantics and logic. 3 Basic Research in Computer Science, a center of the Danish National Research Foundation.

Preprint submitted to Elsevier Preprint 1 February 1999

Introduction

We seek a category theoretic axiomatic account of bisimulation as studied in concurrency, for instance by Milner [22]. There have been several category theoretic approaches to bisimulation [13,15]. One of them, initiated by Joyal, Nielsen, and Winskel [15], uses the notion of open map to define functional bisimulation, then defines a bisimulation to be a span of epimorphic open maps. That work has only partly been axiomatic: they developed a particular construction, namely the presheaf construction, and studied properties of the 2-category generated by it. Here, we adopt their definition of open map, but consider a class of constructions that are defined axiomatically, based on 2monads on Cat. Our work, although essentially generalising theirs, suggests a way of modelling higher order processes (in the category of algebras of the monad) that was not present (because of size problems) in the presheaf approach, but on the other hand, does not, in its generality, directly include the natural way of representing higher order processes in terms of internal homs that has been suggested for presheaf models [34,11]. We shall expand on this in Section 8.

To model bisimulation using open maps in presheaf categories, one starts with a notion of observation, such as a trace. Based upon that, one defines a small category of path objects (observation shapes), ℙ, where an arrow is understood as witnessing an extension of one path by another. Then one considers the presheaf category [ℙ^{op}, Set]. Following [15,14], one defines an open map in [ℙ^{op}, Set] relative to the category ℙ and the Yoneda embedding of ℙ into [ℙ^{op}, Set]. A key example is given by the category of synchronisation trees over a set of labels L. These are the presheaves over the partial order category of finite non empty strings over L, ordered by the prefix ordering. In this case, epimorphic open maps correspond to, so called, zig-zag morphisms that are functional bisimulations. The induced bisimulation relation obtained by considering spans of such epimorphic open maps coincides with Park-Milner’s strong bisimulation [15]. This discussion applies equally to other notions of observation, such as those arising from non interleaving models.

Various questions arise here. First, typically in concurrency, one does not consider arbitrarily branching trees. It is more usual to consider finitely branching trees, or trees for which the branching is limited, for instance to being countable. Second, in the case of the combined presence of higher order and names as in the Higher-Order π-calculus, it is not clear whether the presheaf construction is sufficient (see [9,7] for a more detailed discussion). If we can give an axiomatic account of some of the relevant constructions, we are in a better position to address such issues. An axiomatic account also clarifies the reasoning behind the various decisions. So in this paper, we do not take presheaf categories for granted, but give an axiomatic development of precisely what structure we want in order to model concurrency and what constructions arise in manipulating that structure. For concreteness, we restrict our attention for the bulk of the paper to the operations needed in modelling CCS processes by synchronisation trees. We occasionally refer to more involved examples that were treated using presheaf categories in [34,10,9].

We first observe in Section 1 that, given a category of observations, ℙ, the basic operations of CCS lead us to consider the free completion of the category ℙ under countable colimits: for our choice of ℙ, that is equivalent to the category of countably branching trees. The construction of countable colimit completions extends to a 2-monad T on Cat with strong category theoretic properties, as explained in Sections 3 and 4. Moreover, the constructions we wish to consider, such as nondeterministic sum or parallel composition, arise from maps in Kl(T), the Kleisli 2-category for T. That is typical of basic constructions on ℙ and of other categories of observations.

In Section 2, we recall the universal properties associated with free colimit completions and the notion of left Kan extension that we shall need in Section 5 and 6.

Under a condition on a 2-monad T, namely that it be a dense KZ-monad, which we shall define and which holds of all our leading examples, we can define the notion of open map in each T ℂ (for ℂ a small category) and prove that maps in the Kleisli 2-category of T preserve all open maps. This forms the content of Section 5. The notion of open map, which we recall in Section 4, agrees in our leading examples, with the usual notion of functional bisimulation.

We next consider the structure of Kl(T) for a 2-monad T on Cat that satisfies various conditions true of our examples. In particular, we show that Kl(T) has finite coproducts and finite products and that they agree, and that it has a symmetric monoidal structure. From these facts, it follows that the various constructions on processes, such as taking nondeterministic sum, applying a parallel operator, and prefixing, preserve open maps. It also gives us candidates for higher order structure (though some are outside Kl(T)), allowing a possible way to model a process passing extension of CCS. This analysis forms Sections 6 and 7.

Finally, in Section 8, we compare, especially as far as higher order is concerned, this work with that of [34,10,9,11] using presheaves and profunctors to model process calculi, and we suggest directions for future research.

We do not address weak bisimulation at all here. In no way do we suggest that it is unimportant. But it is a large issue and the ideas of how to extend weak bisimulation to presheaf models [12] are still fresh. We expect that our axiomatics may allow a similar development, but we are not sure yet. It is not clear to us whether directly modelling weak bisimulation is the most interesting development. It may be better to develop a notion of contextual equivalence, using strong bisimulation as a technique, along the lines of the development of testing equivalence. So we defer a detailed analysis of the issues to later work.

To induce bisimulation from functional bisimulation, it suffices to consider spans of epimorphic functional bisimulations. We are careful that all our constructions respect such spans, but we do not consider them explicitly through the course of the paper.

1 A motivating example

For concreteness, we consider the process calculus CCS (assuming a fixed set of labels) as in [22] with models given by labelled trees; but our analysis holds more generally (see [15]). Labelled trees or synchronisation trees as they are usually called [32,33] are primary examples of models for concurrency. In this section we shall briefly review how the tree structure is generated by simple categorical operations on strings, i.e., finite trees with a single branch, of actions.

Definition 1 Let L be a set, not including the the letter τ among its elements. Let L̄ = {l̄ | l ∈ L}, and define the category L whose objects are strings of arbitrary length, possibly infinite, of elements of the set of ‘actions’

A = L ∪ L̄ ∪ {τ} ,

where a map from the string p to the string q is a prefixing of q by p, with composition given by composing inclusions.

The category L^{∗} is the full subcategory of L of finite strings.

The category L^{↑} is the full subcategory of L of non empty strings and L^{+} is the restriction of L^{↑} to strings of finite length.

Definition 2 (Lifting) If ℂ is any category, define ℂ_{⊥} to be the completion of the category ℂ to which a strict new initial object, denoted ⊥, has been added.

Notice that for a set of labels L, there is an isomorphism of categories

L^{∗} ≅ (L^{+})_{⊥} .

A string is a tree with no branching structure and it accounts for a computation path, i.e., a sequence of actions that can be observed of a process. The computation trees of all CCS processes are generated by two operations freely applied to computation paths. First, given processes P and Q, their nondeterministic sum has computation tree determined by the disjoint sum of the computation trees of P and Q. Second, given processes P and Q and an action a, the computation tree for a.(P + Q) is given by identifying the computation trees for a.P and a.Q on the first step. So, to represent the computation trees of nondeterministic sum and of prefixing, we extend the category L by freely adding finite coproducts to model nondeterministic sum and coequalisers to allow computation paths to agree for a while as they proceed. This is equivalent to freely adding finite colimits [20]. Thus we have

Proposition 3 The category of finitely branching synchronisation trees with finitely many maximal branches is equivalent to the free finite colimit completion T_{ω}L^{↑} of the category L^{↑}.

This gives only a limited account of recursion, as we have not allowed finitely branching trees with more than finitely many maximal branches. Moreover, in order to add value passing to CCS, one approach has been to extend a binary nondeterministic operator to a countable one [22]. That yields the category of countably branching trees, and we have

Proposition 4 (1) The category of countably branching synchronisation trees over L ∪ L̄ ∪ {τ}, ST_{ω}, is equivalent to the free countable colimit completion T_{ω_{1}}L^{+} of L^{+}.

(2) The category of finitely branching synchronisation trees over L ∪ L̄ ∪ {τ}, ST_{f}, is a full subcategory of ST_{ω}.

More generally,

Proposition 5 For any regular cardinal κ > ω, the category of synchronisation trees with branching less than κ is the free completion T_{κ}L^{+} of L^{+} under colimits of size less than κ.

This line of argument applies not only to strings but to a range of notions of path objects (see [34,9,7]) giving one reason to consider, for any small category ℂ of path objects, the categories T_{ω}ℂ, T_{ω_{1}}ℂ, and more generally T_{κ}ℂ of free colimit completions of ℂ under finite, countable, and less than κ size colimits respectively. We shall soon have other reasons to consider T_{κ}ℂ for various ℂ, not just ℂ = L^{+}, even while restricting our attention to trees, as they are needed to model many-sorted operations on trees to represent nondeterministic sum and the like. So we seek an axiomatic account of these constructions.

2 Universal properties

We make now explicit what we mean when we are talking of the free completion T_{κ}ℂ of a category ℂ under colimits of size less than κ. This will also give us the opportunity to recall the notion of left Kan extension which will play a crucial role later in the paper. Just like any other free construction the free completion T_{κ} is characterised by a universal property.

Definition 6 Let ℂ be a category with colimits of diagrams of size less than κ. The category ℂ has assigned colimits if for any diagram D : 𝕀 → ℂ of size less than κ a choice of a colimiting cone for D has been made.

Terminology: From now on we shall often write ‘κ-colimit’ instead of ‘colimit of diagram of size less than κ’.

The universal property of T_{κ}(ℂ), for ℂ any category, can then be stated as follows: The category T_{κ}(ℂ) has assigned κ-colimits and there exists a functor

η_{ℂ} : ℂ ↪ T_{κ}(ℂ)

such that for any category 𝔻 with assigned κ-colimits and for any functor

F : ℂ → 𝔻

there exists a unique functor

F_{!} : T_{κ}(ℂ) → 𝔻

such that F_{!} sends assigned colimiting cones to assigned colimiting cones and makes the triangle

\xymatrix{ℂ \ar[dr]_{F} \ar[r]^{η_{ℂ}} & T_{κ}(ℂ) \ar[d]^{F_{!}} \\  & 𝔻}

commute.

Notice that the functor η_{ℂ} is in fact an embedding. Moreover as a consequence of the ‘1-dimensional universal property’ above we also have the following 2dimensional one [16]:

There is an isomorphism of categories between the category of functors from ℂ to 𝔻 and natural transformations, [ℂ, 𝔻], and the category of assignedcolimit preserving functors from T_{κ}(ℂ) to 𝔻 and natural transformations, Cocont_{s}[T_{κ}(ℂ), 𝔻].^{4}

4 Following [4] we shall often refer to assigned-colimit preserving functors as ‘strict colimit preserving functors’, hence the subscript ‘s’ in Cocont_{s}.

In fact more can be said as the above situation is an instance of the general notion of left Kan extension [20,5].

Definition 7 (Kan Extensions) If C ⟵^{G} A ⟶^{F} B is a span of functors, one says that a pair (H, α) is a left Kan extension of G along F if

• H : B → C is a functor

• α : G ⇒ HF is a natural transformation satisfying the following universal

property:

for every other pair (K, β) with β : G ⇒ KF there exists a unique γ : H ⇒ K such that β = γ_{F} · α.

By the usual abuse of language we will often address the functor H as the left Kan extension of G along F and write Lan_{F} (G) to indicate it.

Note that the triangle

\xymatrix{A \ar[r]^{F} \ar[dr]_{G} & B \ar[d]^{Lan_{F} (G)} \\  & C}

need not commute, not even up to natural isomorphism. Still, this happens in many cases of interest.

Proposition 8 If F is full and faithful and (Lan_{F} (G), α) exists then α is a natural isomorphism.

If C is cocomplete and A is small, then Lan_{F} (G) always exists for any F and G and can be computed “pointwise” (see [5]) as a colimit. Thus in this case left Kan extensions are preserved by left adjoints:

Proposition 9 Let C ⟵^{G} 𝔸 ⟶^{F} B be a span of functors, with 𝔸 small and C cocomplete. Let H : C → D be a functor with a right adjoint, then

HLan_{F} (G) ≅ Lan_{F} (HG) .

Left Kan extensions compose in the sense that if (H, α) is the left Kan extension of G along F for C ⟵^{G} A ⟶^{F} B and (K, β) is the left Kan extension of H along F′, for C ⟵^{H} B ⟶^{F′} D, then (K, β_{F} · α) is the left Kan extension of G along F′F:

Lan_{F′F} (G) ≅ Lan_{F′}(Lan_{F} (G)) .

3 The general setting

In order to make our first observation, we need some definitions.

Definition 10 A 2-monad on Cat is a 2-functor T : Cat ⟶ Cat, i.e., a functor that sends natural transformations to natural transformations, respecting domains, codomains and composites of natural transformations, together with 2-natural transformations μ : T^{2} ⇒ T (the multiplication) and η : id ⇒ T (the unit), i.e., natural transformations that respect the 2-categorical structure of Cat, subject to three axioms expressing associativity of μ and the fact that η acts as left and right unit for μ.

Considerable detail of 2-monads and the category theoretic constructions associated with them appears in [17], but we shall try to make this paper reasonably self-contained in regard to 2-monads. The reason 2-monads interest us here is because we have

Proposition 11 For any regular cardinal, κ, T_{κ} extends to a 2-monad on Cat.

Proof: We show how the universal property of Section 2 helps us extending the action of T_{κ} from categories (the objects of Cat) to functors and natural transformations (the arrows and 2-cells of Cat) and how it makes naturally emerging the unit and multiplication needed for a monad structure. In fact η is naturally defined to be given by the embeddings

η_{ℂ} : ℂ ↪ T_{κ}(ℂ) .

If F : ℂ → 𝔻 is any functor, define T_{κ}(F) : T_{κ}(ℂ) → T_{κ}(𝔻) as the unique strict κ-colimit preserving functor which makes the following square commuting:

\xymatrix{ℂ \ar[r]^{η_{ℂ}} \ar[d]_{F} & T_{κ}(ℂ) \ar[d]^{T_{κ}(F)} \\ 𝔻 \ar[r]_{η_{𝔻}} & T_{κ}(𝔻) .}

If α : F ⇒ G : ℂ → 𝔻 is a natural transformation, define

T_{κ}(α) : T_{κ}(F) ⇒ T_{κ}(G) : T_{κ}(ℂ) → T_{κ}(𝔻)

as the unique natural transformation such that

T_{κ}(α)η_{ℂ} = η_{𝔻}α .

For every category ℂ, define μ_{ℂ} : T_{κ}(T_{κ}(ℂ)) → T_{κ}(ℂ) as the unique strict κ-colimit preserving functor making the following triangle commutes:

\xymatrix{T_{κ}(ℂ) \ar[r]^{η_{Tκ(ℂ)}} \ar[dr]_{id_{Tκ(ℂ)}} & T_{κ}(T_{κ}(ℂ)) \ar[d]^{μ_{ℂ}} \\  & T_{κ}(ℂ) .}

The universal property also ensures that all the necessary axioms and coherence conditions are met. For instance to check that

μ_{ℂ}T_{κ}(η_{ℂ}) = id_{T_{κ}(ℂ)}

is enough to notice that

μ_{ℂ}T_{κ}(η_{ℂ})η_{ℂ} = μ_{ℂ}η_{T_{κ}(ℂ)}η_{ℂ} (by definition of T_{κ})
= η_{ℂ}  (by definition of μ_{ℂ}).

In fact by universality it then follows that necessarily μ_{ℂ}T_{κ}(η_{ℂ}) must be equal to id_{T_{κ}(ℂ)}. □

Returning to CCS as modelled by synchronisation trees, an operation such as nondeterministic sum respects the structure of the computation trees of P and Q. More precisely, the functor + : T_{κ}L^{+} × T_{κ}L^{+} ⟶ T_{κ}L^{+} strictly preserves colimits of specified size. We shall show later that, for a general ℂ (and in particular, when ℂ = L^{+}) T_{κ}ℂ × T_{κ}ℂ is of the form T_{κ}𝔻 for another small category 𝔻 (= ℂ + ℂ). So we are led to consider strict κ-colimit preserving functors from T_{κ}𝔻 to T_{κ}ℂ. These are arrows in the Kleisli 2-category for T_{κ}, which is defined as follows.

Definition 12 Given a 2-monad T on Cat, the Kleisli 2-category has as objects categories of the form T ℂ, and arrows those functors H : T ℂ ⟶ T 𝔻 such that μ_{𝔻}T (H) = Hμ_{ℂ}, with composition given by usual composition of functors. An arrow in Kl(T) may equivalently be described as any functor from ℂ to T 𝔻. The 2-cells are those natural transformations α such that μ_{𝔻}T (α) = αμ_{ℂ}.

Proposition 13 The category of countably branching synchronisation trees over a fixed set of labels, ST_{ω}, together with functors from finite products of the category ST_{ω} to itself that preserve the tree structure, form a full subcategory of the Kleisli category Kl(T_{ω_{1}}).

This result extends directly to synchronisation trees of any bounded degree of branching, say κ, with respect to Kl(T_{λ}), with λ a regular cardinal strictly bigger than κ.

The situation is not so straightforward with other operators like prefixing and parallel composition. In fact we cannot expect them to be directly represented by arrows in Kl(T). For instance the parallel composition of processes does not distribute over the sum (P |(Q+R) ≅ (P |Q)+(P |R)). However, a more careful analysis we carry out in Section 7 will represent these other key operators in terms of arrows of Kl(T) and hence allow us to deduce axiomatically that they respect bisimulation too.

4 Functional bisimulations as open maps

We now show how the notion of functional bisimulation in our examples may be identified with the notion of open map. Again, this holds more generally, as explained in [15,34,9,7], but for concreteness, we shall continue to restrict our attention to CCS as modelled by synchronisation trees, and the notion of functional bisimulation there.

Definition 14 (Joyal-Nielsen-Winskel) Let F : ℙ → M be a functor, define an arrow f : M_{1} → M_{2} in M to be F -open if it satisfies the following ‘path lifting property’: For every commuting square

\xymatrix{F (P) \ar[d]_{F (m)} \ar[r]^{p} & M_{1} \ar[d]^{f} \\ F (Q) \ar[r]_{q} & M_{2}}

there exists an arrow r : F (Q) → M_{1} such that in the diagram

\xymatrix{F (P) \ar[d]_{F (m)} \ar[r]^{p} & M \ar[d]^{f} \\ F (Q) \ar[ur]^{r} \ar[r]^{q} & M′}

the two “triangles” commute, i.e., rF (m) = p and fr = q. If F is a canonically chosen embedding one talks of ℙ-open maps rather than F -open ones.

Notice that the diagonal map, r, need not be unique and typically is not unique. Working through the definition in examples, one verifies that open maps correspond to functional bisimulations [15]. We shall content ourselves with recalling the following proposition about synchronisation trees:

Proposition 15 (cf. Proposition 1 of [15]) With respect to the inclusion functor

η_{L} : L ↪ T_{κ}(L) ≃ ST_{κ}

the epimorphic η_{L}-open maps are the “zig-zag morphisms” of [3], the “pmorphisms” of [27], the “abstraction homomorphisms” of [6], and the “pure morphisms” of [2], i.e., those morphisms , f : S → S′, of synchronisation trees with the property that for every state s of S

if f(s) →^{a} s′ in S′ then s →^{a} u in S, for some state u of S.

For any 2-monad T on Cat, we can canonically define the notion of open map on T ℂ for arbitrary ℂ.

Definition 16 Given a 2-monad T on Cat and a small category ℂ, an arrow h : X ⟶ Y in T ℂ is open if it is η_{ℂ}-open, where η_{ℂ} : ℂ → T ℂ is the unit of the monad at ℂ.

Another important class of categories with a canonical choice of open maps is provided by presheaf categories.

Definition 17 Let ℂ be a small category. An arrow of [ℂ^{op}, Set], i.e., a natural transformation between two contravariant functors from ℂ to Set, is open if it is y_{ℂ}-open, where y_{ℂ} : ℂ → [ℂ^{op}, Set] is the Yoneda embedding.

Considerable details about the relevance of presheaf categories for the abstract understanding of models for concurrency and bisimulation appear in a series of papers [15,34,10,9,7]. For the purpose of this paper it is useful to recall the following preservation property.

Theorem 18 (Cattani-Winskel [10,7]) Let F : [ℂ^{op}, Set] → [𝔻^{op}, Set] be a colimit preserving functor. If f is an (epimorphic) open map in [ℂ^{op}, Set] then F (f) is an (epimorphic) open map in [𝔻^{op}, Set].

5 Dense KZ-monads

A fundamental property of process calculi (like CCS) is that constructions involved in modelling the process constructors preserve functional bisimulations, e.g., if P is functionally bisimilar to P′, then P +Q must be functionally bisimilar to P′ + Q, and symmetrically. This is exactly to say, in modelling CCS by finitely branching trees, that open maps are preserved by the functor

+ : T_{ω_{1}}ℂ × T_{ω_{1}}ℂ ⟶ T_{ω_{1}}ℂ .

Thus we want a condition on 2-monads T satisfied by all our examples and such that functors in Kl(T) preserve open maps just like the colimit preserving functors of Theorem 18 do. The first major result of the paper gives such a condition. First, we need some definitions.

Definition 19 A KZ-monad is a 2-monad for which the multiplication μ : T^{2} ⟹ T is left adjoint to ηT with counit of the adjunction given by the identity, where η is the unit of the 2-monad, i.e., for every small category ℂ, the functor μ_{ℂ} : T^{2}ℂ ⟶ T ℂ is left adjoint to the functor η_{T ℂ} : T ℂ ⟶ T^{2}ℂ, and the adjunctions are preserved by functors H : ℂ ⟶ 𝔻. It is equivalent to ask that μ be right adjoint to T η, with the identity being the unit (see [18,30]).

The notion of KZ-monad was introduced to study particular features of 2monads given by free completions under classes of colimits [18]. But they do not characterise such free completions, as the following example shows.

Example 20 Consider the 2-monad on Cat that sends every category to the one object one arrow category 1. It is a KZ-monad trivially, but it does not give free completions under a class of colimits because ℂ typically is not a full subcategory of 1.

Notation: Given a 2-monad T on Cat, let η̃_{ℂ} : T ℂ ⟶ [ℂ^{op}, Set] denote the functor that sends an object X to the functor T ℂ(η_{ℂ}−, X) : ℂ^{op} ⟶ Set.

Observe that the functor η̃_{ℂ} is itself a left Kan extension, in fact it can be obtained as

Lan_{η_{ℂ}}(y_{ℂ}) ,

where y_{ℂ} : ℂ ⟶ [ℂ^{op}, Set] is the Yoneda embedding.

Definition 21 A 2-monad T on Cat is dense if for every small category ℂ, the functors η_{ℂ} : ℂ ⟶ T ℂ and η̃_{ℂ} : T ℂ ⟶ [ℂ^{op}, Set] are fully faithful, and for any H : ℂ ⟶ 𝔻, the functor Lan_{y_{ℂ}}(y_{𝔻}H) : [ℂ^{op}, Set] ⟶ [𝔻^{op}, Set], where y_{ℂ} : ℂ ⟶ [ℂ^{op}, Set] is the Yoneda embedding, restricts to T H : T ℂ ⟶ T 𝔻 up to coherent isomorphism:

[figure: ℂ; y_{ℂ}; η_{ℂ}; H; T ℂ; η̃_{ℂ}; T H; ≅; [ℂ^{op}, Set]; Lan_{y_{ℂ}}(y_{𝔻}H); 𝔻; y_{𝔻}; η_{𝔻}; T 𝔻; η̃_{𝔻}; [𝔻^{op}, Set] .]

In our examples, η_{ℂ} is the inclusion of a category ℂ into its free colimit completion of specified size; we shall not need an explicit description of μ_{ℂ}. Moreover, η_{ℂ} : ℂ ⟶ T ℂ is always fully faithful, and it follows by a general theorem [20] that, since each object of T ℂ is a colimit of a diagram in ℂ, the functor η̃_{ℂ} : T ℂ ⟶ [ℂ^{op}, Set] is also fully faithful, and for every given functor H : ℂ ⟶ 𝔻, the functor Lan_{y_{ℂ}}(y_{𝔻}H) : [ℂ^{op}, Set] ⟶ [𝔻^{op}, Set] restricts to T H : T ℂ ⟶ T 𝔻 up to coherent isomorphism. In fact since left Kan extensions compose we have that

Lan_{y_{ℂ}}(y_{𝔻}H)η̃_{ℂ} = Lan_{y_{ℂ}}(y_{𝔻}H)Lan_{η_{ℂ}}(y_{ℂ})
= Lan_{η_{ℂ}}(Lan_{y_{ℂ}}(y_{𝔻}H)y_{ℂ})
≅ Lan_{η_{ℂ}}(y_{𝔻}H) .

Since both Lan_{η_{ℂ}}(y_{𝔻}H) and η̃_{𝔻}T H preserves κ-colimits it is enough to follow the calculation below,

Lan_{η_{ℂ}}(y_{𝔻}H)η_{ℂ} ≅ y_{𝔻}H = η̃_{𝔻}η_{𝔻}H = η̃_{𝔻}T Hη_{ℂ} ,

to conclude that η̃_{𝔻}T H is naturally (and coherently) isomorphic to

Lan_{y_{ℂ}}(y_{𝔻}H)η̃_{ℂ} .

Hence we have the following:

Proposition 22 If κ is any regular cardinal, T_{κ} is a dense KZ-monad.

Now we can state our first major theorem, which characterises dense KZmonads.

Theorem 23 Let T be a 2-monad on Cat for which η_{ℂ} : ℂ ⟶ T ℂ and η̃_{ℂ} : T ℂ ⟶ [ℂ^{op}, Set] are fully faithful for every ℂ. Then T is a dense KZ-monad if and only if every functor F : T ℂ ⟶ T 𝔻 in Kl(T) is the restriction of Lan_{y_{ℂ}}(η̃_{𝔻}F η_{ℂ}) : [ℂ^{op}, Set] ⟶ [𝔻^{op}, Set] up to coherent isomorphism. Moreover, under the equivalent conditions, every F in Kl(T) is a left Kan extension of F η_{ℂ} : ℂ ⟶ T 𝔻 along η_{ℂ} : ℂ ⟶ T ℂ.

Proof: Suppose T is dense and KZ, and let F : T ℂ ⟶ T 𝔻 be a functor in Kl(T). Then F = μ_{𝔻}T K where K = F η_{ℂ} : ℂ ⟶ T 𝔻. Observe now first of all that for any D object of T^{2}𝔻,

Lan_{y_{T 𝔻}}(η̃_{𝔻})(η̃_{T 𝔻}(D)) ≅ T^{2}𝔻[η_{T 𝔻}(η_{𝔻}−), D] (as a direct coend calculation

would show)

≅ T^{2}𝔻[T η_{𝔻}(η_{𝔻}−), D]  (by naturality of η)
≅ T 𝔻[η_{𝔻}−, μ_{𝔻}D]  (since by KZ-ness, T η_{𝔻} ⊣ μ_{𝔻})
= η̃_{𝔻}(μ_{𝔻}D)  (by definition).

So the density condition holds for μ_{𝔻}. Applying it to K gives that

η̃_{T 𝔻}T K ≅ Lan_{y_{ℂ}}(y_{T 𝔻}K)η̃_{ℂ} .

Recall also that for any functor A : ℂ → [𝔻^{op}, Set] from any small category to a presheaf category, the left Kan extension Lan_{y_{ℂ}}(A) has a right adjoint [21]. Hence

η̃_{𝔻}F = η̃_{𝔻}μ_{𝔻}T K
≅ Lan_{y_{T 𝔻}}(η̃_{𝔻})η̃_{T 𝔻}K
≅ Lan_{y_{T 𝔻}}(η̃_{𝔻})Lan_{y_{ℂ}}(y_{T 𝔻}K)η̃_{ℂ}
≅ Lan_{y_{ℂ}}(Lan_{y_{T 𝔻}}(η̃_{𝔻})y_{T 𝔻}K)η̃_{ℂ} (by Proposition 9)
≅ Lan_{y_{ℂ}}(η̃_{𝔻}K)η̃_{ℂ}  (by Proposition 8)
= Lan_{y_{ℂ}}(η̃_{𝔻}F η_{ℂ})η̃_{ℂ}  (by definition of K).

For the converse, given H : ℂ ⟶ 𝔻, let F = T H. By naturality of η and since η̃_{𝔻}η_{𝔻} = y_{𝔻} : 𝔻 ⟶ [𝔻^{op}, Set] by fully faithfulness of η_{𝔻}, it follows that η̃_{𝔻}F η_{ℂ} = y_{𝔻}H, so T is dense.

To see that T is KZ, first observe that μ_{ℂ} : T^{2}ℂ ⟶ T ℂ is a functor in Kl(T) since, by the monad laws, it respects the structure of T. So, up to isomorphism, μ_{ℂ} is the restriction of Lan_{y_{T ℂ}}(η̃_{ℂ}μ_{ℂ}η_{T ℂ}) = Lan_{y_{T ℂ}} η̃_{ℂ}. But, by fully faithfulness of η̃_{ℂ}, the functor η_{T ℂ} : T ℂ ⟶ T^{2}ℂ is the restriction of the functor sending Kϵ[ℂ^{op}, Set] to [ℂ^{op}, Set](η̃_{ℂ}−, K), but this latter functor is the right adjoint of Lan_{y_{T ℂ}} η̃_{ℂ} [21]. Since η̃_{ℂ} and η̃_{T ℂ} are both fully faithful, it follows that μ_{ℂ} is left adjoint to η_{T ℂ}.

For the final statement of the theorem, given any K : T ℂ ⟶ T 𝔻, it follows by fully faithfulness of η̃_{ℂ} : T ℂ ⟶ [ℂ^{op}, Set] that η̃_{𝔻}K is isomorphic to Lanη̃_{ℂ}(η̃_{𝔻}K)η̃_{ℂ}. Moreover, since η_{ℂ} is fully faithful, the Yoneda embedding y_{ℂ} : ℂ ⟶ [ℂ^{op}, Set] equals η̃_{ℂ}η_{ℂ}. So any natural transformation α : F η_{ℂ} ⇒ Kη_{ℂ}, induces a natural transformation from η̃_{D}F η_{ℂ} : ℂ ⟶ [T 𝔻^{op}, Set] to Lanη̃_{ℂ}(η̃_{𝔻}K)y_{ℂ}, hence by definition of left Kan extension, a natural transformation ᾱ : Lan_{y_{T ℂ}}(η̃_{𝔻}F η_{ℂ}) ⇒ Lanη̃_{ℂ}(η̃_{𝔻}K). The result follows immediately from fully faithfulness of η̃_{𝔻} and the two commutativities up to coherent isomorphism. □

Corollary 24 Given a dense KZ-monad T on Cat, for every ℂ, μ_{ℂ} is the left Kan extension of id_{T ℂ} : T ℂ ⟶ T ℂ along η_{T ℂ} : T ℂ ⟶ T^{2}ℂ and is the restriction of [η_{ℂ}, Set] : [T ℂ^{op}, Set] ⟶ [ℂ^{op}, Set].

Proof: By the last statement of Theorem 23, since μ_{ℂ} is in Kl(T),

μ_{ℂ} = Lan_{η_{T ℂ}}(μ_{ℂ}η_{T ℂ}) = Lan_{η_{T ℂ}}(id_{T ℂ}) .

Moreover observe that the functor [η_{ℂ}, Set] is known [21] to be the same as

Lan_{y_{T ℂ}}(Lan_{η_{ℂ}}(y_{ℂ})) .

Before we also noticed that Lan_{η_{ℂ}}(y_{ℂ}) = η̃_{ℂ} and in the proof of Theorem 23 we have observed that μ_{ℂ} is the restriction of Lan_{y_{ℂ}} η̃_{ℂ}. Putting all this together gives first that

[η_{ℂ}, Set] = Lan_{y_{T ℂ}}(Lan_{η_{ℂ}}(y_{ℂ})) = Lan_{y_{ℂ}} η̃_{ℂ}

and hence that μ_{ℂ} is the restriction of [η_{ℂ}, Set]. □

Corollary 25 Let T be a dense KZ-monad on Cat. Then every functor in Kl(T) preserves open maps.

Proof: Let f : C → C′ be an open map in T ℂ and let F : T ℂ → T 𝔻 be an arrow in Kl(T). Since η̃_{ℂ} is a full and faithful functor and since y_{ℂ} factors as η̃_{ℂ}η_{ℂ}, η_{ℂ}(f) is open in [ℂ^{op}, Set]. By Theorem 18,

Lan_{y_{ℂ}}(η̃_{𝔻}F η_{ℂ})(η_{ℂ}(f))

is open in [𝔻^{op}, Set]. But by Theorem 23,

Lan_{y_{ℂ}}(η̃_{𝔻}F η_{ℂ})(η_{ℂ}(f)) ≅ η̃_{𝔻}F (f)

and since η̃_{𝔻} is full and faithful and y_{𝔻} factorises as η̃_{𝔻}η_{𝔻}, it follows that η̃_{𝔻}F (f) is open in T 𝔻. □

We regard this corollary as fundamental for the reasons outlined above.

Theorem 23 is of fundamental importance. It can be used to characterise all dense KZ-monads on Cat. The notion of dense KZ-monad is the central new mathematical notion we introduce in this paper. It includes all monads that arise as free completions under a class of colimits, and it is possible, using Theorem 23, to characterise dense KZ-monads in those terms. That is beyond the scope of this paper (see [24]), but we do remark that the precise statement is very subtle. For instance,

Example 26 There exists a dense KZ-monad T for which there is no class S of small categories such that for every small category ℂ, the category T ℂ is the free completion of ℂ under colimits of diagrams with shape in S. Consider T 0 = 0 (0 being the empty category) with T ℂ given by freely adding an initial object to ℂ for all other ℂ. Suppose our claim was false. Since T 0 is empty, it follows that every category in S must be nonempty. The free completion of ℂ under colimits of diagrams with shape in S is given by a transfinite induction. At every step in that construction, one adds a new colimit. But since each category in S is nonempty, each new colimit added must have an arrow into it from a pre-existing object, so ultimately from an object of ℂ. So at no point in the transfinite induction does one introduce an initial object, a contradiction.

6 Structure of Kl(T) for dense KZ-monads

Based upon our results of the previous two sections, in particular Corollary 25, in this section we investigate the structure of categories of the form Kl(T) for dense KZ-monads T. Of course, that includes (size bounded) colimit completions as illustrated in Section 4.

6.1 Coproducts

Routinely, as for any monad on a category with coproducts, we have

Proposition 27 For any 2-monad T on Cat, the 2-category Kl(T) has coproducts, with the coproduct of T ℂ and T 𝔻 in Kl(T) given by the construction T (ℂ + 𝔻) in Cat.

This generalises a domain theoretic property on ω-Cpo which is used to model conditional statements. Furthermore, we shall soon show that, under a mild extra condition, T (ℂ + 𝔻) is isomorphic to T ℂ × T 𝔻, and that is important to us as the latter construction is used in defining nondeterministic sum for example. It will follow that Kl(T) has finite products, with the product in Kl(T) of T ℂ and T 𝔻 given by T (ℂ+𝔻). But first, we look into the symmetric monoidal structure the Kleisli category inherits from the product of categories.

6.2 Symmetric monoidal structure

Theorem 28 If T is a dense KZ-monad on Cat, then Kl(T) is a symmetric monoidal 2-category, with T ℂ ⊗ T 𝔻 given by T (ℂ × 𝔻).

Proof: To give a symmetric monoidal structure on Kl(T) that extends the finite product structure on Cat is equivalent to showing that the strength on T corresponding to its Cat-enrichment is commutative [23]. What that means is as follows. For each object X of ℂ, consider the functor t_{X} : 𝔻 ⟶ T (ℂ×𝔻) determined by η_{ℂ×𝔻} composed with the functor into ℂ choosing the object X. Every map f : X ⟶ Y in ℂ determines a natural transformation from t_{X} to t_{Y}. Since the isomorphism between Kl(T)[T 𝔻, T (ℂ×𝔻)] and Cat[𝔻, T (ℂ×𝔻)] is an isomorphism of categories, we obtain a functor t : ℂ×T 𝔻 ⟶ T (ℂ×𝔻). Dually, we obtain a functor t̄: T ℂ × 𝔻 ⟶ T (ℂ × 𝔻). To obtain a symmetric monoidal structure on Kl(T), it suffices to show that the two ways of using these constructions to obtain a functor T̄ : T ℂ × T 𝔻 ⟶ T (ℂ × 𝔻), either by first applying t, then applying T t̄, then applying μ, or dually, give the same result.

To see that, recall that for every functor F : ℂ ⟶ T 𝔻, the lifting of F to Kl(T) is given, up to isomorphism, by the restriction of Lan_{y_{ℂ}}(y_{𝔻}F). And μ_{ℂ} : T^{2}ℂ ⟶ T ℂ is the restriction, up to isomorphism, of [η_{ℂ}, Set] : [T ℂ^{op}, Set] ⟶ [ℂ^{op}, Set]. The result now follows by tedious calculation of the extension of the two composites to the presheaf categories. □

In the proof of the Theorem 28, we have shown

Proposition 29 If T is a dense KZ-monad on Cat and X is an object of T 𝔻, then

\xymatrix{T ℂ ≅ T ℂ × 1 \ar[r]^{id_{T ℂ}×X} & T ℂ × T 𝔻 \ar[r]^{\overline{T}} & T (ℂ × 𝔻)}

is in Kl(T).

6.3 Products

As promised before, we now consider constructions of the form T ℂ × T 𝔻. We first mention that if T is a KZ-monad and T H strictly preserves any class of colimits, for H : ℂ → 𝔻 any functor between any two small categories, then it follows that every functor in Kl(T) preserves that class of colimits. However, because of a particularly subtle but important difference in category theory between the notions of strict preservation and ordinary preservation of a colimit, it need not follow that every functor in Kl(T) strictly preserves the class of colimits. We avoid analysing that distinction in the statement of the theorem, although resolutions are well known to us [16]. Suffice it to say that it follows from routine category theory that all our examples satisfy the hypotheses of the following theorem.

Theorem 30 Let T be a dense KZ-monad on Cat, and suppose every T ℂ has finite coproducts given by restriction from [ℂ^{op}, Set], and every functor in Kl(T) strictly preserves finite coproducts. Then the category T ℂ × T 𝔻 is isomorphic to T (ℂ + 𝔻) naturally in ℂ and 𝔻 and coherently with respect to the associative, commutative, and unitary structures of binary product and coproduct.

Proof: Using the universal property of the Kleisli construction, and using the universal properties of products and coproducts, in order to define a functor H : T (ℂ + 𝔻) ⟶ T ℂ × T 𝔻, we give functors from ℂ to each of T ℂ and T 𝔻 and from 𝔻 to each of T ℂ and T 𝔻. We define them by η_{ℂ} and the constant at the initial object of T 𝔻, and by duality. More in the detail, let

h_{0} : ℂ + 𝔻 → T ℂ

be defined as the copairing [η_{ℂ}, 0], where 0 : 𝔻 → T ℂ is the constant functor which always picks the initial object of T ℂ. Similarly define h_{1} = [0, η_{𝔻}]. Define H_{0} = μ_{ℂ}T h_{0} and H_{1} = μ_{𝔻}T h_{1}. Finally define H = ⟨H_{0}, H_{1}⟩.

We define K : T ℂ × T 𝔻 ⟶ T (ℂ + 𝔻) by sending (X, Y) to (T i_{0})X + (T i_{1})Y, where i_{0} : ℂ ⟶ ℂ+𝔻 and i_{1} : ℂ ⟶ ℂ+𝔻 are the left and right coprojections respectively. In other words K = +_{T (ℂ+𝔻)}(T i_{0} × T i_{1}).

We must show that H and K are mutually inverse. They are obviously natural in ℂ and 𝔻. To see that KH = id_{T (ℂ+𝔻)}, first see that KHη_{ℂ+𝔻} = η_{ℂ+𝔻}, which may be checked on each component. That follows routinely since T i_{0} strictly preserves the initial object, and dually. Now, since finite coproducts are given by restriction from [ℂ^{op}, Set] and using routine manipulation of diagrams, the commutativity extends to T (ℂ + 𝔻).

To see that HK = id_{T ℂ×T 𝔻}, we must verify that π_{0}HK = π_{0} and π_{1}HK = π_{1}, where π_{0} and π_{1} are the first and second projections from T ℂ×T 𝔻 respectively. By definition, π_{0}H and π_{1}H both lie in Kl(T), so preserve finite coproducts strictly. We restrict our attention to π_{0} the other case being dual. We then have the following

π_{0}HK = μ_{ℂ}T h_{0} +_{T (ℂ+𝔻)} (T i_{0} × T i_{1})  (by definition of H and K)
= μ_{ℂ} +_{T^{2}(ℂ)} (T h_{0} × T h_{0})(T i_{0} × T i_{1}) (since + is strictly preserved)
= μ_{ℂ} +_{T^{2}(ℂ)} (T (h_{0}i_{0}) × T (h_{0}i_{1}))
= μ_{ℂ} +_{T^{2}(ℂ)} (T η_{ℂ} × T 0)  (by definition of h_{0})
= +_{T (ℂ)}(μ_{ℂ} × μ_{ℂ})(T η_{ℂ} × T 0)  (since + is strictly preserved)
= +_{T (ℂ)}(μ_{ℂ}T η_{ℂ} × μ_{ℂ}T 0)
= +_{T ℂ}(id_{T ℂ} × 0)  (*)
= π_{0} ,

where the passage marked (∗) holds because μ_{ℂ}T η_{ℂ} = id_{T ℂ} by one of the monad laws; while μ_{ℂ}T 0 = 0 since by Theorem 23 μ_{ℂ}T 0 is Lan_{η_{ℂ}}(0) which can be checked by calculation to be necessarily the constant at 0. □

As promised, this theorem allows us to consider constructions of the form T ℂ × T ℂ ⟶ T ℂ, as required to model nondeterministic sum for example, as functors of the form T 𝔻 ⟶ T ℂ in Kl(T). So, such functors preserve open maps, hence functional bisimulations, as desired.

Remark 31 Theorem 30 is an instance of a limit/colimit coincidence result [26,28,8,31] . In particular, by categorical folklore, the coproduct in Kl(T), T (ℂ+𝔻) is also a bicategorical version of product because both Kl(T)[T ℂ, T (ℂ+ 𝔻)] and Kl(T)[T 𝔻, T (ℂ + 𝔻)] have coproducts that are preserved by composition and the coprojections

T (i) : T ℂ ⟶ T (ℂ + 𝔻) ⟵ T (𝔻) : T (j)

have right adjoints (that become projections for the product). Such a result allows us to conclude that T (ℂ + 𝔻) is a product in a bicategorical sense [30] but not in the strict sense we are asserting; that is, from the limit/colimit coincidence we could only deduce (in principle) an equivalence T (ℂ + 𝔻) ≃ T ℂ × T 𝔻 but not an isomorphism as we do in the proof of Theorem 30. Nonetheless the link of Theorem 30 to the more general question of when limits and colimits of certain diagrams of adjoint pairs coincide is worth exploring in greater detail also to see under what condition one can obtain limits in the usual categorical sense rather than in the bicategorical one.

6.4 Linear function spaces

In the development of presheaf models for process calculi, the monoidal closed structure of profunctors is associated with a form of linear function space which is used to model higher order processes, other function spaces being obtained with the help of appropriate exponentials (!)—see [34,7].

The analysis conducted so far also gives us an idea about how to model higher order structure with respect to the general monad T. Consider an extension of CCS that allows the passing of processes. To model that, we must consider a process that may accept some process and produce a process, something like a λ-abstraction (cf. [25]). So we want a notion of higher order object. Consideration of Kl(T) immediately provides one possibility: there is a natural isomorphism between the category Kl(T)[T (ℂ×𝔻), T 𝔼] and Cat[ℂ, Cat[𝔻, T 𝔼]]. So one might consider the category Cat[𝔻, T 𝔼] (or [𝔻, T 𝔼] for short) as a possible higher order construct. But note that unless Kl(T) is symmetric monoidal closed (which is rare), this construction is not iterable within Kl(T).

This function space construction may however be iterable within a monoidal closed full subcategory of Kl(T) by mimicking the way in which profunctors are considered monoidal closed in [34,11]. For example, suppose T is T_{ω} giving the countable colimit completion of a category. If a category 𝔻 is countable in the strong sense that both its objects and maps form countable sets, then its countable colimit completion T 𝔻 is equivalent to [𝔻^{op}, Set_{ω}], the full subcategory of presheaves over 𝔻 in which every set is countable. The full subcategory of Kl(T) consisting of objects T ℂ where ℂ is countable is monoidal closed; if 𝔻 and 𝔼 are countable then [𝔻, T 𝔼] is isomorphic to T (𝔻^{op}×𝔼) where the “function space” 𝔻^{op} × 𝔼 is also countable. An analogous observation holds for κ colimit completions, with infinite cardinal size κ replacing ω and countability.

There is a second category theoretically natural candidate for modelling a process passing CCS. For any 2-monad on Cat, the Kleisli 2-category Kl(T) embeds fully into the 2-category T −Alg, which is the other major construction one studies given a 2-monad (see [4]). For any regular cardinal κ, T_{κ}−Alg is the 2-category of small categories with colimits of size up to κ and functors that preserve them strictly. It follows from the Theorem 28 that for any dense KZ-monad T on Cat subject to a size condition that all our leading examples satisfy, the 2-category T −Alg is symmetric monoidal closed [19]. That closed structure is another candidate for modelling higher order structure. It is not clear how to define the notion of open map in this setting, but one might restrict attention to categories in Kl(T) and categories generated by applying a higher order construction to them.

In order to account for bisimulation at higher types, we need at the very least to extend the notion of open map from categories of the form T ℂ to categories of the form [𝔻, T 𝔼]. By construction, Cat[ℂ, [𝔻, T 𝔼]] is isomorphic to Kl(T)[T (ℂ × 𝔻), T 𝔼]. So, putting ℂ = 1 and considering this isomorphism on maps of the two categories, we see that to give a map in [𝔻, T 𝔼] is to give a natural transformation between functors in Kl(T) from T ℂ to T 𝔻. The weakest plausible definition is

Definition 32 (Tentative) A map α : X ⟶ Y in [𝔻, T 𝔼], i.e., a natural transformation between X and Y is open if every component of the corresponding natural transformation in Kl(T),

ᾱ =^{def} μ_{𝔼}T (α) ,

is open in T 𝔼.

Thus, Corollary 25 gives us

Proposition 33 For every functor F : T 𝔼 ⟶ T 𝔸 in Kl(T), composition with F sends open maps in [𝔻, T 𝔼] to open maps in [𝔻, T 𝔸].

Trivially, using the composition in Kl(T), composition with respect to 𝔻 also preserves open maps. Obviously, it must be tested against concerns arising naturally from concurrency, but we defer such investigations here.

Remark 34 We have marked the definition as tentative because there are other possibilities, for example that arising from the monoidal closed structure of profunctors which is not equivalent.

It might seem tempting in Definition 32 to define α to be open if every component α_{D}, for D an object of 𝔻, was open in T 𝔼. This definition would have had a significant drawback. Its choice would have meant that open maps were no longer closed under horizontal composition in Kl(T), i.e., α open in [𝔻, T 𝔼] and β open in [𝔼, T 𝔽] would not have implied that β∗α was open in [𝔻, T 𝔽]. In other words, restricting the 2-cells of Kl(T) to be open according to this choice of definition would not have yielded a sub-2-category of Kl(T). In computational terms, the definition would not have enforced that bisimilar abstractions acted on the same input process to give bisimilar outputs. This is surely the minimal requirement one expects of bisimulation for higher-order processes (the requirement is obviously satisfied by Definition 32). Note that the definition of open map and bisimulation in [34,11], arising from the monoidal closed structure of profunctors, is a stricter way to ensure that horizontal composition preserves openness than the condition of Definition 32 above (cf. Section 6.4).

7 Parallel composition and prefixing

We already mentioned in Section 3 that parallel composition and prefixing are not modelled as directly as the sum. Prompted by the desire to give an axiomatic treatment of these operations, we carry out some further analysis of Kl(T). We concentrate first on the class of examples given by the free completions under all colimits up to a certain size κ. The lifting operation of Definition 2, being a free colimit completion, induces a 2-monad on Cat:

Definition 35 Let (−)_{⊥} be the 2-monad on Cat that freely adds to a small category a strict initial object.

Definition 36 For any regular cardinal κ, let C_{κ} be the 2-monad on Cat that takes a small category ℂ to its free completion under all connected colimits of size less than κ.

Proposition 37 The 2-monad on Cat, T_{κ} that takes a small category ℂ to its free completion under all colimits of size less than κ can be factored as

T_{κ} = C_{κ}((−)_{⊥}) .

Corollary 38 For small categories ℂ and 𝔻,

Kl(C_{κ})[T_{κ}ℂ, T_{κ}𝔻] ≅ Kl(T_{κ})[T_{κ}ℂ_{⊥}, T_{κ}𝔻]

Proof:

Kl(C_{κ})[T_{κ}ℂ, T_{κ}𝔻] = Kl(C_{κ})[C_{κ}ℂ_{⊥}, T_{κ}𝔻]
≅ Cat[ℂ_{⊥}, T_{κ}𝔻]
≅ Kl(T_{κ})[T_{κ}ℂ_{⊥}, T_{κ}𝔻]
□

Hence there is a way of representing connected colimit preserving functors between T_{κ}ℂ and T_{κ}𝔻 as arrows of Kl(T_{κ}).

We now consider prefixing and parallel composition for CCS.

Prefixing: Let a ∈ A. Define pre_{a} : L_{⊥}^{+} → L^{+} as follows

\begin{matrix}⊥ & ⟼ & a \\ p & ⟼ & ap . \end{matrix}

By post-composing pre_{a} with η_{L^{+}} we obtain a functor L_{⊥}^{+} → T_{κ}(L^{+}), i.e., a connected colimit preserving functor,

P re_{a} : T_{κ}(L^{+}) → T_{κ}(L^{+}).

This defines precisely the usual prefixing operator on trees.

Parallel Composition: We wish to decompose the usual parallel composition of trees in terms of functors which preserves open map bisimulation. One starts from a functor

|| : L_{⊥}^{+} × L_{⊥}^{+} → T_{κ}(L^{+})

which defines the parallel composition of strings. By freeness, that induces an arrow ||_{!} : T_{κ}(L_{⊥}^{+} × L_{⊥}^{+}) → T_{κ}(L^{+}) in Kl(T_{κ}). In order to get

| : T_{κ}(L^{+}) × T_{κ}(L^{+}) → T_{κ}(L^{+})

one needs to embed T_{κ}(L^{+}) × T_{κ}(L^{+}) into T_{κ}(L_{⊥}^{+} × L_{⊥}^{+}). Recall that T_{κ} is commutative and that L_{⊥}^{+} ≅ L^{∗}. Notice that, if i : L^{+} → L^{∗} is the unit at L^{+} of the 2-monad, (−)_{⊥}, and η_{L^{∗}} : L^{∗} → T_{κ}(L^{∗}) is the unit at L^{∗} of the 2-monad T_{κ}, then Lanĩ(η_{L^{∗}}) : T_{κ}(L^{+}) → T_{κ}(L^{∗}), where ĩ : L^{∗} → T_{κ}(L^{+}) is uniquely determined by the universal property of the (−)_{⊥} completion, exists. Thus we can form the embedding

\xymatrix{T_{κ}(L^{+}) × T_{κ}(L^{+}) \ar[r]^{Lanĩ(η_{L^{∗}})×Lanĩ(η_{L^{∗}})} & T_{κ}(L^{∗}) × T_{κ}(L^{∗}) \ar[r]^{T̄_{(L^{∗},L^{∗})}} & T_{κ}(L^{∗} × L^{∗})} .

Call the composite above e, and define | = ||_{!}e. By Proposition 29, T̄ preserves colimits in both arguments separately, hence | preserves connected colimits in both arguments separately.

In [34,9] explicit descriptions based on decomposition results for presheaves were given of prefixing and parallel composition. In [9] it was suggested how to recover explicit descriptions in the above terms when T_{κ} is replaced by the presheaf completion.

Turning to bisimulation, we have

Proposition 39 Any strict connected κ-colimit preserving functor between T_{κ}(ℂ) and T_{κ}(𝔻) preserves epimorphic open maps.

Proof: A strict connected κ-colimit preserving functor F : T_{κ}(ℂ) → T_{κ}(𝔻) is an object of Kl(C_{κ})[C_{κ}(ℂ_{⊥}), C_{κ}(𝔻_{⊥})] (see Proposition 37). Hence by Corollary 25 F preserves ι_{ℂ_{⊥}}-open maps where ι : id ⇒ C_{κ} is the unit of the monad induced by the completion C_{κ}. To prove the result is then enough to show that ι_{ℂ_{⊥}}-open maps are the same as epimorphic η_{ℂ}-open maps, where η : id ⇒ T_{κ} is the unit of the monad induced by T_{κ}. Let f : D → E be an epimorphic η_{ℂ}-open map. To check that f is also ι_{ℂ_{⊥}}-open one needs to verify that any commuting square like the following

\xymatrix{ι_{ℂ_{⊥}}(C) \ar[r] \ar[d] & D \ar[d]^{f} \\ ι_{ℂ_{⊥}}(C′) \ar[r] & E}

can be split into two commuting triangles. If both C and C′ are different from ⊥ this is ensured by the fact that f is η_{ℂ}-open together with the obvious fact that η_{ℂ} factorises as

ℂ ↪ ℂ_{⊥} →^{ι_{ℂ_{⊥}}} C_{κ}(ℂ_{⊥}) = T_{κ}(ℂ) .

If C = C′ = ⊥ the property holds even more obviously, while if C = ⊥ ≠ C′, the property reduces to show that the objects of ℂ along the embedding η_{ℂ} are strongly projective (see [21] for a definition) in T_{κ}(ℂ), but this can be verified by observing that the embedding η̃_{ℂ} preserves epimorphisms and by recalling that the representables in [ℂ^{op}, Set] are strongly projective [21]. On the other hand if f is ι_{ℂ_{⊥}}-open it is certainly η_{ℂ}-open because of the factorisation of η_{ℂ} recalled above. To check that it is also epimorphic, assume that g, h : E → E′ are two arrows of T_{κ}(ℂ) such that gf = hf. Then

ι̃_{ℂ_{⊥}}(g)ι̃_{ℂ_{⊥}}(f) = ι̃_{ℂ_{⊥}}(gf) = ι̃_{ℂ_{⊥}}(hf) = ι̃_{ℂ_{⊥}}(h)ι̃_{ℂ_{⊥}}(f) .

Moreover ι̃_{ℂ_{⊥}}(f) is y_{ℂ_{⊥}}-open, and ι̃_{ℂ_{⊥}}(D) and ι̃_{ℂ_{⊥}}(E) are rooted presheaves, meaning that ι̃_{ℂ_{⊥}}(D)(⊥) ≅ {∗} ≅ ι̃_{ℂ_{⊥}}(E)(⊥). It is known [15,10,7] that y_{ℂ_{⊥}}- open maps between rooted presheaves are always epimorphic, hence

ι̃_{ℂ_{⊥}}(g) = ι̃_{ℂ_{⊥}}(h)

and therefore, since ι̃_{ℂ_{⊥}} is full and faithful, g = h. □

As a corollary we then have the following

Corollary 40 Prefixing and parallel composition functors on synchronisation trees preserve bisimulation.

We conclude this section by showing a way of axiomatising the situation just described, where the composite of two 2-monads gives rise to a third one together with congruence properties with respect to bisimulation from open maps. Let R be a dense KZ-monad on Cat and let S be another 2-monad on Cat (not necessarily KZ). By a distributive law of S over R one means a natural transformation δ : SR ⇒ RS that preserves multiplications and units of the two 2-monads [1]. If such a distributive law is given, then a 2monad structure is induced on the composite functor T = RS. So we have (cf. Corollary 38)

Kl(R)[T ℂ, T 𝔻] ≅ Kl(T)[T Sℂ, T 𝔻] .

In particular, one obtains a functor in Kl(R) from a functor F : T Sℂ → T 𝔻 in Kl(T), by precomposing F with Rη_{Sℂ} : T ℂ = RSℂ → RSSℂ = T Sℂ, where η : Id ⇒ S is the unit of S. Moreover, at each ℂ, Rη_{Sℂ} sends open maps with respect to Sℂ to open maps with respect to SSℂ, as we saw in Corollary 23. So, if one has that, in T ℂ, being open map bisimilar with respect to ℂ implies being open map bisimilar with respect to Sℂ, then every functor in Kl(R) of domain T ℂ preserves open map bisimulation with respect to ℂ.

In our case this specialises to S = (−)_{⊥} and R = C_{κ}. Although this may seem a heavy way to axiomatise something for which we have so far given only one substantial example, note that even in this single case it is easier to check that it satisfies all the needed requirements than it is to provide a direct proof.

Of course, the point of an axiomatisation is to open up to useful generalisations, and here a shift of viewpoint is helpful. In general terms the construction above expands the maps in the Kleisli category Kl(T) to cover a broader range of operations. A related construction is used in models for linear logic. There the exponential ! of linear logic is represented as a (special kind of) comonad on the category of linear maps and a model of intuitionistic logic, requiring more generous maps, is obtained as the coKleisli category of !. It is notable that the axiomatisation we have been led to in accommodating the operations of prefixing and parallel composition induces a setting familiar from linear logic.

Theorem 41 Assume 2-monads (S, η^{S}, μ^{S}) and (R, η^{R}, μ^{R}) on Cat, and a distributive law of S over R. Then, S induces a 2-comonad S′ on Kl(T), the Kleisli category for the 2-monad (T, η^{T} , μ^{T}) induced on the composite functor T = RS. The functor S′ acts like S on objects.

PROOF. If, under the isomorphism Kl(T)[T ℂ, T 𝔻] ≅ Cat[ℂ, T 𝔻], H : ℂ → T 𝔻 is an arrow of Kl(T), S′(H) is defined as the composite

(Rη_{S𝔻}^{S})(μ_{𝔻}^{T})(η_{ST 𝔻}^{R})(SH) .

The action on natural transformations α : H ⇒ H′ is defined similarly. The counit ε and comultiplication ρ are defined as ε = η_{S}^{R} and ρ = η_{SS}^{T}η_{S}^{S}. It is worth noticing that the result follows also axiomatically by dualising in the spirit of [29], the characterisation of distibutive laws in terms of monad liftings given in [1].

Taking S = (−)_{⊥} and R = C_{κ}, we see lifting as a comonad on the Kleisli category Kl(T_{κ}), when it behaves like a very weak exponential; it is weak in the sense that we cannot expect its coKleisli category to be cartesian closed.

Another example: Take S to be the functor giving the finite colimit completion of a small category, R to be the κ-filtered colimit completion functor. Then the composite T = RS is the κ-colimit completion functor. In this case the coKleisli category consists of κ-accessible categories with κ-filtered colimit preserving functors, an analogue of algebraic cpo’s and continuous functions.

In the last example, it will not be the case that, in T ℂ, being open with respect to ℂ implies being open with respect to Sℂ, and not every functor in the coKleisli category preserves open maps with respect to ℂ. However, there seem to be interesting variations on the choice of S and R, corresponding intuitively to the different degrees that operations may copy their arguments, with respect to which functors in the coKleisli category preserve open maps.

8 Conclusions and further work

We have considered dense KZ-monads T on Cat, and deduced the existence of various structures on the 2-category Kl(T) that allow us to give an axiomatic account of functional bisimulation, showing that various constructors such as prefixing, nondeterministic sum, and a parallel operator, may axiomatically be seen as preserving functional bisimulations. We have proved, under an additional condition, that Kl(T) has finite products and coproducts (and they agree), and a symmetric monoidal structure, and it supports some higher order structure. The axioms hold of all KZ-monads induced by free colimit completions as outlined in Section 4. In future work we plan to refine the axiomatisation in two areas, to support more fully the treatment of higher order processes and to test out the robustness of the axiomatisation given in Section 7 in supporting the range of operations arising in process calculi.

The obvious closely related work, in fact work on which our Theorem 23 depends, was that of [10] which considered categories of presheaves and profunctors. In fact, the free completion under all colimits of a small category ℂ is equivalent to the category [ℂ^{op}, Set]. A proof appears in [16]. It is one of the fundamental theorems of category theory. However, the free completion under all colimits, unlike our examples of Section 4, does not form a 2-monad on Cat. The reason is size: if ℂ is a small category, then so are T_{ω}ℂ, T_{ω_{1}}ℂ, and T_{κ}ℂ, but [ℂ^{op}, Set] is not, so it is not an object of Cat. However, one can pass to a larger universe of sets. Doing this allows us to see some of the results about presheaf categories and profunctors in our terms. Specifically, our work here gives independent proofs that the 2-category of free completions under all colimits, with strict colimit preserving functors, has all finite products and coproducts (and they agree), and is symmetric monoidal, with symmetric monoidal structure given by T (ℂ × 𝔻).

In fact, more is true of this particular 2-category, well-known to be biequivalent to the bicategory of profunctors. In particular, unlike examples given by dense KZ-monads in general, it is symmetric monoidal closed and so provides models for higher order processes (see [34,11]). In the light of the above paragraph, that construction can also be seen axiomatically, by considering a full subcategory of Kl(T) for a particular dense KZ-monad T. As we saw in Section 6.4, the same axiomatisation would be appropriate for any KZ-monad T of the form T_{κ} for an infinite cardinal κ; the monoidal closure of profunctors would cut down to monoidal closed structure on full subcategories of Kl(T) whose objects T 𝔻 were subject to a size restriction on 𝔻. One of our major goals in further work is to study bisimulation on higher order processes in more depth.

Another main goal for future work is the study of weaker forms of equivalence. An obvious such class of equivalences to consider here are those given by weak bisimulation. That involves a construction that takes a tree to another tree, broadly but not precisely by a quotienting operation. Another obvious class of equivalences here are those given by contextual equivalence, for instance testing or failures equivalence. We hope to pursue one of those equivalences too.

Finally, we seek an operational account of the structures we are developing. As in [11], this may provide new versions of process passing calculi with a firm semantic foundation.

References

[1] M. Barr, C. Wells. Toposes, triples and theories. Springer-Verlag, 1985.

[2] D. B. Benson and O. Ben-Schachar. Bisimulation of automata. Information and Computation, 79:60–83, 1988.

[3] J. van Bentham. Correspondence theory. In M. Gabbay and Guenther, editors, Handbook of Philosophical Logic, volume 2, pages 167–247. Reidel, 1984.

[4] R. Blackwell, G.M. Kelly, and A.J. Power. Two-dimensional monad theory. Journal of Pure and Applied Algebra, 59:1–41, 1989.

[5] F. Borceux. Handbook of categorical algebra, vol. 1. CUP, 1994.

[6] I. Castellani. Bisimulation and abstraction homomorphisms. J. Comput. System Sci., 34(2-3):210–235, 1987.

[7] G. L. Cattani. Presheaf models for concurrency. PhD thesis, University of Aarhus, 1999. Forthcoming.

[8] G. L. Cattani, M. Fiore, and G. Winskel. A theory of recursive domains with applications to concurrency. In Proceedings of LICS ’98, pages 214– 225, IEEE Press, 1998.

[9] G. L. Cattani, I. Stark, and G. Winskel. Presheaf models for the π-calculus. In Proceedings of CTCS ’97, LNCS 1290, pages 106–126, 1997.

[10] G. L. Cattani and G. Winskel. Presheaf models for concurrency. In Proceedings of CSL’ 96, LNCS 1258, pages 58–75, 1997.

[11] G. L. Cattani and G. Winskel. On bisimulation for higher order processes. Manuscript, 1998.

[12] M. Fiore, G. L. Cattani and G. Winskel. Weak bisimulation and open maps. Manuscript, 1998.

[13] B. Jacobs and J. Rutten. A tutorial on (Co)algebras and (Co)induction. EACTS Bulletin 62 (1997) 222-259.

[14] A. Joyal and I. Moerdijk. A completeness theorem for open maps. Annals of Pure and Applied Logic, 70:51–86, 1994.

[15] A. Joyal, M. Nielsen, and G. Winskel. Bisimulation from open maps. Information and Computation, 127:164–185, 1996.

[16] G.M. Kelly. Basic concepts of enriched category theory. London Math. Soc. Lecture Note Series 64, CUP, 1982.

[17] G.M. Kelly and R. Street. Review of the elements of 2-categories. In Proceedings of Sydney Category Theory Seminar 1972/73, LNM 420, pages. 75–103, Springer-Verlag, 1974.

[18] A. Kock. Monads for which structures are adjoint to units. Journal of Pure and Applied Algebra, 104:41–59, 1995

[19] A. Kock. Closed categories generated by commutative monads. Journal of the Australian Mathematical Society, 12:405–424, 1971.

[20] S. Mac Lane. Categories for the working mathematician. Springer-Verlag, 1971.

[21] S. Mac Lane and I. Moerdijk. Sheaves in geometry and logic: A First Introduction to Topos Theory. Springer-Verlag, 1992.

[22] R. Milner. Communication and concurrency. Prentice Hall, 1989.

[23] A. J. Power and E. Robinson. Premonoidal categories and notions of computation. Math. Struct. in Comp. Science, 7:453–468, 1997.

[24] A. J. Power, G. L. Cattani and G. Winskel. A representation result for free cocompletions. Research Series RS-98-21, BRICS, Department of Computer Science, University of Aarhus, 1998.

[25] D. Sangiorgi. Bisimulation for higher-order process calculi. Information and Computation, 131(2):141–178, 1996.

[26] D. S. Scott. Continuous lattices. In F.W. Lawvere, editor, Toposes, Algebraic Geometry and Logic, LNM 274, pages 97–136. Springer-Verlag, 1972.

[27] K. Segerberg. Decidability of S4.1. Theoria, 34:7–20, 1968.

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

[29] R. Street. Formal theory of monads. Journal of Pure and Applied Algebra, 2:149–168, 1972.

[30] R. Street. Fibrations in bicategories. Cahiers de Topologie et Géométrie Différentielle, XXI(2):111-160, 1980.

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

[32] Glynn Winskel. Synchronisation trees. Theoretical Computer Science, 34:33–82, 1985.

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

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