# Strategies as Resource Terms, and Their Categorical Semantics

Lison Blondeau-Patissier, Pierre Clairambault, Lionel Vaux Auclair

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

## To cite this version:

Lison Blondeau-Patissier, Pierre Clairambault, Lionel Vaux Auclair. Strategies as Resource Terms, and Their Categorical Semantics. 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023), Jul 2023, Rome, Italy. 10.4230/LIPIcs.FSCD.2023.13. [https://hal.science/hal-04244568v1](https://hal.science/hal-04244568v1)

HAL Id: hal-04244568

Submitted on 16 Oct 2023

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_2.png" /></figure>
# Strategies as Resource Terms, and Their Categorical Semantics

Lison Blondeau-Patissier ☑

Aix Marseille Univ, CNRS, I2M and LIS, Marseille, France

Pierre Clairambault ☑ ID

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

Aix Marseille Univ, CNRS, LIS, Marseille, France

Lionel Vaux Auclair ☑ ID

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

Aix Marseille Univ, CNRS, I2M, Marseille, France

## 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. Though inspiring, their proof is indirect, relying on the injectivity of the relational model w.r.t. 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.

**2012 ACM Subject Classification** Theory of computation → Denotational semantics; Theory of computation → Categorical semantics

**Keywords and phrases** Resource calculus, Game semantics, Categorical semantics

**Digital Object Identifier** 10.4230/LIPIcs.FSCD.2023.13

**Related Version** Full Version: https://arxiv.org/abs/2302.04685

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

Lionel Vaux Auclair: Supported by the ANR projects PPS (ANR-19-CE48-0014), LambdaComb (ANR-21-CE48-0017) and Reciprog (ANR-21-CE48-0019).

## 1 Introduction

The *Taylor expansion* of programs 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* [13], reifying syntactically features of certain vectorial models of linear logic. Since its inception [15], 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 $\lambda$-calculus [2].

*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 [16, 1]. How different is the Taylor expansion of the $\lambda$-calculus from its game semantics?

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

© Lison Blondeau-Patissier, Pierre Clairambault, and Lionel Vaux Auclair; licensed under Creative Commons License CC-BY 4.0

8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023).

Editors: Marco Gaboardi and Femke van Raamsdonk; Article No. 13; pp. 13:1–13:22

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

LIPICS

Leibniz International Proceedings in Informatics

Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
13:2 Strategies as Resource Terms, and Their Categorical Semantics

Not very different, suggest Tsukada and Ong [23], who show that certain normal and η-long
resource terms correspond bijectively to plays in the sense of Hyland-Ong game semantics [16],
up to Opponent's scheduling of the independent explorations of separate branches of the
term, as formalized by Melliès' homotopy equivalence on plays [19].

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 [23], 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 [4]. This was inspired by concurrent games [11] – similar causal structures existed before, first suggested in [17], and fleshed out more in [22]. In [4], 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: see Section 3.2.

We moreover strive to account for non-normal resource terms and *reduction* in the resource calculus, which we recall in Section 2. 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 [4] – 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, as discussed in Section 3.3. 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, in Section 4. And, in Section 5, we 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 [23] considered some dynamic aspects of the correspondence: they proved their bijection 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 results constitute a first step to flesh out this isomorphism into the diagrams:

<figure><img src="image_7.png" /></figure>
where M is a λ-term, s is a resource term, T is Taylor expansion, N is normalization and
$\llbracket - \rrbracket$ is game semantics. Square (a) should commute essentially by definition, while square (b)
should be deduced from (c): we leave the treatment of Taylor expansion for future work (see
also the next paragraphs and Section 6) but (c) already follows from our present results.

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 correspondence between differential categories [5] and resource categories is
also left for future work. Anyway, we 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 [14]: 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 6) that our category of games does induce a cartesian closed differential category
[6, 9, 18]; more generally, we plan to study how this generalizes to any resource category –
provided the necessary sums of morphisms are available.

**Outline.** In Section 2, we detail our resource calculus. In Section 3 we introduce augmentations, show the correspondence with normal resource terms, and introduce strategies. In Section 4 we introduce resource categories, define the interpretation of the resource calculus, and prove that it is invariant under reduction. In Section 5, we show that strategies form a resource category. We conclude in Section 6.

## 2 The Simply-Typed η-Expanded Resource Calculus

**Preliminaries.** 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}, \text{ 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}, \text{ etc.}$ We write $[a_1, \dots, a_n]$ for the bag $\vec{a}$ defined by a list $\vec{a} = \langle a_1, \dots, a_n \rangle$ of elements: we then say $\vec{a}$ is an **enumeration** of $\vec{a}$. We write $\llbracket \rangle$ for the empty bag, and use $*$ for bag concatenation. We also write $|\vec{a}|$ for the size of $\vec{a}$: $|\vec{a}|$ is 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} \llbracket k \rrbracket$. 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 sum

$$ \sum_{\vec{a} \llbracket \vec{a}_1^* \cdots \vec{a}_k \rrbracket} f(\vec{a}_1, \dots, \vec{a}_k) \stackrel{\text{def}}{=} \sum_{p: \vec{a} \llbracket k \rrbracket} f(\vec{a} \upharpoonright_p 1, \dots, \vec{a} \upharpoonright_p k) $$

is independent of the enumeration. When indexing a sum with $\vec{a} \llbracket \vec{a}_1^* \cdots \vec{a}_k \rrbracket$ we thus mean
to sum over all partitionings $p: \vec{a} \llbracket k \rrbracket, \vec{a}_i$ being shorthand for $\vec{a} \upharpoonright_p i$ in the summand.

We will also use tuples of bags: we write $\mathcal{S}(X)$ for $\mathcal{B}(X)^*$. We denote elements of $\mathcal{S}(X)$ as
$\vec{a}, \vec{b}, \text{ etc.}$ just like for plain tuples, but we reserve the name **sequence** for such tuples of bags.
A **k-partitioning** $p: \vec{a} \llbracket k \rrbracket$ of $\vec{a} = \langle a_1, \dots, a_n \rangle$ is a tuple $p = \langle p_1, \dots, p_n \rangle$ of k-partitionings
13:4 Strategies as Resource Terms, and Their Categorical Semantics

$$
\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} &
(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]
\\[1em]
(\lambda z.s) \langle \bar{t} / x \rangle &\stackrel{\text{def}}{=} \lambda z.s \langle \bar{t} / x \rangle
\end{align*}
$$

<caption>Figure 1 Inductive definition of substitution (z is chosen fresh in the abstraction case).</caption>

$$
\frac{\overline{(\lambda x.s) \bar{t} \to s(\bar{t}/x)}}{\lambda x.s \to \lambda x.S'} \qquad \frac{s \to S'}{s \bar{t} \to S' \bar{t}} \qquad \frac{s \to S'}{[s] * \bar{t} \to [S'] * \bar{t}} \qquad \frac{\bar{t} \to \bar{T}'}{s \bar{t} \to s \bar{T}'}
$$

<caption>Figure 2 Rules of single-step reduction.</caption>

$p_i : \bar{a}_i \triangleleft k$. This defines a **partition** $\langle \bar{a} \upharpoonright p_1, \dots, \bar{a} \upharpoonright p_k \rangle$, component-wise: each $\bar{a} \upharpoonright i$ is the sequence $\langle \bar{a}_1 \upharpoonright p_1, \dots, \bar{a}_n \upharpoonright p_n \rangle$. We obtain $\bar{a} = \bar{a} \upharpoonright p_1 * \dots * \bar{a} \upharpoonright p_k$, applying the concatenation of bags component-wise, to sequences all of the same length $n$. And, just as before, the result of the following sum is independent from the enumeration of the bags of $\bar{a}$:

$$
\sum_{\vec{a} \triangleleft \vec{a}_1 \cdots \triangleleft \vec{a}_k} f(\vec{a}_1, \dots, \vec{a}_k) \stackrel{\text{def}}{=} \sum_{p: \vec{a} \triangleleft k} f(\vec{a} \upharpoonright p_1, \dots, \vec{a} \upharpoonright p_k).
$$

**Resource calculus.** The terms of the resource calculus [15] are just like $\lambda$-terms, except that, in an application, the argument is a bag of terms instead of just one term. We denote terms by $s, t, u$ and bags of terms by $\bar{s}, \bar{t}, \bar{u}$, and write $\Delta$ for the set of terms:

$$
\Delta \ni s, t, u, \dots ::= x \mid \lambda x.s \mid s[t_1, \dots, t_n] \ .
$$

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 (non-idempotent) sum $s \langle \bar{t}/x \rangle$ of terms obtained by substituting each element of $\bar{t}$ for exactly one occurrence of $x$ in $s$. The inductive definition is in Figure 1, 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$. 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$ – those may be considered as finite multisets, but we adopt a distinct additive notation to avoid confusion with bags. 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 **reduction of resource terms** $\rightarrow \subseteq \Delta \times \Sigma(\Delta)$ is given in Figure 2. It is extended to $\Sigma(\Delta) \times \Sigma(\Delta)$ by setting $S \rightarrow S'$ whenever $S = t + U$ and $S' = T' + U$ with $t \rightarrow T'$.

► **Theorem 1** ([15]). The reduction $\rightarrow$ on $\Sigma(\Delta)$ is confluent and strongly normalizing.
<figure><img src="image_8.png" /><figcaption>Figure 3 Typing rules for the simply-typed resource calculus.</figcaption></figure>

**Typing and expanded terms.** In the remainder of the paper, we will consider a simply typed version of the resource calculus, based on the following grammar of types

$$F, G, H, \dots ::= o \mid F \to G$$

for a single base type $o$. If $\vec{F} = (F_1, \dots, F_n)$, we write $\vec{F} \to G \stackrel{\text{def}}{=} F_1 \to \dots \to F_n \to G = F_1 \to (\dots \to (F_n \to G) \dots)$. Then any type $H$ can be written uniquely as $H = \vec{F} \to o$.

The above strong normalization result holds in the untyped setting. We use typing only to enforce a syntactic constraint on terms: our resource expressions are $\eta$-expanded, i.e. values of type $\vec{F} \to o$ are terms $\lambda x_1 \dots \lambda x_{|\vec{F}|} s$ with $s$ of type $o$. We fix a type for each variable, so that each type has infinitely many variables – and write $x : F$ for $F$ 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 : F_1, \dots, x_n : F_n$, abbreviated as $\vec{x} : \vec{F}$; 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 S(\Delta) = \mathcal{B}(\Delta)^*$. Given a term $s$ and a resource sequence $\vec{t} = (\vec{t}_1, \dots, \vec{t}_k)$, we also define the application $s \vec{t} \stackrel{\text{def}}{=} s \vec{t}_1 \dots \vec{t}_k = (\dots (s \vec{t}_1) \dots) \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_{\bar{t} \prec \bar{t}_1 * \dots * \bar{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_{\bar{t} \prec \bar{t}_1 * \bar{t}_2} (s \langle \bar{t}_1 / x \rangle) (\vec{u} \langle \bar{t}_2 / x \rangle)$, as in the application case of Figure 1.

The type system appears in Figure 3. For $X \in \{\text{Val}, \text{Base}, \text{Bag}, \text{Seq}\}$, we write $X(\Gamma; F)$ for the set of those $s$ s.t. $\Gamma \vdash_X s : F$. For $X = \text{Base}$ we have $F = o$, so we set $\text{Base}(\Gamma) \stackrel{\text{def}}{=} \text{Base}(\Gamma; o)$. If $\Gamma \vdash_X s : F$, then $s$ is in normal form iff the judgment is derived without (hr) – we write $X_{\text{nf}}(\Gamma; F)$ for the elements of $X(\Gamma; F)$ in normal form. We write $\Sigma X(\Gamma; F)$ for $\Sigma(X(\Gamma; F))$.

**► Lemma 2 (Subject reduction).** If $S \in \Sigma \text{Val}(\Gamma; F)$ and $S \to S'$ then $S' \in \Sigma \text{Val}(\Gamma; F)$.

This follows from substitution lemmas for our four kinds of typed terms, proved by mutual induction: if $\Gamma, x : F \vdash_X t : G$ and $\Gamma \vdash_{\text{Bag}} \bar{s} : F$ then $t \langle \bar{s} / x \rangle \in \Sigma X(\Gamma; G)$.

We also consider a many-step variant of resource reduction, following the structure of expanded terms. We set $s \langle \vec{t} / \vec{x} \rangle \stackrel{\text{def}}{=} s \langle \bar{t}_1 / x_1 \rangle \dots \langle \bar{t}_n / x_n \rangle$ when $\vec{x} = (x_1, \dots, x_n)$, $\vec{t} = (\bar{t}_1, \dots, \bar{t}_n)$, and no $x_i$ occurs free in $\vec{t}$. The **many-step reduction** $\Rightarrow$ is then defined from the base case

$$(\lambda \vec{x} . s) \vec{t} \in \text{Base}(\Gamma) \Rightarrow s \langle \vec{t} / \vec{x} \rangle \in \Sigma \text{Base}(\Gamma) \quad (\text{assuming } |\vec{x}| = |\vec{t}| \neq 0),$$

extended contextually to each syntactic kind of typed expressions, following inductively the type system of Figure 3, and then to sums as for $\to$. It is clear that $\Rightarrow \subset \to^+$ (the transitive closure of $\to$), and that an expanded term is $\Rightarrow$-reducible iff it is $\to$-reducible: it follows that $\Rightarrow$ is strongly normalizing, with the same normal forms as $\to$. In particular $\Rightarrow$ is confluent.
13:6 Strategies as Resource Terms, and Their Categorical Semantics

<figure><img src="image_9.png" /><figcaption>Figure 4 A play in HO games.</figcaption></figure>

<figure><img src="image_10.png" /><figcaption>Figure 5 A homotopic play.</figcaption></figure>

3 Resource Terms as Augmentations

**Plays in game semantics.** In Hyland-Ong game semantics [16] executions are formalized as *plays*, drawn as in Figure 4, read temporally from top to bottom. Nodes are called *moves*, negative (from Opponent / the environment) or positive (from Player / the program) – each corresponds to a resource call, and the dotted lines, called *justification pointers*, carry the hierarchical relationship between those calls. Both Figures 4 and 5 represent plays for

$$ \vdash \lambda f^{(o \to o)} \to (o \to o) \to o. f (\lambda x^o. x) (\lambda y^o. y) : ((o \to o) \to (o \to o) \to o) \to o, $$

where Figure 4 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, Opponents prompts $f$ to call its first argument, to which Player responds the $q^+$ on the fourth line: a call to $x$. Subsequently Opponent evaluates the second argument of $f$ – Player responds by calling $y$ – and then Opponent calls the first argument again.

**Plays and resource terms.** In [23], 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 explicitly resource usage: in Figure 4, the first argument of $f$ is evaluated *twice* while the second one is evaluated *once* – following Tsukada and Ong’s correspondence, the play is written $s = \lambda f. f [\lambda x. x, \lambda x. x] [\lambda y. y]$ in the resource calculus. However, Figure 5 also corresponds to $s$! Tsukada and Ong actually establish a bijection between (normal) resource terms and plays *up to* Melliès’ *homotopy relation* [19], relating plays which, like Figures 4 and 5, only differ via Opponent’s scheduling. But then, is there a more explicit representation of plays *up to* homotopy?

As a matter of fact, there is. In [4], Blondeau-Patissier and Clairambault introduced a *causal* representation of innocent strategies (inspired from *concurrent games* [11, 12] – see also [22]) 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 as in Figure 6 in which the trained eye can read exactly the same data as in the resource term $s$: 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 refine Tsukada and Ong’s result into a bijection of resource terms with *augmentations*.
$$((o \rightarrow o) \rightarrow (o \rightarrow o) \rightarrow o) \rightarrow o$$

<figure><img src="image_11.png" /><figcaption>Figure 6 An augmentation.</figcaption></figure>

$$((o \rightarrow o) \rightarrow (o \rightarrow o) \rightarrow o) \rightarrow o$$

<figure><img src="image_12.png" /><figcaption>Figure 7 An arena.</figcaption></figure>

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

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

<figure><img src="image_15.png" /><figcaption>Figure 8 Arena bool.</figcaption></figure>

<caption>Figure 9 Arena nat.</caption>

<caption>Figure 10 Arena ($o \Rightarrow o \Rightarrow o$).</caption>

## 3.1 Arenas, Positions, Augmentations

**► Definition 3.** An arena is $A = \langle |A|, \le_A, \text{pol}_A \rangle$ where $\langle |A|, \le_A \rangle$ is a (countable) partial order, and $\text{pol}_A : |A| \to \{-, +\}$ is a *polarity function*. These data must satisfy:

finitary: for all $a \in |A|$, $[a]_A \stackrel{\text{def}}{=} \{a' \in |A| \mid a' \le_A a\}$ is finite,

forestial: for all $a_1, a_2 \le_A a$, then $a_1 \le_A a_2$ or $a_2 \le_A a_1$,

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

where $a_1 \to_A a_2$ means $a_1 <_A a_2$ with no event strictly in between. A **--arena** is additionally negative, i.e. $\text{pol}_A(a) = - \text{ for all } a \in \min(A) \stackrel{\text{def}}{=} \{a \in |A| \mid a \text{ minimal}\}$.

Elements of $|A|$ are called *events* or *moves* interchangeably. An **isomorphism** $\varphi : A \cong B$ between arenas is a bijection between events preserving and reflecting all 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. In arenas we draw the immediate causality $\to$ as dotted lines, read from top to bottom. Figures 8 and 9 show the arenas **bool** and **nat**. In those arenas, *initial* (i.e. minimal) moves are Opponent moves starting computation, to which Player may respond with a value.

**Constructions.** We write $X + Y$ for the disjoint union $(\{1\} \times X) \cup (\{2\} \times Y)$ of sets.

**► Definition 4.** The tensor of arenas $A_1$ and $A_2$ is defined in Figure 11.

If additionally $A_1$ and $A_2$ are **--arenas** and $A_2$ is **pointed**, i.e. $\min(A_2)$ is a singleton, then the **arrow** $A_1 \Rightarrow A_2$, a pointed **--arena**, is defined in Figure 12.

The tensor directly extends to countable arity, and each arena decomposes as $A \cong \bigotimes_{i \in I} A_i$ with $A_i$ pointed. We set $A^\perp$ as $A$ with polarities reversed. We write $A \vdash B$ for $A^\perp \otimes B$, $1$ is the empty arena and $o$ has exactly one (negative) move $q$. We interpret types as arenas via $[[o]] = o$ and $[[A \to B]] = [[A]] \Rightarrow [[B]]$, and contexts via $[[\Gamma]] = \bigotimes_{(x:A) \in \Gamma} [[A]]$. Figure 10 shows the interpretation of $(o \to o) \to o \to o$, following the longstanding game semantics convention that keeps moves distinct by attempting to always place them under the corresponding atom.
13:8 Strategies as Resource Terms, and Their Categorical Semantics

$$
\begin{align*}
|A_1 \otimes A_2| &= |A_1| + |A_2| \\
(i, a) \le_{A_1 \otimes A_2} (j, b) &\Leftrightarrow \begin{array}[t]{l} i = j \wedge a \le_{A_i} b \\ \text{pol}_{A_1 \otimes A_2}(i, a) = \text{pol}_{A_i}(a). \end{array} \\
|A_1 \Rightarrow A_2| &= |A_1| + |A_2| \\
(i, a) \le_{A_1 \Rightarrow A_2} (j, b) &\Leftrightarrow \begin{array}[t]{l} (i = j \wedge a \le_{A_i} b) \\ \vee \ (i = 2 \wedge a \in \min(A_2)) \\ \text{pol}_{A_1 \Rightarrow A_2}(i, a) = (-1)^i \cdot \text{pol}_{A_i}(a), \end{array}
\end{align*}
$$

<caption>Figure 11 Tensor of arenas.</caption>

<caption>Figure 12 Arrow of arenas.</caption>

**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 [7] under the name *thick subtrees*. Here, by analogy with concurrent games [11], we call them configurations:

► **Definition 5.** A configuration $x \in \mathcal{C}(A)$ of arena A is $x = (|x|, \le_x, \partial_x)$ such that $\langle |x|, \le_x \rangle$ is a finite forest, and the display map $\partial_x: |x| \to |A|$ is a function s.t.:

minimality-respecting: for any $a \in |x|$, $a$ is $\le_x$-minimal iff $\partial_x(a)$ is $\le_A$-minimal,

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** (noted $x \in \mathcal{C}_\bullet(\mathcal{A})$) if it has exactly one minimal event $\text{init}(x)$.

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 $\to$, Figure 6 is a configuration on Figure 7 – notice that the branch on the left hand side is explored twice.

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-iso 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$, 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 $\underline{x} \in \mathcal{C}(A)$ a representative. In [4], 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 \triangleright y \in \mathcal{C}(A \vdash B)$ similarly.

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

► **Definition 6.** An augmentation on arena $A$ is a tuple $\mathbf{q} = (\langle |\mathbf{q}|, \le_{\langle |\mathbf{q}|\rangle}, \le_q, \partial_q \rangle$, where $\langle |\mathbf{q}| \rangle = \langle |\mathbf{q}|, \le_{\langle |\mathbf{q}|\rangle}, \partial_q \rangle \in \mathcal{C}(A)$, and $\langle |\mathbf{q}|, \le_q \rangle$ is a forest satisfying:

rule-abiding: for all $a_1, a_2 \in |\mathbf{q}|$, if $a_1 \le_{\langle |\mathbf{q}|\rangle} 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_{\langle |\mathbf{q}|\rangle} a_2$,

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

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

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

we then write $\mathbf{q} \in \text{Aug}(A)$, and call $\langle |\mathbf{q}| \rangle \in \mathcal{C}(A)$ the **desequentialization** of $\mathbf{q}$.

Finally, $\mathbf{q}$ is **pointed** if it has a unique minimal event, written $\mathbf{q} \in \text{Aug}_\bullet(\mathcal{A})$.

Figure 6 represents an augmentation $\mathbf{q}$ by showing both relations $\to_{\langle |\mathbf{q}|\rangle}$ (as dotted lines) and $\to_q$. An augmentation $\mathbf{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 [4].
**Isoglementations.** Augmentations are also considered up to iso. An isomorphism $\varphi: q \cong p$ is a bijection preserving and reflecting all structure. An isoglementation is an isomorphism class of augmentations, ranged over by $\mathbf{q}, \mathbf{p}$, etc.: we write $\mathrm{Isog}(A)$ (resp. $\mathrm{Isog}_{\bullet}(A)$) for isoglementations (resp. pointed isoglementations). If $\mathbf{q} \in \mathrm{Aug}(A)$, we write $\bar{\mathbf{q}} \in \mathrm{Isog}(A)$ for its isomorphism class; reciprocally, if $\mathbf{q} \in \mathrm{Isog}(A)$, we fix a representative $\underline{\mathbf{q}} \in \mathbf{q}$.

## 3.2 Isoglementations are Normal Resource Terms

Now we spell out the link between isoglementations and normal resource terms. We first show how the structure of each syntactic kind of terms is reflected by augmentations of the appropriate type. The main result (Theorem 12) follows directly.

**Tensors and sequences.** To reflect the syntactic formation rule for sequences, we show that isoglementations on $A_1 \otimes \dots \otimes A_n$ are tuples. Consider --arenas $\Gamma, A_1, \dots, A_n$, and $\mathbf{q}_i \in \mathrm{Aug}(\Gamma \vdash A_i)$ for $1 \le i \le n$. We set $\bar{\mathbf{q}} = (\langle \mathbf{q}_i | 1 \le i \le n \rangle \in \mathrm{Aug}(\Gamma \vdash \otimes_{1 \le i \le n} A_i))$ with

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

with the two orders $\leq_{\bar{\mathbf{q}}}$ and $\leq_{(\langle \mathbf{q}_i | 1 \le i \le n \rangle)}$ inherited. It is immediate that this construction preserves isomorphisms, so that it extends to isoglementations.

**Proposition 7.** There is a bijection $\langle - , \dots , - \rangle : \prod_{i=1}^n \mathrm{Isog}(\Gamma \vdash A_i) \cong \mathrm{Isog}(\Gamma \vdash \otimes_{1 \le i \le n} A_i)$.

**Proof.** By negative and forestial, any $\mathbf{q} \in \mathrm{Aug}(\Gamma \vdash \otimes_{1 \le i \le n} A_i)$ is isomorphic to some $(\langle \mathbf{q}_i | 1 \le i \le n \rangle)$; this is compatible with isos as they respect display maps. ◀

**Bags and pointedness.** Likewise, isoglementations are bags of pointed isoglementations.

We start by showing the corresponding construction. Consider --arenas $\Gamma$ and $A$, and $\mathbf{q}_1, \mathbf{q}_2 \in \mathrm{Aug}(\Gamma \vdash A)$. We set $\mathbf{q}_1 * \mathbf{q}_2 \in \mathrm{Aug}(\Gamma \vdash A)$ with events $|\mathbf{q}_1 * \mathbf{q}_2| = |\mathbf{q}_1| + |\mathbf{q}_2|$, and display $\partial_{\mathbf{q}_1 * \mathbf{q}_2}(i, m) = \partial_{\mathbf{q}_i}(m)$, and the two orders $\leq_{\mathbf{q}_1 * \mathbf{q}_2}$ and $\leq_{(\langle \mathbf{q}_1 * \mathbf{q}_2 \rangle)}$ inherited. This generalizes to an n-ary operation in the obvious way, which preserves isomorphisms. The operation induced on isoglementations is associative and admits as neutral element the empty isoglementation $1 \in \mathrm{Isog}(\Gamma \vdash A)$ with (a unique representative with) no event.

**Proposition 8.** There is a bijection $- * \dots * - : \mathcal{B}(\mathrm{Isog}_{\bullet}(\Gamma \vdash A)) \cong \mathrm{Isog}(\Gamma \vdash A)$.

**Proof.** As $\mathbf{q} \in \mathrm{Aug}(\Gamma \vdash A)$ is a finite forest, it is isomorphic to a bag of trees. ◀

**Currying.** For --arenas $\Gamma, A$ and $B$, we have $\Lambda_{\Gamma,A,B} : \mathrm{Aug}(\Gamma \otimes A \vdash B) \cong \mathrm{Aug}(\Gamma \vdash A \Rightarrow B)$ a bijection compatible with isos, which leaves the core of the augmentation unchanged and only reassigns the display map in the unique sensible way. Hence we obtain:

**Proposition 9.** For every --arenas $\Gamma, A_1, \dots, A_n$, there is

$$\Lambda_{\Gamma, \bar{\Gamma}} : \mathrm{Isog}_{\bullet}(\Gamma \otimes A_1 \otimes \dots \otimes A_n \vdash o) \cong \mathrm{Isog}_{\bullet}(\Gamma \vdash A_1 \Rightarrow \dots \Rightarrow A_n \Rightarrow o).$$

**Head occurrence.** The above cases handle syntactic kinds Seq, Bag and Val, following the rules (seq), (bag) and (abs) of the type system of Figure 3. It remains to treat rule (hv), i.e. to study the kind Base when the function subterm is a variable occurrence.
13:10 Strategies as Resource Terms, and Their Categorical Semantics

<figure><img src="image_16.png" /><figcaption>Figure 13 Illustration of $\square_i(q)$.</figcaption></figure>

<figure><img src="image_17.png" /><figcaption>Figure 14 Four bijections.</figcaption></figure>

As above, we start with the corresponding construction on augmentations. We write $\vec{B} \Rightarrow \mathfrak{o} \stackrel{\text{def}}{=} B_1 \Rightarrow \dots \Rightarrow B_p \Rightarrow \mathfrak{o}$ for $\vec{B} = \langle B_1, \dots, B_n \rangle$ a tuple of objects, and $\vec{B}^\otimes \stackrel{\text{def}}{=} B_1 \otimes \dots \otimes B_n$. Consider $\Gamma = A_1 \otimes \dots \otimes A_n$ where each $A_i$ is $A_i = \vec{B}_i \Rightarrow \mathfrak{o} \cong \vec{B}_i^\otimes \Rightarrow \mathfrak{o}$; consider also $q \in \text{Aug}(\Gamma \vdash \vec{B}_i^\otimes)$. The **i-lifting of q**, written $\square_i(q) \in \text{Aug}_\bullet(\Gamma \vdash \mathfrak{o})$, is the augmentation that after the initial Opponent move, starts by playing the initial move in $A_i$, then proceeds as $q$. More precisely:

**Definition 10.** Consider $\Gamma = A_1 \otimes \dots \otimes A_n$, with

$$A_i = B_{i,1} \Rightarrow \dots \Rightarrow B_{i,p_i} \Rightarrow \mathfrak{o} \cong \vec{B}_i^\otimes \Rightarrow \mathfrak{o},$$

writing $\vec{B}_i^\otimes = B_{i,1} \otimes \dots \otimes B_{i,p_i}$; consider also $q \in \text{Aug}(\Gamma \vdash \vec{B}_i^\otimes)$. The **i-lifting of q**, written $\square_i(q) \in \text{Aug}_\bullet(\Gamma \vdash \mathfrak{o})$, has partial order $q$ prefixed with two additional moves, i.e. $\ominus \to \oplus \to q$. Its static causality is the least partial order containing dependencies

$$ \begin{array}{ll} m \leq_{\langle\square_i(q)\rangle} n & \text{for } m, n \in |q| \text{ with } m \leq_{\langle\square\rangle} n, \\ \oplus \leq_{\langle\square_i(q)\rangle} m & \text{for all } m \in |q| \text{ with } \partial_q(m) = (2, -), \end{array} $$

and with display map given by the following clauses:

$$ \begin{align*} \partial_{\square_i(q)}(\ominus) &= (2, q) \\ \partial_{\square_i(q)}(\oplus) &= (1, (i, (2, q))) \\ \partial_{\square_i(q)}(m) &= (1, a) & \text{if } \partial_q(m) = (1, a), \\ \partial_{\square_i(q)}(m) &= (1, (i, (1, a))) & \text{if } \partial_q(m) = (2, a), \end{align*} $$

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

We illustrate this in Figure 13. This construction again preserves isomorphisms, and extends to give, for any $q \in \text{Isog}(\Gamma \vdash \vec{B}_i^\otimes)$, its **i-lifting** $\square_i(q) \in \text{Isog}_\bullet(\Gamma \vdash \mathfrak{o})$. Additionally:

**Proposition 11.** Consider $\Gamma, A_1, \dots, A_n$ --arenas and assume $A_1, \dots, A_n$ are as above.

We have a bijection: $\square : \sum_{1 \leq i \leq n} \text{Isog}(\Gamma \vdash \vec{B}_i^\otimes) \cong \text{Isog}_\bullet(\Gamma \vdash \mathfrak{o})$.

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

**Theorem 12.** For $\Gamma$ a context and $F$ a type, there are bijections as in Figure 14.

## 3.3 Strategies and Composition

Next we extend this correspondence to the dynamics of resource terms, linking syntactic substitution with an adequate notion of composition of augmentations.

Consider $A, B$ and $C$ three --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*.
<figure><img src="image_18.png" /><figcaption>Figure 15 Construction of an interaction $p \otimes_{\phi} q$.</figcaption></figure>

<caption>Figure 16 $p \odot_{\phi} q$.</caption>

**Interaction of augmentations.** We can only compose $q$ and $p$ provided they reach the same state on $B$, so we first extract this via their desequentializations: observe $|(q)| \in C(A \vdash B)$ has form $x_A^q \vdash x_B^q$; likewise we write $|(p)| = x_B^p \vdash x_C^p \in C(B \vdash C)$. But what does it mean to “reach the same state”? In general $x_B^q = x_B^p$ is too much: it means $q$ and $p$ not only agree on a common state, but also on its irrelevant concrete representation. States in $B$ are not configurations, but *positions*: symmetry classes of configurations. Thus $q$ and $p$ are *compatible* if $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*:

**Proposition 13.** For $q, p$ as above and $\varphi : x_B^q \cong_B x_B^p$, setting $|p \otimes_{\varphi} q| = |q| + |p|$ with

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

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

$$ \vdash_{\varphi} = \{((1, m), (2, \varphi(m))) \mid m \in x_B^q \text{ & } \mathrm{pol}_{A \vdash B}(\partial_q(m)) = +\} $$

$$ \cup \{((2, \varphi(m)), (1, m)) \mid m \in x_B^q \text{ & } \mathrm{pol}_{B \vdash C}(\partial_p(m)) = +\}, $$

then $\vdash = \vdash_q \cup \vdash_p \cup \vdash_{\varphi}$ is acyclic: its transitive closure is a strict partial order on $|p \otimes_{\varphi} q|$.

We write $\leq_{p \otimes_{\varphi} q}^{\mathrm{def}} = \vdash^*$ for the reflexive and transitive closure of $\vdash$. The acyclicity of $\vdash$ corresponds to a subtle and fundamental property of innocent strategies: they always have a deadlock-free interaction. Our proof is a direct adaptation of a similar fact in concurrent games on event structures [10]. Figure 15 illustrates the construction of an interaction. The two augmentations $q \in \mathrm{Aug}(o \otimes o \vdash o)$ – on the left hand side – and $p \in \mathrm{Aug}(o \vdash (o \to o \to o) \to o)$ – on the right hand side – are shown with their common interface in red, with a symmetry $\varphi : qq \cong_o qq$ bridging them.

**Composing augmentations.** We compose $q$ and $p$ via $\varphi$, by hiding the interaction.

**Proposition 14.** Write $|(q)| = x_A^q \vdash x_B^q$, $|(p)| = x_B^p \vdash x_C^p$, and $\varphi : x_B^q \cong_B x_B^p$.

Then, the structure $p \odot_{\varphi} q$ obtained by restricting $p \otimes_{\varphi} q$ to events in $x_A^q + x_C^p$, with $\partial_{p \odot_{\varphi} q}((1, m)) = \partial_q(m)$ and $\partial_{p \odot_{\varphi} q}((2, m)) = \partial_p(m)$, is an augmentation on $A \vdash C$.

The interaction in Figure 15 yields the augmentation in Figure 16, the composition of $q$ and $p$ via $\varphi$. This extends to isogentations: $p \odot_{\varphi} q \stackrel{\mathrm{def}}{=} \overline{p \odot_{\varphi} q}$ for $q \in \mathrm{Isog}(A \vdash B)$ with $|(q)| = x_A^q \vdash x_B^q, p \in \mathrm{Isog}(B \vdash C)$ with $|(p)| = x_B^p \vdash x_C^p$, and $\varphi : x_B^q \cong_B x_B^p$.

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 there are exactly two symmetries $qq \cong_o qq$. Worse, the result of composition depends on the choice of $\varphi$: if Figure 15 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 16 with the two final causal links crossed, different even up to iso.
13:12 Strategies as Resource Terms, and Their Categorical Semantics

This reminds of the syntactic substitution $(\lambda f. f x x)([y, z]/x) \to \lambda f. f y z + \lambda f. f z y$. As syntactic substitution of resource terms yields sums of resource terms, this suggests that composition of isoglementations should produce sums of isoglementations, called strategies.

**Strategies.** Roughly speaking, a strategy is simply a weighted sum of isoglementations.

**► Definition 15.** A strategy on arena A is a function $\sigma : \text{lsog}(A) \to \overline{\mathbb{R}}_+$, where $\overline{\mathbb{R}}_+$ is the completed half-line of non-negative reals. We then write $\sigma : A$.

We regard $\sigma : A$ as a weighted sum $\sigma = \sum_{\mathbf{q} \in \text{lsog}(A)} \sigma(\mathbf{q}) \cdot \mathbf{q}$. We lift the composition of isoglementations to strategies via the formula

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

for $\sigma : A \vdash B$ and $\tau : B \vdash C$, i.e. $(\tau \odot \sigma)(\mathbf{r})$ is the sum of $\sigma(\mathbf{q})\tau(\mathbf{p})$ over all triples $\mathbf{q}, \mathbf{p}, \varphi$ s.t. $\mathbf{r} = \mathbf{p} \odot_{\varphi} \mathbf{q}$ – there are no convergence issues, as we have been careful to include $+\infty$ as a coefficient in Definition 15 (though this shall not arise in the interpretation).

**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 --arena A. The augmentation $\alpha_x \in \text{Aug}(A \vdash A)$, called the copycat augmentation on $x$, has $\langle\alpha_x\rangle = x \vdash x$, and as causal order $x \vdash x$, augmented with

$$ (1, m) \leq_{\alpha_x} (2, n) \quad \text{if } m \leq_x n \text{ and } \text{pol}_A(\partial_x(m)) = +, $$

$$ (2, m) \leq_{\alpha_x} (1, n) \quad \text{if } m \leq_x n \text{ and } \text{pol}_A(\partial_x(m)) = -, $$

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{lsog}(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? To cancel the sum over all symmetries in (1), we set:

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

where $\text{Sym}(x)$ is the group of *endosymmetries* of $x$, i.e. of all $\varphi : \underline{x} \cong_A \underline{x}$ – the cardinal 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 [15].

3.4 Proof of the Categorical Laws

In this section, we show the main arguments behind the following result:

**► Theorem 16.** The --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 17 (Neutrality).** Consider $q \in \mathrm{Aug}(A \vdash B)$, $x \in \mathcal{C}(B)$ and $\varphi : x_B^q \cong_B x$. Then, $\mathcal{C}_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} \mathcal{C}_y \cong q$.

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

$$|\mathcal{C}_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 $\mathcal{C}_x \odot_{\varphi} q$. ◀

It may be surprising that $\mathcal{C}_x \odot_{\varphi} q \cong q$ regardless of $\varphi$: the choice of the symmetry is reflected in the isomorphism $\mathcal{C}_x \odot_{\varphi} q \cong q$, which this lemma ignores. Similarly, we have:

**Lemma 18 (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

$$\mathbf{r} \odot_{\psi'} (\mathbf{p} \odot_{\varphi} \mathbf{q}) \cong (\mathbf{r} \odot_{\psi} \mathbf{p}) \odot_{\varphi'} \mathbf{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 $\mathbf{r} \odot_{\psi}^3 \mathbf{p} \odot_{\varphi}^3 \mathbf{q}$: $\mathrm{Aug}(A \vdash D)$, defined in a way similar to binary composition. ◀

**Congruence.** 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 : (|q|) \cong_{A \vdash B} (|q'|)$ – a symmetry – therefore it has the form $\varphi_A \vdash \varphi_B$, with $\varphi_A : x_A^q \cong_A x_A^{q'}$ and $\varphi_B : x_B^q \cong_B x_B^{q'}$.

**Lemma 19.** Consider $q, q' \in \mathrm{Aug}(A \vdash B)$, $p, p' \in \mathrm{Aug}(B \vdash C)$, isomorphisms $\theta : x_B^q \cong_B x_B^p$ and $\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 19. 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 reindexing the sum following $\chi$ – or in other words, the composition of strategies does not depend on the choice of representative used for isogmentation. This is often used silently throughout the development.
13:14 Strategies as Resource Terms, and Their Categorical Semantics

<figure><img src="image_19.png" /><figcaption>Figure 17 Monoid laws.</figcaption></figure>

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

**Proposition 20.** 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 $\mathbf{p} \in \mathrm{lsog}(B \vdash B)$, we write $\langle\mathbf{p}\rangle = x_1^\mathbf{p} \vdash x_r^\mathbf{p}$. We have:

$$ 
\begin{align*}
\mathrm{id}_B \odot \sigma &= \sum_{\mathbf{q} \in \mathrm{lsog}(A \vdash B)} \sum_{\mathbf{p} \in \mathrm{lsog}(B \vdash B)} \sum_{\varphi: x_B^{\mathbf{q}} \cong_B x_1^{\mathbf{p}}} \sigma(\mathbf{q}) \mathrm{id}_B(\mathbf{p}) \cdot \mathbf{p} \odot_{\varphi} \mathbf{q} \\
&= \sum_{\mathbf{q} \in \mathrm{lsog}(A \vdash B)} \sum_{\mathbf{x} \in \mathcal{P}(B)} \sum_{\varphi: x_B^{\mathbf{q}} \cong_B x_\mathbf{x}} \frac{\sigma(\mathbf{q})}{\#\mathrm{Sym}(\mathbf{x})} \cdot \mathcal{O}_\mathbf{x} \odot_{\varphi} \mathbf{q}
\end{align*}
$$

using definition of the composition and of the identity. Next, we compute

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

which is $\sigma$; by Lemma 17 and direct reasoning on symmetries $-\sigma \odot \mathrm{id}_A = \sigma$ is symmetric. ◀

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

# 4 Resource Categories

We now develop resource categories, models of the resource calculus inspired by Strat.

## 4.1 Motivation and Definition

As compositions generate sums, we need an additive structure. Following [5], an **additive symmetric monoidal category (asmc)** is a symmetric monoidal category where each hom-set is a commutative monoid, and each operation preserves the additive structure.

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

**Definition 21.** Consider $C$ an additive symmetric monoidal category.

A **bialgebra** on $C$ is $(A, \delta_A, \epsilon_A, \mu_A, \eta_A)$ with $(A, \mu_A, \eta_A)$ a commutative monoid (see Figure 17), $(A, \delta_A, \epsilon_A)$ a commutative comonoid, with additional bialgebra laws (Figure 18).
<figure><img src="image_20.png" /><figcaption>Figure 18 Additional bialgebra laws.</figcaption></figure>

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

In a resource category, all objects shall be bialgebras. This means that for each object $A$, we have morphisms $\delta_A : A \to A \otimes A$, $\epsilon_A : A \to I$, $\mu_A : A \otimes A \to A$, and $\eta_A : I \to A$ satisfying coherence laws [5]. 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 the left. 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 the left, reflecting the sums arising in substitutions.

In contrast with differential categories, morphisms in a resource category intuitively correspond to (sums of) *bags* rather than *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), *)$ a commutative monoid, altogether turning $C(A, B)$ into a commutative semiring, though 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. More formally:

► **Definition 22.** Consider $C$ an asmc where each object has a bialgebra structure.

For $A \in 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 19, plus $\epsilon_A \circ \text{id}_A^\bullet = 0$ and $\text{id}_A^\bullet \circ \eta_A = 0$.

Those laws are reminiscent of the laws of derelictions and coderelictions in bialgebra modalities [5], except that both roles are played by $\text{id}_A^\bullet$. In a resource category $C$, all objects have a pointed identity. The “singleton bags” are those $f \in C(A, B)$ that are **pointed**, i.e. $\text{id}_B^\bullet \circ f = f$ – we write $C_\bullet(\Lambda, B)$. Dually, we may also capture those morphisms which require exactly one resource: $f \in C(A, B)$ is **co-pointed** if $f \circ \text{id}_A^\bullet = f$, and we write $f \in C^\bullet(\Lambda, B)$.

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

► **Definition 23.** A resource category is an asmc $C$ where each $A \in C$ has a bialgebra structure $(A, \delta_A, \epsilon_A, \mu_A, \eta_A)$ and pointed identity $\text{id}_A^\bullet$, such that the bialgebra structure is compatible with the monoidal structure of $C$ (see Figure 20).
13:16 Strategies as Resource Terms, and Their Categorical Semantics

<figure><img src="image_22.png" /><figcaption>Figure 20 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_23.png" /><figcaption>Figure 21 Compatibility of bags with $\delta$.</figcaption></figure>

<figure><img src="image_24.png" /><figcaption>Figure 22 Compatibility of bags with $\mu$.</figcaption></figure>

Additionally, $\mathcal{C}$ is closed if $A \otimes -$ has a right adjoint $A \to -$ for each $A \in \mathcal{C}$.

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 proof of invariance relies on it:

**Lemma 24.** 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 diagram of Figure 21 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 diagram of Figure 22 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. ◀

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

## 4.2 Interpretation of the Resource Calculus

In order to describe the interpretation of the resource calculus, it will be convenient to introduce some of the combinators from the theory of cartesian closed 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{\text{def}}{=} (f \otimes g) \circ \delta_{\Gamma} \in \mathcal{C}(\Gamma, A \otimes B); $$

likewise $\pi_1 \stackrel{\text{def}}{=} \rho_A \circ (A \otimes \epsilon_B) \in \mathcal{C}(A \otimes B, A)$ and $\pi_2 \stackrel{\text{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: we have $\langle \pi_1, \pi_2 \rangle = \text{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** [20].
For any two objects $A, B \in \mathcal{C}$, we have $\mathrm{ev}_{A,B} \in \mathcal{C}((A \to B) \otimes A, B)$ the **evaluation morphism**. If $f \in \mathcal{C}(A \otimes B, C)$, its **currying** is written $\Lambda_{A,B,C}(f) \in \mathcal{C}(A, B \to C)$.

**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 25.** Let $\bar{b} \in \mathcal{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 \in \mathcal{C}(\Delta, \Gamma)$ is a comonoid morphism, then we have:

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

**Proof.** A diagram chase leveraging case (1) of Lemma 24. ▼

This is fairly close to how substitutions propagate through terms in the resource $\lambda$-calculus (see Section 2): 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 26.** Consider $\bar{f} \in \mathcal{B}(\mathcal{C}_{\bullet}(A, B))$. Then $\mathrm{id}_{\mathcal{B}}^{\bullet} \circ \Pi \bar{f} = v$ if $\bar{f} = [v]$, 0 otherwise.

This lemma follows from the conditions of a resource category, though in a not so straightforward way. 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.

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

We first set $[o]^{\mathrm{def}} = o$, $[[\langle F_1, \dots, F_n \rangle]^{\mathrm{def}} = [[F_1]] \otimes \dots \otimes [F_n]]$ and $[[\vec{F} \to o]^{\mathrm{def}} = [[\vec{F}]] \to o$. For contexts, $[[\Gamma]]^{\mathrm{def}} = \otimes_{(x:F) \in \Gamma} [[F]]$. If $(x:F) \in \Gamma$, we write $\mathrm{var}_{x}^{\Gamma} \in \mathcal{C}([\Gamma], [F])$ the projection. For $\Gamma$ and $\Delta$ disjoint we use the iso $\mathbb{M}_{\Gamma, \Delta} \in \mathcal{C}([\Gamma] \otimes [\Delta], [\Gamma, \Delta])$.

The interpretation of terms (or, rather, of typing derivations) follows the four kinds of judgements from Section 2: for $\Gamma, A \in \mathcal{C}$ and $\vec{A} = \langle A_1, \dots, A_n \rangle$, we define

$$ \begin{array}{lclcl} \mathrm{Val}_{\mathcal{C}}(\Gamma; A) & \stackrel{\mathrm{def}}{=} & \mathcal{C}_{\bullet}(\Gamma, A) & \quad & \mathrm{Seq}_{\mathcal{C}}(\Gamma; \vec{A}) & \stackrel{\mathrm{def}}{=} \Pi_{1 \le i \le n} \mathrm{Bag}_{\mathcal{C}}(\Gamma; A_i) \\ \mathrm{Base}_{\mathcal{C}}(\Gamma) & \stackrel{\mathrm{def}}{=} & \mathcal{C}_{\bullet}(\Gamma, o) & \quad & \mathrm{Bag}_{\mathcal{C}}(\Gamma; A) & \stackrel{\mathrm{def}}{=} \mathcal{B}(\mathrm{Val}_{\mathcal{C}}(\Gamma; A)). \end{array} $$

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. via the monoidal structure) in $\mathcal{C}$. This apparent duplication of structure is resolved when interpreting applications: we set $\langle \vec{f} \rangle^{\mathrm{def}} = \langle \Pi \vec{f}_1, \dots, \Pi \vec{f}_n \rangle \in \mathcal{C}(\Gamma, \vec{A}^{\otimes})$ for $\vec{f} = \langle \vec{f}_1, \dots, \vec{f}_n \rangle \in \mathrm{Seq}_{\mathcal{C}}(\Gamma, \vec{A})$, called the **packing** of the sequence $\vec{f}$.

Like bags, packed sequences distribute over pairs and products:

**Lemma 27.** Let $\vec{c} \in \mathrm{Seq}_{\mathcal{C}}(\Delta; \vec{A})$, $h \in \mathcal{C}(\Delta, \Gamma)$, $f \in \mathcal{C}(\Gamma \otimes \vec{A}, B)$, $g \in \mathcal{C}(\Gamma \otimes \vec{A}, C)$. If $h \in \mathcal{C}(\Delta, \Gamma)$ is a comonoid morphism, then we have:

$$ \langle f, g \rangle \circ \langle h, \langle \vec{c} \rangle \rangle = \sum_{\vec{c} \prec \langle \vec{c}_1 \rangle * \vec{c}_2} \langle f \circ \langle h, \langle \vec{c}_1 \rangle \rangle, g \circ \langle h, \langle \vec{c}_2 \rangle \rangle \rangle. $$
13:18 Strategies as Resource Terms, and Their Categorical Semantics

$$ [[\Gamma \vdash_{\text{Val}} \lambda \vec{x}. s : \vec{F} \to o]] = \Lambda_{[[\Gamma], [\vec{x}:\vec{F}]]_o}([[(\Gamma, \vec{x} : \vec{F}) \vdash_{\text{Base}} s : o]] \circ \mathcal{M}_{[[\Gamma], [\vec{x}:\vec{F}]})) $$

$$ [[\Gamma \vdash_{\text{Base}} x \vec{t} : o]] = \text{ev}_{[[\vec{F}]]_o} \circ \langle \text{id}_{\text{id}_{\vec{F}}} \circ \text{var}_{\vec{x}} \circ \langle [[\Gamma \vdash_{\text{Seq}} \vec{t} : \vec{F}] \rangle] \rangle $$

$$ [[\Gamma \vdash_{\text{Base}} s \vec{t} : o]] = \text{ev}_{[[\vec{F}]]_o} \circ \langle [[\Gamma \vdash_{\text{Val}} s : \vec{F} \to o]] \circ \langle [[\Gamma \vdash_{\text{Seq}} \vec{t} : \vec{F}] \rangle] \rangle $$

$$ [[\Gamma \vdash_{\text{Bag}} [s_1, \dots, s_n] : F]] = [[[\Gamma \vdash_{\text{Val}} s_i : F]] | 1 \le i \le n] $$

$$ [[\Gamma \vdash_{\text{Seq}} \langle \bar{s}_1, \dots, \bar{s}_n \rangle : \vec{F}]] = \langle [[\Gamma \vdash_{\text{Bag}} \bar{s}_i : F_i]] | 1 \le i \le n \rangle $$

Figure 23 Interpretation of the resource calculus.

**Proof.** Proved by iterating Lemma 25, for each component of the sequence.

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

We also have a similar lemma for a substitution propagating through a product:

**Lemma 28.** Consider $f,g \in C(\Gamma \otimes A, B)$, $h \in C(\Delta, \Gamma)$ a comonoid morphism, and $\vec{c} \in \text{Seq}_C(\Delta, \vec{A})$. Then,

$$ (f * g) \circ \langle h, \langle \vec{c} \rangle \rangle = \sum_{\vec{c} \prec \vec{c}_1 * \vec{c}_2} (f \circ \langle h, \langle \vec{c}_1 \rangle \rangle) * (g \circ \langle h, \langle \vec{c}_2 \rangle \rangle), $$

and $1 \circ \langle h, \langle \vec{c} \rangle \rangle = 1$ if $\vec{c}$ is empty, 0 otherwise.

**Proof.** Similar to Lemma 27.

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

We now define the four interpretation functions

$\text{Val}(\Gamma; F) \to \text{Val}_C([\Gamma]; [F])$

$\text{Bag}(\Gamma; F) \to \text{Bag}_C([\Gamma]; [F])$

$\text{Base}(\Gamma) \to \text{Base}_C([\Gamma])$

$\text{Seq}(\Gamma; \vec{F}) \to \text{Seq}_C([\Gamma]; [\vec{F}])$

all written $[[\cdot]]$, by mutual induction, as in Figure 23. The interpretation is extended to sums of terms $\Sigma\text{Val}(\Gamma; F) \to \text{Val}_C([\Gamma]; [F])$ and $\Sigma\text{Base}(\Gamma) \to \text{Base}_C([\Gamma])$ relying on the additive structure of $C$ – we give no interpretation to sums of bags or sequences.

4.3 The Soundness Theorem

We show that this interpretation is invariant under reduction. 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:

$$ -\langle -/\vec{x} \rangle : \text{Val}_C([\Gamma, \vec{x} : \vec{F}]; [G]) \times \text{Seq}_C([\Gamma]; [\vec{F}]) \to \text{Val}_C([\Gamma]; [G]) $$

$$ -\langle -/\vec{x} \rangle : \text{Base}_C([\Gamma, \vec{x} : \vec{F}]) \times \text{Seq}_C([\Gamma]; [\vec{F}]) \to \text{Base}_C([\Gamma]) $$

$$ -\langle -/\vec{x} \rangle : \text{Seq}_C([\Gamma, \vec{x} : \vec{F}]; [\vec{G}]) \times \text{Seq}_C([\Gamma]; [\vec{F}]) \to \mathcal{C}([\Gamma], [\vec{G}]) $$

using our cartesian-like notations:

$$ f \langle \vec{g} / \vec{x} \rangle \stackrel{\text{def}}{=} f \circ \mathcal{M}_{[[\Gamma], [\vec{x}:\vec{F}]} \circ \langle \text{id}_{[[\Gamma]]}, \langle \vec{g} \rangle \rangle $$

$$ \vec{f} \langle \vec{g} / \vec{x} \rangle \stackrel{\text{def}}{=} \langle \vec{f} \rangle \circ \mathcal{M}_{[[\Gamma], [\vec{x}:\vec{F}]} \circ \langle \text{id}_{[[\Gamma]]}, \langle \vec{g} \rangle \rangle $$

where the first applies for $f \in \text{Val}_C([\Gamma, \vec{x} : \vec{F}]; [G])$ or $f \in \text{Base}_C([\Gamma, \vec{x} : \vec{F}])$ and the second for $\vec{f} \in \text{Seq}_C([\Gamma, \vec{x} : \vec{F}]; [\vec{G}])$. We may now state the substitution lemma:

**Lemma 29.** Consider $\vec{t} \in \text{Seq}(\Gamma, \vec{F})$, $\Delta = \Gamma, \vec{x} : \vec{F}$ and $s \in \text{Val}(\Delta, G)$ or $s \in \text{Base}(\Delta)$. Then, $\langle s \langle \vec{t} / \vec{x} \rangle \rangle = \langle s \rangle \langle \langle \vec{t} \rangle / \vec{x} \rangle \rangle$.
**Proof.** We show the stronger statement that for all $\vec{g} \in \text{Seq}(\Gamma, \vec{F})$, and $\Delta = \Gamma, \vec{x} : \vec{F}$,

(1) If $f \in \text{Val}(\Delta; G)$, then $\llbracket f \langle \vec{g} / \vec{x} \rangle \rrbracket = \llbracket f \rrbracket \langle \llbracket \vec{g} \rrbracket / \vec{x} \rangle$.

(2) If $f \in \text{Base}(\Delta)$, then $\llbracket f \langle \vec{g} / \vec{x} \rangle \rrbracket = \llbracket f \rrbracket \langle \llbracket \vec{g} \rrbracket / \vec{x} \rangle$.

(3) Assume $\vec{f} \in \text{Seq}(\Delta; \vec{G})$ with $\vec{f} \langle \vec{g} / \vec{x} \rangle = \sum_{1 \le i \le n} \vec{f}_i$, for $\vec{f}_i \in \text{Seq}(\Gamma; \vec{G})$.

Then, $\sum_{1 \le i \le n} \llbracket \vec{f}_i \rrbracket = \llbracket \vec{f} \rrbracket \langle \llbracket \vec{g} \rrbracket / \vec{x} \rangle$;

which follows by induction on typing derivations, using all our lemmas above.

From the substitution lemma above, we may easily deduce:

**Theorem 30.** If $S \in \Sigma \text{Val}(\Gamma; F)$ and $S \Rightarrow S'$ then $\llbracket S \rrbracket = \llbracket S' \rrbracket$.

**Proof.** Preservation of $\beta$-reduction follows from Lemma 29. To show that this extends by context closure, we prove the three statements:

(1) If $s \in \text{Val}(\Gamma; F)$ and $s \Rightarrow S'$ then $\llbracket s \rrbracket = \llbracket S' \rrbracket$,

(2) If $s \in \text{Base}(\Gamma)$ and $s \Rightarrow S'$ then $\llbracket s \rrbracket = \llbracket S' \rrbracket$,

(3) If $\vec{s} \in \text{Seq}(\Gamma; \vec{F})$ and $\vec{s} \Rightarrow \sum_{i \in I} \vec{s}_i$ then $\llbracket \vec{s} \rrbracket = \sum_{i \in I} \llbracket \vec{s}_i \rrbracket$.

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

# 5 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 12.

## 5.1 Additive Symmetric Monoidal Structure

**Tensor.** As for composition we first define the tensor of augmentations, then isoglementations, 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 $\text{id}_A$ in (2) (page 12) and likewise for $\rho_A, \alpha_{A,B,C}$ and $\gamma_{A,B}$. These structural morphisms satisfy the necessary conditions to make $(\text{Strat}, \otimes, 1)$ a symmetric monoidal category.
**Additive Structure.** The sum of strategies is defined pointwise, and 0 is the sum with coefficients all null. All compatibility conditions are direct, making Strat an asmc.

## 5.2 Resource Category Structure

**Bialgebra.** For the strategies for (co)multiplication, we first set configurations $(\llbracket \delta_A^{x,y} \rrbracket) = 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)$, and to strategies by summing over those with coefficients cancelling out symmetries on $x$ and $y$. The unit $\epsilon_A$ and co-unit $\eta_A$ are both strategies with only the empty isoglementation in their support, with coefficient 1. We have:

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

Additionally, it is direct that this is compatible with the monoidal structure.

**Pointed Identity.** The pointed identity $\text{id}_A^\bullet$ is defined by (2), restricted to pointed positions – the laws of Figure 19 follow. The categorical notion of pointedness from Section 4.1 agrees with the concrete one in Section 3.1: $\sigma$ is pointed iff all the isoglementations in its support are.

**Closed structure.** We use the currying bijection $\Lambda_{\Gamma,A,B}$ from Section 3. For $\sigma : \Gamma \otimes A \vdash B$, we set $\Lambda_{\Gamma,A,B}(\sigma) = \sum_{\mathbf{q} \in \text{lsog}(\Gamma \otimes A \vdash B)} \sigma(\mathbf{q}) \cdot \Lambda_{\Gamma,A,B}(\mathbf{q})$, which directly yields

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

from which evaluation is $\text{ev}_{A,B} = \Lambda_{A \Rightarrow B,A,B}^{-1}(\text{id}_{A \Rightarrow B})$. Altogether:

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

**Compatibility with normal forms.** Finally, we show compatibility with normal forms – the crux is that the *i*-lifting in Figure 13 matches the first *Base* clause in Figure 23, when $x$ is the *i*-th variable of $\Gamma$:

* **Proposition 33.** *Consider $s \in \text{Val}(\Gamma; F)$ or $s \in \text{Base}(\Gamma)$ a normal form. Then, $\llbracket s \rrbracket$ is the sum having $\|s\|$ with coefficient 1, and 0 everywhere else.*

* **Corollary 34.** If $s \in \text{Val}(\Gamma; F)$ with normal form $s \Rightarrow^* \sum_{i \in I} s_i$, then $\llbracket s \rrbracket = \sum_{i \in I} \|s_i\|$.

# 6 Concluding remarks

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

Firstly, $x : F \to G$ is not a valid term as it is not $\eta$-long: it hides some infinitary copycat behaviour that must be written explicitly in our typed resource calculus, requiring an infinite sum as in (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 of [9]. 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 $\eta$-long syntax puts the pure $\lambda$-calculus out of reach. It is in fact possible to enforce $\eta$-expandedness 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. This corresponds to finding the analogue of a reflexive object in the category of games. In [23], Tsukada and Ong suggest the resource calculus with tests [8] as a candidate, but this does not seem fit for the task: it does not allow to represent arbitrary infinite sequences of abstractions; and 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 however possible to design a suitable language, enjoying the same relationship with Nakajima trees [21] (see also [3, Exercise 19.4.4]) as that of the ordinary resource calculus with Böhm trees. We leave the exposition of this for future work.

References

1 Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for PCF. *CoRR*, abs/1311.6125, 2013.

2 Davide Barbarossa and Giulio Manzonetto. Taylor subsumes Scott, Berry, Kahn and Plotkin. *Proc. ACM Program. Lang.*, 4(POPL):1:1-1:23, 2020.

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

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

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

6 Richard F Blute, J Robin B Cockett, and Robert AG Seely. Cartesian differential categories. *Theory and Applications of Categories*, 22(23):622-672, 2009.

7 Pierre Boudes. Thick subtrees, games and experiments. In *TLCA*, volume 5608 of *Lecture Notes in Computer Science*, pages 65-79. Springer, 2009.

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

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

10 Simon Castellan and Pierre Clairambault. Disentangling parallelism and interference in game semantics. *CoRR*, abs/2103.15453, 2021.

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

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

13 Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. *Theor. Comput. Sci.*, 309(1-3):1-41, 2003.

14 Thomas Ehrhard and Laurent Regnier. Differential interaction nets. *Theor. Comput. Sci.*, 364(2):166-195, 2006.

15 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.
16 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.

17 Jim Laird. A game semantics of the asynchronous π-calculus. In *CONCUR*, volume 3653 of *Lecture Notes in Computer Science*, pages 51–65. Springer, 2005.

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

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

20 Paul-André Mellies. Categorical semantics of linear logic. *Panoramas et syntheses*, 27:15–215, 2009.

21 Reiji Nakajima. Infinite normal forms for the λ-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.

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

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