[Oxford Internship] The Category of Event Structures
My M1 intership has just begun! This time, it’s at Oxford University, under the supervision of Ohad Kammar.
It will revolve around the foundations of concurrency semantics. To be more precise:
different kinds of maps between Glynn Winskel’s event structures give rise to different kinds of concurrency models. These are expressible as monads over event structures with symmetry and rigid maps. The goal will be to describe these monads using algebraic operations and equations.
Just like last year, I’ll try to write about it with blog posts.
To begin with, let’s begin with the main protagonists: event structures.
The Category of Event Structures
Objects
In broad strokes, event structures are a way to represent a set of events (that are part of a given process) depending on one another: events may be caused/cause/conflict with other events.
- An event structure $E ≝ ⟨\carrier E, ≤_E, \Con[E]⟩$:
-
is given by:
- a poset $(\carrier E, ≤_E)$ of events (where $≤$ is thought of as the causal dependency relation) such that
- for all $e∈ \carrier E$, $\dc e ≝ \lbrace e’∈\carrier E \mid e’ ≤_E e \rbrace$ (downward closure) is finite
- a consistency relation $\Con[E] ⊆ \Pfin(E)$ such that
- for all $e∈ \carrier E$, $\lbrace e \rbrace ∈ \Con[E]$
- $\Con[E]$ is stable under inclusion $⊆$
- if $x ∈ \Con[E]$ and $e’ ≤_E e ∈ x$ then $x ∪ \lbrace e’ \rbrace ∈ \Con[E]$
- a poset $(\carrier E, ≤_E)$ of events (where $≤$ is thought of as the causal dependency relation) such that
- Configurations of an event structure $E$:
- \[\Confstar[E] ≝ \lbrace x ⊆ \carrier E \mid x \text{ is consistent and down-closed} \rbrace\]
where
\[x \text{ is consistent} ⟺ \Pfin(x) ⊆ \Con[E]\]and
\[x \text{ is down-closed} ⟺ \dc x ≝ \bigcup_{e∈ x} \dc e ⊆ x\]NB: $\Conf[E]$ is the set of finite configurations.
\[\left\langle E \right\rangle\]1.
\[∀ p∈\carrier E, \quad \dc p ∈ \Conf[E]\]
This stems from the fact that $\dc p$ is:
- finite by definition of $E$ being an event structure
- down-closed, by transitivity of $≤_E$
-
consistent, as
- $\lbrace p \rbrace ∈ \Con[E]$
-
and by the third property of $\Con[E]$ (with $x = \lbrace p \rbrace$): \(∀ p_1 ∈ \dc p, \lbrace p, p_1 \rbrace ∈ \Con[E]\)
as a result of which, by a straightforward recurrence (by setting $x = \lbrace p, p_1 \rbrace, \ldots, \lbrace p, p_1, ⋯, p_n \rbrace$):
\[∀ p_1, \ldots, p_n ∈ \dc p, \, \lbrace p, p_1, \ldots, p_n \rbrace ∈ \Con[E]\]so by closure under inclusion:
\[∀ p_1, \ldots, p_n ∈ \dc p, \, \underbrace{\lbrace p_1, \ldots, p_n \rbrace}_{\rlap{\text{any finite subset of } \dc p \text{ is of this form}}} ∈ \Con[E]\]
2.
A finite subset of events is in the consistency relation iff it occurs as a subset of a finite configuration.
-
$⟹$: if $x ∈ \Con[E]$, then $x ⊆ \dc x ≝ \bigcup_{e ∈ x} \dc e$, which is:
- finite, as it is a finite ($x$ is finite) union of finite (by the event structure definition) sets
- down-closed, by transitivity of $≤_E$
-
consistent: like in the first exercise (and since any subset of $x$ is in $\Con[E]$ by closure by inclusion), we can show by recurrence that for all $y ≝ \lbrace e^{(1)}, \ldots, e^{(k)} \rbrace ∈ \Pfin(x)$:
\[∀ e_1^{(1)}, \ldots, e_{n_1}^{(1)}, \dots, e_1^{(k)}, ⋯, e_{n_k}^{(k)} ∈ \dc x,\\ \, y ∪ \lbrace e_1^{(1)}, \ldots, e_{n_1}^{(1)}, \dots, e_1^{(k)}, ⋯, e_{n_k}^{(k)} \rbrace ∈ \Con[E]\]which implies, by closure under inclusion, that:
\[∀ e_1^{(1)}, \ldots, e_{n_1}^{(1)}, \dots, e_1^{(k)}, ⋯, e_{n_k}^{(k)} ∈ \dc x,\\ \, \underbrace{\lbrace e_1^{(1)}, \ldots, e_{n_1}^{(1)}, \dots, e_1^{(k)}, ⋯, e_{n_k}^{(k)} \rbrace}_{\rlap{\text{any finite subset of } \dc x \text{ is of this form}}} ∈ \Con[E]\]
-
$⟸$: owing to the fact that any configuration is consistent.
3.
For all $e, e’∈\carrier E$, we have: \(e ≤ e' ⟺ \Big(∀ x ∈ \Conf[E], e'∈ x ⟹ e∈ x\Big)\)
-
$⟹$: it’s due to the fact that $x$ is down-closed, as a configuration.
-
$⟸$: with $x ≝ \dc e’$, it results that $e ∈ \dc e’$, i.e. $e ≤ e’$
Maps
- A map of event structures $f: E ⟶ F$:
-
is a function $f: \carrier E ⟶ \carrier F$ that is
- configuration preserving: if $x ∈ \Conf[E]$, then $f[x] ∈ \Conf[F]$
- locally injective: for $x ∈ \Conf[E]$, if $e_1, e_2 ∈ x$ and $f(e_1) = f(e_2) ∈ F$, then $e_1 = e_2$
- A rigid map of event structures:
-
is a map that is also monotone: if $e_1 ≤_E e_2$, then $f(e_1) ≤_F f(e_2)$.
4.
For any map $f: E ⟶ F$:
\[∀ e ∈\carrier E, \quad \dc f e ⊆ f(\dc e)\]
$\dc f e$ is the smallest configuration containing $f e$, since
- it is a configuration
- for any configuration $y$ such that $f e ∈ y$, $\dc f e ⊆ y$ as $y$ is down-closed
And:
- as $f$ preserves configurations, $f[\dc e]$ is also a configuration
- $f e ∈ f[\dc e]$
so the result follows by minimality of $\dc f e$.
5.
\[\begin{align*} \dc f[x] & = \dc f\Big[\bigcup_{e∈ x} e\Big]\\ & = \dc \bigcup_{e∈ x} f(e) &&\text{(since the direct images preserve union)} \\ & = \bigcup_{e∈ x} \dc f(e) &&\text{(by definition of } \dc \text{ on sets)}\\ & ⊆ \bigcup_{e∈ x} f(\dc e) &&\text{(by the previous lemma)}\\ & = f\Big[\bigcup_{e∈ x} \dc e\Big]\\ & = f[\dc x] &&\text{(by definition of } \dc x \text{ )} \end{align*}\]For any map $f: E ⟶ F$:
\[∀ x ⊆ \carrier E, \quad \dc f [x] ⊆ f[\dc x]\]
6.
Any map $f: E ⟶ F$ is causality reflecting on configurations:
\[∀ e_1, e_2 ∈ x ∈ \Confstar[E], \quad f e_1 ≤_F f e_2 ⟹ e_1 ≤_E e_2\]
If $f(e_1) ∈ \dc f (e_2) ⊆ f (\dc e_2)$, then there exists $e_0 ≤_E e_2$ such that
\[f(e_1) = f(e_0)\]As the configuration $x$ is down-closed: $e_0 ∈ x$. On top of that, as $f$ is injective on the configuration $x \ni e_1, e_0$:
\[e_1 = e_0\]and $e_1 = e_0 ≤_E e_2$
NB: a map is not necessarily causality reflecting on the whole carrier set, as exemplfied by the following counter-example: if
- \[\begin{align*} \carrier E &≝ \lbrace a, b \rbrace \\ \Con[E] &≝ \lbrace \lbrace a \rbrace, \lbrace b \rbrace, ∅ \rbrace\\ a &\not≤_E b \end{align*}\]
- \[\begin{align*} \carrier F &≝ \lbrace c \rbrace \\ \Con[F] &≝ \lbrace \lbrace c \rbrace, ∅ \rbrace& \end{align*}\]
then the only map $f: E ⟶ F$ (sending all the elements to $c$) is not reflecting causality:
\[c = f(a) ≤_F f(b) = c \quad\text{ but }\quad a \not≤ b\]7.
Note that $f: \carrier E ⟶ \carrier F$ is
- monotone iff $∀ e ∈ \carrier E, \, f[\dc e] ⊆ \dc f(e)$
causality reflecting on configurations iff $∀ x ∈ \Confstar[E], ∀ e∈ x, \, f^{-1}_{ x}[\dc f(e)] ⊆ \dc e$
The proof is straightforward.
8.
Any rigid map $f:E⟶F$ is configuration reflecting on configurations:
\[∀ x' ⊆ x ∈ \Confstar[E], \; f[x'] ∈ \Confstar[F] ⟹ x' ∈ \Confstar[E]\]
Let’s show that any $x’ ⊆ x ∈ \Confstar[E]$ such that $f[x’] ∈ \Confstar[F]$ is a configuration of $E$.
-
$x’$ is consistent, as $x$ is (and $⊆$ is transitive)
-
$x’$ is down-closed:
As $f[x’]$ is a configuration, hence down-closed:
\[\dc f[x'] ⊆ f[x']\]But $f$ being monotone implies:
\[f[\dc x'] ⊆ \dc f[x']\]So
\[f[\dc x'] ⊆ f[x']\]and as taking preimages preserves inclusion and $f$ is injective on the configuration $x \supseteq x’$:
\[\dc x' \overset{\small\text{injectivity}}{=} f^{-1}(f(\dc x')) ⊆ f^{-1}(f(x')) \overset{\small\text{injectivity}}{=} x'\]
9.
Any map $f: E ⟶ F$ is rigid iff
\[∀ x ∈\Conf[E], ∀ y ∈ \Conf[F], \quad y ⊆ f[x] ⟹ ∃ x' ∈ \Conf[E], \; x' ⊆ x \, ∧ \, f x' = y\]
-
$⟹$: Let’s assume that $f$ is rigid and $y ⊆ f[x]$. Then $y ≝ f[x’]$, where $x’ ∈ \Pfin(x)$. All that remains to be shown is that $x$ is a configuration, which directly results from the previous lemma.
-
$⟸$: it’ll be sufficient to show that for all $e∈\carrier E$, $f[\dc e] ⊆ \dc f(e)$. As $f$ is a map:
\[y ≝ \dc f(e) ⊆ f[\dc e]\]So there exists $\Conf[E] \ni x’ ⊆ \dc e$ such that $f x’ = y$. On top of that, $f(e) ∈ y$ so by injectivity of $f$ on the configuration $\dc e $:
\[e ∈ x'\]Therefore:
\[\begin{align*} & \quad \dc e ⊆ x' &&\text{(as } x' \text{ is down-closed)} \\ ⟹ & \quad f[\dc e] ⊆ \underbrace{f[x']}_{= \, y \; ≝ \; \dc f(e)} &&\text{(as images preserve inclusion)}\\ \end{align*}\]
Well-founded posets
- A well-founded/finitary poset:
-
is a poset in which every element has only a finite number of elements below it.
10.
Let $P$ be a well-founded poset. Then $⟨\carrier P , ≤_P , \Pfin(P)⟩$ is an event structure.
All the properties to check are trivially true:
-
$≤_P$ is indeed a partial order for which all the downard closures are finite (as $P$ is well-founded)
-
all the singletons are members of $\Pfin(P)$
-
$\Pfin(P)$ is stable under inclusion
-
the augmentation property holds, as $x ∪ \lbrace e’ \rbrace$ is finite provided $x$ is.
11.
Let $P, Q$ be well-founded posets, and $f : \carrier P ⟶ \carrier Q$ be any function. Then: $f$ is a rigid map iff $∀ p ∈ \carrier P, \; f[\dc p] = \dc f p$ and $f$ is causality reflecting.
-
$⟹$: if $f$ is a rigid map, then it is a map, and it is causality reflecting on configurations as showed previously, and for all $p ∈ \carrier P$:
- $f[\dc p] ⊆ \dc f p$ as $f$ is monotone
- $\dc f p ⊆ f[\dc p]$ as shown previously (since $\dc f p$ is the smallest configuration containing $f p$)
-
$⟸$: if $f$ is causality reflecting and $f[\dc p] = \dc fp$, then:
- $f$ is monotone as $f[\dc p] ⊆ \dc f p$ for all $p∈\carrier P$
- $f$ is configuration preserving, as the image of a finite set is a finite set
-
$f$ is injective (and hence locally injective): if $f(e) = f(e’)$, then as $f$ is causality reflecting:
- $f(e) ≤_F f(e’)$ so $e ≤_E e’$
- $f(e’) ≤_F f(e)$ so $e’ ≤_E e$
thus $e = e’$ by antisymmetry.
Path lifting property
- The category of paths $ℙ$:
-
- Objects: finite posets (seen as event structures)
- Morphisms: rigid maps
Let $I : ℙ ↪︎ \cal{E}$ be its full embedding in the category of event structures and rigid maps.
- Comma category $I ↓ E$:
-
- Objects: pairs $⟨P, f⟩$ where $P∈ℙ$ and $f: \carrier P ⟶ \carrier E$ is a rigid map
- Morphisms: $a : ⟨P,f⟩ ⟶ ⟨Q,g⟩$ where $a: \carrier P ⟶ \carrier Q$ is a rigid map and the following triangle commutes:
- A map $f: E ⟶ F$ satisifies the path lifting property:
-
iff any such commuting square where $P, Q ∈ ℙ$ factors into two commuting triangles:
\[\begin{xy} \xymatrix{ P \ar[r] \ar[d] & E \ar[d]^f \\ Q \ar[r] \ar@{.>}[ru] & F } \end{xy}\]
12.
We can regard $⟨\Conf[E], ⊆⟩$ as a sub-category of the comma $I ↓ E$. Is it full?
It’s not: with
- $\carrier E ≝ \lbrace α, β \rbrace, \; α \not≤ β$
- $x ≝ \lbrace α \rbrace ∈ \Conf[E]$
- $f ≝ \begin{cases}
x &⟶ E
α &\mapsto β \end{cases}$
then the following diagram commutes:
\[\begin{xy} \xymatrix{ x \ar[rr]^{f} \ar[rd]_f & & E \ar[ld]^{id} \\ & E & } \end{xy}\]so that $f ∈ \Hom_{I ↓ E}(x, E)$, but $f$ is not the inclusion map.
13.
A rigid map $f : E ⟶ F$ satisfies the path lifting property iff:
\[∀ x∈\Conf[E], ∀ y∈\Conf[F], \quad f[x] ⊆ y ⟹ ∃x'∈\Conf[E]; x⊆x' \; ∧ \; f[x'] = y\]
-
$⟹$: Let $x∈\Conf[E]$ and $y∈\Conf[F]$ such that $f[x] ⊆ y$. Then by lifting property, the following square factors into these two triangles (where $ι_x$ and $ι_y$ are the inclusion maps):
\[\begin{xy} \xymatrix{ x \ar[r]^{ι_x} \ar[d]_{f_{|x}} & E \ar[d]^f \\ y \ar[r]_{ι_y} \ar@{.>}[ru]^{∃ \; φ} & F } \end{xy}\]By setting $x’ ≝ φ[y]$:
- $x’ ∈ \Conf[E]$: since is the image of a finite configuration by a configuration-preserving map
-
$x ⊆ x’$: as
\[\begin{align*} & \quad f[x] ⊆ y \\ ⟺ & \quad \underbrace{φ[f[x]]}_{= \; ι_x[x] \, = \, x} ⊆ \underbrace{φ[y]}_{≝ \; x'} &&\text{(since taking images preserves inclusion)}\\ \end{align*}\] - $f[x’] = f[φ[y]] = ι_y(y) = y$
-
$⟸$: let $P, Q ∈ ℙ$ such that the following square commutes:
\[\begin{xy} \xymatrix{ P \ar[r]^p \ar[d]_g & E \ar[d]^f \\ Q \ar[r]_q & F } \end{xy}\]Then $x ≝ p[P] ∈ \Conf[E]$ and $y ≝ q[Q] ∈ \Conf[F]$ (images of finite configurations by configuration-preserving maps) are such that
\[f[x] = f[p(P)] = q[g[P]] \overset{g[P] \, ⊆ \, Q}{⊆} q[Q] ≝ y\]so there exists a finite configuration $\Conf[E] \ni x’ \supseteq x$ such that $f[x’] = y$.
By local injectivity, the function $f_{ x’}^{ y}: x’ ⟶ y$ (corestriction to $y$ of the restriction to $x’$) is bijective. One can check that its inverse ${f_{ x’}^{ y}}^{-1}$ remains a rigid map: - it is injective, thus locally injective.
- it is monotone, since the map $f$ is causality reflecting on configurations (as seen previously)
-
it is configuration-preserving, that is:
\[∀ \Conf[F] \ni y' ⊆ y, \; f^{-1}[y'] ∈ \Conf[E]\]It amounts to show that
\[∀ x'' ⊆ x', \; y' ≝ f[x''] ∈ \Conf[F] ⟹ x'' ∈ \Conf[E]\]which results from $f$ being configuration-reflecting on the configuration $x’$ (as it is a rigid map: cf. lemma 8).
\[\begin{align*} φ \circ g & = {f_{|x'}^{|y}}^{-1} \circ \underbrace{q \circ g}_{= \, f \circ p} \\ & = p &&\text{(as } f\circ p: P ⟶ f[x] ⊆ f[x'] = y \text{ )} \\ \end{align*}\] \[\begin{xy} \xymatrix{ P \ar[r]^p \ar[d]_g & E \ar[d]^f \\ Q \ar[r]_q \ar@{.>}[ru]_{φ} & F } \end{xy}\]So by setting $φ ≝ {f_{ x’}^{ y}}^{-1} \circ q$, the result follows, as
Leave a comment