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

HAL
open science

# Disentangling Parallelism and Interference in Game Semantics

Simon Castellan, Pierre Clairambault

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

## To cite this version:

Simon Castellan, Pierre Clairambault. Disentangling Parallelism and Interference in Game Semantics. 2021. [hal-03182043](https://hal.science/hal-03182043)

HAL Id: hal-03182043

https://hal.science/hal-03182043

Preprint submitted on 26 Mar 2021

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

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

SIMON CASTELLAN AND PIERRE CLAIRAMBAULT

Inria, Univ Rennes, CNRS, IRISA

e-mail address: Simon.Castellan@inria.fr

Univ Lyon, EnsL, UCBL, CNRS, LIP, F-69342, LYON Cedex 07, France

e-mail address: Pierre.Clairambault@ens-lyon.fr

ABSTRACT. Game semantics is a denotational semantics presenting compositionally the computational behaviour of various kinds of effectful programs. One of its celebrated achievement is to have obtained full abstraction results for programming languages with a variety of computational effects, in a *single* framework. This is known as the *semantic cube* or *Abramsky's cube*, which for sequential deterministic programs establishes a correspondence between certain conditions on strategies ("innocence", "well-bracketing", "visibility") and the absence of matching computational effects.

Outside of the sequential deterministic realm, there are still a wealth of game semantics-based full abstraction results; but they no longer fit in a unified canvas. In particular, Ghica and Murawski's fully abstract model for shared state concurrency (IA$_{‖}$) does not have a matching notion of pure parallel program – we say that parallelism and interference (i.e. state plus semaphores) are *entangled*. In this paper we construct a causal version of Ghica and Murawski's model, also fully abstract for IA$_{‖}$. We provide compositional conditions *parallel innocence* and *sequentiality*, respectively banning interference and parallelism, and leading to four full abstraction results. To our knowledge, this is the first extension of Abramsky's *semantic cube* programme beyond the sequential deterministic world.

INTRODUCTION

How to *prove* that a program *P* is correct, or equivalent to *P'*? This simple question, prerequisite for formally validating software, lies at the heart of decades of work in semantics. Its study prompted a wealth of developments, each with its methodology and scope. *Operational semantics* axiomatizes execution directly on syntax, while *denotational semantics* gives meaning to programs by embedding them in a syntax-independent mathematical space.

*Operational semantics* is powerful and extensible, perfectly fit for formalization in a proof assistant – it is, for instance, behind the celebrated CompCert project [Ler09]. On the other hand, its deployment often follows from ad-hoc choices, and it is not robust to variations in the language. It is tied to syntax and struggles with compositionality<fnref n="1" />. *Denotational*

Key words and phrases: Denotational semantics, game semantics, concurrent games.

<footnote n="1">¹Operational semantics can be made compositional, but behind lie denotational structures: for instance, the operational semantics behind the recent *Compositional CompCert* [SBCA15] “bears much in common” (quoting the paper) with Ghica and Tzevelekos’ operational reconstruction of game semantics [GT12].</footnote>
semantics is syntax-independent, and often more principled. It is a great tool to reason about program equivalence (two programs being equivalent if they denote the same object), to prove general properties of languages (e.g. termination), and it comes with compositional reasoning principles. The wider mathematical space in which programs are embedded sometimes suggests new useful constructs (it is the birth story of Linear Logic [Gir87]). In exchange, it is more mathematically demanding and often quite brittle: distinct fragments of the same language may require radically different representations. Traditional denotational semantics (e.g. Scott domains) model programs as functions, through their input/output behaviour. Effects (e.g. state, non-determinism, etc) can be captured via monads which do not readily combine. Though combining effects has been a driving question in denotational semantics these past decades, it is hardly a streamlined process. For instance, though there is significant recent research activity around domain settings supporting probabilities and higher-order [SYW+16, VKS19], it is unclear how they combine with non-determinism [Gou17], let alone concurrency; nor how all these models relate together.

*Game semantics* [HO00, AJM00], though also denotational, takes a different approach: instead of a function it represents a program as a *strategy*, a collection of (representations of) its interactions against execution environments. Once executions are first-class citizens (called *plays*) one can characterise those achievable with specific effects. This led to a wealth of fully abstract models, rewarded in 2017 by the Alonzo Church Award (from the ACM SIGLOG, the EATCS, the EACSL, and the Kurt Gödel Society). To cite the announcement:

> "Game semantics has changed the landscape of programming language semantics by giving a unified view of the denotational universes of many different languages. This is a remarkable achievement that was not previously thought to be within reach."

But are games models truly “unified”? For *deterministic sequential* programs, absolutely: various degrees of control and state are indeed captured as additional conditions on one single canvas [AM99a] – this is the *semantic cube* or *Abramsky cube*. But beyond the sequential deterministic world, the picture is not so clear. The classic fully abstract models for *finite non-determinism* [HM99], for *probabilistic choice* [DH00] or for *parallelism* [GM08] all rely on the presence of state. Until recently, there were no fully abstract model for any of these *without state* – or in the language of game semantics, there were no notions of non-deterministic, probabilistic or parallel *innocence*. Following the phrasing of the title, our understanding of these effects was *entangled* with state.

However, this picture is currently shifting. Recently, two notions of non-deterministic innocence were proposed independently [CCW14, TO15] – the two settings also handling probabilistic innocence [TO14, CCPW18]. Technically, these settings differ significantly. But conceptually, both enrich strategies with explicit *branching* information. Though the novelty may seem minor, this is in fact a major schism with respect to traditional game semantics, in that this branching information is typically not observable. So instead of a strategy being merely a formal description of how a program is observed by a certain type of contexts, the model starts to carry more intensional, *causal* information, typically inaccessible to the environment but which nonetheless finds its use in capturing compositionally the computational behaviour expressible by certain programming features. This suggests that to disentangle parallelism and state, we must adequately represent the *branching structure* of parallel computation, the (non-observable) causal patterns of pure parallel programs.
Enter *concurrent games*. Concurrent games are a family of game semantics models questioning in various ways the premise that the basic building block should be totally, chronologically ordered *plays*. Pioneered by Melliès and others [AM99b, Mel04, MM07, FP09], they have lately been under intense development, prompted by new definitions due to Rideau and Winskel [RW11]. The name comes from their relationship with the so-called *true concurrency* approach to concurrency theory, following which one represents causal dependence and independence of events explicitely rather than resorting to interleavings. Besides making concurrent games a natural target to model concurrent languages and process calculi [CC16, CY19], it provides us with the required causal description of programs.

**Contributions.** We *disentangle* parallelism and state – or rather parallelism and *interfere*nce, which we intend to also encompass semaphores. More precisely, we provide a fully abstract model of Idealized Parallel Algol ($IA_//$), the paradigmatic language used in the game semantics literature to study shared memory concurrency on top of a higher-order language. Our model is a causal version of that of Ghica and Murawski [GM08], which additionally supports compositional conditions of *parallel innocence* and *sequentiality* respectively eliminating interference and parallelism. Accordingly the paper presents *four* full abstraction results, following all combinations of parallelism and interference on top of the pure language PCF. Thus this is a *semantic square* [AM99a], the first such result pushing Abramsky’s programme beyond the sequential deterministic world.

Of the four full abstraction results glued together, three are classics: Hyland and Ong’s full abstraction for PCF [HO00], Abramsky and McCusker’s full abstraction for Idealized Algol (IA) [AM96], and Ghica and Murawski’s full abstraction for $IA_//$ [GM08]. The fourth result is a variation of the full abstraction for PCF with respect to parallel evaluation initially presented in conference format in [CCW15] – in particular, the notion of parallel innocence comes from there<fnref n="2" /> and was developed as part as the first author’s PhD thesis [Cas17].

These four results [HO00, AM96, GM08, CCW15] vary significantly in their technical underpinnings. For the purposes of this paper, this left us with the task, more challenging than anticipated, of providing the *glue*. Accordingly, a significant part of the paper revisits the results of [HO00] and [AJM00] in a language closer to concurrent games, mixing ideas from HO [HO00], AJM [AJM00] and *asynchronous* [Mel05] games. In doing so we hope that this paper, gathering in a single framework several important developments of the field, could also serve as a modern entry point to game semantics. Accordingly we wrote it with the newcomer in mind, not assuming prior knowledge on game semantics. The development is self-contained, with however a number of details postponed to the appendix. In the development, we also take the time to show how our model relates to other game semantics frameworks, hopefully conveying some panoramic perspective on the field. More generally, we made an important effort in staying as pedagogical as possible. This of course, has a cost in that the paper is intimidatingly lengthy; and we hope the readers will excuse us for that.

**Outline.** In Section 1, we start by describing $IA_//$ and its fragments. In Section 2, we introduce our version of alternating games, its interpretation of PCF, and link with more traditional game semantics. In Section 3, we show how (the absence of) control and state may be captured via conditions of strategies – we present *Abramsky’s cube* and some of its

<footnote n="2">²The paper [CCW15] had two main contributions: a new games model called *thin concurrent games*, and *parallel innocence*. The detailed construction of the former appears in [CCW19], but not parallel innocence. The present paper provides, among other things, detailed proofs for the second contribution of [CCW15].</footnote>
consequences. In Section 4, we present our causal fully abstract model for IA$_{‖}$, based on thin concurrent games. In Section 5 we develop one of the key contributions of this paper, parallel innocence: we leverage the causal description of programs offered by thin concurrent games to characterize the causal shapes definable with pure parallel higher-order programs. In Section 6, we study the sequential fragment of our causal games model, and by linking it with the sequential model of Sections 2 and 3 we show full abstraction results for IA and PCF. Finally, in Section 7 we prove our last full abstraction result, for PCF$_{‖}$.

# 1. IA$_{‖}$ AND ITS FRAGMENTS

Idealized Parallel Algol (IA$_{‖}$) is a higher-order, simply-typed, call-by-name concurrent language with shared memory and semaphores. We also introduce fragments:

PCF$_{‖}$ is the fragment without interference,

IA is the fragment without parallelism, and

PCF has neither interference nor parallelism.

## 1.1. Types. The types of IA$_{‖}$ are the following, highlighting types relative to interference.

$$ A, B ::= \begin{array}{l} U \mid \mathbb{B} \mid \mathbb{N} \mid A \to B \quad \text{PCF} \\ \mid \text{ref} \mid \text{sem} \quad +\text{interference} \end{array} $$

Above, $U$ is a unit type with only one value, and $\mathbb{B}$ and $\mathbb{N}$ are types for booleans and natural numbers. In the presence of interference, **ref** is a type for references storing natural numbers, while **sem** is for semaphores. We refer to $U, \mathbb{B}$ and $\mathbb{N}$ as ground types, and use $X, Y$ to range over those. Let us now give the term constructions and typing rules.

## 1.2. Terms and Typing. We define the terms of the language directly via typing rules.

**Contexts** are lists $x_1 : A_1, \dots, x_n : A_n$. **Typing judgments** have the form $\Gamma \vdash M : A$ with $\Gamma$ a context and $A$ a type. In addition to Figure 1, we consider present an explicit exchange rule allowing us to permute the order of variable declarations in contexts. The eliminator rules for basic datatypes are restricted to eliminate only to ground types – general eliminators are defined as syntactic sugar: e.g. a conditional to **ref** may be obtained as

$$ \frac{\Gamma \vdash M : \mathbb{B} \quad \Gamma \vdash N_1 : \mathbf{ref} \quad \Gamma \vdash N_2 : \mathbf{ref}}{\Gamma \vdash \mathbf{mkvar} (\lambda x. \mathbf{if} M (N_1:=x) (N_2:=x)) (\mathbf{if} M !N_1 !N_2) : \mathbf{ref}} $$

The **bad variable** and **bad semaphore** constructs **mkvar** and **mksem** are a common occurrence in the game semantical literature. While a “good” reference is tied to a memory location, many game models also comprise so-called “bad variables” inhabiting **ref** but not behaving as actual variables. Full abstraction results in the concerned games models [AM96, GM08] require a corresponding syntactic construct **mkvar** allowing one to form bad variables by appending arbitrary read and write methods. The same holds for semaphores.

## 1.3. Further syntactic sugar. First of all, for any type $A$ there is a divergence $\vdash \perp_A : A$, any looping program. Given $\Gamma \vdash M, N : U$, an equality test $\Gamma \vdash M =_U N : \mathbb{B}$ may be defined as $M; N$; **tt**. Likewise, for $\Gamma \vdash M, N : \mathbb{B}$ we define $\Gamma \vdash M =_\mathbb{B} N : \mathbb{B}$ as if $MN$ (if $N \mathbf{ff} \mathbf{tt}$), and $\Gamma \vdash M =_N N : \mathbb{B}$ similarly, with the obvious recursive program.
PCF

$\Gamma \vdash \mathbf{skip} : \mathbb{U}$

$\Gamma \vdash \mathbf{tt} : \mathbb{B}$

$\Gamma \vdash \mathbf{ff} : \mathbb{B}$

$\Gamma \vdash n : \mathbb{N}$

$\Gamma, x : A \vdash x : A$

$\Gamma, x : A \vdash M : B$
$\Gamma \vdash \lambda x^A . M : A \to B$

$\Gamma \vdash M : A \to B$

$\Gamma \vdash N : A$

$\Gamma \vdash M : \mathbb{U}$

$\Gamma \vdash N : \mathbb{X}$

$\Gamma \vdash M ; N : \mathbb{X}$

$\Gamma \vdash M : \mathbb{B}$

$\Gamma \vdash N_1 : \mathbb{X}$

$\Gamma \vdash N_2 : \mathbb{X}$

$\Gamma \vdash M : \mathbb{N}$

$\Gamma \vdash \mathbf{if} M N_1 N_2 : \mathbb{X}$

$\Gamma \vdash \mathbf{succ} M : \mathbb{N}$

$\Gamma \vdash \mathbf{pred} M : \mathbb{N}$

$\Gamma \vdash M : \mathbb{N}$
$\Gamma \vdash \mathbf{iszero} M : \mathbb{B}$

$\Gamma, x : \mathbb{X} \vdash M : \mathbb{Y}$

$\Gamma \vdash N : \mathbb{X}$

$\Gamma \vdash M : A \to A$

$\Gamma \vdash \mathbf{let} x = N \mathbf{in} M : \mathbb{Y}$

$\Gamma \vdash \mathcal{Y} M : A$

+interference

$\Gamma, x : \mathbf{ref} \vdash M : \mathbb{X}$
$\Gamma \vdash \mathbf{newref} x := n \mathbf{in} M : \mathbb{X}$

$\Gamma \vdash M : \mathbf{ref}$
$\Gamma \vdash N : \mathbb{N}$
$\Gamma \vdash M := N : \mathbb{U}$

$\Gamma \vdash M : \mathbf{ref}$
$\Gamma \vdash ! M : \mathbb{N}$

$\Gamma, x : \mathbf{sem} \vdash M : \mathbb{X}$
$\Gamma \vdash \mathbf{newsem} x := n \mathbf{in} M : \mathbb{X}$

$\Gamma \vdash M : \mathbf{sem}$
$\Gamma \vdash \mathbf{grab} M : \mathbb{U}$

$\Gamma \vdash N : \mathbf{sem}$
$\Gamma \vdash \mathbf{release} N : \mathbb{U}$

$\Gamma \vdash M : \mathbb{N} \to \mathbb{U}$
$\Gamma \vdash N : \mathbb{N}$
$\Gamma \vdash \mathbf{mkvar} M N : \mathbf{ref}$

$\Gamma \vdash M : \mathbb{U}$
$\Gamma \vdash N : \mathbb{U}$
$\Gamma \vdash \mathbf{mksem} M N : \mathbf{sem}$

+parallelism

$\Gamma, x_1 : \mathbb{X}, x_2 : \mathbb{X} \vdash M : \mathbb{Y}$
$\Gamma \vdash N_1 : \mathbb{X}$
$\Gamma \vdash N_2 : \mathbb{X}$
$\Gamma \vdash \mathbf{let} \left( \begin{array}{l} x_1 = N_1 \\ x_2 = N_2 \end{array} \right) \mathbf{in} M : \mathbb{Y}$

<caption>Figure 1: Typing rules for $\Gamma A_\parallel$</caption>

We refer to constants of ground type as **values**; we use $v$ to range over those, and $n, b$ or $c$ to range over values of respective types $\mathbb{N}, \mathbb{B}$ or $\mathbb{U}$. We introduce a $n$-ary case construct branching on all values of ground types. By abuse of notation, we write $V \subseteq_f \mathbb{X}$ for any finite subset of the values of ground type $\mathbb{X}$. Writing $V = \{v_1, \dots, v_n\}$, we set

case $M$ of
$v_1 \mapsto N_1$
$v_2 \mapsto N_2$
$\dots$
$v_n \mapsto N_n$

$\mathbf{def}$
$\equiv$

let $x = M$ in
\qquad if $x = \mathbb{X} \ v_1$ then $N_1$
\qquad else if $x = \mathbb{X} \ v_2$ then $N_2$
\qquad \dots
\qquad else if $x = \mathbb{X} \ v_n$ then $N_n$
\qquad else $\perp$

of type $\mathbb{Y}$ in context $\Gamma$ if $\Gamma \vdash M : \mathbb{X}$ and $\Gamma \vdash N_i : \mathbb{Y}$ for all $1 \le i \le n$.

The **let** construct is crucial in this paper: as we shall see later on, strategies may evaluate a variable *once*, and provide a different continuation for each possible value. This behaviour cannot be replicated strictly without **let**, see Section 3.3.1 for a more detailed discussion.
1.4. **Operational semantics.** We give a small-step operational semantics, following [GM08]. We fix a countable set $\mathcal{L}$ of memory locations. A store is a partial map $s: \mathcal{L} \to \mathbb{N}$ with finite domain where $\mathbb{N}$ stands, overloading notations, for natural numbers. Configurations of the operational semantics are tuples $\langle M, s \rangle$ where $s$ is a store with $\text{dom}(s) = \{\ell_1, \dots, \ell_n\}$ and $\Sigma \vdash M : A$ with $\Sigma = \ell_1 : \text{ref}, \dots, \ell_i : \text{ref}, \ell_{i+1} : \text{sem}, \dots, \ell_n : \text{sem}$.

Reduction rules have the form $\langle M, s \rangle \rightsquigarrow \langle M', s' \rangle$ where $\text{dom}(s) = \text{dom}(s')$; we write $\rightsquigarrow^*$ for the reflexive transitive closure. If $\vdash M : \mathbb{X}$, we write $M \downarrow$ if $\langle M, \emptyset \rangle \rightsquigarrow^* \langle v, \emptyset \rangle$ for some value $v$. We give in Figure 2 the reduction rules – there and from now on in the paper we use the notation $\oplus$ to denote the usual set-theoretic union, when it is known disjoint. For rules which do not interact with the state, we omit the state component – it is simply left unchanged by stateless basic reductions, and propagated upwards by stateless context rules.

1.5. **Fragment languages.** Besides PCF, we consider three main languages of interest:

$$ \text{PCF}_{\parallel} = \text{PCF} + \text{parallelism} $$

$$ \text{IA} = \text{PCF} + \text{interference} $$

$$ \text{IA}_{\parallel} = \text{PCF} + \text{interference} + \text{parallelism} $$

IA is a variant of *Idealized Algol with active expressions* [AM96], differing only in that it has semaphores. This is not a significant difference, as semaphores are definable from state in a sequential language. Likewise, $IA_{\parallel}$ is close to the language of [GM08]: it differs only in that the parallelism operation is more general. For $\Gamma \vdash M : \mathbb{U}$ and $\Gamma \vdash N : \mathbb{U}$ we may define their parallel composition $\Gamma \vdash M \parallel N : \mathbb{U}$ (as in [GM08]) by

$$ M \parallel N = \text{let} \left( \begin{array}{l} x = M \\ y = N \end{array} \right) \text{ in skip.} $$

Conversely, for e.g. $\Gamma \vdash N_1 : \mathbb{N}$, $\Gamma \vdash N_2 : \mathbb{N}$ and $\Gamma, x_1 : \mathbb{N}, x_2 : \mathbb{N} \vdash M : A$, the present parallel let construction is definable via state and parallel composition of commands:

$$ \text{let} \left( \begin{array}{l} x_1 = N_1 \\ x_2 = N_2 \end{array} \right) \text{ in } M = \begin{array}{l} \text{newref } v_1 := 0 \text{ in} \\ \text{newref } v_2 := 0 \text{ in } (v_1 := N_1 \parallel v_2 := N_2); M[!v_1/x_1, !v_2/x_2] \end{array} $$

1.6. **Observational Equivalence and Full Abstraction.** Here, $\mathcal{L}$ may refer to any of the fragments above. A $\mathcal{L}$-context for the judgment $\Gamma \vdash A$ is a term $C[]$ of $\mathcal{L}$ with a hole, s.t. for any $\Gamma \vdash M : A$ in $\mathcal{L}$ we have $\vdash C[M] : \mathbb{U}$ obtained by replacing the hole with $M$. Two terms $\Gamma \vdash M, N : A$ of $\mathcal{L}$ are $\mathcal{L}$-observationally equivalent iff

$$ M \sim_{\mathcal{L}} N \quad \Leftrightarrow \quad \text{for all } C[] \text{ a } \mathcal{L}\text{-context for } \Gamma \vdash A, \quad (C[M] \Downarrow \Leftrightarrow C[N] \Downarrow) $$

We omit $\mathcal{L}$ when it is clear from the context. Observational equivalence is usually regarded as the canonical equivalence on programs: $\mathcal{L}$-observationally equivalent programs are intercheangible as long as the evaluation context is in $\mathcal{L}$. Accordingly, denotational semantics often aims to capture observational equivalence. An interpretation of programs $\llbracket - \rrbracket$ into some mathematical universe is called **fully abstract** whenever

$$ M \sim N \quad \Leftrightarrow \quad \llbracket M \rrbracket = \llbracket N \rrbracket $$

for all $\Gamma \vdash M, N : A$. Full abstraction is a gold standard in denotational semantics, as it captures the best possible match between a language and its semantics, ensuring that the denotational semantics is complete for proving equivalence between programs.
<figure><img src="image_3.png" /></figure>

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

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

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

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

<figure><img src="image_8.png" /><figcaption>Figure 2: Operational semantics of IA$_{✓}$</figcaption></figure>
<figure><img src="image_9.png" /><figcaption>Figure 3: An affine arena</figcaption></figure>

<figure><img src="image_10.png" /><figcaption>Figure 4: $U \to (U \otimes U)$</figcaption></figure>

<figure><img src="image_11.png" /><figcaption>Figure 5: An alternating play</figcaption></figure>

## 2. GAME SEMANTICS FOR PCF

2.1. **Games and Strategies.** We present first a game semantics of PCF. Though it is sequential, our presentation is non-standard, somewhat mixing features of AJM [AJM00], HO [HO00] and asynchronous games [Mel05] – this is to facilitate the interplay between all the games models involved. We skip a number of details, found in Appendix B.

Game semantics presents higher-order computation as an exchange of tokens between two players, called “Player” and “Opponent”. *Player* stands for the program under evaluation – events/moves attributed to Player are observable computational events resulting from its execution: calls to variables, program phrases converging to a value. *Opponent* stands for the execution environment. Their interaction follows rules depending on the type of the program under scrutiny. In setting up a game semantics the first step is to extract from the type a structure, called a *game* or an *arena*, which presents all the observable computational events available when interacting on this type, along with their respective causal dependencies.

2.1.1. *Affine arenas.* We first introduce our representation of types as games in the *affine* case, i.e. if any computational event can appear at most once – this is merely to first help the reader build up intuition before handling replication.

Consider $(U \to U) \to B$, where *affineness* implies that each argument may be called at most once. Once a call-by-name execution on that type is initiated, the available observable events are the following: (1) the term may directly converge to **tt** or **ff**, without evaluating its argument; (2) it may call its argument (i.e. it evaluates to $\lambda f^{U \to U}. M$ with *M* having *f* in head position). In the case (2) the control goes back to the environment, which plays for *f*: it may prompt *f* to return the unique value **skip**, or to itself call its argument. Finally, if *f* calls its argument, the corresponding sub-term may reduce to a value.

Overall, these events along with their causal dependencies give rise to the diagram in Figure 3. It is read from top to bottom, with the dashed lines representing the dependency relation. Nodes are called *moves* or *events*, and are labeled with a polarity, – for events due to the environment, and + for events due to the program. Finally, the wiggly line between **tt**<sup>+</sup> and **ff**<sup>+</sup> indicates *conflict*: it represents the fact that only one of these two values may be observed in one execution, whereas all the other pairs of events could conceivably appear together. The reader may convince themselves that indeed, the diagram does represent the observable events in a call-by-name evaluation of $(U \to U) \to B$ as outlined in the previous paragraph. We insist that those are the computational events that are *observable* in the interface with the environment: the program may perform internal computation; a program
<figure><img src="image_12.png" /><figcaption>Figure 6: $\mathbb{U}$</figcaption></figure>

<figure><img src="image_13.png" /><figcaption>Figure 7: $\mathbb{B}$</figcaption></figure>

<figure><img src="image_14.png" /><figcaption>Figure 8: $\mathbb{N}$</figcaption></figure>

<figure><img src="image_15.png" /><figcaption>Figure 9: $!\mathbb{U}$</figcaption></figure>

in an extension of PCF with state could possibly store and read values from a local variable, etc. But those are not observable by a context, thus are not represented in the arena.

To formalize the arena as a mathematical structure, we use *event structures*<fnref n="3" />:

**Definition 2.1.** An **event structure** (es) is a triple $E = (|E|, \leq_E, \#_E)$, where $|E|$ is a (countable) set of **events**, $\leq_E$ is a partial order called **causal dependency** and $\#_E$ is an irreflexive symmetric binary relation on $|E|$ called **conflict**, satisfying:

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

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

An **event structure with polarities** (esp) is an event structure $A$ together with a function $\text{pol}_A: |A| \to \{-, +\}$ assigning to each event a *polarity*.

Figure 3 displays an esp. The wiggly line indicates conflict, but we will not put wiggly lines between all conflicting pairs of events, as long as missing conflicts may be deduced by *conflict inheritance*. A conflict that cannot be deduced by inheriting an earlier conflict is called a **minimal conflict**. As with Figure 3, we will represent types as esps. In fact, the event structures arising via the interpretation of types have a very restricted form. In the definition below, we use the notation $e \rightarrow_E e'$ in an event structure $E$ to mean **immediate causality**, i.e. $e <_E e'$ with no other event strictly in between.

**Definition 2.2.** An **arena** is an esp $(A, \leq_A, \#_A, \text{pol}_A)$ satisfying:

*alternating:* if $a_1 \rightarrow_A a_2$, $\text{pol}_A(a_1) \neq \text{pol}_A(a_2)$,

*forestial:* if $a_1 \leq_A a$ and $a_2 \leq_A a$, then $a_1 \leq_A a_2$ or $a_2 \leq_A a_1$,

*race-free:* if $a_1, a_2 \in |A|$ are in minimal conflict, then $\text{pol}_A(a_1) = \text{pol}_A(a_2)$.

Besides, a **--arena** additionally satisfies the condition:

*negative:* if $a \in \min(A)$, then $\text{pol}_A(a) = -$,

where $\min(A)$ stands for the set of minimal events of $A$.

Types will only yield **--arenas**, but throughout the paper we will use the general case. Finally, though we motivated Definition 2.1 with arenas, event structures will have other uses. Notably, from Section 4 onwards, strategies will also be event structures.

2.1.2. *Basic Constructions.* We give a few basic constructions on event structures and arenas which will allow us to construct in a systematic way, from any type of PCF, a **--arena**.

We give **--arenas** for the ground types of PCF, in Figures 6, 7 and 8, using the same notations $\mathbb{U}, \mathbb{B}$ and $\mathbb{N}$ for the arenas as for the types. For $\mathbb{N}$, even though the picture only shows conflict between neighbours, all positive events are meant to be in pairwise conflict.

<footnote n="3">³More precisely, those are *prime event structures with binary conflict*.</footnote>
We write **1** for the **empty es**, with no event. If A is an esp, we write $A^{\perp}$ for its **dual**, the esp with same events, causality and conflict, but the opposite polarities, i.e. $\text{pol}_{A^{\perp}}(a) = -\text{pol}_A(a)$ for all $a \in |A|$. The simple parallel composition is defined as follows.

**Definition 2.3.** If $E_1, E_2$ are two es, their **simple parallel composition** $E_1 \parallel E_2$ has

$$
\begin{array}{lll}
\text{events:} & |E_1||E_2| = \{1\} \times |E_1| \uplus \{2\} \times |E_2| & \\
\text{causality:} & (i, e) \leq_{E_1||E_2} (j, e') \Leftrightarrow i = j \ \& \ e \leq_{E_i} e' & \\
\text{conflict:} & (i, e) \#_{E_1||E_2} (j, e') \Leftrightarrow i = j \ \& \ e \ \#_{E_i} e' . &
\end{array}
$$

Moreover, if $E_1$ and $E_2$ have polarities (i.e. are esp), then $E_1 \parallel E_2$ also has polarities, defined as $\text{pol}_{E_1||E_2}(1, e) = \text{pol}_{E_1}(e)$ and $\text{pol}_{E_1||E_2}(2, e) = \text{pol}_{E_2}(e)$.

By extension, we often write $X \parallel Y$ for the tagged disjoint union $(\{1\} \times X) \uplus (\{2\} \times Y)$ of two sets $X$ and $Y$. In the simple parallel composition of arenas $A$ and $B$, the two are side by side with no interaction. The arena $A \parallel B$ adequately represents a tensor type $A \otimes B$ where the two resources $A$ and $B$ may be accessed in any order – although PCF does not have such a type, this construction will play an important role in the sequel. We also introduce the **product** $A_1 \& A_2$ of $A_1$ and $A_2$ --arenas, defined as for $A_1 \parallel A_2$ with conflict

$$ (i, e) \#_{A_1 \& A_2} (j, e') \Leftrightarrow i \neq j \lor (i = j \land e \#_{A_i} e'), $$

i.e. $A_1$ and $A_2$ are in conflict. The constructions $\parallel$ and $\&$ have obvious n-ary generalizations. We also introduce another construction on arenas, the affine arrow $A \to B$:

**Definition 2.4.** Let $A, B$ be arenas with $B$ **pointed**, i.e. with *exactly one* minimal $b_0 \in |B|$. The **affine arrow** $A \to B$ has the components of $A^{\perp} \parallel B$ except for causality, set as:

$$ \leq_{A \to B} = \leq_{A^{\perp} \parallel B} \cup \{(2, b_0), (1, a) \mid a \in |A|\}. $$

This completes an interpretation of PCF types as pointed --arenas capturing the causal dependency between computational events in an affine evaluation. For instance, on $A \to B$ computation starts in $B$, but as soon as the initial move of $B$ has been played computation in $A$ may start, with polarity reversed. At this point, the reader may verify that indeed, the arena $(\mathbb{U} \to \mathbb{U}) \to \mathbb{B}$ obtained by applying these constructions is indeed the one in Figure 3.

2.1.3. *General arrow.* Definition 2.4 suffices for the types of PCF (which yield pointed arenas). But we aim to show that strategies have the structure of a *Seely category*, a traditional categorical model for Intuitionistic Linear Logic – and that structure includes tensors, which do not preserve pointedness. To generalize $A \to B$ for $B$ non-pointed, it is natural to set one copy of $A$ for each initial move of $B$. More concretely, $A \to B$ has events and polarities

$$ |A \to B| = (\|_{b \in \min(B)} A)^{\perp} \parallel B, $$

where $\min(B)$ is the set of *minimal events* of $B$. The order has $(2, b) \le (2, b')$ iff $b \le B b'$, $(1, (b, a)) \le (1, (b', a'))$ iff $b = b'$ and $a \le A a'$, $(2, b) \le (1, (b', a))$ iff $b = b'$, and $(1, (b, a)) \le (2, b')$ never, exactly matching the arrow arena of HO games [HO00]. But having two copies of $A$ is in tension with affineness, so we use conflict to tame this copying. The construction is illustrated in Figure 4, displaying the arena $\mathbb{U} \to (\mathbb{U} \otimes \mathbb{U})$. There are two copies of the $\mathbb{U}$ on the left, but still, linearity is guaranteed by the addition of conflict.

To define conflict, writing $\chi_{A,B}: |A \to B| \to |A^{\perp} \parallel B|$ for the obvious map, we use:
**Lemma 2.5.** *Consider A and B two --arenas.*

Then, there is a unique $\#_{A \to B}$ making $A \to B$ a --arena such that for all down-closed finite $x \subseteq |A \to B|$, $x \in \mathscr{C}(A \to B)$ iff $\chi_{A,B} x \in \mathscr{C}(A^{\perp} \parallel B)$ with $\chi_{A,B}$ injective on $x$.

*Proof.* See Appendix B.1.1. □

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

**2.1.4.** *Playing on Arenas.* Now we formulate a notion of execution, relying on the fact that event structures support a natural notion of state or position, called configuration.

**Definition 2.6.** A (finite) configuration of es $E$ is a finite set $x \subseteq |E|$ which is

down-closed: $\forall e \in x, \forall e' \in |E|, e' \leqslant_{E} e \implies e' \in x$

consistent: $\forall e, e' \in x, \neg(e \#_{E} e')$.

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

For $x, y \in \mathscr{C}(E)$, we write $x \leftarrow y$ if there is $e \in |E|$ such that $e \notin x$ and $y = x \cup \{e\}$; $\leftarrow$ is the **covering relation**. If $x \leftarrow x \cup \{e\}$, we say that $x$ **enables** $e$ or **extends by** $e$, written $x \vdash_{E} e$. Configurations of an arena represent **valid execution states**. We may now leverage this to define **plays**, which provide a mathematical notion of **execution**.

**Definition 2.7.** An alternating play on arena $A$ is a sequence $s = s_1 \dots s_n$ which is:

valid: $\forall 1 \leqslant i \leqslant n, \{s_1, \dots, s_i\} \in \mathscr{C}(A)$,

non-repetitive: $\forall 1 \leqslant i, j \leqslant n, s_i = s_j \implies i = j$,

alternating: $\forall 1 \leqslant i \leqslant n-1, \text{pol}_A(s_i) \neq \text{pol}_A(s_{i+1})$,

negative: if $n \geqslant 1$, then $\text{pol}_A(s_1) = -$.

We write $\downarrow\uparrow$-Plays($A$) for the set of alternating plays on $A$.

The notation $\downarrow\uparrow$-Plays($A$) means to suggest that an alternating play has two possible states: O if $s$ has even length and the last move (if any) is by Player, and P otherwise: each new move transitions between them. We denote the empty play with $\varepsilon$, and the prefix ordering with $\sqsubseteq$. In the sequel we sometimes apply $\downarrow\uparrow$-Plays($-$) to esp s other than arenas.

Plays record individual executions, by giving a chronological account of events observed throughout computation. For instance, Figure 5 displays a play on the arena $(\mathbb{U} \to \mathbb{U}) \to \mathbb{B}$ of Figure 3. It is also read from top to bottom. Each move corresponds to a node in Figure 3 – as each move in the arena corresponds to a given type component, the identity of each move in Figure 5 is signified by its position under the matching type component.

**2.1.5.** *Strategies.* Given a term of type $A$ we may, given the adequate technical machinery, ask whether a given play describes a valid execution for that term. The play of Figure 5, for instance, describes a valid execution for $\lambda f \mathbb{U} \to \mathbb{U}$. $f \text{skip}$; $\mathbf{tt} : (\mathbb{U} \to \mathbb{U}) \to \mathbb{B}$: after Opponent starts computation, reduction immediately gets stuck with a variable $f$ in head position. This is an observable event, corresponding to Player calling its argument with $\mathbf{q}^+$. Then, Opponent proceeds to call his argument with $\mathbf{q}^-$, triggering the evaluation of the subterm **skip**. This (trivially) converges to a value, which is observable and corresponds to $\checkmark^+$. The control goes back to $f$ (Opponent), which evaluates to **skip** as well via observable $\checkmark^-$. This triggers the evaluation of $\mathbf{tt}$, leading to the observable $\mathbf{tt}^+$ that terminates computation.

Figure 5 represents one possible execution of $\lambda f \mathbb{U} \to \mathbb{U} \ f \text{skip}$; $\mathbf{tt} : (\mathbb{U} \to \mathbb{U}) \to \mathbb{B}$. In general a term is represented by a *strategy*, which aggregates all possible executions.
<figure><img src="image_17.png" /><figcaption>Figure 10: ($\mathbb{U} \to \mathbb{U}) \to \mathbb{B}$ with replication</figcaption></figure>

<caption>Figure 11: A configuration of $!((\mathbb{U} \to \mathbb{U}) \to \mathbb{B})$</caption>

**Definition 2.8.** A alternating strategy $\sigma : A$ on $--$arena $A$ is $\sigma \subseteq \downarrow\uparrow$-Plays($A$) which is:

non-empty: $\varepsilon \in \sigma$

prefix-closed: $\forall s \subseteq s' \in \sigma, s \in \sigma$

deterministic: $\forall sa_1^+, sa_2^+ \in \sigma, a_1 = a_2$

receptive: $\forall s \in \sigma, sa^- \in \downarrow\uparrow$-Plays($A$) $\implies$ $sa \in \sigma$

An alternating prestrategy $\sigma : A$ satisfies all these conditions except for *receptive*.

In this definition we have started using a convention followed throughout this paper: when introducing an event, we sometimes annotate it with a superscript to indicate its polarity. For instance, "$\forall sa_1^+ \in \sigma, \dots$ is a shorthand for $\forall sa_1 \in \sigma$ such that $\text{pol}(a_1) = +, \dots$".

We will see later on how to compute the strategy for a term. It is a strength of game semantics that this may be done either compositionally by induction on the syntax following the methodology of denotational semantics, or operationally via an abstract machine [GT12].

**2.2. Replication and symmetry.** In this paper we introduce early on the machinery for replication. It requires a small jump in abstraction, but fixes the arenas once and for all.

**2.2.1. Arenas with symmetry.** Figure 3 displays the arena corresponding to affine executions<fnref n="4" /> on type $(\mathbb{U} \to \mathbb{U}) \to \mathbb{B}$. To go beyond affineness, we *expand* the arena to allow multiple calls to arguments – for $(\mathbb{U} \to \mathbb{U}) \to \mathbb{B}$, we obtain an infinite arena as drawn in Figure 10.

In the picture, it seems like *e.g.* all moves $\mathbf{q}^+$ are interchangeable. This is true in spirit but every move must be a distinct event of the arena. Concretely, the expanded arena is computed following the methodology of linear logic: the type $(\mathbb{U} \to \mathbb{U}) \to \mathbb{B}$ is represented by $!((\mathbb{U} \to \mathbb{U}) \to \mathbb{B})$ rather than $(\mathbb{U} \to \mathbb{U}) \to \mathbb{B}$. Here, ! is an *exponential modality* in the sense of linear logic. The full definition of !A will appear in Definition 2.10, but its events are $|!A| = \mathbb{N} \times |A|$, pairs $(n, a)$ where n is called a *copy index*. So in reality, a precise picture of the arena for $(\mathbb{U} \to \mathbb{U}) \to \mathbb{B}$ with replication would be a version of Figure 10 where some events are tagged by *copy index* – see Figure 11 for an example of a configuration of $!((\mathbb{U} \to \mathbb{U}) \to \mathbb{B})$ with explicit indices pictured as grey subscripts.

Expanding the arena so opens up the way to replication without compromising the *non-repetitive* condition: a strategy may replay the “same” move but with different copy indices. But then, it is necessary to identify strategies behaving in the same way save for

<footnote n="4">⁴Affineness is enforced by *non-repetitive* in Definition 2.7. Rather than expand arenas, it is tempting to simply lift it. For this to be sound, it becomes then necessary to include additional structure in plays: the *justification pointers*. This is the choice made in *HO games* [HO00]. This will be detailed in Section 2.4.</footnote>
the choice of copy indices. To that end, following the approach initiated in [CCW14] we enrich arenas with a notion of symmetry, capturing reindexings between configurations.

**Definition 2.9.** An isomorphism family on event structure E is a set $\mathcal{S}(E)$ of bijections between configurations of E, satisfying the additional conditions:

*groupoid:* $\mathcal{S}(E)$ contains identity bijections; is closed under composition and inverse.

*restriction:* for all $\theta: x \simeq y \in \mathcal{S}(E)$ and $x \supseteq x' \in \mathcal{C}(E)$, there is a (necessarily) unique $\theta' \supseteq \theta' \in \mathcal{S}(E)$ such that $\theta' : x' \simeq y'$.

*extension:* for all $\theta: x \simeq y \in \mathcal{S}(E)$, $x \subseteq x' \in \mathcal{C}(E)$, there is a (not necessarily unique) $\theta \subseteq \theta' \in \mathcal{S}(E)$ such that $\theta' : x' \simeq y'$.

Then $(E, \mathcal{S}(E))$ is an **event structure with symmetry (ess)**. If A has polarities preserved by $\mathcal{S}(A)$, A is an **event structure with symmetry and polarities (essp)**.

If A is an ess, we refer to the elements of $\mathcal{S}(A)$ as **symmetries**. We write $\theta: x \cong_A y$ to mean that $\theta: x \simeq y$ is a bijection such that $\theta \in \mathcal{S}(A)$, and write $x = \text{dom}(\theta)$ and $y = \text{cod}(\theta)$. It is an easy exercise to prove that symmetries are automatically order-isomorphisms [Win07], where configurations inherit a partially ordered structure from the causal dependency of A. We regard isomorphism families as *proof-relevant* equivalence relations: they convey the information of which configurations are interchangeable, witnessed by an explicit bijection.

From now on, **arenas** have an isomorphism family. It comprises only identity symmetries on basic arenas $U, B, N$ and **1**. The previous constructions on arenas extend transparently: $A^{\perp}$ has the same symmetries as A. The symmetries on $A \parallel B$ are those of the form

$$ \theta_A \parallel \theta_B : \begin{array}{ccc} x_A \parallel x_B & \cong & y_A \parallel y_B \\ (1, a) & \mapsto & (1, \theta_A(a)) \\ (2, b) & \mapsto & (2, \theta_B(b)) \end{array} $$

for $\theta_A: x_A \cong_A y_A$ and $\theta_B: x_B \cong_B y_B$. Those on $A \& B$ are the symmetries on $A \parallel B$ that are bijections between configurations of $A \& B$, i.e. one of $\theta_A$ and $\theta_B$ must be empty. Note that these constructions $\parallel$ and $\&$ apply to arbitrary event structures with symmetry.

For $A \to B$, if $x, y \in \mathcal{C}(A \to B)$ and $\theta: x \simeq y$ is any bijection, defining first $\chi_{A,B} \theta$ as

$$ \chi_{A,B} x \stackrel{\chi_{A,B}^{-1}}{\cong} x \stackrel{\theta}{\cong} y \stackrel{\chi_{A,B}}{\cong} \chi_{A,B} y, $$

we set $\theta: x \cong_{A \to B} y$ when $\theta$ is an order-isomorphism satisfying $\chi_{A,B} \theta: \chi_{A,B} x \cong_{A \parallel B} \chi_{A,B} y$.

The main arena construction introducing new symmetric events is the **exponential**:

**Definition 2.10.** Let A be a --arena. The --arena !A has components

$$ \begin{array}{lll} \textit{events:} & |!A| = \mathbb{N} \times |A| & \\ \textit{causality:} & (i, a) \leq!_A (j, a') & \Leftrightarrow i = j \ \& \ a \leq_A a' \\ \textit{conflict:} & (i, a) \ #!_A (j, a') & \Leftrightarrow i = j \ \& \ a \ #_A a' \\ \textit{polarities:} & \text{pol}_!A(i, a) = \text{pol}_A(a) & \end{array} $$

along with isomorphism family comprising as symmetries those bijections of the form

$$ \theta : \begin{array}{ccc} \parallel_{n \in \mathbb{N}} x_n & \cong & \parallel_{n \in \mathbb{N}} y_n \\ (n, a) & \mapsto & (\pi(n), \theta_n a) \end{array} $$

for some permutation $\pi \in \zeta(\mathbb{N})$ and some family $(\theta_n)_{n \in \mathbb{N}}$ with $\theta_n: x_n \cong_A y_\pi(n)$ for all $n \in \mathbb{N}$.
This definition applies in general to any ess. Figure 9 shows the plain esp of !U with copy indices indicated as grey subscripts – its symmetries are all order-isomorphisms between configurations. While !(-) does not match a type construction of PCF, we shall follow Girard [Gir87] and define the arrow type of arenas with replication as $A \to B = !A \dashv B$.

### 2.2.2. Symmetry on plays and strategies.
Symmetry will allow us to identify strategies, but it should also affect how strategies play. In the presence of explicit copy indices, a fundamental property is uniformity. Intuitively, a strategy is uniform if its behaviour does not depend (up to symmetry) on the specific copy indices used by its environment.

The first step towards uniformity is to transport symmetry to plays.

**Definition 2.11.** Let A be an arena and $s, t \in \text{↓↑-Plays}(A)$. We say that $s$ and $t$ are symmetric, written $s \cong_A t$, if $s$ and $t$ have the same length, and we have

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

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

Those readers familiar with AJM games may find comfort in the following fact.

**Fact 2.12.** For an arena A, the tuple $\langle |A|, \text{pol}_A, \text{↓↑-Plays}(A), \cong_A \rangle$ is an AJM game [AJM00].

This ignores the Question/Answer labeling in AJM games, which we shall handle later on. The proof is a straightforward exercise. For the experts, we mention that this association of arenas to AJM games does not respect the arena constructions because constructions on AJM games enforce local alternation, while $\text{↓↑-Plays}(-)$ does not. As in HO games [HO00], in our presentation local alternation will only follow from the P-visibility condition.

From the connection with AJM games it seems natural to import the AJM uniformity:

**Definition 2.13.** For A an arena and $\sigma, \tau : A$ alternating prestrategies, we write $\sigma \approx \tau$ iff:

- simulation: $\forall sa^+ \in \sigma, t \in \tau, s \cong_A t \implies \exists b^+, tb^+ \in \tau \ \& \ sa^+ \cong_A tb^+$

- receptive: $\forall s \in \sigma, tb^+ \in \tau, s \cong_A t \implies \exists a^+, sa^+ \in \sigma \ \& \ sa^+ \cong_A tb^+$

- simulation: $\forall sa^- \in \sigma, t \in \tau, sa^- \cong_A tb^- \implies tb^- \in \tau$

- receptive: $\forall s \in \sigma, tb^- \in \tau, sa^- \cong_A tb^- \implies sa^- \in \sigma$

This defines a per $\approx$ on prestrategies<fnref n="5" /> on A. A prestrategy $\sigma : A$ is uniform iff $\sigma \approx \sigma$.

Uniformity is crucial. For the interpretation to respect $\beta$-equivalence we must identify strategies that play the “same moves”, but with different copy indices. For instance, we must consider equal the two strategies $\tau_0, \tau_1 : U \to U$ with unique maximal play:

$$ \tau_0 : \quad !U \dashv U \qquad \begin{array}{c} \mathbf{q}^- \\ \mathbf{q}_0^+ \\ \checkmark_0^- \end{array} $$

$$ \tau_1 : \quad !U \dashv U \qquad \begin{array}{c} \mathbf{q}^- \\ \mathbf{q}_1^+ \\ \checkmark_1^- \end{array} $$

But this quotient is risky. Let us apply both $\tau_0$ and $\tau_1$ to $\sigma : !U$ with only maximal play $\mathbf{q}_0^- \checkmark_0^+$. Though we have yet to define composition, the application of $\tau_0$ to $\sigma$ must converge, while that of $\tau_1$ to $\sigma$ must diverge. So $\tau_0$ and $\tau_1$ cannot be safely identified as

<footnote n="5">⁵For strategies, $\to$, $\leftarrow$-receptive are subsumed by receptive. But these are necessary for uniformity to apply to prestrategies which might not be receptive – this generalization will be used in the technical development.</footnote>
they are distinguishable. In fact here, the culprit is $\sigma$: it is not uniform. Since $\mathbf{q}_0^- \vee_0^+ \in \sigma$, uniformity of $\sigma$ would imply that $\mathbf{q}_1^- \vee_1^+ \in \sigma$ as well, breaking the counter-example.

From now on, all **alternating (pre)strategies** are assumed uniform.

## 2.3. Interpretation of PCF.
The interpretation follows the methodology of denotational semantics, resting on the fact that arenas and strategies form a category with adequate structure. In the main text we only outline this fairly routine construction – though this should be enough to read the paper – but the construction is detailed in Appendix B.

### 2.3.1. Category.
The category $\downarrow\uparrow$-Strat has objects $\to$-arenas, and morphisms the alternating strategies (strategies for short) on $A \to B$. The composition of $\sigma: A \to B$ and $\tau: B \to C$

$$ \tau \odot \sigma : A \to C $$

follows the usual game semantics process of parallel interaction followed by hiding.

First, the **pre-interactions** are sequences $u \in |(A \to B) \to C|^*$ satisfying valid of Definition 2.7. A pre-interaction $u$ has three **restrictions**, with the following types:

$$ u \uparrow A, B \in |A \to B|^*, \quad u \uparrow B, C \in |B \to C|^*, \quad u \uparrow A, C \in |A \to C|^* $$

defined in the obvious way – see Appendix B.1.2. Given prestrategies $\sigma: A \to B$ and $\tau: B \to C$, an **interaction** $u \in \tau \circledast \sigma$ is a pre-interaction $u \in |(A \to B) \to C|^*$ satisfying:

$$ u \uparrow A, B \in \sigma, \quad u \uparrow B, C \in \tau, \quad u \uparrow A, C \in \downarrow\uparrow\text{-Plays}(A \to C). $$

The **composition** of $\sigma$ and $\tau$ comprises all $s \in \downarrow\uparrow\text{-Plays}(A \to C)$ with a **witness**:

$$ \tau \odot \sigma = \{u \uparrow A, C \mid u \in \tau \circledast \sigma\}; $$

it follows that $\tau \odot \sigma: A \to C$ is a prestrategy; and a strategy if $\sigma$ and $\tau$ are.

Composition is associative on prestrategies, but admits identities only for strategies: the **copycat** strategies. If $A$ is a $\to$-arena and $s \in |A \to A|$, there are left and right restrictions

$$ s \uparrow l \in |A|^*, \quad s \uparrow r \in |A|^* $$

defined in the obvious way (see Appendix B.1.4). For $s \in \downarrow\uparrow\text{-Plays}(A \to A)$, $s$ is a copycat play iff (1) for all even-length prefix $s' \subseteq s$ we have $s' \uparrow l = s' \uparrow r$, and (2) for all $(1, (a_1, a_2)) \in |s|$, if $a_2 \in \min(A)$, then $a_1 = a_2$ – a move initial on the left must be justified by the same move on the right. Writing $\omega_A$ for the set of all copycat plays, we have $\omega_A: A \to A$ a strategy as required. For any strategy $\sigma: A \to B$ we have $\omega_B \odot \sigma \odot \omega_A = \sigma$, making $\downarrow\uparrow$-Strat a category.

**Remark 2.14.** Our model shares with AJM games [AJM00] the management of the equivalence $\approx$ on strategies. All our constructions on strategies must preserve $\approx$. For most of them it is clear, but composition requires some care (see Appendix B.3.1). Operations on strategies therefore lift transparently to $\approx$-equivalence classes, and one can then consider $\downarrow\uparrow$-Strat to have as morphisms $\approx$-equivalence classes of strategies (as is done in [AJM00]). This is fine, but it does contrast with how we (also following the practice in AJM games) often refer to specific concrete strategies as being “the interpretation of” specific terms. So we refrain from quotienting, and consider $\downarrow\uparrow$-Strat as having concrete strategies as morphisms, and homsets $\downarrow\uparrow$-Strat($A, B$) additionally equipped with an equivalence relation $\approx$ which all operations preserve. This way the interpretation of terms yields concrete representatives, but categorical laws only hold up to $\approx$. In the sequel we refer only to the plain algebraic structures (as in “symmetric monoidal closed category”, “cartesian closed category”, etc),
with it being understood that laws for these algebraic structures only hold up to ≈ and that for any construction we consider, there is a proof obligation that it preserves ≈ .

2.3.2. *Further structure.* If $A$ and $B$ are $-$arenas, their *tensor* is simply $A \otimes B = A \parallel B$ their parallel composition. For $\sigma_1 : A_1 \to B_1$ and $\sigma_2 : A_2 \to B_2$, the strategy

$$
\sigma_1 \otimes \sigma_2 : A_1 \otimes A_2 \to B_1 \otimes B_2,
$$

defined via adequate restrictions (see Appendix B.2.1), plays as $\sigma_1$ on $A_1, B_1$ and $\sigma_2$ on $A_2, B_2$ – this gives a symmetric monoidal structure, with structural isomorphisms copycat strategies. Moreover, $\downarrow\uparrow$-Strat is cartesian. Its terminal object is the empty $-$arena 1; the product of $A$ and $B$ is the $A \& B$. This forms a cartesian product: there are projections

$$
\pi_A : A \& B \to A
$$

$$
\pi_B : A \& B \to B
$$

acting as copycat, and for $\sigma : C \to A$ and $\tau : C \to B$, their **pairing** $\langle\sigma, \tau\rangle : C \to A \& B$ is
defined simply as the as the set-theoretic union of $\sigma$ and $\tau$ (modulo the obvious relabeling).

Finally, for any $--$arenas $\Gamma, A$ and $B$, there is an iso $\Gamma \otimes A \to B \cong \Gamma \to (A \to B)$, i.e.
a bijection on events preserving and respecting all structure. This yields a bijection

$$
\Lambda_{\Gamma,A,B} : \downarrow\uparrow\text{-Strat}(\Gamma \otimes A, B) \simeq \downarrow\uparrow\text{-Strat}(\Gamma, A \to B)
$$

between the corresponding sets of strategies. Exploiting this, we define the **evaluation**

$$
\mathrm{ev}_{A,B} = \Lambda_{A \to B, A, B}^{-1}(c_{A \to B}) : (A \to B) \otimes A \to B,
$$

and the universal property for monoidal closure is then a direct verification. We conclude:

**Proposition 2.15.** The category $\downarrow\uparrow$-Strat is cartesian and symmetric monoidal closed.

2.3.3. *Exponential.* On $\downarrow\uparrow$-Strat, ! gives an exponential in the sense of Linear Logic [Gir87]: a functor, with natural transformations $\mathrm{der}_A : !A \to A$ and $\mathrm{dig}_A : !A \to !A$ making (!, der, dig) a comonad. Moreover, there are natural isomorphisms $\mathrm{mon}^2_{A,B} : !A \otimes !B \to ! (A \& B)$ and $\mathrm{mon}^0_{A,B} : \mathbf{1} \to !\mathbf{1}$, satisfying the coherence laws of a *Seely category* [Mel09]. So the Kleisli category $\downarrow\uparrow$-Strat! is cartesian closed, and hence a model of the simply-typed $\lambda$-calculus. The construction is routine, and follows the lines of AJM games [AJM00] – see Appendix B.3.

In the sequel, given a Seely category $\mathcal{C}$ and a morphism $f \in \mathcal{C}(!A, B)$, we shall write $f^\dagger \in \mathcal{C}(!A, !B)$ for its **promotion**, defined as $!f \circ \mathrm{dig}_A$ – in particular, recall that Kleisli composition of $f \in \mathcal{C}!(A, B)$ and $g \in \mathcal{C}!(B, C)$ may be defined as $g \circ! f = g \circ f^\dagger \in \mathcal{C}!(A, C)$.

2.3.4. *Recursion.* Strategies on arena *A* may be partially ordered by inclusion; this forms a pointed dcpo. All operations on strategies are continuous with respect to $\subseteq$.

Writing $\downarrow\uparrow$-Strat$_!(A, B)$ for the dcpo of strategies on $A \to B = !A \to B$, the operation

$$
\begin{array}{rcl}
F : & \downarrow\uparrow\text{-Strat}_!(\mathbf{1}, (A \to A) \to A) & \to \\
    & & \downarrow\uparrow\text{-Strat}_!(\mathbf{1}, (A \to A) \to A) \\
\sigma & \mapsto & \lambda f^{A \to A} \cdot f(\sigma f)
\end{array}
$$

written in $\lambda$-calculus syntax following the cartesian closed structure of $\downarrow\uparrow$-Strat$_!$, is continuous.
Its least fixed point $\mathcal{Y}_A \in \downarrow\uparrow$-Strat$_!(\mathbf{1}, (A \to A) \to A)$ is transported to $\downarrow\uparrow$-Strat$_!(\Gamma, (A \to A) \to A)$ by composition with the terminal projection. For each $\sigma \in \downarrow\uparrow$-Strat$_!(\Gamma, A \to A)$,

$$
\mathcal{Y}_A \sigma \approx \sigma (\mathcal{Y}_A \sigma)
$$
<figure><img src="image_18.png" /></figure>

<figure><img src="image_19.png" /><figcaption>Figure 12: Basic strategies for PCF</figcaption></figure>

<figure><img src="image_20.png" /><figcaption>Figure 13: Interpretation of basic combinators</figcaption></figure>

<caption>Figure 14: Strategy for **pred**</caption>

so a fixed point operator up to ≈, as needed to interpret recursion.

It is a curiosity already in AJM games [AJM00] that the recursive equation for the fixpoint combinator must be solved in the domain of *concrete* strategies, rather than ≈-equivalence classes. To the best of our knowledge it is not known if the partial order induced by inclusion on ≈-equivalence classes of strategies has the adequate completeness properties to solve this, i.e. if the quotient of ↓↑-Strat and ↓↑-Strat! by ≈ are dcpo-enriched categories.

2.3.5. *Interpretation.* Types of PCF are interpreted as --arenas: we set [[U]] = U, [[B]] = B, [[N]] = N and [[A → B]] = ![[A]] → [[B]] yielding for any type A an arena [[A]]. A context Γ = x₁: A₁, ..., xₙ: Aₙ is interpreted as [[Γ]] = ⋀₁≤i≤n [[Aᵢ]]. A term Γ ⊢ M : A yields

$$[[M]] \in \text{↓↑-Strat}_!([\Gamma], [A]).$$

We skip the details of the interpretation of the λ-calculus combinators, which follows the standard interpretation of the simply-typed λ-calculus in a cartesian closed category [LS88].

We specify strategies for PCF combinators. For constants, [[skip]] : U, [[tt]] : B, [[ff]] : B and [[n]] : N are the corresponding obvious strategies replying immediately the corresponding value. For the others the interpretation is in Figure 13, annotating strategy operations with ! to emphasize that they are in the Kleisli category ↓↑-Strat!. The strategies used are in Figures 12, 14 and 15. Save for let, the diagram displays exhaustively their maximal plays,
<figure><img src="image_21.png" /><figcaption>Figure 15: Typical play of let</figcaption></figure>

<caption>Figure 16: Pointer annotations on plays</caption>

defining them completely. For **let**, the strategy implements a *memoization* mechanism: it evaluates on $\mathcal{X}$ obtaining a value $v$, then fed to the function argument each call, without re-evaluating it. The play shown for **let** is not maximal as Opponent could play some $\mathbf{q}_{1, i_{n+1}}^{-}$ after. We will see in Section 3.2 that it is fully informative: there is only one *innocent* strategy that includes these plays. The interpretation is completed with $[[\mathcal{Y}_A M]] = \mathcal{Y}_A \odot! [[M]]$.

This interpretation satisfies the main property expected of a denotational semantics:

**Proposition 2.16 (Adequacy).** For any $\vdash M : \mathcal{U}$, $M \llcorner$ if and only if $[[M]] \llcorner$.

Note there are only two strategies on $\mathcal{U}$: the minimal $\{\varepsilon, \mathbf{q}^{-}\}$ matching any *diverging* program, and the converging $\{\varepsilon, \mathbf{q}^{-}, \mathbf{q}^{-}\check{+}^{+}\}$. For $\sigma : \mathcal{U}$, we write $\sigma \llcorner$ if $\sigma$ converges and $\sigma \Uparrow$ if $\sigma$ diverges. We omit the proof which is standard using logical relations, see e.g. [HO00].

This immediately entails soundness for observational equivalence:

**Corollary 2.17.** Let $\Gamma \vdash M, N : A$ be any terms of PCF. If $[[M]] \approx [[N]]$, then $M \sim N$.

*Proof.* Assume $[[M]] \approx [[N]]$, and consider a context $C[-]$ such that $C[M] \llcorner$. By Proposition 2.16, $[[C[M]]] \llcorner$. But $[[C[M]]] = [[C[-]]] \odot! [[M]] \approx [[C[-]]] \odot! [[N]] = [[C[N]]]$, so $C[N] \llcorner$ by Proposition 2.16. The other direction also holds, hence $M \sim N$. $\square$

Computational adequacy is the standard to express that a model accurately describes computation in the language. In fact in game semantics the connection with operational semantics is much stronger, as highlighted earlier. We will elaborate on that in Section 3.

**2.4. HO games.** Before exploring this computational content, we highlight the connection with HO games [HO00], based on representing plays up to symmetry as *plays with pointers*.

2.4.1. *Plays with pointers.* First, a convention. For $A$ a $--$arena and $s \in \downarrow\uparrow$-Plays($A$), then $|s| \in \mathcal{C}(A)$ has two order structures: it is totally ordered chronologically as prescribed by $s$, and has a partial order imported from $\leq_A$. When representing plays, we often annotate them with the immediate causal dependency generating $\leq_A$. For instance, Figure 16 shows it for $s \in \downarrow\uparrow$-Plays($[[\mathcal{U} \to \mathcal{U}] \to \mathcal{B}]$) with $|s|$ displayed in Figure 11. The dashed lines represent immediate causal dependency in $\leq_A$, omitted when it coincides with juxtaposition. We call
these dashed lines pointers, going upwards from one event to its predecessor in A. As arenas are forestial, any move has at most one pointer and only minimal events have none.

It is worth, just this once, being extremely pedantic about the representation used in Figure 16 and others. Recall that $\llbracket (U \to U) \to \mathbb{B} \rrbracket = ! (U \to U) \to \mathbb{B}$. Accordingly,

$$|\llbracket (U \to U) \to \mathbb{B} \rrbracket| = N \times (N \times |U| + |U|) + |\mathbb{B}|$$

with + the tagged disjoint union $A + B = \{1\} \times A \cup \{2\} \times B$, previously also written $||$. So an event of $\llbracket (U \to U) \to \mathbb{B} \rrbracket$ carries a *move* from $U$ or $\mathbb{B}$, *tags* originating from the disjoint unions and indicating one type component, and natural numbers, the *copy indices*. In Figure 16 the information of the *moves* is conveyed by the label, i.e. $\mathbf{q}^{-}$, $\check{+}$, etc. The *tag* is conveyed by the position of the move under the corresponding type component. Finally, the *copy indices* are given as a sequence in grey, with the leftmost integer corresponding to the outermost !. For instance, the move $\mathbf{q}_{0,1}^{-}$ really stands for $(1, (0, (1, (1, \mathbf{q}^{-})))$).

It is often convenient to display pointers, but they are not part of the structure of plays. If they are imported into plays, then copy indices become essentially disposable (up to $\cong$). To make this formal, we start by defining a notion of *plays with pointers* on a $--$arena.

**Definition 2.18.** An alternating play with pointers on A is $s_1...s_n \in |A|^*$ which is:

$$\textit{alternating:} \quad \forall 1 \le i \le n - 1, \text{pol}_A(s_i) \ne \text{pol}_A(s_{i+1}),$$

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

The *non-repetitive* condition of Definition 2.7 would make pointers redundant as each move has a unique predecessor, and the existence of pointers would boil down to the fact that plays reach only down-closed sets of events. It is a useful exercise to show that non-repetitive plays with pointers are in bijection with alternating plays, on arenas without conflict.

Reciprocally, since repetitions are now allowed, we may use them to represent executions with replication even without the expansion process of Section 2.2.

### 2.4.2. Meager and concrete arenas.
Definition 2.18 applies to arenas in the sense of Section 2.2.1, but it ignores part of their structure: it takes no account of *conflict*, and *symmetry*. Indeed, plays with pointers originate from HO games, where arenas are much simpler:

**Definition 2.19.** A meager arena is a partial order with polarities $(A, \le_A, \text{pol}_A)$ s.t.:

*alternating*: if $a_1 \to_A a_2$, $\text{pol}_A(a_1) \ne \text{pol}_A(a_2)$,

*forestial*: if $a_1 \le_A a$ and $a_2 \le_A a$, then $a_1 \le_A a_2$ or $a_2 \le_A a_1$,

without conflict or symmetry. A meager $--$arena additionally satisfies:

*negative*: if $a \in \min(A)$, then $\text{pol}_A(a) = -$.

Clearly, Definition 2.18 applies to meager arenas. Each PCF type A may be interpreted as a meager arena $[A]$, setting $[U] = U$, $[\mathbb{B}] = \mathbb{B}$, $[N] = N$ and $[A \to B] = [A] \to [B]$; i.e. as for $\llbracket - \rrbracket$ but without the ! – this is exactly the interpretation in [HO00]. The arena $\llbracket A \rrbracket$ is then an *expansion* of $[A]$ – the notion of concrete arena makes this explicit:

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

$$\text{lbl} : |A| \to |A^0|,$$
a label function, together satisfying the following additional requirements:

*locally pointed*: for all $x \in \mathscr{C}(A)$, $x$ has at most one minimal event of each polarity,

*rigid*: lbl preserves minimality, and preserves immediate causality $\to$,

*transparent*: for any $x, y \in \mathscr{C}(A)$ and bijection $\theta: x \simeq y$, then $\theta \in \mathscr{S}(A)$ iff $\theta$ is an order-iso preserving lbl.

We shall update this in Section 7.3.1, when further structure becomes required. *Locally pointed* is phrased so as to allow non-negative arenas of the form $A^{\perp} \parallel B$. In most cases, for negative arenas, configurations $x \in \mathscr{C}(A)$ will have at most one minimal event.

Every basic arena $\mathcal{X}$ may be regarded as the concrete arena $(\mathcal{X}, \mathcal{X}, \text{lbl}_{\mathcal{X}})$ with $\text{lbl}_{\mathcal{X}}$ the identity function. Concrete arenas support the arena constructions $\&$ and $\to$ with $(A \& B)^0 = A^0 \otimes B^0$, and $(A \to B)^0 = A^0 \to B^0$. By induction, for every type $A$ this gives us $(\llbracket A \rrbracket, [A], \text{lbl}_A)$, a pointed concrete $--$arena with $\text{lbl}_A$ simply forgetting all copy indices.

**Remark 2.21.** *Transparent* makes explicit the nature of symmetries on arenas arising from types: as they leave all components unchanged except *copy indices*, they are exactly all reindexings. This does not always hold outside the types considered here. In particular, concrete arenas do not support $\otimes$: of course condition *locally pointed* fails, but more fundamentally, valid symmetries in $!(A \otimes B)$ must send $(i, (1, a))$ and $(i, (2, b))$ to the same copy index $j$, a non-local constraint, not reflected by condition *transparent*. This is why we do not consider all arenas to be *concrete*: they fail to cover the full Seely category structure.

In the sequel, we only assume arenas to be concrete when it is explicitely mentioned.

2.4.3. *Pointers and symmetry.* Plays with pointers represent plays up to symmetry:

**Proposition 2.22.** *Consider A a concrete arena. Then, there is a function*

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

*injective and preserving length and prefix.*

*Proof.* For $s \in \downarrow\uparrow\text{-Plays}(A)$, we first construct $s^- \in \mathcal{P} : \downarrow\uparrow\text{-Plays}(A)$ by importing $\to_A$. Then, $\mathcal{P}(s)$ is obtained by applying $\text{lbl}_A$ pointwise. That pointers on $\mathcal{P}(s)$ are well-formed (i.e. that if $s_j$ points to $s_i$, then $s_i \to^{A^0} s_j$) follows from $\text{lbl}$ preserving minimality and the immediate causal order. That $\mathcal{P}$ is invariant under $\cong$ boils down to *transparent*. By construction, $\mathcal{P}$ preserves length and prefix. For injectivity, take $s, s' \in \downarrow\uparrow\text{-Plays}(A)$ such that $\mathcal{P}(s) = \mathcal{P}(s')$. Since $\mathcal{P}$ is length-preserving, $s$ and $s'$ have the same length $n$. Consider

$$ \theta = \{(s_i, s'_i) \mid 1 \le i \le n\} : |s| \approx |s'| $$

the induced bijection. Since $\mathcal{P}(s) = \mathcal{P}(s')$, in particular $s$ and $s'$ have the same pointers, so $\theta$ is an order-isomorphism, and moreover since $\mathcal{P}(s) = \mathcal{P}(s')$ again we also have $\text{lbl}_A(s_i) = \text{lbl}_A(s'_i)$ for all $1 \le i \le n$. Hence, $\theta$ is a symmetry, so by *transparent*, $s \cong s'$ as required. $\square$

However, $\mathcal{P}$ is not surjective. Writing $A = \mathcal{U} \to \mathcal{B}$, the play $s \in \mathcal{P} : \downarrow\uparrow\text{-Plays}([A])$ set as

<figure><img src="image_22.png" /></figure>
is not the image of any play in $↓↑-Plays([A])$, for two reasons: (1) not every move is duplicated in $[A]$, e.g. there is only one copy of $\checkmark$ for every copy of $q^+$ – this linearity discipline is enforced by the *non-repetitive* condition, which is absent in $\mathcal{P}-↓↑-Plays([A])$; and (2) likewise, $[A]$ and $\mathcal{P}-↓↑-Plays([A])$ do not account for *conflict* between $tt^+$ and $ff^+$ in $[A]$.

2.4.4. **HO strategies.** This extends to strategies. For concrete arena $A$ and $\sigma: A$, then $\mathcal{P}(\sigma) = \{\mathcal{P}(s) \mid s \in \sigma\}$ is a strategy on $A^0$ in the Hyland-Ong sense, i.e. a prefix-closed, deterministic set of plays with pointers closed under Opponent extensions. We have:

**Proposition 2.23.** Consider $A$ a concrete arena, and prestrategies $\sigma, \tau: [A]$.

Then, $\sigma \approx \tau$ iff $\mathcal{P}(\sigma) = \mathcal{P}(\tau)$.

*Proof.* If. Consider $\sigma, \tau: A$ s.t. $\mathcal{P}(\sigma) = \mathcal{P}(\tau)$. For $\sigma \approx \tau$ we first check $\rightarrow$-simulation. Consider $sa^+ \in \sigma, t \in \tau$ s.t. $s \cong_A t$. But $\mathcal{P}(sa) \in \mathcal{P}(\tau)$, so there is $t'b' \in \tau$ s.t. $\mathcal{P}(t'b') = \mathcal{P}(sa)$. Hence by Proposition 2.22, $sa \cong_A t'b'$. So $t, t' \in \tau$ and $t \cong_A t'$, with $t'b' \in \tau$. By uniformity of $\tau$, $tb \in \tau$ for some $b$ with $t'b' \cong_A tb$, so $tb \cong_A sa$ as well. The condition $\leftarrow$-simulation is symmetric. For $\rightarrow$-receptive, assume $sa^- \in \sigma, t \in \tau$ and $sa^- \cong_A tb^-$. Since $\mathcal{P}(sa^-) \in \tau$, there is $t'b' \in \tau$ s.t. $\mathcal{P}(sa) = \mathcal{P}(t'b')$, i.e. $sa \cong_A tb$. But then $t'b' \in \tau$ and $t'b' \cong_A tb$, so by uniformity of $\tau$ we have $tb \in \tau$. Finally, $\leftarrow$-receptive is symmetric.

Only if. Consider $\sigma, \sigma': A$ s.t. $\sigma \approx \sigma'$, and take $\mathcal{P}(s) \in \mathcal{P}(\sigma)$ for some $s \in \sigma$. By induction on $s$, we build some $s' \in \sigma'$ s.t. $s \cong_A s'$: for positive extensions this follows from $\sigma \approx \sigma'$; for negative extensions from the extension condition on isomorphism families and the $\rightarrow$-receptive condition on uniformity. But then by Proposition 2.22 we have $\mathcal{P}(s) = \mathcal{P}(s')$, so $\mathcal{P}(\sigma) \subseteq \mathcal{P}(\sigma')$. The argument is symmetric, so $\mathcal{P}(\sigma) = \mathcal{P}(\sigma')$ as desired. $\square$

Plays with pointers permit a presentation of strategies up to $\approx$, avoiding copy indices. They provide the foundation for HO games [HO00], where the interpretation of types is essentially $[-]$ (without conflict), and plays carry pointers. We include the classical example showing that though one may choose copy indices or pointers, one cannot avoid both.

**Example 2.24.** The Kierstead terms $\vdash K_x, K_y : ((\mathbb{B} \rightarrow \mathbb{B}) \rightarrow \mathbb{B}) \rightarrow \mathbb{B}$ are defined as

$$K_x = \lambda F(\mathbb{B} \rightarrow \mathbb{B}) \rightarrow \mathbb{B} \cdot F(\lambda x. F(\lambda y. x)), \quad K_y = \lambda F(\mathbb{B} \rightarrow \mathbb{B}) \rightarrow \mathbb{B} \cdot F(\lambda x. F(\lambda y. y)).$$

Their respective interpretations in $↓↑-Strat_1$ have distinctive plays:

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

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

Here pointers are redundant, and computed from the identity of moves. In particular, in both plays the $q^+$ “points to” the unique $q^-$ with compatible copy indices. Mapping these through $\mathcal{P}$, we get two plays with pointers that only differ through their pointers. In HO games, the Kierstead terms are only distinguished by pointers$^6$. It is crucial to keep them separate: it is a surprisingly challenging exercise to find a PCF context that separates them.

<footnote>$^6$It is necessary to go up to third-order types to find such examples. Pointers are redundant up to second-order types, which is the starting point of algorithmic game semantics [GM03].</footnote>
<figure><img src="image_25.png" /><figcaption>Figure 17: Illustration of the operational contents of game semantics</figcaption></figure>

Plays with pointers are powerful, and indeed the game semantics literature is strongly biaised towards HO games (as opposed to AJM games). This, however, has two costs. Firstly, plays with pointers are not a natural inductive structure, making their manipulation sometimes inelegant or unwieldy (so-called “pointer surgery”). Propositions have been made for clean formalizations, e.g. through nominal sets [GG12]. Another cost is that replication is so hard-wired into the model that it does not enjoy a clean linear decomposition. Enforcing linearity is slightly awkward and relies on additional structure [McC98].

In this work we stick with $\downarrow\uparrow$-Strat rather than adopting plays with explicit pointers. Among other things this will ease the relationship with the forthcoming *thin concurrent games*, which we do not know how to formulate with pointers in general. Besides, in $\downarrow\uparrow$-Strat, pointers *can* be directly obtained from the arena, and as such may be used as in HO games$^7$. In fact, pointers play a central role in this paper. From now on, all representations of plays will display pointers. In contrast, we will often omit copy indices as most of the time they convey no useful information; one can regard this convention as drawing $\mathcal{P}(s)$ rather than $s$.

### 3. SEQUENTIAL COMPUTATIONAL EFFECTS IN GAME SEMANTICS

We now explore the model constructed above, introducing the traditional “semantic cube”.

The plays of a term are computed denotationally, by induction on syntax. However, given a term, an experienced game semanticist will be able to directly list its plays, without going through the intricate definition of the interpretation. This is because as discussed before, plays represent the operational behaviour of the term: rather than denotationally, they can be obtained directly from the term by operational means [DHR96, Jab15, GT12, LS14]. This is illustrated in Figure 17. Opponent moves trigger the evaluation of a subterm, which appears boxed. The following Player move then corresponds to the head (i.e. leftmost)

<footnote>$^7$Another work blurring the lines between HO and AJM is [AJ09] where AJM games are equipped with a *function* able to rebuild pointers without the need to explicitly integrate them in plays. All the data of a game in the sense of [AJ09] can be computed from an arena in our sense, but our arenas are more primitive.</footnote>
variable occurrence (or constant) of the subterm being evaluated. The pointers from Player moves correspond to the stage where the variable in head position was abstracted, or to the function call being returned by the value in head position. More specifically, Figure 17 represents the interaction of the term under study with the applicative context:

$$C[] = [] (\lambda x^{\mathbb{B}} . \lambda y^{\mathbb{B}} . \mathbf{if} x \ (\mathbf{if} y \ \mathbf{skip} \ \mathbf{skip}) \ \mathbf{skip})$$

Figure 17 is strongly inspired by the *Pointer Abstract Machine (PAM)* [DHR96].

**3.1. Well-Bracketing.** Now that *executions as plays* are first-class citizens, independent of programs, we may start classifying them according to the computational capabilities that they witness. For instance, is the following play a possible execution of a term?

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

We argue informally why this cannot be an execution in PCF. The first action of the term is to ask its argument, so it has the form $\lambda f^{U \to U} . f M$; we annotate the figure with the corresponding operational state as in Figure 17. In the last line, **tt** at toplevel indicates the overall computation has terminated to **tt**. This is confusing, since operationally the Opponent move in the third line corresponded to triggering the evaluation of the argument of $f$. How can evaluating the argument of $f$ cause the whole computation to terminate?

Nevertheless, this play is indeed a realistic execution, for the term

$$\lambda f^{U \to U} . \mathbf{callcc} (\lambda k^{\mathbb{B} \to U} . f (k \mathbf{tt}); \perp) : (U \to U) \to \mathbb{B}$$

where **callcc** is the *call-with-current-continuation* primitive originating in *Scheme*, and which famously may be typed with Peirce's law [Gri90]. The precise operational semantics of **callcc** will not be useful for this paper, but informally **callcc** *M* immediately calls *M*, feeding it a special function *k*, the “continuation”. When the continuation is called with value *v*, **callcc** interrupts *M* and returns *v* at toplevel, breaking the call stack discipline.

Can the play above be realised without **callcc** (or some other *control operator*, as such primitives are called)? We can show that the answer is no, by capturing plays that “respect the call stack discipline”, and refining the whole interpretation to show that this invariant is preserved. This is the goal of the notion of *well-bracketing*. First we enrich arenas:

**Definition 3.1.** A Question/Answer labeling on arena *A* is a function

$$\lambda_A : |A| \to \{\mathcal{Q}, \mathcal{A}\}$$

invariant under symmetry (if $\theta: x \cong_A y$, then for all $a \in x$, $\lambda_A(a) = \lambda_A(\theta(a))$) and satisfying:

*question-opening:* if $a \in |A|$ is minimal, then $\lambda_A(a) = \mathcal{Q}$,

*answer-closing:* if $\lambda_A(a) = \mathcal{A}$, then $a$ is maximal for $\leq_A$,

*answer-linear:* if $\lambda_A(a_1) = \lambda_A(a_2) = \mathcal{A}$ with $a \to_A a_1, a_2$, then $a_1 = a_2$ or $a_1 \#_A a_2$.

From now on, **arenas** have a *Question/Answer labeling*. *Questions* intuitively correspond to variable calls, while *Answers* correspond to returns. Basic arenas are enriched as shown in Figure 18. For other constructions the labeling is inherited transparently, with $\lambda_{!A}(i, a) = \lambda_A(a)$, $\lambda_{A_1 \otimes A_2}(i, a) = \lambda_{A_i}(a)$, $\lambda_{A \to B}(2, b) = \lambda_B(b)$, and $\lambda_{A \to B}(1, (b, a)) = \lambda_A(a)$.
<figure><img src="image_27.png" /><figcaption>Figure 18: Question/Answer labeling on basic arenas</figcaption></figure>

If $s \in \text{↓↑-Plays}(A)$ and $s_i$ is an answer, it cannot be minimal in $A$ by question-opening. Its antecedent in $A$ – its *justifier* – must appear in $s$ as some $s_j$ with $j < i$, and is a question by *answer-closing*. We say that $s_i$ **answers** $s_j$. If a question in $s$ has an answer in $s$ we say it is **answered** in $s$. The last unanswered question of $s$, if any, is the **pending question**.

We now capture executions respecting the call stack discipline as *well-bracketed* plays.

**Definition 3.2.** Let $s \in \text{↓↑-Plays}(A)$ be an alternating play.

It is **well-bracketed** if for all prefix $ta^A \subseteq s$, $a$ answers the pending question of $t$.

All plays encountered in the paper until now are well-bracketed, with the exception of the example at the beginning of Section 3.1. We can then define well-bracketed strategies:

**Definition 3.3.** Let $\sigma: A$ be a strategy on $A$.

It is **well-bracketed** iff for all $sa^+ \in \sigma$, if $s$ is well-bracketed then $sa$ is well-bracketed.

In other words, a well-bracketed strategy is never the first to break the call stack discipline. Asking all plays to be well-bracketed is too strict, as illustrated by the play

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

of copycat: the last move does not answer the pending question, but because Opponent broke the normal control flow first. There is a lluf subcategory $\text{↓↑-Strat}^{\text{wb}}$ of $\text{↓↑-Strat}$, having well-bracketed strategies as morphisms. The interpretation of PCF in $\text{↓↑-Strat}_i$ in fact yields only well-bracketed strategies, i.e. has target $\text{↓↑-Strat}_i^{\text{wb}}$. This shows that indeed, the execution at the beginning of Section 3.1 cannot be realised in PCF.

3.2. Visibility and Innocence. Likewise, is this play a possible execution of a term?

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

Again, this seems unfeasible in PCF. Again, on the right hand side we show, assuming a term realising this play, its corresponding operational states. At the third and fifth moves, the *same* subterm is being evaluated; yet we get two distinct answers. In an extension
<figure><img src="image_30.png" /><figcaption>Figure 19: A strategy with references</figcaption></figure>

<caption>Figure 20: Non P-visible play</caption>

of PCF with a primitive `+` for non-deterministic choice, this play would be realisable by $\lambda f^{\mathbb{B} \to \mathbb{U}}. f(\mathbf{tt} + \mathbf{ff}).$ But does it make computational sense in a *deterministic* language?

Once more, the answer is yes: the play above describes a valid execution of the term

$$ \lambda f^{\mathbb{B} \to \mathbb{U}}. \mathbf{newref} \ r \ \mathbf{in} \ f(\mathbf{let} \ x =!r \ \mathbf{in} \ r := 1; (x > 0)) : (\mathbb{B} \to \mathbb{U}) \to \mathbb{U} $$

in PCF extended with references: **newref r in M** allocates a reference r initialized to 0. We show in Figure 19 an operational description as to how this term indeed realises this play.

Again, this cannot be realised in PCF. To show this, we give a version of *innocence* [HO00], formalizing that without state, evaluating the same subterm yields the same response. The first step is a mathematical way to state that two plays “correspond to the same subterm”, like the two prefixes of the play of Figure 19 terminating with a $\mathbf{q}^-$ on the left.

The operation computing (a mathematical notion of) “current subterm” is the *P-view*:

**Definition 3.4.** Let $s \in \downarrow\uparrow$-Plays($A$). Its **P-view** is the subsequence defined by induction:

$$ \begin{align*} \mathbf{r}\varepsilon' &= \varepsilon \\ \mathbf{r}sa^+ &= \mathbf{r}s'a^+ \\ \mathbf{r}sa_1^+ s'a_2^- &= \mathbf{r}s'a_1^+ a_2^- \quad \text{if } a_1^+ \to_A a_2^- \\ \mathbf{r}sa_1^+ s'a_2^- &= a_2^- \quad \text{if } a_2^- \text{ is negative minimal in } A \end{align*} $$

We take the immediate prefix for P-ending plays and follow the pointer for O-ending plays. For instance, the prefixes of length 3 and 5 of the play on Figure 19 have the same P-view, capturing that they correspond to the same subterm. This is a powerful definition – really, the distinguishing feature of HO games [HO00] – and it often takes newcomers a while to digest. Interestingly, our forthcoming *parallel innocence* will be phrased quite differently.

But this is not yet conclusive: if $s \in \downarrow\uparrow$-Plays($A$), it might be that $\mathbf{r}s' \notin \downarrow\uparrow$-Plays($A$). For instance, in Figure 20 we gray out moves not selected in computing the P-view of $s \in \downarrow\uparrow$-Plays($A$) for $A = [(\mathbb{U} \to \mathbb{U}) \to \mathbb{U}]$. The subsequence of $\mathbf{r}s'$ in black is an alternating sequence of $|A|$, but fails valid of Definition 2.7. Indeed, the “justifier” of $\check{+}$, its immediate dependency in $A$, is not selected – thus $|\mathbf{r}s'|$ is not down-closed. Accordingly, we say:

**Definition 3.5.** A play $s \in \downarrow\uparrow$-Plays($A$) is **P-visible** if for all prefix $\forall t \subseteq s$, $\mathbf{r}t' \in \downarrow\uparrow$-Plays($A$).

Likewise, a strategy $\sigma: A$ is **P-visible** iff all its plays are P-visible.

So, “computing P-views never drops pointers”, or “Player always points in the P-view”. On P-visible $s \in \downarrow\uparrow$-Plays($A$), the P-view always yields a well-formed (P-visible) play.

We now define *innocent strategies* as those that behave the same in any situation where the same subterm is being evaluated, i.e. whose behaviour only depends on the *P-view*:
**Definition 3.6.** A P-visible alternating strategy $\sigma : A$ is **innocent** if it satisfies:

innocence: for all $sa^+ \in \sigma$, for all $t \in \sigma$, if $\lceil s' \rceil = \lceil t' \rceil$ then $ta^+ \in \sigma$.

That $ta^+ \in \downarrow\uparrow$-Plays($A$) is well-formed relies on $\lceil s' \rceil = \lceil t' \rceil$, so that the causal dependencies of $a$ in $A$ appear in $t^8$. All structural morphisms of $\downarrow\uparrow$-Strat are innocent. Innocent strategies compose – though this is infamously tricky to prove, prompting a significant line of work investigating the structures arising from the composition of innocent strategies [Cur98, HHM07, CD15]. We do not review here the proof of stability under composition.

The interpretation of PCF yields only innocent strategies, i.e. targets the cartesian closed lluf subcategory $\downarrow\uparrow$-Strat<sub>i</sub><sup>inn</sup> of innocent strategies. Hence, the play at the beginning of Figure 3.2 cannot be realised in PCF. We also get a cartesian closed lluf subcategory $\downarrow\uparrow$-Strat<sub>i</sub><sup>wb,inn</sup> with well-bracketing. Finally, the weaker P-visibility is also preserved under the categorical operations, forming lluf sub-cartesian closed categories $\downarrow\uparrow$-Strat<sub>i</sub><sup>vis</sup> and $\downarrow\uparrow$-Strat<sub>i</sub><sup>wb,vis</sup>.

**3.3. Full Abstraction for PCF.** We have now eliminated all non PCF-definable behaviour. We review the corresponding definability and intensional full abstraction arguments.

**3.3.1. Definability.** Call a **P-view** on arena $A$ any $s \in \downarrow\uparrow$-Plays($A$) invariant under P-view, i.e. $\lceil s' \rceil = s$ – those are exactly the $s \in \downarrow\uparrow$-Plays($A$) such that for all $ts_i^+ s_{i+1}^- \subseteq s$, we have $s_i \to_A s_{i+1}$, in other words *Opponent always points to the previous move*. We motivated P-views as a way to address specific “subterms” of a strategy – it might therefore not be a surprise that those are the key to reconstruct a term from an innocent strategy. We write

$$ \pi\sigma^n = \{\lceil s' \rceil | s \in \sigma\} $$

for the set of P-views of $\sigma$. If $\sigma$ is innocent, then it is simple that $\pi\sigma^n \subseteq \sigma$. Moreover, $\sigma$ can then be recovered as the set of P-visible $s \in \downarrow\uparrow$-Plays($A$) such that for all $t \subseteq s$, $\lceil t' \rceil = \pi\sigma^n$.

For $\sigma : A$ innocent, $\pi\sigma^n$ is not a strategy as in general it fails receptivity. It is however easily verified to be a *prestrategy* – and in particular *uniform*. Moreover, we have:

**Proposition 3.7.** For $\sigma, \tau : A$ innocent strategies on $A$, we have $\pi\sigma^n = \pi\tau^n$ iff $\sigma = \tau$.

Likewise, $\pi\sigma^n \approx \pi\tau^n$ if and only if $\sigma \approx \tau$.

*Proof.* We only detail the second statement. Firstly, if $\sigma \approx \tau$, it is direct that $\pi\sigma^n \approx \pi\tau^n$ as $\pi\sigma^n \subseteq \sigma$ and $\pi\tau^n \subseteq \tau$ and the bisimulation game of Definition 2.13 preserves P-views.

If $\pi\sigma^n \approx \pi\tau^n$, take $sa^+ \in \sigma, t \in \tau$ s.t. $s \cong_A t$. In particular $\lceil s' \rceil \cong_A \lceil t' \rceil$ and $\lceil s'a^+ \rceil \in \pi\sigma^n$. By $\to$-extension, there is $b^+$ s.t. $\lceil t'b^+ \rceil \in \pi\tau^n$, so $tb^+ \in \tau$ by innocence. This proves $\to$-extension, $\leftarrow$-extension is symmetric and $\to, \leftarrow$-receptivity follow by receptivity of $\sigma, \tau$. $\square$

So innocent strategies have two representations: a full $\sigma : A$ satisfying Definition 3.6; or, following Proposition 3.7, the set $\pi\sigma^n$. Anticipating on later developments, we refer to $\pi\sigma^n$ as the *causal* presentation of $\sigma$. In traditional innocent game semantics, the forest of P-views is called (notably by Curien [Cur06]) the *meager* representation, while the set of plays is *fat*. Here this is misleading, because plays in $\pi\sigma^n$ still carry explicit copy indices. In particular $\pi\sigma^n$ has branches matching all copyable Opponent moves, which is “fat”.

To recover the meager representation, we show:

<footnote n="8">⁸In traditional Hyland-Ong games based on plays with points, one would conclude the above definition with something like “... then $ta \in \sigma$, where $a$ has the same pointer as in $sa$”, which is rarely made very formal. Here, because pointers are derived the above definition is rigorous and self-contained.</footnote>
**Proposition 3.8.** Consider A a concrete arena and $\sigma, \tau : A$ innocent strategies.
If $\mathcal{P}(^{\pi}\sigma^{\pi}) = \mathcal{P}(^{\pi}\tau^{\pi})$, then $\sigma \approx \tau$.

*Proof.* Let $\sigma, \tau : [A]$ be innocent strategies on A and assume that $\mathcal{P}(^{\pi}\sigma^{\pi}) = \mathcal{P}(^{\pi}\tau^{\pi})$. By Proposition 2.23, $^{\pi}\sigma^{\pi} \approx ^{\pi}\tau^{\pi}$. Then, by Proposition 3.7, it follows that $\sigma \approx \tau$. $\square$

This, at last, provides the *meager* representation.

These representations have distinct advantages: composition is only directly defined on the fat representation; but it is the meager one that bridges innocent strategies and syntax and allows definability. An innocent alternating strategy $\sigma : A$ is **finite** iff $\mathcal{P}(^{\pi}\sigma^{\pi})$ is finite. Its **size** is simply the cardinal of that set. Definability simply follows the meager form:

**Theorem 3.9.** Let A be a PCF type, and $\sigma : [A]$ be a finite well-bracketed innocent strategy.
Then, there is a PCF term $\vdash M : A$ s.t. $[M] \approx \sigma$.

*Proof.* We describe the argument – for more details, the reader is referred to [HO00].

Without loss of generality, A has the form $A_1 \to \dots \to A_n \to \mathbb{X}$ where for each $1 \le i \le n$,

$$A_i = A_{i,1} \to \dots \to A_{i,p_i} \to \mathbb{X}_i.$$

We reason on $^{\pi}\sigma^{\pi}$, by induction on the size of $\sigma$. If $\sigma$ has no reaction to the (unique) minimal $\mathbf{q}^{-}$ in $\mathbb{X}$ (i.e. $\sigma = \{\varepsilon, \mathbf{q}^{-}\}$), any diverging term will do. Otherwise, by determinism there is exactly one move $a^{+}$ s.t. $\mathbf{q}^{-}a^{+} \in \sigma$. If $a^{+}$ is an answer $v^{+}$ on $\mathbb{X}$, then M is the matching constant. Otherwise, $a^{+}$ is the initial $\mathbf{q}_{i_0}^{+}$ in some $A_{i_0}^{9}$. The situation is drawn as

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

with, in grey, the possible extended P-views. For each extension there is a residual substrategy. We extract those – first, if $\mathbf{q}_{i_0}^{+}$ immediately returns. For each value $v$ in $\mathbb{X}_i$, we form

$$^{\pi}\sigma^{\pi} = \{\mathbf{q}^{-} s | \mathbf{q}^{-} \mathbf{q}_{i_0}^{+} v^{-} s \in ^{\pi}\sigma^{\pi}\},$$

a causal innocent strategy on $[A]$ of size strictly lesser than $\sigma$. By induction hypothesis there is $\vdash M_v : A$ with $[M_v] \approx \sigma_v$. As $\sigma$ is finite, there are finite many $v$ s.t. $\sigma_v$ is non-diverging.

Alternatively, for all $1 \le j \le p_{i_0}$, we consider P-views $\mathbf{q}^{-}\mathbf{q}_{i_0}^{+}\mathbf{q}_{i_0,j}^{-} s \in ^{\pi}\sigma^{\pi}$ where as a P-view, s answers neither $\mathbf{q}_{i_0}^{+}$, nor $\mathbf{q}^{-}$ by well-bracketing. Such a P-view yields

$$\mathbf{q}_{i_0,j}^{-} s \in \downarrow\uparrow\text{-Plays}([A_1 \to \dots \to A_n \to A_{i_0,j}])$$

a P-view where moves in s formerly depending on $\mathbf{q}^{-}$ in $[A]$ are set to depend on $\mathbf{q}_{i_0,j}^{-}$. Considering all such P-views generates a causal innocent strategy of size strictly lesser than $\sigma$, hence by induction hypothesis there is $\vdash M_{i_0,j} : A_1 \to \dots \to A_n \to A_{i_0,j}$ s.t. $[M_{i_0,j}] \approx \sigma_{i_0,j}$.

Finally, with all this data we may form $\vdash M : A$ as

$$\lambda x_1^{A_1} \dots x_n^{A_n} \begin{array}{ll} \textbf{case} & x_{i_0} (M_{i_0,1} x_1 \dots x_n) \dots (M_{i_0,p_{i_0}} x_1 \dots x_n) & \textbf{of} \\ & v_1 \mapsto M_{v_1} \\ & \dots \\ & v_p \mapsto M_{v_p} \end{array}$$

where $p$ is such that every $\sigma_{v_i}$ with $i > p$ is diverging. We get, as needed $[M] \approx \sigma$. $\square$

<footnote n="9">⁹Here the subscripts indicate the type component and not copy indices, which are left un-specified.</footnote>
The final statement is a careful verification following the definition of the interpretation, see [HO00]. Here, **case** is the syntax introduced in Section 1.3, involving the **let** construct. Without that, simply iterating **if** constructs would yield a strategy that re-computes

$$x_{i_0} (M_{i_0,1} x_1 \dots x_n) \dots (M_{i_0,pi_0} x_1 \dots x_n)$$

each time it matches it against a value. This is what is done in [HO00] as their version of PCF does not include a **let** construct. This yields a term that is not $\approx$-equivalent to $\sigma$, but is nonetheless $\sim$-equivalent (see Section 1.6), which suffices for full abstraction. We prefer the present more intensional definability result, and hence have included the **let** construct<fnref n="10" />.

### 3.3.2. *Intensional full abstraction.*
Full abstraction of a denotational model with respect to a language was defined in Section 1.6. Of course, $\downarrow\uparrow$-Strat is not fully abstract for PCF as it stands. For instance, $[[\lambda x^\mathcal{U}. x; x]] \not\approx [[\lambda x^\mathcal{U}. x]]$: game semantics displays explicitely individual calls to $x$, so we see that the term on the left hand side evaluates $x$ twice whereas the other evaluates it once. However, we do of course have $\lambda x^\mathcal{U}. x; x \sim \lambda x^\mathcal{U}. x$; this can for instance be deduced from them having the same interpretation in Scott domains [Plo77].

The celebrated “full abstraction for PCF” results are in fact what (following [AJM00]) we call *intensional full abstraction*. Fixing an interpretation $[[\cdot]]$ of PCF into a $C$, we set

$$f \sim g \quad \Leftrightarrow \quad \forall \alpha \in C(A \to B, [[U]]), \quad (\alpha \circ \bar{f} = \alpha \circ \bar{g}),$$

for $f,g \in C(A,B)$, with $\bar{f}, \bar{g} \in C(1, A \to B)$ obtained via cartesian closure, and **1** the terminal object of $C$. This mimics the definition of observational equivalence. We say that $C$ is **intensionally fully abstract** for PCF iff the quotiented model $C^-$ is fully abstract.

**Theorem 3.10.** *The model $\downarrow\uparrow$-Strat<sub>1</sub><sup>wb,inn</sup> is intensionally fully abstract for PCF.*

*Proof.* Consider $\vdash M, N : A$ s.t. $M \sim N$, and assume $[[M]] \uplus [[N]]$, i.e. there is a test $\alpha \in \downarrow\uparrow$-Strat<sub>1</sub><sup>wb,inn</sup>($[[A]]$, $[[U]]$) s.t. $\alpha \odot_1 [[M]] \neq \alpha \odot_1 [[N]]$ – say w.l.o.g. that $\alpha \odot_1 [[M]] \downarrow$ converges while $\alpha \odot_1 [[N]] \uparrow$. One may prove (see [HO00] for details) that the corresponding interactions expose only a finite part of $\alpha$, so w.l.o.g. we can assume $\alpha$ finite. By Theorem 3.9, $\alpha$ is defined via a PCF term, providing a context $C[-]$ s.t. $[[C[M]]] = \alpha \odot_1 [[M]]$ and $[[C[N]]] = \alpha \odot_1 [[N]]$. But then, we must have $C[M] \downarrow$ while $C[N]$ diverges by Proposition 2.16; contradiction. $\square$

Intensional full abstraction is full abstraction for an *a priori* non effective quotiented model: it does not directly provide effective tools to reason about observational equivalence. Instead, it is a way of stating that we have faithfully captured the intensional behaviour of programs, in the sense that the added tests in the model are not able to distinguish more – there is no “abstraction leak”. Often, it packages adequacy and finite definability.

*Full abstraction* is of course the preferred notion when the quotiented model is sufficiently effective and the interpretation computable (i.e. *effectively presentable* [Plo81]). But when it requires an undecidable quotient<fnref n="11" />, we believe it preferable to use a different terminology: “intensional full abstraction” puts the emphasis on the model pre-quotient. In game semantics, it is that model pre-quotient that had the most impact. In particular it then led to *effective* fully abstract models for stateful languages, leveraging the results and insights above.

<footnote n="10">¹⁰An alternative is to include a primitive **case** evaluating its argument exactly once. The terms then obtained via definability are easily characterised syntactically – dubbed PCF Böhm trees by Curien, and are studied in [Cur98]. The definability process informs a concrete order-isomorphism between finite meager innocent strategies and finite PCF Böhm trees, emphasizing that meager innocent strategies are syntax.</footnote>

<footnote n="11">¹¹For PCF this is unavoidable as observational equivalence is undecidable already for finitary PCF [Loa01].</footnote>
<figure><img src="image_32.png" /><figcaption>Figure 21: $\mathbf{ref}_w$</figcaption></figure>

<figure><img src="image_33.png" /><figcaption>Figure 22: $\mathbf{ref}_r$</figcaption></figure>

<figure><img src="image_34.png" /><figcaption>Figure 23: $\mathbf{sem}$</figcaption></figure>

**3.4. Full Abstraction for IA.** The exposition in Section 3.2 suggests that also without innocence, strategies are computationally relevant for programs with mutable state. We now focus on the game semantics of IA, namely PCF extended with interference (see Section 1).

**3.4.1. Interpretation of types.** With respect to PCF, IA adds the type **ref** of integer references, and the type **sem** of semaphores. Their usual game semantic interpretation is behavioural, in the sense that it represents how one may interact on those types: one may read a reference or write a new value in it; and likewise one may grab a semaphore, or release it.

To capture this, we define --arenas: $\mathbf{ref}_w = \mathcal{A}_{n \in \mathbb{N}} U$, $\mathbf{ref}_r = \mathbb{N}$ and $\mathbf{sem} = U \& U$, and set $[[\mathbf{ref}]] = \mathbf{ref}_w \& \mathbf{ref}_r$ and $[[\mathbf{sem}]] = \mathbf{sem}$. Although we reuse the arena constructions for $U$ and $\mathbb{N}$, for specific moves in these arenas we use the naming conventions of Figures 21, 22 and 23 – in Figures 21 and 22 all distinct moves in the same row are in pairwise conflict.

**3.4.2. Interacting with Memory and Semaphores.** The idea behind Abramsky and McCusker's interpretation of state is that it is not the operations of reading, writing, grabbing or releasing a semaphore that are effectful – indeed, those are just requests via the interface provided by the **ref** and **sem** types and associated commands. The strategy for a program with free reference or semaphore variables will simply record their accesses leaving the memory and semaphores uninterpreted. For instance, the strategy for $x: \mathbf{ref} \vdash x := 0$; $!x: \mathbb{N}$ includes:

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

a play where the value read is not the value just written. The actual effectful computation will be handled in Section 3.4.3 with the creation of new references and semaphores.

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

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

using the (innocent well-bracketed) strategies of Figures 24, 25, 26, and 27. Finally, we set

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

where $[[M]]$ is $[[M]]$ applied to the constant strategy $n$ (using the cartesian closed structure of $\downarrow\uparrow$-Strat), and using implicitly the isomorphisms $\mathbf{ref} \cong (\&_{n \in \mathbb{N}} U) \& \mathbb{N}$ and $\mathbf{sem} \cong U \& U$.

Finite definability of finite innocent well-bracketed strategies still holds – the proof (see [AM96]) directly extends that of Theorem 3.9, using bad variables and semaphores.
<figure><img src="image_38.png" /><figcaption>Figure 24: assign</figcaption></figure>

<caption>Figure 25: deref</caption>

<caption>Figure 26: grab</caption>

<caption>Figure 27: release</caption>

**Proposition 3.11.** Consider A a type of IA, and $\sigma: [[A]]$ finite innocent well-bracketed. Then, there is a IA term $\vdash M: A$ not using newref or newsem, such that $[[M]] \approx \sigma$.

### 3.4.3. Creation of References and Semaphores.
Finally, we introduce the actual effectful behaviour. The idea is to use non-innocent `cell_n`:!ref, `lock_n`:!sem implementing interference. For instance, `cell_n` is a memory cell with `n` currently stored. When read it returns `n`, and upon a write request for `k` $\in$ $\mathbb{N}$, it acknowledges it and proceeds as `cell_k`. Likewise `lock_0` is the strategy for a free semaphore, and `lock_n` for $n > 0$ represents a semaphore in use. Those may be simply described as the language of prefixes of the infinite trees:

$$ \mathit{cell}_n^I = \mathbf{r}_i^- \cdot n_i^+ \cdot \mathit{cell}_n^{I \uplus \{i\}} | \mathbf{wk}_i^- \cdot \mathbf{\check{\vee}}_i^+ \cdot \mathit{cell}_k^{I \uplus \{i\}} \quad (i \notin I) $$

$$ \mathit{lock}_0^I = \mathbf{g}_i^- \cdot \mathbf{\check{\vee}}_i^+ \cdot \mathit{lock}_1^{I \uplus \{i\}} | \mathbf{d}_i^- \quad (i \notin I) $$

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

where symbols are moves in !ref and !sem respectively, separated via $\cdot$ for readability. Here, $I \subseteq_f \mathbb{N}$ collects the copy indices already used, ensuring non-repetitive. We set `cell_n` as (the prefix language of) `cell_n` and `lock_n` as (the prefix language of) `lock_n`; it is direct that `cell_n`:!ref and `lock_n`:!sem. However, they are not innocent. Considering the two plays:

$$ \mathbf{r}_0^- \cdot 0_0^+, \quad \mathbf{w}1_1^- \cdot \mathbf{\check{\vee}}_1^+ \cdot \mathbf{r}_0^- \cdot 1_0^+ \in \mathit{cell}_0, $$

as 「$\mathbf{r}_0^-$」 = 「$\mathbf{w}1_1^- \cdot \mathbf{\check{\vee}}_1^+ \cdot \mathbf{r}_0^-$」, innocence requires $\mathbf{r}_0^- \cdot 1_0^+ \in \mathit{cell}_0$ as well, which is not the case. Of course, it is precisely the role of cell and lock to break innocence and transfer information across distinct copies – however, cell and lock remain P-visible in the sense of Definition 3.5. We now complete the interpretation of IA. Consider $\Gamma, x: \mathbf{ref} \vdash M: A$ with

$$ [[M]] \in \downarrow\uparrow\mathbf{-Strat}_i^{\mathit{wb,vis}}(\Gamma \& \mathbf{ref}, A) $$

omitting some brackets. Using the cartesian closed structure of $\downarrow\uparrow\mathbf{-Strat}_i^{\mathit{wb,vis}}$, we consider

$$ \Lambda_{\Gamma}^{!}([[M]]) \in \downarrow\uparrow\mathbf{-Strat}^{\mathit{wb,vis}}(\mathbf{!ref}, \mathbf{!\Gamma} \dashv A). $$

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

$$ [[\mathbf{newref} x:=n \mathbf{in} M]] = \Lambda_{\Gamma}^{!-1}(\Lambda_{\Gamma}^{!}([[M])) \odot \mathit{cell}_n) \in \downarrow\uparrow\mathbf{-Strat}_i^{\mathit{wb,vis}}(\Gamma, A) $$

$$ [[\mathbf{newsem} x:=n \mathbf{in} M]] = \Lambda_{\Gamma}^{!-1}(\Lambda_{\Gamma}^{!}([[M])) \odot \mathit{lock}_n) \in \downarrow\uparrow\mathbf{-Strat}_i^{\mathit{wb,vis}}(\Gamma, A). $$

This concludes the interpretation of IA in $\downarrow\uparrow\mathbf{-Strat}^{\mathit{wb,vis}}$. Adequacy proceeds as in [AM96], undisturbed by the slightly different technical setting of the present paper.

**Proposition 3.12 (Adequacy).** For any $\vdash M: \mathbb{U}$ in IA, $M \downarrow$ if and only if $[[M]] \downarrow$.
3.4.4. Full Abstraction. We now review the full abstraction result of [AM96]. The argument revolves around a fundamental factorisation theorem, stated as follows.

**Theorem 3.13 (Factorisation).** Let A be a type of IA, and $\sigma : \llbracket A \rrbracket$ be P-visible well-bracketed. Then, there is an innocent well-bracketed Inn($\sigma$) $\in \downarrow\uparrow$-Strat<sup>wb,inn</sup>(!ref, \llbracket A \rrbracket)$^*$ such that

$$ \sigma \approx \mathrm{Inn}(\sigma) \odot \mathrm{cell}_0, $$

and Inn($\sigma$) is finite if $\sigma$ is finite.

*Proof.* For any O-ending $sa^-$, we wish Inn($\sigma$) to act like $\sigma$, but as an innocent strategy it may only depend on $\lceil sa^- \rceil$. However, Inn($\sigma$) may also access the reference, so we will maintain the invariant that the reference contains (an encoding of) the full history, or more precisely of $\mathcal{P}(s)$. Between $\lceil sa^- \rceil$ and $\mathcal{P}(s)$, $\sigma$ knows the full play (up to symmetry).

Upon being called with $a^-$, Inn($\sigma$) reads $\mathcal{P}(s)$ from the reference, then stores $\mathcal{P}(sab)$ in the reference (for $sa^-b^+ \in \sigma$) and then plays b. See [AM96] for more details. □

Finiteness of Inn($\sigma$) follows the definition of finite innocent strategies from Section 3.3.1: having finitely many ($\cong$-equivalence classes of) P-ending P-views. However, finiteness of non-innocent strategies has not yet been defined. We define it now: a strategy in $\downarrow\uparrow$-Strat($A$) is finite iff the set of ($\cong$-equivalence classes of) P-ending plays of $\sigma$ is finite. Despite the common terminology, these two notions are distinct: an innocent strategy may be finite as an innocent strategy while being non-finite as a non-innocent strategy. This mismatch comes from the fact that these two notions both coincide with the domain-theoretic notion of compactness, but in the distinct domains $\downarrow\uparrow$-Strat<sup>wb,inn</sup>($A, B$) and $\downarrow\uparrow$-Strat<sup>wb</sup>($A, B$) (ordered by inclusion) for $--$arenas $A, B$. By Proposition 2.22, these statements involving $\cong$-equivalence classes may be instead phrased with plays with pointers.

From Theorem 3.13 and Proposition 3.11 it is direct that finite definability holds for IA. We can deduce immediately intensional full abstraction for IA, proved as Theorem 3.13.

**Theorem 3.14.** The model $\downarrow\uparrow$-Strat<sup>wb,vis</sup><sub>i</sub> is intensionally fully abstract for IA.

This is exactly as Theorem 3.10. However, in stark contrast with Theorem 3.10, for IA the fully abstract quotient category is effectively presentable. In fact, for $\sigma, \tau : \llbracket A \rrbracket$,

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

where comp($\sigma$) is the set of complete plays of $\sigma$, capturing the completed executions where both players act like P-visible well-bracketed strategies: a play is complete if it is well-bracketed, P-visible, O-visible (the dual to P-visibility, not detailed here), and such that every question has an answer. The result follows from finite definability for IA [AM96].

This effective fully abstract model of IA is one of the most striking results of game semantics. Observational equivalence in IA remains undecidable with bounded integers, at fourth order without recursion [Mur03] and second-order with recursion [Ong02] (of course, observational equivalence is obviously undecidable in the full language as it is Turing-complete). However, the model yielded sound and complete algorithms for observational equivalence on restricted fragments [GM03], starting the field of algorithmic game semantics.

3.5. **The Semantic Cube.** Abramsky's "semantic cube", often called the "Abramsky cube", starts with the observation that game semantics allows the interpretation of both control (i.e. callcc) and state in the same model, i.e. the same category.
**3.5.1. Control.** We have not given the interpretation of **callcc**, nor the corresponding full abstraction result [Lai97]. In fact, in the present technical setting, we cannot interpret **callcc**. This is due, in part, to the added conflict in arenas for basic datatypes with respect to standard HO games [HO00] – see Figures 6, 7, and 8. This conflict imposes that each question can be answered at most once, which is incompatible with **callcc**<fnref n="12" />. In fact:

**Proposition 3.15.** For any PCF type A, any innocent σ : [[A]] is also well-bracketed.

*Proof.* First, any innocent σ : [[A]] is well-bracketed iff its P-views are well-bracketed – see [Lai97] for a proof. Hence if σ is not well-bracketed, then there is a P-view

$$s_1 \dots q^{-,Q} \dots q^{-,Q} \dots a^{+,A}$$

where a answers the first q shown rather than the pending question, the second q shown. But this second $q^{-,Q}$ must be the initial move of a banged sub-arena in the interpretation of A, so we can play it again. And by innocence of σ, the following must be a play of σ:

$$s_1 \dots q^{-,Q} \dots q_i^{-,Q} \dots a^{+,A} q_{i+1}^{-,Q} \dots a^{+,A}$$

where both copies of a point to the first $q^{-,Q}$, absurd by *non-repetitive*.

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

This entails that in fact, Theorem 3.10 holds for $↓↑-\text{Strat}_i^{\text{inn}}$. But no such coincidence holds beyond innocent strategies: for Theorem 3.14 well-bracketing really is needed. In this paper we have adopted an interpretation of ground types incompatible with **callcc**. There is no technical obstacle to modelling **callcc** – one can simply drop conflicts in basic arenas and duplicate return values – but we prefer our design, closer to linear logic and the relational model (see Section 7.1.6). Furthermore, control operators will play no role in the present paper beyond the exposition of the scientific context.

**3.5.2. The Semantic Cube.** We temporarily consider, for the sake of the discussion, a setting with both control and state; say Murawski’s model for interference and control [Mur07], which is essentially equivalent (modulo the representation with pointers) to ours where basic arenas have no conflict and answers are replicated. Let us call it by **Vis**. There is

$$\text{PCF} + \text{interference} + \text{control} \rightarrow \text{Vis}$$

an adequate interpretation, so we can model a rich combination of effects; but that is not all. Indeed, there are four (intensional) full abstraction results:

**Theorem 3.16 (Semantic Cube).** We have four intensional full abstraction results:

<table><tr><td>Vis</td><td>is fully abstract for</td><td>PCF + interference + control</td></tr><tr><td>Vis + innocence</td><td>is fully abstract for</td><td>PCF + control</td></tr><tr><td>Vis + well-bracketing</td><td>is fully abstract for</td><td>PCF + interference</td></tr><tr><td>Vis + innocence + well-bracketing</td><td>is fully abstract for</td><td>PCF</td></tr></table>

We have reviewed two cases before, namely PCF (Theorem 3.10) and PCF + interference (Theorem 3.14). The full abstraction result for PCF + control is due to Laird [Lai97], while for PCF + interference + control appears in Murawski<fnref n="13" /> [Mur07].

<footnote n="12">¹²In addition to conflicts, the incompatibility with **callcc** comes from the fact that our interpretation of types only involves ! on arrows, and not on basic datatypes. To authorize control we should change e.g. the arena $\mathbb{B}$ to one with replicated answers, written (in the language of tensorial logic [MT10]) as $\neg!-(1 \oplus 1)$.</footnote>

<footnote n="13">¹³Murawski uses a different primitive for control, but the difference is superficial within IA.</footnote>
<figure><img src="image_40.png" /><figcaption>Figure 28: The Semantic Cube</figcaption></figure>

This “Semantic Cube”, drawn in Figure 28, expresses that the conditions on strategies
capture the behaviour generated by certain computational effects; or rather the *absence*
of certain effects. The achievement is noteworthy, as it is famously difficult to *combine*
semantic accounts of computational effects. But independently of purely semantic purposes,
this provides us with a microscope to study behaviourally interactions between effects in
programming languages. We demonstrate this with the following orthogonality property<sup>14</sup>
between interference and control which nicely illustrates the strength of game semantics:

**Theorem 3.17.** Let $\vdash_M A$ a term of PCF + interference + control. Assume that

(1) $M \sim N_1$ where $N_1$ is a term of PCF + interference,

(2) $M \sim N_2$ where $N_2$ is a term of PCF + control;

then $M \sim N$ where $N$ is a term of (an infinitary extension of) PCF.

*Proof.* Consider $[[M]] : A$. We have seen in Section 3.4.4 that for IA, strategies are indistinguishable iff they have the same *complete plays*. In the presence of control this phenomenon gets stronger: strategies are indistinguishable iff they have the *same plays* [Mur07]. Hence, $[[M]]$ is an innocent well-bracketed strategy (even though $M$ might internally use state and control). It is approximated by a sequence of finite innocent strategies which may be defined; but as the definability process is monotone this yields an infinitary PCF term. □

It is widely believed that in a version of PCF such as ours with a **let** construct, the innocent well-bracketed games model is **intensionally universal**, meaning that each computable innocent well-bracketed strategy is definable<sup>15</sup>. With such a result, Theorem 3.17 would generalize to conclude the existence of simply a term of PCF, rather than an infinitary term.

**3.6. Towards Concurrency.** The reader may rightly complain that Figure 28 is not a "semantic cube", only a "semantic square". Though we focused on control and interference, there are fully abstract models of languages featuring general references [AHM98], exceptions [Lai01a], coroutines [Lai04], non-determinism [HM99], probabilistic choice [DH00], concurrency [Lai01b, GM08], and others. One imagines that the methodology above generalizes, and that the big "syntactic hypercube" of these effects is matched by a "semantic hypercube".

However, there is no such “semantic hypercube”: the works cited above rely on a priori incompatible formal settings. In this paper, we present steps towards such a semantic

<footnote n="14">¹⁴We learnt of it from a talk by Paul Levy in 2014 [Lev14].</footnote>

<footnote n="15">¹⁵Hyland and Ong have a *extensional universality theorem* [HO00], i.e. up to observational equivalence. *Intensional universality* does not appear anywhere in call-by-name, although it does in call-by-value [MT13].</footnote>
<figure><img src="image_41.png" /><figcaption>Figure 29: Operational content of a non-alternating play</figcaption></figure>

hypercube. More precisely we aim to *disentangle parallelism and interference* in the same sense as the “Abramsky cube” disentangles control and interference, i.e. we must answer:

**Question.** Build a model $\rightarrow$-Strat with notions of parallel innocence and sequentiality s.t.:

$\rightarrow$-Strat is fully abstract for IA$_{\parallel}$,
$\rightarrow$-Strat + parallel innocence is fully abstract for PCF$_{\parallel}$,
$\rightarrow$-Strat + sequentiality is fully abstract for IA,
$\rightarrow$-Strat + parallel innocence + sequentiality is fully abstract for PCF,

all of these being intensional full abstraction results.

The model should be fully abstract for IA$_{\parallel}$, link with $\downarrow\uparrow$-Strat$_{i}^{wb,inn}$ and $\downarrow\uparrow$-Strat$_{i}^{wb}$ (respectively fully abstract for PCF and IA), but also support a notion of parallel innocence yielding full abstraction for PCF$_{\parallel}$. It is natural to start with a simple non-alternating variant of $\downarrow\uparrow$-Strat, inspired by Ghica and Murawski's fully abstract games model for IA$_{\parallel}$ [GM08].

### 3.6.1. *Non-alternating plays and strategies.*
We simply relax alternation in Definition 2.7.

**Definition 3.18.** A non-alternating play on $--arena A$ is $s = s_1 \dots s_n$ which is:

valid: $\forall 1 \le i \le n$, $\{s_1, \dots, s_i\} \in \mathcal{C}(A)$,
non-repetitive: $\forall 1 \le i, j \le n$, $s_i = s_j \implies i = j$,
negative: $n \ge 1 \implies \text{pol}(s_1) = -$.

We write $\mathcal{O}$-Plays($A$) for the set of non-alternating plays on $A$.

The notation (inspired by *template games* [Mel19]), is intended to suggest that whereas alternating plays in $\downarrow\uparrow$-Plays($A$) transition between two states O and P determining which player has control, in $\mathcal{O}$-Plays($A$) there is only one state, in which either player may play. The intuition is simple: as several threads might be running in parallel, their interleaving breaks alternation. We show in Figure 29 a non-alternating play on $\llbracket (U \to U) \to N \rrbracket$, using the same conventions as previously. Resting on the same computational intuitions as before, we show for each move a representation of the matching computational state of a term realizing that play. The figure illustrates that even IA, a sequential language, allows non-alternating plays, as the environment can evaluate subterms in parallel. After the third and fourth moves, two subterms are being evaluated in parallel: $r := 1$ and $!r$, causing a *data race*.

As before, we may now define *strategies* as certain sets of plays.
**Definition 3.19.** A non-alternating strategy $\sigma : A$, is $\sigma \subseteq \mathcal{O}\text{-Plays}(A)$ which is:

non-empty: $\varepsilon \in \sigma$

prefix-closed: $\forall s \sqsubseteq s' \in \sigma, s \in \sigma$

receptive: $\forall s \in \sigma, sa^- \in \mathcal{O}\text{-Plays}(A) \implies sa \in \sigma$

courteous: $\forall sabt \in \sigma, sb \in \mathcal{O}\text{-Plays}(A), (\text{pol}(b) = - \lor \text{pol}(a) = +) \implies sbat \in \sigma$

A non-alternating prestrategy is only required to satisfy *non-empty* and *prefix-closed*.

Let us compare with Definition 2.8. Besides moving to non-alternating plays, we remove determinism. Of course, this is natural since the interleaving semantics of even a pure parallel language represents non-deterministically the choices of the scheduler. The new condition added is *courtesy*, it corresponds to the *saturation* condition of [GM08] (the name “courtesy” is imported from [MM07]). Courtesy expresses that the model is asynchronous. If one has $sa^+b \in \sigma$, there is an execution of $\sigma$ where it plays $a$, then we observe $b$ (of any polarity). But if the surrounding computing environment is asynchronous, nothing forces $a$ to be directly observable by Opponent – $a$ might get stuck in a buffer, in the network, etc. So then, courtesy imposes that $\sigma$ should be *stable under asynchronous delays*: if $sa^+b \in \sigma$ and there is no dependency from $a$ to $b$ in the arena, then $a$ can be postponed after $b$ in $\sigma$.

### 3.6.2. *Well-bracketing*
We introduce *well-bracketing* for non-alternating strategies. In Ghica and Murawski's games, all plays are *well-bracketed* in the sense that they satisfy two conditions, dubbed *fork* and *wait*. We adapt and introduce these conditions now.

**Definition 3.20.** For a `--arena` $A$, $s \in \mathcal{O}\text{-Plays}(A)$ is **well-bracketed** if for any $s' \sqsubseteq s$,

*fork*: if $s' = \dots q^Q \dots m$ with $q \to_A m$, $q$ must be unanswered before $m$ is played,

*wait*: if $s' = \dots q^Q \dots a^A$ with $q \to_A a$, all questions justified by $q$ must be answered.

This differs from the simple *well-bracketing* of alternating plays (Definition 3.2). In a non-alternating setting it does not make sense to refer to the last unanswered question as it might originate in a different thread than the one the Player move to be played belongs to. Instead, this condition forces plays to follow the following protocol: a question, as long as it is not answered, may prompt (i.e. justify) other questions. It can only be answered once all the questions it justified are answered, and then it will not be able to justify anything further. For instance, the play of Figure 29 is *not* well-bracketed: the fourth move $\checkmark_0$ causes a failure to *wait* because it is justified by $q_0^+$, although the latter has justified $q_{0,0}$ as of yet unanswered. If we were to permute the moves $q_{0,0}$ and $\checkmark_0$ then $q_{0,0}$ would cause a failure to *fork* as it would be justified by a question that is already answered.

Rather than imposing this condition on all plays, we impose it on strategies.

**Definition 3.21.** Let $\sigma : A$ be a non-alternating strategy.

It is **well-bracketed** iff for all $sa^+ \in \sigma$, if $s$ is well-bracketed then $sa$ is well-bracketed.

The play of Figure 29 belongs to a well-bracketed strategy: Opponent breaks well-bracketing first. This is a slight difference with Ghica and Murawski's model: we observe all dynamic behaviour of a program of $IA_\parallel$, even that not reachable via a context of $IA_\parallel$. Of course, it is always possible to restrict to well-bracketed plays without cutting any Player behaviour (i.e. the strategy is cut at Opponent extensions, not Player extensions).
<figure><img src="image_42.png" /><figcaption>Figure 30: Two (pointer representation) of plays in a parallel innocent strategy</figcaption></figure>

### 3.6.3. Limitations.
The proximity of non-alternating strategies to both ↓↑-Strat and Ghica and Murawski's model make them a tempting foundation for this paper. However, they have two limitations, both subtly related to their inability to record the branching structure.

Firstly, *parallel innocence* requires adequate causal structures, as illustrated by the following example. Is there a parallel innocent strategy that includes the two plays with pointer representation in Figure 30? Is there a program of PCF$_{‖}$ that may realize both? Traditional innocence forbids that, because in a sequential program, both plays must be visiting the same piece of syntax and obtain the same result. In PCF$_{‖}$ though, the program

$$ \lambda f^{\mathbb{B} \to \mathbb{U}}. \text{let} \left( \begin{array}{l} x = f \mathbf{tt} \\ y = f \mathbf{ff} \end{array} \right) \text{in } x; y : (\mathbb{B} \to \mathbb{U}) \to \mathbb{U} $$

indeed realizes these two plays, corresponding to the evaluation of distinct threads. A deterministic innocent strategy is determined by (the pointer representation of) its *P-views*, so we may see the set of P-views as a witness for innocence. Analogously, what structure may witness that a non-alternating strategy is innocent? In fact, what is missing from the two P-views of Figure 30 is the *branching structure*, keeping these two P-views apart and recording how they are linked to each other. It has already been observed [CCW14, TO15] that *non-deterministic innocence* may be defined by replacing sets of P-views, as witnesses for innocence, with *trees* recording the non-deterministic branching information. Here we must do the same, but instead record the branching structure pertaining to *parallelism* as well – which plain non-alternating strategies cannot capture adequately [CC16].

Secondly, it is unclear how to endow non-alternating strategies with appropriate notions of *symmetry* and *uniformity* as in Definition 2.13. Our attempts in generalizing Definition 2.13 ended up suffering from various pathologies, typically uniformity not being preserved by hiding. The tension with hiding comes from a play $s \in \tau \odot \sigma$ being witnessed by distinct interactions between $\sigma$ and $\tau$ – this suggests again the need for an explicitely branching structure, as then one recovers a *unique witness* property. For these two reasons, we move from plain non-alternating strategies to *thin concurrent games*. We will, however rely on:

**Proposition 3.22.** There is a symmetric monoidal closed category with products ⏎-Strat$^{wb}$, with objects --arenas, and morphisms well-bracketed non-alternating strategies on $A \dashv B$.

*Proof.* The constructions play a minor role in this paper and are very similar to the alternating case, so we omit them. Some details of the construction appear in Appendix C. □

These limitations call for a more intensional setting, representing explicitely the parallel and non-deterministic branching structures. To our knowledge, the only games setting in the literature sufficiently expressive and mature is *thin concurrent games*, one of the possible enrichments with symmetry of the concurrent strategies of Rideau and Winskel [RW11].
## 4. CAUSAL FULL ABSTRACTION FOR IA_//

Thin concurrent games were first introduced in [CCW15], but the detailed construction (along with significant improvements and simplifications) is presented in [CCW19].

In this section, we start with an introduction to thin concurrent games. We omit detailed constructions (which appear in [CCW19]), but we do attempt to give a self-contained introduction, in particular providing required reasoning principles. Then, we apply this setting to give a fully abstract model for IA_//, the causal sibling of Ghica and Murawski’s model [GM08]. In the concurrent games literature, strategies are often referred to as concurrent strategies. Here we prefer causal strategies to better distinguish them with non-alternating strategies, which also represent concurrent behaviour.

### 4.1. Arenas and causal strategies.
First, we must refine the symmetry on arenas.

#### 4.1.1. Polarized symmetry.
Arenas for causal strategies in [CCW19] require the following:

**Definition 4.1.** For A an arena with isomorphism family $\mathcal{S}(A)$, a **polarized decomposition** of $\mathcal{S}(A)$ comprises isomorphism families $\mathcal{S}_-(A)$, $\mathcal{S}_+(A)$ included in $\mathcal{S}(A)$, s.t.:

(1) If $\theta \in \mathcal{S}_-(A) \cap \mathcal{S}_+(A)$, then $\theta$ is an identity bijection,

(2) If $\theta \in \mathcal{S}_-(A)$ and $\theta \subseteq \theta' \in \mathcal{S}(A)$, then $\theta' \in \mathcal{S}_-(A)$,

(3) If $\theta \in \mathcal{S}_+(A)$ and $\theta \subseteq \theta' \in \mathcal{S}(A)$, then $\theta' \in \mathcal{S}_+(A)$.

where $\subseteq^p$ means that only (pairs of) events of polarity $p$ are added.

If $\theta : x \cong_A y$ and $\theta \in \mathcal{S}_-(A)$, we write $\theta : x \cong_A^- y$ and call $\theta$ a **negative symmetry**. Likewise, $\theta : x \cong_A^+ y$ means that $\theta : x \cong_A y$ with $\theta \in \mathcal{S}_+(A)$, called a **positive symmetry**.

Arenas with a polarized decomposition are thin concurrent games<fnref n="16" /> in the sense of [CCW19]. Intuitively, negative symmetries (resp. positive) reindex Opponent (resp. Player) moves – though Definition 4.1 does not involve “copy indices”. By Lemma 3.19 from [CCW19], any $\theta : x \cong_A z$ factors uniquely as $\theta_+ \circ \theta_-$, with $\theta_+$ positive and $\theta_-$ negative.

#### 4.1.2. Constructions on arenas.
First we extend the arena constructions accordingly.

For $U, B$ and $N$, all isomorphism families are reduced to identity bijections between configurations. For the dual of an arena $A$, then for all symmetry $\theta : x \cong_A y$,

$$ \theta : x \cong_{A^{\perp}}^{+} y \Leftrightarrow \theta : x \cong_{A}^{-} y, $$

$$ \theta : x \cong_{A^{\perp}}^{-} y \Leftrightarrow \theta : x \cong_{A}^{+} y. $$

For parallel composition and product, the sub-symmetries are inherited as for the full symmetry in Section 2.2.1 applying to the positive and negative isomorphism families separately. For the arrow, for $x, y \in \mathcal{C}(A \to B)$ and $\theta : x \simeq y$ an order-isomorphism, we set $\theta \in \mathcal{S}_+(A \to B)$ iff $\chi_{A,B} \theta \in \mathcal{S}_+(A^{\perp} \parallel B)$; and $\theta \in \mathcal{S}_-(A \to B)$ iff $\chi_{A,B} \theta \in \mathcal{S}_-(A^{\perp} \parallel B)$.

The most interesting construction is the exponential. Recall that a symmetry in $!A$ is

$$ \theta : \begin{array}{l} \parallel_{n \in N} x_n \cong \parallel_{n \in N} y_n \\ (n, a) \mapsto (\pi(n), \theta_n(a)) \end{array} $$

for some permutation $\pi \in \mathcal{S}(N)$ and for some family $(\theta_n)_{n \in N}$ with $\theta_n : x_n \cong_A y_{\pi(n)}$ for all $n \in N$. First we set $\theta \in \mathcal{S}_-(!A)$ iff for all $n \in N$, $\theta_n : x_n \cong_A^- y_{\pi(n)}$. Finally, we set $\theta \in \mathcal{S}_+(!A)$ iff for all $n \in N$ such that $x_n$ is non-empty, we have $\pi(n) = n$, and $\theta_n : x_n \cong_A^+ y_n$.

<footnote n="16">¹⁶Thin concurrent games in [CCW19] are more general, e.g. they might not be alternating or forestial.</footnote>
Why does !A treat differently the positive and negative isomorphism families? The permutation $\pi(-)$ corresponds to reindexing the minimal events of !A. Because the exponential construction is intended to apply to negative games, $\pi(-)$ reindexes negative moves. But symmetries in $\mathscr{S}_+(!A)$ can only reindex positive moves, so $\pi(-)$ must be the identity. In contrast, symmetries in $\mathscr{S}_-(!A)$ can perform any reindexing on the minimal events. This intuition is further solified by the extension of concrete arenas to these polarized sub-isomorphism families. This will not be required until much later, so it only appears in Section 7.3.1 – but it might still be helpful for the reader to consult it now.

4.1.3. Causal strategies. In contrast with traditional game models, a causal strategy is one global object: an event structure. It presents all execution threads together, with explicit information on how these executions relate via parallel and non-deterministic branching.

**Definition 4.2.** A causal prestrategy $\sigma$: A comprises an ess ($|\sigma|$, $\leq_{\sigma}$, $\#_{\sigma}$, $\mathscr{S}(\sigma)$) with
$$ \partial: |\sigma| \to |A| $$

a function called the **display map**, subject to the following conditions:

*rule-abiding:* for all $x \in \mathscr{C}(\sigma)$, $\partial(x) \in \mathscr{C}(A)$,

*locally injective:* for all $s_1, s_2 \in x \in \mathscr{C}(\sigma)$, if $\partial(s_1) = \partial(s_2)$ then $s_1 = s_2$,

*symmetry-preserving:* for all $\theta \in \mathscr{S}(\sigma)$, $\partial(\theta) = \{(\partial(s_1), \partial(s_2)) \mid (s_1, s_2) \in \theta\} \in \mathscr{S}(A)$,

*~-receptive:* for all $\theta: x \cong_{\sigma} y$, and extensions $x \vdash_{\sigma} s_1^-$, $\partial(\theta) \vdash_{\mathscr{S}(A)} (\partial(s_1^-), a_2^-)$, there is a unique $s_2^- \in |\sigma|$ s.t. $\theta \vdash_{\mathscr{S}(\sigma)} (s_1^-, s_2^-)$ and $\partial(s_2^-) = a_2^-$,

*thin:* for all $\theta: x \cong_{\sigma} y$, and extension $x \vdash_{\sigma} s_1^+$, there is a unique extension $y \vdash_{\sigma} s_2^+$ such that $\theta \vdash_{\mathscr{S}(\sigma)} (s_1^+, s_2^+)$.

Additionally, we say that $\sigma$ is a **causal strategy** if it satisfies the further two conditions:

*negative:* for all $s \in |\sigma|$, if $s$ is minimal then $s$ is negative,

*courteous:* for all $s_1 \to_{\sigma} s_2$, if $\text{pol}(s_1) = +$ or $\text{pol}(s_2) = -$ then $\partial(s_1) \to_A \partial(s_2)$,

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

As a convention, causal strategies are ranged over by symbols in bold font, as in e.g. $\sigma, \tau$. We disambiguate some notations used in the definition. First, $\sigma$ implicitly comes with polarities, imported from A as $\text{pol}_{\sigma}(s) = \text{pol}_{A}(\partial(s))$. We also used the enabling relation on isomorphism families, defined by $\theta \vdash_{\mathscr{S}(A)} (a_1, a_2)$ iff $(a_1, a_2) \notin \theta$ and $\theta \uplus \{(a_1, a_2)\} \in \mathscr{S}(A)$.

Conditions *rule-abiding*, *locally injective* and *symmetry-preserving* together amount to $\partial$ being a **map of event structures with symmetry** [Win07]. Conditions *courteous* and *receptive* play the same role as in Definition 3.19. The condition *~-receptive* forces strategies to treat uniformly any pairs of Opponent events symmetric in the game. Finally, *thin* forces strategies to pick one canonical representative up to symmetry for positive moves. For further explanations and discussions on those conditions, the reader is directed to [CCW19].

Causal strategies and non-alternating strategies differ fundamentally in how the concurrent behaviour is represented. While non-alternating strategies present observable execution traces, causal strategies present the causal constraints underlying the observed behaviour. In Figure 31, we present a causal strategy, corresponding to a linear version of Figure 29. In this diagram and others further on, we draw $\sigma: A$ by picturing the event structure $\sigma$ with events displayed as their image through $\partial_{\sigma}$. Whenever possible, we keep the convention to draw moves under the corresponding type component. The causal dependency $\leq_{\sigma}$ is
<figure><img src="image_43.png" /><figcaption>Figure 31: A causal strategy</figcaption></figure>

<figure><img src="image_44.png" /><figcaption>Figure 32: Two augmentations of Figure 31</figcaption></figure>

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

pictured via its immediate dependency relation $\rightarrow_{\sigma}$. As with arenas, we show immediate conflicts (i.e. not inherited) as wiggly lines. As in plays, we denote by dotted lines the immediate causal dependency in the arena A: for $s \in |\sigma|$, either $\partial_{\sigma}(s)$ is minimal in A, or there is a unique $s' \in |\sigma|$ such that $\partial_{\sigma}(s') \rightarrow_A \partial_{\sigma}(s)$; in which case the diagram has a dotted line between the events representing s and s'. Borrowing earlier terminology, we refer to s' as the **justifier** of s. Finally, the symmetry $\mathcal{S}(\sigma)$ is not shown at all (of course, for Figure 31 it would remain trivial). Indeed it is hard to represent, but also we regard it as not being part of the pertinent operational structure: its mere existence witnesses uniformity.

Figure 31 presents, in one diagram, the full behaviour of the program of Figure 29 under linear execution contexts. Drawing a strategy fully in this way is sometimes challenging. It is often convenient to refer to – and draw – consistent fragments of a causal strategy: an **augmentation** of $\sigma$ is any $(x, \leq_x)$ where $x \in \mathcal{C}(\sigma)$ and $\leq_x$ is the partial order inherited from $\leq_{\sigma}$. For instance the two maximal augmentations of Figure 31 yield the diagrams of Figure 32. In this case, the two configurations correspond to the two resolutions of the date race described with Figure 29: if the write wins, the read yields 1 and depends on $\mathbf{q}^{-}$ (which triggered the write). If the read wins, we read 0 and the write acknowledgment depends on $\mathbf{\checkmark}^{-}$ (which triggered the read). However, this representation of a strategy via its augmentations is partial: it forgets the explicit non-deterministic branching.

### 4.1.4. Non-alternating unfolding.
Causal strategies generate non-alternating strategies:

**Proposition 4.3.** Consider A a $--$arena, and $\sigma$: A a causal strategy.

The non-alternating unfolding of $\sigma$ is (with $\partial_{\sigma}$ applied to plays move-by-move):

$$ \mathcal{C}-\text{Unf}(\sigma) = \partial_{\sigma}(\mathcal{C}-\text{Plays}(\sigma)). $$

Thus defined, $\mathcal{C}-\text{Unf}(\sigma)$: A is a non-alternating strategy on A.

*Proof.* Non-empty and prefix-closed are obvious. For receptive, take $s \in \mathcal{C}-\text{Unf}(\sigma)$ s.t. $sa^- \in \mathcal{C}-\text{Plays}(A)$. By definition, there is $t \in \mathcal{C}-\text{Plays}(\sigma)$ s.t. $s = \partial_{\sigma}(t)$. Thus $t$, written

$$ t = t_1 \dots t_n \in \mathcal{C}-\text{Plays}(\sigma), $$

is such that for all $1 \leq i \leq n$, $\{t_1, \dots, t_i\} \in \mathcal{C}(\sigma)$, and is also non-repetitive and negative. Let us write $x = \{t_1, \dots, t_n\}$. Then, $\partial_{\sigma}(x) = \{s_1, \dots, s_n\} \in \mathcal{C}(A)$, and since $sa^- \in \mathcal{C}-\text{Plays}(A)$ we have $\partial_{\sigma}(x) \vdash_A a^-$. By receptivity of $\sigma$, there is (a unique) $m \in |\sigma|$ such that $x \vdash_{\sigma} m$ and $\partial_{\sigma}(m) = a$. It is then direct that $tm \in \mathcal{C}-\text{Plays}(\sigma)$, witnessing $sa \in \mathcal{C}-\text{Unf}(\sigma)$ as required.

For courteous, consider $s_1a\bar{s}_2 \in \mathcal{C}-\text{Unf}(\sigma)$ s.t. $\text{pol}(a) = +$ or $\text{pol}(b) = -$, and $s_1b \in \mathcal{C}-\text{Plays}(A)$. By definition, there is $t_1m\bar{n}t_2 \in \mathcal{C}-\text{Plays}(\sigma)$ s.t. $s_1a\bar{s}_2 = \partial_{\sigma}(t_1m\bar{n}t_2)$. We claim
that $x = |t_1n| \in \mathscr{C}(\boldsymbol{\sigma})$. We know that $|t_1mn| \in \mathscr{C}(\boldsymbol{\sigma})$; so $x$ is consistent. If it is not down-closed, necessarily $m \dashv_{\boldsymbol{\sigma}} n$. So, by courtesy of $\boldsymbol{\sigma}$, $a \dashv_A b$; contradicting $s_1b \in \mathcal{C}\text{-Plays}(A)$. Thus $|t_1n| \in \mathscr{C}(\boldsymbol{\sigma})$ from which we deduce $t_1nmt_2 \in \mathcal{C}\text{-Plays}(\boldsymbol{\sigma})$, so $s_1bas_2 \in \mathcal{C}\text{-Unf}(\boldsymbol{\sigma})$. $\square$

For instance, the non-alternating play in Figure 29 is in the unfolding of the causal
strategy in Figure 31. This extraction of a non-alternating strategy is an instance of the usual
relationship between interleaving and “truly concurrent” models for concurrency. In this
paper this relationship will in particular allow us to import well-bracketing from $\mathcal{C}\text{-Strat}^{\text{wb}}$.

**Definition 4.4.** Consider $\boldsymbol{\sigma} : A$ a causal strategy on $--$arena $A$.

We say that **σ** is **well-bracketed** if ℵ-Unf(**σ**) : A is well-bracketed.

4.2. **A Category of Causal Strategies.** We now start building the categorical operations on causal strategies, aiming at a Seely category $\dashv_{\sigma}$-Strat. We first focus on composition.

For --arenas A and B, a causal strategy from A to B is a causal strategy

$$
\sigma : A^{\perp} \parallel B,
$$

in the sequel we also write $A \vdash B$ for $A^{\perp} \parallel B$. This is unlike for $\downarrow\uparrow$-Strat and $\mathcal{C}\text{-Strat}$ introduced earlier, for which morphisms from $A$ to $B$ were defined as strategies on $A \dashv \mathcal{O} B$. We do this to keep close to [CCW19]. When linking with $\downarrow\uparrow$-Strat and $\mathcal{C}\text{-Strat}$ we shall deal with this mismatch, but that will not cause us too much trouble<fnref n="17" />.

Composition of causal strategies is more elaborate than for play-based strategies. We
define it in several stages. Fix $\boldsymbol{\sigma} : A \vdash B$ and $\boldsymbol{\tau} : B \vdash C$ two causal (pre)strategies.

4.2.1. *Synchronization*. For configurations $x^{\boldsymbol{\sigma}} \in \mathscr{C}(\boldsymbol{\sigma})$, $x^{\boldsymbol{\tau}} \in \mathscr{C}(\boldsymbol{\tau})$, as a convention we write

$$
\hat{\partial}_{\sigma}(x^{\sigma}) = x_{A}^{\sigma} \parallel x_{B}^{\sigma} \in \mathcal{C}(A \vdash B), \quad \hat{\partial}_{\tau}(x^{\tau}) = x_{B}^{\tau} \parallel x_{C}^{\tau} \in \mathcal{C}(B \vdash C),
$$

for the corresponding projections to the game. In defining composition, the first stage is to
capture when such configurations $x^{\sigma} \in \mathscr{C}(\sigma)$ and $x^{\tau} \in \mathscr{C}(\tau)$ may successfully *synchronise*.

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

$$
\varphi_{x^{\boldsymbol{\sigma}}, x^{\boldsymbol{\tau}}} : x^{\boldsymbol{\sigma}} \parallel x_C^{\boldsymbol{\tau}} \stackrel{\partial_{\sigma} \parallel x_C^{\boldsymbol{\tau}}}{\sim} x_A^{\boldsymbol{\sigma}} \parallel x_B \parallel x_C^{\boldsymbol{\tau}} \stackrel{x_A^{\boldsymbol{\sigma}} \parallel \partial_{\tau}^{-1}}{\sim} x_A^{\boldsymbol{\sigma}} \parallel x^{\boldsymbol{\tau}},
$$

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

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

defined on (the graph of) $\varphi_{x^{\sigma}, x^{\tau}}$ by importing causal constraints of $\sigma$ and $\tau$, is acyclic.

Two matching $x^{\sigma} \in \mathscr{C}(\sigma)$, $x^{\tau} \in \mathscr{C}(\tau)$ agree on the state reached in $B$. By local injectivity of $\partial_{\sigma}$ and $\partial_{\tau}$, this induces a bijection as above, thought of as the induced synchronization between events of $x^{\sigma}$ and $x^{\tau}$ that match in $B$. But this is not enough to capture a sensible notion of execution: some matching pairs might not be reachable, in the sense that $\sigma$ and $\tau$ impose incompatible constraints as to the order in which the state should be reached. To illustrate this we show in Figures 33 and 34 two attempted synchronizations between configurations of the strategy of Figure 31 and the causal strategy for the identity $\lambda x^{\mathcal{U}} x$. In

<footnote n="17">¹⁷Plays on $A \dashv B$ carry more information than on $A \vdash B$, namely the justifier for initial moves in A.
With causal strategies, that information may be read back from the causal structure. See Section 4.3.2.</footnote>
<figure><img src="image_46.png" /><figcaption>Figure 33: Matching, secured</figcaption></figure>

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

both cases, the configurations are matching. In Figure 33, the synchronization is successful and yields causally compatible pairs of configurations. However, in Figure 34 the induced bijection is not *secured*: the two strategies impose opposite constraints as to the order in which the two ✓ moves are to be played. Thus, this synchronization fails. For us, this will entail that the identity $\lambda x^U.x$ may only synchronize successfully with the augmentation of the program of Figure 29 appearing in Figure 33 – so that the only final result is 1.

### 4.2.2. Interaction.
But we must present the interaction of $\sigma$ and $\tau$ as an event structure. More specifically, it should be an event structure with symmetry along with a display map:

**Definition 4.6.** A pre-interaction on A, B, C is an ess $\boldsymbol{\mu} = (|\boldsymbol{\mu}|, \leq_{\boldsymbol{\mu}}, \#_{\boldsymbol{\mu}}, \mathcal{S}(\boldsymbol{\mu}))$ with
$$ \partial : |\boldsymbol{\mu}| \to |A| \parallel |B| \parallel |C| $$

a display map subject to the following conditions:

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

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

*symmetry-preserving:* for all $\theta \in \mathcal{S}(\boldsymbol{\mu})$, $\partial(\theta) \in \mathcal{S}(A \parallel B \parallel C)$,

i.e. $\partial : \boldsymbol{\mu} \to A \parallel B \parallel C$ is a map of event structures with symmetry.

An **isomorphism** between pre-interactions $\boldsymbol{\mu}, \boldsymbol{\nu}$ on A, B, C is an isomorphism $f : \boldsymbol{\mu} \cong \boldsymbol{\nu}$ in the category of event structures with symmetry, commuting with the display maps, i.e. $\partial_{\boldsymbol{\nu}} \circ f = \partial_{\boldsymbol{\mu}}$. The **interaction** between $\boldsymbol{\sigma}$ and $\boldsymbol{\tau}$ is a pre-interaction whose configurations correspond *exactly* with pairs of causally compatible configurations $x^{\boldsymbol{\sigma}} \in \mathcal{C}(\boldsymbol{\sigma})$, $x^{\boldsymbol{\tau}} \in \mathcal{C}(\boldsymbol{\tau})$:

**Proposition 4.7.** There is a pre-interaction $\boldsymbol{\tau} \circledast \boldsymbol{\sigma}$, the **interaction** of $\boldsymbol{\sigma}$ and $\boldsymbol{\tau}$, with

$$ (- \circledast -) : \{(x^{\boldsymbol{\tau}}, x^{\boldsymbol{\sigma}}) \in \mathcal{C}(\boldsymbol{\tau}) \times \mathcal{C}(\boldsymbol{\sigma}) \mid x^{\boldsymbol{\sigma}} \text{ and } x^{\boldsymbol{\tau}} \text{ are causally compatible}\} \cong \mathcal{C}(\boldsymbol{\tau} \circledast \boldsymbol{\sigma}) $$

an order-iso (with causally compatible pairs ordered by component-wise inclusion) satisfying

$$ \partial_{\boldsymbol{\tau} \circledast \boldsymbol{\sigma}}(x^{\boldsymbol{\tau}} \circledast x^{\boldsymbol{\sigma}}) = x_{A}^{\boldsymbol{\sigma}} \parallel x_{B} \parallel x_{C}^{\boldsymbol{\tau}} $$

for all $x^{\boldsymbol{\sigma}} \in \mathcal{C}(\boldsymbol{\sigma})$ and $x^{\boldsymbol{\tau}} \in \mathcal{C}(\boldsymbol{\tau})$ causally compatible.

In particular, any $z \in \mathcal{C}(\boldsymbol{\tau} \circledast \boldsymbol{\sigma})$ is written uniquely as $x^{\boldsymbol{\tau}} \circledast x^{\boldsymbol{\sigma}}$ for $x^{\boldsymbol{\sigma}} \in \mathcal{C}(\boldsymbol{\sigma})$ and $x^{\boldsymbol{\tau}} \in \mathcal{C}(\boldsymbol{\tau})$. Thus, $\mathcal{C}(\boldsymbol{\tau} \circledast \boldsymbol{\sigma})$ may be regarded as the subset of $\mathcal{C}(\boldsymbol{\sigma}) \times \mathcal{C}(\boldsymbol{\tau})$ restricted to those of the matching pairs which cause no deadlock. In fact, this property almost suffices
<figure><img src="image_47.png" /><figcaption>Figure 35: Example of an interaction</figcaption></figure>

to characterise the interaction uniquely – to complete the picture, we must also consider symmetries. Because display maps preserve symmetry, for $\theta^\sigma \in \mathcal{S}(\sigma)$ and $\theta^\tau \in \mathcal{S}(\tau)$,

$$ \partial_{\sigma}(\theta^{\sigma}) = \theta_{A}^{\sigma} \parallel \theta_{B}^{\sigma}, \quad \partial_{\tau}(\theta^{\tau}) = \theta_{B}^{\tau} \parallel \theta_{C}^{\tau}, $$

and we can say that $\theta^\sigma$ and $\theta^\tau$ are **matching** if $\theta_B^\sigma = \theta_B^\tau$, and **causally compatible** if $\mathrm{dom}(\theta^\sigma)$, $\mathrm{dom}(\theta^\tau)$ are causally compatible – or, equivalently, $\mathrm{cod}(\theta^\sigma)$ and $\mathrm{cod}(\theta^\tau)$ are.

Taking into account symmetry, we may strengthen Proposition 4.7 to:

**Proposition 4.8.** There is a pre-interaction $\tau \circledast \sigma$, unique up to iso, such that there are

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

$$ (- \circledast -) : \{ (\theta^\tau, \theta^\sigma) \in \mathcal{S}(\tau) \times \mathcal{S}(\sigma) \mid \theta^\sigma, \theta^\tau \text{ causally compatible} \} \simeq \mathcal{S}(\tau \circledast \sigma) $$

order-isomorphisms commuting with dom and cod, and satisfying

$$ \partial_{\tau \circledast \sigma}(\theta^{\tau} \circledast \theta^{\sigma}) = \theta_{A}^{\sigma} \parallel \theta_{B}^{\sigma} \parallel \theta_{C}^{\tau} $$

for all $\theta^\sigma \in \mathcal{S}(\sigma)$ and $\theta^\tau \in \mathcal{S}(\tau)$ causally compatible.

*Proof.* Follows from the characterisation of the interaction as a pullback, whose projections

$$ \sigma \parallel C \xleftarrow{\Pi_{\sigma}} \tau \circledast \sigma \xrightarrow{\Pi_{\tau}} A \parallel \tau $$

are maps of event structures with symmetry [CCW19] – see Appendix D.2.1 for details. $\square$

There is some redundancy in this statement: first, the action of $(- \circledast -)$ on configurations coincides with that on identity symmetries. Reciprocally, one can actually prove that the action of $(- \circledast -)$ on symmetries, if it exists, is uniquely determined by that on configurations – so the fact that $(- \circledast -)$ extends to symmetries is property rather than structure. Nevertheless, in the sequel, we often find convenient to perform the constructions on symmetries explicitly. Altogether, this characterises the interaction in terms of its states and symmetries.

But there is also an alternative, event-based view: an individual event $m \in |\tau \circledast \sigma|$ may be regarded as a synchronization between its projections $\Pi_\sigma(m) \in |\sigma| \parallel C|$ and $\Pi_\tau(m) \in |A| \parallel \tau|$. But we warn against the misleading idea that $m \in |\tau \circledast \sigma|$ is determined by these projections: intuitively, there is one event in $\tau \circledast \sigma$ for each pair $(s, t)$ of synchronizable events, and each distinct way to reach $s$ and $t$ conjointly in $\sigma$ and $\tau$. A simple example appears in Figure 35 (ignoring for now the $l/r$ annotation and the part in grey): the final two copies of $\checkmark$ have the same projections, but a different causal history. Though we shall not unfold the concrete construction of the interaction [CCW19], it might nonetheless help the reader to have an idea of what its events are concretely defined to be. For $x^\sigma \in \mathcal{C}(\sigma)$ and $x^\tau \in \mathcal{C}(\tau)$ causally compatible, the reflexive transitive closure of $\langle \rangle$ (see Definition 4.5) yields a partial
order $\leq_{x\sigma,x\tau}$ on (the graph of) $\varphi_{x\sigma,x\tau}$. The events of $\tau \circled{\sigma}$ are then precisely the causally compatible pairs $(x^\sigma, x^\tau)$ such that $\leq_{x\sigma,x\tau}$ has a top element: the pair $(\Pi_\sigma(m), \Pi_\tau(m))$.

In the sequel, we shall only reason on the interaction through the proxy of Proposition 4.8 and forthcoming lemmas characterizing immediate causality in the interaction. However, to ease the flow of the exposition, those are postponed to Section 4.2.6.

### 4.2.3. *Composition.*
Following the traditional methodology of game semantics, composition is defined from interaction via *hiding*. We first briefly analyse the *components* of interactions.

The projections $\Pi_\sigma$ and $\Pi_\tau$ project any event of $\tau \circled{\sigma}$ to a matching pair of an event of $\sigma \parallel C$ and an event of $A \parallel \tau$. These projections help us classify every $p \in |\tau \circled{\sigma}|$ into:

(1) $\Pi_\sigma(p) = (1, m)$ with $m \in |\sigma|$, and $\Pi_\tau(p) = (1, a)$ with $a \in |A|$,

(2) $\Pi_\sigma(p) = (1, m)$ with $m \in |\sigma|$, and $\Pi_\tau(p) = (2, n)$ with $n \in |\tau|$,

(3) $\Pi_\sigma(p) = (2, c)$ with $c \in |C|$, and $\Pi_\tau(p) = (2, n)$ with $n \in |\tau|$.

In case (1), the only relevant projection is $\Pi_\sigma(p) = (1, m)$ as $\Pi_\tau(p) = \partial_\sigma(m)$. We write $p_\sigma = m$ and $p_\tau$ is undefined, and we say that $p$ occurs in $A$. In case (3), the only relevant projection is $\Pi_\tau(p) = (2, n)$ as $\Pi_\sigma(p) = \partial_\tau(n)$. We write $p_\tau = t$ and $p_\sigma$ is undefined, and we say that $p$ occurs in $C$. Finally, in case (2) the two projections $\Pi_\sigma(p) = (1, m)$ and $\Pi_\tau(p) = (2, n)$ are relevant, but we must have $\partial_\sigma(m) = (2, b)$ and $\partial_\tau(p) = (1, b)$ for some $b \in |B|$. We write $p_\sigma = m, p_\tau = n$, we say that $p$ occurs in $B$ and that $p$ is **synchronized**.

The definition of composition consists simply in removing all synchronized events:

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

$$ 
\begin{align*}
|\tau \odot \sigma| &= \{p \in |\tau \circled{\sigma}| \mid p \text{ occurs in } A \text{ or } C\}, \\
p_1 \leq_{\tau \odot \sigma} p_2 &\Leftrightarrow p_1 \leq_{\tau \circled{\sigma}} p_2, \\
p_1 \#_{\tau \odot \sigma} p_2 &\Leftrightarrow p_1 \#_{\tau \circled{\sigma}} p_2, \\
\theta : x \cong_{\tau \odot \sigma} y &\Leftrightarrow \exists \theta' \subseteq \theta' : x' \cong_{\tau \circled{\sigma}} y'.
\end{align*}
$$

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

The composition of prestrategies $\sigma : A \vdash B$ and $\tau : B \vdash C$ gives data

$$ (|\tau \odot \sigma|, \leq_{\tau \odot \sigma}, \#_{\tau \odot \sigma}, \mathcal{S}(\tau \odot \sigma), \partial_{\tau \odot \sigma}) $$

satisfying all the axioms of Definition 4.2 except, possibly, $\sim$-receptivity$^{18}$. When composing prestrategies, we will check $\sim$-receptivity separately – this only occurs in Section 4.4.3.

However, if $\sigma$ and $\tau$ are strategies, then so is $\tau \odot \sigma$ [CCW19]. Composition is associative up to iso (with **isomorphisms** between causal strategies defined as between pre-interactions above). In Figure 35, the composition simply keeps the events in black. This means that the composition has two conflicting positive events, both corresponding to $\check{+}^+$: the model records the point of non-deterministic branching even when it brings no observable difference. Though this does not appear in pictures, we insist that events of $\tau \odot \sigma$ are certain events of $\tau \circled{\sigma}$. Thus an event of the composition always carries a unique causal explanation: itself.

To parallel this event-based definition of composition, there is a state-based characterization. A causally compatible pair $x^\sigma \in \mathcal{C}(\sigma), x^\tau \in \mathcal{C}(\tau)$ is **minimal** if for all causally compatible $y^\sigma \in \mathcal{C}(\sigma), y^\tau \in \mathcal{C}(\tau)$ with $y^\sigma \subseteq x^\sigma, y^\tau \subseteq y^\tau$ with $x_A^\sigma = y_A^\sigma$ and $x_C^\tau = y_C^\tau$, then $x_B = y_B$. The same definition applies to causally compatible pairs of symmetries.

<footnote>18However, $\sim$-receptivity of $\sigma$ and $\tau$ is required for $\tau \circled{\sigma}$ to form an ess [CCW19].</footnote>
**Proposition 4.10.** Consider $\sigma: A \vdash B$, and $\tau: B \vdash C$ causal strategies.

There is a causal strategy $\tau \odot \sigma$, unique up to iso, s.t. there are order-isos:

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

$$(- \odot -): \{(\theta^{\tau}, \theta^{\sigma}) \in \mathcal{S}(\tau) \times \mathcal{S}(\sigma) \mid \theta^{\sigma}, \theta^{\tau} \text{ minimal causally compatible}\} \simeq \mathcal{S}(\tau \odot \sigma)$$

commuting with dom and cod; s.t., for $\theta^{\sigma} \in \mathcal{S}(\sigma)$, $\theta^{\tau} \in \mathcal{S}(\tau)$ minimal causally compatible,

$$\partial_{\tau \odot \sigma}(\theta^{\tau} \odot \theta^{\sigma}) = \theta_{A}^{\sigma} \parallel \theta_{C}^{\tau}.$$

The minimality requirement amounts to asking the maximal events of $x^{\sigma}$ and $x^{\tau}$ to occur in $A$ or $C$. As events of $\tau \odot \sigma$ carry their causal witness, configurations of $\tau \odot \sigma$ are in one-to-one correspondence with those configurations of $\tau \oplus \sigma$ whose maximal events occur in $A$ or $C$ – thus Proposition 4.10 follows from Proposition 4.8 (see Appendix D.2.2).

In fact, trailing Opponent moves do not matter as they are forced by receptivity and courtesy to behave as in the game. A configuration $x \in \mathcal{C}(\sigma)$ is +-covered iff the top elements of $x$ (for $\leq_{\sigma}$) are positive – we write $x \in \mathcal{C}^{+}(\sigma)$. Likewise, $\theta \in \mathcal{S}(\sigma)$ is +-covered if $\mathrm{dom}(\theta)$ (or, equivalently, $\mathrm{cod}(\theta)$) is +-covered – we write $\theta \in \mathcal{S}^{+}(\sigma)$. We have [dV20]:

**Lemma 4.11.** Consider $\sigma, \tau: A$ two causal strategies. Assume there are

$$\psi: \mathcal{C}^{+}(\sigma) \simeq \mathcal{C}^{+}(\tau)$$

$$\psi: \mathcal{S}^{+}(\sigma) \simeq \mathcal{S}^{+}(\tau)$$

order-isomorphisms compatible with dom, cod, and display maps.

Then, $\sigma$ and $\tau$ are isomorphic.

See Appendix D.2.3 for the proof. Relying on this we can finally prove:

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

Then, there is a strategy $\tau \odot \sigma: A \vdash C$, unique up to iso, such that there are order-isos:

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

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

commuting with dom and cod, and s.t., for $\theta^{\sigma} \in \mathcal{S}^{+}(\sigma)$ and $\theta^{\tau} \in \mathcal{S}^{+}(\tau)$ causally compatible,

$$\partial_{\tau \odot \sigma}(\theta^{\tau} \odot \theta^{\sigma}) = \theta_{A}^{\sigma} \parallel \theta_{C}^{\tau}.$$

*Proof.* Relatively direct from Proposition 4.10 and Lemma D.14, see Appendix D.2.3. $\square$

This is convenient as +-covered configurations of strategies often have a simpler description (see e.g. Lemma 4.18). Minimality also disappears as a causally compatible pair of +-covered configurations is always minimal (indeed, a synchronized maximal event would be negative for one of the players). This final characterization will be used often to prove equalities between strategies. It is also of great use when linking with the relational model (see Section 7.1), but also for quantitative extensions (see e.g. [CCPW18, CdV20]).

**4.2.4. Congruence.** What is the right equivalence between causal (pre)strategies? There are a few options, several investigated in [CCW19]; here we use positive isomorphism:

**Definition 4.13.** Consider $\sigma, \tau: A$ two causal strategies on arena $A$.

A positive isomorphism $\varphi: \sigma \approx \tau$ is an isomorphism of ess satisfying

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

i.e. for all $x \in \mathcal{C}(\sigma)$, $\{(\partial_{\sigma}(s), \partial_{\tau} \circ \varphi(s)) \mid s \in x\} \in \mathcal{S}_{+}(A)$: the two maps are **positively symmetric**. In that case we say $\sigma$ and $\tau$ are **positively isomorphic**, and write $\sigma \approx \tau$.
This means that $\sigma$ and $\tau$ are the same up to renaming of their events. This renaming
might cause a reindexing of positive events, but it must keep the copy indices of negative
events unchanged. Crucially, positive isomorphism is preserved by composition [CCW19]:

**Proposition 4.14.** Consider $\sigma, \sigma' : A \vdash B$, $\tau, \tau' : B \vdash C$ s.t. $\sigma \approx \sigma'$ and $\tau \approx \tau'$.
Then, we have $\tau \odot \sigma \approx \tau' \odot \sigma'$.

The proof is fairly elaborate. Without going into details, it will be useful to have in
mind the first key step: showing that two (pre)strategies able to synchronize *up to symmetry*,
always also have a synchronization *on the nose*. More precisely, we have the following:

**Proposition 4.15.** Consider $\sigma : A \vdash B$ and $\tau : B \vdash C$ two causal (pre)strategies.

For any $x^\sigma \in \mathscr{C}(\sigma), x^\tau \in \mathscr{C}(\tau)$ and $\theta : x_B^\sigma \cong_B x_B^\tau$ s.t. the composite bijection is secured:

$$
x^{\sigma} \parallel x_{C}^{\tau} \stackrel{\partial_{\sigma} \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},
$$

then there are $y^\sigma \in \mathscr{C}(\sigma)$ and $y^\tau \in \mathscr{C}(\tau)$ causally compatible, along with symmetries

$$
\varphi^{\sigma} : y^{\sigma} \cong_{\sigma} x^{\sigma}, \qquad \varphi^{\tau} : y^{\tau} \cong_{\tau} x^{\tau},
$$

such that $\varphi_B^\tau \circ \theta = \varphi_B^\sigma$.

This follows from Lemma 3.23 in [CCW19]. Intuitively, we play $\mathcal{S}(\boldsymbol{\sigma})$ and $\mathcal{S}(\boldsymbol{\tau})$ against each other. By $\sim$-receptivity and extension they adjust their copy indices interactively until reaching an agreement. This is the first step to congruence, but not the only one: the requirement that we should get a global map $\varphi : \boldsymbol{\tau} \odot \boldsymbol{\sigma} \approx \boldsymbol{\tau}' \odot \boldsymbol{\sigma}'$ is in tension with the definition of isomorphism families, which only guarantees a more local bisimulation-like property. The mismatch is compensated by the uniqueness of extensions granted by thin, without which congruence fails. Details are out of scope for the present paper [CCW19].

If $\boldsymbol{\sigma} \approx \boldsymbol{\tau}$, there can be in principle multiple $\varphi : \boldsymbol{\sigma} \approx \boldsymbol{\tau}$. We leave these isomorphisms to the background, as we have not yet encountered a computational use for these. If they are retained, then arenas, causal strategies and positive morphisms form a bicategory [Paq20].

**Remark 4.16.** In Definition 4.13, one could ask $\varphi$ to preserve $\partial$ up to arbitrary symmetry (weak isomorphism) or even, to be itself invertible only up to symmetry (weak equivalence). This changes the mediating morphisms, but not the resulting equivalence relation between strategies (see Corollary 3.30 in [CCW19]). In this paper we choose positive isomorphism as it seems natural conceptually, and because the additional positivity constraint is useful.

4.2.5. *Copycat.* So as to complete the categorical structure, it remains to define *copycat*.

**Definition 4.17.** For each $--$arena $A$, the **copycat** strategy $\omega_A : A \vdash A$ is defined as:

$$
\begin{align*}
|\mathscr{c}_A| &= |A \vdash A| \\
\partial_{\mathscr{c}_A}(i, a) &= (i, a) \\
(i, a) \leq_{\mathscr{c}_A} (j, a') &\Leftrightarrow a <_A a'; \text{ or } a = a', \text{ pol}_{A \vdash A}(i, a) = - \text{ and } \text{pol}_{A \perp_A}(j, a') = + \\
(i, a) \#_{\mathscr{c}_A} (j, a') &\Leftrightarrow a \#_A a',
\end{align*}
$$

with symmetries those bijections of the form $\theta_1 \parallel \theta_2 : x_1 \parallel x_2 \cong_{c_A} y_1 \parallel y_2$ such that

$$
\theta_1 : x_1 \cong_A y_1, \quad \theta_2 : x_2 \cong_A y_2, \quad \text{and} \quad \theta_1 \cap \theta_2 : x_1 \cap x_2 \cong_A y_1 \cap y_2.
$$
This simplifies the usual definition [CCW19], exploiting the particular shape of arenas. Its immediate causal links import $\to_A$ on either side, along with all the $(i, a) \to_{c_A} (j, a)$ when $\text{pol}_{A \to A}(i, a) = -$ and $\text{pol}_{A \to A}(j, a) = +$. In other words, $c_A$ is an asynchronous forwarder: it is prepared to play any positive event on one side, under the condition that the corresponding negative event appears first on the other side. Its symmetries are inherited from $\mathcal{S}(A \vdash A)$, with the constraint that they should agree on events already forwarded.

Perhaps the simplest description of copycat is through its completely forwarded states:

**Lemma 4.18.** Consider A any --arena. Then, we have:

$$ \begin{aligned} \mathcal{C}^+(\mathbf{c}_A) &= \{x_A \mid x_A \in \mathcal{C}(A \mid A) \mid x_A \in \mathcal{C}(A)\} \\ \mathcal{S}^+(\mathbf{c}_A) &= \{\theta_A \mid \theta_A \in \mathcal{S}(A \mid A) \mid \theta_A \in \mathcal{S}(A)\}. \end{aligned} $$

*Proof.* Straightforward. □

This foreshadows the link with relational semantics in Section 7.1: when restricted to +-covered configurations, copycat looks like the identity relation. We may deduce:

**Proposition 4.19.** *Composition is associative up to ≈ on prestrategies.* For any $\sigma : A \vdash B$,

$$ \mathbf{c}_B \odot \sigma \odot \mathbf{c}_A \approx \sigma, $$

so that --arenas and causal strategies form a category.

*Proof.* Associativity follows from Proposition 4.10 and a ternary version of causal compatibility – see also [CCW19] for a detailed proof via the universal property of the interaction pullback. For neutrality of copycat, there is an order-isomorphism preserving display maps

$$ \begin{aligned} \mathcal{C}^+(\mathbf{c}_B \odot \boldsymbol{\sigma}) &\approx \{(x^{\mathbf{c}_B}, x^{\boldsymbol{\sigma}}) \in \mathcal{C}^+(\mathbf{c}_B) \times \mathcal{C}^+(\boldsymbol{\sigma}) \mid x^{\mathbf{c}_B} \text{ and } x^{\boldsymbol{\sigma}} \text{ causally compatible}\} \\ &\approx \{(x^{\mathbf{c}_B}, x^{\boldsymbol{\sigma}}) \in \mathcal{C}^+(\mathbf{c}_B) \times \mathcal{C}^+(\boldsymbol{\sigma}) \mid x^{\mathbf{c}_B} \text{ and } x^{\boldsymbol{\sigma}} \text{ matching}\} \\ &\approx \{(x_B^{\boldsymbol{\sigma}} \parallel x_B^{\boldsymbol{\sigma}}, x^{\boldsymbol{\sigma}}) \mid x^{\boldsymbol{\sigma}} \in \mathcal{C}^+(\boldsymbol{\sigma})\} \\ &\approx \mathcal{C}^+(\boldsymbol{\sigma}), \end{aligned} $$

using first Proposition 4.12; verifying directly that securedness always holds when composing with copycat; using Lemma 4.18. The same reasoning can be made with symmetries, concluding that $\mathbf{c}_B \odot \boldsymbol{\sigma}$ and $\boldsymbol{\sigma}$ are isomorphic by uniqueness in Proposition 4.12. □

Before we develop further this categorical structure, we introduce a few useful lemmas.

### 4.2.6. Immediate causality in interactions.
Later on, we will need some tools to reason on the causality in $\tau \circled{\sigma}$ and how it relates to that in $\sigma$ and $\tau$.

**Lemma 4.20.** For $\sigma : A \vdash B$, $\tau : B \vdash C$ causal prestrategies, for $m, m' \in |\tau \circled{\sigma}|$, if $m \to_{\tau \circled{\sigma}} m'$, then $m_{\sigma} \to_{\sigma} m'_{\sigma}$, or $m_{\tau} \to_{\tau} m'_{\tau}$, where $m_{\sigma}, m_{\tau}$ are defined whenever used.

The proof is in Appendix D.3. So in the event-based view of interaction, immediate causal links originate in one of the components. For $\sigma$ and $\tau$ strategies, one can track down the responsible component via a polarity analysis. Of course, it is usual in game semantics that events of $\tau \circled{\sigma}$ cannot sensibly be assigned a polarity in $\{-, +\}$, because $\sigma$ and $\tau$ disagree on $B$. A more useful notion of polarity is $\text{pol}_{\tau \circled{\sigma}} : |\tau \circled{\sigma}| \to \{-, l, r\}$ given by:

$$ \begin{aligned} \text{pol}_{\tau \circled{\sigma}}(m) &= | \quad \text{if } m_{\sigma} \text{ is defined and } \text{pol}_{\sigma}(m_{\sigma}) = +, \\ \text{pol}_{\tau \circled{\sigma}}(m) &= r \quad \text{if } m_{\tau} \text{ is defined and } \text{pol}_{\tau}(m_{\tau}) = +, \\ \text{pol}_{\tau \circled{\sigma}}(m) &= - \quad \text{otherwise.} \end{aligned} $$

As an example, we show in Figure 35 the polarities arising from this definition. Then:
**Lemma 4.21.** Consider $\sigma: A \vdash B$ and $\tau: B \vdash C$ strategies, and $m \to_{\tau\otimes\sigma} m'$. Then,

(1) if $\text{pol}_{\tau\otimes\sigma}(m') = \text{l}$, then $m_{\sigma} \to_{\sigma} m'_{\sigma}$,

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

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

*Proof.* (1) By Lemma 4.20, $m_{\sigma}, m'_{\sigma}$ defined and $m_{\sigma} \to_{\sigma} m'_{\sigma}$ – in which case we are done; or $m_{\tau}, m'_{\tau}$ defined and $m_{\tau} \to_{\tau} m'_{\tau}$. Since $\text{pol}_{\tau\otimes\sigma}(m') = \text{l}$, $\text{pol}_{\tau}(m'_{\tau}) = -$. By courtesy, $\partial_{\tau}(m_{\tau}) \to_{B\vdash C} \partial_{\tau}(m'_{\tau})$; hence $m$ occurs in $B$ and $\partial_{\sigma}(m_{\sigma}) \to_{A\vdash B} \partial_{\sigma}(m'_{\sigma})$. By Lemma A.2, $m_{\sigma} <_{\sigma} m'_{\sigma}$, and the causality must be immediate by Lemma D.17. (2) is symmetric.

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

**4.3. Seely Category.** Now, we turn to the different components of a Seely category.

**4.3.1. Symmetric monoidal category with products.** On $\downarrow\uparrow$-Strat, enriched as in Section 4.1.2. The tensor of causal strategies is defined below:

**Definition 4.22.** For $\sigma_1: A_1 \vdash B_1$, $\sigma_2: A_2 \vdash B_2$ causal strategies between $\text{--arenas}$, then

$$ \sigma_1 \otimes \sigma_2 : A_1 \otimes A_2 \vdash B_1 \otimes B_2 $$

is defined as the ess $\sigma_1 \parallel \sigma_2$ along with display map $\partial_{\sigma_1 \otimes \sigma_2}(i, s) = (j, (i, a))$ if $\sigma_i(s) = (j, a)$.

Bifunctoriality is direct via Proposition 4.12. The symmetric monoidal structural isomorphisms are provided by copycat strategies, only changing display maps:

$$ \alpha_{A,B,C} : (A \otimes B) \otimes C \cong A \otimes (B \otimes C) $$

$$ \rho_A : A \otimes \mathbf{1} \cong A $$

$$ s_{A,B} : A \otimes B \cong B \otimes A $$

$$ \lambda_A : \mathbf{1} \otimes A \cong A $$

satisfying up to positive iso the expected naturality and coherence laws [CCW19]. For cartesian products, the projections $\pi_1: A_1 \& A_2 \vdash A_1$ and $\pi_2: A_1 \& A_2 \vdash A_2$ are relabeled copycat strategies, while the pairing of causal strategies is defined similarly to the tensor:

**Definition 4.23.** Consider $\sigma_1: A \vdash B_1$ and $\tau: A \vdash B_2$ causal strategies between $\text{--arenas}$. Then, $\langle\sigma_1, \sigma_2\rangle: A \vdash B_1 \& B_2$ is defined as having ess $\sigma_1 \& \sigma_2$, along with

$$ \partial_{\langle\sigma_1, \sigma_2\rangle}(i, s) = (1, a) \quad \text{if } \partial_{\sigma_i}(s) = (1, a) $$

$$ \partial_{\langle\sigma_1, \sigma_2\rangle}(i, s) = (2, (i, b)) \quad \text{if } \partial_{\sigma_i}(s) = (2, b). $$

It follows from Proposition 4.12 and direct verifications that this yields binary products.

**4.3.2. Monoidal closed structure.** We now describe the monoidal closure.

On objects, the closure is the arrow $A \to B$ from $\downarrow\uparrow$-Strat. However, for now, the strategies on $A \vdash B$ and on $A \to B$ are not in one-to-one correspondence. Indeed strategies in $A \to B$ include a pointer for initial moves in $A$, while strategies in $A \vdash B$ do not. This pointer is not always unique, as illustrated in Figure 36. To cope with this we could have, as for the play-based strategies of the previous sections, set the morphisms of our category directly as strategies on $A \to B$; but in this causal setting that obfuscates composition.

Instead, we restrict to strategies for which this pointer reconstruction is unique:
<figure><img src="image_48.png" /><figcaption>Figure 36: Non-uniqueness of the threading pointer</figcaption></figure>

**Definition 4.24.** A causal strategy $\sigma: A$ on arena $A$ is **pointed** if for each $s \in |\sigma|$ there is a unique event $init(s) \in |\sigma|$ which is minimal for $\leq_{\sigma}$ and such that $init(s) \leq_{\sigma} s$.

Copycat strategies are pointed (as arenas are forestial), and pointed strategies are stable under composition and the other operations on strategies. From now on, we consider that all causal strategies are pointed. We write $\rightarrow$-Strat for the category having $--$arenas as objects, and as morphisms from $A$ to $B$, the pointed causal strategies on $A \vdash B$.

For pointed strategies, the missing pointer can always be recovered uniquely:

**Lemma 4.25.** Let $A, B$ and $C$ be $--$arenas. Then, we have a bijection:

$$ \Lambda_{A,B,C} : \rightarrow\text{-Strat}(A \otimes B, C) \simeq \rightarrow\text{-Strat}(A, B \multimap C) $$

*Proof.* The bijection only affects the display map, leaving the other components unchanged.

The non-trivial direction is from left to right. Consider $\sigma: A \otimes B \vdash C$. We set:

$$ \partial_{\Lambda(\sigma)}(s) = \begin{cases} (1, a) & \text{if } \partial_{\sigma}(s) = (1, (1, a)), \\ (2, (2, c)) & \text{if } \partial_{\sigma}(s) = (2, c), \\ (2, (1, (c, b))) & \text{if } \partial_{\sigma}(s) = (1, (2, b)) \text{ and } \partial_{\sigma}(\text{init}(s)) = (2, c). \end{cases} $$

It is a direct verification that this yields a bijection as claimed. $\square$

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

From this point, we may now easily wrap up the symmetric monoidal closed structure.

**Proposition 4.26.** The category $\rightarrow$-Strat is symmetric monoidal closed.

*Proof.* First, for any $--$arenas $A$ and $B$, we have $A \multimap B$ and an **evaluation**

$$ \mathrm{ev}_{A,B} = \Lambda_{A \multimap B, A, B}^{-1}(\mathfrak{c}_{A \multimap B}) : (A \multimap B) \otimes A \vdash B, $$

and given $\sigma: A \otimes B \vdash C$, $\mathrm{ev}_{B,C} \odot (\Lambda_{A,B,C}(\sigma) \otimes B) \approx \sigma$ follows from a variation over the neutrality of copycat for composition. From there, the universal property is routine. $\square$

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

**4.3.3. The exponential.** The first step is to introduce a functor $! : \rightarrow$-Strat $\rightarrow \rightarrow$-Strat.

**Definition 4.27.** Consider $A$ and $B$ two $--$arenas, and $\sigma: A \vdash B$ a causal strategy.

We define a strategy $!\sigma: !A \vdash !B$ with $!\sigma$ as event structure with symmetry and:

$$ \partial_{!\sigma}(i, m) = \begin{cases} (1, (i, a)) & \text{if } \partial_{\sigma}(m) = (1, a), \\ (2, (i, b)) & \text{if } \partial_{\sigma}(m) = (2, b). \end{cases} $$

It is a direct verification that this defines a causal strategy, and functoriality is proved as for the tensor product of strategies. To complete the categorical structure, we have:
**Proposition 4.28.** The category $\rightarrow$-Strat is a Seely category.

*Proof.* The structure presented above is completed by structural natural families of strategies:

$$ \mathbf{dig}_A : !A \rightarrow !!A $$

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

$$ \mathbf{der}_A : !A \rightarrow A $$

$$ \mathbf{mon}^0 : 1 \cong !1. $$

making (!, dig, der) a comonad along with the *Seely isomorphisms*. Those are all relabeled copycat strategies: for instance, $\mathbf{dig}_A$ is $\mathbf{c}!!A$ relabeled on the left hand side following a bijection $\mathbb{N} \times \mathbb{N} \simeq \mathbb{N}$, $\mathbf{der}_A$ is $\mathbf{c}A$ relabeled to set events on the left hand side to copy index 0, etc. The naturality and coherence are easily verified, exploiting again Proposition 4.12. $\square$

4.3.4. Extracting plays. In Section 4.1.4, we unfolded causal strategies to non-alternating strategies. Here, we show that this is compatible with the categorical operations.

First, we extend the definition in Proposition 4.3 for causal strategies from A to B.

**Definition 4.29.** For A and B two --arenas, and $\sigma : A \vdash B$ a causal strategy, we define

$$ \mathcal{C}\text{-Unf}(\sigma) = \partial_{\Lambda(\sigma)}(\mathcal{C}\text{-Plays}(\sigma)) \in \mathcal{C}\text{-Strat}(A, B) $$

exploiting that $\sigma$ and $\Lambda(\sigma)$ only differ via their display map.

This matches applying Proposition 4.3 to $\Lambda(\sigma) : A \dashrightarrow B$ obtained by monoidal closure.

**Proposition 4.30.** There is a symmetric monoidal closed $\mathcal{C}\text{-Unf}(-) : \rightarrow$-Strat $\rightarrow$ $\mathcal{C}\text{-Strat}$.

*Proof.* For identities, the definition of plays of the asynchronous copycat (Definition C.4) follows the characterisation of configurations of $\mathbf{c}A$ found e.g. in Lemma 3.11 in [CCRW17].

For composition, take $\sigma : A \vdash B$ and $\tau : B \vdash C$. Though $\tau \circledast \sigma$ is not an esp, Definition 3.18 generalizes transparently to $\mathcal{C}\text{-Plays}(\tau \circledast \sigma)$. There are two inclusions to check:

$\mathcal{C}\text{-Unf}(\tau \odot \sigma) \subseteq \mathcal{C}\text{-Unf}(\tau) \odot \mathcal{C}\text{-Unf}(\sigma)$: any $s \in \mathcal{C}\text{-Unf}(\tau \odot \sigma)$ has the form $\partial_{\Lambda(\tau \odot \sigma)}(t)$ for $t \in \mathcal{C}\text{-Plays}(\tau \odot \sigma)$, which in turn can be completed to $v \in \mathcal{C}\text{-Plays}(\tau \circledast \sigma)$. Then $v$ may be displayed to $u \in \mathcal{C}\text{-Unf}(\tau) \circledast \mathcal{C}\text{-Unf}(\sigma)$, witnessing $s \in \mathcal{C}\text{-Unf}(\tau) \odot \mathcal{C}\text{-Unf}(\sigma)$.

$\mathcal{C}\text{-Unf}(\tau) \odot \mathcal{C}\text{-Unf}(\sigma) \subseteq \mathcal{C}\text{-Unf}(\tau \odot \sigma)$: any $s \in \mathcal{C}\text{-Unf}(\tau) \odot \mathcal{C}\text{-Unf}(\sigma)$ has a witness $u \in \mathcal{C}\text{-Unf}(\tau) \circledast \mathcal{C}\text{-Unf}(\sigma)$, projecting to $u \vdash A, B \in \mathcal{C}\text{-Unf}(\sigma)$ and $u \vdash B, C \in \mathcal{C}\text{-Unf}(\tau)$. Those are respectively $\partial_{\Lambda(\sigma)}(s^\sigma)$ and $\partial_{\Lambda(\tau)}(s^\tau)$ for $s^\sigma \in \mathcal{C}\text{-Plays}(\sigma)$ and $s^\tau \in \mathcal{C}\text{-Plays}(\tau)$. Then $x^\sigma := |s^\sigma|$ and $x^\tau := |s^\tau|$ are causally compatible as $u$ induces a linearization of the corresponding bijection. By construction, $x^\tau \circledast x^\sigma$ has a linearization $v$ that displays to $u$; and its restriction to visible events yields $t \in \mathcal{C}\text{-Plays}(\tau \odot \sigma)$ that displays to $s$.

The preservation of the monoidal structure is direct; the functor is strict monoidal. $\square$

As $\mathcal{C}\text{-Strat}$ does not handle symmetry, it supports no equivalence relation corresponding to $\approx$. Nevertheless, this lets us import the stability of well-bracketing under composition. We first generalize Definition 4.4 to well-bracketed causal strategies between --arenas:

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

We say that $\sigma : A \vdash B$ is **well-bracketed** iff $\mathcal{C}\text{-Unf}(\sigma)$ is well-bracketed.

From Propositions 3.22 and 4.30, there is an smcc with products $\rightarrow$-Strat<sup>wb</sup> of --arenas and well-bracketed causal strategies. Finally, $!(-)$ preserves well-bracketing and the other components for the exponential are well-bracketed, so $\rightarrow$-Strat<sup>wb</sup> extends to a Seely category.
4.4. Interpretation of $IA_\parallel$. We now describe the interpretation of $IA_\parallel$ in $\to$-Strat$_i^{wb}$. First the types of $IA_\parallel$ are the same as those of $IA$; their interpretation does not change.

4.4.1. Interpretation of core PCF. We focus on the core PCF primitives, postponing let.

The $\lambda$-calculus primitives are interpreted following the cartesian closed structure of $\to$-Strat$_i^{wb}$. For constants, we use the obvious strategies returning the corresponding value. For basic PCF combinators, there are obvious causal strategies corresponding to Figures 12 and 14. For recursion, we must first define a partial order on causal strategies:

**Definition 4.32.** Consider A an arena, and $\sigma, \tau$: A causal (pre)strategies.

We write $\sigma \leqslant \tau$ iff $\mathscr{C}(\sigma) \subseteq \mathscr{C}(\tau)$ – so $|\sigma| \subseteq |\tau|$ as well – with, additionally:

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

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

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

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

i.e. all components compatible with the inclusion.

Causal strategies on A, ordered by $\leqslant$, form a *directed complete partial order*; however without a least element. Indeed, strategies minimal for $\leqslant$ still have – by receptivity – events corresponding to the minimal events of A, but those are *named* arbitrarily. We solve this as in [CCW19]: we choose one minimal causal strategy $\perp_A: A$ with events *exactly* those negative minimal in A; induced causality, conflict, and isomorphism family; and as display map the identity. For any $\sigma$: A, we pick $\sigma^b \cong \sigma$: A such that $\perp_A \leqslant \sigma^b$, obtained by renaming minimal events. We write $\mathcal{D}_A$ for the pointed dcpo of causal strategies above $\perp_A$.

All operations on strategies examined so far are continuous. So, the operation

$$F : \mathcal{D}_{1\perp(A\to A)\to A} \to \mathcal{D}_{1\perp(A\to A)\to A} \\ \sigma \mapsto (\lambda f^{A\to A} \cdot f(\sigma f))^b,$$

in $\lambda$-calculus syntax following the cartesian closed structure of $\to$-Strat$_i^{wb}$, is continuous. Thus it has a least fixed point $\mathcal{Y}_A \in \mathcal{D}_{1\perp(A\to A)\to A}$, i.e. such that $\mathcal{Y}_A = F(\mathcal{Y}_A)$.

4.4.2. Interpretation of let. We give the interpretation of parallel let, as

$$[[\Gamma \vdash \text{let} \quad \begin{pmatrix} x_1 = N_1 \\ x_2 = N_2 \end{pmatrix} \quad \text{in } M : \mathbb{Y}]] = \text{plet}_{\mathbb{X}, \mathbb{Y}} \odot! \langle [[N_1]], [[N_2]], \Lambda_{\mathbb{X}\&\mathbb{X}}^!([[M]]) \rangle.$$

where $\text{plet}_{\mathbb{X}, \mathbb{Y}} \in \to$-Strat$_i^{wb}(\mathbb{X} \& \mathbb{X} \& ((\mathbb{X} \& \mathbb{X}) \to \mathbb{Y}), \mathbb{Y})$ first evaluates its two arguments $\mathbb{X}$ in parallel. Once they both terminate on $v$ and $w$, it calls its function argument, with $\langle v, w \rangle$.

More formally, we first define a prestrategy “forcing” evaluation to $v, w$, i.e.

$$\text{force}_{v,w} : !((\mathbb{X} \& \mathbb{X} \& ((\mathbb{X} \& \mathbb{X}) \to \mathbb{Y}))) \vdash \mathbb{Y}$$

as in Figure 37 – only a prestrategy, not receptive to other values. Likewise,

$$\text{eval}_{v,w} : !((\mathbb{X} \& \mathbb{X} \& ((\mathbb{X} \& \mathbb{X}) \to \mathbb{Y}))) \vdash \mathbb{Y}$$

is defined by first using the cartesian closed structure of $\to$-Strat$_i^{wb}$ to obtain a strategy

$$\lambda\langle x_1, x_2, f \rangle. f \langle v, w \rangle \in \to \text{Strat}_i^{wb}(\mathbb{X} \& \mathbb{X} \& ((\mathbb{X} \& \mathbb{X}) \to \mathbb{Y}), \mathbb{Y}),$$

evaluating $f$ on $\langle v, w \rangle$, from which $\text{eval}_{v,w}$ is obtained simply by removing the initial $\mathbf{q}^-$. Up to reindexing, we assume $\text{eval}_{v,w}$ does not use copy indices 0 and 1 on the calls to context.
<figure><img src="image_51.png" /><figcaption>Figure 37: The prestrategy $\mathbf{force}_{v,w}$</figcaption></figure>

<figure><img src="image_52.png" /><figcaption>Figure 38: The strategy $\mathbf{plet}_{X,Y}$</figcaption></figure>

Finally, this lets us define $\mathbf{plet}$ via the expression (the supremum refers to $\leq$):

$$ \mathbf{plet}_{X,Y} = \bigvee_{v,w \in X} \mathbf{force}_{v,w} \cdot \mathbf{eval}_{v,w} \in \mathbf{Strat}^w(X \& X \& ((X \& X) \to Y), Y) $$

where the concatenation $\cdot$ sets both maximal (negative) events of $\mathbf{force}_{v,w}$ as dependencies for $\mathbf{eval}_{v,w}$. The full strategy is represented in Figure 38. Unlike for Figure 37, the picture in Figure 38 is to be read as a symbolic representation. The concrete strategy $\mathbf{plet}_{X,Y}$ has patterns as in Figure 38 for all concrete values for $v, w, u$ and copy indices $i$ and $j$.

The interpretation of the sequential let can be obtained as a simplification.

### 4.4.3. Interpretation of interference.
Now, we interpret shared state and semaphores. By and large, it closely follows the sequential interpretation of Sections 3.4.2 and 3.4.3.

For the primitives interacting with memory and semaphores, we use the same definitions as in Section 3.4.2, with the obvious causal strategies matching Figures 24, 25, 26, and 27.

For new references and semaphores, we regard the alternating strategy $\mathbf{cell}_n$ from Section 3.4.3 as a (sequential) event structure: its events $|\mathbf{cell}_n|$ are the non-empty plays, the causal order is given by prefix, the conflicting pairs are all non-comparable plays. The display map

$$ \begin{array}{l} \partial_{\mathbf{cell}_n} : |\mathbf{cell}_n| \to !\mathbf{ref} \\ sa \mapsto a \end{array} $$

keeps the last move. As configurations are sets of prefixes of a given play, we set $\mathcal{S}(\mathbf{cell}_n)$ to comprise those bijections induced by plays $s_1 \cong_A s_2$ symmetric on $A$ (see Definition 2.11).

We display in Figure 39 a few early moves of $\mathbf{cell}_0$, with the convention that all moves in the same row are in pairwise conflict. In this diagram we observe that $\mathbf{cell}_0$ fails *courtesy*: indeed, the immediate causal link $\surd_2^+ \to \mathbf{r}_8^-$, for instance, would be illegal for a strategy.

Note that although $\mathbf{cell}_n : !\mathbf{ref}$ is only a prestrategy and not a strategy, we have:

**Proposition 4.33.** For all $\sigma : !\mathbf{ref} \vdash A$, for all $n \in \mathbb{N}$, $\sigma \odot \mathbf{cell}_n : A$ is a strategy.

*Proof.* First, $\sim$-receptivity is established directly, exploiting that $\sigma$ and $\mathbf{cell}_n$ do not have non-courteous immediate causal links across components – they are *componentwise courteous* in the sense of [CCW19]. Lemma 3.36 from [CCW19] ensures that $\sigma \odot \mathbf{cell}_n$ is $\sim$-receptive.
<figure><img src="image_53.png" /><figcaption>Figure 39: Beginning of **cell**_0</figcaption></figure>

<figure><img src="image_54.png" /><figcaption>Figure 40: Beginning of **lock**_0</figcaption></figure>

It remains to prove $\sigma \odot \text{cell}_n$ receptive and courteous. But those properties are independent of symmetry. Without symmetry, strategies are exactly those prestrategies invariant (up to iso) under composition with copycat [CCRW17]. But then, we compute:

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

so by Theorem 3.20 of [CCRW17], $\sigma \odot \text{cell}_n$ is receptive and courteous as required. $\square$

For semaphores, using the same recipe we obtain a prestrategy $\text{lock}_n : !\text{sem}$ for each $n \in \mathbb{N}$. A beginning of $\text{lock}_0$ is displayed in Figure 40. Note that in this diagram, trailing Opponent moves are indeed maximal, Player has no response – an attempt to release a lock that has not been grabbed, or to grab a lock that has not been released, triggers no response.

The interpretation of new references and semaphores is defined as in Section 3.4.3.

### 4.5. Adequacy.
Adequacy could be deduced from the connection with [GM08] – see Section 4.6.2. Instead we give an independent proof, as we believe it helps build the operational intuitions for the model. Rather than as usual relying on logical relations, we follow an alternative route, proving first adequacy for certain finitary terms in which the correspondence between operational and game semantics is more concrete.

#### 4.5.1. Canonical adequacy.
The sharpest link between operational and game semantics holds factoring out recursion, higher-order, and dynamic generation of semaphores or references.

We temporarily extend $\mathbf{IA}_\parallel$ with an explicit $\perp_A : A$ for every type $A$, interpreted by a minimal strategy with no Player move. Take $\Sigma$ an **interference context**, i.e. of the form

$$ \Sigma = \ell_1 : \text{ref}, \dots, \ell_i : \text{ref}, \ell_{i+1} : \text{sem}, \dots, \ell_n : \text{sem}, $$

and $\Sigma \vdash M : \mathcal{X}$ where $\mathcal{X} \in \{\mathbb{U}, \mathbb{B}, \mathbb{N}\}$. We say $M$ is in **canonical form** if it contains no fixpoint, subterm of higher type, bad references or semaphores, **newref** or **newsem**, with no store-independent reductions available (other than the *interfering reductions* of Figure 2).

To help us link operational and denotational semantics for canonical forms, we introduce a few concepts. First, if $s$ is a store with $\text{dom}(s) = \Sigma$ as above, we interpret it as

$$ [[s]] = (\bigotimes_{1 \le k \le i} \mathbf{cell}_{s(\ell_k)}) \otimes (\bigotimes_{i+1 \le k \le n} \mathbf{lock}_{s(\ell_k)}) : (\bigotimes_{1 \le k \le i} !\text{ref}) \otimes (\bigotimes_{i+1 \le k \le n} !\text{sem}) \cong ![[\Sigma]]. $$

To track evolution of an interaction we use the notion of *residuals*.
**Definition 4.34.** If $E$ is an ess and $x \in \mathscr{C}(E)$, the **residual** $E/x$ has

$$ 
\begin{align*}
|E/x| &= \{e \in |E| \setminus x \mid \forall e' \in x, \neg(e \#_E e')\}, \\
e_1 \leq_{E/x} e_2 &\Leftrightarrow e_1 \leq_E e_2, \\
e_1 \#_{E/x} e_2 &\Leftrightarrow e_1 \#_E e_2, \\
\theta : y \cong_{E/x} z &\Leftrightarrow \theta \cup \mathrm{id}_x : x \cup y \cong_E x \cup z.
\end{align*}
$$

If $E$ has polarities they are preserved as well and for $A$ an arena, $A/x$ is an arena. In particular for $![[\Sigma]]$, by definition and playing Hilbert's hotel, for any $x \in \mathscr{C}(![[\Sigma]])$ with as many Player as Opponent moves, we have $(![[\Sigma]])/x \cong ![[\Sigma]]$. Residuals also apply to causal (pre)strategies: if $\sigma: A$, then for each $x \in \mathscr{C}(\sigma)$, we have $\sigma/x: A/\partial_\sigma(x)$ a prestrategy.

Take $\Sigma \vdash M: X$ in canonical form. Necessarily $[[X]]$ – also written $X$ – has a unique minimal move $\mathbf{q}^-$ and $[[M]]$ has a unique matching minimal move, also written $\mathbf{q}^-$. We set

$$ (M) = [[M]]/\{\mathbf{q}^-\} : \Sigma \vdash (X), $$

where $(X) = [[X]]/\{\mathbf{q}^-\}$, yielding a causal prestrategy in the sense of Definition 4.2.

Now, we are equipped to state the most central ingredient of our proof of adequacy.

**Lemma 4.35.** Consider $\Sigma \vdash M: X$ in canonical form, and $s$ a store with $\mathrm{dom}(s) = \Sigma$. Then, there is a (necessarily interfering) one-step reduction

$$ \langle M, s \rangle \rightsquigarrow \langle M', s' \rangle $$

iff there are matching $x \in \mathscr{C}((M))$ and $y \in \mathscr{C}([s])$ with two elements each, such that

$$ (M)/x \approx (M') : ![[\Sigma]] \vdash (X), \quad [[s]]/y \approx [[s')] : ![[\Sigma]]. $$

*Proof.* For interfering operations $\ell := v, !\ell$, **grab**($\ell$) or **release**($\ell$), it is a direct verification by definition of the interpretation. The result then follows by induction on $M$. $\square$

This identifies store operations that a canonical $M$ may perform immediately with store $s$, with the minimal events of $(M) \circled{[}[[s]]$ that occur in $\Sigma$. It almost suffices to iterate this to obtain adequacy for canonical terms; however interfering reductions might yield non-canonical terms, so state operations must be interleaved with pure reductions. Write $M \triangleright N$ for pure reductions, i.e. the context closure of interference-independent reductions in Figure 2 – these reductions leave invariant the interpretation as causal strategies. Moreover:

**Lemma 4.36.** Consider $\Sigma \vdash M: X$ without fixpoint, subterm of higher type, bad references or semaphores, **newref** or **newsem**. Then, there exists $\Sigma \vdash N: X$ canonical with $M \triangleright^* N$.

Moreover, for any store $s$ with $\mathrm{dom}(s) = \Sigma$, there is $\langle M, s \rangle \rightsquigarrow^* \langle \mathbf{skip}, s' \rangle$ iff there is $\langle N, s \rangle \rightsquigarrow^* \langle \mathbf{skip}, s' \rangle$, and the correspondence preserves the number of interfering operations.

*Proof.* A routine standardization argument. $\square$

Using this, we can prove adequacy for canonical terms. Intuitively, a sequence $\langle M, s \rangle \rightsquigarrow^* \langle \mathbf{skip}, s' \rangle$ can be reproduced semantically: each interfering reduction yields by Lemma 4.35 a pair of events in $(M) \circled{[}[[s]]$, while state-free reductions leave the interpretation unchanged. Reciprocally, a successful interaction in $(M) \odot [[s]]$ is a partially ordered set of memory operations, which may be linearized by securedness; informing a reduction sequence.

**Proposition 4.37.** Consider $\Sigma \vdash M: \mathcal{U}$ in canonical form, and $s$ a store with $\mathrm{dom}(s) = \Sigma$. Then, $\langle M, s \rangle \rightsquigarrow^* \langle \mathbf{skip}, s' \rangle$ iff $(M) \odot [[s]]$ has a positive move.
**Proof.** If. Taking $x \odot y \in (M) \otimes [s]$, we build the sequence by induction on the size of $x \otimes y$.

If $x \otimes y$ has exactly one event, it must match $\check{+}$ in $(\mathbb{U})$. Since $M$ is canonical, by a case inspection on the shape of $M$, the only case for which $(M)$ has a minimal positive event in $(\mathbb{U})$ is a value **skip**. Otherwise, since $x$ and $y$ are causally compatible, there is a sequence

$$ (\emptyset, \emptyset) \leftarrow (x_1, y_1) \leftarrow \dots \leftarrow (x_n, y_n) = (x, y) $$

of one-step extensions (for the product inclusion order) of matching $x_i \in \mathscr{C}((M))$ and $y_i \in \mathscr{C}([s])$, obtained by linearization from the acyclicity of causal compatibility of $x$ and $y$. In particular, $x_1 = \{m_1^+\}$ and $y_1 = \{n_1^-\}$ singleton sets. By Proposition 4.12, $y$ is $+\text{-covered}$, so there is a (unique, by definition of $[s]$) $n_1^- \to_{[s]} n_2^+$, and by Lemma A.5 there is a unique matching $m_1^+ \to_{(M)} m_2^-$. Since $n_2$ only depends on $n_1$ and $m_2$ only depends on $m_1$, w.l.o.g. $x_2 = \{m_1, m_2\}$ and $y_2 = \{n_1, n_2\}$. So, by Lemma 4.35, there is a one-step $\langle M, s \rangle \rightsquigarrow \langle M', s' \rangle$ s.t. $(M)/x_2 \approx (M')$ and $[s]/y_2 \approx [s']$. We may now use Lemma 4.36 to obtain $M' \triangleright_* M''$ with $M''$ canonical and $(M') \approx (M'')$. Now, removing $x_2$ and $y_2$ to the sequence above yields

$$ (\emptyset, \emptyset) \leftarrow (x'_3, y'_3) \leftarrow \dots \leftarrow (x'_n, y'_n) = (x, y) $$

with $x' = x \setminus \{m_1, m_2\}$ and $y' = y \setminus \{n_1, n_2\}$, witnessing that matching $x' \in \mathscr{C}((M''))$ and $y' \in \mathscr{C}([s'])$ are causally compatible, so that $x' \otimes y' \in \mathscr{C}((M'') \otimes [s'])$. But $x'$ and $y'$ are $+\text{-covered}$, so $x' \odot y' \in \mathscr{C}((M'') \odot [s'])$, still with a positive move in $\mathbb{U}$. So $\langle M'', s' \rangle \rightsquigarrow \langle \textbf{skip}, s'' \rangle$ by induction hypothesis, so $\langle M', s' \rangle \rightsquigarrow \langle \textbf{skip}, s'' \rangle$ by Lemma 4.36, so $\langle M, s \rangle \rightsquigarrow \langle \textbf{skip}, s'' \rangle$.

*Only if.* By induction on the number of interfering operations in $\langle M, s \rangle \rightsquigarrow \langle \textbf{skip}, s'' \rangle$.

If $M = \textbf{skip}$ it is immediate. Otherwise, consider $\langle M, s \rangle \rightsquigarrow \langle M', s' \rangle \rightsquigarrow \langle \textbf{skip}, s'' \rangle$. By Lemma 4.35, there are $x \in \mathscr{C}((M))$ and $y \in \mathscr{C}([s])$ matching with two elements each, with

$$ (\langle M \rangle)/x \approx (\langle M' \rangle) \qquad [s]/y \approx [s'] $$

Now, to use the induction hypothesis we convert $M' \triangleright_* M''$ to canonical form; by Lemma 4.36 we have $\langle M'', s \rangle \rightsquigarrow \langle \textbf{skip}, s'' \rangle$ with the same number of interfering operations; and $(M') \approx (M'')$. So by induction hypothesis, there are $+\text{-covered}$ and causally compatible

$$ x' \in \mathscr{C}((M'')), \qquad y' \in \mathscr{C}([s]), $$

where $x'$ has an occurrence of the positive event of $\mathbb{U}$; so up to renaming, $x' \in \mathscr{C}((M)/x)$ and $y' \in \mathscr{C}([s]/y)$. Therefore, by definition of residuals, one may add back $x$ and $y$ to obtain

$$ x \cup x' \in \mathscr{C}((M)), \qquad y \cup y' \in \mathscr{C}([s]), $$

$+\text{-covered}$, causally compatible with a positive move in $\mathbb{U}$, which concludes the proof. $\square$

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

### 4.5.2. *Finitary adequacy.*
We deduce recursion-free adequacy from the canonical case.

To convert terms to canonical form, we perform state-free reductions while pushing declarations of new references or semaphores outside. The latter is done by the commutation rules of Figure 41, from which are missing the three rules for the parallel let, and matching commutations for new semaphores. It is direct that these rules leave the game semantics invariant, and preserve and reflect infinite reduction chains in the operational semantics.

Writing $\equiv$ for the congruence closure of state-free reductions and commutations above:

**Lemma 4.38.** Consider $\vdash M : \mathbb{X}$ a recursion-free term of $|\mathcal{A}|$. Then, there exists

$$ M \equiv \text{new } x_1:=n_1 \text{ in } \dots \text{ new } x_p:=n_p \text{ in } N $$

where each **new** is either **newref** or **newsem**, and $\Sigma \vdash N : \mathbb{X}$ is canonical.