### 4.2.1 Interpretation of PCF

Let us focus first on the purely functional primitives, i.e. on the interpretation of PCF.

**Interpretation of types.** First of all, to every type $A$ we associate an arena: this is done exactly as in Section 3.2.1, by setting $[[B]] = B$, $[[N]] = N$ and $[[U]] = U$ the arenas of 3.8, 3.9 and 3.7 respectively. Arrow types are interpreted as $[[A \to B]] = [[A]] \Rightarrow [[B]]$ using the arrow arena construction of Definition 4.1.3, yielding

$$[[A]] \in \downarrow\uparrow\text{-Strat}$$

an arena for every type $A$ of PCF. This is extended to contexts by

$$[[x_1 : A_1, \dots, x_n : A_n]] = \bigwedge_{1 \le i \le n} [[A_i]].$$

**Interpretation of terms.** The general methodology of the interpretation of terms is that of the interpretation of a simply-typed $\lambda$-calculus in a cartesian closed category. This means that a term$^2 \Gamma \vdash M : A$ gets interpreted as a morphism in $\downarrow\uparrow$-Strat:

$$[[M]] \in \downarrow\uparrow\text{-Strat}([\Gamma], [A]).$$

The primitives for the simply-typed $\lambda$-calculus are covered by the cartesian closed structure of $\downarrow\uparrow$-Strat (see [Lambek and Scott, 1988] for details). For recursion, we set

$$[[\mathcal{Y} M]] = \mathcal{Y}_{[A]} \circ [[M]]$$

for $\Gamma \vdash M : A \to A$, using the strategy $\mathcal{Y}_A$ of (5.2). It remains to provide interpretations for all the additional combinators that PCF adds to the simply-typed $\lambda$-calculus.

First of all, all constants are interpreted by the obvious strategy directly returning the corresponding value. In Figure 4.4, we show the typical plays of strategies for sequential composition, conditionals, successor, and zero test; while Figure 4.6 shows typical plays for the predecessor, and Figure 4.7 shows the typical plays for the let binding strategy. Using these strategies, the strategy is obtained by the clauses in Figure 4.5.

### 4.2.2 Interpretation of State

We complete the interpretation to provide semantics for full IA.

**Interpretation of types.** Before we describe the interpretation of stateful primitives, we must provide arenas for the two additional types $\mathcal{V}$ and $\mathcal{S}$ that IA adds to PCF.

Intuitively, these arenas describe the interface through which a program may interact with a reference or a semaphore. For instance, a reference may be written to; or read from – a semaphore may be grabbed and released. It is convenient to split the arena

<footnote n="2">²Or really, a typing derivation – but type annotations in PCF ensure that each term has a unique derivation.</footnote>
<figure><img src="image_33.png" /><figcaption>Figure 4.4: Typical plays of basic strategies for PCF</figcaption></figure>

<figure><img src="image_34.png" /><figcaption>Figure 4.5: Basic interpretation clauses</figcaption></figure>

<figure><img src="image_35.png" /><figcaption>Figure 4.7: Typical plays for $\text{let}_{X,Y}$</figcaption></figure>
<figure><img src="image_36.png" /><figcaption>Figure 4.8: $V_w$</figcaption></figure>

<caption>Figure 4.9: $V_r$</caption>

<caption>Figure 4.10: S</caption>

for references in two: $V_w$ describes the protocol for writing to the memory, and $V_r$ for reading from the memory. Formally, these and S for semaphores are defined by:

$$V_w = \bigoplus_{n \in N} U, \quad V_r = N, \quad S = U \& U \quad (4.5)$$

with moves renamed as illustrated in Figures 4.8, 4.9 and 4.10; hopefully making the intention behind the moves self-explanatory. Finally, we pair writing and reading with

$$V = V_w \& V_r,$$

and $[[V]] = V$, $[[S]] = S$ completes the interpretation of all IA types.

**Queries.** Next, we must provide strategies for the primitives corresponding to state: manipulation and declaration of variables and semaphores. The usual methodology in game semantics is to separate these primitives in two categories. On the one hand, we have the primitives performing queries to the state: assignment, dereferenciation, grab and release. Those are viewed as not inherently stateful, as they simply propagate the operations made by the program to the central memory. On the other hand, reference and semaphore declaration actually introduce the stateful behaviour.

We start with the former, by providing the interpretation of assignment, dereferenciation, grab and release. This is done via the four following clauses:

$[[M := N]]$ = assign $\odot [[N]], [[M]]$

$[[!M]]$ = deref $\odot [[M]]$

$[[grab(M)]]$ = grab $\odot [[M]]$

$[[release(M)]]$ = release $\odot [[M]]$

using the strategies of Figures 4.11, 4.12, 4.13, and 4.14. For the most part those are simply copycat strategies – or more precisely, following (4.5), projections. In particular we insist that they are *innocent strategies*: they are not responsible for the side effect, as their role is simply to forward queries to the actual memory.

**Declaration of references.** Now, we must provide the interpretation for the declaration of new references, performing the actual side effect.

The *memory cell* implements the stateful behaviour: it acknowledges the write requests; when queried with a read request it outputs the value provided with the latest
<figure><img src="image_37.png" /><figcaption>Figure 4.11: assign</figcaption></figure>

<caption>Figure 4.12: deref</caption>

<caption>Figure 4.13: grab</caption>

<caption>Figure 4.14: release</caption>

write. At first ignoring pointers, it seems natural to first capture this behaviour as a language (as in, a set of words) called cell, on moves of V. Hence we define:

$$ \text{cell}_n := \varepsilon | \text{wk}^- \check{+} \text{cell}_k | \text{r}^- n^+ \text{cell}_n $$

and we define cell as the prefix language of cell₀ (matching the fact that new references are initialized to 0). This definition omits pointers, but they are easily reinstated: Opponent moves are initial, while Player moves point to the previous move.

It is tempting to take cell : V, and for x : V ⊢ M : A a term of IA, to define

$$ [[\text{newref } x \text{ in } M]] = [[M]] \circ \text{cell}, $$

however we run into an issue: cell is not a strategy, since it is not single-threaded. But actually, of course it cannot be single-threaded: single-threadedness ensures that each call is independent, whereas the very nature of cell forces it to link the different queries! To make the definition above single-threaded, we seek to define instead

$$ \text{newr}_X : (V \Rightarrow X) \Rightarrow X, $$

ensuring that all variable queries belong to the same thread. Fixing X for now, we set

$$ \text{newrt}_n := \varepsilon | \text{wk}^- \check{+} \text{newrt}_k | \text{r}^- n^+ \text{newrt}_n | v_1^- v_2^+ \text{newrt}_n $$

and set newrt as the prefix language of q₂⁻q₁⁺newrt₀, where the annotations 1 and 2 help distinguish components, writing (V ⇒ X₁) ⇒ X₂. To cell, newrt adds two initial questions q₂⁻ and q₁⁺ and is prepared at any point to propagate an answer v₁⁻ for q₁⁺ to the corresponding answer v₂⁺ for q₂⁻ – this does not necessarily end the play, and it may happen several times as Opponent may not be well-bracketed. Finally, these plays lack pointers – but they are uniquely determined so as to make the plays P-visible.

This defines newrt, a set of threads; the corresponding single-threaded strategy is:

**Proposition 4.2.1.** Consider X a basic arena, i.e. one of U, B, and N.

Then, there is a unique single-threaded strategy

$$ \text{newr}_X : (V \Rightarrow X) \Rightarrow X $$

such that for all s ∈ newr_X, we have [s] ∈ newrt_X.
$$ \begin{align*} \llbracket \mathit{newref} x := n \text{ in } M \rrbracket &= \mathit{newr}_X \circled{\Gamma}(\llbracket M \rrbracket) \in \llbracket \uparrow\mathit{-Strat}(\llbracket \Gamma \rrbracket, \llbracket A \rrbracket) \rrbracket \\ \llbracket \mathit{newsem} x := n \text{ in } M \rrbracket &= \mathit{news}_X \circled{\Gamma}(\llbracket M \rrbracket) \in \llbracket \uparrow\mathit{-Strat}(\llbracket \Gamma \rrbracket, \llbracket A \rrbracket) \rrbracket. \end{align*} $$

<caption>Figure 4.15: Interpretation of reference and semaphore declaration</caption>

After each Opponent move, there is exactly one active thread: namely, that where Opponent just moved. The single-threaded strategy `newr_X` then simply plays as `newrT_X` in the active thread, ignoring other threads and never switching between them. Operationally, this corresponds to the fact that state in IA is *local*: each execution of the new reference operation is linked to a separate, dynamically allocated memory cell.

Finally, the interpretation of `newref` is given in Figure 4.15 for $\Gamma, x : V \vdash M : X$.

**Declaration of semaphores.** Now, we perform the same construction for semaphores. The definition is analogous and semaphores are not particularly interesting in a sequential language, so we offer fewer details. The semaphore cell is defined first via:

$$ \begin{align*} \mathit{lock}_0 &::= \varepsilon \mid \mathbf{g}^{-\vee} \mathit{+} \mathit{lock}_1 \mid \mathbf{h}^{-} \\ \mathit{lock}_{n+1} &::= \varepsilon \mid \mathbf{h}^{-\vee} \mathit{+} \mathit{lock}_0 \mid \mathbf{g}^{-}, \end{align*} $$

setting `lock` as the prefix language of `lock_0` – pointers are redundant. Observe that in a sequential language, attempting to grab a semaphore that is not free results in divergence; likewise attempting to release a semaphore that is already free yields divergence.

Again, that is not single-threaded. For the actual single-threaded strategy, we set:

$$ \begin{align*} \mathit{newst}_0 &::= \varepsilon \mid \mathbf{g}^{-\vee} \mathit{+} \mathit{newst}_1 \mid \nu_1^{-} \nu_2^{+} \mathit{newst}_0 \mid \mathbf{h}^{-} \\ \mathit{newst}_{n+1} &::= \varepsilon \mid \mathbf{h}^{-\vee} \mathit{+} \mathit{newst}_0 \mid \nu_1^{-} \nu_2^{+} \mathit{newst}_{n+1} \mid \mathbf{g}^{-} \end{align*} $$

and set `newst_X` as the prefix language of `newst_0`, where the subscripts 1 and 2 help distinguish components on ($S \Rightarrow X_1$) $\Rightarrow X_2$. Finally, as for references, we set:

**Proposition 4.2.2.** Consider X a basic arena, i.e. one of U, B, and N.
Then, there is a unique single-threaded strategy

$$ \mathit{news}_X : (V \Rightarrow X) \Rightarrow X $$

such that for all $s \in \mathit{news}_X$, we have $[s] \in \mathit{newst}_X$.

Finally, the interpretation of `newsem` is given in Figure 4.15 for $\Gamma, x : S \vdash M : X$. This almost concludes the interpretation of IA, but two final constructions remain.

**Bad variables and semaphores.** Indeed, recall from Section 2.2.1 that IA includes

$$ \frac{\Gamma \vdash M : \mathbb{N} \to \mathbb{U} \qquad \Gamma \vdash N : \mathbb{N}}{\Gamma \vdash \mathbf{mkvar} MN : \mathbb{V}} \qquad \frac{\Gamma \vdash M : \mathbb{U} \qquad \Gamma \vdash N : \mathbb{U}}{\Gamma \vdash \mathbf{mksem} MN : \mathbb{S}} $$

the so-called bad variable and bad semaphore constructs.
Bad variables and semaphores are not sensible programming primitives, they are here by necessity for definability. Indeed, up to isomorphism $V$ is defined as $(\&_{n \in \mathbb{N}} U) \& N$, and strategies inhabiting it may not be linked with actual memory cells: they may be formed by pairing arbitrary “write” and “read” methods. Thus, to obtain a finite definability result, one must include such pairings should be formable in the syntax <fnref n="3" />.

Through the isomorphisms $V \cong (\&_{n \in \mathbb{N}} U) \& N$ and $S \cong U \& U$, the interpretation is:

$$[[\mathbf{mkvar} M N]] = \langle\langle [[M]] n \mid n \in \mathbb{N} \rangle\rangle, \quad [[\mathbf{mksem} M N]] = \langle\langle [[M]] \mid [[N]] \rangle\rangle,$$

which are the final two clauses of the interpretation of IA.

## 4.3 Complements on Alternating Strategies

In this section, we introduce a few complements on the results and constructions of this chapter. Those may be skipped on first reading; they are intended either as a reference, or because they are referred to further along in this monograph.

### 4.3.1 Complements on Single-Threadedness

First of all, we have introduced in Section 3.3.1 the notion of single-threaded strategies, as a way to enforce that distinct initial moves generate separated copies of the strategy, which may not communicate or share any state. Here we give some complements.

Here we focus on the concept of threads:

**Definition 4.3.1.** An alternating thread on arena A is $t \in \mathcal{I} \uparrow \text{-Play}_s(A)$ with at most one initial move; write $\mathcal{I} \uparrow \text{-Play}_s(A)$ for the set of alternating threads on A.

We mean to make formal that if $\sigma$: A is single-threaded, then it is determined by its set of threads – so it should be equivalently described by a *thread-strategy*:

**Definition 4.3.2.** For A an arena, an alternating thread-strategy $\sigma$: A is a set $\sigma \subseteq \mathcal{I} \uparrow \text{-Play}_s(A)$ satisfying the following conditions:

$$
\begin{array}{ll}
\text{non-empty:} & \epsilon \in \sigma, \\
\text{prefix-closed:} & \forall s \subseteq t \in \sigma, s \in \sigma, \\
\text{receptive:} & \forall s \in \sigma, sa^- \in \mathcal{I} \uparrow \text{-Play}_s(A) \Rightarrow sa^- \in \sigma, \\
\text{deterministic:} & \forall sa^- b_1^+, sa^- b_2^+ \in \sigma, sab_1 = sab_2,
\end{array}
$$

and it is additionally **well-bracketed** if it satisfies

well-bracketing: for all $ta^+ \in \sigma$, if $t$ is well-bracketed then so is $ta$.

<footnote n="3">³A definability result without bad variables can be obtained by switching to nominal games [Tzevelekos, 2009], where nominal techniques are employed to attach reference cells to actual memory locations, but the setting gets more complicated. It must also be mentioned that though finite definability fails for IA without bad variables, full abstraction still holds as proved by McCusker [McCusker, 2003]</footnote>
This is, of course, the same conditions as for Definition 3.1.5, except than they are taken within $\downarrow\uparrow$-Plays$_*(A)$ rather than $\downarrow\uparrow$-Plays$(A)$. Clearly, if $\sigma: A$ is an alternating strategy (single-threaded or not), then $\sigma \cap \downarrow\uparrow$-Plays$_*(A)$ is a thread-strategy.

Reciprocally, we construct a single-threaded strategy from a thread-strategy on A:

**Proposition 4.3.3.** Consider $\sigma$ a thread-strategy on arena A.

Then, constructing the set $\sigma^1$ comprising all plays $s \in \downarrow\uparrow$-Plays$(A)$ which satisfy

threaded-correct: for all $ta^+ \subseteq s$, we have $[ta^+] \in \sigma$,

it follows that $\sigma^1$ is a single-threaded strategy on A.

*Proof.* First, the conditions non-empty, prefix-closed and receptive are clear from the definition. For the rest, we first observe that any $s \in \sigma^1$ is well-threaded, in the sense that for all $ta^-b^+ \subseteq s$, $b$ points within $[sa^-]$. Indeed, for each initial move $s_i$ in $s$, we have $s \vdash i$, comprising the moves of $s$ hereditarily justified by $s_i$, a thread which by condition thread-correct must be in $\sigma$ thus, in particular, alternating. For each $t \subseteq s$ we may define $t \vdash i$ a prefix of $s \vdash i$. Since each $t \vdash i$ is alternating, it is immediate by induction that for $t \subseteq s$ of even length, all $t \vdash i$ have even length, while if $t$ has odd length, exactly one $i_0$ is such that $t \vdash i_0$ has odd length. But then, considering $ta^-b^+ \subseteq s$, at $ta^-$ the only thread with odd length must be $[ta^-]$, which $b^+$ must extend so as to satisfy our invariant; thus $b^+$ must indeed point within $[sa^-]$.

We prove further conditions. For deterministic, if $sa^-b_1^+, sa^-b_2^+ \in \sigma^1$, then we have that $[sa^-b_1^+]$, $[sa^-b_2^+] \in \sigma$, but by our observation above those have the form $ta^-b_1^+, ta^-b_2^+ \in \sigma$ for $ta^- = [sa^-]$. Hence $ta^-b_1^+ = ta^-b_2^+$ by determinism of $\sigma$, from which follows $sa^-b_1^+ = sa^-b_2^+$. Finally, conditions well-threaded and single-threaded of Definition 3.3.2 follow directly from our observation above. $\square$

Any thread-strategy yields a single-threaded strategy, but reciprocally all single-threaded strategies have this form, as we show now:

**Proposition 4.3.4.** Consider $\sigma: A$ a single-threaded strategy. Then, the set

$$ \llbracket \sigma \rrbracket = \{[s] \mid s \in \sigma\} = \sigma \cap \downarrow\uparrow$-Plays$_*(\sigma) $$

is a thread-strategy on A, such that $\sigma = \llbracket \sigma \rrbracket^1$.

*Proof.* It is direct that if $\sigma: A$ is single-threaded, then $\llbracket \sigma \rrbracket = \sigma \cap \downarrow\uparrow$-Plays$_*(A)$; from which it is easy that $\llbracket \sigma \rrbracket$ satisfies the conditions of Definition 4.3.2.

Now, we prove that $\sigma = \llbracket \sigma \rrbracket^1$. For $\subseteq$, consider $s \in \sigma$ and $ta^+ \subseteq s$. Since $ta^+ \in \sigma$, we have $[ta^+] \in \llbracket \sigma \rrbracket$ by definition, hence $s \in \llbracket \sigma \rrbracket^1$. For $\supseteq$, consider $s \in \llbracket \sigma \rrbracket^1$. It is then direct to prove by induction on $s$ that $s \in \sigma$: for negative extensions, this follows from receptivity, for positive extensions from single-threaded. $\square$

Thus altogether, this gives single-threaded alternating strategies two representations: as a single-threaded set of plays with many initial moves, or as a set of threads. This exactly reflects the two presentations of innocent strategies, as sets of plays or as sets of P-views, that was described in Section 3.2.4. We observe a useful consequence:
**Corollary 4.3.5.** Consider $\sigma, \tau : A$ single-threaded strategies.
If $\sigma$ and $\tau$ have the same threads, then they are equal.

*Proof.* Straightforward from Proposition 4.3.4. □

**Further conditions.** Finally, we show how this correspondence preserves the further conditions we considered on alternating strategies. Observe first that the notions of *well-bracketing* and *P-visibility*, respectively introduced in Definitions 3.2.6 and 3.2.8, are conditions on plays and as such transparently apply to thread-strategies. Then:

**Lemma 4.3.6.** Consider $\sigma : A$ a thread-strategy. Then:

(1) $\sigma^1$ is well-bracketed iff $\sigma$ is well-bracketed,

(2) $\sigma^1$ is P-visible iff $\sigma$ is P-visible.

*Proof.* (1) Only if. Straightforward since $\sigma \subseteq \sigma^1$. If. We show by induction on $s$ that for all $s \in \sigma^1$, the pending question is always in the current thread – the result follows.

(2) Only if. As above, follows from $\sigma \subseteq \sigma^1$. If. Follows from the easy observation that the P-view is always contained within the current thread. □

## 4.3.2 Factorization and Definability

With the details of the interpretation in place, we revisit some of the properties of the semantics presented in Chapter 3, providing key steps of the definability proof.

**Innocent definability.** First of all, recall that all finite innocent well-bracketed strategies are definable within PCF (Theorem 3.2.14). But this result only concerns PCF types – we must first generalize it to all IA types, including references and semaphores:

**Theorem 4.3.7.** Let A be an IA type, and $\sigma : [[A]]$ be finite well-bracketed innocent.
There is an IA term $\vdash M : A$, without **newref** or **newsem**, s.t. $[[M]] = \sigma$.

*Proof.* Direct variation of Theorem 3.2.14, crucially using **mkvar** and **mksem**. □

**Factorization.** Thus, extending types from PCF to IA does not affect the innocent definability result. But how can it be generalized to *non-innocent* strategies?

For IA, the main argument is a *factorization result* [Abramsky and McCusker, 1996]:

**Proposition 4.3.8.** Consider an arena $A = A_1 \Rightarrow \dots \Rightarrow A_n \Rightarrow X$, and $\sigma : A$ visible,
well-bracketed, single-threaded. Then there is an innocent $\mathbf{Inn}(\sigma) : V \Rightarrow A$ such that

$$ \mathit{newr}_A \odot \mathbf{Inn}(\sigma) = \sigma $$

for $\mathit{newr}_A$ obtained from $\mathit{newr}_X$ via the cartesian closed structure in the obvious way.
Moreover, if $\sigma$ is finite (resp. computable), then so is $\mathbf{Inn}(\sigma)$.
Sketch. As an innocent strategy, Inn($\sigma$) can only depend on the P-view and hence can-
not act as $\sigma$, which depends on the full play. But the idea is that Inn($\sigma$) can access the
full play indirectly, by maintaining in the reference (an encoding of) the full play. More
precisely, each time it receives an Opponent move $a^-$, Inn($\sigma$) first reads the reference
and obtains (the encoding of) a play $s \in \sigma$. Assuming $sa^-b^+ \in \sigma$, Player stores (the
encoding of) $sa^-b^+$ in the reference, then plays $b^+$. □

This provides the missing argument for finite definability (and hence intensional full
abstraction) for IA: if $[[A]] = A_1 \Rightarrow \dots \Rightarrow A_n \Rightarrow X$ and $\sigma : [[A]]$ is a finite visible,
well-bracketed and single-threaded strategy, then one first obtains a finite innocent and
well-bracketed $\mathbf{Inn}(\sigma) : \mathbf{V} \Rightarrow [[A]]$ by Proposition 4.3.8. By Theorem 4.3.7, there is
$\vdash M : \mathbf{V} \to A$ in IA such that $[[M]] = \mathbf{Inn}(\sigma)$, but then, as required,

$$
[[\lambda x_1 \dots x_n. \mathbf{newref} \ r \ \mathbf{in} \ M \ x_1 \dots x_n \ r]] = \sigma : [[A]]
$$

concluding the proof of finite definability for IA – note that if Theorem 4.3.7 is extended
to a universality result as is expected following Conjecture 3.2.15, we get that every
computable P-visible well-bracketed single-threaded strategy in IA is definable.

4.3.3 Summary of Results

Now that we have introduced the proper categories supporting the interpretations un-
derlying Chapter 3, we restate for future reference the main theorems of that chapter
with proper reference to the target categories of the interpretations:

**Proposition 4.3.9.** *There is a computationally adequate interpretation of IA in $\downarrow\uparrow$-Strat.*

Proof. First stated as Proposition 4.3.9.

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

**Theorem 4.3.10.** *The interpretation of Proposition 4.3.9 refines into an interpretation of PCF in $\downarrow\uparrow$-InnWB, which is intensionally fully abstract.*

Proof. First stated as Theorem 3.2.16.

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

**Theorem 4.3.11.** *The interpretation of Proposition 4.3.9 refines into an interpretation of IA in $\downarrow\uparrow$-WB, which is intensionally fully abstract.*

Proof. First stated as Theorem 3.3.5.

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

4.4 Conclusions and Historical Notes

The compositional setting presented here is robust to a number of variations: for in-
stance, *determinism* can be relaxed, obtaining an intensionally fully abstract model
for an extension of IA with non-deterministic choice<fnref n="4" /> [Harmer and McCusker, 1999].
Non-deterministic strategies can additionally be weighted by *probabilities*, yielding
a model intensionally fully abstract for an extension of IA with probabilistic choice

<footnote n="4">⁴That is not the case with AJM games – determinism is crucial in the way AJM games handle uniformity.</footnote>
[Danos and Harmer, 2000]. However, neither of these two extensions support a notion of innocence banning state: they do not restrict to intensionally fully abstract models for either non-deterministic or probabilistic PCF. Among other things, this is what this monograph aims to solve, as motivated in the introduction.

Beyond those non-deterministic and probabilistic extensions, this alternating compositional setting presented here has seen so many extensions and applications that it would be a daunting task to attempt to survey them exhaustively, and we leave this beyond the scope of this short conclusion. Many extensions keep the general structure of plays and strategies, changing mostly the arenas: a crucial example of that is game semantics for call-by-value [Abramsky and McCusker, 1997, Honda and Yoshida, 1999], or for polarized versions of linear logic [Laurent, 2002]. Other extensions build on the present compositional mechanism, but bring additional structure to moves and/or plays, such as *names* [Tzevelekos, 2009] or *exception pointers* [Laird, 2001a].

A more drastic change is to abandon *alternation* in order to model concurrent computation [Laird, 2001b, Ghica and Murawski, 2008], but this does affect rather deeply the compositional machinery presented in this chapter: we present this next.
# Chapter 5

## Non-Alternating Game Semantics

In this chapter, we continue our introduction to game semantics by presenting the non-alternating version of the games model seen so far. The chapter roughly follows the outline of the previous two chapters: first, we introduce non-alternating plays and strategies appealing to operational intuitions in the style of Chapter 3. Then, we introduce the category $\mathcal{O}-\mathbf{Strat}$, describe the interpretation of $IA_\parallel$, and prove its properties.

The constructions of this chapter mostly follow [Ghica and Murawski, 2008].

### 5.1 Concurrency and Non-Alternation

Thus, let us start again from the intuitions described in Section 3.1, representing interactive executions as plays, and ask ourselves the following question: how should plays be amended if execution is no longer sequential, but becomes concurrent?

#### 5.1.1 Non-Alternating Plays

**Non-alternation.** As a first, example, consider the following program $M$ from $PCF_\parallel$

$$x : \mathbb{N}, y : \mathbb{N} \vdash \mathbf{let} \left( \begin{array}{l} x_1 = x \\ x_2 = y \end{array} \right) \mathbf{in} x_1 + x_2 : \mathbb{N},$$

which evaluates $x$ and $y$ in parallel, then returns their sum. Or more precisely, the intention of the program is to evaluate $x$ and $y$ in parallel, but really the execution order depends on the scheduler. It may still be the case that $x$ is evaluated before $y$, as in the first example of Section 3.1.1. Or, perhaps, the scheduler will evaluate $y$ before $x$. Or
<figure><img src="image_41.png" /><figcaption>Figure 5.1: Operational content of a non-alternating play</figcaption></figure>

they might indeed be evaluated simultaneously, so we must account for the dialogue

O : “What is the return value?”

P : “What is the value of x?”

P : “What is the value of y?”

O : “The value of x is 12.”

O : “The value of y is 30.”

P : “The value of x + y is 42.”

where the evaluation request for y does not wait for the return value for x.

This naturally brings us to the following variation over Definition 3.1.4:

**Definition 5.1.1.** A non-alternating pre-play on A is a legal pointing sequence on A.
We write $\mathcal{O}-\text{PrePlays}(A)$ for the set of non-alternating pre-plays on A.

This is simply Definition 3.1.4 without the condition *alternating*. In other words, *non-alternating pre-play* is a synonym for *legal pointing string*, though we prefer to keep the names separate for conceptual clarity.

**Plays and executions.** Non-alternating pre-plays are represented with the same con-
ventions as alternating plays. As for alternating plays, the non-alternating pre-plays of
a term may be thought of operationally, as illustrated in Figure 5.1.

This example also shows that even for programs which do not use parallel evaluation
as a primitive, the switch from alternating plays to non-alternating plays is impactful:
plays may also describe executions where it is Opponent who first plays concurrently. In
Figure 5.1, Opponent, playing for the argument $f: \mathcal{U} \to \mathcal{U} \to \mathcal{U}$, simultaneously calls
its two arguments. This triggers a *race*, as the two write requests are being evaluated
simultaneously, yielding a non-deterministic result. So in non-alternating games, terms
from IA – a deterministic language – may still have non-deterministic behaviour.

Figure 5.1 is misleading in one respect: it makes it seem like the Player move $\check{+}$
*coincides* with the memory update. In reality, it is an acknowledgment for which we can
only know for sure that it comes *after* the memory update: the message may stay stuck
<figure><img src="image_42.png" /><figcaption>Figure 5.2: Alternative result</figcaption></figure>

in a buffer for a while. The behaviour in Figure 5.2, with exactly the same play until the final result, is just as possible. The consequence of this is that the order in which consecutive acknowledgments arrive is *not* representative of the order in which memory operations are handled: it is irrelevant and cannot influence subsequent behaviour.

**Well-bracketing.** As in sequential games, constructing the games model will require us to introduce a notion of *well-bracketing*. In our presentation of sequential games, *plays* were not well-bracketed; instead well-bracketing was a property of *strategies*<fnref n="1" />. Here we make the opposite choice and impose it directly on *plays*: defining cleanly non-alternating strategies for the primitives of $IA_\parallel$ without well-bracketing becomes very challenging, as we are overwhelmed by the number of *plays*.

As in the alternating case, non well-bracketed plays allow behaviours typical of control operators such as **callee** – with the new addition of parallel versions, such as the **fork** operator on $\mathbb{B}$ that answers **tt** and **ff** in parallel, see [Castellan, 2015]. As in the alternating case, these behaviours must be banned via an adequate condition. By analogy we still call it *well-bracketing*, though this is a bit of a misnomer: for instance,

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

is a perfectly acceptable play for the constant **tt**, though the third move does not answer the pending question. Intuitively, this play is an interleaving of two evaluations of **tt** progressing independently. While each, taken independently, is indeed well-bracketed in the sense of alternating game semantics, this is blurred out in their interleaving – the notion of “pending question” does not make sense anymore.

Thus we must constrain the interplay between questions and answers differently:

**Definition 5.1.2.** Consider A an arena, and s a non-alternating pre-play.

<footnote n="1">¹For modeling IA, both choices are possible, but our discussion on the semantic cube in Section 3.3.3 requires non well-bracketed plays as doing otherwise is incompatible with the interpretation of **callee**.</footnote>
<figure><img src="image_44.png" /><figcaption>Figure 5.3: Logical well-bracketing is weaker than well-bracketing</figcaption></figure>

We say that *s* is logically well-bracketed iff it satisfies the conditions:

fork: for $t \quad q \quad t' \quad m \subseteq s$, *q* is unanswered in *t*'.

join: for $t \ q \ t' \ a^A \subseteq s$, all questions justified by $q$ are answered in $t'$.

By *answer-closing* of Definition 3.2.4, moves labelled *q* are necessarily questions in this definition. Rather than *chronological*, the constraint is *logical*; it is about the hierarchical relationship between functions and arguments. *Fork* means that if a call returns, it can neither return again nor investigate its arguments anymore; *join* means that a call cannot return if there are un-terminated argument calls currently running.

For $s \in \mathcal{D}^\uparrow\mathcal{P}\mathcal{A}^s(A)$ alternating, if $s$ is well-bracketed (in the sense of Definition 3.2.5) then it is logically well-bracketed (in the sense of Definition 5.1.2. However, the converse does not hold as illustrated by Figure 5.3. We may then define:

**Definition 5.1.3.** A *non-alternating play* on *A* is a (logically) well-bracketed *non-alternating pre-play* on *A*. We write $\mathcal{O}^\mathcal{P}\mathcal{A}^s(A)$ for alternating legal plays on *A*.

Recall that the set of alternating legal plays on $A$ was written $\mathcal{D}^\uparrow\mathcal{P}\mathcal{A}^s(A)$, where $\mathcal{D}^\uparrow$
evokes the transition between states O and P, depending on whose turn it is. Here, $\mathcal{O}$
evokes the fact that there is only one state, where both players can potentially play.

It is a puzzling fact that logical well-bracketing may replace chronological well-
bracketing in alternating strategies also, and still get intensional full abstraction for IA
(but not definability), despite the example in Figure 5.3. This boils down to the fact that
logically well-bracketed *complete* plays (i.e. P- and O-visible, and all questions have an
answer) are automatically well-bracketed – so e.g. Figure 5.3 cannot be completed.

**5.1.2 Non-Alternating Strategies**

Now, for strategies, which conditions of Definition 3.1.5 survive? *Non-empty*, *prefix-closed* and *receptive* still make sense. However *deterministic* is unreasonable, firstly because of the non-determinism introduced by the scheduler’s choices, and secondly because a non-deterministic choice may be defined in $IA_{\#}$ (see **choice** in Section 2.2.3).
<figure><img src="image_45.png" /><figcaption>Figure 5.4: Two consecutive P-moves</figcaption></figure>

<figure><img src="image_46.png" /><figcaption>Figure 5.5: The other order</figcaption></figure>

<figure><img src="image_47.png" /><figcaption>Figure 5.6: Two exchangeable moves</figcaption></figure>

<figure><img src="image_48.png" /><figcaption>Figure 5.7: The other order</figcaption></figure>

As a first approximation of non-alternating strategies, we set:

**Definition 5.1.4.** Consider A an arena.

A non-alternating prestrategy $\sigma : A$ is a set $\sigma \subseteq \mathcal{O}\text{-Plays}(A)$ satisfying:

$$ \begin{array}{ll} \text{non-empty:} & \epsilon \in \sigma, \\ \text{prefix-closed:} & \forall s \sqsubseteq t \in \sigma, s \in \sigma. \end{array} $$

Though receptive still makes sense, it is more useful technically to let prestrategies not be receptive, and impose receptivity only later on in Definition 5.1.5.

**Saturation.** Perhaps less obvious is the fact that we need a new condition.

We already mentioned that in a non-alternating play, part of the order in which moves appear is irrelevant. Imagine a program features consecutive Player moves:

$$ \dots m_1^+ m_2^+ \dots \in \mathcal{O}\text{-Plays}(A). $$

Since the play is non-alternating, according to our operational intuition this means that two threads are currently under execution. So we are as in Figure 5.4, which illustrates that: (1) Player has no control over the order in which the two positive moves appear, which is the scheduler's prerogative; and (2) if the positive moves are exchanged, we reach nevertheless the same program state. So the order of two contiguous Player moves is irrelevant, they can be exchanged without affecting the future of the execution.
A symmetric situation is that of two consecutive Opponent moves, in which case, likewise their order is irrelevant and they can be exchanged without affecting the future of execution. Finally, consider a program in IA$_{‖}$ with a play of the form

$$ \dots m_1^+ m_2^- \dots \in \mathcal{O}\text{-Pla\`ys}(A) $$

where $m_2$ is not justified by $m_1$. In that case we are as in Figure 5.6 and the positive $m_1$ can always be postponed until after the negative $m_2$, reaching the same program state, and thus not affecting the future computation. But finally, one cannot always postpone an Opponent move after a Player move: the Player move may actually depend on the Opponent move. Overall, the relevant information in $s \in \mathcal{O}\text{-Pla\`ys}(A)$ is only that which survives permutations as described above; and accordingly we shall require that non-alternating strategies should be *saturated* under those.

Integrating this condition, the definition of non-alternating strategies becomes:

**Definition 5.1.5.** Consider A an arena.

A non-alternating strategy $\sigma : A$, or $\mathcal{O}$-strategy for short, is a prestrategy s.t.:

receptive: $\forall s \in \sigma, sa^- \in \mathcal{O}\text{-Pla\`ys}(A) \Rightarrow sa^- \in \sigma,$

courteous: for $sbat \in \sigma$ with $\text{pol}(a) = +$ or $\text{pol}(b) = -$,
then if $sbat \in \mathcal{O}\text{-Pla\`ys}(A)$, $sbat \in \sigma$ as well.

where it is understood that $sbat$ and $sbat$ have the same pointers.

The earliest appearance of such a saturation that we are aware of is by Selinger [Selinger, 1997]. It seemed to have first appeared in game semantics in [Laird, 2001b], and was called saturation in [Ghica and Murawski, 2008]. We refer to it as courtesy, a terminology imported from [Melliès and Mimram, 2007]: this is for compatibility with the terminology in the forthcoming concurrent games, where the same behaviour is imposed causally rather than by a saturation condition.

It is notable that non-alternating game semantics is obtained “only” by changing the nature of plays: the arenas, representing types, will remain the same.

### 5.1.3 Single-Threadedness

Are all non-alternating strategies sensible w.r.t. IA$_{‖}$?

It is clear that it is not the case: the same phenomenon as in Section 3.3.1 occurs. As in the alternating case, we must impose a condition ensuring that the state is local, in that no information flows between distinct instances of the program. By analogy with the alternating case, we call this *single-threadedness*. But we must warn the reader that this by no means implies that our strategies can only have a single “thread” as in concurrent programming! *Single-threadedness* means that each initial move spawns an independent copy of this program, even if that program is multi-threaded.

But single-threadedness cannot be imported transparently from alternating strategies. Though the *current thread* (Definition 3.3.1) seemingly still makes sense, Player may
have control over several threads simultaneously, as in the play on B displayed below

$$q^{-} \dotfill q^{-} \dotfill t^{+} \dotfill t^{+}$$

which will belong to the strategy for the constant $t$. The last move fails condition *well-threaded* of Definition 3.3.2 even though $t$ does behave independently on all copies.

So we have to approach the issue a bit differently. First, define:

**Definition 5.1.6.** A non-alternating thread on arena A is $t \in \mathcal{O}-\mathcal{Pla}^{\mathcal{y}s}(A)$ with at most one initial move; write $\mathcal{O}-\mathcal{Pla}^{\mathcal{y}s}_{\bullet}(A)$ for the set of non-alternating threads on A.

Single-threaded behaviour is defined first via single threads, which invites:

**Definition 5.1.7.** Consider A an arena.

A thread-strategy $\sigma : A$ is a set $\sigma \subseteq \mathcal{O}-\mathcal{Pla}^{\mathcal{y}s}_{\bullet}(A)$ satisfying:

$$\text{receptive: } \forall s \in \sigma, sa^{-} \in \mathcal{O}-\mathcal{Pla}^{\mathcal{y}s}_{\bullet}(A) \Rightarrow sa^{-} \in \sigma,$$

as well as non-empty, prefix-closed and courteous as in Definitions 5.1.4 and 5.1.5.

As in Definition 5.1.4, a thread-prestrategy is a prestrategy $\sigma \subseteq \mathcal{O}-\mathcal{Pla}^{\mathcal{y}s}_{\bullet}(A)$.

Note that unlike in Definition 5.1.4, receptive must be restricted to threads.

Given a thread-strategy $\sigma : A$, a full non-alternating strategy may be defined by interleaving copies of $\sigma$. Given $s, t \in \mathcal{O}-\mathcal{Pla}^{\mathcal{y}s}(A)$, $s \sqcup t \subseteq \mathcal{O}-\mathcal{Pla}^{\mathcal{y}s}(A)$ denotes the set of interleavings of $s$ and $t$. If $X, Y \subseteq \mathcal{O}-\mathcal{Pla}^{\mathcal{y}s}(A)$, $X \sqcup Y$ is defined as the union of all $s \sqcup t$, for $s \in X$ and $t \in Y$. Finally, if $X \subseteq \mathcal{O}-\mathcal{Pla}^{\mathcal{y}s}(A)$, we set

$$X^{(0)} = \{\epsilon\} \\ X^{(n+1)} = X \sqcup X^{(n)}$$

and $X^1 \subseteq \mathcal{O}-\mathcal{Pla}^{\mathcal{y}s}(A)$, the iterated interleaving of $X$, is $X^1 = \cup_{n \in \mathbb{N}} X^{(n)}$. We have:

**Definition 5.1.8.** Consider A an arena, and $\sigma : A$ a non-alternating strategy on A.
We say that $\sigma$ is single-threaded if there is $\tau : A$ a thread-strategy such that $\sigma = \tau^1$.

In that case $\tau$ is uniquely determined, as it must be the set of threads in $\sigma$. If $\sigma : A$ is a non-alternating strategy on A, write $\sigma^\bullet$ for its set of threads – $\sigma$ is single-threaded iff $\sigma = (\sigma^\bullet)^1$. It also directly follows from Definition 5.1.8 that we have:

**Lemma 5.1.9.** Consider $\sigma, \tau : A$ single-threaded non-alternating strategies.

Then, $\sigma = \tau$ if and only if $\sigma^\bullet = \tau^\bullet$.

### 5.1.4 Full Abstraction for IA$_{\parallel}$

As we shall spell out in Section 5.2, arenas and single-threaded non-alternating strategies form a cartesian closed category $\mathcal{O}-\mathbf{Strat}$ which supports the interpretation of IA$_{\parallel}$. More precisely, types and contexts are interpreted as arenas exactly as in Chapter 4 (IA$_{\parallel}$ brings no new type), and a term $\Gamma \vdash M : A$ is interpreted as a morphism

$$[M] \in \mathcal{O}-\mathbf{Strat}([\Gamma], [A]).$$
<figure><img src="image_49.png" /><figcaption>Figure 5.8: A realizable non P-visible play</figcaption></figure>

<figure><img src="image_50.png" /><figcaption>Figure 5.9: Example of definability of plays in IA<sub>//</sub></figcaption></figure>

**Realizing plays.** But do we have more than IA<sub>//</sub>? It is natural to expect that the answer is yes: in the alternating setting, *P-visibility* is required to ban higher-order references (see Section 3.3.2), and we have not imposed any such condition here.

But P-visibility is not adequate: strategies from IA<sub>//</sub> will not satisfy it, even though we only have ground type references. Figure 5.8 illustrates why: several threads in parallel may cause executions which are undistinguishable, viewed from the outside, from a non-local control flow due to a higher-order reference. In Figure 5.8, one cannot observe that the occurrence of the last move after the next-to-last is entirely coincidental, in that the two moves really belong to completely independent threads.

This phenomenon is general: given a play *s*, it is fairly easy to produce a term that can realize *s*, though typically along with many other plays. We can do this via a purely parallel term that simply mimics the hierarchical dependencies imposed by justification pointers. For instance, for *s* on the left hand side of Figure 5.9, one obtains the term

$$ \lambda x^{\mathcal{U}_1} f^{\mathcal{U}_2 \to \mathcal{U}_3} y^{\mathcal{U}_4}. (x \parallel f \textbf{skip} \parallel y); \perp. \quad (5.1) $$
**Definability.** Now, can we produce a term that realizes *exactly* s, and not more? Not in the strictest sense, since strategies interpreting terms will always be sets of plays satisfying Definition 5.1.5. But there is always a *smallest* strategy containing s:

**Lemma 5.1.10.** Consider $\sigma : A$ a thread-prestrategy.

Then, there is a unique least (for inclusion) thread-strategy $\hat{\sigma} : A$ s.t. $\sigma \subseteq \hat{\sigma}$. Its plays are deduced from $\sigma$ by applying receptive and courteous from Definition 5.1.5.

Regarding $s \in \mathcal{O}-\text{Plays}_s(A)$ as a thread-prestrategy implicitly by prefix-closure, we have $\hat{s} : A$ its **saturation**, a thread-strategy, and $\hat{s}' : A$ a single-threaded strategy.

The saturation process generates many plays, which are however succinctly summarized via a causal dependency between moves: a move depends on another when they cannot be permuted by courtesy. This happens if one points to the other; or for a Player move appearing after an Opponent move in s. It is helpful conceptually to represent these constraints via a diagram on moves, and this is done on the rhs of Figure 5.9: we draw the dependency due to pointers as dotted lines (read from top to bottom), and the dependency from negative moves to positive moves as arrows $\rightarrow$. The resulting object is close to a concurrent strategy in the sense of Part II – by design, $\hat{s}$ comprises exactly the plays that are linearizations of this diagram (with pointers following dotted lines).

Now, we observe that in our example, the purely parallel term of (5.1) captures exactly the static/dotted dependencies on the rhs of Figure 5.9. To capture $\hat{s}$, we must also account for the arrows $\rightarrow$, and this is done by exploiting the memory. For that we define two helper functions. If $M : \forall$, we write $\text{set}(M) : \cup$ for $M := 1$, and $\text{test}(M) : \cup$ for if (iszero !M) $\perp$ skip which converges iff !M is non-zero. Then:

$$ \lambda x \cup_1 f \cup_2 \rightarrow_3 y \cup_4 . \left( \left( \begin{array}{c} x ; \\ \mathbf{set}(\checkmark_1^-) \end{array} \right) \right) \left\| \left( \left( \begin{array}{c} f(\mathbf{set}(\mathbf{q}_2^-)) ; \\ \mathbf{test}(\checkmark_4^-) ; \\ \mathbf{grab}(\checkmark_2^+) ; \\ \mathbf{skip} \end{array} \right) \right) \right\| \left( \left( \begin{array}{c} \mathbf{test}(\checkmark_1^-) ; \\ \mathbf{test}(\mathbf{q}_2^-) ; \\ y ; \\ \mathbf{set}(\checkmark_4^-) \end{array} \right) \right) ; \perp $$

borrows the shape of (5.1), additionally signaling the $\rightarrow$-links through memory (we omit reference and semaphore creations wrapping the term). We use one fresh reference (initialized to 0) for each Opponent move, which gets set to 1 when the Opponent move occurs. Finally, we must ensure that Opponent replications does not cause a duplication of Player moves by prompting re-evaluation of the corresponding subterms, so that we only obtain linearizations of the diagram on the right hand side of Figure 5.9. For that we add semaphores which are grabbed, but never released.

Done systematically for arbitrary plays [Ghica and Murawski, 2008], we get:

**Proposition 5.1.11.** Consider A an arena, and $s \in \mathcal{O}-\text{Plays}_s(A)$.

Then, there is a term $\vdash M : A$ of $IA_\parallel$ such that $[M] = \hat{s}'$.

From this, it is deduced in [Ghica and Murawski, 2008] that we have:

**Theorem 5.1.12.** Arenas and single-threaded strategies form an intensionally fully abstract model for $IA_\parallel$. Moreover, given $\Gamma \vdash M, N : A$, we have

$$ M \approx N \Leftrightarrow \text{comp}([M]) = \text{comp}([N]), $$
where comp($\sigma$) is the set of **non-alternating complete plays**, i.e. **non-alternating plays** such that all questions have an answer.

## 5.2 The Ambiant Cartesian Closed Category ⊔-Strat

As in the alternating case, we now focus on the compositional construction of non-alternating strategies from terms, starting with the categorical structure.

### 5.2.1 Constructing ⊔-Strat

As for alternating strategies, a **non-alternating strategy from A to B** is a non-alternating strategy on $A \Rightarrow B$. The composition of non-alternating strategies largely follows the same route as for alternating strategies in Section 4.1.2, with a few minor changes.

**Interactions.** Consider $\sigma : A \Rightarrow B$ and $\tau : B \Rightarrow C$ non-alternating strategies. As in Section 4.1.2, we start with an appropriate notion of interactions:

**Definition 5.2.1.** Consider A, B and C arenas.

A **non-alternating interaction** on A, B, C is a legal pointing sequence on ($A \Rightarrow B \Rightarrow C$ satisfying the conditions fork and join of Definition 5.1.2).

We write $\mathcal{O}-I(A, B, C)$ the set of all non-alternating interactions on A, B, C.

It is useful to compare with Definition 4.1.6 in the alternating case: the conditions *outer-legal*, *left-legal* and *right-legal*, which amount to all restrictions being alternating, become unnecessary: all restrictions are automatically valid non-alternating plays.

We use the same terminology and conventions as in the alternating case (notably regarding the polarities of moves, see below Definition 4.1.6) for non-alternating interactions. However, the state diagram of Figure 4.2 disappears. Just as plays, non-alternating interactions have no well-defined state, and both players can play anywhere at any time provided the move they play is justified and compatible with well-bracketing.

**Composition.** We now define composition, first for *prestrategies*:

**Definition 5.2.2.** Consider $\sigma : A \Rightarrow B$ and $\tau : B \Rightarrow C$ non-alternating prestrategies.

An **interaction** between $\sigma$ and $\tau$ is any $u \in \mathcal{O}-I(A, B, C)$ such that $u \uparrow A, B \in \sigma$ and $u \uparrow B, C \in \tau$. We write $\sigma \parallel \tau$ for the set of all interactions between $\sigma$ and $\tau$.

We may then define the **composition** $\tau \odot \sigma = \{u \uparrow A, C \mid u \in \sigma \parallel \tau\} : A \Rightarrow C$.

As in the alternating case, if $s \in \tau \odot \sigma$ then by definition there must be some $u \in \sigma \parallel \tau$ such that $s = u \uparrow A, C$, called a **witness** for $s$. However, unlike in the alternating case, the witness is no longer unique. Composition is associative:

**Proposition 5.2.3.** Consider $\sigma : A \Rightarrow B, \tau : B \Rightarrow C$ and $\upsilon : C \Rightarrow D$ prestrategies.

Then, $(\upsilon \odot \tau) \odot \sigma = \upsilon \odot (\tau \odot \sigma)$.

*Proof.* Same proof as in the alternating case: one defines the set $IA(A, B, C, D)$ of ternary interactions as comprising well-bracketed legal pointing sequence on ($A \Rightarrow B \Rightarrow C$).
B) ⇒ C) ⇒ D. Then, one proves a "zipping lemma" with almost the same statement as Lemma 4.1.10 – with only the uniqueness clause missing – and the proof follows transparently as in Proposition 4.1.11 (uniqueness of witness is not needed). ☐

Note that associativity holds already for composition of prestrategies, without relying on receptivity or courtesy. However, we will need these conditions shortly.

We mention the following preservation proposition [Ghica and Murawski, 2008]:

**Proposition 5.2.4.** Consider $\sigma : A \Rightarrow B$ and $\tau : B \Rightarrow C$ prestrategies. Then:

> if $\sigma$ and $\tau$ are strategies, then so is $\tau \odot \sigma$,
> if $\sigma$ and $\tau$ are single-threaded, then so is $\tau \odot \sigma$.

**Copycat.** Composition of non-alternating strategies is as direct as in the alternating case – perhaps simpler, as interactions are “wilder”, not having to follow the rigid structure imposed by alternation and the state diagram. But non-alternation also means that identities cannot be as simple as in Definition 4.1.12: copycat must handle Opponent moves arriving in bulk, possibly before earlier Opponent moves are propagated.

Nevertheless, the non-alternating copycat can be succinctly defined by:

**Definition 5.2.5.** Consider A any arena, and $\mathcal{C}_A^*$ the set of threads of $\mathcal{C}_A$.

The non-alternating copycat on A, written $\mathcal{O}-\mathcal{C}_A$, is simply defined as $\mathcal{C}_A^*!$.

So $\mathcal{O}-\mathcal{C}_A$ is the smallest non-alternating strategy including the alternating copycat. Despite the overload of notations, we will often still refer to the non-alternating copycat simply with $\mathcal{C}_A$ – hopefully, the context should always be sufficient to disambiguate. We shall reserve $\mathcal{O}-\mathcal{C}_A$ for when we need to be extra explicit. Likewise, we shall use $\downarrow\uparrow-\mathcal{C}_A$ for the alternating copycat, when we feel it is useful to emphasize that this is not $\mathcal{O}-\mathcal{C}_A$.

This definition is succinct but not so explicit, so we illustrate it with a play of the non-alternating copycat in Figure 5.2.1. As long as Opponent “plays in turn”, copycat remains alternating. But if Opponent plays several moves in a row – before the previous ones can be propagated – then copycat maintains a buffer of moves to be forwarded and plays them (not necessarily in the same order as they arrived), attempting to restore the same state between the right hand side and the left hand side.

As required, the non-alternating copycat is neutral for composition with respect to non-alternating strategies. In fact, we have the following proposition:

**Proposition 5.2.6.** Consider A, B arenas, and $\sigma : A \Rightarrow B$ a prestrategy.

Then, $\sigma$ is a non-alternating strategy iff $\mathcal{O}-\mathcal{C}_B \odot \sigma = \sigma \odot \mathcal{O}-\mathcal{C}_A = \sigma$.

*Proof.* Direct adaptation of [Ghica and Murawski, 2008, Lemma 16]. ☐

It follows that we have:

**Corollary 5.2.7.** There is a category $\mathcal{O}-\text{Strat}$ with arenas as objects, and as morphisms from A to B all single-threaded strategies on $A \Rightarrow B$.
<figure><img src="image_51.png" /><figcaption>Figure 5.10: An example play of the non-alternating copycat</figcaption></figure>

### 5.2.2 Cartesian Closed Structure

The cartesian closed structure essentially follows that of $\downarrow\uparrow$-Strat.

**Cartesian structure.** On objects, the cartesian structure is defined as in $\downarrow\uparrow$-Strat: the empty arena 1 with no moves is a terminal object, and the product of two arenas A and B is $A \times B$ as defined in Definition 4.1.1. For arenas A, B, the projections

$$ \mathcal{O}-\pi_A : A \times B \Rightarrow A, \qquad \mathcal{O}-\pi_B : A \times B \Rightarrow B $$

are the copycat strategies defined with the obvious adaptation of Definition 5.2.5.

To define the pairing, we prove:

**Lemma 5.2.8.** Consider $\Gamma$, A, B arenas, and $\sigma : \Gamma \Rightarrow A$, $\tau : \Gamma \Rightarrow B$ single-threaded non-alternating strategies. Then, there exists a single-threaded non-alternating

$$ \langle \sigma, \tau \rangle : \Gamma \Rightarrow A \times B, $$

whose set of threads is (up to relabeling) the disjoint union of the threads of $\sigma$ and $\tau$.

*Proof.* Straightforward by definition of single-threaded non-alternating strategies. $\square$

Again, this data satisfies the required equations for cartesian products:

**Lemma 5.2.9.** Consider $\sigma : \Gamma \Rightarrow A$, $\tau : \Gamma \Rightarrow B$, and $\nu : \Delta \Rightarrow \Gamma$ single-threaded. Then, the following equations hold:

$$ \mathcal{O}-\pi_A \odot \langle \sigma, \tau \rangle = \sigma $$

$$ \mathcal{O}-\pi_B \odot \langle \sigma, \tau \rangle = \tau $$

$$ \langle \mathcal{O}-\pi_A, \mathcal{O}-\pi_B \rangle = \mathcal{O}-\mathcal{C}_{A \times B} $$

$$ \langle \sigma, \tau \rangle \odot \nu = \langle \sigma \odot \nu, \tau \odot \nu \rangle. $$
*Proof.* The first two equalities are a variation of Proposition 5.2.6, first proved for threads and extended to strategies via Lemma 5.1.9. The last two are direct on threads and generalized by Lemma 5.1.9. □

It follows from these equations that we have the desired structure:

**Corollary 5.2.10.** *The category $\mathcal{O}$-Strat is cartesian.*

**Cartesian closed structure.** Now, we describe the cartesian closure.

On arenas, $A \Rightarrow B$ is of course the same construction as for alternating strategies. We have seen in Lemma 4.1.18 that there is an isomorphism of arenas

$$ \Xi_{\Gamma,A,B} : (\Gamma \times A) \Rightarrow B \cong \Gamma \Rightarrow (A \Rightarrow B) $$

which, as in the alternating case, immediately yields a bijection:

**Lemma 5.2.11.** *Consider $\Gamma$, $A$ and $B$ three arenas. Then, there is a bijection*

$$ \Lambda_{\Gamma,A,B} : \mathcal{O}\text{-Strat}(\Gamma \times A, B) \approx \mathcal{O}\text{-Strat}(\Gamma, A \Rightarrow B) $$

preserving composition in the sense that

$$ \Lambda_{\Gamma,A,B}(\sigma) \odot \gamma = \Lambda_{\Delta,A,B}(\sigma \odot (\gamma \times A)) $$

for all $\sigma \in \mathcal{O}\text{-Strat}(\Gamma \times A, B)$ and $\gamma \in \mathcal{O}\text{-Strat}(\Delta, \Gamma)$.

*Proof.* A routine manipulation on interactions. □

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

In turn, this bijection lets us define the evaluation strategy simply as

$$ \mathcal{O}\text{-ev}_{A,B} = \Lambda_{A,A,B}^{-1}(\mathcal{O}\text{-c}_{A \Rightarrow B}) \in \mathcal{O}\text{-Strat}((A \Rightarrow B) \times A, B) $$

and from the above, it becomes routine to prove cartesian closure:

**Proposition 5.2.12.** *The category $\mathcal{O}$-Strat is cartesian closed.*

*Proof.* As for Proposition 4.1.20. □

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

### 5.2.3 Recursion

As for alternating strategies, non-alternating strategies are partially ordered by inclusion. This partial order is preserved by all operations, yielding:

**Proposition 5.2.13.** *For any two arenas $A$ and $B$, $\mathcal{O}$-Strat($A$, $B$) is partially ordered by inclusion, yielding a pointed dcpo. All operations on strategies involved in the cartesian closed structure are continuous, making $\mathcal{O}$-Strat enriched over pointed dcpos.*

*Proof.* Direct verifications. □

<figure><img src="image_54.png" /></figure>
As in the alternating case, we define

$$ F : \mathcal{O}\text{-Strat}(A \Rightarrow A, A) \rightarrow \mathcal{O}\text{-Strat}(A \Rightarrow A, A) \\ \sigma \mapsto \lambda f^{A \Rightarrow A} \cdot f(\sigma f) $$

a continuous operation whose least fixed point

$$ \mathcal{O}\text{-}\mathcal{Y}_A = \bigcup_{n \in \mathbb{N}} F^n(\perp) \in \mathcal{O}\text{-Strat}(A \Rightarrow A, A) \quad (5.2) $$

satisfies $\mathcal{O}\text{-}\mathcal{Y}_A = F \mathcal{O}\text{-}\mathcal{Y}_A$ by construction and provides the interpretation of recursion.

## 5.3 Interpretation of IA$_{\parallel}$

### 5.3.1 Interpretation of PCF$_{\parallel}$

First of all, *types* and *contexts* of PCF are interpreted exactly as in $\downarrow\uparrow$-Strat.

For *terms*, any $\Gamma \vdash M : A$ gets interpreted as a morphism

$$ [[M]] \in \mathcal{O}\text{-Strat}([\Gamma], [[A]]). $$

As for $\downarrow\uparrow$-Strat, the primitives for the simply-typed $\lambda$-calculus and for recursion are interpreted using the structure above. It remains to provide interpretations for all the additional combinators that PCF adds to the simply-typed $\lambda$-calculus.

**PCF.** Constants are interpreted by single-threaded strategies returning directly the corresponding value – due to non-alternation, this means they have plays such as

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

for skip : $U$, interleaving various calls in an asynchronous fashion – the generating thread-strategy is simpler to describe, with only one maximal play $q^- \checkmark \check{+}$.

The interpretation of PCF is obtained via the same clauses as in alternating games, in Figure 4.5. This uses single-threaded non-alternating strategies seq, if, succ, iszero and pred whose thread-strategies are exhaustively presented as comprising prefixes of plays of the form displayed in Figures 4.4 and 4.6. Non-alternation does not induce additional plays, because we required that non-alternating plays should be well-bracketed thus Opponent can answer at most once. The strategy let comprises more plays than its alternating version in Figure 4.7. We omit however its definition, obtained as an obvious simplification of the new operation that PCF$_{\parallel}$ adds to PCF: the parallel let.

**PCF$_{\parallel}$**. To complete the interpretation of PCF$_{\parallel}$, we need a single-threaded strategy

$$ \text{plet}_{X,Y} : \quad X \Rightarrow X \Rightarrow (X \Rightarrow X \Rightarrow Y) \Rightarrow Y $$

for the parallel let. Intuitively, its behaviour is simple enough: upon being called, *plet* will interrogate its first two arguments in parallel. Upon receiving two values, it will
<figure><img src="image_56.png" /><figcaption>Figure 5.11: Typical play of $plet_{X,Y}$.</figcaption></figure>

interrogate its function argument and provide it the two values. We show one of its typical plays, in Figure 5.11. It acts in two subsequent stages: first the parallel evaluation of arguments, and then the call to the functional argument with the memoized values.

To define $plet_{X,Y}$ formally, we define sets of pointing sequences for these two stages. Annotating types as $X_1 \Rightarrow X_2 \Rightarrow (X \Rightarrow X \Rightarrow Y) \Rightarrow Y$, for $v$ and $w$ values of $X$, we set

$$ \text{force}_{v,w} ::= \begin{array}{l} \mathbf{q}_1^+ v_1^- \mathbf{q}_2^+ w_2^- | \mathbf{q}_2^+ w_2^- \mathbf{q}_1^+ v_1^- | \mathbf{q}_1^+ \mathbf{q}_2^+ v_1^- w_2^- \\ | \mathbf{q}_1^+ \mathbf{q}_2^+ w_2^- v_1^- | \mathbf{q}_2^+ \mathbf{q}_1^+ v_1^- w_2^- | \mathbf{q}_2^+ \mathbf{q}_1^+ w_2^- v_1^- \end{array} $$

where it is understood that $v_1^-$ points to $\mathbf{q}_1^+$ and $w_2^-$ points to $\mathbf{q}_2^+$.

Next, for the second stage we define another set of pointing sequences, written $eval_{v,w}$. Its elements are obtained by first considering the threads in the strategy

$$ \lambda x^X. \lambda y^X. \lambda f^{X \Rightarrow X \Rightarrow Y}. f v w : X \Rightarrow X \Rightarrow (X \Rightarrow X \Rightarrow Y) \Rightarrow Y, $$

defined exploiting the cartesian closed structure of $\mathcal{O}$-Strat and the corresponding internal language. From such threads, elements of $eval_{v,w}$ are obtained by removing the initial question. Finally, we form the set of pointing sequences

$$ \text{prelet}_{X,Y} = \bigcup_{v,w} \mathbf{q}^- \cdot \text{force}_{v,w} \cdot \text{eval}_{v,w} $$
completed into a set of plays by reinstating the missing pointers in the unique possible way, with missing pointers assigned to the initial move $q^-$. Finally, the non-alternating thread-strategy for $plet_{X,Y}$ is obtained as interleavings of all prefixes of $prelet_{X,Y}$.

Altogether, we obtain $plet_{X,Y} : X \Rightarrow X \Rightarrow (X \Rightarrow X \Rightarrow Y) \Rightarrow Y$ and we complete the interpretation of $PCF_\parallel$ by adding to Figure 4.4 the additional clause

$$[[\Gamma \vdash \textbf{let} \left( \begin{array}{l} x_1 = N_1 \\ x_2 = N_2 \end{array} \right) \textbf{in } M : \mathcal{Y}]] = \textbf{plet}_{X,Y} \circled{!} \langle [[N_1]], [[N_2]], \Lambda^1(\Lambda^1(\langle [M] \rangle)) \rangle$$

### 5.3.2 Interpretation of State

The types $\mathcal{V}$ and $\mathcal{S}$ are interpreted by the same arenas as in Section 4.2.2.

**Queries.** As in the alternating case, we set the interpretation of queries as

$$ \begin{align*} [[M := N]] &= \text{assign} \circ \langle [[N]], [[M]] \rangle \\ [[!M]] &= \text{deref} \circ [[M]] \\ [[\textbf{grab}(M)]] &= \text{grab} \circ [[M]] \\ [[\textbf{release}(M)]] &= \text{release} \circ [[M]] \end{align*} $$

using the single-threaded non-alternating strategies with threads as in Figures 4.11, 4.12, 4.13, and 4.14 – the same basic plays as in the alternating case.

**Declaration.** Now, we must provide the interpretation for the declaration of new references and semaphores. For that, we need non-alternating versions of the strategies for reference and semaphore declaration introduced in Section 4.2.2.

Rather than going again through the concrete definition of these strategies, we set

$$ \mathcal{O}\text{-newr}_X = \widehat{\text{newr}}^*_{X}!, \qquad \mathcal{O}\text{-news}_X = \widehat{\text{news}}^*_{X}! $$

via the saturation process of Lemma 5.1.10, and use those in:

$$ \begin{align*} [[\textbf{newref } x := n \textbf{ in } M]] &= \mathcal{O}\text{-newr}_X \circ \Lambda(\langle [M] \rangle) \in \mathcal{O}\text{-Strat}([[\Gamma]], \langle [A] \rangle) \\ [[\textbf{newsem } x := n \textbf{ in } M]] &= \mathcal{O}\text{-news}_X \circ \Lambda(\langle [M] \rangle) \in \mathcal{O}\text{-Strat}([[\Gamma]], \langle [A] \rangle). \end{align*} $$

**Bad variables and semaphores.** As in the alternating case, through the isomorphisms $\mathcal{V} \cong (\&_{n \in \mathbb{N}} \mathcal{U}) \& \mathcal{N}$ and $\mathcal{S} \cong \mathcal{U} \& \mathcal{U}$, the interpretation is:

$$ [[\textbf{mkvar } M N]] = \langle \langle\langle [M] \rangle n \mid n \in \mathbb{N} \rangle, [[N]] \rangle, \quad [[\textbf{mksem } M N]] = \langle\langle [M] \rangle, [[N]] \rangle, $$

which concludes the interpretation of $IA_\parallel$.
### 5.3.3 Summary of Results

This concludes the construction of the cartesian closed category $\mathcal{O}\text{-Strat}$, as well as the interpretation of $IA_\llcorner$. As in the alternating case, we conclude the technical content of this chapter by summing up a few key results for future reference.

**Proposition 5.3.1.** *There is an adequate interpretation of $IA_\llcorner$ in $\mathcal{O}\text{-Strat}$.*

*Proof.* The interpretation is as described in its chapter. Computational adequacy corresponds to the particular case of Theorem 5.1.12 instantiated on ground type. $\square$

**Theorem 5.3.2.** *The interpretation of Proposition 5.3.1 refines into an interpretation of $IA$ in $\mathcal{O}\text{-Strat}$, which is intensionally fully abstract.*

*Proof.* First stated as Theorem 5.1.12. $\square$

## 5.4 Conclusions and Historical Notes

The first to consider a non-alternating version of play-based game semantics was Laird, who proposed a fully abstract model for a message-passing language called Idealized CSP [Laird, 2001b]. This model had much in common with the one presented here, however plays are equipped with additional “concurrency pointers”, which explicitly mark the different threads acting in a non-alternating plays. Ghica and Murawski’s model was first published in 2004 [Ghica and Murawski, 2004], in conference format. It is strongly related to the non-alternating games of Melliès and Mimram published soon after [Melliès and Mimram, 2007], which contains the definition of a category of games and linear non-alternating strategies, along with an adequate notion of innocence.

Just like in the alternating case in the presence of state, non-alternating games form an effectively presentable fully abstract model, which lead to decision algorithms for observational equivalence – though for very restricted languages: first bounding the number of threads via a type system [Ghica et al., 2006] so that strategies are representable as finite automata, and more recently via other finitary restrictions that allow a representation of non-alternating strategies via more elaborate notions of data automata [Dixon et al., 2021a, Dixon et al., 2021b].

It is noteworthy, in the definability process outlined in Proposition 5.1.11, that it seems we really need semaphores in order to capture a single play. Murawski explored what happened without semaphores [Murawski, 2010]; he proved that then strategies are closed under a stuttering behaviour that affect observational equivalence. This shows that, perhaps surprisingly, semaphores are not definable just via references up to observational equivalence – another of those very results which illustrates well the strength of game semantics.

This concludes the preliminary part. One of the purposes of the rest of this monograph will be to construct and explore $\rightarrow\text{-Strat}$, a *causal* version of $\mathcal{O}\text{-Strat}$.
# Part II

## Thin Concurrent Games
Introduction to Part II

<figure><img src="image_57.png" /><figcaption>Figure 5.12: To survive pointer showers, remember to bring your parallel-or umbrella!</figcaption></figure>

Now that we have spent significant time building up a background on traditional play-
based game semantics, let us forget it all and start from scratch!

*Concurrent games* reject the premise that there exists a global clock; instead relying on a *causal* presentation of program behaviour. This idea was pioneered by Abramsky and Melliès [Abramsky and Melliès, 1999], and its consequences were mainly explored by Melliès in his sequence of insightful papers on *asynchronous games* [Melliès, 2003, Melliès, 2004a, Melliès, 2004b, Melliès, 2005, Melliès and Mimram, 2007]. Inheriting from this, the definitions on which we build were first proposed by Rideau and Winskel [Rideau and Winskel, 2011], also building on other work [Faggian and Hyland, 2002, Curien and Faggian, 2005, Faggian and Piccolo, 2009] inspired by *ludics* – we redirect to Section 6.5 for a longer discussion on the history of these notions.

While thin concurrent games share much conceptually with the game semantics of Part I, they build on a completely different – and more sophisticated – technical basis: the theory of event structures. This enhances their expressiveness, but with the cost of an involved technical development, for two reasons.
Firstly, event structures are more elaborate than the usual objects used in game semantics, such as sequences of moves. Manipulating them rigorously is more complex than for plays, involving a demanding – but (perhaps subjectively) rather elegant – infrastructure involving significant mathematical engineering and ingenuity.

Secondly, we cannot get away with some of the usual informal practice of traditional game semantics. Indeed, researchers in game semantics have sometimes adopted a somewhat informal mathematical style – the strategy does this, if Opponent plays this then the strategy reacts by playing that, *etc*. While this has been criticized, it is true that such phrasings in the literature can usually be unambiguously made formal if needed (though in practice this is rarely done); but this is thanks to the fact that the mathematical objects involved are rather simple and closely follow their natural language description. So it is both the curse and the blessing of concurrent games that when strategies are event structures, such informal descriptions are no longer reasonable.

So, we must prepare the reader for a long mathematical development, in part because of the complexity of our strategies, because the development is carried out with more mathematical precision than is the standard in many game semantics texts, but also because we have taken the space to make the development as pedagogical as possible.

The purpose of Part II is the construction of so-called “thin concurrent games” along with the categorical structure needed to interpret the simply-typed $\lambda$-calculus, leaving for Part III the interpretation of $IA_\parallel$ and its fragments. We consider that the key contribution of Part II is the bicategory **TCG**, a setting for strategies-as-event-structures able to handle symmetry and the interchangeability of moves as required for copy indices and uniformity (in the sense of Section 3.4). We arrive there in two stages: first, in Chapter 6 we develop the bicategory **CG** of concurrent games *without symmetry*; then Chapter 7 introduces **TCG**, a conservative extension of **CG** equipping it to handle symmetry. Finally, **TCG** is only a bicategory and as such does not yet have the further categorical structure required to handle the interpretation of programming language; for that, in Chapter 8 we construct **NTCG**, essentially a model of intuitionistic linear logic with an exponential ! so that the Kleisli category **NTCG**! is cartesian closed.
# Chapter 6

## Basic Concurrent Games

In this chapter, relying on the intuitions introduced previously for traditional game semantics, we introduce the bicategory CG, the foundation for concurrent games on event structures. We do this for pedagogical reasons: CG is only a stepping stone, as it does not yet support the exponential (!) – this will require the addition of symmetry in Chapter 7. But it seems better to first construct CG separately, so as to give the proper spotlight to quite a few new conceptual ideas, instead of introducing everything simultaneously.

CG is a non-deterministic extension of Melliès and Mimram's non-alternating asynchronous games [Melliès and Mimram, 2007]; it was first introduced by Rideau and Winskel in [Rideau and Winskel, 2011] (see also [Castellan et al., 2017a]). The presentation given here is new, exploiting insights obtained over the years, from our experience of working with concurrent games.

### 6.1 Games and Strategies as Event Structures

#### 6.1.1 Basic Intuitions on Concurrent Strategies

**Parallelism.** In the beginning of Section 5.1.1, we motivated non-alternating strategies by considering the plays in a parallel implementation of the arithmetic sum

$$x : \mathbb{N}, y : \mathbb{N} \vdash \text{let} \left( \begin{array}{l} x_1 = x \\ x_2 = y \end{array} \right) \text{in } x_1 + x_2 : \mathbb{N},$$

which we argued required to account for all the orders in which the evaluations of x and y could be performed by the scheduler. Rather than writing down all these interleavings,
an alternative could be to write – naively for now – a diagram of the form:

$$x : \mathbb{N}, y : \mathbb{N} \vdash \mathbb{N}$$

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

the Hasse diagram of a *partial order* in which the two sub-computations occur in in-
dependent branches. As for sequential plays in game semantics, this diagram is read
from top to bottom: first, Opponent initiates computation with $q^{-}$. But then, there are
two follow-ups: the two occurrences of $q^{+}$, prompting the evaluation of the two argu-
ments. Despite them being in the same row, they are not thought of as simultaneous.
Instead they are *independent*: there is no well-defined ordering between them. Concur-
rent strategies display explicitely this independence, whereas the non-alternating game
semantics of Chapter 5 would convey it implicitly by allowing all interleavings.

In a diagram as above, the vertical axis no longer represents time. Instead, the partial order is thought of as expressing *causality*: in order to observe the two occurrences of $q^{+}$, we *must* have seen $q^{-}$. In order to observe (this occurrence of) the answer 42, we *must* have seen the two arguments converge with values 12 and 30.

**Non-determinism.** In such diagrams, the branching structure indicates parallelism, not non-determinism. But then, how is non-determinism going to be represented?

Our answer is to mark branchings that correspond to non-deterministic choice:

B

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

In this diagram, which represents the non-deterministic choice of a boolean, $tt^{+}$ and $ff^{+}$ are linked with a wiggly line indicating *conflict*: only one of them can be seen in a given execution. This marks that the branching is a *non-deterministic* rather than a *parallel* branching. Such situations with these two branching structures are captured by the mathematical notion of an *event structure*, introduced formally in Section 6.1.2.

Concurrent strategies explicitely display all non-deterministic choices, even when
they do not yet yield visibly different behaviours. For instance, in the diagram

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

corresponding e.g. to the term $\lambda f^{\mathbb{B} \to \mathbb{B}}$. ($f \tt \to \mathbb{B}$) ($f \mathbf{ff} \to \mathbb{B}$) for $\mathbb{B}$ a non-deterministic choice operator, the two conflicting occurrences of $q^+$ correspond to the *same* observable behaviour, but they should be kept separate because they have distinct futures. In general, concurrent strategies remember all non-deterministic choices even when they lead to no observable difference: $\mathbf{tt} \mathbb{B} \mathbf{tt}$ will *not* yield the same concurrent strategy as $\mathbf{tt}$.

**Causality.** Though we have motivated the use of partial order models for representing strategies by examples from parallel and non-deterministic computation, we shall see throughout this monograph that it has a deep impact even for pure sequential deterministic computation. As an example, the term $\lambda f.f. \mathbf{tt} \mathbf{ff}$ admits the causal behaviour

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

where it is apparent that the two branches where Opponent explores the two arguments are *causally independent* from each other. In fact, in that case the tree structure coincides with the tree of *P*-views as described in Section 3.2.4, exposing its causal nature.

### 6.1.2 Formalizing Concurrent Strategies

Such diagrams as above, mixing causal dependency and conflict, are certain *event structures* – the partial order model at the core of concurrent games.

**Event structures.** We first define *event structures*<fnref n="1" />:

**Definition 6.1.1.** An *event structure* (es) is a triple $E = (|E|, \le_E, \#_E)$, where $|E|$ is a (countable) set of *events*, $\le_E$ is a partial order called *causal dependency* and $\#_E$ is an

<footnote n="1">¹In the literature, those event structures are called *prime event structures with binary conflict*.</footnote>
irreflexive symmetric binary relation on $|E|$ called conflict, satisfying:

finite causes: $\forall e \in E, [e]_E = \{e' \in E \mid e' \leq_E e\}$ is finite,

conflict inheritance: $\forall e_1 \#_E e_2, \forall e_2 \leq_E e'_2, e_1 \#_E e'_2$.

A given event has only finitely many causes: this fundamental axiom means that any event can appear in a finite execution. *Conflict inheritance* is sometimes called the *vendetta axiom*: conflicts transfer to children, and to their children, and so on for ever. It ensures that two non-conflicting events can always appear together in a finite execution (as the causal dependencies of non-conflict events must be non-conflicting).

The diagrams appearing earlier in this section may be read as event structures. For $E$ an event structure, the **immediate causal dependency** $\rightarrow_E$ is defined as $e \rightarrow_E e'$ if $e <_E e'$ with no event in between: for all $e'' \in E$, $e \leq_E e'' \leq_E e'$ we have $e = e''$ or $e'' = e'$. Likewise, the **immediate conflict** $e \sim_{\sim_E} e'$ means that $e \#_E e'$ and the conflict is not inherited: if $e'' <_E e$, $\neg(e'' \#_E e')$ and if $e'' <_E e'$, $\neg(e \#_E e'')$. These two notations are intensively used, in particular when drawing event structures. For instance, in the diagram (6.1), $tt^+$ and $ff^+$ are in conflict (as they depend on conflicting events), but not in immediate conflict – so they are not linked with a wiggly line.

The most fundamental definition on an event structure is *configurations* – one may regard an event structure as a concrete representation of its set of configurations:

**Definition 6.1.2.** A (finite) configuration of event structure $E$ is a finite $x \subseteq |E|$ s.t.:

down-closed: $\forall e \in x, \forall e' \in E, e' \leq_E e \Rightarrow e' \in x$

consistent: $\forall e, e' \in x, \neg(e \#_E e')$.

We write $\mathscr{C}(E)$ for the set of finite configurations on $E$.

Configurations are the *states* of an event structure: conflict-free finite sets of events with all causal dependencies satisfied. Though a configuration is merely a set, it inherits a partial order which is often drawn in pictures from that of the ambient event structure.

The set $\mathscr{C}(E)$ is naturally ordered by inclusion; it is the *domain of configurations*. Configurations are typically ranged over by variables $x, y, z$. For $x, y \in \mathscr{C}(E)$, we write $x \not\subset y$ if $x$ is immediately below $y$ in the inclusion order, i.e. there is $e \in E$ such that $e \notin x$ and $y = x \cup \{e\}$ – we also write $x \vdash_E e$ and say that $x$ **enables** $e$.

**Games.** Before we formalize strategies, let us look at *games*.

As for arenas, our *games* present observable computational events, along with their dependencies and conflict. In spirit, the way this is done is very close to the arenas of Chapter 3. For instance, the games representing respectively $\mathbb{B}$ and $\mathbb{U}$ are:

$$ B = \begin{tikzpicture}[baseline=(current bounding box.center), scale=0.5, every node/.style={scale=0.5}] \node (q) [q-] at (0,0) {};
\node (u) [u-] at (0,1) {};
\node (tup) [tup-] at (1,0) {};
\node (tupup) [tup-] at (1,1) {};
\draw (q) -- (u);
\draw (u) -- (tup);
\draw (tup) -- (tupup);
\draw (tupup) -- (q);
\node (qup) [q-] at (2,0) {};
\node (uf) [uf-] at (2,1) {};
\node (ff) [ff-] at (2,2) {};
\node (ffup) [ff-] at (2,3) {};
\draw (qup) -- (uf);
\draw (uf) -- (ff);
\draw (ff) -- (ffup);
\draw (ffup) -- (qup);
\node (qupup) [q-] at (3,0) {};
\node (ufup) [uf-] at (3,1) {};
\node (ffup) [ff-] at (3,2) {};
\node (ffupup) [ff-] at (3,3) {};
\draw (qupup) -- (ufup);
\draw (ufup) -- (ffup);
\draw (ffup) -- (ffupup);
\draw (ffupup) -- (qupup);
\end{tikzpicture} \quad U = \begin{tikzpicture}[baseline=(current bounding box.center), scale=0.5, every node/.style={scale=0.5}] \node (q) [q-] at (0,0) {};
\node (u) [u-] at (0,1) {};
\node (qup) [q-] at (1,0) {};
\node (qupup) [q-] at (1,1) {};
\draw (q) -- (u);
\draw (u) -- (qup);
\draw (qup) -- (qupup);
\draw (qupup) -- (q);
\node (qupup) [q-] at (2,0) {};
\node (uf) [uf-] at (2,1) {};
\node (ff) [ff-] at (2,2) {};
\node (ffup) [ff-] at (2,3) {};
\draw (qupup) -- (uf);
\draw (uf) -- (ff);
\draw (ff) -- (ffup);
\draw (ffup) -- (qupup);
\node (qupup) [q-] at (3,0) {};
\node (ufup) [uf-] at (3,1) {};
\node (ffup) [ff-] at (3,2) {};
\node (ffupup) [ff-] at (3,3) {};
\draw (qupup) -- (ufup);
\draw (ufup) -- (ffup);
\draw (ffup) -- (ffupup);
\draw (ffupup) -- (qupup);
\end{tikzpicture} \quad (6.2) $$

where the first is to be compared with the arena for booleans in traditional arena games in Figure 3.8. It is the same, except that the two answers are conflicting: unlike in
traditional game semantics, concurrent games are inherently linear (or rather, affine) and a question may be by default answered at most once. This hints at a deeper difference: in Figure 3.8, the initial question may appear arbitrarily many times in a play. In contrast, the intention here is that a given move can be played at most once: an execution such as at the beginning of Section 3.3.1 would make sense not on B but on its “bang”

$$ !B = \begin{tikzpicture}[baseline=(current bounding box.center), scale=0.5] \draw (0,0) node[above] {$\mathbf{q}_0^-$}; \node at (0,0.5) {$\sim$}; \node at (0,-0.5) {$\mathbf{t}_0^+$}; \draw (0,0) to node[left] {$\mathbf{q}_1^-$} (1,0); \node at (1,0) {$\sim$}; \node at (1,0.5) {$\mathbf{t}_1^+$}; \draw (1,0) to node[left] {$\mathbf{q}_2^-$} (2,0); \node at (2,0) {$\sim$}; \node at (2,0.5) {$\mathbf{t}_2^+$}; \draw (2,0) to node[left] {$\mathbf{q}_5^-$} (3,0); \node at (3,0) {$\sim$}; \node at (3,0.5) {$\mathbf{f}_0^+$}; \draw (3,0) to node[left] {$\mathbf{f}_1^+$} (4,0); \node at (4,0) {$\sim$}; \node at (4,0.5) {$\mathbf{f}_2^+$}; \draw (4,0) to node[left] {$\mathbf{f}_3^+$} (5,0); \node at (5,0) {$\sim$}; \node at (5,0.5) {$\mathbf{f}_5^+$}; \dots \end{tikzpicture} \quad (6.3) $$

involving *copy indices* as in AJM games (see Section 3.4) – but we push this operation aside until Chapter 7, as developing it properly also requires a model in which one can express that all copies are interchangeable, which plain event structures cannot do.

Games feature causal dependency and conflict, hence are *also* event structures:

**Definition 6.1.3.** A game is an es $A = (|A|, \le_A, \#_A)$ with a *polarity function*

$$ \mathrm{pol}_A : |A| \to \{-, +\}. $$

The polarity function simply indicates whether a given move is due to Player (+) or Opponent (-). Though games are event structures, we draw them with specific conventions: in particular, as in (6.2) and following our earlier convention for arenas, immediate causal dependency in games is drawn with dotted lines rather than with the usual symbol $\to$. Having distinct notations for immediate causal dependency in games and strategies will allow us later on to have diagrams with two immediate dependencies superimposed, from a game and from a strategy.

In practice, games in the sense of Definition 6.1.3 are way too wild for our purposes. The games arising from the interpretation of types will have a very specific shape: they are negative (Opponent starts), alternating (immediate causal links are always between different players), forestial (there is no causal merge) and conflict is local (between two moves with the same predecessor, if any). But for the sake of economy, we shall impose such conditions only when they become technically required.

**Prestrategies.** If both strategies and games are to be event structures, what does it mean that an event structure “plays” on another event structure? It is natural to model such a situation as an event structure (the strategy) *labeled* by an event structure (the game), where the labelling function should be a *map of event structures*:

**Definition 6.1.4.** Consider E, F two es. A *map of event structures* $f : E \to F$ is

$$ f : |E| \to |F| $$

a function on events satisfying the further two conditions below:

configuration-preserving: for all $x \in \mathcal{C}(E)$, $f(x) \in \mathcal{C}(F)$,

locally injective: for all $e_1, e_2 \in x \in \mathcal{C}(E)$, if $f e_1 = f e_2$ then $e_1 = e_2$.
This is a kind of simulation map. It transports valid states into valid states while preserving atomicity: within a configuration $x \in \mathscr{C}(E)$, local injectivity ensures that $f$ induces a bijection $f: x \approx f x$; adding an event to $x$ must add an event to $fx$. We shall review a few basic properties of maps of event structures in Section 6.1.3, but for now they let us introduce a first approximation of strategies-as-event-structures:

**Definition 6.1.5.** A prestrategy on game A is a tuple $\sigma = (|\sigma|, \leq_{\sigma}, \#_{\sigma}, \partial_{\sigma})$ where

$$ \partial_{\sigma} : \sigma \to A $$

is a map of event structures.

Observe that here $\sigma$ is a plain event structures, not assumed equipped with a polarity function. Nevertheless, there is an induced notion of polarity on $\sigma$, obtained as $\text{pol}_{\sigma}(s) = \text{pol}_{A}(\partial_{\sigma}(s))$ – we shall use this implicitly from now on.

In contrast with Definition 3.1.2, a prestrategy is not a collection of standalone executions (plays), but one global object, an event structure $\sigma$, aggregating all possible executions. The events in $|\sigma|$ are not events of the game: they are internal to the prestrategy, only linked to the game via the *display map* $\partial_{\sigma}$.

For instance, we may have a prestrategy (in fact, a strategy) on U:

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

with the obvious mapping $\partial_{\sigma}(\bullet_1) = \mathbf{q}^{-}$ and $\partial_{\sigma}(\bullet_2) = \partial_{\sigma}(\bullet_3) = \mathbf{\check{+}}$. We generally prefer drawing (pre)strategies as on the right hand side, which retains all the relevant information, only omitting the *names* of events in $\sigma$ (i.e. $\bullet_1, \bullet_2, \bullet_3$)$^2$.

**Strategies.** The definition of prestrategies ignores polarities, thus not all prestrategies are computationally sensible – we need conditions analogous to Definition 5.1.5:

**Definition 6.1.6.** A prestrategy $\sigma$ on game A is a *strategy* if it satisfies:

courteous: for all $s_1 \dashv\sigma s_2$, if $\text{pol}(s_1) = +$ or $\text{pol}(s_2) = -$ then $\partial_{\sigma}(s_1) \dashv_A \partial_{\sigma}(s_2)$,

receptive: for all $x \in \mathscr{C}(\sigma)$, for all $\partial_{\sigma}(x) \vdash_A a^{-}$, there is a unique $x \vdash_{\sigma} s$ such that $\partial_{\sigma}(s) = a^{-}$,

We write $\sigma : A$ to mean that $\sigma$ is a strategy on game A.

*Receptive* forces strategies to acknowledge uniquely any possible move by Opponent. Finally, *courtesy* gets two birds with one stone. Firstly, it forbids causal links of the form $s_1 \dashv\sigma s_2^{-}$ which are not in the game – a strategy cannot force Opponent to wait before playing a move available in the game. Secondly, it also forbids causal links of the form $s_1^{+} \dashv\sigma s_2^{+}$ not in the game. This is to be understood as an *asynchrony* requirement:

<footnote n="2">²This diagram exploits our convention to write immediate causal links differently in games and strategies.</footnote>
sending two events in causal dependency to causally independent moves. Thus causality is not preserved, but we do have a property in the other direction:

**Lemma 6.1.8.** Consider $f : E \to F$ a map of event structures.
Then, for all $e, e' \in x \in \mathscr{C}(E)$, if $fe \leq_F fe'$ then $e \leq_E e'$.

*Proof.* Since $e' \in E$, we have $[e']_E \in \mathscr{C}(E)$, hence $f[e']_E \in \mathscr{C}(F)$ since $f$ preserves configurations. But by construction, $fe' \in f[e']_E$. Since $f[e']_E \in \mathscr{C}(F)$, it is in particular down-closed. Hence, since $fe \leq_F fe'$, we must have $fe \in f[e']_E$. But this means that there is some $e'' \in [e']_E$ such that $fe'' = fe$ – in other words, there is $e'' \leq_E e'$ such that $fe'' = fe$. Now, we remark that we have $e' \in x$, so as $x$ is down-closed, we must have $e'' \in x$ as well. Thus $e, e'' \in x$ have the same image by $f$, thus $e = e''$ by local injectivity. Hence, we have proved that $e \leq_E e'$ as required. $\square$

Recall that we have defined prestrategies as maps $\partial_\sigma : \sigma \to A$. For $\sigma : A$, the lemma above means that if $s, s' \in x \in \mathscr{C}(\sigma)$, if $\partial_\sigma s \leq_A \partial_\sigma s'$ then $s \leq_\sigma s' -$ in other words, any “static” causal dependency imposed by the game must be respected by the strategy as well. But causality is reflected only within configurations: the map

$$ \begin{array}{ccc} 1 & \sim & 1' \\ \downarrow 2 & & \rightarrow \\ \downarrow & & \downarrow 2 \end{array} $$

is valid, though we have $f1' \leq f2$ but $\neg(1' \leq 2)$ as they are in conflict.

The maps of event structures that are monotone are called **rigid**. In that case:

**Lemma 6.1.9.** Consider $f : E \to F$ a rigid map of event structures.
Then, $f$ preserves immediate causality.

*Proof.* Left as an exercise to the reader. $\square$

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

Rigid maps $f : E \to F$ are too constrained to be interesting as strategies, but they are useful as a sort of inclusions of $E$ within $F$, collapsing non-deterministic branches. The *morphisms between strategies*, as defined in Definition 6.1.7, are rigid maps.

In Definition 6.1.7 we encountered for the first time the *isomorphisms* in the category of event structures, as induced by Definition 6.1.4. It is worth pointing out explicitly that such isomorphisms of event structures (and thus, isomorphisms of strategies) are simply *renamings* of the events, preserving and reflecting all structure:

**Lemma 6.1.10.** Consider $E, F$ event structures, $f : E \to F$ an isomorphism of es.
Then, $f$ is a bijection between events, satisfying the following two properties:

(1) for all $e, e' \in E, e \leq_E e'$ iff $f(e) \leq_F f(e')$,

(2) for all $e, e' \in E, e \#_E e'$ iff $f(e) \#_F f(e')$.

*Proof.* Left as an exercise to the reader. $\square$

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

Reciprocally, bijections satisfying properties (1) and (2) above are obviously isomorphisms of event structures – clearly, the two strategies of (6.4) are isomorphic.
**Mapification.** The above shows that a map of es $f : E \to F$ should not be viewed
as a map of posets; instead it should be seen as a concrete presentation of

$f : \mathcal{C}(E) \to \mathcal{C}(F)$

a monotone function between the generated domains of configurations (the sets of con-
figurations, ordered by inclusion). In fact, we will often reason on event structures via
their domains of configurations; likewise we shall build maps of event structures via
their action on configurations – we call the lemma below the “mapification” lemma,
letting us build maps of event structures from functions on configurations:

**Lemma 6.1.11.** Consider $f : \mathcal{C}(E) \to \mathcal{C}(F)$ preserving unions and cardinality.
Then, there is a unique map of es $\hat{f} : E \to F$ s.t. for all $x \in \mathcal{C}(E)$, $\hat{f}(x) = f(x)$.

*Proof. Existence.* As *f* preserves unions it is monotone. As it preserves cardinality, it preserves *Ø* and *⊂*. The key point is that it preserves *covering squares*:

$$
\begin{array}{ccc}
x & \stackrel{a}{\subset} & y \\
b & \underset{u}{\searrow} & \underset{a}{\stackrel{b'}{\searrow}} b \\
u & \stackrel{a}{\subset} & v
\end{array}
$$

for $a \neq b$. Indeed as $f$ preserves $\subset$, $f(x) \stackrel{b'}{\subset} f(y)$ and $f(x) \stackrel{a'}{\subset} f(u)$. But also $f(v) = f(y \cup u) = f(y) \cup f(u)$ since $f$ preserves unions, thus $f(v) = f(x) \cup \{a', b'\}$. Hence,

$$
\begin{array}{ccc}
f(x) & \stackrel{a'}{\subset} & f(y) \\
b' & \underset{u}{\searrow} & \underset{a'}{\stackrel{b'}{\searrow}} b' \\
f(u) & \stackrel{a'}{\subset} & f(v)
\end{array}
$$

Now, we are in position to define $\hat{f}$. Given $e \in E$, write

$[e]_E = \{e' \in E \mid e' <_E e\}$

its set of **strict causal dependencies**, which is automatically a configuration. Of course,

$[e]_E \stackrel{e}{\subset} [e]_E$

so that $f[e]_E \stackrel{e'}{\subset} f[e]_E$ for some $e' \in F$ – set $\hat{f}(e) = e'$. Now, for any $x \stackrel{e}{\subset} y$, we have

$$
\begin{array}{ccc}
[e]_E & \stackrel{e_1}{\subset} & x_1 \\
e & \underset{[e]_E}{\searrow} & \underset{e_1}{\stackrel{e_2}{\searrow}} x_2 \\
      & \underset{[e]_E}{\searrow} & \underset{e_2}{\stackrel{e_3}{\searrow}} x_3 \\
      & \underset{[e]_E}{\searrow} & \underset{e_3}{\stackrel{e_4}{\searrow}} x_4 \\
      & \underset{[e]_E}{\searrow} & \underset{e_4}{\stackrel{e_5}{\searrow}} x_5 \\
      & \underset{[e]_E}{\searrow} & \underset{e_5}{\stackrel{e_6}{\searrow}} x_6 \\
      & \underset{[e]_E}{\searrow} & \underset{e_6}{\stackrel{e_7}{\searrow}} x_7 \\
      & \underset{[e]_E}{\searrow} & \underset{e_7}{\stackrel{e_8}{\searrow}} x_8 \\
      & \underset{[e]_E}{\searrow} & \underset{e_8}{\stackrel{e_9}{\searrow}} x_9 \\
      & \underset{[e]_E}{\searrow} & \underset{e_9}{\stackrel{e_{10}}{\searrow}} x_{10}
\end{array}
$$
a tiling of covering squares, which are all preserved by $f$, implying $f x \subsetneq f y$. But now, for any $x \in \mathscr{C}(E)$, one may reach it in $\mathscr{C}(E)$ adding events one by one, i.e. there is

$$ \emptyset = x_0 \stackrel{e_1}{\subset} x_1 \stackrel{e_2}{\subset} \dots \stackrel{e_n}{\subset} x_n = x $$

a **covering chain** in $E$ obtained as any linearization of $x$ according to $\leq_E$. But then

$$ \emptyset = f(x_0) \stackrel{\hat{f}(e_1)}{\subset} f(x_1) \stackrel{\hat{f}(e_2)}{\subset} \dots \stackrel{\hat{f}(e_n)}{\subset} f(x_n) = f(x) $$

from the observation above. But this means that $f(x) = \hat{f}(x)$, the latter defined by the direct image. It immediately follows that $\hat{f}$ is a map of event structures: as it coincides with $f$ of configuration it must preserve configurations, and a failure of local injectivity would immediately contradict the fact that $f$ preserves cardinality.

*Uniqueness.* For $h : E \to F$ s.t. $h(x) = f(x)$ for all $x \in \mathscr{C}(E)$, then if $e \in E$,

$$ f([e]_E) \stackrel{h(e)}{\subset} f([e]_E) $$

so that $h(e) = \hat{f}(e)$ as required, concluding the proof. $\square$

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

Of course, reciprocally, if $f : E \to F$ is a map of event structures then $f : \mathscr{C}(E) \to \mathscr{C}(F)$ must preserve cardinality and unions as it is defined as a direct image. It follows that to test equality of maps of es, it suffices to evaluate them on configurations:

**Lemma 6.1.12.** Consider $f, g : E \to F$ maps of event structures.

If for all $x \in \mathscr{C}(E)$ we have $f(x) = g(x)$, then $f = g$.

*Proof.* Obvious by the *uniqueness* clause of Lemma 6.1.11. $\square$

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

Another particularly useful consequence of the mapification lemma is:

**Proposition 6.1.13.** Consider $E, F$ two es, and $f : \mathscr{C}(E) \cong \mathscr{C}(F)$ an order-iso.

Then, there is a unique $\hat{f} : E \cong F$ an iso in ES s.t. for all $x \in \mathscr{C}(E)$, $\hat{f}(x) = f(x)$.

*Proof.* Firstly, $f$ preserves unions as it is an order-isomorphisms and unions are least upper bounds in $\mathscr{C}(E)$. Secondly, as $f$ is a bijection preserving and reflecting inclusion, it must preserve $\subsetneq$ and thus preserves cardinality. Hence, by Lemma 6.1.11 there is $\hat{f} : E \to F$ a map of event structures such that for all $x \in \mathscr{C}(E)$, $\hat{f}(x) = f(x)$. The same argument applies to $f^{-1}$, yielding an inverse to $f$ by Lemma 6.1.12. $\square$

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

Paired with Lemma 6.1.10, we see that given two event structures $E$ and $F$, an order-iso between the domains of configurations $\mathscr{C}(E)$ and $\mathscr{C}(F)$ induces a concrete renaming between $E$ and $F$, a bijection between events preserving and reflecting all structure. In the future, this will provide our main tool to establish isomorphisms between event structures: by exhibiting an order-isomorphism between the domains of configurations.
**Parallel composition.** Next we introduce the *parallel composition* of event structures, an operation which shall play a central role throughout the development.

**Definition 6.1.14.** Consider $E_1$ and $E_2$ two event structures.

Their simple parallel composition, written $E_1 \parallel E_2$, has components:

$$
\begin{array}{ll}
\text{events:} & |E_1 \parallel E_2| = |E_1| + |E_2|, \\
\text{causality:} & (i, e) \le_{E_1 \parallel E_2} (j, e') \iff i = j \ \& \ e \le_{E_i} e', \\
\text{conflict:} & (i, e) \#_{E_1 \parallel E_2} (j, e') \iff i = j \ \& \ e \ #_{E_i} e'.
\end{array}
$$

This simply puts the two event structures side by side, with no interaction. We shall also apply this construction to configurations: if $x_1 \in \mathscr{C}(E_1)$ and $x_2 \in \mathscr{C}(E_2)$, then $x_1 \parallel x_2 \in \mathscr{C}(E_1 \parallel E_2)$ is defined as the same tagged disjoint union as above, i.e. $x_1 \parallel x_2 = x_1 + x_2$. Moreover, all configurations on $E_1 \parallel E_2$ have this form:

**Lemma 6.1.15.** Consider $E_1$ and $E_2$ two event structures. Then, we have

$$(- \parallel -) : \mathscr{C}(E_1) \times \mathscr{C}(E_2) \cong \mathscr{C}(E_1 \parallel E_2)$$

an order-isomorphism, with the order on $\mathscr{C}(E_1) \times \mathscr{C}(E_2)$ set as the product order.

*Proof.* Straightforward. $\square$

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

Along this isomorphism, all configurations of $E_1 \parallel E_2$ are uniquely written as pairs – accordingly, we shall often write $x_1 \parallel x_2 \in \mathscr{C}(E_1 \parallel E_2)$ for arbitrary configurations on a parallel composition. Note that up to isomorphism, $E_1 \parallel E_2$ is the *unique* event structure whose domain of configurations is order-isomorphic to $\mathscr{C}(E_1) \times \mathscr{C}(E_2)$ – this immediately follows from Lemma 6.1.15 and Proposition 6.1.13.

**Basic properties of strategies.** To put our preliminaries into play, we mention a few facts on strategies. The proofs are relatively elementary with the ingredients introduced so far. We omit them, but invite the reader to work them out as exercises.

Recall that if $\sigma : A$ is a prestrategy on game $A$, then events of $\sigma$ inherit a polarity from $A$ via $\text{pol}_{\sigma}(s) = \text{pol}_{A}(\partial_{\sigma}(s))$. Our first lemma states two properties of strategies in the particular case where the game $A$ is forestial and alternating (which is almost always the case when interpreting types of programming languages).

**Lemma 6.1.16.** Consider a game $A$ forestial and alternating as in Definition 3.1.3.

Then, we have the following properties:

(1) $\sigma$ is alternating: if $s_1 \to_{\sigma} s_2$, then $\text{pol}_{\sigma}(s_1) \neq \text{pol}_{\sigma}(s_2)$.

(2) consider $s_1, s_2 \in x \in \mathscr{C}(\sigma)$ such that $\text{pol}_{\sigma}(s_1) = +$ or $\text{pol}_{\sigma}(s_2) = -$. Then $s_1 \to_{\sigma} s_2$ iff $\partial_{\sigma}s_1 \to_A \partial_{\sigma}s_2$.

Thus for such games, the causal structure of strategies is very much constrained: it is alternating, and only immediate causal links $a_1 \to_A a_2^+$ in the game may be postponed by the strategy. In general and even without alternation, a strategy may only introduce new immediate conflicts (with respect to the game) between positive events:
<figure><img src="image_69.png" /><figcaption>Figure 6.1: Example of an interaction and composition</figcaption></figure>

**Lemma 6.1.17.** Consider A a game, and $\sigma : A$ a strategy.

If $s_1 \sim_{\sigma} s_2$ with $\text{pol}_{\sigma}(s_1) = -$ or $\text{pol}_{\sigma}(s_2) = -$, then $\partial_{\sigma}(s_1) \sim_A \partial_{\sigma}(s_2)$ as well.

Now, we move to the composition of (pre)strategies.

## 6.2 Composition of Prestrategies

Before we can phrase composition, we must define strategies between games. As in sequential games, a strategy from a game A to a game B is a strategy that plays on A and B in parallel, except that the polarities in A are reversed.

**Strategies between games.** If A is a game, its dual $A^{\perp}$ has the same components as A, except for $\text{pol}_{A^{\perp}} = -\text{pol}_{A}$. The simple parallel composition of Definition 6.1.14 extends to games with $\text{pol}_{A^{\parallel}B}(1, a) = \text{pol}_{A}(a)$ and $\text{pol}_{A^{\parallel}B}(2, b) = \text{pol}_{B}(b)$. Finally, the hom-game $A \vdash B$ is defined as $A^{\perp} \parallel B$ by Lemma 6.1.15 we have an order-iso

$$(- \vdash -): \mathcal{C}(A) \times \mathcal{C}(B) \cong \mathcal{C}(A \vdash B),$$

and we often write configurations of $A \vdash B$ as $x_A \vdash x_B$ for $x_A \in \mathcal{C}(A)$ and $x_B \in \mathcal{C}(B)$.

Now if A and B are games, a **strategy from A to B** is simply defined as a strategy on $A \vdash B$ – the same definition applies to prestrategies.

**Towards composition.** Now, consider two strategies $\sigma : A \vdash B$ and $\tau : B \vdash C$ that we wish to compose, forming a composite strategy $\tau \odot \sigma : A \vdash C$.

Intuitively, the computation of $\tau \odot \sigma$ proceeds in two steps. First, we form the interaction $\tau \oplus \sigma$; an event structure displayed to $A \parallel B \parallel C$. The interaction has three kinds of events: those displayed to A are directly imported from $\sigma$, those displayed to C come from $\tau$, while those in B are thought of synchronizations between events of $\sigma$ and events of $\tau$ whose display on B match. The causality of $\tau \oplus \sigma$ is obtained as (the transitive closure) of the causal dependencies imposed by $\sigma$ and by $\tau$. Figure 6.1
displays the interaction of two strategies<fnref n="3" />, and again the conflict is that imported from the two strategies. In Figure 6.1 on the right hand side, the synchronized events are grayed out while those in the outer interface remain in black – those are called *visible*. The composition $\tau \odot \sigma$ is obtained from $\tau \otimes \sigma$ by keeping the visible events only.

This intuition is quite natural, but rather hard to capture formally in a way that is both mathematically rigorous and a tractable basis for further developments – much more so than the composition of sequential strategies as in Part I, which is already non-trivial. And while our forthcoming development of composition will indeed follow the route above, it has been crucial in working with concurrent games that the composition of strategies may be characterized almost relationally, via the proposition:

**Proposition 6.2.1.** Consider A, B, C games, and $\sigma : A \vdash B$ and $\tau : B \vdash C$ strategies. Then there is a strategy $\tau \odot \sigma : A \vdash C$, unique up to iso, s.t. there are order-isos:

$$(- \odot -) : \{(x^{\tau}, x^{\sigma}) \in \mathcal{C}^{+}(\tau) \times \mathcal{C}^{+}(\sigma) \mid \text{causally compatible}\} \simeq \mathcal{C}^{+}(\tau \odot \sigma)$$

such that for $x^{\sigma} \in \mathcal{C}^{+}(\sigma)$ and $x^{\tau} \in \mathcal{C}^{+}(\tau)$ causally compatible,

$$\partial_{\tau \odot \sigma}(x^{\tau} \odot x^{\sigma}) = x_{A}^{\sigma} \vdash x_{C}^{\tau}$$

where we write $\partial_{\sigma}x^{\sigma} = x_{A}^{\sigma} \vdash x_{B}^{\sigma}$ and $\partial_{\tau}x^{\tau} = x_{B}^{\tau} \vdash x_{C}^{\tau}$.

Here, $\mathcal{C}^{+}(-)$ denotes the restriction of configurations to those that are +-covered, i.e. whose maximal events are positive – without trailing Opponent moves. Likewise, *causally compatible* refers to a notion that we shall introduce soon: intuitively, $x^{\sigma} \in \mathcal{C}(\sigma)$ and $x^{\tau} \in \mathcal{C}(\tau)$ are causally compatible if they reach the same state in B (i.e. $x_{B}^{\sigma} = x_{B}^{\tau}$), and their synchronization induces no deadlocks. These two notions will be covered in depth soon, but the message for now is that for most purposes, we can ignore the concrete definition of $\sigma$ and $\tau$ and treat its (+-covered) configurations simply as certain pairs of (+-covered) configurations of $\sigma$ and $\tau$. In addition, this completely captures the composition of $\sigma$ and $\tau$ – there is one strategy (up to iso) whose +-covered configurations are such causally compatible pairs, and it is $\tau \odot \sigma$.

Although noticed somewhat late (say around 2020), this proposition has become central in recent developments in concurrent games, as it lets us reason on the composition of strategies while leaving encapsulated the rather elaborate concrete definition. For most purposes, this is all you need to know about composition!

However, this still leaves us with the task of proving it, and thus to construct the composition concretely – first the interaction, and then its hiding. In the present section we focus on prestrategies, while Section 6.3 contains the extension to strategies.

## 6.2.1 Interaction of prestrategies

The next goal is to define interactions of prestrategies. But before that, we define formally the notion of causal compatibility appearing in Proposition 6.2.1.

<footnote n="3">³The game B $\to$ U is defined only in Section 7.1.4, and likewise for other forthcoming examples; hopefully this is not an obstacle to understanding. Though do note that in such examples, the game can be read from the diagram by only keeping dotted lines and ignoring immediate causal links $\to$.</footnote>
<figure><img src="image_70.png" /><figcaption>Figure 6.2: Matching, secured</figcaption></figure>

<caption>Figure 6.3: Matching, non-secured</caption>

**Causally compatible pairs.** Let us fix $\sigma : A \vdash B$ and $\tau : B \vdash C$ prestrategies. For configurations $x^\sigma \in \mathscr{C}(\sigma)$, $x^\tau \in \mathscr{C}(\tau)$, as a convention we write their display as

$$ \partial_{\sigma}(x^{\sigma}) = x_{A}^{\sigma} \parallel x_{B}^{\sigma} \in \mathscr{C}(A \vdash B), \qquad \partial_{\tau}(x^{\tau}) = x_{B}^{\tau} \parallel x_{C}^{\tau} \in \mathscr{C}(B \vdash C), $$

this convention will be used silently from now on.

First, we capture when $x^\sigma \in \mathscr{C}(\sigma)$ and $x^\tau \in \mathscr{C}(\tau)$ may successfully synchronise:

**Definition 6.2.2.** Two configurations $x^\sigma \in \mathscr{C}(\sigma)$ and $x^\tau \in \mathscr{C}(\tau)$ are *causally compatible* if (1) they are matching: $x_B^\sigma = x_B^\tau = x_B$; and (2) if the composite bijection

$$ \varphi[x^{\sigma}, x^{\tau}] : \quad x^{\sigma} \parallel x_{C}^{\tau} \stackrel{\partial_{\sigma} \parallel x_{C}^{\tau}}{\cong} x_{A}^{\sigma} \parallel x_{B} \parallel x_{C}^{\tau} \stackrel{x_{A}^{\sigma} \parallel \partial_{\tau}^{-1}}{\cong} x_{A}^{\sigma} \parallel x^{\tau}, $$

using local injectivity of $\partial_\sigma$ and $\partial_\tau$, is *secured*, in the sense that the relation

$$ (m, n) \triangleleft (m', n') \quad \Leftrightarrow \quad m <_{\sigma \parallel C} m' \lor n <_{A \parallel \tau} n', $$

defined on (the graph of) $\varphi[x^\sigma, x^\tau]$ from the causal constraints of $\sigma$ and $\tau$, is acyclic.

Two matching $x^\sigma \in \mathscr{C}(\sigma)$, $x^\tau \in \mathscr{C}(\tau)$ agree on the state reached in $B$; and this induces a synchronization between the events matching in $B$. But this is not enough to capture a sensible notion of execution: some matching pairs might not be reachable, in the sense that $\sigma$ and $\tau$ impose incompatible constraints as to the order in which the state should be reached. To illustrate this we show in Figures 6.2 and 6.3 two attempted synchronizations between configurations of the strategy on the left hand side of Figure 7.6 and that for the identity $\lambda x^U$. $x$. In both cases, the configurations are matching. In Figure 6.2, the synchronization is successful and yields a causally compatible pair. However, in Figure 6.3 the induced bijection is not *secured*: the two strategies impose opposite constraints as to the order in which the two ✓ moves are to be played.

This disambiguates the statement of Proposition 6.2.1 – we want an *event structure* $\tau \odot \sigma$ whose (+-covered) configurations correspond to (+-covered) causally compatible pairs. Its construction involves several steps, starting with the *interaction*.

**Interactions.** Given $\sigma : A \vdash B$ and $\tau : B \vdash C$ we mean to construct their interaction $\tau \oplus \sigma$. An *interaction* is not quite a strategy, because it involves events in $B$ that have no clear polarity. Accordingly, it is convenient to define a variation:
**Definition 6.2.3.** An interaction on A, B, C is an event structure $\mu = (|\mu|, \leq_{\mu}, \#_{\mu})$ with

$$ \partial : |\mu| \rightarrow |A \parallel B \parallel C| $$

a display map subject to the following conditions:

rule-abiding: for all $x \in \mathcal{C}(\mu)$, $\partial(x) \in \mathcal{C}(A \parallel B \parallel C)$,

locally injective: for all $s_1, s_2 \in x \in \mathcal{C}(\mu)$, if $\partial(s_1) = \partial(s_2)$ then $s_1 = s_2$.

i.e. $\partial : \mu \rightarrow A \parallel B \parallel C$ is a map of event structures.

In other words an interaction on A, B, C is a prestrategy on $A \parallel B \parallel C$, but it is conceptually clearer to keep the notions separate. Now we must define the interaction, written $\tau \otimes \sigma$, of $\sigma$ and $\tau$; but what should be its *events*? Intuitively, each event of $\tau \otimes \sigma$ arises as the synchronization of an event in $\sigma \parallel C$ and one in $A \parallel \tau$ – note the padding out so that both $\sigma \parallel C$ and $A \parallel \tau$ cover $A \parallel B \parallel C$.

But it is not that simple, as can be observed in Figure 6.1, showing an interaction $\tau \otimes \sigma$ of $\sigma : B \to U$ and $\tau : B \to U \vdash N$. The two final events $0^+$ of $\tau \otimes \sigma$ are two unsynchronized versions of the same event in $\tau$. Yet they are different: they have different causal histories, following the earlier non-deterministic choice in $\tau$. This has to do with an important property of the model we already mentioned: it retains the non-deterministic branching point – any event carries its entire causal history.

A pair of synchronized events with a causal history is a *prime secured bijection*:

**Prime secured bijections.** If $x^{\sigma} \in \mathcal{C}(\sigma)$ and $x^{\tau} \in \mathcal{C}(\tau)$ are causally compatible, from Definition 6.2.2 we know that the relation on the graph of $\varphi[x^{\sigma}, x^{\tau}]$ defined as

$$ (m, n) \triangleleft (m', n') \quad \Leftrightarrow \quad m <_{\sigma \parallel C} m' \quad \lor \quad n <_{A \parallel \tau} n', $$

is acyclic, so its reflexive transitive closure yields a partial order $\leq_{\varphi[x^{\sigma}, x^{\tau}]}$. We define:

**Definition 6.2.4.** A *secured bijection* between $\sigma : A \vdash B$ and $\tau : B \vdash C$ is any partial order $\varphi[x^{\sigma}, x^{\tau}]$, for $x^{\sigma} \in \mathcal{C}(\sigma)$ and $x^{\tau} \in \mathcal{C}(\tau)$ causally compatible.

We write $\mathcal{B}(\sigma, \tau)$ for the set of secured bijections between $\sigma$ and $\tau$.

We shall be particularly interested in those secured bijections with a top element:

**Definition 6.2.5.** We say $\varphi \in \mathcal{B}(\sigma, \tau)$ is *prime* if $\leq_{\varphi}$ has a top $\text{top}(\varphi) = (m, n)$.

We write $\mathcal{B}^{\top}(\sigma, \tau)$ for the set of prime secured bijections between $\sigma$ and $\tau$.

So we regard $\varphi \in \mathcal{B}^{\top}(\sigma, \tau)$ with $\text{top}(\varphi) = (m, n)$ as the synchronized pair $(m, n)$ together with a causal explanation for that synchronization. Those will provide the *events* of the interaction. To proceed, we will need the lemma:

**Lemma 6.2.6.** Consider $x^{\sigma}, y^{\sigma} \in \mathcal{C}(\sigma), x^{\tau}, y^{\tau} \in \mathcal{C}(\tau)$. Then, we have:

(1) If $x^{\sigma}, x^{\tau}$ caus. comp., $y^{\sigma}, y^{\tau}$ caus. comp., $x^{\sigma} \cup y^{\sigma} \in \mathcal{C}(\sigma)$ and $x^{\tau} \cup y^{\tau} \in \mathcal{C}(\tau)$, then $x^{\sigma} \cup y^{\sigma}$ and $x^{\tau} \cup y^{\tau}$ are causally compatible.

(2) If $x^{\sigma} \cup y^{\sigma} \in \mathcal{C}(\sigma)$ and $x^{\tau} \cup y^{\tau} \in \mathcal{C}(\tau)$ are causally compatible, if $x^{\sigma}, x^{\tau}$ matching and $y^{\sigma}, y^{\tau}$ matching, then they are causally compatible,

and in both cases, we have $\varphi[x^{\sigma} \cup y^{\sigma}, x^{\tau} \cup y^{\tau}] = \varphi[x^{\sigma}, x^{\tau}] \cup \varphi[y^{\sigma}, y^{\tau}]$.
*Proof.* Straightforward by local injectivity of $\partial_{\sigma}$ and $\partial_{\tau}$.

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

We are now in position to form an event structure:

**Proposition 6.2.7.** *The tuple $(|\tau \otimes \sigma|, \leq_{\tau \otimes \sigma}, \#_{\tau \otimes \sigma})$ defined with*

events: $|\tau \otimes \sigma| = \{\varphi[x^{\sigma}, x^{\tau}] | \text{prime, for } x^{\sigma}, x^{\tau} \text{ causally compatible}\}$

causality: $\phi \leq_{\tau \otimes \sigma} \psi \Leftrightarrow \phi \subseteq \psi$

conflict: $\neg(\phi \#_{\tau \otimes \sigma} \psi) \Leftrightarrow \exists x^{\sigma}, x^{\tau} \text{ causally compatible, } \phi, \psi \subseteq \varphi[x^{\sigma}, x^{\tau}]$.

forms an event structure. Moreover, there are monotone functions

$$ \chi_{\sigma, \tau} : \mathcal{C}(\tau \otimes \sigma) \rightarrow \mathcal{B}(\sigma, \tau) \\ x \mapsto \bigcup x $$

$$ \bar{\chi}_{\sigma, \tau} : \mathcal{B}(\sigma, \tau) \rightarrow \mathcal{C}(\tau \otimes \sigma) \\ \varphi \mapsto \{\psi \in \mathcal{B}^{\top}(\sigma, \tau) | \psi \subseteq \varphi\} $$

forming an order-isomorphism, with both sets ordered by inclusion.

*Proof.* The conditions for an event structure are easily checked. It is immediate that $\bar{\chi}_{\sigma, \tau}$ is well-formed, for $\chi_{\sigma, \tau}$ it follows from Lemma 6.2.6; both maps are monotone with respect to inclusion. Next we observe that for all $\varphi \in \mathcal{B}(\sigma, \tau)$, we have

$$ \varphi = \bigcup \{\psi \in \mathcal{B}^{\top}(\sigma, \tau) | \psi \subseteq \varphi\}; $$

indeed if $(m, n) \in \varphi$ we set $\psi = [(m, n)]_{\varphi}$ the set of all pairs $(m', n') \in \varphi$ such that $(m', n') \leq_{\varphi} (m, n)$ (recall from above Definition 6.2.4 that causal compatibility endows the graph of any secured bijection with a partial order); by construction, $\psi \in \mathcal{B}^{\top}(\sigma, \tau)$ and $\psi \subseteq \varphi$, hence $(m, n) \in \bigcup \{\psi \in \mathcal{B}^{\top}(\sigma, \tau) | \psi \subseteq \varphi\}$ – the other inclusion is direct. Altogether, this shows that $\chi_{\sigma, \tau} \circ \bar{\chi}_{\sigma, \tau} = \varphi$ for all $\varphi \in \mathcal{B}(\sigma, \tau)$ a secured bijection.

Now consider $X \in \mathcal{C}(\tau \otimes \sigma)$ along with $\varphi[x^{\sigma}, x^{\tau}] \in \bar{\chi}_{\sigma, \tau} \circ \chi_{\sigma, \tau} X$, and take $(m, n) = \text{top}(\varphi[x^{\sigma}, x^{\tau}])$. By definition, $(m, n) \in \bigcup X$, but this means that there is $\psi \in X$ such that $(m, n) \in \psi$. But then it follows from local injectivity that $\varphi[x^{\sigma}, x^{\tau}] \subseteq \psi$, hence $\varphi[x^{\sigma}, x^{\tau}] \in X$ as $X$ is down-closed. The other inclusion is straightforward. $\square$

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

We have now constructed an event structure with configurations order-isomorphic to the secured bijections between $\sigma$ and $\tau$. But furthermore:

**Proposition 6.2.8.** *There is an order-isomorphism*

$$ (- \otimes -) : \{(x^{\sigma}, x^{\tau}) \in \mathcal{C}(\sigma) \times \mathcal{C}(\tau) | \text{causally compatible} \} \cong \mathcal{C}(\tau \otimes \sigma), $$

with causally compatible pairs ordered by pairwise inclusion.

*Proof.* By definition, $\mathcal{B}(\sigma, \tau)$ is in order-isomorphism with the set of causally compatible pairs $(x^{\sigma}, x^{\tau})$. We conclude by composition with that of Proposition 6.2.7. $\square$

<figure><img src="image_73.png" /></figure>
This is starting to look like Proposition 6.2.1. In the sequel, we will almost always reason on $\mathscr{C}(\tau \oplus \sigma)$ via this correspondence, and routinely write any configuration $x \in \mathscr{C}(\tau \oplus \sigma)$ as $x^\tau \oplus x^\sigma \in \mathscr{C}(\tau \oplus \sigma)$, without mentioning the use of this proposition.

In passing, let us mention a few lemmas. Firstly, using the mapification lemma will require us to have information on the cardinal of configurations of the interaction:

**Lemma 6.2.9.** Consider $x^\tau \oplus x^\sigma \in \mathscr{C}(\tau \oplus \sigma)$.

Then, $\mathrm{card}(x^\tau \oplus x^\sigma) = \mathrm{card}(x_A^\sigma) + \mathrm{card}(x_B^\sigma) + \mathrm{card}(x_C^\tau)$.

*Proof.* Straightforward from the Propositions 6.2.7 and 6.2.8. $\square$

Similarly, we need compatibility of configurations of the interaction with unions:

**Lemma 6.2.10.** Consider $x^\sigma, y^\sigma \in \mathscr{C}(\sigma)$ and $x^\tau, y^\tau \in \mathscr{C}(\tau)$ satisfying either of the conditions of Lemma 6.2.6. Then, we have the equality:

$$(x^{\tau} \cup y^{\tau}) \oplus (x^{\sigma} \cup y^{\sigma}) = (x^{\tau} \oplus x^{\sigma}) \cup (y^{\tau} \oplus y^{\sigma}).$$

*Proof.* By Lemma 6.2.6, across the order-isomorphism of Proposition 6.2.7. $\square$

**The interaction pullback.** As an important aside, we have:

**Lemma 6.2.11.** There are maps of event structures $\Pi_\sigma$ and $\Pi_\tau$ making the diagram

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

a pullback in the category of event structures and their maps. Moreover, for any $x^\tau \oplus x^\sigma \in \mathscr{C}(\tau \oplus \sigma)$, we have $\Pi_\sigma (x^\tau \oplus x^\sigma) = x^\sigma \parallel x_C^\tau$ and $\Pi_\tau (x^\tau \oplus x^\sigma) = x_A^\sigma \parallel x^\tau$.

*Proof.* We first define the projection maps, as

$$\Pi_\sigma : \tau \oplus \sigma \rightarrow \sigma \parallel C \\ \phi \mapsto \pi_1(\mathrm{top}(\phi))$$

$$\Pi_\tau : \tau \oplus \sigma \rightarrow A \parallel \tau \\ \phi \mapsto \pi_2(\mathrm{top}(\phi)),$$

and check the two conditions for these to be maps of event structures. For rule-abiding, consider $x \in \mathscr{C}(\tau \oplus \sigma)$. By Proposition 6.2.7, $\cup x \in \mathscr{B}(\sigma, \tau)$. But furthermore,

$$\cup x : \Pi_{\sigma} x \cong \Pi_{\tau} x. \qquad (6.5)$$

Indeed, if $m \in \Pi_\sigma x$ there is some $\phi \in x$ such that $m = \pi_1(\mathrm{top}(\phi))$, but then clearly $m \in \mathrm{dom}(\cup x)$. Reciprocally, if $m \in \mathrm{dom}(\cup x)$, this means there is $\phi \in x$ such that $(m, n) \in \phi$ for some $n$. But then, considering the set defined as

$$[(m, n)]_{\phi} = \{(m', n') \in \phi \mid (m', n') \leq_{\phi} (m, n)\},$$
one can check that $[(m, n)]_\phi \in \mathcal{B}^\top(\sigma, \tau)$, and $[(m, n)]_\phi \subseteq \phi$ by construction, so $[(m, n)]_\phi \in x$ as $x$ is down-closed. But so, $m = \Pi_\sigma[(m, n)]_\phi$ so $m \in \Pi_\sigma x$ as required. It also follows that $\Pi_\sigma x \in \mathcal{C}(\sigma \parallel C)$, and using (6.5) and Proposition 6.2.7,

$$ \begin{align*} \Pi_\sigma (x^\tau \oplus x^\sigma) &= \Pi_\sigma (\bar{\chi}_{\sigma, \tau} \varphi[x^\sigma, x^\tau]) \\ &= \mathrm{dom}(\cup (\bar{\chi}_{\sigma, \tau} \varphi[x^\sigma, x^\tau])) \\ &= \mathrm{dom}(\varphi[x^\sigma, x^\tau]) \end{align*} $$

which is $x^\sigma \parallel x_C^\tau$ – and likewise, $\Pi_\tau(x^\tau \oplus x^\sigma) = x_A^\sigma \parallel x^\tau \in \mathcal{C}(A \parallel \tau)$. For local injectivity, assume that $\varphi, \psi \in x$ are such that $\Pi_\sigma \varphi = \Pi_\sigma \psi$, write it $m$. But $\varphi, \psi \subseteq \cup x \in \mathcal{B}(\sigma, \tau)$, and there is a unique $n$ such that $(m, n) \in \cup x$ as it is a bijection. But we must have $\varphi = [(m, n)]_{\cup x}$ and likewise for $\psi$, so $\varphi = \psi$.

That the diagram commutes and satisfies the universal property of the diagram is routine, using the above along with Lemma 6.1.11 (the conditions for mapification come from Lemmas 6.2.9 and 6.2.10) and Proposition 6.2.7. $\square$

In fact, the category **ES** of event structures and their maps has all pullbacks. The construction of $\tau \oplus \sigma$ given here closely follows the construction of pullbacks in **ES**, which in turn is a restriction of the usual synchronizing product of event structures. So this is old technology here, essentially the same used by Winskel in the early 80s to give semantics to parallel composition of CCS processes [Winskel, 1982].

In the sequel we shall not exploit the universal property of this pullback, but we will often refer to its projections: after this section we shall often treat the interaction construction as a black box. The *projections* will be our main device to read back an event $p \in \tau \oplus \sigma$ as a synchronization of $\Pi_\sigma p \in \sigma \parallel C$ and $\Pi_\tau p \in A \parallel \tau$.

Finally, we have seen that configurations of the interaction correspond to secured bijections. But the connection is even tighter: both configurations and secured bijections are partially ordered sets, and it will be important for later on to keep in mind that this correspondence is, locally, an order-isomorphism. This is expressed by:

**Lemma 6.2.12.** Consider $x^\sigma \in \mathcal{C}(\sigma)$ and $x^\tau \in \mathcal{C}(\tau)$ causally compatible.
Then, there is an order-isomorphism $v[x^\sigma, x^\tau] : x^\tau \oplus x^\sigma \cong \varphi[x^\sigma, x^\tau]$ such that

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

commutes, in the category of finite sets and bijections. Moreover, this assignment is monotone, in the sense that if $x^\sigma \subseteq y^\sigma$ and $x^\tau \subseteq y^\tau$, then $v[x^\sigma, x^\tau] \subseteq v[y^\sigma, y^\tau]$.

*Proof.* We set the order-isomorphism $v[x^\sigma, x^\tau]$ as follows:

$$ \begin{align*} v[x^\sigma, x^\tau] : x^\tau \oplus x^\sigma &\to \varphi[x^\sigma, x^\tau] \\ \psi &\mapsto \mathrm{top}(\psi), \end{align*} $$

it is a direct that this defines an order-iso, and that this assignment is monotone. $\square$
**The interaction.** At last, this provides us with the ingredients for the interaction.

**Proposition 6.2.13.** *There is an interaction $\tau \otimes \sigma$, unique up to iso, s.t. there is*

$$(- \otimes -) : \{(x^{\tau}, x^{\sigma}) \in \mathscr{C}(\tau) \times \mathscr{C}(\sigma) \mid x^{\sigma}, x^{\tau} \text{ causally compatible}\} \simeq \mathscr{C}(\tau \otimes \sigma)$$

an order-iso s.t. $\partial_{\tau \otimes \sigma}(x^{\tau} \otimes x^{\sigma}) = x_{A}^{\sigma} \parallel x_{B} \parallel x_{C}^{\tau}$ for all $x^{\sigma}, x^{\tau}$ causally compatible.

*Proof. Existence.* The event structure $\tau \otimes \sigma$ is defined in Lemma 6.2.11, with display map $\partial_{\tau \otimes \sigma} : \tau \otimes \sigma \to A \parallel B \parallel C$ defined as either way around the square. The order-iso for configurations comes from Proposition 6.2.8.

*Uniqueness.* Immediate from the order-isos, by Lemma 6.1.12. □

Here, an isomorphism of interactions simply means an isomorphism of event structures commuting with the display maps. The construction of $\tau \otimes \sigma$ is elaborate – there is no going around it; but fortunately, Proposition 6.2.13 packages most of what we need about the interaction, and may often be used as a black box. It is suspiciously close to Proposition 6.2.1, which may be surprising since this is not composition but interaction, without hiding. We shall see that the restriction to +-covered configurations in Proposition 6.2.1 does a lot to span the distance between interaction and composition.

**Structure of causality.** Proposition 6.2.13 gives a neat state-based description of the interaction, putting the focus on configurations. This is sufficient for many purposes, but it is sometimes necessary to reason on individual events of the interaction.

As explained before, any event $p \in \tau \otimes \sigma$ may be regarded as a synchronization between its projections $\Pi_{\sigma}p \in \sigma \parallel C$ and $\Pi_{\tau}p \in A \parallel \tau$, along with a causal history for this synchronization. These projections help us classify every $p \in \tau \otimes \sigma$ into:

(1) $\Pi_{\sigma}(p) = (1, s)$ with $s \in \sigma$, and $\Pi_{\tau}(p) = (1, a)$ with $a \in A$,

(2) $\Pi_{\sigma}(p) = (1, s)$ with $s \in \sigma$, and $\Pi_{\tau}(p) = (2, t)$ with $t \in \tau$,

(3) $\Pi_{\sigma}(p) = (2, c)$ with $c \in C$, and $\Pi_{\tau}(p) = (2, t)$ with $t \in \tau$.

In case (1), the only relevant projection is $\Pi_{\sigma}(p) = (1, s)$ as $\Pi_{\tau}(p) = \partial_{\sigma}(s)$. We write $p_{\sigma} = s$ and $p_{\tau}$ is undefined, and we say that **p occurs in** A. In case (3), the relevant projection is $\Pi_{\tau}(p) = (2, t)$ as $\Pi_{\sigma}(p) = \partial_{\tau}(t)$. We write $p_{\tau} = t$ and $p_{\sigma}$ is undefined, and **p occurs in** C. Finally, in case (2) the two projections $\Pi_{\sigma}(p) = (1, s)$ and $\Pi_{\tau}(p) = (2, t)$ are relevant, but we must have $\partial_{\sigma}(s) = (2, b)$ and $\partial_{\tau}(t) = (1, b)$ for some $b \in B$. We write $p_{\sigma} = s, p_{\tau} = t$, we say that **p occurs in** B. If **p** occurs in A or C we also say that it is **visible**, while if it occurs in B it is **synchronized** or **invisible**.

Immediate causal links between events of $\tau \otimes \sigma$ must originate from $\sigma$ or $\tau$:

**Lemma 6.2.14.** *Consider $p, p' \in \tau \otimes \sigma$, and assume $p \dashrightarrow_{\tau \otimes \sigma} p'$. Then $p_{\sigma} \dashrightarrow_{\sigma} p'_{\sigma}$ or $p_{\tau} \dashrightarrow_{\tau} p'_{\tau}$, where $p_{\sigma}, p_{\tau}$ are defined whenever used.*

*Proof.* Consider $x^{\tau} \otimes x^{\sigma} \in \mathscr{C}(\tau \otimes \sigma)$ such that $p, p' \in x^{\tau} \otimes x^{\sigma}$. Write $\text{top}(p) = (m, n)$ and $\text{top}(p') = (m', n')$. By Lemma 6.2.12, we have an immediate causal link

$$(m, n) \dashrightarrow_{\varphi[x^{\sigma}, x^{\tau}]} (m', n'),$$
<figure><img src="image_76.png" /><figcaption>Figure 6.4: Example of an interaction with polarity information</figcaption></figure>

which easily implies, by definition of $\leq_{\phi[x_{\sigma}, x_{\tau}]}$, that $m \to_{\sigma\parallel C} m'$ or $n \to_{A\parallel\tau} n'$.

If $m \to_{\sigma\parallel C} m'$, then either $m = (1, s)$, $m' = (1, s')$ and $s \to_{\sigma} s'$ with $s = p_{\sigma}$ and $s' = p'_{\sigma}$ defined as required; or, $m = (2, c)$ and $m' = (2, c')$ with $c \to_{C} c'$. In that case, $n = (2, t)$ and $n' = (2, t')$ and $t = p_{\tau}$ and $t' = p'_{\tau}$ defined. Moreover, $c \to_{C} c'$ implies $\partial_{\tau}(t) \to_{B\vdash C} \partial_{\tau}(t')$, so $t <_{\tau} t'$ by Lemma 6.1.8. If this causal link was not immediate, this would directly contradict $(m, n) \to_{\phi[x_{\sigma}, x_{\tau}]} (m', n')$ – so $p_{\tau} \to_{\tau} p'_{\tau}$ as required. $\square$

For $\sigma$ and $\tau$ strategies, we can track down the responsible of a move via a polarity analysis. Events of $\tau \otimes \sigma$ cannot sensibly be assigned a polarity in $\{-, +\}$, as $\sigma$ and $\tau$ disagree on $B$. A more useful polarity is $\text{pol}_{\tau \otimes \sigma} : |\tau \otimes \sigma| \to \{-, \ell, r\}$ set as:

$\text{pol}_{\tau \otimes \sigma}(p) = \ell$ if $p_{\sigma}$ is defined and $\text{pol}_{\sigma}(p_{\sigma}) = +,$

$\text{pol}_{\tau \otimes \sigma}(p) = r$ if $p_{\tau}$ is defined and $\text{pol}_{\tau}(p_{\tau}) = +,$

$\text{pol}_{\tau \otimes \sigma}(p) = -$ otherwise.

We show in Figure 6.4 a version of Figure 6.1 with those polarities. Then:

**Lemma 6.2.15.** If $\sigma : A \vdash B$ and $\tau : B \vdash C$ are strategies and $p \to_{\tau \otimes \sigma} p'$, then

(1) if $\text{pol}_{\tau \otimes \sigma}(p') = \ell$, then $p_{\sigma} \to_{\sigma} p'_{\sigma}$,

(2) if $\text{pol}_{\tau \otimes \sigma}(p') = r$, then $p_{\tau} \to_{\tau} p'_{\tau}$,

(3) if $\text{pol}_{\tau \otimes \sigma}(p') = -$, then $\partial_{\tau \otimes \sigma}(p) \to_{A\parallel B\parallel C} \partial_{\tau \otimes \sigma}(p')$

where again, $p_{\sigma}, p'_{\sigma}, p_{\tau}$ and $p'_{\tau}$ are defined whenever used.

*Proof.* (1) By Lemma 6.2.14, $p_{\sigma}, p'_{\sigma}$ defined and $p_{\sigma} \to_{\sigma} p'_{\sigma}$ and we are done; or $p_{\tau}, p'_{\tau}$ defined and $p_{\tau} \to_{\tau} p'_{\tau}$. Since $\text{pol}_{\tau \otimes \sigma}(p') = \ell$, $\text{pol}_{\tau}(p'_{\tau}) = -$. By *courteous*, $\partial_{\tau}(p_{\tau}) \to_{B\vdash C} \partial_{\tau}(p'_{\tau})$; hence $m$ occurs in $B$ and $\partial_{\sigma}(p_{\sigma}) \to_{A\vdash B} \partial_{\sigma}(p'_{\sigma})$. By Lemma 6.1.8, $p_{\sigma} <_{\sigma} p'_{\sigma}$, and it is direct that the causality must be immediate. (2) is symmetric.

(3) Assume $p'$ occurs in $A$, the other case is symmetric. In that case only $p'_{\sigma}$ is defined, so Lemma 6.2.14 entails that $p_{\sigma}$ is defined and $p_{\sigma} \to_{\sigma} p'_{\sigma}$. But $\text{pol}_{\sigma}(p'_{\sigma}) = -$, so by courtesy $\partial_{\sigma}(p_{\sigma}) \to_{A\vdash B} \partial_{\sigma}(p'_{\sigma})$, from which the conclusion follows. $\square$

Next, we perform the hiding and introduce the *composition* of prestrategies.
## 6.2.2 Composition of prestrategies

**Hiding.** Composition consists simply in removing all synchronized events:

**Definition 6.2.16.** The composition of $\sigma: A \vdash B$ and $\tau: B \vdash C$ comprises:

$$ \begin{align*} |\tau \odot \sigma| &= \{p \in \tau \oplus \sigma \mid p \text{ occurs in } A \text{ or } C\}, \\ p_1 \leq_{\tau \odot \sigma} p_2 &\Leftrightarrow p_1 \leq_{\tau \oplus \sigma} p_2, \\ p_1 \#_{\tau \odot \sigma} p_2 &\Leftrightarrow p_1 \#_{\tau \oplus \sigma} p_2. \end{align*} $$

with display map $\partial_{\tau \odot \sigma}: |\tau \odot \sigma| \to |A \vdash C|$ obtained as restriction of $\partial_{\tau \oplus \sigma}$.

It is straightforward that $\tau \odot \sigma$ is an event structure. In Figure 6.4, the composition simply keeps the events in black. This means that it has two conflicting positive events, both corresponding to $0^+$: the model records the point of non-deterministic branching even when it brings no observable difference.

Though this does not appear in pictures, we insist that events of $\tau \odot \sigma$ are certain events of $\tau \oplus \sigma$. Thus an event of the composition always carries a unique causal explanation: itself, regarded as an event of the interaction $\tau \oplus \sigma$. Accordingly, we set:

**Definition 6.2.17.** Consider $x \in \mathcal{C}(\tau \odot \sigma)$. Its interaction witness is defined as

$$ [x]_{\tau \oplus \sigma} = \{p \in \tau \oplus \sigma \mid \exists p' \in x, p \leq_{\tau \oplus \sigma} p'\} \in \mathcal{C}(\tau \oplus \sigma) $$

its down-closure in $\tau \oplus \sigma$.

This entails – and it shall play a crucial role in the development – that configurations of the composition are in one-to-one correspondence with those configurations of the interaction whose maximal events are visible. From this idea, we get:

**Proposition 6.2.18.** There is an order-isomorphism

$$ (- \odot -) : \{(x^\tau, x^\sigma) \in \mathcal{C}(\tau) \times \mathcal{C}(\sigma) \mid x^\sigma, x^\tau \text{ minimal caus. comp.}\} \simeq \mathcal{C}(\tau \odot \sigma) $$

where $x^\sigma, x^\tau$ minimal means that the maximal elements of $\phi[x^\sigma, x^\tau]$ occur in A or C.

*Proof.* We decompose the order-isomorphism in two steps.

As a first step, we note that the isomorphism of Proposition 6.2.13 refines to:

$$ (- \oplus -) : \{(x^\tau, x^\sigma) \in \mathcal{C}(\tau) \times \mathcal{C}(\sigma) \mid x^\sigma, x^\tau \text{ min. caus. comp.}\} \simeq \mathcal{C}^v(\tau \oplus \sigma) $$

where $\mathcal{C}^v(\tau \oplus \sigma)$ refers to configurations whose maximal events are visible, i.e. occur in A or C – this is clear by Lemma 6.2.12. Next, we have the order-iso formed with:

$$ \begin{array}{ccc} \mathcal{C}^v(\tau \oplus \sigma) & \to & \mathcal{C}(\tau \odot \sigma) \\ x & \mapsto & x \cap V \end{array} $$

$$ \begin{array}{ccc} \mathcal{C}(\tau \odot \sigma) & \to & \mathcal{C}^v(\tau \oplus \sigma) \\ x & \mapsto & [x]_{\tau \oplus \sigma} \end{array} $$

where $V$ denotes visible events – it is straightforward that this defines an order-iso. $\square$
This shows how even through the hiding operation, configurations of the composition can still be regarded as certain pairs of configurations of the compound strategies. We are certainly starting to get close to our target statement of Proposition 6.2.1.

Note that the operation from left to right is well-defined even if $x^\sigma \in \mathscr{C}(\sigma)$ and $x^\tau \in \mathscr{C}(\tau)$ are causally compatible but not minimal causally compatible. In that case we shall still write $x^\tau \odot x^\sigma = (x^\tau \oplus x^\sigma) \cap V \in \mathscr{C}(\tau \odot \sigma)$, even though $x^\sigma$ and $x^\tau$ cannot necessarily be recovered if the interaction has some maximal synchronized events.

The next lemma states a simple property of this construction, useful for reference:

**Lemma 6.2.19.** For $x^\sigma \in \mathscr{C}(\sigma)$ and $x^\tau \in \mathscr{C}(\tau)$ minimal causally compatible, we have

$$x^\tau \odot x^\sigma = (x^\tau \oplus x^\sigma) \cap V$$

$$x^\tau \oplus x^\sigma = [x^\tau \odot x^\sigma]_{\tau \odot \sigma},$$

where $V$ is the set of visible events.

*Proof.* By def. of $x^\tau \odot x^\sigma$ through the order-iso $\mathscr{C}^v(\tau \oplus \sigma) \simeq \mathscr{C}(\tau \odot \sigma)$ above. $\square$

It will also be useful later on that this is compatible with unions:

**Lemma 6.2.20.** Consider $x^\sigma, y^\sigma \in \mathscr{C}(\sigma)$ and $x^\tau, y^\tau \in \mathscr{C}(\tau)$ satisfying either of the conditions of Lemma 6.2.6. Then, we have the equality:

$$(x^\tau \odot x^\sigma) \cup (y^\tau \odot y^\sigma) = (x^\tau \cup y^\tau) \odot (x^\sigma \cup y^\sigma).$$

*Proof.* By Lemma 6.2.10, we have $(x^\tau \cup y^\tau) \oplus (x^\sigma \cup y^\sigma) = (x^\tau \oplus x^\sigma) \cup (y^\tau \oplus y^\sigma)$, thus $(x^\tau \cup y^\tau) \odot (x^\sigma \cup y^\sigma) = (x^\tau \odot x^\sigma) \cup (y^\tau \odot y^\sigma)$ by restricting to visible events. $\square$

Finally, we relate immediate causality in the interaction and composition:

**Lemma 6.2.21.** Consider $p, p' \in \tau \odot \sigma$. If $p \to_{\tau \odot \sigma} p'$, then we have

$$p \to_{\tau \oplus \sigma} q_1 \to_{\tau \oplus \sigma} \dots \to_{\tau \oplus \sigma} q_n \to_{\tau \oplus \sigma} p'$$

for some $q_1, \dots, q_n \in \tau \oplus \sigma$ synchronized.

*Proof.* Straightforward by definition. $\square$

We wrap up with the main proposition for composition of prestrategies:

**Proposition 6.2.22.** Consider $\sigma : A \vdash B$ and $\tau : B \vdash C$ prestrategies.

Then there is a prestrategy $\tau \odot \sigma$, unique up to iso, s.t. there is an order-iso:

$$(- \odot -) : \{(x^\tau, x^\sigma) \in \mathscr{C}(\tau) \times \mathscr{C}(\sigma) | x^\sigma, x^\tau \text{ min. caus. comp.}\} \simeq \mathscr{C}(\tau \odot \sigma)$$

s.t. for all $x^\sigma \in \mathscr{C}(\sigma)$, $x^\tau \in \mathscr{C}(\tau)$ min. caus. comp., $\partial_{\tau \odot \sigma}(x^\tau \odot x^\sigma) = x_A^\sigma \vdash x_C^\tau$.
<table><caption>Figure 6.5: Ternary causal compatibility</caption><tr><td>(∂<sub>σ</sub> || C || D)(m) &lt;sub>σ</sub></td><td>(∂<sub>σ</sub> || C || D)(m') where m &lt;<sub>σ||C||D</sub> m'</td><td>(m, m' ∈ x<sup>σ</sup> || x<sub>C</sub> || x<sub>D</sub>),</td></tr><tr><td>(A || ∂<sub>τ</sub> || D)(m) &lt;sub>τ</sub></td><td>(A || ∂<sub>τ</sub> || D)(m') where m &lt;<sub>A||τ||D</sub> m'</td><td>(m, m' ∈ x<sub>A</sub> || x<sup>τ</sup> || x<sub>D</sub>),</td></tr><tr><td>(A || B || ∂<sub>δ</sub>)(m) &lt;sub>δ</sub></td><td>(A || B || ∂<sub>δ</sub>)(m') where m &lt;<sub>A||B||δ</sub> m'</td><td>(m, m' ∈ x<sub>A</sub> || x<sub>B</sub> || x<sup>δ</sup>),</td></tr></table>

*Proof. Existence.* The event structure, along with the display map on events, are defined in Definition 6.2.16, with order-isomorphism defined in Proposition 6.2.18. We must check that $\partial_{\tau \odot \sigma}$ is a map of event structures. By Proposition 6.2.13, $\partial_{\tau \oplus \sigma}(x^\tau \oplus x^\sigma) = x_A^\sigma \parallel x_B \parallel x_C^\tau$, hence by definition of $\partial_{\tau \odot \sigma}$, $\partial_{\tau \odot \sigma}(x^\tau \odot x^\sigma) = x_A^\sigma \vdash x_C^\tau$. Now as $\partial_{\tau \oplus \sigma}$ is a map of event structures, it induces a bijection between $x^\tau \oplus x^\sigma$ and $x_A^\sigma \parallel x_B \parallel x_C^\tau$, which by definition of $\tau \odot \sigma$ restricts to a bijection between $x^\tau \odot x^\sigma$ and $x_A^\sigma \vdash x_C^\tau$, so

$$\mathrm{card}(x^{\tau} \odot x^{\sigma}) = \mathrm{card}(x_{A}^{\sigma}) + \mathrm{card}(x_{C}^{\tau})$$

ensuring that $\partial_{\tau \odot \sigma}$ preserves cardinal. By Lemma 6.2.20 it follows that it also preserves unions, and hence forms a map of event structures by Lemma 6.1.11.

*Uniqueness* up to strong iso is straightforward by Lemma 6.1.12. $\square$

### 6.2.3 The associator

We have defined the composition of prestrategies; not yet that of strategies, as we have not yet established that composition preserves receptivity and courtesy. Before doing that we shall study *associativity* of composition, as it turns out that it holds independently of the additional conditions for strategies. Thus fix now prestrategies $\sigma : A \vdash B$, $\tau : B \vdash C$ and $\delta : C \vdash D$. We aim to show that composition is associative up to isomorphism, i.e. that there is an isomorphism of prestrategies, called the *associator*:

$$a_{\sigma, \tau, \delta} : (\delta \odot \tau) \odot \sigma \cong \delta \odot (\tau \odot \sigma).$$

Proposition 6.2.22 makes associativity seem almost trivial: as configurations of the composition are identified to certain pairs of configurations, mapping $(\delta \odot \tau) \odot \sigma$ to $\delta \odot (\tau \odot \sigma)$ is only a matter of sending $(x^\delta \odot x^\tau) \odot x^\sigma$ to $x^\delta \odot (x^\tau \odot x^\sigma)$, i.e. by associativity of the set-theoretic cartesian product – as for associativity for the composition of spans. But as Proposition 6.2.22 makes formal, composition of strategies is composition of spans, plus deadlocks, captured by the *causal compatibility* constraint; and we must also prove that causal compatibility is compatible with associativity.

For this, it is cleaner to introduce *causally compatible triples*:

**Definition 6.2.23.** Consider $x^\sigma \in \mathscr{C}(\sigma)$, $x^\tau \in \mathscr{C}(\tau)$ and $x^\delta \in \mathscr{C}(\delta)$. We set conditions:

matching: if $x_B^\sigma = x_B^\tau = x_B$ and $x_C^\tau = x_C^\delta = x_C$,

causally compatible: if they are matching and the relation $\triangleleft = \triangleleft_\sigma \cup \triangleleft_\tau \cup \triangleleft_\delta$ on $x_A \parallel x_B \parallel x_C \parallel x_D$ defined in Figure 6.5, is acyclic.

minimal: if events maximal for $\triangleleft^*$ occur in A or D.
where $\partial_{\sigma}x^{\sigma} = x_{A} \parallel x_{B}^{\sigma}, \partial_{\tau}x^{\tau} = x_{B}^{\tau} \parallel x_{C}^{\tau}$, and $\partial_{\delta}x^{\delta} = x_{C}^{\delta} \parallel x_{D}$.

Crucially, ternary causal compatibility is equivalent to the two skewed versions:

**Lemma 6.2.24.** For $x^{\sigma} \in \mathscr{C}(\sigma)$, $x^{\tau} \in \mathscr{C}(\tau)$, $x^{\delta} \in \mathscr{C}(\delta)$, the following are equivalent:

(1) $x^{\sigma}, x^{\tau}, x^{\delta}$ are minimal causally compatible,

(2) $x^{\sigma}, x^{\tau}$ are min. caus. comp. and $x^{\tau} \odot x^{\sigma}, x^{\delta}$ are min. caus. comp.,

(3) $x^{\tau}, x^{\delta}$ are min. caus. comp. and $x^{\sigma}, x^{\delta} \odot x^{\tau}$ are min. caus. comp.

*Proof.* (1) ⇒ (2). For $x^{\sigma}, x^{\tau}$ causally compatible, a cycle in $\varphi[x^{\sigma}, x^{\tau}]$ routinely corresponds to a cycle in $x_{A} \parallel x_{B} \parallel x_{C}$ for the relation $\angle_{\sigma} \cup \angle_{\tau}$ defined as:

($\partial_{\sigma} \parallel C)(m) \angle_{\sigma} (\partial_{\sigma} \parallel C)(m')$ where $m <_{\sigma \parallel C} m'$ ($m, m' \in x^{\sigma} \parallel x_{C}$),

($A \parallel \partial_{\tau})(m) \angle_{\tau} (A \parallel \partial_{\tau})(m')$ where $m <_{A \parallel \tau} m'$ ($m, m' \in x_{A} \parallel x^{\tau}$)

which immediately transports to a cycle in $\angle$ on $x_{A} \parallel x_{B} \parallel x_{C} \parallel x_{D}$, contradiction. For minimality, consider $m$ maximal in $x_{A} \parallel x_{B} \parallel x_{C}$ for $\angle_{\sigma} \cup \angle_{\tau}$; assume, seeking a contradiction, that it is in $B$. Then this event considered in $x_{A} \parallel x_{B} \parallel x_{C} \parallel x_{D}$, still denoted by $m$ by abuse of notation, cannot be maximal for $\angle$ by minimality. Thus there is $m \angle n$ for $n$ in $x_{A} \parallel x_{B} \parallel x_{C} \parallel x_{D}$. But by construction of $\angle$, $n$ must be in $A, B, C$ and $m (\angle_{\sigma} \cup \angle_{\tau})$ in $x_{A} \parallel x_{B} \parallel x_{C}$, contradiction. Hence, $x^{\sigma}, x^{\tau}$ minimal.

For $x^{\tau} \odot x^{\sigma}, x^{\delta}$ causally compatible, a cycle in $\varphi[x^{\tau} \odot x^{\sigma}, x^{\delta}]$ corresponds to a cycle in $x_{A} \parallel x_{C} \parallel x_{D}$ for the relation $\angle_{\tau} \circ \sigma \cup \angle_{\delta}$ obtained as above. But this immediately gives a cycle in $x_{A} \parallel x_{B} \parallel x_{C} \parallel x_{D}$ for $(\angle_{\sigma} \cup \angle_{\tau})^{*} \cup \angle_{\delta}$, which gives a cycle in $x_{A} \parallel x_{B} \parallel x_{C} \parallel x_{D}$ for $\angle$, contradiction. For minimality, an event $m$ maximal for $\angle_{\sigma, \tau}$ and $\angle_{\delta}$ cannot be in $C$: otherwise there is $n$ in $A, D$ such that $m \angle^{*} n$, but then it is straightforward that $m (\angle_{\sigma, \tau} \cup \angle_{\delta})^{*} n$, contradicting its maximality.

(2) ⇒ (1). Consider a cycle $m_1 \angle \cdots \angle m_k \angle m_1$. If the cycle remains in $A, B, C$, we get a contradiction to $x^{\sigma}, x^{\tau}$ causally compatible. Otherwise, removing all moves in $B$, we get a cycle in $(\angle_{\sigma, \tau} \cup \angle_{\delta})$ hence a contradiction to $x^{\tau} \odot x^{\sigma}, x^{\delta}$ causally compatible. For minimality, consider $m$ maximal for $\angle^{*}$. By minimality of $x^{\sigma}, x^{\tau}$ it is not in $B$, and by minimality of $x^{\tau} \odot x^{\sigma}, x^{\delta}$ it cannot be in $C$; hence it is in $A$ or $D$.

(1) ⇒ (3), (3) ⇒ (1). Symmetric to the two implications above. $\square$

Altogether, this gives us all the ingredients required for the associator:

**Proposition 6.2.25.** Consider $\sigma : A \vdash B, \tau : B \vdash C$ and $\delta : C \vdash D$ prestrategies.

Then there is a unique isomorphism, the *associator*:

$$a_{\sigma, \tau, \delta} : (\delta \odot \tau) \odot \sigma \cong \delta \odot (\tau \odot \sigma),$$

s.t. for all $x^{\sigma}, x^{\tau}, x^{\delta}$ min. caus. comp., $a_{\sigma, \tau, \delta}((x^{\delta} \odot x^{\tau}) \odot x^{\sigma}) = x^{\delta} \odot (x^{\tau} \odot x^{\sigma})$.

*Proof.* The two clauses serve as the definition of the action of $a_{\delta, \tau, \sigma}$ on configurations, via Proposition 6.2.22 and Lemma 6.2.24. Compatibility with display maps is from the description of the display map of composition in Proposition 6.2.22. To lift this to a map, we observe that preservation of cardinal is clear by local injectivity and preservation of display maps, and preservation of unions follows from Lemma 6.2.20. Finally, the same arguments holds for the inverse, therefore forming an isomorphism. $\square$
Composition of prestrategies is associative, but there does not seem to be an identity turning it into a (bi)category – the obvious candidate, the *copycat strategy* that we shall see later on, is only neutral for composition with respect to *strategies*.

## 6.3 Composition of Strategies

Now we focus on *strategies*, i.e. those prestrategies satisfying the additional conditions of Definition 6.1.6. In this section, we aim in particular to prove Proposition 6.2.1.

### 6.3.1 Composition of Strategies

Thus, we now turn to the composition of strategies. Our first objective is to establish that they are indeed stable under composition.

**Proposition 6.3.1.** Consider $\sigma : A \vdash B$ and $\tau : B \vdash C$ strategies.

Then, $\tau \odot \sigma : A \vdash C$ is a strategy.

*Proof.* By Proposition 6.2.22, we have $\tau \odot \sigma : A \vdash C$ a prestrategy.

*Courteous.* Let $p \to_{\tau \odot \sigma} p'$ s.t. $\text{pol}(p) = +$ or $\text{pol}(p') = -$. By Lemma 6.2.21,

$$p \to_{\tau \otimes \sigma} q_1 \to_{\tau \otimes \sigma} \dots \to_{\tau \otimes \sigma} q_n \to_{\tau \otimes \sigma} p'$$

for some $q_1, \dots, q_n \in \tau \otimes \sigma$ synchronized.

We show that in fact $n = 0$ and $p \to_{\tau \otimes \sigma} p'$. If $\text{pol}(p) = +$, then $\text{pol}_{\tau \otimes \sigma}(q_1) \in \{\ell, r\}$ – assume w.l.o.g. that it is $\ell$. Then by Lemma 6.2.15, $p_\sigma, (q_1)_\sigma$ are defined and $p_\sigma \to_\sigma (q_1)_\sigma$. But by courtesy, this entails $\partial_\sigma(p_\sigma) \to_{A \vdash B} \partial_\sigma((q_1)_\sigma)$, impossible for $q_1$ synchronized. Hence $n = 0$, and $p \to_{\tau \otimes \sigma} p'$. If $\text{pol}(p') = -$, then again by Lemma 6.2.15, $\partial_{\tau \otimes \sigma}(q_n) \to_{A \parallel B \parallel C} \partial_{\tau \otimes \sigma}(p')$, contradicting $q_n$ synchronized, so $p \to_{\tau \otimes \sigma} p'$.

Now, by Lemma 6.2.14, $p_\sigma \to_\sigma p'_\sigma$ or $p_\tau \to_\sigma p'_\tau$, say w.l.o.g. the former. But then $\partial_\sigma(p_\sigma) \to_{A \vdash B} \partial_\sigma(p'_\sigma)$, from which $\partial_{\tau \odot \sigma}(p) \to_{A \vdash C} \partial_{\tau \odot \sigma}(p')$ follows.

*Receptive.* Consider $x^\tau \odot x^\sigma \in \mathscr{C}(\tau \odot \sigma)$, and $\partial_{\tau \odot \sigma}(x^\tau \odot x^\sigma) = x_A^\sigma \parallel x_C^\tau \vdash_{A \vdash C} c^-$, assuming w.l.o.g. it is in C. For *existence*, by receptivity of $\tau$ we have $x^\tau \vdash_\tau t$ such that $\partial_\tau(t) = c$. Writing $y^\tau = x^\tau \uplus \{t\}$, it is direct that $x^\sigma, y^\tau$ is minimal causally compatible, and $x^\tau \odot x^\sigma \leftarrow y^\tau \odot x^\sigma$ provides the required extension, via Proposition 6.2.22. For *uniqueness*, assume $x^\tau \odot x^\sigma \leftarrow c^\tau \odot z^\sigma$ via some event $p$ such that $\partial_{\tau \odot \sigma}(p) = c^-$. So,

$$x^\tau \otimes x^\sigma \subseteq u^\tau \otimes u^\sigma \leftarrow^p z^\tau \otimes z^\sigma$$

where $x^\tau \otimes x^\sigma \subseteq u^\tau \otimes u^\sigma$ adds a set X of synchronized events, such that for all $q \in X$, $q \leq_{\tau \odot \sigma} p$. But for any $q \to_{\tau \odot \sigma} p$, we have $q$ in C by Lemma 6.2.15, so X is empty. As p is in C, this entails $x^\sigma = u^\sigma = z^\sigma$ and $x^\tau = u^\tau \leftarrow c^\tau$. So $z^\tau = x^\tau \uplus \{t'\}$ such that $x^\tau \vdash_\tau t'$ and $\partial_\tau(t') = c$, so $t = t'$ by *receptive* for $\tau$; hence $y^\tau \odot x^\tau = z^\tau \odot z^\sigma$. $\square$

We have a well-defined composition operation for *strategies*, but we have not yet arrived at the claimed Proposition 6.2.1. For that, it still remains to investigate the effect of ignoring the trailing Opponent moves, restricting to *+-covered configurations*.
### 6.3.2 Strategies and +-covered configurations

In traditional alternating game semantics, strategies can be defined in two different ways: as done in Definition 3.1.2 by taking plays finishing by moves of arbitrary polarity, but requiring a receptivity property for strategies; or – as is more standard – by only considering even-length plays in strategies, that is, plays ending with Player moves. For concurrent strategies, a similar effect can be obtained via +-covered configurations:

**Definition 6.3.2.** Consider $\sigma$: A a(pre)strategy on game A. A configuration $x \in \mathscr{C}(\sigma)$ is +-covered if for any $s \in x$ such that $s \leq_{\sigma}$-maximal in x, $\mathrm{pol}_{\sigma}(s) = +$. We write $\mathscr{C}^{+}(\sigma)$ for the +-maximal configurations of $\sigma$.

We shall see that it suffices to compare strategies on their +-covered configurations. To show this, it is convenient to rely not on the original definition of strategies in Definition 6.1.6, but on the following more “big-step” characterization:

**Proposition 6.3.3.** Consider $\sigma$: A a prestrategy on game A. Then it is a strategy iff

- $\text{--discrete opfibration:}$ for all $x^{\sigma} \in \mathscr{C}(\sigma)$, for all $\partial_{\sigma}(x^{\sigma}) \subseteq^{-} y_{A} \in \mathscr{C}(A)$, there exists a unique $x^{\sigma} \subseteq y^{\sigma} \in \mathscr{C}(\sigma)$ s.t. $\partial_{\sigma}(y^{\sigma}) = y_{A}$.

- $\text{+-discrete fibration:}$ for all $x^{\sigma} \in \mathscr{C}(\sigma)$, for all $\partial_{\sigma}(x^{\sigma}) \supseteq^{+} y_{A} \in \mathscr{C}(A)$, there exists a unique $x^{\sigma} \supseteq y^{\sigma} \in \mathscr{C}(\sigma)$ s.t. $\partial_{\sigma}(y^{\sigma}) = y_{A}$.

where $x \subseteq^{p} y$ (for $p \in \{-, +\}$) means $x \subseteq y$ and $\mathrm{pol}_{A}(y \setminus x) \subseteq \{p\}$.

*Proof.* $\text{--discrete opfibration.}$ Existence is clear by repeated applications of receptive. For uniqueness, consider $x^{\sigma} \subseteq y^{\sigma}$, $z^{\sigma} \in \mathscr{C}(\sigma)$ s.t. $\partial_{\sigma}(y^{\sigma}) = \partial_{\sigma}(z^{\sigma}) = y_{A}$. Take $m_{1} \in y^{\sigma} \setminus x^{\sigma}$ and $m_{2} \in z^{\sigma} \setminus x^{\sigma}$ s.t. $\partial_{\sigma}(m_{1}) = \partial_{\sigma}(m_{2})$, w.l.o.g. assume that for any $m'_{1} <_{\sigma} m_{1}$ and $m'_{2} <_{\sigma} m_{2}$, $\partial_{\sigma}(m'_{1}) = \partial_{\sigma}(m'_{2})$ implies $m'_{1} = m'_{2}$. By courteous, $m_{1}$ and $m_{2}$ have the same immediate causal dependencies, so $m_{1} = m_{2}$ by receptive.

$\text{+-discrete fibration.}$ Existence follows by repeated applications of courtesy, which entails that events in $x^{\sigma} \in \mathscr{C}(\sigma)$ displaying to maximal positive events in $\partial_{\sigma}(x^{\sigma})$ must be maximal in $x^{\sigma}$. Uniqueness is clear by locally injective.

In the sequel, we shall only use this direction. So for the sake of economy, for the other direction we simply refer to [Castellan et al., 2017a, Lemma 3.13]. $\square$

This was first noticed by Winskel in [Winskel, 2013b], in seeking a connection between concurrent strategies as profunctors – indeed, by the lemma above, it also follows that strategies are also characterized by the discrete fibration property for the composite partial order $\sqsubseteq_{A} = \supseteq_{A}^{+}$, the so-called “Scott order”, which informs a link with profunctors. In this monograph, we shall merely use the $\text{--discrete opfibration}$ property. Relying on that, we refine the mapification lemma in the following way<fnref n="4" />:

**Lemma 6.3.4.** Consider $\sigma, \tau$: A two strategies. Assume there is a function

$$f: \mathscr{C}^{+}(\sigma) \to \mathscr{C}^{+}(\tau)$$

compatible with display maps and preserving unions. Then, there is a unique morphism of strategies $\hat{f}: \sigma \Rightarrow \tau$ such that for all $x \in \mathscr{C}^{+}(\sigma)$, $\hat{f}x = f x$.

<footnote n="4">⁴Thanks to Victor Blanchi for discovering this nice lemma!</footnote>
*Proof. Uniqueness.* Consider $g, h$ two such extensions, and consider $x \in \mathscr{C}(\boldsymbol{\sigma})$. Removing trailing events from $x$, there is a unique $y \in \mathscr{C}^{+}(\boldsymbol{\sigma})$ such that $y \subseteq^{-} x$. By hypothesis, $g(y) = h(y) = f(y)$. Since $g, h$ are maps of event structures and preserve display maps, they must preserve inclusion and polarities of these inclusions, so that

$$f(y) \subseteq^{-} g(x), h(x)$$

but $\partial_{\tau}g(x) = \partial_{\tau}h(x)$ by pres. of display maps, so $g(x) = h(x)$ by *--discrete opfibration* of Proposition 6.3.3. So $g(x) = h(x)$ for all $x \in \mathscr{C}(\boldsymbol{\sigma})$, so $g = h$ by Lemma 6.1.12.

*Existence.* We first extend $f$ to all configurations: if $x \in \mathscr{C}(\boldsymbol{\sigma})$, as above we consider the unique $y \in \mathscr{C}^{+}(\boldsymbol{\sigma})$ such that $y \subseteq^{-} x$ obtained by removing trailing negative events in $x$; as $f$ preserves display maps we have $\partial_{\tau}f(y) = \partial_{\sigma}y \subseteq^{-} \partial_{\sigma}x$. By *--discrete opfibration* of Proposition 6.3.3, there is a unique $z \in \mathscr{C}(\boldsymbol{\tau})$ such that $f(y) \subseteq^{-} z$ and $\partial_{\tau}(z) = \partial_{\sigma}(x)$; we set $f(x) = z$. So defined, $f : \mathscr{C}(\boldsymbol{\sigma}) \to \mathscr{C}(\boldsymbol{\tau})$ automatically preserves display maps and hence preserves cardinal (as $\partial_{\sigma}$ and $\partial_{\tau}$, as maps of event structures, are locally injective). By uniqueness in *--discrete opfibration* of Proposition 6.3.3, it is easy to prove that $f$ preserves unions. Hence by Lemma 6.1.11, it extends to a map of event structures in a unique way, concluding the proof.

*Rigidity.* We prove that any map of event structures $h : \boldsymbol{\sigma} \to \boldsymbol{\tau}$ such that $\partial_{\tau}oh = \partial_{\sigma}$ and that sends *+*covered configurations to *+*covered configurations, is rigid. We actually show that if $s_1 \to_{\sigma} s_2$, then $h(s_1) <_{\sigma} h(s_2)$, which entails rigidity. If $\mathrm{pol}(s_1) = +$ or $\mathrm{pol}(s_2) = -$, then $\partial_{\sigma}s_1 \to_A \partial_{\sigma}s_2$ by *courteous*, and thus $f(s_1) \leq_{\tau} f(s_2)$ by Lemma 6.1.8 – so that $f(s_1) <_{\tau} f(s_2)$ by local injectivity. It remains to consider the case where $\mathrm{pol}(s_1) = -$ and $\mathrm{pol}(s_2) = +$. In that case, as $[s_2]_{\sigma} \in \mathscr{C}^{+}(\boldsymbol{\sigma})$, we have $h([s_2]_{\sigma}) \in \mathscr{C}^{+}(\boldsymbol{\tau})$ as well. Now, observe that $s_1$ is maximal in $[s_2]_{\sigma}$, otherwise contradicting $s_1 \to_{\sigma} s_2$. Hence writing $x = [s_2]_{\sigma} \setminus \{s_1, s_2\}$, $y = [s_2]_{\sigma} \setminus \{s_2\}$, we have $x \subsetneq y \subsetneq [s_2]_{\sigma}$ in $\mathscr{C}(\boldsymbol{\sigma})$. This is sent to $\boldsymbol{\tau}$ via $h$ to the covering sequence in $\mathscr{C}(\boldsymbol{\tau})$

$$h(x) \stackrel{h(s_1)}{\leftarrow} h(y) \stackrel{h(s_2)}{\leftarrow} h([s_2]_{\sigma}),$$

which shows in particular that only $h(s_2)$ can possibly depend on $h(s_1)$ within $h([s_2]_{\sigma})$. Hence if $\neg(h(s_1) <_{\tau} h(s_2))$, it immediately follows that $h(s_1)$ is maximal in $h([s_2]_{\sigma})$. But $h(s_1)$ is negative, contradicting that $h([s_2]_{\sigma})$ is *+*covered; thus $h(s_1) <_{\sigma} h(s_2)$. $\square$

It is striking that the *rigidity* condition on morphisms is automatic, and follows from the fact that the map of event structures preserves *+*covered configurations!

This lemma will be used often, in two particular situations: firstly, to show that two morphisms of strategies coincide, it suffices to show that they coincide on *+*covered configurations; secondly, in order to prove $\boldsymbol{\sigma}$ and $\boldsymbol{\tau}$ isomorphic, it suffices to produce an order-iso between $\mathscr{C}^{+}(\boldsymbol{\sigma})$ and $\mathscr{C}^{+}(\boldsymbol{\tau})$ compatible with display maps (observing that the supremum of two *+*covered configurations in $\mathscr{C}^{+}(\boldsymbol{\sigma})$, if it exists, is their union).

### 6.3.3 Composition and *+*coveredness

Clearly *+*covered configurations are important, in that morphisms between strategies are entirely determined by their action on *+*covered configurations. Next we show that
additionally, +-covered configurations interact very well with composition. Let us fix
for now $\sigma$: $A \vdash B$ and $\tau$: $B \vdash C$ two strategies, and investigate their composition.

The first step is to remark that +-coverdness makes minimality redundant:

**Lemma 6.3.5.** *Consider $x^\sigma \in \mathscr{C}^+(\sigma)$ and $x^\tau \in \mathscr{C}^+(\tau)$ causally compatible. Then, $x^\sigma$ and $x^\tau$ are minimal causally compatible.*

*Proof.* Seeking a contradiction, assume there is a maximal event of $\varphi[x^\sigma, x^\tau]$ in $B$, necessarily of the form ((1, s), (2, t)) for $s \in x^\sigma$ and $t \in x^\tau$ necessarily both maximal. But necessarily one of them is negative, contradicting +-coveredness of $x^\sigma$ and $x^\tau$. $\square$

Besides, the resulting configurations of the composition are automatically +-covered:

**Lemma 6.3.6.** *Consider $x^\sigma \in \mathscr{C}^+(\sigma)$ and $x^\tau \in \mathscr{C}^+(\tau)$ causally compatible. Then, $x^\tau \odot x^\sigma \in \mathscr{C}^+(\tau \odot \sigma)$.*

*Proof.* First, $x^\sigma, x^\tau$ is minimal causally compatible by Lemma 6.3.5.

Consider $m \in x^\tau \odot x^\sigma$ maximal. This means that $m$ is also maximal in $x^\tau \otimes x^\sigma = [x^\tau \odot x^\sigma]_{\tau \otimes \sigma}$, so corresponds to some pair maximal in $\varphi[x^\sigma, x^\tau]$ via Lemma 6.2.12. Since $x^\sigma, x^\tau$ is minimal causally compatible, this pair is in $A$ or $C$ – say w.l.o.g. in $C$, so it has the form ((2, c), (2, t)) for $t \in x^\tau$. Necessarily, $t$ is maximal in $x^\tau$, so is positive since $x^\sigma \in \mathscr{C}^+(\tau)$. Hence, $m$ is positive as well. $\square$

So causally compatible +-covered $x^\sigma \in \mathscr{C}^+(\sigma)$ and $x^\tau \in \mathscr{C}^+(\tau)$ are minimal, and their composition yields $x^\tau \odot x^\sigma \in \mathscr{C}^+(\tau \odot \sigma)$ +-covered. We prove the converse:

**Lemma 6.3.7.** *Consider $x^\sigma \in \mathscr{C}(\sigma)$ and $x^\tau \in \mathscr{C}(\tau)$ minimal causally compatible. If $x^\tau \odot x^\sigma \in \mathscr{C}^+(\tau \odot \sigma)$ is +-covered, so are $x^\sigma \in \mathscr{C}^+(\sigma)$ and $x^\tau \in \mathscr{C}^+(\tau)$.*

*Proof.* Consider $s \in x^\sigma$ maximal. Necessarily, there is $p \in x^\tau \otimes x^\sigma$ such that $p_\sigma = s$. If $p$ is maximal in $x^\tau \otimes x^\sigma$, by Lemma 6.2.19 we have $x^\tau \otimes x^\sigma = [x^\tau \odot x^\sigma]_{\tau \otimes \sigma}$, so $p$ must be visible and maximal in $x^\tau \odot x^\sigma$, hence positive by hypothesis, and $s$ is positive. Otherwise, there is some $p \dashv_{\tau \otimes \sigma} q$. By Lemma 6.2.14, $p_\sigma \dashv_\sigma q_\sigma$ or $p_\tau \dashv_\tau q_\tau$. The former contradicts maximality of $p_\sigma = s$, so $p_\tau \dashv_\tau q_\tau$. If $s$ is positive, we are done. Otherwise, $p_\tau$ is positive, so $q_\tau$ is also in $B$ by *courteous*, and $\partial_\tau(p_\tau) <_{B \vdash C} \partial_\tau(q_\tau)$. Then $q_\sigma$ is also defined, and by Lemma 6.1.8, $p_\sigma < q_\sigma$, contradicting maximality of $s$. The symmetric reasoning shows any $t \in x^\tau$ maximal in $x^\tau$ is positive. $\square$

We can now finally deduce our characterization of the composition of strategies:

**Proposition 6.2.1.** *Consider A, B, C games, and $\sigma$: $A \vdash B$ and $\tau$: $B \vdash C$ strategies. Then there is a strategy $\tau \odot \sigma$: $A \vdash C$, unique up to iso, s.t. there are order-isos:*

$$(- \odot -) : \{(x^\tau, x^\sigma) \in \mathscr{C}^+(\tau) \times \mathscr{C}^+(\sigma) \mid \text{causally compatible}\} \simeq \mathscr{C}^+(\tau \odot \sigma)$$

such that for $x^\sigma \in \mathscr{C}^+(\sigma)$ and $x^\tau \in \mathscr{C}^+(\tau)$ causally compatible,

$$\partial_{\tau \odot \sigma}(x^\tau \odot x^\sigma) = x_A^\sigma \vdash x_C^\tau$$

where we write $\partial_\sigma x^\sigma = x_A^\sigma \vdash x_B^\sigma$ and $\partial_\tau x^\tau = x_B^\tau \vdash x_C^\tau$.
<figure><img src="image_77.png" /><figcaption>Figure 6.6: The copycat strategy on $(U \to U) \to U$</figcaption></figure>

*Proof. Existence.* The composition exists by Proposition 6.2.22, and is a strategy by Proposition 6.3.1. The isos are restrictions of those of Proposition 6.2.22. By Lemma 6.3.5, causally compatible $x^\sigma \in \mathscr{C}^+(\sigma)$ and $x^\tau \in \mathscr{C}^+(\tau)$ are automatically minimal, and by Lemma 6.3.6, $x^\tau \odot x^\sigma \in \mathscr{C}^+(\tau \odot \sigma)$ is $+\text{-covered}$. Reciproally, if $x^\tau \odot x^\sigma \in \mathscr{C}^+(\tau \odot \sigma)$ is $+\text{-covered}$, then by Lemma 6.3.7, so are $x^\sigma \in \mathscr{C}^+(\sigma)$ and $x^\tau \in \mathscr{C}^+(\tau)$. 

*Uniqueness.* By Lemma 6.3.4. □

This concludes our study of composition of prestrategies and strategies. In the next section, we show that games and strategies may be organized into a bicategory **CG**.

## 6.4 The Bicategory CG

The bicategory will have: as *objects*, games, as *morphisms* from *A* to *B*, the strategies on *A* $\vdash$ *B*, and as *2-cells*, the morphisms of strategies. We have already seen above the composition of strategies and the *unitors*, 2-cells witnessing associativity of composition. It remains to construct *identities*, 2-cells witness identity laws, definition of horizontal composition of 2-cells; after which we must establish the coherence laws.

### 6.4.1 Copycat

First we define *copycat strategies*, which will provide identities.

**Definition.** Copycat, illustrated in Figure 6.6, is an *asynchronous forwarder*: it sends each negative event on *A* $\vdash$ *A* to the matching positive event on the other side.

We start with the components of copycat, postponing the verification of conditions.
**Definition 6.4.1.** For any game A, we set $\mathfrak{c}_A : A \vdash A$ with components:

$$
\begin{array}{rcl}
\text{events:} & |\mathfrak{c}_A| & = |A| + |A| \\
\text{causality:} & \leq_{\mathfrak{c}_A} & = \left( \left( \left( (1, a), (1, a') \right) \mid a \leq_A a' \right) \right) \cup \\
& & \quad \left( \left( (2, a), (2, a') \right) \mid a \leq_A a' \right) \cup \\
& & \quad \left( \left( (1, a), (2, a) \right) \mid \text{pol}_{\mathfrak{c}_A}(a) = + \right) \cup \\
& & \quad \left( \left( (2, a), (1, a) \right) \mid \text{pol}_{\mathfrak{c}_A}(a) = - \right) \right)^* \\
\text{conflict:} & \#_{\mathfrak{c}_A} & = \left\{ (e_1, e_2) \mid \exists e'_1 \leq_{\mathfrak{c}_A} e_2, e'_2 \leq_{\mathfrak{c}_A} e_2, e'_1 \#_{A \vdash A} e'_2 \right\}
\end{array}
$$

where $(-)^*$ is the transitive closure; and $\partial_{\mathfrak{c}_A} : |\mathfrak{c}_A| \to |A \vdash A|$ the identity function.

Copycat is often a challenging landmark in setting up a game semantics, and here it is no exception: it is not obvious at all that it satisfies all the required conditions! We shall slowly examine various aspects of this definition, for a fixed game A.

**The event structure $\mathfrak{c}_A$.** We first focus on the basic structure of $\mathfrak{c}_A$.

**Lemma 6.4.2.** Consider A a game. Then, $|\mathfrak{c}_A|, \leq_A, \#_A$ is an event structure.
Moreover, $\mathcal{C}(\mathfrak{c}_A) = \{x \mid y \mid x, y \in \mathcal{C}(A), x \cap y \subseteq^+ x \& x \cap y \subseteq^- y\}$.

*Proof.* Immediate verifications, omitted. $\square$

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

It will be useful to understand exactly what are the immediate causal links of $\mathfrak{c}_A$:

**Lemma 6.4.3.** Consider A a game, and $(i, a), (j, a') \in \mathfrak{c}_A$. Then $(i, a) \dashrightarrow_{\mathfrak{c}_A} (j, a')$ iff

(1) $i = j, a \dashrightarrow_A a'$, and $(\text{pol}_{\mathfrak{c}_A}(i, a) = + \text{ or } \text{pol}_{\mathfrak{c}_A}(j, a') = -)$, or

(2) $i \neq j, a = a'$, $\text{pol}_{\mathfrak{c}_A}(i, a) = -$ and $\text{pol}_{\mathfrak{c}_A}(j, a') = +$.

This is a direct verification. We also include a direct consequence of this:

**Lemma 6.4.4.** Consider A a game. Then, $\mathcal{C}^+(\mathfrak{c}_A) = \{x \mid x \mid x \in \mathcal{C}(A)\}$.

*Proof.* $\sqsupset$. Clear by Lemma 6.4.2.

$\subseteq$. Consider $x \parallel y \in \mathcal{C}^+(\mathfrak{c}_A)$; by Lemma 6.4.2, we have $x, y \in \mathcal{C}(A)$ with $x \cap y \subseteq^+ x$ and $x \cap y \subseteq^- y$. Suppose one of these inclusions is strict; for instance with $a \in y$ such that $a \notin x$ (the other case is symmetric). Necessarily, $\text{pol}_{\mathfrak{c}_A}(a) = -$. If $a$ is maximal in $y$, then $(2, a)$ is maximal in $x \parallel y$ by Lemma 6.4.3 since $a \notin x$. But $\text{pol}_{A \vdash A}(2, a) = -$, contradicting that $x \parallel y$ is $+-$covered. Otherwise, there is $a' \in y$ such that $a \dashrightarrow_A a'$. Now if $\text{pol}_{\mathfrak{c}_A}(a') = +$, we must have $a' \in x$, so $a \in x$ as $x \in \mathcal{C}(A)$, contradiction. So, $\text{pol}_{\mathfrak{c}_A}(a') = -$. By iterating this reasoning, we find $a'' \in y \setminus x$ negative and maximal for A; and by the reasoning above $(2, a'')$ is negative maximal in $x \parallel y$, contradiction. $\square$

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

This lemma above will play an important role in this monograph: it shows that when restricting to $+-$covered configurations (which is always possible when comparing strategies, by Lemma 6.3.4), copycat behaves as the identity relation. For $x \in \mathcal{C}(A)$, we write $\mathfrak{c}_x = x \vdash x \in \mathcal{C}^+(\mathfrak{c}_A)$ for the corresponding $+-$covered configuration.

Next, we show that copycat indeed is a well-formed strategy.
**Proposition 6.4.5.** For any game A, we have $\mathfrak{c}_A : A \vdash A$ a strategy.

*Proof.* By Lemma 6.4.2, $\mathfrak{c}_A$ is an event structure. It is direct that $\partial_{\mathfrak{c}_A}$ is a map of event structures. *Courteous* follows from Lemma 6.4.3, and *receptive* from Lemma 6.4.2. $\square$

In the sequel, we shall mostly reason on copycat via the characterization of its +- covered configurations in Lemma 6.4.4, showing that it acts as an identity relation.

## 6.4.2 Copycat and Strategies

Now, we show that copycat indeed is neutral for composition with respect to strategies.

**The unitors.** To define the unitor isomorphisms, from our existing tools, the only thing left to prove is that synchronizations with copycat never induce any deadlock. For this – and for later on in this monograph – we introduce the following lemma:

**Lemma 6.4.6.** Take $\sigma : A \vdash B, \tau : B \vdash C$, and $x^\sigma \in \mathscr{C}(\sigma), x^\tau \in \mathscr{C}(\tau)$ matching.

Consider the relation $\triangleleft_\sigma \cup \triangleleft_\tau$ on $x_A \parallel x_B \parallel x_C$ defined with

$$ (\partial_{\sigma} \parallel C)(m) \triangleleft_{\sigma} (\partial_{\sigma} \parallel C)(m') \quad \text{where} \quad m <_{\sigma \parallel C} m' \quad (m, m' \in x^{\sigma} \parallel x_{C}), $$

$$ (A \parallel \partial_{\tau})(m) \triangleleft_{\tau} (A \parallel \partial_{\tau})(m') \quad \text{where} \quad m <_{A \parallel \tau} m' \quad (m, m' \in x_A \parallel x^{\tau}) $$

$$ \text{writing } \partial_{\sigma}(x^{\sigma}) = x_A \parallel x_B \text{ and } \partial_{\tau}(x^{\tau}) = x_B \parallel x_C. $$

Then, $x^\sigma, x^\tau$ are causally compatible iff $\triangleleft_\sigma \cup \triangleleft_\tau$ has no cycle within $x_B$.

*Proof.* If. First, notice that $\triangleleft$ has no direct link between $x_A$ and $x_C$. The crux of the argument is that if $m \triangleleft m'$ with one of them in A, then $m \triangleleft_\sigma m'$: indeed if they are both in A, then by definition either $m \triangleleft_\sigma m'$ and we are done, or $m <_{A \parallel B \parallel C} m'$ and $m \triangleleft_\sigma m'$ follows from Lemma 6.1.8. Likewise, if $m \triangleleft m'$ with one of them in C, then $m \triangleleft_\tau m'$.

We proceed with the proof. First, it is a simple reformulation of the definition that $x^\sigma, x^\tau$ are causally compatible iff $\triangleleft = \triangleleft_\sigma \cup \triangleleft_\tau$ is acyclic. If there is a cycle in $\triangleleft$, it must pass through B: otherwise it still entirely in A or C. But by the observation above, this yields a cycle in $\triangleleft_\sigma$ or $\triangleleft_\tau$, contradiction. So the cycle passes through B. Then, for

$$ m^B \triangleleft n_1^A \triangleleft \dots \triangleleft n_k^A \triangleleft (m')^B, $$

again by the observation above all those links are in $\triangleleft_\sigma$, hence $m^B \triangleleft_\sigma (m')^B$. Likewise, all sections of the cycle in C may be removed symmetrically, yielding a cycle in $x_B$. $\square$

We now focus on the interactions of a strategy with copycat. In particular, the core of the next lemma is that no deadlocks can arise from the interaction of a strategy with copycat, so that all matching pairs of +-covered configurations are causally compatible.

**Lemma 6.4.7.** Consider $\sigma : A \vdash B$ a strategy, and $x^\sigma \in \mathscr{C}^+(\sigma)$, $x^{\mathfrak{c}_B} \in \mathscr{C}^+(\mathfrak{c}_B)$.

Then, $x^\sigma, x^{\mathfrak{c}_B}$ are causally compatible iff $x^{\mathfrak{c}_B} = \mathfrak{c}_{x^\sigma}$, for $\partial_\sigma(x^\sigma) = x_A^\sigma \parallel x_B^\sigma$.
**Proof.** If. Write $\partial_{\sigma}(x^{\sigma}) = x_A \parallel x_B$, and seeking a contradiction, consider a cycle in $x_A \parallel x_B^{\ell} \parallel x_B^{r}$ - using $\ell, r$ for disambiguation - in the relation $\triangleleft_{\sigma} \cup \triangleleft_{\mathfrak{c}_B}$ defined as:

$$ (\partial_{\sigma} \parallel B)(m) \triangleleft_{\sigma} (\partial_{\sigma} \parallel B)(m') \quad \text{where} \quad m <_{\sigma \parallel B} m' \quad (m, m' \in x^{\sigma} \parallel x_{B}^{r}) \\ (A \parallel \partial_{\mathfrak{c}_B})(m) \triangleleft_{\mathfrak{c}_B} (A \parallel \partial_{\mathfrak{c}_B})(m') \quad \text{where} \quad m <_{A \parallel \mathfrak{c}_B} m' \quad (m, m' \in x_A \parallel x_{B}^{\ell} \parallel x_{B}^{r}), $$

by Lemma 6.4.6 we can assume that the cycle is entirely in $x_B^{\ell}$. Now, it is straightforward from the definition of $\mathfrak{c}_B$ that if $m \triangleleft_{\mathfrak{c}_B} m'$ with $m, m'$ in $x_B^{\ell}$, then $m <_{A \parallel B \parallel B} m'$ so that $m \triangleleft_{\sigma} m'$ by Lemma 6.1.8. Thus, this yields a cycle in $\triangleleft_{\sigma}$, contradiction.

Only if. Immediate from the definition and Lemma 6.4.4. □

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

Clearly, the symmetric lemma holds, with a symmetric proof:

**Lemma 6.4.8.** Consider $\sigma : A \vdash B$ a strategy, and $x^{\mathfrak{c}_A} \in \mathcal{C}^+(\mathfrak{c}_A)$, $x^{\sigma} \in \mathcal{C}^+(\sigma)$.

Then, $x^{\mathfrak{c}_A}, x^{\sigma}$ are causally compatible iff $x^{\mathfrak{c}_A} = \mathfrak{c}_{x^{\sigma}}$, for $\partial_{\sigma}(x^{\sigma}) = x_A^{\sigma} \parallel x_B^{\sigma}$.

This completes the ingredients needed to define the *unitors*:

**Proposition 6.4.9.** Consider $\sigma : A \vdash B$ a strategy.

Then there are unique isomorphisms of strategies, the *unitors*:

$$ l_{\sigma} : \mathfrak{c}_{B} \odot \sigma \cong \sigma \qquad r_{\sigma} : \sigma \odot \mathfrak{c}_{A} \cong \sigma $$

such that for all $x^{\sigma} \in \mathcal{C}^{+}(\sigma)$, we have $l_{\sigma}(\mathfrak{c}_{x^{\sigma}} \odot x^{\sigma}) = x^{\sigma}$ and $r_{\sigma}(x^{\sigma} \odot \mathfrak{c}_{x^{\sigma}}) = x^{\sigma}$.

**Proof.** Configurations and symmetries of $\mathfrak{c}_B \odot \sigma$ and $\sigma \odot \mathfrak{c}_A$ have this shape by Lemmas 6.4.7 and 6.4.8. These assignments on configurations are order-isos and compatible with display maps, thus extend to an isomorphism of strategies by Lemma 6.3.4. □

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

### 6.4.3 Horizontal Composition and Bicategorical Structure

The missing piece is the horizontal composition of 2-cells, handled by:

**Proposition 6.4.10.** Consider $\sigma, \sigma' : A \vdash B$ and $\tau, \tau' : B \vdash C$ strategies, and $f : \sigma \Rightarrow \sigma'$, $g : \tau \Rightarrow \tau'$ morphisms of strategies.

There is a unique morphism of strategies, the horizontal composition of $f$ and $g$,

$$ g \odot f : \tau \odot \sigma \Rightarrow \tau' \odot \sigma', $$

such that $(g \odot f)(x^{\tau} \odot x^{\sigma}) = g(x^{\tau}) \odot f(x^{\sigma})$ for all $x^{\tau} \odot x^{\sigma} \in \mathcal{C}^{+}(\tau \odot \sigma)$.

**Proof. Uniqueness.** Obvious from Lemma 6.3.4.

**Existence.** Consider $x^{\tau} \odot x^{\sigma} \in \mathcal{C}^{+}(\tau \odot \sigma)$. As $f$ and $g$ preserve display maps, $f(x^{\sigma})$ and $g(x^{\tau})$ are matching. As $f$ and $g$ are rigid, and by Lemma 6.1.8, they induce order-isos $f : x^{\sigma} \cong f(x^{\sigma})$ and $g : x^{\tau} \cong g(x^{\tau})$, so $f(x^{\sigma})$ and $g(x^{\tau})$ are still +-covered, and causally compatible. So the action on +-covered configurations $x^{\tau} \odot x^{\sigma} \in \mathcal{C}^{+}(\tau \odot \sigma)$ given above is well-defined. It obviously preserves display maps and preserves unions by Lemma 6.2.20, hence it lifts to a morphism of strategies by Lemma 6.2.20. □

<figure><img src="image_82.png" /></figure>
We are now in position to conclude with the bicategorical structure:

**Theorem 6.4.11.** There is CG, a bicategory with: objects, all games, morphisms from A to B, strategies on A ⊢ B, and 2-cells, morphisms of strategies.

*Proof.* Identities are copycat strategies, composition is composition of strategies. Associates are defined in Section 6.2.3, unitors in Section 6.4.2. The laws are obtained by checking them pointwise on $+\text{-covered configurations}$ and concluding by Lemma 6.3.4; for instance, naturality of the left unitor is established very simply, via:

$$ 
\begin{align*}
l_{\sigma} \circ (\mathrm{id} \otimes f)(\mathfrak{c}_{X_B} \sigma \circ x^{\sigma}) &= l_{\sigma}(\mathfrak{c}_{X_B} \sigma \circ f(x^{\sigma})) \\
&= f(x^{\sigma}) \\
&= f \circ l_{\sigma}(\mathfrak{c}_{X_B} \sigma \circ x^{\sigma})
\end{align*}
$$

for $f : \sigma \Rightarrow \sigma' : A \vdash B$ a morphism of strategies, and $x^{\sigma} \in \mathscr{C}^{+}(\sigma)$. $\square$

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

There is, of course, much more to the structure of CG. In particular it is a compact closed bicategory, and may be used as a model for a linear programming language. But we shall not investigate this structure further, and will do it instead for TCG.

### 6.4.4 Characterization of Strategies

Before adding symmetry into the picture, we prove an additional property on copycat. Namely, it allows a neat characterization of strategies among prestrategies:

**Proposition 6.4.12.** Consider $\sigma : A \vdash B$ a prestrategy.

Then, $\sigma$ is a strategy iff $\mathfrak{c}_B \odot \sigma \odot \mathfrak{c}_A \cong \sigma$.

*Proof.* If. It suffices to prove that $\mathfrak{c}_B \odot \sigma \odot \mathfrak{c}_A$ is automatically receptive and courteous.

For courteous, consider $p \to^{\mathfrak{c}_B \odot \sigma \odot \mathfrak{c}_A} p'$ such that $\mathrm{pol}(p) = +$ or $\mathrm{pol}(p') = -$, say first it is the former. Necessarily $p$ occurs in A or B, say w.l.o.g. that it is in B. Up to iso we consider $p \to^{\mathfrak{c}_B \odot \sigma'} p'$, for $\sigma' = \sigma \odot \mathfrak{c}_A$. By Lemma 6.2.21 we have

$$ p \to^{\mathfrak{c}_B \otimes \sigma'} q_1 \to^{\mathfrak{c}_B \otimes \sigma'} \dots \to^{\mathfrak{c}_B \otimes \sigma'} q_n \to^{\mathfrak{c}_B \otimes \sigma'} p' $$

with $q_1, \dots, q_n$ synchronized. By Lemma 6.2.14, we must have $p_{\mathfrak{c}_B} \to^{\mathfrak{c}_B} (q_1)_{\mathfrak{c}_B}$ - as $p_{\sigma}$ does not exist. But as $p$ is positive, this implies $\partial_{\mathfrak{c}_B}(p_{\mathfrak{c}_B}) \to_{B \vdash B} \partial_{\mathfrak{c}_B}((q_1)_{\mathfrak{c}_B})$, contradicting $q_1$ synchronized, so $p \to^{\mathfrak{c}_B \otimes \sigma'} p'$ and $p_{\mathfrak{c}_B} \to^{\mathfrak{c}_B} p'_{\mathfrak{c}_B}$, which entails $\partial_{\mathfrak{c}_B}(p_{\mathfrak{c}_B}) \to_{B \vdash B} \partial_{\mathfrak{c}_B}(p'_{\mathfrak{c}_B})$ so that $\partial_{\mathfrak{c}_B \odot \sigma'}(p) \to_{A \vdash B} \partial_{\mathfrak{c}_B \odot \sigma'}(p')$ as required. All the other cases are symmetric, so that $\partial_{\mathfrak{c}_B \odot \sigma \odot \mathfrak{c}_A}(p) \to_{A \vdash B} \partial_{\mathfrak{c}_B \odot \sigma \mathfrak{c}_A}(p')$ as required.

For receptive, consider $z \in \mathscr{C}(\mathfrak{c}_B \odot \sigma \odot \mathfrak{c}_A)$ with $\partial_{\mathfrak{c}_B \odot \sigma \odot \mathfrak{c}_A}(z) \vdash_{A \vdash B} b^-$, w.l.o.g. assume $b$ occurs in B, and consider again $z$, which by Proposition 6.2.22 we may write as $z = (x_B \parallel y_B) \odot x^{\sigma'} \in \mathscr{C}(\mathfrak{c}_B \odot \sigma')$ with $\sigma' = \sigma \odot \mathfrak{c}_A$, with $\partial_{\mathfrak{c}_B \odot \sigma'}(z) = x_A^{\sigma'} \parallel y_B$. So by hypothesis, we have $y_B \vdash B^-$. Then it is immediate that $x_B \parallel (y_B \cup \{b\})$ are still minimal causally compatible, so that by Proposition 6.2.22 we have

$$ (x_B \parallel y_B) \odot x^{\sigma'} \stackrel{p}{\rightleftharpoons} (x_B \parallel (y_B \cup \{b\})) \odot x^{\sigma'} $$
for some $(x_B \parallel y_B) \odot x^{\sigma'} \vdash_{\omega_B \odot \sigma'} p$ such that $\partial_{\omega_B \odot \sigma'}(p) = b$. Uniqueness is straightforward via Proposition 6.2.22 and definition of $\partial_{\omega_B \odot \sigma'}$.

Receptive and courteous are clearly invariant under strong iso, so $\sigma$ is a strategy.

Only if. By bicategorical laws for CG. ☐

Thus strategies are exactly those prestrategies invariant under composition with copycat, i.e. robust when accessed under asynchronous delay. Conceptually, this vindicates the definition of strategies. Technically, it occasionally provides a convenient way to prove that certain prestrategies are actually strategies. This result appeared as the main theorem in Rideau and Winskel's original paper on concurrent strategies [Rideau and Winskel, 2011]. A result in the same spirit already appeared in Ghica and Murawski's interleaving concurrent games model [Ghica and Murawski, 2008].

## 6.5 Conclusions and Historical Notes

*Concurrent games* were initiated by Abramsky and Melliès' seminal fully complete model for MALL [Abramsky and Melliès, 1999]. There, strategies are certain stable closure operators on dI-domains: intuitively, a strategy-as-closure-operator closes the current position under all available Player moves, played in some unspecified order. Concurrent games were originally presented as a way to circumvent the so-called *Blass problem*, i.e. the non-associativity of composition in Blass' model of linear logic, diagnosed in [Abramsky, 2003] as due to an excess of sequentiality.

**Asynchronous Games.** Following this, Melliès led a research programme on *asynchronous games* [Melliès, 2003, Melliès, 2004a, Melliès, 2004b, Melliès, 2005]. Melliès' goal was to reproduce and extend the success of concurrent games in a language closer to more standard (sequential) game semantics; as well as put the spotlight on the *causal structures* that lurk behind the traditional notion of *innocence*. Asynchronous games are based on Mazurkiewicz traces: plays are *alternating* but related by *homotopy tiles* expressing causal independence between parts of computation. Plays up to homotopy give rise to a notion of *positions* compatible with the positions of the original concurrent games. Based on alternating asynchronous games, Melliès was able to provide a fully complete model of full propositional linear logic [Melliès, 2005], showing that what made this possible already for closure operators was not in fact concurrency, but *positionality* – see [Clairambault, 2023] for a recent retelling of this story.

Later, Melliès and Mimram developed basic *non-alternating* asynchronous games [Melliès and Mimram, 2007]. While non-alternating asynchronous strategies are non-deterministic as sets of plays, they satisfy conditions ensuring that they are essentially deterministic up to the choice of the scheduler – in particular, it follows a posteriori from the conditions that the set of possible executions is the set of linearizations of a *causality* partial order: provided the external Opponent plays in the same way, all execution paths will ultimately reach the same state.
**Strategies as Partial Orders.** Independently, a notion of *strategies-as-partial-orders* emerged from Girard's Ludics [Girard, 2001]. Indeed, *designs* (*strategies in Ludics*) may be seen as a linear version of Hyland-Ong strategies [Faggian and Hyland, 2002], presented following their *causal* structure rather than the traditional chronologically ordered plays. This inspired *Ludics Nets*, or *L-nets* [Faggian and Maurel, 2005]: a notion of *strategies-as-graph*, aiming at a concurrent generalization of designs (see also [Curien and Faggian, 2005] for links with more standard strategies via proof nets). Inspired by this line of work and ideas from Hyland, Faggian and Piccolo introduced a category of *strategies-as-partial-orders* [Faggian and Piccolo, 2009], which lands close to Mimram and Melliès' non-alternating asychronous strategies – but whereas in Mimram and Melliès' work the causal partial order is derived, here it is primitive.

**Strategies as Event Structures.** Rideau and Winskel then introduced the b Category CG [Rideau and Winskel, 2011] that we developed in this chapter: as for Fag- gian and Piccolo, strategies in CG are explicitly partially ordered, but they additionally have a fibred structure letting them harmonously handle non-determinism with explicit branching information – this is analogous to other fibred approaches to non-determinism in game semantics [Eberhart et al., 2017, Jacq and Melliès, 2018]. At the same time, Winskel was starting a research project “ECSYM”, seeking a concurrent generaliza- tion of domain theory – the main inspirations were the non-deterministic extension of domain theory given by spans of event structures [Saunders-Evans and Winskel, 2006] and *event structures with symmetry* [Winskel, 2007]. But ECSYM soon focused on games and strategies and was the cradle for the first steps of the present developments.

From now on, unless specified otherwise and until the end of this document, we shall use the term *concurrent games* to refer specifically to this latter framework **CG** – keeping in mind all its precursors and the intellectual history behind it.
# Chapter 7

## Thin Concurrent Games

The main limitation of **CG** is that it is inherently restricted to speaking about systems with linear resource usage. Indeed, games as in Definition 6.1.3 do not support the *bang* construction from linear logic. Of course, one can define in **CG** a construction on games taking countably many copies as illustrated in (6.3), but this operation is incomplete: analogously to categorifications of the relational model (generalized species of structure [Fiore et al., 2008] or template games [Melliès, 2019b]) where *states* form a groupoid, we need to add additional structure to games, expressing which events are “morally the same” by specifying the admissible permutations between events.

Intuitively, the roadmap for building *concurrent games with symmetry* is to follow the same recipe as for **CG**, but replacing *event structures* (and their maps) with Winskel’s *event structures with symmetry* [Winskel, 2007] – which add to event structures precisely the ability to express these missing permutations. But while developing this, it turned out far more subtle than initially anticipated. With respect to this anticipated roadmap, the main surprise of **TCG** is a rediscovery of phenomenon first noticed by Melliès in the setting of asynchronous games: that a *causal, deterministic* account of uniformity required to split symmetries into two, the *positive* symmetries due to Player, and the *negative* symmetries due to Opponent [Melliès, 2003].

In this chapter, we will review a few of the subtleties and arising design choices. Then we shall focus on constructing *Thin Concurrent Games*, under the form of a bicategory **TCG**. We must hence ask the reader to brace for another rather technical journey. Like **CG**, the construction of **TCG** is not easy. But like **CG**, we did our best to engineer its construction in such a way that one can use it later on while leaving most combinatorial details and low-level definitions nicely encapsulated.

### 7.1 Symmetry in Games and Strategies

In this section, we introduce the basic definitions for games and strategies in the presence of symmetry, leaving for later the compositional structure. Before that, we start
with a few preliminaries on event structures with symmetry.

### 7.1.1 Event Structures with Symmetry

In order to motivate the definition of event structures with symmetry, we start with the key construction that introduces symmetry in games arising from the interpretation of types or linear logic formulas: the bang-making formal the illustration of (6.3).

**Definition 7.1.1.** Consider A a game. Then, we define the bang !A with:

$$
\begin{array}{lll}
\text{events:} & |!A| = \mathbb{N} \times |A| & \\
\text{causality: } (i, a_1) \leq_! A (j, a_2) & \Leftrightarrow i = j \land a_1 \leq_A a_2 & \\
\text{conflict: } (i, a_1) \#_! A (j, a_2) & \Leftrightarrow i = j \land a_1 \#_A a_2 & \\
\text{polarities: } \text{pol}_! A(i, a) & = \text{pol}_A(a). &
\end{array}
$$

Following the methodology of linear logic, the construction !A injects a non-linear behaviour into an otherwise linear setting – one may define the usual, non-linear arrow via $A \to B = !A \dashv B$. To achieve that, the definition above follows the intuition from AJM games (see Section 3.4) that !A consists in countably many independent copies of the game A, kept apart via integers referred to as *copy indices*.

It will be useful to adopt specific notations for configurations of !A. First:

**Definition 7.1.2.** Consider A a game. We write $\text{Fam}(A)$ for the set of all families $(x_i)_{i \in I}$ where $I \subseteq f \mathbb{N}$ is a finite set of integers, and $x_i \in \mathscr{C}(A)$ with $x_i \neq \emptyset$ for all $i \in I$. We call elements of $\text{Fam}(A)$ simply *families* on A.

The set $\text{Fam}(A)$ is partially ordered by $(x_i)_{i \in I} \le (y_j)_{j \in J}$ iff $I \subseteq J$ and $x_i \subseteq y_i$ for all $i \in I$. Families on A are useful in that they correspond to configurations of !A – the proof of this proposition is straightforward, but observe that it crucially relies on the hypothesis that the configurations appearing in families are *non-empty*.

**Proposition 7.1.3.** Consider A a game. Then, the function

$$
\begin{array}{rcl}
\text{Fam}(A) & \to & \mathscr{C}(!A) \\
(x_i)_{i \in I} & \mapsto & \sum_{i \in I} x_i = \bigcup_{i \in I} \{i\} \times x_i
\end{array}
$$

is an order-isomorphism – we often write $[x_i | i \in I] \in \mathscr{C}(!A)$ for $(x_i)_{i \in I} \in \text{Fam}(A)$.

Copy indices are special with respect to other constructions producing new moves. They keep distinct copies apart, but in principle the behaviour of strategies should not depend on the specific integers used: their exact value should not matter, which we express with our convention introduced in Section 3.4 to often write them down in *grey*. But we need a formal way to express that they are indeed interchangeable:

**Definition 7.1.4.** Consider A a game, and $x, y \in \mathscr{C}(!A)$. A *plain reindexing* $\theta: x \cong_A y$ is a bijection $\theta: x \cong y$ such that there is $\pi: I \cong J$ a permutation satisfying

$$ \theta(i, a) = (\pi(i), a) $$

for all $(i, a) \in !A$.
A plain reindexing links two configurations $x, y \in \mathscr{C}(!A)$ which only differ via copy indices for the bang. We need more than an equivalence relation: to express that strategies are “invariant under reindexings”, we need an explicit bijection rather than the mere information that two configurations can be reindexed to each other. Indeed, while in AJM games an equivalence $s \cong_A t$ induces, chronologically, a 1-to-1 matching between the events of $s$ and those of $t$, an equivalence relation does not suffice anymore for configurations, which are only partially ordered – hence explicit bijections are required.

Plain reindexings only change copy indices coming from the external !, but in general reindexings may affect copy indices coming from deep within the type. Thus a type should not be interpreted only with a game, but with a “game with a set of allowed reindexings” – but to what mathematical structure does that correspond?

**Isomorphism families.** It is an *isomorphism family* on an event structure:

**Definition 7.1.5.** An *isomorphism family* on event structure $E$ is a set $\mathcal{S}(E)$ of bijections between configurations of $E$, satisfying the additional conditions:

groupoid: $\mathcal{S}(E)$ contains identities; is closed under composition and inverse.

restriction: for all $\theta: x \simeq y \in \mathcal{S}(E)$ and $x \supseteq x' \in \mathscr{C}(E)$, there is a (necessarily) unique $\theta' \supseteq \theta' \in \mathcal{S}(E)$ s.t. $\theta' : x' \simeq y'$.

extension: for all $\theta: x \simeq y \in \mathcal{S}(E)$, $x \subseteq x' \in \mathscr{C}(E)$, there is a (not necessarily unique) $\theta \subseteq \theta' \in \mathcal{S}(E)$ s.t. $\theta' : x' \simeq y'$.

The pair $(E, \mathcal{S}(E))$ is called an **event structure with symmetry (ess).**

We regard isomorphism families as *proof-relevant* equivalence relations: they convey which configurations are interchangeable, witnessed by an explicit bijection.

If $E$ is an ess, we call the elements of $\mathcal{S}(E)$ **symmetries**. We write $\theta : x \cong_E y$ to mean that $\theta : x \simeq y$ is a bijection such that $\theta \in \mathcal{S}(E)$, and write $x = \mathrm{dom}(\theta)$ and $y = \mathrm{cod}(\theta)$. We also write $x \cong_E y$ to mean that there is a symmetry $\theta$ such that $\theta : x \cong_E y$, this yields an equivalence relation on configurations.

It is an easy exercise to prove that symmetries are automatically order-isomorphisms:

**Lemma 7.1.6.** Consider $E$ an ess, and $\theta : x \cong_E y$ a symmetry.
Then, for all $e_1, e_2 \in x$, we have $e_1 \leq_E e_2$ iff $\theta(e_1) \leq_E \theta(e_2)$.

*Proof.* Left as an exercise to the reader.

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

**Maps with symmetry.** If event structures are equipped with an isomorphism family, we must adjust the notion of maps of event structures so that symmetry is preserved:

**Definition 7.1.7.** Consider $E$ and $F$ two ess, and $f : E \to F$ a map of event structures. We say that $f$ preserves symmetry if for all $\theta \in \mathcal{S}(E)$, we have $f\theta \in \mathcal{S}(F)$, where

$$f\theta = \{(fe, fe') | (e, e') \in \theta\}.$$

Then $f$ is a **map of event structures with symmetry** – we write **ESS** for the category.
It is immediate that $f \theta$ may also be expressed as the composition

$$f \xrightarrow{f^{-1}} x \xrightarrow{\theta} y \xrightarrow{f} fy$$

obtained by exploiting local injectivity of $f$; the above then asks that this composition of bijections should be in $\mathcal{S}(F)$ – this observation will be used silently from now on.

In concurrent games with symmetry, both games and strategies will be certain event structures with symmetry, and the display map of a strategy will have to preserve symmetry. As for plain maps of event structures, maps of event structures with symmetry may be characterized through their action on configurations and symmetries:

**Lemma 7.1.8.** Consider E and F two ess, and $f : E \to F$ a map of event structures. Then $f$ preserves symmetry iff there is a (necessarily unique) function

$$\tilde{f} : \mathcal{S}(E) \to \mathcal{S}(F)$$

commuting with dom and cod, i.e. $\text{dom} \tilde{f} = f \circ \text{dom}$ and $\text{cod} \tilde{f} = f \circ \text{cod}$.

*Proof.* Consider $\theta : x \cong_E y$. By Lemma 7.1.6, $\theta$ is an order-iso, so we get

$$\emptyset = \theta_0 \stackrel{(e_1, e'_1)}{\subset} \theta_1 \stackrel{(e_2, e'_2)}{\subset} \theta_2 \subset \dots \subset \theta_{n-1} \stackrel{(e_n, e'_n)}{\subset} \theta_n = \theta \quad (7.1)$$

by following any covering chain of x or y. By commutation with dom and cod, it is immediate by induction on i that for all $0 \le i \le n$, $\tilde{f} \theta_i = f \theta_i$; in particular $\tilde{f} \theta = f \theta$. This shows uniqueness of $\tilde{f}$ as it must be the action of $f$ on symmetries as specified in Definition 7.1.7. But this means that $f$ sends symmetries to symmetries, thus it preserves symmetry as required. $\square$

Altogether, we get a symmetry-aware version of the mapification lemma:

**Lemma 7.1.9.** Consider E, F two ess, and a function $f : \mathcal{C}(E) \to \mathcal{C}(F)$. If $f$ preserves unions, cardinality, and there is a function $\tilde{f} : \mathcal{S}(E) \to \mathcal{S}(F)$ s.t.

$$\text{dom} \tilde{f} = f \circ \text{dom}, \qquad \text{cod} \tilde{f} = f \circ \text{cod},$$

then there exists a unique map of ess $\hat{f} : E \to F$ s.t. for all $x \in \mathcal{C}(E)$, $\hat{f}(x) = f(x)$.

*Proof.* By Lemma 6.1.11, there is $\hat{f} : E \to F$ a unique map of event structures. By Lemma 7.1.8 it preserves symmetry, which concludes the proof. $\square$

Observe that by Lemma 7.1.8 the map $\tilde{f}$, if it exists, is necessarily unique as it must coincide with the action of $\hat{f}$ (the map of event structures) on symmetries as specified by Definition 7.1.7. In the sequel, when applying Lemma 7.1.9, we shall sometimes accordingly omit the definition of $\tilde{f}$, when we feel its explicit description is not helpful.
**Maps up to Symmetry.** For now, symmetry on event structures puts a new obligation on maps, which must now preserve it. We shall now see that it also provides us with a new equivalence relation on maps, which may coincide up to symmetry only:

**Definition 7.1.10.** Consider E, F ess, and f, g : E → F maps of ess.
We say that f and g are symmetric, written f ∼ g, if the composite bijection

$$f x \stackrel{f^{-1}}{\approx} x \stackrel{g}{\approx} g x$$

written $\langle f, g \rangle_x$ and obtained via local injectivity of f and g, is in $\mathcal{S}(F)$.

Symmetry between maps will be extremely important in the sequel: it allows us to identify maps that are the same only up to reindexing, which will be essential in the construction of models of linear logic. For symmetry to play that role, it must of course be preserved by all constructions on maps. In particular:

**Proposition 7.1.11.** The category ESS, equipped with symmetry on homsets, is enriched over equivalence relations. In particular, composition preserves $\sim$.

*Proof.* Straightforward, using that maps preserve symmetry. □

## 7.1.2 Saturated Games with Symmetry

There are several ways to extend concurrent games in the presence of symmetry. Though this will not be our final word, we first sketch an approach we call “saturated” or “fat” – mathematically, it is easier, but suffers from significant drawbacks.

**Games with symmetry.** The motto leading to saturated concurrent games is to simply follow the same recipe as in Section 6.1.2, but building on ESS rather than ES. Accordingly, we first simply add symmetry to Definition 6.1.3:

**Definition 7.1.12.** A game with symmetry (gws) is an ess A = (|A|, ≤_A, #_A, S(A)) with

$$\mathrm{pol}_A : |A| \to \{-, +\}$$

a polarity function such that for all $\theta : x \cong_A y$ and $a \in x$, $\mathrm{pol}_A(a) = \mathrm{pol}_A(\theta(a))$.

We are not far removed from traditional, sequential notions of games with symmetry from the literature. In particular, the above is a natural concurrent generalization of AJM games – the link can be easily made by first recovering alternating plays:

**Definition 7.1.13.** An alternating play on gws A is a sequence $s = s_1 \dots s_n$ which is:

valid: $\forall 1 \le i \le n$, $\{s_1, \dots, s_i\} \in \mathcal{C}(A)$,

non-repetitive: $\forall 1 \le i, j \le n$, $s_i = s_j \Rightarrow i = j$,

alternating: $\forall 1 \le i \le n-1$, $\mathrm{pol}_A(s_i) \ne \mathrm{pol}_A(s_{i+1})$,

negative: if $n \ge 1$, then $\mathrm{pol}_A(s_1) = -$.

We write $\downarrow\uparrow$-Plays(A) for the set of alternating plays on A.