<figure><img src="image_56.png" /><figcaption>Figure 41: Commutation rules for **newref**</figcaption></figure>

*Proof.* Consider the reduction $\rightarrow$ comprising the (context closure of) the commutations above with $\beta$-reduction and the state-free reductions for **mkvar** and **mksem**. Treating **ref** and **sem** as product types, it is easy to prove from the strong normalization of the simply-typed $\lambda$-calculus with products that $\rightarrow$ terminates. Moreover, as $M$ has type $\mathcal{X} \in \{\mathcal{U}, \mathcal{B}, \mathcal{N}\}$, a $\rightarrow$-normal form $M \rightarrow * M'$ has no abstraction, bad variable or semaphore subterm. Thus

$$M' = \mathbf{new} \ x_1:=n_1 \ \mathbf{in} \ \dots \ \mathbf{new} \ x_p:=n_p \ \mathbf{in} \ N'$$

with $\Sigma \vdash N' : \mathcal{X}$ without recursion, subterm of higher type, bad reference or semaphores, and reference and semaphore initialization. Finally, we conclude by Lemma 4.36. $\square$

The semantics enjoy *finitary adequacy*:

**Proposition 4.39.** For any recursion-free $\vdash M : \mathcal{U}$, we have $M \downarrow \text{ iff } [[M]] \downarrow$.

*Proof.* Immediate consequence of Proposition 4.37 and Lemma 4.38. $\square$

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

### 4.5.3. *Deducing adequacy.*
Finally, we extend the above with recursion.

**Theorem 4.40 (Adequacy).** For $\vdash M : \mathcal{U}$ any term of $|\mathcal{A}_{\parallel}|$, $M \downarrow \text{ iff } [[M]] \downarrow$.

*Proof.* As expected, we simply reason by continuity. For all type $A$ and $n \in \mathbb{N}$, we set

$$\mathcal{Y}_A^0 = \lambda f^{A \rightarrow A} . \perp_A \qquad \mathcal{Y}_A^{n+1} = \lambda f^{A \rightarrow A} . f (\mathcal{Y}_A^n f),$$

yielding $\vdash \mathcal{Y}_A^n : (A \rightarrow A) \rightarrow A$. The $n$-th approximation $\Gamma \vdash M_n : A$ of any term $\Gamma \vdash M : A$ of $|\mathcal{A}_{\parallel}|$ is obtained by replacing each $\mathcal{Y} N$ with $\mathcal{Y}_n N$. It is then routine to show that $M \downarrow$ iff there is $n \in \mathbb{N}$ such that $M_n \downarrow$. Likewise, by definition of the interpretation of recursion (see Section 4.4.1) and continuity of the interpretation, $[[M]] = \bigvee_{n \in \mathbb{N}} [[M_n]]$. Now:

$$M \downarrow \iff \begin{cases} \exists n \in \mathbb{N}, M_n \downarrow, \\ \exists n \in \mathbb{N}, [[M_n]] \text{ has a positive move,} \\ [[M]] \text{ has a positive move,} \end{cases}$$

using the above along with Proposition 4.39. $\square$

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

This continuity argument only works for *may*-convergence: for extensions such as *must* or *fair*-convergence we would have to formulate a more complete correspondence between operational and game semantics – see e.g. [Cas17] for an adequacy result for non-deterministic PCF w.r.t. *must-convergence*. However, we leave this out of this paper.
<figure><img src="image_59.png" /><figcaption>Figure 42: $\lambda x^U y^U$. newref $r := 0$ in
$\mathbf{assume}$ (iszero!$r$); $x$; $r := \mathbf{tt}$
$\parallel \mathbf{assume}$ (not (iszero!$r$)); $y$</figcaption></figure>

<figure><img src="image_60.png" /><figcaption>Figure 43: $\lambda f f^{U \to U \to U}$. newref $r := 0$ in
$f$ ($r := 1$)
*(skip $\otimes$ (assume!$r$))*</figcaption></figure>

4.6. **Full Abstraction.** Now that we have established $\to$-Strat as an adequate model of $IA_\llcorner$, we explore a bit further its observable operational content and prove full abstraction.

4.6.1. *Observable behaviour of causal strategies.* It is clear that without quotient, the interpretation of $IA_\llcorner$ in $\to$-Strat will not be fully abstract: the model records very intensional information that is typically not observable. We give two examples in Figures 42 and 43.

We introduce a few additional pieces of syntactic sugar. First, **assume** : $\mathbb{B} \to \mathcal{U}$ is
$\lambda x^\mathbb{B}$. **if** $x$ **skip** $\perp$ which terminates on **tt** and diverges otherwise. We also define **not** : $\mathbb{B} \to \mathbb{B}$
as the obvious program. Finally, for any $\Gamma \vdash M : A$ and $\Gamma \vdash N : A$ of $IA_\llcorner$, we set

$$
\begin{array}{l}
M \otimes N = \mathbf{newref} x := 0, y := 0 \ \mathbf{in} \\
\qquad (x := 1 \parallel y :=!x); \\
\qquad \mathbf{if} \ (\mathbf{iszero} \ (!y)) \ M \ N
\end{array}
$$

a non-deterministic sum $\Gamma \vdash M \otimes N : A$, behaving non-deterministically as $M$ or $N$.

First, Figure 42 represents the semantics of an encoding of sequential composition via
parallel composition plus shared state. In Ghica and Murawski's model, this program has
the same interpretation as sequential composition, showing their equivalence with respect
to may-testing. In contrast, $\to$-Strat also gives account of the limitation of this encoding:
the greyed out branch on the left corresponds to the bottom read winning the race, causing
divergence<fnref n="19" />. Likewise, Figure 43 also has an unobservable branch greyed out. The model
shows that the program may provide values for the two arguments of $f$ independently, but
it may also provide a value for the second argument of $f$ because $f$ called its first argument.
In a play, an occurrence of $\checkmark^+$ corresponding to a value for the second argument may be
causally explained by either of the two moves, but the distinction is un-observable.

For full abstraction only the observable behaviour matters, and $\to$-Strat clearly records
more than necessary. So we ask: what parts of a concurrent strategy are observable?

<footnote n="19">¹⁹This shows our model remembers *some* divergences, though not enough to get adequacy for *must*: some divergences are lost through hiding. This can be addressed by tweaking hiding to retain those events dubbed *essential* that carry divergences, see [CCHW18, Cas17] – but we shall not take this route in this paper.</footnote>
4.6.2. *Non-alternating plays with pointers.* We approach this question in terms which are no surprise to the reader familiar with Ghica and Murawski's non-alternating games: the observable behaviour is exactly captured by certain *non-alternating plays with pointers*:

**Definition 4.41.** A non-alternating play with pointers on A is a $s_1 \dots s_n$ on $|A|$ s.t.

$$ \text{negative: } n \ge 1 \implies \text{pol}(s_1) = -, $$

with, for all $1 \le j \le n$ s.t. $s_j$ is non-minimal in A, a **pointer** to some earlier $s_i$ such that $s_i \to_A s_j$. We write $\mathcal{P}\text{-}\mathcal{O}\text{-Plays}(A)$ for the set of non-alternating plays with pointers on A.

Ghica and Murawski's model is an analogue of $\mathcal{O}\text{-Strat}$ based on non-alternating plays with pointers. A **GM-strategy** on meager A is a non-empty set of well-bracketed non-alternating plays with pointers (with well-bracketing defined as in Definition 3.20) satisfying conditions analogous to Definition 3.19 (see Definitions 4 and 13 in [GM08]) and additionally *thread-independent* (see Definition 17 of [GM08]). There is a cartesian closed category GM of meager arenas and GM-strategies, supporting the interpretation of $IA_\parallel$.

We shall build a functorial bridge between $\to$-Strat and GM, as in Proposition 4.30, but restricted to the cartesian closed structure as GM has no linear decomposition. We use the concrete arenas of Section 2.20, extended in the obvious way with Question/Answer labeling.

The proof of Proposition 2.22 applies unchanged to prove:

**Proposition 4.42.** For any concrete arena A, there is an injective function

$$ \mathcal{P} : \mathcal{O}\text{-Plays}(A) / \cong \to \mathcal{P}\text{-}\mathcal{O}\text{-Plays}(A^0) $$

preserving length, prefix, justifiers, and reflecting and preserving well-bracketing.

We consider the cartesian closed category $\to$-Strat_c with objects concrete arenas, obtained from $\to$-Strat_l^wb by replacing all operations on arenas with those on concrete arenas.

**Proposition 4.43.** Consider concrete --arenas A, B, and $\sigma \in \to$-Strat_l^wb(A, B). Then,

$$ \mathcal{P}\text{-}\mathcal{O}\text{-Unf}(\sigma) = \{\mathcal{P}(s) \mid s \in \mathcal{O}\text{-Unf}(\sigma^\dagger) \text{ well-bracketed}\} $$

is a GM-strategy on $A^0 \to B^0$. Moreover, $\mathcal{P}\text{-}\mathcal{O}\text{-Unf}$ extends to a cartesian closed functor

$$ \mathcal{P}\text{-}\mathcal{O}\text{-Unf} : \to\text{-Strat}_c \to \text{GM} $$

preserving the interpretation of $IA_\parallel$.

*Proof.* We detail the two critical points: preservation of symmetry, and composition.

*Symmetry.* Consider $\sigma, \tau \in \to$-Strat_l^wb(A, B) s.t. $\sigma \approx \tau$. Then we also have $\Lambda(\sigma^\dagger) \approx \Lambda(\tau^\dagger)$, i.e. there is an iso $\varphi : \sigma^\dagger \cong \tau^\dagger$ s.t. $\partial_{\Lambda(\tau^\dagger)} \circ \varphi \sim^+ \partial_{\Lambda(\sigma^\dagger)}$. Consider $\mathcal{P}(s) \in \mathcal{P}\text{-}\mathcal{O}\text{-Unf}(\sigma)$ for some $s \in \mathcal{O}\text{-Unf}(\Lambda(\sigma^\dagger))$. This means there is $t \in \mathcal{O}\text{-Plays}(\sigma^\dagger)$ s.t. $s = \partial_{\Lambda(\sigma^\dagger)}(t)$. But then, $\varphi(t) \in \mathcal{O}\text{-Plays}(\tau^\dagger)$, and from $\partial_{\Lambda(\tau^\dagger)} \circ \varphi \sim^+ \partial_{\Lambda(\sigma^\dagger)}$ it is direct that $s = \partial_{\Lambda(\sigma^\dagger)}(t) \cong_{A \to B} \partial_{\Lambda(\tau^\dagger)}(\varphi(t))$. By Proposition 4.42, $\mathcal{P}(\partial_{\Lambda(\sigma^\dagger)}(t)) = \mathcal{P}(\partial_{\Lambda(\tau^\dagger)}(\varphi(t)))$, so that $\mathcal{P}(s) \in \mathcal{P}\text{-}\mathcal{O}\text{-Unf}(\tau)$. The other inclusion is symmetric, so $\mathcal{P}\text{-}\mathcal{O}\text{-Unf}(\sigma) = \mathcal{P}\text{-}\mathcal{O}\text{-Unf}(\tau)$.

*Composition.* For $\sigma \in \to$-Strat_l^wb(A, B), \tau \in \to$-Strat_l^wb(B, C)$, we must show

$$ \mathcal{P}\text{-}\mathcal{O}\text{-Unf}(\tau \odot_! \sigma) = \mathcal{P}\text{-}\mathcal{O}\text{-Unf}(\tau) \odot \mathcal{P}\text{-}\mathcal{O}\text{-Unf}(\sigma), $$

there are two inclusions to prove:

$\subseteq$. Consider $\mathcal{P}(s) \in \mathcal{P}\text{-}\mathcal{O}\text{-Unf}(\tau \odot_! \sigma)$. Since $\mathcal{P}\text{-}\mathcal{O}\text{-Unf}(-)$ preserves positive isomorphism and by the laws of Seely categories, $\mathcal{P}(s) \in \mathcal{P}\text{-}\mathcal{O}\text{-Unf}(\tau^\dagger \odot \sigma^\dagger)$ for some $s \in \mathcal{O}\text{-Unf}(\tau^\dagger \odot \sigma^\dagger)$. By Proposition 4.30, the latter is $\mathcal{O}\text{-Unf}(\tau^\dagger) \odot \mathcal{O}\text{-Unf}(\sigma^\dagger)$. Now,
if $u \in \mathcal{C}-\text{Unf}(\boldsymbol{\tau}^\dagger) \circledast \mathcal{C}-\text{Unf}(\boldsymbol{\sigma}^\dagger)$ is a witness for $s \in \mathcal{C}-\text{Unf}(\boldsymbol{\tau}^\dagger) \odot \mathcal{C}-\text{Unf}(\boldsymbol{\sigma}^\dagger)$, then as $\boldsymbol{\sigma}^\dagger$ and $\boldsymbol{\tau}^\dagger$ are well-bracketed, it is direct that $u \uparrow A, B \in \mathcal{C}-\text{Unf}(\boldsymbol{\sigma}^\dagger)$ and $u \uparrow B, C \in \mathcal{C}-\text{Unf}(\boldsymbol{\tau}^\dagger)$ are well-bracketed as well. Therefore, $\mathcal{P}(u \uparrow A, B) \in \mathcal{C}-\text{Unf}(\boldsymbol{\sigma}^\dagger)$ and $\mathcal{P}(u \uparrow B, C) \in \mathcal{C}-\text{Unf}(\boldsymbol{\tau}^\dagger)$, hence $\mathcal{P}(u)$ is a witness in the sense of [GM08] for $\mathcal{P}(s) \in \mathcal{P}-\mathcal{C}-\text{Unf}(\boldsymbol{\tau}) \odot \mathcal{P}-\mathcal{C}-\text{Unf}(\boldsymbol{\sigma})$.

$\cong$. Consider now $s \in \mathcal{P}-\mathcal{C}-\text{Unf}(\boldsymbol{\tau}) \odot \mathcal{P}-\mathcal{C}-\text{Unf}(\boldsymbol{\sigma})$. There is a witness $u$, a sequence with pointers on $(A' \dasharrow B') \dasharrow C'$, with restrictions $u \uparrow A', B' \in \mathcal{P}-\mathcal{C}-\text{Unf}(\boldsymbol{\sigma})$ and $u \uparrow B', C' \in \mathcal{P}-\mathcal{C}-\text{Unf}(\boldsymbol{\tau})$ – we refer to [GM08] for the definitions of restrictions of plays with pointers. Write $u \uparrow A', B' = \mathcal{P}(t^\sigma)$ and $u \uparrow B', C' = \mathcal{P}(t^\tau)$ for $t^\sigma \in \mathcal{C}-\text{Unf}(\boldsymbol{\sigma}^\dagger)$ and $t^\tau \in \mathcal{C}-\text{Unf}(\boldsymbol{\tau}^\dagger)$. Though $t^\sigma$ and $t^\tau$ yield plays with pointers compatible in $B'$, they might not match in $B$ on the nose. But by Proposition 4.42, $t^\sigma \uparrow B \cong_B t^\tau \uparrow B$ match up to symmetry. So, writing

$$t^{\sigma} = \partial_{\Lambda(\boldsymbol{\sigma}^{\dagger})}(v^{\sigma}) \qquad t^{\tau} = \partial_{\Lambda(\boldsymbol{\tau}^{\dagger})}(v^{\tau}),$$

for $v^\sigma \in \mathcal{C}-\text{Plays}(\boldsymbol{\sigma}^\dagger)$ and $v^\tau \in \mathcal{C}-\text{Plays}(\boldsymbol{\tau}^\dagger)$, writing $x^\sigma = |v^\sigma| \in \mathcal{C}(\boldsymbol{\sigma}^\dagger)$ and $x^\tau = |v^\tau| \in \mathcal{C}(\boldsymbol{\tau}^\dagger)$ the symmetry $t^\sigma \uparrow B \cong_B t^\tau \uparrow B$ induces $\theta: x_B^\sigma \cong_B x_B^\tau$. Moreover,

$$x^{\sigma} \parallel x_{C}^{\tau} \stackrel{\partial_{\sigma^{\dagger}} \parallel! C}{\cong} x_{A}^{\sigma} \parallel x_{B}^{\sigma} \parallel x_{C}^{\tau} \stackrel{! A \parallel \theta \parallel! C}{\cong} x_{A}^{\sigma} \parallel x_{B}^{\tau} \parallel x_{C}^{\tau} \stackrel{! A \parallel \partial_{\tau}^{-1}}{\cong} x_{A}^{\sigma} \parallel x^{\tau},$$

is secured, as $u$ directly informs a total ordering of its graph compatible with $\boldsymbol{\sigma}^\dagger$ and $\boldsymbol{\tau}^\dagger$. Hence, by Proposition 4.15, there are $\varphi^\sigma: x^\sigma \cong_{\sigma^\dagger} y^\sigma$ and $\varphi^\tau: x^\tau \cong_{\tau^\dagger} y^\tau$ such that $y_B^\sigma = y_B^\tau$.

Transporting $t^\sigma$ and $t^\tau$ through $\varphi^\sigma$ and $\varphi^\tau$, we get $w^\sigma \in \mathcal{C}-\text{Plays}(\boldsymbol{\sigma}^\dagger)$ and $w^\tau \in \mathcal{C}-\text{Plays}(\boldsymbol{\tau}^\dagger)$ s.t. we still have $\mathcal{P}(w^\sigma) = u \uparrow A', B'$ and $\mathcal{P}(w^\tau) = u \uparrow B', C'$; but this time $w^\sigma \uparrow B = w^\tau \uparrow B$. Zipping them following $u$ we obtain $w \in \mathcal{C}-\text{Plays}(\boldsymbol{\tau}^\dagger) \circledast \mathcal{C}-\text{Plays}(\boldsymbol{\sigma}^\dagger)$ such that $\mathcal{P}(w \uparrow A, C) = s$. But then $w \uparrow A, C \in \mathcal{C}-\text{Plays}(\boldsymbol{\tau}^\dagger) \odot \mathcal{C}-\text{Plays}(\boldsymbol{\sigma}^\dagger)$ by construction, so in $\mathcal{C}-\text{Plays}((\boldsymbol{\tau} \odot! \boldsymbol{\sigma})^\dagger)$ by Proposition 4.30, hence $s \in \mathcal{P}-\mathcal{C}-\text{Unf}(\boldsymbol{\tau} \odot! \boldsymbol{\sigma})$ as required. $\square$

So there is a functorial unfolding from $\dasharrow$-Strat to GM. To further factor out non-observable behaviour, one can restrict to complete plays:

**Definition 4.44.** Consider A a meager $\dasharrow$arena, and $s \in \mathcal{P}-\mathcal{C}-\text{Plays}(A)$.

We say that $s$ is **complete** iff it is well-bracketed and all its questions have an answer.

If $\boldsymbol{\sigma} \in \dasharrow$-Strat$^\text{wb}(A, B)$, $\text{comp}(\boldsymbol{\sigma})$ is the subset of $\mathcal{P}-\mathcal{C}-\text{Unf}(\boldsymbol{\sigma})$ comprising complete plays only. The proposition above allows us to deduce (with $\sim$ defined in Section 3.3.2):

**Proposition 4.45.** Consider A concrete and $\boldsymbol{\sigma}, \boldsymbol{\tau}$: A well-bracketed causal strategies. Then,

$$\text{comp}(\boldsymbol{\sigma}) = \text{comp}(\boldsymbol{\tau}) \quad \implies \quad \boldsymbol{\sigma} \sim \boldsymbol{\tau}.$$

*Proof.* Consider $\boldsymbol{\alpha} \in \dasharrow$-Strat$^\text{wb}(A, \mathbb{U})$ s.t. $\boldsymbol{\alpha} \odot! \boldsymbol{\sigma} \downarrow$. By Proposition 4.43, $\mathbb{q}^{-}\mathbb{q}^{+} \in \mathcal{P}-\mathcal{C}-\text{Unf}(\boldsymbol{\alpha}) \odot \mathcal{P}-\mathcal{C}-\text{Unf}(\boldsymbol{\sigma})$. Considering $u \in \mathcal{P}-\mathcal{C}-\text{Unf}(\boldsymbol{\alpha}) \circledast \mathcal{P}-\mathcal{C}-\text{Unf}(\boldsymbol{\sigma})$, $u \uparrow A^0, \mathbb{U} \in \mathcal{P}-\mathcal{C}-\text{Unf}(\boldsymbol{\sigma})$. From well-bracketing of $\boldsymbol{\sigma}$ and $\boldsymbol{\alpha}$, $u \uparrow A^0$ is well-bracketed and complete, so $u \uparrow A^0 \in \text{comp}(\boldsymbol{\tau})$, so $\mathcal{P}-\mathcal{C}-\text{Unf}(\boldsymbol{\alpha}) \odot \mathcal{P}-\mathcal{C}-\text{Unf}(\boldsymbol{\tau}) \downarrow$, so $\boldsymbol{\alpha} \odot! \boldsymbol{\tau} \downarrow$ by Proposition 4.43. $\square$

To prove the converse and link it to syntactic equivalence, we examine *definability*.

4.6.3. *Definability of plays with pointers.* As in Sections 3.3.2 and 3.4.4, full abstraction relies on *definability*. While definability in IA rests on definability for finite innocent strategies, Ghica and Murawski's definability for IA$_{\llcorner}$ gives directly terms realizing *individual plays*. For conciseness we omit the full development, but illustrate it on a representative example.

Consider $s$ on the left hand side of Figure 44. Naively, we want a term whose only execution is $s$. But strategies satisfy *courtesy*, so one realizing $s$ must also realize all
<figure><img src="image_61.png" /><figcaption>Figure 44: Example of definability of plays in IA$_{‖}$</figcaption></figure>

plays obtainable by adding asynchronous delays. The information from *s* that survives asynchronous delays is that certain positive moves appear *after* earlier negative moves in *s*. Together with the static causality from the arena, this yields a diagram as in the right hand side of Figure 44, very much like a causal strategy. It is directly this diagram that Ghica and Murawski's finite definability reproduces. First, we ignore $\rightarrow$-links and start with a term

$$ \lambda x^{U_1} f^{U_2 \rightarrow U_3} y^{U_4} . (x \parallel f \text{skip} \parallel y); \perp, $$

that performs all computational events available in *s* in a maximally parallel fashion, with only causal dependency enforced by the game. The $\rightarrow$-links are restored through the memory. For that we define two helper functions. If $M: \text{ref}$, we write $\text{set}(M) : \mathbb{U}$ for $M := 1$, and $\text{test}(M) : \mathbb{U}$ for $\text{assume}(\text{not}(\text{iszero}!M))$ which converges iff $!M$ is non-zero. Then:

$$ \lambda x^{U_1} f^{U_2 \rightarrow U_3} y^{U_4} . \left( \left( \begin{array}{c} x; \\ \text{set}(\check{\sqrt{1}}) \end{array} \right) \parallel \left( \begin{array}{c} f(\text{set}(\bar{q}_2)); \\ \text{test}(\check{\sqrt{4}}); \\ \text{grab}(\check{\sqrt{2}}^+); \\ \text{skip} \end{array} \right) \parallel \left( \begin{array}{c} \text{test}(\check{\sqrt{1}}^-); \\ \text{test}(\bar{q}_2^-); \\ y; \\ \text{set}(\check{\sqrt{4}}^-) \end{array} \right) \right); \perp $$

borrows the shape of the first term, signaling the $\rightarrow$-links through memory. We use one fresh reference (initialized to 0) for each Opponent move, which gets set to 1 when the Opponent move occurs. Finally, we use semaphores to ensure that Opponent replications does not cause a duplication of Player moves by prompting re-evaluation of the corresponding subterms – so that we only obtain linearizations of the diagram on the right hand side of Figure 44.

Done systematically for arbitrary plays, this establishes [GM08]:

**Proposition 4.46** (Ghica, Murawski). Consider A a type and $s \in \mathcal{P}\mathcal{C}\mathcal{S}\text{-Plays}([A])$ complete. Then there is $\vdash M_s : A \rightarrow \mathbb{U}$ such that for all $\vdash N : A$,

$$ s \in [N]_{\text{GM}} \iff M_s N \downarrow $$

In particular, as $[N]_{\text{GM}}$ is courteous, any $t \in [N]_{\text{GM}}$ tracing a successful interaction with $M_s$ can be converted to *s* through permutations whose correctness is granted by courtesy.

**Theorem 4.47.** The model $\rightarrow$-Strat$_i^{\text{wb}}$ is intensionally fully abstract for IA$_{‖}$.

*Proof.* Consider $\vdash M, N : A$. If $[M] \sim [N]$, using Theorem 4.40, $M \sim N$. Reciprocally, assume $M \sim N$. Seeking a contradiction, assume $[M] \uplus [N]$. By Proposition 4.45, there is w.l.o.g. $s \in \text{comp}([M])$ where $s \notin \text{comp}([N])$. So, by Proposition 4.43, $s \in [M]_{\text{GM}}$ while $s \notin [N]_{\text{GM}}$. Finally, by Proposition 4.46, we have $M_s M \downarrow$ while $M_s N \uparrow$, contradiction. $\square$
As for Theorem 3.14, the resulting quotient is effective and easily described: for $\sigma, \tau: A$,

$$ \sigma \sim \tau \Leftrightarrow \mathrm{comp}(\sigma) = \mathrm{comp}(\tau). $$

Observational equivalence is undecidable even for the second-order fragment and without recursion [GMO06]. Note also that without semaphores, full abstraction fails [Mur10] as terms are closed under a stuttering behaviour which reduces their observational power.

**4.7. Parallel Innocence and Sequentiality.** We resume the discussion left at Section 3.6: can we find *parallel innocence* and *sequentiality* disentangling parallelism and interference?

A subtlety is that while $IA_\parallel$ is non-deterministic, $PCF_\parallel$ and $IA$ are both deterministic – albeit in different senses. Non-determinism arises in $IA_\parallel$ from the interaction of parallelism and interference so, removing either of these causes, determinism has to be reimposed as well. Accordingly, sequentiality and parallel innocence will include determinism.

## 5. PARALLEL INNOCENCE

We capture the causal patterns definable with pure parallel higher-order programming.

**5.1. Causal determinism.** The sense in which $PCF_\parallel$ is deterministic is fairly different from Definition 2.8. For instance, after the first Opponent move, the strategy of Figure 38 has two available Player moves; but the order in which these moves are played does not matter and will eventually reach the same result: the program is *deterministic up to the choice of the scheduler*. If $E$ is an event structure, write $\mathrm{Con}_E$ for the set of finite consistent sets of events, i.e. for $X \subseteq_f |E|$, $X \in \mathrm{Con}_E$ iff for all $e_1, e_2 \in X$, we have $-(e_1 \#_\sigma e_2)$.

We use Winskel's definition of *determinism* for concurrent strategies [Win12]:

**Definition 5.1.** A causal strategy $\sigma: A$ on arena $A$ is **causally deterministic** if:

*causal determinism:* assume $X \subseteq_f |\sigma|$ is negatively compatible, i.e. $X_- = \{s \in X \mid \mathrm{pol}_\sigma(s) = -\} \in \mathrm{Con}_\sigma$. Then, $X \in \mathrm{Con}_\sigma$ as well.

This ensures that Player branching only spawns parallel threads: only Opponent may initiate conflict. Copycat is deterministic, and deterministic strategies compose [Win12]. All other constructions in the Seely category structure of $\dashv$-Strat preserve determinism.

**5.2. Parallel Innocence.** What causal shapes are distinctive of pure parallel computation?

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

*"Player may merge threads than he himself has spawned"*.

In contrast, both diagrams of Figure 32 bear signs of interference. In the first, the answer $1^+$ depends on $q^-$: the program somehow observes if the function has called its argument, which is only possible if the argument performs some side-effect that the program observes. In the second, $\checkmark^+$ depends on $\checkmark^-$; but likewise this can only occur if the termination of the function triggers a side-effect. In both cases, this is witnessed by Player “merging” causal chains which forked at Opponent moves. To ban such interference, the slogan is:
<figure><img src="image_62.png" /><figcaption>Figure 45: Maximal grounded causal chains of a causal strategy</figcaption></figure>

<figure><img src="image_63.png" /><figcaption>Figure 46: A typical pre-innocent strategy</figcaption></figure>

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

“Player may not merge threads spawned by Opponent”.

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

**Definition 5.2.** Consider A an arena, and $\sigma: A$ a causal strategy.

A grounded causal chain (gcc) in $\sigma$ is $\rho = \{\rho_1, \dots, \rho_n\} \subseteq |\sigma|$ forming
$$ \rho_1 \to \sigma \dots \to \sigma \rho_n $$

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

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

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

**Definition 5.3.** Consider A an arena. A causally deterministic $\sigma: A$ is **pre-innocent** iff

*pre-innocence:* If $m^+ \in |\sigma|$ and $\rho_1 \to m, \rho_2 \to m \in gcc(\sigma)$ are distinct, then their least distinct moves are positive.

As causal strategies are *pointed*, $\rho_1$ and $\rho_2$ necessarily share the same initial move. The strategy of Figure 46 is pre-innocent. In contrast, that of Figure 31 is not – both augmentations of Figure 32 fail pre-innocence. For instance, the second and third gccs of Figure 45 arrive at $1^+$ but before that, the greatest common event is $q^+$, which is positive: Player is merging (via $1^+$) two gccs forked by Opponent, which is forbidden by pre-innocence.

It will follow later on that the sequential pre-innocent causal strategies exactly match the standard alternating innocent strategies of Definition 3.6: sequentiality entails that there is no Player branching. Thus separate branches always correspond to threads spawned by
<figure><img src="image_65.png" /><figcaption>Figure 48: A gcc of a non-visible strategy, losing its pointer</figcaption></figure>

Opponent, which by pre-innocence cannot interfere. The causal structure is then a forest, matching that of *P*-views of Section 3.2. We postpone the details to Section 6.3.

However, it turns out that pre-innocence is incomplete for parallel strategies.

5.2.2. *Visibility*. The problem arises as non-stability of pre-innocence under composition. A counter-example appears in Figure 49, examined when proving compositionality of innocence.

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

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

**Definition 5.4.** A causal strategy $\sigma: A$ is **visible** if for all $\rho \in \text{gcc}(\sigma)$, $\partial_{\sigma}(\rho) \in \mathscr{C}(A)$.

In other words, every move in $\rho$ points within $\rho$. This phrasing highlights the analogy with Definition 3.5, i.e. “Player always points in the P-view”. It is indeed this analogy that inspired the name$^{20}$. But one must be wary: the alternating interpretation of sequential programs with state yields sequential P-visible strategies, but their causal interpretation (as in Figure 31) is *not* necessarily visible. Visibility is very restrictive, it is not clear what would be a sensible programming primitive that would satisfy visibility but not pre-innocence.

We regard visibility as a key contribution. It has far-reaching consequences – some of which will be introduced in the course of this paper. In fact, visibility is used more than parallel innocence in further developments in this line of work [CCPW18, CdV20].

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

**Lemma 5.5.** *Consider $\sigma: A$ a visible causal strategy.*

Then for any $\rho = \rho_1 \to_{\sigma} \dots \to_{\sigma} \rho_n \in \text{gcc}(\sigma)$, $\partial_{\sigma}(\rho) = \partial_{\sigma}(\rho_1) \dots \partial_{\sigma}(\rho_n)$ is a P-view.

*Proof.* By Lemma A.3, $\partial_{\sigma}(\rho)$ is an alternating sequence. By visibility, its prefixes are configurations of $A$. So, $\partial_{\sigma}(\rho) \in \text{↓↑-Plays}(A)$. By Lemma A.4, the predecessor of $a^- \in \partial_{\sigma}(\rho)$ for $\to_A$ is its predecessor in $\partial_{\sigma}(\rho)$, i.e. Opponent always points to the previous move. $\square$

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

**Definition 5.6.** Consider $\sigma: A$ causally deterministic on arena $A$.

It is **parallel innocent** if it is pre-innocent and **visible**.

<footnote>$^{20}$This, plus as in traditional game semantics, visibility is a prerequisite for a working notion of innocence.</footnote>
A standard innocent strategy as in Section 3.2, under its “causal” presentation, is a forest of P-views (see Proposition 3.7), i.e. a forest of (displayed) gccs. In that light the definition of parallel innocent strategies seems natural: they are generated no longer by a forest of P-views, but by a directed acyclic graph of P-views with additional conflict relation. This graph describes how threads are spawned, and then may merge, following the innocence discipline ensuring that Player may not create interference between Opponent's threads.

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

### 5.3. Composition of Visibility. First, we establish compositionality of visibility.

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

**Definition 5.7.** Consider $A$ and $B$ $--$arenas, and $\sigma: A \vdash B$. Then, for all $m, m' \in |\sigma|,$

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

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

and undefined otherwise.

This leaves the justifier undefined exactly for moves corresponding to minimal moves in $B$, the initial moves. Note that assigning the justifier of $m$ minimal in $A$ to init($m$) ensures that the assignment of justifiers is invariant under currying. It might be helpful to the reader to observe that a causal strategy $\sigma: A \vdash B$ is visible iff for all $\rho \in \text{gcc}(\sigma)$, for all $m \in \rho$, just($m$) $\in \rho$ as well: all gccs are closed under justifiers. We mention in passing this lemma:

**Lemma 5.8.** *Consider $A, B$ $--$arenas and $\sigma: A \vdash B$ a causal strategy.*

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

*Proof.* As a map of event structures, $\partial_{\sigma}$ locally reflects causality (Lemma A.2), so just($m$) $<$$_{σ} m$ if the first clause of Definition 5.7 applies; for the other we clearly have init($m$) $<$$_{σ} m$.

If pol$_{σ}$(m) = $-$, then just(e) is defined via the first clause since A is negative, and $\partial_{\sigma}$(just(m)) $\to_{A \vdash B} \partial_{\sigma}$(m). Now, m has a predecessor $m' \to_{\sigma} m$, by courtesy $\partial_{\sigma}(m') \to_{A \vdash B} \partial_{\sigma}(m)$, so $\partial_{\sigma}(m') = \partial_{\sigma}$(just(m)) as A is forestial, and $m' = \text{just}(m)$ by local injectivity. $\square$

5.3.2. *Justifiers in interactions.* We extend justifiers to interactions – consider $A, B$ and $C$ three $--$arenas, and $\sigma: A \vdash B$ and $\tau: B \vdash C$ causal strategies.

**Definition 5.9.** We define the partial function just: $|\tau \otimes \sigma| \to |\tau \otimes \sigma|$ as just($m$) = $m'$ if:

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

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

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

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

This leaves just($m$) undefined exactly if it corresponds to a minimal move in $C$. Clearly the two notions of justifier are compatible, in the sense that for all $m \in |\tau \otimes \sigma|$, if $m_{\sigma}$ is defined then just($m$)$_{\sigma}$ is defined and equal to just($m_{\sigma}$), and likewise for $\tau$.
**5.3.3.** *Views of gccs.* We introduce the main technical device on visible causal interactions.

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

**Definition 5.10.** Consider $\sigma: A \vdash B$ and $\tau: B \vdash C$ with $A, B$ and $C$ --arenas.

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

$$ 
\begin{align*}
^{\tau}\rho_0 \rightarrow \dots \rightarrow \rho_n \rightarrow \rho_{n+1}^{\prime\sigma} &= ^{\tau}\rho_0 \rightarrow \dots \rightarrow \rho_n^{\prime\sigma} \cup \{\rho_{n+1}\}, \\
^{\tau}\rho_0 \rightarrow \dots \rightarrow \rho_i \rightarrow \dots \rightarrow \rho_{n+1}^{-,r}^{\prime\sigma} &= ^{\tau}\rho_0 \rightarrow \dots \rightarrow \rho_i^{\prime\sigma} \cup \{\rho_{n+1}\} \quad \text{if just}(\rho_{n+1}) = \rho_i \text{ in } A \text{ or } B, \\
^{\tau}\rho_0 \rightarrow \dots \rightarrow \rho_i \rightarrow \dots \rightarrow \rho_{n+1}^{\prime\sigma} &= \{\rho_{n+1}\} \quad \text{if } \rho_{n+1} \text{ minimal in } B,
\end{align*}
$$

undefined otherwise. For $\rho \in \text{gcc}(\tau \circledast \sigma)$ ending in $\tau$, we (partially) define $^{\tau}\rho^{\prime\tau} \in \text{gcc}(\tau)$:

$$ 
\begin{align*}
^{\tau}\rho_0 \rightarrow \dots \rightarrow \rho_n \rightarrow \rho_{n+1}^{\prime\tau} &= ^{\tau}\rho_0 \rightarrow \dots \rightarrow \rho_n^{\prime\tau} \cup \{\rho_{n+1}\}, \\
^{\tau}\rho_0 \rightarrow \dots \rightarrow \rho_i \rightarrow \dots \rightarrow \rho_{n+1}^{-,l}^{\prime\tau} &= ^{\tau}\rho_0 \rightarrow \dots \rightarrow \rho_i^{\prime\tau} \cup \{\rho_{n+1}\} \quad \text{if just}(\rho_{n+1}) = \rho_i;
\end{align*}
$$

when defined we call $^{\tau}\rho^{\prime\sigma} \in \text{gcc}(\sigma)$ the **$\sigma$-view** of $\rho$ and $^{\tau}\rho^{\prime\tau} \in \text{gcc}(\tau)$ the **$\tau$-view** of $\rho$.

These definitions almost perfectly follow Definition 3.4. The last clause is only needed for $^{\tau}\rho^{\prime\sigma}$ and not $^{\tau}\rho^{\prime\tau}$, because an initial event in $C$ must be the first event of $\rho$ anyway.

That this yields gccs of $\sigma$ and $\tau$ rests on Lemma 4.21, and courtesy of $\sigma$ and $\tau$. The $\sigma$-view and the $\tau$-view are in principle only partially defined, because it may be, when attempting to follow the opponent's pointer, that that justifier lies outside the gcc. For instance $^{\tau}\rho^{\prime\tau}$, for $\rho$ in Figure 47, is not well-defined: when attempting to compute $^{\tau}q^{-}q_{0}^{r}\sqrt{l}^{\prime\tau}$, none of the clauses apply as just($\sqrt{l}^{\prime}$) = $q_{1}^{r}$ is outside $\rho$. The bulk of the proof of stability of visibility under composition, is to show that this cannot happen for visible strategies:

**Proposition 5.11.** Let $\sigma: A \vdash B$ and $\tau: B \vdash C$ be visible causal strategies.

Then, the views of gccs of $\tau \circledast \sigma$ as in Definition 5.10 are always well-defined.

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

(1) if $\rho$ ends in $\sigma$, then $^{\tau}\rho^{\prime\sigma}$ is well-defined,

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

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

If the last move has polarity $r$, write $\rho = \rho' \rightarrow m_1 \rightarrow m_2^r$. By Lemma 4.21, $m_1 \rightarrow_{\tau} m_2$, so in particular $m_1$ is in $\tau$. By induction hypothesis, $\kappa = ^{\tau}\rho' \rightarrow m_1^{\prime\tau} \in \text{gcc}(\tau)$, so

$$ \kappa \rightarrow m_2 = ^{\tau}\rho^{\prime\tau} \in \text{gcc}(\tau) $$

as well. But if $\rho$ finishes in $\sigma$ and $\tau$ (i.e. in $B$), we must further prove that $^{\tau}\rho^{\prime\sigma} \in \text{gcc}(\sigma)$. In that case, we observe that since $^{\tau}\rho^{\prime\tau} \in \text{gcc}(\tau)$ and $\tau$ is visible, it follows that just($m_2$) $\in$ $^{\tau}\rho^{\prime\tau}$. But that is a subset of $\rho$, so just($m_2$) $\in$ $\rho$. Hence the second clause of Definition 5.10 applies, and we conclude by induction hypothesis. If $\rho$ finishes in $\sigma$, the reasoning is symmetric. $\square$

From this, we are now ready to conclude:

**Proposition 5.12.** Let $\sigma: A \vdash B$ and $\tau: B \vdash C$ be visible causal strategies.

Then, $\tau \odot \sigma: A \vdash C$ is also visible.
<figure><img src="image_66.png" /><figcaption>Figure 49: Failure of preservation of pre-innocence under composition</figcaption></figure>

*Proof.* We prove by induction on $\rho$ that for all $\rho \in \text{gcc}(\tau \circled{\sigma})$, $\partial_{\tau \circled{\sigma}}(\rho) \in \mathscr{C}(A \parallel B \parallel C)$. If $\rho$ is empty it is clear; take $\rho \to m \in \text{gcc}(\tau \circled{\sigma})$. By induction hypothesis, $\partial_{\tau \circled{\sigma}}(\rho) \in \mathscr{C}(A \parallel B \parallel C)$, we only need that the justifier of $m$ is in $\rho$. We reason by cases on the polarity of $m$: if it is $\sigma$, then by Proposition 5.11 $\lceil \rho \to m \rceil^{\sigma} \in \text{gcc}(\sigma)$. But since $\sigma$ is visible, the justifier of $m$ appears in $\lceil \rho \rceil^{\sigma}$; a subset of $\rho$. The other cases are symmetric or trivial.

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

## 5.4. Composition of Innocence. We now address composition of pre-innocence.

We start this section by showing “what could go wrong”. In Figure 49, we show a counter-example to the stability under composition of pre-innocence without visibility, with the corresponding interaction appearing as Figure 50. Let us attempt to explain the phenomenon, calling $\sigma$ the left hand side strategy (parallel composition) and $\tau$ the right hand side one – observe that the dotted lines include the justifications relations from Definition 5.7 rather than just those coming from the arena. Imagine that $\tau$ wants to perform an illegal causal merge between the two argument calls of its argument of type $U \to U \to U$. By pre-innocence it cannot do so directly. However, it can outsource the merge to $\sigma$ by linking (legally with respect to pre-innocence, but illegally with respect to visibility) the arguments of the parallel composition to those that it wants to merge.

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

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

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

**Lemma 5.13 (Forking lemma).** Let $\rho, \kappa \in \text{gcc}(\tau \circled{\sigma})$ be forking gccs ending in $\sigma$, s.t. $\lceil \rho \rceil^{\sigma} \cap \lceil \kappa \rceil^{\sigma} \ne \emptyset$ and $\text{gce}(\lceil \rho \rceil^{\sigma}, \lceil \kappa \rceil^{\sigma})$ negative (the least distinct events, if any, are positive).
<figure><img src="image_67.png" /><figcaption>Figure 50: Illegal causal merge</figcaption></figure>

<figure><img src="image_68.png" /><figcaption>Figure 51: Merging paths in G</figcaption></figure>

Then, gce(↑ρ↑σ, ↑κ↑σ) = gce(ρ, κ). Moreover, the symmetric property holds for τ.

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

$$O-\text{edges} = \{(m_1, m_2) \mid \text{just}(m_1) = m_2\}$$

$$P-\text{edges} = \{(m_1^l, m_2) \mid m_2 \to_{\tau \otimes \sigma} m_1\}$$

where the annotation $m_i^l$ indicates the polarity. Each vertex is source of at most one edge, and following edges consists exactly in computing the σ-view. If ρ and κ have the same final move, then ρ = κ. Otherwise, consider the two paths in G starting with these distinct final moves. Since ↑ρ↑σ ∩ ↑κ↑σ ≠ ∅, these two paths must intersect – Figure 51 represents a typical G with O-edges in blue and P-edges in red with the two typical cases.

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

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

5.4.2. *Stability of* →-pre-innocence. Now, much of the proof consists in restricting the causal shapes in τ ⊗ σ corresponding to a causal merge in τ ⊙ σ, so that the forking lemma applies.

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

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

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

with $m_1, m_2$ and $m$ visible, and no one visible in between. We reason on the polarity of $n$ in $\tau \circledast \sigma$. By Lemma 4.21 and since arenas are forestial, it cannot be negative, so its polarity is either $|$ or $\bar{r}$. Assume it is $|$ – the other case is symmetric. We may compute the $\sigma$-views:

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

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

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

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

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

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

Now, since $\sigma$ is pre-innocent, the least distinct moves $m_1'$ and $m_2'$ of $^{\tau}\kappa_{\le n}^1$ $^{\tau}\sigma$ and $^{\tau}\kappa_{\le p}^2$ $^{\tau}\sigma$ are positive. Thus their common immediate predecessor is negative – but it is also their greatest common event, since $^{\tau}\kappa_{\le n}^1$ $^{\tau}\sigma$ and $^{\tau}\kappa_{\le p}^2$ $^{\tau}\sigma$ are forking. So, by Lemma 5.13,

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

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

**Proposition 5.15.** There is $\to$-Strat<sup>wb,inn</sup>, a sub-Seely category of $\to$-Strat<sup>wb</sup> having the same objects and morphisms restricted to parallel innocent causal strategies.

*Proof.* Propositions 5.12 and 5.14 ensure that parallel innocent strategies compose. Stability under tensor and pairing are immediate. It remains that structural morphisms are innocent.

We detail it for copycat. Consider A a $\to$-arena. We show that any $(i, a) \in |\mathcal{C}_A|$, $(i, a)$ is minimal or has exactly one predecessor for $\to_{\mathcal{C}_A}$. Assume first $\text{pol}(i, a) = -$. If it is not minimal, take $(j, a') \to_{\mathcal{C}_A} (i, a)$. Necessarily $i = j$ and $a' \to_A a$, so uniqueness follows from A forestial. If $\text{pol}(i, a) = +$, its unique immediate predecessor is $(2 - i, a)$. So, $\mathcal{C}_A$ is forestial.
Now, for visibility, consider $\rho \in \mathbf{gcc}(\omega_A)$. But since $\omega_A$ is forestial, $\rho \in \mathcal{C}(\omega_A)$, so clearly $\partial_{\omega_A}(\rho) = \rho \in \mathcal{C}(A \vdash A)$. For parallel innocence, consider $\rho_1 \dashv\omega_A (i, a)$, $\rho_2 \dashv\omega_A (i, a) \in \mathbf{gcc}(\omega_A)$ distinct. But since $\omega_A$ is forestial, $\rho_1 = \rho_2$, contradicting their distinctness. $\square$

5.4.3. *Interpretation of PCF*<sub>//</sub>. We complete the interpretation. For all sequential primitives of PCF<sub>//</sub>, the corresponding strategy is forestial: as for copycat, parallel innocence follows. Finally, the strategy $\text{plet}_{X,Y}$ is shown parallel innocent by direct inspection (see Figure 38). Altogether, this yields an interpretation of PCF<sub>//</sub> in $\dashv\text{-Strat}_i^{\text{wb,inn}}$, and we have:

**Corollary 5.16 (Adequacy).** For $\vdash M : \mathcal{U}$ any term of PCF<sub>//</sub>, $M \Downarrow \text{iff } [[M]]_{\dashv\text{-Strat}_i^{\text{wb,inn}}} \Downarrow$.

*Proof.* Consequence of Theorem 4.40, as PCF<sub>//</sub> is a sub-language of IA<sub>//</sub>. $\square$

By the end of the paper, we will have established that $\dashv\text{-Strat}^{\text{wb,inn}}$ is intensionally fully abstract for PCF<sub>//</sub>. However the corresponding technical development is left for last.

## 6. SEQUENTIALITY AND CAUSAL FULL ABSTRACTION FOR IA AND PCF

In this section, we shall define sequentiality on $\dashv\text{-Strat}^{\text{wb}}$, then prove full abstraction results

$\dashv\text{-Strat}_i^{\text{wb}} + \text{sequentiality}$ is fully abstract for IA,
$\dashv\text{-Strat}_i^{\text{wb}} + \text{parallel innocence} + \text{sequentiality}$ is fully abstract for PCF,

established by linking with Theorems 3.10 and 3.14 for alternating strategies.

### 6.1. Sequentiality.
We construct the Seely category of sequential causal strategies.

#### 6.1.1. Definition.
Intuitively, a causal strategy $\boldsymbol{\sigma}: A$ is sequential if it unfolds gracefully to a (deterministic) alternating strategy. That does not mean that Player never throws parallel threads, or always acts deterministically: for instance, the strategy in Figure 31 should be sequential and yet has certain of its configurations enabling two parallel or two conflicting Player moves. But: as long as Opponent follows an alternating discipline, so should Player.

A play $s \in \mathcal{C}\text{-Plays}(A)$ is **alternating** if $s \in \downarrow\uparrow\text{-Plays}(A)$. We shall often use $\mathcal{C}\text{-Plays}(-)$ or $\downarrow\uparrow\text{-Plays}(-)$ on causal strategies – recall that $\downarrow\uparrow\text{-Plays}(\boldsymbol{\sigma})$ and $\mathcal{C}\text{-Plays}(\boldsymbol{\sigma})$ are sequences of $|\boldsymbol{\sigma}|$, and must not be confused with $\mathcal{C}\text{-Unf}(\boldsymbol{\sigma})$ that includes a move-by-move projection via the display map. We start by giving the definition of (deterministic) sequentiality:

**Definition 6.1.** Consider A an arena. A causal (pre)strategy $\boldsymbol{\sigma}: A$ is **sequential** if:

* reachable sequentiality: for all $tn^+ \in \mathcal{C}\text{-Plays}(\boldsymbol{\sigma})$, if $t \in \downarrow\uparrow\text{-Plays}(\boldsymbol{\sigma})$ then $tn \in \downarrow\uparrow\text{-Plays}(\boldsymbol{\sigma})$.

* sequential determinism: for all $tn_1^+, tn_2^+ \in \downarrow\uparrow\text{-Plays}(\boldsymbol{\sigma})$, then $n_1 = n_2$;

* sequential visibility: every alternating $s \in \mathcal{C}\text{-Unf}(\boldsymbol{\sigma})$ is P-visible.

For sequential determinism, more than merely asking that $\mathcal{C}\text{-Unf}(\boldsymbol{\sigma})$ acts deterministically on alternating plays, this condition imposes that no internal non-deterministic choice is alternatingly reachable, even when this choice would yield no observable non-deterministic behaviour (this is required for the forthcoming alternating projection to preserve symmetry).

Sequential visibility is perhaps puzzling, as P-visibility is usually associated not to sequentiality, but to the absence of higher-order state [AHM98]. From a given control point, a P-visible strategy may only call a procedure bound within the branch of the syntax
tree leading to that control point. In contrast, with higher-order state, a program may
call a procedure stored in the memory, originating from a remote program phrase outside
the current branch. This phenomenon is independent of sequentiality, but in $\rightarrow$-Strat the
causality due to the syntax tree blurs with that due to interference. So strategies arising
from the interpretation of IA$_{\parallel}$ are "morally" P-visible but formalizing this is nontrivial$^{21}$.
For us it is not worth the trouble as P-visibility is not required for full abstraction for IA$_{\parallel}$$^{22}$.
Consequently, it suffices to reinstate it once we restrict to sequential strategies.

6.1.2. *Alternating projection.* We start by defining the alternating projection.

**Definition 6.2.** Consider $A, B$ --arenas, and $\sigma : A \vdash B$ a sequential causal (pre)strategy.
Then, we define $\downarrow\uparrow$-Unf($\sigma$) = $\{\partial_{\Lambda(\sigma)}(t) \mid t \in \downarrow\uparrow$-Plays($\sigma$)}$.

We shall prove that $\downarrow\uparrow$-Unf($\sigma$) is an alternating (pre)strategy on $A \to B$. The two
subtle points are that it is deterministic, and uniform – which both rest on the observation:

**Lemma 6.3.** *Consider A, B --arenas, and σ : A ⊢ B a sequential (pre)strategy.*
*For any s ∈ ↓↑-Unf(σ), there is a unique t ∈ ↓↑-Plays(σ) such that s = ∂<sub>Λ(σ)</sub>(t).*

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

From this it follows that $\downarrow\uparrow$-Unf($\sigma$) satisfies determinism. For uniformity, we prove:

**Lemma 6.4.** *Consider A an arena and $\sigma, \tau : A \vdash B$ sequential causal (pre)strategies.*
*If $\sigma \approx \tau$, then $\downarrow\uparrow$-Unf($\sigma$) $\approx$ $\downarrow\uparrow$-Unf($\tau$).*

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

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

We prove by induction on $s^\sigma \in \downarrow\uparrow$-Unf($\sigma$) that if $s^\sigma \cong_{A\vdash B} s^\tau$ with $s^\tau \in \downarrow\uparrow$-Unf($\tau$), then taking $t^\sigma \in \downarrow\uparrow$-Plays($\sigma$) and $t^\tau \in \downarrow\uparrow$-Plays($\tau$) s.t. $s^\sigma = \partial_{\Lambda(\sigma)}(t^\sigma)$ and $s^\tau = \partial_{\Lambda(\tau)}(t^\tau)$ from Lemma 6.3, we have $\varphi(t^\sigma) \cong_\tau t^\tau$ as in (the obvious generalization of) Definition 2.11.

For $s^\sigma$ empty it is clear. For $s^\sigma m_1^- \in \downarrow\uparrow$-Unf($\sigma$) and $s^\tau m_2^- \in \downarrow\uparrow$-Unf($\tau$) with $s^\sigma m_1^- \cong_{A\vdash B} s^\tau m_2^-$, there is a unique matching $t^\sigma n_1^- \in \downarrow\uparrow$-Plays($\sigma$). So $\varphi(t^\sigma)\varphi(n_1) \in \downarrow\uparrow$-Plays($\tau$), and by induction hypothesis $\varphi(t^\sigma) \cong_\tau t^\tau$. Moreover, from $s^\sigma m_1^- \cong_A s^\tau m_2^-$ and $\partial_{\Lambda(\tau)} \circ \varphi \sim \partial_{\Lambda(\sigma)}$,

$\partial_{\Lambda(\tau)}(\varphi(t^{\sigma})\varphi(n_1)) \cong_{A \vdash B} \partial_{\Lambda(\tau)}(t^{\tau}n_2),$

so $\varphi(t^\sigma)\varphi(n_1) \cong_\tau t^\tau n_2$ by $\sim$-receptivity of $\tau$.

Now, using this auxiliary statement we prove the lemma. For $s^\sigma m_1^+ \in \downarrow\uparrow$-Unf($\sigma$) and $s^\tau m_2^+ \in \downarrow\uparrow$-Unf($\tau$) with $s^\sigma m_1^+ \cong_{A\vdash B} s^\tau m_2^+$, take $t^\sigma n_1 \in \downarrow\uparrow$-Plays($\sigma$) and $t^\tau n_2 \in \downarrow\uparrow$-Plays($\tau$) s.t. $\partial_{\Lambda(\sigma)}(t^\sigma n_1) = s^\sigma m_1$ and $\partial_{\Lambda(\tau)}(t^\tau n_2) = s^\tau m_2$. By induction hypothesis, $\varphi(t^\sigma) \cong_\tau t^\tau$. As the former extends with $\varphi(n_1)$, by extension for $\mathcal{S}(\tau)$ there is some (positive) $n'_2$ s.t. $\varphi(t^\sigma)\varphi(n_1) \cong_\tau t^\tau n'_2$ but now, by reachable determinism of $\tau$, $n_2 = n'_2$. $\square$

In particular, if $\sigma : A \vdash B$ is sequential, then $\sigma \approx \sigma$ via the identity isomorphism,
consequently $\downarrow\uparrow$-Unf($\sigma$) $\approx$ $\downarrow\uparrow$-Unf($\sigma$), i.e. $\downarrow\uparrow$-Unf($\sigma$) is uniform – from here we conclude:

**Proposition 6.5.** *Consider A, B --arenas, and $\sigma : A \vdash B$ a sequential causal strategy.*
*Then, $\downarrow\uparrow$-Unf($\sigma$) : $A \to B$ is a P-visible alternating strategy.*

<footnote>21This was done by Laird in the first interleaving games model [Lai01b], via explicit threading information.</footnote>

<footnote>22Proposition 4.46 shows that non-visible behaviour characteristic of higher-order state can be mimicked by running several threads in parallel and using signaling via *interference* to jump control between them.</footnote>
<figure><img src="image_71.png" /><figcaption>Figure 52: State diagram for sequential interactions</figcaption></figure>

*Proof.* *Prefix-closure* and *receptivity* are clear. *Determinism* is immediate from Lemma 6.3 and *sequential determinism*, and *uniformity* is immediate from Lemma 6.4.

Finally, *P-visibility* is immediate by definition of *sequential visibility*. $\square$

6.1.3. *Composition.* We now focus on composition of sequential causal strategies.

We introduce some terminology. If $A, B$ and $C$ are $\neg$-arenas and $\sigma : A \vdash B, \tau : B \vdash C$ are causal (pre)strategies, then we define $\mathcal{C}\text{-Plays}(\tau \circledast \sigma)$ as in Definition 3.18, referring to polarities of events in $\{-, l, r\}$. If $u \in \mathcal{C}\text{-Plays}(\tau \circledast \sigma)$, we write $u_\sigma \in \mathcal{C}\text{-Plays}(\sigma)$, $u_\tau \in \mathcal{C}\text{-Plays}(\tau)$, and $u_\odot \in \mathcal{C}\text{-Plays}(\tau \odot \sigma)$ for the obvious restrictions. If a play is alternating, it is **in state O** if it has even-length, and **in state P** if it has odd length.

Many properties of causal sequentiality follow from the following crucial observation:

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

Then, for any $u \in \mathcal{C}\text{-Plays}(\tau \circledast \sigma)$ such that $u_\odot \in \downarrow\uparrow\text{-Plays}(\tau \odot \sigma)$, we have $u_\sigma \in \downarrow\uparrow\text{-Plays}(\sigma)$ and $u_\tau \in \downarrow\uparrow\text{-Plays}(\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{C}\text{-Plays}(\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 induction hypothesis, $u_\sigma$ is alternating in state $O$, so ends with a Player move. But so, $u_\sigma m_\sigma^+ \in \mathcal{C}\text{-Plays}(\sigma)$ with $u_\sigma \in \downarrow\uparrow\text{-Plays}(\sigma)$, so $u_\sigma m_\sigma \in \downarrow\uparrow\text{-Plays}(\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 that $m$ occurs in $A$. Since $u_\odot \in \downarrow\uparrow\text{-Plays}(\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$

In other words, 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 52. None of the interacting agents can be the first to break alternation, so the interaction ends up fully alternating. It follows that $\tau \odot \sigma$ satisfies reachable sequentiality:

**Lemma 6.7.** *Consider $\sigma : A \vdash B, \tau : B \vdash C$ sequential causal (pre)strategies.*

Then, $\tau \odot \sigma$ satisfies reachable sequentiality.
**Proof.** Consider $tn^+ \in \mathcal{C}-\text{Plays}(\tau \odot \sigma)$ s.t. $t \in \downarrow\uparrow$-Plays$(\tau \odot \sigma)$. We have either $n_\sigma$ or $n_\tau$ defined and positive, say the former w.l.o.g.. Let us complete $tn$ to $un \in \mathcal{C}-\text{Plays}(\tau \circledast \sigma)$. We have $u_\odot = t \in \downarrow\uparrow$-Plays$(\tau \odot \sigma)$, so by may distinduish along the three cases of Lemma 6.6:

(1) If $u_\sigma, u_\tau, u_\odot$ are in state $O, O, O$. By hypothesis, $u_\sigma n_\sigma^+ \in \mathcal{C}-\text{Plays}(\sigma)$. Since $\sigma$ satisfies reachable sequentiality, $u_\sigma n_\sigma \in \downarrow\uparrow$-Plays$(\sigma)$ as well, contradicting $u_\sigma$ in state $O$.

(2) If $u_\sigma, u_\tau, u_\odot$ are in state $O, P, P$, as in (1) this contradicts reachable sequentiality.

(3) If $u_\sigma, u_\tau, u_\odot$ are in state $P, O, P$. With $u_\odot = t$ in state $P$, $tn \in \downarrow\uparrow$-Plays$(\tau \odot \sigma)$. $\square$

It also follows that $\tau \odot \sigma$ satisfies sequential determinism: Lemma 6.6 expresses that in an alternatingly reachable interaction, only one agent has control at any point. So any alternatingly reachable non-deterministic choice in $\tau \odot \sigma$ can be attributed to $\sigma$ and $\tau$:

**Lemma 6.8.** Consider $\sigma : A \vdash B$ and $\tau : B \vdash C$ sequential causal (pre)strategies.
Then, $\tau \odot \sigma$ satisfies sequential determinism.

**Proof.** Consider $tn_1^+, tn_2^+ \in \downarrow\uparrow$-Plays$(\tau \odot \sigma)$ completed to $u_1n_1, u_2n_2 \in \mathcal{C}-\text{Plays}(\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 t$, so in particular $t' \in \downarrow\uparrow$-Plays$(\tau \odot \sigma)$.

We distinguish cases on Lemma 6.6 applied to $u'$. For (1), $m_1$ and $m_2$ must both be the next negative event appearing in $t$, so $m_1 = m_2$, contradiction. For (2), $m_1$ and $m_2$ both have polarity $r$ and we have $u'_\tau \in \downarrow\uparrow$-Plays$(\tau)$, $u'_\tau(m_1)_\tau^+, u'_\tau(m_2)_\tau^+ \in \downarrow\uparrow$-Plays$(\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. Finally, for (3), then the reasoning is symmetric. $\square$

To conclude compositionality, we link with composition of the alternating projections:

**Lemma 6.9.** Consider $\sigma : A \vdash B$ and $\tau : B \vdash C$ sequential causal (pre)strategies.
Then, $\downarrow\uparrow$-Unf$(\tau \odot \sigma) = \downarrow\uparrow$-Unf$(\tau) \odot \downarrow\uparrow$-Unf$(\sigma)$.

**Proof.** $\supseteq$. If $s \in \downarrow\uparrow$-Unf$(\tau) \odot \downarrow\uparrow$-Unf$(\sigma)$, then it is in $\mathcal{C}-\text{Unf}(\tau) \odot \mathcal{C}-\text{Unf}(\sigma)$, thus in $\mathcal{C}-\text{Unf}(\tau \odot \sigma)$ by Proposition 4.30. As $s$ is alternating, we also have $s \in \downarrow\uparrow$-Unf$(\tau \odot \sigma)$.

$\subseteq$. If $s \in \downarrow\uparrow$-Unf$(\tau \odot \sigma)$, there is $t \in \downarrow\uparrow$-Plays$(\tau \odot \sigma)$ s.t. $s = \partial_{\Lambda(\tau \odot \sigma)}(t)$ completed to $v \in \mathcal{C}-\text{Plays}(\tau \circledast \sigma)$. We display $v$ to $u \in \mathcal{C}-\text{Unf}(\tau) \circledast \mathcal{C}-\text{Unf}(\sigma)$ s.t. $u \upharpoonright A, C = s$. But then, by Lemma 6.6, $v_\sigma \in \downarrow\uparrow$-Plays$(\sigma)$ and $v_\tau \in \downarrow\uparrow$-Plays$(\tau)$, so $u \upharpoonright A, B$ and $u \upharpoonright B, C$ are actually alternating, and $u \in \downarrow\uparrow$-Unf$(\tau) \circledast \downarrow\uparrow$-Unf$(\sigma)$. Thus, $s \in \downarrow\uparrow$-Unf$(\tau) \odot \downarrow\uparrow$-Unf$(\sigma)$. $\square$

**Proposition 6.10.** There is a category $\rightarrow$-Strat$^{\text{seq}}$ of $\rightarrow$-arenas and sequential strategies.
Moreover, there is a functor $\downarrow\uparrow$-Unf($-$) : $\rightarrow$-Strat$^{\text{seq}} \rightarrow \downarrow\uparrow$-Strat$^{\text{vis}}$, preserving $\approx$.

**Proof. Category.** It is straightforward that copycat is sequential. Consider $\sigma : A \vdash B$ and $\tau : B \vdash C$ sequential causal strategies. By Lemma 6.7, $\tau \odot \sigma$ satisfies reachable sequentiality. By Lemma 6.8, it satisfies sequential determinism. By Lemma 6.9 and preservation of P-visible alternating strategies under composition, it satisfies sequential visibility.

**Functorial projection.** Preservation of copycat is a direct verification. Preservation of composition is Lemma 6.9. Preservation of symmetry is Lemma 6.4. $\square$

6.1.4. *Seely category.* We now show that sequential causal strategies form a Seely category.

We use the following notations, for $\sigma : A \vdash B$ and $\tau : C \vdash D$: if $s \in \mathcal{C}-\text{Plays}(\sigma \otimes \tau)$, then $s_\sigma \in \mathcal{C}-\text{Plays}(\sigma)$ and $s_\tau \in \mathcal{C}-\text{Plays}(\tau)$ are the corresponding restrictions, defined in the obvious way. Stability of sequentiality under tensor uses a state analysis as in Lemma 6.6:
**Lemma 6.11.** Consider $\sigma : A \vdash B$ and $\tau : C \vdash D$ sequential (pre)strategies. For any $s \in \downarrow\uparrow$-Plays($\sigma \otimes \tau$) then $s_\sigma \in \downarrow\uparrow$-Plays($\sigma$) and $s_\tau \in \downarrow\uparrow$-Plays($\tau$). Moreover, we are in 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$.

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

Again, this is the familiar state diagram for alternating plays on a tensor of strategies, see e.g. [Har04]. Finally, there is a state diagram for the functorial action of the exponential – as for tensor, if $s \in \mathcal{O}$-Plays($!\sigma$), we write $s_i$ for its restriction on copy index $i$.

**Lemma 6.12.** Consider $\sigma : A \vdash B$ be a sequential (pre)strategy.

For any $s \in \downarrow\uparrow$-Plays($!\sigma$), then for any $i \in \mathbb{N}$, $s_i \in \downarrow\uparrow$-Plays($\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$ and $\tau$. $\square$

As for composition, the preservation of *reachable sequentiality* and *sequential determinism* under composition are immediate applications. We omit the easy verifications that the alternating projection is compatible with tensor and bang; from which – as for composition – it follows that sequential visibility is preserved. All structural strategies involved in the Seely category structure, being variants of copycat, are easily proved sequential. Overall, we have:

**Proposition 6.13.** There is a Seely category $\dashrightarrow$-Strat$^{seq}$ of $\dashleftarrow$-arenas and sequential strategies. Moreover, $\downarrow\uparrow$-Unf($-$) : $\dashrightarrow$-Strat$^{seq}$ $\rightarrow$ $\downarrow\uparrow$-Strat$^{vis}$ preserves $\approx$ and the Seely structure.

## 6.2. Full Abstraction for IA. Next, we fine-tune $\dashrightarrow$-Strat$^{seq}$ to get full abstraction for IA.

### 6.2.1. Interpretation of IA.
It only remains to prove that the interpretation of the primitives of IA, i.e. all primitives of $IA_\parallel$ except for the parallel let, are sequential. We have:

**Lemma 6.14.** The strategies seq, succ, if, iszero, let, assign, deref, grab, release and the prestrategies cell$_n$ and lock$_n$ are sequential. Moreover, for each of those (pre)strategies $\sigma$, $\downarrow\uparrow$-Unf($\sigma$) is the corresponding alternating strategy from Sections 2.3.5 and 3.4.3.

*Proof.* Routine verification. $\square$

It follows that we have an adequate interpretation of IA as sequential strategies, and:

**Proposition 6.15.** For any $\Gamma \vdash M : A$ in IA, we have $[[M]]_{\downarrow\uparrow\text{-Strat}_i^{\text{vis}}} = \downarrow\uparrow$-Plays($[[M]]_{\dashrightarrow\text{-Strat}_i^{\text{seq}}}$).

*Proof.* Straightforward by induction on the derivation $\Gamma \vdash M : A$. $\square$

The two adequate models of IA, $\downarrow\uparrow$-Strat$_i^{\text{vis}}$ and $\dashrightarrow$-Strat$_i^{\text{seq}}$, differ in crucial ways: $\dashrightarrow$-Strat$_i^{\text{seq}}$ is much more expressive, and records intensional *causal* information. Secondly, in $\dashrightarrow$-Strat$_i^{\text{seq}}$ one can also read the behaviour of the program under contexts outside IA.

However, $\dashrightarrow$-Strat$_i^{\text{seq}}$ is not fully abstract for IA – we need to deal with well-bracketing.
<figure><img src="image_72.png" /><figcaption>Figure 53: Definition 3.20 is weaker than Definition 3.2</figcaption></figure>

6.2.2. *Well-bracketing.* Ideally, we would love to have an interpretation-preserving functor

$$ \downarrow\uparrow\text{-Plays}(-) : \text{-Strat}_i^{\text{wb,seq}} \to \downarrow\uparrow\text{-Strat}_i^{\text{wb,vis}}, $$

but Definition 3.20 (for non-alternating plays) is weaker than Definition 3.2 (for alternating plays) when applied on alternating plays, as illustrated in Figure 53. While Definition 3.2 closely follows the operational idea that calls and returns are handled by a single stack, Definition 3.20 restricts the hierarchical relationship between calls and returns.

Fortunately, from a distinguishing test in $\text{-Strat}_i^{\text{wb,seq}}$ one can extract a characteristic complete (see Section 3.4.4) alternating play, which – as we shall see – is well-bracketed as in Definition 3.2. This is due to the following lemma, a well-known observation:

**Lemma 6.16.** Let $s \in \downarrow\uparrow\text{-Plays}(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 proof appears in [CH10, Lemma 5]. $\square$

From this, we may easily deduce the following:

**Lemma 6.17.** Any $s \in \downarrow\uparrow\text{-Plays}(A)$ complete is well-bracketed in the sense of Definition 3.2.

*Proof.* Consider $s \in \downarrow\uparrow\text{-Plays}(A)$ complete but with 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 6.16, no further move can point to $q_2$, contradicting that $s$ is complete. $\square$

The play of Figure 53 is well-bracketed as in Definition 3.20, but it cannot be extended to a complete play: the two questions covered will not be addressed ever again.

6.2.3. *Full abstraction.* From that, we may finally conclude:

**Theorem 6.18.** The model $\text{-Strat}_i^{\text{wb,seq}}$ is intensionally fully abstract for IA.

*Proof.* Let $\vdash M, N : A$ be terms in IA, and assume that $[M] \uplus [N]$, i.e. there is a test $\alpha \in \text{-Strat}_i^{\text{wb,seq}}([A], [U])$ such that $\alpha \odot! [M] \neq \alpha \odot! [N]$ – assume w.l.o.g. that $\alpha \odot! [M]$ converges while $\alpha \odot! [M]$ diverges. Writing $\alpha' = \downarrow\uparrow\text{-Unf}(\alpha)$, it follows that

$$ \alpha' \odot! [M] \downarrow\uparrow\text{-Strat}_i^{\text{wb,vis}} \downarrow \qquad \alpha' \odot! [N] \downarrow\uparrow\text{-Strat}_i^{\text{wb,vis}} \uparrow, $$
but $\alpha'$ may not be well-bracketed as in Definition 3.3. Consider $s \in \alpha'$ involved in $\alpha' \odot! [[M]] \downarrow$ until the rest of the proof, $[[M]]$ is the interpretation in $\downarrow\uparrow$-Strat$_!^{wb,vis}$. The initial question of $s$ has an answer, thus as $[[M]]$ and $\alpha'$ are well-bracketed in the sense of 3.21, all its questions are answered. It is P-visible and O-visible since both $[[M]]$ and $\alpha'$ are P-visible. Hence, it is complete, and so by Lemma 6.17, it is well-bracketed in the sense of Definition 3.3.

Consider $\alpha'$ restricted to (plays symmetric to) prefixes of $s$. Now $\alpha'$ is well-bracketed as in Definition 3.2, and it distinguishes $[[M]]$ and $[[N]]$, hence $M \nrightarrow N$ by Theorem 3.14. $\square$

**6.3. Sequential Innocence.** A causal strategy $\sigma: A$ is sequential innocent if it is both sequential and parallel innocent; those form a Seely category $\rightarrow\sigma$-Strat$^{wb,seq,inn}$.

We already know that $\rightarrow\sigma$-Strat$^{wb,seq,inn}$ supports an adequate interpretation of PCF. For (intensional) full abstraction, we shall prove that $\downarrow\uparrow$-Unf($-$) sends sequential innocent strategies to innocent alternating strategies as in Definition 3.6, and rely on Theorem 3.10.

**6.3.1. Causal analysis of sequential innocence.** First, we shall see that sequential innocent causal strategies are really representations of the *P*-view forests of Section 3.2.

**Lemma 6.19.** Consider $\sigma: A$ a sequential, parallel innocent causal 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 A.3, $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'$ is the only immediate dependency of $m_1$ and $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 $m'$, contradicting its minimality. Hence, $[m'] \cup \{m_i\} \in \mathcal{C}(\sigma)$ for $i \in \{1, 2\}$.

Also writing $[m']$ for the play in $\downarrow\uparrow$-Plays($\sigma$) with events in the same order, we have

$$[m'], [m']m_1, [m']m_2 \in \mathcal{C}-\text{Plays}(\sigma),$$

but by Lemma A.3, $[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^- \rightarrow m_1^+$ and $m^- \rightarrow m_2^+$ in $\sigma$, by sequential determinism and the same reasoning as above, $m_1 = m_2$, so $\sigma$ is O-branching. Finally, as for any causal strategy $\sigma: A$ on $A$ alternating, we have $\rightarrow_{\sigma}$ is alternating as well. $\square$

Let us call a **branch** of sequential innocent $\sigma: A$ a $s = m_1...m_n \in \downarrow\uparrow$-Plays($\sigma$) s.t.

$$m_1 \rightarrow_{\sigma} \dots \rightarrow_{\sigma} m_n \in \text{gcc}(\sigma).$$

Then, $\partial_{\sigma}(s) \in \downarrow\uparrow$-Plays($A$), but there is more: by courtesy of $\sigma$, if $m_i^+ \rightarrow_{\sigma} m_{i+1}^-$ then $\partial_{\sigma}(m_i) \rightarrow_A \partial_{\sigma}(m_{i+1})$, i.e. $\partial_{\sigma}(m_{i+1})$ points to $\partial_{\sigma}(m_i)$ in $\partial_{\sigma}(s)$. In other words, $\partial_{\sigma}(s)$ is actually a *P*-view, i.e. an alternating play where Opponent always points to the previous move. One can display a sequential innocent causal strategy to a forest of P-views as in Section 3.3.1: we have recovered, as the causal structure of sequential innocent causal strategies, the forest of P-views "$\sigma$", the "causal presentation" of alternating innocent
<figure><img src="image_73.png" /><figcaption>Figure 54: Innocence witness for Figure 16</figcaption></figure>

<figure><img src="image_74.png" /><figcaption>Figure 55: An alternative presentation</figcaption></figure>

strategies from Proposition 3.7. This connection confirms that the causal strategies of Section 5 are generalizations of the sets of P-views of traditional innocence<fnref n="23" />.

### 6.3.2. P-views are the causal dependency.
This gives two ways to get plays from $\sigma$: A sequential innocent: following Section 3.3.1, by selecting those plays whose P-views appear in the causal representation; and following Section 5, as displays of alternating plays over $\sigma$ – we must prove them identical. Figure 54 shows the augmentation explored in the play of

$$ [[\lambda f^{U \to U} . f \text{skip}; f \text{skip}; tt]] : [[U \to U) \to B]] $$

in Figure 16 – the numbers in red correspond to the order in which that augmentation is explored. The reader should take some time to digest this picture, and in particular observe that for each prefix of the play in Figure 16, the P-view is exactly (the display of) 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 with 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="24" />.

As an aside, in Figure 55, we give an alternative presentation of the same augmentation, making explicit how an augmentation of a sequential innocent strategy consists is the underlying configuration (here, Figure 11), enriched with immediate causal links. The set of (isomorphism classes of) configurations reached is essentially the information recorded by the relational model; so this presentation shows plainly that innocent game semantics consist in enriching the relational model with explicit causal / temporal information.

Back to the technical development, we must prove that if $\sigma: A$ is sequential innocent, then $\downarrow\uparrow$-Unf($\sigma$) is innocent as in Definition 3.6. This relies on a link between P-views and the causal structure of $\sigma: A$, which should be expected in the light of Figure 54.

<footnote n="23">²³This shows that the causal reasoning permitted by traditional innocence, one of the main tools of traditional game semantics, is not inherently restricted to innocence. This is a powerful observation, and much of the subsequent line of work in concurrent games has consisted in exploring its implications.</footnote>

<footnote n="24">²⁴Different explorations of the same augmentation 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 [Mel04].</footnote>
**Lemma 6.20.** Consider A, B --arenas and $\sigma$: A $\vdash$ B sequential innocent.
Then, for any $tm \in \downarrow\uparrow$-Plays($\sigma$), we have $\mathring{\partial}_{\Lambda(\sigma)}(tm)^{\mathring{\prime}} = \partial_{\Lambda(\sigma)}([m]_{\sigma})$.

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

The crucial observation is that $tm^{-}n^{+} \in \downarrow\uparrow$-Plays($\sigma$), then necessarily $m^{-} \to_{\sigma} n^{+}$.
To prove that, we prove by induction on $t$ that for any $t \in \downarrow\uparrow$-Plays($\sigma$): (1) if $t$ has even length, then all maximal events of $|t| \in \mathscr{C}(\sigma)$ are positive; and (2) if $t$ has odd length, then $|t| \in \mathscr{C}(\sigma)$ has exactly one maximal negative event. Indeed, for $tm^{-} \in \downarrow\uparrow$-Plays($\sigma$), then $t$ has even length, so $|t|$ has all its maximal events positive. But then $|tm^{-}|$ has exactly one maximal negative event, namely $m^{-}$. Likewise, for $tm^{+} \in \downarrow\uparrow$-Plays($\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 6.19, and in particular the fact 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^{-} \to_{\sigma} n^{+}$ as required.

Likewise, if $t_1m^+t_2n^- \in \downarrow\uparrow$-Plays($\sigma$) s.t. $\partial_{\Lambda(\sigma)}(m) \to_A \partial_{\Lambda(\sigma)}(n)$ – so $\mathring{\partial}_{\Lambda(\sigma)}(t_1mt_2n)^{\mathring{\prime}} = \mathring{\partial}_{\Lambda(\sigma)}(t_1)^{\mathring{\prime}}\mathring{\partial}_{\Lambda(\sigma)}(m)\mathring{\partial}_{\Lambda(\sigma)}(n)$ then we must have $m \to_{\sigma} n$ by Lemma A.4. From these two facts, the lemma is a direct verification by induction on $t$. $\square$

6.3.3. Innocent alternating unfolding. From the above, we may now deduce:

**Proposition 6.21.** Consider A, B --arenas, and $\sigma$: A $\vdash$ B a sequential causal strategy.
If $\sigma$ is parallel innocent, then $\downarrow\uparrow$-Unf($\sigma$) is innocent as in Definition 3.6.

*Proof.* First, we must show that $\downarrow\uparrow$-Unf($\sigma$) is P-visible. In other words, we must prove that for all $s \in \downarrow\uparrow$-Unf($\sigma$), $\mathring{s}' \in \downarrow\uparrow$-Plays($A \to B$). For the empty play there is nothing to prove; so consider $sa \in \downarrow\uparrow$-Unf($\sigma$) and $tm \in \downarrow\uparrow$-Plays($\sigma$) such that $sa = \partial_{\Lambda(\sigma)}(tm)$. Now, by Lemma 6.20, we have $\mathring{sa}' = \partial_{\Lambda(\sigma)}([m]_{\sigma})$, as plays – therefore $\mathring{sa}' \in \downarrow\uparrow$-Plays($A \to B$) as required.

Now, we prove innocence. Let $sa^{+}$, $s' \in \downarrow\uparrow$-Unf($\sigma$) such that $\mathring{s}' = \mathring{s}'$. By definition, there is $tm^{+} \in \downarrow\uparrow$-Plays($\sigma$) and $t' \in \downarrow\uparrow$-Plays($\sigma$) such that $sa = \partial_{\Lambda(\sigma)}(tm)$ and $s' = \partial_{\Lambda(\sigma)}(t')$.

Now, by Lemma 6.20, $\mathring{sa}' = \partial_{\Lambda(\sigma)}([m]_{\sigma})$ as plays, hence also $\mathring{s}' = \partial_{\Lambda(\sigma)}([n]_{\sigma})$ for $n \to_{\sigma} m$. Again by Lemma 6.20, $\mathring{s}' = \partial_{\Lambda(\sigma)}([n']_{\sigma})$ for $n'$ the last move of $t'$. Since $\mathring{s}' = \mathring{s}'$, by Lemma 6.3, $[n]_{\sigma} = [n']_{\sigma}$. So, $|t'| \cup \{m\}$ is down-closed. Finally, $|t'| \cup \{m\}$ is negatively compatible since $|t'| \in \mathscr{C}(\sigma)$ and $m$ is positive, hence $|t'| \cup \{m\}$ is compatible as $\sigma$ satisfies *causal determinism*. Therefore, $t'm \in \downarrow\uparrow$-Plays($\sigma$), and $s'm = \partial_{\Lambda(\sigma)}(t'm) \in \downarrow\uparrow$-Unf($\sigma$). $\square$

Altogether, we have proved the following proposition:

**Proposition 6.22.** There is a Seely category $\to$-Strat$^{seq,inn}$ of --arenas and sequential strategies. Moreover, the alternating unfolding preserves $\approx$ and the Seely category structure:

$$ \downarrow\uparrow\text{-Unf}(-) : \to\text{-Strat}^{\text{seq,inn}} \to \downarrow\uparrow\text{-Strat}^{\text{inn}}. $$

*Proof.* It suffices to prove that the functor of Proposition 6.13 sends sequential innocent causal strategies to innocent alternating strategies, which we know by Proposition 6.21. $\square$

We are now equipped to show full abstraction for PCF.
**6.3.4.** Full abstraction for PCF. We show that $\rightarrow\text{-Strat}^{\text{wb,seq,inn}}$ is fully abstract for PCF.

**Theorem 6.23.** The model $\rightarrow\text{-Strat}^{\text{wb,seq,inn}}$ is intensionally fully abstract for PCF.

*Proof.* Let $\vdash M, N : A$ be terms in PCF s.t. $[[M]] \dot{\lor} [[N]]$, i.e. there is $\alpha : ![[A]] \vdash \mathbf{U}$ sequential innocent and well-bracketed such that, w.l.o.g., $\alpha \odot_! [[M]] \downarrow$ and $\alpha \odot_! [[N]] \uparrow$. Then, it follows

$$ \downarrow\uparrow\text{-Unf}(\alpha) \odot_! [[M]] \downarrow\uparrow\text{-Strat}_! \downarrow, \quad \downarrow\uparrow\text{-Unf}(\alpha) \odot_! [[N]] \downarrow\uparrow\text{-Strat}_! \uparrow, $$

with $\downarrow\uparrow\text{-Unf}(\alpha)$ well-bracketed by Proposition 3.15. Hence, $M \dot{\lor} N$ by Theorem 3.10. $\square$

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

## 7. FINITE DEFINABILITY AND FULL ABSTRACTION FOR PCF$_{‖}$

We have now established the following intensional full abstraction results:

$$ \begin{align*} \rightarrow\text{-Strat}_!^{\text{wb}} &\text{ is fully abstract for } IA_{\parallel}, \\ \rightarrow\text{-Strat}_!^{\text{wb}} + \textit{sequentiality} &\text{ is fully abstract for } IA, \\ \rightarrow\text{-Strat}_!^{\text{wb}} + \textit{parallel innocence} + \textit{sequentiality} &\text{ is fully abstract for } PCF, \end{align*} $$

and we are left with the one outstanding objective:

$$ \rightarrow\text{-Strat}_!^{\text{wb}} + \textit{parallel innocence} \text{ is fully abstract for } PCF_{\parallel}. $$

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

Proving finite definability for parallel innocent strategies involves many steps. In Section 7.1, we introduce a more convenient equivalence between parallel innocent strategies, *positional equivalence*. In Section 7.2 we show it suffices to consider tests that satisfy a stronger, *causal*, form of well-bracketing useful for definability. In Section 7.3 we introduce a notion of finiteness, and show that finite tests suffice. In Section 7.4, we show a factorization result, reducing finite definability to that for first-order strategies. In Section 7.5, we conclude the proof of finite definability. Finally, in Section 7.6, we prove intensional full abstraction for PCF$_{‖}$, concluding the technical contents of the paper.

**7.1. The Positional Collapse.** Definability will hold only with respect to *positional equivalence*, a congruence amounting to an equal projection in the relational model.

**7.1.1.** *Positions of arenas.* We will observe strategies only on certain *positions* of arenas.

**Definition 7.1.** Let A be an arena, and $x \in \mathscr{C}(A)$.

We say that $x$ is **complete** iff every question in $x$ has an answer in $x$.

*Complete* configurations mirror the *complete plays* of Section 3.4.4 and onwards. In both cases, all function calls have returned. The difference, however, is that complete plays are sequential whereas complete configurations are not: they are a “static” snapshot presenting all calls and returns and their hierarchical relationships, with no temporal information.

Besides, complete configurations also comprise the ad-hoc choice of copy indices for all replicable moves. So we quotient them out via the following variation.

**Definition 7.2.** Let A be an arena. The set of **positions** on A, ranged over by x, y, ..., is:

$$ \mathcal{A} = \{x \in \mathscr{C}(A) \mid x \text{ complete}\} / \cong_A . $$

If $x \in \mathscr{C}(A)$ is complete, we write $[x] \cong_A \mathcal{A}$ for its symmetry class.
<figure><img src="image_76.png" /><figcaption>Figure 56: Quotienting out evaluation order</figcaption></figure>

For instance, the configuration of Figure 11 is complete. The matching position is described intuitively by removing the grey subscripts, i.e. the copy indices.

### 7.1.2. Positions of strategies.
The positional collapse of a strategy is an explicit desequen-
tialization, obtained by forgetting the chronological ordering of complete plays.

**Definition 7.3.** Consider A an arena, and $\boldsymbol{\sigma}: A$ a causal strategy. The **positions** of $\boldsymbol{\sigma}$ are

$$
\int \boldsymbol{\sigma} = \{x \in \int A \mid \exists x \in \mathscr{C}(\boldsymbol{\sigma}), x = [\partial_{\boldsymbol{\sigma}}(x)]_{\cong} \}.
$$

For $\boldsymbol{\sigma}: A \vdash B$, positions are symmetry classes of parallel compositions $x_A \parallel x_B$, also written $x_A \parallel x_B$ for $x_A = [x_A]_{\cong}, x_B = [x_B]_{\cong}$. They correspond to pairs $(x_A, x_B) \in (fA) \times (fB)$ – so $\int \boldsymbol{\sigma}$ gives a relation from $fA$ to $fB$; accordingly we also write $(x_A, x_B) \in \int \boldsymbol{\sigma}$ for $x_A \parallel x_B \in \int \boldsymbol{\sigma}$.

We illustrate the construction in Figure 56: the example illustrates how, by only keeping
complete positions, the collapse forgets the evaluation order. We define:

**Definition 7.4.** Two causal strategies $\boldsymbol{\sigma}, \boldsymbol{\tau}: A$ are **positionally equivalent** iff $\int \boldsymbol{\sigma} = \int \boldsymbol{\tau}$.
We write $\boldsymbol{\sigma} \equiv \boldsymbol{\tau}$ to denote the fact that $\boldsymbol{\sigma}$ and $\boldsymbol{\tau}$ are positionally equivalent.

This is a drastic quotient, identifying sequential and parallel evaluation. It will help tremendously in our definability procedure, which will not respect the evaluation order. Of course, the more drastic the quotient, the more challenging the corresponding proof obligation that it is preserved by operations on strategies – and in particular by composition.

7.1.3. *Deadlocks*. Stability of positional equivalence by composition boils down to

$$
f(-) : \dashrightarrow \text{Strat} \rightarrow \text{Rel}
$$

being functorial, where Rel is the usual category of *sets and relations*.

For morphisms $\boldsymbol{\sigma} \in \dashrightarrow\text{Strat}(A, B)$, we have defined $\int \boldsymbol{\sigma} \in \text{Rel}(\int A, \int B)$. But for now, this operation has no reason to preserve composition! In fact neither inclusion holds: firstly, $\int (\boldsymbol{\tau} \odot \boldsymbol{\sigma}) \subseteq (\int \boldsymbol{\tau}) \odot (\int \boldsymbol{\sigma})$ may fail as a complete configuration may arise through an interaction involving a non-complete configuration on $B$. We shall see later on that this can be salvaged by restricting to *well-bracketed* causal strategies, ensuring that an interaction producing a complete configuration on $A \vdash C$ will only involve a complete configuration on $B$.

However the other direction also fails, and the diagnosis is more serious. To construct
$(x_A, x_C) \in (f\tau) \odot (f\sigma)$, one provides $x_B \in fB$ mediating for relational composition, so

$$
(x_A, x_B) \in \int \sigma, \quad (x_B, x_C) \in \int \tau,
$$
<figure><img src="image_77.png" /><figcaption>Figure 57: Deadlocking composition of causal strategies</figcaption></figure>

i.e. with $x^\sigma \in \mathscr{C}(\sigma)$ and $x^\tau \in \mathscr{C}(\tau)$ s.t. writing $\partial_\sigma x^\sigma = x_A^\sigma \parallel x_B^\tau$ and $\partial_\tau x^\tau = x_B^\tau \parallel x_A^\sigma$, $x_A^\sigma \in \chi_A$, $x_C^\tau \in \chi_C$, and $x_B^\sigma, x_B^\tau \in \chi_B$, so $x_B^\sigma \cong_B x_B^\tau$ match *up to symmetry*. In other words, we must provide a *witness position* that both strategies agree (up to symmetry) is *reachable*.

On the other hand, composition of strategies is more rigid: not only should the projections of $x^\sigma$ and $x^\tau$ on $B$ match, they should also arrive at this position *in the same chronological ordering*. This is not always possible: these two notions of composition differ when interaction triggers a *causal deadlock*, i.e. pairs of configurations that are *matching* but not *secured* as in Definition 4.5. Figure 57 displays an example: the strategy obtained by composition has no response to the initial Opponent move, while relational composition authorizes $0^+$.

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

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

**Lemma 7.5.** Consider $A, B$ --arenas, $\sigma: A \vdash B$ visible, and $m, m' \in |\sigma|$ s.t. $m <_\sigma m'$. Then, just($m'$) is comparable with $m$ with respect to $\leq_{\sigma}$.

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

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

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

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

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

We saw in Definition 4.5 and Proposition 4.7 that $(x^\sigma, x^\tau)$ corresponds to a configuration of the interaction $\tau \circledast \sigma$ exactly when this bijection is *secured*, i.e. $\prec$ is acyclic.
If $\sigma: A \vdash B$ and $\tau: B \vdash C$ are visible, we claim that this is always the case. We reason by contradiction: starting with a putative deadlock, we repeatedly push it down the causal dependency of the arena, until it reaches a minimal event – but those cannot appear in a cycle. Before giving the formal proof, we showcase the reasoning on a simplified case.

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

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

an immediate causal incompatibility between $p_1$ and $p_2$. In other words we have $p_1 \triangleleft p_2$ and $p_2 \triangleleft p_1$, and we use $p_1 \triangleleft_{\sigma} p_2$ and $p_2 \triangleleft_{\tau} p_1$ to indicate the origin of the causal constraint. Finally, we apply the same conventions for polarity of elements of $\varphi$ as in Section 4.2.6.

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

$$p_1^r \underset{\triangleleft}{\stackrel{\triangleleft}{\circlearrowleft}} p_2^l,$$

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

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

so simple deadlocks between $p_1$ and $\text{just}(p_2)$; or between $\text{just}(p_1)$ and $p_2$. The cumulative depth in $B$ has decreased. The case $p_1 = \text{just}(p_2)$ or $p_2 = \text{just}(p_1)$ is easily discarded.

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

$$\text{just}(p_1) \underset{\triangleleft}{\stackrel{\triangleleft}{\circlearrowleft}} \text{just}(p_2),$$

closer to the root of the arena. Repeating this we eventually hit an impossible simple deadlock with a minimal event in $B$, finally exposing the contradiction. So visibility *structures* the interaction around the dependency of the arena, giving us an effective reasoning principle.

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

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

$\varphi: x^{\sigma} \parallel x_C^{\tau} \stackrel{\partial_{\sigma} \parallel x_C^{\tau}}{\cong} x_A^{\sigma} \parallel x_B^{\sigma} \parallel x_C^{\tau} \stackrel{x_A^{\sigma} \parallel \theta \parallel x_C^{\tau}}{\cong} x_A^{\sigma} \parallel x_B^{\tau} \parallel x_C^{\tau} \stackrel{x_A^{\sigma} \parallel \partial_{\tau}^{-1}}{\cong} x_A^{\sigma} \parallel x^{\tau},$ \\
is secured, in the sense that the relation $\triangleleft$, defined on the graph of $\varphi$ with

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

whenever $l (<_{\sigma} <_{C}) l'$ or $r (<_{A} <_{\tau}) r'$, is acyclic$^{25}$.

<footnote>$^{25}$For $\theta$ an identity, this exactly means that $x^{\sigma}$ and $x^{\tau}$ satisfy the *secured* condition of Definition 4.5.</footnote>
Proof. We use polarities l, r or – for elements of $\varphi$ (i.e. pairs $(l, r)$) as in Section 4.2.6. We say $(l, r)$ occurs in A, B or C in the obvious sense. We use a notion of *justifier* of a pair $(l, r)$ non-minimal in B: as $\theta$ is an order-isomorphism, $\partial_{\sigma}(l)$ is minimal in B iff $\partial_{\tau}(r)$ is. If not, then just($l$) and just($r$) also match up to $\theta$ and (just($l$), just($r$)) must be in $\varphi$ as well – we write it just($l, r$). Suppose now $\triangleleft$ is not secured, i.e. there is $((l_1, r_1), \dots, (l_n, r_n))$ with

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

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

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

then it is easy to prove that $r_i <_{\tau} r_{i+1} <_{\tau} \dots <_{\tau} r_{j-1} <_{\tau} r_j$, so that $p_i^{(B)} \triangleleft p_j^{(B)}$ and the cycle can be shortened, contradicting its minimality – the same argument holds for A.

We restrict to cycles in B. The **depth** of $(l, r)$ is the length of the chain of justifiers to $(l_0, r_0)$ minimal in B – the depth of $(l_0, r_0)$ minimal in B is 0. The depth of the cycle is

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

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

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

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

with $p_{2k+1} \triangleleft_{\tau} p_{2k+2}$ and $p_{2k+2} \triangleleft_{\sigma} p_{2k+3}$. Then, $r_{2k+1} <_{A} \tau r_{2k+2}$. From its polarity, $r_{2k+2} \triangleleft_{\sigma} r_{2k+3}$. cannot be minimal in B. By Lemma 5.8, it has a unique predecessor just($r_{2k+2}$) $\rightarrow_{A} \tau$, so $r_{2k+1} <_{A} \tau r_{2k+2}$. factors as $r_{2k+1} <_{A} \tau$ just($r_{2k+2}$) $\rightarrow_{A} \tau r_{2k+2}$. Accordingly, $p_{2k+1} \triangleleft_{\tau} just(p_{2k+2}) \triangleleft_{\sigma} p_{2k+2}$ – but dependencies in the game are respected by both strategies, so just($p_{2k+2}$) $\triangleleft_{\sigma} p_{2k+2}$. So just($p_{2k+2}$) $\triangleleft_{\sigma} p_{2k+3}$, and we can replace the cycle fragment with

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

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

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

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

with $p_{2k+2}$ minimal in B, then $l_{2k+2} <_{\sigma} l_{2k+3}$ with $l_{2k+2}$ minimal in B, but then $\partial_{\sigma} l_{2k+2} <_{A} \partial_{\sigma} l_{2k+3}$. Indeed, if $\partial_{\sigma} l_{2k+2}$ is minimal in B, $l_{2k+2}$ is (by courtesy) minimal in $\sigma$ $\parallel C$. Likewise, since $l_{2k+3}$ occurs in B, $\partial_{\sigma} l_{2k+3}$ depends (for $\le_{A} \parallel B \parallel C$) on a unique $\partial_{\sigma} l$ minimal in B, where $l$ must also be minimal in $\sigma$. But since $\sigma$ is pointed, $l_{2k+3}$ has a unique minimal dependency, hence $l = l_{2k+2}$ and $\partial_{\sigma} l_{2k+2} <_{A} \partial_{\sigma} l_{2k+3}$. as claimed. But then, $r_{2k+2} <_{A} \tau r_{2k+3}$, so $p_{2k+1}^{\mathrm{l}} \triangleleft_{\tau} p_{2k+2}^{\mathrm{r}} \triangleleft_{\sigma} p_{2k+3}^{\mathrm{l}}$ and again the cycle can be shortened by transitivity, contradicting its minimality.
Now, we have proved a minimal cycle has a canonical form where the strategies alternate, polarity alternates, all events are in B and non-minimal. Since $p_{2k}^r \triangleleft_\sigma p_{2k+1}^r$, writing $p = (l, r) = \text{just}(p_{2k+1})$, we have that $l = \text{just}(l_{2k+1})$ as well. From Lemma 7.5, we know that $l = \text{just}(l_{2k+1})$ is comparable with $l_{2k}$ in $\sigma \parallel C$ (by visibility of $\sigma$). If $\text{just}(l_{2k+1}) = l_{2k}$, then $r_{2k} \triangleleft_\tau r_{2k+1}$ as well. This gives $p_{2k-1} \triangleleft_\tau p_{2k+2}$, contradicting minimality of the cycle. So $\text{just}(l_{2k+1}) \neq l_{2k}$. Similarly, $\text{just}(r_{2k+2})$ is comparable with $r_{2k+1}$ in $A \parallel \tau$, but distinct.

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

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

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

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

which has the same length but smaller depth, absurd.

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

Despite its relatively discreet role in the development, we regard the deadlock-free lemma as one of our main contributions. It is a powerful observation with far-reaching consequences in linking game semantics and relational models. It also gives a lot of weight to the notion of visibility, as a simple, well-behaved and fairly general under-approximation of innocence.

7.1.5. *Preservation of composition.* For preservation of the positional collapse by composition, we need one further lemma: that any complete position is reachable by a *well-bracketed* play.

**Lemma 7.7.** *Take $\sigma : A$ visible well-bracketed on $--arena A$, $x^\sigma \in \mathscr{C}(\sigma)$ with $\partial_\sigma(x)$ complete. Then, there is $t \in \mathcal{U}\text{-Plays}(\sigma)$ such that $|t| = x^\sigma$ and $\partial_\sigma(t)$ is well-bracketed.*

*Proof.* The idea is simple: since $\sigma$ is well-bracketed, it suffices to show that $\partial_\sigma(x)$ is reachable by a well-bracketed Opponent. But we can set up causal constraints forcing Opponent to be well-bracketed, formulated as a visible causal strategy, and apply the deadlock-free lemma.

For $x \in \mathscr{C}(\sigma)$ s.t. $\partial_\sigma(x)$ complete, consider $x_A^\sigma$ as an arena with trivial symmetry. We build $\tau : x_A^\sigma \vdash U$ as $|\tau| = |x_A^\sigma \vdash U|$, and $\leq_{\tau}$ as the order of the arena enriched with:

<table><tr><td>(2, q)<sup>-</sup> &rarr; &tau;</td><td>(1, q)<sup>+, Q</sup></td><td>if q is an initial question in A,</td></tr><tr><td>(1, a)<sup>-, A</sup> &rarr; &tau;</td><td>(2, &uarr;)<sup>+</sup></td><td>if a answers an initial question in A,</td></tr><tr><td>(1, a<sub>1</sub>)<sup>-, A</sup> &rarr; &tau;</td><td>(1, a<sub>2</sub>)<sup>+, A</sup></td><td>if just(a<sub>2</sub>) &rarr;<sub>A</sub> just(a<sub>1</sub>),</td></tr></table>

resulting in $\tau$ visible well-bracketed. By Lemma 7.6, there is a linear ordering of $|x_A^\sigma \vdash U|$ compatible with the constraints of both $\sigma$ and $\tau$. As both are well-bracketed, its projection on the left gives $s \in \mathcal{U}\text{-Unf}(\sigma)$ such that $|s| = x_A^\sigma$ and $s$ well-bracketed as required. $\square$

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

If $\sigma$ and $\tau$ are well-bracketed and visible, then $f(\tau \odot \sigma) = (f\tau) \odot (f\sigma)$.

*Proof.* $\subseteq$. Consider $(x_A, x_C) \in f(\tau \odot \sigma)$. By definition, $x_A \parallel x_C = f(\partial_\tau \odot \sigma(x^\tau \odot x^\sigma))$ for $x^\tau \odot x^\sigma \in \mathscr{C}(\tau \odot \sigma)$ with $\partial_\tau \odot \sigma(x^\tau \odot x^\sigma) = x_A \parallel x_C$ complete, and $x_A = f(x_A, x_C = f(x_C)$. By Lemma 7.7, there is $s \in \mathcal{U}\text{-Unf}(\tau \odot \sigma)$ well-bracketed s.t. $|s| = \partial_\Lambda(\tau \odot \sigma)(x^\tau \odot x^\sigma)$. By Proposition 4.30, there is $u \in \mathcal{U}\text{-Unf}(\tau) \circled{\circ} \mathcal{U}\text{-Unf}(\tau)$ s.t. $u \vdash A, C = s$. Now, since $\sigma$ and $\tau$ are well-bracketed and $s$ is well-bracketed, it is direct by induction that $u$ is well-bracketed.
Since $x_A \parallel x_C = \partial_{\tau \odot \sigma}(x^\tau \odot x^\sigma)$ is complete, in particular the initial question has an answer – but as $u$ is well-bracketed, all questions in $u$ are answered. Writing $\partial_\sigma(x^\sigma) = x_A \parallel x_B$ and $\partial_\tau(x^\tau) = x_B \parallel x_C$, $x_B$ is complete as well. But then, $[x_B] \cong = x_B \in \mathcal{F}B$, so $x^\sigma$ witnesses $(x_A, x_B) \in \int \sigma$ and $x^\tau$ witnesses $(x_B, x_C) \in \int \tau$; so $(x_A, x_C) \in (\int \tau) \odot (\int \sigma)$.

Assume we have symmetry classes of complete configurations $x_A, x_B$ and $x_C$ s.t.

$$ (x_A, x_B) \in \int \sigma \qquad (x_B, x_C) \in \int \tau, $$

so there are $x^\sigma \in \mathscr{C}(\sigma)$ and $x^\tau \in \mathscr{C}(\tau)$ with $\partial_\sigma(x^\sigma) = x_A^\sigma \parallel x_B^\sigma$, $\partial_\tau(x^\tau) = x_B^\tau \parallel x_C^\tau$, with $x_A^\sigma \in x_A$, $x_B^\sigma$, $x_B^\tau \in x_B$, and $x_C^\tau \in x_C$. In particular, there is $\theta : x_B^\sigma \cong_B x_B^\tau$. Now,

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

is secured by Lemma 7.6. They only match up to symmetry, but by Proposition 4.15, there are $y^\sigma \cong_\sigma x^\sigma$ and $y^\tau \cong_\tau x^\tau$ such that $\partial_\sigma(y^\sigma) = y_A^\sigma \parallel y_B^\sigma$, $\partial_\tau(y^\tau) = y_B^\tau \parallel y_C^\tau$ with $y_B^\sigma = y_B^\tau$ – so $y^\tau \odot y^\sigma \in \mathscr{C}(\tau \odot \sigma)$. But since $y^\sigma \cong_\sigma x^\sigma$ and $y^\tau \cong_\tau x^\tau$, we also know that $y_A^\sigma \in x_A$ and $y_C^\tau \in x_C$ still, so $y^\tau \odot y^\sigma$ witnesses $(x_A, x_C) \in (\int \tau \odot \sigma)$ as required. $\square$

So positional equivalence of well-bracketed innocent causal strategies is preserved under composition. The other constructions pose no challenge. Altogether, we get:

**Corollary 7.9.** There is a Seely category $\rightarrow\mathbf{-Strat}^{\mathbf{wb,vis}} / \equiv$ of $\mathbf{--arenas}$ and positional equivalence classes of visible well-bracketed strategies. Finally, the canonical functor

$$ \rightarrow\mathbf{-Strat}^{\mathbf{wb,vis}} \rightarrow \rightarrow\mathbf{-Strat}^{\mathbf{wb,vis}} / \equiv $$

preserves the interpretation of PCF$_\parallel$.

### 7.1.6. On the relational model.
As claimed, this does indeed yield a functor to Rel:

**Proposition 7.10.** The positional collapse defines a functor $f(-) : \rightarrow\mathbf{-Strat}^{\mathbf{wb,vis}} \rightarrow \mathbf{Rel}$.

*Proof.* Composition is Proposition 7.8, while for identity it is a direct verification. $\square$

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

Unfortunately, this functor is not compatible with the Seely category structure. For negative arenas $A, B$ we do have $f(A \otimes B) \cong (fA) \times (fB)$; but for instance $f(A \& B) \not\cong (fA) + (fB)$ because $f(A \& B)$ includes the empty position, which we do not have enough information to send to the left or to the right. Likewise, $f(!A) \not\cong \mathcal{M}_f(fA)$. Considering only non-empty configurations does not solve the issue, as we lose $f(A \otimes B) \cong (fA) \times (fB)$.

This mismatch can be mitigated by focusing on the cartesian closed Kleisli categories. Say that an $\mathbf{--arena}$ $A$ is **strict** if all its minimal (necessarily negative) events are in pairwise conflict – all types and contexts of PCF are interpreted as strict $\mathbf{--arenas}$. If $A$ is an arena, we write $fA$ for the set of non-empty complete positions of $A$. Then:

**Lemma 7.11.** For $A, B, C, D$ $\mathbf{--arenas}$ with $C$ strict there are bijections:

$$ \begin{align*} f(A \otimes B) &\cong (fA) \otimes (fB) & f(A \& B) &\cong fA + fB \\ f(A \dashv C) &\cong (fA) \times (fC) & f(!C) &\cong \mathcal{M}_f(fC). \end{align*} $$

For $B, C$ strict it follows that $f(!B \dashv C) \cong \mathcal{M}_f(fB) \times (fC)$, matching relational semantics. For any PCF type $A$ we obtain $f[[A]] \cong [[A]]_{\mathbf{Rel}}$ – such a bijection is easily established for ground types – so for the interpretation of PCF types, points of the web in the relational model exactly correspond to non-empty complete symmetry classes in the
<figure><img src="image_81.png" /><figcaption>Figure 58: Non-locality of argument sub-strategies</figcaption></figure>

game semantics. This can be extended to an interpretation-preserving functor from games to relations, but we leave the details to a forthcoming paper on the quantitative collapse.

**7.2. Well-Bracketed Pruning.** We need a sufficiently constrained description of the causal shape of strategies so that we might replicate it syntactically. While innocence is a causal notion, well-bracketing is not, and it leaves the causal shape too liberal. We shall now see how via a well-bracketed pruning a more causal form of well-bracketing can be enforced.

**7.2.1. Causal well-bracketing.** Recall the idea of Theorem 3.9: each Player question $\mathbf{q}^+$ corresponds to a call to a variable $x$. Opponent questions pointing to $\mathbf{q}^+$ correspond to $x$ calling an argument; and Opponent answers to $\mathbf{q}^+$ correspond to $x$ evaluating to a return value. The crux of the definability argument is that these subsequent possibilities of Opponent moves pointing to $\mathbf{q}^+$ *split* (the causal representation of) the innocent strategy under scrutiny into sub-strategies independent from each other – as they must be, if they are to correspond to distinct branches of the desired syntax tree.

Parallel innocent strategies enjoy the same “splitting” property, to an extent:

**Lemma 7.12.** Consider A an arena, $\sigma: A$ an innocent causal strategy, and $q^+ \in |\sigma|$.

If $q^+ \to_{\sigma} m_1^-, q^+ \to_{\sigma} m_2^-$ distinct, $\{m \in |\sigma| \mid m \geq_{\sigma} m_1\}$, $\{m \in |\sigma| \mid m \geq_{\sigma} m_2\}$ disjoint.

*Proof.* Obvious by pre-innocence.

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

Unfortunately, this is too weak. Indeed $q^+$ in the statement above should correspond to a syntactic variable occurrence $x$, so that the overall term has form $C[x M_1 \dots M_n]$ where $x$ has arity $n$, with the $M_i$ written in $\text{PCF}_\parallel$. As standalone pieces of syntax in a language without interference they are indeed independent from each other (as guaranteed semantically by Lemma 7.12), but are also independent from the context $C$ – which Lemma 7.12 does not capture. In fact, the current conditions on strategies do not ensure this.

In Figure 58, we show a counter-example: this satisfies all the conditions for an augmentation of a well-bracketed parallel innocent strategy. Here, $\mathbf{q}_1^+$ should correspond to a variable call, and $\mathbf{q}_2^-$ should initiate the exploration of its argument, and independent sub-term. But the subsequent Player move $\mathbf{q}_2^+$, the “head variable occurrence” of the argument sub-term, also depends on a parallel thread. This behaviour is not realizable in $\text{PCF}_\parallel$ and should be banned before any definability attempt.

We now define which causal behaviour is deemed acceptable for $\text{PCF}_\parallel$.
**Definition 7.13.** Consider A an arena, and $\boldsymbol{\sigma}: A$ parallel innocent.

We say that $\boldsymbol{\sigma}$ is **causally well-bracketed** iff it satisfies the two conditions below:

*wb-threads*: for every $\rho \in \text{gcc}(\boldsymbol{\sigma})$, $\rho$ is well-bracketed in the sense of Definition 3.2,

*globular*: for any diagram in $\boldsymbol{\sigma}$ with $X = \{m_1, \dots, m_n\}$ and $Y = \{n_1, \dots, n_p\}$ disjoint:

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

then every question in $X$ (resp. $Y$) is answered in $X$ (resp. $Y$).

The Question/Answer labeling is implicitly imported from $|A|$ to $|\boldsymbol{\sigma}|$ via $\partial_{\boldsymbol{\sigma}}$ – likewise, for $m^Q, n^A \in |\boldsymbol{\sigma}|$, we say that $n$ **answers** $m$ if $\partial_{\boldsymbol{\sigma}}(m) \to_A \partial_{\boldsymbol{\sigma}}(n)$, i.e. $\partial_{\boldsymbol{\sigma}}(n)$ **answers** $\partial_{\boldsymbol{\sigma}}(m)$.

We call such a diagram a *globule*. This bans directly behaviours as in Figure 58. Only Player can merge parallel threads, and only if he is responsible for the fork (by parallel innocence). So, polarities in the definition of globules are not restrictive. One can further observe that globules always have Question/Answer assignments as in

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

Indeed, if $m_1$ was an answer, it would be maximal in $\boldsymbol{\sigma}$ (by Lemma A.7, as answers are maximal in $A$) and the merge would be impossible. So $m_1$ is a question, and by *globular* it has an answer in $\{m_1, \dots, m_{2n}\}$. By courtesy this answer depends immediately on $m_1$ in $\boldsymbol{\sigma}$ and so must be $m_2$. Repeating this we get the description above. Hence in *causally well-bracketed* strategies, parallel threads that might merge follow a strict call/return discipline.

A variant of the proof of Proposition 5.14, relying on Lemma 5.13, shows that causal well-bracketing composes. This was done in [CCW15] (see also [Cas17]), but it is not our route here: we must prove full abstraction with respect to the *same* well-bracketing condition used before. We shall see that the situation is similar as in Section 6.2.2: in *complete* configurations, which suffice for tests, the weaker well-bracketing implies the stronger.

### 7.2.2. Strengthening well-bracketing.
We will show that if $\boldsymbol{\sigma}: A$ is innocent and well-bracketed (as in Definition 4.31) and $x^{\boldsymbol{\sigma}} \in \mathscr{C}(\boldsymbol{\sigma})$ is complete (i.e. all its questions have an answer within $x^{\boldsymbol{\sigma}}$), then the corresponding augmentation is also *causally* well-bracketed – so restricting an innocent well-bracketed $\boldsymbol{\sigma}: A$ to its completable part yields a positionally equivalent, *causally* well-bracketed strategy; a procedure we call “well-bracketed pruning”.

On arenas arising from types, gccs of innocent strategies are *already* well-bracketed – this holds even without well-bracketing. The proof is morally as for Proposition 3.15.

**Lemma 7.14.** Consider A a type, $\boldsymbol{\sigma}: [A]$ an innocent causal strategy, and $\rho \in \text{gcc}(\boldsymbol{\sigma})$. Then, $\rho$ is well-bracketed in the sense of Definition 3.2.

*Proof.* Consider $\rho = \rho_1 \to \dots \to \rho_n \in \text{gcc}(\boldsymbol{\sigma})$ and assume, seeking a contradiction, that $\rho_n$ is an answer not pointing to the pending question. It follows that $\rho$ has the form:

<figure><img src="image_85.png" /></figure>
where $\rho_{j+1}^{-,Q}$ was pending. As $[[A]]$ is the interpretation of a type, $\rho_{j+1}^{-,Q}$ is sibling to countably many symmetric copies, i.e. we may write it as $b_k$ with some copy index $k \in \mathbb{N}$, and consider a copy $b_{k+1} \in |\sigma|$ with both $b_k$ and $b_{k+1}$ pointing to $\rho_j$. Write also $m = \rho_n$.

Consider $x^\sigma \in \mathscr{C}(\sigma)$ with $\rho$ in $x^\sigma$, w.l.o.g. we can assume that (the augmentation) $x^\sigma$ has top element $m$. Consider any $t \in \mathcal{C}-\text{Plays}(x^\sigma)$ s.t. $|t| = x^\sigma$. Then $t$ may be written as $t_1 \cdot b_k \cdot t_2 \cdot m$ where without loss of generality, we may assume that all events after $b_k$ depend on it. Because $\rho$ is in $x^\sigma$, $m$ points in $t_1$. Now, by uniformity of $\sigma$, there is also some

$$t' = t_1 \cdot b_{k+1} \cdot t'_2 \cdot m' \in \mathcal{C}-\text{Plays}(\sigma),$$

such that $t \cong_{\sigma} t'$, where (therefore) $m'$ points to the same move as $m$ in $t_1$. There is some $y^\sigma \in \mathscr{C}(\sigma)$ such that $t' \in \mathcal{C}-\text{Plays}(y^\sigma)$, w.l.o.g. assume $|t'| = y^\sigma$. By innocence, any causal branching in $x^\sigma$ and $y^\sigma$ is due to Player. Next, we observe that $x^\sigma$ and $y^\tau$ are negatively compatible. Indeed if $n_1^- \in |x^\sigma|$, $n_2^- \in |y^\sigma|$ are in minimal conflict in $\sigma$, then by Lemma A.8, $\partial_\sigma(n_1)$ and $\partial_\sigma(n_2)$ are in minimal conflict in $[[A]]$. But by property of arenas originating from types, this implies that $n_1$ and $n_2$ have the same justifier $n$. As moves in $t_2 \cdot m$ depend on $b_k$ and moves in $t'_2 \cdot m'$ depend on $b_{k+1}$, by pre-innocence (Lemma 7.12) these must be disjoint, so $n$ appears in $t_1$. But again by pre-innocence, since $x^\sigma$ has top element $m$ and $y^\sigma$ has top element $m'$, only one Opponent move can point to $n$ in $x^\sigma$; and likewise for $y^\sigma$. As $t \cong_{\sigma} t'$ preserves pointers, that means that $n_1$ and $n_2$ must arrive at the same (chronological) index in $t, t'$, and so their display in $[[A]]$ are related by a symmetry in $[[A]]$. But in arenas arising from PCF types, no conflicting events can be related by a symmetry, contradiction. $\square$

So condition *wb-threads* of Definition 7.13 is automatic, even without assuming well-bracketing. However, condition *globular* is not automatic as illustrated by Figure 58.

We shall now prove *globular* on *complete* augmentations of well-bracketed innocent strategies. Intuitively, the reason is simple. Consider a globule

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

in $x^\sigma$. As $x^\sigma$ is complete, every question is eventually answered. But after the merge, it is too late for questions in the $a_i$s and $b_j$s: if some $b$ such that $a \ge b$ answers $a_i$ then by visibility $a_i$ must appear in all its gccs; but a gcc to $b$ may go through the $b_j$s and avoids $a_i$ entirely. Of course, turning this idea into a proof takes some work. First we prove:

**Lemma 7.15.** Consider a $--$arena A, $\sigma$: A visible well-bracketed, and $x^\sigma \in \mathscr{C}(\sigma)$ complete.
For all $q_1^{-,Q} \in x^\sigma$, for all $q_2^{+,Q} \in x^\sigma$ such that $\partial_\sigma(q_1) \to_A \partial_\sigma(q_2)$, we have:

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

with $a_1$ and $a_2$ the (unique) answers to $q_1$ and $q_2$.

*Proof.* First, $a_1$ and $a_2$ exist as $x^\sigma$ is complete, and are unique by *answer-linear*.

Seeking a contradiction, assume $a_2 \nleq_{\sigma} a_1$, i.e. $a_2 \notin [a_1]_{\sigma}$. As $a_2 \notin [q_2]_{\sigma}$, writing $y = [a_1]_{\sigma} \lor [q_2]_{\sigma}$, $y \in \mathscr{C}(\sigma)$ with $a_1, q_2 \in y$ and $a_2 \notin y$. By Lemma 7.7, there is $t \in \mathcal{C}-\text{Plays}(y)$
well-bracketed s.t. $|t| = y$. So by wait of Definition 3.20, $q_2$ is answered in $|t| = y$. But since $a_2 \notin y$, this means $q_2$ is answered twice in $x^\sigma$, which contradicts answer-linear. $\square$

Using that, we may now formalize and complete the intuitive argument above.

**Lemma 7.16.** For $\sigma : [[A]]$ well-bracketed innocent and $x^\sigma \in \mathscr{C}(\sigma)$ complete, $x^\sigma$ is globular.

*Proof.* Consider a globule in $x^\sigma$, i.e. a diagram

$$ \begin{tikzpicture}[baseline=(current bounding box.center)]
\node (m_0^-) at (0,0) {$m_0^-$};
\node (m_1^-) at (1,0) {$m_1^+$};
\node (m_n^-) at (2,0) {$m_n^-$};
\node (m_1^+) at (3,0) {$m_1^+$};
\node (m_0^+) at (4,0) {$m_0^+$};
\node (n_1^+) at (5,0) {$n_1^+$};
\node (n_p^+) at (6,0) {$n_p^+$};
\draw[->] (m_0^-) -- (m_1^-);
\draw[->] (m_0^-) -- (m_n^-);
\draw[->] (m_1^-) -- (m_0^-);
\draw[->] (m_1^-) -- (n_1^+);
\draw[->] (m_1^-) -- (n_p^-);
\draw[->] (n_1^+) -- (n_p^-);
\draw[->] (n_p^-) -- (n_p^-);
\draw[->] (n_p^-) -- (n_p^-);
\node at (0.5,-0.5) {$\dots \to \dots \to q^{-}, \mathscr{Q} \to \dots \to m_0^- \to m_1^+ \to \dots \to m_n^- \to m^{+,A}$};
\node at (2.5,-0.5) {$\dots \to \dots \to q^{-}, \mathscr{Q} \to \dots \to m_0^- \to m_1^+ \to \dots \to m_n^- \to m^{+,A} \to a^{-}, A \to \dots \to b^{+,A}$};
\end{tikzpicture} $$

with $X = \{m_1, \dots, m_n\}$ and $Y = \{n_1, \dots, n_p\}$ disjoint. Seeking a contradiction, consider $m_i^Q \in X$ unanswered in $X$. First, we consider $q^- = \text{just}(m^+)$. Since $\sigma$ is visible, $q^-$ appears in any gcc of $m$, so $q^- \le \sigma m_0^-$. But hence $m$ is a question, or a gcc like

$$ \dots \to \dots \to q^{-}, \mathscr{Q} \to \dots \to m_0^- \to m_1^+ \to \dots \to m_n^- \to m^{+,A} $$

fails well-bracketing as $m_i$ is unanswered, forbidden by Lemma 7.14. So $m^+$ has an answer $a^-$ in $x^\sigma$. But $q^-$ also has an answer $b^+$ in $x^\sigma$, and by Lemma 7.15, $a^- \le \sigma b^+$. So altogether

$$ \dots \to \dots \to q^{-}, \mathscr{Q} \to \dots \to m_0^- \to m_1^+ \to \dots \to m_n^- \to m^{+, \mathscr{Q}} \to a^{-}, A \to \dots \to b^{+, A} $$

well-bracketed by Lemma 7.14. So in $m^+ \to a^- \to \dots \to b^+$, some move must answer $m_i$; and in particular point to $m_i$. But $m_i$ does not appear in the gcc $\dots \to m_0 \to n_1 \to \dots \to n_p \to m \to a \to \dots \to b$, contradicting visibility. Therefore, $X$ is complete. $\square$

**7.2.3.** *Well-bracketed pruning.* For $x \in \mathscr{C}(\sigma)$, write $x^+ \in \mathscr{C}(\sigma)$ for the greatest +-covered configuration s.t. $x^+ \subseteq x$, obtained by removing trailing Opponent moves.

**Proposition 7.17.** For A a $--$arena and $\sigma : A$ a well-bracketed innocent strategy, set

$$ |\mathrm{comp}(\sigma)| = \cup \{x \in \mathscr{C}(\sigma) \mid x^+ \subseteq y \in \mathscr{C}(\sigma) \text{ complete}\}, $$

with all other components directly inherited from $\sigma$.

Then $\mathrm{comp}(\sigma) = \sigma : A$ is innocent, well bracketed, causally well-bracketed$^{26}$.

*Proof.* Most conditions are immediate consequences of those from $\sigma$. The only non-trivial property is that $\mathscr{S}(\sigma)$ restricted to $|\mathrm{comp}(\sigma)|$ is still an isomorphism family.

First, we prove that for any $\theta : x_1 \cong_\sigma x_2$, $x_1 \in \mathscr{C}(\mathrm{comp}(\sigma))$ iff $x_2 \in \mathscr{C}(\mathrm{comp}(\sigma))$. Indeed, assume $x_1^+ \subseteq y_1 \in \mathscr{C}(\sigma)$ complete. Then, since $\theta$ is an order-iso that preserves polarities, by restriction it restricts to $\theta' : x_1^+ \cong_\sigma x_2^+$. Now, by extension, $\theta'$ extends to $\theta'' : y_1 \cong_\sigma y_2$ for some $x_2^+ \subseteq y_2$. But since $\theta''$ preserves the Question/Answer labeling, $y_2 \in \mathscr{C}(\sigma)$ is complete; hence $x_2 \in \mathscr{C}(\mathrm{comp}(\sigma))$ as required. From that, it is straightforward that $\mathscr{S}(\mathrm{comp}(\sigma))$ comprising symmetries between configurations of $\mathrm{comp}(\sigma)$ is an isomorphism family.

For causal well-bracketing, $\mathrm{comp}(\sigma)$ satisfies *wb-threads* by Lemma 7.14. For *globular*, taking a diagram as in Definition 7.13, $m^+$ appears in a +-covered configuration of $\mathrm{comp}(\sigma)$; hence in a complete configuration of $\sigma$. Thus, the condition follows by Lemma 7.16.

<footnote>$^{26}$A strategy may well be causally well-bracketed without being well-bracketed: an example of that is a strategy $\sigma : \mathcal{U} \to \mathcal{U}$ that simultaneously calls its argument (but does nothing with the result) and returns.</footnote>
Finally, we must show $\sigma \equiv \text{comp}(\sigma)$ – in fact, we show both have the same complete configurations. For that, any complete $x \in \mathscr{C}(\sigma)$ must also be +-covered: take $x \in \mathscr{C}(\sigma)$ complete. If $x$ has a maximal negative event $m^-$, since $x$ is complete, $m$ is an answer. But just(just($m$)) is a Question answered by some $a^{+,A}$ in $x$ – but then $m \leq_{\sigma} a$ by Lemma 7.15, contradicting maximality of $m$. Using this we conclude: clearly, any complete configuration of $\text{comp}(\sigma)$ is a complete configuration of $\sigma$. Reciprocally, a complete $x \in \mathscr{C}(\sigma)$ is +-covered, and thus also a (complete) configuration of $\text{comp}(\sigma)$. So, $\int_{\sigma} = \text{comp}(\sigma)$. $\square$

By construction, we also have that $\text{comp}(\sigma)$ is complete, in the following sense:

**Definition 7.18.** Consider A an arena, and $\sigma : A$ a causal strategy.
We say that $\sigma$ is complete, if for any $x \in \mathscr{C}^+(\sigma)$ there is $x \subseteq y \in \mathscr{C}(\sigma)$ complete.

**7.3. Meager Form.** As for sequential strategies, definability applies for *finite* strategies, defined through a notion of *meager form*. But to define meager forms we will first need to restrict to *concrete arenas* in the sense of Section 2.20, which we must first update.

**7.3.1. Updating concrete arenas.** We enrich and update Definition 2.20.

**Definition 7.19.** A concrete arena is $(A, A^0, \text{lbl}, \text{ind})$ with $A$ an arena, $A^0$ meager arena,

$$ \text{lbl} : |A| \to |A^0|, \quad \text{ind} : |A| \to \mathbb{N} $$

two functions, satisfying, additionally to the conditions of Definition 2.20, the conditions:

*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$.

*Q-wide:* for any $q_1^Q \in |A|$ non-minimal, for any $n \in \mathbb{N}$, there is $q_2^Q \in |A|$ such that $\text{lbl}(q_1) = \text{lbl}(q_2)$, $\text{pred}(q_1) = \text{pred}(q_2)$ and $\text{ind}(q_2) = n$.

*A-narrow:* for any $a^- \in |A|$ minimal or $a^A \in |A|$, $\text{ind}(a) = 0$,

*A-conflicting:* if $a_1, a_2 \in |A|$ are distinct, they are in minimal conflict iff they are both minimal with the same polarity and copy index, or they are both answers to the same question.

*+ - transparent:* for any $\theta : x \cong_A y$, then $\theta \in \mathscr{S}_+(A)$ iff for all $a^- \in x$, $\text{ind}(\theta(a)) = \text{ind}(a)$.

*-- transparent:* for any $\theta : x \cong_A y$, then $\theta \in \mathscr{S}_-(A)$ iff for all $a^+ \in x$, $\text{ind}(\theta(a)) = \text{ind}(a)$.

We call $\text{ind}(a)$ the **copy index** of $a$, and $\text{pred}(-)$ is the (unique) **immediate predecessor**.

In arenas for ground types, all moves have copy index 0. For $A \& B$, the copy index function is simply inherited. For $A \to B$, the copy index of an initial $(1, (i, a))$ in $A$ is simply $i$ – in all other cases it is inherited. It is direct that all requirements are met.

**7.3.2. Meager innocent strategies.** We now introduce the causal counterpart of the meager alternating innocent strategies of Section 3.3.1. Those are parallel innocent strategies in the sense of Section 5, but on a restricted arena authorizing only Player replications:

**Proposition 7.20.** Consider A a concrete arena. Then, setting events:

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

with other components inherited from A, yields an arena $A^+$.
**Proof.** All verifications are straightforward. For symmetry, if $\theta: x \cong_A y$ with $x, y \in \mathscr{C}(A^+)$, then by Definition 7.19, $\theta \in \mathscr{S}_+(A)$. But likewise by Definition 7.19, for $\theta: x \cong_A^+ y$, $x \in \mathscr{C}(A^+)$ iff $y \in \mathscr{C}(A^+)$. Together those imply that the restriction of $\mathscr{I}(A)$ to $A^+$ satisfies extension – other axioms are easy. Finally, from Definition 7.19 again the polarized isomorphism families are $\mathscr{S}_+(A^+) = \mathscr{I}(A^+)$, and $\mathscr{S}_-(A^+)$ restricted to identities. $\square$

So $A^+$ is A where Opponent has only access to copy index 0. This lets us define:

**Definition 7.21.** Consider A a concrete arena.

A meager causal (pre)strategy on A is a causal (pre)strategy $\sigma: A^+$.

As intended, this eliminates the infinity originating from Opponent repetitions. As a side-effect, the isomorphism family of $\sigma$ becomes trivial: as the only non-trivial symmetries of $A^+$ are positive, it follows by condition *thin* (see Lemma 3.28 of [CCW19]) that symmetries of $\sigma$ are reduced to identities – so a meager strategy is really a plain event structure.

Any causal strategy $\sigma: A$ yields a meager strategy $\mathrm{mf}(\sigma): A^+$, simply by restriction:

**Proposition 7.22.** Consider A a concrete arena, and $\sigma: A$ any causal strategy. Setting

$$|\mathrm{mf}(\sigma)| = \{m' \in |\sigma| \mid \forall m^- \leq_{\sigma} m', \mathrm{ind}(\partial_{\sigma}(m)) = 0\}$$

with other components inherited from $\sigma$, yields a meager causal strategy $\mathrm{mf}(\sigma): A^+$.

**Proof.** All conditions are straightforward verifications. $\square$

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

We call $\mathrm{mf}(\sigma): A^+$ the meager form of $\sigma: A$. As $A^+$ is closed under positive symmetry, it is immediate that $\mathrm{mf}(-)$ preserves positive isomorphism: if $\sigma \approx \sigma'$, then $\mathrm{mf}(\sigma) \approx \mathrm{mf}(\sigma')$. As illustration, we show in Figure 59 the meager form of $\mathrm{plet}_{U,U}$ as defined in Section 4.4.2. Unlike Figure 38, this is now not merely a symbolic representation, but an exhaustive display of the full event structure of the meager form – we shall see that as for alternating innocent strategies, meager forms of parallel innocent causally well-bracketed strategies provide a way to give complete formal descriptions of the full infinite strategy.

Without parallel innocence, taking the meager form is a lossy operation. In Figure 60 we show a typical augmentation of the causal strategy obtained as the interpretation of

$$\vdash \mathbf{newref} x:=0 \mathbf{in} \lambda f^{U \to U}. f (\mathbf{let} \ v=!x \ \mathbf{in} \ x:=1; \mathbf{assume} (v=\mathbb{N} \ 1)) : (U \to U) \to U,$$

displaying behaviour that is lost when taking the meager form: any interference between different copies of the same branch – a behaviour typically banned by parallel innocence.

This lets us define finiteness for parallel innocent strategies as in Section 3.3.1:

**Definition 7.23.** Consider A a concrete arena, and $\sigma: A$ a parallel innocent strategy.

We say that $\sigma$ is finite if the set $|\mathrm{mf}(\sigma)|_+ = \{m \in |\mathrm{mf}(\sigma)| \mid \mathrm{pol}(m) = +\}$ is finite.

If $\sigma$ is finite, its size is the cardinal of $|\mathrm{mf}(\sigma)|_+$.

7.3.3. *Finite tests suffice.* The key mechanism behind the reduction to finite tests is to be able to restrict a parallel innocent strategy following a finite subset of its meager form.

Say $x \in \mathscr{C}(\sigma)$ is normal iff for all $m^+ \to_{\sigma} m_1^-$ and $m^+ \to_{\sigma} m_2^-$ in $x$, $m_1 = m_2$. We show that every normal $x \in \mathscr{C}(\sigma)$ has a unique representative in $\mathrm{mf}(\sigma)$.

**Lemma 7.24.** Consider A a concrete arena, $\sigma: A$ a causal strategy, and $x \in \mathscr{C}(\sigma)$ normal.

There is a unique $\mathrm{mf}(x) \in \mathscr{C}(\mathrm{mf}(\sigma))$ s.t. $x \cong_{\sigma} \mathrm{mf}(x)$, and $\theta_x: x \cong_{\sigma} \mathrm{mf}(x)$ is unique.
<figure><img src="image_89.png" /><figcaption>Figure 59: The meager form of $\mathrm{plet}_{U,U}$</figcaption></figure>

<caption>Figure 60: Lossy meager form</caption>

*Proof. Existence.* By induction on $x$. Consider $x \stackrel{m}{\subset} y$. If $m$ is positive, by extension there is an extension of $\theta_x$ with $(m, n)$. As $n$ is positive its negative dependencies are in $\mathfrak{mf}(x)$ so their display have copy index 0, so $n \in |\mathfrak{mf}(\boldsymbol{\sigma})|$. If $m$ is negative, by extension on $A$, there is
$$ \partial_{\boldsymbol{\sigma}} \theta_x \cup \{(\partial_{\boldsymbol{\sigma}}(m), a)\} : \partial_{\boldsymbol{\sigma}}(x) \cup \{\partial_{\boldsymbol{\sigma}}(m)\} \cong_A \partial_{\boldsymbol{\sigma}}(\mathfrak{mf}(x)) \cup \{a\}, $$

with $a$ characterised by ind($a$), label($a$), and pred($a$). If $m$ is an answer, so is $a$ and by A-narrow, ind($a$) = 0. If $m$ is a Question, we may not have ind($a$) = 0. But then by Q-wide, there is $a' \in |A|$ s.t. pred($a'$) = pred($a$), label($a'$) = label($a$) and ind($a'$) = 0; but we must prove that $a'$ is not already in $\partial_{\boldsymbol{\sigma}}(\mathfrak{mf}(x))$. If it is, there is $\theta_x(m') \in \mathfrak{mf}(x)$ s.t. $\partial_{\boldsymbol{\sigma}}(\theta_x(m')) = a'$. By courtesy $m'$ and $m$ are negative in $y$ with the same predecessor, contradicting normality of $y$. So $y$ extends with $a'$ with copy index 0. By transparent, $\partial_{\boldsymbol{\sigma}}(\theta_x) \cup \{(\partial_{\boldsymbol{\sigma}}(m), a')\} \in \mathcal{S}(A)$. So, by ~-receptivity of $\boldsymbol{\sigma}$, $\theta_x$ extends with $(m, \mathfrak{mf}(m))$ in $\boldsymbol{\sigma}$ s.t. $\mathfrak{mf}(m) \in |\mathfrak{mf}(\boldsymbol{\sigma})|$ as required.

*Uniqueness.* For $y_1, y_2 \in \mathcal{C}(\mathfrak{mf}(\boldsymbol{\sigma}))$ s.t. $\theta_1 : x \cong_{\boldsymbol{\sigma}} y_1$ and $\theta_2 : x \cong_{\boldsymbol{\sigma}} y_2$, then $\theta = \theta_2 \circ \theta_1^{-1} : y_1 \cong_{\boldsymbol{\sigma}} y_2$. But copy indices of Opponent events in $\partial_{\boldsymbol{\sigma}}y_1$ and $\partial_{\boldsymbol{\sigma}}y_2$ are 0, so by +-transparent, $\partial_{\boldsymbol{\sigma}}\theta \in \mathcal{S}_+(A)$. By Lemma 3.28 of [CCW19], $y_1 = y_2$ and $\theta = \mathrm{id}$, so $\theta_1 = \theta_2$. $\square$

This does not depend on parallel innocence – which comes in when transporting events:

**Lemma 7.25.** Consider A a concrete arena, $\boldsymbol{\sigma}: A$ parallel innocent, and $m \in |\boldsymbol{\sigma}|$.

Then, there exists a unique $\mathfrak{mf}(m) \in |\mathfrak{mf}(\boldsymbol{\sigma})|$ such that $[m]_{\boldsymbol{\sigma}} \cong_{\boldsymbol{\sigma}} [\mathfrak{mf}(m)]_{\boldsymbol{\sigma}}$.

*Proof. Pre-innocence* exactly states that the prime configuration $[m]_{\boldsymbol{\sigma}}$ is normal. Hence, by Lemma 7.24, there is a unique $y \in \mathcal{C}(\mathfrak{mf}(\boldsymbol{\sigma}))$ such that $[m]_{\boldsymbol{\sigma}} \cong_{\boldsymbol{\sigma}} y$. But then, as symmetries are order-isomorphisms, $y$ is a prime configuration $y = [\mathfrak{mf}(m)]_{\boldsymbol{\sigma}}$ as required. $\square$

Moreover, this assignment is preserved under symmetry:

**Lemma 7.26.** Consider A a concrete arena, $\boldsymbol{\sigma}: A$ parallel innocent.

For any $\theta : x \cong_{\boldsymbol{\sigma}} y$ and $m \in x$, $\mathfrak{mf}(m) = \mathfrak{mf}(\theta(m))$.

*Proof.* As $\theta$ is an order-iso, it restricts to $[m]_{\boldsymbol{\sigma}} \cong_{\boldsymbol{\sigma}} [\theta(m)]_{\boldsymbol{\sigma}}$. Composition with $[m]_{\boldsymbol{\sigma}} \cong [\mathfrak{mf}(m)]_{\boldsymbol{\sigma}}$ and $[\theta(m)]_{\boldsymbol{\sigma}} \cong [\mathfrak{mf}(\theta(m))]_{\boldsymbol{\sigma}}$ yields $\varphi : [\mathfrak{mf}(m)]_{\boldsymbol{\sigma}} \cong_{\boldsymbol{\sigma}} [\mathfrak{mf}(\theta(m))]_{\boldsymbol{\sigma}}$, and $\partial_{\boldsymbol{\sigma}}(\varphi) \in \mathcal{S}_+(A)$ by +-transparent. Hence, by Lemma 3.28 of [CCW19], $\varphi$ is an identity. $\square$

From that, we may deduce the following:
**Corollary 7.27.** For A concrete, $\sigma$: A parallel innocent and $\tau \leqslant$ mf($\sigma$) finite,

$$|\sigma \uparrow \tau| = \{m \in |\sigma| \mid \text{mf}(m) \in |\tau|\}$$

with all other components inherited from $\sigma$ yields a finite innocent $\sigma \uparrow \tau$: A s.t. $\sigma \uparrow \tau \leqslant \sigma$. Moreover, if $\sigma$ is well-bracketed (resp. causally well-bracketed), so is $\sigma \uparrow \tau$.

*Proof.* The only non-trivial condition, extension for $\mathcal{I}(\sigma \uparrow \tau)$, follows from Lemma 7.26. $\square$

From that, we may finally prove that finite tests suffice.

**Corollary 7.28.** Consider A a concrete --arena, and $\sigma_1, \sigma_2$: A parallel innocent.
If there is $\alpha$: !A $\vdash$ U parallel innocent and well-bracketed, such that

$$\alpha \odot! \sigma_1 \downarrow, \quad \alpha \odot! \sigma_2 \uparrow,$$

then there is $\alpha' \leqslant \alpha$ parallel innocent, well-bracketed, and finite, s.t. $\alpha' \odot! \sigma_1$ and $\alpha' \odot! \sigma_2$.

*Proof.* Since $\alpha \odot! \sigma_1 \downarrow$, there is $x^\alpha \odot x^{\sigma_1} \in \mathcal{C}(\alpha \odot \sigma_1^\dagger)$ s.t. $\partial_\alpha x^\alpha = x_A \parallel \{\mathbf{q}^-, \mathbf{\vee}^+\}$. In particular, $x^\alpha$ is finite. So the set $X = \{\text{mf}(m) \mid m \in x^\alpha\}$ is finite, so there is $\tau \leqslant$ mf($\alpha$) a finite meager strategy s.t. $X \subseteq |\tau|$. By Corollary 7.27, $\alpha' = \alpha \uparrow \tau$: A is a finite parallel innocent strategy s.t. $\alpha' \leqslant \alpha$. Moreover, by construction, $x^\alpha \in \mathcal{C}(\alpha')$ with the same causal ordering as in $\alpha$, so that $\alpha' \odot! \sigma_1 \downarrow$ still. Finally, $\alpha' \odot! \sigma_2 \downarrow$ would contradict $\alpha \odot! \sigma_2 \uparrow$ since $\alpha' \leqslant \alpha$. As $\mathcal{I}\text{-Plays}(\alpha') \subseteq \mathcal{I}\text{-Plays}(\alpha)$, $\alpha'$ is still well-bracketed. $\square$

In fact, meager forms of parallel innocent strategies can be expanded back to the original strategy. This is not used in the technical development, but we include it as Appendix D.5.

**7.4. Factorization.** We focus on finite tests. Unlike in the sequential argument of Section 3.3.1, parallel innocent strategies have no “first Player move” to reproduce first syntactically. Hence we organize our definability process differently. Its core is a *factorization result* (Corollary 7.43): namely, that every finite test $\alpha$: !($\&A_i$) $\vdash$ X may be obtained as

$$\alpha \equiv \mathfrak{f}(\alpha) \odot! \langle x_i \alpha_{k,1} \dots \alpha_{k,p_i} \mid i \in I, k \in K_i \rangle, \quad (7.1)$$

with $\mathfrak{f}(\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 7.5.1.

We first extract the components mentioned in (7.1): the *first-order substrategy* $\mathfrak{f}(\alpha)$, and the *argument substrategies* $\alpha_{k,j}$. We use as illustration the strategy with typical maximal augmentations in Figure 61. 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 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 61, the primary questions are $\mathbf{q}_0^+$, $\mathbf{q}_1^+$ and $\mathbf{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 61 there are three, respectively prompted by (i.e. causally depending on) $\mathbf{q}_{0,i}^-$, $\mathbf{q}_{2,k}^-$ and $\mathbf{q}_{1,r}^-$ and colored accordingly.

The strategy of Figure 61 is exactly definable; as illustration we show the term in Figure 62, with subterms colored so as to match the four components of the strategy$^{27}$.

<footnote>$^{27}$In the end, our definability process will not quite give the term of Figure 62 for the strategy of Figure 61, but a sequential version as we do not know how to define first-order strategies in general – see Section 7.5.1.</footnote>
<figure><img src="image_90.png" /><figcaption>Figure 61: A parallel innocent causally well-bracketed strategy</figcaption></figure>

$$f : \mathbb{B} \to \mathbb{U}, g : (\mathbb{U} \to \mathbb{B}) \to \mathbb{B} \vdash \\ \text{let } \left( \begin{array}{l} x = f \tt \\ y = g (\lambda z \mathbb{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 \text{ ff; tt}) \text{ else } ff) : \mathbb{B}$$

<caption>Figure 62: Factorization and definability for Figure 61</caption>

The proof of factorization is organized as follows. In Section 7.4.1, we extract the first-order part, and in Section 7.4.2 we reorganize it so as to be able to re-compose it better. In Section 7.4.3, we extract the argument substrategies. In Section 7.4.4, we conclude.

**7.4.1. Shallow substrategy.** Consider A a type, and $\alpha: [A]$ well-bracketed, parallel innocent, causally well-bracketed, finite, and complete. We call such a strategy a **test strategy**.

Necessarily A has the form $A_1 \to \dots \to A_n \to \mathbb{X}$ where $A_i = A_{i,1} \to \dots \to A_{i,p_i} \to \mathbb{X}_i$. Recall that $\mathbb{X}, \mathbb{X}_i$ range over ground types, i.e. $\mathbb{U}, \mathbb{B}$ and $\mathbb{N}$. Up to currying, we write

$$\alpha : !((\&_1 \leq_i \leq_n A_i) \vdash \mathbb{X}),$$

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

**Proposition 7.29.** We define the **shallow substrategy** as having set of events

$$|\mathrm{sh}(\alpha)| = \{m \in |\alpha| \mid [m]_{\alpha} \text{ has at most one Opponent question}\}, \\ \text{and other components inherited from } \alpha. \text{ Then, } \mathrm{sh}(\alpha) : !((\&\mathbb{X}_i) \vdash \mathbb{X}) \text{ is a test strategy.}$$

*Proof.* Write $\mathrm{sh}(A)$ for the arena $!(\&\mathbb{X}_i) \vdash \mathbb{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 test strategy are direct by restriction from $\alpha$.

We show $\mathrm{sh}(\alpha)$ complete. Consider $x \in \mathscr{C}^+(\mathrm{sh}(\alpha))$. Since $\alpha$ is complete, there is $x \subseteq y \in \mathscr{C}(\alpha)$ complete. In particular, there is an answer $a^+$ to the initial $\mathfrak{q}_0^-$. By Lemma 7.15, all moves of $x$ are below $a^+$ for $\leq_{\sigma}$. So setting $z = [a]_{\sigma}, x \subseteq z$. By Lemma 7.14, all gccs leading to $a$ are well-bracketed, so $[a]_{\sigma}$ is complete. Finally, $[a]_{\sigma} \in \mathscr{C}(\mathrm{sh}(\alpha))$: indeed,
<figure><img src="image_91.png" /><figcaption>Figure 63: Augmentations of the flow substrategy for Figure 61</figcaption></figure>

if it has a non-initial Opponent question $\mathbf{q}^{-}$, it has an answer $\mathbf{b}^{+}$ distinct from $\mathbf{a}^{+}$. But
Player answers are maximal in gccs, contradicting that any gcc can be extended to $\mathbf{a}$. $\square$

This captures the red part of Figure 61. All events of $\mathbf{sh}(\boldsymbol{\alpha})$ are in $\mathbf{mf}(\boldsymbol{\alpha})$: the negative dependencies of $m \in |\mathbf{sh}(\boldsymbol{\alpha})|$ are either answers or the initial question, so by A-narrow their display has copy index 0. Since $\boldsymbol{\alpha}$ is finite, so is the set of positive events of $\mathbf{sh}(\boldsymbol{\alpha})$.

**7.4.2. The flow substrategy.** We must reconstruct $\boldsymbol{\alpha}$ using the categorical structure of $\dasharrow$-Strat.
But as distinct Player questions in the same $\mathbb{X}_i$ may receive distinct argument substrategies,
we need to relabel $\mathbf{sh}(\boldsymbol{\alpha})$ to send those to distinct components. First we define:

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

By construction, $\mathcal{Q} = \wp_{1 \le i \le n} \mathcal{Q}_i$. As $|\mathbf{sh}(\boldsymbol{\alpha})|$ is finite, so is $\mathcal{Q}$, which allows us to set:

**Definition 7.31.** The flow substrategy $\mathbf{flow}(\boldsymbol{\alpha}) : \otimes_{1 \le i \le n} \otimes_{q \in \mathcal{Q}_i} \mathbb{X}_i \vdash \mathbb{X}$ is $\mathbf{sh}(\boldsymbol{\alpha})$ with

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

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

It is a test strategy. We show in Figure 63 the maximal augmentations of the flow
substrategy for Figure 61, tagging each component by the corresponding primary question.

**7.4.3. 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.

Fix a primary question $q \in \mathcal{Q}_i$. It displays to an initial event in $A_i$, which is:

$!A_{i,1} \dasharrow \dots \dasharrow !A_{i,p_i} \dasharrow \mathbb{X}_i.$

Argument substrategies are accessed by Opponent questions pointing to primary ques-
tions. Up to symmetry, there are $p_i$ Opponent questions pointing to $q$, matching the $p_i$
arguments of $A_i$. From now on, if $q \in \mathcal{Q}_i$ is a primary question and $q \dasharrow \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 \mathcal{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:

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

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

**Definition 7.32.** Let $q \in \mathcal{Q}_i$ a primary question, $1 \le j \le p_i$, and $m \in |\alpha|$. We write:

$m \in \mathfrak{sh}(\alpha) \Leftrightarrow [m]_{\alpha}$ comprises exactly one Opponent question,

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

Any $m \in |\alpha|$ receives a tag as either in $\mathfrak{sh}(\alpha)$; or in one of the argument sub-strategies. Crucially, each event receives *exactly one tag*. This is where all our structural constraints on strategies strike in, finally banning the pathological phenomenon of Figure 58.

**Lemma 7.33.** Every event $m \in |\alpha|$ receives exactly one tag following Definition 7.32.

*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, $m \in \mathfrak{sh}(\alpha)$. Assume there are at least two. Take $n \le \alpha m$ minimal s.t. it is a non-initial Opponent question. Then its immediate predecessor is some $q \in \mathcal{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 \mathcal{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 \mathfrak{sh}(\alpha)$. Assume $m \in \alpha_{q,j}$ and $m \in \alpha_{q',j'}$ for $q \in \mathcal{Q}_i, q' \in \mathcal{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 |\mathfrak{sh}(\alpha)|$.

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

<figure><img src="image_92.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 parallel innocence $m_1$ and $n_1$ are positive. By Lemma A.6 so must be $m_{k+1}$, so $m_k$ and $n_p$ are negative. We have a *globule* as in Definition 7.13, so $X$ and $Y$ are complete, and in particular $q$ is answered in $\rho$. Writing $q = m_i, m_{i+1}$ must answer $q$. But since $m \in \alpha_{q,j}, q \to_{\alpha} n^{Qu,-} \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, from Lemma 7.12, $j = j'$. $\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 be defined with events

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

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

The display map requires a careful reindexing of events ending up on the right hand side, illustrated in Figures 64 and 65. For this we split $|\alpha_{q,j}|$ in two subsets: on the one hand, we have those events that depend *statically*, i.e. with respect to $\le_A$ (through $\partial_{\alpha}$) on the primary question $q$ – in Figure 64, those are $q_{i,r}^-, q_{1,r,0}^+, \check{q}_{1,r,0}^-$ and $b_{1,r}^+$. On the other hand,
<figure><img src="image_93.png" /><figcaption>Figure 64: Events of $|\alpha_{q^+,1}|$ of Figure 61</figcaption></figure>

<caption>Figure 65: The corresponding aug. of $\alpha_{q^+,1}$</caption>

the remaining events must follow from new calls to variables in the context – in Figure 64, those are $q_{2r+3}^+$ and $b_{2r+3}^-$. 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 65.

We introduce notations for the canonical embeddings of the set of moves $|A_i|$ and $|A_{i,j}|$ into $|A|$. More precisely, it will be convenient, for each primary question $q \in \mathcal{Q}_i$, to write

$$ \mathrm{inj}_q(-) : |A_i| \to |A| $$

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

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

$$ \partial_{\alpha_{q,j}}(m) = \mathrm{inj}_r(a) \quad \text{if} \quad \partial_{\alpha}(m) = \mathrm{inj}_{q,j}(a), $$

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

where $\mathrm{inj}_l(a) = (1, a)$ and $\mathrm{inj}_r(a) = (2, a)$.

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

**Proposition 7.35.** 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 \mid \theta \in \mathcal{S}(\alpha)\}$, and $\partial_{\alpha_{q,j}}$ in Definition 7.34.

Then, $\alpha_{q,j} : !(&A_i) \vdash !A_{i,j}$ is well-bracketed, causally well-bracketed, parallel innocent.

*Proof.* A routine verification. The key point is that as symmetries of $\alpha$ are order-isomorphisms displayed to symmetries of $A$, it follows that they preserve the tag as in Definition 7.32. $\square$

Finally, we get rid of the ! on the right hand side, using *dereliction der*<sub>A</sub> : !A $\vdash$ A.

**Proposition 7.36.** Consider $q \in \mathcal{Q}_i$ and $1 \le j \le p_i$. Then, $\alpha_{q,j}^\bullet = \mathrm{der}_{A_{i,j}} \odot \alpha_{q,j} : !(&A_i) \vdash A_{i,j}$ is a test strategy with size strictly lesser than $\alpha$.

*Proof.* Using Proposition 4.12, it is easy that $\alpha_{q,j}^\bullet$ is isomorphic, as an ess, to sub-ess of $\alpha_{q,j}$ where Opponent only opens the copy index 0 on the right hand side. There is at least one positive event in $\mathrm{mf}(\alpha)$ but not of $\alpha_{q,j}^\bullet$, namely the primary question $q$. $\square$
$$ \frac{x_A \in \int A \qquad x_B \in \int B}{x_A \otimes x_B \in \int (A \otimes B)} \qquad \frac{x_A \in \int A \qquad x_C \in \int C}{x_A \to x_C \in \int (A \to C)} \qquad \frac{x \in \int A_i \qquad (i \in I)}{(i, x) \in \int (\&_{i \in I} A_i)} \qquad \frac{(x_C^i \in \int C)_{i \in I}}{[x_C^i | i \in I] \in \int C} $$

<caption>Figure 66: Syntax for positions for A, B, C arenas with C strict</caption>

Note $\alpha_{q,j}$ is recovered from $\alpha_{q,j}^{\bullet}$, via the “Bang lemma” [AJM00] (see Appendix D.4):

**Lemma 7.37.** For concrete arenas A, B with B pointed and $\sigma \in \to$-Strat($!A$, $!B$),

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

Summing up, from the original strategy $\alpha : !(&A_i) \vdash \mathbb{X}$, we have now constructed:

$$ \begin{aligned} \mathrm{flow}(\alpha) & : \bigotimes_{1 \le i \le n} \bigotimes_{q \in \mathcal{Q}_i} \mathbb{X}_i \vdash \mathbb{X} \\ \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{aligned} $$

For each primary question $q \in \mathcal{Q}_i$, we use the cartesian closed internal language to form

$$ x_1 : A_1, \dots, x_n : A_n \vdash x_i \alpha_{q,1}^{\bullet} \dots \alpha_{q,p_i}^{\bullet} : \mathbb{X}_i. $$

Let us write $\alpha_q : !(&A_i) \vdash \mathbb{X}_i$ for the resulting strategy. Then, finally,

$$ \mathrm{recomp}(\alpha) = \mathrm{flow}(\alpha) \odot (\bigotimes_{1 \le i \le n} \bigotimes_{q \in \mathcal{Q}_i} \alpha_q) \odot \delta_{&A_i} : !(&A_i) \vdash \mathbb{X}, \quad (7.2) $$

is our candidate to reconstruct $\alpha$. Here, for B an arena 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$.

7.4.4. *Positions of recomp($\alpha$)*. We expect that $\mathrm{recomp}(\alpha) \approx \alpha$, but we shall only prove $\mathrm{recomp}(\alpha) = \alpha$ – this is simpler as positions compose simply relationally.

To help reason on positions, we adopt a syntax presented in Figure 66, following the bijections of Lemma 7.11. We also write $x_A \vdash x_B \in \int (A \vdash B)$ for all $x_A \in \int A$ and $x_B \in \int B$.

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

**Lemma 7.38.** For B strict, the positions $\int \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 \int (!B \vdash (!B)^{\otimes n}) $$

where $x_i \in \int B$ for all $1 \le i \le n$.

By a direct variation of Lemma 4.18. Next we analyse the positions of $\alpha_q$ for $q \in \mathcal{Q}_i$:

**Lemma 7.39.** For any $q \in \mathcal{Q}_i$, the non-empty positions $\int \alpha_q$ are exactly those of the form

$$ \left( \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 \int (!(&A_i) \vdash \mathbb{X}_i) \right) $$

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

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

$$ !(&A_i) \xrightarrow{\delta} \otimes_{p_i+1} !(&A_i) \xrightarrow{(\bigotimes_{1 \le j \le p_i} (\alpha_{q,j}^{\bullet})^{\dagger}) \otimes [x_i]} \otimes_{1 \le j \le p_i} !A_{i,j}) \otimes A_i \xrightarrow{\mathrm{ev}} \mathbb{X}_i $$

in $\to$-Strat. The characterisation follows from Proposition 7.8, Lemma 7.38, Lemma 7.37, and a direct verification analogous to Lemma 7.38 for other copycat-like strategies involved. $\square$
From all those, we may characterise the positions of recomp($\alpha$) as

**Corollary 7.40.** Non-empty positions of recomp($\alpha$) are exactly those of the form

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

where for all $1 \le i \le n$, $\mathcal{Q}'_i$ is a subset of $\mathcal{Q}_i$, all $v_q$ are non-empty, and:

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

*Proof.* Direct from Lemmas 7.38, 7.39 and Proposition 7.8. □

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

**7.4.5. Positions of $\alpha$.** We write $\mathcal{C}^c(\alpha)$ for the complete, non-empty configurations of $\alpha$. If $x \in \mathcal{C}^c(\alpha)$, then $\mathfrak{sh}(x) = \{m \in x \mid m \in \mathfrak{sh}(\alpha)\} \in \mathcal{C}^c(\mathfrak{sh}(\alpha))$ and we write $\mathcal{Q}^x = \mathcal{Q} \cap x$, and $\mathcal{Q}_i^x$ likewise. For each $q \in \mathcal{Q}_i^x$ and $1 \le j \le p_i$, we also have $x_{q,j} = \{m \in x \mid m \in \alpha_{q,j}\} \in \mathcal{C}(\alpha_{q,j})$.

From Lemma 7.33, this informs $x = \mathfrak{sh}(x) \oplus (\biguplus_{1 \le i \le n} \biguplus_{q \in \mathcal{Q}_i^x} \biguplus_{1 \le j \le p_i} x_{q,j})$.

We show that all complete non-empty configurations of $\alpha$ arise in this way:

**Lemma 7.41.** This yields a bijection between $\mathcal{C}^c(\alpha)$ and pairs $(x, (x_{q,j})_{1 \le i \le n, q \in \mathcal{Q}_i^x, 1 \le j \le p_i})$ where $x \in \mathcal{C}^c(\mathfrak{sh}(\alpha))$, $x_{q,j} \in \mathcal{C}(\alpha_{q,j})$ complete for all $1 \le i \le n$, $q \in \mathcal{Q}_i^x$ and $1 \le j \le p_i$.

Moreover, writing $[x, (x_{q,j})_{i,q,j}] = x \oplus (\oplus_{i,q,j} x_{q,j}) \in \mathcal{C}(\alpha)$ this correspondence, we have
$$ \partial_{\alpha}([x, (x_{q,j})_{i,q,j}]) = (\biguplus_{1 \le i \le n} \biguplus_{q \in \mathcal{Q}_i^x} ([\mathrm{inj}_q(z_{q,1} \to \dots \to z_{q,p_i} \to v_q)] \oplus [\biguplus_{1 \le j \le p_i} \mathrm{inj}_j(y_{q,j})])) \oplus \mathrm{inj}_r(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) = \text{inj}_l(\bigotimes_{1 \le i \le n} \bigotimes_{q \in \mathcal{Q}_i^x} v_q) \oplus \text{inj}_r(v) \qquad \partial_{\alpha_{q,j}}(x_{q,j}) = \text{inj}_l(y_{q,j}) \oplus \text{inj}_r(z_{q,j}). $$

*Proof.* From $x \in \mathcal{C}^c(\alpha)$, we get $(\mathfrak{sh}(x), (x_{q,j})_{i,q,j})$ from the decomposition above. Reciprocally, from $(x, (x_{q,j})_{i,q,j})$ we get a configuration in $\mathcal{C}^c(\alpha)$ as their union; it is down-closed by construction and consistent by determinism of $\alpha$ (as any immediate negative conflict originates from the arena, and hence appears in one of the components). Finally, the characterization of the display map follows from display maps of $\text{flow}(\alpha)$ and $\alpha_{q,j}$. □

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

From this we may finally conclude the proof of factorization:

**Corollary 7.42.** The strategies $\alpha$ and recomp($\alpha$) are positionally equivalent.

*Proof.* Taking symmetry classes from Lemma 7.41, we obtain the same characterization of non-empty complete positions of $\alpha$ as in Corollary 7.40. □

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

**7.4.6. Syntactic factorization.** Finally, we must reformulate the result relying on the cartesian closed structure only. The first-order **substrategy** $\mathfrak{fo}(\alpha) \in \mathcal{D}\mathfrak{-Strat}!(\&1 \le i \le n \ \&_q \in \mathcal{Q}_i \ \mathbb{X}_i, \mathbb{X})$ is obtained in the obvious way from $\mathfrak{flow}(\alpha)$ using the Seely category structure. Using Corollary 7.42, Proposition 7.36, and laws of a Seely category, we conclude:

**Corollary 7.43.** Any test strategy $\alpha : !!(\&A_i) \vdash \mathbb{X}$ factors as a composition of test strategies

$$ \alpha \equiv \mathfrak{fo}(\alpha) \odot! \langle x_i \alpha_{q,1}^{\bullet} \dots \alpha_{q,p_i}^{\bullet} \mid 1 \le i \le n, q \in \mathcal{Q}_i \rangle, $$

where for all $1 \le i \le n$, $q \in \mathcal{Q}_i$ and $1 \le j \le p_i$, $\alpha_{q,j}^{\bullet}$ has size strictly lesser than $\alpha$.
<figure><img src="image_97.png" /><figcaption>Figure 67: An undefinable first-order strategy</figcaption></figure>

**7.5. Finite Definability.** Corollary 7.43 allows us to handle the higher-order structure, it only remains to prove definability for first-order test strategies.

**7.5.1. First-order definability.** Not every first-order test strategy is exactly definable in PCF$_{‖}$. For instance, that in Figure 67 is not series-parallel, while it is fairly easy to prove that all PCF$_{‖}$-definable terms on this type yield a series-parallel causal dependency. In general, we have not yet managed to properly understand which first-order strategies are definable. Luckily, we do not need to. Indeed, given a test $\alpha$ it is sufficient to find $M$ such that $[[M]]$ is *positionally equivalent* from $\alpha$. In PCF$_{‖}$, without interference, the order of evaluation is unobservable; and positional equivalence is not sensitive to it. So our definability process will simply sequentialize $\alpha$, while preserving its positions.

Consider $\Gamma = x_1 : \mathbb{X}_1, \dots, x_n : \mathbb{X}_n$, some ground type $\mathbb{X}$, and a test strategy:

$$ \alpha : !((\&\mathbb{X}_i) \vdash \mathbb{X}). $$

If $\frown \alpha$ is empty, any diverging term $M$ will satisfy $\frown[[M]] = \emptyset$. Otherwise, there is some $x \in \mathscr{C}^c(\alpha)$. If $\alpha$ has no primary question, then $x = \{q_0^{Q,-}, a^{A,+}\}$, with $a$ answering $q_0$ – write $\partial_{\alpha}(a) = v$ some answer in $\mathbb{X}$. But then by determinism of $\alpha$, it cannot have any other move and $\alpha \approx [[v]]$. Otherwise, if $\alpha$ has a primary question, it has one $a \in \mathscr{Q}$ which is **minimal**, i.e. it only depends on the initial move. But then $q$ appears in every $x \in \mathscr{C}^c(\alpha)$:

**Lemma 7.44.** For any minimal primary question $q$, for any $y \in \mathscr{C}^c(\alpha)$, we have $q \in y$.

*Proof.* By determinism, $y \cup \{q_0, q\} \in \mathscr{C}(\alpha)$. Since $y$ is complete, there is $a^{A,+} \in y$ such that $a$ answers $q_0$. But then, by Lemma 7.15 we have $q \leq_{\alpha} a$. It follows that $q \in y$ as required. $\square$

Choose $q \in \mathscr{Q}_i$ minimal. As $q$ appears in all non-empty complete configurations, it is safe to first making a call to $x_i$, then branching 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 7.45.** For $q \in \mathscr{Q}_i$ minimal, there is a test strategy $\alpha_{(q)} : !((\&\mathbb{X}_i) \& \mathbb{X}_i) \vdash \mathbb{X}$ s.t.

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

(2) for all $x \vdash w \in \frown \alpha$, then $x = x' + [(i,v)]$ such that $x' + [(n+1,v)] \vdash w \in \frown \alpha_{(q)}$.
*Proof.* The strategy $\alpha_{(q)}$ has components as for $\alpha$ except the display map, which sends $q$ and its answers to the new component. The characterisation of positions is straightforward. $\square$

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

**Lemma 7.46.** For any $v \in V$, the positions of $\langle \mathrm{id}_{\&X_i}, v \rangle^\dagger$ are exactly those of the form

$$x \vdash x + p \cdot [(n + 1, v)] \in \int ((\&X_i) \vdash !((\&X_i) \& X_i)),$$

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

*Proof.* As $\int(-)$ preserves the identity, $\int(\mathrm{id}_{\&X_i}^\dagger)$ comprises exactly positions of the form $x \vdash x$, and likewise, $fv^\dagger$ comprises exactly positions of the form $p \cdot v$ for some $p \in \mathbb{N}$. The lemma then follows from Proposition 7.8 and by applying the laws of Seely categories for $\to$-Strat. $\square$

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

**Lemma 7.47.** We have the following properties:

(1) for any $x \vdash w \in \int\alpha$, there is $x = x' + [(i, v)]$ such that $x' \vdash w \in \int\alpha_{(qv)}$,

(2) for any $x \vdash w \in \int\alpha_{(qv)}$, we have $x + [(i, v)] \vdash w \in \int\alpha$.

*Proof.* By definition, we have $\alpha_{(qv)} = \alpha_{(q)} \odot \langle \mathrm{id}_{\&X_i}, v \rangle^\dagger$, so by Proposition 7.8,

$$\int\alpha_{(qv)} = \int(\alpha_{(q)}) \odot \int(\langle \mathrm{id}_{\&X_i}, v \rangle^\dagger).$$

The lemma directly follows by Lemmas 7.45 and 7.46. $\square$

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

We have $\alpha_{(qv)}$ a test strategy with size strictly smaller than that of $\alpha$. By IH there is

$$x_1 : X_1, \dots, x_n : X_n \vdash N_{(qv)} : X_i,$$

for each $v \in V$, such that $\llbracket N_{(qv)} \rrbracket \equiv \alpha_{(qv)}$. Finally, we define $x_1 : X_1, \dots, x_n : X_n \vdash M : X$ as

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

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

$$x_1 : X_1, \dots, x_n : X_n, x : X_i \vdash M' : X$$

for the iterated if statement, i.e. $M$ is let $x = x_i$ in $M'$. It remains to analyze the positions of $\llbracket M \rrbracket$ and $\llbracket M' \rrbracket$ to show that $\llbracket M \rrbracket \equiv \alpha$ as required. We start with the positions of $\llbracket M' \rrbracket$.

**Lemma 7.48.** We have the following properties:

(1) for any $x + p \cdot [(n + 1, v)] \vdash w \in \int\llbracket M' \rrbracket$ where $x \in \int((\&1 \le i \le n X_i))$, $x \vdash w \in \int\llbracket N_{(qv)} \rrbracket$.

(2) for any $x \vdash w \in \int\llbracket N_{(qv)} \rrbracket$, then there is $p \in \mathbb{N}$ s.t. $x + p \cdot [(n + 1, v)] \vdash w \in \int\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 $\llbracket M' \rrbracket \odot! \langle \mathrm{id}, v \rangle = \llbracket N_{(qv)} \rrbracket$. The claim then follows by Proposition 7.8 and Lemma 7.46. $\square$

<figure><img src="image_100.png" /></figure>
It remains to take the interpretation of the let construction into account. Recall that

$$[[M]] = \text{let}_{\mathbb{X}_i, \mathbb{X}} \odot! \langle \pi_i, \Lambda^!([[M']]) \rangle : !(&\mathbb{X}_i) \vdash \mathbb{X}$$

where $\text{let}_{\mathbb{X}_i, \mathbb{X}} : ! (\mathbb{X}_i \& (!\mathbb{X}_i \to \mathbb{X})) \vdash \mathbb{X}$. We characterize the positions of $\text{let}_{\mathbb{X}_i, \mathbb{X}}$ as follows.

**Lemma 7.49.** The non-empty positions of $\text{let}_{\mathbb{X}_i, \mathbb{X}}$ are exactly those of the form

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

for $\mathbf{v} \in f\mathbb{X}_i$, $\mathbf{w} \in f\mathbb{X}$, and $p \in \mathbb{N}$.

*Proof.* A direct analysis of positions reached by complete configurations of $\text{let}_{\mathbb{X}_i, \mathbb{X}}$. $\square$

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

**Lemma 7.50.** We have the following two properties:

(1) for any $x \vdash w \in f[[M]]$, there is $x' = x' + [(i, v)]$ such that $x' \vdash w \in f[[N_{(qv)}]]$,

(2) for any $x \vdash w \in f[[N_{(qv)}]]$, we have $x + [(i, v)] \vdash w \in f[[M]]$.

*Proof.* By Lemmas 7.48 and 7.49. $\square$

So we have $[[M]] = \alpha$ as desired. Summing up, we have proved:

**Proposition 7.51.** For $\alpha : !(&\mathbb{X}_i) \vdash \mathbb{X}$ any test strategy, there is

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

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

### 7.5.2. Finite definability.
We may now conclude the proof of finite definability.

**Corollary 7.52.** Let $\Gamma \vdash A$ be a PCF typing judgment, and $\alpha : [[\Gamma]] \vdash [[A]]$ a test strategy.

Then, there is $\Gamma \vdash M : A$ such that $[[M]] = \alpha$.

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

$$\alpha \equiv \mathbf{fo}(\alpha) \odot! \langle x_i, \alpha_{q,1}^{\bullet}, \dots, \alpha_{q,p_i}^{\bullet} \mid 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}^{\bullet} : !(&A_i) \vdash A_{i,j}$ a test 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}$$

such that $[[N_{q,j}] = \alpha_{q,j}]$. Let us write $\mathcal{Q}_i = \{q_{i,1}, \dots, q_{i,k_i}\}$. By Proposition 7.51 there is also

$$x_{q_{1,1}} : \mathbb{X}_1, \dots, x_{q_{1,k_1}} : \mathbb{X}_1, \dots, x_{q_{n,1}} : \mathbb{X}_n, \dots, x_{q_{n,k_n}} : \mathbb{X}_n \vdash M_{\mathbf{fo}} : \mathbb{X}$$

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

$$x_1 : A_1, \dots, x_n : A_n \vdash M_{\mathbf{fo}}[x_i N_{q_{i,l},1} \dots N_{q_{i,l},p_i}/x_{q_{i,l}}] : \mathbb{X}.$$

Then we may finally compute

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

using the substitution lemma for cartesian closed categories, compatibility of interpretation with the internal language, the properties of $M_{\mathbf{fo}}$ and $N_{q,j}$ and that $\equiv$ is a congruence. $\square$
7.6. Full Abstraction for PCF$_{‖}$. We may now prove our final full abstraction result.

**Theorem 7.53.** The model $\rightarrow\text{-Strat}_i^{\text{wb,inn}}$ is intensionally fully abstract for PCF$_{‖}$.

*Proof.* Consider $\vdash M, N : A$ such that $M \sim N$, and assume that $[[M]] \vdash [[N]]$, i.e. there is a test $\alpha \in \rightarrow\text{-Strat}_i^{\text{wb,inn}}([A], [U])$ such that, w.l.o.g., $\alpha \odot! [[M]] \downarrow$ and $\alpha \odot! [[N]] \uparrow$.

By Corollary 7.28, we assume $\alpha$ is additionally finite. We consider $\text{comp}(\alpha)$ as defined in Proposition 7.17. By construction it is well-bracketed, parallel innocent, and finite. By Proposition 7.17 it is causally well-bracketed, so a *test strategy*. Proposition 7.17 also states that $\text{comp}(\alpha) \equiv \alpha$ which is a congruence by Corollary 7.9, so

$$ \text{comp}(\alpha) \odot! [[M]] \downarrow, \quad \text{comp}(\alpha) \odot! [[N]] \uparrow. $$

By Corollary 7.52, there is a term $x : A \vdash T : \mathbb{U}$ such that $[[T]] \equiv \text{comp}(\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] \odot! [[M]]] \equiv \text{comp}(\alpha) \odot! [[M]] \downarrow, $$

and likewise, $[[C[N]]] \equiv \text{comp}(\alpha) \odot! [[N]]$. By Theorem 4.40, $C[M] \downarrow$. By hypothesis $M \sim N$, so $C[N] \downarrow$. By Theorem 4.40 again, $[[C[N]]] \downarrow$, hence $\text{comp}(\alpha) \odot! [[N]] \downarrow$, contradiction. $\square$

We may finally answer our main question positively, with the following theorem.

**Theorem 7.54.** The model $\rightarrow\text{-Strat}_i^{\text{wb}}$ supports parallel innocence and sequentiality, s.t.

$$ \begin{align*} \rightarrow\text{-Strat}_i^{\text{wb}} & \text{ is fully abstract for } \text{IA}_{\parallel}, \\ \rightarrow\text{-Strat}_i^{\text{wb,inn}} & \text{ is fully abstract for } \text{PCF}_{\parallel}, \\ \rightarrow\text{-Strat}_i^{\text{wb,seq}} & \text{ is fully abstract for } \text{IA}, \\ \rightarrow\text{-Strat}_i^{\text{wb,seq,inn}} & \text{ is fully abstract for } \text{PCF}, \end{align*} $$

Thus parallel innocence exactly bans interference, and sequentiality exactly bans parallelism. Through this theorem, we have successfully disentangled parallelism and interference.

## 8. CONCLUSION

It is puzzling that disantengling parallelism and interference requires such an intricate machinery whereas the original *semantic cube* arose almost “by accident” from minor variations of the Hyland-Ong model of PCF.

Our interpretation is that computational effects may be organized in distinct categories. Some effects, such as interference and control, bring more freedom as to how execution and its control flow explores a piece of code. Once a sufficiently general mathematical description of the control flow is given (such as the original Hyland-Ong setting for sequential deterministic computation), this additional freedom may be studied and characterized. In contrast, other effects such as non-determinism and parallelism, affect the inherent structure of execution itself: non-determinism quite explicitely so by generating non-deterministic branching, and parallelism in a more DAG-like fashion – we refer to both under the umbrella name “branching effects”. What our paper demonstrates – along with earlier papers on non-deterministic innocence [CCW14, TO15] – is that if we aim to realize fully the “unified semantic landscape” of Abramsky’s programme, we must first deal with branching effects. Non-branching effects should follow by characterizing the causal patterns they allow<fnref n="28" />.

<footnote n="28">²⁸The line is not always so clear between branching and non-branching effects: for instance, in a sequential setting interference is non-branching, but in a parallel setting it generates non-deterministic choice.</footnote>
What other branching effects are around? One currently at the focus of the semantics community is probabilistic choice. By itself, the probabilistic branching structure is not much harder than non-deterministic choice [TO14, CCPW18]. However its interaction with non-deterministic and parallel branching is a significant challenge, and one of the remaining scientific and technical barriers for a truly unified game semantics landscape.

**Acknowledgments.** First we would like to thank Glynn Winskel. Though he has not participated in the developments in this paper per se, we rely deeply on his pioneering work - and our subsequent collaborations - on concurrent games. We owe a lot to his insight.

This work was supported by the ANR project DyVerSe (ANR-19-CE48-0010-01); and by Labex MiLyon (ANR-10-LABX-0070) of Université de Lyon, within the program “In-vestissements d’Avenir” (ANR-11-IDEX-0007), operated by the French ANR.

## REFERENCES

[AHM98] Samson Abramsky, Kohei Honda, and Guy McCusker. A fully abstract game semantics for general references. In *Thirteenth Annual IEEE Symposium on Logic in Computer Science, Indianapolis, Indiana, USA, June 21-24, 1998*, pages 334–344, 1998.

[AJ09] Samson Abramsky and Radha Jagadeesan. Game semantics for access control. *Electr. Notes Theor. Comput. Sci.*, 249:135–156, 2009.

[AJM00] Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for PCF. *Inf. Comput.*, 163(2):409–470, 2000.

[AM96] Samson Abramsky and Guy McCusker. Linearity, sharing and state: a fully abstract game semantics for idealized algol with active expressions. *Electron. Notes Theor. Comput. Sci.*, 3:2–14, 1996.

[AM99a] Samson Abramsky and Guy McCusker. Game semantics. In *Computational logic*, 1999.

[AM99b] Samson Abramsky and Paul-André Melliès. Concurrent games and full completeness. In *14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999*, pages 431–442. IEEE Computer Society, 1999.

[Cas17] Simon Castellan. *Concurrent structures in game semantics*. (*Structures concurrentes en sémantique des jeux*). PhD thesis, University of Lyon, France, 2017.

[CC16] Simon Castellan and Pierre Clairambault. Causality vs. interleavings in concurrent game semantics. In Josée Desharnais and Radha Jagadeesan, editors, *27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Québec City, Canada*, volume 59 of *LIPIcs*, pages 32:1–32:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.

[CCHW18] Simon Castellan, Pierre Clairambault, Jonathan Hayman, and Glynn Winskel. Non-angelic concurrent game semantics. In Christel Baier and Ugo Dal Lago, editors, *Foundations of Software Science and Computation Structures - 21st International Conference, FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings*, volume 10803 of *Lecture Notes in Computer Science*, pages 3–19. Springer, 2018.

[CCPW18] Simon Castellan, Pierre Clairambault, Hugo Paquet, and Glynn Winskel. The concurrent game semantics of probabilistic PCF. In *Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018*, pages 215–224, 2018.

[CCRW17] Simon Castellan, Pierre Clairambault, Silvain Rideau, and Glynn Winskel. Games and strategies as event structures. *Logical Methods in Computer Science*, 13(3), 2017.

[CCW14] Simon Castellan, Pierre Clairambault, and Glynn Winskel. Symmetry in concurrent games. In Thomas A. Henzinger and Dale Miller, editors, *Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014*, pages 28:1–28:10. ACM, 2014.

[CCW15] Simon Castellan, Pierre Clairambault, and Glynn Winskel. The parallel intensionally fully abstract games model of PCF. In *30th Annual ACM/IEEE Symposium on Logic in Computer Science*, 2014.
*Science*, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 232-243. IEEE Computer Society, 2015.

[CCW19] Simon Castellan, Pierre Clairambault, and Glynn Winskel. Thin games with symmetry and concurrent hyland-ong games. *Log. Methods Comput. Sci.*, 15(1), 2019.

[CD15] Pierre Clairambault and Peter Dybjer. Game semantics and normalization by evaluation. In *Andrew M. Pitts, editor, Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings*, volume 9034 of *Lecture Notes in Computer Science*, pages 56-70. Springer, 2015.

[CdV20] Pierre Clairambault and Marc de Visme. Full abstraction for the quantum lambda-calculus. *Proc. ACM Program. Lang.*, 4(POPL):63:1-63:28, 2020.

[CH10] Pierre Clairambault and Russ Harmer. Totality in arena games. *Ann. Pure Appl. Logic*, 161(5):673-689, 2010.

[Cur98] Pierre-Louis Curien. Abstract Böhm trees. *Mathematical Structures in Computer Science*, 8(6):559-591, 1998.

[Cur06] Pierre-Louis Curien. Notes on game semantics. 2006. Unpublished.

[CY19] Simon Castellan and Nobuko Yoshida. Two sides of the same coin: session types and game semantics: a synchronous side and an asynchronous side. *Proc. ACM Program. Lang.*, 3(POPL):27:1-27:29, 2019.

[DH00] Vincent Danos and Russ Harmer. Probabilistic game semantics. In *15th Annual IEEE Symposium on Logic in Computer Science, Santa Barbara, California, USA, June 26-29, 2000*, pages 204-213. IEEE Computer Society, 2000.

[DHR96] Vincent Danos, Hugo Herbelin, and Laurent Regnier. Game semantics & abstract machines. In *Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996*, pages 394-405. IEEE Computer Society, 1996.

[dV20] Marc de Visme. *Quantum Game Semantics*. PhD thesis, University of Lyon, France, 2020.

[FP09] Claudia Faggian and Mauro Piccolo. Partial orders, event structures and linear strategies. In Pierre-Louis Curien, editor, *Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009. Proceedings*, volume 5608 of *Lecture Notes in Computer Science*, pages 95-111. Springer, 2009.

[GG12] Murdoch Gabbay and Dan R. Ghica. Game semantics in the nominal model. In Ulrich Berger and Michael W. Mislove, editors, *Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics, MFPS 2012, Bath, UK, June 6-9, 2012*, volume 286 of *Electronic Notes in Theoretical Computer Science*, pages 173-189. Elsevier, 2012.

[Gir87] Jean-Yves Girard. Linear logic. *Theor. Comput. Sci.*, 50:1-102, 1987.

[GM03] Dan R. Ghica and Guy McCusker. The regular-language semantics of second-order idealized ALGOL. *Theor. Comput. Sci.*, 309(1-3):469-502, 2003.

[GM08] Dan R. Ghica and Andrzej S. Murawski. Angelic semantics of fine-grained concurrency. *Ann. Pure Appl. Log.*, 151(2-3):89-114, 2008.

[GMO06] Dan R. Ghica, Andrzej S. Murawski, and C.-H. Luke Ong. Syntactic control of concurrency. *Theor. Comput. Sci.*, 350(2-3):234-251, 2006.

[Gou17] Jean Goubault-Larrecq. Isomorphism theorems between models of mixed choice. *Math. Struct. Comput. Sci.*, 27(6):1032-1067, 2017.

[Gri90] Timothy Griffin. A formulae-as-types notion of control. In Frances E. Allen, editor, *Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, California, USA, January 1990*, pages 47-58. ACM Press, 1990.

[GT12] Dan R. Ghica and Nikos Tzevelekos. A system-level game semantics. In Ulrich Berger and Michael W. Mislove, editors, *Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics, MFPS 2012, Bath, UK, June 6-9, 2012*, volume 286 of *Electronic Notes in Theoretical Computer Science*, pages 191-211. Elsevier, 2012.

[Har04] Russ Harmer. Innocent game semantics. *Lecture notes*, 2007, 2004.

[HHM07] Russ Harmer, Martin Hyland, and Paul-André Melliès. Categorical combinatorics for innocent strategies. In *22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July 2007, Wroclaw, Poland, Proceedings*, pages 379-388, 2007.
[HM99] Russ Harmer and Guy McCusker. A fully abstract game semantics for finite nondeterminism. In *14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999*, pages 422–430. IEEE Computer Society, 1999.

[HO00] J. M. E. Hyland and C.-H. Luke Ong. On full abstraction for PCF: I, II, and III. *Inf. Comput.*, 163(2):285–408, 2000.

[Jab15] Guilhem Jaber. Operational nominal game semantics. In Andrew M. Pitts, editor, *Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings*, volume 9034 of *Lecture Notes in Computer Science*, pages 264–278. Springer, 2015.

[Lai97] James Laird. Full abstraction for functional languages with control. In *LICS*, pages 58–67, 1997.

[Lai01a] James Laird. A fully abstract game semantics of local exceptions. In *LICS*, 2001.

[Lai01b] James Laird. A game semantics of idealized CSP. *Electr. Notes Theor. Comput. Sci.*, 45:232–257, 2001.

[Lai04] James Laird. A calculus of coroutines. In Josep Díaz, Juhani Karhumäki, Arto Lepistö, and Donald Sannella, editors, *Automata, Languages and Programming: 31st International Colloquium, ICALP 2004, Turku, Finland, July 12-16, 2004. Proceedings*, volume 3142 of *Lecture Notes in Computer Science*, pages 882–893. Springer, 2004.

[Ler09] Xavier Leroy. Formal verification of a realistic compiler. *Commun. ACM*, 52(7):107–115, 2009.

[Lev14] Paul Blain Levy. Transition systems over games, 2014. Talk at the *Chocola* seminar.

[Loa01] Ralph Loader. Finitary PCF is not decidable. *Theor. Comput. Sci.*, 266(1-2):341–364, 2001.

[LS88] Joachim Lambek and Philip J Scott. *Introduction to higher-order categorical logic*, volume 7. Cambridge University Press, 1988.

[LS14] Paul Blain Levy and Sam Staton. Transition systems over games. In *Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, pages 64:1–64:10, 2014.

[McC98] Guy McCusker. *Games and full abstraction for a functional metalanguage with recursive types*. CPHC/BCS distinguished dissertations. Springer, 1998.

[Mel03] Paul-André Melliès. Asynchronous games 1: A group-theoretic formulation of uniformity. *Manuscript, Available online*, 2003.

[Mel04] Paul-André Melliès. Asynchronous games 2: The true concurrency of innocence. In Philippa Gardner and Nobuko Yoshida, editors, *CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings*, volume 3170 of *Lecture Notes in Computer Science*, pages 448–465. Springer, 2004.

[Mel05] Paul-André Melliès. Asynchronous games 4: A fully complete model of propositional linear logic. In *20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26-29 June 2005, Chicago, IL, USA, Proceedings*, pages 386–395. IEEE Computer Society, 2005.

[Mel09] Paul-André Melliès. Categorical semantics of linear logic. *Panoramas et Synthèse*, 2009.

[Mel19] Paul-André Melliès. Categorical combinatorics of scheduling and synchronization in game semantics. *Proc. ACM Program. Lang.*, 3(POPL):23:1–23:30, 2019.

[MM07] Paul-André Melliès and Samuel Mimram. Asynchronous games: Innocence without alternation. In Luís Caires and Vasco Thudichum Vasconcelos, editors, *CONCUR 2007 - Concurrency Theory, 18th International Conference, CONCUR 2007, Lisbon, Portugal, September 3-8, 2007, Proceedings*, volume 4703 of *Lecture Notes in Computer Science*, pages 395–411. Springer, 2007.

[MT10] Paul-André Melliès and Nicolas Tabareau. Resource modalities in tensor logic. *Ann. Pure Appl. Log.*, 161(5):632–653, 2010.

[MT13] Andrzej S. Murawski and Nikos Tzevelekos. Deconstructing general references via game semantics. In Frank Pfenning, editor, *Foundations of Software Science and Computation Structures - 16th International Conference, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings*, volume 7794 of *Lecture Notes in Computer Science*, pages 241–256. Springer, 2013.

[Mur03] Andrzej S. Murawski. On program equivalence in languages with ground-type references. In *18th IEEE Symposium on Logic in Computer Science (LICS 2003), 22-25 June 2003, Ottawa, Canada, Proceedings*, page 108. IEEE Computer Society, 2003.
[Mur07] Andrzej S. Murawski. Bad variables under control. In Jacques Duparc and Thomas A. Henzinger, editors, *Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, Proceedings*, volume 4646 of Lecture Notes in Computer Science, pages 558-572. Springer, 2007.

[Mur10] Andrzej S. Murawski. Full abstraction without synchronization primitives. *Electr. Notes Theor. Comput. Sci.*, 265:423-436, 2010.

[Ong02] C.-H. Luke Ong. Observational equivalence of 3rd-order idealized algol is decidable. In *17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings*, pages 245-256. IEEE Computer Society, 2002.

[Paq20] Hugo Paquet. *Probabilistic concurrent game semantics*. PhD thesis, PhD thesis, University of Cambridge, 2020.

[Plo77] Gordon D. Plotkin. LCF considered as a programming language. *Theor. Comput. Sci.*, 5(3):223-255, 1977.

[Plo81] Gordon D. Plotkin. Post-graduate lecture notes in advanced domain theory (incorporating the "Pisa Notes"). *Dept. of Computer Science, Univ. of Edinburgh*, 1981.

[RW11] Silvain Rideau and Glynn Winskel. Concurrent strategies. In *Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, June 21-24, 2011, Toronto, Ontario, Canada*, pages 409-418. IEEE Computer Society, 2011.

[SBCA15] Gordon Stewart, Lennart Beringer, Santiago Cuellar, and Andrew W. Appel. Compositional compcert. In Sriram K. Rajamani and David Walker, editors, *Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015*, pages 275-287. ACM, 2015.

[SYW$^{+}$16] Sam Staton, Hongseok Yang, Frank D. Wood, Chris Heunen, and Ohad Kammar. Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, *Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016*, pages 525-534. ACM, 2016.

[TO14] Takeshi Tsukada and C.-H. Luke Ong. Innocent strategies are sheaves over plays - deterministic, non-deterministic and probabilistic innocence. *CoRR*, abs/1409.2764, 2014.

[TO15] Takeshi Tsukada and C.-H. Luke Ong. Nondeterminism in game semantics via sheaves. In *30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015*, pages 220-231. IEEE Computer Society, 2015.

[VKS19] Matthijs Vákár, Ohad Kammar, and Sam Staton. A domain theory for statistical probabilistic programming. *Proc. ACM Program. Lang.*, 3(POPL):36:1-36:29, 2019.

[Win07] Glynn Winskel. Event structures with symmetry. *Electr. Notes Theor. Comput. Sci.*, 172:611-652, 2007.

[Win12] Glynn Winskel. Deterministic concurrent strategies. *Formal Asp. Comput.*, 24(4-6):647-660, 2012.

[Win13] Glynn Winskel. Strategies as profunctors. In *FoSSaCS*, pages 418-433, 2013.