Roberto Maieli
email: maieli@mat.uniroma3.it

Non decomposable connectives of linear logic

Keywords: linear logic, partitions sets, proof nets, sequent calculus. 2010 MSC: 03F52, 03B47 Undecomposable entangled connectives . . . . . . . . . . . . . 34

This paper studies the so-called generalized multiplicative connectives of linear logic, focusing on the question of finding the "non-decomposable" ones, i.e., those that may not be expressed as combinations of the default binary connectives of multiplicative linear logic, ⊗ (tensor) and (par). In particular, we concentrate on generalized connectives of a surprisingly simple form, called "entangled connectives", and prove a characterization theorem giving a criterion for identifying the undecomposable ones.

Introduction

Generalized connectives for the pure (units free) multiplicative fragment of linear logic (MLL, [START_REF] Girard | Linear Logic[END_REF]) were introduced by Girard in his seminal paper [START_REF] Girard | Multiplicatives[END_REF] in terms of permutations but most of the results known after then are essentially due to Danos and Regnier [START_REF] Danos | The structure of multiplicatives[END_REF] who replaced permutations by partitions of finite sets. A generalized multiplicative connective may be defined by a pair of dual sets of partitions of a same finite domain {1, 2, ...n}, dual in the sense that they are pairwise orthogonal where orthogonality is defined by a topological condition: the bipartite graph obtained by linking together classes of each partition sharing an element is acyclic and connected (ACC). E.g., partition {(1, 2), (3)} is not orthogonal to partition {(1, 2, 3, )} since the bipartite graph G 1 contains a cycle while the two sets of partitions, {{(1, 2), (3)}} and {{(1, 3), (2)}, {(1), (2, 3)}}, are orthogonal since they are pairwise so (their respective bipartite graphs, G 2 and G 2 , are ACC) as illustrated below:

(1, 2) [START_REF] Danos | The structure of multiplicatives[END_REF] (1, 2, 3)

G 1 : (1, 2) (3) (1, 3) (2) G 2 : (1, 2) (3) (1) (2, 3) G 2 :
There are two ways to interpret logical connectives (formulas) of MLL by means of pairs of orthogonal sets of partitions: one based on the sequent calculus syntax and the other one based on the proof nets syntax, according to the spirit of linear logic. In the sequential syntax, a partition describes a sequent calculus rule for producing the generalized formula: the domain of the partition is the set of principal sub-formulas occurrences of the given formula and each class describes one premise of the rule; so, a multiplicative rule for an n-ary connective F (A 1 , ..., A n ) is completely characterized by the organization of its principal sub-formulas (A 1 , ..., A n ); indeed, since multiplicatives rules are unconditional about the context, any rule can be simply described by a partition over its principal sub-formulas occurrences (their indexes), omitting the contexts. E.g., the two orthogonal sets of partitions (or organizations sets), O F = {{(1, 2), (3)}} and O F ⊥ = {{(1, 3), (2)}, {(1), (2, 3)}}, are compact representations of, respectively, the sequent generalized rule below (when

F (1, 2, 3) = (A 1 A 2 ) ⊗ A 3 ) (1, 2) (3) r(F ) F (1, 2, 3) ≡ (1, 2) (1 2) (3) ⊗ F = (A 1 A 2 ) ⊗ A 3
and the next two sequent n-ary rules (when F ⊥ (1, 2, 3) = (A 1 ⊗ A 2 ) A 3 ): [START_REF] Andreoli | Focussing and Proof Construction[END_REF][START_REF] Danos | The structure of multiplicatives[END_REF] (2)

r 1 (F ⊥ ) F ⊥ (1, 2, 3) ≡ (1, 3) (2) ⊗ (1 ⊗ 2), 3 F ⊥ = (A 1 ⊗ A 2 ) A 3 (1)
(2, 3)

r 2 (F ⊥ ) F ⊥ (1, 2, 3) ≡ (1) (2, 3) ⊗ (1 ⊗ 2), 3 F ⊥ = (A 1 ⊗ A 2 ) A 3
In the graphical syntax, a partition describes the "effects" of a Danos-Regnier switching over the frontier of the syntactical tree of a MLL formula. We may associate to each switching of a formula tree F (A 1 , ..., A n ) a partition of its top frontier A 1 , ..., A n in to classes of connected components. The partitions set of the border leaves of a formula tree F , induced by all switchings, is called the pre-type of F (denoted P F ). E.g., the pre-types the two formula trees below are resp., the partitions set P F = {{(1, 3), (2)}, {(1), (2, 3)}} (pre-type of F = (A 1 A 2 ) ⊗ A 3 ) and the partitions set P F ⊥ = {{(1, 2), ( 3)}} (pre-type of

F ⊥ = (A 1 ⊗ A 2 ) A 3 ).
These two syntaxes describing usual MLL formulas (i.e., definable by means of the basic binary connectives ⊗ and ) are shown to be dual. To be precise, the organizations set of a MLL formula F (denoted O F ) is exactly the dual of the pre-type of F that is, O F = P ⊥ F so, O F is a type (i.e. it is equal to its bi-orthogonal, O F = O ⊥⊥ F ), thus every sequential n-ary connective of MLL, O F and O F ⊥ , is reflexive that is O ⊥ F = O F ⊥ and O ⊥ F ⊥ = O F . We can generalize this construction in a natural way. Given two partitions sets we wonder whether they define a generalized multiplicative connective according to the two dual syntaxes:

• in the sequent calculus syntax it is sufficient to describe a connective1 as a pair of orthogonal organizations sets O C ⊥ O C ⊥ ; each organizations set is a type describing all rules that allow to derive that connective; orthogonality is enough to ensure cut elimination;

• in the proof nets syntax, since partitions are interpreted as switchings associated to a connective and since switchings are in some sense dense sub-sets 2 we may define a connective as a pairs of partitions sets P and Q s.t. P ⊥ Q and P ⊥ ⊥ Q ⊥ : the first condition P ⊥ Q ensures (ACC) correctness of proof structures while the second condition P ⊥ ⊥ Q ⊥ ensures the stability of correctness under cut reduction.

Then, given a pair of partitions sets, P and Q, as describing a connective (in sequential or graphical syntax), we wonder whereas this connective is definable by means of the basic binary connective of MLL ( and ⊗) in which case it is called decomposable. Not all connectives are decomposable. To date there only exists one instance of non (binary) decomposable connective firstly discovered by Girard [START_REF] Girard | Multiplicatives[END_REF] in terms of permutations and later reformulated by Danos-Regnier [START_REF] Danos | The structure of multiplicatives[END_REF] as a pair of orthogonal sets of partitions, G 4 and G ⊥ 4 , over the same domain {1, 2, 3, 4}: Unfortunately, none (uniform) characterization of undecomposable connectives is known up to now. Under this respect, this work represents a first step forward: it defines a class of generalized connectives that are not decomposable, neither in sequential nor in graphical syntax, the so-called undecomposable entangled connectives. A pair of distinct partitions sets with same domain and same weight (cardinality) is entangled when each partition contains only binary or unary classes (Definition 21). Then a connective, P and Q, is entangled whenever P or Q is an entangled pair. Entangled pairs have interesting properties that are investigated throughout Section 4. The first one (Theorem 32, one of the main results of the paper), being that every entangled pair of partitions sets is a type. This result has several consequences: decomposable entangled pairs (and so, decomposable connectives) have a very simple characterization (the normal form of Theorem 36) which can be further used to prove that given an undecomposable entangled connective, P and Q, where P is an entangled pair, then P cannot be embedded into a decomposable type T P , s.t. T and Q become decomposable (see Corollary 40).

Although our notion of entanglement doesn't solve the admittedly, difficult general problem ("try to find an uniform characterization of the full class of undecomposable connectives"), it is far from being and "ad hoc" condition. Intuitively, an entangled type is naturally obtained as soon as we "superpose" (i.e., we sum) the pre-types of two bipoles3 having the same "skeleton" (i.e., the same abstract syntactical tree) up to cyclic permutation of their frontier (the border leaves; see Remarks 41). This fact is a novelty since the union of types is not in general a type while the intersection of types is always a type (Property 3 of Section 2). Indeed, entangled types are the smallest types (w.r.t. the number of partitions), if we exclude the trivial singleton types. So, entangled connectives can be considered, in some sense, "elementary connectives", since they are the "smallest" generalized multiplicative connectives (w.r.t. the number of switchings or the number of sequential rules), if we exclude, of course, the basic ones ( and ⊗). However, the class of undecomposable entangled connectives is quite special and we already discovered examples of undecomposable connectives falling outside of it like e.g. G 9 below (we omit the dual G ⊥ 9 ): [START_REF] Ehrhard | A new correctness criterion for MLL proof nets[END_REF][START_REF] Girard | Multiplicatives[END_REF][START_REF] Girard | Linear Logic[END_REF], [START_REF] Girard | On the meaning of logical rules I: syntax vs. semantics[END_REF][START_REF] Girard | Le point aveugle[END_REF][START_REF] Maieli | Modularity of proof nets: generating the type of a module[END_REF]}, {(2, 3, 4), [START_REF] Girard | Multiplicatives[END_REF][START_REF] Girard | Linear Logic[END_REF][START_REF] Girard | On the meaning of logical rules I: syntax vs. semantics[END_REF], (8, 9, 1)}, {(3, 4, 5), [START_REF] Girard | Linear Logic[END_REF][START_REF] Girard | On the meaning of logical rules I: syntax vs. semantics[END_REF][START_REF] Girard | Le point aveugle[END_REF], (9, 1, 2)} }.

G 9 = { {(1, 2, 3),
We are currently working on a more general characterization 4 of the full class of primitive non decomposable connectives i.e., those ones that cannot be defined by means of other connectives, neither binary nor entangled. More generally, non decomposable generalized connectives witness a deep asymmetry between proof nets and sequent proofs since the former ones allow us to express a kind of parallelism of proofs that the latter ones cannot do: actually, there exist proof nets in η-expanded form, built on non decomposable connectives, that have no correspondence with any sequential proof, if we exclude the identity axioms G, G * . This significant fact, lying at the core of linear logic, was already remarked in [START_REF] Danos | The structure of multiplicatives[END_REF]: "We saw with some surprise that the realm of multiplicatives became quite complex, even handled by a careful generalization. Yet the generalization seems more natural in the non-sequential framework [...]. Maybe we witness here the limits of sequential presentations of logic".

Partitions and orthogonality

Definition 1 (partitions and orthogonality). A partition of a finite set X = {1, ..., n} (also called support) is a set of nonempty subsets of X, called classes (or parts), such that every element i ∈ X is in exactly one of these subsets (i.e., X is a disjoint union of the subsets).

If p and p * are two partitions of X = {1, ..., n}, then:

• the induced graph of incidence of p and p * , denoted G(p, p * ), is the bipartite (undirected) graph which has for vertices the classes of p and p * , two of them being linked iff they share an element i ∈ X;

• p and p * are orthogonal (denoted, p ⊥ p * ) iff the induced graph G(p, p * ) is acyclic and connected (i.e., it is a topological tree; shortly, ACC).

If P and Q are two sets of partitions, we say that P and Q are orthogonal (denoted P ⊥ Q) if they are pointwise orthogonal i.e., ∀p ∈ P, ∀q ∈ Q, p ⊥ q. P ⊥ denotes the set of partitions orthogonal to all the elements of P .

Example 2. Given two partitions,

p 1 = {(1, 2)} and p * 1 = {(1), (2)}) then, p 1 ⊥ p * 1 since the induced graph G 1 (p 1 , p * 1 ) is a tree; conversely, partitions p 2 = {(1), (2, 3)}) and p * 2 = {(1, 2, 3)} are not orthogonal (p 2 ⊥ p * 2 ) since G 2 (p 2 , p *
2 ) contains a cycle as illustrated in Figure 1. Moreover, observe that w.r.t the sets of partitions given below, P 1 , P 2 , Q 1 and Q 2 , we only have 1), (4)}, {(2, 4), (1), (3)}} 3), (4)}, {(3, 4), ( 2), (1)}, {(3, 1), ( 2), (4)}}.

P 1 ⊥ Q 1 and P 2 ⊥ Q 2 while e.g. P 1 ⊥ Q 2 and P 2 ⊥ Q 1 : P 1 = {{(1, 2), (3, 4)}}, Q 1 = {{(1, 3), (2), (4)}, {(1, 4), (2), (3)}, {(2, 3), (
P 2 = {{(2, 3), (4, 1)}}, Q 2 = {{(2, 4), (3), (1)}, {(2, 1), (
(1) [START_REF] Cockett | Weakly Distributive Categories[END_REF] (1, 2) The degree of a class x is the cardinality of x; the weight of a partition p is the cardinality of p. Given a set of partition P , we say that:

G 1 : p * 1 : p 1 : (1) (2, 3) G 2 : p 2 : p * 2 :(1, 2 , 3)
-P has weight w if every partition p ∈ P has weight w; -the size of P is the cardinality of P ; -the dimension of P is the cardinality of its domain X.

As notation, we use: variables X, Y, Z, ..., for finite sets {1, ...n}, variables a, b, c, ..., for arbitrary elements of sets, variables p, q, r, ..., for partitions of a set, variables x, y, z, ..., for classes of a partition and variables A, B, P, Q, ..., for sets of partitions.

Next facts on partitions sets of (Property 3) can be found in the literature on multiplicatives (see e.g. [START_REF] Maieli | Modularity of proof nets: generating the type of a module[END_REF] for detailed proofs).

Property 3 (partitions and types). Let A, B and A i be sets of partitions over {1, ..., n}. Then the following facts hold:

1. A ⊥ B iff A ⊆ B ⊥ iff B ⊆ A ⊥ ; 2. A ⊆ B implies B ⊥ ⊆ A ⊥ ; 3. A ⊆ A ⊥⊥ ; 4. A ⊥ B iff A ⊥⊥ ⊥ B ⊥⊥ ; 5. A ⊥ = A ⊥⊥⊥ ; 6. (A ⊥ B and A ⊥ ⊥ B ⊥ ) iff (A ⊥ = B ⊥⊥ ) iff (B ⊥ = A ⊥⊥ ); 7. In case A ⊥ B and A ⊥ ⊥ B ⊥ : (B ⊥ = A and B = A ⊥ ) iff (A ⊥⊥ = A and B = B ⊥⊥ ); 8. A = A ⊥⊥ iff ∃B : A = B ⊥ ; then, A is called type; 9. ( i A i ) ⊥ = i A ⊥ i ; 10. ( i A i ) ⊥ ⊇ i A ⊥ i ; 11.
if A is a singleton (i.e., A = {p} where p is a partition) then A is type; 12. if A ⊥ B, with A and B nonempty, then all partitions in A (resp., in B) have the same weight.

Let us prove case 6 of Property 3: assume (A ⊥ B) and (A ⊥ ⊥ B ⊥ ) then, by case 1, (A ⊥ ⊥ B ⊥ ) ⇒ (A ⊥ ⊆ B ⊥⊥ ) and (A ⊥ B) ⇒ (A ⊆ B ⊥ ) which implies, by case 2, B ⊥⊥ ⊆ A ⊥ ; so B ⊥⊥ = A ⊥ . Vice-versa assume B ⊥⊥ = A ⊥ then, by case 1, (A ⊥ ⊆ B ⊥⊥ ) ⇒ (A ⊥ ⊥ B ⊥ ) and, by case 3, (B ⊥⊥ ⊆ A ⊥ ) ⇒ (B ⊆ A ⊥ ) from which, by case 1, (A ⊥ B).

We draw attention to the fact that the intersection of types is always a type (case 9) while the union of types is not always a type (case 10): instances of these facts can be found in Example 5.

Case 11 follows by Lemma 4 of [START_REF] Maieli | Modularity of proof nets: generating the type of a module[END_REF]. Finally, case 12 follows by the next well known graph theoretical property (see e.g. [START_REF] Girard | Le point aveugle[END_REF], pages 250-251). Example 5. Assume two sets of partitions P 1 and P 2 over {a, b, c, d} as below then, we can calculate their respective orthogonal types, by case 9 of Property 3, as follows: Concerning case 10 of Property 3, we just observe here that although every singleton {p i } is a type (with i = 1, 2, by case 11 of Property 3), only P 1 is a type while P 2 is not so, since P 2 P ⊥⊥ 2 = (P 1 ∪ P 2 ). We will show in Section 4.1 that as soon as we restrict to consider pairs of singleton sets of partitions, {p} and {q}, having same domain and weight and whose classes have degree 1 ≤ d ≤ 2 then, their union {p} ∪ {q} is a(n entangled) type.

1. if P 1 = {p 1 : {(a, c), (b, d)}, p 2 : {(a, d), (b, c)}} then, P ⊥ 1 = {p 1 } ⊥ ∩ {p 2 } ⊥ = {{(d, c), (

Generalized connectives

Partitions sets allow to express generalized multiplicative connectives in a very abstract, uniform and compact way. A generalized (or n-ary) multiplicative connective C(A 1 , ..., A n ) may be defined, as in [START_REF] Danos | The structure of multiplicatives[END_REF], by a pair of orthogonal sets of partitions, P ⊥ Q, over a same domain {1, ..., n} that is the set of principal sub-formulas indexes of C. There are indeed two dual ways to interpret (orthogonal pairs of) sets of partitions as defining logical connectives: the sequential (Section 3.1) and the graphical one (Section 3.2).

Sequent calculus syntax for generalized connectives

Following [START_REF] Danos | The structure of multiplicatives[END_REF], we may define a connective by means of its sequential rules which are conservative w.r.t. the atoms i.e, the premises of the rule have exactly the same atoms as in the conclusion. Hence a multiplicative rule for an n-ary (i.e., generalized) connective C(A 1 , ..., A n ) is completely characterized by the organization of its principal sub-formulas occurrences (A 1 , ..., A n ) as described in the l.h.s. picture of Figure 2. Since multiplicatives rules are unconditional about the context, any rule can be simply described by a partition over its principal sub-formulas indexes, omitting the contexts Γ 1 , ..., Γ p , as in the r.h.s. picture of Figure 2 Definition 6 (generalized rules as partitions). If R is an n-ary rule, then the corresponding partition p is defined over {1, ..., n} as follows: i, j ∈ {1, ..., n} belong to a same class of p if formulas occurrences A 1 and A j belong to the same premise of R. Conversely, given a partition p, we can check if a rule R satisfies it. Renumber the principal formulas from left to right in the conclusions, and ask if the induced partition is really p. E.g., the two orthogonal sets of partitions, {{(1), (2)}} and {{(1, 2)}}, correspond to the primitive (or basic) binary multiplicative connectives " " and "⊗" of MLL [START_REF] Girard | Linear Logic[END_REF]:

Γ, A 1 ∆, B 2 ⊗ Γ, ∆, ⊗(A 1 , B 2 ) Γ, A 1 , B 2 Γ, (A 1 , B 2 )
Orthogonality ensures cut elimination; e. we cannot actually reduce the cut between D(A 1 , A 2 , A 3 ) and D * (A ⊥ 1 , A ⊥ 2 , A ⊥ 3 ), introduced just above by rules p and p * , by means of cuts between each couple of dual sub-formulas5 , A i and A ⊥ i :

. . .

Γ, A 1 , A 2 . . . ∆, A 3 p Γ, ∆, D(A 1 , A 2 , A 3 ) . . . Σ, A ⊥ 1 , A ⊥ 2 , A ⊥ 3 p * Σ, D * (A ⊥ 1 , A ⊥ 2 , A ⊥ 3 ) π : cut Γ, ∆, Σ
If we denote M LL + the standard MLL sequent calculus of Figure 3 extended with the sequential general multiplicative rules of Figure 2 then, M LL + still satisfies cut elimination 6 .

id A, A ⊥ Γ, A ∆, A ⊥ cut Γ, ∆ Γ, A ∆, B ⊗ Γ, ∆, A ⊗ B Γ, A, B Γ, A B
1. if p ∈ O C (resp., q ∈ O C * ) then F (resp., F ⊥ ) is provable in MLL, from
p (resp., from q), by only means of the binary rules, and ⊗; 2. if p (resp., q) is a partition from which we can derive F in MLL (resp., F ⊥ ) by only means of binary rules, then

p ∈ O C (resp., q ∈ O C * ). Example 9. The generalized connective (O Y , O Y * ) below is decomposable for Y = (1 2) ⊗ 3 ⊗ 4 and Y * = (1 ⊗ 2) 3 4: O Y = {p : {(1, 2), (3), (4)}} O Y * = {q 1 : {(1, 3, 4), (2)}, q 2 : {(2, 3, 4), (1)}, q 3 : {(1, 3), (2, 4)}, q 4 : {(1, 4), (2, 3)}} 1, 2 3 4 p Y (1, 2, 3, 4) 1, 3, 4 2 q 1 Y * (1, 2, 3, 4) 2, 3, 4 1 q 2 Y * (1, 2, 3, 4) 1, 3 2, 4 q 3 Y * (1, 2, 3, 4) 1, 4 2, 3 q 4 Y * (1, 2, 3, 4)
Remarks 10 (The packaging problem). "Partitions of a decomposable connective X and X ⊥ do not describe all proofs involving it, but only those ones that are independent from the context" [START_REF] Danos | The structure of multiplicatives[END_REF]. E.g., assume we want to prove a sequent S with only two conclusions, 2)}}) or we build S stepwise by exploiting the decomposition of D (resp., D * ). Clearly the latter method is more powerful since there are proofs, like the one below, that cannot be derived by the former one. Last rule for D (reps., for D * ) cannot be binary (i.e., with two premises) because any attempt to derive S would build a premise with the other conclusion D ⊥ (resp., D) together with only some (not all) of the principal formulas, A, B and C (resp., A ⊥ , B ⊥ , C ⊥ ): such sequents are never derivable from atomic logical axioms.

D = (A 1 B 2 ) ⊗ C 3 and D * = (A ⊥ 1 ⊗ B ⊥ 2 ) C ⊥ 3 then, either we introduce D (resp., D * ) only by its sequential rules O D = {(1, 2), (3)} (resp., O D * = {{(1), (2, 3)}, {(1, 3), (
A, A ⊥ B, B ⊥ ⊗ A, B, (A ⊥ ⊗ B ⊥ ) (A B), (A ⊥ ⊗ B ⊥ ) C, C ⊥ ⊗ (A B) ⊗ C, (A ⊥ ⊗ B ⊥ ), C ⊥ (A B) ⊗ C, (A ⊥ ⊗ B ⊥ ) C ⊥ ≡ A, A ⊥ B, B ⊥ ⊗ A, B, (A ⊥ ⊗ B ⊥ ) C, C ⊥ D (A B) ⊗ C, (A ⊥ ⊗ B ⊥ ), C ⊥ (A B) ⊗ C, (A ⊥ ⊗ B ⊥ ) C ⊥
In other words, all the binary rules yielding a decomposable connective X (resp., X ⊥ ) in the sequent calculus can be packed in an single rule iff these rules can be permuted in order to appear consecutively (as a "package").

Proof nets syntax for generalized connectives

Dually w.r.t. the sequential view, we may define a connective by means of its internal behavior that is, by means of the the set of partitions induced over its border by the set of switchings (i.e., internal tests) as in [START_REF] Danos | The structure of multiplicatives[END_REF].

Definition 11 (graphical generalized connectives). A generalized multiplicative connective in graphical syntax consists of two sets of partitions, P and Q, over the same domain {1, ..., n}, s.t. P ⊥ Q and

P ⊥ ⊥ Q ⊥ .
Dually to the sequential case, P = {{(a), (b)}} and Q ⊗ = {{(a, b)}} denote the basic connectives " " and "⊗". In the following, unless differently declared, the expression "generalized connectives" means "generalized connectives in the graphical setting" according to Definition 11.

Decomposable graphical connectives

Definition 12 (Danos-Regnier switchings, pre-types and types). Let F be a MLL formula built by the binary multiplicative connectives and ⊗ from its top border X (i.e. the literals of F ); given the parse (or syntactical) tree of F , a Danos-Regnier-switching [START_REF] Danos | The structure of multiplicatives[END_REF] of F is the graph obtained after the mutilation of one of the two premises for each node of F ; then the pre-type of F , denoted by P F , is given by the set of partitions over X induced by all DR-switchings of the parse tree of F . After the mutilation, the elements of the border belonging to a same connected component, constitute a class of the induced partition. We denote T F the type P ⊥⊥ F of F .

Definition 13 (decomposable connectives). A connective (P, Q), is MLL binary decomposable (or definable) iff there exists a formula F , only built with binary connectives of MLL, s.t. P is the pre-type of the parse tree of F and Q is the pre-type of the tree of the dual formula F ⊥ .

In the following we say that a set of partitions P is decomposable if there exists a formula F , s.t. P is the pre-type of F (i.e., P = P F ). Next Fact 14 on decomposable sets of partitions corresponds to Theorem 7 of [START_REF] Maieli | Modularity of proof nets: generating the type of a module[END_REF].

Fact 14 (orthogonal of a decomposable set of partitions). If F is a MLL formula then, P ⊥ F = T F ⊥ . Remarks 15 (expressiveness of the graphical syntax). Connectives defined according to Definition 11 are very expressive. Given a set of partitions P there exists a connective (P, Q) for every Q s.t. Q ⊥⊥ = P ⊥ , by case 6 of Property 3. E.g., given (the type) [START_REF] Cockett | Weakly Distributive Categories[END_REF][START_REF] Ehrhard | A new correctness criterion for MLL proof nets[END_REF], (5)}}, there exist at least two graphical connectives, as follows:

P = {p 1 = {(1, 2), (3, 4), (5)}, p 2 = {(1, 3),
1. (P, P ⊥ ) where, by case 9 of Property 3, P ⊥ = {p 1 } ⊥ ∩ {p 2 } ⊥ is the set of flagged partitions below:

{p 1 } ⊥ : (145) (3) (2) (135) (4) (2) (235) (4) (1) (245) (3) (1) (45) (13) (2) (25) (13) (4) (25) (14) (3) (35) (14) (2) (15) (23) (4) (15) (24) (3) (45) (23) (1) (35) (24) (1)
{p 2 } ⊥ : (145) (2) (3) (125) (4) (3) (325) (4) (1) (345) (2) (1) (45) (12) (3) (35) (12) (4) (35) (14) (2) (25) (14) (3) (15) (32) (4) (15) (34) (2) (45) (32) (1) (25) (34) (1)
2. (P, R) with R = {{(1, 4, 5), ( 2), (3)}, {(3, 2, 5), ( 4), (1)}} P ⊥ (s.t. R ⊥⊥ = P ⊥ ).

Proof structures with generalized links

A generalized multiplicative proof structure is a graph which has for edges formulas of M LL + and for vertices links depicted on the l.h.s. of Figure 4 and defined as follows:

• an axiom link, is a vertex with only a pair of dual atomic conclusions (incident edges), {{(a, a ⊥ )}};

• a cut link, is a vertex with only a pair of dual premises (incident edges), {{(A, A ⊥ )}};

• a generalized link P , denoted λ P , is a vertex with premises A 1 , ..., A n≥2 and exactly one conclusion F (A 1 , ..., A n ) (also denoted by the special symbol ) where (P, Q) is a generalized connective with domain 1, .., n and a bijection ϕ : i → A i ; λ P is immediately given together with its dual link λ Q . We assume there exactly is a generalized link for each connective. In a proof structure, each formula is conclusion of exactly one link and premise of at most one link; in the special case of the conclusions of a proof structure, i.e., formulas that are not premises of any link, we add an handling vertex (in order to have a graph). Not all proof structures are correct that is, correspond (sequentialize) to derivable sequent proofs. In order to characterize those sequentializable among all proof structures we need an intrinsic (i.e. non inductive) correctness criterion. First, we extend the usual notion of DR-switching to generalized links. For the switch of a generalized link λ (where P is a generalized connective), chose a partition p = {x 1 , ..., x h } ∈ P , then chose a class x i ∈ p, that is elect the upper edges belonging to this class and adjacent to the corresponding vertex of λ P , disconnect all other upper edges, then for each remaining class of p \ {x i } connect together the pending edges (disconnected before) to a new vertex as in the rightmost side picture of Figure 4. Then, the correctness criterion for generalized proof structures remains the same as the Danos-Regnier's one for MLL proof nets: a generalized proof structure π is correct (it is a generalized proof net) iff for each choice of the generalized switches, the associated graph is acyclic and connected. So, a generalized proof net is an MLL proof net when each link is an axiom, a cut or a basic binary and ⊗ link. We also compactly describe a basic link by the set of its switches interpreted as partitions over the whole border, i. Remarks 16 (on cut reduction). The "computational meaning" of generalized connectives is assured by the fact that reducing in a proof net a cut between (dual) generalized connectives, C and C * , preserves the correctness criterion [START_REF] Danos | The structure of multiplicatives[END_REF]. This fact follows by Definition 11 of a graphical connective where unlike the sequential syntax, requiring only orthogonality between sets of partitions, P ⊥ Q, is not enough for getting the stability of correctness under cut reduction: orthogonality must "pass to the contexts" P ⊥ ⊥ Q ⊥ ; thus, the first condition P ⊥ Q ensures (ACC) correctness of proof structures while the second condition P ⊥ ⊥ Q ⊥ ensures the stability of correctness under cut reduction. A pictorial view in given in Figure 5. E.g., the sequential generalized connective P X = {{(1, 2), (3)}} and Q X * = {{(1, 3), (2)}} is not a connective in proof net syntax since, by Definition 11, 1)}}. This intuitively means

P cut A 1 ... A i ... A n A ⊥ 1 A ⊥ i ... A ⊥ n ... β π C(A 1 , ..., A n ) C * (A ⊥ 1 , ..., A ⊥ n ) → A 1 ... A i ... A n A ⊥ 1 A ⊥ i ... A ⊥ n ...
P ⊥ X = {{(1, 3), (2)}, {(2, 3), (1)}} is not orthogonal to Q ⊥ X * = {{(1, 2), (3)}, {(2, 3), (
PX : {{(1, 2), (3)}} QX * : {{(1, 3), (2)}} cut {(1), (3, 2)} ∈ Q ⊥ X * {(1), (2, 3)} ∈ P ⊥ X πX * π πX λ X λX λ X * λX * → {(1), (2, 3)} ∈ P ⊥ X {(1), (2, 3)} ∈ Q ⊥ X * cut cut cut π (correct proof structure) (non-correct proof structure)
Figure 6: a cut reduction between "pseudo orthogonal" links that if we admit the generalized links λ X and λ X * (corresponding, resp., to connectives P X and Q X * ) then, the proof net π of Figure 6 (obtained by cutting π X , with conclusion X , against π X * , with conclusion X * ) does not reduce to a correct proof net: actually after the reduction of the cut link (X, X * ), the reductum π will contain both a cycle and a pair of disconnected components.

For simplicity reasons, we assumed in Figure 6 that π X (resp., π X * ) is the proof net built by gluing two orthogonal generalized links (modules) λ X and λ X (resp. λ X * and λ X * ) through their common border {1, 2, 3}.

Sequentialization of decomposable connectives

The most natural way to compare the two syntaxes, sequential and graphical, is through their sequentialzation, i.e. a way to set a precise correspondence between sequential proofs and proof nets. Here we focus only on the comparison w.r.t. decomposable connectives (we refer to Section 5 the comparison w.r.t the undecomposable ones discussed in Section 3.4).

There is a strong link between sequential and parallel decomposable connectives as exemplified by the basic cases O ⊗ = {{(1, 2)}} ⊥ = P ⊥ ⊗ and O = {{(1), (2)}} ⊥ = P ⊥ . Actually, the two syntaxes are orthogonal views of a same decomposable connective, as stated in Proposition 17 proved in [START_REF] Danos | The structure of multiplicatives[END_REF].

Proposition 17 (Danos-Regnier sequentialization). Assume X is a decomposable connective s.t. P X is its pre-type (in proof net syntax) and O X is its set of right rules (the organizations set in the sequential syntax) then: O X ⊆ P ⊥ X (de-sequentialization part) and P ⊥ X ⊆ O X (sequentialization part). E.g., assume

P X = {{(A, C), (B)}, {(B, C), (A)}} and O X = {{(A, B), (C)}} with X = (A B) ⊗ C, then O X = P ⊥
X as illustrated in Figure 7. Next fact immediately follows by Proposition 17 and case 8 of Property 3.

Fact 18 (organizations sets are types). The organizations set O F of a decomposable formula F is a type.

A, A ⊥ B, B ⊥ ⊗ A, B, (A ⊥ ⊗ B ⊥ ) C, C ⊥ X (A B) ⊗ C, (A ⊥ ⊗ B ⊥ ), C ⊥ ⇔ A B C A ⊥ B ⊥ C ⊥ X : ⊗ ⊗ Figure 7: an instance of sequentialization
Corollary 19 (reflexive connectives). A connective (P, Q) is reflexive when P ⊥ = Q and Q ⊥ = P . All decomposable connectives are reflexive in the sequential syntax.

Proof. 1) let X and X ⊥ be a decomposable connective; 2) by Property 3, (P Example 20. We may now interpret the two pairs of orthogonal sets of partitions, (P 1 , Q 1 ) and (P 2 , Q 2 ) of Example 2, as two decomposable connectives, according to the two dual points of view seen above: the sequential one as in Figure 8 and the graphical one as in Figure 9 where the decomposable graphical connectives are displayed as binary trees enclosed in dotted boxes: 2), (4)}, {(1, 4), ( 2), (3)}, {(2, 3), ( 1), (4)}, {(2, 4), ( 1), (3)}} P 2 = {{(2, 3), (4, 1)}} and Q 2 = {{(2, 4), ( 3), (1)}, {(2, 1), ( 3), (4)}, {(3, 4), ( 2), (1)}, {(3, 1), ( 2), (4)}}.

X ⊥ P X ⊥ ) ⇔ (P ⊥⊥ X ⊥ P ⊥⊥ X ⊥ ); 3) by Proposition 17, (O X = P ⊥ X ) ∧ (O X ⊥ = P ⊥ X ⊥ ); 4) by 1, O X ⊥ O X ⊥ then, by 2 and 3, O ⊥ X ⊥ O ⊥ X ⊥ ; 5) by 4 and Property 3 (case 7), it finally follows (O X = O ⊥ X ⊥ ) ∧ (O X ⊥ = O ⊥ X ) since by 3, (O X = O ⊥⊥ X ) ∧ (O X ⊥ = O ⊥⊥ X ⊥ ).
P 1 = {{(1, 2), (3, 4)}} and Q 1 = {{(1, 3), (

Undecomposable connectives

Not all generalized connectives are binary decomposable; e.g. the sequential connective O X = {{(1, 2), (3)}} and O X * = {{(1, 3), (2)}} seen in Remark 16 is undecomposable w.r.t. the basic connectives and ⊗ (it is neither a connective in the graphical syntax, indeed). Anyway, if we complete

(1, 2) (3, 4) p 1 (1 2) ⊗ (3 4) (1, 3) (2) (4) q 1 1 (1 ⊗ 2) (3 ⊗ 4) (1, 4) (2) (3) q 2 1 (1 ⊗ 2) (3 ⊗ 4) (2, 3) (1) (4) q 3 1 (1 ⊗ 2) (3 ⊗ 4) (2, 4) (1)
(3)

q 4 1 (1 ⊗ 2) (3 ⊗ 4) (2, 3) (4, 1) p 2 (2 3) ⊗ (4 1) (2, 4) (3) (1) q 1 2 (2 ⊗ 3) (4 ⊗ 1) (2, 1) (3) (4) q 2 2 (2 ⊗ 3) (4 ⊗ 1) (3, 4) (2)
(1)

q 3 2 (2 ⊗ 3) (4 ⊗ 1) (3, 1) (2) (4) q 4 2 (2 ⊗ 3) (4 ⊗ 1)
Figure 8: generalized decomposable connectives in sequent calculus syntax A more serious example is the famous Girard's connective (G 4 , G ⊥ 4 ): 2), (4)}, {(2, 4), ( 1), (3)}} along with some other instances below (we omit their orthogonal) As we will see in Section 4.3, the pregnancy of Girard's connectives is given by the fact that, unlike the two previous ones, (X, X * ) and (Z, Z * ), there is no chance to complete them in such a way they become decomposable connectives neither in the sequential nor in the graphical setting. That is consequence of the fact that connectives like (G 4 , G ⊥ 4 ) are described by pairs of types. Moreover, sequents like G 4 , G ⊥ 4 are not provable tout court in M LL + (if we exclude the trivial non atomic logical axioms) because of the "packaging problem" seen in Remark 10. Each rule for G 4 (resp., for G ⊥ 4 ) is binary (resp., ternary) so any attempt to derive G 4 (resp., G ⊥ 4 ) would build a premise (of sequent G 4 , G ⊥ 4 ) with the other conclusion together with only some (not all) of the principal formulas of the applied rule; so, sequents like G 4 , G ⊥ 4 are never logically provable from atomic logical axioms. Finally, since G 4 (resp., G ⊥ 4 ) is not decomposable and since there is no chance to embed it into a decomposable connective, sequent G 4 , G ⊥ 4 is not even stepwise derivable.

⊗ ⊗ ⊗ F 1 F ⊥ 1 1 4 3 2 2 1 4 3 P 1 Q 1 bipole anti-bipole ⊗ F 2 F ⊥ 2 ⊗ ⊗ 2 3 4 1 1 4 3 2 P 2 Q 2 bipole anti-bipole
G 4 = {{(1, 2), (3, 4)}, {(2, 3), (4, 1)}} G ⊥ 4 = {{(1, 3), (
G 6 = { {(1, 2
The study of a "minimal" class of undecomposable connectives will be the subject of next sections.

Entangled connectives

In this section we introduce a special class of sets of partitions: entangled pairs (Definition 21) which is then exploited to define the class of entangled connectives (Definition 33). Entangled pairs have interesting properties that are investigated throughout this Section 4. The first one (Theorem 32, one of the main results of the paper), being that every entangled pair of partitions sets is a type. This result has several consequences: decomposable entangled pairs (and so, decomposable connectives) have a very simple characterization (the normal form of Theorem 36), which can be further used to prove that given an undecomposable entangled connective, P and Q, where P is an entangled pair, P cannot be embedded into a decomposable type T P , s.t. T and Q become decomposable (Corollary 40).

Entangled types

Definition 21 (entangled pairs of partitions). Let P be a pair of nonempty distinct partitions, p 1 and p 2 , on the same (finite) domain X = {1, ..., n}. P is an entangled pair if it satisfies the following two conditions:

1. p 1 and p 2 have same weight; 2. each class belonging to p 1 or p 2 has degree 1 or 2.

Definition 22 (restriction of entangled pairs). Given a set of partitions P on a finite domain X and given an element a ∈ X, the restriction of P by point a (also a-restriction of P ), denoted P (↓a) , is the set of partitions obtained after erasing a from each partition of P . A restriction of P by a is conservative when P and P (↓a) have the same weight.

We say that a restriction of an entangled pair P by a point a is admissible when P (↓a) is in turn an entangled pair; hence, an entangled pair P is restrictable if there exists an admissible restriction of P by a point.

We say that an entangled pair P is restrictable only in one point (also P admits only one restriction by a single point) iff ∃a s.t. P (↓a) is an entangled pair and ¬∃b = a s.t. P (↓b) is an entangled pair.

We can extend the notion of restriction to sets of points of the support, i.e., P (↓Y ) where Y ⊆ X.

Example 23. Both P 1 and P ⊥ 1 of Example 5 are entangled pairs while neither P 2 nor P ⊥ 2 is so. Sets P 3 , P 4 and P 4 below are not restrictable entangled pairs; P 5 and P 6 below are both conservative restrictable entangled pairs: in particular, P 5 admits two restrictions, one by point c and another one by point d, while P 6 admits only one restriction, that one by single point a: Lemma 24 (orthogonality of non restrictable entangled pairs). If P is a non restrictable entangled pair then, its orthogonal P ⊥ is not empty.

Proof. Since P = {p 1 , p 2 } is an entangled pair, every element of the support, a ∈ X, must occur in each p i either as singleton class (a) or in a pair class (a, b) for some b ∈ X with a = b. Moreover, since P is not restrictable it cannot be the case that the same point a occurs:

1. as singleton class (a) in both p 1 and in p 2 , or 2. in a pair class in both p 1 and p 2 (that is, it cannot be the case that e.g., (a, b) ∈ p 1 and (a, c) ∈ p 2 ) except when P is in form (1) below, in which case we have P ⊥ = {{(a), (b, c)}} by calculation.

P = p 1 : {(a, b), (c)}, p 2 : {(a, c), (b)} ; (1)
In other words, if P is a non restrictable pair distinct from (1) then ∀a ∈ X one of the following two cases holds:

(i) in case the singleton class (a) occurs in p 1 (resp., occurs in p 2 ) then a must occur in a pair class (a, b) of p 2 (resp., in a pair class (a, b) of p 1 ); (ii) in case a occurs in a pair class (a, b) of p 1 (resp., of p 2 ) then a must occur as singleton class (a) in p 2 (resp., in p 1 ); otherwise the erasing of point a in a non restrictable P would produce two restricted sets, p (↓a) 1

and p

(↓a)
2 , that result to be either equal (p

(↓a) 1 = p (↓a)
2 ), in case P is in form (1), or with distinct weights, w 1 = w 2 , contradicting Definition 21. This means that P must appear as a generalization of P 4 or P 4 of Example 23, that is, the domain X of P must have dimension 2n and form {a 1 , ..., a n } {b 1 , ..., b n }; in other words, X can can be thought as the disjoint sum of two segments of points, S 1 = {a 1 , ..., a n } and S 2 = {b 1 , ..., b n }:

• in the first one, S 1 (resp., in the last one, S 2 ), we find all points that occur both inside pair classes in p 1 and inside singleton classes in p 2 ;

• in the second one (resp., in the first one) we find all points that occur both inside singleton classes in p 1 and inside pair classes in p 2 .

So P is in form (2) below (where n is an even integer):

P = p 1 : {(a 1 , a 2 )
that is, every a i (resp., b i ) must occur together with an other point a j (resp., b j ) in a class of p 1 (resp., p 2 ) moreover, a i and a j (resp., b i and b j ) must occur as singleton classes, (a i ) and (a j ) (resp., (b i ) and (b j )), in p 2 (resp., p 1 ).

Observe that P has weight n/2 + n, by the way we build form (2).

We can now build a partition q = {y 1 , ..., y m } with weight m = n/2 + 1 as follows (also displayed both on the top and on the bottom side of Figure 10):

• first elect a class, e.g. y 1 , containing all the elements of the domain s.t. they do not form pairwise a class of p i ; the degree of y 1 will be n;

• then, chose each remaining class, y j with 2 ≤ j ≤ m, in such a way that it consists of only two elements: one belonging to a class of p i with two elements and the other one belonging to a class of p i with a single element, as the top (resp., bottom) side picture of Figure 10; there are n/2 such classes.

By calculation partition q is orthogonal to each p i since by the Euler-Poincaré law, |V | -|E| = 1 where V and E are resp., vertexes and edges of each induced graph G i (q, p i ) with |V | = n/2 + n + n/2 + 1 = 2n + 1 and |E| = 2n as depicted in Figure 10; therefore P ⊥ = ∅.

p 1 : {(a 1 , a 2 )... {(b 1 , b 2 ) p 2 :
...

(a i-1 , a i ) (b i-1 , b i ) ... (b 2 ) ... (b i-1 ) (b i ) (a n-1 , a n ) (b 1 ) ... (b n-1 )(b n )} ... (b n-1 , b n ) (a 1 ) (a 2 ) ... (a i-1 ) (a i ) ... (a n-1 )(a n )} (a 2 , b 2 ) ... (a i , b i ) (a n , b n )} ... (a 2 , b 2 ) ... (a i , b i ) ... (a n , b n )} y j y m y m y 1 y 1 y 2 y j y 2 q : q : {(a 1 , ..., a i-1 , ..., a n-1 , b 1 , ..., b i-1 , ..., b n-1 ) {(a 1 , ..., a i-1 , ..., a n-1 , b 1 , ..., b i-1 , ..., b n-1 )
Figure 10: orthogonal of non restrictable entangled pair Proposition 25 (restrictable entangled pairs). Let P = {p 1 , p 2 } be an entangled pair that is restrictable by point a; assume the orthogonal of the a-restriction of P , i.e., (P (↓a) ) ⊥ = {q 1 , ..., q m }, is nonempty, then the set of partitions P built according to the two cases below is orthogonal to P .

1. If a is singleton class in both p 1 and p 2 , i.e., P is in form (3)

P = {(a), x 2 , ..., x n }, {(a), y 2 , ..., y n } (3)
then, P is built as follows: for each partition q i , 1 ≤ i ≤ m, insert point a in a class x j i of q i ; repeat this insertion of point a for each class x j i in q i (each insertion produces a "pumped" partition also denoted q a i ∈ P ). 2. Otherwise, if a belongs to a class with two elements, both in p 1 and p 2 , i.e. P is in form (4) below

P = {(a, b), x 2 , ..., x n }, {(a, c), y 2 , ..., y n } (4)
then, P is built as follows: insert (or "pump") the singleton class (a) in each partition q i ∈ P (↓a)⊥ ; so P is as in form ( 5) below (each insertion produces a "pumped" partition also denoted q a i ∈ P ):

P = {q 1 ∪ {(a)}, ..., q i ∪ {(a)}, ...q m ∪ {(a)}} (5)
Proof. By Euler-Poincaré Property 4, every pumped partition q a i ∈ P is orthogonal to every partition p ∈ P (the induced graph G(p, q a i ) is ACC).

Fact 26 (entangled pair of dimension 3). If the dimension of an entangled pair P is 3 (i.e. |X| = 3) then P is in form ( 1) and its weight is 2.

Proof. It follows by calculation: actually, in order to have an entangled pair, P must have at least weight w ≥ 2 and in case weight w is exactly 2 then, at least one class must have degree 2; thus, if |X| = 3 then P must be in form [START_REF] Andreoli | Focussing and Proof Construction[END_REF].

Lemma 27 (orthogonality of entangled pairs). The orthogonal P ⊥ of an entangled pair P is not empty.

Proof. By induction on the dimension |X| of P . The base of induction is when |X| = 3 then P must be in form [START_REF] Andreoli | Focussing and Proof Construction[END_REF], by Fact 26, so its weight w is 2. Thus, P is non restrictable and so by Lemma 24 its orthogonal is not empty.

For the induction step |X| > 3 we split our reasoning in two main cases:

1. if P is restrictable by point a, it is in form (3) or ( 4), then the orthogonal of the restriction P (↓a) , let us say (P (↓a) ) ⊥ = {q 1 , ..., q m }, is not empty by hypothesis of induction, so by Proposition 25, P ⊆ P ⊥ ; 2. otherwise, if P is not restrictable, then we conclude by Lemma 24.

Theorem 28 (non restrictable entangled types). If P is a non restrictable entangled pair (i.e., ¬∃a ∈ X s.t. P (↓a) is an entangled pair) then P is a type.

Proof. If P = {p 1 , p 2 } is a non restrictable entangled pair then, by Lemma 24, either P has form [START_REF] Andreoli | Focussing and Proof Construction[END_REF] or P has form (2). In case P has form (1) then it is a type (simply by calculation). Otherwise, if P has the form (2) then, we reason by absurdum, assuming that P is not a type; so, let p 3 = p i=1,2 be a partition belonging to P ⊥⊥ . We reason on the classes of p 3 . Observe that p 3 cannot contain only singleton classes, otherwise p 3 will have a weight (2n) greater than the weight of p 1 and p 2 , contradicting case 12 of Property 3 (by Lemma 27, P ⊥ is nonempty); thus p 3 must contain at least a class with at least two points. Moreover, since p 3 differs from p 1 and p 2 , it must satisfy at least one of the following three cases:

1. p 3 contains a class x with two points, a i and a j (resp., b i and b j ) which belong to two distinct classes of p 1 (resp., p 2 ); 2. p 3 contains a class x with two points a i and b j s.t. a i ∈ {a 1 , ..., a n } and b j ∈ {b 1 , ..., b n }; 3. p 3 contains two classes x 1 and x 2 s.t. x 1 belongs to p 1 and x 2 belongs to p 2 (resp., x 1 belongs to p 2 and x 2 belongs to p 1 ).

We show now that for each of these three cases we get a contradiction. Indeed, since P has the form (2) then, for each p 3 satisfying (at least) one of cases 1-3, we can build a partition q = {y 1 , ..., y m } in P ⊥ , with weight m = n/2 + 1 like e.g. partition q depicted on the top (resp., bottom) side of Figure 10 in the proof of Lemma 24. We show that p 3 ⊥ q.

1. Case 1 is not consistent (p 3 ⊥ q) because we can chose q in such a way that class y 1 contains two points a i and a j (resp., b i and b j ), occurring resp., in two distinct classes of p 1 (resp., p 2 ), like e.g. class (a 1 , ..., a i-1 , ..., a n-1 , b 1 , ..., b i-1 , ..., b n-1 ) of Figure 10. 2. Case 2 is not consistent (p 3 ⊥ q) because we can chose q in such a way that a class y j contains exactly two points, a i and b j , like e. ) and (a 2 , b 2 ) in Figure 10 (thus, the graph of incidence G(p 3 , q i ) will contain a cycle).

Lemma 29 (restrictable entangled pairs). Let P = {p 1 , p 2 } be a restrictable entangled pair and let p 3 = p i=1,2 be a partition in the type P ⊥⊥ . If some a-restriction of P is a type (i.e., P ↓a = {p

(↓a) 1 , p (↓a)
2 } = (P (↓a) ) ⊥⊥ for some a ∈ X) then, the restriction p (↓a) 3 belongs to P ↓a .

p 2 1 , p 1 2 p 2 2 } is in form (6) below: (a 1 , a 2 ) ... (b 1 , b 2 ) ... (a i-1 , a i ) (b i-1 , b i ) ... (b 2 ) ... (b i-1 ) (b i ) (a n-1 , a n ) (b 1 ) ... (b n-1 )(b n )} ... (b n-1 , b n ) (a 1 ) (a 2 ) ... (a i-1 ) (a i ) ... (a n-1 )(a n )} (c) (b) {(a, c) {(a, b) p 1 : p 2 : P (6)
where the restriction P (↓S 0 ) is exactly that one in form [START_REF] Cockett | Weakly Distributive Categories[END_REF].

Proof. Since the a-restriction is conservative a must occur both in one class of p 1 together with a point b and in one class of p 2 together with a point c of the support that is, (a, b) ∈ p 1 and (a, c) ∈ p 2 for some b, c ∈ X; moreover since P is only restrictable by the single point a, we have that:

1. b = c and 2. b and c cannot occur together with other points of the support in some class of p 2 resp., p 1 otherwise P would be restrictable also in these two points, contradicting the assumption P is only restrictable by a.

This means that if (a, b) ∈ p 1 and (a, c) ∈ p 2 then (b) ∈ p 2 and (c) ∈ p 1 . Now, since P is restrictable, p 1 and p 2 cannot consist of only these two pairs of classes that is, P cannot be reduced in form [START_REF] Andreoli | Focussing and Proof Construction[END_REF]. Thus P must be in form ( 7)

P = p 1 = {(a, b), (c)} Q 1 p 2 = {(a, c), (b)} Q 2 . ( 7
)
where Q 1 and Q 2 are two sets of partitions over the support X \ S 0 with S 0 = {a, b, c}. Finally, since P is restrictable only by point a, Q 1 and Q 2 must be a non restrictable pair in form (2) over S 1 S 2 ; therefore P is an entangled pair in form [START_REF] Girard | Linear Logic[END_REF] with support S 0 : {a, b, c} S 1 : {a 1 , ..., a n } S 2 : {b 1 , ..., b n }.

Lemma 31 (conservative single point restrictable entangled pairs). Assume P = {p 1 , p 2 } is a entangled pair that admits only one conservative restriction by point a, so P is in form [START_REF] Girard | Le point aveugle[END_REF] below with b = c:

P = p 1 : {x 1 = (a, b), x 2 , ..., x n }, p 2 : {y 1 = (a, c), y 2 , ..., y n } . ( 8
)
Let p 3 = p i=1,2 be a partition in P ⊥⊥ then, p 3 must contain either class x 1 = (a, b) or class y 1 = (a, c) of P in form [START_REF] Girard | Le point aveugle[END_REF].

Proof. Assume P admits only one conservative restriction by point a then, by Proposition 30, P is as in form [START_REF] Girard | Linear Logic[END_REF]. Now, consider the next two partitions, q 1 and q 2 :

q 1 : {z 1 = (a), z 2 = (b, c)} ∈ P ⊥ 1 q 2 : {y 1 = (a 1 , ..., a i-1 , ..., a n-1 , b 1 , ..., b i-1 , ..., b n-1 ), ..., y m = (a n , b n )} ∈ P ⊥ 2
where P ⊥ 1 and P ⊥ 2 are resp., the orthogonal of P 1 in form (1) and P 2 in form (2), by Proposition 30, as displayed on top and bottom side of Figure 11. Then build a partition q of the form q 1 q 2 (i, j), for some 1 ≤ i, j ≤ (2n + 3), (a 1 , a 2 ) ...

(b 1 , b 2 ) ... (a i-1 , a i ) (b i-1 , b i ) ... (b 2 ) ... (b i-1 ) (b i ) (a n-1 , a n ) (b 1 ) ... (b n-1 )(b n )} ... (b n-1 , b n )}(a 1 ) (a 2 ) ... (a i-1 ) (a i ) ... (a n-1 )(a n )} (c) (b) {(a, c) {(a, b) p 1 : p 2 : {(a) y m y m y j (a 2 , b 2 ) y 2 ... ... (a i , b i ) (a n , b n )} (a n , b n )} (a i , b i ) ... P y 2 y 1 z 2 y j z 1 y 1 z 2 z 1 q 2 q 1 q 1 q 2 (a 2 , b 2 ) ... (b, c)} (b, c)} {(a) {(a 1 ...a i-1 ...a n-1 b 1 ...b i-1 ...b n-1 ) {(a 1 ...a i-1 ...a n-1 b 1 ...b i-1 ...b n-1 )
Figure 11: a conservative single point restrictable entangled pair where the notation means that we concatenate q 1 and q 2 by mixing classes z h ∈ q 1 and y k ∈ q 2 containing, resp., points i and j. E.g., partition q = {z 1 y 1 , z 2 , y 2 , ..., y m }, displayed in the bottom side of Figure 12, is obtained by concatenating q 1 and q 2 and mixing (by union) classes z 1 and y 1 . By Property 4, q ∈ P ⊥ , since each induced graph G(p i , q) for i = 1, 2 is ACC. Now, assume by absurdum that a occurs in a class of p 3 = p i=1,2 of P ⊥⊥ that is distinct from both classes (a, b) and (a, c) of [START_REF] Girard | Le point aveugle[END_REF]. By Proposition 25 (case 2), a cannot occur in p 3 as singleton class (a). So, assume a belongs to a class (a, d, ...) with d = b and d = c. Then it is easy to find in P ⊥ a partition like q or q , displayed resp., in the bottom and top sides of Figure 12,s.t. the induced graph G(p 3 , q) resp., G(p 3 , q ), contains a cycle. Case (a, b, c) ∈ p 3 is also excluded because of partitions like q or q , containing class z 2 = (b, c).

Theorem 32 (entangled types). Every entangled pair of partitions sets P = {p 1 , p 2 }, with domain X = {1, ..., n}, is a type (P = P ⊥⊥ ) thus, entangled pairs are called entangled types.

(a 1 , a 2 ) ...

(b 1 , b 2 ) ... (a i-1 , a i ) (b i-1 , b i ) ... (b 2 ) ... (b i-1 ) (b i ) (a n-1 , a n ) (b 1 ) ... (b n-1 )(b n )} ... (b n-1 , b n ) (a 1 ) (a 2 ) ... (a i-1 ) (a i ) ... (a n-1 )(a n )} (c) (b) {(a, c) {(a, b) p 1 : p 2 : (b, c) (a) z 2 (a) y 2 z 1 ∪ y 1 q : q : (a 2 , b 2 ) y m y m y j (a 2 , b 2 ) y 2 ... ... ... (a i , b i ) (a n , b n ) (a n , b n ) (a i , b i ) ... z 1 ∪ y j (b, c) y 1 P (a 1 ...a i-1 ...a n-1 b 1 ...b i-1 ...b n-1 ) (a 1 ...a i-1 ...a n-1 b 1 ...b i-1 ...b n-1 )
Figure 12: orthogonal of a conservative only single point restrictable entangled pair Proof. By induction on the dimension of P , i.e. on the cardinality of its domain X = {1, ..., n}.

The base of induction is when n = 3 (there is no entangled pair of dimension 2) then, by Fact 26, P is in form (1), so it is not restrictable; therefore it is a type, by Theorem 28.

For the induction step, assume P has dimension n > 3. If P is not restrictable then, by Theorem 28, P is a type. Otherwise, when P is restrictable, we split our reasoning in two main cases, depending on whether P admits or not a conservative restriction.

Case 1. Assume P admits a non conservative restriction by a point a, then P has the form below P = {p 1 : {(a), x 2 , ..., x n }, p 2 : {(a), y 2 , ..., y n }}.

Assume by absurdum p 3 ∈ P ⊥⊥ with p 3 = p i=1,2 . By Proposition 25 (case 1), a must also occur in p 3 as singleton class, i.e. p 3 = {(a), z 2 , ..., z n } (otherwise, we get a cycle in the induced graph G(q a i , p 3 ) for some pumped q a i ∈ P ⊥ ). By hypothesis of induction, P (↓a) is a type so, by Lemma 29, either p 3 = p 1 or p 3 = p 2 .

Case 2. Assume P admits only conservative restriction by a point as e.g. that one by point a in form (9) below

P = p 1 : {x 1 = (a, b), x 2 , ..., x n }, p 2 : {y 1 = (a, c), y 2 , ..., y n } . (9)
By Lemma 31, P must be restrictable by at least one more point than a; therefore, w.r.t. all possible admissible restrictions of P , there are only three cases involving points d and e.

1. Neither d nor e is an admissible restriction of P . Assume P is restrictable by a point f = a. By hypothesis of induction the restriction P (↓f ) is a type, so by Lemma 29, either p

(↓f ) 3 = p (↓f ) 1
or p

(↓f ) 3 = p (↓f ) 2
, that is absurdum, since p

Since class (a, c) belongs to partition p 2 and since P is not restrictable by c (by hypothesis), then c must occur as singleton class (c) in p 1 ; so, form (9) of P will become like the one below: must also occur either in p 1 or in p 2 : that is inconsistent since, in both cases, c will simultaneously occur in two classes both belonging either to p 1 or to p 2 , that is either p 1 = {(a, b), (c), (d, c), x 4 ..., x n } ∈ P or p 2 = {(a, c), (d, c), y 3 ..., y n } ∈ P .

P = p 1 : {(a,

Entangled connectives

By Lemma 24, as soon as P is an entangled pair, then its orthogonal is nonempty, so it makes sense to define the class of entangled connectives as follows.

Definition 33 (entangled connectives). A generalized connective (P, Q), in graphical or sequential syntax, is called entangled whenever P or Q is an entangled pair of partitions sets.

Next Fact 34 is consequence of case 6 of Property 3 and Theorem 32.

Fact 34. If P is an entangled type then, (P, Q) is an entangled generalized connective iff P = Q ⊥ .

The smallest (w.r.t. the dimension of the domain) entangled decomposable connective is P X = {{(1, 3), (2)}, {(2, 3), (1)}} and Q X * = {{(1, 2), (3)}}, with X = (1 2) ⊗ 3 and X * = (1 ⊗ 2) 3 in graphical syntax.

If P = {p 1 , p 2 } is an entangled pair over X = {1, ..., n} then, each singleton {p i } can be interpreted as the pre-type of a special decomposable formula with border {1, ..., n}, called bipole [START_REF] Andreoli | Focussing and Proof Construction[END_REF]. A bipole B is a MLL formula with only two layers of connectives: a generalized of (i-1)⊗i sub-formulas (with 1 < i ≤ n) that is, B = ˆ ( ⊗1 , ..., ⊗m ) as in the l.h.s. picture of Figure 13. Dually, B ⊥ = ⊗( ˆ 1 , ..., ˆ n ) is called anti-bipole, that is a MLL formula with only two layers of connectives: a generalized ⊗ of (i -1) i sub-formulas (with 1 < i ≤ n) as in the r.h.s. picture of Figure 13. Every bipole satisfies the property that its pre-type is a type (see Lemma 4 of [START_REF] Maieli | Modularity of proof nets: generating the type of a module[END_REF]). To be precise, observe that in case an entangled pair P is interpreted as the (pre-)type of a bipole B then some ⊗-subtrees of B may be unary.

... ... 13: a bipole skeleton on l.h.s. and an anti-bipole skeleton on r.h.s.

1 2 n n -1 ⊗ ⊗ ⊗ i -1 i ... ... 1 2 n n -1 i -1 i ⊗ Figure
In the following we characterize, by means of Theorem 36 and Theorem 39, the class of non binary decomposable entangled connectives. We then show that these connectives can neither be approximated to decomposable connectives (Corollary 40) nor sequentialized in the M LL + sequent calculus (Section 5).

Decomposable normal form of entangled connectives

Definition 35 (decomposable normal form). Let P = {p 1 , p 2 } be an entangled pair of partitions then: P is decomposable iff it is the pre-type of the parse tree of a multiplicative formula; moreover, P is in (decomposable) normal form iff P is the pre-type of a formula tree F with literals indexes as in the l.h.s picture of Figure 14 that is, P is obtained by a between:

• the smallest decomposable entangled connective, {{(1, 3), ( 2 (d,f ), (e)}} is not in normal form (it is not even decomposable). Observe that normal form is defined up to commutativity of MLL.

Theorem 36 (decomposable normal form). An entangled pair of partitions P = {p 1 , p 2 } is decomposable iff P is in normal form (12).

Proof. Assume P is a decomposable entangled pair of partitions, hence by Definition 13, there exists a formula F s.t. pre-type P F of its syntactical tree is P . Since P is entangled (its size is 2 and its weight is ≥ 2), the syntactical tree of F must contain at least a -node otherwise (by reasoning on switchings of F ) the pre-type of F consists of only one partition with a single class (contradicting the assumption P is entangled); for similar reason F cannot consist of only -nodes otherwise the (pre-)type of F contains exactly one partition (contradicting the assumption P is entangled). So, F must contain at least a ⊗-node and a -node. Now it must exist at least a -node L 1 above a ⊗-node L 2 in the tree otherwise F is a bipole and therefore its (pre-)type would consists of a single partition, contradicting the assumption P is entangled pair. So, assume F is as in the r.h.s. picture of Figure 14, where t 1 , t 2 , t 3 and t 4 are sub-trees of the formula tree of F .

First observe that no other link can stay between L 1 and L 2 , otherwise such a link, let us say, L = (resp., let us say L = ⊗) would increase the size s of P (resp., the maximal degree 1 ≤ δ ≤ 2 allowed for each class of p i ) contradicting the assumption P is an entangled pair.

Then observe that every tree t i , for i = 1, 2, 3, must be reduced to single points (i.e., each t i is a tree consisting of a single node), otherwise: 1. in case t i is a tree whose root is a ⊗-node, we get a class with degree > 2, contradicting the assumption P is entangled pair; 2. in case t i is a tree whose root is a -node, by reasoning on the switchings of F (since there would be two -nodes dominating a ⊗-node), we get the size of P is > 2, contradicting the assumption P is entangled pair.

So, t 1 , t 2 and 3 must be single-point trees; moreover t 4 (if any) must be a bipole like that one enclosed by dotted line in the l.h.s. of Fig. 14, otherwise by computing of all possible switchings of F we get that its pre-type P F = P is not an entangled pair, that is contradiction. Thus, F must be as in the l.h.s. picture of Figure 14, with the pre-type consisting of partitions p 1 and p 2 as in normal form (12).

Vice-versa, it is easy to calculate that an entangled pair in normal form (12) is decomposable.

Remarks 37 (normal form and semi-distributive law). Informally we can say that an entangled pair P in decomposable normal form can be thought as the set of the pre-types (types indeed) of the two bipoles (reductum), B 1 and B 2 , that are obtained after one step of weak (or linear or semi-) distributive law [START_REF] Cockett | Weakly Distributive Categories[END_REF] applied to the (redex) formula F (where P = P F ) whose abstract skeleton tree is the one depicted on the l.h.s. of Figure 14. Actually, following [START_REF] Maieli | Modularity of proof nets: generating the type of a module[END_REF], we may define a rewrite relation " wd " on MLL formulas trees generated by associativity and commutativity of ⊗ and plus the weak or semi-distributive law synthetically defined as follows:

F : A B C ⊗ wd ⊗ A C B F 1 : ∧ ⊗ B C A F 2 : (A B) ⊗ C (A ⊗ C) B ∧ (A B) ⊗ C (B ⊗ C) A.
Then it is easy to calculate the equality P = P F = P B 1 ∪ P B 2 once F is as in the l.h.s. of Figure 14 and F wd B i , for i = 1, 2, as below:

⊗ ⊗ ⊗ 1 2 3 4 ... n 5 ... n -1 F : wd ⊗ ⊗ 1 4 ... n 5 ... n -1 2 3 ⊗ B 1 : ∧ ⊗ ⊗ 4 ... n 5 ... n -1 3 ⊗ 2 1 B 2 :
Observe that, via Theorem 38, stated below and proved in [START_REF] Maieli | Modularity of proof nets: generating the type of a module[END_REF], we can show that "if P is a decomposable entangled pair then, P is a type". Actually, if P is a decomposable entangled pair then, by Theorem 36, P is the pre-type of the formula tree F in the l.h.s. of Figure 14 and so, by Theorem 38, P is a type. In other words, if P is a decomposable set of partitions then, by Theorem 38, both types P ⊥⊥ F and P ⊥ F (since, by Fact 14, P ⊥ F = T F ⊥ ) can be computed by the exhaustive * wd -rewriting of F and F ⊥ .

Theorem 38 (Maieli-Puite: type generation of a MLL formula tree).

If F is a MLL formula with pre-type P F then, its type T F can be generated by the exhaustive wd -rewriting of F , as follows:

T F = i P F i s.t., F * wd F i
where each F i is a bipole, with type P F i , obtained by transitive closure of * wd relation from F .

Proof. Given in [START_REF] Maieli | Modularity of proof nets: generating the type of a module[END_REF].

Undecomposable entangled connectives

By Theorem 36, an entangled connective, P and Q, is binary decomposable iff P or Q is in normal form. We want now to make sure that if P (resp., Q) is a non decomposable entangled type, then neither Q (resp., P ) will be decomposable (by Theorem 39), so P and Q is an undecomposable connective.

Theorem 39 (undecomposable entangled connectives). Let E and Q be a generalized connective. If E is an entangled pair that is not binary decomposable then, Q is neither decomposable.

Proof. Let (E, Q) be a generalized connective with E an undecomposable entangled pair. Suppose, for the sake of absurdity, that Q is decomposable, i.e. Q = P A for some formula A. By Fact 34 and by Fact 14, we have

E = (Fact 34) Q ⊥ = P ⊥ A = (Fact 14) T A ⊥
that is, E is the bi-orthogonal of P A ⊥ . Therefore, P A ⊥ is included in E, by case 3 of Property 3. Now, since E has only two elements, if P A ⊥ were strictly included in E, it would be either the empty set or a singleton set so, its biorthogonal would not be E; therefore we have E = P A ⊥ , a contradiction.

Next corollary is consequence of Fact 34 and Theorem 39.

Corollary 40 (completion). Let E and Q be an entangled connective with E being a non (binary) decomposable entangled pair; then, E cannot be completed in such a way to become decomposable (i.e., ¬∃D E s.t. D is binary decomposable with D and Q being a connective).

Remarks 41 (entangled connectives and bipoles). Although our notion of "entanglement" doesn't solve the (admittedly, difficult) general problem ("try to find a characterization of the full class of undecomposable connectives"), it is far from being and "ad hoc" condition. It is rather a natural condition that can be observed as soon as we "superpose" (sum) pairs of bipoles with the same "skeleton" (i.e.,bipoles with the same abstract syntactical tree), like e.g. the two ones, F 1 and F 2 , enclosed by dotted lines in Figure 9 of Section 3.3. More concretely, an entangled connective, P = {p 1 , p 2 } and P ⊥ , can be interpreted as the union (resp., the intersection) of the types of two bipoles (resp., the types of two anti-bipoles) which are equivalent up to cyclic permutations of the literals indexes of the top border that is, bipoles (resp., anti-bipoles) s.t.:

1. they have the same syntactical tree skeleton;

2. they have the same border up to cyclic permutation of literals indexes.

Formally, given two bipoles like F 1 and F 2 of Figure 9, with ). This fact (Theorem 32) is a novelty since the union of types is not in general a type while the intersection of types is always a type (Property 3). Indeed, entangled types are the smallest types (w.r.t. the number of partitions), if we exclude the trivial singleton types (every set consisting of a single partition is a type by case 11 of Property 3). So, entangled connectives can be considered in some sense the "smallest" generalized multiplicative connectives (w.r.t. the number of switchings or the number of rules), if we exclude the basic ones, and ⊗, and bipoles.

T F 1 = {p 1 } and T F 2 = {p 2 }, then P = T F 1 ∪ T F 2 and P ⊥ = T F ⊥ 1 ∩ T F ⊥ 2 is

Sequentialization of undecomposable connectives

The natural correspondence (sequentialization) between sequential decomposable connectives and graphical decomposable connectives is broken by non decomposable connectives! There exist proof nets, containing non decomposable links, without counterpart in the sequential calculus M LL + , if we exclude the trivial correspondence with (non atomic) logical axioms. Let G and G * be an entangled non decomposable connective. By Theorem 39, neither G nor G * is binary decomposable. There is indeed no η-expanded proof of G, G * since each rule for G, resp., G * has at least two premises (see Section 3.4). Actually, sequents of non decomposable entangled formulas G, G * , are not provable from atomic logical axioms in the extended M LL sequent calculus: that is because each rule for G (resp., G * ) is at least binary (it has at least two premises, by the entanglement) so any derivation of this sequent would build a premise with the other conclusion G * (resp., G) together with only some (not all) of the principal formulas of the applied rule. This situation is quite different with proof nets. Consider the proof structure π with only two conclusions, G and G * , as in Figure 15, built as follows:

1. take the two non decomposable links λ G and λ G * ; 2. label the elements of the top border X = {1, ..., n} of λ G (resp., of λ G * ) by n occurrences of literals, a 1 , ..., a n (resp., a ⊥ 1 , ..., a ⊥ n ); 3. put an axiom link for each matching pair of dual literals, a i and a ⊥ i . Clearly π is an η-expanded proof net: each global switching induces an acyclic and connected correction graph; nevertheless, π cannot be "sequentialized" in M LL + , if we exclude the trivial (non atomic) axiom G, G * . Actually, any attempt of starting by sequentializing G (resp., G * ) will induce a single connected proof structure π G * (resp., π G ), with G * (resp., G) among its conclusions, which is not correct: actually, there exist two switchings for π G * (resp., π G ) with at least two disconnected components (consequence of the entanglement conditions of Definition 21). Moreover, since neither G nor G * is binary definable (by Corollary 40, neither G nor G * can be be completed to a decomposable connective), π is not even stepwise sequentializable. This fact witnesses an asymmetry between proof nets and sequent proofs since the former ones allow us to express a kind of parallelism of proofs that the latter ones cannot do.

Conclusions and future works

We gave the first characterization (via Theorems 32, 36 and 39) of a class of multiplicative undecomposable connectives: namely, the entangled connectives (Definition 33) that are not in (decomposable) normal form (Definition 35).

Anyway, there exist non decomposable connectives besides the entangled ones. We are currently working on a more general characterization of the full class of primitive non decomposable connectives (i.e., those ones non definable by means of other connectives). Naively our idea is that a non decomposable connective is rather defined by the set of partitions over the cyclic permutations of the linearly ordered support 1 < ... < n; that's the case with e.g. G 9 below (we omit its orthogonal G ⊥ 9 for the sake of simplicity):

G 9 = { {(1, 2, 3), (4, 5, 6), (7, 8, 9)}, {(2, 3, 4), [START_REF] Girard | Multiplicatives[END_REF][START_REF] Girard | Linear Logic[END_REF][START_REF] Girard | On the meaning of logical rules I: syntax vs. semantics[END_REF], (8, 9, 1)}, {(3, 4, 5), [START_REF] Girard | Linear Logic[END_REF][START_REF] Girard | On the meaning of logical rules I: syntax vs. semantics[END_REF][START_REF] Girard | Le point aveugle[END_REF], (9, 1, 2)} }.

Concerning larger (than MLL) fragments of linear logic, like e.g. MELL or MALL, we don't know at this moment about non definable connectives for such fragments. Certainly, if we restrict to consider the pure additive fragment (ALL) then, there does not exist any generalized connective that cannot be decomposed by the basic additive ones, & and ⊕. There is no "packaging problem" in ALL since contexts in which we derive generalized formulas are simply duplicated. Roughly speaking, non decomposability concerns rather the multiplicative partition of contexts than the additive superposition (better, slicing) of contexts.

The fact that one can compute by means of cut elimination, using such non decomposable connectives, is certainly a good starting point: nevertheless, the study of their connection with concurrency (typically, the Pi-Calculus [START_REF] Milner | Communicating and Mobile Systems: the Pi-Calculus[END_REF]) rather than the Curry-Howard correspondence should be further developed 8 .

Finally, it would be also useful to have a coherence semantics for such non decomposable connectives. We could e.g. use the so-called experiment method of Girard [START_REF] Girard | Multiplicatives[END_REF] for the analysis of proof structures built on such non decomposable connectives. Examples of what can be done with these kind of semantic techniques can be found in [START_REF] Retoré | A Semantic Characterisation of the Correctness of a Proof Net[END_REF] and more recently in [START_REF] Ehrhard | A new correctness criterion for MLL proof nets[END_REF].

G 4 =

 4 {{(1, 2), (3, 4)}, {(2, 3), (4, 1)}} and G ⊥ 4 = {{(1, 3), (2), (4)}, {(2, 4), (1), (3)}}.

Figure 1 :

 1 Figure 1: bipartite graphs of incidence induced by pairs of partitions

Property 4 (

 4 Euler-Poincaré invariance). Given a graph G = (V, E) then, (|V | -|E|) = (|CC| -|Cy|) where |V |, |E|, |CC| and |Cy| denotes, resp., the number of vertices, edges, connected components and primitive cycles of G.

2 =

 2 a), (b)}, {(a, b), (d), (c)}}; 2. if P 2 = {p 1 : {(a, d, c), (b)}, p 2 : {(d, b, c), (a)}} then, P ⊥ {p 1 } ⊥ ∩ {p 2 } ⊥ = {{(b, a), (c), (d)}}.

Figure 2 :

 2 Figure 2: generalized sequential rule

Definition 7 (

 7 sequential multiplicative generalized connectives). A sequential multiplicative generalized connective C consists of two sets of orthogonal partitions, O C ⊥ O * C : a set O C of partitions representing the right rules and a set O * C of partitions representing the left rules handled by the dual connective C * . By duality, the set O * C of left rules for C are exactly the set of right rules for the dual connective C * (i.e., O * C = O C * ).

  g., O D = {p : {(1, 2), (3)}} and O D * = {p * : {(1, 2, 3)}} do not define a sequential connective since O D ⊥ O D * ;

Figure 3 :

 3 Figure 3: Standard MLL Sequent Calculus

Figure 4 :

 4 Figure 4: axiom, cut, generalized links (on l.h.s.) and switching (on r.h.s.)

Figure 5 :

 5 Figure 5: reduction step of a generalized cut link

  e., the top border A, B together with the bottom border = (A ⊗ B) or = (A B): λ = {{(A, )), (B)}, {(A), (B, )}} and λ ⊗ = {{(D, , C)}}.

  By reflexivity, it is enough to indicate only one of the two organizations sets of a sequential connective, O C or O C * , while for a graphical connective we have to indicate a pair of pre-types.

Figure 9 :

 9 Figure 9: generalized decomposable connectives in proof net syntax

P 3 =

 3 { {(a,b),(c)}, {(a,c),(b)} } P 5 = {{(a, c), (b), (d, e), (f )}, {(b, c), (a), (d, f ), (e)}} P 4 = { {(a,b),(c),(d)}, {(c,d),(a),(b)} } P 6 = {(a, b), (c), (d, e), (f ), (g)}, {(a, c), (b), (f, g), (d), (e)} P 4 = {(a, b), (c, d), (e), (f ), (g), (h)}, {(e, f ), (g, h), (a), (b), (c), (d)} .

  , (a 3 , a 4 ), ..., (a n-1 , a n ), (b 1 ), ..., (b n )}, p 2 : {(b 1 , b 2 ), (b 3 , b 4 ), ..., (b n-1 , b n ), (a 1 ), ..., (a n )}

  g., class (a 2 , b 2 ), (a i , b i ), (a n , b n ) or (a 1 , .., a i-1 , ..., a n-1 , b 1 , ..., b i-1 , ..., b n-1 ) in Figure 10. 3. Finally, case 3 is not consistent (p 3 ⊥ q) because if we assume two classes like e.g. (a 1 , a 2 ) and (b 1 , b 2 ) belonging to p 3 , then we can chose q containing two classes like e.g. (a 1 , ..., a i-1 , ..., a n-1 , b 1 , ..., b i-1 , ..., b n-1

3 (p 3 2 . 3 .

 3323 has form (10)) contains a class (a, d, e). Both d and e are admissible restrictions of P . This means that, by Lemma 29 (via hypothesis of induction, P (↓a) is a type and p 3 has form (10)) d = b and e = c (resp., d = c and e = b); then, by playing with admissible restrictions, we get that p 1 (resp., p 2 ) will be inconsistent since it will contain by assumption class (a, b) (resp., class (a, c)) together with class (b, c), this latter occurring as consequence, by Lemma 29, of the restriction of p 3 by point a, i.e.: either p 1 = {(a, b), (b, c), x 3 ..., x n } ∈ P or p 2 = {(a, c), (b, c), y 3 ..., y n } ∈ P . Only one between d and e is an admissible restriction of P . Assume d is an admissible restriction of P (in addition to that one by a). By reasoning on restrictions (since by Lemma 29, via hypothesis of induction, the restriction of p 3 in (10) by d is equal either to p it must be either e = b or e = c. Assume e = c then, p 3 has form (11) below p 3 = {(a, d, c), z 2 , ..., z n }.

2 L

 2 Figure 14: normal form of decomposable entangled connectives

  an entangled connective that is undecomposable, by Definition 35 and Theorem 36. E.g., consider the Girard's undecomposable connective G 4 and G ⊥ 4 which is an entangled connective (by Definition 33): G 4 (resp., G ⊥ 4 ) results by the union (resp., by the intersection) of the types of bipolesF 1 = (1 ⊗ 2) (3 ⊗ 4) and F 2 = (2⊗3) (4⊗1)7 (resp., of the types of anti-bipolesF ⊥ 1 and F ⊥ 2 ) of Figure 9 i.e., G 4 = T F 1 ∪ T F 2 , (resp., G ⊥ 4 = T F ⊥ 1 ∩ T F ⊥ 2

Figure 15 :

 15 Figure 15: non sequentializable proof net with non decomposable conclusions G, G *

  Sequent calculus syntax for generalized connectives . . . . . . 9 3.1.1 Decomposable sequential connectives . . . . . . . . . . 10 3.2 Proof nets syntax for generalized connectives . . . . . . . . . . 11 3.2.1 Decomposable graphical connectives . . . . . . . . . . . 12 3.2.2 Proof structures with generalized links . . . . . . . . . 13 3.3 Sequentialization of decomposable connectives . . . . . . . . . 15 3.4 Undecomposable connectives . . . . . . . . . . . . . . . . . . . 16

	1 Introduction	2
	2 Partitions and orthogonality	6
	3 Generalized connectives	8
	3.1

  .

	Γ 1 , A 1 , ..., A i1 Γ 1 , ..., Γ p , C(A 1 , ..., A n ) ... Γ p , A p , ..., A ip	C	(1, ..., i 1 )	... C(1, ..., n)	(p, ..., i p )	C

  b), (c), x 3 , ..., x n }, p 2 : {(a, c), y 2 , y 3 , ..., y n } .

	By Lemma 29, via hypothesis of induction, the restriction of p 3 in form (11) by a must be equal either to p (↓a) 1 or to p (↓a) 2 ; this means,
	in particular, that class (d, c) of p	(↓a) 3

Every connective is immediately given together with its dual.

"Switchings should be seen as a dense subset of para-proofs", page 41 of[START_REF] Girard | On the meaning of logical rules I: syntax vs. semantics[END_REF].

Naively, a bipole B is a special MLL formula, introduced by Andreoli in[START_REF] Andreoli | Focussing and Proof Construction[END_REF], with only two layers of connectives: a generalized of generalized ⊗-sub-formulas. Bipoles have the nice feature that their pre-types are already types.

For this scope we consider partitions over cyclic permutations of linearly ordered sequences 1 < 2 < ... < n; see Section 6.

This is known as the key-step of cut-reduction: "a key-step between two partitions succeeds iff they are orthogonal" (see Lemma 1 of[START_REF] Danos | The structure of multiplicatives[END_REF]).

See Theorem 3 of[START_REF] Danos | The structure of multiplicatives[END_REF].

Notice that the respective literals indexes of the top borders of F 1 and F 2 are cyclic permutations of the linear sequence 1 < 2 < 3 < 4.

Naively, since, by the Curry-Howard isomorphism, "proofs are supposed to correspond to programs", what should be the program [π] corresponding to the non decomposable proof net π of G, G * (we met in Section 5)? if such a program does exist, is there any correspondence between the non-sequentializability of π and the possibly concurrent nature of such a program π * ? Have we a chance to write "a sequential version" of such a "concurrent program" [π]?

Proof. Assume P admits a non conservative restriction by a point a ∈ X that occurs as singleton class (a) both in p 1 and in p 2 i.e., P is in form (3), P = {p 1 = {(a), x 2 , ..., x n }, p 2 = {(a), y 2 , ..., y n }}, and let p 3 = p i=1,2 be a partition belonging to the type P ⊥⊥ . Point a must also occur in p 3 as singleton class (a), i.e. p 3 = {(a), z 2 , ..., z n }, otherwise we can find a partition q a i ∈ P ⊆ P ⊥ (by Proposition 25 and Lemma 27) s.t. the induced graph G(p 3 , q a i ) contains a cycle (where q a i denotes a partition of {q 1 , ..., q m } = (P (↓a) ) ⊥ in which point a has been "pumped" as in case (1) of Proposition 25). This implies p (↓a) 3 ⊥ q i , ∀q i ∈ (P (↓a) ) ⊥ , i.e., {p

i ) is ACC. Now, by assumption P (↓a) = (P (↓a) ) ⊥⊥ so, {p (↓a) 3 } ⊆ P (↓a) , by case 1 of Property 3. Otherwise, assume P admits only conservative restrictions by a point, i.e., assume P is a-restrictable as in form (4), P = {p 1 = {(a, b), x 2 , ..., x n }, p 2 = {(a, c), y 2 , ..., y n }} for some a in X. Then, point a cannot occur in p 3 as singleton class (a), otherwise, as before, we can find a partition q a i ∈ P ⊆ P ⊥ (by Proposition 25 and Lemma 27) s.t. graph G(p 3 , q a i ) has a disconnected component (where q a i denotes a partition of {q 1 , ..., q m } = (P (↓a) ) ⊥ in which the singleton class (a) has been "pumped" as in case (2) of Proposition 25). So p 3 is in form {(a, d), z 2 , ..., z n } and this means that p (↓a) 3 is orthogonal to every q i ∈ (P (↓a) ) ⊥ , i.e. {p (↓a) 3 } ⊥ (P (↓a) ) ⊥ (reasoning on the ACC induced graphs as before). Now, since by assumption P (↓a) is a type i.e., P (↓a) = (P (↓a) ) ⊥⊥ , we conclude that {p (↓a) 3 } ⊆ P (↓a) , by case 1 of Property 3.

Proposition 30 (conservative single point restrictable pairs). Assume P = {p 1 , p 2 } is a conservative single point restrictable entangled pair that is, P is an entangled pair s.t. (see Definition 22):

1. it admits only one restriction by a single point a and 2. the restriction P (↓a) is conservative.

Then:

1. the support X of P is given by the disjoint sum of next three segments

where S 1 and S 2 are defined as in the proof of Lemma 24, moreover 2. P is obtained by merging the entangled pair P 1 = {p 1 1 , p 1 2 } of form (1) together with the entangled pair P 2 = {p 2 1 , p 2 2 } of form (2) that is, Assume by absurdum p 3 ∈ P ⊥⊥ with p 3 = p i=1,2 . By Proposition 25 (case 2), a cannot occur as singleton class (a) in p 3 (otherwise, we get a disconnection in the induced graph G(q a i , p 3 ) for some pumped q a i ∈ P ⊥ ), therefore the restriction of p 3 by a must be conservative (i.e., p (↓a) 3 and p 3 have the same weight). Now, by hypothesis of induction, the restriction P (↓a) is a type thus, by Lemma 29, either p

2 ; so, a cannot occur in a class of p 3 containing more than three elements (including a). Then, we split our reasoning in two sub-cases depending on whether b is or not equal c in P of form [START_REF] Maieli | Modularity of proof nets: generating the type of a module[END_REF].

Case 2.1. If b = c then form ( 9) of P becomes that below:

By Proposition 25 (case 2) a cannot occur as singleton class (a) in p 3 . So, in case a does not also occur together with b in a class of p 3 then, by Lemma 29, b must occur alone as singleton class (b) in p 3 (by hypothesis of induction, P (↓a) is a type). Now, by Proposition 25 (case 2) there exists at least a partition q i in P ⊥ containing the singleton class (b), so G(p 3 , q i ) contains a disconnected component (contradicting p 3 ∈ P ⊥⊥ ). Otherwise, in case a occurs together with b in a class of p 3 then, we get a contradiction, since, by Lemma 29, either p 3 = p 1 or p 3 = p 2 (by hypothesis of induction, P (↓a) is a type). Case 2.2. In case b = c (w.r.t. P in form ( 9)), we distinguish two main sub-cases, depending on whether a belongs to a class of p 3 containing two or three elements of the domain. Case 2.2.2. Assume that a occurs in a class of p 3 containing three elements; hence p 3 has the form (10) below p 3 = {(a, d, e), z 2 , ..., z n }. [START_REF] Milner | Communicating and Mobile Systems: the Pi-Calculus[END_REF]