# Event structure semantics for multiparty sessions

Ilaria Castellani, Mariangiola Dezani-Ciancaglini, Paola Giannini

► To cite this version:

Ilaria Castellani, Mariangiola Dezani-Ciancaglini, Paola Giannini. Event structure semantics for multiparty sessions. Journal of Logical and Algebraic Methods in Programming, 2023, 131, 10.1016/j.jlamp.2022.100844. hal-03940191

HAL Id: hal-03940191

https://inria.hal.science/hal-03940191

Submitted on 28 Jan 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Event Structure Semantics for Multiparty Sessions

Ilaria Castellani¹,¹,*, Mariangiola Dezani-Ciancagliniᵇ, Paola Gianniniᶜ,²

ªINRIA, Université Côte d'Azur, France

ᵇDipartimento di Informatica, Università di Torino, Italy

ᶜDiSSTE,Università del Piemonte Orientale, Italy

**Abstract**

We propose an interpretation of multiparty sessions as *Flow Event Structures*, which allows concurrency within sessions to be explicitly represented. We show that this interpretation is equivalent, when the multiparty sessions can be described by global types, to an interpretation of such global types as *Prime Event Structures*.

**Keywords:** Communication-centric Systems, Communication-based Programming, Process Calculi, Event Structures, Multiparty Session Types.

# 1. Introduction

Session types were proposed in the mid-nineties [54, 38], as a tool for specifying and analysing web services and communication protocols. They were first introduced in a variant of the π-calculus to describe binary interactions between processes. Such binary interactions may often be viewed as client-server protocols. Subsequently, session types were extended to *multiparty sessions* [39, 40], where several participants may interact with each other. A multiparty session is an interaction among peers, and there is no need to distinguish one of the participants as representing the server. All one needs is an abstract specification of the protocol that guides the interaction. This is called the *global type* of the session. The global type describes the behaviour of the whole session, as opposed to the local types that describe the behaviours of single participants. In a multiparty session, local types may be retrieved as projections from the global type.

Typical safety properties ensured by session types are *communication safety* (absence of communication errors), *session fidelity* (agreement with the protocol) and *deadlock-freedom* [40]. When dealing with multiparty sessions, the type system is often enhanced so as to guarantee also the liveness property known as *progress* (no participant gets stuck) [41].

Some simple examples of sessions not satisfying the above properties are: 1) a

*Corresponding author. INRIA, 2004 Route des Lucioles, BP 93, 06902 Sophia Antipolis FRANCE
*Email addresses: ilaria.castellani@inria.fr (Ilaria Castellani), dezani@di.unito.it (Mariangiola Dezani-Ciancaglini), paola.giannini@uniupo.it (Paola Giannini)

¹This work was partially funded by the ANR17-CE25-0014-01 CISC project.

²This original research has the financial support of the Università del Piemonte Orientale. This work was partially funded by the MIUR project "T-LADIES" (PRIN 2020TL3X8X).
<footnote>sender emitting a message while the receiver expects a different message (communication error); 2) two participants both waiting to receive a message from the other one (deadlock due to a protocol violation); 3) a three-party session where the first participant waits to receive a message from the second participant, which keeps interacting forever with the third participant (starvation).</footnote>

<footnote>What makes session types particularly attractive is that they offer several advantages at once: 1) static safety guarantees, 2) automatic check of protocol implementation correctness, based on local types, and 3) a strong connection with linear logics [13, 55, 59, 52, 14], and with concurrency models such as communicating automata [32], graphical choreographies [44, 56] and message-sequence charts [40].</footnote>

<footnote>In this paper we further investigate the relationship between multiparty session types and concurrency models, by focussing on Event Structures [62]. We consider a standard multiparty session calculus where sessions are described as networks of sequential processes [33]. Each process implements a participant in the session. We propose an interpretation of such networks as *Flow Event Structures* (FESs) [8, 10] (a subclass of Winskel's Stable Event Structures [62]), which allows concurrency between session communications to be explicitly represented. We then introduce global types for these networks, and define an interpretation of them as *Prime Event Structures* (PESs) [60, 49]. Since the syntax of global types does not allow all the concurrency among communications to be expressed, the events of the associated PES need to be defined as equivalence classes of communication sequences up to *permutation equivalence*. We show that when a network is typable by a global type, the FES semantics of the former is equivalent, in a precise technical sense, to the PES semantics of the latter. To prove this equivalence, we exploit the bisimilarity of their Labelled Transition Systems, as expressed by the Subject Reduction and Session Fidelity theorems (Theorem 6.10 and Theorem 6.11). An alternative approach would have been to compare the two ESs directly, thus conducting the whole reasoning within the denotational model itself. However, while one side of the comparison (mapping the PES of the type to the FES of the network, which can be viewed as a synthesis problem) would be very direct, the other side (reconstructing the PES of the type from the FES of the network) would be more involved, as it would require a structural characterisation of the FESs that represent typable networks, which is far from obvious and therefore is left for future work. This issue will be discussed at length at the end of Section 7.</footnote>

<footnote>Event Structures have been used to give semantics to process calculi ever since their introduction at the beginning of the eighties [60, 49] (see Section 9 for an extensive historical discussion). A specific feature of our proposed FES semantics for networks is that we impose strong semantic constraints on the construction of the events themselves (like duality of the histories of their components) in order to reduce the number of events from the very beginning, and to enforce already at the syntactic level some of the expected semantic properties. This allows us to obtain more compact FESs, with fewer events, which is an advantage when displaying their graphical representations³, as well as handling examples and carrying out</footnote>

<footnote n="3">³Both FESs and PESs enjoy a graphical representation (see Figure 5 and Figure 6), as opposed to</footnote>
63 proofs.

64 In a companion paper [16], we investigated a similar Event Structure semantics
65 for a session calculus with asynchronous communication, which led to a quite
66 different treatment as it made use of a new notion of asynchronous global type. A
67 detailed comparison with [16] will be given in Section 9.

68 This paper is an expanded and amended version of [15]. The main novelty is
69 that we use a coinductive definition for processes and global types, which simplifies
70 several definitions and proofs, and a more stringent definition for network events.
71 This definition relies on the new notion of causal set, which is crucial for the
72 correctness of our ES semantics. Finally, the present paper includes the proofs of all
73 results, some of which require ingenuity.
74

75 The paper is organised as follows. Section 2 introduces our multiparty session
76 calculus. In Section 3 we recall the definitions of PESs and FESs, which will be used
77 to interpret processes (Section 4) and networks (Section 5), respectively. PESs are
78 also used to interpret global types (Section 7), which are defined in Section 6. In
79 Section 8 we prove the equivalence between the FES semantics of a network and
80 the PES semantics of its global type. Section 9 discusses related work and sketches
directions for future work.
81

82 The proofs of all theorems and propositions are given in the main paper, except
83 for those of Subject Reduction (Theorem 6.10) and Session Fidelity (Theorem 6.11),
84 which are standard and thus deferred to Appendix B. The proofs of lemmas, when
85 not trivial, are collected in Appendices A, B, C, D and E. To help the reader, Ap-
86 pendix F contains a glossary of the symbols used and a table of the notations with
their meaning and a reference to where they are defined.
87

## 2. A Core Calculus for Multiparty Sessions

88 We now formally introduce our calculus, where multiparty sessions are rep-
89 resented as networks of processes. We assume the following base sets: *session
90 participants*, ranged over by *p*, *q*, *r*,... and forming the set *Part*, and *messages*, ranged
91 over by *λ*, *λ'*,... and forming the set *Msg*.

92 Let $\pi \in \{\mathbf{p}!\lambda, \mathbf{p}?\lambda \mid \mathbf{p} \in \text{Part}, \lambda \in \text{Msg}\}$ denote an *action*. The action $\mathbf{p}!\lambda$ represents an output of message $\lambda$ to participant $\mathbf{p}$, while the action $\mathbf{p}?\lambda$ represents an input of message $\lambda$ from participant $\mathbf{p}$. The *participant of an action*, $\text{pt}(\pi)$, is defined by
93
94
95 $\text{pt}(\mathbf{p}!\lambda) = \text{pt}(\mathbf{p}?\lambda) = \mathbf{p}$.

**Definition 2.1 (Processes).** *Processes are defined by:*

$$
P ::= \mathit{coind} \bigoplus_{i \in I} \mathbf{p}!\lambda_i; P_i \mid \sum_{i \in I} \mathbf{p}?\lambda_i; P_i \mid \mathbf{0}
$$

96 where *I* is non-empty and *λ*<sub>*h*</sub> ≠ *λ*<sub>*k*</sub> for all *h*, *k* ∈ *I*, *h* ≠ *k*, i.e. *messages in choices are all different*.

98 Processes of the shape ⊕<sub>i∈I</sub> p!λ<sub>i</sub>; P<sub>i</sub> and Σ<sub>i∈I</sub> p?λ<sub>i</sub>; P<sub>i</sub> are called output and input processes, respectively.
99

<footnote>other kinds of stable ESs.</footnote>
The symbol ::=coind, in the definition above and in later definitions, indicates that the productions should be interpreted *coinductively*. Namely, they define possibly infinite processes. However, we assume such processes to be *regular*, that is, with finitely many distinct subprocesses. In this way, we only obtain processes which are solutions of finite sets of equations, see [20]. So, when writing processes, we shall use (mutually) recursive equations. When *I* is a singleton, $\bigoplus_{i \in I} p!\lambda_i; P_i$ will be rendered as $p!\lambda; P$ and $\sum_{i \in I} p?\lambda_i; P_i$ will be rendered as $p?\lambda; P$. When *I* contains only two elements, as it will be the case in most of our examples, we shall feel free to use the binary choices $p!\lambda_1; P_1 \oplus p!\lambda_2; P_2$ and $p!\lambda_1; P_1 + p!\lambda_2; P_2$, where the branches $p!\lambda_i; P_i$ should be viewed as being parenthesised (since the connector ; is not an operator of our calculus, but an integral part of the guarded sum operators). Trailing *0* processes will be omitted.

Processes may be viewed as trees whose internal nodes are decorated by $p!$ or $p?$, leaves by $0$, and edges by messages $\lambda$.

In a full-fledged calculus, messages would carry values, namely they would be of the form $\lambda(v)$. For simplicity, we consider only pure messages here. This will allow us to project global types directly to processes, without having to explicitly introduce local types, see Section 6.

**Definition 2.2 (Networks).** Networks are defined by:

$$N = p[[P]] \mid p[[P]] \mid N$$

We assume the standard structural congruence $\equiv$ on networks, stating that parallel composition is associative and commutative and has neutral element $p[[0]]$ for any fresh $p$. Given the associativity of $\parallel$, we shall feel free to write networks in the form $N = p_1[[P_1]] \parallel \cdots \parallel p_n[[P_n]]$ in the sequel.

If $P \neq 0$ we write $p[[P]] \in N$ as short for $N \equiv p[[P]] \parallel N'$ for some $N'$. We define the set of participants of N to be $\{p | \exists P. p[[P]] \in N\}$. We say that a network is *unary* if it has a unique participant<fnref n="4" /> and *binary* if it has exactly two participants.

To express the operational semantics of networks, we use an LTS whose labels record the message exchanged during a communication together with its sender and receiver. The set of communications, ranged over by $\alpha, \alpha'$, is defined to be $\{pq\lambda | p, q \in \text{Part}, \lambda \in \text{Msg}\}$, where $pq\lambda$ represents the transmission of a message $\lambda$ from participant $p$ to participant $q$.

$$p[[ \bigoplus_{i \in I} q!\lambda_i; P_i ]] \parallel q[[ \sum_{j \in J} p?\lambda_j; Q_j ]] \parallel N \xrightarrow{pq\lambda_k} p[[P_k]] \parallel q[[Q_k]] \parallel N \quad \text{where } k \in I \cap J \quad [\text{Com}]$$

<caption>**Figure 1:** LTS for networks.</caption>

The LTS semantics of networks is specified by the unique rule [Com] given in Figure 1. Notice that rule [Com] is symmetric with respect to input and output

<footnote n="4">⁴Unary networks will not be typable, and therefore, by Subject Reduction, a typable network will never evolve to a unary network. On the other hand, this will be possible for non typable networks.</footnote>
132 choices. In a well-typed network (see Section 6) it will always be the case that $I \subseteq J$,
133 ensuring that participant p can freely choose an output, since participant q offers
134 all corresponding inputs. Note also that a unary network has no transitions.

135 Note that we could have given first the (standard) LTS semantics for processes,
136 and then derived the LTS for networks from it. However, the syntax of our calculus
137 is so simple that the LTS for networks can be defined directly. Thus we chose to
138 omit the LTS for processes, which would anyway be of no use in the sequel.

139 In the following we will make an extensive use of finite (and possibly empty)
140 sequences of communications. As usual we define them as traces.

**Definition 2.3 (Traces).** (Finite) traces $\sigma \in \textit{Traces are defined by}$:

$$ \sigma ::= \epsilon \mid \alpha \cdot \sigma $$

141 We use $|\sigma|$ to denote the length of the trace $\sigma$.

142 The set of participants of a trace, notation part($\sigma$), is defined by part($\epsilon$) = $\emptyset$ and
143 part($pq\lambda \cdot \sigma$) = {$p, q$} $\cup$ part($\sigma$).

144 When $\sigma = \alpha_1 \cdots \alpha_n$ ($n \ge 1$) we write $N \xrightarrow{\sigma} N'$ as short for $N \xrightarrow{\alpha_1} N_1 \cdots \xrightarrow{\alpha_n} N_n = N'$.

### 3. Event Structures

146 We recall now the definitions of *Prime Event Structure* (PES) from [60, 49] and
147 *Flow Event Structure* (FES) from [8]. The class of FESs is more general than that
148 of PESs: for a precise comparison of various classes of event structures, we refer
149 the reader to [9]. As we shall see in Sections 4 and 5, while PESs are sufficient to
150 interpret processes, the greater generality of FESs is needed to interpret networks.

151 **Definition 3.1 (Prime Event Structure).** A prime event structure (PES) is a tuple $S = (E, \leq, \#)$ where:

153 1. $E$ is a denumerable set of events;

154 2. $\leq \subseteq (E \times E)$ is a partial order relation, called the causality relation;

155 3. $\# \subseteq (E \times E)$ is an irreflexive symmetric relation, called the conflict relation, satisfying
156 the property: $\forall e, e', e'' \in E : e \# e' \le e'' \Rightarrow e \# e''$ (conflict hereditariness).

157 **Definition 3.2 (Flow Event Structure).** A flow event structure (FES) is a tuple $S = (E, <, \#)$ where:

159 1. $E$ is a denumerable set of events;

160 2. $< \subseteq (E \times E)$ is an irreflexive relation, called the flow relation;

161 3. $\# \subseteq (E \times E)$ is a symmetric relation, called the conflict relation.
<footnote>Note that the flow relation is not required to be transitive, nor acyclic (its reflexive and transitive closure is just a preorder, not necessarily a partial order). Intuitively, the flow relation represents a possible direct causality between two events. Moreover, in a FES the conflict relation is not required to be irreflexive nor hereditary; indeed, FESs may exhibit self-conflicting events, as well as disjunctive causality (an event may have conflicting causes).</footnote>

<footnote>Any PES $S = (E, \leq, \#)$ may be regarded as a FES, with $<$ given by $<$ (the strict ordering) or by the covering relation of $\leq$.</footnote>

<footnote>We now recall the definition of configuration for event structures. Intuitively, a configuration is a set of events having occurred at some stage of the computation. Thus, the semantics of an event structure $S$ is given by its poset of configurations ordered by set inclusion, where $\mathcal{X}_1 \subset \mathcal{X}_2$ means that $S$ may evolve from $\mathcal{X}_1$ to $\mathcal{X}_2$.</footnote>

<footnote>**Definition 3.3 (PES configuration).** Let $S = (E, \leq, \#)$ be a prime event structure. A configuration of $S$ is a finite subset $\mathcal{X}$ of $E$ such that:</footnote>

<footnote n="1">1. $\mathcal{X}$ is downward-closed: $e' \leq e \in \mathcal{X} \Rightarrow e' \in \mathcal{X}$;</footnote>

<footnote n="2">2. $\mathcal{X}$ is conflict-free: $\forall e, e' \in \mathcal{X}, \neg(e \# e')$.</footnote>

<footnote>The definition of configuration for FESs is slightly more elaborated. For a subset $\mathcal{X}$ of $E$, let $\mathcal{X}'$ be the restriction of the flow relation to $\mathcal{X}$ and $\mathcal{X}'^*$ be its transitive and reflexive closure.</footnote>

<footnote>**Definition 3.4 (FES configuration).** Let $S = (E, <, \#)$ be a flow event structure. A configuration of $S$ is a finite subset $\mathcal{X}$ of $E$ such that:</footnote>

<footnote n="1">1. $\mathcal{X}$ is downward-closed up to conflicts: $e' < e \in \mathcal{X}, e' \notin \mathcal{X} \Rightarrow \exists e'' \in \mathcal{X}. e' \# e'' < e$;</footnote>

<footnote n="2">2. $\mathcal{X}$ is conflict-free: $\forall e, e' \in \mathcal{X}, \neg(e \# e')$;</footnote>

<footnote n="3">3. $\mathcal{X}$ has no causality cycles: the relation $\mathcal{X}'$ is a partial order.</footnote>

<footnote>Condition (2) is the same as for prime event structures. Condition (1) is adapted to account for the more general – non-hereditary – conflict relation. It states that any event appears in a configuration with a “complete set of causes”. Condition (3) ensures that any event in a configuration is actually reachable at some stage of the computation.</footnote>

<footnote>If $S$ is a prime or flow event structure, we denote by $C(S)$ its set of configurations. Then, the domain of configurations of $S$ is defined as follows:</footnote>

<footnote>**Definition 3.5 (ES configuration domain).** Let $S$ be a prime or flow event structure with set of configurations $C(S)$. The domain of configurations of $S$ is the partially ordered set $\mathcal{D}(S)=_{\text{def}}(C(S), \subseteq)$.</footnote>

<footnote>We recall from [9] a useful characterisation for configurations of FESs, which is based on the notion of proving sequence, defined as follows:</footnote>
**Definition 3.6 (Proving sequence).** Given a flow event structure $S = (E, <, \#)$, a proving sequence in $S$ is a sequence $e_1, \cdots, e_n$ of distinct non-conflicting events (i.e. $i \neq j \Rightarrow e_i \neq e_j$ and $\neg(e_i \# e_j)$ for all $i, j$) satisfying:

$$ \forall i \le n \forall e \in E : \quad e < e_i \Rightarrow \exists j < i. \quad \text{either } e = e_j \text{ or } e \# e_j < e_i $$

Note that any prefix of a proving sequence is itself a proving sequence.

We have the following characterisation of configurations of FESs in terms of proving sequences.

**Proposition 3.7 (Representation of FES configurations as proving sequences [9]).**
Given a flow event structure $S = (E, <, \#)$, a subset $\mathcal{X}$ of $E$ is a configuration of $S$ if and only if it can be enumerated as a proving sequence $e_1; \cdots; e_n$.

Since PESs may be viewed as particular FESs, we may use Definition 3.6 and Proposition 3.7 both for the FESs associated with networks (see Sections 5) and for the PESs associated with global types (see Section 7). Note that for a PES the condition of Definition 3.6 simplifies to

$$ \forall i \le n \forall e \in E : \quad e < e_i \Rightarrow \exists j < i. \quad e = e_j $$

To conclude this section, we recall from [17] the definition of downward surjectivity (or downward-onto, as it was called there), a property that is required for partial functions between two FESs in order to ensure that they preserve configurations. We will make use of this property in Section 5.

**Definition 3.8 (Downward surjectivity).** Let $S_i = (E_i, <_i, \#)_i$, be a flow event structure, $i = 0, 1$. Let $e_i, e'_i$ range over $E_i, i = 0, 1$. A partial function $f : E_0 \to_* E_1$ is downward surjective if it satisfies the condition:

$$ e_1 <_1 f(e_0) \implies \exists e'_0 \in E_0. \quad e_1 = f(e'_0) $$

## 4. Event Structure Semantics of Processes

In this section, we define an event structure semantics for processes, and show that the obtained event structures are PESs. This semantics will be the basis for defining the ES semantics for networks in Section 5. We start by introducing process events, which are non-empty sequences of actions.

**Definition 4.1 (Process event).** Process events $\eta, \eta'$, also called p-events, are defined by:

$$ \eta ::= \pi \mid \pi \cdot \eta \qquad \pi \in \{\text{p!}\lambda, \text{p?}\lambda \mid \text{p} \in \text{Part}, \lambda \in \text{Msg}\} $$

We denote by $\mathcal{PE}$ the set of p-events, and by $|\eta|$ the length of the sequence of actions in the p-event $\eta$.
Let $\zeta$ denote a (possibly empty) sequence of actions, and $\sqsubseteq$ denote the prefix ordering on such sequences. Each p-event $\eta$ may be written either in the form $\eta = \pi \cdot \zeta$ or in the form $\eta = \zeta \cdot \pi$. We shall feel free to use any of these forms. When a p-event is written as $\eta = \zeta \cdot \pi$, then $\zeta$ may be viewed as the *causal history* of $\eta$, namely the sequence of past actions that must have happened in the process for the last action $\pi$ to be able to happen.

We define the *action* of a p-event to be its last action:

$$ \mathrm{act}(\zeta \cdot \pi) = \pi $$

**Definition 4.2 (Causality and conflict relations on process events).** The causality relation $\leq$ and the conflict relation $\#$ on the set of p-events $\mathcal{PE}$ are defined by:

$$ 223 \qquad 1. \ \eta \sqsubseteq \eta' \Rightarrow \eta \leq \eta'; $$

$$ 224 \qquad 2. \ \pi \neq \pi' \Rightarrow \zeta \cdot \pi \cdot \zeta' \# \zeta \cdot \pi' \cdot \zeta''. $$

**Definition 4.3 (Event structure of a process).** The event structure of process $P$ is the triple

$$ S^P(P) = (\mathcal{PE}(P), \leq_P, \#_P) $$

where:

$226 \qquad 1. \ \mathcal{PE}(P) \subseteq \mathcal{PE}$ is the set of non-empty sequences of labels along the nodes and edges of a path from the root to an edge in the tree of $P$;

$228 \qquad 2. \ \leq_P$ is the restriction of $\leq$ to the set $\mathcal{PE}(P)$;

$229 \qquad 3. \ \#_P$ is the restriction of $\#$ to the set $\mathcal{PE}(P)$.

It is easy to see that $\#_P = (\mathcal{PE}(P) \times \mathcal{PE}(P)) \setminus (\leq_P \cup \geq_P)$. In the following we shall feel free to drop the subscript in $\leq_P$ and $\#_P$.

Note that the set $\mathcal{PE}(P)$ may be denumerable, as shown by the following example.

$$ 233 \qquad \textbf{Example 4.4.} \quad \text{If } P = q!\lambda; P \oplus q!\lambda', \text{ then } \mathcal{PE}(P) = \underbrace{\{q!\lambda \cdots q!\lambda \mid n \geq 1\}}_{n} \cup \underbrace{\{q!\lambda \cdots q!\lambda' \cdot q!\lambda' \mid n \geq 0\}}_{n} $$

**Theorem 4.5.** Let $P$ be a process. Then $S^P(P)$ is a prime event structure.

**Proof** We show that $\leq$ and $\#$ satisfy Properties 2 and 3 of Definition 3.1. Reflexivity, transitivity and antisymmetry of $\leq$ follow from the corresponding properties of $\sqsubseteq$. As for irreflexivity and symmetry of $\#$, they follow from Clause 2 of Definition 4.2 and the corresponding properties of inequality. To show conflict hereditariness, suppose that $\eta \# \eta' \leq \eta''$. From Clause 2 of Definition 4.2 there are $\pi, \pi', \zeta, \zeta'$ and $\zeta''$ such that $\pi \neq \pi'$ and $\eta = \zeta \cdot \pi \cdot \zeta'$ and $\eta' = \zeta \cdot \pi' \cdot \zeta''$. From $\eta' \leq \eta''$ we derive that $\eta'' = \zeta \cdot \pi' \cdot \zeta'' \cdot \zeta_1$ for some $\zeta_1$. Therefore $\eta \# \eta''$, again from Clause 2.
242 **5. Event Structure Semantics of Networks**

In this section we define the ES semantics of networks and show that the result-
ing ESs, which we call *network ESs*, are FESs. We also show that when the network
is binary, then the obtained FES is a PES. The formal treatment involves defining
the set of potential events of network ESs, which we call *network events*, as well as
introducing the notion of *causal set* of a network event and the notion of *narrowing*
of a set of network events. This will be the subject of Section 5.1.

In Section 5.2, we first prove some properties of the conflict relation in network
ESs. Then, we come back to causal sets and we show that they are always finite and
that each configuration includes a unique causal set for each of its network events.
We also discuss the relationship between causal sets and prime configurations,
which are specific configurations that are in 1-1 correspondence with network events
in ESs. Finally, we define a notion of projection of network events on participants,
yielding p-events, and prove that this projection (extended to sets of network events)
is downward surjective and preserves configurations.

The proofs omitted in this section can be found in Appendix A.

258 **5.1. Definitions and Main Properties**

We start by defining network events, the potential events of network ESs. Since
these events represent communications between two network participants **p** and **q**,
they should be pairs of *dual p-events*, namely, of p-events emanating respectively
from **p** and **q**, which have both dual actions and dual causal histories.

Formally, to define network events we need to specify the *location* of p-events,
namely the participant to which they belong:

**Definition 5.1 (Located event).** We call located event a *p-event* η pertaining to a par-
ticipant **p**, written **p** :: η.

As hinted above, network events should be pairs of dual located events $p :: \zeta \cdot \pi$
and $q :: \zeta' \cdot \pi'$ with matching actions $\pi$ and $\pi'$ and matching histories $\zeta$ and $\zeta'$.
To formalise the matching condition, we first define the projections of p-events on
participants, which yield sequences of *undirected actions* of the form $!\lambda$ and $?\lambda$, or the
empty sequence $\epsilon$. Then we introduce a notion of duality between located events,
based on a notion of duality between undirected actions.

Let $\vartheta$ range over $!\lambda$ and $?\lambda$, and $\Theta$ range over (possibly empty) sequences of $\vartheta$'s.

**Definition 5.2 (Projection of p-events on participants).** The duality of undirected
on a participant **p**, written $\eta \vdash p$, is defined by:

$$
\[
q!\lambda \vdash p = \begin{cases} !\lambda & \text{if } p = q \\ \epsilon & \text{otherwise} \end{cases} \qquad q?\lambda \vdash p = \begin{cases} ?\lambda & \text{if } p = q \\ \epsilon & \text{otherwise} \end{cases}
\]
\[
(\pi \cdot \eta) \vdash p = \pi \vdash p \cdot \eta \vdash p
\]
$$

**Definition 5.3 (Duality of undirected action sequences).** The duality of undirected action sequences, written $\Theta \bowtie \Theta'$, is the symmetric relation induced by:

$$
\epsilon \bowtie \epsilon \qquad \Theta \bowtie \Theta' \Rightarrow !\lambda \cdot \Theta \bowtie ?\lambda \cdot \Theta'
$$
**Definition 5.4 (Duality of located events).** Two located events $p :: \eta, q :: \eta'$ are dual, written $p :: \eta \bowtie q :: \eta'$, if $\eta \upharpoonright q \bowtie \eta' \upharpoonright p$ and $pt(\text{act}(\eta)) = q$ and $pt(\text{act}(\eta')) = p$.

276 Dual located events may be sequences of actions of different length. For instance
277 $p :: q!\lambda \cdot r!\lambda' \bowtie r :: p?\lambda'$ and $p :: q!\lambda \bowtie q :: r!\lambda' \cdot p?\lambda$.

**Definition 5.5 (Network event).** Network events $v, v'$, also called n-events, are un-
ordered pairs of dual located events, namely:

$$
v ::= \{p :: \eta, q :: \eta'\} \quad \text{where} \quad p :: \eta \bowtie q :: \eta'
$$

We denote by $\mathcal{N}\mathcal{E}$ the set of n-events.

We define the communication of the event $v$, notation $cm(v)$, by $cm(v) = pq\lambda$ if $v = \{p :: \zeta \cdot q!\lambda, q :: \zeta' \cdot p?\lambda\}$ and we say that the n-event $v$ represents the communication $pq\lambda$. We also define the set of locations of an n-event to be $\text{loc}(\{p :: \eta, q :: \eta'\}) = \{p, q\}$.

It is handy to have a notion of occurrence of a located event in a set of network
283 events:

**Definition 5.6.** A located event $p :: \eta$ occurs in a set $E$ of n-events, notation $p :: \eta \in E$, if $p :: \eta \in v$ and $v \in E$ for some $v$.

We define now the flow and conflict relations on network events. While the
flow relation is the expected one (a network event inherits the causality from its
constituent processes), the conflict relation is more subtle, as it can arise also between
network events with disjoint sets of locations.

In the following definition we use $|\Theta|$ to denote the length of the sequence $\Theta$.

**Definition 5.7 (Flow and conflict relations on n-events).** The flow relation < and the conflict relation # on the set of n-events $\mathcal{N}\mathcal{E}$ are defined by:

1. $v < v'$ if $p :: \eta \in v \& p :: \eta' \in v' \& \eta < \eta'$;

2. $v \# v'$ if

(a) either $p :: \eta \in v \& p :: \eta' \in v' \& \eta \# \eta'$;

(b) or $p :: \eta \in v \& q :: \eta' \in v' \& p \neq q \& |\eta \upharpoonright q| = |\eta' \upharpoonright p| \& \neg(\eta \upharpoonright q \bowtie \eta' \upharpoonright p)$.

Two n-events are in conflict if they share a participant with conflicting p-events (Clause (2a)) or if some of their participants have communicated with each other in the past in incompatible ways (Clause (2b)), as illustrated by the n-events $v$ and $v'$ in Example 5.8 (Point 3). Observe that in Clause (2b) the condition $|\eta \upharpoonright q| = |\eta' \upharpoonright p|$ is needed if we want to check duality of the two projections. Without this condition we could get unwanted conflicts, for instance between $v = \{p :: q!\lambda, q :: p?\lambda\}$ and $v' = \{p :: q!\lambda \cdot q!\lambda', q :: p?\lambda \cdot p?\lambda'\}$. Removing this condition and checking duality only up to the length of the shortest projection would yield more conflicting events, as discussed in Example 5.8 (Point 3). Note also that the two clauses (2a) and (2b) are not exclusive, as shown in Example 5.8 (Point 4).
**Example 5.8.** This example illustrates the use of Definition 5.7 in various cases. It also shows that the flow and conflict relations may be overlapping on n-events.

1. Let $v = \{p :: q!\lambda_1 \cdot r!\lambda, r :: p?\lambda\} \text{ and } v' = \{p :: q!\lambda_2, q :: p?\lambda_2\}$. Then $v#v'$ by Clause (2a) since $q!\lambda_1 \cdot r!\lambda \# q!\lambda_2$. Note that $v#v'$ can be also deduced by Clause (2b), since $(q!\lambda_1 \cdot r!\lambda)\vdash q = !\lambda_1 \text{ and } p?\lambda_2 \vdash p = ?\lambda_2 \text{ and } |!\lambda_1| = |?\lambda_2| \text{ and } \neg(!\lambda_1 \nvDash ?\lambda_2)$.

2. Let $v$ be as in (1) and $v' = \{p :: q!\lambda_2 \cdot q!\lambda, q :: p?\lambda_2 \cdot p?\lambda\}$. Again, we can deduce $v#v'$ using Clause (2a), since $q!\lambda_1 \cdot r!\lambda \# q!\lambda_2 \cdot q!\lambda$. On the other hand, Clause (2b) does not apply in this case, since $(q!\lambda_1 \cdot r!\lambda)\vdash q = !\lambda_1$ and $(p?\lambda_2 \cdot p?\lambda)\vdash p = ?\lambda_2 \cdot ?\lambda$ and thus $|!\lambda_1| \neq |?\lambda_2 \cdot ?\lambda|$.

3. Let $v$ be as in (1) and $v' = \{q :: p?\lambda_2 \cdot s!\lambda, s :: q?\lambda\}$. Here $\text{loc}(v) \cap \text{loc}(v') = \emptyset$, so clearly Clause (2a) does not apply. On the other hand, $v#v'$ can be deduced by Clause (2b), since $(q!\lambda_1 \cdot r!\lambda)\vdash q = !\lambda_1$ and $(p?\lambda_2 \cdot s!\lambda)\vdash p = ?\lambda_2$ and $|!\lambda_1| = |?\lambda_2|$ and $\neg(!\lambda_1 \nvDash ?\lambda_2)$. Consider now $v'' = \{q :: p?\lambda_2 \cdot p?\lambda' \cdot s!\lambda, s :: q?\lambda\}$. Then we cannot deduce $v#v''$ in the same way because the two projections do not have the same length. However, we can deduce $v#v''' < v''$, where $v''' = \{p :: q!\lambda_2, q :: p?\lambda_2\}$. In other words, $v$ and $v''$ are in semantic conflict, as Proposition 5.22 shows, but not in the syntactic conflict # (the fact that semantic conflict is in general larger than syntactic conflict is common to all classes of ESs except PESs). We could have chosen to make the syntactic conflict larger by replacing Clause (2b) by the following alternative clause, where $\Theta, \Theta'$ are as in Definition 5.3 and $\sqsubseteq$ is the prefix ordering:

Clause (2b') or $p :: \eta \in v \& q :: \eta' \in v' \& p \neq q \& (\exists \Theta \sqsubseteq \eta \vdash q, \exists \Theta' \sqsubseteq \eta' \vdash p \cdot |\Theta| = |\Theta'| \& \neg(\Theta \nvDash \Theta'))$

With this alternative clause, we could deduce the syntactic conflict $v#v''$. However, in Definition 5.7 we chose to keep our definition of # stricter in order to have fewer syntactic conflicts to handle in examples and proofs.

4. Let $v$ be as in (1) and $v' = \{p :: q!\lambda_2 \cdot r!\lambda \cdot r!\lambda', r :: p?\lambda \cdot p?\lambda'\}$. In this case we have both $v < v'$ by Clause (1) and $v#v'$ by Clause (2a), namely, causality is inherited from participant $r$ and conflict from participant $p$.

We introduce now the notion of causal set of an n-event $v$ in a given set of events $Ev$. Intuitively, a causal set of $v$ in $Ev$ is a complete set of non-conflicting direct causes of $v$ which is included in $Ev$.

**Definition 5.9 (Causal set).** Let $v \in Ev \subseteq \mathcal{N}\mathcal{E}$. A set of n-events $E$ is a causal set of $v$ in $Ev$ if $E$ is a minimal subset of $Ev$ such that

1. $E \cup \{v\}$ is conflict-free and

2. $p :: \eta \in v$ and $\eta' < \eta$ imply $p :: \eta' \in E$.

Note that in the above definition, the conjunction of minimality and Clause (2) implies that, if $v' \in E$, then $v' < v$. Thus $E$ is a set of direct causes of $v$. Moreover, a causal set of an n-event cannot be included in another causal set of the same n-event, as this would contradict the minimality of the larger set. Hence, Definition 5.9 indeed formalises the idea that causal sets should be complete sets of compatible direct causes of a given n-event.
<footnote n="347">347 **Example 5.10.** Let $v_1 = \{\mathbf{p} :: q!\lambda_1 \cdot r!\lambda, r :: p?\lambda\}$ and $v_2 = \{\mathbf{p} :: q!\lambda_2 \cdot r!\lambda, r :: p?\lambda\}$. Then both $\{v_1\}$ and $\{v_2\}$ are causal sets of $v = \{r :: p?\lambda \cdot s!\lambda', s :: r?\lambda'\}$ in $Ev = \{v_1, v_2, v\}$. Note that $v_1 \# v_2$ and that neither $v_1$ nor $v_2$ has a causal set in $Ev$.</footnote>

<footnote n="350">350 Let us now consider also $v'_1 = \{\mathbf{p} :: q!\lambda_1, q :: p?\lambda_1\}$ and $v'_2 = \{\mathbf{p} :: q!\lambda_2, q :: p?\lambda_2\}$. Then $v$ still has the same causal sets $\{v_1\}$ and $\{v_2\}$ in $Ev' = \{v'_1, v'_2, v_1, v_2, v\}$, while each $v_i$, $i = 1, 2$, has the unique causal set $\{v'_i\}$ in $Ev'$, and each $v'_i$, $i = 1, 2$, has the empty causal set in $Ev'$.</footnote>

<footnote n="354">354 Finally, $v$ has infinitely many causal sets in $\mathcal{N}\mathcal{E}$. For instance, if for every natural number $n$ we let $v_n = \{\mathbf{p} :: q!\lambda_n \cdot r!\lambda, r :: p?\lambda\}$, then each $\{v_n\}$ is a causal set of $v$ in $\mathcal{N}\mathcal{E}$. Symmetrically, a causal set may cause infinitely many events in $\mathcal{N}\mathcal{E}$. For instance, the above causal sets $\{v_1\}$ and $\{v_2\}$ of $v$ could also act as causal sets for any $n$-event $v_n'' = \{r :: p?\lambda \cdot s!\lambda_n, s :: r?\lambda_n\}$ or, assuming the set of participants to be denumerable, for any event $v_n''' = \{r :: p?\lambda \cdot s_n!\lambda', s_n :: r?\lambda'\}$.</footnote>

<footnote n="360">360 When defining the set of events of a network ES, we want to prune out all the $n$-events that do not have a causal set in the set itself. The reason is that such $n$-events should not happen in the event structure of a network, although, when projected on their locations (see Definition 5.25), they would always give rise to $p$-events occurring in a configuration⁵. Example 5.14 should further clarify this point. This pruning is achieved by means of the following narrowing function.</footnote>

<footnote>**Definition 5.11 (Narrowing of a set of n-events).** The narrowing of a set $E$ of $n$-events, denoted by $n(E)$, is the greatest fixpoint of the function $f_E$ on sets of $n$-events defined by:</footnote>

<footnote n="366">366 $f_E(X) = \{v \in E \mid \exists E' \subseteq X. E'$ is a causal set of $v$ in $X\}$</footnote>

<footnote n="367">367 Note that we could not have taken $n(E)$ to be the least fixpoint of $f_E$ rather than its greatest fixpoint. Indeed, the least fixpoint of $f_E$ would be the empty set.</footnote>

<footnote>**Example 5.12.** The following two examples illustrate the notions of causal set and narrowing. Let</footnote>

<footnote n="368">368 $v_1 = \{r :: s?\lambda_1, s :: r!\lambda_1\}$, $v_2 = \{r :: s?\lambda_2, s :: r!\lambda_2\}$, $v_3 = \{\mathbf{p} :: r?\lambda_1, r :: s?\lambda_1 \cdot p!\lambda_1\}$, $v_4 = \{\mathbf{q} :: s?\lambda_2, s :: r!\lambda_2 \cdot q!\lambda_2\}$, $v_5 = \{\mathbf{p} :: r?\lambda_1 \cdot q!\lambda, q :: s?\lambda_2 \cdot p?\lambda\}$</footnote>

<footnote>Then $n(\{v_1, \dots, v_5\}) = \{v_1, \dots, v_4\}$, because a causal set for $v_5$ would need to contain both $v_3$ and $v_4$, but this is not possible, since $v_3 \# v_4$ by Clause (2b) of Definition 5.7. In fact $(s?\lambda_1 \cdot p!\lambda_1) \nvdash s = ?\lambda_1$ and $(r!\lambda_2 \cdot q!\lambda_2) \nvdash r = !\lambda_2$ and $|?\lambda_1| = |!\lambda_2|$ and $\neg(?\lambda_1 \succcurlyeq !\lambda_2)$. Let</footnote>

<footnote n="368">368 $v_1 = \{r :: s?\lambda_1, s :: r!\lambda_1\}$, $v_2 = \{r :: s?\lambda_2, s :: r!\lambda_2\}$, $v_3 = \{\mathbf{p} :: r?\lambda_1, r :: s?\lambda_1 \cdot p!\lambda_1\}$, $v_4 = \{\mathbf{p} :: r?\lambda_1 \cdot s?\lambda_2, s :: r!\lambda_2 \cdot p!\lambda_2\}$, $v_5 = \{\mathbf{p} :: r?\lambda_1 \cdot s?\lambda_2 \cdot q!\lambda, q :: p?\lambda\}$</footnote>

<footnote n="369">369 Here $n(\{v_1, \dots, v_5\}) = \{v_1, v_2, v_3\}$. Indeed, a causal set for $v_4$ would need to contain both $v_2$ and $v_3$, but this is not possible, since $v_2 \# v_3$ by Clause (2a) of Definition 5.7. In fact $s?\lambda_2 \# s?\lambda_1 \cdot p!\lambda_1$. Then, $v_5$ will also be pruned by the narrowing, since any causal set for $v_5$ should contain $v_4$.</footnote>

<footnote n="5">⁵In fact, every event of a PES occurs in a configuration.</footnote>
We can now finally define the event structure associated with a network. The intuition is that the events appearing in some configuration of the event structure should correspond exactly to the transitions executable in some state of the network.

**Definition 5.13 (Event structure of a network).** The event structure of network N is the triple

$$S^N(N) = (\mathcal{NE}(N), <_N, \#_N)$$

where:

1. $\mathcal{NE}(N) = n(\mathcal{CE}(N))$ with $\mathcal{CE}(N) = \{\{p :: \eta, q :: \eta'\} | p[[P]] \in N, q[[Q]] \in N, \eta \in \mathcal{PE}(P), \eta' \in \mathcal{PE}(Q), p :: \eta \rightleftharpoons q :: \eta'\}$

2. $<_N$ is the restriction of $<$ to the set $\mathcal{NE}(N)$;

3. $\#_N$ is the restriction of $\#$ to the set $\mathcal{NE}(N)$.

The set of n-events of the ES associated with a network N is the narrowing of its set of candidate n-events, $\mathcal{CE}(N)$, which contains all pairs of dual located events that may be constructed from two different components of N. We give now a simple example that justifies the use of the narrowing function for building the set of events of a network ES.

**Example 5.14.** Let $N = p[[q?\lambda \cdot r!\lambda']]] \parallel r[[p?\lambda']]]$. Then $\mathcal{CE}(N)$ contains the unique n-event $v = \{p :: q?\lambda \cdot r!\lambda', r :: p?\lambda'\}$. If we did not apply the narrowing function to $\mathcal{CE}(N)$, namely if we took $\mathcal{CE}(N)$ as the set of n-events for $S^N(N)$, then $\{v\}$ would be a possible configuration of $S^N(N)$, which is clearly wrong, since the network N does not have a corresponding transition. Instead, by applying the narrowing function to $\mathcal{CE}(N)$ we obtain $\mathcal{NE}(N) = n(\mathcal{CE}(N)) = \emptyset$, since the n-event $v$ has no causal set in $\mathcal{CE}(N)$, which is what we expect.

The set of n-events of a network ES can be infinite, as shown by the following example.

**Example 5.15.** Let P be as in Example 4.4, $Q = p?\lambda; Q + p?\lambda'$ and $N = p[[P]] \parallel q[[Q]]$. Then

$$\mathcal{NE}(N) = \left\{ \begin{array}{l} \underbrace{\{p :: q!\lambda \cdots q!\lambda, q :: p?\lambda \cdots p?\lambda\}}_{n} | n \ge 1 \\ \cup \\ \underbrace{\{p :: q!\lambda \cdots q!\lambda \cdot q!\lambda', q :: p?\lambda \cdots p?\lambda \cdot p?\lambda'\}}_{n} | n \ge 0 \end{array} \right\}$$

A simple variation of this example shows that even within the events of a network ES, an n-event $v$ may have an infinite number of causal sets. Let $v = \{r :: p?\lambda \cdot s!\lambda', s :: r?\lambda'\}$ be as in Example 5.10. Consider the network $N' = p[[P']]] \parallel q[[Q]] \parallel r[[R]] \parallel s[[S]]$, where $P' = q!\lambda; P' \oplus q!\lambda'; r!\lambda, Q$ is as above, $R = p?\lambda; s!\lambda'$ and $S = r?\lambda'$. Then $v$ has an infinite number of causal sets $E_n = \{v_n\}$ in $\mathcal{NE}(N')$, where

$$v_n = \{p :: q!\lambda \cdots q!\lambda \cdot q!\lambda' \cdot r!\lambda, r :: p?\lambda\}$$
On the other hand, a causal set may only cause a finite number of events in a network ES, since the number of branches in any choice is finite, as well as the number of participants in the network.

**Theorem 5.16.** Let N be a network. Then $S^N(N)$ is a flow event structure with an irreflexive conflict relation.

**Proof** The relation $<_N$ is irreflexive since $\eta < \eta'$ implies $v \neq v'$, where $\eta, \eta', v, v'$ are as in Definition 5.7(1). As for the conflict relation, note first that a conflict between an n-event and itself could not be derived by Clause (2b) of Definition 5.7, since the two located events of an n-event are dual by construction. Lastly, symmetry and irreflexivity of the conflict relation follow from the corresponding properties of conflict between p-events.

The fact that the conflict relation is irreflexive in our network FESs means that we do not exploit the possibility of self-conflicts offered by general FESs. This is due to the way we defined the set of events of our network FESs, using the narrowing function as discussed previously. We could have chosen an alternative definition, introducing additional self-conflicting events of a more liberal form<fnref n="6" /> which would have disappeared when building configurations (together with their successors having no other possible causes), as it was done for CCS in [10]. However, this would have resulted in much larger sets of events for network FESs, leading to more cumbersome examples and proofs. Our design choice here was to reduce the set of events of network FESs by introducing already some semantic constraints on their events (like duality and the existence of causal sets). It should be stressed, however, that the narrowing function does not exclude all non executable events, as shown by the FES in Example 5.20, which has three events, each of which has a causal set but none of which is executable.

Although they have an irreflexive conflict relation like PESs, our network FESs exhibit two important features which are not shared by PESs, namely non-hereditary conflict (as shown by the FES given in Figure 5, where the two conflicting events $v'_1$ and $v'_2$ have a common successor $v$) and causality cycles (as shown by the FES in Example 5.20, where there is a circular dependency among the three events $v_1, v_2$ and $v_3$).

Note that n-events with disjoint sets of locations may be related by the transitive closure of the flow relation, as illustrated by the next example, which also shows how n-events inherit the flow relation from the causality relation of their p-events.

**Example 5.17.** Let N be the network

$$p[[q!\lambda_1]] \parallel q[[p?\lambda_1;r!\lambda_2]] \parallel r[[q?\lambda_2;s!\lambda_3]] \parallel s[[r?\lambda_3]]$$

<footnote n="6">⁶For instance, we could have allowed events of the form {$p :: \eta, *$} to represent incomplete communications, and then prevented them from occurring by putting them in conflict with themselves. In this case, the event $v$ of Example 5.14 would have also been prevented from occurring because of its unique self-conflicting cause {$p :: q?\lambda, *$}, and we would not have needed the narrowing function.</footnote>
Then $\mathcal{S}^N(N)$ has three network events

$$v_1 = \{ \mathbf{p} \:: \mathbf{q}!\lambda_1, \mathbf{q} \:: \mathbf{p}\?\lambda_1 \} \quad v_2 = \{ \mathbf{q} \:: \mathbf{p}\?\lambda_1 \cdot \mathbf{r}\!\lambda_2, \mathbf{r} \:: \mathbf{q}\?\lambda_2 \} \quad v_3 = \{ \mathbf{r} \:: \mathbf{q}\?\lambda_2 \cdot \mathbf{s}\!\lambda_3, \mathbf{s} \:: \mathbf{r}\?\lambda_3 \}$$

The flow relation obtained by Definition 5.13 is: $v_1 < v_2$ and $v_2 < v_3$. These two flows are inherited from the causality relations within the process ESs associated with participants $\mathbf{q}$ and $\mathbf{r}$, respectively. The non-empty configurations are $\{v_1\}$, $\{v_1, v_2\}$ and $\{v_1, v_2, v_3\}$. Note that $\mathcal{S}^N(N)$ has only one proving sequence per configuration (which is the one given by the numbering of events).

Clearly, if a network is unary, then the set of events of its FES is empty. If a network is binary, then its FES may be turned into a PES by replacing $<$ with its reflexive and transitive closure $\prec$. To prove this result, we first show a property of n-events of binary networks. We say that an n-event $v$ is binary if the participants occurring in the p-events of $v$ are contained in $\text{loc}(v)$.

**Lemma 5.18.** Let $v$ and $v'$ be binary n-events with $\text{loc}(v) = \text{loc}(v')$. Then $v \# v'$ iff $\mathbf{p} \:: \eta \in v$ and $\mathbf{p} \:: \eta' \in v'$ imply $\eta \# \eta'$.

**Proposition 5.19.** Let $N = \mathbf{p}_1[[\mathbf{P}_1]] \parallel \mathbf{p}_2[[\mathbf{P}_2]]$ and $\mathcal{S}^N(N) = (\mathcal{N}\mathcal{E}(N), \prec_N, \#)$.
Then $n(\mathcal{C}\mathcal{E}(N)) = \mathcal{C}\mathcal{E}(N)$ and the structure $\mathcal{S}^*_N(N) = \text{def}(\mathcal{N}\mathcal{E}(N), \prec_N, \#)$ is a prime event structure.

**Proof** We first show that $n(\mathcal{C}\mathcal{E}(N)) = \mathcal{C}\mathcal{E}(N)$. By Definition 5.13(1)

$$\mathcal{C}\mathcal{E}(N) = \{\{\mathbf{p}_1 \:: \eta_1, \mathbf{p}_2 \:: \eta_2\} \mid \eta_1 \in \mathcal{P}\mathcal{E}(P_1), \eta_2 \in \mathcal{P}\mathcal{E}(P_2), \mathbf{p}_1 \:: \eta_1 \unlhd \mathbf{p}_2 \:: \eta_2\}$$

Let $\{\mathbf{p}_1 \:: \eta_1, \mathbf{p}_2 \:: \eta_2\} \in \mathcal{C}\mathcal{E}(N)$. Since $\mathbf{p}_1 \:: \eta_1 \unlhd \mathbf{p}_2 \:: \eta_2$ and all the actions in $\eta_1$ involve $\mathbf{p}_2$ and all the actions in $\eta_2$ involve $\mathbf{p}_1$, we know that $\eta_1$ and $\eta_2$ have the same length $n \ge 1$ and for each $i, 1 \le i \le n$, the prefixes of length $i$ of $\eta_1$ and $\eta_2$, written $\eta_1^i$ and $\eta_2^i$, must themselves be dual. Then $\{\mathbf{p}_1 \:: \eta_1^i, \mathbf{p}_2 \:: \eta_2^i\} \in \mathcal{C}\mathcal{E}(N)$ for each $i, 1 \le i \le n$, hence $\{\mathbf{p}_1 \:: \eta_1, \mathbf{p}_2 \:: \eta_2\}$ has a causal set in $\mathcal{C}\mathcal{E}(N)$.

We prove now that the reflexive and transitive closure $\prec_N^*$ of $\prec_N$ is a partial order. Since by definition $\prec_N^*$ is a preorder, we only need to show that it is antisymmetric. Define the length of an n-event $v = \{\mathbf{p}_1 \:: \eta_1, \mathbf{p}_2 \:: \eta_2\}$ to be $\text{length}(v) = \text{def} | \eta_1 | + |\eta_2|$ (where $|\eta|$ is the length of $\eta$). Let now $v, v' \in \mathcal{N}\mathcal{E}(N)$, with $v = \{\mathbf{p}_1 \:: \eta_1, \mathbf{p}_2 \:: \eta_2\}$ and $v' = \{\mathbf{p}_1 \:: \eta'_1, \mathbf{p}_2 \:: \eta'_2\}$. By definition $v \prec_N v'$ implies $\eta_i < \eta'_i$ for some $i = 1, 2$, which in turn implies $|\eta_i| < |\eta'_i|$. As observed above, $\eta_1$ and $\eta_2$ must have the same length, and so must $\eta'_1$ and $\eta'_2$. This means that if $v \prec_N v'$ then $\text{length}(v) = |\eta_1| + |\eta_2| < |\eta'_1| + |\eta'_2| = \text{length}(v')$. From this we can conclude that if $v \prec_N^* v'$ and $v' \prec_N^* v$, then necessarily $v = v'$.

Finally we show that the relation $\#^*$ satisfies the required properties. By Theorem 5.16 we only need to prove that $\#$ is hereditary. Let $v$ and $v'$ be as above. If $v \#^* v'$, then by Lemma 5.18 $\eta_1 \#^* \eta'_1$ and $\eta_2 \#^* \eta'_2$. Let now $v'' = \{\mathbf{p}_1 \:: \eta''_1, \mathbf{p}_2 \:: \eta''_2\}$. If $v' \prec_N^* v''$, this means that there exist $v_1, \dots, v_n$ such that $v' \prec_N v_1 \dots \prec_N v_n = v''$. We prove by induction on $n$ that $v \#^* v''$. For $n = 1$ we have $v' \prec_N v''$. Then by Clause (1) of Definition 5.13 we have $\eta'_j < \eta''_j$ for some $j \in \{1, 2\}$. Since $\eta_i \#^* \eta'_i$ for all $i \in \{1, 2\}$ and $\#$ is hereditary on p-events, we deduce $\eta_j \#^* \eta''_j$, which implies $v \#^* v''$. Suppose now $n > 1$. By induction $v \#^* v_{n-1}$. Since $v_{n-1} \prec_N v_n = v''$ we then obtain $v \#^* v''$ by the same argument as in the base case.
If a network has more than two participants, then the duality requirement on its n-events is not sufficient to ensure the absence of circular dependencies<fnref n="7" />. For instance, in the following ternary network (which may be viewed as representing the 3-philosopher deadlock) the relation <* is not a partial order.

**Example 5.20.** Let N be the network

$$p[[r?\lambda; q!\lambda' ]] \parallel q[[p?\lambda'; r!\lambda' ]] \parallel r[[q?\lambda''; p!\lambda ]]$$

Then $S^N(N)$ has three n-events

$$v_1 = \{p :: r?\lambda, r :: q?\lambda'' \cdot p!\lambda\} \qquad v_2 = \{p :: r?\lambda \cdot q!\lambda', q :: p?\lambda'\}$$

$$v_3 = \{q :: p?\lambda' \cdot r!\lambda'', r :: q?\lambda''\}$$

By Definition 5.13(1) we have $v_1 < v_2 < v_3$ and $v_3 < v_1$. The only configuration of $S^N(N)$ is the empty configuration, because the only set of n-events that satisfies downward-closure up to conflicts is $X = \{v_1, v_2, v_3\}$, but this is not a configuration because $<_X$ is not a partial order (recall that $<_X$ is the restriction of $<$ to X) and hence the condition (3) of Definition 3.4 is not satisfied.

## 5.2. Further Properties

In this subsection, we first prove two properties of the conflict relation in network ESs: non disjoint n-events are always in conflict, and conflict induced by Clause (2b) of Definition 5.7 is semantically inherited. We then discuss the relationship between causal sets and prime configurations and prove two further properties of causal sets, which are shared with prime configurations<fnref n="8" />: finiteness, and the existence of a causal set for each event in a configuration. Finally, observing that the FES of a network may be viewed as the product of the PESs of its processes, we proceed to prove a classical property for ES products, namely that their projections on their components preserve configurations. To this end, we define a projection function from n-events to participants, yielding p-events, and we show that configurations of a network ES project down to configurations of the PESs of its processes.

Let us start with the conflict properties. By definition, two n-events intersect each other if and only if they share a located event $p :: \eta$. Otherwise, the two n-events are disjoint. Note that if $p :: \eta \in (v \cap v')$, then $\text{loc}(v) = \text{loc}(v') = \{p, q\}$, where $q = \text{pt}(\text{act}(\eta))$. The next proposition establishes that two distinct intersecting n-events in $\mathcal{NE}$ are in conflict.

**Lemma 5.21 (Sharing of located events implies conflict).** If $v, v' \in \mathcal{NE}$ and $v \neq v'$ and $(v \cap v') \neq \emptyset$, then $v \# v'$.

Although conflict is not hereditary in FESs, we prove that a conflict due to incompatible mutual projections (i.e., a conflict derived by Clause (2b) of Definition 5.7) is semantically inherited. Let $\vartheta \searrow n$ denote the prefix of length $n$ of $\vartheta$.

<footnote n="7">⁷This is a well-known issue in multiparty session types, which motivated the introduction of global types in [39], see Section 6.</footnote>

<footnote n="8">⁸A prime configuration is a configuration with a unique maximal element, its culminating event.</footnote>
<footnote>**Proposition 5.22 (Semantic conflict hereditariness).** Let $\mathbf{p} :: \eta \in v$ and $\mathbf{q} :: \eta' \in v'$ with $\mathbf{p} \neq \mathbf{q}$. Let $n = \min\{|\eta\mathbf{p}\mathbf{q}|, |\eta'\mathbf{p}'\mathbf{p}|\}$. If $\neg((\eta\mathbf{p}\mathbf{q})\searrow n \bowtie (\eta'\mathbf{p}'\mathbf{p})\searrow n)$, then there exists no configuration $\mathcal{X}$ such that $v, v' \in \mathcal{X}$.</footnote>

<footnote>**Proof** Suppose ad absurdum that $\mathcal{X}$ is a configuration such that $v, v' \in \mathcal{X}$. If $|\eta \mathbf{p} \mathbf{q}| = |\eta' \mathbf{p}' \mathbf{p}|$ then $v \# v'$ by Definition 5.7(2b) and we reach immediately a contradiction. So, assume $|\eta \mathbf{p} \mathbf{q}| > |\eta' \mathbf{p}' \mathbf{p}| = n$. This means that $|\eta| > 1$ and thus there exists a non-empty causal set $E_v$ of $v$ such that $E_v \subseteq \mathcal{X}$. Let $\eta_0 < \eta$ be such that $|\eta_0 \mathbf{p} \mathbf{q}| = |\eta' \mathbf{p}' \mathbf{p}| = n$. By definition of causal set, there exists $v_0 \in E_v$ such that $\mathbf{p} :: \eta_0 \in v_0$. By Definition 5.7(2b) we have then $v_0 \# v'$, contradicting the fact that $\mathcal{X}$ is conflict-free.</footnote>

<footnote>We prove now two further properties of causal sets. For the reader familiar with ESs, the notion of causal set may be reminiscent of that of *prime configuration* [60], which similarly consists of a complete set of causes for a given event⁹. However, there are some important differences: the first is that a causal set does not include the event it causes, unlike a prime configuration. The second is that a causal set only contains direct causes of an event, and thus it is not downward-closed up to conflicts, as opposed to a prime configuration. The last difference is that, while a prime configuration uniquely identifies its caused event, a causal set may cause different events, as shown in Example 5.10.</footnote>

<footnote>A common feature of prime configurations and causal sets is that they are both finite. For causal sets, this is implied by minimality together with Clause (2) of Definition 5.9, as shown by the following proposition.</footnote>

<footnote>**Proposition 5.23.** Let $v \in E_v \subseteq \mathcal{N}\mathcal{E}$. If $E$ is a causal set of $v$ in $E_v$, then $E$ is finite.</footnote>

<footnote>**Proof** Suppose $v = \{\mathbf{p} :: \eta, \mathbf{q} :: \eta'\}$. We show that $|E| \leq |\eta| + |\eta'| - 2$, where $|E|$ is the cardinality of $E$. By Condition (2) of Definition 5.9, for each $\eta_0 < \eta$ and $\eta'_0 < \eta'$ there must be $v_0, v'_0 \in E$ such that $\mathbf{p} :: \eta_0 \in v_0$ and $\mathbf{q} :: \eta'_0 \in v'_0$. Note that $v_0$ and $v'_0$ could possibly coincide. Moreover, there cannot be $v' \in E$ such that $\mathbf{p} :: \eta_0 \in v' \neq v_0$ or $\mathbf{q} :: \eta'_0 \in v' \neq v'_0$, since this would contradict the minimality of $E$ (and also its conflict-freeness, since by Lemma 5.21 we would have either $v' \# v_0$ or $v' \# v'_0$). Hence the number of events in $E$ is at most $(|\eta| - 1) + (|\eta'| - 1)$.</footnote>

<footnote>A key property of causal sets, which is again shared with prime configurations, is that each configuration includes a unique causal set for each n-event in the configuration.</footnote>

<footnote>**Lemma 5.24.** If $\mathcal{X}$ is a configuration of $S^N(N)$ and $v \in \mathcal{X}$, then there is a unique causal set $E$ of $v$ such that $E \subseteq \mathcal{X}$.</footnote>

<footnote>In the remainder of this section we show that projections of n-event configurations give p-event configurations. We start by formalising the projection function of n-events on participants, which yields p-events, and showing that it is downward surjective.</footnote>

<footnote n="9">⁹In PESs, the prime configuration associated with an event is unique, while it is not unique in FESs and more generally in Stable ESs, just like a causal set.</footnote>
**Definition 5.25 (Projection of n-events on participants).**

$$ \mathrm{proj}_{\mathrm{p}}(v) = \begin{cases} \eta & \text{if } \mathrm{p} :: \eta \in v, \\ \mathrm{undefined} & \text{otherwise.} \end{cases} $$

The projection function $\mathrm{proj}_{\mathrm{p}}(\cdot)$ is extended to sets of n-events in the obvious way:

$$ \mathrm{proj}_{\mathrm{p}}(X) = \{\eta \mid \exists v \in X. \mathrm{proj}_{\mathrm{p}}(v) = \eta\} $$

**Example 5.26.** Let {$v_1, v_2, v_3$} be the configuration defined in Example 5.17. We get

$$ \mathrm{proj}_{\mathrm{q}}(\{v_1, v_2, v_3\}) = \{\mathrm{p}?\lambda_1, \mathrm{p}?\lambda_1 \cdot \mathrm{r}?\lambda_2\} $$

**Example 5.27.** Let $N$ and $v$ be as in Example 5.14. As observed there, if we did not apply narrowing the set of events of $S^N(N)$ would be the singleton {$v$}, which would also be a configuration of $S^N(N)$. However, $\mathrm{proj}_{\mathrm{p}}(v) = \{\mathrm{q}?\lambda \cdot \mathrm{r}?\lambda'\}$ would not be a configuration in $S^P(P)$, since it would contain the event $\mathrm{q}?\lambda \cdot \mathrm{r}?\lambda'$ without its cause $\mathrm{q}?\lambda$.

Narrowing ensures that each projection of the set of n-events of a network FES on one of its participants is downward surjective (according to Definition 3.8).

**Proposition 5.28 (Downward surjectivity of projections).**

Let $S^N(N) = (\mathcal{NE}(N), <_N, #_N)$ and $S^P(P) = (\mathcal{PE}(P), \leq_P, #_P)$ and $\mathrm{p}[[P]] \in N$. Then the partial function $\mathrm{proj}_{\mathrm{p}}: \mathcal{NE}(N) \to \mathcal{PE}(P)$ is downward surjective.

**Proof** As mentioned already in Section 3, any PES $S = (E, \leq, #)$ may be viewed as a FES, with $<$ given by $<$ (the strict ordering underlying $\leq$). Let $\eta \in \mathcal{PE}(P)$ and $v \in \mathcal{NE}(N)$. Then the property we need to show is:

$$ \eta <_P \mathrm{proj}_{\mathrm{p}}(v) \implies \exists v' \in \mathcal{NE}(N) . \eta = \mathrm{proj}_{\mathrm{p}}(v') $$

Note that $\eta <_P \mathrm{proj}_{\mathrm{p}}(v)$ implies $\mathrm{proj}_{\mathrm{p}}(v) = \eta \cdot \eta'$ for some $\eta'$. Recall that $\mathcal{NE}(N) = n(\mathcal{CE}(N))$, where $n(\cdot)$ is the narrowing function (Definition 5.11).

By definition of narrowing, $\mathrm{p} :: \eta \cdot \eta' \in \mathcal{NE}(N)$ implies that there is $E \subseteq \mathcal{NE}(N)$ such that $E$ is a causal set of $v$ in $\mathcal{NE}(N)$. Therefore $\mathrm{p} :: \eta \cdot \eta' \in v$ implies $\mathrm{p} :: \eta \in E$ and so $\mathrm{p} :: \eta \in \mathcal{NE}(N)$, which is what we wanted to show.

**Theorem 5.29 (Projection of n-events preserves configurations).** If $\mathrm{p}[[P]] \in N$, then $X \in C(S^N(N))$ implies $\mathrm{proj}_{\mathrm{p}}(X) \in C(S^P(P))$.

**Proof** Clearly, $\mathrm{proj}_{\mathrm{p}}(X)$ is conflict-free. We show that it is also downward-closed. If $v \in X$, by Lemma 5.24 there is a causal set $E$ of $v$ such that $E \subseteq X$. If $\mathrm{p} :: \eta \in v$ and $\eta' < \eta$, by Definition 5.9 there is $v' \in E$ such that $\mathrm{p} :: \eta' \in v'$. We conclude that $v' \in X$, and therefore $\eta' \in \mathrm{proj}_{\mathrm{p}}(X)$.

Notice that the reverse of Theorem 5.29 is not true, namely $\mathrm{p}[[P]] \in N$ does not imply that each configuration of $C(S^P(P))$ can be obtained by projecting some
557 configuration of $C(S^N(N))$ on p. Consider for instance the network $N = p[[q?\lambda]]$. Then $\{q?\lambda\} \in C(S^P(P))$, while $C(S^N(N)) = \emptyset$.

558 The reader may wonder why our ES semantics for sessions is not cast in categorical terms, like classical ES semantics for process calculi [60, 17], where process constructions arise as categorical constructions (e.g., parallel composition arises as a categorical product). In fact, a categorical formulation of our semantics would not be possible, due to our two-level syntax for processes and networks, which does not allow networks to be further composed in parallel. However, it should be clear that our construction of a network FES from the process PESs of its components is a form of parallel composition, and the properties expressed by Proposition 5.28 and Theorem 5.29 give some evidence that this construction satisfies the conditions usually required for a categorical product of ESs.

### 6. Global Types

570 This section is devoted to our type system for multiparty sessions. Global types describe the communication protocols involving all session participants. Usually, 571 global types are projected into local types and typing rules are used to derive local 572 types for processes [39, 19, 40]. The simplicity of our calculus allows us to project 573 directly global types into processes and to have exactly one typing rule, see Figures 2 574 and 3. This section is split in two subsections.

575 The first subsection presents the projection of global types onto processes, together 576 with the proof of its soundness. Moreover it introduces a *boundedness* condition on 577 global types, which is crucial for our type system to ensure progress.

578 The second subsection presents the type system, as well as an LTS for global types.

579 Lastly, the properties of Subject Reduction, Session Fidelity and Progress are shown.

580 The omitted proofs can be found in Appendix B.

#### 6.1. Well-formed Global Types

581 Global types are built from choices among communications.

**Definition 6.1 (Global types).** *Global types* $G$ *are defined by:*

$$ G ::=^{\text{coind}} p \to q : \coprod_{i \in I} \lambda_i; G_i \mid \text{End} $$

582 where *I* is not empty, $\lambda_h \neq \lambda_k$ for all $h, k \in I, h \neq k$, i.e. *messages in choices are all different*.

583 As for processes, $::=^{\text{coind}}$ indicates that global types are defined coinductively. Again, we focus on *regular* terms. Since also processes are defined coinductively this allows for a simpler definition of projection, see Figure 2.

584 The type $p \to q : \coprod_{i \in I} \lambda_i; G_i$ formalises a protocol which starts with the communication of a message $\lambda_k$ from $p$ to $q$, for some $k \in I$, and then, depending on which $\lambda_k$ was chosen by $p$, continues as $G_k$.

585 When *I* is a singleton, a choice $p \to q : \coprod_{i \in I} \lambda_i; G_i$ will be rendered simply as $p \xrightarrow{\lambda} q; G$. When *I* contains only two elements, as for processes we will use the binary choice notation $p \to q : (\lambda_1; G_1 \coprod \lambda_2; G_2)$. Trailing End types will be omitted.
$$ G \upharpoonright r = 0 \text{ if } r \notin \text{part}(G) $$
$$ (p \to q : \boxplus_{i \in I} \lambda_i; G_i) \upharpoonright r = \begin{cases} \sum_{i \in I} p?\lambda_i; G_i \upharpoonright r & \text{if } r = q, \\ \bigoplus_{i \in I} q!\lambda_i; G_i \upharpoonright r & \text{if } r = p, \\ G_1 \upharpoonright r & \text{if } r \notin \{p, q\} \text{ and } r \in \text{part}(G_1) \text{ and} \\ G_i \upharpoonright r = G_1 \upharpoonright r \text{ for all } i \in I \end{cases} $$

<caption>**Figure 2:** Projection of global types onto participants.</caption>

Global types may be viewed as trees whose internal nodes are decorated by pq, leaves by End, and edges by messages $\lambda$. Given a global type, the sequences of decorations of nodes and edges on the path from the root to an edge in the tree of the global type are traces, in the sense of Definition 2.3. We denote by $\text{Tr}^+(G)$ the set of traces of $G$. By definition, $\text{Tr}^+(\text{End}) = \emptyset$ and each trace in $\text{Tr}^+(G)$ is non-empty.

The set of participants of a global type $G$, part($G$), is defined to be the union of the sets of participants of all its traces, namely

$$ \text{part}(G) = \bigcup_{\sigma \in \text{Tr}^+(G)} \text{part}(\sigma) $$

Note that the regularity assumption ensures that the set of participants is finite.

The projection of a global type onto participants is given in Figure 2. As usual, projection is defined only when it is defined on all participants. Because of the simplicity of our calculus, the projection of a global type, when defined, is simply a process. The definition is coinductive, so a global type with an infinite (regular) tree produces a process with a regular tree. The projection of a choice type on the sender produces an output process, i.e. a process sending one of its possible messages to the receiver and then acting according to the projection of the corresponding branch. Similarly for the projection on the receiver, which produces an input process.

Projection of a choice type on the other participants is defined only if it produces the same process for all the branches of the choice. This is a standard condition for multiparty session types [39].

Our coinductive definition of global types is more permissive than that based on the standard $\mu$-notation used in [39], because it allows more global types to be projected, as shown by the following example.

**Example 6.2.** The global type $G = p \to q : (\lambda_1; q \xrightarrow{\lambda_3} r \boxplus \lambda_2; G)$ is projectable and

$$ \bullet \quad G \upharpoonright p = P = q!\lambda_1 \oplus q!\lambda_2; P $$

$$ \bullet \quad G \upharpoonright q = Q = p?\lambda_1; r!\lambda_3 + p?\lambda_2; Q $$

$$ \bullet \quad G \upharpoonright r = q?\lambda_3 $$

On the other hand, the corresponding global type based on the $\mu$-notation

$$ G' = \mu t.p \to q : (\lambda_1; q \xrightarrow{\lambda_3} r \boxplus \lambda_2; t) $$
is not projectable because $G' \upharpoonright r$ is not defined.

However, this additional permissiveness will not be exploited in the present paper. Indeed, the global type $G$ of Example 6.2 will be ruled out by the condition of boundedness, introduced next, which aims at forbidding starvation. On the other hand, such permissiveness could be of interest whenever starvation is not a concern.

To achieve progress, we need to ensure that each network participant occurs in every computation, whether finite or infinite. This means that each type participant must occur in every path of the tree of the type. Projectability already ensures that each participant of a choice type occurs in all its branches. This implies that if one branch of the choice gives rise to an infinite path, either the participant occurs at some finite depth in this path, or this path crosses infinitely many branching points in which the participant occurs in all branches. In the latter case, since the depth of the participant increases when crossing each branching point, there is no bound on the depth of the participant over all paths of the type. Hence, to ensure that all type participants occur in all paths, it is enough to require the existence of such bounds. This motivates the following definition of depth and boundedness.

**Definition 6.3 (Depth and boundedness).**

Let the two functions depth($\sigma$, $p$) and depth($G$, $p$) be defined by:

$$ \text{depth}(\sigma, p) = \begin{cases} n & \text{if } \sigma = \sigma_1 \cdot \alpha \cdot \sigma_2 \text{ and } |\sigma_1| = n - 1 \text{ and } p \notin \text{part}(\sigma_1) \text{ and } p \in \text{part}(\alpha) \\ 0 & \text{otherwise} \end{cases} $$

Then

$$ \text{depth}(G, p) = \sup\{\text{depth}(\sigma, p) \mid \sigma \in \text{Tr}^{+}(G)\} $$

641

We say that a global type $G$ is bounded if depth($G'$, $p$) is finite for all subtrees $G'$ of $G$ and for all participants $p$.

643

If depth($G$, $p$) is finite, then there are no paths in the tree of $G$ in which $p$ is delayed indefinitely. Note that if depth($G$, $p$) is finite, $G$ may have subtrees $G'$ for which depth($G'$, $p$) is infinite as the following example shows.

644

645

646

**Example 6.4.** Consider $G' = q \xrightarrow{\lambda} r$; $G$ where $G$ is as defined in Example 6.2. Then we have:

$$ \text{depth}(G', p) = 2 \qquad \text{depth}(G', q) = 1 \qquad \text{depth}(G', r) = 1 $$

whereas

$$ \text{depth}(G, p) = 1 \qquad \text{depth}(G, q) = 1 \qquad \text{depth}(G, r) = \infty $$

since

648

$$ \text{Tr}^{+}(G) = \underbrace{\{pq\lambda_2 \cdots pq\lambda_2 \cdot pq\lambda_1 \cdot qr\lambda_3 \mid n \ge 0\}}_{n} \cup \{pq\lambda_2 \cdots pq\lambda_2 \cdots\} $$

$$ \text{and } \sup\{2, 3, \dots\} = \infty. $$

649
650

651

652

653

The depths of the participants in $G$ which are not participants of its root com-
munication decrease in the immediate subtrees of $G$. The proof is trivial since, if
$G = p \to q : \coprod_{i \in I} \lambda_i; G_i$, then $\sigma \in \mathrm{Tr}^+(G)$ implies $\sigma = pq\lambda_i \cdot \sigma'$ and $\sigma' \in \mathrm{Tr}^+(G_i)$ for
some $i \in I$.

654

655

**Lemma 6.5.** If $G = p \to q : \coprod_{i \in I} \lambda_i; G_i$ and $r \in \mathrm{part}(G) \setminus \{p, q\}$, then $\mathrm{depth}(G, r) > \mathrm{depth}(G_i, r)$ for all $i \in I$.

656

657

We can now show that the definition of projection given in Figure 2 is sound for bounded global types.

658

**Lemma 6.6.** If $G$ is bounded, then $G \upharpoonright r$ is a partial function for all $r$.

659

660

Boundedness and projectability single out the global types we want to use in our type system.

661

662

**Definition 6.7 (Well-formed global types).** We say that the global type $G$ is well formed if $G$ is bounded and $G \upharpoonright p$ is defined for all $p$.

663

664

Clearly it is sufficient to check that $G \upharpoonright p$ is defined for all $p \in \mathrm{part}(G)$, since otherwise $G \upharpoonright p = 0$.

665

6.2. Type System

$$
\begin{align*}
0 \le 0 [ \le -0 ]
  & \frac{
    \begin{array}{@{}c@{\qquad}c@{}}
      P_i \le Q_i & i \in I \\
      \multicolumn{2}{@{}c@{}}{\text{\scriptsize $\displaystyle\sum_{i \in I \cup J} p?\lambda_i; P_i \le \sum_{i \in I} p?\lambda_i; Q_i$}}
    \end{array}
  }{[ \le -\mathrm{IN} ]}
  &
  \frac{
    \begin{array}{@{}c@{\qquad}c@{}}
      P_i \le Q_i & i \in I \\
      \multicolumn{2}{@{}c@{}}{\text{\scriptsize $\displaystyle\bigoplus_{i \in I} p!\lambda_i; P_i \le \bigoplus_{i \in I} p!\lambda_i; Q_i$}}
    \end{array}
  }{[ \le -\mathrm{OUT} ]}
  \\
  &
  \frac{
    \begin{array}{@{}c@{\qquad}c@{}}
      P_i \le G \upharpoonright p_i & i \in I \\
      \multicolumn{2}{@{}c@{}}{\text{\scriptsize $\displaystyle\vdash \prod_{i \in I} p_i[[ P_i ]] : G$}}
    \end{array}
  }{[ \mathrm{NET} ]}
\end{align*}
$$

<caption>**Figure 3:** Preorder on processes and network typing rule.</caption>

666

667

668

669

670

671

672

673

674

675

The definition of well-typed networks is given in Figure 3. We first define a preorder on processes, $P \le Q$, meaning that process $P$ can be used where we expect process $Q$. More precisely, $P \le Q$ if either $P$ is equal to $Q$, or we are in one of two situations: either both $P$ and $Q$ are output processes with the same receiver and choice of messages, and their continuations after the send are two processes $P'$ and $Q'$ such that $P' \le Q'$; or they are both input processes with the same sender and choice of messages, and $P$ may receive more messages than $Q$ (and thus have more behaviours) but whenever it receives the same message as $Q$ their continuations are two processes $P'$ and $Q'$ such that $P' \le Q'$. The rules are interpreted coinductively, since the processes may have infinite (regular) trees.

676

677

678

A network is well typed if all its participants have associated processes that behave as specified by the projections of a global type. In Rule [NET], the condition $\mathrm{part}(G) \subseteq \{p_i \mid i \in I\}$ ensures that all participants of the global type appear in the
$$ 
\begin{gathered}
\mathbf{p} \to \mathbf{q} : \mathop{\Box}_{i \in I} \lambda_i; \mathbf{G}_i \xrightarrow{\mathbf{pq}\lambda_i} \mathbf{G}_j \quad j \in I \quad [\text{ECOMM}] \\
\frac{\mathbf{G}_i \xrightarrow{\alpha} \mathbf{G}'_i \quad \text{for all } i \in I \quad \text{part}(\alpha) \cap \{\mathbf{p}, \mathbf{q}\} = \emptyset}{\mathbf{p} \to \mathbf{q} : \mathop{\Box}_{i \in I} \lambda_i; \mathbf{G}_i \xrightarrow{\alpha} \mathbf{p} \to \mathbf{q} : \mathop{\Box}_{i \in I} \lambda_i; \mathbf{G}'_i} [\text{ICOMM}]
\end{gathered}
$$

<caption>**Figure 4:** LTS for global types.</caption>

679 network. Moreover it permits additional participants that do not appear in the global type, allowing the typing of sessions containing $\mathbf{p}[[\mathbf{0}]]$ for a fresh $\mathbf{p}$ — a property required to guarantee invariance of types under structural congruence of networks.
680
681
682

**Example 6.8.** The first network of Example 5.15 and the network of Example 5.17 can be typed respectively by

$$ 
\begin{align*}
\mathbf{G} &= \mathbf{p} \to \mathbf{q} : (\lambda; \mathbf{G} \boxplus \lambda') \\
\mathbf{G}' &= \mathbf{p} \xrightarrow{\lambda_1} \mathbf{q}; \mathbf{q} \xrightarrow{\lambda_2} \mathbf{r}; \mathbf{r} \xrightarrow{\lambda_3} \mathbf{s}
\end{align*}
$$

683 It is handy to define the LTS for global types given in Figure 4. Rule [ICOMM] 684 is justified by the fact that in a projectable global type $\mathbf{p} \to \mathbf{q} : \mathop{\Box}_{i \in I} \lambda_i; \mathbf{G}_i$, the 685 behaviours of the participants different from $\mathbf{p}$ and $\mathbf{q}$ are the same in all branches, 686 and hence they are independent from the choice and may be executed before it. 687 This LTS respects well-formedness of global types, as shown by Lemma 6.9.
688
689

**Lemma 6.9.** If $\mathbf{G}$ is a well-formed global type and $\mathbf{G} \xrightarrow{\mathbf{pq}\lambda} \mathbf{G}'$, then $\mathbf{G}'$ is a well-formed global type.

690
691
692
693
694
695
696
697
698
Given this lemma, we will focus on **well-formed global types from now on**.

We end this section with the expected results of Subject Reduction, Session Fidelity [39, 40] and Progress [19, 51]. The proof of Progress relies on Session Fidelity. Both Subject Reduction and Session Fidelity will be used in Section 8 to show the isomorphism between the configuration domains of the FES of a typable network and the PES of its global type (Theorem 8.18).
699
700
701
702

**Theorem 6.10 (Subject Reduction).** If $\vdash N : \mathbf{G}$ and $N \xrightarrow{\alpha} N'$, then $\mathbf{G} \xrightarrow{\alpha} \mathbf{G}'$ and $\vdash N' : \mathbf{G}'$.

**Theorem 6.11 (Session Fidelity).** If $\vdash N : \mathbf{G}$ and $\mathbf{G} \xrightarrow{\alpha} \mathbf{G}'$, then $N \xrightarrow{\alpha} N'$ and $\vdash N' : \mathbf{G}'$.

700
701
702
We are now able to prove that in a typable network, every participant whose process is not terminated may eventually perform a communication. This property is generally referred to as progress.

**Theorem 6.12 (Progress).** If $\vdash N : \mathbf{G}$ and $\mathbf{p}[[\mathbf{P}]] \in N$, then $N \xrightarrow{\sigma \cdot \alpha} N'$ and $\mathbf{p} \in \text{part}(\alpha)$.
704 **Proof** We prove by induction on $d = \text{depth}(G, p)$ that: if $\vdash N : G$ and $p[[P]] \in N$, then $G \xrightarrow{\sigma \cdot \alpha} G'$ with $p \in \text{part}(\alpha)$. This will imply $N \xrightarrow{\sigma \cdot \alpha} N'$ by Session Fidelity (Theorem 6.11).

707 Case $d = 1$. In this case $G = q \to r : \coprod_{i \in I} \lambda_i; G_i$ and $p \in \{q, r\}$ and $G \xrightarrow{qr, \lambda_h} G_h$ for some $h \in I$ by Rule [ECOMM].

708
709 Case $d > 1$. In this case $G = q \to r : \coprod_{i \in I} \lambda_i; G_i$ and $p \notin \{q, r\}$. By Lemma 6.5 this implies $\text{depth}(G_i, p) < d$ for all $i \in I$. Using Rule [ECOMM] we get $G \xrightarrow{qr, \lambda_i} G_i$ for all $i \in I$. By Session Fidelity, $N \xrightarrow{qr, \lambda_i} N_i$ and $\vdash N_i : G_i$ for all $i \in I$. Moreover, since $p \notin \{q, r\}$ we also have $p[[P]] \in N_i$ for all $i \in I$. By induction $G_i \xrightarrow{\sigma_i \cdot \alpha_i} G'_i$ with $p \in \text{part}(\alpha_i)$ for all $i \in I$. We conclude $G \xrightarrow{qr, \lambda_i, \sigma_i \cdot \alpha_i} G'_i$ for all $i \in I$.

714 The proof of the progress theorem shows that the execution strategy which uses
715 only Rule [ECOMM] is fair, since there are no infinite transition sequences where
716 some participant is stuck. This is due to the boundedness condition on global
717 types.

**Example 6.13.** The second network of Example 5.15 and the network of Example 5.20 cannot be typed because they do not enjoy progress. Notice that the candidate global type for the second network of Example 5.15:

$$
G'' = p \to q : (\lambda; G'' \boxplus \lambda'; p \xrightarrow{\lambda} r; r \xrightarrow{\lambda'} s)
$$

718 is not bounded, given that depth(G'', r) and depth(G'', s) are not finite.

719 Moreover we cannot define a global type whose projections are greater than or equal to the
720 processes associated with the network of Example 5.20.

721 **7. Event Structure Semantics of Global Types**

722 We define now the event structure associated with a global type, whose events
723 are equivalence classes of particular traces, and we show that it is a PES.

724 The unique omitted proof can be found in Appendix C.

725 We recall that a trace $\sigma \in \text{Traces}$ is a finite sequence of communications (see
726 Definition 2.3). We will use the following notational conventions:

727 • We denote by $\sigma[i]$ the $i$-th element of $\sigma$, $i > 0$.

728 • If $i \le j$, we define $\sigma[i \dots j] = \sigma[i] \cdots \sigma[j]$ to be the subtrace of $\sigma$ consisting of the
729 $(j-i+1)$ elements starting from the $i$-th one and ending with the $j$-th one. If
730 $i > j$, we convene $\sigma[i \dots j]$ to be the empty trace $\epsilon$.

731 If not otherwise stated we assume that $\sigma$ has $n$ elements, so $\sigma = \sigma[1 \dots n]$.

732 We start by defining an equivalence relation on *Traces* which allows swapping
733 of communications with disjoint participants.
**Definition 7.1 (Permutation equivalence).** The permutation equivalence on Traces is the least equivalence ~ such that

$$ \sigma \cdot \alpha \cdot \alpha' \cdot \sigma' \sim \sigma \cdot \alpha' \cdot \alpha \cdot \sigma' \quad \text{if } \text{part}(\alpha) \cap \text{part}(\alpha') = \emptyset $$

We denote by $[\sigma]_{\sim}$ the equivalence class of the trace $\sigma$, and by Traces/$\sim$ the set of equivalence classes on Traces. Note that $[\epsilon]_{\sim} = \{\epsilon\} \in \text{Traces}/_{\sim}$, and $[\alpha]_{\sim} = \{\alpha\} \in \text{Traces}/_{\sim}$ for any $\alpha$. Moreover $|\sigma'| = |\sigma|$ for all $\sigma' \in [\sigma]_{\sim}$.

The events associated with a global type, called g-events and denoted by $\gamma, \gamma'$, are equivalence classes of particular traces that we call pointed. Intuitively, in a pointed trace all communications but the last one are causes of some subsequent communication. Formally:

**Definition 7.2 (Pointed trace).** A trace $\sigma = \sigma[1 \dots n]$ is said to be pointed if

$$ \text{for all } i, 1 \le i < n, \text{ part}(\sigma[i]) \cap \text{part}(\sigma[(i+1) \dots n]) \neq \emptyset $$

Note that the condition of Definition 7.2 must be satisfied only by the $\sigma[i]$ with $i < n$, thus it is vacuously satisfied by any trace of length 1.

**Example 7.3.** Let $\alpha_1 = pq\lambda_1, \alpha_2 = rs\lambda_2$ and $\alpha_3 = rp\lambda_3$. Then $\sigma_1 = \alpha_1$ and $\sigma_3 = \alpha_1 \cdot \alpha_2 \cdot \alpha_3$ are pointed traces, while $\sigma_2 = \alpha_1 \cdot \alpha_2$ is not a pointed trace.

We use last($\sigma$) to denote the last communication of $\sigma$.

**Lemma 7.4.** Let $\sigma$ be a pointed trace. If $\sigma \sim \sigma'$, then $\sigma'$ is a pointed trace and last($\sigma$) = last($\sigma'$).

**Definition 7.5 (Global event).** Let $\sigma = \sigma' \cdot \alpha$ be a pointed trace. Then $\gamma = [\sigma]_{\sim}$ is a global event, also called g-event, with communication $\alpha$, notation $cm(\gamma) = \alpha$. We denote by $\mathcal{G}$ the set of g-events.

Notice that $cm(\gamma)$ is well defined due to Lemma 7.4.

We now introduce an operator of prefixing of a g-event $\gamma$ by a communication $\alpha$, which acts as follows: if $\alpha$ is a cause of some communication in the trace of $\gamma$, then $\alpha$ is added at the beginning of the trace, otherwise $\gamma$ is left unchanged. This ensures that the operator always transforms a g-event into another g-event. We call this operator "retrieval of a g-event before a communication", because it yields the g-event obtained from $\gamma$ if we were to execute the communication $\alpha$ before $\gamma$. This operator is the counterpart of the "residual of a g-event after a communication", which yields the g-event obtained from $\gamma$ after executing the communication $\alpha$ from $\gamma$, see Definition 8.9.

**Definition 7.6 (Retrieval of g-events before communications).**

1. The retrieval operator $\circ$ applied to a communication and a g-event is defined by:

$$ \alpha \circ [\sigma]_{\sim} = \begin{cases} [\alpha \cdot \sigma]_{\sim} & \text{if } \text{part}(\alpha) \cap \text{part}(\sigma) \neq \emptyset \\ [\sigma]_{\sim} & \text{otherwise} \end{cases} $$
2. The operator ◦ naturally extends to traces:

$$ \epsilon \circ \gamma = \gamma \qquad (\alpha \cdot \sigma) \circ \gamma = \alpha \circ (\sigma \circ \gamma) $$

Using the retrieval, we can define the mapping $ev(\cdot)$ which, applied to a trace $\sigma$, gives the g-event representing the communication $last(\sigma)$ prefixed by its causes occurring in $\sigma$.

**Definition 7.7.** The g-event generated by a non-empty trace is defined by:

$$ ev(\sigma \cdot \alpha) = \sigma \circ [\alpha]_{\sim} $$

Clearly $cm(ev(\sigma)) = last(\sigma)$.

**Example 7.8.** A trace of the global type $p \xrightarrow{\lambda_1} q; q \xrightarrow{\lambda_2} r; s \xrightarrow{\lambda_3} p$ is $pq\lambda_1 \cdot qr\lambda_2 \cdot sp\lambda_3$, and
$$ ev(pq\lambda_1 \cdot qr\lambda_2 \cdot sp\lambda_3) = pq\lambda_1 \cdot qr\lambda_2 \circ \{sp\lambda_3\} = pq\lambda_1 \circ \{sp\lambda_3\} = \{pq\lambda_1 \cdot sp\lambda_3\} $$

We proceed now to define the causality and conflict relations on g-events. To define the conflict relation, it is handy to define the projection of a trace on a participant, which gives the sequence of the participant's actions in the trace. The result is a p-event. In this way we can define the conflict between g-events using the conflict between p-events.

**Definition 7.9 (Projection of traces on participants).**

1. The projection of $\alpha$ onto $r$, $\alpha@r$, is defined by:

$$ pq\lambda@r = \begin{cases} q!\lambda & \text{if } r = p \\ p?\lambda & \text{if } r = q \\ \epsilon & \text{if } r \notin \{p, q\} \end{cases} $$

2. The projection of a trace $\sigma$ onto $r$, $\sigma@r$, is defined by:

$$ \epsilon@r = \epsilon \qquad (\alpha \cdot \sigma)@r = \alpha@r \cdot \sigma@r $$

**Definition 7.10 (Causality and conflict relations on g-events).** The causality relation $\le$ and the conflict relation $\#$ on the set of g-events $\mathcal{G}$ are defined by:

1. $\gamma \le \gamma'$ if $\gamma = [\sigma]_{\sim}$ and $\gamma' = [\sigma \cdot \sigma']_{\sim}$ for some $\sigma, \sigma'$;

2. $[\sigma]_{\sim} \# [\sigma']_{\sim}$ if $\sigma@p \# \sigma'@p$ for some $p$.

If $\gamma = [\sigma \cdot \alpha \cdot \sigma' \cdot \alpha']_{\sim}$, then the communication $\alpha$ must be done before the communication $\alpha'$. This is expressed by the causality $[\sigma \cdot \alpha]_{\sim} \le \gamma$. An example is $[pq\lambda]_{\sim} \le [rs\lambda' \cdot pq\lambda \cdot sq\lambda'']_{\sim}$.

As regards conflict, note that if $\sigma \sim \sigma'$ then $\sigma@p = \sigma'@p$ for all $p$, because $\sim$ does not swap communications which share some participant. Hence, conflict is well defined, since it does not depend on the trace chosen in the equivalence class. The condition $\sigma@p \# \sigma'@p$ states that participant $p$ does the same actions in both traces up to some point, after which it performs two different actions in $\sigma$ and $\sigma'$. For example $[pq\lambda \cdot rp\lambda_1 \cdot qp\lambda']_{\sim} \# [pq\lambda \cdot rp\lambda_2]_{\sim}$, since $(pq\lambda \cdot rp\lambda_1 \cdot qp\lambda')@p = q!\lambda \cdot r?\lambda_1 \cdot q?\lambda' \# q!\lambda \cdot r?\lambda_2 = (pq\lambda \cdot rp\lambda_2)@p$.
**Definition 7.11 (Event structure of a global type).** The event structure of the global type G is the triple

$$ S^G(G) = (\mathcal{G}E(G), \leq_G, \#_G) $$

where:

1. $\mathcal{G}E(G) = \{\text{ev}(\sigma) | \sigma \in \text{Tr}^+(G)\}$

2. $\leq_G$ is the restriction of $\leq$ to the set $\mathcal{G}E(G)$;

3. $\#_G$ is the restriction of $\#$ to the set $\mathcal{G}E(G)$.

Note that, in case the tree of G is infinite, the set $\mathcal{G}E(G)$ is denumerable.

**Example 7.12.** Let $G_1 = p \xrightarrow{\lambda_1} q; r \xrightarrow{\lambda_2} s; r \xrightarrow{\lambda_3} p$ and $G_2 = r \xrightarrow{\lambda_3} s; p \xrightarrow{\lambda_1} q; r \xrightarrow{\lambda_3} p$. Then $\mathcal{G}E(G_1) = \mathcal{G}E(G_2) = \{\gamma_1, \gamma_2, \gamma_3\}$ where

$$ \gamma_1 = \{pq\lambda_1\} \quad \gamma_2 = \{rs\lambda_2\} \quad \gamma_3 = \{pq\lambda_1 \cdot rs\lambda_2 \cdot rp\lambda_3, rs\lambda_2 \cdot pq\lambda_1 \cdot rp\lambda_3\} $$

with $\gamma_1 \leq \gamma_3$ and $\gamma_2 \leq \gamma_3$. The configurations are $\{\gamma_1\}$, $\{\gamma_2\}$, $\{\gamma_1, \gamma_2\}$ and $\{\gamma_1, \gamma_2, \gamma_3\}$, and the proving sequences are

$$ \gamma_1 \quad \gamma_2 \quad \gamma_1; \gamma_2 \quad \gamma_2; \gamma_1 \quad \gamma_1; \gamma_2; \gamma_3 \quad \gamma_2; \gamma_1; \gamma_3 $$

If $G'$ is as in Example 6.8, then $\mathcal{G}E(G') = \{\gamma_1, \gamma_2, \gamma_3\}$ where

$$ \gamma_1 = \{pq\lambda_1\} \quad \gamma_2 = \{pq\lambda_1 \cdot qr\lambda_2\} \quad \gamma_3 = \{pq\lambda_1 \cdot qr\lambda_2 \cdot rs\lambda_3\} $$

with $\gamma_1 \leq \gamma_2 \leq \gamma_3$. The configurations are $\{\gamma_1\}$, $\{\gamma_1, \gamma_2\}$ and $\{\gamma_1, \gamma_2, \gamma_3\}$, and there is a unique proving sequence corresponding to each configuration.

**Theorem 7.13.** Let G be a global type. Then $S^G(G)$ is a prime event structure.

**Proof** We show that $\leq$ and $\#$ satisfy Properties (2) and (3) of Definition 3.1. Reflexivity and transitivity of $\leq$ follow from the properties of concatenation and of permutation equivalence. As for antisymmetry, by Definition 7.10(1) $[\sigma] \leq [\sigma']$ implies $\sigma' \sim \sigma \cdot \sigma_1$ for some $\sigma_1$ and $[\sigma'] \leq [\sigma]$ implies $\sigma \sim \sigma' \cdot \sigma_2$ for some $\sigma_2$. Hence $\sigma \sim \sigma \cdot \sigma_1 \cdot \sigma_2$, which implies $\sigma_1 = \sigma_2 = \epsilon$. Irreflexivity and symmetry of $\#$ follow from the corresponding properties of $\#$ on p-events.

As for conflict hereditariness, suppose that $[\sigma] \leq [\sigma'] \leq [\sigma'']$. By Definition 7.10(1) and (2) we have respectively that $\sigma' \cdot \sigma_1 \sim \sigma''$ for some $\sigma_1$ and $\sigma@p \# \sigma'@p$ for some p. Hence also $\sigma@p \# (\sigma' \cdot \sigma_1)@p$, whence by Definition 7.10(2) we conclude that $[\sigma] \leq [\sigma'']$.

Observe that, while our interpretation of networks as FESs exactly reflects the concurrency expressed by the syntax of networks, our interpretation of global types as PESs exhibits more concurrency than that given by the syntax of global types.

We conclude this section with two pictures that summarise the features of our ES semantics and illustrate the difference between the FES of a network and the
<figure><img src="image_2.png" /><figcaption>Figure 5: FES of the network N.</figcaption></figure>

<figure><img src="image_3.png" /><figcaption>Figure 6: PES of the type G.</figcaption></figure>

<footnote n="811">811 PES of its type. In general these two ESs are not isomorphic, unless the FES of the network is itself a PES.</footnote>

<footnote n="812">812 Consider the network FES pictured in Figure 5, where the arrows represent the flow relation and all the n-events on the left of the dotted line are in conflict with all the n-events on the right of the line. In particular, notice that the conflicts between</footnote>
n-events with a common location are deduced by Clause (2a) of Definition 5.7, while the conflicts between n-events with disjoint sets of locations, such as $v_1'$ and $v_2''$, are deduced by Clause (2b) of Definition 5.7. Observe also that the n-event $v$ has two different causal sets in $\mathcal{NE}(\mathcal{N})$, namely $\{v_1', v_1''\}$ and $\{v_2', v_2''\}$. The reader familiar with ESs will have noticed that there are also two prime configurations whose maximal element is $v$, namely $\{v_1, v_1', v_1'', v\}$ and $\{v_2, v_2', v_2'', v\}$. It is easy to see that the network $\mathcal{N}$ can be typed with the global type $\mathcal{G}$ shown in Figure 6.

Consider now the PES of the type $\mathcal{G}$ pictured in Figure 6, where the arrows represent the covering relation of the partial order of causality and inherited conflicts are not shown. Note that while the FES of $\mathcal{N}$ has a unique maximal n-event $v$, the PES of its type $\mathcal{G}$ has two maximal g-events $\gamma$ and $\gamma'$. This is because an n-event only records the computations that occurred at its locations, while a g-event records the global computation and keeps a record of each choice, including those involving locations that are disjoint from those of its last communication. Indeed, g-events correspond exactly to prime configurations.

Note that the FES of a network may be easily recovered from the PES of its global type by using the following function $gn(\cdot)$ that maps g-events to n-events:

$$gn(\gamma) = \{p :: \sigma@p, q :: \sigma@q\} \quad \text{if } \gamma = [\sigma] \sim \text{with } \text{part}(cm(\gamma)) = \{p, q\}$$

On the other hand, the inverse construction is not as direct. First of all, an n-event in the network FES may give rise to several g-events in the type PES, as shown by the n-event $v$ in Figure 5, which gives rise to the pair of g-events $\gamma$ and $\gamma'$ in Figure 6. Moreover, the local information contained in an n-event is not sufficient to reconstruct the corresponding g-events: for each n-event, we need to consider all the prime configurations that culminate with that event, and then map each of these configurations to a g-event. Hence, we need a function $ng(\cdot)$ that maps n-events to sets of prime configurations of the FES, and then maps each such configuration to a g-event. We will not explicitly define this function here, since we miss another important ingredient to compare the FES of a network and the PES of its type, namely a structural characterisation of the FESs that represent typable networks. Indeed, if we started from the FES of a non typable network, this construction would not be correct. Consider for instance the network $\mathcal{N}'$ obtained from $\mathcal{N}$ by omitting the output $r!\lambda$ from the second branch of the process of $p$. Then the FES of $\mathcal{N}'$ would not contain the n-event $v_2'$ and the event $v$ would have the unique causal set $\{v_1', v_1''\}$, and the unique prime configuration culminating with $v$ would be $\{v_1, v_1', v_1'', v\}$. Then our construction would give a PES that differs from that of type $\mathcal{G}$ only for the absence of the g-events $\gamma'_2$ and $\gamma'$. However, the network $\mathcal{N}'$ is not typable and thus we would expect the construction to fail. Note that in the FES of $\mathcal{N}'$, the n-event $v_2''$ is a cause of $v$ but does not belong to any causal set of $v$. Thus a possible well-formedness property to require for FESs to be images of a typable network would be that each cause of each n-event belong to some causal set of that event. However, this would still not be enough to exclude the FES of the non typable network $\mathcal{N}''$ obtained from $\mathcal{N}'$ by omitting the output $s!\lambda'$ from the second branch of the process of $q$.

To conclude, in the absence of a semantic counterpart for the well-formedness properties of global types, which eludes us for the time being, we will follow another
approach here, namely we will compare the FESs of networks and the PESs of their types at a more operational level, by looking at their configuration domains and by relating their configurations to the transition sequences of the underlying networks and types.

## 8. Equivalence of the two Event Structure Semantics

<figure><img src="image_4.png" /><figcaption>**Figure 7:** Isomorphism proof in a nutshell.</figcaption></figure>

In this section we establish our main result for typable networks (Theorem 8.18), namely the isomorphism between the domain of configurations of the FES of a typable network and the domain of configurations of the PES of its global type. To do so, we first relate the transition sequences of networks and global types to the configurations of their respective ESs. Then, we exploit our results of Subject Reduction (Theorem 6.10) and Session Fidelity (Theorem 6.11), which relate the transition sequences of networks and their global types, to derive a similar relation between the configurations of their respective ESs. The schema of our proof is described by the diagram in Figure 7. Here, SR stands for Subject Reduction and SF for Session Fidelity, and $v_1;...;v_n$ and $\gamma_1;...;\gamma_n$ are proving sequences of $S^N(N)$ and $S^G(G)$, respectively. Finally, nec($\sigma$) and gec($\sigma$) denote the proving sequences of n-events and g-events which correspond to the trace $\sigma$ (as given by Definition 8.3 and Definition 8.13). Theorem 8.8 says that, if $v_1;...;v_n$ is a proving sequence of $S^N(N)$, then $N \xrightarrow{\sigma} N'$, where $\sigma = \text{cm}(v_1) ... \text{cm}(v_n)$. By Subject Reduction (Theorem 6.10) $G \xrightarrow{\sigma} G'$. This implies that gec($\sigma$) is a proving sequence of $S^G(G)$ by Theorem 8.15. Dually, Theorem 8.16 says that, if $\gamma_1;...;\gamma_n$ is a proving sequence of $S^G(G)$, then $G \xrightarrow{\sigma} G'$, where $\sigma = \text{cm}(\gamma_1) ... \text{cm}(\gamma_n)$. By Session Fidelity (Theorem 6.11) $N \xrightarrow{\sigma} N'$. Lastly, nec($\sigma$) is a proving sequence of $S^N(N)$ by Theorem 8.7. The equalities in the top and bottom lines are proved in Lemmas 8.4(1a) and 8.14(1).

This section is divided in two subsections: Section 8.1, which handles the upper part of the above diagram, and Section 8.2, which handles the lower part of the diagram and then connects the two parts using both SR and SF within Theorem 8.18, our closing result. The omitted proofs of Sections 8.1 and 8.2 can be found in Appendices D and E, respectively.
### 8.1. Relating Transition Sequences of Networks and Proving Sequences of their ESs

The aim of this subsection is to relate the traces that label the transition sequences of networks with the configurations of their FESs. We start by showing how network communications affect n-events in the associated FES. To this end we define two partial operators ◊ and ♦, which applied to a communication α and an n-event v yield another n-event v' (when defined), which represents the event v before the communication α or after the communication α, respectively. We call "retrieval" the ◊ operator (in agreement with Definition 7.6) and "residual" the ♦ operator.

Formally, the operators ◊ and ♦ are defined as follows.

## 8.1.1. Definition 8.1 (Retrieval and residual of n-events with respect to communications).

1. The retrieval operator ◊ applied to a communication and a located event returns the located event obtained by prefixing the p-event by the projection of the communication:

$$α ◊ (p :: η) = p :: (α@p) · η$$

2. The residual operator ♦ applied to a communication and a located event returns the located event obtained by erasing from the p-event the projection of the communication (if possible):

$$α ♦ (p :: η) = p :: η' \quad \text{if } η = (α@p) · η'$$

3. The operators ◊ and ♦ naturally extend to n-events and to traces:

$$α ◊ (\{p :: η, q :: η'\}) = \{α ◊ (p :: η), α ◊ (q :: η')\}$$

$$α ♦ (\{p :: η, q :: η'\}) = \{α ♦ (p :: η), α ♦ (q :: η')\}$$

$$ε ◊ v = v \qquad (α · σ) ◊ v = α ◊ (σ ◊ v)$$

$$ε ♦ v = v \qquad (α · σ) ♦ v = σ ♦ (α ♦ v)$$

Note that the operator ◊ is always defined. Instead pqλ♦r :: η is undefined if r ∈ {p, q} and either η is just one atomic action or pqλ@r is not the first atomic action of η. For example pqλ♦p :: q!λ and pqλ♦p :: q!λ' · η with λ ≠ λ' are undefined for any η.

The retrieval and residual operators are inverse of each other. Moreover they preserve the flow and conflict relations.

## 8.2. Lemma 8.2 (Properties of retrieval and residual for n-events).

1. If α ♦ v is defined, then α ◊ (α ♦ v) = v;

2. α ♦ (α ◊ v) = v;

3. If v < v', then α ◊ v < α ◊ v';

4. If v < v' and both α ♦ v and α ♦ v' are defined, then α ♦ v < α ♦ v';

5. If v # v', then α ◊ v # α ◊ v';

6. If v # v' and both α ♦ v and α ♦ v' are defined, then α ♦ v # α ♦ v';
7. If $\alpha \diamond v \# \alpha \diamond v'$, then $v \# v'$.

Starting from the trace $\sigma \neq \epsilon$ that labels a transition sequence in a network, one can reconstruct the corresponding sequence of n-events in its FES. Recall that $\sigma[1 \dots i]$ is the prefix of length $i$ of $\sigma$ and $\sigma[i \dots j]$ is the empty trace if $i > j$.

**Definition 8.3 (Building sequences of n-events from traces).** If $\sigma$ is a non-empty trace with $\sigma[i] = p_i q_i \lambda_i$, $1 \le i \le n$, we define the sequence of n-events corresponding to $\sigma$ by

$$ \mathrm{nec}(\sigma) = v_1; \cdots; v_n $$

where $v_i = \sigma[1 \dots i - 1] \diamond \{p_i :: q_i!\lambda_i, q_i :: p_i?\lambda_i\}$ for $1 \le i \le n$.

It is immediate to see that, if $\sigma = pq\lambda$, then $\mathrm{nec}(\sigma)$ is the event $\{p :: q!\lambda, q :: p?\lambda\}$.

We show now that $\sigma$ can be recovered from $\mathrm{nec}(\sigma)$, and that two n-events occurring in $\mathrm{nec}(\sigma)$ cannot be in conflict. Moreover, the n-event obtained by applying $\mathrm{nec}$ to a communication cannot be in conflict with the n-event obtained by applying the retrieval to the same communication and an arbitrary n-event.

Lastly, we relate the sequences of n-events generated by two traces one of which is a suffix of the other. Given that the mapping $\mathrm{nec}$ is based on the retrieval operator, this relation is naturally expressed using the retrieval and residual operators.

**Lemma 8.4 (Properties of nec(·)).**

1. Let $\mathrm{nec}(\sigma) = v_1; \cdots; v_n$. Then

(a) $\mathrm{cm}(v_i) = \sigma[i]$ for all $i, 1 \le i \le n$;

(b) If $1 \le h, k \le n$, then $\neg(v_h \# v_k)$.

2. $\neg(\mathrm{nec}(\alpha) \# \alpha \diamond v)$ for all $v$.

3. Let $\sigma = \alpha \cdot \sigma'$ and $\sigma' \neq \epsilon$. If $\mathrm{nec}(\sigma) = v_1; \cdots; v_n$ and $\mathrm{nec}(\sigma') = v'_2; \cdots; v'_n$, then $\alpha \diamond v'_i = v_i$ and $\alpha \diamond v_i = v'_i$ for all $i, 2 \le i \le n$.

Notice that if $\alpha \diamond v$ is undefined and $v$ is an n-event of a network with communication $\alpha$, then either $v = \mathrm{nec}(\alpha)$ or $v \# \mathrm{nec}(\alpha)$.

**Lemma 8.5.** If $N \xrightarrow{\alpha} N'$ and $v \in \mathcal{NE}(N)$, then $v = \mathrm{nec}(\alpha)$ or $v \# \mathrm{nec}(\alpha)$ or $\alpha \diamond v$ is defined.

The following lemma, which is technically quite challenging as it involves reasoning about the fixpoint properties of the set of n-events of a network FES (as defined by the narrowing function), relates the sets of n-events of two network FESs, where one network is a one-step derivative of the other, by means of the retrieval and residual operators.

**Lemma 8.6.** Let $N \xrightarrow{\alpha} N'$. Then

1. $\{\mathrm{nec}(\alpha)\} \cup \{\alpha \diamond v | v \in \mathcal{NE}(N')\} \subseteq \mathcal{NE}(N)$;
2. {$\alpha \diamond v | v \in \mathcal{NE}(N)$ and $\alpha \diamond v$ defined} $\subseteq \mathcal{NE}(N')$.

We may now prove the correspondence between the traces labelling the transition sequences of a network and the proving sequences of its FES.

**Theorem 8.7.** If $N \xrightarrow{\sigma} N'$, then nec($\sigma$) is a proving sequence in $S^N(N)$.

**Proof** The proof is by induction on $\sigma$.

*Base case.* Let $\sigma = \alpha$. From $N \xrightarrow{\alpha} N'$ and Lemma 8.6(1) nec($\alpha) \in \mathcal{NE}(N)$. Since nec($\alpha$) has no causes, by Definition 3.6 we conclude that nec($\alpha$) is a proving sequence in $S^N(N)$.

*Inductive case.* Let $\sigma = \alpha \cdot \sigma'$. From $N \xrightarrow{\sigma} N'$ we get $N \xrightarrow{\alpha} N'' \xrightarrow{\sigma'} N'$ for some $N''$. Let nec($\sigma$) = $v_1; \dots; v_n$ and nec($\sigma')$ = $v'_2; \dots; v'_n$. By induction nec($\sigma'$) is a proving sequence in $S^N(N'')$.

We show that nec($\sigma$) is a proving sequence in $S^N(N)$. By Lemma 8.4(1b) nec($\sigma'$) is conflict free. By Lemma 8.4(3) $v_i = \alpha \diamond v'_i$ for all $i, 2 \le i \le n$. This implies $v_i \in \mathcal{NE}(N)$ for all $i, 2 \le i \le n$ by Lemma 8.6(1) and $\neg(v_1 \# v_j)$ for all $i, j, 2 \le i, j \le n$ by Lemma 8.2(7). Finally, since $v_1 = \text{nec}(\alpha)$, by Lemma 8.4(2) we obtain $\neg(v_1 \# v_i)$ for all $i, 2 \le i \le n$. We conclude that nec($\sigma$) is conflict-free and included in $\mathcal{NE}(N)$. Let $v \in \mathcal{NE}(N)$ and $v < v_k$ for some $k, 1 \le k \le n$. This implies $k > 1$ since nec($\alpha$) has no causes. Hence $v_k = \alpha \diamond v'_k$. By Lemma 8.5, we know that $v = \text{nec}(\alpha)$ or $v \# \text{nec}(\alpha)$ or $\alpha \diamond v$ is defined. We consider the three cases. Let part($\alpha$) = $\{p, q\}$.

*Case v = nec(α).* In this case we conclude immediately since nec($\alpha$) = $v_1$ and $1 < k$. *Case v # nec(α).* Since nec($\alpha$) = $v_1$, if $v_1 < v_k$ we are done. If $v_1 \not< v_k$, then $\text{loc}(v_k) \cap \{p, q\} = \emptyset$ otherwise $v_1 \# v_k$. We get $v_k = \alpha \diamond v'_k = v'_k$. Since $v < v_k$, there exists $r :: \eta \in v$ and $r :: \eta' \in v_k = v'_k$ such that $\eta < \eta'$, where $r \notin \{p, q\}$ because $r \in \text{loc}(v_k)$. Since nec($\sigma'$) is a proving sequence in $S^N(N'')$, by Lemma 5.24 there is $v'_h \in \mathcal{NE}(N'')$ such that $r :: \eta \in v'_h$. Since $\alpha \diamond r :: \eta = r :: \eta$ we get $r :: \eta \in v_h$. This implies $v_h < v_k$, where $v_h \# v$ by Lemma 5.21.

*Case α♦v defined.* We get $\alpha \diamond v < v'_k$ by Lemma 8.2(4). Since nec($\sigma'$) is a proving sequence in $S^N(N'')$, there is $h < k$ such that either $\alpha \diamond v = v'_h$ or $\alpha \diamond v \# v'_h < v'_k$. In the first case $v = \alpha \diamond (\alpha \diamond v) = \alpha \diamond v'_h = v_h$ by Lemma 8.2(1). In the second case:

* from $\alpha \diamond v \# v'_h$ we get $(\alpha \diamond (\alpha \diamond v)) \# (\alpha \diamond v'_h)$ by Lemma 8.2(5), which implies $v \# v_h$ by Lemma 8.2(1), and

* from $v'_h < v'_k$ we get $(\alpha \diamond v'_h) < (\alpha \diamond v'_k)$ by Lemma 8.2(3), namely $v_h < v_k$.

**Theorem 8.8.** If $v_1; \dots; v_n$ is a proving sequence in $S^N(N)$, then $N \xrightarrow{\sigma} N'$, where $\sigma = \text{cm}(v_1) \dots \text{cm}(v_n)$.

**Proof** The proof is by induction on $n$.

Case $n = 1$. Let $v_1 = \{p :: \zeta \cdot q!\lambda, q :: \zeta' \cdot p?\lambda\}$. Then $\text{cm}(v_1) = pq\lambda$. We first show that $\zeta = \zeta' = \epsilon$. Assume ad absurdum that $\zeta \neq \epsilon$ or $\zeta' \neq \epsilon$. By narrowing, this implies that there is $v \in \mathcal{NE}(N)$ such that $v < v_1$, contradicting the fact that $v_1$ is a proving sequence.
By Definition 5.13(1) we have $N = \mathbf{p}[[P]] \parallel \mathbf{q}[[Q]] \parallel N_0$ with $\mathbf{q}!\lambda \in \mathcal{PE}(P)$ and $\mathbf{p}\lambda \in \mathcal{PE}(Q)$. Whence by Definition 4.3(1) we get $P = \bigoplus_{i \in I} \mathbf{q}!\lambda_i; P_i$ and $Q = \sum_{j \in J} \mathbf{p}\lambda_j; Q_j$ where $\lambda = \lambda_k$ for some $k \in I \cap J$. Therefore

$$N \xrightarrow{pq\lambda} \mathbf{p}[[P_k]] \parallel \mathbf{q}[[Q_k]] \parallel N_0$$

Case $n > 1$. Let $v_1$ and $N$ be as in the basic case, $N'' = \mathbf{p}[[P_k]] \parallel \mathbf{q}[[Q_k]] \parallel N_0$ and $\alpha = pq\lambda$. Since $v_1; \cdots; v_n$ is a proving sequence, we have $\neg(v_1 \# v_{l'})$ for all $l, l'$ such that $1 \le l, l' \le n$. Moreover, for all $l, 2 \le l \le n$ we have $v_l \ne v_1 = \text{nec}(\alpha)$, thus $\alpha \diamond v_l$ is defined by Lemma 8.5. Let $v'_l = \alpha \diamond v_l$ for all $l, 2 \le l \le n$, then $v'_l \in \mathcal{NE}(N'')$ by Lemma 8.6(2).

We show that $v'_2; \cdots; v'_n$ is a proving sequence in $S^N(N'')$. First notice that for all $l, 2 \le l \le n$, $\neg(v_l \# v_{l'})$ implies $\neg(v'_l \# v'_{l'})$ by Lemma 8.2(5) and (1). Let now $v < v'_h$ for some $h, 2 \le h \le n$. By Lemma 8.2(3) and (1) $\alpha \diamond v < \alpha \diamond (\alpha \diamond v_h) = v_h$. This implies by Definition 3.6 that there is $h' < h$ such that either $\alpha \diamond v = v_{h'}$ or $\alpha \diamond v \# v_{h'} < v_h$. Therefore, since $v'_l$ is defined for all $l, 2 \le l \le n$, we get either $v = v'_{h'}$ by Lemma 8.2(2) or $v \# v'_{h'} < v'_h$ by Lemma 8.2(6) and (4).

By induction $N'' \xrightarrow{\sigma'} N'$ where $\sigma' = \text{cm}(v'_2) \cdots \text{cm}(v'_n)$. Since $\text{cm}(v_l) = \text{cm}(v'_l)$ for all $l, 2 \le l \le n$ we get $\sigma = \alpha \cdot \sigma'$. Hence $N \xrightarrow{\alpha} N'' \xrightarrow{\sigma'} N'$ is the required transition sequence.

## 8.2. Relating Transition Sequences of Global Types and Proving Sequences of their ESs

In this subsection, we relate the traces that label the transition sequences of global types with the configurations of their PESs. As for n-events, we need retrieval and residual operators for g-events. The first operator was already introduced in Definition 7.6, so we only need to define the second one, which is given next.

## Definition 8.9 (Residual of g-events after communications).

1. The residual operator $\bullet$ applied to a communication and a g-event is defined by:

$$\alpha \bullet [\sigma]_{\sim} = \begin{cases} [\sigma]_{\sim} & \text{if } \sigma \sim \alpha \cdot \sigma' \text{ and } \sigma' \neq \epsilon \\ [\sigma]_{\sim} & \text{if } \text{part}(\alpha) \cap \text{part}(\sigma) = \emptyset \end{cases}$$

2. The operator $\bullet$ naturally extends to traces:

$$\epsilon \bullet \gamma = \gamma \qquad (\alpha \cdot \sigma) \bullet \gamma = \sigma \bullet (\alpha \bullet \gamma)$$

The operator $\bullet$, applied to a communication and a g-event, gives the g-event obtained by erasing the communication, if it occurs in head position (modulo $\sim$) in the given g-event, and leaves the g-event unchanged if its participants are disjoint from those of the communication. Note that the operator $\alpha \bullet [\sigma]_{\sim}$ is undefined whenever either $[\sigma]_{\sim} = \{\alpha\}$ or one of the participants of $\alpha$ occurs in $\sigma$ but the first communication of $\sigma$ is different from $\alpha$. For example $pq\lambda \bullet [pq\lambda]_{\sim}$ and $pq\lambda \bullet [pq\lambda' \cdot \sigma]_{\sim}$ with $\lambda \neq \lambda'$ are undefined for any $\sigma$.

The following lemma gives some simple properties of the retrieval and residual operators for g-events. The first five statements correspond to those of Lemma 8.2 for n-events. The last three statements give properties that are relevant only for the operators $\circ$ and $\bullet$.
### Lemma 8.10 (Properties of retrieval and residual for g-events).

1. If $\alpha \bullet \gamma$ is defined, then $\alpha \circ (\alpha \bullet \gamma) = \gamma$;

2. $\alpha \bullet (\alpha \circ \gamma) = \gamma$;

3. If $\gamma_1 < \gamma_2$, then $\alpha \circ \gamma_1 < \alpha \circ \gamma_2$;

4. If $\gamma_1 < \gamma_2$ and both $\alpha \bullet \gamma_1$ and $\alpha \bullet \gamma_2$ are defined, then $\alpha \bullet \gamma_1 < \alpha \bullet \gamma_2$;

5. If $\gamma_1 \# \gamma_2$, then $\alpha \circ \gamma_1 \# \alpha \circ \gamma_2$;

6. If $\gamma < \alpha \circ \gamma'$, then either $\gamma = [\alpha] \sim \alpha \circ \gamma < \gamma'$;

7. If $\mathrm{part}(\alpha_1) \cap \mathrm{part}(\alpha_2) = \emptyset$, then $\alpha_1 \circ (\alpha_2 \circ \gamma) = \alpha_2 \circ (\alpha_1 \circ \gamma)$;

8. If $\mathrm{part}(\alpha_1) \cap \mathrm{part}(\alpha_2) = \emptyset$ and both $\alpha_2 \bullet (\alpha_1 \circ \gamma)$, $\alpha_2 \bullet \gamma$ are defined, then $\alpha_1 \circ (\alpha_2 \bullet \gamma) = \alpha_2 \bullet (\alpha_1 \circ \gamma)$.

The next lemma relates the retrieval and residual operator with the global types in the branches of choices.

### Lemma 8.11. The following hold:

1. If $\gamma \in \mathcal{G}(G)$, then $pq\lambda \circ \gamma \in \mathcal{G}(p \to q : \coprod_{i \in I} \lambda_i; G_i)$, where $\lambda = \lambda_k$ and $G = G_k$ for some $k \in I$;

2. If $\gamma \in \mathcal{G}(p \to q : \coprod_{i \in I} \lambda_i; G_i)$ and $pq\lambda_k \circ \gamma$ is defined, then $pq\lambda_k \circ \gamma \in \mathcal{G}(G_k)$, where $k \in I$.

The following lemma plays the role of Lemma 8.6 for n-events.

### Lemma 8.12. Let $G \xrightarrow{\alpha} G'$.

1. If $\gamma \in \mathcal{G}(G')$, then $\alpha \circ \gamma \in \mathcal{G}(G)$;

2. If $\gamma \in \mathcal{G}(G)$ and $\alpha \circ \gamma$ is defined, then $\alpha \circ \gamma \in \mathcal{G}(G')$.

Each non-empty trace gives rise to a sequence of g-events, compare with Definition 8.3.

**Definition 8.13 (Building sequences of g-events from traces).** We define the sequence of g-events corresponding to a non-empty trace $\sigma$ by

$$ \mathrm{gec}(\sigma) = \gamma_1; \cdots; \gamma_n $$

where $\gamma_i = \mathrm{ev}(\sigma[1 \dots i])$ for all $i, 1 \le i \le n$.

We show that $\mathrm{gec}(\cdot)$ has similar properties as $\mathrm{nec}(\cdot)$, see Lemma 8.4(1). The proof is straightforward.

### Lemma 8.14. Let $\mathrm{gec}(\sigma) = \gamma_1; \cdots; \gamma_n$.
1. $\mathrm{cm}(\gamma_i) = \sigma[i]$ for all $i, 1 \le i \le n$.

2. If $1 \le h, k \le n$, then $\neg(\gamma_h \# \gamma_k)$.

We may now prove the correspondence between the traces labelling the transition sequences of a global type and the proving sequences of its PES. Let us stress the difference between the set of traces $\mathrm{Tr}^+(G)$ of a global type $G$ as defined at page 20 and the set of traces that label the transition sequences of $G$, which is a larger set due to the internal Rule [ICOMM] of the LTS for global types given in Figure 4.

**Theorem 8.15.** If $G \xrightarrow{\sigma} G'$, then $\mathrm{gec}(\sigma)$ is a proving sequence in $S^G(G)$.

**Proof** By induction on $\sigma$.

*Base case.* Let $\sigma = \alpha$, then $\mathrm{gec}(\alpha) = [\alpha]_{\sim}$. We use a further induction on the inference of the transition $G \xrightarrow{\alpha} G'$.

Let $G = p \to q : \coprod_{i \in I} \lambda_i; G_i$, $G' = G_h$ and $\alpha = \mathrm{pq}\lambda_h$ for some $h \in I$. By Definition 7.11(1) $[\mathrm{pq}\lambda_h]_{\sim} \in \mathcal{GE}(G)$.

Let $G = p \to q : \coprod_{i \in I} \lambda_i; G_i$ and $G' = p \to q : \coprod_{i \in I} \lambda_i; G'_i$ and $G_i \xrightarrow{\alpha} G'_i$ for all $i \in I$ and $\mathrm{part}(\alpha) \cap \{p, q\} = \emptyset$. By induction $[\alpha]_{\sim} \in \mathcal{GE}(G_i)$ for all $i \in I$. By Lemma 8.11(1) $\mathrm{pq}\lambda_i \circ [\alpha]_{\sim} \in \mathcal{GE}(G)$ for all $i \in I$. By Definition 7.11(1) $\mathrm{pq}\lambda_i \circ [\alpha]_{\sim} = [\alpha]_{\sim}$, since $\mathrm{part}(\alpha) \cap \{p, q\} = \emptyset$. We conclude $[\alpha]_{\sim} \in \mathcal{GE}(G)$.

*Inductive case.* Let $\sigma = \alpha \cdot \sigma'$ with $\sigma' \neq \epsilon$. From $G \xrightarrow{\sigma} G'$ we get $G \xrightarrow{\alpha} G'' \xrightarrow{\sigma'} G'$ for some $G''$. Let $\mathrm{gec}(\sigma) = \gamma_1; \dots; \gamma_n$ and $\mathrm{gec}(\sigma') = \gamma'_2; \dots; \gamma'_n$. By induction $\mathrm{gec}(\sigma')$ is a proving sequence in $S^G(G'')$. By Definitions 8.13 and 7.6 $\gamma_i = \alpha \circ \gamma'_i$, which implies $\alpha \cdot \gamma_i = \gamma'_i$ by Lemma 8.10(2) for all $i, 2 \le i \le n$.

We can show that $\gamma_1 = [\alpha]_{\sim} \in \mathcal{GE}(G)$ as in the proof of the base case. By Lemma 8.12(1) $\gamma_i \in \mathcal{GE}(G)$ since $\gamma'_i \in \mathcal{GE}(G'')$ and $\alpha \cdot \gamma_i = \gamma'_i$ for all $i, 2 \le i \le n$. We prove that $\mathrm{gec}(\sigma)$ is a proving sequence in $S^G(G)$. Let $\gamma < \gamma_k$ for some $k, 1 \le k \le n$.

Note that this implies $k > 1$. Since $\gamma_k = \alpha \circ \gamma'_k$ by Lemma 8.10(6) either $\gamma = [\alpha]_{\sim}$ or $\alpha \cdot \gamma < \gamma'_k$. If $\gamma = [\alpha]_{\sim} = \gamma_1$ we are done. Otherwise $\alpha \cdot \gamma \in \mathcal{GE}(G'')$ by Lemma 8.11(2).

Since $\mathrm{gec}(\sigma')$ is a proving sequence in $S^G(G'')$, there is $h < k$ such that $\alpha \cdot \gamma = \gamma'_h$ and this implies $\gamma = \alpha \circ (\alpha \cdot \gamma) = \alpha \circ \gamma'_h = \gamma_h$ by Lemma 8.10(1).

**Theorem 8.16.** If $\gamma_1; \dots; \gamma_n$ is a proving sequence in $S^G(G)$, then $G \xrightarrow{\sigma} G'$, where $\sigma = \mathrm{cm}(\gamma_1) \cdots \mathrm{cm}(\gamma_n)$.

**Proof** The proof is by induction on the length $n$ of the proving sequence. Let $\mathrm{cm}(\gamma_1) = \alpha$ and $\{p, q\} = \mathrm{part}(\alpha)$.

*Case* $n = 1$. Since $\gamma_1$ is the first event of a proving sequence, we have $\gamma_1 = [\alpha]_{\sim}$. We show this case by induction on $d = \mathrm{depth}(G, p) = \mathrm{depth}(G, q)$.

*Case* $d = 1$. Let $\alpha = \mathrm{pq}\lambda$ and $G = p \to q : \coprod_{i \in I} \lambda_i; G_i$ and $\lambda = \lambda_h$ for some $h \in I$. Then $G \xrightarrow{\alpha} G_h$ by rule [ECOMM].

*Case* $d > 1$. Let $G = r \to s : \coprod_{i \in I} \lambda_i; G_i$ and $\{r, s\} \cap \{p, q\} = \emptyset$. By Definition 8.9(1) $\mathrm{rs}\lambda_i \cdot \gamma_1$ is defined for all $i \in I$ since $\{r, s\} \cap \{p, q\} = \emptyset$. This implies $\mathrm{rs}\lambda_i \cdot \gamma_1 \in \mathcal{GE}(G_i)$ for all $i \in I$ by Lemma 8.11(2). By induction hypothesis $G_i \xrightarrow{\alpha} G'_i$ for all $i \in I$. Then we can apply rule [ICOMM] to derive $G \xrightarrow{\alpha} r \to s : \coprod_{i \in I} \lambda_i; G'_i$.
Case $n > 1$. Let $G \xrightarrow{\alpha} G''$ be the transition as obtained from the base case. We show that $\alpha \cdot \gamma_j$ is defined for all $j, 2 \le j \le n$. If $\alpha \cdot \gamma_k$ were undefined for some $k, 2 \le k \le n$, then by Definition 8.9(1) either $\gamma_k = \gamma_1$ or $\gamma_k = [\sigma] \sim$ with $\sigma \ne \alpha \cdot \sigma'$ and part($\alpha) \cap part(\sigma) \ne \emptyset$. In the second case $\alpha @ p \# \sigma @ p$ or $\alpha @ q \# \sigma @ q$, which implies $\gamma_k \# \gamma_1$. So both cases are impossible. If $\alpha \cdot \gamma_j$ is defined, by Lemma 8.12(2) we get $\alpha \cdot \gamma_j \in \mathcal{G}(G'')$ for all $j, 2 \le j \le n$.

We show that $\gamma'_2; \cdots; \gamma'_n$ is a proving sequence in $S^G(G'')$ where $\gamma'_j = \alpha \cdot \gamma_j$ for all $j, 2 \le j \le n$. By Lemma 8.10(1) $\gamma_j = \alpha \circ \gamma'_j$ for all $j, 2 \le j \le n$. Then by Lemma 8.10(5) no two events in the sequence $\gamma'_2; \cdots; \gamma'_n$ can be in conflict. Let $\gamma \in \mathcal{G}(G'')$ and $\gamma < \gamma'_h$ for some $h, 2 \le h \le n$. By Lemma 8.12(1) $\alpha \circ \gamma$ and $\alpha \circ \gamma'_h$ belong to $\mathcal{G}(G)$. By Lemma 8.10(3) $\alpha \circ \gamma < \alpha \circ \gamma'_h$. By Lemma 8.10(1) $\alpha \circ \gamma'_h = \gamma_h$. Let $\gamma' = \alpha \circ \gamma$. Then $\gamma' < \gamma_h$ implies, by Definition 3.6 and the fact that $S^G(G)$ is a PES, that there is $k < h$ such that $\gamma' = \gamma_k$. By Lemma 8.10(1) we get $\gamma = \alpha \cdot \gamma' = \alpha \cdot \gamma_k = \gamma'_k$.

Since $\gamma'_2; \cdots; \gamma'_n$ is a proving sequence in $S^G(G'')$, by induction $G'' \xrightarrow{\sigma'} G'$ where $\sigma' = \mathrm{cm}(\gamma'_2) \cdots \mathrm{cm}(\gamma'_n)$. Let $\sigma = \mathrm{cm}(\gamma_1) \cdots \mathrm{cm}(\gamma_n)$. Since $\mathrm{cm}(\gamma'_j) = \mathrm{cm}(\gamma_j)$ for all $j, 2 \le j \le n$, we have $\sigma = \alpha \cdot \sigma'$. Hence $G \xrightarrow{\alpha} G'' \xrightarrow{\sigma'} G'$ is the required transition sequence.

The last ingredient required to prove our main theorem is the following separation result from [9] (Lemma 2.8 p. 12):

**Lemma 8.17 (Separation [9]).** Let $S = (E, <, \#)$ be a flow event structure and $\mathcal{X}, \mathcal{X}' \in C(S)$ be such that $\mathcal{X} \subset \mathcal{X}'$. Then there exist $e \in \mathcal{X}' \setminus \mathcal{X}$ such that $\mathcal{X} \cup \{e\} \in C(S)$.

We may now finally show the correspondence between the configurations of the FES of a network and the configurations of the PES of its global type. Let $\approx$ denote isomorphism on domains of configurations.

**Theorem 8.18 (Isomorphism).** If $\vdash N : G$, then $\mathcal{D}(S^N(N)) \cong \mathcal{D}(S^G(G))$.

**Proof** By Theorem 8.8 if $v_1; \cdots; v_n$ is a proving sequence of $S^N(N)$, then $N \xrightarrow{\sigma} N'$ where $\sigma = \mathrm{cm}(v_1) \cdots \mathrm{cm}(v_n)$. By applying iteratively Subject Reduction (Theorem 6.10) $G \xrightarrow{\sigma} G'$ and $\vdash N' : G'$. By Theorem 8.15 $\mathrm{gec}(\sigma)$ is a proving sequence of $S^G(G)$.

By Theorem 8.16 if $\gamma_1; \cdots; \gamma_n$ is a proving sequence of $S^G(G)$, then $G \xrightarrow{\sigma} G'$ where $\sigma = \mathrm{cm}(\gamma_1) \cdots \mathrm{cm}(\gamma_n)$. By applying iteratively Session Fidelity (Theorem 6.11) $N \xrightarrow{\sigma} N'$ and $\vdash N' : G'$. By Theorem 8.7 $\mathrm{nec}(\sigma)$ is a proving sequence of $S^N(N)$.

Therefore we have a bijection between $\mathcal{D}(S^N(N))$ and $\mathcal{D}(S^G(G))$, given by $\mathrm{nec}(\sigma) \leftrightarrow \mathrm{gec}(\sigma)$ for any $\sigma$ generated by the (bisimilar) LTSs of N and G.

We show now that this bijection preserves inclusion of configurations. By Lemma 8.17 it is enough to prove that if $v_1; \cdots; v_n \in C(S^N(N))$ is mapped to $\gamma_1; \cdots; \gamma_n \in C(S^G(G))$, then $v_1; \cdots; v_n; v \in C(S^N(N))$ iff $\gamma_1; \cdots; \gamma_n; \gamma \in C(S^G(G))$, where $\gamma_1; \cdots; \gamma_n; \gamma$ is the image of $v_1; \cdots; v_n; v$ under the bijection. I.e. let $\mathrm{nec}(\sigma \cdot \alpha) = v_1; \cdots; v_n; v$ and $\mathrm{gec}(\sigma \cdot \alpha) = \gamma_1; \cdots; \gamma_n; \gamma$. This implies $\sigma = \mathrm{cm}(v_1) \cdots \mathrm{cm}(v_n) = \mathrm{cm}(\gamma_1) \cdots \mathrm{cm}(\gamma_n)$ and $\alpha = \mathrm{cm}(v) = \mathrm{cm}(\gamma)$ by Lemmas 8.4 and 8.14.
1124 **9. Related Work and Conclusions**

Event Structures (ESs) were introduced in Winskel's PhD Thesis [60] and in the seminal paper by Nielsen, Plotkin and Winskel [49], roughly in the same frame of time as Milner's calculus CCS [47]. It is therefore not surprising that the relationship between these two approaches for modelling concurrent computations started to be investigated very soon afterwards. The first interpretation of CCS into ESs was proposed by Winskel in [61]. This interpretation made use of Stable ESs, because PESs, the simplest form of ESs, appeared not to be flexible enough to account for CCS parallel composition. Indeed, since CCS parallel composition allows for two concurrent complementary actions to either synchronise or occur independently in any order, each pair of such actions gives rise to two forking computations: this requires duplication of the same continuation process for these forking computations in PESs, while the continuation process may be shared by the forking computations in Stable ESs, which allow for disjunctive causality. Subsequently, ESs (as well as other nonsequential "denotational models" for concurrency such as Petri Nets) have been used as the touchstone for assessing noninterleaving operational semantics for CCS: for instance, the pomset semantics for CCS by Boudol and Castellani [7, 8] and the semantics based on "concurrent histories" proposed by Degano, De Nicola and Montanari [29, 27, 28], were both shown to agree with an interpretation of CCS processes into some class of ESs (PESs for [27, 28], PESs with non-hereditary conflict for [7], and FESs for [8]). Among the early interpretations of process calculi into ESs, we should also mention the PES semantics for TCSP (Theoretical CSP [11, 50]), proposed by Goltz and Loogen [46] and later generalised by Baier and Majster-Cederbaum [2], and the Bundle ES semantics for LOTOS, proposed by Langerak [45] and extended by Katoen [43]. Like FESs, Bundle ESs are a subclass of Stable ESs. We recall the relationships between the above classes of ESs (the reader is referred to [10] for separating examples):

$$ \textit{Prime ESs} \subset \textit{Bundle ESs} \subset \textit{Flow ESs} \subset \textit{Stable ESs} \subset \textit{General ESs} $$

<footnote n="1118">1118 By Theorem 8.8, if $v_1; \dots; v_n; v$ is a proving sequence of $S^N(N)$, then $N \xrightarrow{\sigma} N_0 \xrightarrow{\alpha}$ $N'$. By applying iteratively Subject Reduction (Theorem 6.10) $G \xrightarrow{\sigma} G_0 \xrightarrow{\alpha} G'$ and $\vdash N' : G'$. By Theorem 8.15 $\mathbf{gec}(\sigma \cdot \alpha)$ is a proving sequence of $S^G(G)$.</footnote>

<footnote n="1121">1121 By Theorem 8.16, if $\gamma_1; \dots; \gamma_n; \gamma$ is a proving sequence of $S^G(G)$, then $G \xrightarrow{\sigma} G_0 \xrightarrow{\alpha} G'$. By applying iteratively Session Fidelity (Theorem 6.11) $N \xrightarrow{\sigma} N_0 \xrightarrow{\alpha} N'$ and $\vdash N' : G'$. By Theorem 8.7 $\mathbf{nec}(\sigma \cdot \alpha)$ is a proving sequence of $S^N(N)$.</footnote>

<footnote n="1125">1125 More sophisticated ES semantics for CCS, based on FESs and designed to be robust under action refinement [1, 26, 34], were subsequently proposed by Goltz and van Glabbeek [57]. Importantly, all the above-mentioned classes of ESs, except General ESs, give rise to the same *prime algebraic domains* of configurations, from which one can recover a PES by selecting the complete prime elements.</footnote>

<footnote n="1126">1126 More recently, ES semantics have been investigated for the $\pi$-calculus by Crafa, Varacca and Yoshida [21, 58, 22] and by Cristescu, Krivine and Varacca [23, 24, 25].
1131 Previously, other causal models for the $\pi$-calculus had already been put forward</footnote>
1133 by Jategaonkar and Jagadeesan [42], by Montanari and Pistore [48], by Cattani and
1134 Sewell [18] and by Bruni, Melgratti and Montanari [12]. The main new issue, when
1135 addressing causality-based semantics for the π-calculus, is the implicit causality
1136 induced by scope extrusion. Two alternative views of such implicit causality had
1137 been proposed in early work on noninterleaving operational semantics for the π-
1138 calculus, respectively by Boreale and Sangiorgi [6] and by Degano and Priami [30].
1139 Essentially, in [6] an *extruder* (that is, an output of a private name) is considered to
1140 cause any action that uses the extruded name, whether in subject or object position,
1141 while in [30] it is considered to cause only the actions that use the extruded name
1142 in subject position. Thus, for instance, in the process $P = va(\bar{b}\langle a \rangle | \bar{c}\langle a \rangle | a)$, the two
1143 parallel extruders are considered to be causally dependent in the former approach,
1144 and independent in the latter. All the causal models for the π-calculus mentioned
1145 above, including the ES-based ones, take one or the other of these two stands. Note
1146 that opting for the second one leads necessarily to a non-stable ES model, where
1147 there may be causal ambiguity within the configurations themselves: for instance,
1148 in the above example the maximal configuration contains three events, the extruders
1149 $\bar{b}\langle a \rangle$, $\bar{c}\langle a \rangle$ and the input on $a$, and one does not know which of the two extruders
1150 enabled the input. Indeed, the paper [22] uses non-stable ESs. The use of non-stable
1151 ESs (General ESs) to express situations where a computational step can merge parts
1152 of the state is advocated for instance by Baldan, Corradini and Gadducci in [3].
1153 These ESs give rise to configuration domains that are not prime algebraic, hence
1154 the classical representation theorems have to be adjusted.

1155 In our simple setting, where we deal only with single sessions and do not con-
1156 sider session interleaving nor delegation, we can dispense with channels altogether,
1157 and therefore the question of parallel extrusion does not arise. In this sense, our
1158 notion of causality is closer to that of CCS than to the more complex one of the
1159 π-calculus. However, even in a more general setting, where participants would be
1160 paired with the channel name of the session they pertain to, the issue of parallel
1161 extrusion would not arise: indeed, in the above example *b* and *c* should be equal,
1162 because participants can only delegate their own channel, but then they could not
1163 be in parallel because of linearity, one of the distinguishing features enforced by
1164 session types. Hence we believe that in a session-based framework the two above
1165 views of implicit causality should collapse into just one.

1166 We now briefly discuss our design choices.

• The calculus considered in the present paper uses synchronous communication - rather than asynchronous, buffered communication - because this is how communication is classically modelled in ESs, when they are used to give semantics to process calculi. We should mention however that after first proposing the present study in [15], we also considered a calculus with asynchronous communication in the companion paper [16]. In that work too, networks are interpreted as FESs, and their associated global types, which we called asynchronous types as they split communications into outputs and inputs, are interpreted as PESs. The key result is again an isomorphism between the configuration domain of the FES of a typed network and that of the PES of its type.
1178

1179

1180

1181

1182

* Concerning the choice operator, we adopted here the basic (and most restrictive) variant for it, as it was originally proposed for multiparty session calculi in [39]. This is essentially a simplifying assumption, and we do not foresee any difficulty in extending our results to a more general choice operator, where the projection is rendered more flexible through the use of a merge operator [31].

1183

1184

1185

1186

1187

1188

1189

1190

1191

1192

1193

* As regards the preorder on processes, which is akin to a subtyping relation, we envisaged to use the standard subtyping, in which a process with fewer outputs can be used in place of a process with more outputs. However, in that case Session Fidelity would become weaker, since a transition in the LTS of a global type would only ensure a transition in the LTS of the corresponding network, but not necessarily with the same labelling communication. The main drawback would be that Theorem 8.18 would no longer hold: more precisely, the domains of network configurations would only be embedded in (and not isomorphic to) the domains of their global type configurations. Notably, typability is independent from the use of our preorder or of the standard one, as proved in [4].

1194

1195

1196

1197

1198

1199

1200

1201

As regards future work, we plan to define an asynchronous transition system (ATS) [5] for our calculus, along the lines of [10], and show that it provides a noninterleaving operational semantics for networks that is equivalent to their FES semantics. This would enable us also to investigate the issue of reversibility, jointly on our networks and on their FES representations, since the ATS semantics would give us the handle to unwind networks, while the corresponding FESs could be unrolled following one of the methods proposed in existing work on reversible event structures [53, 25, 36, 37, 35].

1202

1203

1204

1205

1206

1207

1208

1209

1210

1211

1212

1213

As mentioned at the end of Section 7, the quest for a semantic counterpart of our well-formedness conditions on global types – namely, for properties that characterise the FESs obtained from typable networks – is still open. By way of comparison, such semantic well-formedness conditions have been proposed in [56] for graphical choreographies, a truly concurrent graphical model for global specifications with two kinds of forking nodes, representing respectively choice and parallel composition. In [56], those well-formedness conditions, called well-sequencing and well-branchedness, were shown to be sufficient to ensure projectability on local specifications. In our case, the property corresponding to well-sequencing is automatically ensured by our ES semantics, and we conjecture that the well-branchedness condition for choice nodes (corresponding to projectability) could amount in our simpler setting<fnref n="10" /> to the following semantic condition:

1214

1215

1216

Let $v_1, v_2 \in \mathcal{N}\mathcal{E}(N)$ and $p :: \zeta \cdot \pi \in v_1$ and $p :: \zeta \cdot \pi' \in v_2$ with $\pi \neq \pi'$ and $q = pt(\pi) = pt(\pi')$. If $v_1 <^* v'_1$ for some $v'_1 \in \mathcal{N}\mathcal{E}(N)$ such that $r \in \text{loc}(v'_1)$ with $r \notin \{p, q\}$, then $v_2 <^* v'_2$ for some $v'_2 \in \mathcal{N}\mathcal{E}(N)$ such that $r \in \text{loc}(v'_2)$.

1217

1218

1219

This condition would allow us to rule out the FESs of both networks $N'$ and $N''$ discussed at the end of Section 7. However, it should be completed with a condition corresponding to boundedness, and the conjunction of these two conditions might

<footnote n="10">¹⁰Our choice operator for global types is less general than that of [56].</footnote>
1220 still not be sufficient in general to ensure typability. We plan to further investigate
1221 this question in the near future.

1222 *Acknowledgment*. We are strongly indebted to the anonymous referees for their
1223 constructive remarks, which helped us improve the submitted version of the paper.

1224 **References**

1225 [1] Luca Aceto and Matthew Hennessy. Towards action-refinement in process
1226 algebras. In Albert R. Meyer, editor, *LICS*, pages 138–145, Washington, 1989.
1227 IEEE Computer Society Press.

1228 [2] Christel Baier and Mila E. Majster-Cederbaum. The connection between an
event structure semantics and an operational semantics for TCSP. *Acta Informatica*, 31(1):81–104, 1994.
1229
1230

1231 [3] Paolo Baldan, Andrea Corradini, and Fabio Gadducci. Domains and event
1232 structures for fusions. In Joel Ouaknine, editor, *LICS*, pages 1–12, Washington,
1233 2017. IEEE Computer Society Press.

1234 [4] Franco Barbanera, Mariangiola Dezani-Ciancaglini, Ivan Lanese, and Emilio
1235 Tuosto. Composition and decomposition of multiparty sessions. *Journal of
1236 Logical and Algebraic Methods in Programming*, 119:100620, 2021.

1237 [5] Marek Bednarczyk. *Categories of Asynchronous Systems*. PhD thesis, University
1238 of Sussex, 1988.

1239 [6] Michele Boreale and Davide Sangiorgi. A fully abstract semantics for causality
1240 in the π-calculus. *Acta Informatica*, 35(5):353–400, 1998.

1241 [7] Gérard Boudol and Ilaria Castellani. On the semantics of concurrency: partial
1242 orders and transition systems. In Hartmut Ehrig, Robert A. Kowalski, Giorgio
1243 Levi, and Ugo Montanari, editors, *TAPSOFT*, volume 249 of LNCS, pages 123–
1244 137, Heidelberg, 1987. Springer.

1245 [8] Gérard Boudol and Ilaria Castellani. Permutation of transitions: an event structure semantics for CCS and SCCS. In Jaco W. de Bakker, Willem P. de Roever, and Grzegorz Rozenberg, editors, *REX: Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency*, volume 354 of LNCS, pages 411–427, Heidelberg, 1988. Springer.
1246
1247
1248
1249

1250 [9] Gérard Boudol and Ilaria Castellani. Flow models of distributed computations: event structures and nets. Research Report 1482, INRIA, 1991.

1252 [10] Gérard Boudol and Ilaria Castellani. Flow models of distributed computations: three equivalent semantics for CCS. *Information and Computation*, 114(2):247–314, 1994.
1253
1254

1255 [11] Stephen Brookes, Charles A.R. Hoare, and Andrew Roscoe. A theory of communicating sequential processes. *Journal of ACM*, 31(3):560–599, 1984.
1256
1257

1258

1259

[12] Roberto Bruni, Hernán C. Melgratti, and Ugo Montanari. Event structure semantics for nominal calculi. In Christel Baier and Holger Hermanns, editors, CONCUR, volume 4137 of LNCS, pages 295–309, Heidelberg, 2006. Springer.

1260

1261

1262

[13] Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In Paul Gastin and François Laroussinie, editors, CONCUR, volume 6269 of LNCS, pages 222–236, Heidelberg, 2010. Springer.

1263

1264

1265

[14] Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logic propositions as session types. *Mathematical Structures in Computer Science*, 26(3):367–423, 2016.

1266

1267

1268

1269

1270

1271

[15] Ilaria Castellani, Mariangiola Dezani-Ciancaglini, and Paola Giannini. Event structure semantics for multiparty sessions. In Michele Boreale, Flavio Corradini, Michele Loreti, and Rosario Pugliese, editors, *Models, Languages, and Tools for Concurrent and Distributed Programming - Essays Dedicated to Rocco De Nicola on the Occasion of His 65th Birthday*, volume 11665 of LNCS, pages 340–363, Heidelberg, 2019. Springer.

1272

1273

1274

[16] Ilaria Castellani, Mariangiola Dezani-Ciancaglini, and Paola Giannini. Global types and event structure semantics for asynchronous multiparty sessions. *CoRR*, abs/2102.00865, 2021.

1275

1276

[17] Ilaria Castellani and Guo Qiang Zhang. Parallel product of event structures. *Theoretical Computer Science*, 179(1-2):203–215, 1997.

1277

1278

[18] Gian Luca Cattani and Peter Sewell. Models for name-passing processes: interleaving and causal. *Information and Computation*, 190(2):136–178, 2004.

1279

1280

1281

[19] Mario Coppo, Mariangiola Dezani-Ciancaglini, Nobuko Yoshida, and Luca Padovani. Global progress for dynamically interleaved multiparty sessions. *Mathematical Structures in Computer Science*, 26(2):238–302, 2016.

1282

1283

[20] Bruno Courcelle. Fundamental properties of infinite trees. *Theoretical Computer Science*, 25:95–169, 1983.

1284

1285

1286

1287

[21] Silvia Crafa, Daniele Varacca, and Nobuko Yoshida. Compositional event structure semantics for the internal π-calculus. In Luís Caires and Vasco T. Vasconcelos, editors, CONCUR, volume 4703 of LNCS, pages 317–332, Heidelberg, 2007. Springer.

1288

1289

1290

[22] Silvia Crafa, Daniele Varacca, and Nobuko Yoshida. Event structure semantics of parallel extrusion in the π-calculus. In Lars Birkedal, editor, FOSSACS, volume 7213 of LNCS, pages 225–239, Heidelberg, 2012. Springer.

1291

1292

[23] Ioana Cristescu. *Operational and denotational semantics for the reversible π-calculus*. PhD thesis, University Paris Diderot - Paris 7, 2015.
1293

1294

1295

1296

[24] Ioana Cristescu, Jean Krivine, and Daniele Varacca. Rigid families for CCS and the π-calculus. In Martin Leucker, Camilo Rueda, and Frank D. Valencia, editors, *ICTAC*, volume 9399 of LNCS, pages 223–240, Heidelberg, 2015. Springer.

1297

1298

1299

[25] Ioana Cristescu, Jean Krivine, and Daniele Varacca. Rigid families for the reversible π-calculus. In Simon J. Devitt and Ivan Lanese, editors, *Reversible Computation*, volume 9720 of LNCS, pages 3–19, Heidelberg, 2016. Springer.

1300

1301

[26] Philippe Darondeau and Pierpaolo Degano. Refinement of actions in event structures and causal trees. *Theoretical Computer Science*, 118(1):21–48, 1993.

1302

1303

1304

[27] Pierpaolo Degano, Rocco De Nicola, and Ugo Montanari. On the consistency of truly concurrent operational and denotational semantics. In Ashok K. Chandra, editor, *LICS*, Washington, 1988. IEEE Computer Society Press Press.

1305

1306

[28] Pierpaolo Degano, Rocco De Nicola, and Ugo Montanari. A partial ordering semantics for CCS. *Theoretical Computer Science*, 75(3):223–262, 1990.

1307

1308

1309

[29] Pierpaolo Degano and Ugo Montanari. Concurrent histories: A basis for observing distributed systems. *Journal of Computer and System Sciences*, 34(2/3):422–461, 1987.

1310

1311

[30] Pierpaolo Degano and Corrado Priami. Non-interleaving semantics for mobile processes. *Theoretical Computer Science*, 216(1-2):237–270, 1999.

1312

1313

[31] Pierre-Malo Deniélou and Nobuko Yoshida. Dynamic multirole session types. In Mooly Sagiv, editor, *POPL*, pages 435–446, New York, 2011. ACM Press.

1314

1315

1316

[32] Pierre-Malo Deniélou and Nobuko Yoshida. Multiparty session types meet communicating automata. In Helmut Seidl, editor, *ESOP*, volume 7211 of LNCS, pages 194–213, Heidelberg, 2012. Springer.

1317

1318

1319

1320

[33] Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, Svetlana Jaksic, Jovanka Pantovic, and Nobuko Yoshida. Precise subtyping for synchronous multiparty sessions. In *PLACES*, volume 203 of EPTCS, pages 29 – 44, Waterloo, 2016. Open Publishing Association.

1321

1322

[34] Ursula Goltz, Roberto Gorrieri, and Arend Rensink. Comparing syntactic and semantic action refinement. *Information and Computation*, 125(2):118–143, 1996.

1323

1324

[35] Eva Graversen. *Event Structure Semantics of Reversible Process Calculi*. PhD thesis, Imperial College London, 2021.

1325

1326

1327

[36] Eva Graversen, Iain Phillips, and Nobuko Yoshida. Towards a categorical representation of reversible event structures. *Journal of Logical and Algebraic Methods in Programming*, 104:16–59, 2019.

1328

1329

1330

[37] Eva Graversen, Iain C. C. Phillips, and Nobuko Yoshida. Event structure semantics of (controlled) reversible CCS. *Journal of Logical and Algebraic Methods in Programming*, 121:100686, 2021.
1331

1332

1333

1334

[38] Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In Chris Hankin, editor, *ESOP*, volume 1381 of *LNCS*, pages 122–138, Heidelberg, 1998. Springer.

1335

1336

1337

[39] Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In George C. Necula and Philip Wadler, editors, *POPL*, pages 273–284, New York, 2008. ACM Press.

1338

1339

[40] Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. *Journal of ACM*, 63(1):9:1–9:67, 2016.

1340

1341

1342

1343

1344

[41] Hans Hüttel, Ivan Lanese, Vasco T. Vasconcelos, Luís Caires, Marco Carbone, Pierre-Malo Deniélou, Dimitris Mostrous, Luca Padovani, António Ravara, Emilio Tuosto, Hugo Torres Vieira, and Gianluigi Zavattaro. Foundations of session types and behavioural contracts. *ACM Computing Surveys*, 49(1):3:1–3:36, 2016.

1345

1346

1347

1348

[42] Lalita Jategaonkar Jagadeesan and Radha Jagadeesan. Causality and true concurrency: A data-flow analysis of the $\pi$-calculus (extended abstract). In Vangalur S. Alagar and Maurice Nivat, editors, *AMAST*, volume 936 of *LNCS*, pages 277–291, Heidelberg, 1995. Springer.

1349

1350

[43] Joost-Pieter Katoen. *Quantitative and qualitative extensions of event structures*. PhD thesis, University of Twente, 1996.

1351

1352

1353

[44] Julien Lange, Emilio Tuosto, and Nobuko Yoshida. From communicating machines to graphical choreographies. In Sriram K. Rajamani and David Walker, editors, *POPL*, pages 221–232, New York, 2015. ACM Press.

1354

1355

1356

1357

[45] Rom Langerak. Bundle event structures: a non-interleaving semantics for LOTOS. In Michael Diaz and Roland Groz, editors, *Formal Description Techniques for Distributed Systems and Communication Protocols*, pages 331–346, Amsterdam, 1993. North-Holland.

1358

1359

[46] Rita Loogen and Ursula Goltz. Modelling nondeterministic concurrent processes with event structures. *Fundamenta Informaticae*, 14(1):39–74, 1991.

1360

1361

[47] Robin Milner. *A Calculus of Communicating Systems*, volume 92 of LNCS. Springer, Heidelberg, 1980.

1362

1363

1364

[48] Ugo Montanari and Marco Pistore. Concurrent semantics for the $\pi$-calculus. In Stephen Brookes, Michael Main, Austin Melton, and Michael Mislove, editors, *MFPS*, volume 1 of ENTCS, pages 411–429, Oxford, 1995. Elsevier.

1365

1366

[49] Mogens Nielsen, Gordon Plotkin, and Glynn Winskel. Petri nets, event structures and domains, part I. *Theoretical Computer Science*, 13(1):85–108, 1981.
[50] Ernst-Rüdiger Olderog. TCSP: theory of communicating sequential processes. In Wilfried Brauer, Wolfgang Reisig, and Grzegorz Rozenberg, editors, *Advances in Petri Nets*, volume 255 of LNCS, pages 441–465, Heidelberg, 1986. Springer.

[51] Luca Padovani. Type reconstruction for the linear π-calculus with composite regular types. *Logical Methods in Computer Science*, 11(4), 2015.

[52] Jorge A. Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logical relations and observational equivalences for session-based concurrency. *Information and Computation*, 239:254–302, 2014.

[53] Iain Phillips and Irek Ulidowski. Reversibility and asymmetric conflict in event structures. *Journal of Logical and Algebraic Methods in Programming*, 84(6):781–805, 2015.

[54] Kaku Takeuchi, Kohei Honda, and Makoto Kubo. An interaction-based language and its typing system. In Chris Hankin, editor, *PARLE*, volume 817 of LNCS, pages 122–138, Heidelberg, 1994. Springer.

[55] Bernardo Toninho, Luís Caires, and Frank Pfenning. Dependent session types via intuitionistic linear type theory. In Peter Schneider-Kamp and Michael Hanus, editors, *PPDP*, pages 161–172, New York, 2011. ACM Press.

[56] Emilio Tuosto and Roberto Guanciale. Semantics of global view of choreographies. *Journal of Logic and Algebraic Methods in Programming*, 95:17–40, 2018.

[57] Rob J. van Glabbeek and Ursula Goltz. Well-behaved flow event structures for parallel composition and action refinement. *Theoretical Computer Science*, 311(1-3):463–478, 2004.

[58] Daniele Varacca and Nobuko Yoshida. Typed event structures and the linear π-calculus. *Theoretical Computer Science*, 411(19):1949–1973, 2010.

[59] Philip Wadler. Propositions as sessions. *Journal of Functional Programming*, 24(2-3):384–418, 2014.

[60] Glynn Winskel. *Events in Computation*. PhD thesis, University of Edinburgh, 1980.

[61] Glynn Winskel. Event structure semantics for CCS and related languages. In Mogens Nielsen and Erik Meineche Schmidt, editors, *ICALP*, volume 140 of LNCS, pages 561–576, Heidelberg, 1982. Springer.

[62] Glynn Winskel. An introduction to event structures. In Jaco W. de Bakker, Willem P. de Roever, and Grzegorz Rozenberg, editors, *REX: Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency*, volume 354 of LNCS, pages 364–397, Heidelberg, 1988. Springer.
1403

# Appendices

1404

## A. Proofs of Section 5

1405

This section contains the proofs of Lemmas 5.18, 5.21 and 5.24.

1406

1407

**Lemma 5.18** Let $v$ and $v'$ be binary $n$-events with $\text{loc}(v) = \text{loc}(v')$. Then $v \# v'$ iff $p :: \eta \in v$ and $p :: \eta' \in v'$ imply $\eta \# \eta'$.

1408

1409

1410

1411

1412

1413

1414

1415

**Proof** The "if" direction holds by Definition 5.7(2a). We show the "only-if" direction. First observe that for any $n$-event $v = \{p :: \eta_1, q :: \eta_2\}$ the condition $p :: \eta_1 \widehat{\nsim} q :: \eta_2$ of Definition 5.5 implies $\eta_1 \vdash q \bowtie \eta_2 \vdash p$ by Definition 5.4, which in turn implies $|\eta_1 \vdash q| = |\eta_2 \vdash p|$ by Definition 5.3. If $v$ is a binary event, we also have $|\eta_1| = |\eta_1 \vdash q|$ and $|\eta_2| = |\eta_2 \vdash p|$ by Definition 5.2, since all the actions of $\eta_1$ involve $q$ and all the actions of $\eta_2$ involve $p$, and thus the projections do not erase actions. Assume now $v' = \{p :: \eta'_1, q :: \eta'_2\}$. We consider two cases (the others being symmetric):

1416

- $v \# v'$ because $\eta_1 \# \eta'_1$. Then $\eta_1 \vdash q \bowtie \eta_2 \vdash p$ and $\eta'_1 \vdash q \bowtie \eta'_2 \vdash p$ imply $\eta_2 \# \eta'_2$;

1417

1418

1419

1420

1421

- $v \# v'$ because $|\eta_1 \vdash q| = |\eta'_2 \vdash p|$ and $\neg(\eta_1 \vdash q \bowtie \eta'_2 \vdash p)$. As argued before, we have $|\eta_2 \vdash p| = |\eta_1 \vdash q|$ and $|\eta'_2 \vdash p| = |\eta'_1 \vdash q|$. Then, from $|\eta_1 \vdash q| = |\eta'_2 \vdash p|$ and the above remark about binary events, we get $|\eta_2| = |\eta_1| = |\eta'_2| = |\eta'_1|$. From $\neg(\eta_1 \vdash q \bowtie \eta'_2 \vdash p)$ it follows that $\eta_1 \neq \eta'_1$ and $\eta_2 \neq \eta'_2$. Then we may conclude, since $|\eta_i| = |\eta'_i|$ and $\eta_i \neq \eta'_i$ imply $\eta_i \# \eta'_i$ for $i = 1, 2$.

1422

1423

**Lemma 5.21 (Sharing of located events implies conflict)** If $v, v' \in \mathcal{NE}$ and $v \neq v'$ and $(v \cap v') \neq \emptyset$, then $v \# v'$.

1424

1425

1426

1427

1428

**Proof** Let $p :: \eta \in (v \cap v')$ and $\text{loc}(v) = \text{loc}(v') = \{p, q\}$. Then there must exist $\eta_0, \eta'_0$ such that $q :: \eta_0 \in v$ and $q :: \eta'_0 \in v'$. From $p :: \eta \widehat{\nsim} q :: \eta_0$ and $p :: \eta \widehat{\nsim} q :: \eta'_0$ it follows that $\eta_0 \vdash p = \eta'_0 \vdash p$. This, in conjunction with the fact that $\text{pt}(\text{act}(\eta_0)) = \text{pt}(\text{act}(\eta'_0)) = p$, implies that neither $\eta_0 < \eta'_0$ nor $\eta'_0 < \eta_0$. Thus $\eta_0 \# \eta'_0$ and therefore $v \# v'$ by Definition 5.7.

1429

1430

**Lemma 5.24** If $\mathcal{X}$ is a configuration of $S^N(\mathcal{N})$ and $v \in \mathcal{X}$, then there is a unique causal set $E$ of $v$ such that $E \subseteq \mathcal{X}$.

1431

1432

1433

1434

1435

1436

1437

1438

**Proof** By Definition 5.11, if $v \in \mathcal{NE}(\mathcal{N})$, then $v$ has at least one causal set included in $\mathcal{NE}(\mathcal{N})$. Let $E' = \{v' \in \mathcal{X} | v' < v\}$. By Definition 3.4, $E' \cup \{v\}$ is conflict-free. Moreover, if $p :: \eta \in v$ and $\eta' < \eta$, then by Lemma 5.21 there is at most one $v'' \in E'$ such that $p :: \eta' \in v''$. Therefore, $E' \subseteq E$ for some causal set $E$ of $v$ by Definition 5.9. We show that $E \subseteq E'$. Assume ad absurdum that $v_0 \in E \setminus E'$. By definition of causal set, $v_0 < v$. By definition of $E'$, $v_0 \notin E'$ implies $v_0 \notin \mathcal{X}$. By Definition 3.4 this implies $v_0 \# v_1 < v$ for some $v_1 \in \mathcal{X}$. Then $v_1 \in E'$ by definition of $E'$, and thus $v_1 \in E$. Hence $v_0, v_1 \in E$ and $v_0 \# v_1$, contradicting Definition 5.9.
### B. Proofs of Section 6

This section contains the proofs of Lemmas 6.6, 6.9, Theorems 6.10, 6.11 and of the auxiliary Lemmas B.1, B.2, B.3.

**Lemma 6.6** If $G$ is bounded, then $G \uparrow r$ is a partial function for all $r$.

**Proof** We redefine the projection $\downarrow r$ as the largest relation between global types and processes such that $(G, P) \in \downarrow r$ implies:

i) if $r \notin \text{part}(G)$, then $P = 0$;

ii) if $G = r \to p : \coprod_{i \in I} \lambda_i; G_i$, then $P = \bigoplus_{i \in I} q! \lambda_i; P_i$ and $(G_i, P_i) \in \downarrow r$ for all $i \in I$;

iii) if $G = p \to r : \coprod_{i \in I} \lambda_i; G_i$, then $P = \sum_{i \in I} p? \lambda_i; P_i$ and $(G_i, P_i) \in \downarrow r$ for all $i \in I$;

iv) if $G = p \to q : \coprod_{i \in I} \lambda_i; G_i$ and $r \notin \{p, q\}$ and $r \in \text{part}(G_i)$, then $(G_i, P) \in \downarrow r$ for all $i \in I$.

The equality $\mathcal{E}$ of processes is the largest symmetric binary relation $\mathcal{R}$ on processes such that $(P, Q) \in \mathcal{R}$ implies:

(a) if $P = \bigoplus_{i \in I} p! \lambda_i; P_i$, then $Q = \bigoplus_{i \in I} p! \lambda_i; Q_i$ and $(P_i, Q_i) \in \mathcal{R}$ for all $i \in I$;

(b) if $P = \sum_{i \in I} p? \lambda_i; P_i$, then $Q = \sum_{i \in I} p? \lambda_i; Q_i$ and $(P_i, Q_i) \in \mathcal{R}$ for all $i \in I$.

It is then enough to show that the relation

$$ \mathcal{R}_r = \{(P, Q) \mid \exists G. (G, P) \in \downarrow r \text{ and } (G, Q) \in \downarrow r\} $$

satisfies Clauses (a) and (b) (with $\mathcal{R}$ replaced by $\mathcal{R}_r$), since this will imply $\mathcal{R}_r \subseteq \mathcal{E}$.

Note first that $(0, 0) \in \mathcal{R}_r$ because $(\text{End}, 0) \in \downarrow r$, and that $(0, 0) \in \mathcal{E}$ because Clauses (a)

and (b) are vacuously satisfied by the pair $(0, 0)$. The proof is by induction on

$d = \text{depth}(G, r)$. We only consider Clause (b), the proof for Clause (a) being similar.

So, assume $(P, Q) \in \mathcal{R}_r$ and $P = \sum_{i \in I} p? \lambda_i; P_i$.

Case $d = 1$. In this case $G = p \to r : \coprod_{i \in I} \lambda_i; G_i$ and $P = \sum_{i \in I} p? \lambda_i; P_i$ and $(G_i, P_i) \in \downarrow r$

for all $i \in I$. From $(G, Q) \in \downarrow r$ we get $Q = \sum_{i \in I} p? \lambda_i; Q_i$ and $(G_i, Q_i) \in \downarrow r$ for all $i \in I$.

Hence $Q$ has the required form and $(P_i, Q_i) \in \mathcal{R}_r$ for all $i \in I$.

Case $d > 1$. In this case $G = p \to q : \coprod_{j \in J} \lambda'_j; G_j$ and $r \notin \{p, q\}$ and $(G_j, P) \in \downarrow r$ for all

$j \in J$. From $(G, Q) \in \downarrow r$ we get $(G_j, Q) \in \downarrow r$ for all $j \in J$. Then $(P, Q) \in \mathcal{R}_r$.

We need a lemma relating the projections of a well-formed global type with its transitions.

**Lemma B.1.** Let $G$ be a well-formed global type.

1. If $G \uparrow p = \bigoplus_{i \in I} q! \lambda_i; P_i$ and $G \uparrow q = \sum_{j \in J} p? \lambda'_j; Q_j$, then $I = J$, $\lambda_i = \lambda'_i$, $G \xrightarrow{pq\lambda_i} G_i$, $G_i \uparrow p = P_i$ and $G_i \uparrow q = Q_i$ for all $i \in I$.

2. If $G \xrightarrow{pq\lambda} G'$, then $G \uparrow p = \bigoplus_{i \in I} q! \lambda_i; P_i$, $G \uparrow q = \sum_{i \in I} p? \lambda_i; Q_i$, where $\lambda_k = \lambda$ for some $k \in I$, and $G' \uparrow r = G \uparrow r$ for all $r \notin \{p, q\}$.
1471 **Proof** (1). The proof is by induction on $d = \text{depth}(G, p)$.

1472 If $d=1$, then by definition of projection (see Figure 2) $G \upharpoonright p = \bigoplus_{i \in I} q!\lambda_i; P_i$ implies
1473 $G = p \to q : \coprod_{i \in I} \lambda_i; G_i$ with $G_i \upharpoonright p = P_i$. By the same definition $G \upharpoonright q = \sum_{j \in J} p?\lambda'_j; Q_j$

1474 implies $J = I$ and $\lambda'_j = \lambda_j$ and $Q_j = G_j \upharpoonright q$ for all $j \in J$. Moreover $G \xrightarrow{pq\lambda_i} G_i$ by Rule [ECOMM] for all $i \in I$.

1475 If $d > 1$, then $G = r \to s : \coprod_{h \in H} \lambda_h''; G'_h$ with $\{p,q\} \cap \{r,s\} = \emptyset$. By definition of projection $G \upharpoonright p = G'_h \upharpoonright p$ and $G \upharpoonright q = G'_h \upharpoonright q$ for all $h \in H$. By Lemma 6.5 depth($G$, $p$) > depth($G'_h$, $p$) for all $h \in H$. Then by induction $I = J$, $\lambda_i = \lambda'_i$,

1476 $G'_h \xrightarrow{pq\lambda_i} G'_h$, $G'_h \upharpoonright p = P_i$ and $G'_h \upharpoonright q = Q_i$ for all $i \in I$ and all $h \in H$. Let
1477 $G_i = r \to s : \coprod_{h \in H} \lambda_h''; G'_h$. By Rule [ICOMM] $G \xrightarrow{pq\lambda_i} G_i$ for all $i \in I$. By definition of projection $G_i \upharpoonright p = P_i$ and $G_i \upharpoonright q = Q_i$ for all $i \in I$.

1478 (2). The proof is by induction on the transition rules of Figure 4.

1479 The interesting case is:
$$ \frac{G_h \xrightarrow{pq\lambda} G'_h \quad h \in H \quad \{p,q\} \cap \{s,t\} = \emptyset}{s \to t : \coprod_{h \in H} \lambda'_h; G_h \xrightarrow{pq\lambda} s \to t : \coprod_{h \in H} \lambda'_h; G'_h} \quad [\text{ICOMM}] $$

1480 with $G = s \to t : \coprod_{h \in H} \lambda'_h; G_h$ and $G' = s \to t : \coprod_{h \in H} \lambda'_h; G'_h$. By induction
1481 $G_h \upharpoonright p = \bigoplus_{i \in I} q!\lambda_i; P_i$, $G_h \upharpoonright q = \sum_{j \in J} p?\lambda_j; Q_j$, $\lambda = \lambda_k$ for some $k \in I$ and $G'_h \upharpoonright r = G_h \upharpoonright r$
1482 for all $r \notin \{p,q\}$ and all $h \in H$. By definition of projection $G \upharpoonright p = G_h \upharpoonright p$ and
1483 $G \upharpoonright q = G_h \upharpoonright q$ for all $h \in H$. For $r \notin \{p,q,s,t\}$ we get $G' \upharpoonright r = G'_h \upharpoonright r = G_h \upharpoonright r = G \upharpoonright r$.

1484 Moreover $G' \upharpoonright s = \bigoplus_{h \in H} t!\lambda'_h; G'_h \upharpoonright s = \bigoplus_{h \in H} t!\lambda'_h; G_h \upharpoonright s = G \upharpoonright s$ and $G' \upharpoonright t = \sum_{h \in H} t?\lambda'_h; G'_h \upharpoonright t = \sum_{h \in H} s?\lambda'_h; G_h \upharpoonright s = G \upharpoonright t$.

1489 **Lemma 6.9** If $G$ is a well-formed global type and $G \xrightarrow{pq\lambda} G'$, then $G'$ is a well-formed global type.

1490 **Proof** If $G \xrightarrow{pq\lambda} G'$, by Lemma B.1(1) and (2) $G' \upharpoonright r$ is defined for all $r$. The proof
1491 that depth($G''$, $r$) is finite for all $r$ and $G''$ subtree of $G'$ is easy by induction on the
1492 transition rules of Figure 4.

1493 The proofs of Subject Reduction and Session Fidelity rely on the Inversion and
1494 Canonical Form lemmas whose proofs are immediate.

1495 **Lemma B.2 (Inversion).** If $\Gamma \vdash N : G$, then $P \leq G \upharpoonright p$ for all $p[[P]] \in N$.

1496 **Lemma B.3 (Canonical Form).** If $\Gamma \vdash N : G$ and $p \in \text{part}(G)$, then $p[[P]] \in N$ and
1497 $P \leq G \upharpoonright p$.

1500 **Theorem 6.10 (Subject Reduction)** If $\Gamma \vdash N : G$ and $N \xrightarrow{\alpha} N'$, then $G \xrightarrow{\alpha} G'$ and $\Gamma \vdash N' : G'$.

1501 **Proof** Let $\alpha = pq\lambda$. By Rule [Com] of Figure 1, $N \equiv p[[P]] \parallel q[[Q]] \parallel N''$ where
1502 $P = \bigoplus_{i \in I} q!\lambda_i; P_i$ and $Q = \sum_{j \in J} p?\lambda_j; Q_j$ and $N' \equiv p[[P_h]] \parallel q[[Q_h]] \parallel N''$ and $\lambda = \lambda_h$
1503 for some $h \in I \cap J$. From Lemma B.2 we get

1504 1. $G \upharpoonright p = \bigoplus_{i \in I} q!\lambda_i; P'_i$ with $P_i \leq P'_i$ for all $i \in I$, from Rule [≤-Out] of Figure 3,
1505 and
2. $G \upharpoonright q = \sum_{j \in J'} p?\lambda_j; Q'_j$ with $Q_j \le Q'_j$ for all $j \in J' \subseteq J$, from Rule $[ \le -IN ]$ of Figure 3, and

3. $R \le G \upharpoonright r$ for all $r \llbracket R \rrbracket \in N''$.

By Lemma B.1(1) $G \xrightarrow{pq\lambda_h} G_h$ and $G_h \upharpoonright p = P'_h$ and $G_h \upharpoonright q = Q'_h$. By Lemma B.1(2) $G_h \upharpoonright r = G \upharpoonright r$ for all $r \notin \{p, q\}$. We can then choose $G' = G_h$.

**Theorem 6.11 (Session Fidelity)** If $N: G$ and $G \xrightarrow{\alpha} G'$, then $N \xrightarrow{\alpha} N'$ and $N' : G'$.

**Proof** Let $\alpha = pq\lambda$. By Lemma B.1(2) $G \upharpoonright p = \bigoplus_{i \in I} p!\lambda_i; P_i$ and $G \upharpoonright q = \sum_{i \in I} p?\lambda_i; Q_i$ and $\lambda = \lambda_i$ for some $i \in I$ and $G' \upharpoonright r = G \upharpoonright r$ for all $r \notin \{p, q\}$. By Lemma B.1(1) $G' \upharpoonright p = P_i$ and $G' \upharpoonright q = Q_i$. From Lemma B.3 and Lemma B.2 we get $N \equiv p \llbracket P \rrbracket \parallel q \llbracket Q \rrbracket \parallel N''$ and

1. $P = \bigoplus_{i \in I} q!\lambda_i; P'_i$ with $P'_i \le P_i$ for $i \in I$, from Rule $[ \le -OUT ]$ of Figure 3, and

2. $Q = \sum_{j \in J} p?\lambda_j; Q'_j$ with $Q'_j \le Q_j$ for $j \in I \subseteq J$, from Rule $[ \le -IN ]$ of Figure 3, and

3. $R \le G \upharpoonright r$ for all $r \llbracket R \rrbracket \in N''$.

We can then choose $N' = p \llbracket P'_i \rrbracket \parallel q \llbracket Q'_i \rrbracket \parallel N''$.

## C. Proofs of Section 7

**Lemma 7.4** Let $\sigma$ be a pointed trace. If $\sigma \sim \sigma'$, then $\sigma'$ is a pointed trace and $\text{last}(\sigma) = \text{last}(\sigma')$.

**Proof** Let $\sigma \sim \sigma'$. By Definition 7.1 $\sigma'$ is obtained from $\sigma$ by $m$ swaps of adjacent communications. The proof is by induction on such a number $m$. If $m=0$ the result is obvious.

If $m > 0$, then there exists $\sigma_0$ obtained from $\sigma$ by $m-1$ swaps of adjacent communications and there are $\sigma_1, \sigma_2, \alpha$ and $\alpha'$ such that

$$ \sigma_0 = \sigma_1 \cdot \alpha \cdot \alpha' \cdot \sigma_2 \sim \sigma_1 \cdot \alpha' \cdot \alpha \cdot \sigma_2 = \sigma' \quad \text{and} \quad \text{part}(\alpha) \cap \text{part}(\alpha') = \emptyset $$

By induction hypothesis $\sigma_0$ is a pointed trace and $\text{last}(\sigma) = \text{last}(\sigma_0)$. Therefore $\sigma_2 \ne \epsilon$ since otherwise $\alpha'$ would be the last communication of $\sigma_0$ and it cannot be $\text{part}(\alpha) \cap \text{part}(\alpha') = \emptyset$. This implies $\text{last}(\sigma) = \text{last}(\sigma')$.

To show that $\sigma'$ is pointed, since all the communications in $\sigma_1$ and $\sigma_2$ have the same successors in $\sigma_0$ and $\sigma'$, all we have to prove is that the required property holds for the two swapped communications $\alpha'$ and $\alpha$ in $\sigma'$, namely:

$$ \text{part}(\alpha') \cap (\text{part}(\alpha) \cup \text{part}(\sigma_2)) \ne \emptyset $$

$$ \text{part}(\alpha) \cap \text{part}(\sigma_2) \ne \emptyset $$

Since $\text{part}(\alpha) \cap \text{part}(\alpha') = \emptyset$, these two statements are respectively equivalent to:

$$ \text{part}(\alpha') \cap \text{part}(\sigma_2) \ne \emptyset $$

$$ \text{part}(\alpha) \cap (\text{part}(\alpha') \cup \text{part}(\sigma_2)) \ne \emptyset $$

The last two statements are known to hold since $\sigma_0$ is pointed by induction hypothesis.
1525 D. Proofs of Subsection 8.1

This section contains the proofs of Lemmas 8.2, 8.4, 8.5 and 8.6.
1526

Lemma 8.2 (Properties of retrieval and residual for n-events). 1527

1. If $\alpha \diamond v$ is defined, then $\alpha \diamond (\alpha \diamond v) = v$; 1528

2. $\alpha \diamond (\alpha \diamond v) = v$; 1529

3. If $v < v'$, then $\alpha \diamond v < \alpha \diamond v'$; 1530

4. If $v < v'$ and both $\alpha \diamond v$ and $\alpha \diamond v'$ are defined, then $\alpha \diamond v < \alpha \diamond v'$; 1531

5. If $v \# v'$, then $\alpha \diamond v \# \alpha \diamond v'$; 1532

6. If $v \# v'$ and both $\alpha \diamond v$ and $\alpha \diamond v'$ are defined, then $\alpha \diamond v \# \alpha \diamond v'$; 1533

7. If $\alpha \diamond v \# \alpha \diamond v'$, then $v \# v'$. 1534

Proof For (1) and (2) it is enough to show the corresponding properties for located events. 1535

(1) Since $\alpha \diamond (p :: \eta)$ is defined, we have $\eta = (\alpha@p) \cdot \eta'$ and $\alpha \diamond (p :: \eta) = p :: \eta'$ for some $\eta'$. Then $\alpha \diamond (\alpha \diamond (p :: \eta)) = \alpha \diamond (p :: \eta') = p :: (\alpha@p) \cdot \eta' = p :: \eta$. 1536

(2) Since $\alpha \diamond (p :: \eta) = p :: (\alpha@p) \cdot \eta$ is always defined, we immediately get $\alpha \diamond (\alpha \diamond (p :: \eta)) = \alpha \diamond (p :: (\alpha@p) \cdot \eta) = p :: \eta$. 1537
1538

(3) Let $v < v'$. By Definition 5.7(1), there are $p :: \eta \in v$ and $p :: \eta' \in v'$ such that $\eta < \eta'$. Then $\alpha \diamond (p :: \eta) = p :: (\alpha@p) \cdot \eta \in \alpha \diamond v$ and $\alpha \diamond (p :: \eta') = p :: (\alpha@p) \cdot \eta' \in \alpha \diamond v'$. Since $\eta < \eta'$ implies $(\alpha@p) \cdot \eta < (\alpha@p) \cdot \eta'$, we conclude that $\alpha \diamond v < \alpha \diamond v'$. 1539
1540
1541
1542
1543

(4) As in the previous case, there are $p :: \eta \in v$ and $p :: \eta' \in v'$ such that $\eta < \eta'$. Since both $\alpha \diamond v$ and $\alpha \diamond v'$ are defined, there exist $\eta_0$ and $\eta'_0$ such that $\eta = (\alpha@p) \cdot \eta_0$ and $\eta' = (\alpha@p) \cdot \eta'_0$ and $\alpha \diamond (p :: \eta) = p :: \eta_0$ and $\alpha \diamond (p :: \eta') = p :: \eta'_0$. Since $\eta < \eta'$ implies $\eta_0 < \eta'_0$, we conclude that $\alpha \diamond v < \alpha \diamond v'$. 1544
1545
1546
1547

(5) Let $v \# v'$. If Clause (2a) of Definition 5.7 applies, then there are $p :: \eta \in v$ and $p :: \eta' \in v'$ such that $\eta \# \eta'$. From $\alpha \diamond (p :: \eta) = p :: (\alpha@p) \cdot \eta$ and $\alpha \diamond (p :: \eta') = p :: (\alpha@p) \cdot \eta'$ we get $(\alpha@p) \cdot \eta \# (\alpha@p) \cdot \eta'$. If Clause (2b) of Definition 5.7 applies, then there are $p :: \eta \in v$ and $q :: \eta' \in v'$ with $p \neq q$ such that $|\eta \upharpoonright q| = |\eta' \upharpoonright p|$ and $-(\eta \upharpoonright q \succcurlyeq \eta' \upharpoonright p)$. Let $\eta_0 = (\alpha@p) \cdot \eta$ and $\eta'_0 = (\alpha@q) \cdot \eta'$. If part($\alpha$) $\neq$ {p, q}, then $(\alpha@p) \upharpoonright q = \epsilon = (\alpha@q) \upharpoonright p$ and thus $\eta_0 \upharpoonright q = \eta \upharpoonright q$ and $\eta'_0 \upharpoonright p = \eta' \upharpoonright p$. If part($\alpha$) = {p, q}, say $\alpha = pq\lambda$, then $\eta_0 = q!\lambda \cdot \eta$ and $\eta'_0 = p?\lambda \cdot \eta'$, which implies $|\eta_0 \upharpoonright q| = |\eta \upharpoonright q| + 1 = |\eta' \upharpoonright p| + 1 = |\eta'_0 \upharpoonright p|$ and $-(\eta_0 \upharpoonright q \succcurlyeq \eta'_0 \upharpoonright p)$. In both cases we conclude that $\alpha \diamond v \# \alpha \diamond v'$. 1548
1549
1550
1551
1552
1553
1554
1555
1556

(6) The proof is similar to that of Point (5), considering that $\alpha \diamond v$ and $\alpha \diamond v'$ are defined. 1557

(7) Let $\alpha \diamond v \# \alpha \diamond v'$. If Clause (2a) of Definition 5.7 applies, then there are $p :: \eta \in v$ and $p :: \eta' \in v'$ such that $(\alpha@p) \cdot \eta \# (\alpha@p) \cdot \eta'$. Therefore $\eta \# \eta'$ and thus $v \# v'$. If Clause (2b) of Definition 5.7 applies, then there are $p :: \eta_0 = \alpha \diamond (p :: \eta) \in \alpha \diamond v$ and $q :: \eta'_0 = \alpha \diamond (q :: \eta') \in \alpha \diamond v'$ with $p \neq q$ such that $|\eta_0 \upharpoonright q| = |\eta'_0 \upharpoonright p|$ and $-(\eta_0 \upharpoonright q \succcurlyeq \eta'_0 \upharpoonright p)$. It follows that $\eta_0 = (\alpha@p) \cdot \eta$ and $\eta'_0 = (\alpha@q) \cdot \eta'$ and $p :: \eta \in v$ 1558
1559
1560
1561
1562
1563
1564 and $q :: \eta' \in v'$. If $\text{part}(\alpha) \neq \{p, q\}$, then $(\alpha@p) \uparrow q = \epsilon = (\alpha@q) \uparrow p$ and thus
1565 $\eta \uparrow q = \eta_0 \uparrow q$ and $\eta' \uparrow p = \eta'_0 \uparrow p$. If $\text{part}(\alpha) = \{p, q\}$, say $\alpha = pq\lambda$, then $\eta_0 = q!\lambda \cdot \eta$
1566 and $\eta'_0 = p?\lambda \cdot \eta'$, and thus $|\eta \uparrow q| = |\eta_0 \uparrow q| - 1 = |\eta'_0 \uparrow p| - 1 = |\eta' \uparrow p|$ and
1567 $\neg(\eta \uparrow q \bowtie \eta' \uparrow p)$. In both cases we conclude that $v \# v'$.

1568 **Lemma 8.4 (Properties of nec(·))**

1569 1. Let nec($\sigma$) = $v_1$; ... ; $v_n$. Then

1570 (a) $\text{cm}(v_i) = \sigma[i]$ for all $i, 1 \le i \le n;$

1571 (b) If $1 \le h, k \le n$, then $\neg(v_h \# v_k)$.

1572 2. $\neg(\text{nec}(\alpha) \# \alpha \diamond v)$ for all $v$.

1573 3. Let $\sigma = \alpha \cdot \sigma'$ and $\sigma' \neq \epsilon$. If nec($\sigma$) = $v_1$; ... ; $v_n$ and nec($\sigma'$) = $v'_2$; ... ; $v'_n$, then
1574 $\alpha \diamond v'_i = v_i$ and $\alpha \diamond v_i = v'_i$ for all $i, 2 \le i \le n$.

1575 **Proof** (1a) Immediate from Definition 8.3, since $\text{cm}(\sigma \diamond v) = \text{cm}(v)$ for any event $v$.

1576 (1b) We show that neither Clause (2a) nor Clause (2b) of Definition 5.7 can be
1577 used to derive $v_h \# v_k$. Notice that $v_i = \{p_i :: \sigma[1...i]@p_i, q_i :: \sigma[1...i]@q_i\}$. So if
1578 $p :: \eta \in v_h$ and $p :: \eta' \in v_k$ with $h < k$, then either $\eta < \eta'$ or $\eta = \eta'$. Therefore Clause
1579 (2a) does not apply. If $p :: \eta \in v_h$ and $q :: \eta' \in v_k$ and $p \neq q$ and $|\eta \uparrow q| = |\eta' \uparrow p|$, then
1580 it must be $\eta \uparrow q = (\sigma[1...h]@p) \uparrow q \bowtie (\sigma[1...k]@q) \uparrow p = \eta' \uparrow p$. Therefore Clause
1581 (2b) cannot be used.

1582 (2) We show that neither Clause (2a) nor Clause (2b) of Definition 5.7 can be used
1583 to derive nec($\alpha$) # $\alpha \diamond v$. Let part($\alpha$) = $\{p, q\}$. Then nec($\alpha$) = $\{p :: \alpha@p, q :: \alpha@q\}$.
1584 Note that $p :: \eta \in \alpha \diamond v$ iff $\eta = (\alpha@p) \cdot \eta'$ and $p :: \eta' \in v$. Since $\alpha@p < (\alpha@p) \cdot \eta'$,
1585 Clause (2a) of Definition 5.7 cannot be used. Now suppose $r :: \eta \in \alpha \diamond v$ for some
1586 $r \notin \{p, q\}$. In this case $(\alpha@p) \uparrow r = (\alpha@q) \uparrow r = \epsilon$. Therefore, since $\epsilon \bowtie \epsilon$, Clause (2b)
1587 of Definition 5.7 does not apply.

1588 (3) Notice that $\sigma[i] = \sigma'[i-1]$ for all $i, 2 \le i \le n$. Then, by Definition 8.3
1589 $v_i = \sigma[1 \dots i-1] \diamond \text{nec}(\sigma[i]) = \alpha \diamond (\sigma[2 \dots i-1] \diamond \text{nec}(\sigma[i])) =$
1590 $\alpha \diamond (\sigma'[1 \dots i-2] \diamond \text{nec}(\sigma'[i-1])) = \alpha \diamond v'_i$

1590 for all $i, 2 \le i \le n$.

1591 By Lemma 8.2(2) $\alpha \diamond v'_i = v_i$ implies $\alpha \diamond v_i = v'_i$ for all $i, 2 \le i \le n$.

1590 **Lemma 8.5** If $N \xrightarrow{\alpha} N'$ and $v \in \mathcal{N}\mathcal{E}(N)$, then $v = \text{nec}(\alpha)$ or $v \# \text{nec}(\alpha)$ or $\alpha \diamond v$ is defined.

1591 **Proof** Let nec($\alpha$) = $\{p :: \alpha@p, q :: \alpha@q\}$ and $v = \{r :: \eta, s :: \eta'\}$. By Definition 8.1(3)
1592 $\alpha \diamond v$ is defined iff $\eta = (\alpha@r) \cdot \eta_0$ and $\eta' = (\alpha@s) \cdot \eta'_0$ for some $\eta_0, \eta'_0$.

1593 There are 2 possibilities:

1594 • $\{r, s\} \cap \{p, q\} = \emptyset$. Then $\alpha@r = \alpha@s = \epsilon$ and $\alpha \diamond v = v$;

1595 • $\{r, s\} \cap \{p, q\} \neq \emptyset$. Suppose $r = p$. There are three possible subcases:

1596 1. $\eta = \pi \cdot \zeta$ with $\pi \neq \alpha@p$. Then $r :: \eta \# p :: \alpha@p$ and thus $v \# \text{nec}(\alpha)$;
1597

1598

2. $\eta = \alpha@p$. Then either $\eta' = \alpha@q$ and $v = nec(\alpha)$, or $\eta' \neq \alpha@q$ and $v \# nec(\alpha)$ by Lemma 5.21;

1599

1600

1601

1602

3. $\eta = (\alpha@p) \cdot \eta_0$. Then $\alpha \diamond p :: \eta = p :: \eta_0$. Now, if $s \neq q$ we have $\alpha \diamond s :: \eta' = s :: \eta'$, and thus $\alpha \diamond v = \{p :: \eta_0, s :: \eta'\}$. Otherwise, $v = \{p :: (\alpha@p) \cdot \eta_0, q :: \eta'\}$. By Definition 5.5 $p :: (\alpha@p) \cdot \eta_0 \bowtie q :: \eta'$, which implies $\eta' = (\alpha@q) \cdot \eta'_0$ for some $\eta'_0$.

1603

**Lemma 8.6** Let $N \xrightarrow{\alpha} N'$. Then

1604

1. $\{\mathrm{nec}(\alpha)\} \cup \{\alpha \diamond v \mid v \in \mathcal{NE}(N')\} \subseteq \mathcal{NE}(N)$;

1605

2. $\{\alpha \diamond v \mid v \in \mathcal{NE}(N) \text{ and } \alpha \diamond v \text{ defined}\} \subseteq \mathcal{NE}(N')$.

**Proof** Let $\alpha = pq\lambda$. From $N \xrightarrow{\alpha} N'$ we get

$$N = p[\bigoplus_{i \in I} q!\lambda_i; P] \parallel q[\Sigma_{j \in J} p?\lambda_j; Q_j] \parallel N_0$$

where for some $k \in (I \cap J)$ we have $\lambda_k = \lambda$ and

$$N' = p[\mathbf{P}_k] \parallel q[\mathbf{Q}_k] \parallel N_0$$

1606

1607

1608

1609

(1) Let $RT = \{\mathrm{nec}(\alpha)\} \cup \{\alpha \diamond v \mid v \in \mathcal{NE}(N')\}$. We first show that $RT \subseteq \mathcal{CE}(N)$.

By Definition 5.13(1) nec($\alpha$) $\in \mathcal{CE}(N)$. Let $v = \{r :: \eta, s :: \eta'\} \in \mathcal{NE}(N')$. We want to prove that $\alpha \diamond v \in \mathcal{CE}(N)$. By Definition 5.13(1) there are $R, S$ such that $r[\mathbf{R}] \in N'$ and $s[\mathbf{S}] \in N'$ and $\eta \in \mathcal{PE}(R)$ and $\eta' \in \mathcal{PE}(S)$. There are two possible cases:

1610

* $\{r, s\} \cap \{p, q\} = \emptyset$. Then $r[\mathbf{R}] \in N$ and $s[\mathbf{S}] \in N$ and thus $\alpha \diamond v = v \in \mathcal{CE}(N)$;

1611

1612

* $\{r, s\} \cap \{p, q\} \neq \emptyset$. Suppose $r = p$. Then $\eta \in \mathcal{PE}(P_k)$ and $p :: q!\lambda_k \cdot \eta \in \alpha \diamond v$ and $q!\lambda_k \cdot \eta \in \mathcal{PE}(\bigoplus_{i \in I} q!\lambda_i; P_i)$. There are two subcases:

1613

1614

- $s = q$. Then $\eta' \in \mathcal{PE}(Q_k)$ and $q :: p?\lambda_k \cdot \eta' \in \alpha \diamond v$ and $q!\lambda_k \cdot \eta' \in \mathcal{PE}(\Sigma_{j \in J} p?\lambda_j; Q_j)$. We have $\alpha \diamond v = \{p :: q!\lambda_k \cdot \eta, q :: p?\lambda_k \cdot \eta'\} \in \mathcal{CE}(N)$;

1615

1616

- $s \neq q$. Then $\alpha \diamond s :: \eta' = s :: \eta'$, and thus $\alpha \diamond v = \{p :: q!\lambda_k \cdot \eta, s :: \eta'\} \in \mathcal{CE}(N)$.

1617

Therefore in all cases $RT \subseteq \mathcal{CE}(N)$. We want now to show that $RT \subseteq \mathcal{NE}(N)$. Recall from Section 5 that $\mathcal{NE}(N)$ is the greatest fixed point of the function

$$f_{\mathcal{CE}(N)}(X) = \{v_0 \in \mathcal{CE}(N) \mid \exists E_0 \subseteq X. E_0 \text{ is a causal set of } v_0 \text{ in } X\}$$

1618

1619

1620

Then $\mathcal{NE}(N)$ is also the greatest post-fixed point of $f_{\mathcal{CE}(N)}(X)$, namely the greatest $X$ such that $X \subseteq f_{\mathcal{CE}(N)}(X)$. Therefore, to show that $RT \subseteq \mathcal{NE}(N)$, it is enough to show that $RT$ is also a post-fixed point of $f_{\mathcal{CE}(N)}(X)$, namely that $RT \subseteq f_{\mathcal{CE}(N)}(RT)$.

Consider first the event nec($\alpha$). Since the only causal set of nec($\alpha$) in any set is $\emptyset$, it is immediate that nec($\alpha$) $\in f_{\mathcal{CE}(N)}(RT)$. Consider now $\alpha \diamond v \in RT$ for some $v \in \mathcal{NE}(N')$ with loc($v$) = $\{r, s\}$. Define

$$\mathrm{pre}(\alpha, E, v) = \begin{cases} \Xi & \text{if } \{r, s\} \cap \{p, q\} = \emptyset \\ \{\mathrm{nec}(\alpha)\} \cup \Xi & \text{otherwise} \end{cases}$$
1621 where $\Xi = \{\alpha \diamond v' | v' \in E \text{ and } E \text{ is a causal set of } v \text{ in } \mathcal{NE}(N')\}$.

1622 We show that $\text{pre}(\alpha, E, v)$ is a causal set of $\alpha \diamond v$ in $RT$, namely that it is a minimal
1623 subset of $RT$ satisfying Conditions (1) and (2) of Definition 5.9.

1624 Condition (1) If nec($\alpha$) ∈ pre($\alpha$, E, v), then {r, s} ∩ {p, q} ≠ ∅. A conflict between nec($\alpha$) and any other event of pre($\alpha$, E, v) ∪ {α ♦ v} can only be derived by Clause (2a) of Definition 5.7, since nec($\alpha$) = {p :: q!λ, q :: p?λ} and (α@p) ↑ t = (α@q) ↑ t = ε for all t ∉ {p, q}. Suppose r = p. Then p :: q!λ · η ∈ α ♦ v. Since q!λ < q!λ · η, Clause (2a) cannot be used to derive a conflict nec($\alpha$) #α ♦ v. Similarly, if α ♦ v₁ ∈ pre($\alpha$, E, v) and p :: η₁ ∈ v₁, then p :: q!λ · η₁ ∈ α ♦ v₁. Then q!λ < q!λ · η₁, hence Clause (2a) cannot be used to derive nec($\alpha$) #α ♦ v₁.

1631 Suppose now $\alpha \diamond v_1 \in \text{pre}(\alpha, E, v)$ and $\alpha \diamond v_2 \in \text{pre}(\alpha, E, v)$. Since $E$ is a causal set, we
1632 have $\neg(v_1 \# v_2)$. Thus $\neg(\alpha \diamond v_1 \# \alpha \diamond v_2)$ by Lemma 8.2(7).

1633 Condition (2) Let $v = \{r :: \eta, s :: \eta'\}$, we have $\alpha \diamond v = \{r :: (\alpha@r) \cdot \eta, s :: (\alpha@s) \cdot \eta'\}$.
1634 We show that if $\eta_0 < (\alpha@r) \cdot \eta$, then $r :: \eta_0 \in v_0$ for some $v_0 \in \text{pre}(\alpha, E, v)$. From
1635 $\eta_0 < (\alpha@r) \cdot \eta$ we derive $\eta_0 = (\alpha@r) \cdot \zeta$ for some $\zeta$ such that $\zeta < \eta$. If $\zeta \neq \epsilon$,
1636 then $\zeta = \eta'_0 < \eta$. Since $E$ is a causal set, $\eta'_0 < \eta_0$ implies $r :: \eta'_0 \notin E$. Hence
1637 $r :: \eta_0 \notin \text{pre}(\alpha, E, v)$. If instead $\zeta = \epsilon$, then it must be $\eta_0 = \alpha@r \neq \epsilon$ and thus $r \in \{p, q\}$.
1638 In this case $\{\text{nec}(\alpha)\} \in \text{pre}(\alpha, E, v)$ and thus $r :: \eta_0 \notin \text{pre}(\alpha, E, v)$.

1639 As for minimality , we first show that $v' < \alpha \diamond v$ for all $v' \in \text{pre}(\alpha, E, v)$. If nec($\alpha$) $\in$
1640 pre($\alpha, E, v$), then $\{r, s\} \cap \{p, q\} \neq \emptyset$. Then nec($\alpha$) $< \alpha \diamond v$. If $v_1 \in$ pre($\alpha, E, v$) and
1641 $v_1 \neq$ nec($\alpha$), then there exists $v'_1 \in E$ such that $v_1 = \alpha \diamond v'_1$. Since $E$ is a causal set for
1642 $v$, we have $v'_1 < v$. Therefore $v_1 = \alpha \diamond v'_1 < \alpha \diamond v$ by Lemma 8.2(3). Assume now that
1643 pre($\alpha, E, v$) is not minimal. Then there is $E' \subset$ pre($\alpha, E, v$) that verifies Condition (2)
1644 of Definition 5.9 for $\alpha \diamond v$. Let $v' \in$ pre($\alpha, E, v$) $\setminus E'$. Then $v' < \alpha \diamond v = \{r :: \eta_r, s :: \eta_s\}$.
1645 Assume that $r :: \eta'_r \in v'$ with $\eta'_r < \eta_r$ (the proof is similar for $s$). By Condition (2),
1646 there is $v'' \in E'$ such that $r :: \eta'_r \in v''$. But then $v' \# v''$ by Lemma 5.21, contradicting
1647 the fact that pre($\alpha, E, v$) verifies Condition (1). Therefore pre($\alpha, E, v$) is minimal.

(2) Let $\mathcal{R}S = \{\alpha \diamond v \mid v \in \mathcal{N}\mathcal{E}(N) \text{ and } \alpha \diamond v \text{ defined}\}$. We first show that $\mathcal{R}S \subseteq \mathcal{C}\mathcal{E}(N')$. Let $v = \{r :: \eta, s :: \eta'\} \in \mathcal{N}\mathcal{E}(N)$ be such that $\alpha \diamond v$ is defined. We want to prove that $\alpha \diamond v \in \mathcal{C}\mathcal{E}(N')$. By Definition 5.13(1) there are $R, S$ such that $r[[R]] \in N$ and $s[[S]] \in N$ and $\eta \in \mathcal{P}\mathcal{E}(R)$ and $\eta' \in \mathcal{P}\mathcal{E}(S)$. There are two possible cases:

1652 • $\{r, s\} \cap \{p, q\} = \emptyset$. Then $r[[R]] \in N'$ and $s[[S]] \in N'$ and thus $\alpha \diamond v = v \in \mathcal{C}\mathcal{E}(N')$;

1653 • $\{r, s\} \cap \{p, q\} \neq \emptyset$. Suppose $r = p$. Then $\eta \in \mathcal{P}\mathcal{E}(\bigoplus_{i \in I} q!\lambda_i; P_i)$ and since $\alpha \diamond v$ is
1654 defined we have that $\eta = q!\lambda_k \cdot \eta_k$ where $\eta_k \in \mathcal{P}\mathcal{E}(P_k)$. There are two subcases:

1655 - $s = q$. Then $\eta' \in \mathcal{P}\mathcal{E}(\sum_{j \in J} p?\lambda_j; Q_j)$ and since $\alpha \diamond v$ is defined $\eta' = p?\lambda_k \cdot \eta'_k$
1656 where $\eta'_k \in \mathcal{P}\mathcal{E}(Q_k)$. In this case we have $\alpha \diamond v = \{p :: \eta_k, q :: \eta'_k\} \in \mathcal{C}\mathcal{E}(N')$;

1657 - $s \neq q$. Then $\alpha \diamond s :: \eta' = s :: \eta'$, and thus $\alpha \diamond v = \{p :: \eta_k, s :: \eta'\} \in \mathcal{C}\mathcal{E}(N')$.

1658 Therefore in all cases $RS \subseteq \mathcal{C}\mathcal{E}(N')$. We want now to show that $RS \subseteq \mathcal{N}\mathcal{E}(N')$.

We proceed as in the proof of Statement (1). We know that $\mathcal{N}\mathcal{E}(N')$ is the greatest
post-fixed point of the function

$$
f_{\mathcal{C}\mathcal{E}(N')}(X) = \{v_0 \in \mathcal{C}\mathcal{E}(N') \mid \exists E_0 \subseteq X. E_0 \text{ is a causal set of } v_0 \text{ in } X\}
$$

1659 Then, in order to obtain $RS \subseteq \mathcal{N}\mathcal{E}(N')$ it is enough to show that $RS$ is a post-fixed
1660 point of $f_{\mathcal{C}\mathcal{E}(N')}(X)$, namely that $RS \subseteq f_{\mathcal{C}\mathcal{E}(N')}(RS)$.
Let $\alpha \diamond v \in \mathcal{RS}$ for some $v \in \mathcal{NE}(\mathcal{N})$. Define

$$ \mathrm{post}(\alpha, E, v) = \{\alpha \diamond v' \mid v' \in E \text{ and } E \text{ is a causal set of } v \text{ in } \mathcal{NE}(\mathcal{N})\} $$

## E. Proofs of Subsection 8.2

<footnote n="1661">1661 We show that $\mathrm{post}(\alpha, E, v)$ is a causal set of $\alpha \diamond v$ in $\mathcal{RS}$, namely that it is a minimal subset of $\mathcal{RS}$ satisfying Conditions (1) and (2) of Definition 5.9.</footnote>

<footnote n="1662">1662 Condition (1) Suppose $\alpha \diamond v_1 \in \mathrm{post}(\alpha, E, v)$ and $\alpha \diamond v_2 \in \mathrm{post}(\alpha, E, v)$. Since $E$ is a causal set and $v_1, v_2 \in E$, we have $\neg(v_1 \# v_2)$. Thus $\neg(\alpha \diamond v_1 \# \alpha \diamond v_2)$ by Lemma 8.2(5) and (1).</footnote>

<footnote n="1663">1663 Condition (2) Since $v = \{r :: \eta, s :: \eta'\}$ and $\alpha \diamond v$ is defined, we have $\eta = (\alpha@r) \cdot \eta_r$ and $\eta' = (\alpha@s) \cdot \eta_s$ and $\alpha \diamond v = \{r :: \eta_r, s :: \eta_s\}$. Let $\eta_0 < \eta_r$. Then $(\alpha@r) \cdot \eta_0 < (\alpha@r) \cdot \eta_r = \eta$. Since $E$ is a causal set for $v$ in $\mathcal{NE}(\mathcal{N})$, this implies $r :: (\alpha@r) \cdot \eta_0 \in E$. Hence $r :: \eta_0 \in \mathrm{post}(\alpha, E, v)$.</footnote>

<footnote n="1664">1664 As for minimality, we first show that $v' < \alpha \diamond v$ for all $v' \in \mathrm{post}(\alpha, E, v)$. If $v_1 \in \mathrm{post}(\alpha, E, v)$, then there exists $v'_1 \in E$ such that $v_1 = \alpha \diamond v'_1$. Since $E$ is a causal set for $v$, we have $v'_1 < v$. Therefore $v_1 = \alpha \diamond v'_1 < \alpha \diamond v$ by Lemma 8.2(3). Assume now that $\mathrm{post}(\alpha, E, v)$ is not minimal. Then there is $E' \subset \mathrm{post}(\alpha, E, v)$ that verifies Condition (2) of Definition 5.9 for $\alpha \diamond v$. Let $v' \in \mathrm{post}(\alpha, E, v) \setminus E'$. Then $v' < \alpha \diamond v = \{r :: \eta_r, s :: \eta_s\}$.</footnote>

<footnote n="1665">1665 Assume that $r :: \eta'_r \in v'$ with $\eta'_r < \eta_r$ (the proof is similar for $s$). By Condition (2), there is $v'' \in E'$ such that $r :: \eta'_r \in v''$. But then $v' \# v''$ by Lemma 5.21, contradicting the fact that $\mathrm{post}(\alpha, E, v)$ verifies Condition (1). Therefore $\mathrm{post}(\alpha, E, v)$ is minimal.</footnote>

<footnote n="1679">1679 This section contains the proofs of Lemmas 8.10, 8.11 and 8.12.</footnote>

<footnote n="1680">1680 Lemma 8.10 (Properties of retrieval and residual for g-events).</footnote>

<footnote n="1681">1681 1. If $\alpha \circ \gamma$ is defined, then $\alpha \circ (\alpha \circ \gamma) = \gamma$;</footnote>

<footnote n="1682">1682 2. $\alpha \circ (\alpha \circ \gamma) = \gamma$;</footnote>

<footnote n="1683">1683 3. If $\gamma_1 < \gamma_2$, then $\alpha \circ \gamma_1 < \alpha \circ \gamma_2$;</footnote>

<footnote n="1684">1684 4. If $\gamma_1 < \gamma_2$ and both $\alpha \circ \gamma_1$ and $\alpha \circ \gamma_2$ are defined, then $\alpha \circ \gamma_1 < \alpha \circ \gamma_2$;</footnote>

<footnote n="1685">1685 5. If $\gamma_1 \# \gamma_2$, then $\alpha \circ \gamma_1 \# \alpha \circ \gamma_2$;</footnote>

<footnote n="1686">1686 6. If $\gamma < \alpha \circ \gamma'$, then either $\gamma = [\alpha]_{\sim}$ or $\alpha \circ \gamma < \gamma'$;</footnote>

<footnote n="1687">1687 7. If $\mathrm{part}(\alpha_1) \cap \mathrm{part}(\alpha_2) = \emptyset$, then $\alpha_1 \circ (\alpha_2 \circ \gamma) = \alpha_2 \circ (\alpha_1 \circ \gamma)$;</footnote>

<footnote n="1688">1688 8. If $\mathrm{part}(\alpha_1) \cap \mathrm{part}(\alpha_2) = \emptyset$ and both $\alpha_2 \circ (\alpha_1 \circ \gamma)$, $\alpha_2 \circ \gamma$ are defined, then $\alpha_1 \circ (\alpha_2 \circ \gamma) = \alpha_2 \circ (\alpha_1 \circ \gamma)$.</footnote>

<footnote n="1690">1690 Proof (1) If $\alpha \circ [\sigma]_{\sim}$ is defined, then in case $\mathrm{part}(\alpha) \cap \mathrm{part}(\sigma) = \emptyset$ we get $\alpha \circ [\sigma]_{\sim} = [\sigma]_{\sim}$</footnote>

<footnote n="1691">1691 and also $\alpha \circ [\sigma]_{\sim} = [\sigma]_{\sim}$, so $\alpha \circ (\alpha \circ [\sigma]_{\sim}) = [\sigma]_{\sim}$. Instead if $\mathrm{part}(\alpha) \cap \mathrm{part}(\sigma) \neq \emptyset$,</footnote>

<footnote n="1692">1692 then $\alpha \circ [\sigma]_{\sim} = [\sigma']_{\sim}$ where $\sigma \sim \alpha \cdot \sigma'$ and $\sigma' \neq \epsilon$. From $\mathrm{part}(\alpha) \cap \mathrm{part}(\sigma) \neq \emptyset$ we get</footnote>

<footnote n="1693">1693 $\alpha \circ [\sigma']_{\sim} = [\alpha \cdot \sigma']_{\sim}$ by Definition 7.6. This implies $\alpha \circ (\alpha \circ [\sigma]_{\sim}) = [\sigma]_{\sim}$.</footnote>
(2) By Definition 7.6 either $\alpha \circ [\sigma]_{\sim} = [\alpha \cdot \sigma]_{\sim}$ if $\mathrm{part}(\alpha) \cap \mathrm{part}(\sigma) \neq \emptyset$, or $\alpha \circ \sigma = [\sigma]_{\sim}$. In the first case $\alpha \bullet [\alpha \cdot \sigma]_{\sim} = [\sigma]_{\sim}$ and in the second $\alpha \circ [\sigma]_{\sim} = [\sigma]_{\sim}$, which proves the result.

(3) Let $\gamma_1 = [\sigma]_{\sim}$ and $\gamma_2 = [\sigma \cdot \sigma']_{\sim}$. If $\mathrm{part}(\alpha) \cap \mathrm{part}(\sigma) \neq \emptyset$, then $\mathrm{part}(\alpha) \cap \mathrm{part}(\sigma \cdot \sigma') \neq \emptyset$, and we have $\alpha \circ \gamma_1 = [\alpha \cdot \sigma]_{\sim}$ and $\alpha \circ \gamma_2 = [\alpha \cdot \sigma \cdot \sigma']_{\sim}$. Whence $\alpha \circ \gamma_1 \le \alpha \circ \gamma_2$. Suppose now $\mathrm{part}(\alpha) \cap \mathrm{part}(\sigma) = \emptyset$. Then $\alpha \circ \gamma_1 = [\sigma]_{\sim} = \gamma_1$. If also $\mathrm{part}(\alpha) \cap \mathrm{part}(\sigma') = \emptyset$, then $\alpha \circ \gamma_2 = [\sigma \cdot \sigma]_{\sim} = \gamma_2$ and we are done. If instead $\mathrm{part}(\alpha) \cap \mathrm{part}(\sigma') \neq \emptyset$, then $\alpha \circ \gamma_2 = [\alpha \cdot \sigma \cdot \sigma']_{\sim} = [\sigma \cdot \alpha \cdot \sigma']_{\sim}$, whence $\gamma_1 \le \alpha \circ \gamma_2$.

(4) Let $\gamma_1 = [\sigma]_{\sim}$ and $\gamma_2 = [\sigma \cdot \sigma']_{\sim}$. If $\mathrm{part}(\alpha) \cap \mathrm{part}(\sigma) = \mathrm{part}(\alpha) \cap \mathrm{part}(\sigma \cdot \sigma') = \emptyset$, then $\alpha \bullet \gamma_1 = \gamma_1$ and $\alpha \bullet \gamma_2 = \gamma_2$. If $\mathrm{part}(\alpha) \cap \mathrm{part}(\sigma) \neq \emptyset$, then $\sigma \sim \alpha \cdot \sigma_0$, which implies $\alpha \bullet \gamma_1 = [\sigma_0]_{\sim}$ and $\alpha \bullet \gamma_2 = [\sigma_0 \cdot \sigma']_{\sim}$. If $\mathrm{part}(\alpha) \cap \mathrm{part}(\sigma) = \emptyset$ and $\mathrm{part}(\alpha) \cap \mathrm{part}(\sigma \cdot \sigma') \neq \emptyset$, then $\alpha \cdot \gamma_1 = [\sigma]_{\sim}$ and $\sigma' \sim \alpha \cdot \sigma_0$, which implies $\alpha \cdot \gamma_2 = [\sigma \cdot \sigma_0]_{\sim}$.

(5) Let $\gamma_1 = [\sigma]_{\sim}$ and $\gamma_2 = [\sigma']_{\sim}$ and $\sigma \in \mathfrak{p} \# \sigma' \in \mathfrak{p}$ for some $\mathfrak{p}$. The only interesting case is $\mathrm{part}(\alpha) \cap \mathrm{part}(\sigma) = \emptyset$ and $\mathrm{part}(\alpha) \cap \mathrm{part}(\sigma') \neq \emptyset$. This implies $\alpha \circ \gamma_1 = [\sigma]_{\sim}$ and $\alpha \circ \gamma_2 = [\alpha \cdot \sigma']_{\sim}$. We get $(\alpha \cdot \sigma') \in \mathfrak{p} = \sigma' \in \mathfrak{p}$ since $\mathrm{part}(\alpha) \cap \mathrm{part}(\sigma) = \emptyset$ implies $\mathfrak{p} \notin \mathrm{part}(\alpha)$. We conclude $\alpha \circ \gamma_1 \# \alpha \circ \gamma_2$.

(6) The case $\gamma = [\alpha]_{\sim}$ is immediate. If $\alpha \bullet \gamma$ is defined, we get $\alpha \cdot \gamma < \alpha \bullet (\alpha \circ \gamma')$ by Point 4 and $\alpha \circ (\alpha \circ \gamma') = \gamma'$ by Point 2. Otherwise let $\gamma = [\sigma]_{\sim}$ and $\alpha \circ \gamma' = [\sigma \cdot \sigma']_{\sim}$. From $\alpha \bullet \gamma$ undefined we get $\mathrm{part}(\alpha) \cap \mathrm{part}(\sigma) \neq \emptyset$ and $\sigma \neq \alpha \cdot \sigma_0$. Since $\mathrm{part}(\alpha) \cap \mathrm{part}(\sigma) \neq \emptyset$ implies $\mathrm{part}(\alpha) \cap \mathrm{part}(\sigma \cdot \sigma') \neq \emptyset$ we get $\sigma \cdot \sigma' \sim \alpha \cdot \sigma_1$ for some $\sigma_1$ by Definition 7.6(1). Then this case is impossible.

(7) Let $\gamma = [\sigma]_{\sim}$. By Definition 7.6(1) we have four cases:

(a) $\alpha_1 \circ (\alpha_2 \circ \sigma) = [\alpha_1 \cdot (\alpha_2 \cdot \sigma)]_{\sim} = [\alpha_2 \cdot (\alpha_1 \cdot \sigma)]_{\sim} = \alpha_2 \circ (\alpha_1 \circ \sigma)$ if $\mathrm{part}(\alpha_1) \cap \mathrm{part}(\sigma) \neq \emptyset$ and $\mathrm{part}(\alpha_2) \cap \mathrm{part}(\sigma) \neq \emptyset$, since $\mathrm{part}(\alpha_1) \cap \mathrm{part}(\alpha_2) = \emptyset$;

(b) $\alpha_1 \circ (\alpha_2 \circ \sigma) = [\alpha_1 \cdot \sigma]_{\sim} = \alpha_2 \circ (\alpha_1 \circ \sigma)$ if $\mathrm{part}(\alpha_1) \cap \mathrm{part}(\sigma) \neq \emptyset$ and $\mathrm{part}(\alpha_2) \cap \mathrm{part}(\sigma) = \emptyset$;

(c) $\alpha_1 \circ (\alpha_2 \circ \sigma) = [\alpha_2 \cdot \sigma]_{\sim} = \alpha_2 \circ (\alpha_1 \circ \sigma)$ if $\mathrm{part}(\alpha_1) \cap \mathrm{part}(\sigma) = \emptyset$ and $\mathrm{part}(\alpha_2) \cap \mathrm{part}(\sigma) \neq \emptyset$;

(d) $\alpha_1 \circ (\alpha_2 \circ \sigma) = [\sigma]_{\sim} = \alpha_2 \circ (\alpha_1 \circ \sigma)$ if $\mathrm{part}(\alpha_1) \cap \mathrm{part}(\sigma) = \emptyset$ and $\mathrm{part}(\alpha_2) \cap \mathrm{part}(\sigma) = \emptyset$.

(8) Let $\gamma = [\sigma]_{\sim}$. By Definitions 7.6(1) and 8.9(1) we have four cases:

(a) $\alpha_1 \circ (\alpha_2 \cdot \sigma) = [\alpha_1 \cdot \sigma']_{\sim} = \alpha_2 \cdot (\alpha_1 \circ \sigma)$ if $\mathrm{part}(\alpha_1) \cap \mathrm{part}(\sigma) \neq \emptyset$ and $\sigma \sim \alpha_2 \cdot \sigma'$;

(b) $\alpha_1 \circ (\alpha_2 \cdot \sigma) = [\alpha_1 \cdot \sigma]_{\sim} = \alpha_2 \cdot (\alpha_1 \circ \sigma)$ if $\mathrm{part}(\alpha_1) \cap \mathrm{part}(\sigma) \neq \emptyset$ and $\mathrm{part}(\alpha_2) \cap \mathrm{part}(\sigma) = \emptyset$;

(c) $\alpha_1 \circ (\alpha_2 \cdot \sigma) = [\sigma']_{\sim} = \alpha_2 \cdot (\alpha_1 \circ \sigma)$ if $\mathrm{part}(\alpha_1) \cap \mathrm{part}(\sigma) = \emptyset$ and $\sigma \sim \alpha_2 \cdot \sigma'$;

(d) $\alpha_1 \circ (\alpha_2 \cdot \sigma) = [\sigma]_{\sim} = \alpha_2 \circ (\alpha_1 \circ \sigma)$ if $\mathrm{part}(\alpha_1) \cap \mathrm{part}(\sigma) = \emptyset$ and $\mathrm{part}(\alpha_2) \cap \mathrm{part}(\sigma) = \emptyset$.

**Lemma 8.11** *The following hold:*
1733

1. If $\gamma \in \mathcal{G}(G)$, then $pq\lambda \circ \gamma \in \mathcal{G}(p \to q : \coprod_{i \in I} \lambda_i; G_i)$, where $\lambda = \lambda_k$ and $G = G_k$ for some $k \in I$;

1734

1735

2. If $\gamma \in \mathcal{G}(p \to q : \coprod_{i \in I} \lambda_i; G_i)$ and $pq\lambda_k \circ \gamma$ is defined, then $pq\lambda_k \circ \gamma \in \mathcal{G}(G_k)$, where $k \in I$.

1736

1737

**Proof** (1) By Definition 7.11(1) $\gamma \in \mathcal{G}(G)$ implies $\gamma = \text{ev}(\sigma)$ for some $\sigma \in \text{Tr}^+(G)$. Since $pq\lambda \circ \gamma = \text{ev}(pq\lambda \cdot \sigma)$ by Definitions 7.6, 7.7 and $pq\lambda \cdot \sigma \in \text{Tr}^+(p \to q : \coprod_{i \in I} \lambda_i; G_i)$ we conclude $pq\lambda \circ \gamma \in \mathcal{G}(p \to q : \coprod_{i \in I} \lambda_i; G_i)$ by Definition 7.11(1).

1738

1739

1740

(2) By Definition 7.11(1) $\gamma \in \mathcal{G}(p \to q : \coprod_{i \in I} \lambda_i; G_i)$ implies $\gamma = \text{ev}(\sigma)$ for some $\sigma \in \text{Tr}^+(p \to q : \coprod_{i \in I} \lambda_i; G_i)$. We get $\sigma = pq\lambda_h \cdot \sigma'$ with $\sigma' \in \text{Tr}^+(G_h)$ or $\sigma' = \epsilon$ for some $h \in I$. The hypothesis $pq\lambda_k \circ \gamma$ defined implies either $h = k$ and $\sigma' \neq \epsilon$ or $\text{part}(\sigma') \cap \{p, q\} = \emptyset$ and $pq\lambda_k \circ \gamma = \text{ev}(\sigma')$ by Definition 8.9(1). In the first case $\sigma' \in \text{Tr}^+(G_k)$. In the second case $\sigma'' \in \text{Tr}^+(G_k)$ for some $\sigma'' \sim \sigma'$ by definition of projection, which prescribes the same behaviours to all participants different from $p, q$, see Figure 2. We conclude $pq\lambda_k \circ \gamma \in \mathcal{G}(G_k)$ by Definition 7.11(1).

1741

1742

1743

1744

1745

1746

1747

**Lemma 8.12** Let $G \xrightarrow{\alpha} G'$.

1748

1. If $\gamma \in \mathcal{G}(G')$, then $\alpha \circ \gamma \in \mathcal{G}(G)$;

1749

2. If $\gamma \in \mathcal{G}(G)$ and $\alpha \circ \gamma$ is defined, then $\alpha \circ \gamma \in \mathcal{G}(G')$.

1750

**Proof** Both proofs are by induction on the inference of the transition $G \xrightarrow{\alpha} G'$, see Figure 4.

1751

1752

(1) For rule [ECOMM] we get $G = p \to q : \coprod_{i \in I} \lambda_i; G_i$ and $G' = G_k$ and $\alpha = pq\lambda_k$ for some $k \in I$. We conclude $\alpha \circ \gamma \in \mathcal{G}(G)$ by Lemma 8.11(1).

1753

1754

For rule [ICOMM] we get $G = p \to q : \coprod_{i \in I} \lambda_i; G_i$ and $G' = p \to q : \coprod_{i \in I} \lambda_i; G'_i$ and $G_i \xrightarrow{\alpha} G'_i$ for all $i \in I$ and $\text{part}(\alpha) \cap \{p, q\} = \emptyset$. By Definition 7.11(1) $\gamma \in \mathcal{G}(G')$ implies $\gamma = \text{ev}(\sigma)$ for some $\sigma \in \text{Tr}^+(G')$. This implies $\sigma = pq\lambda_k \cdot \sigma'$ and $\gamma = [\sigma_0]$ with either $\sigma_0 \sim pq\lambda_k \cdot \sigma'_0$ for some $k \in I$ or $\text{part}(\sigma_0) \cap \{p, q\} = \emptyset$ by Definition 7.6. Then $pq\lambda_k \circ \gamma$ is defined unless $\sigma_0 = pq\lambda_k$ by Definition 8.9(1). We consider two cases.

1755

1756

1757

1758

1759

If $\sigma_0 = pq\lambda_k$, then $\alpha \circ \gamma = [pq\lambda_k]$ since $\text{part}(\alpha) \cap \{p, q\} = \emptyset$. We conclude $\alpha \circ \gamma \in \mathcal{G}(G)$ by Definition 7.11(1). Otherwise let $\gamma' = pq\lambda_k \circ \gamma$. By Lemma 8.11(2) $\gamma' \in \mathcal{G}(G'_k)$. By induction $\alpha \circ \gamma' \in \mathcal{G}(G_k)$. By Lemma 8.11(1) $pq\lambda_k \circ (\alpha \circ \gamma') \in \mathcal{G}(G)$. We now show that $pq\lambda_k \circ (\alpha \circ \gamma') = \alpha \circ \gamma$. By Lemma 8.10(7) and $\text{part}(\alpha) \cap \{p, q\} = \emptyset$ we get $pq\lambda_k \circ (\alpha \circ \gamma') = \alpha \circ (pq\lambda_k \circ \gamma')$ and by Lemma 8.10(1) we have $pq\lambda_k \circ \gamma' = pq\lambda_k \circ (pq\lambda_k \circ \gamma) = \gamma$. Therefore $pq\lambda_k \circ (\alpha \circ \gamma') = \alpha \circ \gamma \in \mathcal{G}(G)$.

1760

1761

1762

1763

1764

1765

(2) For rule [ECOMM] we get $G = p \to q : \coprod_{i \in I} \lambda_i; G_i$ and $G' = G_k$ and $\alpha = pq\lambda_k$ for some $k \in I$. We conclude $\alpha \circ \gamma \in \mathcal{G}(G')$ by Lemma 8.11(2).

1766

1767

For rule [ICOMM] we get $G = p \to q : \coprod_{i \in I} \lambda_i; G_i$ and $G = p \to q : \coprod_{i \in I} \lambda_i; G'_i$ and $G_i \xrightarrow{\alpha} G'_i$ for all $i \in I$ and $\text{part}(\alpha) \cap \{p, q\} = \emptyset$. By Definition 7.11(1) $\gamma \in \mathcal{G}(G)$ implies $\gamma = \text{ev}(\sigma)$ for some $\sigma \in \text{Tr}^+(G)$. This implies $\sigma = pq\lambda_k \cdot \sigma'$ and $\gamma = [\sigma_0]$ with either $\sigma_0 \sim pq\lambda_k \cdot \sigma'_0$ for some $k \in I$ or $\text{part}(\sigma_0) \cap \{p, q\} = \emptyset$ by Definition 7.6. Then $pq\lambda_k \circ \gamma$ is defined unless $\sigma_0 = pq\lambda_k$ by Definition 8.9(1). We consider two cases.

1768

1769

1770

1771

1772

If $\sigma_0 = pq\lambda_k$, then $\alpha \circ \gamma = [pq\lambda_k]$ since $\text{part}(\alpha) \cap \{p, q\} = \emptyset$. We conclude $\alpha \circ \gamma \in \mathcal{G}(G')$ by Definition 7.11(1). Otherwise let $\gamma' = pq\lambda_k \circ \gamma$. By Lemma 8.11(2) $\gamma' \in \mathcal{G}(G'_k)$.

1773
We first show that $\alpha \cdot \gamma'$ is defined. Since $\alpha \cdot \gamma$ and $pq\lambda_k \cdot \gamma$ are defined, by Definition 8.9(1) we have four cases:

1776 (a) $\sigma_0 \sim \alpha \cdot \sigma_1$ for some $\sigma_1$ and $\sigma_0 \sim pq\lambda_k \cdot \sigma'_0$;

1777 (b) $\sigma_0 \sim \alpha \cdot \sigma_1$ and $\text{part}(\sigma_0) \cap \{p, q\} = \emptyset$;

1778 (c) $\text{part}(\alpha) \cap \text{part}(\sigma_0) = \emptyset$ and $\sigma_0 \sim pq\lambda_k \cdot \sigma'_0$;

1779 (d) $\text{part}(\alpha) \cap \text{part}(\sigma_0) = \emptyset$ and $\text{part}(\sigma_0) \cap \{p, q\} = \emptyset$.

In case (a) $\sigma_0 \sim \alpha \cdot pq\lambda_k \cdot \sigma'_1 \sim pq\lambda_k \cdot \alpha \cdot \sigma'_1$ for some $\sigma'_1$ since $\text{part}(\alpha) \cap \{p, q\} = \emptyset$. Notice that $\sigma'_1 \neq \epsilon$ since $\sigma_0$ is pointed and $\text{part}(\alpha) \cap \{p, q\} = \emptyset$. We get $\gamma' = pq\lambda_k \cdot \gamma = [\alpha \cdot \sigma'_1]_{\sim}$ and $\alpha \cdot \gamma' = [\sigma'_1]_{\sim}$.

In case (b) $\gamma' = \gamma$ and $\alpha \cdot \gamma' = [\sigma_1]_{\sim}$.

In case (c) $\gamma' = [\sigma'_0]_{\sim}$ and $\alpha \cdot \gamma' = [\sigma'_0]_{\sim}$, since $\text{part}(\alpha) \cap \text{part}(\sigma_0) = \emptyset$ implies $\text{part}(\alpha) \cap \text{part}(\sigma'_0) = \emptyset$.

In case (d) $\gamma' = \gamma$ and $\alpha \cdot \gamma' = \gamma$.

By induction $\alpha \cdot \gamma' \in \mathcal{GE}(G'_k)$. By Lemma 8.11(1) $pq\lambda_k \circ (\alpha \cdot \gamma') \in \mathcal{GE}(G')$.

We now show that $pq\lambda_k \circ (\alpha \cdot \gamma') = \alpha \cdot \gamma$. From $\gamma' = pq\lambda_k \cdot \gamma$ and Lemma 8.10(1) $pq\lambda_k \circ \gamma' = \gamma$. Therefore from $\alpha \cdot \gamma$ defined we have $\alpha \cdot (pq\lambda_k \circ \gamma')$ defined. Since $\alpha \cdot \gamma'$ is also defined and $\text{part}(\alpha) \cap \{p, q\} = \emptyset$, by Lemma 8.10(8) we get $pq\lambda_k \circ (\alpha \cdot \gamma') = \alpha \cdot (pq\lambda_k \circ \gamma')$. Therefore $pq\lambda_k \circ (\alpha \cdot \gamma') = \alpha \cdot \gamma \in \mathcal{GE}(G')$.

## 1792 F. Glossary of Symbols and Table of Notations

<table><thead><tr><th>Symbol</th><th>Meaning</th></tr></thead><tbody><tr><td>π</td><td>input/output action: p!λ, p?λ</td></tr><tr><td>α</td><td>communication pqλ</td></tr><tr><td>σ</td><td>trace, finite sequence of communications</td></tr><tr><td>S</td><td>event structure</td></tr><tr><td>χ</td><td>configuration of an event structure</td></tr><tr><td>η</td><td>p-event, non-empty finite sequence of input/output actions</td></tr><tr><td>PE</td><td>set of p-events</td></tr><tr><td>ζ</td><td>(possibly empty) finite sequence of input/output actions</td></tr><tr><td>ϑ</td><td>undirected action: !λ, ?λ</td></tr><tr><td>Θ</td><td>(possibly empty) finite sequence of undirected actions</td></tr><tr><td>ν</td><td>n-event, unordered pair of dual located p-events</td></tr><tr><td>NE</td><td>set of n-events</td></tr><tr><td>γ</td><td>g-event, equivalence class [σ]~ with σ pointed</td></tr><tr><td>GE</td><td>set of g-events</td></tr></tbody></table>