# The Cut-Elimination Thereom for Differential Nets with Promotion

Michele Pagani

► To cite this version:

Michele Pagani. The Cut-Elimination Thereom for Differential Nets with Promotion. 9th International Conference on Typed Lambda Calculi and Applications (TLCA 2009), Jul 2009, Brasilia, Brazil. pp.219-233, 10.1007/978-3-642-02273-9_17. hal-00698974

HAL Id: hal-00698974

https://hal.science/hal-00698974v1

Submitted on 11 Aug 2024

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_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# The Cut-Elimination Theorem for Differential Nets with Promotion

Michele Pagani*

Laboratoire Preuves, Programmes et Systèmes

Université Paris Diderot – Paris 7

&

Dipartimento di Informatica

Università degli Studi di Torino

http://www.di.unito.it/~pagani

**Abstract.** Recently Ehrhard and Regnier have introduced Differential Linear Logic, DiLL for short — an extension of the Multiplicative Exponential fragment of Linear Logic that is able to express non-deterministic computations. The authors have examined the cut-elimination of the promotion-free fragment of DiLL by means of a proofnet-like calculus: differential interaction nets. We extend this analysis to exponential boxes and prove the Cut-Elimination Theorem for the whole DiLL: every differential net that is sequentializable can be reduced to a cut-free net.

## Introduction

The cut-elimination procedure has been invented by Gentzen in order to prove consistency of classical logic and Peano Arithmetics. First, he introduced the *sequent calculus* LK, a proof system sound and complete with respect to classical logic. In this system there is just one deductive rule – the *cut* – which might prove absurdity, so that consistency can be deducted from the redundancy of such rule. In order to achieve it, Gentzen defined then *cut-elimination*, a procedure transforming a proof $\pi$ into another one $\pi'$ of the same theorem where however cuts in $\pi'$ are in “some sense” reduced. Redundancy of the cut rule is then obtained by proving that iterating this procedure always terminates to a cut-free proof – the Cut-Elimination Theorem.

Through the time the procedure of cut-elimination has acquired more and more importance in proof theory, also independently from the question of consistency. In particular in the 60's, cut-elimination revealed a deep nexus between logic and computer science, enabling a correspondence between the execution of programs and the cut-elimination of proofs. This correspondence is called the *Curry-Howard correspondence*, and allows to express termination properties of programming languages as cut-elimination theorems in specific proof systems.

<footnote>* Supported by a post-doc fellowship of Région Île de France and Italian MIUR Project “CONCERTO”.</footnote>
Linear logic (LL, [Gir87]) has been built around cut-elimination: it splits
the connectives "and", "or" of LK in two classes (the *multiplicatives* ⊗, ℛ, and
the *additives* &, ⊕) depending on their behavior during cut-elimination, and it
introduces a new pair of dual connectives (the *exponentials* !, ?) giving a logical
status to the actions of erasing and duplicating whole pieces of a proof. Linear
Logic allows to express cut-elimination as a rewriting of *proof nets* – specific
graphs that give a sharper account of cut-elimination than LK. Indeed the proof
nets drastically decrease the types of commutative cuts, abounding instead in
sequent calculus.

In the syntax of proof nets the commutative cuts are due to the *boxes* – special
hyper-edges representing the sequent rules of LL that have some restriction on
the context (i.e. promotion, additive conjunction and universal quantification)<fnref n="1" />
A particular feature of these cuts is that they can be profoundly affected by
the reduction of other cuts, even changing their commutative nature: this may
considerably muddle the picture (see [PTdF07] for a more detailed discussion).

As far as one restricts to the box-free fragment of LL, the cut-elimination is
easily tamable, the reduction of a cut does not affect that of the others and a
parallel reduction can be defined straightforwardly. Starting from this remark,
Lafont has introduced *interaction nets* [Laf90] – a graph-rewriting paradigm of
distributed computation based on the box-free fragment of the proof nets.

The discovery of LL and proof nets has been a fundamental step towards
the extension of the Curry-Howard correspondence, that was at the beginning
restricted to the functional and sequential core of the programming languages. In
particular Ehrhard and Regnier [ER06] have recently achieved a significant step
towards a logical understanding of concurrency theory with the introduction of
differential linear logic (DiLL). This system extends linear logic with three new
rules handling the ! modality (*codereliction, cocontraction and coweakening*) and
allows to express a concurrent sharing of resources [EL08]. The codereliction in
particular creates data that can be called exactly once, so that a program made
of several subroutines is executed non-deterministically on "coderelicted" inputs,
depending on which subroutine gains the unique available copy of the inputs.
Thus we have formal sums, where each addendum represents a possibility.

The cut-elimination of DiLL is analyzed with a proofnet-like calculus, called *differential nets*. Actually, [ER06] considers only the promotion-free fragment of DiLL, whose nets are without boxes and called *differential interaction nets*, being a non-deterministic example of Lafont’s interaction nets. In that restricted setting the authors prove the Cut-Elimination Theorem. In our paper, we extend their result to the whole DiLL, using differential nets with exponential boxes. The main difficulty in such an extension is to account for the exponential commutative cuts, and specifically for the commutative cut between a codereliction and a box, which has a completely non-standard behavior with respect to the commutative cuts in linear logic proof nets (see the discussion on Figure 6).

<footnote n="1">¹ In this paper, indeed, we consider only the exponential boxes. Up to now, differential nets are restricted to the multiplicatives and exponentials; besides, there are specific notions of LL proof nets able to avoid the boxes for additives and quantifiers.</footnote>
<figure><img src="image_2.png" /><figcaption>Fig. 1: sequent calculus rules for differential linear logic.</figcaption></figure>

# 1 Preliminaries

## 1.1 Differential Nets

We recall differential nets and their cut-elimination: first, we introduce the promotion-free nets, called differential interaction nets in [ER06], then we add boxes to accommodate promotion. In the sake of brevity, the presentation is kept informal, and we refer to [ER06,Vau07] for a more detailed one. We denote sets with braces `{ }`, and sequences by angles `⟨⟩`. Boldface letters `a`, `b` etc. range over sequences, and for $i \le$ length(`a`), $a_i$ denotes the $i$-th element of `a`.

Types of DiLL. The formulas of DiLL are generated by the following grammar, where $X, X^\perp$ range over a fixed set of propositional variables:

$$A, B ::= X \mid X^\perp \mid A \otimes B \mid A \mathcal{N} B \mid !A \mid ?A.$$

Linear negation is involutional ($A^{\perp\perp} = A$) and defined through De Morgan laws: $(X)^\perp := X^\perp, (A \otimes B)^\perp := A^\perp \mathcal{N} B^\perp, (!A)^\perp := ?A^\perp$.

Variables and their negations are **atomic**, $\otimes$, $\mathcal{N}$ are **multiplicative**, while `!`, `?` are **exponential**. For brevity, we omit to consider multiplicative units `1`, `⊥`, however all the results in this paper can be extended to the general case straightforwardly. A **sequent** $\Gamma$ is a finite sequence of formulas $A_1, \dots, A_n$. Capital Greek letters $\Gamma, \Delta$ range over sequents. Fig. 1 gives the rules of DiLL sequent calculus. The calculus is extended with the rule mix and its zeroary version empty— this is needed to have a fair correctness criterion (Prop. 1).

Differential interaction nets. A simple interaction net $\alpha$ is the union of a graph and an hyper-graph on a given set of nodes, respecting the following constraints (see Figure 5(a) for examples).

- The nodes of $\alpha$ are called **ports**, they are crossed exactly by one edge and at most by one hyper-edge. In the figures, the ports are not explicitly depicted, as they correspond to the extremities of the edges.
<figure><img src="image_3.png" /><figcaption>Fig. 2: cells for differential interaction nets, together with their typing rules.</figcaption></figure>

- The edges of $\alpha$ are called **wires**, they are undirected, possibly loops; a wire $\{a, b\}$ between two distinct ports $a, b$ has two orientations: from $a$ to $b$, denoted $\langle a, b \rangle$, and from $b$ to $a$, denoted $\langle b, a \rangle$; with each orientation is associated a formula of DiLL in such a way that the formula associated with $\langle a, b \rangle$ must be the linear negation of the formula associated to $\langle b, a \rangle$.<fnref n="2" />

- The hyper-edges of $\alpha$ are called **cells**, and they are sequences of the ports they cross; the first port crossed by a cell is called **principal**, the other ones (if any) are called **auxiliary**; every cell is labelled by a symbol that determines the **arity** of the cell and the types of the wires incident to it, as it is depicted in Figure 2. We require also that cells are not incident to loops.

The **type of a port** $a$ of $\alpha$ is the type of $\langle b, a \rangle$, where $\{a, b\}$ is the unique wire of $\alpha$ crossing $a$; in particular this means that the ports connected by a wire have dual types. The ports of $\alpha$ which are crossed by no cell nor loop, are called **free**. We require that $\alpha$ is given with an enumeration $p$ of its free ports, called the **interface** of $\alpha$. The **sequent conclusion** of $\alpha$ is $\Gamma = A_1, \dots, A_n$, where $n$ is the length of $p$ and for every $i \le n$, $A_i$ is the type of $p_i$.

A **differential interaction net** with sequent conclusion $\Gamma$ is a finite multi-set<fnref n="3" />, possibly empty, of simple interaction nets with the conclusion $\Gamma$.

The loops must be admitted, as they can be produced by cut-elimination. However, they do not appear in the differential nets that are sequentializable, and so they are voluntarily left out of the discussion the most of times.

*Adding boxes.* Boxes are a special kind of cells parameterized by a net, this last one standing for a proof of the premise of the corresponding promotion rule. Formally, the sets $dN$ of **differential nets** and $sN$ of **simple nets** are defined simultaneously, by induction on the exponential depth. This means that we define $sN_d$ and $dN_d$ for every $d \in \mathbb{N}$ and then we set:

$$sN := \bigcup_{d=0}^{\infty} sN_d,$$

$$dN := \bigcup_{d=0}^{\infty} dN_d.$$

$sN_0$ (resp. $dN_0$) is the set of the simple interaction nets (resp. differential interaction nets).

<footnote n="2">² Loops are intentionally considered untyped.</footnote>

<footnote n="3">³ In a general setting, differential nets are finite linear combinations of simple nets with coefficients in a commutative semiring $R$ with units. In this paper however we will consider only the case $R = \mathbb{N}$, and in such a case the differential nets are the finite multisets of simple nets.</footnote>
<figure><img src="image_4.png" /><figcaption>Fig. 3: a box of type $!\pi$ can be also presented with its contents depicted inside.</figcaption></figure>

action nets). A simple net of $sN_{d+1}$ is a simple net $\alpha$ defined from the cells of Fig. 2 and 3(a), such that every box $o$ of $\alpha$ is labelled by a symbol $!\pi$, where $\pi$ is a differential net of $dN_d$, called the **contents** of $o$. Moreover, together with $o$ it is given a fixed correspondence between the free ports of every simple net $\beta \in \pi$ and the ports of $o$: for every port $a$ of $o$ we denote by $a^\beta$ the correspondent free port of $\beta$. This correspondence enjoys the typing conditions sketched in Fig. 3(b).

A differential net $\pi$ of $dN_d$ with sequent conclusion $\Gamma$ is a finite multiset, possibly empty, of simple nets of $sN_d$ with sequent conclusion $\Gamma$.

Initial Greek letters $\alpha, \beta, \gamma$ (resp. final Greek letters $\pi, \sigma, \rho$) range over simple nets (resp. differential nets). We use the additive notation for multisets: 0 is the empty multiset, $\pi + \sigma$ is the disjoint union of $\pi$ and $\sigma$ (repetition does matter); a differential net $\pi$ can also be written as $\sum_{\alpha \in \pi} \alpha$.

The **depth** of a simple net $\alpha$ (resp. differential net $\pi$) is the minimal $d$ such that $\alpha \in sN_d$ (resp. $\pi \in dN_d$). Many definitions are done by induction on the depth: let us skip to mention it explicitly, when evident. So, we say that a **cell/wire** $w$ is at depth $d$ of a differential net $\pi$, denoted $w \in_d \pi$, whenever $w \in_d \alpha$ for a simple net $\alpha$ of $\pi$; and we say that $w \in_d \alpha$ whenever either $d=0$ and $w$ is a cell/wire of $\alpha$, view as an interaction net, or there is a box $!\rho \in_0 \alpha$ and $w \in_{d-1} \rho$. We write $w \in_! \pi$ meaning $w \in_d \pi$ for a $d \in \mathbb{N}$.

**Switching acyclicity.** Every proof in the sequent calculus of DiLL can be translated in a differential net with the same sequent conclusion. This translation is defined by induction on the size of the proof and can be easily deduced from the sequent rules of Figure 1. The translation is not surjective (neither injective) over $dN$ and we call **sequentializable** the differential nets that are images of it. Purely graph-theoretical conditions, called *correctness criteria*, have been presented in order to characterize the set of sequentializable differential nets. We give here one among the most celebrated of such correctness criteria, *switching acyclicity*, presented originally by Danos and Regnier [DR89] for the multiplicative fragment of linear logic, and then extended to DiLL in [ER06].<fnref n="4" />

A **switching of a cell** $c$ is an undirected graph $\sigma$ whose nodes are the ports of $c$ and whose edges are defined depending on the label of $c$: in case $c$ is of type $\mathcal{N}$ or $?c$, $\sigma$ has exactly one edge, crossing the principal port and one chosen auxiliary port of $c$ (so $c$ has two possible switchings); otherwise $\sigma$ is unique and it has one edge for each auxiliary port of $c$, if any, wiring that port to the principal one. A **correctness graph** of a simple net $\alpha$ is an undirected graph $\sigma$ having

<footnote n="4">⁴ To be precise, [ER06] introduces switching acyclicity in the promotion-free fragment of DiLL, however its generalization to exponential boxes is straightforward.</footnote>
as nodes the ports of $\alpha$ and as edges the wires of $\alpha$ plus the edges obtained substituting every cell with one among its switchings.

A differential net $\pi$ is **switching acyclic** if every simple net of $\pi$ is switching acyclic; a simple net $\alpha$ is switching acyclic if every correctness graph of $\alpha$ is an acyclic graph and for every box $!\rho \in_0 \alpha$, $\rho$ is switching acyclic.

**Proposition 1.** *A differential net $\pi$ is sequentializable iff it is switching acyclic.*

*Proof.* Standard generalization of the technique developed in [DR89,Dan90].

## 1.2 Cut-Elimination

A port is **active** whenever it is the principal port of a cell or it is an auxiliary port of a box. A **cut** is a wire connecting two active ports. A differential net is **cut-free** if it has no cut at any depth.

The reader should notice the difference with respect to the differential interaction nets: in that restricted setting the only active ports are the principal ones. Exponential boxes add commutative cuts, that are wires between the principal port of a cell and an auxiliary port of a box.

*Interaction.* We denote $\alpha^a$ the pair of a simple net and a sequence $\mathbf{a}$ of the free ports of $\alpha$. Let $\alpha^a$ and $\beta^b$ be such that $\mathbf{a}$ and $\mathbf{b}$ have the same length $n$ and for every $i \le n$, $\mathbf{a}_i$ and $\mathbf{b}_i$ have dual types, we call the **interaction** between $\alpha^a$ and $\beta^b$ the simple net $\langle\alpha^a|\beta^b\rangle$ obtained by equaling for every $i \le n$ the port $\mathbf{a}_i$ of $\alpha$ with the port $\mathbf{b}_i$ of $\beta$, and then by merging the wires that have a port in common⁵:

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

We can omit the superscripts $\mathbf{a}$, $\mathbf{b}$ if they are clear or unimportant. The writing $\langle\alpha^{aa'}|\beta^b, \gamma^c\rangle$ means $\langle\langle\alpha^a|\beta^b\rangle^{a'}|\gamma^c\rangle$, where $\mathbf{a}$ and $\mathbf{a}'$ are sequences of distinct free ports of $\alpha$ with the lengths and the dual types of resp. $\mathbf{b}$ and $\mathbf{c}$. Interaction is extended to differential nets by bilinearity:

$$ \langle\sum_{i \le l} \alpha_i^a | \sum_{j \le m} \beta_j^b \rangle = \sum_{\substack{i \le l \\ j \le m}} \langle\alpha_i^a | \beta_j^b \rangle. $$

*Reductions.* Let $\mathbb{R}$ be a binary relation over differential nets with the same sequential conclusion, the **context closure** of $\mathbb{R}$ is the smallest relation $\mathbb{R}^\circ$ s.t.

- $\mathbb{R}^\circ$ is closed by sum: $\pi\mathbb{R}^\circ\pi'$ implies $(\pi + \rho)\mathbb{R}^\circ(\pi' + \rho)$, for $\rho \in \mathrm{dN}$; and

- $\mathbb{R}^\circ$ is closed by interaction: $\pi\mathbb{R}^\circ\pi'$ implies $\langle\alpha|\pi\rangle\mathbb{R}^\circ\langle\alpha|\pi'\rangle$, for $\alpha \in \mathrm{sN}$; and

- $\mathbb{R}^\circ$ is closed by promotion: $\pi\mathbb{R}^\circ\pi'$ implies $!\pi\mathbb{R}^\circ!\pi'$.
<figure><img src="image_6.png" /><figcaption>**Fig. 4:** elementary reduction steps (ers) for differential nets, where * (resp. $\bar{\ast}$) is $?$ (resp. !) or $!$ (resp. ?), and $\$$ is $!w$, or $!c$, or $!\pi$. In the $!w/?w$ ers the contractum is the empty graph.</figcaption></figure>

In Figure 4 we define specific relations called **elementary reduction steps**, **ers** for short. The net at left of an **ers** is the **redex**, that at right the **contractum** of the **ers**. For any union $\mathbb{R}$ among them we define a reduction, denoted $\xrightarrow{\mathbb{R}}$, as the context closure of $\mathbb{R}$. We write by $\xrightarrow{R*}$ the reflexive and transitive closure of $\mathbb{R}$. In particular, we define the **cut-elimination** $\xrightarrow{\text{cut}}$ as the context closure of the whole Figure 4, and the **exponential reduction** $\xrightarrow{e}$ as the context closure of all the **ers** of Figure 4 but the $\otimes/\mathcal{Y}$ **ers**. We say that a differential net $\pi$ **enjoys the cut-elimination** if there is a cut-free differential net $\pi_0$ such that $\pi \xrightarrow{\text{cut}*} \pi_0$.

Notice that the redex of every **ers** in Fig. 4 is a simple net; also the contractum is simple except for $!w/?d$, $!d/?w$, $!d/?c$, $!c/?d$, $!d/p$, and $p/?d$. In particular $!w/?d$ and its symmetric $!d/?w$ yield the empty sum 0. Also the steps $!d/p$ and $p/?d$ yield 0, in case the content of $!\pi$ is 0.

**Proposition 2.** Let $\pi \xrightarrow{\text{cut}} \pi'$. If $\pi$ is switching acyclic, then so it is $\pi'$.

*Proof.* [ER06] gives the proof for the box-free case: the generalization is easy.

<figure><img src="image_7.png" /><figcaption>**Fig. 5:** a simple net not enjoying cut-elimination, nor switching acyclicity.</figcaption></figure>

<footnote n="5">⁵ Although intuitively clear, the operation of merging wires should be handled with care because each of the two interfaces $a$ and $b$ may contain pairs of ports wired together and then loops can be produced. We refer to [Vau07] for a formal definition.</footnote>
*Examples.* Figure 5 depicts a (typed) simple net not enjoying cut-elimination nor switching acyclicity (Figure 5(b) gives its cyclic correctness graph): as known, switching acyclicity is an hypothesis needed to prove<sup>6</sup> cut-elimination. Notice that replacing the !c-cell of Fig. 5(a) with a box gives a counter-example to the cut-elimination for switching cyclic LL nets.

<figure><img src="image_8.png" /><figcaption>Fig. 6: example of a reduction to a cut-free differential net.</figcaption></figure>

Figure 6 gives an example of reduction from the (switching acyclic) simple net in Fig. 6(a) to the cut-free differential net in Fig. 6(f); by the way, notice that the sequent conclusion $X^{\perp}, !X, !X$ is provable in DiLL but not in LL. Let us comment the main ers. In the step (a) $\mathrel{\substack{p/?c \\ \rightarrow}}$ (b) the size of the reduced net is increased since a box is duplicated; moreover, the reduction affects the commutative cut incident to the duplicated box, changing its type from $!d/p$ to $!d/?c$. The fact that the reduction of a cut may affect other cuts takes away from the interaction net paradigm. The step (b) $\mathrel{\substack{!d/?c \\ \rightarrow}}$ (c) creates a sum and duplicates cuts even outside boxes. This duplication is closed to the additive duplication in the sliced proof-nets of LL, but the acquainted reader should observe that in the sliced proof-nets the sums cannot be created (see [PTdF07] for more details). The reduction then focuses on the left addendum of the sum, and reduces a $p/?d$ redex, getting the differential net in (d). The step (d) $\mathrel{\substack{!d/p \\ \rightarrow}}$ (e) is the real crucial one, and shows the main oddities of the cut-elimination of DiLL with boxes. As in the $p/?c$ ers, the size of the reduced net is increased and the reduction affects other cuts, but now among the affected cuts there is the one crossing the principal port of

<footnote n="6"><sup>6</sup> Actually, one can weaken switching acyclicity into *visible acyclicity* [Pag06], keeping cut-elimination.</footnote>
the box involved in the reduction, which can be non commutative. Having ers
affecting non commutative cuts is a peculiarity of DiLL with boxes and makes
subtle importing techniques developed in LL.

## 2 The Cut-Elimination Theorem

We prove our main result: switching acyclic differential nets enjoy the cut-elimination (Theorem 1). This result is achieved by purely combinatorial means, specifically by induction on the pair $\langle \text{grade}(\pi), \text{count}(\pi) \rangle$, lexicographically ordered, where grade and count are measures defined in Definition 1.

We actually guess that $\xrightarrow{\text{cut}}$ is also strongly normalizing$^7$, but its proof should be quite hard and it deserves further research.

**Definition 1.** The grade of a formula *A* is the number grade(*A*) of connectives occurring in *A*; the grade({*a*, *b*}) of a wire {*a*, *b*} is the grade of the type of (*a*, *b*) (or equivalently of the type of (*b*, *a*)). The grade(*π*) of a differential net *π* is the maximum grade of the cuts at any depth of *π*, if any, otherwise it is 0. The count of a differential net *π* is the number count(*π*) of the cuts at any depth of *π* having grade equal to grade(*π*).

Notice that $\pi$ is cut-free iff $\text{grade}(\pi) = 0$ iff $\text{count}(\pi) = 0$. Moreover, consider two differential nets $\rho$ and $\rho'$ s.t. $\langle\text{grade}(\rho'), \text{count}(\rho')\rangle < \langle\text{grade}(\rho), \text{count}(\rho)\rangle$, and a differential net $\pi$ having a box $o \in_! \pi$ of type $!\rho$ and $\text{grade}(\pi) = \text{grade}(\rho)$, then the differential net $\pi'$ defined from $\pi$ by replacing $o$ with a box $o'$ of type $!\rho'$, enjoys $\langle\text{grade}(\pi'), \text{count}(\pi')\rangle < \langle\text{grade}(\pi), \text{count}(\pi)\rangle$.

Recall Figure 4 and remark that the pair $\langle \text{grade}(\pi), \text{count}(\pi) \rangle$, lexicographically ordered, shrinks whenever an ers of type among $\otimes/\mathbb{S}$, $\mathbf{p}/?\mathbf{d}$, $!\mathbf{d}/?\mathbf{d}$, $!\mathbf{w}/?\mathbf{w}$, $!\mathbf{d}/?\mathbf{w}$, $!\mathbf{w}/?\mathbf{d}$, $\mathbf{p}/?\mathbf{w}$ is applied to a cut of $\pi$ with maximal grade. This is not the case for the other types of ers: they are indeed handled by Lemma 1, stating that any cut with exponential type can be reduced into several (possibly 0) cuts with strictly lesser grade. Lemma 1 is proved by induction on the rank a measure defined as follows.

**Definition 2.** We define simultaneously the rank of a cell and the rank of a differential net, by induction on the depth. The rank($\pi$) of a differential net $\pi$ is the maximum rank of its simple nets; the rank of a simple net is the sum of the ranks of its cells; the rank of a cell $c$ is the number

$$
\mathrm{rank}(c) := \begin{cases} (n+1)(\mathrm{rank}(\rho) + 2 + n) & \text{if } c \text{ is a box } !\rho \text{ crossing } n+1 \text{ ports,} \\ 1 & \text{otherwise.} \end{cases}
$$

Recall Figure 4 and notice that the rank of every simple net in the contractum
of a !d/p ers is strictly smaller than that of its redex, so justifying Definition 2.

<footnote>$^7$ For every $\pi$ switching acyclic there is no infinite $\{\pi_i\}_{i \in \mathbb{N}}$ s.t. $\pi_0 = \pi$ and $\pi_i \xrightarrow{\text{cut}} \pi_{i+1}$.</footnote>
<figure><img src="image_9.png" /><figcaption>**Fig. 7:** inductive definition of the !-trees; the ?-trees are defined similarly, using ?-types and ?-cells, except for the !π-case, which does not yield a ?-tree.</figcaption></figure>

**Definition 3.** A !-tree (resp. ?-tree) is a simple net α with a distinguished free port a of type !A (resp. ?A), for a suitable A, called the **root** of α, and such that one of the following inductive conditions hold (see Figure 7):

- α is a wire crossing a;

- α is a !d-cell or a !w-cell (resp. ?d-cell or ?w-cell) with its incident wires and a is the free port wired to the principal port of this cell;

- (only for the !-trees) α is a box !π with its incident wires and a is the free port wired to the principal port of the box;

- α is made of a cocontraction (resp. contraction) l, its incident wires and two !-trees (resp. ?-trees) having their roots auxiliary ports of l, and a is the free port wired to l

Notice a ?-tree is cut-free and switching acyclic; the same holds for !-trees, supposed that the contents of their boxes are resp. cut-free and switching acyclic.

**Lemma 1 (Exponential Lemma).** Let !A be a formula, $\alpha^a = \langle \alpha_1^{a_1}, \dots, \alpha_n^{a_n} \rangle$ be a sequence of $n \ge 1$ !-trees having the root $a_i$ of type !A, and let $\beta^b$ be a simple net with $\mathbf{b} = \langle b_1, \dots, b_n \rangle$ distinguished free ports of type $?A^\perp$. Suppose also $\text{grade}(\beta) < \text{grade}(!A)$ and for every $i \le n$, $\text{grade}(\alpha_i) < \text{grade}(!A)$. The interaction $\langle \beta^b | \alpha^a \rangle$ e-reduces to a differential net $\pi$ such that $\text{grade}(\pi) < \text{grade}(!A)$:

$$ \langle \beta^b | \alpha^a \rangle := \frac{\left( \begin{array}{c|c} \alpha_1 & \\ \hline \beta & \end{array} \right) \dots \left( \begin{array}{c|c} \alpha_n & \\ \hline \beta & \end{array} \right)}{\left( \begin{array}{c|c} c_1 & \\ \hline \beta & \end{array} \right)^{c_n}} \xrightarrow{e^*} \pi, \quad \text{with } \text{grade}(\pi) < \text{grade}(!A). $$

*Proof.* The proof is by induction on the pair $\langle \max_{i \le n}(\text{rank}(\alpha_i)), \text{rank}(\beta) \rangle$, lex-icographically ordered. If no wire $\{c_i, d_i\}$ linking $\beta$ to the !-trees is a cut, then we simply set $\pi = \langle \beta | \alpha \rangle$ (in the sequel we will omit the superscripts **b** and **a**). Otherwise, suppose w.l.o.g. that the wire $\{c_1, d_1\}$ is a cut. The proof splits in several cases, depending on the type of the ers associated with $\{c_1, d_1\}$. We consider only the most delicate cases, the others being straightforward or easy variants of those presented here. In the sequel, $\alpha'$ denotes $\langle \alpha_2^{a_2}, \dots, \alpha_n^{a_n} \rangle$.

**CASE I (p/?d).** If $\alpha_1$ is a box o of type !ρ and $c_1$ is the principal port of a ?d-cell k (see the leftmost net of Fig. 8), then $\langle \beta | \alpha \rangle \xrightarrow{p/?d} \sum_{\delta \in \rho} \gamma_\delta$, where $\gamma_\delta$
is obtained from $\langle\beta|\alpha'\rangle$ by replacing the redex made of $o$ and $k$ with $\delta$ (see the rightmost net of Figure 8). Call $\beta'$ the subnet of $\beta$ not containing the ?d-cell $k$.

<figure><img src="image_10.png" /><figcaption>Fig. 8: case p/?d.</figcaption></figure>

Consider $\langle\beta'|\alpha'\rangle$, which is a subnet of every $\gamma_\delta$, for $\delta \in \rho$. Obviously we have $\max_{2 \le i \le n}(\text{rank}(\alpha_i)) \le \max_{i \le n}(\text{rank}(\alpha_i))$ and $\text{rank}(\beta') = \text{rank}(\beta) - 1$, hence we can apply the induction hypothesis to $\langle\beta'|\alpha'\rangle$ and get a differential net $\pi'$ such that $\langle\beta'|\alpha'\rangle \xrightarrow{e^*} \pi'$ and $\text{grade}(\pi') < \text{grade}(!A)$. From the hypothesis we have also for every $\delta \in \rho$, $\text{grade}(\delta) < \text{grade}(!A)$.

Define $\pi$ as the interaction $\langle\pi'|\rho\rangle$ between the $A^\perp$ free port of (every simple net of) $\pi'$ and the $A$ free port of (every simple net of) $\rho$. Conclude that $\text{grade}(\pi) < \text{grade}(!A)$ and $\langle\beta|\alpha\rangle \xrightarrow{e^*} \pi$.

CASE II (!c/?d). If $\alpha_1$ is a cocontraction $l$ wired to two !-trees $\alpha_l$ and $\alpha_r$ and the port $c_1$ of $\beta$ is the principal port of a dereliction $k$ (see the leftmost net of Fig. 9), then $\langle\beta|\alpha\rangle$ !c/?d-reduces to $\gamma_l + \gamma_r$, where $\gamma_l$ (resp. $\gamma_r$) is obtained by erasing the !-cell $l$ and by wiring its left (resp. right) auxiliary port, denoted $a_l$ (resp. $a_r$), with the principal port $c_1$ of the dereliction $k$, and its right (resp. left) auxiliary port with the principal port $c_w$ of a new weakening cell (see the differential net at the middle of Figure 9, where one must think that the sum distributes). Call

<figure><img src="image_11.png" /><figcaption>Fig. 9: case !c/?d.</figcaption></figure>

$\beta'$ the subnet of $\beta$ not containing the ?d-cell $k$, and notice $\gamma_l$ (resp. $\gamma_r$) can be decomposed into the subnet $\langle\beta'|\alpha'\rangle$ and the subnet $\langle\beta_0^{c_1 c_w}|\alpha_l^{a_l}, \alpha_r^{a_r}\rangle$ (resp. $\langle\beta_0^{c_1 c_w}|\alpha_r^{a_r}, \alpha_l^{a_l}\rangle$), where $\beta_0$ denotes the simple net formed by the ?d-cell $k$ and the weakening created by the ers.
First, consider $\langle\beta'|\alpha'\rangle$: we have $\max_{2\le i\le n}(\mathrm{rank}(\alpha_i)) \le \max_{i\le n}(\mathrm{rank}(\alpha_i))$ and $\mathrm{rank}(\beta') = \mathrm{rank}(\beta) - 1$, hence we can apply the induction hypothesis and get a differential net $\pi'$ s.t. $\langle\beta'|\alpha'\rangle \xrightarrow{e^*} \pi'$ and $\mathrm{grade}(\pi') < \mathrm{grade}(!A)$. Second, consider the simple net $\langle\beta_0^{c_1 c_w}|\alpha_l^{a_l}, \alpha_r^{a_r}\rangle$: we have $\max(\mathrm{rank}(\alpha_l), \mathrm{rank}(\alpha_r)) < \mathrm{rank}(\alpha_1) \le \max_{i\le n}(\mathrm{rank}(\alpha_i))$, hence we can apply the induction hypothesis and get a differential net $\pi'_l$ satisfying $\langle\beta_0^{c_1 c_w}|\alpha_l^{a_l}, \alpha_r^{a_r}\rangle \xrightarrow{e^*} \pi'_l$ and $\mathrm{grade}(\pi'_l) < \mathrm{grade}(!A)$. Similarly we get a differential net $\pi'_r$ satisfying $\langle\beta_0^{c_1 c_w}|\alpha_r^{a_r}, \alpha_l^{a_l}\rangle \xrightarrow{e^*} \pi'_r$ and $\mathrm{grade}(\pi'_r) < \mathrm{grade}(!A)$.

Finally, we define $\pi$ as the interaction between the $A^{\perp}$ free port of (every simple net of) $\pi'$ with the $A$ free port of (every simple net of) $\pi'_l + \pi'_r$, see Figure 9. We have $\langle\beta|\alpha\rangle \xrightarrow{!c/?d} \gamma_l + \gamma_r \xrightarrow{e^*} \pi$ and $\mathrm{grade}(\pi) < \mathrm{grade}(!A)$.

**CASE III** ($!c/?c$). If $\alpha_1$ is a cocontraction $l$ wired to two !-trees $\alpha_l$ and $\alpha_r$ and the port $c_1$ of $\beta$ is the principal port of a contraction $k$ (see the leftmost net of Figure 10) then $\langle\beta|\alpha\rangle!c/?c$-reduces to the net $\gamma$ in the middle of Figure 10. Let $\beta'$ be the subnet of $\beta$ not containing the contraction $k$, let

<figure><img src="image_12.png" /><figcaption>Fig. 10: case $!c/?c$.</figcaption></figure>

$c_l, c_r$ be the two auxiliary ports of $k$ and let $a_l, a_r$ be the two auxiliary ports of $l$, which are also the roots of resp. $\alpha_l$ and $\alpha_r$. Finally, let $l_l, l_r$ be the two copies of $l$ created by the reduction of $\{c_1, d_1\}$: notice $l_l, l_r$ are !-trees having rank equal to $\mathrm{rank}(l) = 1$. Consider $\langle\beta'|l_l, l_r, \alpha'\rangle$, which is a subnet of $\gamma$. Observe that $\max\{\mathrm{rank}(l), \mathrm{rank}(\alpha_2), \dots, \mathrm{rank}(\alpha_n)\} \le \max_{i\le n}(\mathrm{rank}(\alpha_i))$ and $\mathrm{rank}(\beta') = \mathrm{rank}(\beta) - 1$, hence we can apply the induction hypothesis and get a differential net $\pi'$ such that $\langle\beta'|l_l, l_r, \alpha'\rangle \xrightarrow{e^*} \pi'$ and $\mathrm{grade}(\pi') < \mathrm{grade}(!A)$.

For every $\epsilon \in \pi'$, let $\epsilon^+$ be the net formed by $\epsilon$ and the two copies of the contraction $k$ created by the reduction of $\{c_1, d_1\}$ (see the rightmost simple net of Figure 10). Let us consider the interaction $\langle\epsilon^+|\alpha_l, \alpha_r\rangle$ and notice that $\max(\mathrm{rank}(\alpha_l), \mathrm{rank}(\alpha_r)) < \mathrm{rank}(\alpha_1) \le \max_{i\le n}(\mathrm{rank}(\alpha_i))$. We thus apply the induction hypothesis, getting a differential net $\pi_\epsilon$ s.t. $\langle\epsilon^+|\alpha_l, \alpha_r\rangle \xrightarrow{e^*} \pi_\epsilon$ and $\mathrm{grade}(\pi_\epsilon) < \mathrm{grade}(!A)$. Define $\pi = \sum_{\epsilon \in \pi'} \pi_\epsilon$ and conclude: $\langle\beta|\alpha\rangle \xrightarrow{!c/?c} \gamma \xrightarrow{e^*} \pi$ and $\mathrm{grade}(\pi) < \mathrm{grade}(!A)$.

**CASE IV** ($!d/p$). If $\alpha_1$ is a codereliction $l$ and the port $c_1$ of $\beta$ is an auxiliary port of a promotion $o$ of type $!\rho$ (see the leftmost net of Figure 11), then $\langle\beta|\alpha\rangle$
!d/p-reduces to the differential net $\sum_{\delta \in \rho} \beta^\delta$, where $\beta^\delta$ is obtained from $\beta$ by
replacing $o$ with the simple net $\delta'$ outlined at the right of Figure 11. For every

<figure><img src="image_13.png" /><figcaption>Fig. 11: case !d/p.</figcaption></figure>

$\delta \in \rho$, we have $\text{rank}(\beta^\delta) = \text{rank}(\beta') + \text{rank}(\delta')$, where $\beta'$ is the subnet of $\beta$ not
containing $o$; we have also $\text{rank}(\delta') < \text{rank}(!\rho)$, in fact the rank has been suitably
defined to have any contractum of a !d/p ers strictly smaller than the rank of
its redex (Definition 2). Hence we conclude $\text{rank}(\beta^\delta) < \text{rank}(\beta)$. We apply the
induction hypothesis to $\langle\beta^\delta|\alpha\rangle$ getting a differential net $\pi^\delta$ s.t. $\langle\beta^\delta|\alpha\rangle \xrightarrow{e^*} \pi^\delta$
and $\text{grade}(\pi^\delta) < \text{grade}(!A)$. We define $\pi = \sum_{\delta \in \rho} \pi^\delta$ and we conclude $\langle\beta|\alpha\rangle \xrightarrow{!d/p} \sum_{\delta \in \rho} \beta^\delta \xrightarrow{e^*} \pi$ and $\text{grade}(\pi) < \text{grade}(!A)$.

CASE V (OTHERWISE.). The case !d/?c is an easy variant of the case !c/?d. The case !c/p is similar to the case !c/?c: indeed, adopting the notation of Fig. 10, one has to apply three times the induction hypothesis — once applied to $\langle\beta'|\alpha'\rangle$, once to the contents of the box involved in the !c/p ers, and a last time to the interaction with the !-trees residue of $\alpha_l$ and $\alpha_r$. The p/?c, and p/p cases are variations of the case !c/p. The other cases are obvious. □

Let us stress that in general the count of the differential net $\pi$ mentioned
in Lemma 1 may be greater than count($\langle\beta^b|\alpha^a\rangle$): what decreases is the grade.
This motivates the introduction of two distinct measures, grade and count.

**Theorem 1.** For every switching acyclic $\pi$, there is a cut-free $\pi_0$ s.t. $\pi \xrightarrow{\text{cut}*} \pi_0$.

*Proof.* The proof is by induction on the pair $\langle\text{grade}(\pi), \text{count}(\pi)\rangle$, lexicographically ordered. Let $\{a, b\} \in! \pi$ be a cut having maximal grade, i.e. $\text{grade}(\{a, b\}) = \text{grade}(\pi)$, and having maximal depth among the cuts with maximal grade in $\pi$. Let $\alpha$ be the simple net of $\pi$ or of the contents of a box in $\pi$, having $\{a, b\}$ at depth 0. Our goal is to prove that:

(*) there is a cut-free differential net $\rho_\alpha$ such that $\alpha \xrightarrow{\text{cut}*} \rho_\alpha$.

First we show that (*) entails that $\pi$ enjoys the cut-elimination. Indeed since
$\text{grade}(\alpha) = \text{grade}(\pi)$, the differential net $\pi'$ obtained from $\pi$ by substituting
$\alpha$ with $\rho_\alpha$ meets $\langle\text{grade}(\pi'), \text{count}(\pi')\rangle < \langle\text{grade}(\pi), \text{count}(\pi)\rangle$. Since $\pi \xrightarrow{\text{cut}*} \pi'$ and $\pi'$ is switching acyclic (Proposition 2), we conclude by induction hypothesis.

So let us prove (*). The multiplicative case is straightforward. Then suppose $\{a, b\}$ has an exponential type, let $a : !A$ and $b : ?A^\perp$. Let $\alpha!$ be the maximal !-tree of $\alpha$ with root $a$, and let $\alpha?^\gamma$ be the maximal ?-tree of $\alpha$ with root $b$. Let moreover $o_1, \dots, o_n$, for $n \ge 0$, be the boxes of $\alpha$ having one, or more, auxiliary port !A as free port of $\alpha?^\gamma$, and let $\alpha?^{\gamma+}$ be the simple net made of $\alpha?^\gamma$ and of these boxes $o_1, \dots, o_n$. Notice that there is no cut between $\alpha?^\gamma$ and any box $o_i$: indeed, $\alpha?^\gamma$ is a ?-tree, hence none of its free ports is connected to an active port, but $b$. By the switching acyclicity of $\alpha$, the !-tree $\alpha!$ and the simple net $\alpha?^{\gamma+}$ are disjoint, i.e. the sets of the ports in resp. $\alpha!$ and $\alpha?^{\gamma+}$ are disjoint. This means that $\alpha$ may be expressed as the interaction among three simple nets: $\alpha!$, $\alpha?^{\gamma+}$ and a simple net $\beta$, as follows

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

where we denote by $I$ the set of wires, possibly empty, shared between $\beta$ and $\langle\alpha^{?+}|\alpha!\rangle$. Notice that each wire $\{c, d\} \in I$, $d$ denoting the free port for $\beta$, meets exactly one of the following three conditions:

i. either $d$ is an auxiliary port of a !$d$-cell in $\alpha!$ (resp. ?$d$-cell in $\alpha?^\gamma$), and $c$ has type $A^\perp$ (resp. $A$);

ii. or $d$ is an auxiliary port of a !$c$-cell in $\alpha!$ (resp. ?$c$-cell in $\alpha?^\gamma$), and $c$ is of type $?A^\perp$ (resp. !$A$) and it is not active (i.e. nor principal port, neither auxiliary port of a box): in fact if $c$ were the principal port of a cell, then this cell should be a !-cell (resp. ?-cell), and $\alpha!$ (resp. $\alpha?^\gamma$) would not be maximal, while if $c$ were the auxiliary port of a box then $c$ would be a free port of $\alpha?^\gamma$ and this box would be one $o_i$ added to $\alpha?^{\gamma+}$;

iii. or $d$ is an auxiliary port of a box in $\alpha!$ or an auxiliary or principal port of a box $o_i$ in $\alpha?^{\gamma+}$.

By hypothesis, the contents of every box of $\alpha$ have a strictly smaller grade than $\text{grade}(\alpha)$, and so it is in particular for the boxes in $\alpha!$ and those in $\alpha?^{\gamma+}$. We then deduce $\text{grade}(\alpha?^{\gamma+})$, $\text{grade}(\alpha!) < \text{grade}(\alpha) = \text{grade}(\{a, b\})$. This means we can apply Lemma 1 to $\langle\alpha?^{\gamma+}|\alpha!\rangle$, and get a differential net $\rho'$ such that $\langle\alpha?^{\gamma+}|\alpha!\rangle \xrightarrow{\text{e}*} \rho'$ and $\text{grade}(\rho') < \text{grade}(\{a, b\})$. For every $\gamma \in \rho'$, the interaction $\langle\beta|\gamma\rangle$ is the result of replacing in $\alpha$ the subnet $\langle\alpha?^{\gamma+}|\alpha!\rangle$ with $\gamma$. So we have $\alpha \xrightarrow{\text{e}*} \sum_{\gamma \in \rho'} \langle\beta|\gamma\rangle$.

For every $\gamma \in \rho'$ we prove $\langle\text{grade}(\langle\beta|\gamma\rangle), \text{count}(\langle\beta|\gamma\rangle)\rangle < \langle\text{grade}(\alpha), \text{count}(\alpha)\rangle$. Clearly we have $\text{grade}(\langle\beta|\gamma\rangle) \le \text{grade}(\alpha)$, so assume $\text{grade}(\langle\beta|\gamma\rangle) = \text{grade}(\alpha)$ and let us prove $\text{count}(\langle\beta|\gamma\rangle) < \text{count}(\alpha)$. This amounts to count the cuts with $\text{grade}(\alpha)$ in $\langle\beta|\gamma\rangle$ and those in $\alpha = \langle\beta|\langle\alpha?^{\gamma+}|\alpha!\rangle\rangle$. Let us start with $\langle\beta|\gamma\rangle$: