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

HAL
open science

# The Geometry of Causality

Simon Castellan, Pierre Clairambault

► To cite this version:

Simon Castellan, Pierre Clairambault. The Geometry of Causality: Multi-Token Geometry of Interaction and its Causal Unfolding. Proceedings of the ACM on Programming Languages, In press, pp.1-70. hal-03286443v2

HAL Id: hal-03286443

https://hal.science/hal-03286443v2

Submitted on 14 Nov 2022

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>

Distributed under a Creative Commons Attribution 4.0 International License
# The Geometry of Causality

Multi-Token Geometry of Interaction and its Causal Unfolding

SIMON CASTELLAN, Univ Rennes, Inria, CNRS, IRISA, France

PIERRE CLAIRAMBAULT, Aix Marseille Univ, Université de Toulon, CNRS, LIS, Marseille, France

We introduce a multi-token machine for *Idealized Parallel Algol* (IPA), a higher-order concurrent programming language with shared state and semaphores. Our machine takes the shape of a compositional interpretation of terms as *Petri structures*, certain coloured Petri nets. For the purely functional fragment of IPA, our machine is conceptually close to *Geometry of Interaction* token machines, originating from Linear Logic and presenting higher-order computation as the low-level process of a token walking through a graph (a proof net) representing the term. We combine here these ideas with folklore ideas on the representation of first-order imperative concurrent programs as coloured Petri nets.

To prove our machine computationally adequate with respect to the reference operational semantics, we follow game semantics and represent types as certain games specifying dependencies and conflict between computational events. *Petri strategies* are those Petri structures obeying the rules of the game extracted from the type. We show how Petri strategies *unfold* to concurrent strategies in the sense of concurrent games on event structures. This link with concurrent strategies not only allows us to prove adequacy of our machine, but also lets us generate operationally a causal description of the behaviour of programs at higher-order types, which is shown to coincide with that given denotationally by the interpretation in concurrent games.

Additional Key Words and Phrases: Geometry of Interaction, Game Semantics, Shared Memory Concurrency, Coloured Petri Nets, Higher-Order

# 1 INTRODUCTION

## 1.1 The Operational, the Denotational and the Game Semantics

Semantics of programming languages are often classified into two broad families. On the one hand, *operational semantics* formalize execution via concrete, local rules that often operate directly on syntax: this includes methods based on rewriting, labelled transition systems or abstract machines. Mathematically those are usually relatively simple inductive structures making them easy to implement and reason about. However they often focus on *closed* programs, and most formalisms struggle with compositionality. On the other hand, *denotational semantics* embed types and programs in an adequate mathematical space (domains and continuous functions, sets and relations, games and strategies, etc). Compositionality holds by definition, as the denotation is computed by induction on syntax, sending each syntactic construction to a corresponding semantic operation – this makes denotational semantics a great tool for modular reasoning on programs and to inform programming language design. However, the link with the source code is often quite remote: identifying the piece of syntax and the runtime environment responsible for a denotationally observed behaviour can be subtle, in particular because interpretation can involve complex constructions (such as composition of strategies). Denotational semantics abound with *adequacy* results relating evaluation in the sense of operational and denotational semantics, but those typically concern closed programs of

Authors' addresses: Simon Castellan, Univ Rennes, Inria, CNRS, IRISA, Rennes, France, simon.castellan@inria.fr; Pierre Clairambault, Aix Marseille Univ, Université de Toulon, CNRS, LIS, Marseille, France, pierre.clairambault@cnrs.fr.

Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the owner/author(s).

© 2023 Copyright held by the owner/author(s).

2475-1421/2023/1-ART24

https://doi.org/10.1145/3571217
ground type, and are not very informative for open programs. In this paper we ask ourselves: how transparent can we make the link between operational and denotational semantics, for *open* programs of *arbitrary type*? Such a link, if established convincingly, could play a valuable role in the mathematical theory of programming semantics.

To approach this question, we allow ourselves some flexibility on what we exactly mean by “operational semantics”: we do not necessarily refer here to the familiar range of syntactic techniques, but more broadly to, let us say, a formalization of execution specified by concrete, local rules acting on an intermediate representation of programs obtained from the source code in a modular way, with low complexity (say, linear). The goal is that one should then be able to easily extract denotational information from execution traces in this operational semantics. Because denotational semantics predict program evaluation in any context, this implies that our executions cannot stop at computing the result of closed programs of ground types; they must, for open programs of arbitrary type, produce (lazily) a structure that is fully informative of their dynamic behaviour in any context, in a way that is both operationally meaningful and close to denotational semantics. The field that studies such interactive representations of programs is called *game semantics* [Abramsky et al. 2000; Hyland and Ong 2000]: it presents the interactive behaviour of programs as a *strategy* in a two-player game that the program plays with its execution environment. More specifically, we target *concurrent games* [Castellan and Clairambault 2020; Castellan et al. 2017]: based on *event structures*, those offer a representation of the interactive behaviour of programs that is causal and with full non-deterministic branching information. Thanks to this intensional expressivity, they are related by forgetful projections to a growing number of models in the denotational semantics landscape – this includes various other game models [Castellan and Clairambault 2020], relational or weighted relational models [Castellan et al. 2018; Clairambault and de Visme 2020], and the Scott model through Ehrhard’s extensional collapse theorem [Ehrhard 2012].

*Operational game semantics.* Connecting operational and game semantics is far from a new idea. Though it was clear from early work on game semantics [Danos et al. 1996] that interaction between strategies was related to execution by abstract machines, the idea to generate strategies by operational means was – to our knowledge – first suggested by Laird in his trace semantics for higher-order references [Laird 2007] (with the explicit connection with game semantics later worked out by Jaber [Jaber 2015]). In the 2010s, several works were proposed blurring the lines between operational and game semantics [Ghica and Tzevelekos 2012; Levy and Staton 2014], typically via LTSs dealing with open programs by sending and receiving messages from the environment (interestingly, similar structures appear in work on compositional certified compilers [Stewart et al. 2015]); for these systems, compositionality is a theorem rather than a definition. But these developments do not yield strategies in the sense of previously established models. Furthermore they only deal with sequential deterministic programs, and it seems hard to extend LTS-based techniques to give a causal account of the execution of higher-order concurrent programs.

But in fact, a powerful connection between operational and denotational semantics was already established significantly before the above, although not then presented as such: it is Baillot’s result [Baillot 1999] that Girard’s *Geometry of Interaction* for IMELL generates the strategy obtained as its interpretation in so-called Abramsky-Jagadeesan-Malacaria (AJM) games [Abramsky et al. 2000]. As this result is one of our main inspirations, we take some time to introduce its main intuitions.

## 1.2 The Gol Token Machine and AJM Games

Girard’s *Geometry of Interaction (Gol)* was first introduced as a model construction for System F [Girard 1989]; but it was soon realized, following work by Danos, Herbelin and Regnier [Danos et al. 1996; Danos and Regnier 1996] and Mackie [Mackie 1995] that it informed an abstract machine
<figure><img src="image_3.png" /><figcaption>Fig. 1. The λ-graph representation of a term</figcaption></figure>

<figure><img src="image_4.png" /><figcaption>Fig. 2. A token on a wire</figcaption></figure>

that could be used to evaluate programs, with links with Lamping’s optimal reduction [Gonthier et al. 1992]. We introduce this informally, on a simply-typed linear λ-calculus with one atom α.

In order to execute the GoI token machine on a term $\vdash M : A$, one usually first translates it into a *proof net* in the sense of linear logic – or alternatively, to avoid relying too much on familiarity with linear logic, into a simple *λ-graph*: for instance, the linear λ-term

$$ \vdash (\lambda f^{\alpha \to \alpha} . \lambda x^{\alpha} . f x) (\lambda y^{\alpha} . y) : \alpha \to \alpha \qquad (1) $$

may be represented by the graph shown in Figure 1. The reader should recognize in this directed graph the structure of the term: there is one node for each application, and one node for each abstraction. An application node receives two inputs (the function and its argument, drawn on top) and emits one output (the result, drawn at the bottom). An abstraction node receives one input (the “body” of the function, drawn on top) and emits two outputs: a wire for the bound variable, drawn on the side, and a wire for the resulting function, drawn at the bottom. All wires are explicitly labelled with a type. Finally the dangling wires match the overall typing judgment; it is the interface with which the program will interact with its environment. One may define a rewriting theory for such representations (though then this is more elegantly done on linear logic proof nets).

The Geometry of Interaction token machine captures execution as a token walking through this graph, following local rules. At any point in time, the token sits on one of the wires – more precisely, on an occurrence of an atom in the type labelling the wire. The token also has a *direction*: it may follow the orientation of the wire, or go against it – we represent this as an arrow accompanying the atom, as in Figure 2. How is execution formalized? The GoI token machine is initialized by putting a token, going up, on the rightmost atom occurrence on the output dangling wire. This token is then pushed around the graph following simple local rules, of which we show a few:

<figure><img src="image_5.png" /></figure>
<figure><img src="image_6.png" /><figcaption>Fig. 3. An execution of the GoI token machine</figcaption></figure>

<figure><img src="image_7.png" /><figcaption>Fig. 4. Token transitions for contraction</figcaption></figure>

Here, we use $A, B$ to range over arbitrary types while $\alpha$ is reserved to occurrences of the atom. In the transitions shown above, tokens are shown accompanying a type $A$ or $B$, but it is meant that they sit on a *particular atom occurrence* within $A$ or $B$, as e.g. in Figure 2. Each transition moves the token to another copy of the *same* type, so it makes sense to require that it should sit on the *same* atom occurrence as before. The reader should be able to complete the missing rules: in each node, the “As” and the “Bs” are associated pairwise, and the rules simply follow this correspondence. Following these rules, the GoI token machine on our example $\lambda$-graph yields the execution depicted in Figure 3: a token thrown on the output atom $\alpha$ eventually makes its way back to the dangling wire, on the input atom $\alpha$. This input/output behaviour is the same as observed when running the GoI token machine on (the $\lambda$-graph for) $\lambda x. x : \alpha \to \alpha$, reflecting that the $\lambda$-term in (1) indeed evaluates to $\lambda x. x : \alpha \to \alpha$ – it is possible to *read back* the normal form from executions of the GoI.

Of course, the simplicity of this presentation of the GoI token machine exploits the linearity of the language at hand. The non-linear version heavily rests on Girard’s decomposition $A \to B = !A \to B$ of the call-by-name function type as a combination of the linear function type and the “bang” (!) modality, marking replicable resources. Proof nets for non-linear languages then involve explicit “contraction” nodes allowing us to link one abstracted variable to several variable occurrences:

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

This heavily impacts the token game: tokens must carry data identifying resource accesses, and helping route tokens around the net. These “exponential signatures” may be formalized as natural numbers or via a simple inductive definition $\mathcal{E} ::= t\mathcal{E} | r\mathcal{E} | \dots$ (with elements ranged over by $e$ and its variants). The token game exploits this, via rules including those in Figure 4. We omit the details, which we will not rely on in this paper, the full machine appears e.g. in [Baillot 1999].

Altogether, one “runs” a $\lambda$-term by: (1) translating it to a proof net; (2) initializing the machine by putting a token going up on a dangling wire, on a variable occurrence $m$ with exponential signature $e$ – hence the input is a pair $(m, e)$; (3) applying the rules as long as possible. The machine may in principle get stuck or loop forever, we say it *halts* if it emits a token carrying $e'$ going down on an atom occurrence $m'$, corresponding to a pair $(m', e')$. Such pairs, called *moves*, form a set written Moves. Then the GoI token machine on $\Gamma \vdash M : A$ initialized and executed as above yields

$f_M : \text{moves} \to \text{moves},$
a partial function. Now it turns out that this $f_M$ directly informs the strategy $[[M]]$ interpreting $M$ in AJM game semantics. More precisely, and as Baillot proved, the interpretation of types may be set up so that the moves of the game $[[\Gamma \vdash A]]$ indeed form a subset of Moves, and that we have:

**THEOREM 1.1 (BAILLOT, 1999).** Consider $\Gamma \vdash M : A$ any term.

Then, the strategy $[[M]] : [[\Gamma \vdash A]]$, obtained denotationally from $M$, comprises exactly the sequences

$$s = s_1 s_2 \dots s_{2n-1} s_{2n}$$

which are valid plays on $[[\Gamma \vdash A]]$ and such that for all $1 \le i \le n$, we have $s_{2i} = f_M(s_{2i-1})$.

Thus the GoI token machine generates operationally the strategy $[[M]]$ in AJM game semantics, by computing the “next move” by Player (the program under scrutiny) as a (partial) function of the previous move by Opponent (the execution environment). This simple generation mechanism exploits that the strategies interpreting $\lambda$-terms in AJM games are history-free, and only depend on the previous move and not the rest of the play (in AJM jargon, $f_M$ is the “history-free skeleton”).

Baillot proves this for IMELL, Intuitionistic Multiplicative Exponential Linear Logic, which includes the simply-typed $\lambda$-calculus. In this restricted case, this is an elegant solution to our problem: the strategy interpreting a term in a well-established, mainstream game semantics, normally obtained from the term in a denotational, compositional way, is alternatively computed operationally by executing $M$ in the so-called “Interaction Abstract Machine” [Danos et al. 1996]. This is a great inspiration to us, but in terms of expressivity as a programming language IMELL is somewhat trivial – essentially the simply-typed $\lambda$-calculus. Baillot’s technical toolbox does not extend beyond IMELL: it is unclear what is the right extension of proof nets, the token machine is too sequential and allows no memory, and even the notion of “generation of a strategy” is inadequate as the target strategies in game semantics are no longer history-free – we need new tools.

## 1.3 Multi-Token GoI via Petri Nets

In this paper we aim for a result analogous to Theorem 1.1 on a far end of the expressivity spectrum: a language we call *Idealized Parallel Algol* (IPA, see Section 3.1) with a combination of complex programming language features: higher-order, recursion, concurrency, local state and semaphores.

If we are to follow Baillot’s lead, we need a notion of proof net for IPA, a GoI token machine, a game semantics, and an appropriate notion of operational “generation” of a strategy. Concerning the game semantics, IPA has the advantage of being well-studied: it is a cosmetic variation of the language ICA for which Ghica and Murawski have provided an interleaving fully abstract game model [Ghica and Murawski 2008] based on a non-alternating version of Hyland-Ong games [Hyland and Ong 2000]. More recently, Castellan and Clairambault [Castellan and Clairambault 2020] have refined it into a *causal* fully abstract game model based on concurrent games on event structures [Castellan et al. 2017]. The concurrent game model projects onto Ghica and Murawski’s [Castellan and Clairambault 2020] but is more fine-grained: it carries all information about non-deterministic branching and causal dependence and independence between computational events, in the style of *true concurrency* models. It also deals with replication in a way that is analogous with AJM games, using *copy indices* that reflect the *exponential signatures* of the token machine.

On the GoI side, token machines were extended in multiple ways: they were redeveloped in a coalgebraic setting supporting a range of algebraic effects (e.g. nondeterminism, probability, exceptions, global state, interactive I/O, etc.) [Hoshino et al. 2014; Muroya et al. 2016]; and for quantitative effects up to quantum primitives [Dal Lago et al. 2017; Hasuo and Hoshino 2017]. They were extended to *multi-token* machines, for Linear Logic [Laurent 2001] or for functional programs [Dal Lago et al. 2014, 2015] (including in call-by-value) or interaction nets [Dal Lago et al. 2014]; up to multiport interaction nets [Dal Lago et al. 2017] which encompasses concurrent
<figure><img src="image_9.png" /><figcaption>Fig. 5. Parallelism</figcaption></figure>

<figure><img src="image_10.png" /><figcaption>Fig. 6. Non-determinism</figcaption></figure>

behaviour through the translation of the π-calculus [Mazza 2005]. In principle, one could obtain a multi-token machine for IPA by translating terms to the π-calculus and then multiport interaction nets. But generalizing Theorem 1.1 would require all translations to preserve the causal semantics, and the state of the art leaves us unprepared for that. Instead we design a multi-token machine operating on a structure directly obtained from the IPA source code. It is not so surprising that such a machine can be designed, but its correctness is a challenge: GoI correctness proofs usually rest on proof-theoretic techniques, e.g. exploiting the cut elimination result of proof nets or via realizability models, none of which are available for higher-order shared memory concurrency. To solve that we adopt a novel methodology: the adequacy of our multi-token GoI will leverage recent progress in concurrent game semantics of programming languages, via our unfolding theorem.

So how shall we obtain a GoI token machine for IPA? We cannot follow the traditional route exposed before, as it is unclear what would be a fitting notion of proof net. Instead, our idea is to skip proof nets altogether, and directly translate programs into graphs *already equipped with the token game*. Ignoring at first the exponential signatures, it should be clear that the proof nets of Section 1.2 equipped with the token game are finite state machines: the states are simply the possible positions of the token on the proof net. As IPA is a concurrent language, its token machine must have multiple tokens: this invites a translation of programs into *Petri nets*.

*Petri Nets*. Petri nets are multi-token finite automata; they are one of the most well-established "truly concurrent" models in concurrency theory; their use is widespread in computer science and beyond. Roughly speaking, a Petri net is a bipartite directed graph, whose nodes are either *locations* (drawn as circles), or *transitions* (drawn as rectangles). Locations may contain one or several *tokens*, denoted as black dots for now. Locations with edges to a transition *t* are called the *preconditions* of *t*, while locations with an edge from *t* are its *postconditions*. The *token game* consists in *firings*

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

which can occur if all pre-conditions are inhabited – the effect is to remove one token on each pre-condition (unlike what the diagram suggests, there may be several), and add one token on each post-condition. From this simple rule emerges complex concurrent phenomena, reviewed now. In Figure 5 we show a Petri net with a simple parallel behaviour: the initial transition **fork** enables transitions **a** and **b**, which occur completely independently of each other. Once both have fired, **join** may occur. This behaviour may equivalently be displayed as the partial order drawn on the right hand side. In Figure 6, we show a net with a simple non-deterministic behaviour as both transitions **a** and **b** compete for the same token. To draw this in partial order style, we need an additional *conflict relation*, pictured as a wiggly line, which indicates that **a** and **b** are incompatible – together,
<figure><img src="image_12.png" /><figcaption>Fig. 7. Recursion</figcaption></figure>

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

<figure><img src="image_14.png" /><figcaption>Fig. 8. Loops with conflict</figcaption></figure>

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

the partial order and the conflict relation form an *event structure* [Winskel 1986]. Petri nets are *folded* structures: they may comprise *loops*. Just like possibly cyclic finite transition systems unfold to infinite trees, Petri nets unfold to event structures [Hayman and Winskel 2008; Nielsen et al. 1981]: this is illustrated in Figure 7 and in the presence of other phenomena in Figure 8.

In our work, a program will be translated to a Petri net and the matching concurrent strategy will be its unfolding. But IPA is not a linear or affine language. Looking back at the GoI token machine of Section 1.2, it appears that tokens must carry an additional piece of data: an *exponential signature*. Petri nets where the tokens carry an additional data are called *coloured Petri nets*: there, tokens have a distinguished identity formalized as an element of a given set of *colours*, and transitions

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

specify the new colours via a transition function, e.g. here $\delta(t)(c_1, \dots, c_n) = (c'_1, \dots, c'_k)$.

In this paper we introduce *Petri structures*, certain coloured Petri nets, and aim to translate programs to Petri structures systematically. But how shall we do that?

## 1.4 Compositional Construction of Coloured Petri Nets

Just like the translation of a term to a proof net, we shall translate programs compositionally, so that the net reflects the structure of the term. It is convenient to set this up as for a denotational semantics: we provide Petri structures for the basic building blocks of IPA, and assemble them by equipping Petri structures with adequate categorical-like operations. Some existing works already propose ways to compose Petri nets: notably, the *open Petri nets* of [Baez and Master 2020], note also the compositional unfolding of coloured Petri nets of [Chatain and Fabre 2010].

In these works, Petri nets communicate via *locations*: the external interface of an open Petri net consists in certain locations on which tokens may be exchanged with the environment. In contrast, our Petri structures communicate via *transitions*: the external interface of a Petri structure consists in distinguished “visible” transitions via which the net can receive (for *negative* transitions) and send (for *positive* transition) tokens to the outside world. Petri structures “from A to B” have shape

<figure><img src="image_17.png" /></figure>
<figure><img src="image_18.png" /><figcaption>Fig. 9. Composition of Petri nets</figcaption></figure>

where A and B respectively inform sets of addresses {$m_1, \dots, m_k$} and {$m'_1, \dots, m'_n$}. This is inspired by the connection of the traditional GoI token machine with game semantics: the $m_i$s and $m'_i$s correspond to occurrences of atoms in dangling wires. In Section 1.2, receiving an Opponent move (m, e) puts a new token with colour e on the dangling wire corresponding to m – we regard this as firing the negative transition m with input e from the environment, introducing a new token inside the net. Thus we regard visible transitions as *channels* using which the net can communicate with the outside world: firing a negative transition matching m *receives* a token e on channel m and (usually, but not necessarily) puts it in an internal location; firing a positive transition matching m with token e on the precondition (usually) sends e to the outside world on channel m.

These Petri structures can be composed simply by synchronizing them on their matching visible transitions, as illustrated in Figure 9 – see the formal definition in Section 2.2.2. Formerly visible transitions synchronize into an internal transition which we consider to have a new *neutral* (0) polarity, allowing tokens to flow silently between the two composed Petri structures.

## 1.5 Contributions and Outline

*Contributions.* Firstly, we give a translation of IPA into certain coloured Petri nets called *Petri structures*. This is done as a translation $\llbracket - \rrbracket_{\text{PStruct}} : \text{IPA} \to \text{PStruct}$ phrased as a denotational interpretation by induction on syntax. For *M* a program, $\llbracket M \rrbracket$ is regarded as the multi-token machine loaded with *M*. We define a token game, which – as a corollary from further results of the paper – satisfies *adequacy w.r.t.* the reference operational semantics of IPA (Theorem 3.10).

Secondly, we construct an unfolding to Strat, the concurrent games causal model of IPA [Castellan and Clairambault 2020]. But we cannot go directly from PStruct to Strat: morphisms in PStruct are arbitrary nets whose behaviour need not be semantically sensible. In contrast, in Strat, programs yield strategies which must respect the rules of a *game*, derived from the type of the program. To bridge the gap, we define a new (pre)category PStrat, a hybrid between Petri structures and game semantics. Its objects are games (as in Strat) and its morphisms are *strategic Petri structures* or *Petri strategies*, whose behaviour abides by the game and that satisfy an additional *safety* condition. This gives a second interpretation $\llbracket - \rrbracket_{\text{PStrat}} : \text{IPA} \to \text{PStrat}$, but we insist that Petri strategies are simply Petri structures satisfying additional invariants: $\llbracket M \rrbracket_{\text{PStruct}}$ and $\llbracket M \rrbracket_{\text{PStrat}}$ are the same net, and there is an identity-on-morphisms $\mathcal{F} : \text{PStrat} \to \text{PStruct}$ preserving the interpretation.

We then extend the unfolding of Petri nets to an interpretation-preserving functor

$\mathcal{U} : \text{PStrat} \to \text{Strat},$
the main challenge being that unfolding is compatible with composition. Altogether we get

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

a commuting diagram letting us deduce adequacy of GoI from the adequacy theorem in Strat. But we regard (2) as a much stronger adequacy theorem: this diagram expresses that even for open, higher-order terms, the *causal* behaviour specified operationally by the GoI multi-token machine coincides with the behaviour specified denotationally by the concurrent games semantics in Strat.

As a final contribution, the multi-token machine for IPA is fully implemented and available at https://ipatopetrinets.github.io/.

*Outline.* In Section 2 we introduce Petri structures and the core operations on them. In Section 3, we recall IPA and provide Petri structures for its primitives, altogether providing our interpretation. In Section 4, we briefly recall concurrent games, introduce PStrat and describe the unfolding. In Section 5 we describe our implementation, and in Section 6 we conclude.

# 2 PETRI STRUCTURES

In this section we introduce our representation of programs called *Petri structures* and show their main compositionality properties. In Section 2.1, we give the formal definition of Petri structures. In Section 2.2, we show that Petri structures naturally form a (pre)category, i.e. a category without unit laws. In Section 2.3, we discuss how to represent nonlinear programs.

## 2.1 Definition and Examples

The definition of Petri structures depends on two parameters: firstly, a set *Tok* of *tokens*. This is the set of *colours*, the same for all locations. Secondly, a set *M* of *addresses*, serving the role of the “multiplicative addresses” from the introduction. Each *m* ∈ *M* has a *polarity* *pol(m)* ∈ {−, +}, specifying whether it is a label for actions by the program (+) or the environment (−). In our interpretation these two sets have a concrete definition, which we shall postpone until later on.

As a convention we write ♦ for set-theoretic union, when it is assumed or known disjoint.

*Definition 2.1.* A **Petri structure** on *M* ⊆*f* *M* is a tuple

$$ \sigma = \langle \mathcal{L}, \mathcal{T} = \mathcal{T}^{+} \uplus \mathcal{T}^{0} \uplus \mathcal{T}^{-}, \partial, \text{pre}, \text{post}, \delta \rangle $$

where *L* is a finite set of **locations**, *T* is a finite set of **transitions** sorted by *polarity* +, 0 or −,

*∂* is a labeling *T*⁺ ♦ *T*⁻ → *M* preserving polarity,

*pre* is a function *T* → *P(L)* of **pre-conditions**,

*post* is a function *T* → *P(L)* of **post-conditions**,

such that pre(*t*⁻) = ∅, post(*t*⁺) = ∅ for all transitions with the indicated polarity; and *δ* assigns to any *t* ∈ *T* a partial function, the **transition function**, typed according to:

*δ(t°)* : cond(pre(t)) → cond(post(t)),

*δ(t⁻)* : *Tok* → cond(post(t)),

*δ(t⁺)* : cond(pre(t)) → *Tok*,

where cond(*L*) = *Tok*<sup>*L*</sup> is the set of **conditions** of support *L* – we write cond the set of all conditions.

Hopefully, the earlier discussion makes this definition natural. To illustrate it, we start by exhibiting a few Petri structures with limited interaction with the environment.
<figure><img src="image_20.png" /><figcaption>Fig. 10.</figcaption></figure>

<figure><img src="image_21.png" /><figcaption>Fig. 11. Petri structure for skip $\parallel$ skip : $\mathbb{U}$</figcaption></figure>

$$ 
\begin{align*}
\delta(\mathbb{Q}) (\bullet) &= \{\bullet^{\textcircled{1}}, \bullet^{\textcircled{2}}\} \\
\delta(a) (\{\bullet^{\textcircled{1}}\}) &= \{\textcircled{3}\} \\
\delta(b) (\{\bullet^{\textcircled{2}}\}) &= \{\textcircled{4}\} \\
\delta(c) (\{v^{\textcircled{3}}\}) &= \{v^{\textcircled{5}}\} \\
\delta(d) (\{v^{\textcircled{4}}\}) &= \{v^{\textcircled{6}}\} \\
\delta(\Lambda) (\{\textcircled{3}, v^{\textcircled{6}}\}) &= v
\end{align*}
$$

<figure><img src="image_22.png" /><figcaption>Fig. 12. Petri structure for coin : $\mathbb{B}$</figcaption></figure>

$$ 
\begin{align*}
\delta(\mathbb{Q}) (\bullet) &= \{1^{\textcircled{1}}, 0^{\textcircled{2}}, \bullet^{\textcircled{3}}\} \\
\delta(w) (\{n^{\textcircled{1}}, p^{\textcircled{2}}\}) &= \{\textcircled{4}, n^{\textcircled{2}}\} \\
\delta(r) (\{n^{\textcircled{2}}, \bullet^{\textcircled{3}}\}) &= \{n^{\textcircled{2}}, n^{\textcircled{5}}\} \\
\delta(\Lambda) (\{\textcircled{4}, n^{\textcircled{5}}\}) &= \text{iszero}(n)
\end{align*}
$$

### 2.1.1 Closed Petri structures.
This limited interaction will take place via two addresses $\mathbb{Q}$ (negative, for “Question” – the channel used by the environment to initiate computation) and $\mathbb{A}$ (positive, for “Answer” – the channel used by the program to return a value); so we temporarily fix $\mathcal{M} = \{\mathbb{Q}^{-}, \mathbb{A}^{+}\}$. Our first examples include no duplication of resources, hence there is no need for exponential signatures yet. However, and unlike for the plain $\lambda$-calculus of Section 1.2, we will need tokens to carry values that may arise during computation. We define the **data signatures**

$$ \mathcal{D} ::= n \mid t \mid \mathfrak{f} \mid \checkmark \mid \bullet \qquad (3) $$

that reflect the values of ground datatypes in IPA, with $\bullet$ a special dummy data, used to fill the data field for tokens with no defined value. We temporarily fix $\text{Tok} = \mathcal{D}$.

We draw a Petri structure $\sigma$ following the conventions introduced earlier: locations are circles, transitions are boxes – note that in our diagrams in the paper, the integers appearing in locations are not tokens, but simply identifiers for the locations. Altogether the graph drawn carries the information of $\mathcal{L}$, $\mathcal{T}$, pre and post, while $\delta$ is a separate transition table. Whenever unambiguous, we name visible transitions simply as their label via $\partial$. If $L = \{l_1, \dots, l_n\} \subseteq \mathcal{L}$, a condition $(t_i)_{i \in L} \in \text{cond}(L)$ is written $\{t_1^{\textcircled{l_1}}, \dots, t_n^{\textcircled{l_n}}\}$ where each $l_i \in L$ appears exactly once. An individual $t^\text{\textit{l}}$ (for $t \in \text{Tok}, l \in \mathcal{L}$) is called a **token-in-location**, or **tokil** – we write $\text{Tokl}(\sigma)$ for the set of tokils.

We start with the Petri structure skip in Figure 10: it shall interpret the constant skip : $\mathbb{U}$ of IPA, the unique value of type $\mathbb{U}$, which performs no action. Upon being triggered by receiving $\bullet$ on $\mathbb{Q}^{-}$, the net prepares data $\checkmark$ in location 1 by $\delta(\mathbb{Q}^{-})(\bullet) = \{\textcircled{1}\}$. This enables $\mathbb{A}^{+}$, which outputs the value $\checkmark$ via $\delta(\Lambda^{+})(\{v^{\textcircled{1}}\}) = v$. Note that in this transition, $v$ stands for any token, so – for now – any data value in $\mathcal{D}$. Next, Figure 11 presents a parallel evaluation of skip $\parallel$ skip. When triggered the net throws two tokils $\bullet^{\textcircled{1}}$ and $\bullet^{\textcircled{2}}$ corresponding to evaluation requests for the two constants. Both tokils are forwarded to an independent copy of the structure of Figure 10. Upon receiving the two values in locations 5 and 6, the last transition fires and outputs $\checkmark$ on $\mathbb{A}^{+}$. The example – or its closed variant obtained by the interpretation – may be run here.

Petri nets can also represent shared state: Figure 12 shows the closed Petri structure for the term

$$ \vdash \text{newref } r \text{ in } (r := 1 \parallel \text{iszero } !r) : \mathbb{B} \qquad (4) $$

written coin, a non-deterministic choice obtained by setting up a race in the memory (by convention newref initializes $r$ to 0). Though we have not yet introduced IPA, we hope this example is clear – in particular it is worth pointing out our nonstandard typing rule for parallel composition, which allows us to put a program of unit type in parallel with a program of arbitrary ground type.

Upon initialization (by receiving $\bullet$ on $\mathbb{Q}^{-}$), the net throws three tokens: the tokil $0^{\textcircled{2}}$ initializes the variable to 0; the tokil $1^{\textcircled{1}}$ is a write request for the value 1; and $\bullet^{\textcircled{3}}$ is a read request. There is a race between the read $r$ and the write $w$: if $r$ wins, the value in location 5 ends up being 0. If $w$ wins then $r$ reads value 1 instead. The final transition waits for the write acknowledgment and the result of the read to send the value read on $\mathbb{A}^{+}$. This example may be run in the implementation here.
<figure><img src="image_23.png" /><figcaption>Fig. 13. An open Petri structure for $g: \mathbb{U} \to \mathbb{U}, x: \mathbb{U} \vdash g x: \mathbb{U}$</figcaption></figure>

$$ 
\begin{align*}
\delta(\ell_c^Q) (\bullet) &= \{\bullet^@1\} & \delta(\ell_c^g \ell_c^Q) (\{\bullet^@1\}) &= \bullet \\
\delta(\ell_c^g \ell_c^Q) (\bullet) &= \{\bullet^@2\} & \delta(\ell_c^g \ell_c^Q) (\{\bullet^@2\}) &= \bullet \\
\delta(\ell_c^x \ell_c^A) (\checkmark) &= \{\checkmark^@3\} & \delta(\ell_c^g \ell_c^A) (\{\checkmark^@3\}) &= \checkmark \\
\delta(\ell_c^g \ell_c^A) (\checkmark) &= \{\checkmark^@4\} & \delta(\ell_c^A) (\{\checkmark^@4\}) &= \checkmark
\end{align*}
$$

### 2.1.2 Open Petri structures.
The addresses $Q^-$ and $A^+$ are enough to represent the limited interactive behaviour of closed programs of ground type, but open programs will require a wider range of addresses. For instance, Petri structures corresponding to programs typed with $g: \mathbb{U} \to \mathbb{U}, x: \mathbb{U} \vdash \mathbb{U}$ will commucate with their environment through the following addresses:

$$ M = \{\ell_c^g \ell_c^Q^-, \ell_c^g \ell_c^A^+, \ell_c^g \ell_c^Q^+, \ell_c^g \ell_c^A^-, \ell_c^x \ell_c^Q^+, \ell_c^x \ell_c^A^-, \tau_c^Q^-, \tau_c^A^+\} $$

where the injections $\ell_c$ and $\tau_c$ indicate the two sides of $\vdash$; $\ell_c^x$ and $\ell_c^g$ point to a variable name; $\ell_c^-$ and $\tau_c^-$ point to either side of an arrow $\to$; and Q and A stand for “Question” (call) or “Answer” (return). Without Q and A, each element of M corresponds to an occurrence of a base type in $g: \mathbb{U} \to \mathbb{U}, x: \mathbb{U} \vdash \mathbb{U}$, and each such occurrence admits a call (Q) and a return (A).

Based on this set of addresses $M$, we show in Figure 13 the Petri structure for $g: \mathbb{U} \to \mathbb{U}, x: \mathbb{U} \vdash g x: \mathbb{U}$. Upon initialization when receiving token $\bullet$ on $\tau_c^Q^-$, the net interrogates the return value of $g$ by sending $\bullet$ on $\ell_c^g \ell_c^Q^+$. If $g$ calls its argument with $\ell_c^g \ell_c^Q^-$, the net interrogates the return value of $x$. If $x$ returns a value with $\ell_c^x \ell_c^A^-$, this value is propagated to the argument of $g$. Finally, if $g$ returns with $\ell_c^g \ell_c^A$, the value is forwarded to the right hand side via $\tau_c^A^+$. Readers familiar with proof nets will recognize the axiom links in the wiring of Figure 13, readers familiar with game semantics will recognize pairs of Opponent moves and induced Player responses. This example may be run here – for clarity the implementation displays the hierarchical relationship between calls and returns, even though those are not part of the Petri structure.

The set $M$ used for this example is a subset of the full set of **addresses**, defined as

$$ M ::= \ell_c^\diamond M | \tau_c^\diamond M | \ell_c M | \tau_c M | \ell_c^- M | \tau_c^- M | i_c^x M | w_c M | \tau_c^\diamond M | g_c^\diamond M | \tau_c^\diamond M | Q A, $$

for $x$ any element of a countable set $\text{Var}$ of variables – we use $m$ to range over addresses. These addresses allow us to represent explicitly the tags in disjoint union: for instance, the tensor of two set of addresses $M$ and $M'$ is $M \otimes M' = \ell_c^\diamond(M) \stackrel{\cdot}{\leftrightarrow} \tau_c^\diamond(M')$ where e.g. $\ell_c^\diamond(M) = \{\ell_c^m | m \in M\}$. Other constructions are used similarly; the constructors indexed by $\mathbb{V}$ and $\mathbb{S}$ correspond to addresses for reference and semaphore types. The **polarity** of addresses is defined as $\text{pol}(Q) = -, \text{pol}(A) = +, \text{pol}(\ell_c^m) = -\text{pol}(m), \text{pol}(\ell_c^-m) = -\text{pol}(m)$, and preserved in all other cases.

## 2.2 The Precategory PStruct

At the core of our approach is the composition of Petri structures, and the corresponding identities – one might expect those to form a category. We shall see that though composition is associative (up to isomorphism), the identity laws fail (even up to isomorphism), calling for the next notion:

### 2.2.1 Precategories.
It is good to keep in mind that Petri structures should really be regarded not as a semantics, but as an alternative representation of syntax. So composing a Petri structure with the identity plugs it into a purely forwarder net which, though not changing the *behaviour* (as made formal by the unfolding in Section 4), does add new transitions and locations.

Thus we get a structure with associativity but no identity laws, a **precategory**:

**Definition 2.2.** A (small) **precategory** $C$ is given by: (1) a set of **objects** $C_0$; (2) for each $A, B \in C_0$ a set of **morphisms** $C(A, B)$; (3) for each $A \in C_0$, an **identity** $\text{id}_A \in C(A, A)$; and (4) for each
$f \in C(A, B)$ and $g \in C(B, C)$, a **composition** $g \circ f \in C(A, C)$; which is associative, i.e. we have

$$h \circ (g \circ f) = (h \circ g) \circ f$$

for all $f \in C(A, B)$, $g \in C(B, C)$ and $h \in C(C, D)$.

A category is in particular a precategory, and the definition of **functors** between categories applies transparently to precategories. We insist that we do not demand $id_B \circ f = f \circ id_A = f$. One might wonder what it means to call something an “identity” without identity laws. The point is that functors must still preserve these “identities”, so in particular a functor from a precategory to a category (such as $\mathcal{U}$ in this paper) will send $id_A$ to an actual identity with identity laws.

Before defining the precategory PStruct, we need one final component:

**Definition 2.3.** Consider $\sigma, \tau$ two Petri structures on $M \subseteq \mathcal{M}$. An **isomorphism** $\varphi : \sigma \cong \tau$ consists of bijections $\varphi_L : \mathcal{L}_\sigma \cong \mathcal{L}_\tau$ and $\varphi_T : \mathcal{T}_\sigma \cong \mathcal{T}_\tau$ compatible with all structure.

Two Petri structures $\sigma$ and $\tau$ on $M$ are **isomorphic**, written $\sigma \cong \tau$, if there is an (unspecified) isomorphism $\varphi : \sigma \cong \tau$. This is an equivalence relation on Petri structures on $M$. Now we set:

**Definition 2.4.** The precategory PStruct has: (1) objects, all finite subsets of $\mathcal{M}$; (2) morphisms from $M$ to $N$, isomorphism classes of Petri structures on $M \vdash N = \ell_+(M) \triangleright \ell_+(N)$; (3) composition and identities, described respectively in Sections 2.2.2 and 2.2.3.

Though morphisms of PStruct are isomorphism classes of Petri structures, in the sequel we shall treat them as concrete Petri structures, keeping in mind the additional proof obligation that all constructions must preserve isomorphisms (which is always straightforward). Thus we may write $\sigma \in PStruct(M, N)$ for $\sigma$ a concrete Petri structure, or simply $\sigma : M \vdash N$.

As stated before, we shall formulate the translation of IPA to Petri structures as an interpretation of programs in PStruct. While this interpretation adopts the language and methodology of denotational semantics, it is not a denotational semantics in the popular sense of being an invariant of reduction. The Petri structure of a term certainly changes under reduction: the first symptom of that is the fact that identity laws are missing in PStruct. We argue that despite the missing equations the translation remains compositional, in the sense that the translation of a compound expression is a function of the interpretation of its components. It is compositional in the same sense that e.g. the translations of the $\lambda$-calculus to proof nets or to the $\pi$-calculus are compositional.

### 2.2.2 Composition.
Fix two Petri structures $\sigma \in PStruct(M, N)$ and $\tau \in PStruct(N, P)$; we aim to define $\tau \circ \sigma \in PStruct(M, P)$, their *composition*. Composing $\sigma$ and $\tau$ amounts to synchronizing $\sigma$'s visible transitions on the right with $\tau$'s visible transitions on the left:

**Definition 2.5.** Visible $t^\sigma \in \mathcal{T}_\sigma^+ \triangleright \mathcal{T}_\sigma^-$ and $t^\tau \in \mathcal{T}_\tau^+ \triangleright \mathcal{T}_\tau^-$ are **synchronizable** if they have opposite polarities; and $\partial_\sigma(t^\sigma) = \tau_+^m$, $\partial_\tau(t^\tau) = \ell_+^m$ for some $m \in N$. We define the set of transitions:

$$ \begin{align*} \mathcal{T}_{\tau} \otimes \mathcal{T}_{\sigma} &= \{ \ell^{\circ}(t) \mid t \in \mathcal{T}_{\sigma}^{0} \triangleright \mathcal{T}_{\sigma}^{p, \ell_{+}} \} \\ &\quad \triangleright \{ \tau^{\circ}(t) \mid t \in \mathcal{T}_{\tau}^{0} \triangleright \mathcal{T}_{\tau}^{p, \tau} \} \\ &\quad \triangleright \{ t^{\sigma} \otimes t^{\tau} \mid t^{\sigma} \in \mathcal{T}_{\sigma}, t^{\tau} \in \mathcal{T}_{\tau} \text{ synchronizable.} \} \end{align*} $$

with $\mathcal{T}_\sigma^{p,i}$ transitions of polarity $p \in \{-, +\}$ and label $\partial(t) = im$ for $m \in \mathcal{M}$; likewise for $\mathcal{T}_\tau^{p,i}$.

Intuitively, $\mathcal{T}_\tau \otimes \mathcal{T}_\sigma$ imports an unsynchronized $t$ from $\sigma$ as $\ell^\circ(t)$, an unsynchronized $t$ from $\tau$ as $\tau^\circ(t)$, but also a new transition $t^\sigma \otimes t^\tau$ for every synchronizable pair. Here, $\ell^\circ$ and $\tau^\circ$ are formal injections used to keep transitions from $\sigma$ and $\tau$ disjoint. From now on, if $X$ and $Y$ are sets, we write $X +^\circ Y = \ell^\circ(X) \triangleright \tau^\circ(Y)$. We shall use the same convention with other tags later on – or simply write $X + Y = \ell(X) \triangleright \tau(Y)$. Now, we may finally define the **composition** $\tau \circ \sigma : M \vdash P$ as:
$$
\begin{align*}
\text{pre}_{\tau \odot \sigma}(\ell^{\circ}(t)) &= \ell^{\circ}(\text{pre}_{\sigma}(t)) & \text{post}_{\tau \odot \sigma}(\ell^{\circ}(t)) &= \ell^{\circ}(\text{post}_{\sigma}(t)) \\
\text{pre}_{\tau \odot \sigma}(r^{\circ}(t)) &= r^{\circ}(\text{pre}_{\tau}(t)) & \text{post}_{\tau \odot \sigma}(r^{\circ}(t)) &= r^{\circ}(\text{post}_{\tau}(t)) \\
\text{pre}_{\tau \odot \sigma}(t^{+} \otimes t^{-}) &= \ell^{\circ}(\text{pre}_{\sigma}(t^{+})) & \text{post}_{\tau \odot \sigma}(t^{+} \otimes t^{-}) &= r^{\circ}(\text{post}_{\tau}(t^{-})) \\
\text{pre}_{\tau \odot \sigma}(t^{-} \otimes t^{+}) &= r^{\circ}(\text{pre}_{\tau}(t^{+})) & \text{post}_{\tau \odot \sigma}(t^{-} \otimes t^{+}) &= \ell^{\circ}(\text{post}_{\sigma}(t^{-}))
\end{align*}
$$

<figure><img src="image_24.png" /><figcaption>Fig. 15. A composition yielding Figure 11</figcaption></figure>

<figure><img src="image_25.png" /><figcaption>Fig. 16. The Petri structure $\omega_{N \to N}$</figcaption></figure>

**Definition 2.6.** We set $\mathcal{L}_{\tau \odot \sigma} = \mathcal{L}_{\sigma} + \circ \mathcal{L}_{\tau}$; $\mathcal{T}_{\tau \odot \sigma} = \mathcal{T}_{\tau} \otimes \mathcal{T}_{\sigma}$; $\mathcal{T}_{\tau \odot \sigma}^{p} = \mathcal{T}_{\sigma}^{p, \ell_{+}} + \circ \mathcal{T}_{\tau}^{p, \ell_{-}}$ where $p \in \{+, -\}$; $\partial_{\tau \odot \sigma}(\ell^{\circ}(t)) = \partial_{\sigma}(t)$ and $\partial_{\tau \odot \sigma}(r^{\circ}(t)) = \partial_{\tau}(t)$. Conditions are in Figure 14, and:

$$
\begin{align*}
\delta_{\tau \odot \sigma} \langle \ell^{\circ}(t) \rangle (\ell^{\circ}(\alpha)) &= \ell^{\circ} (\delta_{\sigma} \langle t \rangle (\alpha)) \\
\delta_{\tau \odot \sigma} \langle r^{\circ}(t) \rangle (r^{\circ}(\beta)) &= r^{\circ} (\delta_{\tau} \langle t \rangle (\beta)) \\
\delta_{\tau \odot \sigma} \langle t^{+} \otimes t^{-} \rangle (\ell^{\circ}(\alpha)) &= r^{\circ} ((\delta_{\tau} \langle t^{-} \rangle \circ \delta_{\sigma} \langle t^{+} \rangle)(\alpha)) \\
\delta_{\tau \odot \sigma} \langle t^{-} \otimes t^{+} \rangle (r^{\circ}(\beta)) &= \ell^{\circ} ((\delta_{\sigma} \langle t^{-} \rangle \circ \delta_{\tau} \langle t^{+} \rangle)(\beta))
\end{align*}
$$

with $\ell^{\circ}, r^{\circ}$ applied to $\alpha \in \text{cond}_{\sigma}, \beta \in \text{cond}_{\tau}$ by retagging locations, i.e. $\ell^{\circ}(\alpha) = \{(s, d)@^{\ell^{\circ}(l)} | (s, d)@^{l} \in \alpha\} \in \text{cond}_{\tau \odot \sigma}$ and $r^{\circ}(\beta) = \{(s, d)@^{r^{\circ}(l)} | (s, d)@^{l} \in \beta\} \in \text{cond}_{\tau \odot \sigma}$.

We show in Figure 15 an example composition, yielding (up to isomorphism) the structure of Figure 11. Notice how the two copies of Figure 10 glue together the disconnected components – for *calls* and *returns* – of the left hand side operand.

Runs on $\tau \odot \sigma$ happen as follows: at first, the token game is played independently in $\sigma$ and $\tau$. If $\sigma$ wishes to play a positive transition on the right (resp. $\tau$ wishes to play a positive transition on the left), it synchronizes with a matching negative transition on the other side – if it exists. The resulting (neutral) synchronized transition has transition function the composite of the synchronized transitions. The effect is that tokens “jump” between $\sigma$ and $\tau$, following the control flow.

### 2.2.3 The copycat Petri structure.
Next, PStruct requires an “identity”: the copycat Petri structure. Copycat exchanges tokens between left and right, forwarding negative moves on either side to the matching positive move on the other side, keeping tokens otherwise unchanged.

**Definition 2.7.** For $M \subseteq \mathcal{M}$ finite, we define the **copycat Petri structure** on $M$, written $\omega_M$. Its locations are $\mathcal{L}_{\omega_M} = M$, its transitions are $\mathcal{T}_{\omega_M} = M \times \{\ell, r\}$ with polarities as in

$$
\begin{align*}
\mathcal{T}_{\omega_M}^{+} &= (M^{+} \times \{r^{+}\}) \uplus (M^{-} \times \{\ell^{-}\}) \\
\mathcal{T}_{\omega_M}^{-} &= (M^{-} \times \{r^{-}\}) \uplus (M^{+} \times \{\ell^{+}\})
\end{align*}
$$

and no neutral transition, for $M^{+} = \{m \in M | \text{pol}(m) = +\}$, and likewise for $M^{-}$. These transitions are mapped to addresses with $\partial(m, \ell) = \ell_{+}m$ and $\partial(m, r) = r_{-}m$; we set $\text{pre}(m^{+}, r^{+})$, $\text{pre}(m^{-}, \ell^{-})$,
$$
\begin{align*}
\text{pre}_{\sigma \otimes \tau}(\ell^{\otimes}(t)) &= \ell^{\otimes}(\text{pre}_{\sigma}(t)) & \text{post}_{\sigma \otimes \tau}(\ell^{\otimes}(t)) &= \ell^{\otimes}(\text{post}_{\sigma}(t)) \\
\text{pre}_{\sigma \otimes \tau}(r^{\otimes}(t)) &= r^{\otimes}(\text{pre}_{\tau}(t)) & \text{post}_{\sigma \otimes \tau}(r^{\otimes}(t)) &= r^{\otimes}(\text{post}_{\tau}(t))
\end{align*}
$$

<caption>Fig. 17. Pre-conditions and post-conditions for the tensor operation</caption>

post(m⁻, r'), post(m⁺, l) to {m} and pre and post returning Ø elsewhere. Finally:

$$
\begin{align*}
\delta\langle(m^+, r')\rangle(\{(s, d)@m\}) &= (s, d) \\
\delta\langle(m^-, l')\rangle(\{(s, d)@m\}) &= (s, d) \\
\delta\langle(m^-, r')\rangle(s, d) &= \{(s, d)@m\} \\
\delta\langle(m^+, l')\rangle(s, d) &= \{(s, d)@m\},
\end{align*}
$$

altogether giving $c_M : M \vdash M$, a Petri structure from $M$ to $M$.

As an example, we show in Figure 16 the Petri structure $\mathcal{P}_{\mathbb{N} \to \mathbb{N}}$, writing $!\mathbb{N} \to \mathbb{N}$ for the set $\{\ell_{-}Q^{+}, \ell_{-}A^{-}, r_{-}Q^{-}, r_{-}A^{+}\}$ which shall arise as the interpretation of $\mathbb{N} \to \mathbb{N}$.

Composition is associative up to isomorphism, making PStruct a precategory. However, com-
posing with copycat yields a structure with strictly more nodes – copycat will be neutral for
composition only after unfolding as it will unfold to the copycat strategy, see Section 4.

2.2.4 Tensor. Another construction at the core of categorical models of programming languages is the tensor operation, which we now define for Petri structures:

Definition 2.8. Consider $\sigma \in \text{PStruct}(M_1, N_1)$ and $\tau \in \text{PStruct}(M_2, N_2)$.

We set $\mathcal{L}_{\sigma \otimes \tau} = \mathcal{L}_{\sigma} + \otimes \mathcal{L}_{\tau}$; $\mathcal{T}_{\sigma \otimes \tau} = \mathcal{T}_{\sigma} + \otimes \mathcal{T}_{\tau}$ with $\mathcal{T}_{\sigma \otimes \tau}^{p} = \mathcal{T}_{\sigma}^{p} + \otimes \mathcal{T}_{\tau}^{p}$ for $p \in \{+, -\}$;

$$
\begin{align*}
\partial_{\sigma \otimes \tau} (\ell^{\otimes}(t)) &= \ell_{\tau} \ell_{\sigma} m \quad (\partial_{\sigma}(t) = \ell_{\tau} m) \\
\partial_{\sigma \otimes \tau} (r^{\otimes}(t)) &= r_{\tau} \ell_{\sigma} m \quad (\partial_{\sigma}(t) = r_{\tau} m) \\
\partial_{\sigma \otimes \tau} (s^{\otimes}(t)) &= s_{\tau} r_{\sigma} m \quad (\partial_{\tau}(t) = s_{\tau} m) \\
\partial_{\sigma \otimes \tau} (t^{\otimes}(t)) &= t_{\tau} r_{\sigma} m \quad (\partial_{\tau}(t) = t_{\tau} m)
\end{align*}
$$

pre- and post-conditions in Figure 17, and for the transition table we set:

$$
\begin{align*}
\delta_{\sigma \otimes \tau} \langle \ell^{\otimes}(t) \rangle (\ell^{\otimes}(\alpha)) &= \ell^{\otimes} (\delta_{\sigma} \langle t \rangle (\alpha)) \\
\delta_{\sigma \otimes \tau} \langle r^{\otimes}(t) \rangle (r^{\otimes}(\alpha)) &= r^{\otimes} (\delta_{\tau} \langle t \rangle (\alpha))
\end{align*}
$$

with $\ell^\otimes, r^\otimes$ applied on conditions as in Definition 2.6. This yields $\sigma \otimes \tau \in \text{PStruct}(M_1 \otimes M_2, N_1 \otimes N_2)$.

This simply puts σ and τ side by side without interaction. As an example, the Petri structure on the right hand side of the composition symbol in Figure 15 is σ ⊗ σ for σ in Figure 10.

2.3 Exponentials

It is simple to complete the ingredients on Petri structures introduced so far into what could be a
symmetric monoidal closed precategory (we lack currying and structural morphisms), introduced in
Appendix B), sufficient to interpret a linear λ-calculus – the resulting interpretation would yield a
Petri structure that is very close to the GoI token machine described for the linear λ-calculus in
Section 1.2. However, we have yet to deal with the constructions relative to replication of resources.

2.3.1 Tokens. As in traditional GoI, we enrich tokens with exponential signatures so as to be able to address distinct copies of a single resource. This leads us to our definitive notion of tokens:

Definition 2.9. The set Tok of tokens is Tok = E* × D, for D the data signatures from (3),

$$
\mathcal{E} ::= \ell \mathcal{E} | r \mathcal{E} | \langle \mathcal{E}, \mathcal{E} \rangle | \diamond
$$
<figure><img src="image_26.png" /></figure>

$$ \delta_{c_M} \langle \kappa_e \ell_\infty m^- \rangle (e \:: \mathfrak{s}, \mathfrak{d}) = \{ (\ell_e \:: \mathfrak{s}, \mathfrak{d}) \@m^- \} $$

$$ \delta_{c_M} \langle \kappa_e \ell_\infty m^- \rangle (e \:: \mathfrak{s}, \mathfrak{d}) = \{ (\kappa_e \:: \mathfrak{s}, \mathfrak{d}) \@m^- \} $$

$$ \delta_{c_M} \langle \kappa_e \ell_\infty m^+ \rangle (\{ (\ell_e \:: \mathfrak{s}, \mathfrak{d}) \@m^+ \}) = (e \:: \mathfrak{s}, \mathfrak{d}) $$

$$ \delta_{c_M} \langle \kappa_e \ell_\infty m^+ \rangle (\{ (\kappa_e \:: \mathfrak{s}, \mathfrak{d}) \@m^+ \}) = (e \:: \mathfrak{s}, \mathfrak{d}) $$

<caption>Fig. 18. Contraction $c_M$</caption>

is the set of **exponential signatures**, and the set $\mathcal{E}^*$ of finite lists of $\mathcal{E}$ is referred to as **exponential stacks**. We denote exponential stacks via typical list-like notations, e.g. $[] \in \mathcal{E}^*$, $[\diamond, \ell, \diamond] \in \mathcal{E}^*$, etc.

All tokens walking around in Petri structures are now pairs (s, d) of an exponential stack s ∈ $\mathcal{E}^*$, whose length may vary, and a data value d ∈ $\mathcal{D}$. We introduced exponential signatures in Section 1.2; this mechanism corresponds to the linear decomposition of the arrow type A → B as !A → B: !A can be thought of as multiple copies of A indexed by exponential signatures.

Why use exponential stacks and not merely signatures? Linear logic representation of higher-order types have nested exponentials. Each exponential leads to a signature, so we end up with a stack whose length corresponds to the level of nesting. Consider the simple example where a program $f M_1 + f M_2$ interacts with the context $f := \lambda n. n + n$. The program calls f twice with distinct stacks, e.g. $[\ell, \diamond]$ and $[\kappa, \diamond]$. In the first call for instance, the context then reacts by starting two evaluations of $M_1$ with stacks $[\ell, \diamond, e_1]$ and $[\ell, \diamond, e_2]$ where $e_1, e_2$ are two distinct signatures chosen by the context – likewise, we will have $[\kappa, \diamond, e_3]$ and $[\kappa, \diamond, e_4]$ for the second call. In general, stacks alternate between signatures created by the program and signatures created by the context.

If $M \subseteq_f \mathcal{M}$ (an object of PStruct), we set $!M = \mathcal{M}$. The addresses are unchanged, but morally the tokens exchanged have a deeper exponential stack (only enforced formally with PStrat). Though there is no practical difference in PStruct, keeping the notation helps typecheck the constructions.

### 2.3.2 Contraction.
As explained in Section 1.2, contraction exploits exponential signatures to give distinguished identifiers to every resource usage, and to route tokens accordingly in the net. More precisely, we introduce the following Petri structure for $M \subseteq_f \mathcal{M}$:

**Definition 2.10.** The **contraction**, a Petri structure $c_M$ on $!M \vdash !M \otimes !M$, has locations $\mathcal{L}_{c_M} = \mathcal{M}$, transitions $\mathcal{T}_{c_M} = M^+ + (M + \otimes \mathcal{M})$ with polarity as for $\mathcal{M}$, and net and transitions in Figure 18.

In Figure 18 and other forthcoming Petri structures, we omit the transition rules that only propagate tokens with no modification: for instance here, we have $\delta_{c_M} \langle \ell, m^- \rangle (\mathfrak{s}, \mathfrak{d}) = \{ (\mathfrak{s}, \mathfrak{d}) \@m^+ \}$. It is also worth emphasizing that the representation of the net in Figure 18 is symbolic: for each negative $m^- \in \mathcal{M}$ there is a net as in the rhs, for each positive $m^+ \in \mathcal{M}$ a net as in the rhs.

The contraction Petri structure only operates at the top of the exponential stack, leaving everything underneath unchanged. As the token passes through contractions $c_M : !M \vdash !M \otimes !M$ from right to left, it accumulates injections $\ell$ and $\kappa$ at the top of the exponential stack, which may then be used in the other direction to route back to the original resource – as in Figure 4.

### 2.3.3 Promotion.
When interpreting $M N$, $M$ may evaluate $N$ several times, each time passing a different exponential signature. However, since we work compositionally, we have computed a structure $[N]$ (intuitively realising a type $A$) that expects to be evaluated once, and we need to promote it to a structure $[N]^\dagger$ (intuitively realising a type $!A$) that can be evaluated several times.

In traditional GoI, the promotion of $N$ is obtained by wrapping $N$ in a special delimiter called an **exponential box**, which marks the parts of the net being promoted. Special transitions handling exponential stacks are applied when tokens cross the borders of a box. Instead here we rewrite the transitions, leaving the net invariant but changing transition functions as follows:
*Definition 2.11.* Consider $\sigma \in \text{PStruct}(!M, N)$. We set $\mathcal{L}_{\sigma^\dagger} = \mathcal{L}_{\sigma}$, $\mathcal{T}_{\sigma^\dagger} = \mathcal{T}_{\sigma}$ with the same polarities, $\partial_{\sigma^\dagger} = \partial_{\sigma}$, and pre- and post-conditions are also unchanged. Finally, the transition table is:

(1) $\delta_{\sigma^\dagger} \langle t^- \rangle (e :: s, d) = e :: \alpha$ if $\partial_{\sigma}(t) = r_+^-$ and $\delta_{\sigma} \langle t \rangle (s, d) = \alpha$

(2) $\delta_{\sigma^\dagger} \langle t^0 \rangle (e :: \alpha) = e :: \beta$ if $\delta_{\sigma} \langle t \rangle (\alpha) = \beta$

(3) $\delta_{\sigma^\dagger} \langle t^+ \rangle (e :: \alpha) = (e :: s, d)$ if $\partial_{\sigma}(t) = r_+^-$ and $\delta_{\sigma} \langle t \rangle (\alpha) = (s, d)$

(4) $\delta_{\sigma^\dagger} \langle t^+ \rangle (e :: \alpha) = (\langle e, e' \rangle :: s, d)$ if $\partial_{\sigma}(t) = l_+^-$ and $\delta_{\sigma} \langle t \rangle (\alpha) = (e' :: s, d)$

(5) $\delta_{\sigma^\dagger} \langle t^- \rangle (\langle e, e' \rangle :: s, d) = e :: \alpha$ if $\partial_{\sigma}(t) = l_+^-$ and $\delta_{\sigma} \langle t \rangle (e' :: s, d) = \alpha$

where $\partial_{\sigma}(t) = i$ means $\partial_{\sigma}(t) = i \text{m}$ for some $m \in \mathcal{M}$, and $e :: \alpha$ is $\{(e :: s_i, d_i)@l_i | (s_i, d_i)@l_i \in \alpha\}$. With this definition, we obtain $\sigma^\dagger \in \text{PStruct}(!M, !N)$.

In $\sigma^\dagger$, messages on the right hand side from the environment come with an extra signature, which appears at the top of the exponential stacks in incoming tokens (equation 1). Neutral transitions only fire when all the pre-conditions have the same value for that signature but otherwise leave it invariant, in effect creating one independent copy of $\sigma$ for each exponential signature (equation 2). Positive messages on the right hand side reply with the stored signature (equation 3).

The transition functions for the right hand side, if applied unchanged also on the left hand side, would intuitively yield a Petri structure on $!M \vdash !N$, with one additional layer for the exponential stack on the left hand side. Instead, in order to obtain a Petri structure playing on $!M \vdash !N$, we apply the constructor $\langle -, - \rangle$ to pack (equation 4) or unpack (equation 5) two levels of the stack into one. This amounts to inlining the “digging” operation from linear logic.

This way of handling promotion without boxes is original to this work, and only possible thanks to the flexibility offered by Petri structures. With token machines on proof nets a box is needed, because the transitions only depend on the nature of the crossed node and have no way to take into account in how many exponential boxes we currently are – this impossibility is patched when crossing the box borders. In contrast, here we may directly “edit” the transition function when applying promotion. Of course the correctness of this mechanism without boxes is subtle, it seems unclear how it could be proved via any other way than the unfolding to concurrent games.

### 2.3.4 Dereliction.
The reader may wonder what primitive introduces the “leaves” ♦ of exponential signatures. For each $M \subseteq \mathcal{M}$ there is a Petri structure $\text{der}_M : !M \vdash M$ that corresponds to a single resource usage – it is defined like $\mathcal{C}_M$, except for the only two changed clauses

$$ \delta(\langle m^-, \ell \rangle)(\{(s, d)@m\}) = (\diamond ::= s, d) $$

$$ \delta(\langle m^+, \ell \rangle)(\diamond ::= s, d) = \{(s, d)@m\} $$

adding a removing the dummy exponential signature ♦ as a new layer of the stack on the rhs.

## 3 IPA AND ITS INTERPRETATION

Now that the backbone of Petri structures is set up, we define our language of study and examine the additional primitives on Petri structures required for its interpretation.

### 3.1 The language IPA

IPA is a higher-order call-by-name concurrent language with shared memory and semaphores, serving as a paradigmatic language for these features in the game semantics literature [Ghica and Murawski 2008]. Our variant is more expressive in some ways (in particular, it has a let construct); but it also has the restriction that reference and semaphore types should not appear at the right hand side of an arrow. See Section 3.1.4 for a discussion on this restriction.
<figure><img src="image_27.png" /><figcaption>Fig. 19. Typing rules for IPA</figcaption></figure>

### 3.1.1 Types and terms. The types of IPA are:

$$A, B, C ::= O \mid V \mid S \qquad O ::= U \mid B \mid N \mid A \to O$$

where types generated by $O$ are called **well-opened**. We have $U$ a unit type, $B$ and $N$ respectively types for *booleans* and *natural numbers*, a type $V$ for *integer references*, and $S$ for *semaphores*. The split into *standard types* and *well-opened types* implements that $V$ and $S$ should not appear on the right of an arrow. We refer to $U, B$ and $N$ as **ground types**, and use $X, Y, Z$ to range over those.

We define terms directly via typing rules – throughout this paper, we only consider well-typed terms. **Contexts** are lists of typed variables $x_1 : A_1, \dots, x_n : A_n$, where variables come from a fixed countable set $\text{Var}$. **Typing judgments** have the form $\Gamma \vdash M : A$, with $\Gamma$ a context and $A$ a type.

The typing rules appear in Figure 19: we give a few comments and clarifications. The construction $f(M, N)$ applies to any computable $f: \mathcal{X} \times \mathcal{Y} \to \mathcal{Z}$ (abusing notations to treat $\mathcal{X}, \mathcal{Y}, \mathcal{Z}$ as sets), intended to be evaluated left-to-right. This covers usual primitives: we define $M; N = \text{seq}(M, N)$, with $\text{seq}: \mathcal{X} \times \mathcal{Y} \to \mathcal{Y}$ the projection function. Basic arithmetic primitives are obtained similarly. Our asymmetric rule for parallel composition is unusual: we allow *one* of the threads to return a value of ground type, which makes examples shorter without significantly affecting the language. Conditionals eliminate to ground type, but as usual in call-by-name, a more general conditional can be derived. We refer to constants of ground type as **values**; we use $v$ to range over values of any type, and $n, b$ or $c$ to range over values of respective types $N, B$ or $U$.

### 3.1.2 Examples. We saw in (4) a derived non-deterministic primitive. Another simple program is

$$x : U, y : X \vdash \text{newsem s in grab s}; (x; \text{rel s} \parallel \text{grab s}; y) : X,$$

illustrating the use of semaphores. A semaphore has two state: *free*, or *locked*. The command `grab s` attempts to grab a semaphore `s`. If `s` is free, then `grab s` terminates successfully and makes it locked. If `s` is already locked, then the instruction `grab s` waits until `s` becomes free. The command `rel` (for “release”) is symmetric. Thus in the example above, the second thread is stuck until `x` has successfully completed, triggering the release of `s`, authorizing the `grab s` and giving the green light to `y`. Altogether, the program behaves exactly like sequential composition.

As a final example, IPA allows dynamic creation of references and semaphores: for instance,

$$\vdash (\lambda x. x + x) (\text{newref } r \text{ in } r :=!r + 1; !r) : N$$

returns $1+1=2$, because execution causes the initialization of two independent references. An unbounded number of references can arise in this way if this happens within recursion.

Though IPA is a toy language, it is semantically highly non-trivial, raising realistic challenges.
**3.1.3 Operational semantics.** The reference semantics for IPA is a small-step interleaving operational semantics following closely that of [Ghica and Murawski 2008]. We fix a countable set $\mathcal{L}$ of **memory locations**. A store is $s : \mathcal{L} \to \mathbb{N}$ with finite domain where $\mathbb{N}$ stands, overloading notations, for natural numbers. **Configurations** are $\langle M, s \rangle$ with $s$ a store, $\text{dom}(s) = \{\ell_1, \dots, \ell_n\}$ and $\Sigma \vdash M : A$ with $\Sigma = \ell_1 : \mathbb{V}, \dots, \ell_i : \mathbb{V}, \ell_{i+1} : \mathbb{S}, \dots, \ell_n : \mathbb{S}$. Reduction rules have the form $\langle M, s \rangle \rightsquigarrow \langle M', s' \rangle$ where $\text{dom}(s) = \text{dom}(s')$; we write $\rightsquigarrow^*$ for the reflexive transitive closure. If $\vdash M : \mathbb{X}$, we write $M \searrow \emptyset$ if $\langle M, \emptyset \rangle \rightsquigarrow^* \langle v, \emptyset \rangle$ for some value $v$. Then $M$ **converges**, else it **diverges**.

The detailed rules, essentially as in [Ghica and Murawski 2008], are postponed to Appendix A as they will be referred to only indirectly in this paper (via Theorem 4.5).

**3.1.4 On the restriction on types.** Our version of IPA is restricted to the effect that reference and semaphore types cannot occur on the right hand side of an arrow, i.e. types such as $\mathbb{B} \to \mathbb{V}$ are forbidden. This is because $\mathbb{V}$ is semantically treated like a product $\mathbb{V}_w \times \mathbb{V}_r$ of write-only and a read-only reference – and while products can be curried away when on the left hand side of an arrow, that is not the case for products on the right hand side. Dealing with such products is subtle for reasons already suggested by the call-by-name isomorphism of types $A \to (B \times C) \cong (A \to B) \times (A \to C)$: the product morally generates two copies of A, and tokens must carry additional data indexing those copies. Similar difficulties arise when dealing with **additives** in traditional GoI [Girard 1995] – it can be done, but with the price of additional complications.

We opted for a version of IPA without (implicit) products, because (1) it allows us to emphasize the important concepts of our approach, rather than obfuscating them with additional structure for additives; (2) we believe that functions returning variables or semaphores is a rare pattern in functional programming. In any case, this restricted IPA is sufficient as a proof of concept language – it already has all the behaviours that IPA is designed to study: races, interactions between higher-order and state or semaphores, etc; (3) this is an artefact of products in call-by-name. Our next step is to tackle more realistic programming languages, but those will be in call-by-value. The issue does not arise in call-by-value, as the isomorphism of types above disappears.

## 3.2 IPA-structures

**3.2.1 Definition.** What additional data should a precategory like PStruct have, so as to support an interpretation of IPA following the methodology of denotational semantics? We call our proposed answer **IPA-structures**: those start with the operations available in a categorical model of intuitionistic linear logic, to which we add primitives maching IPA (with no equations required):

*Definition 3.1.* An **IPA-structure** is a precategory $C$, with a distinguished set $C_{\bullet} \subseteq C_0$ of **well-opened** objects – we use $A, B, C$ to range over all objects and $O$ to range over $C_{\bullet}$ – and:

* **Constructions.** We have objects $U, B, N \in C_{\bullet}, V, S, 1 \in C_0$, and:

* **tensor:** for $A, B \in C_0$, there is $A \otimes B \in C_0$,

* **product:** for $(A_x)_{x \in V}$ with $V \subseteq_f \text{Var}, \&_{x \in V} A_x \in C_0$,

* **arrow:** for $A \in C_0$ and $O \in C_{\bullet}$, there is $A \to O \in C_{\bullet}$,

* **bang:** for $A \in C_0$, there is $!A \in C_0$,

with $\&\emptyset = \top$ the product of the empty family.

* **Operations.** We have constructions on morphisms:

$$ \begin{align*} \otimes : & C(A_1, B_1) \times C(A_2, B_2) \to C(A_1 \otimes A_2, B_1 \otimes B_2) \\ \Lambda_{x:A,O}^{\Gamma,\Delta} : & C(\!(\!(&[\Gamma, x : A, \Delta]), O) \to C(\!(\!(&[\Gamma, \Delta]), !A \to O) \\ (-)^{\dagger} : & C(!\Gamma, O) \to C(!\Gamma, !O) \end{align*} $$

where, if $\Gamma = x_1 : A_1, \dots, x_n : A_n$ where $A_i \in C_0$ for all $i$, we write $[\Gamma]$ for $(A_x)_{x \in \{x_1, \dots, x_n\}}$;
<figure><img src="image_28.png" /><figcaption>Fig. 20. Interpretation of IPA in an IPA-structure</figcaption></figure>

<figure><img src="image_29.png" /><figcaption>Fig. 21. Primitives of IPA-structures</figcaption></figure>

• **Primitives.** As listed in Figure 21, where $⊗^0A = 1$, $⊗^1A = A$, $⊗^{n+2}A = A \otimes (⊗^{n+1}A)$, and writing $w_A \in C(!A, 1)$ for $c_A^0$ and $c_A \in C(!A, !A \otimes !A)$ for $c_A^2$.

### 3.2.2 Interpretation of IPA.
The interpretation follows the standard lines of the interpretation of call-by-name languages into models of intuitionistic linear logic. Fix C an IPA-structure.

We interpret the types of IPA as objects of C, with $[U] = U$, $[B] = B$, $[N] = N$, $[V] = V$, $[S] = S$, and finally, $[A \to B] = ![A] \to [B]$. Note that well-opened types are mapped to well-opened objects. Contexts are also interpreted as objects of C, with $[x_1 : A_1, \dots, x_n : A_n] = \bigwedge_{X_i \in \{x_1, \dots, x_n\}} [A_i]$.

To any typed term $\Gamma \vdash M : A$ we associate as interpretation a morphism $[\Gamma \vdash M : A] \in C(![\Gamma], [A])$ sometimes shortened to $[M]$, following the clauses of Figure 20. Thus if we can equip PStruct with this additional structure, we will automatically obtain following the definition above

$$[\neg] : \text{IPA} \to \text{PStruct}$$

a translation sending any IPA program, possibly open and of higher type, to a Petri structure.

### 3.2.3 Relating Interpretations.
Recall that at the heart of our methodology for this paper is the diagram (2) with, in particular, operations $\mathcal{U} : PStrat \to Strat$ and $\mathcal{F} : PStrat \to PStruct$ commuting with the interpretation. As our interpretations shall all follow the interpretation of IPA in an IPA-structure detailed above, interpretation-preserving operations shall be obtained by:

**Definition 3.2.** Consider C and D two IPA-structures, and $F : C \to D$ a functor.

Then, $F$ is a **(strict) IPA-functor** iff it preserves all the data of IPA-structures on the nose.

It follows immediately by induction that the interpretation of types and terms is preserved:

**LEMMA 3.3.** Consider C, D two IPA-structures, and $F : C \to D$ an IPA-functor.

Then, for any $\Gamma \vdash M : A$, we have $F([A])_C = [A]_D$, $F([\Gamma])_C = [\Gamma]_D$, and $F([M])_C = [M]_D$.

To sum up: IPA-structures list the ingredients necessary to give an interpretation to all terms of IPA, and IPA-functors list the proof obligations in order to relate two interpretations. In particular, PStruct, PStrat and Strat from (2) will be IPA-structures, and $\mathcal{F}, \mathcal{U}$ will be IPA-functors.
<figure><img src="image_30.png" /></figure>

$$ 
\begin{aligned}
\delta_{\text{op}(f)}(\ell, r_c A^{-})([], d) \\
&= f([], \bullet)^{\text{@2}}, ([], d)^{\text{@3}} \\
\delta_{\text{op}(f)}(r_c A^{+})([([], d)^{\text{@3}}, ([], d')^{\text{@4}}]) \\
&= ([], f(d, d'))
\end{aligned}
 $$

<figure><img src="image_31.png" /><figcaption>Fig. 22. Operators</figcaption></figure>

$$ 
\begin{aligned}
\delta_{\text{newref}}(r_c Q^{-})([], \bullet) \\
&= \{([], \bullet)^{\text{@1}}, ([], 0)^{\text{@2}}\} \\
\delta_{\text{newref}}(w)(\{([e], d)^{\text{@3}}, (\underline{\quad}, \underline{\quad})^{\text{@2}}\}) \\
&= \{([e], d)^{\text{@2}}, ([e], \checkmark)^{\text{@4}}\} \\
\delta_{\text{newref}}(r)(\{([e], \bullet)^{\text{@5}}, (\underline{\quad}, \underline{\quad})^{\text{@2}}\}) \\
&= \{([e], d)^{\text{@2}}, ([e], d)^{\text{@6}}\}
\end{aligned}
 $$

<figure><img src="image_32.png" /><figcaption>Fig. 24. Let binding</figcaption></figure>

$$ 
\begin{aligned}
\delta_{\text{let}}(\ell, r_c A^{-})([], d) \\
&= \{([], d)^{\text{@2}}, ([], d)^{\text{@3}}\} \\
\delta_{\text{let}}(s)(\{([], d)^{\text{@3}}, (s, \bullet)^{\text{@4}}\}) \\
&= \{([], d)^{\text{@3}}, (s, d)^{\text{@5}}\}
\end{aligned}
 $$

## 3.3 PStruct as an IPA-structure

Completing the precategory PStruct into a full IPA-structure requires providing nets for a number of primitives, most of which are straightforward and detailed in Appendix B. Here we focus on three constructions which we consider more informative or noteworthy.

### 3.3.1 Operators.
For $op(f)_Z^{X,Y} \in PStruct(X \otimes Y, Z)$, the net and its transitions are shown in Figure 22. By convention we omit the transitions that are trivial, in the sense that they merely forward tokens without affecting them (the typing specifying uniquely where these tokens should go).

Upon initialization by receiving $([], \bullet)$ on $r_c Q^{-}$, the net first puts $([], \bullet)$ in location 1 triggering the evaluation request for the first argument, i.e. sending $([], \bullet)$ on $\ell, \ell_{\oplus} A^{-}$. When the first argument returns a value with a message on $\ell, \ell_{\oplus} A^{-}$, the net stores the value in location 3, and puts a token in location 2 to evaluate the second argument. Once the value is received on $\ell, r_c A^{-}$, the pre-conditions of $r_c A^{+}$ are met and the net emits the final result, applying $f$ on the two stored values. Here we see that our machine may use several tokens during computation even for sequential programs: locations are used in the style of the GoI token machines to track the control flow, but also as a way to store intermediate results throughout computation.

### 3.3.2 New reference.
For $newref_X \in PStruct(!V \to X, X)$, the net and its non-trivial transitions are shown in Figure 23. The Petri structure newref takes as an argument $!V \to X$, i.e. a “program of type X” that may query a reference. Location 2 stores the current value. Upon initialization with $r_c Q^{-}$, newref: (1) initializes the reference, setting a token with data 0 in location 2; (2) in parallel, gives control to the argument via $\ell, r_c Q^{+}$. Write and read requests arrive respectively in locations 3 and 5. The neutral transitions w and r perform the memory update and reading. Normally, i.e. in the context of the evaluation of a closed program, there is ever at most one token in location 2 (if the net is under a promotion there may be several, kept apart by their exponential stack), forcing reads and writes to be handled in some sequential order. Note that r overwrites the token in the store even through it does not change the value: this is essential in order to get the unfolding right.

### 3.3.3 Let binding.
For $let_{X,Y} \in C((!X \to Y) \otimes X, Y)$, the net and its non-trivial transitions are shown in Figure 24. At first sight, let is only a write-once reference, with value stored in location 3. But we have seen that in the net for newref, read updates overwrite the token storing the current value. Doing the same for the let binding would sequentialize all reads, which is fine in terms of interleavings but would break our causal unfolding as it is not compatible with the expected causal behaviour of the let binding. So instead, transition r reads the stored value with token $([], d)$, and puts back the exact same token, so that further accesses to the value stored do not depend on it.
See Appendix B for the other constructions, which yield:

**COROLLARY 3.4.** *PStruct is an IPA-structure.*

Following Section 3.2.2 we obtain for any term $\Gamma \vdash M : A$ a net $[[M]] \in \text{PStruct}(![[\Gamma]]], [[A]])$ regarded as the token machine with $M$ loaded. In particular, a closed program $\vdash M : X$ yields a Petri structure $[[M]]$ on $\{r_i^Q, r_i^A\}$ which we can execute by playing the token game.

## 3.4 The Token Game and Adequacy

In order to reason formally on the execution of Petri structures, we now formalize the token game. Its states are called markings, in which each location contains a finite set of tokens.

**Definition 3.5.** Consider $\sigma$ a Petri structure. A marking on $\sigma$ is a finite subset of ToklL.

The set of markings on $\sigma$ is written $\mathcal{M}(\sigma)$, ranged over by $\alpha, \beta, \gamma$.

We use the same notation for markings as for conditions, i.e. $\alpha = \{([], \bullet)^@1, ([], \bullet)^@2, (\diamond), \checkmark)^@2\}$ is a (non-reachable) marking for the Petri structure of Figure 11. Unlike for conditions, markings allow several tokens on the same location; however we cannot have the same token twice on the same location – markings are sets, not multisets. It should be clear from this notation that conditions may be regarded as markings, and we shall do so silently from now on.

The token game is a walk on a labelled transition system of markings. While neutral transitions act on markings only, visible ones send or receive tokens on addresses. Together, an address and a token form a **move** – we set Moves = $M \times E^* \times D \approx M \times \text{Tok}$, ranged over by $m$. The transition system is defined in two steps. First, events are transitions instantiated with specific input:

**Definition 3.6.** An **event** of a Petri structure $\sigma$ is a pair $(t, \iota)$ written $t(|\iota|)$ where $\iota$ is an input of $t$, i.e. a token (s, d) if $t$ is negative or some $\alpha \in \text{cond}(\text{pre}(t))$ otherwise. We write:

$$ 
\begin{align*}
t^0(|\alpha|) & : \alpha \mapsto_{\sigma} \beta & \text{if } \delta\langle t \rangle(\alpha) = \beta, \\
t^+(|\alpha|) & : \alpha \mapsto_{\sigma} \emptyset & \text{if } \delta\langle t \rangle(\alpha) = (s, d), \\
t^-(|\alpha|) & : \emptyset \mapsto_{\sigma} \beta & \text{if } \delta\langle t \rangle(s, d) = \beta,
\end{align*}
$$

where $m = (\partial_\sigma(t), s, d)$ is the move played. We write $\mathcal{E}(\sigma)$ the set of events of $\sigma$, ranged over by $e$.

Events inherit from transitions a polarity. A visible $e$ plays a move $m$, written $m = \partial_\sigma(e) = (m, s, d)$. For negative $e$ the token (s, d) is received on $m$, while for positive $e$, (s, d) is sent on $m$.

Events only mention the tokils involved in the transition, i.e. mentioned in the transition function. To obtain the actual token game, one must allow events to occur in the presence of other tokils sitting in the net, not playing any role in the transition. This is captured by the notion of firings:

**Definition 3.7.** The set $\mathcal{F}(\sigma)$ of firings, ranged over by $f$, comprises

$$ 
\begin{align*}
e^0 \upharpoonright \gamma & : \quad \alpha \upharpoonright \gamma \quad \xrightarrow{\sigma} \quad \beta \upharpoonright \gamma & \text{if } e : \alpha \mapsto_{\sigma} \beta, \\
e^+ \upharpoonright \gamma & : \quad \alpha \upharpoonright \gamma \quad \xrightarrow{\sigma} \quad \gamma & \text{if } e : \alpha \mapsto_{\sigma} \emptyset, \\
e^- \upharpoonright \gamma & : \quad \gamma \quad \xrightarrow{\sigma} \quad \gamma \upharpoonright \beta & \text{if } e : \emptyset \mapsto_{\sigma} \beta.
\end{align*}
$$

for $\gamma \in \mathcal{M}(\sigma)$ with $\gamma \cap \alpha = \gamma \cap \beta = \emptyset$.

Note the disjointness assumption, which means a transition can only fire if the tokils it emits do not collide with tokils already present. Now we can finally capture the token game with:

**Definition 3.8.** A **run** in $\sigma$ is a sequence $\rho = f_1 \dots f_n$ of firings s.t. $f_i : \alpha_i \to_{\sigma} \alpha_{i+1}$ or $f_i : \alpha_i \xrightarrow{m} \sigma$ $\alpha_{i+1}$ with $\alpha_1 = \emptyset$. We write $\rho : \emptyset \to_{\sigma} \alpha_{n+1}$ or $\rho : \emptyset \xrightarrow{s} \sigma \alpha_{n+1}$, where $s = m_1 \dots m_p$ lists the moves of visible firings in $\rho$. We also write $s = \text{play}(\rho)$ and call $s$ the **play** of $\rho$.
<figure><img src="image_33.png" /><figcaption>Fig. 25. A run of a Petri structure</figcaption></figure>

For example, (the variant with full tokens of) Figure 11 has

$$ \begin{array}{ccc} \emptyset & \xrightarrow{\substack{(Q, \llbracket \bullet \rrbracket \\ \bullet) \\ \bullet}} & \{([], \bullet)^{\bullet 1}, ([], \bullet)^{\bullet 2}\} \\ \rightarrow & & \{([], \checkmark)^{\bullet 5}, ([], \bullet)^{\bullet 2}\} \\ \rightarrow & & \{([], \checkmark)^{\bullet 5}, ([], \checkmark)^{\bullet 6}\} \\ \rightarrow & & \emptyset \end{array} \quad \xrightarrow{(A, \llbracket \checkmark \rrbracket)} \quad \{([], \checkmark)^{\bullet 3}, ([], \bullet)^{\bullet 2}\} $$

as a run with play($\rho$) = (Q, [], ●)(A, [], ✓). We read it as tokens walking through the Petri net as in Figure 25 (omitting exponential stacks, which are always [] in this example).

We define may-convergence for Petri structures on {$\kappa Q^-$, $\kappa A^+$}:

**Definition 3.9.** Consider $\sigma$ a Petri structure on {$\kappa Q^-$, $\kappa A^+$}. We say $\sigma$ may converge, written $\sigma \Downarrow$, iff there is a run $\rho: \emptyset \to \sigma$ such that play($\rho$) = ($\kappa Q$, [], ●)($\kappa A$, [], d) for some d $\neq$ ●.

Now that this is set up, we can state formally one of the main results of this paper:

**THEOREM 3.10 (ADEQUACY).** For any $M: \mathcal{U}, M \Downarrow$ iff $[M] \Downarrow$.

This is the standard way of stating that at ground type and with respect to may-convergence, the token machine is faithful to standard operational semantics. But here adequacy shall follow from a much more powerful result, also giving a proper account of higher-order: we shall prove that the Petri structure $[M]$ unfolds to the concurrent strategy for $M$.

# 4 UNFOLDING AND CORRECTNESS

We link to the denotational model of IPA presented in [Castellan and Clairambault 2020], where both types and programs are interpreted as event structures, called games and strategies respectively.

In Section 4.1, we recall basic definitions about this model, yielding Strat, an adequate IPA-structure. We wish to define the unfolding as an IPA-functor from PStruct to Strat, but in general the behaviour of Petri structures is too wild for this. So our following step, performed in Section 4.2, is to tame PStruct, eliminating those nets whose behaviour fails to respect a protocol (the game) specified by the type – this leads to another IPA-structure PStrat of Petri strategies. In Section 4.3, we define a causal reconstruction mapping Petri strategies to strategies, i.e. event structures.

## 4.1 Concurrent Strategies for IPA

**4.1.1 Types as Games.** In PStruct, a type is merely interpreted by a finite set of addresses. This forgets information: (1) the possible values, for instance $\mathbb{B}$ and $\mathbb{N}$ have the same interpretation; (2) the dependency from function calls to returns, and the dependency arising from the scope: in ($\mathbb{N} \to \mathbb{B}$) the natural number should not be interrogated before the boolean. Adding this information yields a game, i.e. an event structure with moves as events. Recall first:
**Definition 4.1.** An **event structure (es)** is $E = (|E|, \le_E, \#_E)$, where $|E|$ is a (countable) set of **events**, $\le_E$ is a partial order and $\#_E$ is an irreflexive symmetric binary relation, satisfying:

**finite causes:** $\forall e \in |E|$, $[e]_E$ is finite

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

where $[e]_E = \{e' \in |E| \mid e' \le_E e\} - \#_E$ and $\le_E$ are respectively **conflict** and **causal dependency**.

We write $\to_E$ for the immediate dependency, i.e. $e \to_E e'$ iff $e <_E e'$ with no event strictly in between. An es $E$ comes with a notion of state, its (finite) **configurations**: those are finite $x \subseteq_f |E|$ down-closed for $\le_E$ and compatible, i.e. if $e, e' \in x$, then $\neg(e \#_E e')$. We write $\mathscr{C}(E)$ the configurations of $E$. If $x \in \mathscr{C}(E)$ and $e \notin x$ with $x \cup \{e\} \in \mathscr{C}(E)$, we say $x$ **enables** $e$, written $x \vdash_E e$.

**Definition 4.2.** Consider $A = (|A|, \le_A, \#_A)$ an es with $|A| \subseteq \text{ Moves}$, and write $\text{mult}(A) = \{m \in \mathcal{M} \mid \exists(m, s, d) \in |A|\}$. Then, $A$ is a **game** if it satisfies the additional axiom:

**finite addresses:** the set $\text{mult}(A)$ is finite.

This is the usual notion of concurrent game, except that moves are taken in Moves and hence the *polarity function* $\text{pol}_A : |A| \to \{-, +\}$ is inherited from Moves and no longer part of the data.

We shall need the more specific *arenas*, capturing the causal patterns arising from types:

**Definition 4.3.** An **arena** is a game $A$ satisfying:

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

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

**local conflict:** if $a_1, a_2 \in |A|$ are in minimal conflict, then $[a_1]_A = [a_2]_A$,

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

where $\min(A)$ is the set of minimal events of $A$. Finally, $A$ is **well-opened** if $\min(A)$ is a singleton.

This used the **strict dependencies** $[a]_A = \{a' \in A \mid a' <_A a\}$, and the notion of **minimal conflict**: in an event structure $E$, $e_1, e_2 \in |E|$ are in **minimal conflict** if $e_1 \#_E e_2$, while if $e'_1 \le_E e_1$ and $e'_2 \le_E e_2$ with at least one of these being strict, then $\neg(e'_1 \#_E e'_2)$ – so the conflict is not inherited.

We omit the interpretation of types and contexts as arenas, see Appendix C.1.

**4.1.2 Strategies.** In concurrent games, strategies are also event structures:

**Definition 4.4.** A **prestrategy** $\sigma : A$ on game $A$ comprises an es $(|\sigma|, \le_\sigma, \#_\sigma)$ with $\partial : |\sigma| \to |A|$ a function called the **display map**, subject to the following conditions:

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

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

We say that $\sigma$ is a **strategy** if it satisfies the further two:

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

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

and is **negative** if any $s \in \min(\sigma)$ is negative.

**Rule-abiding** and **locally injective** together amount to $\partial : \sigma \to A$ being a **map of event structures**. The event structure $\sigma$ presents observable computational events along with their causal dependencies and conflicts. Events of $\sigma$ are not moves of the game, but they do correspond to moves via the action of $\partial$. This permits an explicit representation of non-deterministic branching: several events of $\sigma$ may correspond to the same move if they are conflicting and so belong to separate branches of the execution. The strategy keeps them separate, even if they cannot be distinguished.
**THEOREM 4.5.** *The category Strat forms an IPA-structure, and for any $\vdash M : U, [[M]]_{\text{Strat}} \twoheadleftarrow \text{iff } M \twoheadrightarrow$. See [Castellan and Clairambault 2020]. Here $\sigma : U \text{ converges}$, written $\sigma \twoheadleftarrow$, if it has a $+$-move.

## 4.2 Strategic Petri Structures

Aiming for PStrat, given a game A and a Petri structure $\sigma$ on mult(A), we must define what it means for $\sigma$ to follow the rules of A – intuitively, the runs of $\sigma$ must form valid plays on A:

*Definition 4.6.* A sequence $s = s_1 \dots s_n \in \text{Moves}^*$ is a **play** on A, written $s \in \text{Plays}(A)$, if it is:

*valid:* for all $1 \le i \le n$, $\{s_1, \dots, s_i\} \in \mathscr{C}(A)$,

*non-repetitive:* for all $1 \le i \le j \le n$, if $s_i = s_j$ then $i = j$.

Recall that any run $\rho : \emptyset \to \sigma$ on $\sigma$ generates a sequence play($\rho$) obtained by collecting the visible moves in $\rho$ – we shall ask that $\sigma$ behaves as prescribed by the game as long as Opponent does. But we shall also need a safety condition, required for the unfolding. For that, we set:

*Definition 4.7.* Consider $e : \alpha \mapsto \sigma$ an event of $\sigma$. We call pre($e$) = $\alpha$ the **pre-condition** of $e$, and post($e$) = $\beta$ the **post-condition** of $e$. The set new($e$) = $\beta \setminus \alpha$ contains the tokils produced by $e$; and eat($e$) = $\alpha \setminus \beta$ those consumed. Those extend to firings by ignoring the context.

The distinction between post($f$) and new($f$) matters for let: its transition $s$ (see Section 3.3) requires ([], d)@3 to fire, but leaves it unchanged. So ([], d)@3 is both a pre-condition and a post-condition, but is not produced. Other than for let, pre- and post-conditions are always disjoint.

Our safety constraint uses the notion of collection, which gathers the tokils seen in a run so far:

*Definition 4.8.* Consider $\rho = \mathfrak{f}_1 \dots \mathfrak{f}_n : \emptyset \to \sigma$ $\alpha_{i+1}$, a run of $\sigma$, with $\mathfrak{f}_i : \alpha_i \to \alpha_{i+1}$. The collection of $\rho$ is $\text{Coll}(\rho) = \bigcup_{1 \le i \le n+1} \alpha_i$. We say that $\alpha \in \text{cond}_{\sigma}$ is **fresh in** $\rho$ iff $\alpha \cap \text{Coll}(\rho) = \emptyset$.

This lets us finally define Petri strategies on a game A:

*Definition 4.9.* We say that $\sigma$ is **strategic on** A if for any $\rho : \emptyset \xrightarrow{s} \sigma$ $\alpha$ with $s \in \text{Plays}(A)$,

*valid:* if $\mathfrak{f}^+ : \alpha \xrightarrow{a} \beta$, then $sa \in \text{Plays}(A)$,

*receptive:* if $sa^- \in \text{Plays}(A)$, there is a unique $\mathfrak{e}^- \in \mathscr{E}(\sigma)$ s.t. $\mathfrak{e}^- : \emptyset \xrightarrow{a} \beta$ with $\beta \cap \alpha = \emptyset$,

*strongly safe:* if $\mathfrak{f} : \alpha \to \beta$ or $\mathfrak{f} : \alpha \xrightarrow{a} \beta$ with $sa \in \text{Plays}(A)$, then new($\mathfrak{f}$) is fresh in $\rho$,

we write $\sigma : A$ – additionally, $\sigma : A$ is **negative** iff for all $e^0 : \alpha \mapsto \beta$ or $e^+ : \alpha \mapsto \emptyset$, $\alpha \neq \emptyset$.

*Strong safety* entails that in a given execution, a tokil can occur at most once: it cannot appear, be consumed, and reappear later. Thus for each occurring tokil we can unambiguously identify a *cause*, which will be central in the *unfolding* of Petri strategies to actual strategies – see Section 4.3.

Examples of Petri strategies abound in this paper so far, since it shall follow that for all term $\Gamma \vdash M : A$, the Petri structure $[[M]]$ is a Petri strategy on $![[\Gamma]] \vdash [[A]]$. In contrast, the Petri structure **skip** of Section 2.1.1 does not satisfy e.g. **skip** : N, as there is a clear failure of condition valid.

**PROPOSITION 4.10.** *There is an IPA-structure PStrat, with objects arenas (with the associated constructions), and morphisms from A to B the negative Petri strategies $\sigma : A \vdash B$ up to isomorphism. There is an identity-on-morphisms IPA-functor $\mathcal{F} : PStrat \to PStruct$ sending A to mult(A).*

*PROOF.* We must show that all primitives are strategic, and that all operations preserve the property. The main technical challenge is composition: to show that $\tau \circ \sigma$ is a Petri strategy, we exploit that none of $\sigma$ and $\tau$ can be the first one to break the rules. See details in Appendix D. $\square$
<figure><img src="image_34.png" /><figcaption>Fig. 26. $\text{let } x = \text{skip in } x \parallel x$</figcaption></figure>

<figure><img src="image_35.png" /><figcaption>Fig. 27. Events and maximal valid runs</figcaption></figure>

<figure><img src="image_36.png" /><figcaption>Fig. 28. Max. causal run</figcaption></figure>

## 4.3 The Unfolding of a Petri Strategy

Leveraging strong safety we can give a rather direct definition of unfolding, close to the unfolding of 1-safe Petri nets in [Nielsen and Thiagarajan 2002]. An event structure is a global object, putting together all possible executions with explicit causal and branching information. Our definition first performs a causal reconstruction for individual runs, before patching them together via an already existing operation – that of taking the primes of a rigid family [Castellan et al. 2014b].

### 4.3.1 Causal Reconstruction of Runs.
Fix a Petri strategy $\sigma: A \vdash B$. A valid run on $\sigma$ is $\rho: \emptyset \to \sigma \gamma$ such that play($\rho$) $\in$ Plays($A \vdash B$). Valid runs are the executions that abide by the typing discipline of $A \vdash B$. An event e of $\rho$ is an event e of $\sigma$ such that there exists $\gamma$ with e $\supset$ $\gamma$ a firing in $\rho$. By strong safety, $\gamma$ must be unique. We write $\mathcal{E}(\rho)$ for the set of events of $\rho$. Two runs are equivalent if they have the same events: two equivalent runs only differ by meaningless ordering of some events. This induces a semantic dependence on $\mathcal{E}(\rho)$: $e \leq_{\rho} e'$ iff e occurs before e' in any valid $\rho'$ of $\sigma$ equivalent to $\rho$. Our causal reconstruction relies on a concrete characterization of this.

Intuitively an event e of $\rho$ should directly cause e' if pre(e) $\cap$ post(e') $\neq$ $\emptyset$, however, in some cases (notably for let) the same token may be both consumed and produced – i.e. essentially left in place – and this should be accounted for when computing the dependency. An example of this is illustrated in Figures 27 and 28 (omitting exponential stacks): we have pre(a({•@1, √@x})) $\cap$ post(b({•@2, √@x})) $\neq$ $\emptyset$, and yet those two events may be reordered at will.

So we adjust this and define the **dynamic dependency** between events of a run by

$$e \triangleleft_{\sigma} e' \iff (\text{new}(e) \cap \text{pre}(e') \neq \emptyset) \lor (\text{post}(e) \cap \text{eat}(e') \neq \emptyset),$$

on $\mathcal{E}(\rho)$ for any valid $\rho: \emptyset \to \sigma \gamma$. In other words, $e \triangleleft_{\sigma} e'$ if (1) $e'$ requires a token produced by e; or (2) $e'$ consumes a token that e outputs. We also incorporate the **static dependency**

$$e \triangleleft_{A \vdash B} e' \iff e: \alpha \stackrel{a}{\mapsto} \beta, e': \alpha' \stackrel{a'}{\mapsto} \beta', \text{ where } a \to_{A \vdash B} a'$$

importing on events of $\rho$ the dependencies imposed by the game. Altogether, we obtain:

$$\textbf{PROPOSITION 4.11.} \quad \textit{For } \rho \textit{ a valid run of } \sigma, \leq_{\rho} = (\triangleleft_{A \vdash B} \cup \triangleleft_{\sigma})^*.$$

Posets ($\mathcal{E}(\rho)$, $\leq_{\rho}$) are referred to as **causal runs of $\sigma$**; we write $\mathcal{R}(\sigma)$ for the causal runs of $\sigma$. From Proposition 4.11, valid runs of $\sigma$ are exactly the linearizations of causal runs in $\mathcal{R}(\sigma)$.

A valid run $\rho$ of $\sigma$ comprises visible events (generated by visible transitions) and neutral events (generated by neutral transitions), and this dichotomy transports to causal runs. If $q \in \mathcal{R}(\sigma)$, the set of labels of visible events is by construction a configuration of $A \vdash B$, written $\partial_{\sigma}(q) \in \mathcal{C}(A \vdash B)$.

### 4.3.2 Hiding.
The causal run $\mathcal{E}(\rho)$ associated to a valid run $\rho$ reconstructs causal dependencies among all events in $\rho$, neutral or visible. This contrasts with the game semantics of Section 4.1, which records visible events only. To link them, we use the following definition:
**Definition 4.12.** Consider $q \in \mathcal{R}(\sigma)$. The **hiding** of $q$, written $q_\downarrow$, has

events: those $e \in |q|$ that are visible,

causality: the restriction of $\leq_q$,

and $\partial_\sigma(q_\downarrow) = \partial_\sigma(q) \in \mathcal{C}(A \vdash B)$. We call $q_\downarrow$ a **visible causal run** of $\sigma$, and write $q_\downarrow \in \mathcal{R}^V(\sigma)$.

Visible causal runs are extracted via a causal reconstruction from runs of $\sigma$, which – if $\sigma$ comes from a program $M$ – are executions of $M$ in our multi-token machine. Besides this operational nature, we shall see now that they match the denotational interpretation of $M$ in concurrent games.

**4.3.3 Unfolding to a Strategy.** We aggregate all visible causal runs into one *event structure*, via:

**THEOREM 4.13.** *There exists a strategy $\mathcal{U}(\sigma) : A$, unique up to isomorphism, such that there is an order-isomorphism $\varphi : \mathcal{C}(\mathcal{U}(\sigma)) \cong \mathcal{R}^V(\sigma)$ satisfying $\partial_{\mathcal{U}(\sigma)} = \partial_\sigma \circ \varphi$.*

**PROOF.** The crux is that $\mathcal{C}^V(\sigma)$ forms a *rigid family* [Castellan et al. 2014b], i.e. a set $\mathcal{F}$ of posets closed under prefix and such that any finite directed subset has a supremum. In that case, the structure $\text{Pr}(\mathcal{F}) = (|\text{Pr}(\mathcal{F})|, \leq_{\text{Pr}(\mathcal{F})}, \#_{\text{Pr}(\mathcal{F})})$ defined by the following components

$$ 
\begin{array}{lclcl}
|\text{Pr}(\mathcal{F})| & = & \{q \in \mathcal{F} \mid q \text{ prime}\} & & \\
q & \leq_{\text{Pr}(\mathcal{F})} & p & \Leftrightarrow & q \subseteq p \\
\neg(q \ \#_{\text{Pr}(\mathcal{F})} \ p) & \Leftrightarrow & \{q, p\} \uparrow,
\end{array}
$$

where $q \in \mathcal{F}$ is **prime** iff it has a top element, is an event structure with $\chi_{\mathcal{F}} : \mathcal{C}(\text{Pr}(\mathcal{F})) \cong \mathcal{F}$ an order-isomorphism – this is folklore in event structures, see Appendix E.2.

Using this, we set $\mathcal{U}(\sigma) = \text{Pr}(\mathcal{R}^V(\sigma))$. Its display map is uniquely determined by its action on configurations, defined as $\partial_{\mathcal{U}(\sigma)} = \partial_\sigma \circ \chi_{\mathcal{R}^V(\sigma)}$. All remaining conditions follow. $\square$

An event of $\mathcal{U}(\sigma)$ is not quite an event of $\sigma$, but a causal run with a top – which we regard as an event of $\sigma$ (the top) together with a choice of a causal history leading to it.

**4.3.4 Unfolding as an IPA-functor.** As expected, unfolding preserves the interpretation:

**THEOREM 4.14.** *We have an IPA-functor $\mathcal{U} : \text{PStrat} \to \text{Strat}$.*

**PROOF.** A lengthy verification. Most cases follow by inspection, the crux being that the unfolding preserves composition. $\square$

Hence, the main result of this paper follows by Lemma 3.3:

**COROLLARY 4.15.** *Consider $\Gamma \vdash M : A$ any IPA term. Then, $\mathcal{U}(\llbracket M \rrbracket)_{\text{PStrat}} = \llbracket M \rrbracket_{\text{Strat}}$.*

In other words, the strategy $\llbracket M \rrbracket_{\text{Strat}}$ obtained by induction on syntax following the methodology of denotational semantics, can also be extracted directly from running the multi-token machine $\llbracket M \rrbracket_{\text{PStrat}}$, and reading back the causal dependencies between events. From this also follows the adequacy of our multi-token GoI interpretation (Theorem 3.10). Indeed, for $\vdash M : \mathcal{U}$, then

$$ M \Downarrow \stackrel{(1)}{\Leftrightarrow} \llbracket M \rrbracket_{\text{Strat}} \Downarrow \stackrel{(2)}{\Leftrightarrow} \llbracket M \rrbracket_{\text{PStrat}} \Downarrow \stackrel{(3)}{\Leftrightarrow} \llbracket M \rrbracket_{\text{PStruct}} \Downarrow $$

where (1) is by Theorem 4.5, (2) is by Corollary 4.15 (it is immediate that $\llbracket M \rrbracket_{\text{PStrat}} \Downarrow \text{iff } \mathcal{U}(\llbracket M \rrbracket_{\text{PStrat}}) \Downarrow$) and for (3), by Lemma 3.3 and Proposition 4.10, $\llbracket M \rrbracket_{\text{PStrat}} = \llbracket M \rrbracket_{\text{PStruct}}$.

# 5 IMPLEMENTATION

We illustrate this with an interactive web application available here with some documentation here.
<figure><img src="image_37.png" /><figcaption>Fig. 29. Example of an optimization</figcaption></figure>

*Usage.* The interface lets the user enter a IPA program (or choose from a list of examples) and then displays the Petri structure. The user can then fire available transitions and see the tokens flow through the net and the visible causal run obtained via causal reconstruction appear on the left. The implementation also includes a *reverse mode* letting the user undo causally maximal events, not necessarily in the reverse order in which they were played – leveraging our *causal analysis* of runs.

*Optimisations.* Our translation, following the categorical semantics, tends to generate large Petri structures. To keep the nets at a reasonable size, we have implemented several optimisations. We first eliminate locations and transitions that are unreachable from a negative transition, or that never reach a positive transition. Such “dead code” can arise during composition. Moreover, when we have several transitions occurring in a simple sequence, we combine them into one by composing their transition functions and eliminate the intermediate transitions and locations. One example of such optimisation is represented in Figure 29, where we merge a and $b^0$ and remove the location $ℓ$. The new transition c has pre(c) = pre(a) and post(c) = post(a) \ {ℓ} ∪ post(c) and transition function: $δ⟨c⟩(α) = δ⟨a⟩(α) \setminus \{t\} \cup δ⟨b⟩(\{t\})$, where t denotes the tokil at $ℓ$ in $δ⟨a⟩(α)$.

There are minor inconsistencies between examples in the paper and the implementation as optimisation choices are not unique. In the paper, they are chosen so as to make transition functions more intuitive, which sometimes leads to different choices (compare e.g. Figure 12 with this).

# 6 CONCLUSION

Though this is a theoretical contribution, we believe it is worth exploring applications to the compilation and analysis of higher-order, concurrent, effectful programming.

Our translation confines the infinity to tokens (*data* and *exponential* signatures). Forgetting colours, we immediately obtain a finitary over-approximation of the behaviour of programs, a Petri net in the usual sense, that may be used to prove e.g. safety properties. This may be refined by handling colours symbolically or over-approximating them via abstract interpretation – perhaps offering a new truly concurrent basis for the static analysis of higher-order concurrent programs.

Though it is subtle semantically, IPA is of course hardly a realistic programming language. We do not foresee any fundamental obstacle in generalizing this approach: we expect that building a machine faithful to game semantics will let us leverage the impressive array of computational features that this semantic framework has been able to model.

# ACKNOWLEDGMENTS

We are grateful to Olivier Laurent for enlightening discussions on the Geometry of Interaction.

Work supported by the ANR project DyVerSe (ANR-19-CE48-0010-01); and by the Labex MiLyon (ANR-10-LABX-0070) of Université de Lyon, within the program “Investissements d’Avenir” (ANR-11-IDEX-0007), operated by the French National Research Agency (ANR).
REFERENCES

Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. 2000. Full Abstraction for PCF. Inf. Comput. 163, 2 (2000), 409–470. https://doi.org/10.1006/inco.2000.2930

John C. Baez and Jade Master. 2020. Open Petri nets. Math. Struct. Comput. Sci. 30, 3 (2020), 314–341.

Patrick Baillot. 1999. Approches dynamiques en sémantique de la logique linéaire: jeux et géométrie de l'interaction. Ph. D. Dissertation. Aix-Marseille 2.

Simon Castellan and Pierre Clairambault. 2020. Disentangling Parallelism and Interference in Game Semantics. (2020). https://arxiv.org/abs/2103.15453 Submitted.

Simon Castellan, Pierre Clairambault, Hugo Paquet, and Glynn Winskel. 2018. The concurrent game semantics of Probabilistic PCF. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, Anuj Dawar and Erich Grädel (Eds.). ACM, 215–224. https://doi.org/10.1145/3209108.3209187

Simon Castellan, Pierre Clairambault, Silvain Rideau, and Glynn Winskel. 2017. Games and Strategies as Event Structures. Logical Methods in Computer Science 13, 3 (2017). https://doi.org/10.23638/LMCS-13(3:35)2017

Simon Castellan, Pierre Clairambault, and Glynn Winskel. 2014a. Symmetry in concurrent games. In Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, Thomas A. Henzinger and Dale Miller (Eds.). ACM, 28:1–28:10. https://doi.org/10.1145/2603088.2603141

Simon Castellan, Pierre Clairambault, and Glynn Winskel. 2019. Thin Games with Symmetry and Concurrent Hyland-Ong Games. Log. Methods Comput. Sci. 15, 1 (2019). https://doi.org/10.23638/LMCS-15(1:18)2019

Simon Castellan, Jonathan Hayman, Marc Lasson, and Glynn Winskel. 2014b. Strategies as Concurrent Processes. In Proceedings of the 30th Conference on the Mathematical Foundations of Programming Semantics, MFPS 2014, Ithaca, NY, USA, June 12-15, 2014 (Electronic Notes in Theoretical Computer Science, Vol. 308), Bart Jacobs, Alexandra Silva, and Sam Staton (Eds.). Elsevier, 87–107. https://doi.org/10.1016/j.entsc.2014.10.006

Thomas Chatain and Eric Fabre. 2010. Factorization Properties of Symbolic Unfoldings of Colored Petri Nets. In Applications and Theory of Petri Nets, 31st International Conference, PETRI NETS 2010, Braga, Portugal, June 21-25, 2010. Proceedings (Lecture Notes in Computer Science, Vol. 6128), Johan Lilius and Wojciech Penczek (Eds.). Springer, 165–184. https://doi.org/10.1007/978-3-642-13675-7_11

Pierre Clairambault and Marc de Visme. 2020. Full abstraction for the quantum lambda-calculus. Proc. ACM Program. Lang. 4, POPL (2020), 63:1–63:28.

Ugo Dal Lago, Claudia Faggian, Ichiro Hasuo, and Akira Yoshimizu. 2014. The geometry of synchronization. In Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, Thomas A. Henzinger and Dale Miller (Eds.). ACM, 35:1–35:10. https://doi.org/10.1145/2603088.2603154

Ugo Dal Lago, Claudia Faggian, Benoît Valiron, and Akira Yoshimizu. 2015. Parallelism and Synchronization in an Infinitary Context. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015. IEEE Computer Society, 559–572. https://doi.org/10.1109/LICS.2015.58

Ugo Dal Lago, Claudia Faggian, Benoît Valiron, and Akira Yoshimizu. 2017. The geometry of parallelism: classical, probabilistic, and quantum effects. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 833–845. http://dl.acm.org/citation.cfm?id=3009859

Ugo Dal Lago, Ryo Tanaka, and Akira Yoshimizu. 2017. The geometry of concurrent interaction: Handling multiple ports by way of multiple tokens. In LICS. IEEE Computer Society, 1–12.

Vincent Danos, Hugo Herbelin, and Laurent Regnier. 1996. Game Semantics & Abstract Machines. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, July 27-30, 1996. IEEE Computer Society, 394–405. https://doi.org/10.1109/LICS.1996.561456

Vincent Danos and Laurent Regnier. 1996. Reversible, Irreversible and Optimal Lambda-machines. Electron. Notes Theor. Comput. Sci. 3 (1996), 40–60.

Thomas Ehrhard. 2012. The Scott model of linear logic is the extensional collapse of its relational model. Theor. Comput. Sci. 424 (2012), 20–45. https://doi.org/10.1016/j.tcs.2011.11.027

Dan R. Ghica and Andrzej S. Murawski. 2008. Angelic semantics of fine-grained concurrency. Ann. Pure Appl. Logic 151, 2-3 (2008), 89–114.

Dan R. Ghica and Nikos Tzevelekos. 2012. A System-Level Game Semantics. In Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics, MFPS 2012, Bath, UK, June 6-9, 2012 (Electronic Notes in Theoretical Computer Science, Vol. 286), Ulrich Berger and Michael W. Mislove (Eds.). Elsevier, 191–211. https://doi.org/10.1016/j.entsc.2012.08.013

Jean-Yves Girard. 1989. Geometry of interaction 1: Interpretation of System F. In Studies in Logic and the Foundations of Mathematics. Vol. 127. Elsevier, 221–260.
Jean-Yves Girard. 1995. Geometry of interaction III: accommodating the additives. London Mathematical Society Lecture Note Series (1995), 329-389.

Georges Gonthier, Martín Abadi, and Jean-Jacques Lévy. 1992. The Geometry of Optimal Lambda Reduction. In POPL. ACM Press, 15-26.

Ichiro Hasuo and Naohiko Hoshino. 2017. Semantics of higher-order quantum computation via geometry of interaction. Ann. Pure Appl. Log. 168, 2 (2017), 404-469. https://doi.org/10.1016/j.apal.2016.10.010

Jonathan Hayman. 2014. Interaction and Causality in Digital Signature Exchange Protocols. In Trustworthy Global Computing - 9th International Symposium, TGC 2014, Rome, Italy, September 5-6, 2014. Revised Selected Papers (Lecture Notes in Computer Science, Vol. 8902), Matteo Maffei and Emilio Tuosto (Eds.). Springer, 128-143. https://doi.org/10.1007/978-3-662-45917-1_9

Jonathan Hayman and Glynn Winskel. 2008. The unfolding of general Petri nets. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2008, December 9-11, 2008, Bangalore, India (LIPIcs, Vol. 2), Ramesh Hariharan, Madhavan Mukund, and V. Vinay (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 223-234. https://doi.org/10.4230/LIPIcs.FSTTCS.2008.1755

Naohiko Hoshino, Koko Muroya, and Ichiro Hasuo. 2014. Memoryful geometry of interaction: from coalgebraic components to algebraic effects. In Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14-18, 2014, Thomas A. Henzinger and Dale Miller (Eds.). ACM, 52:1-52:10. https://doi.org/10.1145/2603088.2603124

J. M. E. Hyland and C.-H. Luke Ong. 2000. On Full Abstraction for PCF: I, II, and III. Inf. Comput. 163, 2 (2000), 285-408. https://doi.org/10.1006/inco.2000.2917

Guilhem Jaber. 2015. Operational Nominal Game Semantics. In Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings (Lecture Notes in Computer Science, Vol. 9034), Andrew M. Pitts (Ed.). Springer, 264-278. https://doi.org/10.1007/978-3-662-46678-0_17

James Laird. 2007. A Fully Abstract Trace Semantics for General References. In ICALP (Lecture Notes in Computer Science, Vol. 4596). Springer, 667-679.

Olivier Laurent. 2001. A Token Machine for Full Geometry of Interaction. In Typed Lambda Calculi and Applications, 5th International Conference, TLCA 2001, Krakow, Poland, May 2-5, 2001, Proceedings (Lecture Notes in Computer Science, Vol. 2044), Samson Abramsky (Ed.). Springer, 283-297. https://doi.org/10.1007/3-540-45413-6_23

Paul Blain Levy and Sam Staton. 2014. Transition systems over games. In Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14-18, 2014, Thomas A. Henzinger and Dale Miller (Eds.). ACM, 64:1-64:10. https://doi.org/10.1145/2603088.2603150

Ian Mackie. 1995. The Geometry of Interaction Machine. In Conference Record of POPL'95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, USA, January 23-25, 1995, Ron K. Cytron and Peter Lee (Eds.). ACM Press, 198-208. https://doi.org/10.1145/199448.199483

Damiano Mazza. 2005. Multiport Interaction Nets and Concurrency. In CONCUR (Lecture Notes in Computer Science, Vol. 3653). Springer, 21-35.

Koko Muroya, Naohiko Hoshino, and Ichiro Hasuo. 2016. Memoryful geometry of interaction II: recursion and adequacy. In POPL. ACM, 748-760.

Mogens Nielsen, Gordon D. Plotkin, and Glynn Winskel. 1981. Petri Nets, Event Structures and Domains, Part I. Theor. Comput. Sci. 13 (1981), 85-108. https://doi.org/10.1016/0304-3975(81)90112-2

Mogens Nielsen and P. S. Thiagarajan. 2002. Regular Event Structures and Finite Petri Nets: The Conflict-Free Case. In Applications and Theory of Petri Nets 2002, 23rd International Conference, ICATPN 2002, Adelaide, Australia, June 24-30, 2002, Proceedings (Lecture Notes in Computer Science, Vol. 2360), Javier Esparza and Charles Lakos (Eds.). Springer, 335-351. https://doi.org/10.1007/3-540-48068-4_20

Gordon Stewart, Lennart Beringer, Santiago Cuellar, and Andrew W. Appel. 2015. Compositional CompCert. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, Sriram K. Rajamani and David Walker (Eds.). ACM, 275-287. https://doi.org/10.1145/2676726.2676985

Glynn Winskel. 1982. Event Structure Semantics for CCS and Related Languages. In Automata, Languages and Programming, 9th Colloquium, Aarhus, Denmark, July 12-16, 1982, Proceedings (Lecture Notes in Computer Science, Vol. 140), Mogens Nielsen and Erik Meineche Schmidt (Eds.). Springer, 561-576. https://doi.org/10.1007/BFb0012800

Glynn Winskel. 1986. Event Structures. In Advances in Petri Nets (Lecture Notes in Computer Science, Vol. 255). Springer, 325-392.
**Basic red. for PCF**

$$ (\lambda x^A. M) N \rightsquigarrow M[N/x] $$

$$ \text{if } b N_{\text{ft}} N_{\text{iff}} \rightsquigarrow N_b $$

$$ Y M \rightsquigarrow M (Y M) $$

$$ \text{let } x = v \text{ in } M \rightsquigarrow M[v/x] $$

$$ f(v_1, v_2) \rightsquigarrow v $$

$$ (\text{if } f(v_1, v_2) = v) $$

**Basic reductions for references and semaphores**

$$ \text{newref } x \text{ in } v \rightsquigarrow v $$

$$ \text{newsem } x \text{ in } v \rightsquigarrow v $$

**Stateful reductions**

$$ \langle!\ell, s \uplus \{\ell \mapsto n\}\rangle \rightsquigarrow \langle n, s \uplus \{\ell \mapsto n\} \rangle $$

$$ \langle\ell:=n, s \uplus \{\ell \mapsto \_\}\rangle \rightsquigarrow \langle \text{skip}, s \uplus \{\ell \mapsto n\} \rangle $$

$$ \langle \text{grab}(\ell), s \uplus \{\ell \mapsto 0\} \rangle \rightsquigarrow \langle \text{skip}, s \uplus \{\ell \mapsto 1\} \rangle $$

$$ \langle \text{rel}(\ell), s \uplus \{\ell \mapsto n\} \rangle \rightsquigarrow \langle \text{skip}, s \uplus \{\ell \mapsto 0\} \rangle \quad (n > 0) $$

**Stateless context rules**

$$ M \rightsquigarrow M' $$

$$ M \rightsquigarrow M' $$

$$ M \rightsquigarrow M' $$

$$ N \rightsquigarrow N' $$

$$ \frac{M N \rightsquigarrow M' N}{\text{if } M N_1 N_2 \rightsquigarrow \text{if } M' N_1 N_2} $$

$$ \frac{M' N_1 N_2 \rightsquigarrow M' N_1 N_2}{\text{if } M' N_1 N_2 \rightsquigarrow M' N_1 N_2} $$

$$ \frac{!M \rightsquigarrow !M'}{\text{if } !M \rightsquigarrow !M'} $$

$$ \frac{M \rightsquigarrow M'}{M:=N \rightsquigarrow M:=N'} $$

$$ M \rightsquigarrow M' $$

$$ M \rightsquigarrow M' $$

$$ M \rightsquigarrow M' $$

$$ \frac{\text{grab}(M) \rightsquigarrow \text{grab}(M')}{\text{rel}(M) \rightsquigarrow \text{rel}(M')} $$

$$ \frac{\text{rel}(M) \rightsquigarrow \text{rel}(M')}{\text{rel}(M) \rightsquigarrow \text{rel}(M')} $$

$$ \frac{M:=v \rightsquigarrow M':=v}{M:=v \rightsquigarrow M':=v} $$

$$ N \rightsquigarrow N' $$

$$ M_1 \rightsquigarrow M'_1 $$

$$ M_2 \rightsquigarrow M'_2 $$

$$ \frac{\text{let } x = N \text{ in } M \rightsquigarrow \text{let } x = N' \text{ in } M}{\text{let } x = N \text{ in } M \rightsquigarrow \text{let } x = N' \text{ in } M} $$

$$ \frac{f(M_1, M_2) \rightsquigarrow f(M'_1, M_2)}{f(M_1, M_2) \rightsquigarrow f(M'_1, M_2)} $$

$$ \frac{f(M_1, M_2) \rightsquigarrow f(M'_1, M_2)}{f(M_1, M_2) \rightsquigarrow f(M'_1, M_2)} $$

**Stateful context rules**

$$ \frac{\langle M[\ell/x], s \uplus \{\ell \mapsto n\} \rangle \rightsquigarrow \langle M'[\ell/x], s' \uplus \{\ell \mapsto n'\} \rangle}{\langle \text{newref } x:=n \text{ in } M, s \rangle \rightsquigarrow \langle \text{newref } x:=n' \text{ in } M', s' \rangle} \quad (\ell \in \mathcal{L} \text{ fresh}) $$

$$ \frac{\langle M[\ell/x], s \uplus \{\ell \mapsto n\} \rangle \rightsquigarrow \langle M'[\ell/x], s' \uplus \{\ell \mapsto n'\} \rangle}{\langle \text{newsem } x:=n \text{ in } M, s \rangle \rightsquigarrow \langle \text{newsem } x:=n' \text{ in } M', s' \rangle} \quad (\ell \in \mathcal{L} \text{ fresh}) $$

<caption>Fig. 30. Operational semantics of IPA</caption>

# A OPERATIONAL SEMANTICS

We include in Figure 30 the operational semantics of IPA. Here, $M \rightsquigarrow N$ stands for

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

i.e. all rules operate on configurations $\langle M, s \rangle$, but only the relevant part of the tuple is shown.

# B THE IPA-STRUCTURE PStruct

We gather here the missing pieces for the construction of the IPA-structure PStruct.

## B.1 PStruct as an IPA-structure: Constructions, Operations

Now, we introduce the IPA-structure operations for Petri structures, following Definition 3.1.

For PStruct we fix PStruct<sub>•</sub> = PStruct<sub>0</sub>: we do not need to distinguish well-opened objects.

### B.1.1 Constructions.
First of all, the constructions of Section 2.1 are applied to finite sets of addresses simply by applying the corresponding injections from Definition 2.1. In other words we set $M \otimes N = M + \otimes N$; $\&_{x \in V} M_x = \wp_{x \in V} \ell_k^x(M_x)$; $M \to N = M + \to N$ and $!M = M$.

For basic types, we set **U**, **B** and **N** as **G** = {$Q^-, A^+$}. We postpone **V** and **S** to Section B.3.

### B.1.2 Tensor.
The tensor is described in Section 2.2.4.

### B.1.3 Currying.
Rather than merely introducing currying, we introduce a general operation to rename the addresses associated with visible transitions in a Petri structure:

**Definition B.1.** Take $\sigma$ a Petri structure on $M$ and $f: M \to M$ s.t. $M \subseteq \text{dom}(f)$, $f(M) \subseteq N$.
The renaming $\sigma[f]$, a Petri structure on $N$, is as $\sigma$ except for $\partial_{\sigma[f]}(t) = f(\partial_{\sigma}(t))$.

The net itself is not affected, only the labelling function for visible transitions. Now:

*Definition B.2.* Consider $\sigma \in \text{PStruct}(!(&[\Gamma, x : A, \Delta]), O)$. We define the function $\Lambda_x : \mathcal{M}_\vdash \to \mathcal{M}_\vdash$ by $\Lambda_x(\kappa_m) = \kappa_\tau^x m$, $\Lambda_x(\ell_\sigma^x m) = \kappa_\tau^x \ell_\sigma m$, and $\Lambda_x(m) = m$ otherwise.

Then, setting $\Lambda_{x:A,O}^{\Gamma,\Delta}(\sigma) = \sigma[\Lambda_x]$, we obtain $\Lambda_{x:A,O}^{\Gamma,\Delta}(\sigma) \in \text{PStruct}(!(&[\Gamma, \Delta]), !A \to O)$.

This reassigns visible transitions corresponding to variable $x$ to the left hand side of $\to$ on the right hand side of $\vdash$. Transitions initially assigned to the right hand side must also be relabelled, but the rest are unchanged. The net itself (i.e. the graph) remains the same.

### B.1.4 Promotion. Promotion is described in Section 2.3.3.

## B.2 PStruct as an IPA-structure: Stateless Primitives

Next, we describe all the primitives involved in the interpretation of the $\lambda$-calculus and recursion.

### B.2.1 Variable, evaluation. First, the variable is simply a copycat set to component $i_\sigma^x$ of the context.

*Definition B.3.* Consider $M \subseteq \mathcal{M}$ finite, and $x \in \text{Var}$.

We define $\text{var}_{x:M}$ as $\mathcal{L}_{\text{var}_{x:M}} = \mathcal{L}_{\mathcal{C}_M}, \mathcal{T}_{\text{var}_{x:M}} = \mathcal{T}_{\mathcal{C}_M}$, with the same pre- and post-conditions as for $\mathcal{C}_M$. We set $\partial_{\text{var}_{x:M}}(m, \ell) = \ell_\tau^x m$ and $\partial_{\text{var}_{x:M}}(m, \tau) = \kappa_\tau^m$. Finally, the transition table is:

$$ 
\begin{align*}
\delta\langle(m^+, \tau)\rangle(\{(s, d)@m\}) &= (s, d) \\
\delta\langle(m^-, \ell)\rangle(\{(s, d)@m\}) &= (\diamond :: s, d) \\
\delta\langle(m^-, \tau)\rangle(s, d) &= \{(s, d)@m\} \\
\delta\langle(m^+, \ell)\rangle(\diamond :: s, d) &= \{(s, d)@m\}.
\end{align*}
$$

Recall that terms $\Gamma \vdash M : A$ are meant to be interpreted as morphisms $[[M]] \in \mathcal{C}(![\Gamma], [[A]])$. The ! explains the $\diamond$ in the transition table, which corresponds to *dereliction* in linear logic terminology.

Note that the top two of these transitions do not affect the token: they only forward it following the structure of the net. From now on, we call **trivial** such transitions and omit them for succinctness.

Evaluation, used for application, is also a copycat:

*Definition B.4.* For $M, N \subseteq \mathcal{M}$ finite sets, $\text{ev}_{M,N} = \mathcal{C}_{M \to N}[\Omega]$, where $\Omega : \mathcal{M} \to \mathcal{M}$ is $\Omega(\kappa_\tau^x m) = \kappa_\tau^m$, $\Omega(\kappa_\tau^x \ell_\sigma^x m) = \ell_\tau^x \kappa_\tau^x m$, $\Omega(\ell_\sigma^x \kappa_\tau^x m) = \ell_\tau^x \ell_\sigma^x \kappa_\tau^x m$, $\Omega(\ell_\sigma^x \ell_\sigma^x m) = \ell_\sigma^x \ell_\sigma^x \ell_\sigma^x m$, and $\Omega(m) = m$ otherwise.

### B.2.2 Other stateless primitives. For finite $M \subseteq \mathcal{M}$, the (binary) contraction $c_M$ was presented in Section 2.3.2. The $n$-ary contraction, defined likewise, is omitted – it may also be obtained by induction, composing binary contractions.

The fixpoint combinator $Y_M$ is similar: it has $\mathcal{L}_{Y_M} = M, \mathcal{T}_{Y_M} = (M + \neg M) + M$, net in Figure 32a and transition rules in Figure 31. The net has no loops, but loops may arise by composition.

**Operations** were described in Section 3.3.1. **Constants, conditionals** are introduced in Figures 32b, 32c respectively, with transition rules in Figure 31. Hopefully their behaviour is clear at this point. Finally, the **let** was introduced in Section 3.3.3.

## B.3 PStruct as an IPA-structure: Stateful Primitives

For types $\mathcal{V}$ and $\mathcal{S}$ we have addresses $\mathcal{V} = \{w_\mathcal{V}Q^-, w_\mathcal{V}A^+, \kappa_\mathcal{V}Q^-, \kappa_\mathcal{V}A^+\}$ and $\mathcal{S} = \{g_\mathcal{S}Q^-, g_\mathcal{S}A^+, \kappa_\mathcal{S}Q^-, \kappa_\mathcal{S}A^+\}$, where $w_\mathcal{V}$ is the address for write requests, $\kappa_\mathcal{V}$ for read requests, $g_\mathcal{S}$ for grab, $\kappa_\mathcal{S}$ for release.
$$
\begin{align*}
\delta_{\text{if}} \langle \ell_c, \ell_s, \ell_q Q^+ \rangle (\{([], \mathfrak{t})^{@2}\}) &= ([], \bullet) \\
\delta_{\text{if}} \langle \ell_c, \ell_s, \ell_q Q^+ \rangle (\{([], \mathfrak{f})^{@2}\}) &= ([], \bullet) \\
\delta_{Y_M} \langle \kappa_c m^- \rangle (s, d) &= \{(\ell \diamond :: s, d)@m^-\} \\
\delta_{Y_M} \langle \ell_c, \ell_s m^- \rangle (e_1 :: e_2 :: s, d) &= \{(\kappa_c \langle e_1, e_2 \rangle :: s, d)@m^-\} \\
\delta_{Y_M} \langle \kappa_c m^+ \rangle (\{(\ell \diamond :: s, d)@m^+\}) &= (s, d) \\
\delta_{Y_M} \langle \ell_c, \ell_s m^+ \rangle (\{(\kappa_c \langle e_1, e_2 \rangle :: s, d)@m^+\}) &= (e_1 :: e_2 :: s, d) \\
\delta_{\text{newsem}} \langle \kappa_c Q^- \rangle ([, \bullet]) &= \{([], \bullet)^{@1}, ([], \mathfrak{t})^{@2}\} \\
\delta_{\text{newsem}} \langle g \rangle (\{([e], \bullet)^{@3}, (\mathfrak{t})^{@2}\}) &= \{([e], \mathfrak{f})^{@2}, ([e], \check{\mathfrak{t}})^{@4}\} \\
\delta_{\text{newsem}} \langle r \rangle (\{([e], \bullet)^{@3}, (\mathfrak{f})^{@2}\}) &= \{([e], \mathfrak{t})^{@2}, ([e], \check{\mathfrak{t}})^{@6}\}
\end{align*}
$$

<figure><img src="image_38.png" /><figcaption>Fig. 32. The nets of Petri structures for IPA primitives</figcaption></figure>

B.3.1 Reference and semaphore queries. Recall that Definition 3.1 requires primitives

$$
\begin{align*}
\mathit{assign} &\in \mathcal{C}(\mathbf{V} \otimes \mathbf{N}, \mathbf{U}), & \mathit{deref} &\in \mathcal{C}(\mathbf{V}, \mathbf{N}) \\
\mathit{grab} &\in \mathcal{C}(\mathbf{S}, \mathbf{U}), & \mathit{release} &\in \mathcal{C}(\mathbf{S}, \mathbf{U})
\end{align*}
$$

for reference and semaphore queries. Among these, we set **deref** = $\alpha_N [\ell_c m \mapsto \ell_c \kappa_c m, \kappa_c m \mapsto \kappa_c m]$, **grab** = $\alpha_U [\ell_c m \mapsto \ell_c g_\beta m, \kappa_c m \mapsto \kappa_c m]$ and **release** = $\alpha_U [\ell_c m \mapsto \ell_c \kappa_c m, \kappa_c m \mapsto \kappa_c m]$ copycat strategies simply accessing the matching component of the reference or semaphore.

The remaining query **assign** is more elaborate: upon being evaluated, it sends an evaluation
request to its integer argument. Upon receiving a value, it sends the write request, and propagates
the acknowledgement. The net is in Figure 32d and its transition rules are trivial.

B.3.2 Initialization. The actual stateful behaviour is provided by nets for new references and semaphores newref ∈ C (!V → X, X) and newsem ∈ C (!S → X, X). New references were introduced in Section 3.3.2. The (identical) net for new semaphores appears in Figure 32e with non-trivial transitions in Figure 31.
<figure><img src="image_39.png" /><figcaption>Fig. 33. Interpretation of IPA ground types</figcaption></figure>

For new semaphores, in normal operation, location 2 contains exactly one token with data either t or ff, encoding if the semaphore is free. The transitions g and r grab and release the semaphore, and may only fire if the semaphore currently has the adequate state.

## C CONCURRENT STRATEGIES

We now provide details about the construction of the IPA structure of concurrent strategies as presented in [Castellan and Clairambault 2020].

### C.1 Types and Contexts as Games

We detail the interpretation of types. Figure 33 presents the interpretation of ground types.

We now move on to constructions on games and arenas. We write either 1 or ⊤ for the empty arena. If (m, s, d) ∈ Moves, we write $ℓ_◦((m, s, d)) = (ℓ_◦(m), s, d)$ and likewise for all injections appearing in the definition of addresses. This extends to sets of moves by direct image. Address injections also apply to binary relations on moves in the obvious way, e.g. $ℓ_◦(R) = \{(ℓ_◦(m), ℓ_◦(m')) | m R m'\}$.

**Definition C.1.** Consider A, B games. Then we set games $A \otimes B$ and $A \vdash B$ with components:

$$ 
\begin{align*}
|A \otimes B| &= \ell_\circ(|A|) \uplus \tau_\circ(|B|) \\
\le_{A \otimes B} &= \ell_\circ(\le_A) \uplus \tau'_\circ(\le_B) \\
\#_{A \otimes B} &= \ell_\circ(\#A) \uplus \tau_\circ(\#B)
\end{align*}
$$

$$ 
\begin{align*}
|A \vdash B| &= \ell_\tau(|A|) \uplus \tau'_\tau(|B|) \\
\le_{A \vdash B} &= \ell_\tau(\le_A) \uplus \tau'_\tau(\le_B) \\
\#_{A \vdash B} &= \ell_\tau(\#A) \uplus \tau'_\tau(\#B)
\end{align*}
$$

$A \otimes B$ is called the **tensor**, and $A \vdash B$ is called the **hom-game**.

If A, B are arenas, so is $A \otimes B$. In contrast, $A \vdash B$ is never an arena unless A is empty. Formally, both constructions are defined in the same way, but with a distinct injection – remember that $ℓ_τ$ inverts polarity, so that in $A \vdash B$ the polarity is inverted in A.

From the definition, configurations of $A \otimes B$ have a restricted shape: any $x \in \mathscr{C}(A \otimes B)$ decomposes uniquely as $x = \ell_\circ(x_A) \uplus \tau_\circ(x_B)$ with $x_A \in \mathscr{C}(A)$ and $x_B \in \mathscr{C}(B)$ – we write $x = x_A \otimes x_B$. Likewise, any configuration $x \in \mathscr{C}(A \vdash B)$ decomposes as $x = x_A \vdash x_B = \ell_\tau(x_A) \uplus \tau'_\tau(x_B)$.

#### C.1.1 Further arena constructions.
We give the remaining constructions required by Definition 3.1.

First a new notation: for $m = (m, s, d) \in \text{Moves}$ and $e \in \mathcal{E}$, we write $e :: m = (m, e :: s, d)$, i.e. the exponential signature implicitly applies to the exponential stack of $m$. This is an injection, and accordingly we apply it to sets and relations as with the injections from addresses.

**Definition C.2.** We define three other constructions on arenas:

*linear arrow*: for A, O arenas with O well-opened, we define $A \dashrightarrow O$ well-opened in Figure 34a.

*product*: for $(A_x)_{x \in V}$ a family of arenas with $V \subseteq \text{Var}$, we define $\mathcal{A}_{x \in V} A_x$ in Figure 34b.

*bang*: for A an arena, we define !A in Figure 34c.
$$
\begin{align*}
|A \to O| &= \ell_{\to}(|A|) \triangleright \tau_{\to}(|O|) \\
\le_{A \to O} &= \ell_{\to} (\le_{A}) \triangleright \tau_{\to} (\le_{O}) \\
&\quad \triangleright \tau_{\to} (\min(O)) \times \ell_{\to}(|A|) \\
\#_{A \to O} &= \ell_{\to} (#_A) \triangleright \tau_{\to} (#_O)
\end{align*}
$$

(a) Arrow

$$
\begin{align*}
| \& (A_x)_{x \in V} | &= | \triangleright_{x \in V} \dot{t}_k^x (|A_x|) \\
\le_{\& (A_x)_{x \in V}} &= | \triangleright_{x \in V} \dot{t}_k^x (\le_{A_x}) \\
\dot{t}_k^x (a) \# \dot{t}_k^y (a') &\Leftrightarrow (x = y \land a \#_{A_x} a') \\
&\quad \lor (x \neq y)
\end{align*}
$$

(b) Product

$$
\begin{align*}
|!A| &= |\triangleright_{e \in \mathcal{E}} e \:::: |A| \\
\le_{!A} &= |\triangleright_{e \in \mathcal{E}} e \:::: (\le_{A}) \\
\#_{!A} &= |\triangleright_{e \in \mathcal{E}} e \:::: (#_{A})
\end{align*}
$$

(c) Bang

<figure><img src="image_40.png" /><figcaption>Fig. 35. Arenas for references and semaphores</figcaption></figure>

<figure><img src="image_41.png" /><figcaption>Fig. 36. Arena !($U \to \bar{U}$) $\to \mathbb{B}$</figcaption></figure>

<figure><img src="image_42.png" /><figcaption>Fig. 37. Part of a concurrent strategy</figcaption></figure>

It remains to give the arenas for references and semaphores, in Figure 35.

The arrow $A \to O$ enforces that an argument cannot be called before the function has been called. The bang !A creates countably many independent copies of A, one for each exponential signature, for *thread indexing* (for that, [Castellan and Clairambault 2020] uses *integers*).

A more elaborate example of arena is in Figure 36. The representation is symbolic: from the exponentials in the construction, the full arena is infinite and comprises moves as in the diagram for all exponential signatures $e, e' \in \mathcal{E}$. However, we have e.g. $(\ell_{\to} \tau_{\to} Q, [e], \bullet) \le (\ell_{\to} \ell_{\to} Q, [e_1, e_2], \bullet)$ only when $e = e_1$ – in an exponential stack, the first element corresponds to the outermost !($-$).

## C.2 The Category of Arenas and Strategies

Events of a strategy $\sigma$ inherit a polarity from $\text{pol}_\sigma(s) = \text{pol}(\partial(s))$ – a definition used implicitly from now on. Again, this definition is as in [Castellan and Clairambault 2020] without the component and conditions – unnecessary for this paper – pertaining to symmetry.

The event structure $\sigma$ presents observable computational events along with their causal dependencies and conflicts. Events of $\sigma$ are *not* moves of the game, but they do correspond to moves via the action of $\partial$. This permits an explicit representation of non-deterministic branching: several events of $\sigma$ may correspond to the same move if they are conflicting and so belong to separate branches of the execution. The strategy keeps them separate, even if they cannot be distinguished.

We show in Figure 37 (part of) a concurrent strategy playing on the game in Figure 36. In such diagrams we represent the strategy and the explored part of the arena in a single picture. Nodes correspond to events of the strategy, drawn directly as their display through $\partial$ – this means that two conflicting nodes may have the same label, as happens in Figure 37. Arrows $\to$ correspond to the immediate causal dependency in $\sigma$, while dotted lines correspond as before to the causal dependency from the game. The diagram in Figure 37 is a part of the strategy for:
*Example C.3.* We introduce the term $\vdash$ **strictness**: $(\mathbb{U} \to \mathbb{U}) \to \mathbb{B}$, defined as

$$ \vdash \lambda f^{\mathbb{U} \to \mathbb{U}}. \text{newref } x \text{ in } f (x := 1); \text{ not (iszero !}x\text{)} $$

$$ : (\mathbb{U} \to \mathbb{U}) \to \mathbb{B}, $$

using encapsulated state to test if a function $f$ calls its argument (run it here).

Figure 37 reads as follows: Opponent initiates computation with $(x_\sigma Q, [] , \bullet)^-$. This lets Player call his argument with $(\ell_\sigma x_\sigma Q, [\diamond], \bullet)^+$. This lets Opponent return the call with $(\ell_\sigma x_\sigma A, [\diamond], \checkmark)^-$, or call its argument with $(\ell_\sigma \ell_\sigma Q, [\diamond, e])^-$ for any $e \in \mathcal{E}$ (in fact Opponent may call this argument arbitrarily many times with distinct exponential signatures, but Figure 37 only represents one call). But these events are not incompatible: though this behaviour is not realizable within IPA, our model lets Opponent call its argument *and* return *concurrently!* In that case both $x := 1$ and $!x$ are running, so there is a *race*. The conflicts in Figure 37 allow two outcomes, depending on who wins.

It remains to introduce the two conditions *courteous* and *receptive*: the former simply states that a strategy has no control over Opponent moves, and must acknowledge each Opponent move A uniquely. *Courtesy* entails that with respect to the immediate causal links of the game, a strategy can only add new dependencies from negative to positive moves. This formalizes the idea that strategies interact in an *asynchronous* environment, where e.g. causal links between positive moves may not be preserved by propagation of moves through buffers – or through a Petri structure.

### C.2.1 Isomorphic strategies.
Strict equality of strategies is too strict to be useful; instead we use:

*Definition C.4.* Consider $\sigma, \tau$: A two (pre)strategies on game A.

An **isomorphism** $\varphi: \sigma \cong \tau$ is an invertible map of es $\varphi: \sigma \to \tau$ such that $\partial_\tau \circ \varphi = \partial_\sigma$.

We write $\sigma \cong \tau$ to mean that $\sigma$ and $\tau$ are isomorphic, leaving the isomorphism unspecified. Clearly, this is an equivalence relation. It is a basic fact from the theory of event structures that isomorphisms between $\sigma$ and $\tau$ are in one-to-one correspondence with order-isos $\varphi: \mathcal{C}(\sigma) \cong \mathcal{C}(\tau)$ such that $\partial_\tau \circ \varphi = \partial_\sigma$, i.e. any such order-iso is given by a unique isomorphism of strategies – this is convenient as it is often easier to construct a bijection between configurations rather than events.

For strategies, this can be simplified by ignoring trailing Opponent moves. A $x \in \mathcal{C}(\sigma)$ is **+covered** if any $m \in x$ maximal in $x$ is positive; we write $\mathcal{C}^+(\sigma)$ for the **+covered** configurations of $\sigma$. The action of an iso $\varphi$ on **+covered** configurations suffices to completely describe it:

**LEMMA C.5.** Consider $\sigma, \tau$: A two strategies, and $\varphi: \mathcal{C}^+(\sigma) \cong \mathcal{C}^+(\tau)$ an order-iso s.t. $\partial_\tau \circ \varphi = \partial_\sigma$.

Then, there is a unique $\hat{\varphi}: \sigma \cong \tau$ such that $\hat{\varphi}(x) = \varphi(x)$ for all $x \in \mathcal{C}^+(\sigma)$.

This is an application in the trivial case without symmetry of Lemma 5.11 from [Castellan and Clairambault 2020], which will be very helpful in constructing isomorphisms in this paper.

### C.2.2 Composition.
Working towards an IPA-structure, we must first define composition.

A strategy $\sigma$ **from game A** to **game B** is defined as a strategy $\sigma: A \vdash B$. Let us fix for now games A, B and C and strategies $\sigma: A \vdash B$ and $\tau: B \vdash C$ that we wish to compose to $\tau \odot \sigma: A \vdash C$.

Lemma C.5 puts the emphasis on **+covered** configurations, so we investigate what should be the **+covered** configurations of $\tau \odot \sigma$. It turns out that they correspond to pairs $x^\sigma \in \mathcal{C}^+(\sigma)$ and $x^\tau \in \mathcal{C}^+(\tau)$ whose synchronization of $x^\sigma$ and $x^\tau$ through B is “sound”, which we must now define.

We fix the convention that if $x^\sigma \in \mathcal{C}(\sigma)$ and $x^\tau \in \mathcal{C}(\tau)$, we write $\partial_\sigma x^\sigma = x_A^\sigma \vdash x_B^\sigma$ and $\partial_\tau x^\tau = x_B^\tau \vdash x_C^\tau$ where $x_A^\sigma \in \mathcal{C}(A)$, $x_B^\sigma \in \mathcal{C}(B)$, and $x_C^\tau \in \mathcal{C}(C)$. We say $x^\sigma \in \mathcal{C}(\sigma)$ and $x^\tau \in \mathcal{C}(\tau)$ are **matching** if $x_B^\sigma = x_B^\tau$, in which case it is unambiguous to write $\partial_\sigma(x^\sigma) = x_A \vdash x_B$ and $\partial_\tau(x^\tau) = x_B \vdash x_C$. So $x^\sigma$ and $x^\tau$ reach the same state on B, but it remains to see if they do it
<figure><img src="image_43.png" /><figcaption>Fig. 38. Matching, secured configurations</figcaption></figure>

<figure><img src="image_44.png" /><figcaption>Fig. 40. Example of a composition</figcaption></figure>

with compatible causal constraints. For that, we set $x_A \parallel x_B \parallel x_C = l(x_A) \uplus m(x_B) \uplus r(x_C)$, and

$$ \begin{array}{l} \partial_{\sigma}^{l}: x^{\sigma} \rightarrow x_{A} \parallel x_{B} \parallel x_{C} \\ m \mapsto l(a) \quad \text{if } \partial_{\sigma}(m) = l(a), \\ m \mapsto m(b) \quad \text{if } \partial_{\sigma}(m) = r(b), \end{array} $$

$$ \begin{array}{l} \partial_{\tau}^{r}: x^{\tau} \rightarrow x_{A} \parallel x_{B} \parallel x_{C} \\ n \mapsto m(b) \quad \text{if } \partial_{\tau}(n) = l(b), \\ n \mapsto r(c) \quad \text{if } \partial_{\tau}(n) = r(c). \end{array} $$

are variants of the display maps set to embed $x^{\sigma}$ and $x^{\tau}$ in the common space $x_A \parallel x_B \parallel x_C$.

This lets us check the presence of deadlocks by importing all causal constraints to $x_A \parallel x_B \parallel x_C$:

**Definition C.6.** Consider $x^{\sigma} \in \mathscr{C}(\sigma)$ and $x^{\tau} \in \mathscr{C}(\tau)$ matching configurations.

They are **causally compatible** if the relation $\triangleleft = \triangleleft_{\sigma} \uplus \triangleleft_{\tau}$ on $x_A \parallel x_B \parallel x_C$ set with:

$$ \begin{array}{ll} \partial_{\sigma}^{l}(m) & \triangleleft_{\sigma} \partial_{\sigma}^{l}(m') \quad \text{for } m <_{\sigma} m' \\ \partial_{\tau}^{r}(n) & \triangleleft_{\tau} \partial_{\tau}^{r}(n') \quad \text{for } n <_{\tau} n' \end{array} $$

is acyclic. We also say that the pair $x^{\sigma}, x^{\tau}$ is **secured**.

We show in Figures 38 and 39 examples of matching secured and non-secured pairs involved in computing the composition of the strategy of Figure 37 with $\lambda x^{\mathcal{U}}$. $x$. In Figure 39, a deadlock directly arises from opposite causal constraints (highlighted in blue). This entails that the only result arising from this composition will be $\mathcal{t}$ from Figure 38, as expected since $\lambda x$. $x$ is strict.

Then $\tau \odot \sigma$ is the *unique* strategy with as $+\text{-covered}$ configurations the *causally compatible* pairs:

**PROPOSITION C.7.** Consider A, B, C games, and $\sigma: A \vdash B$ and $\tau: B \vdash C$ strategies.

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

$$ \begin{array}{l} (- \odot -) : \{(x^{\tau}, x^{\sigma}) \in \mathscr{C}^{+}(\tau) \times \mathscr{C}^{+}(\sigma) | \text{causally compatible}\} \\ \approx \qquad \mathscr{C}^{+}(\tau \odot \sigma) \end{array} $$

such that for any $x^{\sigma} \in \mathscr{C}^{+}(\sigma)$ and $x^{\tau} \in \mathscr{C}^{+}(\tau)$ *causally compatible*, $\partial_{\tau \odot \sigma}(x^{\tau} \odot x^{\sigma}) = x_{A}^{\sigma} \vdash x_{C}^{\tau}$.

This is a simplification of Proposition 3.3.1 from [Castellan and Clairambault 2020].

Concretely, composition is performed by parallel interaction (via the synchronizing product of es used by Winskel to model CCS [Winskel 1982]); followed by *hiding* which keeps the visible events only. In this paper, the above characterization suffices for our purposes.
Figure 40 shows an example composition which, ignoring exponentials, corresponds to:

$$[f : \mathbb{B} \to \mathbb{U} \vdash f \text{ coin}] \circ [\vdash \lambda x^{\mathbb{B}}. \text{ if } x \text{ skip skip}] : 1 \vdash \mathbb{U}.$$

Observe the resulting strategy has two distinct ways to converge, even though the two occurrences of $(r'_A, []$, $\check{+}$) correspond to the same event of the left hand side strategy. Each event of the composition carries its whole causal history, including the exact synchronizations that lead to it.

### C.3 The IPA-structure Strat

**C.3.1 Categorical structure.** Section C.2 already contains the data of Strat, and composition. It remains to define:

**Copycat.** Copycat may be defined on any game, but it is slightly simpler on arenas:

**Definition C.8.** For each arena A, the **copycat strategy** $\omega_A : A \vdash A$ is defined as having:

$$ \begin{align*} |\omega_A| &= |A \vdash A| \\ \partial_{\omega_A}(m) &= m \\ i(a) \le_{\omega_A} i'(a) &\Leftrightarrow \begin{array}{@{}l@{}} a <_A a'; \text{ or } a = a', \text{ pol}(i(a)) = - \\ \text{and } \text{pol}(i'(a)) = + \end{array} \\ i(a) \#_{\omega_A} i'(a') &\Leftrightarrow a \#_A a' \end{align*} $$

where $i, i' \in \{\ell, r'\}$.

Copycat acts as an asynchronous forwarder, simply receptive to all Opponent moves and prepared to forward them to the other side as soon as they become available. This means that its $+-$covered configurations, where all moves have been successfully forwarded, have a particularly simple shape:

**LEMMA C.9.** *Consider A any arena. Then, we have $\mathcal{C}^+(\omega_A) = \{x_A \vdash x_A \in \mathcal{C}(A \vdash A) \mid x_A \in \mathcal{C}(A)\}$.*

From Lemma C.5 this characterizes $\omega_A$ uniquely up to iso, just like Proposition C.7 for composition. It follows from these two facts that composition preserves isomorphisms, that it is associative and that identities are neutral for composition up to isomorphism, see [Castellan et al. 2017] for details.

**COROLLARY C.10.** *There is Strat, a category having arenas as objects, as morphisms from A to B the negative strategies on the game $A \vdash B$ up to isomorphism, and copycat strategies as identities.*

Unlike PStruct or PStrat, Strat is a category satisfying the identity laws – though this fact will not be directly useful for us in this paper.

**C.3.2 Strat as an IPA-structure: Operations.** We detail the different operations involved in the IPA-structure.

**Tensor.** Fix $\sigma_1 \in \text{Strat}(A_1, B_1)$ and $\sigma_2 \in \text{Strat}(A_2, B_2)$. We define:

**Definition C.11.** We define $\sigma_1 \otimes \sigma_2 \in \text{Strat}(A_1 \otimes A_2, B_1 \otimes B_2)$ with:

$$ \begin{align*} |\sigma_1 \otimes \sigma_2| &= |\sigma_1| + |\sigma_2| \\ &\le \sigma_1 \otimes \sigma_2 = \le \sigma_1 + \le \sigma_2 \\ &\# \sigma_1 \otimes \sigma_2 = \# \sigma_1 + \# \sigma_2 \\ \partial_{\sigma_1 \otimes \sigma_2}(\ell(m)) &= \partial_{\sigma_1}(m) \\ \partial_{\sigma_1 \otimes \sigma_2}(r(m)) &= \partial_{\sigma_2}(m) \end{align*} $$

The conditions for a strategy are straightforward, and so is:
**PROPOSITION C.12.** The strategy $\sigma_1 \otimes \sigma_2 \in \text{Strat}(A_1 \otimes A_2, B_1 \otimes B_2)$ satisfies:

$$ ( - \otimes - ) : \mathcal{C}^{+}(\sigma_1) \times \mathcal{C}^{+}(\sigma_2) \to \mathcal{C}^{+}(\sigma_1 \otimes \sigma_2) $$

such that $\partial_{\sigma_1 \otimes \sigma_2}(x^{\sigma_1} \otimes x^{\sigma_2}) = (x_{A_1}^{\sigma_1} \otimes x_{A_2}^{\sigma_2}) \vdash (x_{B_1}^{\sigma_1} \otimes x_{B_2}^{\sigma_2})$ for all $x^{\sigma_1} \otimes x^{\sigma_2} \in \mathcal{C}^{+}(\sigma_1 \otimes \sigma_2)$.

Moreover, $\sigma_1 \otimes \sigma_2$ is the unique strategy on $A_1 \otimes A_2 \vdash B_1 \otimes B_2$ satisfying this property.

**PROOF.** The property is a direct verification, and uniqueness follows from Lemma C.5. □

*Currying.* As for Petri structures, we start with renaming.

**Definition C.13.** Consider $\sigma$ a strategy on game A, and $f : |A| \to |B|$.

Then, we define the **renaming** to be as $\sigma$ except $\partial_{\sigma[f]}(m) = f(\partial_{\sigma}(m))$.

Without additional conditions, there is no reason why $\sigma[f]$ would be a strategy in general. A convenient situation is when $f$ preserves sufficiently rigidly the rules of the game:

**PROPOSITION C.14.** We say that $f : |A| \to |B|$ is **valid** if it is a map of es, additionally satisfying hypotheses receptive and courteous from Definition 4.4

If $\sigma : A$ and $f$ is valid, then $\sigma[f]$ is a strategy on B.

**PROOF.** Straightforward. □

However, we cannot use this directly for currying, because the function

$$ \Lambda_{x:A,O}^{\Gamma,\Delta} : \begin{array}{rcl} |! & \& & [\Gamma, x : A, \Delta] \vdash O| & \to & |! & \& & [\Gamma, \Delta] \vdash !A \to O| \\ (m, s, d) & \mapsto & (\Lambda^x(m), s, d) \end{array} $$

using $\Lambda_x$ from Definition B.2, is not valid (a singleton configuration in A on the left hand side is indeed sent to a non-configuration on the right hand side). However, we do have:

**PROPOSITION C.15.** Consider $\sigma \in \text{Strat}(! & [\Gamma, x : A, \Delta], O)$.

Then, there exists a unique $\Lambda(\sigma) \in \text{Strat}(! & [\Gamma, x : A, \Delta] \vdash O)$ such that

$$ \varphi : \mathcal{C}^{+}(\sigma) \cong \mathcal{C}^{+}(\Lambda(\sigma)) $$

and satisfying that $\partial_{\Lambda(\sigma)}(\varphi(x^{\sigma})) = \Lambda_{x:A,O}^{\Gamma,\Delta}(\partial_{\sigma}(x^{\sigma}))$ for all $x^{\sigma} \in \mathcal{C}^{+}(\sigma)$.

**PROOF.** Existence. We set $\Lambda(\sigma)$ as $\sigma[\Lambda_{x:A,O}^{\Gamma,\Delta}]$ even though $\Lambda_{x:A,O}^{\Gamma,\Delta}$ is not valid; that this is still well-defined follows directly from $\sigma$ negative (see [Castellan and Clairambault 2020, Lemma 4.25]).

*Uniqueness.* Direct from Lemma C.5. □

*Promotion.* Next we define the promotion of $\sigma \in \text{Strat}(!A, B)$.

First, for any arena A, we define the function

$$ \begin{array}{rcl} \text{dig}_A & : & !A \to !A \\ e_1 :: (e_2 :: m) & \mapsto & \langle e_1, e_2 \rangle :: m \end{array} $$

yielding a map of event structures. If $\sigma$ is a strategy, we write $\mathcal{C}^{+,\neq 0}(\sigma)$ the set of $+\text{-covered}$, non-empty configurations of $\sigma$. Finally, for $X$ a set we write $\text{Fam}(X)$ for the set of families $(x_i)_{i \in I}$ where $x_i \in X$ and $I \subseteq \mathcal{E}$ is a finite subset of exponential signatures.

With these notations in place, we have:

**PROPOSITION C.16.** There is a strategy $\sigma^\dagger \in \text{Strat}(!A, !B)$, unique up to iso, such that there is

$$ [-] : \text{Fam}(\mathcal{C}^{+,\neq 0}(\sigma)) \cong \mathcal{C}^{+}(\sigma^\dagger) $$
satisfying that for all $(x^e)_{e \in E} \in \text{Fam}(\mathscr{C}^{+, \neq \emptyset}(\sigma))$, we have

$$ \partial_{\sigma^i}(([(x^e)_{e \in E}]) = \text{dig}\left(\left(\bigcup_{e \in E} e :: x_{1A}^e\right) \cup \left(\bigcup_{e \in E} e :: x_B^e\right)\right) $$

writing $\partial_{\sigma}(x^e) = x_{1A}^e \cup x_B^e$ for all $e \in E$.

**PROOF. Existence.** Straightforward from [Castellan and Clairambault 2020, Definition 4.27] and renaming following dig.

*Uniqueness.* Direct from Lemma C.5. □

### C.3.3 Strat as an IPA-Structure: Primitives.

*Copycat strategies.* We first address the three primitives arising as copycat-like strategies: variable, evaluation, and contraction.

**Definition C.17.** Consider $\Gamma, x : A, \Delta$ a semantic context. Then we set $\text{Var}_{x:A}^{\Gamma, \Delta}$ as $\omega_A[\text{Var}_x]$ where

$$ \begin{array}{rcl} \text{Var}_x : & (A \vdash A) & \to (\!\&\![\Gamma, x : A, \Delta] \vdash A) \\ & (\tau^i m, s, d) & \mapsto (\tau^i m, s, d) \\ & (\ell^i m, s, d) & \mapsto (\ell^i \tau^x_\delta m, \diamond :: s, d) \end{array} $$

Likewise, the evaluation morphism is simply by renaming.

**Definition C.18.** Consider $A, O$ arenas with $O$ well-opened.

Then we set $\text{ev}_{A,O} = \omega_{A \to O}[\Omega]$ where $\Omega$ is that of Definition B.4 canonically extended to moves.

Finally, we define copycat. As in the main text, for simplicity we give the binary case.

**Definition C.19.** Consider $A$ an arena. Then we set $c_A = \omega_{A \otimes !A}[c] \in \text{Strat}(!A, !A \otimes !A)$ where

$$ \begin{array}{rcl} c : & (!A \otimes !A \vdash !A \otimes !A) & \to (!A \vdash !A \otimes !A) \\ & (\ell^i \ell_\delta^\otimes m, e :: s, d) & \mapsto (\ell^i m, (\ell^i e) :: s, d) \\ & (\ell^i \tau^x_\delta m, e :: s, d) & \mapsto (\ell^i m, (\tau^i e) :: s, d) \\ & (\tau^i m, s, d) & \mapsto (\tau^i m, s, d) \end{array} $$

For the unfolding, it will be convenient to have the following characterization:

**PROPOSITION C.20.** For any arena $A$, $\mathscr{C}^+(c_A) = \{\ell_i(x_{1A}) \uplus \tau^i(y_{1A}) \vdash x_{1A} \otimes y_{1A} \mid x_{1A}, y_{1A} \in \mathscr{C}(!A)\}$.

**PROOF.** Immediate by Lemma C.9 and definition. □

*Constants, conditional, queries.* The strategies are displayed in Figure 41. Note that some of these diagrams use a symbolic representation; whenever there is a branch starting with a negative move with some data, there actually is a branch for any instance of the data allowed in the game.

*Let.* We illustrate the strategy *let* in Figure 42. Note that there is a similar call to !X for all exponential signature $e \in \mathcal{E}$.

*Recursion.* In [Castellan and Clairambault 2020; Castellan et al. 2019], the recursion combinator is obtained via the usual recipe in denotational semantics, as the least fixed point of

$$ F \mapsto (f : O \to O \vdash F f). $$

Let us give a direct description of the strategy obtained (the recursive equation gives a different choice of copy indices, which does not matter up to the equivalence of strategies in [Castellan and Clairambault 2020; Castellan et al. 2019] – the choice we use here allows for a lighter presentation).
<figure><img src="image_45.png" /><figcaption>Fig. 41. Basic strategies for IPA primitives</figcaption></figure>

Let us start by drawing the strategy on U. We use particular exponential signatures generated by

$$ \begin{align*} () &:= \ell \diamond \\ (e_{n+1}, e_n, \dots, e_1) &:= \kappa \langle e_{n+1}, (e_n, \dots, e_1) \rangle, \end{align*} $$

yielding $(e_n, \dots, e_1) \in \mathcal{E}$ for each $e_1, \dots, e_n \in \mathcal{E}$. With this convention, we draw the recursion combinator for U in Figure 43. Again the representation is symbolic, with similar branches for all $e_1, \dots, e_{n+1} \in \mathcal{E}$. We leave in grey the answers, which always propagate back to the previous call.

We consider $Y_O$ for O well-opened, so the recursion strategy in general has a spine exactly as the black part of Figure 43. The rest of the strategy is simple copycat behaviour; which may be simply described via the following direct characterization of the $+-$covered configurations of $Y_O$:
<figure><img src="image_46.png" /><figcaption>Fig. 42. $let_{X,Y} : (!X \to Y) \otimes X \vdash Y$</figcaption></figure>

<figure><img src="image_47.png" /><figcaption>Fig. 43. Fixpoint combinator on U</figcaption></figure>

**PROPOSITION C.21.** For $O$ a well-opened arena, the strategy $Y_O$ has **events** a subset $|Y_O| \subseteq |!| (!O \to O) \vdash O|$, and **+-covered configurations** the compatible unions of configurations of the form

$$ \emptyset \to ((\cdot) :: x) \vdash x \\ (e_{n+1} :: (e_n, \dots, e_1) :: x) \to ((e_{n+1}, \dots, e_1) :: x) \vdash \emptyset, $$

for $n \in \mathbb{N}$, $e_1, \dots, e_{n+1} \in \mathcal{E}$, $x \in \mathcal{C}(O)$; **compatible** means that the union is in $\mathcal{C}(!O \to O) \vdash O)$.

We slightly reformulate this proposition to give a more explicit description of +-covered configurations of $Y_O$. In the next lemma, we use the injection of $(\cdot) : \mathcal{E}^* \to \mathcal{E}$.

**LEMMA C.22.** There is an order-isomorphism between $\mathcal{C}^+(Y_O)$ and tuples $(J \subseteq \mathcal{E}^+, z \in \mathcal{C}(O), (x_s \in \mathcal{C}^\neq\emptyset(O))_{s \in J})$ such that $J$ is suffix-closed, and empty if $z$ is.<fnref n="1" /> The isomorphism sends $(J, z, (x_s))$ to

$$ (\emptyset \to (\cdot) :: z) \leftrightarrow (e :: (s) :: x_{e \cdot s} \to (e \cdot s) :: x_{e \cdot s})_{e \cdot s \in J} \vdash z. $$

*New reference.* Next, we introduce the strategy for reference initialization.

The intuition is that **newref**<sub>X</sub> : !V ~ X ⊢ X applies its argument to cell : !V, the *memory cell*, which implements the stateful behaviour. Just like an actual memory, cell is inherently *sequential*: it treats read and write requests in some sequential order. In order to define it, we first define, for all $n \in \mathbb{N}$, cell<sub>n</sub> as the language of non-empty prefixes of the infinite tree cell<sub>n</sub><sup>0</sup>, defined as:

$$ \text{cell}_n^E = (\tau_{\psi} Q, [e], \bullet)^{-} \cdot (\tau_{\psi} A, [e], n)^{+} \cdot \text{cell}_n^{E \psi\{e\}} \\ | (w_{\psi} Q, [e], k)^{-} \cdot (w_{\psi} A, [e], \check{\vee})^{+} \cdot \text{cell}_k^{E \psi\{e\}}, $$

with $e \notin \mathcal{E}$. Intuitively, words in $\text{cell}_n^E$ are alternating (i.e. Opponent and Player alternate) executions of read and write requests, for a memory cell initialized with value $n$: upon a read request, the memory cell returns $n$ and carries on with $\text{cell}_n$. Upon a write request for $k$, the memory cell returns an acknowledgement and proceeds as $\text{cell}_k$. The set $\mathcal{E}$ propagates the set of exponential signatures already encountered: this lets us always pick fresh exponential signatures for new queries, ensuring words in $\text{cell}_n^E$ are plays on !V in the sense of Definition 4.6. We may then define:

<footnote n="1">¹A stack in $J$ represents a call stack: a list $e_n \cdot e_{n-1} \cdot \dots \cdot e_1$ represents the calls made to the argument: $e_1$ is the first call made in the execution, and so on.</footnote>
*Definition C.23.* We define a prestrategy precell : !V with components:

$$
\begin{align*}
|\text{precell}| &= \text{cell}_0 \\
\leq_{\text{precell}} &= \sqsubseteq \\
s \#_{\text{precell}} s' &\Leftrightarrow \neg(s \sqsubseteq s' \lor s' \sqsubseteq s) \\
\partial_{\text{precell}}(sa) &= a,
\end{align*}
$$

where $\sqsubseteq$ is the prefix ordering.

It is easy to see that this indeed defines a prestrategy. An illustration may be found in [Castellan and Clairambault 2020, Figure 39] (with a slightly different notation for moves). Next we define:

*Definition C.24.* We define a strategy cell : !V as: cell = α<sub>V</sub> ⊙ precell : !V.

Indeed, composition is well-defined on prestrategies, and the copycat envelope of a prestrategy is always a strategy [Castellan et al. 2017]. Intuitively, this wraps the sequential behaviour of cell by buffers, which exactly match the buffers of the Petri structure in Figure ??.

To obtain the strategy for newref<sub>X</sub>, we must add a copycat behaviour on X:

*Definition C.25.* We define a strategy newref<sub>X</sub> : !V ~ X ⊢ X with components:

$$
\begin{align*}
|\text{newref}_X| &= |\text{cell}| + |\alpha_X| \\
\leq_{\text{newref}_X} &= (\leq_{\text{cell}} + \leq_{\alpha_X}) \\
&\quad \cup \{(r_1((r_2 Q, [] , \bullet)), l(s)) \mid m \in |\text{cell}|\} \\
&\quad \cup \{(r_1((l_2 Q, [] , \bullet)), l(s)) \mid m \in |\text{cell}|\} \\
\#_{\text{newref}_X} &= \#_{\text{cell}} + \#_{\alpha_X} \\
\partial_{\text{newref}_X}(l(m)) &= l_r l_{-} \partial_{\text{cell}}(m) \\
\partial_{\text{newref}_X}(r_1(l_r m)) &= l_r r_{-} m \\
\partial_{\text{newref}_X}(r_1(r_2 m)) &= r_2 m
\end{align*}
$$

So cell is plugged after the first Player move of α_X. In other words, newref_X first plays as copycat on X; and plays as cell on !V when it becomes available.

For the later unfolding, we shall use the following characterization of +-covered configurations:

PROPOSITION C.26. There is an order-isomorphism:

$$
\langle-, -\rangle : \mathcal{C}^+(\text{precell}) \times \mathcal{C}^{\neq 0}(\mathbf{X}) \cong \mathcal{C}^{+, \neq 0}(\text{newref}_X)
$$
such that $\partial_{\text{newref}_X}(\langle s, x \rangle) = |s| \to x \vdash x \in \mathcal{C}(!V \to X \vdash X)$.

PROOF. By Definition C.25, the characterization of confs. of composition, and Lemma C.9. □

Above, we implicitly use the one-to-one correspondence between $\mathcal{C}^+(\text{precell})$ and even-length
words in $\text{cell}_0$; and if $s$ is an even length word in $\text{cell}_0$, then $|s| \in \mathcal{C}(!V)$ is its set of events.

In a +-covered configuration of newref, all read and write requests have been successfully handled.
Proposition C.26 shows that besides the almost independent copycat behaviour on X, +-covered
configurations of newref exactly correspond to some sequential ordering of these requests.

*New semaphore.* The interpretation of semaphores work exactly as for references. We first define the alternating behaviour of a semaphore as the language of non-empty prefixes of:

$$
\text{lock}_0^E = (g_5 Q, [e], \bullet)^{-} \cdot (g_5 A, [e], \checkmark)^{+} \cdot \text{lock}_1^{E \psi \{e\}} \quad e \notin E
$$

$$
\text{lock}_n^E = (r_5 Q, [e], \bullet)^{-} \cdot (r_5 A, [e], \checkmark)^{+} \cdot \text{lock}_0^{E \psi \{e\}} \quad e \notin E, n > 0
$$

A semaphore with value 0 may be grabbed, carrying on with value 1. A semaphore with value
$n > 0$ may be released, carrying on with value 0. As for references, the next step is to form:
**Definition C.27.** We define a *prestrategy* prelock : !S with components:

$$
\begin{align*}
|\text{prelock}| &= \text{lock}_0 \\
\leq_{\text{prelock}} &= \sqsubseteq \\
s \#_{\text{prelock}} s' &\Leftrightarrow \neg(s \sqsubseteq s' \lor s' \sqsubseteq s) \\
\partial_{\text{prelock}}(sa) &= a.
\end{align*}
$$

*Definition C.28.* We define a strategy lock : !S as lock = αᵢS ⊙ prelock : !S.

**Definition C.29.** We define a strategy newsemₓ : !S → X ⊢ X with components:

$$
\begin{align*}
|\text{newsem}_X| &= |\text{lock}| + |\alpha_X| \\
\leq_{\text{newref}_X} &= (\leq_{\text{lock}} + \leq_{\alpha_X}) \\
& \quad \cup \{(r_1((r_1^Q, []), \bullet)), l(s)) \mid m \in |\text{lock}|\} \\
& \quad \cup \{(r_2((r_2^Q, []), \bullet)), l(s)) \mid m \in |\text{lock}|\} \\
\#_{\text{newsem}_X} &= \#_{\text{lock}} + \#_{\alpha_X} \\
\partial_{\text{newsem}_X}(l(m)) &= l_1 l_2 \partial_{\text{lock}}(m) \\
\partial_{\text{newsem}_X}(r_1(l_1 m)) &= l_1 r_2 m \\
\partial_{\text{newsem}_X}(r_2(l_2 m)) &= r_2 m
\end{align*}
$$

And, finally, we have a similar characterization of (non-empty) +-covered configurations:

**PROPOSITION C.30.** *There is an order-isomorphism:*

$$
\langle-, -\rangle : \mathcal{C}^{+}(\text{prelock}) \times \mathcal{C}^{\neq 0}(X) \cong \mathcal{C}^{+, \neq 0}(\text{newsem}_X)
$$

$$
\text{such that } \partial_{\text{newsem}_X}(\langle s, x \rangle) = |s| \to x \vdash x \in \mathcal{C}(!S \to X \vdash X).
$$

This concludes the description of the IPA-structure of Strat.

C.3.4 Complement: on symmetry.

Games and strategies with symmetry. Thin concurrent games [Castellan et al. 2019] share with AJM games the fact that strategies play explicit copy indices – in [Castellan et al. 2019] and AJM games those are natural numbers, whereas here they are exponential signatures. The consequence is that in order to satisfy required equational laws (typically, making ! a well-behaved exponential modality), one must be able to consider strategies up to their choice of copy indices.

In concurrent games, this *reindexing* is handled by *event structures with symmetry*:

*Definition C.31.* A **event structure with symmetry** is $E = (|E|, \leq_E, \#_E, \mathcal{S}(E))$ is an es ($|E|, \leq_E, \#_E$) with $\mathcal{S}(E)$ a set of bijections between configurations:

$\theta : x \cong_E y$

comprising all identity bijections, closed under composition and inverse, and satisfying further bisimulation-like properties, omitted here [Castellan et al. 2019].

In [Castellan and Clairambault 2020; Castellan et al. 2019], both games and strategies are event structures with symmetry. Intuitively, in a game A, we have $\theta : x \cong_A y$ in $\mathcal{S}(A)$ when $\theta$ is an order-isomorphism only affecting copy indices – in the terminology of this paper, it changes the exponential signatures in the exponential stack, but leaves all other components unchanged.

The symmetry on the game yields a more permissive equivalence on strategies: namely, a weak isomorphism $\varphi : \sigma \approx \tau$ is an invertible map of event structure such that the triangle

<figure><img src="image_48.png" /></figure>
commutes *up to symmetry*, defined as {($\partial_{\sigma}s, \partial_{\tau}(\varphi(s))$) | s ∈ x} ∈ $\mathcal{S}(A)$ for all x ∈ $\mathcal{C}(\sigma)$. Weak isomorphism makes the exponential satisfy all the required laws (typically, making each !A a commutative comonoid), which were not satisfied up to plain isomorphism.

In turn, composition must preserve weak isomorphism. But that holds only for strategies that are uniform, i.e. invariant under the choice of copy indices. In [Castellan and Clairambault 2020; Castellan et al. 2019], uniformity of strategies is ensured by also adjoining them a symmetry. On a strategy $\sigma$: A, the bisimulation-like properties of $\mathcal{S}(\sigma)$ ensures that if Opponent changes their copy indices, $\sigma$ may change its copy indices accordingly, but not more. This makes $\approx$ a congruence, and strategies up to $\approx$ satisfy all the required equational laws to model higher-order languages. This issue is discussed at length in [Castellan et al. 2019].

*Removing symmetry.* The model developed in [Castellan and Clairambault 2020] is a structure StratSym with two equivalences $\cong$ (standard isomorphism) and $\approx$ (weak isomorphism<fnref n="2" />). Both are preserved by all constructions, but the laws of Seely categories are satisfied with respect to $\approx$ only.

Now, the first observation is that though $\approx$ is crucial in establishing adequacy for StratSym (for instance, the $\beta$-law in IPA is validated by the interpretation only up to $\cong$), the statement itself (Theorem 4.40 in [Castellan and Clairambault 2020]) is independent of the equivalence relation. So once adequacy is established we can ignore $\approx$, and from [Castellan and Clairambault 2020] we get an IPA-structure StratSym/$\cong$ with an adequate interpretation of IPA.

The next point is that symmetries do not carry operational behaviour, they are merely there to witness uniformity so that $\approx$ is a congruence. As mere uniformity witnesses, they can be safely forgotten once $\approx$ is out of the picture. Concretely, in all operations involved in the interpretation, symmetries of the operand strategies are used in computing the symmetries of the resulting strategies only – the event structure itself never depends on the symmetries of operands. Consequently:

**PROPOSITION C.32.** *There is a symmetry-forgetting IPA-functor StratSym/$\cong$ → Strat.*

From this, it follows by Lemma 3.3 that Strat is an adequate IPA-structure.

On a foundational level, it would be interesting to see how symmetries may be obtained by unfolding just as plain strategies. It would require setting up symmetries between histories of runs of Petri strategies as well. But this is not necessary for our purposes, so we leave that for later.

# D THE IPA-STRUCTURE PStrat

## D.1 The Precategory PStrat

The main step is to prove that Petri strategies are stable under composition.

### D.1.1 Composition.
Consider A, B, C arenas, $\sigma: A \vdash B$ and $\tau: B \vdash C$ Petri strategies.

The idea is simple: as Petri strategies, both $\sigma$ and $\tau$ abide by the rules of the game as long as the external Opponent does so. As no agent can be the first to break the rules, the whole interaction ends up correct. This kind of reasoning is very common in game semantics. To formalize it, the difficulty is not conceptual but purely notational: we need tools to project a run $\rho$ on $\tau \odot \sigma$ to runs on $\sigma$ and $\tau$, and to an *interaction* in more familiar game-semantic terms:

**Definition D.1.** Consider the set $\mathit{MInt} = \ell(\mathit{Moves}) \dot{\to} m(\mathit{Moves}) \dot{\to} r(\mathit{Moves})$.

An **interaction** is a sequence $u \in \mathit{MInt}^*$. We write $\mathit{Int}$ for the set of all interactions.

As in traditional play-based game semantics, an interaction has three components: $\sigma$ “plays” on $\ell$, $m$, $\tau$ “plays” on $m$, $r$, and the composite $\tau \odot \sigma$ “plays” on $\ell, r$. Again as in game semantics, we shall *restrict* interactions to these various components. In more generality, we define:

<footnote n="2">²In fact, [Castellan and Clairambault 2020] uses a variant called *positive iso*, but the difference is irrelevant for this discussion.</footnote>
<figure><img src="image_49.png" /><figcaption>Fig. 44. Description of instantiated transitions of $\tau \odot \sigma$</figcaption></figure>

<figure><img src="image_50.png" /><figcaption>Fig. 45. Projections of instantiated transitions</figcaption></figure>

**Definition D.2.** Consider $f : X \to Y$, and $s \in X^*$, we define $s \uparrow f \in Y^*$ the **restriction of s** following s as $\varepsilon \uparrow f = \varepsilon$, $sa \uparrow f = (s \uparrow f)f(a)$ if $f(a)$ is defined, and $sa \uparrow f = s \uparrow f$ otherwise.

A first direct application of this notion is to project $u \in \text{Int}$ to its various components with

$$u_{\sigma} = u \uparrow \ell_{\tau} \ell^{*} \cup \tau_{\tau} m^{*},$$

$$u_{\tau} = u \uparrow \ell_{\tau} m^{*} \cup \tau_{\tau} r,$$

$$u_{\tau \odot \sigma} = u \uparrow \ell_{\tau} \ell^{*} \cup \tau_{\tau} r^{*}$$

where $\ell^* : \ell(\text{Moves}) \to \text{Moves sends } \ell(m) \text{ to } m \text{ and is undefined otherwise, and likewise for } m^*$ and $r^*$. Juxtaposition is function composition, and $\cup$ is the union of their graph.

We also use restriction to extract from a run $\rho$ on $\tau \odot \sigma$ an interaction, and runs $\rho_{\sigma}$ and $\rho_{\tau}$ on $\sigma$ and $\tau$ respectively. But the partial functions involved are more complex, and require us to understand better the shape of instantiated transitions of $\tau \odot \sigma$:

**LEMMA D.3.** Consider $\sigma$ and $\tau$ Petri structures.

Then, instantiated transitions of $\tau \odot \sigma$ are exactly as in Figure 44 – in the sense that that there is a one-to-one correspondence between instantiated transitions in the premises and in the conclusion.

Using this description, we define in Figure 45 partial functions $lbl_{\oplus} : \mathscr{E}_{\tau \odot \sigma} \to \text{MInt}$, $\pi_{\sigma} : \mathscr{E}_{\tau \odot \sigma} \to \mathscr{E}_{\sigma}$ and $\pi_{\tau} : \mathscr{E}_{\tau \odot \sigma} \to \mathscr{E}_{\tau}$ extracting various data from instantiated transitions, following the characterization of instantiated transitions of $\tau \odot \sigma$ given in Figure 44.
Finally, those projection functions are extended to instantiated transitions in context via:

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

and symmetrically for $\pi_{\tau} : \mathcal{F}_{\tau \circ \sigma} \to \mathcal{F}_{\tau}$. Using these, from a run $\rho : \emptyset \to \tau \circ \sigma$ we extract:

$$ \mathrm{Int}(\rho) = \rho \upharpoonright \mathrm{lbl}_{\emptyset} \qquad \rho_{\sigma} = \rho \upharpoonright \pi_{\sigma}, \qquad \rho_{\tau} = \rho \upharpoonright \pi_{\tau}, $$

which allow us to prove the following property:

**LEMMA D.4.** Consider $\rho : \emptyset \to \tau \circ \sigma$. Then, $\alpha = \alpha_{\sigma} + \alpha_{\tau}$ and

$$ \rho_{\sigma} : \emptyset \to \alpha_{\sigma}, \qquad \rho_{\tau} : \emptyset \to \alpha_{\tau} $$

where play($\rho$) = Int($\rho$)$_{\tau \circ \sigma}$, play($\rho_{\sigma}$) = Int($\rho$)$_{\sigma}$ and play($\rho_{\tau}$) = Int($\rho$)$_{\tau}$.
Moreover, Coll($\rho$) = Coll($\rho_{\sigma}$) + $^{\circ}$ Coll($\rho_{\tau}$).

**PROOF.** A lengthy and grindy induction on $\rho$. For $\rho$ empty this is clear, otherwise we reason by cases on the last instantiated transition in context of $\rho$, following the Figure 44.

Consider first that we have $\rho' = \rho(\ell^{\circ}(t^{0})(\ell^{\circ}(\mu)) \upharpoonright \gamma) : \emptyset \to \tau \circ \sigma \beta$ where $\rho : \emptyset \to \tau \circ \sigma \alpha$,

$$ \ell^{\circ}(t^{0})(\ell^{\circ}(\alpha)) : \ell^{\circ}(\mu) \mapsto_{\tau \circ \sigma} \ell^{\circ}(\nu), \qquad \ell^{\circ}(t^{0})(\ell^{\circ}(\alpha)) \upharpoonright \gamma : \alpha \mapsto_{\tau \circ \sigma} \beta $$

with necessarily $\alpha = \ell^{\circ}(\mu) \upharpoonright \gamma$ and $\beta = \ell^{\circ}(\nu) \upharpoonright \gamma$, and $t^{0}(\mu] : \mu \mapsto_{\sigma} \nu$. By IH, $\alpha = \alpha_{\sigma} + \alpha_{\tau}$ with

$$ \rho_{\sigma} : \emptyset \to \alpha_{\sigma}, \qquad \rho_{\tau} : \emptyset \to \alpha_{\tau}, $$

so in particular that entails that $\gamma = \gamma_{\sigma} + \alpha_{\tau}$ with $\alpha_{\sigma} = \mu \upharpoonright \gamma_{\sigma}$. Now, we have

$$ t^{0}(\mu] \upharpoonright \gamma_{\sigma} : \alpha_{\sigma} \to_{\sigma} \beta_{\sigma} $$

writing $\beta_{\sigma} = \nu \upharpoonright \gamma_{\sigma}$. Writing $\beta_{\tau} = \alpha_{\tau} = \gamma_{\tau}$, we have

$$ (\rho(\ell^{\circ}(t^{0})(\ell^{\circ}(\mu)) \upharpoonright \gamma))_{\sigma} = \rho_{\sigma}(t^{0}(\mu] \upharpoonright \gamma_{\sigma}) : \emptyset \to \alpha_{\sigma} \beta_{\sigma} $$

and $(\rho(\ell^{\circ}(t^{0})(\ell^{\circ}(\mu)) \upharpoonright \gamma))_{\tau} = \rho_{\tau} : \emptyset \to \alpha_{\tau} \beta_{\tau}$. Moreover, play($\rho'$) = play($\rho$), Int($\rho'$) = Int($\rho$), play($\rho'_{\sigma}$) = play($\rho_{\sigma}$) and play($\rho'_{\tau}$) = play($\rho_{\tau}$), making required properties obvious. Finally, Coll($\rho'$) = Coll($\rho$) $\cup$ $\ell^{\circ}$(v), Coll($\rho'_{\sigma}$) = Coll($\rho_{\sigma}$) $\cup$ v and Coll($\rho'_{\tau}$) = Coll($\rho_{\tau}$), so Coll($\rho'$) = Coll($\rho'_{\sigma}$) + $^{\circ}$ Coll($\rho'_{\tau}$) follows from IH. The case of a neutral transition from $\tau$ is symmetric.

Next, consider that $\rho' = \rho(\ell^{\circ}(t^{+})(\ell^{\circ}(\alpha)) \upharpoonright \gamma) : \emptyset \to \tau \circ \sigma \beta$, where $\rho : \emptyset \to \tau \circ \sigma \alpha$,

$$ \ell^{\circ}(t^{+})(\ell^{\circ}(\mu)) : \ell^{\circ}(\mu) \stackrel{\ell^{(m)}}{\underset{\tau \circ \sigma}{\to}} \emptyset, \qquad \ell^{\circ}(t^{+})(\ell^{\circ}(\alpha)) \upharpoonright \gamma : \alpha \to \tau \circ \sigma \beta $$

where necessarily $\alpha = \ell^{\circ}(\mu) \upharpoonright \gamma$ and $\beta = \gamma$, and $t^{+}(\mu] : \mu \stackrel{\ell^{(m)}}{\underset{\sigma}{\to}} \emptyset$. Now, by IH, $\alpha = \alpha_{\sigma} + \alpha_{\tau}$ with

$$ \rho_{\sigma} : \emptyset \to \alpha_{\sigma}, \qquad \rho_{\tau} : \emptyset \to \alpha_{\tau}, $$

so in particular that entails $\gamma = \gamma_{\sigma} + \alpha_{\tau}$ with $\alpha_{\sigma} = \mu \upharpoonright \gamma_{\sigma}$. Now, we have

$$ t^{+}(\mu] \upharpoonright \gamma_{\sigma} : \alpha_{\sigma} \to_{\sigma} \beta_{\sigma} $$

writing $\beta_{\sigma} = \gamma_{\sigma}$. Writing $\beta_{\tau} = \alpha_{\tau} = \gamma_{\tau}$, we have

$$ (\rho(\ell^{\circ}(t^{+})(\ell^{\circ}(\mu)) \upharpoonright \gamma))_{\sigma} = \rho_{\sigma}(t^{+}(\mu] \upharpoonright \gamma_{\sigma}) : \emptyset \to \alpha_{\sigma} \beta_{\sigma} $$

and $(\rho(\ell^{\circ}(t^{+})(\ell^{\circ}(\mu)) \upharpoonright \gamma))_{\tau} = \rho_{\tau} : \emptyset \to \alpha_{\tau} \beta_{\tau}$. Moreover, play($\rho'$) = play($\rho$)$\ell^{(m)}(m)$, Int($\rho'$) = Int($\rho$)$\ell^{(m)}(m)$, play($\rho'_{\sigma}$) = play($\rho_{\sigma}$)$\ell^{(m)}(m)$ and play($\rho'_{\tau}$) = play($\rho_{\tau}$), making the required properties clear. Finally, Coll($\rho'$) = Coll($\rho$), Coll($\rho'_{\sigma}$) = Coll($\rho_{\sigma}$) and Coll($\rho'_{\tau}$) = Coll($\rho_{\tau}$), so Coll($\rho'$) = Coll($\rho'_{\sigma}$) + $^{\circ}$ Coll($\rho'_{\tau}$) follows from IH. The case of a positive transition from $\tau$ is symmetric.
Next, consider that we have $\rho' = \rho(\tau^{\circ}(t^{-}) \llbracket (s, d) \rrbracket \uplus \gamma) : \emptyset \longrightarrow \tau^{\circ}\sigma \beta$, where $\rho : \emptyset \longrightarrow \tau^{\circ}\sigma \alpha$,

$$ \ell^{\circ}(t^{-}) \llbracket (s, d) \rrbracket : \emptyset \xrightarrow{\ell^{(m)}} \ell^{\circ}(v), \qquad \ell^{\circ}(t^{-}) \llbracket (s, d) \rrbracket \uplus \gamma : \alpha \longrightarrow \tau^{\circ}\sigma \beta $$

where necessarily, $\alpha = \gamma$ and $\beta = \ell^{\circ}(v) \uplus \gamma$, and $t^{-} \llbracket (s, d) \rrbracket : \emptyset \xrightarrow{\ell^{(m)}} \sigma v$. By IH, $\alpha = \alpha_{\sigma} + \circ \alpha_{\tau}$ with

$$ \rho_{\sigma} : \emptyset \longrightarrow \sigma \alpha_{\sigma}, \qquad \rho_{\tau} : \emptyset \longrightarrow \tau \alpha_{\tau}, $$

so that $\gamma = \gamma_{\sigma} + \circ \gamma_{\tau}$ with $\gamma_{\sigma} = \alpha_{\sigma}, \gamma_{\tau} = \alpha_{\tau}$. Writing $\beta_{\sigma} = \gamma_{\sigma} \uplus \nu$ and $\beta_{\tau} = \gamma_{\tau} = \alpha_{\tau}$, we have

$$ (\rho(\tau^{\circ}(t^{-}) \llbracket (s, d) \rrbracket \uplus \gamma))_{\sigma} = \rho_{\sigma}(t^{-} \llbracket (s, d) \rrbracket \uplus \gamma_{\sigma}) : \emptyset \longrightarrow \sigma \beta_{\sigma} $$

and $(\rho(\tau^{\circ}(t^{-})) \llbracket (s, d) \rrbracket \uplus \gamma)_{\tau} = \rho_{\tau} : \emptyset \longrightarrow \tau \beta_{\tau}$. Moreover, play($\rho'$) = play($\rho$)$\ell_{\cdot}(m)$, Int($\rho'$) = Int($\rho$)$\ell_{\cdot}(m)$, play($\rho'_{\sigma}$) = play($\rho_{\sigma}$)$\ell_{\cdot}(m)$ and play($\rho'_{\tau}$) = play($\rho_{\tau}$), making the required properties clear. Finally, Coll($\rho'$) = Coll($\rho$) $\cup$ $\ell^{\circ}(v)$, with Coll($\rho'_{\sigma}$) = Coll($\rho_{\sigma}$) $\cup$ $\nu$ and Coll($\rho'_{\tau}$) = Coll($\rho_{\tau}$), so Coll($\rho'$) = Coll($\rho'_{\sigma}$) + $\circ$ Coll($\rho'_{\tau}$) follows from IH. Negative transitions from $\tau$ are symmetric.

Consider finally $\rho' = \rho((t^{+} \otimes t^{-}) \llbracket \ell^{\circ}(\mu) \rrbracket) \uplus \gamma : \emptyset \longrightarrow \tau^{\circ}\sigma \beta$ where $\rho : \emptyset \longrightarrow \tau^{\circ}\sigma \alpha$,

$$ (t^{+} \otimes t^{-}) \llbracket \ell^{\circ}(\mu) \rrbracket : \ell^{\circ}(\mu) \longmapsto_{\tau^{\circ}\sigma} \tau^{\circ}(v), \qquad (t^{+} \otimes t^{-}) \llbracket \ell^{\circ}(\mu) \rrbracket \uplus \gamma : \alpha \longrightarrow_{\tau^{\circ}\sigma} \beta $$

where necessarily, $\alpha = \ell^{\circ}(\mu) \uplus \gamma$, $\beta = \tau^{\circ}(v) \uplus \gamma$, and where we necessarily have

$$ t^{+} \llbracket \mu \rrbracket : \mu \xrightarrow{\ell^{(m)}} \sigma \emptyset, \qquad t^{-} \llbracket (s, d) \rrbracket : \emptyset \xrightarrow{\ell^{(m)}} \tau \nu, $$

with $\delta_{\sigma}\langle t^{+} \rangle(\mu) = (s, d)$, $\ell_{\cdot}(m) = (\ell_{\cdot}(m), s, d)$ where $\ell_{\cdot}(m) = \partial_{\sigma}(t^{+})$; and $\delta_{\tau}\langle t^{-} \rangle(s, d) = \nu$. Now,

$$ \rho_{\sigma} : \emptyset \longrightarrow \sigma \alpha_{\sigma}, \qquad \rho_{\tau} : \emptyset \longrightarrow \tau \alpha_{\tau} $$

for $\alpha = \alpha_{\sigma} + \circ \alpha_{\tau}$ by IH, and necessarily $\gamma = \gamma_{\sigma} + \circ \gamma_{\tau}$ with $\alpha_{\sigma} = \mu \uplus \gamma_{\sigma}$ and $\alpha_{\tau} = \gamma_{\tau}$. Writing $\beta_{\sigma} = \gamma_{\sigma}$ and $\beta_{\tau} = \gamma_{\tau} \uplus \nu$, we have $\beta = \beta_{\sigma} \uplus \beta_{\tau}$. Hence, we can form the projected runs

$$ \rho'_{\sigma} = \rho_{\sigma}(t^{+} \llbracket \mu \rrbracket \uplus \gamma_{\sigma}) : \emptyset \longrightarrow \sigma \beta_{\sigma}, \qquad \rho'_{\tau} = \rho_{\tau}(t^{-} \llbracket (s, d) \rrbracket \uplus \gamma_{\tau}) : \emptyset \longrightarrow \tau \beta_{\tau}, $$

satisfying play($\rho'$) = play($\rho$), Int($\rho'$) = Int($\rho$)$m(m)$, play($\rho'_{\sigma}$) = play($\rho_{\sigma}$)$\tau_{\cdot}(m)$ and play($\rho'_{\tau}$) = play($\rho_{\tau}$)$\ell_{\cdot}(m)$ from which the required verifications are immediate. Finally, Coll($\rho'$) = Coll($\rho$) $\cup$ $\tau^{\circ}(v)$ with Coll($\rho'_{\sigma}$) = Coll($\rho_{\sigma}$) and Coll($\rho'_{\tau}$) = Coll($\rho_{\tau}$) $\cup$ $\nu$, so Coll($\rho'$) = Coll($\rho'_{\sigma}$) + $\circ$ Coll($\rho'_{\tau}$) follows from IH. The case $t^{-} \otimes t^{+}$ is symmetric, concluding the proof. $\square$

Using this lemma, we shall now prove that a valid run of $\tau \odot \sigma$ projects to valid runs on $\sigma$ and $\tau$. For this we will also exploit the following easy lemma.

**LEMMA D.5.** Consider A, B arenas, and $s \in |A \vdash B|^*$.

Then, $s \in \text{Plays}(A \vdash B)$ iff $s \upharpoonright \ell_{\cdot}^{*} \in \text{Plays}(A)$ and $s \upharpoonright \tau_{\cdot}^{*} \in \text{Plays}(B)$.

**PROOF.** Straightforward. $\square$

**LEMMA D.6.** Consider $\rho : \emptyset \longrightarrow \tau^{\circ}\sigma \alpha$ such that play($\rho) \in \text{Plays}(A \vdash C)$.

Then, play($\rho_{\sigma}) \in \text{Plays}(A \vdash B)$ and play($\rho_{\tau}) \in \text{Plays}(B \vdash C)$.

**PROOF.** By induction on $\rho$. For $\rho$ empty this is clear.

Consider first that we have $\rho' = \rho(\ell^{\circ}(t^{0}) \llbracket \ell^{\circ}(\mu) \rrbracket \uplus \gamma) : \emptyset \longrightarrow \tau^{\circ}\sigma \beta$ where $\rho : \emptyset \longrightarrow \tau^{\circ}\sigma \alpha$,

$$ \ell^{\circ}(t^{0}) \llbracket \ell^{\circ}(\alpha) \rrbracket : \ell^{\circ}(\mu) \longmapsto_{\tau^{\circ}\sigma} \ell^{\circ}(v), \qquad \ell^{\circ}(t^{0}) \llbracket \ell^{\circ}(\alpha) \rrbracket \uplus \gamma : \alpha \longrightarrow_{\tau^{\circ}\sigma} \beta, $$

in that case play($\rho'_{\sigma}$) = play($\rho_{\sigma}$) and play($\rho'_{\tau}$) = play($\rho_{\tau}$), so the property follows from IH. The case of a neutral transition from $\tau$ is symmetric.

Consider next that $\rho' = \rho(\ell^{\circ}(t^{+}) \llbracket \ell^{\circ}(\alpha) \rrbracket) \uplus \gamma : \emptyset \longrightarrow \tau^{\circ}\sigma \beta$, where $\rho : \emptyset \longrightarrow \tau^{\circ}\sigma \alpha$,

$$ \ell^{\circ}(t^{+}) \llbracket \ell^{\circ}(\mu) \rrbracket : \ell^{\circ}(\mu) \xrightarrow{\ell^{(m)}}_{\tau^{\circ}\sigma} \emptyset, \qquad \ell^{\circ}(t^{+}) \llbracket \ell^{\circ}(\alpha) \rrbracket \uplus \gamma : \alpha \longrightarrow_{\tau^{\circ}\sigma} \beta $$
where necessarily $\alpha = \ell^{\circ}(\mu) \uplus \gamma$ and $\beta = \gamma$, and $t^+(|\mu|) : \mu \stackrel{\ell_c(m)}{\longmapsto} \emptyset$. By IH, we have

$$ \mathrm{play}(\rho_{\sigma}) \in \mathrm{Plays}(A \vdash B), $$

$$ \mathrm{play}(\rho_{\tau}) \in \mathrm{Plays}(B \vdash C) $$

and as $\mathrm{play}(\rho'_{\tau}) = \mathrm{play}(\rho_{\tau})$, we have $\mathrm{play}(\rho'_{\tau}) \in \mathrm{Plays}(B \vdash C)$ as required. Now, we have

$$ \rho_{\sigma} : \emptyset \longrightarrow \alpha_{\sigma}, \quad t^{+}(|\mu|) \uplus \gamma_{\sigma} : \alpha_{\sigma} \stackrel{\ell_c(m)}{\longmapsto} \beta_{\sigma} $$

with components named as in the proof of Lemma D.4, and with $s = \mathrm{play}(\rho_{\sigma}) \in \mathrm{Plays}(A \vdash B)$. Hence by condition valid of Petri strategies, $s\ell_c(m) = \mathrm{play}(\rho'_{\sigma}) \in \mathrm{Plays}(A \vdash B)$, which concludes this case. The case of a positive transition from $\tau$ is symmetric.

Consider next that $\rho' = \rho(\tau^{\circ}(t^{-})(|s, d|)) \uplus \gamma) : \emptyset \longrightarrow \tau_{\circ\sigma}\beta$, where $\rho : \emptyset \longrightarrow \tau_{\circ\sigma}\alpha$,

$$ \ell^{\circ}(t^{-})(|s, d|) : \emptyset \stackrel{\ell_c(m)}{\longmapsto} \ell^{\circ}(\nu), $$

$$ \ell^{\circ}(t^{-})(|s, d|) \uplus \gamma : \alpha \longrightarrow \tau_{\circ\sigma}\beta, $$

in that case $\mathrm{play}(\rho'_{\sigma}) = \mathrm{play}(\sigma)\ell_c(m)^{-}$ and $\mathrm{play}(\rho'_{\tau}) = \mathrm{play}(\tau)$. By IH we have $\mathrm{play}(\rho'_{\sigma}) \in \mathrm{Plays}(A \vdash B)$ and $\mathrm{play}(\rho'_{\tau}) = \mathrm{play}(\rho_{\tau}) \in \mathrm{Plays}(B \vdash C)$. But by hypothesis, we have $\mathrm{play}(\rho') = \mathrm{play}(\rho)\ell_c(m) \in \mathrm{Plays}(A \vdash C)$. By Lemma D.5, $\mathrm{play}(\rho)\ell_c(m) \upharpoonright \ell_c^* = (\mathrm{play}(\rho) \upharpoonright \ell_c^*)m \in \mathrm{Plays}(A)$. But $\mathrm{play}(\rho'_{\sigma}) \upharpoonright \ell_c^* = (\mathrm{play}(\rho) \upharpoonright \ell_c^*)m \in \mathrm{Plays}(A)$, and $\mathrm{play}(\rho'_{\sigma}) \upharpoonright \tau_c^* = \mathrm{play}(\rho_{\sigma}) \upharpoonright \tau_c^*$, so $\mathrm{play}(\rho'_{\sigma}) \in \mathrm{Plays}(A \vdash B)$ by Lemma D.5. The case of a negative transition from $\tau$ is symmetric.

Consider finally $\rho' = \rho((t^{+} \otimes t^{-})(|\ell^{\circ}(\mu)|)) \uplus \gamma) : \emptyset \longrightarrow \tau_{\circ\sigma}\beta$ where $\rho : \emptyset \longrightarrow \tau_{\circ\sigma}\alpha$,

$$ (t^{+} \otimes t^{-})(|\ell^{\circ}(\mu)|) : \ell^{\circ}(\mu) \longmapsto \tau_{\circ\sigma}\tau^{\circ}(\nu), $$

$$ (t^{+} \otimes t^{-})(|\ell^{\circ}(\mu)|) \uplus \gamma : \alpha \longrightarrow \tau_{\circ\sigma}\beta $$

where necessarily, $\alpha = \ell^{\circ}(\mu) \uplus \gamma$, $\beta = \tau^{\circ}(\nu) \uplus \gamma$, and where we necessarily have

$$ t^{+}(|\mu|) : \mu \stackrel{\tau_c(m)}{\longmapsto} \emptyset, \quad t^{-}(|s, d|) : \emptyset \stackrel{\ell_c(m)}{\longmapsto} \tau \nu, $$

with $\delta_{\sigma}\langle t^{+}\rangle(\mu) = (s, d)$, $\ell_c(m) = (\ell_c(m), s, d)$ where $\ell_c(m) = \partial_{\sigma}(t^{+})$; and $\delta_{\tau}\langle t^{-}\rangle(s, d) = \nu$. By IH,

$$ \mathrm{play}(\rho_{\sigma}) \in \mathrm{Plays}(A \vdash B), \quad \mathrm{play}(\rho_{\tau}) \in \mathrm{Plays}(B \vdash C). $$

Summing up the situation on the side of $\sigma$, we have

$$ \rho_{\sigma} : \emptyset \longrightarrow \alpha_{\sigma}, \quad t^{+}(|\mu|) \uplus \gamma_{\sigma} : \alpha_{\sigma} \stackrel{\ell_c(m)}{\longmapsto} \beta_{\sigma} $$

with components as in the proof of Lemma D.4. By condition valid of Petri strategies, $\mathrm{play}(\rho'_{\sigma}) = \mathrm{play}(\rho_{\sigma})\tau_c^*(m) \in \mathrm{Plays}(A \vdash B)$. By Lemma D.5, this entails $\mathrm{play}(\rho_{\sigma})\tau_c^*(m) \upharpoonright \tau_c^* = (\mathrm{play}(\rho_{\sigma}) \upharpoonright \tau_c^*)m \in \mathrm{Plays}(B)$. Now, Lemma D.4 also entails $\mathrm{play}(\rho'_{\sigma}) = \mathrm{Int}(\rho)_{\sigma}$ and $\mathrm{play}(\rho'_{\tau}) = \mathrm{Int}(\rho)_{\tau}$. So:

$$ \mathrm{play}(\rho'_{\sigma}) \upharpoonright \tau_c^* = \mathrm{Int}(\rho) \upharpoonright m^* = \mathrm{play}(\rho'_{\tau}) \upharpoonright \ell_c^*, $$

so that $\mathrm{play}(\rho'_{\tau}) \upharpoonright \ell_c^* = (\mathrm{play}(\rho_{\sigma}) \upharpoonright \ell_c^*)m \in \mathrm{Plays}(B)$. Now, we also have $\mathrm{play}(\rho'_{\tau}) \upharpoonright \tau_c^* = \mathrm{play}(\rho_{\tau}) \upharpoonright \tau_c^* \in \mathrm{Plays}(C)$ by Lemma D.5; so by Lemma D.5 again we deduce $\mathrm{play}(\rho'_{\tau}) \in \mathrm{Plays}(B \vdash C)$ as required. The case of a synchronized transition $t^{-} \otimes t^{+}$ is symmetric. $\square$

We are finally in position to prove that Petri strategies are stable under composition.

**PROPOSITION D.7.** If $\sigma : A \vdash B$ and $\tau : B \vdash C$ are Petri strategies, then so is $\tau \odot \sigma : A \vdash C$.

Moreover, if $\sigma$ and $\tau$ are negative, so is $\tau \odot \sigma$.

**PROOF.** Valid. Consider $\rho : \emptyset \longrightarrow \tau_{\circ\sigma}\alpha$ with $\mathrm{play}(\rho) \in \mathrm{Plays}(A \vdash C)$, and $f^+ : \alpha \stackrel{m'}{\longrightarrow} \beta$. W.l.o.g., assume $m' = \ell_c(m)$. By Lemma D.4, $\alpha$ decomposes as $\alpha_{\sigma} + \circ \alpha_{\tau}$, and we have:

$$ \rho_{\sigma} : \emptyset \longrightarrow \alpha_{\sigma}, \quad \rho_{\tau} : \emptyset \longrightarrow \tau_{\circ} \alpha_{\tau}. $$

Now, $f^+$ must have the form $f^+ = (\ell^{\circ}(t^+)(|\ell^{\circ}(\mu)|)) \uplus \gamma$ with $t^+(|\mu|) : \mu \stackrel{\ell_c(m)}{\longmapsto} \emptyset$, and $\beta = \gamma$. Hence,

$$ t^{+}(|\mu|) \uplus \gamma_{\sigma} : \alpha_{\sigma} \stackrel{\ell_c(m)}{\longmapsto} \beta_{\sigma}, $$
with components named as in the proof of Lemma D.4. At this point we apply Lemma D.6, which ensures that $\text{play}(\rho_{\sigma}) \in \text{Plays}(A \vdash B)$. Hence since $\sigma$ is valid, $\text{play}(\rho_{\sigma})\ell_{+}(m) \in \text{Plays}(A \vdash B)$ as well. It follows by Lemma D.5 that $\text{play}(\rho') = \text{play}(\rho)\ell_{-}(m) \in \text{Plays}(A \vdash C)$ as well.

**Receptive.** Consider $\rho: \emptyset \to \tau \circledot \sigma$ with $s = \text{play}(\rho) \in \text{Plays}(A \vdash C)$, and $sm' \in \text{Plays}(A \vdash C)$ with $m'$ negative – say w.l.o.g. that $m' = \ell_{+}(m)^{-}$. By Lemma D.6, we have

$$ \text{play}(\rho_{\sigma}) \in \text{Plays}(A \vdash B), \quad \text{play}(\rho_{\tau}) \in \text{Plays}(B \vdash C), $$

and by Lemma D.6 we may deduce that $\text{play}(\rho_{\sigma})\ell_{+}(m) \in \text{Plays}(A \vdash B)$. By receptive, there is

$$ e^{-} = t^{-} \langle (s, d) \rangle : \emptyset \stackrel{\ell_{-}(m)}{\longmapsto} \sigma \beta $$

for $\beta \cap \alpha_{\sigma} = \emptyset$. Hence $\ell^{\circ}(t^{-}) \langle (s, d) \rangle : \emptyset \stackrel{\ell_{-}(m)}{\longmapsto} \tau \circledot \sigma \ell^{\circ}(\beta)$ with $\ell^{\circ}(\beta) \cap \alpha = \emptyset$. For uniqueness, if

$$ e' = \emptyset \stackrel{\ell_{-}(m)}{\longmapsto} \tau \circledot \sigma \beta' $$

for some $\beta'$. Necessarily, $e' = \ell^{\circ}(t') \langle (s', d') \rangle$ for $t' \langle (s', d') \rangle : \emptyset \stackrel{\ell_{-}(m)}{\longmapsto} \sigma \beta''$ for $\beta' = \ell^{\circ}(\beta'')$. But by uniqueness of receptivity for $\sigma$, we have $t' \langle (s', d') \rangle = t \langle (s, d) \rangle$, so that $t = t'$, $(s, d) = (s', d')$.

**Strongly safe.** Consider $\rho: \emptyset \to \tau \circledot \sigma$ with $\text{play}(\rho) \in \text{Plays}(A \vdash C)$, with a new instantiated transition in context $f$ – we distinguish cases depending on its form.

Assume first $f = \ell^{\circ}(t^{0}) \langle \ell^{\circ}(\mu) \rangle \uplus \gamma$ for $t^{0}(\mu) : \mu \mapsto_{\sigma} \nu$. By Lemma D.6, we have $\text{play}(\rho_{\sigma}) \in \text{Plays}(A \vdash B)$, so that since $\sigma$ is strongly safe, $\text{new}(t^{0}(\mu))$ is fresh in $\rho_{\sigma}$. But $\text{new}(\ell^{\circ}(t^{0}) \langle \ell^{\circ}(\mu) \rangle) = \ell^{\circ}(\text{new}(t^{0}(\mu)))$. Moreover, by Lemma D.4, $\text{Coll}(\rho) = \text{Coll}(\rho_{\sigma}) + \circledot \text{Coll}(\rho_{\tau})$. So it follows that $\text{new}(f)$ is fresh in $\rho$ as required. The case of a neutral transition from $\tau$ is symmetric.

Next assume $f = \ell^{\circ}(t^{+}) \langle \ell^{\circ}(\mu) \rangle \uplus \gamma$. Then $\text{new}(f) = \emptyset$. Idem for a positive transition from $\tau$.

Next assume $f = \ell^{\circ}(t^{-}) \langle (s, d) \rangle \uplus \gamma : \alpha \stackrel{\ell_{-}(m)}{\longmapsto} \tau \circledot \sigma \beta$ with $\text{play}(\rho)\ell_{+}(m) \in \text{Plays}(A \vdash C)$. We have

$$ t^{-} \langle (s, d) \rangle : \emptyset \stackrel{\ell_{-}(m)}{\longmapsto} \nu, $$

and by Lemma D.6, we have $\text{play}(\rho_{\sigma}) \in \text{Plays}(A \vdash B)$. From $\text{play}(\rho)\ell_{+}(m) \in \text{Plays}(A \vdash C)$ and $\text{play}(\rho_{\sigma}) \in \text{Plays}(A \vdash B)$, it follows easily via Lemma D.5 that $\text{play}(\rho_{\sigma})\ell_{-}(m) \in \text{Plays}(A \vdash B)$. So since $\sigma$ is strongly safe, $\text{new}(t^{-} \langle (s, d) \rangle)$ is fresh in $\rho_{\sigma}$. We conclude as in the neutral case using Lemma D.4. The case of a negative transition from $\tau$ is similar.

Finally, assume $f = (t^{+} \otimes t^{-}) \langle \ell^{\circ}(\mu) \rangle \uplus \gamma$. Say that we have

$$ (t^{+} \otimes t^{-}) \langle \ell^{\circ}(\mu) \rangle : \ell^{\circ}(\mu) \stackrel{\ell_{-}(m)}{\longmapsto} \tau \circledot \sigma \tau^{\circ}(\nu), $$

so that $\text{new}(f) = \tau^{\circ}(\nu) - \text{assume } t^{+}(\mu) : \mu \stackrel{\ell_{-}(m)}{\longmapsto} \sigma \emptyset$ and $t^{-}(\langle (s, d) \rangle) : \emptyset \stackrel{\ell_{-}(m)}{\longmapsto} \tau \nu$. By Lemma D.5, $\text{play}(\rho_{\tau})\ell_{-}(m) \in \text{Plays}(B \vdash C)$. Therefore since $\tau$ is strongly safe, $\text{new}(t^{-} \langle (s, d) \rangle) = \nu$ is fresh in $\rho_{\tau}$. But by Lemma D.4, $\text{Coll}(\rho) = \text{Coll}(\rho_{\sigma}) + \circledot \text{Coll}(\rho_{\tau})$, so $\text{new}(f) = \tau^{\circ}(\nu)$ is fresh in $\rho$ as required. The other synchronized case is symmetric.

**Negative.** Straightforward by inspection and negativity of $\sigma$ and $\tau$. $\square$

### D.1.2 Copycat.
First, we characterize the markings of copycat reachable through a play:

Recall that $\mathcal{L}_{\mathcal{A}} = \text{mult}(A)$, so that the set $\text{TokL}(\mathcal{A}_A)$ of tokils of $\mathcal{A}_A$ is in bijection with $|A|$. This lets us silently coerce a configuration $x \in \mathcal{C}(A)$ into a marking $x \in \mathcal{M}(\mathcal{A}_A)$. In order to show that copycat is a Petri strategy, we first characterize the markings reachable by rule-abiding runs:

**LEMMA D.8.** Consider A an arena, and $\rho: \emptyset \to \tau \circledot \sigma$ such that $\text{play}(\rho) \in \text{Plays}(A \vdash A)$.

Then, $|\text{play}(\rho)| = x \vdash y$ with $x, y \in \mathcal{C}(A)$ and $y \supseteq^{-} x \cap y \supseteq^{+} x$; and $\alpha = (y^{-} \setminus x) \uplus (x^{+} \setminus y)$.

Moreover, $\text{Coll}(\rho) = y^{-} \uplus x^{+}$, where $x^p$ is the subset of $x \in \mathcal{C}(A)$ whose moves have polarity $p$.
PROOF. By induction on $\rho$. For $\rho$ empty, this is clear. Consider $\rho' = \rho f : \emptyset \longrightarrow \alpha_A$ with $\rho : \emptyset \longrightarrow \alpha_A$, and $\text{play}(\rho') \in \text{Plays}(A \vdash A)$. We also have $\text{play}(\rho) \in \text{Plays}(A \vdash A)$, so by IH,

$$|\text{play}(\rho)| = x \vdash y, \quad y \supseteq x \cap y \subseteq x, \quad \alpha = (y^{-} \setminus x) \uplus (x^{+} \setminus y),$$

we reason by cases depending on $f$. If $f = (m^{+}, r')((s, d)^{\text{@m}}) \uplus y$, then $\alpha = \{(s, d)^{\text{@m}}\} \uplus y$, and

$$\begin{align*} |\text{play}(\rho')| &= x \vdash y \uplus \{(m, s, d)\} \\ \beta &= \alpha \setminus \{(s, d)^{\text{@m}}\}; \end{align*}$$

since $\alpha = (y^{-} \setminus x) \uplus (x^{+} \setminus y)$, $(s, d)^{\text{@m}} \in \alpha$ and $(m, s, d)$ is positive, $(m, s, d)$ is positive and must be in $x$. It follows that the invariant is preserved. The case $f = (m^{-}, \ell)((s, d)^{\text{@m}}) \uplus \gamma$ is symmetric.

If $f = (m^{-}, r')((s, d)) \uplus \gamma$, then $\alpha = \gamma$, and

$$\begin{align*} |\text{play}(\rho')| &= x \vdash (y \uplus \{(m, s, d)\}) \\ \beta &= \alpha \uplus \{(s, d)^{\text{@m}}\}; \end{align*}$$

and $(m, s, d)$ is negative. Since $|\text{play}(\rho')| = x \vdash (y \uplus \{(m, s, d)\})$, $(m, s, d) \notin y$. So, it cannot be in $x$. The invariant directly follows. The case $f = (m^{+}, \ell)((s, d)^{\text{@m}}) \uplus \gamma$ is symmetric. $\square$

It is a direct application of this lemma to prove that copycat is a Petri strategy:

PROPOSITION D.9. For any arena A, $\alpha_A : A \vdash A$ is a negative Petri strategy.

PROOF. Valid. Consider $s \in \text{Plays}(A \vdash A)$ and

$$\rho : \emptyset \stackrel{s}{\longrightarrow} \alpha, \quad f^{+} : \alpha \stackrel{m}{\longrightarrow} \beta,$$

and say w.l.o.g. that $m = r_a$ for $a \in |A|$. This means that $f^+ = (m^+, r')((s, d)^{\text{@m}}) \uplus \gamma$, where $\alpha = \gamma \uplus \{(s, d)^{\text{@m}}\}$, and $m = (r_m, s, d)$. We must show that $s(r_m, s, d) \in \text{Plays}(A \vdash A)$.

By Lemma D.8, $\alpha = (y^{-} \setminus x) \uplus (x^{+} \setminus y)$ where $|s| = x \vdash y$. As $m \in \text{mult}^{+}(A)$, $(m, s, d) \in x^{+} \setminus y$. As $(m, s, d) \notin y$, we have condition non-repetitive. Next, we show $|sm| = x \vdash (y \uplus \{a\})$ is down-closed. Consider $a' \to_A a$. Since A is alternating, $a'$ is negative. Since $x \in \mathscr{C}(A)$ and $a \in x$, we must have $a' \in x$ as well. But by Lemma D.8 we have $y \supseteq x \cap y \subseteq x$, so $a' \in y$ as well. Finally, from conditions locally conflicting, alternating and negative of arenas, pairs of events in minimal conflict have the same polarity. Therefore, as $x \cap y \subseteq x$ and $x \cap y \supseteq y$, we have $x \cup y$ consistent, so in particular $y \cup \{a\} \in \mathscr{C}(A)$. It follows that $sm \in \text{Plays}(A \vdash A)$ as needed.

Receptive. Consider $\rho : \emptyset \longrightarrow \alpha_A$ with $\text{play}(\rho) = s \in \text{Plays}(A \vdash A)$ and $sm^- \in \text{Plays}(A \vdash A)$. W.l.o.g. consider $m = r_a(a)$. Decompose $a = (m, s, d)$ for $m^- \in \text{mult}(A)$ and token $(s, d)$. By inspection there is a unique matching instantiated transition, namely $(m^-, r')((s, d)) : \emptyset \stackrel{m}{\longrightarrow} \{(s, d)^{\text{@m}}\}$. Moreover, by Lemma D.8 we have $\alpha = (y^{-} \setminus x) \uplus (x^{+} \setminus y)$ where $|s| = x \vdash y$. But as $sm^- \in \text{Plays}(A \vdash A)$, by non-repetitive we have $m^- \notin y$. It follows that $(s, d)^{\text{@m}} \notin \alpha$ as required.

Strongly safe. Consider $\rho : \emptyset \longrightarrow \alpha_A$ with $\text{play}(\rho) = s \in \text{Plays}(A \vdash A)$ extended with $f$. If $f$ is positive, then new($f$) = $\emptyset$ and there is nothing to prove. Hence, consider w.l.o.g. $f = (m^-, r')((s, d)) \uplus \alpha$ with $s(r_m(m), s, d)^- \in \text{Plays}(A \vdash A)$. Then, new($f$) = $\{(s, d)^{\text{@m}}\}$. Write $|s| = x \vdash y \in \mathscr{C}(A \vdash A)$. By non-repetitive, $(m, s, d) \notin y$. By Lemma D.8, $\text{Coll}(\rho) = y^{-} \uplus x^{+}$; but as $(m, s, d) \notin y$ and $(m, s, d) \notin x^{+}$ (for polarity reasons), it follows that $\{(s, d)^{\text{@m}}\}$ is fresh in $\rho$.

Negative. Straightforward by inspection. $\square$

We do not detail the clear fact that composition is stable under isomorphism of Petri strategies. Altogether, this concludes the proof of:

COROLLARY D.10. There is PStrat, a precategory with objects arenas, and morphisms negative Petri strategies up to isomorphism.