<figure><img src="image_1.png" /></figure>

HAL
open science

# Type Isomorphisms for Multiplicative-Additive Linear Logic

Rémi Di Guardia, Olivier Laurent

<figure><img src="image_2.png" /></figure>

To cite this version:

Rémi Di Guardia, Olivier Laurent. Type Isomorphisms for Multiplicative-Additive Linear Logic. Logical Methods in Computer Science, 2025, 21 (4), 10.46298/lmcs-21(4:24)2025. hal-04460547v3

HAL Id: hal-04460547

https://hal.science/hal-04460547v3

Submitted on 24 Nov 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_3.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# TYPE ISOMORPHISMS FOR MULTIPLICATIVE-ADDITIVE LINEAR LOGIC

RÉMI DI GUARDIA AND OLIVIER LAURENT

Univ Lyon, EnsL, UCBL, CNRS, LIP, F-69342, LYON Cedex 07, France
e-mail address: remi.di.guardia@ens-lyon.org, olivier.laurent@ens-lyon.fr

**ABSTRACT.** We characterize type isomorphisms in the multiplicative-additive fragment of linear logic (MALL), and thus in ★-autonomous categories with finite products, extending a result for the multiplicative fragment by Balat and Di Cosmo [BDC99]. This yields a much richer equational theory involving distributivity and cancellation laws. The unit-free case is obtained by relying on the proof-net syntax introduced by Hughes and Van Glabbeek [HvG05]. We use the sequent calculus to extend our results to full MALL, including all units, thanks to a study of cut-elimination and rule commutations.

## 1. 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, denoted *A* ≅ *B*, if there exist morphisms *A* $\xrightarrow{f}$ *B* and *B* $\xrightarrow{g}$ *A* such that $f \circ g = \text{id}_B$ and $g \circ f = \text{id}_A$; i.e. if the following diagram commutes:

<figure><img src="image_4.png" /></figure>

The arrows *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 \times B \simeq B \times A$, $(A \times B) \times C \simeq A \times (B \times C)$ and $A \times \top \simeq 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 $\lambda x: B.(M(Nx)) =_{\beta\eta} \lambda x: B.x$ and $\lambda x: A.(N(Mx)) =_{\beta\eta} \lambda x: A.x$ where $=_{\beta\eta}$ is βη-equality. This corresponds to isomorphic objects in the syntactic category generated by terms up to $=_{\beta\eta}$. Similarly, type isomorphisms can also be considered in

<figure><img src="image_5.png" /></figure>

<footnote>*Key words and phrases:* Linear Logic, Type Isomorphisms, Multiplicative-Additive fragment, Proof-nets, Ssequent calculus, Star-autonomous categories with finite products.</footnote>

<footnote>* The present paper is a revised and extended version of [DGL23], supplying all proofs and with a different organization.</footnote>
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 [Sol83, DP97], λ-calculus [DC95] and proof theory [BDC99]. Knowing exactly the isomorphisms of a theory matters for (at least) two reasons. First is a semantic motivation: isomorphic objects are those that cannot be distinguished by the theory, making isomorphisms central in category theory – e.g. unicity of a limit holds only up to isomorphism. A natural question is then what is the quotient implicitly done by all these results with an “up to isomorphism”, which then allows one for instance to look only at representatives of these equivalence classes. Second, isomorphisms in a theory are often, but not always, those expected: e.g. in a compact close category with finite products, these products are in fact biproducts [Hou08]. Furthermore, type isomorphisms have been used to develop practical tools, such as search in a library of a functional programming language [Rit91, ARG21].

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 $\mathcal{T}$ is called *sound* with respect to type isomorphisms if types equal up to $\mathcal{T}$ are isomorphic. It is said *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 [FDCB02].

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 one 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 [Sol83, Lau05] 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 [DC95, BDC99]. The more easily the equality ($=_{\beta\eta}$ 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) [Gir87], 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 ($\otimes$ and $\&$), of disjunction ($\not\wedge$ and $\oplus$), of true (1 and $\top$) and of false ($\bot$ and 0). The exponential family is constituted of two modalities ! and ? bridging the gap between multiplicatives and additives through four isomorphisms !($A \& B$) $\simeq!$!$A \otimes!B$, ?($A \oplus B$) $\simeq?$!$A \not\wedge?B$, $!\top \simeq 1$ and ?0 $\simeq \bot$. In the multiplicative fragment (MLL) of LL (using only $\otimes$, $\not\wedge$, 1 and $\bot$, and corresponding to $\star$-autonomous categories), the question of type isomorphisms was answered positively using a syntactic method based on proof-nets by Balat and Di Cosmo [BDC99]:
<table><caption>Table 1: Type isomorphisms in multiplicative-additive linear logic</caption><thead><tr><th colspan="6">AC</th></tr><tr><th>Associativity</th><th>Commutativity</th><th>Distributivity</th><th>Unitality</th><th>Cancellation</th></tr></thead><tbody><tr><td>A ⊗ (B ⊗ C) = (A ⊗ B) ⊗ C</td><td>A ⊗ B = B ⊗ A</td><td>A ⊗ (B ⊕ C) = (A ⊗ B) ⊕ (A ⊗ C)</td><td>A ⊗ 1 = A</td><td>A ⊗ 0 = 0</td></tr><tr><td>A ⊗ (B ⊗ C) = (A ⊗ B) ⊗ C</td><td>A ⊗ B = B ⊗ A</td><td>A ⊗ (B &amp; C) = (A ⊗ B) &amp; (A ⊗ C)</td><td>A ⊗ ⊥ = A</td><td>A ⊗ ⊤ = ⊤</td></tr><tr><td>A ⊕ (B ⊕ C) = (A ⊕ B) ⊕ C</td><td>A ⊕ B = B ⊕ A</td><td></td><td>A ⊕ 0 = A</td><td></td></tr><tr><td>A &amp; (B &amp; C) = (A &amp; B) &amp; C</td><td>A &amp; B = B &amp; A</td><td></td><td>A &amp; ⊤ = A</td><td></td></tr></tbody></table>

isomorphisms emerge from associativity and commutativity of the multiplicative connectives ⊗ and ⨯, as well as unitality 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 [Lau05]. It is conjectured that isomorphisms in full LL correspond to those in its polarized fragment (constituted of the equations on 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. This applies at the same time to the class of ⋆-autonomous categories with finite products (whose corresponding equational theory in its usual syntax is in Table 7 on page 52). This situation is much richer than in the multiplicative fragment since isomorphisms include not only associativity, commutativity and unitality, but also the distributivity of the multiplicative connective ⊗ (resp. ⨯) over the additive ⊕ (resp. &amp;) as well as the associated cancellation law for the additive unit 0 (resp. ⊤) over the multiplicative connective ⊗ (resp. ⨯). Remark also that the &amp; and the ⊕ (corresponding to the categorical product and sum) do not distribute, contrary to what happens for instance in cartesian closed categories.

Using a semantic approach for completeness looks difficult here. In particular, most of the known “concrete” models of MALL (with the meaning that isomorphisms are more easily computed inside) immediately come with unwanted isomorphisms not valid in the syntax. For example, one can check that ⊤ ⊗ A ≅ ⊤ in coherent spaces [Gir87], while it is plainly obvious that ⊤ ⊗ A ≁ ⊤ in the syntax as the second formula is provable but generally the first one is not. An idea would then be to consider less “concrete” models of MALL or of ⋆-autonomous categories with finite products, typically categories built in a natural way over MLL or ⋆-autonomous categories. For instance, one could consider the free completion by products and coproducts of ⋆-autonomous categories, hoping the resulting category corresponds to MALL – in the same spirit as what has been done for bicompletion of ⋆-autonomous categories [Joy95a, Joy95b], except MALL should not be the free bicompletion of MLL as it is not expected to have all limits. Or one could consider models based on coherence spaces such as [HJ97, HJ99, BHS05]. We see two main difficulties with this approach. The first is that isomorphisms may not be that easy to compute in these categories, and we lack results giving isomorphisms of a completion from isomorphisms of the base category. Especially in our case, where we have distributivity isomorphisms involving both multiplicative and additive connectives, meaning isomorphisms of multiplicative-additive linear logic are not directly deducible from those of multiplicative linear logic and of additive linear logic. The second obstacle is that these categories may not correspond exactly to MALL, and can have unwanted isomorphisms. In particular, models built following coherence spaces contain the same unwanted ⊤ ⊗ A ≅ ⊤.
For this reason we prefer to use a syntactic method, and follow the approach from Balat and Di Cosmo [BDC99] based on proof-nets [Gir96]. Indeed, proof-nets provide a very good syntax for linear logic where it is very natural to study properties such as composition of proofs by cut, cut-elimination and identity of proofs. All these highly simplify the problem of isomorphisms. However, already in [BDC99] 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. Indeed, the main result from [HH16a] rules out “simple” canonical proof-nets with multiplicative units, as using such graphs one can solve a PSPACE-complete problem. Nonetheless, if one forgets the canonical requirement for the units, some nice definitions for MLL exist, e.g. [BCST96, Hug12], but one then has to consider such proof-nets up to an equivalence relation known as rewiring. Looking at additives, there are canonical proof-nets for additive linear logic with units [Hei11], but these proof-nets hardly seem expandable to multiplicative-additive linear logic with additive units. 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 [HvG05]. As a complement, proof-nets are not the only tool for considering canonical proofs. For instance, an approach based on focusing in sequent calculus is developed in [CMS08]; however, while it reduces the size of the equivalence class of a proof, there still are different but equivalent proofs.

**Sketch of the proof.** Our proof of completeness can be sketched as follows.

(1) A simple but key idea is to use the distributivity, unitality and cancellation equations of Table 1 from left to right so as to rewrite formulas into a *distributed* form, where none of these equations can be applied anymore. Between such distributed formulas, the only isomorphisms left should be associativity and commutativity ones. Furthermore, units should not play any special role. All the problem now is to prove this is the case.

(2) Working in sequent calculus, we prove that in any isomorphism between distributed formulas one can indeed replace units by fresh atoms and the resulting formulas are still isomorphic. The main difficulty here is that this only holds for distributed formulas, as generally units do not behave like atoms at all. This leads us to identify the following *patterns* in proofs of isomorphisms:

$$ \vdash \vdash, 0 \supset \frac{\vdash 1}{\vdash \perp, 1} \supseteq 1 $$

Once proven that unit rules are constrained to these patterns, it is easy to replace each of their uses by an *ax*-rule. A problem here is that we have to consider proofs up to cut-elimination, which is confluent only up to *rule commutation* [CP05, Theorem 5.1]. In particular, instead of the second pattern above, one must consider the following more general one, with a sequence of $\oplus_1$- and $\oplus_2$-rules between the 1- and $\perp$-rules, that turns the 1-formula into a more complex one $F$:

$$ \frac{\frac{\vdash 1}{\vdash = = \vdash} \supseteq_i \vdash F}{\vdash \perp, F} \perp $$

Moreover, we need two main steps to get these patterns.

(2a) First, we prove these patterns are in the identity proofs and are preserved by all rule commutations, so as to know the equivalence class of the identity has them.
This is done by giving properties preserved by rule commutations, with the tedious work of checking each rule commutation.

(2b) Then, we transpose these patterns backward through cut-elimination to get them in the proofs of isomorphisms. This needs a detailed study to prove that cutting proofs of an isomorphism cannot “completely erase” a unit rule, i.e. that the behavior of erasing cases are quite constrained. We do so by a thorough consideration of the evolution of *slices* when eliminating a *cut*-rule, as well as a meticulous monitoring of *top*-rules during the reduction.

(3) Once the problem reduced to the unit-free case, we can transpose isomorphisms to proof-nets, so as to not have to bother with rule commutations and equivalence classes anymore. There, we prove that proof-nets associated to isomorphisms have very particular shapes, with local constraints on their axioms. More precisely, we prove that the three following configurations are forbidden: an axiom between atoms of a same formula, an atom with no axiom on it, and an atom with axioms to several distinct atoms.

<figure><img src="image_6.png" /></figure>

This means that proof-nets associated to an isomorphism $A \simeq B$ have the following general shape, with each atom of A linked to a unique atom of B by means of one or several axioms:

<figure><img src="image_7.png" /></figure>

This is the main challenge, because having such a shape is again only true for isomorphisms between distributed formulas, so we have to use this global property on distributed formulas in order to deduce a local property on the shape of axioms. We employ here the correctness criterion of Hughes & Van Glabbeek [HvG05] in a direct way. The idea is to prove that a forbidden configuration, typically the third one, implies having in one formula a & being an ancestor of a $\mathcal{Y}$. The distributivity hypothesis then gives a $\otimes$- or $\oplus$-vertex between these two, thanks to which a cycle contradicting the correctness criterion can be built. This crucial part of the proof seems very hard to transpose in sequent calculus as it hinges on a geometric reasoning, and even if it were possible we would expect some heavy work on rule commutations, turning this already complicated proof into an utterly bewildering one.

(4) Knowing that proof-nets have very specific shapes, we recognize they correspond only to a rearrangement of formulas because axioms bind an atom of a formula with one of the isomorphic formula in a bijective fashion. This is enough to finally conclude that the only isomorphisms are associativity and commutativity ones.
**Outline.** Once the necessary definitions given (Section 2), our proof of the completeness of the equational theory of Table 1 goes in two main steps. First, we work in the sequent calculus to simplify the problem and reduce it to the unit-free fragment, by lack of a good-enough notion of proof-nets for MALL including units. This goes through a characterization of the equality of proofs up to axiom-expansion and cut-elimination by means of rule commutations, using a result from [CP05] (Sections 3 and 4). This allows us to analyze the behavior of units inside isomorphisms so as to conclude that they can be replaced with fresh atoms, once formulas are simplified appropriately (Section 5, and points (1) and (2) of the sketch above). Secondly, being in a setting admitting proof-nets, we adapt the proof of Balat & Di Cosmo [BDC99] to the framework of Hughes & Van Glabbeek's proof-nets [HvG05]. We transpose the definition of isomorphisms to this new syntax (Sections 6 and 7), then prove completeness (Section 8, and points (3) and (4) of the sketch above). This last step is the core of the work and 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 sub-formulas can be duplicated through distributivity equations, breaking a linearity property crucial in [BDC99].

Finally, seeing MALL as a category, we extend our result to conclude that Table 1 (or more precisely its adaptation to the language of categories, Table 7 on page 52) provides the equational theory of isomorphisms valid in all $\star$-autonomous categories with finite products (Section 9). We solve the situation of symmetric monoidal closed categories with finite products as well.

We are quite exhaustive on notions in sequent calculus. An informed reader could skip these basic definitions and results, and start reading directly from Section 5 on page 19.

## 2. DEFINITIONS

In this section are first defined formulas and proofs of multiplicative-additive linear logic (Section 2.1). Then are introduced the standard operations on these sequent calculus proofs: axiom-expansion, cut-elimination and rule commutations (Section 2.2). This finally leads to the definition of type isomorphisms for this logic (Section 2.3).

**2.1. Multiplicative-Additive Linear Logic.** The multiplicative-additive fragment of linear logic [Gir87], denoted by MALL, has formulas given by the following grammar, where $X$ belongs to a given enumerable set of atoms:

$$A, B ::= X \mid X^{\perp} \mid A \otimes B \mid A \not\cong B \mid 1 \mid \perp \mid A \& B \mid A \oplus B \mid \top \mid 0$$

Orthogonality ($\perp$)$^\perp$ expands into an involution on arbitrary formulas through $X^{\perp\perp} = X$, $1^{\perp} = \perp$, $\perp^{\perp} = 1$, $\top^{\perp} = 0$, $0^{\perp} = \top$ and De Morgan's laws $(A \otimes B)^{\perp} = B^{\perp} \not\cong A^{\perp}$, $(A \not\cong B)^{\perp} = B^{\perp} \otimes A^{\perp}$, $(A \& B)^{\perp} = B^{\perp} \oplus A^{\perp}$, $(A \oplus B)^{\perp} = B^{\perp} \& A^{\perp}$. We choose the *non-commutative* De Morgan's laws for duality because this will often result in planar graphs on our illustrations, with axiom links not crossing each others (e.g. in the identity proof-net, see Figure 4 on page 38). These non-commutative De Morgan's laws have been used for instance in the context of cyclic linear logic where this leads to planar proof-nets [AM98].

The size $s(A)$ of a formula $A$ is defined as its number of connectives $\otimes$, $\not\cong$, $\&$ and $\oplus$, plus its number of units $1$, $\perp$, $\top$ and $0$ and of atoms and negated atoms (counting occurrences).
Sequents are lists of formulas of the form $\vdash A_1, \dots, A_n$. Sequent calculus rules are, with $A$ and $B$ arbitrary formulas, $\Gamma$ and $\Delta$ contexts (i.e. lists of formulas) and $\sigma$ a permutation:

$$ \begin{array}{ccc} \overline{\vdash A^{\perp}, A} & ax & \overline{\vdash \Gamma} \quad \overline{\vdash \sigma(\Gamma)} \quad ex \qquad \overline{\vdash A, \Gamma} \quad \overline{\vdash A^{\perp}, \Delta} \quad \overline{\vdash \Gamma, \Delta} \quad cut \\ \overline{\vdash A, \Gamma} \quad \overline{\vdash B, \Delta} \quad \otimes & \overline{\vdash A, B, \Gamma} \quad \overline{\vdash A \not\sim B, \Gamma} \quad \not\sim B & \overline{\vdash 1} \quad 1 \qquad \overline{\vdash \Gamma} \quad \overline{\vdash \perp, \Gamma} \quad \perp \\ \overline{\vdash A, \Gamma} \quad \overline{\vdash B, \Gamma} \quad \& & \overline{\vdash A, \Gamma} \quad \overline{\vdash A \oplus B, \Gamma} \quad \oplus 1 & \overline{\vdash B, \Gamma} \quad \overline{\vdash A \oplus B, \Gamma} \quad \oplus 2 \qquad \overline{\vdash \top, \Gamma} \quad \top \end{array} $$

In practice, we consider exchange rules (ex) as incorporated in the conclusion of the rule above, thus dealing with rules like: $\overline{\vdash A, B, \Gamma, \Delta} \quad \not\sim B$. In this spirit, by $\overline{\vdash \Gamma, A, B, \Delta} \quad \not\sim B$ we mean that the appropriate permutation is also incorporated in the rule above. Equivalently, we only consider proofs with exactly one exchange rule below each non-exchange rule.

The main difference with the multiplicative fragment of linear logic (MLL) is the `&-rule`, which introduces some sharing of the context $\Gamma$. From this comes the notion of a *slice* [Gir87, Gir96] which is a partial proof missing some additive component.

**Definition 2.1** (Slice). For $\pi$ a proof, consider the (non-correct) proof tree obtained by deleting one of the two sub-trees of each `&-rule` of $\pi$ (thus, in the new proof tree, `&-rules are unary):

$$ \frac{\vdash A, \Gamma \quad \&_1}{\vdash A \& B, \Gamma} $$

The remaining rules form a *slice* of $\pi$. We denote by $S(\pi)$ the set of slices of $\pi$.

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.

By *unit-free MALL*, we mean the restriction of MALL to formulas not involving the units $1, \perp, \top$ and $0$, and as such without the $1, \perp$ and $\top$-rules. When speaking of a *positive* formula, we mean a formula with main connective $\otimes$ or $\oplus$, a unit $1$ or $0$, or an atom $X$. A *negative* formula is one with main connective $\not\sim$ or `&`, a unit $\perp$ or $\top$, or a negated atom $X^{\perp}$.

## 2.2. Transformations of proofs.
There are two well-known rewriting relations on proofs, *axiom-expansion* and *cut-elimination*. These transformations correspond respectively to $\eta$-expansion and $\beta$-reduction in the $\lambda$-calculus, hence the notations in the following definitions.

**Definition 2.2.** We call *axiom-expansion* the rewriting system $\xrightarrow{\eta}$ described in Table 2.

**Definition 2.3.** We call *cut-elimination* the rewriting system $\xrightarrow{\beta}$ described in Tables 3 and 4 (up to permuting the two branches of any *cut*-rule).

**Remark 2.4.** Another possible $\not\sim \mathcal{Y} - \otimes$ key case for cut-elimination would be the following:

$$ \frac{\pi_1 \qquad \pi_2}{\vdash A, \Gamma \qquad \vdash B, \Delta \qquad \otimes \qquad \overline{\vdash B^{\perp}, A^{\perp}, \Sigma} \qquad \not\sim B} \qquad \overline{\vdash \Gamma, \Delta, \Sigma} \qquad \not\sim B \qquad \beta \qquad \overline{\vdash A, \Gamma \qquad \vdash B^{\perp}, A^{\perp}, \Sigma} \qquad \overline{\vdash \Gamma, \Delta, \Sigma} \qquad \overline{\vdash B^{\perp}, \Gamma, \Sigma} \qquad \overline{\vdash \Gamma, \Delta, \Sigma} \qquad cut $$

This case can be simulated with the given $\not\sim \mathcal{Y} - \otimes$ key case and a *cut-cut* commutative case.
Another relation on proofs is *rule commutation*, which is closely related to cut-elimination as proved in [CP05]. These commutations associate proofs which differ only by the order in which their rules are applied.

**Definition 2.5.** We call *rule commutation* the symmetric relation $|\vdash^r|$ described in Tables 5 and 6. This corresponds to rule commutations in *cut-free MALL*, i.e. with no *cut-rules* above the commutation (there may be *cut-rules* below). In particular, in a $\vdash - \otimes$ commutation we assume the created or erased sub-proof to be cut-free, and in a $\& - \otimes$ commutation the duplicated or superimposed sub-proof to be cut-free.

The restriction of rule commutations in a cut-free setting is important. First, this choice is more appropriate for our purposes as it has fewer cases and corresponds to the equivalence relation between normal forms, namely cut-free proofs. Second, it is crucial for the $\& - \otimes$ commutation: while there is no such restriction in [CP05], their proof contains a mistake that can be patched up thanks to this restriction (more details are given in Section 4 and a corrected proof is written in Appendix A).

**Remark 2.6.** A more general theory of rule commutations exists, without the restriction on cut-free proofs and with commutations involving the *cut-rule*, the latter being the symmetric closure of the commutative cases of cut-elimination in Table 4. See [HvG16] for these commutations in unit-free MALL (and also with the *mix-rule*).

**Remark 2.7.** Looking at the commutative cut-elimination cases, as well as rule commutations, there is no commutation with *ax-* and 1-rules because these rules have no context. For there is no rule for 0, there is no commutation with 0 nor a $\vdash - 0$ key cut-elimination case.

We denote the reflexive transitive closure of $\xrightarrow{\eta} (\text{resp. } \xrightarrow{\beta}, |\vdash^r|)$ by $\xrightarrow{\eta^*} (\text{resp. } \xrightarrow{\beta^*}, |\vdash^r|)$. By $\xrightarrow{\beta^n}$ we mean a sequence of $n \xrightarrow{\beta}$ steps, and similarly for $\xrightarrow{\eta}$. Because of the analogy with the $\lambda$-calculus and since there will be no ambiguity, we use the notation $=_{\beta\eta}$ for equality of proofs up to cut-elimination ($\beta$) and axiom-expansion ($\eta$). Similarly, $=_{\beta}$ is equality up to cut-elimination only.

**2.3. Linear isomorphisms.** We denote by $\pi \bowtie_B \pi'$ the proof obtained by adding a cut on $B$ between proofs $\pi$ with conclusion $\vdash \Gamma, B$ and $\pi'$ with conclusion $\vdash B^\perp, \Delta$, and by $ax_A$ the proof of $\vdash A^\perp, A$ containing just an *ax-rule*.

**Definition 2.8 (Isomorphism).** Two formulas $A$ and $B$ are *isomorphic*, denoted $A \simeq B$, if there exist proofs $\pi$ of $\vdash A^\perp, B$ and $\pi'$ of $\vdash B^\perp, A$ such that $\pi \bowtie_B \pi' =_{\beta\eta} ax_A$ and $\pi' \bowtie_A \pi =_{\beta\eta} ax_B$:

$$ \pi \bowtie_B \pi' = \frac{\begin{array}{c} \pi \\ \vdash A^\perp, B \end{array} \quad \begin{array}{c} \pi' \\ \vdash B^\perp, A \end{array}}{\vdash A^\perp, A} \quad \text{cut} =_{\beta\eta} \overline{\vdash A^\perp, A} \quad ax = ax_A $$ 
and

$$ \pi' \bowtie_A \pi = \frac{\begin{array}{c} \pi' \\ \vdash B^\perp, A \end{array} \quad \begin{array}{c} \pi \\ \vdash A^\perp, B \end{array}}{\vdash B^\perp, B} \quad \text{cut} =_{\beta\eta} \overline{\vdash B^\perp, B} \quad ax = ax_B $$
By $A \overset{\pi,\pi'}{\cong} B$ we mean the *cut-free* proofs $\pi$ and $\pi'$ define an isomorphism between formulas $A$ and $B$, that is $\pi$ is a proof of $\vdash A^{\perp}, B$ and $\pi'$ one of $\vdash B^{\perp}, A$ such that $\pi \overset{B}{\dashv} \pi' =_{\beta\eta} \mathrm{ax}_A$ and $\pi \overset{A}{\dashv} \pi' =_{\beta\eta} \mathrm{ax}_B$. It is quite easy to link these two notations of isomorphisms.

**Lemma 2.9.** Given two formulas $A$ and $B$, $A \cong_B B$ if and only if there exist proofs $\pi$ and $\pi'$ such that $A \cong_B B$.

*Proof.* The converse way follows by definition of an isomorphism. For the direct way, take proofs $\pi$ and $\pi'$ given by the definition of an isomorphism, not necessarily cut-free. One may eliminate all *cut*-rules inside, using weak normalization of cut-elimination $\beta \to$ (Corollary A.11). $\square$

We aim to prove that two MALL formulas are isomorphic if and only if they are equal in the equational theory $\mathcal{L}$ defined as follows, with $\mathcal{AC}$ a smaller equational theory to which we will reduce the problem.

**Definition 2.10** (Equational theories $\mathcal{L}$ and $\mathcal{AC}$). We denote by $\mathcal{L}$ the equational theory given on Table 1 on page 3, while $\mathcal{AC}$ denotes the part with associativity and commutativity equations only.

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

**Theorem 2.11** (Isomorphisms soundness, see [Lau05, Lemma 3]). If $A \stackrel{\mathcal{L}}{=} B$ then $A \cong_B B$.

*Proof.* It suffices to give the proofs for each equation, then check their compositions can be reduced by cut-elimination to an axiom-expansion of an $ax$-rule. For instance, looking at the commutativity of $\mathcal{N}$, i.e. $A \mathcal{N} B \cong_B A \mathcal{N} A$, we set $\pi$ and $\pi'$ the following proofs:

$$ \pi = \frac{\overline{\vdash B^{\perp}, B} \quad ax \quad \overline{\vdash A^{\perp}, A} \quad ax}{\overline{\vdash B^{\perp} \otimes A^{\perp}, B, A} \quad \mathcal{N}} \otimes \quad \text{and} \quad \pi' = \frac{\overline{\vdash A^{\perp}, A} \quad ax \quad \overline{\vdash B^{\perp}, B} \quad ax}{\overline{\vdash A^{\perp} \otimes B^{\perp}, A, B} \quad \mathcal{N}} \otimes \frac{\overline{\vdash A^{\perp} \otimes B^{\perp}, A \mathcal{N} B} \quad \mathcal{N}}{\overline{\vdash A^{\perp} \otimes B^{\perp}, A \mathcal{N} B}} $$

One can check

$$ \begin{array}{ccc} \pi & \pi' & \text{cut} \\ \overline{\begin{array}{c} \vdash B^{\perp} \otimes A^{\perp}, B \mathcal{N} A \\ \vdash B^{\perp} \otimes A^{\perp}, A \mathcal{N} B \end{array}} & \overline{\begin{array}{c} \vdash A^{\perp} \otimes B^{\perp}, A \mathcal{N} B \\ \vdash A^{\perp} \otimes B^{\perp}, A \mathcal{N} B \end{array}} & \text{cut} \\ & \xrightarrow{\beta^*} & \\ \overline{\begin{array}{c} \vdash B^{\perp} \otimes A^{\perp}, A \mathcal{N} B \end{array}} & ax & \xrightarrow{\eta} \overline{\begin{array}{c} \vdash B^{\perp}, B \quad ax \quad \overline{\begin{array}{c} \vdash A^{\perp}, A \quad ax \\ \vdash B^{\perp} \otimes A^{\perp}, A, B \end{array}} \otimes \\ \vdash B^{\perp} \otimes A^{\perp}, A \mathcal{N} B \end{array}} \mathcal{N} \end{array} $$

and
<table><caption>Table 2: Axiom-expansion in sequent calculus (up to a permutation of the conclusion)</caption><tr><td>Y - ⊗</td><td>ax</td><td>η</td><td>ax<br>ax<br>⊗</td></tr><tr><td></td><td>ax</td><td>η</td><td>ax<br>ax<br>⊗</td></tr><tr><td>& - ⊕</td><td>ax</td><td>η</td><td>ax<br>ax<br>⊗</td></tr><tr><td>⊥ - 1</td><td>ax</td><td>η</td><td>⊥</td></tr><tr><td>⊤ - 0</td><td>ax</td><td>η</td><td>⊤</td></tr></table>

<table><caption>Table 3: Cut-elimination in sequent calculus – key cases (up to a permutation of the conclusion)</caption><tr><td>ax</td><td>ax<br>ax<br>π</td><td>ax<br>ax<br>β</td><td>ax<br>ax<br>π</td></tr><tr><td>Y - ⊗</td><td>ax<br>ax<br>π</td><td>ax<br>ax<br>β</td><td>ax<br>ax<br>π</td></tr><tr><td>& - ⊕<sub>1</sub></td><td>ax<br>ax<br>π</td><td>ax<br>ax<br>β</td><td>ax<br>ax<br>π</td></tr><tr><td>& - ⊕<sub>2</sub></td><td>ax<br>ax<br>π</td><td>ax<br>ax<br>β</td><td>ax<br>ax<br>π</td></tr><tr><td>⊥ - 1</td><td>ax<br>ax<br>π</td><td>ax<br>ax<br>β</td><td>ax<br>ax<br>π</td></tr></table>
<table><caption>Table 4: Cut-elimination in sequent calculus – commutative cases (up to a permutation of the conclusion)</caption><tbody><tr><td>Y - cut</td><td>π₁<br>|- A, B, C, Γ<br>|- A, B, Y C, Γ<br>Y<br>|- A, B, C, Γ<br>|- B, Y C, Γ, Δ</td><td>π₂<br>|- A, B, C, Γ<br>|- A, B, C, Γ, Δ<br>Y<br>|- A, B, C, Γ, Δ</td><td>β<br>|- A, B, C, Γ<br>|- A, B, C, Γ, Δ<br>Y<br>|- A, B, C, Γ, Δ</td><td>π₁<br>π₂<br>|- A, B, C, Γ<br>|- A, B, C, Γ, Δ<br>Y<br>|- A, B, C, Γ, Δ</td></tr><tr><td>⊗ - cut - 1</td><td>π₁<br>|- A, B, Γ<br>|- A, B, Γ, Δ<br>Y<br>|- A, B, Γ, Δ<br>|- B, Γ, Δ, Σ</td><td>π₂<br>|- A, B, Γ<br>|- A, B, Γ, Δ<br>Y<br>|- A, B, Γ, Δ<br>|- B, Γ, Δ, Σ</td><td>π₃<br>|- A, B, Γ<br>|- A, B, Γ, Δ<br>Y<br>|- A, B, Γ, Δ<br>|- B, Γ, Δ, Σ</td><td>π₁<br>π₂<br>|- A, B, Γ<br>|- A, B, Γ, Δ<br>Y<br>|- A, B, Γ, Δ<br>|- B, Γ, Δ, Σ</td></tr><tr><td>⊗ - cut - 2</td><td>π₁<br>|- B, Γ<br>|- B, Γ, Δ<br>Y<br>|- B, Γ, Δ<br>|- B, Γ, Δ, Σ</td><td>π₂<br>|- B, Γ<br>|- B, Γ, Δ<br>Y<br>|- B, Γ, Δ<br>|- B, Γ, Δ, Σ</td><td>π₃<br>|- B, Γ<br>|- B, Γ, Δ<br>Y<br>|- B, Γ, Δ<br>|- B, Γ, Δ, Σ</td><td>π₁<br>π₂<br>|- B, Γ<br>|- B, Γ, Δ<br>Y<br>|- B, Γ, Δ<br>|- B, Γ, Δ, Σ</td></tr><tr><td>& - cut</td><td>π₁<br>|- A, B, Γ<br>|- A, B, Γ<br>Y<br>|- A, B, Γ, Δ<br>|- B, Γ, Δ, Σ</td><td>π₂<br>|- A, B, Γ<br>|- A, B, Γ, Δ<br>Y<br>|- A, B, Γ, Δ<br>|- B, Γ, Δ, Σ</td><td>π₃<br>|- A, B, Γ<br>|- A, B, Γ, Δ<br>Y<br>|- A, B, Γ, Δ<br>|- B, Γ, Δ, Σ</td><td>π₁<br>π₂<br>|- A, B, Γ<br>|- A, B, Γ, Δ<br>Y<br>|- A, B, Γ, Δ<br>|- B, Γ, Δ, Σ</td></tr><tr><td>⊕₁ - cut</td><td>π₁<br>|- A, B₁, Γ<br>|- A, B₁ ⊕ B₂, Γ<br>Y<br>|- B₁ ⊕ B₂, Γ, Δ</td><td>π₂<br>|- A, B₁, Γ<br>|- A, B₁ ⊕ B₂, Γ, Δ<br>Y<br>|- B₁ ⊕ B₂, Γ, Δ</td><td>π₃<br>|- A, B₁, Γ<br>|- A, B₁ ⊕ B₂, Γ, Δ<br>Y<br>|- B₁ ⊕ B₂, Γ, Δ</td><td>π₁<br>π₂<br>|- A, B₁, Γ<br>|- A, B₁ ⊕ B₂, Γ, Δ<br>Y<br>|- B₁ ⊕ B₂, Γ, Δ</td></tr><tr><td>⊕₂ - cut</td><td>π₁<br>|- A, B₂, Γ<br>|- A, B₁ ⊕ B₂, Γ<br>Y<br>|- B₁ ⊕ B₂, Γ, Δ</td><td>π₂<br>|- A, B₂, Γ<br>|- A, B₁ ⊕ B₂, Γ, Δ<br>Y<br>|- B₁ ⊕ B₂, Γ, Δ</td><td>π₃<br>|- A, B₂, Γ<br>|- A, B₁ ⊕ B₂, Γ, Δ<br>Y<br>|- B₁ ⊕ B₂, Γ, Δ</td><td>π₁<br>π₂<br>|- A, B₂, Γ<br>|- A, B₁ ⊕ B₂, Γ, Δ<br>Y<br>|- B₁ ⊕ B₂, Γ, Δ</td></tr><tr><td>⊥ - cut</td><td>π₁<br>|- A, Γ<br>|- A, ⊥, Γ<br>Y<br>|- A, ⊥, Γ, Δ</td><td>π₂<br>|- A, Γ<br>|- A, ⊥, Δ<br>Y<br>|- A, ⊥, Γ, Δ</td><td>π₃<br>|- A, Γ<br>|- A, ⊥, Δ<br>Y<br>|- A, ⊥, Γ, Δ</td><td>π₁<br>π₂<br>|- A, Γ<br>|- A, ⊥, Δ<br>Y<br>|- A, ⊥, Γ, Δ</td></tr><tr><td>⊤ - cut</td><td>π₁<br>|- A, ⊤, Γ<br>|- A, ⊤, Δ<br>Y<br>|- A, ⊤, Γ, Δ</td><td>π₂<br>|- A, ⊤, Δ<br>Y<br>|- A, ⊤, Γ, Δ</td><td>π₃<br>|- A, ⊤, Δ<br>Y<br>|- A, ⊤, Γ, Δ</td><td>π₁<br>π₂<br>|- A, Γ<br>|- A, ⊤, Δ<br>Y<br>|- A, ⊤, Γ, Δ</td></tr><tr><td>cut - cut</td><td>π₁<br>|- A, B, Γ<br>|- A, B, Γ, Δ<br>Y<br>|- A, B, Γ, Δ<br>|- B, Γ, Δ, Σ</td><td>π₂<br>|- A, B, Γ<br>|- A, B, Γ, Δ<br>Y<br>|- A, B, Γ, Δ<br>|- B, Γ, Δ, Σ</td><td>π₃<br>|- A, B, Γ<br>|- A, B, Γ, Δ<br>Y<br>|- A, B, Γ, Δ<br>|- B, Γ, Δ, Σ</td><td>π₁<br>π₂<br>|- A, B, Γ<br>|- A, B, Γ, Δ<br>Y<br>|- A, B, Γ, Δ<br>|- B, Γ, Δ, Σ</td></tr></tbody></table>
$$ \begin{array}{ccc} \pi' & \pi & \\ \begin{array}{l} \vdash A^{\perp} \otimes B^{\perp}, A \not\Vdash B \\ \vdash A^{\perp} \otimes B^{\perp}, B \not\Vdash A \end{array} & \begin{array}{l} \vdash B^{\perp} \otimes A^{\perp}, B \not\Vdash A \\ \vdash A^{\perp} \otimes B^{\perp}, B \not\Vdash A \end{array} & \text{cut} \\ \\ \xrightarrow{\beta^*} & \frac{\begin{array}{l} \overline{\vdash A^{\perp}, A} \quad ax \\ \overline{\vdash B^{\perp}, B} \quad ax \end{array}}{\begin{array}{l} \vdash A^{\perp} \otimes B^{\perp}, B, A \\ \vdash A^{\perp} \otimes B^{\perp}, B \not\Vdash A \end{array}} \not\Vdash \\ \\ \xrightarrow{\eta} & \overline{\vdash A^{\perp} \otimes B^{\perp}, B \not\Vdash A} \quad ax & \square \end{array} $$

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

### 3. AXIOM-EXPANSION

The goal of this section is to reduce the study of isomorphisms to proofs with atomic axioms only, i.e. whose ax-rules are on a formula $A = X$ or $A = X^{\perp}$ (for $X$ an atom), no more considering axiom-expansion. Said in another manner, we restrict our study to proofs in normal form for the $\eta$ relation, so as to have only $=_{\beta}$ instead of $=_{\beta\eta}$ when considering isomorphisms.

To begin with, axiom-expansion is convergent.

**Proposition 3.1.** *Axiom-expansion* $\xrightarrow{\eta}$ *is strongly normalizing and confluent.*

*Proof.* Strong normalization follows from the fact that a $\xrightarrow{\eta}$ step strictly decreases the sum of the sizes of the formulas on which an ax-rule is applied.

Confluence can be deduced from the diamond property. Observe that two distinct steps $\tau \stackrel{\eta}{\leftrightarrow} \pi \stackrel{\eta}{\rightarrow} \phi$ always commute, i.e. there exists $\mu$ such that $\tau \xrightarrow{\eta} \mu \stackrel{\eta}{\leftrightarrow} \phi$ (there is no critical pair). Hence the diamond property of $\xrightarrow{\eta}$, thus its confluence. $\square$

**Remark 3.2.** As long as there is an ax-rule not on an atom, a $\xrightarrow{\eta}$ axiom-expansion step can be applied. Thus, atomic-axiom proofs correspond to proofs in normal form for $\xrightarrow{\eta}$.

Thanks to Proposition 3.1, we denote by $\eta(\pi)$ the unique $\eta$-normal form of a proof $\pi$, i.e. the proof obtained by expanding iteratively all ax-rules in $\pi$ (in any order thanks to confluence). Thus, we can define $\text{id}_A = \eta(\text{ax}_A)$, the axiom-expansion of the proof consisting of only one ax-rule. The goal of this section is to prove the following (proof on page 17).

**Proposition 3.3 (Reduction to atomic-axiom proofs).** Let $\pi$ and $\tau$ be proofs such that $\pi =_{\beta\eta} \tau$. Then $\eta(\pi) =_{\beta} \eta(\tau)$ with, in this sequence, only proofs in $\eta$-normal form.

This allows us to then consider proofs with atomic axioms only, manipulated through composition by cut and cut-elimination, never to speak again of $\eta$ rewriting.

We will need some intermediate results to reach our goal. We set $a(\pi \xrightarrow{\beta^*} \tau)$ the multiset of the sizes of the formulas in the ax key cases of these $\xrightarrow{\beta}$ reductions.

**Lemma 3.4.** Let $\pi$, $\tau$ and $\phi$ be proofs such that $\tau \stackrel{\beta}{\leftrightarrow} \pi \xrightarrow{\eta} \phi$. Then there exists $\mu$ such that $\tau \xrightarrow{\eta^*} \mu \stackrel{\beta}{\leftrightarrow} \phi$ or there exist $\mu_1$ and $\mu_2$ such that $\tau \xrightarrow{\eta^*} \mu_2 \stackrel{\beta^*}{\leftrightarrow} \mu_1 \stackrel{\eta^*}{\leftrightarrow} \phi$. Furthermore, $a(\phi \xrightarrow{\beta} \mu) = a(\pi \xrightarrow{\beta} \tau)$ in the first case and $a(\mu_1 \xrightarrow{\beta^*} \mu_2) < a(\pi \xrightarrow{\beta} \tau)$ in the second one. *Diagrammatically:*
<figure><img src="image_8.png" /></figure>

**Proof.** Call $r$ the $ax$-rule that $\pi \xrightarrow{\eta} \phi$ 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 $\mu$ such that $\phi \xrightarrow{\beta} \mu$ and $\tau \xrightarrow{\eta} \mu$ (or $\tau \xrightarrow{\eta} \phi \xrightarrow{\eta} \mu$ if $r$ belongs to a sub-proof duplicated by the $\xrightarrow{\beta}$ step, or $\tau = \mu$ if it belongs to a sub-proof erased by the $\xrightarrow{\beta}$ step). In particular, $a(\phi \xrightarrow{\beta} \mu) = a(\pi \xrightarrow{\beta} \tau)$ for they use the same rules.

Otherwise, the cut-elimination step is an $ax$ key case on $r$, with a cut-rule we call $c$ and a sub-proof $\rho$ in the other branch of $c$ than the one leading to $r$; $A$ is the formula cut by $c$. The reasoning we apply is depicted on Figure 1. Starting from $\phi$, consider the rules introducing $A^{\perp}$ in (all slices of) $\rho$. If any of them are $ax$-rules, then these are necessarily on the formula $A$; expand those $ax$-rules, in both $\phi$ and $\tau$ (keeping the same names for proofs $\pi$, $\tau$ and $\rho$ by abuse). Then, in $\phi$, commute the cut-rule $c$ with rules of $\rho$ until reaching the rules introducing $A^{\perp}$ in all slices (which are rules of the main connective of $A^{\perp}$ or $\top$-rules). Applying the corresponding key cases or $\top$-cut commutative case (first commuting with a rule of the expanded axiom $r$ if $A$ is a positive formula, and doing it after if $A$ is a negative formula), then the units or $ax$ key cases on strict sub-formulas of $A$ yield $\tau$. During these $ax$ key cases, we cut on sub-formulas of $A$, so on formulas of a strictly smaller size. Therefore
$$ \phi \xrightarrow{\eta^*} \beta^* \xrightarrow{\beta} \tau, \text{ with } a(\beta^* \xrightarrow{\beta} \cdot) < a(\pi \xrightarrow{\beta} \tau). \quad \square $$

**Fact 3.5.** Cut-elimination $\xrightarrow{\beta}$ preserves being in $\eta$-normal form.

**Lemma 3.6.** Let $\pi$, $\tau$ and $\phi$ be proofs such that $\tau \stackrel{\eta^*}{\leftarrow} \pi \xrightarrow{\beta^*} \phi$, with $\tau$ an $\eta$-normal proof. There exists an $\eta$-normal proof $\mu$ such that $\tau \xrightarrow{\beta^*} \mu \stackrel{\eta^*}{\leftarrow} \phi$. Diagrammatically:

<figure><img src="image_9.png" /></figure>

**Proof.** Assume $\tau \stackrel{\eta^m}{\leftarrow} \pi \xrightarrow{\beta^n} \phi$. If we find a $\mu$ respecting the diagram, then it is an $\eta$-normal form thanks to Fact 3.5. We reason by induction on the lexicographic order of the triple $(a(\pi \xrightarrow{\beta^*} \phi), n, m)$. If $n = 0$ or $m = 0$, then the result trivially holds ($\mu = \tau$ or $\mu = \phi$).

Consider the case $n+1$ and $m+1$. Therefore, $\tau \stackrel{\eta^n}{\leftarrow} \iota \stackrel{\eta}{\leftarrow} \pi \xrightarrow{\beta} \kappa \xrightarrow{\beta^n} \phi$. We apply Lemma 3.4 on $\iota \stackrel{\eta}{\leftarrow} \pi \xrightarrow{\beta} \kappa$, yielding $\rho$ such that $\iota \xrightarrow{\beta} \rho \stackrel{\eta^*}{\leftarrow} \phi$ with $a(\iota \xrightarrow{\beta} \rho) = a(\pi \xrightarrow{\beta} \kappa)$ or $\rho_1$ and $\rho_2$ such that $\iota \xrightarrow{\eta^*} \rho_1 \xrightarrow{\beta^*} \rho_2 \stackrel{\eta^*}{\leftarrow} \kappa$ with $a(\rho_1 \xrightarrow{\beta^*} \rho_2) < a(\pi \xrightarrow{\beta} \kappa)$. Both of these cases, and the reasoning we will apply, are illustrated by diagrams preceding them, with the following color convention: in blue are uses of Lemma 3.4, in green of confluence of $\xrightarrow{\eta}$ and in red of the induction hypothesis.
<figure><img src="image_10.png" /><figcaption>Figure 1: Schematic representation of the second case of the proof of Lemma 3.4</figcaption></figure>

<figure><img src="image_11.png" /></figure>

Assume to be in the first case. Applying the induction hypothesis on $\tau \stackrel{\eta^m}{\leftarrow} \iota \stackrel{\beta}{\rightarrow} \rho$, with $\tau$ in $\eta$-normal form, $a(\iota \stackrel{\beta}{\rightarrow} \rho) = a(\pi \stackrel{\beta}{\rightarrow} \kappa) \le a(\pi \stackrel{\beta^*}{\rightarrow} \phi)$, $1 \le n+1$ and $m < m+1$, there exists an $\eta$-normal proof $\nu$ such that $\tau \stackrel{\beta^*}{\rightarrow} \nu \stackrel{\eta^*}{\leftarrow} \rho$. We now apply the induction hypothesis
on $\nu \stackrel{\eta^*}{\rightleftharpoons} \rho \stackrel{\eta^*}{\rightleftharpoons} \kappa \stackrel{\beta^n}{\rightleftharpoons} \phi$, with $\nu$ in $\eta$-normal form, $a(\kappa \stackrel{\beta^n}{\rightleftharpoons} \phi) \le a(\pi \stackrel{\beta^*}{\rightleftharpoons} \phi)$ and $n < n + 1$. We obtain an $\eta$-normal proof $\mu$ such that $\nu \stackrel{\beta^*}{\rightleftharpoons} \mu \stackrel{\eta^*}{\rightleftharpoons} \phi$. This concludes the first case.

<figure><img src="image_12.png" /></figure>

Consider the second case. Using the confluence of $\stackrel{\eta}{\rightleftharpoons}$ on $\tau \stackrel{\eta^m}{\rightleftharpoons} \iota \stackrel{\eta^*}{\rightleftharpoons} \rho_1$ (Proposition 3.1), with $\tau$ in $\eta$-normal form, yields $\tau \stackrel{\eta^*}{\rightleftharpoons} \rho_1$. We then apply the induction hypothesis on $\tau \stackrel{\eta^*}{\rightleftharpoons} \rho_1 \stackrel{\beta^*}{\rightleftharpoons} \rho_2$, with $\tau$ in $\eta$-normal form and $a(\rho_1 \stackrel{\beta^*}{\rightleftharpoons} \rho_2) < a(\pi \stackrel{\beta^*}{\rightleftharpoons} \phi)$. This yields an $\eta$-normal proof $\nu$ such that $\tau \stackrel{\beta^*}{\rightleftharpoons} \nu \stackrel{\eta^*}{\rightleftharpoons} \rho_2$. We use the induction hypothesis again, this time on $\nu \stackrel{\eta^*}{\rightleftharpoons} \rho_2 \stackrel{\eta^*}{\rightleftharpoons} \kappa \stackrel{\beta^n}{\rightleftharpoons} \phi$, with $\nu$ in $\eta$-normal form, $a(\kappa \stackrel{\beta^n}{\rightleftharpoons} \phi) \le a(\pi \stackrel{\beta^*}{\rightleftharpoons} \phi)$ and $n < n + 1$. We obtain an $\eta$-normal proof $\mu$ with $\nu \stackrel{\beta^*}{\rightleftharpoons} \mu \stackrel{\eta^*}{\rightleftharpoons} \phi$, solving the second case. $\square$

We can now prove the main result of this section, Proposition 3.3.

*Proof of Proposition 3.3.* We reason by induction on the length of the sequence $\pi =_{\beta\eta} \tau$. If it is of null length, then $\pi = \tau$ hence $\eta(\pi) = \eta(\tau)$. Otherwise, there is a proof $\phi$ such that $\pi - \phi =_{\beta\eta} \tau$ with $\tau \in \{\stackrel{\beta}{\rightleftharpoons}; \stackrel{\beta}{\rightleftharpoons}; \stackrel{\eta}{\rightleftharpoons}; \stackrel{\eta}{\rightleftharpoons}\}$. By induction hypothesis, $\eta(\phi) =_{\beta} \eta(\tau)$, with only axiom-expanded proofs in this sequence. We distinguish cases according to $\pi - \phi$.

If $\pi \stackrel{\beta}{\rightleftharpoons} \phi$, then as $\eta(\pi) \stackrel{\eta^*}{\rightleftharpoons} \pi$ we can apply Lemma 3.6 to obtain an $\eta$-normal proof $\mu$ such that $\eta(\pi) \stackrel{\beta^*}{\rightleftharpoons} \mu \stackrel{\eta^*}{\rightleftharpoons} \phi$. Thus, $\mu = \eta(\phi)$, so $\eta(\pi) \stackrel{\beta^*}{\rightleftharpoons} \eta(\phi) =_{\beta} \eta(\tau)$ and the result holds (with only $\eta$-normal proofs in $\eta(\pi) \stackrel{\beta^*}{\rightleftharpoons} \eta(\phi)$ thanks to Fact 3.5).

Similarly, if $\pi \stackrel{\beta}{\rightleftharpoons} \phi$ then, as $\phi \stackrel{\eta^*}{\rightleftharpoons} \eta(\phi)$, there exists an $\eta$-normal proof $\mu$ such that $\pi \stackrel{\eta^*}{\rightleftharpoons} \mu \stackrel{\beta^*}{\rightleftharpoons} \eta(\phi)$ (Lemma 3.6). Thus $\mu = \eta(\pi)$, and $\eta(\pi) \stackrel{\beta^*}{\rightleftharpoons} \eta(\phi) =_{\beta} \eta(\tau)$.

Finally, if $\pi \stackrel{\eta}{\rightleftharpoons} \phi$ or $\pi \stackrel{\eta^*}{\rightleftharpoons} \phi$, then $\eta(\pi) = \eta(\phi) =_{\beta} \eta(\tau)$ and the conclusion follows. $\square$

## 4. CUT-ELIMINATION AND RULE COMMUTATIONS

It is not possible to apply the reasoning from the previous section (about axiom-expansion) to cut-elimination, because cut-elimination is confluent only up to rule commutations. In the literature of linear logic, there already are known results about (strong) normalization and confluence of cut-elimination but most are for the proof-nets syntax and not for the sequent calculus syntax: e.g. [HvG05, TdF03, TdF01, LM08] about multiplicative-additive linear
logic, [Acc13, DG99] about multiplicative-exponential linear logic, and notably [PTdF10] for all connectives and second order quantifiers. The confluence of cut-elimination up to rule commutations in sequent calculus is expected to hold in linear logic (with all connectives and units), but it has not been proved yet. Fortunately, in the restricted case of MALL, this key result has been proved [CP05, Theorem 5.1], which allows us to reduce the problem of isomorphisms from looking at cut-elimination to considering rule commutations.

A first, easy but important, result is that rule commutation is included in equality up to cut-elimination.

**Proposition 4.1** ($\vdash^r \subseteq =_\beta$). Given proofs $\pi$ and $\tau$, if $\pi \vdash^r \tau$ then $\pi =_\beta \tau$.

*Proof.* It suffices, for each commutation, to give a proof that can be reduced by cut elimination to both sides. We give here only a few representative cases.

* $C_{\&}^{\top}$ and $C_{\top}^{\&}$ commutations. The proof

$$ \frac{\frac{\vdash 0, \top \top \quad \frac{\vdash A_1, \top, \Gamma \top \quad \vdash A_2, \top, \Gamma \top}{\vdash A_1 \& A_2, \top, \Gamma} \&}{\vdash A_1 \& A_2, \top, \Gamma}$$

reduces to both

$$ \frac{\vdash A_1 \& A_2, \top, \Gamma \top}{\vdash A_1 \& A_2, \top, \Gamma} \top \quad \text{and} \quad \frac{\vdash A_1, \top, \Gamma \top}{\vdash A_1 \& A_2, \top, \Gamma} \top \& $$

according respectively to whether the *cut-rule* is first commuted with the $\top$-rule on its left or with the $\&$-rule on its right and then with the $\top$-rule on its left in both occurrences.

* $C_{\oplus i}^{\perp}$ and $C_{\perp i}^{\oplus}$ commutations. The proof

$$ \frac{\frac{\pi \quad \frac{\vdash A_i, \Gamma \quad \vdash A_i^{\perp}, A_i}{\vdash A_i, \perp, \Gamma \perp} \quad \frac{\vdash A_i^{\perp}, A_i}{\vdash A_i^{\perp}, A_1 \oplus A_2} \quad ax}{\vdash A_1 \oplus A_2, \perp, \Gamma} \oplus_i cut} $$

reduces to both

$$ \frac{\pi \quad \frac{\vdash A_i, \Gamma \quad \vdash A_1 \oplus A_2, \Gamma \oplus_i}{\vdash A_1 \oplus A_2, \perp, \Gamma \perp} \quad ax}{\vdash A_1 \oplus A_2, \perp, \Gamma} \quad \text{and} \quad \frac{\pi \quad \frac{\vdash A_i, \Gamma \quad \vdash A_i, \perp, \Gamma \perp}{\vdash A_i, \perp, \Gamma \perp} \quad ax}{\vdash A_1 \oplus A_2, \perp, \Gamma} \quad \oplus_i cut $$

according respectively to whether the *cut-rule* is first commuted with the $\perp$-rule on its left or with the $\oplus_i$-rule on its right.

* $C_{\otimes}^{\otimes}$ commutations. The proof

$$ \frac{\frac{\pi_1 \quad \frac{\vdash A_1, \Gamma \quad \vdash A_2^{\perp}, A_2}{\vdash A_2^{\perp}, A_1 \otimes A_2, \Gamma} \quad ax}{\vdash A_1 \otimes A_2, B_1 \otimes B_2, \Gamma, \Delta, \Sigma} \quad \text{and} \quad \frac{\pi_2 \quad \frac{\vdash A_2, B_1, \Delta \quad \vdash B_2, \Sigma}{\vdash B_1 \otimes B_2, \Delta, \Sigma, A_2} \quad ax}{\vdash A_1 \otimes A_2, B_1 \otimes B_2, \Gamma, \Delta, \Sigma} \quad \text{cut}}{\vdash A_1 \otimes A_2, B_1 \otimes B_2, \Gamma, \Delta, \Sigma} $$

reduces to both

$$ \frac{\pi_1 \quad \frac{\pi_2 \quad \frac{\pi_3 \quad \frac{\pi_1 \quad \frac{\pi_2 \quad \frac{\pi_3 \quad \frac{\pi_1 \quad \pi_2}{\pi_1 \quad \pi_3}}{\pi_1 \quad \pi_2 \quad \pi_3}}{\pi_1 \quad \pi_2 \quad \pi_3}}{\pi_1 \quad \pi_2 \quad \pi_3}}{\pi_1 \quad \pi_2 \quad \pi_3}}{\pi_1 \quad \pi_2 \quad \pi_3}}$$
soundness theorem, Theorem 2.11), and this isomorphism uses that 1 is unital for $\otimes$. Hence, we begin by reducing the problem to so-called *distributed formulas*, using the distributivity, unitality and cancellation equations of Table 1 on page 3 (Section 5.1). Then, for theses special formulas, we identify patterns containing units in proofs equal to an identity up to rule commutations, patterns which can be lifted to proofs of isomorphisms (Section 5.2). Finally, we prove that, in an isomorphism between distributed formulas, replacing units by fresh atoms preserves being an isomorphism, reducing the study of isomorphisms to distributed formulas in the unit-free fragment (Section 5.3).

## 5.1. Reduction to distributed formulas.

**Definition 5.1 (Distributed formula).** A formula is *distributed* if it does not have any sub-formula of the form

$$A \otimes (B \oplus C) \quad (A \oplus B) \otimes C \quad A \otimes 1 \quad 1 \otimes A \quad A \oplus 0 \quad 0 \oplus A \quad A \otimes 0 \quad 0 \otimes A$$

or their duals

$$(C \& B) \mathfrak{R} A \quad C \mathfrak{R} (B \& A) \quad \perp \mathfrak{R} A \quad A \mathfrak{R} \perp \quad \top \& A \quad A \& \top \quad \top \mathfrak{R} A \quad A \mathfrak{R} \top \\ \text{(where } A, B \text{ and } C \text{ are any formulas}).$$

**Remark 5.2.** This notion is stable under duality: if $A$ is distributed, so is $A^{\perp}$.

**Definition 5.3.** We call $\mathfrak{D}$ the following rewriting system on MALL formulas.

<table><thead><tr><th>A &otimes; (B &oplus; C) &rarr; (A &otimes; B) &oplus; (A &otimes; C)<br/>(A &oplus; B) &otimes; C &rarr; (A &otimes; C) &oplus; (B &otimes; C)</th><th>(C &oplus; B) &mathfrak{R} A &rarr; (C &mathfrak{R} A) &oplus; (B &mathfrak{R} A)<br/>C &mathfrak{R} (B &oplus; A) &rarr; (C &mathfrak{R} B) &oplus; (C &mathfrak{R} A)</th></tr></thead><tbody><tr><td>A &otimes; 1 &rarr; A<br/>A &oplus; 0 &rarr; A<br/>A &otimes; 0 &rarr; 0</td><td>1 &otimes; A &rarr; A<br/>0 &oplus; A &rarr; A<br/>0 &otimes; A &rarr; 0</td></tr></tbody></table><table><thead><tr><th>A &mathfrak{R} &perp; &rarr; A<br/>A &oplus; &top; &rarr; A<br/>A &mathfrak{R} &top; &rarr; &top;</th><th>&perp; &mathfrak{R} A &rarr; A<br/>&top; &oplus; A &rarr; A<br/>&top; &mathfrak{R} A &rarr; &top;</th></tr></thead><tbody><tr><td>A &mathfrak{R} &perp; &rarr; A<br/>A &oplus; &top; &rarr; A<br/>A &mathfrak{R} &top; &rarr; &top;</td><td>&perp; &mathfrak{R} A &rarr; A<br/>&top; &oplus; A &rarr; A<br/>&top; &mathfrak{R} A &rarr; &top;</td></tr></tbody></table>

**Fact 5.4.** The rewriting system $\mathfrak{D}$ is strongly normalizing, with as normal forms distributed formulas.

**Proposition 5.5.** If the equational theory denoted $\mathcal{AC}$ – recall Table 1 on page 3 – is complete for isomorphisms between distributed formulas of MALL, then $\mathcal{L}$ is complete for isomorphisms between arbitrary formulas of MALL. In other words, if for all $A_d$ and $B_d$ distributed formulas of MALL, it stands that $A_d \simeq B_d \implies A_d =_{\mathcal{AC}} B_d$, then for all $A$ and $B$ arbitrary formulas of MALL, $A \simeq B \implies A =_{\mathcal{L}} B$.

*Proof.* Consider an isomorphism $A \simeq B$ between two arbitrary formulas $A$ and $B$ of MALL. Let $A_d$ and $B_d$ be associated distributed formulas, obtained as normal forms of the rewriting system $\mathfrak{D}$ (using Fact 5.4). As each rule of this rewriting system corresponds to a valid equality in the theory $\mathcal{L}$, we have $A =_{\mathcal{L}} A_d$ and $B =_{\mathcal{L}} B_d$.

By soundness of $\mathcal{L}$ (Theorem 2.11) and as linear isomorphism is a congruence, we deduce $A_d \simeq A \simeq B \simeq B_d$. The completeness hypothesis on $\mathcal{AC}$ for distributed formulas yields $A_d =_{\mathcal{AC}} B_d$ from $A_d \simeq B_d$. Thus $A =_{\mathcal{L}} A_d =_{\mathcal{L}} B_d =_{\mathcal{L}} B$, using that $\mathcal{AC}$ is included in $\mathcal{L}$. $\square$

Therefore, we can now consider only distributed formulas. We will use this to study units, as well as when solving the unit-free case to prove there are only commutativity and associativity isomorphisms left.
**5.2. Patterns in distributed isomorphisms.** In this section, we prove units in distributed isomorphisms are in very specific sets of rules, which are the following patterns.

**Definition 5.6 (Patterns).**

* We call a $\top/0$-pattern the following sub-proof:

$$ \overline{\top \top, 0}^{\top} $$

* Likewise, we set $1/\bot$-pattern the sub-proof:

$$ \frac{\overline{\top 1}^{1}}{\top \bot, 1} \bot $$

* A $1/\oplus/\bot$-pattern is a 1-rule followed by a (possibly empty) sequence $\rho$ of $\oplus_i$-rules and finally a $\bot$-rule:

$$ \frac{\overline{\top 1}^{1} \rho}{\top \bot, F} \bot $$

The main goal of this part is proving $\top$-1- and $\bot$-rules in proofs of distributed isomorphisms belong to these patterns. The two $\top/0$- and $1/\bot$-patterns are those we truly wish for. However, we will not find directly $1/\bot$-patterns, but the more generic $1/\oplus/\bot$-patterns; this is not a problem, for using $\oplus_i \bot$ commutations turns a $1/\oplus/\bot$-pattern into a $1/\bot$-pattern. We will need at different points the following grammar.

**Definition 5.7.** Given a formula $B$, we define the grammar

$$ \oplus[B] ::= B \mid \oplus[B] \oplus C \mid C \oplus \oplus[B] $$

where $C$ ranges over all formulas. The occurrence of $B$ which is the base case of this grammar is called its distinguished occurrence.

We first analyze the behavior of units in proofs equal to $\mathrm{id}_A$ up to rule commutation (recall $\mathrm{id}_A$ is the axiom-expansion of $\mathrm{ax}_A$, the proof composed of an $\mathrm{ax}$-rule on $A$), and prove they belong to these patterns (Section 5.2.1). We only do so for a *distributed* formula $A$ as we have already seen it is enough in Section 5.1, and as the above patterns hold only for these formulas. We can then obtain our result, for this property is preserved by cut anti-reduction. However, it is not so easy to prove it, and we will consider slices to do so (Section 5.2.2). This finally allows us to remove the units (Section 5.2.3).

**5.2.1. Patterns in identities up to rule commutation.** We study here patterns containing units in proofs equal to an identity up to rule commutation. The tedious case study on rule commutations and the properties to find in this proof are a great example on why we do not want to do the full proof of completeness in sequent calculus, but wish instead to use proof-nets.

**Proposition 5.8.** Let $\pi$ be a proof equal, up to rule commutation, to $\mathrm{id}_A$ with $A$ distributed. Then:

* the $\top$-rules of $\pi$ are in a $\top/0$-pattern $\overline{\top \top, 0}^{\top}$ with $\top$ in $A$ being the dual of $0$ in $A^{\bot}$ (or vice-versa $\top$ in $A^{\bot}$ being the dual of $0$ in $A$);
• $\perp$-rules and 1-rules come by pairs in a $1/\perp/\perp$-pattern
$$ \frac{\overline{\vdash 1} \quad 1}{\overline{\vdash F} \quad \rho} \perp \quad \text{with } \perp \text{ in } A \text{ being} $$
the dual of 1 in $A^{\perp}$ (or vice-versa);

• there is no sequent in $\pi$ of the shape $\vdash B \& C$.

*Proof.* The key idea is to find properties of $\mathrm{id}_A$ preserved by all rule commutations and ensuring the properties described in the statement. Hence, we prove a stronger property: any sequent $S$ of a proof $\pi$ obtained through a sequence of rule commutations from $\mathrm{id}_A$ for a distributed formula $A$ respects:

(1) the formulas of $S$ are distributed;

(2) if $\vdash$ is a formula of $S$, then $S = \vdash \top, 0$, with $0$ in $A^{\perp}$ the dual of $\top$ if $\top$ is a sub-formula of $A$ (or vice-versa);

(3) if $\perp$ is a formula of $S$, then $S = \vdash \perp, \oplus[1]$ with $\oplus[1]$ the grammar defined in Definition 5.7, where the distinguished occurrence of 1 is the dual of $\perp$ in $A^{\perp}$ if $\perp$ is a sub-formula of $A$ (or vice-versa), and the sub-proof of $\pi$ above $S$ is a sequence of $\oplus_i$ rules leading to the distinguished 1, with in addition a $\perp$-rule inside this sequence;

(4) if $B \& C$ is a formula of $S$, then $S = \vdash B \& C, \oplus[C^{\perp} \oplus B^{\perp}]$ with $\oplus[C^{\perp} \oplus B^{\perp}]$ the grammar defined in Definition 5.7, where the distinguished occurrence of $C^{\perp} \oplus B^{\perp}$ is the dual of $B \& C$ in $A^{\perp}$ if $B \& C$ is a sub-formula of $A$ (or vice-versa), and in the sub-proof of $\pi$ above $S$ the $\oplus$-rules of the distinguished $C^{\perp} \oplus B^{\perp}$ are a $\oplus_2$-rule in the left branch of the $\&$-rule of $B \& C$, and a $\oplus_1$-rule in its right branch;

(5) if $S$ contains several negative formulas or several positive formulas, then its negative formulas are all $\mathfrak{S}$-formulas or negated atoms.

Remark that (5) is a corollary of properties (2), (3) and (4). As in $\vdash^{\underline{r}}$ there is no commutation with a *cut-rule* (in particular no *cut* — $\top$ commutation) and no $\otimes$ — $\top$ commutation creating a sub-proof with a *cut-rule*, it follows that $\pi$ is cut-free and has the sub-formula property, making (1) trivially true. We prove that the fully expanded axiom respects properties (2), (3) and (4), and that these properties are preserved by any rule commutation of $\vdash^{\underline{r}}$.

*The fully expanded axiom respects the properties.* We prove by induction on the distributed formula $A$ properties (2), (3) and (4). Notice that sub-formulas of $A$ are also distributed. By symmetry, assume $A$ is positive.

If $A \in \{X, 1, 0\}$ where $X$ is an atom, then:

$$ \mathrm{id}_A \in \left\{ \frac{\overline{\vdash X^{\perp}, X} \ ax}{\overline{\vdash 1} \quad 1} \perp ; \ \overline{\vdash \perp, 1} \perp ; \ \overline{\vdash \top, 0} \top \right\} $$

Each of these proofs respects (2), (3) and (4).

Assume the result holds for $B$ and $C$, and that $A = B \otimes C$. The proof $\mathrm{id}_A$ is:

$$ \frac{\mathrm{id}_B \qquad \mathrm{id}_C}{\frac{\vdash B^{\perp}, B \qquad \vdash C^{\perp}, C \qquad \otimes}{\vdash C^{\perp}, B^{\perp}, B \otimes C \qquad \mathfrak{S} \vdash C^{\perp} \mathfrak{S} B^{\perp}, B \otimes C}} $$

We have to prove the sequents $\vdash C^{\perp}, B^{\perp}, B \otimes C$ and $\vdash C^{\perp} \mathfrak{S} B^{\perp}, B \otimes C$ respect the properties. The latter respects (2), (3) and (4) trivially for it has neither a $\top$, $\perp$ nor $\&$ formula. As $C^{\perp} \mathfrak{S} B^{\perp}$ is distributed, it follows that neither $C^{\perp}$ nor $B^{\perp}$ can be a $\top$, $\perp$ or $\&$ formula, and as such the former sequent also respects the properties.
Suppose $A = B \oplus C$ with sequents of $id_B$ and $id_C$ respecting the properties. Now, $id_A$ is:

$$ \frac{\begin{array}{c} \text{id}_C \\ \vdash C^{\perp}, C \\ \vdash C^{\perp}, B \oplus C \end{array} \oplus_2 \begin{array}{c} \text{id}_B \\ \vdash B^{\perp}, B \\ \vdash B^{\perp}, B \oplus C \end{array} \oplus_1 \begin{array}{c} \& \\ \vdash C^{\perp} \& B^{\perp}, B \oplus C \end{array}}{\vdash C^{\perp} \& B^{\perp}, B \oplus C} \& $$

The sequent $\vdash C^{\perp} \& B^{\perp}, B \oplus C$ respects (2), (3) and (4), as the $\oplus$ is the dual of the $\&$. By symmetry, we show the properties are also fulfilled by $\vdash B^{\perp}, B \oplus C$, and they will be respected by $\vdash C^{\perp}, B \oplus C$ with a similar proof. As the formulas are distributed, $B^{\perp}$ cannot be a $\top$ formula, hence the sequent respects (2). If $B^{\perp}$ is not a $\perp$ nor $\&$ formula, then (3) and (4) hold for $\vdash B^{\perp}, B \oplus C$. If it is, then using that $\vdash B^{\perp}, B$ respects (3) and (4), it follows that $B \oplus C$ is also of the required shape, for $B$ was.

*Every possible rule commutation preserves the properties.* We show that each rule commutation preserves properties (2), (3) and (4), using every time the notations from Tables 5 and 6 in Definition 2.5, on Pages 12 and 13. By symmetry, we treat only one case for $\otimes - \otimes, \mathcal{N} - \otimes, \& - \otimes$ and $\oplus_i - \otimes$ commutations.

**$\top$-commutations:** Using property (2), we cannot do any commutation between a $\top$-rule and a $\mathcal{N}$, $\&$, $\oplus_i$, $\perp$ or $\top$-rule, so no commutations at all involving a $\top$-rule.

**$\perp$-commutations:** Using property (3), we cannot do any commutation between a $\perp$-rule and a $\mathcal{N}$, $\&$, $\oplus$ or $\perp$-rule. A commutation between a $\perp$ and a $\oplus_i$-rule preserves property (3): we have by hypothesis $\Gamma$ empty and $A_1 \oplus A_2$ of the right shape. It also respects (2) and (4) trivially.

*$C_{\mathcal{N}}^{\mathcal{N}}$ commutation:* We have to show the properties for $\vdash A_1, A_2, B_1 \mathcal{N} B_2, \Gamma$. Because $\vdash A_1 \mathcal{N} A_2, B_1 \mathcal{N} B_2, \Gamma$ respects them, negative formulas of $\Gamma$ are $\mathcal{N}$-formulas or negated atoms by (5). By distributivity, if $A_1$ (or $A_2$) is a negative formula, then it must be a $\mathcal{N}$ one or a negated atom. Thus, $\vdash A_1, A_2, B_1 \mathcal{N} B_2, \Gamma$ fulfills (2), (3) and (4).

*$C_{\oplus_j}^{\oplus_i}$ commutation:* We show the properties for $\vdash A_i, B_1 \oplus B_2, \Gamma$. As $\vdash A_1 \oplus A_2, B_1 \oplus B_2, \Gamma$ respects them, negative formulas of $\Gamma$ are $\mathcal{N}$-formulas or negated atoms by (5). If $A_i$ is positive, a $\mathcal{N}$ or a negated atom, then we are done. Otherwise, as $\vdash A_i, B_j, \Gamma$ fulfills the properties, it follows $\Gamma$ is empty and $B_j$ of the desired shape. By (1), $B_j$ is not 0, thus $A_i$ is not $\top$. Whether $A_i$ is $\perp$ or $\&$, the sequent $\vdash A_i, B_1 \oplus B_2$ respects the properties.

*$C_{\otimes}^{\otimes}$ commutation:* We have to show the properties for $\vdash A_1 \otimes A_2, B_1, \Gamma, \Delta$. Because $\vdash A_1 \otimes A_2, B_1 \otimes B_2, \Gamma, \Delta, \Sigma$ respects them, negative formulas of $\Gamma$ and $\Delta$ are $\mathcal{N}$-formulas or negated atoms by (5). If $B_1$ is positive, a $\mathcal{N}$ or a negated atom, then we are done. Otherwise, as $\vdash A_2, B_1, \Delta$ fulfills the properties, it follows $\Delta$ is empty and $B_1$ of the desired shape, so $B_1$ is a 0, 1 or $\oplus$-formula. This is impossible as $B_1 \otimes B_2$ is distributed by (1).

*$C_{\&}^{\&}, C_{\mathcal{N}}^{\mathcal{N}}, C_{\oplus}^{\oplus}, C_{\otimes}^{\otimes}$ and $C_{\&}^{\otimes}$ commutations:* These cases are impossible by property (4).

*$C_{\oplus_i}^{\&}$ and $C_{\&}^{\oplus_i}$ commutations:* In these cases, (4) for $\vdash A_1 \& A_2, B_1 \oplus B_2, \Gamma$ implies $\Gamma$ empty and $B_1 \oplus B_2$ of the desired shape. Thus $B_i$ of the desired shape ($B_1 \oplus B_2$ is not the distinguished formula as it has the same rule $\oplus_i$ in both branches of the $\&$-rule), proving the result for $\vdash A_1 \& A_2, B_i$. For $\vdash A_1, B_1 \oplus B_2$ (and similarly $\vdash A_2, B_1 \oplus B_2$), $A_1$ cannot be a $\top$ by (1), and if it is a $\perp$ or a $\&$, then the hypothesis on $\vdash A_1, B_i$ implies that the properties are also respected in $\vdash A_1, B_1 \oplus B_2$.
$C_{\oplus i}^{\mathfrak{A}}$ and $C_{\oplus i}^{\mathfrak{A}}$ **commutations**: Let us show the properties for $\vdash A_1, A_2, B_1 \oplus B_2, \Gamma$ in the first commutation and $\vdash A_1 \mathfrak{A} A_2, B_i, \Gamma$ in the second. As they hold for $\vdash A_1, A_2, B_i, \Gamma$, negative formulas in $A_1, A_2, B_i, \Gamma$ are $\mathfrak{A}$-formulas or negated atoms by (5) and the result follows.

$C_{\oplus i}^{\mathfrak{A}}$ **commutation**: We have to prove $\vdash A_1, B_1 \oplus B_2, \Gamma$ respects the properties. Because $\vdash A_1 \otimes A_2, B_1 \oplus B_2, \Gamma, \Delta$ fulfills them, negative formulas of $\Gamma$ are $\mathfrak{A}$ or negated atoms by (5). If $A_1$ is a negative formula other than a $\mathfrak{A}$ or an atom, then for $\vdash A_1, B_i, \Gamma$ respects the properties we have that $\Gamma$ is empty and $B_i$ of the desired shape. By (1), $B_i$ is not a 0, so $A_1$ is not a $\top$. But then $B_1 \oplus B_2$ also has the wished shape for $A_1$, and $\vdash A_1, B_1 \oplus B_2$ fulfills the properties.

$C_{\otimes i}^{\mathfrak{A}}$ **commutation**: We prove $\vdash A_1 \otimes A_2, B_i, \Gamma, \Delta$ respects the properties. As they are fulfilled by $\vdash A_1 \otimes A_2, B_1 \oplus B_2, \Gamma, \Delta$, negative formulas of $\Gamma$ and $\Delta$ are $\mathfrak{A}$ or atoms by (5). As $A_1 \otimes A_2$ is distributed by (1), $A_1$ cannot be a 0, 1 nor $\oplus$ formula, so by $\vdash A_1, B_i, \Gamma$ fulfilling the properties it follows that $B_i$ cannot be a negative formula other than a $\mathfrak{A}$ or an atom. The conclusion follows.

$C_{\otimes i}^{\mathfrak{A}}$ **commutation**: We prove the properties for $\vdash A_1, A_2, B_1 \otimes B_2, \Gamma, \Delta$. As they are respected by $\vdash A_1 \mathfrak{A} A_2, B_1 \otimes B_2, \Gamma, \Delta$, according to (5) negative formulas of $\Gamma$ and $\Delta$ can only be $\mathfrak{A}$-formulas or atoms. As $A_1 \mathfrak{A} A_2$ is distributed by (1), $A_1$ and $A_2$ are positive or $\mathfrak{A}$-formulas or atoms. The conclusion follows.

$C_{\otimes i}^{\mathfrak{A}}$ **commutation**: We prove the properties for $\vdash A_1 \mathfrak{A} A_2, B_1, \Gamma$. As $\vdash A_1, A_2, B_1, \Gamma$ respects them, by (5) negative formulas of $\Delta$ and $B_1$ can only be $\mathfrak{A}$-formulas or atoms, proving the result.

Therefore, we proved the expanded axiom respects these properties, and they are preserved by all rule commutations. The conclusion follows. $\square$

5.2.2. Surgery on slices. In order to prove that $\top$ and $\bot$-rules in proofs of distributed isomorphisms belong to $\top/0-$ and $1/\oplus/\bot$-patterns, we show these patterns are preserved by cut anti-reduction and conclude as the identity has these patterns. However, proving this preservation is not easy and uses the notion of slices (recall Definition 2.1 on page 7).

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

$$ \frac{\frac{\vdash A, \Gamma \qquad \vdash B^{\perp}, \Delta}{\vdash A \oplus B, \Gamma \oplus 1} \&_1}{\vdash \Gamma, \Delta} $$

is a failure since the selected sub-formulas of $A \oplus B$ and its dual do not match. More precisely, we have a failure exactly when reducing a key case between $\&_i$ and $\oplus_j$ for $i = j$ – when $i \neq j$ (i.e. $j = 1 - i$) the cut reduces correctly as follows:

$$ \frac{\frac{\vdash A_i, \Gamma \qquad \vdash A_i^{\perp}, \Delta}{\vdash A_1 \oplus A_2, \Gamma \oplus i} \&_j}{\vdash \Gamma, \Delta} \xrightarrow{\beta} \frac{\vdash A_i, \Gamma \qquad \vdash A_i^{\perp}, \Delta}{\vdash \Gamma, \Delta} \text{cut} $$

Given two slices $s \in S(\pi)$ and $r \in S(\rho)$ with respective conclusions $\vdash A, \Gamma$ and $\vdash A^{\perp}, \Delta$, their composition by cut $s \overset{A}{\rightsquigarrow} r$ reduces either to a slice of a normal form of $\pi \overset{A}{\rightsquigarrow} \rho$ or to a failure.
**Lemma 5.9.** Let $\pi_1$ and $\pi_2$ be proofs such that $\pi_1 \xrightarrow{\beta} \pi_2$. For each $s_2 \in S(\pi_2)$, there exists $s_1 \in S(\pi_1)$ such that $s_1 \xrightarrow{\beta} s_2$ or $s_1 = s_2$. Reciprocally, for each $s_1 \in S(\pi_1)$, $s_1$ reduces to a failure or there exists $s_2 \in S(\pi_2)$ such that $s_1 \xrightarrow{\beta} s_2$ or $s_1 = s_2$.

*Proof.* We can check that each cut-elimination step respects this property, with the equality case coming from a reduction in $\pi_1 \xrightarrow{\beta} \pi_2$ on rules not in the considered slice $s_2$ (resp. $s_1$). $\square$

**Lemma 5.10.** Let $\pi_1$ and $\pi_2$ be proofs whose composition over $A$ reduces to a proof $\tau$. For each $s \in S(\tau)$, there exist $s_1 \in S(\pi_1)$ and $s_2 \in S(\pi_2)$ such that $s_1 \overset{A}{\unlhd} s_2$ reduces to $s$.

*Proof.* By induction on the sequence $\pi_1 \overset{A}{\unlhd} \pi_2 \xrightarrow{\beta^*} \tau$, using Lemma 5.9. $\square$

**Lemma 5.11.** Let $\pi_1$ and $\pi_2$ be cut-free proofs of $\vdash \Gamma$ with $\vdash$-rules all in $\vdash/0$-patterns. Assume that $\pi_1 \unlhd^* \pi_2$, where in this sequence there is no rule commutation involving a $\vdash$-rule. Then for each slice $s_1 \in S(\pi_1)$, there exists a unique $s_2 \in S(\pi_2)$ such that $s_1$ and $s_2$ make the same choices for additive connectives in $\Gamma$.

*Proof.* This can be easily checked for each equation in $\unlhd^*$, save for those involving $\vdash$. $\square$

Given a choice $C$ of premises for some additive connectives of a sequent, we say a slice is on $C$ if each $&_i$- and $\oplus_i$-rule in this slice takes premise $i$ for a connective in $C$ whose chosen premise is $i$. This concept will be essential when speaking about proof-nets (in Section 6.1 for instance), as it is related to additive resolutions.

**Lemma 5.12.** Given a choice $C$ of premises for additive connectives of $A$ (but not $A^\perp$), there exists a unique slice of $S(\mathrm{id}_A)$ on it, which furthermore makes on $A^\perp$ the dual choices of $C$.

*Proof.* Direct induction on $A$, following the definition of $\mathrm{id}_A$ on Table 2. $\square$

We now prove a partial reciprocal to Lemma 5.10. Notice in the following statement that the assumption is on the composition over $A$, and the conclusion on the existence of a slice for the composition over $B$, the other formula.

**Lemma 5.13.** Let $\pi$ and $\pi'$ be cut-free proofs respectively of $\vdash A^\perp$, $B$ and $\vdash B^\perp$, $A$, whose composition over $A$ reduces to $\mathrm{id}_B$ up to rule commutation. Set $\rho$ a normal form of $\pi \overset{B}{\unlhd} \pi'$, i.e. any result of eliminating all cut-rules in this proof. Then, for any slice $s$ of $\pi$, there exists a slice $s'$ of $\pi'$ such that $s \overset{B}{\unlhd} s'$ reduces to a slice of $\rho$.

*Proof.* Take $s \in S(\pi)$, and denote by $C$ the choices made in $s$ on $\&$ and $\oplus$ connectives of the formula $B$. We will use that the composition over the formula $A$ reduces to $\mathrm{id}_B$ up to $\unlhd^*$ to find $s' \in S(\pi')$ that makes the dual choices of $C$ on additive connectives of $B^\perp$. This ensures no failure happens during the reduction of $s \overset{B}{\unlhd} s'$, which thus reduces to a slice of $\rho$ (Lemma 5.9).

By hypothesis, call $\tau$ a cut-free proof resulting from cut-elimination of $\pi \overset{A}{\unlhd} \pi'$, with $\tau \unlhd^* \mathrm{id}_B$. By Lemma 5.12, there is a (unique) slice of $\mathrm{id}_B$ with choices $C$ on $B$ and dual choices $C^\perp$ on $B^\perp$. Applying Proposition 5.8, all proofs in the sequence $\tau \unlhd^* \mathrm{id}_B$ have $\vdash$-rules with only 0 in their context; in particular, there cannot be any commutation involving a $\vdash$-rule in this sequence. Using Lemma 5.11, there is a slice $t$ of $\tau$ with choices $C$ and $C^\perp$.
According to Lemma 5.10, we have slices $r \in S(\pi)$ and $r' \in S(\pi')$ whose composition on $A$ reduces to $t$. In particular, $r$ makes choices $C$ on $B$ and $r'$ choices $C^{\perp}$ on $B^{\perp}$, as these choices are those in the resulting slice $t$, and no reversed cut-elimination step can modify them (a $\vdash$-cut commutative case can erase such choices, but taking it in the other direction can only create choices). Therefore, $r'$ makes on $B^{\perp}$ the dual choices of $s$ on $B$, and we can take such a slice as $s'$. $\square$

Lemma 5.13 will be used to prove that any non-ax-rule $r$ in $\pi$ is not erased in all slices by $\& - \oplus_i$ key cases during normalization. More precisely, taking a slice $s$ containing $r$, of principal connective in, say $A^{\perp}$, the lemma gives a slice $s' \in S(\pi')$ that has no failure for a composition over $B$. As $r$ does not introduce a cut formula, the only way for it to be erased during the reduction is by a $\vdash$-cut commutative case, in which case its principal formula becomes a sub-formula of the sequent on which a $\vdash$-rule is applied. This will be enough to conclude in our cases, as we know that the resulting normal form only has $\vdash$-rules of the shape $\vdash \top, 0^{\top}$ (using Theorem 4.3 and Proposition 5.8).

**Lemma 5.14.** Let $r$ be a non-ax-rule in a cut-free slice $s$ of conclusion $\vdash \Gamma, A$, with the conclusion sequent of $r$ of the shape $\Sigma_{\Gamma}, \Sigma_{A}$ where $\Sigma_{\Gamma}$ is a sub-sequent of $\Gamma$ and $\Sigma_{A}$ of $A$. Also assume the principal formula of $r$ belongs to $\Sigma_{\Gamma}$, i.e. is not a sub-formula of $A$. Take $s'$ a cut-free slice of conclusion $\vdash A^{\perp}, \Delta$ such that $s \overset{A}{\rightleftharpoons} s'$ reduces to a cut-free slice $s''$. Then either there is in $s''$ a rule of the same kind as $r$, applied on a sequent $\vdash \Sigma_{\Gamma}, \Theta$ with the same principal formula as $r$, or $\Sigma_{\Gamma}$ is a sub-sequent of a $\vdash$-rule in $s''$, whose main $\vdash$-formula is not in $\Sigma_{\Gamma}$.

*Proof.* By hypothesis, $r$ does not introduce a *cut*-formula, for these formulas are sub-formulas of $A$ or $A^{\perp}$. Therefore, the only reductions in $s \overset{A}{\rightleftharpoons} s' \xrightarrow{\beta^*} s''$ that can erase $r$ are $\vdash$-cut commutative cases, for the $\&_i - \oplus_j$ key cases in the reduction do not lead to a failure. If no such erasure happens, then we are done: other cut commutative cases involving $r$ may modify its conclusion sequent, but only in the part coming from $A$, thus $\Sigma_{\Gamma}$ is preserved.

If a $\vdash$-cut reduction erases $r$, then $\Sigma_{\Gamma}$ is in the context of the resulting $\vdash$-rule $t$, possibly as a sub-sequent. Furthermore, the principal $\vdash$-formula of $t$ is not in $\Sigma_{\Gamma}$. This is enough to conclude, using an induction on the number of steps in $s \overset{A}{\rightleftharpoons} s' \xrightarrow{\beta^*} s''$. Notice that $t$ may be erased too during the reduction but, like $r$, this would lead to $\Sigma_{\Gamma}$ being a sub-sequent of the context of another $\vdash$-rule. $\square$

**Remark 5.15.** Cut-free MALL proofs have the *sub-sequent property*: every sequent in such a proof is a sub-sequent of the conclusion sequent, as every rule respects this property, except the *cut-rule*.

5.2.3. *Patterns in proofs of isomorphisms.* Thanks to the technical results on slices, we can finally deduce that $\vdash$ and $\perp$-rules in proofs of distributed isomorphisms belong to $\vdash/0$- and $1/\oplus/\perp$-patterns.

**Lemma 5.16.** If $A \simeq_B B$ with $A$ and $B$ distributed, then all $\vdash$-rules in $\pi$ and $\pi'$ are in a $\vdash/0$-pattern.

*Proof.* Consider $t$ a $\vdash$-rule $\vdash \Gamma, \Delta^{\top}$ in $\pi$, with $\Gamma$ occurrences of sub-formulas of $A^{\perp}$ and $\Delta$ of $B$ (as the cut-free $\pi$ has for conclusion sequent $\vdash A^{\perp}, B$, see Remark 5.15). By
symmetry, say the main $\top$-formula of $t$ belongs to $\Gamma$, i.e. is a sub-formula of $A^{\perp}$. Call $s$ a slice the $\top$-rule $t$ belongs to.

Set $\rho$ a normal form of $\pi \stackrel{B}{\rightleftharpoons} \pi'$. By Lemma 5.13, there exists a slice $s' \in S(\pi')$ such that $s \stackrel{B}{\rightleftharpoons} s'$ reduces to a slice $s'' \in S(\rho)$. By Lemma 5.14 applied to $t$, $t$ is either preserved and $\Gamma$ as well, or $t$ is absorbed by another $\top$-rule (during a $\top$-cut commutative case) and $\Gamma$ stays in the context of a $\top$-rule, possibly as a sub-sequent. But by Theorem 4.3, $\rho \stackrel{r}{\rightleftharpoons} \text{id}_A$ and, by Proposition 5.8, the only $\top$-rules of $\rho$, and so of $s''$, are $\overline{\top \top, 0}^{\top}$ rules, with $\top$ being the dual occurrence of 0. Thus, $\top$ and 0 are not both sub-formula of $A^{\perp}$, and it follows $\Gamma$ is either a sub-sequent of $\top$ or one of 0. For $\Gamma$ contains $\top$, we conclude that $\Gamma$ is $\top$. Moreover, it follows that $t$ had not been erased during a $\top$-cut commutative case, using Lemma 5.14 (otherwise there would be at least two $\top$-formulas in the resulting $\top$-rule). This implies that $\Delta$ cannot be empty: if it were, $t$ could not commute with any cut-rule, as it could not do a $\top$-cut commutative case for it does not have a cut formula, which is a sub-formula of $B$, in its context, and no other cut-elimination step can change this. Thus, if $\Delta$ were empty then $t$ would be a rule of $s''$, impossible as it is a $\overline{\top \top}^{\top}$ rule.

Similarly, set $\tau$ a normal form of $\pi \stackrel{A}{\rightleftharpoons} \pi'$. By Lemma 5.13 and Lemma 5.14, $t$ is either preserved during the reduction (in a slice) and $\Delta$ as well, or $t$ is absorbed by another $\top$-rule and $\Delta$ stays in the context of a $\top$-rule, possibly as a sub-sequent. But $t$ cannot be preserved: its main formula is a sub-formula of $A^{\perp}$, and in $\tau$ there are only occurrences of sub-formulas of $B$ and $B^{\perp}$. Therefore, $\Delta$ in $\tau$ is in the context of a $\top$-rule, and does not contain its principal $\top$-formula. But by Theorem 4.3 and Proposition 5.8, the only $\top$-rules of $\tau$ are $\overline{\top \top, 0}^{\top}$ rules, with $\top$ being the dual occurrence of 0. Hence, $\Delta$ must be a sub-sequent of 0. As $\Delta$ cannot be empty, $\Delta$ is 0.

Thus, any $\top$-rule $t$ in $\pi$ (and $\pi'$ by symmetry) is of the shape $\overline{\top \top, 0}^{\top}$. $\square$

**Lemma 5.17.** Let $\pi$ be a proof whose $\top$-rules are all in a $\top/0$-pattern. There is a cut-elimination strategy in $\pi$ whose $\top$-cut commutative cases are all of the form:

$$ \frac{\overline{\top \top, 0}^{\top} \quad \overline{\top \top, 0}^{\top} \quad \overline{\top \top, 0}^{\top}}{\top \top, 0} \text{cut} \xrightarrow{\beta} \overline{\top \top, 0}^{\top} $$

*Proof.* Our strategy is the following. First, while we can apply a cut-elimination step which is not a $\top$-cut nor a $\top$-cut commutative case, we do such a reduction step. These operations preserve that all $\top$-rules are in $\top/0$ patterns.

If no such reduction is possible, consider a highest cut-rule, i.e. one with no cut-rule above it. The only possible cases that can be applied using this cut-rule and rules above it are by hypothesis $\top$-cut commutative cases. Thus, the cut-rule is below a $\top$-rule, so necessarily one of its premises is $\overline{\top \top, 0}^{\top}$, with $\top$ not the formula we cut on. But then 0 is the formula we cut on, so there is a $\top$-formula on the other premise; we are in the following situation:

$$ \frac{\overline{\top \top, 0}^{\top} \quad \overline{\top \top, \Gamma}^{\top} \quad \overline{\top \top, \Gamma}^{\top}}{\top \top, \Gamma} \text{cut} $$

We prove the rule $r$ above the premise $\vdash \top, \Gamma$ of the cut-rule is the $\top$-rule corresponding to the cut formula $\top$. If $r$ were not a $\top$-rule, then one could apply a commutative or $ax$ key case, which cannot be. Plus, $r$ cannot be a $\top$-rule corresponding to another $\top$-formula,
because such a rule would have two $\top$-formulas in its conclusion. Thence, $r$ is the $\top$-rule introducing the formula we cut on, and our sub-proof is:

$$ \frac{\vdash \top, 0 \top \qquad \vdash \top, 0 \top}{\vdash \top, 0} \text{cut} $$

A $\top$-cut commutative case yields $\vdash \top, 0 \top$ which is the allowed $\top$-cut reduction step. This reduction strategy terminates (Proposition A.10) and reaches a cut-free proof. $\square$

**Lemma 5.18.** If $A \simeq_B B$ with $A$ and $B$ distributed, then there is no sequent of the shape $\vdash D \& E$ in $\pi$ (and $\pi'$).

*Proof.* Assume w.l.o.g. $D \& E$ is a sub-formula of $A^{\perp}$, and let $s$ be a slice containing the sequent $\vdash D \& E$. Pose $\rho$ a normal form of $\pi \bowtie^B \pi'$ obtained by following the strategy given by Lemma 5.17. By Lemma 5.13, there exists a slice $s' \in S(\pi')$ such that $s \bowtie^B s'$ reduces to a slice $s''$ of $\rho$. Since $D \& E$ is a sub-formula of $A^{\perp}$, it is not a cut formula during the reduction, and the sequent $\vdash D \& E$ remains in $s''$, so in $\rho$. Indeed, reducing cuts using these steps preserves having the sequent $\vdash D \& E$ (as there is no failure in the reduction). This is trivial for all steps except $\top$-cut. In the case a $\top$-cut step, by hypothesis on the reduction strategy, it cannot erase the sequent $\vdash D \& E$ from the proof. Thus, the sequent $\vdash D \& E$ belongs to $\rho$, which is equal to the identity up to rule commutations (Theorem 4.3). This is impossible by Proposition 5.8. $\square$

**Lemma 5.19.** If $A \simeq_B B$ with $A$ and $B$ distributed, then all $\perp$-rules and 1-rules belong to $1/\oplus/\perp$-patterns.

*Proof.* In $\pi$, we look at a possible rule $r$ below a sequent $\vdash \oplus[1]$ (Definition 5.7). It cannot be a $\otimes$-rule by distributivity, nor a $\aleph$-rule for the sequent has a unique formula, nor a $\&$-rule due to Lemma 5.18. If $r$ is a $\oplus_i$-rule, then we keep a sequent $\vdash \oplus[1]$, and if it is a $\perp$-rule then it is one of the required shape.

As a consequence, each 1-rule is followed by some $\oplus_i$-rules and possibly a $\perp$-rule; let us call a $1/\oplus$-pattern a 1-rule followed by a maximal such sequence of $\oplus_i$-rules. If a $1/\oplus$-pattern stops without a $\perp$-rule below it, we have only one formula in the conclusion sequent of the proof: impossible as $\pi$ is a proof of $\vdash A^{\perp}, B$. Thus, the $\perp$-rule exists and to each 1-rule we can associate a $\perp$-rule leading to a $1/\oplus/\perp$-pattern. Henceforth, there are at least as many $\perp$-rules as 1-rules, and as the patterns they belong to have no $\&$-rule, this also holds in any slice.

Consider a slice $s$ of $\pi$. By Lemma 5.13, there exists a slice $s' \in S(\pi')$ such that $s \bowtie^B s'$ reduces to a slice $s''$ of $\rho$, the latter being a normal form of $\pi \bowtie^B \pi'$ obtained by following the strategy given by Lemma 5.17. Moreover, $s''$ contains as many $\perp$-rules as 1-rules, as in $\rho$ they belong to a $1/\oplus/\perp$-pattern (Theorem 4.3 and Proposition 5.8), so are in the same slices. Furthermore, in $s''$, each 1 from $A$ (resp. $A^{\perp}$) corresponds to a $\perp$ from $A^{\perp}$ (resp. $A$).

Remark that, in the reduction $s \bowtie^B s' \xrightarrow{\beta^*} s''$, the only steps that may erase a $\perp$ or 1-rule are $\perp - 1$ and $\top - \text{cut}$ cases. But a $\top - \text{cut}$ commutative case cannot erase non-$\top$-rules by definition of our cut-elimination strategy. Furthermore, a $\perp - 1$ key case erases one 1-rule and one $\perp$-rule. Therefore, with $r_s$ the number of $r$-rules of a slice $s$, we have $\perp_s + \perp_{s'} = 1_s + 1_{s'}$ as $\perp_{s''} = 1_{s''}$ and any reduction step in $s \bowtie^B s' \xrightarrow{\beta^*} s''$ preserves this equality. But, by our
analysis at the beginning of this proof, $1_s \le \perp_s$ and $1_{s'} \le \perp_{s'}$. We conclude $1_s = \perp_s$, i.e. that $s$ has as many $\perp$-rules than 1-rules.

However, each 1-rule, being in a $1/\oplus/\perp$-pattern, belongs to exactly the same slices as the corresponding $\perp$-rule of the pattern. Hence, a $\perp$-rule not in a $1/\oplus/\perp$-pattern would yield a slice $s$ with strictly more $\perp$-rules than 1-rules (taking $s$ any slice containing this $\perp$-rule). Thus, every $\perp$-rule belongs to a $1/\oplus/\perp$-pattern. $\square$

**5.3. Completeness with units from unit-free completeness.** In the $1/\oplus/\perp$-patterns, moving each $\perp$-rule up to the associated 1-rule (which can be done up to $\beta$-equality by Proposition 4.1) allows us to consider units as fresh atoms introduced by *ax*-rules, whence we reduce the problem to the unit-free fragment.

**Theorem 5.20 (Isomorphisms completeness from unit-free completeness).** If $\mathcal{AC}$ is complete for isomorphisms in unit-free distributed MALL, then $\mathcal{AC}$ is complete for isomorphisms in distributed MALL (i.e. $A \simeq B \implies A =_{\mathcal{AC}} B$ for all distributed A and B).

*Proof.* Take A and B distributed formulas in MALL (possibly with units) such that $A \simeq B$. We want $A =_{\mathcal{AC}} B$. Using Lemma 2.9, we have $A \simeq B$. By Lemmas 5.16 and 5.19, $\pi$ and $\tau$ have $\top$-rules only of the shape $\vdash \top, 0 \top$ and $\perp$- and 1-rules in $1/\oplus/\perp$-patterns. Using $\perp$-commutations to move each $\perp$-rule just below the 1-rule above it, we build $\pi'$ and $\tau'$ such that $\pi'$ and $\tau'$ have $\top$-rules only of the shape $\vdash \top, 0 \top$, $\perp$ and 1-rules of the form $\frac{\vdash 1}{\vdash \perp, 1} \perp$, $\pi \vdash^* \pi'$ and $\tau \vdash^* \tau'$. Whence, $\pi' \stackrel{B}{\bowtie} \tau' \vdash^* \pi \stackrel{B}{\bowtie} \tau$ and $\pi' \stackrel{A}{\bowtie} \tau' \vdash^* \pi \stackrel{A}{\bowtie} \tau$. By Proposition 4.1 and Theorem 4.3, for any normal form $\rho$ of $\pi' \stackrel{B}{\bowtie} \tau'$ (resp. $\pi' \stackrel{A}{\bowtie} \tau'$), $\rho \vdash^* \mathrm{id}_A$ (resp. $\rho \vdash^* \mathrm{id}_B$).

We reduce cuts in $\pi' \stackrel{B}{\bowtie} \tau'$ (and similarly in $\pi' \stackrel{A}{\bowtie} \tau'$) following a particular strategy, ensuring that the proofs obtained during the reduction have $\top$-rules only of the shape $\frac{\vdash 1}{\vdash \top, 0} \top$, and $\perp$ and 1-rules of the form $\frac{\vdash 1}{\vdash \perp, 1} \perp$.

First, while we can apply a step of cut-elimination which is not a $\top$-cut, $\perp$-cut, $\perp-1$ or cut-cut case, we do such a reduction step. These operations preserve that all $\top$-rules are applied on sequents $\vdash \top, 0$ (up to exchange) and $\perp$- and 1-rules are in the wished pattern.

If no such reduction is possible, consider a highest cut-rule, i.e. one with no cut-rule above it. The only possible cases that can be applied are $\top$-cut, $\perp$-cut or $\perp-1$.

* If a $\top$-cut commutative case can be applied, then the cut-rule is below a $\top$-rule, so necessarily one of its premises is $\frac{\vdash \top, 0}{\vdash \perp, 0} \top$, with $\top$ not the formula we cut on. But then 0 is the formula we cut on, so there is a $\top$-formula on the other premise; we are in the following situation:

$$ \frac{\frac{\phi}{\vdash \top, \Gamma} r}{\vdash \top, 0} cut $$

We prove the rule $r$ above the premise $\vdash \top, \Gamma$ of the cut-rule is the $\top$-rule corresponding to the cut formula $\top$. If it were not the case, then $r$ commutes with the cut-rule. But $r$ cannot be a $\perp$-rule (which cannot have a $\top$-formula in its context), nor a $\top$-rule corresponding to another $\top$-formula (because such a rule would have two $\top$-formulas in its conclusion). Thence, $r$ is the $\top$-rule introducing the formula we cut on. Thus, our sub-proof is:
$$ \frac{\overline{\vdash \top, 0}^{\top} \quad \overline{\vdash \top, 0}^{\top}}{\vdash \top, 0} \text{cut} $$

A $\top$-$cut$ commutative case yields $\overline{\vdash \top, 0}^{\top}$ as if we had done an $ax$ key case.

* If a $\bot$-$cut$ commutative case can be applied, then the $cut$-rule is below a $\bot$-rule, so necessarily one of its premises is $\frac{\overline{\vdash 1}}{\vdash \bot, 1} \bot$, with $\bot$ not the formula we cut on. But then 1 is the formula we cut on, so there is a $\bot$-formula on the other premise; we are in the following situation:

$$ \frac{\frac{\overline{\vdash 1}}{\vdash \bot, 1} \bot \quad \frac{\phi}{\bot, \Gamma} \quad r}{\vdash \bot, \Gamma} \text{cut} $$

We prove the rule $r$ above the premise $\vdash \bot, \Gamma$ of the $cut$-rule is the $\bot$-rule corresponding to the cut formula $\bot$. If it were not the case, then $r$ commutes with the $cut$-rule. But $r$ cannot be a $\top$-rule (which cannot have a $\bot$-formula in its context), nor a $\bot$-rule corresponding to another $\bot$-formula (because such a rule would have two $\bot$-formulas in its conclusion). Thence, $r$ is the $\bot$-rule introducing the formula we cut on. Thus, our sub-proof is:

$$ \frac{\frac{\overline{\vdash 1}}{\vdash \bot, 1} \bot \quad \frac{\overline{\vdash 1}}{\vdash \bot, 1} \bot}{\vdash \bot, 1} \text{cut} $$

We apply a $\bot$-$cut$ commutative case, followed by a $\bot$-$1$ key case, obtaining $\frac{\overline{\vdash 1}}{\vdash \bot, 1} \bot$ as if we had done an $ax$ key case.

* No $\bot$-$1$ key case can be applied, for 1-rules have below them a $\bot$-rule, so not a $cut$-rule.

This strategy of reduction allows reaching a normal form $\rho$, with $\top$-rules only of the shape $\overline{\vdash \top, 0}^{\top}$, and $\bot$ and 1-rules of the form $\frac{\overline{\vdash 1}}{\vdash \bot, 1} \bot$ (Proposition A.10).

Furthermore, call $\sigma$ the substitution replacing $\top$, 0-, $\bot$- and 1-formulas respectively by $X^{\bot}$, $X$, $Y^{\bot}$ and $Y$, for $X$ and $Y$ fresh atoms. We can reach $\sigma(\rho)$ by cut-elimination from $\sigma(\pi') \stackrel{\sigma(B)}{\rightleftharpoons} \sigma(\tau')$, for the reductions we did on units could as well have been done by $ax$ key cases: no $\bot$-$cut$, nor $\bot$-$1$, nor $\top$-$cut$ case was used, except for cases that could be simulated using $ax$ key cases. Moreover, $\sigma(\text{id}_A) = \text{id}_{\sigma(A)}$, and in $\rho \stackrel{r^*}{\rightleftharpoons} \text{id}_A$ we can assume not to commute any $\bot$-rule because we start and end with 1-rules and $\bot$-rules in $\frac{\overline{\vdash 1}}{\vdash \bot, 1} \bot$ shapes only, and such commutations could only move the $\bot$-rule below or above some $\oplus_i$-rules according to Proposition 5.8. Thus, $\sigma(\rho) \stackrel{r^*}{\rightleftharpoons} \text{id}_{\sigma(A)}$. Using Proposition 4.1, it follows $\sigma(\rho) =_{\beta} \text{id}_{\sigma(A)}$, and therefore $\sigma(\pi') \stackrel{\sigma(B)}{\rightleftharpoons} \sigma(\tau') =_{\beta\eta} \text{ax}_{\sigma(A)}$ with $\text{ax}_{\sigma(A)}$ the $ax$-rule on $\sigma(A)$. A similar result holding for a cut over $A$, we have $\sigma(A) \simeq \sigma(B)$, these formulas being unit-free and distributed. For we assume $\mathcal{A}\mathcal{C}$ to be complete for unit-free distributed isomorphisms, this yields $\sigma(A) =_{\mathcal{A}\mathcal{C}} \sigma(B)$. We conclude $A =_{\mathcal{A}\mathcal{C}} B$ by substituting $X$ by 0 and $Y$ by 1, as $X$ and $Y$ were fresh. $\square$
# 6. PROOF-NETS FOR UNIT-FREE MALL

We will at present change the syntax, no longer considering sequent calculus proofs but *proof-nets*, choosing the syntax from Hughes & Van Glabbeek for unit-free MALL [HvG05]. A key property of proof-nets is to be a more canonical representation of proofs, as they define a quotient of sequent calculus proofs up to rule commutations [HvG16] (we recall Tables 5 and 6 on Pages 12 and 13 give rule commutations).<fnref n="1" /> This yields better properties concerning the study of isomorphisms. As a key example, cut-elimination in proof-nets is confluent and leads to a unique normal form. This spares us tedious case studies on rule commutations – like the one in the proof of Proposition 5.8, which was due to the need to relate the different possible cut-free proofs obtained by cut-elimination. Thus, studying isomorphisms using proof-nets will be less complex. Nonetheless, we leave an inductive definition for a graphical syntax. It would have been ideal to use this syntax from the very beginning. Unfortunately, this was not possible as no notion of proof-nets exists with units and exact quotient on normal forms.

Other definitions of proof-nets exist, see the original one from Girard [Gir96], or others such as [DG11, HH16b]. Still, the definition we take is one of the most satisfactory, from the point of view of canonicity and cut-elimination for instance (see [HvG05, HvG16], or the introduction of [HH16b] for a comparison of alternative definitions). We recall here this definition of proof-nets, and define composition by cut and cut-elimination for this syntax. Please refer to [HvG05] for more details, as well as the intuitions behind the definition. In all that follows, as we use proof-nets, we consider only the unit-free fragment of MALL, unless stated otherwise.

## 6.1. Proof-net.
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^{\perp}$, given a formula $A$; the connective $*$ is unordered. A *cut sequent* [$\Sigma$] $\Gamma$ is composed of a list $\Sigma$ of cut pairs and a sequent $\Gamma$. When $\Sigma = \emptyset$ is empty, we denote it simply by $\Gamma$. For instance, $[X_5 * X_6^{\perp}] X_1 \& X_2^{\perp}, X_3 \oplus X_4^{\perp}$ (where each $X_i$ is an occurrence of the same atom $X$) is a cut sequent, on which we will instantiate the concepts defined in this part.

An *additive resolution* of a cut sequent [$\Sigma$] $\Gamma$ is any result of deleting zero or more cut pairs from $\Sigma$ and one argument sub-tree of each additive connective ($\&$ or $\oplus$) of $\Sigma \cup \Gamma$. A *&-resolution* of a cut sequent [$\Sigma$] $\Gamma$ is any result of deleting one argument sub-tree of each &-connective of $\Sigma \cup \Gamma$. For example, $[] X_1 \& , \oplus X_4^{\perp}$ is one of the eight additive resolutions of $[X_5 * X_6^{\perp}] X_1 \& X_2^{\perp}, X_3 \oplus X_4^{\perp}$, while $[X_5 * X_6^{\perp}] X_1 \& , X_3 \oplus X_4^{\perp}$ is one of its two &-resolutions. Notice the difference on cut pairs: they may be deleted in an additive resolution, but never in a &-resolution.

An (*axiom*) *link* on [$\Sigma$] $\Gamma$ is an unordered pair of complementary leaves in $\Sigma \cup \Gamma$ (labeled with $X$ and $X^{\perp}$ for some atom $X$). A *linking* $\lambda$ on [$\Sigma$] $\Gamma$ is a set of disjoint links on [$\Sigma$] $\Gamma$ respecting the following property: the set made of the leaves of the axiom links of $\lambda$ is the set of leaves of an additive resolution of [$\Sigma$] $\Gamma$; this (unique) additive resolution is denoted [$\Sigma$] $\Gamma \upharpoonright \lambda$. For instance, on the left-most graph of Figure 2, the red axiom links form a linking $\lambda_1 = \{(X_1, X_6^{\perp}); (X_4^{\perp}, X_5)\}$, whose additive resolution is

<footnote n="1">¹While the definition of rule commutations in [HvG16] differs a little from ours, for they also consider commutations involving a *cut-rule*, both definitions coincide on cut-free proof-nets, which are the objects we want canonical.</footnote>
$[X_5 * X_6^\perp] X_1 \& X_2^\perp, X_3 \oplus X_4^\perp \upharpoonright \lambda_1 = [X_5 * X_6^\perp] X_1 \& , \oplus X_4^\perp$ (which is the unique additive resolution associated to the set of leaves $\{X_1; X_4^\perp; X_5; X_6^\perp\}$).

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.

A set of linkings $\Lambda$ on $[\Sigma] \Gamma$ toggles a &-vertex $W$ if both arguments (called *premises*) of $W$ are in $[\Sigma] \Gamma \upharpoonright \Lambda := \bigcup_{\lambda \in \Lambda} [\Sigma] \Gamma \upharpoonright \lambda$. We say a link $a$ *depends* on a &-vertex $W$ in $\Lambda$ if there exist $\lambda, \lambda' \in \Lambda$ such that $a \in \lambda \setminus \lambda'$ and $W$ is the only &-vertex toggled by $\{\lambda; \lambda'\}$. Looking at our running example, and taking $\lambda_1 = \{(X_1, X_6^\perp), (X_4^\perp, X_5)\}$ and $\lambda_2 = \{(X_2^\perp, X_3)\}$, the &-vertex is toggled by $\{\lambda_1; \lambda_2\}$. Furthermore, all links depend on this &-vertex for $\lambda_1$ and $\lambda_2$ contain only different pairs.

The graph $G_\Lambda$ is defined as $[\Sigma] \Gamma \upharpoonright \Lambda$ with the edges from $\bigcup \Lambda$ and enriched with jump edges $l \to W$ for each leaf $l$ and each &-vertex $W$ such that there exists $a \in \lambda \in \Lambda$, between $l$ and some $l'$, with $a$ depending on $W$ in $\Lambda$. When $\Lambda = \{\lambda\}$ is composed of a single linking, we shall simply denote $G_\lambda = G_{\{\lambda\}}$ (which is the graph $[\Sigma] \Gamma \upharpoonright \lambda$ with the edges from $\lambda$ and no jump edge). For our example, the graphs $G_{\lambda_1}, G_{\lambda_2}$ and $G_{\{\lambda_1; \lambda_2\}}$ are illustrated on Figure 2.

In the text of this paper (but not on the graphs), we write $l \xrightarrow{j} W$ for a jump edge from a leaf $l$ to a &-vertex $W$. When drawing proof-nets, we will denote membership of a linking by means of colors.

When we write a $\mathcal{Y}\&$-vertex, we mean a $\mathcal{Y}$- or &-vertex (a *negative vertex*); similarly a $\otimes\oplus$-vertex is a $\otimes$- or $\oplus$-vertex (a *positive vertex*). A *switch edge* of a $\mathcal{Y}\&$-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 $\mathcal{Y}\&$-vertex. A *$\mathcal{Y}$-switching* of a linking $\lambda$ is any subgraph of $G_\lambda$ obtained by deleting a switch edge of each $\mathcal{Y}$-vertex; denoting by $\phi$ this choice of edges, the subgraph it yields is $G_\phi$. For example, a cycle in a $\mathcal{Y}$-switching is a switching cycle, as in a graph $G_\phi$ all $\mathcal{Y}\&$-vertices have one premise.

**Definition 6.1** (Proof-net). A *unit-free MALL proof-net* $\theta$ on a cut sequent $[\Sigma] \Gamma$ is a set of linkings satisfying:

(P0) *Cut*: Every cut pair of $\Sigma$ has a leaf in $\theta$.

(P1) *Resolution*: Exactly one linking of $\theta$ is on any given &-resolution of $[\Sigma] \Gamma$.

(P2) *MLL*: For every $\mathcal{Y}$-switching $\phi$ of every linking $\lambda \in \theta$, $G_\phi$ is a tree.

(P3) *Toggling*: Every set $\Lambda \subseteq \theta$ of two or more linkings toggles a &-vertex that is in no switching cycle of $G_\Lambda$.

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 additive proof-nets [HvG05] and (P2) is the Danos-Regnier criterion for multiplicative proof-nets [DR89]. 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 [DG11] for a similar condition for example). Sets composed of a single linking $\lambda$ are not considered in (P3), for by (P2) the graph $G_\lambda$ has no switching cycle. One can check that our example on Figure 2, $\{\lambda_1; \lambda_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^\perp$. For $V$ a vertex in (the syntactic tree $T(A)$ of) $A$, we denote by $V^\perp$ the corresponding vertex in $A^\perp$. As expected, $V^{\perp\perp} = V$. This also respects orthogonality for formulas on leaves: given a leaf $l$ of $A$, labeled by a formula $X$, the label
<figure><img src="image_13.png" /><figcaption>Figure 2: Graphs from an example of a proof-net: from left to right $G_{\lambda_1}$, $G_{\lambda_2}$ and $G_{\{\lambda_1;\lambda_2\}}$</figcaption></figure>

of $l^{\perp}$ is $X^{\perp}$. We can also define a notion of duality on premises: given a premise of a vertex $V \in T(A)$, the dual premise of $V^{\perp}$ is the corresponding premise in $T(A^{\perp})$. In other words, if in $L - V - R$ we consider the premise $L$ then in $R^{\perp} - V^{\perp} - L^{\perp}$ its dual premise is $L^{\perp}$.

## 6.2. Cut-elimination in proof-nets.

**Definition 6.2 (Composition).** For proof-nets $\theta$ and $\psi$ of respective conclusions $[\Sigma] \Gamma, A$ and $[\Xi] \Delta, A^{\perp}$, the composition over $A$ of $\theta$ and $\psi$ is the proof-net $\theta \overset{A}{\rightleftharpoons} \psi = \{\lambda \cup \mu \mid \lambda \in \theta, \mu \in \psi\}$, with conclusions $[\Sigma, \Xi, A * A^{\perp}] \Gamma, \Delta$.

For example, see Figure 8 with a composition of the proof-nets on Figure 6.

**Definition 6.3 (Cut-elimination).** Let $\theta$ be a set of linkings on a cut sequent $[\Sigma] \Gamma$, and $A * A^{\perp}$ a cut pair in $\Sigma$. Define the *elimination* of $A * A^{\perp}$ (or of the cut $*$ between $A$ and $A^{\perp}$) as:

(a) If $A$ is an atom, delete $A * A^{\perp}$ from $\Sigma$ and replace any pair of links $(l, A)$, $(A^{\perp}, m)$ ($l$ and $m$ being other occurrences of $A^{\perp}$ and $A$ respectively) with the link $(l, m)$.

(b) If $A = A_1 \otimes A_2$ and $A^{\perp} = A_2^{\perp} \mathcal{Y} A_1^{\perp}$ (or vice-versa), replace $A * A^{\perp}$ with two cut pairs $A_1 * A_1^{\perp}$ and $A_2 * A_2^{\perp}$. Retain all original linkings.

(c) If $A = A_1 \& A_2$ and $A^{\perp} = A_2^{\perp} \oplus A_1^{\perp}$ (or vice-versa), replace $A * A^{\perp}$ with two cut pairs $A_1 * A_1^{\perp}$ and $A_2 * A_2^{\perp}$. Delete all *inconsistent* linkings, namely those $\lambda \in \theta$ such that in $[\Sigma] \Gamma \vdash \lambda$ the children $\&$ and $\oplus$ of the cut do not take dual premises. Finally, “garbage collect” by deleting any cut pair $B * B^{\perp}$ for which no leaf of $B * B^{\perp}$ is in any of the remaining linkings.

See Figure 9 for a result on applying steps (b) and (c) to the proof-net of Figure 8. We use for proof-nets the same notations $\overset{\beta}{\to}$ and $\stackrel{\beta}{=} \beta$ as for the sequent calculus.

**Proposition 6.4 [HvG05, Proposition 5.4].** *Eliminating a cut in a proof-net yields a proof-net.*

**Theorem 6.5 [HvG05, Theorem 5.5].** *Cut-elimination of proof-nets is strongly normalizing and confluent.*

A linking $\lambda$ on a cut sequent $[\Sigma] \Gamma$ *matches* if, for every cut pair $A * A^{\perp}$ in $\Sigma$, any given leaf $l$ of $A$ is in $[\Sigma] \Gamma \vdash \lambda$ if and only if $l^{\perp}$ of $A^{\perp}$ is in $[\Sigma] \Gamma \vdash \lambda$. 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* [HvG05], eliminating a cut in a single step by removing inconsistent linkings.
## 7. REDUCTION TO PROOF-NETS

The goal of this section is to shift the study of isomorphisms to the syntax of proof-nets, never to speak of sequent calculus again. We do so by first defining *desequentialization*, a function from sequent calculus proofs to proof-nets (Section 7.1). We then show that cut-elimination in proof-nets simulates the one from sequent calculus (Section 7.2). Finally, we define isomorphisms directly in the syntax of proof-nets (Section 7.3). Recall that all sequent calculus proofs we consider have expanded axioms, thanks to Proposition 3.3.

**7.1. Desequentialization.** We desequentialize a unit-free MALL proof $\pi$ (with expanded axioms) into a set of linkings $\mathcal{R}(\pi)$ by induction on $\pi$:

$$ \frac{\overline{\{((X, X^{\perp}))\} \triangleright [\emptyset] X, X^{\perp}}}{\{\lambda \cup \mu \mid \lambda \in \theta, \mu \in \psi\} \triangleright [\Sigma, \Xi, A * A^{\perp}] \Gamma, \Delta} ax \qquad \frac{\theta \triangleright [\Sigma] \Gamma}{\theta \triangleright [\Sigma] \sigma(\Gamma)} ex $$

$$ \frac{\theta \triangleright [\Sigma] A, \Gamma \qquad \psi \triangleright [\Xi] A^{\perp}, \Delta}{\{\lambda \cup \mu \mid \lambda \in \theta, \mu \in \psi\} \triangleright [\Sigma, \Xi, A * A^{\perp}] \Gamma, \Delta} \text{cut} $$

$$ \frac{\theta \triangleright [\Sigma] A, \Gamma \qquad \psi \triangleright [\Xi] B, \Delta}{\{\lambda \cup \mu \mid \lambda \in \theta, \mu \in \psi\} \triangleright [\Sigma, \Xi] A \otimes B, \Gamma, \Delta} \otimes \frac{\theta \triangleright [\Sigma] A, B, \Gamma}{\theta \triangleright [\Sigma] A \otimes B, \Gamma} \otimes \Sigma $$

$$ \frac{\theta \triangleright [\Xi] A, \Gamma \qquad \psi \triangleright [\Phi] B, \Gamma}{\theta \cup \psi \triangleright [\Xi, \Phi] A \& B, \Gamma} \& \qquad \frac{\theta \triangleright [\Sigma] A, \Gamma}{\theta \triangleright [\Sigma] A \oplus B, \Gamma} \oplus_1 \frac{\theta \triangleright [\Sigma] B, \Gamma}{\theta \triangleright [\Sigma] A \oplus B, \Gamma} \oplus_2 $$

This definition uses the implicit tracking of formula occurrences downwards through the rules, and follows [HvG05] with the notation $\theta \triangleright [\Sigma] \Gamma$ for "$\theta$ is a set of linkings on the cut sequent $[\Sigma] \Gamma$". As identified in [HvG05, Section 5.3.4], desequentializing with both *cut-* and *&-rules* is complex, for cuts can be shared (or not) when translating a *&-rule*: $\frac{\theta \triangleright [\Sigma, \Xi] A, \Gamma \qquad \psi \triangleright [\Sigma, \Phi] B, \Gamma}{\theta \cup \psi \triangleright [\Sigma, \Xi, \Phi] A \& B, \Gamma} \&$. We choose to never share cuts ($\Sigma = \emptyset$), thus desequentialization is a function. The cost being that the following $\&$-$cut$ commutation yields different proof-nets (contrary to the other commutations, see [HvG16]).

$$ \frac{\vdash_{\pi_1} A, B, \Gamma \quad \vdash_{\pi_2} A, C, \Gamma \quad \vdash_{\pi_3} A^{\perp}, \Delta}{\vdash_{\pi_1} A, B \& C, \Gamma \quad \& \quad \vdash_{\pi_2} A^{\perp}, \Delta}{\text{cut}} \equiv \frac{\vdash_{\pi_1} A, B, \Gamma \quad \vdash_{\pi_3} A^{\perp}, \Delta}{\vdash_{\pi_2} B, \Gamma, \Delta}{\text{cut}} \quad \frac{\vdash_{\pi_1} A, C, \Gamma \quad \vdash_{\pi_3} A^{\perp}, \Delta}{\vdash_{\pi_2} C, \Gamma, \Delta}{\text{cut}} \quad \& $$

**Remark 7.1.** An alternative definition of desequentialization in [HvG05] consists in building a linking by slice. In this spirit, if a proof-net $\theta$ is obtained by desequentializing a proof $\pi$, there is a bijection between linkings in $\theta$ and slices of $\pi$.

**Theorem 7.2 (Sequentialization [HvG05, Theorem 5.9]).** A set of linkings on a cut sequent is a translation of a unit-free MALL proof if and only if it is a proof-net.

**Definition 7.3 (Identity proof-net).** We call *identity proof-net* of a unit-free formula $A$, the proof-net corresponding to the proof $\mathrm{id}_A$ (the axiom-expansion of $ax_A = \frac{\vdash A^{\perp}, A}{\vdash} ax$).
<figure><img src="image_14.png" /><figcaption>Figure 3: Illustration of $\triangleleft$ (Definition 7.4) and correspondence with $\& - cut$ cut-elimination</figcaption></figure>

**7.2. Simulation of cut elimination.** We show here that cut elimination in proof-nets mimics the one in sequent calculus, which will allow us in the next section to consider isomorphisms on proof-nets only. As written in Section 7.1, proof-nets have difficulties with the $\& - cut$ commutation, which corresponds to superimposing $*$-vertices.

**Definition 7.4 ($\triangleleft$).** Let $\theta$ and $\psi$ be proof-nets. We denote $\theta \triangleleft \psi$ if there exists a $*$-vertex $C$ in $\theta$ such that the syntactic forest of $\psi$ is the syntactic forest of $\theta$ where the syntactic tree of $C$ is duplicated into the syntactic trees of $C_0$ and $C_1$ (which are different occurrences of $C$), $\theta = \theta_0 \sqcup \theta_1^2$ and $\psi = \psi_0 \sqcup \psi_1$ with, for $i \in \{0; 1\}$, $\psi_i = \theta_i$ up to assimilating $C_i$ with $C$.

See Figure 3 for a graphical representation of this concept, as well as the link with the $\& - cut$ commutative case of cut-elimination.

**Lemma 7.5 (Simulation - $\beta$).** Let $\pi$ and $\pi'$ be unit-free MALL proof trees such that $\pi \xrightarrow{\beta} \pi'$. Then either $R(\pi) = R(\pi')$, $R(\pi) \triangleleft R(\pi')$ or $R(\pi) \xrightarrow{\beta} R(\pi')$.

*Proof.* We reason by cases according to the step $\pi \xrightarrow{\beta} \pi'$. Recall we desequentialize by separating all cuts, and use the notations for steps from Definition 6.3. If $\pi \xrightarrow{\beta} \pi'$ is an ax (resp. $\mathcal{R} - \otimes, \& - \oplus$) key case, then using a step (a) (resp. (b), (c)), we get $R(\pi) \xrightarrow{\beta} R(\pi')$. If it is a $\mathcal{R} - cut, \otimes - cut - 1, \otimes - cut - 2, \oplus_1 - cut$ or $\oplus_2 - cut$ commutative case, then $R(\pi) = R(\pi')$. Finally, in a $\& - cut$ commutative case, we duplicate the cut-rule: $R(\pi) \triangleleft R(\pi')$ (see Figure 3). $\square$

Nonetheless, the $\triangleleft$ relation is not a hard problem since two proofs differing by a $\& - cut$ commutation yield proof-nets equal up to cut-elimination.

**Lemma 7.6 ($\triangleleft \subseteq =\beta$).** Let $\theta$ and $\theta'$ be proof-nets such that $\theta \triangleleft \theta'$. Then $\theta =_{\beta} \theta'$.

*Proof.* By Definition 7.4 of $\triangleleft$, there exists a $*$-vertex $C$ in $\theta$, with $\theta = \theta_0 \sqcup \theta_1$, such that $\theta'$ is $\theta$ where the syntactic tree of $C$ is duplicated into $C_0$ and $C_1$, and linkings in $\theta_0$ (resp. $\theta_1$) use $C_0$ (resp. $C_1$) as $C$.

We reason by induction on 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 $\theta$ yields a proof-net $\Theta$. On the other hand, a corresponding step of cut-elimination on $C_0$ and one on $C_1$ in $\theta'$ yields $\Theta'$.

<footnote n="2">²The symbol $\sqcup$ means a union $\cup$ which happens to be between disjoint sets.</footnote>
If A is an atom, then we applied step (a), and we find $\Theta = \Theta'$.

If A is a ⊗-formula, i.e. $A = A_0 \otimes A_1$, then we applied step (b) and produced cuts $A_0 * A_0^\perp$ and $A_1 * A_1^\perp$ in $\Theta$, and two occurrences of these cuts in $\Theta'$. Thus, $\Theta \triangleleft \Xi \triangleleft \Theta'$ with $\Xi$ the proof-net $\Theta$ where the cut on $A_0$ is duplicated. By induction hypothesis, $\Theta =_\beta \Xi =_\beta \Theta'$. It follows $\theta =_\beta \theta'$ as $\theta \xrightarrow{\beta} \Theta =_\beta \Theta' \leftarrow^\beta \cdot \leftarrow^\beta \theta'$.

Finally, if A is a ⊕-formula with $A = A_0 \oplus A_1$, then we used step (c), producing cuts $A_0 * A_0^\perp$ and $A_1 * A_1^\perp$ in $\Theta$, and two occurrences of these cuts in $\Theta'$. Remark that inconsistent linkings in $\theta'$ for these steps are exactly those of $\theta$, and therefore the same cuts are garbage collected. Whence, $\Theta \triangleleft \cdot \triangleleft \Theta'$, $\Theta \triangleleft \Theta'$ or $\Theta = \Theta'$ (according to the number of cuts garbage collected). In all cases, using the induction hypothesis we conclude $\theta =_\beta \theta'$. $\square$

**Remark 7.7.** Another proof of Lemma 7.6, using the Turbo Cut-elimination procedure and no induction, is possible. We use the Turbo Cut-elimination procedure on $C$ in $\theta$, yielding a proof-net $\Theta$; we also use it in $\theta'$ on $C_0$ then $C_1$, yielding $\Theta'$. Whence, $\theta \xrightarrow{\beta^*} \Theta$ and $\Theta' \xleftarrow{\beta^*} \theta'$. It remains to prove that $\Theta = \Theta'$. Remark that $\Theta$ and $\Theta'$ can only differ by their linkings, for they have the same syntactic forest. Notice that a linking in $\theta_i$, $i \in \{0; 1\}$, matches for $C$ in $\theta$ if and only if it matches for $C_i$ in $\theta'$, because this linking uses $C_i$ as $C$. Thence, the same linkings stay in $\Theta$ and $\Theta'$, and $\Theta = \Theta'$ follows.

**Theorem 7.8 (Simulation Theorem).** Let $\pi$ and $\pi'$ be unit-free MALL proof trees with expanded axioms. If $\pi =_\beta \pi'$, then $\mathcal{R}(\pi) =_\beta \mathcal{R}(\pi')$.

*Proof.* This is a corollary of Lemmas 7.5 and 7.6. $\square$

**7.3. Isomorphisms in proof-nets.** A notion of isomorphism $A \cong B$ can be defined directly on proof-nets: $\theta$ and $\psi$ are two cut-free proof-nets of respective conclusions $A^\perp$, $B$ and $B^\perp$, $A$ such that $\theta \bowtie^B \psi$ and $\psi \bowtie^A \theta$ reduce by cut-elimination to identity proof-nets. Thanks to the Simulation Theorem (Theorem 7.8), we obtain:

**Theorem 7.9 (Type isomorphisms in proof-nets).** Let $A$ and $B$ be two unit-free MALL formulas. If $A \cong B$ then there exist two proof-nets $\theta$ and $\psi$ such that $A \cong B$.

*Proof.* Using Lemma 2.9 followed by Proposition 3.3, there exist unit-free MALL cut-free proofs with expanded axioms $\pi$ and $\tau$, respectively of $\vdash A^\perp$, $B$ and $\vdash B^\perp$, $A$, such that $\pi \bowtie^B \tau =_\beta \mathrm{id}_A$ and $\tau \bowtie^A \pi =_\beta \mathrm{id}_B$. We will prove that $\mathcal{R}(\pi) \bowtie^B \mathcal{R}(\tau)$ reduces by cut-elimination to $\mathcal{R}(\mathrm{id}_A)$, and by symmetry a similar reasoning entails $\mathcal{R}(\tau) \bowtie^A \mathcal{R}(\pi)$ reduces to $\mathcal{R}(\mathrm{id}_B)$. This is enough to conclude: $\theta := \mathcal{R}(\pi)$ and $\psi := \mathcal{R}(\tau)$ are cut-free proof-nets whose composition over $B$ (resp. $A$) yields after cut-elimination the identity proof-net of $A$ (resp. $B$).

By the Simulation Theorem (Theorem 7.8), from $\pi \bowtie^B \tau =_\beta \mathrm{id}_A$ we deduce $\mathcal{R}(\pi) \bowtie^A \tau =_\beta \mathcal{R}(\mathrm{id}_A)$. But $\mathcal{R}(\pi) \bowtie^A \tau =_\beta \mathcal{R}(\pi) \bowtie^A \mathcal{R}(\tau)$ by definition of $\mathcal{R}$ (Section 7.1). Using convergence of cut-elimination (Theorem 6.5) and that $\mathcal{R}(\mathrm{id}_A)$ is cut-free, one gets $\mathcal{R}(\pi) \bowtie^A \mathcal{R}(\tau)$ reduces by cut-elimination to $\mathcal{R}(\mathrm{id}_A)$, as wanted. $\square$
**Remark 7.10.** The converse of Theorem 7.9 holds. Indeed, the goal of the next section is to prove $A \stackrel{\theta,\psi}{\simeq} B \implies A =_L B$. Therefore, using in addition Theorem 2.11:

$$A \stackrel{\theta,\psi}{\simeq} B \implies A =_L B \implies A \simeq B$$

## 8. COMPLETENESS

Our method relates closely to the one used by Balat and Di Cosmo in [BDC99], with some more work due to the distributivity isomorphisms. We work on proof-nets, as they highly simplify the problem by representing proofs up to rule commutations [HvG16]. The core of the proof is as follows. Looking at the expected isomorphisms between distributed formulas, there should be only associativity and commutativity, i.e. reordering of atoms in formulas. In particular, a proof-net of an isomorphism $A \simeq B$ should simply be a bijection between atoms of $A$ and atoms of $B$. We prove it is indeed the case: such a proof-net has a very particular shape with each atom of $A$ having a unique axiom link on it, which goes to an atom of $B$ (and vice-versa); we call bipartite $ax$-unique such a proof-net. Once this is proved, it is not difficult (albeit a bit long) to conclude only rearrangements of atoms are possible, so only associativity and commutativity of connectives. However, proving that proof-nets of an isomorphism are bipartite $ax$-unique is complicated; in particular, this only holds for isomorphisms between distributed formulas (e.g. the proof-nets of a distributivity isomorphism are not of this shape). This is why we go through intermediate steps: we first prove that axiom links are between $A$ and $B$ (i.e. there is no link between two atoms of $A$), then that every atom has a link on it, and finally we prove the unicity of this link. More formally, the special shapes of proof-nets we consider are the followings.

**Definition 8.1** (Full, $Ax$-unique, Bipartite proof-net). A 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$).

For instance:

* the three proof-nets on Figure 4 (page 38) are bipartite and $ax$-unique

* the top-left proof-net of Figure 5 (page 39) is non-bipartite, full and non-$ax$-unique; meanwhile, its top-right proof-net is bipartite and non-full (so non-$ax$-unique)

* both proof-nets on Figure 6 (page 41) are bipartite, full and non-$ax$-unique

Our proof of completeness can be sketched as follows:

(1) we start by studying identity proof-nets and easily prove they are bipartite $ax$-unique (Section 8.1);

(2) then, we show isomorphisms yield bipartite full proof-nets (Section 8.2) – the difficulty here is that bipartiteness and fullness are not preserved by cut anti-reduction, so we have to use a reasoning specific to isomorphisms;

(3) next is proven that distributed isomorphisms have $ax$-unique proof-nets (Section 8.3), which is the core of the argument and where we need the distributivity hypothesis;

(4) we then exploit bipartite $ax$-uniqueness so as to rename atoms in $A \simeq B$ to make $A$ and $B$ having no repetitions of atoms (i.e. each atom appears at most once in $A$), which is called *non-ambiguousness* (Section 8.4);
<figure><img src="image_15.png" /><figcaption>Figure 4: Identity proof-nets (from left to right: atom, $\mathfrak{N}\otimes$ and $\&\oplus$)</figcaption></figure>

(5) finally, isomorphisms between non-ambiguous formulas are easily characterized as being exactly compositions of associativity and commutativity (Section 8.5).

Looking at how isomorphisms of MLL are characterized in [BDC99], the key differences are that $ax$-uniqueness is given for free as there is no slice nor distributivity isomorphism. In particular, steps (4) and (5) are similar to their MLL counterpart – but more complex in MALL as there are more connectives.

**8.1. Properties of identity proof-nets.** Using an induction on the formula $A$, we can prove the following results on the identity proof-net of $A$, and in particular that it is bipartite $ax$-unique. See Figure 4 for a graphical intuition.

**Lemma 8.2.** *The axiom links of an identity proof-net are exactly the $(l, l^{\perp})$, for any leaf $l$.*

*Proof.* By induction on the formula (see Figure 4). $\square$

<figure><img src="image_16.png" /></figure>

**Corollary 8.3.** *An identity proof-net is bipartite $ax$-unique.*

*Proof.* This follows from Lemma 8.2. $\square$

<figure><img src="image_17.png" /></figure>

**Lemma 8.4.** Let $\lambda$ be a linking of an identity proof-net and $V$ an additive vertex in its additive resolution. Recall $V^{\perp}$ is the dual occurrence of $V$ in $A^{\perp}$ (resp. $A$) when $V$ belongs to $A$ (resp. $A^{\perp}$). Then $V^{\perp}$ is also inside the additive resolution of $\lambda$, and its kept premise in this resolution is the dual premise of the one kept for $V$ – i.e. if the left (resp. right) premise of $V$ is kept, then the right (resp. left) premise of $V^{\perp}$ is kept.

*Proof.* Assume w.l.o.g. that the left premise of $V$ is kept in $\lambda$. There is a left-ancestor $l$ of $V$ in the additive resolution of $\lambda$, hence with a link $a \in \lambda$ on it. By Lemma 8.2, $a = (l, l^{\perp})$. As $l^{\perp}$ is a right-ancestor of $V^{\perp}$, the conclusion follows. $\square$

<figure><img src="image_18.png" /></figure>

The next result allows to go from exactly one linking on any $\&$-resolution of $A^{\perp}$, $A$ – Definition 6.1 (P1) – to exactly one linking on any additive resolution of $A$.

**Lemma 8.5.** *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^{\perp}$, $A$ by taking the choices of premise of $R$ on $A$ and, for a $\&$-vertex $W$ of $A^{\perp}$, taking the dual premise chosen in $R$ for $W^{\perp}$. By Lemma 8.4, a linking $\lambda$ is on $R$ if and only if it is on $R'$. Meanwhile, by Definition 6.1 (P1) there is a unique linking $\lambda$ on $R'$; thus the same holds on $R$. $\square$

<figure><img src="image_19.png" /></figure>
<figure><img src="image_20.png" /><figcaption>Figure 5: Non bipartite proof-net (top-left), non full proof-net (top-right) and one of their compositions yielding the identity proof-net (bottom) (jump edges not represented)</figcaption></figure>

**8.2. Bipartite full proof-nets.** We prove here that proof-nets of isomorphisms are bipartite full. Neither fullness, *ax*-uniqueness nor bipartiteness is preserved by cut anti-reduction. A counter-example is given on Figure 5, with a non bipartite proof-net and a non full one whose composition reduces to the identity proof-net (bipartite *ax*-unique by Corollary 8.3). However, if *both* compositions yield identity proof-nets, we get bipartiteness and fullness.

**Lemma 8.6.** Let $\theta$ and $\theta'$ be cut-free proof-nets of respective conclusions $A^{\perp}, B$ and $B^{\perp}, A$, such that $\theta' \stackrel{A}{\rightleftharpoons} \theta$ reduces to the identity proof-net of $B$. For any linking $\lambda \in \theta$, there exists $\lambda' \in \theta'$ such that $\lambda \cup \lambda'$ matches in the composition $\theta \stackrel{B}{\rightleftharpoons} \theta'$ of $\theta$ and $\theta'$ over $B$.

*Proof.* Let us consider a linking $\lambda \in \theta$, and call $\mathcal{C}$ the choices of premise on additive connectives of $B$ that $\lambda$ makes. We search some $\lambda' \in \theta'$ making the dual choices of premise on additive connectives of $B^{\perp}$ compared to $\mathcal{C}$. Consider the composition of $\theta$ and $\theta'$ over $A$. It reduces to the identity proof-net of $B$ by hypothesis. By Lemma 8.5, there exists a unique linking $\nu$ in the identity proof-net of $B$ corresponding to $\mathcal{C}$. Furthermore, this linking $\nu$ of the identity proof-net is derived from some $\mu \cup \mu'$ for $\mu$ a linking of $\theta$ and $\mu'$ one of $\theta'$, with $\mu \cup \mu'$ matching for a cut over $A$: a linking in the identity proof-net is a linking of the form $\mu \cup \mu'$ where axiom links $(l, m_1)$, $(m_1^{\perp}, m_2)$, ..., $(m_n^{\perp}, l^{\perp})$ in $\mu$ and $\mu'$ are replaced with $(l, l^{\perp})$, with $l$ a leaf of $B$ and the $m_i$ and $m_i^{\perp}$ of $A^{\perp}$ and $A$ (because an identity proof-net has only links of the form $(l, l^{\perp})$ by Lemma 8.2). Therefore, $\mu$ makes the choices $\mathcal{C}$ on $B$ and $\mu \cup \mu'$ matches for the composition of $\theta$ and $\theta'$ over both $A$ and $B$. But $\lambda$ makes the same choices $\mathcal{C}$ on $B$ as $\mu$: $\lambda \cup \mu'$ also matches for a cut over $B$. $\square$

**Remark 8.7.** Lemma 8.6 is the analogue of Lemma 5.13 in proof-nets. Indeed, Lemma 5.13 states that given two sequent calculus proofs $\pi$ and $\pi'$ composing to the identity on $B$, and $s$ a slice of $\pi$, there exists a slice $s'$ of $\pi'$ such that $s \stackrel{B}{\rightleftharpoons} s'$ does not fail when reducing cuts –
i.e. the two slices make the dual choices for additive connectives in B. Seeing a linking as a slice, this corresponds to having two matching linkings.

**Corollary 8.8.** *Assuming $A \simeq B$, $\theta$ and $\theta'$ are bipartite.*

*Proof.* We proceed by contradiction: w.l.o.g. there is a link $a$ in some linking $\lambda \in \theta$ which is between leaves of $A^{\perp}$. Remember that in the notation $A \simeq B$, both proof-nets $\theta$ and $\theta'$ are assumed cut-free. Thence, one can apply Lemma 8.6: there exists $\lambda' \in \theta'$ such that $\lambda \cup \lambda'$ matches for a cut over $B$. For $a$ does not involve leaves of $B$, it stays in the linking of the normal form resulting from $\lambda \cup \lambda'$ (after eliminating all cuts in the composition). But this normal form is by hypothesis the identity proof-net of $A$, which is bipartite by Corollary 8.3. Thus, there cannot be an axiom link between leaves of $A^{\perp}$ inside: contradiction. $\square$

**Lemma 8.9.** *Assume $\theta$ and $\theta'$ are cut-free proof-nets of respective conclusions $A^{\perp}, B$ and $B^{\perp}, A$, and that their composition over $B$ reduces to the identity proof-net of $A$. Then any leaf of $A^{\perp}$ (resp. $A$) has at least one axiom link on it in $\theta$ (resp. $\theta'$).*

*Proof.* Towards a contradiction, assume w.l.o.g. a leaf $l$ of $A^{\perp}$ has no link on it in $\theta$. Then, the composition over $B$ of $\theta$ and $\theta'$ 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, n)$. However, the identity proof-net of $A$ is ax-unique by Corollary 8.3, thence full: contradiction. $\square$

**Remark 8.10.** Lemma 8.9 holds not only for isomorphisms but more generally for retractions, which are formulas $A$ and $B$ such that there exist proofs $\pi$ of $\vdash A^{\perp}, B$ and $\pi'$ of $\vdash B^{\perp}, A$ whose composition by cut over $B$ (but not necessarily over $A$) is equal to the axiom on $\vdash A^{\perp}, A$ up to axiom-expansion and cut-elimination. An example of retraction is given by the proof-nets on Figure 5, yielding a retraction between $(A \not\propto A^{\perp}) \otimes B$ and $((A \not\propto A^{\perp}) \otimes B) \oplus B$, which is not an isomorphism. As another example, in MLL there is a well-known retraction between $A$ and $(A \dashv A) \dashv A = (A \otimes A^{\perp}) \not\propto A$.

**Theorem 8.11.** *Assuming $A \simeq B$, $\theta$ and $\theta'$ are bipartite full.*

*Proof.* By Corollary 8.8, $\theta$ and $\theta'$ are bipartite, and thanks to Lemma 8.9, they are full. $\square$

### 8.3. Ax-uniqueness.
In general, isomorphisms do not yield ax-unique proof-nets. A counter-example is distributivity: $A \otimes (B \oplus C) \simeq (A \otimes B) \oplus (A \otimes C)$, see Figure 6. Nonetheless, distributivity equations are the only unit-free equations in $\mathcal{L}$ not giving ax-unique proof-nets. Recall we can consider only distributed formulas (Proposition 5.5). On distributed formulas, distributivity isomorphisms can be ignored, and isomorphisms between distributed formulas happen to be bipartite ax-unique.

#### 8.3.1. Preliminary results.
We mostly use the correctness criterion through the fact we can sequentialize, i.e. recover a proof tree from a proof-net by Theorem 7.2. However, in order to prove ax-uniqueness, we make a direct use of the correctness criterion itself to deduce geometric properties of proof-nets. This part of the proof benefits from the specifics of this syntax. We begin with two preliminary results. For $\Lambda$ a set of linkings and $W$ a $\&$-vertex, let $\Lambda^W$ denote the set of all linkings in $\Lambda$ whose additive resolution does not contain the right argument of $W$. In this definition – taken from [HvG05] – we could have chosen left
<figure><img src="image_21.png" /><figcaption>Figure 6: Proof-nets for $A \otimes (B \oplus C) \simeq (A \otimes B) \oplus (A \otimes C)$</figcaption></figure>

argument instead of right argument, meaning the asymmetry is irrelevant. We use $\Lambda^W$ to deduce from the toggling condition – Definition 6.1 (P3) – a simpler and easier to manipulate (but weaker) condition that a proof-net respects, using that $W$ is not toggled by $\Lambda^W$. Then, given proof-nets of an isomorphism that are not $ax$-unique, we will show they do not respect this simpler condition, hence we will reach a contradiction.

**Lemma 8.12** (Adaptation of Lemma 4.32 in [HvG05]). Let $\omega$ be a jump-free switching cycle in a proof-net $\theta$. There exists a subset of linkings $\Lambda \subseteq \theta$ and a $\&$-vertex $W$ toggled by $\Lambda$ such that $\omega \subseteq \mathcal{G}_{\Lambda}$, $\omega \not\subseteq \mathcal{G}_{\Lambda W}$ and there exists an axiom link $a \in \omega$ depending on $W$ in $\Lambda$.

*Proof.* The proof of this lemma uses some facts from [HvG05] reproduced verbatim here. Write $\lambda \stackrel{W}{\rightleftharpoons} \lambda'$ if linkings $\lambda, \lambda' \in \theta$ are either equal or $W$ is the only $\&$ toggled by $\{\lambda, \lambda'\}$. A subset $\Lambda$ of a proof-net $\theta$ is *saturated* if any strictly larger subset toggles more $\&$ than $\Lambda$. It is straightforward to check that:

(S1) If $\Lambda$ is saturated and toggles $W$, then $\Lambda^W$ is saturated.

(S2) If $\Lambda$ is saturated and toggles $W$ and $\lambda \in \Lambda$, then $\lambda \stackrel{W}{\rightleftharpoons} \lambda_W$ for some $\lambda_W \in \Lambda^W$.

Let us now prove our lemma. Take $\Lambda$ a minimal saturated subset of $\theta$ with $\mathcal{G}_{\Lambda}$ containing $\omega$, and $W$ a $\&$-vertex it toggles. Since $\Lambda$ is minimal, $\omega \not\subseteq \mathcal{G}_{\Lambda W}$ using (S1), so some edge $e$ of $\omega$ is in $\mathcal{G}_{\Lambda}$ but not in $\mathcal{G}_{\Lambda W}$. We claim that, without loss of generality, $e$ is an axiom link. If it is indeed the case then, by (S2), $e \in \lambda \in \Lambda$ and $e \notin \lambda_W$ for $e \notin \Lambda^W$, so $e$ depends on $W$ in $\Lambda$. 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 \to X$ in $\omega$ we have $l \to Z_1 \to \dots \to Z_n \to Y \to X$ in $\omega$ for some leaf $l$, and $Y \to X$ is in $\mathcal{G}_{\Lambda W}$ whenever $l \to Z_1$ is in $\mathcal{G}_{\Lambda W}$. This is because a switching cycle must have an edge using a leaf, for all other edges are in the syntactic forest of the sequent, which is acyclic.

Still without loss of generality, $e$ is not an edge in a syntactic tree. Indeed, in such a case $e \notin \mathcal{G}_{\Lambda W}$ implies $l \notin \mathcal{G}_{\Lambda W}$. As $e$ belongs to the switching cycle $\omega$, let us look at the other edge in this cycle with endpoint $l$, say $e'$. As $l \notin \mathcal{G}_{\Lambda W}$, we also have $e' \notin \mathcal{G}_{\Lambda W}$. Remark that $e'$ cannot be an edge in a syntactic 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 syntactic tree.

As $\omega$ is jump-free, $e$ cannot be a jump edge. The sole possibility is $e$ being a link. $\square$

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 ancestor respecting this property, with a tree represented with its root at the bottom, which is a *descendant* of the leaves. Or equivalently, looking at a tree as a partial order of minimal element the root, the first common descendant is the infimum.

**Lemma 8.13.** Let $\theta$ be a proof-net of conclusions $\Gamma, A$, with a jump edge $l \stackrel{j}{\to} W$ between $l, W \in T(A)$. If $W$ is not a descendant of $l$, then their first common descendant $C$ is a $\mathcal{N}$.
<figure><img src="image_22.png" /><figcaption>Figure 7: Illustration of the proof of Lemma 8.13</figcaption></figure>

*Proof.* As there is a jump $l \xrightarrow{j} W$, there exist linkings $\lambda, \lambda' \in \theta$ such that $W$ is the only & toggled by $\{\lambda; \lambda'\}$, and a link $a \in \lambda \setminus \lambda'$ using the leaf $l$. In particular, the jump $l \xrightarrow{j} W$ is in $G_{\{\lambda; \lambda'\}}$. For $l$ and $W$ are both in the additive resolution of $\lambda$, both premises of $C$ are also in this additive resolution, thus $C$ cannot be an additive connective, so not a & nor a $\oplus$-vertex.

Assume by contradiction that $C$ is a $\otimes$. Call $\delta$ the path in $T(A)$ from $W$ to $C$, and $\mu$ the one from $C$ to $l$ (see Figure 7). Then, $(l \xrightarrow{j} W)\delta\mu$ is a switching cycle in $G_{\{\lambda; \lambda'\}}$. According to Definition 6.1 (P3), there exists a & toggled by $\{\lambda; \lambda'\}$ not in any switching cycle of $G_{\{\lambda; \lambda'\}}$. A contradiction, for $W$ is the only & toggled by $\{\lambda; \lambda'\}$. Whence, $C$ can only be a $\mathcal{Y}$-vertex. $\square$

### 8.3.2. *Isomorphisms of distributed formulas.*
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 6 (on page 41). Composing them together by cut on $(A \otimes B) \oplus (A \otimes C)$ gives the proof-net illustrated on Figure 8. Reducing all cuts not involving atoms yields the proof-net on Figure 9, that we call an *almost reduced composition*. We observe here a switching cycle produced by the two links on $A$ (dashed in blue on Figure 9), less visible in the non-reduced composition of Figure 8 – remember that in MALL proof-nets some switching cycles are allowed, and this is one of those. If we continue to reduce cuts, also eliminating the atomic ones, we obtain the identity proof-net, which has no switching cycle: during these reductions, both links on $A$ are merged. The idea of this section is to proceed by contradiction, considering a non-*ax*-unique proof-net of an isomorphism. We argue that, taking the almost reduced composition of the considered proof-nets, links preventing *ax*-uniqueness yield switching cycles. Then, we prove that for these switching cycles not to contradict the toggling condition of proof-nets (Definition 6.1 (P3)), there must be a non-distributed formula, reaching a contradiction.

**Definition 8.14** (Almost reduced composition). Take $\theta$ and $\theta'$ cut-free proof-nets of respective conclusions $\Gamma, B$ and $B^\perp, \Delta$. The *almost reduced composition* over $B$ of $\theta$ and $\theta'$ is the proof-net resulting from the composition over $B$ of $\theta$ and $\theta'$ where we repeatedly reduce all cuts not involving atoms (i.e. not applying step (a) of Definition 6.3).

Let us fix $A$ and $B$ two unit-free MALL (not necessarily distributed yet) formulas as well as $\theta$ and $\theta'$ such that $A \stackrel{\theta, \theta'}{\cong} B$. By Theorem 8.11, $\theta$ and $\theta'$ are bipartite full. We denote
<figure><img src="image_23.png" /><figcaption>Figure 8: Proof-nets from Figure 6 composed by cut on $(A \otimes B) \oplus (A \otimes C)$</figcaption></figure>

<figure><img src="image_24.png" /><figcaption>Figure 9: An almost reduced composition of the proof-nets on Figure 6</figcaption></figure>

<figure><img src="image_25.png" /><figcaption>Figure 10: Illustration of Lemma 8.15</figcaption></figure>

by $\psi$ the almost reduced composition over $B$ of $\theta$ and $\theta'$. Here, we can extend our duality on vertices and premises (defined in Section 6) to links.

**Lemma 8.15.** An axiom link $a = (l, m)$ belongs to some linking $\lambda \in \psi$ if and only if, up to swapping $l$ and $m$, $l$ is a leaf of $A^{\perp}$ (resp. $A$), $m$ is in the leaves of $B$ (resp. $B^{\perp}$) and there is an axiom link $(l^{\perp}, m^{\perp})$ in the same linking $\lambda$, that we will denote $a^{\perp} = (l^{\perp}, m^{\perp})$ (see Figure 10).

*Proof.* By symmetry, we only need to prove the “if” statement. Linkings of $\psi$ are disjoint union of linkings in $\theta$ and $\theta'$. By symmetry, assume $(l, m) \in \lambda \in \psi$ comes from a linking in $\theta$. As $\theta$ is bipartite, one of the leaves, say $l$, is in $A^{\perp}$ and the other, $m$, is a leaf of $B$. Since the cut $m * m^{\perp}$ belongs to the additive resolution of $\lambda$ ($m$ is inside), $m^{\perp}$ is a leaf in this resolution. Thus, there is a link $(m^{\perp}, l') \in \lambda$ for some leaf $l'$, which necessarily belongs to $A$ by bipartiteness of $\theta'$. It remains to prove $l' = l^{\perp}$. If we were to eliminate all cuts in $\psi$, we would get the identity proof-net on $A$ by hypothesis. But eliminating the cut $m * m^{\perp}$ yields a link $(l, l')$, which is not modified by the elimination of the other atomic cuts. By Lemma 8.2, $l' = l^{\perp}$ follows. □

**Lemma 8.16.** Let $\lambda$ be a linking of $\psi$, and $V$ an additive vertex in its additive resolution. Then $V^{\perp}$ 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 $\lambda$. There is a left-ancestor $l$ of V in the additive resolution of $\lambda$, hence with a link $a \in \lambda$ on it. By Lemma 8.15, we have $a^{\perp} \in \lambda$, using $l^{\perp}$. As $l^{\perp}$ is a right-ancestor of $V^{\perp}$, the conclusion follows. $\square$

**Lemma 8.17.** Let W and P be respectively a $\&$-vertex and a $\oplus$-vertex in $\psi$, with W an ancestor of P. Then for any axiom link a depending on W in $\psi$, a also depends on $P^{\perp}$ in $\psi$.

*Proof.* There exist linkings $\lambda, \lambda' \in \psi$ such that W is the only $\&$ toggled by $\{\lambda; \lambda'\}$ and $a \in \lambda \setminus \lambda'$. We consider a linking $\lambda_{P^{\perp}}$ defined by taking an arbitrary $\&$-resolution of $\lambda$ where we choose the other premise for $P^{\perp}$ (and arbitrary premises for $\&$-vertices introduced this way, meaning for $\&$-ancestors of $P^{\perp}$): by Definition 6.1 (P1), there exists a unique linking on it. By Lemma 8.16, the additive resolutions of $\lambda$ and $\lambda_{P^{\perp}}$ (resp. $\lambda$ and $\lambda'$) differ, on A and $A^{\perp}$, exactly on ancestors of P and $P^{\perp}$ (resp. W and $W^{\perp}$). Thus, the additive resolutions of $\lambda'$ and $\lambda_{P^{\perp}}$ also differ, on A and $A^{\perp}$, exactly on ancestors of P and $P^{\perp}$, for W is an ancestor of P. In particular, $\{\lambda; \lambda_{P^{\perp}}\}$, as well as $\{\lambda'; \lambda_{P^{\perp}}\}$, toggles only $P^{\perp}$. If $a \in \lambda_{P^{\perp}}$, then $a$ depends on $P^{\perp}$ in $\{\lambda'; \lambda_{P^{\perp}}\}$. Otherwise, $a$ depends on $P^{\perp}$ in $\{\lambda; \lambda_{P^{\perp}}\}$. $\square$

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 \xrightarrow{j} W$.

**Lemma 8.18.** Let $l \xrightarrow{j} W$ be a jump edge in $\psi$, with $l$ not an ancestor of W and $l, W \in T(A^{\perp})$ (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^{\perp})$ (resp. $T(A)$).

*Proof.* Let P be a vertex on the path between N and W in $T(A^{\perp})$. By Lemma 8.13, N is a $\mathfrak{N}$-vertex. We prove by contradiction that P can neither be a $\oplus$ nor a $\otimes$-vertex.

Suppose P is a $\oplus$-vertex. By Lemma 8.17, $a$ depends on $P^{\perp}$, and so does $a^{\perp}$ through Lemma 8.15: there is a jump edge $l^{\perp} \xrightarrow{j} P^{\perp}$. Applying Lemma 8.13, the first common descendant of $l^{\perp}$ and $P^{\perp}$, which is $N^{\perp}$, is a $\mathfrak{N}$-vertex: a contradiction as it is a $\otimes$-vertex.

Assume now P to be a $\otimes$-vertex. As there is a jump $l \xrightarrow{j} W$, there exist linkings $\lambda, \lambda' \in \psi$ and a leaf $m$ of B such that W is the only $\&$ toggled by $\{\lambda; \lambda'\}$ and $a = (l, m) \in \lambda \setminus \lambda'$. For P is a $\otimes$, there is a leaf $p$ which is an ancestor of P in the additive resolution of $\lambda$, from a different premise of P than W; it is used by a link $b = (p, q) \in \lambda$ (see Figure 11). Remark $q \neq m$, for $a$ and $b$ are two distinct links in the same linking $\lambda$. Then the switching cycle $l \xrightarrow{j} W \to P \leftarrow p \xrightarrow{b} q \to * \leftarrow q^{\perp} \xrightarrow{b^{\perp}} p^{\perp} \to P^{\perp} \to N^{\perp} \leftarrow l^{\perp} \xrightarrow{a^{\perp}} m^{\perp} \to * \leftarrow m \xrightarrow{a} l$ (dashed in blue on Figure 11) belongs to $G_{\{\lambda; \lambda'\}}$, where unlabeled arrows are paths in the syntactic forest. Contradiction: W, the only $\&$ toggled by $\{\lambda; \lambda'\}$, cannot be in any switching cycle of $G_{\{\lambda; \lambda'\}}$ by Definition 6.1 (P3). $\square$

**Theorem 8.19.** *Assuming $A \simeq B$ with A and B distributed, $\theta$ and $\theta'$ are bipartite ax-unique.*

*Proof.* We already know that $\theta$ and $\theta'$ are bipartite full thanks to Theorem 8.11. We reason by contradiction and assume w.l.o.g. that $\theta$ is not ax-unique: there exist a leaf $l$ of $A^{\perp}$ and two distinct leaves $l_0$ and $l_1$ of B with links $a = (l, l_0)$ and $b = (l, l_1)$ in $\theta$. We consider $\psi$ the almost reduced composition of $\theta$ and $\theta'$ over B, depicted on Figure 12. By Lemma 8.6, $a$ and $b$ are also links in $\psi$ (for the linkings they belong to in $\theta$ have matching linkings in $\theta'$, and we did not eliminate atomic cuts). Using Lemma 8.15, we have in $G_{\psi}$ a switching cycle $\omega = l \xrightarrow{a} l_0 \to * \leftarrow l_0^{\perp} \xrightarrow{b^{\perp}} l^{\perp} \to * \leftarrow l_1 \xrightarrow{b} l$.
<figure><img src="image_26.png" /><figcaption>Figure 11: Switching cycle containing $W$ if $P$ is a $\otimes$-vertex in the proof of Lemma 8.18</figcaption></figure>

<figure><img src="image_27.png" /><figcaption>Figure 12: Almost reduced composition $\psi$ of $\theta$ and $\theta'$ by cut over $B$ in the proof of Theorem 8.19</figcaption></figure>

Let $\Lambda$ be a set of linkings and $W$ an associated $\&$-vertex given by Lemma 8.12 applied to $\omega$. The vertex $W$ belongs to either $T(A)$ or $T(A^{\perp})$: up to swapping them, $W$ is in $T(A^{\perp})$. By Lemma 8.12, $a, a^{\perp}, b$ or $b^{\perp}$ depends on $W$. So $a$ or $b$ depends on $W$ by Lemma 8.15; w.l.o.g. $a$ depends on $W$. 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 $\Lambda^W$, so $a^{\perp}$ and $b^{\perp}$ too (Lemma 8.15); thus $\omega \subseteq \mathcal{G}_{\Lambda^W}$, contradicting Lemma 8.12. Hence, $l$ is not an ancestor of $W$, and we can apply Lemma 8.13: the first common descendant $N$ of $l$ and $W$ in $T(A^{\perp})$ is a $\mathcal{Y}$. Using Lemma 8.18, there is no $\otimes \setminus \oplus$-vertex on the path between the $\mathcal{Y}$-vertex $N$ and its ancestor the $\&$-vertex $W$ in $T(A^{\perp})$. But then, considering the first $\&$-vertex in this path, there is a sub-formula of the shape $-(\mathcal{Y}(-\&-))$ or $-(\&-)\mathcal{Y} -$ in the distributed $A^{\perp}$, a contradiction. $\square$

**8.4. Non-ambiguous formulas.** Once our study is restricted to bipartite *ax-unique* proof-nets, we can also restrict formulas further. This will make apparent that isomorphisms can only be associativity and commutativity.

**Definition 8.20 (Non-ambiguous formula).** A formula $A$ is *non-ambiguous* if each atom in $A$ occurs at most once (whether positively or negatively). Otherwise, $A$ is called *ambiguous*.

**Fact 8.21.** If $A$ is non-ambiguous, so is $A^{\perp}$.
For instance, $X \& Y^{\perp}$ is non-ambiguous, whereas $(A \otimes B) \oplus (A \otimes C)$ is ambiguous. The reduction to non-ambiguous formulas requires to restrict to distributed formulas first: in $(A \otimes B) \oplus (A \otimes C) \simeq A \otimes (B \oplus C)$ we need the two occurrences of $A$ to factorize. The goal of this section is to prove that we can consider only non-ambiguous formulas (Proposition 8.25) and that isomorphisms between these formulas correspond simply to the existence of arbitrary proof-nets (Theorem 8.30). These two results are an adaptation of the work on MLL by Balat & Di Cosmo [BDC99, Section 3].<fnref n="3" />

**8.4.1. Reduction to non-ambiguous formulas.** Given $A \simeq B$ with $A$ or $B$ ambiguous, we replace occurrences of atoms by new fresh atoms to obtain an isomorphism $A' \simeq B'$ between non-ambiguous formulas. This is possible thanks to ax-unicity of the proof-nets. An important remark is that these “replacements of occurrences” are more general than substitutions, because we may replace different occurrences of the same atom by different atoms (or negated atoms) in a formula, i.e. we work at the level of occurrences instead of atoms.

**Lemma 8.22.** *Take $\theta$ an ax-unique cut-free proof-net with $(X, X^{\perp})$ one of its axiom links. For any atom (or negated atom) $Y$, the set of linkings obtained from $\theta$ by replacing the occurrences $X$ and $X^{\perp}$ by $Y$ and $Y^{\perp}$ – in both the conclusion formulas and the linkings of $\theta$ – is a proof-net.*

*Proof.* Call $A'$ and $B'$ the formulas $A$ and $B$ where the occurrences $X$ and $X^{\perp}$ are replaced by $Y$ and $Y^{\perp}$. The resulting set of linkings is indeed a proof-net on $A'$, $B'$, because the sole use of labels of leaves is to ensure an axiom link is between dual atoms (at least without cut). In particular, labels do not matter in the correctness criterion. $\square$

**Lemma 8.23.** *Assume $A \simeq B$ with $\theta$ and $\psi$ bipartite ax-unique proof-nets. Take $X_1^{\perp}$ and $X_2$ occurrences of the atoms $X^{\perp}$ and $X$ in $A^{\perp}$ and $B$, and call $X_1$ and $X_2$ respectively their dual occurrences in $A$ and $B^{\perp}$ (i.e. the occurrences given by the duality function). There is an axiom link $(X_1^{\perp}, X_2)$ in $\theta$ if and only if $(X_1, X_2^{\perp})$ is an axiom link in $\psi$.*

*Proof.* By symmetry, it suffices to prove that if $(X_1^{\perp}, X_2)$ is an axiom link in $\theta$, then $(X_1, X_2^{\perp})$ is an axiom link in $\psi$. By bipartite ax-uniqueness, $(X_1^{\perp}, X_2)$ is the sole axiom link of $\theta$ using $X_1^{\perp}$, and $\psi$ has a unique axiom link $(X_2^{\perp}, X_3)$ on $X_2^{\perp}$ – with $X_3$ an occurrence in $A, B^{\perp}$ of the same atom as $X_1$. Assume w.l.o.g. that $X_2$ is in $B$, so that $X_1$ and $X_3$ are both in $A$. When composing $\theta$ and $\psi$ by cut over $B$ and reducing all cuts, one gets the identity proof-net of $A$, where there is a unique link on $X_1^{\perp}$, linking it to $X_1$ (Lemma 8.2). But the sole link on $X_1^{\perp}$ that may result from this composition is $(X_1^{\perp}, X_3)$. Thence, $X_1 = X_3$ and $(X_1, X_2^{\perp})$ is a link of $\psi$. $\square$

**Lemma 8.24 (Distributed ambiguous isomorphic formulas).** Let $A$ and $B$ be distributed formulas such that $A \simeq B$. There exists a substitution $\sigma$ and distributed formulas $A'$ and $B'$, non-ambiguous, such that $A = \sigma(A')$, $B = \sigma(B')$ and $A' \simeq B'$ for some proof-nets $\theta'$ and $\psi'$.

<footnote n="3">³Our definition of non-ambiguous is stronger than the one from [BDC99] (less formulas are non-ambiguous here). In [BDC99], a formula $A$ is non-ambiguous if each atom in $A$ occurs at most once positive and once negative. This makes for instance $X \& X^{\perp}$ non-ambiguous, whereas by our definition it is ambiguous.</footnote>
**Proof.** For each axiom link $a_\theta = (X^\perp, X)$ of $\theta$, there is an axiom link $a_\psi = (X, X^\perp)$ in $\psi$ between the dual occurrences, and vice-versa (Lemma 8.23). Replace these occurrences of $X^\perp$ and $X$ in $A^\perp$, $B$ and $\theta$ by respectively $Y_a^\perp$ and $Y_a$, for $Y_a$ a fresh atom – with a different fresh atom $Y_a$ for each link $a_\theta$. This operation yields a proof-net $\theta'$ on $A'^\perp$, $B'$ (by repeated applications of Lemma 8.22). Similarly, replace each link $a_\psi = (X, X^\perp)$ in $\psi$ by $(Y_a, Y_a^\perp)$ – with $Y_a$ the fresh atom used for the link $a_\theta = (X^\perp, X)$ of $\theta$. Again, the resulting $\psi'$ is a proof-net (Lemma 8.22), on $B'^\perp$, $A'$ as we renamed occurrences dually. Since cut-elimination does not depend on labels, the compositions of $\theta'$ and $\psi'$ reduces to the identity proof-nets of $A'$ and $B'$: hence $A' \simeq B'$. Remark that $A$ (resp. $B$) is obtained from $A'$ (resp. $B'$) by substituting each $Y_a$ by the atom $X$ of $a_\theta$, for $Y_a$ was fresh. $\square$

**Proposition 8.25 (Reduction to distributed non-ambiguous formulas).** If $\mathcal{A}_C$ is complete for isomorphisms (of proof-nets) between unit-free MALL formulas that are distributed and non-ambiguous, then it is complete for isomorphisms (of proof-nets) between unit-free MALL formulas that are distributed. In other words: assume that for all distributed and non-ambiguous unit-free MALL formulas $A'$ and $B'$, $A' \simeq_B A$ if and only if there exists a substitution $\theta, \psi$ such that $A' =_{\mathcal{A}_C} B'$; then it holds for all distributed unit-free MALL formulas $A$ and $B$, $A \simeq_B A$ if and only if $A =_{\mathcal{A}_C} B$.

**Proof.** Take $A$ and $B$ some distributed unit-free MALL formulas, and assume there exist proof-nets $\theta$ and $\psi$ such that $A \simeq_B A$. Using Lemma 8.24, there is a substitution $\sigma$ and distributed non-ambiguous formulas $A'$ and $B'$ such that $A = \sigma(A')$, $B = \sigma(B')$ and $A' \simeq_B A$ for some proof-nets $\theta'$ and $\psi'$. By completeness hypothesis on $\mathcal{A}_C$ between distributed and non-ambiguous formulas, $A' =_{\mathcal{A}_C} B'$. As a substitution preserves the equations of an equational theory, it follows that $A = \sigma(A') =_{\mathcal{A}_C} \sigma(B') = B$. $\square$

8.4.2. *Simplification with non-ambiguous formulas.* The goal of this part is to show isomorphisms between non-ambiguous formulas correspond simply to the existence of proof-nets, speaking no more about cut-elimination nor identity proof-nets. This is done through Theorem 8.30: when $A$ is non-ambiguous, having proof-nets on $A^\perp$, $B$ and $B^\perp$, $A$ is enough to know their composition over $B$ composes to the identity proof-net of $A$ – simply because this is the sole proof-net on $A^\perp$, $A$. This result will be deduced by proving properties close to the ones of identity proof-nets from Section 8.1.

**Lemma 8.26.** Let $\theta$ be a proof-net of conclusions $A^\perp$, $A$, with $A$ a non-ambiguous formula. Axiom links of $\theta$ are of the form $(l^\perp, l)$ for $l$ a leaf of $A$.

**Proof.** Let $a$ be an axiom link of $\theta$, between leaves $l$ and $m$, with the label of $l$ (resp. $m$) being $X$ (resp. $X^\perp$). By non-ambiguity of $A$, and so $A^\perp$ (Fact 8.21), $X$ (and $X^\perp$) occurs exactly once in $A^\perp$, $A$ (counting $X$ and $X^\perp$ differently). Moreover, the unique leaf labeled $X^\perp$ is the dual of the leaf labeled $X$. Thus, $m = l^\perp$ and $a = (l, l^\perp)$. $\square$

**Lemma 8.27.** Let $\theta$ be a proof-net of conclusions $A^\perp$, $A$, with $A$ a non-ambiguous formula. Take a linking $\lambda \in \theta$ and an additive vertex $V$ in its additive resolution. The vertex $V^\perp$ is in the additive resolution of $\lambda$, and $\lambda$ keeps for $V^\perp$ the dual premise it keeps for $V$.
<figure><img src="image_28.png" /><figcaption>Figure 13: Identity proof-net of $X \mathcal{N} X$ (left-side) and the swap on this formula (right-side)</figcaption></figure>

*Proof.* As $V$ is in the additive resolution $A^{\perp}$, $A \upharpoonright \lambda$ of $\lambda$, one of its ancestor leaves, say $l$, is in $A^{\perp}$, $A \upharpoonright \lambda$: there is a link $a \in \lambda$ on it. By Lemma 8.26, $a = (l, l^{\perp})$. But $l^{\perp}$ is an ancestor of $V^{\perp}$, so $V^{\perp}$ is in $A^{\perp}$, $A \upharpoonright \lambda$, with as premise the dual premise chosen for $V$. $\square$

**Lemma 8.28.** For $A$ a non-ambiguous formula, there is exactly one proof-net of conclusions $A^{\perp}$, $A$: the identity proof-net of $A$.

*Proof.* We prove that for any proof-nets $\theta$ and $\theta'$ of conclusions $A^{\perp}$, $A$, it holds that $\theta = \theta'$. Hence the result when $\theta'$ is the identity proof-net.

Take $\lambda \in \theta$ a linking. It is on some $\&$-resolution $R$ of $A^{\perp}$, $A$. By Definition 6.1 (P1), there exists a unique linking $\lambda' \in \theta'$ on $R$. We wish to prove $\lambda = \lambda'$. They have the same additive resolution, for their choice on a $\oplus$-vertex $P$ is determined by the premise taken for the $\&$-vertex $P^{\perp}$, which is in $R$ (Lemma 8.27). They have the same axiom links on this additive resolution, because any leaf on it is linked to its dual (Lemma 8.26). Therefore, $\lambda = \lambda'$, so $\theta \subseteq \theta'$. By symmetry, the same reasoning yields $\theta' \subseteq \theta$, thus $\theta = \theta'$. $\square$

**Remark 8.29.** This property does not hold outside of non-ambiguous formulas, even distributed. For instance, there are two bipartite $ax$-unique proof-nets of conclusions $X_1^{\perp} \otimes X_2^{\perp}$, $X_3 \mathcal{N} X_4$ (where each $X_i$ is an occurrence of the atom $X$): the identity proof net, with axiom links $(X_1^{\perp}, X_4)$ and $(X_2^{\perp}, X_3)$, and the “swap” with axiom links $(X_1^{\perp}, X_3)$ and $(X_2^{\perp}, X_4)$ – see Figure 13.

**Theorem 8.30** (Non-ambiguous isomorphisms). Let $A$ and $B$ be non-ambiguous formulas. If there exist proof-nets $\theta$ and $\psi$ of respective conclusions $A^{\perp}$, $B$ and $B^{\perp}$, $A$, then $A \stackrel{\theta, \psi}{\simeq} B$.

*Proof.* Both compositions reduce to identity proof-nets. Indeed, the composition of $\theta$ and $\psi$ by cut over $B$ reduces to a proof-net on $A^{\perp}$, $A$, that by Lemma 8.28 can only be the identity proof-net of $A$ – and similarly for a composition by cut over $A$. $\square$

8.5. **Completeness for unit-free distributed MALL.** We now prove the completeness of $\mathcal{AC}$ for unit-free and distributed MALL formulas by reasoning as in [BDC99, Section 4], with some more technicalities for we have to reorder not only $\mathcal{N}$-vertices but also $\&$-vertices.

**Definition 8.31** (Sequentializing vertex). A terminal (i.e. with no descendant) non-leaf vertex $V$ in a proof-net $\theta$ is called *sequentializing* if, depending on its kind:

* $\otimes$\*-vertex: the removal of $V$ in $G_{\theta}$ results in two connected components.

* $\oplus$-vertex: the left or right syntactic sub-tree of $V$ does not belong to $G_{\theta}$ (i.e. has no link on any of its leaves in $G_{\theta}$).

* $\mathcal{N}\&$-vertex: a terminal $\mathcal{N}\&$-vertex is always sequentializing.
<figure><img src="image_29.png" /><figcaption>Figure 14: Illustration of the proof of Lemma 8.32</figcaption></figure>

It is easy to check that removing a sequentializing vertex produces proof-net(s). The sequentialization theorem (Theorem 7.2) states there is always a sequentializing vertex.

**Lemma 8.32.** In a bipartite full proof-net with conclusions $A_l \odot A_r, B$, where $\odot \in \{\mathcal{N}; \oplus\}$, the root of $A_l \odot 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 $\odot = \oplus$ or $\odot = \otimes$, it is not sequentializing. $\square$

**Lemma 8.33 (Reordering $\mathcal{N}$-vertices).** Let $\theta$ be a bipartite ax-unique proof-net of conclusions $A = A_l \mathcal{N} A_r$ and $B = B_l \odot B_r$ with $\odot \in \{\mathcal{N}; \oplus\}$ and $A$ a distributed formula. Then $\odot = \otimes$ and there exist two bipartite ax-unique proof-nets of respective conclusions $A'_l, B_l$ and $A'_r, B_r$ where $A'_l \mathcal{N} A'_r$ is equal to $A_l \mathcal{N} A_r$ up to associativity and commutativity of $\mathcal{N}$.

*Proof.* We remove all terminal (hence sequentializing) $\mathcal{N}$-vertices, all in $A$, without modifying the linkings. The resulting graph is a proof-net of conclusions $A_1, \dots, A_n, B_l \odot B_r$ (see Figure 15). The roots of the new trees $A_i$ cannot be $\&$-vertices because $A$ is distributed: so they are $\otimes \setminus \oplus$-vertices or atoms. These $\otimes \setminus \oplus$-vertices are not sequentializing, since by bipartiteness and fullness every leaf of each $A_i$ is connected to the formula $B_l \odot B_r$ (reasoning as in the proof of Lemma 8.32). Thus, the sequentializing vertex of this proof-net is necessarily $B_l \odot B_r$. It follows $\odot = \otimes$, because all leaves of $B$ are connected to leaves in $A_1, \dots, A_n$, so if $\odot = \oplus$ then $B_l \odot B_r$ cannot be sequentializing. Removing the sequentializing $B_l \otimes B_r$ gives two proof-nets, with a partition 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 $\mathcal{N}$-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 $\mathcal{N}$-vertices, $A'_l \mathcal{N} A'_r$ is equal to $A_l \mathcal{N} A_r$ up to associativity and commutativity of $\mathcal{N}$. $\square$

**Lemma 8.34 (Reordering $\&$-vertices).** Let $\theta$ be a bipartite ax-unique proof-net of conclusions $A = A_l \& A_r$ and $B = B_l \oplus B_r$ with $A$ a distributed formula. Then 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 \& A_r$ up to associativity and commutativity of $\&$.

*Proof.* We remove all terminal $\&$-vertices in the proof-net, which are all in $A$. The resulting graphs are $n$ proof-nets $\theta_i$ (for terminal negative vertices are sequentializing), with $\theta_i$ of conclusions $A_i, B_l \oplus B_r$. An illustration is similar to Figure 15, except we have $n$ proof-nets each having a sole $T(A_i)$ and with in common $T(B)$. We claim that the root of $B_l \oplus B_r$ is
<figure><img src="image_30.png" /><figcaption>Figure 15: Proof-net of Lemma 8.33 with all terminal $\mathcal{N}$-vertices removed</figcaption></figure>

sequentializing in every $\theta_i$. Assuming it for now, this implies that, in each $\theta_i$, $A_i$ is linked only to either $B_l$ or $B_r$ and we can remove the root of $B_l \oplus B_r$. Once this $\oplus$-vertex removed, we put back the removed $\&$-vertices of $A$ in another order: we put together all $\theta_i$ linked to $B_l$ on one side, and all those to $B_r$ on another side, yielding two proof-nets of conclusions $B_l, A'_l$ and $B_r, A'_r$. These proof-nets are bipartite $ax$-unique ones for adding a $\&$ is taking the disjoint union of linkings. We indeed have $A'_l \& A'_r$ equal to $A$ up to associativity and commutativity of $\&$, because we only reordered $\&$-vertices.

Let us now prove our claim: the root of $B_l \oplus B_r$ is sequentializing in every $\theta_i$. Towards a contradiction, assume it is not for some $\theta_i$. Remove all terminal $\mathcal{N}$-vertices of $\theta_i$, which are in $A$ if any. As in the proof of Lemma 8.33, the roots of the new trees cannot be negative vertices because the formula $A$ is distributed: hence, they are $\otimes\backslash\oplus$-vertices or atoms. These $\otimes\backslash\oplus$-vertices cannot be sequentializing, since by bipartiteness and fullness every leaf of $A^i$ is connected to the formula $B_l \oplus B_r$ (reasoning as in the proof of Lemma 8.32). Since removing $\mathcal{N}$-vertices preserves that $B_l \oplus B_r$ is not sequentializing, we have a proof-net with no sequentializing vertices, a contradiction. $\square$

**Theorem 8.35** (Isomorphisms completeness for unit-free MALL). *Given $A$ and $B$ two distributed unit-free MALL formulas, if $A \cong_B^{\theta, \psi}$ for some proof-nets $\theta$ and $\psi$, then $A =_{AC} B$.*

*Proof.* We assume $A$ and $B$ to be non-ambiguous formulas by Proposition 8.25. We reason by induction on the size $s(A)$ of $A$, which is its number of connectives and atoms. Remark that the size is unaffected by commutation and associativity of connectives, and that $s(A) = s(B)$ for $\theta$ is bipartite $ax$-unique (Theorem 8.19), thence $A$ and $B$ have the same number of atoms, so of connectives as they are all binary ones.

If $A$ and $B$ are atoms (i.e. of size 1), then the axiom link in $\theta$ between $A^{\perp}$ and $B$ yields $A = B$ and the property holds. Otherwise, $A^{\perp}$ and $B$ are both non atomic. By Theorem 8.19, $\theta$ and $\psi$ are bipartite $ax$-unique; they have respective conclusions $A^{\perp}, B$ and $B^{\perp}, A$. By Lemma 8.32, one of the formulas $A^{\perp}, B$ is negative, otherwise neither the root of $A^{\perp}$ nor the one of $B$ is sequentializing in $\theta$, contradicting sequentialization (Theorem 7.2). A symmetric reasoning on $\psi$ implies that the other formula is positive, so that either both $A$ and $B$ are positive or both are negative. Assume w.l.o.g. that they are positive. We have two cases:
either $A$ is a $\otimes$-formula, or both $A$ and $B$ are $\oplus$-formulas (if $A$ is a $\oplus$-formula and $B$ a $\otimes$-formula, we switch $A$ and $B$).

Let us consider the first case: $\theta$ is a proof-net of conclusions $A^{\perp}, B$ with $A^{\perp}$ a $\aleph$-formula. By Lemma 8.33, $B$ is a $\otimes$-formula and there exist two bipartite ax-unique proof-nets $\theta_0$ and $\theta_1$ of respective conclusions $A'_0^{\perp}, B_0$ and $A'_1^{\perp}, B_1$, with $A'^{\perp} = A'_1^{\perp} \aleph A'_0^{\perp}$ equal to $A^{\perp}$ up to associativity and commutativity of $\aleph$. Similarly in the second case, Lemma 8.34 yields bipartite ax-unique proof-nets $\theta_0$ and $\theta_1$ of respective conclusions $A'_0^{\perp}, B_0$ and $A'_1^{\perp}, B_1$, with $A'^{\perp} = A'_1^{\perp} \& A'_0^{\perp}$ equal to $A^{\perp}$ up to associativity and commutativity of $\&$. In both cases, remark that $A'$ is distributed and non-ambiguous for it is equal, up to associativity and commutativity, to the distributed and non-ambiguous $A$. In particular, $A'_0, A'_1, B_0$ and $B_1$ are also distributed and non-ambiguous, $A'^{\perp} =_{\mathcal{A}C} A^{\perp}$, and $s(A'_0)$ and $s(A'_1)$ are both less than $s(A)$. To conclude, we only need proof-nets $\psi_0$ and $\psi_1$ of respective conclusions $B_0^{\perp}, A'_0$ and $B_1^{\perp}, A'_1$. We will then apply Theorem 8.30 to obtain $A'_0 \simeq B_0$ and $A'_1 \simeq B_1$. Thence, by induction hypothesis, $A'_0 =_{\mathcal{A}C} B_0$ and $A'_1 =_{\mathcal{A}C} B_1$, thus $A' =_{\mathcal{A}C} B$. As $A =_{\mathcal{A}C} A'$, we will finally conclude $A =_{\mathcal{A}C} B$.

Thus, we look for two proof-nets of respective conclusions $B_0^{\perp}, A'_0$ and $B_1^{\perp}, A'_1$. As $A \simeq B$, and $A \simeq A'$ by soundness of $\mathcal{L} \supseteq \mathcal{A}C$ (Theorem 2.11), it follows using Theorem 7.9 that $A' \simeq B$ for some proof-nets $\Theta$ and $\Psi$.<fnref n="4" /> In particular, $\Theta$ is a proof-net of conclusions $B^{\perp}, A'$, i.e. of conclusions $B_1^{\perp} \odot^{\perp} B_0^{\perp}, A'_0 \odot A'_1$ with $\odot \in \{\otimes; \oplus\}$. Remark that, by non-ambiguousness of $A'$ (resp. $B$), no atom $X$ occurs in both $A'_0$ and $A'_1$ (resp. $B_0$ and $B_1$), counting both positive and negative occurrences $X$ and $X^{\perp}$. We claim that no atom occurs in both $B_0$ and $A'_1$. Indeed, as $\theta_0$ is a bipartite ax-unique proof-net of conclusions $A'_0^{\perp}, B_0$, it follows the atoms of $B_0$ are exactly those of $A'_0$, which we just saw are disjoint from the atoms of $A'_1$. Similarly with $\theta_1$, no atom occurs in both $B_1$ and $A'_0$. These four conditions imply that axiom links in $\Theta$ must be between leaves of $B_0^{\perp}$ and $A'_0$, and between leaves of $B_1^{\perp}$ and $A'_1$. Therefore, once we sequentialize the negative root $\odot^{\perp}$ of $B^{\perp}$ in $\Theta$, the positive root $\odot$ of $A'$ is sequentializing. After sequentializing both, we obtain two proof-nets of respective conclusions $B_0^{\perp}, A'_0$ and $B_1^{\perp}, A'_1$. $\square$

The above theorem, associated with preceding results, yields our main contribution.

**Theorem 8.36 (Isomorphisms completeness).**

*AC* is complete for distributed MALL: given $A$ and $B$ two distributed MALL formulas, if $A \simeq B$, then $A =_{\mathcal{A}C} B$.

*L* is complete for MALL: given $A$ and $B$ two MALL formulas, if $A \simeq B$, then $A =_{L} B$.

**Completeness for fragments of MALL:** for any subset $S$ of $\{\otimes; \aleph; 1; \perp; \&; \oplus; \top; 0\}$, if $A$ and $B$ are formulas using connectives from $S$ only and $A \simeq B$, then $A = B$ in the theory $\mathcal{L}_S$ obtained by extracting from $\mathcal{L}$ the equations that use connectives in $S$ only.

*Proof.* For the first point, using Theorem 5.20 we only have to prove that *AC* is complete for isomorphisms of unit-free distributed formulas. Take *A* and *B* unit-free distributed formulas such that *A* ~*B*. By Theorem 7.9 there exist proof-nets *θ* and *ψ* such that *A* ~ *B*. We conclude by Theorem 8.35 that *A* =*AC* *B*.

The second point follows from the first one and Proposition 5.5.

<footnote n="4">⁴One can easily check that isomorphisms in proof-nets form equivalence classes on formulas.</footnote>
$$ \mathcal{D} \left\{ \begin{array}{l} F \otimes (G \otimes H) = (F \otimes G) \otimes H \qquad F \otimes G = G \otimes F \qquad F \otimes 1 = F \\ (F \otimes G) \to H = F \to (G \to H) \qquad 1 \to F = F \\ F \& (G \& H) = (F \& G) \& H \qquad F \& G = G \& F \qquad F \& \top = F \\ F \to (G \& H) = (F \to G) \& (F \to H) \qquad F \to \top = \top \end{array} \right\} \mathcal{S} \\ \\ (F \to \bot) \to \bot = F $$

<caption>Table 7: Type isomorphisms in ★-autonomous categories with finite products</caption>

For the last point, one can reason similarly as for the second one by looking closely to the proof of Proposition 5.5 (on page 20). Assume A and B use connectives from S only, and $A_d$ (resp. $B_d$) is a normal form of A (resp. B) for the rewriting system $\mathcal{D}$ presented in Definition 5.3. Then $A =_{\mathcal{L}_S} A_d$ and $B =_{\mathcal{L}_S} B_d$ since $\mathcal{D}$ is included in $\mathcal{L}$ and never creates a connective by reduction. Using the first point we know $A_d =_{\mathcal{A}C} B_d$ (since $A_d \simeq A \simeq B \simeq B_d$), so that $A_d =_{\mathcal{L}_S} B_d$ because, in the path $A_d =_{\mathcal{A}C} B_d$, only connectives from S can be used ($\mathcal{A}C \subseteq \mathcal{L}$ never creates nor erases a connective). Finally we conclude $A =_{\mathcal{L}_S} B$. $\square$

The last point gives us for instance an equational theory for isomorphisms of unit-free MALL. Denote by $\mathcal{L}^\dagger$ the part of $\mathcal{L}$ not involving units, i.e. with associativity, commutativity and distributivity equations only. Then $\mathcal{L}^\dagger$ is complete for unit-free MALL: given A and B two unit-free MALL formulas, $A \simeq B \implies A =_{\mathcal{L}^\dagger} B$. Indeed, if $A \simeq B$ in unit-free MALL, then $A \simeq B$ in MALL with A and B using only $\{\otimes; \mathcal{Y}; \&; \oplus\}$ so that $A =_{\mathcal{L}^\dagger} B$ by Theorem 8.36. And, as usual, soundness of $\mathcal{L}^\dagger$ is easy to check. We also get back in the same fashion the results for MLL and unit-free MLL by Balat and Di Cosmo [BDC99].

On the contrary, one cannot deduce anything for intuitionistic subsystems such as IMALL in this way (see Appendix B for counter examples).

## 9. STAR-AUTONOMOUS CATEGORIES WITH FINITE PRODUCTS

Since MALL semantically corresponds to ★-autonomous categories with finite products (which also have finite coproducts), we can use our results on MALL to characterize isomorphisms valid in all such categories. For the historical result of how linear logic can be seen as a category, see [See89]. The main problem here is that formulas and objects are not strictly the same, and we have to study translations from the logic to the category and vice-versa.

We consider objects of ★-autonomous categories described by formulas in the language:

$$ F ::= X \mid F \otimes F \mid 1 \mid F \to F \mid \bot \mid F \& F \mid \top $$

There is some redundancy here since one could define 1 as $\bot \to \bot$ in any ★-autonomous category, but we prefer to keep 1 in the language as it is at the core of monoidal categories. Our goal is to prove the theory $\mathcal{D}$ of Table 7 to be sound and complete for the isomorphisms of ★-autonomous categories with finite products.

We establish this result from the one on MALL, first proving that MALL (with proofs considered up to $\beta\eta$-equality) defines a ★-autonomous category with finite products (Section 9.1). Then, we conclude using a semantic method based on this syntactic category (Section 9.2). In a third step we look at the more general case of symmetric monoidal closed categories – without the requirement of a dualizing object (Section 9.3).
**9.2. Isomorphisms of star-autonomous categories with finite products.** We translate formulas in the language of ⋆-autonomous categories with finite products into MALL formulas and conversely by means of the following translations, with $ℓ(-)$ from the category to the logic and $∂(-)$ in the reverse direction:

$$
\begin{align*}
\ell(X) &= X & \partial(X) &= X \\
\ell(F \otimes G) &= \ell(F) \otimes \ell(G) & \partial(A \otimes B) &= \partial(A) \otimes \partial(B) \\
\ell(1) &= 1 & \partial(1) &= 1 \\
\ell(F \to G) &= \ell(F)^{\perp} \mathfrak{R} \ell(G) & \partial(A \mathfrak{R} B) &= ((\partial(A) \to \perp) \otimes (\partial(B) \to \perp)) \to \perp \\
\ell(\perp) &= \perp & \partial(\perp) &= \perp \\
\ell(F \& G) &= \ell(F) \& \ell(G) & \partial(A \& B) &= \partial(A) \& \partial(B) \\
\ell(\top) &= \top & \partial(\top) &= \top \\
& & \partial(A \oplus B) &= ((\partial(A) \to \perp) \& (\partial(B) \to \perp)) \to \perp \\
& & \partial(0) &= \top \to \perp
\end{align*}
$$

The translation $ℓ(-)$ corresponds exactly to the interpretation of the constructions on objects of a ⋆-autonomous categories with finite products in the concrete category MALL of Section 9.1.

**Lemma 9.1.** The $∂(-)$ and $ℓ(-)$ translations satisfy the following properties:

• $∂(A^{\perp}) =_D ∂(A) \to \perp$

• $∂(ℓ(F)) =_D F$

• $A =_L B$ entails $∂(A) =_D ∂(B)$

*Proof.* The second property relies on the first while the third is independent.

• By induction on $A$:

$$
\begin{align*}
\partial(X^{\perp}) &= X \to \perp = \partial(X) \to \perp \\
\partial(X^{\perp \perp}) &= \partial(X) = X =_D (X \to \perp) \to \perp = \partial(X^{\perp}) \to \perp \\
\partial((A \otimes B)^{\perp}) &= ((\partial(B^{\perp}) \to \perp) \otimes (\partial(A^{\perp}) \to \perp)) \to \perp \\
&=_{D} (((\partial(A) \to \perp) \to \perp) \otimes ((\partial(B) \to \perp) \to \perp)) \to \perp \\
&=_{D} (\partial(A) \otimes \partial(B)) \to \perp = \partial(A \otimes B) \to \perp \\
\partial(1^{\perp}) &= \perp =_D 1 \to \perp = \partial(1) \to \perp \\
\partial((A \mathfrak{R} B)^{\perp}) &= \partial(B^{\perp}) \otimes \partial(A^{\perp}) =_D (\partial(A) \to \perp) \otimes (\partial(B) \to \perp) \\
&=_{D} (((\partial(A) \to \perp) \otimes (\partial(B) \to \perp)) \to \perp) \to \perp \\
&= \partial(A \mathfrak{R} B) \to \perp \\
\partial(\perp^{\perp}) &= 1 =_D (1 \to \perp) \to \perp =_D \perp \to \perp = \partial(\perp) \to \perp \\
\partial((A \& B)^{\perp}) &= ((\partial(B^{\perp}) \to \perp) \& (\partial(A^{\perp}) \to \perp)) \to \perp \\
&=_{D} (((\partial(A) \to \perp) \to \perp) \& ((\partial(B) \to \perp) \to \perp)) \to \perp \\
&=_{D} (\partial(A) \& \partial(B)) \to \perp = \partial(A \& B) \to \perp \\
\partial(\top^{\perp}) &= \top \to \perp = \partial(\top) \to \perp \\
\partial((A \oplus B)^{\perp}) &= \partial(B^{\perp}) \& \partial(A^{\perp}) =_D (\partial(A) \to \perp) \& (\partial(B) \to \perp) \\
&=_{D} (((\partial(A) \to \perp) \& (\partial(B) \to \perp)) \to \perp) \to \perp
\end{align*}
$$
$$= \partial(A \oplus B) \to \bot \\ \partial(0^{\bot}) = \top =_D (\top \to \bot) \to \bot = \partial(0) \to \bot$$

* By induction on $F$, the key case being:

$$\begin{align*} \partial(\ell(F \to G)) &= \partial(\ell(F)^{\bot} \mathfrak{R} \ell(G)) = ((\partial(\ell(F)^{\bot}) \to \bot) \otimes (\partial(\ell(G)) \to \bot)) \to \bot \\ &=_D (((F \to \bot) \to \bot) \otimes (G \to \bot)) \to \bot =_D (F \otimes (G \to \bot)) \to \bot \\ &=_D F \to ((G \to \bot) \to \bot) =_D F \to G \end{align*}$$

* We prove that the image of each equation of Table 1 through $\partial(-)$ is derivable with equations of Table 7. Associativity, commutativity and unitality for $\otimes$ and $\&$ are immediate.

$$\begin{align*} \partial(A \mathfrak{R} (B \mathfrak{R} C)) &= ((\partial(A) \to \bot) \otimes (((\partial(B) \to \bot) \otimes (\partial(C) \to \bot)) \to \bot) \to \bot)) \to \bot \\ &=_D ((\partial(A) \to \bot) \otimes ((\partial(B) \to \bot) \otimes (\partial(C) \to \bot))) \to \bot \\ &=_D (((\partial(A) \to \bot) \otimes (\partial(B) \to \bot)) \otimes (\partial(C) \to \bot)) \to \bot \\ &=_D (((((\partial(A) \to \bot) \otimes (\partial(B) \to \bot) \to \bot) \to \bot)) \otimes (\partial(C) \to \bot)) \to \bot \\ &= \partial((A \mathfrak{R} B) \mathfrak{R} C) \end{align*}$$

$$\begin{align*} \partial(A \mathfrak{R} B) &= ((\partial(A) \to \bot) \otimes (\partial(B) \to \bot)) \to \bot \\ &=_D ((\partial(B) \to \bot) \otimes (\partial(A) \to \bot)) \to \bot = \partial(B \mathfrak{R} A) \end{align*}$$

$$\begin{align*} \partial(A \mathfrak{R} \bot) &= ((\partial(A) \to \bot) \otimes (\bot \to \bot)) \to \bot \\ &=_D ((\partial(A) \to \bot) \otimes ((1 \to \bot) \to \bot)) \to \bot =_D ((\partial(A) \to \bot) \otimes 1) \to \bot \\ &=_D (\partial(A) \to \bot) \to \bot =_D \partial(A) \end{align*}$$

Associativity, commutativity and unitality for $\oplus$ follow the same pattern as for $\mathfrak{R}$. Then we have:

$$\begin{align*} \partial(A \otimes (B \oplus C)) &= \partial(A) \otimes (((\partial(B) \to \bot) \& (\partial(C) \to \bot)) \to \bot) \\ &=_D ((\partial(A) \otimes (((\partial(B) \to \bot) \& (\partial(C) \to \bot)) \to \bot)) \to \bot) \to \bot \\ &=_D (\partial(A) \to (((\partial(B) \to \bot) \& (\partial(C) \to \bot)) \to \bot) \to \bot) \to \bot \\ &=_D (\partial(A) \to ((\partial(B) \to \bot) \& (\partial(C) \to \bot))) \to \bot \\ &=_D ((\partial(A) \to (\partial(B) \to \bot)) \& (\partial(A) \to (\partial(C) \to \bot))) \to \bot \\ &=_D (((\partial(A) \otimes \partial(B)) \to \bot) \& ((\partial(A) \otimes \partial(C)) \to \bot)) \to \bot \\ &= \partial((A \otimes B) \oplus (A \otimes C)) \end{align*}$$

$$\begin{align*} \partial(A \otimes 0) &= \partial(A) \otimes (\top \to \bot) \\ &=_D ((\partial(A) \otimes (\top \to \bot)) \to \bot) \to \bot \\ &=_D (\partial(A) \to ((\top \to \bot) \to \bot)) \to \bot \\ &=_D (\partial(A) \to \top) \to \bot \\ &=_D \top \to \bot = \partial(0) \end{align*}$$

$$\begin{align*} \partial(A \mathfrak{R} (B \& C)) &= ((\partial(A) \to \bot) \otimes ((\partial(B) \& \partial(C)) \to \bot)) \to \bot \\ &=_D (\partial(A) \to \bot) \to (((\partial(B) \& \partial(C)) \to \bot) \to \bot) \\ &=_D (\partial(A) \to \bot) \to (\partial(B) \& \partial(C)) \end{align*}$$
$$
\begin{align*}
&=_{\mathcal{D}} ((\partial(A) \to \bot) \to \partial(B)) \& ((\partial(A) \to \bot) \to \partial(C)) \\
&=_{\mathcal{D}} ((\partial(A) \to \bot) \to ((\partial(B) \to \bot) \to \bot)) \& \\
& \qquad ((\partial(A) \to \bot) \to ((\partial(C) \to \bot) \to \bot))) \\
&=_{\mathcal{D}} (((\partial(A) \to \bot) \otimes (\partial(B) \to \bot)) \to \bot) \& \\
& \qquad (((((\partial(A) \to \bot) \otimes (\partial(C) \to \bot)) \to \bot) \\
&= \partial((A \not\to B) \& (A \not\to C)) \\
\partial(A \not\to \top) &= ((\partial(A) \to \bot) \otimes (\top \to \bot)) \to \bot \\
&=_{\mathcal{D}} (\partial(A) \to \bot) \to ((\top \to \bot) \to \bot) \\
&=_{\mathcal{D}} (\partial(A) \to \bot) \to \top =_{\mathcal{D}} \top = \partial(\top) \quad \square
\end{align*}
$$

**Theorem 9.2** (Isomorphisms in ⋆-autonomous categories with finite products). *The equational theory *D* (Table 7) is sound and complete for isomorphisms in ⋆-autonomous categories with finite products.*

*Proof.* Soundness follows by definition of ⋆-autonomous categories with finite products. For completeness, take an isomorphism *F* ≃ *G*. It yields an isomorphism *ℓ*(*F*) ≃ *ℓ*(*G*) in MALL. As *A* ≃ *B* in MALL is generated by *L* (Theorem 8.36), we get *ℓ*(*F*) =*L* *ℓ*(*G*). From Lemma 9.1, we deduce *F* =*D* *∂*(*ℓ*(*F*)) =*D* *∂*(*ℓ*(*G*)) =*D* *G*. □

**9.3. Isomorphisms of symmetric monoidal closed categories with finite products.** Isomorphisms in symmetric monoidal closed categories (SMCC) have been characterized [DP97] and proved to correspond to equations in the first two lines of Table 7. We extend this result to finite products by proving the soundness and completeness of the theory *S* presented in Table 7.

**Theorem 9.3 (Isomorphisms in SMCC with finite products).** *The equational theory *S* (Table 7) is sound and complete for isomorphisms in symmetric monoidal closed categories with finite products.*

*Proof.* The language of SMCC with finite products is the language of ⋆-autonomous categories with finite products in which we remove $\bot$. In particular the translation $\ell(-)$ can be used to translate the associated formulas into MALL formulas. In order to analyse the image of this restricted translation, we consider the following grammar of MALL formulas (Danos-Regnier output formulas *o* and input formulas $\iota$ [Lam96]):

$$
\begin{array}{lclclclcl}
o & ::= & X & | & o \otimes o & | & o \not\to \iota & | & \iota \not\to o & | & 1 & | & o \& o & | & \top \\
\iota & ::= & X^{\bot} & | & \iota \not\to \iota & | & \iota \otimes o & | & o \otimes \iota & | & \bot & | & \iota \oplus \iota & | & 0
\end{array}
$$

The dual of an output formula is an input formula and conversely. Moreover no MALL formula is both an input and an output formula – let us call this the *non-ambiguity property*. One can check by induction on a formula *F* in the language of SMCC with finite products that *ℓ*(*F*) is an output formula. We define a translation back from output formulas to SMCC formulas (which is well defined thanks to the non-ambiguity property):

$$
\begin{align*}
X^{\circ} &= X \\
(o \otimes o')^{\circ} &= o^{\circ} \otimes o'^{\circ} && 1^{\circ} = 1 \\
(o \& o')^{\circ} &= o^{\circ} \& o'^{\circ} && \top^{\circ} = \top \\
(o \not\to \iota)^{\circ} &= (\iota^{\bot})^{\circ} \to o^{\circ} && (\iota \not\to o)^{\circ} = (\iota^{\bot})^{\circ} \to o^{\circ}
\end{align*}
$$
We use the notation $ι^{\bullet} = (ι^{\perp})^{\circ}$ (so that $(o^{\perp})^{\bullet} = o^{\circ}$). We can check, by induction on $F$, that $ℓ(F)^{\circ} = F$. We now prove that when $o =_L A$ (resp. $ι =_L A$) is an equation from Table 1 (or its symmetric version) then $A$ is an output (resp. input) formula and $o^{\circ} =_S A^{\circ}$ (resp. $ι^{\bullet} =_S A^{\bullet}$):

* If $o$ or $ι$ is of the shape $A \otimes (B \otimes C)$, we have the following possibilities:

- $A$, $B$ and $C$ are output, then $(A \otimes B) \otimes C$ is output and:

$$ (A \otimes (B \otimes C))^{\circ} = A^{\circ} \otimes (B^{\circ} \otimes C^{\circ}) \\ =_S (A^{\circ} \otimes B^{\circ}) \otimes C^{\circ} = ((A \otimes B) \otimes C)^{\circ} $$

- $A$ and $B$ are output and $C$ is input, then $(A \otimes B) \otimes C$ is input and:

$$ (A \otimes (B \otimes C))^{\bullet} = A^{\circ} \to (B^{\circ} \to C^{\bullet}) \\ =_S (A^{\circ} \otimes B^{\circ}) \to C^{\bullet} = ((A \otimes B) \otimes C)^{\bullet} $$

- $A$ and $C$ are output and $B$ is input, then $(A \otimes B) \otimes C$ is input and:

$$ (A \otimes (B \otimes C))^{\bullet} = A^{\circ} \to (C^{\circ} \to B^{\bullet}) \\ =_S (A^{\circ} \otimes C^{\circ}) \to B^{\bullet} =_S (C^{\circ} \otimes A^{\circ}) \to B^{\bullet} \\ =_S C^{\circ} \to (A^{\circ} \to B^{\bullet}) = ((A \otimes B) \otimes C)^{\bullet} $$

- $A$ is input and $B$ and $C$ are output, then $(A \otimes B) \otimes C$ is input and:

$$ (A \otimes (B \otimes C))^{\bullet} = (B^{\circ} \otimes C^{\circ}) \to A^{\bullet} \\ =_S (C^{\circ} \otimes B^{\circ}) \to A^{\bullet} \\ =_S C^{\circ} \to (B^{\circ} \to A^{\bullet}) = ((A \otimes B) \otimes C)^{\bullet} $$

The symmetric case follows the same pattern, as well as associativity of $\mathcal{N}$.

* If $o$ or $ι$ is of the shape $A \otimes B$, we have the following possibilities:

- $A$ and $B$ are output, then $B \otimes A$ is output and $(A \otimes B)^{\circ} = A^{\circ} \otimes B^{\circ} =_S B^{\circ} \otimes A^{\circ} = (B \otimes A)^{\circ}$

- $A$ is output and $B$ is input, then $B \otimes A$ is input and $(A \otimes B)^{\bullet} = A^{\circ} \to B^{\bullet} = (B \otimes A)^{\bullet}$

- $A$ is input and $B$ is output, then $B \otimes A$ is input and $(A \otimes B)^{\bullet} = B^{\circ} \to A^{\bullet} = (B \otimes A)^{\bullet}$. The commutativity of $\mathcal{N}$ follows the same pattern.

* If $o$ or $ι$ is of the shape $A \otimes 1$ then either $A$ is output and $(A \otimes 1)^{\circ} = A^{\circ} \otimes 1 =_S A^{\circ}$, or $A$ is input and $(A \otimes 1)^{\bullet} = 1 \to A^{\bullet} =_S A^{\bullet}$. The symmetric case follows the same pattern, as well as unitality for $\mathcal{N}$.

* If $o = A \& (B \& C)$ then $A$, $B$ and $C$ are output and $(A \& B) \& C$ as well. We have $(A \& (B \& C))^{\circ} = A^{\circ} \& (B^{\circ} \& C^{\circ}) =_S (A^{\circ} \& B^{\circ}) \& C^{\circ} = ((A \& B) \& C)^{\circ}$. The symmetric case follows the same pattern, as well as associativity of $\oplus$.

* If $o = A \& B$ then $A$ and $B$ are output and $B \& A$ as well. We have $(A \& B)^{\circ} = A^{\circ} \& B^{\circ} =_S B^{\circ} \& A^{\circ} = (B \& A)^{\circ}$. The commutativity of $\oplus$ follows the same pattern.

* If $o = A \& \top$ then $A$ is output and $(A \& \top)^{\circ} = A^{\circ} \& \top =_S A^{\circ}$. The symmetric case follows the same pattern, as well as unitality for $\oplus$.

* If $ι = A \otimes (B \oplus C)$ then $A$ is output and $B$ and $C$ are input, and $(A \otimes B) \oplus (A \otimes C)$ is input. We have:

$$ (A \otimes (B \oplus C))^{\bullet} = A^{\circ} \to (C^{\bullet} \& B^{\bullet}) \\ =_S (A^{\circ} \to C^{\bullet}) \& (A^{\circ} \to B^{\bullet}) = ((A \otimes B) \oplus (A \otimes C))^{\bullet} $$

The symmetric case follows the same pattern, as well as distributivity of $\mathcal{N}$ over $\&$.
• If $ι = A \otimes 0$ then $A$ is output and $(A \otimes 0)^{\bullet} = A^{\circ} \to \top =_{S} \top = 0^{\bullet}$. The symmetric case follows the same pattern, as well as cancellation of $\mathfrak{N}$ by $\top$.

Assume now that $F \simeq G$ in the class of SMCC with finite products. As MALL is such a SMCC with finite products, we have $ℓ(F) \simeq ℓ(G)$ in MALL, thus $ℓ(F) =_{L} ℓ(G)$ by Theorem 8.36. As $ℓ(F)$ is an output formula, by induction on the length of the equational derivation of $ℓ(F) =_{L} ℓ(G)$, we get that all the intermediary steps involve output formulas and each equation is mapped to $=_{S}$ by $(-)^{\circ}$ so that $ℓ(F)^{\circ} =_{S} ℓ(G)^{\circ}$. We finally get $F = ℓ(F)^{\circ} =_{S} ℓ(G)^{\circ} = G$.

Conversely soundness easily comes from the definition of SMCC and products. $\square$

## 10. CONCLUSION

Extending the result of Balat and Di Cosmo in [BDC99], we give an equational theory characterising type isomorphisms in multiplicative-additive linear logic with units as well as in $\star$-autonomous categories with finite products: the one described in Table 1 on page 3 (and in Table 7 for $\star$-autonomous categories). We get as a sub-result that isomorphisms for additive linear logic (resp. unit-free additive linear logic) are given by the equational theory $\mathcal{L}$ restricted to additive (resp. additive unit-free) formulas – and more generally this applies to any fragment of MALL, namely multiplicative-additive linear logic without units, with additive units but without multiplicative units, with multiplicative units but without additive units, as well as multiplicative linear logic with and without units. 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 consider rule commutations in 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.

Another perspective is to look at categories. A $\star$-autonomous category with finite products automatically has finite coproducts given by $F \oplus G := ((F \to \bot) \& (G \to \bot)) \to \bot$ and $0 := \top \to \bot$. From equations of Table 7, one can derive:

$$ \left. \begin{array}{rcl} F \oplus G & = & G \oplus F \\ F \oplus (G \oplus H) & = & (F \oplus G) \oplus H \\ F \oplus 0 & = & F \\ F \otimes (G \oplus H) & = & (F \otimes G) \oplus (F \otimes H) \\ F \otimes 0 & = & 0 \\ (F \oplus G) \to H & = & (F \to H) \& (G \to H) \\ 0 \to H & = & \top \end{array} \right\} \mathcal{C} $$

In the weaker setting of SMCC, finite products do not induce finite coproducts. It justifies the possibility of considering them separately. We solved the case of products only (Theorem 9.3) and have conjectures for SMCC with both products and coproducts on one side, and with coproducts only on the other side.

We conjecture that isomorphisms in SMCC with both finite products and finite coproducts correspond to adding the equations of theory $\mathcal{C}$ to $\mathcal{S}$ (Table 7). Our approach through
⋆-autonomous categories does not help since $\top \to (\top \oplus \top)$ and $(0 \& 0) \to 0$ are isomorphic in ★-autonomous categories but not in SMCC with finite products and coproducts.

About SMCC with finite coproducts only (without products), it is important to notice that an initial object 0 in a SMCC induces that $0 \to F$ is a terminal object for any $F$. Thus, the theory of isomorphisms includes the equation $0 \to F \simeq 0 \to G$ even if it does not occur in $C$ (it might be the only missing equation). Regarding a characterization through ★-autonomous categories, it is again not possible since, if we denote by $\top$ a terminal object, $(\top \to 0) \to 0$ and $\top \to (\top \otimes \top)$ are isomorphic in ★-autonomous categories but not in SMCC with finite coproducts.

For the curious reader, we prove in Appendix B that our two examples of isomorphisms in ★-autonomous categories are not isomorphic in the considered SMCC. This is done by bringing one of our results about patterns in isomorphisms of multiplicative-additive linear logic to the setting of intuitionistic multiplicative-additive linear logic.

A more general problem than isomorphisms is the study of type retractions, where only one of the two compositions yields an identity. It is much more difficult – see for example [RU02]. 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 \to A) \to A = (A \otimes A^{\perp}) \not\cong 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 5, but there are also retractions between $A$ and $A \oplus A$.

## ACKNOWLEDGEMENTS

We warmly thank the anonymous referees for their useful and detailed remarks, and in particular for bringing our attention to [CP05].

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.

## REFERENCES

[Acc13] Beniamino Accattoli. Linear logic and strong normalization. In Femke van Raamsdonk, editor, *Rewriting Techniques and Applications*, volume 21 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 39–54. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2013. URL: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.39, doi:10.4230/LIPIcs.RTA.2013.39.

[AM98] Michele Abrusci and Elena Maringelli. A new correctness criterion for cyclic proof nets. *Journal of Logic, Language and Information*, 7:449–459, 1998. doi:10.1023/A:1008354130493.

[ARG21] Clément Allain, Gabriel Radanne, and Laure Gonnord. Isomorphisms are back! In *ML 2021 - ML Workshop*, August 2021. URL: https://hal.science/hal-03355381.

[AT12] Takahito Aoto and Yoshihito Toyama. A reduction-preserving completion for proving confluence of non-terminating term rewriting systems. *Logical Methods in Computer Science*, 8(1):1–29, March 2012. doi:10.2168/LMCS-8(1:31)2012.

[BCST96] Richard Blute, Robin Cockett, Robert Seely, and Todd Trimble. Natural deduction and coherence for weakly distributive categories. *Journal of Pure and Applied Algebra*, 113:229–296, 1996.
[BDC99] Vincent Balat and Roberto Di Cosmo. A linear logical view of linear type isomorphisms. In Jörg Flum and Mario Rodríguez-Artalejo, editors, *Computer Science Logic*, volume 1683 of Lecture Notes in Computer Science, pages 250–265. Springer, 1999.

[BHS05] Richard Blute, Masahiro Hamano, and Philip Scott. Softness of hypercoherences and MALL full completeness. *Annals of Pure and Applied Logic*, 131(1):1–63, 2005. URL: https://www.sciencedirect.com/science/article/pii/S0168007204000855, doi:10.1016/j.apal.2004.05.002.

[Bie95] Gavin Bierman. What is a categorical model of intuitionistic linear logic? In Mariangiola Dezani and Gordon Plotkin, editors, *Typed Lambda Calculi and Applications '95*, volume 902 of Lecture Notes in Computer Science. Springer, April 1995. doi:10.1007/BFb0014046.

[CMS08] Kaustuv Chaudhuri, Dale Miller, and Alexis Saurin. Canonical sequent proofs via multi-focusing. In Giorgio Ausiello, Juhani Karhumäki, Giancarlo Mauri, and Luke Ong, editors, *Fifth IFIP International Conference on Theoretical Computer Science*, volume 273 of Theoretical Computer Science, pages 383–396. Springer, 2008. doi:10.1007/978-0-387-09680-3_26.

[CP05] Robin Cockett and Craig Pastro. A language for multiplicative-additive linear logic. *Electronic Notes in Theoretical Computer Science*, 122:23–65, 2005. Proceedings of the 10th Conference on Category Theory in Computer Science (CTCS 2004). URL: https://www.sciencedirect.com/science/article/pii/S1571066105000320, doi:10.1016/j.entcs.2004.06.049.

[DC95] Roberto Di Cosmo. *Isomorphisms of Types*. Progress in Theoretical Computer Science. Birkhäuser, 1995.

[DG99] Roberto Di, Cosmo and Stefano Guerrini. Strong normalization of proof nets modulo structural congruences. In P. Narendran and M. Rusinowitch, editors, *Rewriting Techniques and Applications*, volume 1631 of Lecture Notes in Computer Science, pages 75–89. Springer, 1999. doi:10.1007/3-540-48685-2_6.

[DG11] Paolo Di Giamberardino. Jump from parallel to sequential proofs: Additives, 2011. https://hal.science/hal-00616386.

[DG24] Rémi Di Guardia. *Identity of Proofs and Formulas using Proof-Nets in Multiplicative-Additive Linear Logic*. Thèse de doctorat, Ecole normale supérieure deyon - ENS LYON, September 2024. URL: https://theses.hal.science/tel-04830060.

[DGL23] Rémi Di Guardia and Olivier Laurent. Type isomorphisms for multiplicative-additive linear logic. In Marco Gaboardi and Femke van Raamsdonk, editors, *International Conference on Formal Structures for Computation and Deduction (FSCD)*, volume 260 of Leibniz International Proceedings in Informatics (LIPIcs), pages 26:1–26:21. Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik, July 2023. doi:10.4230/LIPIcs.FSCD.2023.26.

[DP97] Kosta Dosen and Zoran Petric. Isomorphic objects in symmetric monoidal closed categories. *Mathematical Structures in Computer Science*, 7(6):639–662, 1997. doi:10.1017/S0960129596002241.

[DR89] Vincent Danos and Laurent Regnier. The structure of multiplicatives. *Archive for Mathematical Logic*, 28:181–203, 1989.

[FDCB02] Marcelo Fiore, Roberto Di Cosmo, and Vincent Balat. Remarks on isomorphisms in typed lambda calculi with empty and sum types. In *Proceedings of the seventeenth annual symposium on Logic In Computer Science*, pages 147–156, Copenhagen, July 2002. IEEE, IEEE Computer Society Press.

[Gir87] Jean-Yves Girard. Linear logic. *Theoretical Computer Science*, 50:1–102, 1987. doi:10.1016/0304-3975(87)90045-4.

[Gir96] Jean-Yves Girard. Proof-nets: the parallel syntax for proof-theory. In Aldo Ursini and Paolo Agliano, editors, *Logic and Algebra*, volume 180 of Lecture Notes in Pure and Applied Mathematics, pages 97–124, New York, 1996. Marcel Dekker. doi:10.1201/9780203748671-4.

[Hei11] Willem Heijltjes. Proof nets for additive linear logic with units. In *Proceedings of the twenty-sixth annual symposium on Logic In Computer Science*, pages 207–216, Toronto, June 2011. IEEE, IEEE Computer Society Press.

[HH16a] Willem Heijltjes and Robin Houston. Proof equivalence in MLL is PSPACE-complete. *Logical Methods in Computer Science*, 12(1), 2016. doi:10.2168/LMCS-12(1:2)2016.

[HH16b] Willem Heijltjes and Dominic Hughes. Conflict nets: Efficient locally canonical MALL proof nets. In *Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, pages 437–446. ACM Press, July 2016. doi:10.1145/2933575.2934559.