Richard P Dearden

Matt Colfer

Sam Giles

Diversedentitionsintheearliestchondrichthyans

The dentition in living chondrichthyans (sharks, rays, and elephant sharks) primitively comprises parallel series of ever-growing (and ever-shedding) teeth. Contrastingly, teeth in their sister group osteichthyans (bony fishes and tetrapods) are resorbed and grow in position. "Acanthodians", a poorly understood grade of Palaeozoic fishes in the chondrichthyan stem-group, have long been recognised as key to reconciling these two different modes of growth and discerning the evolutionary origins of teeth. However, these animals display a profusion of poorly understood dental structures as well as a poorly understood relationships. Here we use computed tomographic (CT) methods to better characterise the diversity of oral structures in acanthodian-grade stem-chondrichthyans, and place this in the context of what is known about early chondrichthyan phylogeny.

Conclusions

-Ischnacanthid jaw bones grew by the addition of teeth unidirectionally on an underlying dermal bone, with similarities to both Compagopiscis and chondrichthyan tooth whorls.

-Mandibular splints are probably dermal and possibly present only in acanthodidsthose in ischnacanthids are instead a reinforced region of Meckel's cartilage.

-Acanthodopsis teeth are histologically distinct from underlying bone, but are dissimilar to all other chondrichthyan tooth morphologies. Either an unexpected holdout of teeth in an otherwise toothless clade, or alternatively could be adapted gill rakers?

Introduction12

  Museum national d'histoire naturelle, France, 2 Department of Earth Sciences, University of Oxford, UK, 3 School of Geography, Earth, and Environmental Sciences, University of Birmingham, UK Methods We contextualised this data in the broad agreement from recent phylogenetic studies into early vertebrates (see Coates etal. 2018, Dearden etal. 2019). All four scanned taxa are members of the"Acanthodii" sensu Coates etal. 2018, putatively the earliest-branching grade within chondrichthyans.

-

  1We used CT scanning at Bristol University to scan the jaw bones of four specimens from the collections of the Natural History Museum (NHM), London, UK. All four taxa are Palaeozoic acanthodian-grade stemchondrichthyans. Data was processed in Mimics (Materialise) and visualised in Blender. Simplified scheme of vertebrate relationships 3 On the basis of the inferred character state distribution we suggest possible state changes in the vertebrate total group. osteichthyan -Inner dental arcade shed with resorption (Chen et al) -Putative whorl-like growth in marginal bones (Botella etal.), but see Cunningham etal.) Crown-osteichthyans -ray-finned and lobefinned fishes (inc. tetrapods) -Teeth partially resorbed, shed, and replaced -Teeth borne on dermal jaw bones -Tooth whorls in some taxa (e.g. see Doeland etal.) Teeth of both the lateral and lingual rows added on a dermal bone base, similarly to Compagopiscis (Rücklin et al.) -However, unlike Compagopiscis, they are only added in a single direction, anteriorly. rays, chimaeras -Teeth form parallel rows that are shed labially and replaced lingually -Modified into tooth plates in some taxa -Presumed homologous with stem-chond. tooth whorls -"Acanthodian" stem-chond. -Teeth join at base to form parallel rows which grew by the lingual addition of teeth -Unclear whether teeth or whorls shed (Ørvig 1973).

  -like" stem-chond.-Teeth join at base to form parallel rows which grew by the lingual addition of teeth -

Acknowledgements:Thanks to Emma Bernard at the NHM, London, for access to specimens, and to Tom Davies at Bristol University for help scanning specimens. Thanks also to Christ Church, Oxford, who funded the research via a JRF to SG and the Muséum national d'histoire naturelle, Paris for funding RPD's travel.


Lison Blondeau-Patissier

Pierre Clairambault

Positional Injectivity for Innocent Strategies

Keywords: 2012 ACM Subject Classification Theory of computation → Denotational semantics Game Semantics, Innocence, Relational Semantics, Positionality

In asynchronous games, Melliès proved that innocent strategies are positional: their behaviour only depends on the position, not the temporal order used to reach it. This insightful result shaped our understanding of the link between dynamic (i.e. game) and static (i.e. relational) semantics.

In this paper, we investigate the positionality of innocent strategies in the traditional setting of Hyland-Ong-Nickau-Coquand pointer games. We show that though innocent strategies are not positional, total finite innocent strategies still enjoy a key consequence of positionality, namely positional injectivity: they are entirely determined by their positions. Unfortunately, this does not hold in general: we show a counter-example if finiteness and totality are lifted. For finite partial strategies we leave the problem open; we show however the partial result that two strategies with the same positions must have the same P-views of maximal length.

Introduction

Game semantics presents higher-order computation interactively as an exchange of tokens in a two-player game between Player (the program under study), and Opponent (its execution environment) [START_REF] Hyland | On full abstraction for PCF: I, II, and III[END_REF][START_REF] Abramsky | Full abstraction for PCF[END_REF]. Game semantics has had a strong theoretical impact on denotational semantics, achieving full abstraction results for languages for which other tools struggle.

At the heart of Hyland and Ong's celebrated model [START_REF] Hyland | On full abstraction for PCF: I, II, and III[END_REF] are innocent strategies, matching pure programs. They matter conceptually and technically: many full abstraction results rely on innocent strategies and their definability properties. Accordingly, innocence is perhaps the most studied notion on the foundational side of game semantics, with questions including categorical reconstructions [START_REF] Harmer | Categorical combinatorics for innocent strategies[END_REF], alternative definitions [START_REF] Melliès | Asynchronous games 2: The true concurrency of innocence[END_REF][START_REF] Hirschowitz | Innocent strategies as presheaves and interactive equivalences for CCS[END_REF], non-deterministic [START_REF] Tsukada | Nondeterminism in game semantics via sheaves[END_REF][START_REF] Castellan | Symmetry in concurrent games[END_REF], concurrent [START_REF] Castellan | The parallel intensionally fully abstract games model of PCF[END_REF], or quantitative [START_REF] Tsukada | Innocent strategies are sheaves over plays -deterministic, non-deterministic and probabilistic innocence[END_REF][START_REF] Castellan | The concurrent game semantics of probabilistic PCF[END_REF] extensions. In particular, our modern understanding of innocence is shaped by Melliès' homotopy-theoretic reformulation in asynchronous games [START_REF] Melliès | Asynchronous games 2: The true concurrency of innocence[END_REF]. In this paper, Melliès also introduced an important result: innocent strategies are positional.

Positionality is an elementary notion on games on graphs: a strategy is positional if its behaviour only depends on the current node -the "position" -and not the path leading there. In standard game semantics there is, at first sight, no clear notion of position: plays are primitive, and it is not clear what is the ambient graph. In contrast, asynchronous games and relatives (e.g. concurrent games) admit a transparent notion of position: two plays reach the same position if they feature the same moves, though not necessarily in the same order. In investigating positionality, Melliès' motivation was to bridge standard play-based game semantics with more static, relational-like semantics [START_REF] Abramsky | Concurrent games and full completeness[END_REF][START_REF] Ehrhard | The Scott model of linear logic is the extensional collapse of its relational model[END_REF]. Indeed, points of the web in relational semantics correspond to certain positions in game semantics. Positionality of innocent strategies entails that they are entirely defined by their positions (a property we shall call positional injectivity), so that collapsing game to relational semantics corresponds exactly to keeping only certain positions. See [START_REF] Clairambault | A tale of additives and concurrency in game semantics[END_REF] for a recent account. Now, traditional Hyland-Ong arena games are by no means disconnected from those developments: bridges with relational semantics were also investigated there, notably by Boudes [START_REF] Boudes | Thick subtrees, games and experiments[END_REF]. There, points of the web match so-called thick subtrees, pomsets representing partial explorations of the arena with duplications. This provides positions for Hyland-Ong games. But then, are innocent strategies still positional? Though it came to us as a surprise, it is not hard to find a counter-example. So we focus on the key weakening of the question: are innocent strategies positionally injective? Our main result is positive, for total finite innocent strategies. We first link Hyland-Ong innocence with an alternative, causal formulation inspired from concurrent games [START_REF] Clairambault | A tale of additives and concurrency in game semantics[END_REF], allowing a transparent link between a strategy and its positions. Drawing inspiration from the proof of injectivity of the relational model for MELL proof nets [START_REF] Daniel De | The relational model is injective for multiplicative exponential linear logic[END_REF], we show how to track down duplications in certain well-engineered positions to recover a sufficient portion of the causal structure; and deduce positional injectivity. However, we show that in the general case (without finiteness and totality), positional injectivity fails. Finally, for finite (but not total) innocent strategies we show a partial result, namely that two strategies with the same positions have the same P-views of maximal length.

Tsukada and Ong [START_REF] Tsukada | Plays as resource terms via non-idempotent intersection types[END_REF] show an injective collapse from a category of innocent strategies onto the relational model. Their collapse is similar to ours, with an important distinction: they label moves in each play, coloring contiguous Opponent/Player pairs identically. Labels survive the collapse, allowing to read back causal links directly. This is possible because the web of atomic types is set to comprise countably many such labels -but then, the correspondence between positions and points of the web is lost. In contrast, our theorem requires us to prove injectivity directly, without such labeling.

In Section 2 we introduce the setting and state our main result. In Section 3 we reformulate the problem via a causal presentation of game semantics. In Section 4 we present the proof of positional injectivity for total finite innocent strategies. In Section 5, we show some partial results beyond total finite strategies. Finally, in Section 6, we conclude. Detailed proofs are attached in appendix.

2

Innocent Strategies and Positions

Arenas and Constructions

We start this paper by giving a definition of arenas, which represent types.

▶ Definition 1. An arena is A = ⟨|A|, ≤ A , λ A ⟩ where ⟨|A|, ≤ A ⟩ is a partial order, and λ A : |A| → {-, +} is a polarity function. Moreover, these data must satisfy:

finitary: for all a ∈ |A|, [a] A = {a ′ ∈ |A| | a ′ ≤ A a} is finite, forestial: for all a 1 , a 2 ≤ A a, then a 1 ≤ A a 2 or a 2 ≤ A a 1 , alternating: for all a 1 A a 2 , then λ A (a 1 ) ̸ = λ A (a 2 ), negative: for all a ∈ min(A) = {a ∈ |A| | a minimal}, λ A (a) = -, where a 1 A a 2 means a 1 < A a 2 with no event strictly in between.

Though our notations differ superficially, our arenas are similar to [START_REF] Hyland | On full abstraction for PCF: I, II, and III[END_REF]. They present observable computational events (on a given type) along with their causal dependencies: positive moves are due to Player / the program, and negative moves to Opponent / the environment. We show in Figures 1 and2, read from top to bottom, the representation of the q - tt + ff +

Figure 1

Arena bool q - 0 + 1 + 2 + . . .

(o → o) → o → o q - q + q + q - Figure 3 Arena (o ⇒ o) ⇒ o ⇒ o
datatypes bool and nat as arenas. Opponent initiates the execution with q -, annotated so as to indicate its polarity, and Player may respond any possible value, with a positive move.

We write 1 for the empty arena and o for the arena with exactly one (negative) move. More elaborate types involve matching constructions: the product and the arrow.

▶ Definition 2. Consider A 1 and A 2 arenas. Then, we define A 1 ∥ A 2 as

|A 1 ∥ A 2 | = ({1} × |A 1 |) ∪ ({2} × |A 2 |) (i, a) ≤ A1∥A2 (j, b) ⇔ i = j ∧ a ≤ Ai b λ A1∥A2 (i, a) = λ Ai (a) ,
called their parallel composition or product, and also written

A 1 × A 2 .
For any family (A i ) i∈I of arenas, this extends to i∈I A i in the obvious way. Any arena A decomposes (up to forest iso) as A ∼ = i∈I A i for some family (A i ) i∈I of arenas which are well-opened, i.e. with exactly one initial (i.e. minimal) move. We now define the arrow:

▶ Definition 3. Consider A 1 , A 2 arenas with A 2 well-opened. Then A 1 ⇒ A 2 has: |A 1 ⇒ A 2 | = ({1} × |A 1 |) ∪ ({2} × |A 2 |) (i, a) ≤ A1⇒A2 (j, b) ⇔ (i = j ∧ a ≤ Ai b) ∨ (i = 2 ∧ a ∈ min(A 2 )) λ A1⇒A2 (i, a) = (-1) i • λ Ai (a)
This extends to all arenas with A ⇒ i∈I B i = i∈I A ⇒ B i and A ⇒ 1 = 1.

We will mostly use A ⇒ B for B well-opened. Figure 3

displays (o ⇒ o) ⇒ o ⇒ o, matching the simple type (o → o) → o → o
with atomic type o -the position of moves follows a correspondence between those and atoms of the type. These arena constructions describe call-by-name computation: once Opponent initiates computation with q -, two Player moves become available. Player may call the second argument (terminating computation) or evaluate the first argument, which in turn allows Opponent to call its argument.

Plays and Strategies

In Hyland-Ong games, players are allowed to backtrack, and resume the play from any earlier stage. This is made formal by the notion of pointing strings: ▶ Definition 4. A pointing string over set Σ is a string s ∈ Σ * , where each move may additionally come equipped with a pointer to an earlier move. We often write s = s 1 . . . s n for pointing strings, leaving pointers implicit.

▶ Definition 5. A play on arena A is a pointing string

s = s 1 . . . s n over |A| s.t.: rigid: If s i points to s j , then s j A s i , alternating: for all 1 ≤ i < n, λ A (s i ) ̸ = λ A (s i+1 ), legal: for all 1 ≤ i ≤ n, either s i ∈ min(A) or s i has a pointer. (o → o) → o → o q - q + Figure 4 λf o→o . λx o . x (o → o) → o → o q - q + q - q + Figure 5 λf o→o . λx o . f x (o → o) → o → o q - q + q - q + q - q + Figure 6 λf o→o . λx o . f (f x)
A play is well-opened iff it has exactly one initial move. We write Plays(A) for the set of plays on A, Plays + (A) for even-length plays, and Plays • (A) for well-opened plays.

We write ε for the empty play, ⊑ for the prefix, and ⊑ + if the smaller play has even length. Plays represent higher-order executions. Figures 4, 5 and6 show plays on the arena of Figure 3; matching typical executions of the corresponding simply-typed λ-term. They are read from top to bottom, with pointers as dotted lines. As in Figure 3, the position of moves encodes their identity in the arena. Strategies, representing programs, are sets of plays:

▶ Definition 6. A strategy σ : A on arena A is a non-empty set σ ⊆ Plays + (A) satisfying prefix-closed: ∀s ∈ σ, ∀t ⊑ + s, t ∈ σ , deterministic: ∀s ∈ σ, sab, sab ′ ∈ σ =⇒ sab = sab ′ .
Implicit in the last clause is that sab and sab ′ also have the same pointers.

Visibility and Innocence

Innocence captures that the behaviour only depends on which program phrase currently has control. Intuitively, the "current program phrase" is captured by the P-view. ▶ Definition 7. For any arena A, we set a partial function ⌜-⌝ : Plays(A) ⇀ Plays(A) as:

⌜si⌝ = i if i ∈ min(A), ⌜sn -m + ⌝ = ⌜sn⌝m if the pointer of m is in ⌜sn⌝, ⌜sn + tm -⌝ = ⌜sn⌝m if m points to n,
undefined otherwise. In the last two cases, m keeps its pointer in the resulting play. If defined, ⌜s⌝ is the P-view of s. A play s ∈ Plays(A) is visible iff ∀t ⊑ s, ⌜t⌝ is defined.

We say that s ∈ Plays(A) is a P-view iff ⌜s⌝ = s. A strategy σ : A is visible iff any s ∈ σ is visible. In that case, P-views are always well-defined, so that we may formulate:

▶ Definition 8. A strategy σ : A is innocent iff it is

visible, and satisfies:

innocence: for all sab, t ∈ σ, if ta ∈ Plays(A) and ⌜sa⌝ = ⌜ta⌝, then tab ∈ σ.

where, in tab, b points "as in sab", i.e. so as to ensure that ⌜sab⌝ = ⌜tab⌝.

An innocent σ :

A is determined by ⌜ ⌜σ⌝ ⌝ = {⌜s⌝ | s ∈ σ}, its P-view forest. Figures 4, 5 and 6 present P-views, each inducing an innocent strategy via the P-view forest obtained by evenlength prefix closure. Likewise, Figures 7 and8 induce strategies for the so-called simply-typed "Kierstead terms" λf (o→o)→o . f (λx o . f (λy o . x)) and λf (o→o)→o . f (λx o . f (λy o . y)). P-views are well-opened, so innocent strategies are determined by their set σ • of well-opened plays.

Innocent strategies form a cartesian closed category Inn with as objects arenas, and morphisms from A to B the innocent strategies σ : A ⇒ B. Composing σ : A ⇒ B and τ : B ⇒ C involves a "parallel interaction plus hiding" mechanism, which we omit [START_REF] Hyland | On full abstraction for PCF: I, II, and III[END_REF].

((o → o) → o) → o q - q + q - q + q - q + Figure 7 Kx : ((o → o) → o) → o ((o → o) → o) → o q - q + q - q + q - q + Figure 8 Ky : ((o → o) → o) → o q - 1 1 ∂x o o q + 2 1 o o 4 u u q - 3 1 o o 5 u u q + 6 1 o o 1 1 ∂y G G q - 2 G A A 4 1 G G q + 3 G A A 5 1 G G q - 6 1 G G q + Figure 9
Deseq. Kx and Ky

(o → o → o) → o → o q - q + q - q + q - q + (o → o → o) → o → o q - q + q - q + q - Figure 10 Non-positionality of innocence

Positions

Boudes' "thick subtrees" [START_REF] Boudes | Thick subtrees, games and experiments[END_REF], called positions in this paper, are the central concept informing the link between innocent game semantics and relational semantics. They are simply desequentialized plays, or in other words prefixes of the arena with duplications.

To introduce positions, our first stop is the following notion of configuration. We call events the elements of |x|. Note ⟨|x|, ≤ x ⟩ has exactly one minimal event, which suffices as innocent strategies are determined by well-opened plays. Configurations include:

▶ Definition 9. A configuration x ∈ 𝒞 (A) of arena A is a tuple x = ⟨|x|, ≤ x , ∂ x ⟩ such that ⟨|x|, ≤ x ⟩
▶ Definition 10. The desequentialization (s) ∈ 𝒞 (A) of s = s 1 . . . s n ∈ Plays • (A) has |(s)| = {1, . . . , n}, ∂ (s) (i) = s i ,
and i ≤ (s) j if there is a chain of pointers from s j to s i in s.

We show in Figure 9 the desequentialization of the maximal P-views of K x and K y from Figures 7 and8. Extracting (s) is a first step, we must then forget the identity of its events:

▶ Definition 11. A bijection φ : |x| ∼ = |y| is an isomorphism φ : x ∼ = y iff it is arena-preserving: for all a ∈ |x|, ∂ y (φ(a)) = ∂ x (a), causality-respecting: for all a 1 , a 2 ∈ |x|, we have a 1 x a 2 iff φ(a 1 ) y φ(a 2 ).
A position of A, written x ∈ ⦗A⦘, is an isomorphism class of configurations.

If s ∈ Plays • (A), the position ⦗s⦘ ∈ ⦗A⦘ is the isomorphism class of (s). We pause to consider the positionality of innocent strategies as mentioned in the introduction. Though it will only play a very minor role, we define positional strategies: ▶ Definition 12. Consider σ : A a strategy on A. We set the condition:

positional: ∀sab, t ∈ σ, ta ∈ Plays(A), ⦗sa⦘ = ⦗ta⦘ =⇒ ∃tab ∈ σ, ⦗sab⦘ = ⦗tab⦘.
Innocent strategies are not positional: Figure 10 displays (the two maximal P-views of) the innocent strategy for the λ-term λf o→o→o . λx o . f (f ⊥ x) (f ⊥ ⊥). On the right hand side, the last Opponent move is grayed out as an extension of a P-view triggering no response. After the fifth move the position is the same, contradicting positionality. In Melliès' asynchronous games [START_REF] Melliès | Asynchronous games 2: The true concurrency of innocence[END_REF], explicit copy indices help distinguish the two calls to f . The two plays no longer reach the same position, restoring positionality. But even in asynchronous games, if positions were quotiented by symmetry so as to match relational semantics, positionality would fail.

We turn to the weaker positional injectivity. If σ : A, its positions are those reached by well-opened plays, i.e. ⦗|σ| ⦘ = {⦗s⦘ | s ∈ σ • } ⊆ ⦗A⦘. We may finally ask our main question:

▶ Question 1 (Positional Injectivity). If σ, τ are innocent and ⦗|σ| ⦘ = ⦗|τ | ⦘, do we have σ = τ ?

Links with the Relational Model

To fully appreciate this question, it is informative to consider the link with the relational model. We start with the following observation concerning positions on the arrow arena.

▶ Fact 1. Consider A and B arenas, and write M f (X) for the finite multisets on X.

Then, we have a bijection ⦗A ⇒ B⦘ ∼ = M f (⦗A⦘) × ⦗B⦘.

Recall [START_REF] Ehrhard | The Scott model of linear logic is the extensional collapse of its relational model[END_REF] that the relational model forms a cartesian closed category Rel ! having sets as objects; and as morphisms from A to B the relations R ⊆ M f (A) × B. Considering simple types generated from o and the arrow A → B, and setting the relational interpretation of o as o Rel ! = {q}, then for any type A, there is a bijection r A :

⦗ A Inn ⦘ ∼ = A Rel ! .
▶ Theorem 13. This extends to a functor ⦗| -| ⦘ : Inn → Rel ! , which preserves the interpretation: for any term M : A of the simply-typed λ-calculus, r A (⦗|

M Inn | ⦘) = M Rel ! .
This relational collapse of innocent strategies has been studied extensively [START_REF] Boudes | Thick subtrees, games and experiments[END_REF][START_REF] Melliès | Asynchronous games 2: The true concurrency of innocence[END_REF][START_REF] Tsukada | Plays as resource terms via non-idempotent intersection types[END_REF][START_REF] Castellan | The concurrent game semantics of probabilistic PCF[END_REF][START_REF] Clairambault | Full abstraction for the quantum lambda-calculus[END_REF]. The inclusion ⊆ is easy; the difficulty in proving ⊇ is that game-semantic interaction is temporal: positions arising relationally might, in principle, fail to appear game-semantically because reproducing them yields a deadlock. For innocent strategies this does not happen: this may be proved through connections with syntax [START_REF] Boudes | Thick subtrees, games and experiments[END_REF][START_REF] Tsukada | Plays as resource terms via non-idempotent intersection types[END_REF] or semantically [START_REF] Castellan | The concurrent game semantics of probabilistic PCF[END_REF][START_REF] Clairambault | Full abstraction for the quantum lambda-calculus[END_REF].

In [START_REF] Tsukada | Plays as resource terms via non-idempotent intersection types[END_REF], Tsukada and Ong prove a similar collapse injective. This seems to answer Question 1 positively -but this is not so simple. The interpretation in Rel ! is parametrized by a set X for the ground type o. In [START_REF] Tsukada | Plays as resource terms via non-idempotent intersection types[END_REF], X is required to be countably infinite: this way one allocates one tag for each pair of chronologically contiguous O/P moves, encoding the causal / axiom links. In contrast, for Question 1 we are forced to interpret o with a singleton set {q}, or lose the correspondence between points of the web and positions. We must reconstruct strategies directly from their desequentializations, with no help from labeling or coloring.

Main result

At first this seems desperate. In [START_REF] Tsukada | Plays as resource terms via non-idempotent intersection types[END_REF], an innocent strategy may already be reconstructed from the desequentialization of its P-views. But here, the two plays of Figures 7 and8 yield the configurations of Figure 9, which are isomorphic -so give the same position. Nevertheless K x and K y can be distinguished, via their behaviour under replication. In both plays of Figure 11, we replay the move to which the deepest q + points. This brings K x and K y to react differently, obtaining plays whose positions separate ⦗|K x | ⦘ and ⦗|K y | ⦘. So, by observing the behaviour of a strategy under replication, we can infer some temporal information.

Most of the paper will be devoted to turning this idea into a proof. However, we have only been able to prove the result with the following additional restrictions on strategies.

((o → o) → o) → o ((o → o) → o) → o q - q - q + q + K x ∋ q - K y ∋ q - q +
q + q - q - q + q + q - q - q + q + Total finite strategies are already well-known: on arenas interpreting simple types they exactly correspond to β-normal η-long normal forms of simply-typed λ-terms.

We now state our main result, positional injectivity:

▶ Theorem 15. For any σ, τ : A innocent total finite, σ = τ iff ⦗|σ| ⦘ = ⦗|τ | ⦘.
As observed in Section 2.1, all arenas decompose as

A = i∈I A i with A i well-opened. As × is a cartesian product in Inn, strategies σ : A also decompose as σ = ⟨σ i | i ∈ I⟩ with σ i : A i for all i ∈ I. From innocence it follows that ⦗|⟨σ i | i ∈ I⟩| ⦘ ∼ = i∈I ⦗|σ i | ⦘,
so it suffices to prove Theorem 15 for A well-opened. From now on, we consider all arenas well-opened.

Causal Presentation

Besides the behaviour of strategies under replication, plays also include the order, irrelevant for our purposes, in which branches are explored by Opponent. To isolate the effect of replication, we introduce a causal version of strategies inspired from concurrent games [START_REF] Castellan | Games and strategies as event structures[END_REF].

Augmentations

This formulation rests on the notion of augmentations. Intuitively those correspond to expanded trees of P-views, which enrich configurations with causal wiring from the strategy.

▶ Definition 16. An augmentation on arena

A is a tuple 𝓆 = ⟨|𝓆|, ≤ (𝓆) , ≤ 𝓆 , ∂ 𝓆 ⟩, where (𝓆) = ⟨|𝓆|, ≤ (𝓆) , ∂ 𝓆 ⟩ ∈ 𝒞 (A), and ⟨|𝓆|, ≤ 𝓆 ⟩ is a tree satisfying: rule-abiding: for all a 1 , a 2 ∈ |𝓆|, if a 1 ≤ (𝓆) a 2 , then a 1 ≤ 𝓆 a 2 , courteous: for all a 1 𝓆 a 2 , if λ(a 1 ) = + or λ(a 2 ) = -, then a 1 (𝓆) a 2 , deterministic: for all a - 𝓆 a + 1 and a - 𝓆 a + 2 , then a 1 = a 2 ,
we then write 𝓆 ∈ Aug(A), and call (𝓆) ∈ 𝒞 (A) the desequentialization of 𝓆.

Events of |𝓆| inherit a polarity with λ(a) = λ A (∂ 𝓆 (a)). By rule-abiding and courteous, ⟨|𝓆|, ≤ 𝓆 ⟩ and ⟨|𝓆|, ≤ (𝓆) ⟩ have the same minimal event init(𝓆), called the initial event. If a ∈ |𝓆| is not initial, there is a unique a ′ ∈ |𝓆| such that a ′ 𝓆 a, written a ′ = pred(a) and called the predecessor of a. Likewise, a non-initial a ∈ |𝓆| also has a unique

a ′′ ∈ |𝓆|        q - T v v Ð q + q } } × z $ $ 4 q + q + q - D P P X q - I R R a q - D r r z q - I t t } q + q +        ∈ exp        q - t Ù q + q + q - S T T c q - S v v q +        Figure 12 Causal Kx and its expansion        q - r Ø q + q + t Ù x # # 3 q - E Q Q X q - q - q + q +        ∈ exp        q - t Ù q + q + q - S T T c q - q +        Figure 13
Causal Ky and its expansion such that a ′′ (𝓆) a, written a ′′ = just(a) and called the justifier of a. By courteous and as immediate causality alternates in A (and hence in (𝓆)), both pred(a) and just(a) have polarity opposite to a. They may not coincide, however from courteous they do for a negative.

Figures 12 and13 show augmentations -though the corresponding definitions remain to be seen, those are the causal expansions of K x and K y matching the plays of Section 2.6. In such diagrams, immediate causality from the configuration appears as dotted lines, whereas that coming from the augmentation itself appears as . We set a few auxiliary conditions: ▶ Definition 17. Let 𝓆 ∈ Aug(A) be an augmentation. We set the conditions:

receptive: for all a ∈ |𝓆|, if ∂ 𝓆 (a) A b -, there is a 𝓆 b ′ such that ∂ 𝓆 (b ′ ) = b, +-covered: for all a ∈ |𝓆| maximal in 𝓆, we have λ(a) = +, --linear: for all a 𝓆 a - 1 , a 𝓆 a - 2 , if ∂ 𝓆 (a 1 ) = ∂ 𝓆 (a 2 ) then a 1 = a 2 .
We say that 𝓆 ∈ Aug(A) is total iff it is receptive and +-covered. We will also refer to receptive --linear augmentations as causal strategies.

From Strategies to Causal Strategies

We may easily represent an innocent strategy as a causal strategy: ▶ Proposition 18. For σ : A finite innocent on A well-opened, we set components

|σ| = {⌜s⌝ | s ∈ σ ∧ s ̸ = ε} ∪ {⌜sa⌝ | s ∈ σ ∧ sa ∈ Plays(A)} , s ≤ σ t iff s ⊑ t, sa ≤ (σ) satb iff there is a chain of justifiers from b to a, and ∂ σ (sa) = a. Then σ = ⟨|σ|, ≤ σ , ≤ (σ) , ∂ σ ⟩ ∈ Aug(A)
is a causal strategy, and is total iff σ is total.

The proof appears as Lemmas 39 and 40 in Appendix A. As for configurations, so as to forget the concrete identity of events we consider augmentations up to isomorphism:

▶ Definition 19. A morphism φ : 𝓆 → 𝓅 is a function φ : |𝓆| → |𝓅| satisfying: arena-preserving: ∂ 𝓅 • φ = ∂ 𝓆 , causality-preserving: for all a 1 , a 2 ∈ |𝓆|, if a 1 𝓆 a 2 then φ(a 1 ) 𝓅 φ(a 2 ), configuration-preserving: for all a 1 , a 2 ∈ |𝓆|, if a 1 (𝓆) a 2 then φ(a 1 ) (𝓅) φ(a 2 ).
An isomorphism is an invertible morphism -we then write φ : 𝓆 ∼ = 𝓅.

Note that by arena-preserving, φ must send init(𝓆) to init(𝓅).

The reader may check that the construction of Proposition 18 applied to K x and K y yields, up to isomorphism, the (small) augmentations of Figures 12 and13. The next fact shows that augmentations are indeed an alternative presentation of innocent strategies.

▶ Lemma 20. For any finite innocent strategies σ, τ on arena

A, then σ = τ iff σ ∼ = τ .
Proof. Clearly, σ = τ implies σ = τ . Conversely, assume φ : σ ∼ = τ . Take s = s 1 . . . s n ∈ ⌜ ⌜σ⌝ ⌝, and write s ≤i = s 1 . . . s i . Then we have a chain s ≤1 σ s ≤2 σ . . . σ s ≤n-1 σ s, transported through φ to t ≤1 τ . . . τ t. By arena-preserving, t i = s i for all 1 ≤ i ≤ n. Finally by configuration-preserving, s and t have the same pointers, hence s = t and s ∈ τ . Symmetrically, any P-view t ∈ ⌜ ⌜τ ⌝ ⌝ is in σ, hence ⌜ ⌜σ⌝ ⌝ = ⌜ ⌜τ ⌝ ⌝ and σ = τ by innocence. ◀

Expansions of Causal Strategies

Besides including representations of innocent strategies, augmentations can also represent their expansions, i.e. arbitrary plays, with Opponent's scheduling factored out.

▶ Definition 21. Consider A an arena, and 𝓅 ∈ Aug(A) a causal strategy.

An expansion of 𝓅, written 𝓆 ∈ exp(𝓅), is 𝓆 ∈ Aug(A) such that:

simulation: there is a (necessarily unique) morphism φ : 𝓆 → 𝓅, +-obsessional: for all a -∈ |𝓆| and φ(a

-) 𝓅 b + , there is a - 𝓆 a ′ s.t. φ(a ′ ) = b + .
The relationship between a causal strategy 𝓅 and 𝓆 ∈ exp(𝓅) is analogous to that between an arena A and a configuration x ∈ 𝒞 (A): 𝓆 explores a prefix of 𝓅, possibly visiting the same branch many times. However, determinism ensures that only Opponent may cause duplications, and +-obsessional ensures that only Opponent may refuse to explore certain branches -if a Player move is available in 𝓅, then it must appear in all corresponding branches of 𝓆. Uniqueness of the morphism follows from --linearity and determinism -see Lemma 42 in Appendix A. Figures 12 and13 show expansions of (the causal strategies corresponding to) K x and K y . Now, we set ⦗|𝓅| ⦘ = {⦗𝓆⦘ | 𝓆 ∈ exp(𝓅)} the positions of a causal strategy 𝓅, where ⦗𝓆⦘ is the isomorphism class of (𝓆). By Lemma 20, any innocent σ : A yields a causal strategy σ : A, so this leaves us with the task to prove that the two notions of position coincide.

▶ Proposition 22. For any total finite innocent strategy σ : A, we have ⦗|σ| ⦘ = ⦗|σ| ⦘.

Proof. Additional details appear in Appendix A. Any x ∈ ⦗|σ| ⦘ is the isomorphism class of (s) for s = s 1 . . . s n ∈ σ. We build an expansion 𝓆(s) ∈ exp(σ) as follows. Its configuration is (𝓆(s)) = (s) (see Definition 10) with events |𝓆(s)| = {1, . . . , n}. Its causal order is i ≤ 𝓆(s) j iff j ≥ i and s i is reached in the computation of ⌜s ≤j ⌝. To show that 𝓆(s) ∈ exp(σ) we must provide a morphism φ : 𝓆(s) → σ, which is simply φ(i) = ⌜s ≤i ⌝. So, x = ⦗𝓆(s)⦘ ∈ ⦗|σ| ⦘.

Reciprocally, take x ∈ ⦗|σ| ⦘, obtained as the isomorphism class of some (𝓆), for 𝓆 ∈ exp(σ). From the totality of σ, 𝓆 has maximal events all positive -it has exactly as many Player as Opponent events, and admits a linear extension s = s 1 . . . s n which is alternating, i.e.

λ(s i ) ̸ = λ(s i+1 ) for all 1 ≤ i ≤ n -1. Besides, for any 1 ≤ i ≤ n, ⌜s ≤i ⌝ (treating s as a play on arena (𝓆)) coincides with [s i ] 𝓆 = {s ∈ |𝓆| | s ≤ 𝓆 s i }, totally ordered by ≤ 𝓆 . So, writing ∂ 𝓆 (s) = ∂ 𝓆 (s 1 ) . . . ∂ 𝓆 (s n ) ∈ Plays(A) with pointers inherited from (𝓆), ⌜∂ 𝓆 (s) ≤i ⌝ ∈ ⌜ ⌜σ⌝ ⌝, hence ∂ 𝓆 (s) ∈ σ by innocence and (∂ 𝓆 (s)) ∼ = (s). Therefore, ⦗𝓆⦘ = ⦗∂ 𝓆 (s)⦘ ∈ ⦗|σ| ⦘. ◀
The idea is that plays in σ are exactly linearizations of expansions of σ. From a play we get an expansion by factoring out Opponent's scheduling, mimicking the construction of P-views while keeping duplicated branches separate. Reciprocally, an expansion allows many (alternating) linearizations. For instance, the two plays of Section 2.6 are respectively linearizations of the expansions of Figures 12 and13. This proposition fails if σ is not total, as expansions may then have trailing Opponent moves, preventing an alternating linearization.

Thanks to Proposition 22, we focus on positions reached by expansions of causal strategies.

q - q + q + q + q - q -q -q - q + q + ⇝ q - V w w Ñ q + u Ð Ð Ù x # # 3 q + q + q - F Q Q Y q - R S S c q - F s s { q - R u u q + q + q - { $ $ 5 q + u Ð Ð Ù x # # 3 q + q + q - q - q - i q - { q + q + Figure 14
Non-unique causal explanation q - q + q + q + q - q -q -q -q -q -

q + q + q + q + ⇝ q - I t t } q + w Ñ Ñ w # # 3 q + w Ñ Ñ w # # 3 q + q - E Q Q X q - E Q Q X q - C r r y q - C r r y q - C r r y q - C r r y q + q + q + q +

Positional Injectivity

We now come to the main contribution of this paper, the proof of positional injectivity for total finite causal strategies. We start this section by introducing the proof idea.

Forks and Characteristic Expansions

Just from the static snapshot offered by positions, we must deduce the strategy. Given z ∈ 𝒞 (A), can we uniquely reconstruct its causal explanation, i.e. 𝓆 ∈ Aug(A) such that z = (𝓆)? In general, there is no reason why 𝓆 would be uniquely determined. Indeed, in Figure 14, we show on the left hand side the configuration z 1 underlying Figure 12 -up to iso it has exactly two causal explanations, shown on the right. The rightmost augmentation is not an expansion of K x , so K x is not the only strategy featuring (the isomorphism class of) z 1 . However, we can find a position unique to K x . Consider z 2 the configuration on the left hand side of Figure 15. The only possible augmentation (up to iso) yielding z 2 as a desequentialization appears on the right hand side (call it 𝓆): every other attempt to guess causal wiring fails. In particular, the red and blue immediate causal links are forced by the cardinality of the subsequent duplications. But 𝓆 is an expansion of the unique maximal branch of K x -so it suffices to see z 2 in ⦗|σ| ⦘ to know that σ = K x .

This suggests a proof idea: given 𝓅 1 , 𝓅 2 : A causal strategies with ⦗|𝓅 1 | ⦘ = ⦗|𝓅 2 | ⦘, we devise a characteristic expansion of 𝓅 1 with duplications chosen to make the causal structure essentially unique; meaning it must be an expansion of 𝓅 2 as well. We do this by using:

▶ Definition 23. A fork in 𝓆 ∈ Aug(A) is a maximal non-empty set X ⊆ |𝓆| s.t.: negative: for all a ∈ X, λ(a) = -, sibling: X = {init(𝓆)} or there is b ∈ |𝓆| such that for all a ∈ X, b 𝓆 a, identical: for all a 1 , a 2 ∈ X, ∂ 𝓆 (a 1 ) = ∂ 𝓆 (a 2 ).
We write Fork(𝓆) for the set of forks in augmentation 𝓆.

If 𝓅 is a causal strategy, 𝓆 ∈ exp(𝓅) and X ∈ Fork(𝓆), the definition of expansions ensures that all Player moves caused by Opponent moves in X are copies. So if X has cardinality ♯X = n, and if we find exactly one set of cardinality ≥ n of equivalent Player moves in (𝓆), we may deduce that there is a causal link. For instance, in Figure 15, the causal successors for the fork of cardinality 3 may be found so. In general though, several Opponent moves may cause indistinguishable Player moves, so that the cardinality of a set Y of duplicated Player moves is the sum of the cardinalities of the predecessor forks. To allow us to identify these predecessor sets uniquely, the trick is to construct the expansion so that all forks have cardinality a distinct power of 2, making it so that the predecessor forks can be inferred from the binary decomposition of ♯Y . This brings us to the following definition.

q - ∼ φ q - q + E s s z 3 3 A q + P u u } 6 6 D q - 1 q - 2 q - 1 q - 2 q + W w w Ò ¥ ( ( 9 q + ∼ φ q + q + W w w Ò ¥ ( ( 9 q - q - q - q - q - q - q + q + q + ∼ φ {(q -,q -)} q + q + q + Figure 16
Distinct characteristic expansions reaching the same position ▶ Definition 24. A characteristic expansion of 𝓅 is 𝓆 ∈ exp(𝓅) such that:

injective: for X, Y ∈ Fork(𝓆), if ♯X = ♯Y then X = Y , well-powered: for all X ∈ Fork(𝓆), there is n ∈ N such that ♯X = 2 n , --obsessional: for all a + ∈ |𝓆|, if ∂ 𝓆 (a + ) A b -, there is a + 𝓆 a ′ s.t. ∂ 𝓆 (a ′ ) = b -.
This only constrains causal links in 𝓆 from positives to negatives, but by courteous those are in 𝓆 iff they are in (𝓆). So for 𝓆 ∈ exp(𝓅), that it is a characteristic expansion is in fact a property of (𝓆). Furthermore it is stable under iso so that if

⦗|𝓅 1 | ⦘ = ⦗|𝓅 2 | ⦘, for 𝓆 1 ∈ exp(𝓅 1 )
characteristic there must be 𝓆 2 ∈ exp(𝓅 2 ) characteristic too such that (𝓆 1 ) ∼ = (𝓆 2 ) -so it makes sense to restrict our attention to positions reached by characteristic expansions.

How different can be characteristic 𝓆 1 ∈ exp(𝓅 1 ) and 𝓆 2 ∈ exp(𝓅 2 ) s.t. (𝓆 1 ) ∼ = (𝓆 2 )? A first guess is isomorphic, but that is off the mark; 𝓆 1 and 𝓆 2 have some degree of liberty in swapping forks around (as in Figure 16): they have the "same branches, but with possibly different multiplicity". A significant part of our endeavour has been to construct a relation between augmentations allowing such changes in multiplicity, while ensuring 𝓅 1 ∼ = 𝓅 2 .

Bisimulations Across an Isomorphism

More than simply comparing augmentations, given 𝓆, 𝓅 ∈ Aug(A), a ∈ |𝓆|, b ∈ |𝓅|, we shall need a a predicate a ∼ b expressing that a and b have the same causal follow-up, up to the multiplicity of duplications. In particular, a and b must have "the same pointer", but at first that makes no sense since a and b live in different ambient sets of events. So we also fix an isomorphism φ : (𝓆) ∼ = (𝓅) providing the translation, and aim to define a ∼ φ b parametrized by φ. We give some examples in Figure 16, where φ is any of the two possible isomorphisms, assuming q - 1 and q - 2 correspond to different moves of the arena. This is defined via a bisimulation game: for instance, establishing that the roots are in relation requires us to first match the blue nodes. But as the bisimulation unfolds, requiring all pointers to match up to φ is too strong: the pointers of red moves do not match -but seen from q + this is fine as the justifiers for the red moves are encountered at the same step of the bisimulation game from q + . So our actual predicate has form a ∼ φ Γ b for Γ a context, stating a correspondence between negative moves established in the bisimulation game so far:

▶ Definition 25. A context between 𝓆, 𝓅 ∈ Aug(A) is Γ : dom(Γ) ∼ = cod(Γ) a bijection s.t. dom(Γ) ⊆ |𝓆|, cod(Γ) ⊆ |𝓅|, λ 𝓆 (dom(Γ)) ⊆ {-}, and ∀a -∈ dom(Γ), ∂ 𝓆 (a) = ∂ 𝓅 (Γ(a)).
We may now formulate a first notion of bisimulation across augmentations.

▶ Definition 26. Consider 𝓆, 𝓅 ∈ Aug(A) and an isomorphism φ : (𝓆) ∼ = (𝓅). (1)

if a + 𝓆 a ′ , then there is b + 𝓅 b ′ with a ′ ∼ φ Γ∪{(a ′ ,b ′ )} b ′ , and symmetrically, (2) if a - 𝓆 a ′ , then there is b - 𝓅 b ′ with a ′ ∼ φ Γ b ′ ,
and symmetrically.

As Γ ⊢ (a, b) implies a ′ ̸ ∈ dom(Γ) and b ′ ̸ ∈ cod(Γ), Γ ∪ {(a ′ , b ′ )} remains a bijection.
Of particular interest is the case a ∼ φ ∅ b over an empty context, written simply a ∼ φ b. From this, we deduce a relation between augmentations: we write 𝓆 ∼ φ 𝓅 iff init(𝓆) ∼ φ init(𝓅), for 𝓆, 𝓅 ∈ Aug(A) and φ : (𝓆) ∼ = (𝓅). Resuming the discussion at the end of Section 4.1: bisimulations allow us to express that two characteristic expansions with isomorphic configurations are "the same". More precisely, in due course we will be able to prove:

▶ Proposition 27. Consider 𝓅 1 , 𝓅 2 ∈ Aug(A) causal strategies, 𝓆 1 ∈ exp(𝓅 1 ) and 𝓆 2 ∈ exp(𝓅 2 ) characteristic expansions with an isomorphism φ : (𝓆 1 ) ∼ = (𝓆 2 ). Then, 𝓆 1 ∼ φ 𝓆 2 .
The proof is the core of our injectivity argument, which we will cover in Section 4.5. For now, we focus on how to conclude from 𝓆 1 ∼ φ 𝓆 2 that we have 𝓅 1 ∼ = 𝓅 2 .

Compositional Properties of Bisimulations

To achieve that, we exploit compositional properties of bisimulations. More precisely, we show that 𝓆 i ∈ exp(𝓅 i ) induces a bisimulation 𝓆 i ∼ 𝓅 i , and find a way to compose

𝓅 1 ∼ 𝓆 1 ∼ φ 𝓆 2 ∼ 𝓅 2 (1)
to deduce 𝓅 1 ∼ 𝓅 2 in a sense yet to be defined, and 𝓅 1 ∼ = 𝓅 2 will follow. We start with:

▶
reflexivity: a ∼ id a, transitivity: if a ∼ φ Γ b and b ∼ ψ ∆ c with cod(Γ) = dom(∆), then a ∼ ψ•φ ∆•Γ c, symmetry: if a ∼ φ Γ b then b ∼ φ -1 Γ -1 a.
But in order to treat 𝓆 i ∈ exp(𝓅 i ) as a bisimulation between 𝓆 i and 𝓅 i , Definition 26 does not do the trick: we cannot expect there to be an iso between (𝓆 i ) and (𝓅 i ) as 𝓆 i has by construction many more events. We therefore introduce a variant of Definition 26:

▶ Definition 29. Consider 𝓆, 𝓅 ∈ Aug(A). For a ∈ |𝓆|, b ∈ |𝓅|, Γ, we have a ∼ Γ b if (a) ∂ 𝓆 (a) = ∂ 𝓅 (b) and Γ ⊢ (a, b), (b) just(a + ) ∈ dom(Γ) and Γ(just(a)) = just(b), (1) if a + 𝓆 a ′ , then b + 𝓅 b ′ with a ′ ∼ Γ∪{(a ′ ,b ′ )} b ′ , and symmetrically, (2) if a - 𝓆 a ′ , then b - 𝓅 b ′ with a ′ ∼ Γ b ′ ,

and symmetrically.

This helps us relate 𝓆 and 𝓅 when (𝓆) and (𝓅) are not isomorphic: we set 𝓆 ∼ 𝓅 iff init(𝓆) ∼ {(init(𝓆),init(𝓅))} init(𝓅). A variation of Lemma 28 shows ∼ is an equivalence, and:

▶ Proposition 30. Consider A an arena, 𝓅 ∈ Aug(A) a causal strategy, and 𝓆 ∈ Aug(A).

Then, 𝓆 is a --obsessional expansion of 𝓅 iff 𝓆 ∼ 𝓅.

Proof

⊆ cod(Γ), if a ∼ φ Γ b then a ∼ Γ b.
The proof is immediate by induction: the clause (c) is never used from the hypothesis that Γ is complete. Finally, we apply this to the roots of 𝓆, 𝓅 with context {(init(𝓆), init(𝓅))}.

◀

Altogether, we have:

▶ Proposition 32. Consider 𝓅 1 , 𝓅 2 ∈ Aug(A) causal strategies, 𝓆 1 ∈ exp(𝓅 1 ), 𝓆 2 ∈ exp(𝓅 2 )
characteristic expansions with an iso φ :

(𝓆 1 ) ∼ = (𝓆 2 ). If 𝓆 1 ∼ φ 𝓆 2 , then 𝓅 1 ∼ = 𝓅 2 .
Proof

Clones

In Section 4.1, we introduced characteristic expansions which, via duplications with wellchosen cardinalities, constrain the causal structure. More precisely, if 𝓆 ∈ exp(𝓅) is characteristic, looking at a set of duplicated Player moves in (𝓆) of cardinality n as in Figure 17, decomposing n = i∈I 2 i , we can deduce that the causal predecessors of the q + j 's are among the forks with cardinality 2 i for i ∈ I. But that is not enough: this does not tell us how to distribute the q + j 's to the forks, and not all the choices will work: while the q + j 's are copies, their respective causal follow-ups might differ. So the idea is simple: imagine that the causal follow-ups for the q + j 's are already reconstructed. Then we may compare them using bisimulation, and replicate the same reasoning as above on bisimulation equivalence classes.

So we are left with the task of leveraging bisimulation to define an adequate equivalence relation on |𝓆|. This leads to the notion of clones, our last technical tool. We say that a and b are clones through φ, written a ≈ φ b, if there is a context Γ preserving pointers ( i.e. for all a ′ ∈ dom(Γ), φ(just(a

′ )) = just(Γ(a ′ ))) such that a ∼ φ Γ b.
This allows a and b (and their follow-ups) to change their pointers through some unspecified Γ. Indeed, the picture painted by Figure 17 is limited: a fork might trigger Player moves with different pointers, as in Figure 18. As a ≈ φ b quantifies existentially over contexts,

q - q + 1 q + 2 . . . q + n Figure 17 A set of copied Player moves q + W w w Ò ! 8 8 E q - 1 q - 2 . . . q - n q + 1 ≈ q + 2 ≈ . . . ≈ q + n Figure
i ∈ N, i ∈ I iff there is X i ∈ Fork(𝓆) with ♯X i = 2 i and a -∈ X i , b + ∈ Y such that a - 𝓆 b + .
Proof. For any i ∈ N, we write X i the fork of 𝓆 of cardinality 2 i , if it exists. Consider the set J := {j ∈ N | X j exists, ∃a ∈ X j , ∃b ∈ Y, a 𝓆 b}. Any b ∈ Y is positive and so the unique (by determinism) successor of some negative event a. Moreover a appears in a fork X and by Lemma 34, all events of X are predecessors of events of Y . Hence, we have Y = j∈J succ(X j ), where the union is disjoint since 𝓆 is forest-shaped. Therefore,

♯Y = j∈J ♯succ(X j ) = j∈J ♯X j = j∈J 2 j ,
where the second equality is obtained by determinism. By uniqueness of the binary decomposition, J = I, which proves the lemma by definition of J. ◀

Positional Injectivity

We are finally in a position to prove the core of the injectivity argument.

▶ Lemma 36 (Key lemma). Consider 𝓅 1 , 𝓅 2 ∈ Aug(A) causal strategies, 𝓆 1 ∈ exp(𝓅 1 ) and 𝓆 2 ∈ exp(𝓅 2 ) characteristic expansions, and φ :

(𝓆 1 ) ∼ = (𝓆 2 ). Then, ∀a + ∈ |𝓆 1 |, a ≈ φ φ(a).
Proof. The co-depth of a ∈ |𝓆 i | is the maximal length k of a = a 1 𝓆i . . . 𝓆i a k a causal chain in 𝓆 i . We show by induction on k the two symmetric properties:

(a) for all a + ∈ |𝓆 1 | of co-depth ≤ k, we have a ≈ φ φ(a), (b) for all a + ∈ |𝓆 2 | of co-depth ≤ k, we have a ≈ φ -1 φ -1 (a). Take a + ∈ |𝓆 1 | of co-depth k. If a is maximal in 𝓆 1 , so is φ(a)
in 𝓆 2 and a ≈ φ(a). Else, the successors of a partition as G 1 , . . . , G n ⊆ Fork(𝓆 1 ), where G i = {b - i,1 , . . . , b - i,2 p i }; likewise the successors of φ(a) in 𝓆 2 are the forks φ(G i ). For all 1 ≤ i ≤ n and 1 ≤ j ≤ 2 pi , we claim: for all b i,j 𝓆1 c i,j , there is φ(b i,j ) 𝓆2 d i,j satisfying c i,j ≈ φ d i,j .

(2)

Write X = [c i,j ] ≈ the clone class of c i,j in 𝓆 1 .
It is easy to prove that the clone relation preserves co-depth, so it follows from the induction hypothesis and Lemma 50 that φ(X) is a clone class in 𝓆 2 . By Lemma 35, ♯X has 2 pi in its binary decomposition -and as φ is a bijection, so does ♯(φ(X)). So by Lemma 35, there is φ(b i,j ) ∈ φ(G i ) and d i,j ∈ φ(X) such that φ(b i,j ) 𝓆2 d i,j . Since φ(c i,j ), d i,j ∈ φ(X) they are clones, so using c i,j ≈ φ φ(c i,j ) by induction hypothesis, c i,j ≈ φ d i,j . Likewise, the mirror property of (2) also holds.

Deducing a ≈ φ φ(a) requires some care: cloning is defined via a context, and the c i,j ≈ φ φ(c i,j ) might not share the same. However, the contexts can be put into canonical forms that are shown to agree -Lemma 54 allows us to prove a ≈ φ φ(a) from ( 2) and its mirror property. Finally, (b) is proved symmetrically. ◀ Now, consider 𝓅 1 , 𝓅 2 , 𝓆 1 , 𝓆 2 , φ as in Proposition 27. If the 𝓆 i 's are empty or singleton trees, there is nothing to prove. Otherwise 𝓆 i starts with a -

i 𝓆i b + i with a - i initial. But then [b + i ] ≈ is the only singleton clone class in 𝓆 i . As φ preserves clone classes, φ(b + 1 ) = b + 2 . By Lemma 36, b 1 ≈ φ b 2 . Thus b 1 ∼ φ b 2 , so a 1 ∼ φ a 2 and 𝓆 1 ∼ φ 𝓆 2 .
This concludes the proof of Proposition 27. Putting everything together, we obtain:

▶ Theorem 37. For 𝓅 1 , 𝓅 2 ∈ Aug(A) causal strategies s.t. ⦗|𝓅 1 | ⦘ = ⦗|𝓅 2 | ⦘, then 𝓅 1 ∼ = 𝓅 2 .
Proof. Consider 𝓆 1 ∈ exp(𝓅 1 ) a characteristic expansion. By hypothesis, there must be 𝓆 2 ∈ exp(𝓅 2 ) and φ : (𝓆 1 ) ∼ = (𝓆 2 ); necessarily 𝓆 2 is also a characteristic expansion of 𝓅 2 . By Proposition 27, we have 𝓆 1 ∼ φ 𝓆 2 . By Proposition 32, we have 𝓅 1 ∼ = 𝓅 2 . ◀ Finally, Theorem 15 follows from Theorem 37, Proposition 22 and Lemma 20. Theorem 15 only concerns total finite innocent strategies. In contrast, Theorem 37 requires no totality assumption: totality comes in not in the injectivity argument, but in Proposition 22 linking standard and causal strategies. Without totality, expansions of σ might not have as many Opponent as Player moves, and so may not be linearizable via alternating plays. Intuitively, in alternating plays Opponent may only explore converging parts of the strategy, whereas in the causal setting Opponent is free to explore simultaneously many branches, including divergences. Positional injectivity for partial finite innocent strategies may be studied causally by restricting to +-covered expansions, i.e. with only Player maximal events. But then we must also abandon --obsessionality as Opponent moves leading to divergence will not be played, breaking our proof (Lemma 34 fails) in a way for which we see no fix.

Beyond Total Finite Strategies

Finally, we show some subtleties and partial results on generalizations of Theorem 15. First, positional injectivity fails in general. Consider the infinitary terms

f : o → o → o ⊢ T 1 , T 2 , L, R : o recursively defined as T 1 = f T 2 R, T 2 = f L T 1 , L = f L ⊥ and R = f ⊥ R
in an infinitary simply-typed λ-calculus with divergence ⊥. The corresponding strategies differ: their causal representations appear in Figures 19 and20, infinite trees represented via loops.

We consider positions reached by plays -or equivalently, by +-covered expansions of Figures 19 and20. In fact, both strategies admit all balanced positions on (o → o → o) → o , i.e. with as many Opponent as Player moves. Ignoring the initial q -, a position is a multiset of bricks as in Figure 21, with i ∈ N occurrences of q - 1 and j ∈ N of q - 2 . A brick with i = j = 0 is a leaf. The position is balanced if it has as many Opponent as Player moves. Now, any position can be realized in λf o→o→o . T i by first placing bricks with occurrences of both q - 1 and q - 2 greedily alongside the spine, shown in red in Figures 19 and20. At each step, we continue from only one of the copies opened, leaving others dangling. If this

q - q + 5 5 C q - 1 q - 2 q + R u u q + q - 1 q - 2 H R R `q- 2 d d l q + q - 1 E Q Q X Figure 19 λf o→o→o . T1 q - q + R u u q - 1 q - 2 q + q + 5 5 C q - 1 E Q Q X q - 1 j q - 2 q + q - 2 d d l Figure 20 λf o→o→o . T2 q + q - 1 . . . q - 1 q - 2 . . . q - 2

Figure 21

Bricks gets stuck, apart from leaves we are left with only q - 1 's, or, only q - 2 's, but there is always a matching non-spine infinite branch available. Finally, leaves can always be placed as their number matches that of trailing negative moves by the balanced hypothesis.

We have ⦗| λf o→o→o . T 1 | ⦘ = ⦗| λf o→o→o . T 2 | ⦘ as both strategies can realize all balanced positions on the arena o → o → o , and exactly those: positional injectivity fails.

Positionality for finite innocent strategies remains open. We could only prove:

▶ Theorem 38. Let σ 1 , σ 2 : A be finite innocent strategies with ⦗|σ 1 | ⦘ = ⦗|σ 2 | ⦘.
Then, σ 1 and σ 2 have the same P-views of maximal length.

For the proof (see Appendix C), we assume σ 1 has a P-view s of maximal length n. We perform an expansion of s where each Opponent branching at co-depth 2d + 1 has arity d + 1. By a combinatorial argument on trees, the only way to reassemble its nodes exhaustively in a tree with depth bounded by d is to rebuild exactly the same tree. Hence the tree is also in exp( σ2 ), and s ∈ σ 2 . This steers us into conjecturing that positional injectivity holds for partial finite innocent strategies, but our proof attempts have remained inconclusive.

Conclusion

Though innocent strategies in the Hyland-Ong sense are not positional, total finite innocent strategies satisfy positional injectivity -however, the property fails in general.

Beyond its foundational value, we believe this result may be helpful in the game semantics toolbox. Game semantics can be fiddly; in particular, proofs that two terms yield the same strategy are challenging to write in a concise yet rigorous manner. This owes a lot to the complexity of composition: proving that a play s is in M N involves constructing an "interaction witness" obtained from plays in M and N plus an adequate "zipping" of the two. Manipulations of plays with pointers are tricky and error-prone, and the link between plays and terms is obfuscated by the multi-layered interpretation.

In contrast, Theorem 15 lets us prove innocent strategies equal by comparing their positions. Now, constructing a position of M N simply involves exhibiting matching positions for M and N . Side-stepping the interpretation, this can be presented as typing terms with positions or configurations -combining Section 2.5 and the link between relational semantics and non-idempotent intersection type systems [START_REF] Daniel De | Execution time of λ-terms via denotational semantics and intersection types[END_REF]. For instance, in this way, finite definability, a basic result seldom presented in full formal details, boils down to typing the defined term with the same positions as the original strategy.

A Augmentations and Strategies: Proofs from Section 3

In the sequel, A is a fixed arena. For any augmentation 𝓆 ∈ Aug(A) and event a ∈ |𝓆|, we define succ(a) := {b | a 𝓆 b} the set of immediate successors of a in ≤ 𝓆 . We also define ↑ a the set of descendants of a, i.e. ↑ a := {a ′ | a ≤ 𝓆 a ′ }.

In this first section, we provide more detailed proofs for augmentations as defined in Section 3, studying their expansions and their links with strategies. We start by proving Proposition 18 of Section 3.2, which allows us to see traditional innocent strategies as causal strategies, with the following two lemmas. For any non-empty pointing string s, we use the notation s ω for the last element of s.

▶ Lemma 39. For σ : A finite innocent on A well-opened, σ is a causal strategy, i.e. a receptive --linear augmentation.

Proof. First we must check that (σ) = ⟨|σ|, ≤ (σ) , ∂ σ ⟩ is a configuration. It is clear from the definition and the fact that A is well-opened that ⟨|σ|, ≤ (σ) ⟩ is a finite tree. The well-openedness of A also ensures minimality-respecting.

Causality-preserving. Consider s, t ∈ |σ| such that s (σ) t. Then t ω points to s ω by definition, so by rigidity ∂ σ (s) A ∂ σ (t).

Hence, (σ) is a configuration. We now check that σ is an augmentation. Rule-abiding. Let t ∈ |σ| and s ≤ (σ) t. By definition, there exists a chain of pointers from t ω to s ω . This implies that s ⊑ t, hence s ≤ σ t.

Courteous. Let s σ t such that λ A (s) = + or λ A (t) = -. By definition of ≤ σ , s = s ′ b + and t = s ′ ba -since A is alternating. By definition of a P-view, a points to b and s (σ) t. Deterministic. Let s - σ t + 1 and s - σ t + 2 . By definition of σ , we have s = s ′ a -, t 1 = s ′ ab + 1 , t 2 = s ′ ab + 2
, and b 1 = b 2 (with the same pointer) by determinism of σ. So σ is an augmentation. Finally, we check the two additional conditions. Receptive. Let s ∈ |σ| such that ∂ σ (s) A a -. Since A is alternating, we know s = s ′ b + , and s ∈ σ by definition of σ. Furthermore, ∂ σ (s) A a -implies that sa ∈ Plays(A), where a points to s ω . So sa ∈ |σ|, with s σ sa and ∂ σ (sa) = a.

--linear. Let s σ t - 1 and

s σ t - 2 such that ∂ σ (t 1 ) = ∂ σ (t 2 )
. By definition of ≤ σ , t 1 = sa - 1 and t 2 = sa - 2 , where both a i point to s ω by courtesy. Moreover, by definition of ∂ σ , a 1 = a 2 . Hence t 1 = t 2 . ◀ ▶ Lemma 40. For σ : A finite innocent on A well-opened, σ is total iff σ is total.

Proof. From the previous lemma, σ is always receptive.

If. Assume σ is total. Consider s ∈ |σ| maximal for ≤ σ , and assume λ(s) = -. Then by definition s is a P-view and s = s ′ a -, where s ′ ∈ σ by innocence and s ′ a ∈ Plays(A). By totality of σ, there exists b + such that s ′ ab ∈ σ, and since s is already a P-view we have ⌜s ′ ab⌝ = s ′ ab. Hence s σ s ′ ab, which contradicts the maximality of s.

Only if. Assume σ is total. Consider s ∈ σ such that sa ∈ Plays(A). Let t = ⌜s⌝, then t ∈ σ by innocence of σ. Moreover, ta = ⌜sa⌝ ∈ |σ|. By totality of σ, ta cannot be maximal, so there exists b + such that ta σ tab. Since tab ∈ |σ| and tab = ⌜tab⌝, we also have tab ∈ σ. By innocence of σ, sab ∈ σ, and σ is total. ◀ Those two lemmas prove Proposition 18.

In the development, we focus on expansions of causal strategies (Definition 21). We prove minimality-preservation and uniqueness of morphisms.

▶ Lemma 41. Consider 𝓆 ∈ Aug(A) and a ∈ |𝓆|.

Then ∂ 𝓆 (a) ∈ min(A) iff a = init(𝓆).

Proof. If. Assume that a = init(𝓆). Assuming that ∂ 𝓆 (a) is not minimal, then by condition minimality-preserving of Definition 9, a is not minimal in (𝓆). But then by condition rule-abiding of Definition 16, a cannot be minimal in 𝓆 either, contradiction. Only if. Assume ∂ 𝓆 (a) ∈ min(A). In particular, a has negative polarity since A is negative. Assuming that a is not minimal in 𝓆, then it has an antecedent a ′ 𝓆 a. By courtesy, we have a ′ (𝓆) a as well. Hence, ∂ 𝓆 (a ′ ) A ∂ 𝓆 (a), contradiction. ◀

In particular, this proves that morphisms preserve initial events (by arena-preservation).

▶ Lemma 42. Consider 𝓅 ∈ Aug(A) a causal strategy and 𝓆 ∈ exp(𝓅).

Then there exists a unique morphism φ : 𝓆 → 𝓅.

Proof. The existence is given by the definition of 𝓆 ∈ exp(𝓅). Consider φ, ψ : 𝓆 → 𝓅 two morphisms from 𝓆 to 𝓅. Consider a ∈ |𝓆| minimal such that φ(a) ̸ = ψ(a). If a is minimal for ≤ 𝓆 , this contradicts Lemma 41 (by arena-preservation). Therefore, there is a (necessarily unique) antecedent a ′ 𝓆 a for which φ(a ′ ) = ψ(a ′ ). By causality-preservation of morphisms, we have φ(a ′ ) 𝓅 φ(a) and φ(a ′ ) 𝓅 ψ(a). Proof. Consider x ∈ ⦗|σ| ⦘, it is the isomorphism class of (s) for some s = s 1 . . . s n ∈ σ. We build an augmentation 𝓆(s) as follows: its underlying configuration is (𝓆(s)) = (s), with |𝓆(s)| = {1, . . . , n}. Its causal order is defined inductively with for any i, j ∈ |𝓆(s)|,

i ≤ 𝓆(s) 2j ⇔ i = 2j or i ≤ 𝓆(s) 2j -1 ; i ≤ 𝓆(s) 2j + 1 ⇔ i = 2j + 1 or i ≤ 𝓆(s)
k where s 2j+1 points to s k in s.

Remark that since s is alternating and negative, for any i ∈ |𝓆(s)|, s i is negative iff i is odd. So i ≤ 𝓆(s) j means that s i is reached in the computation of ⌜s ≤j ⌝. It is clear that ⟨|𝓆(s)|, ≤ 𝓆(s) ⟩ is a tree; we must check that 𝓆(s) is an augmentation. Rule-abiding. For any i ≤ (𝓆(s)) j, there exists a chain of justifiers from s i to s j . Since s is P-visible, s i must appear in ⌜s 1 . . . s j ⌝. But ≤ 𝓆(s) is inductively defined to follow the construction of a P-view, so i ≤ 𝓆(s) j.

Courteous. For all i 𝓆(s) j, if pol(s i ) = + (resp. pol(s j ) = -), then i is even (resp. j is odd), and by definition of ≤ 𝓆(s) , we know that s j points to s i . Hence i (𝓆(s)) j.

Deterministic. For any negative i, then i is odd and i 𝓆(s) j implies j = i + 1.

We must now check that 𝓆(s) ∈ exp(σ). Consider φ :

|𝓆(s)| → |σ| such that φ(i) = ⌜s ≤i ⌝. Then φ is a morphism: Arena-preserving. It is clear that ∂ σ • φ = ∂ 𝓆(s)
, since the P-view preserves the last move. Configuration-preserving. For all i (𝓆(s)) j, we know that s j points to s i since (q(s)) = (s). By innocence of σ, s is P-visible and s j keeps its pointer in ⌜s ≤j ⌝ (and this pointer is still s i ). Hence, φ(i) (σ) φ(j).

Causality-preserving. By definition, for any j ∈ |𝓆(s)| such that j ≥ 1, we have 2j -1 𝓆(s) 2j. Moreover, s 2j is positive, so φ(2j) = ⌜s ≤2j ⌝ = ⌜s ≤2j-1 ⌝s 2j , where s 2 j keeps its pointer. So φ(2j -1) σ φ(2j). Likewise, for any i, 2j + 1 ∈ |𝓆(s)|, we have i 𝓆 2j + 1 iff s 2j+1 points to s i in s. In that case, we have φ(2j + 1) = ⌜s ≤2j+1 ⌝ = ⌜s ≤i ⌝s - 2j+1 , where s 2j+1 is negative since 2j + 1 is odd. So φ(i) σ φ(2j + 1). +-obsessional. For all i -∈ |𝓆(s)|, if φ(i) σ t + , then it means t = ⌜s ≤i ⌝b + ∈ σ. Since s ∈ σ, s is of even length, so i + 1 ∈ |𝓆| and by determinism and innocence, s i+1 = b. Therefore, φ(i + 1) = t, and i 𝓆(s) i + 1.

Finally, 𝓆(s) ∈ exp(σ), which means x = ⦗𝓆(s)⦘ ∈ ⦗|σ| ⦘. ◀ ▶ Lemma 44. Consider σ : A a total finite innocent strategy, and x ∈ ⦗|σ| ⦘. Then x ∈ ⦗|σ| ⦘.

Proof. Consider x ∈ ⦗|σ| ⦘, then there exists 𝓆 ∈ exp(σ) such that ⦗𝓆⦘ = x. From the totality of σ (Lemma 40), 𝓆 has maximal events all positive -hence by determinism it has exactly as many Player as Opponent moves. Moreover, by courtesy, any a 𝓆 a ′ implies that λ(a) ̸ = λ(a ′ ), since A is alternating. Therefore, there exists an alternating sequentialization of 𝓆, which we construct inductively. We start by the minimal event of 𝓆, negative by Lemma 41, and its only successor (exists by totality, unique by determinism). If a positive event b + has one or more successors, we inductively construct sequentializations for each subtree of root a -∈ succ(b). All sequences are alternating, start with a negative event, and end with a positive event. Hence, we can concatenate them in an arbitrary order. We obtain an alternating sequence s - 1 , s + 2 , . . . , s + n such that: The same reasoning applies for the symmetric condition. Assume φ(a) + 𝓅 b, then φ -1 (b) exists by receptivity of 𝓆 and --linearity of 𝓅.

|𝓆| = {s i | 1 ≤ i ≤ n}.
(2). Same as for (1), except

[b + ] - 𝓆 = [a] - 𝓆 and [φ(b) + ] - 𝓅 = [φ(a)] - 𝓅 .
The same reasoning applies for the symmetric condition. Assume φ(a) - 𝓅 b, then φ -1 (b) exists by +-obsessionality of 𝓆. ◀

In the following proofs, we will need a few additional properties on bisimulations and contexts, to define a minimal context.

▶ Lemma 46. Consider 𝓆, 𝓅 ∈ Aug(A) with φ : 𝓆 ∼ = 𝓅. Consider a ∼ φ Γ b for some Γ. Then for any a ′ ∈ ↑ a, there exists b ′ ∈ ↑ b such that a ′ ∼ φ Γ∪∆ b ′ , where a = a 0 𝓆 a 1 𝓆 . . . 𝓆 a ′ = a n , b = b 0 𝓅 b 1 𝓅 . . . 𝓅 b ′ = b n , and ∆ is the context defined as ∆ = {(a i , b i ) | 0 ≤ i ≤ n and pol(a i ) = -}. Moreover, if a ∼ φ Γ ′ b for a context Γ ′ , we also have a ′ ∼ φ Γ ′ ∪∆ b ′ . Proof.

B.2 Clones (Section 4.4)

A key notion in the proof of positional injectivity is the notion of clones, a variation of bisimulation. Although the added constraint on contexts makes transitivity more challenging, we can still prove a variation of Lemma 28. We use the same notation that for the usual bisimulation: for any a, b events of an augmentation 𝓆, a ≈ b means a ≈ id b. where Γ 2 ∪ {e, ψ(e)} preserves pointers. Likewise, for any e ′ ∈ dom(Γ 2 ), e ′ / ∈ cod(Γ 1 ), we have Γ 1 ∪ {φ -1 (e ′ ), e ′ } well-defined and pointer-preserving, such that

a ∼ φ Γ1∪{(φ -1 (e ′ ),e ′ )} b .
This allows us to define the following pointer-preserving contexts:

Γ ′ 1 := Γ 1 ∪ {(φ -1 (e ′ ), e ′ ) | e ′ ∈ dom(Γ 2 ), e ′ / ∈ cod(Γ 1 )} Γ ′ 2 := Γ 2 ∪ {(e, ψ(e)) | e ∈ cod(Γ 1 ), e / ∈ dom(Γ 2 )} Then Γ ′ 2 • Γ ′ 1
preserves pointers, and by Lemma 28 we have a

∼ ψ•φ Γ ′ 2 •Γ ′ 1 c, so a ≈ ψ•φ c. ◀ This
≈ ψ c, then a ≈ ψ•φ c, symmetry: if a ≈ φ b then b ≈ φ -1 a.
Proof. Reflexivity. By Lemma 28, a ∼ id a, which implies a ≈ id a.

Transitivity. See Lemma 49. Symmetry. Immediate by Lemma 28: if Γ preserves pointers, so does Γ -1 . ◀

Clones through id in characteristic expansions will be especially interesting, because then we can partition equivalence classes of ≈ id into successors of forks.

▶ Lemma 34. Consider 𝓆 a --obsessional expansion of causal strategy 𝓅 on arena A.

Then, for all a - 1 , a - 2 ∈ X ∈ Fork(𝓆), for all a - We now give the proof of Theorem 38. Consider σ 1 , σ 2 : A finite (but not necessarily total) innocent strategies. If they are empty, there is nothing to prove. Otherwise, let 2n + 2 be the length of s the longest P-view among them. W.l.o.g., assume that s ∈ ⌜ ⌜σ 1 ⌝ ⌝.

Consider 𝓅 1 the sub-augmentation of σ1 restricted to prefixes of s -it is a linear augmentation of length 2n + 2, as shown on the right hand side of Figure 23. We build the wide expansion 𝓆 1 ∈ exp(𝓅 1 ) as in the left hand side of Figure 23. It is the unique --obsessional and +-obsessional expansion of 𝓅 1 s.t. each fork of co-depth 2k has cardinality k (except for the initial move). So for any 1 ≤ k ≤ n, they are n! (n-k)! copies of q + k . Now, since ⦗|σ 1 | ⦘ = ⦗|σ 2 | ⦘, Proposition 22 entails ⦗| σ1 | ⦘ = ⦗| σ2 | ⦘. Therefore, there is 𝓆 2 ∈ exp( σ2 ) along with some isomorphism φ : (𝓆 1 ) ∼ = (𝓆 2 ). By abuse of notation, we keep referring to events of |𝓆 2 | with the same naming convention as in Figure 23, this is justified by the isomorphism φ. Now, we study the shape of 𝓆 2 . It is a tree starting with the unique initial move q - 0 , and by courtesy it cannot break the causal links from positives to negatives; so we may regard it as a tree whose nodes are the q + k 's. For each 0 ≤ k ≤ n, it has exactly n!/k! nodes of arity k (by arity, we mean the number of children in the tree structure) and by hypothesis its depth is bounded by n + 1. The essence of the situation is captured by the following simplified setting:

Fix n ∈ N. Simple trees are finite trees made of nodes k of arity k for 0 ≤ k ≤ n. We set T 0 = 0 , and for k > 0, T k is the tree with root k and k copies of T k-1 as children. If t is a simple tree, its size ♯t is its number of nodes, and its depth is the maximal number of nodes reached in a path. For instance, the depth of T k is k + 1 and

♯T k = k! k i=0 1 i! .
Now, let us consider the set Trees(n) of simple trees of depth ≤ n + 1, and having, for 2 ≤ k ≤ n, n! k! nodes k , and arbitrarily many nodes 1 and 0 . We prove:

▶ Lemma 55. Let t ∈ Trees(n) of maximal size. Then, t = T n .

Proof. Seeking a contradiction, assume t is distinct from T n . Consider a minimal node where they differ, i.e. closest to the root -say t has some p at the row corresponding to k 's in T n . If k = 0 then p > 0 and this contradicts that the depth of t is less than n. So, k ≥ 1.

If p > k, then p ≥ 2. But by minimality, t is the same as T n for all rows closer to the root, so all p for p > k are exhausted. Hence, p < k. If k = 1 and p = 0, then we may replace p with T 1 , yielding t ′ ∈ Trees(n) of size strictly greater than ♯t, contradicting maximality. Otherwise, k ≥ 2. Then the number of nodes k is fixed, there are fewer of those on this row as for T n , and they cannot occur on rows closer to the root. Therefore, there is an occurrence of k strictly deeper in t.

We then perform the transformation as in the diagram:

This yields t ′ ∈ Trees(n). But ♯t ′ > ♯t, contradicting the maximality of t. ◀ Now, from 𝓆 2 we extract a simple tree t(𝓆 2 ) ∈ Trees(n) as follows. For each 0 ≤ k ≤ n, to each q + n-k we associate a node k , with edges as in 𝓆 2 . Because all P-views in σ 2 have length lesser or equal to 2n + 2 and 𝓆 2 ∈ exp( σ2 ), t(𝓆 2 ) has depth ≤ n + 1. The constraints on the number of each node are ensured by the isomorphism φ : (𝓆 1 ) ∼ = (𝓆 2 ). Therefore t(𝓆 2 ) ∈ Trees(n), and by Lemma 55, t(𝓆 2 ) = T n .

This induces directly an isomorphism ψ between (𝓆 1 , ≤ 𝓆1 ) and (𝓆 2 , ≤ 𝓆2 ). Note that there is a priori no reason why ψ and φ would coincide, so to conclude, we must still check that ψ preserves (𝓆1) , i.e. justification pointers. Assume q - j (𝓆1) q + i . Then, q + i has arity n -i, and just(just(q + i )) = q + j of arity n -j. But then, by construction, it follows that for any move a + ∈ |𝓆 1 | of arity n -i, just(just(a)) has arity n -j. This is transported by the isomorphism φ, so this property also holds for 𝓆 2 . Now, consider ψ(q + i ) ∈ |𝓆 2 |. Its justifier is some b -∈ |𝓆 2 | such that just(b -) has arity n -j. But as arity is preserved by ψ, there is only one move with this property in the causal history of ψ(q + i ), namely ψ(q - j ). So, ψ preserves pointers.

Finally, ψ also preserves the image in the arena: by construction of 𝓆 1 , all positive moves with the same arity have the same image, and all negative moves whose justifiers have the same arity also have the same image. Hence, the image only depends on the arity, which is a property of (𝓆 1 ); and since (𝓆 1 ) and (𝓆 2 ) are isomorphic, the same holds for 𝓆 2 . Since ψ preserves arity and justifiers, it also preserves the image in the arena.

We have constructed an isomorphism ψ : 𝓆 1 ∼ = 𝓆 2 . Consider a maximal branch

q - 0 𝓆2 q + 0 𝓆2 . . . 𝓆2 q + n of 𝓆 2 .

Figure 2

 2 Figure 2 Arena nat

Figure 11

 11 Figure 11 Plays yielding positions distinguishing Kx and Ky

Figure 15

 15 Figure 15 Unique causal explanation

For

  a ∈ |𝓆|, b ∈ |𝓅| and Γ a context, we define a predicate a ∼ φ Γ b which holds if, firstly, (a) ∂ 𝓆 (a) = ∂ 𝓅 (b) and Γ ⊢ (a, b) (b) if just(a + ) ∈ dom(Γ), then just(b) ∈ cod(Γ) and Γ(just(a)) = just(b), (c) if just(a + ) ̸ ∈ dom(Γ), then just(b) ̸ ∈ cod(Γ) and φ(just(a)) = just(b), where Γ ⊢ (a, b) means that for all a ′ ∈ dom(Γ), ¬(a ′ > 𝓆 a) and for all b ′ ∈ cod(Γ), ¬(b ′ > 𝓅 b); and inductively, the following two bisimulation conditions hold:

  Lemma 28. Consider augmentations 𝓆, 𝓅, 𝓇 ∈ Aug(A), isomorphisms φ : (𝓆) ∼ = (𝓅), ψ : (𝓅) ∼ = (𝓇), events a ∈ |𝓆|, b ∈ |𝓅|, c ∈ |𝓇|, and contexts Γ, ∆. Then:

▶

  Definition 33. Consider 𝓆, 𝓅 ∈ Aug(A), φ : (𝓆) ∼ = (𝓅), and a ∈ |𝓆|, b ∈ |𝓅|.

  If a is positive, then φ(a) = ψ(a) by determinism of 𝓅, contradiction. If a is negative, then likewise we remark that ∂ 𝓅 (φ(a)) = ∂ 𝓆 (a) and ∂ 𝓅 (ψ(a)) = ∂ 𝓆 (a), contradicting --linearity of 𝓅. ◀ This lemma ensures the uniqueness condition of Definition 21. ▶ Lemma 43. Let σ : A a total finite innocent strategy and x ∈ ⦗|σ| ⦘. Then x ∈ ⦗|σ| ⦘.

  First, (a) is immediate by the definition of Γ⟨a⟩. (b). We know that if a is positive, then just(a + ) ∈ [a] - 𝓆 = dom(Γ⟨a⟩) and just(φ(a)) ∈ [φ(a)] - 𝓅 = cod(Γ⟨a⟩). Moreover just(φ(a)) = φ(just(a)) since φ is configuration-preserving. (1). Assume a + 𝓆 b -. Then φ(a) 𝓅 φ(b). By induction hypothesis, b ∼ Γ(b) φ(b). But [b -] - 𝓆 = [a] - 𝓆 ∪ {b} and [φ(b) -] - 𝓅 = [φ(a)] - 𝓅 ∪ {φ(b)}, so finally b ∼ Γ⟨a⟩∪{(b,φ(b))} φ(b) .

▶

  Immediate by induction of the co-depth of a ′ and by definition of bisimulation. ◀ ▶ Definition 47. Consider 𝓆, 𝓅 ∈ Aug(A), φ : (𝓆) ∼ = (𝓅), a ∈ |𝓆|, b ∈ |𝓅| with a ∼ φ Γ b for some context Γ. We define Γ a,b the minimal context for a ∼ φ Γ b as the restriction of Γ s.t.c ∈ dom(Γ a,b ) ⇔ ∃a ′ ∈ ↑ a, just(a ′ ) = c (a) Γ(c) ̸ = φ(c) (b)for all c ∈ |𝓆|,and symmetrically the mirror condition applies to any d ∈ |𝓅|. Lemma 48. Consider 𝓆, 𝓅 ∈ Aug(A) with φ : (𝓆) ∼ = (𝓅). Consider a ∈ |𝓆|, b ∈ |𝓅| and Γ, Γ ′ two contexts such that a ∼ φ Γ b and a ∼ φ Γ ′ b. Then Γ a,b = Γ ′ a,b . Moreover, Γ a,b is the minimal (for inclusion) context s.t. a ∼ φ Γ a,b b. Proof. The equality comes from Lemma 46 and the definition of Γ a,b and Γ ′ a,b . By induction, a ∼ φ Γ a,b b, since we can safely remove from dom(Γ) all c that are never "used", i.e. such that there exists no a ′ ∈ ↑ a having c as pointer; and all c such that Γ(c) = φ(c), because then we can use condition (c) of Definition 26 instead of condition (b). Finally, for any context Γ ′′ such that a ∼ φ Γ ′′ b, we have Γ a,b = Γ ′′ a,b ⊆ Γ ′′ , so Γ a,b is minimal for inclusion. ◀ This lemma allows us to write the minimal context for a, b without mentioning Γ.

▶

  Lemma 49. Consider 𝓆, 𝓅, 𝓇 ∈ Aug(A), φ : (𝓆) ∼ = (𝓅) and ψ : (𝓅) ∼ = (𝓇), and: a ≈ φ b b ≈ ψ c for some a ∈ |𝓆|, b ∈ |𝓅|, and c ∈ |𝓇|. Then, we also have a ≈ ψ•φ c. Proof. Consider Γ 1 and Γ 2 the minimal contexts such that a ∼ φ Γ1 b and b ∼ ψ Γ2 c. If cod(Γ 1 ) = dom(Γ 2 ), the result is immediate by Lemma 28: we get a ∼ ψ•φ Γ2•Γ1 c with, for any e ∈ dom(Γ 1 ) = dom(Γ 2 • Γ 1 ), ψ(φ(just(e))) = ψ(just(Γ 1 (e))) = just(Γ 2 (Γ 1 (e))) so Γ 2 • Γ 1 preserves pointers and a ≈ ψ•φ c. Now, assume there exists e ∈ cod(Γ 1 ) such that e / ∈ dom(Γ 2 ). Since Γ 1 is minimal, there exists b ′ ∈ ↑ b such that just(b ′ ) = e. By b ∼ ψ Γ2 c and Lemma 46, there exists a matching c ′ ∈ ↑ c such that b ′ ∼ ψ Γ2∪∆ , with ∆ the negative moves between b and b ′ , paired with the negative moves between c and c ′ . Since e ∈ cod(Γ 1 ), ¬(e ≥ 𝓅 b), so e / ∈ dom(∆). Hence, just(c ′ ) = ψ(e) and ψ(e) / ∈ cod(Γ 2 ). So we can write b ∼ ψ Γ2∪{(e,ψ(e))} c

▶

  allows us to prove equivalence properties for the clone relation. Lemma 50. Consider 𝓆, 𝓅, 𝓇 ∈ Aug(A) augmentations, with φ : (𝓆) ∼ = (𝓅) and ψ : (𝓅) ∼ = (𝓇) two isomorphisms, and events a ∈ |𝓆|, b ∈ |𝓅|, c ∈ |𝓇|: reflexivity: a ≈ id a, transitivity: if a ≈ φ b and b

1 𝓆 b + 1 and a - 2 𝓆 b + 2 , b 1 ≈ b 2 .

 12212 Proof. If X = {init(𝓆)}, a 1 = a 2 and the result is immediate by determinism and reflexivity. Otherwise, we note b the predecessor of both a 1 and a 2 for ≤ 𝓆 . First, we prove that b 1 and b 2 are bisimilar. Since 𝓆 is a --obsessional expansion of 𝓅, there exists a (unique, by Lemma 42) morphism φ : 𝓆 → 𝓅. By Lemma 45, b 1 ∼ Γ(b1) φ(b 1 ) and b 2 ∼ Γ(b2) φ(b 2 ) .

Figure 23

 23 Figure 23 Wide expansion of a P-view

  for all a 1 , a 2 ∈ |x|, if a 1 x a 2 then ∂ x (a 1 ) A ∂ x (a 2 ).

	is a finite tree, and ∂ x : |x| → |A|, the display map, is a labeling function s.t.:
	minimality-respecting: for all a ∈ |x|, a is ≤ x -minimal iff ∂ x (a) is ≤ A -minimal,
	causality-preserving:

.

  If. We simply construct φ : 𝓆 → 𝓅 for all a ∈ |𝓆| by induction on ≤ 𝓆 . The image is provided by bisimulation, its uniqueness by determinism and --linearity.Only if. For φ : 𝓆 → 𝓅 and a ∈ |𝓆|, write [a] -𝓆 = {a ′ ∈ |𝓆| | a ′ ≤ 𝓆 a & λ(a ′ ) = -};it is totally ordered by ≤ 𝓆 as 𝓆 is forestial. From the conditions on φ, it is direct that it induces an order-iso [a] - Γ⟨a⟩ φ(a) for all a ∈ |𝓆|. We then apply this to init(𝓆). ◀This vindicates Definition 29. But for (1), we must compose two kinds of bisimulations, following Definitions 26 and 29. Fortunately, whenever both definitions apply, they coincide:▶Lemma 31. Consider 𝓆, 𝓅 ∈ Aug(A), and φ : (𝓆) ∼ = (𝓅). Then, 𝓆 ∼ φ 𝓅 iff 𝓆 ∼ 𝓅. Proof. If. Straightforward from Definitions 26 and 29: case (c) is never used.Only if. We actually prove that for all a ∈ |𝓆|, b ∈ |𝓅|, for all context Γ which is complete in the sense that [a] -

	𝓆	∼ = [φ(a)] -𝓅 , i.e. a context Γ⟨a⟩ : [a] -𝓆	∼ = [φ(a)] -𝓅 . Then, by Lemma 45, we
	obtain a ∼

𝓆 ⊆ dom(Γ) and [b] - 𝓅

  18 A set of clones switching pointers compositional properties of clones are more challenging. Nevertheless, via a canonical form for contexts and leveraging Lemma 28, we show that a ≈ id a, that a ≈ φ b and b ≈ ψ c imply a ≈ ψ•φ c, and that a ≈ φ b implies b ≈ φ -1 a whenever these typecheck -see Appendix B.2. Instantiating Definition 33 with 𝓆 = 𝓅 and φ = id, we get an equivalence relation ≈ on |𝓆|. Moreover, we have the crucial property that forks generate clones (see Appendix B.2): By Lemma 34, if a clone class includes a positive move, it also has all its cousins triggered by the same fork -so clone classes may be partitioned following forks: ▶ Lemma 35. Let 𝓆 be a characteristic expansion of causal strategy 𝓅, and Y a clone class of positive events in |𝓆|, with ♯Y = i∈I 2 i for I ⊆ N finite. Then, for all

▶ Lemma 34. Consider 𝓆 a --obsessional expansion of causal strategy 𝓅 on arena A.

Then, for all a - 1 , a - 2 ∈ X ∈ Fork(𝓆), for all a -

1 𝓆 b + 1 and a - 2 𝓆 b + 2 , b 1 ≈ b 2 .

Proofs from Section 4 B.1 Compositional Properties of Bisimulations (Section 4.3) In

  We can see s := s 1 . . . s n , with pointers imported from (𝓆) (i.e. (s) = (𝓆)), as a play on arena (𝓆). Then for any 1 ≤ i ≤ n, it holds that ⌜s ≤i ⌝ coincides with [s i ] 𝓆 , the causal dependency of s i in 𝓆 (clear by induction on i).Writing ∂ 𝓆 (s) = ∂ 𝓆 (s 1 ) . . . ∂ 𝓆 (s n ) with pointers imported from (𝓆), it follows that ∂ 𝓆 (s) ∈ Plays(A) and ⌜(∂ 𝓆 (s)) ≤i ⌝ ∈ ⌜ ⌜σ⌝ ⌝ (by definition of σ). Hence ∂ 𝓆 (s) ∈ σ by innocence, with (∂ 𝓆 (s)) ∼ = (s). Therefore, (∂ 𝓆 (s)) ∼ = (𝓆), i.e. ⦗𝓆⦘ = ⦗∂ 𝓆 (s)⦘ ∈ ⦗|σ| ⦘. ◀ ▶ Proposition 22.For any total finite innocent strategy σ : A, we have ⦗|σ| ⦘ = ⦗|σ| ⦘. By induction on the co-depth of a ∈ |𝓆|. We must check that a ∼ Γ⟨a⟩ φ(a).

	Proof. Immediate by Lemmas 43 and 44.	◀
	B	Positional Injectivity:

this section, we prove some technical lemmas about bisimulations. Recall that for 𝓆 ∈ Aug(A), a ∈ |𝓆| there is an order-iso Γ⟨a⟩ :

[a] - 𝓆 ∼ = [φ(a)] - 𝓅 ,

with [a] - 𝓆 the totally ordered set of negative dependencies of a in 𝓆. Recall also that the co-depth of a ∈ |𝓆| is the maximal length of a causal chain a = a 1 𝓆 . . . 𝓆 a k in 𝓆. ▶ Lemma 45. Consider 𝓆, 𝓅 ∈ Aug(A) where 𝓅 is a causal strategy and 𝓆 ∈ exp(𝓅) is a --obsessional expansion with the morphism φ : 𝓆 → 𝓅. Then a ∼ Γ⟨a⟩ φ(a) .

Proof.

  Since 𝓆 2 ∈ exp( σ2 ), we have a morphism ν : 𝓆 2 → σ2 . Its image by ν iss 1 σ2 s 1 s 2 σ2 . . . σ2 s 1 . . . s 2n+2a sequence of prefixes of a P-view s 1 . . . s 2n+2 , which, using that 𝓆 1 is an expansion of 𝓅 1 and ψ : 𝓆 1 ∼ = 𝓆 2 , is immediately seen to be exactly s. Hence, s ∈ σ 2 as claimed.

Acknowledgements We thank the reviewers, whose comments greatly helped improve the paper.

1

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

By --linearity of 𝓅, we know that φ(a 1 ) = φ(a 2 ), which implies φ(b 1 ) = φ(b 2 ) by determinism. So cod(Γ(b 1 )) = cod(Γ(b 2 )), and by Lemma 28,

Writing Γ 1 := Γ(b 1 ), Γ 2 := Γ(b 2 ) and Γ := Γ -1 2 • Γ 1 , it remains to check that Γ preserves pointers. Consider c ∈ dom(Γ) = [b 1 ] - 𝓆 , either c = a 1 or c ≤ 𝓆 b. If c = a 1 , then Γ 1 (a 1 ) = φ(a 1 ) = Γ 2 (a 2 ), so Γ(a 1 ) = a 2 (and both have the same pointer b by courtesy). Otherwise, c ≤ 𝓆 b, so c ∈ dom(Γ 2 ) and Γ 1 (c) = φ(c) = Γ 2 (c), hence Γ(c) = c. In both cases, Γ preserves pointers, so finally b 1 ≈ b 2 . ◀

B.3 Positional Injectivity (Section 4.5)

In this section, we prove additional lemmas needed in the proof of Lemma 36.

▶ Lemma 51. Consider 𝓆, 𝓅 ∈ Aug(A) two augmentations such that there exists an isomorphism φ : Proof. Assume, seeking a contradiction, that the minimal context Γ has at least two distinct elements c 1 , c 2 ∈ dom(Γ). First, we can remark that since a ≈ b, there exists Γ ′ a pointerspreserving context such that a ∼ Γ ′ b, and since Γ is a restriction of Γ ′ , Γ also preserves pointers.

By condition (a) of Definition 47, c 1 ≤ 𝓆 a and c 2 ≤ 𝓆 a. Therefore, c 1 ≤ 𝓆 c 2 or c 2 ≤ 𝓆 c 1assume w.l.o.g. that it is the former. By courtesy, just(c 1 ) ≤ 𝓆 just(c 2 ) as well. For the same reason, Γ(c 1 )

If it is the latter, this entails that just(Γ(c 2 )) ≤ 𝓆 just(Γ(c 1 )) by courtesy; i.e., since Γ preserves pointers, just(c 2 ) ≤ 𝓆 just(c 1 ). So just(c 1 ) = just(c 2 ), and because c 1 , c 2 ≤ 𝓆 a, we have c 1 = c 2 , contradiction.

So, Γ(c 1 ) ≤ 𝓆 Γ(c 2 ), and Γ(c 1 ) ̸ = Γ(c 2 ) by hypothesis. By courtesy, this entails that Γ(c 1 ) ≤ 𝓆 just(Γ(c 2 )). Likewise, c 1 ≤ 𝓆 c 2 entails c 1 ≤ 𝓆 just(c 2 ). Moreover, Γ preserves pointers, so just(c 2 ) = just(Γ(c 2 )). Hence, we have both

Proof. First, remark that ∂ 𝓆 (a) = ∂ 𝓅 (φ(a)) and φ(just(a)) = just(φ(a)).

For any i ∈ I, 1 ≤ j ≤ 2 i , let Γ i,j be the minimal context for b i,j and φ(b i,j ). Such a context exists since either b i,j has no successors, and by (4) neither does φ(b i,j ), either b i,j has only one (by determinism) and c i,j ≈ φ d i,j by (3). In both cases, b i,j ≈ φ φ(b i,j ).

We wish to take the union of all Γ i,j as the context for a and φ(a), but this is only possible if they are compatible. More precisely, we must ensure that for all e ∈ 𝓆, i, k ∈ I,

having both e as justifier, then their matching

) also have the same justifier. This can only be a problem if e appears in dom(Γ i,j ) or in dom(Γ k,l ) as otherwise both justifiers are φ(e).

For all i, j, Γ i,j has either one or zero element by Lemma 53. If all Γ i,j are empty, we can directly lift the clone relation to a. Otherwise, consider i, j s.t. Γ i,j :

, since e i,j and f i,j have the same justifier through φ and the only e For b i,j ∼ φ Γi,j φ(b i,j ) and b k,l ∼ φ Γ k,l φ(b k,l ) to be compatible, we need just(d ′ k,l ) = f i,j . But since Γ i,j preserves pointers, φ(just(e i,j )) = just(f i,j ) .

Putting both equalities together, we obtain

which is a fully ordered set for ≤ 𝓅 , so just(d ′ k,l ) and f i,j are comparable. Moreover, they are negative, so by courtesy

where pred is the predecessor for ≤ 𝓅 . Hence, just(d ′ k,l ) = f i,j (see Figure 22, where represents 𝓆 , • • • represents (𝓆) , and → represents ≤ 𝓆 (and the same applies for 𝓅)).

So all contexts Γ i,j are compatible. Writing Γ = ∪ i,j Γ i,j it follows that b i,j ∼ φ Γ φ(b i,j ) via Lemma 52; which entails that a ∼ φ Γ φ(a) by two steps of the bisimulation game. This implies a ≈ φ φ(a) since all Γ i,j preserve pointers. ◀

just(e i,j ) + e i,j a + E s s z