Using these, for any $\neg\neg\text{board } A$ we may obtain strategies for the comonad structure

$$ \mathbf{der}_A : !A \vdash A, \qquad \mathbf{dig}_A : !A \vdash !!A $$

respectively called **dereliction** and **digging** after the following components in linear logic, simply by backward lifting: $\mathbf{der}_A = \mathfrak{d}_{\mathbf{der}_A}$ and $\mathbf{dig}_A = \mathfrak{d}_{\mathbf{dig}_A}$.

We shall prove that this makes $(!, \mathbf{der}, \mathbf{dig})$ a $\sim$-comonad on NTCG, but this requires us to prove a number of coherence laws. For the symmetric monoidal structure, recall that such coherence laws simply followed by equations on renamings, and concluding from functoriality of lifting (i.e. Proposition 8.1.9). However here, the coherence laws for renamings do not hold on the nose. Consider for example one of the unit laws:

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

with the corresponding diagram on renamings on the right hand side, where $?\mathbf{der}_A(i, a) = (i, \mathbf{der}_A(a)) = (i, (0, a))$. This diagram for renamings does not commute: the bottom-left path takes $(i, a)$ to $(\langle i, 0 \rangle, a)$ instead of $(i, a)$ as it should. But of course, this is no surprise: it is well-known that laws for exponentials require reindexing, and it is exactly the reason why we constructed an equivalence $\approx$ on strategies authorizing reindexings.

Note then that the diagram above does commute up to *positive symmetry*, i.e.

$$ \mathbf{dig}_A \circledot \mathbf{der}_A \sim^+ \mathrm{id}_{(\neg A)^+} $$

where recall that $\sim^+$, defined in Definition 7.2.3, formalizes that the two maps are equal up to a *positive symmetry*, i.e. reindexing of Player moves.

This property will be sufficient to establish positive isomorphisms, exploiting:

**Lemma 8.3.6.** Consider $f, f' : A \to B$ winning renamings such that $f \sim^+ f'$ (respectively, $g, g' : B^\perp \to A^\perp$ such that $g \sim^+ g'$). Then, $\mathfrak{c}_f \approx \mathfrak{c}_{f'}$ (resp. $\mathfrak{d}_g \approx \mathfrak{d}_{g'}$).

*Proof.* The positive isos are simply identity maps between the underlying ess, and commutation with the display maps up to positive symmetry is obvious. $\square$

Now, we can prove the expected comonad laws.

**Proposition 8.3.7.** We have $(!, \mathbf{der}, \mathbf{dig})$ a $\sim$-comonad on NTCG.

*Proof. Naturality.* We show naturality of $\mathbf{der}_A$. Consider $\sigma : A \vdash B$. By Lemma 8.1.8, $\mathcal{S}^+(\sigma \circ \mathbf{der}_A) \cong \mathcal{S}^+(\sigma)$ with, for $\theta \in \mathcal{S}^+(\sigma)$, $\partial(\theta) = (0, \theta_A) \vdash \theta_B$ – where $(0, \theta_A)$ stands for $\{((0, a), (0, a')) | (a, a') \in \theta_A\}$. Likewise by Proposition 7.3.1 and Lemma 7.3.14, $\mathcal{S}^+(\mathbf{der}_B \circledot !\sigma)$ comprises matching pairs of $\theta'^{!\sigma} \in \mathcal{S}^+(!\sigma)$ and $\theta_B \parallel \theta_B \in \mathcal{S}^+(\mathfrak{c}_B)$, where the latter displays to $(0, \theta_B) \vdash \theta_B$. So by matching, $\theta'^{!\sigma}$ spans only one copy of index 0, and thus must display to some $(0, \theta_A) \vdash (0, \theta_B)$. From this,
the required order-isomorphism follows easily.

Next, we show naturality of $\mathbf{dig}_A$. First, symmetries in $\mathcal{S}^+(!!\sigma \odot \mathbf{dig}_A)$ are somewhat hard to describe: by Lemma 8.1.8, they correspond to those

$$ \theta : [[x^{i,j} | j \in J_i] | i \in I] \cong [[y^{k,l} | l \in L_k] | k \in K] \quad (8.6) $$

given by (1) a bijection $\pi : I \cong K$; (2) for each $i \in I$, a bijection $\pi_i : J_i \cong L_{\pi(i)}$; and
(3) for each $i \in I, j \in J_i$, a symmetry $\theta^{i,j} : x^{i,j} \cong_{\sigma} y^{\pi(i),\pi_i(j)}$. This is displayed to

$$ \begin{aligned} \theta_{1A} : & \quad [x_A^{i,j} | \langle i, j \rangle \in X] & \cong & \quad [y_A^{k,l} | \langle k, j \rangle \in Y] \\ \theta_{\mathit{!!B}} : & \quad [[x_B^{i,j} | j \in J_i] | i \in I] & \cong & \quad [[y_B^{k,l} | l \in L_k] | k \in K] \end{aligned} $$

where $X$ comprises those $\langle i, j \rangle$ such that $i \in I$ and $j \in J_i$ and $x_A^{i,j}$ is non-empty, and likewise for $Y$. For the other side of the naturality diagram, by Proposition 7.3.1 and Lemma 7.3.14, symmetries in $\mathcal{S}^+(\mathbf{dig}_B \odot !\sigma)$ correspond to pairs

$$ \begin{aligned} \theta^{!\sigma} : & \quad [x^m | m \in X] & \cong & \quad [y^n | n \in Y] \\ \theta^{\mathit{!!B}} : & \quad [[x^{i,j} | i \in I] | j \in J_i] & \cong & \quad [[y^{k,l} | k \in K] | l \in L_k] \end{aligned} $$

which are matching, implying that $X$ comprises those $\langle i, j \rangle$ such that $i \in I$ and $j \in J_i$;
$Y$ comprises those $\langle k, l \rangle$ such that $k \in K$ and $l \in L_k$, and $\theta^{!\sigma}$ first follows a bijection
$\pi : I \cong K$ and for each $i \in I$ a bijection $J_i \cong K_{\pi(i)}$. This means that equivalently,

$$ \theta^{!\sigma} : [[x^{\langle i,j \rangle} | j \in J_i] | i \in I] \cong [[y^{\langle k,l \rangle} | l \in L_k] | k \in K] $$

a symmetry in $!!\sigma$. This matches (8.6); this correspondence is an order-iso compatible with display maps so that $!!\sigma \odot \mathbf{dig}_A \cong \mathbf{dig}_B \odot !\sigma$ as required by Corollary 7.2.13.

*Coherence*. First, we define renamings:

$$ ?\mathit{der}_A : (!A)^{\perp} \to (!A)^{\perp}, \qquad ?\mathit{dig}_A : (!A)^{\perp} \to (!!A)^{\perp} $$

simply copying the index for the outer !. Now, Proposition 8.3.4 (in particular, preservation of copycat) provides us with isomorphisms of ess

$$ !\mathcal{C}_A \cong \mathcal{C}_{!A}, \qquad !\mathcal{C}_{!A} \cong \mathcal{C}_{!!A} $$

which simply by verifying compatibility with display maps, yield positive isomorphisms

$$ !\mathcal{D}_{\mathit{der}_A} \approx \mathcal{D}_{?\mathit{der}_A}, \qquad !\mathcal{D}_{\mathit{dig}_A} \approx \mathcal{D}_{?\mathit{dig}_A}, \quad (8.7) $$

so that finally, noting the positive symmetries between renamings

$$ \mathbf{dig}_A \circled{\mathit{?der}}_A \sim^{+} \mathbf{id} $$

$$ \mathbf{dig}_A \circled{\mathit{der}}_{!A} \sim^{+} \mathbf{id} $$

$$ \mathbf{dig}_A \circled{\mathit{dig}}_{!A} \sim^{+} \mathbf{dig}_A \circ \mathbf{dig}_{!A} $$

we get the coherence laws up to ≈ by (8.7), Lemma 8.3.6 and Proposition 8.1.9. □
This structure lets us define the particularly important following operation. If A and B are strict --boards and $\sigma : !A \vdash B$, then its **promotion** is

$$ \sigma' : !A \vdash !B \qquad (8.8) $$

defined as $\sigma' = !\langle\sigma\rangle \odot \text{dig}_A$, involving both digging and the functorial action of !. Promotion may be taken as a primitive, letting us state:

**Corollary 8.3.8.** Consider the $\sim$-functor $! : \text{NTCG}_s \to \text{NTCG}$, together with: (1) the dereliction strategy $\text{der}_A : !A \vdash A$ for strict $A$; and (2) the promotion operation $\sigma' : !A \vdash !B$ for all $\sigma : !A \vdash B$ with $A$ and $B$ strict.

This yields a relative $\sim$-comonad, with respect to the inclusion $\text{NTCG}_s \subseteq \text{NTCG}$.

*Proof.* Straightforward. $\square$

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

But since we have a regular comonad, why emphasize this less standard relative comonad structure? Well, because as we shall see in Section 10.4, the comonad structure is not preserved by the collapse to the relational model: we shall see that the interplay between the collapse and !A only works well when A is strict.

**Seely isomorphisms.** First, we have an equality $!\Gamma = \mathbf{1}$, so the corresponding isomorphism is realized by the identity. We need one final isomorphism

$$ \mathbf{mon}_{A,B} : !A \otimes !B \cong !\langle(A\&B)\rangle, $$

which we shall obtain via the following renamings:

**Lemma 8.3.9.** Consider A, B two strict --boards. Then, we have winning renamings:

$$ \mathbf{mon}_{A,B} : \begin{array}{rcl} !\langle(A\&B)\rangle^{\perp} & \to & !\langle A \otimes !B \rangle^{\perp} \\ (i, (j, m)) & \mapsto & (j, (i, m)) \end{array} $$

$$ \mathbf{mon}^*_{A,B} : \begin{array}{rcl} !\langle A \otimes !B \rangle^{\perp} & \to & !\langle (A\&B) \rangle^{\perp} \\ (i, (j, m)) & \mapsto & (\langle i, j \rangle, (i, m)) \end{array} $$

satisfying $\mathbf{mon}_{A,B} \circ \mathbf{mon}^*_{A,B} \sim^+ \text{id}$ and $\mathbf{mon}^*_{A,B} \circ \mathbf{mon}_{A,B} \sim^+ \text{id}$.

*Proof.* Straightforward. $\square$

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

As expected, the required isomorphism $\mathbf{mon}_{A,B}$ is obtained by backward lifting, i.e.

$$ \mathbf{mon}_{A,B} = \mathfrak{D}_{\mathbf{mon}_{A,B}}, $$

$$ \mathbf{mon}^{-1}_{A,B} = \mathfrak{D}_{\mathbf{mon}^*_{A,B}}, $$

inverses up to positive iso as follows from Lemmas 8.3.9, 8.3.6 and Proposition 8.1.9.

Note that these strategies cannot be defined via forward lifting, as neither $\mathbf{mon}_{A,B}$ nor $\mathbf{mon}^*_{A,B}$ would be valid renamings if typed without the $(-)^{\perp}$, both failing *receptive*.
*Proof.* Via Lemma 8.3.10, it remains to show that the following diagram commutes

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

up to positive symmetry. We first observe that considering the winning renaming

$$ \mu_{\Gamma} : \begin{array}{ccc} !\langle\Gamma\&\Gamma\rangle^{\perp} & \to & !\langle\Gamma\rangle^{\perp} \\ (i, (j, m)) & \mapsto & (i, (0, m)), \end{array} $$

we have $!\langle\mathrm{der}_{\Gamma}, \mathrm{der}_{\Gamma}\rangle \approx \mathfrak{D}_{\mu_{\Gamma}}$, as is established by a – by now routine – analysis of symmetries of $!\langle\mathrm{der}_{\Gamma}, \mathrm{der}_{\Gamma}\rangle$. The diagram then follows from Proposition 8.1.9, Lemma 8.3.6 and a direct computation of the composition of the renamings involved. $\square$

We may finally conclude the main result of this chapter:

**Theorem 8.3.12.** *There is NTCG, a relative Seely $\sim$-category.*

*Proof.* The only components which were not detailed are naturality of $\mathrm{mon}_{A,B}$, and the coherence diagrams making $!(-)$ a strong symmetric monoidal $\sim$-functor. All these follow from Proposition 8.1.9 via a now routine methodology; we omit details. $\square$

And of course (see Appendix A.1 for the construction of the Kleisli category):

**Corollary 8.3.13.** *The Kleisli $\sim$-category $\mathbf{NTCG}_1$ is cartesian closed.*

In the sequel, we write $\circled_1$ for Kleisli composition, i.e. composition in $\mathbf{NTCG}_1$.

### 8.3.2 Recursion

The last piece of structure that we shall construct in $\mathbf{NTCG}$ is the interpretation of the fixpoint combinator, used to interpret recursion. Following the standard denotational semantics practice, this infinite strategy will be obtained as a least fixed point with respect to a partial order on concrete strategies.

First, we introduce this partial order:

**Definition 8.3.14.** *Consider A a board, and $\sigma, \tau$: A winning strategies.*

We write $\sigma \triangleleft \tau$ if $\mathcal{C}(\sigma) \subseteq \mathcal{C}(\tau)$ – so in particular $|\sigma| \subseteq |\tau|$, and additionally:

(1) for all $s_1, s_2 \in \sigma$, $s_1 \leq_{\sigma} s_2$ iff $s_1 \leq_{\tau} s_2$,

(2) for all $s_1, s_2 \in \sigma$, $s_1 \#_{\sigma} s_2$ iff $s_1 \#_{\tau} s_2$,

(3) for all $x, y \in \mathcal{C}(\sigma)$ and bijection $\theta: x \simeq y$, we have $\theta \in \mathcal{S}(\sigma)$ iff $\theta \in \mathcal{S}(\tau)$,

(4) for all $s \in \sigma$, $\partial_{\sigma}(s) = \partial_{\tau}(s)$,

i.e. all components compatible with the inclusion.
Strategies on A, ordered by $\triangleleft$, form a directed complete partial order, with respect to which all operations on strategies are easily shown to be continuous. We have:

**Proposition 8.3.15.** Consider A a board, and D a directed set of strategies on A.
Then D has a least fixed point for $\triangleleft$, written $\vee D$, and satisfying:

$$ \mathscr{C}^+(\vee D) = \bigcup_{\sigma \in D} \mathscr{C}^+(\sigma), \qquad \mathscr{S}^+(\vee D) = \bigcup_{\sigma \in D} \mathscr{S}^+(\sigma). $$

Moreover, if every $\sigma \in D$ is winning, then so is $\vee D : A$.

*Proof.* We set $|\vee D| = \bigcup_{\sigma \in D} |\sigma|$, and take the union as well for all other components. All verifications are straightforward, and omitted. $\square$

For any $\neg$-boards A and B this turns $\mathbf{NTCG}(A \vdash B)$ into a dcpo. We have:

**Lemma 8.3.16.** The following operations on strategies are continuous:

$$ \neg \circled : \mathbf{NTCG}(B \vdash C) \times \mathbf{NTCG}(A \vdash B) \rightarrow \mathbf{NTCG}(A \vdash C) $$

$$ \neg \otimes \textbf{ : } \mathbf{NTCG}(A \vdash B) \times \mathbf{NTCG}(C \vdash D) \rightarrow \mathbf{NTCG}(A \otimes C \vdash B \otimes D) $$

$$ \langle -, - \rangle : \mathbf{NTCG}(\Gamma \vdash A) \times \mathbf{NTCG}(\Gamma \vdash B) \rightarrow \mathbf{NTCG}(\Gamma \vdash A \& B) $$

$$ (-)! : \mathbf{NTCG}(!\Gamma \vdash A) \rightarrow \mathbf{NTCG}(!\Gamma \vdash !A) $$

*Proof.* Straightforward. $\square$

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

The plan is then to follow the standard denotational semantics route, and define the recursion combinator via Kleene's fixed point theorem, as the least fixed point of a well-chosen functional continuous via the proposition above.

For that, we must deal with a minor inconvenience: Kleene's fixed point theorem applies to continuous functionals over a dcpo with a least element, but the dcpo $\mathbf{NTCG}(A)$ of winning strategies over a board *A* does not in general have a least element. Indeed, strategies on *A* cannot in general be empty, as they must have – by receptivity – events matching the negative minimal events of *A*. But “matching” is loose: they are free to name those events arbitrarily. We solve this as in [Castellan et al., 2019]: we choose one minimal $\perp_A : A$, serving as the canonical least element. Then for any $\sigma : A$, we pick an isomorphic $\sigma \approx \sigma^b : A$ s.t. $\perp_A \triangleleft \sigma^b$, obtained by renaming minimal events. We write $D_A$ for the pointed dcpo of strategies above $\perp_A$. For this new operation:

**Lemma 8.3.17.** For any board A, the following operation is continuous:

$$ (-)^b : \mathbf{NTCG}(A) \rightarrow D_A. $$

*Proof.* Straightforward. $\square$

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

As all operations involved are continuous, for any strict $\neg$-board A we have

$$ F : D_{!\vdash(A \to A)} \to A \rightarrow D_{!\vdash(A \to A)} \to A $$

$$ \sigma \mapsto (\lambda f^{A \to A} . f(\sigma f))^b, $$
continuous, written in $\lambda$-calculus syntax relying on the constructions on strategies corresponding to the cartesian closed structure of $\mathbf{NTCG}_!$ [Lambek and Scott, 1988]. Here, we use $A \to B$ as a notation for $!A \dashv A$. Hence by Kleene's fixpoint theorem,

$$ \mathcal{Y}_A = \bigvee_{n \in \mathbb{N}} F^n(\perp) \in \mathbf{NTCG}_!(\mathbb{T}, (A \to A) \to A) $$

is a least fixpoint of $F$. Finally, in the presence of a strict $\dashv$-board $\Gamma$ serving as context, we set $\mathcal{Y}_{\Gamma,A} = \mathcal{Y}_A \circled{!} e_\Gamma$ where $e_\Gamma \in \mathbf{NTCG}_!(\Gamma, \mathbb{T})$ is the terminal morphism, yielding

$$ \mathcal{Y}_{\Gamma,A} \in \mathbf{NTCG}_!(\Gamma, !(!A \dashv A) \dashv A) \qquad (8.9) $$

which will provide the interpretation of recursion throughout this monograph.

## 8.4 History and Related Work

**Compact Closed Category.** Following Joyal's compact closed category of Conway games [Joyal, 1977], it is certainly expected that a category of unpolarized games should be compact closed – a notable exception to that is of course Blass games [Blass, 1992] which famously do not form a category. A detailed analysis of this so-called “Blass problem” in the context of Conway games may be found in [Melliès, 2004b].

For our particular technical setting of concurrent games on event structures, the compact closed structure was first described in [Castellan et al., 2017a] without symmetry, and extended to thin concurrent games in [Castellan et al., 2019].

**Seely Category.** Seely categories is a convenient categorical axiomatization of models of intuitionistic linear logic, in the presence of a product. Many categories of negative games form Seely categories, starting with simple games [Hyland, 1997] with respect to several choices of exponential modalities.

In the original presentation of thin concurrent games (first in conference version in [Castellan et al., 2015] then detailed in [Castellan et al., 2019]), we did not construct a model of intuitionistic linear logic. Indeed, we opted to construct a category called Concurrent Hyland-Ong games, with objects exactly the same arenas as in traditional Hyland-Ong games. We wanted a conservative extension of HO games: the appeal was to make it easier to adapt and extend the developments that led to their versatility and impact – and in particular, concepts such as justifiers and conditions on strategies such as innocence. Technically, this was done by building a tcg from any Hyland-Ong arena via a variant of the resource modality (inspired by [Harmer et al., 2007]) performing duplications not just at the root, but deep within the arena.

In developing probabilistic concurrent games in [Castellan et al., 2018b], we reverted to an AJM-style $!$, which made it easier to link with the weighted relational model. But then we (re-)discovered (Melliès, at least, was certainly aware of this from his work in asynchronous games) that justifiers, and in general the necessary ingredients to the Hyland-Ong machinery, were already available in concurrent games even with an AJM-style exponential! This is one of the advantages of the causal setting, as opposed to
traditional AJM games. In retrospect, this makes *Concurrent Hyland-Ong Games* mis-
guided: they suffer from the same defect as traditional Hyland-Ong games (lacking a
linear decomposition), while working in the Kleisli category of a Seely category of thin
concurrent games gives you the best of both AJM and HO worlds.

Concerning *relative* Seely category: from **TCG** one can get an actual Seely category [Castellan and Clairambault, 2021]. But the general linear arrow construction is awkward, and the interest of the added expressiveness is unclear for semantic purposes. Finally, the full Seely category structure lacks a clean connection with relational semantics. *Relative* Seely categories give a good compromise for semantics of call-by-name.

**Winning Strategies.** Finally, the *payoff* mechanism and winning strategies we use here are an adaptation of similar mechanisms in [Melliès, 2005] (with a later refinement in [Melliès and Tabareau, 2007]) where they serve essentially the same purpose as here: they cope for the otherwise inherently *affine* nature of game semantics, making strategies more linear and identifying the *stopping* configurations of games, those corresponding points of the web in the relational model. Note that we first adapted this mechanism to concurrent games on event structures in [Clairambault and de Visme, 2020].

It might be unclear to the reader why a mechanism making strategies *linear* is appropriate for a model intended for the languages considered in this monograph, which are non-linear and include full recursion and divergence. Firstly, the term *linear* is not really adequate; we should rather say “following the linearity constraints”, which are made more liberal by using the exponential. Secondly, our notion of winningness does not force termination, it only constrains resource usage of successful terminating executions, if they exist. More precisely, our (new) restriction of winningness to *+covered* configurations has the subtle effect to prevent from forcing Player to respond in diverging branches, say *i.e.* a diverging boolean.
# Part III

## Disentangling Parallelism and State
Introduction to Part III

<figure><img src="image_135.png" /><figcaption>Figure 8.5: The Inception of Parallel Innocence</figcaption></figure>
Now comes the core of this monograph: from NTCG we build a cartesian closed category $\rightarrow-Strat$ in which we disentangle parallelism and state, as in Section 1.7.

More precisely, we first show that $\rightarrow-Strat$ is an intensionally fully abstract denotational model for $IA_\llcorner$, by providing an interpretation-preserving functor

$$ \mathcal{O}-\text{Unf} : \rightarrow-Strat \rightarrow \mathcal{O}-\text{Strat} $$

to non-alternating play-based strategies as described in Chapter 5. The category $\rightarrow-Strat$ is close to NTCG but is not exactly that, for two reasons: firstly, because NTCG and $\mathcal{O}-Strat$ do not have the same objects, and there is no easy way to reconstruct an arena in the sense of Hyland-Ong game from a board – so the objects of $\rightarrow-Strat$ will remember both. Secondly, nothing in NTCG guarantees the logical well-bracketing used in $\mathcal{O}-Strat$, so that must be reimposed as well. This is detailed in Chapter 9.

Once $\rightarrow-Strat$ is constructed along with its interpretation of $IA_\llcorner$ and its unfolding to $\mathcal{O}-Strat$, we set to build our two conditions on strategies, sequentiality and globularity, respectively banning parallelism and state. We first focus on globularity. The heart of globularity is parallel innocence, a condition that removes state by banning certain causal patterns that are deemed inherently stateful. Parallel innocence can be regarded as a conservative extension of traditional Hyland-Ong innocence, in the sense that paired with sequentiality, we obtain a category (equivalent to) $\downarrow\uparrow-\text{Inn}$. As a conceptually important aside, we show that parallel innocence allows a simple functor to the relational model, compatibly with the structure of a model of intuitionistic linear logic. Finally we introduce globularity, which refines parallel innocence by adding a constraint with respect to Questions and Answers. This is detailed in Chapter 10.

Next, we focus on sequentiality – we show that in the presence of sequentiality, $\mathcal{O}-\text{Unf}$ can be refined to an alternating unfolding, an interpretation-preserving

$$ \downarrow\uparrow-\text{Unf} : \rightarrow-\text{Seq} \rightarrow \downarrow\uparrow-\text{Strat} $$

which entails that $\rightarrow-\text{Seq}$ is intensionally fully abstract for $IA$. We also show that in combination with globularity, $\downarrow\uparrow-\text{Unf}$ yields an interpretation-preserving functor

$$ \downarrow\uparrow-\text{Unf} : \rightarrow-\text{SeqGlob} \rightarrow \downarrow\uparrow-\text{InnWB} $$

proving $\rightarrow-\text{SeqGlob}$ intensionally fully abstract for PCF. This appears in Chapter 11.

Finally, it remains to establish that $\rightarrow-\text{Glob}$ is fully abstract for $PCF_\llcorner$. This is proved by an elaborate finite definability argument. To bring concurrent strategies closer to syntax, we must first show that globular strategies enjoy a so-called *meager form*, akin to the forest of *P*-views for traditional sequential innocence. This meager form provides the appropriate notion of *finiteness* or *size* of a globular strategy, on which the definability argument operates. We then show a *factorization* result, to the effect that any globular strategy factors into what is essentially a pure $\lambda$-term, and a globular strategy on a *first-order* arena. It remains to define those first-order strategies, which we do – up to the equivalence generated by the relational collapse. This is detailed in Chapter 12.

Altogether, this disentangles parallelism and state.
# Chapter 9

## The Causal Semantics of IA$_{//}$ and its Unfolding

The purpose of this chapter is to construct $\rightarrow$-Strat – the causal analogue of $\mathcal{C}$-Strat, the fully abstract model of IA$_{//}$ – and describe the interpretation of IA$_{//}$.

The outline is as follows. In Section 9.1, we will first describe the interpretation of IA$_{//}$ in NTCG$_1$ as constructed in Corollary 8.3.13. In Section 9.2, we shall refine NTCG$_1$ into $\rightarrow$-Strat, adding a missing condition so that it unfolds to $\mathcal{C}$-Strat. In Section 9.3, we detail the unfolding to $\mathcal{C}$-Strat and prove full abstraction for IA$_{//}$.

### 9.1 Interpretation of IA$_{//}$

We rely on the cartesian closed $\sim$-category NTCG$_1$ from Part II (see Corollary 8.3.13). Thus, building on the standard interpretation of the simply-typed $\lambda$-calculus, it remains to give an interpretation to all basic datatypes and primitives of IA$_{//}$.

#### 9.1.1 Interpretation of PCF$_{//}$

**Interpretation of types.** The cartesian closed structure of NTCG$_1$ fixes the interpretation of the arrow constructor, which we must complete with an interpretation for the ground types $B, N$ and $U$. Earlier we have already provided $\neg$-boards $B, N$ and $U$ for those ground types, with for instance, for the booleans, the $\neg$-board: with for instance

$$B = \begin{array}{c} q^{-} \\ \vdots \\ t^{+} \sim\!\!\!\sim\!\!\!\sim\!\!\! f^{+} \end{array}$$

In the sequel, we shall refer to these as the **small** boards for ground types. The small ground boards are very natural, but in tension with the fact that in the play-based games
<figure><img src="image_136.png" /><figcaption>Figure 9.1: Configurations of basic strategies for PCF</figcaption></figure>

of Part I, a question may be answered multiple times (possibly with the same answer). So as to avoid a cumbersome mismatch<fnref n="1" />, we introduce an alternative interpretation of base types, where all possible answers are replicated. This is handled by:

**Definition 9.1.1.** Consider $V = \{a, b, c, \dots\}$ an at most countable set of values. We define the strict --board ground($V$) as having essp:

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

with symmetries all bijections only changing copy indices. All symmetries are positive; negative symmetries are restricted to identities. Finally, the payoff function is:

$$ \begin{array}{rcl} \kappa : & \mathscr{C}(\text{ground}(V)) & \to \{-1, 0, +1\} \\ & \emptyset & \mapsto +1 \\ & \{\mathbf{q}^{-}, v_{i}^{+}\} & \mapsto 0 \\ & x & \mapsto -1 \end{array} \quad \text{otherwise} $$

Each value has countably many copies, with no conflict. Thus, when playing a value, a strategy must provide an accompanying copy index. Player may answer *several times*, either with the same or different values, but this is banned from strategies by the *winning mechanism*. However, Opponent may still answer several times (if the board appears

<footnote n="1">¹In non-alternating games, (logical) well-bracketing corrects this. The mismatch occurs only in the upcoming alternating unfolding, as in the alternating case well-bracketing is on strategies rather than on plays.</footnote>
<figure><img src="image_138.png" /><figcaption>Figure 9.2: Basic interpretation clauses</figcaption></figure>

<caption>Figure 9.3: Strategy for pred</caption>

in contravariant position) so that the model conveys information about the behaviour of programs under a context that answers several times.

We define the **large** ground boards as $\mathbf{U} = \text{ground}(\{\checkmark\})$, $\mathbf{B} = \text{ground}(\{\tt t, ff\})$ and $\mathbf{N} = \text{ground}(\mathbb{N})$ (the set of all natural numbers). As explained above, this extends to all *types* of PCF by setting $\llbracket A \to B \rrbracket = \checkmark \llbracket A \rrbracket \to \llbracket B \rrbracket$ using the constructions from Section 8.2.2, yielding for any type $A$ a strict $--\text{board}$ $\llbracket A \rrbracket$. Finally, a *context* $\Gamma = x_1 : A_1, \dots, x_n : A_n$ is interpreted as $\llbracket \Gamma \rrbracket = \bigoplus_{1 \le i \le n} \llbracket A_i \rrbracket$. We insist that $\text{IA}_//$ can be interpreted with the ground types set as $\mathbf{U}, \mathbf{B}$ and $\mathbf{N}$; or as $\mathbf{U}, \mathbf{B}$ and $\mathbf{N}$. We set the large boards as our default choice so as to match with non-alternating games, but we may sometimes refer to the small as well, because it allows for more succinct examples.

**Interpretation of terms.** A term $\Gamma \vdash M : A$ of PCF is interpreted as a strategy

$$ \llbracket M \rrbracket \in \text{NTCG}_1(\llbracket \Gamma \rrbracket, \llbracket A \rrbracket). $$

We invoke the cartesian closed structure of $\text{NTCG}_1$ – writing $\odot_i$ for Kleisli composition, and $\Lambda^!$ for Kleisli currying. We skip the details of the interpretation of the $\lambda$-calculus combinators, which follows the standard lines of the interpretation of the simply-typed $\lambda$-calculus in a cartesian closed category [Lambek and Scott, 1988].

We must specify strategies for the term constructions that PCF adds to the simply-typed $\lambda$-calculus. For constants, we set $\llbracket \text{skip} \rrbracket : \mathbf{U}, \llbracket \tt t \rrbracket : \mathbf{B}, \llbracket \text{ff} \rrbracket : \mathbf{B}$ and $\llbracket n \rrbracket : \mathbf{N}$ as the obvious strategies replying immediately the corresponding value (with copy index 0). For all other combinators, the interpretation is in Figure 9.2. The strategies used are described in Figures 9.1, 9.3 and 9.4. The notation we employ is symbolic: the strategies comprise a branch for each instantiation of the copy index parameters $i, j$ and the value parameters $v, w, \dots$. For instance, the strategy if has as configuration that shown in Figure 9.5 as nothing prevents Opponent from answering a question multiple times – this is in contrast with $\mathcal{O}$-Strat, where plays were always assumed to be well-bracketed. Recall also from Section 8.3.1 that $\langle -, \dots, - \rangle : \mathbb{N}^n \simeq \mathbb{N}$ denotes any bijection. Strategies specified symbolically as above carry a specific choice determining the copy indices of Player moves from those of Opponent moves. This choice does not matter up to positive isomorphism; the only thing that matters is that there is never any collision so that the display maps do satisfy the conditions of a concurrent strategy.
<figure><img src="image_139.png" /><figcaption>Figure 9.4: Typical configuration of let</figcaption></figure>

<figure><img src="image_140.png" /><figcaption>Figure 9.5: Example of a configuration of if</figcaption></figure>

<figure><img src="image_141.png" /><figcaption>Figure 9.6: Typical configuration of plet</figcaption></figure>
<figure><img src="image_142.png" /><figcaption>Figure 9.7: $V_w$</figcaption></figure>

<figure><img src="image_143.png" /><figcaption>Figure 9.8: $V_r$</figcaption></figure>

<figure><img src="image_144.png" /><figcaption>Figure 9.9: S</figcaption></figure>

For let, the strategy implements a memoization mechanism: it evaluates on X first obtaining a value v, which it feeds to the function argument each call. The interpretation is completed with $[[\mathcal{Y}_A M]] = \mathcal{Y}_{\Gamma,A} \circ_! [[M]]$ for $\Gamma \vdash M : A \to A$, using (8.9).

**Semantics of parallelism.** This is extended to PCF simply by adding the clause

$$[[\Gamma \vdash \text{let } \begin{pmatrix} x_1 = N_1 \\ x_2 = N_2 \end{pmatrix} \text{ in } M : \mathcal{V}]] = \text{plet}_{X,Y} \circ_! \langle [[N_1]], [[N_2]], \Lambda^1(\Lambda^1([[M])) \rangle$$

via the strategy $\text{plet}_{X,Y}$ with typical configurations as presented in Figure 9.6. It is interesting to compare this definition with the non-alternating plays in Figure 5.11: the diagram avoids listing all interleavings, hence staying much more faithful to the intuition behind the behaviour of this primitive.

## 9.1.2 Semantics of state

The interpretation of references and semaphores closely follows that in (↓-Strat and) ⊢-Strat. For the types V and S, we first introduce strict —boards $V_w, V_r$ and S as

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

with moves renamed as illustrated in Figures 9.7 (where in $V_w$, all write requests are in pairwise conflict), 9.8 and 9.9. We set $V = V_w \& V_r$, and $[[V]] = V$, $[[S]] = S$.

**Stateless primitives.** As in Section 4.2.2, only the interpretation of the primitives newref and newsem is effectful – other primitives only send various queries to references and semaphores, and as such are simple innocent strategies.

Accordingly, we set the interpretation of memory and semaphore accesses as:

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

using the strategies of Figures 9.10, 9.11, 9.12, and 9.13. Finally, we set
<figure><img src="image_145.png" /><figcaption>Figure 9.10: assign</figcaption></figure>

<caption>Figure 9.11: deref</caption>

<caption>Figure 9.12: grab</caption>

<caption>Figure 9.13: release</caption>

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

where $[[M]]$ is $[[M]]$ applied to the constant strategy $n$ (using the cartesian closed structure of $\mathbf{NTCG}_1$). It remains to define the semantics of **newref** and **newsem**.

**Creation of reference and semaphores.** For **newref** and **newsem**, again we follow in the footsteps of Section 4.2.2. However, in contrast with respect to Section 4.2.2, we must manage copy indices so as to satisfy the constraints of concurrent prestrategies.

For each $I \subseteq_f \mathbb{N}$ and $n \in \mathbb{N}$, we define languages of infinite words on $!V$ and $!S$:

$$ \mathbf{cell}_n^I = \mathbf{r}_i^- \cdot n_0^+ \cdot \mathbf{cell}_n^{I \uplus \{i\}} | \mathbf{wk}_i^- \cdot \mathbf{\checkmark}_0^+ \cdot \mathbf{cell}_k^{I \uplus \{i\}} \quad (i \notin I) $$

$$ \mathbf{lock}_0^I = \mathbf{g}_i^- \cdot \mathbf{\checkmark}_0^+ \cdot \mathbf{lock}_1^{I \uplus \{i\}} | \mathbf{r}_i^- \quad (i \notin I) $$

$$ \mathbf{lock}_n^I = \mathbf{g}_i^- | \mathbf{r}_i^- \cdot \mathbf{\checkmark}_0^+ \cdot \mathbf{lock}_0^{I \uplus \{i\}} \quad (i \notin I, n > 0) $$

where symbols are moves in $!V$ and $!S$ respectively, separated via $\cdot$ for readability. Note that positive moves should really include two copy indices: one for the outer bang, one for the value – we show only the latter, the former is always the same as the previous negative move. Here, $I \subseteq_f \mathbb{N}$ collects the copy indices already used so that each new copy index is fresh, ensuring that no single move appears twice. We set $\mathbf{cell}_n$ as (the prefix language of) $\mathbf{cell}_n^I$ and $\mathbf{lock}_n$ as (the prefix language of) $\mathbf{lock}_n^I$. They may be viewed as event structures by setting events to be finite words, causality the prefix ordering, and setting any incomparable words to be in conflict. The two display maps

$$ \partial_{\mathbf{cell}} : |\mathbf{cell}| \rightarrow !V \qquad \partial_{\mathbf{lock}} : |\mathbf{lock}| \rightarrow !S \\ sa \mapsto a \qquad sa \mapsto a $$

only keep the last move. As configurations of cell and lock are sets of prefixes of a branch which is an alternating play in $!V$ or $!S$, we set $\mathcal{S}(\mathbf{cell}_n)$ to comprise those bijections induced by plays $s_1 \cong_A s_2$ symmetric on $A$ (for $A$ being $!V$ or $!S$, see Definition 7.1.14).

Altogether, we get:

**Proposition 9.1.2.** We have two concurrent prestrategies $\mathbf{cell} : !V$ and $\mathbf{lock} : !S$.
<figure><img src="image_146.png" /><figcaption>Figure 9.14: Beginning of cell$_0$</figcaption></figure>

<figure><img src="image_147.png" /><figcaption>Figure 9.15: Beginning of lock$_0$</figcaption></figure>

We display a few early moves, of cell in Figure 9.14 and lock in Figure 9.15, with the convention that all moves in the same row are in pairwise conflict. We observe that both prestrategies fail courtesy: the immediate causal link $\check{\sigma}_0^+ \rightarrow \mathbf{r}_8^-$, for instance, would be illegal for a strategy. Note that for semaphores, in Figure 9.15, trailing Opponent moves are indeed maximal, Player has no response – an attempt to release a lock that has not been grabbed, or to grab a lock that has not been released, triggers no response.

Note that although cell : !V is only a prestrategy and not a strategy, we have:

**Proposition 9.1.3.** Consider $\sigma : !V \vdash A$ and $\tau : !S \vdash A$.

Then, the two prestrategies $\sigma \odot \text{cell} : A$ and $\tau \odot \text{lock} : A$ are strategies.

*Proof.* We show it for cell, the proof for lock is the same. First, while cell is not courteous, it is *span-courteous* in the sense of Definition 7.3.10. Thus, by Proposition 6.2.22, $\sigma \odot \text{cell}$ is well-defined and a prestrategy. It remains to prove that $\sigma \odot \text{cell}$ is receptive and courteous. But by Proposition 6.4.12, that is the case if and only if it is invariant (up to strong iso) under composition with copycat. Thus we compute:

$$ \begin{aligned} \mathfrak{c}_A \odot (\sigma \odot \text{cell}) &\cong (\mathfrak{c}_A \odot \sigma) \odot \text{cell} \\ &\cong \sigma \odot \text{cell}, \end{aligned} $$

so by Proposition 6.4.12, $\sigma \odot \text{cell}$ is receptive and courteous as required. $\square$

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

It is then easy to deduce the following fact:

**Corollary 9.1.4.** Consider $\sigma \in \text{NTCG}(V, A)$ and $\tau \in \text{NTCG}(S, A)$.

Then, $\sigma \odot \text{cell} \in \text{NTCG}(1, A)$ and $\tau \odot \text{lock} \in \text{NTCG}(1, A)$.

*Proof.* Again, we prove it for $\sigma \odot \text{cell}$. According to Proposition 8.2.15, we must show that it is *negative* and *winning* in the sense of Definition 8.2.14.

Negative is trivial as A is negative. For winning, take $x^\sigma \odot x^{\text{cell}} \in \mathscr{C}^+(\sigma \odot \text{cell})$. Then, $x^\sigma \in \mathscr{C}(\sigma)$ must be +-maximal, otherwise it immediately contradicts +-maximality of $x^\sigma \odot x^{\text{cell}}$ or minimality of $(x^{\text{cell}}, x^\sigma)$ in the sense of Proposition 7.3.9. Now in $x^{\text{cell}}$,
maximal events (if any exists) must be positive, or contradict minimality of $(x^{\text{cell}}, x^{\sigma})$.
But thus $\kappa_{!V}(x_{!V}^{\text{cell}}) = 0$, hence $\kappa_A(x_A^{\sigma}) \ge 0$ follows by $\sigma$ winning. $\square$

We now complete the interpretation. Consider $\Gamma, x : \forall \vdash M : \mathcal{X}$ with

$$[[M]] \in \mathbf{NTCG}_1(\Gamma \& V, \mathcal{X})$$

omitting some brackets. Using the cartesian closed structure of $\mathbf{NTCG}_1$, we consider

$$\Lambda_I^!([[M]]) \in \mathbf{NTCG}(!V, !\Gamma \dashv \mathcal{X})$$

which we compose with the memory cell. Summing up, for references and semaphores,

$$[[\mathbf{newref} x := n \text{ in } M]] = \Lambda_I^{!-1}(\Lambda_I^!([[M]] \circ \text{cell}_n)) \in \mathbf{NTCG}_1(\Gamma, \mathcal{X})$$

$$[[\mathbf{newsem} x := n \text{ in } M]] = \Lambda_I^{!-1}(\Lambda_I^!([[M]] \circ \text{lock}_n)) \in \mathbf{NTCG}_1(\Gamma, \mathcal{X}).$$

concluding the interpretation of $IA_\llcorner$ in $\mathbf{NTCG}$. It shall follow from this chapter that:

**Theorem 9.1.5.** $\mathbf{NTCG}_1$ is adequate for $\mathbf{IA}_\llcorner$.

*Proof.* A consequence of the adequacy of $\mathcal{O}$-Strat for $\mathbf{IA}_\llcorner$ with Theorem 9.3.9. $\square$

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

### 9.1.3 Discussion on the Interpretation

What does the interpretation of $IA_\llcorner$ programs as concurrent strategies look like?

At first sight, the information on programs of $IA_\llcorner$ that the interpretation exposes is conceptually close to that in $\mathcal{O}$-Strat: it is a representation of its interactive behaviour. But the causal information makes it more explicit: for instance, the concurrent strategy for the parallel composition operation is simply described by the diagram

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

which is very close to the *intention* behind the many interleavings of the corresponding non-alternating strategy. Of course that example is somewhat expected: it is the canonical example illustrating what is gained by moving from an *interleaving* to a *truly concurrent* model of concurrency. So beyond this example, let us consider various fragments of $IA_\llcorner$ and provide examples illustrating the expressiveness of the model.
**Sequential innocent strategies.** Though the model is designed to support the interpretation of rich, effectful concurrent programs, it is informative to consider first its interpretation of simple, pure sequential programs.

For instance, the interpretation of the following simple program:

$$ \vdash \lambda f^{U \to U} . f (f \text{ skip}) : (U \to U) \to U \to U $$

yields the strategy whose behaviour is described, in symbolic notation, by

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

Ignoring indices, one may recognize the shape of *meager innocent strategy* from Definition 3.2.12, i.e. the forest of P-views – this is behind the link with sequential innocent strategies in Section 11.3. Accounting for the replications implicit in the symbolic notation, the full strategy has branches for all values of *i*, *j*, *k*, *l*, making the strategy analogous to a normal form with replicated branches as in the *resource calculus*.

This shows that the traditional notion of *P-view* is really a way to recover the causal structure for sequential, purely functional programs. Concurrent games push this handle on causality way beyond purely functional sequential programs.

**Causality of effectful programs.** For pure sequential programs, causality simply conveys syntactic dependency in the sense of imbrication within the syntax tree. But what does it express for effectful programs? We consider the program

$$ \vdash \mathbf{newref} x \mathbf{in} \lambda f^{U \to U} . f (x := 1); \mathbf{not} (\mathbf{iszero} !x) : (U \to U) \to \mathbb{B} $$

that implements a sort of *strictness testing*: if *f* answers without evaluating its argument, then the read is triggered and returns the default value of the memory cell, 0 – hence the program returns *ff*. If *f* does evaluate its argument before returning, then the program returns *tt*. The interpretation yields a strategy which comprises as induced sub-event structure that in Figure 9.16 where copy indices are indicative – unfolding the exact definition of the interpretation might yield different choices. The full strategy is of course infinite, taking into account all possible replications by Opponent.

This showcases a few important phenomena:
<figure><img src="image_152.png" /><figcaption>Figure 9.16: A prefix of the strategy for an effectful program</figcaption></figure>

First of all, the example has conflict, i.e. non-determinism. Why is that, since the program above is in IA, a deterministic language? In fact, IA is only deterministic when observed by a sequential context: here, the model is more permissive and allows the argument function to simultaneously return and call its argument. This triggers a race in memory, which may be resolved in two incompatible ways: the write may win (leading to value `tt`), or the read may win (leading to value `ff`). Accordingly, the diagram has two maximal configurations, corresponding to the two resolutions of this race.

Secondly, beyond merely describing the syntactic tree, causality also flows through memory: $tt_0^+$ depends on $q_0^-$ as it can only happen after reading a value written by the subterm whose evaluation is triggered by $q_0^-$. In contrast, $ff_0^+$ only depends on $\check{q}_0^-$. This may seem strange, because it does not seem to imply that the read *must* happen before the write for us to observe $ff_0^+$. But $ff_0^+$ is only compatible with the copy of the write acknowledgement $\check{q}_0^+$ that *does* depend on $\check{q}_0^-$ (which triggers the read).

When drawing strategies for impure programs we avoid the symbolic representation used before, as it is very misleading. If Opponent duplicates $q_0^-$ in the diagram above, this is not going to “only” duplicate the moves that depend on it: there will now be two read requests and one write requests, leading to 3! = 6 ways to resolve this three-party race. This will give rise to a complex pattern of conflicts too unwieldy to be pleasantly drawn in a single diagram, allowing 6 maximal configurations. One of them will be

<figure><img src="image_153.png" /></figure>
in which by squinting appropriately, the trained eye will recognize an execution where
the write triggered by $q_0^+$ was treated first, then the read, then the write triggered by $q_1^+$
– the only possible alternating linearization of this diagram follows this order.

**Non-determinism.** The example above also shows that a strategy may have two non-deterministic events with the same label. It is crucial that in this model, *conflict is not idempotent*: for instance, $\vdash M = \text{if choice then skip else skip}$ : $U$ yields a strategy

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

with two completely indistinguishable copies of the same computational event $\check{q}_0^+$. In-
tuively, there are two events because there are two derivations of $M \vdash \mathbf{skip}$ – each
event carries its full causal history. Keeping these events separate is sometimes impor-
tant, because they may have different futures. For instance, in the strategy

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

the two events $q_0^+$ look similar, but one will feed a value to the argument function while
the other will not, as in the term $\vdash \lambda f. \mathbf{if choice then f skip else f} \perp$.

One may wonder if this very fine-grained non-deterministic branching information
makes the model sound with respect to must-testing. The answer is: not directly, be-
cause non-deterministic branches not yielding any observable result are erased when
performing the hiding. However, hiding can be amended to correct that: this is done in
[Castellan et al., 2018a] for affine games – we shall however not follow that route here.

**Observable behaviour.** It should be clear from the examples above that the model is extremely intensional; it displays information that reflects the internal workings of the program and is by no means observable. A natural question is then: what parts of the concurrent strategy interpreting an IA<sub>∥</sub> program is observable within IA<sub>∥</sub>? We shall provide an answer to that next, by unfolding to non-alternating game semantics.
## 9.2 Unfolding Causal to Non-Alternating Strategies

For the first time, we must simultaneously consider two kinds of strategies: concurrent strategies, as in, event structures; and non-alternating strategies – which are, of course, also concurrent! To avoid confusion, we shall say *causal* (pre)strategies for event structure based (pre)strategies, and *non-alternating* (pre)strategies otherwise.

Play-based strategies present programs by listing all their observable behaviour, presented as chronologically ordered *plays*. Causal strategies tell us more: *why* an action was performed, which actions are *independent*, also keeping track separately of non-deterministic branches. Intuitively, it is clear how to go from the former to the latter: simply forget the causal structure and retain only the induced linear orderings.

While conceptually clear, doing this concretely will require us to address a number of small but significant mismatches between the two settings.

### 9.2.1 A First Unfolding

**Plays on games with symmetry.** We start with linearizations of event structures.

**Definition 9.2.1.** Consider E an event structure.

A linearization on E 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$.

We write $\mathcal{L}(E)$ for the set of linearizations on E.

If A is a board, then we also call $s \in \mathcal{L}(A)$ a **non-alternating play** on A, and write $\mathcal{O}-\text{Plays}(A) = \mathcal{L}(A)$. Now recall that a board also carries a notion of *symmetry* (see Section 7.1.1). As in Definition 7.1.14, this induces an equivalence on linearizations:

**Definition 9.2.2.** Let E be an ess and $s, t \in \mathcal{L}(E)$. We say that s and t are **symmetric**, written $s \cong_E t$, if s and t have the same length, and we have

$$ \theta_{s,t}^j = \{(s_i, t_i) \mid 1 \le i \le j\} : \{s_1, \dots, s_j\} \cong_E \{t_1, \dots, t_j\} $$

a symmetry in $\mathcal{S}(E)$ for all $1 \le j \le n$; writing $s = s_1 \dots s_n$ and $t = t_1 \dots t_n$.

It is straightforward to establish:

**Lemma 9.2.3.** Consider A a board.

Then, the relation $\cong_A$ on $\mathcal{L}(A)$ is a length-preserving equivalence satisfying:

preservation: if $s_1 \dots s_n \cong_A t_1 \dots t_p$, then for all $1 \le i \le n$, $\text{pol}_A(s_i) = \text{pol}_A(t_i)$,

restriction: if $s_1 \dots s_n \cong_A t_1 \dots t_n$, then for all $1 \le i \le n$, $s_1 \dots s_i \cong_A t_1 \dots t_i$,

simulation: if $s \cong_A t$ and $sa \in \mathcal{L}(A)$, then there is $tb \in \mathcal{L}(A)$ such that $sa \cong_A tb$.

*Proof.* Straightforward from Definitions 7.1.5 and 9.2.2. □

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

We shall rely on this to define our unfolding.
**Linearizing strategies.** As a first step towards the unfolding, we shall extract from any causal strategy $\sigma$ on board A a subset of $\mathcal{O}-\text{Plays}(A)$ – a “non-alternating strategy on A”, though no such formal object has been defined$^2$.

To do so, our main observation is the following:

**Lemma 9.2.4.** Consider $\sigma$: A causal strategy on board A. Then we have:

$$ \begin{array}{rcl} \partial_{\sigma} : & \mathcal{L}(\sigma) & \rightarrow \mathcal{L}(A) = \mathcal{O}-\text{Plays}(A) \\ & \varepsilon & \mapsto \varepsilon \\ & sm & \mapsto \partial_{\sigma}(s)\partial_{\sigma}(m). \end{array} $$

a length-preserving monotone function.

*Proof.* It is immediate from *rule-abiding* and *locally injective* that this is well-defined. Monotonicity and preservation of length are by definition. $\square$

The overload of notations for $\partial_{\sigma}$ should not cause any confusion.

The pre-unfolding of $\sigma$ is then obtained simply by projecting $\mathcal{L}(\sigma)$ – all linearizations of $\sigma$ – through $\partial_{\sigma}$. More precisely, we prove the following proposition:

**Proposition 9.2.5.** Consider $\sigma$: A causal prestrategy on board A. Then, the set

$$ \mathcal{O}-\text{Plays}(\sigma) = \partial_{\sigma}(\mathcal{L}(\sigma)) $$

satisfies the following properties:

non-empty: $\varepsilon \in \mathcal{O}-\text{Plays}(\sigma)$,
prefix-closed: for all $t \in \mathcal{O}-\text{Plays}(\sigma)$, is $s \sqsubseteq t$, then $s \in \mathcal{O}-\text{Plays}(\sigma)$,

and furthermore, if $\sigma$ is a strategy, then we additionally have:

receptive: if $s \in \mathcal{O}-\text{Plays}(\sigma)$ and $sa^- \in \mathcal{L}(A)$, then $sa \in \mathcal{O}-\text{Plays}(\sigma)$,
courteous: if $sabt \in \mathcal{O}-\text{Plays}(\sigma)$ and $\text{pol}(a) = + \text{ or } \text{pol}(b) = -$,
then if $sbat \in \mathcal{L}(A)$, $sbat \in \mathcal{O}-\text{Plays}(\sigma)$.

*Proof.* Non-empty, prefix-closed. Obvious since $\varepsilon \in \mathcal{L}(\sigma)$, $\mathcal{L}(\sigma)$ is prefix-closed and $\partial_{\sigma}$ is monotone and length-preserving.

**Receptive.** Consider $s \in \mathcal{O}-\text{Plays}(\sigma)$ and $sa^- \in \mathcal{L}(A)$. By definition, there is $u \in \mathcal{L}(\sigma)$ s.t. $s = \partial_{\sigma}(u)$. By definition of plays, $|u| \in \mathcal{C}(\sigma)$ and $\partial_{\sigma}(|u|) = |s|$ extends with $a^-$; so by *receptive* there is $m \in |\sigma|$ s.t. $|u|$ extends with $m$ and $\partial_{\sigma} m = a$. Hence, $um \in \mathcal{L}(\sigma)$ and $\partial_{\sigma}(um) = sa$, so that $sa \in \mathcal{O}-\text{Plays}(\sigma)$ as required.

**Courteous.** Consider $sabt \in \mathcal{O}-\text{Plays}(\sigma)$ and assume $\text{pol}(a) = + \text{ or } \text{pol}(b) = -$. By definition, there is $umnv \in \mathcal{L}(\sigma)$ such that $\partial_{\sigma}(u) = s$, $\partial_{\sigma}(m) = a$, $\partial_{\sigma}(n) = b$ and $\partial_{\sigma}(v) = t$. Now, of course we cannot have $n <_{\sigma} m$. If $m, n$ are incomparable, then $umnv \in \mathcal{L}(\sigma)$ as well as needed. Otherwise, $m <_{\sigma} n$. But then, we must have $m \to_{\sigma} n$. Now, since $\text{pol}(m) = + \text{ or } \text{pol}(n) = -$, by *courteous* we have $a \to_{A} b$ as well, contradicting $sbat \in \mathcal{L}(A)$. $\square$

<footnote>$^2$Recall that non-alternating strategies are sets of plays with pointers on arenas, not sets of plays on boards.</footnote>
Note that these properties are essentially those defining a non-alternating strategy (Definition 5.1.5), though based on $\mathcal{L}(A)$ with A a board rather than based on plays with pointers on an arena, i.e. as in a non-alternating version of AJM games.

It is tempting to attempt defining such a non-alternating version of AJM games, and set it as target for the unfolding of causal strategies. After all, thin concurrent games and AJM games rely on a similar mechanism for handling replication, via copy indices and symmetry, whereas $\mathcal{O}$-Strat rests on plays with pointers. However, it turns out that the AJM approach to uniformity breaks down beyond alternating deterministic strategies. An appealing alternative is suggested by Melliès' orbital games [Melliès, 2003], but this has yet to be worked out. In this monograph, the non-alternating pre-unfolding above will only be an intermediary towards the unfolding to plays with pointers.

**Notations.** In this section, the application of the display map to plays

$$ \partial_{\sigma} : \mathcal{L}(\sigma) \to \mathcal{O}-\text{Plays}(\sigma) \subseteq \mathcal{O}-\text{Plays}(A), $$

for a causal $\sigma: A$, is a central concept – it is thus worth introducing some specialized notations (inspired from our notations on configurations) to reason on such situations.

As usual, plays are ranged over via $s, t, u, v$, etc; while single moves are ranged over by $a, b, m, n$ etc. For plays in a game, we often add a tag in subscript as in $s_A, t_A \in \mathcal{O}-\text{Plays}(A)$. For linearizations in a causal strategy, we add a similar tag as a superscript, with e.g. $s^{\sigma}, t^{\sigma} \in \mathcal{L}(\sigma)$. In that case, we write $s_A^{\sigma} \in \partial_{\sigma}(s^{\sigma}) \in \mathcal{O}-\text{Plays}(A)$.

### 9.2.2 Mixed Boards and Pointifixion

The above already gives a notion of unfolding of a causal strategy $\sigma: A$ on a board $A$ as a set of non-alternating plays on $A$. However, the non-alternating game semantics of Chapter 5 is based on plays with pointers. How shall we link the two?

A causal strategy plays on a *board*, whereas non-alternating plays operate on *arenas*, which represent types without duplications. In principle, the arena may be obtained by quotienting the board, but it is not clear how to formalize this elegantly. So instead, we interpret types with a structure that stores *both* the arena and the board, along with the links between the two. Besides connecting the two structures, this will serve as a description of the “concrete” boards, that arise as the interpretation of types.

**Mixed boards.** This is captured by the notion of mixed boards:

**Definition 9.2.6.** A mixed board is $(A, \underline{A}, \text{lbl}_A)$ with $A$ a strict board, $\underline{A}$ an arena, and

$$ \text{lbl}_A : |A| \to |\underline{A}| $$

a label function preserving polarities, satisfying the following requirements:

rigid: $\text{lbl}_A$ preserves and reflects minimality, and preserves $\to$,

transparent: for any $x, y \in \mathcal{C}(A)$ and bijection $\theta: x \simeq y$, then $\theta \in \mathcal{S}(A)$ iff $\theta$ is an order-iso preserving $\text{lbl}_A$,
<figure><img src="image_157.png" /><figcaption>Figure 9.17: The strict board for $U \to U$</figcaption></figure>

<figure><img src="image_158.png" /><figcaption>Figure 9.18: The arena</figcaption></figure>

with additional components postponed until Section 12.1.1 (Definition 12.1.1).

Mixed boards make explicit how multiple moves in the board, kept apart by copy in-
dices, match the same in the arena. Figures 9.17 and 9.18 together form a representative
example, giving the mixed board interpreting the type $U \to U$, where the label function
is clear. Transparent gives a concrete account of symmetries: as they must preserve the
partial order and the label, they only exchange between interchangeable copies.

**Constructions on mixed boards.** All the basic arenas and boards used in the inter-
pretation of ground types may be paired to yield mixed boards: for instance,

$$ (\mathbf{X}, \underline{\mathbf{X}}, \mathrm{lbl}_{\mathbf{X}}) $$

pairs the “large” boards for $U, \mathbb{B}, \mathbb{N}$ from Section 9.1 with the basic arenas from Section 3.2.1, via the obvious labelling map – the mixed boards for references and semaphores are likewise straightforward. So as to lift this to the arrow type, we first need:

**Lemma 9.2.7.** Consider A a mixed board. We extend $lbl_A$ to

$$ \mathrm{lbl}_A : |!A| \to |\underline{A}| $$

by setting $lbl_A(i, a) = \mathrm{lbl}_A(a)$. Then, we still have:

rigid: $lbl_A$ preserves minimality, and preserves immediate causality $\to$,
transparent: for any $x, y \in \mathscr{C}(!A)$ and bijection $\theta : x \approx y$,
then $\theta \in \mathscr{S}(!A)$ iff $\theta$ is an order-iso preserving $lbl_A$.

*Proof.* Rigid is obvious; we show *transparent*. If. Consider $x, y \in \mathscr{C}(!A)$ and a bijec-
tion $\theta : x \approx y$, assume $\theta$ is an order-iso preserving $lbl_A$. Decompose $x$ and $y$ as

$$ x = [x_i \mid i \in I] \quad y = [y_j \mid j \in J] $$

via Lemma 8.3.1 – so that in particular for all $i \in I$, $x_i \neq \emptyset$ and for all $j \in J$, $y_j \neq \emptyset$. If $I$ and $J$ are empty then $\theta = \emptyset \in \mathscr{S}(!A)$. Otherwise, fix $i \in I$. As $A$ is strict, $x_i$ has exactly one initial move $(i, a)$, take $\theta(i, a) = (j, b)$. Set $\pi(i) = j$; done for all $i \in I$ this yields $\pi : I \cong J$, a bijection as $\theta$ induces a bijection between the initial moves of $x$ and $y$. Now since $\theta$ is an order-iso, for all $(i, a') \in x$, we have $\theta(i, a') = (\pi(i), b')$ for
some $b' \in x_{\pi(j)}$. It is direct that $\theta$ restricts to an order-iso $\theta_i : x_i \simeq y_{\pi(j)}$ which still preserves labels. This concludes the proof that $\theta \in \mathcal{S}(!A)$ as required.

Only if. Straightforward.

☐

Via this lemma, all the remaining constructions on arenas extend transparently to mixed boards, pairing the arena with the matching board construction. In particular,

$$ 
\begin{align*}
(A, \underline{A}, \operatorname{lbl}_A) \& (B, \underline{B}, \operatorname{lbl}_B) &= (A \& B, \underline{A} \& \underline{B}, \operatorname{lbl}_{A \& B}) \\
(A, \underline{A}, \operatorname{lbl}_A) \Rightarrow (B, \underline{B}, \operatorname{lbl}_B) &= (!A \to \underline{B}, \underline{A} \Rightarrow \underline{B}, \operatorname{lbl}_{A \Rightarrow B})
\end{align*}
$$

where the labels for mixed board constructions are given by

$$ 
\begin{align*}
\operatorname{lbl}_{A_1 \& A_2}(i, a) &= (i, \operatorname{lbl}_{A_1}(a)) \\
\operatorname{lbl}_{A \Rightarrow B}(2, b) &= (2, \operatorname{lbl}_{A_2}(b)) \\
\operatorname{lbl}_{A \Rightarrow B}(1, (i, a)) &= (1, \operatorname{lbl}_{A_1}(a)) \quad (B \text{ well-opened}) \\
\operatorname{lbl}_{A \Rightarrow B}(1, (b, (i, a))) &= (1, (b, \operatorname{lbl}_{A_2}(a))) \quad (B = \&_{i \in I} B_i \text{ with } B_i \text{ well-opened});
\end{align*}
$$

we omit the immediate verifications that these satisfy the conditions for mixed boards.

Overall, this yields an interpretation of each IA<sub>∥</sub> type (or context) A as a mixed board [[A]]. As a convention, we shall still let A, B, C etc range over mixed boards, and silently coerce them to the board components (as in “let $a \in A$”, etc). The arena component will be referred to explicitly via A, B, etc.

**Pointfixion.** Mixed boards are the adequate setting to link causal strategies with plays with pointers. First, any play on the board A yields a play with pointer on the arena A:

**Lemma 9.2.8.** Consider A a mixed board. Then, the function

$$ (\neg) : \mathcal{O}-\text{Plays}(!A) \to \mathcal{O}-\text{PrePlays}(\underline{A}) $$

sending $s = s_1 \dots s_n \in \mathcal{O}-\text{Plays}(A)$ to $\mathcal{O}$ with components,

moves: the sequence $t = t_1 \dots t_n$ with $t_i = \operatorname{lbl}(s_i)$,

pointers: for $1 \le i < j \le n$, $t_j$ points to $t_i$ iff $s_i \to^{\to!A} t_i$.

is well-defined.

*Proof.* For $s = s_1 \dots s_n \in \mathcal{O}-\text{Plays}(!A)$, $\mathcal{O}$ is $t_1 \dots t_n$, where $t_j$ points to $t_i$ iff $s_i \to^{\to!A} s_j$. We must show that every non-initial move has a pointer: if $t_j$ is non-initial, then $s_j$ is non-initial since $\operatorname{lbl}$ preserves minimality. So there is $a \to^{\to!A} s_j$. But since $s \in \mathcal{O}-\text{Plays}(!A)$, $\{s_1, \dots, s_j\}$ is a configuration thus down-closed, so $a = s_i$ for some $1 \le i < j$. It follows that $t_j$ has a pointer to $t_i$ as required. ☐

☐

This is illustrated in Figure 9.19: on the left, we show a non-alternating play on !(!($U \to U$) $\to$ B) – in this figure, each move carries a sequence of copy indices, from the outermost ! to the innermost<fnref n="3" />. On the right, we show the corresponding play

<footnote n="3">³This is different to the convention in most of this monograph where only the index for the innermost ! is shown, the others being recovered from the immediate dependency.</footnote>
<figure><img src="image_159.png" /><figcaption>Figure 9.19: Recovering pointers</figcaption></figure>

with pointers: it is obtained from the diagram on the rhs by making the immediate dependency from the game an explicit component of the play, then removing copy indices.

Crucially, this construction is invariant under symmetry:

**Proposition 9.2.9.** Consider A a mixed board. Then, ($\hat{\otimes}$) yields a function

$$ (\hat{\otimes}) : \mathcal{O}\text{-Plays}(!A) / \cong_{!A} \rightarrow \mathcal{O}\text{-PrePlays}(\underline{A}), $$

injective and preserving length and prefix.

*Proof.* First, it preserves $\cong_{!A}$: if $s = s_1 \dots s_n \cong_{!A} t_1 \dots t_n = t$, then $\theta = \{(s_i, t_i) \mid 1 \le i \le n\} \in \mathcal{S}(!A)$; but by *transparent* (via Lemma 9.2.8), $lbl(s_i) =lbl(t_i)$ for all $1 \le i \le n$. Furthermore, by Lemma 7.1.6, $\theta$ is an order-isomorphism, so $s_i \to_A s_j$ iff $t_i \to_A t_j$ for all $1 \le i < j \le n$, hence $\mathcal{R}$ and $\mathcal{F}$ have the same pointers. Finally, the construction clearly preserves length and prefix as required.

For injectivity, take $s, t \in \mathcal{O}\text{-Plays}(!A)$ with $\mathcal{R} = \mathcal{F}$, writing $s = s_1 \dots s_n$ and $t = t_1 \dots t_n$. Then, for all $1 \le i \le n$, $\theta_{s,t}^i = \{(s_j, t_j) \mid 1 \le j \le i\}$ is a bijection between configurations of A. But since $\mathcal{R} = \mathcal{F}$, $\theta_{s,t}^i$ is actually an order-isom preserving $lbl$, so by *transparent* (via Lemma 9.2.8) we have $\theta_i \in \mathcal{S}(!A)$. Hence, $s \cong_{!A} t$. $\square$

This proposition makes explicit the folklore idea that *plays with pointers* are concrete representatives for equivalence classes of plays with copy indices. Drawing inspiration from [Danos et al., 1996], we call $\mathcal{R}$ the **pointifixion** of $s$ – note however that in [Danos et al., 1996] the pointers must be *reconstructed* from the copy indices, whereas here, they are already in $s$ as the immediate causal links from the board.
<figure><img src="image_160.png" /><figcaption>Figure 9.20: A configuration of $\sigma : !\{U \to U\} \to B$</figcaption></figure>

Note that though pointfixion was defined as

$$ (\stackrel{\wedge}{\sigma}) : \mathcal{O}-\text{Plays}(!A) / \cong_{!A} \to \mathcal{O}-\text{PrePlays}(\underline{A}), $$

the same definition may be transparently applied to obtain, for all A,

$$ (\stackrel{\wedge}{\sigma}) : \mathcal{O}-\text{Plays}(A) / \cong_A \to \mathcal{O}-\text{PrePlays}_* (\underline{A}), $$

used without further details. Additionally, extensions of plays lift along these functions:

**Lemma 9.2.10.** Consider A a mixed board. We have the following properties:

(1) For all $ta \in \mathcal{O}-\text{PrePlays}_*(\underline{A})$, $s \in \mathcal{O}-\text{Plays}(A)$ such that $t = \mathcal{S}$, there is $sa' \in \mathcal{O}-\text{Plays}(A)$ such that $(\stackrel{\wedge}{\sigma})(sa') = ta$;

(2) For all $ta \in \mathcal{O}-\text{PrePlays}_*(\underline{A})$, $s \in \mathcal{O}-\text{Plays}(!A)$ such that $t = \mathcal{S}$, there is $sa' \in \mathcal{O}-\text{Plays}(!A)$ such that $(\stackrel{\wedge}{\sigma})(sa') = ta$.

*Sketch.* The proof exploits that since we have interpreted ground types duplicating answers, for any extension of $t \in \mathcal{O}-\text{PrePlays}_*(\underline{A})$ one can find a “fresh” move in !A, with a new copy index, matching the extension. However, formalizing this requires the full definition of mixed boards which we prefer to postpone to Section 12.1.1. $\square$

Proposition 9.2.9 and Lemma 9.2.10 entail that plays with pointers on $\underline{A}$ may be regarded *exactly* as non-alternating plays on the $--\text{board}$ !A considered up to symmetry:

**Corollary 9.2.11.** Consider A a mixed board. Then, $(\stackrel{\wedge}{\sigma})$ yields a bijection

$$ (\stackrel{\wedge}{\sigma}) : \mathcal{O}-\text{Plays}(!A) / \cong_{!A} \approx \mathcal{O}-\text{PrePlays}_*(\underline{A}), $$

preserving length and prefix.

The above development concerns *non-alternating pre-plays with pointers* (Definition 5.1.1); recall that the *non-alternating plays with pointers* from which non-alternating game semantics are built are also (logically) well-bracketed (Definition 5.1.3).
<figure><img src="image_161.png" /><figcaption>Figure 9.21: Constructing a play in the unfolding</figcaption></figure>

### 9.2.3 Unfoldings of a Causal Strategy

Next, we describe how to *unfold* a causal strategy to a non-alternating strategy.

More precisely, we shall provide three different unfoldings:

(1) $\mathcal{O}$-Unf<sub>•</sub> unfolds $\boldsymbol{\sigma} : A$ to a non-alternating thread-strategy on $\underline{A}$,

(2) $\mathcal{O}$-Unf<sub>•</sub> unfolds $\boldsymbol{\sigma} : !A$ to a non-alternating strategy on $\underline{A}$,

(3) $\mathcal{O}$-Unf unfolds $\boldsymbol{\sigma} : !A \vdash B$ to a non-alternating strategy on $\underline{A} \Rightarrow \underline{B}$,

for all mixed boards A and B.

**Unfolding to a thread-strategy.** For A a mixed board, we may now *unfold* a causal strategy $\boldsymbol{\sigma} : A$ to a set $\mathcal{O}-Unf_{\cdot}(\boldsymbol{\sigma})$ of threads. Plays in $\mathcal{O}-Unf_{\cdot}(\boldsymbol{\sigma})$ are obtained from $\boldsymbol{\sigma}$ in three steps. First (1) form the *linearizations of configurations of* $\boldsymbol{\sigma}$, i.e. $\mathcal{L}(\boldsymbol{\sigma})$ (Definition 9.2.1). Then (2), project those to $\mathcal{O}-Plays(A)$ by applying $\partial_{\sigma}$ event by event. Then finally, (3) apply pointifixion. More formally, the definition reads as:

**Definition 9.2.12.** Consider A a mixed board, and $\boldsymbol{\sigma} : A$ a causal strategy.

The *unfolding* of $\boldsymbol{\sigma}$ is the set $\mathcal{O}-Unf_{\cdot}(\boldsymbol{\sigma}) = \{(\mathcal{O})(s_A^{\boldsymbol{\sigma}}) \in \mathcal{O}-Plays(\underline{A}) | s^{\boldsymbol{\sigma}} \in \mathcal{L}(\boldsymbol{\sigma})\}$.

Observe that not all linearizations of $\boldsymbol{\sigma}$ contribute to the unfolding, only those which by display and pointifixion yield a (logically) well-bracketed play.

We illustrate this in Figures 9.20 and 9.21. Figure 9.20 displays a configuration of a causal $\boldsymbol{\sigma}$ on $!(U \to U) \dashv B$, first with our usual notational convention, then explicitly separating the internal events of $\boldsymbol{\sigma}$ from their display in the game. In Figure 9.21, we start with the sequence $abcdef \in \mathcal{L}(\boldsymbol{\sigma})$; then follow the two steps of the construction of the corresponding play of the unfolding: first by displaying it on A, then pointifixion. In Figure 9.21, we insist that though pointers appear in the intermediary step, they are not part of the structure of plays and only represent immediate causal dependency in the game. On the right hand side, pointers are now explicitly part of the play.

As expected, this unfolding yields a valid non-alternating thread-strategy on $\underline{A}$:
**Proposition 9.2.13.** Consider $\sigma : A$ a causal strategy.

Then, $\mathcal{O}-\text{Unf}_*(\sigma) : \underline{A}$ is a thread-strategy in the sense of Definition 5.1.7.

*Proof.* Clearly it is a set of threads. Non-empty and prefix-closed are immediate.

*Receptive:* consider $t = (\stackrel{\leftarrow}{s}_A^\sigma)$ for $s^\sigma \in \mathcal{L}(\sigma)$, with $tb^- \in \mathcal{O}-\text{Plays}_*(\underline{A})$. By Lemma 9.2.10, there is $s_A^\sigma a^- \in \mathcal{O}-\text{Plays}(\underline{A})$ such that $(\stackrel{\leftarrow}{s}_A^\sigma a^-) = tb^-$. Now, by Proposition 9.2.5, there is $s^\sigma m \in \mathcal{L}(\sigma)$ displaying to $s_A^\sigma a^-$, and *receptive* follows.

*Courteous:* consider $uabv = (\stackrel{\leftarrow}{u}_A^\sigma a'b'v^\sigma_A)$ where $a$ is positive or $b$ negative, and assume $ubav \in \mathcal{O}-\text{Plays}_*(\underline{A})$. It follows that $u^\sigma a^\sigma b'a'b^\sigma v^\sigma_A \in \mathcal{O}-\text{Plays}(\underline{A})$: if we had $a' \dashv_A b'$, this would mean that $b$ points on $a$ by definition of pointfixion. Hence, $u^\sigma b'a'b^\sigma v^\sigma_A \in \mathcal{O}-\text{Plays}(\sigma)$ by Proposition 9.2.5, whose pointfixion is $ubav$ as required. $\square$

**Unfolding to a non-alternating strategy.** Above, we have defined the unfolding of $\sigma : A$ as a thread-strategy $\mathcal{O}-\text{Unf}_*(\sigma)$. Next we unfold $\sigma : !A$ to a full strategy:

**Definition 9.2.14.** Consider A a mixed board, and $\sigma : !A$ a causal strategy.

The *unfolding* of $\sigma$ is the set $\mathcal{O}-\text{Unf}_1(\sigma) = \{(\stackrel{\leftarrow}{s}_A^\sigma) | s^\sigma \in \mathcal{L}(\sigma)\}$.

With respect to Definition 9.2.12, the only difference is that we start with a causal strategy on !A rather than A. The immediate consequence is that the unfolding process will give us *plays*, rather than merely threads. As before, we have:

**Proposition 9.2.15.** Consider A a mixed board and $\sigma : !A$ a causal strategy.

Then, $\mathcal{O}-\text{Unf}_1(\sigma) : \underline{A}$ is a non-alternating strategy as in Definition 5.1.5.

*Proof.* Same proof as for Proposition 9.2.13. $\square$

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

If $\sigma : A$ is a causal strategy, we may unfold it as a thread-strategy with $\mathcal{O}-\text{Unf}_*(\sigma) : \underline{A}$; or we may unfold its promotion as a full non-alternating strategy with $\mathcal{O}-\text{Unf}_1(\sigma^1) : \underline{A}$. In the sequel we shall need to relate these two unfoldings: in particular, $\mathcal{O}-\text{Unf}_1(\sigma^1)$ is a single-threaded strategy whose generating thread-strategy is $\mathcal{O}-\text{Unf}_*(\sigma)$:

**Lemma 9.2.16.** Consider causal $\sigma : A$, and $\sigma^1 : !A$ its promotion.

Then, $(\mathcal{O}-\text{Unf}_*(\sigma))^1 = \mathcal{O}-\text{Unf}_1(\sigma^1)$.

*Proof.* For $\subseteq$, we show by induction on $n \in \mathbb{N}$ that for all $n \in \mathbb{N}$, $\mathcal{O}-\text{Unf}_*(\sigma)^{(n)}$ as defined below Definition 5.1.7, is included in $\mathcal{O}-\text{Unf}_1(\sigma^1)$. This boils down to the fact that whenever $s \in \mathcal{O}-\text{Unf}_1(\sigma^1)$ and $t \in \mathcal{O}-\text{Unf}_*(\sigma)$, then $s \sqcup t \subseteq \mathcal{O}-\text{Unf}_1(\sigma^1)$.

Consider $u \in s \sqcup t$. We have $s = \hat{u}$ and $t = \mathcal{V}$ for $u = \partial_{\sigma^1}(u')$ and $v = \partial_{\sigma}(v')$ with

$$u' \in \mathcal{O}-\text{Plays}(\sigma^1), \quad v' \in \mathcal{O}-\text{Plays}(\sigma).$$

Now, $u'$ visits only finitely many copies for the outermost !, so considering

$$w' = (i, v'_1) \dots (i, v'_n)$$

for $v' = v'_1 \dots v'_n$, with $i \in \mathbb{N}$ not visited by $u'$, we get $w' \in \mathcal{O}-\text{Plays}(\sigma^1)$ satisfying that writing $w = \partial_{\sigma^1}(w')$, we have $\hat{w} = \mathcal{V} = t$. But necessarily, $u'$ and $w'$ are disjoint; so we may form $z' \in \mathcal{O}-\text{Plays}(\sigma^1)$ the interleaving of $u'$ and $w'$ following the same scheduling
as $u \in s \sqcup t$, and by construction $u = \mathbb{F}$ for $z = \partial_{\sigma'}(z')$.

For $\sqcup$, consider $s \in \mathcal{O}-\mathrm{Unf}_i(\sigma')$. By definition, $s = \mathbb{u}$ and $u = \partial_{\sigma'}(u')$ such that $u' \in \mathcal{O}-\mathrm{Plays}(\sigma')$. By definition, $u'$ visits a finite set $I$ of copy indices; each $i \in I$ yields a restriction $u'_i \in \mathcal{O}-\mathrm{Plays}(\sigma)$. For each $i \in I$, we write $u_i = \partial_{\sigma}(u'_i)$ and $s_i = \mathbb{u}_i$ – by construction, $s_i \in \mathcal{O}-\mathrm{Unf}_i(\sigma)$. Finally, $s$ is an interleaving of all the $s_i$'s. $\square$

**Unfolding from mixed board A to mixed board B.** We wish to relate the Kleisli category $\mathbf{NTCG}_1$ to the cartesian closed category $\mathcal{O}-\mathbf{Strat}$ – this induces two complications in the unfolding, departing from the simple case described above.

Firstly, the way the two hom-sets are constructed differs slightly. Indeed, a morphism $\sigma$ from $A$ to $B$ in $\mathbf{NTCG}_1$ is a causal strategy on $!A \vdash B$, i.e. $(!A)^{\perp} \parallel B$ where $!A, B$ are causally independent. In constrast, non-alternating strategies from $A$ to $B$ have plays in $A \Rightarrow B$, where the arrow construction imposes a dependency between (the initial moves of) the two components. We must thus consider the currying of $\sigma$:

$$ \Lambda(\sigma) : !A \to B. $$

Secondly, the configurations of a causal strategy $\sigma : !A \to B$ have at most one initial move in $B$ – in contrast with non-alternating plays on $A \Rightarrow B$, in which arbitrarily many initial moves in $B$ may occur. This is solved by unfolding not $\Lambda(\sigma)$ but

$$ \Lambda(\sigma)' : !(!A \to B), $$

its promotion, which will be the basis of the unfolding. This prompts:

**Definition 9.2.17.** Consider $\sigma : !A \vdash B$ a causal strategy. Its unfolding is:

$$ \mathcal{O}-\mathrm{Unf}(\sigma) = \mathcal{O}-\mathrm{Unf}_i(\Lambda(\sigma)') : A \Rightarrow B. $$

It is a consequence of Proposition 9.2.15 that this is well-defined.

## 9.3 $\to$-Strat and Full Abstraction

We aim to prove that the unfolding above is as expected compatible with all operations used in the interpretation of $IA_∥$, which shall bridge the two interpretations.

But we shall soon see that this will require us to add one further condition refining $\mathbf{NTCG}_1$ to $\to$-Strat, dealing with the fact that non-alternating plays with pointers are (logically) well-bracketed while arbitrary linearizations might not be.

### 9.3.1 Unfolding the Categorical Structure

We examine how unfolding preserves the categorical structure of $\mathbf{NTCG}_1$.
**Unfolding of copycat.** First, we unfold the identities of NTCG<sub>1</sub>. Here, not much is happening conceptually; however technically the respective definitions of the causal and non-alternating copycat strongly differ: while the causal copycat comes from an explicit, concrete description (Definition 6.4.1), the non-alternating copycat is in a sense the “free asynchronous completion” of the alternating copycat (Definition 5.2.5). This indirect definition makes it quite unwieldy to reason with.

**Proposition 9.3.1.** Consider A a mixed board.

Then, $\mathbf{der}_A : !A \vdash A$ unfolds to the non-alternating copycat strategy, $\mathcal{O}-\mathbf{c}_A$.

*Proof.* Recall from Definition 5.2.5 and Lemma 5.1.10 that the plays of $\mathcal{O}-\mathbf{c}_A$ are those obtained from $\upharpoonright \mathbf{c}_A$ by receptivity and courtesy in the sense of Definition 5.1.5.

By Lemma 9.2.16, it suffices to prove the equality

$$ \mathcal{O}-\text{Unf.}(\Lambda(\mathbf{der}_A)) = \mathcal{O}-\mathbf{c}_A^*, $$

where $\mathcal{O}-\mathbf{c}_A^*$ denotes the set of threads of $\mathcal{O}-\mathbf{c}_A$.

For $\subseteq$ consider $s \in \mathcal{O}-\text{Unf.}(\Lambda(\mathbf{der}_A))$, meaning that there are $s = \hat{t}$ with $t = \partial_{\Lambda(\mathbf{der}_A)}(u)$ for some $u \in \mathcal{L}(\mathbf{c}_A)$. Now, one can show that there is $v \in \upharpoonright \mathcal{L}(\mathbf{c}_A)$ and $w^-$ a sequence of moves of $\mathbf{c}_A$ negative in $A \vdash A$, such that

$$ vw^- \in \mathcal{O}-\text{Plays}(\mathbf{c}_A) $$

has the same moves as $u$, and s.t. $u$ may be obtained from $vw^-$ by courtesy, such that (the pointfixion of) all intermediate plays are logically well-bracketed. Considering

$$ t' = \partial_{\Lambda(\mathbf{der}_A)}(v), \quad s' = \hat{t}, \quad t'' = \partial_{\Lambda(\mathbf{der}_A)}(vw^-), \quad s'' = \hat{t}^*, $$

it is immediate that $t' \in \upharpoonright \mathbf{c}_A$. Thus, $t' \in \mathcal{O}-\mathbf{c}_A$, and so $t'' \in \mathcal{O}-\mathbf{c}_A$ by receptivity. But then, by construction $s$ may be obtained from $s''$ by courtesy, thus $s \in \mathcal{O}-\mathbf{c}_A$.

For $\sqcup$, consider $s \in \mathcal{O}-\mathbf{c}_A$ a thread. By definition, $s$ is obtained by courtesy and receptivity from some $s' \in \upharpoonright \mathbf{c}_A$. Writing $s' \in \mathcal{O}-\text{Plays}(A_1 \Rightarrow A_2)$, for all positive-ending $t' \sqsubseteq s'$, $t' \upharpoonright A_1 = t' \upharpoonright A_2$. By Corollary 9.2.11, there is $u \in \upharpoonright \text{Plays}(A)$ s.t. $t' \upharpoonright A_1 = \hat{u}$. We may then define $v \in \upharpoonright \mathcal{L}(\mathbf{c}_A)$ by interleaving two copies of $u$ in the obvious way, s.t. $v \upharpoonright A_1 = v \upharpoonright A_2 = u$. From the definition, it is direct that writing $w = \partial_{\Lambda(\mathbf{der}_A)}(v)$, $s' = \hat{w}$. By Proposition 9.2.5, applying to $w$ instances of courtesy and receptivity as for $s' \rightsquigarrow s$, we get $z \in \mathcal{O}-\text{Plays}(\mathbf{c}_A)$ s.t. $s = \phi(\partial_{\Lambda(\mathbf{der}_A)}(z))$. $\square$

The definition of $\mathcal{O}-\mathbf{c}_A$ via saturation in Definition 5.2.5 is unpleasant: to prove that a play is in $\mathcal{O}-\mathbf{c}_A$ we must provide a sequence of applications of courtesy and receptivity from a play of $\upharpoonright \mathbf{c}_A$. It seems hard to avoid while staying in the context of pointer games. In contrast, $\overline{\mathbf{der}}_A$ offers via unfolding a concrete definition of $\mathcal{O}-\mathbf{c}_A$.

**Well-bracketing.** Unfolding preserves the identity; but composition is *not* preserved: for $\sigma \in \text{NTCG}_1(A, B)$ and $\tau \in \text{NTCG}_1(B, C)$, we may not have

$$ \mathcal{O}-\text{Unf}(\tau \odot_1 \sigma) \subseteq \mathcal{O}-\text{Unf}(\tau) \odot \mathcal{O}-\text{Unf}(\sigma). $$
The issue is that unfolding only keeps (logically) well-bracketed plays, but well-bracketed plays in the unfolding of $\tau \odot_1 \sigma$ may very well originate in pre-plays in the unfoldings of $\sigma$ and $\tau$ that fail well-bracketing. In order to obtain this inclusion, we shall have to put an additional restriction on causal strategies:

**Definition 9.3.2.** Consider $\sigma$ : !A $\vdash$ B a causal strategy. It is **well-bracketed** iff for all $sm^+ \in \mathcal{L}(\sigma)$, if $\cdot:(\partial_{\Lambda(\sigma)}(s))$ is (logically) well-bracketed, then so is $\cdot:(\partial_{\Lambda(\sigma)}(sm))$.

Alternatively, $\sigma$ is well-bracketed iff the unfolding only “cuts at Opponent moves”. We skip the routine but lengthy verification of the following fact:

**Theorem 9.3.3.** There is $\dashrightarrow$-Strat, a cartesian closed $\sim$-category with objects mixed boards and morphisms those well-bracketed $\sigma \in \text{NTCG}_1(A, B)$, which supports the interpretation of IA<sub>∥</sub>. Moreover there is an obvious forgetful $\sim$-functor

$$ \dashrightarrow\text{-Strat} \to \text{NTCG}_1 $$

sending a mixed board to the underlying $\sim$-board, leaving morphisms unchanged.

**Preservation of composition.** The models $\dashrightarrow$-Strat and $\mathcal{O}$-Strat differ fundamentally in that one is causal while the other is based on interleavings, but that in itself is not hard to manage, via the mechanism of linearizations.

The real challenge is that the compositional mechanisms of these two models follow significantly different principles: (1) $\dashrightarrow$-Strat is constructed via the Kleisli category of the linear model NTCG, while $\mathcal{O}$-Strat is inherently non-linear; (2) $\dashrightarrow$-Strat uses explicit copy indices, while $\mathcal{O}$-Strat uses pointers; and (3) the hom-set of $\dashrightarrow$-Strat is the board !A $\vdash$ B with no causal dependency between A and B, whereas $\mathcal{O}$-Strat uses the arrow construction $A \Rightarrow B$ (which seems unavoidable for a pointer-based model). None of these are particularly challenging, but the three are deeply intertwined and must be managed simultaneously in the compatibility of unfolding with composition<fnref n="4" />.

We address the two directions of the unfolding separately. First:

**Lemma 9.3.4.** Consider $\sigma \in \dashrightarrow$-Strat(A, B) and $\tau \in \dashrightarrow$-Strat(B, C). Then, we have the inclusion $\mathcal{O}$-Unf$_{\bullet}$($\Lambda(\tau \odot \sigma^1)$) $\subseteq$ $\mathcal{O}$-Unf($\tau$) $\odot$ $\mathcal{O}$-Unf($\sigma$).

*Proof.* For $s \in \mathcal{O}$-Unf$_{\bullet}$($\Lambda(\tau \odot \sigma^1)$), by definition $s = \cdot:(\partial_{\Lambda(\tau \odot \sigma^1)}(s'))$ for some $s' \in \mathcal{O}$-Plays($\tau \odot \sigma^1$). There is $u' \in \mathcal{O}$-Plays($\tau \otimes \sigma^1$) with visible restriction $s'$, and

$$ u'_{\sigma'} \in \mathcal{O}\text{-Plays}(\sigma^1) = \mathcal{O}\text{-Plays}(!\sigma), \quad u'_{\tau} \in \mathcal{O}\text{-Plays}(\tau). $$

are projections obtained applying move-by-move (the (partial) projections of moves of the interaction to moves of the compound strategies as defined just above Lemma 6.2.14.

Now, $u'$ is displayed to $v' \in \mathcal{O}$-Plays(!A $||$ !B $||$ C) via $\partial_{\tau \otimes \sigma}$. There is an implicit dependency between moves minimal in the game: moves minimal in !B depend on the minimal move in C. Likewise, there is a unique way to assign moves minimal in !A to

<footnote n="4">⁴Ideally, one would deal with them separately by introducing a separate model: a non-alternating play-based games model based on copy indices rather than pointers – but we leave this out of scope.</footnote>
those minimal in $!B$ in a way compatible with $\partial_{!\Lambda(\sigma)}(u'_{\sigma}) \in \mathcal{O}-\text{Plays}(!A \to B))$. We
form $w' \in \mathcal{O}-\text{I}(\underline{A}, \underline{B}, \underline{C})$ by first applying labels to $v'$ as in Proposition 9.2.9, extended
with this assignment. Now from the constructions, direct verifications entail

$$
w' \upharpoonright \underline{A}, \underline{B} \in \mathcal{O}-\text{Unf}_1(\Lambda(\sigma)^1), \quad w' \upharpoonright \underline{B}, \underline{C} \in \mathcal{O}-\text{Unf}_1(\Lambda(\tau)^1), \quad w' \upharpoonright \underline{A}, \underline{C} = s,
$$

thus $w'$ is a witness for $s \in \mathcal{O}\text{-Unf}(\tau) \odot \mathcal{O}\text{-Unf}(\sigma)$ as required.

☐

These “direct verifications” include, in particular, that the restrictions of $w'$ are (log-
ically) well-bracketed. That $w'$ is itself well-bracketed is established by immediate
induction, using that $\sigma$ and $\tau$ are well-bracketed. Now, we focus on the other inclusion:

**Lemma 9.3.5.** Consider $\sigma \in \text{NTCG}_1(A, B)$, $\tau \in \text{NTCG}_1(B, C)$.

Then, threads in $\mathcal{O}-\text{Unf}(\tau) \odot \mathcal{O}-\text{Unf}(\sigma)$ are in $\mathcal{O}-\text{Unf}_*(\Lambda(\tau \odot \sigma^1))$.

*Proof.* Consider $s \in \mathcal{O}\text{-Unf}(\tau) \odot \mathcal{O}\text{-Unf}(\sigma)$ a thread, so there is $u \in \mathcal{O}\text{-I}(\underline{A}, \underline{B}, \underline{C})$ s.t.
$u \upharpoonright \underline{A}, \underline{B} \in \mathcal{O}\text{-Unf}(\sigma)$, $u \upharpoonright \underline{B}, \underline{C} \in \mathcal{O}\text{-Unf}(\tau)$, and $u \upharpoonright \underline{A}, \underline{C} = s$. By hypothesis,

$$
u \upharpoonright \underline{A}, \underline{B} = \hat{\circ}(\partial_{\Lambda(\sigma)^1}(v^{\sigma})), \quad u \upharpoonright \underline{B}, \underline{C} = \hat{\circ}(\partial_{\Lambda(\tau)^1}(v^{\tau}))
$$

for $v^\sigma \in \mathcal{O}\text{-Plays}(!\sigma) = \mathcal{O}\text{-Plays}(\sigma^1)$ and $v^\tau \in \mathcal{O}\text{-Plays}(!\tau)$; but as $v^\sigma$ has one initial
move, we consider $v^\tau \in \mathcal{O}\text{-Plays}(\tau)$ with $u \upharpoonright \underline{B}, \underline{C} = \hat{\circ}(\partial_{\Lambda(\tau)}(v^\tau))$. We also have:

$$
w^{\sigma} = \partial_{\sigma}^{1}(v^{\sigma}) \in \mathcal{O}\text{-Plays}(!A \vdash !B), \quad w^{\tau} = \partial_{\tau}(v^{\tau}) \in \mathcal{O}\text{-Plays}(!B \vdash C),
$$

and since $u \upharpoonright \underline{A}, \underline{B}$ and $u \upharpoonright \underline{B}, \underline{C}$ coincide on $\underline{B}$, it is a direct verification that

$$
\hat{\circ}(w^{\sigma} \upharpoonright !B) = u \upharpoonright \underline{B} = \hat{\circ}(w^{\tau} \upharpoonright !B),
$$

so that $w^{\sigma} \upharpoonright !B \cong_{!B} w^{\tau} \upharpoonright !B$ by Proposition 9.2.9. Now, writing configurations

$$
x^{\sigma} = |v^{\sigma}|, \quad x^{\tau} = |v^{\tau}|,
$$

this informs a symmetry $\theta : x_{!B}^{\sigma} \cong_{!B} x_{!B}^{\tau}$. The difficulty is that this symmetry might
not be the identity, preventing us from synchronizing $x^{\sigma}$ and $x^{\tau}$.

So additionally, we note that $u$ informs a linearization of the composite bijection

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

witnessing the fact that the triple $(x^\sigma, \theta, x^\tau)$ is causally compatible in the sense of Def-
inition 7.4.3. We write $r \in \mathcal{O}\text{-Plays}(\varphi[x^\sigma, \theta, x^\tau])$ for this linearization; it projects to
$\partial(r) \in \mathcal{O}\text{-Plays}(!A \parallel !B \parallel C)$ in the obvious way, and we have

$$
\hat{\circ}(\partial(r)) = \bar{u} \in \mathcal{O}\text{-Plays}(\underline{A} \times \underline{B} \times \underline{C})
$$

where $\bar{u}$ is $u$ without the pointers of initial moves in $\underline{A}$ and $\underline{B}$.

Thanks to causal compatibility, Proposition 7.4.4 provides us with $y^\sigma \in \mathscr{C}(\sigma^1)$ and $y^\tau \in \mathscr{C}(\tau)$ causally compatible configurations, along with symmetries

$$
\varphi^{\sigma} : x^{\sigma} \cong_{\sigma!} y^{\sigma}, \quad \varphi^{\tau} : x^{\tau} \cong_{\tau} y^{\tau},
$$
such that we have $\varphi_{!A}^{\sigma} \in \mathcal{S}_{-}(!A)$, $\varphi_{C}^{\tau} \in \mathcal{S}_{+}(C)$, and the following diagram commutes

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

following which the linearization $r \in \mathcal{O}-\text{Plays}(\varphi[x^{\sigma}, \theta, x^{\tau}])$ transports to a linearization $r' \in \mathcal{O}-\text{Plays}(\varphi[y^{\sigma}, y^{\tau}])$ satisfying $\partial(r) \cong_{!A||!B||C} \partial(r')$, so that $\hat{\varphi}(\partial(r')) = \bar{u}$.

Now by Proposition 6.2.7, $\varphi[y^{\tau} \otimes y^{\sigma}]$ is order-isomorphic to $y^{\tau} \otimes y^{\sigma} \in \mathcal{C}(\tau \otimes \sigma')$. Accordingly, $r'$ transports to $r'' \in \mathcal{O}-\text{Plays}(y^{\tau} \otimes y^{\sigma})$ such that $\hat{\varphi}(\partial_{\tau \otimes \sigma'}(r'')) = \bar{u}$, which projects to $z \in \mathcal{O}-\text{Plays}(\tau \odot \sigma')$ such that $\hat{\varphi}(\partial_{\tau \odot \sigma'}(z)) = \bar{s}$. But $s$ is a thread so that the pointers of initial moves in $A$ are forced; accordingly $\hat{\varphi}(\partial_{\Lambda(\tau \odot \sigma')}(z)) = s$. $\square$

Note that this inclusion does not require well-bracketing. Altogether:

**Corollary 9.3.6.** Consider $\sigma \in \mathcal{O}\text{-Strat}(A, B)$ and $\tau \in \mathcal{O}\text{-Strat}(B, C)$.

$$ \textit{Then, } \mathcal{O}\text{-Unf}(\tau \odot \sigma) = \mathcal{O}\text{-Unf}(\tau) \odot \mathcal{O}\text{-Unf}(\sigma). $$

*Proof.* For the first inclusion, we compute:

$$ \begin{align*} \mathcal{O}\text{-Unf}(\tau \odot \sigma) &= \mathcal{O}\text{-Unf}(\tau \odot \sigma') \\ &= \mathcal{O}\text{-Unf}_{\mathcal{I}}(\Lambda(\tau \odot \sigma')') \\ &= \mathcal{O}\text{-Unf}_{\mathcal{I}}(\Lambda(\tau \odot \sigma'))' \\ &\subseteq (\mathcal{O}\text{-Unf}(\tau) \odot \mathcal{O}\text{-Unf}(\sigma))' \\ &= \mathcal{O}\text{-Unf}(\tau) \odot \mathcal{O}\text{-Unf}(\sigma) \end{align*} $$

using definition of Kleisli composition, definition of $\mathcal{O}\text{-Unf}$, Lemma 9.2.16, Lemma 9.3.4. Finally, we use that by Lemma 9.2.16, $\mathcal{O}\text{-Unf}(\sigma)$ and $\mathcal{O}\text{-Unf}(\tau)$ are single-threaded strategies so that their composition is, so it is stable under interleavings.

The other inclusion holds on threads by Lemma 9.3.5 and extends to all plays by Lemma 9.2.16 since the non-alternating strategies involved are single-threaded. $\square$

Now, we may finally state:

**Theorem 9.3.7.** Unfolding yields a $\sim$-functor $\mathcal{O}\text{-Unf} : \mathcal{O}\text{-Strat} \to \mathcal{O}\text{-Strat}$.

*Proof.* For any $\sigma \in \mathcal{O}\text{-Strat}(A, B)$, $\mathcal{O}\text{-Unf}(\sigma)$ is a non-alternating strategy on $A \Rightarrow B$, single-threaded by Lemma 9.2.16, thus $\mathcal{O}\text{-Unf}(\sigma) \in \mathcal{O}\text{-Strat}(A, B)$. The only thing remaining to check is that $\mathcal{O}\text{-Unf}$ preserves equivalence, i.e.

$$ \mathcal{O}\text{-Unf}(\sigma) = \mathcal{O}\text{-Unf}(\tau) $$

for all positive iso $\varphi : \sigma \approx \tau \in \mathcal{O}\text{-Strat}(A, B)$. To prove that, consider $s \in \mathcal{O}\text{-Unf}(\sigma)$, i.e. there must be $s^{\sigma} \in \mathcal{L}(\sigma)$ such that $\hat{\varphi}(\partial_{\Lambda(\sigma)}(s^{\sigma})) = s$. But then

$$ \varphi(s^{\sigma}) \in \mathcal{L}(\tau) $$
and from the commutation in the game up to symmetry, it follows immediately that

$$ \partial_{\Lambda(\sigma)}(s^{\sigma}) \cong_{!|A \to B} \partial_{\Lambda(\tau)}(\varphi(s^{\sigma})) $$

which entails that their pointfixion is the same by Proposition 9.2.9. Thus we have found $\varphi(s^{\sigma}) \in \mathcal{L}(\tau)$ such that $\hat{\cdot}(\partial_{\Lambda(\tau)}(\varphi(s^{\sigma}))) = s$, so that $s \in \mathcal{O}-\text{Unf}(\tau)$. $\square$

### 9.3.2 Unfolding the Interpretation of IA<sub>//</sub>

Next, we show that $\mathcal{O}-\text{Unf}$ preserves the interpretation of IA<sub>//</sub>.

**Cartesian closed ~-functor.** Recall that on objects, $\mathcal{O}-\text{Unf}(A, \underline{\Delta}, \text{lbl}_A) = \underline{\Delta}$ is a simple forgetful operation. By definition of constructions on mixed boards it follows that $\mathcal{O}-\text{Unf}(-)$ preserves on the nose the interpretation of ground types, products and arrows, and the terminal object. In order to preserve the cartesian closed structure, from the universal property it suffices to preserve projections and the evaluation morphism. For projections, a direct variation of Proposition 9.3.1 shows that

$$ \mathcal{O}-\text{Unf}(\pi_A^!) = \pi_A, \quad \mathcal{O}-\text{Unf}(\pi_B^!) = \pi_B, $$

so that the cartesian structure is preserved in the strict sense. For the evaluation,

$$ \mathcal{O}-\text{Unf}(\Lambda'(\sigma)) = \Lambda(\mathcal{O}-\text{Unf}(\sigma)) $$

follows from a direct verification for $\sigma : !(\Gamma \& A) \vdash B$ with $\Gamma, A$ and $B$ mixed boards: currying is defined on both sides with essentially the same relabeling. It follows that $\mathcal{O}-\text{Unf}$ preserves $\Lambda^{-1}$ as well, and thus the evaluation (which is $\Lambda^{-1}(\text{id}_{A \to B})$).

Overall, we get:

**Theorem 9.3.8.** We have a cartesian closed ~-functor:

$$ \mathcal{O}-\text{Unf}(-) : \dashv\text{-Strat} \to \mathcal{O}\text{-Strat} $$

It is also straightforward that unfolding is continuous with respect to the dcpo structure of hom-sets, so that $\mathcal{O}-\text{Unf}(\mathcal{Y}_A) = \mathcal{Y}_{\underline{A}}$ for any mixed board A.

**Unfolding PIA<sub>//</sub> primitives.** For all the basic primitives of PIA<sub>//</sub> (constants, conditional, sequential composition, operation, sequential and parallel let bindings, reference and semaphore queries, reference and semaphore creation, and bad variable and semaphores), it follows by inspection that they are preserved by unfolding.

Altogether, we get:

**Theorem 9.3.9.** Consider $\Gamma \vdash M : A$ any term of IA<sub>//</sub>. Then,

$$ \mathcal{O}-\text{Unf}(\llbracket M \rrbracket \dashv\text{-Strat}) = \llbracket M \rrbracket \mathcal{O}\text{-Strat}. $$

Along with intentional full abstraction of $\dashv\text{-Strat}$:
**Theorem 9.3.10.** The interpretation of IA<sub>∥</sub> in $\rightarrow$-Strat is intensionally fully abstract.

*Proof.* Consider $\vdash M, N : A$ observationally equivalent and assume $[[M]]_{\rightarrow\text{-Strat}}$ and $[[N]]_{\rightarrow\text{-Strat}}$ are not, i.e. there is $\alpha \in \rightarrow\text{-Strat}([A], U)$ which distinguishes them. Then,

$$ \mathcal{O}\text{-Unf}(\alpha) \in \mathcal{O}\text{-Strat}([A], U) $$

which, by unfolding, distinguishes $[[M]]_{\mathcal{O}\text{-Strat}}$ and $[[N]]_{\mathcal{O}\text{-Strat}}$. But since $\mathcal{O}\text{-Strat}$ is intensionally fully abstract for IA<sub>∥</sub>, this contradicts the obs. equivalence $M \simeq N$. $\square$

In fact, from Theorems 5.3.2 and 9.3.9 we may immediately deduce that

$$ M \simeq N \quad \Leftrightarrow \quad \mathrm{comp}(\mathcal{O}\text{-Unf}([M]_{\rightarrow\text{-Strat}})) = \mathrm{comp}(\mathcal{O}\text{-Unf}([N]_{\rightarrow\text{-Strat}})). $$

## 9.4 History and Related Work

This interpretation of higher-order concurrency into concurrent games (and its non-alternating unfolding) was first introduced in [Castellan and Clairambault, 2016], although for an affine language. The interpretation of non-affine IA<sub>∥</sub> in full concurrent games was first sketched in [Castellan et al., 2019], though without any adequacy or full abstraction result. The overall results presented here, with the unfolding to $\mathcal{O}\text{-Strat}$, were first presented in [Castellan and Clairambault, 2021].

Overall, this forms the first “truly concurrent” model of a higher-order concurrent language with shared memory. Around the same time this was developed, a truly concurrent model of the asynchronous $\pi$-calculus was proposed [Sakayori and Tsukada, 2017].
# Chapter 10

## Parallel Innocence

As we have seen, $\rightarrow$-Strat (and already NTCG) is a wide semantic realm, with strategies witnessing a wealth of computational phenomena: they reflect higher-order concurrent programs, accessing shared state or semaphores. In this permissive universe, can we capture which causal patterns are definable via programs without state, i.e. with only pure parallel higher-order programming? Answering that is the purpose of this chapter, under the form of a condition on strategies called *parallel innocence*.

The outline is as follows. First, in Section 10.1 we introduce the definition of parallel innocence, motivating the different ingredients in sequence – in particular we introduce *visibility*, a first approximation of parallel innocence that already enjoys a number of its properties. Sections 10.2 and 10.3 are devoted to the stability under composition of parallel innocence: first visibility, and then innocence. In Section 10.4 we show that visible strategies admit an interpretation-preserving collapse to the relational model. Finally, in Section 10.5 we refine parallel innocence into *globularity*, that further constrains the causal shape of strategies accounting for Questions and Answers. This is less fundamental, but will be helpful later on for proving finite definability.

**Remark.** In this chapter, the interpretation is used mostly to provide examples. For succinctness, we shall refer in examples to the interpretation using *small* ground boards rather than *large* ground boards (see the beginning of Section 9.1.1). All formal statements on the interpretation hold for both, based on either small or large ground boards.

Besides, though we eventually must consider parallel innocence on the cartesian closed $\sim$-category $\rightarrow$-Strat, this development is completely independent from mixed boards and (logical) well-bracketing – thus, we prefer to develop the theory of parallel innocence for the linear structure, i.e. based on the relative Seely $\sim$-category NTCG. Of course, all the constructions given here will seamlessly apply to $\rightarrow$-Strat as well.
# 10.1 Defining Parallel Innocence

We now embark on our quest to understand the causal shape of pure parallel programs.

## 10.1.1 Causal Determinism

In PCF$_{‖}$, the *parallel let* lets us write programs like

$$ \Gamma \vdash \mathbf{let} \left( \begin{array}{lcl} x & = & f \mathbf{skip} \\ y & = & g \mathbf{skip} \end{array} \right) \mathbf{in} x + y : \mathcal{Y} $$

where the execution of *f skip* and *g skip* are in parallel. The *execution* of this program is non-deterministic: the scheduler must run one of *f skip* and *g skip* first. Nevertheless, one may argue that in PCF$_{‖}$, this order does not matter. Intuitively, we have

$$ f \mathbf{skip} \cdot g \mathbf{skip} \sim g \mathbf{skip} \cdot f \mathbf{skip} $$

if *f skip* and *g skip* perform no side effect, in the sense that the environment has no way to distinguish between the two: whatever the order, the result of the computation will be the same. We say that this program is *causally deterministic*. This is unlike the behaviour of a true non-deterministic primitive such as **choice**.

Of course, IA$_{‖}$ is a truly non-deterministic language (we have seen in Section 2.2.3 how to define **choice** via a race in the memory). However, this true non-determinism emerges from the combination of shared memory and parallelism. Hence, if *parallel innocence* is to remove shared memory, it must also reinstate causal determinism<fnref n="1" />.

**Definition.** While *causal determinism* may be hard to express in traditional, play-based game semantics, it is straightforward to do so for causal strategies: it simply amounts to asking that Player does not impose any minimal conflicts.

**Definition 10.1.1.** Consider $\sigma : A \vdash B$ a causal strategy.

We say $\sigma$ is **causally deterministic** if for all $s \sim_{\sigma} s'$ in $\sigma$, $\text{pol}(s) = \text{pol}(s') = -$.

This rejects a truly non-deterministic strategy such as in Figure 10.1, but accepts strategies such as that in Figure 10.2 where the conflict originates in Opponent moves. Keep in mind that by Lemma 6.1.17, such an immediate conflict between negative events in the strategy *must* correspond to an immediate conflict in the game.

**Copycat strategies.** We show that copycat strategies are deterministic. First:

**Proposition 10.1.2.** For any *--board A*, $\mathfrak{c}_A \in \text{NTCG}(A, A)$ is **causally deterministic**.

*Proof.* Consider $m_1 \sim_{\mathfrak{c}_A} m_2$ in minimal conflict. In particular, $m_1 \#_{\mathfrak{c}_A} m_2$ meaning that by definition, there is $m'_1 \le_{\mathfrak{c}_A} m_1$ and $m'_2 \le_{\mathfrak{c}_A} m_2$ such that

$$ m'_1 \#_{A \vdash A} m'_2 $$

<footnote n="1">¹The status of determinism in concurrent games is unsatisfactory – see Section 14.2.2 for a discussion.</footnote>
<figure><img src="image_164.png" /><figcaption>Figure 10.1: A non-deterministic strategy</figcaption></figure>

<figure><img src="image_165.png" /><figcaption>Figure 10.2: Deterministic copycat</figcaption></figure>

hence there are $m_1'' \le_{A\vdash A} m_1'$ and $m_2'' \le_{A\vdash A} m_2'$ such that $m_1'' \sim_{A\vdash A} m_2''$. Now, by Lemma 6.1.8, $m_1'' \le_{\omega_A} m_1'$ and $m_2'' \le_{\omega_A} m_2'$, so that $m_1'' \le_{\omega_A} m_1$ and $m_2'' \le_{\omega_A} m_2$; and clearly $m_1'' \#_{\omega_A} m_2''$ as they conflict in the game. Thus by minimality, $m_1'' = m_1$ and $m_2'' = m_2$; hence we have shown that for any $m_1 \sim_{\omega_A} m_2$, $m_1 \sim_{A\vdash A} m_2$ as well.

Now assume, seeking a contradiction, that $\text{pol}_{A\vdash A}(m_1) = +$. By condition *race-free* of Definition 8.2.3, it follows that $\text{pol}_{A\vdash A}(m_2) = +$ as well. But then there are unique

$$m_1' \to_{\omega_A} m_1, \quad m_2' \to_{\omega_A} m_2$$

both negative and corresponding to the same event in A. So, $m_1' \sim_{A\vdash A} m_2'$, contradicting the minimality of $m_1 \sim_{\omega_A} m_2$. Hence, $\text{pol}_{A\vdash A}(m_1) = \text{pol}_{A\vdash A}(m_2) = -$. $\square$

For the first time, we have used the condition *race-free* from the definition of boards. Without this condition, a minimal conflict in the game of mixed polarity, as in

$$\oplus \sim \ominus \Theta,$$

causes copycat to be non-deterministic (as the reader may check).

It is straightforward that this applies to all structural morphisms involved in the categorical structure of NTCG, obtained via lifting of renamings – as the renaming operation $g \cdot \sigma \cdot f$ from Section 8.1.2 does not change the strategy, only its display map.

**Composition.** Next, we show preservation under composition. First, we must be able to attribute the responsibility of a minimal conflict to one of the two players.

**Lemma 10.1.3.** Consider $\sigma : A \vdash B$ and $\tau : B \vdash C$ causal strategies.
Then, for each $p \sim_{\tau \oplus \sigma} p'$, one of the two propositions hold:

(1) $p_\sigma, p'_\sigma$ are defined and $p_\sigma \sim_\sigma p'_\sigma$,

(2) $p_\tau, p'_\tau$ are defined and $p_\tau \sim_\tau p'_\tau$.

*Proof.* An equivalent statement of the hypothesis is that we have

$$x^\tau \otimes x^\sigma \subsetneq y^\tau \otimes y^\sigma, \quad x^\tau \otimes x^\sigma \subsetneq z^\tau \otimes z^\sigma$$
with $y^\tau \oplus y^\sigma$, $z^\tau \oplus z^\sigma$ incompatible. By Lemma 6.2.12, this means that we have

$$ \varphi[x^\sigma, x^\tau] \xrightarrow{(m_1, m_2)} \varphi[y^\sigma, y^\tau], \qquad \varphi[x^\sigma, x^\tau] \xrightarrow{(m'_1, m'_2)} \varphi[z^\sigma, z^\tau] $$

with $\varphi[y^\sigma, y^\tau] \cup \varphi[z^\sigma, z^\tau]$ not a secured bijection. This may be because it is not a bijection – say $m_1 = m'_1$ while $m_2 \neq m'_2$. But then $m_2 = (2, t)$ and $m'_2 = (2, t')$ with $\partial_\tau(t) = \partial_\tau(t')$ and thus $t \#_\tau t'$ by local injectivity. Overall, $p_\tau = t$ and $p'_\tau = t'$ are defined and conflicting. Or, this may be because $m_1 \#_{\sigma\|C} m'_1$ or $m_2 \#_{A\|\tau} m'_2$, say the former. If $m_1 = (1, s)$ and $m'_1 = (1, s')$, then $p_\sigma = s$ and $p'_\sigma = s'$ are defined and conflicting. Otherwise, $m_1 = (2, c)$ and $m_2 = (2, c')$ with $c \#_C c'$. But then, necessarily $m_2 = (2, t)$ and $m'_2 = (2, t')$ with $t \#_\tau t'$, thus $p_\tau = t$ and $p'_\tau = t'$ defined and conflicting.

It remains to prove that the resulting conflict is minimal, but that is obvious: if $p_\sigma \#_\sigma p'_\sigma$, all their strict dependency lie in $x^\sigma$ – and symmetrically if $p_\tau \#_\tau p'_\tau$. $\square$

It remains to link minimal conflicts in the composition with the interaction:

**Lemma 10.1.4.** Consider $\sigma : A \vdash B$ and $\tau : B \vdash C$ causal strategies.

If $p \sim_{\tau \odot \sigma} p'$, then we have a diagram in $\tau \oplus \sigma$:

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

with all $q_i$'s synchronized (if $m > 0$) and $q'_i$'s synchronized (if $n > 0$).

*Proof.* Obvious by definition of $\tau \odot \sigma$. $\square$

**Proposition 10.1.5.** Consider $\sigma : A \vdash B$ and $\tau : B \vdash C$ causally deterministic.

Then, $\tau \odot \sigma : A \vdash C$ is causally deterministic.

*Proof.* Consider $p \sim_{\tau \odot \sigma} p'$ a minimal conflict in $\tau \odot \sigma$, and its originating immediate conflict in $\tau \oplus \sigma$ as guaranteed by Lemma 10.1.4. First, assume that $p \sim_{\tau \oplus \sigma} p'$, i.e. $m = n = 0$. By Lemma 10.1.3, this corresponds to an immediate conflict for $\sigma$ or $\tau$ – assume the former, so that $p_\sigma$ and $p'_\sigma$ are defined and $p_\sigma \sim_\sigma p'_\sigma$. But then since $\sigma$ is causally deterministic, those are negative moves, hence negative in $\tau \odot \sigma$ as well.

Otherwise, we have $m > 0$ or $n > 0$, say the former so that the immediate conflict originates in $q \sim_{\tau \oplus \sigma} q'$ with $q$ synchronized. By Lemma 10.1.3, this corresponds to an immediate conflict for $\sigma$ or $\tau$ – assume the former, so that $q_\sigma$ and $q'_\sigma$ are defined and $q_\sigma \sim_\sigma q'_\sigma$. Since $\sigma$ is causally deterministic, $q_\sigma$ and $q'_\sigma$ must be negative and by Lemma 6.1.17, their display to the game are conflicting. But this implies that $q_\tau$ and $q'_\tau$ are defined and conflicting as well. Additionally we must have $q_\tau \sim_\tau q'_\tau$, or we would get a contradiction with the minimality of $q \sim_{\tau \oplus \sigma} q'$. But since $\tau$ is causally deterministic this means that $q_\tau$ and $q'_\tau$ are negative, contradiction. $\square$
<figure><img src="image_167.png" /><figcaption>Figure 10.3: A causal strategy</figcaption></figure>

<figure><img src="image_168.png" /><figcaption>Figure 10.4: Two configurations of Figure 10.3</figcaption></figure>

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

**Full structure.** For remaining operations on strategies (tensor, pairing, currying, promotion), it is immediate by construction that they preserve causal determinism. So:

**Theorem 10.1.6.** *The relative Seely $\sim$-category NTCG admits a lluf relative Seely sub-$\sim$-category NTCG-Det with morphisms restricted to causally deterministic strategies.*

Additionally, the least upper bound of a chain of causally deterministic strategies is still causally deterministic, hence the fixpoint combinator is causally deterministic. It also follows by direct inspection that the strategies used in the interpretation of $\text{PCF}_{\parallel}$ are all causally deterministic; hence for any $\Gamma \vdash M : A$ in $\text{PCF}_{\parallel}$, it follows that

$$[M] \in \text{NTCG-Det}_1([\Gamma], [A]).$$

But causal determinism is not sufficient to characterise pure parallel computation.

## 10.1.2 Pre-innocence

So, what causal shapes are distinctive of pure parallel computation?

Pure parallel programs may spawn parallel threads, which remain independent in the absence of interference. Once they terminate the program may take new actions that depend on their results, causally “merging” them. A typical causal strategy featuring this behaviour, for $x : \mathcal{U}, y : \mathcal{U} \vdash x \parallel y : \mathcal{U}$, appears in Figure 10.6. The slogan is:

*“Player may merge threads than he himself has spawned”.*

In contrast, both diagrams of Figure 10.4 bear signs of interference. In the first, the answer $1^+$ depends on $q^-$: the program somehow observes if the function has called its argument, which is only possible if the argument performs some side-effect that the program observes. In the second, $\check{1}^+$ depends on $\check{q}^-$; but likewise this can only occur if the termination of the function triggers a side-effect. In both cases, this is witnessed by Player “merging” causal chains which forked at Opponent moves.

To ban such interference, the slogan is:

*“Player may not merge threads spawned by Opponent”.*
<figure><img src="image_170.png" /><figcaption>Figure 10.5: Maximal grounded causal chains of a causal strategy</figcaption></figure>

To define parallel innocence, our first step is to introduce a formal notion of “thread”:

**Definition 10.1.7.** Consider A a board, and $\sigma$: A causal strategy.
A grounded causal chain (gcc) in $\sigma$ is $\rho = \{\rho_1, \dots, \rho_n\} \subseteq |\sigma|$ forming

$$ \rho_1 \to_{\sigma} \dots \to_{\sigma} \rho_n $$

a chain with $\rho_1$ minimal with respect to $\leq_{\sigma}$. We write gcc($\sigma$) for the gccs in $\sigma$.

A gcc is just a set, written $\rho = \rho_1 \to_{\sigma} \dots \to_{\sigma} \rho_n \in \text{gcc}(\sigma)$ with the causal ordering from $\leq_{\sigma}$. If also $\rho_1 \to_{\sigma} \dots \to_{\sigma} \rho_n \to_{\sigma} m \in \text{gcc}(\sigma)$, then we write $\rho \to m = \rho \cup \{m\}$. Gccs are not necessarily down-closed: we show in Figure 10.5 all maximal gccs of a causal strategy. Of those, the second and third omit some dependencies of $1^+$.

We may now make formal the idea of “only merging threads forked by Player”.

**Definition 10.1.8.** For A a board, a causally deterministic $\sigma$: A is pre-innocent iff

pre-innocent: If $m^+ \in \sigma$ and $\rho_1 \to m$, $\rho_2 \to m \in \text{gcc}(\sigma)$ are distinct, then $\min(\rho_1) = \min(\rho_2)$ and their least distinct moves are positive.

The strategy of Figure 10.6 is pre-innocent. In contrast, that of Figure 10.3 is not both configurations of Figure 10.4 fail pre-innocence. For instance, the second and third gccs of Figure 10.5 arrive at $1^+$ but before that, the greatest common event is $q^+$, which is positive: Player is merging (via $1^+$) two gccs forked by Opponent.

It will follow later on that the sequential pre-innocent causal strategies exactly match the standard alternating innocent strategies of Definition 3.2.9; see Section 11.3.

However, for non-sequential strategies, pre-innocence is still incomplete.

### 10.1.3 Visibility

The problem arises as non-stability of pre-innocence under composition.
<figure><img src="image_171.png" /><figcaption>Figure 10.6: A typical pre-innocent strat.</figcaption></figure>

<figure><img src="image_172.png" /><figcaption>Figure 10.7: Partiality of views</figcaption></figure>

<figure><img src="image_173.png" /><figcaption>Figure 10.8: A gcc of a non-visible strategy, losing its pointer</figcaption></figure>

A counter-example appears in Figure 10.9, which we postpone to the section devoted to compositionality of innocence. However, we can already explain the issue intuitively: the definition of pre-innocence relies on gccs which formalize a notion of *thread*. If that intuition is to be taken seriously, gccs should be valid executions of standalone sequential programs. But this is not the case: Figure 10.8 shows a gcc where the last move answers a question that *was not asked* within this gcc. This could not be a valid state of a sequential program, because the last move *loses its pointer*.

*Visible* strategies are simply those such that this does not happen.

**Definition 10.1.9.** A *causal strategy* $\sigma : A$ is *visible* if it is:

pointed: for any $s \in \sigma$, there is a unique $init(s) \leq_{\sigma} s$ minimal in $\sigma$,
valid-gccs: for all $\rho \in gcc(\sigma)$, $\partial_{\sigma}(\rho) \in \mathscr{C}(A)$.

We smuggle in *pointed*, which ensures that separate initial Opponent moves explore
causally independent parts of the strategy. It is necessary for our proof of composition
of visibility, but it is clearly less important than *valid-gccs*, mainly because it is already
implied by pre-innocence (and also, automatic for $\sigma : A \vdash B$ with $B$ strict). Hence,
we shall tend in the future to brush over *pointed*, and identify *visible* and *valid-gccs*.

*Valid-gccs* means that every move in $\rho$ points within $\rho$. This phrasing highlights the
analogy with Definition 3.2.8, i.e. "Player always points in the P-view". It is indeed this
analogy that inspired the name<fnref n="2" />. But one must be wary: the alternating interpretation of sequential programs with state yields sequential P-visible strategies, but their causal interpretation (as in Figure 10.3) may not be visible. Visibility is very restrictive, it is not clear what sensible primitive would satisfy visibility but not pre-innocence.

The following lemma captures how a gcc may be regarded as a standalone thread.

**Lemma 10.1.10.** Consider A a mixed board, and $\sigma$: A a visible causal strategy.
If $\rho = \rho_1 \to_{\sigma} \dots \to_{\sigma} \rho_n \in \text{gcc}(\sigma)$, ($\hat{\circ}$)($\partial_{\sigma}(\rho)$) = ($\hat{\circ}$)($\partial_{\sigma}(\rho_1)$ ... $\partial_{\sigma}(\rho_n)$) is a P-view.

*Proof.* By Lemma 6.1.16, $\partial_{\sigma}(\rho)$ is alternating. By visibility, its prefixes are configurations of A. So, $\partial_{\sigma}(\rho) \in \text{↓↑-Plays}(A)$. By Lemma 6.1.16 again, the predecessor of $a^- \in \partial_{\sigma}(\rho)$ for $\to_A$ is its predecessor in $\partial_{\sigma}(\rho)$, i.e. Opponent always points to the previous move. The statement follows by definition of pointfixion. $\square$

We may now define *parallel innocent* causal strategies, or just *innocent* for short.

**Definition 10.1.11.** Consider $\sigma$: A causally deterministic on board A.
*It is parallel innocent* if it is pre-innocent and *visible*.

A standard innocent strategy as in Section 3.2.3, under its “causal” presentation, is a forest of P-views, i.e. a forest of (displayed) gccs. In that light the definition of parallel innocent strategies seems natural: they are generated no longer by a forest of P-views, but by a directed acyclic graph of P-views with additional conflict relation. This graph describes how threads are spawned, and then may merge, following the innocence discipline ensuring that Player may not create interference between Opponent's threads.

One of the main hurdles, in traditional game semantics, is to prove that innocent strategies compose. We now tackle this problem for parallel innocent strategies.

# 10.2 Composition of Visibility

First, we establish compositionality of visibility.

## 10.2.1 Justifiers in causal strategies

We introduce some machinery on *justifiers*. If $\sigma$: A is a causal strategy on A some --board, then as for plays, the immediate causality in A endows moves in $\sigma$ with a notion of *justifier*. This extends to $\sigma$: A $\vdash$ B where A and B are --boards:

**Definition 10.2.1.** Consider A and B --boards, and $\sigma$: A $\vdash$ B pointed.
We define the *justifiers* in $\sigma$ by setting, for all $m, m' \in \sigma$,

$j(m) = m'$ if $\partial_{\sigma}(m') \to_{A \vdash B} \partial_{\sigma}(m)$,

$j(m) = \text{init}(m)$ if $\partial_{\sigma}(m)$ minimal in A,

and undefined otherwise.

<footnote n="2">²This, plus as in traditional game semantics, visibility is a prerequisite for a working notion of innocence.</footnote>
Since A and B are forestial and $\sigma$ is pointed, $j(-)$ is well-defined as a partial function on $\sigma$, only left undefined for $m \in \sigma$ minimal in $\sigma$. Note that assigning the justifier of $m$ minimal in A to init($m$) ensures that the assignment of justifiers is invariant under currying. It might be helpful to the reader to observe that a pointed causal strategy $\sigma: A \vdash B$ is visible iff for all $\rho \in \text{gcc}(\sigma)$, for all $m \in \rho$, $j(m) \in \rho$ as well: all gccs are closed under justifiers. We mention in passing this lemma:

**Lemma 10.2.2.** *Consider A, B --boards and $\sigma: A \vdash B$ a pointed causal strategy.*

Then, for any non-initial $m \in \sigma$, we have $j(m) <_{\sigma} m$. Moreover, if $\text{pol}_{\sigma}(m) = -$, then $j(m) \to_{\sigma} m$ is its (unique) immediate predecessor in $\sigma$.

*Proof.* As a map of es, $\partial_{\sigma}$ locally reflects causality (Lemma 6.1.8), so $j(m) <_{\sigma} m$ if the first clause of Definition 10.2.1 applies; for the other we clearly have init($m$) <$_{\sigma}$ $m$. The second fact is simply by Lemma 6.1.16. $\square$

## 10.2.2 Justifiers in interactions

So as to prove visibility stable under composition, we first extend justifiers to interactions – consider A, B and C three --boards, and $\sigma: A \vdash B$ and $\tau: B \vdash C$ pointed.

**Definition 10.2.3.** We define $j: |\tau \otimes \sigma| \to |\tau \otimes \sigma|$ as $j(m) = m'$ if:

(1) $\partial_{\tau \otimes \sigma}(m') \to_{A \parallel B \parallel C} \partial_{\tau \otimes \sigma}(m)$, or

(2) $\partial_{\tau \otimes \sigma}(m)$ is minimal in A and $m'_{\sigma} = \text{init}(m_{\sigma})$, or

(3) $\partial_{\tau \otimes \sigma}(m)$ is minimal in B and $m'_{\tau} = \text{init}(m_{\tau})$,

and undefined otherwise. We say that $m'$ is the justifier of $m$ in $\tau \otimes \sigma$.

This leaves $j(m)$ undefined exactly if it corresponds to a minimal move in C. Clearly the two notions of justifier are compatible, in the sense that for all $m \in \tau \otimes \sigma$, if $m_{\sigma}$ is defined then $j(m)_{\sigma}$ is defined and equal to $j(m_{\sigma})$, and likewise for $\tau$.

## 10.2.3 Views of gccs

We introduce the main technical device on visible causal interactions.

We use polarities in interactions as in Lemma 6.2.15, and annotate events accordingly. We also write e.g. $a^{-}, r^{\prime}$ to indicate that $a$ has polarity $-$ or $r$. If $\rho \in \text{gcc}(\tau \otimes \sigma)$ with last event $m$, we say that $\rho$ ends in $\sigma$ if $m_{\sigma}$ is defined, and likewise for $\tau$. We now define views of gccs, used to project a gcc of the interaction to gccs for both strategies.

**Definition 10.2.4.** *Take $\sigma: A \vdash B$ and $\tau: B \vdash C$ pointed with A, B, C --boards.*

If $\rho \in \text{gcc}(\tau \otimes \sigma)$ ends in $\sigma$, we (partially) define $\lceil \rho \rceil^{\sigma} \in \text{gcc}(\sigma)$ by:

$$ \lceil \rho_0 \to \dots \to \rho_n \to \rho_{n+1}^{\prime} \rceil^{\neg \sigma} = \lceil \rho_0 \to \dots \to \rho_n \rceil^{\neg \sigma} \cup \{(\rho_{n+1})_{\sigma}\}, $$

$$ \lceil \rho_0 \to \dots \to \rho_i \to \dots \to \rho_{i+1}^{\prime} \rceil^{\neg \sigma} = \lceil \rho_0 \to \dots \to \rho_i \rceil^{\neg \sigma} \cup \{(\rho_{i+1})_{\sigma}\} \quad \text{if } j(\rho_{i+1}) = \rho_i \text{ in A or B,} $$

$$ \lceil \rho_0 \to \dots \to \rho_i \to \dots \to \rho_{i+1}^{\prime} \rceil^{\neg \sigma} = \{(\rho_{i+1})_{\sigma}\} \quad \text{if } \rho_{i+1} \text{ minimal in B,} $$

undefined otherwise. If $\rho \in \text{gcc}(\tau \otimes \sigma)$ ends in $\tau$, we (partially) define $\lceil \rho \rceil^{\tau} \in \text{gcc}(\tau)$:

$$ \lceil \rho_0 \to \dots \to \rho_n \to \rho_{n+1}^{\prime} \rceil^{\neg \tau} = \lceil \rho_0 \to \dots \to \rho_n \rceil^{\neg \tau} \cup \{(\rho_{n+1})_{\tau}\}, $$

$$ \lceil \rho_0 \to \dots \to \rho_i \to \dots \to \rho_{i+1}^{\prime} \rceil^{\neg \tau} = \lceil \rho_0 \to \dots \to \rho_i \rceil^{\neg \tau} \cup \{(\rho_{i+1})_{\tau}\} \quad \text{if } j(\rho_{i+1}) = \rho_i; $$
when defined, $\lceil \rho \rceil^{\sigma} \in \text{gcc}(\sigma)$ is the $\sigma$-view of $\rho$ and $\lceil \rho \rceil^{\tau} \in \text{gcc}(\tau)$ the $\tau$-view of $\rho$.

These definitions closely follow Definition 3.2.7. The last clause is only needed for $\lceil - \rceil^{\sigma}$ and not $\lceil - \rceil^{\tau}$, because an initial event in $C$ must be the first event of $\rho$ anyway.

That this yields `gccs` of $\sigma$ and $\tau$ rests on Lemma 6.2.15, and courtesy of $\sigma$ and $\tau$. The $\sigma$-view and the $\tau$-view are in principle only partially defined, because it may be, when attempting to follow the opponent's pointer, that that justifier lies outside the `gcc`. For instance $\lceil \rho \rceil^{\tau}$, for $\rho$ in Figure 10.7, is not well-defined: when attempting to compute $\lceil \mathbf{q}^- \mathbf{q}' \rfloor \lceil \mathbf{q}' \rceil \lceil \tau \rceil$, none of the clauses apply as $j(\lceil \mathbf{q}' \rceil) = \mathbf{q}'$ is outside $\rho$. The bulk of the proof of stability of visibility under composition, is to show that this cannot happen:

**Proposition 10.2.5.** Let $\sigma : A \vdash B$ and $\tau : B \vdash C$ be visible causal strategies. Then, the views of `gccs` of $\tau \otimes \sigma$ as in Definition 10.2.4 are always well-defined.

*Proof.* We prove by induction on $\rho$ that, for all prefixes of $\rho$,

(1) if $\rho$ ends in $\sigma$, then $\lceil \rho \rceil^{\sigma} \in \text{gcc}(\sigma)$ is well-defined,

(2) if $\rho$ ends in $\tau$, then $\lceil \rho \rceil^{\tau} \in \text{gcc}(\tau)$ is well-defined.

Assume $\rho$ ends in $\tau$. If the last move has polarity $-$, then either it is initial and there is nothing to prove, or by Lemma 6.2.15 its justifier is its predecessor in $\rho$, so $\lceil \rho \rceil^{\tau} \in \text{gcc}(\tau)$ follows by induction hypothesis (in that case $\rho$ does not end in $\sigma$).

If the last move has polarity, write $\rho = \rho' \to m \to n'$. By Lemma 6.2.15, $m_{\tau} \to_{\tau} n_{\tau}$, so $m$ is in $\tau$. By induction hypothesis, $\kappa = \lceil \rho' \rceil \to \mathbf{m}^{\lceil \tau \rceil} \in \text{gcc}(\tau)$, so

$$ \kappa \to n_{\tau} = \lceil \rho \rceil^{\tau} \in \text{gcc}(\tau) $$

as well. But if $\rho$ ends in $\sigma$ and $\tau$ (i.e. in $B$), we must further prove that $\lceil \rho \rceil^{\sigma} \in \text{gcc}(\sigma)$. In that case, since $\lceil \rho \rceil^{\tau} \in \text{gcc}(\tau)$ and $\tau$ is visible, it follows that $j(n_{\tau}) \in \lceil \rho \rceil^{\tau}$, but this entails $j(n) \in \rho$. Hence the second clause of Definition 10.2.4 applies, and we conclude by induction hypothesis. If $\rho$ finishes in $\sigma$, the reasoning is symmetric. $\square$

From this, we are now ready to conclude:

**Proposition 10.2.6.** Let $\sigma : A \vdash B$ and $\tau : B \vdash C$ be visible causal strategies. Then, $\tau \odot \sigma : A \vdash C$ is also visible.

*Proof.* First, we show that $\tau \odot \sigma$ is pointed. there are distinct $q, q' \in \tau \odot \sigma$ minimal such that $q \le_{\tau \odot \sigma} p$ and $q' \le_{\tau \odot \sigma} p$. It is a direct consequence of courtesy (via Lemma 6.1.16) that then, $q, q'$ must still be minimal in $\tau \otimes \sigma$. Then there must be some $r$ in $\tau \otimes \sigma$ minimal such that there is $m \to_{\tau \otimes \sigma} r$ and $n \to_{\tau \otimes \sigma} r$ with $[m]_{\tau \otimes \sigma}$ and $[n]_{\tau \otimes \sigma}$ disjoint. Now, we distinguish cases depending on the polarity of $r$. If it is $\ell$, then by Lemma 6.2.15, $m_{\sigma}$ and $n_{\sigma}$ are defined and $m_{\sigma} \to_{\sigma} r_{\sigma}$ and $n_{\sigma} \to_{\sigma} r_{\sigma}$. But since $\sigma$ is pointed, $[m_{\sigma}]_{\sigma}$ and $[n_{\sigma}]_{\sigma}$ cannot be disjoint, contradiction. The case for $r$ is symmetric.

Now, we show visibility. For that, we prove by induction on $\rho$ that for all $\rho \in \text{gcc}(\tau \otimes \sigma)$, $\partial_{\tau \otimes \sigma}(\rho) \in \mathcal{C}(A \parallel B \parallel C)$. If $\rho$ is empty it is clear; take $\rho \to m \in \text{gcc}(\tau \otimes \sigma)$. By induction hypothesis, $\partial_{\tau \otimes \sigma}(\rho) \in \mathcal{C}(A \parallel B \parallel C)$, we only need that the justifier of $m$ is in $\rho$. We reason by cases on the polarity of $m$: if it is $\ell$, then by Proposition 10.2.5 $\lceil \rho \rceil \to \mathbf{m}^{\lceil \sigma \rceil} \in \text{gcc}(\sigma)$. But since $\sigma$ is visible, the justifier of $m_{\sigma}$ appears in $\lceil \rho \rceil^{\sigma}$, hence
<figure><img src="image_174.png" /><figcaption>Figure 10.9: Failure of preservation of pre-innocence under composition</figcaption></figure>

the justifier of *m* appears in *ρ*. The other cases are symmetric or trivial.

Now, take $\rho_{\odot} \in \text{gcc}(\tau \odot \sigma)$. By definition of $\tau \odot \sigma$, there is a (non-necessarily unique) $\rho_{\oplus} \in \text{gcc}(\tau \oplus \sigma)$ s.t. $\rho_{\odot}$ comprises exactly those events of $\rho_{\oplus}$ in $A$ or $C$. By the observation above, $\partial_{\tau \oplus \sigma}(\rho_{\oplus}) \in \mathscr{C}(A \parallel B \parallel C)$, hence $\partial_{\tau \odot \sigma}(\rho_{\odot}) \in \mathscr{C}(A \parallel C)$. $\square$

### 10.2.4 The Relative Seely ~-Category NTCG-Vis

In this monograph, we are particularly interested in visibility as a means to ensure that innocence is preserved under composition. However, it is noteworthy that visibility indeed supports all the constructions involved in the relative Seely category structure.

**Theorem 10.2.7.** *There is NTCG-Vis, a relative Seely sub-~-category of NTCG, with morphisms restricted to visible causal strategies.*

*Proof.* As causality in boards is forestal, so is the causality of copycat – it follows immediately that copycat is visible, and this immediately extends to lifted strategies. By Proposition 10.2.6, visibility is stable under composition. For all other operations (tensor, pairing, currying, promotions), it is immediate that visibility is preserved. $\square$

This extends to the fixpoint operation and – by inspection – to all primitive strategies involved in the interpretation of $\text{PCF}_{\parallel}$, so that any term $\Gamma \vdash M : A$ of $\text{PCF}_{\parallel}$ yields a visible causal strategy $[M] \in \text{NTCG-Vis}_i([\Gamma], [A])$. In contrast, the interpretation of $\text{IA}_{\parallel}$ does not satisfy visibility: the non-visible behaviour from Figure 10.8 comes from

$$ \vdash \mathbf{newref} \ x \ \mathbf{in} \ \lambda f \upharpoonright_{U \to U} f \ (x := tt); \ !r \ : (U \to U) \to \mathbb{B}, \quad (10.1) $$

a term of IA. Though visibility does not match tightly any of our programming languages, it will play in important role in this work. But next, we show that in the presence of visibility, innocence becomes stable under composition.

## 10.3 Composition of Innocence

We start by showing “what could go wrong”. In Figure 10.9, we show a counter-
<figure><img src="image_175.png" /><figcaption>Figure 10.10: Illegal causal merge</figcaption></figure>

<figure><img src="image_176.png" /><figcaption>Figure 10.11: Merging paths in $G$</figcaption></figure>

example to the stability under composition of pre-innocence without visibility, with the
corresponding interaction appearing as Figure 10.10. Let us attempt to explain the phe-
nomenon, calling $\sigma$ the left hand side strategy (parallel composition) and $\tau$ the right
hand side one – observe that the dotted lines include the justification relations from
Definition 10.2.1 rather than just those coming from the arena. Imagine that $\tau$ wants to
perform an illegal causal merge between the two argument calls of its argument of type
$U \to U \to U$. By pre-innocence it cannot do so directly. However, it can outsource the
merge to $\sigma$ by linking (legally with respect to pre-innocence, but illegally with respect
to visibility) the arguments of the parallel composition to those that it wants to merge.

We shall prove that this cannot happen in the presence of visibility. Let us fix, until
the end of the section, two visible causal strategies $\sigma : A \vdash B$ and $\tau : B \vdash C$.

**10.3.1 The “forking lemma”**

Taking a closer look at Figure 10.10, we highlight the two illegally merging gccs in the
interaction: while $\sigma$ is responsible for the merge, the point where these gccs forked is
external, outside the scope of $\sigma$! The next lemma, dubbed the “forking lemma”, forbids
this: it implies that visible strategies cannot unknowingly close an Opponent fork.

If $\rho = \rho_1 \to \dots \to \rho_n$ is a gcc and $1 \le i \le n$, $\rho_{\le i}$ is $\rho_1 \to \dots \to \rho_i$. Two gccs $\rho, \kappa$ are **forking** iff $\rho \cap \kappa \ne \emptyset$, and for all $i, j$, if $\rho_i = \kappa_j$ then $\rho_{\le i} = \kappa_{\le j}$. If $\rho, \kappa$ are two forking gccs, we write $gce(\rho, \kappa)$ for their **greatest common event**. Notice that despite the terminology, two forking gccs can be prefix of one another and never truly go separate ways; but if they do diverge, their remainder must be independent.

**Lemma 10.3.1 (Forking lemma).** Consiser $\sigma : A \vdash B$ and $\tau : B \vdash C$ visible strategies. Let $\rho, \kappa \in gcc(\tau \oplus \sigma)$ be forking gccs ending in $\sigma$, s.t. $\lceil \rho \rceil^{\sigma} \cap \lceil \kappa \rceil^{\sigma} \ne \emptyset$ and gce($\lceil \rho \rceil^{\sigma}, \lceil \kappa \rceil^{\sigma}$) negative (the least distinct events, if any, are positive).
Then, gce(Γρ⁻⁷σ, Γκ⁻⁷σ) = gce(ρ, κ)ₐ. The symmetric property holds for τ.

*Proof.* We only detail the proof for σ, the proof for τ is exactly the same. We build a directed graph G with vertices ρ ∪ κ, and edges the (disjoint) union of the sets:

$$
\begin{align*}
\text{O-edges} &= \{(m_1, m_2^\ell) \mid j(m_1) = m_2\} \\
\text{P-edges} &= \{(m_1^\ell, m_2) \mid m_2 \to_{\tau \otimes \sigma} m_1\}
\end{align*}
$$

where (−)ᶜ indicates the polarity. Each vertex is source of at most one edge, and fol-
lowing edges consists exactly in computing the σ-view. If ρ and κ have the same final
move, then ρ = κ. Otherwise, consider the two paths in G starting with these distinct
final moves. Since ⌜ρ⌝<sup>σ</sup> ∩ ⌜κ⌝<sup>σ</sup> ≠ ∅, these paths must intersect – Figure 10.11 repre-
sents a typical G with O-edges in blue and P-edges in red with the two typical cases.

These paths meet at a vertex of incoming degree at least 2; but vertices receive only O-edges, or only P-edges. For the former (as in the bottom of Figure 10.11), then gce(Γρ⁻⁷σ, Γκ⁻⁷σ) is positive, which contradicts the hypothesis. For the latter (as in the top of Figure 10.11), we remark that P-edges are immediate causal links in τ ⊗ σ; and there is at most one event in ρ ∪ κ causing two distinct events: gce(ρ, κ). □

This provides the core argument for the compositionality of pre-innocence: if a pre-
innocent strategy merges two threads, by pre-innocence its *views* of these two threads
fork positively. But then the forking lemma ensures that this strategy sees the actual
forking point for these threads – which therefore cannot be due to the external Opponent.

**10.3.2 Stability of pre-innocence**

Now, much of the proof consists in restricting the causal shapes in τ ⊗ σ corresponding
to a causal merge in τ ⊙ σ, so that the forking lemma applies.

**Proposition 10.3.2.** Consider *σ* : A ⊢ B and *τ* : C ⊢ C visible causal strategies.
If *σ* : A ⊢ B and *τ* : B ⊢ C are pre-innocent, then so is *τ* ⊙ *σ*.

*Proof.* Consider $m \in \tau \odot \sigma$ and distinct $\rho^1 \to m, \rho^2 \to m \in \text{gcc}(\tau \odot \sigma)$. W.l.o.g. assume that whenever $\rho_i^1 = \rho_j^2, \rho_{\le i}^1 = \rho_{\le j}^2$ – or we can ensure this by changing $m$ and $\rho^i$, keeping the same least distinct events. Likewise, since $\rho^1, \rho^2$ are distinct, w.l.o.g. their last moves $m_1 \in \rho^1, m_2 \in \rho^2$ are distinct – or we may replace $m$ with an earlier causal merge. These gccs $\rho^1$ and $\rho^2$ may be completed to $\kappa^1 \to m, \kappa^2 \to m \in \text{gcc}(\tau \oplus \sigma)$ such that $\rho^i$ consists exactly of the events of $\kappa^i$ occurring in A or C. Necessarily, the greatest visible events of $\kappa^1$ and $\kappa^2$ are $m_1$ and $m_2$ respectively. Call $n$ the least common event of $\kappa^1 \to m$ and $\kappa^2 \to m$ above $m_1$ and $m_2$ (which might not be $m$). The situation is:

<figure><img src="image_177.png" /></figure>
with $m_1, m_2$ and $m$ visible, and no one visible in between. We reason on the polarity of $n$ in $\tau \otimes \sigma$. By Lemma 6.2.15 and since arenas are forestial, it cannot be negative, so its polarity is either $\ell$ or $r$. Assume it is $\ell$ – the other case is symmetric.

The polarity of $n$ is positive for $\sigma$, so we compute the $\sigma$-views:

$$ \Gamma_{\kappa_{\le n}^1} \to n^{\neg\sigma}, \quad \Gamma_{\kappa_{\le p}^2} \to n^{\neg\sigma} \in \text{gcc}(\sigma), $$

respectively $\Gamma_{\kappa_{\le n}^1} \neg\sigma \to n_\sigma$ and $\Gamma_{\kappa_{\le p}^2} \neg\sigma \to n_\sigma$, with $\Gamma_{\kappa_{\le n}^1} \neg\sigma$ and $\Gamma_{\kappa_{\le p}^2} \neg\sigma$ distinct as they respectively contain $\kappa_n^1$ and $\kappa_p^2$. Since $\sigma$ is pointed, $\Gamma_{\kappa_{\le n}^1} \neg\sigma \cap \Gamma_{\kappa_{\le p}^2} \neg\sigma \neq \emptyset$, so $\kappa^1 \cap \kappa^2 \neq \emptyset$ as well. Call $m'$ the gce of $\kappa^1$ and $\kappa^2$, necessarily below $m_1$ and $m_2$, then:

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

assuming w.l.o.g. that $\kappa_{\le i}^1 = \kappa_{\le i}^2$ (changing the beginning of $\kappa^2$ if required). Summing up some properties, $\xi^1 = \kappa_{i+1}^1 \dots \kappa_n^1$ and $\xi^2 = \kappa_{i+1}^2 \dots \kappa_p^2$ are disjoint. Thus the $\sigma$-views

$$ \Gamma_{\kappa_{\le n}^1} \neg\sigma, \quad \Gamma_{\kappa_{\le p}^2} \neg\sigma \in \text{gcc}(\sigma) $$

are forking: they coincide on a prefix and disjoint after. Indeed, since $\xi^1$ and $\xi^2$ are disjoint, any common event is in $\kappa_1^1 \to \dots \to \kappa_i^1$, before which the $\sigma$-views coincide.

Since $\sigma$ is pre-innocent, the least distinct moves $m'_1$ and $m'_2$ of $\Gamma_{\kappa_{\le n}^1} \neg\sigma$ and $\Gamma_{\kappa_{\le p}^2} \neg\sigma$ are positive. Thus their common immediate predecessor is negative – but it is also their greatest common event, since $\Gamma_{\kappa_{\le n}^1} \neg\sigma$ and $\Gamma_{\kappa_{\le p}^2} \neg\sigma$ are forking. Thus by Lemma 10.3.1,

$$ \text{gce}(\Gamma_{\kappa_{\le n}^1} \neg\sigma, \Gamma_{\kappa_{\le p}^2} \neg\sigma) = \text{gce}(\kappa_{\le n}^1, \kappa_{\le p}^2)_\sigma = m'_\sigma, $$

so $m'$ is negative for $\sigma$. In $\tau \otimes \sigma$, $m'$ is negative or in $B$ – in both cases the least visible events in $\xi^1$ and $\xi^2$ are positive, but those are our least distinct events of $\rho_1$ and $\rho_2$. $\square$

### 10.3.3 The Relative Seely Category NTCG-Inn

As for visibility, we have:

**Theorem 10.3.3.** *There is NTCG-Inn, a relative Seely sub-~category of NTCG-Det, with morphisms restricted to parallel innocent causal strategies.*

*Proof.* For composition, this is via Propositions 10.1.5, 10.2.6 and 10.3.2. Parallel innocence of copycat is immediate, and that extends to lifted strategies. For all other operations on strategies, preservation of innocence is direct. $\square$
Again this extends to the fixpoint operation and to all primitive strategies involved in the interpretation of PCF<sub>∥</sub>, so that any term Γ ⊢ M : A of PCF<sub>∥</sub> yields

$$[[M]] \in \mathbf{NTCG-Inn}_i([\Gamma], [A])$$

a parallel innocent strategy.

Note that though we bundled causal determinism with parallel innocence in this monograph, they are actually independent in the sense that stability under composition of parallel innocence does not need causal determinism. However, without determinism, parallel innocence as presented here is insufficient to obtain a definability result for a non-deterministic extension of PCF<sub>∥</sub>. We have not yet been able to give a working notion of non-deterministic parallel innocence – see Section 14.2.1 for a discussion.

### 10.3.4 Complement: the “Bang Lemma”

Within the relative Seely ~-category NTCG-Inn, one can prove the “bang lemma” from AJM games [Abramsky et al., 2000] – it is an important technical lemma expressing that essentially, all innocent strategies on !A ⊢ !B are the promotion of some strategy on !A ⊢ B. Note that this does not hold without innocence: a non-innocent strategy on !B may very well impose constraints across its different copies. In AJM games, the bang lemma depends on history-freeness; it does not exist in HO games in the absence of a linear decomposition. Fix A and B two strict boards, and σ : !A ⊢ !B innocent.

A minimal $m \in \sigma$ displays to $\partial_{\sigma}(m) = (2, (i, b))$ for some $i \in \mathbb{N}$ – we say that $m$ is in copy $i$. Being innocent, $\sigma$ is pointed and every event has a unique minimal cause; so we say that arbitrary $m \in \sigma$ is in copy $i$ if its unique minimal cause is. Let us write

$$|\sigma_i| = \{m \in |\sigma| \mid m \text{ is in copy } i\}$$

for the set of events of $\sigma$ in copy $i$. By construction, for $i, j \in \mathbb{N}$ distinct, $|\sigma_i|$ and $|\sigma_j|$ are disjoint, and each inherit from $\sigma$ the structure of an ess. Furthermore, $\sigma_i : !A \vdash B$ with the display map $\partial_{\sigma_i}$ defined in the obvious way. Moreover, we have:

**Lemma 10.3.4.** As event structures with symmetries, we have $\sigma \cong \|_{i \in \mathbb{N}} \sigma_i$.

*Proof.* The non-trivial point is that no immediate conflict in $\sigma$ can span across copies: if $s \sim_{\sigma} s'$ then $\text{pol}(s) = \text{pol}(s') = -$ by causal determinism, and $\partial_{\sigma}(s) \sim \partial_{\sigma}(s')$ as well by Lemma 6.1.17. By definition of bang, this entails that $\partial_{\sigma}(s)$ and $\partial_{\sigma}(s')$ are in a common copy of $B$, or of $A$. If it is $B$ then we are done. If it is $A$ then from polarity reasons they cannot be minimal in $A$, and since $A$ is strict this entails that they are above (for $\le_{!A}$) the same minimal event in $A$. So $s$ and $s'$ are above a common move in $\sigma$, which entails that they are in the same copy. $\square$

They key argument, in the bang lemma, is that these copies are interchangeable:

**Lemma 10.3.5.** For any $i, j \in \mathbb{N}$, we have $\sigma_i \approx \sigma_j$.
*Proof.* We exploit Lemma 7.1.9 and build an iso between the domains of configurations, compatible with symmetry. Consider $x_i \in \mathscr{C}(\sigma_i)$, displaying to

$$ \partial_{\sigma}(x_i) = x_A \| \{i\} \times x_B. $$

By definition of the board constructions, there is a symmetry exchanging $i$ and $j$:

$$ \theta_{i,j}^{-} : x_A \| \{i\} \times x_B \cong_{!A \vdash !B} x_A \| \{j\} \times x_B, $$

and our isomorphism will transport $x_i$ along this negative symmetry. Indeed by Lemma 7.2.6, there are unique $x_j \in \mathscr{C}(\sigma_j)$ and $\psi : x_i \cong_{\sigma} x_j$ s.t. $\partial_{\sigma}\psi = \theta^+ \circ \theta_{i,j}^-$ for some

$$ \theta^+ : x_A \| \{j\} \times x_B \cong_{!A \| !B} y_A \| \{j\} \times y_B $$

where we know that $j$ is unchanged by definition of the positive symmetries of the bang. Therefore, $x_j \in \mathscr{C}(\sigma_j)$ as required. Monotonicity of this operation and the fact that it is a bijection between configurations follow from the *uniqueness* clause for Lemma 7.2.6; compatibility with symmetry follows from composition with the symmetry $\psi$.

This induces an isomorphism of ess $\varphi : \sigma_i \approx \sigma_j$ which we must still check is a positive isomorphism. But for $x_i \in \mathscr{C}(\sigma_i)$, the symmetry $\theta^+$ above entails

$$ \partial_{\sigma}(x_i) = x_A \| x_B \stackrel{\varphi^+}{\cong}_{!A \vdash B} y_A \| y_B = \partial_{\sigma}(x_j) $$

ensuring that the triangle commutes up to positive symmetry as required. $\square$

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

Next we lift a positive isomorphism on one copy index to the whole strategy:

**Lemma 10.3.6.** Consider A and B strict boards, and $\sigma, \tau : !A \vdash !B$ parallel innocent.
If $\sigma_0 \approx \tau_0$, then $\sigma \approx \tau$.

*Proof.* By Lemma 10.3.5, for $i \in \mathbb{N}$, $\sigma_i \approx \sigma_0 \approx \tau_0 \approx \tau_i$, and thus we have

$$ \|_{i \in \mathbb{N}} \sigma_i \approx \|_{i \in \mathbb{N}} \tau_i $$

lifted to an isomorphism of ess $\sigma \cong \tau$ by Lemma 10.3.4. It is then straightforward that this isomorphisms is compatible with display maps up to positive symmetries. $\square$

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

We may finally deduce the bang lemma:

**Lemma 10.3.7.** For A, B strict boards and $\sigma \in \text{NTCG-Inn}(!A, !B)$ parallel innocent,

$$ (\mathrm{der}_B \odot \sigma)^! \approx \sigma. $$

*Proof.* From Proposition 7.3.1, it is direct to establish $\mathrm{der}_B \odot \sigma \approx \sigma_0$. Therefore, by Lemma 10.3.6, for any $\sigma, \tau : !A \vdash !B$, if $\mathrm{der}_B \odot \sigma \approx \mathrm{der}_B \odot \tau$, then $\sigma \approx \tau$. Now as

$$ \mathrm{der}_B \odot (\mathrm{der}_B \odot \sigma)^{\dagger} \approx \mathrm{der}_B \odot \sigma $$

by the laws of relative Seely categories, the lemma follows. $\square$

<figure><img src="image_181.png" /></figure>
<figure><img src="image_182.png" /><figcaption>Figure 10.12: A witness and its display</figcaption></figure>

## 10.4 Relational Collapse

Most consequences of parallel innocence will be presented in Chapter 12, when we focus on finite definability for those and intensional full abstraction for PCF. But we explore now a crucial consequence of parallel innocence (more precisely, of visibility): it allows a simple, transparent translation to the relational model. This will be useful technically later on, but we also regard this as an important contribution in its own right.

### 10.4.1 Stopping Positions and Witnesses

Intuitively, a causal strategy records observable computational events, along with the causal dependencies between them, but we may also regard it as presenting all positions reached in the sense of the relational model, enriching them with causal information.

**Forgetting causality.** Recall that a causal strategy $\sigma: A$ on $--board A$ is specified by an internal event structure $\sigma$, along with a *display map*

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

A configuration $x_A \in \mathscr{C}(A)$ is **reached by $\sigma$** iff there is $x^\sigma \in \mathscr{C}(\sigma)$, its **witness**, such that $\partial_\sigma x^\sigma = x_A$. Intuitively, and as a first approximation, the relational model only remembers which configurations $x_A \in \mathscr{C}(A)$ have a witness (though we shall see below that the relational model only tracks certain configurations considered as *completed* executions, and that *symmetry* entails that points in the relational models should be certain symmetry classes rather than mere configurations).

As an example, we show in Figure 10.12 a configuration of the strategy $\sigma$ for

$$ \vdash \lambda f^{U \to U}. f \text{skip}; f \text{skip}; tt : (U \to U) \to \mathbb{B}; $$

where the configuration appears on the left hand side. This diagram follows our long-standing convention to draw $x^\sigma \in \mathscr{C}(\sigma)$ with events displayed as their image via $\partial_\sigma$,
with the diagram showing immediate causality both in $\sigma$ (drawn as $\rightarrow$) and in $A$ (drawn as dotted lines). Thus, its display via $\partial_{\sigma}$ is obtained diagrammatically simply as the erasure of the $\rightarrow$ relation, moving towards the right hand side of the diagram.

Our claim is that the diagram on the right hand side of Figure 10.12 corresponds (up to symmetry, see below) to an element in the interpretation of the type $(\cup \rightarrow \cup) \rightarrow \mathbb{B}$ in the relational model: that point resulting in **tt**, where the argument is called twice, and where in turn each call of the argument calls its argument twice – written

$$ \alpha = ([([\checkmark, \checkmark], \checkmark), ([\checkmark, \checkmark], \checkmark)], \mathbf{tt}) $$

in standard relational model notation, but (ignoring copy indices) the reader should be able to see how the same information is conveyed on the right hand side of Figure 10.12: each “atom” in $\alpha$ corresponds to a pair of a question and an answer. Then, moving from concurrent games to the relational model essentially consists in forgetting the relation $\rightarrow$ in all configurations – so that we may even regard concurrent games as the relational model enriched with causal information. We now aim to make this more formal.

**Positions.** We wish to extract from a board a set matching the relational interpretation. To that end, we start by examining the most constraining constructor, which is

$$ !X = \mathcal{M}_f(X), $$

the bang of $X$ a set, defined as the set of finite multisets. In contrast, the configurations of a $--board$ $!A$ correspond to the set $\text{Fam}(A)$ of families of non-empty configurations indexed by finite sets of natural numbers (see Proposition 7.1.3). As $\mathcal{M}_f(X)$ may be presented as a quotient of finitely indexed families of elements of $X$, it is natural to define the positions of a $--board$ $A$ as configurations up to symmetry:

**Definition 10.4.1.** Consider $A$ a board.

The set $\mathcal{Pos}(A)$ of **positions** of $A$ is simply defined as the quotient set $\mathcal{C}(A)/\cong_A$.

By convention, we use symbols $x, y, z$, etc to range over positions – i.e. the same letters as for configurations, but with a different font.

As an example, there are four positions on the $--board$ $\mathbb{B}$ of Section 8.2.2: the (symmetry classes corresponding to the) configurations $\emptyset, \{q^{-}\}, \{q^{-}, \mathbf{tt}^{+}\}, \text{and } \{q^{-}, \mathbf{ff}^{+}\}$. This shows that **positions** do not quite match the relational model just yet, as the relational interpretation of $\mathbb{B}$ only has two elements, for the two complete computations.

**Stopping positions of boards.** Fortunately, boards come equipped with exactly the structure needed to eliminate partial computations: the **payoff function**.

Recall from Definition 8.2.3 that boards come equipped with a **payoff function** $\kappa_A : \mathcal{C}(A) \rightarrow \{-1, 0, +1\}$, which was motivated precisely by the need to capture which configurations are complete, and to designate a responsible for non-complete configurations. By condition **invariant**, the payoff function automatically extends to

$$ \kappa_A : \mathcal{Pos}(A) \rightarrow \{-1, 0, +1\} $$

a payoff function for positions. This lets us define:
<figure><img src="image_183.png" /><figcaption>Figure 10.13: Non-deterministic witnesses</figcaption></figure>

<caption>Figure 10.14: Symmetric witnesses</caption>

**Definition 10.4.2.** Consider A a board. Its set of stopping positions is the set

$$ (A) = \{x_A \in \mathcal{P}os(A) \mid \kappa_A(x_A) = 0\} $$

This is indeed the right definition, and we shall see in Section 10.4.4 that it makes the various constructions on boards agree with their relational counterparts.

**Stopping positions of strategies.** To a board A, the relational collapse will associate a set (A). If $\sigma: A$ is a strategy on A, we should assign it a subset of (A). We have seen with Proposition 7.3.1 that causal strategies almost compose relationally already with respect to $+-$covered configurations, so the next definition is almost self-evident:

**Definition 10.4.3.** Consider A a board and $\sigma: A$ a causal strategy. Then,

$$ (\sigma) = \{x_A \in (A) \mid \exists x^\sigma \in \mathcal{C}^+(\sigma), \partial_\sigma x^\sigma \in x_A\} $$

is its relational collapse.

For $x^\sigma \in \mathcal{C}^+(\sigma)$ such that $\partial_\sigma x^\sigma \in x_A \in (A)$, we say that $x^\sigma$ is a **witness** for $x_A$; the relational collapse only keeps stopping positions for which there is a witness. In general, the witness is not unique. We show two examples: in Figure 10.13, the (symmetry class of) $\{q^-, t^+\}$ has two witnesses, illustrating the two distinct non-deterministic branches realizing the value $tt$. But the number of witnesses does not necessarily match the number of non-deterministic branches leading to an observable result: in Figure 10.14, there is an infinite number of witnesses for the stopping position corresponding to value $tt$ – even though all those witnesses are symmetric with each other<fnref n="3" />.

## 10.4.2 Composition and Deadlocks

Now, take A and B two $--$boards, and let us consider the case of a strategy from A to B. Of course the definition above applies, instantiated on the board $A \vdash B$. But in order to get a relation from (A) to (B), we shall make use of the following fact:

**Lemma 10.4.4.** Consider A, B two $--$boards. Then, there is a bijection

$$ s_{A,B}^{\vdash} : (A \vdash B) \simeq (A) \times (B) $$

<footnote n="3">³It is a good intuition that witnesses should somehow count non-deterministic branches leading to an observable result, but it requires a much finer definition of witnesses – see Section 13.3.1.</footnote>
**Proof.** We know from Lemma 7.1.22 that configurations of $A \vdash B$ all have the form $x_A \vdash x_B$ where $x_A \in \mathscr{C}(A)$ and $x_B \in \mathscr{C}(B)$; this extends to symmetry classes since symmetries enjoy the same unique decomposition. By Definition 8.2.5, $x_A \vdash x_B$ has null payoff exactly when both $x_A$ and $x_B$ have (recall that $A \vdash B = A^{\perp\mathcal{R}}B$ by definition, below Definition 8.2.5). The bijection follows this decomposition. $\square$

We use this bijection implicitly when defining the collapse of $\sigma : A \vdash B$ as

$$ (\sigma) = \{(x_A, x_B) \in (A) \times (B) \mid \exists x^\sigma \in \mathscr{C}^+(\sigma), \partial_\sigma x^\sigma \in x_A \vdash x_B \} $$

a morphism in $\mathbf{Rel}((A), (B))$ – now, does this preserve the categorical structure?

**Copycat.** We start the analysis for copycat, which is straightforward:

**Proposition 10.4.5.** Consider $A$ a --board. Then, we have the equality

$$ (\mathscr{c}_A) = \mathrm{id}_{(A)} \in \mathrm{Rel}((A), (A)). $$

**Proof.** $\subseteq$. Consider $x_A \vdash y_A \in (\mathscr{c}_A)$. By definition it has a witness in $\mathscr{c}_A$, which by Lemma 6.4.4 has form $x_A \parallel x_A \in \mathscr{C}^+(\mathscr{c}_A)$ with $x_A \vdash x_A \in x_A \vdash y_A$, so $x_A = y_A$.

$\supset$. Consider $(x_A, x_A) \in \mathrm{id}_{(A)}$ and take any representative $x_A \in x_A$. Again by Lemma 6.4.4, $x_A \parallel x_A \in \mathscr{C}^+(\mathscr{c}_A)$, and it is immediate that it is a witness for $(x_A, x_A)$. $\square$

Indeed from Lemma 6.4.4, and with respect to +-covered configurations, copycat already acts like the relational identity! In the light of Proposition 7.3.1, we may hope that the situation for composition will just as simple.

**Composition: oplax preservation.** For one of the two directions, it is simple:

**Lemma 10.4.6.** Consider --boards $A, B, C$, and $\sigma : A \vdash B, \tau : B \vdash C$. Then, we have $(\tau \odot \sigma) \subseteq (\tau) \circ (\sigma)$.

**Proof.** Consider $(x_A, x_C) \in (\tau \odot \sigma)$. By definition – and inlining Proposition 7.3.1 – there is $x^\tau \odot x^\sigma \in \mathscr{C}^+(\tau \odot \sigma)$ s.t. $\partial_\tau \circ_\sigma (x^\tau \odot x^\sigma) = x_A^\sigma \vdash x_C^\tau \in x_A \vdash x_C$. Thus

$$ \partial_\sigma x^\sigma = x_A^\sigma \vdash x_B^\sigma \in x_A \vdash x_B, \quad \partial_\tau x^\tau = x_B^\tau \vdash x_C^\tau \in x_B \vdash x_C $$

where $x^\sigma \in \mathscr{C}^+(\sigma)$ and $x^\tau \in \mathscr{C}^+(\tau)$ and for $x_B$ the symmetry class of $x_B^\sigma = x_B^\tau = x_B$.

The only thing we must check is that $x_B \in (B)$, i.e. $\kappa_B(x_B) = 0$. But if we had $\kappa_B(x_B) = -1$, we would have $\kappa_{A \vdash B}(x_A \vdash x_B) = -1$, contradicting that $\sigma$ is winning. Likewise, $\kappa_B(x_B) = 1$ would contradict that $\tau$ is winning. Hence, $\kappa_B(x_B) = 0$. $\square$

This is not by chance: the mechanism of payoff and winning strategies has been set up specifically with this collapse in mind. Now, examine the other direction.
<figure><img src="image_184.png" /><figcaption>Figure 10.15: Deadlocking composition of causal strategies</figcaption></figure>

**Composition: non lax preservation.** In the other direction, consider $\sigma : A \vdash B, \tau : B \vdash C$, and $(x_A, x_C) \in (\tau) \circ (\sigma)$. This means that there is $x_B \in (B)$ a stopping position such that $(x_A, x_B) \in (\sigma)$ and $(x_B, x_C) \in (\tau)$; meaning that there are two witnesses

$$x^{\sigma} \in \mathscr{C}^{+}(\sigma), \quad x^{\tau} \in \mathscr{C}^{+}(\tau)$$

such that $x_A^{\sigma} \in x_A, x_C^{\tau} \in x_C$ and $x_B^{\sigma}, x_B^{\tau} \in x_B$ – thus there is $\theta_B : x_B^{\sigma} \cong_B x_B^{\tau}$. So $x^{\sigma}$ and $x^{\tau}$ may not match on $B$ on the nose, but only up to symmetry. This is an issue, but one that we are prepared to handle just as we already did in the proof of Lemma 9.3.5, using Proposition 7.4.4, reindexing both $x^{\sigma}$ and $x^{\tau}$ to find a true synchronization. Thus let us ignore that for now, and pretend that we are lucky enough to have $x_B^{\sigma} = x_B^{\tau}$.

To sum up, relational composition provides us with a *witness position* that both strategies agree (up to symmetry) is *reachable*. In contrast, composition of strategies is more rigid: not only should the projections of $x^{\sigma}$ and $x^{\tau}$ on $B$ match, they should also arrive at this position *in a compatible chronological ordering*. This is not always possible: these two notions of composition differ when interaction triggers a *causal deadlock*, i.e. pairs of configurations that are *matching* but not *secured* as in Definition 6.2.2. Figure 10.15 displays an example: the strategy obtained by composition has no response to the initial Opponent move, while relational composition authorizes $0^+$.

This strikes at the heart of the difference between game and relational semantics: the former is dynamic hence sensitive to deadlocks, while the latter is static. This of course is what lets game semantics model languages with non-commutative effects, but for us, very concretely, it means that the relational model is not lax functorial.

### 10.4.3 The Deadlock-Free Lemma

Our *deus ex machina* is visibility. A powerful – and at first unexpected – consequence of visibility is that any interaction between visible strategies is always deadlock-free. The consequence of visibility that our proof will exploit repeatedly is:

**Lemma 10.4.7.** *Take A, B --boards, $\sigma : A \vdash B$ visible, and $m, m' \in \sigma$ s.t. $m <_{\sigma} m'$. Then, $j(m')$ is comparable with $m$ with respect to $\leq_{\sigma}$.*

*Proof.* Since $m <_{\sigma} m'$, there is $\rho \to m' \in \text{gcc}(\sigma)$ s.t. $m \in \rho$. If $\partial_{\sigma}(m')$ is minimal in A, $\partial_{\sigma}(j(m'))$ is minimal in B, so $j(m')$ is minimal for $\leq_{\sigma}$ by courtesy. But since $\sigma$ is
pointed, $j(m')$ is initial in $\rho$, obviously comparable with $m$ as $\rho$ is totally ordered.
Else, by visibility $j(m') \in \rho$. But $\rho$ is totally ordered, so $m, j(m')$ comparable. $\square$

We shall prove that the composition of visible causal strategies is deadlock-free. But first, we recall the basic mechanisms of interactions between causal strategies. Consider $\sigma : A \vdash B$ and $\tau : B \vdash C$, and configurations $x^\sigma \in \mathscr{C}(\sigma)$, and $x^\tau \in \mathscr{C}(\tau)$ s.t., writing $\partial_\sigma x^\sigma = x_A^\sigma \parallel x_B^\sigma$ and $\partial_\tau x^\tau = x_A^\tau \parallel x_C^\tau$, we have $x_A^\sigma = x_B^\tau = x_B$, i.e. $x^\sigma$ and $x^\tau$ are matching. Recall from Definition 6.2.2 the bijection arising from their synchronization:

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

whose graph is equipped with a relation importing the causal constraints from $\sigma$ and $\tau$:

$$ (l, r) \prec (l', r') \quad \Leftrightarrow \quad l <_{\sigma \parallel C} l' \lor r <_{A \parallel \tau} r'. $$

We saw in Definition 6.2.2 and Proposition 7.3.6 that $(x^\sigma, x^\tau)$ corresponds to a configuration of the interaction $\tau \oplus \sigma$ when this bijection is *secured*, i.e. $\prec$ is acyclic.

If $\sigma : A \vdash B$ and $\tau : B \vdash C$ are visible, we claim that this is always the case.

**Proof sketch.** Before giving the formal proof, we showcase the reasoning on a simplified case. The basic idea is by contradiction: starting with a putative deadlock, we repeatedly push it down the causal dependency of the board, until it reaches a minimal event – but those cannot appear in a cycle.

Consider a **simple deadlock** in $\varphi$, given by $p_1 = (l_1, r_1)$ and $p_2 = (l_2, r_2) \in \varphi$ s.t.

$$ l_1 <_{\sigma \parallel C} l_2, \quad r_2 <_{A \parallel \tau} r_1, $$

an immediate incompatibility between $p_1$ and $p_2$. In other words we have $p_1 \prec p_2$ and $p_2 \prec p_1$; we use $p_1 \prec_\sigma p_2$ and $p_2 \prec_\tau p_1$ to indicate the origin of the causal constraint. We apply the same conventions for polarity of elements of $\varphi$ as for Lemma 6.2.15.

The first observation (skipped here) is that w.l.o.g., the polarities are as in

$$ p_1^{r'} \underset{\Delta_{\tau}}{\stackrel{\Delta_{\sigma}}{\rightleftharpoons}} p_2^{l'}, $$

where both occur in $B$ but not minimal in $B$ – so we may take $j(p_i) = (j(l_i), j(r_i))$. By Lemma 10.4.7, $l_1$ and $j(l_2)$ are comparable for $\sigma$; while $r_2$ and $j(r_1)$ are comparable for $\tau$. If $p_1 \prec_\sigma j(p_2)$ or $p_2 \prec_\tau j(p_1)$, then we respectively have one of the cycles:

<figure><img src="image_185.png" /></figure>
so simple deadlocks between $p_1$ and $j(p_2)$; or between $j(p_1)$ and $p_2$. Those simple dead-
locks are smaller, in the sense that their cumulative depth in $B$ has decreased – justifying
the inductive reasoning. The case $p_1 = j(p_2)$ or $p_2 = j(p_1)$ is easily discarded.

The last case has $j(p_2) \triangleleft_\sigma p_1$ and $j(p_1) \triangleleft_\tau p_2$. But $p_1$ has polarity $r$, so by Lemma 10.2.2 the only immediate dependency in $\sigma$ of $l_1^-$ is $j(l_1)$. So $j(p_2) \triangleleft_\sigma p_1$ factors as $j(p_2) \triangleleft_\sigma j(p_1) \triangleleft_\sigma p_1$. Symmetrically $j(p_1) \triangleleft_\tau j(p_2)$, so we have:

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

closer to the root of the board. Repeating this we eventually hit an impossible simple
deadlock with a minimal event in B, finally exposing the contradiction.

**Detailed proof.** The proof of the deadlock-free lemma is the same in essence, but challenging in form. Firstly, cycles in $\triangleleft$ in Definition 6.2.2 may have arbitrary length. Secondly, in relational composition strategies synchronize on *symmetry classes* rather than configurations; so we must account for synchronization through symmetry.

**Lemma 10.4.8.** Consider $A, B, C$ --boards, $\sigma : A \vdash B$ and $\tau : B \vdash C$ visible causal strategies, $x^\sigma \in \mathcal{C}(\sigma)$ and $x^\tau \in \mathcal{C}(\tau)$ with a symmetry $\theta : x_B^\sigma \cong_B x_B^\tau$.

Then, the composite bijection

$$
\varphi : x^{\sigma} \parallel x_{C}^{\tau} \stackrel{\partial_{\sigma} \parallel x_{C}^{\tau}}{\approx} x_{A}^{\sigma} \parallel x_{B}^{\sigma} \parallel x_{C}^{\tau} \stackrel{x_{A}^{\sigma} \parallel \theta \parallel x_{C}^{\tau}}{\approx} x_{A}^{\sigma} \parallel x_{B}^{\tau} \parallel x_{C}^{\tau} \stackrel{x_{A}^{\sigma} \parallel \partial_{\tau}^{-1}}{\approx} x_{A}^{\sigma} \parallel x^{\tau},
$$

is secured, in the sense that the relation $\triangleleft$, defined on the graph of $\varphi$ with

$(l, r) \triangleleft (l', r')$

whenever $l (<_\sigma <_C) l'$ or $r (<_A <_\tau) r'$, is acyclic; i.e. $(x^\sigma, \theta, x^\tau)$ causally compatible.

*Proof.* We use polarities $\ell, r$ or $-$ for elements of $\varphi$ (i.e. pairs $(l, r)$) as above. We say $(l, r)$ occurs in $A, B$ or $C$ in the obvious sense. We use a notion of *justifier* of a pair $(l, r)$ non-minimal in $B$: as $\theta$ is an order-iso, $(\partial_\sigma \parallel C)(l)$ is minimal in $B$ iff $(A \parallel \partial_\tau)(r)$ is. If not, then $j(l)$ and $j(r)$ also match up to $\theta$ and $(j(l), j(r))$ must be in $\varphi$ as well – we write it $j(l, r)$. Suppose now $\triangleleft$ is *not* secured, i.e. there is $((l_1, r_1), \dots, (l_n, r_n))$ with

$(l_1, r_1) \triangleleft (l_2, r_2) \triangleleft \dots \triangleleft (l_n, r_n) \triangleleft (l_1, r_1),$

written $p_1 \triangleleft \dots \triangleleft p_n \triangleleft p_1$ – the **length** of this cycle is $n$. First, w.l.o.g. the cycle occurs entirely in $B$. Assume it has minimal length. If it occurs entirely in $A$ or $C$, then $(l_i)_{1 \le i \le n}$ (resp. $(r_i)_{1 \le i \le n}$) is a cycle in $\sigma$ (resp. $\tau$), absurd. So, it passes through $B$. Next, if e.g.

$$
p_i^{(B)} \triangleleft p_{i+1}^{(C)} \triangleleft \dots \triangleleft p_{j-1}^{(C)} \triangleleft p_j^{(B)},
$$

then it is easy to prove that $r_i < r_{i+1} < \dots < r_{j-1} < r_j$, so that $p_i^{(B)} \triangleleft p_j^{(B)}$ and the cycle
can be shortened, contradicting its minimality – the same argument holds for A.
We restrict to cycles in $B$. The depth of $(l, r)$ is the length of the chain of justifiers to $(l_0, r_0)$ minimal in $B$ – the depth of $(l_0, r_0)$ minimal in $B$ is 0. The cycle has depth

$$d = \sum_{1 \le i \le n} \text{depth}(l_i, r_i),$$

and we assume w.l.o.g. the cycle minimal for the product order on pairs $(n, d)$. In this proof, all arithmetic computations on indices are done modulo $n$ (the length).

Next, we write $p_i \triangleleft_\sigma p_j$ if $l_i (<_\sigma <_C) l_j$ and $p_i \triangleleft_\tau p_j$ symmetrically. We notice that $\triangleleft_\sigma$ and $\triangleleft_\tau$ alternate – if not we shorten the cycle by transitivity. We assume w.l.o.g. that $p_{2k} \triangleleft_\sigma p_{2k+1}$ and $p_{2k+1} \triangleleft_\tau p_{2k+2}$ for all $k$. But then, $\text{pol}(p_{2k}) = r$ and $\text{pol}(p_{2k+1}) = \ell$ so that polarity in the cycle is alternating as well. Indeed, assume e.g.

$$p_{2k+1} \triangleleft p_{2k+2}^{\ell} \triangleleft p_{2k+3}$$

with $p_{2k+1} \triangleleft_\tau p_{2k+2}$ and $p_{2k+2} \triangleleft_\sigma p_{2k+3}$. Then, $r_{2k+1} <_{A\|\tau} r_{2k+2}$. Negative $r_{2k+2}^{-}$ cannot be minimal in $B$, so by Lemma 10.2.2, it has a unique predecessor $j(r_{2k+2}) \to_{A\|\tau} r_{2k+2}$, so $r_{2k+1} <_{A\|\tau} r_{2k+2}^{-}$ factors as $r_{2k+1} <_{A\|\tau} j(r_{2k+2}) \to_{A\|\tau} r_{2k+2}^{-}$. Accordingly, $p_{2k+1} \triangleleft_\tau j(p_{2k+2}) \triangleleft_\tau p_{2k+2}^{-}$ but dependencies in the game are respected by both strategies, so $j(p_{2k+2}) \triangleleft_\sigma p_{2k+2}$. So $j(p_{2k+2}) \triangleleft_\sigma p_{2k+3}$, and we can replace the cycle fragment with

$$p_{2k+1} \triangleleft j(p_{2k+2}) \triangleleft p_{2k+3}$$

which is still in $B$, has the same length but strictly smaller depth. The symmetric argument applies for $\sigma$, so any $p_{2k+1}$ has polarity $\ell$ and any $p_{2k+2}$ has polarity $r$.

We show the cycle cannot have an event minimal in $B$. Seeking a contradiction, if

$$p_{2k+1}^{\ell} \triangleleft_{\tau} p_{2k+2}^{r} \triangleleft_{\sigma} p_{2k+3}^{\ell}$$

with $p_{2k+2}$ minimal in $B$, then $l_{2k+2} <_{\sigma} l_{2k+3}$ with $l_{2k+2}$ minimal in $B$, but then $\partial_{\sigma\|C}(l_{2k+2}) <_{A\|B\|C} \partial_{\sigma\|C}(l_{2k+3})$. Indeed, if $\partial_{\sigma\|C}(l_{2k+2})$ is minimal in $B$, $l_{2k+2}$ is (by courtesy) minimal in $\sigma \parallel C$. Likewise, since $l_{2k+3}$ occurs in $B$, $\partial_{\sigma\|C}(l_{2k+3})$ depends (for $\le_{A\|B\|C}$) on a unique $\partial_{\sigma\|C}(l)$ minimal in $B$, where $l$ must also be minimal in $\sigma$. But since $\sigma$ is pointed, $l_{2k+3}$ has a unique minimal dependency, hence $l = l_{2k+2}$ and $\partial_{\sigma\|C}(l_{2k+2}) <_{A\|B\|C} \partial_{\sigma\|C}(l_{2k+3})$ as claimed. But then, $r_{2k+2} <_{A\|\tau} r_{2k+3}$, so $p_{2k+1}^{\ell} \triangleleft_\tau p_{2k+2}^{r} \triangleleft_\tau p_{2k+3}^{\ell}$ and again the cycle can be shortened by transitivity.

We have proved a minimal cycle has a canonical form where the strategies alternate, polarity alternates, all events are in $B$ and non-minimal. Since $p_{2k}^{r} \triangleleft_{\sigma} p_{2k+1}^{\ell}$, writing $p = (l, r) = j(p_{2k+1})$, $l = j(l_{2k+1})$ as well. From Lemma 10.4.7, we know that $l = j(l_{2k+1})$ is comparable with $l_{2k}$ in $\sigma \parallel C$ (by visibility of $\sigma$). If $j(l_{2k+1}) = l_{2k}$, then $r_{2k} \triangleleft_\tau r_{2k+1}$ as well. This gives $p_{2k-1} \triangleleft_\tau p_{2k+2}$, contradicting minimality of the cycle. So $j(l_{2k+1}) \neq l_{2k}$. Similarly, $j(r_{2k+2})$ is comparable with $r_{2k+1}$ in $A \parallel \tau$, but distinct.

Assume that we have $p_{2k} \triangleleft_\sigma j(p_{2k+1})$ for some $k$. Since $j(p_{2k+1}) \triangleleft_\tau p_{2k+1} \triangleleft_\tau p_{2k+2}$ we can replace the cycle fragment $p_{2k} \triangleleft p_{2k+1} \triangleleft p_{2k+2}$ with the cycle fragment

$$p_{2k} \triangleleft j(p_{2k+1}) \triangleleft p_{2k+2}$$

which has the same length but smaller depth, absurd. So, $j(p_{2k+1}) \triangleleft_\sigma p_{2k}$ for all $k$ (symmetrically, $j(p_{2k+2}) \triangleleft_\tau p_{2k+1}$ for all $k$). In particular, $j(l_{2k+1}) <_{\sigma} l_{2k}^{-}$ but by
Lemma 10.2.2, $l_{2k}^-$ has a unique immediate predecessor $j(l_{2k})$. So, $j(p_{2k+1}) \triangleleft_{\sigma} j(p_{2k})$ for all $k$; and likewise $j(p_{2k+2}) \triangleleft_{\tau} j(p_{2k+1})$ for all $k$. So we can replace the full cycle with

$$j(p_n) \triangleleft j(p_{n-1}) \triangleleft \dots \triangleleft j(p_1) \triangleleft j(p_n)$$

which has the same length but smaller depth, contradiction. □

The deadlock-free lemma is a powerful observation with far-reaching consequences in linking game semantics and relational models. It also gives a lot of weight to the notion of visibility, as a simple, well-behaved under-approximation of innocence.

As a direct consequence of the deadlock-free lemma, we obtain:

**Corollary 10.4.9.** Consider $-\text{boards } A, B, C$, and $\sigma : A \vdash B, \tau : B \vdash C$ visible.
Then, $(\tau \odot \sigma) = (\tau) \circ (\sigma)$.

*Proof.* $\subseteq$. Follows from Lemma 10.4.6.

$\sqsupset$. Consider $(x_A, x_B) \in (\sigma)$ and $(x_B, x_C) \in (\tau)$, with witnesses $x^\sigma \in \mathscr{C}^+(\sigma)$ and $x^\tau \in \mathscr{C}^+(\tau)$ with $\partial_\sigma(x^\sigma) = x_A^\sigma \parallel x_B^\sigma$, $\partial_\tau(x^\tau) = x_C^\tau \parallel x_B^\tau$, with $x_A^\sigma \in x_A$, $x_B^\sigma \in x_B$, and $x_C^\tau \in x_C$. In particular, there is $\theta : x_B^\sigma \cong_B x_C^\tau$. Now, the composite bijection

$$\varphi : x^\sigma \parallel x_C^\tau \stackrel{\partial_\sigma \parallel x_C^\tau}{\cong} x_A^\sigma \parallel x_B^\sigma \parallel x_C^\tau \stackrel{x_A^\sigma \parallel \theta \parallel x_C^\tau}{\cong} x_A^\sigma \parallel x_B^\tau \parallel x_C^\tau \stackrel{x_A^\sigma \parallel \partial_\tau^{-1}}{\cong} x_A^\sigma \parallel x^\tau,$$

is secured by Lemma 10.4.8. Thus by Proposition 7.4.4, there are reindexings $y^\sigma \cong_\sigma x^\sigma$ and $y^\tau \cong_\tau x^\tau$ such that $\partial_\sigma(y^\sigma) = y_A^\sigma \parallel y_B^\sigma$, $\partial_\tau(y^\tau) = y_B^\tau \parallel y_C^\tau$ with $y_B^\sigma = y_B^\tau - \text{so } y^\tau \odot y^\sigma \in \mathscr{C}(\tau \odot \sigma)$. But since $y^\sigma \cong_\sigma x^\sigma$ and $y^\tau \cong_\tau x^\tau$, we also know that $y_A^\sigma \in x_A$ and $y_C^\tau \in x_C$ still, so $y^\tau \odot y^\sigma$ witnesses $(x_A, x_C) \in (\tau \odot \sigma)$ as required. □

### 10.4.4 A Relative Seely $\sim$-Functor

Next, we show that the relational collapse preserves the rest of the structure – it should form a relative Seely $\sim$-functor. Relative Seely ($\sim$)-functors are simply ($\sim$)-functors equipped with isomorphisms expressing the preservation of the additional structure, satisfying certain coherence conditions. Just like relative Seely categories, relative Seely ($\sim$)-functors are not a standard notion. However, they are certainly an unsurprising one, so in this monograph we opted to relegate it to the appendix (Appendix A.2).

To construct our concrete relative Seely $\sim$-functor, we start with:

**Proposition 10.4.10.** We have a $\sim$-functor $(-) : \text{NTCG-Vis} \to \text{Rel}$.

*Proof.* Preservation of copycat is by Proposition 10.4.5, and preservation of composition is by Proposition 10.4.9. It remains to show that $(-)$ preserves $\approx$.

Hence, consider $\sigma, \sigma' : A \vdash B$ with $f : \sigma \approx \sigma'$, and take $(x_A, x_B) \in (\sigma)$. By definition, there is a witness $x^\sigma \in \mathscr{C}^+(\sigma)$ such that $\partial_\sigma x^\sigma \in x_A \vdash x_B$. But then,

$$f[x^\sigma]_A \vdash f[x^\sigma]_B : x_A^\sigma \vdash x_B^\sigma \cong_{A \vdash B} f(x^\sigma)_A \vdash f(x^\sigma)_B$$

so that $f(x^\sigma) \in x_A \vdash x_B$ as required. The other inclusion holds by symmetry. □

Next, we examine preservation of the full categorical structure.
**Preservation of the monoidal structure.** Following Definition A.2.1, we require

$$ \begin{aligned} s_{A,B}^{\otimes} & : & (A) \times (B) & \cong (A \otimes B) \\ s^1 & : & 1 & \cong (1) \end{aligned} $$

isomorphisms in **Rel**, natural in **A** and **B** – those follow from the bijections of Lemma 7.1.22 in the obvious way, which is indeed compatible with payoff.

**Proposition 10.4.11.** We have $((–), s^{\otimes}, s^1)$ a symmetric monoidal ~-functor.

*Proof.* All verifications are straightforward. For naturality, we must show that

$$ \begin{array}{ccc} (A) \times (B) & \xrightarrow{s_{A,B}^{\otimes}} & (A \otimes B) \\ (\sigma) \times (\tau) & \searrow & (\sigma \otimes \tau) \\ (A') \times (B') & \xrightarrow{s_{A',B'}^{\otimes}} & (A' \otimes B') \end{array} $$

commutes for $\sigma : A \vdash A'$ and $\tau : B \vdash B'$, which is direct by Proposition 8.1.1. $\square$

**Preservation of !.** Next we deal with the exponential structure, which is the most challenging. Inspecting the requirements for relative Seely functors we must first show that $(-)$ preserves strict objects – but this is trivial: as a proper Seely category, **Rel** is regarded as a relative Seely category with all objects strict. Then we must provide

$$ s_S^1 : \mathcal{M}_f((S)) \cong (!S) $$

for every strict $S$, subject to coherence conditions. We first construct the bijection:

**Proposition 10.4.12.** For any $S$ strict, there is a bijection $s_S^1 : \mathcal{M}_f((S)) \cong (!S)$.

*Proof.* First, recall from Lemma 8.3.1 that we have a bijection

$$ \mathrm{Fam}(\mathcal{C}^{\neq \emptyset}(S)) \cong \mathcal{C}(!S) $$

following which configurations of null payoff of $!S$ correspond to families of non-empty configurations of null payoff of $S$. But $S$ is strict, thus its configurations of null payoff are non-empty. Hence the bijection above may be directly refined into another bijection

$$ \mathrm{Fam}(\langle!S\rangle) \cong (\langle!S\rangle) $$

where $\langle!A\rangle$ is the set of configurations of null payoff. Inlining this bijection, we may define the inverse of $s_S^1$ on representatives directly as follows:

$$ (s_S^1)^{-1} : \langle!S\rangle \rightarrow \mathcal{M}_f((S)) \\ [x_i^S | i \in I] \mapsto [x_i^S | i \in I] $$

where $x_i^S$ denotes the symmetry class of $x_i^S$, $[x_i^S | i \in I]$ (with a bold font) is our notation for families, and $[x_i^S | i \in I]$ (with non-bold font) is multiset comprehension.
**Invariant.** Consider $\theta : [x_i^S | i \in I] \cong_S [y_j^S | j \in J]$ a symmetry, which by definition is given by a bijection $\pi : I \cong J$ and a family $(\theta_i)_{i \in I}$ where $\theta_i : x_i^S \cong_S y_{\pi(i)}^S$ for all $i \in I$. But then, $x_i^S = y_{\pi(i)}^S$, from which, as required, we deduce that

$$[x_i^S | i \in I] = [y_{\pi(i)}^S | i \in I] = [y_j^S | j \in J].$$

**Injective.** Assume $[x_i^S | i \in I] = [y_j^S | j \in J]$. Thus, there is a bijection $\pi : I \cong J$ such that for all $i \in I$, $x_i^S = y_{\pi(i)}^S$. Hence, for all $i \in I$ there is $\theta_i : x_i^S \cong_S y_{\pi(i)}^S$, altogether forming a symmetry $\theta : [x_i^S | i \in I] \cong_S [y_j^S | j \in J]$.

**Surjective.** Consider a multiset $\{x_1, \dots, x_n\} \in \mathcal{M}_f((S))$. For each $1 \le i \le n$, consider a representative $x_i \in x_i$. Then, $[x_i | 1 \le i \le n]$ provides a pre-image. $\square$

Observe that there is no such bijection $\mathcal{M}_f((A)) \cong (!A)$ for A non-strict, because
$$[\emptyset] \neq [\emptyset, \emptyset]$$

are distinct elements of $\mathcal{M}_f((A))$, but can only be represented in $(!A)$ with the same (empty) configuration since there are no events. The relational model may remember how many times a game is *not* visited, which makes no sense in terms of games. This is the reason behind the preservation of the *relative* Seely ~-categorical structure only.

Among the several diagrams to check, the most subtle is preservation of promotion:

**Lemma 10.4.13.** Consider $S, T$ strict and $\sigma : !S \vdash T$.
Then, the following square commutes in **Rel**:

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

**Proof.** We use a multiset notation for stopping positions of $!S$ and $!T$, inlining Proposition 10.4.12. The upper-right path computes to the pairs that can be written as

$$([x_{i,j} | i \in I, j \in J_i], [y_i | i \in I])$$

for $x_{i,j} \in (S)$ and $y_i \in (T)$ where we have that for all $i \in I$, $([x_{i,j} | j \in J_i], y_i) \in (\sigma)$.
Thus for all $i \in I$, there is $x_i^\sigma \in \mathcal{C}^+(\sigma)$ witnessing that pair, i.e. we have

$$\partial_\sigma x_i^\sigma \in [x_{i,j} | j \in J_i] \vdash y_i.$$

Thus, relying on Proposition 8.3.3 we may form $[x_i^\sigma | i \in I] \in \mathcal{C}^+(\sigma^1)$ (by Lemma 8.1.8, $\sigma^1$ only differs from $!\sigma$ via its display map), and a direct verification ensures that

$$\partial_{\sigma^1}[x_i^\sigma | i \in I] \in ([x_{i,j} | i \in I, j \in J_i], [y_i | i \in I])$$

as required. The other direction follows the same decompositions. $\square$
**Relative Seely ~-functor.** To wrap up, we introduce the missing components. First,

$$s^T : \emptyset \cong (T)$$

is simply the empty relation. For the product and the arrow, we prove:

**Lemma 10.4.14.** Consider $A, S, T$ --boards with $S, T$ strict. Then, we have bijections

$$s_{S,T}^{\&} : (S) + (T) \cong (S \& T)$$

$$s_{A,S}^{\neg\&} : (A) \times (S) \cong (A \to S)$$

*Proof.* For the product, recall first that by Lemma 8.2.9, we have a bijection

$$\mathcal{C}^{\neq\emptyset}(S) + \mathcal{C}^{\neq\emptyset}(T) \cong \mathcal{C}^{\neq\emptyset}(S \& T)$$

which holds also for symmetries, and thus extends to symmetry classes. But now we note that $S, T$, and $S \& T$ are strict, therefore configurations of null payoff must be non-empty. It follows that the bijection above extends to stopping positions.

For the arrow, similarly recall that by Lemma 8.2.12, we have a bijection

$$\mathcal{C}^{\neq\emptyset}(A \to S) \cong \mathcal{C}(A) \times \mathcal{C}^{\neq\emptyset}(S)$$

which also holds to symmetry and thus extends to symmetry classes. But again note that since $S$ is strict, configurations with null payoff must be non-empty, and thus the above extends to a bijection on stopping positions. $\square$

The missing five coherence diagrams of relative Seely ~-functors are direct, from an analysis of the symmetry classes reached by the component strategies. Projections, dereliction and monoidality are defined by lifting, hence the corresponding diagrams follow as for copycat in Proposition 10.4.5. For evaluation, this follows from the description of its +-covered configurations in Proposition 8.2.27. Altogether:

**Corollary 10.4.15.** We have a relative Seely ~-functor $(-) : \text{NTCG-Vis} \to \text{Rel}$.

By Theorem A.2.3 we have a cartesian closed ~-functor $(-) : \text{NTCG-Vis}_1 \to \text{Rel}_1$.

Once the deadlock-free lemma is established, this interpretation-preserving collapse from concurrent games to the relational model is strikingly simple, and emphasizes how the concurrent games model may be regarded as a causal and temporal extension of the relational model. This extension is of course far from negligible as it allows one to represent programming languages with non-commutative effects, such as references.

**Positional equivalence.** In this monograph, we shall exploit this concretely by reasoning on strategies up to the induced equivalence relation:

**Definition 10.4.16.** Consider $A, B$ --boards, and $\sigma, \sigma' \in \text{NTCG-Vis}(A, B)$.

We say that $\sigma$ and $\sigma'$ are **positionally equivalent**, written $\sigma \equiv \sigma'$, iff $(\sigma) = (\sigma')$.
<figure><img src="image_188.png" /><figcaption>Figure 10.16: Quotienting out evaluation order</figcaption></figure>

$$ \frac{x_A \in (A) \qquad x_B \in (B)}{x_A \otimes x_B \in (A \otimes B)} \qquad \frac{x_A \in (A) \qquad x_C \in (C)}{x_A \to x_C \in (A \to C)} \\ \frac{x \in (A)_i \qquad (i \in I)}{(i, x) \in (\&_{i \in I} A_i)} \qquad \frac{(x_C^i \in (C))_{i \in I}}{[x_C^i | i \in I] \in (!C)} \qquad \frac{x_A \in (A) \qquad x_B \in (B)}{x_A \vdash x_B \in (A \vdash B)} $$

<caption>Figure 10.17: Syntax for positions for A, B, C --boards with C strict</caption>

Concretely, positional equivalence amounts to quotienting out information about the evaluation order, as illustrated in Figure 10.16. It is a very brutal quotient, which would clearly be inconsistent in the presence of any non-commutative effect. But since (–) is a relative Seely ~-functor, positional equivalence is a congruence within visible causal strategies: it is preserved by all operations used in computing the interpretation. In other words, there is another relative Seely ~-category where visible strategies are considered up to positional equivalence – we shall not move to this ~-category, but the finite definability result of Chapter 12 will hold up to positional equivalence only.

**Back to** `->-Strat`. The developments presented in this chapter have no interaction with mixed boards and well-bracketing, hence transport transparently from `NTCG_1` to `->-Strat`. Hence there are `->-Vis` and `->-Inn`, two cartesian closed sub-~ categories of `->-Strat` with morphisms respectively restricted to *visible* and *parallel innocent strategies*. They both support the interpretation of `PCF_2`, with cartesian closed ~-functors:

$$ \begin{align*} (-) & : \dashrightarrow \text{-Vis} \rightarrow \text{Rel}_1 \\ (-) & : \dashrightarrow \text{-Inn} \rightarrow \text{Rel}_1; \end{align*} $$

preserving the interpretation. Consequently, `->-Vis` and `->-Inn` both support positional equivalence which is preserved by all operations used in the interpretation of `PCF_2`.
<figure><img src="image_189.png" /><figcaption>Figure 10.18: A well-bracketed innocent strategy with a non well-bracketed gcc</figcaption></figure>

**A syntax for positions.** It will be convenient to have a syntactic description of the shape of positions on various --boards constructions. We give this description in Figure 10.17, directly applying the bijection $s_{A,B}^{\otimes}$ from Proposition 10.4.11, $s_{A,C}^{-\circ}$ and $s_{C,D}^{\&}$ from Lemma 10.4.14, $s_S^{!}$ Proposition 10.4.12, and the obvious variant of $s_{A,B}^{\otimes}$ for $\vd$.

# 10.5 Globularity

Though we regard parallel innocence (and *visibility*) as the key conditions to understand the causal shape of pure parallel programs, it is not yet precise enough to entail our definability result. For definability purposes, we need yet again more rigid constraints on the causal shape of strategies, taking the form of a final condition called *globularity*.

## 10.5.1 Motivation and Definition

**Well-bracketed gccs.** In Section 10.1.2, we introduced *pre-innocence* with the intuition that a gcc may be regarded as a standalone sequential program, and pre-innocence brings constraints as to how these “sequential threads” may be forked and merged. But if these “threads” do correspond to good old sequential computations, they should certainly satisfy a condition akin to sequential well-bracketing (see Definition 3.2.5).

Strategies in $\dashv$-**Strat** already satisfy a well-bracketing condition (Definition 9.3.2). However, it is based in the *logical* well-bracketing of non-alternating plays (Definition 5.1.2), which is insufficient to ensure that gccs are (sequentially) well-bracketed: this is illustrated in Figure 10.18, displaying a well-bracketed innocent causal strategy with a non well-bracketed gcc highlighted. This invites the condition, for $\sigma$ in $\dashv$-**Inn**:

*wb-threads*: any $\rho \in \text{gcc}(\sigma)$ is well-bracketed in the sense of Definition 3.2.5.

However, this is not yet enough to fully capture higher-order pure parallel computation. The final condition required has to do with which gccs can be legally merged.
**Definition 10.5.1.** Consider A, B mixed boards, and $\sigma \in \text{→-Inn}(A, B)$.
Then $\sigma$ is **globular** if it satisfies conditions *wb-threads* and *globules*.

**10.5.2 Composition of Globularity**

In this section, we develop the compositional structure of globularity.

**Basic categorical structure.** As usual when introducing a new condition on strategies, we must show that it is compatible with all our constructions on strategies – and as is often the case, the most crucial point is compatibility with copycat and composition.

Recall that the definition of globularity concerns morphisms in $\text{→-Inn}$, defined as (a subcategory of) a Kleisli category, i.e. its morphisms are certain strategies on $!A \vdash B$ where A and B are mixed boards. In examining compatibility of globularity with the categorical structure, it is convenient to work with the basic constructions in NTCG (copycat, composition) rather than those in the Kleisli category (Kleisli composition). Here we shall do that, keeping in mind the slight abuse that technically the definition of globularity refers to the Question/Answer labelling, which was not required on boards, but arises only in mixed boards, via the link with the arena.

**Proposition 10.5.2.** *The copycat strategy $\mathfrak{c}_A : A \vdash A$ is globular.*

*Proof.* The condition *wb-threads* boils down to the proof that P-views of the alternating copycat are well-bracketed in the sense of Definition 3.2.5. *Globularity* holds vacuously, as the event structure for copycat has no causal merge. $\square$

As usual, this reasoning applies to all copycat strategies involved in the interpretation: projections, structural morphisms for the monoidal structure, dereliction, etc.

Now, we establish stability of globularity under composition:

**Proposition 10.5.3.** *Consider $\sigma : A \vdash B$ and $\tau : B \vdash C$ globular.*
Then, $\tau \odot \sigma : A \vdash C$ is globular.*

*Proof.* For *wb-threads*, we first prove that all *gcs* in $\tau \otimes \sigma$ are well-bracketed – this is a variation of the fact that alternating innocent strategies are well-bracketed iff their measure form is (Proposition 3.2.13). For *globules*, by the same reasoning as in Proposition 10.3.2, a globule in $\tau \odot \sigma$ originates in a diagram picturing causal chains

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

in $\tau \otimes \sigma$, constructed as and satisfying the same properties as in Proposition 10.3.2 – in particular $n$ has polarity $\ell$ without loss of generality. But then as in Proposition 10.3.2,

$$ \mathrm{gce}(\Gamma \kappa_{\le n}^1 \neg \sigma, \Gamma \kappa_{\le p}^2 \neg \sigma) = \mathrm{gce}(\kappa_{\le n}^1, \kappa_{\le p}^2)_{\sigma} = m'_{\sigma}, $$
by the forking lemma, i.e. $\sigma$ sees the same fork as in $\tau \otimes \sigma$. Since $\sigma$ is *globular*, all questions between $m'_\sigma$ and $n_\sigma$ in both $\Gamma_{\kappa^{<n}} \nleq \sigma$ and $\Gamma_{\kappa^{<n}} \nleq \sigma$ have an answer. But as observed above, gccs in $\tau \otimes \sigma$ are well-bracketed, which entails that all questions between $m'$ and $n$ in $\kappa^1$ and $\kappa^2$ also have an answer – hence, *globules* is satisfied in $\tau \odot \sigma$. $\square$

**Interpretation of PCF$\parallel$.** As for parallel innocence, preservation of globularity for all other operations is straightforward. We omit the details of that, and of the fact that the basic primitives of PCF$\parallel$ yields globular strategies. Altogether, we get:

**Theorem 10.5.4.** *there is $\rightarrow$-Glob, a cartesian closed sub-~-category of $\rightarrow$-Strat, with morphisms restricted to globular strategies.*

Moreover, $\rightarrow$-Glob supports the interpretation of PCF$\parallel$.

**10.6 History and Related Work**

*Parallel innocence* and its accompanying theory (the forking lemma and stability under composition, the deadlock-free lemma and the collapse to **Rel**, globularity) have been developed in close collaboration with Simon Castellan during his PhD thesis<fnref n="4" /> – they first appear in published form in [Castellan et al., 2015]; though the presentation given here differs significantly, having matured quite a bit since then.

Parallel innocence was first developed aiming for a finite definability result for (essentially) PCF$_{‖}$, which was achieved in [Castellan et al., 2015]. It became a cornerstone of subsequent developments in concurrent games. Though surprisingly, it is not *parallel innocence* per se that turned out so useful in our later work, but *visibility* and the deadlock-free lemma! Indeed, this is one of the key ingredients in our subsequent results relating concurrent games and relational models, in the probabilistic [Castellan et al., 2018b], the general weighted case [Clairambault and Paquet, 2021], the quantum case [Clairambault and de Visme, 2020] and more recently for generalized species of structure [Clairambault et al., 2023b]. In a sense, the deadlock-free lemma explains why the relational models work at all for pure parallel programs: no deadlocks can arise in composing them, so that causal information has no impact on possible synchronizations and can safely be forgotten. No such miracle occurs for effectful programming languages, for which the causal information is unavoidable.

**Related work.** In [Melliès and Mimram, 2007], Melliès and Mimram have sketched a notion of innocent strategies in the setting of non-alternating asynchronous games (which are essentially the linear, causally deterministic part of TCG), with the purpose of eliminating deadlocks from composition. This appears with more details in Mimram's PhD thesis [Mimram, 2008]. According to their definition, innocence amounts to a correctness criterion inspired from linear logic proof nets. We are not aware of a direct link with the present developments, though this would be interesting to explore.

<footnote n="4">⁴More precisely, visibility and parallel innocence were invented on the 7th of february 2014, a (probably) rainy friday – as witnessed by Figure 8.5.</footnote>
# Chapter 11

## Sequentiality

The conditions of *parallel innocence* and *globularity* developed in the previous chapter enforce *pure computation*, which may still be parallel. In contrast, the conditions developed in this chapter aim to reinstate *sequentiality*, which may still be impure.

*Sequentiality* is probably the simplest of our conditions on strategies, but it still comes with a few subtleties. Firstly, the concept of sequentiality is of course tied to *time*, which is notably absent from concurrent strategies! So it makes sense that the definition will have to refer to linearizations of strategies, in the style developed in the unfolding of causal to non-alternating strategies in Chapter 9. Secondly, a phenomenon occurs that is similar to what we encountered for parallel innocence: as *non-determinism* arises from the combination of parallelism and state, *sequentiality* must reinstate it – but not quite under the same form as in the previous chapter: it is hard to unify *sequential* determinism and *causal* determinism (see discussion in Section 14.2.2).

**Outline.** The developments of this chapter will proceed as follows. In Section 11.1, we develop sequentiality, aiming to show that sequential strategies form a sub-relative Seely ~-category **NTCG-Seq**, that refines to a sub-cartesian closed ~-category $\rightarrowleftarrow$-Seq of $\rightarrowleftarrow$-Strat, supporting the interpretation of IA. In Section 11.2, we show that the non-alternating unfolding $\mathcal{C}$-Unf of Chapter 9 refines into an interpretation-preserving

$$ \llcorner \uparrow \text{-Unf} : \rightarrowleftarrow \text{-Seq} \rightarrow \llcorner \uparrow \text{-Strat} $$

which entails that $\rightarrowleftarrow$-Seq is intensionally fully abstract for IA. In Section 11.3, we show that in combination with *globularity*, $\llcorner \uparrow \text{-Unf}$ yields an interpretation-preserving functor

$$ \llcorner \uparrow \text{-Unf} : \rightarrowleftarrow \text{-SeqGlob} \rightarrow \llcorner \uparrow \text{-InnWB} $$

proving $\rightarrowleftarrow$-SeqGlob intensionally fully abstract for PCF.
# 11.1 Sequentiality

*Sequentiality* has no interaction with mixed boards or well-bracketing, hence we carry it out in the relative Seely ~-category **NTCG**. Likewise, for succinctness, the examples shall be based on the *small* interpretation of ground types (see Section 9.1.1) – although the actual interpretation remains the same as for IA<sub>//</sub>, *i.e.* large.

## 11.1.1 Definition of Sequentiality

What is a sequential causal strategy? The right answer is more subtle than it looks.

**Sequential event structures.** As strategies are certain event structures, it seems reasonable to start by looking at what is a sequential event structure. Event structures are concurrent generalizations of trees or forests: there is a natural representation of forests as event structures, which entails a canonical notion of sequentiality:

**Definition 11.1.1.** An event structure *E* is sequential if it satisfies the conditions:

forestial: for all $e_1, e_2 \le_E e'$, then $e_1 \le_E e_2$ or $e_2 \le_E e_1$.

\#-branching: for all $e_1, e_2 \in E$, $e_1 \#_E e_2$ iff they are causally incomparable.

In other words, a sequential event structure has the shape of a forest as in

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

whose configurations, always totally ordered, correspond to branches of the forest.

However, it is quickly apparent that this is not useful as a definition of sequential causal strategies. Technically, *receptivity* entails that conflicts between negative moves should be exactly as in the game. But negative events may not conflict in the game, as in *e.g.* the initial moves of !B; so no strategy can actually be sequential on !B.

More fundamentally, it turns out that although IA is indeed a sequential language, the shape of causality in the corresponding strategies is certainly *not* sequential. We show two examples: first in Figure 11.1 we repeat the example of Figure 10.3. This is (an affine linear version of) the interpretation of the term in (10.1), a term of IA which should hence be deemed sequential – we see that even though the program itself does not spawn parallel threads, the strategy cannot be sequential as in Definition 11.1.1 as it must show how the program reacts when Opponent does. A similar phenomenon occurs for pure sequential innocent programs: Figure 11.2 shows a configuration of

$$ \vdash \lambda f^{U \to U}. f \text{ skip}; f \text{ skip}; \text{ tt} : (U \to U) \to \mathbb{B} $$

which has a typical shape for pure sequential programs. We see that although the causal shape of pure sequential programs is indeed forestial, the branches do *not* conflict.
<figure><img src="image_192.png" /><figcaption>Figure 11.1: A sequential strategy</figcaption></figure>

<caption>Figure 11.2: A sequential innocent configuration</caption>

**Alternating linearizations.** So how shall we instead define sequentiality?

Let us set the stage for the definition. First, recall that the definition of *linearizations* (Definition 9.2.1) associates to any event structure the set $\mathcal{L}(E)$ of words of $|E|$, which are non-repetitive and whose prefixes form configurations. Now through its display map, $\sigma$ has polarities, so we can look at those *alternating linearizations*:

**Definition 11.1.2.** Consider $E$ an event structure with polarities.

The set $\downarrow\uparrow\mathcal{L}(E)$ of *alternating linearizations* comprises those $s \in \mathcal{L}(E)$ such that polarities alternate and the first move (if $s$ is non-empty) is negative.

We insist that $\downarrow\uparrow\mathcal{L}(\sigma)$ comprises words of events of $\sigma$: we have not yet projected $\sigma$ to the game. Its elements are internal witnesses of sequential executions, invisible to the environment. Despite this, we can perform on $\downarrow\uparrow\mathcal{L}(\sigma)$ certain operations usually done on alternating legal plays on arenas. In particular, we can compute the *P-view*:

**Definition 11.1.3.** Consider $\sigma \in \text{NTCG}(A, B)$ pointed, and $s \in \downarrow\uparrow\mathcal{L}(\sigma)$.

Its *P-view* is the subsequence $\lceil s \rceil$ defined by:

$$ 
\begin{align*}
\lceil \epsilon \rceil &= \epsilon \\
\lceil sm^+ \rceil &= \lceil s^\top m^+ \rceil \\
\lceil sn^+ s' m^- \rceil &= \lceil s^\top n^+ m^- \rceil \quad \text{if } m \text{ points to } n, \\
\lceil sm^- \rceil &= m^- \quad \text{if } m \text{ is minimal,}
\end{align*}
$$

where $m$ points to $n$ if $\partial_\sigma(n) \to_{A \vdash B} \partial_\sigma(m)$; or if $\partial_\sigma(m)$ is minimal in $A$ and $n = \text{init}(m)$.

We say $s \in \downarrow\uparrow\mathcal{L}(\sigma)$ is *P-visible* if for all $t \sqsubseteq s$, $\lceil t \rceil \in \downarrow\uparrow\mathcal{L}(\sigma)$.

This mimics the traditional definition (Definition 3.2.7), except that sequences $s \in \downarrow\uparrow\mathcal{L}(\sigma)$ do not have pointers; those are derived from the immediate causality in the game as in Lemma 9.2.8. Observe that this is where the hypothesis *pointed* is needed: as causal strategies play on $A \vdash B$, the causal dependency from initial moves in $B$ to initial moves in $A$ may only be recovered from the immediate causality in $\sigma$: pointedness ensures that moves minimal in $A$ have a unique initial dependency which must be minimal in $B$, which ensures that the justifier is always well-defined.
**Sequentiality.** Programs of IA will respect sequentiality only within a sequential execution: we wish to impose that in any state reachable in a sequential execution, Player will not throw parallel threads. But as explained in Section 10.1, as for parallel innovation, sequentiality must also reinstate a notion of determinism. Altogether we get:

**Definition 11.1.4.** A strategy $\sigma \in \text{NTCG}(A, B)$ is sequential if:

pointed: if $s \in \sigma$, there is a unique $\text{init}(s) \le_{\sigma} s$ minimal in $\sigma$,

sequential determinism: if $tn_1^+, tn_2^+ \in \downarrow\uparrow\text{-}\mathcal{L}(\sigma)$, then $n_1 = n_2$,

sequential visibility: if $s \in \downarrow\uparrow\text{-}\mathcal{L}(\sigma)$, writing $\lceil s \rceil = s_1 \dots s_n$ and $1 \le j \le n$, if $s_j$ is non-minimal then there is $1 \le i < j$ s.t. $j(s_j) = s_i$,

where the justifier $j(m)$ of $m \in \sigma$ refers to Definition 10.2.1.

For sequential determinism, more than asking that the unfolding acts deterministically on alternating plays, this condition ensures that no internal non-deterministic choice is alternatingly reachable, even when this choice would yield no observable non-deterministic behaviour (surprisingly for us, this turned out necessary).

Sequential visibility is perhaps puzzling, as P-visibility of alternating strategies (Definition 3.2.8) is usually associated not to sequentiality, but to the absence of higher-order state (see Section 3.3.2). From a given control point, a P-visible strategy may only call a procedure bound within the branch of the syntax tree leading to that control point. In contrast, with higher-order state, a program may call a procedure stored in the memory, originating from a remote program phrase outside the current branch. This phenomenon is independent of sequentiality, but in NTCG the causality due to the syntax tree blurs with that passing via state or semaphores. So strategies arising from the interpretation of $IA_{\parallel}$ are “morally” P-visible but formalizing this is nontrivial<fnref n="1" />. For us it is not worth the trouble as P-visibility is not required for full abstraction for $IA_{\parallel}$<fnref n="2" />. Consequently, it suffices to reinstate it once we restrict to sequential strategies.

The strategy in Figure 10.6 is not sequential: it fails sequential determinism as two Player moves are available after the initial move. In contrast, the strategy in Figure 11.1 is sequential: although it may perform non-deterministic choices and play Player moves in parallel, none of these behaviours are reachable in an alternating execution.

We mention a direct consequence of sequentiality:

**Lemma 11.1.5.** Consider $\sigma \in \text{NTCG}(A, B)$ a sequential causal strategy.

Then, it automatically satisfies the following additional condition:

reachable sequentiality: if $tn^+ \in \mathcal{L}(\sigma)$, if $t \in \downarrow\uparrow\text{-}\mathcal{L}(\sigma)$ then $tn \in \downarrow\uparrow\text{-}\mathcal{L}(\sigma)$.

*Proof.* Consider $tn^+ \in \mathcal{L}(\sigma)$ with $t \in \downarrow\uparrow\text{-}\mathcal{L}(\sigma)$. If $tn \notin \downarrow\uparrow\text{-}\mathcal{L}(\sigma)$, this necessarily means that $tn^+$ fails alternation, i.e. $t = sm^+$. But then, we argue that $sn^+ \in \mathcal{L}(\sigma)$ as well. Indeed, this may fail only if $m^+ \to_{\sigma} n^+$. But by *courteous*, this implies $\partial_{\sigma}(m) \to_{A \vdash B} \partial_{\sigma}(n)$ as well. But as a board, $A \vdash B$ is *alternating*, contradiction. $\square$

<footnote n="1">¹This was done by Laird in the first interleaving games model [Laird, 2001b], via threading information.</footnote>

<footnote n="2">²Proposition 5.1.11 shows that non-visible behaviour characteristic of higher-order state can be mimicked by running several threads in parallel and using signaling via *interference* to jump control between them.</footnote>