# An application of parallel cut elimination in multiplicative linear logic to
the Taylor expansion of proof nets

Jules Chouquet  IRIF UMR 8243, Université Paris Diderot, Sorbonne Paris Cité,
CNRS, France<EMAIL_ADDRESS>and  Lionel Vaux Auclair  Aix-Marseille
Univ, CNRS, Centrale Marseille, I2M, Marseille, France  lionel.vaux@univ-
amu.fr https://orcid.org/0000-0001-9466-418X

###### Abstract.

We examine some combinatorial properties of parallel cut elimination in
multiplicative linear logic (MLL) proof nets. We show that, provided we impose
a constraint on some paths, we can bound the size of all the nets satisfying
this constraint and reducing to a fixed resultant net. This result gives a
sufficient condition for an infinite weighted sum of nets to reduce into
another sum of nets, while keeping coefficients finite. We moreover show that
our constraints are stable under reduction.

Our approach is motivated by the quantitative semantics of linear logic: many
models have been proposed, whose structure reflect the Taylor expansion of
multiplicative exponential linear logic (MELL) proof nets into infinite sums
of differential nets. In order to simulate one cut elimination step in MELL,
it is necessary to reduce an arbitrary number of cuts in the differential nets
of its Taylor expansion. It turns out our results apply to differential nets,
because their cut elimination is essentially multiplicative. We moreover show
that the set of differential nets that occur in the Taylor expansion of an
MELL net automatically satisfies our constraints.

Interestingly, our nets are untyped: we only rely on the sequentiality of
linear logic nets and the dynamics of cut elimination. The paths on which we
impose bounds are the switching paths involved in the Danos–Regnier criterion
for sequentiality. In order to accommodate multiplicative units and
weakenings, our nets come equipped with jumps: each weakening node is
connected to some other node. Our constraint can then be summed up as a bound
on both the length of switching paths, and the number of weakenings that jump
to a common node.

##  1\. Introduction

###  1.1. Context: quantitative semantics and Taylor expansion

Linear logic takes its roots in the denotational semantics of
$\lambda$-calculus: it is often presented, by Girard himself [Gir87], as the
result of a careful investigation of the model of coherence spaces. Since its
early days, linear logic has thus generated a rich ecosystem of denotational
models, among which we distinguish the family of _quantitative semantics_.
Indeed, the first ideas behind linear logic were exposed even before coherence
spaces, in the model of normal functors [Gir88], in which Girard proposed to
consider analyticity, instead of mere continuity, as the key property of the
interpretation of $\lambda$-terms: in this setting, terms denote power series,
representing analytic maps between modules.

This quantitative interpretation reflects precise operational properties of
programs: the degree of a monomial in a power series is closely related to the
number of times a function uses its argument. Following this framework,
various models were considered — among which we shall include the multiset
relational model as a degenerate, boolean-valued instance. These models
allowed to represent and characterize quantitative properties such as the
execution time [dC09], including best and worst case analysis for non-
deterministic programs [LMMP13], or the probability of reaching a value
[DE11]. It is notable that this whole approach gained momentum in the early
2000’s, after the introduction by Ehrhard of models [Ehr02, Ehr05] in which
the notion of analytic maps interpreting $\lambda$-terms took its usual sense,
while Girard’s original model involved set-valued formal power series. Indeed,
the keystone in the success of this line of work is an analogue of the Taylor
expansion formula, that can be established both for $\lambda$-terms and for
linear logic proofs.

Mimicking this denotational structure, Ehrhard and Regnier introduced the
differential $\lambda$-calculus [ER03] and differential linear logic [ER05],
which allow to formulate a syntactic version of Taylor expansion: to a
$\lambda$-term (resp. to a linear logic proof), we associate an infinite
linear combination of approximants [ER08, Ehr16]. In particular, the dynamics
(_i.e._ $\beta$-reduction or cut elimination) of those systems is dictated by
the identities of quantitative semantics. In turn, Taylor expansion has become
a useful device to design and study new models of linear logic, in which
morphisms admit a matrix representation: the Taylor expansion formula allows
to describe the interpretation of promotion — the operation by which a linear
resource becomes freely duplicable — in an explicit, systematic manner. It is
in fact possible to show that any model of differential linear logic without
promotion gives rise to a model of full linear logic in this way [dC07]: in
some sense, one can simulate cut elimination through Taylor expansion.

###  1.2. Motivation: reduction in Taylor expansion

There is a difficulty, however: Taylor expansion generates infinite sums and,
_a priori_ , there is no guarantee that the coefficients in these sums will
remain finite under reduction. In previous works [dC07, LMMP13], coefficients
were thus required to be taken in a complete semiring: all sums should
converge. In order to illustrate this requirement, let us first consider the
case of $\lambda$-calculus.

The linear fragment of differential $\lambda$-calculus, called resource
$\lambda$-calculus, is the target of the syntactic Taylor expansion of
$\lambda$-terms. In this calculus, the application of a term to another is
replaced with a multilinear variant: $\langle s\rangle[t_{1},\dotsc,t_{n}]$
denotes the $n$-linear symmetric application of resource term $s$ to the
multiset of resource terms $[t_{1},\dotsc,t_{n}]$. Then, if
$x_{1},\dotsc,x_{k}$ denote the occurrences of $x$ in $s$, the redex
$\langle\lambda x.s\rangle[t_{1},\dotsc,t_{n}]$ reduces to the sum
$\sum_{f:\\{1,\dotsc,k\\}\stackrel{{\scriptstyle\sim}}{{\to}}\\{1,\dotsc,n\\}}s[t_{f(1)}/x_{1},\dotsc,t_{f(k)}/x_{k}]$:
here $f$ ranges over all bijections
$\\{1,\dotsc,k\\}\stackrel{{\scriptstyle\sim}}{{\to}}\\{1,\dotsc,n\\}$ so this
sum is zero if $n\not=k$. As sums are generated by reduction, it should be
noted that all the syntactic constructs are linear, both in the sense that
they commute to sums, and in the sense that, in the elimination of a redex, no
subterm of the argument multiset is copied nor erased. The key case of Taylor
expansion is that of application:

$\mathcal{T}(MN)=\sum_{n\in
N}\frac{1}{n!}\langle\mathcal{T}(M)\rangle\mathcal{T}(N)^{n}$ (1)

where $\mathcal{T}(N)^{n}$ is the multiset made of $n$ copies of
$\mathcal{T}(N)$ — by $n$-linearity, $\mathcal{T}(N)^{n}$ is itself an
infinite linear combination of multisets of resource terms appearing in
$\mathcal{T}(N)$. Admitting that $\langle M\rangle[N_{1},\dotsc,N_{n}]$
represents the $n$-th derivative of $M$, computed at $0$, and $n$-linearly
applied to $N_{1}$, …, $N_{n}$, one immediately recognizes the usual Taylor
expansion formula.

From (1), it is immediately clear that, to simulate one reduction step
occurring in $N$, it is necessary to reduce in parallel in an unbounded number
of subterms of each component of the expansion. Unrestricted parallel
reduction, however, is ill defined in this setting. Consider the sum
$\sum_{n\in\mathbf{N}}\langle\lambda xx\rangle[\cdots\langle\lambda
xx\rangle[y]\cdots]$ where each summand consists of $n$ successive linear
applications of the identity to the variable $y$: then by simultaneous
reduction of all redexes in each component, each summand yields $y$, so the
result should be $\sum_{n\in\mathbf{N}}y$ which is not defined unless the
semiring of coefficients is complete in some sense.

Those considerations apply to linear logic as well as to $\lambda$-calculus.
We will use proof nets [Gir87] as the syntax for proofs of multiplicative
exponential linear logic (MELL). The target of Taylor expansion is then in
promotion-free differential nets [ER05], which we call _resource nets_ in the
following, by analogy with the resource $\lambda$-calculus: these form the
multilinear fragment of differential linear logic.

$\oc$$\cdots$$?$$?$$\cdots$$P$

expands to $\sum_{n\in\mathbf{N}}\frac{1}{n!}\leavevmode\hbox to154.05pt{\vbox
to60.15pt{\pgfpicture\makeatletter\hbox{\hskip-8.3359pt\lower-42.87956pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}} {}{}{{}}{} {}{} {}{} {}{}
{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{8.5359pt}{4.0pt}\pgfsys@lineto{8.5359pt}{13.07182pt}\pgfsys@curveto{8.5359pt}{15.28099pt}{10.32674pt}{17.07182pt}{12.5359pt}{17.07182pt}\pgfsys@lineto{72.82323pt}{17.07182pt}\pgfsys@curveto{75.0324pt}{17.07182pt}{76.82323pt}{15.28099pt}{76.82323pt}{13.07182pt}\pgfsys@lineto{76.82323pt}{4.0pt}\pgfsys@curveto{76.82323pt}{1.79083pt}{75.0324pt}{0.0pt}{72.82323pt}{0.0pt}\pgfsys@lineto{12.5359pt}{0.0pt}\pgfsys@curveto{10.32674pt}{0.0pt}{8.5359pt}{1.79083pt}{8.5359pt}{4.0pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
}
{}{{}}{}{{}}{}\pgfsys@moveto{37.55797pt}{-5.12158pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{33.80797pt}{-7.62158pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\cdots$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{}{{}}{}{{}}{}\pgfsys@moveto{42.67957pt}{8.5359pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{31.27504pt}{6.0359pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\mathcal{T}(P)$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\par{}{{}}{}{{}}{}\pgfsys@moveto{85.35913pt}{8.5359pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{79.50832pt}{6.0359pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\stackrel{{\scriptstyle n}}{{\cdots}}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \par{}{}{{}}{} {}{} {}{}
{}{}
{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{93.89505pt}{4.0pt}\pgfsys@lineto{93.89505pt}{13.07182pt}\pgfsys@curveto{93.89505pt}{15.28099pt}{95.68588pt}{17.07182pt}{97.89505pt}{17.07182pt}\pgfsys@lineto{158.18237pt}{17.07182pt}\pgfsys@curveto{160.39154pt}{17.07182pt}{162.18237pt}{15.28099pt}{162.18237pt}{13.07182pt}\pgfsys@lineto{162.18237pt}{4.0pt}\pgfsys@curveto{162.18237pt}{1.79083pt}{160.39154pt}{0.0pt}{158.18237pt}{0.0pt}\pgfsys@lineto{97.89505pt}{0.0pt}\pgfsys@curveto{95.68588pt}{0.0pt}{93.89505pt}{1.79083pt}{93.89505pt}{4.0pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
}
{}{{}}{}{{}}{}\pgfsys@moveto{128.03871pt}{8.5359pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{116.63419pt}{6.0359pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\mathcal{T}(P)$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{}{{}}{}{{}}{}\pgfsys@moveto{116.08847pt}{-5.12158pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{112.33847pt}{-7.62158pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\cdots$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\par{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{66.2097pt}{-29.87569pt}\pgfsys@curveto{66.2097pt}{-26.30882pt}{63.31825pt}{-23.41737pt}{59.75139pt}{-23.41737pt}\pgfsys@curveto{56.18452pt}{-23.41737pt}{53.29308pt}{-26.30882pt}{53.29308pt}{-29.87569pt}\pgfsys@curveto{53.29308pt}{-33.44255pt}{56.18452pt}{-36.334pt}{59.75139pt}{-36.334pt}\pgfsys@curveto{63.31825pt}{-36.334pt}{66.2097pt}{-33.44255pt}{66.2097pt}{-29.87569pt}\pgfsys@closepath\pgfsys@moveto{59.75139pt}{-29.87569pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{57.62639pt}{-33.00069pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{\small{$?$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{100.35336pt}{-29.87569pt}\pgfsys@curveto{100.35336pt}{-26.30882pt}{97.46191pt}{-23.41737pt}{93.89505pt}{-23.41737pt}\pgfsys@curveto{90.32819pt}{-23.41737pt}{87.43674pt}{-26.30882pt}{87.43674pt}{-29.87569pt}\pgfsys@curveto{87.43674pt}{-33.44255pt}{90.32819pt}{-36.334pt}{93.89505pt}{-36.334pt}\pgfsys@curveto{97.46191pt}{-36.334pt}{100.35336pt}{-33.44255pt}{100.35336pt}{-29.87569pt}\pgfsys@closepath\pgfsys@moveto{93.89505pt}{-29.87569pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{91.77005pt}{-33.00069pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{\small{$?$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{117.42519pt}{-29.87569pt}\pgfsys@curveto{117.42519pt}{-26.30882pt}{114.53374pt}{-23.41737pt}{110.96687pt}{-23.41737pt}\pgfsys@curveto{107.40001pt}{-23.41737pt}{104.50856pt}{-26.30882pt}{104.50856pt}{-29.87569pt}\pgfsys@curveto{104.50856pt}{-33.44255pt}{107.40001pt}{-36.334pt}{110.96687pt}{-36.334pt}\pgfsys@curveto{114.53374pt}{-36.334pt}{117.42519pt}{-33.44255pt}{117.42519pt}{-29.87569pt}\pgfsys@closepath\pgfsys@moveto{110.96687pt}{-29.87569pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{109.71687pt}{-33.00069pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{\small{$!$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{57.87717pt}{-21.01767pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\tiny{\vbox{\halign{\hfil#\hfil\cr\cr\vskip
2.0pt\cr\hbox{{$\ldots$}}\cr}}}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{92.02127pt}{-21.01767pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\tiny{\vbox{\halign{\hfil#\hfil\cr\cr\vskip
2.0pt\cr\hbox{{$\ldots$}}\cr}}}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}{{{{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{109.09332pt}{-21.01767pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\tiny{\vbox{\halign{\hfil#\hfil\cr\cr\vskip
2.0pt\cr\hbox{{$\ldots$}}\cr}}}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{73.07323pt}{-32.37569pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\cdots$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \par{{}}{}
{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@moveto{59.75217pt}{-36.53447pt}\pgfsys@lineto{59.75139pt}{-42.67957pt}\pgfsys@stroke\pgfsys@invoke{
} {{}}{}
{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@moveto{93.89627pt}{-36.53447pt}\pgfsys@lineto{93.89505pt}{-42.67957pt}\pgfsys@stroke\pgfsys@invoke{
} {{}}{}
{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@moveto{110.96832pt}{-36.53447pt}\pgfsys@lineto{110.96687pt}{-42.67957pt}\pgfsys@stroke\pgfsys@invoke{
} \par{}{{}}{} {{}{}{{}}{}}{{}{}}{{}}
{{{}}{{}}}{{}}{{}{}{{}}{}}{{{}}{{}}}{{}}{}{{}}{{{{{{}}{}{}{}{}{{}}}}}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{2.79999pt}\pgfsys@invoke{
}{}\pgfsys@moveto{17.07182pt}{0.0pt}\pgfsys@curveto{17.07182pt}{-17.94821pt}{45.63837pt}{-9.7195pt}{55.93315pt}{-24.42183pt}\pgfsys@stroke\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{\pgfsys@setlinewidth{2.0pt}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@invoke{
}\pgfsys@moveto{17.07182pt}{0.0pt}\pgfsys@curveto{17.07182pt}{-17.94821pt}{45.63837pt}{-9.7195pt}{55.93315pt}{-24.42183pt}\pgfsys@stroke\pgfsys@invoke{
}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope {}{{}}{}
{{}{}{{}}{}}{{}{}}{{}}
{{{}}{{}}}{{}}{{}{}{{}}{}}{{{}}{{}}}{{}}{}{{}}{{{{{{}}{}{}{}{}{{}}}}}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{2.79999pt}\pgfsys@invoke{
}{}\pgfsys@moveto{51.21548pt}{0.0pt}\pgfsys@curveto{51.21548pt}{-17.94844pt}{79.78235pt}{-9.71931pt}{90.07738pt}{-24.42174pt}\pgfsys@stroke\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{\pgfsys@setlinewidth{2.0pt}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@invoke{
}\pgfsys@moveto{51.21548pt}{0.0pt}\pgfsys@curveto{51.21548pt}{-17.94844pt}{79.78235pt}{-9.71931pt}{90.07738pt}{-24.42174pt}\pgfsys@stroke\pgfsys@invoke{
}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope {}{{}}{}
{{}{}{{}}{}}{{}{}}{{}}
{{{}}{{}}}{{}}{{}{}{{}}{}}{{{}}{{}}}{{}}{}{{}}{{{{{{}}{}{}{}{}{{}}}}}{}{}{}{}}{}\pgfsys@moveto{68.28731pt}{0.0pt}\pgfsys@curveto{68.28731pt}{-17.94856pt}{96.85432pt}{-9.71922pt}{107.14943pt}{-24.42174pt}\pgfsys@stroke\pgfsys@invoke{
} \par{}{{}}{} {{}{}{{}}{}}{{}{}}{{}}
{{{}}{{}}}{{}}{{}{}{{}}{}}{{{}}{{}}}{{}}{}{{}}{{{{{{}}{}{}{}{}{{}}}}}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{2.79999pt}\pgfsys@invoke{
}{}\pgfsys@moveto{102.43097pt}{0.0pt}\pgfsys@curveto{102.43097pt}{-17.94753pt}{73.86557pt}{-9.72006pt}{63.57147pt}{-24.42192pt}\pgfsys@stroke\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{\pgfsys@setlinewidth{2.0pt}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@invoke{
}\pgfsys@moveto{102.43097pt}{0.0pt}\pgfsys@curveto{102.43097pt}{-17.94753pt}{73.86557pt}{-9.72006pt}{63.57147pt}{-24.42192pt}\pgfsys@stroke\pgfsys@invoke{
}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope {}{{}}{}
{{}{}{{}}{}}{{}{}}{{}}
{{{}}{{}}}{{}}{{}{}{{}}{}}{{{}}{{}}}{{}}{}{{}}{{{{{{}}{}{}{}{}{{}}}}}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{2.79999pt}\pgfsys@invoke{
}{}\pgfsys@moveto{136.57463pt}{0.0pt}\pgfsys@curveto{136.57463pt}{-17.9473pt}{108.00955pt}{-9.72025pt}{97.71568pt}{-24.42203pt}\pgfsys@stroke\pgfsys@invoke{
}\pgfsys@beginscope\pgfsys@invoke{
}{\pgfsys@setlinewidth{2.0pt}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.75,0.75,0.75}\pgfsys@color@gray@stroke{0.75}\pgfsys@invoke{
}\pgfsys@moveto{136.57463pt}{0.0pt}\pgfsys@curveto{136.57463pt}{-17.9473pt}{108.00955pt}{-9.72025pt}{97.71568pt}{-24.42203pt}\pgfsys@stroke\pgfsys@invoke{
}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope {}{{}}{}
{{}{}{{}}{}}{{}{}}{{}}
{{{}}{{}}}{{}}{{}{}{{}}{}}{{{}}{{}}}{{}}{}{{}}{{{{{{}}{}{}{}{}{{}}}}}{}{}{}{}}{}\pgfsys@moveto{153.64645pt}{0.0pt}\pgfsys@curveto{153.64645pt}{-17.94724pt}{125.08156pt}{-9.7203pt}{114.78772pt}{-24.42203pt}\pgfsys@stroke\pgfsys@invoke{
} \par \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}$

Figure 1. Taylor expansion of a promotion box (thick wires denote an arbitrary
number of wires)

In linear logic, Taylor expansion consists in replacing duplicable subnets,
embodied by promotion boxes, with explicit copies, as in Figure 1: if we take
$n$ copies of the box, the main port of the box is replaced with an $n$-ary
$\oc$-link, while the $\wn$-links at the border of the box collect all copies
of the corresponding auxiliary ports. Again, to follow a single cut
elimination step in $P$, it is necessary to reduce an arbitrary number of
copies. And unrestricted parallel cut elimination in an infinite sum of
resource nets is broken, as one can easily construct an infinite family of
nets, all reducing to the same resource net $p$ in a single step of parallel
cut elimination: see Figure 2.

axcutaxcut$\stackrel{{\scriptstyle n}}{{\cdots}}$$p$ Figure 2. Example of a
family of nets, all reducing to a single net $p$, by the parallel elimination
of axiom cuts.

###  1.3. Our approach: taming the combinatorial explosion of antireduction

The problem of convergence of series of linear approximants under reduction
was first tackled by Ehrhard and Regnier, for the normalization of Taylor
expansion of ordinary $\lambda$-terms [ER08]. Their argument relies on a
uniformity property, specific to the pure $\lambda$-calculus: the support of
the Taylor expansion of a $\lambda$-term forms a clique in some fixed
coherence space of resource terms. This method cannot be adapted to proof
nets: there is no coherence relation on differential nets such that all
supports of Taylor expansions are cliques [Tas09, Section V.4.1].

An alternative method to ensure convergence without any uniformity hypothesis
was first developed by Ehrhard for typed terms in a $\lambda$-calculus
extended with linear combinations of terms [Ehr10]: there, the presence of
sums also forbade the existence of a suitable coherence relation. This method
can be generalized to strongly normalizable [PTV16], or even weakly
normalizable [Vau17] terms. One striking feature of this approach is that it
concentrates on the support (_i.e._ the set of terms having non-zero
coefficients) of the Taylor expansion. In each case, one shows that, given a
normal resource term $t$ and a $\lambda$-term $M$, there are finitely many
terms $s$, such that:

  * •

the coefficient of $s$ in $\mathcal{T}(M)$ is non zero; and

  * •

the coefficient of $t$ in the normal form of $s$ is non zero.

This allows to normalize the Taylor expansion: simply normalize in each
component, then compute the sum, which is component-wise finite.

The second author then remarked that the same could be done for
$\beta$-reduction [Vau17], even without any uniformity, typing or
normalizability requirement. Indeed, writing $s\rightrightarrows t$ if $s$ and
$t$ are resource terms such that $t$ appears in the support of a parallel
reduct of $s$, the size of $s$ is bounded by a function of the size of $t$
_and_ the height of $s$. So, given that if $s$ appears in $\mathcal{T}(M)$
then its height is bounded by that of $M$, it follows that, for a fixed
resource term $t$ there are finitely many terms $s$ in the support of
$\mathcal{T}(M)$ such that $s\rightrightarrows t$: in short, parallel
reduction is always well-defined on the Taylor expansion of a $\lambda$-term.

Our purpose in the present paper is to develop a similar technique for MELL
proof nets: we show that one can bound the size of a resource net $p$ by a
function of the size of any of its parallel reducts, and of an additional
quantity on $p$, yet to be defined. The main challenge is indeed to circumvent
the lack of inductive structure in proof nets: in such a graphical syntax,
there is no structural notion of height.

We claim that a side condition on switching paths, _i.e._ paths in the sense
of Danos–Regnier’s correctness criterion [DR89], is an appropriate
replacement. Backing this claim, there are first some intuitions:

  * •

the main culprits for the unbounded loss of size in reduction are the chains
of consecutive cuts, as in Figure 2;

  * •

we want the validity of our side condition to be stable under reduction so,
rather than chains of cuts, we should consider the length of switching paths;

  * •

indeed, if $p$ reduces to $q$ _via_ cut elimination, then the switching paths
of $q$ are somehow related with those of $p$;

  * •

and the switching paths of a resource net in $\mathcal{T}(P)$ are somehow
related with those of $P$.

In the following we will establish precise formulations of those last two
points: we study the structure of switching paths through cut elimination in
Section 4; and we describe the switching paths of the elements of
$\mathcal{T}(P)$ in Section 7.

$+$cut$-$$+$cut$-$${\cdots}$$p$ Figure 3. Evanescent cuts: here each $(+)$
node can denote a tensor unit $\mathbf{1}$ or a coweakening (a nullary
$\oc$-link), and then the corresponding $(-)$ node should be the dual unit
$\bot$ or a weakening (a nullary $\wn$-link). Then the depicted net reduces to
$p$ in one parallel cut elimination step.

In presence of multiplicative units, or of weakenings (nullary $\wn$-links)
and coweakenings (nullary $\oc$-links), we must also take special care of
another kind of cuts, that we call _evanescent cuts_ : when a cut between such
nullary links is eliminated, it simply vanishes, leaving the rest of the net
untouched, as in Figure 3, which is obviously an obstacle for our purpose.111
The treatment of weakenings is indeed the main novelty of the present extended
version over our conference paper [CVA18].

In order to deal with nullary links, a well known trick is to attach each
weakening (or $\bot$-link) to another node in the net: switching paths can
then follow such jumps, which is useful to characterize exactly those nets
that come from proof trees [Gir96, Appendix A.2]. Here we will rely on this
structure to control the effect of eliminating evanescent cuts on the size of
a net.

In all our exposition, we adopt a particular presentation of nets: we consider
$n$-ary exponential links rather than separate (co)dereliction and
(co)contraction, as this allows to reduce the dynamics of resource nets to
that of multiplicative linear logic (MLL) proof nets.222 In other words, we
adhere to a version of linear logic proof nets and resource nets which is
sometimes called _nouvelle syntaxe_ , although it dates back to Regnier’s PhD
thesis [Reg92]. For the linear logic _connoisseur_ , this is already apparent
in Figure 1. See also the discussion in our conclusion (Section 8).

###  1.4. Outline

In Section 2, we first introduce MLL proof nets formally, in the term-based
syntax of Ehrhard [Ehr14]. We define the parallel cut elimination relation
$\rightrightarrows$ in this setting, that we decompose into multiplicative
reduction $\rightrightarrows_{m}$, axiom-cut reduction $\rightrightarrows_{a}$
and evanescent reduction $\rightrightarrows_{e}$. We also present the notion
of switching path for this syntax, and introduce the two quantities that will
be our main objects of study in the following:

  * •

the maximum number $\mathbf{jd}(p)$ of $\bot$-links that jump to a common
target;

  * •

the maximum length $\mathbf{ln}(p)$ of any switching path in the net $p$.

Let us mention that typing plays absolutely no role in our approach, so we do
not even consider formulas of linear logic in our exposition: we will rely on
the geometrical structure of nets only.

We show in Section 3 that, if $p\rightrightarrows_{m}q$,
$p\rightrightarrows_{a}q$ or $p\rightrightarrows_{e}q$ then the size of $p$ is
bounded by a function of $\mathbf{ln}(p)$, $\mathbf{jd}(p)$, and the size of
$q$. In order to be able to iterate this combinatorial argument, we must show
that, given bounds for $\mathbf{ln}(p)$ and $\mathbf{jd}(p)$, we can infer
bounds on $\mathbf{ln}(q)$ and $\mathbf{jd}(q)$: this is the subject of
Sections 4 and 5.

Section 4 is dedicated to the proof that we can bound $\mathbf{ln}(q)$ by a
function of $\mathbf{ln}(p)$: the main case is the multiplicative reduction,
as this may create new switching paths in $q$ that we must relate with those
in $p$. In this task, we concentrate on the notion of _slipknot_ : a pair of
residuals of a cut of $p$ occurring in a path of $q$. Slipknots are essential
in understanding how switching paths are structured after cut elimination:
this analysis is motivated by a technical requirement of our approach, but it
can also be considered as a contribution to the theory of MLL nets _per se_.

In Section 5, we show that $\mathbf{jd}(q)$ is bounded by a function of
$\mathbf{ln}(p)$ and $\mathbf{jd}(p)$: the critical case here is that of
chains of jumps between evanescent cuts.

We leverage all of the above results in Section 6, to generalize them to a
reduction $p\rightrightarrows q$, or even an arbitrary sequence of reductions.
In particular, if $p\rightrightarrows q$ then the size of $p$ is bounded by a
function of the size of $q$ and of $\mathbf{ln}(p)$ and $\mathbf{jd}(p)$.
Again, this result is motivated by the study of quantitative semantics, but it
is essentially a theorem about MLL.

We establish the applicability of our approach to the Taylor expansion of MELL
proof nets in Section 7: we show that if $p$ is a resource net of
$\mathcal{T}(P)$, then $\mathbf{ln}(p)$ is bounded by a function of the size
of $P$, and $\mathbf{jd}(p)$ is bounded by the size of $P$.

Finally, we discuss the scope of our results in the concluding Section 8.

##  2\. Definitions

We provide here the minimal definitions necessary for us to work with MLL
proof nets. As stated before, let us stress the fact that the choice of MLL is
not decisive for the development of Sections 2 to 6. The reader can check that
we rely on three ingredients only:

  * •

the definition of switching paths;

  * •

the fact that multiplicative reduction amounts to plug bijectively the
premises of a $\otimes$-link with those of -link (in the nullary case,
evanescent cuts simply vanish);

  * •

the definition of jumps and how they are affected by cut elimination.

The results of those sections are thus directly applicable to resource nets,
thanks to our choice of generalized exponential links: this will be done in
Section 7.

###  2.1. Nets

A proof net is usually presented as a graphical object such as that of Figure
4. Following Ehrhard [Ehr14, Ehr16], we will rely on a term syntax for
denoting such nets. This is based on a quite standard trichotomy: a proof net
can be divided into a top layer of axioms, followed by trees of connectives,
down to cuts between the conclusions of some trees.

$\bot$axcut$\mathbf{1}$$\otimes$ax$\bot$cut$\bot$$\mathbf{1}$cut$\bot$$\mathbf{1}$
Figure 4. An example of multiplicative net

We will represent the conclusions of axiom rules by variables: the duality
between two conclusions of an axiom rule is given by an involution
$x\mapsto\overline{x}$ over the set $\mathbf{V}$ of variables. Our nets will
be finite families of trees and cuts, where trees are inductively generated
from variables by the application of MLL connectives, of arbitrary arity:
$\otimes(t_{1},\dotsc,t_{n})$ and $\invamp(t_{1},\dotsc,t_{n})$. A tree thus
represents a conclusion of a net, together with the nodes above it, up to
axiom conclusions. A cut is then given by the pair of trees $\langle
t_{1}\mathopen{|}t_{2}\rangle$, whose conclusions it cuts together. In order
to distinguish between various occurrences of nullary connectives
$\mathbf{1}=\otimes()$ and $\bot=\invamp()$, we will index them with labels
taken from sets $\mathbf{U}_{\mathbf{1}}$ and $\mathbf{U}_{\bot}$.

Formally, the set of _raw trees_ (denoted by $s$, $t$, _etc._) is generated as
follows:

$t\Coloneqq
x\mid\mathbf{1}_{\lambda}\mid\bot_{\mu}\mid\otimes(t_{1},\dots,t_{n})\mid\invamp(t_{1},\dots,t_{n})$

where $x$ ranges over $\mathbf{V}$, $\lambda$ ranges over
$\mathbf{U}_{\mathbf{1}}$, $\mu$ ranges over $\mathbf{U}_{\bot}$ and we
require $n\not=0$ in the two last cases. We assume $\mathbf{V}$,
$\mathbf{U}_{\mathbf{1}}$ and $\mathbf{U}_{\bot}$ are pairwise disjoint and
all three are denumerably infinite. We will always identify a nullary
connective tree $\mathbf{1}_{\lambda}$ or $\bot_{\mu}$ with its label
$\lambda$ or $\mu$, so that
$\mathbf{A}=\mathbf{V}\cup\mathbf{U}_{\mathbf{1}}\cup\mathbf{U}_{\bot}$ is
just the set of _atomic trees_. We will generally use letters $x$, $y$, $z$
for variables, $\mu$ for the elements of $\mathbf{U}_{\bot}$, $\lambda$ for
the elements of $\mathbf{U}_{\mathbf{1}}$, and $s$, $t$, $u$, $v$ for
arbitrary raw trees.

We write $\mathbf{T}(t)$ for the set of _subtrees_ of a given raw tree $t$,
which is defined inductively in the natural way : if $t\in\mathbf{A}$, then
$\mathbf{T}(t)=\\{t\\}$; if $t=\diamond(t_{1},\dots,t_{n})$ with
$\diamond\in\\{\otimes,\invamp\\}$, then
$\mathbf{T}(t)=\\{t\\}\cup\bigcup_{i\in\\{1,\dots,n\\}}\mathbf{T}(t_{i})$. We
moreover write $\mathbf{V}(t)$ for $\mathbf{T}(t)\cap\mathbf{V}$, and
similarly for $\mathbf{U}_{\mathbf{1}}(t)$, $\mathbf{U}_{\bot}(t)$ and
$\mathbf{A}(t)$. A _tree_ is then a raw tree $t$ such that if
$\diamond(t_{1},\dotsc,t_{n})\in\mathbf{T}(t)$ then the sets
$\mathbf{A}(t_{i})$ for $1\leq i\leq n$ are pairwise disjoint: in other words,
each atom occurs at most once in $t$. As a consequence, each subtree
$u\in\mathbf{T}(t)$ occurs exactly once in a tree $t$.

A cut is an unordered pair $c=\langle t\mathopen{|}s\rangle$ of trees such
that $\mathbf{A}(t)\cap\mathbf{A}(s)=\emptyset$, and then we set
$\mathbf{T}(c)=\mathbf{T}(t)\cup\mathbf{T}(s)$, and similarly for
$\mathbf{V}(c)$, $\mathbf{U}_{\mathbf{1}}(c)$, $\mathbf{U}_{\bot}(c)$ and
$\mathbf{A}(c)$. Note that, in the absence of typing, we do not put any
compatibility requirement on cut trees.

Given a set $A$, we denote by $\overrightarrow{a}$ any finite family
$(a_{i})_{i\in I}\in A^{I}$ of elements of $A$. In general, we abusively
identify $\overrightarrow{a}$ with any enumeration $(a_{1},\dotsc,a_{n})\in
A^{n}$ of its elements, and we may even write
$\overrightarrow{a}=a_{1},\dotsc,a_{n}$ in this case; moreover, we simply
write $\overrightarrow{a},\overrightarrow{b}$ for the concatenation of
families $\overrightarrow{a}$ and $\overrightarrow{b}$ (whose index set is
implicitly the sum of the index sets of $\overrightarrow{a}$ and
$\overrightarrow{b}$). We may also write, e.g., $a_{i}\in\overrightarrow{a}$,
identifying the family $\overrightarrow{a}$ with its support set. Since we
only consider families of pairwise distinct elements, such abuse of notation
is generally harmless: in this case, the only difference between
$(a_{i})_{i\in I}$ and its support set $\\{a_{i}\mid i\in I\\}$ is whether the
bijection $i\mapsto a_{i}$ is part of the data or not. If $f$ is a function
from $A$ to any powerset, we extend it to families in the obvious way, setting
$f(\overrightarrow{a})=\bigcup_{a\in\overrightarrow{a}}f(a)$. E.g., if
$\overrightarrow{\gamma}$ is a family of trees or cuts we write
$\mathbf{V}(\overrightarrow{\gamma})=\bigcup_{\gamma\in\overrightarrow{\gamma}}\mathbf{V}(\gamma)$.

An MLL _bare proof net_ is a pair $p=(\overrightarrow{c};\overrightarrow{t})$
of a finite family $\overrightarrow{c}$ of pairwise distinct cuts and a finite
family $\overrightarrow{t}$ of pairwise distinct trees such that: for all
distinct cuts or trees
$\gamma,\gamma^{\prime}\in\overrightarrow{c}\cup\overrightarrow{t}$,
$\mathbf{A}(\gamma)\cap\mathbf{A}(\gamma^{\prime})=\emptyset$; and
$\mathbf{V}(p)=\mathbf{V}(\overrightarrow{c})\cup\mathbf{V}(\overrightarrow{t})$
is closed under the involution $x\mapsto\overline{x}$. We write
$\mathbf{C}(p)=\overrightarrow{c}$ for the family of cuts of $p$. For any
tree, cut or bare proof net $\gamma$, we define the _size_ of $\gamma$ as
$\mathbf{size}(\gamma)=\\#\mathbf{T}(\gamma)$: graphically, $\mathbf{size}(p)$
is nothing but the number of wires in $p$.

######  Remark 1.

In a graphical structure such as that of Figure 4, the interface (_i.e._ the
set of extremities of dangling wires, which represent the conclusions of the
net) is relevant: in particular, cut elimination preserves this interface. So,
in $p=(\overrightarrow{c};\overrightarrow{t})$, $\overrightarrow{t}$ is
intrinsically a family, whose index set is precisely the interface of the
structure.

On the other hand, the rest of the net should be considered up to isomorphism:
in our case, this amounts to the reindexing of cuts, and the renaming of
atoms, preserving the duality involution on variables. We may call
$\alpha$-equivalence the corresponding equivalence relation on bare proof
nets, as it has the very same status as the renaming of bound variables in the
ordinary $\lambda$-calculus. In particular, $\overrightarrow{c}$ should be
considered as a set, although we introduce it as a family here, just because
it will be convenient to treat the concatenation
$\overrightarrow{c},\overrightarrow{t}$ as a family of cuts and trees in the
following.

The reader may check that bare proof nets quotiented by $\alpha$-equivalence,
as introduced above, are exactly the usual (untyped) proof structures for MLL
(with connectives of arbitrary arity). We keep this quotient implicit whenever
possible in the remaining: in any case, $\alpha$-equivalence preserves the
size of nets, as well as the length of paths to be introduced later.333 Note
that this situation differs slightly from the case of interaction nets
[Laf90], where explicit axioms and cuts links are missing and there is no top-
down orientation _a priori_. Term syntaxes have been proposed for those [MS08,
FM99, among others] but the correspondence is less immediate: it must be
restricted to deadlock-free interaction nets and, in addition to
$\alpha$-equivalence, one must introduce some mechanism to deal with implicit
axiom-cut elimination in the application of reduction rules.

As announced in our introduction, our nets will be equipped with jumps from
$\bot$ nodes to other nodes. An MLL _proof net_ will thus be the data of a
bare proof net $p$ and of a jump function
$\jmath:\mathbf{U}_{\bot}(p)\to\mathbf{T}(p)$. We will often identify a proof
net with its underlying bare net $p$, and then write $\jmath_{p}$ for the
associated jump function. Figure 5 presents such a net, whose underlying
graphical structure is that of Figure 4.

$\bot$$\mu_{1}$ax$x$$\overline{x}$cut$\mathbf{1}$$\lambda_{1}$$\otimes$ax$y$$\overline{y}$$\bot$$\mu_{2}$cut$\bot$$\mu_{3}$$\mathbf{1}$$\lambda_{2}$cut$\bot$$\mu_{4}$$\mathbf{1}$$\lambda_{3}$
Figure 5. The net
$p_{0}=(\langle\invamp(x,\overline{x})\mathopen{|}\otimes(\mathbf{1}_{\lambda_{1}},y)\rangle,\langle\overline{y}\mathopen{|}\bot_{\mu_{3}}\rangle,\langle\mathbf{1}_{\lambda_{2}}\mathopen{|}\bot_{\mu_{4}}\rangle;\bot_{\mu_{1}},\bot_{\mu_{2}},\mathbf{1}_{\lambda_{3}})$
with
$\jmath_{p_{0}}:\mu_{1}\mapsto\invamp(x,\overline{x}),\mu_{2}\mapsto\overline{y},\mu_{3}\mapsto\lambda_{2},\mu_{4}\mapsto\lambda_{3}$.

We can already introduce the first of our two key quantities: the _jump
degree_ $\mathbf{jd}(p)$ of a net $p$. We first define the jump degree of any
tree $t\in\mathbf{T}(p)$, setting
$\mathbf{jd}_{p}(t)=\\#\\{\mu\in\mathbf{U}_{\bot}(p)\mid\jmath_{p}(\mu)=t\\}$.
We will often write $\mathbf{jd}(t)$ instead of $\mathbf{jd}_{p}(t)$ if $p$ is
clear from the context. Then we set $\mathbf{jd}(p)=\max\\{\mathbf{jd}(t)\mid
t\in\mathbf{T}(p)\\}$.

######  Remark 2.

Originally, jumps were introduced as _pis aller_ for the characterization of
sequentializable proof nets [Gir96, Appendix A.2]. Indeed, in presence of
multiplicative units and without jumps, Danos–Regnier’s correctness criterion,
requiring the connectedness and acyclicity of switching graphs, fails to
accept some proof nets corresponding to proof trees using the $\bot$-rule. So,
to characterize all sequentializable nets, one has to require the existence of
a jump function that makes all the switching graphs connected and acyclic.
This additional structure is somewhat arbitrary, and it restores a form of
bureaucratic sequentiality: distinct jumping functions on the same bare net
may yield equivalent sequentializations. And there is no satisfactory solution
to that issue: if a notion of proof net could capture proof equivalence in MLL
with units, then deciding the identity of proof nets in that setting would not
be tractable, simply because proof equivalence is PSPACE-complete [HH16].

A simple, consensual alternative is to forget about jumps and drop the
connectedness requirement: the acyclicity criterion characterizes exactly
those nets that are sequentializable using an additional $mix$-rule,
corresponding to the parallel juxtaposition of nets. In particular, this
weaker requirement is sufficient to avoid the problematic cases of cut
elimination. This is the approach we adopt: after defining switchings and
paths in Subsection 2.3, we will restrict our attention to acyclic nets only.

We associate jump functions with nets nonetheless, but for a different
purpose: bounding the jump degree in a net will allow us to control the
combinatorics of the elimination of evanescent cuts, in situations such as
that of Figure 3. Since switching paths can follow jumps, and those paths will
be our main focus throughout the remaining of the paper, we chose to consider
proof nets as equipped with jumps by default. Still, the reader should be
aware that the main subject of interest is the underlying structure of bare
proof nets.

###  2.2. Cut elimination

A reducible cut is a cut $\langle t\mathopen{|}s\rangle$ such that:

  * •

$t$ is a variable and $\overline{t}\not\in\mathbf{V}(s)$ (_axiom cut_);

  * •

or $t\in\mathbf{U}_{\mathbf{1}}$ and $s\in\mathbf{U}_{\bot}$, and
$\jmath(s)\not\in\\{t,s\\}$ (_evanescent cut_);

  * •

or we can write $t=\otimes(t_{1},\dots,t_{n})$ and
$s=\invamp(s_{1},\dots,s_{n})$ (_multiplicative cut_).

The _substitution_ $\gamma[t/x]$ of a tree $t$ for a variable $x$ in a tree
(or cut, or family of trees and/or cuts) $\gamma$ is defined in the usual way,
with the additional assumption that $\mathbf{A}(t)$ and $\mathbf{A}(\gamma)$
are disjoint. By the definition of trees, this substitution is essentially
linear: each variable $x$ appears at most once in $\gamma$.

There are three basic cut elimination steps defined for bare proof nets, one
for each kind of reducible cut:

  * •

the elimination of a multiplicative cut yields a family of cuts: we write

$\langle\otimes(t_{1},\dots,t_{n})\mathopen{|}\invamp(s_{1},\dots,s_{n})\rangle\to_{m}\langle
t_{1}\mathopen{|}s_{1}\rangle,\dotsc,\langle t_{n}\mathopen{|}s_{n}\rangle$

that we extend to nets by setting
$(c,\overrightarrow{c};\overrightarrow{t})\to_{m}(\overrightarrow{c}^{\prime},\overrightarrow{c};\overrightarrow{t})$
whenever $c\to_{m}\overrightarrow{c}^{\prime}$;

  * •

the elimination of an axiom cut generates a substitution: we write $(\langle
x\mathopen{|}s\rangle,\overrightarrow{c};\overrightarrow{t})\to_{a}(\overrightarrow{c};\overrightarrow{t})[s/\overline{x}]$
whenever $\overline{x}\not\in\mathbf{V}(s)$;

  * •

the elimination of an evanescent cut just deletes that cut: we write
$(\langle\lambda\mathopen{|}\mu\rangle,\overrightarrow{c};\overrightarrow{t})\to_{e}(\overrightarrow{c};\overrightarrow{t})$
whenever $\jmath_{p}(\mu)\not\in\\{\mu,\lambda\\}$.444 Since the cuts of a net
are given as a family rather than a sequence, the order in which we write cuts
in this definition is not relevant: despite our abusive notation, the reduced
cut need not be the first in the enumeration, because this enumeration is not
fixed.

Then we write $p\to p^{\prime}$ if $p\to_{m}p^{\prime}$ or
$p\to_{a}p^{\prime}$ or $p\to_{e}p^{\prime}$. Observe that if $p\to
p^{\prime}$ then $\mathbf{A}(p^{\prime})\subseteq\mathbf{A}(p)$.

In order to define cut elimination between proof nets (and not bare proof nets
only), we need to modify the jump function. Indeed, assume $p=(\langle
t\mathopen{|}s\rangle,\overrightarrow{c};\overrightarrow{t})$ and $p^{\prime}$
is obtained from $p$ by reducing the cut $\langle t\mathopen{|}s\rangle$. Then
$\mathbf{U}_{\bot}(p^{\prime})\subseteq\mathbf{U}_{\bot}(p)$, but if
$\mu\in\mathbf{U}_{\bot}(p^{\prime})$ and $\jmath_{p}(\mu)=t$, we need to
redefine $\jmath_{p^{\prime}}(\mu)$, as in general
$t\not\in\mathbf{T}(p^{\prime})$. This is done as follows:

  * •

if $\langle
t\mathopen{|}s\rangle=\langle\otimes(t_{1},\dots,t_{n})\mathopen{|}\invamp(s_{1},\dots,s_{n})\rangle$
then for all $\mu\in\mathbf{U}_{\bot}(p)=\mathbf{U}_{\bot}(p^{\prime})$ such
that $\jmath_{p}(\mu)=\otimes(t_{1},\dots,t_{n})$ (resp.
$\invamp(s_{1},\dots,s_{n})$), we set $\jmath_{p^{\prime}}(\mu)=t_{1}$ (resp.
$s_{1}$);555 We arbitrarily redirect the jumps to the first subtree to
simplify the presentation, but we could equivalently have set
$\jmath_{p^{\prime}}(\mu)$ to be any of the immediate subtrees of
$\jmath_{p}(\mu)$, non deterministically: in fact, this slight generalization
is necessary to deal with cut elimination in resource nets. Other strategies
for choosing the destination of a jump exist in the literature: for instance,
one may be tempted to systematically redirect jumps to atoms, as it is done by
Tortora de Falco [TdF00, Definition 1.3.3]. But this kind of transformation is
not local and it would certainly complicate our arguments.

  * •

if $\langle t\mathopen{|}s\rangle=\langle t\mathopen{|}x\rangle$ and
$p^{\prime}$ is obtained from $p$ by substituting $t$ for $\overline{x}$, then
for all $\mu\in\mathbf{U}_{\bot}(p)=\mathbf{U}_{\bot}(p^{\prime})$ such that
$\jmath_{p}\in\\{x,\overline{x}\\}$, we set $\jmath_{p^{\prime}}(\mu)=t$;

  * •

if $\langle t\mathopen{|}s\rangle=\langle\mu\mathopen{|}\lambda\rangle$, then
for all
$\mu^{\prime}\in\mathbf{U}_{\bot}(p^{\prime})=\mathbf{U}_{\bot}(p)\setminus\\{\mu\\}$
such that $\jmath_{p}(\mu^{\prime})\in\\{\mu,\lambda\\}$, we set
$\jmath_{p^{\prime}}(\mu^{\prime})=\jmath_{p}(\mu)$.

The result of eliminating the multiplicative cut (resp. axiom cut; evanescent
cut) of the net $p_{0}$ of Figure 5 is depicted in Figure 6 (resp. Figure 7;
Figure 8).

$\bot$$\mu_{1}$ax$x$$\overline{x}$cutcut$\mathbf{1}$$\lambda_{1}$ax$y$$\overline{y}$$\bot$$\mu_{2}$cut$\bot$$\mu_{3}$$\mathbf{1}$$\lambda_{2}$cut$\bot$$\mu_{4}$$\mathbf{1}$$\lambda_{3}$
Figure 6. The net $p^{\prime}_{m}=(\langle
x\mathopen{|}\mathbf{1}_{\lambda_{1}}\rangle,\langle\overline{x}\mathopen{|}y\rangle,\langle\overline{y}\mathopen{|}\bot_{\mu_{3}}\rangle,\langle\mathbf{1}_{\lambda_{2}}\mathopen{|}\bot_{\mu_{4}}\rangle;\bot_{\mu_{1}},\bot_{\mu_{2}},\mathbf{1}_{\lambda_{3}})$
with $\jmath_{p^{\prime}_{m}}:\mu_{1}\mapsto
x,\mu_{2}\mapsto\overline{y},\mu_{3}\mapsto\lambda_{2},\mu_{4}\mapsto\lambda_{3}$,
so that $p_{0}\to_{m}p^{\prime}_{m}$.
$\bot$$\mu_{1}$ax$x$$\overline{x}$cut$\mathbf{1}$$\lambda_{1}$$\otimes$$\bot$$\mu_{2}$$\bot$$\mu_{3}$$\mathbf{1}$$\lambda_{2}$cut$\bot$$\mu_{4}$$\mathbf{1}$$\lambda_{3}$
Figure 7. The net
$p^{\prime}_{a}=(\langle\invamp(x,\overline{x})\mathopen{|}\otimes(\mathbf{1}_{\lambda_{1}},\bot_{\mu_{3}}\rangle,\langle\mathbf{1}_{\lambda_{2}}\mathopen{|}\bot_{\mu_{4}}\rangle;\bot_{\mu_{1}},\bot_{\mu_{2}},\mathbf{1}_{\lambda_{3}})$
with
$\jmath_{p^{\prime}_{a}}:\mu_{1}\mapsto\invamp(x,\overline{x}),\mu_{2}\mapsto\mu_{3},\mu_{3}\mapsto\lambda_{2},\mu_{4}\mapsto\lambda_{3}$,
so that $p_{0}\to_{a}p^{\prime}_{a}$.
$\bot$$\mu_{1}$ax$x$$\overline{x}$cut$\mathbf{1}$$\lambda_{1}$$\otimes$ax$y$$\overline{y}$$\bot$$\mu_{2}$cut$\bot$$\mu_{3}$$\mathbf{1}$$\lambda_{3}$
Figure 8. The net
$p^{\prime}_{e}=(\langle\invamp(x,\overline{x})\mathopen{|}\otimes(\mathbf{1}_{\lambda_{1}},y)\rangle,\langle\overline{y}\mathopen{|}\bot_{\mu_{3}}\rangle;\bot_{\mu_{1}},\bot_{\mu_{2}},\mathbf{1}_{\lambda_{3}})$
with
$\jmath_{p^{\prime}_{e}}:\mu_{1}\mapsto\invamp(x,\overline{x}),\mu_{2}\mapsto\overline{y},\mu_{3}\mapsto\lambda_{3}$,
so that $p_{0}\to_{e}p^{\prime}_{e}$.
$\bot$$\mu_{1}$ax$x$$\overline{x}$cutcut$\mathbf{1}$$\lambda_{1}$$\bot$$\mu_{2}$$\bot$$\mu_{3}$$\mathbf{1}$$\lambda_{3}$
Figure 9. The net $p^{\prime}=(\langle
x\mathopen{|}\mathbf{1}_{\lambda_{1}}\rangle,\langle\overline{x}\mathopen{|}\bot_{\mu_{3}}\rangle;\bot_{\mu_{1}},\bot_{\mu_{2}},\mathbf{1}_{\lambda_{3}})$
with $\jmath_{p^{\prime}}:\mu_{1}\mapsto
x,\mu_{2}\mapsto\mu_{3},\mu_{3}\mapsto\lambda_{3}$, so that
$p_{0}\rightrightarrows p^{\prime}$.

We are in fact interested in the simultaneous elimination of any number of
reducible cuts, that we describe as follows. We write $p\rightrightarrows
p^{\prime}$ if

$p=(c_{1},\dotsc,c_{k},\langle x_{1}\mathopen{|}t_{1}\rangle,\dotsc,\langle
x_{n}\mathopen{|}t_{n}\rangle,\langle\mu_{1}\mathopen{|}\lambda_{1}\rangle,\dots,\langle\mu_{l}\mathopen{|}\lambda_{l}\rangle,\overrightarrow{c};\overrightarrow{t})$

and

$p^{\prime}=(\overrightarrow{c}^{\prime}_{1},\dotsc,\overrightarrow{c}^{\prime}_{k},\overrightarrow{c};\overrightarrow{t})[t_{1}/\overline{x}_{1}]\cdots[t_{n}/\overline{x}_{n}],$

assuming that:

  * •

$c_{i}\to_{m}\overrightarrow{c}^{\prime}_{i}$ for $1\leq i\leq k$,

  * •

$\overline{x}_{i}\not\in\\{x_{1},\dotsc,x_{n}\\}$ and
$\overline{x}_{i}\not\in\mathbf{V}(t_{j})$ for $1\leq i\leq j\leq n$, and

  * •

$\jmath_{p}(\mu_{i})\not\in\\{\mu_{j},\lambda_{j}\\}$ for $1\leq i\leq j\leq
l$.

It should be clear that $p^{\prime}$ is then obtained from $p$ by successively
eliminating the particular cuts we have selected, thus performing $k$ steps of
$\to_{m}$, $n$ steps of $\to_{a}$, $l$ steps of $\to_{e}$, _in no particular
order_ : indeed, one can check that any two elimination steps of distinct cuts
commute on the nose. The resulting jump function $\jmath_{p^{\prime}}$ can be
described directly, by inspecting the possible cases for
$\jmath_{p}(\mu^{\prime})$ with
$\mu^{\prime}\in\mathbf{U}_{\bot}(p^{\prime})$:

  * •

if
$c_{i}=\langle\otimes(u_{1},\dotsc,u_{r})\mathopen{|}\invamp(v_{1},\dotsc,v_{r})\rangle$
and, e.g., $\jmath_{p}(\mu^{\prime})=\otimes(u_{1},\dotsc,u_{r})$ then
$\jmath_{p^{\prime}}(\mu^{\prime})=u_{1}[t_{1}/\overline{x}_{1}]\cdots[t_{n}/\overline{x}_{n}]$;

  * •

if $\jmath_{p}(\mu^{\prime})\in\\{x_{i},\overline{x}_{i}\\}$ then
$\jmath_{p^{\prime}}(\mu^{\prime})=t_{i}[t_{i+1}/\overline{x}_{i+1}]\cdots[t_{n}/\overline{x}_{n}]$;

  * •

if $\jmath_{p}(\mu^{\prime})\in\\{\mu_{i},\lambda_{i}\\}$ then
$\jmath_{p^{\prime}}(\mu^{\prime})=\rho(i)[t_{1}/\overline{x}_{1}]\cdots[t_{n}/\overline{x}_{n}]$,
where $\rho:\\{1,\dotsc,l\\}\to\mathbf{T}(p)$ is the redirection function
inductively defined by $\rho(j)=\rho(i)$ if
$\jmath_{p}(\mu_{j})\in\\{\mu_{i},\lambda_{i}\\}$ (in which case $i<j$) and
$\rho(j)=\jmath_{p}(\mu_{j})$ otherwise;

  * •

otherwise
$\jmath_{p^{\prime}}(\mu^{\prime})=\jmath_{p}(\mu^{\prime})[t_{1}/\overline{x}_{1}]\cdots[t_{n}/\overline{x}_{n}]$.

The result of simultaneously eliminating all the cuts of the net $p_{0}$ of
Figure 5 is depicted in Figure 9.

This general description of parallel cut elimination is obviously not very
handy. In order not to get lost in notation, we will restrict our attention to
the particular case in which only cuts of the same nature are simultaneously
eliminated: we write $p\rightrightarrows_{m}p^{\prime}$ if $n=l=0$
(multiplicative cuts only), $p\rightrightarrows_{a}p$ if $k=l=0$ (axiom cuts
only), and $p\rightrightarrows_{e}p^{\prime}$ if $n=k=0$ (evanescent cuts
only). Then we can decompose any parallel reduction $p\rightrightarrows
p^{\prime}$ into three separate steps: e.g.,
$p\rightrightarrows_{m}\cdot\rightrightarrows_{a}\cdot\rightrightarrows_{e}p^{\prime}$.666
Of course, the converse does not hold: for instance the reductions
$(\langle\invamp(x,\overline{x})\mathopen{|}\otimes(y,z)\rangle;\overline{y},\overline{z})\rightrightarrows_{m}(\langle
x\mathopen{|}y\rangle,\langle\overline{x}\mathopen{|}z\rangle;\overline{y},\overline{z})\rightrightarrows_{a}(\langle
y\mathopen{|}z\rangle;\overline{y},\overline{z})$ cannot be performed in a
single step, as the cut $\langle x\mathopen{|}y\rangle$ was newly created.

###  2.3. Paths

In order to control the effect of parallel reduction on the size of proof
nets, we rely on a side condition involving the length of switching paths,
_i.e._ paths in the sense of Danos–Regnier’s correctness criterion [DR89].

Let us write $\mathbf{T}(p)$ (resp. $\mathbf{T}_{\otimes}(p)$) for the set of
the subtrees of $p$ of the form $\invamp(t_{1},\dotsc,t_{n})$ (resp.
$\otimes(t_{1},\dotsc,t_{n})$). In our setting, a _switching_ of a net $p$ is
a map $I:\mathbf{T}(p)\to\mathbf{T}(p)$ such that, for each
$t=\invamp(t_{1},\dots t_{n})\in\mathbf{T}(p)$,
$I(t)\in\\{t_{1},\dots,t_{n}\\}$. Given a net $p$ and a switching $I$ of $p$,
the associated _switching graph_ is the unoriented graph with vertices in
$\mathbf{T}(p)$ and edges given as follows:

  * •

one _axiom edge_ $\sim_{\\{x,\overline{x}\\}}$ for each axiom
$\\{x,\overline{x}\\}\subseteq\mathbf{V}(p)$, connecting $x$ and
$\overline{x}$;

  * •

one _$\otimes$ -edge_ $\sim_{t,t_{i}}$ for each pair $(t,t_{i})$ with
$t=\otimes(t_{1},\dotsc,t_{n})\in\mathbf{T}_{\otimes}(p)$, connecting $t$ and
$t_{i}$;

  * •

one _-edge_ $\sim_{t}$ for each $t\in\mathbf{T}(p)$, connecting $t$ and
$I(t)$;

  * •

one _jump edge_ $\sim_{\mu}$ for each $\mu\in\mathbf{U}_{\bot}(p)$, connecting
$\mu$ and $\jmath_{p}(\mu)$;

  * •

one _cut edge_ $\sim_{c}$ for each cut $c=\langle
t\mathopen{|}s\rangle\in\mathbf{C}(p)$, connecting $t$ and $s$.

Whenever necessary, we may write, e.g., $\sim_{e}^{p}$ or $\sim_{e}^{p,I}$ for
the edge $\sim_{e}$ to make the underlying net and switching explicit. On the
other hand, we will often simply write $e$ instead of $\sim_{e}$ for denoting
an edge. Each edge $e$ induces a symmetric relation, involving at most two
subtrees of $p$: we write $t\sim_{e}u$, and say $t$ and $u$ are _adjacent_
whenever $t$ and $u$ are connected by $e$. _A priori_ , it might be the case
that distinct edges induce the same relation: for instance, if $c=\langle
x\mathopen{|}\overline{x}\rangle\in\mathbf{C}(p)$, we have
$x\sim_{c}\overline{x}$ as well as $x\sim_{\\{x,\overline{x}\\}}\overline{x}$;
and if $\jmath_{p}(\mu)=\mu^{\prime}$ and $\jmath_{p}(\mu^{\prime})=\mu$, we
have $\mu\sim_{\mu}\mu^{\prime}$ as well as
$\mu\sim_{\mu^{\prime}}\mu^{\prime}$. Avoiding such cycles is precisely the
purpose of the correctness criterion.

Given a switching $I$ in $p$, an _$I$ -path_ is the data of a tree
$t_{0}\in\mathbf{T}(p)$ and of a sequence $(e_{1},\dotsc,e_{n})$ of pairwise
distinct consecutive edges starting from $t_{0}$: in other words, we require
that there exist $t_{1},\dotsc,t_{n}\in\mathbf{T}(p)$ such that, for each
$i\in\\{1,\dots,n\\}$, $t_{i-1}\sim_{e_{i}}t_{i}$.777 In standard terminology
of graph theory, an $I$-path in $p$ is a trail in the switching graph induced
by $p$ and $I$.  For instance, if
$p=(;\otimes(x,y),\invamp(\overline{y},\overline{x}))$ and
$I(\invamp(\overline{y},\overline{x}))=\overline{x}$, then the chain of
adjacencies
$\invamp(\overline{x},\overline{y})\sim_{\invamp(\overline{x},\overline{y})}\overline{x}\sim_{\\{x,\overline{x}\\}}x\sim_{\otimes(x,y),x}\otimes(x,y)\sim_{\otimes(x,y),y}y\sim_{\\{y,\overline{y}\\}}\overline{y}$
defines a maximal $I$-path in $p$ (see Figure 10).

$\otimes$axax$x$$\overline{x}$$y$$\mid$$\overline{y}$ Figure 10. A path in
$(;\otimes(x,y),\invamp(\overline{y},\overline{x}))$ for switching
$I:\invamp(\overline{y},\overline{x})\mapsto\overline{x}$ (we strike out the
other premise).

We write $\mathbf{P}(p,I)$ for the set of all $I$-paths in $p$. We write
$\chi:t_{0}\leadsto_{p,I}t_{n}$ whenever
$\chi=t_{0}\sim_{e_{1}}\cdots\sim_{e_{n}}t_{n}$ is an $I$-path from $t_{0}$ to
$t_{n}$ in $p$: with these notations, we say $\chi$ _visits_ the trees
$t_{0},\dotsc,t_{n}$, and $\chi$ _crosses_ the edges $e_{1},\dotsc,e_{n}$;
moreover we write $\mathbf{ln}(\chi)=n$ for the length of $\chi$. A _subpath_
of $\chi$ is any $I$-path of the form
$t_{i}\sim_{e_{i+1}}\cdots\sim_{e_{i+k}}t_{i+k}$. We write $\chi^{\dagger}$
for the reverse $I$-path:
$\chi^{\dagger}=t_{n}\sim_{e_{n}}\cdots\sim_{e_{0}}t_{0}$. The _empty path_
from $t\in\mathbf{T}(p)$ is the only $\epsilon_{t}:t\leadsto_{p,I}t$ of length
$0$. We say $I$-paths $\chi$ and $\chi^{\prime}$ are _disjoint_ if no edge is
crossed by both $\chi$ and $\chi^{\prime}$. Observe that disjoint paths can
visit common trees: in particular, if $\chi:t\leadsto_{p,I}s$ and
$\chi^{\prime}:s\leadsto_{p,I}u$ are disjoint, we write
$\chi\chi^{\prime}:t\leadsto_{p,I}u$ for the concatenation of $\chi$ and
$\chi^{\prime}$.

We call _path_ in $p$ any $I$-path for $I$ a switching of $p$, we write
$\mathbf{P}(p)$ for the set of all paths in $p$, and we denote by
$\mathbf{ln}(p)=\max\\{\mathbf{ln}(\chi)\mid\chi\in\mathbf{P}(p)\\}$ the
maximal length of a path in $p$. We then write $\chi:t\leadsto_{p}s$ if
$\chi\in\mathbf{P}(p)$ is a path from $t$ to $s$ in $p$, and we write
$t\leadsto_{p}s$, or simply $t\leadsto s$, whenever such a path exists. This
relation on $\mathbf{T}(p)$ is reflexive (_via_ the empty path
$\epsilon_{t}:t\leadsto t$) and symmetric (_via_ reversing paths). Observe
that if $\chi_{1},\cdots,\chi_{n}\in\mathbf{P}(p)$ are pairwise disjoint, then
there exists $I$ such that $\chi_{i}\in\mathbf{P}(p,I)$ for $1\leq i\leq n$.
This does not make the relation $\leadsto_{p}$ transitive: for instance, if
$p=(;x,\invamp(\overline{x},\overline{y}),y)$, we have paths
$x\leadsto\invamp(\overline{x},\overline{y})$ and
$\invamp(\overline{x},\overline{y})\leadsto y$, but both cross
$\invamp(\overline{x},\overline{y})$ for different switchings, and indeed,
there is no path $x\leadsto y$.

We say a net $p$ is _acyclic_ if, for all $\chi\in\mathbf{P}(p)$ and
$t\in\mathbf{T}(p)$, $\chi$ visits $t$ at most once: in other words, there is
no (non-empty) _cycle_ $\chi:t\leadsto t$. Notice that, given any family of
pairwise distinct cuts in an acyclic net $p$, it is always possible to satisfy
the side conditions on free variables and on jumps necessary to reduce these
cuts in parallel (provided each cut in the family has the shape of a
multiplicative, axiom or evanescent cut). Moreover, it is a very standard
result that acyclicity is preserved by cut elimination:

######  Lemma 3.

If $p^{\prime}$ is obtained from $p$ by cut elimination and $p$ is acyclic
then so is $p^{\prime}$.

######  Proof 2.1.

It suffices to check that if $p\to p^{\prime}$ then any cycle in $p^{\prime}$
induces a cycle in $p$.888 We do not detail the proof as it is quite standard.
We will moreover generalize this technique to all paths (and not only cycles)
in the next section.

From now on, we consider acyclic nets only.

##  3\. Bounding the size of antireducts: three kinds of cuts

In this section, we show that the loss of size during a parallel reduction
$p\rightrightarrows_{m}q$, $p\rightrightarrows_{a}q$ or
$p\rightrightarrows_{e}q$ is directly controlled by $\mathbf{ln}(p)$,
$\mathbf{jd}(p)$ and $\mathbf{size}(q)$: more precisely, we show that the
ratio $\frac{\mathbf{size}(p)}{\mathbf{size}(q)}$ is bounded by a function of
$\mathbf{ln}(p)$ and $\mathbf{jd}(p)$ in each case.

###  3.1. Elimination of multiplicative cuts

The elimination of multiplicative cuts cannot decrease the size by more than a
half:

######  Lemma 4.

If $p\rightrightarrows_{m}q$ then $\mathbf{size}(p)\leq 2\mathbf{size}(q)$.

######  Proof 3.1.

Since the elimination of a multiplicative cut does not affect the rest of the
(bare) net, it is sufficient to observe that if $c\to_{m}\overrightarrow{c}$
then $\mathbf{size}(c)=2+\mathbf{size}(\overrightarrow{c})\leq
2\mathbf{size}(\overrightarrow{c})$.999 This is due to the fact that we
distinguish between strict connectives and their nullary versions, that are
subject to evanescent reductions.

So in this case, $\mathbf{ln}(p)$ and $\mathbf{jd}(p)$ actually play no rôle.

###  3.2. Elimination of axiom cuts

Observe that:

  * •

if $x\in\mathbf{V}(\gamma)$ then
$\mathbf{size}(\gamma[t/x])=\mathbf{size}(\gamma)+\mathbf{size}(t)-1$;

  * •

if $x\not\in\mathbf{V}(\gamma)$ then
$\mathbf{size}(\gamma[t/x])=\mathbf{size}(\gamma)$.

It follows that, in the elimination of a single axiom cut $p\to_{a}q$, we have
$\mathbf{size}(p)=\mathbf{size}(q)+2$. But we cannot reproduce the proof of
Lemma 4 for $\rightrightarrows_{a}$: as depicted in Figure 2, a chain of
arbitrarily many axiom cuts may reduce into a single wire. We can bound the
length of those chains by $\mathbf{ln}(p)$, however, and this allows us to
bound the loss of size during reduction.

######  Lemma 5.

If $p\rightrightarrows_{a}q$ then
$\mathbf{size}(p)\leq(\mathbf{ln}(p)+1)\mathbf{size}(q)$.

######  Proof 3.2.

Assume $p=(\langle x_{1}\mathopen{|}t_{1}\rangle,\dotsc,\langle
x_{n}\mathopen{|}t_{n}\rangle,\overrightarrow{c};\overrightarrow{s})$ and
$q=(\overrightarrow{c};\overrightarrow{s})[t_{1}/\overline{x}_{1}]\cdots[t_{n}/\overline{x}_{n}]$
with $\overline{x}_{i}\not\in\\{x_{1},\dotsc,x_{n}\\}$ and
$\overline{x}_{i}\not\in\mathbf{V}(t_{j})$ for $1\leq i\leq j\leq n$. To
establish the result in this case, we make the chains of eliminated axiom cuts
explicit.

Due to the condition on free variables, we can partition $\langle
x_{1}\mathopen{|}t_{1}\rangle,\dotsc,\langle x_{n}\mathopen{|}t_{n}\rangle$
into tuples $\overrightarrow{c}_{1},\dotsc,\overrightarrow{c}_{k}$ of the
shape $\overrightarrow{c}_{i}=(\langle
x^{i}_{0}\mathopen{|}\overline{x}^{i}_{1}\rangle,\dotsc,\langle
x^{i}_{n_{i}-1}\mathopen{|}\overline{x}^{i}_{n_{i}}\rangle,\langle
x^{i}_{n_{i}}\mathopen{|}t^{i}\rangle)$ so that:

  * •

$x_{j}^{i}\in\\{x_{1},\dotsc,x_{n}\\}$ for $1\leq i\leq k$ and $0\leq j\leq
n_{i}$;

  * •

$\overline{x}_{j}^{i}\in\\{t_{1},\dotsc,t_{n}\\}$ for $1\leq i\leq k$ and
$1\leq j\leq n_{i}$;

  * •

$t^{i}\in\\{t_{1},\dotsc,t_{n}\\}$ for $1\leq i\leq k$;

  * •

each $\overrightarrow{c}_{i}$ is maximal with this shape, _i.e._
$\overline{x}^{i}_{0}\not\in\\{t_{1},\dotsc,t_{n}\\}$ and
$t^{i}\not\in\\{\overline{x}_{1},\dotsc,\overline{x}_{n}\\}$.

Without loss of generality, we can moreover require that, if $i<i^{\prime}$,
then $\langle x^{i}_{n_{i}}\mathopen{|}t^{i}\rangle$ occurs before $\langle
x^{i^{\prime}}_{n_{i^{\prime}}}\mathopen{|}t^{i^{\prime}}\rangle$ in the tuple
$(\langle x_{1}\mathopen{|}t_{1}\rangle,\dotsc,\langle
x_{n}\mathopen{|}t_{n}\rangle)$. Moreover observe that, by the condition on
free variables, the order of the cuts in each $\overrightarrow{c}_{i}$ is
necessarily the same as in $(\langle
x_{1}\mathopen{|}t_{1}\rangle,\dotsc,\langle x_{n}\mathopen{|}t_{n}\rangle)$.

By a standard result on substitutions, if $x\not=y$, $x\not\in\mathbf{V}(v)$
and $y\not\in\mathbf{V}(u)$ then $\gamma[u/x][v/y]=\gamma[v/y][u/x]$:

  * •

if $i\not=i^{\prime}$, we have
$\overline{x}^{i}_{j}\not=\overline{x}^{i^{\prime}}_{j^{\prime}}$ for $0\leq
j\leq n_{i}$ and $0\leq j^{\prime}\leq n_{i^{\prime}}$, so the substitutions
$[\overline{x}^{i}_{j+1}/\overline{x}^{i}_{j}]$ and
$[\overline{x}^{i^{\prime}}_{j^{\prime}+1}/\overline{x}^{i^{\prime}}_{j^{\prime}}]$
always commute for $1\leq i<i^{\prime}\leq k$, $0\leq j<n_{i}$ and $0\leq
j^{\prime}<n_{j^{\prime}}$;

  * •

if $i<i^{\prime}$ and $\langle
x^{i^{\prime}}_{j^{\prime}}\mathopen{|}\overline{x}^{i^{\prime}}_{j^{\prime}+1}\rangle$
occurs before $\langle x^{i}_{n_{i}}\mathopen{|}t^{i}\rangle$ in $(\langle
x_{1}\mathopen{|}t_{1}\rangle,\dotsc,\langle x_{n}\mathopen{|}t_{n}\rangle)$,
the condition on free variables imposes that
$\overline{x}^{i^{\prime}}_{j^{\prime}}\not\in\mathbf{V}(t^{i})$ so the
substitutions $[t^{i}/\overline{x}^{i}_{n_{i}}]$ and
$[\overline{x}^{i^{\prime}}_{j^{\prime}+1}/\overline{x}^{i^{\prime}}_{j^{\prime}}]$
commute in this case.

By iterating those two observations, we can reorder the substitutions in $q$
and obtain:

$\displaystyle q$
$\displaystyle=(\overrightarrow{c};\overrightarrow{s})[t_{1}/\overline{x}_{1}]\cdots[t_{n}/\overline{x}_{n}]$
$\displaystyle=(\overrightarrow{c};\overrightarrow{s})[\overline{x}^{1}_{1}/\overline{x}^{1}_{0}]\cdots[\overline{x}^{1}_{n_{1}}/\overline{x}^{1}_{n_{1}-1}][t^{1}/\overline{x}^{1}_{n_{1}}]\cdots[\overline{x}^{k}_{1}/\overline{x}^{k}_{0}]\cdots[\overline{x}^{k}_{n_{k}}/\overline{x}^{k}_{n_{k}-1}][t^{k}/\overline{x}^{k}_{n_{k}}]$
$\displaystyle=(\overrightarrow{c};\overrightarrow{s})[t^{1}/\overline{x}^{1}_{0}]\cdots[t^{k}/\overline{x}^{k}_{0}].$

It follows that
$\mathbf{size}(q)=\mathbf{size}(\overrightarrow{c})+\mathbf{size}(\overrightarrow{s})+\sum_{i=1}^{k}\mathbf{size}(t^{i})-k$.
For $1\leq i\leq k$, $\overrightarrow{c}_{i}$ induces a path
$\overline{x}^{0}_{i}\leadsto t^{i}$ of length $2n_{i}+2$ ($n_{i}+1$ cuts and
$n_{i}+1$ axioms). Hence $2n_{i}\leq\mathbf{ln}(p)-2$ and:

$\displaystyle\mathbf{size}(p)$
$\displaystyle=\mathbf{size}(\overrightarrow{c})+\mathbf{size}(\overrightarrow{s})+\sum_{i=1}^{k}(\mathbf{size}(t^{i})+2n_{i}+1)$
$\displaystyle\leq\mathbf{size}(\overrightarrow{c})+\mathbf{size}(\overrightarrow{s})+\sum_{i=1}^{k}\mathbf{size}(t^{i})+k(\mathbf{ln}(p)-1)$
$\displaystyle\leq\mathbf{size}(q)+k\mathbf{ln}(p).$

To conclude, it will be sufficient to prove that $\mathbf{size}(q)\geq k$. For
$1\leq i\leq k$, let
$A_{i}=\\{j>i\mid\overline{x}^{j}_{0}\in\mathbf{V}(t^{i})\\}$, and then let
$A_{0}=\\{i\mid\overline{x}^{i}_{0}\in\mathbf{V}(\overrightarrow{c},\overrightarrow{s})\\}$.
It follows from the construction that $\\{A_{0},\dotsc,A_{k-1}\\}$ is a
partition (possibly including empty sets) of $\\{1,\dotsc,k\\}$. By
construction, for each $j\in A_{i}$, $\overline{x}^{j}_{0}$ is a strict
subtree of $t^{i}$: it follows that $\mathbf{size}(t^{i})>\\#A_{i}$. Now
consider
$q_{i}=(\overrightarrow{c};\overrightarrow{s})[t^{1}/\overline{x}^{1}_{0}]\cdots[t^{i}/\overline{x}^{i}_{0}]$
for $0\leq i\leq k$ so that $q=q_{k}$. For $1\leq i\leq k$, we obtain
$\mathbf{size}(q_{i})=\mathbf{size}(q_{i-1})+\mathbf{size}(t^{i})-1\geq\mathbf{size}(q_{i-1})+\\#A_{i}$.
Also observe that
$\mathbf{size}(q_{0})=\mathbf{size}(\overrightarrow{c};\overrightarrow{s})\geq\\#A_{0}$.
Then we can conclude:
$\mathbf{size}(q)=\mathbf{size}(q_{k})\geq\sum_{i=0}^{k}\\#A_{i}=k$.

###  3.3. Elimination of evanescent cuts

We now consider the case of a reduction $p\rightrightarrows_{e}q$: we bound
the maximal number of evanescent cuts appearing in $p$ by a function of
$\mathbf{ln}(p)$, $\mathbf{jd}(p)$ and $\mathbf{size}(q)$.

We rely on the basic fact that if $t\in\mathbf{T}(q)\subseteq\mathbf{T}(p)$,
then there are at most $\mathbf{jd}(p)$ evanescent cuts of $p$ that jump to
$t$. The main difficulty is that an evanescent cut of $p$ can jump to another
evanescent cut of $p$, that is also eliminated in the step
$p\rightrightarrows_{e}q$. See Figure 11 for a graphical representation of the
critical case. To deal with this phenomenon, we observe that a sequence of
cuts
$\langle\mu_{1}\mathopen{|}\lambda_{1}\rangle,\dots,\langle\mu_{n}\mathopen{|}\lambda_{n}\rangle$
with $\jmath_{p}(\mu_{i})\in\\{\lambda_{i+1},\mu_{i+1}\\}$ for all
$i\in\\{1,\dots,n-1\\}$, induces a path of length at least $n$: hence
$n\leq\mathbf{ln}(p)$. We define for all $n\in\mathbf{N}$ and all
$t\in\mathbf{T}(p)$, $\mathbf{I}^{n}(t)$ as follows :
$\mathbf{I}^{0}(t)=\jmath_{p}^{-1}(t)=\\{\mu\in\mathbf{U}_{\bot}(p)\mid\jmath_{p}(\mu)=t\\}$,
and
$\mathbf{I}^{m+1}(t)=\\{\mu^{\prime}\in\mathbf{U}_{\bot}(p)\mid\jmath_{p}(\mu^{\prime})\in\\{\mu,\lambda\\},\langle\mu\mathopen{|}\lambda\rangle\in\mathbf{C}(p),\mu\in\mathbf{I}^{m}(t)\\}$.
We can already observe that $\\#\mathbf{I}^{0}(t)=\mathbf{jd}(t)$. This
definition is parametrized by $\jmath_{p}$, and may we write
$\mathbf{I}^{n}_{p}(t)$ to make the underlying net explicit.

$t$$\bot$$\bot$$1$$1$ . . . $\leq\mathbf{jd}(p)$$1$$1$$\bot$$\bot$ . . .
$1$$1$$\bot$$\bot$ . . . . . . $\leq 2\mathbf{jd}(p)$$\leq
2\mathbf{jd}(p)$$1$$\bot$$1$$\bot$$\dots$$\dots$$\vdots$$\bot$$\bot$$\vdots$$\bot$$\bot$$\vdots$$\vdots$$\leq\left(2\mathbf{jd}(p)\right)^{n+1}$$\mathbf{I}^{0}(t)$$\mathbf{I}^{1}(t)$$\mathbf{I}^{n-1}(t)$$\mathbf{I}^{n}(t)$$n\leq\mathbf{ln}(p)$
Figure 11. Evanescent reductions : critical case

######  Lemma 6.

Let $p,q$ be two nets such that $p\rightrightarrows_{e}q$. Then:

  1. (1)

for all $t\in\mathbf{T}(p)$,
$\\#\left(\bigcup_{i\in\mathbf{N}}\mathbf{I}_{p}^{i}(t)\right)\leq(2\mathbf{jd}(p))^{\mathbf{ln}(p)+1}$;

  2. (2)

there are at most $\mathbf{size}(q)\times(2\mathbf{jd}(p))^{\mathbf{ln}(p)+1}$
evanescent cuts in $\mathbf{C}(p)$.

######  Proof 3.3.

We first establish that the set
$\\{n\in\mathbf{N}\mid\mathbf{I}^{n}(t)\neq\emptyset\\}$ is finite for all
$t$. Indeed, for each $\mu_{n}\in\mathbf{I}^{n}(t)$, there is a sequence of
cuts $c_{0},\dotsc,c_{n-1}$ such that, writing
$c_{i}=\langle\lambda_{i}\mathopen{|}\mu_{i}\rangle$, the unique path from
$\mu_{n}$ to $t$ is $\chi=\chi_{n}\cdots\chi_{1}(\mu_{0}\sim_{\mu_{0}}t)$
where, for $1\leq i\leq n$:

  * •

either $\jmath_{p}(\mu_{i})=\lambda_{i-1}$ and
$\chi_{i}=\mu_{i}\sim_{\mu_{i}}\lambda_{i-1}\sim_{c_{i-1}}\mu_{i-1}$;

  * •

or $\jmath_{p}(\mu_{i})=\mu_{i-1}$ and
$\chi_{i}=\mu_{i}\sim_{\mu_{i}}\mu_{i-1}$.

We observe that $\mathbf{ln}(\chi)\geq n+1$, and then we deduce
$n<\mathbf{ln}(p)$ as soon as $\mathbf{I}^{n}(t)\neq\emptyset$.

Now we bound the size of each $\mathbf{I}_{p}^{n}(t)$: we show that
$\\#\mathbf{I}_{p}^{n}(t)\leq(2\mathbf{jd}(p))^{n+1}$, by induction on $n$. We
already have $\\#\mathbf{I}_{p}^{0}(t)=\mathbf{jd}(t)\leq\mathbf{jd}(p)$. Now
assume the result holds for $n\geq 0$. Then, for each
$c=\langle\mu\mathopen{|}\lambda\rangle\in\mathbf{C}(p)$ such that
$\mu\in\mathbf{I}_{p}^{n}(t)$, the number of $\mu^{\prime}$ such that
$\jmath_{p}(\mu^{\prime})\in c$ is at most
$\mathbf{jd}(\mu)+\mathbf{jd}(\lambda)\leq 2\mathbf{jd}(p)$. We obtain:
$\\#\mathbf{I}_{p}^{n+1}(t)\leq 2\mathbf{jd}(p)\\#\mathbf{I}_{p}^{n}$, which
enables the induction.

We thus get
$\\#\left(\bigcup_{i\in\mathbf{N}}\mathbf{I}_{p}^{i}(t)\right)\leq\sum_{i=0}^{\mathbf{ln}(p)-1}(2\mathbf{jd}(p))^{i+1}\leq(2\mathbf{jd}(p))^{\mathbf{ln}(p)+1}$
which entails (1). To deduce (2) from (1), it will be sufficient to show that,
for each $\mu\in\mathbf{U}_{\bot}(p)$, there exists $t\in\mathbf{T}(q)$ such
that $\mu\in\mathbf{I}_{p}^{k}(t)$ for some $k\in\mathbf{N}$: indeed the
number of evanescent cuts in $p$ is obviously bounded by
$\\#\mathbf{U}_{\bot}(p)$.

For that purpose, write $\mu_{0}=\mu$ and let $(c_{i})_{i\in\\{1,\dots,k\\}}$
be the longest sequence of cuts
$c_{i}=\langle\lambda_{i}\mathopen{|}\mu_{i}\rangle\in\mathbf{C}(p)$ such
that, for all $i\in\\{0,\dots,k-1\\}$,
$\jmath_{p}(\mu_{i})\in\\{\mu_{i+1},\lambda_{i+1}\\}$: such a maximal sequence
exists by acyclicity. Necessarily, $\jmath_{p}(\mu_{k})$ is not part of an
evanescent cut in $\mathbf{C}(p)$, so $\jmath_{p}(\mu_{k})\in\mathbf{T}(q)$:
we conclude since $\mu_{0}\in\mathbf{I}_{p}^{k}(\jmath_{p}(\mu_{k}))$.

Writing $\psi(i,j,k)=i(1+2(2j)^{k+1})$, we obtain:

######  Lemma 7.

If $p\rightrightarrows_{e}q$, then
$\mathbf{size}(p)\leq\psi(\mathbf{size}(q),\mathbf{jd}(p),\mathbf{ln}(p))$.

######  Proof 3.4.

Writing
$p=(\langle\mu_{1}\mathopen{|}\lambda_{1}\rangle,\dots,\langle\mu_{n}\mathopen{|}\lambda_{n}\rangle,\overrightarrow{c};\overrightarrow{t})$
and $q=(\overrightarrow{c};\overrightarrow{t})$, we obtain

$\mathbf{size}(p)=\mathbf{size}(q)+2n\leq\mathbf{size}(q)(1+2(2\mathbf{jd}(p))^{\mathbf{ln}(p)+1})$

by Lemma 6.

###  3.4. Towards the general case

Recall that any parallel cut elimination step $p\rightrightarrows q$ can be
decomposed into, e.g.:
$p\rightrightarrows_{e}p^{\prime}\rightrightarrows_{m}p^{\prime\prime}\rightrightarrows_{a}q$.
We would like to apply the previous results to this sequence of reductions, in
order to bound the size of $p$ by a function of $\mathbf{size}(q)$,
$\mathbf{ln}(p)$ and $\mathbf{jd}(p)$. Observe however that this would require
us to infer a bound on $\mathbf{ln}(p^{\prime\prime})$ from the bounds on $p$,
in order to apply Lemma 5.

More generally, to be able to apply our results to a sequence of reductions
$p\rightrightarrows\cdots\rightrightarrows q$, we need to ensure that for any
reduction $p\rightrightarrows p^{\prime}$, we can bound
$\mathbf{ln}(p^{\prime})$ and $\mathbf{jd}(p^{\prime})$ by functions of
$\mathbf{ln}(p)$ and $\mathbf{jd}(p)$. This is the subject of the following
two sections.

##  4\. Variations of $\mathbf{ln}(p)$ under reduction

Here we establish that the possible increase of $\mathbf{ln}(p)$ under
reduction is bounded. It should be clear that:

######  Lemma 8.

If $p\rightrightarrows_{a}q$ or $p\rightrightarrows_{e}q$, then
$\mathbf{ln}(q)\leq\mathbf{ln}(p)$.

Indeed axiom and evanescent reductions only shorten paths, without really
changing the topology of the net.

In the case of multiplicative cuts however, cuts are duplicated and new paths
are created. Consider for instance a net $r$, as in Figure 12, obtained from
three nets $p_{1}$, $p_{2}$ and $q$, by forming the cut
$\langle\otimes(t_{1},t_{2})\mathopen{|}\invamp(s_{1},s_{2})\rangle$ where
$t_{1}\in\mathbf{T}(p_{1})$, $t_{2}\in\mathbf{T}(p_{2})$ and
$s_{1},s_{2}\in\mathbf{T}(q)$. Observe that, in the reduct $r^{\prime}$
obtained by forming two cuts $\langle t_{1}\mathopen{|}s_{1}\rangle$ and
$\langle t_{2}\mathopen{|}s_{2}\rangle$, we may very well form a path that
travels from $p_{1}$ to $q$ then $p_{2}$; while in $p$, this is forbidden by
any switching of $\invamp(s_{1},s_{2})$. For instance, if we consider
$I(\invamp(s_{1},s_{2}))=s_{1}$, we may only form a path between $p_{1}$ and
$p_{2}$ through $\otimes(t_{1},t_{2})$, or a path between $q$ and one of the
$p_{i}$’s, through $s_{1}$ and the cut.

$p_{1}$$p_{2}$$\otimes$$q$$\mid$cut

$p_{1}$$p_{2}$cutcut$q$

Figure 12. A cut, the resulting slipknot, and examples of paths before and
after reduction

In the remainder of this section, we fix a reduction step
$p\rightrightarrows_{m}q$, and we show that the previous example describes a
general mechanism: a path $\chi$ in $q$ that is not already in $p$ must
involve a subpath $\chi^{\prime}$ between two residuals of a cut of $p$ that
was eliminated in $p\rightrightarrows_{m}q$. We refer to this situation as a
_slipknot_ in $\chi$.

More formally, consider $c=\langle
t_{0}\mathopen{|}s_{0}\rangle\in\mathbf{C}(p)$ with
$t_{0}=\otimes(t_{1},\dotsc,t_{n})$ and $s_{0}=\invamp(s_{1},\dotsc,s_{n})$
and assume $c$ is eliminated in the reduction $p\rightrightarrows_{m}q$: then
the _residuals_ of $c$ in $q$ are the cuts $\langle
t_{i}\mathopen{|}s_{i}\rangle\in\mathbf{C}(q)$ for $1\leq i\leq n$. For any
edge $e$, we write $(e)$ for any length 1 path $t\sim_{e}s$. If
$\chi\in\mathbf{P}(q)$, a _slipknot_ of $\chi$ is any subpath
$(d)\xi(d^{\prime})$ where $d$ and $d^{\prime}$ are (necessarily distinct)
residuals of the same cut in $p$. In the remaining of this section, we show
that a path in $q$ is necessarily obtained by alternating paths (essentially)
in $p$ and slipknots in $q$, that recursively consist of such alternations.
This will allow us to bound $\mathbf{ln}(q)$ depending on $\mathbf{ln}(p)$, by
reasoning inductively on these paths.

###  4.1. Preserved paths

Notice that $\mathbf{T}(q)\subseteq\mathbf{T}(p)$ and, given a switching $J$
of $q$, it is always possible to extend $J$ into a switching $I$ of $p$: to
determine $I$ uniquely amounts to select a premise for each -tree in an
eliminated cut.

Let $J$ be a switching of $q$ and $I$ an extension of $J$ on $p$. Observe that
if $t\sim^{p,I}_{e}t^{\prime}$ and neither $t$ nor $t^{\prime}$ is an element
of an eliminated cut, then $e$ is also an edge of $q$ that is not a residual
cut; conversely, if $t\sim^{q,J}_{e}t^{\prime}$ and $e$ is not a residual cut,
then $e$ is also an edge of $p$. We then say the edge $e$ is _preserved_ by
the reduction $p\rightrightarrows_{m}q$. If a preserved edge $e$ is a cut, an
axiom, a $\otimes$-edge or a -edge, then $e$ has the same endpoints in $p$ and
in $q$: $t\sim^{p,I}_{e}t^{\prime}$ iff $t\sim^{q,J}_{e}t^{\prime}$. If
$e=\mu$ is a jump, one endpoint might be changed: indeed,
$\mu\sim^{p}_{e}\jmath_{p}(\mu)$ and $\mu\sim^{q}_{e}\jmath_{q}(\mu)$, and we
might have $\jmath_{p}(\mu)\not=\jmath_{q}(\mu)$ when $\jmath_{p}(\mu)$ is
part of an eliminated cut. In this case, we say $e$ is a _redirected jump_. We
say $u\in\mathbf{T}(p)$ is an _anchor_ of $v\in\mathbf{T}(q)$, if either $u=v$
or $u$ is involved in an eliminated cut $c=\langle
u\mathopen{|}u^{\prime}\rangle$, and either $u=\otimes(\overrightarrow{t})$
and $v\in\overrightarrow{t}$ or $u=\invamp(\overrightarrow{s})$ and
$v\in\overrightarrow{s}$.

######  Lemma 9.

Assume $(d)\chi(d^{\prime})\in\mathbf{P}(q)$ and $d$ and $d^{\prime}$ are
residuals. Then $\chi$ is non empty, and its first and last edges are
preserved.

######  Proof 4.1.

This is a direct consequence of the fact that if $(c)(e)$ is a path and $c$ is
a cut then $e$ is not a cut.

Observe that even if a path $\chi\in\mathbf{P}(q)$ crosses preserved edges
only, it is not sufficient to have $\chi\in\mathbf{P}(p)$, because the
endpoints of redirected jumps might change. We say $\chi$ is a _preserved
path_ if $\chi$ crosses preserved edges only, and we can write either
$\chi=\chi^{\prime}$ or $\chi=(t\sim_{\mu}\bot_{\mu})\chi^{\prime}$ or
$\chi^{\prime}(\bot_{\mu^{\prime}}\sim_{\mu^{\prime}}t^{\prime})$ or
$\chi=(t\sim_{\mu}\bot_{\mu})\chi^{\prime}(\bot_{\mu^{\prime}}\sim_{\mu^{\prime}}t^{\prime})$
where $\chi^{\prime}$ crosses no redirected jump.

######  Lemma 10.

Any non empty preserved path $\chi:t\leadsto_{q}t^{\prime}$ induces a unique
preserved path $\chi^{-}:s\leadsto_{p}s^{\prime}$ with the same sequence of
edges: in particular, $\chi^{-}\in\mathbf{P}(p,I)$ as soon as
$\chi\in\mathbf{P}(q,J)$ and $I$ is an extension of $J$; and $s$ (resp.
$s^{\prime}$) is an anchor of $t$ (resp. $t^{\prime}$’). Moreover, if
$\chi_{1}\chi_{2}$ is a preserved path then
$(\chi_{1}\chi_{2})^{-}=\chi^{-}_{1}\chi^{-}_{2}\in\mathbf{P}(p)$.

######  Proof 4.2.

The first part is a direct consequence of the definition. If moreover
$\chi_{1}\chi_{2}$ is a preserved path, and neither $\chi_{1}$ nor $\chi_{2}$
is an empty path, then neither the last edge of $\chi_{1}$ nor the first edge
of $\chi_{2}$ can be a redirected jump.

By convention, if $\chi$ is empty, we set $\chi^{-}=\chi$. We say $\chi^{-}$
is the path of $p$ _generated by_ $\chi$. In the next two subsections, we
extend the generation of paths in $p$ from paths in $q$, first to paths
without slipknots, then to arbitrary paths.

###  4.2. Bridges and straight paths

Let $c=\langle t_{0}\mathopen{|}s_{0}\rangle\in\mathbf{C}(p)$ with
$t_{0}=\otimes(\overrightarrow{t})$ and $s_{0}=\invamp(\overrightarrow{s})$.
We say an edge $e$ is _bound to $c$_ if either $e=c$, or $e=(t_{0},t)$ with
$t\in\overrightarrow{t}$, or $e=s_{0}$. And we say $\chi\in\mathbf{P}(p)$ is
bound to $c$ if all the edges crossed by $\chi$ are bound to $c$. Observe that
$e\in\mathbf{P}(p)$ is a preserved edge iff it is not bound to an eliminated
cut.

######  Lemma 11.

Let $c=\langle t_{0}\mathopen{|}s_{0}\rangle$:

  * •

if $\chi\in\mathbf{P}(p)$ is bound to $c=\langle
t_{0}\mathopen{|}s_{0}\rangle$ and $s_{0}=\invamp(\overrightarrow{s})$ then
there exists $s\in\overrightarrow{s}$ such that $\chi\in\mathbf{P}(p,I)$
whenever $I(s_{0})=s$;

  * •

if $\chi\in\mathbf{P}(p,I)$ does not cross any edge bound to $c$ then
$\chi\in\mathbf{P}(p,I^{\prime})$ whenever $I$ and $I^{\prime}$ differ only on
$s_{0}$.

######  Proof 4.3.

It is sufficient to observe that the edge $s_{0}$ is bound to $c$; and the
only edge $e\in\mathbf{T}(p)$ that may be visited by a path bound to $c$ is
$s_{0}$.

A _$c$ -bridge_ is a path $\chi$ that is bound to $c$ and that crosses $c$.
Observe that $\chi$ is a $c$-bridge iff either $\chi$ or the reverse path
$\chi^{\dagger}$ is a subpath of some
$t\sim_{(t_{0},t)}t_{0}\sim_{c}s_{0}\sim_{s_{0}}s$ with
$t\in\overrightarrow{t}$ and $s\in\overrightarrow{s}$. Moreover, given
$t\in\\{t_{0}\\}\cup\overrightarrow{t}$ and
$s\in\\{s_{0}\\}\cup\overrightarrow{s}$ there is a unique $c$-bridge
$t\leadsto s$.

######  Lemma 12.

Assume $\chi_{1}\xi\chi_{2}\in\mathbf{P}(q)$ and $\xi=t\sim_{\langle
t\mathopen{|}s\rangle}s$, where $\chi_{1}$ and $\chi_{2}$ are preserved paths,
$t\in\overrightarrow{t}$ and $s\in\overrightarrow{s}$. Then there exists a
$c$-bridge $\xi^{\simeq}$ such that
$\chi_{1}^{-}\xi^{\simeq}\chi_{2}^{-}\in\mathbf{P}(p)$.

######  Proof 4.4.

Write $\chi_{1}:v_{1}\leadsto_{q,J}t$ and $\chi_{2}:s\leadsto_{q,J}v_{2}$: by
Lemma 10, we obtain $\chi_{1}^{-}:u_{1}\leadsto_{p,I}t^{\prime}$ and
$\chi_{2}^{-}:s^{\prime}\leadsto_{p,I}u_{2}$ where $u_{1}$, $t^{\prime}$,
$s^{\prime}$ and $u_{2}$ are anchors of $v_{1}$, $t$, $s$ and $v_{2}$
respectively, for any extension $I$ of $J$. In particular,
$t^{\prime}\in\\{t,t_{0}\\}$ and $s^{\prime}\in\\{s,s_{0}\\}$ and we can fix
$\xi^{\simeq}:t^{\prime}\leadsto s^{\prime}$ to be the only $c$-bridge with
those endpoints. Observe indeed that $\xi^{\simeq}\in\mathbf{P}(p,I)$ as soon
as $I(s_{0})=s$. Then by Lemmas 10 and 11, we can concatenate
$\chi_{1}^{-}\xi^{\simeq}\chi_{2}^{-}:u_{1}\leadsto_{p,I}u_{2}$.

Despite the notation, the definition of $\xi^{\simeq}$ does depend on
$\chi_{1}$ and $\chi_{2}$: whenever we use Lemma 12, however, the values of
$\chi_{1}$ and $\chi_{2}$ should be clear from the context.

We say a path $\chi\in\mathbf{P}(q)$ is a _straight path_ if it has no
slipknot. Such a path is essentially a path of $p$, up to replacing residuals
with bridges:

######  Lemma 13.

If $\chi$ is a straight path, there exists a unique sequence of pairwise
distinct eliminated cuts
$c_{1},\dotsc,c_{n}\in\mathbf{C}(p)\setminus\mathbf{C}(q)$, such that we can
write $\chi=\chi_{1}(d_{1})\cdots\chi_{n}(d_{n})\chi_{n+1}$ where each $d_{i}$
is a residual of $c_{i}$ and $\chi$ crosses no other residual. Moreover we can
form
$\chi^{-}=\chi^{-}_{1}(d_{1})^{\simeq}\cdots\chi^{-}_{n}(d_{n})^{\simeq}\chi_{n+1}^{-}\in\mathbf{P}(p)$.

######  Proof 4.5.

The first part is straightforward reformulation of the absence of slipknots.
The second part follows by applying Lemma 12 to each
$\chi_{i}(d_{i})\chi_{i+1}$ (or the reverse path): the concatenation of
preserved paths and bridges in the definition of $\chi^{-}$ is allowed by
Lemmas 10 and 11.

We say two paths $\chi_{1},\chi_{2}\in\mathbf{P}(q)$ are _independent_ if they
are disjoint and there is no eliminated cut $c$ such that both $\chi_{1}$ and
$\chi_{2}$ cross a residual of $c$.

######  Lemma 14.

Assume $\chi_{1},\dotsc,\chi_{n}\in\mathbf{P}(q,J)$ are pairwise independent
straight paths and $c_{1},\dotsc,c_{k}\in\mathbf{C}(p)\setminus\mathbf{C}(q)$
are such that no $\chi_{i}$ crosses a residual of $c_{j}$, for $1\leq i\leq n$
and $1\leq j\leq k$. Then for any $\xi_{1},\dotsc,\xi_{k}\in\mathbf{P}(p)$
such that $\xi_{i}$ is bound to $c$ for $1\leq i\leq k$, there exists an
extension $I$ of $J$ such that $\chi_{i}^{-}\in\mathbf{P}(p,I)$ for $1\leq
i\leq n$ and $\xi_{j}\in\mathbf{P}(p,I)$ for $1\leq j\leq k$.

######  Proof 4.6.

It is sufficient to observe that if $\chi^{-}$ crosses an edge bound to an
eliminated cut $c$ then $\chi$ crosses a residual of $c$. Then the result is a
direct consequence of the definition of $\chi^{-}_{i}$, together with Lemmas
10 and 11.

The generation of a path is thus compatible with the concatenation of
independent straight paths:

######  Lemma 15.

If $\chi_{1}:v\leadsto_{q}u$ and $\chi_{2}:u\leadsto_{q}t$ are independent
straight paths then $\chi_{1}\chi_{2}$ is a straight path and
$(\chi_{1}\chi_{2})^{-}=\chi_{1}^{-}\chi_{2}^{-}$.

######  Proof 4.7.

That $\chi_{1}\chi_{2}$ is a straight path follows directly from the
hypotheses. Write
$\chi_{i}=\chi^{i}_{1}(d^{i}_{1})\cdots\chi^{i}_{n_{i}}(d^{i}_{n_{i}})\chi^{i}_{n_{i}+1}$:
it is then sufficient to apply the definition of $\chi^{-}_{i}$ and observe
that
$(\chi^{1}_{n_{1}+1}\chi^{2}_{1})^{-}=(\chi^{1}_{n_{1}+1})^{-}(\chi^{2}_{1})^{-}$
by Lemma 10.

###  4.3. Bounces and slipknots

Let $c=\langle t_{0}\mathopen{|}s_{0}\rangle\in\mathbf{C}(p)$ with
$t_{0}=\otimes(\overrightarrow{t})$. A _$c$ -bounce_ is a path $\chi$ that is
bound to $c$, that does not cross $c$ and that visits $t_{0}$: $\chi$ is
either the empty path $\epsilon_{t_{0}}$, or $t_{0}\sim_{t_{0},t}t$ or
$t\sim_{t_{0},t}t_{0}$ with $t\in\overrightarrow{t}$, or
$t\sim_{(t_{0},t)}t_{0}\sim_{(t_{0},t^{\prime})}t^{\prime}$ with
$t\not=t^{\prime}\in\overrightarrow{t}$. Given
$t,t^{\prime}\in\\{t_{0}\\}\cup\overrightarrow{t}$, such that either $t=t_{0}$
or $t^{\prime}=t_{0}$ or $t\not=t^{\prime}$, there is a unique $c$-bounce
$t\leadsto t^{\prime}$.

######  Lemma 16.

Assume $\chi_{1}\xi\chi_{2}\in\mathbf{P}(q)$ and $\xi=(t_{1}\sim_{\langle
t_{1}\mathopen{|}s_{1}\rangle}s_{1})\xi^{\prime}(s_{2}\sim_{\langle
t_{2}\mathopen{|}s_{2}\rangle}t_{2})$, where $\chi_{1}$ and $\chi_{2}$ are
preserved paths, $t_{1},t_{2}\in\overrightarrow{t}$ and
$s_{1},s_{2}\in\overrightarrow{s}$. Then there exists a $c$-bounce
$\xi^{\vee}$ such that $\chi_{1}^{-}\xi^{\vee}\chi_{2}^{-}\in\mathbf{P}(p)$.

######  Proof 4.8.

Necessarily, $\langle t_{1}\mathopen{|}s_{1}\rangle\not=\langle
t_{2}\mathopen{|}s_{2}\rangle$, hence $t_{1}\not=t_{2}$. Write
$\chi_{1}:v_{1}\leadsto_{q}t_{1}$ and $\chi_{2}:t_{2}\leadsto_{q}v_{2}$: we
obtain $\chi_{1}^{-}:u_{1}\leadsto_{p}t^{\prime}_{1}$ and
$\chi_{2}^{-}:t^{\prime}_{2}\leadsto_{p}u_{2}$ where $u_{1}$,
$t^{\prime}_{1}$, $t^{\prime}_{2}$ and $u_{2}$ are anchors of $v_{1}$,
$t_{1}$, $t_{2}$ and $v_{2}$ respectively, for any extension $I$ of $J$. In
particular, $t^{\prime}_{1}\in\\{t_{1},t_{0}\\}$ and
$t^{\prime}_{2}\in\\{t_{2},t_{0}\\}$ with $t_{1}\not=t_{2}$, and we can fix
$\xi^{\vee}:t^{\prime}_{1}\leadsto t^{\prime}_{2}$ to be the only the only
$c$-bounce with those endpoints. Then we can concatenate
$\chi_{1}^{-}\xi^{\vee}\chi_{2}^{-}:u_{1}\leadsto_{p}u_{2}$ by Lemmas 10 and
11.

Again, the definition of $\xi^{\vee}$ does depend on $\chi_{1}$ and $\chi_{2}$
but these should be clear from the context when we use Lemma 16.

We are now ready to prove that paths in $q$ are alternations of straight paths
and slipknots, and generate paths in $p$ by replacing slipknots with bounces:

######  Theorem 17.

For each path $\chi\in\mathbf{P}(q)$, there exists a unique sequence of
pairwise distinct eliminated cuts
$c_{1},\dotsc,c_{n}\in\mathbf{C}(p)\setminus\mathbf{C}(q)$, such than we can
write $\chi=\chi_{1}\xi_{1}\cdots\chi_{n}\xi_{n}\chi_{n+1}$ where:

  * •

each $\chi_{i}$ is a straight path that crosses no residual of $c_{j}$ for
$1\leq j\leq n$;

  * •

$\chi_{i}$ and $\chi_{j}$ are independent when $i\not=j$;

  * •

each $\xi_{i}$ is a slipknot
$(d_{i})\xi^{\prime}_{i}(d^{\prime}_{i}):t_{i}\leadsto t^{\prime}_{i}$ where
$d_{i}$ and $d^{\prime}_{i}$ are residuals of $c_{i}$, and $t_{i}$ and
$t^{\prime}_{i}$ are distinct premises of the $\otimes$-tree of $c_{i}$.

Moreover
$\chi^{-}=\chi^{-}_{1}\xi_{1}^{\vee}\cdots\chi^{-}_{n}\xi^{\vee}_{n}\chi^{-}_{n+1}\in\mathbf{P}(p)$.

$\otimes$$c_{n}$$\otimes$$c_{1}$$\chi_{1}^{-}$$\chi_{n+1}^{-}$

reduces to
$d_{1}$$d_{1}^{\prime}$$\xi_{1}^{\prime}$$\chi_{1}$$d_{n}$$d_{n}^{\prime}$$\xi_{n}^{\prime}$$\chi_{n+1}$

Figure 13. Schematic shape of slipknots on a path (axiom and cut nodes
ommited)

Figure 13 illustrates the relationship between $\chi^{-}$ and $\chi$, in the
simple case where each cut is between binary connectives, and no redirected
jump is involved: each $\chi_{i}^{-}$ bounces on the $\otimes$ side of $c_{i}$
and joins $\chi_{i+1}^{-}$ directly instead of crossing the cut.

The proof of Theorem 17 is by induction on the length of $\chi$. We break it
down into a series of intermediate results. Formally, given
$\chi\in\mathbf{P}(q)$:

  * •

we first establish Lemma 18 for all paths such that Theorem 17 holds;

  * •

we deduce Lemma 19 for $\chi$ from Theorem 17 and Lemma 18 applied to $\chi$;

  * •

Lemma 20 for $\chi$ is a direct consequence of Lemma 19 applied to strict
subpaths of $\chi$;

  * •

we prove Lemma 21 for $\chi$ by applying Theorem 17, Lemma 18 and Lemma 20 to
strict subpaths of $\chi$;

  * •

then we prove Theorem 17 for $\chi$ by applying Lemmas 20 and 21 to $\chi$,
and Lemma 18 to strict subpaths of $\chi$.

######  Lemma 18.

Assume $\chi_{1},\dotsc,\chi_{n}\in\mathbf{P}(q,J)$ are pairwise disjoint
paths, and $c_{1},\dotsc,c_{k}\in\mathbf{C}(p)\setminus\mathbf{C}(q)$, are
such that no $\chi_{i}$ crosses a residual of $c_{j}$, for $1\leq i\leq n$ and
$1\leq j\leq k$. Then for any $\xi_{1},\dotsc,\xi_{k}\in\mathbf{P}(p)$ such
that $\xi_{i}$ is bound to $c$ for $1\leq i\leq k$, there exists an extension
$I$ of $J$ such that $\chi_{i}^{-}\in\mathbf{P}(p,I)$ for $1\leq i\leq n$ and
$\xi_{j}\in\mathbf{P}(p,I)$ for $1\leq j\leq k$.

######  Proof 4.9.

This is a direct consequence of the definition of $\chi^{-}_{i}$ in Theorem
17, together with Lemma 14.

######  Lemma 19.

Assume $d=\langle t\mathopen{|}s\rangle$ and $d^{\prime}=\langle
t^{\prime}\mathopen{|}s^{\prime}\rangle$ are distinct residuals of the same
cut $c=\langle t_{0}\mathopen{|}s_{0}\rangle$ with
$t_{0}=\otimes(\overrightarrow{t})$, $s_{0}=\invamp(\overrightarrow{s})$,
$t,t^{\prime}\in\overrightarrow{t}$ and $s,s^{\prime}\in\overrightarrow{s}$.
If $u\in d$, $u^{\prime}\in d^{\prime}$ and $\chi:u\leadsto_{q}u^{\prime}$
crosses no residual of $c$ then $u=s$ and $u^{\prime}=s^{\prime}$.

######  Proof 4.10.

Write $\chi=\chi_{1}\xi_{1}\cdots\chi_{n}\xi_{n}\chi_{n+1}$ as in Theorem 17,
and $\chi^{-}:v\leadsto_{p,I}v^{\prime}$ where $v$ (resp. $v^{\prime}$) is an
anchor of $u$ (resp. $u^{\prime}$). Observe that $\chi$ is non empty because
$u\not=u^{\prime}$. Moreover, the first edge of $\chi$ is a preserved edge: if
$\chi=(u\sim_{e}v)\chi^{\prime}$ then $e$ cannot be a cut, as otherwise we
would have $e=d$ and $\chi$ would cross a residual of $c$. It follows that
$\chi_{1}^{-}$ is non empty, hence $\chi^{-}$ is non empty. Since $\chi^{-}$
is non empty, there is no path $\zeta:v\leadsto v^{\prime}$ bound to $c$:
otherwise, by Lemma 18, we could form a non empty cycle
$\zeta^{\dagger}\chi^{-}:v^{\prime}\leadsto_{p}v^{\prime}$ .

If $u=t$ and $u^{\prime}=t^{\prime}$, we have $v\in\\{t,t_{0}\\}$ and
$v^{\prime}\in\\{t^{\prime},t_{0}\\}$ with $t\not=t^{\prime}$, and we obtain a
$c$-bounce $v\leadsto v^{\prime}$, hence a contradiction. If $u=t$ and
$u^{\prime}=s^{\prime}$, we have $v\in\\{t,t_{0}\\}$ and
$v^{\prime}\in\\{s^{\prime},s_{0}\\}$, and we obtain a $c$-bridge $v\leadsto
v^{\prime}$, hence a contradiction. We rule out the case $u=s$ and
$u^{\prime}=t^{\prime}$ symmetrically.

######  Lemma 20.

If $\chi\in\mathbf{P}(q)$ and
$c=\langle\otimes(\overrightarrow{t})\mathopen{|}\invamp(\overrightarrow{s})\rangle\in\mathbf{C}(p)\setminus\mathbf{C}(q)$,
then $\chi$ crosses at most two residuals of $c$, and in this case we can
write $\chi=\chi_{1}(t\sim_{\langle
t\mathopen{|}s\rangle}s)\chi_{2}(s^{\prime}\sim_{\langle
t^{\prime}\mathopen{|}s^{\prime}\rangle}t^{\prime})\chi_{3}$ with
$t,t^{\prime}\in\overrightarrow{t}$ and $s,s^{\prime}\in\overrightarrow{s}$.

######  Proof 4.11.

If $\chi=\chi_{1}(d)\chi_{2}(d^{\prime})\chi_{3}$, where $d=\langle
t\mathopen{|}s\rangle$ and $d^{\prime}=\langle
t^{\prime}\mathopen{|}s^{\prime}\rangle$ are residuals of $c$ with
$t,t^{\prime}\in\overrightarrow{t}$ and $s,s^{\prime}\in\overrightarrow{s}$,
and if $\chi_{2}$ crosses no residual of $c$, then by Lemma 19 applied to
$\chi_{2}$, we obtain $\chi=\chi_{1}(t\sim_{\langle
t\mathopen{|}s\rangle}s)\chi_{2}(s^{\prime}\sim_{\langle
t^{\prime}\mathopen{|}s^{\prime}\rangle}t^{\prime})\chi_{3}$. If moreover
$\chi_{1}$ (resp. $\chi_{3}$) crossed another residual of $c$, we would obtain
a contradiction by applying Lemma 19 to a strict subpath of $\chi_{1}$ (resp.
$\chi_{3}$) hence of $\chi$.

######  Lemma 21.

Slipknots are well-bracketed in the following sense: there is no path
$\chi=(d_{1})\chi_{1}(d_{2})\chi_{2}(d^{\prime}_{1})\chi_{3}(d^{\prime}_{2})\in\mathbf{P}(q)$
such that, for $1\leq i\leq 2$, $d_{i}$ and $d^{\prime}_{i}$ are residuals of
the same cut.

######  Proof 4.12.

Assume
$\chi=(d_{1})\chi_{1}(d_{2})\chi_{2}(d^{\prime}_{1})\chi_{3}(d^{\prime}_{2})\in\mathbf{P}(q)$
such that, for $1\leq i\leq 2$, $d_{i}$ and $d^{\prime}_{i}$ are residuals of
the same cut. We can assume w.l.o.g. that $\chi_{1}$ and $\chi_{3}$ are
independent: otherwise there is a prefix of $\chi$ with this additional
property.

For $1\leq i\leq 2$, let $c_{i}=\langle
t_{0}^{i}\mathopen{|}s_{0}^{i}\rangle$, with
$t^{i}_{0}=\otimes(\overrightarrow{t}_{i})$ and
$s^{i}_{0}=\invamp(\overrightarrow{s}_{i})$, and assume
$d_{i}=\\{t_{i},s_{i}\\}$ and
$d^{\prime}_{i}=\\{t^{\prime}_{i},s^{\prime}_{i}\\}$, with
$t_{i},t^{\prime}_{i}\in\overrightarrow{t}_{i}$ and
$s_{i},s^{\prime}_{i}\in\overrightarrow{s}_{i}$. By Lemma 20, we must have
$\chi=(t_{1}\sim_{d_{1}}s_{1})\chi_{1}(t_{2}\sim_{d_{2}}s_{2})\chi_{2}(s^{\prime}_{1}\sim_{d^{\prime}_{1}}t^{\prime}_{1})\chi_{3}(s^{\prime}_{2}\sim_{d^{\prime}_{2}}t^{\prime}_{2})$.

By Theorem 17, we obtain $\chi_{1}^{-}:u_{1}\leadsto_{p}v_{2}$ and
$\chi_{3}^{-}:v_{1}\leadsto_{p}u_{2}$, where $u_{1}\in\\{s_{1},s_{0}^{1}\\}$,
$v_{2}\in\\{t_{2},t_{0}^{2}\\}$, $v_{1}\in\\{t^{\prime}_{1},t_{0}^{1}\\}$ and
$u_{2}\in\\{s^{\prime}_{2},s_{0}^{2}\\}$. Write
$\zeta_{1}:v_{1}\leadsto_{p}u_{1}$ (resp. $\zeta_{2}:v_{2}\leadsto_{p}u_{2}$)
for the only $c_{1}$-bridge (resp. $c_{2}$-bridge) with those endpoints. Then
we obtain a non empty cycle
$\chi^{-}_{1}\zeta_{2}(\chi_{3}^{\dagger})^{-}\zeta_{1}:u_{1}\leadsto_{p}u_{1}$:
the concatenation is allowed by Lemma 18 applied to $\chi_{1}$ and
$\chi_{3}^{\dagger}$.

######  Proof 4.13 (Proof of Theorem 17).

By Lemma 21, we can write
$\chi=\chi_{1}\xi_{1}\cdots\chi_{n}\xi_{n}\chi_{n+1}$ where
$\xi_{1},\dotsc,\xi_{n}$ are the slipknots of $\chi$ that are maximal (_i.e._
not strict subpaths of other slipknots) and this writing is unique. Let
$c_{1},\dotsc,c_{n}$ be the associated eliminated cuts. By Lemma 20, the
$c_{j}$’s are pairwise distinct, and $\xi_{j}:t_{j}\leadsto_{p}t^{\prime}_{j}$
where $t_{j}$ and $t^{\prime}_{j}$ are distinct premises of the $\otimes$-tree
of $c_{j}$. Moreover, since each slipknot of $\chi$ is a subpath of some
$\xi_{j}$:

  * •

each $\chi_{i}$ is a straight path and it crosses no residual of any $c_{j}$;

  * •

the $\chi_{i}$’s are pairwise independent.

If $n=0$, we can set $\chi^{-}=\chi_{1}^{-}$. Otherwise, we apply Lemma 18 to
the $\chi_{i}$’s, which are strict subpaths of $\chi$, which allows to
concatenate
$\chi^{-}=\chi^{-}_{1}\xi_{1}^{\vee}\cdots\chi^{-}_{n}\xi^{\vee}_{n}\chi^{-}_{n+1}\in\mathbf{P}(p)$.

Again, the construction of $\chi^{-}$ is compatible with the concatenation of
independent paths:

######  Lemma 22.

If $\chi_{1}\chi_{2}\in\mathbf{P}(q)$ and $\chi_{1}$ and $\chi_{2}$ are
independent, then $(\chi_{1}\chi_{2})^{-}=\chi_{1}^{-}\chi_{2}^{-}$.

######  Proof 4.14.

As for Lemma 15, this is a direct consequence of the definition of
$(\chi_{1}\chi_{2})^{-}$, $\chi_{1}^{-}$ and $\chi_{2}^{-}$, this time using
Lemma 15 to concatenate a straight suffix of $\chi_{1}$ and a straight prefix
of $\chi_{2}$.

###  4.4. Bounding the growth of $\mathbf{ln}$

Now we show that we can bound $\mathbf{ln}(q)$ depending only on
$\mathbf{ln}(p)$. We first need some basic properties relating the length of
$\chi^{-}$ with that of $\chi$.

######  Lemma 23.

Let $\chi,\xi\in\mathbf{P}(q)$ and $\zeta\in\mathbf{P}(p)$:

  1. (1)

if $\chi$ is preserved then $\mathbf{ln}(\chi^{-})=\mathbf{ln}(\chi)$;

  2. (2)

if $\zeta$ is a bridge then $1\leq\mathbf{ln}(\zeta)\leq 3$;

  3. (3)

if $\zeta$ is a bounce then $\mathbf{ln}(\zeta)\leq 2$;

  4. (4)

if $\chi$ is straight, then $\mathbf{ln}(\chi)\leq\mathbf{ln}(\chi^{-})\leq
3\mathbf{ln}(\chi)$;

  5. (5)

if $\xi$ is a prefix of $\chi$ and $\chi$ is straight then $\xi^{-}$ is a
prefix of $\chi^{-}$;

  6. (6)

if $\xi$ is a slipknot then $\mathbf{ln}(\xi)\geq 3$ and
$\mathbf{ln}(\xi^{\vee})<\mathbf{ln}(\xi)$;

  7. (7)

in general $\mathbf{ln}(\chi^{-})\leq 3\mathbf{ln}(\chi)$.

######  Proof 4.15.

The first three properties are direct consequences of the definitions. Item
(4) follows from (1) and (2). Item (5) follows from Lemma 15. Item (6) follows
from Lemma 9 and (3). And item (7) follows from (4) and (6).

Observe that in general, we do not have
$\mathbf{ln}(\zeta^{-})\leq\mathbf{ln}(\chi^{-})$ when $\zeta$ is a prefix of
$\chi$: $\zeta$ may enter an arbitrarily long slipknot of $\chi$ that is
replaced by a single bounce in $\chi^{-}$. For this reason, we introduce the
following notion: if $\chi\in\mathbf{P}(q)$, we define the _width_ of $\chi$
(relative to the reduction $p\rightrightarrows_{m}q$ we consider) by
$0pt(\chi)=\max\\{\mathbf{ln}(\zeta^{-})\mid\zeta\text{ prefix of }\chi\\}$.

######  Lemma 24.

For any path $\chi\in\mathbf{P}(q)$, $\mathbf{ln}(\chi^{-})\leq
0pt(\chi)\leq\mathbf{ln}(p)$ and $0pt(\chi)\leq 3\mathbf{ln}(\chi)$. Moreover,
if $\zeta$ is a prefix of $\chi$, we have $0pt(\zeta)\leq 0pt(\chi)$. If
moreover $\chi$ is straight,
$0pt(\chi)=\mathbf{ln}(\chi^{-})\geq\mathbf{ln}(\chi)$.

######  Proof 4.16.

We obtain $\mathbf{ln}(\chi^{-})\leq 0pt(\chi)\leq\mathbf{ln}(p)$ and
$0pt(\zeta)\leq 0pt(\chi)$ directly from the definition of width. Item (7) of
Lemma 23 gives $0pt(\chi)\leq 3\mathbf{ln}(\chi)$. If $\chi$ is straight
$0pt(\chi)=\mathbf{ln}(\chi^{-})\geq\mathbf{ln}(\chi)$ follows from items (4)
and (5) of Lemma 23.

Define $\varphi:\mathbf{N}\to\mathbf{N}$ inductively by $\varphi(0)=0$ and
$\varphi(n)=n+(n+1)(\varphi(n-1)+2)$ if $n>0$. Observe that
$n\leq\varphi(n)\leq\varphi(n+1)$.

######  Lemma 25.

If $\chi\in\mathbf{P}(q)$ then $\mathbf{ln}(\chi)\leq\varphi(0pt(\chi))$.

######  Proof 4.17.

The proof is by induction on $0pt(\chi)$. If $\chi$ is straight then, by Lemma
24, $\mathbf{ln}(\chi)\leq 0pt(\chi)\leq\varphi(0pt(\chi))$.

Write $\chi=\chi_{1}\xi_{1}\cdots\chi_{n}\xi_{n}\chi_{n+1}$ as in Theorem 17:
we have
$\mathbf{ln}(\chi)=\sum_{i=1}^{n+1}\mathbf{ln}(\chi_{i})+\sum_{j=1}^{n}\mathbf{ln}(\xi_{j})$.
Since
$\chi^{-}=\chi_{1}^{-}\xi_{1}^{\vee}\cdots\chi_{n}^{-}\xi_{n}^{\vee}\chi_{n+1}^{-}$,
we have $\sum_{i=1}^{n+1}\mathbf{ln}(\chi_{i}^{-})\leq\mathbf{ln}(\chi^{-})$.
Since each $\chi_{i}$ is straight, we obtain
$\mathbf{ln}(\chi)\leq\mathbf{ln}(\chi^{-})+\sum_{j=1}^{n}\mathbf{ln}(\xi_{j})$
from the previous inequality, by applying item (4) of Lemma 23.

Moreover observe that, by Lemma 9, $\chi_{i}$ is non empty for $1<i<n+1$.
Hence $\mathbf{ln}(\chi^{-})\geq n-1$, and we obtain $n\leq 0pt(\chi)+1$.

It remains to bound $\mathbf{ln}(\xi_{j})$ for $1\leq j\leq n$. We can write
$\xi_{j}=(d_{j})\chi^{\prime}_{j}(d^{\prime}_{j})$ where $d_{j}$ and
$d^{\prime}_{j}$ are the residuals of the cut $c_{j}$ associated with
$\xi_{j}$. Let $\zeta^{\prime}_{j}$ be a prefix of $\chi^{\prime}_{j}$ and
write $\zeta_{j}=\chi_{1}\xi_{1}\cdots\chi_{j}(d_{j})\zeta^{\prime}_{j}$ which
is a prefix of $\chi$. Observe that, by Theorem 17, $c_{j}$ has no residual in
$\zeta_{j}$ other than $d_{j}$, and $\chi_{1}\xi_{1}\cdots\chi_{j}(d_{j})$ and
$\zeta^{\prime}_{j}$ are independent. Hence $\chi_{j}(d_{j})$ is straight and
$\zeta_{j}^{-}=\chi_{1}^{-}\xi_{1}^{\vee}\cdots\chi_{j}^{-}d_{j}^{\simeq}(\zeta^{\prime}_{j})^{-}$
follows by Lemma 22. Since $\mathbf{ln}(d_{j}^{\simeq})\geq 1$, we obtain
$\mathbf{ln}((\zeta^{\prime}_{j})^{-})\leq\mathbf{ln}(\zeta_{j}^{-})-1\leq
0pt(\chi)-1$.

Hence $0pt(\chi^{\prime}_{j})\leq 0pt(\chi)-1$: we apply the induction
hypothesis and obtain
$\mathbf{ln}(\chi^{\prime}_{j})\leq\varphi(0pt(\chi^{\prime}_{j}))\leq\varphi(0pt(\chi)-1)$
because $\varphi$ is monotonous. It follows that
$\mathbf{ln}(\xi_{j})\leq\varphi(0pt(\chi)-1)+2$, and we conclude:

$\displaystyle\mathbf{ln}(\chi)$
$\displaystyle\leq\mathbf{ln}(\chi^{-})+\sum_{j=1}^{n}\mathbf{ln}(\xi_{j})$
$\displaystyle\leq 0pt(\chi)+(0pt(\chi)+1)(\varphi(0pt(\chi)-1)+2)$
$\displaystyle\leq\varphi(0pt(\chi)).$

Using Lemma 24 again, we obtain:

######  Corollary 26.

Let $p\rightrightarrows_{m}q$. Then,
$\mathbf{ln}(q)\leq\varphi(\mathbf{ln}(p))$.

Notice that the previous result can be seen as a quantitative version of the
preservation of acyclicity in proof nets under reduction. In the following
example, we illustrate how acyclicity is mandatory for the existence of a
function $\varphi$ as in Corollary 26. Let $p=(\langle
t\mathopen{|}s\rangle;)$ with $t=\otimes(x_{0},\dotsc,x_{n})$ and
$s=\invamp(\overline{x}_{1},\dotsc,\overline{x}_{n},\overline{x}_{0})$: by
setting $I(s)=\overline{x}_{i}$, we obtain a cycle
$x_{i}\sim_{\\{x_{i},\overline{x}_{i}\\}}\overline{x}_{i}\sim_{s}s\sim_{\langle
t\mathopen{|}s\rangle}t\sim_{t,x_{i}}x_{i}$. Since each path
$\chi\in\mathbf{P}(p)$ can cross each of $s$ and $\langle
t\mathopen{|}s\rangle$ at most once, it is easy to check that
$\mathbf{ln}(p)=6$.

But $p\rightrightarrows_{m}q=(\langle
x_{0}\mathopen{|}\overline{x}_{1}\rangle,\dotsc,\langle
x_{n-1}\mathopen{|}\overline{x}_{n}\rangle,\langle
x_{n}\mathopen{|}\overline{x}_{0}\rangle;)$ hence $\mathbf{ln}(q)=2(n+1)$. The
situation is illustrated in Figure 14.

axax . . . ax$\otimes$cut$x_{0}\ $$\ \overline{x}_{0}$$x_{1}\ $$\
\overline{x}_{1}$$x_{n}\ $$\ \overline{x}_{n}$ . . . . . . axax . . . axcutcut
. . . cut$x_{0}\ $$\ \overline{x}_{0}$$x_{1}\ $$\ \overline{x}_{1}$$x_{n}\ $$\
\overline{x}_{n}$$\scriptstyle\cdots$$\scriptstyle\cdots$$\rightrightarrows_{m}$
Figure 14. A cyclic counterexample to Corollary 26

###  4.5. Erratum

In the extended abstract of the present paper, the analogue [CVA18, Subsection
3.2] of Subsection 4.4 claimed to establish similar results for another
measure on paths: rather than the length $\mathbf{ln}(\xi)$ of a path $\xi$,
we considered the number $\mathbf{cc}(\xi)$ of all the cuts $\langle
t\mathopen{|}s\rangle$ such that $\xi$ visits $t$ or $s$.

It is easy to check that Lemma 5 still holds if we replace the maximal length
of a path with the maximum number of cuts in a chain of axiom cuts in the
sense of Figure 2. Given the situation depicted in Figure 13, however, it is
evident that a bound on the number of cuts crossed by a path cannot be
preserved: the path on the left hand side crosses no cut, while the path in
the reduct crosses an arbitrary number of (possibly axiom) cuts. We introduced
$\mathbf{cc}(\xi)$ in our previous attempt, precisely to capture this example:
if $\xi$ is the path following the tensors of the left hand side, then
$\mathbf{cc}(\xi)\geq n$. But this fix is actually not sufficient: if we
replace each $c_{i}=\langle t_{i}\mathopen{|}s_{i}\rangle$ in Figure 13, with
$\langle\otimes(t_{i},s_{i})\mathopen{|}\invamp(x_{i},\overline{x_{i}})\rangle$,
a path in the obtained net can visit at most two of these new cuts, but it
reduces to the left hand side, with $\xi$ such that $\mathbf{cc}(\xi)\geq n$.

It might be possible to adapt our method for dealing with a relaxed definition
of visited cut: for instance, we might consider the number of cuts $c$ such
that $\xi$ visits a tree $t\in\mathbf{T}(c)$ (instead of $t\in c$). But this
notion is no longer local, and would introduce further technicalities: for
that reason, we decided to focus on the length of paths instead, which is a
more intuitive and standard notion, without any _ad hoc_ reference to cuts.

##  5\. Variations of $\mathbf{jd}(p)$ under reduction

For establishing that $\mathbf{jd}(q)$ is bounded as a function of
$\mathbf{jd}(p)$ and $\mathbf{ln}(p)$ we examine the reductions separately.

######  Lemma 27.

Let $p,q$ two proof nets. If $p\rightrightarrows_{m}q$, then
$\mathbf{jd}(q)\leq 2\mathbf{jd}(p)$.

######  Proof 5.1.

For all $t\in\mathbf{T}(q)$ the only case in which
$\jmath^{-1}_{q}(t)\not=\jmath^{-1}_{p}(t)$ is that of redirected jumps: there
must be $\mu\in\mathbf{U}_{\bot}(q)$ such that $t$ is part of a residual
$\langle t\mathopen{|}s\rangle$ of an eliminated cut $\langle
t_{0}\mathopen{|}s_{0}\rangle\in\mathbf{C}(p)$, with $\jmath_{p}(\mu)=t_{0}$.
In this case we have
$\mathbf{jd}_{q}(t)=\mathbf{jd}_{p}(t)+\mathbf{jd}_{p}(t_{0})\leq
2\mathbf{jd}(p)$.

######  Lemma 28.

Let $p,q$ two proof nets. If $p\rightrightarrows_{e}q$, then
$\mathbf{jd}(q)\leq(2\mathbf{jd}(p))^{\mathbf{ln}(p)+1}$.

######  Proof 5.2.

Fix $t\in\mathbf{T}(q)$. For any $\mu\in\mathbf{U}_{\bot}(q)$, if
$\jmath_{q}(\mu)=t$, then $\mu\in\mathbf{I}_{p}^{n}(t)$ for some
$n\in\mathbf{N}$: this is precisely the purpose of the definition of
$\mathbf{I}^{n}_{p}$. We obtain
$\mathbf{jd}_{q}(t)\leq\\#\left(\bigcup_{n\in\mathbf{N}}\mathbf{I}_{p}^{n}(t)\right)\leq(2\mathbf{jd}(p))^{\mathbf{ln}(p)+1}$
by Lemma 6 (1).

######  Lemma 29.

Let $p,q$ two proof nets. If $p\rightrightarrows_{a}q$, then
$\mathbf{jd}(q)\leq(\mathbf{ln}(p)+1)\mathbf{jd}(p)$.

######  Proof 5.3.

As in the proof of Lemma 5, we can write
$p=(\overrightarrow{c_{1}},\dotsc,\overrightarrow{c_{k}},\overrightarrow{c};\overrightarrow{s})$
and
$q=(\overrightarrow{c};\overrightarrow{s})[t^{1}/\overline{x}^{1}_{0}]\cdots[t^{k}/\overline{x}^{k}_{0}]$
where $\overrightarrow{c}_{i}=(\langle
x^{i}_{0}\mathopen{|}\overline{x}^{i}_{1}\rangle,\dotsc,\langle
x^{i}_{n_{i}-1}\mathopen{|}\overline{x}^{i}_{n_{i}}\rangle,\langle
x^{i}_{n_{i}}\mathopen{|}t^{i}\rangle)$.

By the definition of cut elimination, for all $\mu\in\mathbf{U}_{\bot}(q)$ we
have:

$\jmath_{q}(\mu)=\begin{cases}t^{i}[t^{i+1}/\overline{x}_{0}^{i+1}]\cdots[t^{k}/\overline{x}_{0}^{k}]&\text{if
$\jmath_{p}(\mu)\in\\{x^{i}_{0},\overline{x}^{i}_{0},x^{i}_{1},\dots,\overline{x}^{i}_{n_{i}},t^{i}\\}$}\\\
\jmath_{q}(\mu)[t^{1}/\overline{x}_{0}^{1}]\cdots[t^{k}/\overline{x}_{0}^{k}]&\text{otherwise}\end{cases}.$

It follows that:

  * •

$\mathbf{jd}_{q}(t^{i}[t^{i+1}/\overline{x}_{0}^{i+1}]\cdots[t^{k}/\overline{x}_{0}^{k}])=\mathbf{jd}_{p}(t^{i})+\sum_{j=0}^{n_{i}}(\mathbf{jd}_{p}(x^{i}_{j})+\mathbf{jd}_{p}(\overline{x}^{i}_{j}))\leq(2n_{i}+3)\mathbf{jd}(p)$;

  * •

if
$t\in\mathbf{T}(p)\setminus\bigcup_{i=1}^{k}\\{x^{i}_{0},\overline{x}^{i}_{0},x^{i}_{1},\dots,\overline{x}^{i}_{n_{i}},t^{i}\\}$,
then
$\mathbf{jd}_{q}(t[t^{1}/\overline{x}_{0}^{1}]\cdots[t^{k}/\overline{x}_{0}^{k}])=\mathbf{jd}_{p}(t)$.

To conclude, it is sufficient to observe that $2n_{i}+2\leq\mathbf{ln}(p)$:
indeed each $\overrightarrow{c}_{i}$ induces a path alternating between
$n_{i}+1$ axioms an $n_{i}+1$ cuts.

##  6\. Bounding the size of antireducts: general and iterated case

The previous results now allow us to treat the general case of a reduction
$p\rightrightarrows q$.

######  Theorem 30.

If $p\rightrightarrows q$ then
$\mathbf{size}(p)\leq\psi\left(2(\mathbf{ln}(p)+1)\mathbf{size}(q),\mathbf{ln}(p),\mathbf{jd}(p)\right)$.

######  Proof 6.1.

Consider $q^{\prime},q^{\prime\prime}$ such that
$p\rightrightarrows_{e}q^{\prime}\rightrightarrows_{a}q^{\prime\prime}\rightrightarrows_{m}q$.
We have:

$\displaystyle\mathbf{size}(p)$
$\displaystyle\leq\psi(\mathbf{size}(q^{\prime}),\mathbf{jd}(p),\mathbf{ln}(p))$
(by Lemma 7)
$\displaystyle\leq\psi((\mathbf{ln}(q^{\prime})+1)\mathbf{size}(q^{\prime\prime}),\mathbf{jd}(p),\mathbf{ln}(p))$
(by Lemma 5)
$\displaystyle\leq\psi((\mathbf{ln}(p)+1)\mathbf{size}(q^{\prime\prime}),\mathbf{jd}(p),\mathbf{ln}(p))$
(by Lemma 8)
$\displaystyle\leq\psi(2(\mathbf{ln}(p)+1)\mathbf{size}(q),\mathbf{jd}(p),\mathbf{ln}(p))$
$\displaystyle\text{(by Lemma~{}\ref{mult})}\quad.$

######  Corollary 31.

If $q$ is an MLL net and $n,m\in\mathbf{N}$, then

$\\{p\mid p\rightrightarrows q,\ \mathbf{jd}(p)\leq m\text{ and
}\mathbf{ln}(p)\leq n\\}$

is finite.

Of course, that result holds only up to the $\alpha$-equivalence mentioned in
Remark 1: then it is easy to check that the cardinality of
$\\{p\mid\mathbf{size}(p)\leq k\\}$ is bounded by a function of
$k\in\mathbf{N}$. Also recall from Remark 2 that we are actually interested in
bare nets rather than nets with jumps, so Corollary 31 should be read as
follows: given a bare net $q$ and $n,m\in\mathbf{N}$ there are finitely many
bare nets $p$ such that $p\rightrightarrows q$ and that can be equipped with a
jump function $\jmath_{p}$ satisfying $\mathbf{jd}(p)\leq m$ and
$\mathbf{ln}(p)\leq n$. More precisely, Theorem 30 entails that the number of
such bare nets $p$ can be bounded by a function of $m$, $n$ and
$\mathbf{size}(q)$.

It follows that, given an infinite linear combination $\sum_{i\in
I}a_{i}.p_{i}$, assuming that we can equip each $p_{i}$ with a jump function
$\jmath_{p_{i}}$ so that $\\{\mathbf{ln}(p_{i})\mid i\in
I\\}\cup\\{\mathbf{jd}(p_{i})\mid i\in I\\}$ is finite, we can always consider
an arbitrary family of reductions $p_{i}\rightrightarrows q_{i}$ for $i\in I$
and form the sum $\sum_{i\in I}a_{i}.q_{i}$: this is always well defined. But
if we want to iterate this process and perform a reduction from $\sum_{i\in
I}a_{i}.q_{i}$ to $\sum_{i\in I}a_{i}.r_{i}$, when $q_{i}\rightrightarrows
r_{i}$ for $i\in I$, we need to ensure that a similar side condition holds for
the $q_{i}$’s. Again, this is a consequence of our previous results, which we
sum up in the following two theorems.

######  Theorem 32.

Let $p\rightrightarrows q$. Then $\mathbf{ln}(q)\leq\varphi(\mathbf{ln}(p))$.

######  Proof 6.2.

Consider $q^{\prime},q^{\prime\prime}$ such that
$p\rightrightarrows_{m}q^{\prime}\rightrightarrows_{e}q^{\prime\prime}\rightrightarrows_{a}q$.
We have:

$\displaystyle\mathbf{ln}(q)$ $\displaystyle\leq\mathbf{ln}(q^{\prime\prime})$
(by Lemma 8) $\displaystyle\leq\mathbf{ln}(q^{\prime})$ (by Lemma 8)
$\displaystyle\leq\varphi(\mathbf{ln}(p))$ $\displaystyle\text{(by
Corollary~{}\ref{vc})}\quad.$

######  Theorem 33.

There exists a function $\theta:\mathbf{N}\to\mathbf{N}$ such that
$\mathbf{jd}(q)\leq\theta(\mathbf{ln}(p),\mathbf{jd}(p))$ whenever
$p\rightrightarrows q$.

######  Proof 6.3.

Consider $q^{\prime},q^{\prime\prime}$ such that
$p\rightrightarrows_{a}q^{\prime}\rightrightarrows_{e}q^{\prime\prime}\rightrightarrows_{m}q$.
We have

$\displaystyle\mathbf{jd}(q)$ $\displaystyle\leq
2\mathbf{jd}(q^{\prime\prime})$ (by Lemma 27) $\displaystyle\leq
2(2\mathbf{jd}(q^{\prime}))^{\mathbf{ln}(q^{\prime})+1}$ (by Lemma 28)
$\displaystyle\leq
2(2(\mathbf{ln}(p)+1)\mathbf{jd}(p))^{\mathbf{ln}(q^{\prime})+1}$ (by Lemma
29) $\displaystyle\leq
2(2(\mathbf{ln}(p)+1)\mathbf{jd}(p))^{\mathbf{ln}(p)+1}$
$\displaystyle\text{(by Lemma~{}\ref{cc_ax_e})}\quad.$

By the previous results, we can iterate Corollary 31 and obtain:

######  Corollary 34.

If $q$ is an MLL net and $k,n,m\in\mathbf{N}$, then

$\\{p\mid p\rightrightarrows^{k}q,\ \mathbf{jd}(p)\leq m\text{ and
}\mathbf{ln}(p)\leq n\\}$

is finite.

##  7\. Taylor expansion

We now show how the previous results apply to Taylor expansion. For that
purpose, we must extend our syntax to MELL proof nets. Our presentation
departs from Ehrhard’s [Ehr16] in our treatment of promotion boxes: instead of
introducing boxes as tree constructors labelled by nets, with auxiliary ports
as inputs, we consider box ports as $0$-ary trees, that are related with each
other in a _box context_ , associating each box with its contents. This is in
accordance with the usual presentation of promotion as a black box, and has
two motivations:

  * •

in Ehrhard’s syntax, the promotion is not a net but an open tree, for which
the trees associated with auxiliary ports must be mentioned explicitly: this
would complicate the expression of Taylor expansion;

  * •

since we consider a single class of $\wn$-links instead of having a separate
dereliction, we must impose constraints on auxiliary ports, that are easier to
express when these ports are directly represented in the syntax.

Then we show that if $p$ is a resource net in the support of the Taylor
expansion of an MELL proof net $P$, then $\mathbf{ln}(p)$ and $\mathbf{jd}(p)$
are bounded by functions of $P$.

Observe that we need only to consider the support of Taylor expansion, so we
do not formalize the expansion of MELL nets into infinite linear combinations
of resource nets: rather, we introduce $\mathcal{T}(P)$ as a set of
approximants.

###  7.1. MELL nets

In addition to the set of variables, we fix a denumerable set $\mathbf{B}$ of
_box ports_ : we assume given an enumeration $\mathbf{B}=\\{a^{b}_{i}\mid
i,b\in\mathbf{N}\\}$. We call _principal ports_ the ports $a^{b}_{0}$ and
_auxiliary ports_ the other ports. Instead of separate contractions and
derelictions, we consider a unified $\wn$-link of arbitrary arity; auxiliary
ports of boxes must be premises of such links (or of auxiliary ports of outer
boxes, that must satisfy this constraint inductively).

The weakenings (and coweakenings, in the resource nets yet to be introduced)
are not essentially different from the multiplicative units in our untyped
nets. Indeed, we will see that the geometrical and combinatorial behaviour of
the $\wn$-link (resp. the $\oc$-link) is identical to that of the
(respectively, of the $\otimes$). This will be reflected in our use of labels:
in addition to $\mathbf{U}_{\mathbf{1}}$ and $\mathbf{U}_{\bot}$, we will use
labels from denumerable sets $\mathbf{U}_{\oc}$ and $\mathbf{U}_{\wn}$ (now
assuming $\mathbf{V}$, $\mathbf{B}$, $\mathbf{U}_{\mathbf{1}}$,
$\mathbf{U}_{\bot}$, $\mathbf{U}_{\oc}$ and $\mathbf{U}_{\wn}$ are pairwise
disjoint), and write
$\mathbf{U}_{+}=\mathbf{U}_{\mathbf{1}}\cup\mathbf{U}_{\oc}$ and
$\mathbf{U}_{-}=\mathbf{U}_{\bot}\cup\mathbf{U}_{\wn}$.

We introduce the corresponding term syntax. _Raw pre-trees_ ($S^{\circ}$,
$T^{\circ}$, _etc._) and _raw trees_ ($S$, $T$, _etc._) are defined by mutual
induction as follows:

$\displaystyle T$ $\displaystyle\Coloneqq
x\mid\mathbf{1}_{\lambda}\mid\bot_{\mu}\mid\otimes(T_{1},\dotsc,T_{n})\mid\invamp(T_{1},\dotsc,T_{n})\mid
a^{b}_{0}\mid\wn_{\mu^{\prime}}()\mid\wn(T^{\circ}_{1},\dotsc,T^{\circ}_{n})$
$\displaystyle T^{\circ}$ $\displaystyle\Coloneqq T\mid a^{b}_{i+1}$

where $x$ ranges over $\mathbf{V}$, $\lambda$ ranges over
$\mathbf{U}_{\mathbf{1}}$, $\mu$ ranges over $\mathbf{U}_{\bot}$,
$\mu^{\prime}$ ranges over $\mathbf{U}_{\wn}$, $b$ and $i$ range over
$\mathbf{N}$ and we require $n\not=0$ in each of
$\otimes(T_{1},\dotsc,T_{n})$, $\invamp(T_{1},\dotsc,T_{n})$ and
$\wn(T^{\circ}_{1},\dotsc,T^{\circ}_{n})$. The set $\mathbf{T}^{\circ}(S)$ of
the sub-pre-trees of $S$ is defined in the natural way, as well as the set
$\mathbf{T}(S)$ of sub-trees of $S$, from which we derive the definitions of
$\mathbf{V}(S)$, $\mathbf{B}(S)$, $\mathbf{U}_{\bot}(S)$, _etc._ The set
$\mathbf{A}(S)$ of atoms of $S$ is then
$\mathbf{V}(S)\cup\mathbf{B}(S)\cup\mathbf{U}_{\mathbf{1}}(S)\cup\mathbf{U}_{-}(S)$.

A _tree_ (resp. a _pre-tree_) is a raw tree (resp. raw pre-tree) in which each
atom occurs at most once. A _cut_ is an unordered pair of trees $C=\langle
T\mathopen{|}S\rangle$ with disjoints sets of atoms. Pre-trees and cuts only
describe the surface level of MELL nets: we also have to introduce promotion
boxes.

We now define _box contexts_ and _pre-nets_ by mutual induction as follows. A
box context $\Theta$ is the data of a finite set
$B_{\Theta}\subset\mathbf{N}$, and of a pre-net of the form
$\Theta(b)=(\Theta_{b};\overrightarrow{C}_{b};T_{b},\overrightarrow{S}^{\circ}_{b};\jmath_{b})$,
for each $b\in B_{\Theta}$. We then write $\mathbf{ar}_{\Theta}(b)$, or simply
$\mathbf{ar}(b)$ for the length of the family
$\overrightarrow{S}^{\circ}_{b}$, which we call the _arity_ of the box $b$. A
pre-net is a tuple
$P^{\circ}=(\Theta;\overrightarrow{C};\overrightarrow{S}^{\circ};\jmath)$
where:

  * •

$\Theta$ is a box context;

  * •

the _jump function_ $\jmath$ is a function
$\mathbf{U}_{-}(\overrightarrow{C},\overrightarrow{S}^{\circ})\to\mathbf{T}(\overrightarrow{C},\overrightarrow{S}^{\circ})$;

  * •

each atom occurs at most once in
$\overrightarrow{C},\overrightarrow{S}^{\circ}$;

  * •

$a^{b}_{i}\in\mathbf{B}(\overrightarrow{C};\overrightarrow{S}^{\circ})$ iff
$b\in B_{\Theta}$ and $0\leq i\leq\mathbf{ar}(b)$;

  * •

$\mathbf{V}(\overrightarrow{C},\overrightarrow{S}^{\circ})$ is closed under
the involution $x\mapsto\overline{x}$.

Then a _net_ is a pre-net of the form
$P=(\Theta;\overrightarrow{C};\overrightarrow{S};\jmath)$, _i.e._ without
auxiliary ports as conclusions. In the following, we may write, e.g.,
$\Theta_{P}$ for $\Theta$ in this case. An example is illustrated in Figure
15.

######  Remark 35.

To be formal, in the definition of a box context $\Theta$, we should also fix
an enumeration of the family $\overrightarrow{S}^{\circ}_{b}$ in $\Theta(b)$.
Indeed, when we write $a_{0}^{b},a_{1}^{b},\dots,a_{\mathbf{ar}(b)}^{b}$ for
the ports of a box $b$, and
$\Theta(b)=(\Theta_{b};\overrightarrow{C}_{b};T_{b},S^{\circ}_{b,1},\dots,S^{\circ}_{b,\mathbf{ar}(b)};\jmath_{b})$
for the contents of the box, we implicitly assume a bijection which maps each
pre-tree $S^{\circ}_{b,i}$ to the auxiliary port $a_{i}^{b}$ of which it is a
premise (which leaves $T$ to be mapped to $a_{0}^{b}$). We prefer to keep this
information implicit in the following, as the notations should allow to
recover it, whenever necessary.

On the other hand, an analogue of Remark 1 applies in this new setting, as
pre-nets and nets should be considered up to some notion of isomorphism
preserving the interface, which amounts to:

  * •

reindexing cuts, so that $\overrightarrow{C}$ is considered as a set;

  * •

reordering premises of $\wn$-links, which accounts for the associativity and
commutativity of the underlying binary contraction;

  * •

renaming atoms and boxes and, simultaneously, changing the enumeration of the
family $\overrightarrow{S}^{\circ}_{b}$ in each box, all this preserving the
duality involution on variables, the partition $\\{a^{b}_{i}\mid
i\in\mathbf{N}\\}_{b\in\mathbf{N}}$ of $\mathbf{B}$, the jump functions, and
the association of each $S^{\circ}_{b,i+1}$ to $a^{b}_{i+1}$.

We still consider this as a form of $\alpha$-equivalence as it only involves
particular renamings of atoms or indices, preserving the rest of the
structure. Again, we keep this quotient implicit whenever possible in the
remaining.

Also, as already mentioned in Remark 2, we rely on jumps to control the
combinatorics of the elimination of evanescent cuts: we need nets to be
equipped with jumps only to ensure that the resource nets in the Taylor
expansion can also be equipped with jumps, that moreover enjoy uniform bounds.
More precisely, we will show that if an MELL net $P$ can be equipped with
$\jmath_{P}$ that satisfies the acyclicity criterion, then each
$p\in\mathcal{T}(P)$ can be equipped with $\jmath_{p}$, satisfying uniform
bounds on $\mathbf{ln}(p)$ and $\mathbf{jd}(p)$ .

The existence of such a jump function $\jmath_{P}$ should be understood as
side condition only: we keep it in the definition of nets by default because
we rely on it everywhere in the following, but in the end we are actually
interested in the compatibility of Taylor expansion with cut elimination for
nets without jumps. And the reader may check that, without jumps, our pre-nets
(up to $\alpha$-equivalence) are essentially the same as, e.g., the in-PS’s
(up to the names of internal ports) defined by de Carvalho [dC16] for his
proof of the injectivity of Taylor expansion.

ax$\wn$$\oc$cutax$\bot$$\wn$$\oc$$\wn$$\wn$$x\ $$\ \overline{x}$$y\ $$\
\overline{y}$$\mu$$\mu^{\prime}$$1$$2$$1$$2$$3$$b$$b^{\prime}$ Figure 15.
Representation of the net
$(\Theta;;\wn(a^{b}_{3}),\wn(a^{b}_{2},a^{b}_{1}),a^{b}_{0};\jmath)$ where
$B_{\Theta}=\\{b\\}$, $\mathbf{ar}(b)=3$ and
$\Theta(b)=(\Theta^{\prime};\langle
a^{b^{\prime}}_{0}\mathopen{|}\mu\rangle;\overline{y},y,a^{b^{\prime}}_{1},\wn(a^{b^{\prime}}_{2});\jmath^{\prime})$
where $B_{\Theta^{\prime}}=\\{b^{\prime}\\}$, $\mathbf{ar}(b^{\prime})=2$,
$\jmath^{\prime}(\mu)=y$ and
$\Theta^{\prime}(b^{\prime})=(\Theta^{\prime\prime};;\overline{x},x,\mu^{\prime};\jmath^{\prime\prime})$
where $B_{\Theta^{\prime\prime}}=\emptyset$ and
$\jmath^{\prime\prime}(\mu^{\prime})=x$. .

Given a pre-net
$P^{\circ}=(\Theta;\overrightarrow{C};\overrightarrow{S}^{\circ};\jmath)$, we
write
$\mathbf{V}(P^{\circ})=\mathbf{V}(\overrightarrow{C};\overrightarrow{S}^{\circ})$,
$\mathbf{T}(P^{\circ})=\mathbf{T}(\overrightarrow{C};\overrightarrow{S}^{\circ})$,
_etc._ We define the _toplevel size_ of MELL pre-nets by
$\mathbf{size}_{0}(P^{\circ})=\\#\mathbf{T}^{\circ}(P^{\circ})$. We write
$0pt(P^{\circ})$ for the maximum level of nesting of boxes in $P^{\circ}$,
_i.e._ the inductive depth in the above definition of pre-nets. The _size_ of
MELL pre-nets includes that of their boxes: we set
$\mathbf{size}(P^{\circ})=\mathbf{size}_{0}(P^{\circ})+\sum_{b\in
B_{\Theta}}\mathbf{size}(\Theta(b))$ — this definition is of course by
induction on $0pt(P^{\circ})$.

Notice that, by the above definition, for all
$\mu\in\mathbf{U}_{-}(\overrightarrow{C},\overrightarrow{S}^{\circ})$,
$\jmath_{P^{\circ}}(\mu)$ must be at the same depth as $\mu$, and cannot be an
auxiliary port.

We extend the switching functions of MLL to $\wn$-links: for each
$T=\wn(T^{\circ}_{1},\dots,T^{\circ}_{n})\in\mathbf{T}(P^{\circ})$,
$I(T)\in\\{T^{\circ}_{1},\dots,T^{\circ}_{n}\\}$, which induces a _$\wn$
-edge_ $T\sim^{P^{\circ},I}_{T}I(T)$. We also consider _box edges_
$a^{b}_{0}\sim^{P^{\circ}}_{b,i}a^{b}_{i}$ for $b\in B_{\Theta}$ and $1\leq
i\leq ar(b)$: w.r.t. paths, a box $b$ behaves like $\mathbf{ar}(b)$ axiom
links having the principal port of the box as a common vertice, and the
content is not considered. Finally, _jump edges_ also include the case of
weakenings: $\mu\sim^{P^{\circ}}_{\mu}\jmath(\mu)$ for
$\mu\in\mathbf{U}_{-}(P^{\circ})$.

We write $\mathbf{P}(P^{\circ},I)$ (resp. $\mathbf{P}(P^{\circ})$) for the set
of $I$-paths (resp. paths) in $P^{\circ}$. We say a pre-net $P^{\circ}$ is
_acyclic_ if there is no cycle in $\mathbf{P}(P^{\circ})$ and, inductively,
each $\Theta(b)$ is acyclic. From now on, we consider acyclic pre-nets only.

###  7.2. Resource nets and Taylor expansion

The Taylor expansion of a net $P$ will be a set of _resource nets_ : these are
the same as the multiplicative nets introduced before, with the addition of
term constructors for $\oc$ and $\wn$. Raw trees are given as follows:

$t\Coloneqq
x\mid\mathbf{1}_{\lambda}\mid\bot_{\mu}\mid\otimes(t_{1},\dotsc,t_{n})\mid\invamp(t_{1},\dotsc,t_{n})\mid\oc_{\lambda^{\prime}}()\mid\wn_{\mu^{\prime}}()\mid\oc(t_{1},\dotsc,t_{n})\mid\wn(t_{1},\dotsc,t_{n}).$

where $x$ ranges in $\mathbf{V}$, $\lambda$ ranges over
$\mathbf{U}_{\mathbf{1}}$, $\mu$ ranges over $\mathbf{U}_{\bot}$,
$\lambda^{\prime}$ ranges over $\mathbf{U}_{\oc}$, $\mu^{\prime}$ ranges over
$\mathbf{U}_{\wn}$, and we require $n\not=0$ in each case. In resource nets,
we extend switchings to $\wn$-links and jumps from weakenings as in MELL nets,
associated with $\wn$-edges and jump edges. Moreover, for each
$t=\oc(t_{1},\dots,t_{n})$, we have _$\oc$ -edges_ $t\sim_{t,t_{i}}t_{i}$ for
$1\leq i\leq n$. Observe that, except for the notation of the root
constructor, the trees $\oc_{\lambda}()$, $\wn_{\mu}()$,
$\oc(t_{1},\dotsc,t_{n})$ and $\wn(t_{1},\dotsc,t_{n})$, are exactly the same
as $\mathbf{1}_{\lambda}$, $\bot_{\mu}$, $\otimes(t_{1},\dotsc,t_{n})$ and
$\invamp(t_{1},\dotsc,t_{n})$ respectively: in particular they induce the same
geometry for paths.

During Taylor expansion, we need to replace a box in a pre-net with an
arbitrary number of approximants of this box. Let us call _box replacement of
arity $n$_ the data $r=(\overrightarrow{s}_{0},\dotsc,\overrightarrow{s}_{n})$
of $n+1$ families of pairwise distinct resource trees
$\overrightarrow{s}_{0},\dotsc,\overrightarrow{s}_{n}$, such that
$\mathbf{A}(s)\cap\mathbf{A}(s^{\prime})=\emptyset$ whenever
$s\in\overrightarrow{s}_{i}$ and
$s^{\prime}\in\overrightarrow{s}_{i^{\prime}}$, and $i\not=i^{\prime}$ or
$s\not=s^{\prime}$. A family $\overrightarrow{r}=(r_{b})_{b\in B}$ of box
replacements such that
$\mathbf{A}(r_{b})\cap\mathbf{A}(r_{b^{\prime}})=\emptyset$ for
$b\not=b^{\prime}\in B$ is _applicable to the pre-term $T^{\circ}$_ if
$\mathbf{A}(T^{\circ})\cap\mathbf{A}(\overrightarrow{r})=\emptyset$ and, for
each $a^{b}_{i}\in\mathbf{B}(T^{\circ})$, $b\in B$ and $r_{b}$ is of arity at
least $i$.

Let $\overrightarrow{r}$ be a $B$-indexed family of box replacements, and
write
$r_{b}=(\overrightarrow{s}^{b}_{0},\dotsc,\overrightarrow{s}^{b}_{n_{b}})$ for
each $b\in B$. Assuming that $\overrightarrow{r}$ is applicable to the tree
$S$ (resp. the pre-tree $S^{\circ}$), the _substitution of
$\overrightarrow{r}$ for the boxes of $S$_ (resp. of $S^{\circ}$) is the tree
$S[\overrightarrow{r}]$ (resp. the family of pre-trees
$S^{\circ}\\{\overrightarrow{r}\\}$) defined by mutual induction on pre-trees
and trees as follows:

$\displaystyle\begin{aligned}
x[\overrightarrow{r}]&=x&\lambda[\overrightarrow{r}]&=\lambda&\mu[\overrightarrow{r}]&=\mu&a^{b}_{0}[\overrightarrow{r}]&=\begin{cases}\lambda_{b}&\text{if
$\overrightarrow{s}^{b}_{0}$ is empty}\\\
\oc(\overrightarrow{s}^{b}_{0})&\text{otherwise}\\\ \end{cases}\end{aligned}$
$\displaystyle\begin{aligned}
\otimes(T_{1},\dotsc,T_{n})[\overrightarrow{r}]&=\otimes(T_{1}[\overrightarrow{r}],\dotsc,T_{n}[\overrightarrow{r}])\\\
\invamp(T_{1},\dotsc,T_{n})[\overrightarrow{r}]&=\invamp(T_{1}[\overrightarrow{r}],\dotsc,T_{n}[\overrightarrow{r}])\\\
\wn(T^{\circ}_{1},\dotsc,T^{\circ}_{n})[\overrightarrow{r}]&=\begin{cases}\mu_{\wn(T^{\circ}_{1},\dotsc,T^{\circ}_{n})}&\text{if
$T^{\circ}_{1}\\{\overrightarrow{r}\\},\dotsc,T^{\circ}_{n}\\{\overrightarrow{r}\\}$