Gluing resource proof-structures: inhabitation and inverting Taylor]Gluing resource proof-structures: inhabitation and inverting the Taylor expansion

G. Guerrieri]Giulio Guerrieri[a]
Huawei Research, Edinburgh Research Centre, Edinburgh, United Kingdom

L. Pellissier]Luc Pellissier[b]
Université Paris Est Créteil, LACL, F-94010 Créteil, France

L. Tortora de Falco]Lorenzo Tortora de Falco[c]
Università Roma Tre, Dipartimento di Matematica e Fisica, Rome, Italy

A Multiplicative-Exponential Linear Logic (MELL) proof-structure can be
expanded into a set of resource proof-structures: its Taylor expansion. We
introduce a new criterion characterizing (and deciding in the finite case) those sets of resource
proof-structures that are part of the Taylor expansion of some MELL
proof-structure, through a rewriting system acting both on resource and MELL
proof-structures.  We also prove semi-decidability of
the type inhabitation problem for cut-free MELL proof-structures.

§ INTRODUCTION

§.§.§ The Taylor expansion

Girard's linear logic (, <cit.>) is a
refinement of intuitionistic and classical logic that isolates the infinitary
parts of reasoning
in two dual modalities: the exponentials $\oc$
and $\wn$.
They give a logical status to operations of memory management such as
copying and erasing: a linear ( exponential-free) proof corresponds—via the
Curry–Howard isomorphism—to a program that uses its argument linearly,
exactly once, while an exponential proof corresponds to a program that can
use its argument at will.

The intuition that linear programs are analogous to linear functions
(as studied in linear algebra) while exponential programs mirror a more general
class of analytic functions
got a technical incarnation in Ehrhard's work <cit.> on $\LL$-based denotational semantics for the $\lambda$-calculus.
This investigation has been then internalized in the syntax, yielding the resource $\lambda$-calculus <cit.>, inspired by <cit.>:
there, copying and erasing are forbidden
and replaced by the possibility to apply a
function to a bag of resource $\lambda$-terms which specifies how many times (in a finite number) an argument can be linearly passed to the function, so as to represent only bounded computations.

The Taylor expansion <cit.> (more precisely, its support; but here and throughout the paper we do not consider the rational coefficients in the Taylor expansion) associates with every ordinary $\lambda$-term a—generally infinite—set of resource $\lambda$-terms, recursively approximating
the usual application: the Taylor expansion of the $\lambda$-term $MN$ is made up
of all resource $\lambda$-terms of the form $t[u_1, \dots, u_n]$, where $t$ is a
resource $\lambda$-term in the Taylor expansion of $M$, and $[u_1,\dots,u_n]$ is
a bag of $n$ (for any $n \geqslant 0$) resource $\lambda$-terms in
the Taylor expansion of $N$.  Roughly, the idea is to decompose a program into a
set of purely “resource-sensitive programs”, all of them containing only bounded (although
possibly non-linear) calls to inputs. The notion of Taylor expansion has had
many applications in the theory of the $\lambda$-calculus,  in the study of
linear head reduction <cit.>, normalization
<cit.>, Böhm trees
$\lambda$-theories <cit.>, intersection
types <cit.>.
In general, understanding the relation
between a program and its Taylor expansion renews the logical approach to the
quantitative analysis of computation started with the inception of .

A natural question is the inverse Taylor expansion problem: Which sets of resource $\lambda$-terms are included in the Taylor expansion of a same $\lambda$-term?
How to characterize them?
Ehrhard and Regnier <cit.> defined a simple coherence binary relation such that a finite set of resource $\lambda$-terms is included in the Taylor expansion of a $\lambda$-term if and only if all the elements
of this set are pairwise coherent. Coherence is crucial in many structural
properties of the resource $\lambda$-calculus, such as in the proof that in the $\lambda$-calculus normalization and Taylor expansion commute <cit.>.

We aim to solve the inverse Taylor expansion problem in the more general context of , more precisely in the multiplicative-exponential fragment $\MELL$ of , being aware that for $\MELL$
no coherence relation can characterize the solutions (see below).
Our characterization is constructive, in that it allows us to define a decision procedure to solve the inverse Taylor expansion problem in the finite case.
A side effect of this investigation is apparently unrelated to the notion of Taylor expansion:
we characterize $\MELL$ formulas that are inhabited by cut-free proof-structures, so as to prove semi-decidability of the type inhabitation problem for cut-free proof-structures (again, see below).

§.§.§ Proof-nets, proof-structures and their Taylor expansion: seeing trees behind graphs

In $\MELL$, linearity and the sharp analysis of computations naturally lead to
represent proofs in a more general graph-like syntax instead of a
term-like or tree-like one.A term-like object is
essentially a tree, with one output (its root) and many inputs (its other
leaves).  Indeed, linear negation is involutive and classical duality can be
interpreted as the possibility of juggling between different conclusions,
without a distinguished output <cit.>.  Graphs representing proofs
in are called proof-nets: their syntax is richer and more
expressive than the $\lambda$-calculus (which corresponds to an intuitionistic implicative fragment of ).
Contrary to $\lambda$-terms, proof-nets
are special inhabitants of the wider land of proof-structures.
A proof-structure is any “graph” that can be build in the language of proof-nets and it need not represent a proof in .
Proof-nets can be characterized, among
proof-structures, by abstract (geometric) conditions called correctness criteria

Proof-structures are well-behaved for performing computations: indeed,
cut-elimination steps can be defined for proof-structures, and proof-nets
can also be seen as the proof-structures with a good behavior with respect to
cut-elimination <cit.>. Furthermore, proof-structures can be
interpreted in denotational models and proof-nets can be characterized among them by semantic means <cit.>.
It is then natural to attack problems in the general framework of proof-structures.
In our work, correctness plays no role at all, hence we will
consider proof-structures and not only proof-nets.
proof-structures are a
particular kind of graphs, whose edges are labeled by $\MELL$ formulas and
vertices  (aka cells) by $\MELL$ connectives, and for which special subgraphs are
highlighted, the boxes, representing the parts of the proof-structure
that can be discarded and copied (called an unbounded number of times) during cut-elimination.
A box is
delimited from the rest of a proof-structure by exponential modalities:
its border is made of one
$\oc$-cell, its principal door, and arbitrarily many $\wn$-cells, its auxiliary
Boxes are either nested or disjoint (they cannot partially overlap),
so as to add a tree-like structure to

As in the $\lambda$-calculus,
one can define box-free resource (or $\DiLL_0$) proof-structures<cit.>, where
Aka differential proof-structures <cit.>, differential nets <cit.>, simple nets <cit.>.
$\oc$-cells make resources available boundedly,
and the Taylor expansion of $\MELL$ proof-structures into these resource proof-structures, that recursively copies the
content of the boxes an arbitrary number of times.
In fact, as somehow anticipated by Boudes <cit.>,
such a Taylor expansion operation can be carried on any tree-like
This primitive, abstract, notion of Taylor expansion can then be pulled back to
the structure of interest (in this case, the resource proof-structures), as shown in <cit.> and put forth again here.

§.§.§ The question of coherence for proof-structures

The inverse Taylor expansion problem has a natural counterpart
for proof-structures: given a set $\Pi$ of resource proof-structures, is there a
$\MELL$ proof-structure the Taylor expansion of which includes $\Pi$?
Pagani and Tasson <cit.> give the following answer: it is possible to
decide whether a finite set of resource proof-structures is a subset of the
Taylor expansion of a same proof-structure (and even possible to do it
in nondeterministic polynomial time); but unlike the $\lambda$-calculus, the structure of the relation “being
part of the Taylor expansion of a same proof-structure” is much more
complicated than a binary (or even $n$-ary) coherence. Indeed, for any $n>1$, it
is possible to find ${n+1}$ resource proof-structures such that any $n$ of them
are in the Taylor expansion of some $\MELL$ proof-structure, but there is no
$\MELL$ proof-structure whose Taylor expansion has all the $n\!+\!1$ as elements
(see our Example <ref> and <cit.>).

In this work, we introduce a new combinatorial criterion, ,
for deciding whether a set of resource proof-structures is a subset of the
Taylor expansion of some $\MELL$ proof structure, based on a rewriting system on lists of $\MELL$ formulas. Our criterion is more general
and simpler than the one of <cit.>, which is limited
to the cut-free case with atomic axioms and characterizes only finite sets: we do not have these limitations.
Akin to <cit.>, our criterion yields a decision procedure for the inverse Taylor expansion problem when the set of resource proof-structures given as input is finite.
We believe that our criterion is a useful tool for studying proof-structures.
We conjecture that it can be used to show that a binary coherence relation exists for resource proof-structures satisfying a suitable geometric restriction.
It might also shed light on correctness and sequentialization.

As the proof-structures we consider are typed, an unrelated difficulty arises: a
resource proof-structure $\rho$ of type $A$ might not be in the Taylor expansion of any cut-free \(\MELL\)
proof-structure, not because it does not respect the structure imposed by the
Taylor expansion, but because
there is no cut-free proof-structure of type $A$, and $\rho$ can
“mask” this “untypeability”.Similarly, in the $\lambda$-calculus, there is no closed $\lambda$-term of type \(X \to Y\) with \(X \neq Y\) atomic, but the resource $\lambda$-term \((\lambda f.f)[\,]\) can be given that type: the empty bag $[\,]$ kills any information on the argument.
To solve this issue, we enrich the resource (but not \(\MELL\)) proof-structure
syntax with a “universal” proof-structure:
a special \(\maltese\)-cell (daimon) that can have any number of outputs of any types,
representing information plainly missing (see <Ref> for more details and the way this matter is handled by Pagani and Tasson <cit.>).

§.§.§ Our contribution

This paper is the long version of <cit.> and we keep its structure and main results: the  criterion that solves the inverse Taylor expansion problem in proof-structures (<Ref>), and the way we prove it, which consists in showing that the Taylor expansion defines a natural transformation (<Ref>) from the realm of resource proof-structures to the realm of proof-structures (see <Ref> for an informal explanation).
With respect to <cit.>, the main novelties are:

* Following <cit.>, we introduce rigorous definitions of all the notions of graph theory (<Ref>) involved in the definition of proof-structures and Taylor expansion.
In this way, we can present here a purely graphical definition of $\MELL$ proof-structures (<Ref>), so as to keep Girard's original intuition of a proof-structure as a graph even in and to avoid ad hoc technicalities to identify the border and the content of a box.
This is not only an aesthetic issue but also practical, in that our proof-structures are manageable: sophisticated operations on them can be easily defined.
For instance, we give an elegant definition of their Taylor expansion by means of pullbacks (<Ref>).

* With respect to <cit.>, here we use daimons in a different and more limited way. In particular, unlike <cit.>, our proof-structures do not contain any $\maltese$-cell.
Thus, our results refer to a more standard and interesting definition of proof-structures,
and we deal with less syntactic categories than in <cit.>, simplifying the presentation and fixing some technical inaccuracies in a few definitions and lemmas in <cit.>.

* Consequently, our results (notably, naturality and )
are more informative, and allow us to decide the inverse Taylor expansion problem  in the finite case (<Ref>).

* We solve the apparently unrelated type inhabitation problem for cut-free proof-structures (<Ref>), not considered in <cit.>:
our rewrite system semi-decides if, for a list $\Gamma$ of formulas, there is a cut-free proof-structure of type $\Gamma$.
We only provide a semi-algorithm: we can guess a rewriting and check its correctness; but there is no bound on its length.
Inhabitation problems are well-studied in many type systems for the $\lambda$-calculus, but 	no results are in the literature for proof-structures.
Our contribution may shed some light on the open problem of decidability of .

* Akin to <cit.>, to simplify the presentation, we first focus on proof-structures restricted to atomic axioms, then <Ref> shows how to lift our results to the non-atomic case.
Compared to <cit.>, the lift is more elegant and requires less

§ OUTLINE AND TECHNICAL ISSUES

§.§.§ Rewriting

The essence of our rewrite system is not located
in proof-structures but in
lists of formulas (Definition <ref>).
Roughly, the rewrite system is
generated by elementary steps akin to rules of sequent calculus read from the
bottom up: they act on a list of conclusions, analogous to a monolaterous
right-handed sequent.
These steps can be seen as morphisms in a category $\Scheduling$ whose objects are lists of formulas, and are actually more sequentialized than sequent
calculus rules, as they do not allow for commutation. For instance, the
rule corresponding to the introduction of a $\otimes$ on the $i$th formula, is
defined as
$\otimes_i : (C_1,\dots,C_{i-1},A\otimes B, C_{i+1}, \dots,
C_n) \to (C_1,\dots,C_{i-1},A, B, C_{i+1}, \dots,

\vspace{\beforepn}
\tikzsetnextfilename{images/mell-tensor-intro-1}
\pnet{
\pnformulae{
\pnf[A]{$A$}~\pnf[Ab]{$A^{\bot}$}
\pnaxiom[ax]{A,Ab}
\pntensor{A,Ab}[i]{$A \otimes A^{\bot}$}
\pnrewrite[\otimes_1]
\tikzsetnextfilename{images/mell-tensor-intro-2}
\pnet{
\pnformulae{
\pnf[A]{$A$}~\pnf[Ab]{$A^{\bot}$}
\pnaxiom[ax]{A,Ab}

These rewrite steps then act on $\MELL$ proof-structures, coherently with
their type, by modifying (most of the times, erasing) a cell immediately above the conclusion of the proof-structure.
Formally, this means that there is a functor $\MELLFunctor$ from $\Scheduling$ to the category $\Rel$ of sets and relations, associating with
every list of formulas the set of proof-structures with these conclusions, and with
every rewrite step a relation implementing it (Definition <ref>).
The rules deconstruct the proof-structure, starting from its conclusions. The rule
$\otimes_1$ acts by removing a $\otimes$-cell on the first conclusion, replacing
it by two conclusions.

These rules can only act on specific proof-structures, and indeed, capture a lot
of their structure: $\otimes_i$ can be applied to a proof-structure $R$ if and
only if $R$ has a $\otimes$-cell in the conclusion $i$ (as opposed to, say, an
axiom). So, in particular, every proof-structure is completely characterized by
any sequence rewriting it to the empty proof-structure.

§.§.§ Naturality

The same rules also act on sets of resource (aka $\DiLL_0$) proof-structures, defining the
functor $\PPolyPN$ from the category $\Scheduling$ of rewrite steps into the category $\Rel$
(Definition <ref>). When carefully defined, the Taylor expansion induces
a natural transformation from $\PPolyPN$ to $\MELLFunctor$
(<Ref>). By applying this naturality repeatedly, we get
our characterization (<Ref>): a set of resource
proof-structures $\Pi$ is a subset of the Taylor expansion of a $\MELL$
proof-structure if and only if $\Pi$ is , that is, there is a sequence rewriting $\Pi$ to the singleton of
the empty proof-structure.

The naturality property is not only a mean to obtain our characterization, but also an interesting result in itself: natural transformations can often be used to express fundamental properties in a mathematical context.
In this case, the Taylor expansion is natural with respect to the
possibility of building a (\(\MELL\) or resource) proof-structure by adding a
cell to its conclusions or boxing it.
Said differently, naturality of the Taylor expansion roughly means that the rewrite rules that deconstruct a proof-structure $R$ and a set of resource proof-structures in the Taylor expansion of $R$ mimic each other.

§.§.§ Quasi-proof-structures and mix

Our rewrite rules consume proof-structures from their conclusions. The rule
corresponding to boxes in $\MELL$ opens a box by deleting its principal door (a
$\oc$-cell) and its border, while for a resource proof-structure
it deletes a $\oc$-cell and separates the different copies of the content of the box (possibly) represented by such a $\oc$-cell.
This operation is problematic in a twofold way.
In a resource proof-structure, where the border of boxes is not marked, it is not clear how to identify such copies.
On the other side, in a $\MELL$ proof-structure the content of a box is not to be treated as if it were at the same level as what is outside of the box:
it can be copied many times or erased, while what is outside boxes cannot,
and treating the content in the same way as the outside suppresses this
distinction, which is crucial in .
So, we need to remember that the content of a box, even if it is at depth $0$ (not contained in any other box) after erasing the box wrapping it by means of our rewrite rules,
is not to be mixed with the rest of the structure
at depth $0$.

\vspace{\beforepn}
\tikzsetnextfilename{images/root}
\pnet{
\pnsomenet[u]{$\pi$}{1.25cm}{0.5cm}
\pnoutfrom{u.-140}[pi1c]{$\qquad \ \!\!\cdots$}
\pnoutfrom{u.-40}[u2a2]{$\quad$}
\pnsemibox{u}

In order for our proof-structures to provide this information,
we need to generalize them and consider that a proof-structure can have
a forest of boxes, instead of just a tree: this yields the notion of
quasi-proof-structure (Definition <ref>).
In this way, according to our rewrite rules, opening a box by deleting its principal door amounts to taking a
box in the tree and disconnecting it from its root, creating a new tree. We draw
this in a quasi-proof-structure by surrounding each component—made of the objects having the same root—with a dashed line,
open from the bottom, remembering the phantom presence of the border of the box,
even if it was erased.
This allows one to open the box only when it is alone in a component, just surrounded by a dashed line
(Definition <ref>).

This is not merely a technical remark, as this generalization gives a status to
the $\Mix$ rule of : indeed, mixing two proofs amounts to taking two proofs
and considering them as one, without any other modifications. Here, it amounts to
taking two proof-structures, each with its box-tree, and considering them as one by
merging the roots of their trees (see the mix step in Definition <ref>).
We embed this design decision up to the level of formulas, which are segregated
in different zones that have to be mixed before interacting.

Indeed, our rewrite rules actually act on conclusions arranged as a list of lists of formulas.

§.§.§ Geometric invariance and emptiness: the filled Taylor expansion

The use of forests instead of trees for the nesting structure of boxes, where
the different roots are thought of as the contents of long-gone boxes, has an
interesting consequence in the Taylor expansion: indeed, an element of the
Taylor expansion of a proof-structure contains an arbitrary number of copies of
the contents of the boxes, in particular zero. If we think of the part at
depth $0$ of a $\MELL$ proof-structure as inside an invisible box, its content
can be deleted in some elements of the Taylor expansion just as any other
box.The dual case, of copying the contents of a box, poses no problem
in our approach.
As erasing completely the conclusions would
cause the Taylor expansion not preserve the conclusions (which would lead to
technical complications), we introduce the filled Taylor expansion
(Definition <ref>), which contains not only the elements of the usual
Taylor expansion, but also elements of the Taylor expansion where one component
has been erased and replaced by a \(\maltese\)-cell (daimon), representing lack of information, apart from the number and types of the conclusions.
Roughly, a $\maltese$-cell is a placeholder for any $\DiLL_0$ proof-structure of given conclusions.

§.§.§ and cut-free

Our criterion is based on local rewritings, which yields a geometric and modular approach to the inverse Taylor expansion problem. From the geometric point of view, there is nothing special in the elementary rewrite step corresponding to the cut rule, and it is natural to prove our criterion in presence of cuts (<Ref>.<ref>).
But from the proof-theoretical point of view, the gulf separating cut-free proof-structures from the others shows up: for every formula $A$, the set of $\MELL$ proof-structures with conclusion of type $A$ is never empty, while this might very well be the case if we restrict to cut-free $\MELL$ proof-structures (see Example <ref> and Remark <ref>). The modularity of our proofs allows to straightforwardly adapt the criterion to the cut-free case (<Ref>.<ref>) and thus to state correctly (and easily solve) the type inhabitation problem for (cut-free) $\MELL$ proof-structures (<Ref>).

§.§.§ Outline

<Ref> recalls some preliminary notions on graph theory.
In <Ref> we define (and $\DiLL_0$) proof-structures and quasi-proof-structures with atomic axioms.
<Ref> defines the notion of Taylor expansion.
<Ref> introduces the rewriting rules on lists of lists of formulas and lifts them to quasi-proof-structures via the functor $\MELLFunctor$.
In <Ref> we lift the rewriting rules to $\DiLL_0$ quasi-proof-structures via the functor $\PPolyPN$ and we show our first main result: the Taylor expansion induces a natural transformation between the two functors.
<Ref> proves two other main results: the solution of the inverse Taylor expansion problem (via a criterion) and the solution of the  type inhabitation problem in .
<Ref> proves that the inverse Taylor expansion problem is decidable in the finite case.
In <Ref> we show how to adapt our method when axioms are not necessarily atomic.
<Ref> concludes with some final remarks.

§ PRELIMINARIES ON GRAPHS

§.§.§ Graphs with half-edges.

There are many formalizations of the familiar notion of graph.
Here we adopt the one due to <cit.>:The folklore attributes the definition of graphs
with half-edges to Kontsevitch and Manin, but the idea can actually be traced
back to Grothendieck's dessins d'enfant.
a graph is still a set of edges and a set of vertices,
but edges are now split in halves, allowing some of them to be hanging.
Splitting every edge in two has at least four features of particular interest to represent proof-structures:

* two half-edges are connected by an involution, thus defining an edge linking two vertices (possibly the same vertex).
The fixed points of this involution are “hanging” edges,
linked to a vertex only on one endpoint:
they are well suited for representing the conclusions of a proof-structure.
In this way it is also easy to define some intuitive but formally tricky operations such as
grafting/substituting a graph into/for another graph (see Example <ref>);

* given any vertex $v$ in a graph $\tau$, it is natural to
define the corolla of $v$, that is $v$ itself with
the half-edges linked to it; $\tau$ is the union of its corollas, glued together by the involution;

* while studying proof-structures, it is often necessary to treat
them both as directed and undirected graphs.
With this definition of graph, an orientation, a labeling and a coloring, are structures on top of the structure of the undirected graph (see Definition <ref>);

* this definition of graph allows
a uniform syntax to represent both proof-structures and other structures of interest (, the box-tree of a proof-structure).
In this way, we avoid appealing to ad hoc conditions in the definitions of proof-structure and Taylor expansion, which are then more compact and rely only on notions from graph theory.

A (finite)
The finiteness condition on $F_\tau$ and $V_\tau$ can be dropped, so as to allow for possibly infinite graphs. We require it because we only deal with finite graphs.
graph  is a quadruple
$\tau = (F_{\tau}, V_{\tau}, \partial_{\tau}, j_{\tau})$, where

* $F_{\tau}$ is a finite set, whose elements are called flags of

* $V_{\tau}$ is a finite set, whose elements are called vertices of

* $\partial_{\tau} \colon F_{\tau} \to V_{\tau}$ is a function associating with
each flag its endpoint;

* $j_{\tau} \colon F_{\tau} \to F_{\tau}$ is an involution, $(j_{\tau} \circ j_{\tau}) (f) = f$ for every $f \in F_{\tau}$.

The graph $\tau  = (F_{\tau}, V_{\tau}, \partial_{\tau}, j_{\tau})$ is [empty graph]empty if $V_{\tau} = \emptyset$.This implies that $\partial_{\tau}$ is the empty function and $F_{\tau} = \emptyset$ (since $F_\tau$ is the domain of $\partial_\tau$).

A subgraph of a graph $\tau = (F_{\tau}, V_{\tau}, \partial_{\tau}, j_{\tau})$ is a graph $\sigma = (F_{\sigma}, V_{\sigma}, \partial_{\sigma}, j_{\sigma})$ where $F_\sigma \subseteq F_{\tau}$, $V_\sigma \subseteq V_{\tau}$, $\partial_\sigma = \partial_{\tau} \mathord{\upharpoonright}_{F_\sigma}$, and, for all $f \in F_\sigma$, $j_\sigma(f) = j_{\tau}(f)$ if $j_{\tau}(f) \in F_\sigma$, otherwise $j_\sigma(f) = f$.

In a graph $\tau  = (F_{\tau}, V_{\tau}, \partial_{\tau}, j_{\tau})$, a tail of $\tau$ is a fixed point of the involution $j_\tau$,  a flag $f = j_\tau(f)$.
A set $\{f,f'\}$ of two flags with $j_\tau(f) = f' \neq f$ is an edge of
$\tau$ between vertices $\partial_{\tau}(f)$ and $\partial_{\tau}(f')$;
$f, f'$ are the halves of the edge;
if $\partial_{\tau}(f) = \partial_{\tau}(f')$ then the edge is a loop.

Given two graphs $\tau$ and $\tau'$, it is always possible to consider their
disjoint union $\tau \sqcup \tau'$ defined as the disjoint union of the
underlying sets and functions.

A one-vertex graph with set of flags $F$ and
involution the identity function $\id_F$ on $F$ is called a corolla
(the endpoint of each flag is the only vertex); it is usually denoted by $\ast_F$.

Given a graph $\tau = (F_{\tau}, V_{\tau}, \partial_{\tau}, j_{\tau})$, a vertex
$v \in V_{\tau}$ defines a corolla
$\tau_v = (F_v, \{v\}, \allowbreak \partial_{\tau}|_{F_v}, \allowbreak\id_{F_v})$ where $F_v = \partial_{\tau}^{-1}(v)$.
A graph $\tau$ can be seen as the disjoint union of the corollas of its vertices, and the involution gluing some flags (the ones that are not tails in $\tau$) in edges.

[graph morphism and isomorphism]

Let $\tau, \sigma$ be two graphs. A graph morphism
$h \colon \tau \to \sigma$
from $\tau$ to $\sigma$ is a couple of functions $(h_F \colon F_{\tau} \to F_{\sigma}, h_V \colon V_{\tau} \to
V_{\sigma})$ such that $h_V \circ \partial_{\tau} = \partial_{\sigma} \circ
h_F$ and $h_F \circ j_{\tau} = j_{\sigma} \circ h_F$ ($h_F$ and $h_V$ are the components of $h$).

A graph morphism is [empty graph morphism]empty ( an [identity graph morphism]identity) if
its components are empty ( identity) functions.
A graph isomorphism is a graph morphism whose components are bijective.

Intuitively, a graph morphism preserves tails and edges.
The category $\Graph$ $\Graph$ has graphs as objects and graph morphisms as arrows:
indeed, graph morphisms compose in a associative way (by composing their components) and identity graph morphisms are neutral for such a composition.
$\Graph$ is a monoidal category, with disjoint union as a monoidal product.

§.§.§ Graphs with structure.

Some structures can be put on top of a graph.
[structured graph]

Let $\tau = (F_\tau, V_\tau, \partial_\tau, j_\tau)$ be a graph.

* A labeled graph $(\tau,\ell_\tau)$ with labels in $L$ is a graph
and a function $\ell_\tau \colon V_{\tau} \to L$.

* A colored graph $(\tau,\FlagType_\tau)$ with colors in $C$ is a graph $\tau$ and a function $\FlagType_\tau \colon F_{\tau} \to C$ such that $\FlagType_\tau(f) = \FlagType_\tau(f')$ for the two halves $f,f'$ of any edge of $\tau$.

* A directed graph $(\tau, \Orient_\tau)$ is a graph $\tau$
and a function $\Orient_\tau \colon F_{\tau} \to \{\In, \Out\}$ such that $\Orient_\tau(f) \neq \Orient_\tau(f')$ for the two halves $f,f'$ of any edge of $\tau$.
If $\Orient_\tau(f) = \Out$ and $\Orient_\tau(f') = \In$, $\{f,f'\}$ is said an edge of $\tau$ from $\partial_{\tau}(f)$ to $\partial_{\tau}(f')$;
$\In$-oriented ($\Out$-oriented) tails of $\tau$ are called inputs (resp. outputs) of $\tau$;
if $v$ is a vertex of $\tau$,
the inputs (outputs) of $v$ are the elements of the set
$\In_{\tau}(v) = \partial_{\tau}^{-1}(v) \cap \mathsf{o}_\tau^{-1}(\In)$
(resp. $\Out_{\tau}(v) = \partial_{\tau}^{-1}(v) \cap \mathsf{o}_\tau^{-1}(\Out)$).

* An ordered graph $(\tau,<_{\tau})$ is a graph $\tau$ together
with an order $<_{\tau}$ on its flags.

Different structures on a graph $\tau$ can combine modularly, for instance $\tau$ can be endowed with a labeling $\VertType_{\tau}$ and an orientation $\Orient_{\tau}$, so as to form a directed labeled graph $(\tau, \Orient_{\tau}, \VertType_{\tau})$; and conversely, a directed labeled graph $(\tau, \Orient_{\tau}, \VertType_{\tau})$ can be seen as a directed graph $(\tau, \Orient_{\tau})$, forgetting the labeling $\VertType_{\tau}$.
Roughly, a graph is labeled ( colored) when labels are associated with its vertices (edges and “hanging” edges).
In a directed graph, an input ( output) of a vertex $v$ is a—half or hanging—edge incoming in ( outgoing from) $v$.

Graphs can be depicted in diagrammatic form, vertices are represented by small rounded boxes and flags by wires touching their endpoint.
As a graph is just a
disjoint union of corollas glued by the involution, we only need to
depict corollas (<Ref>, on the left) and place the two halves of an edge next to each other (<Ref>, on the right).
In directed graphs, inputs of a corolla are depicted above the corolla,
outputs below; arrows also show their orientation.
The color of a flag $f$ (if any) is written next to $f$.
The label of a vertex $v$ (if any) is written inside $v$.
If ordered, flags of a corolla are depicted increasing from left to right.
A dotted gray wire denote an arbitrary number (possibly $0$) of flags (see <Ref>).

The directed labeled colored ordered corolla $\mathbf{5} = (\ast_{\mathbf{5}}, \Orient_\mathbf{5}, \VertType_\mathbf{5}, \FlagType_\mathbf{5}, <_{\mathbf{5}})$ depicted in <Ref> (on the left) has $\ast$ as its only vertex and $F_\mathbf{5} = \{0, 1, 2, 3, 4\}$ as its set of flags;
it is endowed with the order $0 <_{\mathbf{5}} 4$ and $1 <_{\mathbf{5}} 2 <_{\mathbf{5}} 3$,
the labeling
$\VertType_\mathbf{5}(\ast) = \maltese$, the orientation $\Orient_\mathbf{5} \colon F_\mathbf{5} \to \{\In, \Out\}$ defined by
$\Orient_\mathbf{5}(0) = \Orient_\mathbf{5}(4) = \Out$ and $\Orient_\mathbf{5}(1) = \Orient_\mathbf{5}(2) = \Orient_\mathbf{5}(3) = \In$,
the coloring $\FlagType_\mathbf{5} \colon F_\mathbf{5} \to \{A_0,\ldots,A_4\}$  defined by $\mathsf{c}(i) = A_i$ for all $i \in F_\mathbf{5}$.

Let $\sigma_{\ax}$ be the directed labeled colored corolla, whose only vertex is labeled by $\ax$, and whose only flags are the outputs $5$ (colored by $A_2$) and $6$ (colored by $A_3$).
The directed labeled colored ordered two-vertex graph $\rho$
in <Ref> (on the right) is
obtained by “grafting” $\sigma_{\ax}$ into $\mathbf{5}$,  from $\sigma_{\ax}$ and $\mathbf{5}$	by defining the involution $j_{\rho} \colon \{0, \dots, 6\} \to \{0, \dots, 6\}$ as $j_{\rho}(i) = j_{\mathbf{5}}(i)$ for $i \in \{0,1,4\}$, and $j_{\rho}(i) = i+3$ for $i \in \{2,3\}$, and $j_{\rho}(i) = i-3$ for $i \in \{5,6\}$.

Each enrichment of the graph structure introduced in Definition <ref>
induces a notion of structure-preserving morphism (and isomorphism) that extends the notion of graph morphism (and graph isomorphism) seen in Definition <ref>, so as to form an associated category.
Moreover, different kinds of structure preservation can be combined in a modular way.
For instance, given two directed labeled graphs $(\tau, \Orient_\tau, \VertType_\tau)$ and $(\sigma, \Orient_\sigma, \VertType_\sigma)$ both with labels in $L$,
(in particular, they can be seen as two directed graphs $(\tau, \Orient_\tau)$ and $(\sigma, \Orient_\sigma)$, forgetting labels),
a directed graph morphism $h \colon (\tau, \Orient_\tau) \to (\sigma, \Orient_\sigma)$ is a graph morphism $h =(h_F, h_V) \colon \tau \to \sigma$ such that $\Orient_\sigma \circ h_F = \Orient_\tau$;
this means that $h_F$ maps input ( output) flags of $\tau$ to input ( output) flags of $\sigma$.
And a directed labeled isomorphism $h \colon (\tau, \Orient_\tau, \VertType_\tau) \to (\sigma, \Orient_\sigma, \VertType_\sigma)$ is a graph isomorphism $h =(h_F, h_V) \colon \tau \to \sigma$ such that $\Orient_\sigma \circ h_F = \Orient_\tau$ and $\VertType_\sigma \circ h_V = \VertType_\tau$.

$\mathbf{5} \ = \ $

$\rho \ = \ $

A directed labeled colored ordered corolla $\mathbf{5}$ (left), and a directed labeled colored ordered two-vertex graph $\rho$ (right), see Example <ref>.

§.§.§ Trees and paths.

An undirected path on a graph $\tau$ is a finite sequence of flags $\varphi = (f_1, \dots, f_{2n})$ for some $n \in \Nat$ such that, for all
$1 \leqslant i \leqslant n$, $j_\tau(f_{2i-1}) = f_{2i} \neq f_{2i-1}$ and (if $i \neq n$) $\partial_\tau(f_{2i}) = \partial_\tau (f_{2i+1})$ with $f_{2i} \neq f_{2i+1}$.
We say that $\varphi$ is between $\partial_\tau(f_1)$ and $\partial_\tau(f_{2n})$ if $n > 0$ (and it is a cycle if moreover $\partial_\tau(f_1) =\partial_\tau(f_{2n})$), otherwise it is the empty (undirected) path, which is between any vertex and itself; the [path length]length of $\varphi$ is $n$.
Note that $\varphi$ cannot cross any tail of $\tau$.
Two vertices in a graph are connected if there is an undirected path between them.

Let $\tau$ be a graph: $\tau$ is connected if any vertices $v, v' \in V_\tau$ are connected;
a connected component of $\tau$ is a maximal (with respect to the inclusion of flags and vertices) connected subgraph of $\tau$;
$\tau$ is acyclic (or a forest) if
it has no cycles;
$\tau$ is a tree if it is a connected forest.
Note that a forest can be seen as a non-empty finite sequence of trees, each tree is a connected component;
so, an empty forest can be seen as a non-empty finite sequence of [empty graph]empty trees.

A rooted tree $\tau$ is a [empty graph]non-empty directed tree such that each vertex has exactly one output.
So, by finiteness, $\tau$ has exactly one output tail $f$: the endpoint of $f$
is called the root of $\tau$.

Let $\tau$ and $\tau'$ be two rooted trees, and $h \colon \tau \to \tau'$ be
a directed graph morphism.
As $h_F$ preserves tails and orientation, $h_V$ maps the root of $\tau$ to the root of $\tau'$.
Rooted trees and directed graph morphisms over them form a category $\RootedTree$.

A directed path on a directed graph $\tau$ is an undirected path $\varphi = (f_1, \dots, f_{2n})$ for some $n \in \Nat$ where $f_{2i-1}$ is output and $f_{2i}$ is input for all $1 \leqslant i \leqslant n$.
We say that $\varphi$ is from $\partial_\tau(f_1)$ to $\partial_\tau(f_{2n})$ if $n > 0$; otherwise it is the empty (directed) path,
from any vertex to itself.

The set of directed paths on a directed tree $\tau$ is finite.
As such, we define the reflexive-transitive closure, or free category,
$\tau^{\circlearrowleft}$ of $\tau$ as the directed graph with same vertices and same tails as $\tau$, and with an edge from $v$ to $v'$ for any directed path from $v$ to $v'$ in $\tau$.
The operator $(\cdot)^\circlearrowleft$ lifts to a functor from the category $\RootedTree$ to the category of directed graphs,
so for every morphism $f$ in $\RootedTree$, $f^\circlearrowleft$ is a directed graph morphism between directed graphs.

§.§.§ Pullback in the category of graphs

The category of graphs has all pullbacks, a fact that we use extensively. We
recall here all the
definitions and facts involved in that affirmation.

Let \(\catC\) be a category. Let \(X\), \(Y\), \(Z\) be  objects of
\(\catC\), and $f \colon X \to Z$ and $g \colon Y \to Z$ be arrows of $\catC$.
A pullback of
$f$ and $g$ is the triple $(P,\oc_X,\oc_Y)$ where $P$ is an object of $\catC$ and $\oc_X \colon P \to X$ and $\oc_Y \colon P \to Y$ are arrows of $\catC$ such that diagram (<ref>)
commutes and, for any $(Q, h \colon Q \to X, k \colon Q \to Y)$ making the same
diagram commute, there is a unique arrow $u \colon Q \to P$ factorizing $h$ and $k$, such that diagram (<ref>) commutes.

\begin{align}\label{eq:pullback}
\begin{tikzcd}
P \ar[r,"\oc_X"] \ar[d,swap,"\oc_Y"]
\&
X 	\ar[d,"f"]
\\
Y  \ar[r,"g"]
\&
\end{tikzcd}
\end{align}

\begin{align}\label{eq:pullback-universal}
\begin{tikzcd}
\arrow[bend left]{drr}{h}
\arrow[bend right,swap]{ddr}{k}
\arrow[dashed]{dr}
{u} \& \&
\\[-15pt]
\& P \arrow{r}{\oc_X} \arrow{d}[swap]{\oc_Y}
\& X \arrow{d}{f}
\\
\& Y \arrow{r}{g}
\& Z
\end{tikzcd}
\end{align}

\begin{align}\label{eq:pullback-corner}
\begin{tikzcd}
X \!\times_Z \! Y \ar[r,"\oc_X"] \ar[d,swap,"\oc_Y"]
\arrow[dr, phantom, "\scalebox{1.5}{$\lrcorner$}" , very near start, color=black]
\&
X 	\ar[d,"f"]
\\
Y  \ar[r,"g"]
\&
\end{tikzcd}
\end{align}

A pullback $(P, \oc_X, \oc_Y)$ of $f \colon X \to Z$ and $g \colon Y \to Z$ is unique (up to unique isomorphism); $P$ is usually denoted by $X \times_Z Y$ (leaving $f,g$ implicit) and depicted like in diagram (<ref>).

All pullbacks exist in the category $\Graph$ of graphs. Let us show it explicitly.
Let \(\tau = (F_{\tau}, V_{\tau}, \partial_{\tau}, j_{\tau})\), \(\sigma = (F_{\sigma},
V_{\sigma}, \partial_{\sigma}, j_{\sigma})\) and \(\rho = (F_{\rho}, V_{\rho},
\partial_{\rho}, j_{\rho})\) be graphs, and let $g = (g_F, g_V) \colon \sigma \to \tau$ and $h = (h_F, h_V) \colon \rho \to \tau$ be graph morphisms.
Consider the sets

\begin{align*}
F &= \left\{ (f_\sigma, f_\rho) \in F_{\sigma} \times F_{\rho} \mid g_F(f_\sigma) = h_F(f_\rho)
\right\}
& \
V &= \left\{ (v_\sigma, v_\rho) \in V_{\sigma} \times V_{\rho} \mid g_V(v_\sigma) = h_V(v_\rho)
\right\}.
\end{align*}

They are both equipped with their natural projections
$\pi_{\sigma}^F \colon F \to F_\sigma$, $\pi_{\rho}^F \colon F \to F_\rho$ and $\pi_{\sigma}^V \colon V \to V_\sigma$, $\pi_{\rho}^V \colon V \to V_\rho$.
Let $f\in F$.

\begin{align*}
(g_V \circ \partial_{\sigma}\circ \pi_{\sigma}^F) (f)
&= (\partial_{\tau} \circ g_F \circ \pi_{\sigma}^F) (f)
\quad\text{because \(g\) is a graph morphism}\\
&= (\partial_{\tau} \circ h_F \circ \pi_{\rho}^F) (f) \quad\text{by definition of
\(F\)}\\
&= (h_V \circ \partial_{\rho} \circ \pi_{\rho}^F)(f) \quad\text{because \(h\) is a
graph morphism.}
\end{align*}

Hence, we can define $\partial \colon F \to V\) by \(\partial (f) =
((\partial_{\sigma}\circ \pi_{\sigma}^F) (f), (\partial_{\rho} \circ
\pi_{\rho}^F)(f))$. In the same way, we define $j \colon F \to F\) by \(j(f) =
((j_{\sigma} \circ \pi_{\sigma}^F)(f), (j_{\rho} \circ \pi_{\rho}^F)(f))$, and
check that it is an involution.

Thus, \(\sigma \times_{\tau} \rho = (F,V,\partial,j)\) is a graph\footnotemark
\footnotetext{Note that if $\sigma$ or $\rho$ is the \kl{empty graph}, then so is $\sigma \times_{\tau} \rho$, and $\pi_\sigma$ and $\pi_\rho$ are \kl{empty graph morphisms}.}
and \(\pi_{\sigma} = (\pi_{\sigma}^F, \pi_{\sigma}^V) \colon \sigma \times_{\tau} \rho \to \sigma\) and
\(\pi_{\rho} = (\pi_{\rho}^F, \pi_{\rho}^V) \colon \sigma \times_{\tau} \rho \to \rho\) are graph morphisms  such that diagram \eqref{eq:pullback-graph} below commutes.
\begin{center}
\begin{minipage}{0.3\textwidth}
\begin{align}\label{eq:pullback-graph}
\begin{tikzcd}
\sigma \!\times_{\tau}\! \rho \ar[r,"\pi_\sigma"] \ar[d,swap,"\pi_\rho"]
\&
\sigma  \ar[d,"g"]
\\
\rho 	\ar[r,"h"]
\&
\tau
\end{tikzcd}
\end{align}
\end{minipage}
\qquad\qquad
\begin{minipage}{0.3\textwidth}
\begin{align}\label{eq:pullback-graph-universal}
\begin{tikzcd}
\mu \ar[r,"p"] \ar[d,swap,"q"]
\&
\sigma  \ar[d,"g"]
\\
\rho 	\ar[r,"h"]
\&
\tau
\end{tikzcd}
\end{align}
\end{minipage}
\end{center}

\noindent Consider now any graph $\mu = (F_{\mu},V_{\mu},\partial_{\mu},j_{\mu})$ and graph morphisms $p = (p_F, p_V) \colon \mu \to \sigma$ and $q = (q_F, q_V) \colon \mu \to \rho$ such that diagram \eqref{eq:pullback-graph-universal} above
commutes. For every $f\in F_{\mu}\), let \(r_F(f) = (p_F(f),q_F(f))$, and for every
\(v\in V_{\mu}\), let $r_V(v) = (p_V(v),q_V(v))$.
It is easy to check that it defines a
graph morphism $r = (r_F, r_V) \colon \mu \to \sigma \times_{\tau} \rho$ that is the unique one to factorize $p$ and $q$.
Therefore, $(\sigma \times_{\tau} \rho, \pi_\sigma, \pi_\rho)$ is the pullback of $g$ and $h$.

Roughly, the pullback $\sigma \times_\tau \rho$ is obtained as a sort of ``lax intersection'' of the ``similar'' vertices of $\sigma$ and $\rho$ (they are ``similar'' when they are sent to the same vertex in $\tau$, by $g_V $ and $h_V$ respectively), and keeping whatever flags that are in the ``intersection''.
So, $\sigma \times_\tau \rho$ is the maximal graph that is ``compatible'' with both $\sigma$ and $\rho$.

The pullback construction lifts to directed, labeled, colored and ordered graphs.

% !TEX root = mainFinal.tex
\section{\MELL proof-structures and quasi-proof-structures}
\label{sect:proof-nets}

We present here a purely graphical definition of $\MELL$ proof-structures,
following the non-inductive approach of \cite{Wollic}: a \MELL proof-structure $R$ is essentially a labeled directed graph $|R|$ together with some additional information to identify its boxes.
Our definition is completely based on standard notions (recalled in \Cref{sect:graphs}) from graph theory: it is formal (with an eye towards complete computer formalization) but avoids \emph{ad hoc} technicalities to identify boxes.
Indeed, the inductive and ordered structure of the boxes of $R$ is recovered by means of a tree $\TreeT_{R}$ and a graph morphism  $\BoxFunction_{R}$ from $|R|$ to $\TreeT_{R}$ which allows us to recognize the content and the border of all boxes in $R$.
We use $n$-ary vertices of type $\wn$ collapsing weakening, dereliction and contraction (like in \cite{DanosRegnier95}).
In this way, we get a \emph{canonical} representation of \MELL proof-structures with respect to operations like associativity and commutativity of contractions, or neutrality of weakening with respect to contraction.

One of the benefits of our purely graphical definition of proof-structure is that notions involving proof-structures such as isomorphism (see below), Taylor expansion (see \Cref{sect:taylor}) and correctness graph (see \cite{Wollic}) can be defined rigorously by means of standard (and not \textit{ad hoc}) mathematical tools from graph theory, making them more ``manageable''.

\subsection{\texorpdfstring{$\MELL$}{MELL} formulas and lists}
\label{subparagraph:Formulas}

Given a countably infinite set of propositional variables $X, Y, Z, \dots$,
\intro{\(\MELL\) formulas} are defined by the following inductive grammar:
\begin{equation*}
\label{eq:formula}
A,B \Coloneqq X \mid X^\bot \mid \one \mid \bot \mid A
\otimes B \mid A \parr B \mid \oc A \mid \wn A
\qquad \text{(set: } \Formulas_{\MELL}\text{)}
\end{equation*}

\intro{Linear negation} $(\cdot)^\bot$ is defined via De Morgan laws $\one^\bot = \bot$,
$(A \otimes B)^\bot = A^\bot \parr B^\bot$ and $(\oc A)^\bot = \wn A^\bot$, so as to
be involutive, \ie{} $A^{\bot\bot} = A$ for any $\MELL$ formula $A$ (we say that $A$ and $A^\bot$ are \intro{dual}).
Variables and their negations are \intro{atomic} formulas; $\otimes$ and $\parr$ (resp.~$\oc$ and $\wn$) are \emph{multiplicative} (resp.~\intro{exponential}) \intro{connectives}; $\one$ and $\bot$ are  (\emph{multiplicative}) \intro{units}.

We call any finite sequence a \emph{list}.
The \intro{empty list} is denoted by~$\emptylist$.
A list $(x_1, \dots, x_n)$ with $n \!>\! 0$ and $x_i \!= \emptylist$ for all $1 \!\leqslant\! i \!\leqslant\! n$ is denoted by $n \emptylist$ or $\emptylists$.
Note that a list $\emptylists$ is not empty.

%For a list $\Gamma = (A_1, \dots, A_m)$ of \kl{\(\MELL\) formulas}, a
%\intro{partition} of $\Gamma$ is a list $\Gamma' = (\Gamma_1; \cdots;\allowbreak \Gamma_n)$ of lists
%of \kl{\(\MELL\) formulas} such that there are $0 = i_0 < \dots < i_n = m$
%with \mbox{$\Gamma_j = (A_{i_{j-1}+1}, \dots, A_{i_{j}})$} for all
%$1 \leqslant j \leqslant n$;
%the partition $\Gamma'$ of $\Gamma$ is also denoted by
%$(A_1, \dots, A_{i_1}; \cdots ; A_{i_{n-1}+1}, \dots, A_m)$, with lists
%separated by semicolons.
%The \intro{flattening} of $\Gamma'$ is $\Gamma$.
Let $m,n \in \Nat$ and $\{i_j\}_{0 \leqslant j \leqslant n} \subseteq \Nat$ with $i_j < i_{j+1}$, $i_0 = 0$, $i_n = m$.
%Let $m, n, i_0, \dots, i_n \in \Nat$ with $i_j < i_{j+1}$ for all $0 \leqslant j < n$, $i_0 = 0$, $i_n = m$.
Let $A_1, \dots, A_m$ be \kl{\MELL formulas}, let $\Gamma_{\!j} = (A_{i_{j-1}+1}, \dots, A_{i_{j}})$ for all $1 \leqslant j \leqslant n$.
The list $\Gamma = (\Gamma_1, \allowbreak \dots, \allowbreak \Gamma_n)$ of lists of \kl{\MELL formulas} is also denoted by $(A_1, \dots, A_{i_1}; \cdots ; A_{i_{n-1}+1}, \dots, A_m)$, with lists separated by semicolons.
The \intro{flattening} of $\Gamma$ is the list $(A_1, \dots, A_m)$ of \MELL formulas.

\subsection{Proof-structures}
\label{subsect:proof-structure}

\begin{figure}[!t]
\vspace*{-3\baselineskip}
\centering
\pnet{
\pnformulae{
\pnf[Xcut]{$A$}~\pnf[Xncut]{$A^{\bot}$}~~~
\pnf[Ao]{$A$}~\pnf[Bo]{$B$}~
\pnf[Ap]{$A$}~\pnf[Bp]{$B$}~
\pnf[A1]{$A$}~\pnf[l]{$\cdots$}~\pnf[An]{$A$}~
\pnf[A1e]{$A$}~\pnf[le]{$\cdots$}~\pnf[Ane]{$A$}
\\
\pnf[Xax]{$X$}~\pnf[Xnax]{$X^{\bot}$}~~~
\pnf[1]{$\mathbf{1}$}~\pnf[bot]{$\bot$}~~~~~~~~~~~
\pnf[i]{$A_1$}~\pnf[d]{$\overset{p > 0}{\ldots}$}~\pnf[j]{$A_p$}
\pnaxiom[ax]{Xax,Xnax}
\pncut[cut]{Xcut,Xncut}
\pnone{1}
\pnbot{bot}
\pntensor{Ao,Bo}[AoB]{$A\otimes B$}
\pnpar{Ap,Bp}[ApB]{$A \parr B$}
\pnexp{}{A1,l,An}[]{$\wn A$}
\pnbag{}{A1e,le,Ane}[]{$\oc A$}
\pndaimon{i,j}

\vspace*{-\baselineskip}
\caption{Cells, with their labels and their typed inputs and outputs.
\label{fig:resource-cells}
\end{figure}

We define here proof-structures corresponding to some subsystems and extensions of \LL:
\MELL, \DiLL and $\DiLL_0$.
Full differential linear logic (\DiLL) is an extension of \MELL (with the same
language as \MELL) provided with both promotion rule (\ie, boxes) and
co-structural rules for the $\oc$-modality (the duals of the structural rules handling the
$\wn$-modality): $\DiLL_0$ and \MELL are particular
subsystems of \DiLL, respectively the promotion-free one (\ie, without boxes) and
the one without co-structural rules.
We reuse the syntax of proof-structures given in \cite{Wollic}, based on the graph notions introduced in \Cref{sect:graphs}.
Note that, unlike \cite{PaganiTasson2009}, we allow the presence of cuts (vertices of type $\cut$), even though we are not interested in cut-elimination and its study is left to future work.

\begin{defi}[module, proof-structure]
\label{def:proof-structure}
A (\DiLL) \intro{module} $M = (\rvert M \lvert, \VertType, \Orient, \FlagType, \allowbreak <)$ is a \kl[labeled graph]{labeled} ($\VertType$), \kl[directed graph]{directed} ($\Orient$), \kl[colored graph]{colored} ($\FlagType$), \kl[ordered graph]{ordered} ($<$) \kl{graph} $\lvert M \rvert$ without \kl{loops} such that:
\begin{itemize}
\item the map $\VertType \colon V_{|M|} \to \{ \textup{\ax}, \textup{\cut}, \one, \bot, \otimes, \parr, \wn, \oc, \maltese\}
$ associates with each vertex $v$ its \intro[vertex type]{type} $\VertType(v)$;
\item the map $\FlagType \colon F_{|M|} \to \Formulas_{\MELL}$ associates with each flag $f$ its \intro[edge type]{type} $\FlagType(f)$;
\item $<$ is a strict partial order on the \kl{flags} of $|M|$ that is total on the \kl{tails} of $|M|$ and on the inputs of each \kl{vertex} of type $\parr$ or $\otimes$, separately;

\item for every vertex $v \in V_{|M|}$,
\begin{itemize}
\item if $\VertType(v) = \textup{\cut}$, $v$ has no \kl{output} and
two \kl{inputs} $i_1$ and $i_2$, such that $\FlagType(i_1) = \FlagType(i_2)^{\bot}$;

\item if $\VertType(v) = \textup{\ax}$, $v$ has no inputs and
two outputs $o_1$ and $o_2$, with $\FlagType(o_1) = \FlagType(o_2)^{\bot}$ \kl{atomic};\footnotemark
\footnotetext{\label{note:atomic}We deal with \emph{atomic axioms} only to simplify the presentation in the next sections.
The general case with non-atomic axioms (\ie $\FlagType(o_1)$ and $\FlagType(o_2)$ are still \kl{dual} but not necessarily \kl{atomic}) is discussed in \Cref{sect:nonatomic}.}

\item if $\VertType(v) \in \{\one, \bot\}$, $v$ has no
inputs and only one output $o$, with $\FlagType(o) = \VertType(v)$;

\item if $\VertType(v) \in \{ \otimes, \parr \}$, $v$ has
two inputs $i_1 < i_2$ and one output $o$, with $\FlagType(o) = \FlagType(i_1) \, \VertType(v) \, \FlagType(i_2)$;

\item if $\VertType(v) \in \{\wn, \oc\}$, $v$ has
$n \geqslant 0$ inputs $i_1, \ldots, i_n$  and one output $o$, such that
$\FlagType(o) = \VertType(v) \, \FlagType(i_j)$ for all $1\leqslant j \leqslant n$;\footnotemark
\footnotetext{This implies that $\FlagType(i_j) = \FlagType(i_k)$ for all $1 \leqslant j,k \leqslant n$. There are no conditions on the number $n$ of inputs.}
$v$ is a \emph{contraction} (\resp \emph{co-contraction}) if $\VertType(v) = \wn$ (\resp $\VertType(v) = \oc$);

\item if $\VertType(v) =  \maltese$,
$v$ has no inputs and
$p > 0$ outputs $o_1,\ldots,o_p$.\footnotemark
\footnotetext{There are no conditions on the number of outputs $o_1,\ldots,o_p$ (besides $p > 0$) or on their types.}
\end{itemize}
In Figure \ref{fig:resource-cells} we depicted the corollas associated with
all types of vertices.
\end{itemize}

A (\DiLL) \intro{proof-structure} is a triple $R = (|R|,\TreeT,\BoxFunction)$ where:
\begin{itemize}
\item $|R|  = (\rVert R \lVert, \VertType_R, \Orient_R, \FlagType_R, \allowbreak <_R)$ is a \kl{module} with no input tails, called the \intro{structured graph} of $R$, and $\lVert R \rVert  = (F_{\rVert R \lVert}, V_{\rVert R \lVert}, \partial_{\rVert R \lVert}, j_{\rVert R \lVert})$ is the (\emph{undirected}) \intro[undirected graph]{graph} of $R$;
\item
$\TreeT$ is a \kl{rooted tree}
with no input tails, called the \intro{box-tree} of $R$;\footnotemark
\footnotetext{Intuitively, $\TreeT$ represents the tree-structure of the nested boxes of $R$, see Remark \ref{rmk:box} below.}
\item  $\BoxFunction = (\BoxFunction_{F}, \BoxFunction_{V}) \colon |R| \to \TreeT^{\ReflexiveTransitive}$ is a \kl{directed graph morphism},\footnotemark
\footnotetext{\label{foot:struct}The structured graph $|R|$ of
$R$ is more structured than a directed graph such as $\TreeT^{\ReflexiveTransitive}$: $|R|$ is directed but also labeled, colored, ordered.
When we talk of a morphism between two structured graphs where one of the two, say $\sigma$, is less structured than the other, say $\tau$, we mean that $\tau$ must be only considered with the same structure as $\sigma$.
Thus, in this case, $\BoxFunction$ is a morphism from $(\lVert R \rVert, \Orient_{R})$---discarding $\VertType_{R}$, $\FlagType_{R}$, $<_{R}$---to $\TreeT^{\ReflexiveTransitive}$.}
called the \intro{box-function} of $R$, such that $\BoxFunction_{F}$ induces a bijection from a subset of $\bigcup_{ v \in V_{\lVert R \rVert}, \VertType(v) = \oc}\In_{\lvert R \rvert}(v)$ (the set of inputs of the vertices of type $\oc$ in $\lvert R \rvert$) to the set of input flags in $\TreeT$;\footnotemark
\footnotetext{\label{foot:box}It means that for any input flag $f'$ in $\TreeT$ there is exactly one input $f$ of some vertex of type $\oc$ in $|R|$ such that $\BoxFunction_F(f) = f'$;
but, for any input $f$ of some vertex of type $\oc$ in $|R|$, $\BoxFunction_{F}(f)$ need not be an input flag in $\TreeT$ (by definition of directed graph morphism, $\BoxFunction_{F}(f)$ is necessarily an input flag in $\TreeT^{\ReflexiveTransitive}$).
In particular, if $|R|$ has no vertices of type $\oc$, $\TreeT$ is a root with its output and no inputs; and if $\lVert R \rVert$ is the \kl[empty graph]{empty graph}, $\BoxFunction$ is the \kl{empty graph morphism} from $\lvert R \rvert$ to such a $\TreeT$.
Intuitively, given a vertex $v$ of type $\oc$ in $\lvert R \rvert$,
a box is associated with (and only with) each input $f$ of $v$ such that $\BoxFunction_{F}(f)$ is an input flag in $\TreeT$ and not only in $\TreeT^{\ReflexiveTransitive}$: $f$ represents the principal door in the border of such a box, indeed
by definition of directed graph morphism, $\BoxFunction_V((\partial_{\lVert R \rVert}\circ j_{\lVert R \rVert})(f)) \neq \BoxFunction_V(\partial_{\lVert R \rVert}(f))$, and  for all $f' \in F_{\lVert R \rVert}$, if $f' \neq f$ then $\BoxFunction_{F}(f') \neq \BoxFunction_{F}(f)$.}
and for any
$v \in V_{\lVert R \rVert}$ and any input $f$ of $v$,
if $\BoxFunction_V((\partial_{\lVert R \rVert} \circ j_{\lVert R \rVert}) (f)) \neq
\BoxFunction_V(\partial_{\lVert R \rVert} (f))$ then $\VertType(v) \in \{ \oc, \wn
\}$.\footnotemark
\footnotetext{\label{note:border}Roughly, it says that the border of a box is made of inputs
of vertices of type $\oc$ or $\wn$ in $\lvert R \rvert$.}
\end{itemize}

A (\DiLL) \kl{proof-structure} $R = (|R|, \TreeT, \BoxFunction)$ is said to be:
\begin{enumerate}
\item \intro[$\MELL$ proof-structure]{$\MELL$} if its structured graph $\lvert R \rvert$ has no vertices of type $\maltese$ and
\begin{itemize}
\item all vertices in $|R|$ of type $\oc$ have exactly one input,

\item the bijection induced by $\BoxFunction_F$ is defined on the whole set $\bigcup_{ v \in V_{\lVert R \rVert}, \VertType(v) = \oc}\In_{\lvert R \rvert}(v)$;\footnotemark
\footnotetext{It means that for any input flag $f'$ in $\TreeT$ there is exactly one vertex of type $\oc$ in $|R|$ whose unique input $f$ is such that $\BoxFunction_F(f) = f'$;
and, if $f$ is the (only) input some vertex of type $\oc$ in $|R|$, $\BoxFunction_{F}(f)$ is an input flag in $\TreeT$.
Intuitively, a box is associated with (and only with) the unique input of each vertex of type $\oc$~in~$\lvert R \rvert$.}
\end{itemize}
\item  \intro[$\DiLL_0$ proof-structures]{$\DiLL_0$} (or \emph{resource})
if $\TreeT$ consists only of the root with its output, and either $|R|$ has no vertices  of type $\maltese$ or $\lvert R \rvert$ is a \intro{daimon}, \ie $\lvert R \rvert$ has only one vertex and it is of type $\maltese$;

\item \intro[empty proof-structure]{empty} (which is both $\MELL$ and $\DiLL_0$) if its \kl[undirected graph]{graph} $\lVert R \rVert$ is \kl[empty graph]{empty}; it is denoted by $\emptynet$;

\item \intro{cut-free} if its \kl{structured graph} $\lvert R \rvert$ has no vertices of type $\Cut$, otherwise it is \intro{with cuts}.
\end{enumerate}
\end{defi}

Our \kl{$\MELL$ proof-structures} correspond to
usual $\MELL$ proof-structures (as in \cite{CarvalhoTortora}).
Our \kl{$\DiLL_0$ proof-structures} correspond to
usual $\DiLL_0$ proof-structures (as in \cite{DBLP:journals/tcs/EhrhardR06}) except that we
allow also (proof-structures that are) \emph{daimons}.
Daimons will be used in the Taylor expansion to deal with the content of a box taken $0$ times (see \Cref{sect:taylor}).
Our interest for $\DiLL$ proof-structures
is just to have a unitary syntax subsuming both \MELL and $\DiLL_0$ without considering
cut-elimination: for this reason, unlike \cite{Pagani09,Tranquilli09,Tranquilli11}, our $\DiLL$ proof-structures are not allowed to contain a
sum of $\DiLL$ proof-structure inside a box.\footnotemark
\footnotetext{This restriction is without loss of generality, because a box containing a
sum of proof-structures is equivalent (see \cite{Tranquilli09}) to a co-contraction
of the boxes of each proof-structure in
the sum. Also, the vertex of type $\maltese$ corresponds to the empty sum inside a box: roughly, it is the content of an ``empty box''.}

Given a proof-structure $R = (|R|, \TreeT, \BoxFunction)$, the output \kl{tails}
of $|R|$ are the \intro{conclusions} of $R$.
The \intro[proof-structure type]{type} of $R$ is the list of the \kl[edge type]{types} of these
conclusions, ordered according to $<_{\lvert R \rvert}$.

Borrowing the terminology from \cite{DBLP:journals/tcs/EhrhardR06,DBLP:conf/popl/Lafont90}, in proof-structures, we speak of \intro{cells} instead of vertices, and of \emph{$\ell$-cell} for a
cell of \kl[vertex type]{type} $\ell$.
An \intro{hypothesis} is a cell without inputs.

\begin{rem}[box]
\label{rmk:box}
In our syntax, boxes do not have explicit constructors or cells, hence boxes and
depth of a proof structure $R = (|R|, \TreeT, \BoxFunction)$ are recovered in a non-inductive~way.

Roughly, any non-root vertex $v$ in $\TreeT$ induces a subgraph of $\TreeT^{\ReflexiveTransitive}$ made up of all vertices ``above $v$''
with their inputs and outputs: the preimage of this subgraph through $\BoxFunction$ is the \emph{box} of $v$ in $\lvert R \rvert$.
The preimage of the root of $\TreeT$ through $\BoxFunction$
is the part of $|R|$ outside~any~box.

More precisely, with 	every flag $f$ of $|R|$ such that ${\BoxFunction_{F}}(f)$ is an input flag of $\TreeT$\footnotemark
\footnotetext{\label{foot:box-tree}By the constraints on $\BoxFunction$, this
condition can be fulfilled only by inputs of $\oc$-cells in $|R|$, and an input of a $\oc$-cell need not fulfill it;
in particular, if $R$ is a \kl{\MELL proof-structure}, then this
condition is fulfilled by all and only the inputs of $\oc$-cells (and such
an input is unique for any $\oc$-cell) in $|R|$;
but if $R$ is a $\DiLL_0$ proof-structure, this condition is not fulfilled by any flag in $|R|$ (since $\TreeT$ has no inputs) and so $\BoxFunction$ is a \kl{directed graph
morphism} associating the root of $\TreeT$ with any cell of $R$.
Thus, in a \kl[DiLL0 proof-structure]{$\DiLL_0$ proof-structure}
$\rho = (|\rho|,\TreeT_{\rho},\BoxFunction_{\rho})$, there are no boxes, $\TreeT_{\rho}$ and
$\BoxFunction_{\rho}$ do not induce any structure on $|\rho|$: $\rho$ can be
\mbox{identified with $|\rho|$.}}
is associated a \intro{box} $B_{\!f}$, that is the \kl{subgraph}
of $|R|$ (which is actually a proof-structure) made up of all the cells $v$ (with their inputs and outputs) such that there is a directed path on $\TreeT$ from ${\BoxFunction_{V}}(v)$ to 	${\BoxFunction_{V}}((\partial_{\lVert R \rVert} \circ j_{\lVert R \rVert})(f))$ (note that $f$ and the $\oc$-cell of which $f$ is an input
are not in $B_f$).
A \emph{conclusion} of such a box $B_{\!f}$
is any output flag $f'$
in $B_{\!f}$ such that $(\partial_{\lVert R \rVert} \circ j_{\lVert R \rVert})(f')$ is not in $B_{\!f}$.
The tree-structure of	$\TreeT$ expresses the usual \emph{nesting condition}~of~boxes:
two boxes in $|R|$ are either disjoint or contained one in the other.

The \intro{depth} of a cell $v$ of $R$ is the \kl[path length]{length} of the directed path in
$\TreeT$ from $\BoxFunction_{V}(v)$ to the root of $\TreeT$.
The \intro[depth of proof-structure]{depth} of $R$ is the maximal \kl{depth} of the cells~of~$R$.
\end{rem}

\begin{figure}[!t]
\vspace{\beforepn}
\centering
\begin{subfigure}[b]{0.58\textwidth}
\centering
\scalebox{0.8}{
\pnet{
\pnformulae{
~~~\pnf[botax]{$\bot$}~\pnf[1ax]{$\one$}~~~\pnf[Y]{$Y$}~\pnf[Yp]{$Y^\bot$} \\
\\
\\ \\
\pnf[Xp]{$X^\bot$}
\pnone[1axcell]{1ax}
\pnbot[botaxcell]{botax}
\pnaxiom[axprop]{Xp,X}
\pnaxiom[axprop']{Y,Yp}
\pnboxc{1axcell,botaxcell,botax,1ax}{purple}
\pnbag{}{1ax}[!1ax]{$\oc \one$}[1.2]
\pnbot[botcell]{bot}[1][-.02]
\pnone[1cell]{1}
\pnboxc{1,1cell,1axcell,botaxcell,botax,1ax,!1ax}{blue}
\pnbag{}{1}[!1]{$\oc \one$}[1.7]
\pnexp{}{bot,botax}[?bot]{$\wn \bot$}[1.8]
\pnexp{}{!1ax,!1}[?!1]{$\wn\oc \one$}[1]
\pntensor{X,?bot}[tens]{$X \otimes \wn \bot$}[0.9]
\pnexp{}{Y}[?Y]{$\wn Y$}
\pnpar{?Y,Yp}[par]{$\wn Y \parr Y^\bot$}
\pnboxc{axprop',Y,Yp,?Y,par}{red}
\pnbag{}{par}[!par]{$\oc (\wn Y \parr Y^\bot)$}[1.3]
\pnone[1cell']{1'}
\pnboxc{1',1cell'}{orange}
\pnbag{}{1'}[!1']{$\oc \one$}[1.2]
\caption{The \kl{structured graph} $\lvert S \rvert$.}
\end{subfigure}
\begin{subfigure}[b]{0.4\textwidth}
\centering
\scalebox{0.8}{
\raisebox{-1cm}{
\begin{forest}
for tree={grow'=north, edge=<-, l-=2em}
[$ $, name=root
[${\,\bullet\,}$, name = root1
[$ $, name = box11o,
[$\textcolor{blue}{\bullet}$, name = box11, edge = blue
[$ $, name = box111o, edge = blue
[$\textcolor{purple}{\,\bullet\,}$, name = box111, edge = purple]
[$ $, name = box21o
[$\textcolor{red}{\bullet}$, name = box21, edge = red]
[$ $, name = box22o
[$\textcolor{orange}{\bullet}$, name = box22, edge = orange]
\coordinate (box111') at ([shift={(0:0.8)}]box111);
\draw[<-,dotted,purple,line width=1pt] (box111) to[out=north east,
in=north west] (box111');
\draw[<-,dotted,purple,line width=1pt] (box111') to[out=south west,
in=south east] (box111);
\coordinate (box111root1) at ([shift={(-110:2.5)}]box111);
\draw[->,dotted,purple,line width=1pt] (box111) to[out=south west,
in=north west] (box111root1);
\draw[->,dotted,line width=1pt] (box111root1) to[out=south east,
in=west] (root1);
\coordinate (box11') at ([shift={(180:0.8)}]box11);
\draw[<-,dotted,blue,line width=1pt] (box11) to[out=north west,
in=north east] (box11');
\draw[<-,dotted,blue,line width=1pt] (box11') to[out=south east,
in=south west] (box11);
\coordinate (box21') at ([shift={(90:0.8)}]box21);
\draw[->,dotted,red,line width=1pt] (box21) to[out=north west,
in=south west] (box21');
\draw[->,dotted,red,line width=1pt] (box21') to[out=south east,
in=north east] (box21);
\coordinate (box22') at ([shift={(0:0.8)}]box22);
\draw[<-,dotted,orange,line width=1pt] (box22) to[out=north east,
in=north west] (box22');
\draw[<-,dotted,orange,line width=1pt] (box22') to[out=south west,
in=south east] (box22);
\coordinate (root1') at ([shift={(-30:0.8)}]root1);
\draw[->,dotted,line width=1pt] (root1) to[out=south,
in=west] (root1');
\draw[->,dotted,line width=1pt] (root1') to[out=north,
in=east] (root1);
\end{forest}
\caption{The \kl{box-tree} \texorpdfstring{$\TreeT_{S}$}{} (without dotted
lines) and the reflexive-transitive closure
\texorpdfstring{$\TreeT_{S}^{\ReflexiveTransitive}$}{} of
\texorpdfstring{$\TreeT_{S}$}{} (with also dotted lines).}
\end{subfigure}
\caption{A \MELL proof-structure $S = (\lvert S \rvert, \TreeT_{S}, \BoxFunction_{S})$.}
\label{fig:pointed-proof-net}
\end{figure}

\begin{exa}
In \Cref{fig:pointed-proof-net} a \MELL proof-structure $S = (\lvert S \rvert, \TreeT_{S}, \BoxFunction_{S})$ is depicted.
The box-function $\BoxFunction_{S}$ is kept implicit by
means of colors: the colored areas in $|S|$ represent boxes (the preimages of non-root vertices of $\TreeT_{S}$ through $\BoxFunction_{S}$), and the same color is used on $\TreeT_{S}$ to show where each box is mapped by $\BoxFunction_{S}$.
\end{exa}

The proof-structures we have defined depend on the carrier sets for vertices and flags.
It is natural to abstract away from them, and identify two proof-structures that differ only in the name of their vertices and flags, through a handy notion of isomorphism (\ie~structure-preserving bijection) inherited from the one of \kl{graph isomorphism} defined in \Cref{sect:graphs}.

\begin{definition}[isomorphism]
Let $R = (|R|, \TreeT, \BoxFunction)$ and $R' = (|R'|, \TreeT', \BoxFunction')$ be proof-structures.
An \emph{isomorphism} from $R$ to $R'$ is a couple $(\varphi_{\lvert\cdot\rvert}, \varphi_\mathsf{tree})$ where
$\varphi_{\lvert\cdot\rvert} \colon |R| \to |R'|$ is a \kl{structured graph} isomorphism,
and $\varphi_\mathsf{tree} \colon \TreeT \to \TreeT'$ is a \kl[directed graph morphism]{directed graph isomorphism},
such that the diagram below commutes.
\begin{equation*}
\begin{tikzcd}[row sep=3.0ex]
\lvert R \rvert \arrow[r, "\BoxFunction"] \arrow[d, "\varphi_{\lvert\cdot\rvert}"]
\& \mathcal{A}^\circlearrowleft \arrow[d, "\varphi_\mathsf{tree}^\circlearrowleft"]
\\
\lvert R' \rvert \arrow[r, "\BoxFunction'"]
\& \mathcal{A}'^\circlearrowleft
\end{tikzcd}
\end{equation*}
\end{definition}

Note that if $R$ is a \MELL or
$\DiLL_0$ proof-structure isomorphic to a proof-structure $R'$, then $R'$ is respectively \MELL or $\DiLL_0$.
Often we implicitly consider proof-structures up to isomorphism (as we do, for instance, in every figure representing proof-structures).

\subsection{Quasi-proof-structures}

We need to consider more general structures in order to accommodate our
rewrite rules, as discussed in \Cref{sect:outline}, p.~\pageref{subsect:intro-quasi-proof-structure} (the rewrite rules are defined in \Cref{sect:rules,sec:naturality}).
This is why we extend all the definitions to \emph{tuples} of proof-structures.

\begin{defi}[quasi-proof-structure]
\label{def:quasi-proof-structure}
A (\DiLL) \intro{quasi-proof-structure} is a tuple
$R = (R_1,\dots,R_n)$
of proof-structures, for some $n > 0$;
for all $ 1 \leqslant i \leqslant n$, $R_i$ is a \intro{component} of $R$.
If $R_i = \emptynet$
for all $ 1 \leqslant i \leqslant n$, then $R$ is an \intro{empty quasi-proof-structure}, noted $n \emptynet$ or $\emptynets$.\footnotemark
\footnotetext{The $0$-ary tuple of proof-structures is \emph{not} a quasi-proof-structure.
Indeed, every quasi-proof-structure has at least one (possibly \kl[empty proof-structure]{empty}) component. Note that the components of a quasi-proof-structure are independent of each other, in particular they may differ in the number of their conclusions or in their type.}

For convenience, given a proof-structure $R_i = (\lvert R_i \rvert, \TreeT_{i}, \BoxFunction_{i})$ for all $1 \leqslant i \leqslant n$, we denote the quasi-proof-structure $R = (R_1, \dots, R_n)$ as $R = (\lvert R \rvert, \ForestT_{R}, \BoxFunction_{R})$, where $|R| = (\lvert R_1 \rvert, \dots, \lvert R_n \rvert)$ is the \intro[structured graph of quasi-proof-structure]{structured graph} of $R$,
$\ForestT_{R} = (\TreeT_{1}, \dots, \TreeT_{n})$ is the \intro{box-forest} of $R$,  $\BoxFunction_{R} = (\BoxFunction_{1}, \dots, \BoxFunction_{n})$ is the \intro[box-function of quasi-proof-structure]{box-function} of $R$;
the \emph{graph} of $R$ is $\lVert R \rVert = (\lVert R_1 \rVert, \dots, \lVert R_n\rVert)$.

A \intro[conclusion of quasi-proof-structure]{conclusion} of $R$ is any \kl{conclusion} of any component of $R$.

A quasi-proof-structure $R$ is \intro[MELL quasi-proof-structure]{\MELL} (\resp \intro[DiLL0 quasi-proof-structure]{$\DiLL_0$}) if all components of $R$ are \MELL (\resp $\DiLL_0$) proof-structures.
\end{defi}

The short notation $R = (\lvert R \rvert, \ForestT_{R}, \BoxFunction_{R})$ for quasi-proof-structures makes sense because the structured graph $|R| = (|R_1|, \dots, |R_n|)$ can be seen as the disjoint union  of its components $|R_1|, \dots, |R_n|$, and similarly for $\ForestT_{R}$ and $\BoxFunction_{R}$. In particular, the box-forest $\ForestT_{R}$ is the disjoint union of the box-trees $\TreeT_{1}, \dots, \TreeT_{n}$ of $R_1, \dots, R_n$.
The box-function $\BoxFunction_{R}$ locates not only the boxes on $\lvert R \rvert$, but also the different components of $R$ on $\lvert R \rvert$ (see also Remark~\ref{rmk:components}).

The only delicate point is the definition of the order $<_{|R|}$ for the \kl[conclusion of quasi-proof-structure]{conclusions} of the quasi-proof-structure $R = (R_1, \dots, R_n)$, given the order $<_{|R_i|}$ for each component $|R_i|$.
Given the conclusions $f,f'$ of $R$, we set $f <_{|R|} f'$ if either $f$ is a conclusion of $R_i$ and $f'$ is a conclusion of $R_{i'}$ with $i < i'$, or $f$ and $f'$ are conclusions of the same \mbox{component $R_j$ and $f <_{|R_j|} f'$.}

We often identify the conclusions of $R$ and their order $<_{|R|}$ with a finite initial segment of $\Nat \setminus \{0\}$ and its natural order.
Note that $\emptynets$ has no conclusions, akin to $\emptynet$, as $\lVert\emptynet\rVert$ is \kl[empty graph]{empty}.

The \intro[quasi-proof-structure type]{type} of a quasi-proof-structure $R = (R_1, \dots, R_n)$ is a list $\Gamma = (\Gamma_1, \dots, \Gamma_n)$ of lists of \MELL formulas such that $\Gamma_i$ is the \kl[proof-structure type]{type} of $R_i$ for all $1 \leqslant i \leqslant n$.
When $n=1$, we often identify $R$ and $R_1$ (a quasi-proof-structure with only one component and a proof-structure), or $\Gamma$ and $\Gamma_1$ (the type of a quasi-proof-structure with only one component and the type of a proof-structure).
So, the type of a quasi-proof-structure $R$ \mbox{determines if $R$ is a proof-structure.}

The \kl[quasi-proof-structure type]{type} of an \kl{empty quasi-proof-structure} $\emptynets$ is a non-empty list of empty lists of \MELL formulas, where each occurrence of the empty list of \MELL formulas is the type of a component $\emptynet$ of $\emptynets$.
More precisely, $\emptylist$ is the type of $\emptynet$, and $\kl[empty quasi-proof-structure]{n\emptylist}$ is the type of $n \emptynet$ for every $n > 0$.

\begin{exa}
In \Cref{fig:pointed-quasi-proof-net} a \(\MELL\)
\kl{quasi-proof-structure} $R$ is depicted. The colored areas represent the preimages of
boxes, and
each dashed box represents a component of $R$ (in other examples, the absence of a dashed line means that there is only one component).
\end{exa}

\begin{figure}[!t]
\vspace{\beforepn}
\centering
\begin{subfigure}[b]{0.58\textwidth}
\centering
\scalebox{0.8}{
\pnet{
\pnformulae{
~~~\pnf[botax]{$\bot$}~\pnf[1ax]{$\one$}~~~\pnf[Y]{$Y$}~\pnf[Yp]{$Y^\bot$} \\
~~\pnf[bot]{$\bot$}~~~\pnf[1]{$\one$} \\
~\pnf[X]{$X$}~~~~~~~~~\pnf[1']{$\one$} \\ \\ \\
\pnf[Xp]{$X^\bot$}
\pnone[1axcell]{1ax}
\pnbot[botaxcell]{botax}
\pnaxiom[axprop]{Xp,X}
\pnaxiom[axprop']{Y,Yp}
\pnboxc{1axcell,botaxcell,botax,1ax}{purple}
\pnbag{}{1ax}[!1ax]{$\oc \one$}[1.2]
\pnbot[botcell]{bot}[1][-.02]
\pnone[1cell]{1}
\pnboxc{1,1cell,1axcell,botaxcell,botax,1ax,!1ax}{blue}
\pnbag{}{1}[!1]{$\oc \one$}[1.7]
\pnexp{}{bot,botax}[?bot]{$\wn \bot$}[1.7]
\pnexp{}{!1ax,!1}[?!1]{$\wn\oc \one$}[.9]
\pntensor{X,?bot}[tens]{$X \otimes \wn \bot$}[.9]
\pnexp{}{Y}[?Y]{$\wn Y$}
\pnpar{?Y,Yp}[par]{$\wn Y \parr Y^\bot$}
\pnboxc{axprop',Y,Yp,?Y,par}{red}
\pnbag{}{par}[!par]{$\,\,\oc (\wn Y \parr Y^\bot)$}[1.2]
\pnone[1cell']{1'}
\pnboxc{1',1cell'}{orange}
\pnbag{}{1'}[!1']{$\oc \one$}[1.3]
\pnsemiboxc{axprop,Xp,1,1axcell,botaxcell}{green}
\pnsemiboxc{axprop',!1',Y}{gray}
\caption{The structured graph $\lvert R \rvert$.}
\end{subfigure}%
\begin{subfigure}[b]{0.4\textwidth}
\centering
\scalebox{0.8}{
\begin{forest}
for tree={grow'=north, edge=<-, l-=2em}
[$ $, name=root
[$\textcolor{green}{\bullet}$, name = root3, edge = green
[$ $, name = box11o, edge = green
[$\textcolor{blue}{\bullet}$, name = box11, edge = blue
[$ $, name = box111o, edge = blue
[$\textcolor{purple}{\,\bullet\,}$, name = box111, edge = purple]
\coordinate (box111') at ([shift={(0:0.8)}]box111);
\draw[<-,dotted,purple,line width=1pt] (box111) to[out=north east,
in=north west] (box111');
\draw[<-,dotted,purple,line width=1pt] (box111') to[out=south west,
in=south east] (box111);
\coordinate (box111root3) at ([shift={(-110:2.7)}]box111);
\draw[->,dotted,purple,line width=1pt] (box111) to[out=south west,
in=north west] (box111root3);
\draw[->,dotted,green,line width=1pt] (box111root3) to[out=south east,
in=west] (root3);
\coordinate (box11') at ([shift={(180:0.8)}]box11);
\draw[<-,dotted,blue,line width=1pt] (box11) to[out=north west,
in=north east] (box11');
\draw[<-,dotted,blue,line width=1pt] (box11') to[out=south east,
in=south west] (box11);
\coordinate (root3') at ([shift={(-30:0.8)}]root3);
\draw[->,dotted,green,line width=1pt] (root1) to[out=south,
in=west] (root3');
\draw[->,dotted,green,line width=1pt] (root3') to[out=north,
in=east] (root3);
\end{forest}
\begin{forest}
for tree={grow'=north, edge=<-, l-=2em}
[$ $, name=root
[$\textcolor{gray}{\bullet}$, name = root1, edge = gray
[$ $, name = box21o, edge = gray
[$\textcolor{red}{\bullet}$, name = box21, edge = red]
[$ $, name = box22o, edge = gray
[$\textcolor{orange}{\bullet}$, name = box22, edge = orange]
\coordinate (box11') at ([shift={(180:0.8)}]box11);
\coordinate (box21') at ([shift={(90:0.8)}]box21);
\draw[->,dotted,red,line width=1pt] (box21) to[out=north west,
in=south west] (box21');
\draw[->,dotted,red,line width=1pt] (box21') to[out=south east,
in=north east] (box21);
\coordinate (box22') at ([shift={(0:0.8)}]box22);
\draw[<-,dotted,orange,line width=1pt] (box22) to[out=north east,
in=north west] (box22');
\draw[<-,dotted,orange,line width=1pt] (box22') to[out=south west,
in=south east] (box22);
\coordinate (root1') at ([shift={(-30:0.8)}]root1);
\draw[->,dotted,gray,line width=1pt] (root1) to[out=south,
in=west] (root1');
\draw[->,dotted,gray,line width=1pt] (root1') to[out=north,
in=east] (root1);
\end{forest}
\caption{The \kl{box-forest} \texorpdfstring{$\ForestT_{R}$}{} (without dotted
lines) and the reflexive-transitive closure
\texorpdfstring{$\ForestT_{R}^{\ReflexiveTransitive}$}{} of
\texorpdfstring{$\ForestT_{R}$}{} (with also dotted lines).}
\end{subfigure}
\caption{A \(\MELL\) quasi-proof-structure $R = (\lvert R \rvert, \ForestT_{R}, \BoxFunction_{R})$.}
\label{fig:pointed-quasi-proof-net}
\end{figure}

\begin{remark}[components]
\label{rmk:components}
A difference arises between a $\DiLL_0$ proof-structure and a $\DiLL_0$ quasi-proof-structure.
Both have no boxes.
In the former, its box-tree and box-function do not induce any structure on its \kl{structured graph}, so we can identify a $\DiLL_0$ proof-structure with its \kl{structured graph}.
In the latter, its box-forest and box-function do
induce a structure on its structured graph: indeed, its box-forest is made up only of roots with their output and its box-function separates the components of its structured graph, by mapping the vertices to the roots.
So, we cannot identify a $\DiLL_0$ quasi-proof-structure with~its~\kl{structured graph}.
\end{remark}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "mainFinal"
%%% End:

% !TEX root = mainFinal.tex
\section{The Taylor expansion}
\label{sect:taylor}

The \emph{Taylor expansion} $\Taylor{R}$ \cite{Ehrhard:2008} of a \MELL (or more generally \DiLL) proof-structure $R$ is a possibly infinite set of $\DiLL_0$ proof-structures:
roughly, each element of $\Taylor{R}$ is obtained from $R$
by approximating---\ie~replacing---each box $B$ in $R$ with $n_B$ copies of its content (for some $n_B \in \Nat$), recursively on the \kl{depth} of $R$.
Note that $n_B$ depends not only on $B$ but also on which ``copy''
of all boxes containing $B$ we are considering.
Usually, the Taylor expansion $\Taylor{R}$ of a \MELL proof-structure $R$ is defined globally and inductively \cite{MazzaPagani07,PaganiTasson2009,ChouquetVaux18}: with $R$ is directly associated the whole set $\Taylor{R}$ by induction on the depth of~$R$.
A drawback of this
approach is that, for each element of $\Taylor{R}$, the way the copies of the content of a box are merged is defined ``by hand'', which is syntactically heavy.

Following \cite{Wollic}, we adopt an alternative non-inductive approach, which
strongly refines \cite{FSCD2016}: the Taylor expansion is defined \emph{pointwise}
(see Example \ref{ex:proto-taylor} and \Cref{fig:taylor-expansion}).
Indeed, proof-structures have a tree structure made explicit by their \kl{box-function}.
The definition of the Taylor expansion uses this tree structure:
first, we define how to ``\emph{expand}'' a tree via the notion of \kl{thick subtree} \cite{Boudes:2009} (Definition \ref{def:thick}; roughly, it states the
number of copies of each box to be taken, recursively),
we then take all
these expansions of the box-tree of a proof-structure and we \emph{pull} them \emph{back} to the underlying graphs (Definition \ref{def:proto}), finally
we \emph{forget} the tree structures associated with them (Definition \ref{def:taylor}).
Thus, pullbacks give an abstract and elegant way to define the merging of copies of the content of a box in an
element of $\Taylor{R}$.
The use of pullbacks is made possible because all the ingredients in our
definition of a proof-structure live in the category of directed graphs (as defined in \Cref{sect:graphs}).

An advantage of our approach is that it smoothly generalizes to \kl{quasi-proof-structures}.

\begin{defi}[thick subtree and subforest]
\label{def:thick}
Let $\sigma$ be a \kl{rooted tree}.
A \intro{thick subtree} of $\sigma$ is a pair
$(\tau, h)$ of a rooted tree $\tau$ and a directed graph morphism
$h = (h_F, h_V) \colon \tau \to \sigma$.

Let $\sigma = (\sigma_1, \dots, \sigma_n)$ be a \kl{forest} of \kl{rooted trees}, with $n > 0$.
A \intro{thick subforest} of $\sigma$ is a tuple $((\tau_1, h_1), \dots, (\tau_n, h_n))$ where  $(\tau_i, h_i)$ is a thick subtree of $\sigma_i$ for all $1 \leqslant i \leqslant n$.
It is denoted by $(\tau, h)$, where $\tau = (\tau_1, \dots, \tau_n)$ and $h = (h_1, \dots, h_n)$.
\end{defi}

\begin{exa}
\label{ex:proto-taylor}
The following is a graphical presentation of a \kl{thick subforest} $(\tau,h)$
of the \kl{box-forest} $\ForestT_R$ of the \kl{quasi-proof-structure} in
\Cref{fig:pointed-quasi-proof-net}, where the directed graph morphism
$h = (h_F, h_V) \colon \tau \to \ForestT_R$ is depicted chromatically (same color means same
image via $h$).
\vspace{-0.3\baselineskip}
\begin{align*}
\scalebox{0.7}{
\raisebox{1.3cm}{\Large$\tau \ = \ $}
\begin{forest}
for tree={grow'=north, edge=<-, l=0.2pt}
[$ $
[$\textcolor{green}{\bullet}$, edge = green,
[$ $, edge = green
[$\textcolor{blue}{\bullet}$, edge = blue
[$ $, edge = blue
[$\textcolor{purple}{\bullet}$, edge = purple]
[$ $, edge = green,
[$\textcolor{blue}{\bullet}$, edge = blue]
[$ $, edge = green,
[$\textcolor{blue}{\bullet}$, edge = blue
[$ $, edge = blue
[$\textcolor{purple}{\bullet}$, edge = purple]
[$ $, edge = blue
[$\textcolor{purple}{\bullet}$, edge = purple]
\end{forest}
\begin{forest}
for tree={grow'=north, edge=<-, l=0.2pt}
[$ $, edge = gray
[$\textcolor{gray}{\bullet}$, edge = gray
[$ $, edge = gray
[$\textcolor{red}{\bullet}$, edge = red]
[$ $, edge = gray
[$\textcolor{orange}{\bullet}$, edge = orange]
[$ $, edge = gray
[$\textcolor{orange}{\bullet}$, edge = orange]
[$ $, edge = gray
[$\textcolor{orange}{\bullet}$, edge = orange]
[$ $, edge = gray
[$\textcolor{orange}{\bullet}$, edge = orange]
\end{forest}
\raisebox{1.3cm}{\Large$\qquad\overset{h}{\longrightarrow}\qquad$}
\begin{forest}
for tree={grow'=north, edge=<-, l=0.2pt}
[$ $, edge = green
[$\textcolor{green}{\bullet}$, edge = green
[$ $, edge = green
[$\textcolor{blue}{\bullet}$, edge = blue
[$ $, edge = blue
[$\textcolor{purple}{\bullet}$, edge = purple]
\end{forest}
\
\begin{forest}
for tree={grow'=north, edge=<-, l=0.2pt}
[$ $, edge = gray
[$\textcolor{gray}{\bullet}$, edge = gray
[$ $, edge = gray
[$\textcolor{red}{\bullet}$, edge = red]
[$ $, edge = gray
[$\textcolor{orange}{\bullet}$, edge = orange]
\end{forest}
\raisebox{1.3cm}{\Large$ \ =  \ \ForestT_R$}
\end{align*}
Intuitively, it means that $\tau$ is obtained from $\ForestT_R$ by taking $3$
copies of the blue box, $1$ copy of the red box and $4$ copies of the orange
box; in the first (resp.~second; third) copy of the blue box, $1$ copy
(resp.~$0$ copies; $2$ copies) of the purple box has been taken.
\end{exa}

\begin{remark}[roots]
\label{rmk:roots}
If $(\tau,h)$ is a \kl{thick subforest} of a forest $\sigma$ of rooted trees, $h$ sets up a bijection between the roots of $\tau$ and $\sigma$, by definition of \kl{directed graph morphism};
so, we can identify the roots of $\tau$ with the ones of $\sigma$.
In particular, if $\sigma$ is made of roots with their output and no inputs, the only thick subforest of $\sigma$ is $\sigma$ with its \kl{identity graph morphism}.
\end{remark}

The crucial point is to pull back the expansion of a forest to quasi-proof-structures.

\begin{defi}[proto-Taylor expansion]
\label{def:proto}
Let $R = (|R|, \ForestT_R, \BoxFunction_{R})$ be a \kl{quasi-proof-structure}.
The \intro{proto-Taylor expansion} of $R$ is the set $\ProtoTaylor{R}$ of
thick subforests of $\ForestT_{R}$.

Let $t = (\tau_t, h_t) \in \ProtoTaylor{R}$.
The \intro[tree expansion]{$t$-expansion} of $R$ is the \kl{pullback} $(R_t, p_t, p_R)$ below,
computed in the category of
directed graphs and directed graph morphisms.\footnotemark
\footnotetext{So, $\lvert R \rvert$ is considered as directed graph (see \Cref{foot:struct}), forgetting that it is colored, labeled, ordered.}
\begin{align*}
\begin{tikzcd}
R_t \ar[r,"p_t"] \ar[d,swap,"p_R"]
\arrow[dr, phantom, "\scalebox{1.5}{$\lrcorner$}" , very near start, color=black]
\& \tau_t^{\circlearrowleft}
\ar[d,"h_t^{\circlearrowleft}"]\\
\lvert R \rvert  \ar[r,"\BoxFunction_{R}"]\& \ForestT_{R}^{\circlearrowleft}
\end{tikzcd}
\end{align*}
\end{defi}

Given a \kl{quasi-proof-structure} $R$ and $t = (\tau_t, h_t) \in \ProtoTaylor{R}$,
the directed graph $R_t$ inherits the types of its vertices and flags by pre-composition of $\VertType_{\lvert R \rvert}$ and $\FlagType_{\lvert R \rvert}$ with the \kl{graph morphism} $p_R \colon R_t \to |R|$.
The order on the flags of $R_t$ is induced by the one on~$\lvert R \rvert$~via~$p_R$.

Let $[\tau_t]$ be the forest made up of the roots of $\tau_t$ and
$\iota \colon \tau_t \to [\tau_t]$ be the graph morphism sending each vertex of
$\tau_t$ to the root below it; $\iota^\circlearrowleft$ induces by
post-composition a morphism
$\overline{h_t} = \iota^\circlearrowleft \circ p_t \colon R_t \to
[\tau_t]^{\circlearrowleft}$. The triple $(R_t, [\tau_t], \overline{h_t})$ is a
$\DiLL_0$ \kl{quasi-proof-structure}, and it is a $\DiLL_0$ \kl{proof-structure} if $R$ is a
We can now define the \emph{Taylor expansion} $\Taylor{R}$ of a quasi-proof-structure $R$ (an example of an element of a Taylor expansion~is~in~\Cref{fig:taylor-expansion}).

\begin{defi}[Taylor expansion]
\label{def:taylor}
Let $R$ be a quasi-proof-structure. The \intro{Taylor expansion} of $R$ is the
set of \polyadic{} quasi-proof-structures
\mbox{$\Taylor{R} = \{ (R_t, [\tau_t], \overline{h_t}) \mid t = (\tau_t, h_t) \in
\ProtoTaylor{R}\}$.}
\end{defi}

An element $(R_t, [\tau_t], \overline{h_t})$ of the Taylor expansion of a quasi-proof-structure $R$
has much less
structure than the pullback $(R_t,p_t,p_R)$: the latter
indeed is a $\DiLL_0$ quasi-proof-structure $R_t$ coming with its projections
$|R| \stackrel{p_R}{\longleftarrow} R_t \stackrel{p_t}{\longrightarrow}
\tau_t^\circlearrowleft$, which establish a precise correspondence between cells and flags of $R_t$ and cells and flags of $R$:
a cell in $R_t$ is labeled (via
the projections) by both the cell of $|R|$ and the branch of the box-forest of $R$ it
arose from.  But $(R_t, [\tau_t], \overline{h_t})$ where $R_t$ is without its
projections $p_t$ and $p_R$ loses the correspondence with
$R $.

\begin{figure}[!t]
\vspace{\beforepn}
\centering
\scalebox{0.75}{
\pnet{
\pnformulae{
~~~\pnf[botax]{$\bot$}~\pnf[1ax]{$\one$}~\pnf[botaxbis]{$\bot$}~\pnf[1axbis]{$\one$}~\pnf[botaxtris]{$\bot$}~\pnf[1axtris]{$\one$}~~~~~\pnf[Y]{$Y$}~\pnf[Yp]{$Y^\bot$} \\
~~\pnf[bot]{$\bot$}~~~~~~~\pnf[1]{$\one$}~\pnf[1bis]{$\one$}~\pnf[1tris]{$\one$} \\
~\pnf[X]{$X$}~~~~~~~~~~~~~~\pnf[1']{$\one$}~\pnf[1'']{$\one$}~\pnf[1''']{$\one$}~\pnf[1'''']{$\one$} \\
\pnf[Xp]{$X^\bot$}~~~~~~\pnf[1cow]{$\oc \one$}
\pnone[1axcell]{1ax}
\pnbot[botaxcell]{botax}
\pnaxiom[axprop]{Xp,X}
\pnone[1axcellbis]{1axbis}
\pnbot[botaxcellbis]{botaxbis}
\pnone[1axcelltris]{1axtris}
\pnbot[botaxcelltris]{botaxtris}
\pnaxiom[axprop']{Y,Yp}
\pnbag{}{1ax}[!1ax]{$\oc 1$}
\pnbag{}{1axbis,1axtris}[!1axtris]{$\oc \one$}[1][.3]
\pninitial{$\oc$}[cow]{1cow}
\pnbot[botcell]{bot}
\pnone[1cell]{1}
\pnone[1cellbis]{1bis}
\pnone[1celltris]{1tris}
\pnbag{}{1,1bis,1tris}[!1]{$\oc \one$}
\pnexp{}{bot,botax,botaxbis,botaxtris}[?bot]{$\wn \bot$}[1.5][-1]
\pnexp{}{!1ax,!1axtris,!1,1cow}[?!1]{$\wn\oc 1$}[1]
\pntensor{X,?bot}[tens]{$X \otimes \wn \bot$}[.9]
\pnexp{}{Y}[?Y]{$\wn Y$}
\pnpar{?Y,Yp}[par]{$\wn Y \parr Y^\bot$}
\pnbag{}{par}[!par]{$\,\,\oc (\wn Y \parr Y^\bot)$}
\pnone[1cell']{1'}
\pnone[1cell'']{1''}
\pnone[1cell''']{1'''}
\pnone[1cell'''']{1''''}
\pnbag{}{1',1'',1''',1''''}[!1']{$\oc 1$}[1.5]
\pnsemiboxc{1axcell,botaxcell,1axcellbis,botaxcellbis,1axcelltris,axprop,Xp,1,1bis,1tris,ax,tens}{green}
\pnsemiboxc{axprop',!1',1'''',Y}{gray}
\qquad
\begin{forest}
for tree={grow'=north, edge=<-, l=0.2pt}
[$ $, edge = green
[$\textcolor{green}{\bullet}$, name = box12,  edge = green]
\coordinate (box12') at ([shift={(90:0.8)}]box12);
\draw[->,dotted,green,line width=1pt] (box12) to[out=north west,
in=south west] (box12');
\draw[->,dotted,green,line width=1pt] (box12') to[out=south east,
in=north east] (box12);
\end{forest}
\
\begin{forest}
for tree={grow'=north, edge=<-, l=0.2pt}
[$ $, edge = gray
[$\textcolor{gray}{\bullet}$, name = box21, edge = gray]
\coordinate (box21') at ([shift={(90:0.8)}]box21);
\draw[->,dotted,gray,line width=1pt] (box21) to[out=north west,
in=south west] (box21');
\draw[->,dotted,gray,line width=1pt] (box21') to[out=south east,
in=north east] (box21);
\end{forest}
\caption{An element $\rho$ of the Taylor expansion of the $\MELL$ quasi-\-proof-structure $R$ in \Cref{fig:pointed-quasi-proof-net}, obtained from the element of $\ProtoTaylor{R}$ in Example~\ref{ex:proto-taylor}.}
\label{fig:taylor-expansion}
\end{figure}

\begin{rem}[conclusions]
\label{rmk:conclusions}
By definition and Remark \ref{rmk:roots}, the Taylor expansion preserves \kl[conclusion of quasi-proof-structure]{conclusions} and \kl[quasi-proof-structure type]{type}: each element of the Taylor expansion of a quasi-proof-structure $R$ has the \emph{same conclusions} and the \emph{same type} as $R$.
More precisely, there is a
bijection $\varphi$ from the conclusions of a quasi-proof-structure $R$ to the
ones in each element $\rho$ of $\Taylor{R}$ such that $i$ and $\varphi(i)$
have the same type and the same root (\ie
$\BoxFunction_{R_F}(i) = \BoxFunction_{\rho_F}(\varphi(i))$ up to the bijection of Remark \ref{rmk:roots}).
So, the \kl[proof-structure type]{types} of $R$ and $\rho$ are the same (as a list of lists).
\end{rem}

\begin{example}[Taylor of the empty]
\label{ex:taylor-empty}
By Definitions \ref{def:proof-structure} and \ref{def:quasi-proof-structure}, the box-tree of $\emptynet$ is just a root with its output and no inputs (we call it a \emph{root-tree}), and the box-forest of $\kl[empty quasi-proof-structure]{n\emptynet}$ is a list of $n$ root-trees, for all $n > 0$; the box-function of $\emptynet$ is the \kl{empty graph morphism} and the box-function of $n\emptynet$ is a list of $n$ such morphisms.
By Remark \ref{rmk:roots}, $\ProtoTaylor{\emptynet}$ (\resp\ $\ProtoTaylor{n\emptynet}$ for all $n \!>\! 0$) is $\{(\tau, h)\}$ where $\tau$ is a root-tree (\resp\ a forest of $n$ root-trees) and $h$ is the \kl{identity graph morphism} on $\tau$.
By Definition \ref{def:taylor}, $\Taylor{\emptynet} = \{\emptynet\}$ and $\Taylor{\kl[empty quasi-proof-structure]{n \emptynet}} = \{n \emptynet\}$~for~all~$n \!>\! 0$.
\end{example}

\subsection{The filled Taylor expansion}
\label{subsec:fat}

As discussed in \Cref{subsec:intro-fattened}
(p.~\pageref{subsec:intro-fattened}), the rewriting rules we will introduce in \Cref{sect:rules} need to ``represent'' the emptiness introduced by the Taylor expansion (taking $0$
copies of a box) so as to preserve the conclusions.
Thus, an element of the \emph{filled Taylor expansion} $\FatTaylor{R}$ of a quasi-proof-structure $R$
(an example is in \Cref{fig:emptyings}) is obtained from an element of $\Taylor{R}$
where some \kl{components} can be erased and replaced by
\kl{daimons} with the same conclusions (hence $\Taylor{R} \subseteq \FatTaylor{R}$).
The filled Taylor expansion (and not the plain one) will play a crucial role in \Cref{sec:naturality} to define a natural transformation.

\begin{defi}[emptying, filled Taylor expansion]
\label{def:FilledTaylor}
The \intro[emptying of proof-structure]{emptying} of a $\DiLL_0$ proof-structure~
$\rho$ with at least one conclusion is a \kl{daimon} whose \kl{conclusions} and \kl[proof-structure type]{type} are the same as $\rho$.

An \intro{emptying} of a \kl[DiLL0 quasi-proof-structure]{$\DiLL_0$ \emph{quasi}-proof-structure} $\rho$ is a $\DiLL_0$ quasi-proof-structure obtained from $\rho$ by replacing
some (possibly none) \kl{components} of $\rho$ having at least one conclusion with their \kl[emptying of proof-structure]{emptying}.

The \intro{filled Taylor expansion} $\FatTaylor{R}$ of a
quasi-proof-structure $R$ is the set of all the emptyings of all the elements of
its Taylor expansion $\Taylor{R}$.

If $\rho = (R_t, [\tau_t], \overline{h_t}) \in \Taylor{R}$, and $r_1, \dots, r_n$ are some roots of  $[\tau_t]$, the \intro[emptying on]{emptying of $\rho$ on $r_1, \dots, r_n$}, denoted by $\rho_{r_1 \dots r_n}$, is the element of $\FatTaylor{R}$ obtained by substituting a daimon
for each component of $\rho$ with at least one conclusion corresponding to the root $r_i$ (\ie, if such a conclusion is an output of a vertex $v$, then $\overline{h_t}_V(v) = r_i$), for all $1 \leqslant i \leqslant n$.
\end{defi}

\begin{figure}[!t]
\vspace{\beforepn}
\centering
\scalebox{0.75}{
\pnet{
\pnformulae{
\pnf[Xp]{$X^\bot$}~~\pnf[tens]{$X\otimes \wn \bot$}~~\pnf[?!1]{$\wn\oc 1$}~~~\pnf[YY]{$\oc (\wn Y \parr Y^\bot)$}
\pndaimon[dai]{Xp,tens,?!1}
\pncown[!par]{YY}
\pnone[1cell']{1'}
\pnone[1cell'']{1''}
\pnbag{}{1',1''}[!1']{$\oc 1$}
\pnsemiboxc{dai,Xp,tens,?!1}{green}
\pnsemiboxc{YY,1cell',1cell'',!par,yg}{gray}
\qquad
\quad
\raisebox{-.5cm}{
\begin{forest}
for tree={grow'=north, edge=<-, l=0.2pt}
[$ $, edge = green
[$\textcolor{green}{\bullet}$, name = box12, edge = green]
\coordinate (box12') at ([shift={(90:0.8)}]box12);
\draw[->,dotted,green,line width=1pt] (box12) to[out=north west,
in=south west] (box12');
\draw[->,dotted,green,line width=1pt] (box12') to[out=south east,
in=north east] (box12);
\end{forest}
\
\begin{forest}
for tree={grow'=north, edge=<-, l=0.2pt}
[$ $, edge = gray
[$\textcolor{gray}{\bullet}$, edge = gray]
\coordinate (box21') at ([shift={(90:0.8)}]box21);
\draw[->,dotted,gray,line width=1pt] (box21) to[out=north west,
in=south west] (box21');
\draw[->,dotted,gray,line width=1pt] (box21') to[out=south east,
in=north east] (box21);
\end{forest}
\quad
\caption{An element of the filled Taylor expansion of the $\MELL$ quasi-proof-structure $R$ in \Cref{fig:pointed-quasi-proof-net}, obtained as an emptying of $\rho$ in~\Cref{fig:taylor-expansion}.}
\label{fig:emptyings}
\end{figure}

\begin{remark}[conclusions of emptying]
\label{rmk:conclusions-emptying}
By construction, the \kl{filled Taylor expansion} preserves conclusions and type, as the Taylor expansion does (Remark \ref{rmk:conclusions}):  conclusions and type of a quasi-proof-structure $R$ and of \emph{any} emptying of \emph{any} element of $\Taylor{R}$ are the same.
\end{remark}

\begin{example}[filled Taylor of the empty]
\label{ex:filled-taylor-empty}
From Example \ref{ex:taylor-empty} and Definition \ref{def:FilledTaylor}, it follows that $\Taylor{\emptynet} = \{\emptynet\} = \FatTaylor{\emptynet}$ and for every $n > 0$, $\Taylor{n\emptynet} = \{\kl[empty quasi-proof-structure]{n \emptynet}\} = \FatTaylor{\kl[empty quasi-proof-structure]{n\emptynet}}$.
\end{example}

\begin{remark}[connection]
\label{rmk:connection}
The Taylor expansion does not ``create connection''; the filled Taylor expansion does, but only in a component that has been filled by a daimon.
More precisely, let $i$ and $j$ be conclusions of a quasi-proof-structure $R = (|R|, \ForestT_R, \BoxFunction_R)$, let $\rho = \allowbreak(|\rho|, \ForestT_\rho, \BoxFunction_{\rho}) \!\in \Taylor{R}$
and let $\rho_{r_1 \dots r_n} \in \FatTaylor{R}$ be the \kl[emptying on]{emptying of $\rho$ on} the roots $r_1, \dots, r_n$.
If $i$ and $j$ are not connected in the (undirected) \kl[undirected graph]{graph} $\lVert R \rVert$ of $R$, then $i$ and $j$ are not connected in the (undirected) graph $\lVert \rho \rVert$ of $\rho$.
And if $i$ and $j$ are connected in the (undirected) graph of $\lVert \rho_{r_1 \dots r_n} \rVert$ of $\rho_{r_1 \dots r_n}$, then $i$ and $j$ are output tails of the same $\maltese$-cell in $\rho_{r_1 \dots r_n}$.

\end{remark}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "mainFinal"
%%% End:

% !TEX root = mainFinal.tex
\section{Means of destruction: unwinding \texorpdfstring{$\MELL$}{MELL} quasi-proof-structures}
\label{sect:rules}

\begin{figure}[!t]
\centering
\small
\arraycolsep=1.4pt
(\Gamma_1; \cdots ; \Gamma_k, \FlagType(i), \FlagType(i\!+\!1), \Gamma_{k}'; \cdots; \Gamma_n)
&(\Gamma_1; \cdots ; \Gamma_k, \FlagType(i\!+\!1),  \FlagType(i), \Gamma_{k}'; \cdots; \Gamma_n)
\\
(\Gamma_1; \cdots ; \Gamma_{k}, \FlagType(i), \FlagType(i\!+\!1), \Gamma_{k}'; \cdots; \Gamma_n)
&(\Gamma_1; \cdots ; \Gamma_{k}, \FlagType(i); \FlagType(i\!+\!1), \Gamma_{k}'; \cdots; \Gamma_n)
\\
(\Gamma_1; \cdots ; \Gamma_{k\!-\!1}; \FlagType(i\!-\!1), \FlagType(i); \Gamma_{k\!+\!1}; \cdots; \Gamma_n)
&(\Gamma_1; \cdots ; \Gamma_{k\!-\!1}; \emptylist; \Gamma_{k\!+\!1} ; \cdots; \Gamma_n) \text{ if } \FlagType(i\!-\!1) = \FlagType(i)^\bot \text{ \kl{atomic}}
\\
(\Gamma_1; \cdots ; \Gamma_{k}; \cdots; \Gamma_n)
&(\Gamma_1; \cdots ; \Gamma_k, \FlagType(i), \FlagType(i\!+\!1); \cdots; \Gamma_n)
\text{ if } \FlagType(i) = \FlagType(i\!+\!1)^\bot
\\
(\Gamma_1; \cdots ; \Gamma_{k\!-\!1}; \FlagType(i); \Gamma_{k\!+\!1}; \cdots; \Gamma_n)
&(\Gamma_1; \cdots ; \Gamma_{k\!-\!1}; \emptylist; \Gamma_{k\!+\!1} ; \cdots; \Gamma_n) \text{ if } \FlagType(i) = \One
\\
(\Gamma_1; \cdots; \Gamma_{k\!-\!1}; \FlagType(i); \Gamma_{k\!+\!1}; \cdots; \Gamma_n)
&(\Gamma_1; \cdots ; \Gamma_{k\!-\!1}; \emptylist; \Gamma_{k\!+\!1}; \cdots; \Gamma_n)  \text{ if } \FlagType(i) = \bot
\\
(\Gamma_1; \cdots ; \Gamma_k, \FlagType(i); \cdots; \Gamma_n)
&(\Gamma_1; \cdots ; \Gamma_{k}, A, B; \cdots; \Gamma_n) \text{ if } \FlagType(i) = A \otimes B
\\
(\Gamma_1; \cdots ; \Gamma_{k}, \FlagType(i); \cdots; \Gamma_n)
&(\Gamma_1; \cdots ; \Gamma_{k}, A, B; \cdots; \Gamma_n) \text{ if } \FlagType(i) = A \parr B
\\
(\Gamma_1; \cdots ; \Gamma_{k}, \FlagType(i); \cdots; \Gamma_n)
&(\Gamma_1; \cdots ; \Gamma_{k}, \wn A, \wn A; \cdots; \Gamma_n) \text{ if } \FlagType(i) = \wn A
\\
(\Gamma_1; \cdots ; \Gamma_{k}, \FlagType(i); \cdots; \Gamma_n)
&(\Gamma_1; \cdots ; \Gamma_{k}, A; \cdots; \Gamma_n)
\text{ if } \FlagType(i) = \wn A
\\
(\Gamma_1; \cdots ; \Gamma_{k\!-\!1}; \FlagType(i); \Gamma_{k\!+\!1}; \cdots; \Gamma_n)
&(\Gamma_1; \cdots ; \Gamma_{k\!-\!1}; \emptylist; \Gamma_{k\!+\!1} ; \cdots; \Gamma_n) \text{ if } \FlagType(i) = \wn A
\\
(\Gamma_{\!1}; \cdots ; \Gamma_{\!k\!-\!1}; \wn A_1, \overset{p \geqslant 0}{\dots}, \wn A_p, \FlagType(i); \Gamma_{\!k\!+\!1}\cdots; \Gamma_{\!n})
&(\Gamma_{\!1}; \cdots ; \Gamma_{\!k\!-\!1}; \wn A_1, \overset{p \geqslant 0}{\dots}, \wn A_p, A; \Gamma_{\!k\!+\!1}; \cdots; \Gamma_{\!n}) \text{ if } \FlagType(i) = \oc A
\end{array}$
\caption{The generators of $\Scheduling$.
In the source $\Gamma$ of each arrow, $\FlagType(i)$
is the $i^\text{th}$ formula in the \kl{flattening} of $\Gamma$ (the
arrow's name keeps track~of~$i$).
The $\Gamma_k$'s are (possibly empty) lists of \MELL formulas.}
\label{fig:elementary-schedulings}
\end{figure}

Our aim is to deconstruct ($\MELL$ or \polyadic) proof-structures
from their conclusions.
To do that, we introduce the category of schedulings.
The arrows of this category are sequences of deconstructing
rules, acting on lists of lists of \MELL formulas.
These arrows act through functors on (\MELL or $\DiLL_0$) quasi-proof-structures, exhibiting their sequential structure.

\begin{defi}[the category $\Scheduling$]
\label{def:unwinding-paths}
Let $\Scheduling$ be the category of \kl{schedulings} whose
\begin{itemize}
\item objects are lists $\Gamma = (\Gamma_1; \cdots; \Gamma_n)$ of lists of
$\MELL$ formulas, with $n \geqslant 0$;

\item arrows are freely generated by composition of the \intro{elementary
schedulings} in \Cref{fig:elementary-schedulings};
identities are the empty sequence of elementary schedulings, called \intro{empty scheduling}.
\end{itemize}
A \intro{scheduling} is any arrow $\sched \colon \Gamma \to \Gamma'$ in $\Scheduling$.
We write the composition of schedulings
by juxtaposition in the diagrammatic
order; so, if $\sched \colon \Gamma \to \Gamma'$ and
$\sched' \colon \Gamma' \to \Gamma''$, then~$\sched\sched' \colon \Gamma\to \Gamma''$.
If $\sched = a_1 \cdots a_k$ where $k \geqslant 0$ and the $a_i$'s are elementary schedulings, the \intro{length} of $\sched$ is $k$.
\end{defi}

Reading \Cref{fig:elementary-schedulings} left-to-right, $\Mix_{i}$ is the only elementary scheduling that changes (and increases) the number of lists in a list $\Gamma$ of lists of \MELL formulas.
The only elementary schedulings decreasing the number of \MELL formulas in the \kl{flattening} of $\Gamma$ are $\Ax_{i}, \One_i, \bot_{i}, \Weak_i$.

\begin{exa}
\label{ex:barbara-path}
$\parr_1 \, \parr_2 \, \parr_3 \, \otimes_1 \, \otimes_3 \, \Ex_1 \, \Ex_2 \, \Mix_{2}
\, \Ax_2 \, \Ex_2 \, \Mix_{2} \, \Ax_2 \, \Ax_2$ is a scheduling
from $\big((X \otimes Y^\bot) \parr ((Y \otimes Z^\bot) \parr (X^\bot \parr	Z))\big)$
to $3\emptylist$, the list of 3 \kl{empty lists} of \MELL formulas.
\end{exa}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "mainFinal"
%%% End:

% !TEX root = mainFinal.tex

The category $\Scheduling$ acts on \kl{$\MELL$ quasi-proof-structures}, exhibiting a
sequential structure in their construction, by means of the rewrite rules in \Cref{fig:actions-all} (Definition \ref{def:unwinding}).
To ease their reading, we make explicit the name of the active conclusions (to be intended as positive integers), we only draw the components affected by the rewrite rule and omit the ones left unchanged;
\eg{}, if the affected component consists only of an $\Ax$-cell whose outputs are the conclusions $i\!-\!1$ and $i$, we write
\parbox[b][1.5\baselineskip]{1.05cm}{
\(
\scalebox{\smallproofnets}{
\pnet{
\pnformulae{
\pnf[i]{$\,\,\,i\!-\!1$}~\pnf[j]{$i$}
\pnaxiom[ax]{i,j} [0.8]
\pnsemibox{ax}
\)
} ignoring the other components.
Given a list $\Gamma$ of lists of $\MELL$ formulas, $\MELLFunctor(\Gamma)$ is the set of \kl{$\MELL$ quasi-proof-structures} of type $\Gamma$.

\begin{figure}[t]
\vspace{\beforepn}
\centering
\begin{subfigure}[c]{0.4\textwidth}
\begin{align*}
\pnet{
\pnsomenet[u]{}{2cm}{0.7cm}[at (-1,0.75)]
\pnoutfromswitch{u.-153}[A]{$\Gamma_k\,$}
\pnoutfrom{u.-135}[B]{$i$}
\pnoutfrom{u.-65}[A']{$i\!+\!1$}
\pnoutfromswitch{u.-27}[B']{$\,\,\Gamma_{k}'$}
\pnsemibox{u,A,A',B,B'}
\pnrewrite[\Ex_{i}]
\pnet{
\pnsomenet[u]{}{2cm}{0.7cm}[at (-1,0.75)]
\pnoutfromswitch{u.-153}[A]{$\Gamma_{k}\,$}
\pnoutfrom{u.-110}[B]{$i\!+\!1$}
\pnoutfrom{u.-45}[A']{$i$}
\pnoutfromswitch{u.-27}[B']{$\,\,\Gamma_{k}'$}
\pnsemibox{u,A,B,A',B'}
\end{align*}
\vspace{-\baselineskip}
\caption{Exchange}
\label{fig:exc}
\end{subfigure}\hfill%
\begin{subfigure}[c]{0.4\textwidth}
\begin{align*}
\pnet{
\pnsomenet[u]{}{1cm}{0.7cm}[at (-1,0.75)]
\pnoutfromswitch{u.-125}[A]{$\Gamma_k\,$}
\pnoutfrom{u.-55}[B]{$i$}
\pnsomenet[u']{}{1cm}{0.7cm}[at (0.3,0.75)]
\pnoutfrom{u'.-127}[A']{$i\!+\!1$}
\pnoutfromswitch{u'.-52}[B']{$\,\,\Gamma_k'$}
\pnsemibox{u,u',A,A',B,B'}
\pnrewrite[\Mix_{i}]
\pnet{
\pnsomenet[u]{}{1cm}{0.7cm}[at (-1,0.75)]
\pnoutfromswitch{u.-125}[A]{$\Gamma_{k}$}
\pnoutfrom{u.-55}[B]{$i$}
\pnsomenet[u']{}{1cm}{0.7cm}[at (0.8,0.75)]
\pnoutfrom{u'.-127}[A']{$i\!+\!1$}
\pnoutfromswitch{u'.-52}[B']{$\,\,\Gamma_k'$}
\pnsemibox{u,A,B}
\pnsemibox{u',A',B'}
\end{align*}
\vspace{-\baselineskip}
\caption{Mix}
\label{fig:mix}
\end{subfigure}
\begin{subfigure}[c]{0.3\textwidth}
\vspace*{-\baselineskip}
\begin{align*}
\pnet{
\pnformulae{
\pnaxiom[ax]{i,j}
\pnsemibox{ax,i,j}
\pnrewrite[\Ax_{i}]
\pnet{
\pnformulae{
\pnf[empty]{}
\pnsemibox{empty}
\end{align*}
\vspace{-\baselineskip}
\caption{Hypothesis (\(\Ax, \One, \bot, \Weak\))}
\label{fig:hypothesis}
\end{subfigure}\hfill%
\begin{subfigure}[c]{0.4\textwidth}
\begin{align*}
\pnet{
\pnsomenet[u]{}{1.75cm}{0.7cm}[at (-2,0)]
\pnoutfromswitch{u.-150}[k]{$\Gamma_{\!k}$}
\pnoutfrom{u.-95}[A]{$A$}
\pnoutfrom{u.-30}[B]{$\,A^\bot$}
\pncut[cut]{A,B}
\pnsemibox{u,cut}
\pnrewrite[\Cut^i]
\pnet{
\pnsomenet[u]{}{1.75cm}{0.7cm}[at (-2,0)]
\pnoutfromswitch{u.-150}[k]{$\Gamma_{\!k}$}
\pnoutfrom{u.-95}[B]{$i$}
\pnoutfrom{u.-30}[A]{$\,i\!+\!1$}
\pnsemibox{u,A,B}
\end{align*}
\vspace{-3\baselineskip}
\caption{Cut}
\label{fig:cut}
\end{subfigure}
\begin{subfigure}[b]{0.4\textwidth}
\begin{align*}
\pnet{
\pnsomenet[u]{}{1.75cm}{0.7cm}
\pnoutfromswitch{u.-150}[k]{$\Gamma_{\!k}$}
\pnoutfrom{u.-95}[A]{$A$}
\pnoutfrom{u.-30}[B]{$B$}
\pntensor{A,B}[i]{$i$}
\pnsemibox{u,k,A,B,i}
\pnrewrite[\otimes_i]
\pnet{
\pnsomenet[u]{}{1.75cm}{0.7cm}
\pnoutfromswitch{u.-150}[k]{$\Gamma_{\!k}$}
\pnoutfrom{u.-95}[A]{$i$}
\pnoutfrom{u.-30}[B]{$\,i\!+\!1$}
\pnsemibox{u,k,A,B}
\end{align*}
\vspace{-\baselineskip}
\caption{Multiplicative (\(\otimes, \parr\))}
\label{fig:tensor}
\end{subfigure}\hfill%
\begin{subfigure}[b]{0.4\textwidth}
\begin{align*}
\pnet{
\pnsomenet[u]{}{1.75cm}{0.7cm}
\pnoutfromswitch{u.-150}[k]{$\Gamma_{k}$}
\pnoutfromswitch{u.-95}[C]{$A$}
\pnoutfromswitch{u.-30}[D]{$A$}
\pnexp{}{C*, D*}[i]{$i$}
\pnsemibox{u,i}
\pnrewrite[\Contr_i]
\pnet{
\pnsomenet[u]{}{1.75cm}{0.7cm}
\pnoutfromswitch{u.-150}[k]{$\Gamma_{k}$}
\pnoutfromswitch{u.-95}[C]{$A$}
\pnexp{}{C*}[i]{$i$}
\pnoutfromswitch{u.-30}[D]{$A$}
\pnexp{}{D*}[i1]{$i\!+\!1$}
\pnsemibox{u,i,i1}
\end{align*}

\vspace{-\baselineskip}
\caption{Contraction}
\label{fig:contraction}
\end{subfigure}
\begin{subfigure}[b]{0.4\textwidth}
\begin{align*}
\pnet{
\pnsomenet[u]{}{1.25cm}{0.7cm}
\pnoutfromswitch{u.-130}[k]{$\Gamma_k$}
\pnoutfrom{u.-50}[A]{$A$}
\pnexp{}{A}[i]{$i$}
\pnsemibox{u,k,A,i}
\pnrewrite[\Der_i]
\pnet{
\pnsomenet[u]{}{1.25cm}{0.7cm}
\pnoutfromswitch{u.-130}[k]{$\Gamma_{k}$}
\pnoutfrom{u.-50}[A]{$i$}
\pnsemibox{u,k,A}
\end{align*}
\vspace{-\baselineskip}
\caption{Dereliction}
\label{fig:dereliction}
\end{subfigure}\hfill%
\begin{subfigure}[b]{0.4\textwidth}
\begin{align*}
\pnet{
\pnsomenet[u]{}{2cm}{0.7cm}
\pnbox{u}
\pnoutfrom{u.-25}[pi1c]{$A$}
\pnbag{}{pi1c}{$i$}
\pnoutfromswitch{u.-65}[ap]{$-$}
\pnexp{}{ap*}[?ap]{\small $\,\wn A_{p}$}
\pnoutfromswitch{u.-155}[a1]{$-$}
\pnexp{}{a1*}[?a1]{\small $\quad\wn A_1 \overset{p \geqslant 0}{\cdots}$}
\pnsemibox{pi1c,ap,?ap,u}
\pnrewrite[\BoxR_{i}]
\pnet{
\pnsomenet[u]{}{2cm}{0.7cm}
\pnoutfrom{u.-25}[pi1c]{$i$}[2.5cm][]
\pnoutfromswitch{u.-65}[ap]{$-$}
\pnexp{}{ap*}[?ap]{\small$\,\wn A_{p}$}
\pnoutfromswitch{u.-155}[a1]{$-$}
\pnexp{}{a1*}[?a1]{\small $\quad\wn A_1 \overset{p \geqslant 0}{\cdots}$}
\pnsemibox{u,pi1c,ap,?ap}
\end{align*}
\vspace{-\baselineskip}
\caption{Box}
\label{fig:box}
\end{subfigure}
\caption{\mbox{Action of elementary schedulings on \MELL quasi-proof-structures.}}
\label{fig:actions-all}
\end{figure}

\begin{defi}[action of schedulings on $\MELL$ quasi-proof-structures]
\label{def:unwinding}
An \kl{elementary scheduling} {$a \colon \Gamma \to \Gamma'$} defines a
relation $\mathop{\pnrewrite[a]} \subseteq \MELLFunctor(\Gamma) \times \MELLFunctor(\Gamma')$, called the \intro[action of elementary scheduling]{action} of $a$, as the smallest relation containing all the cases in
\Cref{fig:actions-all}, with the following remarks:
\begin{description}
\item[exchange] $\pnrewrite[\Ex_i]$ swaps the order of two consecutive conclusions in the same component.

\item[mix] given a \kl{component} $R$ with at least two conclusions $i$ and $i\!+\!1$ such that no conclusion $j \leqslant i$ is \kl{connected} in $\lVert R \rVert$ to any conclusion $j' \geqslant i\!+\!1$, $\!\pnrewrite[\!\Mix_i\!]$ splits $R$ into two components, one with the conclusions $j \leqslant i$, the other with the conclusions $j' \geqslant i\!+\!1$.\footnotemark
\footnotetext{See \Cref{note:split-tree} for a more precise account.
Read in reverse, $\Mix_{i}$ is analogous to the mix rule in the sequent calculus for $\MELL$: it merges two components into one component putting together their conclusions.}

\item[hypothesis] if  $a\in \{\Ax_{i}, \One_i, \bot_i, \Weak_i \}$,
$\pnrewrite[a]$ deletes an \kl{hypothesis} (\ie a \kl{cell} without inputs) that is the only
cell in its \kl{component}, yielding an \kl[empty proof-structure]{empty} component.
We have drawn the case $\Ax$ in
\Cref{fig:hypothesis}, the other cases ($\One$, $\bot$, $\wn$) are similar, except for the number of conclusions.

\item[cut] read in reverse, $\pnrewrite[\Cut^i]$ relates a quasi-proof-structure with two conclusions $i$
and $i+1$ with the quasi-proof-structure where these two
conclusions are cut by a $\cut$-\kl{cell} of \kl{depth} $0$.
This rule, from left to right, is nondeterministic (as there are many possible cuts).

\item[multiplicative] if $a \in \{\otimes_i, \parr_i\}$,
$\pnrewrite[a]$ deletes a cell labeled by a multiplicative connective, $\otimes$ or $\parr$.
The new conclusions $i$ and $i+1$ inherit the order from the inputs of the erased cell.
We have only drawn the case $\otimes$ in \Cref{fig:tensor}, the case $\parr$ is

\item[contraction] $\pnrewrite[\Contr_i]$ splits a $\wn$-\kl{cell} with $h+k$ inputs into two
$\wn$-cells (so, it duplicates a $\wn$-cell) with $h$ and $k$ inputs, respectively (\(h,k \geqslant 0\)).
The rule, from left to right, \mbox{is nondeterministic}.

\item[dereliction] $\pnrewrite[\Der_i]$ only applies if the $\wn$-\kl{cell} (with $1$ input) does not
shift a level in the \kl{box-forest}, \ie it is not just outside a \kl{box}
(otherwise $\mathop{\pnrewrite[\Der_i]}$ would not yield a \mbox{$\MELL$ quasi-proof-structure)}.

\item[box] $\pnrewrite[\BoxR_i]$ only applies if a box (and its border) is alone in its \kl{component}.
In particular, each $\wn$-cell represented in \Cref{fig:box} has at least one input (this is what ``$-$'' stands for).
\end{description}

The rewrite relation is extended by composition of relations to define, for every \kl{scheduling} $\sched \colon \Gamma \to \Gamma'$, a relation $\mathop{\pnrewrite[\sched]} \subseteq \MELLFunctor(\Gamma) \times \MELLFunctor(\Gamma')$, called the \intro[action of scheduling]{action} of $\sched$.\footnotemark
\footnotetext{That is,
given the schedulings $\sched \colon \Gamma \to \Gamma'$ and $\sched' \colon \Gamma' \to \Gamma''$ and the quasi-proof-structures $R \in \MELLFunctor(\Gamma)$ and $R'' \in \MELLFunctor(\Gamma'')$, $R \pnrewrite[\sched\sched'] R''$ if and only if there is $R' \in \MELLFunctor(\Gamma')$ such that $R \pnrewrite[\sched] R'$ and $R' \pnrewrite[\sched'] R''$ (often denoted by $R \pnrewrite[\sched] \, \pnrewrite[\sched'] R''$).
The action of the \kl{empty scheduling} is the identity relation.}
\end{defi}

Except $\Mix_i$, $\Ex_i$ and $\Contr_i$, the \kl[action of elementary scheduling]{action} of an \kl{elementary scheduling} is a rewrite rule on \MELL quasi-proof-structures that destroys either a $\cut$-cell of \kl{depth} $0$ or a cell whose output is a conclusion.
The types of the conclusions are updated according to \Cref{fig:elementary-schedulings}.
The \kl[action of scheduling]{action of a scheduling} is just
the composition of a number (possibly none) of these rewrite rules.

The action of schedulings cannot decrease the number of components of a \MELL quasi-proof-structure, and the action of $\Mix_{i}$ is the only one that increases this number.

Among the \kl[action of elementary scheduling]{actions} of \kl{elementary schedulings} in \Cref{fig:actions-all}, the cases $\Mix$ and  $\BoxR$
are the only ones that change
the \kl{box-forest} of a quasi-proof-structure: $\Mix$ splits a tree in two distinct trees by splitting its root, while $\BoxR$ merges a root of a tree with a non-root vertex just above it.
For instance, the action $\Mix_i$ rewrites the \MELL proof-structure $S$ in \Cref{fig:pointed-proof-net} to the \MELL quasi-proof-structure $R$ in \Cref{fig:pointed-quasi-proof-net}, when $i$ is the conclusion of $S$ of type $\wn\oc \one$.

The way the \kl[action of elementary scheduling]{action of an elementary scheduling} is defined (Definition \ref{def:unwinding}) automatically rules out the possibility that a \MELL quasi-proof-structure rewrites to a \kl{module} that is not a \MELL quasi-proof-structure.
For instance, the elementary scheduling $\Der_1$ cannot \kl[action of elementary scheduling]{act} on the \MELL proof-structure $Q$ below, because it would yield a module $Q'$ that is not a \MELL quasi-proof-structure, as in $Q'$ it would be impossible to define a \kl{box-function}  that fulfills the constraints of Definition \ref{def:proof-structure} for \MELL (see \Cref{note:border});
$Q'$ is just a $\DiLL_0$ proof-structure.

\begin{center}
\vspace{\beforepn}
$Q \ = $
\scalebox{0.8}{
\pnet{
\pnformulae{
\pnf[i]{$X$}~\pnf[j]{$ X^\bot$}
\pnexp{}{i}[i']{$\wn X$}[1.2]
\pnbag{}{j}[j']{$\oc X^\bot$}[1.2]
\pnbox{i,j,ax}
\pnaxiom[ax]{i,j}
$ \ \ \not\pnrewrite[\Der_{1}] \ $
\scalebox{0.8}{
\pnet{
\pnformulae{
\pnf[i]{$X$}~\pnf[j]{$ X^\bot$}
\pnbag{}{j}[j']{$\oc X^\bot$}
\pnaxiom[ax]{i,j}
$= \ Q'$
\end{center}

\kl[action of scheduling]{Actions of schedulings} can been seen as arrows in the category $\Rel$ of sets and relations.

\begin{defi}[functor $\MELLFunctor$]
\label{def:FunctorMELL}
We define a functor \intro[mell functor]{$\MELLFunctor \colon \Scheduling \to \Rel$} by:
\begin{itemize}
\item \emph{on objects:} for every list $\Gamma$ of lists of \MELL formulas, $\MELLFunctor(\Gamma)$ is the set of $\MELL$
quasi-proof-structures of type $\Gamma$;
\item \emph{on arrows:} for any $\sched \colon \Gamma \to \Gamma'$,
$\MELLFunctor(\sched)$ is $\pnrewrite[\sched] \colon \MELLFunctor(\Gamma) \to \MELLFunctor(\Gamma')$ (Definition~\ref{def:unwinding}).
\end{itemize}
\end{defi}

Lemmas \ref{prop:unwinding-co-functional}, \ref{lem:cell-or-mix}, \ref{lemma:contraction} and Proposition~\ref{prop:unwinding-to-empty} express some properties of our rewrite rules.

\begin{lem}[co-functionality]
\label{prop:unwinding-co-functional}
Let $\sched \colon \Gamma \to \Gamma'$ be a \kl{scheduling}.
The action $\pnrewrite[\sched]$ of $\sched$ is a co-function
from $\MELLFunctor(\Gamma)$ to $\MELLFunctor(\Gamma')$,
that is,
a function $ \op{\pnrewrite[\sched]} \colon \MELLFunctor(\Gamma') \to \MELLFunctor(\Gamma)$.
\end{lem}

Let $R, R'$ be \MELL quasi-proof-structures, $a$ be an \kl{elementary scheduling}.
We say that:
\begin{itemize}
\item $a$ \intro{applies} to $R$ if $R\pnrewrite[\!\Ex_{i_1}\!\dots\Ex_{i_n}a\!]R'$
for some elementary schedulings $\Ex_{i_1},\dots,\Ex_{i_n}$ ($n \!\geqslant\! 0$);

\item $R \pnrewrite[a] R'$ is \intro[nullary splitting for elementary scheduling]{nullary $\Contr$-splitting} if $a = \Contr_{i}$ and its action from $R$ to $R'$ splits the $\wn$-\kl{cell} of $R$ with output $i$ and $h \geqslant 0$ inputs into
two $\wn$-cells, one with $h$ inputs and one with $0$ inputs.
\end{itemize}

\begin{lem}[applicability of elementary scheduling]
\label{lem:cell-or-mix}
Let $R$ be a non-empty $\MELL$ quasi-proof-structure.
Then an \kl{elementary scheduling}
$a\in \{\Mix_i, \Ax_i, \One_i, \bot_i, \otimes_i, \allowbreak \parr_i, \Contr_i, \Der_i, \Weak_i,
\Cut^i,	\allowbreak \BoxR_{i}\}$ \kl{applies} to $R$, for some conclusion $i$ of $R$ (or input $i$ of a $\cut$-cell of \kl{depth} $0$ in $R$).

No elementary scheduling applies to an \kl[empty quasi-proof-structure]{empty} quasi-proof-structure.
\end{lem}

To deconstruct a \MELL quasi-proof-structure $R$, nullary $\Contr$-splitting actions are problematic because	they increase any reasonable size for $R$.
Luckily, the lemma below says roughly that, in \MELL, nullary $\Contr$-splitting actions are superfluous as means of destruction.
Remark \ref{rmk:nullary-splitting} will show that they are needed to achieve the naturality result (\Cref{thm:projection-natural}).

\begin{lemma}[splitting]
\label{lemma:contraction}
Let $R$ be a \MELL quasi-proof-structure with at least a conclusion $i$.
If $a = \Contr_{i}$  and $R \pnrewrite[a] R'$ is \kl[nullary splitting for elementary scheduling]{nullary $\Contr$-splitting}, then for some \MELL quasi-proof-structure $S$:
\begin{enumerate}
\item	either $i$ is the output of a $\wn$-cell of $R$ with $k \!\geqslant\! 2$ inputs and $R \!\pnrewrite[\!a]\! S$ is not nullary $\Contr\!$-splitting;

\item\label{p:cell-or-mix-der}
or $i$ is the output of a $\wn$-cell of $R$ with $0/1$ inputs and in the same component as $i$ there are conclusions $i_0, \dots, i_n$ with $n \!\geqslant\! 0$ (possibly $i \!=\! i_j$ or $i_j \!=\! i_{j'}$ for some $0 \leqslant j,j' \!\leqslant n$; $i_0$ may also be an input of a $\cut$-cell of \kl{depth} $0$) such that $R \pnrewrite[\!\Ex_{i_1} \!\dots \Ex_{i_n}\!] S' \pnrewrite[\!a'\!] S$ with $a' \in \allowbreak \{\Mix_{i_0}, \allowbreak\BoxR_{i_0}, \allowbreak\otimes_{i_0}, \parr_{i_0}, \Cut^{i_0}, \Der_{i_0}, \Weak_{i_0}, \Contr_{i_0}\}$ and if $a' = \Contr_{i_0}$ then $S' \pnrewrite[\!a'\!] S$ is not nullary~$\Contr$-splitting.

\end{enumerate}
\end{lemma}

Lemmas \ref{prop:unwinding-co-functional}, \ref{lem:cell-or-mix} and \ref{lemma:contraction} are proven by simple inspection of the rewrite rules in \Cref{fig:actions-all}.
The proof of Lemma \ref{prop:unwinding-co-functional} has a subtle case:
given $R' \!\in \MELLFunctor(\Gamma')$, if $\sched = \Contr_i$ there is a (unique) $R \in \MELLFunctor(\Gamma)$ such that $R\pnrewrite[\sched] R'$ because any conclusion of $R'$ of type $\wn A$ is the output of a $\wn$-cell (thanks to atomic axioms, \Cref{note:atomic};
for non-atomic axioms,~see~\Cref{sect:nonatomic}).

Given a scheduling $\sched$, we say $R \pnrewrite[\sched] R'$ \intro[nullary splitting for scheduling]{has nullary $\Contr$-splittings} if there is an elementary scheduling $a$ such that $R \pnrewrite[\sched] R' = R \pnrewrite[\sched_{1}] R_1 \pnrewrite[a] R_2 \pnrewrite[\sched_2] R'$ and $R_1 \pnrewrite[a] R_2$ is nullary $\Contr$-splitting.

Every \MELL quasi-proof-structure can be unwound from its conclusions to an \kl[empty quasi-proof-structure]{empty} one by the action of some scheduling, and nullary $\Contr$-splittings are not needed for that.

\begin{prop}[normalization]
\label{prop:unwinding-to-empty}
Let $R$ be a $\MELL$ quasi-proof-structure of \kl[quasi-proof-structure type]{type} $\Gamma$.
Then, there exists a \kl{scheduling} $\sched \colon \Gamma \to \emptylists$ such that $R \pnrewrite[\sched] \emptynets$, without nullary $\Contr$-splittings.
\end{prop}

\begin{proof}
Let the \emph{size} of a \MELL quasi-proof-structure $R$ be the triple $(p,q,r)$ where:
\begin{itemize}
\item $p$ is the (finite) multiset of the number of inputs of each $\wn$-cell in $R$;
\item $q$ is the number of cells in $R$;
\item $r$ is the (finite) multiset of the number of \kl{conclusions} of each \kl{component} of $R$.
\end{itemize}
Multisets are well-ordered as usual, triples are well-ordered lexicographically.

By Lemmas \ref{lem:cell-or-mix} and \ref{lemma:contraction}, it suffices to show that such a size is left unchanged by $\pnrewrite[\!\Ex_{i}]$ and decreases with any action of $\Contr_i$ that is not nullary $\Contr$-splitting ($p$ decreases) and with any action in \Cref{fig:actions-all} other than the ones of $\Ex_{i}$ and $\Contr_{i}$ (the action of $\Mix_{i}$ leaves $p$ and $q$ unchanged and decreases $r$; the remaining actions leave $p$ unchanged and decrease $q$).
\end{proof}

Proposition \ref{prop:unwinding-to-empty} and the last statement in Lemma \ref{lem:cell-or-mix} imply that actions of elementary schedulings define a weakly normalizing rewrite system on \MELL quasi-proof-structures:
the normal forms are exactly the empty quasi-proof-structures $n \emptynet$, for all $n > 0$.
This rewrite system is not strongly normalizing because of the actions of $\Ex_i$ and, more significantly, $\Contr_i$ when are nullary $\Contr$-splitting.
An example of an indefinitely extendable rewriting is~below.

\vspace{\beforepn}
\begin{center}
\scalebox{0.8}{
\pnet{
\pnformulae{\pnf[X]{$\wn \one$}}
\pnwn[cown]{X}
\ \ $\pnrewrite[\Contr_1]$ \ \
\scalebox{0.8}{
\pnet{
\pnformulae{\pnf[X]{$\wn \one$}~\pnf[X']{$\wn \one$}}
\pnwn[cown]{X}
\pnwn{X'}
\ \ $\pnrewrite[\Contr_1]$ \ \
\scalebox{0.8}{
\pnet{
\pnformulae{\pnf[X]{$\wn \one$}~\pnf[X']{$\wn \one$}~\pnf[X'']{$\wn \one$}}
\pnwn[cown]{X}
\pnwn{X'}
\pnwn{X''}
\ \ $\pnrewrite[\Contr_1]$ \ \
\dots
\end{center}

The action of a scheduling $\sched$ such that $R \pnrewrite[\sched] \emptynets$, read
backward, can be seen as a
sequence of elementary steps to build the $\MELL$ quasi-proof-structure $R$ from an empty one $\emptynets$.
An example of a rewriting from some $R$ to $\emptynets$ is in \Cref{fig:longex2} (\Cref{sec:glueable}).
Intuitively, a \kl{scheduling} $\sched \colon (\Gamma) \to \emptylists\,$ ``encodes'' a way to build a \MELL proof-structure of type $\Gamma$ from scratch.

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "mainFinal"
%%% End:

% !TEX root = mainFinal.tex
\section{Naturality of unwinding \texorpdfstring{\polyadic}{DiLL0} quasi-proof-structures}
\label{sec:naturality}

We show here how the actions of schedulings act on $\DiLL_0$ quasi-proof-structures, mimicking the behavior of the actions of schedulings on \MELL quasi-proof-structures seen in \Cref{sect:rules}.
\kl{Schedulings} are the same, the novelty is that $\DiLL_0$ quasi-proof-structures have no boxes and might have daimons.
The bridge between the $\MELL$ and $\DiLL_0$ frameworks is given by the \kl{filled Taylor expansion}, which actually defines a \emph{natural transformation} (\Cref{thm:projection-natural}).

For $\Gamma$ a list of lists of $\MELL$ formulas, $\intro[qDiLL0]{\PolyPN}(\Gamma)$ is the
set of $\DiLL_0$ quasi-proof-structures of type $\Gamma$ (we assume they have the \emph{same} conclusions).
For any set $X$, its powerset is

\begin{figure}[t]
% prevent right column from overflowing into right margin
\newcommand{\figureNineRightColumnWidth}{0.5\textwidth}
\vspace*{-3\baselineskip}
\centering
\begin{subfigure}[c]{0.4\textwidth}
\scalebox{0.88}{
\pnet{
\pnformulae{
\pnf[A]{$\Gamma_k$}~\pnf[B]{$i$}~\pnf[A']{$i\!+\!1$}~\pnf[B']{$\Gamma_{k}'$}
\pndaimon[dai]{A*,A',B,B'*}
\pnsemibox{dai,A,A',B,B'}
\pnet{
\pnformulae{
\pnf[A]{$\Gamma_k$}~\pnf[A']{$i\!+\!1$}~\pnf[B]{$i$}~\pnf[B']{$\Gamma_{k}'$}
\pndaimon[dai]{A*,A',B,B'*}
\pnsemibox{dai,A,A',B,B'}
\Bigg\}$
\vspace{-.5\baselineskip}
\caption{Daimoned exchange}
\label{fig:exc-daimon}
\end{subfigure}\hfill%
\begin{subfigure}[c]{\figureNineRightColumnWidth}
\scalebox{0.88}{
\pnet{
\pnformulae{
\pnf[A]{$\Gamma_k$}~\pnf[B]{$i$}~\pnf[A']{$i\!+\!1$}~\pnf[B']{$\Gamma_{k}'$}
\pndaimon[dai]{A*,A',B,B'*}
\pnsemibox{dai,A,A',B,B'}
\pnet{
\pnformulae{
\pnf[A]{$\Gamma_k$}~\pnf[B]{$i$}~~\pnf[A']{$i\!+\!1$}~\pnf[B']{$\Gamma_{k}'$}
\pndaimon[dai]{A*,B}
\pndaimon[dai']{A',B'*}
\pnsemibox{dai,A,B}
\pnsemibox{dai',A',B'}
\Bigg\}$
\vspace{-.5\baselineskip}
\caption{Daimoned mix}
\label{fig:mix-daimon}
\end{subfigure}

\begin{subfigure}[c]{0.4\textwidth}
\vspace*{-\baselineskip}
\scalebox{0.88}{
\pnet{
\pnformulae{
\pnf[i]{$i\!-\!1$}~\pnf[j]{$i$}
\pndaimon[ax]{i,j}
\pnsemibox{ax,i,j}
\pnet{
\pnformulae{
\pnf[empty]{}
\pnsemibox{empty}
\bigg\}$
\vspace{-.5\baselineskip}
\caption{Daimoned hypothesis (\(\Ax, \One, \bot, \Weak\))}
\label{fig:hypothesis-daimon}
\end{subfigure}\hfill%
\begin{subfigure}[c]{\figureNineRightColumnWidth}
\vspace*{-2\baselineskip}
\scalebox{0.88}{
\pnet{
\pnformulae{
\pnf[G]{$\Gamma_k$}
\pndaimon[dai]{G*}[1][.5]
\pnsemibox{dai,G}
\pnet{
\pnformulae{
\pnf[G]{$\Gamma_k$}
\pndaimon[dai]{G*,i,j}
\pnsemibox{dai,G,i,j}
\Bigg\}$
\vspace{-.5\baselineskip}
\caption{Daimoned cut ($\Gamma_{\!k} \neq \emptylist$)}
\label{fig:cut-daimon}
\end{subfigure}

\vspace{-\baselineskip}
\begin{subfigure}[b]{0.5\textwidth}
\scalebox{0.88}{
\pnet{
\pnformulae{
\pnf[G]{$\Gamma_k$}~\pnf[i]{$i$}
\pndaimon[dai]{G*,i}[1][.05]
\pnsemibox{dai,G,i}
\pnet{
\pnformulae{
\pnf[G]{$\Gamma_k$}~\pnf[i]{$i$}~\pnf[j]{$i\!+\!1$}
\pndaimon[dai]{G*,i,j}
\pnsemibox{dai,G,i,j}
\Bigg\}$
\vspace{-.5\baselineskip}
\caption{Daimoned multiplicative (\(\otimes, \parr\))}
\label{fig:tensor-daimon}
\end{subfigure}\hfill%
\begin{subfigure}[b]{\figureNineRightColumnWidth}
\scalebox{0.88}{
\pnet{
\pnformulae{
\pnf[G]{$\Gamma_k$}~\pnf[i]{$i$}
\pndaimon[dai]{G*,i}[1][.05]
\pnsemibox{dai,G,i}
\pnet{
\pnformulae{
\pnf[G]{$\Gamma_k$}~\pnf[i]{$i$}~\pnf[j]{$i\!+\!1$}
\pndaimon[dai]{G*,i,j}
\pnsemibox{dai,G,i,j}
\Bigg\}$
\vspace{-.5\baselineskip}
\caption{Daimoned contraction}
\label{fig:contraction-daimon}
\end{subfigure}

\vspace{-\baselineskip}
\begin{subfigure}[b]{0.4\textwidth}
\scalebox{0.88}{
\pnet{
\pnformulae{
\pnf[G]{$\Gamma_k$}~\pnf[i]{$i$}
\pndaimon[dai]{G*,i}[1][.0]
\pnsemibox{dai,G,i}
\pnet{
\pnformulae{
\pnf[G]{$\Gamma_k$}~\pnf[i]{$i$}
\pndaimon[dai]{G*,i}[1][.0]
\pnsemibox{dai,G,i}
\Bigg\}$
\vspace{-.5\baselineskip}
\caption{Daimoned dereliction}
\label{fig:dereliction-daimon}
\end{subfigure}\hfill%
\begin{subfigure}[b]{\figureNineRightColumnWidth}
\scalebox{0.88}{
\pnet{
\pnformulae{
\pnf[a1]{$\quad\; \wn \! A_1\;\overset{p\geqslant 0}{\cdots}$}~~
\pnf[ap]{$\wn \! A_p$}~
\pnf[i]{$i$}
\pndaimon[dai]{a1,ap,i}[1][.0]
\pnsemibox{dai,a1,ap,i}
\pnet{
\pnformulae{
\pnf[a1]{$\quad\; \wn \! A_1\;\overset{p\geqslant 0}{\cdots}$}~~
\pnf[ap]{$\wn \! A_p$}~
\pnf[i]{$i$}
\pndaimon[dai]{a1,ap,i}[1][.0]
\pnsemibox{dai,a1,ap,i}
\Bigg\}$
\vspace{-.5\baselineskip}
\caption{Daimoned box}
\label{fig:box-daimon}
\end{subfigure}

\begin{subfigure}[b]{0.2\textwidth}
\scalebox{0.88}{
\pnet{
\pnformulae{
\pnf[a1]{$\quad\; \wn \! A_1\;\overset{p\geqslant 0}{\cdots}$}~~
\pnf[ap]{\!$\wn \! A_p$}~
\pnf[i]{$i$}
\pnwn[?a1]{a1}
\pnwn[?ap]{ap}
\pncown[!i]{i}
\pnsemibox{a1,ap,i,?a1,?ap,!i}
\pnet{
\pnformulae{
\pnf[a1]{$\quad\; \wn \! A_1\;\overset{p\geqslant 0}{\cdots}$}~~
\pnf[ap]{\!$\wn \! A_p$}~
\pnf[i]{$i$}
\pndaimon[dai]{a1,ap,i}[1][.0]
\pnsemibox{dai,a1,ap,i}
\Bigg\}$
\vspace{-.5\baselineskip}
\caption{Empty box}
\label{fig:empty-box}
\end{subfigure}\hfill%
\begin{subfigure}[b]{\figureNineRightColumnWidth}
\scalebox{0.85}{
\pnet{
\pnformulae{
\pnf{$\dots$}}
\pnsomenet[rhom]{$\rho_m$}{2cm}{0.5cm}[at (0,1.5)]
\pnsomenet[rho1]{$\rho_1$}{1.4cm}{0.5cm}[at (0,0)]
\pnoutfrom{rho1.-26}[rho1c]{$A$}
\pnoutfrom{rhom.-18}[rhomc]{$A$}
\pnbag[!]{}{rho1c,rhomc}{$i$}[1][0.2]
\pnoutfromswitch{rho1.-82}[rho1ap]{$A_p$}
\pnoutfromswitch{rhom.-40}[rhomap]{$A_p$}
\pnoutfromswitch{rho1.-154}[rho1a1]{$A_1$}
\pnoutfromswitch{rhom.-162}[rhoma1]{$A_1$}
\pnexp[?a1]{}{rho1a1*,rhoma1*}{$\quad \wn \! A_{1} \,\overset{p \geqslant 0}{\cdots}$}[1][-0.2]
\pnexp[?ap]{}{rho1ap*,rhomap*}{$\,\wn \! A_{p}$}
\pnsemibox{rho1,rhom,!,?a1}
\pnet{
\pnformulae{
\pnf{$\dots$}}
\pnsomenet[rho1]{$\rho_j$}{2cm}{0.5cm}[at (0,0)]
\pnoutfrom{rho1.-20}[pi1c]{$i$}[2]
\pnoutfromswitch{rho1.-45}[rho1ap]{$A_p$}
\pnoutfromswitch{rho1.-160}[rho1a1]{$A_1$}
\pnexp[?a1]{}{rho1a1*}{$\quad \wn \! A_{1} \,\overset{p\geqslant 0}{\cdots}$}
\pnexp[?ap]{}{rho1ap*}{$\,\wn \! A_{p}$}
\pnsemibox{rho1,?a1,?ap}
}\right\}_{1 \leqslant j \leqslant m}$
\vspace{-.5\baselineskip}
\caption{Non-empty box ($m > 0$)}
\label{fig:polybox}
\end{subfigure}

Lists $\Gamma_{\!k}$ and $\Gamma_{\!k'}$ may be empty, except in \Cref{fig:cut-daimon} since a $\maltese$-cell has at least  an output.
\caption{\mbox{Action of elementary schedulings on $\DiLL_0$ quasi-proof-structures.}}
\label{fig:actions-daimon}
\end{figure}

\begin{defi}[action of schedulings on \texorpdfstring{\polyadic}{DiLL0}
\label{def:paths-on-polyadic}
An \kl{elementary scheduling} $a \colon \Gamma \to \Gamma'$ defines a relation
$\pnrewrite[a] \ \subseteq \kl{\PolyPN}(\Gamma) \times \PowerSet{\kl{\PolyPN}(\Gamma')}$, called the \intro[action of elementary scheduling on dill]{action} of $a$, as the smallest relation containing
all the rules in \Cref{fig:actions-all}---except \Cref{fig:box}, and with the same remarks\footnotemark---and in \Cref{fig:actions-daimon}.
\footnotetext{More precisely, if $\pnrewrite[a] \ \subseteq \kl{\PolyPN}(\Gamma) \times \PowerSet{\kl{\PolyPN}(\Gamma')}$, in the rewrite rule $\pnrewrite[a]$ in \Cref{fig:actions-all} the quasi-proof-structure on the right-hand-side must be replaced by the singleton set containing it.}
We extend it to a relation $ \pnrewrite[a] \ \subseteq \PowerSet{\PolyPN(\Gamma)} \times\PowerSet{\PolyPN(\Gamma')}$ by the multiplication of the monad powerset $X \mapsto \PowerSet{X}$.\footnotemark
\footnotetext{\label{foot:lifting}
More explicitly, given $\Pi \subseteq \PolyPN(\Gamma)$ and $\Pi' \subseteq \PolyPN(\Gamma')$, $\Pi \pnrewrite[a] \Pi'$ means that
$\Pi' = \bigcup\{\rho' \subseteq \PolyPN(\Gamma') \mid \exists \, \rho \in \Pi : \rho \pnrewrite[a] \rho'\}$.
Thus, $\rho \pnrewrite[a] \rho' \subseteq \Pi'$ for every $\rho \in \Pi$.
And, in particular, $\emptyset \pnrewrite[a] \emptyset$.
Roughly, the same rewrite rule applies to the \emph{same} conclusion of \emph{each} element of a set of $\DiLL_0$ quasi-proof-structures.
Note that $\emptyset \neq \Pi \pnrewrite[a] \Pi'$ implies $\Pi' \neq \emptyset$, since there is no elementary scheduling $a$ such that $\rho \pnrewrite[a] \emptyset$.}
The rewrite relation on
$\PowerSet{\PolyPN(\Gamma)} \times\PowerSet{\PolyPN(\Gamma')}$ is extended by composition of relations to define, for any \kl{scheduling} $\sched \colon \Gamma \to \Gamma'$, a relation $\pnrewrite[\sched] \,\subseteq \PowerSet{\PolyPN(\Gamma)} \times \PowerSet{\PolyPN(\Gamma')}$, \mbox{the
\intro[action of scheduling on dill]{action} of $\sched$.}
\end{defi}

Roughly, any rewrite rule in \Cref{fig:actions-daimon}---except
\Cref{fig:empty-box,fig:polybox}---mimics the behavior of the corresponding rule in
\Cref{fig:actions-all} using a $\maltese$-cell.
Since every elementary scheduling has at least two versions of its action, one in \Cref{fig:actions-all} and one (or two for $\BoxR_{i}$) in \Cref{fig:actions-daimon}, when $\Pi \pnrewrite[a] \Pi'$, some elements of $\Pi$ may rewrite according to one version of the action of $a$, others elements according to another version.
In any case, all the elements of $\Pi'$ have the same conclusions, as the elements of $\Pi$ do.
Types are updated according to \Cref{fig:elementary-schedulings}.

The \kl[action of elementary scheduling on dill]{action} in \Cref{fig:empty-box} acts on a component made of one \emph{co-weakening} (a $\oc$-cell without inputs) and some \emph{weakenings} ($\wn$-cells without inputs), it erases them and creates a $\maltese$-cell, whose outputs are all the conclusions of the component.
If we just erased the co-weakening with output of type $\oc A$, we would lose the information about the type $A$;
this is one of the reasons why a $\maltese$-cell is needed.
Intuitively, a co-weakening represents a box taken $0$ times, so there is no information about the content of the box, apart from its type.
The \kl{daimon} is a ``universal'' $\DiLL_0$ proof-structure representing this information plainly~missing.

The \kl[action of elementary scheduling on dill]{action} in \Cref{fig:polybox} separates the copies of a candidate for a box. It
requires that,
in the \kl[undirected graph]{graph} of the component on the left of $\pnrewrite[\!\BoxR_i]$, $\rho_{j}$ is not connected to $\rho_{j'}$ for $j \neq j'$, except for the $\oc$-cell and the $\wn$-cells in the
conclusions.  Read in reverse, the rule associates with a non-empty finite set
of $\DiLL_0$ quasi-proof-structures $\{\rho_1, \dots, \rho_m\}$ the merging of
$\rho_1, \dots, \rho_m$, that is the $\DiLL_0$ quasi-proof-structure depicted on
the left of $\pnrewrite[\!\BoxR_i]$.