BRICS RS-99-7 G. Winskel: Event Structures as Presheaves—Two Representation Theorems BRICS

Basic Research in Computer Science

Event Structures as Presheaves —Two Representation Theorems

Glynn Winskel BRICS Report Series RS-99-7 ISSN 0909-0878 March 1999 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1999, Glynn Winskel.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

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

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

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

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

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

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

This document in subdirectory RS/99/7/

Event Structures as Presheaves —Two Representation Theorems

Glynn Winskel

BRICS^{⋆}, University of Aarhus, Denmark

Abstract. The category of event structures is known to embed fully and faithfully in the category of presheaves over pomsets. Here a characterisation of the presheaves represented by event structures is presented. The proof goes via a characterisation of the presheaves represented by event structures when the morphisms on event structures are “strict” in that they preserve the partial order of causal dependency.

1 Introduction

Presheaves have been advanced as a model of nondeterministic processes which supports a notion of bisimulation and as well extends to higher order [7, 12, 5, 4, 3, 10, 13, 6, 2]. At the start of this work, the paper [7] showed that the category of (labelled) event structures embedded fully and faithfully in the category of presheaves over pomsets; the embedding arises canonically from the fact that pomsets can be regarded as event structures. The paper [7] gave several grounds for viewing the presheaf category as consisting of generalised event structures.

Clearly some presheaves were not obtained from event structures, among them those presheaves which were not “rooted” in the sense of not having a unique starting state. The empty presheaf is not rooted. It allows no computation, not even the empty pomset. At the other extreme, the terminal presheaf, which assigns a singleton set to each pomset, supports all computational behaviour (like the “chaos” of CSP); although rooted it cannot correspond to an event structure, seen most quickly by noticing that all morphisms from pomsets to event structures are mono a state of affairs not reflected in the presheaf category for the terminal object. Other presheaves not corresponding to event structures could be nevertheless understood within broader classes of models such as certain categories of Petri nets. But the precise boundary was unclear; there remained the question of precisely which presheaves over pomsets arose from event structures.

This paper uncovers the conditions that characterise those presheaves represented by event structures (Theorem 17). The proof involves first showing an analogous result for a stricter class of morphisms on event structures (Theorem 9). A condition central to both theorems is one equivalent to saying that the presheaves should be separated with respect to a simple Grothendieck topology.

⋆ Basic Research in CS, Centre of the Danish National Research Foundation.

2 Event Structures and Pomsets

We will work with labelled event structures, and throughout this paper we assume a fixed set of labels L.

A (labelled) event structure [11] is a structure (E, ≤, Con, l) consisting of a set E, of events which are partially ordered by ≤, the causal dependency relation, a nonempty consistency relation Con consisting 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. Events e, e′ ∈ E are concurrent (causally independent) iff (e ≰ e′ & e′ ≰ e & {e, e′} ∈ Con). A configuration of E is a subset x ⊆ E which is

– downwards-closed: ∀e, e′. e′ ≤ e ∈ x ⇒ e′ ∈ x, and

– consistent: ∀X. X finite & X ⊆ x ⇒ X ∈ Con. An event e determines a prime configuration [e] = {e_{1} ∈ E | e_{1} ≤ e} consisting of all its causal predecessors and the event itself.

We restrict attention to label-preserving morphisms on event structures over the common labelling set L (the fibres of [11]). Let E = (E, ≤, Con, l), E′ = (E′, ≤′, Con′, l′) be event structures over L. A morphism from E to E′ consists of a function f : E → E′ on events which preserves labels (i.e. l = l′ ∘ f) such that if x is a configuration of E, then its image fx is a configuration of E′ and if for e_{1}, e_{2} ∈ x their images are equal, i.e. f(e_{1}) = f(e_{2}), then e_{1} = e_{2}. We can equivalently describe a morphism of event structures from E to E′ as a function f : E → E′ such that

\begin{matrix}∀e ∈ E. [f(e)] ⊆ f[e] & \\ ∀X ∈ Con. [fX ∈ Con′ & (∀e_{1}, e_{2} ∈ X. f(e_{1}) = f(e_{2}) ⇒ e_{1} = e_{2})]. \end{matrix}

We say a morphism f : E → E′ of event structures is strict iff [f(e)] = f[e].

It is easy to check that the function composition of two morphisms of event structures is a morphism so that we obtain a category.

Definition 1. We write E for the associated category of event structures, writing E_{s} for the subcategory with strict morphisms.

In event structures a configuration, to be thought of as a computation path, carries more structure than simply a string of actions. A configuration inherits the shape of a pomset from the causal dependency and labelling of the event structure. Pomsets [9] are partial orders of labelled events and so can be identified with special event structures where all finite subsets of events are consistent.

Definition 2. Say a pomset is prime when it has a top event e with respect to the causal dependency relation ≤—so its set of events is [e].

Morphisms from pomsets to event structures are 1-1 functions which send downwards-closed sets to downwards-closed sets. Thus a morphism from pomset P to pomset Q may not only extend P by extra events but also relax the causal dependency relation; two events causally related in P may have images no longer causally related in Q—of course this cannot occur for a strict morphism which would force P to be a pomset prefix of Q.

We separate the forms of morphism corresponding to the different ways one pomset can extend another.

Definition 3. Define Pom to be the full subcategory of event structures E with objects finite pomsets. Define Pom_{s} to be the subcategory of Pom where all morphisms are strict morphisms.

An epimorphism in Pom is called an augmentation (following [9], though note the switch of direction relative to loc. cit.).

It is clear that all isomorphisms in Pom are augmentations (and strict) and that restricting to augmentation morphisms also yields a subcategory of Pom.

Proposition 4. In Pom, any morphism f : P → Q factors uniquely to within isomorphism as a composition f = P ^{\underline{a}}→ Q_{0} ^{\underline{j}}→ Q where a is an augmentation and j is a strict morphism.

Such augment-strict factorisations play a central role in the proof of the second representation theorem.

3 Presheaf models

Here a presheaf over an (essentially small) category ℙ is thought of as standing for a nondeterministic process whose computation paths have the shape of objects of ℙ; according to this view the morphisms of ℙ express how one path shape extends to another. In this paper ℙ will be either Pom or Pom_{s}.

The objects (presheaves) of ℙ̂ consist of functors ℙ^{op} → Set, to the category of sets. The morphisms of ℙ̂ are natural transformations between functors. A presheaf X : ℙ^{op} → Set can be thought of as specifying for a typical object P the set X(P) of computation paths of shape P. It acts on a morphism j : P → Q in ℙ to give a function X(j) : F (Q) → F (P) saying how Q-paths restrict to P - paths. Notation: Let X be a presheaf over a category ℙ. Let j : P → Q be a morphism in ℙ. As is usual, we will frequently write y · j for X(j)(y), the restriction of y ∈ X(Q) along j : P → Q, a morphism in ℙ. Note that the functoriality of X ensures that (y · k) · j, which we will most often write as y · k · j, equals y · (k ∘ j), when j : P → Q, k : Q → R and y ∈ X(R).

Definition 5. Let X be a presheaf over ℙ. Define its category of elements els(X) to be the category consisting of: objects (P, x) where P is an object of ℙ and x ∈ X(P); morphisms j : (P, x) → (Q, y) whenever j : P → Q in ℙ and x = y · j.

The Yoneda embedding Y : ℙ → ℙ̂ expresses how to regard a path P as the presheaf ℙ[−, P], such presheaves being called representables. The category of presheaves ℙ̂ is the free colimit completion of ℙ: for any functor F : ℙ → E where E has all small colimits, there is a functor Lan_{Y}(F) : ℙ̂ → E, unique to within isomorphism, such that

\xymatrix{ℙ \ar[r]^{Y} \ar[dr]_{F} & ℙ̂ \ar[d]^{Lan_{Y} (F)} \\  & E}

commutes. In particular, as presheaf categories have all small colimits we can instantiate E to a presheaf category ℚ̂. The functor Lan_{Y}(F) (a left Kan extension) can be described explicitly (see e.g. [8]) as that functor such that

Lan_{Y}(F)(X) = colim_{(P,x)∈els(X)}F (P)

for any X ∈ ℙ̂; its action on morphisms is determined by the universal property of colimits.

Colimits in Set: Colimits of presheaves are given pointwise in terms of colimits in Set for which we can make use of an explicit construction of colimits (see e.g. [1]):

Proposition 6. Let 𝕀 be a small category. Let D : 𝕀 → Set be a functor (called a diagram of shape 𝕀 in Set). Then, D has a colimit in Set given explicitly as the cone consisting of the set C and functions γ_{i} : D(i) → C, for i ∈ 𝕀, described as follows. The set C is the set of equivalence classes

C = ⨄_{i∈I} D(i) / ∼

where ∼ is the least equivalence relation on the set ⨄_{i∈I} D(i) for which

(i, x) ∼ (j, y) if D(f)(x) = y , for some f : i → j in 𝕀 .

The function γ_{i} : D(i) → C, where i ∈ 𝕀, takes x ∈ D(i) to the equivalence class {(i, x)}_{∼}.

As colimits are unique to within isomorphism, we can and shall assume that all the colimits in Set we consider are given explicitly as in Proposition 6.

4 The Problem

There is a canonical functor c from the category of event structures E to the category of presheaves { \atop Pom}. The functor c takes an event structure E of E to the presheaf E[−, E]; in detail, c(E) is the presheaf which for each path object P yields the set of paths E[P, E] from P into E. The functor c takes a morphism f : E → E′ in E to the natural transformation E[−, f] : E[−, E] → E[−, E′] whose component at an object P of Pom is the function E[P, E] → E[P, E′] taking p to f ∘ p—intuitively, a path p : P → E in E is taken to a path f ∘ p : P → E′ in E′.

Because the inclusion functor Pom ↪ E is dense,

Theorem 7. [7] The canonical functor c : E → { \atop Pom} is full and faithful.

The canonical functor c_{s} : E_{s} → \begin{matrix} \\ Pom & s \end{matrix} is defined analogously, but with respect to strict morphisms on event structures and pomsets, and analogously:

Theorem 8. The canonical functor from c_{s} : E_{s} → \begin{matrix} \\ Pom & s \end{matrix} is full and faithful.

The problem addressed in this paper is the characterisation of those presheaves which correspond to event structures with respect to the canonical embeddings. These amount to representation theorems; a presheaf X over Pom is said to be represented by an event structure E in E iff X ≅ E[−, E]. It turns out that characterising the presheaves in { \atop Pom} which are represented by event structures in E involves first characterising those presheaves in \begin{matrix} \\ Pom & s \end{matrix} represented by event structures in E_{s}, the strict case.

5 Representation Theorem—Strict Morphisms

This section is devoted to showing our first representation theorem:

Theorem 9. A presheaf X ∈ \begin{matrix} \\ Pom & s \end{matrix} is isomorphic to E_{s}[−, E] for some event structure E iff X is nonempty and satisfies the conditions

(Mono) For all j_{1}, j_{2} : P → Q in Pom_{s}, where P is prime,

∀x ∈ X(Q). x · j_{1} = x · j_{2} ⇒ j_{1} = j_{2}.

(Separated) For all x, x′ ∈ X(Q) where Q is a pomset,

if (∀j : P → Q in Pom_{s} with P prime, x · j = x′ · j) then x = x′.

Remark 10. The empty presheaf assigns the emptyset to each pomset, even the empty pomset, and so cannot be represented by any event structure which will always have the empty configuration. As we will see the condition “Mono” expresses that morphisms from pomsets into event structures are mono. In fact “Mono” is equivalent to the corresponding condition where P is not restricted to be prime. The condition “Separated” is equivalent to saying that the presheaf X is separated with respect to the Grothendieck topology (see e.g. [8]) with basis consisting of collections {k_{i} : P_{i} → Q | i ∈ I} of jointly surjective morphisms. Note that “Separated” implies that any nonempty presheaf X is rooted in the sense that X(∅), the set assigned to the empty pomset ∅, is a singleton; because there are no prime pomsets mapping into the empty pomset.

It is easy to show the “only if” half of the theorem.

Lemma 11. Let E be an event structure in E_{s}. Let X be the presheaf E_{s}[−, E]. Then X is nonempty and satisfies the conditions “Mono” and “Separated”.

Proof. “Mono”: Let x ∈ E_{s}[Q, E] and j_{1}, j_{2} : P → Q morphisms in Pom_{s}. For the presheaf E_{s}[−, E] obtained via the hom-functor, x · j_{1} = x · j_{2} means x ∘ j_{1} = x ∘ j_{2}, so j_{1} = j_{2} as x is 1-1 and thus mono. “Separated”: Suppose x, x′ ∈ E_{s}[Q, E] have the property that x · j = x′ · j for all j : P → Q in Pom_{s}, from a prime pomset P. But this implies x ∘ j = x′ ∘ j for all inclusions j : [e] ↪ Q where e is an event of Q. Hence, x and x′ agree on all events of Q and so are equal. □

To show the converse, “if” direction, of Theorem 9 we construct an event structure from a nonempty presheaf satisfying the “Mono” and “Separated” conditions. We do this by forming a colimit in E_{s}. Not all colimits exist in E_{s}. However if a nonempty presheaf X satisfies the “Mono” condition we can construct a colimit as follows.

Lemma 12. Let X be a nonempty presheaf over Pom_{s} which satisfies the “Mono” condition. Then the colimit colim_{(Q,x)∈els(X)}Q exists in E_{s}. Its events E can be taken to be the colimit in Set

⨄_{(Q,x)∈els(X)} Q / ∼

where ∼ is the least equivalence relation such that

((Q, x), q) ∼ ((Q′, x′), q′) if ∃k : Q → Q′ in Pom_{s}. x = x′.k & k(q) = q′ ,

when the components of the colimiting cone in E_{s}, at (Q, x) ∈ els(X), are given by maps

γ_{Q,x} : Q → E with q ↦ {(Q, x), q)}_{∼} .

The causal dependency and consistency relations on E satisfy:

– e ≤ e′ iff there are q ≤ q′ in Q for some pomset Q and x ∈ X(Q) such that γ_{Q,x}(q) = e and γ_{Q,x}(q′) = e′,

– C ∈ Con iff there is S ⊆ Q for some pomset Q and x ∈ X(Q) such that C = γ_{Q,x}S.

Proof. Write ((Q, x), q) ∼_{1} ((Q′, x′), q′) iff ∃k : Q → Q′. x = x′ · k & k(q) = q′. By definition, the relation ∼ is the symmetric transitive closure of ∼_{1}.

Suppose that ((Q, x), q) ∼_{1} ((Q′, x′), q′) and that i : [q] ↪ Q and i′ : [q′] ↪ Q′ are the associated inclusion morphisms in Pom_{s}. Then “restricting” along i and i′ we obtain

((Q, x), q) ∼_{1} ((Q′, x′), q′)
∼_{1}  ∼_{1}
(([q], x · i), q) ∼_{1} (([q′], x′ · i′), q′) .

Recalling that morphisms are strict we see that for x ∈ X(Q), x′ ∈ X(Q′),

(([q], x · i), q) ∼_{1} (([q′], x′ · i′), q′) iff ∃k : [q] ≅ [q′]. x · i = x′ · i′ · k .

Thus a ∼_{1}-chain establishing ((Q, x), q) ∼ ((Q′, x′), q′) restricts to a ∼_{1}-chain involving only prime pomsets. Noting that the ∼_{1} relation is already symmetric and transitive when only prime pomsets are involved, we obtain

\begin{aligned}((Q, x), q) ∼ ((Q′, x′), q′) & iff (([q], x · i), q) ∼_{1} (([q′], x′ · i′), q′) \\ & iff ∃k : [q] ≅ [q′]. x · i = x′ · i′ · k \end{aligned}

where i : [q] ↪ Q and i′ : [q′] ↪ Q′ are the inclusion morphisms.

It follows that each γ_{Q,x} : Q → E is 1-1. Suppose q, q′ ∈ Q and ((Q, x), q) ∼ ((Q, x), q′). Then we obtain

k : [q] ≅ [q′] & x · i = x′ · i′ · k

where i : [q] ↪ Q and i′ : [q′] ↪ Q′. But X is assumed to satisfy the “Mono” condition. Hence i = i′ ∘ k so that q = i(q) = i′ ∘ k(q) = i′(q′) = q′, making γ_{Q,x} a 1-1 function.

As ∼_{1} respects causal predecessors [−], defining the causal dependency and consistency relations as above yields an event structure and ensures that each γ_{Q,x} is a morphism in E_{s}. Together γ_{Q,x}, where (Q, x) ∈ els(X), form a cone in E_{s}, which is colimiting because it is so in Set. □

Prime pomsets distribute through the colimits of Lemma 12:

Lemma 13. Let X be a nonempty presheaf over Pom_{s} satisfying the “Mono” condition. Let P be a prime pomset. The canonical map from the colimiting cone,

φ_{P} : colim_{(Q,x)∈els(X)}E_{s}[P, Q] → E_{s}[P, colim_{(Q,x)∈els(X)}Q] ,

acting so

φ_{P} : {((Q, x), j)}_{∼} ↦ γ_{Q,x} ∘ j ,

is an isomorphism, where γ_{Q,x} where (Q, x) ∈ els(X), is the colimiting cone to colim_{(Q,x)∈els(X)}Q.

Proof. Write E for the event structure obtained as the colimit colim_{(Q,x)∈els(X)}Q in Lemma 12. We first check that φ_{P} is well-defined. In the explicit presentation of the colimit C = colim_{(Q,x)∈els(X)}E_{s}[P, Q] in Set the equivalence relation ∼ is generated by ∼_{1} where

((Q, x), j) ∼_{1} ((Q′, x′), j′) iff ∃k : Q → Q′ in Pom_{s}. x = x′ · k & k ∘ j = j′.

Thus, if ((Q, x), j) ∼_{1} ((Q′, x′), j′), then there is k : (Q, x) → (Q′, x′) in els(X). So, as E, γ is a cone, we directly obtain γ_{Q,x} = γ_{Q′,x′} ∘ k. Thus

φ_{P} (((Q, x), j)) = γ_{Q,x} ∘ j = γ_{Q′,x′} ∘ k ∘ j = γ_{Q′,x′} ∘ j′ = φ_{P} (((Q′, x′), j′)) .

Hence φ_{P} is well-defined as a function. We require in addition that φ_{P} is 1-1 and onto. “onto”: Suppose f : P → E in E_{s}. As a prime pomset, P is [p] for some event p. The image f(p), in E, is an equivalence class {((Q, x), q)}_{∼}, choosing any representative ((Q, x), q), where (Q, x) ∈ els(X) and q ∈ Q. Because morphisms are strict [p] ≅ [q], so f must factor through γ_{Q,x} for some j : P → Q in Pom_{s}:

\xymatrix{P \ar[r]^{f} \ar[d]_{j} & E \\ Q \ar[ur]_{γ_{Q,x}}}

But now φ_{P} ({((Q, x), j)}_{∼}) = γ_{Q,x} ∘ j = f. “1-1”: Again, as P is prime it has the form [p] for some p ∈ P. First note that any equivalence class c ∈ colim_{(Q,x)∈els(x)}E_{s}[P, Q] has a representative of the form (([q], x), j), j) where j : [p] ≅ [q]. To see this note that for any representative ((Q, y), l),

((Q, y), l) ∼_{1} (([q], y · i), l_{0})

where q = l(p) and l factors as [p] ≅^{l_{0}} [q] ↪^{i} Q.

Thus assuming that φ_{P} (c) = φ_{P} (c′) for c, c′ ∈ colim_{(Q,x)∈els(X)}E_{s}[P, Q], there are representatives (([q], x), j) and (([q′], x′), j′) where j : [p] ≅ [q] and j′ : [p] ≅ q′] for which

γ_{[q],x} ∘ j = γ_{[q′],x′} ∘ j′.  (1)

Consequently, γ_{[q],x}(q) = γ_{[q′],x′}(q′), from which we obtain ((([q], x), q) ∼ (([q′], x′), q′) in E. But now (just as in the proof of Lemma 12) we derive the existence of an isomorphism k such that

k : [q] ≅ [q′] & x = x′ · k .  (2)

As k : ([q], x) ≅ ([q′], x′) is a morphism in els(X) and E, γ is a cone, we see that

γ_{[q],x} = γ_{[q′],x′} ∘ k .

Hence, by (1),

γ_{[q′],x′} ∘ j′ = γ_{[q],x} ∘ j = γ_{[q′],x′} ∘ k ∘ j ,

ensuring j′ = k∘j from the injectivity of γ_{[q′],x′}. With (2), this yields (([q], x), j) ∼_{1} (([q′], x′), j′) in C, making c = c′. Hence φ_{P} is 1-1. □

It is well-known that a presheaf is the colimit of its representables and that colimits in categories of presheaves are obtained pointwise [8]. With our explicit treatment of colimits in Set we obtain an explicit isomorphism:

Lemma 14. Let X be a presheaf over Pom_{s}. Let P ∈ Pom_{s}. Then

ψ_{P} : X(P) ≅ colim_{(Q,x)∈els(X)}Pom_{s}[P, Q] ,

where ψ_{P} (z) = {((P, z), 1_{P})}_{∼}.

Now we can prove the “if” half of the first representation theorem:

Lemma 15. Suppose X, a nonempty presheaf over Pom_{s}, satisfies the “Mono” and “Separated” conditions. Let E be the event structure obtained as the colimit colim_{(Q,x)∈els(X)}Q in E_{s} (cf. Lemma 12). Then, there is a natural isomorphism

θ : X ≅ E_{s}[−, E]

which has components θ_{Q} : X(Q) → E_{s}[Q, E], at pomset Q, given by

θ(x) = γ_{Q,x}

for x ∈ X(Q). [We adopt the notation of Lemma 12 where γ_{Q,x} : Q → E is the component of the colimiting cone at (Q, x) ∈ els(X).]

Proof. We first check that θ is a natural transformation. Suppose j : Q → Q′ in Pom_{s}. We require the following naturality square to commute:

\xymatrix{X(Q) \ar[r]^{θ_{Q}} & E_{s}[Q, E] \\ X(Q′) \ar[u]^{X(j)} \ar[r]^{θ_{Q′}} & E_{s}[Q′, E] . \ar[u]_{−∘j}}

I.e., letting x′ ∈ X(Q′), we require γ_{Q,x′·j} = (γ_{Q′,x′}) ∘ j. But this is a direct consequence of E, γ forming a cone.

For θ to be a natural isomorphism we need that each θ_{Q}, at a pomset Q, is 1-1 and onto: “onto”: Supposing f : Q → E the image of Q must be consistent in E. Hence, by the way the consistency relation is defined on E in Lemma 12, the map f must factor as

\xymatrix{Q \ar[r]^{f} \ar[d]_{j} & E \\ Q_{0} \ar[ur]_{γ_{Q_{0},x_{0}}}}

for some (Q_{0}, x_{0}) ∈ els(X). Take x = x_{0} · j ∈ X(Q). Then, f = γ_{Q_{0},x_{0}} ∘ j = γ_{Q,x} because E, γ is a cone and (Q, x) ^{\underline{j}}→ (Q_{0}, x_{0}) in els(X). Hence θ_{Q}(x) = f. “1-1”: Suppose θ_{Q}(x) = θ_{Q}(x′) for x, x′ ∈ X(Q). Then, for any j : P → Q with P prime, θ_{P} (x · j) = θ_{P} (x′ · j) by naturality. Thus because X is “Separated”, it is sufficient to show that θ_{P} is 1-1 for each prime pomset P. However, each component θ_{P}, when P is a prime pomset, arises as the composition of isomorphisms

X(P) ≅^{ψ_{P}} colim_{(Q,x)∈els(X)}Pom_{s}[P, Q]  cf. Lemma 14,
= colim_{(Q,x)∈els(X)}E_{s}[P, Q] as Pom_{s} ↪ E_{s} is full,
≅^{φ_{P}} E_{s}[P, E] cf. Lemma 13.
□

As a corollary of Lemmas 11 and 15 we obtain the first representation theorem (Theorem 9) whose statement heads this section.

6 Representation Theorem—Nonstrict Morphisms

Our aim now is to characterise those presheaves over Pom represented by event structures in E. Notation: We make heavy use of the augment-strict factorisation of Proposition 4 and it is helpful to adopt the convention that arrows ↠ stand for augmentations while ↣ stand for strict morphisms. The statement of the second representation theorem involves a “confluence” condition on the category of elements of a presheaf.

Confluence Conditions: We will be interested in presheaves Y ∈ { \atop Pom} for which the category of elements els(Y) satisfies the confluence condition:

Letting a : P ↠ Q and f : P → R, in els(Y),

if \xymatrix{(R, z) \\ (P, x) \ar[u]^{f} \ar@{->>}[r]_{a} & (Q, y)} then \xymatrix{(R, z) \ar@{->>}[r]^{a′} & (S, w) \\ (P, x) \ar[u]^{f} \ar@{->>}[r]_{a} & (Q, y) \ar[u]_{f′}} commutes,

for some (S, w) in els(Y) with a′ : R ↠ S and f′ : Q → S.

We can summarise the confluence condition in the diagram:

\xymatrix{· \ar@{->>}[r]^{a′} & · \\ · \ar[u]^{f} \ar@{->>}[r]_{a} & · \ar@{-->}[u]_{f′}}

Remark 16. By specialising f in the confluence condition to an augmentation we obtain a condition which we likewise summarise as the confluence diagram:

\xymatrix{· \ar@{->>}[r]^{a′} & · \\ · \ar@{->>}[u]^{f} \ar@{->>}[r]_{a} & · \ar@{->>}[u]_{f′}}

Note that in this case the morphism f′ will also be an augmentation just because it is a second factor of an epimorphism.

The remainder of the paper is devoted to showing the second representation theorem:

Theorem 17. A presheaf Y ∈ { \atop Pom} is isomorphic to E[−, E] for some event structure E iff Y is nonempty and satisfies the conditions

(Mono) For all j_{1}, j_{2} : P → Q in Pom, where P is prime,

∀y ∈ Y (Q). y · j_{1} = y · j_{2} ⇒ j_{1} = j_{2}.

(Separated) For all y, y′ ∈ Y (Q) where Q is a pomset,

if (∀j : P → Q in Pom, with P prime, y · j = y′ · j) then y = y′. (Confluent) The confluence condition above holds of els(Y).

The proof of Theorem 17 uses the first representation theorem (Theorem 9) characterising which presheaves in \begin{matrix} \\ Pom & s \end{matrix} are represented by event structures E in E_{s}. The proof has three main parts Sections 6.1, 6.2 and 6.3.

In Section 6.1 the extension of the obvious inclusion functor Pom_{s} ↪ Pom to a colimit-preserving functor L : \begin{matrix} \\ Pom & s \end{matrix} → { \atop Pom} is characterised (Lemma 18).

The next stage, presented in Section 6.2, is to relate the two canonical embeddings c_{s} : E_{s} → \begin{matrix} \\ Pom & s \end{matrix} and c : E → { \atop Pom} in the diagram

\xymatrix{E_{s} \ar@{^{(}->}[r] \ar[d]_{c_{s}} & E \ar[d]^{c} \\ \begin{matrix} \\ Pom & s \end{matrix} \ar[r]^{L} & { \atop Pom}}

which is shown to commute up to isomorphism (Lemma 20). It follows that the presheaves in { \atop Pom} represented by event structures in E are, to within isomorphism, the images under L of those presheaves in \begin{matrix} \\ Pom & s \end{matrix} represented by event structures in E_{s}.

Finally, in Section 6.3, it is shown that, to within isomorphism, the images in { \atop Pom} under L of presheaves in \begin{matrix} \\ Pom & s \end{matrix} are those which satisfy the “Confluent” condition, and that the “Mono” and “Separated” conditions transfer via L to the corresponding conditions in { \atop Pom} (Lemma 21). This yields the second representation theorem (Theorem 17).

6.1 The Functor L

To within isomorphism, there is a colimit-preserving function L : \begin{matrix} \\ Pom & s \end{matrix} → { \atop Pom} such that

\xymatrix{Pom_{s} \ar@{^{(}->}[r]^{I} \ar[d]_{Y_{s}} & Pom \ar[d]^{Y} \\ \begin{matrix} \\ Pom & s \end{matrix} \ar[r]^{L} & { \atop Pom}}

commutes to within isomorphism. The functor L may be obtained as the left-

Kan extension, so Lan_{Y_{s}}(Y ∘ I)(X) = colim_{(P,x)∈els(X)}Y(P) for X ∈ \begin{matrix} \\ Pom & s \end{matrix}.

By exploiting the augment-strict factorisation (Proposition 4) we give a more workable characterisation.

Lemma 18. Let X ∈ \begin{matrix} \\ Pom & s \end{matrix}, Q ∈ Pom. Define

L(X)(Q) = {{(P, x, a)}_{≃} | x ∈ X(P) & a : Q ↠ P)}

where (P, x, a) ≃ (P′, x′, a′) iff ∃k : P ≅ P. x = x′ · k & k ∘ a = a′. For f : Q → Q′, define L(X)(f) : L(X)(Q′) → (LX)(Q) to act so

{(P′, x′, a′)}_{≃} ↦ {(P, x′ · i, a)}_{≃}

where i : P ↣ P′ and a : Q ↠ P are an augment-strict factorisation i∘a = a′∘f:

[figure: Q′; a′; P′; Q; f; a; P; i]

Then, L(X) is a presheaf over Pom such that L(X) ≅ Lan_{Y_{S}}(Y ∘ I)(X).

Proof. As colimits of presheaves are obtained pointwise, from the explicit description of colimits in Set, Proposition 6, we see

Lan_{Y_{s}}(Y∘I)(X)(Q) = colim_{(P,x)∈els(X)}Pom_{s}[Q, P] = ⨄_{(P,x)∈els(X)} Pom[Q, P]/∼

where ∼ is the least equivalence relation such that

((P, x), f) ∼ ((P′, x′), f′) iff ∃k : P ↣ P′. x = x′ · k & k ∘ f = f′ .

It follows that for each ((P′, x′), f′) ∈ ⨄_{(P,x)∈els(X)} Pom[Q, P]

((P, x′ · i), a) ∼ ((P′, x′), f′)

where an augment-strict factorisation of f is:

[figure: P′; Q; f′; a; P; i]

The isomorphism L(X)(Q) ≅ Lan_{Y_{s}}(Y ∘ I)(X)(Q) is a direct consequence.

Via the isomorphism we obtain a colimiting cone with vertex L(X)(Q); it has components γ_{P,x} : Pom_{s}[Q, P] → L(X)(Q) for (P, x) ∈ els(X) given by γ_{P,x}(g) = {(P_{0}, x · i_{0}, a_{0})}_{≃} where g has augment-strict factorisation:

[figure: P; Q; g; a_{0}; P; i_{0}]

We require that the isomorphism is natural in Q. To show this it is sufficient to verify that with respect to f : Q → Q′ in Pom the map L(X)(f) is the (necessarily unique) mediating map from the colimiting cone L(X)(Q′), γ′ to the cone L(X)(Q), γ ∘ f, i.e. for all (P, x) ∈ els(X),

L(X)(f) ∘ γ′_{P,x} = γ_{P,x} ∘ f .

The verification relies on augment-strict factorisation being unique to within isomorphism. □

Remark 19. Let X be a presheaf over Pom_{s}. In the special case when f is an augmentation a_{0} : Q ↠ Q′, L(X)(a_{0}) : {(P′, x′, a′)}_{≃} ↦ {(P′, x′, a′ ∘ a_{0})}_{≃} .

6.2 Relating Non-Strict and Strict

The next lemma relates the two canonical embeddings c_{s} : E_{s} → \begin{matrix} \\ Pom & s \end{matrix} and

c : E → { \atop Pom}.

Lemma 20. Let E be an event structure in E_{s}. Then, L ∘ c_{s}(E) ≅ c(E).

Proof. We require that L(E_{s}[−, E]) ≅ E[−, E]. ¿From the definition of L,

L(E_{s}[−, E])(Q) = {{(P, x, a)}_{≃} | x : P ↣ E & a : Q ↠ P }

where (P, x, a) ≃ (P′, x′, a′) iff ∃k : P ≅ P′. k ∘ a = a′ & x = x′ · k. Thus elements of L(E_{s}[−, E])(Q) are in 1-1 correspondence with factorisations (to within isomorphism) of morphisms in E[Q, E]. As such factorisations are unique, we obtain the isomorphism

α_{E} : L(E_{s}[−, E])(Q) ≅ E[Q, E] where {(P, x, a)}_{≃} ↦ x ∘ a .

To check that the isomorphism α_{Q} is natural in Q, we require for f : Q → Q′ that the naturality square

\xymatrix{\{\{(P, x, a)\}_{≃} | x : P ↣ E & a : Q ↠ P \} \ar[r]^{α_{Q}} & E[Q, E] \\ \{\{(P′, x′, a′)\}_{≃} | x′ : P′ ↣ E & a′ : Q′ ↠ P′\} \ar[u]^{L(E_{s}[−,E])(f)} \ar[r]^{α_{A′}} & E[Q′, E] \ar[u]_{−∘f}}

commutes. However, by definition

L(E_{s}[−, E])(f)({(P′, x′, a′)}_{≃}) = {(P, x′ ∘ i, a)}_{≃}

where a : Q ↠ P and i : P ↣ P′ provide an augment-strict factorisation of a′ ∘ f :

[figure: Q′; a′; P′; x′; E; Q; f; a; P; i]

Clearly, α_{Q}({(P, x′ ∘ i, a)}_{≃}) = x′ ∘ i ∘ a = x′ ∘ a′ ∘ f = α′_{Q}({P′, x′, a′}_{≃}) ∘ f, so the naturality square commutes, as required. □

6.3 Transfer of Conditions via L

We characterise, to within isomorphism, those presheaves which are images under L : \begin{matrix} \\ Pom & s \end{matrix} → { \atop Pom} as those which are “Confluent” and see how the key conditions of the first representation theorem transfer across L.

Lemma 21. (i) Let Y ∈ { \atop Pom}. Then Y satisfies the “Confluent” condition iff

Y ≅ L(X) for some X ∈ \begin{matrix} \\ Pom & s \end{matrix}. (ii) Let X ∈ \begin{matrix} \\ Pom & s \end{matrix}. Then, X satisfies the “Mono” and “Separated” conditions

iff L(X) satisfies the “Mono” and “Separated” conditions

Proof. (i)“if”: Suppose that in els(L(X))

f : (Q, q) → (R, r) and b : (Q, q) → (Q′, q′)

where q ∈ L(X)(Q), r ∈ L(X)(R) and q′ ∈ L(X)(Q′) and f : Q → R and b : Q ↠ Q′ in Pom. Assume f factorises as

f = Q ↠^{a_{1}} P_{1} ↣^{i} P.

Then, from the definition of L(X),

r = {(P, x, a)}_{≃}, q′ = {(P′, x′, a′)}_{≃} and r = {(P_{1}, x·i, a_{1})}_{≃} = {(P′, x′, a′∘b)}_{≃}

for some a : R ↠ P with x ∈ X(P), and a′ : Q′ ↠ P′ with x′ ∈ X(P′).

Because (P_{1}, x · i, a_{1}) ≃ (P′, x′, a′ ∘ b) there is an isomorphism j : P_{1} ≅ P′ making (P_{1}, x · i, 1_{P_{1}}) ≃ (P′, x′, 1_{P′}). Summarising all the facts in a diagram in els(L(X)) we obtain the two commuting squares

[figure: (P, x̃); (R, r); a; (P_{1}, x̃ · i); i; j; (Q, q); f; a_{1}; b; (P′, x̃′); (Q′, q′); a′]

where x̃ = {(P, x, 1_{P})}_{≃}, x̃′ = {(P′, x′, 1_{P′})}_{≃} and x̃ · i = {(P_{1}, x · i, 1_{P_{1}})}_{≃}. In particular, noting the isomorphism j : (P_{1}, x̃ · i) ≅ (P′, x̃′), we see the “Confluent” condition is satisfied in els(L(X)). “only if”: To show the converse, we show how given Y ∈ { \atop Pom} which is “Confluent” there is a presheaf ext(Y) ∈ \begin{matrix} \\ Pom & s \end{matrix} such that L(ext(Y)) ≅ Y. The presheaf ext(Y) consists of just the extreme elements of Y, those elements of Y which are not restrictions of elements with respect to any augmentations other than isomorphisms:

– ext(Y)(P) = {y ∈ Y (P) | ∀a : P ↠ Q, y′ ∈ Y (Q)). y = y′ · a ⇒ a is iso.} for pomsets P.

– ext(Y)(j) is the restriction of Y (j), for morphisms j : P ↣ P′ in Pom_{s}; that ext(Y)(j) is well-defined, i.e. that if y′ ∈ ext(Y)(P′), then Y (j)(y′) ∈ ext(Y)(P), follows directly from Y being “Confluent” and the uniqueness up to isomorphism of factorisation. It is now clear that ext(Y) ∈ \begin{matrix} \\ Pom & s \end{matrix}. We require that L(ext(Y)) ≅ Y. By

definition L(ext(Y)(Q) = {{(P, y, a}_{≃} | y ∈ ext(Y)(P) & a : Q ↠ P }. Defining δ({P, y, a)}_{≃}) = y · a yields a function δ : L(ext(Y))(Q) → Y (Q) which is seen to be well-defined directly from the definition of ≃. δ is 1-1: Suppose δ({(P, Y, a)}_{≃}) = δ({(P′, y′, a′)}_{≃}). Then y_{0} =_{def} y ·a = y′ ·a′. As Y is assumed “Confluent” we obtain a commuting diagram

\xymatrix{ & (P, y) \ar@{->>}[dr]^{b} \\ (Q, y_{0}) \ar@{->>}[ur]^{a} \ar@{->>}[dr]_{a′} &  & (P_{1}, y_{1}) \\  & (P′, y′) \ar@{->>}[ur]_{b′}}

in els(Y). However (P, y) and (P′, y′) are extreme elements of Y. Hence b and b′ are isomorphisms making (P, y, a) ≃ (P′, y′, a′). δ is onto: Suppose y ∈ Y (Q). Because pomsets in Pom are finite, any chain

(Q, y) ↠^{a_{1}} (Q, y) ↠^{a_{2}} ⋯ ↠^{a_{n}} (Q_{n}, y_{n}) ↠^{a_{n+1}} ⋯

is els(Y) must eventually only involve isomorphisms, i.e. for some n for all m ≥ n, each augmentation a_{m} is an isomorphism. Taking a = a_{n−1} ∘ ⋯ ∘ a_{1} there is an extreme element y_{n} for which δ({(Q_{n}, a, y_{n})}_{≃}) = y_{n} · a = y.

It follows that, to within isomorphism, the images of L are precisely those presheaves Y of { \atop Pom} which are “Confluent”. (ii) We now show that the “Mono” and “Separated” conditions transfer via L. We first observe that for X ∈ \begin{matrix} \\ Pom & s \end{matrix},

ext(L(X)) ≅ X

because extreme elements of L(X), of the form {(P, x, 1_{P})}_{≃}, are in 1-1 correspondence with x ∈ X(P). “if”: Assuming L(X) is “Mono” and “Separated”, the “Mono” and “Separated” conditions can be also seen to hold in the restriction ext(L(X)), which is isomorphic to X. “only if”: Assuming X is “Mono” and “Separated” entails that X ≅ E_{s}[−, E] for some event structure E. By Lemma 20, L(X) ≅ E[−, E]. Now, just as in the proof of Lemma 11, E[−, E] and so L(X) satisfies “Mono” (because morphism from pomsets to event structure in E are mono) and “Separated” (because morphisms are determined by their actions on events.) □

We now obtain, as a corollary: Proof of Theorem 17: By Lemma 20, a nonempty presheaf Y ∈ { \atop Pom} is represented by some event structure in E iff Y ≅ L(X) for some nonempty X ∈ \begin{matrix} \\ Pom & s \end{matrix} which is “Mono” and “Separated”. But Lemma 21 says that the latter properties hold of X iff Y ≅ L(X) is “Mono”, “Separated” and “Confluent”. □

References

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

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

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

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

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

6. M. Fiore, G. L. Cattani and G. Winskel. Weak bisimulation and open maps. To appear in LICS’99.

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

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

9. Pratt, V.R., Modelling concurrency with partial orders. International Journal of Parallel Programming, 15,1, p.33-71, Feb. 1986.

10. A. J. Power, G. L. Cattani and G. Winskel. A categorical axiomatics for bisimulation. In Proceedings of CONCUR’98, LNCS 1466, pages 591–596, 1998.

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

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

13. G.Winskel. A Linear Metalanguage for Concurrency. In Proceedings of AMAST’98, LNCS, 1999.

Recent BRICS Report Series Publications

RS-99-7 Glynn Winskel. Event Structures as Presheaves—Two Representation Theorems. March 1999. 16 pp.

RS-99-6 Rune B. Lyngsø, Christian N. S. Pedersen, and Henrik Nielsen. Measures on Hidden Markov Models. February 1999. 27 pp. To appear in Seventh International Conference on Intelligent Systems for Molecular Biology, ISMB ’99 Proceedings, 1999.

RS-99-5 Julian C. Bradfield and Perdita Stevens. Observational Mu-Calculus. February 1999. 18 pp.

RS-99-4 Sibylle B. Fröschle and Thomas Troels Hildebrandt. On Plain and Hereditary History-Preserving Bisimulation. February 1999. 21 pp.

RS-99-3 Peter Bro Miltersen. Two Notes on the Computational Complexity of One-Dimensional Sandpiles. February 1999. 8 pp.

RS-99-2 Ivan B. Damgård. An Error in the Mixed Adversary Protocol by Fitzi, Hirt and Maurer. February 1999. 4 pp.

RS-99-1 Marcin Jurdziński and Mogens Nielsen. Hereditary History Preserving Simulation is Undecidable. January 1999. 15 pp.

RS-98-55 Andrew D. Gordon, Paul D. Hankin, and Søren B. Lassen. Compilation and Equivalence of Imperative Objects (Revised Report). December 1998. iv+75 pp. This is a revision of Technical Report 429, University of Cambridge Computer Laboratory, June 1997, and the earlier BRICS report RS-97-19, July 1997. Appears in Ramesh and Sivakumar, editors, Foundations of Software Technology and Theoretical Computer Science: 17th Conference, FST&TCS ’97 Proceedings, LNCS 1346, 1997, pages 74–87.

RS-98-54 Olivier Danvy and Ulrik P. Schultz. Lambda-Dropping: Transforming Recursive Equations into Programs with Block Structure. December 1998. 55 pp. To appear in Theoretical Computer Science.

RS-98-53 Julian C. Bradfield. Fixpoint Alternation: Arithmetic, Transition Systems, and the Binary Tree. December 1998. 20 pp.