                    In Proceedings of CONCUR '98, \begin{matrix}c \\ ◯ \end{matrix}Springer-Verlag

A Categorical Axiomatics for Bisimulation

Gian Luca Cattani^{1}, John Power^{2,}^{⋆}, Glynn Winskel^{1}

1BRICS^{⋆⋆}, University of Aarhus, Denmark 2LFCS, University of Edinburgh, Scotland

Abstract. We give an axiomatic category theoretic account of bisimulation in process algebras based on the idea of functional bisimulations as open maps. We work with 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, that 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.

Introduction

We seek a category theoretic axiomatic account of bisimulation as studied in concurrency, for instance by Milner [16]. There have been several category theoretic approaches to bisimulation [8, 10]. One of them, initiated by Joyal, Nielsen, and Winskel [10], 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. Our work, although essentially generalising theirs, suggests ways of modelling higher order processes that were not present (because of size problems) in the presheaf approach, but on the contrary, does not directly include the natural way of representing higher order processes in terms of internal homs that has been suggested for presheaf models [22, 7]. We shall expand on this in Section 6.

⋆ This work is supported by EPSRC grant GR/J84205: Frameworks for programming

language semantics and logic. ⋆⋆ Basic Research in Computer Science, Centre of the Danish National Research Foun-

dation.

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 [10, 9], 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 L^{+} 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 [10]. 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 [5] for a more detailed discussion).Third, it is not clear how to model weak notions of bisimulation. 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 [22, 6, 5].

We first observe 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, as we shall see in Section 2. The construction of countable colimit completions extends to a 2-monad T on Cat with strong category theoretic properties, as explained in Sections 2 and 3. 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.

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. The notion of open map agrees, in our leading examples, with the usual notion of functional bisimulation. That forms the content of Section 3.

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 a candidate for higher order structure (though outside Kl(T)), allowing a possible way to model a process passing extension of CCS. This analysis forms Sections 4 and 5.

Finally, in Section 6, we compare, especially as far as higher order is concerned, this work with that of [22, 6, 5, 7] 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 such a large issue that it requires a full paper devoted to it. There are delicate points involved. First, we do have some ideas about how one might approach it directly, as it amounts to an operation that takes a tree representing strong bisimulation and replacing it by a tree that is essentially but not quite a quotient, representing weak bisimulation. We hope that our axiomatics may allow that, but we are not sure yet. Second, it is not clear to us yet 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 [16] with models given by labelled synchronisation trees; but our analysis holds more generally (see [10]).

Definition 1. Let L be a set, not including the the letter τ among its elements. Let L̄ = {ā | a ∈ L}, and define the category L whose objects are strings of arbitrary length, possibly infinite, of elements of L ∪ L̄ ∪ {τ}, where a map from p to q is a prefixing of q by p, with composition given by composing inclusions. The category L^{↑} is the full subcategory of non empty strings and L^{+} is the restriction of L^{↑} to strings of finite length.

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 [15]. Thus we have

Proposition/Example 2. 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 [16]. That yields the category of countably branching trees, and we have

Proposition/Example 3. 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/Example 4. 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, 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 manysorted operations on trees to represent nondeterministic sum and the like. So we seek an axiomatic account of these constructions.

2 The general setting

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

Definition 5. 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 2natural transformations μ : T^{2} ⇒ T and η : id ⇒ T, 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 [12], 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 6. For any regular cardinal, κ, T_{κ} extends to a 2-monad on Cat.

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 7. 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 8. 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 5 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.

Remark 9. The analysis conducted so far also gives us an idea about how to model higher order structure. 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. [18]). 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). It may however be iterable within a monoidal closed subcategory of Kl(T) by mimicking the way in which profunctors are considered monoidal closed in [22, 7]. 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.

An object of [𝔻, T 𝔼] is equivalent to a functor from T 𝔻 to T 𝔼 in Kl(T), which in the case of finitely branching trees, is how we model operators on processes such as nondeterministic sum. We shall return to this construction when we analyse functional bisimulation in the next section.

3 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 [10], but for concreteness, we shall continue to restrict our attention to CCS as modelled by synchronisation trees, and the notion of functional bisimulation there. For any 2-monad T on Cat, we can define the notion of open map on T ℂ for arbitrary ℂ, cf [10].

Definition 10. Given a 2-monad T on Cat and a small category ℂ, an arrow h : X ⟶ Y in T ℂ is open if for any commuting square

\xymatrix{η_{ℂ}(c) \ar[r]^{p} \ar[d]_{η_{ℂ}(m)} & X \ar[d]^{h} \\ η_{ℂ}(c′) \ar[r]_{q} & Y}

with m : c → c′ in ℂ, there exists a map

\xymatrix{η_{ℂ}(c) \ar[r]^{p} \ar[d]_{η_{ℂ}(m)} & X \ar[d]^{h} \\ η_{ℂ}(c′) \ar@{.>}[ur]^{r} \ar[r]_{q} & Y}

such that the two triangles commute.

Note 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 [10].

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 dually. This is exactly to say, in modelling CCS by finitely branching trees, that open maps are preserved by the functor

+ : T ℂ × T ℂ ⟶ T ℂ .

Thus we want a condition on T satisfied by all our examples and such that functors in Kl(T) preserve open maps. The first major result of the paper gives such a condition. First, we need some definitions.

Definition 11. 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 [13, 21]).

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

Example 12. 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.

• Given functors H : C ⟶ D and J : C ⟶ C′, the left Kan extension of H along J is given by a functor Lan_{J}H : C′ ⟶ D and a natural transformation α : H ⇒ (Lan_{J}H)J that is universal among such natural transformations, i.e., given any functor K : C′ ⟶ D and any natural transformation β : H ⇒ KJ, there exists a unique natural transformation γ : Lan_{J}H ⇒ K such that β = γ_{J}α.

If it exists, a left Kan extension is unique up to coherent isomorphism. If J is fully faithful and a left Kan extension exists, then α is necessarily an isomorphism. The left Kan extension always exists if C is a small category and D is cocomplete (see [15], [11] or [3] for more detail on left Kan extensions, see [6] for applications to concurrency).

Definition 13. 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 : C ⟶ D, 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.

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 [11] 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. We have

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

Now we can state our first major theorem.

Theorem 15. 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 KZmonad 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 = μ_{𝔻}K where K = F η_{ℂ} : ℂ ⟶ T 𝔻. Using the density condition applied to K and the definition of KZ-monad, and the fact that left Kan extensions into cocomplete categories (such as [(T 𝔻)^{op}, Set]) are colimits, so are preserved by functors with right adjoints, gives the result.

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 ℂ}} η̃_{ℂ}. 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 16. Given a dense KZ-monad T on Cat, for every ℂ, μ_{ℂ} is the left Kan extension of id : T ℂ ⟶ T ℂ along η_{T ℂ} : T ℂ ⟶ T^{2}ℂ and is the restriction of [η_{ℂ}, Set] : [T ℂ^{op}, Set] ⟶ [ℂ^{op}, Set].

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

Proof. Given a small category ℂ, one may define open maps in [ℂ^{op}, Set] just as we did in T ℂ, with openness relative to the Yoneda embedding y_{ℂ} : ℂ ⟶ [ℂ^{op}, Set]. It was stated in [6] (a proof will appear in the forthcoming PhD thesis of the first author of this paper) that all functors of the form Lan_{y_{ℂ}}(y_{𝔻}H) : [ℂ^{op}, Set] ⟶ [𝔻^{op}, Set] preserve open maps. Since η_{ℂ} and η̃_{ℂ} are both fully faithful, a map in T ℂ is open if and only if its image under η̃_{ℂ} is open. Putting that together with Theorem 15 yields the result.

We regard this corollary as fundamental for the reasons outlined above. In order to account for bisimulation at higher types, we need 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 18. 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} μ_{E}T (α) ,

is open in T 𝔼.

Thus, Corollary 17 gives us

Proposition 19. 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. This suggests a notion of functional bisimulation at higher types arising from category theoretic principles. Obviously, it must be tested against concerns arising naturally from concurrency, but we defer such investigations here.

Remark 20. It might seem tempting in Definition 18 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 18). Note that the definition of open map and bisimulation in [22, 7], arising from the monoidal closed structure of profunctors, is a stricter way to ensure that horizontal composition preserves openness than the condition of Definition 18 above.

Theorem 15 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 15, to characterise dense KZ-monads in those terms. That is beyond the scope of this paper (see [17]), but we do remark that the precise statement is very subtle. For instance,

Example 21. 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.

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

Based upon our results of the previous two sections, in particular Corollary 17, 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 3.

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

Proposition 22. 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 does not immediately appear to be of computational interest, although it does generalise a domain theoretic property on ω−Cpo which is used to model conditional statements. However, 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 have

Theorem 23. 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. 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 23, we have shown

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

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

is in Kl(T).

This opens a second category theoretically natural candidate for modelling 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 [1]). It follows from the Theorem 23 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 [14]. 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; it may be possible to define open maps for any such category similarly to the previous section; but we leave that for further work.

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.

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 [11]. Suffice it to say that it follows from routine category theory that all our examples satisfy the hypotheses of the following theorem.

Theorem 25. 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.

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.

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. Restricting our attention to π_{0}, the other case being dual, it suffices to show that (π_{0}H × π_{0}H)(T i_{0} × T i_{1}) sends (X, Y) to (X, 0), where 0 is the initial object of T ℂ. Again, this amounts to two commutativities.

For the first, observe that π_{0}H = μ_{C}T (η_{C}, 0), so precomposing with T i_{0} yields the identity since (η_{ℂ}, 0)i_{o} = η_{ℂ} and by one of the monadic unit laws, giving the desired commutativity.

For the second, by a similar calculation, it suffices to show that the lifting of the constant functor 0 : 𝔻 ⟶ T ℂ to T 𝔻 is the constant functor at the initial object 0 of T ℂ. But by Theorem 15, the lifting is given by the left Kan extension of 0 : 𝔻 ⟶ T ℂ along η_{ℂ} : ℂ ⟶ T ℂ; and one can check by calculation that that is necessarily the constant at 0.

As promised before, 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 26. Theorem 25 is an instance of a limit/colimit coincidence [19, 20, 4]. 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 [21] 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 25. Nonetheless the link of Theorem 25 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.

5 Parallel Composition and Prefixing

We already mentioned in Section 2 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 κ.

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

Definition 28. 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 29. 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 30. 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 ∈ L. Define pre_{a} : L_{⊥}^{+} → L^{+} as follows

⊥ ↦ a
p ↦ ap

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: One starts from a functor

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

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 note that, if i : L → L_{⊥} is the unit at L of the 2-monad, (−)_{⊥}, and η : L_{⊥} → T_{κ}(L_{⊥}) is the unit at L_{⊥} of the 2-monad T_{κ}, then Lanĩ(η_{L_{⊥}}) : T_{κ}(L) → T_{κ}(L_{⊥}) exists, hence 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 24, T̄ preserves colimits in both arguments separately, hence | preserves connected colimits in both arguments separately.

In [22, 5] explicit descriptions based on decomposition results for presheaves were given of prefixing and parallel composition. In [5] 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 31. Any connected colimit preserving functor between T_{κ}(ℂ) and T_{κ}(𝔻) preserves epimorphic open maps.

Corollary 32. 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 mean a natural transformation δ : SR ⇒ RS that preserves multiplications ad units of the two 2-monads [2]. If such a distributive law is given, then a 2-monad structure is induced on the composite functor T = RS. So we have (cf. Corollary 30)

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 15. So, if one has that, in T ℂ, being open with respect to ℂ implies being open with respect to Sℂ, then the every functor in Kl(R) of domain T ℂ preserves open maps 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 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.

6 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 all hold of for KZ-monads induced by free colimit completions as outlined in Section 3.

The obvious closely related work, in fact work on which our Theorem 15 depends, was that of [6] 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 [11]. It is one of the fundamental theorems of category theory. However, the free completion under all colimits, unlike our examples of Section 3, 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 [22, 7]). 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. By Remark 9, ending Section 2, 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 [7], this may provide new versions of process passing calculi with a firm semantic foundation.

References

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

2. M. Barr, C. Wells. Toposes, Triples and Theories. Springer-Verlag, 1985.

3. F. Borceux. Handbook of Categorical Algebra, vol. 1. CUP, 1994.

4. G. L. Cattani, M. Fiore, and G. Winskel. A Theory of Recursive Domains with Applications to Concurrency. To appear in Proceedings of LICS ’98.

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

6. G. L. Cattani and G. Winskel. Presheaf Models for Concurrency. In Proceedings of CSL’ 96, LNCS 1258, pages 58–75, 1997.

7. G. L. Cattani and G. Winskel. On bisimulation for higher order processes. Manuscript, 1998.

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

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

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

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

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

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

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

15. S. Mac Lane. Categories for the working mathematician. Springer-Verlag, 1971.

16. R. Milner. Communication and concurrency. Prentice Hall, 1989.

17. A. J. Power, G. L. Cattani and G. Winskel. A representation result for free cocompletions. Submitted for publication.

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

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

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

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

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