Paolo Di Giamberardino
email: digiambe@lipn.univ-paris13.fr

Jump from Parallel to Sequential Proofs: Additives

we introduced a framework for proof nets of the multiplicative fragment of Linear Logic, where partially sequentialized nets are allowed.

In this paper we extend this result to include additives, using a definition of proof net, called J-proof net, which corresponds to a typed version of an L-net of Faggian and Maurel.

In J-proof nets, sequentiality constraints are represented using the proof-net notion of jumps; by gradual insertion or removal of jumps then it is possible to characterize nets with different degrees of sequentiality. As a byproduct, we obtain then a proof of the sequentialization theorem.

Moreover, we provide a denotational model for J-proof nets which is an extension of the relational one, and we show that the "degree" of sequentiality of a J-proof net can be read-off from its semantics, by proving that the model is injective with respect to J-proof nets.

Introduction

Game models of computation interpret a program as a strategy in a game: usually such strategies appear as trees, (for instance, innocent Hyland-Ong strategies, see [START_REF] Hyland | On full abstraction for PCF: I, II, and III[END_REF]), and composition between strategies yields a linearly ordered set of moves, which somehow describes the "trace" of the computation. Using tree strategies, it has been possible to solve the outstanding open problem of providing a fully abstract model of PCF, a paradigmatic sequential programming language based on λ-calculus ([HO00], [START_REF] Abramsky | Full abstraction for PCF[END_REF]).

Several proposals have been made (see among others [START_REF] Hyland | Games on graphs and sequentially realizable functionals[END_REF][START_REF] Abramski | Concurrent games and full completeness[END_REF][START_REF] Melliès | Asynchronous games 2 : The true concurrency of innocence[END_REF]) in order to extend game semantics to represent more parallel forms of computation; in these approaches, strategies are no more trees, but more generally graphs, so that the order between the actions is not completely specified: the composition between graph strategies yields a partially ordered set of moves.

Recently, in the context of ludics (a game model based on linear logic, introduced by Girard in [START_REF] Girard | Locus solum: from the rules of logic to the logic of rules[END_REF]), a parallel generalization of ludics strategies called L-nets was proposed by Faggian and Maurel [START_REF] Faggian | Ludics nets, a game model of concurrent interaction[END_REF]. A design (i.e. a ludics strategy) can be thought of as a merging of two kinds of orders between actions, as pointed out by Faggian in [START_REF] Faggian | Travelling on designs: ludics dynamics[END_REF]:

-the causal (or spatial ) order, representing the causal dependencies between actions; -the sequential (or temporal ) order, representing how causally independent actions are scheduled. L-nets are built from standard designs by relaxing the sequential order between actions, in such a way to have still enough information to compute; a characteristic feature of this approach is to provide an homogeneous space of strategies with different levels of sequentiality, depending on the amount of sequential order they contain. Such a space has as extremes from one side parallel L-nets (with minimal sequentiality), from the other sequential L-nets (which correspond to designs, see [START_REF] Curien | L-nets, strategies and proof-nets[END_REF]); by the way, designs are a special case of L-nets, as trees are a special case of graphs.

The definition of L-nets is directly inspired from the one of proof net ( a graph representation of linear logic proofs introduced by Girard in [START_REF] Girard | Linear logic[END_REF]); actually we could think of L-nets as a sort of abstract, untyped proof nets.

In [START_REF] Curien | L-nets, strategies and proof-nets[END_REF] Faggian and Curien analyzed the relation between parallel and sequential L-nets using specific techniques coming from the framework of proof nets (namely sequentialization, desequenzialization, splitting theorems, and so on); in particular, they showed how to turn a graph strategy (L-net) into a tree strategy (design) by introducing a maximal amount of sequential order, and viceversa. Nevertheless, in the conclusions of the paper the following questions were still open :

• What is the notion of proof net underlying the one of L-net?

• Is it possible to turn gradually an L-net into a design, by introducing sequential order little by little (that is to move from graph strategies to tree strategies in a continuum) ?

The first motivation of the present paper is to provide answers for the questions above by introducing a new kind of proof nets called J-proof nets, which are the typed, logical counterpart of L-nets. By the insertion of special edges called jumps, representing sequentiality constraints, we can gradually increase the amount of sequential order on a J-proof net; in this way as in L-nets, we can characterize J-proof nets with different degrees of sequentiality.

A second, more general motivation behind the introduction of J-proof nets lies in the attempt to reconcile two different notions of canonical representation of proofs provided by linear logic, namely that of proof net and the one of focusing proof, as we point out in the following paragraphs.

Proof nets. In 1987, in the seminal paper [START_REF] Girard | Linear logic[END_REF], Girard introduces linear logic (briefly LL) from a fine analysis of intuitionistic and classical logic; such a refinement provides a logical status to the structural rules (weakening and contraction) of sequent calculus (due to the introduction of the exponential connectives, ! and ? ) and splits the usual propositional connectives ("and ", "or ") in two classes (the additives &, ⊕, and the multiplicatives ⊗, ).

The deep insight on the standard connectives operated by LL allows to represent proofs as graphs called proof nets, whose nodes correspond to linear logic rules and which satisfy some specific geometrical properties (called correctness criteria); such a discovery brought to the fore the geometrical nature of proofs.

The main characteristic of proof nets is to be modular, parallel objects: in a proof net, there is no direct reference to the sequential succession of steps which brought to its construction.

As a consequence, a proof net turns out to be a canonical representative of a class of sequent calculus proofs equivalent modulo permutations of rules: sequentialization, one of the key results in the theory of proof nets, allows to recover a sequent calculus proof from a proof net, by proving that among the nodes of the proof net one can be chosen as a sequent calculus last rule; by iterated application of this property, it is possible to retrieve a proof in sequent calculus.

We must remark that outside multiplicative linear logic (briefly M LL), the beautiful theory of proof nets becomes less elegant and (in some cases) quite complicated: for instance, the search of a proper representation of additives in proof nets has been an open problem for a long time, only recently solved by Hughes and Van Glaabeek in [START_REF] Hughes | Proof nets for unit-free multiplicative-additive linear logic[END_REF].

Nevertheless, proof nets allows to eliminate those naive aspects of sequentiality which are not naturally inherent to the structure of proofs.

However there exists also another side of sequentiality, more intrinsic than the simple ordered succession of rules. Such a meaningful notion of sequentiality has been disclosed by the discovery inside linear logic of polarities.

Polarities. LL, tampering the structural rules with the exponential connectives, allows for the first time to define an involutive negation independent from structural rules, called linear negation.

Such a discovery enlightened the operational meaning of negation as a change of viewpoint. In computer science, a program is executed in a given environment; this process can be either analyzed from the point of view of the program or from the one of the environment, and negation is here the switch between these two positions.

It is worth mentioning that the above intuition contributed in a remarkable way to the birth of game semantics, which interprets computation as a game between two players, one representing the program, and the other representing the environment (see [START_REF] Abramsky | Full abstraction for PCF[END_REF], [START_REF] Hyland | On full abstraction for PCF: I, II, and III[END_REF]).

The refinement of usual negation inside LL was the starting point of a deep analysis of the logical notion of duality, which eventually brought to the discovery of polarities.

Multiplicative and additive connectives of LL naturally splits into two dual families:

-Positives (or synchronous): ⊗, ⊕; -Negatives (or asynchronous): , &.

A formula is positive (resp. negative) if its outermost connective is positive (resp. negative).

The difference between positive and negative formulas relies in the fact that, while the rules introducing negative formulas are reversible (that is, the conclusion of the rule implies the premises), the rules introducing positive formulas are irreversible.

Following this distinction, in [START_REF] Andreoli | Logic programming with focusing proofs in linear logic[END_REF], Andreoli proved that any proof of linear logic can be transformed modulo permutations of rules into a proof which satisfies (bottom-up) the following discipline: i) negative formulas, if any, are decomposed immediately;

ii) otherwise, one chooses a positive formula, and keeps decomposing it up to its negative subformulas. Such proofs are called focusing.

The alternation of positive and negative steps provides then a canonical way to construct a sequent calculus proof, yielding an intrinsic, non-trivial notion of time in proofs, as pointed out by Girard in [START_REF] Girard | On the meaning of logical rules. I: Syntax versus semantics[END_REF].

Looking at focusing proofs through the lens of interaction, a positive cluster of rules appears as the act of posing a question to an Opponent by a Proponent, and a negative cluster of rules as the reception of an answer from the Opponent; if we apply linear negation, we switch the point of view, turning questions into answers and answers into questions.

To provide a canonical representation of focusing proofs in multiplicative-additive linear logic (briefly M ALL), in [START_REF] Girard | On the meaning of logical rules II: multiplicative/additive case[END_REF] Girard introduced a calculus called hypersequentialized calculus (briefly HS), using synthetic connectives, that is considering clusters of connectives of the same polarity as a single connective. The distinctive feature of HS is the presence of only two kinds of logical rules (the positive rule and the negative rule), one strictly alternating with the other.

Nevertheless, the hypersequentialized approach too has its limitations: mainly, it forces to leave aside the geometrical representation of proof nets, in spite of the simplicity and elegance of its multiplicative part.

Jumps: sequentializing à la carte. Clearly there is a mismatch regarding the nature of proofs between proof nets and hypersequentialized calculus. Firstly, proof nets exhibit an elegant geometrical structure which is absent in HS; furthermore, while proof nets are timeless, parallel objects, in hypersequentialized proofs there is an explicit marking of time, which makes them sequential in a strong, natural sense.

The spirit behind the present work is to try to reconcile this mismatch, by proposing a notion of proof net compatible with HS and recovering in this way polarities (and time) in a geometrical, parallel setting: here is where L-nets come into the picture.

It is well known that a design in ludics corresponds to an abstract, untyped hypersequentialized proof. What we would like to achieve is a notion of proof net which corresponds to the one of L-net, as an hypersequentialized proof corresponds to a design. In order to accomplish this task, we must find a counterpart for both the causal and the sequential ordering in the representation of proof nets. Concerning the causal ordering, if we restrict to M ALL, we have already an answer in the subformula relation induced by the structure of the links in a proof net. To properly characterize sequential order in proof nets, we have to resort to the notion of jump (as observed in [START_REF] Faggian | Ludics nets, a game model of concurrent interaction[END_REF]).

The idea of using edges to represent sequentiality constraints has been widely used in the study of correctness criteria for proof nets: in [START_REF] Girard | Quantifiers in linear logic II. Nuovi problemi della Logica e della Filosofia della scienza[END_REF] and [START_REF] Girard | Proof-nets : the parallel syntax for proof-theory[END_REF], Girard, as a part of the correctness criterion for proof nets, introduces jumps: if a link n is a , &, ⊥ or ∀ link, a jump is an untyped edge between n and another link m, which represents a sequential ordering between n and m; n precedes m (bottom-up) in every sequentialization.

Girard, in several occasions, suggested that it could be possible to retrieve a sequent calculus proof from a proof net just by fixing some temporal information on it, using jumps.

Let us try to make this point clearer with an example; consider the sketch of proof net below:

Ax Ax

⊗ ⊗

We remark that such a configuration is forbidden in sequent calculus: one must decide which one of the two ⊗ is the last rule. To retrieve a proof then we draw a jump between the leftmost (negative) and the rightmost (positive) ⊗, meaning that the corresponding rule must precede (bottom-up) the corresponding ⊗ rule in the sequentialization;

Ax Ax

⊗ ⊗

Now, the sequent calculus proof π induced by this proof net will have as last rule the leftmost ⊗, followed respectively by the leftmost , the rightmost ⊗ and the rightmost ; we stress that such a proof respects the focusing discipline. Instead of fixing the order in the way above, we could as well draw a jump between the the rightmost (negative) and the leftmost (positive) ⊗, as below, obtaining a different focusing proof π ′ : Ax Ax

⊗ ⊗

Furthermore, once fixed an order between links using jumps, some other choices become unavailable: namely one cannot draw both the jumps above at the same time, without creating a cycle, which would prevent us to obtain an order on the rules.

Ax Ax

⊗ ⊗

Once all possible jumps have been chosen, one directly retrieves in this way a focusing proof.

In previous work [START_REF] Di | Jump from parallel to sequential proof: multiplicatives[END_REF][START_REF] Di | Proof nets sequentialisation in multiplicative linear logic[END_REF], realizing the proposal put forward by Girard, we provided a simple proof of sequentialization theorem for the multiplicative fragment of Linear Logic; we proved that by gradual insertion of jumps in a proof net, one increases step by step sequentiality information, until one directly retrieves a sequent calculus proof. Our proof relied on a technical result, that we called arborisation lemma, which provides a way to insert edges into a directed acyclic graph G, preserving a geometrical property called switching acyclicity (which corresponds to the correctness criterion of proof nets) and increasing at the same time the order induced by G.

J-proof nets. Building up on such previous results, in the present work :

• we introduce proof nets with jumps for the hypersequentialized calculus, called J-proof nets, by translating L-nets to a typed setting: the basic idea is to use jumps to represent sequential order;

• we extend the sequentialization method used in [START_REF] Di | Jump from parallel to sequential proof: multiplicatives[END_REF][START_REF] Di | Proof nets sequentialisation in multiplicative linear logic[END_REF] for the multiplicative fragment in order to take into account additives, and we show that we can gradually remove or add sequentiality in a J-proof net, in the form of jumps, to get more parallel or more sequential proofs, in the style of L-nets. At any time, the information provided by jumps always makes possible to retrieve a fully sequentialized J-proof net, which directly corresponds to an hypersequentialized proof.

In this way, as in L-nets, we get an homogeneous space of J-proof nets with different degrees of sequentiality, having as extremes from one side J-proof nets with minimal sequentiality, from the other J-proof nets with maximal sequentiality, that is HS proofs; moreover, adding jumps provides a way to move in a continuum from one extreme to the other.

Outline of the paper

First, in section 2 we provide some background. We present the hypersequentialised calculus , together with an informal introduction to two important notions to understand additive connectives: the one of slice (see [START_REF] Girard | Linear logic[END_REF]) and the one of superposition. Then we recall some graph theoretical definitions that we will use throughout the paper.

In section 3 we introduce our main objects of study: J-proof nets. As usual in proof nets theory, we first define a general class of graphs, called J-proof structures, and then we isolate among them the ones coming from HS, called J-proof nets, using a correctness criterion.

In section 4 we provide a formal definition in our setting of the "superposition" effect induced by additives, using the key notion of sharing equivalence; to define such equivalence we will import concepts and tools from the setting of ludics and L-nets, establishing in this way a direct connection between the two frameworks.

Section 5 is dedicated to the proof of the sequentialization theorem. We extend the sequentialization method used in [START_REF] Di | Jump from parallel to sequential proof: multiplicatives[END_REF] to include additives; the relevance of this result is clear, if one consider that the problem of sequentializing in presence of additives is one of the most difficult in the framework of proof nets.

In section 6 we introduce and study the dynamics of cut reduction. In subsection 6.2 we define cut-elimination on J-proof structures, following [START_REF] Faggian | Ludics nets, a game model of concurrent interaction[END_REF] and [START_REF] Laurent | Slicing polarized additive normalization[END_REF]). In subsection 6.3 using pointed sets, we define a model of cut-reduction in J-proof nets, called pointed semantics, which extends usual relational semantics: differently from the standard relational model, pointed sets allow in fact to semantically characterize jumps. In subsection 6.3.2 we show that pointed semantics is a faithful description of J-proof nets, by proving that the model is injective with respect to J-proof nets: namely, two J-proof nets with the same interpretation in pointed semantics are syntactically equivalent.

Then in section 6.4, using injectivity of pointed semantics, we will prove that composition of J-proof nets is stable under cut reduction (a similar strategy was used also by Laurent and Tortora de Falco in [START_REF] Laurent | Slicing polarized additive normalization[END_REF]). The use of semantics to prove a syntactical property should not be surprising; in the spirit of the program launched in [START_REF] Girard | On the meaning of logical rules. I: Syntax versus semantics[END_REF] by Girard, syntax and semantics are just two different ways to describe the same object.

Finally, in section 7 we adress some general questions concerning J-proof nets; namely, the problem of canonicity (which was first posed in the setting of L-nets by Faggian and Curien in [CF]), the relation with monomial proof nets (see [START_REF] Girard | Proof-nets : the parallel syntax for proof-theory[END_REF], [START_REF] Hughes | Proof nets for unit-free multiplicative-additive linear logic[END_REF]) and the link with multifocalization (see [START_REF] Chaudhuri | Canonical sequent proofs via multi-focusing[END_REF]).

Background

In this section we introduce the principal notions and concepts we will use throughout the paper. In subsection 2.1 after an informal introduction of synthetic formulas, we define the hypersequentialized calculus; then we introduce the reader to the notions of slices and superposition, absolutely necessary to understand additives. In subsection 2.2 we recall basic concepts of graph theory. Finally in subsection 2.3 we provide some indications on how to represent hypersequentialized proofs as graphs.

Hypersequentialized calculus

From M ALL to HS

Let us consider the grammar of M ALL without atoms, and additive costants:

F := 1 | ⊥ | F F | F ⊗ F | F &F | F ⊕ F
Starting from this grammar, we define the notion of synthetic formula as a sort of "canonical representative" of the formulas of M ALL equivalent modulo the usual associative, distributive and neutral element properties of linear logic connectives.

Let us give an informal sketch of how to build a synthetic formula . Let us consider the following formula:

A = (1&1) (1&1)
First of all, we apply to A the distributivity property (B&C) D ⋍ (B D)&(C D) using it as a rewriting rule oriented from left to right. We obtain as "normal form" the formula A ′ :

A ′ = ((1 1)&(1 1))&((1 1)&(1 1))
Now let us look at the subformula tree t of A ′ :

((1 1)&(1 1))&((1 1)&(1 1)) (1 1) (1 1)&(1 1) 1 1 (1 1) (1 1)&(1 1) (1 1) (1 1) 1 1 1 1 1 1
The tree t is composed bottom-up by two layers: a first layer of negative formulas, and then a set of positive formulas, which are the leaves of the tree. The negative layer is itself divided in two layers: first a set formulas whose outermost connective is & (its "additive" sub-layer), and then a set of formulas whose outermost connective is (its "multiplicative" sub-layer).

The negative layer of connectives in t can be represented by a single "big step" negative connective, as follows.

Let us assign to every positive leaf an integer index as a place marker, in the following way:

1 2 3 4 5 6 7 8 ((1 1)&(1 1))&((1 1)&(1 1)) (1 1) (1 1)&(1 1) 1 1 (1 1) (1 1)&(1 1) (1 1) (1 1) 1 1 1 1 1 1
Let us consider the maximal subtrees of t having a formula as root (we can call them -trees); there are four of them in t. We can partition the leaves of t by grouping together the leaves belonging to the same -tree.

We call a set I of indexes of leaves belonging to the same -tree a ramification of t; we call directory the set N of all ramifications I of t. In our case, the directory of t contains the following ramifications: {1, 2}, {3, 4}, {5, 6}, {7, 8}. Now, it is easy to verify that if we replace t with any other subformula tree t ′ equivalent to t modulo associativity and neutral elements, the directories of t and t ′ will be the same.

The information provided by the directory N is enough to retrieve all the formulas whose subformula tree is equivalent to t modulo the usual isomorphisms of linear connectives. Now if we want to rewrite the formula retaining only the information provided by the directory N we would obtain something like this:

&( (1 1 , 1 2 ), (1 3 , 1 4 ), (1 5 , 1 6 ), (1 7 , 1 8 ))
We call such an object a synthetic formula; we stress that the possibility of defining such a formula depends strictly from the fact that rewriting a formula, using the associative, distributive and neutral element property of LL, preserves the polarity of the formula.

Due to the focalization property (see the introduction of the paper) then it is possible to define a linear logic calculus manipulating only synthetic formulas. We call such a calculus hypersequentialized calculus.

HS syntax

The grammar of hypersequentialized formulas is the following:

N ::= & I∈N ( i∈I (P i )) P ::= ⊕ I∈N (⊗ i∈I (N i ))
where

• there are two kinds of formulas: N formulas are negative while P formulas are positive;

• I is a ramification (that is an index set) and N is a non-empty 1 directory (that is, a set of ramifications).

Duality is defined as follows:

(⊕ I∈N (⊗ i∈I (A i ))) ⊥ = & I∈N ( i∈I (A ⊥ i )) (& I∈N ( i∈I (A i ))) ⊥ = ⊕ I∈N (⊗ i∈I (A ⊥ i )) P ⊥⊥ = P
1 For technical reasons we do not consider the additive constants ⊤ and 0

Note We remark the following facts:

• By & I∈N ( i∈I (P i )) we indicate the synthetic formula which represents all possible combinations of the formulas P i (where i is an element of the ramification I belonging to the directory N ) modulo the associativity and distributivity properties of usual and & connectives in LL, and neutral element property of connective of LL; in case the directory N is a singleton, we shall use the abbreviation ( i∈I (P i )); if for some I ∈ N , I is a singleton or is empty, then we will denote the component ( i∈I (P i )) corresponding to I as ↑ P in the former case, and as ⊥ in the latter.

• By ⊕ I∈N (⊗ i∈I (N i )) we indicate the synthetic formula which represents all possible combinations of the formulas N i (where i is an element of the ramification I belonging to the directory N ) modulo the associativity and distributivity of usual ⊗ and ⊕ connectives in LL, and neutral element property of ⊗ connective of LL; in case the directory N is a singleton, we shall use the abbreviation (⊗ i∈I (N i )); if for some I ∈ N , I is a singleton or is empty, then we will denote the component (⊗ i∈I (N i )) corresponding to I as ↓ N in the former case, and as 1 in the latter.

Note that ↑ and ↓ are "linear" versions of the exponentials ?, !, acting as polarity inverter (see [START_REF] Laurent | Polarized games[END_REF], [START_REF] Girard | Locus solum: from the rules of logic to the logic of rules[END_REF]). Moreover, for technical reasons we must forbid the presence of more than one empty ramification I in a directory N ; this will prevent us from representing, for example the formula 1 ⊕ 1.

The HS (+ Mix) calculus is the following:

⊢ Γ 1 , N 1 . . . ⊢ Γ n , N n (+,I) ⊢ Γ 1 , . . . , Γ n , ⊕ J∈N (⊗ j∈J N j ) ⊢ Γ, P 1 1 . . . , P k1 1 . . . ⊢ Γ, P 1 n . . . , P kn n (-,N ) ⊢ Γ, & J∈N ( j∈J P j ) ⊢ Γ ⊢ ∆ mix ⊢ Γ, ∆ ⊢ Γ, P ⊢ ∆, P ⊥ cut ⊢ Γ, ∆
where:

• in the (+, I) rule the cardinality of I is n;

• in the (-, N ) rule the cardinality of N is n, with n = 0, and the cardinality of J is k i for J ∈ N and i ∈ {1, . . . , n}

• Γ, ∆, . . . only contain positive formulas.

Additives and superposition Before presenting J-proof nets, we want to give a first intuition about two fundamental notions which naturally come out whenever a linear logic calculus includes additives: the one of slice and the one of superposition.

Let us consider the following sequent proof

π of ⊢ ⊕(⊗(⊥ 1 , ⊥ 2 ), ⊗(⊥ 3 , ⊥ 4 )), &( (1 1 , 1 2 ), (1 3 , 1 4 )): (+,{}) ⊢ 1 (-,{}) ⊢ 1, ⊥ (+,{}) ⊢ 1 (-,{}) ⊢ 1, ⊥ (+,{1,2}) ⊢ ⊕(⊗(⊥ 1 , ⊥ 2 ), ⊗(⊥ 3 , ⊥ 4 )), 1, 1 (+,{}) ⊢ 1 (-,{}) ⊢ 1, ⊥ (+,{}) ⊢ 1 (-,{}) ⊢ 1, ⊥ (+,{3,4}) ⊢ ⊕(⊗(⊥ 1 , ⊥ 2 ), ⊗(⊥ 3 , ⊥ 4 )), 1, 1 (-,{{1,2},{3,4}}) ⊢ ⊕(⊗(⊥ 1 , ⊥ 2 ), ⊗(⊥ 3 , ⊥ 4 )), &( (1 1 , 1 2 ), (1 3 , 1 4 ))
Now, we choose a branch for each (-, N ) rule, (in this case just one); by erasing the right branch we get the following derivation s 1 :

(+,{}) ⊢ 1 (-,{}) ⊢ 1, ⊥ (+,{}) ⊢ 1 (-,{}) ⊢ 1, ⊥ (+,{1,2}) ⊢ ⊕(⊗(⊥ 1 , ⊥ 2 ), ⊗(⊥ 3 , ⊥ 4 )), 1, 1 (-,{{1,2},{3,4}}) ⊢ ⊕(⊗(⊥ 1 , ⊥ 2 ), ⊗(⊥ 3 , ⊥ 4 )), &( (1 1 , 1 2 ), (1 3 , 1 4 ))
and by erasing the left branch, we get the following derivation s 2 :

(+,{}) ⊢ 1 (-,{}) ⊢ 1, ⊥ (+,{}) ⊢ 1 (-,{}) ⊢ 1, ⊥ ⊢ 1, ⊥ (+,{3,4}) ⊢ ⊕(⊗(⊥ 1 , ⊥ 2 ), ⊗(⊥ 3 , ⊥ 4 )), 1, 1 (-,{{1,2},{3,4}}) ⊢ ⊕(⊗(⊥ 1 , ⊥ 2 ), ⊗(⊥ 3 , ⊥ 4 )), &( (1 1 , 1 2 ), (1 3 , 1 4 ))
In both s 1 and s 2 the (-, N )-rule is unary (the "additive" part is erased and only the "multiplicative" part is kept).

Following this observation, a (-, N )-rule appears as a set (superposition) of unary rules having the same active formulas. If we consider a sequent calculus derivation in HS, and for each (-, N )-rule we select one of the premises, we obtain a derivation where all (-, N )-rules contain a single ramification; actually we "forget" the additive structure of the proof, keeping only the multiplicative one. This is called a slice. Hence, an HS proof containing some (-, N )-rule can be thought of as a superposition of multiplicative proofs (that is, slices).

Actually, the notion of slice is as old as Linear Logic itself: it appears for the first time in the seminal paper [START_REF] Girard | Linear logic[END_REF]; it has been used by Laurent and Tortora de Falco for studying normalization on polarized proof nets (see [START_REF] Laurent | Slicing polarized additive normalization[END_REF]) and is a key notion of ludics and L-nets.

The main point when one deals with additive proof nets is to properly reconstruct the structure of the multiplicative proofs an additive proof is composed of, and to correctly superpose them; such a task is usually fulfilled by boxes (as in [START_REF] Girard | Linear logic[END_REF], [START_REF] Laurent | Slicing polarized additive normalization[END_REF], [START_REF] Tortora De Falco | The additive multiboxes[END_REF]) or by boolean weights (as in [START_REF] Girard | Proof-nets : the parallel syntax for proof-theory[END_REF], [START_REF] Laurent | Polarized proof-nets: proof-nets for LC (extended abstract)[END_REF], [START_REF] Maieli | Retractile proof nets of the purely multiplicative and additive fragment of linear logic[END_REF]), which provide enough "synchronization points" to glue slices together. As we will see later, in additive J-proof nets it is possible to glue together slices due to the presence of jumps, acting as synchronization points.

Preliminaries on graphs

A directed graph G is an ordered pair (V, E), where V is a finite set whose elements are called nodes, and E is a set of ordered pairs of nodes called edges.

We will denote nodes by small initial Latin letters a, b, c, . . . and edges by small final Latin letters . . . , x, y, z.

To denote that there is an edge from a node a to a node b, we will write a → b; we say that an edge x from a to b is emergent from a and incident on b; b is called the target of x and a is called the source.

The in-degree (resp. out-degree) of a node is the number of its incident (resp. emergent) edges; two edges are coincident when they have the same target.

Given a directed graph G = (V, E) and a subset V ′ of V , the restriction of G to V ′ is the graph G ′ = (V ′ , E ′ ) where E ′ is the restriction of E to the elements of V ′ .

Given a directed graph G a path (resp. directed path) r from a node b to a node c is a sequence a 1 , . . . , a n of nodes such that b = a 1 , c = a n , and for each a i , a i+1 , there is an edge x either from a i to a i+1 , either from a i+1 to a i (resp. from a i to a i+1 ); in this case, x is said to be used by r; given a path r = a 1 , . . . , a n we will say that r leaves a 1 and enters in a n . Moreover, we require all nodes in a path from a node b to a node c to be distinct, with the possible exception of b and c.

If there is a directed path from a to b, we denote it by a + -→ b. A graph G is connected if for any pair of nodes a, b of G there exists a path from a to b. A cycle (resp. directed cycle) is a path (resp. directed path) a 1 , . . . , a n such that a 1 = a n . A directed acyclic graph (d.a.g.) is a directed graph without directed cycles. When drawing a d.a.g we will represent edges oriented up-down so that we may speak of moving downwardly or upwardly in the graph; in the same spirit we will say that a node is just above (resp. hereditarily above) or below (resp. hereditarily below) another node.

A d.a.g. with pending edges is a d.a.g. where some edges have a source but not a target. We call typed d.a.g. a d.a.g. with pending edges whose edges are possibly labelled with formulas ; we call such edges typed.

We call typed d.a.g. with ports a typed d.a.g. G where for each node b the typed edges incident on b and the typed pending edges of G are partitioned into subsets called ports.

We call module a d.a.g, where some edges have a target but not a source. We recall that we can represent a strict partial order as a d.a.g., where we have an edge b → a whenever a < 1 b (i.e. a < b, and there is no c such that a < c and c < b.) Conversely (the transitive closure of) a d.a.g. G induces a strict partial order ≺ G on the nodes of G.

We call predecessor of a node c, a node which immediately precedes (bottom-up) c in ≺ G (similarly for the successor).

A root of a d.a.g. is a node with no predecessors.

A forest (resp. tree) is a d.a.g. G such that, given a node a and a root b of G, there exists at most one (resp. exactly one) directed path from a to b.

Similarly, a strict order on a set is arborescent when each element has at most one immediate predecessor. An edge a → b is transitive if there is a node c such that a + -→ c and c → b. The skeleton of a d.a.g. G (denoted Sk(G)) is the directed graph obtained from G by erasing all the edges which are transitive Since Sk(G) is obtained from G just by erasing transitive edges, the order associated with Sk(G) as a d.a.g and the order associated with G as a d.a.g. are equal; so if the order associated with G is arborescent, the skeleton of G is a forest.

HS proofs as d.a.g.'s

Let us consider the following HS proof π 1 :

⊢⊥, 1 ⊢⊥, 1 ⊢⊥, 1 ⊢⊥, 1 ⊢ ⊗(⊥ 1 , ⊥ 2 , ⊥ 3 , ⊥ 4 ), 1, 1, 1, 1 (+, {1, 2, 3, 4}) (-,{{1,2}} ) ⊢ ⊗(⊥ 1 , ⊥ 2 , ⊥ 3 , ⊥ 4 ), 1, 1, (1 1 , 1 2 ) ⊢ 1, ⊥ (+,{3,4}) ⊢ ⊗(⊥ 1 , ⊥ 2 , ⊥ 3 , ⊥ 4 ), 1, 1, ⊗( (1 1 , 1 2 ) 3 , ⊥ 4 ), 1 (-,{{5,6}}) ⊢ ⊗(⊥ 1 , ⊥ 2 , ⊥ 3 , ⊥ 4 ), (1 5 , 1 6 ), ⊗( (1 1 , 1 2 ) 3 , ⊥ 4 ), 1 ⊢ 1, ⊥ (+,{7,8}) ⊢ ⊗(⊥ 1 , ⊥ 2 , ⊥ 3 , ⊥ 4 ), ⊗( (1 5 , 1 6 ) 7 , ⊥ 8 ), ⊗( (1 1 , 1 2 ) 3 , ⊥ 4 ), 1, 1
where each initial sequent is the conclusion of the following proof:

(+,{}) ⊢ 1 (-,{}) ⊢ 1, ⊥
The order of application of rules provides an arborescent partial order, which yields the following d.a.g. G 1 :

(+, {}) (+, {7, 8}) (-, {{}}) (-, {{5, 6}}) (+, {3, 4}) (-, {{1, 2}}) (+, {1, 2, 3, 4}) (+, {}) (+, {}) (+, {}) (+, {}) (-, {{}}) (-, {{}}) (-, {{}}) (-, {{}}) (-, {{}}) (+, {})
We can refine our analysis, and observe that the order associated with π 1 it is actually the merging of two orders:

• the causal order, which is the transitive closure of the following relation: a rule a is causally dependent from a rule b when the formula introduced by b is an active formula in the premises of a;

• the sequential order: a is sequentially dependent from b if a follows b (top-down) in the proof but it is not causally dependent from it.

For instance, the rule (+, {7, 8}) is causally dependent from the rule (-, {{5, 6}}), and is sequentially dependent for example from the rule (+, {3, 4}).

Let us draw the d.a.g G ′ 1 associated with the causal order (we label the edges with types in order to stress the subformula relation)

(1 1 , 1 2 ) (1 5 , 1 6 ) 1 1 1 1 1 1 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊗(⊥ 1 , ⊥ 2 , ⊥ 3 , ⊥ 4 ) ⊗( (1 5 , 1 6 ) 7 , ⊥ 8 ) ⊗( (1 1 , 1 2 ) 3 , ⊥ 4 ) (-, {{}}) (-, {{}}) (-, {{}}) (-, {{}}) (+, {1, 2, 3, 4}) (+, {}) (+, {}) (-, {{1, 2}}) (+, {}) (+, {}) (-, {{5, 6}}) (+, {3, 4}) (-, {{}}) (-, {{}}) (+, {7, 8}) (+, {}) (+, {})
If we add to G ′ 1 the information provided by the sequential order (in the form of dashed edges) we obtain the following d.a.g G ′′ 1 :

(

1 1 , 1 2 ) (1 5 , 1 6 ) 1 1 1 1 1 1 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊗(⊥ 1 , ⊥ 2 , ⊥ 3 , ⊥ 4 ) ⊗( (1 5 , 1 6 ) 7 , ⊥ 8 ) ⊗( (1 1 , 1 2 ) 3 , ⊥ 4 ) (-, {{}}) (-, {{}}) (-, {{}}) (-, {{}}) (+, {1, 2, 3, 4}) (+, {}) (+, {}) (-, {{1, 2}}) (+, {}) (+, {}) (-, {{5, 6}}) (+, {3, 4}) (-, {{}}) (-, {{}}) (+, {7, 8}) (+, {}) (+, {})
whose transitive closure bring us back to G 1 .

In G ′′ 2 we can observe that there are two kind of edges: the ones corresponding to causal order, (which is the correspondent of the structure of links in proof nets) and the ones corresponding to sequential order. We call the latter jumps. Now consider this other HS proof π 2 (differing from the first one only by permutation of rules):

⊢⊥, 1 ⊢⊥, 1 ⊢⊥, 1 ⊢⊥, 1 ⊢ ⊗(⊥ 1 , ⊥ 2 , ⊥ 3 , ⊥ 4 ), 1, 1, 1, 1 (+, {1, 2, 3, 4}) (-,{{5,6}}) ⊢ ⊗(⊥ 1 , ⊥ 2 , ⊥ 3 , ⊥ 4 ), 1, 1, (1 5 , 1 6 ) ⊢ 1, ⊥ (+,{7,8}) ⊢ ⊗(⊥ 1 , ⊥ 2 , ⊥ 3 , ⊥ 4 ), 1, 1, ⊗( (1 5 , 1 6 ) 7 , ⊥ 8 ), 1 (-,{{1,2}}) ⊢ ⊗(⊥ 1 , ⊥ 2 , ⊥ 3 , ⊥ 4 ), (1 1 , 1 2 ), ⊗( (1 5 , 1 6 ) 7 , ⊥ 8 ), 1 ⊢ 1, ⊥ (+,{3,4}) ⊢ ⊗(⊥ 1 , ⊥ 2 , ⊥ 3 , ⊥ 4 ), ⊗( (1 5 , 1 6 ) 7 , ⊥ 8 , ⊗( (1 1 , 1 2 ) 3 , ⊥ 4 ), 1, 1
If we perform on π 2 the same analysis we did on π 1 , we get the following graph G ′′ 2 , where the causal order is the same as G ′′ 1 but the sequential order is different.

(

1 1 , 1 2 ) (1 5 , 1 6 ) 1 1 1 1 1 1 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊗( (1 1 , 1 2 ) 3 , ⊥ 4 ) ⊗(⊥ 1 , ⊥ 2 , ⊥ 3 , ⊥ 4 ) ⊗( (1 5 , 1 6 ) 7 , ⊥ 8 ) (-, {{}}) (-, {{}}) (-, {{}}) (-, {{}}) (+, {1, 2, 3, 4}) (+, {}) (+, {}) (-, {{1, 2}}) (+, {}) (+, {}) (-, {{5, 6}}) (+, {3, 4}) (-, {{}}) (-, {{}}) (+, {7, 8}) (+, {}) (+, {})
Starting from this observations, in the following section we will define a notion of proof net with jumps, whose links correspond to HS rules. The question we will try to answer will be the following:

If we "relax" the sequential order in both G ′′ 1 , G ′′ 2 can we find another d.a.g. G ′′ 3 such that:

• Both G ′′ 1 , G ′′ 2 can be retrieved from G ′′ 3 ; • G ′′
3 is "logically" sound (as proof nets are sound with respect to linear sequent calculus)?

We stress that the examples above do not contain any "additive" feature; in order to represent proofs respecting the constraints induced by additives (namely the "contraction" of contexts implicit in the &-rule of LL) we will make use of d.a.g.'s with ports instead of plain d.a.g.'s.

J-proof nets

In this section we present J-proof nets for HS, using a syntax which is directly inspired by L-nets.

Firstly, in subsection 3.1, we give a first definition of pre-proof structure as a typed d.a.g. with ports; we introduce this first notion in order to represent the "additive contraction" effect induced by the (-, N )-rule. While in others syntaxes (as [START_REF] Laurent | Polarized proof-nets: proof-nets for LC (extended abstract)[END_REF]) this is done by introducing an explicit "additive contraction" link, here we adopt the convention of incorporating contraction into links, by partioning edges of the same type incident on the same link into ports. Then we refine the definition of pre-proof structure into the one of J-proof structure, which will allow us to define in our setting the notion of slice, a fundamental tool to deal with additives. In subsection 3.2 we study the relation between J-proof structures and HS, by defining sequentializable J-proof structures; then, in subsection 3.3, we introduce the correctness criterion and we define J-proof nets.

J-proof structures

Definition 1 (Pre-proof structure) A pre-proof structure is a typed d.a.g. with ports whose nodes (also called links) are labelled by one of the symbols cut, + I∈N , -I∈N

The label of a link imposes some constraints on the number and the types of its incident and emergent edges: we will call premises (resp. conclusions) the typed edges incident on (resp. emergent from) a link; an untyped edge is called a jump.

+ I∈N -I∈N Cut P ⊥ P i∈I P i ′ ∈I & I∈N ( i∈I (P i )) ⊕ I∈N (⊗ i∈I (N i )) N i ′ ∈I N i∈I C C C P Figure 1: Links of a pre-proof structure
• a cut-link has no conclusions, and two ports, one containing n ≥ 1 premises all typed by a formula A and the other containing k ≥ 1 premises all typed by A ⊥ ;

• a -I∈N link b (also called negative link) has:

one port for each i ∈ I; each port contains n ≥ 1 premises which are typed by the same formula P ;

one conclusion, typed by a formula N .

n ≥ 0 jumps incident on b.

If the premises of the i-th port (for i ∈ I) are typed by a formula P i , then the conclusion is typed by & J∈N ( j∈J (P j )), where I ∈ N .

• a + I∈N link b (also called positive link) has:

one port for each i ∈ I; each port contains n ≥ 1 premises which are typed by the same formula N ;

one conclusion, typed by a formula P .

n ≥ 0 jumps emergent from b.

If the premises in the i-th port (for i ∈ I) are typed by a formula N i , then the conclusion is typed by

⊕ j∈N (⊗ j∈j (N j ))
, where I ∈ N .

A link whose conclusion is a pending edge is called a terminal link; pending edges are also partitioned into ports called terminal ports in such a way that, if two pending edges belong to the same terminal port, they have the same type. Informally, we will call type of a port the type of the edges contained by the port. The conclusions of a pre-proof structure are the types of its terminal ports.

The constraints and the links of definition 1 are synthetically represented in fig. 1; we denote ports by black spots, and we distinguish positive and negative links by their shape; following this graphical convention, we will often label a positive (resp. negative) link simply with I ∈ N instead of + I∈N (resp. -I∈N ).

J-proof structures and slices

To properly take into account the structure of additives, we must now refine our definition of proof structure, as follows:

Definition 2 (Contracted links and &-rule) Given a pre-proof structure , two links a, b are contracted if the conclusion of a and the conclusion of b belong to the same port.

A & rule W is a maximal set {w 1 , . . . , w n } of negative contracted links. We will consider & rules as a sort of "macro" links, so we adopt for them the same terminology we use for links; we will often refer to the premises (resp. conclusion) of a &-rule W , meaning the premises (resp.conclusion) of the elements of W .

An additive pair is a pair of negative links belonging to the same & rule.

A & rule containing terminal links is called a terminal & rule.

{1, 2} {3, 4} {3, 4} {1, 2} {} {} {} {} {} {} {} {} 1 1 1 1 ⊥ ⊥ ⊥ ⊥ &( (1 1 , 1 2 ), (1 3 , 1 4 )) ⊕(⊗(⊥ 1 , ⊥ 2 ), ⊗(⊥ 3 , ⊥ 4 ))
Figure 2: example of J-proof structure Definition 3 (J-proof structure) A pre-proof structure R is a J-proof structure if it satisfies the followings:

Positivity: If a link a has in-degree 0, then is positive; In addition to the above conditions, a J-proof structure must have at most one negative conclusion.

Additives: if two
Remark 1 Since every J-proof structure R is a d.a.g, we can associate with it a partial order ≺ R . From now on we will always identify two J-proof structures which are equal modulo transitive jumps, where a transitive jump is a transitive edge which is a jump.

Let us give some explanations on the conditions of definition 3:

• Positivity forbids the presence of negative 0-ary links in a J-proof structure. Such a constraint is required to represent the fact that in the calculus HS defined above there can be only positive initial rules.

• Given the synthetic connective & I∈N ( i∈I (A i )), each of the ramifications I ∈ N corresponds to a branch of a (clustered) &. In J-proof structures we represent the sequent calculus rule introducing a & formula not with a single link, but with a set of links (the &-rule defined above), each of them corresponding to a branch of a &. The Additives condition then allows to recognize the different branches of which a &-rule is composed, by assigning to two different components of a &-rule a different ramification I ∈ N .

• The Coherence condition is required in order to define a proper notion of slice on J-proof structures. It assures that no conflict rises when determining if a link belongs or not to a given slice: namely, if a link is hereditarily above a component of a &-rule, then it cannot be above any other component of the same &-rule.

• The Contraction condition allows us to recognize whenever two different slices are superposed; by Contraction, we know that each time two links are contracted, we can determine the &-rule which justifies the superposition. Combining this condition with the previous one, we can then identify slices simply by looking at the links which are hereditarily above a given element of a & rule W , for all & rules.

{1, 2} {1, 2} {} {} {} {} 1 1 ⊥ ⊥ &( (1 1 , 1 2 ), (1 3 , 1 4 )) ⊕(⊗(⊥ 1 , ⊥ 2 ), ⊗(⊥ 3 , ⊥ 4 ))
Figure 3: a slice of the J-proof structure in fig. 2 Now we are in the position to formally define the notion of slice of a J-proof structure:

Definition 4 A slice of a J-proof structure R is a graph S obtained by selecting, for each & rule W = {w 1 , . . . , w n } of R, an element w i of W , erasing all the w j = w i ∈ W , and recursively all the links above them, and all the edges emergent from an erased link.

Totality

Once introduced the notion of slice, a natural restriction is to consider only "well defined" J-proof structures: that is, J-proof structures whose slices are themselves J-proof structures. We do that introducing the notion of totality.

Definition 5 A multiplicative J-proof structure is a J-proof structure without contracted links.

Definition 6 Given two J-proof structures R, R ′ we say that R, R ′ have the same conclusions whenever there exists a bijection between the terminal ports of R and the terminal ports of Definition 7 (Total J-proof structure) A J-proof structure R is total if

R ′ s.t. if b is terminal port of R and b ′ is the corresponding terminal port of R ′ ,
• for each negative-link a of R, with conclusion & I∈N ( i∈I (P i )), if N contains more than one ramification, then a belongs to a &-rule W and there is a bijective correspondence between the elements of N and the elements of W .

• for any slice S of R, S is a multiplicative J-proof structure with the same conclusions as R.

{1, 2} {3, 4} {3, 4} {1, 2} {} {} {} {} {} {} {} {} 1 1 1 1 ⊥ ⊥ ⊥ ⊥ ⊕(⊗(⊥1 , ⊥2), ⊗(⊥3 , ⊥4)) ⊕(⊗(⊥1 , ⊥2), ⊗(⊥3 , ⊥4 ))
&( (11 , 12), (13 , 14 ), (15 , 16 ))

Figure 4: example of J-proof structure which is not total

In figure 4 we show a J-proof structure R which is not total: there is not a bijective correspondence between the elements of the leftmost negative rule W and the elements of the directory {{1, 2}, {3, 4}, {5, 6}} of the conclusion of W ; morover the two slices of R have not the same conclusions of R . The J-proof structure in figure 2 instead is total.

Jumps and the additive structure

One important difference with respect to the definition of J-proof structure already given in [START_REF] Di | Jump from parallel to sequential proof: multiplicatives[END_REF] for the multiplicative fragment, is the role of jumps; in the additive case they not only graduate sequentiality, but allow also to keep track of the additive structure through the notion of dependency, which we define in the following.

Given a total J-proof structure R, a & rule W and a slice S of R, we denote by S W any slice of R obtained by choosing the same element as S for all & rule Z = W of R, while making a different choice only for W .

Definition 8 Given a &-rule W of a total J-proof structure R, we say that a link c depends from W iff for every slice S which contains a, all the slices S W does not contain a.

Proposition 1 Let R be a total J-proof structure, a be a link of R and W a & rule. a depends from W iff for some w ∈ W , a

+ -→ w in R.
Proof. The right to left direction is trivial. From left to right, let us suppose by absurd that a depends from W but for no element w of W , a + -→ w in R. But then for every slice S of R, by definition of slice, if a belongs to S then a belongs to any slice S W too, contradicting the hypothesis that a depends from W .

Axiom links

The reader confident with linear logic proof nets has certainly noticed that in the list of links defining a J-proof structure we did not include the axiom link, corresponding to the axiom rule of sequent calculus. An axiom link in proof nets has the following shape, with no premises and two conclusion typed by dual atomic formulas:

Ax P P ⊥
This choice was made to simplify our presentation of J-proof structure; nevertheless, we can simulate axiom links in our setting. If a is an axiom link, then we can replace it with a 0-ary positive link and a 0-ary negative link connected together through a jump as follows:

{} {} 1 ⊥
Modulo this replacement then, all the results which follow still hold in presence of axiom links.

J-proof structures and sequent calculus

Given an HS proof π and a J-proof structure R, we say that R can be associated with π, if R can be inductively decomposed in such a way that each step of decomposition of R corresponds to the writing down of a rule of π. If a J-proof structure R can be associated with a proof π of HS, we say that π is a sequentialization of R.

Decomposing a J-proof structure Given a J-proof structure R and a terminal link b of R by removing b from R we mean the following operation:

• erasing b (and all edges emergent from b) from R. We stress that, after erasing b, the edges incident on b become pending edges.

• partitioning the new typed pending edges into new terminal ports, in such a way that two new typed pending edges belong to two different terminal ports if and only if they were contained in two different ports of b. Any non typed pending edge is erased.

Definition 9 (Scope) Let R be a J-proof structure and W a terminal & rule of R: we call scope of an element w of W (denoted R w ) the graph obtained from R by erasing all links w ′ such that w ′ ∈ W and w ′ = w, and all links and edges hereditarily above some w ′ .

Proposition 2 Let R be a total J-proof structure with a terminal & rule W and let w be an element of W . The graph R ′ w obtained by taking R w (the scope of w in R) and removing w is a total J-proof structure.

Proof. First we have to prove that R ′ w is a J-proof structure: to prove that is enough to prove that R w is a J-proof structure: we must check then the four conditions of definition 3. The preservation of the coherence condition is a direct consequence of the fact the that R w is obtained by restricting R, so if a link a is above two different elements of the same & rule in R w then it is the case also in R, which is impossible by coherence condition on R. For the same reason, additive condition on R implies additive condition on R w . Concerning contraction condition, we reason by absurd and suppose that there are two positive contracted links a, b of R w that do not satisfy the contraction condition; since R w is a restriction of R, a, b must be contracted also in R; so by contraction condition on R there is an additive pair y 1 , y 2 such that a

+ -→ y 1 (resp. b + -→ y 2 ) in R.
Since we supposed that a, b do not satisfy the contraction condition on R w , the path a + -→ y 1 or the path b + -→ y 2 do not belong to R w . W.l.o.g., suppose that the path a + -→ y 1 does not belong to R w ; then at least one node c in the path does not belong to R w . But then we obtain a contradiction, since, by definition of scope, in R c + -→ w ′ for some element w ′ = w of W , and then a + -→ w ′ ; but then a cannot belong to R w , contradicting our initial hypothesis on a, b. Concerning positivity condition, it is easy to verify that by definition of scope, a link a of R belongs to R w iff a belongs to a slice S of R obtained by choosing w for the & rule W ; then by totality condition on R, S is a multiplicative J-proof structure, so it satisfies the positivity condition; but then also R w satisfies it. So R w is a J-proof structure, and then R ′ w is trivially a J-proof structure too. The fact that R ′ w is total is a direct consequence of the fact that 1) any slice of R w is a slice of R so by totality on R is a multiplicative J-proof structure; 2) any slice of R obtained by choosing the element w of W is a slice of R w , by definition of scope. It is then easy to verify that, once removed w, R ′ w is total.

Definition 10 (Splitting positive) Let R be a J-proof structure and c a positive terminal link with n ports (resp. a cut link with two ports); We say that c is splitting for R if removing c, R splits into R 1 , . . . , R n (resp. R 1 , R 2 ) J-proof structures, one for each port of c .

Sequentializable J-proof-structures

The following definitions are adapted from [START_REF] Laurent | Polarized proof-nets: proof-nets for LC (extended abstract)[END_REF].

Definition 11 We define the relation "L sequentializes R in ε", where R is a J-proof structure, L is a terminal link or a terminal &-rule of R and ε is a set of J-proof structures , in the following way, depending from L:

• If L is a positive link with no ports, and is the only link of R, then L sequentializes R into ∅;

• if L is a positive link or a cut link with n ports and is splitting, then L sequentializes R into {R 1 , . . . , R n } J-proof structures;

• if L is a terminal & rule W = {w 1 , . . . w n } with conclusion & J∈N ( j∈J (P j )
) such that there is a bijection between the elements of N and the elements of W , we consider for each w j the scope R wj of w j . If for all j ∈ {1, . . . n}, R wj is a J-proof structure with the same conclusions of R, and the graph R ′ wj obtained by removing w j from R wj is a J-proof structure too, then L sequentializes R into {R ′ w1 , . . . , R ′ wn }. • if L is a terminal negative link which does not belong to a &-rule, and removing it we get a J-proof structure R 0 , then L sequentializes R into R 0 .

Definition 12 (Sequentializable J-proof structure) A J-proof structure R is sequentializable if

• R has a terminal & rule (resp. a terminal negative link), which sequentializes R into a set of sequentializable J-proof structures (resp. a J-proof structure);

• R has no terminal & rule or terminal negative link and -R is composed by a single connected component, and at least one of its links sequentializes R into a set of sequentializable J-proof structures or into the empty set;

-R is composed by more than one connected component and each component is a sequentializable J-proof structure.

Proposition 3 If a J-proof structure R is sequentializable, there exists at least one proof π of HS, such that π is the sequentialization of R.

Proof.

By induction on the links of R:

1. n = 1: by positivity, the only node in R is a 0-ary positive link, whose sequentialization is the proof ⊢ 1 .

2. n > 1: suppose R contains one terminal &-rule W = {w 1 , . . . w n } with conclusion & J∈N ( j∈J (P j )); then by definition of sequentializable J-proof structure, W sequentializes R into R 1 , . . . , R n J-proof structures with conclusions respectively Γ, P 1 1 , . . . P k1 1 , . . . Γ, P 1 n . . . P kn n ; each R j by induction hypothesis has a sequentialization π j with conclusion ⊢ Γ, P j 1 , . . . P kj j . We obtain the sequentialization π of R by applying a (-, N ) rule with conclusion ⊢ Γ, & J∈N ( j∈J (P j )) to all π 1 , . . . π n .

If R has no terminal &-rule, but has a terminal negative link n of conclusion (P 1 , . . . P n ), then by definition of sequentializable J-proof structure n sequentializes R into a J-proof structure R 0 with conclusion Γ, P 1 , . . . P n ; R 0 by induction hypothesis has a sequentialization π 0 with conclusion ⊢ Γ, P 1 , . . . P n . We obtain the sequentialization π of R by applying a (-, {{J}}) rule with conclusion ⊢ Γ, (P 1 , . . . P n ) to π 0 .

Otherwise R has no negative conclusion; suppose R is composed by a single connected component; since it is sequentializable there exists at least one link L which sequentializes R. We choose one such link and we reason by cases:

• L is a cut link whose premises are typed by P, P ⊥ ; then L sequentializes R into two J-proof structures R 1 , R 2 with conclusions respectively Γ, P and ∆, P ⊥ ; by induction hypothesis R 1 (resp. R 2 ) has a sequentialization π 1 with conclusion ⊢ Γ, P (resp. π 2 with conclusion ⊢ ∆, P ⊥ ). We obtain the sequentialization π of R by applying to π 1 , π 2 a cut rule with conclusion ⊢ Γ, ∆; • L is a positive link + I∈N with conclusion ⊕ J∈N (⊗ j∈J (N j )); we recall that each port of L corresponds to an i ∈ I. L sequentializes R into R 1 , . . . , R n J-proof structures with conclusions respectively Γ 1 , N 1 . . . Γ n , N n ,; by induction hypothesis there exist π 1 , . . . , π n proofs with conclusion ⊢ Γ 1 , N 1 , . . . ⊢ Γ n , N n , which are sequenzializations of R 1 , . . . , R n , respectively. We obtain the sequentialization π of R by applying a (+,

I) rule with conclusion ⊢ Γ 1 , . . . , Γ n , ⊕ J∈N (⊗ j∈J (N j )) to π 1 , . . . , π n .
Otherwise, R is composed by more than one connected component, and each of them is a sequentializable J-proof structure; we conclude by applying induction hypothesis on them, followed by a sequence of Mix rules.

Correctness criterion

A correctness criterion must allow to characterize in an intrinsic, purely geometrical way all sequentializable J-proof structures, that is the ones which can be sequentialized into HS proofs; the J-proof structures satisfyng the criterion are called J-proof nets. The correctness criterion for J-proof structures in the additive case is composed by two conditions:

• a quantitative one, the totality condition, which assures that in a J-proof net there are enough slices to retrieve a sequent calculus proof. We have already discussed this condition in subsection 3.1.1.

• a qualitative one, called cycles condition, which is a reformulation in our setting of the homonymous condition introduced by Curien and Faggian on L-nets , see [START_REF] Curien | L-nets, strategies and proof-nets[END_REF].

⊗(↑ (10)10, &(13, 14)11) ⊗(↑ (10)10, &(11, 12)11) In order to define the Cycles condition, we need to introduce the notion of switching path in a J-proof structure:

1 1 1 1 1 1 {} {} {} {} {} {} {0} {1} {2} {0} {4} {3} {5} {6} {10, 11} {10
Definition 13 (Switching path and cycle) Given a J-proof structure R, and a &-rule W (resp. a negative link n) of R, we call switching edge of W (resp. n) any edge incident on an element of W (resp. on n). A switching path is a path which never uses two different switching edges of the same &-rule (resp. negative link) of R; a switching cycle is a switching path which is a cycle. Definition 14 (Cycles-correct J-proof-structure) A J-proof structure R is cycles-correct if, given a non empty union C of switching cycles of R, there is a negative rule W ∈ R not intersecting C and a pair w 1 , w 2 ∈ W such that for some links c 1 , c 2 ∈ C , c 1 + -→ w 1 and c 2 + -→ w 2 ; in this case we say that the additive pair

w 1 , w 2 ∈ W breaks C.
Cycles condition deals with cycles which crosses different slices of the same J-proof structure; in fact, in the framework of additive proof nets, as first pointed out by Girard in [START_REF] Girard | Proof-nets : the parallel syntax for proof-theory[END_REF], the correctness of the single slices of a proof structure does not imply the sequentiability of the whole proof net (see for example the representation of the Gustave function as a proof structure given in [START_REF] Hughes | Proof nets for unit-free multiplicative-additive linear logic[END_REF]).

In fig 6 we provide an example (due to Claudia Faggian) of a J-proof structure which is slice by slice switching acyclic, but it is not cycles-correct: there is a cycle crossing all the &-rules and all the terminal positive links.

As a consequence, we cannot choose any of the terminal positive links as the last rule of a sequent calculus proof, since none of them is splitting. In fig 5 instead we provide an example of a cycles-correct J-proof structure containing a "legal" cycle, which does not violate the Cycles condition. The example is based on an analogous one contained in [START_REF] Hughes | Proof nets for unit-free multiplicative-additive linear logic[END_REF]. Definition 15 (J-proof net) A J-proof net is a J-proof structure which is total and cycles-correct.

1 1 1 1 1 1 1 1 1 {} {} {} {} 1 1 1 {} {} {} {} {} {} {} {3, 4} ↑ (12) {3, 4} {3, 4} ↑ (12)
Theorem 1 (Sequentialization) Let R be a J-proof structure; R is a J-proof net iff is sequentializable.

The right to left direction is (as usual) trivial. In section 5 we provide a proof of the left to right one, upgrading the technique already used in [START_REF] Di | Jump from parallel to sequential proof: multiplicatives[END_REF] for the multiplicative fragment.

J-proof nets, L-nets and superposition

We already remarked that the "essence" of an additive proof is to be a superposition of proofs; in order to address the problem of sequenzialization, we need then to give a precise definition of what it means to "superpose" two proofs (or in our case, two J-proof structures). We define the operation of superposition of J-proof structures, by adapting the notion of union of chronicles from ludics and L-nets (see [CF]) to our setting. We begin by recalling the basic ludic notion of adress and by defining its relation with J-proof structure.

Note. In this section, we will only consider J-proof structures without cut links.

Adresses and ludification

An address is a sequence ξ of natural numbers. An adress σ is subadress of an adress ξ if ξ is a prefix of σ.

Let us take a non-empty multiset of formulas of HS. Let us call them A 1 , . . . , A n . A localization f of A 1 , . . . A n is a function which associates with every node F of the subformula tree of A j an adress, for every  ∈ {1, . . . , n}, in the following way:

• For every  ∈ {1, . . . , n} f (A j ) = ξ , where ξ is an arbitrary adress;

• f (A j ) = f (A k ), for j = k ∈ {1, . . . , n}; {1, 2} {1, 2} {} {} {} {} 1 1 ⊥ ⊥ ⊕(⊗(⊥ 1 , ⊥ 2 ), ⊗(⊥ 3 , ⊥ 4 )) &( (1 1 , 1 2 ), (1 3 , 1 4 )) {} 1 {5} {6, 7} ↑ 1 5 ⊗(↑ (1 5 ) 6 , &( (1 1 , 1 2 ), (1 3 , 1 4 )) 7 ) Figure 7: A J-proof structure R 1 . {1, 2} {1, 2} {} {} {} {} {} {5} {6, 7} ξ ξ6 ξ7 ξ65 ξ71 ξ72 σ σ1 σ2
Figure 8: A J-proof structure R 1 labelled with actions

• If f (F ) = σ, and F = ⊕ I∈N (⊗ i∈I (N i )) (resp. & I∈N ( i∈I (P i ))) then f (N i ) (resp. f (P i )) = σi, for i ∈ I ∈ N .
Informally, localization can be thought of as a way to unambiguously retrieve the position of a formula, given a forest of subformula trees.

Ludification An action is a pair k = (ξ, I) where ξ is an adress and I is a finite index set (that is, a ramification). An action k = (ξ, I) is said to use the adress ξ. We say that an action (ξ, I) generates the adress ξi for all i ∈ I, and that an action a is parent of an action b if a generates the adress used by b.

Given a J-proof structure R with conclusions A 1 , . . . , A n and a localization f of A 1 , . . . , A n , a ludification of R is a function l which associates with each link of R an action, in the following way:

• if a is a positive link labeled by (+, I) (resp. a negative link labelled by (-, I)), with conclusion P (resp.

N ) and

f (P ) = ξ (resp. f (N ) = ξ) then l(a) = (ξ, I).
With a slight abuse, we will extend the parent relation from actions to links, meaning that if a, b are links, a is parent of b iff l(a) is a parent of l(b); moreover, we will say that a and b are similar, if l(a) and l(b) use the same adress.

We call view of a link a the set of actions {l(a)} ∪{l(a ′ ); a + -→ a ′ }, equipped with the following order relation :

l(b) < l(c) iff b ≺ R c.
Remark 2 It is easy to observe that the ludification function l is completely determined by the localization function f on the conclusions of R; meaning, up to the choice of f , the function l is unique.

In figure 8 , in order to clarify how actions can be associated with links, we show how, starting from the J-proof structure R 1 given in figure 7, formulas can be replaced with adresses.

J-proof structure and L-nets The reader acquainted with L-nets will observe that the object represented in figure 8 is actually an L-net. In fact, to transform a cut-free J-proof structure R with conclusion Γ, N (where N is the unique negative conclusion of R) into an L-net G with interface ξ ⊢ Λ, it is enough to provide a localization of the conclusions of R which associate with N the adress ξ, and with the formulas in Γ the addresses in Λ; The set of views associated with the links of R straightforwardly induces an L-net with interface ξ ⊢ Λ.

Sharing equivalence

Before explaining how to superpose two J-proof structures, first we must define how to compare them in order to decide the portion of J-proof structures to be superposed. We introduce then an equivalence relation on J-proof structures, that we call sharing equivalence.

Definition 16 Let R 1 , . . . , R n be J-proof structures with the same conclusions. Let f be a localization for the conclusions of R 1 ; since R 1 , . . . , R n have the same conclusions, f is a localization also for the conclusions of R i for all i in {1, . . . , n}. Let l be a function from the links of R 1 , . . . R n to actions, such that l restricted to R i is the ludification of R i induced by f , for all i in {1, . . . , n}. Given two links a, a ′ of R 1 , . . . , R n , we say that a is sharing equivalent to a ′ modulo l (denoted by a ≡ l a ′ ) iff the view of a induced by l is equal to the view of a ′ induced by l.

Proposition 4 Let R 1 , . . . , R n be J-proof structures with the same conclusions and a, a ′ be two links of R 1 , . . . R n . Let f, f ′ be two localizations of the conclusions of R 1 (and hence of the conclusions of all R i for i ∈ {1, . . . , n}), and l, l ′ the ludifications of R 1 , . . . R n corresponding respectively to f, f ′ . Then a ≡ l a ′ if and only if a ≡ l ′ a ′ .

Proof.

Consider a single conclusion A of R 1 , . . . , R n and the two addresses ξ, σ associated with A respectively by f, f ′ . Now let us consider all the links a of R 1 , . . . , R n , such that l(a) = (λ, I) and λ has ξ has prefix (so that the conclusion of a is subformula of A) ; if we substitute in λ ξ with σ, we get an address λ ′ such that (λ ′ , I) = l ′ (a). Now, if we generalize the procedure to all the conclusions of R 1 , . . . , R n , substituting in l the adresses associated with the conclusions of R 1 , . . . , R n by f with the ones associated by f ′ , we get that l(a) = l ′ (a) for all links a; and moreover, for all links a, the view of a induced by l is equal to the view of a induced by l ′ . We conclude that, given f and two links a, b of R 1 , . . . R n such that a is sharing equivalent with b modulo l, if we replace f with f ′ in l ′ , then a is still sharing equivalent with b modulo l ′ .

Since by proposition 4, the relation of sharing equivalence induced by a ludification l does not depend from the specific ludification l chosen, we will speak more generally of sharing equivalence and denote it by ≡ (instead of ≡ l ).

Proposition 5 Given R 1 , . . . , R n J-proof structures with the same conclusions, the relation ≡ is an equivalence relation on the links of R 1 , . . . , R n ; moreover, there exists a unique sharing equivalence on R 1 , . . . , R n .

Proof. Sharing equivalence is trivially an equivalence relation; concerning unicity is a consequence of the definition of ludification of a J-proof structure, of remark 2 and proposition 4.

Proposition 6 Let R 1 , . . . , R n be J-proof structures with the same conclusions. and a, a ′ be two links in R 1 , . . . , R n . If a is sharing equivalent to a ′ then the type of the conclusion of a and the type of the conclusion of a ′ are the same.

Proof. Trivial from the fact that to be sharing equivalent for two links a, a ′ implies that l(a) = l(a ′ ) for some ludification l; that is l(a) and l(a ′ ) are two actions using the same addresses, meaning that the conclusions of a, a ′ are typed by the same formula, by definition of ludification of a J-proof structure.

In figure 10 we provide a representation of the J-proof structure R 2 in figure 9 where we have replaced formulas with adresses: comparing R 2 with the J-proof structure R 1 with the same conclusions in fig. 7 and looking at their views, we can tell for example that the left terminal positive links of R 1 and R 2 are sharing equivalent, but the right terminal positive links of R 1 , R 2 are not.

Superposition

Definition 17 Let R 1 , . . . , R n be J-proof structures with the same conclusions. Let a ∈ R j and a ′ ∈ R k be two similar links. Then a, a ′ are said to be sibling, whenever a is not sharing equivalent to a ′ , but either the parent b of a in R j and the parent b ′ of a ′ in R k are sharing equivalent or a, a ′ are both terminal links. Definition 18 (Compatibility) Let R 1 , . . . , R n be J-proof structures with the same conclusions. We say that R 1 , . . . , R n satisfy the compatibility condition whenever for any two sibling positive links b ∈ R j and b ′ ∈ R k , there are two negative sibling links

a ∈ R j , a ′ ∈ R k , such that b + -→ a in R j and b ′ + -→ a ′ in R k .
Definition 19 (Superposition) Let R 1 , . . . , R n be J-proof structures with the same conclusions. The superposition of R 1 , . . . , R n , is the J-proof structure R having the same conclusions of R 1 , . . . , R n , such that:

1. for all R 1 , . . . , R n and for every link a ′ of R i , there exists a link a of R s.t. a ≡ a ′ ;

2. R = R ′ 1 ∪ . . . ∪ R ′ n , where, given an R i for i ∈ {1, . . . , n}, R ′ i is the restriction of R to the set {a ∈ R : ∃a ′ ∈ R i s.t.a ≡ a ′ }.
Given R 1 , . . . , R n J-proof structures with the same conclusions, we will denote their superposition by ≬ (R 1 , . . . , R n ).

Proposition 7 Let R 1 , . . . , R n be J-proof structures with the same conclusions; there exists a unique J-proof structure R =≬ (R 1 , . . . , R n ) iff R 1 , . . . , R n satisfies the compatibility condition.

Proof. First of all, it is easy to see that if a, b are links of R 1 , . . . R n , the links a ′ , b ′ of R s.t. a ≡ a ′ and b ≡ b ′ are contracted iff a, b are sibling; as a consequence, it is easy to see that the compatibility condition is nothing but a reformulation of the contraction condition in terms of sharing equivalence.

Once stressed this, the left to right direction is trivial. Concerning the right to left direction, we have to prove that R is a J-proof structure; that is we have to prove that the constraints given in the definition of J-proof structure are respected. Concerning positivity condition, let us consider a negative link a of R; by point 2) of definition 19, there exists a link a ′ in some R i s.t. a ≡ a ′ ; by positivity condition on R i there exists a positive link b

′ in R i such that b ′ + -→ a ′ in R i ,
+ -→ b in R, {1, 2} {3, 4} {3, 4} {1, 2} {} {} {} {} {} {} {} {} 1 1 1 1 ⊥ ⊥ ⊥ ⊥ ⊕(⊗(⊥1 , ⊥2 ), ⊗(⊥3 , ⊥4
′ in R i such that a ′ + -→ b ′ in R i and b ≡ b ′ (
otherwise a, a ′ would not be sharing equivalent) ; but then if a is above two different elements of the same & rule in R, so does a ′ in R i , contradicting the hypothesis that R i is a J-proof structure.

Last, we show that additives condition holds for R. Suppose that w, w ′ are two negative sibling links of R j , R k respectively. We have two cases: either w, w ′ are both terminal links, or they aren't. In the first case, by definition of sharing equivalence, in order to be not sharing equivalent w, w ′ must have two different labels J, K ∈ N ; then w, w ′ satisfy the Additives condition on R. In the second case, since w, w ′ are siblings and not terminal, there exists in R j a link x (resp. in R k a link x ′ ) such that x is the parent of w in R j (resp. x ′ is the parent of w ′′ in R k ) and x ≡ x ′ . Since w, w ′ are negative links, and the views of their parents are the same, in order to be not sharing equivalent w, w ′ must have two different labels J, K ∈ N ; then w, w ′ satisfy the additives condition on R. Unicity of R is a consequence of the unicity of the sharing equivalence on R 1 , . . . , R n .

Proposition 8 If S 1 , . . . , S n are the slices of a total J-proof structure R, then ≬ (S 1 , . . . , S n ) = R Proof. Straightforward from the definitions.

In fig. 11 we provide the superposition R 3 of the J-proof structures R 1 , R 2 in fig. 7,9. The set of views associated with R 3 can be retrieved looking at fig 12. It can be easily verified that R 3 contains exactly the views of R 1 , R 2 .

Sequentializing with jumps

In this section we will provide a proof of the sequentialization theorem by showing how to retrieve a sequentialization of a J-proof net by adding jumps on it. First in subsection 5.1 we will isolate a particular class of J-proof structures, called arborescent, which we prove to be in a one-to one correspondence with HS proofs.

In the rest of the section we will show how we can turn any J-proof net R into an arborescent J-proof net R J by adding jumps. In subsection 5.2 we will first show a simple, purely multiplicative example recalling the techinque already used in [START_REF] Di | Jump from parallel to sequential proof: multiplicatives[END_REF]. Then in subsection 5.3, we will give an example of how to generalize the technique to include the additive case. In subsection 5.4 we formally define the operation of adding jumps on a J-proof structure and in subsection 5.5 we will finally prove the sequentialization theorem for J-proof nets.

Note. In this section, we will only consider J-proof nets without cut-links; we will speak about the question of sequentialization with cut-links in section 6.

Arborescence and sequent calculus

Definition 20 (Arborescent J-proof structure) A J-proof structure R is arborescent when the order ≺ R associated with R as a d.a.g. is arborescent.

Proposition 9 There is a one to one correspondance between cut-free arborescent total J-proof structures and cut-free proofs of HS, such that if a proof π is associated with an arborescent J-proof structure R, then π is the unique sequentialization of R.

Proof.

The proof is by induction on the height n of an HS proof π: n = 1: in this case, π is composed by just a 0-ary positive rule ⊢ 1 to which we associate a 0-ary positive link, whose unique sequentialization is trivially π. n = k + 1: We have different cases depending on the last rule of π:

• Let the last rule of π be a (-, N ) rule L with conclusion ⊢ Γ, & J∈N ( j∈J (P J )) and premises Γ, P 1 1 , . . . P k1 1 , . . . Γ, P 1 n . . . P kn n . Let R I be the arborescent J-proof structure associated by induction hypothesis with the proof π I of the premise Γ, P 1 I , . . . P kI I of L, corresponding to the ramification I ∈ N ; by induction hypothesis, π I is the unique sequentialization of R I . The arborescent J-proof structure R associated with π is the J-proof structure obtained in the following way:

1. add a -I∈N link b I with conclusion & J∈N ( j∈J (P j )) to each R I for I ∈ N , in order to get an arborescent J-proof structure R ′ I with conclusions Γ, & J∈N ( j∈J (P j )) for each I ∈ N ; 2. for every R ′ I and for every positive terminal link a of R ′ I , add a jump in R ′ I from a to b I , obtaining an arborescent J-proof-structure R ′′ I for each I ∈ N ; 3. R =≬ J∈N R ′′ J . It is easy to verify that R is a total arborescent J-proof structure whose unique sequentialization is π.

• Let the last rule of π be (+, I) rule with conclusion ⊢ Γ 1 , . . . , Γ n , ⊕ J∈N (⊗ j∈J (N j )), and premises respectively ⊢ Γ 1 , N 1 , . . . , ⊢ Γ n , N n . Let R i be the arborescent J-proof structure associated with the proof π i of the premise ⊢ Γ i , N i of L for i ∈ {1, . . . , n}; by induction hypothesis, π i is the unique sequentialization of R i for i ∈ {1, . . . , n}. Then the arborescent J-proof structure associated with π is the J-proof structure R obtained by connecting all R i together with a + I∈N -link with conclusion ⊕ J∈N (⊗ j∈J (N j )) for i ∈ {1, . . . , n}.

• Let the last rule of π be a Mix rule with conclusions ⊢ Γ, ∆ and premises respectively ⊢ Γ, ⊢ ∆; let R 1 , R 2 be the arborescent J-proof structures associated by induction hypothesis respectively with the proof π 1 , π 2 of the premises of L; always by induction hypothesis, π 1 (resp. π 2 ) is the unique sequentialization of R 1 (resp. R 2 ). Then the arborescent J-proof structure associated with π is the union of R 1 , R 2 .

Sequentializing with jumps: the multiplicative case

Let us consider the multiplicative J-proof net R given in fig. 13. Is easy to verify that R is sequentializable and that the proofs π 1 , π 2 of section 2.3, are two sequentializations of R. The order associated with R is not arborescent; to make it arborescent we add jumps between the leftmost negative link and the middle positive link, and between the rightmost negative link and the leftmost positive link, obtaining the J-proof structure R 1 in fig 14 ;  Now we consider the partial order induced by R 1 as a directed graph; the order is arborescent, so by Prop 9, R 1 is sequentializable into a unique proof, which happens to be π 1 .

But adding jumps as in R 1 is not the only way to retrieve an arborescent order; also the arborescent J-proof structure R 2 in fig 15 can be obtained from R by adding jumps. R 2 is sequentializable into a unique proof, namely π 2 .

The example above is purely multiplicative: adding jumps in presence of additives is a more delicate operation, which we will describe just below.

Sequentializing with jumps: the additive case

Let us consider the total J-proof net R in fig 16. It is easy to verify that R is sequentializable and that the following two proofs, named respectively π 1 , π 2 are two sequentializations of R: (+,{})

(+,{}) ⊢ 1 (-,{}) ⊢ 1, ⊥ (+,{1}) ⊢ 1, ⊕(⊥ 1 , ⊥ 2 ) (+,{}) ⊢ 1 (-,{}) ⊢ 1, ⊥ (+,{2}) ⊢ 1, ⊕(⊥ 1 , ⊥ 2 ) (-,{{1},{2}}) ⊢ &(1 1 , 1 2 ), ⊕(⊥ 1 , ⊥ 2 ) (+,{5}) ⊢ ⊕((&(1 1 , 1 2 )) 5 , ⊥ 6 ), ⊕(⊥ 1 , ⊥ 2 ) (+,{}) ⊢ 1 (-,{}) ⊢ 1, ⊥ (+,{1}) ⊢ 1, ⊕(⊥ 1 , ⊥ 2 ) (+,{}) ⊢ 1 (-,{}) ⊢ 1, ⊥ (+,{2}) ⊢ 1, ⊕(⊥ 1 , ⊥ 2 ) (-,{{1},{2}}) ⊢ &(1 1 , 1 2 ), ⊕(⊥ 1 , ⊥ 2 ) (+,{5}) ⊢ ⊕((&(1 1 , 1 2 )) 5 , ⊥ 6 ), ⊕(⊥ 1 , ⊥ 2 ) (-,{{3},{4}}) ⊢ ⊕((&(1 1 , 1 2 )) 5 , ⊥ 6 ), &((⊕(⊥ 1 , ⊥ 2 )) 3 , (⊕(⊥ 1 , ⊥ 2 )) 4 ) (+,{7}) ⊢ ⊕((&(1 1 , 1 2 )) 5 , ⊥ 6 ), ⊕((&(⊕(⊥ 1 , ⊥ 2 )) 3 , (⊕(⊥ 1 , ⊥ 2 )) 4 ) 7 , ⊥ 8 ) (11, 12) (15, 16) 1 1 1 1 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊗(⊥1, ⊥2, ⊥3 ,
⊢ 1 (-,{}) ⊢ 1, ⊥ (+,{1}) ⊢ 1, ⊕(⊥ 1 , ⊥ 2 ) (+,{}) ⊢ 1 (-,{}) ⊢ 1, ⊥ (+,{1}) ⊢ 1, ⊕(⊥ 1 , ⊥ 2 ) (-,{{3},{4}}) ⊢ &((⊕(⊥ 1 , ⊥ 2 )) 3 , (⊕(⊥ 1 , ⊥ 2 )) 4 ), 1 (+,{7}) ⊢ ⊕((&((⊕(⊥ 1 , ⊥ 2 )) 3 , (⊕(⊥ 1 , ⊥ 2 )) 4 )) 7 , ⊥ 8 ), 1, (+,{}) ⊢ 1 (-,{}) ⊢ 1, ⊥ (+,{2}) ⊢ 1, ⊕(⊥ 1 , ⊥ 2 ) (+,{}) ⊢ 1 (-,{}) ⊢ 1, ⊥ (+,{2}) ⊢ 1, ⊕(⊥ 1 , ⊥ 2 ) (-,{{3},{4}}) ⊢ &((⊕(⊥ 1 , ⊥ 2 )) 3 , (⊕(⊥ 1 , ⊥ 2 )) 4 ), 1 (+,{7}) ⊢ ⊕((&((⊕(⊥ 1 , ⊥ 2 )) 3 , (⊕(⊥ 1 , ⊥ 2 )) 4 )) 7 , ⊥ 8 ), 1 (-,{{1},{2}}) ⊢ &(1 1 , 1 2 ), ⊕((&((⊕(⊥ 1 , ⊥ 2 )) 3 , (⊕(⊥ 1 , ⊥ 2 )) 4 )) 7 , ⊥ 8 ) (+,{5}) ⊢ ⊕((&(1 1 , 1 2 )) 5 , ⊥ 6 ), ⊕((&((⊕(⊥ 1 , ⊥ 2 )) 3 , (⊕(⊥ 1 , ⊥ 2 )) 4 )) 7 , ⊥ 8 )
The arborescent J-proof structures R 1 , R 2 , which directly correspond respectively to π 1 , π 2 , are depicted in fig. 17, 18. The fact that R 1 , R 2 directly correspond to π 1 , π 2 is evident if we look at their skeletons in fig. 19, 20 ; the order between links matches perfectly the order between rules. Now, we must define a procedure to transform R in, for example, R 1 using jumps. A first, naive approach would be to add some jumps in R from the leftmost terminal positive link a to the elements of the rightmost &-rule W . Unfortunately, this method is wrong: it can be easily verified that adding such jumps on R will violate the coherence condition in the definition of J-proof structure. Moreover we have to deal with the fact that some links of R must be duplicated in order to get a J-proof structure corresponding to the proof π 1 : the naive approach does not take that into account. So we refine our procedure in the following way: instead of adding jumps directly on R, we add the jumps on the slices of R. Consider separately each of the four slices S 1 , S 2 , S 3 , S 4 of R and add in each slice a jump from a to the element of W which appears in the slice as in fig. 21 (we mark in red the jump added in each slice). In this way we get four multiplicative J-proof structures S ′ 1 , S ′ 2 , S ′ 3 , S ′ 4 ; now if we superpose them we retrieve exactly the J-proof structure R 1 in fig. 17. Observe that superposing S ′ 1 , S ′ 2 , S ′ 3 , S ′ 4 duplicates the leftmost positive terminal link in R 1 . We could as well add jumps in each of the slices S 1 , S 2 , S 3 , S 4 from the rightmost terminal positive link a ′ to elements of the leftmost &-rule W ′ and then superpose, obtaining the J-proof structure R 2 in fig 18 . Observe that this time is the rightmost terminal positive link which is duplicated in R 2 .

Sequentializing with jumps: the general case

In the example above, we have considered only the case where the target of the jump we want to add belongs to a terminal &-rule. To deal with the general case, we must take into account the fact that adding a jump from a link a to a link b implies (by transitivity) implicitly adding a jump from a to every negative link b

′ s.t. b + -→ b ′ .
Definition 21 (Adding a jump) Let R be a total J-proof structure, and a (resp. b) a positive (resp. negative) link of R. To add a jump from a to b we perform the following operations: 1. take the set of all the slices S 1 , . . . , S n of R; 2. for each slice S i of R, modify S i into S ′ i in the following way:

• if a does not belong to S i , then S ′ i = S i ; • if both a, b belongs to S i , S ′
i is obtained by adding a jump from a to b in S i ; • if a belongs to S i and b does not, then there exists at least one & rule W such that b depends from W in R (otherwise b would belong to S i ). To get S ′ i we add a jump from a to w, for all negative links w in S i such that for some &-rule W in R, w ∈ W and b depends from W .

The result of adding a jump from a to b is the J-prof structure R ′ which is the superposition of S ′ 1 , . . . , S ′ n .

Remark 3 It is straightforward that adding jumps on a multiplicative J-proof structure, as in the example of subsection 5.2, is a special case of the procedure defined in Definition 21. In this special case the target of the jump to be added does not depend from any &-rule.

Proposition 10 Let R be a total J-proof structure, a a positive link and b a negative link; then there exists a unique total J-proof structure R ′ obtained by adding a jump from a to b.

{1} {2} {1} {1} {2} {2} {3} {} {} {} {} {} {} {} {} 1 1 1 1 ⊥ ⊥ ⊥ ⊥ &(11, 12) {5} {7} {4} {4} {3} {7} ⊕(⊥1, ⊥2) ⊕(⊥1, ⊥2) ⊕((&(A1, B2))5, ⊥6) ⊕((&((⊕(⊥1, ⊥2))3, (⊕(⊥1, ⊥2))4)7, ⊥8) ⊕(⊥1, ⊥2) ⊕(⊥1, ⊥2) &((⊕(⊥1, ⊥2))3, (⊕(⊥1, ⊥2))4) &((⊕(⊥1, ⊥2))3, (⊕(⊥1, ⊥2))4)
Figure 18: The J-proof net R 2

Proof.

Let S 1 , . . . , S n be the slices of R and S ′ 1 , . . . , S ′ n be the multiplicative J-proof structures obtained by adding jumps following definition 21. To check that the superposition of S ′ 1 , . . . , S ′ n is a total J-proof structure, by proposition 7 we have just to check that compatibility condition on S ′ 1 , . . . , S ′ n is respected. Let us consider two positive links a ′ , a ′′ respectively belonging to S ′ j , S ′ k such that a ′ , a ′′ are siblings. Let us consider the occurrences 2 of a ′ , a ′′ in the slices S j , S k of R from which S ′ j , S ′ k are build. We have to prove that there exist two negative links w ′ in S ′ j w ′′ in S ′ k , such that a ′ + -→ w ′ in S j , a ′′ + -→ w ′′ in S k and w ′ , w ′′ are siblings in S ′ j , S ′ k . We have two cases:

1. Suppose a ′ in S j and a ′′ in S k are not siblings; first we show that a ′ ≡ a ′′ in S j , S k . In fact, let a ′ in S j and a ′′ in S k be not siblings and suppose by absurd that a ′ is not sharing equivalent to a ′′ in S j , S k . Since a ′ , a ′′ are siblings in S ′ j , S ′ k , then the link b ′ which is the parent of a ′ and the link b ′′ which is the parent of a ′′ are sharing equivalent in S ′ j , S ′ k . From the fact that a ′ , a ′′ are neither siblings nor sharing equivalent in S j , S k we must conclude that b ′ , b ′′ are not sharing equivalent in S j , S k (otherwise a ′ , a ′′ would be siblings in S j , S k ); but this would contradict the assumption that b ′ , b ′′ are sharing equivalent in S ′ j , S ′ k , because two nodes which are not sharing equivalent in S j , S k cannot be sharing equivalent in S ′ j , S ′ k (since the set of predecessors of a link can only increase by adding jumps). We must conclude then that a ′ ≡ a ′′ in S j , S k ; then it is straightforward that a ′ , a ′′ are two different occurences in S j , S k of the same link c of R. Now the set of predecessors of c are different in S ′ j and S ′ k (since a ′ , a ′′ are siblings in S ′ j , S ′ k ) so it must be that c + -→ a, where a is the source of the jumps to be added in R. Now let us consider all the &-rules b depends from in R. There must exists at least one &-rule Z such that b depends from Z in R, and for two different elements z, z ′ of Z z ∈ S j , z ′ ∈ S k ; otherwise by definition 21, we would add the same jumps from a in S ′ j and in S ′ k , and then a ′ , a ′′ would be sharing equivalent in S ′ j , S ′ k since a ′ ≡ a ′′ in S j , S k and a ′ + -→ a in S j (resp. a ′′ + -→ a in S k ). By the existence of z, z ′ and by definition of adding jumps, a

+ -→ z ′
in S ′ j and a + -→ z ′′ in S ′ k ; since z ′ , z ′′ belong to the same &-rule in R, they are siblings in S j , S k ; the set of predecessors of z ′ (resp. of z ′′ ) is the same in S j and in S ′ j (resp. in S k and in S ′ k ), so they are sibling also in S ′ j , S ′ k , and a ′ + -→ z ′ in S ′ j , a ′′ + -→ z ′′ in S ′ k . We conclude that S ′ j , S ′ k respect the compatibility condition.

2. Suppose a ′ in S j and a ′′ in S k are siblings: then by contraction condition on R (and the equivalence between compatibility and contraction condition) there exists respectively a negative link w ′ in S j s.t. a ′ + -→ w ′ and a negative link w ′′ in S k s.t. a ′ + -→ w ′′ and w ′ , w ′′ are siblings (so they belong to the same &-rule W of R). Now we have two sub-cases:

• w ′ , w ′′ are siblings also in S ′ j , S ′ k . Then compatibility condition is respected.

2 Since slices are subgraphs of a given graph, it makes sense to talk of different occurences of the same node in different slices. • w ′ , w ′′ are not siblings in S ′ j , S ′ k . If this is the case, then w ′ + -→ a in S j , w ′′ + -→ a in S k , and adding the jump from a to b makes that in S ′ j , S ′ k , w ′ , w ′′ are no more siblings. Now let us consider all the &-rules b depends from in R; using the same argument used in point 1), we can prove that there must exist a pair of negative links z ′ in S j , z ′′ in S k s.t. z ′ , z ′′ are two different elements of the same &-rule Z of R, b depends from Z in R, a + -→ z ′ in S ′ j (but not in S j ) and a + -→ z ′′ in S ′ k (but not in S k ). Since z ′ , z ′′ belong to the same &-rule in R, they are siblings in S j , S k ; by definition of adding jumps, the set of predecessors of z ′ (resp. of z ′′ ) is the same in S j and in S ′ j (resp. in S k and in S ′ k ), so they are sibling also in S ′ j , S ′ k , and a ′ + -→ z ′ in S ′ j ,a ′′ + -→ z ′′ in S ′ k , and we are done.

Concerning totality of R ′ , is trivially preserved from totality of R. The result is a consequence of the following observation: take a slice S i of R containing an element w of a &-rule W of R. Now if we choose a different element w ′ of W there exists (by totality of R) exactly one slice S j of R containing w ′ and such that for any other &-rule Z of R, S i , S j contain the same element z of Z. If we consider the multiplicative J-proof structures S ′ i , S ′ j corresponding respectively to S i , S j , induced by the adding of jumps, it is easy to see that the occurence of w in S ′ i and the occurence of w ′ in S ′ j are siblings, so they belong to the same &-rule of R ′ .

Proposition 11 Let R, R ′ be two total J-proof structure s.t. R ′ is obtained from R by adding jumps and ≺ R ′ is arborescent. Then R is sequentializable.

Proof. By proposition 9, R ′ is sequentializable into a unique proof π. We show that also R is sequentializable into π, by proving that if a link sequentializes R ′ , then a corresponding link of R sequentializes R too. We reason by induction on the number of links in R: n = 1: in this case, R and R ′ are composed by just a positive link without premises, trivially sequentializable;

n = k + 1: Suppose R, R ′ have a negative conclusion. If it is the conclusion of a &-rule consider the corre- sponding terminal &-rule W = {w 1 . . . , w n } in R ′ ; since R ′ is sequentializable, W sequentializes R ′ into {R ′ 1 , . . . R ′ n }
arborescent, sequentializable J-proof structures. Now we take the corresponding terminal negative rule W ′ = {w ′ 1 . . . , w ′ n } of R; for each element w ′ i of W ′ by proposition 2 the graph R ′ w ′ i obtained by removing w ′ i from the scope R w ′ i is a total J-proof structure. Since R ′ is obtained by adding jumps on R, each slice S ′ of R ′ can be obtained from a unique slice S of R by adding jumps on it. It is not difficult to prove then that each R ′ i can be obtained by adding jumps on R w ′ i , so R w ′ i is sequentializable by induction hypothesis, and W ′ sequentializes R. But then R is sequentializable. If the negative conclusion of R, R ′ is not the conclusion of a &-rule we consider the corresponding terminal negative link c of R ′ ; since R ′ is sequentializable, c sequentializes R ′ into an arborescent, sequentializable J-proof structure R ′ 0 ; it is easy to check that the J-proof structure R 0 obtained by removing the terminal negative link c ′ corresponding to c from R is a total J-proof structure and that R ′ 0 can be obtained by adding jumps on R 0 , so by induction hypothesis R 0 is sequentializable and c ′ sequentializes R.

Otherwise, we reason by cases, depending if R ′ is composed by one or more than one connected component:

• if R ′ is composed by a single connected component, we consider the terminal positive link c of R ′ which is minimal in ≺ R ′ ; c sequentializes R ′ into {R ′ 1 , .
. . , R ′ n } arborescent, sequentializable J-proof structures, so c is splitting for R. The corresponding terminal positive link c ′ of R must be splitting too (because adding jumps preserve connectedness) so it splits R into {R 1 , . . . , R n } total J-proof structures such that each R ′ i can be obtained by adding jumps on R i . But then {R 1 , . . . , R n } are sequentializable by induction hypothesis, and c ′ sequentializes R, so R is sequentializable.

• if R ′ is composed by {R ′ 1 , . . . , R ′ n } connected components, each component R ′
i is an arborescent, sequentializable J-proof structure; is easy to verify in this case R can be divided into {R 1 , . . . , R n } disjoint, total J-proof structure and that each R ′ i can be obtained by adding jumps on R i , so each R i by induction hypothesis is sequentializable. Then R is sequentializable.

Sequentialization

Now all is set to proceed with the main result of this section, namely the proof of the sequentialization theorem. To prove that a J-proof net is sequentializable, we use the following road map:

• given a J-proof net R, we iteratively add jumps on R until we get a J-proof net R ′ which contains a "maximal" amount of jumps; that is, any jump added on R ′ either breaks the correctness criterion (obtaining something which is not a J-proof net anymore) or is redudant (it does not increase the order associated to R ′ as a d.a.g.). J-proof nets as R ′ are called saturated (we formally define them below).

• The order associated with a saturated J-proof net is arborescent (Lemma 3).

• If the order associated with R ′ is arborescent, there exists a unique proof π which is the sequenzialization of R ′ (Prop. 9).

• if R ′ sequentializes into π, R too is sequentializable into π (prop.11); so R is sequentializable. &((⊕(⊥ 1 , ⊥ 2 )) 3 , (⊕(⊥ 1 , ⊥ 2 )) 4 ) ⊕((&(A 1 , B 2 )) 5 , ⊥ 6 ) &((⊕(⊥ 1 , ⊥ 2 )) 3 , (⊕(⊥ 1 , ⊥ 2 )) 4 ) ⊕((&(A 1 , B 2 )) 5 , ⊥ 6 ) ⊕((&(A 1 , B 2 )) 5 , ⊥ 6 ) &((⊕(⊥ 1 , ⊥ 2 )) 3 , (⊕(⊥ 1 , ⊥ 2 )) 4 ) ⊕((&(A 1 , B 2 )) 5 , ⊥ 6 ) &((⊕(⊥ 1 , ⊥ 2 )) 3 , (⊕(⊥ 1 , ⊥ 2 )) 4 ) ⊕((&((⊕(⊥ 1 , ⊥ 2 )) 3 , (⊕(⊥ 1 , ⊥ 2 )) 4 ) 7 , ⊥ 8 ) ⊕((&((⊕(⊥ 1 , ⊥ 2 )) 3 , (⊕(⊥ 1 , ⊥ 2 )) 4 ) 7 , ⊥ 8 ) ⊕((&((⊕(⊥ 1 , ⊥ 2 )) 3 , (⊕(⊥ 1 , ⊥ 2 )) 4 ) 7 , ⊥ 8 ) ⊕((&((⊕(⊥ 1 , ⊥ 2 )) 3 , (⊕(⊥ 1 , ⊥ 2 )) 4 ) 7 , ⊥ 8 ) S 2 {2} {1} {4} {1} {3} {2} {4} {3} {2} {2} {1} {1} {} {} 1 ⊥ &(1 1 , 1 2 ) ⊕(⊥ 1 , ⊥ 2 ) {5} {7} {} {} S 1 1 ⊥ &(1 1 , 1 2 ) ⊕(⊥ 1 , ⊥ 2 ) {5} {7} S 3 1 {} {} {5} {7} &(1 1 , 1 2 ) ⊕(⊥ 1 , ⊥ 2 ) {} {} S 4 {5} {7} &(1 1 , 1 2 ) ⊕(⊥ 1 , ⊥ 2 ) ⊥ ⊥ 1 Figure 21: adding a jump on R
The crucial point is the proof of Lemma 3; a restricted version of Lemma 3 for the multiplicative fragment was the main technical novelty introduced in [START_REF] Di | Jump from parallel to sequential proof: multiplicatives[END_REF].

A major obstacle to the extension of Lemma 3 to additives is the possible presence of "legal" switching cycles in additive J-proof nets, allowed by Cycles condition of the correctness criterion, but forbidden in the multiplicative case.

The first step towards the proof of sequentialization will be then to prove that Lemma 3 still holds in presence of additives; the auxiliary result allowing this will be Lemma 2, which states that any saturated J-proof net does not contain switching cycles.

A saturated J-proof net is switching acyclic.

Definition 22 (Saturated J-proof net) A J-proof net R is saturated if for every J-proof structure R ′ obtained from R by adding a jump, either Proof. The proof is a direct consequence of the fact that, if there was a strong switching path from w to a, then there would be also a strong switching path from b to a, since b depends from W , so b + -→ w for some element w of W by Prop. 1; this would contradict the hypothesis, q.e.d.

R ′ is not a J-proof net or ≺ R =≺ R ′ . Given a J-proof net R, a saturation R ′ of R is a saturated J-proof
Proposition 13 Let R be a J-proof net, a be a positive link and b a negative link of R; if there isn't any strong switching path from b to a in R, then the J-proof structure R ′ obtained by adding a jump from a to b in R, is a J-proof net.

Proof. By proposition 10, we must only prove that Cycles condition holds. The property follows from the fact that adding a jump from a to b cannot create new switching cycles: any new switching cycle in R ′ should use a jump from a which was not in R, and the conclusion of the link which is the target of the jump. A cycle like that cannot exist in R ′ , by the hypothesis that there is not any strong switching path from b to a in R3 , and Prop. 12.

Lemma 1 Let R be a J-proof net, C a union of switching cycles of R; then there exists an additive pair w 1 , w 2 ∈ W of R which breaks C and a positive link c ∈ C (we call such a positive link proper) s.t.

¬(c

+ -→ w 1 ) and ¬(c + -→ w 2 ); 2. c belongs to a cycle C ′ ∈ C s.t. there exists a node d ∈ C ′ which is hereditarily above w 1 or w 2 .

Proof.

The proof is by induction on the number n of cycles in C: -→ w 1 and d ′ + -→ w 2 ; in any case we contradict the condition coherence of definition 3, so there exists some link c s.t. ¬(c + -→ w i ) for i = 1, 2. Furthermore there has to be at least one positive link which enjoys the property, otherwise C would not be switching.

n = 1: Since n = 1, C is composed
n > 1: We proceed ad absurdum and we suppose that for all additive pairs in R breaking C, C does not contain a positive proper link.

Let us consider an additive pair w 1 , w 2 ∈ W breaking C in R, which exists by the correctness criterion on R.

Then by our hypothesis, by definition of proper link and by coherence condition on J-proof structures, we can partition the cycles of C in three groups: C 1 (the cycles with all elements above w 1 ), C 2 (the cycles with all elements above w 2 ) and C 0 ( the cycles whose elements are neither above w 1 or w 2 ). Now by induction hypothesis on C 1 ∪ C 0 , there exists an additive pair w ′ 1 , w ′ 2 which breaks C 1 ∪ C 0 and a positive link c ′ belonging to some swithcing cycle

C ′ ∈ C 1 ∪ C 0 such that c ′ is proper. Obviously neither w ′ 1 or w ′
2 can belong to C 2 ; otherwise they would be above w 2 , and then either there would be some cycle in C 1 which is above w 1 and w 2 , contradicting our hypothesis on C 1 , or there would be some cycle in C 0 which is above w 2 , contradicting our hypothesis on C 2 . But then the additive pair w ′ 1 , w ′ 2 breaks C too, and c is a proper link of C contradicting our hypothesis that, for all additive pairs breaking C, C does not contain any proper positive link.

Lemma 2 Let R be a J-proof net; if R contains a switching cycle , then R is not saturated.

Proof.

We consider the union C of all the switching cycles of R (there is at least one by hypothesis).There exists, by lemma 1, an additive pair w 1 , w 2 which breaks C and a positive proper link c belonging to a cycle C ′ ∈ C. By the fact that c is proper there exists a node d belonging to the same cycle C ′ ∈ C as c s.t. d is hereditarily above w 1 or w 2 ; w.l.o.g., let us assume that d is hereditarily above w 1 . By the existence of d there exists a switching path r ′ from c to w 1 , composed by a switching path from c to d (containing only nodes of C ′ ) and nodes in a directed path from d ∈ C ′ to w 1 .

Let's suppose that w 1 belong to a terminal &-rule W of R: in this case by proposition 13 we can add a jump from c to W , this doesn't create cycles and increases the order.

Otherwise W is not terminal; if this is the case, we show that there cannot be any strong switching path from a link w ′ in W to c. Let us suppose that there is a strong switching path r : w ′ . . . c in R; now if r and r ′ are disjoint by composing them we get a switching cycle intersecting W ; by correctness criterion, since w 1 , w 2 break C and w 1 , w 2 belong to W , W doesn't intersect any switching cycle of C, and since C contains all the switching cycles of R, we contradict the hypothesis that R is correct.

If r and r ′ do intersect, let's take the first point e starting from w ′ and going down on r where r meets C ′ (if r doesn't meet C ′ , this means that r and r ′ intersect on the directed path from d in C ′ to w 1 ; then we have a switching cycle intersecting W , contradicting correctness of R as above). The only interesting case is if e is negative: by the fact that e is in a switching cycle where at least d is above w 1 , there exists a strong switching path r ′′ from e to w 1 , so we compose the subpath of r from w ′ to e with r ′′ and we get a switching cycle intersecting W , contradicting correctness of R as above.

So there isn't any strong switching path from w ′ to c, then by proposition 13 we can add a jump from c to W in R, and retrieve a J-proof net R ′ .

A saturated J-proof net is arborescent.

Lemma 3 (Arborisation) Let R be a J-proof net. If R is saturated then ≺ R is arborescent.

Proof.

We prove that if ≺ R is not arborescent, then there exists a negative and a positive link s.t. we can add a jump between them which does not create cycles andmakes the order increase, the proof being just an adaption to J-proof nets of the arborisation lemma of [START_REF] Di | Jump from parallel to sequential proof: multiplicatives[END_REF].

If R contains some switching cycles, then we apply lemma 2 and we have done; so we can restrict ourselves to the case where R doesn't contain any switching cycle.

If ≺ R is not arborescent, then in ≺ R there exists a link a with two immediate predecessors b and c (they are incomparable). Observe that b and c are immediately below a in Sk(R) and also in R, that a must be positive and that b and c are two negative links which cannot depend from the same & rule, by condition coherence on a.

We have two possibilities: Assume that r and r ′ are not disjoint. Let d be the first node (starting from b ) where r and r ′ meets. Observe that d must be negative (otherwise there would be a cycle). Each path uses one of the premises, and the conclusion of d (hence the paths meet also in the node below d). From the fact that d is the first point starting from b where r and r ′ meet it follows that: (i) r ′ enters in d using one of the switching edges of d, and exits from its conclusion; (ii) each of r and r ′ must use a different switching edge of d.

Then we distinguish two cases (see fig 24):

• r enters d from one of its switching edges; we build a switching cycle taking the sub path b, ...., d of r ′ and the sub path d, ...., b of r.

• r enters d from the conclusion; then we build a switching cycle composing the sub path of r c, ..., d , the reversed sub path of r ′ d, ..., b and the path b, a, c .

Proof of Theorem 1 Proof. The left to right direction is trivial as usual; concerning the right to left direction, let us consider a saturation R ′ of R. By the arborisation lemma, ≺ R ′ is arborescent, so by proposition 9 R ′ is sequentializable into a unique proof π. But then, by proposition 11, R too is sequentializable into π. Figure 24: Case 2 in the proof of the arborisation lemma, where the paths r, r ′ are not disjoint.

J-proof nets and Mix rule

The proof of sequentialization provided above, could be easily adjusted in order to characterize exactly the J-proof nets whose sequentializations do not contain any occurence of the Mix rule. As usual in proof nets syntax, this is done by properly introducing the notion of correction graph; we skip the proof, which does not present any relevant difference w.r.t. the standard one (see [START_REF] Girard | Linear logic[END_REF]).

Definition 24 (Correction graph) Given a J-proof net R, a switching s is the choice of a switching edge for every & rule of R (and for every negative link which does not belong to a &-rule); a correction graph s(R) is the graph obtained by erasing the switching edges of R not chosen by s.

Definition 25 (s-connected) A J-proof net R is s-connected if all its correction graphs are connected.

Theorem 2 Let R be a J-proof net which is s-connected; then R is sequentializable, and any proof π associated with R does not make use of the Mix rule.

Cut elimination and semantics

In this section we study the dynamics of cut-reduction in J-proof structures. First in subsection 6.1 we discuss about sequentialization in presence of cut-links. Then in subsection 6.2 we define cut-elimination on J-proof structures. As in L-nets, reduction is performed in parallel on each slice: so to reduce a J-proof structure R, we will decompose R in slices, perform reduction separately on each of them, and then superpose all the cut free slices obtained in this way.

In subsection 6.3 we provide a denotational semantics of J-proof nets, using a variation of standard relational semantics based on the notion of pointed set (i.e. a set A equipped with a special element called point of A). The aim is to refine the relational model, in order to be able to semantically characterize sequential ordering, which in our setting is represented by jumps; as a matter of fact, jumps usually are not captured by relational semantics.

Actually, our approach is inspired by [START_REF] Boudes | Unifying static and dynamic denotational semantics[END_REF], where a step is made in the direction of developing a unified framework for both static (sets, coherence spaces, etc) and dynamic (games) denotational semantics.

Finally, in 6.4 we solve the question, left opened in 6.1, of the stability of correctness under cut-reduction.

Cut and sequentialization

Unfortunately, we cannot straightforwardly extend our proof of sequentialization in presence of cut-links. The problem relies in the definition of superposition of J-proof structures: as a matter of fact, superposing J-proof structures in presence of cut links is quite difficult. This is not a novelty: actually, in the framework of sliced polarized proof nets of [START_REF] Laurent | Slicing polarized additive normalization[END_REF], a similar problem is present, which makes hard to conciliate the presence of cuts inside proof nets and sequentialization. The way out is to consider only cut-free J-proof nets (for which we can prove sequentialization), compose them using cut-links, and then reducing the J-proof net obtained until we reach the normal form (which is cut-free, so that we can deal with it again).

The absence of "internal" cut links is not so restricting as it seems: as pointed out in [START_REF] Laurent | Slicing polarized additive normalization[END_REF], the "syntactical" difference between considering or not "internal" cut links is the same as the "semantical" distinction between "small steps" and "big steps" operational semantics in computer science.

The central point of this argument is the preservation of the property of being sequentializable under cut reduction; we prove this result in section 6.4 by using the injectivity property of pointed semantics with respect to J-proof nets, that we state in subsection 6.3.2; actually, this strategy is the same used by Laurent and Tortora de Falco for sliced polarized proof nets, using relational semantics.

Cut elimination

Now we define cut elimination on J-proof structures; we first begin by defining cut reduction for multiplicative J-proof structures in subsection 6.2.1. In subsection 6.2.2 then we extend cut elimination to the general case. In subsection 6.2.3 we prove that total J-proof structures are closed under cut-reduction, assuming a weaker form of correctness (namely that all slices composing a J-proof structure are switching acyclic).

Cut elimination on J-proof structures: the multiplicative case

There are two kinds of cut-elimination steps (we denote by R R ′ the relation "R reduces to R ′ "):

1. the + I∈N /-I∈N (where I = I) reduction step, which replaces the module β in R (depicted on top of Fig. 25) with the module γ (depicted on bottom of Fig. 25).

2. the + J∈N /-K∈N (where J = K) reduction step, which replaces R with the empty J-proof structure (see Fig. 26).

Let R R ′ ; when a node a (resp. an edge l) of R ′ comes from a (unique) node (resp. edge) ←a (resp. ←l ) of R we say that ←a (resp.

←l ) is the ancestor of a (resp. l) in R and that a (resp l) is a residue of ←a (resp. ←l ) in R ′ . We denote sometimes the residues of a node b (resp. an edge r) by

-→ b (resp. -→ r ).
Definition 26 (Correct multiplicative J-proof structure) A multiplicative J-proof structure is correct iff it is switching acyclic.

Proposition 14 Let c be a cut link between a positive link a and a negative link b in R, such that for some links a

′ , b ′ of R, b ′ + -→ b and a + -→ a ′ ; then if R R ′ by reducing c with a + I∈N /-I∈N step, in R ′ b ′ + -→ a ′ .
Proof. Straightforward from the definition of + I∈N /-I∈N step.

With respect to the rewriting rules + I∈N /-I∈N , + K∈N /-J∈N , reduction enjoys the following properties:

+I∈N -I∈N ⋆ ⋆ ⋆ ⋆ Cut Cut Cut Nn N ⊥ 1 ⊕I∈N (⊗i∈I (Ni)) Nn N1 N ⊥ n N ⊥ 1 N ⊥ n N1 &I∈N ( i∈I (N ⊥ i ))
Figure 25:

+ I∈N /-I∈N cut reduction. Theorem 3 (Preservation of correctness) Given a multiplicative J-proof structure R, if R is correct and R R ′ , then R ′ is correct.
Proof.

If the cut t to be reduced in R is reduced through a + K∈N /-J∈N step , the result is obvious. Otherwise, if t is reduced through a + I∈N /-I∈N step, we proceed ad absurdum: we assume that there is a switching cycle in R ′ , and we show that this contradicts the hypothesis that R is correct. Now, if the cycle does not cross the module γ in R ′ , then the switching cycle is also in R and we are done. Otherwise, it does cross γ: let us call c 1 , . . . , c n the cut links of R ′ created by reducing t in R, a i being the negative premise and b i being the positive premise of c i for i = 1, . . . , n; let us call f any negative link and g any positive link in γ in R ′ such that g jumps on f but ←g does not jump on ←f in R. The switching cycle may cross the module in different ways, using n new cuts and m new jumps created by reducing t in R; we detail some relevant cases, showing that each of them brings to a contradiction.

1. Suppose the cycle crosses exactly one cut link c i of R ′ created by reducing t in R and no new jumps (so n = 1 and m = 0); in this case, the cycle connects a i with b i with a path going outside the module γ in R ′ . Then there is a switching cycle in R, obtained by choosing ←b i as a switching edge in R.

2. Suppose that the cycle crosses exactly two new cut links c i , c j of R ′ created by reducing t in R and no new jumps (so n = 2 and m = 0). Then we have two subcases:

• Suppose the cycle connects a j with b i and b j with a i (for j = i) with a path going outside the module γ in R ′ ; then we reason as in case 1, opportunely choosing a switching edge.

• Suppose the cycle connects a i with a j and b i with b j (for j = i) with a path going outside the module γ in R ′ . Then it is easy to see that there is a switching cycle in R too, since ←a i and ←a j are connected inside the module β in R.

If the cycle crosses more than two cut links of R ′ created by reducing t in R and no new jumps (so n ≥ 2 and m = 0) the argument is completely analogous.

3. suppose the cycle does not cross any of the new cut links of R ′ created by reducing t in R, but it does cross one new created jump (so n = 0 and m = 1). In this case the cycle connects f with g outside the module γ in R ′ . Then there is a switching path connecting ←g with ←f outside the module β in R too, and is easy to see that there is a switching cycle in R too (since ←g and ←f are connected in the module β in R). If the cycle crosses more than two new jumps created by reducing t in R and no new cut links (so n = 0 and m ≥ 1) the argument is completely analogous. 4. suppose the cycle crosses at least one cut link c i of R ′ created by reducing t in R, and one new jump (so n ≥ 1 and m = 1). In this case the cycle connects a i with f outside the module γ in R ′ . Then there is a switching path connecting ←f with ←a i outside the module β in R too, and is easy to see that there is a switching cycle in R too (since ←f and ←a i are connected in the module β in R). If the cycle crosses more than two new jumps created by reducing t in R (so n ≥ 1 and m ≥ 1) the argument is completely analogous.

In all cases, supposing that R ′ contains a switching cycle implies that R contains a switching cycle, contradicting the hypothesis that R is correct. So R ′ is correct.

Theorem 4 (Strong normalization) For every correct multiplicative J-proof structure S, there is no infinite sequences of reductions S S 1 S 2 . . . S n . . .

Proof.

Trivial by the fact that at each step the number of links decreases.

Theorem 5 (Confluence) For every correct multiplicative J-proof structure S 1 , S 2 and S 3 , such that S 1 S 2 and S 1 S 3 , there is a slice S 4 , s.t. S 2 S 4 and S 3 S 4 .

Proof.

It easily follows from confluence of standard multiplicative proof nets (see [START_REF] Girard | Linear logic[END_REF]).

-J∈N

+K∈N ∅ Cut ⋆ ⋆ &I∈N ( i∈I (N ⊥ i )) ⊕I∈N (⊗i∈I (Ni))
Figure 26: + K∈N /-J∈N cut reduction (with J = K).

Cut elimination on J-proof structures: the general case

Once defined reduction for multiplicative J-proof structures, reduction of a total J-proof structure R in the general case follows these steps:

1. take the set of all the slices S 1 , . . . , S n of R;

2. for each slice S i of R, reduce S i to reach its normal form S ′ i : 3. take the J-prof structure R ′ which is the superposition of S ′ 1 , . . . , S ′ n .

One condition is necessary in order to well define reduction: the normal forms of the slices composing a J-proof structure must be cut-free, otherwise it would be impossible to superpose them. For this purpose we require that J-proof structures for being reduced satisfy a constraint called weakly correctness:

Definition 27 A J-proof structure is weakly correct when is total and all its slices are correct (that is switching acyclic).

The fact that the normal form of a slice of a weakly correct J-proof structure is cut-free is a simple consequence of Theorem 3. Now we can formally define the normal form of a J-proof structure:

Definition 28 Let R be a weakly correct J-proof structure and {S 1 , . . . , S n } be the set of the slices of R. If S ′ 1 , . . . , S ′ n are the cut-free slices obtained by reducing {S 1 , . . . , S n } , we call normal form of R ( denoted by [R]) the J-proof structure R ′ which is the superposition of S ′ 1 , . . . , S ′ n .

Example of cut elimination Let us consider the following J-proof structure R:

{1, 2} {} {3, 4} {} {} {} 1 1 1 1 {1, 2} {3, 4} {} {} {} {} ⊥ ⊥ ⊥ ⊥ {} 1 {5} {6, 7} ↑ 1 5 {1, 2} {} {3, 4} {} {} {} 1 1 1 1 cut ⊕(⊗(⊥ 1 , ⊥ 2 ), ⊗(⊥ 3 , ⊥ 4 )) &( (1 1 , 1 2 ), (1 3 , 1 4 )) &( (1 1 , 1 2 ), (1 3 , 1 4 )) ⊗(↑ (1 5 ) 6 , &( (1 1 , 1 2 ), (1 3 , 1 4 )) 7 )
To reduce it to normal form we consider each of the four slices of R.

The slice S 1 :

{1, 2} {} {} ⊥ ⊥ {} 1 {5} {6, 7} ↑ 1 5 {1, 2} {} {} 1 1 cut {} {3, 4} {} 1 1 ⊗(↑ (1 5 ) 6 , &( (1 1 , 1 2 ), (1 3 , 1 4 )) 7 ) ⊕(⊗(⊥ 1 , ⊥ 2 ), ⊗(⊥ 3 , ⊥ 4 )) &( (1 1 , 1 2 ), (1 3 , 1 4 )) &( (1 1 , 1 2 ), (1 3 , 1 4 ))
and the slice S 2 :

{3, 4} {} {} ⊥ ⊥ {} 1 {5} {6, 7} ↑ 1 5 {} {3, 4} {} 1 1 cut {1, 2} {} {} 1 1 &( (1 1 , 1 2 ), (1 3 , 1 4 )) ⊗(↑ (1 5 ) 6 , &( (1 1 , 1 2 ), (1 3 , 1 4 )) 7 ) ⊕(⊗(⊥ 1 , ⊥ 2 ), ⊗(⊥ 3 , ⊥ 4 )) &( (1 1 , 1 2 ), (1 3 , 1 4 ))
both reduce to the empty slice through a + K∈N /-J∈N step. The slice S 3 :

{1, 2} {} {} ⊥ ⊥ {} 1 {5} {6, 7} ↑ 1 5 {1, 2} {} {} 1 1 cut {1, 2} {} {} 1 1 ⊗(↑ (1 5 ) 6 , &( (1 1 , 1 2 ), (1 3 , 1 4 )) 7 ) ⊕(⊗(⊥ 1 , ⊥ 2 ), ⊗(⊥ 3 , ⊥ 4 )) &( (1 1 , 1 2 ), (1 3 , 1 4 )) &( (1 1 , 1 2 ), (1 3 , 1 4 ))
reduces to the slice S ′ 3 :

{} 1 {5} {6, 7} ↑ 1 5 {1, 2} {} {} 1 1 ⊗(↑ (1 5 ) 6 , &( (1 1 , 1 2 ), (1 3 , 1 4 )) 7 ) &( (1 1 , 1 2 ), (1 3 , 1 4 ))
the slice S 4 :

{3, 4} {} {} ⊥ ⊥ {} 1 {5} {6, 7} ↑ 1 5 {} {3, 4} {} 1 1 cut {} {3, 4} {} 1 1 &( (1 1 , 1 2 ), (1 3 , 1 4 )) ⊕(⊗(⊥ 1 , ⊥ 2 ), ⊗(⊥ 3 , ⊥ 4 )) &( (1 1 , 1 2 ), (1 3 , 1 4 )) ⊗(↑ (1 5 ) 6 , &( (1 1 , 1 2 ), (1 3 , 1 4 )) 7 )
reduces to the slice S ′ 4 :

{} 1 {5} {6, 7} ↑ 1 5 {} {3, 4} {} 1 1 &( (1 1 , 1 2 ), (1 3 , 1 4 )) ⊗(↑ (1 5 ) 6 , &( (1 1 , 1 2 ), (1 3 , 1 4 )) 7 )
Now if we consider the superposition of the normal forms of S 1 , S 2 , S 3 , S 4 we get the J-proof structure R ′ below, which is the normal form of R:

{} 1 {5} {6, 7} ↑ 1 5 {1, 2} {} {3, 4} {} {} {} 1 1 1 1 &( (1 1 , 1 2 ), (1 3 , 1 4 )) ⊗(↑ (1 5 ) 6 , &( (1 1 , 1 2 ), (1 3 , 1 4 )) 7 )

Preservation of weakly correctness

Now we want to prove that the normal form [R] of a weakly correct J-proof structure R is still a weakly correct J-proof structure; the delicate part is proving that [R] is still a J-proof structure. Given a link a of a J-proof structure R, we say that a belongs to the right (resp. left) branch of a cut-link c iff there exists a directed path from a to c, which does not use jumps, entering c by its right (resp. left) port.

Given a J-proof structure R and a link a of R, we say that a is hidden by a cut link c (or simply hidden) if a belongs to a branch of a cut link c of R, we call it visible otherwise.

A slice is persistent if it does not reduce itself to the empty slice.

If S is a persistent slice, and a is a link hidden by some cut-link c of S, the opposite link of a is the link b in the opposite branch of c w.r.t. a, such that there exists a slice S ′ obtained by a sequence of reduction from S where the conclusion of a and the conclusion of b are premises of the same cut link c ′ of S ′ . Lemma 4 Let S 1 , S 2 be two persistent slices of a weakly correct J-proof structure R. Let a and b be a pair of positive links of R, such that a + -→ w in S 1 and b + -→ y in S 2 , where w, y are two negative links of R which form an additive pair. Then there exists a finite sequence s = (w 1 , y 1 ), . . . , (w n , y n ) of additive pairs of R, s.t.:

1. w 1 = w, y 1 = y; 2. for each i = n, w i , y i are hidden, their respectively opposite links a ′ , b ′ are contracted in R and a ′ + -→ w i+1 in S 1 , b ′ + -→ y i+1 in S 2 ;

3. w n , y n are visible.

Proof. We proceed by induction on the lenght n of the sequence s. If n = 1, trivially w, y are visible. Otherwise, w i , y i are hidden; then by persistence of S 1 , S 2 the opposite link a ′ of w i in S 1 and the opposite link b ′ of y i in S 2 must be two different contracted links of R (otherwise one of S 1 , S 2 should reduce to the empty slice). But then by contraction condition on R, there exists a negative link w ′ in S ′ 1 (resp. a negative link y ′ in S ′

2 ) such that a + -→ w ′ and b ′ + -→ y ′ and w ′ , y ′ form an additive pair in R; we take w ′ , y ′ as w i+1 , y i+1 in s. Finiteness of s is a consequence of finiteness and correctness of S 1 , S 2 .

Lemma 5 Let S 1 , S 2 be two persistent slices of a weakly correct J-proof structure R. Let a and b be a pair of positive links of S 1 , S 2 respectively, such that a, b are two different occurences of the same visible link c of R and c + -→ d for some hidden link d of R (so a

+ -→ d in S 1 , b + -→ d in S 2 ).
Then there exists a maximal finite sequence of links s : c 1 , d 1 , . . . c n , d n where c i is a positive link of R, d i is an hidden negative link of R, such that:

• c 1 = c (resp d 1 = d); • c i + -→ d i in R;
• for each i, the opposite positive link of d i in S 1 (resp. the opposite positive link of d i in S 2 ) are both occurences of c i+1 in S 1 , S 2 , and d i , d i+1 are not hidden by the same cut link c of R.

Proof. The proof is a simple induction on the lenght n of s. Finiteness of s is a consequence of weak correctness and finiteness of R, and of the observation which follows. Given the final element c n , d n of s, by definition of s and by maximality of s it must be that d n is hidden by a cut link m of R, and the opposite positive link a ′ of d n in S 1 (resp. the opposite positive link b ′ of d n in S 2 ) are either occurences of two different contracted links of R, or they are occurences of the same link c ′ of R. In the latter case, there is not any negative link d ′ hidden by a cut link

m ′ = m such that c ′ + -→ d ′ in R in R.
Proposition 15 Given a weakly correct J-proof structure R and a normal form [R] of R, [R] is a weakly correct J-proof structure.

Proof.

We first have to check that [R] is a J-proof structure; by proposition 7, it is enough to check that the compatibility condition of definition 18 is respected.

Consider the multiplicative, cut-free J-proof structures S ′ j , S ′ k obtained by reducing two different persistent slices S j , S k of R. Now let us suppose that there is a positive link a ∈ S ′ j and a positive link b ∈ S ′ k such that a and b are siblings; a, b are clearly visible in S j , S k . We have to prove that there exist two negative links w ′ in S ′ j , w ′′ in S ′ k , such that a

+ -→ w ′ in S ′ j , b + -→ w ′′ in S ′
k and w ′ , w ′′ are siblings in S ′ j , S ′ k . Now we have the following cases:

1. Suppose that a + -→ w j in S j and b + -→ w k in S k , where w j , w k are two negative links which forms an additive pair in R; then by lemma 4 there exist a finite sequence s = (w j1 , w k1 ), . . . (w jn , w kn ) of additive pairs of R. We remark that every two different hidden elements (w ji , w ki ), (w j l , w k l ) of s are hidden by two different cut links of R (by weakly correctness of R); the final pair w jn , w kn of s is visible with w jn belonging to S j (resp w kn belonging to S k ). By repeated applications of remark 4 and by theorem 5 it follows that in S ′ j a + -→ w jn ; similarly we can found that b + -→ w kn in S ′ k . We have two subcases:

(a) if w jn , w kn are not above any cut link of R, then w jn , w kn must be sibling in S ′ j , S ′ k , and they form an additive pair in [R] too. But then S ′ j , S ′ k satisfy the compatibility condition. occurences of the same link of R, then it is straightforward that after reduction the view of c in S ′ j and the view of c in S ′ k will stay the same, so w jn , w kn must be sibling in S ′ j , S ′ k , and they form an additive pair in [R], q.e.d. ii. Otherwise, the opposite positive link d ′ of d n in S j and the opposite positive link d ′′ of d n in S k are two different contracted links of R. In this case after reduction the view of c in S ′ j and the view of c in S ′ k may differ, so w jn , w kn could be not sibling in S ′ j , S ′ k . Then we search for two new negative sibling links: since d ′ and d ′′ are two different contracted links of R, then by contraction condition on R, there exists a negative link w ′′ j in S j and a negative link w ′′ k in S k such that w ′′ j , w ′′ k form an additive pair in R and d ′ + -→ w ′′ j in S j (resp. d ′′ + -→ w ′′ k in S k ). By repeated applications of remark 4 and by theorem 5 it follows that in S ′ j a + -→ w ′′ j and that b

+ -→ w ′′ k in S ′
k . If w ′′ j , w ′′ k are not above any cut link of R, they must be sibling in S ′ j , S ′ k ; but then S ′ j , S ′ k satisfy the compatibility condition, q.e.d. Otherwise, we replicate on w ′′ j , w ′′ k the same procedure from the beginning of point 1. (replacing w j , w k with w ′′ j , w ′′ k and a, b with d ′ , d ′′ ), iterating the applications of lemma 4 and lemma 5 until by finiteness of R we eventually found a proper visible additive pair of R.

2. Suppose that there is no additive pair w 1 , w 2 of R such that a Once proved that [R] is a J-proof structure, it remains to check that is weakly correct: switching acyclicity slice by slice is trivially preserved, due to theorem 3. Preservation of totality is a simple consequence of the following observation: take a non-persistent slice S of a J-proof structure R. Cut-reduction of S must end with a + K∈N /-J∈N , with K = J. Then by totality of R there must exist a slice S ′ of R such that:

• For all visible &-rules W of R, S ′ contains the same element w as S;

• For all hidden &-rules W ′ of R, if an element w ′ of W ′ chosen by S is the "active" link of a + K∈N /-J∈N step reducing S the empty slice, we choose in S ′ another element w ′′ of W ′ which gives rise instead to a + I∈N /-I∈N step during the reduction of S ′ (such an element exists by totality of R).

Such a slice S ′ is clearly persistent, so for every non-persistent slice S of R there exists a persistent slice S ′ of R which makes the same choices of elements as S on the visible &-rules of R. This is enough to conclude the totality of [R].

Theorem 6 (Existence of a normal form) Given a weakly correct J-proof structure R, there exists a weakly correct J-proof structure R ′ such that R ′ = [R].

Proof.

The proof is an easy consequence of theorem 4.

Theorem 7 (Confluence) If R, R ′ , R ′′ are weakly correct J-proof structures, such that R ′ , R ′′ are normal forms of R, then R ′ = R ′′ .

Proof. Trivial, from theorem 5.

Semantics

We focus now on semantics, following these steps: in subsection 6.3.1 we define the interpretation of a Jproof structure in pointed sets using the notion of experiment and we prove that semantics is stable under cut-reduction. Then in subsection 6.3.2, we prove that pointed sets semantics is injective with respect to total J-proof structures, that is for any two total J-proof structures R, R ′ , if R and R ′ have the same interpretation, then R = R ′ . Experiments have been introduced by Girard in [START_REF] Girard | Linear logic[END_REF], and extensively studied in [START_REF] Tortora De Falco | Réseaux, cohérence et expériences obsessionnelles[END_REF] by Tortora de Falco, as a way to compute the interpretation of a proof net without resorting to sequentialization. Semantic injectivity has been studied in the setting of linear logic mainly by Tortora (see [START_REF] Tortora De Falco | Réseaux, cohérence et expériences obsessionnelles[END_REF] and Pagani in [START_REF] Pagani | Proof nets and cliques: towards the understanding of analytical proofs[END_REF]; however, it is a traditional question in the denotational semantics of λ-calculus, and it is deeply related with the one of syntactical separability stated in the Böhm theorem for pure λ-calculus ([Boh68]); furthermore, syntactical separability is also one of the main properties in ludics (both of designs, see [START_REF] Girard | Locus solum: from the rules of logic to the logic of rules[END_REF], and more generally of L-nets, see [START_REF] Faggian | Ludics nets, a game model of concurrent interaction[END_REF]).

By now we will denote sets by A, B, C, . . . and elements of a set by a, b, c, . . .. A pointed set A * is given by a set A ∪ {0 A * } where 0 A * is a distinguished object which does not belong to A; this object is called the point of A * .

The pointed product A 1 ⊛. . .⊛A n of n sets A 1 , . . . , A n is the pointed set A 1 ×. . .×A n ∪{0 A ⊛ An } whose elements are the tuples of the cartesian product A 1 × . . . × A n together with a distinguished fresh object 0 A1 ⊛...⊛ An which does not belong to A 1 × . . . × A n .

By A 1 ⊎ . . . ⊎ A n we denote the disjoint union of A 1 , . . . , A n .

In general, a formula is interpreted by a disjoint union (indexed by ramifications) of pointed products of pointed sets.

More formally, the interpretation F of a formula F of HS is defined in the following way:

• a positive formula ⊕ I∈N (⊗ i∈I (N i )) is interpreted by the set ⊎ I∈N (⊛ i∈I (N * i ));

• a negative formula & I∈N ( i∈I (P i )) is interpreted by the set ⊎ I∈N (⊛ i∈I (P * i )).

Experiments

Given a J-proof structure R with conclusions C 1 , . . . , C n , we define the interpretation R of R as a subset of

C * 1 ⊛ • • • ⊛ C *
n , which we define using the notion of experiment. In the sequel, for simplicity's sake and when it is clear from the context, given a pointed set

A * = ⊎ I∈N (⊛ i∈I (A * i )) which interprets a formula & I∈N ( i∈I (A i )) (resp. a formula ⊕ I∈N (⊗ i∈I (A i ))
), we will denote the elements I, 0 ⊛i∈I (A * i) (for I ∈ N ) of A * , simply by 0 A * or by 0.

Definition 29 (Experiments) Let S be a multiplicative J-proof structure and e an application associating with every edge a of type A of S an element of A * ; e is an experiment of S when the following conditions hold:

• if x, y are premises of a cut link with premises x and y, then e(x) = e(y).

• Suppose x is the conclusion of a negative link -I∈N with premises x 1 of type P 1 , . . . , x n of type P n . If for all i ∈ {1, . . . , n} e(x i ) = 0 P * i , then e(x) =< I, < 0 P * 1 , . . . , 0 P * n >> or e(x) =< I, 0 P * 1 ⊛...⊛P * n >.

Otherwise e(x) =< I, < a 1 , . . . , a n >>, where e(x 1 ) = a 1 , . . . , e(x n ) = a n .

• Suppose x is the conclusion of a positive link + I∈N with premises x 1 of type N 1 , . . . , x n of type N n . If for all i ∈ {1, . . . , n} e(x i ) = 0

N * i , then e(x) =< I, < 0 N * 1 , . . . , 0 N * n >> or e(x) =< I, 0 N * 1 ⊛...⊛N * n >.
Otherwise e(x) =< I, < a 1 , . . . , a n >>, where e(x 1 ) = a 1 , . . . , e(x n ) = a n .

• If a is a positive link with conclusion x of type A and b is a negative link with conclusion y of type B, and there is a jump between b and a, then if e(x) = 0 A * , e(y) = 0 B * .

If x 1 , . . . , x n of type respectively A 1 , . . . , A n are the conclusions of S and e is an experiment of S such that e(x i ) = a i then we shall say that < a 1 , . . . , a n > is the conclusion or the result of the experiment e of S, and we will denote it by |e|. The set of the results of all experiments on S is the interpretation S of S; in case S is empty , then its interpretation is the empty set.

Let R be a total J-proof structure and {S 1 , . . . , S n } the set of slices of R; the interpretation R of R is the union of S 1 , . . . , S n .

In figure 27, 28 we provide two examples of experiments on the slices of the J-proof structure in fig. 11.

({5}, <<>>) <> 0 1 0 1 0 ⊥ 0 ⊥ ({3, 4}, 0 1⊛1 ) ({6, 7}, < ({5}, <<>>), ({3, 4}, 0 1⊛1 ) >) ({3, 4}, 0 ⊥⊛⊥ ) {3, 4} {3, 4} {} {} {} {} 1 1 ⊥ ⊥ ⊕(⊗(⊥ 1 , ⊥ 2 ), ⊗(⊥ 3 , ⊥ 4 )) &( (1 1 , 1 2 ), (1 3 , 1 4 )) {} {5} {6, 7} ↑ 1 5 1 ⊗(↑ (1 5 ) 6 , &( (1 1 , 1 2 ), (1 3 , 1 4 )) 7 )
Figure 27: example of experiment Remark 5 We can consider experiments as a way to travel bottom-up on a J-proof structure R looking only at its semantics; starting from an element of R , then it is possible to rebuild bottom-up R itself. Observe that the " 0" points introduced in pointed sets semantics, can be used in experiments as a sort of semantical "traffic light", forbidding bottom-up the access to a whole portion of R; in this way it becomes possible to recover information about the sequential order contained in R.

Proposition 16 If S is a correct multiplicative J-proof structure, and S S ′ , then S = S ′ . Proof. We must show that for every experiment e on S ′ , there is an experiment e ′ of S with the same result.

Having as reference fig. 25 let us suppose that S S ′ with a + I∈N /-I∈N step reducing a cut in S between a positive link a with conclusion x and premises x 1 of type N 1 , . . . , x n of type N n , and a negative link b with conclusion y and premises y 1 of type P 1 , . . . , y n of type P n ; we denote the edges of type P 1 , . . . , P n (resp. N 1 , . . . , N n ) by y 1 , . . . , y n (resp. x 1 , . . . , x n ). Suppose that a positive link c of typed conclusion z jumps on b, and that a jumps on a negative link d with conclusion w.

The delicate part is the one dealing with jumps, the rest of the proof trivially following from the preservation of relational semantics under cut reduction (see for instance [START_REF] Girard | Linear logic[END_REF]).

Let us consider an experiment e of S ′ . The relevant cases to check are the following:

• if in S ′ e(w) = 0, then e(z) = 0, e(y 1 ) = 0, . . . , e(y n ) = 0 by definition of experiment. We can then build an experiment e ′ of S with the same values on the corresponding edges of S by assigning e ′ (x) = 0 and e ′ (y) = 0;

• suppose in S ′ e(w) = 0, e(z) = 0 and e(y 1 ) = 0, . . . , e(y n ) = 0. We can then build an experiment e ′ of S with the same values on the corresponding edges of S by assigning e ′ (y) =< 0 P 0 1 , . . . , 0 P 0 n > and e ′ (x) =< 0 N * 1 , . . . , 0 N * n >.

Proposition 17 If R, R ′ are weakly correct J-proof structures, such that R ′ = [R], then R = R ′ .
Proof. The proof is a consequence of proposition 16.

Injectivity

We first prove injectivity with respect to multiplicative J-proof structures, then we extend the result to the general case.

Multiplicative J-proof structures and injectivity.

Definition 30 (Relational result) Let S be a multiplicative J-proof structure and |e| the result of an experiment on S; |e| is relational if it does not contain any occurrence of the element 0.

The set of relational results of experiments on a multiplicative J-proof structure S is called the relational part of S ; we will denote it by S Rel .

Remark 6 Given two multiplicative J-proof structures S, S ′ , if S = S ′ then S Rel = S ′ Rel .

Remark 7 Let S be a multiplicative J-proof structure and e, e ′ be two experiments of S. If |e| = |e ′ |, then e = e ′ ; in other words an experiment is completely determined by its result.

Remark 8 Given a multiplicative J-proof structure S, there exists a unique relational experiment e on S. In fact the relational part S Rel of S is a singleton, since the procedure of bulding an experiment is completely deterministic, provided it never assign the label 0 to any edges.

Given a slice S, we denote by S -the graph obtained by erasing all the jumps of S.

Lemma 6 Let S, S ′ be two multiplicative cut-free J-proof structures with the same conclusions; S Rel = S ′ Rel iff S -= S ′-.

Proof.

The proof can be obtained by a straightforward adaptation of the proof of injectivity of relational semantics for M LL proof nets given by Tortora de Falco in [START_REF] Tortora De Falco | Obsessional experiments for linear logic proof-nets[END_REF]. Such a property implies that the unique relational experiment of S (resp. S ′ ) allows to completely reconstruct S (resp S ′ ), up to jumps.

Lemma 7 Given a multiplicative J-proof structure S, a positive link a with typed conclusion x and a negative link b with typed conclusion y, b ≺ S a (that is, b precedes a in the order associated with S as a d.a.g.) iff for all experiments e of R, e(x) = 0 ⇒ e(y) = 0.

Proof. The proof is an easy consequence of definition of experiment.

Theorem 8 (Injectivity) Let S and S ′ be two cut-free multiplicative J-proof structures with the same conclusions. S = S ′ iff S = S ′ .

Proof.

The right to left direction is trivial.

Concerning the left to right direction, S = S ′ , so S Rel = S ′ Rel . Since S Rel = S ′ Rel , by lemma 6, S -= S ′-. Now, by remark 7 , given an element γ of S (resp. S ′ ) there exists a unique experiment e of S (resp. of S ′ ) such that |e| = γ. Now, we build from S -(resp. S ′-) a multiplicative J-proof structure S J (resp. S ′J ) in the following way; for any positive link a of typed conclusion x and for any negative link b of typed conclusion y, we check that for every element γ of S , given the unique experiment e of S (resp. S ′ ) induced by γ, e(x) = 0 ⇒ e(y) = 0; if it is the case and a is not above b in S -(resp. in S ′-) we make a jump on b. Using lemma 7, we can easily conclude that S J = S, and S ′J = S ′ (up to transitive jumps); since S = S ′ and S -= S ′-, S = S ′ .

Proposition 18 Let S be a multiplicative cut free J-proof structure and S ′ a multiplicative cut-free J-proof structure with the same conclusions as S. S ′ can be obtained by adding jumps on S iff S Rel = S ′ Rel and S ′ ⊆ S .

Proof.

The left to right direction is trivial.

Concerning the right to left direction, by lemma 6, S -= S ′-. Since S ′ ⊆ S , using lemma 7 we can say that all the jumps of S are jumps of S ′ . In order to obtain S, we just add to S all the jumps of S ′ which are not jumps of S; in this way we obtain a J-proof structure S J = S ′ . Injectivity, general case. Given a J-proof structure R with conclusions Γ, an index assignment of R is a function φ associating with any formula of type & I∈N ( i∈I (P i )) occurring in Γ a J ∈ N .

It is easy to check that if R is total, to any index assignment φ there is a unique slice S φ of R, and to each slice of R there is (at least one) index assignment φ.

Let us consider an element < J, δ > of ⊎ I∈N (⊛ i∈I (P * i )), interpretation of a formula & I∈N ( i∈I (P i )), and an element γ of the interpretation R of a total J-proof structure R with conclusions Γ; we say that γ is compatible with an index assignment φ on Γ iff for any occurrence of < J, δ > in γ, on the corresponding occurrence of & I∈N ( i∈I

(P i )) in Γ, φ(& I∈N ( i∈I (P i ))) = J.
Proposition 19 Given a total J-proof structure R, an element γ of R is compatible with an index assignment φ, iff γ is the result of an experiment on S φ .

Proof. Suppose γ is not the result of an experiment on S φ ; then it is the result of an experiment on another slice S ′ of R, which differs from S φ for at least one component of a & rule. But then it is easy to observe that γ cannot be compatible with S ′ . The other direction is trivial.

Proposition 20 Given a total J-proof structure R and an index assignment φ, S φ = {γ ∈ R |γ is compatible with φ}.

Proof. Easy consequence of proposition 19.

Theorem 9 (Injectivity) Let R and R ′ be two cut-free total J-proof structures with the same conclusions Γ.

R = R ′ iff R = R ′ .

Proof.

The right to left direction is trivial.

Concerning the left to right direction, let us take the slice S φ of R corresponding to the index assignment φ of Γ, and suppose S φ is not a slice of R ′ . By proposition 20

S φ = {γ ∈ R |γ is compatible with φ}. Since R = R ′ , {γ ∈ R |γ is compatible with φ} = {γ ∈ R ′ |γ
is compatible with φ}; then for the unique slice S ′φ of R ′ which corresponds to φ by proposition 20 S ′φ = {γ ∈ R ′ |γ is compatible with φ}, and S ′φ = S φ ; but then by theorem 8 S ′φ = S φ so S φ is a slice of R ′ , contradicting our hypothesis that S φ was not a slice of R ′ .

Proposition 21 Let R be a cut-free total J-proof structure and R ′ a cut-free total J-proof structure with the same conclusions as R. R ′ is obtained by adding jumps on R iff R Rel = R ′ Rel and R ′ ⊆ R .

Proof.

The left to right direction is trivial.

Concerning the right to left direction, we prove that for every slice S of R there exists a slice S ′ of R ′ such that S ′ is obtained from S by adding jumps.

Let us take the slice S φ of R corresponding to the index assignment φ of Γ, and suppose that for no slices S ′ of R ′ , S ′ is obtained by adding jumps on S φ ). By proposition 20 S φ = {γ ∈ R |γ is compatible with φ}, and S φ Rel = {γ ∈ R Rel |γ is compatible with φ}.

Since R Rel = R ′ Rel , then {γ ∈ R Rel |γ is compatible with φ} = {γ ∈ R ′ Rel |γ is compatible with φ} and since R ⊇ R ′ , {γ ∈ R |γ is compatible with φ} ⊇ {γ ∈ R ′ |γ is compatible with φ}; then for the unique slice S ′φ of R ′ which corresponds to φ by proposition 20 S ′φ = {γ ∈ R ′ |γ is compatible with φ}, and S ′φ Rel = {γ ∈ R ′ Rel |γ is compatible with φ}; so S ′φ Rel = S φ Rel , and S ′φ ⊆ S φ ; but then by proposition 18 S ′φ is obtained by adding jumps on S φ ), contradicting our hypothesis that for no slices S ′ of R ′ , S ′ is obtained by adding jumps on S φ ).

Similarly, we can prove that for every slice S ′ of R ′ there exists a slice S of R such that S ′ is obtained by adding jumps on S; but then it is immediate that R ′ can be obtained by adding jumps on R.

Correctness criterion is stable under reduction

Definition 31 Given two J-proof structures R 1 , R 2 with conclusions respectively Γ, P and ∆, P ⊥ , the composition of R 1 , R 2 is the J-proof structure with conclusion Γ, ∆ obtained by connecting R 1 , R 2 through a cut-link with premises P, P ⊥ .

Remark 9 If R 1 , R 2 are sequentializable then their composition R is sequentializable.

Proposition 22 Let R be the composition of two arborescent, weakly correct J-proof structures R 1 , R 2 ; then the normal form of R is arborescent.

Proof. The proof is a simple consequence of Proposition 14 and of the fact that the operation of superposition of J-proof structures preserves arborescence (as it can be easily verified).

Proposition 23 Let R 1 , R 2 be two sequentializable cut-free J-proof structures, and R be their composition. The normal form [R] of R is sequentializable.

Proof.

Since R 1 , R 2 are sequentializable they are J-proof nets by Theorem 1. Then we consider two saturations R ′ 1 , R ′ 2 of resp. R 1 , R 2 ; they are arborescent by the arborisation lemma. We take their composition R ′ . Now we reduce R to its normal form R 0 and R ′ to its normal form R ′ 0 . We show that the following diagram commutes (where vertical edges represents the addition of jumps, and horizontal edges stands for normalization).

R ----→ R 0     R ′ ----→ R ′ 0 Now by proposition 21, R ′ ⊆ R ; by Proposition 17 R = R 0 and R ′ = R ′ 0 , so R ′ 0 ⊆ R 0 . By Proposition 21 R ′
0 is obtained by adding jumps on R 0 and by Proposition 22 R ′ 0 is arborescent; So R ′ 0 is sequentializable by Proposition 9 and R 0 is sequentializable by Proposition 11.

Theorem 10 Let R 1 , R 2 be two cut-free J-proof nets, and R be their composition. The normal form [R] of R is a J-proof net.

Proof. A simple consequence of Proposition 23 and Theorem 1.

7 Are J-proof nets canonical objects?

So far, we have defined a syntax placed somehow in-between focusing, hypersequentialized proofs and proof nets, and we proved that the objects of such syntax have a good computational behaviour. We also proved that we can characterize hypersequentialized proofs in our setting as saturated J-proof nets, that is objects containing a maximal amount of sequential information. A natural question is then the following: if J-proof nets with "maximal" sequentiality correspond to HS proofs, what is the correspondent of a J-proof net with "minimal" sequentiality?

In this section we will try to answer to this question. First, in subsection 7.1 we will precisely define the notion of parallel J-proof net and we will consider if such an object can be considered canonical ; then in subsection 7.2 we will refine our analysis of parallel J-proof nets through the notion of monomiality, introduced by Girard in [START_REF] Girard | Proof-nets : the parallel syntax for proof-theory[END_REF]. Finally, in subsection 7.3 we will discuss the relation between J-proof nets and multifocalization (see [START_REF] Chaudhuri | Canonical sequent proofs via multi-focusing[END_REF]). For a thorough comparison between J-proof nets and polarized proof nets (see [START_REF] Laurent | Étude de la polarisation en logique[END_REF]) we refer instead to [Gia].

Parallel J-proof nets

Let us consider the following order relation on J-proof nets: given two J-proof nets R, R ′ we say that R is more sequential than R ′ (denoted by R ′ ≪ R) if R can be obtained from R ′ by adding jumps.

It is easy to see that the relation ≪ is a partial order on the set of J-proof nets, whose maximal elements are saturated J-proof nets; we call the mimal elements of the order parallel J-proof nets, defined as follows:

Definition 32 A parallel J-proof net is a J-proof net R such that, given any other J-proof net R ′ , cannot be obtained by adding jumps on R ′ .

Given two J-proof nets R 1 , R 2 , we say that R 1 is jump-permutable to R 2 (denoted R 1 ≈ R 2 ) iff, for some parallel J-proof net R, R ≪ R 1 and R ≪ R 2 ; informally R 1 ≈ R 2 if R 2 can be obtained from R 1 by "permutation of jumps", namely erasing jumps from R 1 to get R and then adding jumps to R to get R 2 .

Given a parallel J-proof net R let us consider the set of J-proof nets E = {R ′ |R ≪ R ′ }, that is the set of all J-proof nets that can be obtained from R by adding jumps.

We want to know if :

1. the relation ≈ is an equivalence relation;

2. E can be considered an "equivalence class" for ≈; 3. R can be considered a "canonical" representative of the J-proof nets in E.

A minimal requirement to satisfy these conditions would be the following: given any two parallel J-proof nets R 1 , R 2 , there must not be a J-proof net R 3 such that R 1 ≪ R 3 and R 2 ≪ R 3 . Unfortunately, this is not the case, as we can see in the following example.

Let us consider the parallel J-proof nets R 1 , R 2 resp. in fig. 29, 30. Both R 1 , R 2 are parallel: we cannot remove any jump from them without violating the contraction condition. The saturated J-proof net R 3 in fig. 31 can be obtained by adding jumps both on R 1 , R 2 , so R 1 ≪ R 3 and R 2 ≪ R 3 , but R 1 and R 2 are not comparable with respect to ≪. Moreover, since R 3 is saturated, it corresponds to an HS proof; so we can say that parallel J-proof nets fail to provide canonical representatives w.r.t HS proofs.

J-proof nets and monomiality

Let us try to clarify the reason behind the presence of two different J-proof nets representing the same HS proof with an example. In this example we will resort to boolean weights, a tool first introduced by Girard in [START_REF] Girard | Proof-nets : the parallel syntax for proof-theory[END_REF] to study the dependency relation on the links of a proof net induced by the presence of additives.

Let us consider the two J-proof nets R 1 , R 2 above. We can characterize the dependencies between the links and the &-rules in R 1 , R 2 in the following way: first we assign a boolean variable, p (resp q) to the leftmost (resp. rightmost) &-rule.

Then we label the links with boolean weights, in such a way that if a link a depends from the left component of the leftmost (resp. rightmost) &-rule then its weight contains the boolean variable p (resp. q); if instead a depends from the right component of the leftmost (resp. rightmost) &-rule then its weight contains the negation p (resp. q) of the boolean variable p (resp. q). Assigning a value among 1, 0 to each of the boolean variable p, q and erasing the links whose weight is equal to 0 yields a slice of R 1 (resp. R 2 ). In fig 32, 33 we represent the J-proof nets R 1 , R 2 labelled with boolean weights: we omit jumps, since we can retrieve them by looking at dependencies induced by the weights of links.

We can observe that all weights labelling R 1 , R 2 are monomials4 . Now we know from [START_REF] Hughes | Proof nets for unit-free multiplicative-additive linear logic[END_REF] that expressing additives dependencies trough monomials it is not enough to provide a unique canonical representative for sequent calculus proofs equivalent modulo permutation of rules; this explains why there cannot be a J-proof net "quotienting" R 1 , R 2 . Such a J-proof net should satisfy the non-monomial labelling provided in fig 34; but if we try to add the jumps in a way to satisfy the dependency relations induced by the non-monomial weights, we get the structure R represented in fig. 29 which does not satisfy the contraction condition.

It is worth noticing that each evaluation of the boolean weights in R, produce nevertheless a slice which is actually a multiplicative J-proof structure. An interesting point to develop (which we postpone to future work)

J-proof nets and multifocusing

In [START_REF] Chaudhuri | Canonical sequent proofs via multi-focusing[END_REF], Miller, Saurin and Chaudhuri have introduced a generalization of M ALL f oc , the multiplicative/additive fragment of Andreoli's focusing calculus ; in such a calculus it is possible to focus on more than one formula at a time, due to a rule called multifocalization. Such a rule has the following shape (we refer to [START_REF] Chaudhuri | Canonical sequent proofs via multi-focusing[END_REF] for a detailed description of the calculus):

⊢ Γ ⇓ ∆ ⊢ Γ, ∆ ⇑ [M F ]
where ∆ contains only positive formulas.

In the multifocusing calculus, as in M ALL f oc , the sequent has a stoup, (the part of the sequent after ⇓) which contains the formulas to be decomposed (bottom up) during focalization; but while in M ALL f oc the stoup contains a single formula, in the multifocusing calculus we may focus on more than one formula at a time. All the formulas under focus will then be decomposed until only negative formulas remain, which will be decomposed in the next negative phase until we reach their positive components; a new set of positive formulas to focus on then will be chosen and so on. An interesting feature of the multifocusing calculus is that it allows to graduate the "level" of focalization of a proof, depending on how many formulas are included in the stoup on an application of the M F rule. In the following we will show an example of how J-proof nets allow to capture such a "multifocalization" property.

For simplicity's sake we will restrict our examples to the multiplicative case; nevertheless, our argument is perfectly sound also in presence of additives.

Let us consider the following two focusing proofs, denoted respectively π 1 , π 2 (to stress the order of application of rules, we mark some of them with an integer), where the focus of the M F rule is a single formula:

1] ⊢⇓ 1 [M F ] ⊢ 1 ⇑ [⊥] ⊢ 1 ⇑⊥ [R⇓] ⊢ 1 ⇓⊥ [1] ⊢⇓ 1 [M F ] ⊢ 1 ⇑ [⊥] ⊢ 1 ⇑⊥ [R⇓] ⊢ 1 ⇓⊥ ⊢ 1, 1 ⇓ (⊥ ⊗ ⊥) [1] ⊢⇓ 1 [M F ] ⊢ 1 ⇑ [⊥] ⊢ 1 ⇑⊥ [R⇓] ⊢ 1 ⇓⊥ ⊢ 1, 1, 1 ⇓ ((⊥ ⊗ ⊥)⊗ ⊥) [1] ⊢⇓ 1 [M F ] ⊢ 1 ⇑ [⊥] ⊢ 1 ⇑⊥ [R⇓] ⊢ 1 ⇓⊥ [⊗] ⊢ 1, 1, 1, 1 ⇓ (((⊥ ⊗ ⊥)⊗ ⊥)⊗ ⊥) [M F ] ⊢ (((⊥ ⊗ ⊥)⊗ ⊥)⊗ ⊥), 1, 1, 1, 1 ⇑)
[R⇑] ⊢ (((⊥ ⊗ ⊥)⊗ ⊥)⊗ ⊥), 1, 1 ⇑ 1, 1)

[ 2 ] ⊢ (((⊥ ⊗ ⊥)⊗ ⊥)⊗ ⊥), 1, 1 ⇑ 1 1)

[R⇓] ⊢ (((⊥ ⊗ ⊥)⊗ ⊥)⊗ ⊥), 1, 1 ⇓ 1 1)

[1] ⊢⇓ 1 [M F ] ⊢ 1 ⇑ [⊥] ⊢ 1 ⇑⊥ [R⇓] ⊢ 1 ⇓⊥ [⊗ 2 ] ⊢ (((⊥ ⊗ ⊥)⊗ ⊥)⊗ ⊥), 1, 1, 1 ⇓ ((1 1)⊗ ⊥))
[M F ] ⊢ (((⊥ ⊗ ⊥)⊗ ⊥)⊗ ⊥), ((1 1)⊗ ⊥), 1, 1, 1 ⇑)

[R⇑] ⊢ (((⊥ ⊗ ⊥)⊗ ⊥)⊗ ⊥), ((1 1)⊗ ⊥), 1 ⇑ 1, 1)

[ 1 ] ⊢ (((⊥ ⊗ ⊥)⊗ ⊥)⊗ ⊥), ((1 1)⊗ ⊥), 1 ⇑ 1 1)

[R⇓] ⊢ (((⊥ ⊗ ⊥)⊗ ⊥)⊗ ⊥), ((1 1)⊗ ⊥), 1 ⇓ 1 1)

[1] ⊢⇓ 1 [M F ] ⊢ 1 ⇑ [⊥] ⊢ 1 ⇑⊥ [R⇓] ⊢ 1 ⇓⊥
[⊗ 1 ] ⊢ (((⊥ ⊗ ⊥)⊗ ⊥)⊗ ⊥), ((1 1)⊗ ⊥), 1, 1 ⇓ ((1 1)⊗ ⊥)

[M F ] ⊢ (((⊥ ⊗ ⊥)⊗ ⊥)⊗ ⊥), ((1 1)⊗ ⊥), ((1 1)⊗ ⊥), 1, 1

⇑ [1] ⊢⇓ 1 [M F ] ⊢ 1 ⇑ [⊥] ⊢ 1 ⇑⊥ [R⇓] ⊢ 1 ⇓⊥ [1] ⊢⇓ 1 [M F ] ⊢ 1 ⇑ [⊥] ⊢ 1 ⇑⊥ [R⇓] ⊢ 1 ⇓⊥ ⊢ 1, 1 ⇓ (⊥ ⊗ ⊥) [1] ⊢⇓ 1 [M F ] ⊢ 1 ⇑ [⊥] ⊢ 1 ⇑⊥ [R⇓] ⊢ 1 ⇓⊥ ⊢ 1, 1, 1 ⇓ ((⊥ ⊗ ⊥)⊗ ⊥) [1] ⊢⇓ 1 [M F ] ⊢ 1 ⇑ [⊥] ⊢ 1 ⇑⊥ [R⇓] ⊢ 1 ⇓⊥ [⊗] ⊢ 1, 1, 1, 1 ⇓ (((⊥ ⊗ ⊥)⊗ ⊥)⊗ ⊥)
[M F ] ⊢ (((⊥ ⊗ ⊥)⊗ ⊥)⊗ ⊥), 1, 1, 1, 1 ⇑)

[R⇑] ⊢ (((⊥ ⊗ ⊥)⊗ ⊥)⊗ ⊥), 1, 1 ⇑ 1, 1)

[ 1 ] ⊢ (((⊥ ⊗ ⊥)⊗ ⊥)⊗ ⊥), 1, 1 ⇑ 1 1)

[R⇓] ⊢ (((⊥ ⊗ ⊥)⊗ ⊥)⊗ ⊥), 1, 1 ⇓ 1 1)

[1] ⊢⇓ 1 [M F ] ⊢ 1 ⇑ [⊥] ⊢ 1 ⇑⊥ [R⇓] ⊢ 1 ⇓⊥ [⊗ 1 ] ⊢ (((⊥ ⊗ ⊥)⊗ ⊥)⊗ ⊥), 1, 1, 1 ⇓ ((1 1)⊗ ⊥))
[M F ] ⊢ (((⊥ ⊗ ⊥)⊗ ⊥)⊗ ⊥), ((1 1)⊗ ⊥), 1, 1, 1 ⇑)

[R⇑] ⊢ (((⊥ ⊗ ⊥)⊗ ⊥)⊗ ⊥), ((1 1)⊗ ⊥), 1 ⇑ 1, 1)

[ 2 ] ⊢ (((⊥ ⊗ ⊥)⊗ ⊥)⊗ ⊥), ((1 1)⊗ ⊥), 1 ⇑ 1 1)

[R⇓] ⊢ (((⊥ ⊗ ⊥)⊗ ⊥)⊗ ⊥), ((1 1)⊗ ⊥), 1 ⇓ 1 1)

[1] ⊢⇓ 1 [M F ] ⊢ 1 ⇑ [⊥] ⊢ 1 ⇑⊥ [R⇓] ⊢ 1 ⇓⊥ [⊗ 2 ] ⊢ (((⊥ ⊗ ⊥)⊗ ⊥)⊗ ⊥), ((1 1)⊗ ⊥), 1, 1 ⇓ ((1 1)⊗ ⊥)
[M F ] ⊢ (((⊥ ⊗ ⊥)⊗ ⊥)⊗ ⊥), ((1 1)⊗ ⊥), ((1 1)⊗ ⊥), 1, 1 ⇑

In π 1 , the first passage in the stoup decomposes the bipole (⊗ 1 , 1 ), and the second one the bipole (⊗ 2 , 2 ), while in π 2 the order of passages in the stoup is reversed. Each of these proofs directly corresponds to a J-proof net; since π 1 , π 2 are focusing, they correspond respectively to the saturated J-proof net R 1 in fig. 36 andR 2 in fig. 37 (for simplicity'sake, we label edges with formulas of M ALL and links with rules occuring in π 1 , π 2 ); in each of R 1 , R 2 we can observe how jumps tell the order in which bipoles will be decomposed through the stoup: at each step of sequentialization the minimal (w.r.t. the d.a.g. order) bipole of R 1 (resp. R 2 ) is the only splitting one. Figure 36: Multifocalization allows for a third possibility: to decompose both bipoles (⊗ 1 , 1 ), (⊗ 2 , 2 ) in the stoup at the same time, as in the following proof π 3 .

1 1 1 1 1 1 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ (1 1) (1 1) 1 ⊥ 1 1 ⊥ ⊥ ⊥ ⊥ 1 1 ⊥ 1 (( 1
1] ⊢⇓ 1 [M F ] ⊢ 1 ⇑ [⊥] ⊢ 1 ⇑⊥ [R⇓] ⊢ 1 ⇓⊥ [1] ⊢⇓ 1 [M F ] ⊢ 1 ⇑ [⊥] ⊢ 1 ⇑⊥ [R⇓] ⊢ 1 ⇓⊥ ⊢ 1, 1 ⇓ (⊥ ⊗ ⊥) [1] ⊢⇓ 1 [M F ] ⊢ 1 ⇑ [⊥] ⊢ 1 ⇑⊥ [R⇓] ⊢ 1 ⇓⊥ ⊢ 1, 1, 1 ⇓ ((⊥ ⊗ ⊥)⊗ ⊥) [1] ⊢⇓ 1 [M F ] ⊢ 1 ⇑ [⊥] ⊢ 1 ⇑⊥ [R⇓] ⊢ 1 ⇓⊥ [⊗] ⊢ 1, 1, 1, 1 ⇓ (((⊥ ⊗ ⊥)⊗ ⊥)⊗ ⊥)
[M F ] ⊢ (((⊥ ⊗ ⊥)⊗ ⊥)⊗ ⊥), 1, 1, 1, 1 ⇑)

[R⇑] ⊢ (((⊥ ⊗ ⊥)⊗ ⊥)⊗ ⊥) ⇑ 1, 1, 1, 1

[ 1 ] ⊢ (((⊥ ⊗ ⊥)⊗ ⊥)⊗ ⊥) ⇑ (1 1), 1, 1

[ 2 ] ⊢ (((⊥ ⊗ ⊥)⊗ ⊥)⊗ ⊥) ⇑ (1 1), (1 1)

[R⇓] ⊢ (((⊥ ⊗ ⊥)⊗ ⊥)⊗ ⊥) ⇓ (1 1), (1 1)

[1] ⊢⇓ 1 [M F ] ⊢ 1 ⇑ [⊥] ⊢ 1 ⇑⊥ [R⇓] ⊢ 1 ⇓⊥ [⊗ 1 ] ⊢ (((⊥ ⊗ ⊥)⊗ ⊥)⊗ ⊥), 1 ⇓ ((1 1)⊗ ⊥), 1 1) [1] ⊢⇓ 1 [M F ] ⊢ 1 ⇑ [⊥] ⊢ 1 ⇑⊥ [R⇓] ⊢ 1 ⇓⊥ [⊗ 2 ] ⊢ (((⊥ ⊗ ⊥)⊗ ⊥)⊗ ⊥), 1, 1 ⇓ ((1 1)⊗ ⊥), ((1 1)⊗ ⊥)
[M F ] ⊢ (((⊥ ⊗ ⊥)⊗ ⊥)⊗ ⊥), ((1 1)⊗ ⊥), ((1 1)⊗ ⊥), 1, 1 ⇑ Such a multifocalized proof π 3 directly corresponds to the J-proof net R 3 in fig. 38. In R 3 too, the minimal bipoles coincide exactly with the splitting ones, and in this case they are more than one: we can then sequentialize R 3 by removing at the same time both bipoles, decomposing them simultaneously in the stoup. The jumps originating from the middle ⊗ link tell that it must wait for both (⊗ 1 , 1 ), (⊗ 2 , 2 ) to be decomposed in order to enter the stoup. As a future research direction, we plan to deepen the study of the relation between multifocalization and J-proof nets, especially the connection between parallel J-proof nets and maximal multifocusing proofs.

1 1 1 1 1 1 ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ (1 1) (1 1) 1 ⊥ 1 1 ⊥ ⊥ ⊥ ⊥ 1 1 ⊥ 1 (( 1

  Outline of the paper . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2 Background 6 2.1 Hypersequentialized calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.1.1 From M ALL to HS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.1.2 HS syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.2 Preliminaries on graphs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.3 HS proofs as d.a.g.'s . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 3 J-proof nets 12 3.1 J-proof structures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 3.1.1 Totality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 3.1.2 Jumps and the additive structure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 3.1.3 Axiom links . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 3.2 J-proof structures and sequent calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 3.2.1 Sequentializable J-proof-structures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 3.3 Correctness criterion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 4 J-proof nets, L-nets and superposition 19 4.1 Adresses and ludification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 4.2 Sharing equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 4.3 Superposition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 5 Sequentializing with jumps 23 5.1 Arborescence and sequent calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 5.2 Sequentializing with jumps: the multiplicative case . . . . . . . . . . . . . . . . . . . . . . . . . . 24 5.3 Sequentializing with jumps: the additive case . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 5.4 Sequentializing with jumps: the general case . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 5.5 Sequentialization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 5.5.

  links a, b of R belong to the same & rule, then the label of a is -J∈N and the label of b is -J ′ ∈N and J = J ′ ; Coherence: given a link a and two negative links b, c, if a + -→ b and a + -→ c then b and c do not belong to the same & rule; Contraction: given two positive contracted links a, b, there exists an additive pair w 1 , w 2 s.t. a + -→ w 1 and b + -→ w 2 .

  then b, b ′ have the same type (and vice versa).

Figure 5 :

 5 Figure 5: An example of a J-proof structure with a "legal" cycle (marked in red), justified by a negative rule (marked in blue).

↑Figure 6 :

 6 Figure 6: An example of a J-proof structure with an "illegal" cycle (marked in red)

Figure 10 :

 10 Figure 9: A J-proof structure R 2 .

  but then by point 1) of definition 19 and by definition of sharing equivalence there exists a positive link b ∈ R such that b ≡ b ′ and b + -→ a, so R respects the positivity condition. Concerning coherence condition, let us consider a link a of R; by point 2) of definition 19, there exist a link a ′ in some R i s.t. a ≡ a ′ . Now it is easy to verify that, by definition 19, for all links b such that a

Figure 11 :Figure 12 :

 1112 Figure 11: The superposition of R 1 , R 2 .

  Figure 13:

  Figure 15:

  Figure 17: The J-proof net R 1

Figure 19 :

 19 Figure 19: The skeleton of R 1

Figure 20 :

 20 Figure 20: The skeleton of R 2

  net obtained from R by adding jumps. Definition 23 (Strong switching path) Given a negative link b of of a J-proof structure R, a strong switching path b, . . . , a from a node b to a node a is a switching path which does not use any switching edge of b (or of any other node b ′ belonging to the same &-rule as b in R).Proposition 12 Let a be a positive link, b a negative link and W any &-rule in a J-proof net R, s.t. b depends from W . If there isn't any strong switching path from b to a in R, then there isn't any strong switching path from w to a in R for any element w of W .

  by a single switching cycle C; by the correctness criterion, there exists an additive pair w 1 , w 2 ∈ W which breaks C in R . Let's suppose by absurd that every link of C is above either w 1 or w 2 ; then we can partition the nodes of C in two sets, A = {a : a + -→ w 1 } and B = {b : b + -→ w 2 }, disjoint by condition coherence of the definition of J-proof structure. Given any two elements a ∈ A and b ∈ B, there exists a path r : a . . . b connecting them. We consider the first edge of r starting from a which connects a node d of A with a node d ′ of B; either it is an incident edge d → d ′ , and then d + -→ w 1 and d + -→ w 2 , or it is an emergent edge d ← d ′ , and then d ′ +

1Figure 22 :Figure 23 :

 2223 Figure 22: Case 1 in the proof of the arborisation lemma

Remark 4

 4 Consider an hidden negative link a of a persistent slice S and its opposite link b; a and b belongs to two different branches of the same cut-link c. Now if there are two links a ′ , b ′ in S such that a ′ + -→ a and b + -→ b ′ and a ′ , b ′ are not hidden by c, then by definition of + I∈N /-I∈N step, by proposition 14 and by definition of opposite link, there is a slice S ′ obtained by reducing S such that in S ′ a ′ + -→ b ′ .

  (b) otherwise, there exists a negative hidden link d of R s.t. c + -→ d for the parent c of w jn , w kn in R. Since both S j , S k contains c, we can apply lemma 5 to obtain a maximal sequence c 1 , d 1 , . . . c n , d n of links of R, as descripted in the statement of lemma 5. Let us consider the last element c n , d n of the sequence. There are two possibilities: i. If the opposite positive link d ′ of d n in S j and the opposite positive link d ′′ of d n in S k are two

+-→ w 1

 1 and b + -→ w 2 , then a, b cannot be contracted in R (by contraction condition); so a, b must be two different occurrences of the same link c of R in S j , S k . Then we can apply lemma 5 to obtain a sequence c 1 , d 1 , . . . c n , d n of link of R, as descripted in the statement of lemma 5. Such a sequence must terminate with an element c n , d n such that the opposite positive link d ′ of d n in S j and the opposite positive link d ′′ of d n in S k are two different contracted links of R (otherwise, a would be sharing equivalent to b in S ′ j , S ′ k , contradicting the assumption that a, b are sibling in S ′ j , S ′ k ). But then by contraction condition on R there exists a negative link w ′′ j in S j and a negative link w ′′ k in S k such that w ′′ j , w ′′ k form an additive pair in R and d ′ + -→ w ′′ j in S j (resp. d ′′ + -→ w ′′ k in S k ). By remark 4 and theorem 5 it follows that in S ′ j a + -→ w ′′ j and that b + -→ w ′′ k in S ′ k . Now we replicate on w ′′ j , w ′′ k the same procedure from the beginning of point 1. (replacing w j , w k with w ′′ j , w ′′ k and a, b with d ′ , d ′′ ), iterating the applications of lemma 4 and lemma 5 until by finiteness of R we eventually found a proper visible additive pair of R.

  Figure 28: example of experiment

Figure 29

 29 Figure 29: a parallel J-proof net R 1

Figure 31 :

 31 Figure 30: a parallel J-proof net R 2

Figure 32 :Figure 33 :

 3233 Figure 32: R 1 labelled with boolean weights

Figure 35 :

 35 Figure 34: Non-monomial labelling

[

  Figure 37:

[

  Figure 38:

  1 A saturated J-proof net is switching acyclic. . . . . . . . . . . . . . . . . . . . . . . . . . . 32 5.5.2 A saturated J-proof net is arborescent. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 5.5.3 J-proof nets and Mix rule . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Cut and sequentialization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 6.2 Cut elimination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 6.2.1 Cut elimination on J-proof structures: the multiplicative case . . . . . . . . . . . . . . . . 36 6.2.2 Cut elimination on J-proof structures: the general case . . . . . . . . . . . . . . . . . . . . 38 6.2.3 Preservation of weakly correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 6.3 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 6.3.1 Experiments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 6.3.2 Injectivity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 6.4 Correctness criterion is stable under reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 Parallel J-proof nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 7.2 J-proof nets and monomiality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 7.3 J-proof nets and multifocusing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50

	6 Cut elimination and semantics	35
	6.1 7 Are J-proof nets canonical objects?	48
	7.1

It is not possible that adding a jump having has target b in R increases the number of strong switching paths starting from b in R ′ since such paths cannot use the switching edges of b (and a jump is a switching edge).

Given a proper weight algebra (which takes into account the possible presence of n-ary &-rules), this observation is easily generalized to all J-proof structures; we left the details to the reader.

Acknowledgements

The author is indebted with Jean-Yves Girard, for having first suggested the idea of sequentializing with jumps. This paper relies on a huge amount of work and discussions with Claudia Faggian; I would like to thank her for all her support. Thanks to Pierre Boudes, Damiano Mazza and Lorenzo Tortora de Falco for many useful comments and insights.