This means that restricting a sequential strategy to its alternating linearizations only cuts at Opponent moves: it never prevents Player from playing.

### 11.1.2 Categorical Structure

We show that sequential causal strategies form a sub-~-category of NTCG.

**Sequentiality of copycat.** First, we show that the copycat strategy is sequential:

**Lemma 11.1.6.** Consider A a --board. Then, $\mathfrak{c}_A : A \vdash A$ is sequential.

*Proof.* First, $\mathfrak{c}_A$ is pointed, as its causal shape is forestial. For the other two conditions, we observe that the even-length alternating linearizations of $\mathfrak{c}_A$ are exactly those words on $s \in |A_1 \vdash A_2|^*$ (with indices used for disambiguation only) such that for all even-length prefix $t \sqsubseteq s$, $t \vdash A_1 = t \vdash A_2$, with the restriction $\uparrow$ defined in the obvious way. The two conditions sequential determinism and sequential visibility follow easily. $\square$

**Composition of sequential determinism.** As often when introducing a new condition, much of the work required is in checking stability under composition. Here in particular, something is striking: recall from Section 4.1.3 that proving associativity of composition for alternating strategies involves the study of a “state diagram” for interactions (in contrast, nothing of the sort shows up when constructing the associator for the composition of causal strategies) – this diagram intervenes again here.

Let us start by introducing some further terminology. Consider $\sigma : A \vdash B$ and $\tau : B \vdash C$ two causal strategies, and $p \in \tau \otimes \sigma$ an event of the interaction. We have analyzed above Lemma 6.2.14 the different possible polarities of $p$ – at least one of $p_\sigma \in \sigma$ and $p_\tau \in \tau$ must be defined, possibly both if $p$ occurs in $B$, in which case $p$ does not appear in the composition. Otherwise $p$ occurs in $A$ or $C$ and we have $p \in \tau \odot \sigma$; let us write $p_\odot = p \in \tau \odot \sigma$ if that is the case, and undefined otherwise.

Applying these projections move-by-move, from $s \in \mathcal{L}(\tau \otimes \sigma)$ we get:

**Lemma 11.1.7.** Consider $s = s_1 \dots s_n \in \mathcal{L}(\tau \otimes \sigma)$. Then, forming

$$s_{\sigma} = (s_1)_{\sigma} \dots (s_n)_{\sigma}$$

$$s_{\tau} = (s_1)_{\tau} \dots (s_n)_{\tau}$$

$$s_{\odot} = (s_1)_{\odot} \dots (s_n)_{\odot},$$

removing moves where the projection is undefined, we have that

$$u_{\sigma} \in \mathcal{L}(\sigma), \quad u_{\tau} \in \mathcal{L}(\tau), \quad u_{\odot} \in \mathcal{L}(\tau \odot \sigma).$$

*Proof.* From the definition, it is immediate that for all $x^\sigma \in \mathcal{C}(\sigma)$, $x^\tau \in \mathcal{C}(\tau)$ causally compatible, we have $(x^\tau \otimes x^\sigma)_\sigma = x^\sigma \in \mathcal{C}(\sigma)$ (where $(x^\tau \otimes x^\sigma)_\sigma$ is obtained as for linearizations above, applying $(-)_\sigma$ event-by-event), $(x^\tau \otimes x^\sigma)_\tau = x^\tau \in \mathcal{C}(\tau)$ and $(x^\tau \otimes x^\sigma)_\odot \in \mathcal{C}(\tau \odot \sigma)$ (by definition of $\tau \odot \sigma$). The claims on linearizations follow. $\square$
A linearization $u \in \mathcal{L}(\sigma)$ may be – or not – alternating, i.e. $u \in \mathcal{J}\uparrow\mathcal{L}(\sigma)$. If it is, then as for legal plays on arenas (Definition 3.1.4) two cases are possible: if it has even length (so that the last move is by Player), we say that it is **in state O**. If it has odd length (so that the last move is by Opponent), we say that it is **in state P**.

Putting the projections of the lemma above to work, we have the state diagram:

**Lemma 11.1.8.** Consider A, B, C --boards, and $\sigma$: A $\vdash$ B, $\tau$: B $\vdash$ C sequential.

For any $u \in \mathcal{L}(\tau \circledast \sigma)$ such that $u_\odot \in \mathcal{J}\uparrow\mathcal{L}(\tau \circledast \sigma)$ we have $u_\sigma \in \mathcal{J}\uparrow\mathcal{L}(\sigma)$ and $u_\tau \in \mathcal{J}\uparrow\mathcal{L}(\tau)$, and we are in one of the following three cases:

(1) $u_\sigma, u_\tau, u_\odot$ are respectively in state O, O, O,

(2) $u_\sigma, u_\tau, u_\odot$ are respectively in state O, P, P,

(3) $u_\sigma, u_\tau, u_\odot$ are respectively in state P, O, P.

*Proof.* By induction on $u$. If $u$ is empty, this is clear. Consider $um \in \mathcal{L}(\tau \circledast \sigma)$. By induction hypothesis $u$ is in one of cases (1), (2) and (3). We distinguish cases:

(1) Seeking a contradiction, assume $m$ occurs in B. Then, one of $m_\sigma$ or $m_\tau$ is positive – say w.l.o.g. the former. By IH, $u_\sigma$ is alternating in state O, so ends with a Player move. But so, $u_\sigma m_\sigma^+ \in \mathcal{L}(\sigma)$ with $u_\sigma \in \mathcal{J}\uparrow\mathcal{L}(\sigma)$, so $u_\sigma m_\sigma \in \mathcal{J}\uparrow\mathcal{L}(\sigma)$ since $\sigma$ satisfies reachable sequentiality, contradiction. So, $m$ occurs in A or C – assume w.l.o.g. in A. Since $u_\odot$ is in state O, $m$ is negative – then, it is direct that $um$ satisfies (3).

(2) First assume $m$ occurs in A. Since $u_\odot \in \mathcal{J}\uparrow\mathcal{L}(\tau \circledast \sigma)$ is in state P, then $m$ is positive; then $m_\sigma$ is positive, contradicting reachable sequentiality of $\sigma$ with the fact that $u_\sigma$ is in state O. Similarly, if $m$ occurs in B it has polarity $r$ and we transition to (3), and if $m$ occurs in C it has polarity $r$ and we transition to (1).

(3) Symmetric to (2). $\square$

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

As long as the external Opponent respects the alternation discipline, interactions follow the familiar *state diagram* of interactions in alternating game semantics, shown in Figure 4.2. None of the interacting agents can be the first to break alternation, so the interaction ends up alternating. It follows that $\tau \circledast \sigma$ satisfies sequential determinism:

**Proposition 11.1.9.** Consider $\sigma$: A $\vdash$ B and $\tau$: B $\vdash$ C sequential *causal strategies*. Then, $\tau \circledast \sigma$ satisfies sequential determinism.

*Proof.* Consider $tn_1^+, tn_2^+ \in \mathcal{J}\uparrow\mathcal{L}(\tau \circledast \sigma)$ completed to $u_1n_1, u_2n_2 \in \mathcal{L}(\tau \circledast \sigma)$, and $u'$ the greatest common prefix of $u_1n_1$ and $u_2n_2$, with $u'm_1 \subseteq u_1n_1$ and $u'm_2 \subseteq u_2n_2$. Necessarily, the visible restriction of $u'$ is a prefix $t' \subseteq tn_i$, so in particular $t' \in \mathcal{J}\uparrow\mathcal{L}(\tau \circledast \sigma)$. We distinguish cases on Lemma 11.1.7 applied to $u'$.

For (1) (state OOO), $m_1$ and $m_2$ must both be the next negative event appearing in $t$, so $m_1 = m_2$, contradiction. For (2) (state OPP), $m_1$ and $m_2$ both have polarity $r$ and we have $u'_\tau \in \mathcal{J}\uparrow\mathcal{L}(\tau)$, $u'_\tau(m_1)_\tau^+, u'_\tau(m_2)_\tau^+ \in \mathcal{J}\uparrow\mathcal{L}(\tau)$. Hence $(m_1)_\tau = (m_2)_\tau$ since $\tau$ satisfies sequential determinism – so $m_1 = m_2$ by local injectivity of the projection $\Pi_\tau$; contradiction. For (3) (state POP), the reasoning is symmetric. $\square$

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

By the state diagram, in an alternating interaction, only one agent has control at any point. So any alternatingly reachable non-deterministic choice in $\tau \circledast \sigma$ can be attributed
to $\sigma$ and $\tau$. Since they are both deterministic, no such choice exists. We single out the linearizations of an interaction $u \in \mathcal{L}(\tau \oplus \sigma)$ that satisfy the state diagram of interactions as in Lemma 11.1.8: the alternating interactions.

**Definition 11.1.10.** Consider $u \in \mathcal{L}(\tau \oplus \sigma)$. It is an alternating interaction, written $u \in \downarrow\uparrow\mathcal{L}(\tau \oplus \sigma)$, if $u_\odot \in \downarrow\uparrow\mathcal{L}(\tau \odot \sigma)$, $u_\sigma \in \downarrow\uparrow\mathcal{L}(\sigma)$ and $u_\tau \in \downarrow\uparrow\mathcal{L}(\tau)$.

The notation $\downarrow\uparrow\mathcal{L}(\tau \oplus \sigma)$ should hopefully not cause confusion, since $\tau \oplus \sigma$ does not have polarities: the polarity of synchronized events is indetermined.

A fundamental property is that an alternating linearization between sequential strategies is necessarily witnessed by an alternating interaction:

**Lemma 11.1.11.** Consider $\sigma: A \vdash B$ and $\tau: B \vdash C$ sequential, and $u \in \mathcal{L}(\tau \oplus \sigma)$. If $u_\odot \in \downarrow\uparrow\mathcal{L}(\tau \odot \sigma)$, then $u \in \downarrow\uparrow\mathcal{L}(\tau \oplus \sigma)$.

*Proof.* By induction on $u$. Consider $um \in \mathcal{L}(\tau \oplus \sigma)$ such that $(um)_\odot \in \downarrow\uparrow\mathcal{L}(\tau \odot \sigma)$. By induction hypothesis, $u \in \downarrow\uparrow\mathcal{L}(\tau \oplus \sigma)$, so it must be in one of the states of Lemma 11.1.7. For (1) (state OOO). Then necessarily $m$ is negative, and it is immediate that the invariant is preserved. For (2) (state OPP), then we reason by cases depending on when $m$ occurs. If it occurs in $A$, then it must be positive in $\tau \odot \sigma$ since $(um)_\odot \in \downarrow\uparrow\mathcal{L}(\tau \odot \sigma)$. Then $m_\sigma$ is defined and positive. So $u_\sigma \in \downarrow\uparrow\mathcal{L}(\sigma)$ and $u_\sigma m_\sigma^+ \in \mathcal{L}(\sigma)$, thus by Lemma 11.1.5 we have $u_\sigma m_\sigma^+ \in \downarrow\uparrow\mathcal{L}(\sigma)$ as well, contradicting that $u_\sigma$ is in state O. Thus $m$ occurs in $B$ or $C$, so that $m_\tau$ is defined. But then $u_\tau \in \downarrow\uparrow\mathcal{L}(\tau)$ and $u_\tau m_\tau \in \mathcal{L}(\tau)$, thus by Lemma 11.1.5 we have $u_\tau m_\tau \in \downarrow\uparrow\mathcal{L}(\tau)$, thus $m_\tau$ is positive. If $m$ occurs in $B$ then the invariant is preserved and $um$ is in state POP, if $m$ occurs in $C$ then the invariant is preserved and $um$ is in state OOO. Finally, (3) (state POP) is symmetric. $\square$

**Composition of sequential visibility.** Next, we must prove that the composition of sequential strategies satisfies sequential visibility. This is a direct variation of the stability under composition of P-visible strategies in alternating game semantics.

As announced, we generalize P-views to alternating interactions:

**Definition 11.1.12.** For $u \in \downarrow\uparrow\mathcal{L}(\tau \oplus \sigma)$, we define the subsequence $\lceil u \rceil$ with

$$ \begin{align*} \lceil \varepsilon \rceil &= \varepsilon \\ \lceil um \rceil &= \lceil u \rceil m \tag{if $m$ is positive or synchronized} \\ \lceil un^+u'm^- \rceil &= \lceil u \rceil n^+m' \tag{if $m$ is justified by $n$} \\ \lceil um^- \rceil &= m^- \tag{$m^-$ minimal} \end{align*} $$

Those are the same clauses as in Definition 11.1.3, applying to interactions rather than alternating linearizations of a causal strategy. The idea is the same: we browse the sequence, going back in time and following pointers of moves by the external Opponent.

The main argument behind the composition of sequential visibility is:

**Lemma 11.1.13.** Consider $u \in \downarrow\uparrow\mathcal{L}(\tau \oplus \sigma)$.

Writing $\lceil u \rceil = u_1 \dots u_n$ and for $1 \le j \le n$, if $u_j$ is non-minimal in $\tau \oplus \sigma$ then there is $1 \le i < j$ such that $j(u_j) = u_i$ – where $j(m)$ refers to Definition 10.2.3.
*Proof.* We show by mutual induction the following properties, for $u \in \text{↓}^{\rightarrow}\mathcal{L}(\tau \otimes \sigma)$:

(1) writing $\lceil u \rceil = u_1 \dots u_n$ and for $1 \le j \le n$, if $u_j$ is non-minimal in $\tau \otimes \sigma$
then there is $1 \le i < j$ such that $j(u_j) = u_i$,

(2) if $u = vm$ with $m_\sigma$ defined, $\lceil u_\sigma \rceil$ is a subsequence of $\lceil u \rceil_\sigma$,

(3) if $u = vm$ with $m_\tau$ is defined, $\lceil u_\tau \rceil$ is a subsequence of $\lceil u \rceil_\tau$,

and we refer to (1) as $\lceil u \rceil$ being *well-justified*.

For (1), write $u = vn$. If $n$ is negative, then either it is minimal (then the property
is trivial), or $u = v_1l^+v_2n^-$ where $j(n^-) = l^+$ (say w.l.o.g. $l$ is positive for $\sigma$). Then
by induction hypothesis, $\lceil v_1l^+ \rceil$ is well-justified and as $\lceil v_1l^+v_2n^- \rceil = \lceil v_1l^+n^- \rceil$ with
$j(n) = l$, $\lceil u \rceil$ is well-justified as well. Otherwise, $\lceil u \rceil = \lceil v \rceil n$ and by induction hypothe-
sis, $\lceil v \rceil$ is well-justified, but we must show that the justifier of $n$ is in $\lceil v \rceil$. Necessarily $n$
is positive for $\sigma$ or $\tau$, say $\sigma$ w.l.o.g.. As $(vn)_\sigma = v_\sigma n_\sigma^+ \in \text{↓}^{\rightarrow}\mathcal{L}(\sigma)$, as $\sigma$ is sequentially
visible, $n_\sigma$ must point within $\lceil v_\sigma \rceil$. Now by Lemma 11.1.8, since $n$ is positive for $\sigma$, $v$ is
in state POP. If the last move of $v$ occurs in $C$, since $v_\circ$ has state P it must be negative.
But since $v_\tau$ has state O it must be Player – contradiction, so the last move of $v$ occurs
in $A$ or $B$ and its projection to $\sigma$ is defined. Thus by (2) of the induction hypothesis on
$v$, $\lceil v_\sigma \rceil$ is a subsequence of $\lceil v \rceil_\sigma$. Now by sequential visibility of $\sigma$, the justifier of $n_\sigma$
is in $\lceil v_\sigma \rceil$, thus in $\lceil v \rceil_\sigma$, hence it $\lceil v \rceil$.

For (2), assume $m_\sigma$ is defined. If it is positive, then by Lemma 11.1.8 $v$ must be
in state POP; write $v = v'n$. If $n$ occurs in $C$, then it must be negative since $v_\circ$ is in
state P, but this contradicts that $v_\tau$ is in state O. Thus, $n$ occurs in $A$ or $C$, but then $n_\sigma$
is defined (and negative). Hence, by induction hypothesis, $\lceil v_\sigma \rceil$ is a subsequence of
$\lceil v \rceil_\sigma$. But $\lceil um \rceil_\sigma = \lceil u_\sigma \rceil m_\sigma$ and $\lceil u \rceil_\sigma = \lceil v \rceil_\sigma m_\sigma$, hence $\lceil u_\sigma \rceil$ is a subsequence of
$\lceil u \rceil_\sigma$ as required. Next if $m_\sigma$ is negative, write $u = v_1nv_2m$ with $j(m) = n$. Two sub-
cases arise. If $m$ occurs in $A$, then it is negative and $\lceil u \rceil = \lceil v_1 \rceil nm$. Likewise, $\lceil u_\sigma \rceil =
\lceil (v_1)_\sigma \rceil n_\sigma^+ m_\sigma^-$, so the result follows by induction hypothesis. Finally if $m$ occurs in $B$,
then by (1), $\lceil u \rceil$ is well-justified, hence $n$ appears in $\lceil v_1nv_2 \rceil$, i.e. $\lceil v_1nv_2 \rceil = \lceil v_1 \rceil nm_2$
and $\lceil u \rceil_\sigma = \lceil v_1 \rceil n_\sigma (v_2')_\sigma m_\sigma$. Likewise by definition $\lceil u_\sigma \rceil = \lceil (v_1)_\sigma \rceil n_\sigma m_\sigma$. Finally by
induction hypothesis $\lceil (v_1)_\sigma \rceil$ is a subsequence of $\lceil v_1 \rceil_\sigma$, hence the result follows.

For (3), it is the same reasoning as above.

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

From this, we may conclude:

**Proposition 11.1.14.** Consider $\sigma : A \vdash B$ and $\tau : B \vdash C$ sequential causal strategies.
Then, $\tau \odot \sigma$ satisfies sequential visibility.

*Proof.* Consider $s \in \text{↓}^{\rightarrow}\mathcal{L}(\tau \odot \sigma)$, and write $\lceil s \rceil = s_1 \dots s_n$, consider $1 \le j \le n$ with $s_j$
non-minimal. Necessarily, there is $u \in \mathcal{L}(\tau \otimes \sigma)$ such that $u_\circ = s \in \text{↓}^{\rightarrow}\mathcal{L}(\tau \odot \sigma)$. By
Lemma 11.1.11, we have $u \in \text{↓}^{\rightarrow}\mathcal{L}(\tau \otimes \sigma)$. Write $\lceil u \rceil = u_1 \dots u_m$ – from the definition
it is immediate that $\lceil u \rceil_\circ = \lceil s \rceil$, so there is a unique $j'$ such that $u_{j'} = s_j$ (necessarily
non-minimal). By Lemma 11.1.13, there is some $1 \le i' < j'$ such that $j(u_{j'}) = u_{i'}$. First, $u_{i'}$ may occur in $B$ (if $u_{j'}$ is minimal in $A$ and $u_{i'}$ minimal in $B$). Then by Lemma
11.1.13, there is $1 \le k' < i'$ such that $j(u_{k'}) = u_{k'}$, necessarily minimal in $C$. But then
$j(u_{j'}) = (u_{k'})$ for $\tau \odot \sigma$ – but $u_{k'} = s_k$ for some $1 \le k < j$, and the property is proved.
If $u_{i'}$ does not occur in $B$, then it is visible and $j(u_{j'}) = u_{i'}$ in $\tau \odot \sigma$ as well. As above
$u_{i'} = s_i$ for some $1 \le i < j$, which concludes the proof.

$\square$

<figure><img src="image_196.png" /></figure>
Putting everything together, we have:

**Corollary 11.1.15.** The ~-category NTCG admits a lluf sub~-category NTCG-Seq with morphisms restricted to causal sequential strategies.

*Proof.* Firstly, copycat is sequential by Lemma 11.1.6. Consider $\sigma \in \text{NTCG}(A, B)$ and $\tau \in \text{NTCG}(B, C)$ sequential. Firstly, the proof that $\tau \odot \sigma \in \text{NTCG}(A, C)$ is pointed is as in Proposition 10.2.6 (which did not rely on visibility). Composition of sequential determinism and sequential visibility are Propositions 11.1.9 and 11.1.14. □

Next, we move to the rest of the categorical structure.

### 11.1.3 A Relative Seely ~-Category

All structural morphisms of NTCG are obtained by lifting, and it is immediate (as for Lemma 11.1.6) that they are sequential. The next step is to prove that other operations on strategies (tensor, pairing, currying and promotion) preserve sequentiality. We shall consider them all, focusing on the two non-trivial cases: tensor and promotion.

**Tensor.** Consider $\sigma : A \vdash B$ and $\tau : C \vdash D$. Similarly to interactions, if $m \in \sigma \otimes \tau$, write $m_\sigma \in \sigma$ as $m'$ if $m = (1, m')$ and undefined otherwise; and $m_\tau \in \tau$ partially defined symmetrically. For $s \in \mathcal{L}(\sigma \otimes \tau)$, write $s_\sigma \in \mathcal{L}(\sigma)$ and $s_\tau \in \mathcal{L}(\tau)$ defined in the obvious way. Using these projections, the stability of sequentiality under tensor exploits a state case analysis, similar to Lemma 11.1.8:

**Lemma 11.1.16.** *Take A, B, C, D --boards, $\sigma : A \vdash B$, $\tau : C \vdash D$ sequential. If $s \in \downarrow\vdash\mathcal{L}(\sigma \otimes \tau)$, then $s_\sigma \in \downarrow\vdash\mathcal{L}(\sigma)$, $s_\tau \in \downarrow\vdash\mathcal{L}(\tau)$. Moreover, one of*

(1) $s_\sigma, s_\tau$, $s$ are respectively in state O, O, O,

(2) $s_\sigma, s_\tau$, $s$ are respectively in state O, P, P,

(3) $s_\sigma, s_\tau$, $s$ are respectively in state P, O, P,

must hold.

*Proof.* Straightforward by induction on $s$, using reachable sequentiality of $\sigma$ and $\tau$. □

Thus, in a tensor of sequential strategies $\sigma \otimes \tau$, at most one of $\sigma$ and $\tau$ has control at a given point in time, and only Opponent is able to switch. From this, we may prove:

**Proposition 11.1.17.** *Take A, B, C, D --boards, $\sigma : A \vdash B$, $\tau : C \vdash D$ sequential. Then, $\sigma \otimes \tau$ is sequential.*

*Proof. Pointed:* this is straightforward, as the event structure $\sigma \otimes \tau$ is simply $\sigma \parallel \tau$.

*Sequential determinism:* Consider $sm^+, sn^+ \in \downarrow\vdash\mathcal{L}(\sigma \otimes \tau)$. By Lemma 11.1.16, $s_\sigma, s_\tau$, $s$ must be in one of the states OOO, OPP, or POP. If it is OOO, then $s$ is in state O, contradicting $sm^+ \in \downarrow\vdash\mathcal{L}(\sigma \otimes \tau)$. If it is OPP, then $m_\tau^+, n_\tau^+$ must be defined, or contradict that $s_\sigma$ is in state O – but then, $(sm^+)_\tau = s_\tau m_\tau^+ \in \mathcal{L}(\tau)$, and $(sn)_\tau = s_\tau n_\tau^+ \in \mathcal{L}(\tau)$. As $s_\tau \in \downarrow\vdash\mathcal{L}(\tau)$ is in state P, thus $s_\tau m_\tau^+, s_\tau n_\tau^+ \in \downarrow\vdash\mathcal{L}(\tau)$, hence $m_\tau^+ = n_\tau^+$ by sequential determinism of $\tau$. Hence, $m^+ = n^+$ as required. Finally, if $s$ is in state POP,
the reasoning is symmetric.

**Sequential visibility:** Consider $s \in \mathcal{J}\uparrow\mathcal{L}(\sigma \otimes \tau)$. By Lemma 11.1.16, we have $s_\sigma \in \mathcal{J}\uparrow\mathcal{L}(\sigma)$ and $s_\tau \in \mathcal{J}\uparrow\mathcal{L}(\tau)$. Moreover, it is immediate from Lemma 11.1.16 that only Opponent may switch between $\sigma$ and $\tau$, and consequently $\lceil s \rceil$ is entirely in $\sigma$ or in $\tau$. Hence, sequential visibility of $\sigma$ and $\tau$ allow us to conclude. $\square$

**Promotion.** The proof for promotion is analogous. Consider A and B strict $--$boards, and $\sigma : !A \vdash B$ sequential. Recall that every move $m \in \sigma^1$ has the form $m = (i, m')$ where $i \in \mathbb{N}$ is its copy index. For $j \in \mathbb{N}$ we then partially define $s_j = m'$ if $i = j$ and undefined otherwise. Again, if $s \in \mathcal{L}(\sigma \otimes \tau)$, then its projection $s_i$ for $i \in \mathbb{N}$ is defined in the obvious way. Using these, we state the promotion state case analysis:

**Lemma 11.1.18.** Consider A, B strict $--$boards, and $\sigma : !A \vdash B$ sequential.

For any $s \in \mathcal{J}\uparrow\mathcal{L}(\sigma^1)$, for any $i \in \mathbb{N}$, $s_i \in \mathcal{J}\uparrow\mathcal{L}(\sigma)$ and we are in one of:

(1) $s$ has state $O$, and for all $i \in \mathbb{N}$, $s_i$ has state $O$,

(2) $s$ has state $P$, and there exists a unique $i \in \mathbb{N}$ such that $s_i$ has state $P$.

*Proof.* Straightforward by induction on $s$, using reachable sequentiality of $\sigma$. $\square$

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

As for tensor, we conclude:

**Proposition 11.1.19.** Consider A, B strict $--$boards, and $\sigma : !A \vdash B$ sequential.

Then, $\sigma^1 : !A \vdash !B$ is a sequential strategy.

*Proof.* Similar to the proof of Proposition 11.1.17. $\square$

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

**Remainder of the structure.** That pairing preserves sequentiality is straightforward; so is currying as the internal event structure is unchanged (along with the justifier function $j(-)$). Altogether, we have the ingredients to conclude the relative Seely structure:

**Theorem 11.1.20.** There is NTCG-Seq, a relative Seely sub-$\sim$-category of NTCG, with morphisms restricted to sequential causal strategies.

*Proof.* Follows from Corollary 11.1.15, Propositions 11.1.17 and 11.1.19, and omitted direct verifications for pairing, currying and structural isomorphisms. $\square$

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

### 11.1.4 $\to$-Seq and Interpretation of IA

As a relative Seely $\sim$-category, NTCG-Seq induces a cartesian closed $\sim$-category:

**Definition 11.1.21.** There is $\to$-Seq, a cartesian closed sub-$\sim$-category of $\to$-Strat.

Its objects are mixed boards, its morphisms are those of $\to$-Strat restricted to sequential strategies, and the equivalence relation is as in $\to$-Strat.

For stateless primitives (i.e. PCF primitives, reference and semaphore queries, bad variables and semaphores), it is direct by inspection to show that the corresponding strategies are sequential – we omit those verifications. Finally, we also have:
**Proposition 11.1.22.** Consider $\sigma \in \rightarrow\text{-Seq}(V, A)$ sequential with A well-opened.
Then, $\sigma \odot \text{cell} \in \rightarrow\text{-Strat}(\tau, A)$ is also sequential.

*Proof.* Although cell is not a strategy (it fails courtesy), it does satisfy conditions sequential determinism and sequential visibility (the latter involves the notion of justifier which is defined in Definition 10.2.1 only for pointed strategies, but this is needed only for strategies from A to B – it is not necessary for cell : V). It follows from the same arguments as in Proposition 11.1.9 and 11.1.14 that $\sigma \odot \text{cell}$ satisfies these two conditions – it is also obvious from A well-opened that $\sigma \odot \text{cell}$ is pointed. $\square$

The exact same reasoning establishes that for $\sigma \in \rightarrow\text{-Seq}(S, A)$ with A well-opened, $\sigma \odot \text{lock} : A$ is sequential as well. Altogether we have the ingredients for:

**Corollary 11.1.23.** The interpretation of $IA_\parallel$ in $\rightarrow\text{-Strat}$ of Chapter 9 restricts to an adequate interpretation of IA in $\rightarrow\text{-Seq}$.

*Proof.* That the interpretation of IA terms yields sequential strategies follows from Theorem 11.1.20, verifications for basic primitives, Proposition 11.1.22 for new references, and the analogous for new semaphores. Adequacy is an immediate consequence of adequacy of the adequacy of the interpretation of $IA_\parallel$ in $\text{NTCG}_1$ (Theorem 9.1.5). $\square$

## 11.2 The Alternating Unfolding

Now that we have constructed $\rightarrow\text{-Seq}$ and proved that the interpretation of IA indeed yields sequential causal strategies, we examine the unfolding of $\rightarrow\text{-Seq}$ onto $\downarrow\uparrow$-Strat.

### 11.2.1 Alternating Unfolding on a Mixed Board

The alternating unfolding of a sequential strategy is a simple refinement of the non-alternating unfolding of Section 9.2 – recall that for causal $\sigma : A$ on mixed board A, its unfolding was obtained by first considering all linearizations of $\sigma$, then displaying these linearizations to the game, and finally recovering plays with pointers by pointfixion.

We now adapt this to the alternating case.

**Alternating linearizations.** Recall from Definition 11.1.2 the set $\downarrow\uparrow\text{-}\mathcal{L}(E)$ of the alternating linearizations of an event structure with polarities $E$, which applies to a causal strategy $\sigma : A$ thanks to the polarities inherited from A. Our first observation is:

**Lemma 11.2.1.** Consider $\sigma : A$ a causal strategy on a board A.
The length-preserving monotone function of Lemma 9.2.4 restricts to

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

*Proof.* Straightforward. $\square$
We recall our convention in such a situation: alternating linearizations in $\sigma$ are often denoted as $s^\sigma \in \downarrow\uparrow\mathcal{L}(\sigma)$ with the causal strategy added as superscript, and their display is $s_A^\sigma = \partial_\sigma(s^\sigma) \in \downarrow\uparrow\text{-Plays}(A)$. As in the non-alternating case, this displayed linearization enjoys the main properties expected of what would be a play-based alternating strategy on $A$ – to prove that, the following lemma shall be useful:

**Lemma 11.2.2.** Consider A a board, and $\sigma$: A a sequential causal strategy.

For any $s \in \downarrow\uparrow\text{-Plays}(\sigma)$, there is a unique $t \in \downarrow\uparrow\mathcal{L}(\sigma)$ such that $s = \partial_\sigma(t)$.

*Proof.* Immediate by induction, using *receptivity* and *sequential determinism*. $\square$

We obtain a strategy in the sense of *simple games* (Definition 3.1.2):

**Proposition 11.2.3.** Consider $\sigma$: A a sequential strategy on board A. Then, the set

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

satisfies the following properties:

non-empty: $\epsilon \in \downarrow\uparrow\text{-Plays}(\sigma)$,

prefix-closed: for all $t \in \downarrow\uparrow\text{-Plays}(\sigma)$, is $s \sqsubseteq t$, then $s \in \downarrow\downarrow\text{-Plays}(\sigma)$,

receptive: if $s \in \downarrow\uparrow\text{-Plays}(\sigma)$ and $sa^- \in \downarrow\uparrow\text{-Plays}(A)$, then $sa \in \downarrow\uparrow\text{-Plays}(\sigma)$,

deterministic: if $sa^+, sb^+ \in \downarrow\uparrow\text{-Plays}(\sigma)$, then $a^+ = b^+$,

*Proof.* Non-empty, prefix-closed, receptive. Same proof as for Proposition 9.2.5.

*Deterministic.* Immediate by Lemma 11.2.2 and sequential determinism. $\square$

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

With the appropriate phrasing it also follows that $\downarrow\uparrow\text{-Plays}(\sigma)$ is P-visible, but we have not defined the P-view of alternating plays on A and it does not seem worth the detour. Thus, following the non-alternating case, we shall now apply the above to a sequential strategy on a mixed board, and follow it up with pointfixion.

**Alternating linearizations up to symmetry.** The above proposition does not say anything about symmetry. Recall that we proved in Proposition 7.1.15 that for A a gws (hence, in particular, for A a board), the set of plays $\downarrow\uparrow\text{-Plays}(A)$ equipped with the equivalence relation $\cong_A$ (from Definition 7.1.14) is automatically an AJM game. Accordingly, we expect that $\downarrow\uparrow\text{-Plays}(\sigma)$ is *uniform* in the sense of AJM games – this is natural as a consistency check, but it shall also be required later on.

To prove this, the first step is a symmetry-aware version of Lemma 11.2.2. Here for $s^\sigma, t^\sigma \in \downarrow\uparrow\mathcal{L}(\sigma)$, we write $s^\sigma \cong_\sigma t^\sigma$ for the equivalence relation defined in exactly the same way as the AJM equivalence on plays on gws (Definition 7.1.14).

**Lemma 11.2.4.** Consider A a --board, $\sigma$: A a sequential causal strategy.

For all $s^\sigma, t^\sigma \in \downarrow\uparrow\mathcal{L}(\sigma)$, if $s_A^\sigma \cong_A t_A^\sigma$ then $s^\sigma \cong_\sigma t^\sigma$.
*Proof.* By induction on the length of linearizations – note from $s_A^\sigma \cong_A t_A^\sigma$ that $s^\sigma$ and $t^\sigma$ have the same length. If they are both empty then there is nothing to prove.

Consider $s^\sigma m^- \in \downarrow\uparrow\mathcal{L}(\sigma)$ displaying to $s_A^\sigma a^- \in \downarrow\uparrow\text{-Plays}(\sigma)$, and $t^\sigma n^- \in \downarrow\uparrow\mathcal{L}(\sigma)$ displaying to $t_A^\sigma b^- \in \downarrow\uparrow\text{-Plays}(\sigma)$, s.t. $s_A^\sigma a^- \cong_A t_A^\sigma b^-$. By IH, we have $s^\sigma \cong_\sigma t^\sigma$. But then it immediately follows by $\sim$-receptivity of $\sigma$ that $s^\sigma m^- \cong_\sigma t^\sigma n^-$ as required.

Now, consider $s^\sigma m^+ \in \downarrow\uparrow\mathcal{L}(\sigma)$ displaying to $s_A^\sigma a^+ \in \downarrow\uparrow\text{-Plays}(\sigma)$, and $t^\sigma n^+ \in \downarrow\uparrow\mathcal{L}(\sigma)$ displaying to $t_A^\sigma b^+ \in \downarrow\uparrow\text{-Plays}(\sigma)$, such that $s_A^\sigma a^+ \cong_A t_A^\sigma b^+$. By induction hypothesis, we have $s^\sigma \cong_\sigma t^\sigma$. Now, by extension for $\cong_\sigma$, we must have $t^\sigma p^+ \in \downarrow\uparrow\mathcal{L}(\sigma)$ such that $s^\sigma m^+ \cong_\sigma s^\tau p^+$. But by sequential determinism, it follows that $n^+ = p^+$, hence we do have $s^\sigma m^+ \cong_\sigma t^\sigma n^+$ as required. $\square$

The following lemma has two purposes: it will ensure that strategies obtained as displayed linearizations are indeed uniform in the sense of AJM strategies, and that two positively isomorphic sequential strategies will yield equivalent AJM strategies.

**Lemma 11.2.5.** Consider A a $-$board and $\sigma, \tau$: A sequential causal strategies.

If $\sigma \approx \tau$ (as in Section 7.2.1), then $\downarrow\uparrow\text{-Plays}(\sigma) \approx \downarrow\uparrow\text{-Plays}(\tau)$ (as in Definition 3.4.4).

*Proof.* If $\sigma \approx \tau$, by Definition 7.2.4 there is an iso $\varphi : \sigma \cong \tau$ of ess satisfying

$$ \partial_{\tau} \circ \varphi \sim^{+} \partial_{\sigma}, $$

which in particular entails that for all $s^\sigma \in \downarrow\uparrow\mathcal{L}(\sigma)$, we have $s_A^\sigma \cong_A \varphi(s^\sigma)_A$. Combined with Lemma 11.2.4, this has an important direct consequence: if $s^\sigma \in \downarrow\uparrow\mathcal{L}(\sigma)$ and $s^\tau \in \downarrow\uparrow\mathcal{L}(\tau)$ are such that $s_A^\sigma \cong_A s_A^\tau$, then it also follows that $\varphi(s^\sigma)_A \cong_A s_A^\tau$, and consequently $\varphi(s^\sigma) \cong_\tau s^\tau$ by Lemma 11.2.4 – we shall use that in the proof below.

→-simulation: consider $s_A^\sigma a^+ \in \downarrow\uparrow\text{-Plays}(\sigma)$, $s_A^\tau \in \downarrow\uparrow\text{-Plays}(\tau)$ such that $s_A^\sigma \cong_A s_A^\tau$. By our auxiliary statement, we necessarily have $\varphi(s^\sigma) \cong_\tau s^\tau$. Now writing $s^\sigma m^+ \in \downarrow\uparrow\mathcal{L}(\sigma)$ the witness for $s_A^\sigma a^+ \in \downarrow\uparrow\text{-Plays}(\sigma)$, we have $\varphi(s^\sigma)\varphi(m^+) \in \downarrow\uparrow\mathcal{L}(\tau)$ with $\varphi(s^\sigma) \cong_\tau s^\tau$, hence by extension for $\tau$ there is $n^+$ such that $\varphi(s^\sigma)\varphi(m^+) \cong_\tau s^\tau n^+$, with

$$ s_A^\sigma a^+ \cong_A \partial_\sigma(s^\sigma m^+) \cong_A \partial_\tau(s^\tau n^+) = s_A^\tau b^+ \in \downarrow\uparrow\text{-Plays}(\tau) $$

as required. The case for $\leftarrow$-simulation is symmetric.

→-receptive: consider $s_A^\sigma a^- \in \downarrow\uparrow\text{-Plays}(\sigma)$, $s_A^\tau \in \downarrow\uparrow\text{-Plays}(\tau)$, and $s_A^\sigma a^- \cong_A s_A^\tau b^-$. By the observation above, $\varphi(s^\sigma) \cong_\tau s^\tau$. Write $s^\sigma m^- \in \downarrow\uparrow\mathcal{L}(\sigma)$ such that $\partial_\sigma(s^\sigma m^-) = s_A^\sigma a^-$, and write $\varphi(m^-) = n^-$. Then $\varphi(s^\sigma)n^- \in \downarrow\uparrow\mathcal{L}(\tau)$ displayed to $\varphi(s^\sigma)_A c^-$, and

$$ \varphi(s^\sigma)_A c^- \cong_A s_A^\sigma a^- \cong_A s_A^\tau b^-, $$

where $\varphi(s^\sigma) \cong_\tau s^\tau$, hence by $\sim$-receptivity of $\tau$ there must be a unique extension

$$ \varphi(s^\sigma)n^- \cong_\tau s^\tau p^-, $$

such that $\partial_\tau(s^\tau p^-) = s_A^\tau b^-$. Finally, $\leftarrow$-receptive is symmetric. $\square$

In particular, we obtain as a direct corollary:

**Corollary 11.2.6.** If $\sigma$: A is a sequential strategy, then $\downarrow\uparrow\text{-Plays}(\sigma)$ is an AJM strategy.
*Proof.* From Proposition 11.2.3 we lack uniformity, obvious from Lemma 11.2.5. ☐

However, our goal is to unfold to strategies in HO games rather than AJM games.

**Pointfixion of Alternating Plays** From a sequential causal strategy, we wish to obtain an alternating strategy in the sense of Chapter 3; but those play on *arenas* rather than *boards*. Hence the situation is exactly the same as in Section 9.2: it is unclear how to automatically obtain an arena in the sense of Chapter 3 from a board, hence we unfold sequential causal strategies playing on *mixed boards* in the sense of Definition 9.2.6 – comprising the data of the board, the arena, along with the link between the two.

As in Corollary 9.2.11 for the non-alternating case, we have:

**Proposition 11.2.7.** Consider A a mixed board. Then, ($\hat{\sim}$) restricts to bijections

$$ (\hat{\sim}) : \mathcal{I} \uparrow \text{-Plays}(!A) / \cong_A \approx \mathcal{I} \uparrow \text{-Plays}(\underline{A}), $$

$$ (\hat{\sim}) : \mathcal{I} \uparrow \text{-Plays}(A) / \cong_A \approx \mathcal{I} \uparrow \text{-Plays}_{\bullet}(\underline{A}), $$

preserving length and prefix.

*Proof.* Simply the restriction of Corollary 9.2.11 to alternating plays. ☐

Corollary 9.2.11 stated a similar bijection between $\mathcal{O}-\text{Plays}(!A)$ up to symmetry and $\text{pre-plays} \mathcal{O}-\text{PrePlays}(\underline{A})$. The mismatch with the above is because while this bijection does not account for any well-bracketing constraint, non-alternating plays with pointers were defined as always logically well-bracketed (Definition 5.1.3) whereas alternating plays have no such hardwired condition<fnref n="3" /> (Definition 3.1.4).

## 11.2.2 Alternating Unfoldings of Sequential Strategies

Now, we are in position to define the *alternating unfolding* of a sequential causal strategy. As for non-alternating strategies, we shall actually define three unfoldings:

(1) $\mathcal{I} \uparrow$-Unf. unfolds $\sigma : A$ to an alternating thread-strategy on $\underline{A}$,

(2) $\mathcal{I} \uparrow$-Unf$_{!}$ unfolds $\sigma : !A$ to an alternating strategy on $\underline{A}$,

(3) $\mathcal{I} \uparrow$-Unf unfolds $\sigma : !A \vdash B$ to an alternating strategy on $\underline{A} \Rightarrow \underline{B}$,

for all mixed boards A and B.

**Unfolding to a thread-strategy.** First, we define the pointed alternating unfolding of a sequential causal strategy on a mixed board A. The definition is essentially the same as Definition 9.2.12 for the non-alternating unfolding of causal strategies:

**Definition 11.2.8.** Consider A a mixed board, and $\sigma : A$ a sequential causal strategy. The unfolding of $\sigma$ is the set $\mathcal{I} \uparrow$-Unf$_{\bullet}(\sigma) = \{\hat{\circ}\}(s_A^\sigma) \in \mathcal{I} \uparrow \text{-Plays}(\underline{A}) | s^\sigma \in \mathcal{L}(\sigma)\}$.

<footnote n="3">³In general, we consider it better to impose conditions on strategies rather than on plays whenever possible, so as to not unnecessarily constrain the behaviour of the execution environment. But for non-alternating strategies we were brought to assume all plays to be logically well-bracketing, as the non-alternating strategies for basic IA$_{\parallel}$ primitives are hard to define rigourously otherwise: they have too many plays!</footnote>
We show that this is indeed a valid alternating thread-strategy. With respect to Proposition 9.2.13 in the non-alternating case, the difficulty is to prove determinism: this puts together (1) sequential determinism, (2) Proposition 11.2.7 ensuring that alternating plays with pointers on $\underline{A}$ exactly represent alternating plays on $A$ up to symmetry, and (3) Lemma 11.2.4 showing uniqueness of the witness in $\downarrow\uparrow-\mathcal{L}(\sigma)$ for a plays in $\downarrow\uparrow-\text{Plays}(\sigma)$, up to symmetry. Putting those together, we get the proposition:

**Proposition 11.2.9.** Consider $\sigma: A$ a causal strategy on mixed board $A$. Then, $\downarrow\uparrow-\text{Unf}_t(\sigma): \underline{A}$ is a P-visible thread-strategy in the sense of Definition 4.3.2.

*Proof.* It is a set of threads since $A$ is strict. Non-empty and prefix-closed are direct.

*Receptive:* consider $t = (\hat{\sigma})(s_A^\sigma)$ for $s^\sigma \in \downarrow\uparrow-\mathcal{L}(\sigma)$, with $tb^- \in \downarrow\uparrow-\text{Plays}_t(\underline{A})$. By Lemma 9.2.10, there is $s_A^\sigma a^- \in \mathcal{O}-\text{Plays}(\underline{A})$ such that $(\hat{\sigma})(s_A^\sigma a^-) = tb^-$; but by construction $s_A^\sigma a^-$ is alternating, thus in $\downarrow\uparrow-\text{Plays}(\underline{A})$. Now, by Proposition 11.2.3, there is $s^\sigma m \in \downarrow\uparrow-\mathcal{L}(\sigma)$ displaying to $s_A^\sigma a^-$, and *receptive* follows.

*Deterministic:* Consider $sa^-b_1^+$, $sa^-b_2^+ \in \downarrow\uparrow-\text{Unf}_t(\sigma)$, so there are $t^\sigma m^\sigma n^\sigma \in \downarrow\uparrow-\mathcal{L}(\sigma)$ and $u^\sigma c^\sigma d^\sigma \in \downarrow\uparrow-\mathcal{L}(\sigma)$ s.t. $sa^-b_1^+ = (\hat{\sigma})(t_A^\sigma m_A^\sigma n_A^\sigma)$ and $sa^-b_2^+ = (\hat{\sigma})(u_A^\sigma c_A^\sigma d_A^\sigma)$. Thus

$$t^\sigma m_A^\sigma n_A^\sigma \in \downarrow\uparrow-\text{Plays}(\sigma), \quad u^\sigma c_A^\sigma d_A^\sigma \in \downarrow\uparrow-\text{Plays}(\sigma),$$

with $(\hat{\sigma})(t_A^\sigma m_A^\sigma) = (\hat{\sigma})(u_A^\sigma c_A^\sigma) = sa^-$, which entails $t_A^\sigma m_A^\sigma \cong_A u_A^\sigma c_A^\sigma$ by Proposition 11.2.7. But then, by Lemma 11.2.4, we must actually have

$$t^\sigma m^\sigma \cong_A u^\sigma c^\sigma,$$

but hence by extension, there is $t^\sigma m^\sigma n^\sigma \cong_A u^\sigma c^\sigma e^\sigma$. But by sequential determinism for $\sigma$, this means $e^\sigma = d^\sigma$, so that $t^\sigma m^\sigma n^\sigma \cong_A u^\sigma c^\sigma d^\sigma$. Thus their display are also symmetric, so their pointifixion must be equal by Proposition 11.2.7.

*P-visible:* Straightforward by definition of sequential visibility. $\square$

**Unfolding to an alternating strategy.** Next, we show how to unfold a sequential causal strategy to a full alternating strategy – again the definition closely mimics the non-alternating case, more specifically Definition 9.2.14

**Definition 11.2.10.** Consider A a mixed board, and $\sigma: !A$ a sequential causal strategy. The unfolding of $\sigma$ is the set $\downarrow\uparrow-\text{Unf}_t(\sigma) = \{(\hat{\sigma})(s_A^\sigma) | s^\sigma \in \downarrow\uparrow-\mathcal{L}(\sigma)\}$.

This is a well-formed alternating strategy on arena $\underline{A}$:

**Proposition 11.2.11.** Consider A a mixed board and $\sigma: !A$ a sequential strategy. Then, $\downarrow\uparrow-\text{Unf}_t(\sigma): \underline{A}$ is a P-visible alternating strategy as in Definition 3.1.5.

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

As in the non-alternating case, if $\sigma: A$ is a sequential causal strategy, we may unfold it to a thread-strategy $\downarrow\uparrow-\text{Unf}_t(\sigma): \underline{A}$ and then obtain the corresponding single-threaded alternating strategy $\sigma^1$, or we may directly unfold its promotion as an alternating strategy with $\downarrow\uparrow-\text{Unf}_t(\sigma^1)$ – the two options coincide, as we show now.
**Lemma 11.2.12.** Consider sequential causal $\sigma: A$, and $\sigma^1: !A$ its promotion. Then, $(\downarrow\uparrow-\mathrm{Unf}_\bullet(\sigma))^1 = (\downarrow\uparrow-\mathrm{Unf}_1(\sigma^1))$.

*Proof.* $\subseteq$. We actually show by induction on $n$ that for all $s = s_1 \dots s_n \in (\downarrow\uparrow-\mathrm{Unf}_\bullet(\sigma))^1$, there is $t = t_1 \dots t_n \in \downarrow\uparrow-\mathcal{L}(\sigma^1)$ such that $s = (\stackrel{\wedge}{\circ})(t_!A)$ and for all prefix $s_1 \dots s_k$, writing

$$s_{\pi(1)} \dots s_{\pi(k)} = [s_1 \dots s_k]$$

the current thread of $s_1 \dots s_k$ for $\pi: \{1, \dots, p\} \to \{1, \dots, k\}$ some injection, we have $t_{\pi(1)}, \dots, t_{\pi(p)} \in \downarrow\uparrow-\mathcal{L}(\sigma)$ and $s_{\pi(1)} \dots s_{\pi(k)} = (\stackrel{\wedge}{\circ})(\partial_\sigma(t_{\pi(1)} \dots t_{\pi(p)}))$; the proof by induction is straightforward, relying on Lemma 9.2.10 and receptivity for negative extensions, on Lemma 11.2.4 and extension of isomorphism families for positive extensions.

$\supset$. Necessarily, any $sa^+ \in \downarrow\uparrow-\mathrm{Unf}_\bullet(\sigma^1)$ comes from some $tm^+ \in \downarrow\uparrow-\mathcal{L}(\sigma^1)$, where $m$ is in the component of $\sigma^1$ with copy index $i$. It is then straightforward that the moves of $tm^+$ with the same initial hereditary justifier as $m^+$ are exactly those events in copy index $i$, written $t'm^+ \in \downarrow\uparrow-\mathcal{L}(\sigma)$; and then we must have that

$$[sa^+] = [\stackrel{\wedge}{\circ}(\partial_\sigma'(tm^+))] = (\stackrel{\wedge}{\circ})(\partial_\sigma(t'm^+)) \in \downarrow\uparrow-\mathrm{Unf}_\bullet(\sigma)$$

as required, concluding the proof of the inclusion. $\square$

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

**Unfolding from mixed board A to mixed board B.** As in the non-alternating case, we finish with the definition of the unfolding of a sequential causal strategy from one mixed board to another – again this must deal with the fact that morphisms from A to B in $\to$-Seq are causal sequential strategies on $!A \vdash B$ (with at most one initial move) whereas morphisms in $\downarrow\uparrow$-Strat are alternating P-visible strategies on $A \Rightarrow B$, whose plays have arbitrarily many initial moves. Thus to deal with these differences, we set:

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

$$\downarrow\uparrow-\mathrm{Unf}(\sigma) = \downarrow\uparrow-\mathrm{Unf}_1(\Lambda(\sigma)^1) : A \Rightarrow B.$$

It is a consequence of Proposition 11.2.11 that this is well-defined:

**Proposition 11.2.14.** For any $\sigma \in \to$-Seq($A, B$), we have $\downarrow\uparrow-\mathrm{Unf}(\sigma) \in \downarrow\uparrow$-Strat($A, B$).

*Proof.* In complement to Proposition 11.2.11, it remains to prove that $\downarrow\uparrow-\mathrm{Unf}(\sigma)$ is single-threaded. But by Lemma 11.2.12, we have $\downarrow\uparrow-\mathrm{Unf}(\sigma) = \downarrow\uparrow-\mathrm{Unf}_\bullet(\Lambda(\sigma))^1$ which is single-threaded by Proposition 4.3.3; this concludes the proof. $\square$

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

### 11.2.3 Unfolding the Basic Categorical Structure

Next, we aim to show that the unfolding defined just above yields a $\sim$-functor

$$\downarrow\uparrow-\mathrm{Unf}(-) : \to$-Seq $\to$ \downarrow\uparrow$-Strat

which we will show preserves the interpretation of IA.
**Identities.** First, we show that unfolding preserves identities. Of course, one must keep in mind that $\rightarrow$-Seq is built on top of the Kleisli category $\mathbf{NTCG}_1$, so that the identity to be unfolded is actually dereliction $\mathbf{der}_A : !A \vdash A$.

**Proposition 11.2.15.** Consider A a mixed board. Then,

$$ \downarrow\uparrow-\mathrm{Unf}(\mathbf{der}_A) = \downarrow\uparrow-\mathbf{c}_A \in \downarrow\uparrow-\mathrm{Strat}(\underline{A}, \underline{A}). $$

*Proof.* By Lemma 11.2.12 and Proposition 4.3.4 it suffices to show the equality

$$ \downarrow\uparrow-\mathrm{Unf}_c(\Lambda(\mathbf{der}_A)) = \downarrow\uparrow-\mathbf{c}_A^*, $$

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

For $\sqsubseteq$, consider $s \in \downarrow\uparrow-\mathrm{Unf}_c(\Lambda(\mathbf{der}_A))$, meaning that $s = \hat{s}$ with $t = \partial_{\Lambda(\mathbf{der}_A)}(u)$ for some $u \in \downarrow\uparrow-\mathcal{L}(\mathbf{c}_A)$. Recalling that $|\mathbf{c}_A| = |A_1 \vdash A_2|$ with tags used for disambiguation, we observed in the proof of Lemma 11.1.6 that alternating linearizations on $\mathbf{c}_A$ are exactly those $v \in |A_1 \vdash A_2|^*$ such that for all event-length $w \sqsubseteq v$, we have $w \vdash A_1 = w \vdash A_2$. Now any even-length $s' \sqsubseteq s$ comes from $w \sqsubseteq u$ an even-length prefix of $u$ on which this observation applies, and it is direct that $s' \vdash A_1 = s' \vdash A_2$.

For $\sqsupseteq$, consider $s \in \downarrow\uparrow-\mathbf{c}_A^*$, assuming first that it has even length – hence $s \vdash A_1 = s \vdash A_2$. By Lemma 9.2.10, there is $t \in \downarrow\uparrow-\mathrm{Plays}(A)$ such that $\hat{t} = s \vdash A_1 = s \vdash A_2$. Interleaving two copies of $t$, it is straightforward to get $u \in \downarrow\uparrow-\mathrm{Plays}(A_1 \vdash A_2)$ such that $u \vdash A_1 = u \vdash A_2 = t$, and that for all even-length prefix $v \sqsubseteq u$, we have $v \vdash A_1 = v \vdash A_2$ as well, hence $u \in \downarrow\uparrow-\mathcal{L}(\mathbf{c}_A)$ – it is then a direct verification that writing $w = \partial_{\Lambda(\mathbf{der}_A)}(u)$, we have $\hat{w} = s$ as required. Finally, if $s$ has odd length, we use the above without the last move, and conclude by *receptivity* of $\downarrow\uparrow-\mathrm{Unf}_c(\mathbf{der}_A)$. $\square$

**Composition.** Here, the reasoning is pretty much the same as in the non-alternating case, except that plays and witnesses have to be ensured alternating – which follows easily from sequentiality. Thus we give fewer details than in the non-alternating case:

**Proposition 11.2.16.** Consider $\sigma \in \rightarrow$-Seq(A, B) and $\tau \in \rightarrow$-Seq(B, C). Then:

$$ \downarrow\uparrow-\mathrm{Unf}(\tau \circ_1 \sigma) = \downarrow\uparrow-\mathrm{Unf}(\tau) \circ \downarrow\uparrow-\mathrm{Unf}(\sigma) $$

*Proof.* First of all, we prove the inclusion

$$ \downarrow\uparrow-\mathrm{Unf}_c(\Lambda(\tau \odot \sigma')) \subseteq \downarrow\uparrow-\mathrm{Unf}(\tau) \odot \downarrow\uparrow-\mathrm{Unf}(\sigma), $$

this follows by the same reasoning as in Lemma 9.3.4, additionally observing by induction that the interaction we obtain is in $\downarrow\uparrow-\mathrm{Unf}(\sigma) \parallel \downarrow\uparrow-\mathrm{Unf}(\tau)$ (in the sense of Definition 4.1.7) exploiting that $\sigma$ and $\tau$ satisfy *reachable sequentiality* (Lemma 11.1.5).

Next, we show the following inclusion:

$$ \llbracket \downarrow\uparrow-\mathrm{Unf}(\tau) \odot \downarrow\uparrow-\mathrm{Unf}(\sigma) \rrbracket \subseteq \downarrow\uparrow-\mathrm{Unf}_c(\Lambda(\tau \odot \sigma')), $$

in this case this follows exactly as in 9.3.5, as the play for which we construct a witness in $\tau \odot \sigma'$ is by hypothesis alternating.

From these two inclusions, the desired equality follows as in Corollary 9.3.6. $\square$
Altogether, we have proved:

**Theorem 11.2.17.** *Unfolding yields a $\sim$-functor $\downarrow\uparrow$-Unf : $\dashv$-Seq $\rightarrow$ $\downarrow\uparrow$-Strat.*

*Proof.* The only thing remaining to check is that $\downarrow\uparrow$-Unf preserves equivalence, which is proved exactly as in Theorem 9.3.7. $\square$

### 11.2.4 Unfolding the Interpretation of IA

As in the non-alternating case, it is an immediate verification that the alternating unfolding preserves the cartesian closed structure: preservation of projections is a variation of Proposition 11.2.15, it is a simple verification that unfolding preserves currying and its inverse, so that evaluation is preserved as well – altogether we get

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

a cartesian closed $\sim$-functor. The unfolding is continuous with respect to the dcpo structure on hom-sets, so that the fixpoint operator is preserved. Finally, it follows by inspection that the unfolding preserves the interpretation of all IA primitives, so that:

**Theorem 11.2.18.** *We have a cartesian closed $\sim$-functor:*

$$ \downarrow\uparrow\text{-Unf}(-) : \dashv\text{-Seq} \rightarrow \downarrow\uparrow\text{-Strat,} $$

*preserving the interpretation in the sense that for $\Gamma \vdash M : A$ any term of IA, we have*

$$ \downarrow\uparrow\text{-Unf}(\llbracket M \rrbracket_{\dashv\text{-Seq}}) = \llbracket M \rrbracket_{\downarrow\uparrow\text{-Strat}}. $$

**Intensional full abstraction.** We motivated the unfolding

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

as a way to show that $\dashv\text{-Seq}$ is intensionally fully abstract for IA, i.e. to inherit in concurrent games the full abstraction result for IA in alternating game semantics (Theorem 3.3.5). However, full abstraction does not hold for $\downarrow\uparrow$-Strat but only with respect to *well-bracketed* P-visible alternating strategies, i.e. for $\downarrow\uparrow$-WB.

Strategies in $\dashv\text{-Seq}$ already embark two notions of well-bracketing: the winning mechanism implemented in NTCG (see Section 8.2) already bans call/cc, and we also imported logical well-bracketing from non-alternating games in Definition 9.3.2 – so we may hope that the unfolding actually lifts to a cartesian closed $\sim$-functor

$$ \downarrow\uparrow\text{-Unf}(-) : \dashv\text{-Seq} \rightarrow \downarrow\uparrow\text{-WB,} $$

but that is not the case: we showed in Figure 10.18 a sequential causal strategy whose alternating unfolding is not well-bracketed. The strategy is winning: its $\pm$-covered configurations have a positive payoff. Its non-alternating unfolding is logically well-bracketed (this matches the counter-example to the fact that logical well-bracketing implies well-bracketing, seen in Figure 5.3). Nevertheless, the play following the long causal chain is not well-bracketed as the final move does not answer the pending question. However this does not prevent the interpretation of IA in $\dashv\text{-Seq}$ to be intensionally fully abstract, because this phenomenon cannot occur in plays where the initial move has an answer.
**Lemma 11.2.19.** Let $s \in \mathcal{I}^\uparrow-\mathcal{P}\mathcal{A}\mathcal{Y}\mathcal{S}(\mathcal{A})$ be P- and O-visible. Assume that $s$ has the form

$$s = \dots s_i \cdots s_j \dots$$

where no further move points to $s_j$. Then, no move after $s_j$ can point within $s_i \dots s_j$.

*Proof.* By P- or O-visibility, $s_{j+1}$ points strictly before $s_i$. Then no view can ever see $s_{i+1} \dots s_j$ – so no move can point there. Besides, $s_i$ can only be seen by the player responsible for it, so no move can point to $s_i$.

A detailed proof appears in [Clairambault and Harmer, 2010, Lemma 5]. □

From this, we may easily deduce the following:

**Lemma 11.2.20.** Consider $s \in \mathcal{I}^\uparrow-\mathcal{P}\mathcal{A}\mathcal{Y}\mathcal{S}(\mathcal{A})$ O- and P-visible, and such that any Question has an answer. Then, $s$ is well-bracketed in the sense of Definition 3.2.5.

*Proof.* Assume $s$ has a well-bracketing failure, i.e. as in:

$$s = \dots q_1^Q \cdots q_2^Q \cdots a^A \dots$$

with $q_2$ unanswered when playing $a$. By *answer-closing*, no further move can point to $a$. Thus by Lemma 11.2.19, no further move can point to $q_2$ which must therefore remain unanswered, contradicting the hypothesis that every question has an answer. □

From all this, we may now conclude:

**Theorem 11.2.21.** *The interpretation of IA in $\rightarrow$-Seq is intensionally fully abstract.*

*Proof.* Let $\vdash M, N : A$ be terms in IA, and assume that $[[M]] \neq [[N]]$, i.e. there is a test $\alpha \in \rightarrow$-Seq($[[A]]$, $[[U]]$) such that $\alpha \circled_1 [[M]] \neq \alpha \circled_1 [[N]]$ – assume w.l.o.g. that $\alpha \circled_1 [[M]]$ converges while $\alpha \circled_1 [[M]]$ diverges. Writing $\alpha' = \mathcal{I}^\uparrow$-Unf($\alpha$), it follows that

$$\alpha' \circ [[M]]_{\mathcal{I}^\uparrow-\text{Strat}} \Downarrow \qquad \alpha' \circ [[N]]_{\mathcal{I}^\uparrow-\text{Strat}} \Uparrow,$$

since, by Theorem 11.2.18, the alternating unfolding preserves composition and the interpretation of IA. Here, $\alpha'$ is a P-visible alternating strategy, but because of the phenomena highlighted in Figure 10.18 it may not be well-bracketed as in Definition 3.2.6. Consider $s \in \alpha'$ involved in $\alpha' \circled_1 [[M]] \Downarrow$ – until the rest of the proof, $[[M]]$ is the interpretation in $\mathcal{I}^\uparrow$-Strat. The initial question of $s$ has an answer. Moreover, $[[M]]$ is the alternating restriction of $\mathcal{O}$-Unf($[[M]]_{\rightarrow}$-Strat) which is logically well-bracketed, and likewise $\alpha'$ is logically well-bracketed, thus $s$ is logically well-bracketed and hence all its questions are answered. It is P-visible and O-visible since both $[[M]]$ and $\alpha'$ are P-visible. Hence, by Lemma 11.2.20, it is well-bracketed as in Definition 3.2.6.

Consider $\alpha'$ restricted to prefixes of $s$. Now $\alpha'$ is well-bracketed as in Definition 3.2.5, and it distinguishes $[[M]]$ and $[[N]]$, hence $M \neq N$ by Theorem 4.3.11. □
So far we have seen that:

- $\rightarrow\text{-Strat}$ is intensionally fully abstract for $IA_\parallel$ (Theorem 9.3.10),

- $\rightarrow\text{-Seq}$ is intensionally fully abstract for $IA$ (Theorem 11.2.21).

It remains to prove two matching theorems in the presence of parallel innocence.

## 11.3 Sequential Innocence

In this section, we study the combination of sequentiality and parallel innocence, and establish links with traditional innocence as introduced in Section 3.2.

Let us start with the definition:

**Definition 11.3.1.** A causal strategy $\sigma: A$ is sequential innocent if it is both sequential (as in Definition 11.1.4) and parallel innocent (as in Definition 10.1.11).

As both sequential and parallel innocent causal strategies form a cartesian closed sub-~category of $\rightarrow\text{-Strat}$, there is a cartesian closed ~category $\rightarrow\text{-SeqInn}$ of sequential innocent strategies. As PCF may be interpreted in both $\rightarrow\text{-Seq}$ and $\rightarrow\text{-Inn}$, it follows that it has an adequate interpretation in $\rightarrow\text{-SeqInn}$ as well. In this section we shall prove that this interpretation is intensionally fully abstract, by proving that $\downarrow\text{-Strat}(\text{--})$ sends sequential innocent strategies to innocent alternating strategies as in Definition 3.2.9, and rely on Theorem 4.3.10 to deduce intensional full abstraction.

### 11.3.1 Causal Analysis of Sequential Innocence

**Basic causal shape.** So as to establish the link with traditional innocence, we first aim to understand better what constraints on the causal shape are brought by the combination of parallel innocence, and sequentiality. Roughly speaking, parallel innocence only allows Player to merge threads he spawned, whereas sequentiality prevents Player to spawn parallel threads: it follows that the causal shape of a sequential innocent strategy must be purely forestial, with branchings the entire responsibility of Opponent:

**Lemma 11.3.2.** Consider A a board, and $\sigma$: A a sequential, parallel innocent strategy. Then, $\sigma$ is an O-branching alternating forest.

*Proof.* First, we prove that for all $m \in \sigma$, its set of dependencies $[m]_\sigma$ is a total order.

Seeking a contradiction, take $m' \in \sigma$ minimal with $m' \rightarrow_{\sigma} m_1$ and $m' \rightarrow_{\sigma} m_2$ distinct, all within $[m]_\sigma$. By minimality, $[m']_\sigma$ is a total order, i.e. a gcc. By Lemma 6.1.16, $m_1$ and $m_2$ have the same polarity, opposite of $m'$. Consider $\rho_1 \in \text{gcc}(\sigma)$ a gcc for $m$ passing through $m' \rightarrow_{\sigma} m_1$, and $\rho_2 \in \text{gcc}(\sigma)$ a gcc for $m$ passing through $m' \rightarrow_{\sigma} m_2$. Then $\rho_1$ and $\rho_2$ have least distinct events $m_1$ and $m_2$; hence by pre-innocence $m_1$ and $m_2$ are positive. Now, $m'$ must be the only immediate dependency of $m_1$, and the only immediate dependency of $m_2$; indeed if there was $m'' \rightarrow_{\sigma} m_i$, then considering $\rho' \rightarrow m_i \in \text{gcc}(\sigma)$ passing through $m''$, $\rho$ and $\rho'$ would fork at some event smaller than
<figure><img src="image_203.png" /><figcaption>Figure 11.3: A sequential innocent causal strategy</figcaption></figure>

$m'$, contradicting its minimality. Hence, $[m'] \cup \{m_i\} \in \mathcal{C}(\sigma)$ for $i \in \{1, 2\}$.

Also writing $[m']$ for the linearization in $\downarrow\uparrow\mathcal{L}(\sigma)$ with events in the same order,

$$[m'], [m']m_1, [m']m_2 \in \mathcal{L}(\sigma),$$

but by Lemma 6.1.16, $[m']m_1^+$ and $[m']m_2^+$ are alternating. By sequential determinism of $\sigma$, it follows that $m_1 = m_2$, contradiction. So, for all $m \in \sigma$, $[m]_\sigma$ is a total order.

Thus $([\sigma], \leq_\sigma)$ is a forest. Likewise, if $m^- \to m_1^+$ and $m^- \to m_2^+$ in $\sigma$, by sequential determinism and the same reasoning as above, $m_1 = m_2$, so $\sigma$ is $\mathcal{O}$-branching. Finally, as for any causal strategy $\sigma: A$ on $A$ alternating, we have $\to_\sigma$ is alternating as well. $\square$

**Description.** The causal shape of a sequential innocent strategy is a forest, but it might not be obvious to the reader what this forest actually represents. Thus we start this discussion by looking at the interpretation as a causal strategy of the simple term

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

of pure PCF. The interpretation of this term yields the strategy in Figure 11.3.

This event structure is infinite, since Opponent may play any of his available moves an arbitrary number of times, using any natural number as copy index.

Intuitively, this diagram follows the structure of the term: once computation is initiated, Player asks for the output of $f$. Each time $f$ calls its argument, Player answers $\checkmark^+$. Note though that unlike in traditional game semantics, the strategy shows that these calls are causally independent from each other. Likewise, the game permits Opponent to have $f$ return multiple times. Each time this happens, this triggers another call to $f$, which may call its argument any number of times, and return any number of times.
<figure><img src="image_204.png" /><figcaption>Figure 11.4: Maximal P-views of $\lambda f. f \text{ skip;} f \text{ skip;} \text{ tt}$</figcaption></figure>

It seems clear from this diagram that the strategy contains a lot of redundant information: by symmetry, it intuitively suffices to know how the strategy behaves if Opponent performs each available action exactly once, say with copy index 0:

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

leading to what we shall call the *meager form* in general for parallel innocent strategies, in Section 12.1. Ignoring the copy indices we observe here that we have a tree with three maximal branches, which coincide with the three maximal P-views of the corresponding innocent alternating strategy in the traditional sense, as displayed in Figure 11.4. This plainly shows that P-views actually express the *causal* structures in traditional game semantics already, with however one main difference with respect to concurrent games: sets of P-views cannot express Opponent replications, so that composing them requires using plays, stepping out of the causal representation. In contrast, concurrent games remain causal also in the presence of Opponent replications.

**Recovering P-views.** Next we show that, as expected from the discussion above, the branches of a sequential innocent strategy do correspond to P-views.

**Proposition 11.3.3.** Consider A a mixed board, and $\sigma$: A sequential innocent.
For all $\rho \in \text{gcc}(\sigma)$, $(\sigma)(\partial_{\sigma}(\rho))$ is a P-view.

*Proof.* By Lemma 11.3.2, $\sigma$ is forestal, so that prefixes of $\rho$ are down-closed and inform configurations. Hence, we actually have $\rho \in \mathcal{L}(\sigma)$. Moreover, by Lemma
6.1.16, immediate causality alternates in $\sigma$ and in particular, $\rho \in \downarrow\uparrow\mathcal{L}(\sigma)$. In particular, $\partial_{\sigma}(\rho) \in \downarrow\uparrow\text{Plays}(A)$ and hence $(\stackrel{\rightarrow}{\sigma})(\partial_{\sigma}(\rho)) \in \downarrow\uparrow\text{Plays}(A)$.

To prove that it is a P-view, it remains to show that Opponent moves point to the previous move. But if we have $s = s_1 \dots s_i^+ s_{i+1}^- \dots = (\stackrel{\rightarrow}{\sigma})(\partial_{\sigma}(\rho))$, those must come from

$$ \rho = \rho_1 \rightarrow \sigma \dots \rightarrow \sigma \rho_i^+ \rightarrow \sigma \rho_{i+1}^- \rightarrow \sigma \dots, $$

then $\partial_{\sigma}(\rho_i^+) \rightarrow_A \partial_{\sigma}(\rho_{i+1}^-)$ by courtesy, which entails that $s_{i+1}^-$ points to $s_i^+$.

□

Thus indeed, we may regard a sequential innocent strategy as a presentation of an expanded version of the forest of P-views, with an explicit choice of copy indices.

## 11.3.2 The Unfolding Preserves Innocence

We now aim to show that the unfolding of a sequential innocent strategy is innocent in the sense of traditional Hyland-Ong game semantics, as introduced in Chapter 3.

**Alternating linearizations.** In order to prove that, our first step will be to study alternating linearizations of sequential innocent strategies, in particular understanding how the mechanism of P-views captures the causal structure.

Recall the *P-view* of an alternating linearization, introduced in Definition 11.1.3.

**Lemma 11.3.4.** *Consider $\sigma \in \text{NTCG}(A, B)$ sequential innocent.*

Then, for all $tm \in \downarrow\uparrow\mathcal{L}(\sigma)$, we have $\lceil tm \rceil = [m]_{\sigma}$.

*Proof.* Here we treat $[m]_{\sigma}$ as the sequence induced by its total ordering.

The crucial observation is that if $tm^{-}n^{+} \in \downarrow\uparrow\mathcal{L}(\sigma)$, then necessarily $m^{-} \rightarrow_{\sigma} n^{+}$. To prove that, we prove by induction that for any $t \in \downarrow\uparrow\mathcal{L}(\sigma)$: (1) if $t$ has even length, then all maximal events of $|t| \in \mathcal{C}(\sigma)$ are positive; and (2) if $t$ has odd length, then $|t| \in \mathcal{C}(\sigma)$ has exactly one maximal negative event. Indeed, for $tm^{-} \in \downarrow\uparrow\mathcal{L}(\sigma)$, then $t$ has even length, so $|tm^{-}|$ has all its maximal events positive. But then $|tm^{-}|$ has exactly one maximal negative event, namely $m^{-}$. Likewise, for $tm^{+} \in \downarrow\uparrow\mathcal{L}(\sigma)$, then $|t|$ has exactly one maximal negative event. Now, the immediate predecessor of $m$ must be negative. But if it is not maximal in $|t|$, this contradicts Lemma 11.3.2, and in particular that $\sigma$ is *O-branching*. Therefore, the predecessor of $m$ must be the unique maximal negative event of $|t|$, and $|tm|$ has all maximal events positive as required.

Now, if $tm^{-}n^{+}$, then $|tm^{-}|$ has exactly one maximal negative event (namely $m^{-}$); while the maximal events of $|tm^{-}n^{+}|$ are all positive (and comprise $n^{+}$). Hence, $m^{-} \rightarrow_{\sigma} n^{+}$ as required. Likewise, if $t_1m^{+}t_2n^{-} \in \downarrow\uparrow\mathcal{L}(\sigma)$ such that $j(n) = m$ so $\lceil t_1m_1t_2n_2 \rceil = \lceil t_1 \rceil \mathcal{M}n$ then we must have $\partial_{\sigma}(m) \rightarrow \partial_{\sigma}(n)$ hence $m \rightarrow_{\sigma} n$ by Lemma 6.1.16. From these two facts, the lemma is a direct verification by induction on $t$. □

We regard this as the fundamental reason why the mechanism of P-views works: on alternating linearizations, it recaptures exactly the causal structure explicitly carried by concurrent strategies – a strength of concurrent games is that beyond the alternating
<figure><img src="image_206.png" /><figcaption>Figure 11.5: Witness for Figure 9.19</figcaption></figure>

deterministic realm, P-views are no longer available while concurrent strategies remain.

As an illustration, Figure 11.5 shows the configuration explored in the play of

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

in Figure 9.19 (note that this is another presentation of the diagram on the left hand side of Figure 10.12) – the numbers in red correspond to the order in which the linearization proceeds. As proved above, at each stage the P-view is exactly the branch leading to the corresponding move in the configuration. Opponent could explore the same configuration in a different order, corresponding to a different play visiting the same P-views. On the other hand, only Opponent has any degree of freedom in this exploration: Player has ever at most one possible move, that immediately caused by the last Opponent move<fnref n="4" />.

**Innocence of the unfolding.** Now, we show that as expected, the alternating unfolding of a sequential innocent strategy is innocent in the traditional sense.

**Proposition 11.3.5.** Consider A a mixed board, and $\sigma$: A sequential innocent.
Then, $\downarrow\uparrow$-Unf$_1(\sigma^1)$: A is an innocent alternating strategy (as in Definition 3.2.9).

*Proof.* We already know from Proposition 11.2.11 that $\downarrow\uparrow$-Unf$_1(\sigma^1)$ is P-visible.

Consider $sa^-b^+, ta^- \in \downarrow\uparrow$-Unf$(\sigma^1)$ s.t. $\lceil sa^- \rceil = \lceil ta^- \rceil$. By definition, there are witnesses $umn \in \downarrow\uparrow$-$\mathcal{L}(\sigma^1)$ for $sa^-b^+$ and $vo \in \downarrow\uparrow$-$\mathcal{L}(\sigma^1)$ for $ta^-$. By Lemma 11.3.4,

$$ \lceil um \rceil = [m]_{\sigma^1}, \quad \lceil vo \rceil = [o]_{\sigma^1} $$

<footnote n="4">⁴Different explorations of the same configuration may be related by permuting contiguous OP pairs of moves. Deterministic innocent strategies may be defined as those stable under the permutations of OP pairs permitted by the arena: this is the idea behind Melliès' presentation of innocence [Melliès, 2004a].</footnote>
As both sequential and globular strategies form a cartesian closed sub-~-category of $\rightarrow$-Strat, there is a cartesian closed $\sim$-category $\rightarrow$-SeqGlob of sequential globular strategies. As PCF may be interpreted in both $\rightarrow$-Seq and $\rightarrow$-Glob, it follows that it has an adequate interpretation in $\rightarrow$-SeqGlob as well – here we shall prove that this interpretation is actually exactly the same as that in $\downarrow\uparrow$-InnWB.

We first show that the unfolding of a sequential globular strategy is well-bracketed:

**Proposition 11.3.9.** Consider A and B mixed boards, and $\sigma \in \rightarrow$-SeqGlob(A, B).
Then, $\downarrow\uparrow$-Unf($\sigma$) $\in$ $\downarrow\uparrow$-Inn(A, B) is well-bracketed (in the sense of Definition 3.2.6).

*Proof.* Recall that $\downarrow\uparrow$-Unf($\sigma$) is defined as $\downarrow\uparrow$-Unf$_1$(A($\sigma$))$^1$, which is innocent by Proposition 11.3.5. Moreover, by Proposition 11.3.6 its non-empty P-views are exactly the

$$s = (\stackrel{\sim}{\sigma})(\partial_{\sigma}([m]_{\sigma}))$$

for $m \in \sigma$. But by *wb-threads*, $[m]_{\sigma}$ is a well-bracketed gcc; it entails directly that $s$ is well-bracketed. Thus by Proposition 3.2.13, $\downarrow\uparrow$-Unf($\sigma$) is well-bracketed. $\square$

Together with Theorem 11.2.18, we get:

**Theorem 11.3.10.** The alternating unfolding yields

$$\downarrow\uparrow$-Unf($-$) : $\rightarrow$-SeqGlob $\rightarrow$ \downarrow\uparrow$-InnWB

a cartesian closed $\sim$-functor preserving the interpretation of PCF.

In fact, we shall be able to prove later on:

**Theorem 11.3.11.** The induced functor $\downarrow\uparrow$-Unf($-$) : $\rightarrow$-SeqGlob/$\approx$ $\rightarrow$ $\downarrow\uparrow$-InnWB is full and faithful: for all A, B mixed boards, the alternating unfolding induces a bijection

$$\downarrow\uparrow$-Unf($-$) : $\rightarrow$-SeqGlob(A, B)/$\approx$ $\simeq$ $\downarrow\uparrow$-InnWB(A, B).$$

*Proof.* This requires the notion of *meager form* of a parallel innocent causal strategy, introduced in Section 12.1.2 – hence, we postpone the proof until Section 12.1.3. $\square$

This should not surprise the reader: we have seen in Section 11.3.1 that the causal shape of a sequential innocent causal strategy is a forest, whose branches correspond to P-views enriched with explicit copy indices. Once we factor out the choice of copy indices via positive iso, we are left with exactly the same information as P-views.

### 11.3.4 Intensional Full Abstraction

At last, we are finally equipped to prove the final result of this chapter:

**Theorem 11.3.12.** The interpretation of PCF in $\rightarrow$-SeqGlob is *intens. fully abstract*.
*Proof.* Let $\vdash M, N : A$ be terms in PCF, and assume $[[M]] \not\subseteq [[N]]$, i.e. there is $\alpha \in \text{→-SeqGlob}([A], [[\cup]])$ s.t. $\alpha \circ_1 [[M]] \neq \alpha \circ_1 [[N]]$ – assume w.l.o.g. $\alpha \circ_1 [[M]]$ converges while $\alpha \circ_1 [[M]]$ diverges. Then it follows from Theorem 11.3.7 that

$$ \text{↓↑-Unf}(\alpha) \odot [[M]]_{\text{↓↑-Strat}} \text{↓} \qquad \text{↓↑-Unf}(\alpha) \odot [[N]]_{\text{↓↑-Strat}} \text{↑}, $$

where $\text{↓↑-Unf}(\alpha)$ is an innocent alternating strategy, but also well-bracketed by Theorem 11.3.10. Thus finally, it follows that $M \not\supseteq N$ by Theorem 4.3.10. $\square$

This leaves us with one, final theorem to prove in Part III: that the model $\text{→-Inn}$ of parallel innocent strategies is intensionally fully abstract for $\text{PCF}_\gamma$. This will prove the most challenging of our full abstraction results, investigated in the next chapter.

## 11.4 History and Related Work

Though it seemed clear for a long time that concurrent strategies supported a fitting notion of sequentiality, the constructions presented in this chapter were not worked out until the long paper [Castellan and Clairambault, 2021], with a few significant surprises in store. The presentation given here is slightly simpler.

**Related work.** Though the results of this chapter are new, the developments resonate significantly with several earlier works. First and foremost, the structure of sequential innocent strategies is close to the designs of Girard's *Ludics* [Girard, 2001], and part of our developments are reminiscent of Faggian and Hyland's work on the connection between Ludics and Hyland-Ong games [Faggian and Hyland, 2002]. Again, the causal shape of sequential innocent strategies was also noticed by Melliès: diagrams such as in Figure 11.3 are very syntactic in nature, and may be written down via terms of the *non-uniform $\lambda$-calculus* introduced in [Melliès, 2004a].

Another notable aspect of this chapter is the analysis of polarities necessary to prove sequentiality stable under composition and tensoring (see e.g. Lemmas 11.1.8 and 11.1.16). Such lemmas are fundamental structures of the theory of sequentiality. In traditional presentations of alternating strategies, they show up early when proving determinism stable under composition, and associativity (Chapter 4); here instead they show up when proving sequentiality stable under composition. Usually they are kept implicit, relegated to technical appendices (if anything); but they are at the foreground of Melliès' recent *template games* [Melliès, 2019a, Melliès, 2019b].
# Chapter 12

## Finite Definability for PCF$_{‖}$

We are approaching the end of the journey. Over the course of the previous three chap-
ters, we have established the following intensional full abstraction results

<table><tr><td>→-Strat</td><td>is fully abstract for</td><td>IA<sub>‖</sub>,</td></tr><tr><td>→-Strat + sequentiality</td><td>is fully abstract for</td><td>IA,</td></tr><tr><td>→-Strat + globularity + sequentiality</td><td>is fully abstract for</td><td>PCF,</td></tr></table>

and we are left with the one outstanding objective:

$$ \rightarrow\text{-Strat} + \text{globularity} \text{ is fully abstract for } \text{PCF}_{\parallel}. $$

This is also the most challenging of our full abstraction results: for the others we
could leverage earlier work, but here we must prove finite definability from scratch.

Proving finite definability for globular strategies is a technical endeavour, involving
a number of steps. First of all, what is “finite” in “finite definability”? Recall that this is
already subtle for traditional innocent strategies, where finiteness is defined with respect
to a *meager* representation: the forest of P-views (see Section 3.2.4). Accordingly, we
shall start in Section 12.1 by providing a compact, *meager* form for parallel innocent
strategies. Once this is done, we focus on the causal shape of globular strategies. There
our observation, is that parallel behaviour is inherently *first-order*: two threads whose
destiny is to be merged cannot delve into the higher-order structure. This allows us to
prove a *factorization* result: any globular strategy can be decomposed into (the inter-
pretation of) a pure $\lambda$-term, and a globular purely first-order strategy – this is detailed
in Section 12.2. Finally, it remains to show finite definability for first-order globular
strategies, which we do up to positional equivalence in Section 12.3.

Let us now delve in, starting with the *meager* form.
<figure><img src="image_207.png" /><figcaption>Figure 12.1: Meager form of a sequential innocent strategy on (U → U) → B</figcaption></figure>

**12.1 Meager Form**

Analogously to traditional innocent strategies, globular causal strategies support a notion of *meager form*, where all Opponent replications are factored out.

**Introducing the meager form** We have already seen in Section 11.3.1 the computation of the meager form for a sequential innocent strategy, summed up in Figure 12.1: so as to factor out Opponent’s duplications, it suffices to only keep those Opponent moves that have 0 as their copy index (it is actually not straightforward how to make this formal for arbitrary mixed boards, we shall see later on how to do that). In doing so, we get a useful notion of finite sequential innocent strategy: although the tree at the left hand side of Figure 12.1 is infinite, the strategy is finite because factoring out Opponent’s duplications yields the finite tree on the right hand side of Figure 12.1.

Then, the full strategy can be fully recovered from it: all the branches of the diagram on the left hand side of Figure 12.1 are copies of some branch of the meager form, and thus with each new Opponent copy of a move, we can make an independent copy of the subsequent subtree, choosing copy indices so as to avoid collisions. We shall see that the only information lost in going from left to right is the specific choice of copy indices, which however does not matter up to positive isomorphism.

This motivates the meager form and its expansion for sequential innocent strategies; but in this section we develop this in general for *parallel* innocent strategies. We show an example of the computation of the meager form of a parallel innocent strategy in Figure 12.2 – again we shall see that no essential information is lost. The diagram on the right hand side informs the full causal strategy: there is one copy of the final answer for each pair of answers to the two arguments, so that Opponent providing a new copy of the value for either argument prompts a new independent copy of the final answer.
<figure><img src="image_208.png" /><figcaption>Figure 12.2: Meager form of parallel composition</figcaption></figure>

12.1.1 Updating Mixed Boards

To make this formal, we need a way to specify the copy index of a move occurring deep
in the board; forcing us to complete the definition of mixed boards (Definition 9.2.6).

**Making copy indices explicit.** If $A$ is a board (and thus in particular, for a mixed board) its *causality* is forestial, thus any non-minimal event $a \in A$ has a unique **predecessor** for $\to_A$, written $\text{pred}(a) \to_A a$; by convention we also specify that $\text{pred}(a) = *$ if $a$ is a minimal event. With these conventions in place, we complete Definition 9.2.6 (the intention is that the definition of mixed board was that below from the start, but with some of the components postponed, as they played no role until now).

**Definition 12.1.1.** A mixed board is $(A, \underline{A})$ with $A$ a strict board, $\underline{A}$ an arena, with

$$
\mathrm{lbl}_A : |A| \to |\underline{A}|, \quad \mathrm{ind}_A : |A| \to \mathbb{N},
$$

with *lbl*<sub>*A*</sub> a *label* function preserving polarities, satisfying *Definition 9.2.6*, and *ind*<sub>*A*</sub> an
*indexing* function, with the following additional conditions:

initialized: for all $\underline{a} \in \min(\underline{A})$ there is a unique $a \in \min(A)$ s.t. $\text{lbl}(a) = \underline{a}$,
and it additionally satisfies $\text{ind}(a) = 0$.

local conflict: if $a \rightsquigarrow a'$, we have $\text{pred}(a) = \text{pred}(a')$ and $\text{ind}(a) = \text{ind}(a')$,

invariant conflict: if $a_1 \rightsquigarrow a_2$, $\text{lbl}(a_1) = \text{lbl}(b_1)$, $\text{lbl}(a_2) = \text{lbl}(b_2)$, $\text{pred}(b_1) = \text{pred}(b_2)$ and $\text{ind}(b_1) = \text{ind}(b_2)$, then $b_1 \rightsquigarrow b_2$.

jointly injective: for $a_1, a_2 \in A$, if $\text{lbl}(a_1) = \text{lbl}(a_2)$, $\text{ind}(a_1) = \text{ind}(a_2)$, and $\text{pred}(a_1) = \text{pred}(a_2)$, then $a_1 = a_2$.

wide: for any $a \in A$, $b \in \underline{A}$ such that $\text{lbl}(a) \to_{\underline{A}} b$, and $n \in \mathbb{N}$,
there is $b \in A$ s.t. $\text{pred}(b) = a$, $\text{lbl}(b) = \underline{b}$ and $\text{ind}(b) = n$.

+-transparent: for $\theta : x \cong_A y$, $\theta \in S_+(A)$ iff for all $a^- \in x$, $\text{ind}(\theta(a)) = \text{ind}(a)$.

-transparent: for $\theta : x \cong_A y$, $\theta \in S_-(A)$ iff for all $a^+ \in x$, $\text{ind}(\theta(a)) = \text{ind}(a)$.

In particular, the function ind<sub>A</sub> explicitly associates to every move *a* ∈ *A* of the board
a **copy index**. While this definition looks intimidating, its intention is simply to bind
<figure><img src="image_209.png" /><figcaption>Figure 12.3: Copy indices for ground(V)</figcaption></figure>

tightly the board and the arena so that events of the board are determined by their label in the arena, their predecessor in the board and their copy index. By *transparent*, the copy index is the only thing that symmetries can change. By +-transparent, positive symmetries can only change indices of positive moves, while by --transparent, negative symmetries can only change indices of negative moves.

Accounting for the new component ind<sub>A</sub> : |A| → N of mixed boards, we must now define the copy indices for all our mixed board constructions. For basic mixed boards, recall that they were obtained by linking the arenas for ground types with the ground strict boards obtained as ground(V) for some set V of values. Thus we must equip this with a copy index function: for a set of values V = {a, b, c, ...}, we define the copy indices for the ground board ground(V) (Definition 9.1.1) as specified in Figure 12.3. For all basic mixed boards, it is clear that Definition 12.1.1 is satisfied. We extend the copy index function to all constructions on mixed boards used in the interpretation, via:

$$
\begin{align*}
\mathrm{ind}_{A_1 \& A_2}(i, a) &= \mathrm{ind}_{A_i}(a) \\
\mathrm{ind}_{A \Rightarrow B}(2, b) &= \mathrm{ind}_{B}(b) \\
\mathrm{lbl}_{A \Rightarrow B}(1, (b, (i, a))) &= i \quad \text{if } a \in \min(A), \\
\mathrm{lbl}_{A \Rightarrow B}(1, (b, (i, a))) &= \mathrm{ind}_A(a) \quad \text{otherwise,}
\end{align*}
$$

for $B = \bigwedge_{i \in I} B_i$ with $B_i$ well-opened. We omit the routine verification that these defi-
nitions indeed preserve the conditions of Definition 12.1.1.

Introducing explicit copy indices only makes explicit a notion that we have already
referred to in the exposition; for instance in diagrams such as in Figure 11.5 where the
greyed-out subscripts are nothing but the numbers given by the copy index function. In
mixed boards, the board is essentially an expanded form of the arena, with all branches
replaced with countably many copies: playing a new move consists in picking a justifier
(if any), picking an enabled move in the arena, and picking a copy index<fnref n="1" />

**Properties.** Equipped with this now completed notion of mixed board, we may now prove the property that was postponed after Definition 9.2.6.

<footnote n="1">¹In fact, we could have set $\dashv$-Strat as having mere arenas as objects, and having strategies play on the generated board – this was the road suggested in [Castellan et al., 2019]. We prefer the present presentation, which allows for a smoother link with the relative Seely category structure of NTCG and the relational model.</footnote>
**Lemma 9.2.10.** Consider A a mixed board. We have the following properties:

(1) For all $ta \in \mathcal{O}-\text{PrePlays}_s(\underline{A})$, $s \in \mathcal{O}-\text{Plays}(A)$ such that $t = \mathcal{F}$, there is $sa' \in \mathcal{O}-\text{Plays}(A)$ such that $(\stackrel{\frown}{-})(sa') = ta$;

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

*Proof.* (1) Consider $ta \in \mathcal{O}-\text{PrePlays}_s(\underline{A})$ and $s \in \mathcal{O}-\text{Plays}(A)$ such that $t = \mathcal{F}$. If $t$ is empty, then $a$ is initial in $\underline{A}$ and the property follows by *initialized*. Otherwise, write

$$s = s_1 \dots s_n \qquad t = \mathcal{F} = t_1 \dots t_n$$

where $a$ points to $t_i$. Now, consider $p$ a copy index not yet appearing in $s$. By *wide*, there is $a' \in A$ such that $\text{lbl}(a') = a$, $\text{pred}(a') = s_i$ and $\text{ind}(a') = p$. Then $sa' \in \mathcal{L}(A)$. Indeed, $|s| \cup \{a'\} \in \mathcal{C}(A)$: it is down-closed as $\text{pred}(a') \in |s|$ and conflict-free by *locally conflicting* since no other move in $s$ has index $p$. Finally, $(\stackrel{\frown}{-})(sa') = ta$.

(2) same reasoning as for (1). □

## 12.1.2 Meager Innocent Strategies

Now, we are equipped to define *meager parallel innocent strategies*, the notion analogous to the *meager innocent strategies* in the traditional setting (see Section 3.2.4).

**Definition.** In analogy to the traditional case, *meager innocent strategies* are supposed to be parallel innocent strategies, but playing on games not allowing any Opponent replications. We formalize this by restricting Opponent to copy index 0:

**Definition 12.1.2.** Consider A a mixed board. Then, we set $A_+$ a strict board with

$$|A_+| = \{a' \in |A| \mid \forall a^- \leq_A a', \text{ind}_A(a) = 0\},$$

and all other components inherited. We call $A_+$ the **positive restriction** of A.

This definition of the positive restriction has the immediate consequence that its only non-trivial symmetries are positive, since Opponent moves must have index 0:

**Lemma 12.1.3.** For A a mixed board, if $\theta \in \mathcal{S}(A_+)$ then $\theta \in \mathcal{S}_+(A_+) \subseteq \mathcal{S}_+(A)$.

This is obvious by +-transparent. We now define meager parallel innocent strategies:

**Definition 12.1.4.** Consider A a mixed board.

*A meager parallel innocent strategy on A is a parallel innocent strategy on $A_+$.*

For instance, the diagrams on the right hand side of Figures 12.1 and 12.2 are meager parallel innocent strategies. Note that on the left hand side of these diagrams, the infinite nature of the strategies forces us to resort to a symbolic notation so as to describe those finitely; also the notation conveys no information on the symmetries, although those are in principle part of the data. In contrast, for meager parallel innocent strategies:
**Proposition 12.1.5.** Consider A a mixed board, and $\sigma : A_+$ meager parallel innocent.
Then its symmetries are trivial, i.e. $\mathcal{S}(\sigma) = \{\mathrm{id}_x : x \cong_{\sigma} x \mid x \in \mathcal{C}(\sigma)\}$.

*Proof.* Consider $\theta : x \cong_{\sigma} y$ any symmetry. By Lemma 12.1.3, $\partial_{\sigma} \theta \in \mathcal{S}_+(A_+)$. Hence by *thin*, we have that $x = y$ and $\theta = \mathrm{id}_x$; thus $\mathcal{S}(\sigma)$ is restricted to identities. $\square$

Thus when specifying a meager parallel innocent strategy $\sigma$, it is unnecessary to specify the isomorphism family $\mathcal{S}(\sigma)$, which is trivial. Thus it is entirely sufficient to describe $\sigma$ with a diagram (as on the right hand side of Figures 12.1 and 12.2) describing the event structure concretely, with no ellipse or symbolic representation. Likewise, a *positive iso* between meager parallel innocent strategies boils down to an isomorphism

$$ \varphi : \sigma \cong \tau $$

of plain event structures such that $\partial_{\tau} \circ \varphi \sim \partial_{\sigma}$, which amounts to renaming the internal events of $\sigma$ and $\tau$ and changing the copy indices of positive moves.

**Meager form.** The above is interesting, *provided* it does indeed give an alternative but equivalent representation for usual parallel innocent strategies. Accordingly, we now define the *meager form* of parallel innocent strategies – in the obvious way:

**Proposition 12.1.6.** Consider A a mixed board, and $\sigma : A$ a parallel innocent strategy.
Then, setting the set of events

$$ |\mathrm{mf}(\sigma)| = \{m \in |\sigma| \mid \partial_{\sigma}[m]_{\sigma} \in \mathcal{C}(A_+)\} $$

with all components inherited yields a meager parallel innocent strategy $\mathrm{mf}(\sigma)$ on A.
Moreover, $\mathrm{mf}(-)$ preserves $\approx$.

*Proof.* There are a few conditions to check, which we list below.

*Event structure with symmetry.* It is easy that $\mathrm{mf}(\sigma)$ is an event structure. For symmetry only the *extension* axiom is non-trivial: if $\theta : x \cong_{\sigma} y$ with $x, y \in \mathcal{C}(\mathrm{mf}(\sigma))$, then by the same reasoning as in Proposition 12.1.5, $\theta = \mathrm{id}_x$; *extension* follows.

*Strategy, winning, visible, parallel innocent.* Immediate verifications.

*Preservation of $\approx$.* Consider $\varphi : \sigma \approx \tau$ a positive isomorphism. Then, the important observation is that $\varphi$ sends $\mathrm{mf}(\sigma)$ to $\mathrm{mf}(\tau)$. Indeed if $m \in \mathrm{mf}(\sigma)$, then

$$ \langle \partial_{\sigma}, \partial_{\tau} \circ \varphi \rangle_{[m]_{\sigma}} : \partial_{\sigma}[m]_{\sigma} \cong_{A}^{+} \partial_{\tau}[\varphi(m)]_{\tau} $$

which by *+transparent*, being positive, must preserve the copy indices of negative events. Hence $\partial_{\tau}[\varphi(m)]_{\tau} \in \mathcal{C}(A_+)$, and $\varphi$ restricts to $\mathrm{mf}(\varphi) : \mathrm{mf}(\sigma) \approx \mathrm{mf}(\tau)$. $\square$

Note that in the construction of $\mathrm{mf}(\sigma)$ we have never actually used the hypothesis that $\sigma$ is parallel innocent, and the construction works in more generality. However, the operation is not very interesting for non-innocent strategies as it is lossy: if $\sigma$ is not parallel innocent, one cannot in general reconstruct $\sigma$ from $\mathrm{mf}(\sigma)$.

Next, we show how to recover a parallel innocent strategy from a meager form.
<figure><img src="image_210.png" /><figcaption>Figure 12.4: Expansion of meager parallel composition</figcaption></figure>

**Expansion of a meager parallel innocent strategy.** Fix A a mixed board, and $\sigma$: $A_+$ meager parallel innocent on A. We must infer from $\sigma$ its behaviour if Opponent performs arbitrary duplications, by performing adequately many copies of its events. We shall achieve that by pairing each event of a meager parallel innocent strategy with the choice of a copy index for each of its duplicable Opponent dependencies, i.e. its negative dependencies save for the initial move – we call such choice an exponential slice. We must then assign a new copy index for positive moves, hashing together the positive move and the exponential slice. The process is displayed in Figure 12.4.

Consider $m \in \sigma$. How many copies of $m$ should we include in the expanded form? The answer is that there should be one copy for each simultaneous choice of a copy index for each duplicable negative dependency of $m$. Write

$$[m]_{\sigma}^{-} = \{n^{-} \in |\sigma| \mid n^{-} \leq_{\sigma} m\}$$

for the **negative dependencies** of $m$. Then, we define:

**Definition 12.1.7.** An exponential slice for $\sigma$ is a function, for some $m \in \sigma$,

$$\alpha : [m]_{\sigma}^{-} \to \mathbb{N}.$$

such that $\alpha(n) = 0$ for $n$ minimal.

An **expanded event** is $m = (m, \alpha_m : [m]_\sigma^- \to \mathbb{N})$, we write $m = (m, \alpha) \in \exp(\sigma)$.

We write $lbl((m, \alpha)) = m$. If $lbl(m)$ is negative we say that $m$ is **negative**, and write $ind((m, \alpha)) = \alpha(m)$ for its **copy index**. For $m = (m, \alpha)$, $n = (n, \beta) \in \exp(\sigma)$, we write $m \sqsubseteq n$ iff $m \leq_{\sigma} n$, and for all $e^{-} \leq_{\sigma} m$, we have $\alpha(e^{-}) = \beta(e^{-})$. Note that if $m$ is negative, as $lbl(m)$ has a unique predecessor in $\sigma$, $m$ must have a unique predecessor in $\exp(\sigma)$, written $pred(m)$. We set the *minimal conflict* $m \sim_{\exp(\sigma)} n$ iff $m$ and $n$ are negative, $pred(m) = pred(n)$, $lbl(m) \sim_{\sigma} label(n)$ and $ind(m) = ind(n)$.

Towards defining a strategy, we first extend this to an event structure with symmetry:
**Proposition 12.1.8.** Consider $\exp(\sigma)$ with events $|\exp(\sigma)|$, components

$$ m \leq_{\exp(\sigma)} n \Leftrightarrow m \sqsubseteq n \\ m \#_{\exp(\sigma)} n \Leftrightarrow \exists m' \sqsubseteq m, n' \sqsubseteq n, m' \sim_{\exp(\sigma)} n' $$

and $\mathcal{S}(\exp(\sigma))$ comprising all order-isos preserving $lbl(-)$ between configurations.
Then, $\exp(\sigma)$ is an event structure with symmetry.

*Proof.* The less trivial point is that $\#_{\exp(\sigma)}$ is irreflexive so assume $m \#_{\exp(\sigma)} m$, meaning there are $n, o \sqsubseteq m$ such that $n \sim_{\exp(\sigma)} o$. So $\text{pred}(n) = \text{pred}(o) = p$, $\text{lbl}(n) \sim_{\sigma} \text{lbl}(o)$, and $\text{ind}(n) = \text{ind}(o)$. But this means we have $\text{lbl}(n) \le_{\sigma} \text{lbl}(m)$ and $\text{lbl}(o) \le_{\sigma} \text{lbl}(m)$ with $\text{lbl}(n) \sim_{\sigma} \text{lbl}(o)$, thus $\text{lbl}(m) \#_{\sigma} \text{lbl}(m)$, contradiction since $\sigma$ is an event structure.

*Event structure with symmetry.* The non-trivial point is the extension axiom. Consider $\theta: x \cong_{\exp(\sigma)} y$, and $x \vdash_{\exp(\sigma)} (m, \alpha)$. If $m$ is positive, then for each $n^- \le_{\sigma} m$, we have $(n^-, \alpha \uparrow [n^-]^-_{\sigma}) \in x$, and we write $\theta((n^-, \alpha \uparrow [n^-]^-_{\sigma})) = (n^-, \beta_n)$. Then we set:

$$ \gamma(n^-) = \beta_n(n^-) $$

for all $n^- \le_{\sigma} m$, yielding $(m, \gamma) \in \exp(\sigma)$. Then, we observe that $y \vdash_{\exp(\sigma)} (m, \gamma)$: indeed if $(p, \gamma') \le_{\exp(\sigma)} (m, \gamma)$ then one can prove that $\theta((p, \alpha')) = (p, \gamma')$ for $\alpha' = \alpha \uparrow [p]^-_{\sigma}$. Moreover, $y \cup \{(m, \gamma)\}$ is consistent as immediate conflicts are negative. Likewise $\theta \vdash ((m, \alpha), (m, \gamma))$ by definition of $\mathcal{S}(\exp(\sigma))$. Finally if $m$ is negative, then write $(n, \beta) = \text{pred}(m, \alpha)$ and $(n, \beta') = \theta(n, \beta)$. Set $\alpha' : [m]_{\sigma} \to \mathbb{N}$ as $\alpha'(o) = \beta(o)$ for $o <_{\sigma} m$, and $\alpha'(m) = i$ fresh; then it is straightforward that $\theta \vdash ((m, \alpha), (m, \alpha'))$. $\square$

Now, in order to obtain a strategy, we must specify its display map. In particular, we must set a copy index for all moves. For negative moves, it should clearly match that given by the exponential slice. For positive moves, we choose arbitrarily

$$ \# : \sum_{m^+ \in |\sigma|} \mathbb{N}^{[m^+]^-} \to \mathbb{N} $$

any injective function, which we shall use to fix a copy index for positive moves – note that the strategy obtained will not depend (up to positive iso) on this choice.

In order to better formulate the definition, we shall use the lemma:

**Lemma 12.1.9.** Consider $a \in A$ non-minimal, and write $\text{pred}(a) = b$ its predecessor.
Then for all $b \in A$ such that $\text{lbl}(b) = b$, and $n \in \mathbb{N}$, there is a unique $a \in A$ such that $\text{lbl}(a) = a$, $\text{pred}(a) = b$ and $\text{ind}(a) = n$.

*Proof.* Direct consequence of *wide* and *jointly injective* of mixed boards. $\square$

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

Notice also that each non-minimal $m \in \exp(\sigma)$ has a natural notion of **justifier**: for $m = (m, \alpha)$, we set $j(m) = (j(m), \alpha \uparrow [j(m)]^-_{\sigma})$ – we make use of this below:
**Lemma 12.1.10.** The function defined by induction on $\leq_{\sigma}$ via the clauses

$$
\begin{array}{l@{\qquad}l}
\partial_{\exp(\sigma)}(m^{-}, \alpha) = a^{-} & \text{such that} \\
\left\{
\begin{array}{@{}l@{}}
\text{pred}(a^{-}) = \partial_{\exp(\sigma)}(j(m^{-}, \alpha)) \\
\text{lbl}(a^{-}) = \text{lbl}(\partial_{\sigma}(m^{-})) \\
\text{ind}(a^{-}) = \alpha(m^{-})
\end{array}
\right. \\
\\
\partial_{\exp(\sigma)}(m^{+}, \alpha) = a^{+} & \text{such that} \\
\left\{
\begin{array}{@{}l@{}}
\text{pred}(a^{+}) = \partial_{\exp(\sigma)}(j(m^{+}, \alpha)) \\
\text{lbl}(a^{+}) = \text{lbl}(\partial_{\sigma}(m^{+})) \\
\text{ind}(a^{+}) = \#(m^{+}, \alpha)
\end{array}
\right.
\end{array}
$$

is a map of event structures with symmetry $\partial_{\exp(\sigma)} : \exp(\sigma) \to A$.

*Proof.* It is clear by construction that the image of a configuration is down-closed, and it is easily verified that $\partial_{\exp(\sigma)}$ is locally injective. Now considering $x \in \mathscr{C}(\exp(\sigma))$, we must show that $\partial_{\exp(\sigma)}(x)$ is conflict-free. Seeking a contradiction, assume there are $m = (m^{-}, \alpha)$ and $n = (n^{-}, \beta)$ s.t. $\partial_{\exp(\sigma)}(m) \rightsquigarrow_{\exp(\sigma)} \partial_{\exp(\sigma)}(n)$. By definition of $\partial_{\exp(\sigma)}$, $\text{lbl}(\partial_{\sigma}(m^{-})) = \text{lbl}(\partial_{\exp(\sigma)}(m))$ and $\text{lbl}(\partial_{\sigma}(n^{-})) = \text{lbl}(\partial_{\exp(\sigma)}(n))$. By local conflict, $\partial_{\exp(\sigma)}(m)$ and $\partial_{\exp(\sigma)}(n)$ must have the same predecessor, so $j(m^{-}, \alpha)$ and $j(n^{-}, \beta)$ have the same display. But they are compatible, thus by local injectivity they must be equal – in turn this entails that $\text{pred}(m^{-}) = \text{pred}(n^{-})$, thus $\text{pred}(\partial_{\sigma}(m^{-})) = \text{pred}(\partial_{\sigma}(n^{-}))$ by courtesy. Thus by invariant conflict, we have $\partial_{\sigma}(m^{-}) \rightsquigarrow_{\sigma} \partial_{\sigma}(n^{-})$ which entails $m^{-} \rightsquigarrow_{\sigma} n^{-}$. Summing up, $\text{lbl}(m) \rightsquigarrow_{\sigma} \text{lbl}(n)$, $\text{ind}(m) = \text{ind}(n)$ since $\text{ind}(\partial_{\exp(\sigma)}(m)) = \text{ind}(\partial_{\exp(\sigma)}(n))$ by local conflict, and $\text{pred}(m) = \text{pred}(n)$, thus $m \rightsquigarrow_{\exp(\sigma)} n$.

Finally if $\theta \in \mathcal{S}(\exp(\sigma))$, it is by definition an order-isomorphism preserving labels. From that it is obvious that it must preserve justifiers. It follows from the definition that $\partial_{\exp(\sigma)} \theta$ is an order-isopererving labels, hence a symmetry by *transparent*. $\square$

There is still a lot of work to do in order to obtain a causal strategy; first we must
construct a strategy in the sense of Definition 6.1.6. But in order to prove properties
based on configurations (starting with *receptive*), we must understand better how con-
figurations of $\exp(\sigma)$ relate to configurations of $\sigma$. We shall establish such a connection
not in general, but in the particular case of so-called *linear* configurations:

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

Then, $x \in \mathscr{C}(\boldsymbol{\sigma})$ is **linear** if for all $n_1^-, n_2^- \in x$, if $\text{pred}(n_1^-) = \text{pred}(n_2^-)$ then $n_1^- = n_2^-$.

Linear configurations are analogous to P-views: Opponent may point on any given
Player move at most once. Their interest comes from the following observation:

**Lemma 12.1.12.** If $\boldsymbol{\sigma} : A$ is parallel innocent and $m \in \boldsymbol{\sigma}$, $[m]_{\boldsymbol{\sigma}} \in \mathscr{C}(\boldsymbol{\sigma})$ is linear.

If $\boldsymbol{\sigma} : A$ is a meager parallel innocent and $m \in \exp(\boldsymbol{\sigma})$, then $[m]_{\exp(\boldsymbol{\sigma})}$ is linear.

*Proof.* The first is a direct consequence of pre-innocence (and Lemma 6.1.16); the second is straightforward from the definition, boiling down to the pre-innocence of $\boldsymbol{\sigma}$. $\square$

Next, we observe that if $\boldsymbol{\sigma} : A$ is a meager parallel innocent strategy, any linear configuration $x \in \mathscr{C}(\boldsymbol{\sigma})$ may be canonically regarded as a (linear) configuration of $\exp(\boldsymbol{\sigma})$ by adjoining the constant $0$ copy index to all Opponent moves:
**Lemma 12.1.13.** Consider A a mixed board, and $\sigma$: A meager parallel innocent.
For each linear $x \in \mathscr{C}(\sigma)$, with $0_m : [m]_\sigma^- \to \mathbb{N}$ the constant $0$ function, setting

$$ \exp(x) = \{(m, 0_m) \mid m \in x\}, $$

we get $\exp(x) \in \mathscr{C}(\exp(\sigma))$ a linear configuration; and $\kappa_x : m \mapsto (m, 0_m)$ is an order-isomorphism $\kappa_x : x \cong \exp(x)$ compatible with display maps, i.e. $\partial_{\exp(\sigma)} \circ \kappa_x \sim^{+} \partial_\sigma$.

*Proof.* Straightforward, since meager parallel innocent strategies play on $A_+$. $\square$

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

It is also straightforward that $\kappa_x$ preserves and reflects symmetry. Reciprocally, all linear configurations of $\exp(\sigma)$ are canonically symmetric to a configuration of $\sigma$:

**Lemma 12.1.14.** Consider A a mixed board, meager $\sigma$: A, and $x \in \mathscr{C}(\exp(\sigma))$ linear.
There are unique $\mathrm{mf}(x) \in \mathscr{C}(\sigma)$ and $\theta_x : x \cong_{\exp(\sigma)} \exp(\mathrm{mf}(x))$, given by

$$ \mathrm{mf}(x) = \{m \mid (m, \alpha) \in x\}, \quad \theta_x = \{((m, \alpha), (m, 0_m)) \mid (m, \alpha) \in x\}. $$

*Proof. Existence.* We prove that this data satisfies the required conditions by induction on $x$. For $x$ empty this is clear. If $x \vdash (m^-, \alpha)$, then by induction hypothesis, $\mathrm{mf}(x) \in \mathscr{C}(\sigma)$. It is immediate that $\mathrm{mf}(x) \cup \{m^-\}$ is down-closed. If it was conflicting, then there would be $n^- \in \mathrm{mf}(x)$ such that $m^- \not\sim_{\sigma} n^-$. But then, by Lemma 6.1.17, we have $\partial_{\sigma}(m^-) \not\sim_A \partial_{\sigma}(n^-)$, which by local conflict entails $\mathrm{pred}(\partial_{\sigma}(m^-)) = \mathrm{pred}(\partial_{\sigma}(n^-))$, hence $\mathrm{pred}(m^-) = \mathrm{pred}(n^-)$ by Lemma 6.1.16. Writing $p^+ \in \sigma$ for this predecessor,

$$ (p^+, \alpha') \dashv_{\exp(\sigma)} (m^-, \alpha), \quad (p^+, \beta') \dashv_{\exp(\sigma)} (n^-, \beta) $$

with all four events in $x \cup \{(m^-, \alpha)\}$ linear. If $\alpha' = \beta'$ we get $(m^-, \alpha) = (n^-, \beta)$ by linearity hence $m^- = n^-$, contradiction. Otherwise $(p^+, \alpha')$, $(p^+, \beta') \in x$ differ, but this directly entails a failure of linearity as well – contradiction. Now if $x \vdash (m^+, \alpha)$, as above $\mathrm{mf}(x) \cup \{m^+\}$ is down-closed. It must also be conflict-free, since by causal determinism, minimal conflicts in $\sigma$ are negative. It is direct to check that $\xi_x : x \cong \mathrm{mf}(x)$ sending $(m, \alpha)$ to $m$ is an order-isomorphism and that $\theta_x = \kappa_{\mathrm{mf}(x)} \circ \xi_x$ is an order-is preserving labels, hence a symmetry in $\exp(\sigma)$ as required.

*Uniqueness.* Assume we have $y \in \mathscr{C}(\sigma)$ and $\theta'_x : x \cong_{\exp(\sigma)} \exp(y)$. Then,

$$ \theta'_x \circ \theta_x^{-1} : \exp(\mathrm{mf}(x)) \cong_{\exp(\sigma)} \exp(y) $$

which entails $\exp(\mathrm{mf}(x)) = \exp(y)$ (so that $\mathrm{mf}(x) = y$) and $\theta'_x \circ \theta_x^{-1}$ is an identity by definition of symmetries in $\exp(\sigma)$; this concludes the proof. $\square$

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

Now, we may finally prove:

**Proposition 12.1.15.** Consider A a mixed board, and $\sigma$: A meager parallel innocent.
Then, $\exp(\sigma)$ with the components above is a parallel innocent strategy.
*Proof. Receptive.* Consider $x \in \mathscr{C}(\exp(\sigma))$ and $\partial_{\exp(\sigma)} x \vdash_A a^-$. Call $c^+ \in \partial_{\exp(\sigma)} x$ the predecessor of $a^-$ in $x$ – there is a unique $m = (m, \alpha) \in x$ such that $\partial_{\exp(\sigma)} m = c^+$. By Lemma 12.1.12, $[m]_{\exp(\sigma)}$ is linear, and thus by Lemma 12.1.14 there is

$$ \theta_x : [(m, \alpha)]_{\exp(\sigma)} \cong_{\exp(\sigma)} [(m, 0_m)]_{\exp(\sigma)}, $$

mapping via $\partial_{\exp(\sigma)}$ to a symmetry in $A$ which must extend by some $(a^-, b^-)$. By *wide*, we may assume that $\mathrm{ind}(b^-) = 0$ so that the extension is in $A_+$. By Lemma 12.1.13 and receptivity of $\sigma$, there is a unique $[m]_\sigma \vdash_\sigma n^-$ such that $\partial_\sigma(n^-) = b^-$. Extending $\alpha$ to $\alpha' : [n^-]_\sigma^- \to \mathbb{N}$ with $\alpha'(n^-) = \mathrm{ind}(a^-)$, by *jointly injective* we get the required extension – it is compatible with $x$ by definition of minimal conflict.

~receptive~ is similar, and all further conditions are straightforward. $\square$

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

This at last concludes the construction of $\exp(\sigma)$ as a parallel innocent strategy.

**Equivalence of meager and expanded forms.** Finally, so as to show that meager parallel innocent strategies provide an equivalent representation of parallel innocent strategies, we must prove that the two constructions $\mathrm{mf}(-)$ and $\exp(-)$ preserve positive isomorphisms, and are inverses up to positive isomorphism.

**Proposition 12.1.16.** The constructions $\mathrm{mf}(-)$ and $\exp(-)$ preserve positive isos.

*Proof.* It is obvious that $\mathrm{mf}(-)$ preserves positive isomorphisms. Consider $\varphi : \sigma \approx \tau$ a positive iso between meager parallel innocent strategies on $A$; we must construct

$$ \exp(\varphi) : \exp(\sigma) \approx \exp(\tau) $$

a positive isomorphism between the expansions. We simply set:

$$ \begin{array}{rcl} \exp(\varphi) & : & \exp(\sigma) \approx \exp(\tau) \\ (m, \alpha) & \mapsto & (\varphi(m), \alpha') \end{array} $$

where for $\varphi(n)^- \le_\tau \varphi(m)$, $\alpha'(\varphi(n)) = \alpha(n)$. It is direct that this is an order-iso; it preserves and reflects immediate conflict by *causal determinism* and *invariant conflict*. For positivity, for all $(m, \alpha) \in \exp(\sigma)$, $\exp(\varphi)$ on $[(m, \alpha)]_{\exp(\sigma)}$ factors as

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

omitting subscripts for readability – where every triangle commutes up to symmetry via Lemmas 12.1.13 and 12.1.14, and positivity follows by +-transparent. $\square$

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

It remains to show that $\mathrm{mf}(-)$ and $\exp(-)$ are inverses up to positive iso. We start with the easy direction, that a meager strategy can be recovered from its expansion:
**Proposition 12.1.17.** Consider $\sigma : A$ meager parallel innocent. Then, the function

$$ \Phi : \sigma \to \mathrm{mf}(\exp(\sigma)) \\ m \mapsto (m, 0_m), $$

yields a positive isomorphism $\Phi : \sigma \approx \mathrm{mf}(\exp(\sigma))$.

*Proof.* We omit the direct verification that this is an isomorphism of ess. Positivity follows from Lemma 12.1.13 on prime configurations, extended by taking unions. $\square$

Finally we must show that analogously, a full parallel innocent strategy can always be recovered from its meager form. This means that given a parallel innocent strategy $\sigma : A$, we must provide a bijection between events of $\sigma$ and of $\exp(\mathrm{mf}(\sigma))$, hence extract from any $m \in \sigma$ a label in $\mathrm{mf}(\sigma)$ and an exponential slice.

We start by the following generalization of Lemma 12.1.14:

**Lemma 12.1.18.** Consider A a mixed board, and $\sigma : A$ a parallel innocent strategy.

For $x \in \mathscr{C}(\sigma)$ linear, there are unique $\mathrm{mf}(x) \in \mathscr{C}(\mathrm{mf}(\sigma))$ and $\theta_x : x \cong_{\sigma} \mathrm{mf}(x)$.

*Proof.* Existence. By induction on $x$. If $x$ is empty there is nothing to do. If $x \vdash_{\sigma} a^-$, then $\theta_x$ extends with some $(a^-, b^-)$. By wide, we may assume that $\mathrm{ind}(b^-) = 0$, so that it fits in $A_+$ (such $b^-$ cannot be in $\mathrm{mf}(x)$ by linearity of $x$). If $x \vdash_{\sigma} a^+$, then the extension of $\theta_x$ automatically does the trick.

Uniqueness. As in Lemma 12.1.14. $\square$

In particular, given parallel innocent $\sigma : A$ and $m \in \sigma$ we know from Lemma 12.1.12 that $[m]_{\sigma}$ is linear, thus Lemma 12.1.18 gives us a unique $\mathrm{mf}([m]_{\sigma}) = [\mathrm{lbl}(m)]_{\sigma} \in \mathscr{C}(\mathrm{mf}(\sigma))$ with $\theta_m : [m]_{\sigma} \cong_{\sigma} [\mathrm{lbl}(m)]_{\sigma}$. As the notation suggests, $\mathrm{lbl}(m)$ is considered as the label of $m$, i.e. the move of $\mathrm{mf}(\sigma)$ that $m$ is considered a duplicate of.

This duplicate is also characterized by an exponential slice, defined as:

$$ \alpha : [\mathrm{lbl}(m)]_{\sigma}^{-} \to \mathbb{N} \\ \theta_m(n) \mapsto \mathrm{ind}(\partial_{\sigma}(n)), $$

and writing $\alpha = \mathrm{sl}(m)$ we get $(\mathrm{lbl}(m), \mathrm{sl}(m)) \in \exp(\mathrm{mf}(\sigma))$. Besides:

**Proposition 12.1.19.** Consider $\sigma : A$ parallel innocent. Then, the function

$$ \Psi : \sigma \to \exp(\mathrm{mf}(\sigma)) \\ m \mapsto (\mathrm{lbl}(m), \mathrm{sl}(m)) $$

yields a positive isomorphism $\Psi : \sigma \approx \exp(\mathrm{mf}(\sigma))$.

*Proof.* Injective. We prove that if $\mathrm{lbl}(m) = \mathrm{lbl}(m')$ and $\mathrm{sl}(m) = \mathrm{sl}(m')$, then $m = m'$.

Indeed if $\mathrm{lbl}(m) = \mathrm{lbl}(m')$, by definition this means there are two symmetries

$$ \theta_m : [m]_{\sigma} \cong_{\sigma} [\mathrm{lbl}(m)]_{\sigma}, \quad \theta_{m'} : [m']_{\sigma} \cong_{\sigma} [\mathrm{lbl}(m)]_{\sigma} $$
which we may compose to get $\theta = \theta_{m'}^{-1} \circ \theta_m : [m]_{\sigma} \cong_{\sigma} [m']_{\sigma}$. Now, since $sl(m) = sl(m')$, it follows that $\partial_{\sigma} \theta$ preserves indices of negative events, so that it is positive by +-transparent. Hence, $\theta$ is an identity and $[m]_{\sigma} = [m']_{\sigma}$ since $\sigma$ is thin.

**Surjective.** Consider $(n, \alpha) \in \exp(mf(\sigma))$, then we construct by induction on $m$ some $m \in \sigma$ s.t. $lbl(m) = n$ and $sl(m) = \alpha$, along with a symmetry $\theta : [m]_{\sigma} \cong_{\sigma} [n]_{\sigma}$. If $(n, \alpha) \to_{\exp(mf(\sigma))} (n', \alpha')$ positive, by necessity $\alpha' = \alpha$. Then $\theta$ extends to $\theta' : [m']_{\sigma} \cong_{\sigma} [n']_{\sigma}$ so that $lbl(m') = n'$, and it is direct that $sl(m') = \alpha$ as required. If $(n', \alpha')$ is negative, then by $\sim$-receptive and wide, there is a unique $m \to_{\sigma} m'$ such $\theta$ extends with $(m, m')$, and $ind(\partial_{\sigma}(m)) = \alpha'(m')$ – so that $lbl(m') = n'$ and $sl(m') = \alpha'$.

Remaining verifications are direct, positivity following from +-transparent. $\square$

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

Altogether, we have proved:

**Theorem 12.1.20.** Consider A a mixed board. The operations $mf(-)$ and $exp(-)$ inform a one-to-one correspondence between parallel innocent strategies on A (up to positive iso), and meager parallel innocent strategies on A (up to positive iso).

*Proof.* The statement packages Propositions 12.1.16, 12.1.17 and 12.1.19. $\square$

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

Thus, just as for traditional alternating innocent strategies, parallel innocent strategies have a compact representation via the *meager form*. This is important conceptually: in traditional alternating innocent strategies, the *meager form* may be regarded as *syntax* as *meager sequential innocent strategies* are alternative representations of a syntactic notion of normal form for PCF, the *PCF Böhm trees* – we reviewed this correspondence in Section 3.2.4. Here, by analogy, *meager parallel innocent strategies* may also be regarded as syntax, but *DAG-shaped* rather than tree-shaped.

We included Theorem 12.1.20 because of its conceptual importance, however we shall not rely on it in our definability theorem: we shall only use the notion of *meager form* insofar as it gives an adequate notion of *finiteness* for parallel innocent strategies, that extends the *finiteness* of traditional innocent strategies reviewed in Section 3.2.4.

### 12.1.3 The Meager Form of Sequential Globularity

Here we take a small detour, and prove Theorem 11.3.11 which we postponed until we had access to the *meager form* of parallel innocent strategies. We recall the statement:

**Theorem 11.3.11.** *The induced functor $\downarrow\uparrow$-Unf(-) : $\dashv$-SeqGlob/$\approx$ $\to$ $\downarrow\uparrow$-InnWB is full and faithful: for all A, B mixed boards, the alternating unfolding induces a bijection*

$$ \downarrow\uparrow\text{-Unf}(-) : \dashv\text{-SeqGlob}(A, B)/\approx \simeq \downarrow\uparrow\text{-InnWB}(\underline{A}, \underline{B}). $$

*Proof. Faithful.* Consider $\sigma, \tau : A$ sequential globular on mixed board A, and assume $\downarrow\uparrow$-Unf$_1(\sigma') = \downarrow\uparrow$-Unf$_1(\tau')$. In particular, they have the same P-views – recall from Proposition 11.3.6 that P-views of $\downarrow\uparrow$-Unf$_1(\sigma')$ are exactly those of the form

$$ (\hat{\otimes})(\partial_{\sigma}([m]_{\sigma})) $$
for all events $m \in \sigma$. But by Lemma 12.1.18, there is a unique

$$ \theta_m : [m]_\sigma \cong_\sigma [\mathrm{lbl}(m)]_\sigma $$

with $\mathrm{lbl}(m) \in \mathrm{mf}(\sigma)$. From that, it is clear that $m$ and $\mathrm{lbl}(m)$ generate the same P-view, i.e. $(\widehat{\sigma})(\partial_\sigma([m]_\sigma)) = (\widehat{\sigma})(\partial_\sigma([\mathrm{lbl}(m)]_\sigma))$. Therefore, the P-views of $\downarrow\uparrow$-Unf$_1(\sigma')$ can be obtained simply from the events of the meager form of $\sigma$. Moreover, for any P-view $s$ on $\mathcal{A}$, there is at most one $m \in \mathrm{mf}(\sigma)$ generating $s$ – if they were two, they would be symmetric by Lemma 11.2.4, and thus equal by Proposition 12.1.5. Thus, any P-view of $\downarrow\uparrow$-Unf$_1(\sigma') = \downarrow\uparrow$-Unf$_1(\tau')$ is witnessed by exactly one event of $\mathrm{mf}(\sigma)$, and exactly one event of $\mathrm{mf}(\tau)$. This entails a bijection $\varphi : |\mathrm{mf}(\sigma)| \simeq |\mathrm{mf}(\tau)|$, and it is a direct verification that this entails a positive isomorphism $\varphi : \mathrm{mf}(\sigma) \approx \mathrm{mf}(\tau)$. By Theorem 12.1.20, this entails $\sigma \approx \tau$ as well – from this follows that $\downarrow\uparrow$-Unf$_1(-)$ is faithful.

**Full.** Now, consider $\sigma : \mathcal{A}$ an innocent well-bracketed alternating strategy on $\mathcal{A}$. For every non-empty even-length P-view $s$ of $\sigma$, choose a copy index $\sharp s \in \mathbb{N}$ so that this is injective. We then specify a meager causal innocent strategy with events

$$ |\sigma| = \{s \in \sigma \mid s \text{ non-empty P-view}\}, $$

with causality the prefix ordering, no conflict, trivial symmetries. We set the display map by induction: for odd-length $sa^+b^-$, we set it to the unique event $b'$ with $\mathrm{lbl}(b') = b$, $\mathrm{pred}(b') = \partial_\sigma(sa^+)$, and $\mathrm{ind}(b') = 0$ – this event exists by wide. For even-length $s = s_1a^-s_2b^+$ where $b^+$ points to $a^-$, we set the display to the unique event $b'$ with $\mathrm{lbl}(b') = b$, $\mathrm{pred}(b') = \partial_\sigma(s_1a^-)$ and $\mathrm{ind}(b') = \sharp s$. Altogether, it is easily verified that this defines a meager sequential innocent strategy on $\mathcal{A}$ and that $(\widehat{\sigma})(\partial_\sigma([s]_\sigma)) = s$. Hence the P-views of $\downarrow\uparrow$-Unf$_1(\sigma')$ are exactly those of $\sigma$ by Proposition 11.3.6, thus $\downarrow\uparrow$-Unf$_1(\sigma') = \sigma$ by Proposition 3.2.13 – from this follows that $\downarrow\uparrow$-Unf$_1(-)$ is full. $\square$

So that indeed, globular causal strategies are conservative extensions of traditional well-bracketed innocent strategies. Moreover, we established that by showing that the meager form of globular strategies specializes to the meager form of Section 3.2.4.

### 12.1.4 Finite Tests Suffice

Back on track, we now introduce a notion of finiteness for parallel innocent strategies:

**Definition 12.1.21.** Consider A a mixed board, and $\sigma : A$ a parallel innocent strategy. Then $\sigma$ is finite iff $|\mathrm{mf}(\sigma)|_+ = \{s \in |\mathrm{mf}(\sigma)| \mid \mathrm{pol}(s) = +\}$ is finite. In that case, the size of $\sigma$ is the cardinal of $|\mathrm{mf}(\sigma)|_+$.

As in the case of traditional innocent strategies, our forthcoming definability result will concern only finite parallel innocent strategies. So that finite definability does entail intensional full abstraction, we must show that if two strategies can be distinguished by a parallel innocent strategy, then they can be distinguished by a finite one.

Any parallel innocent strategy can be approximated by finite ones:

**Proposition 12.1.22.** Consider A a mixed board, and $\sigma : A$ a parallel innocent. Writing

$$ D = \{\tau : A \mid \tau \text{ finite} \& \tau \triangleleft \sigma\} $$
yields a directed set of finite parallel innocent strategies, such that $\sigma = \bigvee D$.

*Proof.* By definition, $\bigvee D \triangleleft \sigma$. For the other direction, pick $m \in \sigma$. Considering

$$|\tau| = \{n \in |\sigma| \mid \forall p^{+} \leq_{\sigma} n, \mathrm{mf}(p^{+}) \leq_{\sigma} \mathrm{mf}(m)\},$$

it is easily verified that inheriting from $\sigma$ all additional components makes $\tau : A$ a parallel innocent strategy s.t. $\tau \triangleleft \sigma$. Moreover $m \in \tau$, and $\tau$ is finite since all positive events of $\mathrm{mf}(\tau)$ are below $\mathrm{mf}(m)$. Altogether $\tau \in D$ and $m \in \tau$, so $m \in \bigvee D$. $\square$

The development above concerns strategies on mixed boards, but recall that mor-
phisms in $\dashrightarrow$-**Strat** are strategies between mixed boards: a $\sigma \in \dashrightarrow$-**Strat**(A, B) is a
well-bracketed causal strategy on $!A \vdash B$. Nevertheless the above directly extends:
$\sigma \in \dashrightarrow$-**Inn**(A, B) is finite if $\Lambda(\sigma) : A \Rightarrow B$ is. From the above, we get:

**Corollary 12.1.23.** Consider A a mixed board, and $\sigma_1, \sigma_2 : A$ parallel innocent.

If there is $\alpha : !A \vdash U$ parallel innocent such that

$$\alpha \odot_1 \sigma_1 \downarrow, \quad \alpha \odot_1 \sigma_2 \uparrow,$$

then there is $\alpha' \triangleleft \alpha$ finite and parallel innocent, such that

$$\alpha' \odot_1 \sigma_1 \downarrow, \quad \alpha' \odot_1 \sigma_2 \uparrow.$$

Finally if $\alpha$ is globular (resp. well-bracketed), then so is $\alpha'$.

*Proof.* By Proposition 12.1.22, $\Lambda(\alpha) = \bigvee D$ for $D$ some directed set of finite parallel innocent strategies – automatically innocent, as this is inherited from $\alpha$. The result then directly follows by continuity of composition of causal strategies; preservation of well-bracketing and globularity are immediate. $\square$

**12.2 Factorization**

Our next goal is to prove a definability result for finite globular strategies, but it shall
be more complex than in the traditional case. Indeed, unlike in Section 3.2.4, globular
strategies have no “first Player move” to reproduce first syntactically. Hence we organize
our definability process differently. Its core is a factorization result (Corollary 12.2.18):
namely, that every finite globular $\alpha : !(&A_i) \vdash \mathcal{X}$ may be obtained as

$$\alpha \equiv \mathrm{fo}(\alpha) \odot_1 \langle x_i \alpha_{k,1} \dots \alpha_{k,p_i} \mid i \in I, k \in K_i \rangle, \quad (12.1)$$

with $\mathrm{fo}(\alpha)$ a strategy on a first-order type and $\alpha_{k,j}$ strictly smaller. This reduces finite definability to that for finite first-order strategies, dealt with in Section 12.3.1.

We first extract the components mentioned in (12.1): the first-order substrategy $\mathrm{fo}(\alpha)$,
and the argument substrategies $\alpha_{k,j}$. We use as illustration the meager strategy with typ-
ical linear configurations in Figure 12.5. The first-order sub-strategy, in red, has events
those depending on no Opponent question besides the initial move: it is independent of
Opponent's exploration of the arguments, and is purely first-order. The Player questions
<figure><img src="image_219.png" /><figcaption>Figure 12.5: A finite meager globular strategy</figcaption></figure>

$$
f : \mathbb{B} \to \mathcal{U}, g : (\mathcal{U} \to \mathbb{B}) \to \mathbb{B} \vdash \\
\textbf{let} \left( \begin{array}{l} x = f \tt{t} \\ y = g (\lambda z \mathcal{U} . \text{let} \left( \begin{array}{l} u = z \\ v = g \perp \end{array} \right) \text{in } v) \end{array} \right) \text{ in (if } y \text{ then } (f \tt{ff}; \tt{tt}) \text{ else } \tt{ff}) : \mathbb{B}
$$

<caption>Figure 12.6: Factorization and definability for Figure 12.5</caption>

in this first-order part play a special role; we call them *primary questions*. Intuitively, they correspond to occurrences of variables not appearing in an argument to a variable call. In Figure 12.5, the primary questions are $q_1^+$, $q_1^+$ and $q_2^+$. Depending on their type, the primary questions admit arguments that Opponent can access by playing questions pointing to them. Parts of the strategy accessed in this way are the *argument sub-strategies* – in Figure 12.5 there are three, respectively prompted by (i.e. causally depending on) $q_{0,i}^-$, $q_{2,k}^-$ and $q_{1,r}^-$ and colored accordingly.

The strategy of Figure 12.5 is exactly definable; as illustration we show the term in Figure 12.6, with subterms colored so as to match the four components of the strategy<fnref n="2" />.

The proof of factorization is organized as follows: in Section 12.2.1 we extract the first-order part, in Section 12.2.2, we extract the argument substrategies, and in Section 12.2.3, we recompose them to obtain the original strategy back.

**12.2.1 The Flow Substrategy**

**Shallow substrategy.** Consider $A$ a type, and $\alpha : [A]$ a finite globular strategy.

Necessarily $A$ has form $A_1 \to \dots \to A_n \to \mathcal{X}$ for $A_i = A_{i,1} \to \dots \to A_{i,p_i} \to \mathcal{X}_i$.

<footnote n="2">²In the end, our definability process will not quite give the term of Figure 12.6 but a sequential version as we only know how to define first-order strategies in general up to *positional equivalence* – see Section 12.3.1.</footnote>
Recall $\mathcal{X}$, $\mathcal{X}_i$ range over ground types, i.e. $\cup$, $\mathbb{B}$ and $\mathbb{N}$. Up to currying, we write

$$ \alpha : !(&_{1\le i\le n} A_i) \vdash \mathbf{X}, $$

omitting semantic brackets. We often shorten the left hand side part to $!(&A_i)$, and reuse $A$ for the board $!(&A_i) \vdash \mathbf{X}$. Now, we start with the *shallow substrategy*. First:

**Definition 12.2.1.** Consider an event $m \in \alpha$.

Then $m$ is **shallow** iff $[m]_\alpha$ contains exactly one Opponent question.

In Figure 12.5, the shallow events are exactly those in red. Note that if $m$ is shallow, then the Opponent question in $[m]_\alpha$ is necessarily the initial Opponent question. As one can dive within the $A_i$s only via an Opponent question, this means that $m$ and its causal history must remain in the *first-order* part of the arena.

The shallow substrategy is obtained by restricting $\alpha$ to shallow events:

**Proposition 12.2.2.** Set $\mathrm{sh}(\alpha)$ with the shallow events of $\alpha$, other components inherited.

Then, $\mathrm{sh}(\alpha) : !(&\mathbf{X}_i) \vdash \mathbf{X}$ is finite globular.

*Proof.* Write $\mathrm{sh}(A)$ for the board $!(&\mathbf{X}_i) \vdash \mathbf{X}$. First, for each $m \in \mathrm{sh}(\alpha)$, $\partial_\alpha(m) \in \mathrm{sh}(A)$: indeed, the least events in $A$ but not in $\mathrm{sh}(A)$ are Opponent questions. For extension, as symmetries are order-isos preserving polarities and Q/A labeling, they preserve $\mathrm{sh}(\alpha)$. The conditions for a finite globular strategy are direct from $\alpha$. $\square$

This captures the strategy induced by the red part of Figure 12.5.

**The flow substrategy** Eventually we wish to reconstruct $\alpha$ from its first-order and argument substrategies using the composition mechanisms available on causal strategies. But we cannot hope to do that merely with $\mathrm{sh}(\alpha)$. Indeed, two Player questions in $\mathrm{sh}(\alpha)$ playing in the same component $\mathbf{X}_i$ must receive the same argument substrategy if $\alpha$ is to be reassembled compositionally – but there is no reason why two Player questions in the same component should always have the same argument substrategy!

Thus rather than working with $\mathrm{sh}(\alpha)$, we need to relabel it to send distinct (non-symmetric) Player questions to distinct components. First we define:

**Definition 12.2.3.** A **primary question** of $\alpha$ is any $q^{Q,+} \in \mathrm{mf}(\mathrm{sh}(\alpha))$. We write $\mathcal{Q}$ for the set of primary questions, and $\mathcal{Q}_i$ for the primary questions displaying to $\mathbf{X}_i$.

By construction, $\mathcal{Q} = \wp_{1\le i\le n} \mathcal{Q}_i$ – as observed above, $\mathcal{Q}$ is finite. A $m^{Q,+} \in \mathrm{sh}(\alpha)$ might not be a primary question, but it must necessarily be symmetric to $\mathrm{lbl}(m) \in \mathcal{Q}$ a primary question (as its *label*, i.e. its representative in the meager form).

**Definition 12.2.4.** The *flow substrategy* of $\alpha$, written

$$ \mathrm{flow}(\alpha) : \bigotimes_{1 \le i \le n} \bigotimes_{q \in \mathcal{Q}_i} !\mathbf{X}_i \vdash \mathbf{X} $$
<figure><img src="image_220.png" /><figcaption>Figure 12.7: Configurations of the flow substrategy for Figure 12.5</figcaption></figure>

is obtained as sh(α) with the display map ∂_sh(α) replaced with:

$$
\begin{align*}
\partial_{\text{flow}(\alpha)}(m^{Q,-}) &= (2, a) & \text{if } \partial_{\text{sh}(\alpha)}(m^{Q,-}) &= (2, a) \\
\partial_{\text{flow}(\alpha)}(m^{A,+}) &= (2, a) & \text{if } \partial_{\text{sh}(\alpha)}(m^{A,+}) &= (2, a) \\
\partial_{\text{flow}(\alpha)}(m^{Q,+}) &= (1, (i, (\text{lbl}(m), (j, a)))) & \text{if } \partial_{\text{sh}(\alpha)}(m^{Q,+}) &= (1, (j, (i, a))) \\
\partial_{\text{flow}(\alpha)}(m^{A,-}) &= (1, (i, (j(\text{lbl}(m)), (j, a)))) & \text{if } \partial_{\text{sh}(\alpha)}(m^{A,-}) &= (1, (j, (i, a))),
\end{align*}
$$

i.e. sending each $q \in \mathcal{Q}$ and its answers to the copy of $X_i$ specified by indices $i, q$.

It is a finite globular strategy (though not a morphism in $\rightarrow$-Strat, but the same definition applies nonetheless). Figure 12.7 shows typical configurations of the flow substrategy for Figure 12.5, tagging each component by a primary question.

**12.2.2 The Argument Substrategies**

Next, we focus on the higher-order structure, aiming to extract the arguments to (the variable calls corresponding to) the primary questions. A slight complication comes from the fact that because answers in the shallow substrategy can be replicated, **α** actually comprises many copies of each argument substrategy – we solve that by temporarily only considering the part of **α** where shallow answers have copy index 0:

**Definition 12.2.5.** An event $m \in \alpha$ is *canonical* iff for all shallow $n^{A,-} \le \alpha m$, $\text{ind}(\partial_{\alpha}(n)) = 0$. We write $\|\alpha\|$ the set of canonical events of $\alpha$.

A primary question is always canonical; so are all events in mf(α). Now, fix a primary question $q \in \mathcal{Q}_i$. It displays to an initial event in $A_i$, which is:

$!A_{i,1} \to \dots \to !A_{i,p_i} \to \mathbf{X}_i .$

Argument substrategies are accessed by Opponent questions pointing to (moves sym-
metric to) primary questions. Up to symmetry, there are $p_i$ distinct Opponent questions
pointing to $q$, matching the $p_i$ arguments of $A_i$. From now on, if $q \in \mathbb{Q}_i$ is a primary question and $q \to_{\sigma} m^{Q, -}$ an Opponent question, we shall say that $m$ is **in component $j$** if it displays to an initial move of $!A_{i,j}$. For $q \in \mathbb{Q}_i$ and $1 \le j \le p_i$, we shall extract the argument sub-strategy $\alpha_{q,j}$ initiated by Opponent questions pointing to $q$ in component $j$. As the strategy provides the information for an argument of $A_i$ it must live in $A_{i,j}$; but it can still access the context, so we aim for a finite globular strategy:

$$ \alpha_{q,j} : !(&A_i) \vdash !A_{i,j}. $$

**Extracting events.** To do this, we assign to all events of $\alpha$ tags, as follows:

**Definition 12.2.6.** Consider $m \in \|\alpha\|$. We write:

$$ m \in \mathrm{sh}(\alpha) \Leftrightarrow \text{m is shallow,} $$

$$ m \in \alpha_{q,j} \Leftrightarrow \text{there is } q \to_{\alpha} n^{Q, -} \text{ in component } j, \text{ such that } n \le_{\alpha} m, $$

where in the second clause, $q \in \mathbb{Q}_i$ is a primary question and $1 \le j \le p_i$.

Any $m \in \|\alpha\|$ receives a tag as either in $\mathrm{sh}(\alpha)$; or in one of the argument sub-strategies. Crucially, each event receives *exactly one tag* – this is subtle and involves all our structural constraints on strategies. For instance, without *globular*, in Figure 10.19 the move $q_2^+$ would be tagged for *two* distinct argument sub-strategies.

**Lemma 12.2.7.** Every $m \in \|\alpha\|$ receives exactly one tag following Definition 12.2.6.

*Proof.* First, each $m \in \|\alpha\|$ receives *at least* one tag. Any $[m]_\alpha$ contains at least one Opponent question: the initial move. If it contains exactly one Opponent question, then $m$ is shallow by definition. Assume there are at least two. Take $n^{Q, -} \le_\alpha m$ minimal such that it is a non-initial Opponent question. Then its immediate predecessor must be some primary question $q \in \mathbb{Q}_i$; and so there is $1 \le j \le p_i$ s.t. $m \in \alpha_{q,j}$.

We prove that $m$ receives *at most* one tag. Clearly if $m \in \alpha_{q,j}$ for some $q \in \mathbb{Q}_i$ and $1 \le j \le p_i$, there are at least two Opponent questions in $[m]_\alpha$ so we cannot have $m \in \mathrm{sh}(\alpha)$. But $m$ could be in two argument substrategies: assume $m \in \alpha_{q,j}$ and $m \in \alpha_{q',j'}$ for $q \in \mathbb{Q}_i, q' \in \mathbb{Q}_{i'}, 1 \le j \le p_i$ and $1 \le j' \le p_{i'}$. We first show that $q = q'$; seeking a contradiction assume they are distinct. But $q$ and $q'$ cannot be comparable: if $q \le_\alpha q'$, $[q']_\alpha$ has at least two Opponent questions, contradicting $q' \in \mathrm{sh}(\alpha)$.

Take $\rho \to m, \rho' \to m \in \mathrm{gcc}(\alpha)$, respectively passing through $q$ and $q'$. We draw:

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

and since $q, q'$ are distinct, the diagram may be chosen with $X = \{m_1, \dots, m_k\}$ and $Y = \{n_1, \dots, n_p\}$ disjoint. By *pre-innocence*, $m_1$ and $n_1$ are positive. Moreover, since the board is forestial and alternating, it is immediate from Lemma 6.1.16 that $m_{k+1}$ is positive, and $m_k, n_p$ positive. Altogether we have a *globule*, so $X$ and $Y$ are complete by globularity – and moreover the diagram has the shape as in (10.2), and in particular $q$
<figure><img src="image_222.png" /><figcaption>Figure 12.8: Ev. $|\alpha_{q_1^+,1}|$ of Figure 12.5</figcaption></figure>

<caption>Figure 12.9: Its reassignment in $\alpha_{q_1^+,1}$</caption>

is answered in $\rho$. Additionally as observed in (10.2), writing $q = m_i$, $m_{i+1}$ must answer $q$. But since $m \in \alpha_{q,j}$, $q \to_{\alpha} n^{Q_{u,-}} \le_{\alpha} m$ where $n$ is a negative question in component $j$. Then necessarily, $n = m_{i+1}$, or we get a contradiction with parallel innocence. Thus $m_{i+1}$ is both a question and an answer, contradiction, so $q = q'$.

Finally, if $j$ and $j'$ were distinct, there would be necessarily distinct $q \to_{\alpha} n_1^{Q,-}$ in component $j$ and $n_2^{q,-}$ in component $j'$ such that $n_1, n_2 \le_{\alpha} m$, but this is in direct contradiction with pre-innocence. Thus $j = j'$, concluding the proof. $\square$

This shows any $m \in \|\alpha\|$ can always be attributed to exactly one of the sub-strategies we wish to extract. Accordingly, the argument sub-strategies will have events

$$|\alpha_{q,j}| = \{m \in \|\alpha\| \mid m \in \alpha_{q,j}\},$$

completed to pass by inheriting the components from $\alpha$, as will be made explicit later.

**Assigning display map.** The main challenge in extracting the argument sub-strategies is to define what shall be their new display maps. Indeed, $\partial_{\alpha}$ still displays events in $\alpha_{q,j}$ to moves in $!(A_i) \vdash X$, whereas $\partial_{\alpha_{q,j}}$ must display then to $!(A_i) \vdash !A_{i,j}$.

For this, we must give special care to those events that correspond to the new $!A_{i,j}$ component on the right hand side, reindexing them as illustrated in Figures 12.8 and 12.9. For this we split $|\alpha_{q,j}|$ in two subsets: on the one hand, some events depend statically, i.e. with respect to $\le_A$ (through $\partial_{\alpha}$) on the primary question $q$ – in Figure 12.8, those are $q_0^-, q_0^+, \check{0}^-$ and $b_0^+$. On the other hand, the remaining events must follow from new calls to variables in the context – in Figure 12.8, those are $q_3^+$ and $b_0^-$. These two subsets are treated differently when defining the new display map: the former are left unchanged, while the latter are reindexed as in Figure 12.9.
It will be helpful to have notations for the canonical embeddings of the set of moves $|A_i|$ and $|A_{i,j}|$ into $|A|$. More precisely, for each primary question $q \in \mathcal{Q}_i$, we write

$$ \iota_q(-) : |A_i| \to |A| $$

the injection adding the sequence of tags addressing $A_i$ within $A$, originating from the tagged disjoint unions in the board constructions – in particular, $\iota_q$ maps the initial move of $A_i$ to $\partial_\alpha(q)$. Likewise, $\iota_{q,j} : |A_{i,j}| \to |A|$ addresses the $j$-th argument of $q$. Then:

**Definition 12.2.8.** We define a display map for $\alpha_{q,j}$ by setting, for $m \in \alpha_{q,j}$:

$$ \partial_{\alpha_{q,j}}(m) = \iota_{\nu}(a) \quad \text{if } \partial_{\alpha}(m) = \iota_{q,j}(a), $$

$$ \partial_{\alpha_{q,j}}(m) = \partial_{\alpha}(m) \quad \text{otherwise,} $$

where $\iota_\nu(a) = (1, a)$ and $\iota_\mu(a) = (2, a)$.

Altogether, this lets us extract $\alpha_{q,j}$ as intended:

**Proposition 12.2.9.** Consider $q \in \mathcal{Q}_i$ and $1 \le j \le p_i$. The argument *substrategy* for $q, j$ is $(|\alpha_{q,j}|, \le_{q,j}, \#_{q,j}, \mathcal{S}(\alpha_{q,j}), \partial_{\alpha_{q,j}})$, with components $\le_{q,j}$ and $\#_{q,j}$ the restrictions of $\alpha, \mathcal{S}(\alpha_{q,j}) = \{\theta \cap |\alpha_{q,j}|^2 | \theta \in \mathcal{S}(\alpha)\}$, and $\partial_{\alpha_{q,j}}$ in Definition 12.2.8.

Then, $\alpha_{q,j} : !(&A_i) \vdash !A_{i,j}$ is a globular finite strategy.

*Proof.* A lengthy but routine verification. $\square$

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

**Removing the bang.** But we must obtain a morphism in $\dasharrow$-Glob, and thus eliminate the bang on the right hand side. This is done by composition with *dereliction*, i.e.

$$ \alpha_{q,j}^{\bullet} = \mathrm{der}_{A_{i,j}} \odot \alpha_{q,j} : !(&A_i) \vdash A_{i,j}, $$

it only remains to show that this satisfies the conditions which will later on allow us to proceed from $\alpha_{q,i}^*$ with the inductive definability argument:

**Proposition 12.2.10.** Consider $q \in \mathcal{Q}_i$ a primary question, and $1 \le j \le p_i$.

Then, $\alpha_{q,j}^*$ is finite globular with size strictly lesser than $\alpha$.

*Proof.* Using Proposition 7.3.1, it is easy that $\alpha_{q,j}^*$ is positively isomorphic to the strategy obtained from $\alpha_{q,j}$ by restricting the initial Opponent question to copy index 0. This also informs an injection of $\mathrm{mf}(\alpha_{q,j}^*)$ into $\mathrm{mf}(\alpha)$ not reaching the primary question $q$, from which follows the announced size constraint. $\square$

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

Note that $\alpha_{q,j}$ is easily recovered from $\alpha_{q,j}^*$, as we have

$$ \alpha_{q,j} \approx (\mathrm{der}_{A_{i,j}} \odot \alpha_{q,j})^1 = (\alpha_{q,j}^*)^1 \quad (12.2) $$

via the “bang lemma” (Lemma 10.3.7) and by definition of $\alpha_{q,j}^!$.
### 12.2.3 Recomposition

Having extracted from $\alpha$ its flow substrategy and its argument substrategies, our next aim is to prove that $\alpha$ can be reconstructed from those.

**Reconstructing $\alpha$.** From the original strategy $\alpha : !(&A_i) \vdash X$, we have now extracted the flow substrategy and a family of argument substrategies:

$$ 
\begin{array}{l@{\quad}l}
\text{flow}(\boldsymbol{\alpha}) & : \bigotimes_{1 \le i \le n} \bigotimes_{q \in \mathcal{Q}_i} !X_i \vdash X \\
\boldsymbol{\alpha}_{q,j}^{\bullet} & : !(&A_i) \vdash A_{i,j} \qquad \text{for each } q \in \mathcal{Q}_i \text{ and } 1 \le j \le p_i.
\end{array}
$$

For each $q \in \mathcal{Q}_i$, we first form a strategy $\alpha_q : !(&A_i) \vdash X_i$ gathering all the arguments for the primary question $q$. This is constructed from the argument substrategies, using the internal language corresponding to the cartesian closed structure of $\dashv$-Inn:

$$ \boldsymbol{\alpha}_q = x_1 : A_1, \dots, x_n : A_n \vdash x_i \boldsymbol{\alpha}_{q,1}^{\bullet} \dots \boldsymbol{\alpha}_{q,p_i}^{\bullet} : X_i. $$

Then, we plug each $\alpha_q$ onto the corresponding primary question in the flow substrategy. This is done relying on the relative Seely category structure of NTCG-Inn:

$$ \text{recomp}(\boldsymbol{\alpha}) = \text{flow}(\boldsymbol{\alpha}) \odot (\bigotimes_{1 \le i \le n} \bigotimes_{q \in \mathcal{Q}_i} \boldsymbol{\alpha}_q^{\bullet}) \odot \delta_{\&A_i} : !(&A_i) \vdash X, $$

where for $B$ a strict board and $n \in \mathbb{N}$, we write $\delta_B : !B \vdash (!B)^{\otimes n}$ for the obvious strategy (leaving $n$ implicit). In the sequel we may only write $\delta$.

**Positions of recomp($\alpha$).** Recall that the positional equivalence $\equiv$, studied in Section 10.4, consists in listing the zero-payoff symmetry classes of configurations reached by (+-covered configurations of) a visible strategy. We expect that $\text{recomp}(\alpha) \approx \alpha$, but we shall only prove $\text{recomp}(\alpha) \equiv \alpha$ – this is simpler as positions compose relationally. We shall make use of the syntax for positions on $\dashv$-boards introduced in Figure 10.17.

We now analyse the positions of the recomposition (12.2.3). We start with:

**Lemma 12.2.11.** Consider $B$ a strict $\dashv$-board.

Then, the positions $(\delta_B)$ of $\delta_B : !B \vdash (!B)^{\otimes n}$ are exactly those

$$ \left( \sum_{1 \le i \le n} x_i \vdash \bigotimes_{1 \le i \le n} x_i \right) \in (!B \vdash (!B)^{\otimes n}) $$

where $x_i \in (!B)$ for all $1 \le i \le n$.

*Proof.* By a direct variation of Lemma 6.4.4. $\square$

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

Next we analyse the positions of $\alpha_q$ for $q \in \mathcal{Q}_i$:
**Lemma 12.2.12.** For any $q \in \mathbb{Q}_i$, the positions $(\alpha_q)$ are exactly those of the form

$$ \left( \left[ (i, y_{q,1} \to \dots \to y_{q,p_i} \to v_q) \right] + \sum_{1 \le j \le p_i} x_{q,j} \right) \vdash v_q \in (\mathcal{I}(\&A_i) \vdash \mathcal{X}_i) $$

where for each $1 \le j \le p_i$, $(x_{q,j} \vdash y_{q,j}) \in (\alpha_{q,j})$, and for $v_q \in (\mathcal{X}_i)$.

*Proof.* From the laws of relative Seely categories, $\alpha_q$ is positively isomorphic to

$$ \begin{array}{rcl} \mathcal{I}(\&A_i) & \stackrel{\delta}{\longrightarrow} & \otimes_{p_i+1} \mathcal{I}(\&A_i) \\ & \stackrel{\downarrow}{\longrightarrow} & (\otimes_{1 \le j \le p_i} (\alpha_{q,j}^*)') \otimes \llbracket x_i \rrbracket \\ & \stackrel{\mathcal{I}(\&A_i)}{\longrightarrow} & A_i \stackrel{\mathrm{ev}}{\longrightarrow} \mathcal{X}_i \end{array} $$

in NTCG. The lemma follows from Corollary 10.4.15, Lemma 12.2.11, (12.2)and characterisations analogous to Lemma 12.2.11 for other copycat-like strategies. $\square$

From all those, we may characterise the positions of recomp($\alpha$) as

**Corollary 12.2.13.** The positions of recomp($\alpha$) are exactly those of the form

$$ \sum_{1 \le i \le n} \sum_{q \in \mathbb{Q}_i'} \left( \left[ (i, y_{q,1} \to \dots \to y_{q,p_i} \to v_q) \right] + \sum_{1 \le j \le p_i} x_{q,j} \right) \vdash v \in (\mathcal{I}(\&A_i) \vdash \mathcal{X}) $$

where for all $1 \le i \le n$, $\mathbb{Q}_i'$ is a subset of $\mathbb{Q}_i$, and:

$$ (\otimes_{1 \le i \le n} \otimes_{q \in \mathbb{Q}_i'} v_q \vdash v) \in (\text{flow}(\alpha)), \quad ((x_{q,j} \vdash y_{q,j}) \in (\alpha_{q,j}))_{q \in \mathbb{Q}_i', 1 \le j \le p_i} $$

*Proof.* Direct from Lemmas 12.2.11, 12.2.12 and Corollary 10.4.15. $\square$

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

**Positions of $\alpha$.** Next, we must similarly characterise the positions of $\alpha$.

We call **stopping configurations** of $\alpha$ those $x \in \mathbb{C}^+(\alpha)$ such that $\kappa(\partial_\alpha(x)) = 0$ (i.e. those configurations that contribute a point to the relational collapse), and such that all Opponent answers in $x$ have copy index 0. Write stop($\alpha$) for this set; our first observation is that the relational collapse of $\alpha$ is entirely spanned by stopping configurations – the restriction to the copy index of Opponent answers has no consequence.

**Lemma 12.2.14.** Consider $x_\Gamma \vdash x_\chi \in (\alpha)$.

Then, there is a stopping configuration $x \in \text{stop}(\alpha)$ such that $\partial_\alpha x \in x_\Gamma \vdash x_\chi$.

*Proof.* By definition, there is $y \in \mathbb{C}^+(\alpha)$ such that $\partial_\alpha y \in x_\Gamma \vdash x_\chi$. In particular, $\kappa(\partial_\alpha y) = 0$. By definition of payoff on ground types, this entails that all questions in $y$ have exactly one answer. We construct $z \in \mathbb{C}(A)$ from $\partial_\alpha(y)$ using *wide*, by changing the copy index of every negative answer to 0 – by $--\text{transparent}$, we obtain a symmetry

$$ \theta : \partial_{\alpha}(x) \cong_A^- z, $$
and applying Lemma 7.2.6 we get $y \cong_{\alpha} x$ and $\varphi : \partial_{\alpha} y \cong_{A}^{+} z$. By $\text{+-transparent}$, $\varphi$ preserves the copy indices of negative events, thus the indices of negative answers in $\partial_{\alpha} y$ is $0$. Finally, as $x \cong_{\alpha} y$ we have $\partial_{\alpha} y \in x_{\Gamma} \vdash x_{\chi}$, and $y$ is a stopping configuration. $\square$

Restricting to stopping configurations is important, because events of stopping configurations are canonical in the sense of Definition 12.2.5 (i.e. the shallow Opponent answers on which they depend have copy index $0$) – and argument sub-strategies were extracted from the canonical events of $\alpha$, following Definition 12.2.6. Thanks to this, we shall be able to partition any $x \in \text{stop}(\alpha)$ into stopping configurations from the flow substrategy, and the argument sub-strategies. This partitionning is the key argument to link the positions of $\alpha$ with the positions of its sub-strategies.

Let us perform this partitioning. We define components of the partition as

$$ \begin{aligned} \mathrm{sh}(x) &= \{m \in x \mid m \in \mathrm{sh}(\alpha)\} \\ x_{q,j} &= \{m \in x \mid m \in \alpha_{q,j}\}, \quad (\text{for } q \in \mathcal{Q}_i \text{ and } 1 \le j \le p_i) \end{aligned} $$

additionally we write $\mathcal{Q}^x = \mathcal{Q} \cap x$, and $\mathcal{Q}_i^x$ likewise. We have:

**Lemma 12.2.15.** Consider $x \in \text{stop}(\alpha)$. Then $\mathrm{sh}(x) \in \text{stop}(\mathrm{sh}(\alpha))$, $x_{q,j} \in \text{stop}(\alpha_{q,j})$ and $x$ partitions as

$$ x = \mathrm{sh}(x) \uplus \left( \bigcup_{1 \le i \le n} \bigcup_{q \in \mathcal{Q}_i^x} \bigcup_{1 \le j \le p_i} x_{q,j} \right), $$

moreover this decomposition is compatible with display maps, in the sense that

$$ \partial_{\alpha}(x) = (\uplus_{1 \le i \le n} \uplus_{q \in \mathcal{Q}_i^x} ([l_q(z_{q,1} \to \dots \to z_{q,p_i} \to v_q)] \uplus [\uplus_{1 \le j \le p_i} l_{\ell}(y_{q,j})])) \uplus l_{\nu}(v), $$

where we have, for all $1 \le i \le n$, $q \in \mathcal{Q}_i^x$ and $1 \le j \le p_i$:

$$ \partial_{\text{flow}(\alpha)}(x) = l_{\ell} \left( \bigotimes_{1 \le i \le n} \bigotimes_{q \in \mathcal{Q}_i^x} v_q \right) \uplus l_{\nu}(v) \quad \partial_{\alpha_{q,j}}(x_{q,j}) = l_{\ell}(y_{q,j}) \uplus l_{\nu}(z_{q,j}). $$

*Proof.* From Lemma 12.2.7, lengthy but straightforward verifications. $\square$

Reciprocally, any compatible collection of stopping configurations from the various substrategies may be assembled into a stopping configuration of $\alpha$:

**Lemma 12.2.16.** For $x \in \text{stop}(\mathrm{sh}(\alpha))$ and $(x_{q,j} \in \text{stop}(\alpha_{q,j}))_{1 \le i \le n, q \in \mathcal{Q}_i^x, 1 \le j \le p_i}$,

$$ x \uplus \left( \bigcup_{1 \le i \le n} \bigcup_{q \in \mathcal{Q}_i^x} \bigcup_{1 \le j \le p_i} x_{q,j} \right) \in \text{stop}(\alpha). $$

*Proof.* Lengthy but straightforward verifications. $\square$
From this we may finally conclude the proof of factorization:

**Corollary 12.2.17.** *The strategies α and recomp(α) are positionally equivalent.*

*Proof.* Altogether, Lemmas 12.2.15 and 12.2.16 ensure that stopping configurations of α are in one-to-one correspondence with the data of stopping configurations $x \in \text{stop}(\text{sh}(\alpha))$ and families $(x_{q,j})_{1 \le i \le n, q \in \mathbb{Q}^x}, 1 \le j \le p_i$, in a way compatible with the display maps as stated in Lemma 12.2.15. Taking symmetry classes, we derive the same characterisation of complete positions of α as that of recomp(α) in Corollary 12.2.13. □

**Syntactic factorization.** Finally, we reformulate this relying on the cartesian closed structure only. The **first-order substrategy** $fo(\alpha) \in \text{NTCG}_1(\&_{1 \le i \le n} \&_{q \in \mathbb{Q}} X_i, X)$ is obtained in the obvious way from flow($\alpha$) using the relative Seely category structure. Using Corollary 12.2.17, Proposition 12.2.10, and laws of a relative Seely category:

**Corollary 12.2.18.** Any globular strategy $\alpha : !(&A_i) \vdash X$ factors as

$$ \alpha \equiv fo(\alpha) \odot_1 \langle x_i \alpha_{q,1}^* \dots \alpha_{q,p_i}^* | 1 \le i \le n, q \in \mathbb{Q}_i \rangle, $$

where $fo(\alpha) : !(&X_i) \vdash X$ and $\alpha_{q,j}^* : !(&A_i) \vdash A_{i,j}$ are globular.

If $\alpha$ is finite, so are $fo(\alpha)$ and $\alpha_{q,j}^*$, the latter with size strictly lesser than that of $\alpha$.

## 12.3 Finite Definability and Full Abstraction

### 12.3.1 First-Order Definability

Assuming we are in the process of an inductive definability procedure, we may assume that we have terms for the argument sub-strategies $\alpha_{q,j}^*$. Thus, it remains to define

$$ fo(\alpha) : !(&X_i) \vdash X $$

the first-order substrategy.

**Strict definability.** This naturally asks the question: does finite definability hold for first-order globular strategies? It is fairly easy to see that the answer is negative:

**Proposition 12.3.1.** *The strategy with meager form pictured in Figure 12.10 is finite globular, but not definable in PCF$_{‖}$.*

*Sketch.* By rewriting means, one may establish that if it was definable in PCF$_{‖}$, then it would be definable just via parallel compositions of variables. However, such terms composed only of parallel compositions and variables are easily seen to yield series-parallel causal shapes; thus the example in Figure 12.10 is undefinable. □

For strategies on the game $!(&U) \vdash U$, it seems that we may get finite definability up to positive isomorphism by restricting globular strategies further to those that have a series-parallel causal shape. But for more complex datatypes, requiring a series-parallel causal shape is not enough to get back definability: an example phenomenon appears in
<figure><img src="image_227.png" /><figcaption>Figure 12.10: An undefinable strategy</figcaption></figure>

<figure><img src="image_228.png" /><figcaption>Figure 12.11: Dynamic causal shape</figcaption></figure>

Figure 12.11, where the structure of forking/merging threads is impacted by the values. Though we do not have a proof, it seems clear that this is undefinable: in a term as in

$$ \textbf{let} \left( \begin{array}{l} x_1 = M_1 \\ x_2 = M_2 \\ x_3 = M_3 \end{array} \right) \textbf{in } N $$

then the first move in N will depend on the values obtained for $x_1$, $x_2$ and $x_3$: there is no way to indicate that e.g. if $x_2$ is true, then N should not wait for $x_1$.

Altogether, we have not been able to characterise the globular strategies definable in PCF$_{‖}$. A natural option would be to reify the first-order globular strategies, i.e. to consider them as syntax and add a new syntactic construct for every first-order globular strategy. This seems interesting, because first-order globular strategies are indeed relevant from a computational point of view; however it seems hard to give then an appealing syntactic theory. Instead, we shall weaken our objective and only perform definability *up to positional equivalence* – which will suffice for our purposes<fnref n="3" />.

### 12.3.2 Positional First-Order Definability

Moving from positive isomorphism to positional equivalence is convenient, because positional equivalence may not respect the evaluation order. This lets us construct a purely sequential version of any finite globular first-order strategy.

From now on, fix a first-order finite globular strategy $\alpha : !(&\mathcal{X}_i) \vdash \mathcal{X}$.

**Necessary primary question.** Once prompted, $\alpha$ may launch many computations in parallel, via *minimal primary questions* (i.e. that only depend on the Opponent initial

<footnote n="3">³Of course, the factorization result of Corollary 12.2.18 is already up to positional equivalence, but this is mostly for convenience: factorization should hold up to positive isomorphism.</footnote>
question). The idea is that our sequential definability procedure will choose any of those
(the choice does not matter up to positional equivalence), and evaluate it first. However,
we must show that all these primary questions are actually *necessary*, in the sense that
any stopping configuration necessarily includes this primary question, answered.

**Lemma 12.3.2.** Consider $\alpha \in \text{→-Glob}(\&X_i, \mathcal{X})$ finite globular.

Then for each minimal primary question $q$ and $x \in \text{stop}(\alpha)$, we have $q \in x$.

*Proof.* Consider $x \in \text{stop}(\alpha)$ and seeking a contradiction, assume $q \notin x$. By *causal determinism*, $q$ is compatible with $x$. Consider $t \in \mathcal{L}(x)$ any linearization of $x$, yielding

$$s = (\cdot)(\partial_{\Lambda(\alpha)}(t)) \in \mathcal{O}-\text{Unf}(\alpha),$$

it is straightforward that it is (logically) well-bracketed. Now, $\alpha$ is a morphism in $\text{→-Strat}$, and must thus be well-bracketed in the sense of Definition 9.3.2. Therefore,

$$sa^+ = (\cdot)(\partial_{\Lambda(\alpha)}(tq)) \in \mathcal{O}-\text{Unf}(\alpha)$$

should be (logically) well-bracketed. But it is not, since $q$ points to the initial Opponent question which must already be answered in $x$: a contradiction, thus $q \in x$. $\square$

Thus we may safely begin the sequentialization with any minimal primary question: by this lemma, we know that it will appear in all stopping configurations.

**Residual.** Choose $q \in \mathcal{Q}_{i_0}$ minimal. As $q$ appears in every stopping configuration, it is safe to first make a call to $x_{i_0}$, then branch on the possible return values. Since $\alpha$ is finite, there is a finite set $V$ of values leading to an observable result. Now, for each $v \in V$, we define $\alpha_{(qv)}$ the *residual* of $\alpha$ after $q$ yields value $v$; and then proceed inductively. To define this residual, our first step is to rename $\alpha$ to isolate this first call:

**Lemma 12.3.3.** There is $\alpha_{(q)} \in \text{→-Glob}((\&X_i)\&X_{i_0}, X)$ with the same ess as $\alpha$ and differing only via its display map, such that:

(1) for $x \vdash w \in (\alpha_{(q)})$, then $x = x' + [(i_0, v)]$ such that $x' + [(i_0, v)] \vdash w \in (\alpha)$,

(2) for $x \vdash w \in (\alpha)$, then $x = x' + [(i_0, v)]$ such that $x' + [(n+1, v)] \vdash w \in (\alpha_{(q)})$.

*Proof.* The strategy $\alpha_{(q)}$ has the same components as $\alpha$, with display map sending $q$ and its answers to the new component. The characterisation of positions is direct. $\square$

Note that in the second clause, the decomposition $x = x' + [(i_0, v)]$ is not unique: there may be several values in component $i$, but one of them yields a position of $\alpha_{(q)}$.

We set the residual $\alpha_{(qv)}$ as $\alpha_{(qv)} = \alpha_{(q)} \circ_1 \langle \text{der}_{\&X_i}, v \rangle : !((\&X_i) \vdash X) \text{ writing } v : !((\&X_i) \vdash X_{i_0}) \text{ the constant strategy. In order to characterize its positions, we note:}$

**Lemma 12.3.4.** For any $v \in V$, the positions of $\langle \text{der}_{\&X_i}, v \rangle!$ are exactly of the form

$$x \vdash x + p \cdot [(n+1, v)] \in (\!((\&X_i) \vdash \!((\&X_i)\&X_{i_0})),$$

where $p \cdot [(n+1, v)]$ denotes the $p$-fold sum, and for any $x \in (\!((\&X_i)))$ and $p \in \mathbb{N}$.
*Proof.* Straightforward verification.

☐

Using this lemma, we link the positions of $\alpha$ and $\alpha_{(qv)}$.

**Lemma 12.3.5.** *Consider positions $x \in (\mathfrak{f}(\mathbf{X}_i))$ and $w \in (\mathbf{X})$. Then, $x \vdash w \in (\alpha)$ iff $x' + [(i_0, v)] \text{ with } x' \vdash w \in (\alpha_{(qv)})$.*

*Proof.* By definition, we have $\alpha_{(qv)} = \alpha_{(q)} \odot (\mathrm{der}_{\&\mathbf{X}_i}, v)^1$, so by Corollary 10.4.15,

$$ (\alpha_{(qv)}) = ((\alpha_{(q)})) \odot (\langle \mathrm{der}_{\&\mathbf{X}_i}, v \rangle^1). $$

The lemma directly follows by Lemmas 12.3.3 and 12.3.4.

☐

**Reconstruction.** We now rebuild a term. We have $\alpha_{(qv)}$ a globular finite strategy with size strictly lesser than that of $\alpha$. By induction hypothesis, there is a term

$$ x_1 : \mathcal{X}_1, \dots, x_n : \mathcal{X}_n \vdash N_{(qv)} : \mathcal{X}_{i_0}, $$

for each $v \in V$, such that $[N_{(qv)}] = \alpha_{(qv)}$. We set $x_1 : \mathcal{X}_1, \dots, x_n : \mathcal{X}_n \vdash M : \mathcal{X}$ as

$$
\begin{array}{lclcl}
\textbf{case } x_{i_0} & \textbf{of} & & & \\
v_1 \mapsto N_{(qv_1)} & & \textbf{let } x = x_{i_0} & \textbf{in} & \\
& & & & \textbf{if } x = \mathcal{X} \ v_1 \ \textbf{then } N_{(qv_1)} \\
v_2 \mapsto N_{(qv_2)} & \stackrel{\text{def}}{=} & & & \textbf{else if } x = \mathcal{X} \ v_2 \ \textbf{then } N_{(qv_2)} \\
\multicolumn{5}{l}{\text{...}} \\
v_p \mapsto N_{(qv_p)} & & & & \textbf{else if } x = \mathcal{X} \ v_p \ \textbf{then } N_{(qv_p)} \\
& & & & \textbf{else } \perp
\end{array}
$$

where $V = \{v_1, \dots, v_p\}$, using the syntactic sugar introduced in Section 2.2.3. Write

$$ x_1 : \mathcal{X}_1, \dots, x_n : \mathcal{X}_n, x : \mathcal{X}_i \vdash M' : \mathcal{X} $$

for the iterated if statement, i.e. $M$ is **let $x = x_{i_0}$ in $M'$**.

**Analysis.** It remains to analyze the positions of $[[M]]$ and $[[M']]$ to show that $[[M]] = \alpha$ as required. We start by an analysis of the positions of $[[M']]$.

**Lemma 12.3.6.** *Consider positions $x \in (\mathfrak{f}(\mathbf{X}_i))$ and $w \in (\mathbf{X})$. Then, $x \vdash w \in (\llbracket N_{(qv)} \rrbracket)$ iff there is $p \in \mathbb{N}$ such that $x+p \cdot [(n+1, v)] \vdash w \in (\llbracket M' \rrbracket)$.*

*Proof.* It is a direct verification, amounting to the correctness of our definition for equality test and the usual laws for conditionals, that for any $v \in V$ we have $[[M']] \odot_! (\mathrm{der}, v) = [[N_{(qv)}]]$. The claim then follows by Corollary 10.4.15 and Lemma 12.3.4. ☐

☐

It remains to take the interpretation of the **let** construction into account. Recall that

$$ [[M]] = \mathrm{let}_{\mathbf{X}_{i_0}, \mathbf{X}} \odot_! \langle \pi_{i_0}, \Lambda^1(\llbracket M' \rrbracket) \rangle : \mathfrak{f}(\mathbf{X}_i) \vdash \mathbf{X} $$

where $\mathrm{let}_{\mathbf{X}_{i_0}, \mathbf{X}} : \mathfrak{f}(\mathbf{X}_i) \& (\mathfrak{f}(\mathbf{X}_i \to \mathbf{X})) \vdash \mathbf{X}$. The positions of $\mathrm{let}_{\mathbf{X}_{i_0}, \mathbf{X}}$ are as follows:
**Lemma 12.3.7.** The positions of $\text{let}_{\mathbf{X}_{i_0}, \mathbf{X}}$ are exactly those of the form

$$[(1, v)] + [(2, ((p \cdot [v]) \to w))] \vdash w \in ((!(\mathbf{X}_{i_0}) \& (!\mathbf{X}_i \to \mathbf{X})) \vdash \mathbf{X})]$$

for $v \in (\mathbf{X}_{i_0})$, $w \in (\mathbf{X})$, and $p \in \mathbb{N}$.

*Proof.* A direct analysis of positions reached by stopping configurations of $\text{let}_{\mathbf{X}_{i_0}, \mathbf{X}}$. $\square$

We can now wrap up, showing that $[[M]]$ has the same non-empty positions as $\alpha$.

**Lemma 12.3.8.** Consider $x \in (\&\mathbf{X}_i)$ and $w \in (\mathbf{X})$.

Then, $x \vdash w \in ([M])$ iff $x = x' + [(i_0, v)]$ with $x' \vdash w \in ([N_{(qv)})]$.

*Proof.* By Lemmas 12.3.6 and 12.3.7. $\square$

Note that this exactly matches the characterisation of positions of $\alpha$ in Lemma 12.3.5. As $\alpha_{(qv)} \equiv [[N_{(qv)}]]$ by induction hypothesis, it follows that $[[M]] \equiv \alpha$. Summing up, we have proved finite first-order definability up to positional equivalence:

**Theorem 12.3.9.** For $\alpha \in \rightarrow\text{-Glob}((\&\mathbf{X}_i), \mathbf{X})$ finite, there is

$$x_1 : \mathcal{X}_1, \dots, x_n : \mathcal{X}_n \vdash \mathbf{M} : \mathcal{X}$$

a term of PCF (not using parallel evaluation) such that $[[M]] \equiv \alpha$.

### 12.3.3 Finite Globular Definability

We may now conclude the proof of finite definability.

**Theorem 12.3.10.** Let $\Gamma \vdash A$ be a PCF typing judgment, $\alpha \in \rightarrow\text{-Glob}([\Gamma], [[A]])$ finite.

Then, there is $\Gamma \vdash \mathbf{M} : A$ such that $[[M]] \equiv \alpha$.

*Proof.* Up to currying, $\alpha : !((\&A_i) \vdash \mathbf{X})$, writing $A_i = A_{i,1} \to \dots \to A_{i,p_i} \to \mathcal{X}_i$ for $1 \le i \le n$. We reason by induction on the size of $\alpha$. By Corollary 12.2.18,

$$\alpha \equiv \text{fo}(\alpha) \odot_1 \langle x_i, \alpha_{q,i}^* \dots \alpha_{q,p_i}^* | 1 \le i \le n, q \in \mathcal{Q}_i \rangle,$$

with each $\mathcal{Q}_i$ finite, and for $1 \le i \le n$, $q \in \mathcal{Q}_i$ and $1 \le j \le p_i$, $\alpha_{q,j}^* : !((\&A_i) \vdash A_{i,j})$ a globular finite strategy of size strictly smaller than $\alpha$. By induction hypothesis, there is

$$x_1 : A_1, \dots, x_n : A_n \vdash N_{q,j} : A_{i,j}$$

s.t. $[[N_{q,j}] \equiv \alpha_{q,j}$. Let us write $\mathcal{Q}_i = \{q_{i,1}, \dots, q_{i,k_i}\}$. By Theorem 12.3.9 there is

$$x_{q_{1,1}} : \mathcal{X}_1, \dots, x_{q_{1,k_1}} : \mathcal{X}_1, \dots, x_{q_{n,1}} : \mathcal{X}_n, \dots, x_{q_{n,k_n}} : \mathcal{X}_n \vdash \mathbf{M}_{fo} : \mathcal{X}$$

such that $[[\mathbf{M}_{fo}] \equiv \text{fo}(\alpha)$. Then, we define the term $x_1 : A_1, \dots, x_n : A_n \vdash \mathbf{M} : \mathcal{X}$ as

$$x_1 : A_1, \dots, x_n : A_n \vdash \mathbf{M}_{fo}[x_i N_{q_{i,l},1} \dots N_{q_{i,l},p_i} / x_{q_{i,l}}] : \mathcal{X}.$$
Then we may finally compute

$$
\begin{align*}
[\mathcal{M}] &= [M_{fo}] \circ_! \langle [x_i N_{q_{i,l},1} \dots N_{q_{l,l},p_i}] | 1 \le i \le n, q_{i,l} \in \mathbb{Q}_i \rangle \\
&\equiv [M_{fo}] \circ_! \langle x_i [N_{q,1}] \dots [N_{q,n}] | 1 \le i \le n, q \in \mathbb{Q}_i \rangle \\
&\equiv fo(\alpha) \circ_! \langle x_i \alpha_{q,1}^* \dots \alpha_{q,p_i}^* | 1 \le i \le n, q \in \mathbb{Q}_i \rangle
\end{align*}
$$

using the substitution lemma for cartesian closed categories, properties of the internal language, the properties of $M_{fo}$ and $N_{q,j}$ and that $\equiv$ is a congruence. $\square$

12.3.4 Intensional Full Abstraction

We may now prove our final full abstraction result:

**Theorem 12.3.11.** The model $\dashrightarrow$-Glob is intensionally fully abstract for PCF$_{‖}$.

*Proof.* Consider $\vdash M, N : A$ such that $M \simeq N$, and assume that $[M] \not\subseteq [N]$, i.e. there is a test $\alpha \in \dashrightarrow$-Glob($[A]$, $[\Upsilon]$) such that, w.l.o.g., $\alpha \circ_! [M] \Downarrow$ and $\alpha \circ_! [N] \Uparrow$.

By Corollary 12.1.23, we assume $\alpha$ is additionally finite. By Theorem 12.3.9, there is a term $x : A \vdash T : \bigcup$ such that $[T] \equiv \alpha$. Defining the context $C[-] = (\lambda x^A. T)[-]$, it follows from the laws of cartesian closed categories that

$$
[C[M]] = [(\lambda x^A.T) M] \approx [T[M/x]] \approx [T] \circ_! [M] \equiv \alpha \circ_! [M] \Downarrow,
$$

and $[C[N]] \equiv \text{comp}(\alpha) \circ_! [N]$. By Theorem 9.1.5, $C[M] \Downarrow$. By hypothesis $M \simeq N$, so $C[N] \Downarrow$. By Theorem 9.1.5 again, $[C[N]] \Downarrow$, hence $\alpha \circ_! [N] \Downarrow$, contradiction. $\square$

Summing up, in Part III we have constructed a cartesian closed $\sim$-category $\dashrightarrow$-Strat.
We have defined two conditions on morphisms of $\dashrightarrow$-Strat, sequentiality and globu-
larity, forming three sub-cartesian closed $\sim$-categories of $\dashrightarrow$-Strat: $\dashrightarrow$-Seq, $\dashrightarrow$-Glob
and $\dashrightarrow$-SeqGlob. We established four intensional full abstraction results

<table>
  <tbody>
    <tr>
      <td>dashrightarrow-Strat</td>
      <td>is fully abstract for</td>
      <td>IA<sub>‖</sub></td>
      <td>(Th. 9.3.10)</td>
    </tr>
    <tr>
      <td>dashrightarrow-Strat + sequentiality</td>
      <td>is fully abstract for</td>
      <td>IA</td>
      <td>(Th. 11.2.21)</td>
    </tr>
    <tr>
      <td>dashrightarrow-Strat + globularity + sequentiality</td>
      <td>is fully abstract for</td>
      <td>PCF</td>
      <td>(Th. 11.3.12)</td>
    </tr>
    <tr>
      <td>dashrightarrow-Strat + globularity</td>
      <td>is fully abstract for</td>
      <td>PCF<sub>‖</sub></td>
      <td>(Th. 12.3.11)</td>
    </tr>
  </tbody>
</table>

therefore achieving our objective to disentangle parallelism and state. A significant part
of this consisted in establishing interpretation-preserving cartesian closed $\sim$-functors

$\mathcal{O}$-Unf : $\dashrightarrow$-Strat $\rightarrow$ $\mathcal{O}$-Strat (Theorem 9.3.8)

$\downarrow\uparrow$-Unf : $\dashrightarrow$-Seq $\rightarrow$ $\downarrow\uparrow$-Strat (Theorem 11.2.18)

$\downarrow\uparrow$-Unf : $\dashrightarrow$-SeqGlob $\rightarrow$ $\downarrow\uparrow$-Inn (Theorem 11.3.7)

(-) : $\dashrightarrow$-Glob $\rightarrow$ Rel<sub>i</sub> (Corollary 10.4.15)

to previously established models of different nature, which altogether, or so we hope,
substantiates our claim that *thin concurrent games* can play a valuable role at the inter-
face of many denotational semantics of programming languages.
Part IV

**Other Developments and
Openings**
# Introduction to Part IV

<figure><img src="image_229.png" /><figcaption>Figure 12.12: Concurrent strategies want cycles too!</figcaption></figure>

In this final part, we conclude the monograph by providing some larger perspective on the landscape of concurrent games. First, in Chapter 13, we shall give a synthesis of a lot of the work done in concurrent games that could not be presented in this document. Then, in Chapter 14 we give some conclusions: we ask to what extent the work done so far substantiates the view evoked in the introduction, of concurrent games as a bridge between interactive semantics. We also then present a few open problems raised in the present development, and conclude with some perspectives.
# Chapter 13

## Further Work

In this monograph so far, we have given a detailed, technical account of what we consider to be the core results and developments in the theory of (thin) concurrent games. But this is not the full story; and though this monograph is already intimidating lengthy, we feel like a survey of the further work accomplished is called for. We show in Figure 13.1 all the works accounted for in this monograph, either in the main technical content or in this survey, grouped by themes and along with the (technical, rather than in terms of mere inspiration) dependencies between them.

This is not intended to be an exhaustive survey of concurrent games, but only of the lines of work that I have been leading. There are other interesting developments in concurrent games in which I did not participate; or for which my participation was minor; or that feel too loosely connected from the main thrust of the present document.

### 13.1 Effects and Concurrency

This section summarises work that was mostly developed in close collaboration with Simon Castellan, during his PhD thesis (2014-2017).

In 2015, our paper introducing TCG, our concept of parallel innocence, and our full abstraction result for parallel evaluation of PCF, was published [Castellan et al., 2015]. At that time, it felt ironic and a little embarassing that we had something called *concurrent games* and yet had not developed semantics for actual concurrent effects.

It was very clear for us at the time how to interpret IA$_{\parallel}$ in TCG, but for a while, what was not clear was which theorem to prove! In the denotational semantics literature, the gold standard is full abstraction. We were confident that we could inherit intensional full abstraction by linearizing our model to [Ghica and Murawski, 2008] (though the details of this were not actually written up before this monograph – and they did require some care), but it felt unsatisfactory to only reprove an old result, and at that, one that
<figure><img src="image_230.png" /><figcaption>Figure 13.1: The event structure of contributions in concurrent games</figcaption></figure>
does not actually need the causal information. So what is the right nail, for a hammer whose specialty is to uncover structure that by nature is *not* observable?

### 13.1.1 Non-canonical causal presentation

The mainstream approach, in formalizing the execution of concurrent systems, is by interleaving the executions of its sequential components – this is the approach followed by Ghica and Murawski's fully abstract model for IA$_{‖}$ [Ghica and Murawski, 2008].

But considering a concurrent system formed of *n* sequential processes

$$P_1 \parallel \cdots \parallel P_n,$$

even if each $P_i$ performs only *one* atomic action, this induces $n!$ different executions: this is the *state explosion problem*, one of the main challenges to the algorithmic verification of concurrent systems. In contrast, the *truly concurrent* approach followed by concurrent games avoids interleavings and proposes a more compact representation of executions, that may in principle be helpful for algorithmic verification.

This makes concurrent games seem promising as a basis for an observational equivalence checker for IA$_{‖}$, especially in the light of Ghica and Murawski's full abstraction result [Ghica and Murawski, 2008] and the topic of *algorithmic game semantics* [Ghica and McCusker, 2003]. More precisely, the hope was to formalize the intuition that non-alternating strategies in the sense of $\mathcal{O}$-**Strat** already had an implicit causal structure, i.e. that a non-alternating strategy interpreting a term *M* was simply

$$[M] = \mathcal{O}\text{-Unf}(\sigma_M)$$

for $\sigma_M$ a **canonical causal explanation** for $[M]$, a compact representation of the interleavings that may be used instead of the interleavings for algorithmic purposes.

In [Castellan and Clairambault, 2016] we showed that this was *not* the case, already in the affine case. We first built a concurrent games model of an affine version of IA$_{‖}$, a corresponding non-alternating model, and an interpretation-preserving functor from the causal to the interleaving model. Then we showed that a non-alternating strategy could have *distinct* and *incomparable minimal* causal explanations – additionally, we proved this already happens within the interpretation of affine IA$_{‖}$: there are two affine programs with incomparable *causal* behaviour that have the same non-alternating unfolding. This phenomenon is illustrated in Figure 13.2.

This does not show that concurrent games *cannot* help for checking the equivalence of higher-order concurrent programs, it only points out a fundamental obstacle to the route we had in mind. It is also a hint that the value of concurrent games is in its presentation of the *intensional behaviour*, not as an efficient way to present the interleavings. Thus, we then refocused our research on the intensional behaviour.

### 13.1.2 Non-angelic concurrent games

Another aspect of concurrent games that was clear from the start is that they record explicitly the point of non-deterministic branching. For instance, the program $x: \bigcup T$
<figure><img src="image_231.png" /><figcaption>Figure 13.2: As the goal is only to reconstruct interleavings, the branching structure does not matter, so rather than an event structure we can work only with a set of augmentations, i.e. the partial orders induced by configurations. In this example, both the second and the third augmentation can be removed without changing the interleavings – but no other; yielding two incompatible minimal causal explanations.</figcaption></figure>

<figure><img src="image_232.png" /><figcaption>Figure 13.3: Recording non-angelic behaviour</figcaption></figure>

<figure><img src="image_233.png" /><figcaption>Figure 13.4: After hiding</figcaption></figure>

<figure><img src="image_234.png" /><figcaption>Figure 13.5: Composition with essential events</figcaption></figure>

**if choice then** $x$; $\bot$ **else** $x$; $\checkmark$: $U$ yields the strategy of Figure 13.3, tracking explicitly the two incompatible calls to $x$ and the fact that one yields to a divergence, while the other yields termination. In most earlier games models (with the notable exception of [Harmer and McCusker, 1999] for Erratic IA), the diverging branch would be ignored: this is a direct consequence of the traditional methodology of representing a program as a *set of plays*, i.e. a set of converging behaviour. We only record the converging behaviour, forgetting the non-deterministic branching information, leading to an *angelic* view of termination, i.e. may-convergence.

This discussion might lead the reader to expect that concurrent games are sound with respect to must-convergence, but that is not the case: *hiding* removes branches that do not prompt any visible behaviour, even if they witness possible non-deterministic branches. For instance, composing the strategy of Figure 13.3 with **skip** yields the interaction of Figure 13.4 which, after hiding, yields the constant strategy $\llbracket$**skip**$\rrbracket$ – because of hiding, we forget that something may have gone wrong in the computation.

Nevertheless, in [Castellan et al., 2018a], we proved that concurrent games are easily amended so as to recall more than angelic information on program behaviour. It is simply a matter of changing *hiding*, so that we retain events that are part of a minimal conflict: those are kept through hiding as events of neutral polarity, dubbed *essential*
*events.* With this modification, the composition above yields the strategy of Figure 13.5 where the events labelled ⋆ are those essential events. With this interpretation, we keep more than angelic information: in fact, we show that (the transition system generated by) the strategy is weakly bisimilary to (the transition system generated by) the operational semantics, for an affine version of IA<sub>⋆</sub>. We are not aware of any other work capturing by denotational means such a precise information on program behaviour.

This felt a rather good illustration of the expressivity of concurrent games, and in particular of its feature that it retains the non-deterministic branching information. But, weak bisimulation does not really take causality into account.

### 13.1.3 Resource-tracking concurrent games

This is a collaboration with Aurore Alcolei during her PhD thesis, and Olivier Laurent.

To explore the expressiveness of causality in concurrent games, we needed to record information about programs that really depends on the causal independence between events, and is incompatible with an interleaving interpretation. As a natural objective, we thought of the following problem. Consider IA<sub>⋆</sub> extended with a primitive wait(n) that takes a natural number n, and waits for n seconds. The program

$$ \vdash \mathbf{newref} r \text{ in let} \quad \left( \begin{array}{l} x = \mathbf{wait}(1); r := 1; \mathbf{wait}(2) \\ y = \mathbf{wait}(2); r := 2; \mathbf{wait}(1) \end{array} \right) \quad \mathbf{in} !r : \mathbb{N} $$

always evaluates in 6 seconds according to an interleaving operational semantics, as all the wait instructions must be handled before termination. But running this program on a multicore architecture, one will observe faster termination times: the program should evaluate to 2 in about 3 seconds, but – if the thread for x gets stuck – we can in principle observe a termination to 1 in at least 4 seconds. This can be captured operationally via a semantics where threads can wait in parallel, but it seems hard to capture denotationally as one must be able to see when parts of the computation are causally independent.

Investigating this question, we had two main inspirations: firstly [Ghica, 2005], where Ghica builds a variant of ⊠-Strat to capture semantically the (interleaving) execution time for an IA<sub>⋆</sub>-like language; and secondly [Laird et al., 2013], where the authors use the relational model weighted over the tropical or arctic semirings to capture resource usage for a PCF-like language extended with non-deterministic choice.

In [Alcolei et al., 2019] we introduce a version of concurrent games parametrized by an algebraic structure we call a resource bimonoid, that tracks resource consumption sequentially and in parallel – our main example is $\mathbb{R}_+$ for time, equipped with + (for sequential resource consumption) and max (for parallel resource consumption). In this model, strategies track resource consumption: each positive move comes equipped with an expression describing the resource usage necessary to play this move, as a function of the resources used to reach its causal dependencies. Building on this, we give (among other results) an interpretation of an affine IA<sub>⋆</sub>-like language extended with wait, correctly predicting execution time in a maximally parallel evaluation model. This is illustrated in Figure 13.6, that shows the interaction yielding the interpretation of the program above, where each event is annotated by its minimal time of appearance.
<figure><img src="image_235.png" /><figcaption>Figure 13.6: Predicting minimal parallel evaluation time</figcaption></figure>

This is neat as it is an application that really exploits the causal information available in concurrent games. It is also the first occurrence of a trend that we followed next: the enriching of concurrent games with quantitative information.

## 13.2 Quantitative Concurrent Games

This section summarizes work developed in collaboration with Hugo Paquet and Glynn Winskel, as part of Hugo Paquet’s PhD thesis<fnref n="1" />; and – regarding the work on semantics of quantum programming – as part of Marc de Visme’s PhD thesis (2017-2020).

The original motivation for this line of work was two-fold. The first was an intriguing gap in the literature, originally investigated by Hugo during a research internship at IRIF with Christine Tasson. There were two fully abstract models for fairly close probabilistic languages: probabilistic game semantics [Danos and Harmer, 2000] for probabilistic IA, and the weighted relational model [Laird et al., 2013] for probabilistic PCF. While these models were fairly close in spirit, it was very unclear how to actually relate them formally. Could we have a time-forgetting map from games to weighted relations? From reading Melliès’ papers on asynchronous games [Melliès, 2005], it was clear to me that the source of such a time-forgetting map should not be Danos and

<footnote n="1">¹Hugo did his PhD in Cambridge with Glynn Winskel, defended in 2019, but I spent most of the year 2016 in Cambridge, and a lot of that work was carried out during that time.</footnote>
Harmer's model, but rather a concurrent games version, for reasons similar to those that make the relational collapse of Section 10.4 tick.

The second motivation was to give a notion of probabilistic innocence, i.e. to capture the interactive behaviour of pure parallel programs. It had been known for long that the naive theory of non-deterministic innocence does not work in sequential game semantics [Harmer, 1999]; and it seemed that such a theory could be obtained in probabilistic concurrent games thanks to their explicit handling of the branching information<fnref n="2" />.

In both cases, this seemed to be problems where concurrent games were naturally helpful, so we embarked in our journey in probabilistic concurrent games.

### 13.2.1 Probabilistic PCF

When we started working on this, there was already a notion of probabilistic concurrent strategy, due to Glynn [Winskel, 2013a], which we first review.

The initial idea is simple: a probabilistic concurrent strategy is a strategy $\sigma$ with

$$v_{\sigma} : \mathcal{C}(\sigma) \to [0, 1]$$

a probability valuation that expresses the probabilistic weight of the Player choices made so far. So for instance, a strategy for a fair random boolean would have

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

with $v(\emptyset) = 1$, $v(\{\mathbf{q}^{-}\}) = 1$, $v(\{\mathbf{q}^{-}, \mathbf{t}^{+}\}) = v(\{\mathbf{q}^{-}, \mathbf{f}^{+}\}) = \frac{1}{2}$ – playing Opponent moves has no impact on the probability valuation as only the weight of the Player choices is tracked (this is similar to the approach in [Danos and Harmer, 2000]).

Glynn's probabilistic strategies must satisfy additional conditions. The easy ones are

normalized: $v(\emptyset) = 1$,

receptive: if $x^{\sigma} \subseteq \mathbf{y}^{\sigma}$, then $v(x^{\sigma}) = v(y^{\sigma})$,

but there is more. If from a configuration $x^{\sigma} \in \mathcal{C}(\sigma)$, $\sigma$ can do two events $s_{1}^{+}$ and $s_{2}^{+}$ which are additionally conflicting, then we expect to have the inequality

$$\frac{v(x^{\sigma} \cup \{s_{1}^{+}\})}{v(x^{\sigma})} + \frac{v(x^{\sigma} \cup \{s_{2}^{+}\})}{v(x^{\sigma})} \le 1 :$$

the first term of the sum is the probability of playing $s_{1}^{+}$ in configuration $x^{\sigma}$, the second is the probability of playing $s_{2}^{+}$ in configuration $x^{\sigma}$; the condition amounts to asking that those form a sub-probability distribution – note the same condition can be written

$$v(x^{\sigma}) \ge v(x^{\sigma} \cup \{s_{1}^{+}\}) + v(x^{\sigma} \cup \{s_{2}^{+}\}).$$

<footnote n="2">²Other works had already arrived at notions of non-deterministic innocence via adopting strategies with explicit branching structure [Castellan et al., 2014, Tsukada and Ong, 2015].</footnote>
In sequential probabilistic game semantics [Danos and Harmer, 2000], a similar condition suffices. But the soundness of this relies on the conflict between $s_1^+$ and $s_2^+$, so that $x^\sigma \cup \{s_1^+\}$ and $x^\sigma \cup \{s_2^+\}$ delineate two disjoint parts of the probability space. In concurrent games it is possible that $x^\sigma \cup \{s_1^+, s_2^+\}$ is also a configuration, which is accounted for twice in the sum above. Correcting for this yields the inequality

$$v(x^\sigma) \ge v(x^\sigma \cup \{s_1^+\}) + v(x^\sigma \cup \{s_2^+\}) - v(x^\sigma \cup \{s_1^+, s_2^+\}),$$

but a similar phenomenon occurs for three concurrent events, in which case

$$v(x^\sigma) \ge v(x^\sigma \cup \{s_1^+\}) + v(x^\sigma \cup \{s_2^+\}) + v(x^\sigma \cup \{s_3^+\}) \\ -v(x^\sigma \cup \{s_1^+, s_2^+\}) - v(x^\sigma \cup \{s_1^+, s_3^+\}) - v(x^\sigma \cup \{s_2^+, s_3^+\}) \\ +v(x^\sigma \cup \{s_1^+, s_2^+, s_3^+\}),$$

and the general formula can be written following the *inclusion-exclusion principle* – Glynn called this the *drop condition* as it requires that a quantity, the “drop” obtained as the left hand side term minus the right hand side term, should be positive.

Note that by *receptive*, it suffices to assign probability valuations to +-covered configurations. This makes the compositional structure of probabilistic strategies very easy:

$$v_{\tau \odot \sigma}(x^{\tau} \odot x^{\sigma}) = v_{\sigma}(x^{\sigma}) \cdot v_{\tau}(x^{\tau}) \quad (13.1)$$

for all $x^{\tau} \odot x^{\sigma} \in \mathscr{C}^{+}(\tau \odot \sigma)$; and $v_{\omega_A}(\omega_x) = 1$ for all $x \in \mathscr{C}(A)$. Probabilistic strategies directly inherit from **CG** the structure of a bicategory (the only difficulty being composition of the drop condition). But it is “only” a bicategory, and we needed much more in order to interpret **PCF**, so our first task was to merge this with **TCG**.

In doing that, we had the good surprise to find that this needed almost no work at all! In dealing with symmetry, the only condition that must be added to strategies is

$$\textit{invariance:} \quad \text{for all } x^\sigma \cong_\sigma y^\sigma, \text{ we have } v_\sigma(x^\sigma) = v_\sigma(y^\sigma)$$

ensuring that the probability valuation is invariant under symmetry – the drop condition, for instance, remained unchanged<fnref n="3" />, forming a relative Seely category that we shall refer to as **ProbNTCG** in the context of this monograph. Then, the same constructions used to model **PCF** and reported in Chapter 8 work just as well to give a model of probabilistic **PCF** – this was the starting point of the paper [Castellan et al., 2018b].

**Probabilistic innocence.** Then in that situation, we looked for a notion of *probabilistic innocence* – note that we are talking about *sequential probabilistic innocence*, as it is already unclear what is parallel *non-deterministic innocence*, see Section 14.2.1. Hence we could build on the sequential non-deterministic innocence of [Castellan et al., 2014]:

**Definition 13.2.1.** A strategy $\sigma$ on board A is non-deterministic sequential innocent if:

negative: for all $s \in \min(\sigma)$, $\text{pol}_\sigma(s) = -$,
forestial: if $s_1, s_2 \le_\sigma s$, then $s_1 \le_\sigma s_2$ or $s_2 \le_\sigma s_2$,
locally conflicting: if $s_1 \rightsquigarrow_\sigma s_2$, then $[s_1)_\sigma = [s_2)_\sigma$,
locally sequential: if $s^- \to_\sigma s_1^+, s_2^+$, then $s_1^+ \rightsquigarrow_\sigma s_2^+$.

<footnote n="3">³Note in passing the nightmare avoided by using *thin* concurrent games instead of the *saturated* concurrent games of [Castellan et al., 2014]! See Section 7.1.2 for a reminder on the thin / saturated distinction.</footnote>
This takes as a definition the forestial shape that was derived in this monograph from combined sequentiality and parallel innocence (see Lemma 11.3.2); with the difference that the resulting forest might not be O-branching: Player is now also able to branch. But that Player branching cannot be parallel branching, it must come with a conflict. Thus any configuration is an O-branching forest, where each branch is an independent exploration of a branch of the term, following the intuitions of Section 11.3.1.

Now for a *probabilistic strategy*, how should the probabilistic weight behave with respect to this forestial structure? What we proposed in [Castellan et al., 2018b] is that on top of non-deterministic sequential innocence, we should have

**Definition 13.2.2.** Consider $\sigma$: A probabilistic, non-deterministic seq. innocent. It is probabilistic innocent iff for all $x, y \in \mathscr{C}(\sigma)$ such that $x \cup y \in \mathscr{C}(\sigma)$,

$$v_{\sigma}(x \cup y) = \frac{v_{\sigma}(x) \cdot v_{\sigma}(y)}{v_{\sigma}(x \cap y)}.$$

This asserts that two *causally independent* branches of a configuration must also be *probabilistically independent*: the extensions $x \cap y \subseteq x$ and $x \cap y \subseteq y$ must explore distinct branches of the syntax tree, and hence trigger independent probabilistic choices.

Probabilistic innocent strategies form a relative Seely category that supports the interpretation of probabilistic PCF, and enjoy a finite definability result yielding intensional full abstraction for probabilistic PCF. But probabilistic PCF has a simpler, actually fully abstract model: probabilistic coherence spaces [Ehrhard et al., 2018] and hence their backbone, the weighted relational model [Laird et al., 2013].

Our paper had a second result, an interpretation-preserving collapse to the weighted relational model, but we shall come back to that in Section 13.3. In any case, there was clearly a parallel between concurrent games and relational models: just as relational models are made quantitative by attaching to each point of the “web” a coefficient, and concurrent games are made quantitative by attaching to each configuration a coefficient. But the relational supports more elaborate weights than just scalars: in particular, points of the web can be decorated by finite dimensional Hilbert spaces and completely positive maps, to obtain a computationally adequate model of the quantum $\lambda$-calculus [Pagani et al., 2014]. This suggested to do the same in concurrent games.

## 13.2.2 Quantum strategies

This is joint work with Marc de Visme for his PhD (2017-2020), and Glynn Winskel.

In Marc's PhD thesis, we set as main objective to build a computationally adequate concurrent games model for the quantum $\lambda$-calculus; this is a call-by-value language, linear but with an explicit exponential modality, structured via the types

$$A, B ::= \text{qubit} \mid \mathbf{1} \mid A \otimes B \mid A \oplus B \mid \text{list}(A) \mid A \to B \mid ! (A \to B),$$

with e.g. $\mathbb{B} = \mathbf{1} \oplus \mathbf{1}$ defined as syntactic sugar; linearity is of course crucial because qubits *cannot* be duplicated. Terms include the expected term formers for these types,
along with new primitives, used to manipulate quantum data:

$$ \mathbf{new} : \mathbb{B} \to \text{qubit}, \quad \mathbf{meas} : \text{qubit} \to \mathbb{B}, \quad \mathcal{U} : \text{qubit}^{\otimes n} \to \text{qubit}^{\otimes n}, $$

where **new** initializes a new qubit based on a boolean, **meas** measures a qubit (with a probabilistic result), and **U** imports any *n*-ary unitary inside the syntax.

Building a concurrent games model for this language posed several challenges. First of course, the language is call-by-value – while there were no earlier concurrent games models of call-by-value languages, it was not too difficult to infer what the corresponding structure should be, looking at traditional games models for call-by-value languages [Abramsky and McCusker, 1997, Honda and Yoshida, 1999] and from the game semantics of tensorial logic in e.g. [Melliès and Tabareau, 2007]. In particular, in contrast with **NTCG**, types (ignoring the quantum aspect) should be interpreted as *positive* games, where Player always starts. For instance, the type `1 → 1` yields the board

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

where computation starts by Player providing a value – in that written $\lambda^+$, as it carries the information that the program yields an abstraction. This enables Opponent to call the function by providing an argument which can only be the unique value of unit type, which in turn enables Player to terminate with again, the unique value of unit type.

The main challenge was dealing with quantum information. For this, our idea follows the paradigm to separate *quantum data* and *classical control*, putting together ideas from probabilistic concurrent games above, and quantum relational semantics [Pagani et al., 2014]. For *classical control*, qubits are interpreted just like the unit type, so that the plain event structure for qubit $\to$ qubit is exactly like `1 → 1` above. The difference comes with *quantum data*, for which each event $a \in A$ of the game comes labelled with a (finite dimensional) Hilbert space $\mathcal{H}_A(a)$. Events that do not carry any quantum state are annotated with the 1-dimensional Hilbert space, the unit for the tensor of Hilbert spaces, i.e. the complex numbers $C$. Events that do have a quantum content carry a non-trivial Hilbert space; for instance qubit $\to$ qubit becomes the game

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

with Hilbert space annotations in green. Intuitively, playing a move annotated with a Hilbert space *H*, has a side effect of opening *H* in the quantum register. Accordingly,
<figure><img src="image_239.png" /><figcaption>Figure 13.7: Quantum strategy for measurement</figcaption></figure>

any configuration $x \in \mathcal{C}(A)$ yields a finite dimensional Hilbert space

$$ \mathcal{Q}_A(x) = \bigotimes_{a \in x} \mathcal{Q}_A(a), $$

the tensor of the Hilbert spaces opened in $x$. Now the idea is that a strategy $\sigma: A$ is accompanied by a valuation as for probabilistic strategies, except it is *typed*: to each $x^\sigma \in \mathcal{C}(\sigma)$ we associate a *density operator* on the Hilbert space of moves played so far:

$$ v_{\sigma}(x^{\sigma}) \in \mathbf{DOp}(\mathcal{Q}_{A}(\partial_{\sigma} x^{\sigma})), $$

recall that density operators are the standard representation of *mixed quantum states*, i.e. supporting pure states but also convex (probabilistic) sums and measurements. Now, the definition of quantum strategies is analogous to that of probabilistic strategies, except that the valuations are *typed*: the *drop condition* can be defined, though it is with respect to the so-called *Löowner order* between density operators and involves some tracing out to bring all density operators to the same Hilbert space.

At the core of our approach, we use that for a strategy between games $\sigma: A \vdash B$, a quantum valuation on $A \vdash B$, i.e. a density operator on a tensor Hilbert space

$$ v_{\sigma}(x^{\sigma}) \in \mathbf{DOp}(\mathcal{Q}_{A}(x_{A}^{\sigma}) \otimes \mathcal{Q}_{B}(x_{B}^{\sigma})) $$

may be equivalently presented as a *completely positive map*, i.e. a morphism

$$ v_{\sigma}^{\rightarrow}(x^{\sigma}) \in \mathbf{CPM}(\mathcal{Q}_{A}(x_{A}^{\sigma}), \mathcal{Q}_{B}(x_{B}^{\sigma})), $$

in the compact closed category **CPM** that we shall not define here, but which should be thought of as taking mixed states on $\mathcal{Q}_A(x_A^\sigma)$ (so, certain operators on $\mathcal{Q}_A(x_A^\sigma)$ to mixed states on $\mathcal{Q}_B(x_B^\sigma)$. This lets us define the quantum valuation of the composition $\tau \odot \sigma$ simply by composition of the quantum valuations of $\sigma$ and $\tau$ respectively, via

$$ v_{\tau \odot \sigma}^{\rightarrow}(x^{\tau} \odot x^{\sigma}) = v_{\tau}^{\rightarrow}(x^{\tau}) \circ v_{\sigma}^{\rightarrow}(x^{\sigma}) $$

reminiscent of (13.1) for probabilistic strategies.

As an example, we show in Figure 13.7 the quantum strategies for measurement. Its control flow seems to select a boolean non-deterministically, but each branch is
weighted by the **CPM** map taking a density matrix on $\mathbb{C}^2$ and maps it to (a 1 by 1 matrix with) the probability of obtaining the corresponding value via a measurement.

With Marc and Glynn, we published a first paper [Clairambault et al., 2019] presenting the model; its main results are computational adequacy, but also an important consequence of the quantum *drop condition*: our quantum valuations can be presented as *superoperators*, those **CPM** maps that are trace non-increasing, they correspond to the physically realizable transformations on mixed quantum states. More precisely, consider $\sigma: A, x^\sigma \in \mathcal{C}(\sigma)$ and $\partial_\sigma x^\sigma = x_A$, and split $x_A$ into its positive and negative events $x_A = x_A^- \oplus x_A^+$. Then we may present equivalently $v_\sigma(x^\sigma)$ as

$$v_{\sigma}^{-+}(x^{\sigma}) \in \mathbf{CPM}(\mathcal{Q}_{A}(x_{A}^{-}), \mathcal{Q}_{A}(x_{A}^{+})),$$

which we show is always a superoperator. This was an improvement with respect to the earlier denotational model of the quantum $\lambda$-calculus [Pagani et al., 2014], for which there was no such boundedness property – their model construction required valuations to include an infinitary completion of **CPM**, just as the weighted relational model requires an infinitary completion of scalars to work around convergence issues.

In a second paper with Marc [Clairambault and de Visme, 2020], we were able to exploit this boundedness property to adapt in our model the proof method of Ehrhard, Pagani and Tasson for their full abstraction result of probabilistic coherence spaces for Probabilistic PCF [Ehrhard et al., 2018]. This shows that our model is fully abstract for the quantum $\lambda$-calculus, modulo a quotient of strategies that amounts to a quantitative relational collapse to the model of [Pagani et al., 2014], which entails that their model was already fully abstract. We cover the ideas around this quantitative collapse next.

## 13.3 Quantitative Relational Collapses

### 13.3.1 Counting witnesses and quantitative collapse

When working on [Castellan et al., 2018b], one of our goals was to understand the link between probabilistic alternating game semantics [Danos and Harmer, 2000] and probabilistic coherence spaces [Danos and Ehrhard, 2011] via the weighted relational model [Laird et al., 2013]; for that we meant to define an interpretation-preserving functor

$$(-) : \text{ProbNTCG-Vis} \to \bar{\mathbb{R}}_{+} \text{-Rel}$$

refining quantitatively the one of Corollary 10.4.15 – recall that here, $\bar{\mathbb{R}}_{+} \text{-Rel}$ is the weighted relational model [Laird et al., 2013], here weighted by the semiring $\bar{\mathbb{R}}_{+} = \bar{\mathbb{R}}_{+} \oplus \{+\infty\}$ of the completed positive reals. Its objects are sets, and morphisms from A to B are matrices $(\alpha_{a,b})_{a \in A, b \in B}$ where $\alpha_{a,b} \in \bar{\mathbb{R}}_{+}$ for all $a \in A$ and $b \in B$.

Composition of $\alpha \in \bar{\mathbb{R}}_{+} \text{-Rel}(A, B)$ and $\beta \in \bar{\mathbb{R}}_{+} \text{-Rel}(B, C)$ is matrix multiplication:

$$(\beta \circ \alpha)_{a,c} = \sum_{b \in B} \alpha_{a,b} \cdot \beta_{b,c}$$
which might not converge if $B$ is infinite – hence the completion to $\overline{\mathbb{R}}_+$.

At the time we were investigating this, it felt like it should be a minor variation of the usual relational collapse of Section 10.4. Recall that for $\sigma : A, \text{Definition 10.4.3 has}$

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

recording all $x_A \in (A)$ which is reachable in $\sigma$, which is witnessed by $x^\sigma \in \mathscr{C}^+(\sigma)$ such that $\partial_\sigma x^\sigma \in x_A$. Intuitively, instead of only recording the mere existence of such a witness, we must sum the weight of all possible witnesses. Of course that is too naive: as a strategy needs to be receptive to all Opponent reindexings, and as there are usually countably many of those, each “witness” in the sense above usually has countably many distinct but symmetric peers, yielding almost always infinitely many witnesses.

In [Castellan et al., 2018b], we proposed to solve this issue by summing not over all concrete witnesses as above, but over all symmetry classes of witnesses:

$$ (\sigma)_{x_A} = \sum_{x^\sigma \in \text{wit}^{\approx}_{\sigma}(x_A)} v_\sigma(x^\sigma) $$

for $\text{wit}^{\approx}_{\sigma}(x_A) = \{x^\sigma \in \mathscr{C}^+(\sigma) \mid \partial_\sigma x^\sigma\}$ using that by invariance, the valuation $v_\sigma$ lifts to symmetry classes. This yields a finite coefficient that operates as it should on simple examples. For composition, functoriality amount to proving the equality

$$ (\tau \odot \sigma)_{x_A \vdash x_C} = \sum_{x_B \in (B)} (\sigma)_{x_A \vdash x_B} \cdot (\tau)_{x_B \vdash x_C} $$

which seems like it should be a natural consequence of a bijection

$$ \text{wit}^{\approx}_{\tau \odot \sigma}(x_A \vdash x_C) \approx \sum_{x_B \in (B)} \text{wit}^{\approx}_{\sigma}(x_A \vdash x_B) \times \text{wit}^{\approx}_{\tau}(x_B \vdash x_C). \quad (13.2) $$

This seems simple enough: from $x^\sigma \in \text{wit}^{\approx}_{\sigma}(x_A \vdash x_B)$ and $x^\tau \in \text{wit}^{\approx}_{\tau}(x_B \vdash x_C)$, we can pick representatives $x^\sigma \in x^\sigma$, $x^\tau \in x^\tau$ and a symmetry $\theta_B : x^\sigma \approx_B x^\tau$, and obtain an element of $\text{wit}^{\approx}_{\tau \odot \sigma}(x_A \vdash x_C)$ as (the symmetry class of) $x^\tau \odot \theta_B x^\sigma$ defined following Definition 7.4.6. It can be checked that any $x \in \text{wit}^{\approx}_{\tau \odot \sigma}(x_A \vdash x_C)$ can be obtained in this ways, and that $x^\sigma \in \text{wit}^{\approx}_{\sigma}(x_A \vdash x_B)$ and $x^\tau \in \text{wit}^{\approx}_{\tau}(x_B \vdash x_C)$ can be uniquely recovered from $x$. So this bijection seemed to work just fine, as expected!

**Counting witnesses.** This is how the collapse was written in [Castellan et al., 2018b], and it was the state of my understanding for about two years. But later on, when writing the details of the quantum version of this collapse with Marc, we realized that something was off – the more typed version of the collapse made it more apparent.

The issue is that in the reasoning above, we have defined

$$ \text{wit}^{\approx}_{\sigma}(x_A \vdash x_B) \times \text{wit}^{\approx}_{\tau}(x_B \vdash x_C) \rightarrow \text{wit}^{\approx}_{\tau \odot \sigma}(x_A \vdash x_C) $$

a function by working on concrete representatives, and we had not checked that the result does not depend on the representative. And of course it does, and it also depends