Paul-André Melliès

Asynchronous games 2 The true concurrency of innocence

In game semantics, the higher-order value passing mechanisms of the λ-calculus are decomposed as sequences of atomic actions exchanged by a Player and its Opponent. Seen from this angle, game semantics is reminiscent of trace semantics in concurrency theory, where a process is identified to the sequences of requests it generates in the course of time. Asynchronous game semantics is an attempt to bridge the gap between the two subjects, and to see mainstream game semantics as a refined and interactive form of trace semantics. Asynchronous games are positional games played on Mazurkiewicz traces, which reformulate (and generalize) the familiar notion of arena game. The interleaving semantics of λ-terms, expressed as innocent strategies, may be analyzed in this framework, in the perspective of true concurrency. The analysis reveals that innocent strategies are positional strategies regulated by forward and backward confluence properties. This captures, we believe, the essence of innocence. We conclude the article by defining a non uniform variant of the λ-calculus, in which the game semantics of a λ-term is formulated directly as a trace semantics, performing the syntactic exploration or parsing of that λ-term.

Introduction

Game semantics has taught us the art of converting the higher-order value passing mechanisms of the λ-calculus into sequences of atomic actions exchanged by a Player and its Opponent in the course of time. This metamorphosis of higherorder syntax has significantly sharpened our understanding of the simply-typed λ-calculus, either as a pure calculus, or as a calculus extended with programming features like recursion, conditional branching, local control, local states, references, non determinism, probabilistic choice, etc.

Game semantics is reminiscent of trace semantics in concurrency theory. There, a process is described as a symbolic device which interacts with its environment 1 This work has been partly supported by the FNS ACI Géométrie du Calcul (GEOCAL). Postal address: Equipe PPS, Université Paris VII, 2 place Jussieu, Case 7014, 75251 Paris Cedex 05, FRANCE. Email address: mellies@pps.jussieu.fr Preprint submitted to Theoretical Computer Science by emitting or receiving requests. A sequence of such requests is called a trace. The trace semantics of a process π is defined as the set of traces generated by the process. In many situations, this semantics characterizes the contextual behaviour of the process. In other situations, it is refined into a bisimulation semantics.

Game semantics develops pretty much the same story for the λ-calculus. The terminology changes of course: requests are called moves, and traces are called plays. But everything works arguably as in trace semantics: the semantics of a λ-term M of type A is the set of plays σ generated by the λ-term M ; and this set of plays σ characterizes the contextual behaviour of the λ-term. The novelty of game semantics, not present in trace semantics, is that the type A defines a game, and that the set of plays σ generated by the λ-term M defines a strategy of that game.

The main thesis of this work is that game semantics is really the trace semantics of the λ-calculus -and even more than that: its Mazurkiewicz trace semantics. The thesis is quite unexpected, since the λ-calculus is often considered as the historical paradigm of sequentiality, whereas Mazurkiewicz traces describe truly concurrent mechanisms. The thesis is also far from immediate. It prescribes to reevaluate a large part of the conceptual and technical choices accepted today in game semantics... in order to bridge the gap with trace semantics and concurrency theory. Three issues are raised here:

(1) The treatment of duplication in mainstream game semantics (eg. in arena games) distorts the bond with trace semantics -in particular with Mazurkiewicz traces -by adding justification pointers to traces. This prompts us to revisit this specific treatment of duplication in our first article on asynchronous games [START_REF] Melliès | Asynchronous games 1: a group-theoretic formulation of uniformity[END_REF]. We recall below the group-theoretic formulation of arena games operated there in order to "eliminate" these justification pointers -or rather, in order to reunderstand them as copy indices modulo group action. (2) Thirty years ago, Antoni Mazurkiewicz developed a theory of asynchronous traces in which the interleaving semantics and the true concurrency semantics of a concurrent computation are related by permuting the order of independent events in sequences of transitions. On the other hand, current game semantics provides an interleaving semantics of the λ-calculus, in which λ-terms are expressed as innocent strategies. What is the true concurrency counterpart of this interleaving semantics? The task of this second article on asynchronous games is precisely to answer this question in a satisfactory way. (3) Ten years ago, a series of full abstraction theorems for PCF were obtained by characterizing the interactive behaviour of λ-terms as either innocent, or history-free strategies, see [START_REF] Abramsky | Full abstraction for PCF[END_REF][START_REF] Hyland | On full abstraction for PCF: I, II and III[END_REF][START_REF] Nickau | Hereditarily sequential functionals[END_REF]. We believe that the present work is another significant stage in the "full abstraction" program initiated by Robin Milner [START_REF] Milner | Fully abstract models of typed lambda-calculi[END_REF]. For the first time indeed, we do not simply characterize, but also derive the syntax of λ-terms from elementary causality principles, expressed in asynchronous transition systems. This reconstruction requires the mediation of [START_REF] Melliès | Asynchronous games 1: a group-theoretic formulation of uniformity[END_REF] and of its indexed treatment of threads. This leads us to an in-dexed and non-uniform λ-calculus, from which the usual λ-calculus follows by group-theoretic principles. In this non-uniform variant of the λ-calculus, the game semantics of a λ-term may be directly formulated as a trace semantics performing the syntactic exploration or parsing of the λ-term.

The treatment of duplication. The language of traces is limited, but sufficient to interpret the affine fragment of the λ-calculus, in which every variable occurs at most once in a λ-term. In this fragment, every trace (= play) generated by a λ-term is an alternating sequence of received requests (= Opponent moves) and emitted requests (= Player moves). And a request appears at most once in a trace.

In order to extend the affine fragment to the whole λ-calculus, one needs to handle the duplication mechanisms semantically. This is a delicate matter. Several solutions have been considered in the literature already, and coexist today. By way of illustration, consider the λ-term chosen by Alonzo Church in order to interpret the natural number 2: M = λf.λx.f f x.

Placed in front of two λ-terms P and Q, the λ-term M duplicates its first argument P , and applies it twice to its second argument Q. This is performed syntactically by two β-reductions:

M P Q -→ β (λx.P P x)Q -→ β P P Q.

Obviously, the remainder of the computation depends on the λ-terms P and Q.

The game-theoretic interpretation of the λ-term M has to anticipate all cases. This requires the semantics to manipulate several threads of the λ-term P simultaneously -and possibly many more than the two copies P (1) and P [START_REF] Abramsky | Full abstraction for PCF[END_REF] appearing in the λterm P (1) P (2) Q, typically when the λ-term P (1) uses its first argument P (2) several times in the remainder of the computation. Now, the difficulty is that each thread of P should be clearly distinguished. A compact and elegant solution has been devised by Martin Hyland, Luke Ong and Hanno Nickau in the framework of arena games [START_REF] Hyland | On full abstraction for PCF: I, II and III[END_REF][START_REF] Nickau | Hereditarily sequential functionals[END_REF]. We recall that an arena is a forest, whose nodes are the moves of the game, and whose branches m n are oriented to express that the move m justifies the move n. A move n is called initial when it is a root of the forest, or alternatively, when there is no move m such that m n. A justified play is then defined as a pair (m 1 • • • m k , ϕ) consisting of a sequence of moves m 1 • • • m k and a partial function ϕ : {1, ..., k} → {1, ..., k} providing the so-called pointer structure of the play. The partial function ϕ associates to every occurrence i of a non-initial move m i the occurrence ϕ(i) of a move m ϕ(i) such that m ϕ(i) m i . One requires that ϕ(i) < i in order to ensure that the justifying move m ϕ(i) occurs before the justified move m i . Finally, the partial function ϕ is never defined on any occurrence i of an initial move m i .

The pointer structure ϕ provides the necessary information to distinguish the several threads of a λ-term in the course of interaction -typically the several threads or copies of P in example [START_REF] Abramsky | Sequentiality vs. concurrency in games and logic[END_REF]. The pointer structure ϕ is conveniently represented by drawing "backward pointers" between occurrences of the sequence m 1 • • • m k . By way of illustration, consider the arena m n p in which the only initial move is m. A typical justified play (s, ϕ) of this arena is represented graphically as:

m • n T T • p S S • n x x • p Y Y • n { { • p c c • m • n T T • p. | | (2)
Because adding justification pointers distorts the bond with trace semantics, in particular with Mazurkiewicz traces, we shift in [START_REF] Melliès | Asynchronous games 1: a group-theoretic formulation of uniformity[END_REF] to another management principle based on thread indexing, already considered in [START_REF] Abramsky | Full abstraction for PCF[END_REF][START_REF] Hyland | Game semantics[END_REF]. The idea is to assign to each copy of the λ-term P in example (1) a natural number k ∈ N (its index) which characterizes the thread among the other copies of P . In the case of the justified play [START_REF] Abramsky | Full abstraction for PCF[END_REF], this amounts to (a) adding a dumb move in order to justify the initial moves of the sequence, (b) indexing every justification pointer of the resulting sequence with a natural number:

• m 17 T T • n 5 T T • p 69 S S • n 4 x x • p 20 Y Y • n 1 y y • p 7 c c • m 5 x x • n 70 T T • p 4 | | (3)
then finally (c) encoding the sequence (3) as the sequence of indexed moves below:

m 17 • n 17,5 • p 17,5,69 • n 17,4 • p 17,4,20 • n 17,1 • p 17,5,7 • m 5 • n 5,70 • p 17,4,4 . (4)
Obviously, the translation of a justified play (s, ϕ) depends on the choice of indices put on its justification pointers. Had we not taken sides with trace semantics and concurrency theory, we would be tempted (as most people do in fact) to retract to the notation (2) which is arguably simpler than its translation (4). But we carry on instead, and prompted by our task, decide to regulate the indexing by asking that two justification pointers starting from different occurrences i and j of the same move n, and ending on the same occurrence ϕ(i) = ϕ(j), receive different indices k and k . This indexing policy ensures that every indexed move occurs at most once in the sequence [START_REF] Abramsky | Game semantics[END_REF]. In this way, we are back to the simplicity of the affine fragment of the λ-calculus.

An interesting point remains to be understood: what can be said about two different encodings of the same justified play? The first article of our series [START_REF] Melliès | Asynchronous games 1: a group-theoretic formulation of uniformity[END_REF] clarifies this point in the following way. Every game is equipped with a left and a right group action on moves:

G × M -→ M (g, m) → g m M × H -→ M (m, h) → m h (5)
where M denotes the set of indexed moves, and G and H the two groups acting on that set of moves. Intuitively, the left (resp. right) group action operates on a move m k 0 ,...,k j by altering the indices k 2i+1 assigned by Player (resp. the indices k 2i assigned by Opponent). Consequently, the orbit of a move m k 0 ,...,k j modulo a combination of the left and right group actions is precisely the set of all moves of the form m k 0 ,...,k j . Now, the left and right group action on moves induces a left and a right group action on plays, defined in a pointwise manner:

g (m 1 • • • m k ) = (g m 1 ) • • • (g m k ) (m 1 • • • m k ) h = (m 1 h) • • • (m k h) (6)
It appears that the justified plays of the original arena game coincide precisely with the orbits of plays modulo left and right group action. Typically, the justified play (2) is just the play (4) modulo pointwise group action [START_REF] Baader | Term Rewriting and All That[END_REF]. One significant contribution of the present article is to reveal that the two group actions (5) are inherently syntactical group actions on a non-uniform variant of the λ-calculus, see Section 6 for details.

Asynchronous traces. After these necessary preliminaries on duplication and thread indexing, we shift to the core of this article: the comparison of true concurrency and interleaving in game semantics. Let us recall first a few principles of trace semantics in concurrency theory. Two requests a and b starting from a process π are called independent when they can be emitted or received by the process π in any order, without interference. Independence of the two requests a and b is represented graphically by tiling the two sequences a • b and b • a in the 2-dimensional diagram below:

π π 1 b > > | | | | | ∼ π 2 a BB B B B π b = = z z z z z a a a D D D D D (7)
The interleaving semantics of a process π is defined as the set of traces it generates in the course of time. The true concurrency semantics of the process is deduced from this by quotienting the traces modulo the homotopy equivalence ∼ obtained by permuting independent requests. Expressing true concurrency by permuting the order of events in a symbolic trajectory stands among the fundamentals of concurrency theory. The idea originates from the work of Antoni Mazurkiewicz on asynchronous traces over a partially ordered alphabet [START_REF] Mazurkiewicz | Concurrent program schemes and their interpretations[END_REF][START_REF] Mazurkiewicz | Introduction to trace theory[END_REF] and leads to the notion of asynchronous transition system developed in [START_REF] Panangaden | Stability and sequentiality in data flow networks[END_REF][START_REF] Kuske | Non deterministic automata with concurrency relations and domains[END_REF][START_REF] Winskel | Models for concurrency[END_REF]. The same idea reappears (independently) in Jean-Jacques Lévy's description of the λ-calculus [START_REF] Lévy | Réductions correctes et optimales dans le lambda-calcul[END_REF], and plays a key role in the author's work on axiomatic rewriting theory [START_REF] Melliès | Axiomatic rewriting 4: a stability theorem in rewriting theory[END_REF][START_REF] Melliès | Axiomatic rewriting 6: Residual theory revisited[END_REF].

The principle may be generalized to n-dimensional transition systems generated by cubical sets -where permutation of events amounts to directed homotopyas advocated by Vaughn Pratt and Eric Goubault in [START_REF] Pratt | Modeling concurrency with geometry[END_REF][START_REF] Goubault | Geometry and concurrency: A user's guide[END_REF].

In comparison to concurrency theory and rewriting theory, mainstream game semantics is still very much 1-dimensional. By way of illustration, take the sequential boolean game B, starting by an Opponent question q followed by a Player answer true or false:

false _ _ ? ? ? ? ? ? true ? ?

q O O (8)
The plays of the tensor product B ⊗ B are obtained by interleaving the plays of the two instances B 1 and B 2 of the boolean game B. Thus, (a fragment of) the game B ⊗ B defines a tree which looks exactly like this:

false 2
_ _ ? ? ? true 1 ? ?

q 2
_ _ ? ? ? q 1 ? ?

true 1
_ _ ? ? ? false 2 ? ?

q 1 g g O O O O O O q 2 7 7 o o o o o o (9)
We observe in [START_REF] Melliès | Sequential algorithms and strongly stable functions[END_REF] that the two plays in [START_REF] Berger | Sequentiality and the pi-calculus (extended abstract)[END_REF] are different from a procedural point of view, but equivalent from an extensional point of view -since both of them realize the "extensional value" (true, f alse). We thus bend the two paths, and obtain a permutation tile with the shape of a 2-dimensional octagon:

false 2 7 7 o o o o o o o o true 1 g g O O O O O O O O q 2 ? ? q 1
_ _ ? ? ? ? ?

true 1
_ _ ? ? ? ? ?

false 2 ? ? q 1 g g O O O O O O O O q 2 7 7 o o o o o o o o (10)
By doing so, we shift from the familiar sequential games played on decision trees, to a new kind of sequential games played on directed acyclic graphs (dags). We analyze in this way the extensional content of sequential games, and deliver an alternative (and game-theoretic) proof of Thomas Ehrhard's collapse theorem [START_REF] Ehrhard | A relative definability result for strongly stable functions and some corollaries[END_REF].

The extensional framework developed in [START_REF] Melliès | Sequential algorithms and strongly stable functions[END_REF] is extremely instructive, but not entirely satisfactory because the permutation tiles are "global" -that is, they involve more than two permuting moves in general. In contrast, the asynchronous games developed in the present article admit only "local" permutation tiles, permuting two moves, and similar to tile [START_REF] Baillot | Approches dynamiques en sémantique de la logique linéaire: jeux et géometrie de l'interaction[END_REF]. By way of illustration, shifting to asynchronous games decomposes the "global" tile [START_REF] Bezem | Abstract reduction systems[END_REF] ? ?

∼ q 1? ? ? _ _ ? ? ?

false 2 ? ? q 1
_ _ ? ? ? ? ? ? ? q 2 ? ? [START_REF] Danos | Games semantics and abstract machines[END_REF] Note that shifting from a directed acyclic graph in Diagram [START_REF] Bezem | Abstract reduction systems[END_REF] to an asynchronous game in Diagram [START_REF] Danos | Games semantics and abstract machines[END_REF] induces concurrent plays like q 1 • q 2 in the model. This indicates that a satisfactory theory of sequentiality requires a truly concurrent background, in which sequential plays like q 1 • true 1 • q 2 • false 2 coexist with concurrent plays like q 1 • q 2 or q 1 • q 2 • true 1 • false 2 .

The non-uniform λ-calculus. Here comes the most surprising, most difficult, and maybe most controversial, part of the paper. An asynchronous game is defined in Section 2 as an event structure whose events are polarized +1 for Player moves and -1 for Opponent moves. This polarization of events gives rise to a new class of events m • n consisting of an Opponent move m followed by a Player move n. We call OP -moves any such pair of moves. Just like ordinary moves, two OP -moves m 1 • n 1 and m 2 • n 2 may be permuted in a play, in the following way:

The permutation diagram [START_REF] Ehrhard | A relative definability result for strongly stable functions and some corollaries[END_REF] induces a homotopy relation ∼ OP between plays. The dual relation ∼ P O is defined symmetrically, by permuting P O-moves m • n together, where by P O-move m • n we mean a Player move m followed by an Opponent move n, see Section 2 for a formal definition. Note that both ∼ OP and ∼ P O preserve alternation of plays. Now, there is a well-established theory of stable asynchronous transition systems in which every equivalence class modulo homotopy ∼ may be represented as an event structure of so-called canonical representatives, see for instance [START_REF] Panangaden | Stability and sequentiality in data flow networks[END_REF][START_REF] Kuske | Non deterministic automata with concurrency relations and domains[END_REF][START_REF] Melliès | Axiomatic rewriting 4: a stability theorem in rewriting theory[END_REF]. The canonical representative of a transition a in a given sequence of transitions s • a describes the cascade of transitions necessary in s in order to enable the transition a. More formally, a sequence of transitions t • a is a canonical representative of a sequence of transitions s • a precisely when:

(1) s • a ∼ t • a • t for some sequence of transitions t , and (2) whenever t ∼ t • b, the transition a cannot be permuted before the transition b.

The stability property ensures that this canonical representative t • a of the transition a is unique, modulo homotopy equivalence ∼ on the sequence t. Now, the asynchronous transition system with OP -moves as transitions happens to be stable. This implies that every OP -move m • n in an alternating play s • m • n has a unique canonical representative of the form t • m • n, modulo homotopy equivalence ∼ OP on the sequence t. Strikingly, this canonical representative coincides with the so-called Player view s • m • n of the play s • m • n defined by Martin Hyland, Luke Ong and Hanno Nickau in the framework of arena games [START_REF] Hyland | On full abstraction for PCF: I, II and III[END_REF][START_REF] Nickau | Hereditarily sequential functionals[END_REF] and adapted to the more "concurrent" framework of asynchronous games in Section 3. Now, Vincent Danos, Hugo Herbelin and Laurent Regnier observe in their work on arena games that every Player view of a justified play (s, φ) corresponds to the branch of an η-long Böhm tree, see [START_REF] Danos | Games semantics and abstract machines[END_REF] for details. The correspondence adapts smoothly to the indexed treatment of threads devised by the author in [START_REF] Melliès | Asynchronous games 1: a group-theoretic formulation of uniformity[END_REF]. In this situation, every Player view of a play s corresponds to the branch of a non-uniform η-long Böhm tree. From this results a non-uniform λ-calculus (defined in Section 6) with a remarkable feature: the strategy σ associated to a non-uniform λ-term P may be alternatively formulated as a trace semantics performing the syntactic exploration or parsing of the λ-term P .

In this way, we reconstruct by rational means a non-uniform variant of the λcalculus, starting from purely diagrammatic reflections on Mazurkiewicz traces and two-player games. The simply-typed λ-calculus itself (or more exactly, the familiar notion of η-long Böhm tree) follows by the group-theoretic techniques elaborated in [START_REF] Melliès | Asynchronous games 1: a group-theoretic formulation of uniformity[END_REF] and further studied in Section 6. Hence, a diagrammatic and integrated framework emerges here, liberated from syntax, in which the evaluation of a λterm P against a context E[-] performs a symbolic trajectory s : * x

• whose homotopy class modulo ∼ OP expresses the syntactic subterm of P consumed during the evaluation of E[P ],

• whose homotopy class modulo ∼ P O expresses the syntactic subterm of E [-] consumed during the evaluation of E[P ],

• whose homotopy class modulo ∼ coincides with the target position x, and provides the type (or formula) of what remains unconsumed after the evaluation.

Related works. The idea of relating a dynamic and a static semantics of linear logic is formulated for the first time by Patrick Baillot, Vincent Danos, Thomas Ehrhard and Laurent Regnier in their early work on "timeless games" [START_REF] Baillot | Timeless games[END_REF] and carried on by Patrick Baillot in his PhD thesis [START_REF] Baillot | Approches dynamiques en sémantique de la logique linéaire: jeux et géometrie de l'interaction[END_REF]. The idea reappears then in the concurrent game model of linear logic introduced by Samson Abramsky and the author [START_REF] Abramsky | Concurrent games and full completeness[END_REF]. There, concurrent games are defined as complete lattices of positions, and concurrent strategies as closure operators on these lattices. As a closure operator, every strategy is at the same time an increasing function on positions (the dynamic point of view) and a set of positions (the static point of view). The present paper is the result of a long journey (five years!) to connect this concurrent game semantics to mainstream sequential game semantics. See also the discussion in [START_REF] Abramsky | Sequentiality vs. concurrency in games and logic[END_REF].

Martin Hyland and Andrea Schalk develop in [START_REF] Hyland | Games on graphs and sequentially realizable functionals[END_REF] a notion of games on graphs quite similar to the constructions presented here and in [START_REF] Melliès | Sequential algorithms and strongly stable functions[END_REF]. One difference is the treatment of duplication: backtracking in [START_REF] Hyland | Games on graphs and sequentially realizable functionals[END_REF][START_REF] Melliès | Sequential algorithms and strongly stable functions[END_REF], repetitive and indexed here. From this choice follows that the permutation tiles are global in [START_REF] Hyland | Games on graphs and sequentially realizable functionals[END_REF][START_REF] Melliès | Sequential algorithms and strongly stable functions[END_REF] and local here. Another difference is that our positions are defined as downward-closed subsets of moves.

This article reformulates arena games and innocent strategies using concepts imported from concurrency theory. Conversely, much work has been devoted in the process calculus community to clarify the connections between the π-calculus and the λ-calculus -in particular by Martin Berger, Kohei Honda and Nobuko Yoshida in their work on sequentiality [START_REF] Berger | Sequentiality and the pi-calculus (extended abstract)[END_REF]. This offers an opportunity for an elegant synthesis of the two subjects, using asynchronous games, which we are currently investigating. Besides, several game models of concurrent programming languages have been already formulated in the interleaving framework of arena games [START_REF] Laird | A game semantics of Idealized CSP[END_REF][START_REF] Ghica | Angelic semantics of fine-grained concurrency[END_REF]. It will be certainly instructive to recast them inside our asynchronous framework.

Outline. In the remainder of the article, we define our notion of asynchronous game (Section 2) and adapt the usual definition of innocent strategy to our setting (Section 3). We then characterize the innocent strategies in two ways: diagrammatically (Section 4) and positionally (Section 5). This leads to a non-uniform variant of the λ-calculus, for which we define a trace semantics, and which we relate to the usual λ-calculus (Section 6). Finally, we describe a series of possible refinements of asynchronous games (Section 7) and conclude (Section 8).

We choose the simplest possible definition of asynchronous game, in which the only relation between moves is an order relation ≤ which reformulates the justification structure of arena games. This is enough to describe the language PCF, a simplytyped λ-calculus enriched with arithmetic, conditional branching, and recursion. A series of more expressive versions of the semantics are discussed in section 7.

Event structures. An event structure is an ordered set (M, ≤) such that every element m ∈ M defines a finite downward-closed subset

m ↓ = {n ∈ M | n ≤ m}.
Asynchronous games. An asynchronous game is a triple A = (M A , ≤ A , λ A ) consisting of:

• an event structure (M A , ≤ A ) whose elements are called the moves of the game,

• a function λ A : M A -→ {-1, +1} which associates to every move a polarity +1 (for the Player moves) or -1 (for the Opponent moves).

Positions.

A position of an asynchronous game A is any finite downward closed subset of (M A , ≤ A ).

The lattice of positions. The set of positions of A is denoted D(A). Positions are ordered by inclusion, and closed under finite union. The partial order (D(A), ⊆) thus defines a sup-lattice. The empty position is the least element of (D(A), ⊆).

It is denoted * A . Positions are also closed under arbitrary nonempty intersection. Adding a top element to (D(A), ⊆) provides a neutral element to intersection, and induces a complete lattice D(A) = (D(A), ⊆) . The greatest lower bound and least upper bound of a family (x i ) i∈I of positions in D(A) are computed respectively as:

i∈I x i =      if I is empty, i∈I x i otherwise, i∈I x i =      if i∈I x i is infinite, i∈I x i if i∈I x i is finite. We call D(A)
the lattice of positions associated to the game A.

The asynchronous graph. Every asynchronous game A induces a graph G(A):

• whose nodes are the positions x, y ∈ D(A),

• whose edges m : x -→ y are the moves verifying y = x {m}, where denotes disjoint union, or equivalently, that y = x ∪ {m} and that the move m is not an element of x.

We call this graph G(A) the asynchronous graph of the game A. We write s : x y for a path x

m 1 -→ x 1 m 2 -→ • • • m k-1 -→ x k-1 m k
-→ y between two positions x and y. Note that there is no repetition of move in the sequence:

∀i, j ∈ {1, ..., k}, i = j ⇒ m i = m j . The target y of the path s : x y may be deduced from the source x and the sequence of moves m 1 , ..., m k , using the equation:

y = x 1≤i≤k {m i }.
A path of G(A) is thus characterized by its source (or alternatively, its target) and the sequence of moves

m 1 • • • m k .
Homotopy. Given two paths s, s : x y of length 2 in the asynchronous graph G(A), we write s ∼ 1 s when s = m • n and s = n • m for two moves m, n ∈ M A . The homotopy equivalence ∼ between paths is defined as the least equivalence relation containing ∼ 1 , and closed under composition; that is, for every four paths s 1 : x 1 x 2 and s, s : x 2 x 3 and s 2 :

x 3 x 4 : s ∼ s ⇒ s 1 • s • s 2 ∼ s 1 • s • s 2 .
We also use the notation ∼ in our diagrams to indicate that two (necessarily different) moves m and n are permuted:

z y 1 n > > | | | | | y 2 m BB B B B x n > > | | | | | m BB B B B ∼ (13)
Note that our current definition of asynchronous game implies that two paths s 1 :

x 1 y 1 and s 2 : x 2 y 2 are homotopic iff x 1 = x 2 and y 1 = y 2 . Thus, homotopy becomes informative only in the presence of an independence relation between moves, see Section 7.

Alternating paths. A path m

1 • • • m k : x y is alternating when: ∀i ∈ {1, ..., k -1}, λ A (m i+1 ) = -λ A (m i ).
Alternating homotopy. Given two paths s, s : x y of length 4 in the asynchronous graph G(A), we write

s ∼ 1 OP s when s = m 1 • n 1 • m 2 • n 2 and s = m 2 • n 2 • m 1 • n 1 for two Opponent moves m 1 , m 2 ∈ M A and two Player moves n 1 , n 2 ∈ M A .
The situation is summarized in diagram [START_REF] Ehrhard | A relative definability result for strongly stable functions and some corollaries[END_REF]. The relation ∼ OP is defined as the least equivalence relation containing ∼ 1 OP and closed under composition.

Note that s ∼ OP s implies s ∼ s , but that the converse is not necessarily true, even when the two paths s and s are alternating. A typical illustration of the phenomenon occurs in diagram [START_REF] Ehrhard | A relative definability result for strongly stable functions and some corollaries[END_REF] when the moves n 1 may be permuted in front of the move m 1 by homotopy:

m 1 • n 1 ∼ 1 n 1 • m 1 .
In that case, the sequence of moves

m 2 • n 1 • m 1 • n 2 defines an alternating path, which is homotopic to the path m 1 • n 1 • m 2 • n 2 modulo ∼ but not homotopic to that path modulo ∼ OP .

Plays. A play is a path starting from the empty position *

A : * A m 1 -→ x 1 m 2 -→ • • • m k-1 -→ x k-1 m k -→ x k
in the asynchronous graph G(A). The set of plays is noted

P A . Equivalently, a play of A is a finite sequence s = m 1 • • • m k of moves, without repetition, such that the set {m 1 , ..., m j } is downward closed in (M A , ≤ A ) for every 1 ≤ j ≤ k.

Strategy.

A strategy σ is a set of alternating plays of even length such that:

• the strategy s ∈ σ contains the empty play,

• every nonempty play s ∈ σ starts with an Opponent move,

• σ is closed by even-length prefix:

∀s ∈ P A , ∀m, n ∈ M A , s • m • n ∈ σ ⇒ s ∈ σ, • σ is deterministic: ∀s ∈ P A , ∀m, n 1 , n 2 ∈ M A , s • m • n 1 ∈ σ and s • m • n 2 ∈ σ ⇒ n 1 = n 2 .
We write σ : A when σ is a strategy of A.

Innocent strategies

Ten years ago, Martin Hyland, Luke Ong and Hanno Nickau introduced the notion of innocent strategy in the framework of arena games, and solved in this way the Full Abstraction problem for the language PCF, see [START_REF] Hyland | On full abstraction for PCF: I, II and III[END_REF][START_REF] Nickau | Hereditarily sequential functionals[END_REF] for details. Innocent strategies characterize the interactive behaviour of the simply-typed λ-calculus equipped with a constant Ω for non-termination. This enriched variant of the λcalculus appears under several guises in the literature: either as a calculus of η-long Böhm trees [START_REF] Danos | Games semantics and abstract machines[END_REF], or as partial proofs of Polarized Linear Logic [START_REF] Laurent | Polarized games (extended abstract)[END_REF], or (after a continuation-passing style translation) as the language PCF augmented with local control [START_REF] Laird | Full abstraction for functional languages with control[END_REF][START_REF] Abramsky | Game semantics[END_REF][START_REF] Harmer | Games and full abstraction for nondeterministic languages[END_REF].

The traditional definition of innocence is formulated in two stages. First, a notion of Player view of a justified play (s, ϕ) is computed using the pointer structure ϕ of the play in the arena game. Then, an innocent strategy is defined as a strategy which plays according to the current Player view.

Here, we recast the definition of innocence in asynchronous games. The resulting definition is simpler than in arena games, for two reasons. First, every move m occurs at most once in a play of an asynchronous game. Consequently, there is no need to distinguish the move m from its occurrences in the play -which is a shallow but irritating difficulty of arena games. Then, every play s comes equipped with an implicit pointer structure ϕ given by the causality relation ≤ between moves. Thus, the definition of Player view of a play s does not require any explicit pointer structure ϕ in an asynchronous game. We explain this key point now.

Justification pointers. Suppose that m and n are two different moves of an asynchronous game A. We write m A n, and say that m justifies n, when:

• m ≤ A n, and

• for every move p ∈ M A such that m ≤ A p ≤ A n, either m = p or p = n.
A move m is called initial when it has no justifier, or alternatively, when it is minimal in the ordered set (M A , ≤ A ).

View extraction. We define the binary relation OP as the smallest relation between alternating plays such that:

s 1 • m • n • s 2 OP s 1 • s 2
for every alternating play s 1 , every nonempty alternating path s 2 , every Opponent move m which does not justify any move in s 2 , and every Player move n which does not justify any move in s 2 .

Player view. The relation OP defines a noetherian and locally confluent rewriting system on alternating plays. By Newman's Lemma, the rewriting system is confluent, see [START_REF] Baader | Term Rewriting and All That[END_REF][START_REF] Bezem | Abstract reduction systems[END_REF]. Thus, every alternating play s ∈ P A induces a unique normal form noted s ∈ P A and called its Player view:

s OP s 1 OP • • • OP s k OP s .
This definition by extraction improves in many ways the traditional definition by induction formulated in [START_REF] Mccusker | Games and full abstraction for a functional metalanguage with recursive types[END_REF][START_REF] Abramsky | Game semantics[END_REF][START_REF] Harmer | Games and full abstraction for nondeterministic languages[END_REF]. The definition by extraction ensures for instance that the Player view s of a play s is a play. This is not the case with the inductive definition. We come back to that interesting point later in the section, when we define the notion of visible play in an asynchronous game.

Asynchronous innocence.

A strategy σ is called innocent in an asynchronous game A when for every plays s, t ∈ σ, for every Opponent move m ∈ M A and Player move n ∈ M A :

s • m • n ∈ σ and t • m ∈ P A and s • m ∼ OP t • m ⇒ t • m • n ∈ σ.
This definition of innocence is more concise than the familiar one, formulated in [START_REF] Hyland | On full abstraction for PCF: I, II and III[END_REF][START_REF] Nickau | Hereditarily sequential functionals[END_REF][START_REF] Abramsky | Game semantics[END_REF]. In particular, it does not require any visibility condition on the strategy. It also generalizes the usual notion of innocence to more "concurrent" arenas, in which several moves m 1 , ..., m k may justify the same move n -a situation which does not occur in arena games associated to linear or intuitionistic types.

Before carrying on, we establish that in any asynchronous game A, Lemma 1 Every innocent strategy σ is closed under ∼ OP -equivalence:

∀s, t ∈ P A , s ∈ σ, s ∼ OP t ⇒ t ∈ σ.
PROOF. It is sufficient to establish the assertion for two plays s and t of the form:

s = s 1 • m 1 • n 1 • m 2 • n 2 • s 2 , t = s 1 • m 2 • n 2 • m 1 • n 1 • s 2 ,
where s 1 and s 2 are two paths, m 1 and m 2 are two Opponent moves, and n 1 and n 2 are two Player moves. The proof is by induction on the length of the path s 2 . First, we establish the property when the path s 2 is empty. Suppose that

s = s 1 • m 1 • n 1 • m 2 • n 2
is a play of the strategy σ, and that

t = s 1 • m 2 • n 2 • m 1 • n 1 (14)
is a play of the game. As prefix of ( 14) the sequence s 1 • m 2 defines a play. This ensures that neither of the two moves m 1 and n 1 justifies the move m 2 , which implies in turn that there exists an extraction step

s 1 • m 1 • n 1 • m 2 OP s 1 • m 2 .
By definition of the Player view as the normal form of extraction, the Player views of

s 1 • m 1 • n 1 • m 2 and of s 1 • m 2 coincide.
We apply here our hypothesis that the strategy σ is innocent, and deduce from

s 1 • m 1 • n 1 • m 2 • n 2 ∈ σ that s 1 • m 2 • n 2 ∈ σ.
We carry on, and establish now that

s 1 • m 2 • n 2 • m 1 • n 1 ∈ σ. As a prefix of (14) the sequence s 1 • m 2 • n 2 • m 1 defines a play.
Since neither of the moves m 2 and n 2 justifies the move n 1 (as testifies the fact that s is a play), there exists an extraction step

s 1 • m 2 • n 2 • m 1 OP s 1 • m 1 .
From this follows that the Player views of s 1 • m 1 and of

s 1 • m 2 • n 2 • m 1 coincide.
Again, we apply the hypothesis that the strategy σ is innocent, and deduce from

s • m 1 • n 1 ∈ σ that s 1 • m 2 • n 2 • m 1 • n 1 ∈ σ.
This proves the assertion when the path s 2 is empty. Now, suppose that the path s 2 is not empty, and factors as s 3 • m • n. In that case, the two plays s and t factor as:

s = s 1 • m 1 • n 1 • m 2 • n 2 • s 3 • m • n, t = s 1 • m 2 • n 2 • m 1 • n 1 • s 3 • m • n.
By hypothesis, the play s is an element of the strategy σ. By definition, a strategy is closed by even-length prefix. Thus, the play

s 1 •m 1 •n 1 •m 2 •n 2 •s 3 is also element of the strategy σ.
By induction hypothesis, it follows that the play

s 1 •m 2 •n 2 •m 1 •n 1 •s 3
is an element of the strategy σ. Now, we observe that two ∼ OP -equivalent plays have ∼ OP -equivalent Player views: this key property is a simple consequence of the definition by extraction of a Player view. The property ensures that the Player views of

s 1 •m 1 •n 1 •m 2 •n 2 •s 3 •m and s 1 •m 2 •n 2 •m 1 •n 1 •s 3 •m are ∼ OP -equivalent.
We may thus apply the hypothesis that σ is innocent, and deduce from s ∈ σ that t ∈ σ. This concludes our argument by induction.

Corollary 2 If an innocent strategy σ contains a play s, it also contains its Player view s . Moreover, if s•m is a play in which m is an Opponent move, then s•m factors as s • m = t • m where the play t is an element of the strategy σ.

PROOF. By definition of the Player view of the play s ∈ σ, there exists a path s such that s ∼ OP s •s . We know by Lemma 1 that s •s ∈ σ. By definition, the strategy σ is closed under even-length prefix. The Player view of a play s of evenlength, is itself of even-length. We conclude that s ∈ σ. The second assertion is proved in exactly the same way.

Intuitionistic games. We conclude this section by showing that our definition of innocence is equivalent to the traditional one when the underlying asynchronous game satisfies:

• every Opponent move n has at most one justifying move m,

• when it exists, this justifying move m is a Player move.

By convention, we call intuitionistic any asynchronous game verifying the two properties. This denomination is justified by the fact that any asynchronous game interpreting an intuitionistic type satisfies the two properties.

Player view (HON).

In order to work out the comparison, we recast in our asynchronous framework the original definition of innocence -or more precisely its familiar formulation devised by Guy McCusker in his PhD thesis [START_REF] Mccusker | Games and full abstraction for a functional metalanguage with recursive types[END_REF]. We require to that purpose that the underlying asynchronous game is intuitionistic. To every alternating play s of the asynchronous game, we associate its Hyland-Ong-Nickau (HON for short) view s , defined by induction on the length of the play s, as follows: The definition is valid because an Opponent move n has at most one justifying move m in the intuitionistic game. It is worth stressing that the Player HONview s of an alternating play s is not necessarily a play: it is only an alternating sequence of moves. This is not particularly surprising, since the problem is recurrent in arena games. We have just imported it... The bad situation occurs precisely when one applies the first clause:

s • n = s • n when the move n is Player, s • m • t • n = s • m • n
s • n = s • n (15)
to a play s • n in which a move m which justifies the Player move n does not appear in the sequence s . Note that this is precisely the situation in which the two definitions of Player views (by extraction vs. by induction) differ. In that situation indeed, the equation

s • n = s • n (16)
does not hold... since by construction, the Player view s•n contains the justifying move m. The following lemma clarifies the situation:

Lemma 3 Suppose that s is an alternating play in an intuitionistic game. Then, the equality s = s holds iff the alternating sequence s is a play.

PROOF. The left-to-right implication is immediate, because the Player view s of an alternating play s is a play by construction. We prove the right-to-left implication by induction on the length of s. Suppose that the alternating sequence s is a play. The assertion of the lemma is immediate when the play s is empty. Otherwise, we proceed by case analysis on its last move. Suppose that the last move of the play s is a Player move n. Then, the play decomposes as s = t • n. By hypothesis, the sequence s is a play. From the equality

s = t • n = t • n (17)
follows that t is a play, and that every justifying move of the move n appears in the play t . We apply our induction hypothesis on t, and deduce that

t = t (18)
Now, we claim that the equality

t • n = t • n (19)
holds. This is established as follows. By definition of the Player view t , there exists a sequence of extractions:

t OP • • • OP t .
This sequence induces in turn a sequence 17) and ( 18) and ( 19) that

t • n OP • • • OP t •
s = t • n = t • n = t • n = t • n = s .
This concludes our argument by induction when the last move of s is a move by Player.

Now, suppose that the last move of the play s is an Opponent move n. The assertion of the lemma is immediate when n is an initial move: in that case, s = s = n. Otherwise, the play decomposes as s = t • m • u • n where m is the unique move justifying n in the intuitionistic game. This move m is a Player move. By hypothesis, the sequence s is a play. From this and the equality

s = t • m • u • n = t • m • n (20)
follows that t • m is a play. We apply our induction hypothesis on t•m and deduce that

t • m = t • m . (21)
We claim that the equality

t • m • u • n = t • m • n (22)
holds. Note already that there exists a sequence

t • m • u • n OP • • • OP t • m • n
which "extracts" the path u from the play t • m • u • n. By definition of the Player view as the normal form of the extraction procedure, this implies that

t • m • u • n = t • m • n .
There remains to show that

t • m • n = t • m • n.
The sequence of extractions 20) and ( 21) and ( 22) that

s = t • m • u • n = t • m • n = t • m • n = t • u • m • n = s .
This concludes our argument by induction when the last move of s is a move by Opponent. This establishes the assertion of Lemma 3.

Visibility. We define a notion of visibility in asynchronous games, similar to the notion of visibility in arena games [START_REF] Abramsky | Linearity, sharing and state: a fully abstract game semantics for idealized algol with active expressions[END_REF][START_REF] Abramsky | Game semantics[END_REF]. Consider an asynchronous game, and an alternating play s of that game. We declare that the play s is P -visible when the equality

t • m • n = t • m • n
holds for every Player move n and prefix t•m•n of the play. This equality formulates in a concise way that every justifying move of n appears in the Player view s•m . Note that in the particular case of an intuitionistic game, the HON-view s of a P -visible play s is a play -and not just an alternating sequence of moves. From this follows, by Lemma 3, that the equality s = s holds for every P -visible play s.

We prove that in any asynchronous game A, Lemma 4 An innocent strategy σ contains only P -visible plays.

PROOF. Suppose that σ is an innocent strategy, and that s is a play of σ.

u ∈ σ, u • m ∈ P A and t • m • n ∈ σ, that t • m • n = u • m • n
is a play of the strategy σ. The fact that t • m • n defines a play ensures that all the justifying moves of n appear in t

• m = u • m. Equivalently, that t • m • n = t • m • n.
This being true for every Player move n and prefix t • m • n of the play s, we conclude that the play s is P -visible.

Innocence (HON).

At this point, we recast the traditional definition of innocence in our asynchronous framework, and show that it coincides with the definition of innocence given previously. For the purpose, we suppose that the underlying asynchronous game is intuitionistic -so that we may speak of the HON-view of a play. In such a game, a strategy σ is called HON-innocent when for every plays s, t ∈ σ, for every Opponent move m ∈ M A and Player move n ∈ M A :

s • m • n ∈ σ and t • m ∈ P A and s • m = t • m ⇒ t • m • n ∈ σ.
Besides, one requires that every move justifying the move n in the play t • m, appears in the sequence t • m . This last condition is called the visibility condition, because it is equivalent to requiring that every play of the strategy σ is P -visible.

We prove that in any intuitionistic game A,

Proposition 5 A strategy σ is innocent iff it is HON-innocent.
PROOF. We start by the left-to-right implication. Suppose that the strategy σ is innocent. We establish that the strategy σ is HON-innocent. Suppose that s and t are two plays of the strategy σ, that m is an Opponent move, and n is a Player move such that s • m • n is a play of the strategy σ. Suppose also that t • m is a play of the game, and that s • m = t • m . We show that t • m • n is a play of σ in order to establish that the strategy σ is HON-innocent. By Lemma 4, the play t is P -visible. The move m is an Opponent move. By definition of P -visibility, the play t • m is also P -visible. From this follows that t • m is a play. By Lemma 3, the two plays t • m and t • m coincide. We may reuse the argument to show that s • m is a play equal to s • m . By hypothesis, s • m = t • m . This implies that s • m = t • m . We apply the hypothesis that σ is innocent, and deduce that t • m • n is a play of σ. The proof is nearly finished. There remains to check the visibility condition that every play of the innocent strategy σ is P -visible. This is precisely what Lemma 4 states. We conclude that the strategy σ is HON-innocent.

We establish the right-to-left implication now. Suppose that the strategy σ is HONinnocent, that s • m • n is a play of σ in which s is a play of σ, m is an Opponent move, and n is a Player move. Suppose also that t is a play of σ, that t • m is a play, and that s • m ∼ OP t • m . As elements of the HON-innocent strategy σ, the plays s and t are P -visible. By definition of P -visibility, the plays s • m and t • m are also P -visible, because the move m is Opponent. Thus, the sequences s • m and t • m are plays. By Lemma 3, they are equal to s • m and t • m respectively. The equivalence s • m ∼ OP t • m follows from that. Here comes the crux of the proof. Observe that, by definition, every Player move in the HONview s • m justifies the following Opponent move. This ensures that the ∼ OPequivalence class of the play s • m is a singleton. The equality s • m = t • m follows immediately. We apply the hypothesis that the strategy σ is HON-innocent, and deduce that t • m • n is a play of σ. This concludes the proof of the proposition. Proposition 5 ensures that the homotopy relation s • m ∼ OP t • m appearing in our definition of innocence in asynchronous games may be replaced by an equality s • m = t • m when the asynchronous game is intuitionistic. The homotopy relation s • m ∼ OP t • m appears in the definition only to deal with "concurrent" asynchronous games in which, typically, an Opponent move may be justified by several Player moves of the arena.

Diagrammatic innocence

The reformulation of Player views and innocence performed in Section 3 does not really take advantage of the asynchronous structure of our games. It could be easily carried out in arena games. In this section, we shift to a diagrammatic presentation of innocence. This alternative presentation is inherently asynchronous, and could not be formalized properly in arena games. It prepares the positional characterization of innocence delivered in Section 5.

The diagrammatic presentation of innocence devised in this section is inspired by rewriting theory, and more particularly by the diagrammatic approach developed by the author and a few others in that field [START_REF] Melliès | Axiomatic rewriting 4: a stability theorem in rewriting theory[END_REF][START_REF] Melliès | Axiomatic rewriting 6: Residual theory revisited[END_REF][START_REF] Tennent | Term Rewriting Systems[END_REF]. There is a well-established tradition there, initiated by Alonzo Church and Barkley Rosser, to deduce the "global" properties of the rewriting space (like confluence or standardization) from "local" diagrammatic properties satisfied by redexes and residuals. We proceed in a similar way below, and reduce the "global" definition of innocence devised in Section 3 to exactly two "local" diagrammatic properties -called backward consistency (see Figure 1) and forward consistency (see Figure 2). The two diagrammatic properties should be understood as interactive variants of the familiar local confluence property in rewriting theory. Each of them captures a particular aspect of innocence, somewhat hidden in the original definition. We show below that, taken together, they characterize innocence. Remarkably, the "global" notion of Player view disappears completely from the resulting presentation.

Let us explain briefly the two diagrammatic properties. Backward consistency expresses that an innocent strategy σ should react consistently to a change in the order of Opponent's inquiries. Consider a sequence of interactions s followed by the strategy σ: In that case, Opponent may permute her order of inquiry, and play the move m 2 before playing the move m 1 . Backward consistency ensures that the strategy σ provides exactly the same answer to each inquiry m 1 and m 2 as in the original play s. That is, Player plays the move n 2 after Opponent has played the move m 2 ; then plays the move n 2 after Opponent has played the move m 1 .

s = s 1 • m 1 • n 1 • m 2 • n 2 • s 2 σ s 2 O O O
The remainder of the interaction (noted s 2 ) proceeds then as previously. From this follows that the play

s = s 1 • m 2 • n 2 • m 1 • n 1 • s 2
is also element of the strategy σ.

Forward consistency is a kind of converse to backward consistency, which captures the liveness aspect of innocence. Consider two sequences of interactions followed by the strategy σ:

s = s 1 • m 1 • n 1 and s = s 1 • m 2 • n 2
in which the moves m 1 and m 2 are played by Opponent, and the moves n 1 and n 2 are played by Player. Suppose that the two moves m 1 and m 2 do not coincide. In that case, Opponent may extend the play s with the move m 2 . Forward consistency ensures that the strategy σ provides an answer to this inquiry m 2 : this is precisely the liveness property mentioned earlier. Besides, Player answers the move n 2 . Consequently, the play

s = s 1 • m 1 • n 1 • m 2 • n 2
is an element of the strategy σ, and thus the "local confluence" diagram of Figure 2 may be completed in the same way as in Figure 1.

Backward consistency.

A strategy σ is called backward consistent (see Figure 1) when every play s 1 ∈ σ, every path s

s 1 • m 1 • n 1 • m 2 • n 2 • s 2 ∈ σ and ¬(n 1 A m 2 ) and ¬(m 1 A m 2 )
satisfy also the properties:

¬(n 1 A n 2 ) and ¬(m 1 A n 2 ) and s 1 • m 2 • n 2 • m 1 • n 1 • s 2 ∈ σ.
Forward consistency. A strategy σ is called forward consistent (see Figure 2) when every play s 1 ∈ σ, every pair of Opponent moves m 1 , m 2 , and every pair of Player moves n 1 , n 2 satisfying the properties:

s 1 • m 1 • n 1 ∈ σ and s 1 • m 2 • n 2 ∈ σ and m 1 = m 2
satisfy also the properties:

n 1 = n 2 and s 1 • m 1 • n 1 • m 2 • n 2 ∈ σ.
We use a diagrammatic proof to establish that, for any strategy σ of an asynchronous game A:

Proposition 6 (diagrammatic characterization)

The strategy σ is innocent iff it is backward and forward consistent.

PROOF. (⇒)

This direction is the easiest one. Suppose that the strategy σ is innocent. We establish that the strategy σ is backward consistent. Suppose that the sequence of moves

s 1 • m 1 • n 1 • m 2 • n 2 • s 2 is a play of the strategy σ, in which ¬(n 1 A m 2 ) and ¬(m 1 A m 2 )
. From this follows that the sequence s 1 • m 2 is a play because the sequence

s 1 • m 1 • n 1 • m 2 is a play and ¬(n 1 A m 2 ) and ¬(m 1 A m 2 )
. Now, the extraction step

s 1 • m 2 OP s 1 • m 1 • n 1 • m 2 implies that the Player views s 1 • m 2 and s 1 • m 1 • n 1 • m 2 coincide.
We apply here the hypothesis that the strategy σ is innocent, and deduce from

s 1 • m 1 • n 1 • m 2 • n 2 ∈ σ that s 1 • m 2 • n 2 ∈ σ.
In particular, the sequence s 1 • m 2 • n 2 is a play, and ¬(n 1 A n 2 ) and ¬(m 1 A n 2 ). This establishes that the sequence

s 1 • m 2 • n 2 • m 1 • n 1 • s 2 is
a play of the game. We apply Lemma 1 and deduce from

s 1 • m 1 • n 1 • m 2 • n 2 • s 2 ∈ σ and from s 1 • m 1 • n 1 • m 2 • n 2 • s 2 ∼ OP s 1 • m 2 • n 2 • m 1 • n 1 • s 2 that s 1 • m 2 • n 2 • m 1 • n 1 • s 2 ∈ σ.
We conclude that the strategy σ is backward consistent. We establish now that the innocent strategy σ is forward consistent. Suppose that

s 1 • m 1 • n 1 ∈ σ, that s 1 • m 2 • n 2 ∈ σ,
and that m 1 = m 2 . In that case, the sequence s • m 1 • n 1 • m 2 is a play, whose P -view coincides with the P -view of the play s • m 2 . We apply the hypothesis that the strategy σ is innocent, and deduce from

s 1 • m 2 • n 2 ∈ σ that s 1 • m 1 • n 1 • m 2 • n 2 ∈ σ.
We have just established that the innocent strategy σ is backward consistent. From this and ¬(n 1 A m 2 ) and ¬(m 1 A m 2 ) follows that

s 1 • m 2 • n 2 • m 1 • n 1 ∈ σ.
Moreover, the two moves n 1 and n 2 are necessarily different, since they appear in the same play

s 1 • m 1 • n 1 • m 2 • n 2 .
We conclude that every innocent strategy is backward and forward consistent.

(⇐) This direction is more difficult to establish. Suppose that the strategy σ is backward and forward consistent. Suppose that s : * A x is a play of the strategy σ, and that m : x -→ y is an Opponent move defining a composite play s • m : * A y. Suppose moreover that n is a Player move. We claim that:

s • m • n ∈ σ ⇐⇒ s • m • n ∈ σ. (23)
In particular, we claim that each of the two alternating sequences of moves s • m • n and s • m • n is a play when one of them is a play of the strategy σ. We prove this claim as follows. The Player view s • m is of the form t • m : * A y where t : * A

x is a play of even-length, and m : x -→ y is the Opponent move m starting this time from the position x . By definition of the Player view s • m , there exists two alternating paths of even-length

t 1 = p 1 •p 2 • • • p 2k-1 •p 2k : x x and t 2 = p 1 •p 2 • • • p 2k-1 •p 2k : y y such that t • t 1 ∼ OP s and t 1 ∼ m • t 2 .
We illustrate the situation in Figure 3 (left) with a diagram for the case k = 2. Backward consistency ensures that the strategy σ is closed under ∼ OP -equivalence.

x m / / y

• m / / p 4 O O ∼ • p 4 O O * A t , , s 2 2 ∼ OP • m / / p 3 O O ∼ • p 3 O O • m / / p 2 O O ∼ • p 2 O O x m / / p 1 O O ∼ y p 1 O O x m / / y n / / z • m / / p 4 O O ∼ • O O n / / ∼ • p 4 O O * A t , , s 2 2 ∼ OP • m / / p 3 O O ∼ • O O n / / ∼ • p 3 O O • m / / p 2 O O ∼ • O O n / / ∼ • p 2 O O x m / / p 1 O O ∼ y O O n / / ∼ z p 1 O O
Fig. 3. The situation when k = 2 (before and after applying the diagrammatic reasoning).

From this follows that the plays t and t

• p 1 • p 2 • • • p 2j-1
• p 2j are elements of the strategy σ, for every index j ≤ k.

Now, suppose that the sequence s • m • n is a play of the strategy σ. In that case, we apply the backward consistency hypothesis k times on the play

t • p 1 • p 2 • • • p 2k-1 • p 2k • m • n ∈ σ
and deduce in this way that s•m •n = t•m•n is a play of the strategy σ. Figure 3 (right) describes the situation after applying the backward consistency hypothesis k = 2 times. This proves the direction (⇒) of our claim [START_REF] Laurent | Polarized games (extended abstract)[END_REF]. Now, suppose that the sequence s • m • n is a play of the strategy σ. In that case, we apply the forward consistency hypothesis k times on the play

t • p 1 • p 2 • • • p 2k-1 • p 2k ∈ σ and the play s • m • n = t • m • n to deduce that the sequence t • p 1 • p 2 • • • p 2k-1 • p 2k • m • n is a play of the strategy σ.
From this, and the equivalence

s • m • n ∼ OP t • p 1 • p 2 • • • p 2k-1 • p 2k • m • n
we deduce that the sequence s • m • n is a play of the strategy σ. Again, this last step is justified by the fact that the strategy σ is closed under ∼ OP -equivalence, because it satisfies backward consistency. Figure 3 (right) describes the situation after applying the forward consistency hypothesis k = 2 times. This proves our claim [START_REF] Laurent | Polarized games (extended abstract)[END_REF].

After this preliminary result, we establish that the strategy σ is innocent. Suppose that s • m • n and t are two plays of the strategy σ, that t • m is a play, and that s • m ∼ OP t • m . In order to establish that the strategy σ is innocent, we want to prove that t • m • n ∈ σ. We proceed as follows. We deduce from s [START_REF] Laurent | Polarized games (extended abstract)[END_REF]. We conclude that every backward and forward consistent strategy is innocent.

• m • n ∈ σ and (23) that s • m • n ∈ σ. This and s • m • n ∼ OP t • m • n implies that t • m • n ∈ σ because the strategy σ is closed under ∼ OP -equivalence. Now, t • m • n ∈ σ follows from t • m • n ∈ σ and

Positional innocence

We establish the main result of the article in this section. This result states namely that innocent strategies are positional (Theorem 8). We show more precisely that innocent strategies are relational2 , in the sense explained below (Proposition 10). This raises an interesting question. Every relational strategy σ is characterized by the set of positions σ • it encounters. So, when is a given set of positions X of the form X = σ • for an innocent strategy σ?

In order to answer that question properly, we introduce the notion of pure innocence. A purely innocent strategy is an innocent strategy which satisfies an additional property, a variant of backward consistency, depicted in Figure 4. After showing that innocence and pure innocence coincide in intuitionistic asynchronous games (Lemma 11), we characterize the set X of positions of the form X = σ • for a purely innocent strategy σ (Proposition 12). This characterization demonstrates among other things that innocent (and purely innocent) strategies are concurrent strategies in the sense of the concurrent game model of linear logic introduced by Samson Abramsky and the author in [START_REF] Abramsky | Concurrent games and full completeness[END_REF] (Proposition 13).

Positional strategy. A strategy σ : A is called positional when for every two plays s 1 , s 2 : * A

x in the strategy σ, and every path t : x y of G(A), one has:

( s 1 ∼ s 2 and s 1 • t ∈ σ ) ⇒ s 2 • t ∈ σ.
We establish below the key lemma to prove Theorem 8. Given two paths s and t, we write s t when there exists a path s such that s • s ∼ t. Similarly, we write s OP t when there exists a path s such that s • s ∼ OP t.

We prove that Lemma 7 For every innocent strategy σ of an asynchronous game A, and for every two plays s and t of the strategy σ, s t ⇒ s OP t.

PROOF. Consider a play s 0 : * A x of the innocent strategy σ, and two paths s 1 : x y and s 2 : x z such that the two composite plays s 0 • s 1 : * A y and

s 0 • s 2 : * A
z are elements of the strategy σ. Suppose moreover that s 1 s 2 . We prove by induction on the length of the path s 1 that s 1 OP s 2 . The assertion is immediate when the path s 1 is empty. Now, suppose that the path s 1 factors as s 1 = m • n • t 1 where m is an Opponent move and n is a Player move. The path s 2 decomposes as a sequence

s 2 = m 1 • n 1 • • • m k • n k ( 24
)
consisting of Opponent moves m i and Player moves n i , for 1 ≤ i ≤ k. The Opponent move m appears in the play s 2 because s 1 s 2 . From this follows

(1) that m = m j for some index 1 ≤ j ≤ k, and

(2) that the move m = m j is not justified by any Opponent move m i or Player move n i for 1 ≤ i < j.

We apply then j -1 times our hypothesis that the strategy σ is backward consistent, and construct in this way a path

t 2 = m 1 • n 1 • • • m j • n j • • • m k • n k (25) satisfying m j • n j • t 2 ∼ OP s 2 and s 0 • m j • n j • t 2 ∈ σ.
The notation m j • n j used in [START_REF] Mazurkiewicz | Concurrent program schemes and their interpretations[END_REF] indicates that the two moves m j and n j are removed from the sequence [START_REF] Lévy | Réductions correctes et optimales dans le lambda-calcul[END_REF]. The two plays s 0 • m • n and s 0 • m j • n j are elements of the strategy σ because the strategy is closed under even-length prefix.

The equality n = n j follows immediately from the equality m = m j and from the determinism of the strategy σ. The series

m • n • t 1 = s 1 s 2 ∼ OP m • n • t 2 implies that m • n • t 1 m • n • t 2 ,
which implies in turn that t 1 t 2 by leftsimplification. Left-simplification is justified here by the fact that two paths are homotopic modulo ∼ in the asynchronous graph G(A) if and only if they have the same source and target. Now, we may apply our induction hypothesis to the play t 0 = s 0 • m • n and to the paths t 1 and t 2 -because the length of the path t 1 is strictly less than the length path s 1 = m • n • t 1 ; and because the two plays t 0 • t 1 and t 0 • t 2 are elements of the strategy σ. We may thus deduce from t 1 t 2 that t 1 OP t 2 . The series

s 1 = m • n • t 1 OP m • n • t 2 = m j • n j • t 2 ∼ OP s 2
implies then that s 1 OP s 2 . This concludes our proof by induction of the lemma.

Theorem 8 (positionality) Every innocent strategy σ is positional.

PROOF. Suppose that s 1 , s 2 : * A x denote two homotopic plays: s 1 ∼ s 2 ; and that the two plays are elements of the innocent strategy σ. Suppose now that t : x y denotes a path which may be postcomposed to the plays s 1 and s 2 in order to define composite plays s 1 • t, s 2 • t : * A y. Suppose finally that the play s 1 • t is an element of the strategy σ. We deduce from s 1 ∼ s 2 that s 1 s 2 . We then apply Lemma 7 and deduce that s 1 OP s 2 . This implies in turn that s 1 ∼ OP s 2 because the two plays s 1 and s 2 have the same length. From this follows that s 1 • t ∼ OP s 2 • t. We conclude from Lemma 1 and s 1 • t ∈ σ that the play s 2 • t is an element of the strategy σ.

Relational strategy. To every strategy σ, we associate the set of positions σ • played by the strategy in D(A), defined as:

σ • = {x ∈ D(A) | ∃s ∈ σ, s : * A x}.
Conversely, to every set of positions X ⊂ D(A), we associate the set X ⊂ P A of alternating plays of even-length

* A = x 0 m 1 -→ x 1 m 2 -→ x 2 -→ • • • -→ x 2k-2 m 2k-1 -→ x 2k-1 m 2k -→ x 2k
in which

(1) every move m 2i+1 is an Opponent move, and

(2) every move m 2i+2 is a Player move, and

(3) every position x 2j is an element of X,

for 0 ≤ i ≤ k -1 and 0 ≤ j ≤ k.
It is immediate that every strategy σ is included in the set of alternating plays (σ • ) .

A strategy σ is called relational when

σ = (σ • ) . ( 26
)
Intuitively, a strategy σ is relational when it may be described alternatively as the underlying relation σ • . We prove that:

Lemma 9 Every relational strategy is positional.

PROOF. Consider a set X of positions, two plays s 1 and s 2 elements of X , and a path t. Suppose that s 1 ∼ s 2 , and that s 1 • t defines a play which is an element of X . Every even-length prefix * x of the play s 2 • t is an even-length prefix of the play s 2 , or has the same target x as an even-length prefix of the play s 1 • t. From this follows that this target position x is an element of X for every even-length prefix of s 2 • t. We conclude that the play s 2 • t is an element of X . Now, suppose that the strategy σ is relational. The property above instantiated at X = σ • implies that the strategy σ = X is positional.

Obviously, every relational strategy σ may be recovered from its set of positions σ • by using equation [START_REF] Mazurkiewicz | Introduction to trace theory[END_REF]. This is not necessarily the case for a positional strategy. Consider for instance the asynchronous game B ⊗ B with two initial Opponent moves q 1 , q 2 and four Player moves false 1 , true 1 , false 2 , true 2 justified as expected:

q 1 true 1 , q 1 false 1 , q 2 true 2 , q 2 false 2 .
Consider the smallest strategy σ of B ⊗ B which contains the two plays:

q 1 • true 1 • q 2 • false 2 and q 2 • false 2 .
The strategy σ is positional, but not relational, because the play

s = q 2 • false 2 • q 1 • true 1
is an element of (σ • ) but not an element of the strategy σ. For that reason, we strengthen Theorem 8 and establish the following statement:

Proposition 10 (relationality) Every innocent strategy σ is relational.

PROOF. Suppose that the strategy σ is innocent, and that s is a play of (σ • ) . We prove that s is a play of the strategy σ by induction on the length of s. The proof is immediate when the play s is empty. Otherwise, by definition of (σ • ) , the play s : * A x factors as s = t • m • n where t is a play of (σ • ) , where m is an Opponent move, and where n is a Player move. We know by induction hypothesis that the play t ∈ (σ • ) is an element of the strategy σ. Besides, the target position x of the play s is an element of σ • . By definition of σ • , there exists a play u ∈ σ with the position x as target. In particular, t • m • n ∼ u, and thus t u. We deduce from this and Lemma 7 that t OP u. By definition, there exists an alternating path t such that t • t ∼ OP u. This path t coincides necessarily with m • n. This establishes the equivalence t • m • n ∼ OP u. From this and Lemma 1, we obtain that t • m • n is a play of the strategy σ. This concludes our proof by induction that σ = (σ • ) .

Pure innocence.

An innocent strategy σ is called purely innocent (see Figure 4) when every play s 1 ∈ σ, every path s 2 , every pair m 1 , m 2 of Opponent moves, and every pair n 1 , n 2 of Player moves satisfying the properties:

s 1 • m 1 • n 1 • m 2 • n 2 • s 2 ∈ σ and ¬(n 1 A m 2 ) and ¬(n 1 A n 2 )
satisfy also the properties:

¬(m 1 A m 2 ) and ¬(m 1 A n 2 ) and s 1 • m 2 • n 2 • m 1 • n 1 • s 2 ∈ σ. σ s 2 O O O O n 2 ? ? ∼ n 1
_ _ ? ? ? ? ? m 2 ? ? ∼ _ _ ? ? ? ? ? ? ?

n 1
_ _ ? ? ? ? ? ? ?

m 1
_ _ ? ? ? ? ? _ _ ? ? ? ? ? m 2 ? ?

s 1 O O O O ⇒ s 2 O O O
s 1 O O O O ∈ σ Fig. 4. Reverse consistency
This additional condition is called reverse consistency because it coincides with the backward consistency property (see Figure 1) in which the direction of all moves has been reversed. We establish now that pure innocence coincides with innocence in the particular case of intuitionistic games.

Lemma 11

In any intuitionistic asynchronous game, a strategy σ is purely innocent iff it is innocent.

PROOF. The proof is nearly immediate, and works in any asynchronous game in which no Opponent move justifies another Opponent move. It works in particular in any intuitionistic game. Suppose that the strategy σ is innocent, and that we are in the situation of Figure 4 (left) with a play s 1 ∈ P A , a path s 2 , and moves m 1 , n 1 , m 2 , n 2 ∈ M A such that:

s 1 • m 1 • n 1 • m 2 • n 2 • s 2 ∈ σ and ¬(n 1 A m 2 ) and ¬(n 1 A n 2 ).
By hypothesis on the underlying asynchronous game, the Opponent move m 1 does not justify the Opponent move m 2 . We are thus in the situation of Figure 1 (left). We may thus apply our hypothesis that the strategy σ satisfies backward consistency, and deduce the properties:

¬(m 1 A n 2 ) and s 1 • m 2 • n 2 • m 1 • n 1 • s 2 ∈ σ.
We conclude that the strategy σ is purely innocent.

We express below our positional characterization of pure innocence (Proposition 12). One intriguing aspect of this characterization is that it is nearly self-dual: the second and fourth clauses are exactly the first and third clauses after reversing the direction and the polarity of the moves. Closure under intersection and union demonstrates that purely innocent strategies are inherently concurrent. We come back to that point in Proposition 13. Forward and backward confluence (together with mutual attraction and the initial condition) ensure that every position x ∈ X induces an alternating play of even-length s ∈ X with target the position x. The last clause is called initial condition because it indicates on which position * A the strategy will start interacting with its environment.

The notion of forward confluence appears in [START_REF] Hyland | Games on graphs and sequentially realizable functionals[END_REF] where it is called conflict-freeness, and (independently) in the author's game-theoretic proof [START_REF] Melliès | Sequential algorithms and strongly stable functions[END_REF] of Thomas Ehrhard's collapse theorem -where the notion plays a fundamental role in the dynamic analysis of hypercoherence spaces. To some extent, forward confluence is the positional counterpart of determinism in the usual definition of strategy formulated at the end of Section 2. Remarkably, the dual notion of backward confluence offers here a positional account of the fact that plays are closed under even-length prefix. This reveals that this familiar condition on strategies (understood as sets of sequences) is a hidden form of backward determinism.

Proposition 12 (positional characterization) A set of positions X ⊂ D(A) is of the form X = σ • for a purely innocent strategy σ iff the set X satisfies the following properties: PROOF. Suppose that σ is a purely innocent strategy. We establish that the set of positions σ • satisfies the six clauses formulated in Proposition 12. We prove first that σ • is closed under unions and intersections. The proof applies the familiar diagrammatic techniques of rewriting theory, based on local diagram chasing and residuals, see for instance [START_REF] Lévy | Réductions correctes et optimales dans le lambda-calcul[END_REF][START_REF] Huet | Call by need computations in non-ambiguous linear term rewriting systems[END_REF][START_REF] Bezem | Abstract reduction systems[END_REF][START_REF] Melliès | Axiomatic rewriting 6: Residual theory revisited[END_REF]. Suppose that x ∈ σ • and y ∈ σ • . By definition, there exists two plays s ∈ σ and t ∈ σ such that:

• X is closed under intersection: x, y ∈ X ⇒ x ∩ y ∈ X, • X is closed under union: x, y ∈ X ⇒ x ∪ y ∈ X, • forward confluence: if X x m -→ y w ∈ X and m is an Opponent move, then there exists a unique Player move y n -→ z such that X z w ∈ X, • backward confluence: if X w y n -→ z ∈ X
s : * A x and t : * A y.
The property of forward consistency enables us to apply a series of permutations of OP-moves on s and t, in order to construct two "residual" paths s/t : y x ∪ y and t/s : x x ∪ y such that:

s • (t/s) ∼ OP t • (s/t) and s • (t/s) ∈ σ and t • (s/t) ∈ σ.
This establishes that x ∪ y ∈ σ • . The proof that x ∩ y ∈ σ • works in a similar way.

The key observation in that respect is that the asynchronous transition system with the elements of σ • as states, and the OP-moves as transitions, is not only confluent: it is also stable in the sense of [START_REF] Panangaden | Stability and sequentiality in data flow networks[END_REF][START_REF] Kuske | Non deterministic automata with concurrency relations and domains[END_REF][START_REF] Melliès | Axiomatic rewriting 4: a stability theorem in rewriting theory[END_REF].

We establish now the forward confluence of σ • . Suppose that two positions x, w are elements of σ • , and that

x m -→ y w (27)
for some position y and Opponent move m. By definition of σ • , there exists a play s ∈ σ whose target is the position x, and a play t ∈ σ whose target is the positions w. It follows from ( 27) that s t, and from Lemma 7 that s OP t. Thus, there exists a path

s = m 1 • n 1 • • • m k • n k : x w (28)
consisting of Opponent moves m i and Player moves n i , for

1 ≤ i ≤ k, such that s • s ∼ OP t.
The Opponent move m is an element of the position w, but not an element of the position x. This implies (1) that m = m j for some index 1 ≤ j ≤ k, and (2) that the move m = m j is not justified by any Opponent move m i or Player move n i , for 1 ≤ i < j.

We apply j -1 times our hypothesis that the strategy σ is backward consistent, and construct in this way a path

s = m 1 • n 1 • • • m j • n j • • • m k • n k satisfying m j • n j • s ∼ OP s and s 1 • m j • n j • s ∈ σ.
Just as in the proof of Lemma 7, the notation m j • n j indicates that the two moves m j , n j are removed from the sequence [START_REF] Melliès | Axiomatic rewriting 4: a stability theorem in rewriting theory[END_REF].

We claim that the move n : y -→ z defined as n = n j is the unique Player move from the position y whose target position z is an element of the set σ • , which satisfies moreover

x m -→ y n -→ z w. (29)
By definition, the position z is the target of the even-length play

s 1 •m j •n j = s 1 •m•n which is prefix of the play s 1 • m j • n j • s ∈ σ.
From this follows that s 1 • m j • n j is a play of the strategy σ, and thus, that its target z is an element of the set σ • . Besides, the fact that z w follows immediately from the definition of the move n j . We have established that the Player move n : y -→ z has a position of σ • as target, and satisfies [START_REF] Melliès | Axiomatic rewriting 6: Residual theory revisited[END_REF]. We prove now that there is a unique such Player move n from the position y. Suppose that another Player move n : y -→ z has its target position z in the set σ • , and satisfying z w. In that case, the position y coincides with the intersection of the two positions z = y {n} and z = y {n }. Now, we have just established that the set σ • is closed under intersection. The position y is thus an element of the set σ • . This and y = x {m} contradicts the fact that every position of the set σ • contains as many Opponent moves as Player moves. This concludes the proof that the set σ • satisfies forward confluence.

The backward confluence property of σ • is established in the same way, by duality. Reverse consistency replaces backward consistency in the argument to obtain the Opponent move m solution of the confluence problem. Closure under intersection is replaced by closure under union in order to establish the uniqueness of that move m.

The two last assertions are immediate: mutual attraction follows from Lemma 7, and the initial condition that σ • contains the starting position * A follows from the fact that the strategy σ contains the empty play A . This concludes the proof that the set of positions σ • satisfies the six assertions of Proposition 12 when the strategy σ is purely innocent.

We establish now the converse property that any set X of positions satisfying the six clauses of Proposition 12 is of the form σ • for a relational strategy σ. Suppose that we are given such a set X of positions. We define σ as the set of alternating sequences σ = X . We recall that, by definition, the set σ contains the set of alternating plays of evenlength

* A = x 0 m 1 -→ x 1 m 2 -→ x 2 -→ • • • -→ x 2k-2 m 2k-1 -→ x 2k-1 m 2k -→ x 2k
in which (1) every move m 2i+1 is an Opponent move, (2) every move m 2i+2 is a Player move, and (3) every position x 2j is an element of X, for 0 ≤ i ≤ k -1 and 0 ≤ j ≤ k.

We show that for every position x ∈ X, there exists a play s ∈ σ whose target is the position x. This is easily established by induction on the size of x. The property is immediate when the position x is empty. Suppose now that the position x ∈ X is not empty. There exists a path * A

x starting from the position * A . The initial condition ensures that this position * A is an element of X. By mutual attraction, there exists a Player move m : y -→ x. By backward confluence, there exists an Opponent move n : z -→ y such that z ∈ X. By induction hypothesis applied to the position z, there exists a play s : * A z in the strategy σ. By definition of X , the play

s • m • n : * A z n -→ y m -→ x
is also an element of σ = X . This concludes our proof by induction that every position x ∈ X is the target of a play s ∈ σ.

Now, we show that the set of plays σ defines a strategy in the traditional sense, formulated at the end of Section 2. To that purpose, we check that the four conditions required on the set of plays σ are satisfied:

• the set σ contains the empty play because X contains the empty position,

• by definition of σ as X , every nonempty play s ∈ σ starts with an Opponent move, and σ is closed under even-length prefix,

• suppose that s • m • n 1 ∈ σ and s • m • n 2 ∈ σ, where s : * A
x and m : x -→ y and n i : y -→ z i for i ∈ {1, 2}. By definition of σ as X , the two positions z 1 = y {n 1 } and z 2 = y {n 2 } are elements of X. Since the set X is closed under intersection, the position z 1 ∩ z 2 is also element of X. Suppose that the two moves n 1 and n 2 are different. In that case, y = z 1 ∩ z 2 is element of X, and thus target of an alternating play t ∈ σ. As such, the position y contains as many Opponent moves as Player moves. This contradicts the fact that y = x {m} and that the position x contains as many Opponent moves as Player moves as the target of the alternating play s ∈ σ. We conclude that n 1 = n 2 and thus, that σ is deterministic.

We have just established that σ defines a strategy. There remains to show that the strategy σ satisfies the three consistency properties of pure innocence (backward, forward, and reverse). We start by establishing the backward consistency property. Suppose that we are in the situation of Figure 1, with a play

s 1 : * A x four moves x m 1 -→ y 1 n 1 -→ y 2 m 2 -→ y 3 n 2 -→ w satisfying ¬(n 1 A m 2 ) and ¬(m 1 A m 2 )
and a path s 2 : w w satisfying all together

s 1 • m 1 • n 1 • m 2 • n 2 • s 2 ∈ σ.
By forward confluence applied to the positions x ∈ X and w ∈ X, and to the Opponent move m 2 : x -→ z 1 there exists a Player move n : z 1 -→ z 2 such that z 2 ∈ X and:

x m 2 -→ z 1 n -→ z 2 w.
By forward confluence again, applied to the positions z 2 ∈ X and w ∈ X, and to the Opponent move:

m 1 : z 2 -→ z 3
there exists a Player move n : z 3 -→ z 4 with z 4 w and thus z 4 = w for cardinality reasons. We conclude that the play

* A s 1 x m 2 -→ z 1 n -→ z 2 m 1 -→ z 3 n -→ w s 2 w
is an element of the strategy σ. There remains to show that n = n 2 and n = n 1 .

The only other possibility is that n = n 1 and n = n 2 . We claim that this last possibility would contradict the backward confluence of X. In that case, indeed, the two positions y 3 and z 3 are equal, and thus define with the position x ∈ X and the move n = n 2 a typical backward confluence problem:

X x y 3 n 2 -→ w ∈ σ
Now, the Opponent moves m 1 and m 2 provide two different solutions to this backward confluence problem:

x y 2 m 2 -→ y 3 n 2 -→ w ∈ σ and x z 2 m 1 -→ z 3 n 2 -→ w ∈ σ
with the two positions y 2 and z 2 elements of the set X. This contradicts the hypothesis that there exists a unique such solution. We conclude that n = n 2 and n = n 1 , and thus that the play *

A s 1 x m 2 -→ z 1 n 2 -→ z 2 m 1 -→ z 3 n 1 -→ w s 2 w
is an element of the strategy σ. This establishes that the strategy σ satisfies backward consistency. Reverse consistency is established in exactly the same way, but dually, by reversing the direction and the polarity of the moves. Forward consistency is established by reduction to backward consistency, using the fact that the set X is closed under unions. This concludes the proof of Proposition 12.

Proposition 13 Every innocent strategy σ : A defines a closure operator σ • on the complete lattice D(A) of positions.

PROOF. By convention, the closure operator σ • on the lattice D(A) is denoted in the same way as the set of positions σ • played by the strategy σ. By definition, the closure operator σ • associates to every element x of the lattice the element

σ • (x) = {z ∈ D(A) | z ∈ σ • and z ≥ x}. (30)
Note that σ • (x) = precisely when there exists no position y ∈ σ • above the element x in the sup-lattice D(A). Let us check here that (30) defines a closure operator on the lattice D(A) , although the exercise is pretty elementary. By closure operator on the lattice D(A) , we mean a monotone, continuous, increasing and idempotent endofunction of the lattice. Monotonicity means that, for every two elements x, y of the lattice D(A) ,

x ≤ y ⇒ σ • (x) ≤ σ • (y).
≤ σ • (x) (31)
for every element x of the lattice. This inequality follows immediately from the definition of the element σ • (x) as the greatest lower bound of a set of elements greater than the element x. Now, idempotency means that

σ • (σ • (x)) = σ • (x)
for every element x of the lattice. This follows immediately from the equality:

{z ∈ D(A) | z ∈ σ • and z ≥ x} = {z ∈ D(A) | z ∈ σ • and z ≥ σ • (x)}.
Finally, continuity means that

σ • ( i∈N x i ) = i∈N σ • (x i ) (32)
for every infinite increasing sequence (x i ) i∈N of elements:

x 0 ≤ x 1 ≤ • • • ≤ x i-1 ≤ x i ≤ x i+1 ≤ • • • (33)
in the complete lattice D(A) . At this point, we take advantage of a very particular property of that lattice: every increasing sequence of the form [START_REF] Melliès | Asynchronous games 3: an innocent model of linear logic[END_REF] in the lattice D(A) is either stationary -that is, there exists a natural number N ∈ N such that: ∀i ∈ N, i ≥ N ⇒ x i = x i+1 , or converges to the element :

i∈N x i = . (34)
Equation ( 32) follows immediately when the sequence [START_REF] Melliès | Asynchronous games 3: an innocent model of linear logic[END_REF] is stationary; and it follows from the equality This series of properties explicates the true concurrency nature of innocence. Proposition 13 bridges sequential arena games with concurrent games as they are formulated by Samson Abramsky and the author in [START_REF] Abramsky | Concurrent games and full completeness[END_REF]. We illustrate this in Figure 5 with the innocent strategy σ : B ⊗ B which answers "true" (Vrai in French) on the left component, and "false" on the right component. The four positions of σ • are indicated on the graph: * ⊗ * , V ⊗ * , * ⊗F , and V ⊗F . Note that the innocent strategy σ understood as the closure operator or concurrent strategy σ • plays directly the position V ⊗ F ∈ σ • from the position q ⊗ q, and thus answers simultaneously the two questions q 1 and q 2 asked by Opponent concurrently.

i∈N σ • (x i ) = (35)
Despite the illustration, the reader may still find the idea of positionality difficult to grasp. If this is the case, we hope that the proposition below will clarify the situation. It is quite straightforward to define a notion of innocent counter-strategy τ interacting against the strategy σ. The counter-strategy τ may withdraw at any stage of the interaction. Every withdrawal of τ is expressed by an even-length play s : * A x in the strategy τ , whose target position x ∈ τ • is of even cardinality. Our next result states that the static evaluation (by intersection) of σ • against τ • coincides with the dynamic evaluation (by interaction) of σ against τ . Proposition 14 For every position x ∈ D(A):

σ • ∩ τ • = {x} ⇐⇒ σ ∩ τ = {s} and s : * A x.
It is nearly routine to construct from this a category G with asynchronous games as objects, and innocent strategies as morphisms. The only difficulty is to interpret the exponentials. This is done following the principles of [START_REF] Melliès | Asynchronous games 1: a group-theoretic formulation of uniformity[END_REF]: every game is equipped with a left and right group action, and the exponential !A is interpreted as an infinite tensor product !A = k∈N A. The resulting category G defines a model of intuitionistic linear logic without additives. The usual category of arena games and innocent strategies embeds fully and faithfully (as a cartesian closed category) in the Kleisli category associated to the category G and to its comonad. The interested reader will find the detailed construction in [START_REF] Melliès | Asynchronous games 1: a group-theoretic formulation of uniformity[END_REF].

The non uniform λ-calculus

We introduce in this section a non-uniform variant of the λ-calculus. This λ-calculus is called non-uniform because the argument of a function λx.P is not a λ-term Q, but a vector -→ Q of λ-terms Q i where i ∈ N is an index for each occurrence x(i) (or function call) of the variable x in the λ-term P . The calculus is affine in nature: two occurrences of x(i) never occur in the same term. However, the simply-typed λ-calculus may be encoded in this affine calculus, using the group-theoretic ideas developed in our first article on asynchronous games [START_REF] Melliès | Asynchronous games 1: a group-theoretic formulation of uniformity[END_REF].

Definition of the calculus. The non-uniform λ-terms P and vectors of arguments -→ Q are defined by mutual induction:

P ::= x(i) located variable | P - → Q application | λx.P abstraction - → Q ::= (Q i ) i∈N vector of non-uniform λ-terms indexed by an integer i ∈ N
where a located variable x(i) consists of a variable x in the usual sense, and an integer i ∈ N. We require that every located variable x(i) appears at most once in a term. Note that a non-uniform λ-term is generally infinite. The β-reduction is defined as

(λx.P ) - → Q -→ β P [x(i) := Q i ]
where P [x(i) := Q i ] denotes the non-uniform λ-term obtained by replacing each located variable x(i) in P by the non-uniform λ-term Q i . The non-uniform λ-terms are typed by the simple types of the λ-calculus, built on the base type α:

x(i) : A x(i) : A Γ P : A ⇒ B (∆ i Q i : A) i∈N Γ, ∆ 0 , ∆ 1 , ∆ 2 , • • • P - → Q : B Γ, x(i 0 ) : A, x(i 1 ) : A, x(i 2 ) : A, • • • P : B Γ λx.P : A ⇒ B
Here, a context Γ, ∆, ... may contain an infinite number of located variables, since the ⇒-elimination rule involves a family of derivation trees (∆ i Q i : A) i∈N . On the other hand, the ⇒-introduction rule may migrate an infinite number of located variables x(i) from the context to the λ-term.

Non-uniform η-long Böhm trees. The non-uniform η-long Böhm trees of simple type ) or Ω B where Ω B is a fixed constant of type B, (3) or λx 1 ...λx m . where is a fixed constant of type α, and every variable x j is of type A j , for 1 ≤ j ≤ m.

A = A 1 ⇒ • • • A m ⇒ α are of three kinds: (1) λx 1 ...λx m . ( y(i) -→ Q 1 • • • -→ Q n ) where • every variable x j is of type A j for 1 ≤ j ≤ m, • the located variable y(i) is of type B = B 1 ⇒ • • • B n ⇒ α for some type B, • every non uniform η-long Böhm tree (Q k ) i is of type B k , for 1 ≤ k ≤ n and i ∈ N. ( 2
Trace semantics. Every non-uniform η-long Böhm tree of simple type

A = A 1 ⇒ • • • A m ⇒ α
is interpreted by our game model as an innocent strategy in the asynchronous game interpreting A. This game semantics may be formulated as a trace semantics on non-uniform η-long Böhm trees, in the following way.

The Opponent transitions (or moves) are generated by the rule

Ω A -→ λx 1 • • • λx m .
where A = A 1 ⇒ • • • A m ⇒ α and the variable x j is of type A j for every index 1 ≤ j ≤ m.

The Player transitions are generated by the rule

-→ x(i) - → Ω A 1 • • • - → Ω Am
where x(i) is a located variable of type A = A 1 ⇒ • • • A m ⇒ α, and -→ Ω A j is the vector which associates to every index i ∈ N the constant Ω A j , for every 1 ≤ j ≤ m.

Every move from an η-long Böhm tree is then labelled by a subtree of the type A, once translated in linear logic as an infinite formula, using the equation

A ⇒ B = !A B
and the definition of the exponential modality as an infinite tensor:

!A = i∈N A.
Uniformity and bi-invariance. The usual (uniform) η-long Böhm trees of the λcalculus are extracted from their non-uniform counterpart using the bi-invariance principle introduced in [START_REF] Melliès | Asynchronous games 1: a group-theoretic formulation of uniformity[END_REF]. As recalled in the introduction, every game is equipped with a left and a right group action on moves. A strategy σ is called bi-invariant when, for every play s ∈ σ and every right action h ∈ H, there exists a left action g ∈ G such that (g s) h ∈ σ. This characterizes the strategies which are "blind to thread indexing", and thus the strategies which behave as if they were defined directly in an arena game. The concept of bi-invariance remains formal and enigmatic in [START_REF] Melliès | Asynchronous games 1: a group-theoretic formulation of uniformity[END_REF]. Here, quite fortunately, the non-uniform λ-calculus provides a syntactical explanation for the concept of bi-invariance, which clarifies its meaning and significance. We discuss that now.

Every intuitionistic type A defines a left and right group action (5) on the asynchronous game [A] interpreting it in the asynchronous game model. These two group actions may be understood syntactically as acting on the non-uniform η-long Böhm trees P of type A, as follows: the effect of a right group action h ∈ H is to permute the indices inside the vectors of arguments -→ Q in P , while the effect of a left group action g ∈ G is to permute the indices of the located variables x(i) in P . By analogy with [START_REF] Melliès | Asynchronous games 1: a group-theoretic formulation of uniformity[END_REF], a non-uniform η-long Böhm tree P is called bi-invariant when for every permutation h ∈ H, there is a permutation g ∈ G such that (g P ) h = P.

It is not difficult to see that an η-long Böhm tree in the usual λ-calculus is just a bi-invariant η-long Böhm tree in the non-uniform λ-calculus, modulo left group action (that is, permutation of the indices of the located variables.)

For instance, let P j denote the non-uniform η-long Böhm tree P j = λx.λy.(x(j) -→ y )

of type A = (α ⇒ α) ⇒ (α ⇒ α) where -→ y associates to every index i ∈ N the located variable y(i). Obviously, P j is bi-invariant, and represents the uniform η-long Böhm tree λx.λy.x y of same type A. Note that P j is equivalent to any P k modulo left group action. The trace (or game) semantics of P j is given by: Ω A m -→ λx.λy.

-→ Q k ) n k -→ • • •
Here, the move m by Opponent (labelled by the type A) asks for the value of the head variable of P j , and the move n by Player (labelled by the type (α ⇒ α) j ) answers x(j); then, the move m k by Opponent (labelled by α k in (α ⇒ α) j ) asks for the value of the head variable of the k-th argument of x(j), inducing the vector of arguments

-→ Q k =      (Q k ) k = (Q k ) i = Ω α when i = k
finally the move n k by Player (labelled by α k ) answers y(k), etc... This example illustrates the fact that the trace (or game) semantics of a non-uniform η-long Böhm tree is the syntactic exploration or parsing of that tree by the Opponent. At any point of the interaction, the Player view s of the play s describes the current branch of the non-uniform η-long Böhm tree.

Additional structures

For clarity's sake, we deliver the simplest possible definition of asynchronous game in Section 2. We review below three natural extensions of the definition.

Compatibility. Every asynchronous game may be equipped with an incompatibility relation # between moves, in order to model the additives of intuitionistic linear logic. The relation # indicates when two moves cannot appear in the same position, and thus cannot appear in the same play. The coherence axiom (m 1 #m 2 ≤ m 3 ⇒ m 1 #m 3 ) is required on every triple of moves m 1 , m 2 , m 3 , just as in event structures [START_REF] Winskel | Models for concurrency[END_REF].

Internal vs. external positions. We may go further, and assign to every position x of the asynchronous game an integer κ(x) ∈ Z called its payoff. By convention, a position x is called external when the payoff κ(x) is null, and internal otherwise. It is then possible to construct a game model of propositional linear logic, by identifying two strategies playing the same external positions. Remarkably, the resulting model incorporates the well-bracketed and the non well-bracketed variants of the original innocent arena game model. We give a detailed account of this construction in [START_REF] Melliès | Asynchronous games 3: an innocent model of linear logic[END_REF].

Independence. There is a well-established tradition in trace semantics of describing the interference mechanisms between concurrent threads by an independence relation I between events [START_REF] Mazurkiewicz | Introduction to trace theory[END_REF]. Similarly, every asynchronous game may be equipped with an independence relation between moves, in order to analyze interference in imperative programming languages. Consider the game model of Idealized Algol formulated by Samson Abramsky and Guy McCusker in [START_REF] Abramsky | Linearity, sharing and state: a fully abstract game semantics for idealized algol with active expressions[END_REF]. Suppose that an independence relation indicates that the moves read and write(n) interfere in the interpretation of the variable type var, for every natural number n. In that case, the interference between read and write(n) induces obstructions ("holes") to the homotopy relation ∼ on the game var, as indicated below:

_ _ ? ? ? ? ? ? read ? ?

Interestingly, the asynchronous definition of innocence adapts smoothly, and remains compositional in the presence of interfering moves (that is, it defines a category). Strategies are not positional anymore, but homotopic: they play according to the homotopy class of the current play. We believe that a geometric account of states and side effects will emerge naturally from this observation. Typically, the "state" of the system would be defined as the homotopy class of the current play; and the analysis of interference between any two such "states" would be resolved topologically. It is encouraging to see that similar intuitions have been already advocated by Uday Reddy in his work on object-based semantics of imperative languages [START_REF] Reddy | Global state considered unnecessary: Introduction to object-based semantics[END_REF].

Conclusion

The theory of asynchronous games is designed to bridge the gap between mainstream game semantics and concurrency theory. The preliminary results of this theory (exposed in this article) are extremely encouraging. We establish indeed that the cardinal notion of sequential game semantics -innocence -follows from elementary principles of concurrency theory, formulated in asynchronous transition systems. We introduce on the way a non-uniform λ-calculus, whose game semantics coincides with a trace semantics performing the syntactic exploration or parsing of λ-terms. This provides a concurrency-friendly picture of the λ-calculus, and firm foundations for a diagrammatic investigation of its syntax and semantics.

  when the move n is Opponent and justified by m, s • n = n when the move n is Opponent and initial, = where is the empty play.

  and n is a Player move, then there exists a unique Opponent move x m -→ y such that X w x ∈ X, • mutual attraction: if X x y ∈ X then either x = y, or there exists an Opponent move x m -→ x and a Player move y n -→ y such that x y , • initial condition: the root * A is an element of X.

  This follows immediately from the fact that {z ∈ D(A) | z ∈ σ • and z ≥ x} ⊇ {z ∈ D(A) | z ∈ σ • and z ≥ y} when x ≤ y. By increasing, one means that the function σ • satisfies the inequality x

Fig. 5 .

 5 Fig. 5. The innocent strategy σ and its four positions in the game B ⊗ Bwhen the sequence[START_REF] Melliès | Asynchronous games 3: an innocent model of linear logic[END_REF] converges to the element -Equation (35) being itself an immediate consequence of Equation[START_REF] Melliès | Sequential algorithms and strongly stable functions[END_REF] and Equation[START_REF] Milner | Fully abstract models of typed lambda-calculi[END_REF].

n-→

  λx.λy.( x(j) -→ Ω α ) m k -→ λx.λy. ( x(j)

  into four "local" tiles:

	q 2	false 2 ? ? ∼ true 1 ? ? ? ? ? ∼ _ _ ? ? ? ? ? ? ? true 1 false 2 _ _ ? ? ? ? ?

∼ q 1

_ _ ? ? ? ? ? ? ? true 1 _ _ ? ? ? ? ? ? ?

q 2

  because m is the only move in t • m justifying the move n. Besides, the resulting play t • m • n is a normal form for extraction, because any step • n = u, this contradicting the fact that t • m is a normal form for view extraction. This proves our claim that t • m • n = t • m • n. We deduce from equations (

	t • m • n	OP u
	would induce a step
	t • m	OP v
	with v

t • m OP t • m induces a sequence of extractions t • m • n OP t • m • n

  Every prefix t • m • n of the play s in which n is a Player move, is of even-length. By definition of a strategy, the two plays t and t•m•n are elements of σ. By Corollary 2, the Player view t • m factors as u • m where u ∈ σ. By definition of the Player

view, t • m = u • m . We apply here the hypothesis that σ is innocent, and deduce from

  O Fig. 1. Backward consistency in which the moves m 1 and m 2 are played by Opponent, and the moves n 1 and n 2 are played by Player. Suppose that the move m 2 is not justified by any of the two moves m 1 and n 1 .

			O O O O
			s 2
	n 2 ? ? ∼ _ _ ? ? ? ? ? ? ? _ _ ? ? ? ? ? m 2 n 1 ? ? ∼ _ _ ? ? ? ? ? m 1 _ _ ? ? ? ? ? m 2 ? ? O O O O	⇒	n 2 ? ? ∼ _ _ ? ? ? ? ? ? ? ∼ _ _ ? ? ? ? ? n 1 ? ? ∼ _ _ ? ? ? ? ? m 1 _ _ ? ? ? ? ? m 2 n 1 ? ? ∼ m 1 O O O O _ _ ? ? ? ? ? m 2 ? ? _ _ ? ? ? ? ? n 2 ? ?	∈ σ
	s 1		s 1

  O

	n 2 ? ? ∼ _ _ ? ? ? ? ? ? ? ∼ _ _ ? ? ? ? ? n 1 ? ? ∼ _ _ ? ? ? ? ? m 1 _ _ ? ? ? ? ? m 2 n 1 ? ? ∼ _ _ ? ? ? ? ? n 2 ? ?
	m 1

Relationality is called "pure positionality" in the extended abstract[START_REF] Melliès | Asynchronous games 2: the true concurrency of innocence[END_REF].