Rémi Di Guardia

Olivier Laurent

Type Isomorphisms for Multiplicative-Additive Linear Logic

Keywords: 2012 ACM Subject Classification Theory of computation → Linear logic Linear Logic, Type Isomorphisms, Multiplicative-Additive fragment, Proof nets, Sequent calculus, Star-autonomous categories with finite products

. We then use the sequent calculus to extend our results to full MALL (including all units).

Introduction

The question of type isomorphisms consists in trying to understand when two types in a type system (or two formulas in a logic) are "the same". The general question can be described in category theory: two objects A and B are isomorphic (A ≃ B) if there exist morphisms A f -→ B and B g -→ A such that f • g = id B and g • f = id A . f and g are the underlying isomorphisms. Given a (class of) category, the question is then to find equations characterizing when two objects A and B are isomorphic (in all instances of the class). The focus here is on pairs of isomorphic objects rather than on the isomorphisms themselves. For example, in the class of cartesian categories, one finds the following isomorphic objects:

A × B ≃ B × A, (A × B) × C ≃ A × (B × C) and A × ⊤ ≃ A.
Regarding type systems and logics, one can instantiate the categorical notion. For instance in typed λ-calculi: two types A and B are isomorphic if there exist two λ-terms M : A → B and N : B → A such that λx : B.(M (N x)) = βη λx : B.x and λx : A.(N (M x)) = βη λx : A.x where = βη is βη-equality. This corresponds to isomorphic objects in the syntactic category generated by terms up to = βη . Similarly, type isomorphisms can also be considered in logic, following what happens in the λ-calculus through the Curry-Howard correspondence: simply replace λ-terms with proofs, types with formulas, β-reduction with cut-elimination and η-expansion with axiom-expansion. In this way, type isomorphisms are studied in a wide range of theories, such as category theory [START_REF] Soloviev | The category of finite sets and cartesian closed categories[END_REF], λ-calculus [START_REF] Di | Isomorphisms of Types[END_REF] and proof theory [START_REF] Balat | A linear logical view of linear type isomorphisms[END_REF]. They may be used to develop practical tools, such as search in a library of a functional programming language [START_REF] Rittri | Using types as search keys in function libraries[END_REF].

Following the definition, it is usually easy to prove that the type-isomorphism relation is a congruence. It is then natural to look for an equational theory generating this congruence. Testing whether or not two types are isomorphic is then much easier. An equational theory T is called sound with respect to type isomorphisms if types equal up to T are isomorphic. It is called complete if it equates any pair of isomorphic types. Given a (class of) category, a type system or a logic, our goal is to find an associated sound and complete equational theory for type isomorphisms. This is not always possible as the induced theory may not be finitely axiomatisable (see for instance [START_REF] Fiore | Remarks on isomorphisms in typed lambda calculi with empty and sum types[END_REF]).

Soundness is usually the easy direction as it is sufficient to exhibit pairs of terms corresponding to each equation. The completeness part is often harder, and there are in the literature two main approaches to solve this problem. The first is a semantic method, relying on the fact that if two types are isomorphic then they are isomorphic in all (denotational) models. One thus looks for a model in which isomorphisms can be computed (more easily than in the syntactic model) and are all included in the equational theory under consideration (this is the approach used in [START_REF] Soloviev | The category of finite sets and cartesian closed categories[END_REF][START_REF] Laurent | Classical isomorphisms of types[END_REF] for example). Finding such a model simple enough for its isomorphisms to be computed, but still complex enough not to contain isomorphisms absent in the syntax is the difficulty. The second method is the syntactic one, which consists in studying isomorphisms directly in the syntax. The analysis of pairs of terms composing to the identity should provide information on their structure and then on their type so as to deduce the completeness of the equational theory (see for example [START_REF] Di | Isomorphisms of Types[END_REF][START_REF] Balat | A linear logical view of linear type isomorphisms[END_REF]). The easier the equality (= βη for example) between proof objects can be computed, the easier the analysis of isomorphisms will be.

We place ourselves in the framework of linear logic (LL) [START_REF] Girard | Linear logic[END_REF], the underlying question being "is there an equational theory corresponding to the isomorphisms between formulas in this logic?". LL is a very rich logic containing three classes of propositional connectives: multiplicative, additive and exponential ones. The multiplicative and additive families provide two copies of each classical propositional connective: two copies of conjunction (⊗ and &), of disjunction (`and ⊕), of true (1 and ⊤) and of false (⊥ and 0). The exponential family is constituted of two modalities ! and ? bridging the gap between multiplicatives and additives through four isomorphisms !(A & B) ≃ !A ⊗ !B, ?(A ⊕ B) ≃ ?A `?B, !⊤ ≃ 1 and ?0 ≃ ⊥. In the multiplicative fragment (MLL) of LL (using only ⊗, `, 1 and ⊥, and corresponding to ⋆-autonomous categories), the question of type isomorphisms was answered positively using a syntactic method based on proof-nets by Balat and Di Cosmo [START_REF] Balat | A linear logical view of linear type isomorphisms[END_REF]: isomorphisms emerge from associativity and commutativity of the multiplicative connectives ⊗ and `, as well as neutrality of the multiplicative units 1 and ⊥. The question was also solved for the polarized fragment of LL by one of the authors using game semantics [START_REF] Laurent | Classical isomorphisms of types[END_REF]. It is conjectured that isomorphisms in full LL correspond to those in its polarized fragment (Table 1 together with the four exponential equations above). As a step towards solving this conjecture, we prove the type isomorphisms in the multiplicative-additive fragment (MALL) of LL are generated by the equational theory of Table 1 (and this applies at the same time to the class of ⋆-autonomous categories with finite products). This situation is much richer than in the multiplicative fragment since isomorphisms include not only associativity, commutativity and neutrality, but also the distributivity of the multiplicative connective ⊗ (resp. `) over the additive ⊕ (resp. &) as well as the associated annihilation laws for the additive unit 0 (resp. ⊤) over the multiplicative connective ⊗ (resp. `). Using a semantic approach looks difficult as most of the known models of MALL immediately come with unwanted isomorphisms not valid in the syntax: ⊤ ⊗ A ≃ ⊤ in coherent spaces for example [START_REF] Girard | Linear logic[END_REF]. For this reason we use a syntactic method. We follow the approach by Balat and Di Cosmo [START_REF] Balat | A linear logical view of linear type isomorphisms[END_REF] based on proof-nets. Indeed, proof-nets provide a very 1 Type isomorphisms in MALL good syntax for linear logic where studying composition of proofs by cut, cut-elimination and identity of proofs is very natural. However, already in [START_REF] Balat | A linear logical view of linear type isomorphisms[END_REF] some trick had to be used to deal with units as proof-nets are working perfectly only in the unit-free multiplicative fragment of linear logic. If one puts units aside, there is a notion of proof-nets incorporating both multiplicative and additive connectives in such a way that cut-free proofs are represented in a canonical way, and cut-elimination can be dealt with in a parallel manner. This is the syntax of proof-nets introduced by Hughes & Van Glabbeek in [START_REF] Hughes | Proof nets for unit-free multiplicative-additive linear logic[END_REF].

Commutativity A ⊗ B = B ⊗ A A `B = B `A A ⊕ B = B ⊕ A A & B = B & A Associativity A ⊗ (B ⊗ C) = (A ⊗ B) ⊗ C A `(B `C) = (A `B) `C A ⊕ (B ⊕ C) = (A ⊕ B) ⊕ C A & (B & C) = (A & B) & C Distributivity A ⊗ (B ⊕ C) = (A ⊗ B) ⊕ (A ⊗ C) A `(B & C) = (A `B) & (A `C) Neutrality A ⊗ 1 = A A `⊥ = A A ⊕ 0 = A A & ⊤ = A Annihilation A ⊗ 0 = 0 A `⊤ = ⊤ Table
Our proof of the completeness of the equational theory of Table 1 goes in two steps. First we adapt, in Section 3, the proof of Balat & Di Cosmo [START_REF] Balat | A linear logical view of linear type isomorphisms[END_REF] to the setting of Hughes & Van Glabbeek's proof-nets [START_REF] Hughes | Proof nets for unit-free multiplicative-additive linear logic[END_REF]. This requires a precise analysis of the structure of proof-nets because of the richer structure induced by the presence of the additive connectives. The situation is much more complex than in the multiplicative setting since for example subformulas can be duplicated through distributivity equations, breaking a linearity property crucial in [START_REF] Balat | A linear logical view of linear type isomorphisms[END_REF]. Once this is solved, it remains to add units (Section 4). By lack of a goodenough notion of proof-nets for MALL including units, we go back to the sequent calculus to deal with units on top of the results obtained for the unit-free fragment. This goes through a characterization of the equality of proofs up to cut-elimination and axiom-expansion by means of rule commutations. A result which is not surprising, but never proved before for MALL as far as we know, and rather tedious to settle. Using it, we analyse the behaviour of units inside isomorphisms to conclude that they can be replaced with fresh atoms, once formulas are simplified appropriately. We can conclude by means of the unit-free case. Finally, seeing MALL as a category, we extend our result to conclude that Table 1 (together with A ⊸ B ≃ A ⊥ `B, De Morgan's laws and involutivity of negation) provides the equational theory of isomorphisms valid in all ⋆-autonomous categories with finite products (Section 5).

Full proofs are given in appendix.

Definitions and preliminary results

Multiplicative-Additive Linear Logic

The multiplicative-additive fragment of linear logic [START_REF] Girard | Linear logic[END_REF], denoted by MALL, has formulas given by the following grammar, where X belongs to a given enumerable set of atoms:

A, B := X | X ⊥ | A ⊗ B | A `B | 1 | ⊥ | A & B | A ⊕ B | ⊤ | 0
Orthogonality (•) ⊥ expands into an involution on arbitrary formulas through X ⊥⊥ = X on an atom X, 1 ⊥ = ⊥, ⊥ ⊥ = 1, ⊤ ⊥ = 0, 0 ⊥ = ⊤ and De Morgan's laws (A ⊗ B) ⊥

= B ⊥ `A⊥ , (A `B) ⊥ = B ⊥ ⊗ A ⊥ , (A & B) ⊥ = B ⊥ ⊕ A ⊥ , (A ⊕ B) ⊥ = B ⊥ & A ⊥ .
The non-commutative De Morgan's laws are the good notion of duality, as shown in the context of cyclic linear logic where this leads to planar proof-nets [START_REF] Abrusci | A new correctness criterion for cyclic proof nets[END_REF]. This choice in our setting will often result in planar graphs on our illustrations, with axiom links not crossing each others.

Sequents are lists of formulas of the form ⊢ A 1 , . . . , A n . Sequent calculus rules are:

1 ax ⊢ A ⊥ ,A ⊢ Γ ex ⊢ σ(Γ) ⊢ A, Γ ⊢ A ⊥ , ∆ cut ⊢ Γ, ∆ ⊢ A, Γ ⊢ B, ∆ ⊗ ⊢ A ⊗ B, Γ, ∆ ⊢ A, B, Γ ⊢ A `B, Γ 1 ⊢ 1 ⊢ Γ ⊥ ⊢ ⊥, Γ ⊢ A, Γ ⊢ B, Γ & ⊢ A & B, Γ ⊢ A, Γ ⊕ 1 ⊢ A ⊕ B, Γ ⊢ B, Γ ⊕ 2 ⊢ A ⊕ B, Γ ⊤ ⊢ ⊤, Γ
In practice we consider exchange rules as incorporated in the conclusion of the rule above, thus dealing with rules like:

⊢ A, B, Γ, ∆ ⊢ Γ, A `B, ∆ . In this spirit, when we write ⊢ Γ, A, B, ∆ ⊢ Γ, A `B, ∆ we mean that the appropriate permutation is also incorporated in the rule above.

The main difference with the multiplicative fragment of linear logic (MLL) is the &-rule, which introduces some sharing of the context Γ. From this comes the notion of a slice [START_REF] Girard | Linear logic[END_REF][START_REF] Girard | Proof-nets: the parallel syntax for proof-theory[END_REF] which is a partial proof missing some additive component. Slices are obtained by using the same rules as proofs except for the &-rule which is replaced by its two sliced versions:

⊢ A, Γ & 1 ⊢ A & B, Γ ⊢ B, Γ & 2 ⊢ A & B, Γ
By unit-free MALL, we mean the restriction of MALL to formulas not involving the units 1, ⊥, ⊤ and 0, and as such without the 1, ⊥ and ⊤-rules. When speaking of a positive formula, we mean a formula with main connective ⊗ or ⊕, a unit 1 or 0, or an atom X. A negative formula is one with main connective `or &, a unit ⊥ or ⊤, or a negated atom X ⊥ .

Linear isomorphisms

▶ Definition 1 (Isomorphism). Two formulas A and B are isomorphic, denoted A ≃ B, if there exist proofs π of ⊢ A ⊥ , B and π ′ of ⊢ B ⊥ , A whose composition by cut over B (resp. A) is equal to the axiom on ⊢ A ⊥ , A (resp. ⊢ B ⊥ , B) up to axiom-expansion and cut-elimination. (Axiom-expansion and cut-elimination for MALL are recalled in Appendix A.)

Because of the analogy with the λ-calculus and since there will be no ambiguity, we use the notation = βη for equality of proofs up to cut-elimination (β) and axiom-expansion (η). Similarly, = β is equality up to cut-elimination only. We use the notations π B ▷◁ π ′ for the proof obtained by adding a cut on B between π and π ′ , and A π, π ′ ≃ B when π and π ′ define an isomorphism between A and B, that is when π B ▷◁ π ′ = βη id A and π A ▷◁ π ′ = βη id B (where id A is the axiom-expansion of the proof of ⊢ A ⊥ , A containing just an axiom rule).

We aim to prove that two MALL (resp. unit-free MALL) formulas are isomorphic if and only if they are equal in the equational theory E (resp. E † ) defined as follows.

▶ Definition 2 (Equational theories). We denote by E the equational theory given on Table 1 on Page 3, while E † denotes the part not involving units, i.e. with commutativity, associativity and distributivity only.

Given an equational theory T , the notation A = T B means that formulas A and B are equal in the theory T . As often, the soundness part is easy (but tedious) to prove.

▶ Theorem 3 (Isomorphisms soundness, see Lemma 3 in [START_REF] Laurent | Classical isomorphisms of types[END_REF]).

If A = E B then A ≃ B.
1 With A and B arbitrary formulas, Γ and ∆ contexts (i.e. lists of formulas) and σ a permutation.

All the difficulty lies in the proof of the other implication, completeness, on which the rest of this work focuses.

Axiom-expansion

A first simplification is that we can reduce the definition of isomorphisms to proofs with expanded axioms only, no more using the η relation. Given an MALL proof π, we denote by η(π) the η-normal form of π, i.e. the proof obtained by expanding iteratively all ax-rules in π (axiom-expansion is confluent and strongly normalizing, see Appendix B.1).

▶ Proposition 4 (Reduction to axiom-expanded proofs). Let π and ϖ be MALL proofs such that π = βη ϖ. Then η(π) = β η(ϖ) with, in this sequence, only proofs in η-normal form.

Thus, we will from now on consider only proofs with expanded axioms, manipulated through composition by cut and cut-elimination. To prove completeness, we start with the unit-free case by using a syntactic approach based on the proof-nets from Hughes & Van Glabbeek [START_REF] Hughes | Proof nets for unit-free multiplicative-additive linear logic[END_REF], which are a more canonical representation of proofs [START_REF] Hughes | MALL proof nets identify proofs modulo rule commutation[END_REF].

Proof-nets for unit-free MALL

We use the definition of unit-free MALL proof-net from [START_REF] Hughes | Proof nets for unit-free multiplicative-additive linear logic[END_REF]. Other definitions exist, see the original one from Girard [START_REF] Girard | Proof-nets: the parallel syntax for proof-theory[END_REF], or others such as [START_REF] Di | Jump from parallel to sequential proofs: Additives[END_REF][START_REF] Heijltjes | Conflict nets: Efficient locally canonical MALL proof nets[END_REF]. Still, the definition we take is one of the most satisfactory, from the point of view of canonicity and cut-elimination for instance (see [START_REF] Hughes | Proof nets for unit-free multiplicative-additive linear logic[END_REF][START_REF] Hughes | MALL proof nets identify proofs modulo rule commutation[END_REF], or the introduction of [START_REF] Heijltjes | Conflict nets: Efficient locally canonical MALL proof nets[END_REF] for a comparison of alternative definitions). We recall here quickly this definition of proof-nets. Please refer to [START_REF] Hughes | Proof nets for unit-free multiplicative-additive linear logic[END_REF] for more details.

A sequent is seen as its syntactic forest with as internal vertices its connectives and as leaves the atoms of its formulas. We always identify a formula A with its syntactic tree T (A). A cut pair is a formula A * A ⊥ , for a formula A; the connective * is unordered. A cut sequent [Σ] Γ is composed of a list Σ of cut pairs and a sequent Γ. When Σ = ∅ is empty, we denote it simply by Γ. When we write a `\&-vertex, we mean a `or &-vertex (a negative vertex); similarly a ⊗\⊕-vertex is a ⊗-or ⊕-vertex (a positive vertex). An additive resolution of a cut sequent [Σ] Γ is any result of deleting zero or more cut pairs from Σ and one argument subtree of each additive connective (& or ⊕) of Σ ∪ Γ. A &-resolution of a cut sequent [Σ] Γ is any result of deleting one argument subtree of each &-connective of Σ ∪ Γ.

An (axiom) link on [Σ] Γ is an unordered pair of complementary leaves in Σ ∪ Γ (labeled with X and X ⊥ ). A linking λ on [Σ] Γ is a set of links on [Σ] Γ such that the sets of the leaves of its links form a partition of the set of leaves of an additive resolution of [Σ] Γ, additive resolution which is denoted

[Σ] Γ ↾ λ. A set of linkings Λ on [Σ] Γ toggles a &-vertex W if both arguments (called premises) of W are in [Σ] Γ ↾ Λ := λ∈Λ [Σ] Γ ↾ λ. We say a link a depends on a &-vertex W in Λ if there exist λ, λ ′ ∈ Λ such that a ∈ λ\λ ′ and W is the only &-vertex toggled by {λ; λ ′ }. The graph G Λ is defined as [Σ] Γ ↾ Λ
with the edges from Λ and enriched with jump edges l → W for each leaf l and each &-vertex W such that there exists a ∈ λ ∈ Λ, between l and some l ′ , with a depending on W in Λ. When Λ = {λ} is composed of a single linking, we shall simply denote G λ = G {λ} (which is the graph [Σ] Γ ↾ λ with the edges from λ and no jump edge).

A switch edge of a `\&-vertex N is an in-edge of N , i.e. an edge between N and one of its premises or a jump to N . A switching cycle is a cycle with at most one switch edge of each `\&-vertex. A `-switching of a linking λ is any subgraph of G λ obtained by deleting a switch edge of each `-vertex; denoting by ϕ this choice of edges, the subgraph it yields is G ϕ . These conditions are called the correctness criterion. Condition (P0) is here to prevent unused * -vertices. A cut-free proof-net is one without * -vertices (it respects (P0) trivially). Condition (P1) is a correctness criterion for ALL proof-nets [START_REF] Hughes | Proof nets for unit-free multiplicative-additive linear logic[END_REF] and (P2) is the Danos-Regnier criterion for MLL proof-nets [START_REF] Danos | The structure of multiplicatives[END_REF]. However, (P1) and (P2) together are insufficient for cut-free MALL proof-nets, hence the last condition (P3) taking into account interactions between the slices (see also [START_REF] Di | Jump from parallel to sequential proofs: Additives[END_REF] for a similar condition for example). Sets composed of a single linking λ are not considered in (P3), for by (P2) the graph G λ has no switching cycle.

X 1 X ⊥ 4 & ⊕ * X 5 X ⊥ 6 X ⊥ 2 X 3 & ⊕ X 1 X ⊥ 2 X 3 X ⊥ 4 & ⊕ * X 5 X ⊥ 6
An example of proof-net, illustrated on Figure 1, is the following. On the cut sequent

[X 5 * X ⊥ 6 ] X 1 & X ⊥ 2 , X 3 ⊕ X ⊥ 4 (where each X i is an occurrence of the same atom X), set λ 1 = {(X 1 , X ⊥ 6 ), (X ⊥ 4 , X 5 )} and λ 2 = {(X ⊥ 2 , X 3 )}. One can check {λ 1 ; λ 2 } is a proof-net.
In the particular setting of isomorphisms, we mainly consider proof-nets with two conclusions. This allows to define a notion of duality on leaves and connectives. Consider a cut sequent containing both A and A ⊥ . For V a vertex in (the syntax tree T (A) of) A, we denote by V ⊥ the corresponding vertex in A ⊥ . As expected, V ⊥⊥ = V . This also respects orthogonality for formulas on leaves: given a leaf l of A, labeled by a formula X, the label of l ⊥ is X ⊥ . We can also define a notion of duality on premises: given a premise of a vertex V ∈ T (A), the dual premise of V ⊥ is the corresponding premise in T (A ⊥ ). In other words, if in L -V -R we consider the premise L then in R ⊥ -V ⊥ -L ⊥ its dual premise is L ⊥ .

▶ Definition 6 (Composition). Given proof-nets θ and ϑ of respective conclusions

[Σ] Γ, A and [Ξ] ∆, A ⊥ , the composition over A of θ and ϑ is the proof-net θ A ▷◁ ϑ = {λ ∪ µ | λ ∈ θ, µ ∈ ϑ}, with conclusions [Σ, Ξ, A * A ⊥ ] Γ, ∆.
For example, see Figure 7 with a composition of the proof-nets on Figure 5.

▶ Definition 7 (Cut-elimination). Let θ be a set of linkings on a cut sequent [Σ] Γ, and

(b) If

A = A 1 ⊗ A 2 and A ⊥ = A ⊥ 2 `A⊥ 1 (or vice-versa), replace A * A ⊥ with two cut pairs A 1 * A ⊥ 1 and A 2 * A ⊥ 2 .

Retain all original linkings. (c) If

A = A 1 & A 2 and A ⊥ = A ⊥ 2 ⊕ A ⊥ 1 (or vice-versa), replace A * A ⊥ with two cut pairs A 1 * A ⊥ 1 and A 2 * A ⊥ 2 .
Delete all inconsistent linkings, namely those λ ∈ θ such that in [Σ] Γ ↾ λ the children & and ⊕ of the cut do not take dual premises. Finally, "garbage collect" by deleting any cut pair B * B ⊥ for which no leaf of B * B ⊥ is in any of the remaining linkings.

See Figure 8 for a result on applying steps (b) and (c) to the proof-net of Figure 7.

▶ Proposition 8 (Proposition 5.4 in [START_REF] Hughes | Proof nets for unit-free multiplicative-additive linear logic[END_REF]). Eliminating a cut in a proof-net yields a proof-net.

▶ Theorem 9 (Theorem 5.5 in [START_REF] Hughes | Proof nets for unit-free multiplicative-additive linear logic[END_REF]). Cut-elimination of proof-nets is strongly normalizing and confluent.

A linking λ on a cut sequent [Σ] Γ matches if, for every cut pair

A * A ⊥ in Σ, any given leaf l of A is in [Σ] Γ ↾ λ if and only if l ⊥ of A ⊥ is in [Σ] Γ ↾ λ.
A linking matches if and only if, when cut-elimination is carried out, the linking never becomes inconsistent, and thus is never deleted. This allows defining Turbo Cut-elimination [START_REF] Hughes | Proof nets for unit-free multiplicative-additive linear logic[END_REF], eliminating a cut in a single step by removing inconsistent linkings.

3

Completeness for unit-free MALL

Our method relates closely to the one used by Balat and Di Cosmo in [START_REF] Balat | A linear logical view of linear type isomorphisms[END_REF]. We work on proofnets, as they highly simplify the problem by representing proofs up to rule commutations [START_REF] Hughes | MALL proof nets identify proofs modulo rule commutation[END_REF].

We start by transposing the study of unit-free MALL isomorphisms to proof-nets of a particular shape, called bipartite full (Sections 3.1 and 3.2). Then, we use the distributivity isomorphisms to reduce the problem to special formulas, called distributed, allowing to consider even more constrained proof-nets (Section 3.3). These are the key differences with the proof in MLL from [START_REF] Balat | A linear logical view of linear type isomorphisms[END_REF], where some properties are given for free as there are no slice nor distributivity isomorphism. From this point the problem is similar to unit-free MLL, with commutativity and associativity only. We conclude as in [START_REF] Balat | A linear logical view of linear type isomorphisms[END_REF]: restricting the problem to so-called non-ambiguous formulas, isomorphisms are easily characterized (Section 3.4).

Reduction to proof-nets

We desequentialize a unit-free MALL proof π (with expanded axioms) into a proof-net R(π) by induction on π using the steps detailed on Figure 2, following [START_REF] Hughes | Proof nets for unit-free multiplicative-additive linear logic[END_REF] with the notation θ ▷ [Σ] Γ for "θ is a set of linkings on the cut sequent [Σ] Γ". As identified in Section 5.3.4 of [START_REF] Hughes | Proof nets for unit-free multiplicative-additive linear logic[END_REF], desequentializing with both cut and &-rules is complex, for cuts can be shared (or not)

when translating a &-rule: θ ▷ [Σ, Ξ] A, Γ ϑ ▷ [Σ, Φ] B, Γ & θ ∪ ϑ ▷ [Σ, Ξ, Φ] A & B, Γ
. We choose to never share cuts (Σ = ∅), thus desequentialization is a function. The cost being that the following &-cut commutation yields different proof-nets (contrary to the other commutations, see [START_REF] Hughes | MALL proof nets identify proofs modulo rule commutation[END_REF]).

π 1 ⊢ A, B, Γ π 2 ⊢ A, C, Γ & ⊢ A, B & C, Γ π 3 ⊢ A ⊥ , ∆ cut ⊢ B & C, Γ, ∆ ≡ π 1 ⊢ A, B, Γ π 3 ⊢ A ⊥ , ∆ cut ⊢ B, Γ, ∆ π 2 ⊢ A, C, Γ π 3 ⊢ A ⊥ , ∆ cut ⊢ C, Γ, ∆ & ⊢ B & C, Γ, ∆
▶ Theorem 10 (Sequentialization, Theorem 5.9 in [START_REF] Hughes | Proof nets for unit-free multiplicative-additive linear logic[END_REF]). A set of linkings on a cut sequent is a translation of a MALL proof if and only if it is a proof-net.

▶ Definition 11 (Identity proof-net). We call identity proof-net of a unit-free MALL formula A, the proof-net corresponding to the proof id A (the axiom-expansion of ax ⊢ A ⊥ ,A

).

▶ Theorem 12 (Simulation Theorem). Let π and ϖ be unit-free MALL proof trees (with expanded axioms).

If π = β ϖ, then R(π) = β R(ϖ). A notion of isomorphism A θ, ϑ
≃ B can be defined directly on proof-nets: θ and ϑ are two cut-free proof-nets of respective conclusions A ⊥ , B and B ⊥ , A such that θ B ▷◁ ϑ and ϑ A ▷◁ θ reduce by cut-elimination to identity proof-nets. Using the Simulation Theorem, we obtain:

ax {{(X, X ⊥ )}} ▷ [∅] X, X ⊥ θ ▷ [Σ] Γ ex θ ▷ [Σ] σ(Γ) θ ▷ [Σ] A, Γ ϑ ▷ [Ξ] A ⊥ , ∆ cut {λ ∪ µ | λ ∈ θ, µ ∈ ϑ} ▷ [Σ, Ξ, A * A ⊥ ] Γ, ∆ θ ▷ [Σ] A, Γ ϑ ▷ [Ξ] B, ∆ ⊗ {λ ∪ µ | λ ∈ θ, µ ∈ ϑ} ▷ [Σ, Ξ] A ⊗ B, Γ, ∆ θ ▷ [Σ] A, B, Γ θ ▷ [Σ] A `B, Γ θ ▷ [Ξ] A, Γ ϑ ▷ [Φ] B, Γ & θ ∪ ϑ ▷ [Ξ, Φ] A & B, Γ θ ▷ [Σ] A, Γ ⊕ 1 θ ▷ [Σ] A ⊕ B, Γ θ ▷ [Σ] B, Γ ⊕ 2 θ ▷ [Σ] A ⊕ B, Γ
We use the implicit tracking of formula occurrences downwards through the rules.

Figure 2 Inductive definition of the translation of unit-free MALL proof trees to sets of linkings

X ⊥ X X ⊥ Y ⊥ Y X `⊗ X ⊥ Y ⊥ Y X & ⊕

Reduction to bipartite full proof-nets

▶ Definition 14 (Full, Ax -unique, Bipartite proof-net). A cut-free proof-net is called full if any of its leaves has (at least) one link on it. Furthermore, if for any leaf there exists a unique link on it (possibly shared among several linkings), then we call this proof-net ax-unique.

A cut-free proof-net is bipartite if it has two conclusions, A and B, and each of its links is between a leaf of A and a leaf of B (no link between leaves of A, or between leaves of B).

We show identity proof-nets are bipartite ax-unique, and isomorphisms are bipartite full. Using an induction on the formula A, we can prove the following results on the identity proof-net of A (see Figure 3 for a graphical intuition).

▶ Proposition 15.

(i) An identity proof-net is bipartite ax-unique.

(ii) The axiom links of an identity proof-net are exactly the (l, l ⊥ ), for any leaf l.

(iii) In the identity proof-net of A, exactly one linking is on any given additive resolution of the conclusion A.

Neither fullness, ax-uniqueness nor bipartiteness is preserved by cut anti-reduction. A counter-example is given on Figure 4, with a non bipartite proof-net and a non full one whose composition reduces to the identity proof-net (bipartite ax-unique by Proposition 15(i)). 2However, if both compositions yield identity proof-nets, we get bipartiteness and fullness. ▶ Lemma 16. Let θ and θ ′ be cut-free proof-nets of respective conclusions A ⊥ , B and B ⊥ , A, such that θ ′ A ▷◁ θ reduces to the identity proof-net of B. For any linking λ ∈ θ, there exists

A `A⊥ ⊗ B B ⊥ & B ⊥ À ⊗ A ⊥ B ⊕ B ⊗ A ⊥ À A ⊥ ⊗ A B⊥ A `A⊥ ⊗ B B ⊥ & B ⊥ À ⊗ A ⊥ B ⊕ B ⊗ A ⊥ À A ⊥ ⊗ A B⊥ *
λ ′ ∈ θ ′ such that λ ∪ λ ′ matches in the composition over B of θ and θ ′ , θ B ▷◁ θ ′ .
Proof. Let us consider a linking λ ∈ θ, and call C the choices of premise on additive connectives of B that λ makes. We search some λ ′ ∈ θ ′ making the dual choices of premise on additive connectives of B ⊥ compared to C. Consider the composition of θ and θ ′ over A. It reduces to the identity proof-net of B by hypothesis. By Proposition 15(iii), there exists a unique linking in the identity proof-net of B corresponding to C. Furthermore, the linkings of the identity proof-net are derived from the µ ∪ µ ′ for µ a linking of θ and µ ′ one of θ ′ , with µ ∪ µ ′ matching for a cut over A: a linking in the identity proof-net is a linking of the form µ ∪ µ ′ where axiom links (l, m) ∈ µ and (m ⊥ , l ⊥ ) ∈ µ ′ are replaced with (l, l ⊥ ), with l a leaf of B and m one of A ⊥ (because an identity proof-net has only links of the form (l, l ⊥ ) by Proposition 15(ii)). Therefore, there exist µ ∈ θ and µ ′ ∈ θ ′ such that µ makes the choices C on B and µ ∪ µ ′ matches for the composition of θ and θ ′ over both A and B. But λ makes the same choices C on B as µ: λ ∪ µ ′ also matches for a cut over

◀ A B C ⊕ ⊗ C ⊥ A ⊥ B ⊥ A ⊥ `& A B A C ⊗ ⊗ ⊕ C ⊥ B ⊥ A ⊥ & Figure 5 Proof-nets for A ⊗ (B ⊕ C) ≃ (A ⊗ B) ⊕ (A ⊗ C)

Distribution

In general, isomorphisms do not yield ax-unique proof-nets. A counter-example is distributivity: 5. Nonetheless, distributivity equations are the only ones in E † not giving ax-unique proof-nets. We will restrict our study to so-called distributed formulas. Once formulas are distributed, distributivity isomorphisms can be ignored, and isomorphisms between distributed formulas happen to be bipartite ax-unique.

A ⊗ (B ⊕ C) ≃ (A ⊗ B) ⊕ (A ⊗ C), see Figure
▶ Definition 20 (Distributed formula). An MALL formula is distributed if it does not have any sub-formula of the form

A ⊗ (B ⊕ C), (A ⊕ B) ⊗ C, A ⊗ 1, 1 ⊗ A, A ⊕ 0, 0 ⊕ A, A ⊗ 0, 0 ⊗ A or their duals (C & B) `A, C `(B & A), ⊥ `A, A `⊥, ⊤ & A, A & ⊤, ⊤ `A, A
`⊤ (where A, B and C are any formulas).

▶ Remark. This notion is stable by duality: if A is distributed, so is A ⊥ .

▶ Proposition 21. If E is complete for isomorphisms between distributed formulas, then it is complete for isomorphisms between arbitrary formulas.

We mostly use the correctness criterion through the fact we can sequentialize, i.e. recover a proof tree from a proof-net by Theorem 10. However, in order to prove ax-uniqueness, we make a direct use of the correctness criterion to deduce geometric properties of proof-nets. This part of the proof takes benefits from the specificities of this syntax. We begin with two preliminary results. For Λ a set of linkings and W a &-vertex, Λ W denote the set of all linkings in Λ whose additive resolution does not contain the right argument of W .

▶ Lemma 22 (Lemma 4.32 in [START_REF] Hughes | Proof nets for unit-free multiplicative-additive linear logic[END_REF], adapted). Let ω be a jump-free switching cycle in a proof-net θ. There exists a subset of linkings Λ ⊆ θ such that ω ⊆ G Λ , ω ̸ ⊆ G Λ W and for any &-vertex W toggled by Λ, there exists an axiom link a ∈ ω depending on W in Λ.

For U and V vertices in a tree, their first common descendant is the vertex of the tree which is a descendant of both U and V and which has no descendant respecting this property (with a tree represented with its root at the bottom, which is a descendant of the leaves).

▶ Lemma 23. Let θ be a proof-net of conclusions Γ, A. If there is a jump edge l j -→ W with l, W ∈ T (A) and W not a descendant of l, then their first common descendant C is a `.

Proof. As there is a jump l j -→ W , there exist linkings λ, λ ′ ∈ θ such that W is the only & toggled by {λ; λ ′ }, and a link a ∈ λ\λ ′ using the leaf l. In particular, the jump l j -→ W is in G {λ;λ ′ } . For l and W are both in the additive resolution of λ, both premises of C are in the additive resolution of λ, thus C cannot be an additive connective, so not a & nor a ⊕-vertex.

Assume by contradiction that C is a ⊗. Call δ the path in T (A) from W to C, and µ the one from C to l (see Figure 6). Then, (l j -→ W )δµ is a switching cycle in G {λ;λ ′ } . According to (P3), there exists a & toggled by {λ; λ ′ } not in any switching cycle of G {λ;λ ′ } . A contradiction, for W is the only & toggled by {λ; λ ′ }. Whence, C can only be a `.

◀ A T (A) l W & C µ δ j Figure 6
Illustration of the proof of Lemma 23 Now, let us prove that isomorphisms of distributed formulas are bipartite ax-unique. We will consider proof-nets corresponding to an isomorphism that we cut and where we eliminate all cuts not involving atoms. To give some intuition, let us consider the non-ax-unique proof-nets of Figure 5. Composing them together by cut on (A ⊗ B) ⊕ (A ⊗ C) gives the proof-net illustrated on Figure 7. Reducing all cuts not involving atoms yields the proof-net on Figure 8, that we call an almost reduced composition. We stop there because of the switching cycle produced by the two links on A (dashed in blue on Figure 8), less visible in the non-reduced composition of Figure 7. However, reducing all cuts gives the identity proof-net, which has no switching cycle: during these reductions, both links on A are merged. By using almost reduced composition, we are going to prove that links preventing ax-uniqueness yield switching cycles, and moreover that these cycles are due to non-distributed formulas only.

A B C ⊕ ⊗ C ⊥ A ⊥ B ⊥ A ⊥ `& A B A C ⊗ ⊗ ⊕ C ⊥ B ⊥ A ⊥ & *
▶ Definition 24 (Almost reduced composition). Take θ and θ ′ cut-free proof-nets of respective conclusions A, B and B ⊥ , C. The almost reduced composition over B of θ and θ ′ is the proof-net resulting from the composition over B of θ and θ ′ where we repeatedly reduce all cuts not involving atoms ( i.e. not applying step (a) of Definition 7).

Let us fix A and B two unit-free MALL (not necessarily distributed yet) formulas as well as θ and θ ′ such that A θ, θ ′ ≃ B. By Theorem 19, θ and θ ′ are bipartite full. We denote by ϑ the almost reduced composition over B of θ and θ ′ . Here, we can extend our duality on vertices and premises (defined in Section 2.4) to links. ▶ Lemma 25. Given l a leaf of A (resp. A ⊥ ) and m one of B ⊥ (resp. B), there is an axiom link a = (l, m) in some linking λ ∈ ϑ if and only if there is an axiom link (l ⊥ , m ⊥ ) in the same linking λ, that we will denote a ⊥ = (l ⊥ , m ⊥ ) (see Figure 9).

A B C ⊕ ⊗ C ⊥ A ⊥ B ⊥ A ⊥ A B A C C ⊥ B ⊥ A ⊥ & * * * *
Proof. By symmetry, assume (l, m) ∈ λ ∈ ϑ. As the cut m * m ⊥ belongs to the additive resolution of λ (for m is inside), m ⊥ is a leaf in this resolution. Thus, there is a link (m ⊥ , l ′ ) ∈ λ for some leaf l ′ , which necessarily belongs to A by bipartiteness of θ ′ . It stays to prove l ′ = l ⊥ . If we were to eliminate all cuts in ϑ, we would get the identity proof-net on A by hypothesis. But eliminating the cut m * m ⊥ yields a link (l, l ′ ), which is not modified by the elimination of the other atomic cuts. By Proposition 15(ii), l ′ = l ⊥ follows. ◀ ▶ Lemma 26. Let λ be a linking of ϑ, and V an additive vertex in its additive resolution. Then V ⊥ is also inside, with as premise kept the dual premise of the one kept for V .

▶ Lemma 27. Let W and P be respectively a &-vertex and a ⊕-vertex in ϑ, with W an ancestor of P . Then for any axiom link a depending on W in ϑ, a also depends on P ⊥ in ϑ.

Proof. There exist linkings λ, λ ′ ∈ ϑ such that W is the only & toggled by {λ; λ ′ } and a ∈ λ\λ ′ . We consider a linking λ P ⊥ defined by taking an arbitrary &-resolution of λ where we choose the other premise for P ⊥ (and arbitrary premises for &-vertices introduced this way): by (P1), there exists a unique linking on it. By Lemma 26, the additive resolutions of λ and λ P ⊥ (resp. λ and λ ′ ) differ exactly on ancestors of P and P ⊥ (resp. W and W ⊥ ). Thus, the additive resolutions of λ ′ and λ P ⊥ also differ exactly on ancestors of P and P ⊥ , for W is an ancestor of P . In particular, {λ; λ P ⊥ }, as well as {λ ′ ; λ P ⊥ }, toggles only P ⊥ . If a ∈ λ P ⊥ , then a depends on P ⊥ in {λ ′ ; λ P ⊥ }. Otherwise, a depends on P ⊥ in {λ; λ P ⊥ }. ◀

The key result to use distributivity is that a positive vertex "between" a leaf l and a &-vertex W in the same tree prevents them from interacting, i.e. there is no jump l j -→ W . ▶ Lemma 28. Let l j -→ W be a jump edge in ϑ, with l not an ancestor of W and l, W ∈ T (A ⊥ ) (resp. T (A)). Denoting by N the first common descendant of l and W , there is no positive vertex in the path between N and W in T (A ⊥ ) (resp. T (A)).

Proof. Let P be a vertex on the path between N and W in T (A ⊥ ). By Lemma 23, N is a `-vertex. We prove by contradiction that P can neither be a ⊕ nor a ⊗-vertex.

Suppose P is a ⊕-vertex. By Lemma 27, a depends on P ⊥ , and so does a ⊥ through Lemma 25: there is a jump edge l ⊥ j -→ P ⊥ . Applying Lemma 23, the first common descendant of l ⊥ and P ⊥ , which is N ⊥ , is a `-vertex: a contradiction as it is a ⊗-vertex.

Assume now P to be a ⊗-vertex. As there is a jump l j -→ W , there exist linkings λ, λ ′ ∈ ϑ and a leaf m of B such that W is the only & toggled by {λ; λ ′ } and a = (l, m) ∈ λ\λ ′ . For P is a ⊗, there is a leaf p which is an ancestor of P in the additive resolution of λ, from a different premise of P than W ; it is used by a link b = (p, q) ∈ λ3 (see Figure 10). Then the switching cycle Proof. We already know that θ and θ ′ are bipartite full thanks to Theorem 19. We reason by contradiction and assume w.l.o.g. that θ is not ax-unique: there exist a leaf l of A ⊥ and two distinct leaves l 0 and l 1 of B with links a = (l, l 0 ) and b = (l, l 1 ) in θ. We consider ϑ the almost reduced composition of θ and θ ′ over B, depicted on Figure 11. By Lemma 16, a and b are also links in ϑ (for the linkings they belong to in θ have matching linkings in θ ′ , and we did not eliminate atomic cuts). Using Lemma 25, we have in

A ⊥ A l p W & P ⊗ N `l⊥ p ⊥ W ⊥ ⊕ P ⊥ Ǹ ⊥ ⊗ B B ⊥ . . . q m m ⊥ q ⊥ . . . * * . . . a a ⊥ b b ⊥ j Figure 10 Switching cycle containing W if P is a ⊗-vertex in the proof of Lemma 28 A ⊥ . . . * * . . . A B B ⊥ T (A ⊥ ) T (A) l . . . l 0 l 1 . . . . . . l ⊥ 1 l ⊥ 0 . . . a b l ⊥ a ⊥ b ⊥
l j -→ W → P ← p b -q → * ← q ⊥ b ⊥ -p ⊥ → P ⊥ → N ⊥ ← l ⊥ a ⊥ -m ⊥ → * ← m a -l (dashed in blue on
G ϑ a switching cycle ω = l a -l 0 → * ← l ⊥ 0 a ⊥ -l ⊥ b ⊥ -l ⊥ 1 → * ← l 1 b -l.
Let Λ be a set of linkings given by Lemma 22 applied to ω. As there are two distinct links on l in ω ⊆ G Λ , Λ contains at least two linkings. By (P3), there exists W a & toggled by Λ that is not in any switching cycle of G Λ . By Lemma 22, a, a ⊥ , b or b ⊥ depends on W . So a or b depends on W by Lemma 25; w.l.o.g. a depends on W . The vertex W belongs to either T (A) or T (A ⊥ ): up to considering a ⊥ instead of a, W is in T (A ⊥ ). Remark l is not an ancestor of W : if it were, by symmetry assume it is a left-ancestor. Whence a and b belong to Λ W , so a ⊥ and b ⊥ too (Lemma 25); thus ω ⊆ G Λ W , contradicting Lemma 22. By Lemma 23, the first common descendant N of l and W in T (A ⊥ ) is a `. There is a ⊗\⊕ on the path between the `N and its ancestor the & W in T (A ⊥ ), for there is no sub-formula of the shape -`(-& -) in the distributed A ⊥ . This contradicts Lemma 28. ◀

Non-ambiguous formulas & Completeness for unit-free MALL

Once our study is restricted to bipartite ax-unique proof-nets, we can also restrict formulas.

▶ Definition 30 (Non-ambiguous formula). A formula A is said non-ambiguous if each atom in A occurs at most once positive and once negative.

▶ Remark. This means all leaves in A are distinct. If A is non-ambiguous, so is A ⊥ .

For instance, X & X ⊥ is non-ambiguous, whereas (A ⊗ B) ⊕ (A ⊗ C) is ambiguous. The reduction to non-ambiguous formulas requires to restrict to distributed formulas first: in

(A ⊗ B) ⊕ (A ⊗ C) ≃ A ⊗ (B ⊕ C)
we need the two occurrences of A to factorize. The two following results are a direct adaptation of Section 3 in [START_REF] Balat | A linear logical view of linear type isomorphisms[END_REF].

▶ Corollary 31 (Reduction to distributed non-ambiguous formulas). The set of couples of distributed formulas A and B such that

A θ, ϑ

≃ B is the set of instances (by a substitution on atoms) of couples of distributed non-ambiguous formulas

A ′ and B ′ such that A ′ θ ′ , ϑ ′ ≃ B ′ .
▶ Corollary 32. Let A and B be non-ambiguous formulas. If there exist bipartite proof-nets θ and ϑ of respective conclusions A ⊥ , B and

B ⊥ , A, then A θ, ϑ ≃ B.
We then prove the completeness of E † for unit-free MALL by reasoning as in Section 4 of [START_REF] Balat | A linear logical view of linear type isomorphisms[END_REF] (with some more technicalities for we reorder not only `-vertices but also &-vertices).

▶ Theorem 33 (Isomorphisms completeness for unit-free MALL). Given A and B two unit-free MALL formulas, if

A ≃ B, then A = E † B.

Completeness for MALL with units

We now consider full MALL, with units, and show how to reduce it to the unit-free case.

We solve this addition purely in sequent calculus showing that, for distributed formulas, multiplicative and additive units can be replaced by fresh atoms.

A key property of proof-nets is to define a quotient of sequent calculus proofs up to rule commutations [START_REF] Hughes | MALL proof nets identify proofs modulo rule commutation[END_REF] (see Appendix A for rule commutations in MALL). Because no such notion of proof-nets exist with units, we are forced to stay in the sequent calculus, meaning that we have to deal with possible rule commutations. As a key example, cut-elimination in proof-nets is confluent and leads to a unique normal form. This is not true in the sequent calculus and we need to relate the different possible cut-free proofs obtained by cut-elimination.

▶ Theorem 34 (Confluence up to rule commutations). If π 1 and π 2 are cut-free proofs obtained by cut-elimination from the same proof π, then π 1 and π 2 are equal up to rule commutations. This result is not surprising but has not already been proved as far as we know for it is rather tedious to establish. It is an important general result about sequent calculus which we are convinced should hold for full linear logic. It can be lifted to βη-equality of proofs.

▶ Theorem 35. Let π and ϖ be βη-equal MALL proofs. Then, letting π ′ (resp. ϖ ′ ) be a result of expanding all axioms and then eliminating all cuts in π (resp. ϖ), π ′ is equal to ϖ ′ up to rule commutations.

After these general properties, let us move to the question of type isomorphisms. We need to analyse the behaviour of units in proofs equal to id A up to rule commutations. We only do so for a distributed formula A as we have already seen it is enough in Section 3.3.

▶ Proposition 36. Let π be a proof equal, up to rule commutations, to id

A with A distributed.
The ⊤-rules of π are of the shape ⊤ ⊢ ⊤, 0 (with ⊤ in A being the dual of 0 in A ⊥ , or vice-versa) and ⊥-rules and 1-rules come by pairs separated with ⊕ i -rules only, called a 1/ ⊕ /⊥-pattern:

1 ⊢ 1 ρ ⊢ F ⊥ ⊢ ⊥, F
where ρ is a sequence of ⊕ i -rules (with ⊥ in A being the dual of 1 in A ⊥ , or vice-versa). Moreover, there are no sequent in π of the shape ⊢ B & C.

Proof. The key idea is to find properties of id A preserved by all rule commutations and ensuring the properties described in the statement. For any sequent S in the proof:

(1) the formulas of S are distributed;

(2) if ⊤ is a formula of S, then S = ⊢ ⊤, 0;

(3) if ⊥ is a formula of S, then S = ⊢ ⊥, F with F given by the following grammar

F := 1 | F ⊕ D | D ⊕ F , where the distinguished 1 is the dual of ⊥ in A ⊥ if ⊥ a sub-formula of A (or vice-versa)
, D is any formula, and the sub-proof of π above S is a sequence of ⊕ i rules leading to the distinguished 1;

(4) if B & C is a formula of S, then S = ⊢ B & C, F
with F given by the following grammar Moving each ⊥-rule up to the associated 1-rule (which can be done up to βη-equality) allows us to consider units as fresh atoms introduced by ax-rules and to apply Theorem 33.

F := C ⊥ ⊕ B ⊥ | F ⊕ D | D ⊕ F , where the distinguished C ⊥ ⊕ B ⊥ is the dual of B & C in A ⊥ if B & C a sub-

▶ Theorem 38 (Isomorphisms completeness with units). If

A ≃ B then A = E B.

Star-autonomous categories with finite products

We prove here that the equational theory E (along A ⊸ B ≃ A ⊥ `B, De Morgan's laws and involutivity of negation) also corresponds to the isomorphisms present in all ⋆-autonomous categories with finite products. For the historical result of how linear logic can be seen as a category, see [START_REF] Seely | Linear logic, ⋆-autonomous categories and cofree coalgebras[END_REF]. We establish this result from the one on MALL, first proving that MALL (with proofs considered up to βη-equality) defines a ⋆-autonomous category with finite products (Section 5.1). Then, we conclude using a semantic method (Section 5.2).

MALL as a star-autonomous category with finite products

The logic MALL, with proofs taken up to βη-equality, defines a ⋆-autonomous category with finite products, that we will call MALL. Indeed, we can define it as follows.

Objects of MALL are formulas of MALL, while its morphisms from A to B are proofs of ⊢ A ⊥ , B, considered up to βη-equality. 4 One can check that a proof of MALL is an isomorphism if and only if, when seen as a morphism, it is an isomorphism in MALL.

We define a bifunctor ⊗ on MALL, associating to formulas (i.e. objects) A and B the formula A ⊗ B and to proofs (i.e. morphisms) π 0 and π 1 respectively of ⊢ A ⊥ 0 , B 0 and

⊢ A ⊥ 1 , B 1 the following proof of ⊢ (A 0 ⊗ A 1 ) ⊥ , B 0 ⊗ B 1 : π 0 ⊢ A ⊥ 0 , B 0 π 1 ⊢ A ⊥ 1 , B 1 ⊗ ⊢ A ⊥ 1 , A ⊥ 0 , B 0 ⊗ B 1 ⊢ A ⊥ 1 `A⊥ 0 , B 0 ⊗ B 1 One can check that (MALL, ⊗, 1, α, λ, ρ, γ) forms a symmetric monoidal category, where 1 is the 1-formula, α are isomorphisms of MALL associated to (A ⊗ B) ⊗ C ≃ A ⊗ (B ⊗ C) seen
as a natural isomorphism of MALL, and similarly for λ with 1

⊗ A ≃ A, ρ with A ⊗ 1 ≃ A, and γ with A ⊗ B ≃ B ⊗ A.
Furthermore, define A ⊸ B := A ⊥ `B and ev A,B as the following morphism from

(A ⊸ B) ⊗ A to B (i.e. a proof of ⊢ A ⊥ `(B ⊥ ⊗ A), B): ax ⊢ B ⊥ ,B ax ⊢ A ⊥ ,A ⊗ ⊢ A ⊥ , B ⊥ ⊗ A, B ⊢ A ⊥ `(B ⊥ ⊗ A), B
It can be checked that MALL is a symmetric monoidal closed category with as exponential object (A ⊸ B, ev A,B ) for objects A and B.

Moreover, one can also check that ⊥ is a dualizing object for this category, making MALL a ⋆-autonomous category. This relies on the following morphism from (A ⊸ ⊥) ⊸ ⊥ to A (which is an inverse of the curryfication of ev A,⊥ ):

1 ⊢ 1 ax ⊢ A ⊥ ,A ⊥ ⊢ A ⊥ , ⊥, A ⊢ A ⊥ `⊥, A ⊗ ⊢ 1 ⊗ (A ⊥ `⊥), A
Finally, ⊤ is a terminal object of MALL, and A & B is the product of objects A and B, with as projections π A and π B the following morphisms respectively from

A & B to A and from A & B to B: ax ⊢ A ⊥ ,A ⊕ 2 ⊢ B ⊥ ⊕ A ⊥ , A and ax ⊢ B ⊥ ,B ⊕ 1 ⊢ B ⊥ ⊕ A ⊥ , B
Therefore, MALL is a ⋆-autonomous category with finite products [START_REF] Seely | Linear logic, ⋆-autonomous categories and cofree coalgebras[END_REF].

Isomorphisms of star-autonomous categories with finite products

We take the same notations as in the previous section (& for product, . . . ). One can easily check that isomorphisms in a ⋆-autonomous category with finite products form a congruence (as all binary connectives define bifunctors), and that E is sound (i.e. that equations defining

A ⊸ B ≃ A ⊥ `B X ⊥⊥ ≃ X (A ⊗ B) ⊥ ≃ B ⊥ `A⊥ (A `B) ⊥ ≃ B ⊥ ⊗ A ⊥ 1 ⊥ ≃ ⊥ ⊥ ⊥ ≃ 1 (A & B) ⊥ ≃ B ⊥ ⊕ A ⊥ (A ⊕ B) ⊥ ≃ B ⊥ & A ⊥ ⊤ ⊥ ≃ 0 0 ⊥ ≃ ⊤
(A ⊸ ⊥) ⊸ ⊥ ≃ (A ⊥ `⊥) ⊥ `⊥ ≃ (A ⊥ `⊥) ⊥ ≃ 1 ⊗ A ⊥⊥ ≃ A ⊥⊥ ≃ A (

Conclusion

Extending the result of Balat and Di Cosmo in [START_REF] Balat | A linear logical view of linear type isomorphisms[END_REF], we give an equational theory characterising type isomorphisms in multiplicative-additive linear logic with units as well as in ⋆-autonomous categories with finite products: the one described on Table 1 on Page 3 (together with Table 2 for ⋆-autonomous categories). Looking at the proof, we get as a sub-result that isomorphisms for ALL (resp. unit-free ALL) are given by the equational theory E (resp. E † ) restricted to ALL formulas (and more generally this applies to any fragment of MALL, thanks to the sub-formula property). Proof-nets were a major tool to prove completeness, as notions like fullness and ax-uniqueness are much harder to define and manipulate in sequent calculus. However, we could not use them for taking care of the (additive) units, because there is no known appropriate notion of proof-nets. We have thus been forced to develop (some parts of) the theory of cut-elimination, axiom-expansion and rule commutations for the sequent calculus of MALL with units. The immediate question to address is the extension of our results to the characterization of type isomorphisms for full propositional linear logic, thus including the exponential connectives. This is clearly not immediate since the interaction between additive and exponential connectives is not well described in proof-nets.

A more general problem is the study of type retractions (where only one of the two compositions yields an identity) which is also much more difficult (see for example [START_REF] Regnier | Retractions of types with many atoms[END_REF]). The question is mostly open in the case of linear logic. Even in multiplicative linear logic (where there is for example a retraction between A and (A ⊸ A) ⊸ A = (A ⊗ A ⊥ ) `A which is not an isomorphism, and where the associated proof-nets are not bipartite), no characterization is known. In the multiplicative-additive fragment, the problem looks even harder, with more retractions; for instance the one depicted on Figure 4, but there also is a retraction between A and A ⊕ A. 3 Axiom-expansion in the sequent calculus of MALL In appendix are first described transformations of proofs: axiom-expansion η -→, cutelimination β -→ and rule commutations = c (Appendix A). Then come proofs of various sections of the paper: about reduction to axiom-expanded proofs (Appendix B), completeness for unit-free MALL (Appendix C) and for full MALL (Appendix D). Proofs are given in the order their results appear in the main part.

`-⊗ ax ⊢ A ⊗ B, B ⊥ `A⊥ η -→ ax ⊢ A ⊥ ,A ax ⊢ B ⊥ ,B ⊗ ⊢ A ⊗ B, A ⊥ , B ⊥ ⊢ A ⊗ B, B ⊥ `A⊥ & -⊕ ax ⊢ A ⊕ B, B ⊥ & A ⊥ η -→ ax ⊢ B, B ⊥ ⊕2 ⊢ A ⊕ B, B ⊥ ax ⊢ A, A ⊥ ⊕1 ⊢ A ⊕ B, A ⊥ & ⊢ A ⊕ B, B ⊥ & A ⊥ ⊥ -1 ax ⊢ 1, ⊥ η -→ 1 ⊢ 1 ⊥ ⊢ 1, ⊥ ⊤ -0 ax ⊢ 0, ⊤ η -→ ⊤ ⊢ 0, ⊤ Table

A Transformations of sequent calculus proofs in MALL

▶ Definition 40. In the sequent calculus of MALL, we call axiom-expansion the rewriting system η -→ described on Table 3.

▶ Definition 41. In the sequent calculus of MALL, we call cut-elimination the rewriting system β -→ described on Tables 4 and5 (up to commuting the two branches of a cut-rule). 5 ▶ Definition 42. In the sequent calculus of MALL, we call rule commutation the equational theory = c described on Tables 6 and7. This corresponds to rule commutations in cut-free MALL; in particular, in a ⊤ -⊗ permutation we assume the created or erased sub-proof to be cut-free.

We denote the reflexive transitive closure of η -→ (resp.

β -→, = c ) by η * -→ (resp. β * -→, = * c ).

B Proofs for the reduction to axiom-expanded proofs

This appendix contains proofs for the results stated in Section 2.3.

B.1 Axiom-expansion is confluent and strongly normalizing

▶ Proposition 43. The relation η -→ is confluent and strongly normalizing. 5 Another possible key case would be the following:

π1 ⊢ A, Γ π2 ⊢ B, ∆ ⊗ ⊢ A ⊗ B, Γ, ∆ π3 ⊢ B ⊥ , A ⊥ , Σ ⊢ B ⊥ `A⊥ , Σ cut ⊢ Γ, ∆, Σ β -→ π2 ⊢ B, ∆ π1 ⊢ A, Γ π3 ⊢ B ⊥ , A ⊥ , Σ cut ⊢ B ⊥ , Γ, Σ cut ⊢ Γ, ∆, Σ
This case can be simulated with the given `-⊗ key case and a cut -cut commutative case.

ax ax ⊢ A ⊥ ,A π ⊢ A, Γ cut ⊢ A, Γ β -→ π ⊢ A, Γ `-⊗ π1 ⊢ A, Γ π2 ⊢ B, ∆ ⊗ ⊢ A ⊗ B, Γ, ∆ π3 ⊢ B ⊥ , A ⊥ , Σ ⊢ B ⊥ `A⊥ , Σ cut ⊢ Γ, ∆, Σ β -→ π1 ⊢ A, Γ π2 ⊢ B, ∆ π3 ⊢ B ⊥ , A ⊥ , Σ cut ⊢ A ⊥ , ∆, Σ cut ⊢ Γ, ∆, Σ & -⊕1 π1 ⊢ A1, Γ π2 ⊢ A2, Γ & ⊢ A1 & A2, Γ π3 ⊢ A ⊥ 2 , ∆ ⊕1 ⊢ A ⊥ 2 ⊕ A ⊥ 1 , ∆ cut ⊢ Γ, ∆ β -→ π2 ⊢ A2, Γ π3 ⊢ A ⊥ 2 , ∆ cut ⊢ Γ, ∆ & -⊕2 π1 ⊢ A1, Γ π2 ⊢ A2, Γ & ⊢ A1 & A2, Γ π3 ⊢ A ⊥ 1 , ∆ ⊕2 ⊢ A ⊥ 2 ⊕ A ⊥ 1 , ∆ cut ⊢ Γ, ∆ β -→ π1 ⊢ A1, Γ π3 ⊢ A ⊥ 1 , ∆ cut ⊢ Γ, ∆ ⊥ -1 1 ⊢ 1 π ⊢ Γ ⊥ ⊢ Γ, ⊥ cut ⊢ Γ β -→ π ⊢ Γ
(No ⊤ -0 key case as there are no rule for 0.)

`-cut π1 ⊢ A, B, C, Γ ⊢ A, B `C, Γ π2 ⊢ A ⊥ , ∆ cut ⊢ B `C, Γ, ∆ β -→ π1 ⊢ A, B, C, Γ π2 ⊢ A ⊥ , ∆ cut ⊢ B, C, Γ, ∆ ⊢ B `C, Γ, ∆ ⊗ -cut -1 π1 ⊢ A, B, Γ π2 ⊢ C, ∆ ⊗ ⊢ A, B ⊗ C, Γ, ∆ π3 ⊢ A ⊥ , Σ cut ⊢ B ⊗ C, Γ, ∆, Σ β -→ π1 ⊢ A, B, Γ π3 ⊢ A ⊥ , Σ cut ⊢ B, Γ, Σ π2 ⊢ C, ∆ ⊗ ⊢ B ⊗ C, Γ, ∆, Σ ⊗ -cut -2 π1 ⊢ B, Γ π2 ⊢ A, C, ∆ ⊗ ⊢ A, B ⊗ C, Γ, ∆ π3 ⊢ A ⊥ , Σ cut ⊢ B ⊗ C, Γ, ∆, Σ β -→ π1 ⊢ B, Γ π2 ⊢ A, C, ∆ π3 ⊢ A ⊥ , Σ cut ⊢ C, ∆, Σ ⊗ ⊢ B ⊗ C, Γ, ∆, Σ & -cut π1 ⊢ A, B, Γ π2 ⊢ A, C, Γ & ⊢ A, B & C, Γ π3 ⊢ A ⊥ , ∆ cut ⊢ B & C, Γ, ∆ β -→ π1 ⊢ A, B, Γ π3 ⊢ A ⊥ , ∆ cut ⊢ B, Γ, ∆ π2 ⊢ A, C, Γ π3 ⊢ A ⊥ , ∆ cut ⊢ C, Γ, ∆ & ⊢ B & C, Γ, ∆ ⊕i -cut π1 ⊢ A, Bi, Γ ⊕i ⊢ A, B1 ⊕ B2, Γ π2 ⊢ A ⊥ , ∆ cut ⊢ B1 ⊕ B2, Γ, ∆ β -→ π1 ⊢ A, Bi, Γ π2 ⊢ A ⊥ , ∆ cut ⊢ Bi, Γ, ∆ ⊕i ⊢ B1 ⊕ B2, Γ, ∆ ⊥ -cut π1 ⊢ A, Γ ⊥ ⊢ A, ⊥, Γ π2 ⊢ A ⊥ , ∆ cut ⊢ ⊥, Γ, ∆ β -→ π1 ⊢ A, Γ π2 ⊢ A ⊥ , ∆ cut ⊢ Γ, ∆ ⊥ ⊢ ⊥, Γ, ∆ ⊤ -cut ⊤ ⊢ A, ⊤, Γ π ⊢ A ⊥ , ∆ cut ⊢ ⊤, Γ, ∆ β -→ ⊤ ⊢ ⊤, Γ, ∆ cut -cut π1 ⊢ A, B, Γ π2 ⊢ B ⊥ , ∆ cut ⊢ A, Γ, ∆ π3 ⊢ A ⊥ , Σ cut ⊢ Γ, ∆, Σ β -→ π1 ⊢ A, B, Γ π3 ⊢ A ⊥ , Σ cut ⊢ B, Γ, Σ π2 ⊢ B ⊥ , ∆ cut ⊢ Γ, ∆, Σ (No ax -cut nor 1 -cut nor 0 -cut commutative
cases as the ax and 1-rules have no context and there are no rule for 0.)

⊤ ⊢ A1 `A2, ⊤, Γ C ⊤ -→ ←- C ⊤ `⊤ ⊢ A1, A2, ⊤, Γ ⊢ A1 `A2, ⊤, Γ π1 ⊢ A1, A2, Γ ⊢ A1 `A2, Γ ⊥ ⊢ A1 `A2, ⊥, Γ C ⊥ -→ ←- C ⊥ `π1 ⊢ A1, A2, Γ ⊥ ⊢ A1, A2, ⊥, Γ ⊢ A1 `A2, ⊥, Γ ⊤ ⊢ A1 ⊗ A2, ⊤, Γ, ∆ C ⊗ ⊤ -→ ←- C ⊤ ⊗ ⊤ ⊢ A1, ⊤, Γ π ⊢ A2, ∆ ⊗ ⊢ A1 ⊗ A2, ⊤, Γ, ∆ π1 ⊢ A1, Γ π2 ⊢ A2, ∆ ⊗ ⊢ A1 ⊗ A2, Γ, ∆ ⊥ ⊢ A1 ⊗ A2, ⊥, Γ, ∆ C ⊗ ⊥ -→ ←- C ⊥ ⊗ π1 ⊢ A1, Γ ⊥ ⊢ A1, ⊥, Γ π2 ⊢ A2, ∆ ⊗ ⊢ A1 ⊗ A2, ⊥, Γ, ∆ ⊤ ⊢ A1 ⊗ A2, ⊤, Γ, ∆ C ⊗ ⊤ -→ ←- C ⊤ ⊗ π ⊢ A1, Γ ⊤ ⊢ A2, ⊤, ∆ ⊗ ⊢ A1 ⊗ A2, ⊤, Γ, ∆ π1 ⊢ A1, Γ π2 ⊢ A2, ∆ ⊗ ⊢ A1 ⊗ A2, Γ, ∆ ⊥ ⊢ A1 ⊗ A2, ⊥, Γ, ∆ C ⊗ ⊥ -→ ←- C ⊥ ⊗ π1 ⊢ A1, Γ π2 ⊢ A2, ∆ ⊥ ⊢ A2, ⊥, ∆ ⊗ ⊢ A1 ⊗ A2, ⊥, Γ, ∆ ⊤ ⊢ A1 & A2, ⊤, Γ C & ⊤ -→ ←- C ⊤ & ⊤ ⊢ A1, ⊤, Γ ⊤ ⊢ A2, ⊤, Γ & ⊢ A1 & A2, ⊤, Γ π1 ⊢ A1, Γ π2 ⊢ A2, Γ & ⊢ A1 & A2, Γ ⊥ ⊢ A1 & A2, ⊥, Γ C & ⊥ -→ ←- C ⊥ & π1 ⊢ A1, Γ ⊥ ⊢ A1, ⊥, Γ π2 ⊢ A2, Γ ⊥ ⊢ A2, ⊥, Γ & ⊢ A1 & A2, ⊥, Γ ⊤ ⊢ A1 ⊕ A2, ⊤, Γ C ⊕ i ⊤ -→ ←- C ⊤ ⊕ i ⊤ ⊢ Ai, ⊤, Γ ⊕i ⊢ A1 ⊕ A2, ⊤, Γ π ⊢ Ai, Γ ⊕i ⊢ A1 ⊕ A2, Γ ⊥ ⊢ A1 ⊕ A2, ⊥, Γ C ⊕ i ⊥ -→ ←- C ⊥ ⊕ i π ⊢ Ai, Γ ⊥ ⊢ Ai, ⊥, Γ ⊕i ⊢ A1 ⊕ A2, ⊥, Γ ⊤0 ⊢ ⊤0, ⊤1, Γ C ⊤ ⊤ -→ ⊤1 ⊢ ⊤0, ⊤1, Γ π ⊢ Γ ⊥0 ⊢ ⊥0, Γ ⊥1 ⊢ ⊥0, ⊥1, Γ C ⊥ ⊥ -→ π ⊢ Γ ⊥1 ⊢ ⊥1, Γ ⊥0 ⊢ ⊥0, ⊥1, Γ ⊤ ⊢ ⊤, ⊥, Γ C ⊥ ⊤ -→ ←- C ⊤ ⊥ ⊤ ⊢ ⊤, Γ ⊥ ⊢ ⊤, ⊥, Γ
(No commutation with ax, 1 nor 0 as the ax and 1-rules have no context and there are no rule for 0.) ▶ Lemma 44. Let π, ϖ and ϕ be MALL proofs such that 12 for diagrams corresponding to these cases.) Proof. Call r the ax-rule that π η -→ ϕ expands, and A its formula. If the cut-elimination step is not an ax key case using r, then the two steps commute and there exists φ such that ϕ

π ϕ ϖ η β φ β η * = π ϕ ϖ η β φ 1 φ 2 η * β * η * < π ϕ ϖ ENF β * η * φ ENF η * β *
ϖ β ←-π η -→ ϕ. Then there exists φ such that ϖ η * -→ φ β ←-ϕ or there exist φ 1 and φ 2 such that ϕ η * -→ φ 1 β * -→ φ 2 η * ←-ϖ. Furthermore, a(ϕ β -→ φ) = a(π β -→ ϖ) in the first case and a(φ 1 β * -→ φ 2 ) < a(π β -→ ϖ) in the second one. (See Figure
⊢ A1, A2, B1, B2, Γ ⊢ A1 `A2, B1, B2, Γ ⊢ A1 `A2, B1 `B2, Γ C - → π ⊢ A1, A2, B1, B2, Γ ⊢ A1, A2, B1 `B2, Γ ⊢ A1 `A2, B1 `B2, Γ π1 ⊢ A1, Γ π2 ⊢ A2, B1, ∆ π3 ⊢ B2, Σ ⊗ ⊢ A2, B1 ⊗ B2, ∆, Σ ⊗ ⊢ A1 ⊗ A2, B1 ⊗ B2, Γ, ∆, Σ C ⊗ ⊗ -→ π1 ⊢ A1, Γ π2 ⊢ A2, B1, ∆ ⊗ ⊢ A1 ⊗ A2, B1, Γ, ∆ π3 ⊢ B2, Σ ⊗ ⊢ A1 ⊗ A2, B1 ⊗ B2, Γ, ∆, Σ π1 ⊢ A1, Γ π2 ⊢ B1, ∆ π3 ⊢ A2, B2, Σ ⊗ ⊢ A2, B1 ⊗ B2, ∆, Σ ⊗ ⊢ A1 ⊗ A2, B1 ⊗ B2, Γ, ∆, Σ C ⊗ ⊗ -→ π1 ⊢ A1, Γ π3 ⊢ A2, B2, Σ ⊗ ⊢ A1 ⊗ A2, B2, Γ, Σ π2 ⊢ B1, ∆ ⊗ ⊢ A1 ⊗ A2, B1 ⊗ B2, Γ, ∆, Σ π1 ⊢ A1, B1, Γ π2 ⊢ B2, ∆ ⊗ ⊢ A1, B1 ⊗ B2, Γ, ∆ π3 ⊢ A2, Σ ⊗ ⊢ A1 ⊗ A2, B1 ⊗ B2, Γ, ∆, Σ C ⊗ ⊗ -→ π1 ⊢ A1, B1, Γ π3 ⊢ A2, Σ ⊗ ⊢ A1 ⊗ A2, B1, Γ, Σ π2 ⊢ B2, ∆ ⊗ ⊢ A1 ⊗ A2, B1 ⊗ B2, Γ, ∆, Σ π1 ⊢ B1, Γ π2 ⊢ A1, B2, ∆ ⊗ ⊢ A1, B1 ⊗ B2, Γ, ∆ π3 ⊢ A2, Σ ⊗ ⊢ A1 ⊗ A2, B1 ⊗ B2, Γ, ∆, Σ C ⊗ ⊗ -→ π1 ⊢ B1, Γ π2 ⊢ A1, B2, ∆ π3 ⊢ A2, Σ ⊗ ⊢ A1 ⊗ A2, B2, ∆, Σ ⊗ ⊢ A1 ⊗ A2, B1 ⊗ B2, Γ, ∆, Σ π1 ⊢ A1, B1, Γ π2 ⊢ A2, B1, Γ & ⊢ A1 & A2, B1, Γ π3 ⊢ A1, B2, Γ π4 ⊢ A2, B2, Γ & ⊢ A1 & A2, B2, Γ & ⊢ A1 & A2, B1 & B2, Γ C & & -→ π1 ⊢ A1, B1, Γ π3 ⊢ A1, B2, Γ & ⊢ A1, B1 & B2, Γ π2 ⊢ A2, B1, Γ π4 ⊢ A2, B2, Γ & ⊢ A2, B1 & B2, Γ & ⊢ A1 & A2, B1 & B2, Γ π ⊢ Ai, Bj, Γ ⊕i ⊢ A1 ⊕ A2, Bj, Γ ⊕j ⊢ A1 ⊕ A2, B1 ⊕ B2, Γ C ⊕ i ⊕ j -→ π ⊢ Ai, Bj, Γ ⊕j ⊢ Ai, B1 ⊕ B2, Γ ⊕i ⊢ A1 ⊕ A2, B1 ⊕ B2, Γ π1 ⊢ A1, A2, B1, Γ ⊢ A1 `A2, B1, Γ π2 ⊢ B2, ∆ ⊗ ⊢ A1 `A2, B1 ⊗ B2, Γ, ∆ C ⊗ -→ ←- C ⊗ `π1 ⊢ A1, A2, B1, Γ π2 ⊢ B2, ∆ ⊗ ⊢ A1, A2, B1 ⊗ B2, Γ, ∆ ⊢ A1 `A2, B1 ⊗ B2, Γ, ∆ π1 ⊢ B1, Γ π2 ⊢ A1, A2, B2, ∆ ⊢ A1 `A2, B2, ∆ ⊗ ⊢ A1 `A2, B1 ⊗ B2, Γ, ∆ C ⊗ -→ ←- C ⊗ `π1 ⊢ B1, Γ π2 ⊢ A1, A2, B2, ∆ ⊗ ⊢ A1, A2, B1 ⊗ B2, Γ, ∆ ⊢ A1 `A2, B1 ⊗ B2, Γ, ∆ π1 ⊢ A1, A2, B1, Γ ⊢ A1 `A2, B1, Γ π1 ⊢ A1, A2, B2, Γ ⊢ A1 `A2, B2, Γ & ⊢ A1 `A2, B1 & B2, Γ C & -→ ←- C & `π1 ⊢ A1, A2, B1, Γ π1 ⊢ A1, A2, B2, Γ & ⊢ A1, A2, B1 & B2, Γ ⊢ A1 `A2, B1 & B2, Γ π1 ⊢ A1, A2, Bi, Γ ⊢ A1 `A2, Bi, Γ ⊕i ⊢ A1 `A2, B1 ⊕ B2, Γ C ⊕i -→ ←- C ⊕ i `π1 ⊢ A1, A2, Bi, Γ ⊕i ⊢ A1, A2, B1 ⊕ B2, Γ ⊢ A1 `A2, B1 ⊕ B2, Γ π1 ⊢ A1, Γ π2 ⊢ A2, B1, ∆ ⊗ ⊢ A1 ⊗ A2, B1, Γ, ∆ π1 ⊢ A1, Γ π3 ⊢ A2, B2, ∆ ⊗ ⊢ A1 ⊗ A2, B2, Γ, ∆ & ⊢ A1 ⊗ A2, B1 & B2, Γ, ∆ C ⊗ & -→ ←- C & ⊗ π1 ⊢ A1, Γ π2 ⊢ A2, B1, ∆ π3 ⊢ A2, B2, ∆ & ⊢ A2, B1 & B2, ∆ ⊗ ⊢ A1 ⊗ A2, B1 & B2, Γ, ∆ π1 ⊢ A1, B1, Γ π2 ⊢ A2, ∆ ⊗ ⊢ A1 ⊗ A2, B1, Γ, ∆ π3 ⊢ A1, B2, Γ π2 ⊢ A2, ∆ ⊗ ⊢ A1 ⊗ A2, B2, Γ, ∆ & ⊢ A1 ⊗ A2, B1 & B2, Γ, ∆ C ⊗ & -→ ←- C & ⊗ π1 ⊢ A1, B1, Γ π3 ⊢ A1, B2, Γ & ⊢ A1, B1 & B2, Γ π2 ⊢ A2, ∆ ⊗ ⊢ A1 ⊗ A2, B1 & B2, Γ, ∆ π1 ⊢ A1, Bi, Γ π2 ⊢ A2, ∆ ⊗ ⊢ A1 ⊗ A2, Bi, Γ, ∆ ⊕i ⊢ A1 ⊗ A2, B1 ⊕ B2, Γ, ∆ C ⊗ ⊕ i -→ ←- C ⊕ i ⊗ π1 ⊢ A1, Bi, Γ ⊕i ⊢ A1, B1 ⊕ B2, Γ π2 ⊢ A2, ∆ ⊗ ⊢ A1 ⊗ A2, B1 ⊕ B2, Γ, ∆ π1 ⊢ A1, Γ π2 ⊢ A2, Bi, ∆ ⊗ ⊢ A1 ⊗ A2, Bi, Γ, ∆ ⊕i ⊢ A1 ⊗ A2, B1 ⊕ B2, Γ, ∆ C ⊗ ⊕ i -→ ←- C ⊕ i ⊗ π1 ⊢ A1, Bi, Γ π2 ⊢ A2, ∆ ⊕i ⊢ A2, B1 ⊕ B2, ∆ ⊗ ⊢ A1 ⊗ A2, B1 ⊕ B2, Γ, ∆ π1 ⊢ A1, Bi, Γ π2 ⊢ A2, Bi, Γ & ⊢ A1 & A2, Bi, Γ ⊕i ⊢ A1 & A2, B1 ⊕ B2, Γ C & ⊕ i -→ ←- C ⊕ i & π1 ⊢ A1, Bi, Γ ⊕i ⊢ A1, B1 ⊕ B2, Γ π2 ⊢ A2, Bi, Γ ⊕i ⊢ A2, B1 ⊕ B2, Γ & ⊢ A1 & A2, B1 ⊕ B2, Γ
(No commutation with ax, 1 nor 0 as the ax and 1-rule have no context and there are no rule for 0.)

Table 7 Rule commutations not involving a unit rule

Otherwise, the cut-elimination step is an ax key case on r, with a cut-rule we call c and a sub-proof ρ in the other branch of c that the one leading to r. Starting from ϕ, consider the rules introducing A ⊥ in (all slices of) ρ. If any of them are ax-rules, then these are necessarily on the formula A; expand those ax-rules, in both ϕ and ϖ (keep the same name for proofs π, ϖ and ρ by abuse). Then, in ϕ, commute the cut-rule c with rules of ρ until reaching the rules introducing A ⊥ in all slices (which are rules of the main connective of A or ⊤-rules). Applying the corresponding key cases or ⊤ -cut commutative case (first commuting with a rule of the expanded axiom r if A is a positive formula), then the ax key cases on strict sub-formulas of A yields ϖ. During these ax key cases, we cut on sub-formulas of A, so on formulas of a strictly smaller size. Therefore Consider the case n + 1 and m + 1. Therefore, ϖ

ϕ η * -→ • β * -→ • η * ←-ϖ, with a(• β * -→ •) < a(π β -→ ϖ). ◀ ▶ Remark. Cut-elimination β -→
η m ←-ι η ←-π β -→ κ β n -→ ϕ. We apply Lemma 44 on ι η ←-π β -→ κ, yielding φ such that ι β -→ φ η * ←-ϕ with a(ι β -→ φ) = a(π β -→ κ) or φ 1 and φ 2 such that ι η * -→ φ 1 β * -→ φ 2 η * ←-κ with a(φ 1 β * -→ φ 2 ) < a(π β -→ κ).
Both of these cases, and the reasonings we will apply, are illustrated on the diagrams of Figure 13.

Assume to be in the first case. Applying the induction hypothesis on ϖ

η m ←-ι β -→ φ, with ϖ in η-normal form, a(ι β -→ φ) = a(π β -→ κ) ≤ a(π β * -→ ϕ), 1 ≤ n +
β * ←-η(ϕ) = β η(ϖ). Finally, if π η -→ ϕ or π η ←-ϕ, then η(π) = η(φ) = β η(ϖ) and the conclusion follows. ◀ π ι ϖ ENF κ ϕ η η m β β n φ = η * β IH ν ENF β * η * IH µ ENF β * η * π ι ϖ ENF κ ϕ η η m β β n φ 1 φ 2 < η * β * η * η * IH ν ENF β * η * IH µ ENF β * η *

C Proofs for the completeness for unit-free MALL

This appendix contains proofs of results stated in Section 3 and leading to the proof of completeness for unit-free MALL. All the sequent calculus proofs we consider in this section have expanded axioms.

C.1 Proof of the Simulation Theorem (Theorem 12)

▶ Definition 46 (◁). Let θ and ϑ be MALL proof-nets. We denote θ ◁ ϑ if there exists a * -vertex C in θ such that the syntax forest of ϑ is the syntax forest of θ where the syntax tree of C is duplicated into the syntax trees of C 0 and C 1 (which are different occurrences of C), θ = θ 0 ⊔ θ 1 6 and ϑ = ϑ 0 ⊔ ϑ 1 , with ϑ i = θ i up to assimilating C i with C (for i ∈ {0; 1}).

▶ Lemma 47 (Simulationβ). Let π and ϖ be unit-free MALL proof trees such that π

β -→ ϖ. We have R(π) = R(ϖ), R(π) β -→ R(ϖ) or R(π) ◁ R(ϖ).
Proof. We reason by cases according to the step π β -→ ϖ. Recall that we desequentialize by separating all cuts, and use the notations for steps from Definition 7. If π β -→ ϖ is an ax (resp. `-⊗, & -⊕) key case, then using a step (a) (resp. (b), (c)), R(π) We reason by induction on the size of the formula A of C (and also C 0 and C 1 ); w.l.o.g. A is positive. Applying a step of cut-elimination on C in θ yields a proof-net Θ. On the other hand, a step of cut-elimination on C 0 and C 1 in θ ′ yields Θ ′ . If A is an atom, then we applied step (a), and we find Θ = Θ ′ .

β -→ R(ϖ). If it is a `-cut, ⊗ -cut -1, ⊗ -cut -2, ⊕ 1 -cut or ⊕ 2 -cut commutative case, then R(π) = R(ϖ).
If A is a ⊗-formula, i.e. A = A 0 ⊗ A 1 , then we applied step (b) and produced cuts A 0 * A ⊥ 0 and A 1 * A ⊥ 1 in Θ, and two occurrences of these cuts in Θ ′ . Thus, Θ ◁ Ξ ◁ Θ ′ with Ξ the 6 The symbol ⊔ means a union ∪ which happens to be between disjoint sets.

proof-net Θ where the cut on A 0 is duplicated. By induction hypothesis, Θ

= β Ξ = β Θ ′ . It follows θ = β θ ′ as θ β -→ Θ = β Θ ′ β ←-• β ←-θ ′ . Finally, if A is a ⊕-formula with A = A 0 ⊕ A 1 ,
then we used step (c), producing cuts A 0 * A ⊥ 0 and A 1 * A ⊥ 1 in Θ, and two occurrences of these cuts in Θ ′ . Remark that inconsistent linkings in θ ′ for these steps are exactly those of θ, and therefore the same cuts are garbage collected. Whence, Θ ◁ • ◁ Θ ′ , Θ ◁ Θ ′ or Θ = Θ ′ (according to the number of cuts garbage collected). In all cases, using the induction hypothesis we conclude θ = β θ ′ . ◀ ▶ Remark. Another proof of Lemma 48, using the Turbo Cut-elimination procedure and no induction, is possible. We use the Turbo Cut-elimination procedure on C in θ, yielding a proof-net Θ; we also use it in

θ ′ on C 0 then C 1 , yielding Θ ′ . Whence, θ β * -→ Θ and Θ ′ β * ←-θ ′ .
It stays to prove that Θ = Θ ′ . Remark that Θ and Θ ′ can only differ by their linkings, for they have the same syntax forest. Notice that a linking in θ i , i ∈ {0; 1}, matches for C in θ if and only if it matches for C i in θ ′ (because this linking uses C i as C). Thence, the same linkings stay in Θ and Θ ′ , and Θ = Θ ′ follows.

▶ Theorem 12 (Simulation Theorem). Let π and ϖ be unit-free MALL proof trees (with expanded axioms).

If π = β ϖ, then R(π) = β R(ϖ).
Proof. This is a corollary of Lemmas 47 and 48. ◀

C.2 Proof of the Reduction to proof-net Theorem (Theorem 13)

We call B(θ) the β-normal form of the proof-net θ, with all cuts eliminated.

R(id A ) is cut-free, B(B(R(π)) B ▷◁ B(R(ϖ))) = B(R(id A )) = R(id A ). Similarly, B(B(R(ϖ)) A ▷◁ B(R(π))) = R(id B
). Thus, there exist cut-free proof-nets θ := B(R(π)) and ϑ := B(R(ϖ)) whose composition over B (resp. A) yields after cut-elimination the identity proof-net of A (resp. B). ◀

C.3 Proofs of the properties of identity proof-nets from Proposition 15

We prove each result separately.

▶ Lemma 50. The axiom links of an identity proof-net are exactly the (l, l ⊥ ), for any leaf l.

Proof. By induction on the formula (see Figure 3 on Page 8). ◀ ▶ Corollary 51. An identity proof-net is bipartite ax-unique.

Proof. This follows from Lemma 50. ◀ ▶ Lemma 52. Let λ be a linking of an identity proof-net and V an additive vertex in its additive resolution. Then V ⊥ is also inside with, as premise kept, the dual premise of the one kept for V .

Proof. Assume w.l.o.g. that the left premise of V is kept in λ. There is a left-ancestor l of V in the additive resolution of λ, hence with a link a ∈ λ on it. By Lemma 50, a = (l, l ⊥ ). As l ⊥ is a right-ancestor of V ⊥ , the conclusion follows. ◀ ▶ Lemma 53. In the identity proof-net of A, exactly one linking is on any given additive resolution of the conclusion A.

Proof. Consider such an additive resolution R. There is an associated &-resolution R ′ of A ⊥ , A by taking the choices of premise of R on A and, for a &-vertex W of A ⊥ , taking the dual premise chosen in R for W ⊥ . By Lemma 52, a linking λ is on R if and only if it is on R ′ . Meanwhile, by (P1) there is a unique linking λ on R ′ ; thus the same holds on R. ◀

C.4 Proof of Lemma 18

▶ Lemma 18. Assume θ and θ ′ are cut-free proof-nets of respective conclusions A ⊥ , B and B ⊥ , A, and that their composition over B yields the identity proof-net of A. Then any leaf of A ⊥ (resp. A) has (at least) one axiom link on it in θ (resp. θ ′ ).

Proof. Towards a contradiction, assume w.l.o.g. a leaf l of A ⊥ has no link on it in θ. Then, the composition over B of θ and θ ′ has no link on l either. And reducing cuts cannot create links using l, for it only takes links (l, m) and (m, n) to merge them into (l, m). However, the identity proof-net of A is ax-unique by Proposition 15(i), thence full: contradiction. ◀

C.5 Proof of Proposition 21

▶ Proposition 21. If E is complete for isomorphisms between distributed formulas, then it is complete for isomorphisms between arbitrary formulas.

Proof. The following rewriting system is strongly normalizing, with as normal forms distributed formulas, and each rule corresponds to a valid equality in the theory E (see Table 1):

A ⊗ (B ⊕ C) → (A ⊗ B) ⊕ (A ⊗ C) (C & B) `A → (C `A) & (B `A) (A ⊕ B) ⊗ C → (A ⊗ C) ⊕ (B ⊗ C) C `(B & A) → (C `B) & (C `A) A ⊗ 1 → A 1 ⊗ A → A A `⊥ → A ⊥ `A → A A ⊕ 0 → A 0 ⊕ A → A A & ⊤ → A ⊤ & A → A A ⊗ 0 → 0 0 ⊗ A → 0 A `⊤ → ⊤ ⊤ `A → ⊤
Consider an isomorphism A ≃ B between two arbitrary formulas A and B. Let A d and B d be associated distributed formulas, obtained as normal forms of the above rewriting system. As this rewriting system is included in E, we have

A = E A d and B = E B d .
By soundness of E (Theorem 3) and as linear isomorphism is a congruence, we deduce

A d ≃ A ≃ B ≃ B d .
= λ W for some λ W ∈ Λ W .
Let us now prove our lemma. Take Λ a minimal saturated subset of θ with G Λ containing ω. Since Λ is minimal, ω ̸ ⊆ G Λ W (using (S1)), so some edge e of ω is in G Λ but not in G Λ W . We claim that, without loss of generality, e is an axiom link. If it is indeed the case, then e ∈ λ ∈ Λ and e / ∈ λ W for e / ∈ Λ W , so e depends on W in Λ (using (S2)). We now prove our claim by eliminating other possibilities step by step.

Without loss of generality, e is an edge from a leaf l to some X, because for any other edge Y → X in ω we have

l → Z 1 → • • • → Z n = Y → X in ω for some leaf l, and Y → X is in G Λ W whenever l → Z 1 is in G Λ W .
Still without loss of generality, e is not an edge in a syntax tree. Indeed, in such a case e / ∈ G Λ W implies l / ∈ G Λ W . As e belongs to the switching cycle ω, let us look at the other edge in this cycle with endpoint l, say e ′ . As l / ∈ G Λ W , we also have e ′ / ∈ G Λ W . Remark that e ′ cannot be an edge in a syntax tree, for only one such edge has for endpoint the leaf l, namely e. We can replace e with e ′ to assume e is not an edge in a syntax tree.

As ω is jump-free, e cannot be a jump edge. The sole possibility is e being a link. ◀

C.7 Proof of Lemma 26

▶ Lemma 26. Let λ be a linking of ϑ, and V an additive vertex in its additive resolution. Then V ⊥ is also inside, with as premise kept the dual premise of the one kept for V .

Proof. Assume w.l.o.g. that the left premise of V is kept in λ. There is a left-ancestor l of V in the additive resolution of λ, hence with a link a ∈ λ on it. By Lemma 25, we have a ⊥ ∈ λ, using l ⊥ . As l ⊥ is a right-ancestor of V ⊥ , the conclusion follows. ◀

C.8 Proof of Corollary 31

This proof follows very closely the one for MLL of Balat & Di Cosmo (Section 3 in [START_REF] Balat | A linear logical view of linear type isomorphisms[END_REF]).

In the following, we will call substitution the usual operation [A 1 /X 1 , . . . , A n /X n ] of replacement of the propositional atoms X i of a formula by the formulas A i . We will consider substitutions extended to proof-nets, i.e. if σ is a substitution and θ a proof-net, σ(θ) will be the proof-net obtained from θ by replacing all formulas F j appearing in it by σ(F j ). We will also use a more general notion, renaming, that may replace different occurrences of the same atom by different formulas in a proof-net, i.e. substitute on leaves instead of atoms.

▶ Definition 54 (Renaming). An application α from the set of leaves of a proof-net θ to a set of atoms is a renaming if α(θ), the graph obtained by substitution of each label of a leaf l of θ by α(l), is a proof-net.

Remark that if θ is bipartite ax-unique, then the definition of α only on leaves in one conclusion of θ is sufficient to define a renaming α on θ. This is because every leaf of the other conclusion is linked to exactly one leaf in this conclusion, and no leaves in a given conclusion are linked together. Note also that if the conclusions of θ are ambiguous formulas, then two different occurrences of the same atom can be renamed differently, unlike what happens in the case of substitutions.

▶ Theorem 55 (Renaming preserves isomorphisms). For A and B distributed formulas, assume A θ, θ ′ ≃ B, with θ and θ ′ proof-nets of respective conclusions A ⊥ , B and B ⊥ , A. If α is a renaming of the leaves of θ, then there exists α ′ , a renaming of the leaves of θ ′ , such that α ′ (A)

α(θ), α ′ (θ ′ ) ≃ α(B); more precisely: α ′ (θ ′ ) is a proof-net α(A ⊥ ) = α ′ (A) ⊥ and α ′ (B ⊥ ) = α(B) ⊥ the composition of α(θ) and α ′ (θ ′ ) by cut over α(B) (resp. α ′ (A)) gives the identity proof-net of α ′ (A) (resp. α(B)).
Proof. We first define α ′ . By Theorem 29, θ ′ is bipartite ax-unique, so it is sufficient to define α ′ only on the occurrences of B ⊥ , i.e. to define α ′ (B ⊥ ). We set α ′ (B ⊥ ) = α(B) ⊥ . Then the composition of α(θ) and α ′ (θ ′ ) by cut over α(B) is a proof-net. Since cut-elimination does not depend on labels, this composition reduces to an identity proof-net with conclusions α(A ⊥ ), α ′ (A). An induction, on the number of connectives of α(A), shows that this is the identity proof-net of α(A ⊥ ). Thus α(A ⊥ ) = α ′ (A) ⊥ . But then, the composition of α ′ (θ ′ ) and α(θ) by cut over α ′ (A) is a proof-net, that reduces to an identity net (since cut-elimination does not depend on labels), that is the identity proof-net of α(B). Hence, α ′ (A) Proof. The proof-nets θ and θ ′ are bipartite ax-unique (Theorem 29), with conclusions B ⊥ , A and A ⊥ , B respectively. One can define a renaming α such that α(A) has distinct atoms (i.e. no atom of α(A) occurs twice in α(A), even one positively and one negatively), for it is sufficient to define α only on leaves of A. In particular, α(A) is non-ambiguous.

α(θ), α ′ (θ ′ ) ≃ α(B).
Then, Theorem 55 gives an algorithm for defining a renaming α ′ such that α ′ (A)

α(θ), α ′ (θ ′ ) ≃ α(B), with in particular α ′ (A ⊥ ) = α(A) ⊥ and α(B ⊥ ) = α ′ (B) ⊥ . Pose A ′ := α ′ (A) and B ′ := α(B), hence A ′ α(θ), α ′ (θ ′ )
≃ B ′ and α(θ) has for conclusions B ′ ⊥ , A ′ . Formulas A ′ and B ′ are distributed, as renaming acts only on leaves.

On α(θ) one can define a renaming α -1 such that α -1 (A ′ ) = A, hence α -1 (B ′ ⊥ ) = B ⊥ . Since α(θ) is bipartite ax-unique, it is equivalent to define α -1 on α(θ) or only on leaves of A ′ . Because all atoms of A ′ are distinct, two distinct leaves of A ′ correspond to distinct atoms of A ′ . One can then define a substitution σ on atoms of A ′ by σ(X) = α -1 (l(X)), with l(X) the unique leaf of A ′ with label X. Thus, Conversely, let A ′ and B ′ be distributed non-ambiguous formulas such that A ′ θ ′ , ϑ ′ ≃ B ′ , and σ a substitution on atoms of A ′ (so also on atoms of B ′ ). Let θ ′ and ϑ ′ are bipartite ax-unique proof-nets (Theorem 29). The substitution σ defines on θ ′ a renaming α (any substitution can be seen as a renaming). Let α ′ be the renaming defined on ϑ ′ , associated to α in Theorem 55. Since Proof. Let a be an axiom link of θ. By bipartiteness, it uses a leaf l of A and a leaf m of A ⊥ . Denote by X the label of l, whence the label of m is X ⊥ . However, the only leaf of A ⊥ with label X ⊥ is l ⊥ , because A ⊥ is non-ambiguous. Thus, m = l ⊥ and a = (l, l ⊥ ). ◀ ▶ Lemma 59. Let θ be a bipartite proof-net of conclusions A ⊥ , A, with A a non-ambiguous formula. Take a linking λ ∈ θ and an additive vertex V in its additive resolution. The vertex V ⊥ is in the additive resolution of λ, and λ keeps for V ⊥ the dual premise it keeps for V .

θ = α -1 (α(θ)) = σ(α(θ)): in particular, σ(A ′ ) = A and σ(B ′ ⊥ ) = B ⊥ , so σ(B ′ ) = B. Finally, A ′ and B ′ are distributed non-ambiguous formulas such that A ′ α(θ), α ′ (θ ′ ) ≃ B ′ , A = σ(A ′ ) and B = σ(B ′ ). ◀ ▶ Corollary
σ(A ′ ⊥ ) = α(A ′ ⊥ ) = (α ′ (A ′ )) ⊥ , α ′ is also the renaming induced by σ on ϑ ′ . As α ′ (A ′ ) α(θ ′ ), α ′ (ϑ ′ ) ≃ α(B ′ ) by Theorem 55, it follows σ ′ (A ′ ) α(θ ′ ), α ′ (ϑ ′ ) ≃ σ(B ′ ). ◀ C.
Proof. As V is in the additive resolution (A ⊥ , A) ↾ λ of λ, one of its ancestor leaves, say l, is in (A ⊥ , A) ↾ λ: there is a link a ∈ λ on it. By Lemma 58, a = (l, l ⊥ ). But l ⊥ is an ancestor of V ⊥ , so V ⊥ is in (A ⊥ , A) ↾ λ, with as premise the dual premise chosen for V . ◀ ▶ Lemma 60. Let A be a non-ambiguous formula, θ and θ ′ bipartite proof-nets of conclusions A ⊥ , A. Then θ = θ ′ .

Proof. Take λ ∈ θ a linking. It is on some &-resolution R of A ⊥ , A. By (P1), there exists a unique linking λ ′ ∈ θ ′ on R. We have to prove λ = λ ′ . They have the same additive resolution, for their choice on a ⊕-vertex P is determined by the premise taken for the &-vertex P ⊥ , which is in R (Lemma 59). They have the same axiom links on this additive resolution, because any leaf on it is linked to its dual (Lemma 58). Therefore, λ = λ ′ , so θ ⊆ θ ′ . By symmetry, the same reasoning yields θ ′ ⊆ θ, thus θ = θ ′ . ◀ ▶ Corollary 61. Let A be a non-ambiguous formula. There is exactly one bipartite proof-net of conclusions A ⊥ , A: the identity proof-net of A.

Proof. This follows from Proposition 15(i) and Lemma 60. ◀ It is easy to check that removing a sequentializing vertex produces proof-net(s). The sequentialization theorem affirms there exists a sequentializing vertex in a proof-net.

Type Isomorphisms for Multiplicative-Additive Linear Logic

A l A r ⊚ B T (A l ) T (A r ) T (B) l r
▶ Lemma 64. In a bipartite full proof-net with conclusions A l ⊚ A r , B, where ⊚ ∈ {⊗; ⊕}, the root of A l ⊚ A r is not sequentializing.

Proof. Let l be a leaf of A l and r one of A r . By bipartiteness and fullness, there are leaves m and s of B with axiom links (l, m) and (r, s) in the proof-net (see Figure 14). As there is a path in T (B) between m and s, whether ⊚ = ⊕ or ⊚ = ⊗, it is not sequentializing. Proof. We remove all terminal (hence sequentializing) `-vertices, all in A, without modifying the linkings. The resulting graph is a proof-net of conclusions A 1 , . . . , A n , B l ⊙ B r (see Figure 15). The roots of the new trees A i cannot be &-vertices because A is distributed: so they are ⊗\⊕-vertices or atoms. These ⊗\⊕-vertices are not sequentializing, since by bipartiteness and fullness every leaf of each A i is connected to the formula B l ⊙ B r (reasoning Proof. By Theorem 13, there exist proof-nets θ and ϑ such that A θ, ϑ ≃ B. We prove the following stronger result: if A θ, ϑ ≃ B for some proof-nets θ and ϑ, then A = E † B. We assume A and B to be distributed and non-ambiguous formulas by Proposition 21 and Corollary 31. We reason by induction on the size of A, s(A). 7 If A and B are atoms (i.e. of null size), then A = B and the property holds. Otherwise, A ⊥ and B are both non atomic. By Theorem 29, θ and ϑ are bipartite ax-unique; they have respective conclusions A ⊥ , B and B ⊥ , A. By Lemma 64, one of the formulas A ⊥ , B is negative, otherwise neither the root of A ⊥ nor B is sequentializing in θ, contradicting sequentialization (Theorem 10). A symmetric reasoning on ϑ implies that the other formula is positive. Assume w.l.o.g. that B = B 0 ⊙ B 1 is positive (i.e. ⊙ ∈ {⊗; ⊕}) and A ⊥ negative. We distinguish cases according to the kind of the roots of A ⊥ and B, considering the proof-net θ. If B a ⊗-formula and A a &-formula, we instead consider ϑ of conclusions B ⊥ , A, where A is a ⊕-formula and B ⊥ a `-formula. Whence, either A ⊥ is a `-formula, or B and A ⊥ are respectively a ⊕-formula and a &-formula.

In the first (resp. second) case, by Lemma 65 (resp. Lemma 66) ⊙ = ⊗ (in the first case only) and there exist two bipartite ax-unique proof-nets θ 0 and θ 1 of respective conclusions

A ′ 0 ⊥ , B 0 and A ′ 1 ⊥ , B 1 , with A ′ ⊥ = A ′ 1 ⊥ `A′ 0 ⊥ (resp. A ′ ⊥ = A ′ 1 ⊥ & A ′ 0 ⊥ ) equal to A ⊥ up
to associativity and commutativity of `(resp. &). In particular, A ′ ⊥ = E † A ⊥ , and s(A ′ 0 ) and s(A ′ 1 ) are both less than s(A). To conclude, we only need bipartite proof-nets ϑ 0 and ϑ 1 of respective conclusions B ⊥ 0 , A ′ 0 and B ⊥ 1 , A ′ 1 . We will then apply Corollary 32 to obtain

A ′ 0 θ 0 , ϑ 0 ≃ B 0 and A ′ 1 θ 1 , ϑ 1 ≃ B 1 . Thence, by induction hypothesis, A ′ 0 = E † B 0 and A ′ 1 = E † B 1 , thus A ′ = E † B. 8 As A = E † A ′ , we will finally conclude A = E † B.
Thus, we look for two bipartite proof-nets of respective conclusions

B ⊥ 0 , A ′ 0 and B ⊥ 1 , A ′ 1 . As A θ, ϑ
≃ B, and A ≃ A ′ by soundness of E † (Theorem 3), it follows using Theorem 13 that A ′ Θ, Θ ′ ≃ B for some proof-nets Θ and Θ ′ . 9 Furthermore, Θ is a bipartite ax-unique proof-net (Theorem 29) of conclusions B ⊥ , A ′ , i.e. of conclusions

B ⊥ 1 ⊙ ⊥ B ⊥ 0 , A ′ 0 ⊚ A ′ 1 with (⊙ ⊥ , ⊚) ∈ {(`, ⊗); (&, ⊕)}.
We had a bipartite ax-unique proof-net θ 0 of conclusions A ′ 0 ⊥ , B 0 , therefore the atoms or negated atoms of B 0 are exactly those of A ′ 0 . Similarly, the atoms and negated atoms of B 1 are exactly those of A ′ 1 . Whence, no atom nor negated atom of B 0 (resp. B 1 ) is one of A ′ 1 (resp. A ′ 0 ), for otherwise an atom or negated atom of A 0 (resp. A 1 ) also occurs in A ′ 1 (resp A ′ 0 ), contradicting non-ambiguousness of A ′ . This implies that axiom links in Θ must be between leaves of B ⊥ 0 and A ′ 0 , and between leaves of B ⊥ 1 and A ′ 1 . Therefore, once we sequentialize the negative root ⊙ ⊥ of B ⊥ in Θ, the positive root ⊚ of A ′ is sequentializing. After sequentializing both, we obtain two bipartite ax-unique proof-nets, of respective conclusions B ⊥ 0 , A ′ 0 and B ⊥ 1 , A ′ 1 . ◀

D Proofs for the completeness for full MALL

This appendix contains proofs of results stated in Section 4 and leading to the proof of completeness for full MALL. In all this section, by proof we mean a sequent calculus proof of MALL, we never consider proof-nets. 7 Remark that s(A) = s(B), because θ is bipartite ax-unique (Theorem 29), thence A and B have the same number of atoms, so of connectives as they are all binary ones. 8 The formula A ′ is distributed for it is equal up to associativity and commutativity to the distributed A.

Whence, A ′ 0 and A ′ 1 are also distributed. 9 One can easily check that isomorphisms in proof-nets form equivalence classes on formulas.

D.1 Proof of Theorems 34 and 35

▶ Definition 67. We define the weight w(π) of a proof π by induction:

w ax ⊢ A ⊥ ,A = 1. w   π ⊢ A, Γ ϖ ⊢ A ⊥ , ∆ cut ⊢ Γ, ∆   = w(π) + w(ϖ) w π ⊢ A, Γ ϖ ⊢ B, ∆ ⊗ ⊢ A ⊗ B, Γ, ∆ = w(π) + w(ϖ) + 1 w π ⊢ A, B, Γ ⊢ A `B, Γ = w(π) + 1 w 1 ⊢ 1 = 1 w π ⊢ Γ ⊥ ⊢ ⊥, Γ = w(π) + 1 w π ⊢ A, Γ ϖ ⊢ B, Γ & ⊢ A & B, Γ = max (w(π), w(ϖ)) + 1 w π ⊢ A i , Γ ⊕ i ⊢ A 1 ⊕ A 2 , Γ = w(π) + 1 w ⊤ ⊢ ⊤, Γ = 1 ▶ Definition 68. A block B of cut-rules in a proof π is a maximal set of cut-rules in π
such that all of these rules are a premise of another rule in the set, or use as premise the conclusion of a rule in the set. A block can also be seen as a maximal sub-proof composed of cut-rules only.

We call measure |B| of a block B of cut-rules in a proof π the weight of its root cut-rule, i.e. |B| = i w(π i ) where the π i are the sub-proofs whose conclusions are the premises of the cut-rules of |B|, premises which are not the conclusion of a cut-rule.

The measure |c| of a cut-rule c in a proof π is the measure of the block it belongs to. The measure |π| of a proof π is the multiset of the measures of its cut-rules. ▶ Lemma 70. Cut-elimination not involving the cut -cut commutation in MALL sequent calculus is strongly normalizing. In particular, cut-elimination is weakly normalizing.

▶
Proof. As long as there exists a cut-rule, we can choose to do a β -→ step (for instance by considering a cut-rule with no other cut-rule above it). This strictly decreases the measure of the proof by Lemma 69, ensuring termination.

◀

π 1 π 2 π 3 = c β ϖ 1 ϖ 2 β * = * c β * π t π l π r β β ϖ l ϖ r β * = * c β * π 1 π 2 π 3 ∼ c β ϖ 1 ϖ 2 β β * β *
|ϖ 2 | ≤ max(|ϖ 1 |, |π 3 |) < max(|π 1 |, |π 2 |).
Another general case is when the rules involved in the two steps are distinct, but the β -→ step eliminates a subtree containing the rules of the = c step (this can arise when using a & -⊕ i key case or a ⊤ -cut commutative case). In this case, doing first the

β -→ step directly yields π 3 : π 1 β -→ π 3 , with |π 3 | < |π 1 |. A = c
step cannot erase a sub-proof containing the rules of a β -→ step, for the only possible case for this is a ⊤ -⊗ commutative case, and we assumed in this case that the sub-proof erased (or created) is cut-free.

From now on, we suppose not to be in such situations, meaning both steps involve (at least) one common rule. This rule cannot be a cut one, for there are no commutations involving a cut-rule in = c . We distinguish cases according to the kind of π 2 β -→ π 3 .

If π 2 β

-→ π 3 is an ax key case. As an ax-rule never commutes, the two steps share no rule.

If π 2 β -→ π 3 is a `-⊗ key case. In this case, π 2 and π 3 are the following proofs:

ρ 1 ⊢ A, Γ ρ 2 ⊢ B, ∆ ⊗ ⊢ A ⊗ B, Γ, ∆ ρ 3 ⊢ B ⊥ , A ⊥ , Σ ⊢ B ⊥ `A⊥ , Σ cut ⊢ Γ, ∆, Σ ρ 4 ρ 1 ⊢ A, Γ ρ 2 ⊢ B, ∆ ρ 3 ⊢ B ⊥ , A ⊥ , Σ cut ⊢ A ⊥ , ∆, Σ cut ⊢ Γ, ∆, Σ ρ 4
By our assumption, π 1 = c π 2 was a step pushing down the ⊗ or `-rule, and up some non cut-rule r. We can in π 1 commute the cut-rule up and r down (as r cannot introduce the formula on which we cut). This yields a proof ϖ 1 such that π 1 β -→ ϖ 1 with this commutative step, and ϖ 1 β -→ ϖ 3 using the same step as in π 2 β -→ π 3 , unless r is a ⊤-rule, case we will discuss in a second step, and if r is a &-rule we do it on both occurrences, obtaining

ϖ 1 β -→ ϖ 2 β -→ ϖ 3 . Thus, except if r is a ⊤-rule, we have ϖ 1 β * -→ ϖ 3 .
Then, in ϖ 3 we can commute r up above one or two (according to its original position) of the cut-rules created by this key case, yielding π 3 using one or two

β ←-step. Therefore, π 1 β -→ ϖ 1 β * -→ ϖ 3 β *
←-π 3 . Now, let us consider the case where the other rule r in the = c step is a ⊤-rule, say above the ⊗ formula (the case where it is above the `is similar). The proof π 1 is

⊤ ⊢ A ⊗ B, Γ, ∆ ρ 3 ⊢ B ⊥ , A ⊥ , Σ ⊢ B ⊥ `A⊥ , Σ cut ⊢ Γ, ∆, Σ ρ 4 . First executing a commutative ⊤ -cut β -→
step in π 1 using this rule, we obtain ϖ 1 = ⊤ ⊢ Γ, ∆, Σ ρ 4 . Using one or two ⊤ -cut commutations yields π 3 , by putting the ⊤-rule in the corresponding ρ i it was in π 2 . Whence,

π 1 β -→ ϖ 1 β * ←-π 3 . Similarly, if r is commuted with the `-rule, we obtain π 1 β -→ ϖ 1 β ←-π 3 .
This concludes the study when = c is a commutation with the ⊗ or `-rule.

In both subcases, the result on measures follows by Lemma 69.

If π 2 β -→ π 3 is a & -⊕ i key case.
This case is similar to the previous one, in simpler as we create one new cut-rule and not two. We have π 2 the following proof:

ρ 2 ⊢ A 2 , Γ ρ 1 ⊢ A 1 , Γ & ⊢ A 2 & A 1 , Γ ρ 3 ⊢ A ⊥ i , ∆ ⊕ i ⊢ A ⊥ 1 ⊕ A ⊥ 2 , ∆ cut ⊢ Γ, ∆ ρ 4
and π 3 the next one:

ρ i ⊢ A i , Γ ρ 3 ⊢ A ⊥ i , ∆ cut ⊢ Γ, ∆ ρ 4
The π 1 = c π 2 step was a commutation pushing down the & or ⊕ i -rule, and another non-cut-rule r up. We can first commute r and the cut-rule, yielding π 1 β -→ ϖ 1 . Applying the key case then yields ϖ 1 β -→ ϖ 3 , unless r is a ⊤-rule, case we will discuss in a second step, and if r is a &-rule we can do it on both occurrences, obtaining ϖ 1

β -→ ϖ 2 β -→ ϖ 3 .
Then, in ϖ 3 , we can commute r up above the cut-rule created by this key case, yielding π 3 .

Therefore, π 1

β -→ ϖ 1 β * -→ ϖ 3 β ←-π 3 (if r is not a ⊤-rule)
. Now, let us consider the case where the other rule r in the = c step is a ⊤-rule, above the & or ⊕ formula. First executing a ⊤ -cut commutative step in π 1 using this rule, we

obtain ϖ 1 = ⊤ ⊢ Γ, ∆ ϖ 3
. Then, a ⊤ -cut commutation yields π 3 by putting the ⊤-rule in the corresponding ρ i it was in π 2 . Whence, π 1

β -→ ϖ 1 β ←-π 3 .
In both subcases, the result on measures follows by Lemma 69.

If π 2 β -→ π 3 is a ⊥ -1 key case.
This case is also similar to the `-⊗ key case, in simpler as there are less sub-proofs. We have

π 2 = 1 ⊢ 1 ρ 1 ⊢ Γ ⊥ ⊢ ⊥, Γ cut ⊢ Γ ρ 2 and π 3 = ρ 1 ⊢ Γ ρ 2 .
The 1-rule does not commute, so the π 1 = c π 2 step was a commutation pushing down the ⊥-rule, and another non-cut-rule r up. We can first commute r and the cut-rule, yielding

π 1 β -→ ϖ 1 .
Applying the key case then yields ϖ 1 β -→ π 3 , unless r is a ⊤-rule, case we will discuss in a second step, and if r is a &-rule we can do it on both occurrences, obtaining

ϖ 1 β * -→ π 3 .
Now, let us consider the case where the other rule r in the = c step is a ⊤-rule, above the ⊥ formula. Applying a ⊤ -cut commutative step in π 1 using this rule, we directly obtain

π 3 . Whence, π 1 β -→ π 3 .
In both subcases, the result on measures follows by Lemma 69.

If π 2 β

-→ π 3 is a commutative case. We have π 1 = c π 2 and π 2 β -→ π 3 having exactly one rule in common, for the cut-rule does not belong to the commutations in = c and a commutative cut-elimination case involves two rules. Thus, the = c step involves the rule r that will be commuted down in the β -→ step, and call s the other rule involved in = c . These rules r and s are not cut-rules. The proof π 1 has from top to bottom r, s and cut, π 2 has s, r and cut, and π 3 has s, cut and r. Assume for the moment neither r nor s is a ⊤-rule.

If the cut-rule commutes with s, we first commute s -cut then r -cut, yielding π 1

β -→ ϖ 1 β * -→ ϖ 3 (the β *
-→ being of length one, except if s is a &-rule, in which case we need to do the r -cut commutation for both occurrences). The proof ϖ 3 has from top to bottom cut, r and s. We then commute r with s and then s with cut (twice if r is a &-rule), yielding

ϖ 3 = c ϖ 4 β * ←-π 3 .
The result on measures is a consequence of Lemma 69. Otherwise, s is a rule introducing the formula on which we cut. We first reduce in the same way all cut-rules in the branch of the cut-rule not containing s, yielding ϖ 1 from π 1 through π 1 -→ ϖ 6 , with ϖ 6 differing from ϖ 2 by having r below ρ and not above s. Schematically we have:

π 1 = ρ 1 r x s x ρ 2 cut ρ 3 ; ϖ 1 = ρ 1 r x s x ρ ′ 2 s ⊥ ρ cut ρ 3 ; ϖ 2 = ρ 1 r x s x ρ ′ 2 s ⊥ x cut ρ ρ 3 π 2 = ρ 1 s x r x ρ 2 cut ρ 3 π 3 = ρ 1 s ρ 2 cut x r ρ 3 ; ϖ 7 = ρ 1 s x ρ ′ 2 s ⊥ ρ cut x r ρ 3 ; ϖ 6 = ρ 1 s x ρ ′ 2 s ⊥ x cut ρ r ρ 3
Using the appropriate key case or ⊤ -cut commutative case to eliminate the cut-rule in ϖ 2 , we obtain a new proof ϖ 3 (as usual, if there are &-rules in ρ, we need to do so for all duplicates). In this new proof, if any cut-rules have been introduced by the key case we used, we can commute them with the rule r (which cannot introduce the formula of the cut, for this is a sub-formula of the s rule, which commutes with the r rule). The produced proof is called ϖ 4 , and we have ϖ

2 β * -→ ϖ 3 β * -→ ϖ 4 .
On the other hand, we can also eliminate the cut-rule in the same way in ϖ 6 , yielding a proof ϖ 5 such that ϖ 6 β * -→ ϖ 5 . We have ϖ 5 being ϖ 4 , except the rule r is below the rules of ρ in ϖ 5 and above in ϖ 4 . We can commute this rule r up from ϖ 5 to ϖ 4 , and it never commutes with a ⊤-rule there for we commute it until reaching the cut-rule and a ⊤-rule is 0-ary, and neither does it commutes with a cut-rule as

ρ is cut-free. This yields π 1 β * -→ ϖ 1 β * -→ ϖ 2 β * -→ ϖ 3 β * -→ ϖ 4 = * c ϖ 5 β * ←-ϖ 6 β * ←-ϖ 7 β * ←-π 3 .
The result on measure follows by Lemmas 69 and 71.

Assume now r is a ⊤-rule while s is not. Then π 1 = c π 2 consists in erasing the rule s, and π 2 β -→ π 3 erases the cut-rule. As before, if s and the cut commute, then we commute them and do the ⊤ -cut case, before commuting r and s: this yields π 1

β -→ • β -→ • = c π 3
, and the measures are as wished by Lemma 69. Otherwise, we proceed similarly as in the previous subcase. Using the same notations, we build as before ϖ 1 and ϖ 2 by eliminating cut-rules and commuting the cut-rule up until reaching the rule s ⊥ introducing the other formula of the cut-rule:

π 1 = r = ⊤ x s x ρ 2 cut ρ 3 ; ϖ 1 = r = ⊤ x s x ρ ′ 2 s ⊥ ρ cut ρ 3 ; ϖ 2 = r = ⊤ x s x ρ ′ 2 s ⊥ x cut ρ ρ 3 π 2 = r = ⊤ x ρ 2 cut ρ 3 π 3 = r = ⊤ ρ 3
We eliminate the cut in ϖ 2 , then use the ⊤-rule r to erase any introduced cut-rules, reaching

ϖ 3 = ⊤ ρ ρ 3
. As ρ is cut-free, we can commute r down with = * c (if s ⊥ was a ⊤-rule, we first use a ⊤ -⊤ commutation), finally obtaining π 3 . Therefore π ←-π r (diagrammatically represented on Figure 16). Furthermore, the sequence ϖ l = * c ϖ r contains proofs of measure at most max(|π l |, |π r |).

1 β * -→ ϖ 1 β * -→ ϖ 2 β * -→ ϖ 3 = * c π
Proof. This proof is similar to the one of Lemma 72. In all cases, the exhibited sequence = * c will have length 0 or 1, thus the result on measures will follow by Lemma 69.

If the π l β ←-π t and π t β -→ π r steps involve only distinct rules then, taking into account that rules of one may be duplicated or erased by the other step, we have a proof ϖ such that

π l β * -→ ϖ β *
←-π r . From now on, we assume not to be in this case, meaning both steps involve (at least) one common rule. We distinguish cases according to the kinds of the β -→ steps.

If both steps are key or ⊤ -cut commutative cases. As the two reductions share a rule, it must be the cut-rule. If π l = π r we are done, otherwise we have above this cut rule two rules of kind ax or ⊤. We can check that each of these critical pairs leads to the same resulting proof from any choice of cut-elimination, unless both cases are ⊤ -cut commutative cases, in which case the results are equal up to a ⊤ -⊤ commutation. Thus π l = π r or π l = c π r . ←-π r (taking into account that rules of one may be duplicated or erased by the other step). Now, assume both reductions involve a same cut-rule. The key case must be an ax key case or a ⊤-cut commutative case, for otherwise the commutative step cannot share a rule with it (because the commutative step cannot be a cut -cut case). We can still do this key step after the commutation (maybe twice in case of duplication), recovering π r if it is an ax-key case or a proof equal to a ⊤-commutation in the ⊤ -cut case (we need the ⊤-rule to absorb with the rule sent below the cut-rule during the commutative step). Thus: ←-π 3 (diagrammatically represented on Figure 16).

If

Proof. Remember a block of cut-rules is a maximal set of cut-rules in a proof such that all of these rules are a premise of another rule in the set, or use as premise the conclusion of a rule in the set (Definition 68). We begin by observing that two cut -cut commutations in different blocks always commute (remark a cut -cut commutation cannot duplicate nor erase a sub-proof). Call B the block containing the (unique) cut-rule c of π 2 involved in

π 2 β -→ π 3 . This allows to decompose π 1 ∼ c π 2 into π 1 ∼ B0 c ϖ 1 ∼ B1 c ϖ 2 . . . ϖ n ∼ Bn c π 2 , with ∼ Bi
c composed uniquely of cut -cut commutations between rules of a same block B i , all B i being disjoint and different from B, except B 0 = B (we can always add an empty sequence of commutations if needed). -→ duplicates B ′ , then we need to do each cut -cut commutation twice to recover π 3 . Thus, applying this reasoning successively on blocks

Given commutations in another block

B ′ than B, if ρ ∼ B ′ c π 2 β -→ π 3 then there exists ρ ′ such that ρ β -→ ρ ′ ∼ B ′ c π 3 . Indeed, no commutation in ρ ∼ B ′ c π 2 involves
B i from B n to B 1 yields π 1 ∼ B0 c ϖ 1 β -→ π ′ 3 ∼ B1 c ϖ ′ 2 . . . ϖ ′ n ∼ Bn c π 3 .
It suffices now to prove there exist κ and

κ ′ such that π 1 β -→ κ β * -→ κ ′ β * ←-π ′ 3 .
Indeed, seeing ∼ c as a particular case of If r and c 0 commute (with a commutative β -→ step), then we can do this commutation, yielding some proof κ from π 1 . We can then commute cut-rules to bring c below r and execute the corresponding β -→ step, yielding some proof κ ′ . Observe then that in π 3 commuting the rule c 0 up until reaching r, then commuting it up with r and with c 0 (or instead with any cut-rules created by the β -→ step between c and r if it is a key or ⊤ -cut commutative step) yields κ ′ . We then have π 1

β -→ κ β * -→ κ ′ β * ←-π 3 .
Suppose now that r and c 0 do not commute. This means r is a rule introducing the formula A 0 on which c 0 cuts. This also implies that the π 2 β -→ π 3 is not a key step, because r cannot introduce the formula A on which c cuts. Call ρ the sub-proof of π 1 above c 0 in the branch not leading to r. This is also the sub-proof of π 3 above c 0 in the same branch, up to bringing c 0 on top of the block B by some β * -→ steps first (c does not belong to this branch as it commuted with r). We reduce all cut-rules in ρ using only β -→ steps (using Lemma 70), in the same way in both π 1 and π 3 , obtaining a cut-free proof ρ ′ , in π ′ 1 and π ′ 3 respectively. In particular, we have π

1 β * -→ π ′ 1 and π 3 β * -→ • β * -→ π ′ 3 .
Call r ⊥ the rule in ρ ′ introducing the formula A ⊥ 0 (which is a rule of the main connective of A ⊥ or an ax or ⊤-rule), and τ the sequence of rules in ρ ′ between c 0 and r ⊥ . We commute in π ′ 1 (resp. π ′ 3 ) rules of τ with c 0 , yielding π ′

1 β * -→ π ′′ 1 (resp. π ′ 3 β * -→ π ′′
3 ) as τ is cut-free, obtaining a proof with c 0 having on its premises rules r and r ⊥ .

We can now apply a key or ⊤ -cut commutative case on c 0 , yielding π ′′

1 β -→ π ′′′ 1 and π ρ κ ρ ′ κ ′ π ′ ϖ ′ ∼ c ∼ c ∼ c β β β * β * ι 1 ι 3 β β * β * ι 4 ι 5 β * β * = * c ι ′ 1 ι ′ 4 ι ′ 5 β * β * β * = * c = * c = * c = * c Figure 17
Diagram of the case n ̸ = ∅ and k = 0 in the proof of Proposition 75 Hypotheses are depicted in black; in red is an application of Lemma 74; in green of Lemma 73; blue parts correspond to using the induction hypothesis on the underlined proofs along to Lemma 70.

π ′′ 3 β -→ π ′′′ 3 .
Observe that π ′′′ 1 and π ′′′ 3 differ only by the fact that in π ′′′ 1 the cut-rule c is below, in the block B, while it is above the rules created by the key case on c 0 (or erased if it was ⊤ -cut commutative case) in π ′′′ 3 . We can commute it up in B in π ′′′ 1 , then commute it with any rules created by the case on c 0 to recover π ′′′ 3 . Whence π Proof. We denote by n the maximum of the measures of the proofs on the sequence π = * c ϖ, and k the length of this sequence (i.e. its number of proofs minus 1). We prove the result by induction on the lexicographic order of (n, k).

1 β * -→ π ′ 1 β * -→ π ′′ 1 β -→ π ′′′ 1 β * -→ π ′′′ 3 β ←-π ′′ 3 β * ←-π ′ 3 β * ←-• β * ←-π 3 , and in particular π 1 β -→ β * -→ π ′′′
If n = ∅, then π and ϖ are cut-free, thus their only normal form are themselves and π = * c ϖ. Thus, assume from now on that n > ∅, thus π has a cut and therefore ϖ has a cut too (as = c preserves having a cut-rule).

Assume k = 0, and take π ′ (resp. ϖ ′ ) a normal form of π (resp. ϖ). Therefore,

π ′ β * ←-π = ϖ β * -→ ϖ ′ . As n ̸ = ∅, one of the β -→ step in π β * -→ π ′ (resp. π β * -→ ϖ ′ ) is a β -→
step. Consider a sequence leading to the first such

β -→ step: we have π ′ β * ←-ρ ′ β ←-ρ ∼ c π ∼ c κ β -→ κ ′ β * -→ ϖ ′ , thus π ′ β * ←-ρ ′ β ←-ρ ∼ c κ β -→ κ ′ β * -→ ϖ ′ .
The reasoning we will do is illustrated on the diagram of Figure 17. Proving the result for ρ ′ and κ ′ is enough

to yield π ′ = * c ϖ ′ . Applying Lemma 74, ρ ′ β * -→ ι 1 β * ←-ι 3 β ←-κ β -→ κ ′ . Using Lemma 73, ρ ′ β * -→ ι 1 β * ←-ι 3 β * -→ ι 4 = * c ι 5 β * ←-κ ′ ,
* c , ι ′ 5 = * c ϖ ′ π ϖ ρ ρ ′ π ′ ϖ ′ = c ∼ c β β * β * ι 1 ι 2 β β * β * ι 3 ι 4 β * β * = * c ι ′ 1 ι ′ 3 ι ′ 4 β * β * β * = * c = * c = * c = * c Figure 18
Diagram of the case n ̸ = ∅ and k = 1 in the proof of Proposition 75 Hypotheses are depicted in black; in red is an application of Lemma 74; in green of Lemma 72; blue parts correspond to using the induction hypothesis on the underlined proofs along to Lemma 70.

as normal forms of κ ′ are equal up to = * c . Therefore,

π ′ = * c ι ′ 1 = * c ι ′ 4 = * c ι ′ 5 = * c ϖ ′ and we conclude π ′ = * c ϖ ′ Suppose now that k = 1, thus π = c ϖ. Take π ′ (resp. ϖ ′ ) a normal form of π (resp. ϖ). As n ̸ = ∅, one of the β -→ step in π β * -→ π ′ is a β -→ step. We set π ∼ c ρ β -→ ρ ′ β *
-→ π ′ . A diagram representing the proof of this case is depicted on Figure 18. Applying Lemma 74, Proof. This is a particular case of Proposition 75 with π = ϖ. ◀ ▶ Theorem 35. Let π and ϖ be βη-equal MALL proofs. Then, letting π ′ (resp. ϖ ′ ) be a result of expanding all axioms and then eliminating all cuts in π (resp. ϖ), π ′ is equal to ϖ ′ up to rule commutations.

ρ ′ β * -→ ι 1 β * ←-ι 2 β ←-π.
Proof. We have π = βη ϖ, so η(π) = β η(ϖ) by Proposition 4. This sequence can be

decomposed into η(π) = µ 0 β * ←-ν 1 β * -→ µ 1 β * ←-ν 2 β * -→ µ 2 β * ←-ν 3 . . . ν n β * -→ µ n = η(ϖ) for some proofs ν i and µ i . Each µ i has a normal form µ ′ i (by Lemma 70, choosing µ ′ 0 = π ′ and µ ′ n = ϖ ′ ). Theorem 34 applied to ν i yields µ ′ i-1 = * c µ ′ i , see the diagram on Figure 19. Thence π ′ = µ ′ 0 = * c µ ′ n = ϖ ′ . ◀ η(π) = µ 0 ν 1 µ 1 ν 2 µ 2 ν 3 µ 3 ν 4 . . . . . . ν n µ n = η(ϖ) β * β * β * β * β * β * β * β * π ′ = µ ′ 0 µ ′ 1 µ ′ 2 µ ′ 3 . . . µ ′ n = ϖ ′ β * β * β * β * β * = * c = * c = * c = * c = * c

D.2 Proof of Proposition 36

▶ Proposition 36. Let π be a proof equal, up to rule commutations, to id A with A distributed. The ⊤-rules of π are of the shape ⊤ ⊢ ⊤, 0 (with ⊤ in A being the dual of 0 in A ⊥ , or vice-versa) and ⊥-rules and 1-rules come by pairs separated with ⊕ i -rules only, called a 1/ ⊕ /⊥-pattern:

1 ⊢ 1 ρ ⊢ F ⊥ ⊢ ⊥, F
where ρ is a sequence of ⊕ i -rules (with ⊥ in A being the dual of 1 in A ⊥ , or vice-versa). Moreover, there are no sequent in π of the shape ⊢ B & C.

Proof. We prove a stronger property: any sequent S of a proof π obtained through a sequence of rule commutations of cut-free MALL from id A for a distributed formula A respects:

(1) the formulas of S are distributed;

(2) if ⊤ is a formula of S, then S = ⊢ ⊤, 0;

(3) if ⊥ is a formula of S, then S = ⊢ ⊥, F with F given by the following grammar

F := 1 | F ⊕ D | D ⊕ F , where the distinguished 1 is the dual of ⊥ in A ⊥ if ⊥ a sub-
) if S contains several negative formulas or several positive formulas, then its negative formulas are `-formulas. Remark that ( 5) is a corollary of properties (2), ( 3) and ( 4). As we have in = c no commutations with a cut-rule (in particular no cut -⊤ commutation) and no ⊤ -⊗ commutation creating a sub-proof with a cut-rule, it follows π is cut-free and has the sub-formula property, making (1) trivially true. We will prove that the fully expanded axiom respects properties (2), ( 3) and ( 4), and that they are preserved by any rule commutation of = c .

The fully expanded axiom respects the properties

We prove it by induction on the distributed formula A. Notice that sub-formulas of A are also distributed. By symmetry, assume A is positive.

If A ∈ {X, 1, 0} where X is an atom, then:

id A ∈ { ax ⊢ X ⊥ ,X ; 1 ⊢ 1 ⊥ ⊢ ⊥, 1 ; ⊤ ⊢ ⊤, 0 }
Each of these proofs respects (2), ( 3) and ( 4). Assume the result holds for B and C, and that

A = B ⊗ C. The proof id A is: id B ⊢ B ⊥ , B id C ⊢ C ⊥ , C ⊗ ⊢ B ⊥ , C ⊥ , B ⊗ C ⊢ B ⊥ `C⊥ , B ⊗ C
We have to prove the sequents ⊢ B ⊥ , C ⊥ , B ⊗C and ⊢ B ⊥ `C⊥ , B ⊗C respect the properties. The latter respects (2), ( 3) and ( 4) trivially for its has neither a ⊤, ⊥ nor & formula. As B ⊥ `C⊥ is distributed, it follows that neither B ⊥ not C ⊥ can be a ⊤, ⊥ or & formula, and as such the former sequent also respects the properties.

Suppose A = B ⊕ C with sequents of B and C respecting the properties. Now, id A is: 3) and ( 4), as the ⊕ is the dual of the &. By symmetry, we show the properties are also fulfilled by ⊢ B ⊥ , B ⊕ C, and they will be respected by ⊢ C ⊥ , B ⊕ C with a similar proof. As the formulas are distributed, B ⊥ cannot be a ⊤ formula. If B ⊥ is not a ⊥ nor & formulas, then (2), ( 3) and ( 4) hold for ⊢ B ⊥ , B ⊕ C. If it is, then using that ⊢ B ⊥ , B respects (3) and ( 4), it follows that in B ⊕ C is also of the required shape, as B was.

id C ⊢ C ⊥ , C ⊕ 2 ⊢ C ⊥ , B ⊕ C id B ⊢ B ⊥ , B ⊕ 1 ⊢ B ⊥ , B ⊕ C & ⊢ C ⊥ & B ⊥ , B ⊕ C The sequent ⊢ C ⊥ & B ⊥ , B ⊕ C respects (2), (

Every possible rule commutation preserves the properties

We show it for each rule commutation, using every time the notations from Tables 6 and7 in Definition 42, on Pages 22 and 21. By symmetry, we treat only one case for ⊗ -⊗, `-⊗, & -⊗ and ⊕ i -⊗ commutations.

⊤-commutations Using properties (1) and (2), we cannot do any commutation between a ⊤-rule and a `, ⊗, &, ⊕ i , ⊥ or ⊤-rule, so no commutations at all involving a ⊤-rule (we supposed to not consider commutations with cut-rules exactly for this case).

⊥-commutations Using properties (1) and (3), we cannot do any commutation between a ⊥-rule and a `, ⊗, & or ⊥-rule. A commutation between a ⊥ and a ⊕ i -rule preserves property (3): we have by hypothesis Γ empty and A 1 ⊕ A 2 of the right shape. It also respects ( 2) and (4) trivially.

C `commutation We have to show the properties for ⊢ A 1 , A 2 , B 1 `B2 , Γ. As ⊢ A 1 À2 , B 1 `B2 , Γ respects them, negative formulas of Γ are `-formulas by [START_REF] Di | Jump from parallel to sequential proofs: Additives[END_REF]. By distributivity, if A 1 (or A 2 ) is a negative formula, then it must be a `one. Thus, ⊢ A 1 , A 2 , B 1 `B2 , Γ fulfills (2), ( 3) and (4).

C ⊕i ⊕j commutation We have to show the properties for

⊢ A i , B 1 ⊕ B 2 , Γ. As ⊢ A 1 ⊕ A 2 , B 1 ⊕ B 2 , Γ
respects them, negative formulas of Γ are `-formulas by [START_REF] Di | Jump from parallel to sequential proofs: Additives[END_REF]. If A i is positive or a `, then we are done. Otherwise, as ⊢ A i , B j , Γ fulfills the properties, it follows Γ is empty and B j of the desired shape. By (1), B j is not 0, thus

A i is not ⊤. Whether A i is ⊥ or &, the sequent ⊢ A i , B 1 ⊕ B 2 respects the properties. C ⊗ ⊗ commutation We have to show the properties for ⊢ A 1 ⊗ A 2 , B 1 , Γ, ∆. As ⊢ A 1 ⊗ A 2 , B 1 ⊗ B 2 ,
Γ, ∆, Σ respects them, negative formulas of Γ and ∆ are `-formulas by [START_REF] Di | Jump from parallel to sequential proofs: Additives[END_REF]. If B 1 is positive or a `, then we are done. Otherwise, as ⊢ A 2 , B 1 , ∆ fulfills the properties, it follows ∆ is empty and B 1 of the desired shape, so B 1 is a 0, 1 or ⊕-formula. This is impossible as B 1 ⊗ B 2 is distributed by [START_REF] Abrusci | A new correctness criterion for cyclic proof nets[END_REF]. [START_REF] Abrusci | A new correctness criterion for cyclic proof nets[END_REF], and if it is a ⊥ or a &, then the hypothesis on ⊢ A 1 , B i implies that the properties are also respected in

C & & , C & `, C & , C & ⊗ and
⊢ A 1 & A 2 , B i . For ⊢ A 1 , B 1 ⊕ B 2 (and similarly ⊢ A 2 , B 1 ⊕ B 2 ), A 1 cannot be a ⊤ by
⊢ A 1 , B 1 ⊕ B 2 .
C ⊕i and C ⊕i `commutations Let us show the properties for ⊢ A 1 , A 2 , B 1 ⊕ B 2 , Γ in the first commutation and ⊢ A 1 `A2 , B i , Γ in the second. As they hold for ⊢ A 1 , A 2 , B i , Γ, negative formulas in A 1 , A 2 , B i , Γ are `-formulas by ( 5) and the result follows.

C ⊗ ⊕i commutation We prove ⊢ A 1 , B 1 ⊕ B 2 , Γ respects the properties. As ⊢ A 1 ⊗ A 2 , B 1 ⊕ B 2 ,
Γ, ∆ fulfills them, negative formulas of Γ are `by [START_REF] Di | Jump from parallel to sequential proofs: Additives[END_REF]. If A 1 is a negative other than a `, then for ⊢ A 1 , B i , Γ respects the properties we have that Γ is empty and B i of the desired shape. By (1), B i is not a 0, so A 1 is not a ⊤. But then B 1 ⊕ B 2 also have the wished shape for A 1 , and

⊢ A 1 , B 1 ⊕ B 2 fulfills the properties. C ⊕i ⊗ commutation We prove ⊢ A 1 ⊗ A 2 , B i , Γ, ∆ respects the properties. As ⊢ A 1 ⊗ A 2 , B 1 ⊕ B 2 ,
Γ, ∆ fulfills them, negative formulas of Γ and ∆ are `by [START_REF] Di | Jump from parallel to sequential proofs: Additives[END_REF]. As A 1 ⊗ A 2 is distributed (1), A 1 cannot be a 0, 1 nor ⊕ formula, so by ⊢ A 1 , B i , Γ fulfilling the properties it follows that B i cannot be a negative other than a `. The conclusion follows.

C ⊗ commutation We prove the properties for [START_REF] Di | Jump from parallel to sequential proofs: Additives[END_REF] negatives of Γ and ∆ can only be `-formulas. As A 1 `A2 is distributed by (1), A 1 and A 2 are positive or `-formulas. The conclusion follows.

⊢ A 1 , A 2 , B 1 ⊗ B 2 , Γ, ∆. As ⊢ A 1 À2 , B 1 ⊗ B 2 , Γ, ∆ respects them, by
C ⊗ `commutation We prove the properties for ⊢ A 1 `A2 , B 1 , Γ. As ⊢ A 1 , A 2 , B 1 , Γ respects them, by (5) negative of ∆ and B 1 can only be `-formulas, proving the result. Therefore, we proved the expanded identity respects these properties, and they are preserved by all rule commutations. The conclusion follows. ◀

D.3 Proof of Lemma 37

▶ Definition 76 (Slice). For π an MALL sequent calculus proof, consider the (non-correct) proof tree obtained by deleting one of the two subtree of each &-rule of π (thus, in the new proof tree, &-rules are unary):

⊢ A, Γ & 1 ⊢ A & B, Γ ⊢ B, Γ & 2 ⊢ A & B, Γ
The remaining rules form a slice of π. We denote by S(π) the set of slices of π.

Note the relation between slices in the sequent calculus and linkings in proof-nets: a slice "belongs" to an additive resolution, and a &-resolution "selects" a slice from a proof. 10 In this spirit, if a proof-net θ is obtained by desequentializing a proof π, there is a bijection between linkings in θ and slices of π. Slices satisfy a linearity property (validated by proofs of MLL as well): any connective in the conclusion is introduced by at most one rule in a slice.

Cut-elimination can be extended from proofs to slices except that some reduction steps produce failures for slices: when a & 1 faces a ⊕ 1 and conversely. The reduction of the slice

⊢ A, Γ ⊕ 1 ⊢ A ⊕ B, Γ ⊢ B ⊥ , ∆ & 1 ⊢ B ⊥ & A ⊥ , ∆ cut ⊢ Γ, ∆
10 An alternative definition of desequentialization in [START_REF] Hughes | Proof nets for unit-free multiplicative-additive linear logic[END_REF] consists in building a linking by slice. is a failure since the selected sub-formulas of A ⊕ B and its dual do not match. Given two slices s and r with respective conclusions ⊢ A, Γ and ⊢ A ⊥ , ∆, their composition by cut s A ▷◁ r reduces either to a slice or to a failure. Given two sets of slices S 1 (all with conclusion ⊢ A, Γ) and S 2 (all with conclusion ⊢ A ⊥ , Γ), their composition S 1 A ▷◁ S 2 is the set of all slices obtained by composing a slice in S 1 with a slice in S 2 . Given a set of slices S, its normal form is the set of all cut-free slices obtained by reducing the cuts in the slices of S. This can give an empty set if all slices in S lead to failures during reduction.

▶ Lemma 77. Let π 1 and π 2 be cut-free proofs whose composition over A reduces to a cut-free proof ϖ. The normal form of S(π 1 ) A ▷◁ S(π 2 ) is S(ϖ). Moreover, for each s ∈ S(ϖ), there exist s 1 ∈ S(π 1 ) and s 2 ∈ S(π 2 ) such that s 1 A ▷◁ s 2 reduces to s, and s 1 and s 2 make dual choices on the additive connectives of A.

Proof. We can check that each cut-elimination steps preserves the set of slices. Moreover, if a slice is obtained by making distinct choices on the dual occurrences of an additive connective of a cut formula, then it reduces (in possibly many steps) to a failure. ◀ ▶ Lemma 78. Let π 1 and π 2 be cut-free proofs of ⊢ Γ with ⊤-rules only of the shape ⊤ ⊢ ⊤, 0

. Assume that π 1 = * c π 2 , where in this sequence there are no rule commutations involving a ⊤-rule. Then for each slice s 1 ∈ S(π 1 ), there exists a unique s 2 ∈ S(π 2 ) such that s 1 and s 2 make the same choices for additive connectives in Γ.

Proof. This can be easily checked for each possible equation in = c . ◀ ▶ Lemma 79. Given a choice C of premise for additive connectives of A (but not A ⊥ ), there exists a unique slice of S(id A ) on it, which furthermore makes on A ⊥ the dual choices of C.

Proof. Direct induction on A, following the definition of id A on Table 3. ◀ ▶ Lemma 80. Let π and π ′ be cut-free MALL proofs respectively of ⊢ A ⊥ , B and ⊢ B ⊥ , A, whose composition over A reduces to id B up to rule commutation. Set ρ the proof obtained by eliminating all cuts in the composition of π and π ′ over B, without using any ax or ⊥ -1 key case as well as ⊤ -cut commutative case. Then for any slice s of π, there exists a slice s ′ of π ′ such that s ∪ s ′ has the same 0-ary rules as a slice of ρ.

Proof. Take s ∈ S(π), and denote by C the choices made in s on & and ⊕ connectives of the formula B. Any slice of ρ has for 0-ary rules the ones of r ∪r ′ for r ∈ S(π) and r ′ ∈ S(π ′ ) such that r ′ makes choices on B corresponding to the dual of those of r on B ⊥ (using Lemma 77). Call ρ ′ a cut-free proof resulting from cut-elimination of the composition of π and π ′ over A; by hypothesis, ρ ′ = * c id B . By Lemma 79, there is a (unique) slice of id B with choices C on B and dual choices C ⊥ on B ⊥ . Applying Proposition 36 and Lemma 78, there is a slice r ′ of ρ ′ with choices C and C ⊥ . According to Lemma 77, we have slices t ∈ S(π) and t ′ ∈ S(π ′ ) whose composition reduces to r ′ . In particular, t makes choices C on B and t ′ choices C ⊥ on B ⊥ . Therefore, t ′ makes on B ⊥ the dual choices of s on B, and as such the composition of s and t ′ reduces to a slice of ρ. ◀ ▶ Remark. Lemma 80 is the analogue of Lemma 16 in sequent calculus.

Lemma 80 will be used to prove that & -⊕ i key cases during cut-elimination do not erase 0-ary rules. More precisely, given A π, π ′ ≃ B and considering a 0-ary rule t (typically a ⊤-or 1-rule) in π, we use this lemma to say that t is still in the reduction of π A ▷◁ π ′ before applying any ax, ⊥ -1 or ⊤ -cut case. This is done by taking a slice t belongs to, then finding an associated slice such that normalization of the composition is not a failure thanks to the lemma, and thus the resulting slice belongs to the normal form. ▶ Lemma 37. If A π, π ′ ≃ B with π and π ′ cut-free then all ⊤-rules in π and π ′ are of the form ⊤ ⊢ ⊤, 0 and all ⊥-rules and 1-rules belong to 1/ ⊕ /⊥-patterns.

Proof. Consider t a ⊤-rule ⊤ ⊢ Γ, ∆ in π, with Γ occurrences of sub-formulas of A ⊥ and ∆ of B. Call s the slice it belongs to. By Lemma 80 and Proposition 36, there exists s ′ ∈ S(π ′ ) such that s B ▷◁ s ′ reduces to a slice in which the only ⊤-rules are ⊤ ⊢ ⊤, 0 rules, with ⊤ being the dual occurrence of 0. Along the reduction, t is either preserved and Γ as well, or t is absorbed by another ⊤-rule and Γ stays in the context of a ⊤-rule. As in the resulting proof ⊤ and 0 are not both sub-formula of A ⊥ , it follows Γ is a subsequent of ⊤ or of 0. By symmetry (cutting on the other formula), ∆ is too. Moreover, Γ or ∆ must contain a ⊤. Thus, ⊤-rules in π are of the form ⊤ ⊢ ⊤ , ⊤ ⊢ ⊤, 0 or ⊤ ⊢ ⊤, ⊤ .

Assume there is a ⊤ ⊢ ⊤ rule in π, with ⊤ a sub-formula of A ⊥ . Again it belongs to a slice whose reduction leads to a slice containing only ⊤-rules of the form ⊤ ⊢ ⊤, 0 . This is not possible since the ⊤ ⊢ ⊤ rule cannot be absorbed by a ⊤ -cut commutation for it has no context in B.

Suppose now there is a ⊤ ⊢ ⊤, ⊤ rule in π. When such a rule is absorbed by another ⊤-rule in a ⊤ -cut commutation, the resulting ⊤-rule still has (at least) two ⊤-formulas. But when reaching the normal form, we only have ⊤-rules with one ⊤-formula: contradiction. We conclude that all ⊤-rules in π are of the form ⊤ ⊢ ⊤, 0 . We now prove the part of the lemma for ⊥-rules. For this we will need the following result: ( * ) there are no sequent of the shape ⊢ D & E in π. Assume w.l.o.g. D & E is a sub-formula of A ⊥ , and let s be a slice containing it (i.e. one of its two parts). By Lemma 80, there exists a slice s ′ ∈ S(π ′ ) such that s In π, we look at a possible rule r below a sequent ⊢ F . It cannot be a ⊗-rule by distributivity, nor a `-rule has the sequent has a unique formula, or a &-rule due to ( * ). If r is a ⊕ i -rule, then we keep a sequent ⊢ F , and if it is a ⊥-rule then it is one of the required shape.

As a consequence, each 1-rule is followed by some ⊕ i -rules and possibly a ⊥-rule (let us call a 1/⊕-pattern a 1-rule followed by a maximal such sequence of ⊕ i -rules). If a 1/⊕-pattern stops without a ⊥-rule below it, we have only one formula in the conclusion sequent of the proof: impossible as π is a proof of ⊢ A ⊥ , B. Thus, the ⊥-rule exists and to each 1-rule we can associate a ⊥-rule leading to 1/ ⊕ /⊥-pattern. Henceforth, there are at least as many ⊥-rules as 1-rules. Now, in the normal forms, the number of 1-rules is the same as the number of ⊥-rules. Consider a ⊥-rule r which is erased during normalization by cut over B, and let s be a slice containing it. By Lemma 80, there exists a slice s ′ ∈ S(π ′ ) such that s B ▷◁ s ′ reduces to a slice of the normal form. If r disappears, it must be through a ⊥ -1 key case which also erases a 1-rule (it cannot be through a ⊤ -cut commutative case as ⊤-rules are of the shape ⊤ ⊢ ⊤, 0

). Furthermore, if we duplicate a 1-rule then it is on top of a 1/ ⊕ /⊥-pattern and thus we duplicate a ⊥-rule as well. As a consequence, (number of ⊥-rules -number of 1-rules) can only increase during the reduction. We conclude the number of ⊥-rules is equal to the number of 1-rules in π, and thus every ⊥-rule belongs to a 1/ ⊕ /⊥-pattern. ◀

D.4 Proof of Theorem 38

▶ Proposition 81. Taking proofs π and ϖ such that π = * c ϖ, we have π = βη ϖ.

Proof. By giving the reductions for each equality. For example: ). Secondly, when a cut-rule has above one of its (let say left) premises a ⊥-rule (necessarily with a 1-rule above, a property we are going to preserve through our reduction strategy):

π ⊢ A 1 , A 2 , B 1 , B 2 , Γ ⊢ A 1 `A2 , B 1 , B 2 , Γ ⊢ A 1 `A2 , B 1 `B2 , Γ ax ⊢ A 2 ⊥ ,A 2 ax ⊢ A 1 ⊥ ,A 1 ⊗ ⊢ A ⊥ 2 ⊗ A ⊥ 1 , A 1 , A 2 ⊢ A ⊥ 2 ⊗ A ⊥ 1 , A 1 `A2 cut ⊢ A 1 `A2 , B 1 `B2 , Γ reduces to both π ⊢ A 1 , A 2 , B 1 , B 2 , Γ ⊢ A 1 `A2 , B 1 , B 2 , Γ ⊢ A 1 `A2 , B 1 `B2 , Γ and π ⊢ A 1 , A 2 , B 1 , B 2 , Γ ⊢ A 1 , A 2 , B 1 `B2 , Γ ⊢ A 1 `A2 ,
If it is of the shape

1 ⊢ 1 ⊥ ⊢ 1, ⊥ ϕ ⊢ 1, Γ cut ⊢ 1, Γ
, we commute this cut-rule with the rules of ϕ until we reach the 1-rule introducing 1 and we reduce the obtained cut-rule

1 ⊢ 1 ⊥ ⊢ 1, ⊥ 1 ⊢ 1 cut ⊢ 1 into 1 ⊢ 1
. What we get is exactly ϕ.

Figure 1 ▶

 1 Figure 1 Graphs from an example of a proof-net: from left to right G λ 1 , G λ 2 and G {λ 1 ;λ 2 }

  A * A ⊥ a cut pair in Σ. Define the elimination of A * A ⊥ (or of the cut * between A and A ⊥ ) as: (a) If A is an atom, delete A * A ⊥ from Σ and replace any pair of links (l, A), (A ⊥ , m) (l and m being other occurrences of A ⊥ and A respectively) with the link (l, m).

Figure 3 ▶ Theorem 13 (

 313 Figure 3 Identity proof-nets (from left to right: atoms, `\⊗ and &\⊕)

Figure 4

 4 Figure 4 Non bipartite proof-net (top-left), non full proof-net (top-right) and one of their composition yielding the identity proof-net (bottom) (jump edges not represented)

Figure 7

 7 Figure 7 Proof-nets from Figure 5 composed by cut on (A ⊗ B) ⊕ (A ⊗ C)

Figure 8

 8 Figure 8An almost reduced composition of the proof-nets on Figure5

Figure 9

 9 Figure 9 Illustration of Lemma 25

Figure 11

 11 Figure 11 Almost reduced composition ϑ of θ and θ ′ by cut over B in the proof of Theorem 29

Figure 10 )▶

 10 belongs to G {λ;λ ′ } . Contradiction: W , the only & toggled by {λ; λ ′ }, cannot be in any switching cycle of G {λ;λ ′ } by (P3). ◀ Theorem 29. Assuming A θ, θ ′ ≃ B with A and B distributed, θ and θ ′ are bipartite ax-unique.

▶

  formula of A (or vice-versa), D is any formula, and in the sub-proof of π above S the ⊕-rules of the distinguished C ⊥ ⊕ B ⊥ are a ⊕ 2 -rule in the left-branch of the &-rule of B & C, and a ⊕ 1 -rule in its right branch; (5) if S contains several negative formulas or several positive formulas, then its negative formulas are `-formulas. See Appendix D.2. ◀ These properties are preserved by cut anti-reduction. Lemma 37. If A π, π ′ ≃ B with π and π ′ cut-free then all ⊤-rules in π and π ′ are of the form ⊤ ⊢ ⊤, 0 and all ⊥-rules and 1-rules belong to 1/ ⊕ /⊥-patterns.

Figure 12

 12 Figure 12 Diagrams of Lemmas 44 (left and center) and 45 (right, ENF means in η-normal form)

  β -→ φ and ϖ η -→ φ (or ϖ η -→ • η -→ φ if r belongs to a sub-proof duplicated by the β -→ step, or ϖ = φ if it belongs to a sub-proof erased by the β -→ step). In particular, a(ϕ β -→ φ) = a(π β -→ ϖ) for they use the same rules.

  π

▶

  preserves being in η-normal form. Lemma 45. Let π, ϖ and ϕ be proofs such that ϖ η * ←-π β * -→ ϕ, with ϖ an η-normal proof. There exists an η-normal proof φ such that ϖ β * -→ φ η * ←-ϕ. This is depicted on Figure 12. Proof. We have ϖ η m ←-π β n -→ ϕ. We reason by induction on the lexicographic order of the triple a(π β * -→ ϕ), n, m . If n = 0 or m = 0, then the result trivially holds.

--→ φ 1 (

 1 1 and m < m + 1, there exists an η-normal proof ν such that ϖ ϕ, with ν in η-normal form, a(κ β n -→ ϕ) ≤ a(π β * -→ ϕ) and n < n + 1. We obtain an η-normal proof µ such that ν β * -→ µ η * ←-ϕ. This concludes the first case. Consider the second case. Using the confluence of η Proposition 43), with ϖ in η-normal form, yields ϖ η *←-φ 1 . We then apply the induction hypothesis onϖ η * ←-φ 1 β * -→ φ 2 , with ϖ in η-normal form and a(φ 1 β * -→ φ 2 ) < a(π β * -→ ϕ). This yields an η-normal proof ν such that ϖ β * -→ ν η * ←-φ 2 .We use the induction hypothesis again, this time onν η * ←-φ 2 η * ←-κ β n -→ ϕ, with ν in η-normal form, a(κ β n -→ ϕ) ≤ a(π β * -→ ϕ) and n < n + 1. We obtain an η-normal proof µ with ν β * -→ µ η *←-ϕ, solving the second case. ◀ ▶ Proposition 4 (Reduction to axiom-expanded proofs). Let π and ϖ be MALL proofs such that π = βη ϖ. Then η(π) = β η(ϖ) with, in this sequence, only proofs in η-normal form.Proof. We reason by induction on the length of the sequence π = βη ϖ. If it is of null length, then π = ϖ and η(π) = η(ϖ). Otherwise, we have a proof ϕ such that πϕ = βη ϖ with -By induction hypothesis, η(ϕ) = β η(ϖ) using only proofs in η-normal form. We distinguish cases according to πϕ.If π β -→ ϕ, then as η(π) η * ←-π we can apply Lemma 45 to obtain an η-normal proof φ such that η(π) β * -→ φ η * ←-ϕ. Thus, φ = η(ϕ), so η(π) β * -→ η(ϕ) = β η(ϖ) and the result holds. Similarly, if π β ←-ϕ then, as ϕ η * -→ η(ϕ), there exists an η-normal proof φ such that π η * -→ φ β * ←-η(ϕ) (Lemma 45). Thus φ = η(π), and η(π)

Figure 13

 13 Figure 13 Diagrams of the cases of the proof of Lemma 45 (ENF means in η-normal form) In blue are uses of Lemma 44, in green of confluence of η -→ and in red of the induction hypothesis.

▶

  Finally, in a & -cut commutative case, we duplicate the cut-rule: R(π) ◁ R(ϖ).◀ Lemma 48 (◁ ⊆ = β ). Let θ and θ ′ be proof-nets such that θ ◁ θ ′ . Then θ = β θ ′ .Proof. By Definition 46 of ◁, there exists a * -vertex C in θ, with θ = θ 0 ⊔ θ 1 , such that θ ′ is θ where the syntax tree of C is duplicated into C 0 and C 1 , and linkings in θ 0 (respectively θ 1 ) use C 0 (respectively C 1 ) as C.

▶ Lemma 49 .

 49 Let π, ϖ and ρ be unit-free MALL proof trees of respective sequents ⊢ A, Γ, ⊢ A ⊥ , ∆ and ⊢ Γ, ∆. Assume πA ▷◁ ϖ = β ρ. Then B(R(π)) A ▷◁ B(R(ϖ)) reduces, after fully eliminating the cut on A, to B(R(ρ)).Proof. By the Simulation Theorem (Theorem 12), R(πA ▷◁ ϖ) = β R(ρ). By definition of R (Section 3.1), R(π A ▷◁ ϖ) = R(π) A ▷◁ R(ϖ), so by Theorem 9 B(R(π) A ▷◁ R(ϖ)) = B(R(ρ)).Moreover, by confluence of cut-elimination (Theorem 9), B(R(π) A ▷◁ R(ϖ)) can be obtained by taking the β-normal forms of R(π) and R(ϖ), composing them over A and reducing this cut. In other words, B(R(π)A ▷◁ R(ϖ)) = B(B(R(π)) A ▷◁ B(R(ϖ))),and the result follows. ◀ ▶ Theorem 13 (Type isomorphisms in proof-nets). Let A and B be two unit-free MALL formulas. If A ≃ B then there exist two proof-nets θ and ϑ such that A θ, ϑ ≃ B. Proof. By Definition 1 of an isomorphism and Proposition 4, there exist unit-free MALL proofs π and ϖ, respectively of ⊢ A ⊥ , B and ⊢ B ⊥ , A, such that π B ▷◁ ϖ = β id A and ϖ A ▷◁ π = β id B . By Lemma 49 and as

◀▶

  Lemma 56 (Distributed ambiguous isomorphic formulas). Let A and B be distributed formulas, such that A is ambiguous and A θ, θ ′ ≃ B. There exists a substitution σ and distributed formulas A ′ and B ′ , non-ambiguous, such that A = σ(A ′ ), B = σ(B ′ ) and A ′ ϑ, ϑ ′ ≃ B ′ for some proof-nets ϑ and ϑ ′ .

◀▶

  Lemma 65 (Reordering `-vertices). Let θ be a bipartite ax-unique proof-net of conclusions A = A l `Ar and B = B l ⊙ B r with ⊙ ∈ {⊗; ⊕} and A a distributed formula. Then ⊙ = ⊗ and there exist two bipartite ax-unique proof-nets of respective conclusions A ′ l , B l and A ′ r , B r where A ′ l `A′ r is equal to A l `Ar up to associativity and commutativity of `.

Proof.

  It suffices to compute the measure before and after each cut-elimination step. ◀ We denote by β -→ a β -→ step other than a cut -cut commutation. Also note ∼ c the equivalence closure of cut -cut commutation (which is already a symmetric relation).

Figure 16 1 and ϖ 2 such that π 1 β-→ ϖ 1 = * c ϖ 2 β←-π 3 (of π 2 β-→ π 3 ( 1 β-→ ϖ 1 , 3 β-→ ϖ 2 We conclude π 1 β-→ ϖ 1 = c ϖ 2 β←-π 3 , 2 β-→ π 3 step duplicates a sub-proof containing the rules of π 1 = c π 2 (which may happen if π 2 β-→ π 3 -→ step first, yielding π 1 β-→ ϖ 1 , 1 β-→ ϖ 1 = c ϖ 2 = c π 3 .

 1611232311321123231223111123 Figure 16 Diagrams of Lemmas 72, 73, and 74 (from left to right)

-→ ϖ 1 and ϖ 7 from π 3 through π 3 β-→ ϖ 7 ;

 37 * they share this sub-proof, and we use the strong normalization of β -→ (Lemma 70). Denote by s ⊥ the rule introducing the dual formula of s (i.e. the other formula on which we cut), and by ρ the rules in ϖ 1 (and ϖ 3 ) between s ⊥ and the cut-rule. By commuting the cut-rule above all rules in ρ, we have ϖ 1 β * -→ ϖ 2 with ϖ 2 having the cut-rule between s and s ⊥ . Doing the same commutations in ϖ 7 gives ϖ 7 β *

3 . 1 β

 31 And any proof in ϖ 3 = * c π 3 has measure at most |ϖ 3 | (as we only erase rules using ⊤ starting from ϖ 3 ) and|ϖ 3 | < |π 1 | for ϖ 2 β *-→ ϖ 3 is a non-empty sequence (still using Lemma 69). Finally, if s is a ⊤-rule then π 1 = c π 2 consists in introducing the rule r, before commuting it down with the cut-rule in π 2 β -→ π 3 (or erasing the cut-rule with it if r is also a ⊤-rule). Thus π -→ • = c • β ←-π 3 , by first using a ⊤ -cut commutative case with s, then introducing r through s then reintroducing the cut-rule. The result on measures follows by Lemma 69. ◀ ▶ Lemma 73. Let π t , π l and π r be MALL proofs such that π l β ←-π t β -→ π r . Then there exist ϖ l and ϖ r such that π l β * -→ ϖ l = * c ϖ r β *

  one step is a key or ⊤ -cut commutative step and the other a commutative step other than ⊤ -cut. By symmetry, assume π t β -→ π r is the key or ⊤ -cut step. If the cut-rules involved in these cases are distinct, then doing the commutative step cannot prevent doing the key one, so both steps commute and we have a proof ϖ such that π l β * -→ ϖ β *

-▶ 2 β-→ π 3 . Then there exist ϖ 1 and ϖ 2 such that π 1 β-

 2311 r (ax-key case and not a & -cut commutative case) π l β -→ β -→ π r (ax-key case and & -cut commutative case) π l β -→= c π r (⊤ -cut commutative case and not a & -cut commutative case) →= c π r (⊤ -cut commutative case and & -cut commutative case) If both steps are not key nor ⊤-cut commutative steps. Here again, as the two reductions share a rule, it must be the cut-rule. If π l ̸ = π r , then in π t β -→ π l we sent a rule from a branch of the cut below it, and in π t β -→ π r we do similarly on the other branch. We can do the commutation of π t β -→ π r in π l , and similarly the one of π t β -→ π l in π r (maybe twice in case of a duplication). The two resulting proofs differ exactly by the order of the two rules below the cut-rule, so are equal up to a commutation of these rules (which are not ⊤-rules by hypothesis). Thus, π l = π r or π l β * -→ • = c • β * ←-π r . ◀ Lemma 74. Let π 1 , π 2 and π 3 be proofs such that π 1 ∼ c π

  does not erase nor duplicate a sub-proof containing the block B ′ , then we have the result by first doing the β -→ step, then commutations of ∼ B ′ c . If the β -→ step erases the block B ′ , then ρ β -→ π 3 , which is a particular case of the previous one with ∼ B ′ c being equality. Finally, if β

2 β-→ π 3 1 β 2 β-→ π 3 1 β-→ π 3 ,

 2312313 π 3 , leading to the conclusion. Whence, we consider proofs such that π 1 ∼ B c π where β -→ involves a cut-rule in the block B, and prove there exist κ and κ ′ such that π ′ β * ←-π 3 . Call r one of the non-cut-rules involved in π (i.e. another rule than c). In π 1 , there is a cut-rule c 0 below r, belonging to B. If c 0 = c and this result holds for all possible choices of r, then we can first do β -→ in π 1 , then cut -cut commutations inside the rest of the block B to obtain π 3 : we have π and we are done. Thus, assume we choose an r such that c 0 ̸ = c.

▶

  Proposition 75. Let π and ϖ be proofs such that π = * c ϖ. For any normal form π ′ (resp. ϖ ′ ) for cut-elimination of π (resp. ϖ), π ′ = * c ϖ ′ .

with proofs in ι 4 = * c ι 5

 5 of measure at most max(|ι 3 |, |κ ′ |). However, n = |π| = |κ| > |κ ′ |, n = |ρ| > |ρ ′ | and n = |κ| > |ι 3 | by Lemma 69. Therefore, n > max(|ι 3 |, |κ ′ |) and the sequence ι 4 = * c ι 5 has proofs of measures strictly smaller than n, and ρ ′ , κ ′ and ι 3 are sequences of null length of measure strictly smaller than n. By induction hypothesis, we obtain that normal forms of ι 4 and ι 5 are related by = * c , and similarly between normal forms of ρ ′ , between normal forms of κ ′ and between normal forms of ι 3 . But normal forms of ι 5 are included in normal forms of κ ′ , those of ι 4 in those of ι 3 , and those of ι 1 in those of ρ ′ and ι 3 . Therefore, by taking a normal form ι ′ i of ι i through Lemma 70, we have π ′ = * c ι ′ 1 as normal forms of ρ ′ are equal up to = * c , ι ′ 1 = * c ι ′ 4 as normal forms of ι 3 are equal up to = * c , ι ′ 4 = * c ι ′ 5 as normal forms of ι 4 and those of ι 3 are equal up to =

-→ ι 3 = * c ι 4 β▶

 4 We then use Lemma 72 to have ι 2 β * * ←-ϖ, with the sequence ι 3 = * c ι 4 having proofs of measure strictly smaller than max(|π|, |ϖ|) ≤ n. By Lemma 69, |ρ ′ | < |ρ| = |π| and |ι 2 | < |π| ≤ n. Furthermore, ϖ can be seen as an empty sequence of ϖ = * c ϖ of measure at most n. By induction hypothesis, we obtain that normal forms of ι 3 and ι 4 are related by = * c , and similarly between normal forms of ρ ′ , between normal forms of ι 2 and between normal forms of ϖ. But normal forms of ι 1 are included in normal forms of ρ ′ and of ι 2 , those of ι 3 in those of ι 2 , and those of ι 4 in those of ϖ. Therefore, by taking a normal form ι ′ i of ι i through Lemma 70, we have π ′ = * c ι ′ 1 as normal forms of ρ ′ are equal up to = * c , ι ′ 1 = * c ι ′ 3 as normal forms of ι 2 are equal up to = * c , ι ′ 3 = * c ι ′ 4 as normal forms of ι 3 and those of ι 4 are equal up to = * c , ι ′ 4 = * c ϖ ′ as normal forms of ϖ are equal up to = * c . Therefore,π ′ = * c ι ′ 1 = * c ι ′ 3 = * c ι ′ 4 = * c ϖ ′ and we conclude π ′ = * c ϖ ′ . Lastly, assume k > 1. We have π = c ρ = * c ϖ. Take π ′ (resp. ρ ′ , ϖ ′ ) a normal form of π (resp.ρ, ϖ) (Lemma 70). By induction hypothesis on ρ = * c ϖ of length k -1 and maximum measure at most n, it follows that ρ ′ = * c ϖ ′ . Similarly on π = c ρ of length 1 < k and maximum measure at most n, we obtain π ′ = * c ρ ′ . Thus, π ′ = * c ϖ ′ . ◀ Theorem 34 (Confluence up to rule commutations). If π 1 and π 2 are cut-free proofs obtained by cut-elimination from the same proof π, then π 1 and π 2 are equal up to rule commutations.

Figure 19

 19 Figure 19 Diagram of the proof of Theorem 35 In black are hypotheses; in blue are applications of Lemma 70; in red are uses of Theorem 34.

  formula of A (or vice-versa), D is any formula, and the sub-proof of π above S is a sequence of ⊕ i rules leading to the distinguished 1;(4) if B & C is a formula of S, then S = ⊢ B & C, Fwith F given by the following grammarF := C ⊥ ⊕ B ⊥ | F ⊕ D | D ⊕ F , where the distinguished C ⊥ ⊕ B ⊥ is the dual of B & C in A ⊥ if B & C asub-formula of A (or vice-versa), D is any formula, and in the sub-proof of π above S the ⊕-rules of the distinguished C ⊥ ⊕ B ⊥ are a ⊕ 2 -rule in the left-branch of the &-rule of B & C, and a ⊕ 1 -rule in its right branch;

B

  ▷◁ s ′ reduces to a slice satisfying Proposition 36. Since D & E is a sub-formula of A ⊥ , it is not cut and the rule & i introducing D & E in s remains in the normal form. This contradicts Proposition 36 since any &-rule must have a non-empty context. Set F := 1 | F ⊕ D | D ⊕ F (with D an arbitrary formula).

▶

  B 1 `B2 , Γ (according to whether the cut-rule is first commuted with the `-rule on its left or on its right), thus the C `commutation is included in = β .◀ Theorem 38 (Isomorphisms completeness with units).If A ≃ B then A = E B.Proof. We can assume A and B to be distributed (Proposition 21). As A ≃ B, there are proofs π and ϖ of ⊢ A ⊥ , B and ⊢ B ⊥ , A, whose composition over B (resp. A) is equal to the axiom on ⊢ A ⊥ , A (resp. ⊢ B ⊥ , B) up to βη-equality. We assume w.l.o.g. π and ϖ to be cut-free proofs, and work only with axiom-expanded proofs thanks to Proposition 4. Using Theorem 35, we have π = * c id B . By Lemma 37, π and ϖ have ⊤-rules only of the shape ⊤ ⊢ ⊤, 0 and ⊥ and 1-rules in 1/ ⊕ /⊥-patterns. Using ⊥-commutations to move each ⊥-rule just below the 1-rule above it, we build π ′ and ϖ ′ such that π ′ and ϖ ′ have ⊤-rules only of the shape ⊤ ⊢ ⊤, 0 , ⊥ and 1-rules of the form 1⊢ 1 ⊥ ⊢ ⊥, 1 , π = * c π ′ and ϖ = * c ϖ ′ . Whence, π ′ B ▷◁ ϖ ′ = * c π B ▷◁ ϖ and π ′ A ▷◁ ϖ ′ = * c π A ▷◁ ϖ. By Theorem 35, for any normal form ρ of π ′ B ▷◁ ϖ ′ (resp. π ′ A ▷◁ ϖ ′ ), ρ = * c id A (resp. ρ = * c id B). We reduce cuts in π ′ B ▷◁ ϖ ′ (and similarly in π ′ A ▷◁ ϖ ′ ) in the following way. First, observe that when a ⊤-rule is above a cut-rule, then it is necessarily in a ⊤ ⊢ ⊤, 0 ϕ ⊢ ⊤, Γ cut ⊢ ⊤, Γ sub-proof, that we can reduce into ϕ ⊢ ⊤, Γ (because in this case ϕ = ⊤ ⊢ ⊤, 0

B. ◀ ▶ Corollary 17. Assuming A

  We proceed by contradiction: w.l.o.g. there is a link a in some linking λ ∈ θ which is between leaves of A ⊥ . By Lemma 16 there exists λ ′ ∈ θ ′ such that λ ∪ λ ′ matches for a cut over B. Whence a, which does not involve leaves of B, belongs to a linking of the composition where cuts have been eliminated (it belongs to the linking resulting from λ ∪ λ ′ ).

	θ, θ ′ ≃ B, θ and θ ′ are bipartite.
	Proof. But this reduction yields a bipartite proof-net by Proposition 15(i), a contradiction.	◀
	▶ Lemma 18. Assume θ and θ ′ are cut-free proof-nets of respective conclusions A ⊥ , B and
	B ⊥ , A, and that their composition over B yields the identity proof-net of A. Then any leaf
	of A ⊥ (resp. A) has (at least) one axiom link on it in θ (resp. θ ′ ).
	▶ Theorem 19. Assuming A θ, θ ′

≃ B, θ and θ ′ are bipartite full.

Proof. By Corollary 17, θ and θ ′ are bipartite, and thanks to Lemma 18, they are full.

Table 2

 2 De Morgan's isomorphisms E in Table1on Page 3 are isomorphisms in any ⋆-autonomous category with finite products). Moreover the isomorphisms of Table2(which are equalities in MALL) also hold in any ⋆-autonomous category with finite products.Completeness follows by Theorem 38 (isomorphisms in MALL are exactly those given by E) and from the fact that two objects definable in the language of ⋆-autonomous categories with finite products are equal in MALL if and only if they are related by the equational theory generated by Table2. For example, one can deduce

Table 2 .

 2 the last equation being derivable by induction on A). Henceforth, isomorphisms valid in all ⋆-autonomous categories with finite products are included in E enriched with ▶ Theorem 39 (Isomorphisms in ⋆-autonomous categories with finite products). E enriched with Table2is a sound and complete equational theory for isomorphisms in ⋆-autonomous categories with finite products.

Table 4

 4 Cut-elimination in sequent calculus (key cases)

Table 5

 5 Cut-elimination in sequent calculus (commutative cases)

Table 6

 6 Rule commutations involving a unit rule

  The completeness hypothesis on E for distributed formulas yieldsA d = E B d , and thus A = E A d = E B d = E B.The proof of this lemma uses some facts from[START_REF] Hughes | Proof nets for unit-free multiplicative-additive linear logic[END_REF] reproduced verbatim here. For Λ a set of linkings and W a &-vertex, Λ W denote the set of all linkings in Λ whose additive resolution does not contain the right argument of W . Write λ ′ if linkings λ, λ ′ ∈ θ are either equal or W is the only & toggled by {λ, λ ′ }. A subset Λ of a proof-net θ is saturated if any strictly larger subset toggles more & than Λ. It is straightforward to check that: (S1) If Λ is saturated and toggles W , then Λ W is saturated. (S2) If Λ is saturated and toggles W and λ ∈ Λ, then λ

	W

◀

C.6 Proof of Lemma 22

▶ Lemma 22 (Lemma 4.32 in

[START_REF] Hughes | Proof nets for unit-free multiplicative-additive linear logic[END_REF]

, adapted). Let ω be a jump-free switching cycle in a proof-net θ. There exists a subset of linkings Λ ⊆ θ such that ω ⊆ G Λ , ω ̸ ⊆ G Λ W and for any &-vertex W toggled by Λ, there exists an axiom link a ∈ ω depending on W in Λ.

Proof.

W = λ

  We show each inclusion separately. Let A and B be two distributed formulas such that A If A or B is ambiguous, then A and B are instances of two non-ambiguous distributed formulas A ′ and B ′ such that A ′ θ ′ , ϑ ′ ≃ B ′ by Lemma 56. Otherwise, A and B are non-ambiguous and the result holds.

	θ, ϑ ≃ B.

31 (Reduction to distributed non-ambiguous formulas). The set of couples of distributed formulas A and B such that

A θ, ϑ

≃ B is the set of instances (by a substitution on atoms) of couples of distributed non-ambiguous formulas

A ′ and B ′ such that A ′ θ ′ , ϑ ′ ≃ B ′ .

Proof.

9 Proof of Corollary 32

▶ Lemma 57. Let θ and ϑ be bipartite proof-nets of respective conclusions A, B and B ⊥ , C. Their composition over B reduces to a bipartite proof-net.

Proof. The resulting proof-net has for conclusions A, C. The only links in the new proof-net that were not in θ nor ϑ are those resulting from the replacement of a pair of links (l, m) and (m ⊥ , n) with a link (l, n), where m is a leaf of B. By bipartiteness of θ and ϑ, it follows l is a leaf of A and n one of C, so the new axiom link is between a leaf of A and one of C. ◀ ▶ Lemma 58. Let θ be a bipartite proof-net of conclusions A ⊥ , A, with A a non-ambiguous formula. Axiom links of θ are of the form (l ⊥ , l) for l a leaf of A.

  Figure 14 Illustration of the proof of Lemma 64▶ Theorem 62 (Bipartite proof-nets for non-ambiguous formulas). Let θ and θ ′ be bipartite proof-nets of respective conclusions A ⊥ , B and B ⊥ , A, with A a non-ambiguous formula. Then their composition over B reduces to the identity proof-net of A.

m s Proof. By Lemma 57, the composition of θ and θ ′ by cut reduces to a bipartite proof-net, of conclusions A ⊥ , A. By Corollary 61, this can only be the identity proof-net of A. ◀ ▶ Corollary 32. Let A and B be non-ambiguous formulas. If there exist bipartite proof-nets θ and ϑ of respective conclusions A ⊥ , B and B ⊥ , A, then A θ, ϑ ≃ B. Proof. By Theorem 62 both compositions yields identity proof-nets, whence A θ, ϑ ≃ B. ◀ C.10 Isomorphisms completeness for unit-free MALL (Theorem 33) ▶ Definition 63 (Sequentializing vertex). A terminal ( i.e. with no descendant) non-leaf vertex V in a proof-net θ is called sequentializing if, depending on its kind: ⊗\ * -vertex: the removal of V in G θ has two connected components. ⊕-vertex: the left or right syntax tree of V does not belong to G θ ( i.e. has no link on any of its leaves in G θ ). `\&-vertex: a terminal `\&-vertex is always sequentializing.

  & ⊕i and C ⊕i& commutations In these cases, (4) for ⊢ A 1 & A 2 , B 1 ⊕ B 2 , Γ imply Γ empty and B 1 ⊕ B 2 of the desired shape. Thus B i of the desired shape (B 1 ⊕ B 2 is not the distinguished formula as it has the same rule ⊕ i in both branches of the &-rule), proving the result for

C ⊗ & commutations These cases are impossible by property (4).

C

This example gives a retraction between (A `A⊥ ) ⊗ B and ((A `A⊥ ) ⊗ B) ⊕ B in MALL which is not an isomorphism (as is the retraction between A and (A ⊸ A) ⊸ A = (A ⊗ A ⊥ ) `A in MLL).

With q ̸ = m, as a and b are two distinct links in the same linking λ.

We recall that (•) ⊥ is defined by induction, making it an involution.

Funding This work was performed within the framework of the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon, within the program "Investissements d'Avenir" (ANR-11-IDEX-0007), and supported by the projects DyVerSe (ANR-19-CE48-0010), QuaReMe (ANR-20-CE48-0005) and ReCiProg (ANR-21-CE48-0019), all operated by the French National Research Agency (ANR). This work was also supported by the IRN Linear Logic.

1

as in the proof of Lemma 64). Thus, the sequentializing vertex of this proof-net is necessarily B l ⊙ B r . It follows ⊙ = ⊗, because all leaves of B are connected to leaves in A 1 , . . . , A n , so if ⊙ = ⊕ then B l ⊙ B r cannot be sequentializing. Removing the sequentializing B l ⊗ B r gives two proof-nets, with a bipartition of the A i into two classes: those linked to leaves of B l and the others linked to leaves of B r . We recover from these proof-nets bipartite ax-unique ones by adding `-vertices under the A i in an arbitrary order, yielding formulas A ′ l (with those linked to B l ) and A ′ r (with those linked to B r ). As we only removed and put back `-vertices, A ′ Proof. We remove all terminal &-vertices in the proof-net, then all terminal `-vertices, all in A. The resulting graphs are proof-nets θ i (for terminal negative vertices are sequentializing), of conclusions A i 1 , . . . , A i ni , B l ⊕ B r for the i-th proof-net. An illustration is Figure 15, except we have several of these proof-nets, having in common exactly T (B). As in the proof of Lemma 65, the roots of the new trees A i j cannot be negative vertices because the formula A is distributed: so they are ⊗\⊕-vertices or atoms. These ⊗\⊕-vertices cannot be sequentializing, since by bipartiteness and fullness every leaf of A i j is connected to the formula B l ⊕ B r (reasoning as in the proof of Lemma 64). Thus, the sequentializing vertex of these proof-nets is necessarily B l ⊕ B r , we can remove it: for a given i, all A i j are linked only to either B l or B r . We put back the `-vertices we removed, in the very same order. We then put back the &-vertices we removed, but in another order: we put together all θ i linked to B l , and all those to B r , yielding two proof-nets of conclusions B l , A ′ l and B r , A ′ r . These proof-nets are bipartite ax-unique ones (because adding and removing `does not modify the linkings, and & is disjoint union of linkings). We indeed have

to associativity and commutativity of &, because we only reordered &-vertices. ◀

We conclude by induction on the size s(A) of A, which is its number of connectives (thus unaffected by commutation and associativity of connectives).

▶ Theorem 33 (Isomorphisms completeness for unit-free MALL). Given A and B two unit-free MALL formulas, if

, we commute the cut-rule with the rules of ϕ until we reach the ⊥-rule introducing ⊥ and we reduce the obtained cut-rule

. What we get is exactly ϕ.

This strategy allows reaching a normal form ρ, with ⊤-rules only of the shape ⊤ ⊢ ⊤, 0 and ⊥ and 1-rules of the form

(this is preserved by our strategy). Furthermore, call σ the substitution replacing ⊤, 0, ⊥ and 1-formulas respectively by X ⊥ , X, Y ⊥ and Y , for X and Y fresh atoms. We can reach σ(ρ) by cut-elimination from σ(π ′ )

▷◁ σ(ϖ ′ ), for the reductions we did on units could as well have been done by ax-key cases. Moreover, σ(id A ) = id σ(A) , and in ρ = * c id A we can assume not to commute any ⊥-rule (for we start and end with 1-rules and ⊥-rules in

shapes only, and such commutations could only move the ⊥-rule below or above some ⊕ i -rules according to Proposition 36). Thus, σ(ρ) = * c id σ(A) . Using Proposition 81, it follows σ(ρ) = βη id σ(A) , and therefore σ(π ′ ) σ(B) ▷◁ σ(ϖ ′ ) = βη ax σ(A) with ax σ(A) the ax-rule on σ(A). A similar result holding for a cut over A, we have σ(A) ≃ σ(B), these formulas being unit-free. By Theorem 33, σ(A) = E σ(B). We conclude A = E B by substituting X by 0 and Y by 1 (as X and Y were fresh). ◀