Tom Hirschowitz
email: tom.hirschowitz@univ-savoie.fr

Damien Pous
email: damien.pous@ens-lyon.fr

Innocent strategies as presheaves and interactive equivalences for CCS 1

. We equip innocent strategies with a simple notion of interaction.

We then prove decomposition results for innocent strategies, and, restricting to presheaves of finite ordinals, prove that innocent strategies are a final coalgebra for a polynomial functor [27] derived from the game. This leads to a translation of CCS with recursive equations.

 in concurrency theory. In this framework, we consider analogues of fair testing and must testing. We show that must testing is strictly finer in our model than in CCS, since it avoids what we call 'spatial unfairness'. Still, it differs from fair testing, and we show that it coincides with a relaxed form of fair testing.

Note: This is an expanded version of our ICE '11 paper [19]. It notably simplifies a few aspects of the development, and corrects the mistaken statement that fair and must testing coincide in our semantic framework. Must testing only coincides with a relaxed variant of fair testing. This version also subsumes a previous preprint, providing more compact proofs.

Overview

Theories of programming languages Research in programming languages is mainly technological. Indeed, it heavily relies on techniques which

are ubiquitous in the field, but almost never formally made systematic. Typically, the definition of a language then quotiented by variable renaming (αconversion) appears in many theoretical papers about functional programming languages. Why isn't there yet any abstract framework performing these systematic steps for you? Because the quest for a real theory of programming languages is not achieved yet, in the sense of a corpus of results that actually help developing them or reasoning about them. However, many attempts at such a theory do exist.

A problem for most of them is that they do not account for the dynamics of execution, which limits their range of application. This is for example the case of Fiore et al.'s second-order theories [START_REF] Fiore | Second-order and dependently-sorted abstract syntax[END_REF][START_REF] Hirschowitz | Modules over monads and linearity[END_REF][START_REF] Hirschowitz | Modules over monads and initial semantics[END_REF]. A problem for most of the other theories of programming languages is that they neglect denotational semantics, i.e., they do not provide a notion of model for a given language. This is for example the case of Milner et al.'s bigraphs [START_REF] Jensen | Bigraphs and mobile processes (revised)[END_REF], or of most approaches to structural operational semantics [START_REF] Plotkin | A structural approach to operational semantics[END_REF], with the notable exception of the bialgebraic semantics of Turi and Plotkin [START_REF] Turi | Towards a mathematical operational semantics[END_REF]. A recent, related, and promising approach is Kleene coalgebra, as advocated by Bonsangue et al. [START_REF] Bonsangue | A Kleene theorem for polynomial coalgebras[END_REF]. Finally, higher-order rewriting [START_REF] Nipkow | Higher-order critical pairs[END_REF], and its semantics in double categories [START_REF] Gadducci | The tile model[END_REF] or in cartesian closed 2-categories [START_REF] Hirschowitz | Cartesian closed 2-categories and permutation equivalence in higher-order rewriting[END_REF], is not currently known to adequately account for process calculi.

Towards a new approach The most relevant approaches to us are bialgebraic semantics and Kleene coalgebra, since the programme underlying the present paper concerns a possible alternative. A first difference, which is a bit technical but may be of importance, is that both bialgebraic semantics and Kleene coalgebra are based on labelled transition systems (LTSs), while our approach is based on reduction semantics. This seems relevant, since reduction semantics is often considered more primitive than LTSs, and much work has been devoted to deriving the latter from the former [START_REF] Sewell | From rewrite rules to bisimulation congruences[END_REF][START_REF] Leifer | Deriving bisimulation congruences for reactive systems[END_REF][START_REF] Jensen | Bigraphs and mobile processes (revised)[END_REF][START_REF] Sassone | Deriving bisimulation congruences using 2-categories[END_REF][START_REF] Rathke | Deconstructing behavioural theories of mobility[END_REF].

More generally, our approach puts more emphasis on interaction between programs, and hence is less interesting in cases where there is no interaction. A sort of wild hope is that this might lead to unexpected models of programming languages, e.g., physical ones. This could also involve finding a good notion of morphism between languages, and possibly propose a notion of compilation. At any rate, the framework is not set up yet, so investigating the precise relationship with bialgebraic semantics and Kleene coalgebra is deferred to further work.

How will this new approach look like? Compared to such long-term goals, we only take a small step forward here, by considering a particular case, namely Milner's CCS [START_REF] Milner | A Calculus of Communicating Systems[END_REF], and providing a new view of it. This view borrows ideas from the following lines of research: game semantics [START_REF] Hyland | Semantics and Logics of Computation, chapter Game Semantics[END_REF], and in particular the notion of an innocent strategy, graphical games [START_REF] Delande | A neutral approach to proof and refutation in mall[END_REF][START_REF] André | Contraction-free proofs and finitary games for linear logic[END_REF], Krivine realisability [START_REF] Krivine | Dependent choice, 'quote' and the clock[END_REF], ludics [START_REF] Girard | Locus solum: From the rules of logic to the logic of rules[END_REF], testing equivalences in concurrency [START_REF] De | Testing equivalences for processes[END_REF][START_REF] Beffara | réalisabilité et concurrence[END_REF], the presheaf approach to concurrency [START_REF] Joyal | Bisimulation and open maps[END_REF][START_REF] Kasangian | Observational trees as models for concurrency[END_REF], and sheaves [START_REF] Maclane | Sheaves in Geometry and Logic: A First Introduction to Topos Theory[END_REF]. It is also, more remotely, related to graph rewriting [START_REF] Ehrig | editors[END_REF] and computads [START_REF] Burroni | Higher-dimensional word problems with applications to equational logic[END_REF].

From strategies to presheaves Game semantics [START_REF] Hyland | Semantics and Logics of Computation, chapter Game Semantics[END_REF] has provided fully complete models of programming languages. It is based on the notion of a strategy, i.e., a set of plays in some game, satisfying a few conditions. In concurrency theory, taking as a semantics the set of accepted plays, or 'traces', is known as trace semantics. Trace semantics is generally considered too coarse, since it equates, for a most famous example, the right and the wrong coffee machines, a.pb `cq and ab `ac [START_REF] Milner | A Calculus of Communicating Systems[END_REF].

An observation essentially due to Joyal, Nielsen, and Winskel is that strategies, i.e., prefix-closed sets of plays, are actually particular presheaves of booleans on the category C with plays as objects, and prefix inclusions as morphisms. By presheaves of booleans on C we here mean functors C op Ñ 2, where 2 is the preorder category 0 ď 1. If a play p is accepted, i.e., mapped to 1, then its prefix inclusions q ãÑ p are mapped to the unique morphism with domain 1, i.e., id 1 , which entails that q is also accepted.

Following Joyal, Nielsen, and Winskel, we observe that considering instead presheaves (of sets) on C yields a much finer semantics. So, a play p is now mapped to a set Sppq, to be thought of as the set of ways for p to be accepted by the strategy S. Considering the set of players as a team, Sppq may also be thought of as the set of possible states of the team after playing p -which is empty if the team never accepts to play p.

This presheaf semantics is fine enough to account for bisimilarity [START_REF] Joyal | Bisimulation and open maps[END_REF][START_REF] Kasangian | Observational trees as models for concurrency[END_REF]. Indeed, presheaves are essentially forests with edges labelled by moves. For example, in the setting where plays are finite words on an alphabet, the wrong coffee machine may be represented by the presheaf S defined by the equations on the left and pictured as on the right: Spǫq " t‹u, Spaq " tx, x 1 u, Spabq " tyu, Spacq " ty 1 u,

Spǫ ãÑ aq " tx Þ Ñ ‹, x 1 Þ Ñ ‹u, Spa ãÑ abq " ty Þ Ñ xu, Spa ãÑ acq " ty 1 Þ Ñ x 1 u : ‹ x x 1 y y 1 . a a b c
So, in summary: the standard notion of strategy may be generalised to account for branching equivalences, by passing from presheaves of booleans to presheaves of sets.

Multiple players Traditional game semantics mostly emphasises twoplayer games. There is an implicit appearance of three-player games in the definition of composition of strategies, and of four-player games in the proof of its associativity, but these games are never given a proper status.

A central idea of graphical games, and to a lesser extent of ludics, is the emphasis on multiple-player games.

Here, there first is a base category B of positions, whose objects represent configurations of players. Since the game represents CCS, it should be natural that players are related to each other via the knowledge of communication channels. So, roughly, positions are bipartite graphs with vertex sets players and channels, and edges from channels to players indicating when the former is known to the latter. As a first approximation, morphisms of positions may be thought of as just embeddings of such graphs.

Second, there is a category E of plays, with a functor to B sending each play to its initial position. Plays are represented in a more flexible way than just sequences of moves, namely using a kind of string diagrams. This echoes the idea [START_REF] Melliès | Asynchronous games 2: the true concurrency of innocence[END_REF] that two moves may be independent, and that plays should not depend on the order in which two independent moves are performed. Furthermore, our plays are a rather general notion, allowing, e.g., to focus on a given player. Morphisms of plays account both for:

• prefix inclusion, i.e., inclusion of a play into a longer play, and

• position enlargement, e.g., inclusion of information about some players into information about more players. Now, restricting to plays over a given initial position X, and then taking presheaves on this category E X , we have a category of strategies on X.

Innocence A fundamental idea of game semantics is the notion of innocence, which says that players have a restricted view of the play, and that their actions may only depend on that view.

We implement this here by defining a subcategory V X ãÑ E X of views on X, and deeming a presheaf F on E X innocent when it is determined by its restriction F 1 to V X , in the sense that it is isomorphic to the right Kan extension [START_REF] Mac | Categories for the Working Mathematician[END_REF] of F 1 along V op X ãÑ E op X . We then define innocent strategies to be just presheaves on V X , and view them as (naive) strategies via the (essential) embedding y V X ãÑ x E X induced by right Kan extension.

Interaction For each position X, we thus have a category S X " y V X of innocent strategies. In game semantics, composition of strategies is achieved in two steps: interaction and hiding. Essentially, interaction amounts to considering the three-player game obtained by letting two two-player games interact at a common interface. Hiding then forgets what happens at that interface, to recover a proper two-player game.

We have not yet investigated hiding in our approach, but, thanks to the central status of multiple-player games, interaction is accounted for in a very streamlined way. For any position X with two subpositions X 1 ãÑ X and X 2 ãÑ X such that each player is in either X 1 or X 2 , but none is in both, given innocent strategies F 1 P S X 1 and F 2 P S X 2 , there is a unique innocent strategy, the amalgamation rF 1 , F 2 s of F 1 and F 2 , whose restrictions to X 1 and X 2 are F 1 and F 2 .

Amalgamation in this sense models interaction in the sense of game semantics, and, using the correspondence with presheaves on E X given by right Kan extension, it is the key to defining interactive equivalences.

CCS Next, we define a translation of CCS terms with recursive equations into innocent strategies. This rests on spatial and temporal decomposition results for innocent strategies. Spatial decomposition says that giving a strategy on a position X is the same as giving a strategy for each of its players. Temporal decomposition says that a strategy is determined up to isomorphism by its set of initial states, plus what remains of each of them after each basic move. Restricting to presheaves of finite ordinals, we also prove that innocent strategies form a final coalgebra for a polynomial functor (in the sense of Kock [START_REF] Kock | Polynomial functors and trees[END_REF]) derived from the game, thus hinting at links with Kleene coalgebra. It is then easy to translate finite CCS into the language induced by our polynomial functor, and to finally extend the translation to CCS with recursive equations via infinite unfolding.

A natural question is then: which equivalence does this translation induce on CCS terms? As explained in the following paragraph, we provide some preliminary results about interactive equivalences, but essentially leave the question open.

Interactive equivalences Returning to our model, we then define a notion of interactive equivalence, which is close in spirit to both testing equivalences in concurrency theory and Krivine realisability and ludics.

The game, as sketched above, allows interacting with players which are not part of the considered position. E.g., a player in the considered position X may perform an input which is not part of any synchronisation. A test for an innocent strategy F on X is then, roughly, an innocent strategy G on a position X 1 with the same channels as X. To decide whether F passes the test G, we consider a restricted variant of the game on the 'union' X Y X 1 , forbidding any interaction with the outside. We call that variant the closedworld game.

Then F passes G iff the amalgamation rF, Gs, right Kan extended to E XYX 1 and then restricted to the closed-world game, belongs to some initially fixed class of strategies, K K XYX 1 . Finally, two innocent strategies F and F 1 on X are equivalent when they pass the same tests.

Here are two examples for K K. Consider a tick move, fixed in advance. Then call successful all plays containing at least one tick, and accordingly call successful all states reached after a successful play. One may consider:

• K K m , consisting of strategies whose maximal states (those that admit no strict extensions) are all successful; the tick move plays a rôle analogous to the daimon in ludics: it is the only move which is observable from the outside;

• K K f , consisting of strategies in which all states on finite plays admit a successful extension.

From the classical concurrency theory point of view on behavioural equivalences, the first choice clearly mimicks must testing equivalence, while the second mimicks fair testing equivalence [START_REF] Natarajan | Divergence and fair testing[END_REF][START_REF] Brinksma | Fair testing[END_REF]. Consider the processes Ω and Ω|a, where Ω is a process doing infinitely many silent transitions. These processes are intuitively quite different: the latter can do an output on the channel a, while the former cannot. They are however equated by standard must testing equivalence: the infinite trace provided by Ω may prevent the output prefix from being performed. In fact, must testing equivalence heavily relies on the potential unfairness of the scheduler. In the literature, this peculiar behaviour actually motivates the introduction of fair testing equivalence.

In contrast, our notion of play is more flexible than standard traces, so that our counterpart to must testing equivalence actually distinguishes these two processes: the infinite play where the output prefix is not performed is not maximal, so that the corresponding unfair behaviour is not taken into account. In other words, thanks to our notion of play, the rather natural notion of must testing already avoids what we call 'spatial unfairness'. However, must testing does not coincide with fair testing in our setting, because there are other sources of unfairness, that are not handled properly. Technically, we prove that K K m coincides with the set of strategies whose states all admit a successful extension. However, the restriction to finite plays in the definition of K K f is required to rule out other sources of unfairness.

Summary In summary, our approach emphasises a flexible notion of multiple-player play, encompassing both views in the sense of game semantics, closed-world plays, and intermediate notions. Strategies are then described as presheaves on plays, while innocent strategies are presheaves on views. Innocent strategies admit a notion of interaction, or amalgamation, and are embedded into strategies via right Kan extension. This allows a notion of testing, or interactive equivalence by amalgamation with the test, right Kan extension, and finally restriction to closed-world.

Our main technical contributions are then a translation of CCS terms with recursive equations into innocent strategies, and the study of fair and must equivalences in our setting.

Perspectives Our next task is clearly to tighten the link with CCS. Namely, we should explore which equivalence on CCS is induced via our translation, for a given interactive equivalence. We will start with K K f . Furthermore, the very notion of interactive equivalence might deserve closer consideration. Its current form is rather ad hoc, and one could hope to see it emerge more naturally from the game. For instance, the fixed class K K of 'successful' strategies should probably be more constrained than is done here. Also, the paradigm of observing via the set of successful tests might admit sensible refinements, e.g., probabilistic ones.

Another possible research direction is to tighten the link with 'graphical' approaches to rewriting, such as graph rewriting or computads. E.g., our plays might be presented by a computad [START_REF] Guiraud | Higher-dimensional categories with finite derivation type[END_REF], or be the bicategory of rewrite sequences up to shift equivalence, generated by a graph grammar in the sense of Gadducci et al. [START_REF] Gadducci | A bi-categorical axiomatisation of concurrent graph rewriting[END_REF]. Both goals might require some technical adjustments, however. For computads, we would need the usual yoga of U-turns to flexibly model our positions; e.g., zigzags of U-turns are usually only equal up to a higher-dimensional cell, while they would map to equal positions in our setting. For graph rewriting, the problem is that our positions are not exactly graphs (e.g., the channels known to a player are linearly ordered).

Other perspectives include the treatment of more complicated calculi like π or λ. In particular, calculi with duplication of terms will pose a serious challenge. An even longer-term hope is to be able to abstract over our approach. Is it possible to systematise the process starting from a calculus as studied in programming language theory, and generating its strategies modulo interactive equivalence? If this is ever understood, the next question is: when does a translation between two such calculi preserve a given interactive equivalence? Finding general criteria for this might have useful implications in programming languages, especially compilation.

Notation Throughout the paper, we abusively identify n with t1 . . . nu, for readability. So, e.g., i P n means i P t1, . . . , nu.

F C F C 1 GD GD 1 F pf q u u 1

Gpgq

The various categories and functors constructed in the development are summed up with a short description in Table 1. There, given two functors C F Ý Ñ E G Ð Ý D, we denote (slightly abusively) by C Ó E D the comma category: it has as objects triples pC, D, uq with C P C, D P D, and u : F pCq Ñ GpDq in E, and as morphisms pC, D, uq Ñ pC 1 , D 1 , u 1 q pairs pf, gq making the square above commute. Also, when F is the identity on C and G : 1 Ñ C is an object C of C, this yields the usual slice category, which we abbreviate as C{C. Finally, the category of presheaves on any category C is denoted by p C " rC op , Sets.

We denote by obpCq the set of objects of any small category C. For any functor F : C Ñ D, we denote by F op : C op Ñ D op the functor induced on opposite categories, defined exactly as F on both objects and morphisms. Also, recall that an embedding of categories is an injective-on-objects, faithful functor. This admits the following generalisation: a functor F : C Ñ D is essentially injective on objects when F C -F C 1 implies C -C 1 . Any faithful, essentially injective on objects functor is called an essential embedding.

Category

Description of its objects

p C 'diagrams' B ãÑ p C positions E ãÑ pB Ó p C p Cq plays E X " pE Ó B pB{Xqq plays on a position X V X ãÑ E X views on X S X " y V X innocent strategies on X W ãÑ E closed-

Plays as string diagrams

We now describe our approach more precisely, starting with the category of multiple-player plays. For the sake of clarity, we first describe this category in an informal way, before giving the precise definition (Section 3).

Positions

Since the game represents CCS, it should be natural that players are related to each other via the knowledge of communication channels. This is represented by a kind of4 finite, bipartite graph: an example position is on the right. Bullets represent players, circles represent channels, and edges indicate when a player knows a channel. The channels known by a player are linearly ordered. Formally, as explained in Section 3, positions are presheaves over a certain category C 1 . Morphisms of positions are natural transformations, which are roughly morphisms of graphs, mapping players to players and channels to channels. In full generality, morphisms thus do not have to be injective, but include in particular embeddings of positions in the intuitive sense. Positions and morphisms between them form a category B.

Moves

Plays will be defined as glueings of moves between positions. Moves are derived from the very definition of CCS, as we now sketch. The diagrams we draw in this section will be given a very precise combinatorial definition in Section 3.

Let us start with the forking move, which corresponds to parallel composition in CCS: a process (the player) forks into two sub-processes. In the case of a player knowing two channels, the forking move is represented by the diagram , [START_REF] Beffara | réalisabilité et concurrence[END_REF] to be thought of as a move from the bottom position X (with one player p) to the top position Y . (with two players, which we call the 'avatars' of p). The left-and right-hand borders are just channels evolving in time, not noticing that the represented player forks into two. The surfaces spread between those vertical lines represent links (edges in the involved positions) evolving in time. For example, each link here divides into two when the player forks, thus representing the fact that both of the avatars retain knowledge of the corresponding channel. There is of course an instance π n of forking for each n, according to the number of channels known to the player. As for channels known to a player, the players and channels touching the black triangle are ordered: there are different 'ports' for the initial player and its two avatars.

We then have a tick move ♥ n , whose role is to define successful plays, and a move for the channel creation or restriction of CCS, here ν n . In the case where the player knows two channels, they are graphically represented as ♥ and respectively. As expected, there is an instance of each of these two moves for each number n of channels known to the player.

We also need a move to model CCS-like synchronisation, between two players. For all n and m, representing the numbers of channels known to the players involved in the synchronisation, and for all i P n, j P m, there is a synchronisation τ n,i,m,j , represented, in the case where one player outputs on channel 3 P 3 and the other inputs on channel 1 P 2, by .

As we shall see in Section 3, the dotted wire in the picture is actually a point in the formal representation (i.e., an element of the corresponding presheaf).

The above four kinds of moves (forking, tick, channel creation, and synchronisation) come from the reduction semantics of CCS. We classify these as closed-world moves, since they correspond to the evolution of a group of players in isolation.

We however need a more fine-grained structure for moves: moves whose final position has more than one player (forking and synchronisation) must be decomposed into basic moves, to get an appropriate notion of view.

We introduce two sub-moves for forking: left and right half-forking. In the case where the player knows two channels, they are represented by the following diagrams, respectively: and .

(2)

These sub-moves represent what each of the 'avatars' of the forking player sees of the move. We call π l n and π r n the respective instances of the left-hand and right-hand basic moves for a player knowing n channels. Formally, there will be injections from the left and right half-forking moves to the corresponding forking moves.

We finally decompose synchronisation into an input move and an output move: a.P and a.P in CCS become o n,i and ι n,i here (where n is the number of known channels, i P t1 . . . nu is the index of the channel bearing the synchronisation). Here, output on the right-hand channel and input on the left-hand channel respectively look like and .

(3) Like with forking, there will be injections from the input and output moves to the corresponding synchronisation moves.

All in all, there are three classes of moves, which we summarise in Table 2.

• Tick, channel creation, half-forking, and input/output moves are basic moves: they evolve from a position with exactly one player to another position with exactly one player. These moves are used to define views later on.

• Forking, synchronisation, tick and channel creation moves are closedworld moves: they correspond to the case where a group of players evolves on its own, in isolation; they are central to the notion of interactive equivalence.

• We need a third class of moves, called full, which consists of forking, input, output, tick and channel creation. They involve a single player and all of its avatars. They appear, e.g., in the statement of Lemma 12, which is a partial correctness criterion for closed-world plays.

Formally, we define moves as cospans X ãÑ P Ðâ Y in the category of diagrams (technically a presheaf category p C-see Section 3), where X is the initial position and Y the final one. Both legs of the cospan are actually monic morphisms in p C, as will be the case for all cospans considered here.

Plays

We now sketch how plays are defined as glueings of moves. We start with the following example, depicted in Figure 1. The initial position consists of two players p 1 and p 2 sharing knowledge of a channel a, each of them knowing another channel, resp. a 1 and a 2 . The play consists of four moves: first p 1 forks into p 1,1 and p 1,2 , then p 2 forks into p 2,1 and p 2,2 , and then p 1,1 does a left half-fork into p 1,1,1 ; finally p 1,1,1 synchronises (as the sender) with p 2,1 . Now, we reach the limits of the graphical representation, but the order in which p 1 and p 2 fork is irrelevant: if p 2 forks before p 1 , we obtain the same play. This means that glueing the various parts of the picture in Figure 1 in different orders formally yields the same result (although there are subtle issues in representing this result graphically in a canonical way).

Let us now sketch a definition of plays. Recall that moves may be seen as cospans X ãÑ M Ðâ Y , and consider an extended notion of move, which may occur in a position not limited to players involved in the move. For example, the moves in Figure 1 are extended moves in this sense.

Definition 1 A play is an embedding X 0 ãÑ U in the category p C of diagrams, isomorphic to a possibly denumerable 'composition' of moves in the (bi)category Cospanp p Cq of cospans in p C, i.e., obtained as a colimit:

X 0 X 1 . . . X n X n`1 X n`2 . . . M 0 . . . M n M n`1 . . . U, . p 1 p 2 a a 1 a 2 Figure 1: An example play
where each X i ãÑ M i Ðâ X i`1 is an extended move.

We often denote plays just by U , leaving the embedding X ãÑ U implicit.

Remark 1 For finite plays, one might want to keep track not only of the initial position, but also of the final position. This indeed makes sense. Finite plays then compose 'vertically', and form a double category. But infinite plays do not really have any final position, which explains our definition.

U V X Y. h k
Let a morphism pX ãÑ U q Ñ pY ãÑ V q of plays be a pair ph, kq making the diagram on the right commute in p C. This permits both inclusion 'in width' and 'in height'. E.g., the play consisting of the left-hand basic move in (2) embeds in exactly two ways into the play of Figure 1. (Only two because the image of the base position must lie in the base position of the codomain.) We have:

Proposition 1 Plays and morphisms between them form a category E.

There is a projection functor E Ñ B mapping each play X ãÑ U to its base position X. This functor has a section, which is an embedding B ãÑ E, mapping each position X to the 'identity' play X ãÑ X on X.

Remark 2 (Size) The category E is only locally small. Since presheaves on a locally small category are less well-behaved than on a small category, we will actually consider a skeleton of E. Because E consists only of denumerable presheaves, this skeleton is a small category. Thus, our presheaves in the next section may be understood as taken on a small category.

Remark 3 Plays are not very far from being just (infinite) abstract syntax trees (or forests) 'glued together along channels'. E.g., the play from Figure 1 is the glueing of, say pπ l 2 pa.0qq|0 and a|0 along a.

Relativisation

If we now want to restrict to plays over a given base position X, we may consider Definition 2 Let the category E X have

• as objects pairs of a play Y ãÑ U and a morphism Y Ñ X,

• as morphisms pY ãÑ U q Ñ pY 1 ãÑ U 1 q all pairs ph, kq making the diagram

U U 1 Y Y 1 X k h commute in p C.
We will usually abbreviate U Ðâ Y Ñ X as just U when no ambiguity arises. As for morphisms of positions, in full generality, h and k, as well as the morphisms Y Ñ X, do not have to be injective.

Example 1 Let X be the position . The play in Figure 1, say Y ãÑ U , equipped with the injection Y ãÑ X mapping the two players of Y to the two leftmost players of X, is an object of E X .

One naively could imagine that the objects E X could just consist of plays X ãÑ U on X. However, spatial decomposition, Theorem 1, relies on our slightly more complex definition. E.g., still in Figure 1, this allows us to distinguish between the identity view r2s r2s

p 1
ãÝ Ñ X on p 1 from the identity view r2s r2s

p 2
ãÝ Ñ X on p 2 , which would otherwise not be possible.

Diagrams

In this section, we define the category on which the string diagrams of the previous section are presheaves. The techniques used here date back at least to Carboni and Johnstone [START_REF] Carboni | Connected limits, familial representability and artin glueing[END_REF][START_REF] Carboni | Corrigenda for 'connected limits, familial representability and artin glueing[END_REF].

First steps

Let us first consider two small examples. It is well-known that directed graphs form a presheaf category: consider the category C freely generated by the graph with two vertices, say ‹ and r1s, and two edges d, c : ‹ Ñ r1s between them. One way to visualise this is to compute the category of elements of a few presheaves on C. Recall that the category of elements of a presheaf F on C is the comma category y Ó p C F , where y is the Yoneda embedding. Via Yoneda, it has as elements pairs pC, xq with C P obpCq and x P F pCq, and morphisms pC, xq Ñ pD, yq morphisms f : C Ñ D in C such that F pf qpyq " x (which we abbreviate as y ¨f " x when the context is clear).

Example 2 Consider the graph

0 1 2 e e 1
with three vertices 0, 1, and 2, and two edges e and e 1 . This graph is represented by the presheaf F defined by the following equations, whose category of elements is actually freely generated by the graph on the right:

• F p‹q " t0, 1, 2u, • F pr1sq " te, e 1 u,
• e ¨d " 0,

• e ¨c " 1,

• e 1 ¨d " 1,

• e 1 ¨c " 2, 1 e e 1 0 2. d c d c
This latter graph is not exactly the original one, but it does represent it. Indeed, for each vertex we know whether it is in F p‹q or F pr1sq, hence whether it represents a 'vertex' or an 'edge'. The arrows all go from a 'vertex' v to an 'edge' e. They lie over d when v is the domain of e, and over c when v is the codomain of e.

Multigraphs, i.e., graphs whose edges have a list of sources instead of just one, may also be seen as a presheaves on the category freely generated by the graph with

• as vertices: one special vertex ‹, plus for each natural number n a vertex, say, rns; and

• for all n P N, n `1 edges ‹ Ñ rns, called d 1 , . . . , d n , and c.

It should be natural for presheaves on this category to look like multigraphs: the elements of a presheaf F over ‹ are the vertices in the multigraph, the elements over rns are the n-ary multiedges, and the action of the d i 's give the ith source of a multiedge, while the action of c gives its target.

Example 3 Similarly, computing a few categories of elements might help visualising. As above, consider F defined by

• F p‹q " t0, 1, 2, 3, 4, 5u,

• F pr1sq " F pr0sq " H,

• F pr2sq " te 1 u,

• F pr3sq " teu,

• F prn `4sq " H,

• e ¨c " 0,

• e ¨d1 " 1,

• e ¨d2 " 2,

• e ¨d3 " 3,

• e 1 ¨c " 1,

• e 1 ¨d1 " 4,

• e 1 ¨d2 " 5, whose category of elements is freely generated by the graph:

0 e 1 2 3 e 1 4 5. c d 1 c d 2 d 3 d 1 d 2
Now, this pattern may be extended to higher dimensions. Consider for example extending the previous base graph with a vertex rm 1 , . . . , m n ; ps for all natural numbers n, p, m 1 , . . . , m n , plus edges s 1 : rm 1 s Ñ rm 1 , . . . , m n ; ps, . . . , s n : rm n s Ñ rm 1 , . . . , m n ; ps, and t : rps Ñ rm 1 , . . . , m n ; ps.

Let now C be the free category on this extended graph. Presheaves on C are a kind of 2-multigraphs: they have vertices, multiedges, and multiedges between multiedges.

We could continue this in higher dimensions.

Constructing the base category

Our base category follows a very similar pattern. We start from a slightly different graph: let G 0 have just one vertex ‹; let G 1 , have one vertex ‹, plus a vertex rns for each natural number n, plus n edges d 1 , . . . , d n : ‹ Ñ rns.

Let C 0 and C 1 be the categories freely generated by G 0 and G 1 , respectively. So, presheaves on C 1 are a kind of hypergraphs with arity (since vertices incident to a hyperedge are numbered). This is enough to model positions.

Example 4

The position drawn at the beginning of Section 2.1 may be represented as the presheaf

• ‹ Þ Ñ t1, 2, 3u, • r2s Þ Ñ tx, zu, • r3s Þ Ñ tyu, • Þ Ñ H, • x ¨d1 " 1, • x ¨d2 " 2,
• z ¨d1 " 2,

• z ¨d2 " 3,

• y ¨d1 " 1,

• y ¨d2 " 2,

• y ¨d3 " 3, whose category of elements is:

1 3 x y z 2. d 1 d 1 d 3 d 2 d 2 d 2 d 1
Now, consider the graph G 2 , which is G 1 augmented with:

• for all n, vertices ♥ n , π l n , π r n , ν n ,

• for all n and 1 ď i ď n, vertices o n,i and ι n,i ,

• for all n, edges s, t : rns Ñ ♥ n , s, t : rns Ñ π l n , s, t : rns Ñ π r n , s : rns Ñ ν n , t : rn `1s Ñ ν n ,

• for all n and 1 ď i ď n, edges s, t : rns Ñ o n,i , s, t : rns Ñ ι n,i .

We slightly abuse language here by calling all these t's and s's the same. We could label them with their codomain, but we refrain from doing so for the sake of readability. Now, let C 2 be the category generated by G 2 and the relations s ˝di " t ˝di for all n and 1 ď i ď n (for all sensible-common-codomains). The intuition here is that for any basic move by a player with n channels, these n channels remain the same after the move. This includes the case of ν n , for which the absence of any equation involving the new channel makes it different from the others.

Example 5 Again, computing a few categories of elements is in order. For example, the category of elements of (the representable presheaf on) ι 3,3 is the poset freely generated by the graph

td 1 t td 3 td 2 id ι 3,3 sd 1 s sd 3 sd 2 ,
to be compared with the corresponding pictures (3).

Example 6 Similarly, the category of elements of ν 1 is the poset freely generated by the graph

td 1 t td 2 id ν 1 sd 1 s.
Note that only channel creation changes the number of channels known to the player, and accordingly the corresponding morphism t has domain rn`1s.

Presheaves on C 2 are enough to model basic moves, but since we want more, we continue, as follows.

Let G 3 be G 2 , augmented with:

• for all n, a vertex π n , and

• edges l : π l n Ñ π n and r : π r n Ñ π n .
Definition 3 Let C 3 be the category generated by G 3 , the previous relations, plus the relations l ˝s " r ˝s.

The equation models the fact that a forking move should be played by just one player. We also call s " l ˝s " r ˝s the common composite, which gives a uniform notation for the initial player of full moves.

Example 7

The category of elements of π 2 is the poset freely generated by the graph

ltd 1 " rtd 1 lt rt ltd 2 " rtd 2 l id π 2 r lsd 1 " rsd 1 ls " rs lsd 2 " rsd 2 .
The two views corresponding to left and right half-forking are subcategories, and the object id π 2 'ties them together'.

Presheaves on C 3 are enough to model full moves; to model closed-world moves, and in particular synchronisation, we continue as follows.

Let G 4 be G 3 , augmented with, for all n, m, 1 ď i ď n, and 1 ď j ď m,

• a vertex τ n,i,m,j , and This equation is the exact point where we enforce that a synchronisation involves an input and an output on the same channel, as announced in Example 5.

• edges ǫ : o n,i Ñ τ n,i

Example 8

The category of elements of τ 3,3,1,1 is the preorder freely generated by the graph

ǫtd 1 ǫt ǫtd 3 " ρtd 1 ρt ρtd 2 ǫtd 2 ǫ id τ 3,3,2,1 ρ ǫsd 1 ǫs ǫsd 3 " ρsd 1 ρs ρsd 2 ǫsd 2 .
Again, the two views corresponding to ι 3,3 and ι 2,1 are subcategories, and the new object τ 3,3,2,1 ties them together.

Positions and moves

We have now defined the base category C " C 4 on which the string diagrams of Section 2 are presheaves. More accurately we have defined a sequence C 0 ãÑ . . . ãÑ C 4 of subcategories.

Positions Positions are finite presheaves on C 1 , or equivalently, finite presheaves on C 4 empty except over C 1 .

Moves Basic moves should be essentially representable presheaves on objects in obpC 2 qz obpC 1 q. Recall however that basic moves are defined as particular cospans in p C. This is also easy: in the generating graph G 2 , each such object c has exactly two morphisms s and t into it, from objects, say, rn s s and rn t s, respectively. By Yoneda, these induce a cospan

rn s s s Ý Ñ c t Ð Ý rn t s in p
C, which is the desired cospan. (Observe, again, that only ν n has n s ‰ n t .)

Similarly, full moves either are basic moves, or are essentially representable presheaves on objects in obpC 3 qz obpC 1 q, i.e., representables on some π n . To define the expected cospan, first observe that by the equation ls " rs, we obtain an morphism rns

s Ý Ñ π l n l Ý Ñ π n , equal to rs, in p
C. This will form the first leg of the cospan. For the other, observe that for each n and i P n, we obtain, by the equations ltd i " lsd i " rsd i " rtd i and by Yoneda, that the outermost part of

n ¨‹ rns rns n|n π r n π l n π n rd i s iPn rd i s iPn t t r l t (4)
commutes in p C, where n ¨‹ denotes an n-fold coproduct of ‹. Letting n|n be the induced pushout, and the dashed morphism t be obtained by its universal property, we obtain the desired cospan rns ls Ý Ñ π n t Ð Ý n|n. Finally, closed-world moves either are full moves, or are essentially representable presheaves on some τ n,i,m,j . To define the expected cospan, we proceed as in Figure 2: compute the pushout n i | j m, and infer the dashed morphisms s 1 and t 1 to obtain the desired cospan

n i | j m s 1 Ý Ñ τ n,i,m,j t 1 Ð Ý n i | j m.
Remark 4 (Isomorphisms) Moves are particular cospans in p C. For certain moves, the involved objects are representable, but not for others, like forking or synchronisation, whose final position is not representable. In the latter cases, our definition thus relies on a choice, e.g., of pushout in (4). Thus, let us be completely accurate: a move is a cospan which is isomorphic to one of the cospans chosen above, in p C ¨Ð¨Ñ¨, i.e., the category of functors

‹ rms rns n i | j m ‹ ι m,j o n,i τ n,i,m,j ‹ rms rns n i | j m t s d i d j d i d j d i d j t s t 1 s 1

Extended moves, plays, and relativisation

The most delicate part of our formalisation of Section 3 is perhaps the passage from moves to extended moves. Recall from the paragraph above Definition 1 that an extended move should be like a move occurring in a larger position.

Moves with interfaces

To formalise this idea, we first equip moves with interfaces, as standard in graph rewriting [START_REF] Johnstone | Quasitoposes, quasiadhesive categories and Artin glueing[END_REF]. Since moves are cospans, one might expect that interfaces are cospans too. This may be done, but there is a simpler, equivalent presentation. The route we follow here might have to be generalised in order to handle more complex calculi than CCS, but let us save the complications for later work.

Here, we define an interface for a cospan X Ñ M Ð Y to consist of a presheaf I and morphisms

X Ð I Ñ Y such that I Y X M (5)
commutes, and I has dimension 0, i.e., is empty except over C 0 , i.e., consists only of channels.

Definition 5 A cospan equipped with an interface is called a cospan with interface.

Moves are particular cospans, and we now equip them with canonical interfaces: all moves except channel creation preserve the set of channels, the interface is then n ¨‹, with the obvious inclusion. For example, the less obvious case is π n : we choose

n ¨‹ n|n rns π n ,
where the upper map is as in (4). For channel creation, we naturally choose n ¨‹ rn `1s rns ν n .

rd i s iPn Definition 6 A move with interface is one of these cospans with interface. The basic, full, or closed-world character is retained from the underlying move.

Extended moves We now plug moves with interfaces into contexts, in the following sense.

Definition 7 A context for a cospan with interface (5) is a position Z, equipped with a morphism I Ñ Z.

From any cospan with interface µ as in (5) and context C : I Ñ Z, we construct the cospan Crµs as in:

Y Y 1 M M 1 I Z X X 1 .
C I.e., we push the available morphisms out of I along C, and infer the dashed morphisms, which form the desired cospan.

Definition 8 An extended move is a cospan of the shape Crµs, for any move with interface µ and context C as above.

Example 9 Recall that r2s is a position with one player knowing two channels. Recall from Figure 2 the pushout

‹ r2s r2s 2 2 | 1 2, d 1 d 2 p 1 p 2
equivalently obtained as the pushout

‹ `‹ ‹ `r2s r2s 2 2 | 1 2. id‹`d 1 rd 1 ,d 2 s p 1 ra 1 ,p 2 s
The base position of Figure 1 is thus 2 2 | 1 2. Recall also from (4) that 2|2 denotes the position with two players both knowing two channels. Now, we have the forking move r2s ãÑ π 2 Ðâ 2|2. Equipping it with the interface rd 1 , d 2 s : ‹ `‹ Ñ r2s, and putting it in the context id ‹ `d1 : ‹ `‹ Ñ ‹ `r2s, (which happens to be the same as the interface), we obtain

2|2 p2|2q 2 | 1 2 π 2 M ‹ `‹ ‹ `r2s r2s 2 2 | 1 2. rd 1 ,d 2 s id‹`d 1
This formally constructs the first layer of Figure 1. Constructing the whole play would be a little too verbose to be included here, but essentially straightforward.

Plays and relativisation

We may now read Definition 1 again, this time in the formal setting, to define plays. Similarly, the definition of morphisms now makes rigorous sense, as well as Proposition 1.

Proof of Proposition 1: E is the full subcategory of the arrow category of p C whose objects are plays. l Similarly, Section 2.4 now makes rigorous sense.

Innocent strategies as sheaves

Now that the category of plays is defined, we move on to defining innocent strategies. There is a notion of a Grothendieck site [START_REF] Maclane | Sheaves in Geometry and Logic: A First Introduction to Topos Theory[END_REF], which consists of a category equipped with a (generalised) topology. On such sites, one may define a category of sheaves, which are very roughly the presheaves that are determined locally w.r.t. the generalised topology. We claim that there is a topology on each E X , for which sheaves adequately model innocent strategies. Fortunately, in our setting, sheaves admit a simple description, so that we can avoid the whole machinery. But sheaves were the way we arrived at the main ideas presented here, because they convey the right intuition: plays form a Grothendieck site, and the states of innocent strategies should be determined locally.

In this section, we first define innocent strategies, and state the spatial and temporal decomposition theorems. We then present our coalgebraic interpretation of innocent strategies, i.e., we define a polynomial endofunctor F, and show that presheaves of finite ordinals on views form a final F-coalgebra. We then derive from this a formal language and its interpretation in terms of innocent strategies. We finally use this language to translate CCS with recursive equations into innocent strategies.

Innocent strategies

Definition 9 A view is a finite, possibly empty 'composition' rns ãÑ V of (extended) basic moves in Cospanp p Cq, i.e., a play in which all the cospans are basic moves.

When the composition is empty, we obtain rns ãÑ rns, the identity view on rns. We also note in passing that empty presheaves cannot be views, i.e., X ãÑ H is never a view.

Example 10 Forking (1) has two non-trivial views, namely the (left legs of ) basic moves [START_REF] Bonsangue | A Kleene theorem for polynomial coalgebras[END_REF]. Each of them embeds into forking: . Example 11 In Figure 1, the leftmost branch contains a view consisting of three basic moves: two π l 2 and an output. Definition 10 For any position X, let V X be the full subcategory of E X consisting of views.

More precisely, V X consists of spans U Ðâ Y Ñ X where Y ãÑ U is a view. Definition 11 Let the category S X of innocent strategies on X be the category y V X of presheaves on V X .

A possible interpretation is that for a presheaf F P y V X and view V P V X , F pV q is the set of possible states of the strategy F after playing V .

It might thus seem that we could content ourselves with defining only views, as opposed to plays. However, in order to define interactive equivalences in Section 5, we need to view innocent strategies as (particular) presheaves on the whole of E X .

C D E F G H K α 1 ε α
The connection is as follows. Recall from MacLane [START_REF] Mac | Categories for the Working Mathematician[END_REF] the notion of right Kan extension. Given functors F and G as on the right, a right Kan extension Ran F pGq of G along F is a functor H : D Ñ E, equipped with a natural transformation ε : HF Ñ G, such that for all functors K : D Ñ E and transformations α : KF Ñ G, there is a unique α 1 : K Ñ H such that α " ε ' pα 1 ˝id F q, where ' is vertical composition of natural transformations. Now, precomposition with F induces a functor CatpF, Eq : CatpD, Eq Ñ CatpC, Eq, where CatpD, Eq is the category of functors D Ñ E and natural transformations between them. When E is complete, right Kan extensions always exist (and an explicit formula for our setting is given below), and choosing one of them for each functor C Ñ E induces a right adjoint to CatpF, Eq. Furthermore, it is known that when F is full and faithful, then ε is a natural isomorphism, i.e., HF -G.

Proposition 2 If F is full and faithful, then Ran F is a full essential embedding.

Proof: First, let us show that Ran F is essentially injective on objects. Indeed, assume H " Ran F pGq, Ran F pG 1 q " H 1 , and i : H Ñ H 1 is an isomorphism with inverse k. We must construct an isomorphism G -

G 1 . Let j : G Ñ G 1 be ε G 1 ' piF q ' ε ´1 G . Similarly, let l : G 1 Ñ G be ε G ' pkF q ' ε ´1 G 1 . We have l ' j " ε G ' pkF q ' ε ´1 G 1 ' ε G 1 ' piF q ' ε ´1 G " ε G ' pkF q ' piF q ' ε ´1 G " ε G ' ppk ' iq ˝F q ' ε ´1 G " ε G ' ε ´1 G " id G .
Similarly, j ' l " id G 1 and we have G -G 1 .

To see that Ran F is full, observe that for any i :

H Ñ H 1 , with H " Ran F pGq and H 1 " Ran F pG 1 q, j " ε G 1 ' piF q ' ε ´1 G is an antecedent of i by Ran F . Indeed, by definition, Ran F pjq is the unique i 1 : H Ñ H 1 such that ε G 1 ' pi 1 F q " j ' ε G . But the latter is equal to ε G 1 ' piF q, so i 1 " i.
Finally, to show that Ran F is faithful, consider G, G 1 : C Ñ E and two natural transformations i, j : G Ñ G 1 such that Ran F piq " Ran F pjq " k. Then, by construction of k, we have

i ' ε G " ε G 1 ' pkF q " j ' ε G .
But, ε G being an isomorphism, this implies i " j as desired. l Returning to views and plays, the embedding i X : V X ãÑ E X is full, so right Kan extension along i op X : V op X Ñ E op X induces a full essential embedding Ran i op X : y V X Ñ x E X . The (co)restriction of this essential embedding to its essential image thus yields an essentially surjective, fully faithful functor, i.e., an equivalence of categories:

Proposition 3 The category S X is equivalent to the essential image of Ran i op X .
The standard characterisation of right Kan extensions as ends [START_REF] Mac | Categories for the Working Mathematician[END_REF] yields, for any F P y V X and U P E X :

Ran i op X pF qpU q " ż V PV X F pV q E X pV,U q ,
i.e., giving an element of Ran i op X pF q on a play U amounts to giving, for each view V and morphism V Ñ U , an element of F pV q, satisfying some compatibility conditions. In Example 12 below, we compute an example right Kan extension.

The interpretation of strategies in terms of states extends: for any presheaf F P x E X and play U P E X , F pU q is the set of possible states of the strategy F after playing U . That F is in the image of Ran i op X amounts to F pU q being a compatible tuple of states of F after playing each view of U .

Example 12 Here is an example of a presheaf F P x E X which is not innocent, i.e., not in the image of Ran i op X . Consider the position X consisting of three players, say x, y, z, sharing a channel, say a. Let X x be the subposition with only x and a, and similarly for X y , X z , X x,y , and X x,z . Let I x " pι 1,1 Ðâ X x ãÑ Xq be the play where x inputs on a, and similarly let O y and O z be the plays where y and z output on a, respectively. Let now S x,y " pτ 1,1,1,1 Ðâ X x,y ãÑ Xq be the play where x and y synchronise on a (x inputs and y outputs), and similarly let S x,z be the play where x and z synchronise on a.

Finally, we define a presheaf F on E{X such that F pS x,y q " 2 is a two-element set, and F pS x,z q " H. To define F on other plays, the idea is to map any strict subplay of S x,y and S x,z to a one-element set 1, and other plays to H. The cleanest technical way to do this seems to be as follows. The poset Ex 11 defined by

O y I x O z S x,y S x,z
fully embeds into E{X, via, say i 11 . Let F 0 be the presheaf on Ex 11 defined by:

1 1 1 2 H.
We now let F " Ran i op 11 pF 0 q. Because i 11 is fully faithful, F coincides with F 0 on the plays of Ex 11 , as desired. Now, F fails to be innocent on two counts. First, since x and y accept to input and output in only one way, it is non-innocent to accept that they synchronise in more than one way. Formally, S x,y has two non-trivial views, I x and O y , so since F maps identity views to a singleton, F pS x,y q should be isomorphic to F pI x q ˆF pO y q " 1 ˆ1 " 1. The second reason why F is not innocent is that, since x and z accept to input and output, F should accept that they synchronise. Formally, F pS x,z q should also be a singleton. This altogether models the fact that in CCS, processes do not get to know with which other processes they synchronise.

The restriction of F to V X , i.e., F 1 " F ˝iop X , in turn has a right Kan extension F 2 , which is innocent. (In passing, the unit of the adjunction Catpi op X , Setq % Ran i op X is a natural transformation F Ñ F 2 .) To conclude this example, let us compute F 2 . First, F 1 only retains from F its values on views. So, if X x denotes the empty view on X x , F 1 pX x q " 1, and similarly F 1 pX y q " F 1 pX z q " 1. Furthermore, F 1 pI x q " F 1 pO y q " F 1 pO z q " 1. Finally, for any view V not isomorphic to any of the previous ones, F 1 pV q " H. So, recall that F 2 maps any play U Ðâ Y ãÑ X to ş V PV X F 1 pV q E X pV,U q . So, e.g., since the views of S x,y are subviews of I x and O y , we have F 2 pS x,y q " F 1 pI x q ˆF 1 pO y q " 1. Similarly, F 2 pS x,z q " 1. But also, for any play U such that all views V Ñ U are subviews of either of I x , O y , or O z , we have F 2 pU q " 1. Finally, for any play U such that there exists a view V Ñ U which is not a subview of any of I x , O y , or O z , we have F 2 pU q " H.

One way to understand Proposition 3 is to view y V X as the syntax for innocent strategies: presheaves on views are (almost) infinite terms in a cer-tain syntax (see Section 4.4 below). On the other hand, seeing them as presheaves on plays will allow us to consider their global behaviour: see Section 5 when we restrict to the closed-world game. Thus, right Kan extension followed by restriction to closed-world will associate a semantics to innocent strategies.

Remark 5

The relevant Grothendieck topology on E X says, roughly, that a play is covered by its views. Any sheaf for this topology is determined by its restriction to V X , for its elements on any non-view play U are precisely amalgamations of its elements on views of U . Right Kan extension just computes these amalgamations in the particular case of a topology derived from a full subcategory, here views. So, we have defined for each X the category S X of innocent strategies on X. This assignment is actually functorial B op Ñ CAT, as follows (where CAT is the large category of locally small categories). Any morphism

f : Y Ñ X induces a functor f ! : V Y Ñ V X mapping pV Ðâ Z Ñ Y q to pV Ðâ Z Ñ Y Ñ Xq. Precomposition with pf ! q op thus induces a functor S f : y V X Ñ x V Y .
Proposition 4 This defines a functor S : B op Ñ CAT.

Proof: A straightforward verification. l But there is more: for any position, giving a strategy for each player in it easily yields a strategy on the whole position. We call this amalgamation of innocent strategies (because the functor S is indeed a stack [START_REF] Vistoli | Notes on Grothendieck topologies, fibered categories and descent theory[END_REF], and this is a particular case of amalgamation in that stack). Formally, consider any subpositions X 1 and X 2 of a given position X, inducing a partition of the players of X, i.e., such that X 1 Y X 2 contains all players of X, and X 1 X X 2 contains none. Then V X is isomorphic to the coproduct V X 1 `VX 2 . (Indeed, a view contains in particular an initial player in X, which forces it to belong either in V X 1 or in V X 2 .) Definition 12 Given innocent strategies F 1 on X 1 and F 2 on X 2 , let their amalgamation be their copairing

rF 1 , F 2 s : V op X -pV X 1 `VX 2 q op -V op X 1 `Vop X 2 Ñ Set.
By universal property of coproduct:

Proposition 5 Amalgamation yields an isomorphism of categories

y V X -y V X 1 ˆy V X 2 .
Example 13 Consider again the position X from Example 12, and let X y,z be the subposition with only y and z. We have V X » pV Xx `VXy,z q, which we may explain by hand as follows. A view on X has a base player, x, y, or z, and so belongs either in V Xx or in V Xy,z . Furthermore, if V is a view on x and W is a view on y, then V X pV, W q " H (and similarly for any pair of distinct players in X). Now, recall F 1 , the restriction of F to V X . We may define F x : V op Xx Ñ Set to be the restriction of F 1 along the (opposite of the) embedding V Xx ãÑ V X , and similarly F y,z to be the restriction of F 1 along V Xy,z ãÑ V X . We have obviously F 1 " rF x , F y,z s.

Analogous reasoning leads to what we call spatial decomposition. For any X, let PlpXq " ř n Xprnsq, i.e., the set of pairs pn, xq, where x is a player in X, knowing n channels.

Theorem 1 We have y V X - ś pn,xqPPlpXq y V rns .
Again, this is a particular case of amalgamation in the stack S, but we do not need to spell out the definition here.

Temporal decomposition

Let us now describe temporal decomposition. Recall that basic moves are left and right half-forking (2), input, output, tick, and channel creation.

Definition 13 Let M be the graph with vertices all natural numbers n, and with edges n Ñ n 1 all (isomorphism classes of ) basic moves M : rns Ñ rn 1 s.

Recall from Remark 4 that the notion of isomorphism considered here is that of an isomorphism of cospans in p C.

Definition 14 Let M n be the set of edges from n in M.

For stating the temporal decomposition theorem, we need a standard [21] categorical construction, the category of families on a given category C. First, given a set X, consider the category FampXq with as objects Xindexed families of sets Y " pY x q xPX , and as morphisms Y Ñ Z families pf x : Y x Ñ Z x q xPX of maps. This category is equivalently described as the slice category Set{X. To see the correspondence, consider any family pY x q xPX , and map it to the projection function ř xPX Y x Ñ X sending px, yq to x. Conversely, given f : Y Ñ X, let, for any x P X, Y x be the fibre of f over x, i.e., f ´1pxq.

Generalising from sets X to small categories C, FampCq has as objects families p : Y Ñ obpCq indexed by the objects of C. Morphisms pY, pq Ñ pZ, qq are pairs of u : Y Ñ Z and v : Y Ñ morpCq, where morpCq is the set of morphisms of C, such that dom ˝v " p, and cod ˝v " q ˝u. Thus, any element y P Y over C P C is mapped to some upyq P Z over C 1 P C, and this mapping is labelled by a morphism vpyq : C Ñ C 1 in C. The obtained category is locally small. Further generalising, for C a locally small category, we may define FampCq in exactly the same way (with Y still a set), and the obtained category remains locally small.

The temporal decomposition theorem is:

Theorem 2 There is an equivalence of categories

S n » Fam ˜ź M PMn S codpM q ¸.
The main intuition is that an innocent strategy is determined up to isomorphism by (i) its initial states, and (ii) what remains of them after each possible basic move. The family construction is what permits innocent strategies with several possible states over the identity play.

Proof sketch: For general reasons, we have:

Fam `śMPMn S codpM q ˘" Fam ´śMPMn rV op codpM q , Sets -

Fam `"ř M PMn V codpM q op , Set ‰» " ř M PMn V op codpM q , Set ı Ó ∆,
where ∆ : Set Ñ r ř M PMn V op codpM q , Sets maps any set X to the constant presheaf mapping any object to X and any morphism to the identity.

By definition, the last category is a lax pullback " ř

M PMn V op codpM q , Set ı " ř M PMn V op codpM q , Set ı Set " ř M PMn V op codpM q , Set ı Ó ∆ ∆ in CAT.
Now, any basic move M : n Ñ n 1 induces a functor p´˝M q : V rn 1 s Ñ V rns , mapping any view V P V rn 1 s to V ˝M (with composition in Cospanp p Cq). We show that the square

ř M PMn V op codpM q ř M PMn V op codpM q 1 V op rns ! xid rns y r´˝M s M PMn λ (6)
is a lax pushout in Cat, where λ M,V : id rns Ñ M ˝V , seen in V rns , is the obvious inclusion, which for general reasons is mapped by the hom-2-functor CATp´, Setq to a lax pullback. But CATp!, Setq " ∆ and CATpid , Setq " id , so we obtain a canonical isomorphism of lax pullbacks S rns " rV op rns , Sets -

« ÿ M PMn V op codpM q , Set ff Ó ∆.
More detail is in Appendix A. l

Remark 6

The theorem almost makes innocent strategies into a sketch (on the category with positions as objects, finite compositions of extended moves as morphisms, and the M X 's as distinguished cones). Briefly, being a sketch would require a bijection of sets S n -ś M PMn S codpM q . Here, the bijection becomes an equivalence of categories, and the family construction sneaks in.

Innocent strategies as a terminal coalgebra

Temporal decomposition gives

S n » Fam ˜ź M PMn S codpM q ¸,
for all n. Considering a variant of this formula as a system of equations will lead to our interpretation of CCS. The first step is to replace Set with FinOrd, the category of finite ordinals and monotone functions. The proof applies mutatis mutandis and we obtain an equivalence, which, because both categories are skeletal, is an isomorphism:

Ŋ V rns -Fam f ˜ź M PMn Ŕ V codpM q ¸, (7)
where

• Fam f is the same as Fam but with finite families, i.e., for any category C, obpFam f pCqq " ř IPFinOrd pobpCqq I " pobpCqq ˚is the set of finite words over objects of C, also known as the free monoid on obpCq;

• and for any category C, u C denotes the functor category rC op , FinOrds.

Remark 7 Recall that in the proof of Theorem 2, Fam arises from the 'constant presheaf ' functor ∆ : Set Ñ p

´, with ´a complicated category. This functor itself is equal to restriction along ´Ñ 1, via p 1 -Replacing Set with FinOrd thus replaces ∆ with the analogous functor FinOrd Ñ u

´, via u 1 -FinOrd, and thus Fam with Fam f . Furthermore, because FinOrd embeds into Set, the special strategies of Ŋ V rns embed into S rns .

Then, taking advantage of the fact that FinOrd is a small category, we consider its set FinOrd 0 of objects, i.e., finite ordinals, and the endofunctor F on Set{FinOrd 0 defined on any family of sets X " pX i q iPFinOrd 0 by:

pFpXqq n " ÿ IPFinOrd 0 ˜ź M PMn X codpM q ¸I ,
where we abusively confuse rn 1 s " codpM q and the natural number n 1 itself. The isomorphism [START_REF] De | Testing equivalences for processes[END_REF] becomes obp Ŋ V rns q -pFpobp Ň V ´qqq n .

We may decompose F as follows. Consider the endofunctor on Set{ FinOrd 0 defined by pBXq n " ś M PMn X codpM q , for any family X. We obviously have:

Lemma 1 F is equal to the composite pB´q ˚.
This endofunctor is polynomial [START_REF] Kock | Polynomial functors and trees[END_REF] and we now give a characterisation of its final coalgebra. The rest of this subsection is devoted to proving: Theorem 3 The family obp Ň

V n q formed for each n by (the objects of ) Ň V n is a terminal coalgebra for F. Ξ; Γ $ P Γ $ rec x 1 p∆ 1 q := P 1 , . . . , x n p∆ n q := P n in P

Translating CCS

It is rather easy to translate CCS into this language. First, define CCS syntax by the natural deduction rules in Figure 3, where Names and Vars are two fixed, disjoint, and infinite sets of names and variables; Ξ ranges over finite sequences of pairs px : nq of a variable x and its arity n P FinOrd 0 , such that the variables are pairwise distinct; Γ ranges over finite sequences of pairwise distinct names; there are two judgements: Γ $ P for global processes, Ξ; Γ $ P for open processes. Rule Global is the only rule for forming global processes, and there Ξ " px 1 : |∆ 1 |, . . . , x n : |∆ n |q. Finally, α denotes a or a, for a P Names, and tau " tau " a.

First, we define the following (approximation of a) translation on open processes, mapping each open process Ξ; Γ $ P to P P Ň V n , for n " |Γ|. This translation ignores the recursive definitions, and we will refine it below to take them into account. We proceed by induction on P , leaving contexts Ξ; Γ implicit:

xpa 1 , . . . , a k q Þ Ñ H P |Q Þ Ñ x π l n Þ Ñ P , π r n Þ Ñ Q , Þ Ñ H y νa.P Þ Ñ xν n Þ Ñ P , Þ Ñ Hy ř iPI α i .P i Þ Ñ x po n,j Þ Ñ ř kPI j P k , ι n,j Þ Ñ ř kPI j P k q jPn , Þ Ñ H y.
Let us explain intuitions and notation. In the first case, we assume implicitly that px : kq P Ξ; the intuition is just that we approximate variables with empty strategies. Next, P |Q is translated to the strategy with one initial state, which only accepts left and right half-forking first, and then lets its avatars play P and Q , respectively. Similarly, νa.P is translated to the strategy with one initial state, accepting only the channel creation move, and then playing P . In the last case, the guarded sum ř iPI α i .P i is translated to the strategy with one initial state, which

• accepts input on any channel a when α i " a for some i P I, and output on any channel a when α i " a for some i P I;

• after an input on a, plays the sum of all P i 's such that α i " a; and after an output on a, plays the sum of all P i 's such that α i " a.

Formally, in the definition, we let, for all j P n, I j " ti P I | α i " a j u and I j " ti P I | α i " a j u. In particular, if I " H, we obtain 0. Thus, almost all translations of open processes have exactly one initial state, i.e., map the identity view on rns to the singleton 1. The only exceptions are variable applications, which are mapped to the empty presheaf.

The translation extends to global processes as follows. Fixing a global process Q " prec x 1 p∆ 1 q := P 1 , . . . , x k p∆ k q := P k in P q typed in Γ with n names, define the sequence pP i q iPFinOrd 0 of open processes (all typed in Ξ; Γ) as follows. First, P 0 " P . Then, let P i`1 " dP i , where d is the derivation endomap on open processes typed in any extension Ξ; pΓ, ∆q of Ξ; Γ, which unfolds one layer of recursive definitions. This map is defined by induction on its argument as follows: dpx l pa 1 , . . . , a k l qq " P l rb j Þ Ñ a j s 1ďjďk l dpP |Qq " dP |dQ dpνa.P q " νa.dP dp ř iPI α i .P i q " ř iPI α i .pdP i q,

where for all l P t1, . . . , ku, ∆ l " pb 1 , . . . , b k l q, and P rσs denotes simultaneous, capture-avoiding substitution of names in P by σ. By construction, the translations of these open processes form a sequence P 0 ãÑ P 1 . . . of inclusions in Ň

V n , such that for any natural number i and view V P V n of length i, P j pV q is fixed after j " pk `1qi, at worst, i.e., for all j ě pk `1qi, P j pV q " P pk`1qi pV q. Thus, this sequence has a colimit in Ň

V n , the presheaf sending any view V of length i to P pk`1qi pV q. We put:

Definition 16 Let the translation of Q be Q " colim iPFinOrd P i .
Which equivalence is induced by this mapping on CCS, especially when taking into account the interactive equivalences developed in the next section? This is the main question we will try to address in future work.

5 Interactive equivalences 5.1 Fair testing vs. must testing: the standard case An important part of concurrency theory consists in studying behavioural equivalences. Since each such equivalence is supposed to define when two processes behave the same, it might seem paradoxical to consider several of them. Van Glabbeek [START_REF] Van Glabbeek | The linear time-branching time spectrum (extended abstract)[END_REF] argues that each behavioural equivalence corresponds to a physical scenario for observing processes.

A distinction we wish to make here is between fair scenarios, and potentially unfair ones. An example of a fair scenario is when parallel composition of processes is thought of as modelling different physical agents, e.g., in a game with several players. Otherwise said, players are really independent. On the other hand, an example of a potentially unfair scenario is when parallelism is implemented via a scheduler.

This has consequences on so-called testing equivalences [START_REF] De | Testing equivalences for processes[END_REF]. Let ♥ be a fixed action.

Definition 17 A process P is must orthogonal to a context C, notation P K m C, when all maximal traces of CrP s play ♥ at some point.

Here, maximal means either infinite or finite without extensions. Let P K m be the set of all contexts must orthogonal to P . Definition 18 P and Q are must equivalent, notation P " m Q, when

P K m " Q K m .
In transition systems, or automata, we have Ω " m Ω|a (where Ω is the looping process, producing infinitely many silent transitions). This might be surprising, because the context C " a.♥ | intuitively should distinguish these processes, by being orthogonal to Ω|a but not to Ω alone. However, it is not orthogonal to Ω|a, because CrΩ|as has an infinite looping trace giving priority to Ω. This looping trace is unfair, because the synchronisation on a is never performed. Thus, one may view the equivalence Ω " m Ω|a as exploiting potential unfairness of a hypothetical scheduler.

Usually, concurrency theorists consider this too coarse, and resort to fair testing equivalence.

Definition 19 A process P is fair orthogonal to a context C, notation P K f C, when all finite traces of CrP s extend to traces that play ♥ at some point.

Again, P K f denotes the set of all contexts fair orthogonal to P . Definition 20 P and Q are fair equivalent, notation P " f Q, when P K f " Q K f . This solves the issue, i.e., Ω  f Ω|a.

In summary, the mainstream setting for testing equivalences relies on traces; and the notion of maximality for traces is intrinsically unfair. This is usually rectified by resorting to fair testing equivalence over must testing equivalence. Our setting is more flexible, in the sense that maximal plays are better behaved than maximal traces. In terms of the previous section, this allows viewing the looping trace Ω|a|a.♥ τ Ý Ñ Ω|a|a.♥ τ Ý Ñ . . . as non-maximal. In the next sections, we define an abstract notion of interactive equivalence (still in the particular case of CCS but in our setting) and we instantiate it to define and study the counterparts of must and fair testing equivalences.

Interactive equivalences

Definition 21 A play is closed-world when it is a composite of closed-world extended moves.

Equivalently, a play is closed-world when all of its basic moves are part of a closed-world move.

Let W ãÑ E be the full subcategory of closed-world plays, WpXq being the fibre over X for the projection functor W Ñ B, i.e., the subcategory of W consisting of closed-world plays with base X, and morphisms pid X , kq between them 5 .

Let the category of closed-world behaviours on X be the category G X " { WpXq of presheaves on WpXq. We may now put:

Definition 22 An observable criterion consists for all positions X, of a replete subcategory K K X ãÑ G X .

Recall that K K X being replete means that for all F P K K X and isomorphism f : F Ñ F 1 in G X , F 1 and f are in K K X . An observable criterion specifies the class of 'successful', closed-world behaviours. The two criteria considered below are two ways of formalising the idea that a successful behaviour is one in which all accepted closed-world plays are 'successful', in the sense that some player plays the tick move at some point.

We now define interactive equivalences. Recall that rF, Gs denotes the amalgamation of F and G, and that right Kan extension along i op Z induces a functor Ran i op Z : x V Z Ñ x E Z . Furthermore, precomposition with the canonical inclusion j Z : WpZq ãÑ E Z induces a functor j Z : x E Z Ñ { WpZq. Composing the two, we obtain a functor Gl : S Z Ñ G Z :

S Z " x V Z Ran i op Z Ý ÝÝÝ Ñ x E Z j Z Ý Ñ { WpZq " G Z .
Definition 23 For any innocent strategy F on X and any pushout square P of positions as on the right, with I consisting only of channels, let F K K P be the class of all innocent strategies G on Y such that GlprF, Gsq P K K Z .

I Y X Z (8)
Here, G is thought of as a test for F . Also, P denotes the whole pushout square and F K K P denotes all the valid tests for the considered pushout square P . From the CCS point of view, I corresponds to the set of names shared by the process under observation pF q and the test pGq.

Definition 24 Any two innocent strategies F, F 1 P S X are K K-equivalent, notation F " K K F 1 , iff for all pushouts P as in 8, F K K P " F 1 K K P .

Fair vs. must

Let us now define fair and must testing equivalences. Let a closed-world play be successful when it contains a ♥ n . Furthermore, for any closed-world behaviour G P G X and closed-world play U P WpXq, an extension of a state σ P GpU q to U 1 is a σ 1 P GpU 1 q with i : U Ñ U 1 and Gpiqpσ 1 q " σ. The extension σ 1 is successful when U 1 is. The intuition is that the behaviour G, before reaching U 1 with state σ 1 , passed through U with state σ.

Definition 25

The fair criterion K K f contains all closed-world behaviours G such that any state σ P GpU q for finite U admits a successful extension. Now call an extension of σ P GpU q strict when U Ñ U 1 is not surjective, or, equivalently, when U 1 contains more moves than U . For any closed-world behaviour G P G X , a state σ P GpU q is G-maximal when it has no strict extension.

Definition 26 Let the must criterion K K m consist of all closed-world behaviours G such that for all closed-world U and G-maximal σ P GpU q, U is successful.

As explained in the introduction and Section 5.1, unlike in the standard setting, this definition of must testing equivalence distinguishes between the processes Ω and Ω|a. Indeed, take the CCS context C " a.♥ | , which we can implement by choosing as a test the strategy T " a.♥ on a single player knowing one channel a. Taking I to consist of the sole channel a, the pushout Z as in Definition 23 consists of two players, say x for the observed strategy and y for the test strategy, sharing the channel a. Now, assuming that Ω loops deterministically, the global behaviour G " Glpr P , T sq has exactly one state on the identity play, and again exactly one state on the play π 1 consisting of only one fork move by x. Thus, G reaches a position with three players, say x 1 playing Ω, x 2 playing a, and y playing a.♥. The play with infinitely many silent moves by x 1 is not maximal: we could insert (anywhere in the sequence of moves by x 1 ) a synchronisation move by x 2 and y, and then a tick move by the avatar of y. Essentially: our notion of play is more fair than just traces.

To get more intuition about must testing equivalence in our setting, we prove that it actually coincides with the testing equivalence generated by the following criterion: Definition 27 The spatially fair criterion K K sf contains all closed-world behaviours G such that any state σ P GpU q admits a successful extension.

This criterion is almost like the fair criterion, except that we do not restrict to finite plays. The key result to show the equivalence is: Theorem 4 For any innocent strategy F on X, any state σ P GlpF qpU q admits a GlpF q-maximal extension.

The proof is in Appendix B. Thanks to the theorem, we have: Lemma 6 For all F P S X , GlpF q P K K m X iff GlpF q P K K sf X .

Proof: Let G " GlpF q.

(ñ) By Theorem 4, any state σ P GpU q has a G-maximal extension σ 1 P GpU 1 q, which is successful by hypothesis, hence σ has a successful extension.

(ð) Any G-maximal σ P GpU q admits by hypothesis a successful extension which may only be on U by G-maximality, and hence U is successful. l (Note that U is not necessarily finite in the proof of the right-to-left implication, so that the argument does not apply to the fair criterion.)

Now comes the expected result:

Theorem 5 For all F, F 1 P S X , F " K K m F 1 iff F " K K sf F 1 .

Proof: (ñ) Consider two innocent strategies F and F 1 on X, and an innocent strategy G on Y (as in the pushout ( 8)). As in spatial decomposition (Proposition 5), copairing induces an isomorphism S X ˆSY Ñ S Z , and we have, using Lemma 6:

GlrF, Gs P K K sf iff GlrF, Gs P K K m iff GlrF 1 , Gs P K K m iff GlrF 1 , Gs P K K sf (ð) Symmetric. l Intuitively, must testing only considers spatially fair schedulings, in the sense that all players appearing in a play should be given the opportunity to play: no one should starve.

However, this is not the only source of unfairness, so that must testing and fair testing differ. To see this, consider the CCS process P " νb.rec xpa, bq := b|pb.pxpa, bqq `aq in xpa, bq, that can repeatedly perform synchronisations on the private channel b, until it chooses to perform an output on a. We have Ω " sf P while Ω  f P . Indeed, since the choice between doing a synchronisation on b or an output on a is done by a single player, the infinite play where the output on a is never performed is maximal: no player starve, we just have a player that repeatedly chooses the same branch, in an unfair way.

We leave for future work the investigation of such unfair scenarios and their correlation to the corresponding behaviours in classical presentations of CCS.

Definition 4

 4 ,m,j and ρ : ι m,j Ñ τ n,i,m,j (ǫ and ρ respectively stand for 'emission' and 'reception'). Let C 4 be the category generated by G 4 , the previous relations, plus, for each o n,i ǫ Ý Ñ τ n,i,m,j ρ Ð Ý ι m,j , the relation ǫ ˝s ˝di " ρ ˝s ˝dj .

Figure 2 :

 2 Figure 2: Construction of the synchronisation move

Figure 3 :

 3 Figure 3: CCS syntax

Table 1 :

 1 Summary of categories and functors

		world plays
	WpXq	closed-world plays on X

Table 2 :

 2 Summary of classes of moves

	Basic	Full	Closed-world
	Left half-forking Right half-forking	Forking	Forking
	Input Output	Input Output	Synchronisation
	Channel creation	Channel creation Channel creation
	Tick	Tick	Tick

  FinOrd 0 and @i P I, tα i u P Γq

		CCSApp
		Ξ; Γ $ xpa 1 , . . . , a n q	ppx : nq P Ξ and a 1 , . . . , a n P Γq
		Ξ; Γ, a $ P Ξ; Γ $ νa.P	(a R Γ)	Ξ; Γ $ P Ξ; Γ $ P |Q Ξ; Γ $ Q
	. . .	Ξ; Γ $ P i Ξ; Γ $ pI P Global . . . p@i P Iq ÿ iPI α i .P i
		Ξ; ∆ 1 $ P 1	. . .	Ξ; ∆ n $ P n

Only 'a kind of', because, as mentioned above, the channels known to a player are linearly ordered.

This is not exactly equivalent to what could be noted WX , since in the latter there are objects U Ðâ Y ãÑ X with a strict inclusion Y ãÑ X. However, both should be equivalent for what we do in this paper, i.e., fair and must equivalences.

 [START_REF] Beffara | réalisabilité et concurrence[END_REF]Both authors have been partially funded by the French projects CHoCo (ANR-07-BLAN-0324), PiCoq (ANR-10-BLAN-0305-01), and CNRS PEPS CoGIP.

Consider any F-coalgebra a : X Ñ FX. We define by induction on N a sequence of maps f N : X Ñ Ő V r´s , such that for any view V of length less than N (i.e., with less than N basic moves), and any N 1 ą N , f N 1 pxqpV q " f N pxqpV q, and similarly the action of f N pxq on morphisms is the same as that of f N 1 pxq.

To start the induction, take f 0 pxq to be the strategy mapping id rns to πpapxqq, i.e., the length of apxq P ř IPFinOrd 0 ppBXq n q I , and all other views to 0.

Furthermore, given f N , define f N `1 to be

where the equivalence is by temporal decomposition.

Unfolding the definitions yields:

Lemma 2 Consider any x P X n , and apxq " pz 1 , . . . , z k q. For any move M : n Ñ n 1 and view V : n 1 Ñ n 2 of length at most N , and for any i P k, f N `1pxqpV ˝M q " ř iPk f N pz i pM qqpV q. For any x P X n , we have a sequence f 0 pxq ãÑ f 1 pxq ãÑ . . . f N pxq ãÑ f N `1pxq ãÑ . . . which is pointwise stationary. This sequence thus has a colimit in Ŋ V rns , the presheaf mapping any view V of length N to f N pV q (or equivalently f N 1 pV q for any N 1 ě N ), which allows us to define:

By construction, we have

Lemma 3

The following diagram commutes:

The map f is a morphism of F-coalgebras.

Proof: Let, for any innocent strategy S P Ŋ V rns and i P Spid rns q, S |i be the strategy mapping any view V to the fibre over i of SpV q Ñ Spid rns q. Using the notations of Lemma 2, we must show that for any i P k, we have pf pxqq |i pV ˝M q " f pz i pM qqpV q. But Lemma 2 entails that f pxqpV ˝M q Ñ f pxqpid rns q is actually the coproduct over i 1 P k of all f pz i 1 pM qqpV q

The map f is the unique map X Ñ Ő V r´s of F-coalgebras.

Proof: Consider any such map g of coalgebras. It must be such that gpxqpid rns q " πpapxqq, and furthermore, using the same notation as before, for any i P k pgpxqq |i pV ˝M q " gpz i pM qqpV q, which imposes by induction that f " g. l The last two lemmas directly entail Theorem 3.

Languages

A consequence of Theorem 3 is that the family Ň

V n supports the operations of the grammar

n $ F denotes a presheaf of finite ordinals on V n . The interpretation is as follows: given presheaves F 1 , . . . , F I , for I P FinOrd 0 , the first rule constructs the finite coproduct ř iPI F i of presheaves (finite coproducts exist in Ň

V n because they do in FinOrd). In particular, when I is the empty ordinal, we sum over an empty set, so the rule degenerates to n $ H Ïn terms of presheaves, this is just the constantly empty presheaf.

For the second rule, if for all basic M : rns Ñ rn 1 s, we are given

Here, we provide an element of the right-hand side of [START_REF] De | Testing equivalences for processes[END_REF], consisting of the finite ordinal I " 1 " t1u, and the function mapping M to F M P Ő V rn 1 s (up to currying). That was for parsing; the intuition is that we construct a presheaf with one initial state, 1, which maps any view starting with M , say V ˝M , to F M pV q. Thus the F M 's specify what remains of our presheaf after each possible basic move. In particular, when all the F M 's are empty, we obtain a presheaf which has an initial state, but which does nothing beyond it. We abbreviate it as 0 " x Þ Ñ Hy.

A Temporal decomposition

This section is a proof of Theorem 2. Let us first review the general equivalences mentioned in the proof sketch. The product of a family of presheaf categories is isomorphic to the category of presheaves over the corresponding coproduct of categories:

Furthermore, let the functor ∆ : Set Ñ p C map any set X to the constant presheaf mapping any C P C to X. We have: Lemma 8 For any small category C, Famp p Cq » p p C Ó ∆q.

Proof: A generalisation of the more well-known Set X » Set{X. l

Corollary 1 We have:

V op codpM q , Sets Ó ∆q.

We now construct the lax pushout [START_REF] Carboni | Corrigenda for 'connected limits, familial representability and artin glueing[END_REF]. A first step is the construction, for each move rns ãÑ M Ðâ rn 1 s, of a functor p´˝M q : V rn 1 s Ñ V rns given by precomposition with M in Cospanp p Cq. This functor maps any V 1 :

This of course relies on the choice of such a colimit for every V and

, is mapped to the dashed morphism induced by universal property of pushout in

Once the choice has been made on objects, the map for morphisms is determined uniquely. This family of functors allows us to decompose V rns as follows:

is a lax pushout, where λ M,V : id rns Ñ M ˝V , seen in V rns , is the obvious inclusion.

Proof: For any category C, taking such a lax pushout of id C with 1 just adds a terminal object to C. The rest is an easy verification. A dual result of course holds with V rns , reversing the direction of λ. l Now, it is well-known that, in any small 2-category K, any contravariant hom-2-functor, i.e., 2-functor of the shape Kp´, Xq for X P K, maps weighted colimits in K to weighted limits in Cat. For an introduction to weighted limits and colimits in the case of enrichment over Cat, see Kelly [START_REF] Kelly | Elementary observations on 2-categorical limits[END_REF]. Here, for any 2-category P , and 2-functors G : P Ñ K and J : P op Ñ Cat, any colimit L " J ‹ G of G weighted by J with unit ξ : J Ñ KpGp´q, Lq in rP op , Cats is mapped, for any object X P K, by the hom-2-functor Kp´, Xq to a limit of KpGp´q, Xq : P op Ñ Cat weighted by J in Cat, with unit Kpξ, Xq : J Ñ CatpKpL, Xq, KpGp´q, Xqq, in Cat. In particular, lax pushouts are mapped to lax pullbacks. As usual, considering a larger universe, we may replace Cat with CAT and obtain the same results with K " Cat.

Recalling our lax pushout [START_REF] Ehrig | editors[END_REF] and taking the hom-categories to Set, we obtain a lax pullback

n CAT, i.e., a comma category. But observe that restriction along ! is precisely ∆ : Set Ñ r ř M PMn V op codpM q , Sets, so we have indeed shown that S rns is a comma category r ř M PMn V op codpM q , Sets Ó ∆.

B Maximal extensions

This section is a proof of Theorem 4.

Lemma 10 For any position X, the category WpXq of closed-world plays is a preorder.

Proof: Easy. l In the following, we consider the quotient poset.

Lemma 11

In WpXq, any non-decreasing chain admits an upper bound.

Recall M, the graph of all basic moves, and the set M n of edges from n, for each n. Let now, for each n, M f n be the analogous set with full moves, i.e., the set of isomorphism classes of full moves from rns.

Lemma 12

For each play U P E X , the coproduct of all s maps from full moves ¨ÿ nPFinOrd ÿ

is injective.

Recall here that for forking, we have also called s the common composite l ˝s " r ˝s (see the discussion following Definition 3). Proof: By induction on U . l Lemma 13 Any non-decreasing sequence in the poset WpXq admits its colimit in p C as an upper bound.

Proof: Consider any increasing sequence U 1 ãÑ U 2 ãÑ . . . of plays in WpXq. Let U be its colimit in p C. We want to prove that U is a play. First, observe that U satisfies joint injectivity of s-maps as in Lemma 12: indeed, if we had a player p and two full moves M and M 1 such that spM q " spM 1 q " p, then all of M , M 1 , and p would appear in some U i , which, being a play, has to satisfy joint injectivity.

For each n, U n comes with a sequence of compatible (closed-world) extended moves

which are also (by the colimit cocone) morphisms over U in p C. For each i ě 1, taking the colimit of the i first moves yields a finite play X ãÑ U n i Ðâ X n i . By convention, letting U n 0 " X extends this to i ě 0. Similarly, we may consider all the given plays infinite, by accepting not only extended moves, but also identity cospans.

We consider the poset of pairs pN, nq P tp0, 0qu Z ř N PFinOrd ˚N , with lexicographic order, i.e., pN, nq ď pN 1 , n 1 q when N ă N 1 or when N " N 1 and n ď n 1 .

We will construct by induction on pN, nq a sequence of composable closed-world moves, with colimit U 1 , such that for all pN, nq, U n N ´n`1 Ď U 1 in WpXq{U . More precisely, we construct for each pN, nq an integer K N,n and a sequence

(again, if K N,n " 0, we mean the empty sequence) such that

• for all pN 1 , n 1 q ă pN, nq, we have

• and the colimit, say U N,n , of pM N,n i q iPK N,n is such that for all pN 1 , n 1 q ď pN, nq, U n 1 N ´n1 `1 Ď U N,n in WpXq{U . For the base case, we let K 0,0 " 0, which forces M 0,0 to be the empty sequence on X.

For the induction step, consider any pN, nq ‰ p0, 0q, and let pN 0 , n 0 q be the predecessor of pN, nq. The induction hypothesis gives a K N 0 ,n 0 and a sequence pM N 0 ,n 0 i q iPK N 0 ,n 0 satisfying some hypotheses, among which the existence of a diagram

,n 0 , then we put K N,n " K N 0 ,n 0 and pM N,n i q iPK N,n " pM N 0 ,n 0 i q iPK N 0 ,n 0 , and all induction hypotheses go through.

Otherwise, M n N ´n`1 is played by players in X n N ´n which are not in the joint image of all s maps [START_REF] Fiore | Second-order and dependently-sorted abstract syntax[END_REF] in U N 0 ,n 0 , otherwise s maps in U could not be jointly injective, contradicting Lemma 12. Technically, the diagram

is obtained by pushing some (non-extended) closed-world move Y Ñ M Ð Y 1 along some morphism I Ñ Z from an interface I, and the induced morphism

a pushout; Z 1 consists of the players in X N 0 ,n 0 K N 0 ,n 0 that are not in the image of Y , plus their names, plus possibly missing names from I.

Then, pushing Y Ñ M Ð Y 1 along I Ñ Z 1 , we obtain an extended move X N 0 ,n 0 K N 0 ,n 0 ãÑ M 1 Ðâ X 1 . We let K N,n " K N 0 ,n 0 `1 and define pM N,n i q iPK N,n to be the extension of pM N 0 ,n 0 i q iPK N 0 ,n 0 by M 1 . This induces a unique map U N,n Ñ U by universal property of U N,n as a colimit. All induction hypotheses go through; in particular, U n N ´n`1 is a union U n N ´n Y M n N ´n`1 in WpXq{U , and actually a union U n N ´n Y M ; similarly, U N,n " U N 0 ,n 0 Y M ; so, since we have U n N ´n Ď U N 0 ,n 0 by induction hypothesis, we obtain U n N ´n`1 Ď U N,n . The sequences M N,n induce by union a possibly infinite sequence of closed-world extended moves, i.e., a closed-world play U 1 , such that for all pN, nq, U n N ´n`1 Ď U 1 , hence, for all n, U n Ď U 1 Ď U , i.e., U 1 -U . Thus, U is indeed a play. l

We are almost ready for proving Theorem 4. We just need one more lemma. Consider any innocent strategy F on X, play U P WpXq, and any state σ P GlpF qpU q. Consider now the poset F σ of GlpF q-extensions of σ (made into a poset by choosing a skeleton of WpXq), where σ 1 P F pU 1 q ď σ 2 P F pU 2 q iff U 1 ď U 2 . This poset is not empty, since it contains σ. Furthermore, we have: Lemma 14 Any non-decreasing sequence in F σ admits an upper bound.

Proof: Any such sequence, say pσ i q iPFinOrd , induces a non-decreasing sequence of plays in WpXq, say pU i q i , which by Lemma 13 admits its colimit, say U 1 , as an upper bound. Now, any view inclusion j : V ãÑ U 1 , factors through some U i , and we let σ j " pσ i q |V (this does not depend on the choice of i). This assignment determines (by innocence of F and by construction of the right Kan extension as an end) an element σ 1 P F pU 1 q, which is an upper bound for pσ i q iPFinOrd . l Proof of Theorem 4:

Consider any innocent strategy F on X, play U P WpXq, and any state σ P GlpF qpU q. Consider as above the poset F σ of GlpF q-extensions of σ. By the last lemma, we may apply Zorn's lemma to choose a maximal element of F σ , which is a GlpF q-maximal extension of σ. l