# Strategies as Resource Terms, and their Categorical Semantics

Lison Blondeau-Patissier, Pierre Clairambault, Lionel Vaux Auclair

► To cite this version:

Lison Blondeau-Patissier, Pierre Clairambault, Lionel Vaux Auclair. Strategies as Resource Terms, and their Categorical Semantics. Logical Methods in Computer Science, 2025, 21 (4), 10.46298/lmcs-21(4:9)2025 . hal-05383171

HAL Id: hal-05383171

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

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>

Distributed under a Creative Commons Attribution 4.0 International License
# STRATEGIES AS RESOURCE TERMS, AND THEIR CATEGORICAL SEMANTICS

LISON BLONDEAU-PATISSIER$^{a,b,c}$, PIERRE CLAIRAMBAULT$^{b}$, AND LIONEL VAUX AUCLAIR$^{c}$

**ABSTRACT.** As shown by Tsukada and Ong, simply-typed, normal and $\eta$-long resource terms correspond to plays in Hyland-Ong games, quotiented by Melliès' homotopy equivalence. The original proof of this inspiring result is indirect, relying on the injectivity of the relational model with respect to both sides of the correspondence – in particular, the dynamics of the resource calculus is taken into account only *via* the compatibility of the relational model with the composition of normal terms defined by normalization.

In the present paper, we revisit and extend these results. Our first contribution is to restate the correspondence by considering causal structures we call *augmentations*, which are canonical representatives of Hyland-Ong plays up to homotopy. This allows us to give a direct and explicit account of the connection with normal resource terms. As a second contribution, we extend this account to the *reduction* of resource terms: building on a notion of strategies as weighted sums of augmentations, we provide a denotational model of the resource calculus, invariant under reduction. A key step – and our third contribution – is a categorical model we call a *resource category*, which is to the resource calculus what differential categories are to the differential $\lambda$-calculus.

## 1. INTRODUCTION

The *Taylor expansion* of $\lambda$-terms translates programs with possibly infinite behaviour to infinite formal sums of terms of a language with a strongly finitary behaviour called the *resource calculus*. Its discovery dates back to Ehrhard and Regnier's *differential $\lambda$-calculus* [ER03], reifying syntactically the features of particular models of linear logic

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

<footnote>a ENS de Lyon, CNRS, Université Claude Bernard Lyon 1, LIP, Lyon, France
*e-mail address*: lison.blondeau-patissier@ens-lyon.org</footnote>

<footnote>b Aix Marseille Univ, CNRS, LIS, Marseille, France
*e-mail address*: pierre.clairambault@cnrs.fr</footnote>

<footnote>c Aix-Marseille Univ, CNRS, I2M, Marseille, France
*e-mail address*: lionel.vaux@univ-amu.fr</footnote>

<footnote n="2012">2012 *ACM CCS*: Theory of computation → Denotational semantics, Categorical semantics.</footnote>

<footnote>Key words and phrases: Resource calculus, Game semantics, Categorical semantics.</footnote>

<footnote>* This paper is an extended version of [BCVA23b].</footnote>

<footnote>*Pierre Clairambault*: Supported by the ANR projects DyVerSe (ANR-19-CE48-0010-01) and by the Labex MiLyon (ANR-10-LABX-0070) of Université de Lyon.</footnote>

<footnote>Lionel Vaux Auclair: Supported by the ANR projects PPS (ANR-19-CE48-0014), LambdaComb (ANR-21-CE48-0017) and Reciprog (ANR-21-CE48-0019).</footnote>
where types are interpreted as particular topological vector spaces, and proofs as linear and continuous maps between them. Since its inception [ER08], Taylor expansion was intended as a quantitative alternative to order-based approximation techniques, such as Scott continuity and Böhm trees. For instance, Barbarossa and Manzonetto leveraged it to get simpler proofs of known results in pure λ-calculus [BM20].

*Game semantics* is another well-established line of work, also representing programs as collections of finite behaviours. It is particularly well known for its many full abstraction results [HO00, AJM00]. How different is the Taylor expansion of the λ-calculus from its game semantics? Not very different, suggest Tsukada and Ong [TO16], who show that certain normal and η-long resource terms correspond bijectively to plays in the sense of Hyland-Ong game semantics [HO00], up to Opponent's scheduling of the independent explorations of separate branches of the term, as formalized by Melliès' homotopy equivalence on plays [Mel06].

The account of this insightful result by Tsukada and Ong is inspiring, but it also comes with limitations. Their focus is on normal resource terms, and the dynamics is treated only in the form of the composition of terms, *i.e.* substitution followed by normalization. The correspondence is also very indirect, relying on the injectivity of the relational model w.r.t. both normal resource terms and plays up to homotopy. In [TO16], after laying out the intuitions supporting the correspondence, Tsukada and Ong motivate this indirect route, writing: "The idea will now be intuitively clear. However the definition based on the above argument, which heavily depends on graphical operations, does not seem so easy to handle."

In the present paper, we handle this very task. We rely on a representation of plays quotienting out Opponent's scheduling, recently introduced by the first two authors [BC21]. This was inspired by concurrent games [CCRW17] – similar causal structures existed before, first suggested in [Lai05], and fleshed out more in [ST17]. In [BC21], plays are replaced by so-called *augmentations*, which * augment * valid states of the game with causal constraints imposed by the program. Our first contribution is an explicit description of the bijection between normal resource terms and isomorphism classes of augmentations (called *isoglementations*, for the sake of brevity), in a style similar to traditional finite definability arguments.

We moreover strive to account for non-normal resource terms and *reduction* in the resource calculus. In game semantics, this typically relies on a category of strategies, whose composition is defined by interaction between plays. Considering the interaction of augmentations – which was not addressed in [BC21] – an interesting phenomenon occurs. Indeed, there is no canonical way to *synchronize* two augmentations: they can only interact *via* a mediating map, called a *symmetry*, and the result of the interaction depends on the chosen symmetry! Composition is then obtained by summing over all symmetries. This is not an artificial phenomenon arising from our implementation choices: it is analogous to the non-determinism inherent to the substitution of resource terms. And this is instrumental in our second contribution: the correspondence between normal resource terms and isoglementations refines into a denotational interpretation, invariant under reduction, of resource terms as “strategies” – weighted sums of isoglementations.

To establish this result we expose the structure of the category of strategies that is relevant to obtain a model of the resource calculus: we call *resource categories* the resulting categorical model, which is our third contribution. We then show that strategies indeed form a resource category, completing the proof of the previous point.
**Related and future work.** As mentioned above, Tsukada and Ong [TO16] considered some dynamic aspects of the correspondence: they proved their bijection is compatible with the compositions of terms and plays, *via* composition in the relational model. Nonetheless, they did not consider an interpretation of *non-normal* resource terms as strategies: the question of invariance under reduction could not even be formulated, and the relevant structure of the category of strategies could not be exposed. Still, they state that the normal form of the Taylor expansion of a λ-term is isomorphic to its game semantics.

Our contributions in the present paper constitute a first step to flesh out this isomorphism into the commuting diagrams:

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

where $M$ is a λ-term, $s$ is a resource term, $\mathcal{T}$ is Taylor expansion, $\mathcal{N}$ is normalization and $\llbracket - \rrbracket$ is game semantics. The main outcome of this paper is to establish the commutation of $(c)$, which appears in our paper under the form of Corollary 7.4 – here, $\simeq$ is the bijection between weighted sums of normal resource terms and strategies, obtained by lifting to weighted sums our bijection between normal resource terms and isoglementations. The commutation of $(b)$ follows just using the linearity of $\llbracket - \rrbracket$ and $\mathcal{N}$. In contrast, $(a)$ does not follow from this paper. We expect that it should be derived from the inductive definitions of both Taylor expansion and the game semantics interpretation, showing that the interpretation of each $(\eta$-long) λ-term constructor matches the Taylor expansion of that constructor; but we prefer to keep this paper focused on the finitary resource calculus, so we leave that for future work (see also the next paragraphs and section 8).

A significant aspect of our contributions is to take coefficients into account. This is far from anecdotal: it requires new methods (we cannot get that *via* the relational model), it makes the development significantly more complex, and it is necessary if one expects to apply these tools to a quantitative setting (e.g., with probabilities) and to provide the basis of a full game semantical account of quantitative Taylor expansion.

The exact relationship between differential categories [BCS06, BCLS20] and resource categories is the subject of ongoing work. The construction of a resource category from a differential category (more precisely, from an additive monoidal storage category with codereliction [BCLS20]) has been exposed by the first author [Blo24], although the proposed construction does not preserve closure. The reverse direction is less clear. Indeed, let us stress the fact that the resource calculus is the finitary fragment of the differential λ-calculus: it does not contain the pure λ-calculus. Accordingly, models of the resource calculus are rather related to those of promotion-free differential linear logic [ER06]: the exponential modality (!) need not be a comonad. From such a model, one can recover an interpretation of the full differential λ-calculus *via* Taylor expansion, *provided the necessary infinite sums are available*. So we are convinced (see our concluding remarks in section 8) that our category of games does induce a cartesian closed differential category [BCS09, BEM10, Man12]; more generally, we plan to study how this generalizes to any resource category – provided the necessary sums of morphisms are available.

**Outline of the paper.** After introducing preliminary notations in section 2, we review the resource calculus in section 3; in particular, we consider a simply typed version whose normal
forms are $\eta$-long, meaning that each variable is fully applied. In section 4 we introduce augmentations, and show that normal resource terms are in bijective correspondence with isoglementations i.e. isomorphism classes of augmentations. We moreover introduce a category of strategies, which are weighted sums of isoglementations, in section 5. In section 6 we introduce resource categories, define the interpretation of the resource calculus in a resource category, and prove that it is invariant under reduction. We then show that strategies form a resource category in section 7; we moreover show in subsection 7.3 that, up to the bijection between normal terms and isoglementations, the interpretation of resource terms as strategies coincides with normalization. In section 8, we conclude by discussing the role and side-effects of $\eta$-expansion in the resource calculus, in the light of game semantics and Taylor expansion.

**Differences with the conference version.** A short version of this article [BCVA23b] was published in the proceedings of the FSCD 2023 conference [GvR23]. Compared with that former version, the present paper provides a more detailed account of our constructions, and technical lemmas that were previously left out are included in appendices. Moreover, the resource calculus we consider is slightly different: instead of fully applying each variable and each redex, as was also done by Tsukada and Ong [TO16], we only impose this constraint on variables. It turns out that this simplifies the exposition, and still yields the same $\eta$-long normal forms.

## 2. PRELIMINARIES ON TUPLES AND BAGS

If $X$ is a set, we write $X^*$ for the set of finite lists, or tuples, of elements of $X$, ranged over by $\vec{a}, \vec{b}$, etc. We write $\vec{a} = \langle a_1, \dots, a_n \rangle$ to list the elements of $\vec{a}$, of length $|\vec{a}| = n$. The empty list is $\langle \rangle$, and concatenation is simply juxtaposition, e.g., $\vec{a}\vec{b}$.

We write $\mathcal{B}(X)$ for the set of finite multisets of elements of $X$, which we call **bags**, ranged over by $\vec{a}, \vec{b}$, etc. We write $\vec{a} = [a_1, \dots, a_n]$ for the bag induced by the list $\vec{a} = \langle a_1, \dots, a_n \rangle$ of elements: we then say $\vec{a}$ is an **enumeration** of $\vec{a}$ in this case. We write $\llbracket \rrbracket$ for the empty bag, and use $*$ for bag concatenation. We also write $|\vec{a}|$ for the length of $\vec{a}$, i.e. the length of any enumeration of $\vec{a}$.

We shall often need to *partition* bags, which requires some care. For $\vec{a} \in \mathcal{B}(X)$ and $k \in \mathbb{N}$, a **k-partitioning** of $\vec{a}$ is a function $p : \{1, \dots, |\vec{a}|\} \to \{1, \dots, k\}$: we write $p : \vec{a} \prec k$. Given an enumeration $\langle a_1, \dots, a_n \rangle$ of $\vec{a}$, the associated **k-partition** is the tuple $\langle \vec{a} \upharpoonright_p 1, \dots, \vec{a} \upharpoonright_p k \rangle$, where we set $\vec{a} \upharpoonright_p i = [a_j \mid p(j) = i]$ for $1 \le i \le k$, so that $\vec{a} = \vec{a} \upharpoonright_p 1 * \dots * \vec{a} \upharpoonright_p k$. The obtained k-partition does depend on the chosen enumeration of $\vec{a}$ but, for any function $f : \mathcal{B}(X)^k \to \mathcal{M}$ with values in a commutative monoid $\mathcal{M}$ (noted additively), the finite sum

$$ \sum_{\vec{a} \prec \vec{a}_1 * \dots * \vec{a}_k} f(\vec{a}_1, \dots, \vec{a}_k) \stackrel{\text{def}}{=} \sum_{p : \vec{a} \prec k} f(\vec{a} \upharpoonright_p 1, \dots, \vec{a} \upharpoonright_p k) \in \mathcal{M} \quad (2.1) $$

is independent from the enumeration. When indexing a sum with $\vec{a} \prec \vec{a}_1 * \dots * \vec{a}_k$ we thus mean to sum over all partitionings $p : \vec{a} \prec k$, using $\vec{a}_i$ as a shorthand for $\vec{a} \upharpoonright_p i$ in each summand.

We will also consider tuples of bags: we write $S(X)$ for $\mathcal{B}(X)^*$. We denote elements of $S(X)$ as $\vec{a}, \vec{b}$, etc. just like for plain tuples, but we reserve the name **sequence** for such tuples of bags.
$$ \Delta \ni s, t, u, \dots ::= x \mid \lambda x.s \mid s \bar{t} \\ \mathcal{B}(\Delta) \ni \bar{s}, \bar{t}, \bar{u}, \dots ::= [s_1, \dots, s_n] $$

<caption>Figure 1: Syntax of the resource calculus: resource terms and resource bags</caption>

$$ \begin{align*} y\langle\bar{t}/x\rangle &\stackrel{\text{def}}{=} \begin{cases} t & \text{if } y = x \text{ and } \bar{t} = [t] \\ y & \text{if } y \neq x \text{ and } \bar{t} = [] \\ 0 & \text{otherwise} \end{cases} \\ (\lambda z.s)\langle\bar{t}/x\rangle &\stackrel{\text{def}}{=} \lambda z.s\langle\bar{t}/x\rangle \\ (s \bar{u})\langle\bar{t}/x\rangle &\stackrel{\text{def}}{=} \sum_{\bar{t} < \bar{t}_1 * \bar{t}_2} (s\langle\bar{t}_1/x\rangle)(\bar{u}\langle\bar{t}_2/x\rangle) \\ [s_1, \dots, s_n]\langle\bar{t}/x\rangle &\stackrel{\text{def}}{=} \sum_{\bar{t} < \bar{t}_1 * \dots * \bar{t}_n} [s_1\langle\bar{t}_1/x\rangle, \dots, s_n\langle\bar{t}_n/x\rangle] \end{align*} $$

<caption>Figure 2: Inductive definition of substitution ($z$ is chosen fresh in the abstraction case)</caption>

### 3. THE SIMPLY-TYPED η-EXPANDED RESOURCE CALCULUS

**Resource calculus.** The terms of the resource calculus [ER08], called **resource terms**, are just like ordinary $\lambda$-terms, except that the argument in an application is a bag of terms instead of just one term. We recall the syntax in Figure 1: we denote resource terms by $s, t, u$, and bags of terms, which we call **resource bags**, by $\bar{s}, \bar{t}, \bar{u}$, possibly with sub- and superscripts, and write $\Delta$ for the set of terms.

The dynamics relies on a multilinear variant of substitution, that we will call **resource substitution**: a redex $(\lambda x.s)\bar{t}$ reduces to a formal finite sum $s\langle\bar{t}/x\rangle$ of terms, each summand being obtained by substituting each element of $\bar{t}$ for exactly one occurrence of $x$ in $s$. The inductive definition is in Figure 2, relying on an extension of syntactic constructs to finite sums of expressions:

$$ \lambda x.S \stackrel{\text{def}}{=} \sum_{i \in I} \lambda x.s_i \quad [S] * \bar{T} \stackrel{\text{def}}{=} \sum_{i \in I} \sum_{j \in J} [s_i] * \bar{t}_j \quad S \bar{T} \stackrel{\text{def}}{=} \sum_{i \in I} \sum_{j \in J} s_i \bar{t}_j, $$

for $S = \sum_{i \in I} s_i$ and $\bar{T} = \sum_{j \in J} \bar{t}_j$. Note that the application (resp. bag) case in Figure 2 uses the notation introduced in (2.1), the target commutative monoid being the set of formal finite sums of resource terms (resp. of resource bags). Also note that the definition of $[s_1, \dots, s_n]\langle\bar{t}/x\rangle$ does not depend on the chosen enumeration $\langle s_1, \dots, s_n \rangle$. Resource substitution is in turn extended by linearity, setting $S\langle\bar{T}/x\rangle \stackrel{\text{def}}{=} \sum_{i \in I} \sum_{j \in J} s_i \langle\bar{t}_j/x\rangle$ with the same notations as above.

The actual protagonists of the calculus are thus sums of terms rather than single terms. We will generally write $\Sigma(X)$ for the set of finite formal sums on set $X$ – one may equivalently consider $\Sigma(X)$ as the free $\mathbb{N}$-module generated by $X$ and define sums by taking (finite) linear combinations of elements of $X$, with weights in $\mathbb{N}$, but any such linear combination can be written as a plain sum; those may also be considered as finite multisets, but we adopt a distinct additive notation to avoid confusion with bags.
$$ \frac{\bar{t} \rightsquigarrow \bar{T}'}{s \bar{t} \rightsquigarrow s \bar{T}'} \qquad \frac{s \rightsquigarrow S'}{s \bar{t} \rightsquigarrow S' \bar{t}} \qquad \frac{s \rightsquigarrow S'}{[s] * \bar{t} \rightsquigarrow [S'] * \bar{t}} \qquad \frac{\lambda x.s \rightsquigarrow \lambda x.S'}{\lambda x.s \rightsquigarrow \lambda x.S'} \qquad \frac{\bar{t} \rightsquigarrow \bar{T}'}{\bar{t} \rightsquigarrow \bar{T}} $$

<caption>Figure 3: Rules of resource reduction</caption>

The **reduction of resource terms** $\rightsquigarrow \subseteq \Delta \times \Sigma(\Delta)$ is defined inductively by the rules of Figure 3 – simultaneously with the reduction of resource bags $\rightsquigarrow \subseteq \mathcal{B}(\Delta) \times \Sigma(\mathcal{B}(\Delta))$. It is extended to $\rightsquigarrow \subseteq \Sigma(\Delta) \times \Sigma(\Delta)$ by setting $S \rightsquigarrow S'$ whenever $S = t + U$ and $S' = T' + U$ with $t \rightsquigarrow T'$.

**Theorem 3.1** [ER08]. *The reduction $\rightsquigarrow$ on $\Sigma(\Delta)$ is confluent and strongly normalizing.*

**Typing and $\eta$-long terms.** In the remainder of the paper, we will consider a simply typed version of the resource calculus, based on the usual grammar of types

$$ A, B, \dots ::= o \mid A \to B $$

with a single base type $o$. If $\vec{A} = \langle A_1, \dots, A_n \rangle$, we write $\vec{A} \to B \stackrel{\text{def}}{=} A_1 \to \dots \to A_n \to B = A_1 \to (\dots \to (A_n \to B) \dots)$. Then any type $C$ can be written uniquely as $C = \vec{A} \to o$.

The above strong normalization result holds in the untyped setting. We use typing only to enforce a syntactic constraint on terms, ensuring that normal resource expressions are in $\eta$-long form: normal terms of type $\vec{A} \to o$ will necessarily have the shape $\lambda x_1 \dots \lambda x_{|\vec{A}|} s$ with $s$ a normal term of type $o$, which must then be a fully applied variable. This is required to obtain an exact correspondence between normal terms and isoglementations, because game semantics is inherently extensional.

We fix a type for each variable, so that each type has infinitely many variables, and write $x : A$ when $A$ is the type of $x$. A typing context $\Gamma$ is a finite set of typed variables. As usual we write it as any enumeration $x_1 : A_1, \dots, x_n : A_n$, abbreviated as $\vec{x} : \vec{A}$; we may then also write $\lambda \vec{x}. s \stackrel{\text{def}}{=} \lambda x_1 \dots \lambda x_n s$.

We call **resource sequence** any sequence $\vec{s} \in \mathcal{S}(\Delta) = \mathcal{B}(\Delta)^*$. Given a term $s$ and a resource sequence $\vec{t} = \langle \vec{t}_1, \dots, \vec{t}_k \rangle$, we also define the application $s \vec{t} \stackrel{\text{def}}{=} s \vec{t}_1 \cdots \vec{t}_k = (\cdots(s \vec{t}_1) \cdots) \vec{t}_k$. We extend resource substitution to sequences by setting

$$ \langle \bar{s}_1, \dots, \bar{s}_n \rangle \langle \bar{t}/x \rangle \stackrel{\text{def}}{=} \sum_{\vec{t} \prec \vec{t}_1 * \dots * \vec{t}_n} \langle \bar{s}_1 \langle \bar{t}_1/x \rangle, \dots, \bar{s}_n \langle \bar{t}_n/x \rangle \rangle $$

so that $(s \vec{u}) \langle \bar{t}/x \rangle = \sum_{\vec{t} \prec \vec{t}_1 * \dots * \vec{t}_2} (s \langle \bar{t}_1/x \rangle) (\vec{u} \langle \bar{t}_2/x \rangle)$, which generalizes the application case of Figure 2.

The type system is given in Figure 4: this is a straightforward adaptation of the usual simple type system for the ordinary $\lambda$-calculus, where bags are typed uniformly (all the elements of a bag share the same type), with the additional requirement that variables are fully applied. Note that there are three kinds of judgements: $\Gamma \vdash_{\mathrm{Tm}} s : A$ for terms, $\Gamma \vdash_{\mathrm{Bg}} \bar{s} : A$ for bags, and $\Gamma \vdash_{\mathrm{Sq}} \vec{s} : \vec{A}$ for sequences. For $X \in \{\mathrm{Tm}, \mathrm{Bg}, \mathrm{Sq}\}$, we write $X(\Gamma; A)$ for the set of those expressions $s$ $s.t. \Gamma \vdash_X s : A$. We moreover write $X_{\mathrm{nf}}(\Gamma; A)$ for the elements of $X(\Gamma; A)$ that are in normal form.

**Lemma 3.2.** *We have $s \in X_{\mathrm{nf}}(\Gamma; A)$ iff $\Gamma \vdash_X s : A$ is derivable without using the application rule (app).*
$$ \frac{\Gamma, x : A \vdash_{\mathfrak{Tm}} s : B}{\Gamma \vdash_{\mathfrak{Tm}} \lambda x.s : A \to B} \quad \text{(abs)} $$

$$ \frac{\Gamma \vdash_{\mathfrak{Tm}} s : A \to B \quad \Gamma \vdash_{\mathfrak{Bg}} \bar{t} : A}{\Gamma \vdash_{\mathfrak{Tm}} s \bar{t} : B} \quad \text{(app)} $$

$$ \frac{\Gamma, x : \vec{A} \to o \vdash_{\mathfrak{Sq}} \vec{t} : \vec{A}}{\Gamma, x : \vec{A} \to o \vdash_{\mathfrak{Tm}} x \vec{t} : o} \quad \text{(var)} $$

$$ \frac{\Gamma \vdash_{\mathfrak{Tm}} s_1 : A \quad \dots \quad \Gamma \vdash_{\mathfrak{Tm}} s_n : A}{\Gamma \vdash_{\mathfrak{Bg}} [s_1, \dots, s_n] : A} \quad \text{(bag)} $$

$$ \frac{\Gamma \vdash_{\mathfrak{Bg}} \bar{s}_1 : A_1 \quad \dots \quad \Gamma \vdash_{\mathfrak{Bg}} \bar{s}_n : A_n}{\Gamma \vdash_{\mathfrak{Sq}} \langle \bar{s}_1, \dots, \bar{s}_n \rangle : \langle A_1, \dots, A_n \rangle} \quad \text{(seq)} $$

<caption>Figure 4: Typing rules for the simply-typed η-long resource calculus</caption>

*Proof.* Given a derivation tree for $\Gamma \vdash_X s : A$ using rule (app) at least once, consider a minimal subderivation with this property: it must have an instance of (app) at its root, and its premises are derived without (app). The left premise must thus be derived by (abs): we have ruled out (app), and the conclusion of (var) is never an arrow type. We thus obtain a redex. □

**Corollary 3.3.** If $s \in \mathfrak{Tm}_{nf}(\Gamma; A \to B)$, then we can write $s = \lambda x.t$ with $x : A$ and $t \in \mathfrak{Tm}_{nf}(\Gamma, x : A; B)$. And if $s \in \mathfrak{Tm}_{nf}(\Gamma; o)$, then we can write $s = y \vec{u}$ with $y : \vec{C} \to o \in \Gamma$ and $\vec{u} \in \mathfrak{Sq}_{nf}(\Gamma; \vec{C})$.

Now we extend the type system to finite sums of terms, by setting $\Gamma \vdash_X \sum_{i \in I} s_i : A$ if $\Gamma \vdash_X s_i : A$ for each $i \in I$; and we write $\Sigma X(\Gamma; A)$ for $\Sigma(X(\Gamma; A))$. This type system enjoys subject reduction w.r.t. $\rightsquigarrow$. As is usual, the key result for subject reduction is a substitution lemma.

**Lemma 3.4.** If $s \in \mathfrak{X}(\Gamma, x : B; A)$ and $\bar{t} \in \mathfrak{Bg}(\Gamma; B)$ then $s \langle \bar{t}/x \rangle \in \Sigma \mathfrak{X}(\Gamma; A)$.

*Proof.* Straightforward, by mutual induction on the three syntactic kinds. □

**Lemma 3.5 (Subject reduction).** If $S \in \Sigma X(\Gamma; A)$ and $S \rightsquigarrow S'$ then $S' \in \Sigma X(\Gamma; A)$.

*Proof.* We first treat the case of $S = s \in \mathfrak{X}(\Gamma; A)$ by induction on the definition of the reduction $s \rightsquigarrow S'$: the case of a redex is by the substitution lemma, and the other cases follow by contextuality. The extension to sums is straightforward. □

Note that for the rest of this paper, all the resource terms we consider will be typed in the system above. By normal resource term, we will thus always mean normal η-long typed resource term.

# 4. RESOURCE TERMS AS AUGMENTATIONS

Game semantics represents programs by recording all their interactions with an execution environment. This is formalized in a game-theoretic language: a program is represented as a strategy in a two-player game. The first player (corresponding to the program under scrutiny) is called *Player*, associated with the *positive* polarity; while the second (corresponding to the execution environment) is called *Opponent*, associated with the *negative* polarity.
<figure><img src="image_4.png" /><figcaption>Figure 5: Two homotopic plays in HO games</figcaption></figure>

**Plays in game semantics.** In Hyland-Ong game semantics [HO00], this leads to a formalization of executions as *plays*, drawn in diagrams such as in Figure 5, read temporally from top to bottom. Nodes are called *moves* or *events*, negative (from Opponent) or positive (from Player) – each corresponds to a resource call, and the dotted lines, called *justification pointers*, carry the hierarchical relationship between those calls.

Both diagrams in Figure 5 represent plays for a simply typed λ-term of the shape

$$ \vdash \lambda f (o \to o) \to (o \to o) \to o . f (\lambda x^o . x) (\lambda y^o . f M_1 M_2) : ((o \to o) \to (o \to o) \to o) \to o $$

with $M_1, M_2$ unspecified terms of type $o \to o$ (in which $y$ and $f$ may occur free). For instance, the first diagram of Figure 5 reads as follows: Opponent starts computation with the initial $q^-$, to which Player reacts with the first $q^+$, corresponding to calling $f$. With $q^-$ on the third line, Opponent prompts $f$ to inspect its first argument, to which Player responds with $q^+$ on the fourth line, corresponding to a call to $x$. Subsequently, Opponent evaluates the second argument of $f$, which also has a head occurrence of $f$: Player thus answers by calling $f$ again but, this time, Opponent does not inspect the arguments $M_1$ and $M_2$ fed to $f$. Instead, Opponent evaluates the first argument of the first call to $f$ again. This addresses the same subterm as the third move, and so Player reacts as before (the fact that Player *must* react in the same way, if the program under scrutiny is pure, corresponds to the notion of *innocence* in Hyland-Ong games). The second diagram of Figure 5 is very similar, the only difference being that Opponent starts with evaluating twice the first argument of $f$, and then evaluates the second one.

**Plays and resource terms.** In [TO16], seeking a syntactic counterpart to the *plays* of HO games, Tsukada and Ong state: “*plays in HO/N-games are terms of a well-known and important calculus, the resource calculus*”. This is natural as both game semantics and the resource calculus are quantitative and represent resource usage explicitly. In the first play of Figure 5, the first argument of the first call to $f$ is evaluated *twice* while the second one is evaluated *once*; and none of the arguments to the second call to $f$ is evaluated: this play is accordingly identified with the resource term

$$ \vdash_{Tm} \lambda f . f [\lambda x.x, \lambda x.x] [\lambda y.f []] : ((o \to o) \to (o \to o) \to o) \to o. \quad (4.1) $$

However, the other play of Figure 5 *also* corresponds to that resource term!

Tsukada and Ong actually establish a bijection between (simply typed, normal and $\eta$-long) resource terms and plays *up to* Melliès' *homotopy relation* [Mel06], relating plays which, like those of Figure 5, only differ via Opponent's scheduling.
<figure><img src="image_5.png" /><figcaption>Figure 6: An augmentation</figcaption></figure>

The quotient of plays up to homotopy equivalence can be given an explicit representation. In [BC21], Blondeau-Patissier and Clairambault introduced a *causal* representation of innocent strategies (inspired from concurrent games [CCRW17, CCW19] – see also [ST17]) as a technical tool to prove a positional injectivity theorem for innocent strategies. There, a strategy is not a set of plays, but instead gathers diagrams such as in Figure 6, in which the trained eye can read exactly the same data as in the resource term (4.1): the model replaces the chronological *plays* of game semantics with causal structures called *augmentations*, of which the plays are just particular linearizations. Thus as the first contribution of this paper, we recast Tsukada and Ong’s correspondence as a bijection between normal resource terms and augmentations.

**4.1. Arenas, Configurations, Augmentations.** Before defining augmentations (and their isomorphism classes, isoglementations), we need to introduce arenas and configurations (and their isomorphism classes, positions). As with HO games, arenas correspond to types: they represent sets of available computational events for Opponent and Player given the type, and they feature a static hierarchy between events, playing a similar role to the enabling relation of HO arenas. Positions, i.e. configurations up to symmetry, are the collapse of plays in the relational model: configurations feature only events along with a static causal order representing the hierarchical dependencies between function calls, without any temporal information. Finally, augmentations are configurations “augmented” with another, dynamic causal order, corresponding to the causal links appearing in normal resource terms – akin to finite Böhm-like trees [Bar84, Section 10.1].

**Arenas.** First we introduce the representation of types: arenas. Given a poset $A = \langle |A|, \le_A \rangle$, we write $\min(A)$ (resp. $\max(A)$) for the set of its minimal (resp. maximal) elements; and we write $a_1 \to_A a_2$ when $a_1 <_A a_2$ with no element strictly in between ($a_1$ is immediately below $a_2$). We call forest any poset $A$ such that the principal ideal $\{a' \in |A| \mid a' \le_A a\}$ of each $a \in |A|$ is finite and linearly ordered by $\le_A$.

**Definition 4.1.** An arena is a triple $A = \langle |A|, \le_A, \text{pol}_A \rangle$ where $\langle |A|, \le_A \rangle$ is a (countable) forest, and $\text{pol}_A : |A| \to \{-, +\}$ is a polarity function, which is

alternating: for all $a_1 \to_A a_2$, $\text{pol}_A(a_1) \neq \text{pol}_A(a_2)$.

In a negative arena, we moreover require $\text{pol}_A(a) = -$ for all $a \in \min(A)$.
<figure><img src="image_6.png" /><figcaption>Figure 7: The arena $\llbracket ((o \to o) \to (o \to o) \to o) \to o \rrbracket$</figcaption></figure>

Elements of $|A|$ are called **events** or **moves** interchangeably. An **isomorphism** $\varphi: A \cong B$ of arenas is a bijection between events preserving and reflecting all the structure.

Arenas present computational events with their causal dependencies: positive moves for Player, and negative moves for Opponent. We often annotate moves with their polarity. When depicting arenas we draw the immediate causality $\to$ as dotted lines, read from top to bottom. The (negative) arena corresponding to the type $((o \to o) \to (o \to o) \to o) \to o$ is depicted in Figure 7: we present the construction of the arena $\llbracket A \rrbracket$ associated with a type A in the next paragraph.

**Constructions.** To interpret elaborate datatypes, we define some constructors on arenas. We write $X + Y$ for the disjoint union $(\{1\} \times X) \cup (\{2\} \times Y)$ of sets.

**Definition 4.2.** The tensor of arenas $A_1$ and $A_2$ is defined as follows:

$$ 
\begin{array}{lclcl}
|A_1 \otimes A_2| & \stackrel{\text{def}}{=} & |A_1| + |A_2| & & \\
(i, a) \leq_{A_1 \otimes A_2} (j, b) & \stackrel{\text{def}}{\iff} & i = j \land a \leq_{A_i} b & & \\
\text{pol}_{A_1 \otimes A_2}(i, a) & \stackrel{\text{def}}{=} & \text{pol}_{A_i}(a). & &
\end{array}
$$

An arena A is **pointed** if it has exactly one minimal event, written $\text{init}(A)$. The tensor directly extends to countable arity, and each arena decomposes as $A \cong \otimes_{i \in \min(A)} A_i$ with each $A_i$ pointed with $\text{init}(A_i) = i$. We set $A^{\perp}$ as A with polarities reversed, and write $A \vdash B$ for $A^{\perp} \otimes B$. The arena $A \vdash B$, called the **hom-game**, is the ambient game for strategies from A to B. However, it is not negative and hence will fail to be an object of our category. To reinstate negativity we must ensure an additional dependency, as done in the arrow construction below:

**Definition 4.3.** If $A_1$ and $A_2$ are negative arenas with $A_2$ pointed, then the **arrow** $A_1 \Rightarrow A_2$ is the pointed negative arena defined as follows:

$$ 
\begin{array}{lclcl}
|A_1 \Rightarrow A_2| & \stackrel{\text{def}}{=} & |A_1| + |A_2| & & \\
(i, a) \leq_{A_1 \Rightarrow A_2} (j, b) & \stackrel{\text{def}}{\iff} & (i = j \land a \leq_{A_i} b) \lor (i, a) = (2, \text{init}(A_2)) & & \\
\text{pol}_{A_1 \Rightarrow A_2}(1, a) & \stackrel{\text{def}}{=} & -\text{pol}_{A_1}(a) & & \\
\text{pol}_{A_1 \Rightarrow A_2}(2, a) & \stackrel{\text{def}}{=} & \text{pol}_{A_2}(a). & &
\end{array}
$$

We shall also use the generalization of this construction to $A \Rightarrow B$ for $B$ not necessarily pointed. In that case, writing $B \cong \otimes_{i \in \min(B)} B_i$, we set $A \Rightarrow B = \otimes_{i \in \min(B)} A \Rightarrow B_i$.

Finally, 1 is the empty arena and $o$ has exactly one (negative) move $q$. We interpret types as arenas via $\llbracket o \rrbracket = o$ and $\llbracket A \to B \rrbracket = \llbracket A \rrbracket \Rightarrow \llbracket B \rrbracket$, and contexts via $\llbracket \Gamma \rrbracket = \otimes_{(x:A) \in \Gamma} \llbracket A \rrbracket$.
As announced, Figure 7 shows the interpretation of $((o \to o) \to (o \to o) \to o) \to o$. Note that several nodes in the figure are drawn with the same label. We could distinguish them via indices to keep them apart. But as each move corresponds to an occurrence of an atom in the type, we find it more convenient to follow the long-standing game semantics convention and keep moves distinct by attempting to always place them under the corresponding atom.

**Configurations.** Next we define the states reached when playing on arena A. Intuitively, a state is a sub-tree of A but where each branch may be explored multiple times – such structures were first introduced by Boudes [Bou09] under the name *thick subtrees*. Here, by analogy with concurrent games [CCRW17], we call them *configurations*.

**Definition 4.4.** A configuration $x \in \mathcal{C}(A)$ of arena $A$ is $x = (|x|, \le_x, \partial_x)$ such that $(|x|, \le_x)$ is a finite forest, and where $\partial_x$ is a function $\partial_x: |x| \to |A|$ called the **display map**, subject to the conditions:

*minimality-respecting:* for any $a \in |x|$, $a \in \min(x)$ iff $\partial_x(a) \in \min(A)$,

*causality-preserving:* for all $a_1, a_2 \in |x|$, if $a_1 \to_x a_2$ then $\partial_x(a_1) \to_A \partial_x(a_2)$,

and $x$ is **pointed** (and we write $x \in \mathcal{C}_\bullet(\mathcal{A})$) if it has exactly one minimal event.

A polarity on $x$ is deduced by $\text{pol}(a) = \text{pol}_A(\partial_x(a))$. We write $a^-$ (resp. $a^+$) for $a$ s.t. $\text{pol}(a) = -$ (resp. $\text{pol}(a) = +$). Ignoring the arrows with triangle heads and keeping only the dotted lines oriented from top to bottom, the diagram of Figure 6 defines a configuration on the arena of Figure 7 – notice that the branch on the left hand side is explored twice, and so is the first $q^+$.

For $x, y \in \mathcal{C}(A)$, the sets $|x|$ and $|y|$ are arbitrary and only related to $A$ via $\partial_x$ and $\partial_y$ – their specific identity is irrelevant. So configurations should be compared up to *symmetry*: a **symmetry** $\varphi: x \cong_A y$ is an order-isomorphism s.t. $\partial_y \circ \varphi = \partial_x$. Symmetry classes of configurations are called **positions**: the set of positions on $A$ is written $\mathcal{P}(A)$, and they are ranged over by $x, y, \text{etc.}$ (note the change of font). A position $x$ is **pointed**, written $x \in \mathcal{P}_\bullet(\mathcal{A})$, if any of its representatives is. If $x \in \mathcal{C}(A)$, we write $\bar{x} \in \mathcal{P}(A)$ for the corresponding position. Reciprocally, if $x \in \mathcal{P}(A)$, we fix a representative $\underline{x} \in \mathcal{C}(A)$. In [BC21], positions were shown to correspond to points in the relational model (if $o$ is interpreted as a singleton).

If $x \in \mathcal{C}(A)$ and $y \in \mathcal{C}(B)$, then $x \otimes y \in \mathcal{C}(A \otimes B)$ has events the disjoint union $|x| + |y|$, and display map inherited. We define $x \vdash y \in \mathcal{C}(A \vdash B)$ similarly. If moreover $A = B$, we define $x * y \in \mathcal{C}(A)$ with, again, $|x * y| = |x| + |y|$, and with display map the co-pairing $[\partial_x, \partial_y] : |x * y| \to |A|$.

**Augmentations.** We finally define our representation of plays up to homotopy:

**Definition 4.5.** An augmentation on arena $A$ is a quadruple $q = (|q|, \le_{(q|)}, \le_q, \partial_q)$, where $(q|) = (|q|, \le_{(q|)}, \partial_q) \in \mathcal{C}(A)$, and $(|q|, \le_q)$ is a forest satisfying:

*rule-abiding:* for all $a_1, a_2 \in |q|$, if $a_1 \le_{(q|)} a_2$, then $a_1 \le_q a_2$,

*courteous:* for all $a_1 \to_q a_2$, if $\text{pol}(a_1) = +$ or $\text{pol}(a_2) = -$, then $a_1 \to_{(q|)} a_2$,

*deterministic:* for all $a^- \to_q a_1^+$ and $a^- \to_q a_2^+$, we have $a_1 = a_2$,

*+-covered:* for all $a \in \max(q)$, we have $\text{pol}(a) = +$,

*negative:* for all $a \in \min(q)$, we have $\text{pol}(a) = -$.

We then write $q \in \text{Aug}(A)$, and call $(q|) \in \mathcal{C}(A)$ the **desequentialization** of $q$. Finally, $q$ is **pointed** if $\min(q)$ is a singleton, and we then write $q \in \text{Aug}_\bullet(A)$.
Figure 6 represents an augmentation $q$ by showing both relations $\dashrightarrow_{\langle q \rangle}$ (as dotted lines) and $\dashrightarrow_q$ (as arrows with black triangle heads). An augmentation $q \in \text{Aug}(A)$ augments a configuration $x \in \mathcal{C}(A)$ by specifying causal constraints imposed by the term: for each event, the augmentation gives the necessary conditions before it can be played. Augmentations are analogous to plays: *plays* in the Hyland-Ong sense can be recovered via the alternating linearizations of augmentations [BC21]. However, augmentations factor out Opponent's scheduling, hence give an explicit representation of plays up to homotopy.

**Isogmentations.** Just like for configurations, augmentations should be considered up to isomorphism. An **isomorphism** of augmentations $\varphi: q \cong p$ is a bijection preserving and reflecting all the structure. An **isogmentation** is an isomorphism class of augmentations, ranged over by $\mathbf{q}, \mathbf{p}, \text{etc.}:$ we write $\mathbf{lsog}(A)$ (resp. $\mathbf{lsog}_{\bullet}(A)$) for isogmentations (resp. pointed isogmentations). If $q \in \text{Aug}(A)$, we write $\bar{q} \in \mathbf{lsog}(A)$ for its isomorphism class; reciprocally, if $\mathbf{q} \in \mathbf{lsog}(A)$, we fix a representative $\mathbf{q} \in \mathbf{q}$.

**4.2. Isogmentations are Normal Resource Terms.** Now we spell out the link between isogmentations and normal resource terms. We first show how the structure of each syntactic kind is reflected by augmentations of the appropriate type: in particular, terms will be mapped to pointed isogmentations, and bags to general isogmentations. The main result (Theorem 4.11) follows directly.

**Tensors and sequences.** To reflect the syntactic formation rule for sequences, we first show that isogmentations on $A_1 \otimes \dots \otimes A_n$ are tuples of isogmentations on the $A_i$'s. Consider negative arenas $\Gamma, A_1, \dots, A_n$, and $q_i \in \text{Aug}(\Gamma \vdash A_i)$ for $1 \le i \le n$. We set $\vec{q} = \langle q_i \mid 1 \le i \le n \rangle \in \text{Aug}(\Gamma \vdash \otimes_{1 \le i \le n} A_i)$ with

$$|\vec{q}| \stackrel{\text{def}}{=} \sum_{i=1}^{n} |q_i|, \quad \left\{ \begin{array}{ll} \partial_{\vec{q}}(i, m) & \stackrel{\text{def}}{=} (1, g) & \text{if } \partial_{q_i}(m) = (1, g), \\ \partial_{\vec{q}}(i, m) & \stackrel{\text{def}}{=} (2, (i, a)) & \text{if } \partial_{q_i}(m) = (2, a), \end{array} \right.$$

where $m \in |q_i|$, $g \in |\Gamma|$, $a \in |A_i|$, and with the two orders $\le_{\vec{q}}$ and $\le_{\langle q \rangle}$ inherited. It is immediate that this construction preserves isomorphisms, so that it extends to isogmentations.

**Proposition 4.6.** *The previous construction on augmentations induces a bijection*

$$\langle -, \dots, - \rangle : \prod_{i=1}^{n} \mathbf{lsog}(\Gamma \vdash A_i) \cong \mathbf{lsog}(\Gamma \vdash \otimes_{1 \le i \le n} A_i).$$

*Proof. Injective.* As an isomorphism must preserve $\dashrightarrow$ and display maps, any isomorphism

$$\varphi : \langle q_i \mid i \in I \rangle \cong \langle p_i \mid i \in I \rangle$$

decomposes uniquely into a sequence of $\varphi_i : q_i \cong p_i$, as required.

*Surjective.* Consider $q \in \text{Aug}(\Gamma \vdash \otimes_{1 \le i \le n} A_i)$. Since $q$ is a forest, $m \in |q|$ has a unique minimal antecedent, sent by the display map (via condition *negative*) to one of the $A_i$'s – we say that $m$ is above $A_i$. Defining accordingly $q_i$ as $q$ restricted to the events above $A_i$, we easily construct an isomorphism $q \cong \langle q_i \mid 1 \le i \le n \rangle$ as required. $\square$
**Bags and pointedness.** The next step is to reflect the typing rule for bags, by showing that isoglementations are *bags of pointed isoglementations*.

We start by describing the corresponding construction. Consider negative arenas $\Gamma$ and $A$, and $q_1, q_2 \in \text{Aug}(\Gamma \vdash A)$. We set $q_1 * q_2 \in \text{Aug}(\Gamma \vdash A)$ with events $|q_1 * q_2| = |q_1| + |q_2|$, and display $\partial_{q_1 * q_2}(i, m) = \partial_{q_i}(m)$, and the two orders $\leq_{q_1 * q_2}$ and $\leq_{\emptyset(q_1 * q_2)}$ inherited. This generalizes to an $n$-ary operation in the obvious way, which preserves isomorphisms. The operation induced on isoglementations is associative and commutative, and it admits as neutral element the empty isoglementation $1 \in \text{lsog}(\Gamma \vdash A)$ with (a unique representative with) no event.

**Proposition 4.7.** *The previous construction on augmentations induces a bijection*

$$ [- , \dots , -] : \mathfrak{B}(\text{lsog}_{\bullet}(\Gamma \vdash A)) \cong \text{lsog}(\Gamma \vdash A) . $$

*Proof. Injective.* Pick $q_1, \dots, q_n, p_1, \dots, p_m \in \text{Aug}_{\bullet}(\Gamma \vdash A)$. Because the $q_i$'s and $p_i$'s are pointed and isomorphisms preserve the forest structure, an isomorphism $\varphi : q_1 * \dots * q_n \cong p_1 * \dots * p_m$ forces $m = n$ and induces a permutation $\pi$ on $n$ and a family of isos ($\varphi_i : q_i \cong p_{\pi(i)}$) $1 \le i \le n$, which implies $[q_i | 1 \le i \le n] = [\bar{p}_i | 1 \le i \le n]$ as bags.

*Surjective.* As any $q \in \text{Aug}(\Gamma \vdash A)$ is finite, it has a finite set $I$ of initial moves. Since $q$ is a forest, any $m \in |q|$ is above exactly one initial move. For $i \in I$, write $q_i \in \text{Aug}_{\bullet}(\Gamma \vdash A)$ the restriction of $q$ above $i$; then $q \cong q_1 * \dots * q_n$ as required. $\square$

**Currying.** For negative arenas $\Gamma$, $A$ and $B$, we have a bijection

$$ \Lambda_{\Gamma,A,B} : \text{Aug}(\Gamma \otimes A \vdash B) \cong \text{Aug}(\Gamma \vdash A \Rightarrow B) $$

leaving the augmentation unchanged except for the display map, which is reassigned following

$$ \begin{align*} \partial_{\Lambda(q)}(m) &= (1, \gamma) & \text{if } \partial_q(m) &= (1, (1, \gamma)) \\ \partial_{\Lambda(q)}(m) &= (2, (i, (2, b))) & \text{if } \partial_q(m) &= (2, b) \text{ and } \partial_q(\text{init}(m)) &= (2, i) \\ \partial_{\Lambda(q)}(m) &= (2, (i, (1, a))) & \text{if } \partial_q(m) &= (1, (2, a)) \text{ and } \partial_q(\text{init}(m)) &= (2, i) \end{align*} $$

where $\text{init}(m)$ denotes the unique $m' \in \min(q)$ such that $m' \le q m$ – note that $\partial_q(m')$ must be of the shape $(2, i)$ with $i \in \min(B)$ because $q$ is negative and rule-abiding.

Since isomorphisms of augmentations are order-isomorphisms and preserve display maps, the definition of this bijection is obviously compatible with isomorphisms, and we obtain:

**Proposition 4.8.** *The previous bijection defined on augmentations induces a bijection*

$$ \Lambda_{\Gamma,A,B} : \text{lsog}_{\bullet}(\Gamma \otimes A \vdash B) \cong \text{lsog}_{\bullet}(\Gamma \vdash A \Rightarrow B) . $$

**Head occurrence.** The previous constructions handle the rules (seq), (bag) and (abs) of the type system of Figure 4. By Lemma 3.2, the only remaining case to treat all typed normal forms is (var).

As above, we start with the corresponding construction on augmentations. We write $\vec{B} \Rightarrow o \stackrel{\text{def}}{=} B_1 \Rightarrow \dots \Rightarrow B_p \Rightarrow o$ for $\vec{B} = \langle B_1, \dots, B_n \rangle$ a tuple of objects, and $\vec{B}^{\otimes \text{def}} = B_1 \otimes \dots \otimes B_n$. Consider $\Gamma = A_1 \otimes \dots \otimes A_n$ where each $A_i$ is a negative arena of the shape $A_i = \vec{B}_i \Rightarrow o \cong \vec{B}_i^{\otimes \Gamma} \Rightarrow o$. Given $q \in \text{Aug}(\Gamma \vdash \vec{B}_i^{\otimes \Gamma})$, the *i-lifting of q*, written $\Box_i(q) \in \text{Aug}_{\bullet}(\Gamma \vdash o)$, is the augmentation that after the initial Opponent move, starts by playing the initial move $q_i$ of $A_i$ (which is negative in $A_i$ hence positive in $\Gamma \vdash o$), then proceeds as $q$. Writing $q_{i,1}, \dots, q_{i,l}$ for the initial moves of $q$ (which must be mapped to
<figure><img src="image_7.png" /><figcaption>Figure 8: Illustration of $\square_i(q)$</figcaption></figure>

initial moves of $\Gamma \vdash \vec{B}_i^\otimes$, hence of $\vec{B}_i^\otimes$ because $q$ is negative by definition), $\square_i(q)$ may be depicted as in Figure 8.

More formally:

**Definition 4.9.** The $i$-lifting of $q$, written $\square_i(q) \in \mathrm{Aug}_\bullet(\Gamma \vdash o)$, has partial order $\le_q$ prefixed with two additional moves, namely $\ominus$ and $\oplus$ with $\ominus \to \oplus$ and $\oplus \to m$ for each $m \in \mathrm{init}(q)$. Its desequentialization is the least partial order containing dependencies

$$m \leq_{(\square_i(q))} n \quad \text{for } m, n \in |q| \text{ with } m \leq_{(q)} n,$$

$$\oplus \le_{(\square_i(q))} m \quad \text{for all } m \in |q| \text{ with } \partial_q(m) = (2, a) \text{ for some } a \in |\vec{B}_i^\otimes|,$$

and with display map given by the following clauses:<fnref n="1" />

$$\partial_{\square_i(q)}(\ominus) \stackrel{\mathrm{def}}{=} (2, q)$$

$$\partial_{\square_i(q)}(\oplus) \stackrel{\mathrm{def}}{=} (1, (i, (2, q)))$$

$$\partial_{\square_i(q)}(m) \stackrel{\mathrm{def}}{=} (1, a) \quad \text{if } \partial_q(m) = (1, a),$$

$$\partial_{\square_i(q)}(m) \stackrel{\mathrm{def}}{=} (1, (i, (1, a))) \quad \text{if } \partial_q(m) = (2, a),$$

altogether defining $\square_i(q) \in \mathrm{Aug}_\bullet(\Gamma \vdash o)$ as required.

This construction again preserves isomorphisms and thus extends to isoglementations: for any $q \in \mathrm{lsog}(\Gamma \vdash \vec{B}_i^\otimes)$, we obtain its $i$-lifting $\square_i(q) \in \mathrm{lsog}_\bullet(\Gamma \vdash o)$.

**Proposition 4.10.** *The previous construction on augmentations induces a bijection*

$$\square : \sum_{1 \le i \le n} \mathrm{lsog}(\Gamma \vdash \vec{B}_i^\otimes) \simeq \mathrm{lsog}_\bullet(\Gamma \vdash o).$$

*Proof.* We set $\square(i, q) = \overline{\square_i(q)}$.

*Surjective.* Any $q \in \mathrm{Aug}_\bullet(\Gamma \vdash o)$ has a unique initial move, which is negative hence cannot be maximal by $+-\mathrm{covered}$. By *determinism*, there is a unique subsequent Player move, displayed to the initial move of some $A_i$. The subsequent moves define $q' \in \mathrm{Aug}(\Gamma \vdash \vec{B}_i^\otimes)$ s.t. $q \cong \square_i(q')$.

*Injective.* Given isomorphic $q \cong \square_i(q')$ and $p \cong \square_j(p')$, we obviously have $i = j$ since isomorphisms of augmentations preserve display maps; and the isomorphism decomposes into $q' \cong p'$ as required. $\square$

<footnote n="1">¹Recall that we write $q$ for the only move of the arena $o$. Also, we keep the isomorphism $A_i \cong \vec{B}_i^\otimes \Rightarrow o$ implicit whenever we write moves in $A_i$, so that we can consider $(i, (2, q)) \in |\Gamma|$, and $(i, (1, a)) \in |\Gamma|$ whenever $a \in |\vec{B}_i^\otimes|$.</footnote>
Putting together the above results, we may now deduce:

**Theorem 4.11.** For $\Gamma$ a context and $A$ a type, there are bijections:

$$ \|\cdot\|_{\mathbf{Tm}} : \mathbf{Tm}_{nf}(\Gamma; A) \simeq \mathbf{lsog}_{\bullet}(\llbracket \Gamma \rrbracket \vdash \llbracket A \rrbracket) $$

$$ \|\cdot\|_{\mathbf{Bg}} : \mathbf{Bg}_{nf}(\Gamma; A) \simeq \mathbf{lsog}(\llbracket \Gamma \rrbracket \vdash \llbracket A \rrbracket) $$

$$ \|\cdot\|_{\mathbf{Sq}} : \mathbf{Sq}_{nf}(\Gamma; \vec{A}) \simeq \mathbf{lsog}(\llbracket \Gamma \rrbracket \vdash \llbracket \vec{A} \rrbracket) $$

*Proof.* The three functions are defined by mutual induction using Propositions 4.6, 4.7, 4.8 and 4.10. For injectivity, we reason directly by induction on the syntax, using the injectivity of each construction. For surjectivity, we reason by induction on the size (i.e. the number of events) of augmentations, the syntactic kind (considering $\mathbf{Tm} < \mathbf{Bg} < \mathbf{Sq}$), and also the type $A$ in the $\mathbf{Tm}$ case: the decomposition provided by Proposition 4.10 yields augmentations of strictly smaller size (we remove the two initial moves); the bijection of Proposition 4.8 preserves the size of augmentations and stays in the kind $\mathbf{Tm}$, but yields a smaller output type; the remaining two decompositions do not increase the size and yield a lower kind. $\square$

## 5. A CATEGORY OF STRATEGIES

In the remaining of the paper, we will extend the previous static correspondence between normal resource terms and isoglementations into a *dynamic correspondence*. In the present section, we introduce *strategies* as weighted sums of isoglementations, and define a *composition* of strategies so that strategies form a category *Strat*. We will show in later sections that one can interpret (not necessarily normal) resource terms as strategies, in a compositional way: the interpretation is defined inductively on terms, each syntactic constructor being reflected by a construction on strategies; and it will follow from our results that composition is the image of resource substitution through this interpretation, which is moreover invariant under resource reduction. We will expose the relevant structure for the interpretation by introducing the notion of *resource category* in section 6: showing that *Strat* is indeed a resource category, in section 7, will yield the correspondence announced as the commutation of square (c) in our introduction.

5.1. **Strategies and Composition.** Consider $A, B$ and $C$ three negative arenas, and fix two augmentations $q \in \text{Aug}(A \vdash B)$, $p \in \text{Aug}(B \vdash C)$. We shall compose them via *interaction*, followed by *hiding*.

**Interaction of augmentations.** Intuitively, we can only compose $q$ and $p$ provided they reach the same state on $B$, so we first extract the “state they reach” via their desequentializations: let us write $x_A^q$ for the events of $q$ that display to $A$ and $x_B^q$ for those that display to $B$ – these define<fnref n="2" /> $x_A^q \in C(A)$ and $x_B^q \in C(B)$ and likewise for $p$.

But what does it mean to “reach the same state”? In general requiring $x_B^q = x_B^p$ is meaningless, since this data should really be considered up to isomorphism. States in $B$ are not configurations, but *positions*: symmetry classes of configurations. Thus $q$ and $p$ are *compatible* if $x_B^q$ and $x_B^p$ are *symmetric*, i.e. if there is a symmetry $\varphi: x_B^q \cong_B x_B^p$ – we write $x_B^q \cong_B x_B^p$ for the equivalence. Accordingly, we must define the composition of two compatible augmentations *along with* a mediating symmetry. We first form *interactions*:

<footnote n="2">²Up to isomorphism of augmentations we may consider that $\langle q \rangle = x_A^q \vdash x_B^q$, but we need not assume that.</footnote>
<figure><img src="image_8.png" /><figcaption>Figure 9: Construction of an interaction $p \circled{\circ} q$.</figcaption></figure>

**Definition 5.1.** For $q, p$ as above and $\varphi : x_B^q \cong_B x_B^p$, the **interaction** $p \circled{\circ} q$ is the pair $\langle |p \circled{\circ} q|, \leq_{p \circled{\circ} q} \rangle$ of the set $|p \circled{\circ} q| \stackrel{\text{def}}{=} |q| + |p|$ and the binary relation $\leq_{p \circled{\circ} q}$ on $|p \circled{\circ} q|$ defined as the transitive closure of $\triangleright \stackrel{\text{def}}{=} \triangleright_q \cup \triangleright_p \cup \triangleright_\varphi$ with

$$ \triangleright_q = \{((1, m), (1, m')) \mid m <_q m'\}, $$

$$ \triangleright_p = \{((2, m), (2, m')) \mid m <_p m'\}, $$

$$ \begin{aligned} \triangleright_\varphi = & \{((1, m), (2, \varphi(m))) \mid m \in x_B^q \wedge \text{pol}_{A \vdash B}(\partial_q(m)) = +\} \\ & \cup \{((2, m), (1, \varphi^{-1}(m))) \mid m \in x_B^p \wedge \text{pol}_{B \vdash C}(\partial_p(m)) = +\}. \end{aligned} $$

**Proposition 5.2.** The interaction $p \circled{\circ} q$ is a partially ordered set.

*Proof.* We show that $\triangleright$ is acyclic, i.e. its transitive closure is a strict partial order. This corresponds to a subtle and fundamental property of innocent strategies: they always have a deadlock-free interaction. Our proof, which appears in Appendix A, is a direct adaptation of a similar fact in concurrent games on event structures [CC24]. $\square$

Figure 9 illustrates the construction of an interaction. The two augmentations $q \in \text{Aug}(o \otimes o \vdash o)$ – on the left hand side – and $p \in \text{Aug}(o \vdash (o \Rightarrow o \Rightarrow o) \Rightarrow o)$ – on the right hand side – are shown with their common interface in red, bridged by a symmetry $\varphi$.

In order to show that the forthcoming composition of augmentation is well-behaved, we need to characterize immediate causal dependency in the interaction. It turns out that this is very constrained – this is detailed in two lemmas: the first, for forward causality, follows.

**Lemma 5.3.** If $m = (1, m') \to_{p \circled{\circ} q} n$ for $m' \in |q|$, then we have:

(1) If $m'$ is negative in $q$, then $n = (1, n')$ and $m' \to_q n'$;

(2) If $m'$ is positive in $q$ and displaying to $A$, then $n = (1, n')$ and $m' \to_q n'$;

(3) If $m'$ is positive in $q$ and displaying to $B$, then $n = (2, \varphi(m'))$,

and symmetrically for $m = (2, m') \to_{p \circled{\circ} q} n$ for $m' \in |p|$.

*Proof.* Necessarily, an immediate causal link must originate from one of the clauses of the relation $\triangleright$ above. For (1), for polarity reasons it can only be $(1, m') \triangleright_q n$ so that $n = (1, n')$ with $m' <_q n'$, and furthermore we must have $m' \to_q n'$ or that would immediately contradict $m \to_{p \circled{\circ} q} n$. For (2), similarly only the clause $\triangleright_q$ may apply.

For (3), we must show that $m \triangleright_q n$ is impossible. If that was the case, then $n = (1, n')$ with $m' <_q n'$, where we must have $m' \to_q n'$ (or contradict $m \to n$). But as $m'$ is positive,
by courtesy we have $m' \to_{\llbracket q \rrbracket} n'$, and thus $\varphi(m') \to_{\llbracket p \rrbracket} \varphi(n')$ as $\varphi$ is an order-isomorphism.
And by rule-abiding, that entails $\varphi(m') <_p \varphi(n')$, so that altogether we have

$$m \triangleright_{\varphi} (2, \varphi(m')) \triangleright_{p} (2, \varphi(n')) \triangleright_{\varphi} n$$

contradicting the fact that $m \to_{p \otimes_{\varphi} q} n$ is an immediate causal link. □

Symmetrically, in the “backwards” direction, we have:

**Lemma 5.4.** If $m \to_{p \otimes_{\varphi} q} (1, n') = n$ for $n' \in |q|$, then we have:

(1) If $n'$ is positive in $q$, then $m = (1, m')$ and $m' \to_{q} n'$;

(2) If $n'$ is negative in $q$ and displaying to $A$, then $m = (1, m')$ and $m' \to_{q} n'$;

(3) If $n'$ is negative in $q$ and displaying to $B$, then $m = (1, \varphi^{-1}(m'))$,

and symmetrically for $m \to_{p \otimes_{\varphi} q} (2, n')$ for $n' \in |p|$.

*Proof.* Analogous to the proof of Lemma 5.3. □

Now, we can go on and define the composition of augmentations.

**Composing augmentations.** We compose $q$ and $p$ via $\varphi$, by hiding the interaction. Recall that we write $\llbracket q \rrbracket \cong x_A^q \vdash x_B^q \in C(A \vdash B)$ and $\llbracket p \rrbracket \cong x_B^p \vdash x_C^p \in C(B \vdash C)$.

**Proposition 5.5.** The structure $p \odot_{\varphi} q$ obtained by restricting $p \otimes_{\varphi} q$ to $x_A^q + x_C^p$, with

$$\llbracket p \odot_{\varphi} q \rrbracket \stackrel{\text{def}}{=} x_A^q \vdash x_C^p, \quad \partial_{p \odot_{\varphi} q}((1, m)) \stackrel{\text{def}}{=} \partial_q((1, m)), \quad \partial_{p \odot_{\varphi} q}((2, m)) \stackrel{\text{def}}{=} \partial_p((2, m))$$

is an augmentation on $A \vdash C$.

*Proof.* Let us call an event $m \in |p \otimes_{\varphi} q|$ **visible** if it appears in $p \odot_{\varphi} q$, **hidden** otherwise.

*Rule-abiding* is immediate from the definition and the fact that $q$ and $p$ are rule-abiding. For *negative*, by case analysis, an event minimal in $p \odot_{\varphi} q$ must also be minimal in $p \otimes_{\varphi} q$, it must thus come from $p$ and occur in $C$, and be minimal in $p$, hence negative; +-covered is symmetric.

It remains to show that $p \odot_{\varphi} q$ is a forest, and that it satisfies conditions *courteous* and *deterministic* – for those, we show analogous properties on the interaction $p \otimes_{\varphi} q$. First, it is a forest: any move can have at most one causal predecessor by Lemma 5.4. Since $q$ and $p$ are deterministic, and $\triangleright_{\varphi}$ does not branch, Lemma 5.3 entails that $p \otimes_{\varphi} q$ can only branch at negative visible events, from which it follows that $p \odot_{\varphi} q$ is deterministic. Finally if $m \to_{p \odot_{\varphi} q} n$, this means we must have a sequence in the interaction

$$m \to_{p \otimes_{\varphi} q} m_1 \to_{p \otimes_{\varphi} q} \dots \to_{p \otimes_{\varphi} q} m_k \to_{p \otimes_{\varphi} q} n$$

in $p \otimes_{\varphi} q$ where $m_1, \dots, m_k$ are hidden. But then if $m$ is positive, $m_1$ cannot be hidden by Lemma 5.3, so that $k = 0$ and $m \to_{p \otimes_{\varphi} q} n$. But as both $m$ and $n$ are visible, this is only possible if they both come from $q$ or both come from $p$, contradicting the courtesy of $q$ or $p$. Likewise, if $n$ is negative, we reason likewise relying on Lemma 5.4 instead. □

The interaction in Figure 9 yields the augmentation in Figure 10, the composition of $q$ and $p$ via $\varphi$. Composition is then extended to isoglementations: for $q \in \mathfrak{lsog}(A \vdash B)$ and $p \in \mathfrak{lsog}(B \vdash C)$, we write $x_B^q \stackrel{\text{def}}{=} x_B^q$ and $x_B^p \stackrel{\text{def}}{=} x_B^p$, and then for $\varphi: x_B^q \cong_B x_B^p$, we define $p \odot_{\varphi} q \stackrel{\text{def}}{=} \underline{p \odot_{\varphi} q}$. We will soon show (in subsection 5.2) that the composition of augmentations is compatible with isomorphisms, so the previous lifting to isoglementations does not depend on the choice of representatives.
<figure><img src="image_9.png" /><figcaption>Figure 10: The composition $p \odot_{\varphi} q$, with $q$ and $p$ from Figure 9.</figcaption></figure>

One fact is puzzling: the composition of $q$ and $p$ is only defined once we have fixed a mediating $\varphi : x_B^q \cong_B x_B^p$, which is not unique – for instance, writing $qq \in \mathrm{Aug}(o)$ for the augmentation with two copies of the only move $q$ of $o$, there are exactly two symmetries $qq \cong_o qq$. Worse, the result of composition depends on the choice of $\varphi$: if Figure 9 was constructed with the symmetry $\psi : qq \cong_o qq$ swapping the two moves, we would get the variant $p \odot_{\psi} q$ of Figure 10 with the two final causal links crossed: $p \odot_{\varphi} q$ and $p \odot_{\psi} q$ are distinct, even up to iso.

This is reminiscent of the behaviour of resource substitution: e.g.,

$$ (\lambda f.f[x][x])\langle[y, z]/x\rangle = \lambda f.f[y][z] + \lambda f.f[z][y]. $$

As substitution of resource terms yields sums of resource terms, this suggests that composition of isoglementations should produce sums of isoglementations, which we will call strategies.

**Strategies.** A strategy is simply a weighted sum of isoglementations.

**Definition 5.6.** A strategy on arena $A$ is a function $\sigma : \mathrm{lsog}(A) \to \bar{\mathbb{R}}_+$, where $\bar{\mathbb{R}}_+$ is the completed half-line of non-negative real numbers. We then write $\sigma : A$.

We regard $\sigma : A$ as a weighted sum $\sigma = \sum_{q \in \mathrm{lsog}(A)} \sigma(q) \cdot q$, and we write $\mathrm{supp}(\sigma)$ for its support set: $\mathrm{supp}(\sigma) \stackrel{\mathrm{def}}{=} \{q \in \mathrm{lsog}(A) \mid \sigma(q) \neq 0\}$. We lift the composition of isoglementations to strategies via the formula

$$ \tau \odot \sigma \stackrel{\mathrm{def}}{=} \sum_{q \in \mathrm{lsog}(A \vdash B)} \sum_{p \in \mathrm{lsog}(B \vdash C)} \sum_{\varphi: x_B^q \cong_B x_B^p} \sigma(q) \tau(p) \cdot (p \odot_{\varphi} q) \quad (5.1) $$

for $\sigma : A \vdash B$ and $\tau : B \vdash C$, i.e. $(\tau \odot \sigma)(r)$ is the sum of $\sigma(q)\tau(p)$ over all triples $q, p, \varphi$ s.t. $r = p \odot_{\varphi} q$ – there are no convergence issues, as we consider positive coefficients and we have been careful to include $+\infty \in \bar{\mathbb{R}}_+$ in Definition 5.6.

**Identities.** We also introduce identities: *copycat strategies*, formal sums of specific isoglementations presenting typical copycat behaviour; we start by defining their concrete representatives.

Consider $x \in C(A)$ on negative arena $A$. The augmentation $\alpha_x \in \mathrm{Aug}(A \vdash A)$, called the **copycat** augmentation on $x$, has desequentialization $\langle \alpha_x \rangle \stackrel{\mathrm{def}}{=} x \vdash x$ and causal order
$x \vdash x$, augmented with

$$ \begin{array}{lcl} (1, m) & \leq & \alpha_x \quad (2, n) & \text{if } m \leq x \text{ and } \text{pol}_A(\partial_x(m)) = +, \\ (2, m) & \leq & \alpha_x \quad (1, n) & \text{if } m \leq x \text{ and } \text{pol}_A(\partial_x(m)) = -, \end{array} $$

so $\alpha_x$ adds to $x \vdash x$ all immediate causal links of the form $(2, m) \to (1, m)$ for negative $m$, and $(1, m) \to (2, m)$ for positive $m$. Again, this lifts to isoglementations by setting, for $x \in \mathcal{P}(A)$, the **copycat isoglementation** $\alpha_x \in \text{Isog}(A \vdash A)$ as the isomorphism class of $\alpha_x$.

The strategy $\text{id}_A : A \vdash A$ should have the isoglementation $\alpha_x$ for all position $x \in \mathcal{P}(A)$. But with which coefficient? If $\text{id}_A$ is to be an identity, then there is no choice: this coefficient must exactly cancel the sum over all symmetries in (5.1). Thus:

$$ \text{id}_A \stackrel{\text{def}}{=} \sum_{x \in \mathcal{P}(A)} \frac{1}{\#\text{Sym}(x)} \cdot \alpha_x \qquad (5.2) $$

where $\text{Sym}(x)$ is the group of *endosymmetries* of $x$, i.e. of all $\varphi : \underline{x} \cong_A \underline{x}$ – the cardinality of $\text{Sym}(x)$ does not depend on the choice of $\underline{x}$. This use of such a coefficient to compensate for future sums over sets of permutations is reminiscent of the Taylor expansion of $\lambda$-terms [ER08].

## 5.2. Proof of the Categorical Laws.
In this section, we show the main arguments behind the following result:

**Theorem 5.7.** *The negative arenas and strategies between them form a category, Strat.*

This is proved in several stages. Firstly, we establish isomorphisms corresponding to categorical laws, working concretely on augmentations – this means that these laws will refer to certain isomorphisms explicitly. Then, we show that composition of augmentations is compatible with isomorphisms, so that it carries out to isoglementations. From all that, we are in position to conclude and prove that Strat is indeed a category.

**Laws on the composition of augmentations.** The following lemma specifies in what sense the copycat augmentation is neutral for composition:

**Lemma 5.8 (Neutrality).** *Consider $q \in \text{Aug}(A \vdash B)$, $x \in \mathcal{C}(B)$ and $\varphi : x_B^q \cong_B x$. Then, $\alpha_x \odot_\varphi q \cong q$. Likewise, for any $y \in \mathcal{C}(A)$ and $\psi : y \cong_A x_A^q$, we have $q \odot_\psi \alpha_y \cong q$.*

*Proof.* Recall that $\alpha_x \odot_\varphi q$ is obtained by considering $\alpha_x \oplus_\varphi q$ with events $|q| + |\alpha_x|$, i.e. $|q| + (x + x)$ with causal order as described in Proposition 5.2. The composition $\alpha_x \odot_\varphi q$ is then the restriction to its visible events, i.e. $x_A^q + (\emptyset + x)$. Then

$$ |\alpha_x \odot_\varphi q| = x_A^q + (\emptyset + x) \cong x_A^q + x \stackrel{x_A^q + \varphi^{-1}}{\cong} x_A^q + x_B^q \cong |q| $$

forms a bijection between the sets of events, which is checked to be an isomorphism of augmentations by a direct analysis of the causal order of $\alpha_x \odot_\varphi q$. $\square$

It may be surprising that $\alpha_x \odot_\varphi q \cong q$ regardless of $\varphi$: the choice of the symmetry is reflected in the induced isomorphism $\phi_\varphi : \alpha_x \odot_\varphi q \cong q$, which the statement of this lemma ignores. Similarly, we have:
**Lemma 5.9 (Associativity).** Consider $q \in \mathrm{Aug}(A \vdash B)$, $p \in \mathrm{Aug}(B \vdash C)$, $r \in \mathrm{Aug}(C \vdash D)$, and two symmetries $\varphi : x_B^q \cong_B x_B^p$ and $\psi : x_C^p \cong_C x_C^r$. Then

$$r \odot \psi' (p \odot \varphi q) \cong (r \odot \psi p) \odot \varphi' q.$$

with $\varphi'$, $\psi'$ obtained from $\varphi$ and $\psi$, adjusting tags for disjoint unions in the obvious way.

*Proof.* A routine proof, relating the two compositions to a ternary composition $r \odot_{\psi}^3 p \odot_{\varphi}^3 q : \mathrm{Aug}(A \vdash D)$, defined in a way similar to binary composition. $\square$

**Congruence.** To lift the previous results to isogentations and strategies, composition must preserve isomorphisms.

Consider augmentations $q, q' \in \mathrm{Aug}(A \vdash B)$ with $\varphi : q \cong q'$, we know that $\varphi$ is an isomorphism of configurations $\varphi : (\langle q \rangle) \cong_{A \vdash B} (\langle q' \rangle)$ – a symmetry – therefore it projects to symmetries $\varphi_A : x_A^q \cong_A x_A^{q'}$ and $\varphi_B : x_B^q \cong_B x_B^{q'}$.

**Lemma 5.10.** Consider $q, q' \in \mathrm{Aug}(A \vdash B)$, $p, p' \in \mathrm{Aug}(B \vdash C)$, and isomorphisms $\theta : x_B^q \cong_B x_B^p, \theta' : x_B^{q'} \cong_B x_B^{p'}$, $\varphi : q \cong q'$ and $\psi : p \cong p'$ such that $\theta' \circ \varphi_B = \psi_B \circ \theta$.

Then, we have an isomorphism $\psi \odot_{\theta, \theta'} \varphi : p \odot_{\theta} q \cong p' \odot_{\theta'} q'$.

The proof is a direct verification that the obvious morphism between $p \odot_{\theta} q$ and $p' \odot_{\theta'} q'$ is indeed an isomorphism. The main consequence of this lemma is the following. Consider $q, q' \in \mathrm{Aug}(A \vdash B)$, $p, p' \in \mathrm{Aug}(B \vdash C)$, isomorphisms $\varphi : q \cong q'$ and $\psi : p \cong p'$, not requiring any commutation property as above. Still, $\varphi$ and $\psi$ project to symmetries

$$\varphi_B : x_B^q \cong_B x_B^{q'}, \qquad \psi_B : x_B^p \cong_B x_B^{p'}.$$

inducing a bijection

$$\chi : \begin{array}{ccc} x_B^q \cong_B x_B^p & \cong & x_B^{q'} \cong_B x_B^{p'} \\ \theta & \mapsto & \psi_B \circ \theta \circ \varphi_B^{-1}, \end{array}$$

so that for any $\theta : x_B^q \cong_B x_B^p$, we have $p \odot_{\theta} q \cong p' \odot_{\chi(\theta)} q'$ by Lemma 5.10. It ensues that we can substitute one representative for another when summing over all mediating symmetries:

$$\sum_{\theta: x_B^q \cong_B x_B^p} \overline{p \odot_{\theta} q} = \sum_{\theta: x_B^q \cong_B x_B^p} \overline{p' \odot_{\chi(\theta)} q'} = \sum_{\theta: x_B^{q'} \cong_B x_B^{p'}} \overline{p' \odot_{\theta} q'}$$

using the observation above, and re-indexing the sum following $\chi$ – or in other words, the composition of strategies does not depend on the choice of representative used for isogentations. This is often used silently throughout the development.

**Categorical laws.** We are now equipped to show Theorem 5.7. First, the identity laws:

**Proposition 5.11.** Consider $\sigma : A \vdash B$. Then, $\mathrm{id}_B \odot \sigma = \sigma \odot \mathrm{id}_A = \sigma$.

*Proof.* We focus on $\mathrm{id}_B \odot \sigma$. For any $p \in \mathrm{lsog}(B \vdash B)$, we write $(\underline{p}) = x_1^p \vdash x_r^p$. We have:

$$\begin{align*} \mathrm{id}_B \odot \sigma &= \sum_{q \in \mathrm{lsog}(A \vdash B)} \sum_{p \in \mathrm{lsog}(B \vdash B)} \sum_{\varphi : x_B^q \cong_B x_1^p} \sigma(q) \mathrm{id}_B(p) \cdot p \odot_{\varphi} q \\ &= \sum_{q \in \mathrm{lsog}(A \vdash B)} \sum_{x \in \mathcal{P}(B)} \sum_{\varphi : x_B^q \cong_B x \cong_B x_1^p} \frac{\sigma(q)}{\#\mathrm{Sym}(x)} \cdot \alpha_x \odot_{\varphi} q \end{align*}$$
using the definitions of the composition and of the identity strategy. Next, we compute

$$
\begin{align*}
\mathrm{id}_B \odot \sigma &= \sum_{q \in \mathrm{Isog}(A \vdash B)} \sum_{x \in \mathcal{P}(B)} \sum_{\varphi: x_B^q \cong_B x} \frac{\sigma(q)}{\#\mathrm{Sym}(x)} \cdot q \\
&= \sum_{q \in \mathrm{Isog}(A \vdash B)} \sum_{\varphi \in \mathrm{Sym}(\bar{x}_B^q)} \frac{\sigma(q)}{\#\mathrm{Sym}(\bar{x}_B^q)} \cdot q \\
&= \sum_{q \in \mathrm{Isog}(A \vdash B)} \sigma(q) \cdot q = \sigma
\end{align*}
$$

by Lemma 5.8 and direct reasoning on symmetries. The proof of the identity $\sigma \odot \mathrm{id}_A = \sigma$ is
symmetric. $\square$

Notice how the sum over all symmetries exactly compensates for the coefficient in
(5.2). Likewise, associativity of the composition of strategies follows from Lemma 5.9 and
bilinearity of composition, altogether concluding the proof that Strat is a category.

6. RESOURCE CATEGORIES

What further structure does Strat enjoy, that we could leverage to design an interpretation of
the resource calculus? It is not clear how to turn Strat into any existing notion of differential
category. It is not cartesian, and thus is not a cartesian differential category [BCS09].
Neither does it have the structure of a model of differential linear logic; it is additive and
symmetric monoidal but there is no clear candidate for the exponential modality. Overall, it
should be regarded as a new categorical structure, whose morphisms are analogous to (sums
of) *bags* of resource terms inhabiting a simple type, rather than single resource terms.

Thus we develop *resource categories*, models of the resource calculus inspired by Strat.

6.1. Motivation and Definition. Both substitution of resource terms and composition of isoglementations generate sums, so we need an additive structure. Following [BCLS20], an additive symmetric monoidal category (asmc) is a symmetric monoidal category where each homset is a commutative monoid, and each operation preserves the additive structure.

**Bialgebras.** As for differential categories, resource categories build on *bialgebras*:

**Definition 6.1.** Consider $\mathcal{C}$ an additive symmetric monoidal category.

A bialgebra on $\mathcal{C}$ is $(A, \delta_A, \epsilon_A, \mu_A, \eta_A)$ with $(A, \mu_A : A \otimes A \to A, \eta_A : I \to A)$ a commutative monoid (see Figure 11), and $(A, \delta_A : A \to A \otimes A, \epsilon_A : A \to I)$ a commutative comonoid (satisfying dual identities), with additional bialgebra laws (Figure 12).

In a resource category, all objects shall be bialgebras. Comonoids $(A, \delta_A, \epsilon_A)$ are the usual categorical description of duplicable objects. Intuitively, requests made to $\delta_A$ on either side of the tensor on the rhs, are sent to thelhs. Categorically the monoid structure $(A, \mu_A, \eta_A)$ is dual, but its intuitive behaviour is different: each request on the rhs is forwarded, non-deterministically, to either side of the tensor on thelhs, reflecting the *sums* arising in substitutions. These operational intuitions will be captured precisely by the resource category structure of Strat.
<figure><img src="image_10.png" /><figcaption>Figure 11: Monoid laws</figcaption></figure>

<figure><img src="image_11.png" /><figcaption>Figure 12: Bialgebra laws</figcaption></figure>

<figure><img src="image_12.png" /><figcaption>Figure 13: Laws for (co)multiplication and pointed identity</figcaption></figure>

In contrast with differential categories, morphisms in a resource category intuitively correspond to (sums of) *bags* rather than (sums of) *terms*. Morally, the empty bag from $A$ to $B$ is captured from the bialgebra structure as $\eta_B \circ \epsilon_A \in C(A, B)$, written 1. Likewise, the **product** $f * g = \mu_B \circ (f \otimes g) \circ \delta_A \in C(A, B)$ of $f, g \in C(A, B)$ captures the union of bags. This makes $(C(A, B), *, 1)$ a commutative monoid, altogether turning $C(A, B)$ into a commutative semiring, although composition and tensor in $C$ only preserve the additive monoid.

A bag of morphisms may be **flattened** into a morphism by the following operation: if $\bar{f} = [f_1, \dots, f_n] \in \mathcal{B}(C(A, B))$, we write $\Pi \bar{f} \stackrel{\text{def}}{=} f_1 * \dots * f_n \in C(A, B)$.

**Pointed identities.** Resource categories axiomatize categorically the singleton bags. For that, a pivotal role is played by the **pointed identity**, a chosen idempotent $\text{id}_A^{\bullet} \in C(A, A)$ which we think of as a singleton bag with a linear copycat behaviour. From this we may capture the singleton bags as those $f \in C(A, B)$ such that $\text{id}_B^{\bullet} \circ f = f$. Dually, we may also capture the morphisms that access *exactly one* resource: those are the $f \in C(A, B)$ such that $f \circ \text{id}_A^{\bullet} = f$. More formally:

**Definition 6.2.** Consider $\mathcal{C}$ an asmc where each object is equipped with a bialgebra structure. For $A \in \mathcal{C}$, a **pointed identity** on $A$ is an idempotent $\text{id}_A^{\bullet} \in C(A, A)$ satisfying the equations shown as string diagrams in Figure 13, plus $\epsilon_A \circ \text{id}_A^{\bullet} = 0$ and $\text{id}_A^{\bullet} \circ \eta_A = 0$.
<figure><img src="image_13.png" /><figcaption>Figure 14: Compatibility of comonoids with the monoidal structure – there are symmetric conditions for the compatibility of monoids with the monoidal structure.</figcaption></figure>

<figure><img src="image_14.png" /><figcaption>Figure 15: Compatibility of bags of pointed (resp. co-pointed) morphisms with $\delta$ (resp. $\mu$).</figcaption></figure>

Those laws are reminiscent of the laws of derelictions and coderelictions in bialgebra modalities [BCLS20], except that both roles are played by $\mathrm{id}_A$. In a resource category $\mathcal{C}$, all objects have a pointed identity. The “singleton bags” are those $f \in \mathcal{C}(A, B)$ that are **pointed**, i.e. $\mathrm{id}_B \circ f = f$ – we write $f \in \mathcal{C}_\bullet(\mathcal{A}, \mathcal{B})$. Dually, $f \in \mathcal{C}(\mathcal{A}, \mathcal{B})$ is **co-pointed** if $f \circ \mathrm{id}_A = f$, and we write $f \in \mathcal{C}^\bullet(\mathcal{A}, \mathcal{B})$.

**Resource categories.** Altogether, we are now ready to define resource categories:

**Definition 6.3.** A resource category is an asmc $\mathcal{C}$ where each $A \in \mathcal{C}$ has a bialgebra structure $(A, \delta_A, \epsilon_A, \mu_A, \eta_A)$ and pointed identity $\mathrm{id}_A$, such that the bialgebra structure is compatible with the monoidal structure of $\mathcal{C}$ in the sense that the diagrams of Figure 14 commute, and symmetrically for the monoid structure, with symmetric coherence laws.

This simple definition has powerful consequences. In particular, the following key property, derived from the definition of resource categories, expresses how the product of a bag of pointed morphisms interacts with the comonoid structure – and dually for the product of a bag of co-pointed morphisms and monoids. Much of the forthcoming proof that the interpretation is invariant under reduction relies on it:
**Lemma 6.4.** Consider $\mathcal{C}$ a resource category, then we have the following properties:

(1) For any bag of pointed morphisms $\bar{f} \in \mathcal{B}(\mathcal{C}_{\bullet}(A, B))$,

(a) the first diagram of Figure 15 commutes; and

(b) we have $\epsilon_B \circ \Pi \bar{f} = 1$ if $\bar{f}$ is empty, 0 otherwise;

(2) For any bag of co-pointed morphisms $\bar{f} \in \mathcal{B}(\mathcal{C}^{\bullet}(A, B))$,

(a) the second diagram of Figure 15 commutes; and

(b) we have $\Pi \bar{f} \circ \eta_A = 1$ if $\bar{f}$ is empty, 0 otherwise.

*Proof.* This follows from a lengthy but mostly direct diagram chase. $\square$

**Closed resource categories.** The notion of resource category is enough to reflect categorically the mechanism of resource substitution, but in order to also capture resource reduction, we must furthermore impose some closure condition.

First, assuming that the monoidal structure of $\mathcal{C}$ is closed, i.e. that the endofunctor $- \otimes A$ has a right adjoint $A \Rightarrow -$ for each $A \in \mathcal{C}$, we obtain the following constructions, borrowing the terminology and notations from the theory of cartesian closed categories: if $f \in \mathcal{C}(A \otimes B, C)$, the **currying of** $f$ is the image of $f$ by the adjunction, written

$$ \Lambda_{A,B,C}(f) \in \mathcal{C}(A, B \Rightarrow C), $$

and for any two objects $A, B \in \mathcal{C}$, we have the **evaluation morphism**

$$ \mathrm{ev}_{A,B} \stackrel{\mathrm{def}}{=} \Lambda_{A \Rightarrow B,A,B}^{-1}(\mathrm{id}_{A \Rightarrow B}) \in \mathcal{C}((A \Rightarrow B) \otimes A, B). $$

**Definition 6.5.** A resource category is said to be **closed** if its monoidal structure is closed and, moreover, currying is compatible with pointed identities: for all $A, B \in \mathcal{C}$,

$$ \mathrm{id}_{A \Rightarrow B}^{\bullet} = \Lambda_{A \Rightarrow B,A,B}(\mathrm{id}_{B}^{\bullet} \circ \mathrm{ev}_{A,B}). $$

## 6.2. Interpretation of the Resource Calculus.
In order to describe the interpretation of the resource calculus, it will be convenient to introduce some additional combinators, mimicking the structure of cartesian categories in resource categories:

**Cartesian combinators.** The **pairing** of $f \in \mathcal{C}(\Gamma, A)$ and $g \in \mathcal{C}(\Gamma, B)$ is

$$ \langle f, g \rangle \stackrel{\mathrm{def}}{=} (f \otimes g) \circ \delta_{\Gamma} \in \mathcal{C}(\Gamma, A \otimes B); $$

likewise $\pi_1 \stackrel{\mathrm{def}}{=} \rho_A \circ (A \otimes \epsilon_B) \in \mathcal{C}(A \otimes B, A)$ and $\pi_2 \stackrel{\mathrm{def}}{=} \lambda_B \circ (\epsilon_A \otimes B) \in \mathcal{C}(A \otimes B, B)$ are the two **projections** – we shall also use their obvious $n$-ary generalizations. The laws of cartesian categories fail in general: we have $\langle \pi_1, \pi_2 \rangle = \mathrm{id}_{A \otimes B}$, but e.g. $\pi_1 \circ \langle f, h \rangle = f$ only holds if $h$ is **erasable** (i.e. $\epsilon_B \circ h = \epsilon_\Gamma$) and $\langle f, g \rangle \circ h = \langle f \circ h, g \circ h \rangle$ if $h$ is **duplicable** (i.e. $\delta_\Gamma \circ h = (h \otimes h) \circ \delta_\Delta$) – so we do get the usual laws if $h$ is a **comonoid morphism** [Mel09].
**Lemmas on propagation of substitutions.** Morphisms coming from the interpretation are not comonoid morphisms, but many structural morphisms are: for instance it follows from a direct diagram chase that projections *are* comonoid morphisms.

As explained above, comonoid morphisms propagate in tuples as in a cartesian category. But, importantly, resource categories also specify how some non comonoid morphisms propagate through a pairing, even paired with a comonoid morphism:

**Lemma 6.6.** Let $\mathcal{C}$ be a resource category, $\bar{b} \in \mathfrak{B}(\mathcal{C}_{\bullet}(\Delta, A))$, $h \in \mathcal{C}(\Delta, \Gamma)$, $f \in \mathcal{C}(\Gamma \otimes A, B)$, $g \in \mathcal{C}(\Gamma \otimes A, C)$. If $h$ is a comonoid morphism, then we have:

$$ \langle f, g \rangle \circ \langle h, \Pi \bar{b} \rangle = \sum_{\bar{b} \prec \bar{b}_1 * \bar{b}_2} \langle f \circ \langle h, \Pi \bar{b}_1 \rangle, g \circ \langle h, \Pi \bar{b}_2 \rangle \rangle . $$

If moreover $B = C$ then

$$ (f * g) \circ \langle h, \Pi \bar{b} \rangle = \sum_{\bar{b} \prec \bar{b}_1 * \bar{b}_2} (f \circ \langle h, \Pi \bar{b}_1 \rangle) * (g \circ \langle h, \Pi \bar{b}_2 \rangle) . $$

Finally, $1 \circ \langle h, \Pi \bar{b} \rangle = 1$ if $\bar{b}$ is empty, 0 otherwise.

*Proof.* This is a simple verification based on item (1) of Lemma 6.4.

For the first equality, for instance, we start by unfolding:

$$ \langle f, g \rangle \circ \langle h, \Pi \bar{b} \rangle = (f \otimes g) \circ \delta_{\Gamma \otimes A} \circ (h \otimes \Pi \bar{b}) \circ \delta_{\Delta} \quad (6.1) $$

and then we reason equationally, denoting by $i_{A,B}: (A \otimes A) \otimes (B \otimes B) \cong (A \otimes B) \otimes (A \otimes B)$ the obvious structural isomorphism as in Figure 14:

$$
\begin{align*}
\delta_{\Gamma \otimes A} \circ (h \otimes \Pi \bar{b})
&= i_{\Gamma, A} \circ (\delta_{\Gamma} \otimes \delta_{A}) \circ (h \otimes \Pi \bar{b}) \\
&= i_{\Gamma, A} \circ (\delta_{\Gamma} \circ h) \otimes (\delta_{A} \circ \Pi \bar{b}) \\
&= i_{\Gamma, A} \circ ((h \otimes h) \circ \delta_{\Delta}) \otimes ((\sum_{\bar{b} \prec \bar{b}_1 * \bar{b}_2} \Pi \bar{b}_1 \otimes \Pi \bar{b}_2) \circ \delta_{\Delta}) \\
&= \sum_{\bar{b} \prec \bar{b}_1 * \bar{b}_2} i_{\Gamma, A} \circ ((h \otimes h) \circ \delta_{\Delta}) \otimes ((\Pi \bar{b}_1 \otimes \Pi \bar{b}_2) \circ \delta_{\Delta}) \\
&= \sum_{\bar{b} \prec \bar{b}_1 * \bar{b}_2} i_{\Gamma, A} \circ ((h \otimes h) \otimes (\Pi \bar{b}_1 \otimes \Pi \bar{b}_2)) \circ (\delta_{\Delta} \otimes \delta_{\Delta}) \\
&= \sum_{\bar{b} \prec \bar{b}_1 * \bar{b}_2} ((h \otimes \Pi \bar{b}_1) \otimes (h \otimes \Pi \bar{b}_2)) \circ i_{\Delta, \Delta} \circ (\delta_{\Delta} \otimes \delta_{\Delta}) \\
&= \sum_{\bar{b} \prec \bar{b}_1 * \bar{b}_2} ((h \otimes \Pi \bar{b}_1) \otimes (h \otimes \Pi \bar{b}_2)) \circ \delta_{\Delta \otimes \Delta}
\end{align*}
$$

using compatibility of $\delta_A$ with the monoidal structure, bifunctoriality of the tensor, the fact that $h$ is a comonoid morphism along with item (1) of Lemma 6.4, linearity of all operations with respect to the sum, again bifunctoriality of the tensor, naturality of $i_{A,B}$, and again compatibility of $\delta$ with the monoidal structure.
Substituting this in (6.1), we obtain (accounting for linearity):

$$
\begin{align*}
\langle f, g \rangle \circ \langle h, \Pi \bar{b} \rangle &= \sum_{\bar{b} < \bar{b}_1 * \bar{b}_2} (f \otimes g) \circ ((h \otimes \Pi \bar{b}_1) \otimes (h \otimes \Pi \bar{b}_2)) \circ \delta_{\Delta \otimes \Delta} \circ \delta_{\Delta} \\
&= \sum_{\bar{b} < \bar{b}_1 * \bar{b}_2} (f \otimes g) \circ ((h \otimes \Pi \bar{b}_1) \otimes (h \otimes \Pi \bar{b}_2)) \circ (\delta_{\Delta} \otimes \delta_{\Delta}) \circ \delta_{\Delta} \\
&= \sum_{\bar{b} < \bar{b}_1 * \bar{b}_2} \langle f \circ \langle h, \Pi \bar{b}_1 \rangle, g \circ \langle h, \Pi \bar{b}_2 \rangle \rangle
\end{align*}
$$

where $\delta_\Delta \circ \delta_{\Delta \otimes \Delta} = \delta_\Delta \circ (\delta_\Delta \circ \delta_\Delta)$ follows from the fact that $\Delta$ is a *commutative comonoid*, and the rest is by definition of tupling, and bifunctoriality of tensor.

The second equality has essentially the same proof, and the last is straightforward. □

This is fairly close to how substitutions propagate through terms in the resource $\lambda$-calculus (see section 3): we sum over all the partitions of the bag $\bar{b}$ into two components, to be distributed to the two components of the pair – when using this lemma in the proof of the substitution lemma, the comonoid morphism $h$ shall simply be an identity leaving all the unsubstituted variables unchanged. Syntactic substitution has another important case, namely when a substitution encounters a variable occurrence. Likewise here, we have:

**Lemma 6.7.** Consider $\bar{f} \in \mathcal{B}(C_\bullet(A, B))$. Then $\mathrm{id}_B^\bullet \circ \Pi \bar{f} = v$ if $\bar{f} = [v]$, 0 otherwise.

Again this lemma follows by diagram chasing, using the conditions of a resource category. It illustrates how the pointed identity is able to pick a single element of a bag. If the bag has too many elements or not enough, then the composition yields 0 – this reflects syntactic substitution, where the substitution must offer *exactly* as many resources as there are occurrences of the substituted variable.

**Interpretation.** From now on, we fix a closed resource category $\mathcal{C}$ with a chosen object $o$.

We first set $[o] \stackrel{\mathrm{def}}{=} o$, $[\langle A_1, \dots, A_n \rangle] \stackrel{\mathrm{def}}{=} [A_1] \otimes \dots \otimes [A_n]$ and $[A \to B] \stackrel{\mathrm{def}}{=} [A] \Rightarrow [B]$. For contexts, $[[\Gamma]] \stackrel{\mathrm{def}}{=} \bigotimes_{(x:A) \in \Gamma} [[A]]$. Note that currying and associativity morphisms induce an isomorphism

$$[[A]] \xrightarrow{\zeta_A} [[\vec{B}]] \Rightarrow o$$

for any type $A = \vec{B} \to o$. If $(x : A) \in \Gamma$, we then write

$$[[\Gamma]] \xrightarrow{\mathrm{var}_x^\Gamma} [[\vec{B}]] \Rightarrow o$$

for the projection morphism $[[\Gamma]] \to [[A]]$ followed by $\zeta_A$. For $\Gamma$ and $\Delta$ disjoint we also use the iso $\mathbb{M}_{\Gamma, \Delta} \in \mathcal{C}([\Gamma] \otimes [\Delta], [\Gamma, \Delta])$. The properties of closed resource categories ensure the following commutation:

**Lemma 6.8.** For any type $A = \vec{B} \to o$, $\zeta_A \circ \mathrm{id}_{[[A]]}^\bullet = \mathrm{id}_{[[\vec{B} \to o]]}^\bullet \circ \zeta_A$.

The interpretation of terms (or, rather, of typing derivations) then follows the three kinds of judgements from section 3: for $\Gamma, A \in \mathcal{C}$ and $\vec{A} = (A_1, \dots, A_n)$, we define

$$\mathrm{Tm}_C(\Gamma; A) \stackrel{\mathrm{def}}{=} C_\bullet(\Gamma, A) \quad \mathrm{Bg}_C(\Gamma; A) \stackrel{\mathrm{def}}{=} \mathcal{B}(\mathrm{Tm}_C(\Gamma; A)) \quad \mathrm{Sq}_C(\Gamma; \vec{A}) \stackrel{\mathrm{def}}{=} \Pi_{1 \le i \le n} \mathrm{Bg}_C(\Gamma; A_i).$$

Notably, sequences and bags are interpreted as *actual* sequences and bags at the “meta-level”, rather than via the “internal” bags (i.e. products of pointed maps) or products (i.e.
$$
\begin{align*}
\llbracket \Gamma \vdash_{\mathfrak{Tm}} \lambda x.s : A \to B \rrbracket &\stackrel{\text{def}}{=} \Lambda_{\llbracket \Gamma \rrbracket, \llbracket A \rrbracket, \llbracket B \rrbracket} (\llbracket \Gamma, x : A \vdash_{\mathfrak{Tm}} s : B \rrbracket \circ \mathsf{M}_{\llbracket \Gamma \rrbracket, \llbracket x:A \rrbracket}) \\
\llbracket \Gamma \vdash_{\mathfrak{Tm}} x \bar{t} : o \rrbracket &\stackrel{\text{def}}{=} \mathrm{ev}_{\llbracket \bar{A} \rrbracket, o} \circ \langle \mathrm{id}_{\llbracket \bar{A} \rrbracket}^{\bullet} \circ \mathrm{var}_x^{\Gamma}, \langle \llbracket \Gamma \vdash_{\mathfrak{Sq}} \bar{t} : \bar{A} \rrbracket \rangle \rangle \\
\llbracket \Gamma \vdash_{\mathfrak{Tm}} s \bar{t} : B \rrbracket &\stackrel{\text{def}}{=} \mathrm{ev}_{\llbracket A \rrbracket, \llbracket B \rrbracket} \circ \langle \llbracket \Gamma \vdash_{\mathfrak{Tm}} s : A \to B \rrbracket, \Pi \llbracket \Gamma \vdash_{\mathfrak{Bg}} \bar{t} : A \rrbracket \rangle \\
\llbracket \Gamma \vdash_{\mathfrak{Bg}} [s_1, \dots, s_n] : A \rrbracket &\stackrel{\text{def}}{=} [\llbracket \Gamma \vdash_{\mathfrak{Tm}} s_i : A \rrbracket \mid 1 \le i \le n] \\
\llbracket \Gamma \vdash_{\mathfrak{Sq}} \langle \bar{s}_1, \dots, \bar{s}_n \rangle : \bar{A} \rrbracket &\stackrel{\text{def}}{=} \langle \llbracket \Gamma \vdash_{\mathfrak{Bg}} \bar{s}_i : A_i \rrbracket \mid 1 \le i \le n \rangle
\end{align*}
$$

<caption>Figure 16: Interpretation of the resource calculus</caption>

via the monoidal structure) in $\mathcal{C}$. This apparent duplication of structure will be resolved when interpreting applications. For that purpose, in addition to the product $\Pi \bar{f} \in \mathcal{C}(\Gamma, A)$ of a bag of morphisms $\bar{f} \in \mathfrak{Bg}(\Gamma; A)$, we also define the **packing**

$$
\langle \bar{f} \rangle \stackrel{\text{def}}{=} \langle \Pi \bar{f}_1, \dots, \Pi \bar{f}_n \rangle \in \mathcal{C}(\Gamma, \bar{A}^{\otimes})
$$

of any sequence of morphisms $\vec{f} = (\bar{f}_1, \dots, \bar{f}_n) \in \mathfrak{Sq}_C(\Gamma; \vec{A})$.

We now define the three interpretation functions

$$
\mathfrak{Tm}(\Gamma; A) \to \mathfrak{Tm}_C(\llbracket \Gamma \rrbracket; \llbracket A \rrbracket) \quad \mathfrak{Bg}(\Gamma; A) \to \mathfrak{Bg}_C(\llbracket \Gamma \rrbracket; \llbracket A \rrbracket) \quad \mathfrak{Sq}(\Gamma; \vec{A}) \to \mathfrak{Sq}_C(\llbracket \Gamma \rrbracket; \llbracket \vec{A} \rrbracket)
$$

all written $\llbracket - \rrbracket$, by mutual induction, as in Figure 16. The interpretation is extended to sums of terms $\Sigma \mathfrak{Tm}(\Gamma; A) \to \mathfrak{Tm}_C(\llbracket \Gamma \rrbracket; \llbracket A \rrbracket)$ relying on the additive structure of $\mathcal{C}$ – we give no interpretation to sums of bags or sequences.

**6.3. The Soundness Theorem.** We show that this interpretation is invariant under reduction.

**Semantic substitution.** The bulk of the proof consists in proving a suitable substitution lemma, for which we must first give a semantic account of substitution. We define three semantic substitution functions:

$$
\begin{align*}
-\langle -/\vec{x} \rangle : \mathfrak{Tm}_C(\llbracket \Gamma, x : A \rrbracket; \llbracket B \rrbracket) \times \mathfrak{Bg}_C(\llbracket \Gamma \rrbracket; \llbracket A \rrbracket) &\to \mathfrak{Tm}_C(\llbracket \Gamma \rrbracket; \llbracket B \rrbracket) \\
-\langle -/\vec{x} \rangle : \mathfrak{Bg}_C(\llbracket \Gamma, x : A \rrbracket; \llbracket B \rrbracket) \times \mathfrak{Bg}_C(\llbracket \Gamma \rrbracket; \llbracket A \rrbracket) &\to \mathcal{C}(\llbracket \Gamma \rrbracket, \llbracket B \rrbracket) \\
-\langle -/\vec{x} \rangle : \mathfrak{Sq}_C(\llbracket \Gamma, x : A \rrbracket; \llbracket \vec{B} \rrbracket) \times \mathfrak{Bg}_C(\llbracket \Gamma \rrbracket; \llbracket A \rrbracket) &\to \mathcal{C}(\llbracket \Gamma \rrbracket, \llbracket \vec{B} \rrbracket)
\end{align*}
$$

using our cartesian-like notations:

$$
\begin{align*}
f \langle \bar{g}/x \rangle &\stackrel{\text{def}}{=} f \circ \mathsf{M}_{\llbracket \Gamma \rrbracket, \llbracket x:A \rrbracket} \circ \langle \mathrm{id}_{\llbracket \Gamma \rrbracket}, \Pi \bar{g} \rangle \\
\bar{f} \langle \bar{g}/x \rangle &\stackrel{\text{def}}{=} \Pi \bar{f} \circ \mathsf{M}_{\llbracket \Gamma \rrbracket, \llbracket x:A \rrbracket} \circ \langle \mathrm{id}_{\llbracket \Gamma \rrbracket}, \Pi \bar{g} \rangle \\
\vec{f} \langle \bar{g}/x \rangle &\stackrel{\text{def}}{=} \langle \vec{f} \rangle \circ \mathsf{M}_{\llbracket \Gamma \rrbracket, \llbracket x:A \rrbracket} \circ \langle \mathrm{id}_{\llbracket \Gamma \rrbracket}, \Pi \bar{g} \rangle
\end{align*}
$$

for $f \in \mathfrak{Tm}_C(\llbracket \Gamma, x : A \rrbracket; \llbracket B \rrbracket)$, $\bar{f} \in \mathfrak{Bg}_C(\llbracket \Gamma, x : A \rrbracket; \llbracket B \rrbracket)$, and $\vec{f} \in \mathfrak{Sq}_C(\llbracket \Gamma, x : A \rrbracket; \llbracket \vec{B} \rrbracket)$ respectively. We may now state the substitution lemma:

**Lemma 6.9.** Consider $\bar{t} \in \mathfrak{Bg}(\Gamma; A)$, $\Delta = \Gamma, x : A$ and $s \in \mathfrak{Tm}(\Delta; B)$. Then,

$$
\llbracket s \langle \bar{t} / x \rangle \rrbracket = \llbracket s \rrbracket \llbracket \langle \bar{t} \rangle / x \rrbracket .
$$
*Proof.* We show the stronger statement that for all $\bar{t} \in \text{Bg}(\Gamma; A)$ and $\Delta = \Gamma, x : A$,

(1) if $s \in \text{Tm}(\Delta; B)$, then $\llbracket s\langle\bar{t}/x\rangle\rrbracket = \llbracket s\rrbracket\llbracket\llbracket\bar{t}\rrbracket/x\rrbracket$;

(2) assume $\bar{s} \in \text{Bg}(\Delta; B)$ with $\bar{s}\langle\bar{t}/x\rangle = \sum_{1\le i\le n} \bar{s}_i$, where $\bar{s}_i \in \text{Bg}(\Gamma; B)$, then $\sum_{1\le i\le n} \Pi[\bar{s}_i] = \llbracket \bar{s} \rrbracket\llbracket \llbracket \bar{t} \rrbracket/x \rrbracket$;

(3) assume $\vec{s} \in \text{Sq}(\Delta; \vec{B})$ with $\vec{s}\langle\vec{t}/x\rangle = \sum_{1\le i\le n} \vec{s}_i$, where $\vec{s}_i \in \text{Sq}(\Gamma; \vec{B})$, then $\sum_{1\le i\le n} \langle[\vec{s}_i]\rangle = \llbracket \vec{s} \rrbracket\llbracket \llbracket \vec{t} \rrbracket/x \rrbracket$;

which follows by induction on typing derivations, using the lemmas of the previous subsection. $\square$

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

From the substitution lemma above, we may easily deduce:

**Theorem 6.10.** If $S \in \Sigma\text{Tm}(\Gamma; A)$ and $S \rightsquigarrow S'$ then $\llbracket S \rrbracket = \llbracket S' \rrbracket$.

*Proof.* Preservation of $\beta$-reduction follows from Lemma 6.9. Invariance for bags and sequences must be stated carefully: reduction yields sums of bags and sequences whereas the sets $\text{Bg}_C(\Gamma, A)$ and $\text{Sq}_C(\Gamma, \vec{A})$ are not stable under sums. To show that invariance extends by context closure, we prove the three statements:

(1) if $s \in \text{Tm}(\Gamma; A)$ and $s \rightsquigarrow S'$ then $\llbracket s \rrbracket = \llbracket S' \rrbracket$;

(2) if $\bar{s} \in \text{Bg}(\Gamma; A)$ and $\bar{s} \rightsquigarrow \sum_{i \in I} \bar{s}_i$ then $\Pi[\bar{s}] = \sum_{i \in I} \Pi[\bar{s}_i]$;

(3) if $\vec{s} \in \text{Sq}(\Gamma; \vec{A})$ and $\vec{s} \rightsquigarrow \sum_{i \in I} \vec{s}_i$ then $\langle[\vec{s}]\rangle = \sum_{i \in I} \langle[\vec{s}_i]\rangle$;

by mutual induction, following the inductive definition of context closure. Finally, it is immediate that this extends to sums as required. $\square$

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

# 7. GAME SEMANTICS AS A RESOURCE CATEGORY

It remains to check that **Strat** is indeed a resource category, and that the induced interpretation of normal forms coincides with the bijections from Theorem 4.11.

## 7.1. Additive Symmetric Monoidal Structure.

**Tensor.** As for composition we first define the tensor of augmentations, then isogenometations, then strategies. For $A_i, B_i$ arenas with $q_i \in \text{Aug}(A_i \vdash B_i)$ for $i = 1, 2$, we set $q_1 \otimes q_2 \in \text{Aug}(A_1 \otimes A_2 \vdash B_1 \otimes B_2)$ with $|q_1 \otimes q_2| = |q_1| + |q_2|$ and $\partial_{q_1 \otimes q_2}(i, m) = (j, (i, n))$ if $\partial_{q_i}(m) = (j, n)$, and the orders $\le_{q_1 \otimes q_2}$ and $\le_{\langle q_1 \otimes q_2 \rangle}$ inherited. This construction preserves isomorphisms, hence the tensor $q_1 \otimes q_2 \in \text{Isog}(A_1 \otimes A_2 \vdash B_1 \otimes B_2)$ may be defined via any representative – for definiteness, we use the chosen representatives of $q_1$ and $q_2$. We lift the definition to strategies with, for $\sigma_1 : \Gamma_1 \vdash A_1$ and $\sigma_2 : \Gamma_2 \vdash A_2$:

$$ \sigma_1 \otimes \sigma_2 \stackrel{\text{def}}{=} \sum_{q_1 \in \text{Isog}(A_1 \vdash B_1)} \sum_{q_2 \in \text{Isog}(A_2 \vdash B_2)} \sigma_1(q_1) \sigma_2(q_2) \cdot (q_1 \otimes q_2). $$
**Structural morphisms.** Structural morphisms are all variations of copycat. As we did for copycat itself, we start with concrete representatives. Consider A, B, C arenas, and $x \in C(A)$, $y \in C(B)$, $z \in C(C)$. Noting $\emptyset$ the empty configuration on 1, we set:

$$ (\lambda_A^x) = \emptyset \otimes x \vdash x, \quad (\alpha_{A,B,C}^{x,y,z}) = x \otimes (y \otimes z) \vdash (x \otimes y) \otimes z, $$

$$ (\rho_A^x) = x \otimes \emptyset \vdash x, \quad (\gamma_{A,B}^{x,y}) = x \otimes y \vdash y \otimes x. $$

and $\lambda_A^x$, $\rho_A^x$, $\alpha_{A,B,C}^{x,y,z}$ and $\gamma_{A,B}^{x,y}$ are defined from these, augmented with the obvious copycat behaviour.

We lift this to isoglementations: for $x \in \mathcal{P}(A)$, $\lambda_A^x$ is the isomorphism class of $\lambda_A^x$; and likewise for the others. Then the strategy $\lambda_A$ is defined as for $\mathrm{id}_A$ in (5.2) (page 19) by setting

$$ \lambda_A \stackrel{\mathrm{def}}{=} \sum_{x \in \mathcal{P}(A)} \frac{1}{\#\mathrm{Sym}(x)} \cdot \lambda_A^x $$

and likewise for $\rho_A$, $\alpha_{A,B,C}$ and $\gamma_{A,B}$. These structural morphisms satisfy the necessary conditions to make $(\mathrm{Strat}, \otimes, 1)$ a symmetric monoidal category.

**Additive Structure.** The additive structure is simply given by the formal sum. Consider $\Gamma$, A negative arenas and $\sigma, \tau : \Gamma \vdash A$, then the sum $\sigma + \tau : \Gamma \vdash A$ is:

$$ \sigma + \tau \stackrel{\mathrm{def}}{=} \sum_{q \in \mathrm{lsog}(\Gamma \vdash A)} (\sigma(q) + \tau(q)) \cdot q, $$

and 0 is the empty strategy $(\mathrm{supp}(0) = \emptyset)$. The tensor and the composition are compatible with the additive structure, hence Strat is an asmc.

## 7.2. Resource Category Structure.

**Bialgebra.** As resource categories rest on bialgebras, this is our next step in understanding the categorical structure of Strat. For the strategies for (co)multiplication, we first set configurations $((\delta_A^{x,y}) = x * y \vdash x \otimes y$ and $((\mu_A^{x,y}) = x \otimes y \vdash x * y$ for any A and $x, y \in C(A)$; $\delta_A^{x,y}$, $\mu_A^{x,y}$ are obtained by adjoining copycat behaviour on $x$ and $y$. This lifts to isoglementations $\delta_A^{x,y}$ and $\mu_A^{x,y}$ for $x, y \in \mathcal{P}(A)$. We can now define the strategies as:

$$ \delta_A \stackrel{\mathrm{def}}{=} \sum_{x,y \in \mathcal{P}(A)} \frac{1}{\#\mathrm{Sym}(x) \times \#\mathrm{Sym}(y)} \cdot \delta_A^{x,y} \qquad \mu_A \stackrel{\mathrm{def}}{=} \sum_{x,y \in \mathcal{P}(A)} \frac{1}{\#\mathrm{Sym}(x) \times \#\mathrm{Sym}(y)} \cdot \mu_A^{x,y}. $$

The unit $\epsilon_A$ and co-unit and $\eta_A$ are both strategies with only the empty isoglementation in their support, with coefficient 1. This provides the components for the following result:

**Proposition 7.1.** For any negative arena A, the tuple $(A, \delta_A, \epsilon_A, \mu_A, \eta_A)$ is a bialgebra.

*Proof.* Most of the identities involved in the bialgebra structure are straightforward. The only subtle law is the distributivity between $\delta_A$ and $\mu_A$, which is detailed in Appendix B. $\square$

Additionally, it is direct that this is compatible with the monoidal structure.
**Pointed Identity.** Now, we focus on the next component of resource categories: pointed identities and morphisms. So we start by defining the pointed identity as the copycat strategy over pointed positions only:

$$ \mathrm{id}_{\mathrm{A}}^{\bullet} = \sum_{x \in \mathcal{P}_{\bullet}(\mathrm{A})} \frac{1}{\#\mathrm{Sym}(x)} \cdot \alpha_{x} $$

where $\mathcal{P}_{\bullet}(\mathrm{A})$ denotes pointed positions of $\mathrm{A}$, i.e. $x \in \mathcal{P}(\mathrm{A})$ such that $\underline{x}$ is pointed. Note that for any $x \in \mathcal{P}_{\bullet}(\mathrm{A})$, we have $\langle \alpha_{\underline{x}} \rangle = \underline{x} \vdash \underline{x}$, where both $\underline{x}$'s are pointed. Hence, isoglementations in $\mathrm{id}_{\mathrm{A}}^{\bullet}$ have both left and right components pointed – which explains why $\mathrm{id}_{\mathrm{A}}^{\bullet}$ satisfies the pointed identity laws.

This definition corresponds to the intuition given in the previous section. We want *pointed morphisms* to represent singleton bags – strategies whose isoglementations are all pointed. But for any $\sigma : \Gamma \vdash A$, since $\mathrm{id}_{\mathrm{A}}^{\bullet}$ is defined over pointed positions only, the composition $\mathrm{id}_{\mathrm{A}}^{\bullet} \odot \sigma$ preserves only the isoglementations in $\sigma$ which are themselves pointed – hence $\mathrm{id}_{\mathrm{A}}^{\bullet} \odot \sigma = \sigma$ iff all isoglementations of $\sigma$ are pointed. Dually, we want *co-pointed morphisms* to represent morphisms which require exactly one resource. Consider again $\sigma : \Gamma \vdash A$, then $\sigma \odot \mathrm{id}_{\mathrm{A}}^{\bullet}$ preserves only the isoglementations which have their left component pointed – hence $\sigma$ is co-pointed iff the left components of all of its isoglementations are pointed.

**Closed structure.** Finally, we look at monoidal closure. We use the currying bijection $\Lambda_{\Gamma,A,B}$ from section 4. For $\sigma : \Gamma \otimes A \vdash B$, we set $\Lambda_{\Gamma,A,B}(\sigma) = \sum_{q \in \mathrm{lsog}(\Gamma \otimes A \vdash B)} \sigma(q) \cdot \Lambda_{\Gamma,A,B}(q)$, which directly yields

$$ \Lambda_{\Gamma,A,B} : \mathrm{Strat}(\Gamma \otimes A, B) \cong \mathrm{Strat}(\Gamma, A \Rightarrow B). $$

The laws of monoidal closure are easily verified, as well as the additional identity of Definition 6.5, finally yielding the desired structure:

**Theorem 7.2.** *Strat is a closed resource category.*

**7.3. Compatibility with normal forms.** Finally, we show that, up to the bijection $\|\cdot\|$ between normal resource terms and isoglementations, the interpretation of a resource term in the resource category *Strat* coincides with its normal form.

**Proposition 7.3.** *Consider $s \in \mathrm{Tm}_{\mathrm{nf}}(\Gamma; A)$. Then $\llbracket s \rrbracket$ is the sum having $\|s\|$ with coefficient 1, and 0 everywhere else.*

*Proof.* Recall the interpretation of the resource calculus in a resource category given in Figure 16. Restricting to normal forms rules out the third clause in that figure. We treat the remaining cases inductively. The identity follows immediately from the induction hypothesis for sequences, bags and abstraction terms, since the interpretation matches the bijections of Propositions 4.6, 4.7 and 4.8. The case of a fully applied variable is less obvious, but the *i*-lifting described in Figure 8 actually corresponds to the composition with $\mathrm{ev}_{\llbracket \bar{A} \rrbracket,o}$ in the variable clause of Figure 16, recalling that

$$ \mathrm{ev}_{\llbracket \bar{A} \rrbracket,o} = \Lambda_{\llbracket \bar{A} \rrbracket \Rightarrow o, \llbracket \bar{A} \rrbracket,o}^{-1}(\mathrm{id}_{\llbracket \bar{A} \rrbracket \Rightarrow o}). \quad \square $$

Thus, our interpretation in *Strat* computes a representation of the normal form:

**Corollary 7.4.** *If $s \in \mathrm{Tm}(\Gamma; A)$ has normal form $\sum_{i \in I} s_i$, then $\llbracket s \rrbracket = \sum_{i \in I} \|s_i\|$.*
## 8. CONCLUDING REMARKS

The correspondence with game semantics relies on the terms of the resource calculus to be $η$-expanded. This was expected – as in [TO16] – but some consequences deserve discussion.

Firstly, $x: A \to B$ is not a valid term as it is not $η$-long: it hides some infinitary copycat behaviour, requiring an infinite sum as in (5.2). This makes our calculus finitary in a stronger sense than usual: each normal resource term describes a simple, finite behaviour, and one can prove that it corresponds to a single point of the relational model – as in [TO16] again. This also means that in the absence of infinite sums, our typed syntax is not a resource category as it lacks identities.

Secondly, one might think that having an $η$-long syntax puts the pure, untyped $λ$-calculus out of reach. In [TO16], Tsukada and Ong suggest the resource calculus with tests [BCEM12] as a candidate for extending the correspondence to the untyped setting, but this does not seem fit for the task: it gives a syntactic counterpart to points of the relational model that do not correspond to any normal resource term nor any pointed augmentation.

It is in fact possible to enforce full $η$-expansion on terms without typing, but this requires altering the syntax of the calculus allowing for infinite sequences of abstractions, as well as applications to infinite sequences of (almost always empty) bags. Keeping the correspondence between terms and augmentations then relies on finding the analogue of a reflexive object in the category of games. And the resulting *extensional resource calculus*, enjoys a close relationship with Nakajima trees [Nak75] (see also [Bar84, Exercise 19.4.4]), similar to that of the ordinary resource calculus with Böhm trees. More precisely, it is possible to design an extensional version of Taylor expansion, so that the normal form of the Taylor expansion of a $λ$-term characterizes exactly its Nakajima tree or, equivalently, its class in the greatest sensible consistent $λ$-theory $H^*$. This is the subject of a separate paper, in preparation [BCVA23a].

## APPENDIX A. PROOF OF THE ABSENCE OF DEADLOCKS IN INTERACTIONS

The goal of this section is to prove Proposition 5.2: fixing $q \in \text{Aug}(A \vdash B)$ and $p \in \text{Aug}(B \vdash C)$ and $\varphi: x_B^q \cong_B x_B^p$, we must prove that $\vdash$ is acyclic on $p \stackrel{\otimes \varphi}{\to} q$.

If $m \in |p \stackrel{\otimes \varphi}{\to} q|$, it **occurs in** A if it has form $(1, m')$ with $\partial_q(m') = (1, a)$; and **occurs in** C if it has form $(2, m')$ with $\partial_p(m') = (2, c)$. Otherwise, it **occurs in** B.

First, we note that a cycle in $\vdash$ induces a cycle that is entirely in B.

**Lemma A.1.** Consider $q \in \text{Aug}(A \vdash B)$, $p \in \text{Aug}(B \vdash C)$ and $\varphi: x_B^q \cong_B x_B^p$.

If $\vdash$ has a cycle in $p \stackrel{\otimes \varphi}{\to} q$, then it has a cycle entirely in B.

*Proof.* First, observe that $\vdash$ has no direct link between A and C. Consider a cycle

$$m_1 \vdash \dots \vdash m_n \vdash m_1,$$

first note that this cycle must pass through B. Otherwise, it is entirely in A or entirely in C, making $\vdash_q$ or $\vdash_{q'}$ cyclic, contradiction. Now, consider a section

$$m_i^B \vdash m_{i+1}^A \vdash \dots \vdash m_j^A \vdash m_{j+1}^B$$

with the segment $m_{i+1} \vdash \dots \vdash m_j$ entirely in A. By definition, we must have

$$m_i^B \vdash_q m_{i+1}^A \vdash_q \dots \vdash_q m_j^A \vdash_q m_{j+1}^B,$$
so that $m_i^B \triangleright_q m_{j+1}^B$ by transitivity of $\triangleright_q$. Hence, a segment of the cycle in A may be removed, preserving the cycle. Symmetrically, any segment in C may be removed, yielding a cycle within B. $\square$

Hence, we restrict our attention to cycles entirely within B. Given a cycle

$$m_1 \triangleright \dots \triangleright m_n \triangleright m_1$$

we call $n$ its **length**. Next we show that this cycle can also be assumed not to contain any element minimal in B. We introduce additional conventions. If $m$ occurs in B, we say it **occurs in** $B^1$ if it is $(1, m')$ for $m' \in |q|$, and **occurs in** $B^r$ otherwise.

We will use this lemma:

**Lemma A.2.** Consider $q \in \text{Aug}(A \vdash B)$ and $m, m' \in |q|$ such that $m <_q m'$, with $m'$ occurring in B and $\partial_q(m)$ minimal in B. Then, $m <_{\langle|q|\rangle} m'$.

*Proof.* Since $\langle|q|\rangle$ is a forest, there is a unique $n <_{\langle|q|\rangle} m'$ such that $n$ is minimal in B. By rule-abiding, $n$ is minimal for $\leq_q$. Since $q$ is a forest, it follows that $n = m$. $\square$

Exploiting that, we prove:

**Lemma A.3.** Consider $q \in \text{Aug}(A \vdash B)$, $p \in \text{Aug}(B \vdash C)$ and $\varphi : x_B^q \cong_B x_B^p$. If $\triangleright$ has a cycle, then it has one entirely in B and without minimal event in B.

*Proof.* By Lemma A.1, assume the cycle is entirely in B. Consider a cycle

$$m_1 \triangleright \dots \triangleright m_n \triangleright m_1$$

entirely in B of minimal length. Seeking a contradiction, consider $m_i$ minimal in B.

Assume first it is in $B^r$. Since B is negative, $m_i$ is positive in $p$, hence we cannot have $m_{i-1} \triangleright_{\varphi} m_i$ and we must have $m_{i-1} \triangleright_p m_i$. Then, if $m_{i+1}$ is also in $B^r$, we have

$$m_{i-1} \triangleright_p m_i \triangleright_p m_{i+1}$$

so $m_{i-1} \triangleright_p m_{i+1}$, shortening the cycle and contradicting its minimality. So $m_{i+1}$ is in $B^1$. But then $m_i \triangleright_{\varphi} m_{i+1}$ so that $\varphi(m_{i+1}) = m_i$. As an isomorphism of configurations, $\varphi$ preserves the display to B, so $m_{i+1}$ is minimal in $B^1$.

In all cases, the cycle thus contains a minimal element of $B^1$, call it $m_i = (1, m'_i)$, with $m'_i$ negative in $q$: since $q$ is courteous, $m'_i$ is also minimal in $q$ so we cannot have $m_{i-1} \triangleright_q m_i$. Then

$$m_{i-1} \triangleright_{\varphi} m_i \triangleright_q m_{i+1} \triangleright_q \dots \triangleright_q m_j \triangleright_{\varphi} m_{j+1}$$

where all relations in between $m_i$ and $m_j = (1, m'_j)$ are in $\triangleright_q$ (by definition, only those can apply until we jump to $B^r$ via $\triangleright_{\varphi}$), and where by definition, $\varphi(m'_j) = m'_{j+1}$. But then, by transitivity, $m_i \triangleright_q m_j$, i.e. $m'_i <_q m'_j$. But by Lemma A.2, this entails $m'_i <_{\langle|q|\rangle} m'_j$. Now as $\varphi$ is an isomorphism of configurations, this entails $\varphi(m'_i) <_{\langle|p|\rangle} \varphi(m'_j)$, and by rule-abiding, this entails $\varphi(m'_i) <_p \varphi(m'_j)$, i.e. $m_{i-1} \triangleright_p m_{j+1}$. But this means that the segment $m_i \dots m_j$ may be removed from the cycle, contradicting the minimality of the latter. $\square$

So it suffices to focus on cycles entirely in B, comprising no minimal event.

Let us write $\langle|p \triangleright_{\varphi} q|\rangle$ for $|q| + |p|$, partially ordered by: $(i, m) <_{\langle|p \triangleright_{\varphi} q|\rangle} (j, n)$ iff $i = j = 1$ and $m <_{\langle|q|\rangle} n$, or $i = j = 2$ and $m <_{\langle|p|\rangle} n$. If $m \in |p \triangleright_{\varphi} q|$ is not minimal in $\langle|p \triangleright_{\varphi} q|\rangle$, it has a unique predecessor in $\langle|p \triangleright_{\varphi} q|\rangle$ called its **justifier** and written just($m$). We say $m$ occurring in B has **polarity 1** if it has the form $(1, m')$ with $\text{pol}_{A \vdash B}(\partial_q(m')) = +$, **has polarity r** if
it has the form $(2, m')$ with $\text{pol}_{B \vdash C}(\partial_p(m')) = +$, and **has polarity** $\varphi$ otherwise. We may then write $m^1$, $m^\mathbf{r}$ or $m^\varphi$ instead of $m$, depending on its polarity.

**Lemma A.4.** We have the following properties:

(1) if $m \triangleright_q n^\varphi$, then $m \triangleright_q^* \text{just}(n)$,

(2) if $m \triangleright_p n^\varphi$, then $m \triangleright_p^* \text{just}(n)$,

where the events are annotated with their assumed polarity.

*Proof.* (1) We must have $m = (1, m')$ and $n = (1, n')$ with $m' <_q n'$, with $n'$ negative. By *rule-abiding* and *courtesy*, $\text{just}(n') \to_q n'$. Since $q$ is a forest, $m' \le_q \text{just}(n')$.

(2) Symmetric. $\square$

Now, for any $m \in |p \oplus_{\varphi} q|$, its **depth**, written $\text{depth}(m)$, is 0 if $m$ is minimal in $|(p \oplus_{\varphi} q)|$, otherwise $\text{depth}(\text{just}(m)) + 1$. Now, we prove the *deadlock-free lemma*:

**Lemma A.5.** Consider $q \in \text{Aug}(A \vdash B)$, $p \in \text{Aug}(B \vdash C)$ and $\varphi : x_B^q \cong_B x_B^p$.

Then $\triangleright$ is acyclic.

*Proof.* Seeking a contradiction, assume there is a cycle. By Lemma A.3 it is entirely in $B$, without a minimal event in $B$. Writing it $\rho = m_1 \triangleright \dots \triangleright m_n \triangleright m_1$, define its **depth**

$$ \text{depth}(\rho) = \sum_{i=1}^{n} \text{depth}(m_i), $$

and *w.l.o.g.* assume $\rho$ minimal for the product order on pairs $(n, d)$ where $d = \text{depth}(\rho)$ and $n$ is its length. We notice that $\rho$ has no consecutive $\triangleright_q$ or $\triangleright_p$ – or we shorten the cycle by transitivity, breaking minimality. It also has no consecutive $\triangleright_\varphi$ by definition. This entails that $n = 4k$, with *w.l.o.g.*

$$ m_{4i} \triangleright_q m_{4i+1} \triangleright_\varphi m_{4i+2} \triangleright_p m_{4i+3} \triangleright_\varphi m_{4i+4}, $$

and from now on all indices are considered modulo $n$.

Then $m_{4i+1}$ has polarity 1. Otherwise, it has polarity $\varphi$, making $m_{4i+1} \triangleright_\varphi m_{4i+2}$ impossible. Likewise, $m_{4i+3}$ has polarity $\mathbf{r}$, while $m_{4i+2}$ and $m_{4i+4}$ have polarity $\varphi$.

We claim $\text{just}(m_{4i+1}) \triangleright_q \text{just}(m_{4i})$. Observe $\text{just}(m_{4i+1}) \to_{|(p \oplus_{\varphi} q)|} m_{4i+1}$ by definition; but by *rule-abiding* this entails that $\text{just}(m_{4i+1}) \triangleright_q m_{4i+1}$. Since $q$ is a forest, that makes $\text{just}(m_{4i+1})$ comparable with $m_{4i}$ for $\triangleright_q^*$. If $\text{just}(m_{4i+1}) = m_{4i}$, then

$$ m_{4i-1} \triangleright_p m_{4i+2} $$

since $\varphi$ is a symmetry and by *rule-abiding* – but this allows us to shorten the cycle, contradicting its minimality. Likewise, if $m_{4i} \triangleright_q \text{just}(m_{4i+1})$ then, observing that $\text{just}(m_{4i+1})$ is of polarity $\varphi$ ($m_{4i+1}$ has polarity 1), we obtain

$$ m_{4i} \triangleright_q \text{just}(\text{just}(m_{4i+1})) $$

by Lemma A.4 – we cannot have an equality as they have distinct polarities. But then

$$ m_{4i} \triangleright_q \text{just}(\text{just}(m_{4i+1})) \triangleright_\varphi \text{just}(\text{just}(m_{4i+2})) \triangleright_p m_{4i+3} $$

yielding a cycle with the same length but strictly smaller depth, absurd. The last case remaining has $\text{just}(m_{4i+1}) \triangleright_q m_{4i}$, but so $\text{just}(m_{4i+1}) \triangleright_q \text{just}(m_{4i})$ by Lemma A.4 (again, the equality is impossible for polarity reasons).
With the same reasoning, just($m_{4i+3}$) ▷$_p$ just($m_{4i+2}$); and just($m_{4i+2}$) ▷$_φ$ just($m_{4i+1}$) and just($m_{4i+4}$) ▷$_φ$ just($4i + 3$) by definition. So we can replace the whole cycle with

$$ \mathrm{just}(m_1) \triangleright \mathrm{just}(m_n) \triangleright \dots \triangleright \mathrm{just}(m_1) $$

reversing directions, with the same length but strictly smaller depth, contradiction. □

## APPENDIX B. PROOF OF THE BIALGEBRA DISTRIBUTIVITY LAW

Most laws for the bialgebra structure are straightforward; we detail the exchange rule between $\delta_A$ and $\mu_A$, which is more subtle.

For that, we must first introduce some notation: we write

$$ \mathbf{d}_A \stackrel{\mathrm{def}}{=} (\mathrm{id}_A \otimes \gamma_{A,A} \otimes \mathrm{id}_A) \odot (\delta_A \otimes \delta_A), \qquad \mathbf{g}_A \stackrel{\mathrm{def}}{=} \mu_A \otimes \mu_A $$

for “distribute” and “gather”, which lets us phrase the desired bialgebra law as $\delta_A \odot \mu_A = \mathbf{g}_A \odot \mathbf{d}_A$. We skip the direct verification that, writing $S(x_1, \dots, x_n) = \#\mathrm{Sym}(x_1) \times \dots \times \#\mathrm{Sym}(x_n)$,

$$ \mathbf{d}_A = \sum_{x,y,u,v \in \mathcal{P}(A)} \frac{1}{S(x,y,u,v)} \cdot \mathbf{d}_A^{x,y,u,v} $$

$$ \mathbf{g}_A = \sum_{x,y,u,v \in \mathcal{P}(A)} \frac{1}{S(x,y,u,v)} \cdot \mathbf{g}_A^{x,y,u,v} $$

where $\mathbf{d}_A^{x,y,u,v}$ and $\mathbf{g}_A^{x,y,u,v}$ are isomorphism classes of $\mathbf{d}_A^{x,y,u,v}$ and $\mathbf{g}_A^{x,y,u,v}$ for

$$ (\mathbf{d}_A^{x,y,u,v}) = (x * y) \otimes (u * v) \vdash (x \otimes u) \otimes (y \otimes v) $$

$$ (\mathbf{g}_A^{x,y,u,v}) = (x \otimes y) \otimes (u \otimes v) \vdash (x * y) \otimes (u * v) $$

with the obvious copycat behaviour on each component $x, y, u, v$.

We must introduce some additional notation. Consider A a negative arena and $x \in \mathcal{C}(A)$. We write $x = y \bowtie z$ when $y, z \in \mathcal{C}(A)$, $x = y \cup z$ and $y \cap z = \emptyset$ – this is analogous to $x = y * z$ (and entails $x \cong y * z$), but instead of the tagged disjoint union we have the standard set-theoretic union, which happens to be disjoint. If $x = y \bowtie z$ with $y \in y$ and $z \in z$, we write

$$ x \triangleleft y, z. $$

But there may be several splittings of $x$ into $y$ and $z$, i.e. pairs $(y, z)$ such that $x = y \bowtie z$ with $y \in y$ and $z \in z$. We write $|x \triangleleft y, z|$ the number of such pairs. It is easy to see that this is invariant under symmetry, thus we may write $|x \triangleleft y, z|$ for $|x \triangleleft y, z|$ for any $x \in x$.

For our proof, the first key observation is the following lemma:

**Lemma B.1.** Consider A a negative arena, and $x, y, x', y' \in \mathcal{P}(A)$. Then,

$$ \delta_A^{x,y} \odot \mu_A^{x',y'} = \sum_{\substack{x_l,x_r,y_l,y_r \text{ s.t.} \\ x_l \ast x_r = x, y_l \ast y_r = y \\ x_l \ast y_l = x', x_r \ast y_r = y'}} |x \triangleleft x_l, x_r| |y \triangleleft y_l, y_r| |x' \triangleleft x_l, y_l| |y' \triangleleft y_r, y_r| \cdot \mathbf{g}_A^{x_l,y_l,x_r,y_r} \odot \mathbf{d}_A^{x_l,x_r,y_l,y_r} $$
*Proof.* Consider a symmetry $\varphi : x * y \cong x' * y'$. This symmetry sends some events of $x$ to $x'$, and some others to $y'$ – likewise, it sends some events of $y$ to $x'$, and some to $y'$. Following these partitions, symmetries $\varphi : x * y \cong x' * y'$ are in bijection with

$$ \left\{ \begin{array}{l} x = x_l \bowtie x_r \\ y = y_l \bowtie y_r \\ x' = x'_l \bowtie x'_r \\ y' = y'_l \bowtie y'_r \end{array} \right. , \quad \begin{array}{l} \varphi_{l,l} : x_l \cong x'_l \\ \varphi_{l,r} : x_r \cong y'_l \\ \varphi_{r,l} : y_l \cong x'_r \\ \varphi_{r,r} : y_r \cong y'_r \end{array} $$

Additionally, this decomposition satisfies

$$ \delta_A^{x,y} \odot \varphi \mu_A^{x',y'} = g_A^{x'_l,x'_r,y'_l,y'_r} \odot (\varphi_{l,l} \otimes \varphi_{r,l}) \otimes (\varphi_{l,r} \otimes \varphi_{r,r}) \, d_A^{x_l,x_r,y_l,y_r} $$

which is verified by an immediate analysis of the copycat behaviour of this composition.

To prove the lemma, we then proceed with, for arbitrary $x \in \mathbf{x}, y \in \mathbf{y}, x' \in \mathbf{x}', y' \in \mathbf{y'}$:

$$
\begin{align*}
\delta_A^{x,y} \odot \mu_A^{x',y'}
&= \sum_{\varphi:x*y \cong x'*y'} \overline{\delta_A^{x,y} \odot \varphi \mu_A^{x',y'}} \\
&= \sum_{x=x_l \bowtie x_r} \sum_{y=y_l \bowtie y_r} \sum_{\varphi_{l,l}:x_l \cong x'_l} \overline{g_A^{x'_l,x'_r,y'_l,y'_r} \odot (\varphi_{l,l} \otimes \varphi_{r,l}) \otimes (\varphi_{l,r} \otimes \varphi_{r,r})} \, d_A^{x_l,x_r,y_l,y_r} \\
&= \sum_{x_l,x_r,y_l,y_r \text{ s.t.}} \sum_{x'=x_l \bowtie x_r \text{ s.t. } x_l \in x_l, x_r \in x_r} \sum_{y'=y_l \bowtie y_r \text{ s.t. } y_l \in y_l, y_r \in y_r} \overline{g_A^{x'_l,x'_r,y'_l,y'_r} \odot (\varphi_{l,l} \otimes \varphi_{r,l}) \otimes (\varphi_{l,r} \otimes \varphi_{r,r})} \, d_A^{x_l,x_r,y_l,y_r} \\
&= \sum_{x_l,x_r,y_l,y_r \text{ s.t.}} \sum_{x'=x_l \bowtie x_r \text{ s.t. } x_l \in x_l, x_r \in x_r} \sum_{y'=y_l \bowtie y_r \text{ s.t. } y_l \in y_l, y_r \in y_r} \overline{g_A^{x'_l,x'_r,y'_l,y'_r} \odot d_A^{x_l,x_r,y_l,y_r}} \\
&= \sum_{x_l,x_r,y_l,y_r \text{ s.t.}} |x \diamond x_l, x_r| |y \diamond y_l, y_r| |x' \diamond x_l, y_l| |y' \diamond x_r, y_r| \cdot g_A^{x_l,y_l,x_r,y_r} \odot d_A^{x_l,x_r,y_l,y_r}.
\end{align*}
$$

by the definition of composition of isogmentations (which does not depend on the chosen representative); the observation above; reorganizing the sum by symmetry classes; again via the definition of composition of isogmentations; and by definition of splittings. $\square$

This is sufficient to ensure that $\delta_A \odot \mu_A$ and $g_A \odot d_A$ have the same isogmentations, but not that they occur with the same coefficient. For that, the next key observation is:

**Lemma B.2.** Consider A a negative arena, and $x, y \in \mathcal{P}(A)$. Then,

$$ \#\mathrm{Sym}(x * y) = |x * y \diamond x, y| \times \#\mathrm{Sym}(x) \times \#\mathrm{Sym}(y). $$
*Proof.* Fix arbitrary $x \in x$ and $y \in y$ that we assume disjoint, and $z = x \bowtie y \in x * y$. The set of symmetries on $x * y$ is clearly in bijection with the set of symmetries

$$ \varphi : z \cong x * y $$

which we shall study. As in the lemma above, such a symmetry sends some events of $z$ to $x$ and some to $y$; this induces a splitting $z = x' \bowtie y'$ with induced $\varphi_x : x' \cong x$ and $\varphi_y : y' \cong y$, so that $x' \in x$ and $y' \in y$. Conversely, any such splitting of $z$ with accompanying symmetries yields a symmetry $z \cong x * y$. From this it is straightforward to obtain a bijection witnessing the announced equality (keeping in mind that we may fix in advance a chosen $\kappa_x : x \cong \underline{x}$ for all $x \in x$, so as to bridge between symmetries $x' \cong x$ and endosymmetries $\underline{x} \cong \bar{x}$). $\square$

With this in place, we may finally prove the exchange law of bialgebras:

$$
\begin{align*}
\delta_A \odot \mu_A
&= \sum_{\substack{x,y \in \mathcal{P}(A) \\ x',y' \in \mathcal{P}(A)}} \frac{1}{S(x,y,x',y')} \cdot \delta_A^{x,y} \odot \mu_A^{x',y'} \\
&= \sum_{\substack{x,y \in \mathcal{P}(A) \\ x',y' \in \mathcal{P}(A)}} \sum_{\substack{x_l,x_r,y_l,y_r \text{ s.t.} \\ x_l*x_r=x, y_l*y_r=y \\ x_l*y_l=x', x_r*y_r=y'}} \frac{|x \diamond x_l, x_r| |y \diamond y_l, y_r| |x' \diamond x_l, y_l| |y' \diamond x_r, y_r|}{S(x,y,x',y')} \cdot g_A^{x_l,y_l,x_r,y_r} \odot d_A^{x_l,x_r,y_l,y_r} \\
&= \sum_{\substack{x_l,x_r,y_l,y_r \in \mathcal{P}(A)}} \frac{|x \diamond x_l, x_r| |y \diamond y_l, y_r| |x' \diamond x_l, y_l| |y' \diamond x_r, y_r|}{S(x_l * x_r, y_l * y_r, x_l * y_l, x_r * y_r)} \cdot g_A^{x_l,y_l,x_r,y_r} \odot d_A^{x_l,x_r,y_l,y_r} \\
&= \sum_{\substack{x_l,x_r,y_l,y_r \in \mathcal{P}(A)}} \frac{1}{S(x_l, x_r, y_l, y_r)^2} \cdot g_A^{x_l,y_l,x_r,y_r} \odot d_A^{x_l,x_r,y_l,y_r} \\
&= \left( \sum_{\substack{x_l,x_r,y_l,y_r \in \mathcal{P}(A)}} \frac{1}{S(x_l, x_r, y_l, y_r)} \cdot g_A^{x_l,y_l,x_r,y_r} \right) \odot \left( \sum_{\substack{x_l,x_r,y_l,y_r \in \mathcal{P}(A)}} \frac{1}{S(x_l, x_r, y_l, y_r)} \cdot d_A^{x_l,y_l,x_r,y_r} \right) \\
&= g_A \odot d_A
\end{align*}
$$

by first unfolding the definitions of $\delta_A$ and $\mu_A$; then by Lemma B.1; then re-indexing the sum in the obvious way; then applying Lemma B.2; and finally by linearity, observing that all the compositions $g_A^{x_l,y_l,x_r,y_r} \odot d_A^{x'_l,x'_r,y'_l,y'_r}$ where one of $x_l = x'_l, y_l = x'_r, x_r = y'_l$ and $y_r = y'_r$ does not hold is null.

## REFERENCES

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

[Bar84] Hendrik Pieter Barendregt. *The lambda calculus - its syntax and semantics*, volume 103 of *Studies in logic and the foundations of mathematics*. North-Holland, 1984.

[BC21] Lison Blondeau-Patissier and Pierre Clairambault. Positional injectivity for innocent strategies. In Naoki Kobayashi, editor, *6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference)*, volume 195 of *LIPIcs*, pages 17:1–17:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LIPIcs.FSCD.2021.17.
[BCEM12] Antonio Bucciarelli, Alberto Carraro, Thomas Ehrhard, and Giulio Manzonetto. Full abstraction for the resource lambda calculus with tests, through Taylor expansion. *Log. Methods Comput. Sci.*, 8(4), 2012. doi:10.2168/LMCS-8(4:3)2012.

[BCLS20] Richard Blute, J. Robin B. Cockett, Jean-Simon Pacaud Lemay, and Robert A. G. Seely. Differential categories revisited. *Appl. Categorical Struct.*, 28(2):171–235, 2020. doi:10.1007/s10485-019-09572-y.

[BCS06] Richard Blute, J. Robin B. Cockett, and Robert A. G. Seely. Differential categories. *Math. Struct. Comput. Sci.*, 16(6):1049–1083, 2006. doi:10.1017/S0960129506005676.

[BCS09] Richard F. Blute, J. Robin B. Cockett, and Robert A. G. Seely. Cartesian differential categories. *Theory and Applications of Categories*, 22(23):622–672, 2009. URL: http://www.tac.mta.ca/tac/volumes/22/23/22-23.pdf.

[BCVA23a] Lison Blondeau-Patissier, Pierre Clairambault, and Lionel Vaux Auclair. Extensional taylor expansion. *CoRR*, abs/2305.08489, 2023. arXiv:2305.08489, doi:10.48550/ARXIV.2305.08489.

[BCVA23b] Lison Blondeau-Patissier, Pierre Clairambault, and Lionel Vaux Auclair. Strategies as resource terms, and their categorical semantics. In Marco Gaboardi and Femke van Raamsdonk, editors, *8th International Conference on Formal Structures for Computation and Deduction, FSCD 2023, July 3-6, 2023, Rome, Italy*, volume 260 of *LIPIcs*, pages 13:1–13:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPICS.FSCD.2023.13.

[BEM10] Antonio Bucciarelli, Thomas Ehrhard, and Giulio Manzonetto. Categorical models for simply typed resource calculi. In *MFPS*, volume 265 of *Electronic Notes in Theoretical Computer Science*, pages 213–230. Elsevier, 2010. doi:10.1016/j.entcs.2010.08.013.

[Blo24] Lison Blondeau-Patissier. Resource Categories from Differential Categories. In *JFLA 2024 - 35es Journées Francophones des Langages Applicatifs*, Saint-Jacut-de-la-Mer, France, January 2024. URL: https://inria.hal.science/hal-04406440.

[BM20] Davide Barbarossa and Giulio Manzonetto. Taylor subsumes Scott, Berry, Kahn and Plotkin. *Proc. ACM Program. Lang.*, 4(POPL):1–1:1–23, 2020. doi:10.1145/3371069.

[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.

[CC24] Simon Cattellan and Pierre Clairambault. Disentangling parallelism and interference in game semantics. *Log. Methods Comput. Sci.*, 20(3), 2024. doi:10.46298/LMCS-20(3:24)2024.

[CCRW17] Simon Castellan, Pierre Clairambault, Silvain Rideau, and Glynn Winskel. Games and strategies as event structures. *Log. Methods Comput. Sci.*, 13(3), 2017. doi:10.23638/LMCS-13(3:35)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. doi:10.23638/LMCS-15(1:18)2019.

[ER03] Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. *Theor. Comput. Sci.*, 309(1-3):1–41, 2003. doi:10.1016/S0304-3975(03)00392-X.

[ER06] Thomas Ehrhard and Laurent Regnier. Differential interaction nets. *Theor. Comput. Sci.*, 364(2):166–195, 2006. doi:10.1016/j.tcs.2006.08.003.

[ER08] Thomas Ehrhard and Laurent Regnier. Uniformity and the Taylor expansion of ordinary lambda-terms. *Theor. Comput. Sci.*, 403(2-3):347–372, 2008. doi:10.1016/j.tcs.2008.06.001.

[GvR23] Marco Gaboardi and Femke van Raamsdonk, editors, *8th International Conference on Formal Structures for Computation and Deduction, FSCD 2023, July 3-6, 2023, Rome, Italy*, volume 260 of *LIPIcs*. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://www.dagstuhl.de/dagpub/978-3-95977-277-8.

[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.

[Lai05] Jim Laird. A game semantics of the asynchronous pi-calculus. In *CONCUR*, volume 3653 of *Lecture Notes in Computer Science*, pages 51–65. Springer, 2005. doi:10.1007/11539452_8.

[Man12] Giulio Manzonetto. What is a categorical model of the differential and the resource λ-calculi? *Math. Struct. Comput. Sci.*, 22(3):451–520, 2012. doi:10.1017/S0960129511000594.

[Mel06] Paul-André Melliès. Asynchronous games 2: The true concurrency of innocence. *Theor. Comput. Sci.*, 358(2-3):200–228, 2006. doi:10.1016/j.tcs.2006.01.016.
[Mel09] Paul-André Melliès. *Categorical semantics of linear logic*, volume 27 of *Panoramas et synthèses*, pages 1–196. Société Mathématique de France, 2009.

[Nak75] Reiji Nakajima. Infinite normal forms for the lambda - calculus. In Corrado Böhm, editor, *Lambda-Calculus and Computer Science Theory, Proceedings of the Symposium Held in Rome, Italy, March 25-27, 1975*, volume 37 of *Lecture Notes in Computer Science*, pages 62–82. Springer, 1975. doi:10.1007/BFb0029519.

[ST17] Ken Sakayori and Takeshi Tsukada. A truly concurrent game model of the asynchronous π-calculus. In Javier Esparza and Andrzej S. Murawski, editors, *Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings*, volume 10203 of *Lecture Notes in Computer Science*, pages 389–406, 2017. doi:10.1007/978-3-662-54458-7_23.

[TO16] Takeshi Tsukada and C.-H. Luke Ong. Plays as resource terms via non-idempotent intersection types. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, *Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016*, pages 237–246. ACM, 2016. doi:10.1145/2933575.2934553.