Simon Castellan
email: simon.castellan@ens-lyon.fr

Pierre Clairambault
email: pierre.clairambault@ens-lyon.fr

Glynn Winskel
email: glynn.winskel@cl.cam.ac.uk

THIN GAMES WITH SYMMETRY AND CONCURRENT HYLAND-ONG GAMES

Keywords: 1998 ACM Subject Classification: F.3.2 Games, event structures, concurrency

published or not. The documents may come   L'archive ouverte pluridisciplinaire

Introduction

In game semantics, computation is represented within a two-player game played between the program and its execution environment -the program is often considered to be Player and the execution environment Opponent. The two players make moves corresponding to computational events: the program calling an external function is a Player move, and this function returning is an Opponent move. Originally motivated by the very foundational quest of understanding higher-order sequentiality [HO00, AJM00], game semantics developed into a rich subject, with a wide scope spanning logical aspects of computation, through the Curry-Howard correspondence, to the conception of new decision algorithms for equivalence or verification problems on higher-order programs.

Game semantics often plays one of the two following roles in the literature.

(1) A syntax-free, compositional operational semantics. The strategy interpreting a program is a syntax-free object -in essence it is a representation of the behaviour of the program, with no information as to how this behaviour is written down in the syntax. In particular, it abstracts cleanly from the bureaucratic aspects of the syntax and reduction of the language under examination. It is by nature compositional, because the strategy for a term is calculated by induction on its syntax tree, following the methodology of denotational semantics. In particular, the application of one term to another is interpreted as the composition of the corresponding strategies.

A compositional fine-grained description of the execution of higher-order programs is a useful tool -for instance, it provides methodologies to study problems such as termination or complexity in the abstract, in a syntax-free manner [START_REF] Clairambault | Totality in arena games[END_REF][START_REF] Clairambault | Bounding linear head reduction and visible interaction through skeletons[END_REF]. Such a representation is also key to further program analysis. It can provide an invariant for compilation [START_REF] Ghica | Geometry of synthesis: a structured approach to VLSI design[END_REF][START_REF] Schöpp | On the relation of interaction semantics to continuations and defunctionalization[END_REF], or a compositional model construction on which to perform model-checking [START_REF] Abramsky | Applying game semantics to compositional software modeling and verification[END_REF]. Even in the purely functional case, it was recently proposed by Jones et al [START_REF] Berezun | Partial evaluation and normalisation by traversals[END_REF] as a convenient closure-free way to compute the partial evaluation of a term.

Although historically the focus on game semantics has often been on the second role mentioned below, a good part of its recent developments have been indeed as a syntaxfree, compositional operational semantics. In this direction, it is to be compared with various similar frameworks. Normal form bisimulations [START_REF] Søren | Typed normal form bisimulation[END_REF] are close relatives, as recently emphasized by Levy and Staton [START_REF] Blain | Transition systems over games[END_REF]. Recent developments of the geometry of interaction also pursue similar methods and objectives [START_REF] Hoshino | Memoryful geometry of interaction: from coalgebraic components to algebraic effects[END_REF][START_REF] Dal Lago | Parallelism and synchronization in an infinitary context (long version)[END_REF]. Finally, Hirschowitz and collaborators have provided a very general framework in which one can give syntax-free descriptions of different kinds of programs [START_REF] Hirschowitz | Innocent strategies as presheaves and interactive equivalences for CCS[END_REF][START_REF] Eberhart | An intensionally fully-abstract sheaf model for pi[END_REF].

(2) An observational classification of effects. Beyond the use of game semantics as an operational semantics, the separation of the observable behaviour of a term from its syntax allowed researchers to study computational features of programs in terms of the observations that they permitted. One of the most acclaimed achievements of early game semantics is the identification of conditions on strategies (visibility, innocence, well-bracketing) in the context of Hyland-Ong games, that characterize, not syntactically but observationally, the behaviour of programs having access to certain effects. Indeed, innocent well-bracketed strategies are essentially purely functional programs [START_REF] Hyland | On full abstraction for PCF: I, II, and III[END_REF]: relaxing innocence to visibility captures the use of ground state [START_REF] Abramsky | Linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions[END_REF] while removing well-bracketing captures control operators [START_REF] Laird | Full abstraction for functional languages with control[END_REF]. Finally, removing visibility captures terms that have access to higherorder references [START_REF] Abramsky | A fully abstract game semantics for general references[END_REF]. This is known as the semantic cube or Abramsky cube.

Each combination of these conditions corresponds to a certain programming language, for which the strategies have exactly the same observation power as programs. In many cases the resulting model is fully abstract, without the need for a quotient. This allowed researchers in game semantics, starting with Ghica and McCusker [START_REF] Ghica | The regular-language semantics of second-order idealized a lgol[END_REF], to give decision procedures for observational equivalence of programs in certain programming languages where the fully abstract games model is algorithmically presented [START_REF] Murawski | Third-order idealized algol with iteration is decidable[END_REF][START_REF] Cotton-Barratt | Fragments of ML decidable by nested data class memory automata[END_REF].

Despite this impressive flexibility, each game semantics model comes with its limitations. The notion of play, which is at the heart of any game semantics model, specifies the observational power of the execution environment. Whereas the capabilities of Player can be adjusted to a certain extent via conditions on strategies, this cannot be pushed further than what is wired into the model construction. For instance in Hyland and Ong's original model, plays are well-bracketed and visible for both players -it follows that we only observe parts of programs visible to an evaluation context with no access to higher-order state and control operators. Clearly that can be solved; for instance by allowing more general plays as in [START_REF] Abramsky | A fully abstract game semantics for general references[END_REF]. Then again, the whole model has to be rethought if one wishes to allow Opponent to be concurrent. The same line of thought led Ghica and Tzevelekos to define system-level game semantics [START_REF] Ghica | A system-level game semantics[END_REF], in an effort to take as few assumptions as possible as to the power of the execution environment. We advocate here another option, namely to use a causal model.

Causality. In causal game semantics, a program is not represented by an enumeration of all its possible interactions with an Opponent of observational strength wired into the model. Instead, it is represented by an abstract structure displaying information about the causal choices behind the program's actions. On the one hand, this means that the model is more intensional and most likely further away from quotient-free full abstraction results. On the other, the representation makes few assumption as to the computational features available to the execution environment. This makes the model more modular, and a finer representation: from the causal game semantics of a program, it is always possible to recover -in an effective manner -the set of plays corresponding to an observation by a certain kind of environment. The causal representation has other advantages. For instance, as long advocated by Melliès, it allows us to get rid of artificialities in the standard play-based composition mechanism for innocent strategies, making more explicit the fact that it is relational (this is key to the full completeness results for fragments of linear logic [START_REF] Abramsky | Concurrent games and full completeness[END_REF][START_REF] Melliès | Asynchronous games 4: A fully complete model of propositional linear logic[END_REF]). Furthermore, the importance of causal representations for programs has been advocated in the past for various purposes, ranging from error diagnostics [START_REF] Benveniste | Diagnosis of asynchronous discrete-event systems: a net unfolding approach[END_REF] to the study of reversible aspects of computation [START_REF] Cristescu | A compositional semantics for the reversible p-calculus[END_REF]. Last but not least, causal representations display the evolution of a concurrent system with partial orders rather than interleavings (it is "truly concurrent"). Such representations avoid the state explosion problem of interleaving-based ones [START_REF] Godefroid | Partial-Order Methods for the Verification of Concurrent Systems -An Approach to the State-Explosion Problem[END_REF], leading to potential applications to the verification of concurrent systems.

Contributions. Giving causal representations of the execution of programs is not a new problem. Such models have been developed for various process languages, from CCS [START_REF] Winskel | Event structures[END_REF], up to (recently) the full π-calculus [START_REF] Eberhart | An intensionally fully-abstract sheaf model for pi[END_REF][START_REF] Cristescu | Rigid families for CCS and the πcalculus[END_REF]. There seem to exist few developments on truly concurrent semantics of concurrent languages with shared state, with the notable exception of a Petri net semantics for a simple imperative programming language [START_REF] Hayman | Independence and concurrent separation logic[END_REF].

In this paper, we give a general framework in which one can define such truly concurrent models for higher-order concurrent languages, with various synchronization primitives. This has the form of a cartesian closed category of arenas and concurrent strategies, which are certain event structures. The approach is conservative over the category of Hyland-Ong innocent strategies for PCF (and over the more recent work [START_REF] Tsukada | Nondeterminism in game semantics via sheaves[END_REF] in the non-deterministic case), in the sense that a pure term is interpreted as its forest of P-views. In this paper, we develop this category in detail, and illustrate it by spelling out the interpretation of Idealized Parallel Algol (IPA), a higher-order concurrent programming language with shared state and semaphores as synchronization primitives. The methodology is that of game semantics, which provides a well-rooted hope that any of the many languages that one can model in game semantics could be given a truly concurrent representation in this framework as well.

To achieve that, we build on the category CG of concurrent games on event structures introduced by Rideau and Winskel [START_REF] Rideau | Concurrent strategies[END_REF][START_REF] Castellan | Games and strategies as event structures[END_REF], which itself belongs to a family of game semantics focusing on positionality rather than sequentiality initiated by Abramsky and Melliès in [START_REF] Abramsky | Concurrent games and full completeness[END_REF] and subsequently pushed by Melliès and others [START_REF] Melliès | Asynchronous games 4: A fully complete model of propositional linear logic[END_REF][START_REF] Melliès | Asynchronous games: Innocence without alternation[END_REF]. Relative to CG, the main technical difficulty is to handle replication in programming languages: the same resource may be accessed many times, but subsequent behaviour cannot depend on the low-level details of how replication is implemented in the model (it is the uniformity problem solved with equivalence relations in AJM games). The first layer of our framework addresses this difficulty: we first build a compact closed category Tcg, designed to play a similar role as CG in that it offers the basic compositional mechanisms on which further semantic constructions rely, while handling uniformity. Then, relying in Tcg we build the announced cartesian closed category Cho, designed as a conservative extension of usual Hyland-Ong games. We consider the main contributions of this paper to be these two categories of strategies Tcg and Cho; the interpretation of IPA in Cho is mostly there for motivations and illustrations purposes. We insist that the intermediate Tcg is a contribution in itself rather than a means to an end for the construction of Cho; and indeed in some further work we have found it convenient to build on Tcg directly rather than through Cho.

Other work. Here, we find it appropriate to give some further insight on the broader context of the developments presented in this paper. The bulk of the present paper is the detailed construction of the games model used in the conference paper [START_REF] Castellan | The parallel intensionally fully abstract games model of PCF[END_REF] to build a fully abstract games model of PCF based on parallel evaluation. The result of [START_REF] Castellan | The parallel intensionally fully abstract games model of PCF[END_REF] also necessitates the development of a concurrent notion of innocence [START_REF] Hyland | On full abstraction for PCF: I, II, and III[END_REF], not covered here. The approach to uniformity adopted here is that given in [START_REF] Castellan | The parallel intensionally fully abstract games model of PCF[END_REF], rather than the earlier approach of [START_REF] Castellan | Symmetry in concurrent games[END_REF] (which we will however mention in the course of the paper).

Our aim for the current paper is that it serves as a reference for the construction of Tcg and Cho. In that, besides the illustrative interpretation of IPA, it contains no striking application of the framework. Hence, to help motivate the rather lengthy and technically involved model construction, we feel it is helpful to add some further perspective on the use of this model. This framework is a cornerstone for a number of subsequent developments, obtaining achievements that were not within reach with the previously existing tools of game semantics. In [START_REF] Castellan | The parallel intensionally fully abstract games model of PCF[END_REF], pairing Cho with a notion of concurrent innocence we have given a fully abstract model of PCF based on parallel evaluation. This was extended to non-deterministic PCF in the first author's PhD thesis [START_REF] Castellan | Concurrent structures in game semantics[END_REF]. The category Tcg was found to accommodate transparently probabilities, supporting the first notion of probabilistic innocence. This was applied successfully to probabilistic PCF [START_REF] Castellan | The concurrent game semantics of probabilistic PCF[END_REF] and the probabilistic λ-calculus [START_REF] Clairambault | Fully abstract models of the probabilistic lambdacalculus[END_REF]. Besides those a number of developments are currently under way, in which the constructions detailed here play a crucial role. A common trend in all these developments is that further structure sits on Tcg and Cho in a high-level modular way, and do not interact with the details of the construction, making those convenient for further semantic constructions despite their intricacies.

Outline. In Section 2, we give some basic ideas behind the formalization of game semantics on top of event structures, and introduce the key issues that we will have to solve in order to push these ideas to a fully-fledged games model. In particular, we will show that we need to move to a setting of event structures with symmetry, in order to handle uniformity of strategies with respect to replicated resources. In Section 3, we give the first main contribution of this paper: the compact closed category Tcg. In Section 4, we rely on it to construct our cartesian closed category Cho. Finally in Section 5, we illustrate Cho by describing the interpretation of IPA.

Arenas, concurrent strategies, and uniformity

This first section has several purposes: firstly, it aims to introduce the basic ideas behind our concurrent formulation of Hyland-Ong games. Secondly, it recalls from [START_REF] Castellan | Games and strategies as event structures[END_REF] the required preliminaries on games on event structures. Finally, it introduces the main difficulties encountered in trying to obtain a cartesian closed category based on this, motivating the definitions of Section 3.

2.1. Preliminaries on Idealized Parallel Algol. Before presenting our game semantics, we fix a syntax (inspired by [START_REF] Ghica | Angelic semantics of fine-grained concurrency[END_REF]) for Idealized Parallel Algol (IPA). It will not be exactly the same language as in [START_REF] Ghica | Angelic semantics of fine-grained concurrency[END_REF] -notably, it lacks semaphores. We omit them in order to keep the language simple, but they can be interpreted with the same methodology than shared variables. Note that the language is mostly here to fix notations and for providing examples and illustrations. Indeed, the focus on the paper is on the model construction rather than its applications, which will come later in companion papers.

The types of IPA are the following.

A, B ∶∶= com B N A → B ref
The type com is a type of commands, which returns no useful value (if it returns at all, it returns skip), but may perform read/write operations on the memory. The types N and B are types for expressions that (if they return) return respectively a natural number or a boolean. Finally, ref is the type for integer variables. Note that we consider active expressions, i.e. the evaluation of a term of type B or N can trigger side effects.

Raw terms of IPA are described as follows.

M, N ∶∶= x M N λx. M Y tt ff if M N 1 N 2 n succ M pred M iszero M skip M ; N M ∥ N newref r in M M ∶= N !M mkvar
The first three lines describe the syntax of PCF [START_REF] Plotkin | LCF considered as a programming language[END_REF]. The fourth line describes commands and combinators for them. Finally, the fifth line gives the primitives for manipulating variables. We include the so-called bad variable constructor [START_REF] Abramsky | Linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions[END_REF], but it will only play a very minor role in our development.

These terms are subject to mostly standard typing rules. We give most of them in Figure 1, omitting the standard rules for the λ-calculus, the fixpoint combinator, and constants. By convention, we use X to range over ground types: com, B, N. By abuse of notation, we will also use N and B respectively for the sets of (total) natural numbers and booleans.

Although some of our typing rules seem restricted to output ground types, the full rules can be derived as syntactic sugar. For instance, a version of if that eliminates to ref can be obtained as:

Figure 1. Typing rules of IPA Γ ⊢ M ∶ B Γ ⊢ N i ∶ ref Γ ⊢ mkvar (λx. if M (N 1 ∶= x) (N 2 ∶= x)) (if M !N 1 !N 2 ) ∶ ref
It is an easy verification that the other rules can be generalized similarly.

The language can be equipped with standard (small-step) operational semantics, see [START_REF] Ghica | Angelic semantics of fine-grained concurrency[END_REF] for details. We omit it here since it will play no role in the technical development.

2.2. Partial orders and conflicts for strategies. We now start introducing our semantics. In the remainder of this section we introduce gradually the main ideas behind our model, relying as much as possible on examples. Our starting point will be the standard Hyland-Ong innocent semantics for PCF, which we will use to motivate concurrent games on event structures. This section will culminate on the issues of replication and uniformity, which will prompt the developments of Section 3. 2.2.1. Dialogue games. Hyland-Ong games formalize the intuition that a program is a strategy having a dialogue with its execution environment. A possible dialogue on the type B → B → B → B appears in Figure 2. The diagram is read from top to bottom. Each

B → B → B → B q (-, Q) q ✐ ❣ ❢ ❞ ❜ ❛ ❴ (+, Q) tt ✤ (-, A) q ⑧ ⑤ ① ✉ r ♦ ♠ (+, Q) tt ✤ (-, A) tt ✘ ✛ ✢ ✤ ✦ ★ ✫ (+, A) Figure 2. A dialogue on B → B → B → B
move is either by Player or Opponent, and is either a Question or an Answer. Questions correspond to variable calls, whereas Answers indicate a call terminating. The dashed lines between moves (traditionally called justification pointers) convey information about thread indexing; in this example they are redundant but become required at higher types -we will see more on them later.

In natural language, this diagram would read: "The environment starts the evaluation of a term of type B → B → B → B by interrogating its return type (-, Q). The evaluation requires information on the first argument, so the term triggers its evaluation by playing under the corresponding component of the type (+, Q). The evaluation of the argument terminates with value tt (-, A). Knowing that its first argument is tt, the term now needs information on its second argument (+, Q). This argument returns tt (-, A), and now the term computes and returns tt at toplevel (+, A)." The reader should recognize here a description of an execution of if .

In Hyland-Ong games, sequential innocent strategies consist of sets of dialogues as above, where Opponent moves are justified by the preceding one -such dialogues are known as P -views. A strategy for a term of PCF contains several such dialogues, specifying the term entirely. The full strategy for if contains in total four maximal P-views, displayed in Figure 3. Such non-empty sets of P-views (satisfying further conditions: determinism and

B → B → B → B q (-, Q) q ♣ ♠ • ❣ ❞ ❜ ❴ (+, Q) tt ✤ (-, A) q ✍ ☛ ✂ ① t (+, Q) b ✤ (-, A) b ✫ ★ ✦ ✤ ✢ ✛ ✘ (+, A) B → B → B → B q (-, Q) q ♣ • • ❣ ❞ ❛ ❴ (+, Q) ff ✤ (-, A) q ✘ ✏ ✟ (+, Q) b ✤ (-, A) b ✘ ✛ ✢ ✤ ✦ ★ ✫ (+, A)
Figure 3. Maximal P -views for if well-bracketing) are usually called well-bracketed innocent strategies. Because of their correspondence with certain normal forms (PCF Böhm trees [START_REF] Curien | Abstract Böhm trees[END_REF]), they are the cornerstone of Hyland-Ong games and of the full abstraction results they allowed.

2.2.2. Partially ordered dialogues. In Hyland-Ong games, every P-view is a total order, meaning that the whole sequential innocent strategy is a tree. In our framework, we question this premise. For instance, informally, the intuitive behaviour of the parallel composition operation ∥∶ com → com → com of IPA is most elegantly represented as in Figure 4. The diagram of Figure 4 is analogous to the previous ones, but is now partially ordered rather than totally ordered. The relation denotes immediate causality; it was unnecessary before, as it coincided with chronological contiguity. The justification pointers remain -we will see more on their precise nature later. Note that in the standard game semantics for IPA [START_REF] Ghica | Angelic semantics of fine-grained concurrency[END_REF], this partial order would be only implicit; and given by all the possible linear orderings of the partial order above. Here instead, the partial order will be the first-class object of interest. Strategies, in particular, will be partially ordered.

com → com → com run ✴ s s { ♦ ♦ ♦ ♦ ♦ ♦ ♦ ✬ p p w ❣ ❣ ❣ ❣ ❣ ❣ ❣ ❣ ❣ ❣ ❣ ❣ ❣ ❣ ❣ ❣ ❣ ❣ (-, Q) run • • ✐ ❣ ❡ ❝ ❜ ❴ run ✇ ♦ ❤ ❴ (+, Q) done ✗ 9 9 F ❲ ❲ ❲ ❲ ❲ ❲ ❲ ❲ ❲ ❲ ❲ ❲ ❲ ❲ ❲ ❲ ❲ ✤ done ✎ 5 5 C ❖ ❖ ❖ ❖ ❖ ❖ ✤ (-, A) done ✘ ✚ ✢ ✤ ✦ ✩ ✫ (+, A)
Figure 4. A partially ordered dialogue 2.2.3. Non-determinism. Concurrent languages are, in general, non-deterministic. Note that we do not mean non-deterministic in the sense that, as above, the execution admits multiple distinct linear orderings. For us, non-determinism means that execution takes irreconciliable routes, even up to permutation of independent events. We illustrate that by the following two examples.

B q ■ Ø ✠ ✠ ✠ ✈ " " 2 ✻ ✻ ✻ (-, Q) tt / o / o / o ✠ ✈ ff ✻ (+, A) com → com run ✬ p p w ❣ ❣ ❣ ❣ ❣ ❣ ❣ ❣ ❣ ❣ ❣ ❣ ❣ ❣ ❣ ❣ ❣ ❣ ✱ r r z • • • • • • • • • (-, Q) run ❴ • • ❤ ❣ ❡ ❝ ❜ / o / o / o run ❴ ✇ s ♣ • ❢ (+, Q) done ✤ done ✤ ✒ 6 6 D | | | | | | | | (-, A) done ✘ ✚ ✢ ✤ ✦ ✩ ✫ (+, A) Figure 5. Non-deterministic dialogues
In the above two diagrams, the wiggly line

/ o / o
indicates immediate conflict. Two moves/events related by immediate conflict are incompatible, and can never occur together in an execution. Accordingly, the first example is a representation of our strategy for the non-deterministic boolean, which answers either true or false. The second example illustrates another key aspect of our model: we remember explicitly the point of nondeterministic choice. Here, Player silently flips a coin. If the result is heads, they evaluate the argument, then terminate. However, if the result is tails, they evaluate the argument, then diverge. Typical play-based game semantics would forget the halting branch, which is contained in the other. Instead, our model represents the two branches explicitly.

We now show how to make such diagrams formal.

2.3. Prestrategies on arenas.

∀e ∈ E, [e] E = {e ′ ∈ E e ′ ≤ E e} is finite ∀e ∈ E, {e} ∈ Con E ∀X ∈ Con E , ∀Y ⊆ X, Y ∈ Con E ∀X ∈ Con E , ∀e ∈ E, ∀e ′ ∈ X, e ≤ E e ′ ⇒ X ∪ {e} ∈ Con E
The set Con E of consistent subsets specifies which events can occur together in an execution of the system. The states of an event structure E, called the (finite) configurations, are those finite sets x ⊆ E that are both consistent and down-closed (i.e. for all e ∈ x, for all e ′ ≤ e, then e ′ ∈ x) -the set of configurations on E is written C (E), and is partially ordered by inclusion. Configurations with a maximal element are called prime configurations, they are those of the form [e] for e ∈ E (note that we drop the E in [e] E whenever, as above, this is clear from the context) -more generally, we will write [X] E for the down-closure of a set of events X in E. We will also use the notation [e) = [e] ∖ {e}. We write x e -⊂ to mean that e ∈ x and x ∪ {e} ∈ C (E). Finally, when drawing event structures as above, we do not represent the full partial order ≤ but the immediate causality generating it, defined as e e ′ whenever e < e ′ and for any e ≤ e ′′ ≤ e ′ , either e = e ′′ or e ′′ = e ′ . We will often omit the subscripts in ≤ or when they are clear from the context. In this paper, most of the event structures we consider (such as those in the previous subsection) have a simpler consistency structure. Definition 2.2. An event structure with binary conflict is a triple (E, ≤ E , # E ), where ≤ E is a partial order and # E is an irreflexive symmetric binary relation on E, such that:

∀e ∈ E, [e] E is finite ∀e 1 # E e 2 , ∀e 2 ≤ E e ′ 2 , e 1 # E e ′ 2
It is easy to check that an event structure with binary conflict is an event structure, with Con E = {X ∈ P f (E) ∀e 1 , e 2 ∈ X, ¬(e 1 # E e 2 )}. On the other hand, not every event structure can be described via a binary conflict (take e.g. three events with any subset of cardinal less than two being consistent). The strategies in the cartesian closed category we aim to build will only have binary conflict, and accordingly in Section 4 we will restrict to event structures with binary conflict. In the meantime, some aspects of the theoretical development are smoother when carried out with arbirary consistency.

In an event structure with binary conflict, we can trace back conflicts to their original cause. For e 1 # E e 2 we say that the conflict is minimal, written e / o / o E e ′ , iff for all e ′′ ≤ e we have ¬(e ′′ # E e ′ ) and for all e ′′ ≤ e ′ we have ¬(e # E e ′ ). As above, we will often drop the subscripts in # or / o / o when they are clear from the context. Following this notation, all the diagrams of the previous subsection can be regarded as representations of event structures with binary conflict (ignoring the dashed lines).

Games and arenas.

In game semantics, dialogues as in Subsection 2.2 obey the rules of a game inherited from the type. In order to define it, let us first recall the following notion from [START_REF] Castellan | Games and strategies as event structures[END_REF].

Definition 2.3. An event structure with polarities (esp) is an event structure A along with a polarity function pol A ∶ A → {-, +} associating to any event a polarity, that is eitherfor Opponent or + for Player.

By a game, we simply mean an event structure with polarities.

Those games form the objects of the category CG of concurrent games of [START_REF] Castellan | Games and strategies as event structures[END_REF]. As one key aim of the paper is to reconstruct a version of Hyland-Ong games, certain games called arenas will play a particular role in our development (being the objects of our cartesian closed category Cho). Definition 2.4. An arena is a conflict-free (all finite sets consistent) esp/game satisfying:

• Forest. if a 1 , a 2 ≤ a ∈ A, then either a 1 ≤ a 2 or a 2 ≤ a 1 . • Alternation. if a 1 a 2 , then pol(a 1 ) ≠ pol(a 2
). An arena A is negative if all its minimal events have negative polarity.

Arenas are close representations of types. Although formulated a bit differently, our arenas are the same as in [START_REF] Hyland | On full abstraction for PCF: I, II, and III[END_REF] (with the exception of the absence of the Question/Answer labeling, which we do not require: as we do not aim for a full abstraction result, no notion of well-bracketing is needed).

Example 2.5. Leaving for later the general interpretation of types, we have:

B q - ✓ ❆ ✵ ✩ tt + ff + com run - ✤ ✤ done + com → com run - • ✈ ✄ | ❍ ❀ run + ✤ ✤ done +
done - Throughout this paper, we will often omit the semantic brackets on types when this causes no confusion and simply refer to these arenas as B, com, etc.

By convention, we represent immediate causality in arenas by dashed lines ❴ ❴ ❴ rather than . Events are ordered from top to bottom, and are annotated with their polarity. We observe in the third example -and it will be a general fact once we give the formal definitions -that each move in the arena com → com comes from a well-defined occurrence of a base type com in com → com: run -and done + come from the output com, and run + and done -come from the input com. As usual in game semantics, this is used in the representation of dialogues (as in Subsection 2.2): whenever possible, moves are placed under the corresponding base type occurrence.

2.3.3.

Prestrategies. The dialogues of Subsection 2.2, and our notion of strategies (called prestrategies for now -more conditions are to come), will be event structures labeled by a game. In other words, a prestrategy will be an event stucture S along with a labeling function σ ∶ S → A associating to each event in S an image in the game. These labeling functions need to satisfy conditions corresponding to the notion of map of event structures.

Definition 2.6. Let E, F be event structures. A morphism (map) of event structures f ∶ E → F is a function, satisfying:

• Preservation of configurations. For all x ∈ C (E), f x ∈ C (F ),

• Local injectivity. For all e, e ′ ∈ x ∈ C (E), if f e = f e ′ then e = e ′ . Event structures and maps between then form a category E.

A prestrategy on a game A is a map of event structures σ ∶ S → A.

So a prestrategy σ ∶ S → A must only reach valid states of A, and behaves linearly: in a configuration, each event of the game appears at most once. We note in passing that for non-linear languages, this linearity assumption will be circumvented by creating duplicates of events -more on that later.

If σ ∶ S → A is a prestrategy, then S automatically inherits from A a polarity function that we write pol S ∶ S → {-, +}, leaving the dependency on σ implicit. Of course, it is equivalent to require S to be explicitely equipped with polarities, in a way preserved by σ -we then say that σ is a map of esps.

2.3.4. Representations of prestrategies. We will only draw prestrategies with binary conflict. When drawing such a σ ∶ S → A as in Subsection 2.2, we only draw S (more precisely, with immediate causality and immediate conflict / o / o ), where each event is presented as its image through A, and placed under the corresponding ground type occurrence in the type. We use the dashed lines

❴ ❴ ❴
to represent the relation on S induced by immediate causality on A. For instance, the second diagram of Figure 5 is a representation of the map of event structures below.

σ ∶ S G G com → com s 1 ✫ D D ✰ r r y ❦ ❦ ❦ ❦ ❦ ❦ ❦ ❦ ❦ ❦ ❦ ❁ y y Ó ⑤ ⑤ ⑤ ⑤ run q q q ▼ ▼ ▼ s 2 ✘ P P ❴ / o / o / o s 3 ✛ I I ❴ run ✤ ✤ done s 4 ✕ R R s 5 ✗ Q Q ✄ ' ' 8 ❈ ❈ ❈ ❈ done s 6 ✚ W W
As the reader can see, this explicit map notation is a bit cumbersome. Its representation as in Figure 5 conveys the relevant information -the only thing lost is the "name" (s 1 , . . . , s 6 ) of moves in S. More formally, it should be clear to the reader that such a representation displays a finite prestrategy σ ∶ S → A adequately up to isomorphism of prestrategies:

Definition 2.7. Let σ ∶ S → A and τ ∶ T → A be prestrategies. A morphism from σ to τ is a map of event structures f ∶ S → T such that τ ○ f = σ.
Accordingly, an isomorphism between σ and τ is given by (f, g), where f ∶ S → T and g ∶ T → S are maps between σ and τ such that g ○ f = id S and f ○ g = id T . We write σ ≅ τ to mean that σ and τ are isomorphic -in that case we might sometimes say that σ and τ are strongly isomorphic to emphasize the distinction with weak isomorphisms, to be defined in Definition 2.28.

2.4.

Compositional structure. In order to obtain such representations of programs compositionally, the standard methodology of denotational semantics suggests to organize them as a category. Rideau and Winskel [START_REF] Rideau | Concurrent strategies[END_REF] give the basic ingredients for the construction of a (bi)category of games on event structures. We give here the main ideas and definitions, but refer the reader to [START_REF] Castellan | Games and strategies as event structures[END_REF] for a more in-depth construction with proofs.

We start with the following simple definition.

Definition 2.8. The simple parallel composition E 1 ∥ E 2 of two event structures E 1 and E 2 has:

• Events. The disjoint union {1} × E 1 ∪ {2} × E 2 , • Causality. We have (i, e) ≤ E 1 ∥E 2 (j, e ′ ) iff i = j and e ≤ E i e ′ , • Consistency. For X = {1} × X 1 ⊎ {2} × X 2 (often written simply X 1 ∥ X 2 ) a finite subset of E 1 ∥ E 2 , we have X ∈ Con E 1 ∥E 2 iff X 1 ∈ Con E 1 and X 2 ∈ Con E 2 .
The simple parallel composition of event structures with binary conflict still has binary conflict. Simple parallel composition can also be applied to maps In other words, the two event structures are put side by side, without any interaction. If A is a game, then there is also its dual A ⊥ , defined as having the same events, causality, consistency as A, but reversed polarity: pol A ⊥ (a) = -pol A (a). Both operations -∥and (-) ⊥ are defined on all esps/games, but preserve arenas.

f ∶ E → E ′ and g ∶ F → F ′ to form f ∥ g ∶ E ∥ F → E ′ ∥ F ′ in
2.4.1. Morphisms. Given games A and B, a prestrategy from A to B is a prestrategy:

σ ∶ S → A ⊥ ∥ B
We will sometimes write σ ∶ A + G G B to keep the S anonymous. The basic example of a prestrategy from A to A is the copycat strategy. Definition 2.9. Let A be a game. We define an event structure C C A as having:

• Events. Those of A ⊥ ∥ A,

• Causality. The transitive closure of the relation:

{((1, a), (1, a ′ )) a ≤ A ⊥ a ′ } ∪ {((2, a), (2, a ′ )) a ≤ A a ′ }∪ {((1, a), (2, a)) pol A (a) = +} ∪ {((2, a), (1, a)) pol A (a) = -} • Consistency. For X a finite subset of C C A , we have X ∈ Con C C A iff [X] C C A ∈ Con A ⊥ ∥A .
In particular, if A is an arena, then C C A is conflict-free. The copycat prestrategy is the identity function, which is a map of es:

c c A ∶ C C A → A ⊥ ∥ A
Example 2.10. The copycat prestrategy from com → com to itself is:

com → com ⊥ ∥ com → com run - ✫ o o v ❢ ❢❢ ❢❢ ❢❢ ❢❢ ❢❢ ❢ ❢ run + ✱ r r z • • • • ❴ run - ✘ @ @ G ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ✈ • done - ✘ @ @ G ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ✤ run + ❴ ✏ ✌ ✠ ✆ ✁ ⑤ done + ✙ ✤ ✪ done - ✫ o o v ❢❢ ❢❢ ❢❢ ❢❢ ❢❢ ❢❢ ✤ done + ✪ ✤ ✙
Note that the partial order above is a tree, whose branches are exactly the P-views of the usual corresponding copycat strategy in Hyland-Ong games.

2.4.2. Interaction. As usual in game semantics, composition is obtained by a two-step process: parallel interaction, plus hiding. The main difficulty in defining the composition of prestrategies is parallel interaction -we first explain how it is done on a closed interaction between σ ∶ S → A and τ ∶ T → A ⊥ . The interaction of σ and τ , written σ ∧ τ ∶ S ∧ T → A, will be a labeled event structure (by which we mean an event structure S ∧ T with a map σ ∧ τ , the labelling function) describing the behaviours accepted by both σ and τ .

Its construction is done in several stages. Firstly, its states should correspond to certain pairings between matching states of σ and states of τ , i.e. pairs (x, y) ∈ C (S) × C (T ) such that σx = τ y. Note that in such a case, the local injectivity assumption on σ and τ induces a bijection ϕ x,y between x and y -in fact matching pairs (x, y) are in one-to-one correspondence with bijections ϕ ∶ x ≃ y between configurations of S and T such that for all s ∈ x, τ (ϕ s) = σ s, indicating which events synchronise with each other. However, not all such bijections represent valid states of the interaction, as σ and τ might not agree on the order in which to play events in x, y. This is addressed by requiring bijections to be secured, as below.

Definition 2.11. Let σ ∶ S → A and τ ∶ T → A ⊥ be prestrategies. A secured bijection between x ∈ C (S) and y ∈ C (T ) is a bijection ϕ ∶ x ≃ y such that for all s ∈ x we have τ (ϕ s) = σ s, and which is secured, in the sense that the reflexive transitive closure of (s, t)

⊲ (s ′ , t ′ ) ⇔ s < S s ′ ∨ t < T t ′
is a partial order written ≤ ϕ on (the graph of ) ϕ, making (ϕ, ≤ ϕ ) a poset. We write B sec σ,τ the set of secured bijections between σ and τ .

Example 2.12. In the diagram below are represented two prestrategies σ on com ∥ com, and τ on (com ∥ com) ⊥ .

com ∥ com (com ∥ com) ⊥ run - ❴ run - ✯ q q x • • • • • run + ❴ done + ✤ done - ✤ ✕ 8 8 E ❯ ❯ ❯ ❯ ❯ ❯ run +
The dotted line is the only pair in the unique maximal secured bijection in B sec σ,τ . The maximum configurations of σ and τ are matching, but not in a secured way. This gives a notion of state of the interaction, but we expected to build a labeled event structure. Hence we wish to present B sec σ,τ (up to isomorphism) as the set of configurations of an event structure S ∧ T . This is done via the prime construction. Say that a secured bijection (ϕ, ≤ ϕ ) is a prime when it has exactly one maximal element (s ϕ , t ϕ ). In other words, a prime secured bijection is the data of one synchronisation (s ϕ , t ϕ ), plus a causally valid history for it. We now form: Definition 2.13. The event structure S ∧ T is obtained as follows:

• Events. Prime secured bijections ϕ ∈ B sec σ,τ . • Causal order. Inclusion of secured bijections.

• Consistency. For X a finite subset of B sec σ,τ of prime secured bijections, we have X ∈ Con S∧T iff ∪X ∈ B sec σ,τ . There is a map of es σ ∧ τ ∶ S ∧ T → A, given by (σ ∧ τ ) ϕ = σ s ϕ = τ t ϕ .

In passing, we note that if σ ∶ S → A and τ ∶ T → A ⊥ have binary conflict (meaning S and T have binary conflict), then so does σ ∧ τ ∶ S ∧ T → A, with ¬(ϕ 1 # S∧T ϕ 2 ) iff ϕ 1 ∪ ϕ 2 ∈ B sec σ,τ -this easily boils down to the lemma below. Lemma 2.14. Assume σ, τ have binary conflict, and let X be a finite subset of B sec σ,τ . Then the two following statements are equivalent.

(1) We have ∪X ∈ B sec σ,τ , (2) For all ϕ, ψ ∈ X, ¬(ϕ # ψ).

Proof. (1) ⇒ (2). Obvious, since ϕ ∪ ψ is a down-closed subset of ∪X.

(2) ⇒ (1). First we show that ∪X is a bijection from a configuration of S to a configuration of T . Indeed if (s, t 1 ), (s, t 2 ) ∈ ∪X then (s, t 1 ) ∈ ϕ and (s, t 2 ) ∈ ψ for some ϕ, ψ ∈ X. But then ϕ ∪ ψ ∈ B sec σ,τ by hypothesis, so in particular it is a bijection, so t 1 = t 2 . Hence ∪X is a bijection. Furthermore its projections are configurations. Indeed, since X is pairwise compatible, π 1 X is a pairwise compatible set of configurations of S, hence ∪(π 1 X) ∈ C (S) since S has binary conflict -and likewise for ∪(π 2 X). It remains to prove that ∪X is secured. But all ϕ ∈ X are down-closed partial orders induced as subsets of a common preorder of synchronized events. Taking their union cannot introduce cycles, as these would already occur in the separate components by down-closure. Hence ∪X ∈ B sec σ,τ . It will also be useful later to have a concrete understanding of how minimal conflict arises in an interaction; hence we prove the following lemma. The second part of the statement follows easily.

In fact, what we have described above is the pullback construction in E. There are maps of event structures:

Π 1 ∶ S ∧ T → S Π 2 ∶ S ∧ T → T ϕ ↦ s ϕ ϕ ↦ t ϕ
making the following square commute, and a pullback (from Lemma 2.11 of [START_REF] Castellan | Games and strategies as event structures[END_REF]):

S ∧ T Π 1 { { ✈ ✈ ✈ ✈ ✈ Π 2 6 6 ❍ ❍ ❍ ❍ ❍ ❄ ⑧ S σ 5 5 ❍ ❍ ❍ ❍ ❍ T τ z z ✈ ✈ ✈ ✈ ✈
A We motivated the pullback by asking for an es whose configurations are secured bijections. And indeed, those are in a very close correspondence.

Proposition 2.16. For any x ∈ C (S ∧ T ), we have ϕ x = ∪x ∶ Π 1 x ≃ Π 2 x. Moreover, the assignment:

C (S ∧ T ) → B sec σ,τ
x ↦ ϕ x is an order-isormorhism (with both sets ordered by inclusion). Finally, there is a family of order-isomorphisms:

ν x ∶ x ≅ ϕ x ψ ↦ (s ψ , t ψ
) that is natural in x, i.e. for x ⊆ y and ϕ ∈ x we have ν x ϕ = ν y ϕ.

Proof. Direct extension of Lemma 2.9 in [START_REF] Castellan | Games and strategies as event structures[END_REF]. This allows us, when reasoning on configurations of a pullback, to manipulate directly secured bijections rather than compatible sets of prime secured bijections. Likewise, when reasoning on events of the pullback in an ambiant configuration, we can directly apply ν and reason on synchronised pairs. In the proofs, we will often use this proposition implicitely and transfer silently between the different representations.

Finally, we are in position to define the parallel interaction of two prestrategies σ ∶ S → A ⊥ ∥ B and τ ∶ T → B ⊥ ∥ C. We simply form the pullback:

(σ ∥ C) ∧ (A ∥ τ ) Π 1 w w ♣ ♣ ♣ ♣ ♣ ♣ ♣ Π 2 9 9 ◆ ◆ ◆ ◆ ◆ ◆ ◆ ❄ ⑧ S ∥ C σ∥C 9 9 ◆ ◆ ◆ ◆ ◆ ◆ ◆ A ∥ T A∥τ w w ♣ ♣ ♣ ♣ ♣ ♣ ♣ A ∥ B ∥ C
We write T ⊛ S = (σ ∥ C) ∧ (A ∥ τ ) for the interaction, and τ ⊛ σ ∶ T ⊛ S → A ∥ B ∥ C for either side of the pullback square. Hence we get the interaction of σ and τ , τ ⊛ σ, as a labeled event structure.

Example 2.17. Consider the following prestrategies σ ∶ S → com → com and τ ∶ T → com → com ⊥ ∥ com (note that to match the definition of interaction above, we can consider σ ∶ S → 1 ⊥ ∥ com → com , where 1 is the empty arena).

σ ∶ com → com τ ∶ com → com ⊥ ∥ com run - ✲ s s z ♠ ♠ ♠ run - ✲ s s z ♠ ♠ ♠ run + ① ♠ ❴ run + ✇ ♠ ✯ q q x • • • • • • ❴ done - ✤ ✑ 6 6 D ◗ ◗ ◗ run - r • ❝ ✷ u u } r r ✟ 0 0 @ ❍ ❍ done - ✤ ✑ 6 6 D ◗ ◗ ◗ done + ✙ ✤ ✪ done + r / o / o / o / o done + ❍ done + ✙ ✤ ✪
We display below a representation of the interaction:

τ ⊛ σ ∶ T ⊛ S → (com → com) ∥ com
We only display polarities for the moves in the right hand side com. Indeed events on the left hand side (synchronised) part of the interaction have no well-defined polarity, as the two strategies disagree on them.

τ ⊛ σ ∶ (com → com) ∥ com run - ★ n n t ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ ❝ run ★ n n t ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ ❝ run ❣ ❡ ❝ ❛ ❴ ✰ r r y ✓ 7 7 D done ❦ / o / o / o / o ✛ B B H ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ done ❙ ✚ A A H ) ) ) ) ) ) ) ) ) ) ) ) ) done ✍ ✄ ✈ ✚ A A H ) ) ) ) ) ) ) ) ) ) ) ) ) done ✵ ❀ ❍ ✛ B B H ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ done + ✗ ✔ ✑ ✍ ☛ ✞ ✄ done + ✬ ✯ ✲ ✵ ✸ ✼ ❀
We leave it to the reader to check that each event in this diagram corresponds uniquely to a configuration in S ∥ com and a matching configuration in T such that the induced bijection is secured. 2.4.3. Hiding. Once we have performed the interaction, it is fairly simple to obtain the composition by ignoring the synchronised events, i.e. those that map to B. This is an instance of the following projection operation. Definition 2.18. Let E be an event structure, and V ⊆ E a set of events of E. The projection of E to V , written E ↓ V , has components:

• Events. V . • Causality. The order ≤ E restricted to V . • Consistency. The sets X ∈ Con E such that X ⊆ V .
This gives an event structure -it is clear that a hiding of an event structure with binary conflict still has binary conflict. Note as well the unique witness property reminiscent of that used in studying the composition of deterministic strategies in standard game semantics: for any x ∈ C (E ↓ V ), there exists a unique y ∈ C (E) such that y ∩ V = x, and whose maximal events are those of x; obtained as y =

[x] E = {e ∈ E ∃e ′ ∈ x, e ≤ E e ′ } ∈ C (E).
Finally, we define composition. From

σ ∶ S → A ⊥ ∥ B and τ ∶ T → B ⊥ ∥ C, first compute the interaction τ ⊛ σ ∶ T ⊛ S → A ∥ B ∥ C. Then, set V ⊆ T ⊛ S to comprise all ϕ ∈ T ⊛ S such that (τ ⊛ σ) ϕ ∈ B. Writing T ⊙ S = T ⊛ S ↓ V ,
the composition of σ and τ is:

τ ⊙ σ ∶ T ⊙ S → A ⊥ ∥ C ϕ ↦ (τ ⊛ σ) ϕ
From the fact that interaction and hiding preserve binary conflict, it follows that for σ ∶ S → A ⊥ ∥ B and τ ∶ T → B ⊥ ∥ C, if S, T, A, C have binary conflict, then so does T ⊙ S.

Example 2.19. Consider the interaction of Example 2.17. After hiding, the resulting composition is:

com run - ✶ t t } q q ✌ 3 3 B ▼ ▼ done + q / o / o / o / o done + ▼
Note that the conflict between the two maximal events, although it was inherited in the interaction, becomes minimal after projection as its original cause has been hidden away.

Composition is associative up to isomorphism [START_REF] Castellan | Games and strategies as event structures[END_REF]. However, copycat is not neutral for composition with respect to prestrategies -it is only the case for strategies (see [START_REF] Castellan | Games and strategies as event structures[END_REF] for details): Definition 2.20. A prestrategy σ ∶ S → A on a game A is a strategy if it is:

• Receptive. For all x ∈ C (S), if σx a - -⊂ , then there exists a unique s ∈ S such that

x s -⊂ and σ s = a. • Courteous. If s 1 S s 2 and pol(s 1 ) = + or pol(s 2 ) = -, then σ s 1 A σ s 2 .
Putting everything together, we get [CCRW17]:

Theorem 2.21. There is a compact closed category CG of games and strategies up to isomorphism.

2.5. Interpreting programs and replication. The category CG is a general framework for composing concurrent strategies. We can rely on it to build a model of an affine variant of IPA: that involves restricting to negative arenas, and interpreting function space in IPA via the usual arrow arena construction. We refrain from giving the details here, since we will give them in the non-affine case later on. However, before going on to handling replication, we will give examples in the affine case and try to convey further intuition as to what the model computes. Then we will present the expanded arenas used to handle replication, and we will introduce the issue of uniformity. 2.5.1. Concurrent strategies and view functions. As the reader familiar with Hyland-Ong games may have noticed, our examples before showed how to represent as concurrent strategies, view functions rather than expanded strategies -or, in Curien's terminology [START_REF] Curien | Abstract Böhm trees[END_REF], meager rather than fat innocent strategies. And indeed, in our framework it is the case that a pure program will be interpreted directly as its view function, never constructing the full set of plays. For illustration, the interpretation of the affine pure program:

λf B→com .f tt ∶ (B → com) → com
will be the strategy:

(B → com) → com run - ✱ r r z • • • • run + ✈ • ✵ t t | ♣ ♣ ♣ ♣ ❴ q - ⑥ ♣ ❴ done - ✑ 6 6 D ◗ ◗ ◗ ✤ tt + ✤ done + ✙ ✤ ✪
which the reader can match against the tree of P -views for the corresponding Hyland-Ong innocent strategy. The composition of such strategies is computed directly using pullbacks in E, never constructing the expanded plays. In other words, we never work with full Hyland-Ong strategies, but always with their causal representations: the view functions. But the usual strategies for stateful programs [START_REF] Abramsky | Linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions[END_REF] are not generalizations of meager innocent strategies, but of fat ones: the behaviour of programs must be observed not only on P-views but on general plays. Hence, the reader may wonder if evading them causes us to lose that ability. Fortunately it is not the case, and strategies for stateful programs can be represented causally just as innocent strategies. For instance, consider the following example.

Example 2.22. Consider the following term of IA.

newref b in λf com→com . f (b ∶= tt); !b ∶ (com → com) → B
Following (the affine variant of) the interpretation of Section 5, it yields the strategy:

(com → com) → B q - ✲ s s z ♠ ♠ ♠ ♠ ♠ ♠ ♠ run + ❴ ✉ ♠ ❢ ✭ p p w ❤ ❤ ❤ ❤ ❤ ❤ ❤ ❤ ❤ ❤ ❤ run - ✸ u u ~ss s s ☛ 2 2 A ❑ ❑ ❑ ❑ ✘ @ @ G ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ♠ ❦ ❤ ❢ ❞ done - ✟ 0 0 @ ❍ ❍ ❍ ❍ ✕ 8 8 E ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ✤ ✷ u u } r r r r done + / o / o / o / o / o / o s , l , l , l -m -m -m -m . n . n . n . n / o / o / o / o /
o 0 p 0 p 0 p 0 p 1 q 1 q 1 q 1 q 2 r 2 r 2 r 2 r

done + / o / o / o / o / o / o ❃ ❑ tt + / o / o / o ✜ ✚ ✗ ✕ ✒ ✎ ☞ ff + ✧ ✩ ✬ ✮ ✱ ✴ ✷
The done + to the left is duplicated, witnessing the two outcomes of the race in the memory that happens if the argument does not respect the evaluation stack, and concurrently returns done -and asks for its argument. The reader familiar with the game semantics for Idealized Algol [START_REF] Abramsky | Linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions[END_REF] can check that taking the set of (well-bracketed) alternating linear orderings of configurations of this event structure yields the expected set of plays. 2.5.2. Replication. But so far, we have only seen affine programs and strategies, i.e. that call each resource at most once. As it stands, the local injectivity condition in Definition 2.6 forbids us from having two compatible events corresponding to the same move in the game. It is natural to consider dropping it, but then we lose access to the nice structural properties of E (such as pullbacks). It is unclear to us how one would go about defining composition of strategies in such a setting, let alone proving that it forms a category; in particular if one insists on remembering the point of non-deterministic branching.

Instead, the solution behind our category Cho takes inspiration from AJM games [AJM00] and from the reconstruction of HO games in [START_REF] Harmer | Categorical combinatorics for innocent strategies[END_REF] : we explicitly duplicate moves in arenas. Rather than playing directly on an arena A, our strategies play in !A, a variant of A with events duplicated countably many times, in depth. More formally: Definition 2.23. Let A be an arena, and a ∈ A. An indexing function for a is a function:

α ∶ [a] → ω
which associates, to a and its dependencies, a copy index. From α ∶ [a] → ω, we write lbl α = a for its label, and ind α = α (lbl α) for the copy index of a. Indexing functions will be the events of !A. Its full structure will be: Definition 2.24. From an arena A, we build a new arena !A, comprising:

• Events. indexing functions α ∶ [a] → ω, • Causal order. for α ∶ [a] → ω and β ∶ [b] → ω, we have α ≤ !A β iff a ≤ A b and for all a ′ ≤ A a, α(a ′ ) = β(a ′ ). • Polarity. For α ∈ !A, pol !A (α) = pol A (lbl α).
Moves in !A have a rather complex structure. However, note that just as A -which was required to be an arena rather than a general game -!A is a forest. For each α ∶ [a] → ω, either a is minimal and then so is α, or there is a unique a ′ A a -in which case the restriction of α to [a ′ ] gives a unique α ′ such that α ′ !A α. In other words, α is entirely determined by the data of lbl α = a, ind α = α(a), and its immediate predecessor α ′ , called its justifier just(α). Using this decomposition inductively, we can unambiguously draw configurations of !A by annotating each event by its copy index, and its justifier.

Example 2.25. The following is a representation of a configuration of !B:

q 0 q 3 tt 1 ✌ ⑥ ♦ tt 4 ✶ ❆ ❖ tt 1 ☞ ⑤ ♦ ff 2 ff 6 ❇
where, e.g. the events labeled tt 1 respectively denote {q ↦ 0, tt ↦ 1} and {q ↦ 3, tt ↦ 1}.

Using the additional space granted by !A, we can now represent programs evaluating their arguments multiple times. For instance, a valid strategy σ ∶ S → ! (B → B) → B → B for the term λf B→B x B . f (f x) could contain, for i, j ∈ ω and injective function ⟨-, -⟩ ∶ ω 2 → ω, a configuration:

(B → B) → B → B q -,i ✫ o o v ❢❢ ❢❢ ❢❢ ❢❢ ❢❢ ❢❢ ❢ q +,0 • ❤ ❢ ❝ ❛ ✲ s s z ♠ ♠ ♠ q -,j ♠ ✑ 6 6 D ◗ ◗ q +,j+1 ① ✈ s ♣ ♥ • ✳ s s { ♥ ♥ q -,k ♥ ✘ @ @ G ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ q +,⟨j,k⟩ ☞ ✍ ✑ ✓ ✕ ✗
This diagram exploits the representation introduced just above for configurations of !A: each event is specified through its label and copy index. The full strategy σ would comprise such configurations for all i, j ∈ ω. For each positive event, σ must provide a copy index -this choice must be made globally, in a way that avoids collisions to maintain local injectivity of σ.

2.5.3. Strategies up to copy indices. Using the composition mechanism introduced before, one may define an interpretation of terms of IPA as concurrent strategies on expanded arenas. However, as observed above, such strategies not only carry information about the events they play and their causal history, but also the data of specific copy indices that seem largely irrelevant -e.g., as above, the choice of an injection ⟨-, -⟩. In fact, for reasons familiar from AJM games [AJM00], strategies will not satisfy the laws of cartesian closed categories unless we consider them up to their specific choice of copy indices. Let us observe that on an example.

Example 2.26. Consider the term M to be f

∶ B → B → B ⊢ λx B . f x x ∶ B → B. Its interpretation could contain: ! B → B → B → ! B → B q -,i ✪ o o u ❡❡ ❡❡ ❡❡ ❡ ❡❡ ❡❡ ❡ ❡❡ ❡❡ ❡❡ q +,i ✯ q q x • • • • • • • • ✼ w w Ñ ✇ ✇ q -,j 1 q • ❞ ✘ @ @ G ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ q -,j 2 ✇ ✘ @ @ G ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ q +,2j 1 ☎ ✁ ⑦ ④ ① ✉ q +,2j 2 +1 ✖ ✓ ✏ ✌ ✡ ✞
Because of the contraction, the Opponent events of indices j 1 and j 2 corresponding to different events in the arena trigger Player events corresponding to the same event in the arena. Local injectivity is ensured by the functions 2n and 2n + 1 having disjoint codomain. Likewise, consider two terms, with chosen configurations of their strategies:

λx B y B . x ∶ ! B → B → B q -,i ✳ s s { ♥ ♥ ♥ ♥ ♥ q +,0 ① ♥ ❢ λx B y B . y ∶ ! B → B → B q -,i ✽ w w Ñ ① ① q +,0

①

Then we have:

M ⊙ λx B y B . x ∶ ! B → B q -,i ✽ w w Ñ ① ① q +,0 ① M ⊙ λx B y B . y ∶ ! B → B q -,i ✽ w w Ñ ① ① q +,1

①

These are required to be the same by the laws of cartesian closed categories, since (λf. M ) (λxy. x) = β (λf. M ) (λxy. y). However, they are not isomorphic as strategies.

In order to solve this mismatch, we first need to formalize what it means for two configurations of !A to be the same up to the choice of copy indices.

Definition 2.27. Let x, y ∈ C (!A). A reindexing iso between x and y is an orderisomorphism:

θ ∶ x ≅ y which preserves labels: for all α ∈ x, lbl α = lbl (θ α).

A reindexing iso θ ∶ x ≅ y is positive iff it preserves the copy index of negative events, i.e. for all α -∈ x, ind α = ind (θ α). Negative reindexing isos are defined dually.

Intuitively, two configurations of C (!A) related by a reindexing iso are distinct representations of one thick subtree of A in the sense of Boudes [START_REF] Boudes | Thick subtrees, games and experiments[END_REF], i.e. a subtree of the arena with duplicated sub-arenas. Two strategies are to be identified iff they are isomorphic, with the commuting triangle to !A being weakened to a commutation up to reindexing iso -in fact, it turns out to be simpler to strengthen that to positive reindexing isos. Altogether:

Definition 2.28. Let σ ∶ S → !A, τ ∶ T → !A be two strategies. A weak morphism from σ to τ is f ∶ S → T , such that the triangle S f A A σ 2 2 ❇ ❇ T τ } } ⑤ ⑤ !A
commutes up to positive symmetry, in the sense that for all x ∈ C (S), the set:

{(σ s, τ (f s)) s ∈ x} is a positive reindexing iso. If f ∶ S → T , g ∶ T → S
are two weak morphisms such that g ○ f = id S and f ○ g = id T , we say that (f, g) is a weak isomorphism, and write σ ≈ τ to mean that σ and τ are weakly isomorphic.

The two strategies of Example 2.26 are weakly isomorphic. And in fact, a consequence of the developments of this paper is that the natural interpretation of terms ⊢ M ∶ A of PCF as strategies on !A hinted at here is sound and computationally adequate (it is reasonable to expect the same statement for IPA to be true as well, but it does not follow from the results in this paper). However, proving it bumps into a significant difficulty: without further contraints on strategies, weak isomorphism is not a congruence. Indeed, strategies can behave differently depending on Opponent's choice of copy indices. For instance, composing the two weakly isomorphic M ⊙ λx B y B . x and M ⊙ λx B y B . y of Example 2.26 with

B → B → B → B q -,i ✯ q q x • • • • • • • • • • q +,i ✫ o o v ❢ ❢ ❢ ❢ ❢ ❢ ❢❢ ❢ ❢ ❢ ❢ ❢ ❢ ❢❢ ✯ q q x • • • • • • • • • ✺ v v ✉ ✉ q -,0 ✚ A A H ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) • ❤ ❢ ❞ ❜ ❛ q -,1 ♣ ♠ • ❣ ❞ q -,i ✉ q +,0 ✗ ✕ ✒ ✎ ☞ ✟
yields, in the one hand, a strategy that calls its argument, and on the other, one that does not. Clearly, they are not weakly isomorphic. This is because the strategy above is not uniform: its behaviour not only depends on Opponent's moves, but also on their copy index. A useful analogy is that of a program that looks up the address where it is loaded in memory, and uses that information to specify its behaviour.

In AJM games [START_REF] Abramsky | Full abstraction for PCF[END_REF], uniformity is ensured by equipping games with an equivalence relation on plays not unlike our reindexing isomorphisms, and then requiring strategies to satisfy closure properties with respect to it. Our approach to uniformity bears some resemblance with that, but the richer structure of our plays prevents us from following the AJM recipe directly. To conclude this section and transition to the next, we give a few ideas motivating our approach to uniformity as detailed in the next section.

In traditional game semantics, plays are sequences of moves, i.e. total orders. Hence, the mere fact that two plays s 1 and s 2 (necessarily of the same length) are in relation in AJM games informs a one-to-one correspondence between the moves appearing in s 1 and those appearing in s 2 . In contrast, in our present setting the states (in the game) are partially ordered configurations x ∈ C (!A), so an equivalence x ∼ !A y between x, y ∈ C (!A) no longer informs such a one-to-one correspondence. This correspondence will then have to become primitive: the equivalence between two configurations must be witnessed by a specific isomorphism, such as a reindexing iso. We like indeed to think of the set of reindexing isomorphisms as forming a "proof-relevant" equivalence relation between configurations of !A -it expresses not only which configurations are in relation, but also how.

How, then, to express that a strategy σ ∶ S → !A is uniform? It is tempting, for x, y ∈ C (S), to simply set x ∼ S y when σx ∼ !A σy -the witness isomorphism σx ≅ σy then informing an isomorphism x ≅ y. This yields a set of isomorphisms between configurations of S, which then may be asked to satisfy closure properties ensuring uniformity. However, it turns out that this is too much to ask: such a simple definition rejects perfectly uniform strategies, some of which are definable through IPA. Intuitively (and unlike for the deterministic sequential strategies of AJM games), a term/strategy may play symmetric moves for non-symmetric reasons. So we opt instead for a more intensional option: we endow strategies with their own "proof-relevant equivalence relation" expressing which configurations they considers equivalent, and how. This "uniformity witness" is part of strategies with symmetry, and propagated through composition and other constructions on strategies. It cannot be recovered uniquely (except for innocent strategies [START_REF] Castellan | The parallel intensionally fully abstract games model of PCF[END_REF], though this is out of scope for this paper) -Appendix A.1 contains a more detailed discussion along the lines of this paragraph, with examples.

We now go on to the formalization of these ideas.

Thin concurrent games

Dealing with uniformity requires us to replicate the construction of concurrent games in a more expressive setting, capable to express that certain events or configurations might be symmetric, i.e. interchangeable; making their indistinguishability part of the structure. Event structures with symmetry [START_REF] Winskel | Event structures with symmetry[END_REF] were designed precisely to cope with such situations. In this section, we construct a replacement for CG based on those, enforcing uniformity of strategies over symmetric events, and hence supporting uniform replication.

In the previous section, a game was an event structure structure A, while a strategy was an event structure S labeled by A, i.e. a map σ ∶ S → A in the category E of event structures and maps between them -furthermore, composition of strategies was obtained by leveraging universal constructions in E, e.g. pullback for interaction. In order to build games with symmetry, it is mathematically appealing to replicate the definitions and constructions, but this time based on the category E ∼ of event structures with symmetry and maps between them (to be defined in Definition 3.6). It is also as economical as we can do with the generality we wish to give the model (and in particular, so that it supports IPA) -we have explored a number of simpler alternatives, which fail in various ways.

In Section 3.1, we first recall event structures with symmetry, and expand on the above methodology for enriching concurrent games with symmetry. Though mathematically appealing, pushing these guidelines bumps against significant obstacles, allowing for two main solutions: the saturated (or fat) and thin approaches (respectively appearing in conference papers [START_REF] Castellan | Symmetry in concurrent games[END_REF] and [START_REF] Castellan | The parallel intensionally fully abstract games model of PCF[END_REF]). After briefly reviewing the fat case, the rest of the section commits to the thin. In Section 3.2, we develop thin concurrent games, focusing on the problem of uniformity, which imposes the most constraints on their design. Finally in Section 3.3, we show that thin games with symmetry form a compact closed category. Then, before going further along the main narrative of the paper and constructing the cartesian closed category of Concurrent Hyland-Ong games in Section 4, we show that Tcg also supports the construction of an AJM-style exponential modality.

3.1. Symmetry on event structures and games. In this first part, we review the main technical tool -event structures with symmetry -and introduce the main challenges in constructing games based on those.

3.1.1. Event structures with symmetry. Intuitively, symmetry on event structures should behave as an equivalence relation, but also satisfy bisimulation-like properties in order to ensure that symmetric states have the same futures (up to symmetry). Looking for a notion of symmetry on event structures satisfying these two aspects, a natural methodology is to instantiate known categorical constructions.

In their seminar paper [JNW93], Joyal, Nielsen and Winskel gave a categorical notion of bisimulation between objects E and F as a span

B l 6⑥ ⑥ ⑥ r 2 2 ❆ ❆ ❆ ❆ E F
where l and r are open maps, i.e. satisfy a path lifting condition formulated as a factorisation property. Winskel later defined an event structure with symmetry in [START_REF] Winskel | Event structures with symmetry[END_REF] as an event structure E with a span of open maps as above (with E = F ), additionally satisfying categorical formulations of the laws of equivalence relations -we omit details, opting below for a more concrete equivalent definition. Besides their algebraic genesis, event structures with symmetry have already proved adequate as a modeling framework: most notably, Hayman and Winskel proved in [START_REF] Hayman | The unfolding of general petri nets[END_REF] that the universal characterization of the unfolding of safe Petri nets as event structures could be extended to general Petri nets, provided one unfolds to event structures with symmetry -the multiple tokens in one place yielding distinct yet symmetric copies of enabled transitions. Symmetry on event structures can be also defined via isomorphism families [START_REF] Winskel | Event structures with symmetry[END_REF].

Definition 3.1 (Isomorphism families and event structures with symmetry). Let A be an event structure and à be a set of bijections between configurations of A. Then, à is an isomorphism family on A if it satisfies:

• (Groupoid) The set à contains all identity bijections, and is stable under composition and inverse of bijections.

• (Restriction) For every bijection θ ∶ x ≃ y ∈ Ã and x ′ ∈ C (A) such that x ′ ⊆ x, then the restriction θ ↾ x ′ of θ to x ′ is in Ã. In particular, θ x ′ ∈ C (A). • (Extension) For every θ ∶ x ≃ y ∈ Ã and extension x ⊆ x ′ ∈ C (A), there exists a (non- necessarily unique) y ⊆ y ′ ∈ C (A) and an extension θ ⊆ θ ′ such that θ ′ ∶ x ′ ≃ y ′ ∈ Ã.
In this case the pair A = (A, Ã) is called an event structure with symmetry (ess). We will use S, T , A, B, . . . to range over event structures with symmetry. If A additionally has polarities and bijections in à preserve them, we say that A is an event structure with symmetry and polarities (essp).

One natural way to think of an isomorphism family is as a proof-relevant historypreserving bisimulation and equivalence relation between configurations: the equivalence between configurations is witnessed by precise bijections between their events.

The following represents a rather trivial example of an event structure with symmetry:

1 W W 7 7 o o G G 2 y y e e
with events {1, 2}, no non-trivial causality and all finite sets consistent, and symmetry comprising all bijections between configurations meaning that all events are interchangeable. In this diagram we use an arrow o o G G to convey the information that events are symmetric.

In general however, the information of symmetry is more contextual and cannot be represented that easily. For instance, one may consider an event structure with symmetry with events {1, 2, 1 ′ , 2 ′ }, trivial causality and all finite sets consistents, and symmetry comprising all bijections between configurations that are subsets of two maximal bijections:

1 o o G G 1 2 o o G G 2 1 ′ o o G G 1 ′ 2 ′ o o G G 2 ′ 1 2 2 ❅ ❅ ❅ ❅ ❅ ❅ ❅ ❅ 1 2 1 1 ❄ ❄ ❄ ❄ ❄ ❄ ❄ ❄ 2 1 ′ ~b b ⑦ ⑦ ⑦ ⑦ ⑦ ⑦ ⑦ ⑦ 1 ′ 2 ′ c c ⑧ ⑧ ⑧ ⑧ ⑧ ⑧ ⑧ ⑧
2 ′ It is a good exercise to verify that this yields an event structure with symmetry. There one can observe that from the empty bijection one can put 2 and 2 ′ in correspondance, however if (1, 1) is already in the bijection, then its extension with (2, 2 ′ ) forms the bijection between configurations {(1, 1), (2, 2 ′ )} which is not in the isomorphism family, not being a subset of either of the bijections above. In that sense symmetry is contextual: whether two events can be interchanged depends on which events have already been exchanged. Being sets of bijections, symmetries on event structures are rather hard to picture. In this paper, most diagrams representing event structures with symmetry will only display the event structure (the observable actions) and keep the symmetry (witnessing uniformity) implicit.

The following lemma, easy consequence of the (Restriction) axiom, is important to keep in mind when manipulating symmetry: Lemma 3.2. Let A be an ess and θ ∶ x ≃ y ∈ Ã. Then, θ is an order-isomorphism.

Hence, if θ ∈ Ã, we write θ ∶ x ≅ y (rather than just x ≃ y) to indicate that θ preserves and reflects the (implicit, inherited from ≤ A ) ordering on x and y. Instead of θ ∶ x ≅ y ∈ Ã, we will also often use the more compact notation θ ∶ x ≅ Ã y; and we will refer to θ as a symmetry between x and y. Given a symmetry θ, we write dom θ and codom θ for its domain and codomain respectively.

3.1.2. Constructions on ess. In the interpretation of games, as discussed in Section 2.5.3 all non-trivial symmetries come from replication. Accordingly our key construction of ess comes from the discussion of Section 2.5.2 -the following is established by a direct verification.

Proposition 3.3. Let A be an arena. Recall !A (Definition 2.24) whose events are functions α ∶ [a] → N with a ∈ A. The sets ! A of reindexing isos (see Definition 2.27), ! A -of negative reindexing isos, and ! A + of positive reindexing isos, are isomorphism families on !A.

This will be at the heart of our construction of the cartesian closed category of concurrent Hyland-Ong games, in Section 4. We mention in passing another construction on event structures with symmetry, more reminiscent of AJM games [START_REF] Abramsky | Full abstraction for PCF[END_REF].

Definition 3.4. If A is an ess, then ! AJM A has events, causality, consistency that of ∥ ω A. Its isomorphism family comprises those bijections θ ∶ ∥ i∈I x i ≃ ∥ j∈J y j such that there exists a permutation π ∶ I ≃ J, and for all i ∈ I a symmetry

θ i ∶ x i ≅ A y π(i) such that for all (i, a) ∈ ∥ i∈I x i , we have θ(i, a) = (π(i), θ i (a)).
The reader familiar with AJM games will recognize the similarity with the definition of the equivalence relation between plays in an exponential games in the AJM setting. In this paper we focus on HO-style games, but it has become crucial in further work that our setting with symmetry supports AJM-style games as well -we will come back to that in Section 3.3.4. Throughout the paper we reserve the notation ! for HO-style replication, i.e. the ess !A of Proposition 3.3 from an arena A. In contrast, the AJM-style exponential will always be denoted by ! AJM to reflect its lesser importance in the present development.

Besides the above, ess support all the basic constructions on event structures.

Definition 3.5. Let A and B be ess. We build their simple parallel composition as

(A ∥ B, à ∥ B) where à ∥ B is the set of bijections of the form θ 1 ∥ θ 2 ∶ x ∥ y ≃ x ′ ∥ y ′ where x, x ′ ∈ C (A), y, y ′ ∈ C (B), θ 1 ∈ Ã, θ 2 ∈ B and θ 1 ∥ θ 2 is defined as (i, a) ↦ (i, θ i (a)).
If A is a game with symmetry, its dual A ⊥ has the same isomorphism family à on A ⊥ .

3.1.3. Categorical structure. Just as maps of event structures were at the heart of the construction of concurrent games, games with symmetry will make use of maps between ess.

Definition 3.6. Let A, B be event structures with symmetry. A map of event structures f ∶ A → B preserves symmetry iff for all θ ∶ x ≅ Ã y, the bijection

f θ = {(f a, f a ′ ) (a, a ′ ) ∈ θ} is in B.
In that case, f is a map of event stuctures with symmetry, written f ∶ A → B.

Event structures with symmetry and their maps form a category written E ∼ . Finally, if A, B have polarities, maps are required to preserve those as well.

In E ∼ , morphisms can be compared up to symmetry, abstracting away from the comparison of morphisms up to the choice of copy indices of the previous section.

Definition 3.7. Let f, g ∶ A → B be maps of event structures with symmetry. They are symmetric (written f ∼ B g) when for all x ∈ C (A), the bijection {(f s, gs) s ∈ x} is in B.

As usual, we write f ∼ g instead of f ∼ B g when B is clear from the context. With this definition, we will be able to reformulate Definition 2.28 by requiring the triangle to commute up to symmetry, i.e. τ ○ f ∼ σ (postponed for now).

3.1.4. Pullbacks and pseudo-pullbacks. The construction of CG relies crucially on properties of the category E of event structures and their maps. In order to construct games with symmetry, it is appealing to attempt replicating the same constructions, but building on E ∼ rather than E. In other words, a game with symmetry would be an ess A with polarities, and a strategy on A would be a map σ ∶ S → A between ess. A strategy from A to B would be σ ∶ S → A ⊥ ∥ B, and those would be composed by pullback as in Section 2, and so on.

A first obstacle in replicating those constructions is that unlike E, the category E ∼ does not have all pullbacks (a proof of that appears in Appendix A.2) -one may understand that by the fact that E ∼ really may be more adequately regarded as enriched over equivalence relations: indeed, maps should be compared up to symmetry rather than on the nose. Hence, one is tempted to have the role of pullbacks played by a universal construction taking symmetry into account, such as pseudo-pullbacks or bi-pullbacks.

Definition 3.8. Let f ∶ A → C and g ∶ B → C in E ∼ . A pseudo-pullback of f and g is P Π 1 7⑦ ⑦ ⑦ Π 2 1 1 ❅ ❅ ❅ ❅ ❄ ⑧ A ∼ f 2 2 ❅ ❅ ❅ ❅ B g ⑦ ⑦ ⑦ ⑦ C
commuting up to symmetry, and such that for all

f ′ ∶ X → A, g ′ ∶ X → B such that f ○ f ′ ∼ g ○ g ′ there exists a unique map h ∶ X → P such that Π 1 ○ f = f ′ and Π 2 ○ g = g ′ . It is a bi-pullback iff for all f ′ ∶ X → A, g ′ ∶ X → B such that f ○ f ′ ∼ g ○ g ′ there is h ∶ X → P, unique up to symmetry, such that Π 1 ○ f ∼ f ′ and Π 2 ○ g ∼ g ′ .
In particular, any pseudo-pullback is a bi-pullback. It turns out that E ∼ has all pseudopullbacks [START_REF] Winskel | Event structures with symmetry[END_REF], so one may opt to use those for composing strategies. Though sensible, this choice has technically heavy consequences -we will come back to them later. However, there is another possibility to compose strategies with symmetry: it may be that though E ∼ does not have all pullbacks, it has all those required to compute the interaction of strategies. And indeed, using polarity it is easy to capture maps that interact well in the presence of symmetry: just as receptivity prevents a strategy from refusing an Opponent move, ∼receptivity prevents it from refusing to consider two Opponent moves to be symmetric.

Definition 3.9. If A is a essp, a map of ess σ ∶ S → A is ∼-receptive iff for all θ ∶ x 1 ≅ S x 2 , for all x 1 s - 1 -⊂ and σ x 2 a - 2 -⊂ such that σ θ ∪ {(σ s 1 , a 2 )} ∈ Ã,
there is a unique s 2 such that σ s 2 = a 2 , and we have θ ∪ {(s 1 , s 2 )} ∈ S.

Moreover, σ as above is strong-receptive if it is both receptive and ∼-receptive.

Dual ∼-receptive maps always have pullbacks in E ∼ : intuitively, the polarity helps determining whose responsibility it is to set two events as symmetric. However, before we prove that, let us include an example illustrating the following fact: besides ensuring pullbacks, ∼-receptivity is key to ensure that strategies based on ess are indeed uniform.

Example 3.10. Recall the non-uniform strategy from Section 2:

! B 1 → B 2 → ! B 3 → B 4 q -,i 4 ✭ p p w ❤ ❤ ❤ ❤ ❤ ❤ ❤ ❤ ❤ ❤ q +,i 2 ✪ o o u ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ✮ q q x ✐ ✐ ✐ ✐ ✐ ✐ ✐ ✐ ✐ ✷ u u } r r q -,0 1 ✚ A A H ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ✐ ❣ ❡ ❝ ❜ ❵ q -,1 1 ♦ ✐ ❝ q -,i 1 r q +,0 3 ✓ ✌ ✆
Assume now there is an isomorphism family S on this event structure S such that the labelling map

σ ∶ S → ! B → B ⊥ ∥ ! B → B is ∼-receptive.
By ∼-receptivity (since the identity on {q -,0 4 , q +,0 2 } must be in S), we must have that the bijection {q -,0 4 , q +,0 2 , q -,0 1 } ≅ {q -,0 4 , q +,0 2 , q -,1 1 } is in S. However, only the left hand side part can be extended by q +,0 3 , absurd. As ∼-receptivity is crucial to ensure uniformity, it will be required whether we wish to compute interaction via pullback or pseudo-pullback.

We now prove that as claimed above, pullbacks exist along dual ∼-receptive maps of ess. To define the isomorphism family for the pullback, we first notice that bijections on configurations of the (plain) pullback induce bijections on their projections: Lemma 3.11. Let σ ∶ S → A and τ ∶ T → A be maps of event structures. Let θ ∶ w ≃ z be a bijection, where w, z ∈ C (S ∧ T ). There are (unique) bijections

θ S ∶ Π 1 w ≃ Π 1 z and θ T ∶ Π 2 w ≃ Π 2 z satisfying Π 1 ○ θ = θ S ○ Π 1 and Π 2 ○ θ = θ T ○ Π 2 . Moreover, the mapping θ ↦ (θ S , θ T ) is monotonic w.r.t. inclusion. Proof. By local injectivity, Π 1 defines a bijection w ≃ Π 1 w and z ≃ Π 1 z. With this remark, θ S is simply defined as Π 1 ○ θ ○ Π -1
1 . The equation and uniqueness are by definition, and monotonicity is obvious. The definition of θ T is symmetric.

For σ ∶ S → A and τ ∶ T → A maps of ess, define S ∧ T to contain those bijections

θ ∶ w ≅ z such that θ S ∶ Π 1 w ≅ Π 1 z ∈ S and θ T ∶ Π 2 w ≅ Π 2 z ∈ T .
Bearing in mind the correspondence between configurations of S ∧ T and secured bijections x ≃ y, there is an order-isomorphism between those bijections θ ∈ S ∧ T and commutative squares between secured bijections x ≃ y and x ′ ≃ y ′ (ordered by componentwise union):

x θ S ≅ S ≃ σ σx = τ y ≃ τ y θ T ≅ T x ′ ≃ σ σx ′ = τ y ′ ≃ τ y ′
This definition indeed yields a pullback in E ∼ :

Lemma 3.12. Let σ ∶ S → A and τ ∶ T → A ⊥ be ∼-receptive maps of ess. The set S ∧ T is an isomorphism family on S ∧ T and the ess (S ∧ T, S ∧ T ) is a pullback in E ∼ of σ and τ , written S ∧ T .

Proof idea. The only difficulty is in proving the (Extension) condition. The argument exploits that an extension is positive for one of σ, τ , negative for the other -apply (Extension) for the positive, and ∼-receptivity for the other. The details are in Appendix B.1.

3.1.5. Equivalences between strategies. So, should we base our composition of strategies with symmetry on pullbacks or pseudo-pullbacks? To make up our mind another aspect must weight in: the universal property used to compose strategies impacts the equivalence up to which strategies may be considered. Indeed in CG strategies are naturally considered up to isomorphism (Definition 2.7), and that is of course preserved by pullbacks (pullbacks along isomorphic maps being isomorphic). In contrast, as pointed out in Section 2.5.3 in the presence of replication it is crucial to consider strategies up to symmetry, and there is no reason for an equivalence such as that of Definition 2.28 to be preserved by pullback. However, pseudo-pullbacks do preserve notions of equivalence: Definition 3.13. Two maps of ess σ ∶ S → A and σ ′ ∶ S ′ → A are weak-equivalent iff there are maps of ess f ∶ S → S ′ , g ∶ S ′ → S such that g ○ f ∼ id S , f ○ g ∼ id T , and the two triangles below commute up to symmetry:

S f G G σ 1 1 ❄ ❄ ❄ ❄ ∼ S ′ σ ′ 6⑥ ⑥ ⑥ A S ′ g G G σ ′ 2 2 ❆ ❆ ❆ ❆ ∼ S σ ⑧ ⑧ ⑧ ⑧
A They are strong-equivalent iff the triangles further commute on the nose.

It follows from their definition that pseudo-pullbacks preserve strong equivalence, and that bi-pullbacks preserve weak equivalence. Being a particular case of bi-pullbacks, pseudopullbacks preserve both. Weak equivalence looks like the notion of Definition 2.28 and indeed can serve to compare strategies up to their choice of copy indices (we will come back later to the subtle differences between weak equivalence and Definition 2.28), while the requirement that the triangles commute on the nose makes strong equivalence look less obviously relevant for that purpose. In any case, the take-away message for this discussion seems to be: just use pseudo-pullbacks for interaction! Mathematically, this seems an elegant approach to concurrent games with symmetry: as E ∼ is enriched over equivalence relations, in building concurrent games with symmetry it is natural to mimic the constructions of CG from E using the corresponding operations on ess that take account of the enrichment. Indeed, this natural solution was the basis for our first account of symmetry in concurrent games [START_REF] Castellan | Symmetry in concurrent games[END_REF]. It works as a general framework (indeed [START_REF] Castellan | Symmetry in concurrent games[END_REF] contains a construction of HO and AJM-style games), but suffers from significant drawbacks concerning its applicability for further semantic purposes.

! B → B q -,i ✪ o o u ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ✭ p p w ❤ ❤ ❤ ❤ ❤ ❤ ❤ ❤ ❤ ❤ ❤ ❤ ❤ ❤ ❤ ❤ ❤ ✱ r r z • • • • • • • • • • ✾ w w Ò ② ② ② q +,0 • ✐ ❤ ❣ ❡ ❞ ❝ ❛ / o q +,1 / o ❦ • ❤ ❢ ❞ ❜ q +,2 ... r ♦ • ✐ ❢ q +,j ...
T ⊛ S Π 1 { { ✇ ✇ ✇ ✇ ✇ ✇ Π 2 6 6 ❍ ❍ ❍ ❍ ❍ ❍ ❄ ⑧ S ∥ C σ∥C 5 5 ❋ ❋ ❋ ❋ ❋ ∼ A ∥ T A∥τ { { ✇ ✇ ✇ ✇ ✇ ✇ A ∥ B ∥ C
Unlike pullbacks, pseudo-pullbacks commute up to symmetry. Consequently, interaction via pseudo-pullback allows one to synchronize configurations that do not match on the nose, but up to symmetry. Accordingly, the pseudo-pullback analogue of Proposition 2.16 says that configurations in C (T ⊛ S) correspond to the data of

x S ∥ x C ∈ C (S ∥ C), x A ∥ x T ∈ C (A ∥ T ) and θ ∈ Ã ∥ B ∥ C such that: x S ∥ x C σ ↦ x A ∥ x B ∥ x C θ ≅ Ã∥ B∥ C y A ∥ y B ∥ y C τ ↦ y A ∥ y T
It carries a symmetry θ ∈ Ã ∥ B ∥ C which mediates between configurations of S and T not quite matching on the game, but can also apply a symmetry on the visible output in the game. Everything becomes "up to symmetry", including the visible actions of the interaction. Concretely, because of that, composition based on pseudo-pullbacks has a "saturation" effect: for x ∈ C (S) in a saturated σ ∶ S → A, for all θ ∶ σx ≅ Ã y ′ there must be ϕ ∶ x ≅ S y such that σy = y ′ . In other words, if a saturated strategy is prepared to play a move, by necessity it is also prepared to play non-deterministically all symmetric moves. To behave well with pseudo-pullback-based composition, all strategies need to be saturated, even copycat [START_REF] Castellan | Symmetry in concurrent games[END_REF]. We display in Figure 6 the saturated strategy corresponding to the two diagrams at the end of Example 2.26 -to alleviate the diagram we only represent a few binary conflicts, but in reality all positive events are pairwise incompatible and symmetric: the strategy chooses non-deterministically one copy index and plays it.

The reader with a background in game semantics will recognize here a phenomenon familiar from AJM games: in [START_REF] Baillot | Believe it or not, AJM's Games Model is a Model of Classical Linear Logic[END_REF] was introduced a variant of AJM games where strategies were similarly required to be saturated under the action of the equivalence relation. Independently of the specific purposes of [START_REF] Baillot | Believe it or not, AJM's Games Model is a Model of Classical Linear Logic[END_REF] (which required it for technical reasons), saturation provides a different approach to uniformity in AJM games than the traditional one [START_REF] Abramsky | Full abstraction for PCF[END_REF]. While it has remained rather marginal in game semantics, some recent works based on AJM games are actually based on saturation [START_REF] Abramsky | Game semantics for access control[END_REF][START_REF] Vákár | Game semantics for dependent types[END_REF], as it provides a slightly simpler mathematical foundation for uniformity.

While mathematically natural, saturation in concurrent games has some significant drawbacks. First of all, it makes strategies more "abstract": even the underlying event structure becomes impossible to represent faithfully. As copy indices are chosen nondeterministically, all (non-trivial) strategies fail determinism in the usual sense of concurrent games [START_REF] Winskel | Deterministic concurrent strategies[END_REF] and it is tricky to recover a working notion of determinism up to symmetry. More generally, notions in CG that rely on a concrete analysis of the shape of conflict (such as single-threadedness -see Definition 4.8 -or all our further work on innocence [START_REF] Castellan | The parallel intensionally fully abstract games model of PCF[END_REF]) are hard to accommodate with saturated symmetry as the non-deterministic choice of symmetric events pollutes the genuine dynamic behaviour of the strategy. Last but not least, the saturated framework is not conservative over CG: one cannot "forget symmetry" functorially as composition mechanisms inherently involve it. This means that developments in CG are less likely to adapt transparently to saturated symmetry.

For these reasons, we have found it necessary to develop an alternative approach to uniformity (first presented in [START_REF] Castellan | The parallel intensionally fully abstract games model of PCF[END_REF]), called thin concurrent games as opposed to saturated, which is conservative over CG: in particular, the core components of the categorical structure (composition, copycat) match those in CG. In that respect, it is analogous to the traditional AJM way of handling uniformity [START_REF] Abramsky | Full abstraction for PCF[END_REF]. This has been a subtle endeavour, but the effort pays off: conservativity over CG means that many developments on CG extend transparently with thin symmetry, undisturbed by the uniformity requirements. Such successes include of course concurrent innocence [START_REF] Castellan | The parallel intensionally fully abstract games model of PCF[END_REF], but also the more recent probabilistic extension [START_REF] Castellan | The concurrent game semantics of probabilistic PCF[END_REF], and other works as of now unpublished. So the following construction of Tcg is hard work, but experience tells that the subtleties involved can be mostly abstracted away when relying on Tcg, and one can work like in CG simply with the additional proof obligations that further structure should be invariant under symmetry.

3.2. Thin concurrent games. Rather than changing the compositional machinery to preserve weak equivalence, we instead seek further restrictions on strategies for their standard interaction pullback to preserve it. Interestingly the answer turns out to be a minimality condition mirroring saturation, suggesting a sort of duality that is still under investigation.

3.2.1. Thinness. Our starting point is the fact that, unfortunately, weak equivalence of ∼receptive maps is not preserved under composition or pullback -a counter-example appears in Appendix A.3. Our interpretation of that failure is that the (Extension) axiom is too permissive for strategies. Indeed, consider σ ∶ S → A a ∼-receptive map of essps, and θ ∶ x ≅ S y, suppose further that x extends by some positive event s + ∈ S (strategies will be strong-receptive, as such extensions by negative events are inconsequential and entirely governed by the game). By (Extension), we then have some s ′ with:

x ∪ {s} -⊂ θ ′ ≅ S y ∪ {s ′ } -⊂ x θ ≅ S y
The crux of the issue is in how this s ′ is chosen. For saturated strategies the set of available choices for s ′ is canonical: there are as many s ′ as there are symmetric events in the game. In contrast, in the counter-example of Appendix A.3, there is no canonical choice (more specifically, the counter-example exploits a situation where no valid assignment from the choices for s to the choices for s ′ can be described globally as a map of event structures).

This need of a canonical choice for positive extensions motivates the definition:

Definition 3.14. An essp A is thin if for θ ∶ x ≅ Ã y and x a + 1 -⊂ , there is a unique y a + 2 -⊂ s.t. x ∪ {a 1 } θ∪{(a 1 ,a 2 )} ≅ Ã y ∪ {a 2 }
The canonicity of the choice of positive extensions is ensured by uniqueness. Thinness is the main ingredient of our forthcoming definition of ∼-strategies; the next objective in our construction being to show that indeed (under mild further conditions), the interaction between thin maps preserves weak equivalence (a phenomenon we will from now on refer to as congruence, for brevity). For that we first mention a slightly simpler equivalent formulation of thinness -the equivalence proof is an interesting exercise.

Lemma 3.15. An essp A is thin iff for all x ∈ C (A), for all id x ⊆ + θ ∈ Ã, then θ = id y for some x ⊆ y ∈ C (A).

The ∼-strategies will be certain ∼-receptive σ ∶ S → A, with S thin (we will also say that σ is thin). An intuitive reading of thinness prompted by Lemma 3.15 is that σ will not take the initiative of declaring two positive events symmetric. As long as negative extensions of the symmetry remain identity bijections, positive extensions will too. As a consequence: Lemma 3.16. Let σ ∶ S → A and τ ∶ T → A ⊥ be thin ∼-receptive maps of essp.

Then, S ∧ T is trivial (reduced to identities).

Proof. We prove by induction that all bijections in S ∧ T are identities. Let z ∈ C (S ∧ T ) and assume id z extends by (e, e ′ ) to θ ∈ S ∧ T . Assume for instance Π 2 e is positive in T (the other case is similar). By construction id Π 2 z extends to θ T = Π 2 θ ∈ T by positive events (Π 2 e, Π 2 e ′ ), hence Π 2 e = Π 2 e ′ and θ T is the identity because T is thin. By local injectivity of Π 2 it follows that e and e ′ must be equal, or incompatible extensions of z. But if they are incompatible, by Lemma 2.15 (and Proposition 2.16) it means that Π 1 e and Π 1 e ′ are incompatible extensions of Π 1 z mapping to the same event in the game, contradicting the ∼-receptivity of σ. Hence e = e ′ and θ is the identity.

In other words, a closed interaction between thin ∼-receptive maps has a trivial symmetry. Of course that will not be the case for an open interaction between σ ∶ S → A ⊥ ∥ B and τ ∶ T → B ⊥ ∥ C, where the external Opponent may contribute new symmetric pairs of negative events on A ⊥ ∥ C. Indeed, computing this interaction involves the pullback

T ⊛ S Π 1 { { ✇ ✇ ✇ ✇ ✇ ✇ Π 2 6 6 ❍ ❍ ❍ ❍ ❍ ❍ ❄ ⑧ S ∥ C σ∥C 5 5 ❋ ❋ ❋ ❋ ❋ A ∥ T A∥τ { { ✇ ✇ ✇ ✇ ✇ ✇ A ∥ B ∥ C
on which Lemma 3.16 does not apply, because id C ⊥ ∶ C ⊥ → C ⊥ and id A ∶ A → A are not thin -indeed, A could be e.g. the essp of Proposition 3.3, whose isomorphism family includes all reindexing isomorphisms. In our proof of congruence, it will be of great importance that we are able to consider a sub-structure of the open interaction above where the external Opponent does not contribute new symmetric pairs, i.e. restrict symmetries so as arrive in the realm of Lemma 3.16. Concretely, we need a thin replacement A + → A for A → A, and likewise for C. But no such replacement exist without further conditions on games1 .

3.2.2. Thin concurrent games and ∼-strategies. The requirement above suggests that besides being essps, games with symmetry A should feature a sub-symmetry Ãsuch that id A ∶ A -→ A satisfies the conditions of Lemma 3.16, i.e. is thin and ∼-receptive. By duality, we also need Ã+ such that A ⊥ + → A ⊥ is thin ∼-receptive. These polarised sub-symmetries, along with their desired properties, are nicely captured by the following definition2 . Definition 3.17. A thin concurrent game (tcg) is an essp A with two additional isomorphism families Ãand Ã+ on A such that:

(a) The families Ã+ and Ãare subsets of Ã,

(b) If θ ∈ Ã+ ∩ Ã-then θ is an identity bijection, (c) If θ ∈ Ã-and θ ⊆ -θ ′ ∈ Ã then θ ′ ∈ Ã-, (d) If θ ∈ Ã+ and θ ⊆ + θ ′ ∈ Ã then θ ′ ∈ Ã+ . where θ ⊆ -θ ′ (resp. θ ⊆ + θ ′ ) means that θ ⊆ θ ′ such that θ ′ ∖θ
only contains pairs of negative (resp. positive) events. The triple (A, Ã-, Ã+ ) will be often written simply A.

Thin concurrent games support the basic operations on essps: the dual is (A, Ã-, Ã+ ) ⊥ = (A ⊥ , Ã+ , Ã-), and the simple parallel composition is performed componentwise:

(A, Ã-, Ã+ ) ∥ (B, B-, B+ ) = (A ∥ B, Ã-∥ B-, Ã+ ∥ B+ ).
Of course, thin concurrent games include our guiding example: Proposition 3.18. Let A be an arena. Then, (!A, ! A, ! A -, ! A + ) is a thin concurrent game.

Through this example one may get a more concrete understanding of the sub-symmetries: Ã+ comprises the symmetries where only Player has performed non-trivial exchanges between moves (so "copy indices" of negative events are preserved), and dually for Ã-.

We mention right away two important properties of tcgs. Firstly, it follows as required that A -is thin (and likewise for A ⊥ + ). Indeed, using the characterisation of Lemma 3.15, consider x ∈ C (A), and id x ⊆ + θ ∈ Ã-. But id x is in all three isomorphism families and in particular in Ã+ , so θ ∈ Ã+ as well by (d). Hence, θ = id y for some y ∈ C (A) by (b).

Secondly, it follows from the axiom that any θ ∈ A can be factored uniquely:

Lemma 3.19 (Decomposition lemma). For A a tcg, we have an order-isomorphism:

Ã-× A Ã+ → Ã (θ -, θ + ) ↦ θ -○ θ +
where Ã-× A Ã+ = {(θ -, θ + ) ∈ Ã-× Ã+ codom θ + = dom θ -} is ordered by pairwise inclusion and à is ordered by inclusion.

Proof. The map is clearly well defined because Ãand Ã+ are included in Ã.

Injectivity. Assume we have θ = θ -

1 ○ θ + 1 = θ - 2 ○ θ + 2 ∶ x ≅ Ã y.
By using groupoid laws we get that θ

+ 1 ○ (θ + 2 ) -1 = (θ - 1 ) -1 ○ θ - 2 ∶ z 2 ≅ z 1 ∈ Ã-∩
Ã+ hence both are equal to the identity. Surjectivity. By induction on θ ∈ Ã we build a preimage. Assume we have the decomposition of θ = θ -○ θ + , and that θ extends to θ ′ ∶ x ′ ≅ y ′ by a pair of fixed polarity, say positive. We use the extension axiom on θ -to get

θ -⊆ θ ′-∶ z ′ ≅ Ã-y ′ . It follows that θ + ⊆ (θ ′-) -1 ○ θ ′ ∶ x ′ ≅ Ã z ′ is a positive extension of θ + so it must belong to Ã+ by (d). Hence θ ′ = θ ′-○ (θ ′-) -1 ○ θ ′ provides the required decomposition.
Monotonicity. Monotonicity of the decomposition follows from uniqueness.

So the full à is actually redundant, and can be uniquely recovered from Ãand Ã+ . This structure of a game with two isomorphism families is strongly reminiscent of Melliès' earlier approach to uniformity by bi-invariance under two group actions [START_REF] Mellies | Asynchronous games 1: A group-theoretic formulation of uniformity[END_REF]. This suggests that there is something intrinsic in this decomposition of symmetry as compositions of Opponent's reindexings and Player's reindexing. This structure, that alternation and sequentiality allows to keep hidden in AJM's equivalence relations, seems to become inevitable in a thin treatment of symmetry in games where sequentiality is not hard-wired.

Before going on to the proof of congruence, as we are finally in a position to formalize what we mean by strategy with symmetry, we start by doing that. Definition 3.20. Let A be a tcg. A pre-∼-strategy on A is a thin, ∼-receptive map of essp σ ∶ S → A.

It is a ∼-strategy if it is also receptive and courteous ( i.e. σ ∶ S → A is a strategy).

We are mainly interested in the interaction and composition of ∼-strategies, but we perform some of the developments with the slightly more permissive conditions of pre-∼strategies as it is occasionally useful (in particular when we model state in Section 5.3) to be able to compose "strategies" that are not courteous or receptive.

3.2.3. Congruence. We start by stating the property ensuring congruence: the bi-pullback property. Our next objective is to prove it for all interactions between pre-∼-strategies. Definition 3.21 (Bi-pullback property). Let σ ∶ S → A ⊥ ∥ B and τ ∶ T → B ⊥ ∥ C be ∼-receptive maps of essps. Their interaction has the bi-pullback property iff the pullback

T ⊛ S Π 1 y y s s s s s Π 2 8 8 ▲ ▲ ▲ ▲ ▲ ❄ ⑧ S ∥ C σ∥C 7 7 ❏ ❏ ❏ ❏ A ∥ T A∥τ y y s s s s A ∥ B ∥ C is a bi-pullback.
In essence, the definition of interaction of strategies via pullback expresses that given x S ∈ C (S) and x T ∈ C (T ) that match on B (i.e. σx S = x A ∥ x B and τ x T = x B ∥ x C ) and are causally compatible (see Proposition 2.16), we can form their synchronization uniquely as some z ∈ C (T ⊛ S) such that Π 1 z = x S ∥ x C and Π 2 z = x A ∥ x T . The bipullback property extends this method to construct synchronized states: it asserts in essence that if such x S ∈ C (S) and x T ∈ C (T ) only match up to symmetry (e.g. they fail to agree because of copy index mismatches), one can always find a "common ground", both strategies changing their choice of symmetric events, yielding some x S ≅ S x ′ S and x T ≅ T x ′ T where x ′ S and x ′ T now match on the nose and can be synchronized directly. This process of tweaking "copy indices" to find a common ground can be done interactively, and -beyond the bi-pullback property -is at the heart of the congruence problem. To illustrate that and showcase the inductive process at play, we include the following example of transporting a weak equivalence through composition.

Example 3.22. Consider the two following strategies on ! com

σ 1 ∶ ! com σ 2 ∶ ! com run -,i ❴ run -,i ❴ done +,0 ✤ done +,1
✤ only differing by the choice of copy index for done. There is an obvious weak equivalence between them, call ϕ ∶ S 1 → S 2 the obvious invertible map. Consider now the following strategy τ (which, in IPA, represents x ∶ com ⊢ x; x ∶ com):

! com → ! com run -,i ✪ o o u ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ✹ ✲ ✫ ✤ ✘ ✑ ✡ run +,⟨i,0⟩ ❴ done -,j ❴ ✤ run +,⟨i,j+1⟩ ❴ done -,k ✙ A A G ( ( ( ( ( ( ( ( ( ( ( ( (
✤ done +,⟨j,k⟩ In order to build a weak equivalence between the resulting compositions τ ⊙ σ 1 and τ ⊙ σ 2 , a reasonable first step is to build a weak equivalence between the interactions τ ⊛ σ 1 and τ ⊛ σ 2 . In particular, given a configuration of T ⊛ S 1 , we should be able to build a corresponding configuration of T ⊛ S 2 . Consider e.g. the following configuration of T ⊛ S 1 .

! com → ! com run -,i ✫ o o v ❢❢ ❢❢ ❢ ❢❢ ❢❢ ❢ ❢❢ ❢ ✩ ★ ✦ ✤ ✢ ✛ ✚ run ⟨i,0⟩ ❴ done 0 ❴ ✤ run ⟨i,1⟩ ❴ done 0 ✘ @ @ G ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ✤ done +,⟨0,0⟩
where events on the left hand side are drawn without polarity, as they are synchronised between σ 1 and τ . By projections, we get configurations x ∈ C (S 1 ∥ ! com ) and y ∈ C (T ) such that (σ 1 ∥ ! com ) x = τ y and such that the induced bijection is secured.

In order to construct a configuration in T ⊛ S 2 , it is natural to try and replace x with ϕ(x) -and that would work out if ϕ was a strong equivalence. But as it is only a weak equivalence, we do not have

(σ 2 ∥ ! com ) (ϕ x) = τ y, only (σ 2 ∥ ! com ) (ϕ x) ≅ ! com ∥! com τ y
Here we observe the phenomenon hinted at above: the need to extract from ϕ x ∈ C (S 2 ) and y ∈ C (T ), only matching up to symmetry, a valid configuration of T ⊛ S 2 . For our example, the only possibility is:

! com → ! com run -,i ✫ o o v ❢❢ ❢❢ ❢ ❢❢ ❢❢ ❢ ❢❢ ❢ ✹ ✲ ✫ ✤ ✘ ✑ ✡ run ⟨i,0⟩ ❴ done 1 ❴ ✤ run ⟨i,2⟩ ❴ done 1 ✘ @ @ G ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ✤ done +,⟨1,1⟩
It appears that both ϕ x and y had to change, in order to find an agreement as to the choice of copy indices. To compute it, we replay the interaction up to the first disagreement between σ 1 and σ 2 . By hypothesis, this disagreement yields symmetric configurations of the game. Hence by ∼-receptivity, T comprises a bijection:

! com → ! com run -,i ✫ o o v ❢❢ ❢❢ ❢❢ ❢❢ ❢❢ ❢❢ run +,⟨i,0⟩ ❴ done -,0 ✤ ≅ T ! com → ! com run -,i ✫ o o v ❢❢ ❢❢ ❢❢ ❢❢ ❢❢ ❢❢ run +,⟨i,0⟩ ❴ done -,1
✤ By (Extension) in T , we know that this bijection can be extended to some:

! com → ! com run -,i ✫ o o v ❢❢ ❢❢ ❢❢ ❢❢ ❢❢ ❢❢ run +,⟨i,0⟩ ❴ done -,0 ✤ ❴ run +,⟨i,1⟩ ≅ T ! com → ! com run -,i ✫ o o v ❢❢ ❢❢ ❢❢ ❢❢ ❢❢ ❢❢ run +,⟨i,0⟩ ❴ done -,1 ✤ ❴ run +,⟨i,2⟩
Likewise, by ∼-receptivity of σ 2 ∥ ! com this extension is lifted to S2 ∥ ! com , and we then apply (Extension) on S2 . And the process goes on, interactively between σ 2 and τ , until we get x ′ ≅ S∥ ! com ϕ x and y ′ ≅ T y such that (σ 2 ∥ ! com ) x ′ = τ y ′ (which in our example, is the configuration of the interaction represented above).

Formalizing this interactive process of using ∼-receptivity on one strategy and extension on the other yields the following lemma: Lemma 3.23 (Weak bipullback property). Let σ ∶ S → A and τ ∶ T → A ⊥ be pre-∼strategies. Let x ∈ C (S) and y ∈ C (T ) and θ ∶ σx ≅ Ã τ y, such that the composite bijection

x σ ≃ σ x θ ≅ Ã τ y τ ≃ y
is secured. Then, there exists z ∈ C (S ∧ T ) along with θ S ∶ x ≅ S Π 1 z and θ T ∶ Π 2 z ≅ T y, such that τ θ T ○ σθ S = θ. Moreover, z is unique up to symmetry.

Proof. Uniqueness. Assume we have such (z, θ S , θ T ) and

(z ′ , θ ′ S , θ ′ T ). Then it is easy to see that θ ′ S ○ θ -1 S ∶ Π 1 z ≅ S Π 1 z ′ and similarly θ ′ T ○ θ -1 T ∶ Π 2 z ≅ T Π 2 z ′ .
Those match on the game A, so they induce a z ≅ z ′ in S ∧ T as desired.

Existence. We proceed by induction on θ; the base case is trivial. Assume θ extends by (σs, τ t) to θ ′ ∶ σx ′ ≅ τ y ′ . For instance, s is positive. We have θ S ∶ x ≅ Π 1 z and x can be extended to x ′ by s, so by the extension property of the symmetry θ S extends to

θ ′ S ∶ x ′ ≅ z ′ S .
This means that τ θ T can be extended by symmetric negative (for T ) events so by ∼-receptivity, θ T can extend to θ ′ T ∶ z ′ T ≅ T y ′ , with σz ′ S = τ z ′ T by construction. Since the bijection z ′ S ≅ z ′ T is obviously secured, we get z ′ ∈ C (S ∧ T ) that satisfies our property. Note that we did not need that σ and τ are thin -only ∼-receptivity. This statement is a step in the right direction, however the non-uniqueness of z (only up to symmetry) is problematic: it cannot be used to build maps, in particular it cannot be used to lift a weak equivalence σ → σ ′ to τ ⊛ σ → τ ⊛ σ ′ . However, we will see now that if the interacting strategies are thin, we can use Lemma 3.16 to "tighten the screws" and show that then the choice of z is unique; from this observation the required map will follow.

We now prove the main technical result of this section, the bi-pullback lemma.

Lemma 3.24. Let σ ∶ S → A ⊥ ∥ B and τ ∶ T → B ⊥ ∥ C playing on tcgs. Then, their interaction has the bi-pullback property.

Proof. Recall that for f ∶ X → S ∥ C, g ∶ X → A ∥ T such that τ ○ g ∼ Ã∥ B∥ C σ ○ f , we need h ∶ X → T ⊛ S, unique up to symmetry, such that Π 1 ○ h ∼ S∥ C f and Π 2 ○ h ∼ Ã∥ T g.
Uniquess up to symmetry follows from Π 1 ○ h ∼ S∥ C f and Π 2 ○ h ∼ Ã∥ T g and definition of the symmetry on the pullback. The main difficulty is existence. As hinted above, the trick is to apply Lemma 3.23, not on the raw interaction pullback, but on that between:

(σ ∥ (C ⊥ ) -) ∶ S ∥ (C ⊥ ) -→ A ⊥ ∥ B ∥ C ⊥ (A -∥ τ ) ∶ A -∥ T → A ∥ B ⊥ ∥ C Write T ⊛ ′ S for this pullback, with projections Π 1 ∶ T ⊛ ′ S → S ∥ (C ⊥ ) -and Π 2 ∶ T ⊛ ′ S → A -∥ T .
The underlying event structure of T ⊛ ′ S is the same as for T ⊛ S, but the symmetry is tighter: intuitively, it is that where the external Opponent does not change their copy indices. In fact, the two maps above are thin, so by Lemma 3.16, the symmetry of T ⊛ ′ S is very tight indeed: it is restricted to identities. Nevertheless, for x ∈ C (X) we can apply Lemma 3.23 to f x ∈ C (S ∥ C) and g x ∈ C (A ∥ T ), and get z ∈ C (T ⊛ S) -but its uniqueness up to symmetry now holds in T ⊛ ′ S with trivial symmetry, so z is unique. By uniqueness, this association induces a function ψ ∶ C (X) → C (T ⊛ S) such that Π 1 (ψ x) ≅ S∥ C f x and Π 2 (ψ x) ≅ Ã∥ T g x. It is then routine to verify that this function is monotonic, preserves cardinality and unions (hence it is generated by a map of event structures); and that it preserves symmetry -details are omitted. This concludes our proof of congruence for interactions, i.e. the following corollary, simply proved by applying the bi-pullback property.

Corollary 3.25. Weak equivalence is preserved by interactions of pre-∼-strategies on thin concurrent games.

It will of course follow immediately, once composition is defined in Section 3.3.1, that it preserves weak equivalence as well.

3.2.4. Weak isomorphism. Weak equivalence is a natural lax version of the isomorphism of strategies in CG in the presence of symmetry: all equalities in the definition of isomorphism are replaced with symmetry. However, as the reader may have noticed, there is a mismatch between weak equivalence and the weak isomorphisms of Definition 2.28, used in Section 2 to compare strategies up to copy indices. Let us start this discussion by recasting weak isomorphism in the context of thin concurrent games. Definition 3.26. Let σ ∶ S → A and σ ′ ∶ S ′ → A be maps of ess, where A is a tcg. A positive morphism from σ to σ ′ is a map of ess f ∶ S → S ′ such that σ ′ ○ f ∼ A+ σ.

We say that f is a weak isomorphism if it is furthermore invertible on the nose, i.e. there is g ∶ S ′ → S such that g ○ f = id S and f ○ g = id S ′ -we write σ ≈ σ ′ for the corresponding equivalence relation.

The thin concurrent games presented in [START_REF] Castellan | The parallel intensionally fully abstract games model of PCF[END_REF] relied solely on weak equivalence to compare strategies up to symmetry; its refinement with weak isomorphism presented here came later. At first sight it looks like in switching from weak equivalence to weak isomorphisms we are trading an arguably mathematically canonical notion for one that is more concrete, but also possibly more ad-hoc. Of course, if weak isomorphism is a congruence, then the change is convenient. Indeed, having mediating maps be inverses on the nose makes the equivalence more conservative over plain event structures: if σ ≈ σ ′ as above, then S and S ′ are isomorphic as plain event structures (though of course the projection to the game does not commute on the nose). The tighter the equivalence is, the easier it is to transport properties and structure across. But in fact, we will see in this section that it is not a compromise at all: if σ ∶ S → A and σ ′ ∶ S ′ → A are ∼-strategies, then they are weakly isomorphic if and only if they are weakly equivalent 3 ! In order to prove that, the first step is to observe that the mediating maps being inverses on the nose comes for free, provided one insists on using positive weak equivalences.

Lemma 3.27. Let σ ∶ S → A and σ ′ ∶ S ′ → A be pre-∼-strategies, and f ∶ S → S ′ , g ∶ S ′ → S forming a positive weak equivalence, i.e.

σ ′ ○ f ∼ A+ σ and σ ○ g ∼ A + σ ′ .
Then, f and g are actually inverse on the nose (and so form a weak isomorphism).

The proof of that is obvious in the light of the following lemma, which shows plainly the phenomenon at play. Lemma 3.28. Let σ ∶ S → A be a pre-∼-strategy on a tcg A, and let θ ∶ x ≅ S y such that σθ ∈ Ã+ . Then, x = y and θ = id x .

3 For that, thinness plays a crucial role: if σ ∶ S → A ⊥ ∥ B and τ ∶ T → B ⊥ ∥ C are pre-∼-strategies, their composition via pullback and pseudo-pullback (as in Section 3.1.6) are weakly equivalent as both are given by a bi-pullback, but they are certainly not weakly isomorphic.

Proof. By induction on θ. If θ is empty, it is clear. For id x (s,s ′ ) -⊂ θ ∈ S. If s and s ′ are positive, then by thin s = s ′ . If negative, then σθ ∈ Ã+ ∩ Ã-, hence is an identity. So θ is a negative extension of id x , whose image in A is an identity; hence it is an identity by ∼-receptivity.

It is of course not the case that every weak equivalence is positive. However, every map between pre-∼-strategies is symmetric to one which does preserve the projection on the game up to positive symmetry: intuitively, if f sends negative s -∈ S to f s with a different "copy index", we set f ′ s to the unique matching move positively symmetric to f s.

Lemma 3.29. Let σ ∶ S → A and σ ′ ∶ S ′ → A be pre-∼-strategies, and f ∶ S → S ′ such that σ ′ ○ f ∼ Ã σ. Then, there exists a unique f ′ ∶ S → S ′ such that f ∼ S′ f ′ , and σ ′ ○ f ′ ∼ Ã+ f . Sketch. For x ∈ C (S), the hypotheses give us θ x ∶ σ ′ (f x) ≅ Ã σx, which we need to make positive. For that, we first use Lemma 3.19 to decompose θ x as

σ ′ (f x) θ - x ≅ Ã-y θ + x ≅ Ã+ σx such that θ x = θ + x ○ θ - x .
The key idea is then to transport f x over this negative symmetry θ - x , yielding x ′ ≅ S′ f x such that σ ′ x ′ ≅ Ã+ y (which can be done by induction on f x and θ - x ), so that σx ≅ Ã+ σ ′ x ′ as well. We then set f ′ x to be x ′ , and extract from this a map f ′ ∶ S → S ′ .

The details appear in Appendix B.4. This is a rather powerful result: it entails that every symmetry class of such weak maps from σ to σ ′ has a canonical representative, namely the unique equivalent map for which the projection to the game commutes up to positive symmetry.

As an immediate corollary, we have:

Corollary 3.30. Let σ ∶ S → A and σ ′ ∶ S ′ → A be pre-∼-strategies. Then, they are weakly isomorphic if and only if they are weakly equivalent.

Proof. If σ and σ ′ are weakly equivalent, from Lemma 3.29 one easily gets a positive weak equivalence. By Lemma 3.27, it is a weak isomorphism. The other direction is trivial.

As mentioned earlier, from Lemma 3.24 it will be obvious once composition is defined that it preserves weak equivalence. But from the above, each weak equivalence is canonically represented by a weak isomorphism; the induced equivalence relation on ∼-strategies is the same. In particular, it will follow just as directly that weak isomorphism is a congruence.

3.3. Categorical structure. Since the beginning of Section 3 we have focused on the crucial problem of congruence, which imposes the most constraints on the design of games with symmetry. Now that this is solved, we unfold the rest of the work required to build a core setting for game semantics, i.e. a compact closed category of tcgs and ∼-strategies.

Composition.

As the previous section focused on interaction, it makes sense to start the construction by completing it to get composition. Composition of pre-∼-strategies will be defined by simply enriching the composition of Section 2.4.3 with symmetry.

Let σ ∶ S → A ⊥ ∥ B and τ ∶ T → B ⊥ ∥ C be pre-∼-strategies. Ignoring symmetry, recall from Section 2 that τ ⊙ σ ∶ T ⊙ S → A ⊥ ∥ C is obtained using projection (Definition 2.18): given V = {p ∈ T ⊛ S (τ ⊛ σ) p ∈ B} we set T ⊙ S = T ⊛ S ↓ V , and τ ⊙ σ to be the corresponding restriction of τ ⊛ σ. We now extend this in the presence of symmetry. Lemma 3.31. Let E be an ess and V ⊆ E closed under symmetry, in the sense that for all θ ∶ x ≅ Ẽ y, for all e ∈ V ∩ x, we have θ e ∈ V as well. Then, defining

Ẽ ↓ V = {θ ∶ x ≃ y x, y ∈ C (E ↓ V ), ∃θ ⊆ θ ′ ∈ Ẽ, θ ′ ∶ [x] E ≅ Ẽ [y] E }
we have that Ẽ ↓ V is an isomorphism family, making E ↓ V = (E ↓ V, Ẽ ↓ V ) into an event structure with symmetry.

Proof. As usual the axiom (Groupoid) is clear. In this proof we abbreviate

[x] E to [x] for x ∈ C (E ↓ V ) for clarity reasons. (Restriction) Let θ ∶ x ≃ y ∈ Ẽ ↓ V , and x 0 ∈ C (E ↓ V ) such that x 0 ⊆ x. By definition there is θ ⊆ θ ′ ∶ [x] ≅ Ẽ [y]. We have [x 0 ] ⊆ [x]. Therefore, by (Restriction) on Ẽ we have θ ′ 0 ⊆ θ ′ with θ ′ 0 ∶ [x 0 ]≅ Ẽ y ′ 0 . Since V is closed under symmetry, θ ′ 0 ∩ V 2 ∶ x 0 ≃ y ′ 0 ∩ V is still a bijection, which by definition is in Ẽ ↓ V . It is clear by construction that θ ′ 0 ∩ V 2 ⊆ θ. (Extension) Let θ ∶ x ≃ y ∈ Ẽ ↓ V , and x ⊆ x 0 ∈ C (E ↓ V ). By definition there is θ ⊆ θ ′ ∶ [x] ≅ Ẽ [y]. We have [x] ⊆ [x 0 ] ∈ C (E ↓ V ), therefore by (Extension) for Ẽ there is θ ′ 0 ∶ [x 0 ] ≅ Ẽ y ′ 0 . Again since V is closed under symmetry, θ ′ 0 ∩ V 2 ∶ x 0 ≃ y ′ 0 ∩ V is still a bijection.
By definition it is in Ẽ ↓ V , and by construction it contains θ.

Given ∼-receptive σ ∶ S → A ⊥ ∥ B and τ ∶ T → B ⊥ ∥ C (where A, B and C are tcgs), V = {p ∈ S ⊛ T (τ ⊛ σ) p ∈ B} is closed under symmetry; we can thus apply Lemma 3.31. Accordingly we set T ⊙ S as T ⊛ S ↓ V , i.e. comprising bijections θ ∶ x ≃ y such that there is

θ ⊆ θ ∶ [x] T ⊛S ≅ T ⊛ S [y] T ⊛S .
This makes T ⊙ S = (T ⊙ S, T ⊙ S) an event structure with symmetry. In fact, we will show in Lemma 3.33 that if S and T are thin, the witnessing symmetry θ is unique.

Summing up, we state:

Lemma 3.32. If σ ∶ S → A ⊥ ∥ B and τ ∶ T → B ⊥ ∥ C are pre-∼-strategies, then τ ⊙ σ ∶ T ⊙ S → A ⊥ ∥ C
is a map of ess.

Proof. We prove that τ ⊙ σ preserves symmetry. Let θ ∶ x ≅ T ⊙ S y. By definition, there is

θ ⊆ θ ∶ [x] ≅ T ⊛ S [y]. Then, (τ ⊛ σ) θ is some θ A ∥ θ B ∥ θ C ∶ x A ∥ x B ∥ x C ≅ Ã∥ B∥ C y A ∥ y B ∥ y C since (τ ⊛ σ) preserves symmetry. But then (τ ⊙ σ) θ is θ A ∥ θ C ∶ x A ∥ x C ≅ Ã∥ C y A ∥ y C
which is a valid symmetry in à ∥ C as required.

In order to get a notion of composition for ∼-strategies, we need to show that composition preserves thinness, and ∼-receptivity. We will treat them in that order.

The preservation of thinness under composition boils down to one crucial property: the fact that any symmetry between configurations of the composition has a unique witness in the interaction. Indeed, recall from Lemma 3.16 that the closed interaction between dual thin maps has a trivial symmetry. Of course composition is obtained via an open interaction, which does not have trivial symmetry as the external Opponent can contribute new isomorphic pairs of negative events. Nevertheless, whenever the interaction stays within B the phenomenon above applies, and the symmetry is fixed: only the external Opponent can put in relation two non-identical events first. As a result, a bijection in the symmetry of the interaction is fully determined by its restriction to visible events: Lemma 3.33 (Unique witness). Let σ ∶ S → A ⊥ ∥ B and τ ∶ T → B ⊥ ∥ C be pre-∼-strategies. Recall the set of visible events of the interaction:

V = {e ∈ T ⊛ S (τ ⊛ σ) e ∈ B} Let θ ∶ x ≅ T ⊛ S y and θ ′ ∶ x ≅ T ⊛ S y ′ such that θ ∩ V 2 = θ ′ ∩ V 2 . Then θ = θ ′ .
Proof. By hypothesis, we have that y∩V = y ′ ∩V . Note that θ○θ ′-1 ∶ y ′ ≅ y ∈ ( S ∥ C)∧( Ã ∥ T ) and contains id y∩V . So necessarily, the projection of θ ○ θ ′-1 to A and C is an identity bijection. As a result, the symmetry θ ○ θ ′-1 actually belongs to ( S ∥ (C + ) ⊥ ) ∧ (A -∥ T ). This is a pullback of pre-∼-strategies, so θ ○ θ ′-1 is an identity by Lemma 3.16, so θ = θ ′ .

Using this, we can prove that thinness is stable under composition.

Lemma 3.34. For σ ∶ S → A ⊥ ∥ B and τ ∶ T → B ⊥ ∥ C pre-∼-strategies, τ ⊙ σ is thin.

Proof. Let z ∈ C (T ⊙ S) such that id z extends by positives (e, e ′ ) to θ ∶ x ≅ y ∈ T ⊙ S with witness θ ∶ [x] ≅ T ⊛S [y]. Write θ 0 for θ ∖ {(e, e ′ )} ∶ x 0 ≅ y 0 . By hypothesis, θ 0 behaves like the identity on the visible part of x 0 . Hence, by Lemma 3.33, θ 0 is the identity on x 0 .

Since id x 0 = θ 0 can be extended by (e, e ′ ) to θ which is positive in T ⊙ S we can assume eg. Π 2 e and Π 2 e ′ are positive in T . Hence Π 2 θ 0 (which is also an identity) extends by positive (Π 2 e, Π 2 e ′ ). Since τ is thin, we have Π 2 e = Π 2 e ′ from which e = e ′ follows (e and e ′ are positive), as desired.

We now focus on ∼-receptivity. Unlike thinness, it turns out that ∼-receptivity is not preserved by composition without further hypotheses, so pre-∼-strategies are not stable under composition. To ensure preservation of ∼-receptivity one needs courtesy, however it is sometimes necessary to consider "strategies" that are not quite ∼-strategies -in particular for the interpretation of state in Section 5.3. So we introduce a more restricted form of courtesy sufficient to ensure preservation of ∼-receptivity. Definition 3.35. Let σ ∶ S → A ⊥ ∥ B be a pre-∼-strategy. We say that σ is (A, B)-courteous iff for all s 1 s 2 in S, if pol S (s 2 ) = -( i.e. pol A ⊥ ∥B (σ s 2 ) = -), then s 1 and s 2 map to the same A B component.

We will also say that σ ∶ S → A ⊥ ∥ B is componentwise courteous to mean that it is (A, B)-courteous, when A and B are clear from the context. So σ is not necessarily courteous, but is not allowed to influence negative moves accross components. As announced, we have the following. Lemma 3.36. Let σ ∶ S → A ⊥ ∥ B and τ ∶ T → B ⊥ ∥ C be pre-∼-strategies, such that σ is (A, B)-courteous and τ is (B, C)-courteous. Then, τ ⊙σ is ∼-receptive and (A, C)-courteous.

Proof. The key ingredient of the proof is that thanks to componentwise courtesy of σ and τ , the immediate dependency of a negative event has to be a visible event in the same component (and not a neutral event); hence availability of a negative extension is entirely determined by the visible part of the interaction, and ∼-receptivity follows. Technical details are fairly tedious, and relegated to Appendix B.2. So, componentwise courteous pre-∼-strategy are stable under composition. The ∼strategies are precisely those that are furthermore courteous and receptive as plain strategies, and we know from [START_REF] Castellan | Games and strategies as event structures[END_REF] that those are stable under composition; so ∼-strategies are preserved under composition as well. We will see in Section 3.3.3 that composition is associative (up to strong isomorphism) -however, before then we now focus on a crucial element of the compositional structure: its identity, the ∼-strategy copycat.

3.3.2.

Copycat. Recall that the copycat strategy on game A is a labeled event structure:

c c A ∶ C C A → A ⊥ ∥ A
where C C A has the same events as A ⊥ ∥ A, but additional immediate causal links from negative events on one side to matching positive events on the other side. Consequently,

configurations x ∈ C (C C A ) decompose as x = x 1 ∥ x 2 ∈ C (A ⊥ ∥ A).
The following definition is forced by the requirement that the map c c A should be a map of ess, and that each symmetry should be an order-iso. Definition 3.37. Let A be a tcg. Given

x = x 1 ∥ x 2 ∈ C (C C A ), y = y 1 ∥ y 2 ∈ C (C C A )
, the set of symmetries between x and y (written C C Ã) comprises any bijection θ = θ 1 ∥ θ 2 such that θ 1 , θ 2 ∈ Ã, and which is an order-iso (for the order on x, y induced by

≤ C C A ).
This definition is forced by necessity. However, to reason on such symmetries, it will be convenient to rely on a more high-level characterisation that does not explicitly require an order-isomorphism. To introduce it, recall first from [CCRW17] that configurations x ∈ C (C C A ) are exactly those x 1 ∥ x 2 ∈ C (A ∥ A) such that (with polarity as in A ∥ A):

x 2 ⊇ -x 1 ∩ x 2 ⊆ + x 1
Furthermore, it is observed in [START_REF] Winskel | Strategies as profunctors[END_REF][START_REF] Castellan | Games and strategies as event structures[END_REF] that this relation between x 2 and x 1 is a partial order called the "Scott order", written x 2 ⊑ A x 1 . This order is of crucial importance in the construction and study of the bicategory CG.

Proposition 3.38. The set C C Ã is equivalently defined as comprising the bijections

θ 1 ∥ θ 2 ∶ x 1 ∥ x 2 ≃ Ã⊥ ∥ Ã y 1 ∥ y 2
satisfying the further condition that for all a ∈ x 1 ∩ x 2 , we have θ 1 (a) = θ 2 (a).

Proof. Fairly straightforward, details are in Appendix B.3.

In other words, C C

à comprises those θ 1 ∥ θ 2 ∈ Ã⊥ ∥ à such that θ 2 ⊇ -θ 1 ∩ θ 2 ⊆ + θ 1 , i.e.
θ 2 ⊑ Ã θ 1 . This justifies the notation C C Ã, as this agrees with the description of configurations of copycat via the Scott order. Wrapping up this construction, we state: Proposition 3.39. Let A be a tcg. Then, writing

C C A = (C C A , C C Ã), the map c c A ∶ C C A → A ⊥ ∥ A is a ∼-strategy.
Sketch. The details are fairly tedious and relegated to Appendix B.3. Interestingly it relies on A being a tcg: for arbitrary essp A, the set C C Ã fails (Extension) (see Appendix A.4).

3.3.3.

Compact closed structure. We now describe the categorical structure of the constructions above. As all our constructions are conservative extensions of those in CG (for which categorical laws are proved in details in [START_REF] Castellan | Games and strategies as event structures[END_REF]), the proofs of categorical laws boil down to showing that all the isomorphisms involved preserve symmetry. In fact all laws can be actually deduced directly from those in CG established in [START_REF] Castellan | Games and strategies as event structures[END_REF], by exploiting the representation of event structures with symmetry as spans (Section 3.1.1). As the details are at the same time unsurprising and rather tedious, we chose to omit them. Proposition 3.40. We have a category Tcg having tcgs as objects, and as morphisms from A to B the ∼-strategies σ ∶ S → A ⊥ ∥ B, up to weak isomorphism.

Furthermore, composition of componentwise courteous pre-∼-strategies is associative.

We also write

σ ∶ A Tcg + G G B if σ ∶ S → A ⊥ ∥ B is a ∼-strategy from A to B
, keeping the S anonymous. Note that the associativity and unity laws actually hold up to strong isomorphism, i.e. the projection to the game is preserved on the nose. The situation will be the same for all laws relative to the compact closed structure. Of course, this implies that they hold up to weak isomorphism as well.

We now equip Tcg with a monoidal structure. For that, observe first that the category EP ∼ of essps and maps preserving symmetry and polarities already has a monoidal structure, with tensor ∥ extending to maps in the obvious way. The tensor for Tcg is defined on tcgs A and B to be A ⊗ B = A ∥ B (below Definition 3.17). Likewise, the tensor of ∼-strategies

σ 1 ∶ S 1 → A ⊥ 1 ∥ B 1 and σ 2 ∶ S 2 → A ⊥ 2 ∥ B 2 is the map σ 1 ⊗ σ 2 , defined as the composite S 1 ∥ S 2 σ 1 ∥σ 2 G G (A ⊥ 1 ∥ B 1 ) ∥ (A ⊥ 2 ∥ B 2 ) γ G G (A 1 ∥ A 2 ) ⊥ ∥ (B 1 ∥ B 2 )
where γ is the obvious relabeling. Again, as this is compatible with the tensor of strategies in CG, establishing that we have a bifunctor -⊗ -∶ Tcg × Tcg → Tcg just amounts to the fact that the corresponding isomorphisms in CG additionally preserve symmetry.

In order to construct the compact closed structure of Tcg, we need to define all the required structural isomorphisms, such as e.g. the strategy (A ∥ B) ∥ C + G G A ∥ (B ∥ C) expressing that the monoidal product is associative. For that we follow [START_REF] Castellan | Games and strategies as event structures[END_REF] and simply lift them from the corresponding isomorphisms from the monoidal structure of the category EP ∼ of essps and maps preserving both polarity and symmetry between them. Definition 3.41. Let f ∶ A → B be a strong-receptive courteous polarities-preserving map between tcgs. Then its lifting is the ∼-strategy

f = (A ⊥ ∥ f ) ○ c c A ∶ C C A → A ⊥ ∥ B
which is a ∼-strategy from A to B (in particular, it is thin).

We then have:

Theorem 3.42. The category Tcg is compact closed.

Proof. For completeness, we list here all structural morphisms for the symmetric monoidal structure of EP ∼ .

ρ A ∶ A ∥ 1 → A λ A ∶ 1 ∥ A → A s A,B ∶ A ∥ B → B ∥ A α A,B,C ∶ (A ∥ B) ∥ C → A ∥ (B ∥ C)
These isomorphisms are then lifted to ∼-strategies.

ρ A ∶ A ⊗ 1 Tcg + G G A λ A ∶ 1 ⊗ A Tcg + G G A s A,B ∶ A ⊗ B Tcg + G G B ⊗ A α A,B,C ∶ (A ⊗ B) ⊗ C Tcg + G G A ⊗ (B ⊗ C)
As before, coherence and naturality laws are easily adapted from those in CG. Finally, there are (copycat) ∼-strategies

η A ∶ 1 Tcg + G G A ⊥ ⊗ A ǫ A ∶ A ⊗ A ⊥ Tcg + G G 1 satisfying the necessary equations up to isomorphism of ∼-strategies.
Finally, we adapt from [START_REF] Castellan | Games and strategies as event structures[END_REF] the lifting lemma, which we will use later. It characterises the effect of composition of a ∼-strategy via a lifted map.

Lemma 3.43. Let f ∶ B → C be a strong-receptive courteous polarities-preserving map between tcgs, and σ ∶ S → A ⊥ ∥ B a ∼-strategy. Then, those ∼-strategies are isomorphic:

f ⊙ σ ∶ C C B ⊙ S → A ⊥ ∥ C (A ⊥ ∥ f ) ○ σ ∶ S → A ⊥ ∥ C
Note that for f ∶ B ⊥ → A ⊥ strong-receptive and courteous, we have the dual lifting

f ⊥ = (f ∥ B) ○ c c B ∶ A Tcg + G G B;
and, by duality, the symmetric lemma to the above holds: for

σ ∶ B Tcg + G G C, σ ⊙ f ⊥ ≅ (f ∥ C) ○ σ.
Finally we note:

Lemma 3.44. Let f ∶ A → B be an isomorphism of tcgs -so both f and f -1 are strongreceptive courteous. Then, f ≅ f -1 ⊥ .

All this work to build just a compact closed category may feel a little bit anticlimactic to the reader, and understandably so since by itself, a compact closed category can only be used to interpret a simple logic such as Multiplicative Linear Logic. For us however, it represents a crucial achievement in the construction of our framework for game semantics: it covers all the basic compositional properties, while remaining completely agnostic as to the language under study, its features, evaluation strategy, etc.

The focus of the present paper is the construction of the category of Concurrent Hyland-Ong games in the next section; but we consider Tcg as a crucial contribution of the paper in itself, and it can certainly be used in other ways than just through Concurrent Hyland-Ong games. For instance, just like in Hyland-Ong games, replication in Cho is ubiquitous: one cannot speak anymore of linear resources. In contrast, building directly on Tcg (as we did in [START_REF] Castellan | The concurrent game semantics of probabilistic PCF[END_REF]) with a AJM-style exponential allows for a more traditional approach to replication (i.e. a model of ILL), and allows mixing linear and non-linear resources.

3.3.4. AJM-style exponentials. For completeness, and to emphasize the different ways in which one can work with Tcg, we conclude this section by building an AJM-style exponential -we only show that we have an exponential modality, and leave the construction of a full model of Intuitionnistic Linear Logic as out of scope. The remaining sections of this paper are independent of this construction.

Of course, to construct an AJM-style exponential in Tcg the first step is to extend the construction of ! AJM A in Definition 3.4 to tcgs. On that front the first news is bad: ! AJM A cannot be made a tcg in general. For instance, write ⊖⊕ for the tcg with two events, one negative and one positive, the rest of the structure being trivial. Then, ! AJM (⊖⊕) cannot be decomposed into ! AJM (⊖⊕) -and ! AJM (⊖⊕) + satisfying the axioms of tcgs. Intuitively, that is because ! AJM (⊖⊕) forces symmetry constraints across polarities, e.g. {(1, ⊖)} ≅ {(1, ⊖)} and {(1, ⊕)} ≅ {(2, ⊕)} are incompatible, although they have dual polarities and their projections are compatible. The issue runs deeper than a lack of generality of tcgs: C C ! AJM (⊖⊕) fails the (Extension) axiom of isomorphism families (see Appendix A.4).

Fortunately, this phenomenon is circumscribed to non-polarized games with minimal events belonging to both players. Say that a game A is negative (resp. positive) if all its minimal events have negative (resp. positive) polarity. Then we have: Proposition 3.45. Let A be a negative tcg. We define ! AJM A -to include all bijections θ ∶ ∥ i∈I x i ≃ ∥ j∈J y j such that there exists a permutation π ∶ I ≃ J, and for all i ∈ I a symmetry θ i ∶ x i ≅ Ã-y π(i) such that for all (i, a) ∈ ∥ i∈I x i , we have θ(i, a) = (π(i), θ i (a)). Likewise, ! AJM A + is defined in the same way, with Ã+ replacing Ãand π restricted to be the identity.

Then, (! AJM A,

! AJM A -, ! AJM A + ) is a tcg. Proof. Straightforward.
It is possible to have an AJM-style exponential in a non-polarized setting in the saturated games of [START_REF] Castellan | Symmetry in concurrent games[END_REF] mentioned at the beginning of the section. Hence the inability to cover uniform replication on non-polarized games is a restriction of Tcg, however we believe the gains from Tcg far outweight this cost, especially since there are very few situations in game semantics that require uniform replication in non-polarized games (in fact, the only example we are aware of is a games model of classical Linear Logic -interestingly, this is also the paper in which the saturated variant of AJM games was introduced [START_REF] Baillot | Believe it or not, AJM's Games Model is a Model of Classical Linear Logic[END_REF]).

We now prove that ! AJM is an exponential modality in the negative subcategory of Tcg, that we define now. Proposition 3.46. There is a symmetric monoidal subcategory Tcg -of Tcg having as objects the negative tcgs, and as morphisms the negative ∼-strategies σ ∶ S → A ⊥ ∥ B, where the negativity of σ means that the minimal events of S are negative.

Proof. The only non-trivial thing to check is that negative (pre)strategies are stable under composition, which will be proved as Lemma 4.3 in the next section.

We finally conclude this section: Theorem 3.47. The operation ! AJM extends to a linear exponential comonad:

! AJM ∶ Tcg -→ Tcg -
Proof. First we define the functorial action: for σ ∶ S → A ⊥ ∥ B between negative tcgs, we have ! AJM σ ∶ ! AJM S → (! AJM A) ⊥ ∥ ! AJM B defined in the obvious way; functoriality is a variant of that of ⊗. As for the monoidal structure, the components are lifted from maps in EP ∼ . More precisely, for any negative tcgs A, B there are maps defined in the standard way:

(! AJM A) ⊥ ⊗ (! AJM A) ⊥ → (! AJM A) ⊥ A ⊥ → (! AJM A) ⊥ (! AJM ! AJM A) ⊥ → (! AJM A) ⊥ 1 → (! AJM A) ⊥ (! AJM (A ⊗ B)) ⊥ → (! AJM A) ⊥ ⊗ (! AJM B) ⊥ ! AJM 1 ≅ 1
All those maps are courteous and strong-receptive, so by the "dual lifting" operation below Lemma 3.43 they yield ∼-strategies in the other direction, e.g.

! AJM A + G G ! AJM A ⊗ ! AJM A and ! AJM A + G G ! AJM ! AJM A.
It follows direction from Lemma 3.43 that these ∼-strategies are natural and satisfy the required coherence laws up to positive symmetry.

Concurrent Hyland-Ong games

We have constructed a compact closed category Tcg, which is equipped to deal with the problem evoked at the end of Section 2. Using it, we can revisit (more formally) the interpretation sketched in Subsection 2.5. Exploiting the developments of the previous section, and in particular the fact that weak isomorphism is a congruence, it will follow that the two terms of Example 2.26 cannot be distinguished by any strategy in the model. Indeed, we will get a cartesian closed category supporting e.g. the interpretation of IPA.

From now on, all event structures are assumed to have binary conflict. All the operations we will consider on them (simple parallel composition, composition, interaction, etc.) have been established throughout the development to preserve that property.

4.1. The cartesian category Cho. We now construct the category Cho proper, of Concurrent Hyland-Ong games; and prove that it is cartesian. The objects of Cho will be negative arenas, as in Definition 2.4 -with the further restriction that arenas should have a countable set of events, assumed from now on. The morphisms from arena A to arena B will be certain ∼-strategies from !A to !B (up to weak isomorphism):

σ ∶ S → (!A) ⊥ ∥ (!B)
Just as in standard HO games, we restrict strategies in order to satisfy the laws of a cartesian category. We will now inspect the different requirements of a cartesian category, and introduce the additional conditions on strategies as they are required. 4.1.1. Terminal object and negativity. First of all, a cartesian category has a terminal object. In our case, this will be the empty arena 1, defined as having an empty set of eventsnote that !1 also has an empty set of events. However, as it is, 1 is not a terminal object. For each negative arena A, it is easy to see that the unique labelling function

e A ∶ 1 → (!A) ⊥ ∥ (!1)
is a ∼-strategy. Crucially, it is receptive since, by negativity of A, the minimal events of (!A) ⊥ are all positive. However, e A might not be unique from !A to 1, as illustrated below.

Example 4.1. The following diagram represents a ∼-strategy from !com to !1.

(!com) ⊥ ∥ (!1)

run +,0
The answer to this issue is clear: we need to require morphisms in Cho to be negative, just as arenas. As in Proposition 3.46, σ ∶ S → (!A) ⊥ ∥ (!B) is negative whenever the underlying event structure S is negative, i.e. its minimal events are negative -note that this definition makes sense in general without symmetry, for a prestrategy σ ∶ S → A.

We then easily have:

Proposition 4.2. For any negative arena A, the empty ∼-strategy:

e A ∶ 1 → (!A) ⊥ ∥ (!1)
is the unique negative ∼-strategy from !A to !1. In more generality, the only negative prestrategy σ ∶ S → A ⊥ ∥ 1 for a negative game A is the empty prestrategy.

Proof. Immediate, as in a negative prestrategy σ ∶ S → A ⊥ ∥ 1, any hypothetical minimal events in S have nowhere to map to.

Thus, in order to get a category of ∼-strategies with a terminal object, we will require that all ∼-strategies are negative. Clearly copycat is negative, along with all ∼-strategies obtained by lifting. Moreover, negative ∼-strategies are stable under composition. Since negativity makes sense without symmetry, we prove that in slightly greater generality.

Lemma 4.3. Let σ ∶ S → A ⊥ ∥ B and τ ∶ T → B ⊥ ∥ C be negative prestrategies (with A, B, C negative). Then, τ ⊙ σ is still negative.

Proof. First, maps of event structures preserve minimal events: for f ∶ A → B and a minimal in A, it follows easily from the axioms that f a is minimal in B. Hence, minimal events of T ⊛ S are projected to minimal events of S ∥ C and A ∥ T . Take e ∈ T ⊛ S a minimal event. If (τ ⊛ σ) e is in A, then Π 1 e is a minimal event of S projected to a (necessarily positive) minimal event of A -absurd because σ is negative. Likewise, if (τ ⊛ σ) e is in B, this contradicts the negativity of τ . So minimal events of T ⊛ S are visible and are in C. Now, take any minimal event e ∈ T ⊙ S. Since minimal events of T ⊛ S are visible, e is also minimal in T ⊛ S. By the previous remark, (τ ⊙ σ) e is in C and is minimal. It is also negative because C is negative.

Therefore, the category having arenas as objects and as morphisms from A to B, negative ∼-strategies σ ∶ S → (!A) ⊥ ∥ (!B) up to weak isomorphism, has a terminal object 1. We now investigate the existence of products. 4.1.2. Binary products and single-threadedness. For two arenas A and B, their product A × B is defined as the parallel composition A ∥ B, which is still a negative arena.

Projections. Note that there is an injection map of event structures with symmetry:

i A ∶ !A → !(A × B) (α ∶ [a] → ω) ↦ α ′ ∶ [(1, a)] → ω (1, a ′ ) ↦ α(a ′ ) Likewise, there is i B ∶ !B → !(A × B).
Using those, we define the projections

̟ A ∶ C C !A → !(A × B) ⊥ ∥ !A ̟ B ∶ C C !B → !(A × B) ⊥ ∥ !B by lifting the injections, i.e. ̟ A = i A ⊥ ⊥ and ̟ B = i B ⊥ ⊥ (see Definition 3.41).
Pairing. Now, for negative ∼-strategies σ ∶ S → !A ⊥ ∥ !B and τ ∶ T → !A ⊥ ∥ !C, we wish to define their pairing ⟨σ, τ ⟩, a ∼-strategy from !A to !(B × C). This ∼-strategy will simply be obtained by relabeling the parallel composition of S and T . In simple cases, it suffices to take the co-pairing:

⟪σ, τ ⟫ ∶ S ∥ T → !A ⊥ ∥ !(B × C) = [(!A ⊥ ∥ i B ) ○ σ, (!A ⊥ ∥ i C ) ○ τ
] However, this is not always well-defined as a ∼-strategy. Indeed, it might fail local injectivity if some events in S and T have the same image in !A ⊥ . As a first step towards the general construction of pairing, let us prove that this gives a well-defined ∼-strategy when the images of σ and τ are disjoint.

Lemma 4.4. If negative ∼-strategies σ ∶ S → !A ⊥ ∥ !B and τ ∶ T → !A ⊥ ∥ !C have disjoint codomain on !A ⊥ , then ⟪σ, τ ⟫ as above is a negative ∼-strategy.
Proof. First, we prove that it is a ∼-strategy. That it is a map of essps along with courtesy and thinness are direct verifications. Strong-receptivity needs further attention. Take θ ∶

x S ∥ x T ≅ y S ∥ y T ∈ S ∥ T , write θ = θ S ∥ θ T . Its projection to the game is ⟪σ, τ ⟫ θ = ((!A ⊥ ∥ i B ) ○ σ θ S ) ⊎ ((!A ⊥ ∥ i C ) ○ τ θ T )
which is a valid symmetry in G = !A ⊥ ∥ !(B ×C). Assume it extends by a pair (c - 1 , c - 2 ). Since dependency in the game is forest-shaped, there are unique d 1 G c - 1 and d 2 c - 2 , and since symmetries are order-preserving, we have

(d 1 , d 2 ) ∈ ⟪σ, τ ⟫ θ. But that means that it must be either in ((!A ⊥ ∥ i B ) ○ σ) θ S , or in ((!A ⊥ ∥ i C ) ○ τ ) θ T .
We can then apply strong-receptivity of σ, τ , and the injection maps, to produce the extension to θ = θ S ∥ θ T . Now, we prove that this simple pairing behaves well w.r.t. projections. Proposition 4.5. Assume negative ∼-strategies σ ∶ S → !A ⊥ ∥ !B and τ ∶ T → !A ⊥ ∥ !C as in the previous lemma. Then, we have (strong) isomorphisms:

̟ B ⊙ ⟪σ, τ ⟫ ≅ σ ̟ C ⊙ ⟪σ, τ ⟫ ≅ τ
Proof. Let us prove the first. More precisely, we prove that the interactions ̟ B ⊛ ⟪σ, τ ⟫ and c c !B ⊛ σ are isomorphic. This will entail by restriction an isomorphism between the corresponding compositions, and the latter is isomorphic to σ as copycat is the identity.

We establish the isomorphism between ̟ B ⊛ ⟪σ, τ ⟫ and c c !B ⊛ σ first for the plain event structures -by Lemma 2.12 of [START_REF] Castellan | Games and strategies as event structures[END_REF] it suffices to prove that they have an isomorphic domain of configurations. Using Proposition 2.16, we know that configurations of the event structure for the former interaction correspond to secured bijections

(x S ∥ x T ) ∥ x B ≃ y A ∥ (y 1 B ∥ y 2 B ) where x S ∈ C (S), x T ∈ C (T ), ⟪σ, τ ⟫ (x S ∥ x T ) = y A ∥ (i B y 1 B ), and y 1 B ∥ y 2 B ∈ C (C C !B )
, and where the bijection is the unique such that image of events through the labelings ⟪σ, τ ⟫ ∥ !B and !A ∥ ̟ B match. In particular, ⟪σ, τ ⟫ (x S ∥ x T ) does not reach !C. But any minimal events of x T are negative by negativity of τ , and hence must be in !C (since A is negative). Therefore, x T is empty. Getting rid of x T yields a secured bijection corresponding to a configuration of the event structure of c c !B ⊛ σ. This association is bijective, and yields the required isomorphism between domains of configurations. By construction, it is clear that this isomorphism preserves symmetry. So, we know how to construct a pairing behaving well with projections, when the paired strategies happen to have a disjoint codomain. However, for arbitrary σ ∶ S → !A ⊥ ∥ !B and τ ∶ T → !A ⊥ ∥ !C, there might in general be collisions: events s ∈ S and t ∈ T such that σ s = τ t. In such a case, the co-pairing as above fails local injectivity, and therefore does not correspond to a strategy. Fortunately, we can relabel moves of S and T , not changing their weak isomorphism class, to ensure that there are no such collisions. For that, we note that there are maps of event structures with symmetry

ι e ∶ !A ⊥ → !A ⊥ ι o ∶ !A ⊥ → !A ⊥
such that ι e ∼ + ι o ∼ + id !A ⊥ , but such that ι e and ι o have disjoint codomain. For definiteness, say that ι e sends (necessarily positive) minimal events with copy index i to the same events with copy index 2i, and preserves the index of other events. Likewise, ι o follows the injection i ↦ 2i + 1. These maps preserve the index of negative events, so that ι e ∼ + ι o ∼ + id !A ⊥ . Given arbitrary σ ∶ S → !A ⊥ ∥ !B and τ ∶ T → !A ⊥ ∥ !C, we define:

σ e = (ι e ∥ !B) ○ σ τ o = (ι o ∥ !C) ○ τ
From ι e ∼ + ι o ∼ + id !A ⊥ it is obvious that σ ≈ σ e and τ ≈ τ o , but σ e and τ o now have disjoint codomains: σ e (resp. τ o ) only reaches indexing functions in !A whose index for minimal events is even (resp. odd). Therefore, using Proposition 4.5, we define:

⟨σ, τ ⟩ = ⟪σ e , τ o ⟫
The pairing of arbitrary negative ∼-strategies σ ∶ S → !A ⊥ ∥ !B and τ ∶ T → !A ⊥ ∥ !C is defined as ⟨σ, τ ⟩. We have, as required, ̟ B ⊙ ⟨σ, τ ⟩ = ̟ B ⊙ ⟪σ e , τ o ⟫ ≅ σ e ≈ σ, and for the same reason ̟ C ⊙ ⟨σ, τ ⟩ ≈ τ . It is an immediate verification that ⟨-, -⟩ preserves weak isomorphism, so it will still make sense as an operation on the quotient category.

Example 4.6. Consider the copycat strategy c c ! com on ! com .

! com → ! com run -,i ✮ q q x ✐ ✐ ✐ ✐ ✐ ✐ ✐ run +,i ❴ done -,j ✤ ✕ 8 8 E ❯ ❯ ❯ ❯ ❯ ❯ done +,j ✙ ✤ ✪ Following the definition above, ⟨ c c ! com , c c ! com ⟩ is the ∼-strategy illustrated below. ! com → !( com × com ) run -,i ★ n n t ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ run -,j ★ n n t ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ run +,2i ❴ run +,2j+1 ❴ done -,k ✛ B B H ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ✤ done -,l ✛ B B H ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ✤ done +,k ✪ ✤ ✙ done +,l ✪ ✤ ✙
As prescribed by the construction, the positive moves on the left hand side had to be relabeled to avoid the collision in the case where i = j.

σ 1 ∶ !( com × com ) run -,i ❴ run -,j ✲ s s z ♠ ♠ ♠ done +,j ✤ ⟨̟ l ⊙ σ 1 , ̟ r ⊙ σ 1 ⟩ ∶ !( com × com ) run -,i run -,j σ 2 ∶ !( com × com ) run -,i ❴ run -,j ❴ done +,0 ✤ done +,0 ✤ ⟨̟ l ⊙ σ 2 , ̟ r ⊙ σ 2 ⟩ ∶ !( com × com ) run -,i ❴ run -,j ❴ done +,0 ✤ done +,0 ✤ Figure 7.
Failures to surjective pairing Note that the above only displays the event part of the ∼-strategy ⟨ c c ! com , c c ! com ⟩, but its construction also equips it with a symmetry ensuring its uniformity.

Surjective pairing. In order to obtain a product, we also need to prove surjective pairing, that is, that for all σ ∶ S → !A ⊥ ∥ !(B × C), we have:

σ ≈ ⟨̟ B ⊙ σ, ̟ C ⊙ σ⟩
However, as it stands, this is in general not the case.

Example 4.7. In Figure 7, we display on the left hand side two ∼-strategies σ 1 , σ 2 ∶ !1 Tcg + G G !( com × com ), and on the right hand side the corresponding distinct ∼-strategies obtained by projection and pairing.

We observe that surjective pairing fails for these strategies, as behaviours that span both components get erased through composition with the projections. This is analogous as in standard Hyland-Ong games [START_REF] Harmer | Games and full abstraction for nondeterministic languages[END_REF], where single-threadedness ensures that strategies treat independently events hereditarily caused by distinct minimal events. The definition is independent from symmetry, so we state it first in more generality. Definition 4.8. Let σ ∶ S → A be a prestrategy. We say that σ is single-threaded if it satisfies the following two conditions.

(1) For any s ∈ S, [s] has exactly one minimal event written init(s).

(2) Whenever s 1 # s 2 in S, init(s 1 ) = init(s 2 ).

Single-threaded ∼-strategies always satisfy surjective pairing.

Proposition 4.9. Let σ ∶ S → !A ⊥ ∥ !(B × C) be a single-threaded ∼-strategy. Then:

σ ≈ ⟨̟ B ⊙ σ, ̟ C ⊙ σ⟩
Proof. First of all, we define two subsets of S as follows:

S B = {s ∈ S σ (init(s)) ∈ B} S C = {s ∈ S σ (init(s)) ∈ C}
(we abuse notations slightly with ∈ B, ∈ C).

By single-threadedness, S B and S C are disjoint and down-closed, with no immediate conflict spanning both components -in other words, S = S B ⊎ S C . They are obviously still event structures. The restrictions of σ (along with a simple relabeling to !B !C)

σ B ∶ S B → !A ⊥ ∥ !B σ C ∶ S C → !A ⊥ ∥ !C
are receptive and courteous, i.e. are strategies. This decomposition also works at the level of symmetries. Any θ ∈ S preserves S B and S C . Indeed if (s B , s C ) ∈ θ, then (init(s B ), init(s C )) ∈ θ as well: absurd, since one maps to !B and the other to !C. It follows that θ = θ B ⊎ θ C where θ B and θ C are bijections between configurations of S B and S C respectively. The set of restrictions to S B (resp. S C ) of symmetries in S yields a set of bijections between configurations of S B (resp. S C ), which is easily checked to satisfy the conditions for an isomorphism family S B (resp. S C ). The labeling functions σ B and σ C preserve symmetry. Strong-receptivity and thinness follow directly from those for σ, so σ B and σ C are ∼-strategies.

By construction, σ B and σ C have disjoint codomain; so we can form their pairing ⟪σ B , σ C ⟫ without relabeling. Then, the obvious bijection S = S B ⊎ S C ≅ S B ∥ S C is an isomorphism of event structures, preserves symmetry, and preserves labeling so as to yield an isomorphism of ∼-strategies:

σ ≅ ⟪σ B , σ C ⟫ By Proposition 4.5, it follows that ̟ B ⊙ σ ≅ σ B and ̟ C ⊙ σ ≅ σ C . But clearly, ⟪σ B , σ C ⟫ ≈ ⟨σ B , σ C ⟩,
and ⟨-, -⟩ preserves weak isomorphism, so we have surjective pairing. So, single-threadedness ensures surjective pairing. It is clear that copycat ∼-strategies -and lifted ∼-strategies in general -on (expanded) arenas are single-threaded, since C C !A has the shape of a conflict-free forest. In order to get a cartesian category, the last thing to check is that single-threaded strategies are stable under composition.

Single-threadedness and its stability under composition is independent from symmetry, so we state it and prove it below in greater generality.

Proposition 4.10. Let σ ∶ S → A ⊥ ∥ B and τ ∶ T → B ⊥ ∥ C be negative single-threaded prestrategies. Then, τ ⊙ σ is single-threaded.

Proof. The details are rather tedious; we postpone them to Appendix B.5.

We have finished constructing our basic category of Concurrent Hyland-Ong games. Let us call Cho the category having: as objects, negative arenas; and as morphisms from A to B, negative single-threaded ∼-strategies σ ∶ S → !A ⊥ ∥ !B, up to weak isomorphism.

As for Tcg we will also sometimes write

σ ∶ A Cho + G G B to mean that σ is a morphism from A to B in Cho (or just σ ∶ A + G G B
when Cho is clear from the context). We get: Proposition 4.11. The category Cho has finite products.

In particular, it follows as usual that × is a bifunctor Cho 2 → Cho, by setting

σ 1 × σ 2 = ⟨σ 1 ⊙ ̟ A 1 , σ 2 ⊙ ̟ A 2 ⟩, for σ 1 ∶ A 1 + G G B 1 and σ 2 ∶ A 2 + G G B 2 .
When constructing the cartesian closed structure, we will leverage the compact closed structure of Tcg. Therefore, it is useful to connect the cartesian structure of Cho with the monoidal structure of Tcg. For that, we note that there is an isomorphism of essps:

m A,B ∶ !(A × B) ≅ !A ⊗ !B
Using Definition 3.41, it lifts to an iso m A,B in Tcg between them. Consequently:

Lemma 4.12. Let σ 1 ∶ A 1 Cho + G G B 1 and σ 2 ∶ A 2 Cho + G G B 2 . Then, σ 1 × σ 2 ≈ m B 1 ,B 2 -1 ⊙ (σ 1 ⊗ σ 2 ) ⊙ m A 1 ,A 2 Proof. Write σ 1 ∶ S 1 → !A ⊥ 1 ∥ !B 1 and σ 2 ∶ S 2 → !A ⊥ 2 ∥ !B 2 . By definition, σ 1 × σ 2 = ⟨σ 1 ⊙ ̟ A 1 , σ 2 ⊙ ̟ A 2 ⟩ By Lemma 3.43, σ 1 ⊙ ̟ A 1 ≅ (i A ⊥ 1 ∥ !B 1 ) ○ σ 1 and σ 2 ⊙ ̟ A 2 ≅ (i A ⊥ 2 ∥ !B 2 ) ○ σ 2 .
These maps have disjoint codomain, so up to weak isomorphism their pairing is

⟪(i A ⊥ 1 ∥ !B 1 ) ○ σ 1 , (i A ⊥ 2 ∥ !B 2 ) ○ σ 2 ⟫ ∶ S 1 ∥ S 2 → !(A 1 × A 2 ) ⊥ ∥ !(B 1 × B 2 ) Likewise by Lemma 3.43, m B 1 ,B 2 -1 ⊙ (σ 1 ⊗ σ 2 ) ⊙ m A 1 ,A 2
has (up to isomorphism) essp S 1 ∥ S 2 and labeling function the obvious relabeling of σ 1 ⊗ σ 2 by m A 1 ,A 2 and m B 1 ,B 2 . It is a simple verification that these two coincide. 4.2. Cartesian closure. We finish the construction of our cartesian closed category by describing the cartesian closure. We have constructed Cho as a subcategory of Tcgwhich, as a compact closed category, is symmetric monoidal closed. We wish to leverage this closed structure of Tcg in order to transfer it to Cho. 4.2.1. Arrow arena. For two thin concurrent games A and B in Tcg, the corresponding exponential object (following the compact closed structure) is obtained as A ⊥ ∥ B. In Cho, where objects are arenas, this hints at defining the exponential object of A, B as A ⊥ ∥ B. Indeed, it is easy to check that !(A ⊥ ∥ B) ≅ !A ⊥ ∥ !B, so this matches the closed structure of Tcg. However, objects in Cho are required to be negative arenas, and A ⊥ ∥ B is no longer negative. Therefore, we are brought to introduce a negative variant of A ⊥ ∥ B, that would be an object of Cho. The natural choice, familiar from Hyland-Ong games, is to make events in A depend on minimal events of B. It would be incorrect to make events of A depend on all minimal events of B, so we will instead create as many copies of A as they are minimal events in B. Writing min(B) for the set of minimal events of B, we define: Definition 4.13. Let A, B be two negative arenas. Their arrow is A ⇒ B, with the following components.

• Events, and polarity. Those of (∥ b∈min(B) A ⊥ ) ∥ B.

• Causality. As follows:

≤ (∥ b∈min(B) A ⊥ )∥B ⊎{((2, b), (1, (b, a))) b ∈ min(B) & a ∈ A}
Example 4.14. The reader can check that com ⇒ com is the arena presented as com → com in Example 2.5. As com has only one minimal event, there is no duplication of the left hand side. However, the arena com

⇒ ( com × com ) is displayed below. com ⇒ ( com × com ) run - ❞ ❢ ❤ • • ✤ ✤ run - ❞ ❢ ❣ ✐ ❦ ✤ ✤ run + ✤ ✤ run + ✤ ✤ done + done + done - done -
This is exactly the arena construction of [START_REF] Hyland | On full abstraction for PCF: I, II, and III[END_REF], where arenas are forests.

4.2.2. Cartesian closed structure. Our proof of cartesian closure will leverage the compact closed structure of Tcg. More precisely, we will show that there is a bijection (up to weak isomorphism) between negative single-threaded ∼-strategies playing respectively on !A ⊥ ∥ !(B ⇒ C) and !A ⊥ ∥ (!B ⊥ ∥ !C). This bijection will leave the internal event structure of strategies unchanged, and will only operate through relabeling. First, we describe the action of the bijection from

!A ⊥ ∥ !(B ⇒ C) to !A ⊥ ∥ (!B ⊥ ∥ !C).
Let us first explain it on an example. Consider a ∼-strategy represented as below -which is, in essence, a curried version of the contraction on com of Example 4.6.

com ⇒ ( com × com ) run -,i ✩ n n u ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ run -,j ✩ n n u ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ run +,0 ❣ ❡ ❞ ❝ ❛ ❴ run +,0 ❣ ❡ ❞ ❝ ❛ ❴ done -,k ✤ ✚ A A H ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) done -,l ✤ ✚ A A H ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) done +,k ✪ ✤ ✙ done +,l ✪ ✤ ✙
Note that the positive moves on the left hand side have copy index 0, whereas in Example 4.6 they were carefully chosen so as to avoid collisions. This makes sense because the current arena has more causal links: the two positive moves on the left are already made distinct by their justification pointers, so there is no need to distinguish them further via their copy indices. As this example illustrates, we cannot simply relabel this ∼-strategy to com ⊥ ∥ ( com × com ) without changing copy indices, as that would result in a collision, i.e. a failure of local injectivity of the labeling function.

Therefore, we use countability of the arena in order to do a collision-free relabeling.

Lemma 4.15. There is a strong-receptive, courteous map of essps:

χ A,B ∶ !(A ⇒ B) → !A ⊥ ∥ !B
which, additionally, preserves the copy index of negative events.

Proof. For events b ∈ B we use ♯ b for the natural number associated to b by the countability of B. As in Section 2.5, we use ⟨-⟩ ∶ ω 3 → ω for any injective function; the collision with the pairing operation should not generate any confusion. We set:

χ A,B ∶ !(A ⇒ B) → !A ⊥ ∥ !B (α ∶ [(1, (b, a))] → ω) ↦ (1, α ′ ) (β ∶ [(2, b)] → ω) ↦ (2, β ′ ) where: α ′ ∶ [a] → ω a ′ ↦ ⟨♯ b, α((2, b)), α((1, (b, a ′ )))⟩ (if a ′ ∈ min(A)) a ′ ↦ α((1, (b, a ′ ))) (otherwise)
and:

β ′ ∶ [b] → ω b ′ ↦ β((2, b ′ ))
This χ A,B preserves symmetry, is strong-receptive (since minimal events of A ⊥ are positive) and courteous (it only breaks immediate causal links from minimal events of B to minimal events of A ⊥ , so from negative to positive). This allows us, from σ ∶ S → !C ⊥ ∥ !(A ⇒ B), to define its relabeling:

Φ(σ) ∶ S → !C ⊥ ∥ (!A ⊥ ∥ !B) = (!C ⊥ ∥ χ A,B ) ○ σ
For well-chosen hashing function ♯ and injection ⟨-⟩, this relabeling applied to the curried contraction above yields exactly the ∼-strategy of Example 4.6. Before going on to the other direction, we note a further property of this relabeling.

Lemma 4.16. Let σ ∶ S → !C ⊥ ∥ !(A ⇒ B) be a negative single-threaded ∼-strategy. Take s 1 , s 2 ∈ S such that σ s 1 has the form (2, β) with lbl β = (2, b) (b ∈ min(B)), and σ s 2 = (2, α) with lbl α = (1, (b ′ , a)). Then, b = b ′ iff s 1 = init(s 2 ).
Proof. Straightforward consequence of single-threadedness.

Lemma 4.17. Let σ 1 , σ 2 ∶ S → !C ⊥ ∥ !(A ⇒ B) be two negative single-threaded ∼-strategies sharing the same internal ess. Then,

σ 1 ∼ + σ 2 iff Φ(σ 1 ) ∼ + Φ(σ 2 ).
Proof. if. Assume Φ(σ 1 ) ∼ + Φ(σ 2 ). Take x ∈ C (S), and form θ = {(σ 1 s, σ 2 s) s ∈ x}. We wish to prove that θ is a valid symmetry on !C ⊥ ∥ !(A ⇒ B). Firstly, we remark that the following diagram of bijections commutes.

x

σ 1 z z ✉ ✉ ✉ ✉ ✉ ✉ ✉ ✉ ✉ ✉ σ 2 6 6 ■ ■ ■ ■ ■ ■ ■ ■ ■ ■ σ 1 x !C ⊥ ∥χ A,B θ G G σ 2 x !C ⊥ ∥χ A,B Φ(σ 1 ) x θ ′ !C ⊥ ∥(θ ′ !A ⊥ ∥θ ′ !B ) G G Φ(σ 2 ) x
It follows that θ decomposes as θ !C ⊥ ∥ θ !(A⇒B) with θ !C ⊥ ∈ !C ⊥ , and we are left to prove that θ !(A⇒B) ∈ !(A ⇒ B). By construction it is a bijection, so we need to prove that it preserves and reflects causality, that it preserves labels, and that it preserves indices of negative events -which is clear, as they are preserved throughout this diagram.

We prove that it preserves immediate causality. The only nontrivial case concerns immediate causal links not preserved by χ A,B , i.e. those of the form:

σ 1 s 1 = (2, {(2, b) ↦ n}) (2, {(2, b) ↦ n, (1, (b, a)) ↦ p}) = σ 1 s 2
But then, by Lemma 4.16, we have s 1 = init(s 2 ). Since labels are preserved by θ ′ !A ⊥ and θ ′ !B , and using Lemma 4.16 again, we still have θ (σ 2 s 1 ) θ (σ 2 s 2 ). The argument also applies to the θ -1 , which therefore is an order-isomorphism.

Preservation of labels also follows directly from Lemma 4.16. Finally, θ is a positive symmetry as all bijections involved preserve the copy index of negative events.

only if. By preservation of symmetry for χ A,B , and the fact that it preserves the copy index of negative events.

Relabeling from !C

⊥ ∥ (!A ⊥ ∥ !B) to !C ⊥ ∥ !(A ⇒ B)
is more subtle: we go from a game having one copy of A to one having as many as minimal moves in B. Thus, choosing the label for events formerly mapping to A requires identifying a copy of A corresponding to some minimal event in B. Here condition (1) of single-threadedness is crucial: each s mapped to A has a unique minimal dependency init(s) mapped to a minimal event of B, hence specifying the copy of A that s should be sent to. More formally, we prove:

Lemma 4.18. For any single-threaded ∼-strategy σ ∶ S → !C ∥ (!A ∥ !B), there is σ ′ ∶ S → !C ∥ !(A ⇒ B), unique up to positive symmetry, such that σ ∼ + (!C ∥ χ A,B ) ○ σ ′ . Proof. We define σ ′ ∶ S → !C ∥ !(A ⇒ B). For s ∈ S, if σ(s) = (1, γ) we set σ ′ (s) = (1, γ) still. If σ(s) = (2, (2, β)) with β ∶ [b] → ω, then we set σ ′ (s) = (2, β ′ ) with β ′ ∶ [(2, b)] → ω (2, b ′ ) ↦ β(b ′ ) If σ(s) = (2, (1, α)) with α ∶ [a]
→ ω, then by condition (1) of single-threadedness it has a unique minimal dependency init(s) ≤ s. By hypothesis, σ (init(s)) has the form (2, (2, β)) with β = {b ↦ n}. Therefore we set:

α ′ ∶ [(1, (b, a))] → ω (1, (b, a ′ )) ↦ α(a ′ ) (2, b) ↦ n and we define σ ′ (s) = (2, α ′ ).
It is routine to check that this map is strong-receptive and courteous, and that its composition with !C ∥ χ A,B is positively symmetric to σ. It follows from Lemma 4.17 that it preserves symmetry, and that it is unique up to positive symmetry.

From that, we deduce the following.

Proposition 4.19. There is a bijection Φ up to weak isomorphism, preserving and reflecting weak isomorphism, between:

• Negative, single-threaded

∼-strategies σ ∶ S → !C ⊥ ∥ !(A ⇒ B), • Negative, single-threaded ∼-strategies σ ′ ∶ S → !C ⊥ ∥ (!A ⊥ ∥ !B). Moreover this bijection is compatible with pre-composition: for all τ ∶ T → !D ⊥ ∥ !C, Φ(σ) ⊙ τ ≃ Φ(σ ⊙ τ ) Proof. On the one hand Φ(σ) is obtained as (!C ⊥ ∥ χ A,B ) ○ σ, while Φ -1 (σ ′
) is obtained by the unique factorisation of Lemma 4.18. The bijection up to weak isomorphism follows from Lemma 4.18 as well.

We now prove stability under composition. By definition, we have Φ(σ) = (!C ⊥ ∥ χ A,B ) ○ σ. But by Lemma 3.43 this is the same (up to isomorphism) as χ A,B ⊙ σ, so the action of Φ can be obtained by post-composition via a lifted map. Stability under composition follows immediately by associativity of composition.

And finally, we deduce:

Theorem 4.20. The category Cho is cartesian closed.

Proof. We already know that it is cartesian. Throughout this proof, in the construction of the components of the cartesian closed structure, we ignore the associativity and unity isomorphisms from the compact closed structure of Tcg -those can be easily and uniquely recovered from the context.

For any two arenas A, B, we first define the evaluation ∼-strategy:

ev A,B ∶ A × (A ⇒ B) Cho + G G B = (ǫ !A ⊗ !B) ⊙ (!A ⊗ Φ( c c !(A⇒B) )) ⊙ m A,A⇒B
Likewise, for any σ ∶ A × C Cho + G G B, we define its curryfication as:

Λ(σ) ∶ C Cho + G G (A ⇒ B) = Φ -1 (!A ⊥ ⊗ (σ ⊙ m A,C -1 ) ⊙ (η !A ⊗ !C))
It is then a straightforward equational reasoning to prove the two equations [START_REF] Lambek | Introduction to higher-order categorical logic[END_REF], for

σ ∶ A × C Cho + G G B and τ ∶ C Cho + G G (A ⇒ B), (β) ev A,B ⊙ (A × Λ(σ)) ≈ σ (η) Λ(ev A,B ⊙ (A × σ)) ≈ σ
using mainly Proposition 4.19 and the compact closed structure of Tcg, in combination with Lemma 4.12 to relate the cartesian structure of Cho and the monoidal structure of Tcg -all the structural isomorphisms involved in the definition cancel each other.

Recursion.

As the final technical part of this paper, we prove that Cho supports the interpretation of a fixpoint combinator. Usually in game semantics, the interpretation of the fixpoint combinator Y is obtained by showing that the category of games and strategies is enriched over a category of sufficiently complete partial orders. Here however it will not be the case: indeed, just as in AJM games [AJM00], our cartesian closed category is a quotient (its morphisms being weak isomorphism classes). It is not clear that the natural ordering on weak isomorphism classes is complete. However, this is not a real issue: although weak isomorphism classes of ∼-strategies might not form a complete partial order, concrete ∼-strategies do. Therefore, when solving recursive strategy equations, we will make sure to work with concrete ∼-strategies rather than weak isomorphism classes.

Our first step will be to order (concrete) ∼-strategies.

Definition 4.21. Let σ ∶ S → A, τ ∶ T → A be two ∼-strategies on a tcg A. We write σ ⊴ τ iff S ⊆ T , the inclusion map S ↪ T is a map of essps, with all data in S coinciding with the restriction of that in T , and such that for all s ∈ S, σ s = τ s

The ∼-strategies on A ordered by ⊴ form a directed complete partial order (dcpo). It is not pointed though -it does not have a least element. Indeed, although a ⊴-minimal ∼-strategy only comprises (by receptivity) events matching minimal negative events of A, their name in S is arbitrary, so there is one ⊴-minimal ∼-strategy on A for each renaming of the minimal negative events of A. For each A we distinguish one ⊴-minimal ∼-strategy A ∶ min -(A) → A that has as events the negative minimal events of A with induced symmetry, and as labeling function the identity. Not every ∼-strategy is above A . However, for every ∼-strategy σ ∶ S → A, we pick one σ ≅ σ † such that A ⊴ σ † obtained by renaming the minimal negative events of S. We write D A for the pointed dcpo of ∼-strategies above A .

Lemma 4.22. For any tcg A, D A is a pointed dcpo with A as minimal element.

Proof. If Γ = {γ ∶ S γ → A} ⊆ D A is a directed subset of D A , we form ∨Γ = ∪γ ∶ ⋃ γ∈Γ S γ → A
with all components defined as componentwise union.

It is direct that this defines a ∼-strategy, which is the least upper bound of Γ.

If all ∼-strategies in a directed set Γ are negative or single-threaded, so is ∨Γ. We now note that all the operations we defined on ∼-strategies in this section are continuous for ⊴.

Lemma 4.23. Composition, tensor, pairing, curryfication and the (-) † operation defined above are continuous for ⊴.

Proof. Straightforward.

From the above, we deduce the following.

Corollary 4.24. For any arena A there is a fixpoint combinator

Y A ∶ (A ⇒ A) Cho + G G A, i.e.
a single-threaded ∼-strategy such that:

Y A ≈ ev A,A ⊙ ⟨Y A , c c !(A⇒A) ⟩
Proof. First, we define the following operation, using the combinators on Cho.

F ∶ D !(A→A) ⊥ ∥!A → D !(A→A) ⊥ ∥!A σ ↦ (ev A,A ⊙ ⟨σ, c c !(A⇒A) ⟩) †
By Lemma 4.23 it is continuous, and from the outermost dagger it has indeed value in D !(A⇒A) ⊥ ∥A . Thus, we can take its least fixpoint Y A ∈ D !(A⇒A) ⊥ ∥A . The weak isomorphism in the statement actually follows as an equality.

Interpretation of IPA

In this section, we illustrate our model by defining the interpretation of IPA, displaying the interpretation of programs of interest, and proving a few properties along the way. We emphasise here that our purpose is not to prove full abstraction, nor to prove deep properties of the interpretation. We feel indeed that given the length of the paper, the specifics of such an endeavour are best left for later. Furthermore, it is our impression that it serves the purpose of this paper better (introducing and developing Concurrent Hyland-Ong games) to give the reader an understanding of what the model computes, what it can and cannot do, rather than delve into additional technical developments.

Throughout this section, by strategy we mean ∼-strategy (symmetries will be implicit).

5.1. Sequential innocent part. In this subsection, we focus on the interpretation of the (sequential) innocent part of IPA, i.e. essentially PCF, plus the combinators for commands.

In other words, it lacks state and parallel composition of commands.

tt = ! B q -,i ❴ tt +,0 ✤ ff = ! B q -,i ❴ ff +,0 ✤ n = ! N q -,i ❴ n +,0 ✤ skip = ! com run -,i ❴ done +,0 ✤ Figure 8. Interpretation of constants of IPA
Interpretation of types. The arenas for the types com and B were given in Example 2.5. The interpretation for N is a countably infinite variant of the interpretation of B:

N q - ✠ ❱ ▼ ❈ 0 + 1 + . . . n + . . .

The interpretation extends to all types (not containing ref ), with

A → B = A ⇒ B .
Interpretation of terms. The interpretation follows the standard lines of the interpretation of the λ-calculus in a cartesian closed category. A context Γ = x 1 ∶ A 1 , . . . , x n ∶ A n is interpreted as the product Π 1≤i≤n A i (which is just the parallel composition of the A i s).

A typing sequent Γ ⊢ M ∶ A is interpreted as a Cho-morphism:

Γ ⊢ M ∶ A ∶ Γ Cho + G G A
For the λ-calculus combinators -variables, application, abstraction -, the interpretation is standard (and we do not detail it). For the fixpoint combinators, we use the combinator Y of Section 4.3. The interpretation of constants is displayed in Figure 8. Note that we only display representations, treating multiple copies of Opponent moves symbolically. The reader should be able to expand them unambiguously to the full event structures, and to detail their isomorphism families. Note also that we give these interpretations over the empty context -they can easily be relabeled to any context Γ.

Likewise, the interpretation of function symbols is given in Figure 9. We have only one figure for a unary function op ∶ X → X, which covers (up to obvious relabeling) the cases of succ ∶ N → N, pred ∶ N → N and iszero ∶ N → B. The interpretation of sequents involving those follows as usual, with e.g. the following composition in Cho:

Γ ⊢ if M N 1 N 2 ∶ X = if ⊙ ⟨ M , N 1 , N 2 ⟩ ∶ Γ Cho + G G X
At this point, we have defined the interpretation of the sequential innocent fragment of IPA. Using the cartesian closed structure and the definition of the fixpoint combinator, it would be straightforward to prove soundness and adequacy of the interpretation, e.g. using logical relations. We refrain from detailing this -rather standard -proof.

The paper already contains some examples of the interpretation of terms of the fragment of IPA currently under study, most notably in Section 2 -where for some, copy indices need to be adequately adjoined. The interpretation of such terms yields rather simple event structures, whose causal order is forest-shaped and without conflict. Modulo copy indices, and as it was noted in Section 2, these forests exactly coincide with the view

op -= ! X ⊥ ∥ ! X q -,i ✱ r r z • • • • • • • q +,i ❴ x -,j ✤ ✒ 6 6 D | | | | op(x) +,⟨j,♯ x⟩ ✙ ✤ ✪ -; -= ! com × X ⊥ ∥ ! X run -,i ✪ o o u ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡ run +,i ❴ done -,j ✤ ✓ 7 7 D ❙ ❙ ❙ ❙ run +,⟨i,j⟩ ❴ x -,k ✤ ✒ 6 6 D | | | | | x +,⟨j,k⟩ ✚ ✛ ✢ ✤ ✦ ★ ✩ if ---= ! B × X × X ⊥ ∥ ! X q -,i ✩ n n u ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ q +,i ❆ z z Õ ⑥ % % 6 tt -,j 1 ✁ ✕ 8 8 E ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ff -,j 2 ❂ ✕ 8 8 E ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ q +,⟨i,j 1 ⟩ ❴ q +,⟨i,j 2 ⟩ ❴ x -,k 1 ✤ ✖ 9 9 F ❱ ❱ ❱ ❱ ❱ ❱ ❱ ❱ ❱ ❱ x -,k 2 ✤ ✘ @ @ G ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ x +,⟨1,j 1 ,k 1 ⟩ ✛ ✙ ✗ ✖ ✔ ✒ ✏ x +,⟨2,j 2 ,j 2 ⟩ ★ ✪ ✫ ✭ ✯ ✱ ✳ Figure 9
. Interpretation of sequential function symbols of IPA functions of standard Hyland-Ong games: their branches are exactly the P -views. Hence, our interpretation computes the composition of innocent strategies while staying within a causal representation corresponding to view functions, never resorting to expanded plays.

Non-determinism. Although the fragment of the language currently under study is deterministic, we find it interesting to study some examples given by its extension with a nondeterministic primitive. Therefore, we add to the language a new constant coin ∶ B which returns a random boolean. Its interpretation is (an obvious extension with copy indices of) the strategy on the left hand side of Figure 5. For Γ ⊢ M, N ∶ A, we define as syntactic sugar a non-deterministic sum

Γ ⊢ M + N ∶ A as Γ ⊢ if coin M N ∶ A.
We give in Figure 10 representations of the interpretation of some well-chosen terms. Copy indices are not exactly as given by the interpretation function (though they are up to weak isomorphism): they have been relabeled for convenience of presentation.

As Figure 10a illustrates, the model represents non-determinism in a non-idempotent way: redundant non-deterministic choices are kept separate by the interpretation. In Figure 10c, (which is syntactic sugar for Y (λx B .x)) is interpreted as the empty strategy. The interpretation of tt + illustrates that, despite displaying explicitely the point of non-deterministic branching, the hiding step of the interpretation removes some diverging branches of the interaction. Figures 10b and10d display two strategies which have the

! B q -,i ❅ z z Õ ⑦ % % 6 ❃ ❃ ❃ tt +,0 ✎ / o / o / o tt +,0 ✴ ❃ (a) tt + tt ! B → B ⊥ ∥ ! B q -,i ❁ y y Ó ⑤ ⑤ ⑤ q +,i ✶ t t } q q q q q q ❴ q -,j ❆ z z Õ ✁ ✁ ✁ ⑦ % % 6 ❃ ❃ ❃ ③ q ✐ b -,k ✤ ✄ ' ' 8 ❈ ❈ ❈ tt +,0 ✏ ✁ / o / o / o ff +,0 ❃ b +,k ✘ ✚ ✢ ✤ ✦ ✩ ✫ (b) f ∶ B → B ⊢ f (tt + ff ) ∶ B ! B q -,i ❴ tt ✤ (c) tt + ! B → B ⊥ ∥ ! B q -,i ✭ p p w ❤ ❤ ❤ ❤ ❤ ❤ ❤ ❤ ❤ ❤ ❤ ❤ ❤ ❤ ❤ ✷ u u } r r r r r r q +,i / o / o / o ❴ ✱ r r z • • • • • • • • • • • q +,i ❴ ✱ r r z • • • • • • • • • • • q +,0 r ♦ • ✐ ❢ ❴ q +,0 r ♦ • ✐ ❣ ❴ b -,k 1 ✤ ✑ 6 6 D ◗ ◗ ◗ ◗ ◗ ◗ ◗ ◗ ◗ ◗ b -,l 2 ✤ ✑ 6 6 D ◗ ◗ ◗ ◗ ◗ ◗ ◗ ◗ ◗ ◗ ◗ tt +,0 ✤ ff +,0 ✤ b +,k 1 ✜ ✚ ✘ ✖ ✔ ✑ ✎ b +,l 2 ✦ ★ ✪ ✭ ✯ ✱ ✴ (d) f ∶ B → B ⊢ (f tt) + (f ff )
Figure 10. Intepretation of some non-deterministic terms same branches (P-views), but differ in their branching points. This gives an interpretation of non-deterministic sequential programs that is similar to Tsukada and Ong's recent presheaf-based model [START_REF] Tsukada | Nondeterminism in game semantics via sheaves[END_REF], although our composition mechanism is very different. It is fairly easy to capture exactly their category as a subcategory of Cho, whose morphisms are sequential innocent [CCW14, CCW15] but not deterministic. 5.2. Concurrent innocent part. Now, we go on to show how our model represents concurrent primitives. The only concurrent primitive of IPA is parallel composition, whose interpretation relies on the following strategy This strategy is no longer a forest, but rather a directed acyclic graph. We also note that this is a deterministic strategy: there is no conflict in its event structure. As we shall see later, without any non-deterministic primitive, it is only in the presence of shared state that non-deterministic strategies will arise. In fact, a major advantage of our approach to modeling concurrent languages is that, not being based on interleavings, we represent the execution of such non-interfering terms deterministically.

∥ = ! com × com ⊥ ∥ com run -,i ✪ o o u ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ✯ q q x • • • • • • • • run +,i ❴ run +,i ❴ done -,j ✤ ✙ A A G ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( done
-,k ✤ ✔ 8 8 E ❚ ❚ ❚ ❚ ❚ ❚ done +,⟨j,k⟩ ✚ ✢ ✤ ✦ ✩ ✫ q -,i 3 ✷ u u } r r r r r r ☞ 3 3 A ▲ ▲ ▲ ▲ ▲ ▲ q +,i 1 ❋ } } × ✝ ✝ ✝ ① # # 3 ✽ ✽ ✽ q +,i 2 ❋ } } × ✝ ✝ ✝ ② # # 4 ✾ ✾ ✾ tt -,j 1 1 ✇ # # 3 ✼ ✼ ✼ ✼ ✝ ff -,j 2 1 ③ $ $ 4 ✿ ✿ ✿ tt -,k 1 2 ❉ | | Ö ☎ ☎ ☎ ✝ ff -,k 2 2 ❋ } } × ✝ ✝ ✝ ✾ tt +,⟨1,j 1 ⟩ 3 ✔ ✒ ✏ ✍ ☛ ✠ ✝ tt +,⟨2,⟨j 2 ,k 1 ⟩⟩ 3 ✤ ✤ ✤ ✤ ✤ ✤ ✤ ✤ ff +,⟨j 2 ,k 2 ⟩ 3 ✯ ✱ ✳ ✶ ✸ ✻ ✾ (a) Parallel left-or on ! B 1 × B 2 ⊥ ∥ ! B 3 q -,i 3 ✸ u u ~ss s s s s ☛ 2 2 A ❑ ❑ ❑ ❑ ❑ ❑ q +,i 1 ❋ } } × ✝ ✝ ✝ ① # # 3 ✽ ✽ ✽ q +,i 2 ❋ } } × ✝ ✝ ✝ ② # # 4 ✾ ✾ ✾ tt -,j 1 1 ✇ # # 3 ✼ ✼ ✼ ✝ ff -,j 2 1 ✑ 6 6 D ◗ ◗ ◗ ◗ ◗ ◗ ◗ ◗ ◗ ◗ ◗ ✽ tt -,k 1 2 ❋ } } × ✝ ✝ ✝ ✝ ff -,k 2 2 ❋ } } × ✝ ✝ ✝ ✾ tt +,j 1 3 / o / o / o / o ✕ ✓ ✑ ✍ ☞ ✠ ✞ tt +,k 1 3 ✤ ✤ ✤ ✤ ✤ ✤ ✤ ✤ ff +,⟨j 2 ,k 2 ⟩ 3 ✮ ✰ ✳ ✵ ✷ ✺ ✽ (b) Parallel-or on ! B 1 × B 2 ⊥ ∥ ! B 3
In [START_REF] Castellan | The parallel intensionally fully abstract games model of PCF[END_REF], we exploit this property: we give a concurrent notion of innocence where strategies are directed acyclic graphs rather than forests, and using this notion we give an intensionally fully abstract model of a variant of PCF where independent computations are performed in parallel. The detailed construction is out of the scope of this particular paper, but let us illustrate it with two examples that are both concurrent innocent.

Figure 11 displays two concurrent innocent strategies (we associate moves to the corresponding sub-type using indices rather than location). In Figure 11a, we have a strategy for a parallel implementation of the left or, that is strict in its left argument. Indeed, although the strategy starts evaluating both its arguments in parallel, it can only return at toplevel if its first argument has returned. However, this is not true anymore for the strategy of Figure 11b. There, it suffices that one argument returns tt for the overall computation to return tt -indeed, this strategy computes the well-known parallel-or function [START_REF] Plotkin | LCF considered as a programming language[END_REF]. 5.3. Stateful part. Finally, we finish the interpretation of IPA and describe how to interpret the primitives dealing with manipulations of state. For the simplicity of presentation, references only store booleans; however the method applies just as well to integers.

A variable can be interacted with in two ways: via reading and writing. As usual in game semantics, we follow this idea for the interpretation of variables, and take ref to be a product arena comprising actions for reading the reference or writing on the reference. More precisely, we define:

ref = R - ✎ ❃ ✴ W - tt W - ff tt +
ff + ok + ok + We now describe the interpretation of term constructors for the manipulation of state. As usual, assignment and dereferenciation are simply interpreted as (sequential innocent)

! ref × B ⊥ ∥ ! com run -,i ✮ q q x ✐ ✐ ✐ ✐ ✐ ✐ ✐ ✐ q +,i ❴ b -,j ✲ s s z ♠ ♠ ♠ ♠ ♠ ✤ W ⟨i,j⟩ b ❴ ok -,k ✤ ✙ A A G ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( done
+,⟨j,k,♯ b⟩ ✚ ✜ ✢ ✤ ✦ ✧ ✩ (a) -∶= - ! ref ⊥ ∥ ! B q -,i ✳ s s { ♥ ♥ ♥ ♥ ♥ ♥ ♥ R +,i ❴ b -,j ✤ ✏ 5 5 C b +,j ✚ ✢ ✤ ✦ ✩ ✫ (b) ! - Figure 12.
Strategies for assignment and dereferenciation strategies that interact with the memory cell. We give in Figure 12 the strategies used in the interpretation of those. Using those, we can define:

Γ ⊢ M ∶= N ∶ com = -∶= -⊙ ⟨ M , N ⟩ Γ ⊢ ! M ∶ B = ! -⊙ M
Before giving the interpretation of genuine references, we mention that the interpretation of mkvar exploits as usual the isomorphism between ref and B × com 2 [AM96].

New reference. As usual, the subtle part is the interpretation of newref . Indeed, whereas the strategies for assignment and dereferenciation only interact with the interface of the variable in an innocent way, it is newref that provides an implementation for the memory.

If Γ, x ∶ ref ⊢ M ∶ A depends on a reference x, its interpretation plays on (up to iso) ! ref ⊥ ∥ ! Γ ⊥ ∥ ! A . Naively (we will see that this is a slight simplification), all we have to do is to build a strategy cell ∶ ! ref , and compose M with it to obtain newref x in M .

To define cell, we keep in mind the operational behaviour of a memory cell. In our (sequentially consistent) understanding of memory in a concurrent setting, although reads and writes are called concurrently, they are performed in some sequential order by the central memory. Thus the behaviour of a boolean memory cell is best described as the prefix language of the infinite traces:

Cell tt ∶∶= R -⋅ tt + ⋅ Cell tt W - tt ⋅ ok + ⋅ Cell tt W - ff ⋅ ok + ⋅ Cell ff Cell ff ∶∶= R -⋅ ff + ⋅ Cell ff W - tt ⋅ ok + ⋅ Cell tt W - ff ⋅ ok + ⋅ Cell ff
This language is ordered by prefix, so that Cell ff is a forest. Setting all incomparable words to conflict with each other, we get an event structure whose events are words, and configurations are prefix-closed sets of prefixes of a word -so in one-to-one correspondence with words. This event structure, with the obvious labeling function, can be regarded as a prestrategy on ref (not on ! ref ). But in order to fit in our framework, we need to equip it with copy indices (and symmetry). This calls for extra bookkeeping, as we need to make sure that the same copy index is not used twice in the same branch. We define

! ref → X ⊥ ∥ ! X q -,i ✹ u u t t t q +,i ✷ u u } r r r ❴ Cell r x -,j ☞ 3 3 A ▲ ▲ ▲ x +,j ✙ ✤ ✪ Figure 13. The pre-∼-strategy newcell Cell I R ,I tt ,I ff tt ∶∶= R -,i ⋅ tt +,0 ⋅ Cell I R ∪{i},I tt ,I ff tt (i ∈ I R ) W -,i tt ⋅ ok +,0 ⋅ Cell I R ,I tt ∪{i},I ff tt (i ∈ I tt ) W -,i ff ⋅ ok +,0 ⋅ Cell I R ,I tt ,I ff ∪{i} ff (i ∈ I ff )
and similarly for Cell I R ,I tt ,I ff ff . Then we define the event structure Cell via Cell ∅,∅,∅ ff , as we did above. It has an isomorphism family, that relates any two words differing only on their copy indices. Moreover the names of the events denote the labeling function to ! ref (with all positive moves pointing -that is, being immediately dependent in the game -to the prevous move). Overall, we get a map of essp:

/ o / o / o / o / o / o ❴ W -,7 tt ❴ ff +,0 ✤ ❴ ff +,0 ✤ ok +,0 ✤ ✻ v v Ð ✈ ✈ ✈ ✈ ✠ 1 1 @ ■ ■ ■ ■ R -,4 ❴ R -,0 / o / o / o / o / o / o / o ❴ W -,7 ff ff +,0 ✤ tt +,0

✤

We have constructed cell ∶ Cell → ! ref a map of essps. Unfortunately, cell is not a ∼strategy: it is neither receptive (after playing R -,4 above one cannot play R -,4 , although it is compatible in the game) nor courteous (we have ff +,0 R -,4 which does not hold in ! ref ). However, cell is a thin pre-∼-strategy, and as such can be composed with M ∶ ! ref ⊥ ∥ ! A to obtain M ⊙ cell -and it turns out that M ⊙ cell is always a valid ∼-strategy.

Still, that is not quite what we want. The intended semantics for newref x in M is that each of its evaluations spawns a new, independent memory cell, whereas the operation above would have it spawned once and for all and shared over all copies of M . In other words, M ⊙ cell is a valid ∼-strategy indeed, but it might not be single-threaded. So finally, we build another pre-∼-strategy displayed in Figure 13, where Cell means a copy of the pre-∼-strategy above, with minimal events pointing as indicated.

Finally, from Γ, x ∶ ref ⊢ M ∶ X, we define:

newref r in M = newcell ⊙ Λ( M ) ∶ ! Γ Tcg + G G ! X Then,
despite newcell being a pre-∼-strategy rather than a ∼-strategy, we have: Proposition 5.2. For any Γ, x ∶ ref ⊢ M ∶ X, the thin pre-∼-strategy:

newref r in M = newcell ⊙ Λ( M ) is a single-threaded ∼-strategy.
Proof. The composition is well-defined (as a map of essps) since both compounds are ∼receptive. Moreover, both compounds are also componentwise courteous (see Definition 3.35), so by Lemma 3.36 the composition newcell ⊙ Λ( M ) is a componentwise courteous pre-∼-strategy. It is also thin, negative and single-threaded as these properties are stable under composition (respectively Lemmas 3.34, 4.3 and Proposition 4.10).

It remains to check that it is receptive and courteous. But that does not involve symmetry at all; and by the results of [START_REF] Rideau | Concurrent strategies[END_REF][START_REF] Castellan | Games and strategies as event structures[END_REF] it suffices to check that

c c ! X ⊙ (newcell ⊙ Λ( M )) ⊙ c c ! Γ ≅ newcell ⊙ Λ( M )
but that follows from the composition of componentwise courteous pre-∼-strategies being associative, Λ( M ) being a strategy, and the easy fact that c c ! X ⊙ newcell ≅ newcell.

This concludes the definition of the interpretation of IPA in Cho. As said before, we do not aim in this paper to prove properties of this interpretation, such as soundness or adequacy -those could be either proved directly as in [START_REF] Abramsky | Linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions[END_REF], or more easily by constructing a functor to the interpretation of [START_REF] Abramsky | Linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions[END_REF] linearizing the partial orders. In any case, the proof would take additional space without bringing much insight or taking advantage of the more refined representation offered by our event structures strategies, so we chose not to include it. However, we will now illustrate this interpretation by providing some examples.

Some examples.

First example: strictness test. As a first example, we detail the interpretation of the term of Example 2.22. Recall that it was:

newref b in λf com→com . f (b ∶= tt); !b ∶ (com → com) → B
As the constructor new is only defined on terms of ground type, this is just syntactic sugar for λf com→com . newref b ∈ f (b ∶= tt); !b ∶ (com → com) → B. In order to define its interpretation, the first step is to define:

f ∶ com → com, b ∶ ref ⊢ f (b ∶= tt); !b ∶ B ∶ com → com × ref Cho + G G B
This is covered by the definitions above, using the cartesian closed structure and the strategies of Figure 12 for assignment and dereferenciation. Computing this yields the strategy represented below (again, the copy indices given by the actual interpretation function differ, but this is irrelevant up to weak isomorphism). Again, this deterministic event structure is forest-shaped and its branches are versions with explicit copy indices of the P-views of the corresponding innocent strategy in Hyland-Ong games.

f com→com ⊢ λr ref . f (r ∶= tt); !r = ! com → com ∥ ! ref → B q -,i ✩ n n u ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞ run +,i ✮ q q x ✐ ✐ ✐ ✐ ✐ ✐ ✐ ❴ run -,j ✙ A A G ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( (
• ✐ ❢ ❝ done -,k ✤ ✗ 9 9 F ❲ ❲ ❲ ❲ ❲ ❲ ❲ ❲ ❲ ❲ ❲ W +,j tt ❴ ⑦ ④ ① ✉ s ♣ R +,k ✎ ☞ ✠ ✆ ✁ ❴ ok -,l ✤ ✪ o o u ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡ b -,m ✤ ✏ 5 5 C done +,l ✪ ✤ ✙ b +,⟨k,m⟩ ✚ ✜ ✢ ✤ ✦ ✧ ✩
Now, we compose it with newcell. We represent below the event structure resulting from their interaction. Events of the hidden/synchronised part of the interaction no longer have a well-defined polarity, hence we set it to 0. After hiding, the minimal conflict between the first two events in cell is inherited by the final positive events. The reader can check that hiding yields (up to the copy indices) the event structure of Example 2.22.

! com → com ⊥ ∥ ! ref → B ⊥ ∥ ! B q -,i ✮ q q x ✐ ✐ ✐ ✐ ✐ ✐ ✐ ✐ ✐ ✐ ✐ q 0,i ✪ o o u ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ run +,i ❴ ✭ p p w ❤ ❤ ❤ ❤ ❤ ❤ ❤ ❤ ❤ run -,j ♥ ❦ ❤ ❡ ❝ ✘ @ @ G ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ✏ 5 5 C done -,k ✤ ✕ 8 8 E ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ♦ ' ✴ ✴ ✴ ✴ ✴ ✴ ✴ ✴ ✴ ✴ ✴ ✴ W 0,j tt ⑤ ② ✈ t r ♦ / o / o ❴ R 0,k ✌ ✡ ✞ ✄ ⑧ ❴ ok 0,0 ✤ ❴ ✸
u u ~ss s s s s s s s s s s s s s s s s s s s s s s s s s s

ff 0,0 ✤ ❴ ✂ ' ' 7 ❇ ❇ ❇ ❇ ❇ ❇ ❇ ❇ ❇ ❇ ❇ ❇ ❇ ❇ ❇ R 0,k ✍ ✌ ☛ ✡ ✟ ✞ ✆ ✄ ✁ ⑥ ⑤ ③ ❴ W 0,j tt ✖ ✔ ✓ ✑ ✎ ✌ ☛ ❴ tt 0,0 ✤ ✕ 8 8 E ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ok 0,0 ✤ ✰ r r y ❦ ❦ ❦ ❦ ❦ ❦ ❦ ❦ ❦ ❦ ❦ ❦ ❦ ❦ ❦ ❦ ❦ ❦ ❦ tt 0,⟨k,0⟩ ✣ ✢ ✜ ✜ ✛ ✛ ✚ ✙ ✙ ✘ ✘ ✗ ✖ ✖ ✖ 9 9 F ❱ ❱ ❱ ❱ ❱ ❱ ❱ ❱ ❱ ❱ ff 0,⟨k,0⟩ ✥ ✦ ✧ ✧ ★ ★ ✩ ✪ ✪ ✫ ✬ ✬ ✭ ✭ ✕ 8 8 E ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ done +,0 ✜ ✛ ✙ ✘ ✖ ✕ ✓ done +,0 ★ ✩ ✪ ✬ ✭ ✯ ✰ tt +,⟨k,0⟩ ✤ ✣ ✣ ✢ ✢ ✜ ✜ ✛ ✛ ✛ ✚ ✚ ✙ ✙ ✘ ff +,⟨k,0⟩ ✤ ✥ ✥ ✦ ✦ ✧ ✧ ★ ★ ✩ ✩ ✩ ✪ ✪ ✫
The reader familiar with Abramsky and McCusker's model for IA will see that taking the plays -i.e. alternating well-bracketed linear orderings of configurations, without copy indices -yields the expected sequential strategy. But our model says more, e.g. it specifies the behaviour of the strategy if Opponent both asks its argument and returns in parallel.

Second example: synchronization through state. We interpret the following term of IPA.

x ∶ com, y ∶ com ⊢ newref r in if (!r) (x; r ∶= tt) ∥ if (!r) y ∶ com
This term simulates sequential composition through parallel composition and state up to may-equivalence: the only execution that survives divergence is the one where the first thread is executed before the second, so that y is run after x has terminated.

As before, we first compute the interpretation of the variant of this term where the variable has been abstracted away, obtaining the following strategy.

! com ⊥ ∥ ! com ⊥ ∥ ! ref → com run -,i ✩ n n u ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞ ✯ q q x • • • • • • • • • R +,0 ❤ ❤ ❣ ❢ ❢ ❡ ❞ ❞ ❝ ❜ ❜ ❛ ❵ ✺ v v ✉ ✉ ✉ ✉ ✁& & 7 ❆ ❆ R +,1 q ♠ • ❣ ❡ ❆ z z Õ ✁ ✁ ⑥ % % 6 ❂ ❂ tt -,j1 ✉ • ff -,j2 ❆ ★ n n t ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ ❝❝ tt -,j3 ✁ ✪ o o u ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ff -,j4 ❂ run +,⟨i,j2⟩ ❴ run +,⟨i,j3⟩ ❴ done -,k ✤ ✘ @ @ G ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ done -,l ✤ ✑ 6 6 D W +,⟨j2,k⟩ tt ② ② ① ✇ ✇ ✈ ✉ ✉ t s s r r q ❴ ok -,m ✤ ✛ B B H ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ done +,⟨j2,k,l,m⟩ ✜ ✜ ✢ ✢ ✣ ✣ ✤ ✥ ✥ ✦ ✦ ✧ ✧ ★
We now compute a part of the interaction with newcell, pictured below.

! com ⊥ ∥ ! com ⊥ ∥ ! ref → com ∥ ! com run -,i ✭ p p w ❤❤ ❤❤ ❤❤ ❤❤ ❤❤ ❤❤ run 0,i ✩ n n u ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞ ❞❞❞ ❞ ✮ q q x ✐✐ ✐✐ ✐✐ ✐✐ ✐✐ R 0,2i ❴ ❣ ❣ ❢ ❡ ❡ ❞ ❞ ❝ ❝ ❜ ❜ ❛ ❵ / o / o / o / o / o / o / o R 0,2i+1 ❴ ♥ ❦ ✐ ❣ ❞ ff 0,0 ✯ q q x • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • ✐ $ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✮ ✤ ff 0,0 ❴ ✤ R 0,2i ❴ ✝ ✄ ⑥ ③ ✇ ✉ ff 0,0 ✧ m m t ❜❜❜ ❜❜❜ ❜❜❜ ❜❜❜ ❜❜❜ ❜❜❜ ❜❜❜ ❜❜❜ ❜❜❜ ❜❜❜ ❜❜❜ ❜❜❜ ❜❜❜ ❜❜❜ ❜❜❜ ✤ run +,⟨i,0⟩ ❴ run +,⟨i,0⟩ ❴ done -,k ✚ A A H ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ✤ ✕ 8 8 E ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ ❯ done -,l ✛ B B H ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ❬ ✤ W 0,⟨0,k⟩ tt / o / o / o / o / o ⑧ ⑦ ⑦ ⑥ ⑤ ⑤ ④ ④ ③ ② ② ① ① ① ① ✇ ✇ ✇ ❴ R 0,2i+1 ❴ ✌ ☞ ☛ ☛ ✡ ✡ ✠ ✟ ✟ ✞ ✝ ✝ ✆ ☎ ☎ W 0,⟨0,l⟩ tt ❴ ✕ ✔ ✓ ✓ ✒ ✒ ✑ ✑ ✏ ✏ ✎ ✍ ✍ ✌ ✌ ok 0,0 ✤ ❴ ff 0,0 ✤ ❴ ok 0,0 ✤ R 0,2i+1 ✝ ✝ ✝ ✆ ✆ ✆ ✆ ☎ ☎ ☎ ☎ ✄ ✄ ✄ ✄ ✂ ✂ ✂ ✂ ✁ ✁ ✁ ⑧ ⑧ ⑧ ⑦ ❴ W 0,⟨0,k⟩ tt ✑ ✏ ✏ ✏ ✎ ✎ ✍ ✍ ✌ ✌ ☞ ☞ ☛ ☛ ☛ ❴ tt 0,0 ✤ ✴ s s { ♦ ♦ ♦ ♦ ok 0,0 ✤ run +,⟨i,0⟩ ❴ done -,m ✤ ✜ B B I ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ ❭ done 0,⟨0,k,m,0⟩ ✢ ✢ ✢ ✣ ✣ ✣ ✣ ✣ ✣ ✣ ✣ ✤ ✤ ✤ ✤ ✤ ✤ ✤ ✥ ✥ ✥ ✥ ✥ ✥ ✥ ✦ ✦ ✦ ✦ ✦ ✖ 9 9 F ❱ ❱ ❱ ❱ ❱ ❱ ❱ ❱ done +,⟨0,k,m,0⟩ ✢ ✢ ✢ ✣ ✣ ✣ ✣ ✣ ✣ ✣ ✣ ✤ ✤ ✤ ✤ ✤ ✤ ✤ ✤ ✤ ✥ ✥ ✥ ✥ ✥ ✥ ✥ ✥ ✦ ✦ ✦
which, after hiding, yields a strategy with sub-event structures such as:

λx com , y com . newref r in (if (!r) (x; r ∶= tt)) ∥ (if (!r) y ) = ! com ⊥ ∥ ! com ⊥ ∥ ! com run -,i ✪ o o u ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ★ n n t ❝❝❝ ❝❝❝ ❝❝❝ ❝❝❝ ❝❝❝ ❝❝❝ ❝❝ ❝❝❝ ❝❝❝ ❝❝ ❝❝❝ ❝❝❝ ❝❝ ❝❝ run +,⟨i,0⟩ / o / o / o ❴ ❡ ❡ ❞ ❞ ❞ ❝ ❝ ❜ ❜ ❛ ❛ ❛ ❵ run +,⟨i,0⟩ ❴ ❤ ❣ ❢ ❢ ❡ ❡ ❞ ❝ ❝ ❜ ❛ ❛ done -,l ✤ done -,k ✤ ✓ 7 7 D ❙ ❙ ❙ ❙ ❙ ❙ run +,⟨i,0⟩ ✞ ☎ ✁ ⑦ ④ ① ✉ ❴ done -,m ✕ 8 8 E ❯ ❯ ❯ ❯ ❯ ❯ ✤ done +,⟨0,k,m,0⟩ ✛ ✜ ✣ ✤ ✥ ✧ ★
Here, there are several observations to make. Firstly, the copy index of the call to y does not depend on k. This might seem surprising: the diagram suggests that if Opponent plays two occurrences of done -,k , once with k = 0 and once with k = 1, Player will play the subsequent run +,⟨i,0⟩ twice, breaking local injectivity. In fact, recomputing the interaction with two occurrences of done -,k one realizes that the two occurrences of run +,⟨i,0⟩ do exist, but they conflict with each other: this triggers new W 0,⟨0,k⟩ tt events, which would be sequentialized in some order by the memory. The R 0,2i+1 would happen at some point during that sequentialization; each of these possible occurrences of R 0,2i+1 would lead to a call to y -so there would be multiple non-deterministic calls to y. This illustrates that our symbolic representation of strategies is incomplete, and does not specify in general their behaviour if Opponent replicates their moves (though it is crucial in [START_REF] Castellan | The parallel intensionally fully abstract games model of PCF[END_REF] that this representation becomes complete for innocent strategies).

Secondly, we note that this term, in the Ghica-Murawski model of IPA [START_REF] Ghica | Angelic semantics of fine-grained concurrency[END_REF], would be interpreted by the same strategy than that for sequential composition. Unlike their model, we keep some information about non-deterministic branching; meaning that we do remember here that the term has a chance to diverge. In the interpretation presented in this paper, we do not remember all the information about divergences though. If one was to simplify the term above to newref r in λx com , y com . x; r ∶= tt ∥ if !r y , the branch where the read arrives too early w.r.t. the write would be hidden away by composition. The sole purpose of the superfluous read in our example above is to create a race in memory before x, spawning two non-deterministic copies of the execution of x. In one of them the computation is doomed, as the second thread is stuck in a loop.

Conclusions

In this paper, we have given the detailed development leading to our cartesian closed category Cho of Concurrent Hyland-Ong games, a setting that we illustrated with an interpretation of IPA. The cartesian closed category Cho conservatively extends standard Hyland-Ong games, in the sense that in our setting purely functional programs are interpreted as (copy-index aware versions of) their tree of P-views -but our setting also supports stateful, non-deterministic, or concurrent languages, or any combination thereof.

The cornerstone of our construction is a compact closed category Tcg of thin concurrent games, which extends Rideau and Winskel's category CG of games and strategies as event structures [START_REF] Rideau | Concurrent strategies[END_REF][START_REF] Castellan | Games and strategies as event structures[END_REF]. Note the interest of Tcg is not restricted to the construction of Cho. It supports games that are much more general than those obtained from arenas. The future will tell how this mathematical space is best exploited, but in subsequent work we have already sometimes found it more convenient to build directly on Tcg and on the AJM-style exponential ! AJM rather than on Cho.

Overall, we believe the framework is a very powerful setting for game semantics, whose ramifications will take some time to explore. Because it is conservative over traditional innocent game semantics but remembers the non-deterministic branching points, it natively supports a notion of non-deterministic innocence [START_REF] Castellan | Symmetry in concurrent games[END_REF][START_REF] Castellan | Concurrent structures in game semantics[END_REF] (achieving this in traditional game semantics has long remained an open problem, only solved recently via reworking Hyland-Ong games using ideas from sheaf theory to remember the non-deterministic branching points [START_REF] Tsukada | Nondeterminism in game semantics via sheaves[END_REF]). For the same reason, it has been possible to extend the present framework to give models of non-deterministic languages adequate for any of may, must and fair -equivalence, whereas traditional game semantics are mostly confined to angelic non-determinism. The framework extends, also transparently, with quantitative information: in [START_REF] Castellan | The concurrent game semantics of probabilistic PCF[END_REF][START_REF] Clairambault | Fully abstract models of the probabilistic lambdacalculus[END_REF] it has been extended with probabilities, along with a notion of probabilistic innocence permitting a definability result and a collapse to the probabilistic relational model -such results were not within reach using the traditional toolbox of game semantics. A number of further extensions are under active development.

Beyond theoretical results, it is our hope that the truly concurrent nature of this model will prove useful as a basis for algorithmic analysis and verification of concurrent programs. isomorphism family S may allow these two permutations to extend (in S) to permutations on the full set {⊖ 0 , ⊖ 1 , ⊕ 0 , ⊕ 1 }. By thinness, the identity bijection can only extend by the identity. However, the thin axiom does not restrict the possible extensions of π. This means that π can extend e.g. by (⊕ 0 , ⊕ 0 ) or by (⊕ 0 , ⊕ 1 ). In fact, there are exactly two isomorphism families S1 and S2 on S making σ a ∼-strategy, with maximal extension of π respectively given by π 1 (left), and π 2 (right):

⊖ 0 → ⊖ 1 ⊖ 0 → ⊖ 1 ⊖ 1 → ⊖ 0 ⊖ 1 → ⊖ 0 ⊕ 0 → ⊕ 1 ⊕ 0 → ⊕ 0 ⊕ 1 → ⊕ 0 ⊕ 1 → ⊕ 1 π 1 ∈ S1 π 2 ∈ S2 This yields two ∼-strategies σ 1 ∶ S 1 → A and σ 2 ∶ S 2 → A,
which differ only by how they react to Opponent permuting their copy indices: either by also permuting (σ 1 ) or by doing nothing (σ 2 ). The two resulting ∼-strategies are not weakly isomorphic or weakly equivalent because there are no maps between S 1 and S 2 .

A.1.3. Operational interpretation. Here we attempt to give an operational reading on the difference between σ 1 and σ 2 above, by recasting the phenomenon in IPA (this is best read after Section 5). In the interpretation of IPA, these subtle differences between uniformity witnesses can convey indirect information reminiscent from the difference between causality due to the program order, and that due to the dependencies in memory.

Consider the two terms M 1 , M 2 of type (com → com) → com → com:

M 1 = λf x. newref r in f (incr r; wait (!r = 2). x; ) M 2 = λf x. newref r in (f (incr r; )) ∥ (wait (!r = 2). (x ∥ x))
where incr r is a short-hand for r ∶=!r + 1 and wait b. M for Y (λl.if b M l). For both terms, the strategy includes the following pattern, where the variable f calls its argument twice:

(com → com) → (com → com) run - ✪ o o u ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡❡ ❡ run + ✐ ❣ ❡ ❞ ❜ ❛ ✮ q q x ✐ ✐ ✐ ✐ ✐ ✐ ✐ ✐ ✐ ✐ ✐ ❁ y y Ó ⑤ ⑤ ⑤ run - ✘ @ @ G ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ✚ A A H ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ♥ ❦ ✐ ❢ ❞ run - ✑ 6 6 D ◗ ◗ ◗ ◗ ◗ ◗ ✘ @ @ G ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ❳ ☞ ⑤ done + ✁ ⑦ ④ ② ✈ t r done + ✙ ✗ ✔ ✒ ✎ ☞ ✟
We omit copy indices to reduce clutter. As soon as f calls its argument twice, the two programs call x twice. The reader will recognize in the four lowest events the same pattern as in the previous example -and the isomorphism families for M 1 and M 2 restricted to this pattern indeed behave respectively like σ 1 and σ 2 .

It follows from the definition of the interpretation that this dynamics of an index exchange causing an index exchange occurs in the purely functional stage of the interpretation, as opposed to the accounting of state. As a consequence, the dynamics of indices exchange follows the causal links that originates from the program syntax tree, but ignores those that come from communication through the memory. Hence in M 1 the Opponent exchange causes a Player exchange because the occurrence of x appears within the argument of f in the syntax tree. In contrast, in M 2 the Opponent exchange causes no Player exchange as the dependency only flows through the memory.

A.2. Absence of pullbacks in E ∼ . The category of event structures with symmetry does not have pullbacks in general. For that we first note that if a diagram has a pullback in E ∼ , then, forgetting symmetry, it is also a pullback in E. The reason for that is the following proposition.

Proposition A.1. The forgetful functor E ∼ → E which to any event structure with symmetry A = (A, Ã) associates A, has a left adjoint.

Proof. The right adjoint associates, to any event structure A, the event structure with symmetry (A, refl A ), where

refl A = {{(a, a) a ∈ x} x ∈ C (A)}
is the minimal symmetry on A. It is straightforward that this defines an adjunction.

Hence the symmetry-forgetting functor is a right adjoint, and as such preserves pullbacks. Now, in order to prove that E ∼ does not have pullbacks, we are going to construct a diagram in E ∼ whose pullback in E has no possible isomorphism family. Indeed, consider A the following event structure:

⋅ a ❂ y y Ô ⑥ ⑥ ⑥ ⑥ ⑥ ⑥ ⑥ ✁ & & 7 ❆ ❆ ❆ ❆ ❆ ❆ ❆ ⋅ b ❃ y y Ô ⑦ ⑦ ⑦ ⑦ ⑦ ⑦ ⑦ & & 7 ❅ ❅ ❅ ❅ ❅ ❅ ❅ ⋅ 1 / o / o / o / o / o / o / o / o ⋅ 2 ⋅ 3 / o / o / o / o / o / o / o / o ⋅ 4
Write A for A equipped with the maximal isomorphism family: all order-isomorphisms are in the family. Write A 1 for the sub-event with symmetry where ⋅ 1 can only be sent to itself and to ⋅ 3 ; and ⋅ 2 can only be sent to itself and to ⋅ 4 . Similarly, write A 2 for that where ⋅ 1 can only be sent to ⋅ 4 and ⋅ 2 to ⋅ 3 . Now we have the following diagram:

A 1 id 2 2 ❆ ❆ ❆ ❆ ❆ ❆ ❆ ❆ A 2 id 6⑥ ⑥ ⑥ ⑥ ⑥ ⑥ ⑥ A Assume this diagram has a pullback (A 3 , Π 1 , Π 2 )
. By Proposition A.1 its underlying event structure is A and the projection maps are both identities on objects. The isomorphism {(⋅ a , ⋅ b )} ∶ {⋅ a } ≅ A 3 {⋅ b } must be in A 3 as it is in both A 1 and A 2 . However, its left hand side {⋅ a } can be extended with ⋅ 1 , so by the extension property we must have

{(⋅ a , ⋅ b ), (⋅ 1 , ⋅ i )} ∶ {⋅ a , ⋅ 1 } ≅ A 3 {⋅ b , ⋅ i } with i ∈ {3, 4}.
But by construction such an iso cannot be in both A 1 and A 2 , absurd.

A.3. Weak equivalence is not a congruence. This key observation is one of the key facts guiding the design of our games.

Let A, B and C be "games", i.e. essps in the context of this discussion. Consider σ 1 ∶ S 1 → A ⊥ ∥ B, σ 2 ∶ S 2 → A ⊥ ∥ B, and τ ∶ T → B ⊥ ∥ C be "strategies", i.e. maps of essps in the context of this discussion. Assume further than σ 1 and σ 2 are weakly equivalent, i.e. that there are f ∶ S 1 → S 2 and g ∶ S 2 → S 1 such that g ○ f ∼ id S 1 , f ○ g ∼ id S 2 , and the two obvious triangles commute up to symmetry. It first came as a surprise to us that then, τ ⊙ σ 1 and τ ⊙ σ 2 might not be weakly equivalent. Indeed, the extension property of isomorphism families ensures that two symmetric configurations have "bisimilar futures". So it is natural to expect τ ⊙ σ 1 and τ ⊙ σ 2 to behave similarly, and indeed they do, but in a way less strict than that expressed by weak equivalence.

To be more precise, first consider the essp P (the "pentagram"):

P = ⊕ 1 $ d $ d $ d $ d $ d $ d T T T T T T ⊕ 2 z : z : z : z : z : z : J J J J J J ⊕ 5 / o / o / o / o / o / o / o ⊕ 3 ⊕ 4
Its isomorphism family is the maximal one, i.e. all bijections between configurations are in the family. In P, two events will eventually be played. It does not matter which ones, since they are all symmetric -the only thing that matters is the multiplicity.

We consider P as a strategy on a game B with the same events as P ({⊕ 1 , ⊕ 2 , ⊕ 3 , ⊕ 4 , ⊕ 5 }), the maximal isomorphism family, and no conflict. We write α 1 for the obvious labeling

α 1 ∶ P → B ⊕ i ↦ ⊕ i
which indeed informs a strategy on B. We will also be interested in another strategy:

α 2 ∶ S → B
where S has events {⊕ 1 , ⊕ 2 } and again maximal isomorphism family. The map α 2 sends ⊕ i in S to ⊕ i in B. The strategies α 1 and α 2 behave similarly, since both will eventually play two events; and we do not care which ones since all possible choices are symmetric in the game. Despite that, α 1 and α 2 are not weakly equivalent. In fact, there is no map from α 1 to α 2 : such a map would require us to build a map of event structures from P to S, but the reader can check that this would induce a 2-coloring of P , which is not bipartite.

We will now obtain α 1 and α 2 respectively as compositions τ ⊙ σ 1 and τ ⊙ σ 2 , for weakly equivalent σ 1 and σ 2 . We introduce the game

A = ⊕ a / o / o / o ⊕ b
with again the maximal isomorphism family. The strategy τ ∶ T → A ⊥ ∥ B selects α 1 or α 2 depending on Opponent's choice in A. Its events are represented below.

⊖ a / o / o / o / o / o / o / o / o / o / o ❑ Ð Ð Ù ☛ ☛ ☛ ☛ s ! ! 0 ✸ ✸ ✸ ✸ ) ❵ ❴ ⊖ b ❑ Ð Ð Ù ☛ ☛ ☛ ☛ s ! ! 0 ✸ ✸ ✸ ✸ ⊕ 1 $ d $ d $ d $ d $ d $ d T T T T T T ⊕ 2 z : z : z : z : z : z : J J J J J J ⊕ 1 ⊕ 2 ⊕ 5 / o / o / o / o / o / o / o ⊕ 3 ⊕ 4
Its isomorphism family is, again, the maximal one: all order-isomorphisms between configurations are valid symmetries. One can check that this satisfies indeed the axioms for an isomorphism family; crucially the extension axiom uses the fact that P and S are bisimilar (and that the symmetry on B is the maximal one).

Finally, consider σ 1 , σ 2 on A, with σ 1 playing only ⊕ a and σ 2 playing only ⊕ b . They are clearly weakly equivalent, since {(⊕ a , ⊕ b )} is in Ã. But by construction we have τ ⊙ σ 1 ≅ α 1 and τ ⊙ σ 2 ≅ α 2 , which as we observed are not weakly equivalent.

Note that the games A and B are both tcgs; but crucially τ is not thin (Definition 3.14). Indeed, for instance, the symmetry {(⊖ a , ⊖ b )} extends to both {(⊖ a , ⊖ b ), (⊕ 1 , ⊕ 1 )} and {(⊖ a , ⊖ b ), (⊕ 1 , ⊕ 2 )}, which is forbidden by Definition 3.14. For thin strategies, positive extensions of the symmetry must be canonically chosen, making it impossible that composite strategies as above are bisimilar but not weakly equivalent.

A.4. Failure of extension for copycat on general games. In the main text, we give (Definition 3.37) a candidate C C Ã for the isomorphism family on copycat for any essp A. The valid symmetries on C C A are simply those order-isomorphisms between configurations of C C A which map to valid symmetries on A ⊥ ∥ A.

We prove in Proposition 3.39 that this satisfies the extension property of isomorphism families if the game is a tcg. This boiled down to Lemma B.3, which shows that tcgs are race-preserving : races in the isomorphism family always originate to races in the game. As this phenomenon played an important role in the design of the theory, we find it useful to include here an example demonstrating the fact that without this race-preservation property (so if the games are plain event structures with polarities and symmetry, rather than tcgs), the extension property fails in general for the isomorphism family on copycat.

Consider an essp A = {a -, b + }. We form ! 2 A with events/causality/polarities/conflict those of A ∥ A (we write a -,i for (i, a) -), and isomorphism families the set of bijections between configurations included in the two maximal ones: {(a -,1 , a -,1 ), (b +,1 , b +,1 ), (a -,2 , a -,2 ), (b +,2 , b +,2 )} {(a -,1 , a -,2 ), (b +,1 , b +,2 ), (a -,2 , a -,1 ), (b +,2 , b +,1 )} So maximal symmetries either globally preserve the copy indices, or globally swap them. It is not possible for a symmetry to, e.g. send a -,1 to a -,1 and b +,1 to b +,2 . It is, in fact, a binary version of the ! AJM operation of Definition 3.4, applied to A.

From Definition 3.37, C C ! 2 A is equipped with a candidate isomorphism family C C ! 2 A . We now show that this however fails the (Extension) axiom of isomorphism families. From the definition, the diagram below represents a valid symmetry in C C ! 2 A .

! 2 A ⊥ ∥ ! 2 A ≅ C C ! 2 A ! 2 A ⊥ ∥ ! 2 A b -,1
a -,1 b -,1 a -,2 The issue will come from the fact that the symmetry follows irreconciliable courses in the left and the right components of C C ! 2 : in the left component it preserves copy indices, whereas in the right component it swaps them. So it the left hand side of this symmetry extends as depicted below

! 2 A ⊥ ∥ ! 2 A ≅ C C ! 2 A ! 2 A ⊥ ∥ ! 2 A b -,1 a -,1
b -,1 a -,2 b +,1 the only matching extension on the right hand side is with b +,1 as well (b +,2 is not possible as it would require to play b -,2 first), but (b +,1 , b +,1 ) is not a valid extension of the symmetry above, as for that it would need to swap the copy index instead of preserving it. (Extension). Let θ ∶ w ≅ S∧ T z. Assume w can be extended by an event e ∈ S ∧ T to w ′ . Write s = Π 1 e and t = Π 2 e, and assume e.g. σs is positive in A. We then have:

Π 1 w ′ ≃ (σ ∧ τ ) w ′ ≃ Π 2 w ′ Π 1 w s R 2 ❍ ❍ ❍ ❍ ❍ ❍ θ S ≅ S ≃ σ (σ ∧ τ ) w ≃ τ Π 2 w θ T ≅ T t , ✈ ✈ ✈ ✈ ✈ ✈ Π 1 z ≃ σ (σ ∧ τ ) z ≃ τ Π 2 z
We first use the extension property on θ S as Π 1 w s -⊂ : θ S extends by (s, s ′ ). Since σθ S = τ θ T , this means that τ θ T extends by (σs, σs ′ ) which is negative in A ⊥ . By ∼receptivity of τ , θ T extends by (t, t ′ ) with τ t = σs and τ t ′ = σs ′ . The picture is now:

Π 1 w ′ ≅ S ≃ (σ ∧ τ ) w ′ ≃ Π 2 w ′ ≅ T Π 1 w s R 2 ❍ ❍ ❍ ❍ ❍ ❍ θ S ≅ S ≃ σ (σ ∧ τ ) w ≃ τ Π 2 w θ T ≅ T t , ✈ ✈ ✈ ✈ ✈ ✈ Π 1 z s ′ l L t t t ≃ σ (σ ∧ τ ) z ≃ τ Π 2 z t ′ r ❏ ❏ ❏ z 1 ≃ σz 1 = τ z 2 ≃ z 2
The obtained ϕ ∶ z 1 ≃ z 2 is secured by construction, so as observed in Definition 2.11 its graph is ordered by ≤ ϕ compatible with ≤ S and ≤ T . Therefore restricting ϕ to the causal history of (s ′ , t ′ ) yields e ′ = [(s ′ , t ′ )] ϕ a prime secured bijection, i.e. an event e ′ ∈ S ∧ T such that z e ′ -⊂ z ′ . Finally, θ ∪ {(e, e ′ )} ∈ S ∧ T because θ S ∪ {(s, s ′ )} ∈ S and θ T ∪ {(t, t ′ )} ∈ T . If σs is negative, the dual reasoning uses extension on T and then ∼-receptivity of σ. It is a pullback. Clearly the maps Π 1 ∶ S ∧T → S and Π 2 ∶ S ∧T → T preserve symmetry: they map θ to θ S and θ T respectively. We only need to check the universal property. Assume we have two morphisms of ess ϕ ∶ X → S and ψ ∶ X → T such that the square commutes:

X ϕ Ù Ù ψ S ∧ T | | ① ① ① ① ① ① ① 5 5 ❋ ❋ ❋ ❋ ❋ ❋ ❋ S σ 5 5 ❋ ❋ ❋ ❋ ❋ ❋ ❋ T τ { { ① ① ① ① ① ① ① A
Because S ∧ T is a pullback in E there is a map of event structures ⟨ϕ, ψ⟩ ∶ X → S ∧ T making the two triangles commute, which is unique in E. This uniqueness lifts to E ∼ as the forgetful functor E ∼ → E is faithful. To conclude we need only to prove that ⟨ϕ, ψ⟩ preserves symmetry and is thus a morphism in E ∼ . Let θ ∶ x ≅ X y. It is transported to a bijection ⟨ϕ, ψ⟩ θ ∶ ⟨ϕ, ψ⟩ x ≃ ⟨ϕ, ψ⟩ y such that (⟨ϕ, ψ⟩ θ) S = ϕ θ and (⟨ϕ, ψ⟩ θ) T = ψ θ, thus ⟨ϕ, ψ⟩ θ ∈ S ∧ T by definition.

B.2. Composition of ∼-receptivity and componentwise courtesy. To prove that, we first introduce the following more local characterisation for ∼-receptivity.

Lemma B.1. Let A be a tcg and σ ∶ S → A be a map of ess. Then, σ is ∼-receptive iff for all x ∈ C (S) and x s - 1 -⊂ , for all id σ x ∪ {(σ s 1 , a 2 )} ∈ Ã, there exists a unique s 2 such that σ s 2 = a 2 , and we have id x ∪ {(s 1 , s 2 )} ∈ S. -⊂ . Since σ is a map of ess, we must have σ θ ∪ {(σ s 1 , σ s ′ 1 )} ∈ Ã as well. By (Groupoid), it follows that id σx 2 ∪ {(σ s ′ 1 , a 2 )} ∈ Ã. By hypothesis, we get a unique s 2 such that σ s 2 = a 2 , satisfying id x 2 ∪ {(s ′ 1 , s 2 )} ∈ S. And finally, by (Groupoid) again, θ ∪ {(s 1 , s 2 )} ∈ S.

Using that, we prove: Lemma 3.36. Let σ ∶ S → A ⊥ ∥ B and τ ∶ T → B ⊥ ∥ C be pre-∼-strategies, such that σ is (A, B)-courteous and τ is (B, C)-courteous. Then, τ ⊙σ is ∼-receptive and (A, C)-courteous.

Proof. As a preliminary to the proof, we note that thanks to (A, B)-courtesy of σ and (B, C)-courtesy of τ , the immediate dependencies of negative p ∈ T ⊙ S in T ⊛ S have to be visible as well, and must map to the same component -this is the key argument of the proof. Indeed assume p ′ p in T ⊛ S with visible p mapping to a negative event in A ⊥ ∥ C, for instance in C. Then by general properties of the pullback in E, since p maps to C, its immediate causal dependencies p ′ p in T ⊛ S must be such that Π 2 p ′ Π 2 p in A ∥ T (consequence of e.g. Lemma 2.7 of [START_REF] Castellan | Games and strategies as event structures[END_REF] with Proposition 2.16), but since p maps to C those must actually both be in T , and since τ is (B, C)-courteous p ′ must map to C as well, therefore it is visible.

From that, it is clear that τ ⊙σ is (A, C)-courteous. We now show that it is ∼-receptive. We prove it via Lemma B.1. Take z ∈ C (T ⊙ S), assume z extends via some negative p, say in C. The configuration z has a witness [z] ∈ C (T ⊛ S), however in general this witness might not extend with p, as it may need to perform some invisible events prior to that. In our case though, the preliminary above shows that this is not possible: the immediate dependencies in T ⊛ S of p are visible as well, and hence in z ⊆ [z]. Now, if we also have that (τ ⊙ σ) z extends with c -with id (τ ⊙σ) z ∪ {((τ ⊙ σ) p, c)} ∈ Ã ∥ B ∥ C, then

Π 2 [z] Π 2 p -⊂ id Π 2 [z] ∪ {((A ∥ τ ) (Π 2 p), c)} ∈ Ã ∥ B ∥ C
so using ∼-receptivity of A ∥ τ , we can uniquely lift c to A ∥ T , hence to T ⊛ S and T ⊙ S, and that lifting is by construction compatible with T ⊛ S and T ⊙ S.

B.3. Proofs for the copycat ∼-strategy. This section contains proofs relative to the construction of the isomorphism family for the copycat strategy. We start with a simple caracterisation of the valid symmetries announced in the main text.

Proposition 3.38. The set C C Ã is equivalently defined as comprising the bijections

θ 1 ∥ θ 2 ∶ x 1 ∥ x 2 ≃ Ã⊥ ∥ Ã y 1 ∥ y 2
satisfying the further condition that for all a ∈ x 1 ∩ x 2 , we have θ 1 (a) = θ 2 (a).

Proof. Take θ = θ 1 ∥ θ 2 ∶ x 1 ∥ x 2 ≅ y 1 ∥ y 2 . If θ is an order-iso, then take a ∈ x 1 ∩ x 2 . Assume without loss of generality that pol A (a) = +, so that (1, a)

(2, a) in C C A . But then since θ is an order-iso, it preserves immediate causal dependency, therefore (1, θ 1 a) (2, θ 2 a). But since these two events are in different components of A ⊥ ∥ A, this necessarily means that θ 1 a = θ 2 a as required (using e.g. the characterisation of immediate causality of copycat in Lemma 3.3 of [START_REF] Castellan | Games and strategies as event structures[END_REF]).

Lemma 3.29. Let σ ∶ S → A and σ ′ ∶ S ′ → A be pre-∼-strategies, and f ∶ S → S ′ such that σ ′ ○ f ∼ Ã σ. Then, there exists a unique f ′ ∶ S → S ′ such that f ∼ S′ f ′ , and σ ′ ○ f ′ ∼ Ã+ f .

Proof. We show that for all x ∈ C (S), there is a unique ϕ x ∶ f x ≅ S′ x ′ such that σx ≅ Ã+ σ ′ x ′ .

Uniqueness is again a consequence of Lemma 3.28.

Existence. If x ∈ C (S), then by hypothesis we know that the triangle induces

θ x ∶ σ ′ (f x) ≅ Ã σx
By Lemma 3.19, θ x decomposes as σ ′ (f x)

θ - x ≅ Ã-y θ +
x ≅ Ã+ σx. By Lemma B.4, there is

ϕ x ∶ f x ≅ S′ x ′ such that σϕ = θ ′ x + ○ θ -
x . We then have θ ′

x + θ x -1 ∶ σx ≅ Ã+ σ ′ x as required. It is routine to show that the assignment from x to x ′ is monotonic, preserves cardinality and unions, hence it is generated by a map of event structures f ′ ∶ S → S ′ , which by construction preserves symmetry. By construction, f ′ satisfies the desired properties. The uniqueness of f ′ follows directly from Lemma 3.28. B.5. Preservation of single-threadedness. Proposition 4.10. Let σ ∶ S → A ⊥ ∥ B and τ ∶ T → B ⊥ ∥ C be negative single-threaded prestrategies. Then, τ ⊙ σ is single-threaded.

We first prove that the interaction T ⊛ S satisfies the single-threadedness conditions. More precisely, we prove by induction on ϕ that for any secured bijection ϕ ∶ x S ∥ x C ≃ y A ∥ y T representing (via Proposition 2.16) a configuration of T ⊛ S, then

ϕ = ⊎ 1≤i≤n ϕ i
where each ϕ i is a secured bijection with a unique minimal event. Indeed, assume ϕ where ϕ ′ fails this condition. Necessarily, either c = (1, s + ) or d = (2, t + ), w.l.o.g. assume the first. Then, the immediate predecessors of (c, d) in ≤ ϕ ′ must be ((1, s - 1 ), d 1 ), . . . , ((1, s - p ), d p ) (using Lemma 2.7 of [CCRW17]), with s i S s. By hypothesis, there are 1 ≤ i, j ≤ p and distinct 1 ≤ k ≠ l ≤ n such that ((1, s - i ), d i ) ∈ ϕ k and ((1, s - j ), d j ) ∈ ϕ l . But ϕ k (resp. ϕ l ) must contain an event synchronized with init(s i ) (resp. init(s j )). Since σ is single-threaded and s i , s j ∈ [s] we have init(s i ) = init(s j ), which contradicts ϕ l ∩ ϕ k = ∅. Now, we go on to prove single-threadedness.

(1) Prime secured bijections have no non-trivial decomposition as above, therefore they have a unique minimal event. This is true in particular for the visible prime secured bijections. Condition (1) of single-threadedness follows then from the fact used in the proof of Lemma 4.3 that a minimal event in the interaction of negative strategies is always visible.

(2) Finally, assume there is a minimal conflict ϕ / o / o ψ in T ⊙ S between visible prime secured bijections. This means that there are non-necessarily visible prime secured bijections ϕ ′ ⊆ [ϕ] T ⊛S , ψ ′ ⊆ [ψ] T ⊛S , such that ϕ ′ / o / o ψ ′ in T ⊛ S. Writing ϕ ′′ (resp. ψ ′′ ) for ϕ ′ (resp. ψ ′ ) without its top event, minimality of ϕ ′ / o / o ψ ′ means that ϕ ′′ ∪ ψ ′′ is a valid secured bijection. Therefore, it decomposes:

ϕ ′′ ∪ ψ ′′ = ⊎ 1≤i≤n ϕ i
With each ϕ i a secured bijection having exactly one minimal event. If n = 1, we are done since as remarked the unique minimal event is necessarily visible. Otherwise, there are at least two ϕ i , ϕ j with distinct minimal events.

Then ). But by single-threadedness of σ, init(s ϕ ′ ) = init(s ψ ′ ), so there should be an event synchronized with init(s 1 ) = init(s 2 ) both in ϕ i and ϕ j , absurd.

  the obvious way; as usual we also write f ∥ F for f ∥ id F . If A and B have polarities, so is A ∥ B, with pol A∥B ((1, a)) = pol A (a) and pol A∥B ((2, b)) = pol B (b).

Figure 6 .

 6 Figure 6. Saturated interpretation of the strategies of Example 2.26

Figure 11 .

 11 Figure 11. Two concurrent innocent strategies Using this strategy we can define Γ ⊢ M ∥ N ∶ com = ∥ ⊙ ⟨ M , N ⟩.This strategy is no longer a forest, but rather a directed acyclic graph. We also note that this is a deterministic strategy: there is no conflict in its event structure. As we shall see later, without any non-deterministic primitive, it is only in the presence of shared state that non-deterministic strategies will arise. In fact, a major advantage of our approach to modeling concurrent languages is that, not being based on interleavings, we represent the execution of such non-interfering terms deterministically.In[START_REF] Castellan | The parallel intensionally fully abstract games model of PCF[END_REF], we exploit this property: we give a concurrent notion of innocence where strategies are directed acyclic graphs rather than forests, and using this notion we give an intensionally fully abstract model of a variant of PCF where independent computations are performed in parallel. The detailed construction is out of the scope of this particular paper, but let us illustrate it with two examples that are both concurrent innocent.Figure11displays two concurrent innocent strategies (we associate moves to the corresponding sub-type using indices rather than location). In Figure11a, we have a strategy for a parallel implementation of the left or, that is strict in its left argument. Indeed, although the strategy starts evaluating both its arguments in parallel, it can only return at toplevel if its first argument has returned. However, this is not true anymore for the strategy of Figure11b. There, it suffices that one argument returns tt for the overall computation to return tt -indeed, this strategy computes the well-known parallel-or function[START_REF] Plotkin | LCF considered as a programming language[END_REF].

  cell ∶ Cell → ! ref Example 5.1. The following diagram represents a sub-event structure of Cell. 2 r 1 q 0 p 0 p / o . n . n -m , l + k + k ❴ R -,4

Appendix B .

 . Postponed proofs B.1. Pullbacks of dual ∼-receptive maps.Lemma 3.12. Let σ ∶ S → A and τ ∶ T → A ⊥ be ∼-receptive maps of ess. The set S ∧ T is an isomorphism family on S ∧ T and the ess (S ∧ T, S ∧ T ) is a pullback in E ∼ of σ and τ , written S ∧ T .Proof. The (Groupoid) and (Restriction) axioms are direct consequences of the corresponding conditions for S and T .

  Proof. only if. Particular case of the definition of ∼-receptivity.

1 -⊂ and σ x 2 a - 2 -

 12 if. Assume θ ∶ x 1 ≅ S x 2 , x 1 s - ⊂ such that σ θ ∪ {(σ s 1 , a 2 )} ∈ Ã. By (Extension), there is s ′ 1 such that θ (s 1 ,s ′ 1 )

1

  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 Empty game/arena. E ↓ V . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 Projection of an event structure (hiding). τ ⊙ σ ∶ T ⊙ S → A ⊥ ∥ C . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 Composition of σ ∶ S → A ⊥ ∥ B and τ ∶ T → B ⊥ ∥ C. lbl α . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 Label of an indexing function α. ind α . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 Copy index of an indexing function α. !A . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 Expanded arena. just(α) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 Justifier (unique immediate dependency) of α in !A. ⟨ 1 , . . . , n ⟩ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 Any injective function ω n → ω. x ≅ y . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 Order-isomorphism between (possibly implicitly) ordered sets. σ ≈ τ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 Weak isomorphism. A . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 Event structure with symmetry A = (A, Ã). Ã . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 Isomorphism family of an ess A. θ ↾ x . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 Restriction of θ ∶ x ′ ≅ y ′ ∈ Ã to subconfiguration x ⊆ x ′ . θ ∶ x ≅ y . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 Order-preserving bijection between x and y. θ ∶ x ≅ Ã y . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 θ ∶ x ≅ y ∈ Ã. dom θ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 Domain of θ. codom θ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 Codomain of θ. ! A -. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 Set of negative reindexing isos on !A. ! A + . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 Set of positive reindexing isos on !A. θ 1 ∥ θ 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 Parallel composition θ 1 ∥ θ 2 ∶ x ∥ y ≃ x ′ ∥ y ′ of bijections θ 1 ∶ x ≃ x ′ and θ 2 ∶ y ≃ y ′ . f θ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 Forward image f θ = {(f a 1 , f a 2 ) (a 1 , a 2 ) ∈ θ} of a bijection. E ∼ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 Category of event structures with symmetry and morphisms preserving symmetry. f ∼ B g . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 Maps f, g ∶ A → B in E ∼ are symmetric.

  Lemma 2.15. Let σ ∶ S → A and τ ∶ T → A ⊥ be prestrategies, and ϕ ∈ B sec σ,τ . Then if ϕ ∶ x ≃ y extends in B sec σ,τ with (s 1 , t 1 ) and (s2 , t 2 ) but ϕ ∪ {(s 1 , t 1 ), (s 2 , t 2 )} ∈ B sec σ,τ . Then, either x ∪ {s 1 , s 2 } ∈ C (S) or y ∪ {t 1 , t 2 } ∈ C (T ). If x∪{s 1 , s 2 } ∈ C (S), y ∪{t 1 , t 2 } ∈ C (T ),and s 1 , s 2 and t 1 , t 2 are distinct, then clearly ϕ∪{(s 1 , t 1 ), (s 2 , t 2 )} ∈ B sec σ,τ . However if e.g. s 1 = s 2 , then τ t 1 = τ t 2 , hence y∪{t 1 , t 2 } ∈ C (T ) by local injectivity -and similarly if t 1 = t 2 .

	/ o In particular, if S, T have binary conflict and ϕ, ψ are events in S ∧T such that ϕ / o then s ϕ / o / o s ψ or t ϕ / o / o t ψ .	ψ,
	Proof.

  , using Lemma 2.15, ϕ ′ / o / o ψ ′ implies that their top elements have the form((1, s ϕ ′ ), d ϕ ′ ) and ((1, s ψ ′ ), d ψ ′ ) with s ϕ ′ / o / o S s ψ ′ , or (c ϕ ′ , (2, t ϕ ′ )) and (c ψ ′ , (2, t ψ ′ )) with t ϕ ′ / o/ o T t ψ ′ , w.l.o.g. say the first. By receptivity and courtesy of σ, we have pol(s ϕ ′ ) = pol(s ψ ′ ) = +. Since n ≥ 2, there are (c 1 , d 1 ) ϕ ((1, s + ϕ ′ ), d ϕ ′ ) with (c 1 , d 1 ) ∈ ϕ i and (c 2 , d 2 ) ψ ((1, s + ψ ′ ), d ψ ′ ) with (c 2 , d 2 ) ∈ ϕ j .By Lemma 2.7 of [CCRW17], as an immediate dependency of ((1, s + ϕ ′ ), d ϕ ′ ), we have (c 1 , d 1 ) = ((1, s - 1 ), d 1 ) with s 1 S s ϕ ′ (similarly, (c 2 , d 2 ) = ((1, s - 2 ), d 2 ) with s 2 S s ψ ′

SIMON CASTELLAN, PIERRE CLAIRAMBAULT, AND GLYNN WINSKELΓ ⊢ M ∶ com Γ ⊢ N ∶ com Γ ⊢ M ∥ N ∶ com Γ ⊢ M ∶ com Γ ⊢ N ∶ X Γ ⊢ M ; N ∶ X Γ ⊢ M ∶ ref Γ ⊢ N ∶ N Γ ⊢ M ∶= N ∶ com Γ, x ∶ ref ⊢ M ∶ X Γ ⊢ newref x in M ∶ X Γ ⊢ M ∶ B Γ ⊢ N i ∶ X Γ ⊢ if M N 1 N 2 ∶ X Γ ⊢ M ∶ N → com Γ ⊢ N ∶ N Γ ⊢ mkvar M N ∶ ref

In fact the counter-example of Appendix A.3 can be adapted to show that without further hypothesis on games, congruence fails even for thin strategies.

This formulation was a later improvement on the original definition of[START_REF] Castellan | The parallel intensionally fully abstract games model of PCF[END_REF].

Acknowledgments. This work was partially supported by the LABEX MILYON (ANR-10-LABX-0070), and by the ERC Advanced Grant ECSYM.

Appendix A. Examples and counter-examples

A.1. Necessity for uniformity witnesses. In this first appendix, we give a few examples illustrating why uniformity is achieved by having strategies carry uniformity witnesses, rather than simply as a lifting property with respect to the symmetry in the game.

A.1.1. Necessity of witness. Our first example illustrates that simply requiring strategies on expanded arenas to satisfy a lifting property with respect to the reindexing isos in the game (as in AJM games) is unsound: it is too strict, and rejects some valid uniform strategies. In particular, it becomes required when one wishes to express uniformity for strategies with a non-deterministic branching behaviour. For instance, consider the following strategy.

where subscripts are there just to distinguish occurrences of moves in the discussion.

The strategy throws a non-deterministic coin. If it gets heads it calls its argument, then diverges. On the other hand if it gets tails it calls for its argument, then returns. This behaviour is easily definable in IPA, however a naive attempt at defining uniformity rejects it. Indeed, the two configurations {run -,0 3 , run +,0 1 , done -,0 1 } and {run -,0 3 , run +,0 2 , done -,0 2 } have the same image in the game, so in particular they coincide up to reindexing iso. However, the latter can be extended with {done +,0 3 } whereas the former cannot. This is because while the two events run +,0 1 and run +,0 2 have the same image in the game (and hence are symmetric), they correspond to entirely distinct events in the dynamic behaviour of the program and should not be considered symmetric by the strategy. Hence we need to equip strategies with uniformity witnesses that record which events are symmetric.

A.1.2. Non-uniqueness of witness. If a uniformity witness is needed, one may still hope to prove that it can be recovered in a unique or canonical way, so that being uniform can still be considered as a property rather than a piece of structure. Our next example shows that it is not the case: uniform strategies can very well differ only via their uniformity witnesses (this is best read after Section 3).

Consider the tcg A with events {⊖ 0 , ⊖ 1 , ⊕ 0 , ⊕ 1 }, all compatible, with trivial causality and symmetry consisting in all polarity-preserving bijections. Now consider the strategy (without symmetry) σ ∶ S → A described as follows:

By strong receptivity, any isomorphism family S on S making σ a ∼-strategy must contain the two permutations id and π of the set {⊖ 0 , ⊖ 1 }. We now consider how a valid Reciprocally, assume that for all a ∈ x 1 ∩ x 2 , θ 1 a = θ 2 a. Using again Lemma 3.3 of [START_REF] Castellan | Games and strategies as event structures[END_REF], it is immediate that θ preserves immediate causal links. The same reasoning applies to θ -1 (it is easy to show that the hypothesis is stable under inverse), so it reflects immediate causal links as well; and is an order-iso.

We now set to prove Proposition 3.39. Most verifications are direct; the main issue being to show that C C Ã always satisfies the axioms of isomorphism families. The first two axioms are immediate consequences of the definition of C C Ã in Definition 3.37: Lemma B.2. For any tcg A, the family C C Ã satisfies the axioms (Groupoid) and (Restriction) of isomorphism families.

The main difficulty is to show the (Extension) axiom. And for good reasons: indeed, this axiom fails if A is an essp with no further constraints (as illustrated in Appendix A.4). That it holds when A is a tcg boils down to the property below.

Lemma B.3. Let A be a tcg. Then à is race-preserving, in the sense that for any θ ∶ x ≅ à y, for any θ ⊆ + θ 1 ∶ x 1 ≅ à y 1 and θ ⊆ -θ 2 ∶ x 2 ≅ à y 2 , if x 1 and x 2 are compatible (x 1 ∪x 2 ∈ C (A)), then so are θ 1 and θ 2 : θ 1 ∪ θ 2 ∈ à as well.

Proof. We first prove that Ã+ and Ãare race-preserving. Let θ ∶ x ≅ Ã+ y with a positive extension θ 1 ∶ x 1 ≅ Ã+ y 1 and a negative extension

Using (Extension) of Ã+ twice to θ 1 and θ 2 , we get to the following picture:

By the (Groupoid) axiom on Ã+ , we have id

A dual reasoning shows that Ãis race-preserving as well. Now, we deduce the result for Ã, using the decomposition of Lemma 3.19. Assume

By monotonicity of the decomposition, we have θ

That à is race-preserving is actually a sufficient condition for the (Extension) axiom to hold on C C Ã. With this we can finally complete the proof.

Proposition 3.39. Let A be a tcg. Then, writing

-⊂ . There are two cases:

and by construction its domain is y ∪ {a}. To sum up, we have:

We need to check that this is a valid extension in C C Ã as well. By the characterisation of Proposition 3.38, we only have to check that id x c = (id y ∪{(a, b)}) c for each c ∈ x∩(y ∪{a}), but in fact we must have c ∈ x ∩ y. Indeed, we cannot have a ∈ x, as by x ⊇ + x ∩ y ⊆ -y and pol A (a) =that would imply a ∈ y as well, absurd. So the verification is obvious.

Finally, that copycat is thin is an immediate consequence of A -and A ⊥ + being thin along with the characterisation of symmetries in copycat of Proposition 3.38. B.4. Positivisation of mediating maps. We start with the following lemma, which intuitively allows us to canonically "transport" a configuration along a negative symmetry.

Then, there is a unique

Proof. Uniqueness. If there are two such

2 such that σψ ∈ Ã+ ; by Lemma 3.28 it follows that ψ is an identity and x ′ 1 = x ′ 2 , ϕ 1 = ϕ 2 . Existence. Direct by induction of x and θ -. For negative extensions, it follows from the (Extension) property for Ã+ and ∼-receptivity of σ. For positive extensions, it follows from the (Extension) axiom for S and axiom (d) of tcgs on A.

Index of notions