Pierre-Louis Curien

Claudia Faggian

An approach to innocent strategies as graphs

This paper proposes an approach for extending to graphs the close relation between proofs and innocent strategies. We work in the setting of L-nets, introduced by Faggian and Maurel as a game model of concurrent interaction. We show how L-nets satisfying an additional condition, which we call LS-nets, can be sequentialized into traditional tree-like strategies. Conversely, sequential strategies can be relaxed into more asynchronous ones.

We develop an algebra of constructors and destructors that serve to build and decompose graph strategies, and to describe a class of minimally sequential graph strategies, which can be seen as an abstract kind of multiplicative-additive proofnets.

Introduction

In the context of game semantics several proposals have emerged -with different motivations -towards strategies where sequentiality is relaxed to capture a more asynchronous form of interaction [AM99, Hyl01, Mel04, HS02, MW05, SPP05]. Such strategies often appear as graphs, contrarily to more traditional (sequential) strategies, as in particular Hyland-Ong innocent strategies [START_REF] Hyland | On full abstraction for PCF[END_REF], which appear as trees. Here we will consider the setting of L-nets, recently introduced by Faggian and Maurel [START_REF] Faggian | Ludics nets, a game model of concurrent interaction[END_REF] as a game model of concurrent interaction, based on Girard's ludics.

A strategy describes in an abstract way the operational behaviour of a proof (or program). An interaction between tree strategies produces a sequence of actions, which describes the trace of the computation. The idea underlying L-nets (as well as other closely related approaches) is to not completely specify the order in which the actions should be performed, while still being able to express constraints. Certain tasks may have to be performed before other tasks; other actions can be performed in parallel, or scheduled in any order. A strategy is now a directed acyclic graph. The interaction results into a partial order, allowing for parallelism.

In this paper we are interested in relating parallel strategies and sequential strategies. Working in the setting of L-nets, we show how strategies represented by graphs, with partial ordering information, can be sequentialized into tree-like strategies; conversely, sequential strategies can be relaxed into more asynchronous ones.

The tree strategies and the graph strategies that we will consider are Girard's designs [START_REF] Girard | Locus solum[END_REF] and (a subset of) Faggian and Maurel's L-nets, respectively. Syntactically, designs are particular sorts of Curien's abstract Böhm trees [START_REF] Curien | Abstract Böhm trees[END_REF][START_REF] Curien | Introduction to linear logic and ludics, part II[END_REF]).

As a computational object, a design is a Hyland-Ong innocent strategy on a universal arena, as discussed in [START_REF] Faggian | Designs, disputes and strategies[END_REF]. L-nets are (potentially infinite) graph strategies on this arena. They subsume sequential strategies as a special case: a tree is, in particular, a graph. On the other hand, it is possible to define a class of L-nets of minimal sequentiality, which we call parallel L-nets.

Hence we have a homogeneous space inside which we can move, adding or relaxing sequentiality (i.e., dependency between the actions). Between completely sequential and completely parallel strategies, we get a full range of intermediate strategies with decreasing sequentiality level.

The present paper builds on a preliminary extended abstract [START_REF] Curien | L-nets, strategies and proof-nets[END_REF], and on a subsequent analysis of the basic constructors and destructors on (graph or tree) strategies that are at work in our sequentialization an desequentialization procedures [Fag].

Two flavours of views. It is known that (innocent) tree strategies can be presented as sets of views with certain properties. A view is a totally ordered sequence of moves (again with certain properties), and the set of views forms a tree. Any interaction results into a totally ordered set of moves.

An L-net is a set of partially ordered views, each of which is a partially ordered set of moves, where the partial order expresses an enabling relation, or a scheduling among moves. The set of such partially ordered views forms a directed acyclic graph. Any interaction results into a partially ordered set of moves.

The proof-net experience. Tree strategies can be seen as abstract sequent calculus derivations. Specifically, designs arise as abstract (untyped) versions of (focalized) sequent calculus proofs of multiplicative-additive linear logic. By contrast, the class of graph strategies of minimal sequentiality (the parallel L-nets) can be seen as abstract multiplicative-additive proof-nets. Indeed, there are two standard ways to handle proofs in linear logic: either as sequent calculus derivations, or as proof-nets, which are graph-like structures satisfying a so-called correctness criterion. Sequent calculus derivations can be mapped onto proof-nets, by forgetting some of the order between the rules, and conversely proof-nets can be sequentialized into proofs.

While the origins of game semantics are closely connected to the analysis of correct proof structures [START_REF] Abramsky | Games and full completeness for multiplicative linear logic[END_REF], this paper is, to the best of our knowledge, the first attempt to transfer -so to say in the other direction -the use of proof-net techniques to the semantic setting of (innocent) games. In this respect, our contribution fits into a general research direction aiming at bringing closer together syntax and semantics.

Relating sequential and parallel strategies. As we have anticipated, L-nets are a conservative extension of innocent strategies (in the form used by ludics). This makes it possible to relate the two approaches. We are able to associate a set of tree-strategies to a parallel L-net (in fact, any "correct" L-net, see below) D, by saturating the order, i.e., we add sequentiality to the point that all choices on scheduling of the moves during an execution are determined. Conversely, given a tree strategy Π, we have a desequen-tialization procedure, which returns a parallel strategy, forgetting some "inessential" information on the scheduling.

Sequentialization is not possible for an arbitrary L-net, as L-nets can be intrinsically parallel, in the sense that actions depend on each other in an essential way. It is easy to build a counter-example to sequentialization by taking inspiration from Gustave function (a well-known example of a non-sequential function, see e.g. [START_REF] Amadio | Domains and Lambda-calculi[END_REF]). For this reason, we introduce L S -nets, which are L-nets satisfying a condition called Cycles. This condition upgrades the Acyclicity condition of [START_REF] Faggian | Ludics nets, a game model of concurrent interaction[END_REF], which is sufficient for computation purposes (i.e., to guarantee that strategies compose), but not for our goals here. Condition Cycles can be considered as an abstract correctness criterion, and as a matter of fact, it is the adaptation to our setting of Hughes and Van Glabbeek's toggling condition [START_REF] Hughes | Proof nets for unit-free multiplicativeadditive linear logic[END_REF].

A correctness criterion for proof-nets has two roles: it guarantees that (i) normalization is possible (we are not stuck with cycles during normalization), and (ii) it is possible to associate a sequent calculus derivation to the graph. The Acyclicity condition is a minimal criterion which takes care of (i); the new Cycles conditions guarantees also (ii).

We present an algebra of constructors and destructors allowing us to build and decompose graph strategies. This in particular allows us to (co)inductively define the classes of strategies of maximal and minimal sequentiality (i.e. of sequential and parallel strategies, respectively).

The destructors and constructors are also used to define the sequentialization procedure. This procedure works as a stream-like, bottom-up process (coinductively) acting on potentially infinite L S -nets. Dually, the same operations serve us to define a desequentialization procedure that transforms L-forests into parallel L-nets. We shall show that sequentialization and desequentialization can be performed so as to be inverse to each other.

Plan of the paper. Section 2 and Appendix B provide some background on (focalized) linear logic and designs, i.e., we introduce the ingredients of our universal arena and the tree strategies on which we work. Section 3 introduces our graph strategies. We recall the definition of L-net [START_REF] Faggian | Ludics nets, a game model of concurrent interaction[END_REF], and we define our subclass of sequentializable L-nets, the L S -nets 1 .

The key technical result about L S -nets is the Splitting Lemma, which we prove in Appendix C. The core of the paper lies in Sections 4 through 8: we present our basic (co)algebra of elementary operations on L-nets (Sections 4 and 7), we describe our sequentialization and desequentialization procedures (Sections 5 and 6, respectively), and we relate them (Section 8). In Section 9, we impose connectedness restrictions on both the source and target of the procedures, so as to adjust the picture to Girard's original designs. Section 10 is a concluding section.

Tree strategies and sequent calculus derivations

Designs, introduced in [START_REF] Girard | Locus solum[END_REF], have a twofold nature: they are at the same time semantic structures (an innocent strategy, presented as a set of views) and syntactic structures, which can be understood as abstract sequent calculus derivations (in a focusing calculus, which we will introduce next).

In the following, we review in which (intuitive) sense a tree strategy can be associated with a sequent calculus derivation, and vice versa. In Appendix B, we provide formal procedures.

Focalization and synthetic connectives

Multiplicative and additive connectives of linear logic separate into two families: synchronous (also called positive) connectives: ⊗, ⊕, 1, 0, and asynchronous (or negative) ones:

& , &, ⊥, . A formula is positive (negative) if its outermost connective is positive (negative).

A cluster of connectives with the same polarity can be seen as a single connective (called a synthetic connective), and a "cascade" of decompositions with the same polarity as a single rule. This corresponds to a property known as focalization, discovered by Andreoli (see [START_REF] Andreoli | Focussing and proof construction[END_REF]), and which provides a (complete) so-called focusing strategy in proof-search: (i) negative connectives, if any, are given priority for persistent decomposition, (ii) when a subgoal containing only positive formulas is reached, choose a positive focus, and persistently decompose it up to its negative sub-formulas.

The division of connectives into positive and negative ones is not only fundamental to proof-search in linear logic, but also corresponds to the Opponent/Player alternation in a strategy. Shift. To these standard connectives, it is natural to add two new (dual) connectives, called shift2 : ↓ (positive) and ↑ (negative). The role of the shift operators is to change the polarity of a formula: if N is negative, ↓ N is positive, and if P is positive, ↑ P is negative. When decomposing a positive connective into its negative subformulas (or viceversa), the shift marks the polarity change. As an example, the formula (A&B) ⊕ (C ⊗ D) should now be written (↓ (A &B )) ⊕ (C ⊗ D ), where, say, A is the result of recursively decorating A with shift operators. The shift is the connective which captures "time" (or sequentiality): it marks a step in computation.

Focusing calculus. Focalization is captured by the following sequent calculus, originally introduced by Girard in [START_REF] Girard | On the meaning of logical rules I: syntax vs. semantics[END_REF], and closely related to Andreoli's focusing calculus (see [START_REF] Andreoli | Focussing and proof construction[END_REF]). We refer to those papers for more details.

Axioms: x ⊥ , x

We assume by convention that all atoms x are positive (hence x ⊥ is negative).

Any positive (resp. negative) cluster of connectives can be written as a ⊕ of ⊗ (resp. a & of & ), modulo distributivity and associativity. The rules for synthetic connectives are as follows. Notice that each rule has labels; rather than more usual labels such as ⊗L, ⊗R, etc., we use formulas in the labels, as described below.

Positive connectives:

Let P (N 1 , . . . , N n ) = ⊕ I∈N (⊗ i∈I (↓ N i ))
, where N is a set of sets I of indices. Each ⊗ i∈I (↓ N i ) is called an additive component. In the calculus, there is an introduction rule for each additive component:

. . . N i , ∆ i . . . N j , ∆ j . . . P, . . . , ∆ i , . . . , ∆ j , . . . (P, N I )

A positive rule is labelled with a pair of (i) the active formula (or focus) P of the conclusion, and (ii) the set N I = {N i : i ∈ I} of the subformulas of the additive component to which the rule corresponds. Note that we should rather speak of a rule scheme, because even when P and N I have been fixed, there remains freedom in the way of splitting the rest of the sequent between the premises.

Negative connectives: Let N (P 1 , . . . , P n ) = & I∈N ( & i∈I (↑ P i ))
. It admits only one introduction rule, which has a premise for each additive component & i∈I (↑ P i ):

. . . P I , ∆ P J , ∆ . . . N, ∆ {. . . , (N, P I ), (N, P J ), . . . } where P I = {P i : i ∈ I}. A negative rule is labelled by a set of pairs, each of the form (focus, set of subformulas), for each premise.

We call each of the pairs we used in the labels an action. We call an action positive (resp. negative) if it appears in the label of a positive (resp. negative) rule. In a negative rule, there is an action for each additive component.

In the purely multiplicative case (no connectives ⊕, &), all negative rules have a single premise, and hence are labelled by a single action, while only one rule can be applied to each positive connective.

It is important to notice the duality between positive and negative rules: each premise (encoded by the action) (N, P I ) of a negative rule corresponds to one positive rule (N ⊥ , P ⊥ I ) (where

P ⊥ I = {N ⊥ i : i ∈ I}).
Another observation is that, starting with a proof of a sequent P or N consisting of one formula only, the rules maintain the invariant that all sequents contain at most one negative formula, a fact that can be stressed by writing N ⊥ ∆ (resp.

N ⊥ i ∆ i , N ⊥ j ∆ j ,...) instead of N, ∆ (resp. N i , ∆ i , N j , ∆ j ,. . . ).
Finally we note the following two special cases of the positive and negative rules (when N = {I} is a singleton and I is a singleton):

N ⊥ ∆ ↓ N, ∆ (↓ N, N ) P, ∆ (↑ P ) ⊥ ∆ (↑ P, P )
In the sequel, we shall keep the shift operators implicit, except in those special cases. As a matter of fact, all the other shift operators can be (uniquely) reconstructed.

Sequent derivation

Typed . . . a 0 , c (c, M I ) a ⊥ c (a, {a 0 }) . . . b 0 , d (d, N J ) b ⊥ d (b, {b 0 }) c, d, a ⊗ b (a ⊗ b), {a, b}) (c & d) ⊥ a ⊗ b (c & d, {c, d}) (c & d,{c,d}) (a⊗b,{a,b}) (a,{a0}) (c,MI ) . . . (b,{b0}) (d,NJ ) . . . Untyped . . . ξ10, σ 1 (σ 1 , I) ξ1 σ 1 (ξ1, {0}) . . . ξ 2 0, σ2 (σ 2 , J) ξ2 σ 2 (ξ2, {0}) σ1, σ2, ξ (ξ, {1, 2}) σ ξ (σ, {1, 2}) (σ,{1,2}) (ξ,{1,2}) (ξ1,{0}) (σ1,I)
. . .

(ξ2,{0}) (σ2,J)
. . .

Designs as (untyped) focusing proofs

Designs are an abstract version of focusing proofs. They are obtained in two steps. One transforms a sequent calculus proof into a tree whose nodes are labelled by actions, and one replaces all the formula occurrences by addresses. Conversely, given a design, we can build the "skeleton" of a sequent calculus derivation. Such a skeleton becomes a concrete (typed) derivation as soon as we are able to decorate it with types. Let us sketch this using an example.

First example. Consider the (purely multiplicative) derivation on the l.h.s. of Figure 1, where a =↑ a 0 and b =↑ b 0 are negative formulas and where c, d are positive formulas. By forgetting everything in the sequent derivation but the labels of the rules, we obtain the tree depicted in the top right corner of Figure 1. This representation is more concise than the original sequent proof, but it still carries all relevant information, i.e., the sequents can be reconstructed. For example, when we apply the ⊗ rule, we know that the context of a ⊗ b is c, d, because they are used afterwards (above). After the decomposition of a ⊗ b, we know that c (resp. d) is in the context of a (resp. b) because it is used after a (resp. b).

Addresses (loci).

One of the essential features of ludics is that proofs do not manipulate formulas, but addresses. An address is a sequence of natural numbers, which could be thought of as a name, a channel, or as the address of a memory cell where an occurrence of a formula is stored. If we give address ξ to an occurrence of a formula, its (immediate) subformulas will receive addresses ξi, ξj, etc. Let a = ((

p 1 & p 2 ) ⊗ q ⊥ ) ⊕ r ⊥ .
If we locate a at the address ξ, we can locate p 1 & p 2 , q, r respectively at ξ1, ξ2, ξ3 (the choice of addresses is arbitrary, as long as each occurrence receives a distinct immediate extension of ξ).

Let us consider an action, say, (P, N I ), where N I corresponds to ⊗ i∈I (↓ N i ). Its translation is (ξ, K), where ξ is the address of P , and K is the (finite) set of natural numbers corresponding to the relative addresses i of the subformulas N i .

First example, continued. Coming back to our example (Figure 1), let us abstract from the type annotation (the formulas), and work with addresses. We locate a ⊗ b at the address ξ; for its subformulas a and b we choose the subaddresses ξ1 and ξ2. In the same way, we locate c & d, c, d, a 0 , b 0 at the addresses σ, σ1, σ2, ξ10, ξ20, respectively. The result is depicted in the bottom right corner of Figure 1.

The two successive transformations are in fact independent. One can first transform formulas into addresses in the sequent calculus proof, yielding the bottom left abstract sequent derivation, and then keep only the tree of abstract labels. In Girard's terminology, the bottom left derivation and the bottom right tree are called dessin and dessein, respectively: they are the syntactic face and the semantic face of the same objects, which are called designs.

To indicate the polarity, in our pictures of designs and L-nets, we circle positive actions (to remind that they are clusters of ⊗ and ⊕).

Understanding the additives.

A &-rule must be thought of as the superposition of two unary rules on the same formula, corresponding to the two actions (a&b, a) and (a&b, b). Given a sequent calculus derivation in Multiplicative Additive Linear Logic (MALL), if for each &-rule we select one of the premises, we obtain a derivation where all &-rules are unary. This is called a slice [START_REF] Girard | Linear logic[END_REF]. For example, the derivation on the l.h.s. below can be decomposed into the slices on the r.h.s.: A more structured example. Let

a = (m ⊗ n) ⊕ c , m = (p 1 & p 2 )&(q 1 & q 2 )&r , n = b 1 & b 2 & b 3 ,
with r, p i , q i , b i (i = 1, 2) positive formulas. Consider the following derivation: is a bipole, and the partition of the negative actions consists of the two sets {(ξ2, {1, 2, 3})} and {(ξ1, {1, 2}), (ξ1, {3, 4}), (ξ1, {5})} .

. . . p 1 , p 2 (p 1 , . . .) . . . q 1 , q 2 (q 2 , . . .) . . . r (r, . . .) m R 1 . . . b 1 , b 2 , b 3 . . . n R 2 (m ⊗ n) ⊕ c a, {m, n} where R 1 = {(m, {p 1 , p 2 }), (m, {q 1 , q 2 }), (m, r)} and R 2 = {(n, {b 1 , b 2 , b 3 })}.
Relating two orders: towards proof-nets. Let us consider a multiplicative design (or a slice). We are given two partial orders, which correspond to two kinds of information on each action k = (σ, I): (i) a time relation (sequential order), specified by the tree structure of the design; (ii) a space relation (prefix order), corresponding to the relation of being subaddress (the arena dependency in game semantics).

Let us look again at our first example of design. We make explicit the relation of being a subaddress with a dashed arrow, as follows:

ξ σ σ2 σ1 1, 2 1, 2 0 ξ1 0 ξ2 0 0 σ ξ ξ1 ξ2 σ1 σ2
If we emphasize the prefix order rather than the sequential order, we recognize something similar to a proof-net (see [START_REF] Faggian | Travelling on designs: ludics dynamics[END_REF]), with some additional information on sequentialization. Taking forward this idea of proof-nets leads us to L-nets.

L-nets and L S -nets

In this section, we recall the notion of L-net of Faggian and Maurel [START_REF] Faggian | Ludics nets, a game model of concurrent interaction[END_REF]. We drop the Acyclicity condition3 , which we replace in Section 3.7 by a stronger condition. We will call L S -nets the class of L-nets which satisfy the stronger condition.

L-nets have an internal structure, described by a directed acyclic graph (d.a.g.) on polarized actions, and an interface, providing the names on which the L-net can communicate with the rest of the world.

Actions (moves).

An action is either the special symbol † (called daimon) or (cf. above) a pair k = (ξ, I) given by an address ξ and a finite set I of indices (which are natural numbers). We say that k uses the address ξ.

The prefix relation induces a relation between the actions. We say that an action (ξ, I) generates the addresses ξi, for all i ∈ I, and that a is parent of b, if the action a generates the address of the action b (i.e., a = (ξ, I) is parent of b = (ξi, K)).

A polarized action is given by an action k together with a polarity, positive (k + ) or negative (k -). The parent relation extends to polarized actions, with the condition that if a is parent of b, their polarity must be opposite. (Or, equivalently, all addresses of the same length have the same polarity.)

The action † is defined to be positive. When clear from the context, or not relevant, we omit the explicit indication of the polarity.

Arena. Actions together with the parent relation define what could be called a universal arena.

Interface

An interface (called base in [START_REF] Girard | Locus solum[END_REF]) is a pair of finite sets Ξ, Λ of addresses, which we write as a sequent Ξ Λ, and which we call the negative and the positive addresses (or the inner and the outer names) of the interface, respectively. The addresses must be pairwise disjoint, i.e., incomparable with respect to the prefix relation. We think of the inner names as passive, or receiving, and of the outer names as active or sending.

We impose that Ξ is either empty or a singleton (cf. Section 2.1).

Directed graphs (d.a.g.) and terminology

We recall that a directed acyclic graph (d.a.g.) G is an oriented graph without (oriented) cycles. In all our pictures, the edges are oriented downwards. We consider any directed acyclic graphs G up to its transitive closure. In fact, we will only be interested in the properties of non transitive edges. An edge is called transitive if there exists another oriented path (of length > 1) from its source to its target.

We write c ← b if there is a non transitive edge from b to c. We say that c is the predecessor of b We use + ← for the transitive closure of ←. Sometimes, when describing operations on graphs, it is convenient to uniformly add to the graph an edge with a certain property, without caring if this edge is transitive or not. In such a case, we write c ←b.

A node n of G is called minimal (resp. maximal) if there is no node a such that a ← n (resp. n ← a). Downward closure. Given a node n ∈ G, we denote by n ↓ (the downward closure of n) the sub-graph induced by restriction of G on {n} ∪ {n : n + ← n}. D.a.g.'s and partial orders. It is standard to represent a strict partial order as a d.a.g., where we have a ← b whenever a < 1 b (i.e., there is no c such that a < c and c < b.) Conversely, (the transitive closure of) a d.a.g. is a strict partial order on the nodes (or equivalently on the labels, if the nodes are labelled and all the labels are distinct).

L-nets

Nodes labelled by actions. We are going to work with nodes labelled by polarized actions. In the sequel, depending on the context, k = (ξ, I) will read as either "k is a node labelled by (ξ, I)", or "k is an action equal to (ξ, I)". We shall let k, a, b, c, . . . range over nodes and actions. We extend to nodes the terminology we have introduced for the actions. We will say that a node is positive or negative, and that a node uses or generates an address, if it is the case for the labelling action. Definition 3.1 (L-nets) An L-net D is given by:

• An interface Ξ Λ. If Ξ is empty (resp. non-empty), D is called positive (resp.
negative).

• A possibly infinite set A of nodes which are labelled by polarized actions 4 .

4 Hence nodes are occurrences of actions.

• A structure on A of directed acyclic bipartite graph (if k ← k , the two nodes have opposite polarity) which satisfies conditions 1-4 and 5-6 below.

1. Views. For each node k, all the addresses used in k ↓ are distinct .

2.

Parents.

-For each node a, using address σ, either σ belongs to the interface (and then the polarity of a is as indicated by the interface), or σ has been generated by (the action of) a preceding node c (It follows that if a negative node is not minimal then its parent is its unique predecessor.) 3. Negativity. If Ξ = {ξ} is not empty and D is not empty, then at least one node uses ξ.

4.

Positivity. If a is maximal w.r.t. ←, then it is positive.

The conditions so far are enough if all addresses are distinct (i.e., if the structure is purely multiplicative). Conditions 5-6 below allow us to deal with the multiple use of addresses induced by the additive structure.

Two distinct negative nodes are called sibling -and we say that they form an additive pair -if they use the same address and if either they have the same predecessor, or they are both minimal.

5.

Sibling. Any two sibling nodes have distinct labels, i.e., of the form (σ, I 1 ), (σ, I 2 ), with I 1 = I 2 .

6. Additives. Given two distinct positive nodes k 1 , k 2 which use the same address ξ (i.e., k 1 = (ξ, K 1 ), k 2 = (ξ, K 2 )), there exists an additive pair w 1 , w 2 such that w 1 + ← k 1 , and

w 2 + ← k 2 .
Remark 3.2 Note that by condition Parents every minimal node uses an address in the basis. Conversely, the same condition also imposes an action using the negative address of the base (if any) to be minimal, but actions using a positive address of the base need not be minimal.

In order to obtain a good computational behaviour of L-nets as strategies, and to be able to relate them to sequential innocent strategies, we still need a correctness criterion on graphs, which we give in Section 3.7. If we have in mind the theory of proof-nets, L-nets can be seen as "proof-structures."

The key role of condition Additives is to ensure a one-to-one correspondence between the nodes of an L-net and the sets of actions in their downward closure, that represent their history, or their preconditions.

Lemma 3.3 For each pair of distinct nodes k, k of an L-net D, the sets of actions of

k ↓ and k ↓ are different.
Proof. Suppose that the sets of actions of k ↓ and k ↓ are the same. Then in particular there exists some k 1 ∈ k ↓ such that k and k 1 have the same label. We distinguish two cases:

• If k 1 = k , then k ↓
1 is strictly contained in k ↓ , and hence by our assumption k 1 and k must be distinct.

• If k 1 = k , then k 1 = k by assumption.
Hence in both cases we have proved that k 1 and k are distinct. By condition Additives, there exists an additive pair w 1 , w 2 such that w 1 ∈ k ↓ and w 2 ∈ k ↓ 1 (and hence w 2 ∈ k ↓ ). Then, by our assumption, there is a node w ∈ k ↓ that has the same label as w 2 : this is impossible, as it would violate condition Views applied to k.

Rules and conclusions.

A negative rule is a maximal set of (negative) sibling nodes. A positive rule consists of a single positive node. The positive nodes induce a partition of the d.a.g. into bipoles (cf. Section 2.2). Each bipole itself is partitioned into a positive rule (its root) and a set of negative rules. For example, the following bipole has two negative rules (R

1 = {(σ1, J)} and R 2 = {(σ2, J ), (σ2, J )}) and one positive rule (R = {(σ, {1, 2})}). (σ,{1,2}) (σ1,J) (σ2,J ) (σ2,J )
We say that a rule is unary if it is a singleton (a positive rule is always unary). When a rule is not unary, we call it an additive rule (think of each action as an additive component, cf. Section 2.2). Note that an additive rule is necessarily a negative rule, but negative rules can be unary (see Section 3.6). Note also that if w 1 , w 2 form an additive pair, then w 1 , w 2 belong to the same negative rule.

By analogy with proof-nets, we call conclusion a rule whose nodes are all minimal. We also observe that by condition Parents and Negativity, an L-net is positive if and only it has only positive conclusions, and a (non-empty) L-net is negative if and only if it has a negative conclusion. Note that an L-net can have at most one negative conclusion, by definition of a rule, and by the assumption that a basis contains at most one negative address.

Slices

We call purely multiplicative an L-net in which all used addresses are distinct, or, equivalently by condition Additives, in which all negative rules are unary (there are no additive pairs).

A slice S of an L-net D is a (downward closed) subgraph of D which is a purely multiplicative.

In this paper, by slice we always mean a maximal slice.

Correctness criterion: L S -nets

We recall that we are only interested in the properties of non transitive edges. All conditions in this section are therefore on the skeleton of the graph.

Paths.

The following notions are relative to some L-net D. An edge is an entering edge of the node a if it has a as target. If R is a negative rule and e an entering edge of an action a ∈ R, we call e a switching edge of R.

A rule path is a sequence of nodes k 1 , ...k n belonging to distinct rules, and such that for each i < n either k i → k i+1 (the path is going down) or k i ← k i+1 (the path is going up). A rule cycle is defined similarly as a sequence of nodes k 1 , ...k n , k n+1 , where the k i 's (i ≤ n) are distinct, where k 1 = k n+1 , and for each i < n + 1 either

k i → k i+1 or k i ← k i+1 .
A switching path is a rule path which uses at most one switching edge for each negative rule, i.e., the path does not contain three successive nodes

k i-1 , k i , k i+1 such that k i is negative, k i ← k i-1 , and k i ← k i+1 .
A switching cycle is a rule cycle which uses at most one switching edge for each negative rule. Now we can complete the definition of L S -net. We want to be able to sequentialize our graphs. The following condition (which can be seen as a correctness criterion) guarantees that it is always possible to find a rule which does not depend on others.

Definition 3.4 (L S -nets) An L S -net is an L-net such that the following condition holds:

• Cycles. Given a non-empty union C of switching cycles, there is an additive rule W not intersecting C, and a pair w 1 , w 2 ∈ W such that for some nodes

c 1 , c 2 ∈ C, w 1 + ← c 1 , and w 2 + ← c 2 .
L-nets and L S -nets. The condition Cycles strengthens the Acyclicity condition of [START_REF] Faggian | Ludics nets, a game model of concurrent interaction[END_REF]. Acyclicity asserts that there are no switching cycles in a slice. It is immediate that the condition Cycles implies the acyclicity condition, and reduces to it in a purely mutliplicative framework (i.e., in the absence of any additive rule). Notice that while acyclicity is a property of a slice, the new condition speaks of cycles which traverse slices.

L-nets as sets of views / chronicles

Just as innocent strategies (and designs), an L-net can be presented as a set of views, with some properties. In this setting, a view is not a sequence of moves, but a partial order (with a top element).

Views/chronicles.

Definition 3.5 (Chronicles) We call chronicle (or view) on Ξ Λ a set c of polarized actions equipped with a partial order, such that: c has a top element, if a < 1 b (cf. Section 3.3), they have opposite polarity, and c satisfies (the analog of) condition Parents.

A chronicle is positive or negative according to the polarity of its top element.

We define a partial order on chronicles as follows: c c if c is the restriction of c to {x : x ≤ a}, for a certain a ∈ c . A set S of chronicles is closed under restriction if c ∈ S and c c implies c ∈ S.

From L-nets to sets of chronicles. Any node k of an L-net D defines a chronicle: indeed, k ↓ induces a partial order on its nodes (cf. Section 3.3) and by the condition Views, there is a one-to-one correspondence between the nodes and the actions in k ↓ . Let n be the action labelling the node n. We set:

k = {n : n ∈ k ↓ },
with the order induced by ← .

Hence we can associate to each L-net D a set Views(D) of chronicles, as follows:

Views(D) = { n : n is a node of D} .
The set Views(D) is closed under restriction.

From sets of chronicles to L-nets. Conversely, given a set ∆ of chronicles which is closed under restriction, we define a directed graph Graph(∆) as follows: the nodes are the elements of ∆, and c ← c iff c 1 c .

Lemma 3.6 Let ∆ be a (possibly infinite) set of chronicles closed under restriction. Graph(∆) is an L-net iff it satisfies conditions Positivity and Additives.

Proof.

The conditions Parents and Views hold obviously. Condition Sibling also holds: two negative chronicles with the same parent c have the form c 1 = c ∪ a and

c 2 = c ∪ b. If c 1 = c 2 , necessarily a = b.
It is rather easy to express both Positivity and Additives in terms of chronicles. Hence we can also define an-L-net on a given interface as a set of chronicles closed under restriction, which satisfies (the analogue of) Positivity and Additives.

Relating the presentations. It is immediate that Views(Graph(∆)) = ∆, if ∆ is a set of chronicles closed under restriction. Conversely, given (the skeleton of) an L-net D, we have that Graph(Views(D)) is isomorphic to D (easy consequence of Lemma 3.3).

Summarizing, we have shown that Views and Graph are inverse bijections. We will use both presentations for L-nets. The presentation of L-nets as sets of chronicles, on which we will largely rely, allows us to compare nodes in different graphs, by comparing the corresponding chronicles. (In particular, this makes it possible to treat easily the superposition of two L-nets, see Section 4.3 and Appendix A.2). Sometimes, the graph presentation is more intuitive. However, it is obvious that all notions and conditions can be expressed in either terms. Observe in particular that

k 1 + ← k 2 iff k 1 k 2 iff k 1 < k 2 in k 2 .
Conventions. We will often not distinguish between isomorphic notions. Moreover, to keep notation simple, we will sometimes write k ∈ c (for example, k ∈ k ) instead of k ∈ c. We will also use the action for the node labelled by that action, when the node is uniquely determined.

When we want to make clear or stress the polarity, we explicitly decorate actions, nodes, chronicles and L-nets with their polarity (for example, k + , c + , D + ).

Designs and L-forests

If the chronicles are totally ordered (that is, if they are sequences of actions), the above definitions produce a forest, corresponding to a "standard" (sequential) innocent strategy. In particular, the designs of [START_REF] Girard | Locus solum[END_REF] can be regarded as a special case of L-nets: they are those L-nets Π such that:

1. Π is a forest and branches only on positive nodes; 2. there is a unique conclusion.

(We speak here of L-nets rather than L S -nets, because condition Cycles is vacuous for forests.)

If we do not impose conditions on the branching into nodes, we obtain a more general notion.

Definition 3.7 An L-forest is an L-net Π such that:

1. Π is a forest;

all conclusions have the same polarity (hence, if Π is negative, then it has only one conclusion, which is negative).

In Appendix B, we will show that L-forests arise from adding a form of MIX rule to the sequent calculus underlying designs. L-forests provide the natural target and source for our sequentialization and desequentialization procedures. In Section 9, we will restrict our setting to the L-nets which correspond to designs.

Sequential versus parallel strategies: an overview

Part of the process of abstraction leading from the syntax to strategies is that an action (a move) can be seen as a cluster of operations that can be performed together (thanks to focalization). However, in a tree strategy (L-forests, designs, innocent strategies...) there remains a lot of artificial sequentiality, in the same way as in sequent calculus proofs for linear logic. In the case of proofs, the solution has been to develop proofnets, a theory which has revealed itself extremely fruitful. The advantage of proof-nets is that information which is irrelevant to the "essence" of the proof is forgotten. More precisely, proof-nets allow us to identify sequent calculus derivations which only differ by some permutations of rules. Consider, for example, the two standard derivations

a, a ⊥ b, b ⊥ c, c ⊥ . . . (a ⊥ ⊗ b) a ⊥ ⊗ b, b ⊥ ⊗ c, . . . (b ⊥ ⊗ c) and a, a ⊥ b, b ⊥ c, c ⊥ . . . (b ⊥ ⊗ c) a ⊥ ⊗ b, b ⊥ ⊗ c, . . . (a ⊥ ⊗ b)
and compare them with the (unique) corresponding proof-net, which has the following shape:

⊗ ⊗
The different permutations of the rules correspond to different sequentializations of the proof-net, that is, in our view, to different schedulings of the rules.

Similarly, sequential strategies (hence designs, in particular) distinguish proofs (or programs) which only differ by the order in which the operations are performed. The situation is in fact the same as for the sequent calculus, and we want to apply similar techniques.

We will define two procedures which we call desequentialization and sequentialization, that associate

• an L S -net deseq Π to an L-forest Π (Section 6), and

• a set of L-forests {seq D} to an L S -net D (Section 5), respectively.

All dependency which is taken away by desequentialization can be (non-deterministically) restored through sequentialization (Theorem 8.2). The non-determinism corresponds to the fact that several L-forests Π i can be associated to the same L S -net D, each of which can be recovered by sequentialization of D. In Section 7, we make precise in which sense deseq Π has less sequentiality than Π, and give a description of the L Snets of "minimal sequentiality" (which we call parallel L-nets), based on the operations presented in Section 4.

Why targetting L-forests. An L-net does not need to be connected (in the ordinary graph-theoretic sense). Non-connectedness is a natural and desirable feature if we want both parallelism and partial proofs, that is, proofs which can be completed into a proper proof. Actually, non-connectedness is an ingredient of Andreoli's concurrent proof construction [START_REF] Andreoli | Focussing proof-net construction as a middleware paradigm[END_REF]. On the logical side, non-connectedness corresponds to the MIX rule (which is refused in [START_REF] Girard | Locus solum[END_REF]).

We first prove a sequentialization (and desequentialization) result that holds for all L S -nets, and that has L-forests as target. In Section 9, we shall restrict this procedure so as to have designs as target.

Operations on L S -nets

In this section, we introduce operations that allow us to decompose and recompose L-nets and L S -nets. We shall make an intense use of these operations in Sections 4.2 through 4.6 where we shall describe sequentialization and desequentialization of L Snets.

Preliminary properties

A convenient notion is that of partial strategy. We say that an L-net is partial if it does not satisfy condition Positivity.

We will make a repeated use of the following result. Observe that any cycle in G is also a cycle in D. If we have a collection of switching cycles inside G, the condition Cycles for D gives us an additive rule W that is not traversed by any of the cycles, and a pair w 1 , w 2 ∈ W ∩ G. Then, taking W ∩ G, w 1 , and w 2 , the condition holds in G.

Rooting and boxing

The following constructions add a new unary conclusion.

Definition 4.3 (Rooting)

Let D be a positive or negative L-net (of interface ξi, ξj, . . . , ∆ or ξi ∆). Let (ξ, I) be a negative or positive action, respectively. We indicate by x • D the graph obtained as follows:

1. add a node x = (ξ, I) to D; 2. add an edge x ←k for each node k which uses an address ξi (for some i ∈ I).

If (ξ, I) is positive, the result is always an L-net (on the interface ξ, ∆). If (ξ, I) is negative, the result is a possibly partial L-net (on the interface ξ ∆). The condition Positivity is satisfied only if at least one of the addresses ξi is used in D. Definition 4.4 (Boxing) Let D be a positive L-net (of interface ξi, ξj, . . . , ∆) and let (ξ, I) be a negative action, with i, j, . . . ∈ I. We indicate by x D the graph obtained as follows:

1. add a node x = (ξ, I) to D;

add an edge x ← k for each node k which belongs to a conclusion of D.

The result is clearly an L-net of interface ξ ∆.

Remark 4.5 Note that we have used ←and ← in the definitions of rooting and boxing, respectively. This accounts for the fact that in the case of rooting an added edge (ξ, I) ←k might be non transitive if k uses an address ξi and is situated above a node using an address ξj.

On positive L-nets, rooting or boxing give us two choices for adding a new negative node:

• Rooting is a parallel operation, in the sense that it only adds the minimum amount of sequentiality which is necessary for the satisfaction of condition Parents.

• Boxing instead is a serial (sequential) operation, which adds a maximal amount of sequentiality. If we think in terms of proof-nets, boxing corresponds to enclosing D in a box, which has x as principal port.

As we shall see in Section 7, repetitive and consistent use of rooting and boxing will lead to (abstract versions of) proof-nets and sequent calculus derivations, respectively.

Remark 4.6 Rooting and Boxing are two extremes. In between, we can define intermediate operators which add, on top of rooting, as much sequentiality as we wish: after rooting, we add any number of edges from positive nodes to x. Let us indicate this (generically) by x D. Hence, with respect to the order on the nodes, we have:

Order (x • D) ⊆ Order (x D) ⊆ Order(x D) .
The differences between the three L-nets is only the amount of order between x and the nodes of D.

Superposition of L-nets.

The union of a collection of L-nets is their union as sets of chronicles. The union is not disjoint in general; we also call this operation superposition. Under which conditions is a union of L-nets an L-net? By Lemma 3.6, if D 1 , D 2 are L-nets (resp. L S -nets), D 1 ∪ D 2 is an L-net (resp. an L S -net) iff it satisfies condition Additives (resp. conditions Additives and Cycles). An especially relevant case is the following one, which we single out.

(k + • D 1 ) ∪ (k + • D 2 ) is an L S -net.
Proof.

Condition Additives is obviously inherited by the disjointness assumption. We show that this also true of condition Cycles. Suppose that there is a switching cycle traversing both D 1 and D 2 , and consider two minimal portions of the cycle going from D 1 to D 2 and from D 2 to D 1 , respectively. At most one of these portions can go through k. Thus, the other portion consists of two consecutive nodes c 1 and c 2 , with, say, c 1 ∈ D 1 , c 2 ∈ D 2 , and c 1 1 c 2 , contradicting the disjointness assumption.

Remark 4.8 In defining the superposition of graphs it is crucial that we work not just with nodes, but with their view. This allows us to compare nodes belonging to different graphs. This fact plays a key role when defining additive union (below).

Splitting

The following key lemma allows us to decompose a positive L S -net which satisfies the condition Cycles into disjoint components, where each component is itself an L S -net.

Definition 4.9 (Splitting rules)

1. A negative rule W = {. . . , w I , . . .} of an Lnet D is called splitting if either it is conclusion of D (each w I is a root), or if deleting the edges w ← w I to the root of W 's bipole (for all w I ∈ W ), there is no more connection (i.e., no sequence of consecutive edges) between any of the w I 's and w.

A positive rule of D is called splitting if it is a conclusion and all negative rules

just above it are splitting. 2. Suppose for a contradiction that there are two nodes k 1 , k 2 , say in D ξi and in D ξj using the same address. By condition Additives applied to D, there exists an additive pair w 1 , w 2 , with w 1 , w 2 below k 1 , k 2 , respectively, which by downward closedness implies w 1 ∈ D ξi and w 2 ∈ D ξj . This is impossible because all the nodes in any negative rule W of D belong to the same connected component.

Root removal

The following operation allows us to decompose a negative L-net, whose negative conclusion is unary (this is the only negative destructor we need in the case of a purely multiplicative L-net). It is immediate that the result is an L-net on the interface . . . , ξi, . . . , ∆ (i ∈ I).

Additive structure

In a setting in which all negative rules are unary (as for slices or in multiplicative linear logic), root removal is all we need to decompose a negative L-net. In a general setting, the following constructions allow us to decompose, and to reconstruct, a negative L-net. Intuitively, Φ is a function on chronicles which marks with an edge towards x I the chronicles of D I which are specific to it, or more precisely those chronicles which are not shared by all D J 's.

Remark 4.15 Notice that if the set of D I 's is a singleton, then Φ(D I ) = D I . This remark will allow us to treat both unary and non unary conclusions as a single case.

The following two lemmas will play a crucial role in the decomposition of L-nets. Their statement refers to the notations in Definition 4.14. Given a collection of switching cycles, assume it is contained inside one of the Φ(D J )'s: in such a case the additive pair is given by the condition applied to Φ(D J ).

Otherwise, we have at least a node k 1 ∈ B I and a node k 2 ∈ B J (with I = J) traversed by the cycles. By construction, x I + ← k 1 and x J + ← k 2 , and condition Cycles is satisfied.

Remark 4.18

Notice that D J is not an L-net in general , because its maximal chronicles do not need to be positive.

Proof.

1. By Lemma 4.16, we can write D = C ( J B J ). We compute Scope(x I , D):

• by definition of scoping, the B J 's (J = I) are left out;

• no chronicle of C contains an x J , since C is disjoint from each B I ;

• every chronicle of B I contains x I , and hence no chronicle of B I contains any x J (J = I), by condition Views.

It follows that Scope(x I , D) = C B I = Φ(D I ).

2. This follows immediately from 1, since all what Φ does to D I is undone when x I is removed.

Constructors and destructors

Summing up the content of this section, the operators we have presented can be grouped into two families:

• Rooting, boxing, union and additive union are constructors.

• Splitting, root removal, and scoping are destructors. The decomposition of an L S -net goes as follows:

D is positive. All conclusions are positive. If there are no negative rules, we are finished: our L-net is reduced to its conclusions. Otherwise, by splitting, D = ( i (x

• D i )) C. Hence D . . . , D i , . . . , C .
D is negative (and non empty). Let X be the unique negative conclusion of D.

i. If X is unary, we decompose D by root removal. ii. Otherwise, we reduce D to the previous case by scoping.

In general terms, assuming X = {. . . , x I , . . . } we have:

D

. . . , Scope(x I , D) \ x I , . . . .

These constructors and destructors are put to use in the following sections.

Sequentializing a graph strategy

An edge of an L-net states a dependency, an enabling relation, or a precedence among actions. The aim of this section is to provide a procedure, which takes an L S -net and adds sequentiality in such a way that the constraints specified by the L-net are respected.

Let us consider a very simple example: a chronicle c, i.e., a partially ordered view. A sequentialization of c is a linear extension of the partial order. That is, we add sequentiality (edges) to obtain a total order. A total order which extends c will define a complete scheduling of the tasks, respecting the constraint that each action is performed only after all of its constraints are satisfied.

Dependency between the actions of a slice, and of sets of slices (L-nets) is more subtle, as there are also global constraints. The key point in the sequentialization is to select a rule which does not depend on others. This is exactly the role of the Splitting Lemma, and the reason for the condition Cycles.

The process of sequentialization is non-deterministic, as one can expect, i.e., there are several tree strategies which can be associated to the same L S -net.

As we have both multiplicative and additive structure, when sequentializing we will perform two tasks:

1. add sequentiality (sequential links) until the order in each chronicle is completely determined;

2. separate slices which are shared through additive superposition. Otherwise we select a positive splitting rule x = (ξ, I) and proceed as follows. By Proposition 4.11, each of the components D i obtained by splitting is an L Snet whith a negative conclusion on an address ξi. Then:

• seq D = i (x • seq D i ).
2. Assume D = i C i , where the C i 's are the connected components of D. Then:

• seq D = i (seq C i ).
Proposition 5.1 If D is an L S -net on the interface Ξ ∆, seq D is an L-forest on the same interface.

Proof. We have already established all partial results needed to prove this. This procedure applies to infinite L-nets, by coinduction. Indeed, one can formally show that L-forests form a final coalgebra and the L S -nets form a coalgebra for a functor F on sets, and that seq is the associated unique coalgebra morphism. We only sketch the construction below. The reader unfamiliar with final coalgebra semantics can get the necessary background from [START_REF] Jacobs | A tutorial on (co)algebras and (co)induction[END_REF].

• One considers the functor F in the category of sets and functions that takes a set X to the disjoint union of the set of all finite sets whose elements are of the form ((ξ, I), {. . . , a i , . . .}), where the a i 's form a collection of elements of X indexed by a subset of I, and of the set of all {. . . , ((ζ, J), a J ), . . .}, where the a J 's form a collection of elements of X indexed by some N ⊆ P f (ω).

• One proves that the collection of all L-forests forms a final coalgebra for this functor. The situation is similar to that of, say, Böhm trees. The coalgebra structure takes a positive (respectively negative) L-forest and decomposes it into its root(s) and its immediate subforests.

• Thanks to the Splitting Lemma, one can choose a decomposition for each positive L S -net, and codify this "oracle" in the form of a coalgebra structure on the collection of all L S -nets.

• Then seq is the unique coalgebra morphism from this coalgebra to the final coalgebra. That it is a coalgebra morphism amounts to the equations given above to define seq D.

Desequentializing a tree strategy

We are now looking for a desequentialization transformation in the opposite direction, from L-forests to L S -nets. This transformation should take as input the output of the sequentialization procedure. We have already seen that the output of seq is only of a potential (or coinductive) nature. More precisely, its progressive construction yields at any step an actual finite part Π -the part of the forest that has been already recognized -, and a collection of L S -nets to sequentialize, each associated with a leaf of Π.

Dually, we shall desequentialize truncations of L-forests (up to an arbitrary finite level). The output of the procedure will be a finite L S -net D, on which one could graft appropriately the (possibly infinite) subforests that have been taken away by the truncation.

In order to define the desequentialization procedure, we need to introduce a new notion, that of decoration.

Making the axioms explicit: decorations. In Section 3.10, we have illustrated the purpose of desequentialization by taking as example the relation between proof-nets and sequent calculus derivations. Our aim is to remove some artificial sequentialization, while preserving essential information:

1. axioms (multiplicative proof-net = formula tree + axioms [Gir87]); 2. dependency due to additive rules: some nodes must not be shared.

The second issue is addressed by our definition of additive union (cf. Section 4.6). As for axioms, such information is present in the source L-forest (or design), but is implicit (and not univoque). To make the information on the axioms explicit (and univoque), we introduce an auxiliary notion, that of decorated node. Essentially, we decorate each leaf k with a set of addresses, which we denote by link(k); this information codes the axioms. For example, a leaf k = (ξ, {0}) which is decorated with the address σ will correspond to the axiom ξ0, σ. The decoration is closely related to the sequent calculus presentation of an L-forest, and we describe it in detail in Appendix B.

In Section 2.2, we already exemplified how to move from an L-forest to an explicit sequent calculus style presentation. Essentially, given an L-forest Π, we associate to each node k a sequent of addresses. Each leaf k = (ξ, I) in the forest will correspond to a generalized axiom in the sequent calculus derivation, of either (see Section B) of the two forms

ξ, Γ k = (ξ, I) + Γ k = †
The decoration we will use captures this information: we decorate each leaf k of the L-forest with the set Γ of addresses which appear in the sequent associated to k.

Decorated leaves as boxes.

The two ideas of truncation of an L-forest and of decorating the leaves of an L-forest are related, and complement each other. Suppose that we truncate the tree Π after the node k, leaving out the subtrees Π i , above k. The sequent associated to the node k, which is now a leaf, is the interface of the subtree

(k • Π i ).
Hence, the addresses in link(k) are meant as the addresses which are used in the Π i 's. In this sense, a decorated leaf acts as a sort of (black) box: we hide the content of the box (i.e., (k • Π i )) and only keep memory of the interface (the conclusion of the box).

Link sets versus infinitary expansions. In ludics, identity axioms are interpreted by infinitary strategies, called faxes in [START_REF] Girard | Locus solum[END_REF]. These strategies are an instance of the copy-cat strategies of game semantics. In such infinitary strategies, every generated action is eventually used. Faxes are the typical example of what we want to enclose in a box. Actually, even if we are establishing general results, the kind of strategies we are really interested in are those corresponding to proofs. Morally, the (real) use of link sets is to deal with finite truncations of these strategies. In other words, link sets are a way to express (in a finitary way) the axioms. Definition 6.1 A decorated L S -net is an L S -net D in which all leaves k are equipped with a finite set link (k) of addresses (called the link set of k), in such a way that the conditions on L S -nets hold with respect to all addresses (thus, including those in the link sets).

We still use D to denote a decorated L S -net.

Observe that if D is an L-net, and given an assignment of link sets to the leaves of D, all what we have to check for it to yield a decorated L S -net are conditions Parents and Additives.

From now on, we upgrade the definition of "a node uses an address" as follows:

Definition 6.2 (used addresses) Let k be a node labelled by an action and possibly a link set. We say that the node k uses an address ξ if either

• ξ is the address of the action, or

• ξ appears in the link set.

The extension of the operators we have introduced for L-nets to decorated L-nets is immediate. The upgraded definition plays a role only when rooting an L-net on a negative action: now (with the notation of Definition 4.3), we add an edge (ξ, I) ←k for each node k such that k is generated by (ξ, I), or k is a leaf such that ξi ∈ link (k). We maintain the same notations as in Section 4.

Remark 6.3

The new edges (ξ, I) ←k where k is a leaf such that ξi ∈ link (k) are close in spirit to the µ-pointers recently introduced by Laurent in his investigations on game semantics for first-order (classical) logic [Lau].

Observe that a label of a node is now a a decorated action, i.e., an action possibly together with a link set . Actions which are decorated in a different way are different, and we do not identify them. This is natural if we consider that they correspond to different axioms.

In the following, we define a desequentialization procedure, which takes as input finite decorated L-forests. More precisely we choose a special decoration discipline, which corresponds to the idea of making the axioms explicit. In Appendix B, we prove that it is always possible to choose a decoration which satisfies the following property.

Definition 6.4 (well-decorated) A well decorated L-net is a decorated L-net D such that all addresses of the interface, and all addresses generated by a negative action of D are used in D (in the sense of Definition 6.2).

Lemma 6.5 Every L-forest can be well decorated.

Proof. See Corollary B.5.

Desequentialization procedure.

Π is negative. Let X = {x I , x J , . . .} be the conclusion of Π. Let us call Π I the subforest above x I (i.e., Π = I (x I Π I )). Then:

• deseq Π = ↓ I (x I • deseq Π I ).
Π is positive.

1. Assume Π is a tree of conclusion x, using address ξ. If the tree is reduced to a single node, then we are done (base case). Otherwise, it has the form

Π = i (x • Π i ),
where each Π i is the subforest of all the trees on the address ξi (i ∈ I). Then:

• deseq Π = i (x • deseq Π i ).
2. Assume Π = i Π i . Then:

• deseq Π = i (deseq Π i ).
Proposition 6.6 If Π is a well decorated L-forest on the interface Ξ ∆, then deseq Π is an L S -net on the same interface.

Proof.

All steps needed to show that deseq Π is a partial L S -net are immediate. Notice that in the positive case, i (x • deseq Π i ) is an L S -net by Proposition 4.7 (since all the addresses used in different Π i 's are disjoint, so are the addresses of the deseq Π i 's).

Condition Positivity follows from Lemma 6.7 below, and by (the upgraded) definition of rooting.

Notice that decorations play a role only to prove that deseq D satisfies condition Positivity. Lemma 6.7 Let Π be a well decorated L-forest on the interface Ξ ∆. All the addresses of the interface are used in deseq Π.

Proof. Similar to the proof of Lemma 9.6.

Remark 6.8 At any step of the desequentialization:

• the sets of labels of Π and deseq Π are the same (intuitively, no node is deleted);

• if l is the label of a leaf in Π, it also labels a leaf in deseq Π.

An algebraic presentation

In this section, we focus on the L S -nets generated by the constructors (rooting, boxing, union and additive union), and we single out two important classes of L S -nets, obtained by consistently using rooting, or consistently using boxing, respectively (cf. Section 4.2). In the first case, we speak of parallel L-nets, which we regard as abstract proofnets. In the second case, we get the L-forests, which correspond to abstract sequent calculus derivations (see Appendix B).

In the following, we denote with D + a positive L-net, and with D - σ a negative Lnet whose negative conclusion has address σ. We denote by k + a (possibly decorated) positive action.

Abstract proof-nets. A parallel L-net is an L S -net generated by the following grammar:

D := D + | D - σ D + := E + . . . E + E + := k + | i∈I ((ξ, I) + • D - ξi ) D - σ := ↓ J (σ, J) -• D +
Such an L S -net has minimal sequentiality, in the sense that the we use constructors of minimal sequentiality.

Abstract sequent calculus derivations. The sequential L-nets are the L-nets generated by the following grammar:

D := D + | D - σ D + := E + . . . E + E + := k + | i∈I ((ξ, I) + • D - ξi ) D - σ := J ((σ, J) -D + )
It is clear that sequential L-nets and L-forests are one and the same thing. Notice that, by construction, both classes of L-nets hereditarily admit splitting.

Remark 7.1 1. We write i∈I ((ξ, I) • D ξi ) instead of (ξ, I) • ( i∈I D ξi ), because ( i∈I D ξi ) is not an L-net, according to our definition.

2. The production D + := E + . . . E + takes care of graphs which are not connected (i.e., that a re built using the MIX rule).

Relating sequential and parallel strategies

In this section, we study the relation between L-forests (sequential strategies) and parallel L-nets (parallel strategies). We have already proved (Proposition 5.1) that for every L S -net, seq D is an L-forest. Conversely, the following is an immediate consequence of the definition of parallel L-nets.

Proposition 8.1 For every L-forest Π, deseq Π is a parallel L-net.

Every time we desequentialize an L-forest Π, there is a sequentialization procedure seq such that seq (deseq Π) = Π. Theorem 8.2 Given an L-forest Π, there exists a strategy of sequentialization such that Π = seq (deseq Π).

Proof. We only consider the interesting cases.

D is negative. Let us denote by {x I , . . . } the conclusion of the tree. Since Π =

I (x I Π i ), its desequentialization is deseq Π = ↓ I (x I •deseq Π I ).
To sequentialize, we use scoping. By Lemma 4.19 (ii), Scope(x I , (deseq Π)) \ x I = deseq Π I . Hence

seq (deseq Π) = I (x I seq (deseq Π I )) . D is positive. If the root is x, Π = i (x.Π i ). Since deseq Π = i (x • deseq Π i ),
to sequentialize it we select x as splitting rule. Removing x gets us back to the set of all deseq Π i 's. Hence:

seq (deseq Π) = i (x • seq (deseq Π i )) .
Theorem 8.2 says that in the desequentialization there is no essential loss of information. All dependency (sequentialization) which is taken away can be restored.

Establishing a result in the opposite direction (i.e., deseq (seq D) = D) only makes sense starting from a parallel L-net, because as deseq Π reduces sequentiality to a "minimal" amount, if D is not parallel there is no hope that deseq (seq D) = D.

Theorem 8.3 If R is a parallel L-net, it admits a sequentialization procedure such that deseq (seq R) = R.
Proof. Following the destructors, we are guaranteed (i) to have splitting, and (ii) that when we use scoping, we are in the situation described by Lemma 4.19. We just spell out the definitions.

• If R is negative, we have R -= ↓ I (x I •R I ).
deseq (seq R -) = ↓ I (x I • (deseq (seq R I )))
follows

• If R is positive, assume R + = i (x • R i ) (all others cases are immediate).
By construction, x is a splitting positive rule, and we select it. We have that seq R = i (x • seq R i ). Hence we have:

deseq (seq R + ) = i (x • (deseq (seq R i ))) .
Corollary 8.4 (Completeness) An L S -net D is a parallel L-net if and only if there is an L-forest Π such that D = deseq Π. In particular, parallel L-nets are L S -nets.

Remark 8.5 The crucial point in the proof of Theorem 8.3 is that the following holds for a parallel L-net:

R -= ↓ I (x I • (Scope(x I , R) \ x I )) ,
i.e. we can decompose (or destruct) a negative parallel L-net (scoping) and then reconstruct it (rooting and additive union). This does not hold in general for an L S -net D.

Remark 8.6

We have omited decorations in this section for simplicity. To be perfectly rigorous, one should maintain decorations through all the sequentialization and desequentialization process. For example, the sequentialization of a well decorated L S -net is defined just as the sequentialization of an L S -net (the only difference concerns the base case, where the decorations are kept).

Proof.

The claim is true if Π consists of a single decorated action on Γ (Π is essentially reduced to an axiom).

Assume Π = i ((ξ, I) + • Π i ) is positive and has interface ξ, ∆. Each Π i is an L-forest of interface ξi ∆. For each i, any slice S i ⊆ deseq Π i uses all the addresses in ξi ∆. Hence i ((ξi) • deseq S i ) is a slice which uses all the addresses in ξ, ∆.

Assume Π = I ((ξ, I) -Π I ) is negative and has interface ξ ∆. By Lemma 9.2, T is a slice in ↓ I ((ξ, I) -• deseq Π I ) iff T is a slice of Φ((ξ, I) • deseq Π I ), for some I. Moreover, T I = T \ x I is a slice of deseq Π I .
Each Π I is an L-forest of interface ξ * I, ∆ (where ξ * I = {ξi, i ∈ I}). Hence T I uses all the addresses in such a interface, and we can obtain the slice T = (ξ, I) -• S I which uses all the addresses in ξ ∆. Finally, since T is obtained from T by adding some edges, this operation does not change the nodes, and hence does not change the set of used addresses. Proposition 9.7 If Π is a design, and if we choose a uniform decoration for Π, then deseq Π is S-connected.

Proof.

By assumption, Π is an S-connected L-forest.

Π is negative. By Lemma 9.2, S is a slice of deseq Π = I Φ(x I • deseq Π I ) iff S is a slice of Φ(x I • D I )
, for some I. We have that S I = S \ x I is a slice of deseq Π I . By hypothesis, S I is S-connected. Let x I = (ξ, I). By Lemma 9.6, in x I • S I there are some edges connecting x I to the nodes of S I , those using some ξi. We obtain S by adding some more edges.

We conclude by observing that (i) any choice of an edge entering x I leaves x I connected to a node of S I , (ii) any switching S of S restricted to S I is a switching of S I , and (iii) by hypothesis, any two nodes of S I are connected in S.

Π is positive. By Lemma 9.2, S is a slice of deseq Π = i (x • deseq Π i ) iff S = i (x • S i ), and S i is a slice of deseq Π i , for all i. By induction, all the S i 's are S-connected, and hence S is S-connected.

Discussion and further work

Graduating sequentiality. In our setting, if we have minimal sequentiality, we have "parallel" strategies. At the other extreme, if we have maximal sequentiality, we have designs. The tools we have defined allow us to vary between these extremes, and hence provide us with a framework in which we can graduate sequentiality.

We are currently investigating this gradient of sequentiality, in particular along the following two directions. (i) In this paper we saturate L-nets to maximal sequentiality. We are studying how to perform sequentialization gradually, by adding sequential edges progressively. (ii) We would like to have a more precise understanding of what it means to have maximal or minimal sequentiality, and to investigate the extent of our desequentialization.

Actually, we already have answers to both questions in the multiplicative case, but the extension to the additive case needs further investigation.

Proof-nets. If tree strategies can be seen as abstract sequent calculus derivations, Lnets correspond to abstract proof-nets. We are currently investigating a typed setting, which also means to define a new syntax for proof-nets.

The typed counter-part of L S -nets should be an extension of focusing proof-nets [START_REF] Andreoli | Focussing proof-net construction as a middleware paradigm[END_REF]. While previous work on focusing proof-nets was limited to multiplicative linear logic, our framework extends to additive connectives.

We expect also to study the gradient of sequentiality in a typed setting, and then, mirroring the treatment of strategies, we expect to be able to move from MALL proofnets to sequent calculus derivations in a continuum. More precisely, using the semantical experience, we treat the graphs as orders. Then, we vary the amount of sequentiality (order) on the graphs (proof-nets) from most parallel to most sequential, where the most-sequential proof-nets can be seen as sequent calculus derivations.

This setting would realize a goal which was first proposed by Girard. Preliminary steps in this direction have already produced an extremely simple new proof of sequentialization for multiplicative proof-nets [START_REF] Giamberardino | A jump from parallel to sequential proofs[END_REF].

Further questions. We have singled out two classes of L-nets, those of maximal sequentiality (which are idempotent with respect to seq ) and those of minimal sequentiality. Notice that while seq applies to arbitrary L-nets, here we have defined deseq only on trees. We expect to be able to define the desequentialization of arbitrary L-nets, by using the Splitting Lemma.

Moreover, we are able to give a direct characterization of L-forests, while we only have an inductive definition of parallel L-nets. Beside the problem of expressing minimal sequentiality, we also need to capture the fact that an L-net admits decomposition. The condition Acyclicity captures the L-nets which hereditarily admit splitting (i.e., positive decomposition). To describe the L-nets which hereditarily admit negative decomposition (scoping with good properties), we need some weak form of typing, such as the typing provided by an arena. We postpone the definition of such a setting to future work.

Equational theory, canonicity. An underlying idea, which needs further study, is that a parallel strategy has not only an interest as an "asynchronous" model of computation, but also could play the same role that proof-nets have in providing an equational theory for proofs.

We expect to be able to use the parallel L-nets as an equivalence class on L-forests, i.e.,

Π 1 ∼ = Π 2 ⇐⇒ deseq Π 1 = deseq Π 2 .
If we restrict to purely multiplicative L-nets, it is easy to show that given two parallel L-nets R 1 , R 2 (seq R 1 = seq R 2 ) =⇒ (R 1 = R 2 ) (canonicity). We do not know if this is true also in the additive case.

A Examples

A.1 Sequentialization

Let us consider the following L-net R:

ξ, {0} α, {0} α0, {0} ξ0, I ξ0, J α00, {1} α00, {2}
We have two negative rules ({(ξ0, I), (ξ0, J)} and {(α0, {0})}), and two positive conclusions, both splitting. To sequentialize, we choose one of them. If we choose (ξ, {0}), we obtain the two trees on the left-hand side of Figure 2, and then the design X. Instead, by choosing (α, {0}) we obtain the design A (on the r.h.s.).

A.2 Superposition

The superposition of two L-nets is their union as sets of chronicles. Let us see an example. Consider the two L-nets D 1 , D 2 in Figure 3. The superposition of D 1 and D 2 produces the L-net D = D 1 D 2 . In fact, the set of chronicles of D 1 is the set of chronicles defined by each of its nodes k, that is:

{ α,0 , α,0 α0,0
, (ξ0, I), (α00, {1}) = D 1 }.

The set of chronicles of D 2 is:

{ α,0 , α,0 α0,0
, (ξ0, J), (α00, {2}) = D 2 }.

The resulting union is:

{ α,0 , α,0 α0,0
, (ξ0, I), (ξ0, J), D 1 , D 2 }, which corresponds to D.

A.3 Desequentialization

Example 1. Desequentializing either of the designs A or X in our previous example A.1, equipped with the only possible uniform decoration, yields the original L-net R.

The only uniform decoration is, for both designs:

• link(α00, 1) = {ξ0 * I},

• link(α00, 2) = {ξ0 * J}.

Example 2. Let us consider the design in Figure 4, where we just omit an obvious negative action at the place of . . . . The only uniform decoration is:

• link(b) = {α001, ξ0 * I},
• link(c) = {α002, ξ0 * J}.

Following the desequentialization procedure, a few easy steps produce the two L-nets D 1 , D 2 , represented in Figure 5. Observe that we have a chronicle for each node; D 1 D 2 is equal to { (α, {0}) , (α0, {0}) }. We obtain D 1 by adding the relation (ξ0, I) ← (α00, {1}), and D 2 in a similar way. Remember that we do not explicitly write the (non transitive) edge ξ0 ←b. The union D 1 D 2 produces the L-net on the right-hand side of Figure 5.

A.4 A typed example: additives

The following (typical) example with additives illustrates the relation between tree strategies and (parallel) L-nets.

Assume we have derivations Π 1 , Π 2 , Π 3 , Π 4 of (respectively) A, C, A, D, B, C, B, D. In the sequent calculus (and in proof-nets with boxes [START_REF] Girard | Linear logic[END_REF]) there are two distinct ways to derive A&B, C&D, and the two derivations differ only by commutations of the rules. The same phenomenon can be reproduced in the setting of designs, or in the setting of polarized linear logic [START_REF] Laurent | Etude de la polarisation en logique[END_REF]. Very similar to the above derivations are the two following (typed) designs, where we introduce some ↓'s in order to fit into our polarized setting. We write formulas instead of addresses, to make the example easier to grasp.

↓A&B A&B,A ↓C&D C&D,C Π 1 C&D,D Π 2 A&B,B ↓C&D C&D,C Π 3 C&D,D Π 4 ↓C&D C&D,C ↓A&B A&B,A Π 1 A&B,B Π 3 C&D,D ↓A&B A&B,A Π 2 A&B,B Π 4
The desequentialization of either of the trees above is the following L S -net R:

↓ A&B ↓ C&D A&B, A A&B, B C&D, C C&D, D AC AD BC BD Π * 1 Π * 2 Π * 3 Π * 4
Conversely, when sequentializing R, we get either one or the other tree back, depending on whether we choose to start from A&B or from C&D. Notice that both A&B and C&D are splitting.

B Sequent calculus presentation of L-forests and decoration

In this section, we recall the sequent calculus for designs [START_REF] Girard | Locus solum[END_REF] (see also [START_REF] Curien | Introduction to linear logic and ludics, part II[END_REF]). We add a rule which corresponds to the MIX rule, and we examine the correspondence between such extended designs and L-forests. In this section, Π will range over sequent calculus proofs. This does not conflict with our use of Π to denote L-forests, since we show here in some detail that they are essentially one and the same thing.

Girard's original sequent calculus for designs is the following (an interface is called well-formed if it consists of pairwise disjoint addresses with respect to the prefix ordering):

Daimon: ( Λ well formed) Λ †
Positive rule (I ⊆ ω finite, one premise for each i ∈ I, all Λ i 's pairwise disjoint and included in Λ, ξ, Λ well formed):

• • • ξi Λ i • • • ξ, Λ (ξ, I) +
Negative rule (N ⊆ P f (ω) possibly infinite, one premise for each J ∈ N , all Λ J 's included in Λ, ξ Λ well formed):

• • • ξ * J, Λ J • • • ξ Λ {(ξ, J) -: J ∈ N }
xhere ξ * J stands for the set of the ξj's (j ∈ J).

We add the following rule (which is a type-free counterpart of the MIX rule from linear logic [START_REF] Girard | Linear logic[END_REF]):

MIX ( Λ 1 , . . . , Λ n well formed, all Λ m 's pairwise disjoint) Λ 1 . . . Λ n Λ 1 , . . . , Λ n MIX Remark B.1
The negative rule conveys some inherent weakening. Each action (ξ, J) - creates simultaneously all the addresses ξj (j ∈ J), which are recorded in the sequent, regardless of whether they will be used or not.

Applications of the rule Daimon yield positive leaves in a proof tree. We shall also consider as a positive leaf any proof tree of the following form:

. . . ξi Λ i ∅ . . . ξ, Λ (ξ, I) +
where all negative rules are applied with N empty. We shall write simply:

ξ, Λ (ξ, I) +

We now briefly review how we can translate (in this extended setting) a sequent calculus proof Π into an L-forest Π. The translation satisfies the following invariant. A proof of a sequent Λ translates to a forest whose roots (or conclusions) are on distinct addresses of Λ, and a proof of a sequent ξ Λ translates to a forest all of whose conclusions are of address ξ. The definition is by induction, according to the last rule of the proof. We use the syntax introduced in Section 7. We omit the (easy) proof that Π is an L-forest.

• Daimon. Then Π = †.

• (ξ, I) + . Then Π = i∈I ((ξ, I) + • Π i ), where the Π i 's are the proofs of the sequents ξi Λ i (i ∈ I). Note that Π is a tree.

• {(ξ, J) -: J ∈ N }. Then Π = J ((ξ, J) -Π J ), where the Π J 's are the proofs of the sequents ξ * J, Λ J .

• MIX. Then Π = m Π m , where the Π m 's are the proofs of the sequents Λ m 's.

It should be clear that the rules of Π (as defined in Section 3) correspond univoquely to the occurrences of rules in Π. By going from Π to Π, we have just forgotten all sequent informations except at the root. We now examine the converse direction, from L-forests to sequent calculus proofs.

Proposition B.2

The mapping Π → Π is onto. More precisely, for every L-forest D there exists a uniform sequent calculus proof Π such that D = Π, where a uniform proof is a proof in which the positive and negative rules are constrained as follows:

• • • ξi Λ i • • • ξ, i Λ i (ξ, I) + • • • ξ * J, Λ • • • ξ Λ {(ξ, J) -: J ∈ N }
i.e., we require that in the positive rule, no address is lost (Λ = i Λ i ), and, in the negative rule, all Λ J 's are chosen maximal (and equal to Λ).

Proof.

We have to extend the setting of [START_REF] Girard | Locus solum[END_REF] (see also [START_REF] Curien | Introduction to linear logic and ludics, part II[END_REF]) from designs to L-forests, and to make sure that the target is restricted to uniform proofs. Let D be an L-forest. There are four cases. In each case, we sketch how to (coinductively) generate the final rule of the proof (we give more details for the quite similar proof of Proposition B.4 (2) below).

Remark B.3 The uniform proof discipline described in the statement of Proposition B.2 corresponds to pushing weakening maximally to the leaves.

The assignment of a sequent calculus proof to an L-forest is non-deterministic, i.e., the map Π → Π is not injective. With decorations (cf. Section 6), we get a bijective correspondence. We recall (cf. Definitions 6.1, 6.4, and 9.4) that

• a decorated L-forest is an L-forest D in which all leaves k are equipped with a finite set link (k) of addresses (called the link set of k), in such a way that the conditions on L-nets hold with respect to all addresses (including those in the link sets);

• a well decorated L-net is a decorated L-net D such that all addresses of the interface, and all addresses generated by a negative action of D are used in D, i.e., appear as a label of the underlying L-net or in a link set;

• a uniformly decorated L-forest is a decorated L-forest D such that every (maximal) slice of D is well decorated.

Proposition B.4

1. Well decorated L-forests are in one-to-one correspondence with sequent calculus proofs subject to the restriction that in all applications of the positive rule (resp. negative rule) we have i∈I Λ i = Λ (resp. J∈N Λ J = Λ).

Uniformly decorated L-forests are in one-to-one correspondence with the proofs subject to the further restriction of uniformity (cf. Proposition B.2).

Proof.

1. The correspondence in one direction is obtained by adapting Π, as follows: for each leaf with conclusion Λ (resp.

ξ, Λ) obtained by an application of † (resp. (ξ, I) + ), the translation is now † (resp. (ξ, I) + ) with link ( †) = Λ (resp. link ((ξ, I) + ) = Λ). It is easily checked that the respective restrictions on the construction of proofs ensure that Π is a well decorated or a uniformly decorated L-forest.

Conversely, given a well decorated L-forest D, we associate (deterministically) a proof, as follows. An invariant of the construction is that the minimal addresses (in the prefix ordering) used in D form the final sequent of the associated proof D .

• D = i C i has several positive conclusions. Then we translate each of the trees C 1 , . . . , C n of D, yielding proofs of sequents Λ 1 , . . . , Λ n . By the invariant, we know that all addresses in Λ m are used in C i , and then by condition Additives we are sure that the Λ m 's are distinct. Therefore we can apply the MIX rule, and we define D as

C 1 . . . C n Λ 1 , . . . , Λ n MIX • D has conclusion k = † with link (k) = Λ. Then D is Λ †
• D has only one positive conclusion (ξ, I) + . If D is reduced to a leaf, then we proceed as in the previous case. If D = {j∈J} ((ξ, I) + • D j ), for some J ⊆ I, by the same reasoning as in the first case, we have that the D j 's are proofs of sequents Λ j , for paiwise disjoint Λ j 's. Then we define D as . . . D j . . . ξk ∅ . . .

Λ (ξ, I) +

where j (resp. k) ranges over J (resp. I \ J), and where Λ is the union of the Λ i 's.

• D = J ((ξ, J) D J ). By construction of the decoration, all addresses ξj (j ∈ J) are minimal in D J . By this remark, and applying induction, we get that D J is a proof of a sequent of the form ξ * J, Λ J . Then we define D as

. . . D J . . . ξ Λ {(ξ, J) -: J ∈ N }
where N = {J : (ξ, J) -is a root of D} and Λ is the union of the Λ J 's.

The final sequent of D is its interface, by the invariant of the translation, and by the initial construction of the decoration, that takes the basis of D into account.

It is straightforward to prove that this transformation is inverse to the transformation Π → Π.

2. This correspondence is simply obtained by restricting the correspondence to uniformly decorated L-nets and to uniform proofs.

Corollary B.5 Every L-forest can be uniformly decorated, and hence a fortiori well decorated.

Proof. To an L-forest D, we can associate a uniform proof by Proposition B.2, and then a uniform decoration, by Proposition B.4.

Remark B.6 Note that the bijective correspondences of Proposition B.4 induce a bijective correspondence between the link sets used in the decoration of an L-forest and the generalized axioms used in the corresponding sequent calculus proof.

C Proof of the Splitting Lemma

In this section, we prove Lemma 4.11, namely that every L S -net D has a splitting conclusion.

We recall from section 4.4 that a negative rule W = {. . . , w I , . . .} of an L-net D is called splitting if either it is conclusion of the L S -net (each w I is a root), or if deleting all the edges w I → w there is no more connection (i.e., no sequence of consecutive edges) between any of the w I 's and w, and that a positive conclusion of D is called splitting if all negative rules just above it are splitting.

If D is negative, then the Splitting Lemma holds vacuously. For positive D's, we first establish the following Negative Splitting Lemma.

Lemma C.1 (Negative Splitting Lemma) Every positive L S -net D which has a negative rule has a splitting negative rule among all the negative rules of level 1 (i.e., located just above a conclusion).

Our proof is an adaptation to our setting of the proof of the similar lemma in [START_REF] Hughes | Proof nets for unit-free multiplicativeadditive linear logic[END_REF]. A switching path x 0 . . . x n is called strong (and denoted x 0 ⇐ x n ) if either its last node is positive or if it ends upwards in the last node. Strong switching paths satisfy the following concatenation property: if γ 1 is a strong switching path and γ 2 is a switching path such that their concatenation γ 1 γ 2 is a rule path (cf. section 3.7), then γ 1 γ 2 is switching, and if moreover γ 2 is strong, then γ 1 γ 2 is strong.

Definition C.2 (Domination)

Given an L S -net D, a negative rule X and a finite set of nodes G, we say that G is an X-zone if for every z ∈ G there are nodes x ∈ X and x such that x ← x ⇐ z, where the path x ⇐ z is included in G. Given a node z of D, we say that X dominates z, denoted X D z (or simply X z), if there exists an X-zone G in D such that z ∈ G. We say that the zone G and the sequence x ← x ⇐ z witness X z.

The following statement lists some simple consequences of the definition of domination.

Lemma C.3

1. X-zones are closed under unions.

2. If X z is witnessed by a sequence x ← x ⇐ z, then X dominates every node of the path x ⇐ z.

If

x ← y for some x ∈ X, then X y.

4. Given a negative rule W , if X dominates a node w ∈ W then X dominates all w ∈ W .

5. If X y, and if y ← z, or if z ← y and z is not negative, then X z.

Proof. The first three parts of the statement are obvious. Let X w be witnessed by G and x ← x ⇐ w. By definition of strong, the path x ⇐ w terminates with k ← w. Then we obtain a strong path to any w ∈ W by just replacing the last edge with k ← w . It follows that G ∪ W is an X-zone, and therefore (∀ w ∈ W X w ).

We now prove the last assertion of the statement. Let G and x ← a ⇐ y be a witness of X y. If z does not belong to a rule that intersects the sequence a . . . y, then the sequence a . . . yz is a path, that is switching by the assumptions. Hence G ∪ {z} and x ← a ⇐ z are a witness for X z. If z intersects the sequence a . . . y, then we conclude using the second and fourth parts of the statement.

Thanks to Lemma C.3, we shall henceforth safely assume that X-zones are rulesaturated, i.e. are unions of rules.

The notion of domination extends to rules. Let W be a rule. We write W 1 W 2 if there exists w 2 ∈ W 2 such that W 1 w 2 (or, equivalently, if W 1 w 2 for all w 2 ∈ W 2 , by Lemma C.3). If X is not dominated, we say that it is free.

Proof. The proof is by contradiction. Let X be a negative rule that is neither free nor dominated by a free negative rule. We shall build an infinite sequence of rules X i which are all distinct, are all not free, and are such that . . . X i+1 X i . . . X 1 X 0 X , contradicting the finiteness of D. We take X 0 = X. By assumption, X 0 is not free. Suppose that we have constructed the sequence up to X i . We distinguish two cases:

1. If X i is not in a switching cycle, we choose any X i+1 such that X i+1 X i (this is possible since X i is not free by induction hypothesis). This X i+1 is fresh as otherwise we would have by transitivity X i X i , contradicting our assumption on X i , by Lemma C.7.

2. If X i is in a switching cycle, then by Lemma C.6 we can choose a rule X i+1 such that X i+1 intersects no switching cycle. This X i+1 is fresh as otherwise we would have by transitivity X i+1 X i+1 , and this contradicts our assumption about the choice of X i+1 , by Lemma C.7.

In both cases, we have constructed a fresh X i+1 such that X i+1 X i . Moreover, by transitivity, X i+1 X, from which it follows that X i+1 is not free.

Let X, Y be distinct negative rules.

• We write X ←→ Y if there is a switching path z 0 . . . z n (called witnessing path) such that x ← z 0 and z n → y, for some x ∈ X and y ∈ Y .

• We write X →← Y if X, Y belong to the same bipole, hence x → k and y → k, for some k and all x ∈ X and y ∈ Y .

Lemma C.9 If X, Y and Z are negative rules such that X = Y , X Z and Y Z, then X ←→ Y .

Proof. Consider x ← a z (for some x ∈ X and z ∈ Z). Let z be the first node on the path from a to z such that Y z (and hence y ← b ⇐ z for some y ∈ Y ). Then we get a path witnessing X ←→ Y by going from a to z and then from z to b. This sequence of nodes is a rule path since if it were not, there would be z 1 in the first portion and z 2 in the second portion belonging to the same rule, but we have that Y z implies Y z 2 which in turn implies Y z 1 , contradicting the minimality of z . It is switching since the path from b to z is strong.

Lemma C.10 If X is a free negative rule of D and does not split, then there exist free negative rules Y, Z of D such that X →← Y and X ←→ Z.

Proof. Let c be the node just below X. Since X does not split, for some x ∈ X we can form a cycle (in the ordinary sense of graph theory, i.e. without the disjoint rules assumption) xc . . . ax, without using any edge between c and X other than c ← x. Since X is free, c is a conclusion of the net, and the next node on the cycle must be some y such that c ← y. By construction, y belongs to a rule Y distinct from X, and thus we have X →← Y .

Next we observe that we cannot have X x, because X is free, and that X a because x ← a (since the only edge of D out of x is already used). Let b be the first node, following the cycle in the direction xc . . ., such that X b. The node z before b must be negative and we must have z ← b as otherwise we would have X z by Lemma C.3. Let Z be the rule to which z belongs. Then we have X ←→ Z . If Z is free, we can set Z = Z . If Z is not free, it dominates some free Z, by Proposition C.8, and we conclude by Lemma C.9 (since X {b}, and Z {b} by transitivity).

We are now able to prove the Negative Splitting Lemma for finite L S -nets, i.e. for L S -nets having finitely many nodes.

Proof (Negative Splitting Lemma, finite case). If the L S -net D has no splitting negative rules, then all its conclusions must be positive, and starting from a free negative rule X 0 (whose existence is guaranteed by Proposition C.8), and using again and again Lemma C.10, we can build an infinite sequence X 0 →← X 1 ←→ X 2 →← . . . where X i+1 is a free negative rule and X i+1 = X i , for all i. Since there are only finitely many free negative rules, we have X i = X j = X for some i < j. By the definition of the →← and ←→ relations, we can form a switching sequence of nodes starting in X i = X and ending in X j = X which is nondegenerate (i.e. of length at least 2) since X i = X i+1 . But this sequence is not guaranteed to be a rule path. To build a rule path, we take two nodes z 1 and z 2 at minimal distance in the sequence such that z 1 and z 2 belong to the same rule. Again, this distance is non-degenerate, as z 1 and z 2 cannot belong to the same path witnessing some X 2k+1 ←→ X 2k+2 (i ≤ 2k + 1 < j), and moreover, by the same reason, the path z 1 z 1 . . . z 2 z 2 from z 1 to z 2 must cross some X n . We distinguish two cases:

1. If z 1 ← z 1 or z 2 ← z 2 , say, z 1 ← z 1 , then we also have z 1 ← z 2 , and adding this (reversed) edge to the path from z 1 to z 2 yields a switching cycle. Then, by a (weakened form of) Lemma C.6, we obtain that X n is dominated.

2. If z 1 ← z 1 and z 2 ← z 2 , then we are in the situation of the (second part of the statement of) Lemma C.5, and we also obtain that X n is dominated.

We have reached a contradiction, since X n is free by construction.

The Negative Splitting Lemma holds actually for arbitrary L S -nets. The following definition and lemma ensure a finiteness condition, even if our L S -net D is infinite.

Definition C.11 Let D be an L S -net whose conclusions are all positive. We denote by Neg 1 (D) the set of negative rules that are just above a conclusion (i.e., the set of rules of level 1).

Lemma C.12

1. The set Neg 1 (D) is finite.

2. Every free (negative) rule is in Neg 1 (D).

only by not containing k. We are thus almost in the situation of Lemma 4.2, modulo straightforward adaptations. Let us look for example at the condition Additives: the path leading down from k 1 to w 1 (resp. from k 2 to w 2 ) does not go through k, and hence belongs to k 1 D (resp. k 2 D ), so condition Additives in D is inherited from condition Additives in D.

We have that size(D k ) < size(D), because every conclusion k of D k is a conclusion of D, and every negative rule of D k is a negative rule of D. Moreover, every free splitting negative rule of D k is a splitting negative rule of D: indeed, if D k splits into D k and D X , then D splits into (D k ∪ D X ) and D X . We are now ready to prove that D has a positive splitting conclusion, by induction on size(D):

• Base case. Obvious. Since one positive conlusion is a leaf, it is splitting vacuously.

•

Figure 1 :

 1 Figure 1: From focalized proofs to designs

+←

  a of opposite polarity, called the parent of a (this node c is uniquely determined by condtion Views). -If a ← b and if a is positive, then b must use an address generated by a. -If a is negative, it has at most one predecessor.

Lemma 4. 1 (

 1 Downward closure) Let D be an L-net. Assume G ⊆ D, and that G is downward closed (for any k ∈ G, if a ∈ D and a + ← k in D, then a ∈ G). G is a (possibly partial) L-net. If D satisfies condition Cycles, so does G. Proof. All properties are inherited from D. Any chronicle of G is also a chronicle of D. Let us check the preservation of conditions Additives and Cycles. If k 1 , k 2 are two distinct nodes in G on the same address, then condition Additives for D provides a pair of negative nodes w 1 , w 2 such that w i + ← k i , which (by downwards closure) belong to G.

Corollary 4. 2

 2 If D is an L S -net and K is a set of positive nodes of D, then the subgraph induced on {k ↓ : k ∈ K} is an L S -net.

Proposition 4. 7

 7 If two positive L S -nets are of the form k + • D 1 , k + • D 2 and are such that the sets of addresses used by D 1 and D 2 are disjoint, then

Lemma 4. 10 (

 10 Splitting Lemma) Every L S -net D has a splitting conclusion. In particular, if all the conclusions are positive (i.e., if D is positive), there is at least one positive splitting rule.The proof is given in Appendix C.Splitting. As a consequence of the Splitting Lemma, we have the following property. Proposition 4.11 (Splitting) Let D be an L S -net. If D is positive, then there exists a positive conclusion k = (ξ, I), which we call a splitting conclusion of D, such that D = ( i∈I (k • D ξi )) C . Moreover, 1. all D ξi 's and C are L S -nets, and 2. they do not share addresses. Proof. Let k = (ξ, I) be a splitting positive conclusion. By deleting k, the graph splits into several connected components. Let us indicate by D ξi the part of the graph which is connected to some nodes of address ξi, and let us indicate by C the rest of the graph. 1. It is immediate that each C and all G i 's are downward closed, and hence are L S -nets by Lemma 4.1. It follows readily that D ξi = G i \ k is an L S -net, for all i.

  Definition 4.12 (Root removal) Given an L-net D (of interface ξ ∆) with a negative unary conclusion {x} with x = (ξ, I), we indicate by D \ x the graph obtained from D by removing x.

Definition 4 .

 4 13 (Scoping) Let D be an L-net of negative conclusion X = {x I : I ∈ N }. For all I ∈ N , we define the scope of x I in D as follows: Scope(x I , D) = {c : c c , c ∈ D, c positive and x J ∈ c for all J ∈ N \ {I}} .

  or equivalently: Scope(x I , D) = {k ↓ : k positive and x J + ← k for all J ∈ N \ {I}} . By Lemma 4.1, if D is an L-net (resp. an L S -net), Scope(x I , D) ⊆ D is an L-net (resp. an L S -net). Definition 4.14 (Additive union) Let D I , D J , . . . be a set of L-nets which all have negative unary conclusions x I = (ξ, I), x J = (ξ, J), . . . on the same address ξ (with distinct I, J, . . .). Their additive union ↓ I D I is defined as ↓ I D I = I Φ(D I ) , where each Φ(D I ) is obtained from D I by minimally adding edges in such a way that x I + ← k (in Φ(D I ) for each positive node k ∈ D I such that k ∈ D J (for some J = I).

Lemma 4.16 1 .I

 1 The chronicles of Φ(D I ) can be partitioned into two disjoint sets: Φ(D I ) = C B I , where C = J D J = {c : c ∈ D J , for all J} B I = { k ∈ Φ(D I ) : x I + ← k} = {c ∈ Φ(D I ) : x I ∈ c} 2. If D = ↓ a chronicle c of Φ(D I ) does not belong to B I , then, by construction, no edge has been added, which implies both that c is a chronicle of D I and that it belongs to all D J 's (J = I). Thus Φ(D I ) = C ∪ B I . Moreover, if x I ∈ c, then c cannot belong to any D J (J = I), as this would entail x I ∈ D J , contradicting the assumption that D J has a unary conclusion. Hence the union is disjoint. 2. If D = ↓ I D I = I Φ(D I ), we can write D = I (C B I ) = C ( I B I ). Proposition 4.17 ↓ I D I is an L-net. Moreover the construction preserves condition Cycles. Proof. It is immediate that each Φ(D I ) is an L-net. All properties are inherited from D. As for condition Cycles, notice that all the newly added edges enter x I , and no switching path which uses the new edges to x I can continue to form a cycle. Hence all Φ(D I )'s are L S -nets. We are left to show (cf. Section 4.3) that ↓ I D I = J Φ(D J ) satisfies conditions Additives and Cycles. We just check condition Cycles. It is convenient to partition the nodes of ↓ I D I as in Lemma 4.16.

Lemma 4 .

 4 19 If D = ↓ J D J , then: 1. Scope(x I , D) = Φ(D I ). 2. Assume D I = x I • C I , or D I = x I C I . Then: Scope(x I , D) \ x I = C I .

Sequentialization procedure.

  The following procedure progressively transforms an L S -net D into an L-forest on the same interface as D. It works bottom-up and follows the paradigm of lazy, stream-like computation. The procedure is non-deterministic. In what follows, D = seq D should be read as: "D is a possible sequentialization of D". D is negative. Let X = {. . . , x I , . . . } be the unique negative conclusion of D. Let D I = Scope(x I , D) \ x I , for all I. Then: • seq D = I (x I seq D I ). D is positive. 1. Assume D is connected (in the ordinary graph-theoretic sense). If D consists of a single positive node, we are finished.

Remark 7. 2

 2 If D I , D J , . . . are L-forests, then • ↓ I D I = I D I , and • positive rooting behaves in a "boxing-like" fashion in x + • D - i .

  By definition of sequentialization, we have seq R = I (x I (Scope(x I , R) \ x I )) . But by Lemma, 4.19, we have Scope(x I , R) \ x I = R I . Hence we have in fact seq R = I (x I (seq R I ) , from which

  Figure 2:

  Figure 3:

  Figure 4:

  Figure 5:

  Induction case. Let k be a splitting positive conclusion of D k . If k = k, then it is also a splitting positive conclusion of D, since every negative rule just above k is splitting in D k , hence in D. If k = k, let Y be a negative rule just above k. If Y = X, it is splitting by construction; if Y = X, Y belongs to D k by construction, and hence Y is splitting in D k , and hence also in D, so that k is a positive splitting conclusion. This completes the proof.

L S -nets were called logical L-nets in[START_REF] Curien | L-nets, strategies and proof-nets[END_REF].

The shift operators have been introduced by Girard as part of the decomposition of the exponentials.

Thus L-nets stand here for the L-nets of[START_REF] Faggian | Ludics nets, a game model of concurrent interaction[END_REF] minus the Acyclicity condition.

If D is a leaf, then the associated proof is its interface.

If D is a positive L-forest with more than one root, then we transform each of the trees E j of D into a proof of Λ j , where each Λ j consists of the minimal addresses used in E j , and then we accommodate the constraint Λ = j Λ j by dispatching arbitrarily any ξ ∈ Λ \ ( i Λ i ) to exactly one of the Λ j 's, yielding suitable Λ j 's.

If D is positive and is a tree, then we proceed essentially as in the previous case.

If D is negative on interface ξ Λ, then it is easily seen that each ξ * J, Λ is an interface for the corresponding subtree of D, so that we can carry on the construction.

Acknowledgments. We would like to thank Olivier Laurent for numerous discussions on MALL proof-nets, and also Dominic Hughes and Rob van Glabbeek for fruitful exchanges on the technique of domination.

Restricting the picture to designs

As mentioned earlier (and as proved in Appendix B), L-forests correspond to designs with MIX. In this section, we show that we can get rid of this rule by (unsurprisingly) imposing an additional connectedness assumption on L S -nets.

Given an L-net D and a slice S ⊆ D, a switching graph of S is a subgraph obtained from S by choosing a single entering edge for each negative node, and deleting all the other ones. A slice is S-connected if all its switching graphs are connected. Finally, we call an L-net S-connected if all its maximal slices are.

An S-connected L-forest is obviously a tree, and in fact it is a design.

Lemma 9.1 An L-forest Π is S-connected iff it is a design (in the sense of [START_REF] Girard | Locus solum[END_REF]).

Sequentialization and desequentialization preserve S-connectedness, and hence by restriction to S-connected L S -nets our results specialize to designs, rather than arbitrary L-forests. We shall give details only for the desequentialization. The proofs concerning the sequentialization are similar and simpler. In order to restrict the converse transformation, we need a strengthening of Lemma 6.7. Definition 9.4 A uniformly decorated L-forest is an L-forest that is well decorated slicewise, i.e., each slice S uses all the addresses of the interface, and all the addresses generated by a negative action of S. Lemma 9.5 Every L-forest can be uniformly decorated.

Lemma 9.2 (Slices)

Proof. See Corollary B.5.

There is a bijective correspondence between uniformly decorated L-forests, and their sequent calculus representation (Proposition B.4).

Lemma 9.6 (Used addresses)

Let Π be a uniformly decorated L-forest on the interface Ξ ∆. If S is a maximal slice of the decorated L-net deseq Π, all the addresses of the interface are used in S.

Lemma C.4 Domination is transitive.

Proof. Assume X Y and Y Z, witnessed by (rule-saturated) G and x ← a ⇐ y, and by G and y ← b ⇐ z (z ∈ Z, y, y ∈ Y , x ∈ X). By Lemma C.3, we can assume y = y . It is enough to show that G ∪ G is an X-zone, and for this we only have to consider z ∈ G \ G, if any, witnessed by y ← b ⇐ z . Let z be the last node in the sequence y b . . . z which is in G, witnessed by x ← a ⇐ z . Then, concatenating with the rest of the sequence from (the successor of) z to z , we obtain a path (by construction, and because G is rule-saturated). This path is strong and switching because its constituents are. Proof. We prove the second part of the statement (the reasoning is the same for the first part). Let G 1 (resp. G 2 ) be the set of nodes on a path going up from w 1 to z 0 (resp. from w 2 to z n ). We shall show that G 1 ∪ G 2 ∪ C is a W -zone. That G 1 and G 2 are W -zones follows readily from Lemma C.3. Let z ∈ C. Because C is switching, we have either z 0 ⇐ z or z n ⇐ z. Suppose that we have, say, z 0 ⇐ z. Let z 1 be the first node on the way up from w 0 to z 0 that belongs to a rule intersecting z 0 ⇐ z at some z 2 . Then the sequence obtained by going up from w 1 to z 2 and then to z is witnessing W z.

Lemma C.6

Let D be a finite L S -net. If a rule X intersects a switching cycle, then X is dominated by an additive rule W which intersects no switching cycle.

Proof. We construct a sequence of negative rules W i as follows. We set X = W 0 . If W i intersects a switching cycle, then applying the condition Cycles gives us a rule W i+1 . We have W i+1 W i , by Lemma C.5. At each iteration the union of the cycles increases strictly, and hence by finiteness of D we eventually reach some negative rule W n = W which intersects no switching cycle. Moreover, we have W X by Lemma C.4.

Due to the finiteness condition in the previous lemma, we shall first establish the Splitting Lemma in the finite case, and then show how to lift the result also to infinite L S -nets.

Lemma C.7 If X X, then X is in a switching cycle.

Proof. If X X, we have x ← a ⇐ x for some x ∈ X. Then we can close the path from a to x with the edge x ← a. Because the path from a to x is strong, the cycle is switching.

Proposition C.8 Let D be a finite L S -net. Every negative rule is either free or dominated by a free negative rule. As a consequence, if there are negative rules, there exists a free negative rule.

Proof.

By the finiteness of the interface, there are finitely many conclusions, and since there are are only finitely many rules just above a positive rule, it follows that Neg 1 (D) is finite. Suppose that W is a rule of level > 1, then, going down from W , we reach a rule W that dominates W (that W W follows by repeated use of Lemma C.3). The second part of the statement follows.

Proof (Negative Splitting Lemma, infinite case). Let D be an infinite L S -net. We concentrate on Neg 1 (D). For each pair X, X ∈ Neg 1 (D) such that X X , we take an X-zone witnessing this domination. Let F be a minimal (finite) L S -net containing these zones, obtained by possibly adding in a minimal way positive chronicles to the set F of all chronicles k , where k ranges over the union of the zones (note that F is already a partial L-net by Lemma 4.1). By construction, Neg 1 (F) consists of all sets X ∩ F such that X ∈ Neg 1 (D) and X ∩ F = ∅. Moreover, for any two X, X ∈ Neg 1 (D), we have, by construction of F:

It follows that if (X ∩ F) ∈ Neg 1 (F) is free (in F), then X is free (in D), using the fact that whenever a rule is dominated, it is dominated by a rule in Neg 1 (D). Now, suppose that there exists a negative rule X of D that is neither free nor dominated by a free rule. We can assume X ∈ Neg 1 (D) since this property is a fortiori true of any negative rule below. Then, as we noted above, X ∩ F is not free. Neither can X ∩ F be dominated by a free rule X ∩ F, because then we would have that X is free and X D X. Therefore X ∩ F is neither free nor dominated by a free rule in F, contradicting the Negative Splitting Lemma (finite case).

We now prove the Splitting Lemma, as a consequence of the Negative Splitting Lemma.

Proof (Splitting Lemma). Let D be an L S -net that has only positive conclusions. We define size(D) as:

• 0 if at least one of the positive conclusions of D is a leaf, and otherwise as • the cardinal of the set of level 1 negative rules of D.

Since D has finitely many positive conclusions, the size of D is finite, even if D is not finite.

We apply the Negative Splitting Lemma to D. We select a splitting negative rule X. Since D has no negative conclusion, X is just above a conclusion k of D. We delete the edges from x to k, for all x ∈ X.

Let us call D X the union of the connected components (in the ordinary unoriented graph-theoretic sense) of the elements of X, and D k the rest of the graph, which contains k. We prove that D X and D k are L S -nets. Let D stand for either D X or D k . We note that if c ∈ D , then D contains every path of D starting from c that does not go through one of the deleted edges. It follows that c D possibly differs from c D