Nicolas Guenot

Lutz Straßburger

Symmetric Normalisation for Intuitionistic Logic

Keywords: F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic-Proof Theory Deep Inference, Intuitionistic Logic, Cut elimination

We present two proof systems for implication-only intuitionistic logic in the calculus of structures. The first is a direct adaptation of the standard sequent calculus to the deep inference setting, and we describe a procedure for cut elimination, similar to the one from the sequent calculus, but using a non-local rewriting. The second system is the symmetric completion of the first, as normally given in deep inference for logics with a DeMorgan duality: all inference rules have duals, as cut is dual to the identity axiom. We prove a generalisation of cut elimination, that we call symmetric normalisation, where all rules dual to standard ones are permuted up in the derivation. The result is a decomposition theorem having cut elimination and interpolation as corollaries.

Introduction

The calculus of structures [START_REF] Guglielmi | Non-commutativity and MELL in the calculus of structures[END_REF][START_REF] Guglielmi | A system of interaction and structure[END_REF] is a formalism for proof theory following the deep inference methodology, where inference rules do not only operate on the outer connective of formulas, but also arbitrarily deep inside formulas. As a consequence, there is no distinction between the object-level and the meta-level in the deductive system, and there is no "comma" or "branching" as in the sequent calculus.

On one side, this provides a greater freedom when designing new deductive systems such as completely local proof systems, as done in classical [START_REF] Brünnler | Atomic cut elimination for classical logic[END_REF] and linear logic [START_REF] Straßburger | MELL in the Calculus of Structures[END_REF][START_REF] Straßburger | Linear Logic and Noncommutativity in the Calculus of Structures[END_REF], or for proving new results as decomposition theorems [START_REF] Straßburger | MELL in the Calculus of Structures[END_REF][START_REF] Straßburger | A system of interaction and structure IV: The exponentials and decomposition[END_REF]. On the other side, this means that the traditional techniques applied in normalisation proofs cannot directly be used. As a consequence, methods for proving cut elimination in the calculus of structures have been developed, from the usual semantic arguments [START_REF] Brünnler | A local system for classical logic[END_REF] or rule permutations [START_REF] Straßburger | MELL in the Calculus of Structures[END_REF] to the use of graphical representations of proofs such as atomic flows [START_REF] Guglielmi | Breaking paths in atomic flows for classical logic[END_REF]. One of the most standard techniques involves using a splitting lemma [START_REF] Guglielmi | A system of interaction and structure[END_REF][START_REF] Guglielmi | A system of interaction and structure V: The exponentials and splitting[END_REF] that performs a complex, non-local transformation.

Unfortunately, all of these methods were developed for logics with a De Morgan duality. Although recently, several systems for intuitionistic logic in the deep inference setting have been proposed [START_REF] Tiu | A local system for intuitionistic logic[END_REF][START_REF] Brünnler | An algorithmic interpretation of a deep inference system[END_REF][START_REF] Gundersen | Atomic lambdacalculus, a typed lambda-calculus with explicit sharing[END_REF] and their relation to the λ-calculus has been investigated, no normalisation procedure has been given yet that would be entirely internal to the calculus of structures. Our goal is to give such a procedure for a basic intuitionistic system.

First, we define in Section 2 a proof system JS∪{i↑}, which has a shape typical for systems in the calculus of structures but is also close to the standard sequent calculus LJ, which is used for proving soundness and completeness in Section 3. The i↑ rule in this system corresponds to the cut rule of LJ, and it can be eliminated from any proof using the transformation described in Section 4, based on an upwards permutation of cuts. However, it relies on the fact that all cuts can be reduced to apply on atoms before starting to permute them. This is not possible in the sequent calculus, and it requires a non-local rewriting of the whole proof.

In order to devise a purely local procedure for normalisation, we move to the second step, where the JS system is completed into the fully symmetric system SJS, in which each down rule r↓ of JS is given a dual up rule r↑ -for example, cut is dual to the identity axiom. In this setting, described in Section 5, the two subsystems JS↓ (down rules) and JS↑ (up rules) can be separated to obtain a normal form, not only for proofs but for open derivations in general:

A SJS B → A JS↑ I JS↓ B ≡ - JS B when A is truth (1)
so that no up rule r1↑ can appear below a down rule r2↓. This is a generalisation of the standard cut elimination procedure, since in the case of a proof, where A is the truth unit, we can see by inspection of the rules of JS↑ that the upper part of the derivation must be empty, resulting in a normal proof in the JS system. Furthermore, the formula I in (1) is an interpolant for A and B. This gives us an alternative proof of the interpolation theorem for intuitionistic logic (see for example [START_REF] Mints | Interpolation theorems for intuitionistic predicate logic[END_REF]). The termination argument for normalisation relies on a complex measure based on flow-graphs, as found in [START_REF] Straßburger | MELL in the Calculus of Structures[END_REF][START_REF] Straßburger | A system of interaction and structure IV: The exponentials and decomposition[END_REF]. There are simpler normalisation proofs for deep inference systems using reducibility sets, as given for example in [START_REF] Gundersen | A proof of strong normalisation of the typed atomic lambda-calculus[END_REF][START_REF] Gimenez | The structure of interaction[END_REF], but these did not achieve full decomposition. We also think that the system presented here can be the basis for a systematic treatment of intermediate logics in the calculus of structures, as done in [START_REF] Ciabattoni | Structural extensions of display calculi: A general recipe[END_REF] for display calculi, and in [START_REF] Ciabattoni | From axioms to analytic rules in nonclassical logics[END_REF][START_REF] Ciabattoni | Expanding the realm of systematic proof theory[END_REF] for hypersequents.

An Intuitionistic Calculus of Structures

We consider first a system for implication-only intuitionistic logic presented in the calculus of structures [START_REF] Guglielmi | A system of interaction and structure[END_REF], a formalism based on deep inference, merging the object-level (usually formulas) and the meta-level (usually sequents) in a single level of structures. To define these objects, we assume given a countable set A of atoms, denoted by small latin letters such as a, b, c, the connective ⊃ for intuitionistic implication, and the constant t for intuitionistic truth, that will be left unit of the implication. Formally, we define the set of formulas by the grammar:

A, B ::= a | t | A ⊃ B (2)
As usual in deep inference, we consider equivalence classes of formulas, similar to sequents, where comma is commutative and associative in most systems.

Definition 1. The structures of our system are equivalence classes of formulas generated by the smallest congruence relation ≡ that is determined by the following equations:

t ⊃ A ≡ A A ⊃ (B ⊃ C) ≡ B ⊃ (A ⊃ C) (3)
The first equation makes t the left unit of ⊃ and the second allows the exchange of formulas on the left, corresponding to the exchange of formulas in the antecedent of a sequent. We sometimes make explicit the rewriting steps corresponding to the congruence, by using an inference rule ≡ which can be applied with premise A and conclusion B whenever A ≡ B. Note that implication is right associative, so that we can write A ⊃ B ⊃ C without ambiguity.

In the setting of deep inference, we have the ability to apply any inference rule inside some "context", which means rewriting a structure located inside another structure. In the intuitionistic framework, there are two kinds of contexts, the positive and the negative ones, on the left-hand side of an even (respectively odd) number of implications.

Definition 2. The positive and negative contexts, denoted by π and η respectively, are structures with a hole -, defined as:

π ::= -| η ⊃ A η ::= π ⊃ A
Note that for contexts the same equational theory (3) applies as for structures. In particular, the context -⊃ a ⊃ b can be written a ⊃ -⊃ b. A structure is obtained by replacing the hole with some structure, written π{A} or η{A}, respectively. Notice that positive contexts preserve the polarity of a context plugged inside, and negative contexts invert it. A substructure occurrence A of some B is in positive position if B = π{A} for a positive context π, and in negative position if B = η{A} for some negative η. We write ∆ ⊃ B, where ∆ is a multiset {A1, . . . , An} of structures, to denote A1 ⊃ • • • ⊃ An ⊃ B, and by extension we will write π{∆} or η{∆} when a context is of the shape η0{-⊃ B } or π0{-⊃ B }, respectively. This notation is overloaded, so that π{∆} is π{A} when ∆ is the singleton {A}, and similarly η{∆} is η{A}.

Example 3. Given two contexts π{-} = a ⊃ (-⊃ b) ⊃ c and η{-} = -⊃ d, and multisets Γ = {F } and ∆ = {a, G}, we have π{F } = a ⊃ (F ⊃ b) ⊃ c, and η{∆} = a ⊃ G ⊃ d as well as π{η{Γ}} = a ⊃ ((F ⊃ d) ⊃ b) ⊃ c.
In the calculus of structures, an inference rule must always have exactly one premise. A rule instance is obtained by applying the scheme of a rule on particular structures, inside a context. Then, a derivation D has one premise A and a conclusion B, and a proof D ′ of B is some derivation with premise t and conclusion B. In this context, we use the standard notations of the calculus of structures for such objects:

A D B and - D ′

B

The specific rules used in the system JS ∪ {i↑} are shown in Figure 1. The cut-free system JS is obtained by removing the i↑

π{∆} i↓ --------------------- π{(∆ ⊃ A) ⊃ A} η{(∆ ⊃ A) ⊃ A} i↑ --------------------- η{∆} π{B } w↓ ------------- π{A ⊃ B } π{((A ⊃ B) ⊃ C) ⊃ D } s↓ ------------------------------ π{A ⊃ (B ⊃ C) ⊃ D } π{A ⊃ A ⊃ B } c↓ ------------------- π{A ⊃ B } Figure 1.
Inference rules for the system JS ∪ {i↑} rule of cut. In an instance of i↓ or i↑, the structure A introduced in the conclusion or premise respectively, is called principal structure. This system has a typical shape for deep inference, and it is related to the classical system KS [START_REF] Brünnler | Atomic cut elimination for classical logic[END_REF]. Apart from the switch rule s↓, rules are similar to those of the sequent calculus, with a variation on the identity rule. There, the structures in ∆ are carried over, as they have to be proved for the conclusion to hold -note that an equivalent rule has been proposed for the sequent calculus [START_REF] Schroeder-Heister | Implications-as-rules versus implicationsas-links: an alternative implication-left schema for the sequent calculus[END_REF].

Remark 4. The identity rule i↓ can only be applied when the notation π{∆} is meaningful, which means that either π{-} is not -, so that the structures carried over appear on the left of an implication, or ∆ is reduced to a single structure B. The standard identity rule can be recovered by considering that ∆ is {t}, since a proof is a derivation with premise t.

Example 5. Here are two valid derivations in JS ∪ {i↑}:

t ⊃ A ≡ ------ A w↓ ------- B ⊃ A i↓ ---------------------- ((B ⊃ A) ⊃ A) ⊃ A i↑ ---------------------- B ⊃ A (C ⊃ D ⊃ B) ⊃ (C ⊃ D ⊃ B) ⊃ B c↓ ---------------------------------------- (C ⊃ D ⊃ B) ⊃ B i↓ ------------------------------------ (((C ⊃ D ⊃ A) ⊃ A) ⊃ B) ⊃ B s↓ ------------------------------------ (C ⊃ D ⊃ A) ⊃ (A ⊃ B) ⊃ B ≡ ---------------------------------- (A ⊃ B) ⊃ (C ⊃ D ⊃ A) ⊃ B
Because of the choices in its design, JS ∪ {i↑} is quite different from other intuitionistic systems in deep inference [START_REF] Tiu | A local system for intuitionistic logic[END_REF][START_REF] Brünnler | An algorithmic interpretation of a deep inference system[END_REF]. Nonetheless, it has the properties that one expects of a system in this setting -concerning the identity rule, cut and its elimination: we do not investigate atomic contraction here, although it usually possible to obtain it in deep inference [START_REF] Tiu | A local system for intuitionistic logic[END_REF]. We can, for example, always reduce the i↓ rule to the form where the principal structure is an atom:

π{∆} ai↓ -------------------- π{(∆ ⊃ a) ⊃ a} (4)
and we call this rule atomic identity. The reduction of any instance of the general identity to several instances of the atomic identity rule is straightforward, as in the sequent calculus.

Proposition 6. The rule i↓ is derivable for {s↓, ai↓}.

Proof. Given an instance r of i↓, we proceed by induction on the number of atoms in the principal structure A of r. If A is simply an atom a, we are done. In general, A has the shape B ⊃ C, we use the rewriting from:

π{∆} i↓ -------------------------------------- π{(∆ ⊃ (B ⊃ C)) ⊃ (B ⊃ C)}
to the derivation below, and conclude by induction hypothesis.

π{∆} i↓ --------------------- π{(∆ ⊃ C) ⊃ C } ≡ -------------------------- π{(t ⊃ ∆ ⊃ C) ⊃ C } i↓ ------------------------------------------- π{(((t ⊃ B) ⊃ B) ⊃ ∆ ⊃ C) ⊃ C } s↓ ------------------------------------------- π{(t ⊃ B) ⊃ (B ⊃ ∆ ⊃ C) ⊃ C } ≡ ----------------------------------------- π{(∆ ⊃ (B ⊃ C)) ⊃ (B ⊃ C)}
Furthermore, we have the following property of the switch rule, that can be used to push structures inside contexts, based on the idea that inside a formula, a t unit can be created anywhere using the congruence, as a placeholder where a formula can be plugged.

Lemma 7. For π and ρ positive contexts, there is a derivation in {s↓} from π{ρ{A} ⊃ B } to π{A ⊃ ρ{t} ⊃ B }.

Proof. We proceed by induction on ρ{-}. In the base case, we use the congruence. In the inductive case, for some C and D we have ρ{-} = (ρ ′ {-} ⊃ C) ⊃ D. We use the following derivation:

π{((ρ ′ {A} ⊃ C) ⊃ D) ⊃ B } D π{((A ⊃ ρ ′ {t} ⊃ C) ⊃ D) ⊃ B } s↓ ----------------------------------------- π{A ⊃ ((ρ ′ {t} ⊃ C) ⊃ D) ⊃ B }
where D exists by induction hypothesis.

Relation to the Sequent Calculus

The simplest way to prove JS ∪ {i↑} suitable for intuitionistic logic is to prove soundness and completeness with respect to the sequent calculus shown in Figure 2, based on the definition of formulas given in (2). This will require translations between structures and sequents: for any structure, pick a representation A and translate it into ⊢ A. Conversely, given any sequent, we proceed by induction on the length of the antecedent to find its representation:

Γ, A ⊢ B S = Γ ⊢ A ⊃ B S ⊢ A S = A Theorem 8 (Soundness of JS∪{i↑}). If A is provable in JS∪{i↑}, then the sequent ⊢ A is provable in LJ ∪ {cut}.
Proof. We proceed by structural induction on any proof D of A in JS ∪ {i↑}. In the base case, when D is just the structure t, we can use the t R rule. In the general case, we consider the bottommost instance r in D, as shown below on the left:

- D ′ π{C } r ------- π{B } →
? ? ? ? ?

Π ′
⊢ π{C } ? ? ? ? ?

Π ′′ π{C } ⊢ π{B } cut ------------------------------- π{B }
Any rule instance r can be considered to follow the scheme shown above, including the ones defined in a negative context, because such a context must be contained in a positive context. By case analysis on r one can show that C ⊢ B is provable in LJ ∪ {cut}note that whenever C ≡ B then B ⊢ C and C ⊢ B are provable. From a proof of C ⊢ B in LJ ∪ {cut} we obtain the proof Π ′′ of π{C } ⊢ π{B }, by induction on π. Therefore, we can build the proof shown above on the right, where Π ′ exists by induction hypothesis, applied on D ′ .

Theorem 9

(Completeness of JS ∪ {i↑}). If a sequent Γ ⊢ A is provable in LJ ∪ {cut}, then Γ ⊢ A S is provable in JS ∪ {i↑}.
Proof. We proceed by structural induction on some proof Π of Γ ⊢ A in LJ ∪ {cut}, using a case analysis on the bottommost instance r in Π. We only show the ⊃ L case below. ? ? ? ? ? ?

Π 1
∆ ⊢ B ? ? ? ? ? ? ?

Π 2 Ψ, C ⊢ A ⊃ L -------------------------- ∆, Ψ, B ⊃ C ⊢ A → - D 2 Ψ ⊃ C ⊃ A ≡ --------------------- Ψ ⊃ (t ⊃ C) ⊃ A D ′ 1 Ψ ⊃ ((∆ ⊃ B) ⊃ C) ⊃ A s↓ * = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = ∆ ⊃ Ψ ⊃ (B ⊃ C) ⊃ A ax ------- A ⊢ A Γ ⊢ A ∆, A ⊢ B cut ------------------------- Γ, ∆ ⊢ B t R --- ⊢ t Γ ⊢ B wk ---------- Γ, A ⊢ B Γ, A, A ⊢ B ct -------------- Γ, A ⊢ B Γ ⊢ A t L --------- Γ, t ⊢ A Γ, A ⊢ B ⊃ R ------------- Γ ⊢ A ⊃ B Γ ⊢ A ∆, B ⊢ C ⊃ L ------------------------- Γ, ∆, A ⊃ B ⊢ C Figure 2
. Inference rules for system LJ ∪ {cut}

By induction hypothesis we produce proofs D1 of ∆ ⊢ B S and D2 of Ψ, C ⊢ A S , and D ′ 1 is obtained by plugging D1 inside the context Ψ ⊃ (-⊃ C) ⊃ A. In the translation, s↓ * denotes the sequence of s↓ needed to move all structures from ∆ to the left of B (as done in Lemma 7). The case for cut is similar but it uses i↑, and all other cases are straightforward.

As the cut rule in LJ ∪ {cut}, the rule i↑ is admissible in the JS ∪ {i↑} system. One proof of this can be obtained directly from the translation above: the completeness proof of JS ∪ {i↑} uses i↑ only for translating a cut instance. Thus, cut elimination for LJ entails cut elimination for JS. However, in the following, we give another proof, using an internal cut elimination procedure described in terms of permutation of rule instances.

Cut Elimination

The procedure we will present here is based on the permutation of inference rules, similar to what can be seen in the sequent calculus. However, permuting rule instances in a system with deep inference can be more involved than in the traditional, shallow formalisms, because of the freedom offered when composing or modifying the structures. As a consequence, the induction measure used to show that the permutation process terminates needs to keep track of the relationship between occurrences of structures and substructures in a given derivation. For this, we will use a variant of the notion of logical flow-graphs [START_REF] Buss | The undecidability of k-provability[END_REF].

Definition 10. An occurrence of t in a structure is non-trivial if it occurs on the right-most position in a substructure not equal to t via equations (3), otherwise it is called trivial.

In other words, non-trivial occurrences of t are those that cannot be removed using equations (3), except when consider t as a whole structure. Conversely, every structure has a representation with no trivial t occurrence. Definition 11. A particle in a derivation D is an occurrence of an atom or a non-trivial occurrence of t in a structure in D.

Definition 12. The head of a structure A is the rightmost particle in A; a particle is positive (respectively, negative) if it is in positive (respectively, negative) position.

Definition 13. The down-flow-graph G (D) of a derivation D is the directed graph whose vertices are the negative particles of D, such that there is an edge from a negative particle p to a negative particle q, if and only if p occurs in the premise of a rule instance r in D and q occurs in the conclusion of the same instance r, and one of the following conditions holds:

1. p and q are the same occurrence in the context π{-} or η{-} of r (as shown in Figure 1), or 2. p and q are the same occurrence in one of B, C, D, ∆ in an instance of w↓, c↓, s↓, i↓, or i↑ (see Figure 1), or

π1{Ψ} r1↓ -------- π1{F } ai↑ -------- π0{F } (1) -→ π1{Ψ} ai↑ -------- π0{Ψ} r1↓ -------- π0{F } π{∆ ⊃ a} ai↓ ---------------------------- π{((∆ ⊃ a) ⊃ a) ⊃ a} ai↑ ---------------------------- π{∆ ⊃ a} (3) -→ π{∆ ⊃ a} π{B } w↓ ------------- π{F ⊃ B } ai↑ ------------- π{∆ ⊃ B } (6) -→ π{B } w↓ * = = = = = = = = = = = = = = π{∆ ⊃ B } η1{F } r1↓ -------- η0{F } ai↑ -------- η0{∆} (2) -→ η1{F } ai↑ -------- η1{∆} r1↓ -------- η0{∆} η{a} ai↓ ------------------- η{(a ⊃ a) ⊃ a} ai↑ ------------------- η{a} (4) -→ η{a} π{F ⊃ F ⊃ B } c↓ ------------------- π{F ⊃ B } ai↑ ------------- π{∆ ⊃ B } (7) -→ π{F ⊃ F ⊃ B } ai↑ ------------------- π{F ⊃ ∆ ⊃ B } ai↑ ------------------- π{∆ ⊃ ∆ ⊃ B } c↓ * = = = = = = = = = = = = = = = = = = = = π{∆ ⊃ B } π{((B ⊃ ∆ ⊃ a) ⊃ a) ⊃ C } s↓ ----------------------------------- π{B ⊃ ((∆ ⊃ a) ⊃ a) ⊃ C } ai↑ ----------------------------------- π{B ⊃ ∆ ⊃ C } (5) -→ π{((B ⊃ ∆ ⊃ a) ⊃ a) ⊃ C } ai↑ ----------------------------------- π{B ⊃ ∆ ⊃ C } Figure 3.
Reduction steps for atomic cut elimination in JS ∪ {ai↑}, where F = (∆ ⊃ a) ⊃ a 3. p and q are the same occurrence in the A in an instance of s↓ (see Figure 1), or 4. p occurs inside one of the two A in the premise of a c↓, and q is the same occurrence in the A in the conclusion of the c↓ (see Figure 1).

An edge in G (D) is also called a down edge.

Definition 14. The multiplicity of a (negative) particle p in a derivation D is the number of particles q in D, such that there is a path from q to p in G (D) and no incoming edges to q.

Example 15. In the derivation below we show all down edges. The multiplicity of a in the conclusion is 3, the one of c is 2.

((((a ⊃ a ⊃ b) ⊃ c) ⊃ a ⊃ b) ⊃ c) ⊃ d c↓ ----------------------------------------------- ((((a ⊃ b) ⊃ c) ⊃ a ⊃ b) ⊃ c) ⊃ d s↓ ----------------------------------------- ((a ⊃ b) ⊃ c) ⊃ ((a ⊃ b) ⊃ c) ⊃ d c↓ ----------------------------------------- ((a ⊃ b) ⊃ c) ⊃ d
Definition 16. The height of a derivation D, denoted by h(D), is the number of rule instances in D.

Lemma 17. For any positive context π and a structure A, if π{A} is provable in JS then π{t} is also provable in JS.

The proof of this lemma uses a straighforward induction on the height of the derivation. We are now ready to see our cut elimination, which is done in two stages. First, we reduce cuts to their atomic form, which is dual to atomic identity (4):

η{(∆ ⊃ a) ⊃ a} ai↑ -------------------- η{∆} (5)
In JS ∪ {i↑}, the reduction from general to atomic cuts is achieved via the non-local rewriting called merging described in Lemma 18 below. For stating it, we need contexts with more than one hole. The notation π{A1 } . . . {An } denotes a structure with substructures A1 to An in positive positions. Replacing one Ai with a holeproduces an ordinary positive context. The object π{-} . . . {-}, which is obtained by replacing each of A1, . . . , An with a hole -, is called an n-ary positive context.

Lemma 18 (Merging). Let η be a negative context, let π be an n-ary positive context, and let A and B be structures. For every proof

D of η{A ⊃ π{t} . . . {t} ⊃ B } in JS ∪ {ai↑}, there is also a proof D ′ of η{π{A} . . . {A} ⊃ B } in JS ∪ {ai↑}.
Proof. Let m1, . . . , mn be the multiplicities of the n distinguished occurrences of t in π{t} . . . {t} in the conclusion of D, and let m = n i=1 mi. We proceed by induction on the pair (m, h(D)), under lexicographic ordering, using a case analysis on the instance r at the bottom of D:

1. If r acts inside A, we can use the induction hypothesis on the proof D1 above r, and apply n instances of r, one inside each hole in π:

η{A ′ ⊃ π{t} . . . {t} ⊃ B } r -------------------------------- η{A ⊃ π{t} . . . {t} ⊃ B } -→ η{π{A ′ } . . . {A ′ } ⊃ B } r * = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = η{π{A} . . . {A} ⊃ B }
and if A ′ is just t, we need no induction hypothesis. Notice that since we start with a proof, this case must occur eventually. 2. If r acts inside B or inside η, we can proceed immediately by induction hypothesis. 3. If r acts inside π{t} . . . {t}, we have some subcases:

• If r is weakening, we proceed immediately by induction hypothesis. (If r deletes all the "holes" of π, then we also need Lemma 17 for building D ′ .) • If r is a contraction, possibly duplicating some "holes" of π, observe that even though n increases through instances of c↓, the sum of the mi cannot. Thus, we can proceed by induction hypothesis. • If r is a switch, note that it is a purely linear rule, moving substructures around but keeping their polarity. Thus, m is preserved, and we can we proceed by induction hypothesis. • If r is an identity removing a pair of substructures, there are three possibilities: None of the distinguished occurrences of t is affected. We proceed by induction hypothesis. Some of the t are inside the removed substructures. As in the weakening case, we can proceed by induction hypothesis.

We have a situation where r is an i↓, and one (or more) of the distinguished occurrences of t is inside the ∆ that goes through the identity. More precisely, we have

π{t} . . . {t} = ρ{(t ⊃ • • • ⊃ t ⊃ ∆ ⊃ F ) ⊃ F } (6)
for some (unary) positive context ρ, such that all the t on the right in (6) are in one of the holes on the left (but not all holes on the left need to be as shown on the right).

Then we have the following situation:

η{A ⊃ ρ{t, . . . , t, ∆} ⊃ B } i↓ --------------------------------------------------- η{A ⊃ ρ{(t ⊃ • • • ⊃ t ⊃ ∆ ⊃ F ) ⊃ F } ⊃ B } (7)
where ρ{t, . . . , t, ∆} ⊃ B is

t ⊃ • • • ⊃ t ⊃ ∆ ⊃ B if ρ{-} = {-} ν{t ⊃ • • • ⊃ t ⊃ ∆ ⊃ X } ⊃ B if ρ{-} = ν{-⊃ X }
for some negative context ν and some structure X. We can now replace (7) above by

η{ρ ′ {A, . . . , A, ∆ ′ } ⊃ B } i↓ ----------------------------------------------------- η{ρ ′ {(A ⊃ • • • ⊃ A ⊃ ∆ ′ ⊃ F ) ⊃ F } ⊃ B }
and proceed by induction hypothesis. Here, ρ ′ and ∆ ′ are obtained from ρ and ∆, respectively, by replacing the distinguished occurrences of t in π by A, so that

ρ ′ {(A ⊃ • • • ⊃ A ⊃ ∆ ′ ⊃ F ) ⊃ F } = π{A} . . . {A}. 4.
If r is a s↓ moving a structure A ′ from the context ν to the left of A, we apply the induction hypothesis to the proof above this s↓ and proceed as follows, with η{-} = ρ{-⊃ D }:

ρ{((A ′ ⊃ A) ⊃ π{t} . . . {t} ⊃ B) ⊃ D } s↓ ------------------------------------------------- ρ{A ′ ⊃ (A ⊃ π{t} . . . {t} ⊃ B) ⊃ D } -→ ρ{(π{A ′ ⊃ A} . . . {A ′ ⊃ A} ⊃ B) ⊃ D } D s↓ ρ{A ′ ⊃ • • • ⊃ A ′ ⊃ (π{A} . . . {A} ⊃ B) ⊃ D } c↓ * = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = ρ{A ′ ⊃ (π{A} . . . {A} ⊃ B) ⊃ D }
where we use n -1 instances of c↓ to get n copies of A ′ , and where the derivation D consisting of s↓ is obtained by applying n times Lemma 7. 5. If r is a w↓ erasing A ⊃ π{t} . . . {t} ⊃ B, we use w↓ to obtain D ′ without using the induction hypothesis. 6. If r is a c↓ duplicating A ⊃ π{t} . . . {t} ⊃ B, we rewrite premise and conclusion, and apply the induction hypothesis twice, as the multiplicity of the copies is less than the original, which included all of the mi.

The second stage of cut elimation is a permutation argument moving all the ai↑ instances towards the top of the derivation, where they must eventually disappear. The key observation is that these permutations will be simpler than expected because atomic cuts interact less with other rules than general cuts.

Lemma 19. For any given proof D in JS ∪ {i↑}, there is a proof in JS ∪ {ai↑} with the same conclusion.

Proof. Let the rank of a cut be the size of its principal structurethe A in i↑ in Figure 1. We proceed by induction, using the multiset of the ranks of all cuts in D as induction measure. If all cuts are atomic we are done and D is a proof in JS ∪ {ai↑}. Otherwise, we consider the topmost i↑ instance in D with a non-atomic principal structure B ⊃ C and rewrite D as:

- D 1 η{B ⊃ (∆ ⊃ (B ⊃ C)) ⊃ C } ≡ -------------------------------------- η{(∆ ⊃ (B ⊃ C)) ⊃ (B ⊃ C)} i↑ -------------------------------------- η{∆} -→ - D ′ 1 η{(∆ ⊃ (B ⊃ B) ⊃ C) ⊃ C } i↑ ------------------------------------ η{(∆ ⊃ C) ⊃ C } i↑ --------------------- η{∆}
where D ′ 1 is obtained from D1 by Lemma 18, after observing that the premise of the cut can be rewritten via ≡ to have the shape of the structure considered in that lemma.

Lemma 20 (Atomic cut elimination). Any proof in JS ∪ {ai↑} without non-atomic i↓ instances can be turned into a JS proof.

Proof. By induction on the number of ai↑ instances in the proof; if there is any, consider the topmost one. Let D be the cut-free derivation above, and let m be the multiplicity in D of the head of F = (∆ ⊃ a) ⊃ a in the premise of this ai↑ instance. We proceed by a second induction on the pair (m, h(D)), and show that this ai↑ can be eliminated, using a case analysis on the bottommost instance r1 in D -see the list of cases in Figure 3: 1-2. If our ai↑ and r1 operate on unrelated structures, we can trivially permute ai↑ above r1, and proceed by induction hypothesis, as h(D) has decreased. 3-4. If r1 is an identity ai↓ matching our ai↑, then both instances can disappear and we conclude by the main induction hypothesis, since one cut was erased. 5. If r1 is a s↓ moving some structure to the left of the positive a introduced in the cut, we assimilate it in the ai↑ instance and go on by induction hypothesis, as h(D) decreased. 6. If r1 is a w↓ erasing both principal atoms of our ai↑, we can remove the cut, keep the w↓ and then conclude by the main induction hypothesis, as one cut was erased. 7. If r1 is a c↓ duplicating the two principal atoms of our ai↑, we copy the cut, compose the two copies and apply the induction hypothesis twice. This is possible because both new ai↑ have smaller multiplicity, and no transformation from Figure 3 can increase the multiplicity of any particle introduced in a cut.

Theorem 21 (Cut elimination). Any proof of A in JS ∪ {i↑} can be transformed into a proof of A in JS.

Proof. By Lemma 19 we make cut instances atomic, then we apply Proposition 6 to make identity instances atomic. Finally, we can conclude by applying Lemma 20.

This cut elimination procedure is not local, because merging in Lemma 18 rewrites the whole proof, when making all cuts atomic by Lemma 19. To solve this we need a derivation or inference rule to perform the merging transformation of:

η{B ⊃ (∆ ⊃ B ⊃ C) ⊃ C } ≡ -------------------------------------- η{(∆ ⊃ (B ⊃ C)) ⊃ (B ⊃ C)} i↑ -------------------------------------- η{∆} (8)
into the derivation: ----------------------------------

η{B ⊃ (∆ ⊃ B ⊃ C) ⊃ C } = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = = η{(∆ ⊃ (B ⊃ B) ⊃ C) ⊃ C } i↑ -
- η{(∆ ⊃ C) ⊃ C } i↑ --------------------- η{∆} (9)
This is the motivation for the symmetric system introduced in the next section.

Symmetric Normalisation

The missing piece to decompose cuts to their atomic form as shown in (9) is the rule s↑, dual to the switch s↓ rule, which allows to move a substructure in positive position outside of some deep contextthe opposite of moving a structure deeper inside other structures, as done by the switch rule in Lemma 7. This logically leads us to the completion of JS ∪ {i↑} into the symmetric system SJS, following the usual scheme in deep inference [START_REF] Brünnler | Atomic cut elimination for classical logic[END_REF][START_REF] Straßburger | MELL in the Calculus of Structures[END_REF]. In the intuitionistic setting, where DeMorgan duality does not exist, the dual of a rule is obtained by inverting premise and conclusion, and then using the result in the opposite context.

π{∆} i↓ --------------------- π{(∆ ⊃ A) ⊃ A} η{(∆ ⊃ A) ⊃ A} i↑ --------------------- η{∆} π{((A ⊃ B) ⊃ C) ⊃ D } s↓ ------------------------------ π{A ⊃ (B ⊃ C) ⊃ D } η{A ⊃ (B ⊃ C) ⊃ D } s↑ ------------------------------ η{((A ⊃ B) ⊃ C) ⊃ D } π{A ⊃ A ⊃ B } c↓ ------------------- π{A ⊃ B } η{A ⊃ B } c↑ ------------------- η{A ⊃ A ⊃ B } π{B } w↓ ------------- π{A ⊃ B } η{A ⊃ B } w↑ ------------- η{B } Figure 4.
Inference rules for the symmetric system SJS Starting from the same definitions, as used in JS ∪ {i↑}, we add the whole up fragment {i↑, c↑, w↑, s↑} to JS, and we call the resulting system SJS, for which the set of inference rules is shown in Figure 4. In this extension, the basic JS system is called the down fragment, also denoted by JS↓, and we will write JS↑ to denote the up fragment. Many properties of JS are kept in SJS, and in particular the rule i↓ can be reduced to atomic form, using the same transformation as for JS in Proposition 6. But due to the new duality, the rule i↑ can also be reduced to its atomic form, without applying Lemma 18 or any other non-local transformation.

Proposition 22. The rule i↑ is derivable for {s↑, ai↑}.

Proof. This is dual to Proposition 6: we proceed by induction on the principal structure of the cut. At each step, the cut is decomposed into two cuts on smaller structures by using a s↑ instance, as shown in (9).

Another standard property of any such symmetric system in the calculus of structures is that the dual of any rule can be derived by using cut and identity.

Proposition 23. Any up rule r↑ is derivable for {i↓, i↑, r↓}, and dually any down rule r↓ is derivable for {i↓, i↑, r↑}.

Proof. From any given r↓ we can derive r↑ and dually r↓ from r↑, as follows:

π{B } r↓ ------- π{A} , η{A} r↑ ------- η{B } -→ η{A} i↓ --------------------- η{(B ⊃ B) ⊃ A} r↓ --------------------- η{(B ⊃ A) ⊃ A} i↑ --------------------- η{B }
This definition of SJS as a symmetric extension of the basic JS system leads to a simple proof of adequacy with respect to the standard sequent calculus LJ for intuitionistic logic, even though the language of proofs in SJS is much richer.

Theorem 24. A structure A is provable in the SJS system if and only if the sequent ⊢ A is provable in LJ ∪ {cut}.

Proof. Completeness is immediate from Theorem 9, since JS∪{i↑} is a subset of the SJS system. Then, soundness can be proved by using Proposition 23 and Theorem 8.

As mentioned before, the new up-down symmetry appearing in the inference rules of SJS allows us to prove cut elimination with local rule permutations only. Furthermore, we are able to state and prove a strong decomposition theorem inside SJS that generalises cut elimination by separating more groups of rules than the up and down fragments.

Theorem 25 (Decomposition). Any derivation can be decomposed in SJS as shown on the left below, and any proof can be turned into one of the shape shown on the right below:

P SJS Q → P {c↑} P ′ {w↑} P ′′ {s↑} P ′′′ {i↑} I {i↓} Q ′′′ {s↓} Q ′′ {w↓} Q ′ {c↓} Q - SJS Q → - {i↓} Q ′′′ {s↓} Q ′′ {w↓} Q ′ {c↓} Q (10)
Before proving this in the remainder of this section, we observe that it entails cut elimination but also gives a new proof for Craig's interpolation theorem in intuitionistic logic [START_REF] Mints | Interpolation theorems for intuitionistic predicate logic[END_REF]. For any given provable formula P ⊃ Q, there is a derivation from P to Q in SJS, and the formula I obtained by decomposition (10) is an interpolant of P and Q. Such a strong decomposition theorem, immediately entailing interpolation, has to our knowledge only be obtained for classical propositional logic [START_REF] Brünnler | Deep Inference and Symmetry in Classical Proofs[END_REF] and for the multiplicative and exponential fragment of linear logic [START_REF] Straßburger | Linear Logic and Noncommutativity in the Calculus of Structures[END_REF]. Proving Theorem 25 requires a generalisation of Definition 13. Definition 26. For a derivation D, its (full) flow-graph G (D) is the directed graph whose vertices are all the particles of D and whose set of edges is the union of the sets of down edges, up edges, down-left edges, up-left edges and pure left edges:

• A down edge is defined as an edge between negative particles p and q in D as in Definition 13, with the difference that in 2) we include the rules w↑, c↑, and s↑, and in 3) we include the rule s↑. We also add: 5. p is an occurrence in the A in the premise of a c↑, and q is the same occurrence in one of the two A in the conclusion of the c↑. • An up edge is defined dually between positive particles p and q going upwards, so for having an edge from p to q, the positive particle p must occur in the conclusion of a rule instance r and q must occur in the premise of the same rule instance r. • There is an down-left edge from some negative particle p to a negative particle q, if and only if p is the head of C in the premise of some instance of s↓ and q is the head of A in the conclusion of that s↓. • Dually, there is an up-left edge from some positive particle p to a positive particle q, if and only if p is the head of C in the conclusion of some instance of s↑ and q is the head of A in the premise of that s↑. • Finally, there is a pure left edge from p to q, if and only if either p is the head of B and q is the head of A in the premise of an instance of s↓, or dually, p is the head of B and q the head of A in the conclusion of a s↑ instance.

Observe that the pure left edges are the only ones connecting particles of different polarities in a flow-graph. ---------------------------- ---------------------------------- --------------------------------- η{A ---------------------------------- ---------------------------------- ---------------------------------------- Here is a derivation and its complete flow-graph:

η{E ′ ⊃ D } r -------------- η{E ⊃ D } c↑ ------------------- η{E ⊃ E ⊃ D } (1) -→ η{E ′ ⊃ D } c↑ --------------------- η{E ′ ⊃ E ′ ⊃ D } r --------------------- η{E ′ ⊃ E ⊃ D } r -------------------- η{E ⊃ E ⊃ D } η ′ {E ⊃ D } r -------------- η{E ⊃ D } c↑ ------------------- η{E ⊃ E ⊃ D } (2) -→ η ′ {E ⊃ D } c↑ -------------------- η ′ {E ⊃ E ⊃ D } r -------------------- η{E ⊃ E ⊃ D } π{C ′ ⊃ C ′ ⊃ D } c↓ --------------------- π{C ′ ⊃ D } c↑ -------------- π{C ⊃ D } (3) -→ π{C ′ ⊃ C ′ ⊃ D } c↑ --------------------- π{C ⊃ C ′ ⊃ D } c↑ -------------------- π{C ⊃ C ⊃ D } c↓ ------------------- π{C ⊃ D } π{D } w↓ -------------- π{C ′ ⊃ D } c↑ -------------- π{C ⊃ D } (4) -→ π{D } w↓ ------------- π{C ⊃ D } π{((A ⊃ D) ⊃ E) ⊃ F } s↓ ------------------------------ π{A ⊃ (D ⊃ E) ⊃ F } c↑ ---------------------------------- π{A ⊃ (D ⊃ D ⊃ E) ⊃ F } (5) -→ π{((A ⊃ D) ⊃ E) ⊃ F } c↑ --------------------------------------------- π{((A ⊃ D) ⊃ (A ⊃ D) ⊃ E) ⊃ F } s↓ -------------------------------------------- π{A ⊃ (D ⊃ (A ⊃ D) ⊃ E) ⊃ F } s↓ ------------------------------------------ π{A ⊃ A ⊃ (D ⊃ D ⊃ E) ⊃ F } c↓ ---------------------------------------- π{A ⊃ (D ⊃ D ⊃ E) ⊃ F } η{A ⊃ (B ⊃ C) ⊃ D } s↑ -
- η{((A ⊃ B) ⊃ C) ⊃ D } c↑ -
- η{((A ⊃ A ⊃ B) ⊃ C) ⊃ D } (6) -→ η{A ⊃ (B ⊃ C) ⊃ D } c↑ -
⊃ A ⊃ (B ⊃ C) ⊃ D } s↑ -
- η{A ⊃ ((A ⊃ B) ⊃ C) ⊃ D } s↑ -
- η{((A ⊃ A ⊃ B) ⊃ C) ⊃ D } η{A ⊃ (B ⊃ C) ⊃ D } s↑ ------------------------------ η{((A ⊃ B) ⊃ C) ⊃ D } c↑ ----------------------------------------------------- η{((A ⊃ B) ⊃ C) ⊃ ((A ⊃ B) ⊃ C) ⊃ D } (7) -→ η{A ⊃ (B ⊃ C) ⊃ D } c↑ -
- η{A ⊃ (B ⊃ C) ⊃ (B ⊃ C) ⊃ D } c↑ ------------------------------------------------ η{A ⊃ A ⊃ (B ⊃ C) ⊃ (B ⊃ C) ⊃ D } ≡ ------------------------------------------------ η{A ⊃ (B ⊃ C) ⊃ A ⊃ (B ⊃ C) ⊃ D } s↑ -------------------------------------------------- η{A ⊃ (B ⊃ C) ⊃ ((A ⊃ B) ⊃ C) ⊃ D } s↑ ----------------------------------------------------- η{((A ⊃ B) ⊃ C) ⊃ ((A ⊃ B) ⊃ C) ⊃ D }
((a ⊃ d) ⊃ e) ⊃ f s↓ ---------------------- a ⊃ (d ⊃ e) ⊃ f c↑ ------------------------- a ⊃ (d ⊃ d ⊃ e) ⊃ f
Lemma 28. Any derivation in the SJS system can be transformed in the following two ways:

P SJS Q → P {c↑} P ′ SJS\{c↑} Q and P SJS Q → P SJS\{c↓} Q ′ {c↓} Q Proof sketch.
The first transformation is obtained using local transformations shown in Figure 5, and the second one is obtained dually. To prove termination, we need an induction measure making heavy use of the flow-graphs defined above. The measure is more complex than one might expect, because of non-trivial interferences in the reductions of Figure 5. For example, case (7) duplicates a c↑, but the second c↑ can be duplicated via case (3) by an instance of c↓ that is introduced by case (5) moving up the first c↑ of (7), and so on. The precise definition of the induction measure is beyond the space limitations of this paper, but it is very close to the one given in [START_REF] Straßburger | MELL in the Calculus of Structures[END_REF] (and simplified in [START_REF] Straßburger | A system of interaction and structure IV: The exponentials and decomposition[END_REF]) for a system for multiplicative exponential linear logic. Here, the situation is slightly simpler because we are in an intuitionistic setting.

Definition 29. An n-flip path inside G (D) is a path with at most n pure left edges. The flipping number of a path is the number of pure left edges in it, and the flipping number of a particle p is the maximum of the flipping numbers of all paths starting in p.

Lemma 30. Every derivation D from P to Q in SJS can be transformed as shown below:

P SJS Q → P {c↑} P ′ SJS\{c↓,c↑} Q ′ {c↓} Q Proof.
We repeatedly use the transformations of the previous lemma, permuting all instances of c↓ down, and all instances of c↑ up. Let us define the flipping number of a c↓ instance to be the flipping number of the head of A in its conclusion, and similary, the flipping number of a c↑ to be the flipping number of the head of the A in its premise. Then, the flipping value of a derivation D, denoted fl (D), is the multiset of all the flipping numbers of all c↓ and c↑ in D. By inspecting the cases in Figure 5 used in the proof of Lemma 28, one can see that the flipping value of D decreases after each run, because the flipping number of the new c↓ in case (5) in Figure 5 is smaller than the flipping number of the c↑ before. This is enough to ensure termination of the whole process, provided that there is no cycle in the flow-graph of D, because no transformation in Figure 5 increases the flipping number of a path. The acyclicity of G (D) is ensured by Lemmas 31 and 32 below. ----------------------------- π{C ⊃ (D ⊃ E) ⊃ F } w↑ ---------------------------- π{C ---------------------------- ---------------------------- ---------------------------- ---------------------------- ------------------- Proof. Note that D consists of two parts: an upper part consisting only of c↑, and a lower part that does not contain any c↑. In that lower part of D, all c↓ are in a position as in case (5) in Figure 5.

η{E ′ ⊃ D } r -------------- η{E ⊃ D } w↑ ------------- η{D } -→ η{E ′ ⊃ D } w↑ -------------- η{D } η ′ {E ⊃ D } r -------------- η{E ⊃ D } w↑ ------------- η{D } -→ η ′ {E ⊃ D } w↑ -------------- η ′ {D } r -------- η{D } π{D } w↓ -------------- π{C ′ ⊃ D } w↑ -------------- π{C ⊃ D } -→ π{D } w↓ ------------- π{C ⊃ D } π{((C ⊃ D) ⊃ E) ⊃ F } s↓ -
⊃ E ⊃ F } -→ π{((C ⊃ D) ⊃ E) ⊃ F } w↑ ------------------------------ π{E ⊃ F } w↓ ------------------- π{C ⊃ E ⊃ F } η{A ⊃ (B ⊃ C) ⊃ D } s↑ -
- η{((A ⊃ B) ⊃ C) ⊃ D } w↑ -
- η{(B ⊃ C) ⊃ D } -→ η{A ⊃ (B ⊃ C) ⊃ D } w↑ --------------------------- η{(B ⊃ C) ⊃ D } η{A ⊃ (B ⊃ C) ⊃ D } s↑ -
- η{((A ⊃ B) ⊃ C) ⊃ D } w↑ -
- η{D } -→ η{A ⊃ (B ⊃ C) ⊃ D } w↑ -------------------------- η{(B ⊃ C) ⊃ D } w↑ -
If G (D) contains a cycle, then this cycle must be present in the lower part. So, without loss of generality, we can discard the upper part, and assume D to be c↑-free. We now transform D into D - by eliminating all instances of c↓, without destroying the cycle, but changing premise and conclusion of the derivation. We proceed by induction on the number of instances of c↓ in D, using a case analysis on the bottommost such instance:

1. The cycle does not pass through A in the conclusion of the c↓. Then it also does not pass through any of the two A in the premise. We can therefore eliminate this instance of c↓ as shown below, and go on by induction.

P D 1 π{A ⊃ A ⊃ B } c↓ ------------------- π{A ⊃ B } D 2 Q → P D 1 π{A ⊃ A ⊃ B } D {s↓} A ⊃ π{A ⊃ B } A⊃D 2 A ⊃ Q (11)
where D exists by Lemma 7. The resulting derivation D ′ has one instance of c↓ less, but the cyle is still present in G (D ′ ) since only edges connecting one of the A in the premise to the A in the conclusion of c↓ are removed, and all paths not using those edges are preserved. 2. The cycle goes through A in the conclusion and through only one A in the premise, as indicated below:

. . .

------------------------------------- π{ A ⊃ A ⊃ B } c↓ ------------------------------------- π{ A ⊃ B } ----------------------- . . . (12)
In this case we proceed as in the previous case, using (11) to construct D ′ because the cycle does not use the edges that connect the right A in the premise to the A in the conclusion of the c↓. As before, D ′ still contains a cycle and has one c↓ instance less. 3. The cycle contains a path between the two copies of A in the premise of c↓ without going through its conclusion:

. . . -----------------------------------

------------------------------------- π{ A ⊃ A ⊃ B } c↓ -
- π{ A ⊃ B } ----------------------- . . . (13)
This means there is an instance of s↓ above the c↓ whose pure left edge connects a particle in the left A to one in the right A. But the c↓ is in a position as shown on the right in case (5) of Figure 5, there is no such s↓ in the derivation in that figure, and permuting the c↑ up cannot introduce such a s↓. Thus, this case is impossible. 4. The last possibility is that the cycle passes through both A in the premise of the c↓ without a direct path between the two A, as follows:

. . .

----------------------------------------------- π{ A ⊃ A ⊃ B } c↓ ----------------------------------------------- π{ A ⊃ B } --------------------------- . . . (14)
By construction, D contains no instances of c↑, and all c↓ in D are as on the right of case (5) in Figure 5. But the c↑ that created the c↓ and will be moved up acts the same on both A in the premise of c↓. Thus, all paths existing on one side also exist on the other, as follows:

. . . --------------------------------------------- ---------------------------------------------- η{((( ---------------------------------------------

----------------------------------------------- π{ A ⊃ A ⊃ B } c↓ -
- π{ A ⊃ B } --------------------------- . . . ( 15
) π{((A ⊃ B) ⊃ (C ⊃ D) ⊃ E) ⊃ F } s↓ --------------------------------------------- π{A ⊃ (B ⊃ (C ⊃ D) ⊃ E) ⊃ F } s↑ --------------------------------------------- π{A ⊃ (((B ⊃ C) ⊃ D) ⊃ E) ⊃ F } -→ π{((A ⊃ B) ⊃ (C ⊃ D) ⊃ E) ⊃ F } s↑ ----------------------------------------------- π{((((A ⊃ B) ⊃ C) ⊃ D) ⊃ E) ⊃ F } s↓ ----------------------------------------------- π{((A ⊃ (B ⊃ C) ⊃ D) ⊃ E) ⊃ F } s↓ --------------------------------------------- π{A ⊃ (((B ⊃ C) ⊃ D) ⊃ E) ⊃ F } η{A ⊃ (((B ⊃ C) ⊃ D) ⊃ E) ⊃ F } s↓ -------------------------------------------- η{A ⊃ (B ⊃ (C ⊃ D) ⊃ E) ⊃ F } s↑ -------------------------------------------- η{((A ⊃ B) ⊃ (C ⊃ D) ⊃ E) ⊃ F } -→ η{A ⊃ (((B ⊃ C) ⊃ D) ⊃ E) ⊃ F } s↑ -------------------------------------------- η{((A ⊃ (B ⊃ C) ⊃ D) ⊃ E) ⊃ F } s↑ -
(A ⊃ B) ⊃ C) ⊃ D) ⊃ E) ⊃ F } s↓ -
- η{((A ⊃ B) ⊃ (C ⊃ D) ⊃ E) ⊃ F } Figure 7. Permutation cases for s↑
Hence, the derivation contains another cycle that passes only through one A in the premise of the c↓, as below:

. . . ---------------------------------------------

----------------------------------------------- π{ A ⊃ A ⊃ B } c↓ -
- π{ A ⊃ B } --------------------------- . . . (16)
This is the same situation as in case 2 above, so that we can proceed as before.

We have obtained a derivation D -containing no instances of c↓ and c↑, but G (D -) has a cycle. In D -we now permute all instances of w↓ upwards in the derivation and all instances of w↑ downwards, and call D • the part in between.

P SJS\{c↓,c↑} D - Q → P {w↓} P • {i↓,i↑,s↓,s↑} D • Q • {w↑} Q (17)
Transformation ( 17) is obtained by simple rule permutations. Most cases are trivial, except when w↓ meets i↓ as follows: ---------------------------- ----------------------------------

η{∆ ⊃ E } i↓ -
- η{((∆ ⊃ C) ⊃ C) ⊃ E } w↓ -
- η{((∆ ⊃ C) ⊃ A ⊃ C) ⊃ E } (18)
which can be replaced by the following, where ∆ = D1, ∆ ′ :

η{D1 ⊃ ∆ ′ ⊃ E } w↓ ------------------------------ η{(A ⊃ D1) ⊃ ∆ ′ ⊃ E } i↓ ----------------------------------------------- η{(((A ⊃ D1) ⊃ ∆ ′ ⊃ C) ⊃ C) ⊃ E } s↓ ----------------------------------------------- η{(A ⊃ (D1 ⊃ ∆ ′ ⊃ C) ⊃ C) ⊃ E } ≡ -------------------------------------------- η{((∆ ⊃ C) ⊃ A ⊃ C) ⊃ E } (19)
and dually for w↑. Since the cycle cannot go through particles occurring in the structure A introduced by an instance of w↑ or w↓, and the transformation in (17) preserves all paths, our cycle must still be present in D • .

Lemma 32. The flow-graph of a derivation in the subsystem {i↓, i↑, s↓, s↑} does not contain any cycle.

Proof. This set of rules is the ⊸-only fragment of intuitionistic multiplicative linear logic. Therefore, the statement we make here follows immediately from the acyclicity condition of proof nets for intuitionistic multiplicative linear logic. For a direct proof of this, see [START_REF] Straßburger | Linear Logic and Noncommutativity in the Calculus of Structures[END_REF][START_REF] Straßburger | MELL in the Calculus of Structures[END_REF][START_REF] Straßburger | A system of interaction and structure IV: The exponentials and decomposition[END_REF].

We still need to prove that other parts of the decomposition can be obtained by permuting the other rule instances in any derivation without any c↑ and c↓ instances. We start with weakenings, that can be easily moved, and then decompose the fragment containing only switches and the interactions rules of identity and cut.

Lemma 33. Every derivation D from P ′ to Q ′ in SJS \ {c↓, c↓} can be transformed as shown below:

P ′ SJS\{c↓,c↑} Q ′ → P ′ {w↑} P ′′ {i↓,i↑,s↓,s↑} Q ′′ {w↓} Q ′ Proof.
We can permute all w↑ up as shown in Figure 6, and all w↓ down by the dual permutations, and repeat this until all instances of w↑ and w↓ are separated. It terminates because no permutation step increases the length of the derivation, each permutation step moves an instance of weakening closer to its destination, and whenever a new weakening is introduced, one instance of switch disappears.

Lemma 34. Every derivation in the subsystem {i↓, i↑, s↓, s↑} can be transformed as shown below:

P ′′ {i↓,i↑,s↓,s↑} Q ′′ → P ′′ {ai↑,s↑} I {ai↓,s↓} Q ′′ (20)
Proof sketch. First, we use Propositions 6 and 22 to reduce instances of i↑ and i↓ to their atomic versions ai↑ and ai↓, respectively. Then, the transformation (20) is obtained by permuting all instances of ai↑ and s↑ up, using an induction on the number of up instances below a down instance in the derivation. If the topmost such instance is an ai↑, we proceed as for Lemma 20, having to consider only the cases (1)-(5) in Figure 3. If it is a s↑, we have three non-trivial cases: the dual of (5) in Figure 3, where the s↑ disappears, and the two cases in Figure 7. Due to space restrictions, we cannot show the details of the induction measure here, but the basic idea is to group s↑ instances into a compound coswitch rule. This is a standard technique for the calculus of structures (see, e.g., [START_REF] Straßburger | Linear Logic and Noncommutativity in the Calculus of Structures[END_REF]).

Q ′′ → I {i↓} Q ′′′ {s↓} Q ′′
Proof. The permutations of the s↑ instances over i↑ instances are always trivial, so that we can use a straightforward induction, and proceed dually for s↓ and i↓.

All of these lemmas together allow us to complete the proof of Theorem 25, but successively applying each transformation to a given SJS derivation.

Proof of Theorem 25. The decomposition of the given derivation is obtained by applying Lemmas 30, 33, 34, and 35. The second statement then follows immediately from the first since P ≡ t implies P ≡ P ′ ≡ P ′′ ≡ P ′′′ ≡ I ≡ t.

Conclusion and Future Work

We presented the system called JS in the calculus of structures, implementing in a quite direct way the usual rules of LJ while obtaining as a benefit the incremental nature of inference rules in deep inference. Although the cut elimination result for JS is not very surprising, the internal procedure in the calculus of structure is interesting, because intuitionistic logic (which is the original source of computational interpretations of proof systems) is the least understood of all standard logics in the deep inference setting.

The extension of JS into the symmetric SJS system is a natural generalisation in setting of the calculus of structures, where the notion of normal form of proofs takes its full strength in terms of symmetry, and where the decomposition theorem obtained is a strong statement on the relation between inference rules. Such a symmetric system also has a certain potential in terms of computation: all of the up rules in SJS may be interpreted as typing rules for some terms based on λ-terms or combinators. As a consequence, the language of programs, under a Curry-Howard interpretation, would be much richer than what is obtained from proofs in natural deduction or from sequent calculi. For example, this would introduce in the calculus an operator representing the co-contraction rule, which is known to relate to a form of sharing, and this operator would interact with other ones in an intricate way -for example, with the representation of the switch, which can be used to implement a form of internal communication [START_REF] Guenot | Nested Deduction in Logical Foundations for Computation[END_REF]. Moreover, refining SJS with its normalisation procedure into a system with atomic contraction would provide a setting where a local treatment of cuts (usually associated to some form of explicit substitution in computational interpretations) could be successfully mixed with an incremental treatment of duplications, as found in the atomic λ-calculus [START_REF] Gundersen | Atomic lambdacalculus, a typed lambda-calculus with explicit sharing[END_REF].

The results established here are also an important step towards the development of the proof theory of intermediate logics in the calculus of structures. The expressivity of formalisms based on the deep inference methodology allows to apply powerful techniques from substructural proof theory. We expect that the techniques developed in the intuitionistic setting will be versatile enough to apply to many other logics without De Morgan duality.

Definition 36. Given an instance of c↑, we define its head as the head of A in its premise, and the head of a c↓ instance is the head of A in its conclusion. A particle p is n-flip entangled with an instance of c↑ (resp. c↓) if there is an n-flip path from the head of that c↑ (resp. c↓) to p. The n-flip c-number of a particle p, denoted by # n c(p), is the number of c↑and c↓-instances p is n-flip entangled with, increased by 1.

Definition 37. Let D be a derivation. A particle p in D is in the scope of a particle q, iff p and q occur in the same line in D, and that line contains a subformula occurrence A, such that p is inside A, and q is the head of A. The onion of a positive (resp. negative) particle p, denoted by (p), is the set of negative (resp. positive) particles q, such that p is in the scope of q. Now, the contraction potential of a particle p, denoted by c (p), is defined as the product of the 1-flip c-numbers of its onion, i.e., c

= q∈ (p) # 1 c(q) (p)
Remark 38. The contraction potential plays essentially the same role as the multiplicity in the previous section. However, dure to the flip and the scope change in case (5) in Figure 5, the multiplicity is not enough for our measure.

Definition 39. For a given instance of a s↑ (resp. s↓), we define its front head to be the head of C and its rear head to be the head of A in the conclusion of that s↑ (resp. premise of that s↓). Then, an instance of a s↑ or s↓ is on a path in the flow-graph, if its front head is on that path. The explosiveness of of an s↑or s↓-instance is the 0-flip c-number of its rear head. The s-number of a path is the sum of the explosivenesses of the s↑and s↓-instances on that path, increased by 1. The n-flip s-number of a particle p, denoted by # n s(p), is the maximum of the s-numbers of the paths starting in p. Now, the switch-contraction potential of a particle p, denoted by cs (p), is defined as the product of its 0-flip s-number and its contraction potential, i.e,

cs (p) = # 0 s(p) • q∈ (p) # 1 c(q)
Finally, for a given c↑ instance in a derivation D, we define its status to be 0 if all rule instances above that c↑ in D are also c↑, and 1 otherwise. I.e., a c↑ instance with status 0 is "already at the top of the derivation".

Proof of Lemma 28. We define the rank of a c↑ instance to be the pair s, p (under lexicographic ordering), where s is its status and p the switch-contraction potential of its head. Then the c↑rank of a derivation D, denoted by rk c↑ (D), is the multiset of the ranks of its c↑ instances. we now use as induction measure the pair (rk c↑ (D), h), under lexicographic ordering, where for rk c↑ (D) we use the multiset ordering and where h is the number of of non-c↑ instance above the topmost c↑ that did not yet reach the top. In Figure 8 we repeat the reductions of Figure 8, with added flowgraph edges for the heads of the concerned substructures. A crucial observation is that whenever we have two particles p and q in premise and/or conclusion of a rewriting fragment, there is an nflip path from p to q on the left, iff there is such a path on the right. It can happen-in cases (5) and ( 6)-that such a path is duplicated on the right. But this does not affect the rank of c↑-instances below. Now, there are three kinds of cases: First, case (4): the c↑ disappears, and our measure clearly goes down.

Second, cases (1), (2), (5), and (6): the c↑ moves up and no other c↑ is added to the derivation. Then the distance of this c↑ to the top has been reduced, and none of the other c↑ below in the derivation has changed its rank. This is obvious for cases (1) and (2). For case (6), notice that the sum of the explosivenesses of the two new s↑ is smaller than the explosiveness of the old s↑. In case (5), note that the contraction potential of a particle in C in the conclusion does not change in the transformation. The new instances of s↓ do not play a role in the 0-flip s-number of a c↑.

Third, cases (3) and (7): a second c↑ is introduced. In case (3), the two new c↑ have smaller contraction potential, and therefore also smaller rank than the original one. In case (7), the heads of the two new c↑ have a smaller 0-flip s-number, and the two new s↑ have both a smaller explosiveness than the one on the left.

Complements on proof of Lemma 34. Handling permutations of switches requires to define a compound switch rule ss↑ as follows:

η{A ⊃ ν{t}} ss↑ ---------------- η{ν{A}} equivalent to a sequence of s↑ instances (dual to Lemma 7). We then proceed by induction on the height of the derivation above the considered r↑ instance of this rule, using a case analysis on r1↓, the rule instance directly above it:

1. If r1↓ is not affecting A or the hole of ν, then the permutation is immediate and we can go on by applying the induction hypothesis. 2. If r1↓ is an instance of ai↓ interacting with one of the s↑ in r↑, it assimilates one of these s↑ as shown below, where ν = η{(ρ{-} ⊃ d) ⊃ d} for a negative context η and positive context ρ: π{(A ⊃ η{ρ{t}}) ⊃ C } ai↓ ------------------------------------------- π{(A ⊃ η{(ρ{t} ⊃ d) ⊃ d}) ⊃ C } ss↑ ------------------------------------------- π{η{(ρ{A} ⊃ d) ⊃ d} ⊃ C } -→ π{(A ⊃ η{ρ{t}}) ⊃ C } ss↑ ------------------------------ π{η{ρ{A}} ⊃ C } ai↑ ------------------------------------ π{η{(ρ{A} ⊃ d) ⊃ d} ⊃ C } and we conclude by induction hypothesis -except if r↑ was a simple s↑ instance, in which case it disappeared. 3. If r1↓ is an instance of s↓ moving some B inside A, it is permuted by introducing a sequence of s↓, and then we proceed by induction hypothesis:

π{((B ⊃ A) ⊃ ν{t}) ⊃ C } s↓ --------------------------------- π{B ⊃ (A ⊃ ν{t}) ⊃ C } ss↑ ------------------------------- π{B ⊃ ν{A} ⊃ C } -→ π{((B ⊃ A) ⊃ ν{t}) ⊃ C } ss↑ --------------------------------- π{ν{B ⊃ A} ⊃ C } s↓ * = = = = = = = = = = = = = = = = = = = = = = = = = π{B ⊃ ν{A} ⊃ C } This sequence of s↓ exists by Lemmma 7. 4. If r1↓ is an instance of s↓ moving the hole of one of the s↑ composing r↑, then one more s↑ is needed inside r↑ after permutation (cf. Figure 7), so that the permutation is as follows, where ν = η{η ′ {-} ⊃ (D ⊃ E) ⊃ F } for negative contexts η{E ′ ⊃ D } r -------------- η{E ⊃ D } c↑ ------------------- η{E ⊃ E ⊃ D }

(1)

-→ η{E ′ ⊃ D } c↑ --------------------- η{E ′ ⊃ E ′ ⊃ D } r --------------------- η{E ′ ⊃ E ⊃ D } r -------------------- η{E ⊃ E ⊃ D } η ′ {E ⊃ D } r -------------- η{E ⊃ D } c↑ ------------------- η{E ⊃ E ⊃ D }

(2)

-→ η ′ {E ⊃ D } c↑ -------------------- η ′ {E ⊃ E ⊃ D } r -------------------- η{E ⊃ E ⊃ D } π{C ′ ⊃ C ′ ⊃ D } c↓ --------------------- π{C ′ ⊃ D } c↑ -------------- π{C ⊃ D }

(3) -→ π{C ′ ⊃ C ′ ⊃ D } c↑ --------------------- π{C ⊃ C ′ ⊃ D } c↑ -------------------- π{C ⊃ C ⊃ D } c↓ ------------------- π{C ⊃ D } π{D } w↓ -------------- π{C ′ ⊃ D } c↑ -------------- π{C ⊃ D }

-→ π{D } w↓ ------------- π{C ⊃ D } π{((A ⊃ D) ⊃ E) ⊃ F } s↓ ------------------------------ π{A ⊃ (D ⊃ E) ⊃ F } c↑ ---------------------------------- π{A ⊃ (D ⊃ D ⊃ E) ⊃ F }

(5)

-→ π{((A ⊃ D) ⊃ E) ⊃ F } c↑ --------------------------------------------- π{((A ⊃ D) ⊃ (A ⊃ D) ⊃ E) ⊃ F } s↓ --------------------------------------------- π{A ⊃ (D ⊃ (A ⊃ D) ⊃ E) ⊃ F } s↓ ------------------------------------------ π{A ⊃ A ⊃ (D ⊃ D ⊃ E) ⊃ F } c↓ ---------------------------------------- π{A ⊃ (D ⊃ D ⊃ E) ⊃ F } η{A ⊃ (B ⊃ C) ⊃ D } s↑ ------------------------------ η{((A ⊃ B) ⊃ C) ⊃ D } c↑ ------------------------------------ η{((

A ⊃ A ⊃ B) ⊃ C) ⊃ D } (6)
-→ η{A ⊃ (B ⊃ C) ⊃ D } c↑ ---------------------------------- η{A ⊃ A ⊃ (B ⊃ C) ⊃ D } s↑ ------------------------------------ η{A ⊃ ((A ⊃ B) ⊃ C) ⊃ D } s↑ ------------------------------------ η{((A ⊃ A ⊃ B) ⊃ C) ⊃ D } η{A ⊃ (B ⊃ C) ⊃ D } s↑ ------------------------------ η{((A ⊃ B) ⊃ C) ⊃ D } c↑ ----------------------------------------------------- η{((

A ⊃ B) ⊃ C) ⊃ ((A ⊃ B) ⊃ C) ⊃ D } (7)
-→ η{A ⊃ (B ⊃ C) ⊃ D } c↑ ------------------------------------------ η{A ⊃ (B ⊃ C) ⊃ (B ⊃ C) ⊃ D } c↑ ------------------------------------------------ η{A ⊃ A ⊃ (B ⊃ C) ⊃ (B ⊃ C) ⊃ D } ≡ ------------------------------------------------ η{A ⊃ (B ⊃ C) ⊃ A ⊃ (B ⊃ C) ⊃ D } s↑ -------------------------------------------------- η{A ⊃ (B ⊃ C) ⊃ ((A ⊃ B) ⊃ C) ⊃ D } s↑ ----------------------------------------------------- π{(A ⊃ η{((η ′ {t} ⊃ D) ⊃ E) ⊃ F }) ⊃ C } s↓ ------------------------------------------------------ π{A ⊃ η{η ′ {t} ⊃ (D ⊃ E) ⊃ F } ⊃ C } ss↑ ------------------------------------------------- π{η{η ′ {A} ⊃ (D ⊃ E) ⊃ F } ⊃ C } -→ π{(A ⊃ η{((η ′ {t} ⊃ D) ⊃ E) ⊃ F }) ⊃ C } ss↑ ------------------------------------------------------ π{η{((η ′ {A} ⊃ D) ⊃ E) ⊃ F } ⊃ C } s↓ ----------------------------------------------- π{η{η ′ {A} ⊃ (D ⊃ E) ⊃ F } ⊃ C } and we conclude by induction hypothesis.

Figure 5 .

 5 Figure 5. Permutation cases for c↑

Lemma 35 .

 35 Any derivation in {i↓, s↓} (respectively {i↑, s↑}) can be transformed as below on the left (respectively right).

Figure 8 .

 8 Figure 8. Permutation cases for c↑ with some flow-graph edges

  For any derivation D in SJS obtained by moving all c↓ down and all c↑ up, using Lemma 28 twice, if G (D) contains a cycle, then there is a derivation D • in the subsystem {i↓, i↑, s↓, s↑} whose flow-graph also contains a cycle.

	η{D }	-
	Figure 6. Permutation cases for w↑
	Lemma 31.

Acknowledgements. This work was partially funded by the Demtech grant 10-092309 from the Danish Council for Strategic Research.

Appendix

This appendix is not part of the published paper. It contains straightforward but tedious details of the two sketched proofs (Lemma 28 and Lemma 34) in the main text. For the proof of Lemma 28, we need to define the induction measure first.


Youssef Benama

Thècle Alix

Nicolas Perry

Supporting make or buy decision for reconfigurable manufacturing system, in multi-site context

Keywords: Mobility, RMS, make or buy, multi-site context, MCDM

The make or buy decision is a strategic issue. When looking for finding out which components or products should be manufactured in house or externalized, questions about the required human and technical resources as well as costs of the externalization are to be answered. In the case of mobile manufacturing systems that are movable between various locations, long term strategic considerations must be considered when addressing the make or buy decision problem. This paper aims to provide a structured make or buy decision model, adapted for reconfigurable manufacturing systems with strong mobility constraints. Industrial application case is provided to illustrate the presented method.

Introduction

The make or buy decision problem also known as "sourcing", "outsourcing" or subcontracting" problem, is among the most pervasive issues confronting modern organizations [START_REF] Padillo | A multiple-criteria decision methodology for the makeor-buy problem[END_REF]. Making the right decision with regard to outsourcing can provide a major boost to a company's financial performance, although there is evidence that many companies do not achieve the advantages of outsourcing [START_REF] Van De Water | A decision support model based on the Analytic Hierarchy Process for the Make or Buy decision in manufacturing[END_REF]. McIvor [START_REF] Mcivor | A strategic model for the formulation of an effective make or buy decision[END_REF] demonstrates that decisions on outsourcing are rarely taken on the basis of particular strategic perspectives. Most of time the only intention is gaining short-term cost advantages [START_REF] Van De Water | A decision support model based on the Analytic Hierarchy Process for the Make or Buy decision in manufacturing[END_REF].

The "make or buy" decision is a strategic decision and has implications for the overall corporate strategy of the organization by analyzing a number of strategic factors in case of short term cost reduction purpose, long-term strategic considerations, which have greater importance, should be considered [START_REF] Öncü | Make or Buy' Analysis for Local Manufacture or Import Decisions in Defense System Procurements Using AHP: The Case of Turkey[END_REF]. Padillo [START_REF] Padillo | A multiple-criteria decision methodology for the makeor-buy problem[END_REF] identified six disciplines covered by the make or buy problem: (1)industrial organization; (2)corporate/business strategy; (3) purchasing or supply management (4) strategic operations management;

(5) operations research; and (6) cost accounting or managerial economics. Make or buy decision was argued most frequently by the economists. They have con-sidered the "make or buy" problem especially with the perspective of costs. But the "make or buy" decision considerations should not only focus on costs [START_REF] Öncü | Make or Buy' Analysis for Local Manufacture or Import Decisions in Defense System Procurements Using AHP: The Case of Turkey[END_REF]. Many authors, have noted the need to include multiple factors when performing a make or buy analysis [START_REF] Padillo | A multiple-criteria decision methodology for the makeor-buy problem[END_REF]. They take into account strategic competitive performance, managerial performance, sourcing performance and financial performance. McIvor [START_REF] Mcivor | A case-based reasoning approach to the make or buy decision[END_REF] proposed a model based on technical capability, comparison of internal and external capabilities, organization profiles and total acquisition costs.

On the other hand, manufacturing systems operating in a context characterized by: demand fluctuation, local production and site dependency, should cope with specifications such as mobility, scalability and functional adaptability. Those specifications allow fast and cost effectively adaptation to environment changes. In the literature, manufacturing systems meeting these specifications are referenced as Reconfigurable Manufacturing Systems (RMS) [START_REF] Elmaraghy | Flexible and reconfigurable manufacturing systems paradigms[END_REF]- [START_REF] Stillström | The concept of mobile manufacturing[END_REF]. In the area of RMS, we notice a lack of models that takes into account the production system mobility, when addressing the "make or buy" problem. Furthermore, in multi-site context, a long term vision should be incorporated into the decision model In the following sections we detail our proposed make or buy model adapted to RMS systems. Then, we provide an industrial application case to illustrate the model. Finally we will conclude and present further works.

The proposed make or buy model for RMS systems

The proposed decision model framework is adapted from the model proposed by van de Water and van Peet [START_REF] Van De Water | A decision support model based on the Analytic Hierarchy Process for the Make or Buy decision in manufacturing[END_REF]. This framework highlights 3 decision model stages:

 Strategic analysis: the make or buy decision is based on the satisfaction of multiple objectives (e.g. cost, risk...). This stage deals with the importance of each objective. The given importance highlights the priorities of the decision maker. Decision situation has an impact on these priorities, for example, considering the purchasing situation classification presented by Faris [START_REF] Faris | Industrial buying and creative marketing[END_REF].  Alternative evaluation: this stage proposes a model to evaluate in house manufacturing or external sourcing alternatives. The evaluation model is based on indicators definition. Each of the four indicators proposed is depending on other parameters which we call attributes. This stage will be detailed in the next section.  Providers selection: this stage is about contractual aspects in the provider selection process and collaboration nature definition. It's based on previous stage results. While our aim is to identify if manufacturing of a specified product will be achieved in house or via external sourcing. This stage is out of this paper scope.

Alternative evaluation model:

Assessment of techno-economic objective.

Cost evaluation.

We identify three attributes linked to cost objective: (1) supply cost: it takes into account material purchasing costs and shipping costs set from transportation costs and customs clearance fees. ( 2) on site storage cost: It depends on component value, storage period and cost of all tools used in storage activity. (3) on site transformation cost: concerns all costs linked to transformation operations and value added activities realized on site. For in house manufacturing case, it takes into account, machinery investment, cost relative to usual functioning like process configuration cost, maintenance cost and energy cost. In addition, for a mobile manufacturing system, machinery are shipped on site, so it's necessary to consider the shipping cost of machines. On the other hand, External sourcing case concerns in most cases quality inspection operations when receiving materials, and reworking operations.

To assess the satisfaction of the cost objective, we use the satisfaction function proposed by Harrington [START_REF] Collignan | Méthode d'optimisation et d'aide à la décision en conception mécanique: Application à une structure aéronautique[END_REF] which appears to give satisfactory results in our case.

Technical capability objective.

Internal technical capability.

Internal technical feasibility describes the ability of in-house manufacturing alternative to ensure the know-how and process required to satisfy the product feasibility on site. It depends on: System mobility: machinery and resources must be movable from one site to another. Qualification availability: operators are needed to be hired locally.

Energy availability and accessibility: in the context of desertic location, energy accessibility may be difficult, that can limit the use of certain resources (welding...). On the other hand, internal technical capacity is related to the ability to supply the necessary quantity of raw materials. Two factors are involved: (1) the availability of qualified suppliers, (2) their proximity from the geographical production location.

Supplier technical capability

McIvor and Humphreys [START_REF] Mcivor | A case-based reasoning approach to the make or buy decision[END_REF] Evaluation of each technical capability factor is realized by giving notation between 0 and 1. Non-compensatory aggregation strategy is needed because the failure of one technical capability factor could not be compensated by the well performance of another factor. GOWA Aggregation operator could be used to make aggregation.

Socio-economic objective.

In the case of public projects where clients are governments or official institutes, socio-economic issues must be considered. We propose to incorporate in our model a socio-economic objective, which is concerned with the direct employment creation. This objective will be directly linked to geographical production localization of the supplier: if the supplier is localized in the same country than client site, the satisfaction value is 1, otherwise, the satisfaction value is 0.1. For a considered make or buy alternative, the assessment of the corresponding technoeconomic objective is based on the aggregation of cost, technical capability and socioeconomic objectives. For aggregation, we use GOWA operator [START_REF] Yager | Generalized OWA Aggregation Operators[END_REF]:

0 * * 1

Risk Objective

Identification of risk factors.

Padillo [START_REF] Padillo | A multiple-criteria decision methodology for the makeor-buy problem[END_REF] identified 4 sourcing risk attributes: appropriation risk, technology diffusion risk, end-product degradation risk, and supply disruption risk. Appropriation and technology diffusion risks are relevant mostly for outsourcing alternatives. While Supply disruption is applicable to both in-house and outsourcing alternatives [START_REF] Padillo | A multiple-criteria decision methodology for the makeor-buy problem[END_REF]. On the other side, end-product degradation risk is in relation with the outsourcing of an activity that is located between the firm and its customers. This type of risk is not present in our problem, but the risk about transportation activity remains dominant. Wagner [START_REF] Wagner | An empirical examination of supply chain performance along several dimensions of risk[END_REF] divided risk sources into five distinct classes: (1) demand side (2) supply side; (3) regulatory, legal and bureaucratic; (4) infrastructure; and (5) catastrophic.

Srinivasan [START_REF] Srinivasan | Buyer-supplier partnership quality and supply chain performance: Moderating role of risks, and environmental uncertainty[END_REF] focus on two types of factors that can impact the performance of supply chain, the first factors are internal to supply chain, which are demand and supply risks, like demand variability, lead-time variability supply delays, order cancellations, etc.). On the other hand, environment uncertainty which includes factors that are external to the supply chain. Those factors are strategic in nature, like, changes in product or process technology, competitor behavior, changes in consumer preferences, etc.

Production system mobility implies that the characteristics of the site where the production system will be implanted will vary. In consequent, the risk factors related to implantation site should be integrated in the analysis. We use a macro-environment analysis, like the PESTLE approach to characterize risks related to the implantation site. In the other hand, either make or buy situations require realization of additional operations by the buying firm. Internal operations need human and machinery interventions and should be realized locally on site. In consequent, internal risks corresponding to human and machinery failures should be considered in both situations. The assessment of each risk factor is firstly conducted using the FMECA (Failure Modes, Effects and Criticality Analysis). Each risk factor will be identified and quantified in term of likelihood of occurrence and in term of severity. Thereby, the overall risk criticality of will be defined by summing the corresponding criticality of risk factors. The next question is how to judge if the level of the risk criticality is acceptable or not. We define a satisfaction function that will express the preferences of the decision maker. We use Derringer function (Derringer, 1980); the decision maker expresses an interval of criticality levels among which the criticality level of the considered alternative will be acceptable.

Performance evaluation.

Local Performance evaluation.

Local performance evaluation aims to find out the best alternative for each considered site localization. Each objective is evaluated as it was mentioned previously. The decision-maker should express it's preference between the importance of each objective. Aggregation of the local performance is made using the GOWA operator [START_REF] Yager | Generalized OWA Aggregation Operators[END_REF]. This operator allow the DM to adapt the aggregation strategy, i.e. if compensation will be considered or not, to each situation decision, by setting the trade-off strategy parameter. For each site i, Local performance evaluation of alternative j is assessed : * * 2

TEO : Technical and Economical Objective value. RO : Risk Objective value

Global Performance evaluation.

Global Performance evaluation aims to determine the best alternative in regard to overall sites. First condition that should be verified is the importance of each site. For

Factors of risk

Loss of confidentiality of a particular value-creating asset by entering into a sourcing relationship with an outside Fig. 2. Identification of risk factors strategic reasons, like the willingness to enter a new market, or for reasons of market size. Global Performance Evaluation (GPE) of the alternative j is given by : * 3 n: number of sites where the production system will operate. is the importance of the site i.

is the local performance evaluation of the alternative j, for the site i. s is the trade-off strategy parameter. All alternatives will be ranked following the GPE value, and then the best alternative will have the high GPE.

Industrial application

The Industrial application concerns an enterprise E, operating in solar energy sector. For confidentiality reasons, real values have been changed, but hypotheses and assumptions remain valid. The component analyzed is a steel part obtained by bending process. This part is critical because it contributes to mechanical resistance of the endproduct. The production should be operated by the same reconfigurable manufacturing system sequentially on 5 different sites. The expected volume demands are: S1 : 20000, S2=18000, S3 = 16000, S4 = 5000, S5 = 11000. We consider 3 different alternatives: A1 : part will be manufactured by the internal production system. A2: part will be realized by an external low cost supplier in Eastern Europe. A3: corresponds to an external supplier localized in North Africa.

Stage 1: Strategic Analysis

Objective's weighting . Importance of each objective is set using a pairwise comparison. Therefore, the importance of each objective will be obtained by the eigenvector of the matrix : Cost Objective :0.635, Technical capability=0.287 and Socio-economical objective=0.078. In order to assess local performance for each site, technical and economical objective and risk objective will be considered with the same importance: ω 0.5 and ω 0.5

Stage 2: Evaluation of Alternatives

Evaluation of techno-economic objective (TEO):. Technical and economical objective is assessed from cost, technical capability (figure 4) and socio-economic objectives (figure 5). Compensation (s=100) has been made between these attributes. For alternative 1, poor satisfaction values of cost and technical objectives are compensated by the satisfaction of the socio-economic objective.

Evaluation of risk objective:. Alternative 1 allows better control of risk factors, because in this case technology diffusion risk doesn't exist, supply disruption and product degradation risks are re-duced because supplying raw materials has less value than supplying finite components. In the other hand, internal risks are more important in the case of internalization because more resources are needed, in consequent, human and machinery failures have more impact in this case.

Local performance Evaluation:

For each alternative, in order to assess the local performance, non compensatory aggregation (s=-100) is made between TEO and risk objective, and that for each site location. In the case study, figure 3 shows alternative 1 ranked 1.

Global performance Evaluation:. The global make or buy decision must be made by accounting for all local performance evaluations. Compensation (s=100) is made between different sites. This implies that business 'strategic plan included that sites with negative financial results can be compensated by other sites with positive results. Figure 8 shows that alternative 1 presents in this case the best solution regarding the 5 sites. We note that all the 5 site locations are assumed to have the same importance : ω = 0.2.

Fig. 1 .

 1 Fig. 1. Structure of the alternative's evaluation model

Fig. 3 . 4 .Fig. 5 . 6 .Fig. 7 .Fig. 8 . 9 .

 3456789 Fig. 3. Satisfaction of cost objective Fig. 4. Satisfaction of technical capability

  identified 6 criteria to evaluate the technological capabilities of supplier, which include manufacturing capabilities, technical support, design capability, investment in R&D, speed of development and new product introduction (NPI) rate. In our analysis, technical support, investment on R&D and design capability are embedded in technical feasibility. On the other hand, manufacturing capability, speed of development and NPI rate determine the technical capacity of suppliers.

  Öncü stated that "A government concerned with economic growth cannot ignore the economic aspects of technology. Major purpose of national technology policy is the harnessing of technology to meet economic and social goals[...]. When one local-manufacture project is chosen rather than an import the choices have consequences for employment,[...]. Each local manufacture project will affect employment and wage payments."[START_REF] Öncü | Make or Buy' Analysis for Local Manufacture or Import Decisions in Defense System Procurements Using AHP: The Case of Turkey[END_REF]. The socio-economic benefits in terms of promoting local employment have an impact on final decision.

CONCLUSION AND OUTLOOK

The paper aims to propose a structured decision model adapted for reconfigurable systems in multi-site context. Although the financial objective has traditionally dominated the analysis of make or buy alternatives, this research demonstrates that is possible to consider strategic and technological issues in connection with the decision. The study allows to consider specific characteristics of the mobile manufacturing systems and provides a model that take into account a longer term vision. There are additional areas to investigate. We considered that all providers and production sites were well identified. However, it depends on the commercial strategy of the firm. Uncertainty about future clients and likely suppliers should be considered.