# The Qualitative Collapse of Concurrent Games

Pierre Clairambault

► To cite this version:

Pierre Clairambault. The Qualitative Collapse of Concurrent Games. 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2025), Jun 2025, Singapour, Singapore. pp.513-526, 10.1109/LICS65433.2025.00045. hal-05383155

HAL Id: hal-05383155

https://hal.science/hal-05383155v1

Submitted on 26 Nov 2025

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

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

<figure><img src="image_1.png" /></figure>
# The Qualitative Collapse of Concurrent Games

Pierre Clairambault

CNRS, Aix Marseille Univ, LIS

Marseille, France

Pierre.Clairambault@cnrs.fr

***Abstract***—We construct an interpretation-preserving functor from a category of concurrent games to the category of Scott domains and Scott-continuous functions. We give a concrete description of this functor, extending earlier results on the *relational* collapse of game semantics. The crux is an intricate combinatorial lemma allowing us to synchronize states of strategies which involve the same resources, but with different multiplicity.

Putting this together with the previously established relational collapse, this provides a new proof of the *qualitative-quantitative* correspondence first established by Ehrhard in his celebrated *extensional collapse theorem*. Whereas Ehrhard's proof is indirect and rests on an abstract realizability construction, our result gives a concrete, combinatorial description of the extraction of quantitative information from a qualitative model.

# I. INTRODUCTION

## A. General Introduction

The heart of denotational semantics is certainly *domain theory*, where types are interpreted as partially ordered sets, and programs as (continuous) functions between those. This idea, originally pioneered by Scott and Strachey [SS71], has spread wide and far, and underlies much of the modern theory of programming languages. In the terminology of this paper, this functional semantics is *qualitative*: it tracks the amount of information about the input needed to compute a given part of the output, but not *how many times* that information is needed, or how many times the argument of a function is evaluated.

Another deeply influential discovery, in that field of research, is Girard's invention of *linear logic* [Gir87]. Linear logic is a logic of resources; it gives a special status to those functions that are *linear* in the sense that they evaluate their argument *exactly once*. Starting with the interpretation of λ-terms as normal functors [Gir88], linear logic prompted the development of denotational models that are sensitive to resources, in the sense that they also record the multiplicity of resource usage: in the terminology of this paper, they are *quantitative*. Quantitative models have been under active development in the following three decades, with a number of remarkable achievements. For instance, quantitative models (and their type-theoretic presentations as *non-idempotent intersection types*) provide a semantic characterization of execution time [dC18]. Their resource-sensitivity lets them track numerous quantitative aspects of computation [LMMP13], or provide

models of properly quantitative computational effects, such as probabilistic choice [EPT18] or quantum effects [PSV14], for which they give fully abstract models [EPT18], [CdV20].

The drawback of this quantitative aspect, however, is that they are infinitary. Even for the simply-typed λ-calculus with a finite interpretation for ground types, they give infinitary semantics, because they rely on finite multisets to represent the arrow type. A "proof" that a certain point is in the quantitative semantics of a term (which can often be represented as a derivation in a non-idempotent intersection type system), is really a de-temporised, "static" representation of the full execution. In contrast, the functional models as in domain theory, and their syntactic presentations as idempotent intersection type systems, remain finitary: for instance, they give a finite interpretation to simply-typed programs with finite ground types. They talk by bounded means of an unbounded object: the execution – this is the key to their algorithmic use in e.g. higher-order model-checking [Aeh06], [KO09].

There is a fascinating scientific tension between these *qualitative* and *quantitative* models. On the one hand, they are remarkably similar: with the right presentation, the only significant difference in their construction is whether the exponential modality should be based on finite sets or finite multisets. On the other hand, the associated proof methods are very different: quantitative models are infinitary, but their connection with the execution is simple logically (though it can still be subtle combinatorially), allowing them to provide useful program approximants [BM20]; qualitative models are finitary, but linking them with execution requires tools with considerable logical complexity, such as logical relations. Surprisingly, this tension has been somewhat little studied, perhaps also because the two families of models correspond to different communities. However, there is one important paper that strikes right at that tension: Ehrhard's result that the linear Scott model of the simply-typed λ-calculus is the *extensional collapse* of its relational model [Ehr12]. Ehrhard's proof entails, in particular, that a point *a* in the qualitative model is in the semantics of a program *M* iff it has a "quantitativation" *a*′ in the *quantitative* semantics of *M*. At the core of this result is the construction of a model that is somewhat hybrid between qualitative and quantitative; of quantitative relations which behave well with respect to a preorder relation rearranging resources. But this hybrid model is obtained by formulating and maintaining an invariant (by *biorthogonality*) implying this quantitativation, it gives us no combinatorial understanding of that process, and no way to

<footnote>This work was supported by the ANR project DyVerSe (ANR-19-CE48-0010-01); by the Labex MiLyon (ANR-10-LABX-0070) of Université de Lyon, within the program "Investissements d'Avenir" (ANR-11-IDEX-0007), operated by the French National Research Agency (ANR); and by the PEPR integrated project EPiQ ANR-22-PETQ-0007 part of Plan France 2030.</footnote>
compute it in concrete cases.

Here, we provide a combinatorial understanding of this quantitativation process, using *game semantics*. Game semantics is another quantitative denotational model, originally developed to attack the famous full abstraction problem for PCF [AJM00], [HO00]. Game semantics enriches the relational model with *time* or *causality*, presenting interactive executions of a program with its runtime environment as *plays* on a game whose rules are determined by the type. Despite its clear intellectual affiliation with quantitative semantics, understanding the precise relationship between games and relational models has required a longstanding line of research [BDER97], [Ehr96], [Mel06], [Mel05], [Bou09]. In the modern dress of *thin concurrent games* [CCW19], [Cla24a], building on *concurrent games on event structures* [RW11] and in the footsteps of Melliès's insightful work on *asynchronous games* [Mel05], this relationship now appears as a simple forgetful interpretation-preserving functor to the relational model, erasing the "dynamic" causal dependency coming from the program, keeping only the "static" causal dependency from the type – this is summed up in [Cla24a], see also [CCPW18], [CdV20], [COP23] for quantitative or bicategorical extensions.

In this paper, we complement this “relational collapse” with a related interpretation-preserving functor to the *linear Scott model*, a linear decomposition of a (full subcategory of) Scott domains due independently to Huth [Hut93] and Winskel [Win98]. To construct a Scott domain from a game, we equip the latter with adequate notions of morphisms, *cartesian morphisms*, which allow the rearrangement (contraction and weakening) of resources. The crux of the issue is then to show that this collapse operation to the linear Scott model preserves composition: this rests on a crucial proposition (Proposition 5) showing that if innocent strategies can synchronize up to cartesian morphisms, then one can find adequate expansions of the states making them synchronize on the nose. This forms the core of our combinatorial account of Ehrhard's quantitativation result: because our games model has interpretation-preserving functors to both the relational model and the Scott model, we also reprove the precise connection between the two (Theorem 8). This is also a contribution to the line of work connecting game semantics to “static” semantics, targetting for the first time a qualitative semantics: Scott domains.

Let us now move to a more technical introduction.

## B. *The Relational Model and Quantitative Semantics*

1) **The relational model:** We assume that the reader is familiar with the category **Rel** of sets and relations (see e.g. [Ehr12] for a reference). **Rel** is a Seely category [Mel09]: its monoidal product is the cartesian product of sets, its cartesian product is given by the disjoint union, and its exponential modality ! sends a set **A** to the set $\mathcal{M}_f(\mathbf{A})$ of *finite multisets* of elements of **A**. We adopt standard conventions for multisets: a list notation $[a_1, \dots, a_n]$ possibly with repetitions, with the empty multiset written $[\cdot]$. Multiset union is written $+$.

As **Rel** is a Seely category, one can consider the Kleisli category for the exponential comonad !, which is cartesian

<figure><img src="image_2.png" /><figcaption>Fig. 1. Example of a play</figcaption></figure>

<figure><img src="image_3.png" /><figcaption>Fig. 2. Its position</figcaption></figure>

closed. It thus supports the interpretation of the simply-typed $\lambda$-calculus: this sends any type $\mathbf{A}$ to a set $[[\mathbf{A}]]$ via<fnref n="1" /> $[[o]] = \{\star\}$ and $[[A \to B]] = \mathcal{M}_f([A]) \times [[B]]$. this set $[[\mathbf{A}]]$ is often referred to as the **web** of $\mathbf{A}$. Likewise, any well-typed term $\vdash M : \mathbf{A}$ yields $[[M]] \subseteq [[\mathbf{A}]]$ a subset of the web. One may think of elements of $[[\mathbf{A}]]$ as sort of *detemporalized execution traces*, and indeed they do correspond to plays in the game semantics sense where time has been suppressed. For example, we have

$$ (([\star], \star), ([\star, \star], \star), ([\star, \star], \star)) \quad (1) $$

in $[[\lambda fx. f (fx) : (o \to o) \to o \to o]]$, interpreted as an execution of the term which calls $f$ twice. For one of these calls, $f$ calls its argument once; the other time, twice – so the term ends up using $x$ twice. The same element can be rewritten as an expression $[[\star] \to \star, [\star, \star] \to \star] \to [\star, \star] \to \star$ where $[\star, \star]$ is regarded as $\star \cap \star$ with $\cap$ a commutative but non-idempotent operation, informing a presentation of the relational model as a *non-idempotent intersection type system*.

2) **Rel and game semantics:** Game semantics present computation as an exchange of moves between two players: Player $(+)$, who plays for the program under scrutiny, and Opponent $(-)$, who plays for the execution environment. In this setting, an execution traditionally appears as a *play*, a chronological sequence of moves linked with so-called *pointers* indicating their hierarchical relationships. As an example, we show in Figure 1 a play in (the strategy for) $\lambda fx. f (fx)$. It is read from top to bottom, and each move is placed under the corresponding type component. Opponent starts computation, which prompts the evaluation of $f$ with $q^+$. Then $f$ calls its argument, which prompts the evaluation of the second occurrence of $f$. After that, $f$ calls its argument twice, and $x$ gets evaluated twice. Moves are linked with so-called *justification pointers*, carrying the hierarchical relationships between variable calls.

Intuitively, one moves from (traditional) game semantics to relational semantics by forgetting *time* [BDER97]: from Figure 1 this yields the tree of Figure 2 (ignoring solid arrows), where the correspondence between moves and atoms in the type is conveyed via subscripts. This turns out to be an alternative representation of $[[\star] \to \star, [\star, \star] \to \star] \to [\star, \star] \to \star$ encountered earlier – carrying the same information about variable calls, their multiplicity and dependencies. Modern

<footnote n="1">¹The interpretation is parametrised by an interpretation for the base type. In this paper we use the singleton type for simplicity, but we show in the long version [Cla24b] how to extend that to an arbitrary set.</footnote>
presentations of game semantics [Mel05], [RW11], [CCRW17] reject time; instead, *positions* as pictured in Figure 2 are primitive. In *concurrent games*, such positions are enriched instead with *causal wiring* conveying the causal dependencies from the term, pictured with solid arrows $\to$ in Figure 2.

3) *Rigidity and symmetries: Positions*, those trees matching points in the relational model, are *unordered*: children of a same node which correspond to the same type component can be permuted at will – this corresponds to the fact that elements of $!A$ in the relational model are *multisets*.

In *thin concurrent games*, strategies play not on these quotiented structures, but rather on chosen concrete representatives called *configurations*. There, distinct copies of moves are kept separate by attributing each an identifier, an integer called its *copy index*. We draw in Figure 3 concrete representatives for the position of Figure 2, where copy indices appear in *grey*.

This feature of working with concrete representatives of positions is not unique to thin concurrent games: it is common in *categorifications* of the relational model, such as generalized species of structure [FGHW08]. There, types are interpreted not as sets comprising quotiented structures, but as *groupoids*, with objects concrete representatives of non-idempotent intersection types obtained as in *Rel* but with *lists* $\langle\alpha_1, \dots, \alpha_n\rangle$ instead of finite multisets. In quantitative semantics, these concrete representatives of quotiented objects are often referred to as *rigid*. In this categorified situation, the quotient is replaced with explicit morphisms generated by permutations between elements of these lists.

Likewise, thin concurrent games are *rigid*; and concrete configurations are related by so-called *symmetries*, forest isomorphisms which can only change copy indices. In Figure 3 we show two symmetries, which are the tree isomorphisms respecting the topological position of nodes. In thin concurrent games, the polarity of moves lets us set apart sub-groupoids of *polarized symmetries*: some symmetries, dubbed *positive*, only change the copy index of positive moves; while others, dubbed *negative*, only reindex *negative* moves. Not every symmetry is negative or positive: the composite symmetry in Figure 3 is neither. But every symmetry factors as a composition of the two, as in Figure 3.

### C. From Quantitative to Qualitative

1) *Idempotent intersection types:* In terms of intersection types, being qualitative means $\alpha \cap \alpha = \alpha$, i.e. that $\cap$ is idempotent: an expression $\alpha_1 \cap \dots \cap \alpha_n$ no longer corresponds to the finite multiset $[\alpha_1, \dots, \alpha_n]$, but to the set $\{\alpha_1, \dots, \alpha_n\}$. But brutally enforcing $\alpha \cap \alpha = \alpha$ in this way fails: the finite powerset endofunctor on Rel fails to be a comonad.

This can be fixed by moving from sets to *preorders*, insisting that relations are *down-closed*. This preorder can be presented as a subtyping relation, typically with $\star \le \star$ and

$$ \frac{\bar{\alpha}_2 \le \bar{\alpha}_1 \qquad \beta_1 \le \beta_2}{\bar{\alpha}_1 \to \beta_1 \le \bar{\alpha}_2 \to \beta_2} \qquad \frac{\forall i \in I \ \exists j \in J \ \alpha_i \le \beta_j}{[\alpha_i \mid i \in I] \le [\beta_j \mid j \in J]} \quad (2) $$

noting that the order is contravariant on the left hand side for the arrow. Note in particular that we have $\bar{\alpha} \cap \bar{\alpha} \le \bar{\alpha}$ and

$\llcorner \le \bar{\alpha}$ which reminds us of the logical laws of *contraction* and *weakening*, in that sense this preorder is *cartesian*. Types can still be multisets, but idempotence follows from the equivalence generated by this preorder: indeed, $\bar{\alpha} \le \bar{\alpha} \cap \llcorner \le \bar{\alpha} \cap \bar{\alpha}$ also. This view on idempotent intersection types is implicit in the *linear Scott model*, the linear decomposition of Scott domains discovered by Huth [Hut93] and Winskel [Win98].

The heart of Ehrhard's *extensional collapse theorem* [Ehr12] is then that the interpretation of a simply-typed $\lambda$-term in the linear Scott model is simply the *down-closure* of its relational interpretation, linking the qualitative and the quantitative.

2) *Cartesian maps:* As non-idempotent intersection types may be *categorified* into a groupoid, the preorder $\le$ should be refined into a *category*: this is achieved, for instance, through the cartesian closed bicategory of cartesian distributors [Oli21]. In this setting, given a category $A$, a morphism from $\langle \alpha_i \mid i \in I \rangle$ to $\langle \beta_j \mid j \in J \rangle$ in $!A$ consists of a function $h: I \to J$, together with a family $(f_i)_{i \in I}$ where $f_i: \alpha_i \to \beta_{f(i)}$ in $A$ – we call this a cartesian morphism, as $!A$ is the opposite of the free cartesian category over $A$. A morphism from $\alpha_1 \to \beta_1$ to $\alpha_2 \to \beta_2$ consists of morphisms $f: \alpha_2 \to \alpha_1$ and $g: \beta_1 \to \beta_2$, reflecting (2).

In this paper, we achieve an analogous categorification in thin concurrent games, turning the groupoid of configurations into a *category* of configurations. Drawing inspiration from symmetries and the contraction maps above, a natural guess is that morphisms should simply be forest morphisms which preserve the type component. For instance, we could have

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

contracting all copies down to copy index 0. But this does not take into account the contravariance on the left hand side of arrows. The missing ingredient is to account for *polarity* – *negative* contraction maps can only contract and weaken negative moves, while *positive* contraction maps can only contract and weaken positive moves, as in Figure 4. Cartesian morphisms are obtained as relational compositions

$$ \bar{\alpha} \quad \alpha \quad \bar{\alpha} \quad \alpha \quad \dots \quad \bar{\alpha} \quad \alpha $$

which are therefore no longer forest morphisms, but do induce the adequate preorder on (symmetry classes of) configurations.

3) *Cartesian matching problems:* The main contribution of this paper is to extend this into a structure-preserving functor from a category of thin concurrent games into the linear Scott model. This builds on earlier results on the relational collapse of thin concurrent games: informally, a strategy $\sigma: A \vdash B$ from $A$ to $B$ is an aggregate of states $x^\sigma$, with

$$ x_A^\sigma \leftrightarrow x_A^\sigma \leftrightarrow x_B^\sigma $$

projections obtained – ignoring the issue of taking symmetry classes – by simply forgetting the causal arrows $\to$ displayed e.g. in Figure 2. The *relational collapse* of $\sigma$ then gathers all
<figure><img src="image_5.png" /><figcaption>Fig. 3. Concrete configurations with copy indices</figcaption></figure>

<figure><img src="image_6.png" /><figcaption>Fig. 4. Cartesian morphisms</figcaption></figure>

pairs $(x_A^\sigma, x_B^\sigma)$. But to reach the linear Scott model, we need to build a relation that is *down-closed*! We shall achieve this by sending $\sigma$ to all pairs $(y_A, y_B)$ such that we have

$$y_A \overset{\leftarrow\overrightarrow{}}{\rightleftarrows} x_A^\sigma \leftrightarrow x^\sigma \mapsto x_B^\sigma \overset{\leftarrow\overrightarrow{}}{\rightleftarrows} y_B,$$

i.e. simply the down-closure with respect to $\overset{\leftarrow\overrightarrow{}}{\rightleftarrows}$. This does yield a valid morphism in the linear Scott model. But this leaves us with the hard task to show that this down-closure remains functorial. So for $\sigma: A \vdash B$ and $\tau: B \vdash C$, given

$$x^\sigma \mapsto x_B^\sigma \overset{\leftarrow\overrightarrow{}}{\rightleftarrows} x_B \overset{\leftarrow\overrightarrow{}}{\rightleftarrows} x_B^\tau \leftrightarrow x^\tau,$$

we must find a synchronization $z^{\tau \odot \sigma}$ in $\tau \odot \sigma$ whose (down-closure of the) projection on $A, C$ is the same. An analogous property is necessary with respect to symmetries to construct thin concurrent games [Cla24a, Proposition 7.4.4]. But here, the situation is significantly more complex: both $x^\sigma$ and $x^\tau$ are trying to duplicate and erase each other, and we must find a satisfactory state where all these duplications and erasures are satisfied – we call this a *cartesian matching problem*.

In game semantics we approach the question concretely, and provide a combinatorial argument to resolve such matchings. This is the crux; from there it is not hard to provide an interpretation-preserving functor to the linear Scott model.

### D. *Outline*.

Of course, this general idea comes with various technical hurdles. First, we must introduce thin concurrent games, along with their relational collapse. This already comes with a significant technical set-up on top of thin concurrent games: typically, those configurations that match points in the relational model must be identified via a *payoff* mechanism. One must also introduce the slightly unorthodox concept of a *relative Seely* (~-)categories, a weakening of Seely categories, as the structure of plain Seely categories is not preserved by the relational collapse. Additionally, defining cartesian morphisms demands a fairly concrete description of the games considered, referring explicitly to copy indices: for that we import from [Cla24a] the rather clunky notion of *mixed board*. Altogether, this content is well-covered in other sources [Cla24a], [COP23], which our presentation follows.

In Section II, we recall thin concurrent games and their *relational collapse*. In Section III we refine our games to allow the collapse to the linear Scott model; we introduce and study *cartesian morphisms* on a mixed board. In Section IV we solve cartesian matching problems, and derive our main results.

## II. THIN CONCURRENT GAMES

### A. Basic Concurrent Games

The framework of concurrent games [MM07], [FP09], [RW11] is not merely a game semantics for concurrency, but a deep reworking of the basic mechanisms of game semantics using causal “truly concurrent” structures from concurrency theory [NPW79], which we must first introduce.

1) *Event structures:* Concurrent games and strategies are based on event structures. An event structure represents the behaviour of a system as a set of possible computational events equipped with dependency and incompatibility constraints.

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

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

vendetta: $\forall e_1 \#_E e_2, \forall e_2 \le_E e'_2, e_1 \#_E e'_2$.

Operationally, an event can occur if all its dependencies are met, and no conflicting events have occurred. A finite set $x \subseteq_f |E|$ down-closed for $\le_E$ and comprising no conflicting pair is called a **configuration** – we write $\mathcal{C}(E)$ for the set of configurations on $E$, naturally ordered by inclusion. If $x \in \mathcal{C}(E)$ and $e \in |E|$ is such that $e \notin x$ but $x \cup \{e\} \in \mathcal{C}(E)$, we say that $e$ is **enabled** by $x$ and write $x \vdash_E e$. For $e_1, e_2 \in |E|$ we write $e_1 \to_E e_2$ for the **immediate causal dependency**, i.e. $e_1 <_E e_2$ with no event strictly in between. Finally, two events $e_1, e_2 \in |E|$ are **in immediate conflict**, written $e_1 \rightsquigarrow_E e_2$, if $e_1 \#_E e_2$, and this conflict is not inherited by *vendetta*. A **map of es** from $E$ to $F$ is a function $f: |E| \to |F|$ such that: (1) for all $x \in \mathcal{C}(E)$, the direct image $fx \in \mathcal{C}(F)$; and (2) for all $x \in \mathcal{C}(E)$ and $e, e' \in x$, if $fe = fe'$ then $e = e'$.
2) **Games and strategies:** Throughout this paper, we will gradually refine our notion of game. For now, a **plain game** is simply an event structure $A$ together with a **polarity function** $\text{pol}_A: |A| \to \{-, +\}$ which specifies, for each event $a \in A$, whether it is **positive** (i.e. due to Player / the program) or **negative** (i.e. due to Opponent / the environment). Events are often called **moves**, and annotated with their polarity.

A strategy is an event structure with a projection map to $A$:

**Definition 2.** Consider $A$ a plain game. A strategy on $A$, written $\sigma: A$, is an es $\sigma$ together with a map $\partial_\sigma: \sigma \to A$ called the **display map**, satisfying two conditions [Cla24a].

We skip the two conditions, which do not play a major role in this paper (their use is encapsulated in technical lemmas and propositions proved elsewhere). Note also that though a strategy does not come with a polarity function for the moves in $\sigma$, they do inherit a polarity through $\partial_\sigma$.

As a simple example, the usual game $\mathbb{B}$ for booleans is

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

drawn from top to bottom: Opponent initiates computation with the first move $q$, to which Player can react with $tt$ or $ff$.

Strategies give a “proof-relevant” account of execution, in the sense that moves and configurations of the game can have multiple witnesses in the strategy. For example, on the left below, $b$ and $c$ are both mapped to the same move $tt$:

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

We denote immediate causality by $\to$ in strategies, and by dotted lines for games – this lets us represent the strategy in a single diagram, as on the right above. Similar diagrams may represent not entire games and strategies but configurations of games and strategies, which implicitly inherit a partial order.

3) **Morphisms between strategies:** For $\sigma$ and $\tau$ two strategies on $A$, a **morphism** from $\sigma$ to $\tau$, written $f: \sigma \Rightarrow \tau$, is a map of event structures $f: \sigma \to \tau$ preserving the dependency relation $\leq$ (we say it is **rigid**) and such that $\partial_\tau \circ f = \partial_\sigma$.

4) **+-covered configurations:** A strategy is completely characterized by a subset of its configurations, called **+-covered**.

For a strategy $\sigma$ on a game $A$, a configuration $x \in \mathscr{C}(\sigma)$ is **+-covered** if all its maximal events are positive. We write $\mathscr{C}^+(\sigma)$ for **+-covered** configurations of $\sigma$, ordered by $\subseteq$.

**Lemma 1.** Consider a plain game $A$, and strategies $\sigma, \tau: A$.

If $f: \mathscr{C}^+(\sigma) \cong \mathscr{C}^+(\tau)$ is an order-isomorphism such that $\partial_\tau \circ f = \partial_\sigma$, then there is a unique isomorphism of strategies $\tilde{f}: \sigma \cong \tau$ such that for all $x \in \mathscr{C}^+(\sigma)$, $\tilde{f}(x) = f(x)$.

This immediate consequence of [Cla24a, Lemma 6.3.4] is the first hint of a methodology central to this paper: in concurrent games, we rarely reason at the level of individual events, preferring whenever possible to reason with configurations, especially when linking with relational-like models.

## B. A ~-category of concurrent games and strategies

We now show how games and strategies are organized into a ~-category – that is, a bicategory where 2-cells are degenerated so that each hom-set forms a setoid<fnref n="2" />.

1) **Strategies between games:** If $A$ is a plain game, its **dual** $A^\perp$ has the same components as $A$ except for the reversed polarity. In particular $\mathscr{C}(A) = \mathscr{C}(A^\perp)$. The **parallel composition** $A \parallel B$ of $A$ and $B$ is simply $A$ and $B$ side by side, with no interaction – its events are the tagged disjoint union $|A| \parallel |B| = |A| + |B| = \{1\} \times |A| \uplus \{2\} \times |B|$, and other components are inherited. Likewise, the **hom** $A \vdash B$ is simply defined as $A^\perp \parallel B$. We write $x_A \parallel x_B$ for the configuration of $A \otimes B$ that has $x_A \in \mathscr{C}(A)$ on the left and $x_B \in \mathscr{C}(B)$ on the right, and likewise for $x_A \vdash x_B \in \mathscr{C}(A \vdash B)$, informing

$$ - \parallel - : \mathscr{C}(A) \times \mathscr{C}(B) \cong \mathscr{C}(A \parallel B), \quad (3) $$

$$ - \vdash - : \mathscr{C}(A) \times \mathscr{C}(B) \cong \mathscr{C}(A \vdash B) \quad (4) $$

order-isomorphisms. A **strategy from** $A$ to $B$ is a strategy on the game $A \vdash B$. Note that if $\sigma: A \vdash B$ and $x^\sigma \in \mathscr{C}(\sigma)$, by convention we write $\partial_\sigma(x^\sigma) = x_A^\sigma \vdash x_B^\sigma \in \mathscr{C}(A \vdash B)$.

Our first example of a strategy between games is **copycat** $\mathscr{C}_A: A \vdash A$, the identity morphism on $A$ in our ~-category. Concretely, copycat on $A$ has the same events as $A \vdash A$, but adds immediate causal links between copies of the same move across components. Via Lemma 1, the following characterizes copycat up to isomorphism [Cla24a, Lemma 6.4.4].

**Proposition 1.** If $A$ is a game, there is an order-isomorphism

$$ \mathscr{C}_{(-)} : \mathscr{C}(A) \cong \mathscr{C}^{+}(\mathscr{C}_{A}) $$

such that for all $x \in \mathscr{C}(A)$, $\partial_{\mathscr{C}_A}(\mathscr{C}_x) = x \vdash x$.

So the copycat strategy is essentially the diagonal relation.

2) **Composition:** Consider $\sigma: A \vdash B$ and $\tau: B \vdash C$. We define their composition $\tau \odot \sigma: A \vdash C$. Concurrent games are a dynamic model, and to successfully synchronize, $\sigma$ and $\tau$ must agree to play the same events in the same order.

We say that configurations $x^\sigma \in \mathscr{C}(\sigma)$ and $x^\tau \in \mathscr{C}(\tau)$ are **matching** if they reach the same configuration on $B$, i.e. $x_B^\sigma = x_B^\tau = x_B$. If that is the case, it induces a synchronization between events of $x^\sigma$ and $x^\tau$. If the causal constraints of $\sigma$ and $\tau$ are globally compatible through this synchronization – i.e. there is no deadlock – we say that $x^\sigma$ and $x^\tau$ are **causally compatible** (the precise definition [Cla24a] plays no role in this paper). The **composition** of $\sigma$ and $\tau$ is the unique (up to iso) strategy whose **+-covered** configurations are essentially causally compatible pairs of **+-covered** configurations. Writing $\mathscr{CC}(\sigma, \tau)$ for causally compatible pairs $(x^\sigma, x^\tau) \in \mathscr{C}^+(\sigma) \times \mathscr{C}^+(\tau)$ (ordered componentwise):

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

There is a strategy $\tau \odot \sigma: A \vdash C$, unique up to iso, with

$$ - \odot - : \mathscr{CC}(\sigma, \tau) \cong \mathscr{C}^{+}(\tau \odot \sigma) $$

<footnote n="2">²Games and strategies actually form a proper bicategory [COP23]. Here we only consider a ~-category, as the coherence laws play no role in the paper.</footnote>
an order-isomorphism s.t. for all $x^\sigma \in \mathscr{C}^+(\sigma)$ and $x^\tau \in \mathscr{C}^+(\tau)$ causally compatible, $\partial_{\tau \odot \sigma}(x^\tau \odot x^\sigma) = x_A^\sigma \vdash x_A^\tau$.

See [Cla24a, Proposition 6.2.1]. This description of composition emphasizes the conceptual difference between a static model, in which composition is based merely on matching pairs, and a dynamic model, based on causal compatibility and sensitive to deadlocks. We get [Cla24a, Theorem 6.4.11]:

**Theorem 1.** There is a ~-category **CG** with: (1) objects, plain games; (2) morphisms from $A$ to $B$, strategies $\sigma : A \vdash B$; and equivalence relation, isomorphism of strategies.

### C. Adding Symmetry

The ambient ~-category in which this paper takes place is not quite **CG**, but a refinement sensitive to symmetry. We now go from **CG** to **TCG** by replacing the set of configurations $\mathscr{C}(A)$ with a groupoid of configurations $\mathscr{S}(A)$ whose morphisms are chosen bijections called *symmetries*.

1) Event structures with symmetry: We start with [Win07]:

**Definition 3.** An isomorphism family on es E is a groupoid $\mathscr{S}(E)$ with objects configurations, and morphisms certain bijections between configurations, satisfying two conditions.

We call $(E, \mathscr{S}(E))$ an event structure with symmetry (ess).

We call morphisms in $\mathscr{S}(E)$ symmetries, and write $\theta: x \cong_E y$ if $\theta: x \cong y$ with $\theta \in \mathscr{S}(E)$. The domain $\mathrm{dom}(\theta)$ of $\theta: x \cong_E y$ is $x$, and likewise its codomain $\mathrm{cod}(\theta)$ is $y$. A map of ess $E \to F$ is a map of es such that the bijection

$$f\theta \stackrel{\mathrm{def}}{\cong} f x \stackrel{f^{-1}}{\cong} x \stackrel{\theta}{\cong} y \stackrel{f}{\cong} fy,$$

is in $\mathscr{S}(F)$ for every $\theta: x \cong_E y$ (recall that $f$ restricted to any configuration is bijective). This exactly amounts to making $f: \mathscr{S}(E) \to \mathscr{S}(F)$ a functor of groupoids. There is a 2-category **ESS** of ess, maps of ess, and natural transformations between the induced functors. For $f,g: E \to F$ such a natural transformation is necessarily unique [Win07], and corresponds to the fact that for every $x \in \mathscr{C}(E)$ the composite bijection

$$f x \stackrel{f^{-1}}{\cong} x \stackrel{g}{\cong} g x \qquad (5)$$

via local injectivity of $f$ and $g$, is in $\mathscr{S}(F)$. So this is an equivalence, denoted $f \sim g$ – we say $f,g$ are *symmetric*.

2) Thin games: To match the polarized structure, a game with symmetry is an ess with two sub-symmetries, one for each player (see e.g. [Mel03], [CCW19], [Paq22]).

**Definition 4.** A thin concurrent game (tcg) is a game $A$ with isomorphism families $\mathscr{S}(A), \mathscr{S}_+(A), \mathscr{S}_-(A)$ s.t. $\mathscr{S}_+(A), \mathscr{S}_-(A) \subseteq \mathscr{S}(A)$, symmetries preserve polarity, and

(1) if $\theta \in \mathscr{S}_+(A) \cap \mathscr{S}_-(A)$, then $\theta = \mathrm{id}_x$ for $x \in \mathscr{C}(A)$,

(2) if $\theta \in \mathscr{S}_-(A)$, $\theta \subseteq \theta' \in \mathscr{S}(A)$, then $\theta' \in \mathscr{S}_-(A)$,

(3) if $\theta \in \mathscr{S}_+(A)$, $\theta \supseteq \theta' \in \mathscr{S}(A)$, then $\theta' \in \mathscr{S}_+(A)$,

where $\theta \subseteq \theta'$ is $\theta \subseteq \theta'$ with (pairs of) events of polarity p.

Elements of $\mathscr{S}_+(A)$ are **positive**; they intuitively correspond to symmetries carried by positive moves, introduced

by Player. We write $\theta: x \cong_A^+ y$ if $\theta \in \mathscr{S}_+(A)$ – and symmetrically for $\mathscr{S}_-(A)$. We have [Cla24a, Lemma 7.1.18]:

**Lemma 2.** For $A$ a tcg and $\theta: x \cong_A^+ z$, there are unique $y \in \mathscr{C}(A)$, $\theta_-: x \cong_A^- y$ and $\theta_+: y \cong_A^+ z$ s.t. $\theta = \theta_+ \circ \theta_-$.

We extend with symmetry the basic constructions on games: the **dual** $A^\perp$ has the same symmetries as $A$, but $\mathscr{S}_+(A^\perp) = \mathscr{S}_-(A)$ and $\mathscr{S}_-(A^\perp) = \mathscr{S}_+(A)$; the **parallel composition** $A_1 \parallel A_2$ has symmetries those $\theta_1 \parallel \theta_2: x_1 \parallel x_2 \cong_{A_1 \parallel A_2} y_1 \parallel y_2$, where each $\theta_i: x_i \cong_{A_i} y_i$, and similarly for positive and negative symmetries; the **hom** $A \vdash B$ is $A^\perp \parallel B$.

3) Thin strategies: We now extend strategies:

**Definition 5.** A strategy on tcg $A$, written $\sigma: A$, is an ess $\sigma$ with a map of ess $\partial_\sigma: \sigma \to A$ forming a strategy in the sense of Definition 2, subject to two additional conditions [Cla24a].

The composition of thin strategies $\sigma: A \vdash B$ and $\tau: B \vdash C$ is obtained by equipping $\tau \odot \sigma$ (Proposition 2) with an adequate isomorphism family. If $\mathscr{S}^+(\sigma)$ is the restriction of $\mathscr{S}(\sigma)$ to $+\text{-covered}$ configurations, then we can write $\mathrm{CC}(\mathscr{S}^+(\sigma), \mathscr{S}^+(\tau))$ for the pairs $(\varphi^\sigma, \varphi^\tau)$ of symmetries which are matching, i.e. $\varphi_B^\sigma = \varphi_B^\tau$ and whose domain (or equivalently, codomain) are causally compatible.

**Proposition 3.** Consider $\sigma: A \vdash B$ and $\tau: B \vdash C$ thin strategies. There is a unique symmetry on $\tau \odot \sigma$ with a bijection

$$(- \odot -) : \mathrm{CC}(\mathscr{S}^+(\sigma), \mathscr{S}^+(\tau)) \cong \mathscr{S}^+(\tau \odot \sigma)$$

commuting with dom and cod and compatible with display maps, i.e. $(\varphi^\tau \odot \varphi^\sigma)_A = \varphi_A^\sigma$ and $(\varphi^\tau \odot \varphi^\sigma)_C = \varphi_C^\sigma$.

This follows from [Cla24a, Proposition 7.3.1]. This makes $\tau \odot \sigma: A \vdash C$ a thin strategy. In order to form a ~-category, it is necessary to give the adequate equivalence relation between thin strategies. For two maps $f,g: E \to A$ into a tcg, we write $f \sim^+ g$ if $f \sim g$ and for every $x \in \mathscr{C}(E)$ the symmetry obtained as (5) is positive. This lets us give the next definition:

**Definition 6.** Let $\sigma, \tau: A \vdash B$ be thin strategies. A positive morphism of strategies from $\sigma$ to $\tau$ is a rigid map of ess $f: \sigma \to \tau$ such that $\partial_\tau \circ f \sim^+ \partial_\sigma$. We write $f: \sigma \Rightarrow \tau$ to mean that $f$ is a positive morphism from $\sigma$ to $\tau$.

A positive iso $f: \sigma \cong \tau$ is an invertible positive morphism.

Positive isomorphisms will provide the equivalence relation for the ~-categorical structure of thin concurrent games. A crucial challenge in constructing this ~-category is then to ensure that positive isomorphism is preserved under composition. This demands in particular, given $f: \sigma \Rightarrow \sigma': A \vdash B$ and $g: \tau \Rightarrow \tau': B \vdash C$, to form a horizontal composition

$$g \odot f : \tau \odot \sigma \Rightarrow \tau' \odot \sigma' : A \vdash C,$$

which requires us to transport $x^\tau \odot x^\sigma \in \mathscr{C}^+(\tau \odot \sigma)$ to $\mathscr{C}^+(\tau' \odot \sigma')$ via $f$ and $g$. However, the issue is that $f(x^\sigma)$ and $g(x^\tau)$ may not be matching: the hypotheses at hand only yield $\theta: f(x^\sigma)_B \cong_B g(x^\tau)_B$ a mediating symmetry – hence to achieve our goals, we use [Cla24a, Proposition 7.4.4]:
<table><caption>Fig. 5. Payoff for ⊗ and ∁</caption><thead><tr><th>⊗</th><th>-1</th><th>0</th><th>+1</th><th>∁</th><th>-1</th><th>0</th><th>+1</th></tr></thead><tbody><tr><th>-1</th><td>-1</td><td>-1</td><td>-1</td><td>-1</td><td>-1</td><td>-1</td><td>+1</td></tr><tr><th>0</th><td>-1</td><td>0</td><td>+1</td><td>0</td><td>-1</td><td>0</td><td>+1</td></tr><tr><th>+1</th><td>-1</td><td>+1</td><td>+1</td><td>+1</td><td>+1</td><td>+1</td><td>+1</td></tr></tbody></table>

**Proposition 4.** Consider $x^\sigma \in \mathscr{C}^+(\sigma)$, $\theta_B : x_B^\sigma \cong_B x_B^\tau$, $x^\tau \in \mathscr{C}^+(\tau)$ causally compatible. Then, there are unique $y^\tau \odot y^\sigma \in \mathscr{C}^+(\tau \odot \sigma)$ with $\varphi^\sigma : x^\sigma \cong_\sigma y^\sigma$ and $\varphi^\tau : x^\tau \cong_\tau y^\tau$, such that $\varphi_A^\sigma \in \mathscr{I}_-(A)$ and $\varphi_C^\tau \in \mathscr{I}_+(C)$, and $\varphi_B^\sigma \circ \theta = \varphi_B^\sigma$.

Altogether, this allows us to construct:

**Theorem 2.** There is a $\sim$-category TCG with: (1) objects, thin concurrent games; (2) morphisms, strategies $\sigma : A \vdash B$; (3) equivalence, positive isomorphism.

### D. Boards

Following earlier work [Cla24a], we must now enrich tcgs with structure allowing us to identify those configurations that correspond to points in the relational model.

**Definition 7.** A **board** is a tcg $A$ with $\kappa_A : \mathscr{C}(A) \to \{-1, 0, +1\}$ a **payoff function**, subject to conditions [Cla24a].

A **--board** is additionally negative (i.e. minimal events are negative) and initialized (i.e. $\kappa_A(\emptyset) \ge 0$). A **--board A** is **strict** if $\kappa_A(\emptyset) = 1$ and its initial moves are in conflict. It is **well-opened** if it is strict with exactly one initial move.

The payoff function $\kappa_A$ assigns a value to each configuration. Configurations $x$ with payoff 0 are called **complete**, written $x \in \mathscr{C}^0(A)$. Otherwise, $\kappa_A$ assigns a responsibility for why a configuration is non-complete: if $\kappa_A(x) = -1$ then Player is responsible, otherwise it is Opponent.

The objects of our forthcoming category will be **--boards**. The first basic **--boards** are the units. In the presence of the payoff function the empty tcg $\emptyset$ splits into two units, the **top** $\top$ with $\kappa_\top(\emptyset) = 1$, and the **one** **--board 1** with $\kappa_1(\emptyset) = 0$. To interpret the base type we shall use a strict board, also written $o$, with only one move $q^-$ and $\kappa_o(\emptyset) = 1$, $\kappa_o(\{q\}) = 0$.

1) **Dual, tensor and par:** The **dual** extends with payoff via $\kappa_{A^\perp}(x) = -\kappa_A(x)$. **Parallel composition** splits into:

**Definition 8.** Consider A and B two boards. Their tensor $A \otimes B$ and their par $A \mathcal{N} B$ are $A \parallel B$ enriched with:

$$ \kappa_{A \bullet B}(x_A \parallel x_B) = \kappa_A(x_A) \bullet \kappa_B(x_B) $$

for $\bullet \in \{\otimes, \mathcal{N}\}$ defined on payoff values in Figure 5.

If A and B are **--boards**, $A \vdash B$ denotes $A^\perp \mathcal{N} B$. The isos (3) and (4) refine to bijections for $\bullet \in \{\otimes, \mathcal{N}, \vdash\}$:

$$ - \bullet - : \mathscr{C}^0(A) \times \mathscr{C}^0(B) \cong \mathscr{C}^0(A \bullet B). \quad (6) $$

2) **The with:** The **sum** $E+F$ of two ess $E$ and $F$ is $E \parallel F$ with added pairwise conflicts between events of $E$ and $F$.

This directly extends to tcgs. If $A, B$ are tcgs and $x_A \in \mathscr{C}(A)$, we write $(1, x_A) \in \mathscr{C}(A+B)$ as a shorthand for $\{1\} \times$

$x_A$ and likewise for $(2, x_B) = \{2\} \times x_B \in \mathscr{C}(A+B)$ for $x_B \in \mathscr{C}(B)$. Note that all configurations of $A+B$ have the form $(1, x_A)$ for $x_A \in \mathscr{C}(A)$ or $(2, x_B)$ for $x_B \in \mathscr{C}(B)$. For non-empty configurations, this decomposition is unique.

**Definition 9.** Consider $S$ and $T$ two strict **--boards**. Their **with** $S \& T$ is the strict **--board** with tcg the sum $S + T$ and $\kappa_{S \& T}(1, x_S) = \kappa_S(x_S)$ and $\kappa_{S \& T}(2, x_T) = \kappa_T(x_T)$ for non-empty configurations and $\kappa_{S \& T}(\emptyset) = 1$.

This construction will give a cartesian product in the sub-category of strict **--boards**. In the sequel, we shall use the obvious $n$-ary generalization of the product. Any strict **--board** $S$ decomposes uniquely (up to forest isomorphism) as $S \cong \&_{i \in I} S_i$, where each $S_i$ is well-opened.

3) **Linear closure:** We start with a restricted case:

**Definition 10.** Consider A a **--board** and $S$ well-opened. Then, $A \to S$ has tcg set as $A \vdash S$ except for:

$$ \text{causality: } \le_{A \to S} = \le_{A \vdash S} \cup \{(2, s_0), (1, a) \mid a \in A\} $$

where $\min(S) = \{s_0\}$, yielding a well-opened **--board**.

This corrects the non-negativity of $A \vdash S$, by forcing the missing dependency. In the sequel, we shall need $A \to S$ not only when $S$ is well-opened but when it is strict. In that case, $A \to S$ may be defined directly via strict boards, as done in:

**Definition 11.** Consider A a **--board**, and $S$ a strict **--board**, with $S \cong \&_{i \in I} S_i$. Then, we define $A \to S = \&_{i \in I} (A \to S_i)$.

4) **Exponential:** We start with a construction on ess:

**Definition 12.** The **bang** !E of an ess E has components:

$$ \begin{array}{l} \text{events: } |!A| = \mathbb{N} \times |A| \\ \text{causality: } (i, a_1) \le!_A (j, a_2) \Leftrightarrow i = j \wedge a_1 \le_A a_2 \\ \text{conflict: } (i, a_1) \#!_A (j, a_2) \Leftrightarrow i = j \wedge a_1 \#_A a_2 \end{array} $$

with $\theta \in \mathscr{I}(!A)$ iff there is $\pi : \mathbb{N} \cong \mathbb{N}$ and $(\theta_n)_{n \in \mathbb{N}} \in \mathscr{I}(A)^{\mathbb{N}}$ s.t. for all $(i, a) \in \mathrm{dom}(\theta)$, $\theta(i, a) = (\pi(i), \theta_i(a))$.

In $(i, e) \in !E$, we refer to $i$ as a **copy index**. Here, symmetries express that copy indices can be reindexed at will. This directly extends to tcgs, see e.g. [Cla24a] for details.

### E. The Relative Seely Category of Sequential Innocence

Finally, the results of this paper will not hold for all strategies, but only those of a restricted shape.

1) **Deterministic sequential innocence:** We first introduce:

**Definition 13.** Consider A a board, and $\sigma : A$ a strategy.

We say that $\sigma$ is **deterministic sequential innocent** (dsinn) iff it is negative, winning (i.e. for all $x^\sigma \in \mathscr{C}^+(\sigma)$, $\kappa_A(\partial_\sigma x^\sigma) \ge 0$), and $\le_\sigma$ is an **Opponent-branching forest**.

Winning ensures that strategies are well-behaved with respect to payoff: in particular, a closed interaction between winning strategies will always result in a complete position, which is essential for the relational collapse. Requiring an Opponent-branching forest makes $\sigma$ mimic a syntactic tree:
this ensures that composition is deadlock-free and therefore
matches relational composition.

Copycat strategies on --boards are automatically determin-
istic sequential innocent. Deterministic sequential innocence
is also stable under composition, which ensures [Cla24a]:

**Theorem 3.** There is a ~-category DSInn with: --boards;
dsinn strategies; up to positive isomorphism.

2) *Relative Seely categories: DSInn* is a Seely category, but this structure is not preserved by the relational collapse (see [COP23]). The categorical notion describing the structure that *is* preserved is called a *relative Seely category* [CP21], [Cla24a]; we now recall the definition.

**Definition 14.** A relative Seely category is a symmetric monoidal category $(C, \otimes, 1)$ equipped with a full subcategory $C_s$ which has finite products preserved by the inclusion $J: C_s \to C$; with the following data and axioms:

* For every $B \in C$ there is $B \dashv -: C_s \to C_s$ with $\Lambda(-): C(A \otimes B, S) \simeq C(A, B \dashv S)$ a bijection natural in $A \in C$ and $S \in C_s$.

* There is a $J$-relative comonad $! : C_s \to C$. This means that we have, for every $S \in C_s$, an object $!S \in C$ and a **dereliction** morphism $\text{der}_S : !S \to S$, and for every $\sigma : !S \to T$, a **promotion** $\sigma^1 : !S \to !T$.

* $! : (C_s, \& , \top) \to (C, \otimes, 1)$ is symmetric strong monoidal, subject to a few coherence conditions [Cla24a].

Any Seely category is a relative Seely category with $C = C_s$. For any relative Seely category, the Kleisli category associated with $!$, denoted $C_!$, is cartesian closed: it has objects those of $C_s$, morphisms $C_!(S, T) = C(!S, T)$, products $\&$, and function space $S \Rightarrow T = !S \dashv T$. There is an accompanying notion of morphism: a **relative Seely functor** from $C$ to $D$ is a functor $F: C \to D$ together with isomorphisms

$$
\begin{align*}
t^\otimes_{A,B} & : FA \otimes FB \cong F(A \otimes B) \\
t^\&_{S,T} & : FS \& FT \cong F(S \& T) \\
t^{\neg}_{A,S} & : FA \dashv FS \cong F(A \dashv S)
\end{align*}
$$

and $t^1 : 1 \cong F1$, $t^\top : \top \cong F\top$, $t_S^1 : !FS \cong F!S$ satisfying
appropriate naturality and coherence conditions [Cla24a]. This
ensures that $F$ lifts to a cartesian closed functor $F_! : C_! \to D_!$.

3) *The relative Seely category DSInn:* From now on, by *strategy* we mean a morphism in DSInn.

Given $\sigma: A \vdash B$ and $\tau: C \vdash D$, their **tensor** $\sigma: A \otimes C \vdash B \otimes D$ has ess $\sigma \parallel \tau$ with the obvious display map. For --boards $\Gamma, S, T$ with $S, T$ strict, $\sigma: \Gamma \vdash S$ and $\tau: \Gamma \vdash T$, the **pairing** has ess $\sigma + \tau$ with the obvious display map, and the **projections** $\pi_S: S \& T \vdash S$ and $\pi_T: S \& T \vdash T$ are copycat strategies. The **currying** of $\sigma: \Gamma \otimes A \vdash B$ is $\Lambda(\sigma): \Gamma \vdash A \dashv B$ with ess $\sigma$, and display map the only sensible reassignment, the **evaluation** $\text{ev}_{A,S}: (A \dashv S) \otimes A \vdash S$ is the obvious copycat strategy. The **promotion** of $\sigma: !S \vdash T$ has ess $!\sigma$, and the display map following a bijection $\mathbb{N} \times \mathbb{N} \simeq \mathbb{N}$ on the left hand side. The **dereliction** strategy $\text{der}_A: !A \vdash A$

$$
\begin{align*}
s_{A,B}^{\perp} & : \mathfrak{R}(A) \times \mathfrak{R}(B) & \approx \mathfrak{R}(A \vdash B) \\
s_{A,B}^{\otimes} & : \mathfrak{R}(A) \times \mathfrak{R}(B) & \approx \mathfrak{R}(A \otimes B) \\
s_1^1 & : \mathbf{1} & \approx \mathfrak{R}(\mathbf{1}) \\
s_S^1 & : \mathcal{M}_f(\mathfrak{R}(S)) & \approx \mathfrak{R}(\mathbf{!S}) \\
s_S^\top & : \emptyset & \approx \mathfrak{R}(\top) \\
s_{S,T}^\& & : \mathfrak{R}(S) + \mathfrak{R}(T) & \approx \mathfrak{R}(S \& T) \\
s_{A,S}^\neg & : \mathfrak{R}(A) \times \mathfrak{R}(S) & \approx \mathfrak{R}(A \dashv S)
\end{align*}
$$

<figure><img src="image_9.png" /><figcaption>Fig. 7. The relational collapse : forgetting the dynamic order</figcaption></figure>

is defined as a copycat strategy, opening one copy with copy
index 0. Finally, the *Seely isomorphisms* are

$$
\text{see}_{S,T} : \mathbf{!}S \otimes \mathbf{!}T \cong \mathbf{!}(S \ \& \ T),
$$

defined again by the obvious copycat strategy, and the obvious
isomorphism $!\top \cong \mathbf{1}$ between empty games. Altogether, these
provide all the components for the desired structure:

**Theorem 4.** *The components above make DSInn a relative Seely category; where the strict full subcategory DSInn<sub>s</sub> is restricted to strict --boards.*

Therefore, the Kleisli category DSInn<sub>!</sub> is cartesian closed.

F. Relational Collapse

1) *Collapsing games:* From a board, the web as in the relational model is got as the symmetry classes of null payoff:

$$
\mathfrak{R}(A) = \{x \in \mathcal{C}(A) \mid \kappa_A(x) = 0\} / \cong_A \quad (7)
$$

called the **positions** of a board A. Here, we use symbols
x, y, z... to range over symmetry classes of configurations –
note the different font than for configurations.

This is compatible with constructions: there are relatively
straightforward bijections presented in Figure 6 where A, B
are any --boards and S, T are strict. As an immediate corol-
lary we get a bijection, for every simple type A:

$$
s_A : [[A]]_{\text{Rel}} \cong \mathfrak{R}([A])_{\text{DSInn}} \quad (8)
$$

by induction on $A$ – and similarly for a context $\Gamma$.

2) *Collapsing strategies:* Now, we send a strategy $\sigma: A \vdash B$ to those positions reached by +-covered configurations:

$$
\mathfrak{R}(\sigma) = \{(x_A, x_B) \in \mathfrak{R}(A) \times \mathfrak{R}(B) \\ \qquad | \exists x^{\sigma} \in \mathcal{C}^{+}(\sigma), x_A^{\sigma} \in x_A, x_B^{\sigma} \in x_B\}.
$$

This is illustrated in Figure 7, with one +-covered configu-
ration arising from the interpretation of $\lambda f x. f (f x) : (o_1 \to
o_2) \to o_3 \to o_4$, labelling the occurrences of the base type to
match the moves in the diagram. This operation forgets the
dynamic causal links $\to$, along with *copy indices*.
3) **A Relative Seely Functor:** The main difficulty is to prove preservation of composition; and in particular the *causal compatibility* clause of Proposition 2. This relies on a *deadlock-free lemma* ensuring that innocent strategies cannot deadlock, see e.g. [Cla24a]. For the additional structure, preservation is witnessed by the bijections of Figure 6, which altogether form the components of [Cla24a, Corollary 10.4.15]:

**Theorem 5.** *The above provide the components for $\Re(-)$ : DSInn $\to$ Rel a relative Seely functor.*

In particular $\Re_! : DSInn_! \to Rel_!$ is cartesian closed, so:

**Corollary 1.** *Consider $\Gamma \vdash M : A$ a simply-typed $\lambda$-term.*

$$ \text{Then, } [[M]]_{\text{Rel}_!} = s_A \circ \Re([[[M]]_{\text{DSInn}_!}) \circ !s_{\Gamma}^{-1}. $$

### III. FROM GAMES TO THE LINEAR SCOTT MODEL

#### A. The Linear Scott Model

1) **The basic category:** The linear Scott model can be presented either as a category of functions between certain complete lattices, or equivalently, as a category of relations between certain preordered sets [Ehr12] – we opt for the latter:

**Definition 15.** ScottL has: (1) objects, preorders ($|A|, \le_A$); (2) morphisms from A to B, relations $\alpha \subseteq |A| \times |B|$ which are down-closed: if $(a, b) \in \alpha$ and $a \le_A a'$, $b \le_B b'$, then $(a', b') \in \alpha$. Composition is relational composition, and identities are obtained as $\text{id}_A = \{(a, a') | a' \le_A a\}$.

We write $A^{\text{op}}$ for the **opposite** preorder. The **product** preorder has $(a, b) \le_{A \times B} (a', b')$ iff $a \le_A a'$ and $b \le_B b'$. If $X \subseteq |A|$, we write $[X]_A$ for its down-closure in A.

2) **Seely category:** ScottL is symmetric monoidal: if A and B are preorders, then $A \otimes B = A \times B$. The monoidal unit is $1 = (\{\star\}, =)$, and the functorial action of $\otimes$ is as in the relational model, while structural morphisms are the **down-closure** of their relational counterparts. Likewise, the cartesian structure of Rel adapts to ScottL transparently, with $A \& B = A + B$ the disjoint union of the two preorders; $\top = (\emptyset, \emptyset)$ is terminal. The pairing operation is the same as in Rel, and projections in ScottL are obtained as the down-closure of those in Rel. We additionally set $A \to B = A^{\text{op}} \times B$ – again, currying is as in Rel, and evaluation in ScottL is the down-closure of evaluation in Rel. Altogether, this makes ScottL a cartesian symmetric monoidal closed category.

For the exponential, we set $|!A| = \mathcal{M}_f(|A|)$ and

$$ \mu \leq_A! \nu \Leftrightarrow \forall a \in \text{supp}(\mu), \exists a' \in \text{supp}(\nu), a \leq_A a', $$

where the **support** $\text{supp}(\mu)$ of $\mu \in \mathcal{M}_f(X)$ is the set of $x \in X$ with non-zero multiplicity. Again, this preorder is built on the same set as the exponential for the plain relational model. Together with the other components [Ehr12], this yields:

**Theorem 6.** *This makes ScottL a Seely category.*

This Seely category ScottL will be the target of our qualitative collapse. Though the exponential is built from finite multisets, this model does not actually record quantitative information, as morphisms are down-closed.

$$ (o_1 \to o_2) \to o_3 \to o_4 $$

<figure><img src="image_10.png" /><figcaption>Fig. 8. Interpretation of $(o \to o) \to o \to o$ as an arena</figcaption></figure>

We omit the presentation of ScottL as a category of functions, but we do mention that there is a full and faithful cartesian closed functor ScottL_! $\to$ Scott to the usual category of Scott domains and Scott-continuous functions, so that ScottL_! can be regarded as a full subcategory of Scott (with objects being algebraic complete lattices) [Ehr12].

For A a game, we now intend to make $\Re(A)$ a preorder by adjoining the adequate notion of cartesian morphism.

#### B. Mixed Boards

The definition of cartesian morphisms relies on copy indices. But whereas moves in boards arising from types do have copy indices, these have no official status in thin concurrent games, and this must first be corrected. For this we adopt the notion of mixed board, introduced in [Cla24a] to link thin concurrent games with standard Hyland-Ong games.

1) **Arenas:** Those boards arising from the interpretation of simple types have a specific shape – namely, they are themselves an **expansion** of a simpler structure called an **arena**:

**Definition 16.** An arena comprises $A = (|A|, \text{pol}_A, \le_A)$ a countable, negative, alternating forest. Additionally we fix, for each move $a \in |A|$, a set $\text{Ind}(a)$ which is either $\mathbb{N}$ or $\{*\}$.

This resembles Hyland-Ong arenas, with a slight change in presentation so as to remain close to boards. The new component is the set $\text{Ind}(a)$, which indicates which moves are duplicable by specifying the admissible copy indices.

We briefly present the main constructions on arenas. First, for the atom, we write $\mathcal{o}$ for the arena with exactly one (negative) move $q^-$, with $\text{Ind}(q^-) = \{*\}$: this move is not duplicable. If A is an arena, the **exponential** $!A$ has the same components as A (we do not duplicate the moves), but we set $\text{Ind}_!A(a^-) = \mathbb{N}$ for every $a^-$ minimal: we set the initial moves as duplicable. The **parallel composition** $A \parallel B$ adapts transparently to arenas, with the $\text{Ind}(-)$ function inherited. Note that any arena may be written as $A \cong \|_{i \in I} A_i$ with $A_i$ well-opened. If A and B are arenas with B well-opened, then $A \to B$ is an arena (again with $\text{Ind}$ inherited); this extends to B not well-opened with $A \to (\|_{i \in I} B_i) = \|_{i \in I} A \to B_i$.

Altogether, this lets us interpret simple types as arenas with $[[\mathcal{o}}]_{\mathbf{Ar}} = \mathcal{o}$ and $[[A \to B]] = ![[A]]_{\mathbf{Ar}} \to [[B]]_{\mathbf{Ar}}$: moves are not explicitly duplicated, but simply marked with the admissible copy indices. We show in Figure 8 the interpretation of the simple type $(o \to o) \to o \to o$ as an arena.

2) **Mixed boards:** Mixed boards pair a $--$board with an arena – here $\text{pred}(-)$ denotes the unique predecessor of a non-minimal move, exploiting that boards are forests:
<figure><img src="image_11.png" /><figcaption>Fig. 9. A structural map on $(o_1 \to o_2) \to o_3 \to o_4$</figcaption></figure>

**Definition 17.** A mixed board is $(A, \underline{A})$ with $A$ a $--board$, $\underline{A}$ an arena, with two functions $lbl_A : |A| \to |\underline{A}|$ and $ind_A : |A| \to \mathbb{N} \uplus \{*\}$, with $lbl_A$ a label forest morphism and $ind_A$ an indexing function s.t. $ind_A(a) \in \text{Ind}(\underline{a})$ for all $a \in A$, satisfying additional conditions [Cla24a]. A mixed board is strict if $A$ is strict and $\text{Ind}(\underline{a}) = \{*\}$ for every $\underline{a} \in \underline{A}$ minimal.

We use underlined metavariables to range over events of the underlying arena. The additional conditions express that the board is an “expanded” version of the arena, where moves can be copied at will by assigning new copy indices. The mixed board for the atom is $(o, \underline{o})$ with $lbl : \underline{q}^- \mapsto \underline{q}^-$ and $ind : \underline{q}^- \mapsto * -$ we shall denote this mixed board by $o$. The tensor of mixed boards has $\underline{A} \otimes \underline{B} = \underline{A} \parallel \underline{B}$, with components inherited, and the **with** is defined likewise. The **bang** of strict $S$ has $!S = !\underline{S}$ (i.e. with just $\text{Ind}(\underline{s}) = \mathbb{N}$ for $\underline{s} \in \underline{S}$ minimal and other components unchanged). The **linear arrow** $A \to S$ is extended to mixed boards in the obvious way.

### C. Cartesian Morphisms

On mixed boards, we may now define cartesian morphisms. 1) **Structural maps:** From now on, fix a mixed board $A$.

**Definition 18.** A structural map $f : x \rightsquigarrow y$, for $x, y \in \mathcal{C}(A)$, is a forest morphism $f : x \to y$ preserving labels.

In Figure 9 we give an example of a structural map, where $q_{3,2}^+$ and $q_{3,6}^+$ are sent to themselves, and the other assignments are forced. Note that all copy indices can be changed freely. The structural map contracts both positive and negative moves, while $q_{3,7}^+$ is not reached – it is regarded as *weakened*.

Structural maps form a category, and one can consider the associated preorder with configurations as elements, and $x \le y$ iff there is some structural map $f : x \rightsquigarrow y$. However, this preorder is not actually the one we need, because it is not compatible with the linear arrow construction of preorders. Indeed, recall that in **ScottL**, the linear arrow was $A \to B = A^{\text{op}} \times B$ contravariant on the left hand side, whereas structural maps on $A \to B$ are covariant on both sides. To recover the appropriate variance, we must account for polarities:

**Definition 19.** Given $f : x \rightsquigarrow y$, we define the conditions:

- **--total:** if $a^+ \in x, f a^+ \to b^-$ in $y$, there is $a^+ \to c^-$ in $x$ s.t. $f c^- = b^-$; for all $b^-$ minimal in $y$ there is $c^-$ in $x$ s.t. $f c^- = b^-$.

- **+total:** if $a^- \in x, f a^- \to b^+$, there is $a^- \to c^+$ in $x$ such that $f c^+ = b^+$,

- **--preserving:** if $a^- \in x$, $\text{ind}_A(f a) = \text{ind}_A a$,

- **+preserving:** if $a^+ \in x$, $\text{ind}_A(f a) = \text{ind}_A a$,

we call a structural map **positive** iff it is $--$preserving and $--$total; we call it **negative** iff it is $+$-preserving and $+$-total. For these notions, we use notations $f : x \rightsquigarrow y$ and $f : x \rightsquigarrow y$.

Positive structural maps can only contract and weaken positive moves, and likewise for negative maps. It follows from the conditions on mixed boards that positive (resp. negative) symmetries are positive (resp. negative) structural maps.

2) **Cartesian morphisms:** Cartesian morphisms take positive maps covariantly and negative maps contravariantly.

**Definition 20.** A cartesian morphism $\chi : x_1 \rightsquigarrow x_n$ is any composite relation, for $x_1, \dots, x_n \in \mathcal{C}(A)$:

$$x_1 \rightsquigarrow x_2 \rightsquigarrow x_3 \dots x_{n-2} \rightsquigarrow x_{n-1} \rightsquigarrow x_n$$

A cartesian morphism $\chi : x \rightsquigarrow y$ is a relation between $x$ and $y$, i.e. $\chi \subseteq x \times y$, but it is in general not functional in either direction. We give in Figure 10 an example cartesian morphism (without the structural maps to alleviate notation).

As we will need to build structural maps gradually, we shall make use of the following **partial** variants:

**Definition 21.** A partial positive map, written $f : x \rightsquigarrow^2 y$, is a structural map satisfying $--$preserving (but not $--$total).

Likewise, a partial negative map, written $f : \rightsquigarrow^2 y$, is a structural map satisfying $+$-preserving (but not $+$-total).

If $R \subseteq A \times B$ is a relation from $A$ to $B$, we write $R^{\perp} \subseteq B \times A$ for the reverse relation. We will also apply this to functions, regarded as functional relations.

**Lemma 3.** Consider $\chi : x \rightsquigarrow^2 z$ a cartesian morphism.

There are unique $y \in \mathcal{C}(A)$, $\chi_- : y \rightsquigarrow x$, $\chi_+ : y \rightsquigarrow z$, s.t. $\chi_+ \circ \chi_- \subseteq \chi$. Additionally, the inclusion is an equality.

In particular, every cartesian morphism $\chi : x \rightsquigarrow^2 y$ can be written uniquely as a relational composition $x \rightsquigarrow \chi_- \rightsquigarrow y$.

### D. Reconstructing the Preorder

From the relational collapse, we must equip the set $\Re(A)$ of positions of $A$ from (7) with a preorder derived from cartesian morphisms. The obvious route is to start by defining it on configurations: for $x, y \in \mathcal{C}(A)$, we set $x \rightsquigarrow y$ iff there is $\chi : y \rightsquigarrow x$, noting the inversion in directions. As symmetries are structural maps and each symmetry has a positive-negative factorization (Lemma 2), this lifts to symmetry classes – we write $x \rightsquigarrow^2 y$ if $x \rightsquigarrow y$ holds for any $x \in x$ and $y \in y$.

**Definition 22.** For any mixed board $A$, $\mathfrak{S}(A) := (\Re(A), \mathfrak{S}^{\perp})$.

This is compatible with all the constructions on preorders involved in the relative Seely structure of **ScottL**. More precisely, the bijections of Figure 6 can be verified to be compatible with the preorder, i.e. to yield preorder-isomorphisms.

## IV. QUALITATIVE COLLAPSE

To generalize this to strategies, the basic idea is simple: we simply take the down-closure of the relational collapse:

$$\mathfrak{S}(\sigma) = [\Re(\sigma)]_{\mathfrak{S}(A)^{\text{op}} \times \mathfrak{S}(B)} \in \text{ScottL}[\mathfrak{S}(A), \mathfrak{S}(B)] \quad (9)$$
<figure><img src="image_12.png" /><figcaption>Fig. 10. A cartesian morphism</figcaption></figure>

It is clear that this is a morphism in **ScottL**, and $\mathfrak{S}(\mathfrak{C}_A) = \text{id}_{\mathfrak{S}(A)}$ for every $A$. We also easily have oplax functoriality:

**Lemma 4.** Consider $A, B$ and $C$ mixed boards, and $\sigma : A \vdash B, \tau : B \vdash C$. Then, $\mathfrak{S}(\tau \odot \sigma) \subseteq \mathfrak{S}(\tau) \circ \mathfrak{S}(\sigma)$.

However, the inequality $\mathfrak{S}(\tau) \circ \mathfrak{S}(\sigma) \subseteq \mathfrak{S}(\tau \odot \sigma)$ is more problematic, and demands an analogue of Proposition 4 for cartesian morphisms. Given $(y_A, y_C) \in \mathfrak{S}(\tau) \circ \mathfrak{S}(\sigma)$, unfolding definitions yields witnesses $x^\sigma \in \mathcal{C}^+(\sigma)$ and $x^\tau \in \mathcal{C}^+(\tau)$ along with a cartesian morphism $\chi : x_B^\sigma \stackrel{\leftrightarrow}{\rightleftharpoons} x_B^\tau$. From this, we want some $y^\tau \odot y^\sigma \in \mathcal{C}^+(\tau \odot \sigma)$ such that $y_A^\sigma \stackrel{\leftrightarrow}{\rightleftharpoons} x_A^\sigma$ and $x_C^\tau \stackrel{\leftrightarrow}{\rightleftharpoons} y_C^\tau$. In the sequel, we shall refer to this data as, respectively, a cartesian (matching) problem, and a solution to the problem. Both strategies are actively trying to duplicate and erase each other, and a solution is a situation where both strategies have reached a state where they have all the resources they need, not more and not less.

**Example 1.** Given $n, m \in \mathbb{N}$, write $\vdash M_\sigma = \lambda f x. f^n x : (o \to o) \to o \to o$ and $g : (o \to o) \to o \to o \vdash M_\tau = \lambda x. g^m x : (o \to o) \to o \to o$, the Church integer for $n$ and $M_\tau$ that for $m$ (on different types). Interpreting those (with a promotion for $M_\sigma$) yields $\sigma \in \text{DSInn}[1, B]$ and $\tau \in \text{DSInn}[B, C]$ with $B = ![(o \to o) \to o \to o]$ and $C = [(o \to o) \to o \to o]$. As events in $B$ in $C$ correspond to atoms in those types, we write $B$ as $(a \to b) \to c \to d$ and $C$ as $(e \to f) \to g \to h$ to ease the correspondence.

The upper part of Figure 11 presents a cartesian problem involving $\sigma$ and $\tau$. On the upper left part, we have the typical (unduplicated) configuration of $\sigma$, displayed onto $B$ as the configuration indicated (omitting copy indices). Likewise, on the upper right corner, we have the typical (unduplicated) configuration of $\tau$, larger than for $\sigma$ because of $\eta$-expansion, displayed to $B$ as shown. There is a cartesian morphism as shown, linking all pairs of moves with the same label.

Resolving this problem involves performing all the necessary duplications: $\tau$ makes $m$ copies of $\sigma$, but the first copy of $\sigma$ makes $n$ copies of the $m-1$ remaining calls of $\sigma$, and so on... The solution appears in the bottom part of the diagram, consisting in the indicated expansions of the configurations of $\sigma$ and $\tau$, whose display on $B$ now match.

The example above illustrates that solving a cartesian problem can involve an exponential blowup in the size of the configurations – indeed, we know that the Church integer for $m$ applied to that for $n$ normalizes to the Church integer for $n^m$, witnessing the $n^m$ calls to the event $f^+$ in the duplicated version of the configuration for $\tau$ in the diagram. In general, the situation is far worse: the size of the solution is not

elementary in the size of the problem, witnessing the usual bounds in the normalization of the simply-typed $\lambda$-calculus.

From this explosion, it is clear that the resolution of a cartesian problem will be non-trivial. In particular, we rely on a non-trivial termination argument, introduced next.

## A. Bounding Interactions

Here we provide an upper bound on the size of solutions to cartesian problems – this relies on earlier work on the size of interactions in Hyland-Ong games [Cla11], [Cla13], [Cla15].

1) **Structural maps in strategies:** Our first step is:

**Definition 23.** For $\sigma : A \vdash B$ and $x^\sigma, y^\sigma \in \mathcal{C}(\sigma)$, a **partial structural map** is a forest morphism $f : x^\sigma \to y^\sigma$ such that $\partial_\sigma f = f_A \vdash f_B$ for $f_A : x_A^\sigma \rightsquigarrow y_A^\sigma$ and $f_B : x_B^\sigma \rightsquigarrow y_B^\sigma$, where $\partial_\sigma f$, the **display** of $f$ to $A \vdash B$, is obtained as

$$x_A^\sigma \vdash x_B^\sigma \stackrel{\partial_\sigma^{-1}}{\approx} x^\sigma \xrightarrow{f} y^\sigma \stackrel{\partial_\sigma}{\approx} y_A^\sigma \vdash y_B^\sigma.$$

We write $f : x^\sigma \rightsquigarrow y^\sigma$. It is a **structural map**, written $f : x^\sigma \rightsquigarrow y^\sigma$, if $f s \to_\sigma t^+$ implies $s \to_\sigma u^+$ s.t. $f(u^+) = t^+$.

Structural maps are contraction maps acting on strategies rather than games. Call a **branch** of $\sigma$ any $\rho_1 \to_\sigma \dots \to_\sigma \rho_n$ with $\rho_1 \in \min(\sigma)$ – write $\text{br}(\sigma)$ for the set of branches of $\sigma$ and $\text{br}(x^\sigma)$ for the branches within $x^\sigma \in \mathcal{C}(\sigma)$. Structural maps automatically send any branch to a symmetric one, i.e. for any $\rho \in \text{br}(x^\sigma)$, $f$ induces a symmetry $f|_{\rho} : \rho \cong_\sigma f \rho$.

2) **The upper bound:** Now fix $\sigma : A \vdash B, \tau : B \vdash C$ with $x^\sigma \in \mathcal{C}(\sigma)$, $x^\tau \in \mathcal{C}(\tau)$ and a cartesian morphism $\chi : x_B^\sigma \stackrel{\leftrightarrow}{\rightleftharpoons} x_B^\tau$. We call the **$\tau$-size** of $(x^\sigma, \chi, x^\tau)$ the minimal $n$ s.t. every branch of $x_A^\sigma \parallel x^\tau$ is smaller than $2n$; its **$\sigma$-size** the minimal $p$ such that every branch of $x^\sigma \parallel x_C^\tau$ is smaller than $2p$; its **depth** the minimal $d+2$ such that every branch of $x_C^\tau$ is smaller than $d+2$, every branch of $x_B^\sigma, x_B^\tau$ is smaller than $d+1$, and every branch of $x_A^\sigma$ is smaller than $d$. Finally, its **branching degree** is the minimal $b$ such that (regarded as trees), $x^\sigma$ and $x^\tau$ have branching degree smaller than $b$. Then:

**Lemma 5.** Consider $(x^\sigma \in \mathcal{C}(\sigma), \chi, x^\tau \in \mathcal{C}(\tau))$ as above with $\tau$-size less than $n \ge 1$, $\sigma$-size less than $p \ge 1$, depth less than $d \ge 3$ and branching degree less than $b \ge 2$.

Then, for any $y^\sigma \in \mathcal{C}(\sigma)$ and $y^\tau \in \mathcal{C}(\tau)$ matching such that there are partial structural maps $\chi^\sigma : y^\sigma \rightsquigarrow x^\sigma, \chi^\tau : y^\tau \rightsquigarrow x^\tau$ with $\chi_A^\sigma : y_A^\sigma \rightsquigarrow x_A^\sigma$ and $\chi_C^\tau : y_C^\tau \rightsquigarrow x_C^\tau$, we have

$$\#(y^\tau \circled{y^\sigma}) \le b^{2d-3} \binom{\frac{p^{n+1}-1}{p-1}-1}{d-1}.$$

$$\text{for } 2_0^k = k \text{ and } 2_k^{n+1} = 2^{2n}.$$
<figure><img src="image_13.png" /><figcaption>Fig. 11. Example resolution of a cartesian matching problem</figcaption></figure>

This is a consequence of [Cla15, Theorem 4.17], exploiting
that a branch of $y^\tau \circled{\circled{y^\sigma}}$ yields a *pointer structure*, i.e. a *P-
visible* and *O-visible* interaction as in *Hyland-Ong* games.

The assumption that $\chi_A^\sigma$ is negative and $\chi_C^\tau$ positive is crucial: it ensures that $y^\sigma$ and $y^\tau$ do not have more duplications by the external Opponent than in $x^\sigma$ and $x^\tau$, so that the upper bound to the branching degree of $x^\sigma, x^\tau$ transports to $y^\sigma, y^\tau$ and to $y^\tau \circled{\circled{y^\sigma}}$. Finally, as $\#y^\sigma \le \#(y^\tau \circled{\circled{y^\sigma}})$ and likewise for $\tau$, the same upper bound applies to $\#y^\sigma$ and $\#y^\tau$.

B. *The Scott Collapse*

1) Solving cartesian problems: We now formally define:

**Definition 24.** Consider $\sigma : A \vdash B$ and $\tau : B \vdash C$. A cartesian (matching) problem is the data of $x^\sigma \in \mathscr{C}(\sigma)$, $x^\tau \in \mathscr{C}(\tau)$ and a cartesian morphism $\chi : x_B^\sigma \bar{\omega} \stackrel{\omega}{\to} x_B^\tau$.

A solution is given by $y^\sigma \in \mathscr{C}(\sigma)$, $y^\tau \in \mathscr{C}(\tau)$, $\chi^\sigma, \chi^\tau$ s.t.:

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

with $\chi_A^\sigma : y_A^\sigma \bar{\omega} \stackrel{\omega}{\to} x_A^\sigma$ and $\chi_C^\tau : y_C^\tau \stackrel{\omega}{\to} x_C^\tau$.

This captures the notion of cartesian matching problem introduced in the introduction. Now, the next key proposition shows how to solve cartesian problems:

**Proposition 5.** Consider $\sigma : A \vdash B$ and $\tau : B \vdash C$.

Then any cartesian problem for $\sigma$, $\tau$ has a unique solution.

Sketch. Existence. Fix $x^\sigma \in \mathscr{C}(\sigma)$, $x^\tau \in \mathscr{C}(\tau)$, $\chi : x_B^\sigma \bar{\omega} \stackrel{\omega}{\to} x_B^\tau$
a cartesian problem. We can find a *partial solution*, i.e. as
above with $\chi^\sigma$, $\chi^\tau$ partial – indeed one can take $y^\sigma = y^\tau = \emptyset$.
Such partial solutions are partially ordered by componentwise
inclusion. By Lemma 5, there is a bound $N \in \mathbb{N}$ on the
cardinal of $y^\tau \circled{\circled{y^\sigma}}$ for partial solutions; thus there is a partial
solution of maximal size. From now on, we fix a partial

solution $y^\sigma, y^\tau, \chi^\sigma, \chi^\tau$ of maximal size; it follows that it is
actually a total solution, as any breach of totality yields an
extension contradicting maximality.

Uniqueness follows easily by deterministic sequential inno-
cence and the fact that $\chi_A^\sigma$ is negative and $\chi_C^\tau$ positive. $\square$

2) A relative Seely functor: The property above is the key conceptual contribution of this work. The functoriality of the collapse to the linear Scott model immediately follows.

**Theorem 7.** We have a relative Seely $\mathfrak{S} : \mathrm{DSInn} \to \mathrm{Scott}$.

The required structural isomorphisms are simply (the down-
closure of) those of Figure 6. Most required conditions are
straightforward, save for the preservation of promotion which
requires some care. As a relative Seely functor, it induces a
cartesian closed functor $\mathfrak{S}$! which therefore preserves the in-
terpretation of the simply-typed $\lambda$-calculus. In other words, for
any $\Gamma \vdash M : A$, $[[M]]_{\mathrm{ScottL}_!} = [s_A] \circ \mathfrak{S}([[[M]]_{\mathrm{DSInn}_!}] \circ [!s_\Gamma])$.

This concludes the link between thin concurrent games and the linear Scott model – which is, again, a cartesian closed subcategory of the usual category of Scott domains. We may now leverage it to study the direct link between the relational model and the linear Scott model, in the spirit of [Ehr12]:

**Theorem 8.** For any $\Gamma \vdash M : A$, $[[M]]_{\text{ScottL}_!} = [[M]]_{\text{Rel}_!}$.

This is direct from their description in terms of $[[M]]_{\text{DSInn}_!}$.

We conclude with a few remarks. Firstly, this is done
with the interpretation of the base type fixed to a singleton
$[[o]] = \{\star\}$. In the full version in supplementary material this is
extended to an arbitrary set. The crux of the argument remains
Proposition 5, but with additional technicalities that we had
to omit because of space limitations. Secondly, this reproves
Ehrhard’s correspondance between qualitative and quantitative
models, not his *extensional collapse* theorem that does not
seem to immediately follow. We do not see it as a limitation,
as we see the link between qualitative and quantitative as the
influential and impactful part of Ehrhard’s paper.

V. CONCLUSIONS

In addition to reproving Ehrhard’s result by different means,
this result is a stepping stone for other work in progress.

The first one is an infinitary extension of Theorem 7, also
accounting for infinitary executions, i.e. infinite configurations;
we believe this result is key to a complete semantic under-
stading of the decidability of higher-order model-checking
[Ong06]. The second one is a bicategorical extension: from
the result therein, it is not too hard to send strategies
to cartesian distributors [Oli21]. If we manage to prove
(pseudo-)functoriality; we could get a bicategorical version of
Ehrhard’s result, leveraging earlier results in [COP23].

ACKNOWLEDGMENT

The author would like to thank Charles Grellois for intense
black board discussions which motivated this development.

REFERENCES

[Aeh06] Klaus Aehlig. A finite semantics of simply-typed lambda terms for infinite runs of automata. In Zoltán Ésik, editor, *Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, September 25-29, 2006, Proceedings*, volume 4207 of *Lecture Notes in Computer Science*, pages 104–118. Springer, 2006. doi:10.1007/11874683\_7.

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

[BDER97] Patrick Baillot, Vincent Danos, Thomas Ehrhard, and Laurent Regnier. Timeless games. In Mogens Nielsen and Wolfgang Thomas, editors, *Computer Science Logic, 11th International Workshop, CSL '97, Annual Conference of the EACSL, Aarhus, Denmark, August 23-29, 1997, Selected Papers*, volume 1414 of *Lecture Notes in Computer Science*, pages 56–77. Springer, 1997. doi:10.1007/BFb0028007.

[BM20] Davide Barbarossa and Giulio Manzonetto. Taylor subsumes scott, berry, kahn and plotkin. *Proc. ACM Program. Lang., 4(POPL):1:1–1:23, 2020*.

[Bou09] Pierre Boudes. Thick subtrees, games and experiments. In Pierre-Louis Curien, editor, *Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009. Proceedings*, volume 5608 of *Lecture Notes in Computer Science*, pages 65–79. Springer, 2009. doi:10.1007/978-3-642-02273-9\_7.

[CCPW18] Simon Castellan, Pierre Clairambault, Hugo Paquet, and Glynn Winskel. The concurrent game semantics of probabilistic PCF. In *LICS*, pages 215–224. ACM, 2018.

[CCRW17] Simon Castellan, Pierre Clairambault, Silvain Rideau, and Glynn Winskel. Games and strategies as event structures. *Log. Methods Comput. Sci.*, 13(3), 2017.

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

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

[Cla11] Pierre Clairambault. Estimation of the length of interactions in arena game semantics. In *FoSSaCS*, volume 6604 of *Lecture Notes in Computer Science*, pages 335–349. Springer, 2011.

[Cla13] Pierre Clairambault. Bounding skeletons, locally scoped terms and exact bounds for linear head reduction. In *TLCA*, volume 7941 of *Lecture Notes in Computer Science*, pages 109–124. Springer, 2013.

[Cla15] Pierre Clairambault. Bounding linear head reduction and visible interaction through skeletons. *Log. Methods Comput. Sci.*, 11(2), 2015.

[Cla24a] Pierre Clairambault. Causal investigations in interactive semantics, 2024. Habilitation à Diriger les Recherches.

[Cla24b] Pierre Clairambault. The qualitative collapse of concurrent games. CoRR, abs/2410.11389, 2024. URL: https://arxiv.org/abs/2410.11389.

[COP23] Pierre Clairambault, Federico Olimpieri, and Hugo Paquet. From thin concurrent games to generalized species of structures. In *38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023, Boston, MA, USA, June 26-29, 2023*, pages 1–14. IEEE, 2023. doi:10.1109/LICS56636.2023.10175681.

[CP21] Pierre Clairambault and Hugo Paquet. The quantitative collapse of concurrent games with symmetry. CoRR, abs/2107.03155, 2021.

[dC18] Daniel de Carvalho. Execution time of λ-terms via denotational semantics and intersection types. *Math. Struct. Comput. Sci.*, 28(7):1169–1203, 2018. doi:10.1017/S0960129516000396.

[Ehr96] Thomas Ehrhard. Projecting sequential algorithms on strongly stable functions. *Ann. Pure Appl. Log.*, 77(3):201–244, 1996. doi:10.1016/0168-0072(95)00026-7.

[Ehr12] Thomas Ehrhard. The scott model of linear logic is the extensional collapse of its relational model. *Theor. Comput. Sci.*, 424:20–45, 2012.

[EPT18] Thomas Ehrhard, Michele Pagani, and Christine Tasson. Full abstraction for probabilistic PCF. *J. ACM*, 65(4):23:1–23:44, 2018. doi:10.1145/3164540.

[FGHW08] Marcelo Fiore, Nicola Gambino, Martin Hyland, and Glynn Winskel. The cartesian closed bicategory of generalised species of structures. *Journal of the London Mathematical Society*, 77(1):203–220, 2008.

[FP09] Claudia Faggian and Mauro Piccolo. Partial orders, event structures and linear strategies. In *TLCA*, volume 5608 of *Lecture Notes in Computer Science*, pages 95–111. Springer, 2009.

[Gir87] Jean-Yves Girard. Linear logic. *Theor. Comput. Sci.*, 50:1–102, 1987. doi:10.1016/0304-3975(87)90045-4.

[Gir88] Jean-Yves Girard. Normal functors, power series and λ-calculus. *Ann. Pure Appl. Log.*, 37(2):129–177, 1988. doi:10.1016/0168-0072(88)90025-5.

[HO00] J. M. E. Hyland and C.-H. Luke Ong. On full abstraction for PCF: i, ii, and III. *Inf. Comput.*, 163(2):285–408, 2000. doi:10.1006/inco.2000.2917.

[Hut93] Michael Huth. Linear domains and linear maps. In Stephen D. Brookes, Michael G. Main, Austin Melton, Michael W. Mislove, and David A. Schmidt, editors, *Mathematical Foundations of Programming Semantics, 9th International Conference, New Orleans, LA, USA, April 7-10, 1993, Proceedings*, volume 802 of *Lecture Notes in Computer Science*, pages 438–453. Springer, 1993. doi:10.1007/3-540-58027-1\_21.

[KO09] Naoki Kobayashi and C.-H. Luke Ong. A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In *Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, 11-14 August 2009, Los Angeles, CA, USA*, pages 179–188. IEEE Computer Society, 2009. doi:10.1109/LICS.2009.29.

[LMMP13] Jim Laird, Giulio Manzonetto, Guy McCusker, and Michele Pagani. Weighted relational models of typed lambda-calculi. In *28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013*, pages 301–310. IEEE Computer Society, 2013. doi:10.1109/LICS.2013.36.

[Mel03] Paul-André Mellies. Asynchronous games 1: Uniformity by group invariance, 2003.

[Mel05] Paul-André Mellies. Asynchronous games 4: A fully complete model of propositional linear logic. In *LICS*, pages 386–395. IEEE Computer Society, 2005.

[Mel06] Paul-André Mellies. Asynchronous games 2: The true concurrency of innocence. *Theor. Comput. Sci.*, 358(2-3):200–228, 2006.

[Mel09] Paul-André Mellies. Categorical semantics of linear logic. *Panoramas et synthèses*, 27:15–215, 2009.

[MM07] Paul-André Mellies and Samuel Mimram. Asynchronous games: Innocence without alternation. In *CONCUR*, volume 4703 of
Lecture Notes in Computer Science, pages 395–411. Springer, 2007.

[NPW79] Mogens Nielsen, Gordon D. Plotkin, and Glynn Winskel. Petri nets, event structures and domains. In Semantics of Concurrent Computation, volume 70 of Lecture Notes in Computer Science, pages 266–284. Springer, 1979.

[Oli21] Federico Olimpieri. Intersection type distributors. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1–15. IEEE, 2021. doi:10.1109/LICS52264.2021.9470617.

[Ong06] C.-H. Luke Ong. On model-checking trees generated by higher-order recursion schemes. In 21st IEEE Symposium on Logic in Computer Science LICS 2006, 12-15 August 2006, Seattle, WA, USA, Proceedings, pages 81–90. IEEE Computer Society, 2006. doi:10.1109/LICS.2006.38.

[Paq22] Hugo Paquet. Bi-invariance for uniform strategies on event structures. In MFPS, 2022.

[PSV14] Michele Pagani, Peter Selinger, and Benoît Valiron. Applying quantitative semantics to higher-order quantum computing. In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 647–658. ACM, 2014. doi:10.1145/2535838.2535879.

[RW11] Silvain Rideau and Glynn Winskel. Concurrent strategies. In LICS, pages 409–418. IEEE Computer Society, 2011.

[SS71] Dana S Scott and Christopher Strachey. Toward a mathematical semantics for computer languages, volume 1. Oxford University Computing Laboratory, Programming Research Group Oxford, 1971.

[Win98] Glynn Winskel. A linear metalanguage for concurrency. In Armando Martin Haeberer, editor, Algebraic Methodology and Software Technology, 7th International Conference, AMAST '98, Amazonia, Brasil, January 4-8, 1999, Proceedings, volume 1548 of Lecture Notes in Computer Science, pages 42–58. Springer, 1998. doi:10.1007/3-540-49253-4\_6.

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