Presheaf Models for CCS-like Languages

Gian Luca Cattani^{a,1} Glynn Winskel^{b}

aComputer Laboratory, University of Cambridge, New Museums Site, Pembroke Street, Cambridge CB2 3QG, UK. Email: Luca.Cattani@cl.cam.ac.uk

bBRICS^{2}, Department of Computer Science, University of Aarhus, Ny Munkegade bldg. 540, 8000 Aarhus C, DK. Email: gwinskel@brics.dk

Abstract

The aim of this paper is to harness the mathematical machinery around presheaves for the purposes of process calculi. Joyal, Nielsen and Winskel proposed a general definition of bisimulation from open maps. Here we show that open-map bisimulations within a range of presheaf models are congruences for a general process language, in which CCS and related languages are easily encoded. The results are then transferred to traditional models for processes. By first establishing the congruence results for presheaf models, abstract, general proofs of congruence properties can be provided and the awkwardness caused through traditional models not always possessing the cartesian liftings, used in the break-down of process operations, are side-stepped. The abstract results are applied to show that hereditary historypreserving bisimulation is a congruence for CCS-like languages to which is added a refinement operator on event structures as proposed by van Glabbeek and Goltz.

1 This author is supported by EPSRC grant GR/L62290: Calculi for Interactive Systems: Theory and Experiment. 2 Basic Research in Computer Science, a centre of the Danish National Research Foundation.

Preprint submitted to Elsevier Preprint 9 November 1999 Contents

1 Preliminaries 4 1.1 Traditional models 5 1.2 Bisimulation from open maps 6 1.3 Presheaves as non-deterministic processes 8 1.4 Left Kan extensions 11 1.5 Fibred categories 14 1.6 The Grothendieck construction 16 2 A general process language and its categorical models 21 2.1 Denotational semantics of Proc 22 3 Presheaf models for Proc 24 3.1 The Grothendieck construction for presheaf models 26 4 Semantic constructions in Groth(ℙ_{(−)}) 29 5 Concrete models revisited 38 6 Refinement for event structures 41 References 45

Introduction

Joyal and Moerdijk’s open maps [18] led to an abstract view of bisimulation [19], applicable to models for concurrency once they are presented as categories, along the lines of the handbook chapter [29]. A central idea was to define bisimulation through a span of open maps and explore its consequences over models for concurrency ranging from “interleaving” models like transition systems to “independence” models like event structures, and later on Petri nets [23], in which concurrency or parallelism of actions is expressed by some relation of independence. This paper takes up the suggestion of [19] to study presheaf models for concurrent computation. There are several reasons for doing this.

One reason is that, once one passes the barrier of unfamiliarity, presheaves form an intuitively appealing model of nondeterministic computation. Nondeterministic computations are identified with presheaves over a path category; objects of the path category specify the possible shapes of computation paths while its morphisms specify how one path can be extended to another. Because the presheaf category is equivalent to the category obtained by freely adjoining all colimits to the original path category, an individual presheaf is obtained, in effect, by identifying subpaths within a collection of computation paths.

As was argued in [19] presheaf models are promising generalisations of existing models. This is because well-known models like synchronisation trees and labelled event structures embed fully and faithfully into appropriate presheaf categories, and, for general reasons, presheaves support operations such as those coming from Kan extensions [21,2]. One particular Kan extension, resulting in a functor between presheaves over pomsets, was advanced as a good candidate for an operation of refinement of the kind proposed for event structures. Here it is shown that this Kan extension acts, when restricted to presheaves associated with event structures, in the same way as the refinement operation on event structures proposed by Goltz and van Glabbeek in [12]. To highlight the gain of working at a more abstract level than is common in concurrency theory, we can often exploit an important general result [6,3] that any colimit-preserving functor between presheaf categories automatically preserves open maps. In particular, this result specialises to show that the refinement, obtained as a Kan extension, preserves open maps and so open-map bisimulation.

One point of approaching models for concurrency as categories is that operations fundamental to process calculi appear automatically, as built out of universal constructions. An obvious question is whether these universal constructions preserve open maps and therefore bisimulation. Our approach here is to prove that operations on presheaves preserve open maps and then transfer these preservation properties to concrete models like synchronisation trees and event structures, through canonical embeddings using results such as Proposition 69.^{3} Working with presheaves also avoids some obstructions to a treatment of weak bisimulation on independence models [10], though this topic is not dealt with here.

A more general, and probably the most important, motivation for presheaf models is the hope they give of making concurrency less separate a study. Through presheaf models we are trying to bring concurrency theory within

3 The paper [8] shows that any “ℙ-factorisable functor” preserves open maps and so bisimulation. In contrast we aim to take advantage of the preservation properties of universal constructions—a strategy proposed in the conclusion of [19].

domain theory, though with the proviso that this should be understood liberally enough to include generalisations of domain theory like those envisaged in “axiomatic domain theory” [24,9,11]. The use of presheaves as models for concurrency is not confined to languages expressible in Proc. For instance, following the work in [28] a treatment of presheaf categories as domains has been devised [7,4] and applied to the constructions of presheaf models for more sophisticated languages [5,3]. Other applications, to nondeterministic dataflow, fairness and weak bisimulation, can be found in [16,15,10].

Specifically, this paper builds on the analysis of the handbook chapter [29], with open map bisimulation in mind, to axiomatise a presheaf based semantics of the “general purpose” process language Proc treated there. On top of the categorical structure which is needed for the semantics of Proc, phrased in terms of fibrations, we require the satisfaction of two conditions borrowed from categorical logic, the Beck-Chevalley condition and the Fröbenius Reciprocity law. These two conditions are important in proving the general congruence results of bisimulation that are expected. The analysis of the constructions involved in the semantics of Proc together with the corresponding preservation properties of open map bisimulation form the core of the paper. As an application of the general congruence results, we show that hereditary history-preserving bisimulation [19,1] is a congruence for Proc and conclude by proving that the refinement of event structures proposed in [12] preserves hereditary history-preserving bisimulation.

The paper is organised as follows. In the first section we recall the basic definitions and results from concurrency and category theory that we will need in order to make the paper reasonably self-contained. Section 2 introduces the language Proc and discusses the appropriate notion of categorical model for it. Section 3 defines presheaf models for Proc and in the following section the relevant semantic constructions are discussed and proved to preserve bisimulation. Section 5 and 6 present the two applications to hereditary historypreserving bisimulation and event structures discussed above.

An earlier extended abstract of this paper appeared as [6].

1 Preliminaries

This section recalls three fundamental models for concurrent computation and provides the categorical background.

1.1 Traditional models

We focus on three traditional models for concurrency: transition systems, synchronisation trees and event structures (see [29] for more background). A transition system is a structure (S, i, L, tran) where

• S is a set of states with initial state i,

• L is a set of labels,

• tran ⊆ S × L × S is the transition relation. Usually, a transition (s, a, s′) is written as s ^{\underline{a}}→ s′.

Let T_{0} = (S_{0}, i_{0}, L_{0}, tran_{0}) and T_{1} = (S_{1}, i_{1}, L_{1}, tran_{1}) be transition systems. A morphism f : T_{0} → T_{1} is a pair f = (σ, λ) where

• σ : S_{0} → S_{1}, such that σ(i_{0}) = i_{1}, and

• λ : L_{0} ⇀ L_{1}, a partial function, which together satisfy

(s, a, s′) ∈ tran_{0} & λ(a) defined
⟹ (σ(s), λ(a), σ(s′)) ∈ tran_{1}, and
(s, a, s′) ∈ tran_{0} & λ(a) undefined ⟹ σ(s) = σ(s′).

A synchronisation tree is a transition system whose transition graph has the form of a tree with root the initial state.

Definition 1 (The Categories T S and ST ) Define T S to be the category of objects transition systems and arrows transition systems morphisms. The composition of arrows is defined componentwise.

Define ST to be the full subcategory of T S of Synchronisation Trees.

Transition systems and synchronisation trees are often called “interleaving models” because they represent parallel/concurrent composition by nondeterministically interleaving the actions of processes. In contrast, event structures represent a class of “independence models” (among them Petri nets) in which concurrency is represented directly as a form of causal independence.

Define a (labelled) event structure to be a structure (E, ≤, Con, l) consisting of a set E, of events which are partially ordered by ≤, the causal dependency relation, a consistency relation Con which is a non-empty family of finite subsets of events, and a labelling function l : E → L, which satisfy

{e′ | e′ ≤ e} is finite,
{e} ∈ Con,
Y ⊆ X ∈ Con ⟹ Y ∈ Con,
X ∈ Con & e ≤ e′ ∈ X ⟹ X ∪ {e} ∈ Con,

for all events e, e′ and their subsets X, Y. Two events e, e′ ∈ E are said to be concurrent (causally independent) iff

(e ≰ e′ & e′ ≰ e & {e, e′} ∈ Con).

A set, x, of events in E is said to be a configuration if it is

downwards-closed: ∀e, e′. e′ ≤ e ∈ x ⟹ e′ ∈ x, and
consistent: ∀X. X finite & X ⊆ x ⟹ X ∈ Con.

A morphism of event structures consists of

(η, λ) : E → E′,

where E = (E, ≤, Con, l), E′ = (E′, ≤′, Con′, l′) are event structures, η : E ⇀ E′ is a partial function on events, λ : L ⇀ L′ is a partial function on labelling sets such that

(i) l′ ∘ η = λ ∘ l, (ii) If x is a configuration of E, then ηx is a configuration of E′ and if for

e_{1}, e_{2} ∈ x their images are both defined with η(e_{1}) = η(e_{2}), then e_{1} = e_{2}.

Definition 2 (The Category of Event Structures) Define ES to be the category of objects event structures and arrows event structures morphisms. The composition of arrows is defined componentwise.

The definition of morphism on event structures is given rather abruptly—see [29] for motivation. The categories T S, ST and ES are related by coreflections: the inclusion functor ST ↪ T S has a right adjoint unfolding transition systems to trees; the functor ST → ES identifying a synchronisation tree with an event structure has a right adjoint serialising an event structure to a synchronisation tree.

The categories of models described above can be fibred with respect to their labelling sets.

Definition 3 For M ∈ {ST , T S, ES} and L a set of labels, define M_{L} to be the subcategory of M of those objects labelled in L and morphisms which have the identity on L as relabelling part.

1.2 Bisimulation from open maps

We now describe the characterisation of bisimulation via open maps proposed in [19], to which we refer for a more detailed discussion. We need to fix on an idea of the computation paths in our model. For instance a (computation) path of a transition system with labelling set L is reasonably taken to be a finite sequence of transitions that the transition system can perform. It has the shape of a string of labels in L.

Definition 4 (Finite strings regarded as a category) Let L be a set. Define L^{+} to be the partial order of finite non-empty strings over L regarded as a category. It is convenient to identify strings in L^{+} with the equivalent subcategory of ST_{L} consisting of those special synchronisation trees consisting of a finite single branch of nonzero length.

Define L^{∗} to be the extension of L^{+} to all finite strings.

To take account of the added independence structure of event structures, the shape of their computation paths is taken to be a finite pomset [25].

Definition 5 (Labelled pomsets) Let L be a set. The category Pom_{L} is taken to be the subcategory of ES_{L}, for a labelling set L, consisting of those finite non-empty event structures in which all subsets of events are in the consistency relation. In other words the objects P of Pom_{L} are triples P = (P, ≤, l) where P is a finite non-empty set, ≤ is a partial order on P and l : P → L is a function. A morphism f : P → Q in Pom_{L} is given by a injective function that preserve the labelling and send downward closed sets of P to downward closed sets of Q.

Define (Pom_{L})_{⊥} to be the extension of Pom_{L} to include the empty pomset as well.

Both the operation of adjoining the empty string, taking L^{+} to L^{∗}, and the empty pomset to Pom_{L} are special cases of the “lifting” construction on categories which will meet in Definition 8)—this accounts for the notation in the definition above.

We can obtain a general definition of bisimulation from open maps. Roughly speaking open maps are morphisms with the property that any extension of a computation path in the range can be matched by an extension in its domain.

Definition 6 (ℙ-open maps) Assume a category of models M and a choice of path category, a subcategory ℙ ↪ M consisting of path objects together with morphisms expressing how they can be extended. Let f : M → M′ be an arrow in M. We say that f is a ℙ-open map if, whenever, for m : P → Q a morphism in ℙ, a “square”

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

in M commutes, i.e., q ∘ m = f ∘ p, meaning the path f ∘ p in M′ can be extended via m to a path q in M′, then there is a (not necessarily unique) morphism p′ such that in the diagram

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

the two “triangles” commute, i.e., p′ ∘ m = p and f ∘ p′ = q, meaning the path p can be extended via m to a path p′ in M which matches q.

Two objects M_{1}, M_{2} of M are said to be ℙ-bisimilar iff there is a span of

ℙ-open morphisms f_{1}, f_{2}: \xymatrix{ & M \ar[dl]_{f_{1}} \ar[dr]^{f_{2}} \\ M_{1} & & M_{2} .}

In the case of traditional models we obtain known equivalences. In ST_{L}, L^{∗}- bisimulation coincides with Park and Milner’s strong bisimulation; for event structures ES_{L}, (Pom_{L})_{⊥}-bisimulation coincides with hereditary history-preserving bisimulation due to Bednarczyk refining ideas of van Glabbeek and Goltz, Rabinovitch and Traktenbrot [1,12,26].

The following easy-to-prove preservation property will be used later.

Proposition 7 Suppose M has products. Let f_{1} : M_{1} → N_{1} and f_{2} : M_{2} → N_{2} be ℙ-open maps. Then f_{1} × f_{2} : M_{1} × M_{2} → N_{1} × N_{2} is ℙ-open.

1.3 Presheaves as non-deterministic processes

Presheaf categories are the central mathematical notion around which this paper is built. Let ℙ be a category. We shall call ℙ a path category because we are thinking of its objects as specifying computation path shapes and its morphisms as path extensions. The category of presheaves over ℙ, often denoted by ℙ̂ or by Set^{ℙ^{op}}, is the category whose objects are contravariant functors from ℙ to Set (the category of sets and functions) and whose arrows are the natural transformations between such functors. The category ℙ̂ is the “free cocompletion” of ℙ, in the sense that it can be obtained to within equivalence of categories, by freely adding all possible colimits of diagrams in ℙ. The category ℙ̂ is very rich in structure and is well known to be an example of a topos (for more details on toposes and functor categories, see [22]).

A category of presheaves, ℙ̂, is accompanied by a functor, the Yoneda embedding, y_{ℙ} : ℙ → ℙ̂, which fully and faithfully embeds ℙ in the category of presheaves. Given any object P of ℙ, the presheaf y_{ℙ}(P) is the contravariant hom-functor, ℙ[−, P], which to any Q, an object of ℙ, associates the set ℙ[Q, P] of arrows of ℙ from Q to P, and to any arrow f : Q → Q′ associates the function that by precomposition with f sends any arrow g : Q′ → P to g ∘ f : Q → P.

Via the Yoneda embedding we can regard ℙ as essentially a full subcategory of ℙ̂. We have a situation fitting that needed for defining open maps and bisimulation in ℙ̂, along the lines of Section 1.2. The Yoneda Lemma (see e.g. [21]) provides a natural bijection between ℙ̂[y_{ℙ}(P), F] and F (P). This justifies the intuition that a presheaf F : ℙ^{op} → Set can be thought of as specifying for a typical path object P the set, F (P), of computation paths of shape P. The presheaf F acts on a morphism m : P → Q in ℙ to give a function F (m) : F (Q) → F (P) saying how Q-paths restrict to P -paths.

It turns out that to rule out the unfortunate case of the arrows from the initial, always empty, presheaf to any other presheaf being open, it is more convenient to define open map bisimulation for presheaves with respect to a strict extension of the Yoneda embedding.

Definition 8 If ℙ is a category, define ℙ_{⊥} to be the category ℙ to which a new initial object, ⊥, has been added. Define y_{ℙ}^{∘} : ℙ_{⊥} ↪ ℙ̂ to be the strict, i.e., initial-object preserving, extension of the Yoneda embedding y_{ℙ}.

As we shall see, y_{ℙ}^{∘} : ℙ_{⊥} ↪ ℙ̂ is the universal arrow associated with another characterisation of the presheaf category ℙ̂, as the free connected-colimit preserving completion of ℙ_{⊥}.^{4}

Definition 9 (Open maps for presheaves) If ℙ is a small category and f : X → Y is an arrow between presheaves over ℙ, define f to be ℙ-open (or simply open when no confusion arises) if it is open according to Definition 6 with respect to the embedding y_{ℙ}^{∘}.

By considering open maps with respect to y_{ℙ}^{∘} rather than y_{ℙ} we obtain that open maps are necessarily epimorphic (as are L^{∗}- and (Pom_{L})_{⊥}-open maps in contrast to L^{+}- and Pom_{L}-open maps for transition systems and event structures, respectively).

Proposition 10 An arrow between presheaves over a category ℙ is open if and only if it is epimorphic (i.e., pointwise a surjective function) and open with respect to the Yoneda embedding, y_{ℙ}.

4 In earlier work [19,6], we have made use of rooted presheaves of a category ℙ_{⊥}. A rooted presheaf is a presheaf X over ℙ_{⊥} in which the set X(⊥) is a singleton. Note that the subcategory of rooted presheaves over ℙ_{⊥} is isomorphic to the category of presheaves ℙ̂, and that this is the connected-colimit completion of ℙ_{⊥}.

A model, like a transition system or a labelled event structure, gives rise to a presheaf. For a category of models M and a choice of path category forming a subcategory ℙ ↪ M, there is a canonical functor from the category of models M to the category of presheaves ℙ̂. The functor, c_{M} : M → ℙ̂, takes an object M of M to the presheaf M[−, M]—more intuitively, it takes the model M to the presheaf which for each path object P yields the set of paths M[P, M] from P into M. The canonical functor takes a morphism f : M → M′ in M to the natural transformation, M[−, f] : M[−, M] → M[−, M], whose component at an object P of ℙ is the function M[P, M] → M[P, M′] taking p to f ∘ p—a path p : P → M in M is taken to a path f ∘ p : P → M in M. More generally for F : ℙ → M any functor, one can define c_{F} : M → ℙ̂ to be c_{F} (M) =^{def} M[F (−), M] on objects and to act by composition on morphisms.

The canonical functors from synchronisation trees ST_{L} to presheaves L̂^{+} and from event structures ES_{L} to \begin{matrix} \\ Pom & L \end{matrix} are full and faithful, so canonical embeddings. Generally, a canonical functor c_{M} is full and faithful whenever the path category is dense in the category of models M (see MacLane [21], P. 243), as remarked in [19]. Because such canonical embeddings are also dense they preserve all existing limits [30]. On the other hand, we cannot expect c_{M} to preserve general colimits in M. The following proposition asserts that colimits of certain diagrams are preserved (we shall need it in Section 6).

Proposition 11 Let M be a category, ℙ be a category with a functor F : ℙ → M. Let Δ : 𝔻 → M be another functor from a small category 𝔻 satisfying the following property of “density with respect to F ”: If (M, δ_{D} : Δ(D) → M) is a colimiting cone for Δ, then for any P ∈|ℙ| and p : F (P) → M, there exists a D ∈|𝔻| and d : F (p) → Δ(d) such that:

• p = δ_{D}d.

• For any other factorisation

\xymatrix{F (P) \ar[rr]^{p} \ar[dr]_{d′} &  & M \\  & Δ(D′) , \ar[ur]_{δ_{D′}}}

there exists m : D → D′ such that

Δ(m)d = d′  and  δ_{D′}Δ(m) = δ_{D} .

Then c_{F} (M) ≅ colim c_{F} Δ.

Remark: Proposition 11 above can be made into an “if and only if” statement if we replace the condition on m by one saying that any two factorisations are connected by a chain of spans

D = D_{0} ⟵^{m_{1}} D_{1} ⟶^{m_{2}} D_{2} ← ⋯ ⟶^{m_{n}} D_{n} = D′

in 𝔻 with p_{i} : F (P_{i}) → Δ(D_{i}) such that:

δ_{D_{i−1}}m_{i} = δ_{D_{i}} (for i odd) δ_{D_{i}}m_{i} = δ_{D_{i−1}} (for i even)
m_{i}p_{i} = p_{i−1} (for i odd) m_{i}P_{i−1} = p_{i} (for i even) .

Open map bisimulation is clearly preserved whenever the canonical functors are full and faithful and is reflected too in the case of synchronisation trees and event structures.

Proposition 12 (Joyal-Nielsen-Winskel)

(i) Two synchronisation trees, over labelling set L, are L^{∗}-bisimilar (i.e.strong bisimilar) iff their corresponding presheaves, under the canonical embedding, are related by a span of L^{+}-open maps.

(ii) Two event structures, over labelling set L, are (Pom_{L})_{⊥}-bisimilar (equivalently, hereditary history-preserving bisimilar) iff their corresponding presheaves, under the canonical embedding, are related by a span of Pom_{L}- open maps.

Having established the link between categories of models and categories of presheaves over appropriate path categories, we can look for general constructions on presheaves, useful in modelling processes, that preserve openness and hence bisimulation. Left Kan extensions will be among such constructions. Before we introduce this powerful operation we mention a simple property, straightforward to verify, of the canonical embeddings c_{ST_{L}} of synchronisation trees and c_{ES_{L}} of event structures, that we shall need in Section 5.

Proposition 13 The canonical embeddings, c_{ST_{L}} and c_{ES_{L}} preserve coproducts and initial objects.

1.4 Left Kan extensions

We introduce the notion of Left Kan extension, a construction which we use extensively.

Definition 14 (Left Kan Extensions) If C ⟵^{G} A ⟶^{F} B are 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 call the functor H 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 15 If F is full and faithful and (Lan_{F} (G), α) exists then α is a natural isomorphism.

If C is cocomplete and A is essentially small, then Lan_{F} (G) always exists for any F and G and can be computed “pointwise” (see [2]) as a colimit. 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)) .

Let ℙ be a category. We mentioned earlier that ℙ̂ is the free colimit completion of ℙ. In more detail:

Proposition 16 The Yoneda embedding y_{ℙ} : ℙ → ℙ̂ satisfies the universal property that for any functor F : ℙ → E, where E is a cocomplete category, there is a colimit-preserving functor G : ℙ̂ → E, unique to within isomorphism, such that F ≅ G ∘ y_{ℙ}:

\xymatrix{ℙ \ar[r]^{y_{ℙ}} \ar[dr]_{F} & ℙ̂ \ar[d]^{G} \\  & E}

To within isomorphism, the functor G is given as the left Kan extension Lan_{y_{ℙ}}(F). Conversely, if G : ℙ̂ → ℚ̂ is a colimit-preserving functor then, to within isomorphism, G is Lan_{y_{ℙ}}(G ∘ y_{ℙ}).

In fact, Lan_{y_{ℙ}}(F) has right adjoint a functor taking Y in E to the presheaf E[F (-), Y]; the right adjoint is also a left Kan extension, being Lan_{F} (y_{ℙ}) to within isomorphism.

A key result that we use in this paper is the following theorem which entails that the left Kan extensions described above preserve open maps, a powerful tool in showing operations preserve bisimulation:

Theorem 17 Let F : ℙ̂ → ℚ̂ be a colimit preserving functor and let f be a ℙ-open map, then F (f) is a ℚ-open map.

A proof of the above theorem appears in [3]. We shall not be interested only in colimit-preserving functors and in [3] a similar preservation property for a larger class of functors is also proved.

Theorem 18 Let F : ℙ̂ → ℚ̂ be a connected-colimit preserving functor, i.e., a functor which preserves colimits of connected diagrams, and let f be a ℙ-open map, then F (f) is a ℚ-open map.

The operations that we use for modelling process constructors on presheaves all fall within the class of connected-colimit preserving functors. This will enable us to establish that open-map bisimulation in presheaf models is a congruence for a general process language, once and for all.

We present the connection between the strict extension of the Yoneda embedding y_{ℙ}^{∘} and connected-colimit preserving functors.

Proposition 19 (See [3]) Let ℙ be a small category. With respect to the embedding y_{ℙ}^{∘} : ℙ_{⊥} → ℙ̂, the category ℙ̂ is the free connected-colimit completion of ℙ_{⊥}. Moreover if F : ℙ_{⊥} → E is a functor, with E a category with connectedcolimits, then the universal extension of F is Lan_{y_{ℙ}^{∘}}(F) : ℙ̂ → E.

Recall the Kan extensions arising in an important special case. A functor F : ℙ → ℚ gives rise to a triple of adjoint functors F_{!} ⊣ F^{∗} ⊣ F_{∗} (see [22]) that can be described as

F_{!} = Lan_{y_{ℙ}}(y_{ℚ}F), F^{∗} = Lan_{y_{ℚ}F} (y_{ℙ}), F_{∗} = Lan_{F^{∗}y_{ℚ}}(y_{ℚ}) .

Instantiating this to F = I : ℙ ↪ ℙ_{⊥}, the obvious embedding of ℙ in ℙ_{⊥}, we deduce the following.

Proposition 20 If I : ℙ ↪ ℙ_{⊥} is the obvious embedding of ℙ into ℙ_{⊥}, then I_{∗} preserves connected-colimits.

Proof: As we wrote I_{∗} = Lan_{I^{∗}y_{ℙ_{⊥}}}(y_{ℙ}). A straightforward calculation shows that I^{∗}y_{ℙ_{⊥}} = y_{ℙ}^{∘}, hence by Proposition 19, I_{∗} is connected-colimit preserving. □

Notice that I_{∗} can be defined more concretely as acting on a presheaf X in the following way:

I_{∗}(X)(P) = \{ \begin{matrix}X(P) & if P ≠ ⊥ \\ \{∗\} & otherwise. \end{matrix}

Later, we shall make great use of the following definition.

Definition 21 Let F : ℙ_{⊥} → ℚ_{⊥} be a functor that preserves the initial ob-

ject. Consider the composite functor \xymatrix{ℙ \ar[r]^{I_{ℙ}} & ℙ_{⊥} \ar[r]^{F} & ℚ_{⊥} \ar[r]^{y_{ℚ}^{∘}} & ℚ̂}. Define F^{l} =^{def}

Lan_{y_{ℙ}}(y_{ℚ}^{∘}F I_{ℙ}) : ℙ̂ → ℚ̂ and F^{r} =^{def} Lan_{y_{ℚ}^{∘}F I_{ℙ}}(y_{ℙ}).

Proposition 22 With respect to Definition 21 above we have that:

(1) F^{l} ⊣ F^{r}.

(2) F^{r} is connected-colimit preserving.

(3) F^{l} is colimit-preserving and F^{l} ≅ I_{ℚ}^{∗}(F I_{ℙ})_{!} ≅ I_{ℚ}^{∗}F_{!}I_{ℙ,!}, where I_{ℚ} : ℚ ↪ ℚ_{⊥}.

Proof:

(1) By Proposition 16 (with F instantiated to y_{ℚ}^{∘}F I_{ℙ}).

(2) Since left Kan extensions compose, we have that F^{r} =^{def} Lan_{y_{ℚ}^{∘}F I_{ℙ}}(y_{ℙ}) ≅ Lan_{y_{ℚ}^{∘}}(Lan_{F I_{ℙ}}(y_{ℙ})) and hence, by Proposition 19, we can deduce that F^{r} preserves connected colimits.

(3) As remarked earlier, left Kan extensions with respect to the Yoneda embedding correspond to colimit preserving functors, to within isomorphism. Recall from the proof of Proposition 20, that y_{ℚ}^{∘} = I_{ℚ}^{∗}y_{ℚ_{⊥}}. Notice moreover that colimit-preserving functors, such as I_{ℚ}^{∗}, preserve left Kan extensions (see [2]). Thus we can establish the following chain of isomorphisms:

F^{l} =^{def} Lan_{y_{ℙ}}(y_{ℚ}^{∘}F I_{ℙ}) ≅ Lan_{y_{ℙ}}(I_{ℚ}^{∗}y_{ℚ_{⊥}}F I_{ℙ}) ≅ I_{ℚ}^{∗}Lan_{y_{ℙ}}(y_{ℚ_{⊥}}F I_{ℙ})

=^{def} I_{ℚ}^{∗}(F I_{ℙ})_{!} ≅ I_{ℚ}^{∗}F_{!}I_{ℙ,!} .

□

1.5 Fibred categories

Indexing structure plays a fundamental role in the categorical analysis of models for concurrency [29,27]. In the context of categorical models for CCS-like languages we will consider presheaf categories indexed by a category of labelling sets. There is a tight correspondence between indexed categories and fibrations; the former represent the class of fibrations for which a definite (coherent) choice of a cleavage has been made. We introduce in this section the basic terminology of fibred category theory^{5} together with pointers to the related notion of elementary existential doctrine [20] of which the presheaf models of Section 3 will be an example.

5 A more detailed introduction to fibrations can be found in, e.g., [17].

Definition 23 (Cartesian arrows) Let π : E → B be a functor. An arrow in E, f : e′ → e is cartesian (with respect to π) if for every other arrow g : e′′ → e such that π(g) = βα with β = π(f), there exists a unique h : e′′ → e′ with g = fh and π(h) = α:

\xymatrix{e′′ \ar@{.>}[dr]_{∃!h} \ar[drr]^{g} \\  & e′ \ar[r]_{f} & e \\ π(e′′) \ar[r]|{α} & π(e′) \ar[r]^{β} & π(e) & .}

Definition 24 (Fibrations) A functor π : E → B is a fibration if for every β : b′ → b in B and e ∈|E | such that π(e) = b, there exists a cartesian arrow, f, of codomain e such that π(f) = β. The arrow f is called a cartesian lifting of e with respect to β.

Definition 25 If π : E → B is a functor, an arrow f : e′ → e of E is said to be vertical if π(f) = 1_{e}.

Definition 26 If π : E → B is a functor and b an object of B. Define the fibre over b (with respect to π) to be the subcategory E_{b} of E of those objects e and arrows f such that π(e) = b and π(f) = 1_{b}.

If π is a fibration then a choice of cartesian arrows induces cartesian lifting functors between the fibres:

Proposition 27 (Cartesian lifting functors) Let π : E → B a fibration. Let β : b′ → b be an arrow in B. For every object e ∈| E_{b} | let β_{e}^{∗} : β^{∗}(e) → e be a chosen cartesian lifting of e with respect to β. This choice induces the following cartesian lifting functors β^{∗} : E_{b} → E_{b′}:

• On objects e ↦ β^{∗}(e) as chosen above

• On arrows (f : \overline{e} → e) ↦ β^{∗}(f) that is defined to be the unique arrow such that the following square commutes:

\xymatrix{β^{∗}(\overline{e}) \ar[r]^{β∗ ; \overline{e}} \ar[d]_{β^{∗}(f)} & \overline{e} \ar[d]^{f} \\ β^{∗}(e) \ar[r]_{β_{e}^{∗}} & e.}

A choice of cartesian arrows for a fibration is called a cleavage and a fibration with a chosen cleavage is called a cloven fibration. If the choice of the cleavage is functorial, i.e., (1_{b})_{e}^{∗} = 1_{e} and for b′′ ⟶^{α} b′ ⟶^{β} b, (βα)_{e}^{∗} = α_{β_{e}^{∗}}^{∗}, then the fibration is said to be split.

We will make extensive use of the dual notion of cofibration:

Definition 28 (Cofibrations and Bifibrations) A functor π : E → B is a cofibration if the dual functor π^{op} : E^{op} → B^{op} is a fibration. A functor that is both a fibration and a cofibration is called a bifibration.

Dually, one talks of cocartesian arrows, cocartesian liftings, cocartesian lifting functors and (functorial) cocleavages.

1.6 The Grothendieck construction

Cloven fibrations are equivalent to indexed categories.^{6} In fact any indexed category gives rise (via a construction due to Grothendieck [13]) to a cloven fibration and vice versa any cloven fibration induces an indexed category.

Definition 29 (Indexed categories) Let B be any category. A B-indexed category in CAT is given by a pseudo-functor F : B^{op} → CAT , that is F associates to each object of b, a category F (b), to any arrow β : b′ → b a functor β^{∗} : F (b) → F (b′) with natural isomorphisms, ϕ_{b} : 1_{F (b)} ⟶^{≃} (1_{b})^{∗} and

ϕ_{(α,β)} : α^{∗}β^{∗} ⟶^{≃} (βα)^{∗} for any b ∈|B | and for any two arrows b′′ ⟶^{α} b′ ⟶^{β} b

of B satisfying the coherence conditions given by commutativity of the following diagrams:

\xymatrix{α^{∗}(1_{b})^{∗} \ar[dr]_{ϕ_{α,1_{b}}} & α^{∗} \ar[l]_{α^{∗}ϕ_{b}} \ar[r]^{(ϕ_{b})_{α^{∗}}} \ar[d]^{1_{α^{∗}}} & (1_{b′})^{∗}α^{∗} \ar[dl]^{ϕ_{1_{b′} ,α}} \\  & α^{∗}}

\xymatrix{α^{∗}β^{∗}γ^{∗} \ar[r]^{(ϕ_{α,β})_{γ^{∗}}} \ar[d]_{α^{∗}ϕ_{β,γ}} & (βα)^{∗}γ^{∗} \ar[d]^{ϕ_{βα,γ}} \\ α^{∗}(γβ)^{∗} \ar[r]_{ϕ_{α,γβ}} & (γβα)^{∗} ,}

with γ being another arrow of B, γ : b → b′′′.

Definition 30 (Grothendieck construction) Given a B-indexed category F : B^{op} → CAT , define the following category Groth(F):

• Objects: Pairs ⟨c, b⟩, with c ∈|F (b)| and b ∈|B |.

• Arrows: A pair ⟨f, β⟩ is an arrow from ⟨c′, b′⟩ to ⟨c, b⟩ if β : b′ → b is an arrow in B and f : c′ → F (β)(c) is an arrow in F (b′). If ⟨f, α⟩ : ⟨c′′, b′′⟩ → ⟨c′, b′⟩ and ⟨g, β⟩ : ⟨c′, b′⟩ → ⟨c, b⟩ then their composite is the pair ⟨h, βα⟩

6 See for example [14] for a precise account of this statement.

where h is the following arrow

c ⟶^{f} F (α)c′ ⟶^{F (α)g} F (α)F (β)c′′ ⟶^{ϕ_{α,β}} F (βα)c′′ .

The coherence conditions of Definition 29 ensure associativity of composition.

The obvious projection π : Groth(F) → B that projects any pair onto its the second component is a fibration. A cartesian lifting for ⟨c, b⟩ with respect to β : b′ → b is given by the pair ⟨1_{F (β)c}, β⟩.

Our main example of a bifibration will be given by an elementary existential doctrine in the sense of Lawvere [20] whose categories of attributes will be presheaf categories. We will consider the following two conditions on fibrations, which usually arise in the context of categorical logic [22,20].

Definition 31 Let P : B^{op} → CAT be a pseudo-functor. If β : b′ → b is an arrow in B, we write β^{∗} for P(β). Suppose that for any β, β^{∗} has a left adjoint β_{!}.

• Beck-Chevalley Condition: Say that P satisfies the Beck-Chevalley condition if for every pullback square in B

[figure: b′′′; \overline{α}; \overline{β}; b′; α; b′′; β; b]

with α monic, the following square commutes up to a natural isomorphism:

\xymatrix{P(b′′′) \ar[d]_{_{\overline{α}_{!}}} & P(b′) \ar[l]_{^{\overline{β}^{∗}}} \ar[d]^{α_{!}} \\ P(b′′) & P(b) . \ar[l]^{β^{∗}}}

• Fröbenius Reciprocity Law: Suppose now that for every b ∈| B |, P(b) has binary products. Say that P satisfies the Fröbenius Reciprocity Law if for every β : b′ → b and c ∈| P(b) | the following square commutes up to a natural isomorphism:

\xymatrix{b′ \ar[d]_{β} & P(b′) \ar[d]_{β_{!}} & P(b′) \ar[l]_{β^{∗}(c)×−} \ar[d]^{β_{!}} \\ b & P(b) & P(b) . \ar[l]_{c×−}}

We round off this section with a few facts about fibrations and indexed categories that we need later.

Proposition 32 Let P : B^{op} → CAT be a pseudo-functor satisfying the Beck-Chevalley condition, then for any monic arrow β : b′ ↣ b,

β^{∗}β_{!} ≅ 1_{P(b′)} .

If P satisfies also the Fröbenius reciprocity law, then for any monic arrow β : b′ ↣ b, the functor β_{!} preserves products.

Proof: For the easy proof of the first statement see [22] P.175. The second, categorical folklore it seems, can be proved easily, as follows. Let c′, d′ be two objects of P(b′), then

β_{!}(c′ × d′) ≅ β_{!}(β^{∗}β_{!}c′ × d′)  (from the property above)
≅ β_{!}c′ × β_{!}d′  (by Fröbenius reciprocity law)

□

We use the last result to prove a fact about products (Proposition 34) that will be useful later in Section 4 to prove that parallel compositions respect bisimulation. We first need a lemma.

Lemma 33 Let P : B^{op} → CAT be a pseudo-functor, satisfying both the Beck-Chevalley condition and the Fröbenius Reciprocity law. Let the following square be a pullback of monomorphisms in B:

[figure: a; β; α; b; γ; c; δ; d .]

If X and Y are two objects of P(d) such that δ_{!}δ^{∗}X ≅ X and γ_{!}γ^{∗}Y ≅ Y, then

X × Y ≅ δ_{!}α_{!}α^{∗}δ^{∗}(X × Y) .

Proof:

X × Y ≅ δ_{!}δ^{∗}X × Y  (by hypothesis)
≅ δ_{!}(δ^{∗}X × δ^{∗}Y)  (by Fröbenius)
≅ δ_{!}δ^{∗}X × δ_{!}δ^{∗}Y  (by Proposition 32)
≅ X × δ_{!}δ^{∗}Y  (by hypothesis)
≅ X × δ_{!}δ^{∗}γ_{!}γ^{∗}Y  (by hypothesis)
≅ X × δ_{!}α_{!}β^{∗}γ^{∗}Y  (by Beck-Chevalley)
≅ X × δ_{!}α_{!}α^{∗}δ^{∗}Y  (since δα ≅ γβ)
≅ δ_{!}α_{!}(α^{∗}δ^{∗}X × α^{∗}δ^{∗}Y)  (by Fröbenius)
≅ δ_{!}α_{!}α^{∗}δ^{∗}(X × Y)  (since α^{∗} and δ^{∗} are right adjoints).
□

Proposition 34 Let P : B^{op} → CAT be a pseudo-functor, satisfying both the Beck-Chevalley condition and the Fröbenius Reciprocity law. If a diagram

[figure: a; c; π_{b}; π_{a}; b; d; i; f; l; r; k; e; j]

is a limiting cone in B, then for any object X ∈|P(d)| and Y ∈|P(e)|, there is an isomorphism in P(c),

k_{!}(l^{∗}X × r^{∗}Y) ≅ π_{a}^{∗}i_{!}X × π_{b}^{∗}j_{!}Y .

Proof: Observe first of all that the limit of the diagram

[figure: a; c; π_{b}; π_{a}; b; d; i; e; j]

is obtained by taking three pullbacks, i.e., the limiting cone can be constructed as follows,

[figure: a; c; π_{b}; π_{a}; b; d; i; ·; δ; π_{d}; ·; γ; π_{e}; e; j; f; α; β]

where all the quadrilaterals in the diagram above are pullbacks. Without loss of generality we can assume that l = π_{d}α, r = π_{l}β and k = δα = βγ. We deduce the following natural isomorphism:

δ_{!}δ^{∗}π_{a}^{∗}i_{!} ≅ δ_{!}δ^{∗}δ_{!}π_{d}^{∗} (by Beck-Chevalley)
≅ δ_{!}π_{d}^{∗}  (by Proposition 32)
≅ π_{a}^{∗}i_{!}  (by Beck-Chevalley).

Similarly one deduces that γ_{!}γ^{∗}π_{b}^{∗}j_{!} ≅ π_{b}^{∗}j_{!}. Hence,

π_{a}^{∗}i_{!}X × π_{b}^{∗}j_{!}Y ≅ δ_{!}α_{!}α^{∗}δ^{∗}(π_{a}^{∗}i_{!}X × π_{b}^{∗}j_{!}Y)  (by Lemma 33)
≅ k_{!}(α^{∗}δ^{∗}π_{a}^{∗}i_{!}X × α^{∗}δ^{∗}π_{b}^{∗}j_{!}Y)
≅ k_{!}(α^{∗}δ^{∗}δ_{!}π_{d}^{∗}X × α^{∗}α_{!}β^{∗}π_{e}^{∗}Y) (by Beck-Chevalley)
≅ k_{!}(α^{∗}π_{d}^{∗}X × β^{∗}π_{e}^{∗}Y)  (by Proposition 32)
≅ k_{!}(l^{∗}X × r^{∗}Y) .
□

Proposition 35 Let π : E → B be a fibration (cofibration). Let Δ be a class of diagram shapes (i.e., a class of categories). Suppose that for every object b of B, the fibre E_{b} has limits (colimits) of diagrams of shape δ for every δ ∈ Δ and suppose that B has limits (colimits) of diagrams of shape δ for every δ ∈ Δ too. Then E has limits (colimits) of diagrams of shape δ for every δ ∈ Δ.

Proof: We simply give the description of how to build a limiting cone in E for a diagram of shape δ ∈ Δ. Let F : δ → E be a functor. Consider πF : δ → B. By assumption there exists a limiting cone for πF. Let b = lim πF and for any d ∈| δ |, let β_{d} : πF (d) → b be the corresponding edge of the cone. Let (β_{d}^{∗} : β_{d}^{∗}(F (d)) → F (d))_{d∈|δ|} be a family of cartesian arrows. This family induces a functor, β_{(−)}^{∗}F : δ → E_{b}. By assumption there exists a limiting cone to such a functor. Let (e, f_{d} : e → β_{d}^{∗}F (d)) be such a cone, then by postcomposing with the corresponding cartesian arrows one obtains a limiting cone (e, β_{d}^{∗}f_{d} : e → F (d)) in E. □

Morphisms of transition systems, synchronisation trees consist of pairs, one component of which is a partial function between labelling sets. By projecting to this component we obtain functors p_{T S} : T S → Set_{∗}, p_{ST} : ST → Set_{∗} and p_{ES} : ES → Set_{∗} from the categories of models to Set_{∗}, the category of sets and partial functions.

Proposition 36 (Implicit in [29]) The functors p_{T S} : T S → Set_{∗} and p_{ST} : ST → Set_{∗} are bifibrations. The functor p_{ES} : ES → Set_{∗} is a cofibration. There exist cartesian liftings of all monomorphisms.

Notation: If L and M are two sets, we write L ×_{∗} M for the categorical product of L and M as objects of Set_{∗}. Concretely L ×_{∗} M can be realised as the disjoint union of sets L + M + L × M, while L × M as the usual cartesian product of sets.

2 A general process language and its categorical models

We introduce the process language Proc of [29] within which a class of CCSlike languages can be expressed. The distinctive feature of Proc is that its parallel composition operator is a general product out of which different parallel compositions can be constructed with the help of restriction and relabelling operations. As noted in [29], if the terms of Proc are to be interpreted in categories of labelled structures (such as labelled transition systems, event structures) it is convenient to regard such categories as fibred over the labelling sets, more precisely over the category Set_{∗} of sets and partial maps. Viewed in this way we obtain the universal characterisations of the operators associated with restriction and relabelling in terms of (co)cartesian liftings. Prefixing requires a more ad hoc treatment.

Define the terms of the language Proc:

t ::= Nil | at | t_{0} ⊕ t_{1} | t_{0} × t_{1} | t↾Λ | t{Ξ} | x | rec x.t

where a is a label, Λ is a subset of labels, while Ξ is a total function from labels to labels, and x is drawn from some infinite set of a variables that we denote by V ars.

The handbook chapter [29] presented an analysis of the categorical status of the operations involved in the semantics of Proc. The structure, left somewhat implicit there, leads to an axiomatisation of the categories which are models of Proc. We emphasise the role of partial relabelling functions as substitution operators and impose upon them the Fröbenius reciprocity law and the Beck-Chevalley condition of Section 1.5

Definition 37 (Models for Proc) A categorical model for Proc is given by a functor π : M → Set_{∗} such that:

• M has binary products (×).

• For every set L, the fibre M_{L} has initial object (0_{L}), binary coproducts (+_{L}) and colimits of ω-chains.

• For every inclusion i : L ↪ M of sets, there exists a cartesian lifting functor i^{∗} : M_{M} → M_{L}.

• For every total function f : L → M, there exists a cocartesian lifting functor f_{!} : M_{L} → M_{M}.

• For every set L and label a ∈ L, there exists a prefixing endofunctor

P re_{a,L} : M_{L} → M_{L}

which preserves ω-colimits as well as existing cocartesian lifting functors for partial maps f : L ⇀ M, that are defined on a, i.e., if f is a partial map from L to M such that f(a) is defined and such that f_{!} exists, then the following square commutes, up to coherent isomorphism:

\xymatrix{M_{L} \ar[r]^{P re_{a,L}} \ar[d]_{f_{!}} & M_{L} \ar[d]^{f_{!}} \\ M_{M} \ar[r]_{P re_{f(a),M}} & M_{M}.}

• Whenever applicable, i.e., whenever the required (co)cartesian arrows exist, the Fröbenius reciprocity law and Beck-Chevalley condition of Definition 31 hold.

In [29] several models were considered, ranging from ‘interleaving’ models, like transition systems and synchronisation trees, to ‘non-interleaving’ models, like event structures, Petri nets or transition systems with independence. Here we recall briefly, how the structure required in the definition above is used to give semantics to terms of Proc .

We first derive some properties of models. In fact a model for Proc, as described in Definition 37, is not necessarily a cofibration. Still it has enough cocartesian liftings for us to deduce the following corollary (of the proof) of Proposition 35:

Corollary 38 If π : M → Set_{∗} is a model for Proc, then M has an initial object, binary coproducts and colimits of ω-chains.

2.1 Denotational semantics of Proc

The operation ⊕ will be used to model the nondeterministic sum. This operation contrasts with the categorical sum in that the labelling set of the nondeterministic sum is obtained as a union rather than a disjoint union of the labelling sets of the two components.

Definition 39 Let π : M → Set_{∗} be a model for Proc . If M is an object of M_{L} and N an object of M_{L′}, define M ⊕ N ∈|M_{L∪L′} | to be

M ⊕ N = i_{L,!}(M) +_{L∪L′} i_{L′,!}(N) .

For any two sets L, L′, this construction induces a functor (− ⊕ −) : M_{L} × M_{L′} → M_{L∪L′}. However, because of the choice of taking the union and not the disjoint set of labelling sets, this does not lift to a functor M × M → M; it does not have a well defined action on arrows. In fact it is not possible to define what f ⊕ g must be for two arbitrary arrows f : M → M′ and g : N → N′ of M. A definition is possible, however, when π(f) and π(g) agree on π(M) ∩ π(N). This occurs for arrows in a common fibre when π(f) and π(g) will be the same identity function. More generally one can define a bifunctor ⊕ : M_{in} ×M_{in} → M_{in} where M_{in} is the subcategory of M of those arrows, f, such that π(f) is an inclusion of sets.

Let π : M → Set_{∗} be a model as in Definition 37. We describe the denotational semantics of Proc inductively on the structure of the well typed terms, assuming an environment ρ : V ars →|M|, a function to the objects of M:

Nil: [[Nil]]_{ρ} = 0_{∅} an initial object of M

Variables: [[x]]_{ρ} = ρ(x)

Sum: [[t_{1} ⊕ t_{2}]]_{ρ} = [[t_{1}]]_{ρ} ⊕ [[t_{2}]]_{ρ}

Product: [[t_{1} × t_{2}]]_{ρ} = [[t_{1}]]_{ρ} × [[t_{2}]]_{ρ}

Restriction: [[t_{1}↾Λ]]_{ρ} = i^{∗}([[t_{1}]]_{ρ}), where i : Λ ∩ π([[t_{1}]]_{ρ}) ↪ π([[t_{1}]]_{ρ})

Relabelling:For Ξ : L → M a relabelling function, [[t_{1}[Ξ]]]_{ρ} = Ξ′_{!}([[t_{1}]]_{ρ}), where

Ξ′ : π([[t_{1}]]_{ρ}) → π([[t_{1}]]_{ρ}) ∪ M is defined as Ξ′(a) = \{ \begin{matrix}a & if a ∉ L \\ Ξ(a) & if a ∈ L . \end{matrix}

Prefixing: [[at]]_{ρ} = P re_{a,L∪{a}}(i_{!}([[t]]_{ρ})), where π([[t]]_{ρ}) = L and i : L ↪ L ∪ {a}.

Recursion: Let t be any term, and let x be a variable (possibly free in t). Given any environment ρ the term t and the variable x determine an endofunctor

t_{ρ}^{x} : \begin{matrix}M_{in} & → & M_{in} \\ M & ↦ & [[t]]_{ρ[M/x]} . \end{matrix}

From t_{ρ}^{x}, the following ω-chain is derivable:

T : \begin{matrix}ω & → & M \\ 0 & ↦ & [[t]]_{ρ[[[Nil]]_{ρ}/x]} \\ n & ↦ & [[t]]_{ρ[T^{n−1}/x]} for n > 0 \end{matrix}

Define [[recx.t]]ρ = colim T. Since all the constructions involved in the denotation of a term t are ω-colimits preserving functors, then colim T is a fixed point for t_{ρ}^{x}.

The interpretation of the terms of Proc as objects of M has not involved Fröbenius reciprocity or the Beck-Chevalley condition. As we shall see in the next section these two conditions come into play when equipping models with a notion of bisimulation. Then the presence of these conditions will matter: they constrain the action that the cartesian arrows have on objects of M and are needed in showing that bisimulation is a congruence.

3 Presheaf models for Proc

As we saw in the previous section, the denotation of a term of Proc is given mainly in terms of universal constructions: (co)products, (co)cartesian liftings and fixed points. (The ad hoc treatment of prefixing is the exception.) Since we have an abstract definition of bisimulation via open maps we can hope to obtain abstract proofs of congruence with respect to bisimulation. But this task seems impossible with respect to the general definition of model for Proc. However, by specialising to presheaf models we can exploit the richness of constructions there to obtain a very general congruence theorem. The canonical embeddings from traditional models to presheaf categories preserve and reflect bisimulation as well as the process algebra operations. Consequently, the congruence results for presheaf models can be transferred to traditional models, as we do in Section 5 for the event structure model of Proc.

We begin by describing what we need to build a presheaf model for Proc. We require a family of path categories, indexed by sets of labels. Partial relabelling functions L ⇀ M will be associated with functors mapping computation paths over L to (possibly empty) computation paths over M. We will again need functors to represent prefixing, but this time they will be derived from more basic functors associated with lifting.

Definition 40 (Path structure for Proc) A path structure for Proc consists of a functor ℙ_{(−)} from Set_{∗} to Cat, the category of small categories, which sends λ : L ⇀ M to \overline{λ} : (ℙ_{L})_{⊥} → (ℙ_{M})_{⊥} such that:

(1) The functors \overline{λ}, for λ : L ⇀ M, preserve initial objects.

(2) For each set L and element a ∈ L, there is an explicitly given prefixing functor pre_{a,L} : (ℙ_{L})_{⊥} → ℙ_{L} satisfying commutativity of the following diagram, where I_{M}, I_{L} are the obvious embeddings:

\xymatrix{(ℙ_{L})_{⊥} \ar[r]^{pre_{a,L}} \ar[d]_{\overline{λ}} & ℙ_{L} \ar@{^{(}->}[r]^{I_{L}} & (ℙ_{L})_{⊥} \ar[d]^{\overline{λ}} \\ _{(ℙ_{M})_{⊥}} \ar[r]_{pre_{λ(a),M}} & ℙ_{M} \ar@{^{(}->}[r]_{I_{M}} & _{(ℙ_{M})_{⊥}}}

for any λ : L ⇀ M that is defined on a.

A process with labelling set L is to denote a presheaf over ℙ_{L}.

With the Grothendieck construction of Section 1.6 in mind, one sees that a path structure for Proc defines a split cofibration in Set_{∗}.

Example 41

(1) Define (−)^{+} : Set_{∗} → Cat to be the functor that associates to each set L the partial ordered set (regarded as a category) L^{+} of finite nonempty strings of elements of L, and to each partial map λ : L ⇀ M the monotone map (i.e., the functor) \overline{λ} : L^{∗} → M^{∗} that pointwise relabels every string over L to a string over M according to λ, sending every letter on which λ is undefined to the empty string (ε). The prefixing functors are defined by usual prefixing of strings, i.e., pre_{a,L}(σ) = aσ.

(2) Define Pom_{(−)} : Set_{∗} → Cat to be the functor that associates to each set L the category of non-empty pomsets labelled in L. If λ : L ⇀ M, then \overline{λ} : (Pom_{L})_{⊥} → (Pom_{M})_{⊥} is the following functor:

• On objects: Given a (possibly empty) pomset P = (P, ≤, l), \overline{λ}(P) = (P′, ≤′, l′) with P′ = {e ∈ P | λ(l(e)) is defined}, ≤′=≤ ∩(P′ ×P′) and l′(e) = λ(l(e)).

• On arrows: If f : P → Q is an arrow in (Pom_{L})_{⊥}, \overline{λ}(f) is simply the restriction of f to P′ and Q′. The prefixing functors are again the obvious ones, i.e., the prefixing pre_{a,L}(P) of a pomset P is obtained by adding a new event, labelled ‘a’, which is placed below all the events of P in the causal order relation.

Recall from the Definition 21 that from every functor F : ℙ_{⊥} → ℚ_{⊥}, that preserves the initial object, between small categories one can derive a pair of adjoint functors F^{l} ⊣ F^{r} : ℙ̂ → ℚ̂, with F^{r} being connected-colimit preserving. Hence, using the Grothendieck construction, from a path structure for Proc we can derive a bifibration, whose fibres will the be the categories ℙ̂_{L}.

3.1 The Grothendieck construction for presheaf models

Given a path structure ℙ_{(−)}, we can glue together all the fibres, consisting of categories of presheaves over ℙ_{L}, to form a fibration over Set_{∗} which we call Groth(ℙ_{(−)}):

Objects: pairs ⟨X, L⟩ with L ∈ |Set_{∗}| and X a presheaf over ℙ_{L},

Arrows: pairs ⟨f, λ⟩ : ⟨X, L⟩ → ⟨Y, M⟩ with λ : L ⇀ M and f : X → \overline{λ}^{r}(Y).

The composition of arrows is ⟨g, μ⟩ ∘ ⟨f, λ⟩ = ⟨\overline{λ}^{r}(g) ∘ f, μ ∘ λ⟩. Clearly the projection ⟨X, L⟩ ↦ L is the object part of a functor π : Groth(ℙ_{(−)}) → Set_{∗}. Intuitively, the Grothendieck construction glues the various fibres together; it adds arrows between presheaves (possibly over different fibres), to allow for the possibility of a partial relabelling of actions. The adjunctions ensure that the Grothendieck fibration is in fact a bifibration [17]; the cocartesian lifting of λ with respect to X is (η_{X}, λ) : X → \overline{λ}^{l}(X) where η_{X} : X → \overline{λ}^{r}\overline{λ}^{l}(X) is the component of the unit of the adjunction at X. Since the fibres are presheaf categories they satisfy all the colimit completeness requirements in Definition 37. Moreover by applying Proposition 35 we can deduce that Groth(ℙ_{(−)}) has binary products.

Even if the functor ℙ_{(−)} induces a split cofibration, whose fibres are the categories (ℙ_{L})_{⊥}, for a set L, when extended to Groth(ℙ_{(−)}) this property is lost. On the other hand, since the \overline{λ}^{r}’s are defined by composition, Groth(ℙ_{(−)}) is a split fibration.

Definition 42 (Presheaf Models for Proc) A presheaf model for Proc, consists of a path structure ℙ_{(−)} as in Definition 40 satisfying the extra condition that the induced bifibration Groth(ℙ_{(−)}) satisfies both the Fröbenius Reciprocity law and the Beck-Chevalley condition.

Presheaf models for Proc, ℙ_{(−)}, induce categorical models in the sense of Definition 37.

Theorem 43 If ℙ_{(−)} is a presheaf model for Proc, then Groth(ℙ_{(−)}) is a model in the sense of Definition 37, where the prefixing functors are defined as follows, for any a ∈ L:

\xymatrix{P re_{a,L} : ℙ̂_{L} \ar[r]^{I_{L,∗}} & \begin{matrix} \\ (ℙ_{L}) & ⊥ \end{matrix} \ar[r]^{pre_{a,L,!}} & ℙ̂_{L} ,}

where we recall that pre_{a,L,!} = Lan_{y_{_{(ℙ_{L})}_{⊥}}}(y_{ℙ_{L}pre_{a,L}}) and I_{L,∗} is defined as in Section 1.4.

To prove the theorem we need the following lemma:

Lemma 44 Let F : ℙ_{⊥} → ℚ_{⊥} be a functor and let I_{ℙ} : ℙ → ℙ_{⊥} and I_{ℚ} : ℚ → ℚ_{⊥} be the obvious embeddings, then the following square commutes up to a natural isomorphism:

\xymatrix{ℙ̂ \ar[r]^{I_{ℙ,∗}} \ar[d]_{F^{l}} & ℙ̂_{⊥} \ar[d]^{F_{!}} \\ ℚ̂ \ar[r]^{I_{ℚ,∗}} & ℚ̂_{⊥} .}

Proof: Observe that all the arrows in the above square are connected-colimit preserving functors. It is now an easy calculation to show that

F_{!}I_{ℙ,∗}y_{ℙ}^{∘} ≅ I_{ℚ,∗}F^{l}y_{ℙ}^{∘} .

Thus F_{!}I_{ℙ,∗} is isomorphic to I_{ℚ,∗}F^{l}. □

Proof:[of Theorem 43] The only thing which we need to check is that the prefixing functors satisfy the condition given in Definition 37. The check is provided by the following chain of isomorphisms:

\overline{λ}^{l}P re_{a,L} = \overline{λ}^{l}pre_{a,L,!}I_{L,∗}  (by definition of P re)
≅ I_{M}^{∗} \overline{λ}_{!}I_{L,!}pre_{a,L,!}I_{L,∗}  (by Proposition 22)
≅ I_{M}^{∗}I_{M,!}pre_{λ(a),M,!}\overline{λ}_{!}I_{L,∗}  (by Definition 40)
≅ pre_{λ(a),M,!}\overline{λ}_{!}I_{L,∗}  (since I_{M} is an embedding)
≅ pre_{λ(a),M,!}I_{M,∗}\overline{λ}^{l}  (by Lemma 44)
≅ P re_{λ(a),M} \overline{λ}^{l}  (by definition of P re).
□

We can now equip our model with a canonical notion of bisimulation. We first bring two objects over a common fibre and then see whether they are open map bisimilar there.

Definition 45 (Open map bisimulation in Groth(ℙ_{(−)})) Let ⟨X, L⟩ and ⟨Y, M⟩ be two objects in Groth(ℙ_{(−)}). We say that they are (open map) bisimilar if \overline{i_{L}}^{l}(⟨X, L⟩) and \overline{i_{M}}^{l}(⟨Y, M⟩) are related by a span of ℙ_{L∪M}-open maps, where i_{L} and i_{M} are the set inclusions L ↪^{i_{L}} L ∪ M ↩^{i_{M}} M.

Notation: In the remainder of this paper, we shall write ⟨X, L⟩ ∼ ⟨Y, M⟩ to mean that they are open map bisimilar, and X ∼_{L} Y to say that both X and Y are in |ℙ̂_{L} | and that they are ℙ_{L}-open bisimilar. Hence we have that

⟨X, L⟩ ∼ ⟨Y, M⟩ if and only if \overline{i_{L}}^{l}(X) ∼_{L∪M} \overline{i_{M}}^{l}(Y) .

From the above definition we immediately see that moving objects across different fibres along cocartesian liftings preserves bisimulation. But we can deduce more: bisimulation is a congruence with respect to the process operations. Its proof relies mainly on Theorems 17 and 18. We begin by observing that for any ⟨X, L⟩ in Groth(ℙ_{(−)}), there exists a least subset L′ of L with inclusion function i : L′ ↪ L, such that, ⟨\overline{i}^{r}X, L′⟩ ∼ ⟨X, L⟩.

Proposition 46 Let ⟨X, L⟩ ∈| Groth(ℙ_{−}) |. Let M ↪^{i} L ↩^{j} N be two inclusions, such that ⟨\overline{i}^{r}X, M⟩ ∼ ⟨X, L⟩ ∼ ⟨\overline{j}^{r}X, N⟩, then if

\xymatrix{M ∩ N \ar@{^{(}->}[r]^{l} \ar@{^{(}->}[d]_{k} & M \ar@{^{(}->}[d]^{i} \\ N \ar@{^{(}->}[r]_{j} & L}

is the obvious pullback square of inclusions,

⟨\overline{j}^{r}\overline{k}^{r}X, M ∩ N⟩ = ⟨\overline{l}^{r}\overline{i}^{r}X, M ∩ N⟩ ∼ ⟨X, L⟩ .

Proof: The equality holds obviously. For bisimilarity we need to show that \overline{i}^{l}\overline{l}^{l}\overline{l}^{r}\overline{i}^{r}X ∼_{L} X. By assumption \overline{i}^{l}\overline{i}^{r}X ∼_{L} X, hence by Theorem 18, \overline{j}^{r}\overline{i}^{l}\overline{i}^{r}X ∼_{N} \overline{j}^{r}X. By the Beck-Chevalley condition, \overline{j}^{r}\overline{i}^{l}\overline{i}^{r}X ≅ \overline{k}^{l}\overline{l}^{r}\overline{i}^{r}X, hence by composing with \overline{j}^{l}, \overline{j}^{l}\overline{k}^{l}\overline{l}^{r}\overline{i}^{r}X ∼_{L} \overline{j}^{l}\overline{j}^{r}X ∼_{L} X. Since the square of inclusions is a commutative one, we know that \overline{j}^{l}\overline{k}^{l} ≅ \overline{i}^{l}\overline{l}^{l}, thus

\overline{i}^{l}\overline{l}^{l}\overline{l}^{r}\overline{i}^{r}X ∼_{L} X .
□

Corollary 47 For any ⟨X, L⟩ ∈|Groth(ℙ_{−})|, there exists a least subset L′ of L such that ⟨\overline{i}^{r}X, L′⟩ ∼ ⟨X, L⟩, where i : L′ ↪ L is the inclusion function.

Proof: Take L′ to be equal to the intersection of all M ⊆ L, such that ⟨\overline{i_{M}}^{r}X, M⟩ ∼ ⟨X, L⟩, where i_{M} : M ↪ L is the inclusion function. □

Definition 48 For any ⟨X, L⟩ ∈| Groth(ℙ_{−}) |, say that X reduces to M, if M is a subset of L, and ⟨X, L⟩ ∼ ⟨\overline{i}^{r}X, M⟩. If L′ is the least subset of L for which X can be reduced to, say that X has support L′.

That a presheaf X over paths ℙ_{L} reduces to a presheaf over paths ℙ_{L′} with L′ ⊆ L means that X is described to within bisimulation as a presheaf over ℙ_{L′}.

The above results yield the following characterisations of bisimilarity.

Proposition 49 Two objects ⟨X, L⟩, ⟨Y, M⟩ ∈| Groth(ℙ_{−}) | are bisimilar iff they both reduce to L ∩ M and \overline{i}^{r}X ∼_{L∩M} \overline{j}^{r}Y, for L ↩^{i} L ∩ M ↪^{j} M.

Corollary 50 Two objects ⟨X, L⟩, ⟨Y, M⟩ ∈|Groth(ℙ_{−})| are bisimilar iff they have the same set N as support with L ↩^{i} N ↪^{j} M and \overline{i}^{r}X ∼_{N} \overline{j}^{r}Y.

As we shall see all the operations involved in the semantics of Proc preserve bisimulation.

Before going into the semantics of Proc in presheaf models we recall the following instantiation of Proposition 32 to Groth(ℙ_{(−)}).

Proposition 51 Let ℙ_{(−)} : Set_{∗} → Cat be a presheaf model for Proc . Let i : L ↣ M be a monomorphism in Set_{∗}, i.e., an injective (total) function. Then the following facts hold:

• \overline{i}^{r}\overline{i}^{l} ≅ 1_{ℙ_{L}}.

• \overline{i}^{l} preserves products in the fibres, i.e., for every two presheaves X, Y ∈|ℙ̂_{L} |,

\overline{i}^{l}(X × Y) ≅ \overline{i}^{l}(X) × \overline{i}^{l}(Y) .^{7}

4 Semantic constructions in Groth(ℙ_{(−)})

We analyse the constructions used in Groth(ℙ_{(−)}) to give the semantics of Proc according to Section 2.1 and show that they preserve bisimulation.

Products: As we have already said the category Groth(ℙ_{(−)}) has products. They can be constructed (cf. Proposition 35) using the products in the fibres as follows. Given ⟨X, L⟩, ⟨Y, M⟩ ∈ |Groth(ℙ_{(−)})|. Define

⟨X, L⟩ × ⟨Y, M⟩ = ⟨\overline{π_{L}}^{r}(X) × \overline{π_{M}}^{r}(Y), L ×_{∗} M⟩

where L ↼^{π_{L}} L ×_{∗} M ⇀^{π_{M}} M are the projections of the product in Set_{∗}.

Proposition 52 If ⟨X, L⟩ is open map map bisimilar to ⟨X′, L′⟩ and ⟨Y, M⟩ is open map bisimilar to ⟨Y′, M′⟩ then the product ⟨X, L⟩ × ⟨Y, M⟩ is open map bisimilar to the product ⟨X′, L′⟩ × ⟨Y′, M′⟩.

7 We use the same symbol “×” to indicate the product of two objects in a category, irrespective of the fact that sometime, as here, products taken in different categories appear in the same expression. We believe the reader can disambiguate from the context.

Proof: Let N = L ×_{∗} M and N′ = L′ ×_{∗} M′. Consider the diagram

\xymatrix{L \ar@{^{(}->}[d]_{i_{L}} & N \ar@{^{(}->}[d]_{i_{N}} \ar[r]^{π_{M}} \ar[l]_{π_{L}} & M \ar@{^{(}->}[d]^{i_{M}} \\ L ∪ L′ & N ∪ N′ \ar[l]|{α} \ar[r]^{β} & M ∪ M′ \\ L′ \ar@{^{(}->}[u]^{i′_{L}} & N′ \ar@{^{(}->}[u]^{i_{N′}} \ar[r]^{π_{M′}} \ar[l]_{π_{L′}} & M′ , \ar@{^{(}->}[u]^{i_{M′}}}

with α and β the obvious projecting partial functions. Observe that since the set N ∪ N′ is included in (L ∪ L′) ×_{∗} (M ∪ M′), then both the upper diagram and the lower one are limiting cones of vertex N and N′, respectively. Hence by Proposition 34 we have the following two isomorphisms in { \atop ℙ_{N∪N′}}:

\overline{i_{N}}^{l}(\overline{π_{L}}^{r}X × \overline{π_{M}}^{r}Y) ≅ \overline{α}^{r}\overline{i_{L}}^{l}X × \overline{β}^{r}\overline{i_{M}}^{l}Y
\overline{i_{N′}}^{l}(\overline{π_{L′}}^{r}X′ × \overline{π_{M′}}^{r}Y′) ≅ \overline{α}^{r}\overline{i_{L′}}^{l}X′ × \overline{β}^{r}\overline{i_{M′}}^{l}Y′ .

Consequently, we have to prove that assuming \overline{i_{L}}^{l}X ∼_{L∪L′} \overline{i_{L′}}^{l}X′ and \overline{i_{M}}^{l}Y ∼_{M∪M′} \overline{i_{M′}}^{l}Y′ we have

\overline{α}^{r}\overline{i_{L}}^{l}X × \overline{β}^{r}\overline{i_{M}}^{l}Y ∼_{N∪N′} \overline{α}^{r}\overline{i_{L′}}^{l}X′ × \overline{β}^{r}\overline{i_{M′}}^{l}Y′ .

By Theorem 18, we deduce that \overline{α}^{r}\overline{i_{L}}^{l}X ∼_{N∪N′} \overline{α}^{r}\overline{i_{L′}}^{l}X′ and \overline{β}^{r}\overline{i_{M}}^{l}Y ∼_{N∪N′} \overline{β}^{r}\overline{i_{M′}}^{l}Y′. Hence, by Proposition 7

\overline{α}^{r}\overline{i_{L}}^{l}X × \overline{β}^{r}\overline{i_{M}}^{l}Y ∼_{N∪N′} \overline{α}^{r}\overline{i_{L′}}^{l}X′ × \overline{β}^{r}\overline{i_{M′}}^{l}Y′ .
□

Note that the above proof makes essential use of the Beck-Chevalley condition and the Fröbenius Reciprocity law (via Proposition 34).

Sum: Let ⟨X, L⟩, ⟨Y, M⟩ ∈ |Groth(ℙ_{(−)})|. Define

⟨X, L⟩ ⊕ ⟨Y, M⟩ = ⟨\overline{i_{L}}^{l}(X) + \overline{i_{M}}^{l}(Y), L ∪ M⟩

where L →^{i_{L}} L ∪ M ←^{i_{M}} M are the obvious set inclusions.

Proposition 53 The functor ⊕ preserves open map bisimulation; if ⟨X, L⟩ is open map bisimilar to ⟨X′, L′⟩ and ⟨Y, M⟩ is open map bisimilar to ⟨Y′, M′⟩ then ⟨X, L⟩ ⊕ ⟨Y, M⟩ is open map bisimilar to ⟨X′, L′⟩ ⊕ ⟨Y′, M′⟩

Proof: The proof is a straightforward application of Theorem 17. Let N = L ∪ M, N′ = L′ ∪ M′, L′′ = L ∪ L′ and N′′ = N ∪ N′. Consider the following diagram of inclusions:

\xymatrix{L \ar@{^{(}->}[d]_{i_{L}} \ar@{^{(}->}[r]^{j_{L}} & N \ar@{^{(}->}[d]_{i_{N}} & M \ar@{^{(}->}[d]^{i_{M}} \ar@{^{(}->}[l]_{j_{M}} \\ L′′ \ar@{^{(}->}[r]^{j_{L′′}} & N′′ & M′′ \ar@{^{(}->}[l]_{j_{M′′}} \\ L′ \ar@{^{(}->}[u]^{i_{L′}} \ar@{^{(}->}[r]_{j_{L′}} & N′ \ar@{^{(}->}[u]^{i_{N′}} & M′ . \ar@{^{(}->}[l]^{j_{M′}} \ar@{^{(}->}[u]_{i_{M′}}}

By assumption \overline{i_{L,!}}X ∼_{L′′} \overline{i_{L′,!}}X′ and \overline{i_{M,!}}X ∼_{M′′} \overline{i_{M′,!}}X′, hence

\overline{i_{N,!}}(\overline{j_{L,!}}X + \overline{j_{M,!}}Y) ≅ \overline{i_{N,!}}\overline{j_{L,!}}X + \overline{i_{N,!}}\overline{j_{M,!}}Y
≅ \overline{j_{L′′,!}}\overline{i_{L,!}}X + \overline{j_{M′′,!}}\overline{i_{M,!}}Y
∼_{N′′} \overline{j_{L′′,!}}\overline{i_{L′,!}}X′ + \overline{j_{M′′,!}}\overline{i_{M′,!}}Y′
≅ \overline{i_{N′,!}}\overline{j_{L′,!}}X′ + \overline{i_{N′,!}}\overline{j_{M′,!}}Y′
≅ \overline{i_{N′,!}}(\overline{j_{L′,!}}X′ + \overline{j_{M′,!}}Y′) .
□

Remark: This sum construction is not the coproduct because of the choice of labelling set for the sum. It can be shown that, if [i_{L}, i_{M}] : L + M → L ∪ M is the mediating map from the coproduct of sets, then

⟨X, L⟩ ⊕ ⟨Y, M⟩ ≅ \overline{[i_{L}, i_{M}]}^{l}(⟨X, L⟩ + ⟨Y, M⟩).

Restriction: Let Λ be a set and let ⟨X, L⟩ ∈ |Groth(ℙ_{(−)})|. Then consider the inclusion map i : Λ ∩ L ↪ L and define the restriction of X to Λ ∩ L to be

⟨X, L⟩↾Λ = ⟨\overline{i}^{r}(X), Λ ∩ L⟩ .

Proposition 54 The functor (−) ↾ Λ preserves open map bisimulation; if ⟨X, L⟩ is open map bisimilar to ⟨X′, L′⟩ then ⟨X, L⟩↾Λ is open map bisimilar to ⟨X′, L′⟩↾Λ

Proof: Consider the diagram of inclusions

\xymatrix{Λ ∩ L \ar@{^{(}->}[r]^{k} \ar@{^{(}->}[d]_{j_{L}} & L \ar@{^{(}->}[d]^{i_{L}} \\ Λ ∩ (L ∪ L′) \ar@{^{(}->}[r]|{l} & L ∪ L′ \\ Λ ∩ L′ \ar@{^{(}->}[r]|{m} \ar@{^{(}->}[u]^{j_{L′}} & L′ . \ar@{^{(}->}[u]_{i_{L′}}}

Both squares are readily seen to be pullbacks, therefore by Beck-Chevalley, \overline{j_{L}}^{l}\overline{k}^{r} ≅ \overline{l}^{r}\overline{i_{L}}^{l} and \overline{j_{L′}}^{l}\overline{m}^{r} ≅ \overline{l}^{r}\overline{i_{L′}}^{l}. Assuming, \overline{i_{L}}^{l}X ∼_{L∪L′} \overline{i_{L′}}^{l}X′, we can deduce

\overline{j_{L}}^{l}\overline{k}^{r}X  ≅ \overline{l}^{r}\overline{i_{L}}^{l}X
∼_{Λ∩(L∪L′)} \overline{l}^{r}\overline{i_{L′}}^{l}X′ (by Theorem 18)
≅ \overline{j_{L′}}^{l}\overline{m}^{r}X′ .

□

Relabelling: Let Ξ : L → M be total. Take ⟨X, L⟩ as usual, define the relabelling to be

⟨X, L⟩[Ξ] = ⟨\overline{Ξ}^{l}(X), M⟩ .

Relabelling preserves bisimulation:

Proposition 55 If ⟨X, L⟩ is open map bisimilar to ⟨X′, L′⟩ then ⟨X, L⟩[Ξ] is open map bisimilar to ⟨X′, L′⟩[Ξ]

Proof: Again this is a straightforward application of Theorem 17. Consider the commuting diagram

\xymatrix{L \ar[r]^{Ξ_{L}} \ar@{^{(}->}[d]_{i_{L}} & Ξ_{L}L \ar@{^{(}->}[d]^{j_{L}} \\ L ∪ L′ \ar[r]^{Ξ_{L∪L′}} & Ξ_{L∪L′}(L ∪ L′) \\ L′ \ar[r]^{Ξ_{L′}} \ar@{^{(}->}[u]^{i_{L′}} & L′ . \ar@{^{(}->}[u]^{j_{L′}}}

Knowing that \overline{i_{L,!}}X ∼_{L∪L′} \overline{i_{L′,!}}X′, we obtain

\overline{j_{L,!}}\overline{Ξ_{L,!}}X  ≅  \overline{Ξ_{L∪L′,!}}\overline{i_{L,!}}X
∼_{Ξ_{L∪L′}L∪L′} \overline{Ξ_{L∪L′,!}}\overline{i_{L′,!}}X′
≅  \overline{j_{L′,!}}\overline{Ξ_{L′,!}}X′ .
□

Prefixing: Prefixing is dealt with by using the functors P re_{a,L} defined as in Theorem 43. The preservation property of bisimulation is automatically ensured.

Proposition 56 Let a ∈ L ∩ L′. If ⟨X, L⟩ is open map bisimilar to ⟨X′, L′⟩ then P re_{a,L}(⟨X, L⟩) is open map bisimilar to P re_{a,L′}(⟨X′, L′⟩)

Recursion: Letting F : Groth(ℙ_{(−)}) → Groth(ℙ_{(−)}) be a functor, define rec(F) to be the colimit colim ω_{F} where

ω_{F} : \begin{matrix}ω & → & Groth(ℙ_{(−)}) \\ n & ↦ & F^{n}(⟨0, ∅⟩). \end{matrix}

Here 0 is the unique, up to isomorphism, presheaf over ℙ_{∅}. Any F^{n}(⟨0, ∅⟩) consists of a pair ⟨X_{n}, L_{n}⟩ with X_{n} ∈ |ℙ̂_{L_{n}}|, and we can express the colimit as a pair ⟨X, L⟩, where L is the colimit in Set_{∗} of the L_{n} and X is the colimit in ℙ̂_{L} of all the cocartesian liftings of the X_{n}, along the edges of the cocone i_{n} : L_{n} → L.

We already observed that the operations on Groth(ℙ_{(−)}) associated with the term constructors are functors but for the sum (− ⊕ −); the sum nevertheless becomes functorial if one restricts to Groth(ℙ_{(−)})_{in}, the subcategory of Groth(ℙ_{(−)}) with morphisms given by pairs ⟨f, i⟩ where i is an inclusion of sets. Having F : Groth(ℙ_{(−)})_{in} → Groth(ℙ_{(−)})_{in}, we can define rec(F) as above. Notice that L = ∪_{n}L_{n} and every i_{n} : L_{n} → L is an inclusion of sets.

All our constructions are continuous with respect to ω-chains (particular kinds of connected diagram) and restrict to Groth(ℙ_{(−)})_{in}. Hence rec(F) determines a fixed point where F is derived from a denotation of a term t as in Section 2.1. So, the construction above yields a denotation for a recursively defined process in terms of an ω-colimit of presheaves over a common path category. We would like to deduce the bisimulation of recursive processes rec x.t, rec y.u from bisimulation between the open terms t and u. Such open terms give rise to endofunctors on Groth(ℙ_{(−)})_{in} We start by extending the notion of open map, and therefore bisimulation, to functors. Following Definition 45 and 48, we first say when an arrow ⟨f, i⟩ in Groth(ℙ_{(−)})_{in} (and hence in Groth(ℙ_{(−)})) is open.

Definition 57 An arrow ⟨f, i⟩ : ⟨X, L⟩ → ⟨Y, M⟩ in Groth(ℙ_{(−)})_{in} is open if the transpose f′ : \overline{i}^{l}X → Y of f, with respect to the adjunction \overline{i}^{l} ⊣ \overline{i}^{r}, is ℙ_{M}-open.

Proposition 58 If ⟨f, i⟩ : ⟨X, L⟩ → ⟨Y, M⟩ is open in the sense of Definition 57 above, then f is ℙ_{L}-open and Y reduces to L.

Proof: By the adjunction f = \overline{i}^{r}(f′)η_{X}, where η_{X} is the unit at X of the adjunction \overline{i}^{l} ⊣ \overline{i}^{r}. But we know that η_{X} is an isomorphism, since i is a monomorphism (cf. Proposition 51), hence f is the composite of two open maps and therefore is open. So we have that X ∼_{L} \overline{i}^{r}Y, hence \overline{i}^{l}X ∼_{M} \overline{i}^{l}\overline{i}^{r}Y. Therefore Y ∼_{M} \overline{i}^{l}X ∼_{M} \overline{i}^{l}\overline{i}^{r}Y. □

An obvious question is whether the Proposition 58 above can be made into an “if and only if” statement. However, we seem to need an extra assumption on the presheaf model to obtain the converse implication. For instance, using Lemma 6(ii) of [19] we can obtain the following:

Proposition 59 Let ℙ_{(−)} : Set_{∗} → Cat be a presheaf model such that for any injective total function (i.e., any monomorphism of Set_{∗}), i : L → M and for any two objects P ∈|ℙ_{L} | and Q ∈|ℙ_{M} |,

ℙ_{M}[Q, \overline{i}P] ≠ ∅ only if Q ≅ \overline{i}P′ for some P′ ∈|ℙ_{L} | .

Then, for any Y ∈| ℙ̂_{M} | with support L, the counit, ε_{Y}, of the adjunction \overline{i}^{l} ⊣ \overline{i}^{r} is ℙ_{M}-open.

It is now seen that the proposition above induces the converse of Proposition 58, since f′ = ε_{Y} \overline{i}^{l}f. Notice that both the presheaf models of Example 41 satisfy the condition required by Proposition 59.

Back to recursion:

Definition 60 Let F, G : C → Groth(ℙ_{(−)})_{in} be two functors. Let α : F ⟶^{.} G be a natural transformation. Say that α is open if for every c ∈|C |, α_{c} is open according to Definition 57.

We consider two endofunctors F, G on Groth(ℙ_{(−)})_{in} bisimilar if there is another endofunctor R and a span of open natural transformations α : R →^{.} F and β : R →^{.} G relating them.

Proposition 61 Let C be a category with initial object 0. Every natural transformation α : R ⟶^{.} F, with R, F : C → C endofunctors induces a natural transformation ω_{α} : ω_{R} ⟶^{.} ω_{F} where ω_{R} (ω_{F}) are defined inductively by:

• ω_{R}(0) = 0 (ω_{F} (0) = 0)

• ω_{R}(n + 1) = R(ω_{R}(n)) (ω_{F} (n + 1) = F (ω_{F} (n))

• ω_{R}(0 ≤ 1) = 0_{R0} (ω_{F} (0 ≤ 1) = 0_{F 0})

• ω_{R}(n+1 ≤ n+2) = R(ω_{R}(n ≤ n+1) (ω_{F} (n+1 ≤ n+2) = F (ω_{F} (n ≤ n+1))

Proof: Inductively define

• (ω_{α})_{0} =^{def} 1_{0}

• (ω_{α})_{n+1} =^{def} α_{F^{n}0}R((ω_{α})_{n}) = F ((ω_{α})_{n})α_{R^{n}0} where the second equality holds by naturality of α.

To check that ω_{α} is a natural transformation, we need to show that the following square commutes for any n ≥ 0:

\xymatrix{R^{n}0 \ar[r]^{ω_{R}(n≤n+1)} \ar[d]_{(ω_{α})_{n}} & R^{n+1}0 \ar[d]^{(ω_{α})_{n+1}} \\ F^{n}0 \ar[r]_{ω_{F} (n≤n+1)} & F^{n+1}0 .}

The proof goes routinely, by induction. The base case follows immediately by initiality of 0. Assuming n > 0, we see that

(ω_{α})_{n+1}ω_{R}(n ≤ n + 1) = (ω_{α})_{n+1}R(ω_{R}(n − 1 ≤ n))

(by definition of ω_{R})

= α_{F^{n}0}R((ω_{α})_{n})R(ω_{R}(n − 1 ≤ n))

(by definition of ω_{α})

= α_{F^{n}0}R((ω_{α})_{n}ω_{R}(n − 1 ≤ n))

(by functoriality of R)

= α_{F^{n}0}R(ω_{F} (n − 1 ≤ n)(ω_{α})_{n−1})

(by inductive hypothesis)

= α_{F^{n}0}R(ω_{F} (n − 1 ≤ n))R((ω_{α})_{n−1})

(by functoriality of R)

= F (ω_{F} (n − 1 ≤ n))α_{F^{n−1}0}R((ω_{α})_{n−1})

(by naturality of α)

= ω_{F} (n ≤ n + 1)(ω_{α})_{n}

(by definition).

□

We deduce:

Proposition 62 Let F, R be endofunctors of Groth(ℙ_{(−)})_{in} and let α : R →^{.} X be a natural transformation. Then there is a natural transformation ω_{α} : ω_{R} →^{.} ω_{F}. Moreover if α is open and X preserve open morphisms, then ω_{α} is open.

Proof: Proposition 61, instantiated to Groth(ℙ_{(−)})_{in}, proves the first part. The second part is immediately verified by inspecting the definition of ω_{α}. □

Open maps are preserved in passing to the colimit, in particular:

Proposition 63 Let F, R : ω → ℙ̂ be functors and α : R →^{.} F a natural transformation such that for every n, α_{n} is a ℙ-open map. Then the map colim α : colim R → colim F, uniquely determined by the universal property of colimits, is a ℙ-open map.

Proof: Let the following be a commutative square with P and Q objects of ℙ:

\xymatrix{P \ar[r]^{p} \ar[d]_{m} & colim R \ar[d]^{colim α} \\ Q \ar[r]_{q} & colim F .}  (1)

Since colim R and colim F are colimits of ω-chains there exists a number n and arrows

p_{n} : P → R(n) and q_{n} : Q → F (n)

such that the following diagram commutes:

\xymatrix{P \ar[r]^{p_{n}} \ar[d]_{m} \ar[rr]^{p} & R(n) \ar[d]^{α_{n}} \ar[r]^{R_{n,∞}} & colim R \ar[d]^{colim α} \\ Q \ar[r]_{q_{n}} \ar[rr]_{q} & F (n) \ar[r]_{F_{n,∞}} & colim F ,}

where R_{n,∞} and F_{n,∞} are edges of the corresponding colimiting cones. By assumption, α_{n} is ℙ-open, hence there exists r_{n} : Q → R(n) splitting the leftmost square in two commutative triangles. Then

r =^{def} R_{n,∞}r_{n}

is an arrow from Q to colim R that splits the Diagram (1) in two commutative triangles.

If every α_{n} is an epimorphic natural transformation, then obviously, since colimits in presheaf categories are calculated pointwise, colim α is epimorphic as well. □

Since the calculation of colimits of ω-chains in Groth(ℙ_{(−)})_{in} is reduced to calculating them in the colimiting fibre, the above proposition yields:

Proposition 64 Let ω_{F} , ω_{R} : ω → Groth(ℙ_{(−)})_{in} and ω_{α} : ω_{R} →^{.} ω_{F}, be as in Proposition 62, with ω_{α} open, then the (adjoint transpose of the) arrow

colim ω_{α} : colim ω_{R} → colim ω_{F} ,

uniquely determined by the universal property of the colimit, is an open map in the fibre over the colimiting labelling set.

Proof: We have already remarked that colimits of ω-chains

⋯ → ⟨X_{n}, L_{n}⟩ → ⟨X_{n+1}, L_{n+1}⟩ → ⋯,

in Groth(ℙ_{(−)})_{in} are obtained by taking first the union

L = ∪_{n∈ω}L_{n}

of the all the labelling sets in the chain and then calculating the colimit of the chain induced in the fibre over L, by cocartesian liftings of all the X_{n}. We now make this explanation more precise, in order to show that the functor part of colim α arises from a situation satisfying the hypothesis of Proposition 63. We need some notation first. Let’s write ⟨R_{n}, L_{n}⟩ for ω_{R}(n), ⟨F_{n}, M_{n}⟩ for ω_{F} (n). For every n, let ⟨r_{n}, i_{n}⟩ and ⟨f_{n}, j_{n}⟩ be ω_{R}(n ≤ n + 1) and ω_{F} (n ≤ n + 1), where, for simplicity we already assume that r_{n} : \overline{(i_{n})}^{l}R_{n} → R_{n+1} and f_{n} : \overline{(j_{n})}^{l}F_{n} → F_{n+1}, rather than taking their transposes. For every n, let ⟨α_{n}, k_{n}⟩ be (ω_{α})_{n}, where again we take α_{n} : \overline{(k_{n})}^{l}R_{n} → F_{n}. Naturality of ω_{α} means that the following square commutes (where the indicated isomorphisms are uniquely determined by the universal property of left Kan extensions):

\xymatrix{\overline{(j_{n}k_{n})}^{l}R_{n} = \overline{(k_{n+1}i_{n})}^{l}R_{n} \ar[r]|{≃} \ar[d]_{≅} & \overline{(k_{n+1})}^{l}\overline{(i_{n})}^{l}R_{n} \ar[r]^{\overline{(k_{n+1})}^{l}r_{n}} & \overline{(k_{n+1})}^{l}R_{n+1} \ar[dd]^{α_{n+1}} \\ \overline{(j_{n})}^{l}\overline{(k_{n})}^{l}R_{n} \ar[d]_{\overline{(j_{n})}^{l}α_{n}} \\ \overline{(j_{n})}^{l}F_{n} \ar[rr]_{f_{n}} &  & F_{n+1} .}

Now, writing

i_{n,∞} : L_{n} → L = ∪_{n∈ω}L_{n} ,

for every n, and ⟨R_{∞}, L⟩ for colim ω_{R}, we have that R_{∞} can be calculated as the colimit of the following chain in ℙ̂_{L}:

\xymatrix{⋯ \ar[r] & \overline{(i_{n,∞})}^{l}R_{n} \ar[r]|{≃} & \overline{(i_{n+1,∞})}^{l}\overline{(i_{n})}^{l}R_{n} \ar[r]^{\overline{(i_{n+1,∞})}^{l}r_{n}} & \overline{(i_{n+1,∞})}^{l}R_{n+1} \ar[r] & · · · .}

Similarly one calculates colim F, moreover from the commutativity of the above diagram it follows that for every n, the following diagram commutes too (where k : L ↪ M is the inclusion function):

\xymatrix{\overline{k}^{l}\overline{(i_{n,∞})}^{l}R_{n} \ar[r]|{≃} \ar[d]_{≅} & \overline{k}^{l}\overline{(i_{n+1,∞})}^{l}\overline{(i_{n})}^{l}R_{n} \ar[r]^{\overline{k}^{l}\overline{(i_{n+1,∞})}^{l}r_{n}} & \overline{k}^{l}\overline{(i_{n+1,∞})}^{l}R_{n+1} \ar[d]^{≅} \\ \overline{(j_{n,∞}k_{n})}^{l} = \overline{(ki_{n,∞})}^{l}R_{n} \ar[d]_{≅} &  & \overline{(j_{n+1,∞}k_{n+1})}^{l} = \overline{(ki_{n+1,∞})}^{l}R_{n+1} \ar[d]^{≅} \\ \overline{(j_{n,∞})}^{l}\overline{(k_{n})}^{l}R_{n} \ar[d]_{\overline{(j_{n,∞})}^{l}α_{n}} &  & \overline{(j_{n+1,∞)}}^{l}\overline{(k_{n+1})}^{l}R_{n+1} \ar[d]^{\overline{(j_{n+1,∞})}^{l}α_{n+1}} \\ \overline{(j_{n,∞})}^{l}F_{n} \ar[r]|{≃} & \overline{(j_{n+1,∞})}^{l}\overline{(j_{n})}^{l}F_{n} \ar[r]^{\overline{(j_{n+1,∞})}^{l}f_{n}} & \overline{(j_{n+1,∞)}}^{l}F_{n+1} .}

Hence α_{∞} : \overline{k}^{l}R_{∞} → F_{∞} is the unique mediating morphism between two colimiting cones connected by a natural transformation that is pointwise an open map, since every vertical arrow in the diagram above is either an isomorphism (hence an open map) or the transformation along a colimit preserving functor of an open map (hence an open map because of Theorem 17). This falls within the hypothesis of Proposition 63, and so α_{∞} is ℙ_{M}-open. □

Consequently, if two endofunctors F, G ranging over Groth(ℙ_{(−)})_{in} are bisimilar and preserve open maps, then the colimits rec(F), rec(G) are bisimilar. A term with a free variable, built-up from the constructions of this section, will determine an endofunctor on Groth(ℙ_{(−)})_{in} which preserves open maps by this section propositions. It follows that if two open terms t and u are bisimilar, i.e., induce bisimilar functors, then the recursive definitions rec x.t and rec y.u are bisimilar.

5 Concrete models revisited

We have already mentioned the full embeddings

\begin{matrix}ST_{L} ↪ L̂^{+} \\ ES_{L} ↪ \begin{matrix} \\ Pom & L \end{matrix} \end{matrix}

The first is actually an equivalence of categories. The second is a strict inclusion (for instance the terminal presheaf cannot be represented as an event structure) that not only preserves but reflects bisimulation (see Proposition 12). We consider the presheaf models Groth((−)^{+}) and Groth(Pom_{(−)}) of Example 41. We can now transfer the results from the presheaf models to the concrete models of synchronisation trees and event structures by noting that the canonical embeddings between fibres, ST_{L} → L̂^{+} and ES_{L} → \begin{matrix} \\ Pom & L \end{matrix}, extend to full and faithful embeddings from ST and ES to the corresponding presheaf models. In particular we again have that the embedding ST ↪ Groth((−)^{+}) is an equivalence. We illustrate then the situation with event structures.

We recalled in Proposition 36 that the functor p_{ES} : ES → Set_{∗} is a cofibration. We now provide a cocleavage which is functorial (cf. end of Section 1.5) and hence makes p_{ES} : ES → Set_{∗} into a split cofibration.

Let E = (E, ≤, Con, l : E → L) be an event structure and let α : L ⇀ L′ be a partial function. define α_{!}(E) = (E′, ≤′, Con′, l′ : E′ → L′) to consist of:

• E′ = {e ∈ E | α(l(e)) is defined}

• ≤′=≤ ∩(E′ × E′)

• Con′ = {x ∈ Con | x ⊆ E′}

• l′(e′) = α(l(e′)), for every e′ ∈ E′.

It is straightforward to verify that α_{!}(E) is an event structure and that the pair ⟨1′, α⟩, with 1′ : E ⇀ E′ the truncation of the identity functions on events to E′, is an event structure morphism.

Proposition 65 Given an event structure E = (E, ≤, Con, l : E → L) and a partial function α : L ⇀ L′, the event structures morphism ⟨1′, α⟩ is a cocartesian arrow.

We will write α_{!,E} for ⟨1′, α⟩. There is an induced cocartesian lifting functor α_{!} : ES_{L} → ES_{L′}. If we restrict the construction above to pomsets we obtain the functor \overline{α} : (Pom_{L})_{⊥} → (Pom_{L′})_{⊥} of Example 41.

It is easy to verify that this choice of cocartesian lifting functors is functorial:

Proposition 66 Given an event structure E = (E, ≤, Con, l : E → L) and a partial function α : L ⇀ L′, the following hold:

(1) If α = 1_{L}, then α_{!,E} is the identity morphism ⟨1_{E}, 1_{L}⟩ : E → E.

(2) If β : L′ → L′′ is another partial function, then β_{!,α_{!}(E)}α_{!,E} = (βα)_{!,E}.

Notation: If ⟨f, α⟩ : E → \overline{E} is an event structure morphism, write f_{α} for the unique function such that ⟨f, α⟩ = ⟨f_{α}, 1′_{L}⟩α_{!,E}. That is, f_{α} is the restriction of f to the elements of α_{!}(E) that, by the way, is equal to the set {e ∈ E | f(e) is defined}. Call f_{α} the transpose of f.

With this notation in mind, define c : ES → Groth(Pom_{(−)}) to be

• On objects: c(E, ≤, Con, l : E → L) = ⟨c_{L}(E), L⟩

• On arrows: If ⟨f, α⟩ : E → E′ with α : L ⇀ L′, then c(⟨f, α⟩) = ⟨c(f), α⟩ where

c(f) : c_{L}(E) = ES_{L}[−, E] → ES_{L′}[\overline{α}(−), E′] = \overline{α}^{r}(c_{L′}(E′))

is defined by composition and transposition (recall that on pomsets, α_{!} is another name for \overline{α}), i.e., c(f)_{P} (p) = (fp)_{α}.

This defines a functor because from Proposition 66 one has that (1_{E}p)_{1_{L}} = p and (g(fp)_{α})_{β} = (gfp)_{βα} and from these equalities one deduces that c⟨1_{E}, 1_{L}⟩ = ⟨1_{E}, 1_{L}⟩ and c(⟨g, β⟩⟨f, α⟩) = c(⟨gf, βα⟩). Moreover, again from Proposition 66, one sees that for any arrow ⟨f, 1_{L}⟩ : E → E′, (fp)_{1_{L}} = fp, hence c acts as c_{L} when restricted to ES_{L}.

Proposition 67 The functor c : ES → Groth(Pom_{(−)}) is a dense full embedding.

Proof: Straightforward from the fact that c extends the c_{L}’s that were dense full embeddings and the fact that via cocartesian liftings, every arrow between objects of Groth(Pom_{(−)}) in different fibres is uniquely determined by an arrow in a fibre. □

It is known that every dense full embedding preserves limits [30]. Moreover a direct calculation shows that c respects relabelling (i.e., cocartesian liftings) and cartesian liftings of inclusions.

Proposition 68 Let α : L ⇀ M be a partial function, then there is a natural isomorphism

c_{M}α_{!} ≅ \overline{α}^{l}c_{L} .

Let λ : L ↪ M be an inclusion map, then

c_{L}λ^{∗} ≅ \overline{λ}^{r}c_{M} ,

where λ^{∗} is the right adjoint of λ_{!} defined on objects as follows:

λ(E, ≤, Con, l) = (E′, ≤′, Con′, l′) ,

where E′ = {e ∈ E|∀e′ ≤ e ∃a ∈ L λ(a) = l(e′)}, ≤′=≤ ∩E′ × E′, Con′ = {x ∈ Con | x ⊆ E′} and l′(e) = a, where a is the unique element of L, such that λ(a) = l(e).

We have already noticed that c_{L} preserves coproducts (Proposition 13). After Proposition 35 we know that coproducts in a cofibred category are built using coproducts in the fibres and cocartesian liftings, hence c preserves coproducts. Summarising:

Proposition 69 The embedding c : ES → Groth(Pom_{(−)}) preserves all limits that exists in ES, coproducts, cocartesian liftings and cartesian liftings of inclusion.

A denotational semantics of Proc in ES was given in [29] and corresponds to the one described abstractly in Section 2.1. Proposition 69 above ensure that (after the embedding with c) the semantics in ES correspond to the one in Groth(Pom_{(−)}), hence the following:

Theorem 70 Let ES[[ · ]] and Groth(Pom_{(−)})[[ · ]] stand for the respective semantics of Proc. Let ρ : V ars →|ES | be an environment function, then

c(ES[[t]]_{ρ}) ≅ Groth(Pom_{(−)})[[t]]_{c∘ρ} .

By Proposition 12(ii), open maps and bisimulation coincide, via the canonical embeddings, in ES_{L} and the fibre over L in Groth(Pom_{(−)}). Hence we can transfer the congruence property deduced for the presheaf semantics to deduce, in particular, that hereditary history-preserving bisimulation is a congruence for the language Proc.

Theorem 71 Hereditary history-preserving bisimulation is a congruence for the language Proc with respect to the event structure semantics of the language Proc.

6 Refinement for event structures

As a further example of an application of Theorem 17, we prove the refinement operator for event structures proposed in [12] preserves hereditary historypreserving bisimulation (abbreviated to hhpb).

Definition 72 (cf. [12], Section 2) A refinement function is a function r from L to | Pom_{M} |, objects of Pom_{M}; so any element a ∈ L is sent to a non-empty pomset r(a) over M.

Definition 73 (A refinement functor) A refinement function as in the definition above induces a refinement functor

R : Pom_{L} → Pom_{M}

acting as follows:

• On objects: If P = (P, ≤_{P} , λ_{P} , L) is a pomset over L, then define R(P) = (R(P), ≤_{R(P)}, λ_{R(P)}, M) with: · R(P) = {(x, x′)|x ∈ P ∧ x′ ∈ r(λ_{P} (x))} · (x, x′) ≤_{R(P)} (y, y′) if either x ≤_{P} y and x ≠ y or x = y and x′ ≤_{r(λ_{P} (x))} y′ · λ_{R(P)}(x, x′) = λ_{r(λ_{P} (x))}(x′).

• On arrows: If f : P → Q in Pom_{L}, define R(f)(x, x′) = (f(x), x′).

One can see r as inducing a refinement functor, say R^{ES}, on event structures as well. If (E, ≤, Con, l) is an event structure over L, R^{ES}(E) is defined on E, ≤ and l as for pomsets, while X ∈ Con_{R^{ES}(E)} iff {x ∈ E | ∃x′ .(x, x′) ∈ X} ∈ Con.

As remarked in [19], the functor R_{!}, obtained as a left Kan extension, is a good candidate for the extension of this refinement to presheaves including those corresponding to event structures. But does the functor R_{!} act like the operation of refinement R^{ES} on event structures? More precisely, if we let c_{L} : ES_{L} → { \atop Pom}_{L} and c_{M} : ES_{M} → { \atop Pom}_{M} denote the canonical embeddings, do we have that the following square commutes (up to a natural isomorphism)?

\xymatrix{ES_{L} \ar[r]^{c_{L}} \ar[d]_{R^{ES}} & \begin{matrix} \\ Pom & L \end{matrix} \ar[d]^{R_{!}} \\ _{ES_{M}} \ar[r]_{c_{M}} & \begin{matrix} \\ Pom & M \end{matrix}}

We embark on proving that it does.

Lemma 74 Let E be an event structure in ES_{L}, let Q be a pomset over M and let R^{ES} : ES_{L} → ES_{M} be a refinement functor. Then for any q : Q → R^{ES}(E) there exists a pomset P_{q} ∈|Pom_{L} | and a morphism p : P → E such that

• There exists a morphism p_{q} : Q → R^{ES}(P) = R(P) such that q = R^{ES}(p)p_{q}.

• For any other factorisation

\xymatrix{Q \ar[rr]^{q} \ar[dr]_{p′_{q}} &  & R^{ES}(E) \\  & R^{ES}(P′) \ar[ur]_{R^{ES}(p′)}}

there exists a unique mediating morphism of pomsets, m : P → P′, such that

p′_{q} = R^{ES}(m)p_{q}  and  p′m = p .

Proof: Define P = {e ∈ E|∃(e, f) ∈ R(E) ∃y ∈ Q q(y) = (e, f)}, with the order relation induced by Q, i.e., e ≤_{P} e′ if either e = e′ or there exist y ≤_{Q} y′ with q(y) = (e, f) and q(y′) = (e′, f′). The verification of the properties is straightforward. □

Proposition 75 Let i_{L} : Pom_{L} → ES_{L} and i_{M} : Pom_{M} → ES_{M} be the inclusion functors, then

R^{ES} ≅ Lan_{i_{L}}(i_{M} ∘ R).

Proof: Recall that Pom_{L} is dense in ES_{L}, i.e., for every E ∈|ES_{L} |,

E ≅ colim i_{L}/E → Pom_{L} ⟶^{i_{L}} ES_{L}.

Using the Lemma 74 above it is not difficult to verify that

R^{ES}(E) ≅ colim i_{L}/E → Pom_{L} ⟶^{R} Pom_{M} ⟶^{i_{M}} ES_{M} .  (2)

From this we can deduce that R^{ES} ≅ Lan_{i_{L}}(i_{M} ∘ R). In fact R^{ES} ∘ i_{L} = i_{M} ∘ R and moreover if F : ES_{L} → ES_{M} is a functor and α : F ∘ i_{L} ⟶^{.} R ∘ i_{m} is a natural transformation, there exists a unique β : R^{ES} ⟶^{.} F such that

β_{i_{L}} = α.  (3)

To show this, observe first of all that if β is a natural transformation satisfying (3), then for any E ∈|ES_{L} | and f : P → E,

β_{E} ∘ R^{ES}(f) = F (f) ∘ α_{P} .  (4)

In fact

β_{E} ∘ R^{ES}(f) = F (f) ∘ β_{i_{L}(P)} (by naturality of β)
= F (f) ∘ α_{P}  (by equation (3)).

But since, for any E ∈|ES_{L} |, (2) holds, there exists a unique β_{E} : R^{ES}(E) → F (E) satisfying β_{E} ∘ R^{ES}(f) = F (f) ∘ α_{P} . Commutativity of the naturality squares follows as well from the universal property of colimits. We need to prove that for any g : E → E′ in ES_{L}, the following diagram commutes:

\xymatrix{R^{ES}(E) \ar[r]^{β_{E}} \ar[d]_{R^{ES}(g)} & F (E) \ar[d]^{F (g)} \\ R^{ES}(E′) \ar[r]_{β_{E′}} & F (E′) .}

It is enough to show that for any f : P → E, F (g) ∘ β_{E} ∘ R^{ES}(f) = β_{E′} ∘ R^{ES}(g) ∘ R^{ES}(f). This follows by the following calculation:

F (g) ∘ β_{E} ∘ R^{ES}(f) = F (g) ∘ F (f) ∘ α_{P}  (by equation (4))
= F (gf) ∘ α_{P}  (by functoriality of F)
= β_{E′} ∘ R^{ES}(gf)  (by equation (4))
= β_{E′} ∘ R^{ES}(g) ∘ R^{ES}(f) (by functoriality of R^{ES})
□

We then have a functor R : Pom_{L} → Pom_{M} that can be extended as follows:

\xymatrix{Pom_{L} \ar[rr]^{i_{L}} \ar[dr]_{R} &  & ES_{L} \ar[r]^{c_{L}} \ar[dd]^{R^{ES}=Lan_{i_{L}}(i_{M} R)} & \begin{matrix} \\ Pom & L \end{matrix} \ar[dd]^{Lan_{y_{_{Pom}_{L}}} (y_{Pom_{M}} R)=R_{!}} \\  & _{Pom_{M}} \ar[dr]_{i_{M}} \\  &  & _{ES_{M}} \ar[r]_{c_{M}} & \begin{matrix} \\ Pom & M \end{matrix} .}

We want to show that the square on the right commutes up to a natural isomorphism. We show first of all that

c_{M}R^{ES} ≅ Lan_{i_{L}}(c_{M}i_{M}R) = Lan_{i_{L}}(y_{Pom_{M}} R) .

From this in fact it will follow that (using that left Kan extensions compose, cf. Section 1.4),

Lan_{y_{Pom_{L}}}(y_{Pom_{M}} R) ≅ Lan_{c_{L}}(Lan_{i_{L}}(y_{Pom_{M}} R)
≅ Lan_{c_{L}}(c_{M}R^{ES}) .

Hence, since c_{L} is full and faithful (cf. Proposition 15)

Lan_{y_{Pom_{L}}}(y_{Pom_{M}} R)c_{L} ≅ Lan_{c_{L}}(c_{M}R^{ES})c_{L} ≅ c_{M}R^{ES} .

To prove that c_{M}R^{ES} ≅ Lan_{i_{L}}(c_{M}i_{M}R), we apply Proposition 11.

Proposition 76 There is a natural isomorphism

c_{M}R^{ES} ≅ Lan_{i_{L}}(c_{M}i_{M}R) .

Proof: The proof is an immediate consequence of Proposition 11 and of Lemma 74. In fact, as we saw in the proof of Proposition 75, Lan_{i_{L}}(i_{M}R) can be expressed as the colimit (2) and Lemma 74 ensures that the conditions of Proposition 11 are met. □

Now we can use Theorem 17 to deduce that R_{!} preserves open map bisimulation.

Proposition 77 For any refinement function r : L →| Pom_{M} |, the associated refinement functor R_{!} : \begin{matrix} \\ Pom & L \end{matrix} → \begin{matrix} \\ Pom & M \end{matrix} preserves open map bisimulation; if X and Y are two Pom_{L}-open bisimilar presheaves, then R_{!}(X) and R_{!}(Y) are Pom_{M}-open bisimilar.

As a consequence, using Proposition 12, we have:

Corollary 78 For any refinement function r : L →| Pom_{M} |, the associated refinement functor R^{ES} : ES_{L} → ES_{M} preserves hereditary history-preserving bisimulation; If E and E′ are two hereditary history-preserving bisimilar event structures in ES_{L} , then R^{ES}(E) and R^{ES}(E′) are hereditary history-preserving bisimilar.

Proof:

E hhpb E′ ⟹ c_{L}(E) Pom_{L}-open bisimilar to c_{L}(E′)
⟹ R_{!}c_{L}(E) Pom_{M}-open bisimilar to R_{!}c_{L}(E′)
⟺ c_{M}R^{ES}(E) Pom_{M}-open bisimilar to c_{M}R^{ES}(E′)
⟺ R^{ES}(E) hhpb R^{ES}(E′) .
□

Acknowledgements Thanks are due to Gordon Plotkin who suggested improvements.

References

[1] M. Bednarczyk. Hereditary history preserving bisimulation or what is the power of the future perfect in program logics. Technical report, Polish Academy of Sciences, Gdansk, 1991.

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

[3] G. L. Cattani. Presheaf Models for Concurrency. PhD thesis, University of Aarhus, 1999.

[4] G. L. Cattani, M. P. Fiore, and G. Winskel. A theory of recursive domains with applications to concurrency. In LICS ’98, Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science, pages 214–225. IEEE Computer Society Press, 1998.

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

[6] G. L. Cattani and G. Winskel. Presheaf models for concurrency. In D. van Dalen and M. Bezem, editors, Computer Science Logic. 10th International Workshop, CSL ’96, Annual Conference of the European Association for Computer Science Logic. Selected Papers, volume 1258 of Lecture Notes in Computer Science, pages 58–75. Springer-Verlag, 1997.

[7] G. L. Cattani and G. Winskel. Profunctors, open maps and bisimulation. Manuscript in preparation, 1999.

[8] A. Cheng and M. Nielsen. Open maps, behavioural equivalences, and congruences. Theoretical Computer Science, 190(1):87–112, 1998.

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

[10] M. P. Fiore, G. L. Cattani, and G. Winskel. Weak bisimulation and open maps (extended abstract). In LICS ’99, Proceedings of the Fourteenth Annual IEEE Symposium on Logic in Computer Science, pages 67–76. IEEE Computer Society Press, 1999.

[11] M. P. Fiore, G. D. Plotkin, and A. J. Power. Complete cuboidal sets in axiomatic domain theory. In LICS ’97, Proceedings of the Twelfth Annual IEEE Symposium on Logic in Computer Science, pages 268–279. IEEE Computer Society Press, 1997.

[12] R. van Glabbeek and U. Goltz. Equivalence notions for concurrent systems and refinement of actions. In Mathematical Foundations of Computer Science 1989, number 379 in Lecture Notes in Computer Science, pages 237–248. Springer-Verlag, 1989.

[13] A. Grothendieck. Revêtements étales et groupe fondamental, volume 224 of Lecture Notes in Mathematics. Springer-Verlag, Berlin, 1971. Séminaire de Géométrie Algébrique du Bois Marie 1960–1961 (SGA 1), Dirigé par Alexandre Grothendieck. Augmenté de deux exposés de M. Raynaud.

[14] C. Hermida. Fibrations Logical Predicates and Indeterminates. PhD thesis, University of Edinburgh, 1993. Available as Technical Report DAIMI-PB 462, Computer Science Department, University of Aarhus.

[15] T. T. Hildebrandt. A fully abstract presheaf semantics for SCCS with finite delay. In Proceedings of the 8th International Conference on Category Theory and Computer Science, CTCS ’99, ENTCS. Elsevier, 1999. To appear.

[16] T. T. Hildebrandt, P. Panangaden, and G. Winskel. A relational model of nondeterministic dataflow. In D. Sangiorgi and R. de Simone, editors, Proceedings of the 9th International Conference on Concurrency Theory, CONCUR ’98, volume 1466 of Lecture Notes in Computer Science, pages 613–628. Springer-Verlag, 1998.

[17] B. Jacobs. Categorical Logic and Type Theory. Number 141 in Studies in Logic and the Foundations of Mathematics. North Holland, Amsterdam, 1999.

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

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

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

[21] S. Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer-Verlag, 1971.

[22] S. Mac Lane and I. Moerdijk. Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer-Verlag, 1992.

[23] M. Nielsen and G. Winskel. Petri nets and bisimulation. Theoretical Computer Science, 153:211–244, 1996.

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

[25] V. Pratt. Modelling concurrency with partial orders. International Journal of Parallel Processing, 15:33–71, 1986.

[26] A. Rabinovitch and B. Traktenbrot. Behaviour structures and nets. Fundamenta Informatica, 11(4):357–404, 1988.

[27] G. Winskel. A category of labelled petri nets and compositional proof system. In LICS ’88, Proceedings of the Third Annual IEEE Symposium on Logic in Computer Science, pages 142–154. IEEE Computer Society Press, 1988.

[28] G. Winskel. A presheaf semantics of value-passing processes (extended abstract). In U. Montanari and V. Sassone, editors, CONCUR’96, Proceedings of the 7th International Conference on Concurrency Theory, volume 1119 of Lecture Notes in Computer Science, pages 98–114. Springer-Verlag, 1996.

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

[30] O. Wyler. Lecture notes on topoi and quasitopoi. World Scientific Publishing Co. Inc., Teaneck, NJ, 1991.