Intuitively, $\rho_1, \dots, \rho_m$ represent $m\!>\!0$ possible copies of a box,
whose ``compatibility'' must be analyzed ``in parallel'': this is why the \kl[action of elementary scheduling on dill]{action} rewrites a single $\DiLL_0$ quasi-proof-structure to a (finite) \emph{set} of them.

Note that a $\maltese$-cell can be created only by the rewrite rule in \Cref{fig:empty-box}, and erased only by the \kl[action of elementary scheduling on dill]{action of elementary scheduling} called hypothesis in \Cref{fig:hypothesis-daimon}: $\Ax_{i}, \One_i, \bot_i, \Weak_i$\,.

\begin{example}
\label{ex:box}
Consider the $\DiLL_0$ proof-structures below ($X$ is a propositional variable).
We have that $\{\rho_0,\rho_1,\rho_2\} \pnrewrite[\BoxR_{2}] \{\rho_0',\rho_1',\rho_2'\}$ because $\rho_0 \pnrewrite[\BoxR_{2}] \{\rho_0'\}$ (according to \Cref{fig:empty-box}), $\rho_1 \pnrewrite[\BoxR_{2}] \{\rho_1'\}$ (according to \Cref{fig:polybox}) and $\rho_2 \pnrewrite[\BoxR_{2}] \{\rho_1',\rho_2'\}$ (according to \Cref{fig:polybox}).
\begin{center}
%		$\rho_0$
%		\qquad\qquad\quad
%		$\rho_1$
%		\qquad\qquad\quad
%		$\rho_2$
%		\qquad\qquad\qquad\quad
%		$\rho_0'$
%		\qquad\qquad
%		$\rho_1'$
%		\qquad\qquad
%		$\rho_2'$
%		\qquad\qquad

\vspace*{-2.5\baselineskip}
$\rho_0 =\!\! $
\scalebox{0.8}{
\pnet{
\pnformulae{\\
\pnf[x]{$\wn X$}~\pnf[bbx']{$\oc\oc X^{\!\perp}$}
\pnwn{x}
\pncown{bbx'}
\quad
$\rho_1 =\!\! $
\scalebox{0.8}{
\pnet{
\pnformulae{
\\
\pnf[x]{$\wn X$}~\pnf[bx']{$\oc X^{\!\perp}$}
\pnwn{x}
\pncown{bx'}
\pnbag{}{bx'}{$\oc\oc X^{\!\perp}$}
\quad
$\rho_2 =\!\! $
\scalebox{0.8}{
\pnet{
\pnformulae{\pnf[x]{$X$}~\pnf[x']{$X^{\!\perp}$}
\\
~~\pnf[bx'']{$\oc X^{\!\perp}$}
\pnaxiom{x,x'}
\pnexp{}{x}{$\wn X$}
\pnbag{}{x'}[bx']{$\oc X^{\!\perp}$}
\pncown{bx''}
\pnbag{}{bx',bx''}{$\oc\oc X^{\!\perp}$}
\quad
$\rho_0' =\!\! $
\scalebox{0.8}{
\pnet{
\pnformulae{\\
\pnf[x]{$\wn X$}~\pnf[bx']{$\oc X^{\!\perp}$}
\pndaimon{x,bx'}
\quad
$\rho_1' =\!\! $
\scalebox{0.8}{
\pnet{
\pnformulae{\\
\pnf[x]{$\wn X$}~\pnf[bx']{$\oc X^{\!\perp}$}
\pnwn{x}
\pncown{bx'}
\quad
$\rho_2' =\!\! $
\scalebox{0.8}{
\pnet{
\pnformulae{\pnf[x]{$X$}~\pnf[x']{$X^{\!\perp}$}
\pnaxiom{x,x'}
\pnexp{}{x}{$\wn X$}
\pnbag{}{x'}[bx']{$\oc X^{\!\perp}$}
\end{center}
\end{example}

\begin{example}
\label{ex:church}
Consider the $\DiLL_0$ proof-structures $\pi$ and $\pi'$ below.
\begin{center}
\vspace{\beforepn}
$\pi = $
\scalebox{0.8}{
\pnet{
\pnformulae{~~\pnf[ba]{$\oc X$}~\pnf[na]{$X^{\bot}$}\\\\\\
\\
\pnf[na']{$\wn X^{\!\bot}$}~~~~~\pnf[a]{$X$}
\pnwn{na'}
\pncown{ba}
\pnaxiom{na,a}
\pntensor{ba,na}[bana]{$\oc X \otimes X^{\bot}$}
\pnexp{}{bana}{$\wn (\oc X \otimes X^{\bot})$}[1.1]
\qquad\qquad\qquad
$\pi' = $
\scalebox{0.8}{
\pnet{
\pnformulae{~~~~~~\pnf[ba]{$\oc X$}~\pnf[na]{$X^{\bot}$}\\\\\\
\\
\pnf[na']{$\wn X^{\!\bot}\,$}~~~\pnf[wntens]{$\wn (\oc X \!\otimes\! X^{\!\bot})$}~~~~~~\pnf[a]{$X$}
\pnwn{na'}
\pnwn{wntens}
\pncown{ba}
\pnaxiom{na,a}
\pntensor{ba,na}[bana]{$\oc X \otimes X^{\bot}$}
\pnexp{}{bana}{$\wn (\oc X \!\otimes\! X^{\!\bot})$}[1.1]
\end{center}

For every $n > 0$, the singleton $\{\pi\}$ rewrites to \(\{(n\!+\!1)\emptynet\}\) by the \kl[action of scheduling]{action} of the scheduling $\nu_n^1$ where, for all $k > 0$, $\nu_n^k \colon (\wn X^\bot, \wn (\oc X \otimes X^\bot), X; \underbrace{\emptylist; \cdots; \emptylist}_{k\!-\!1 \text{ times}}) \to (k\!+\!n)\emptylist$ is defined by:
\begin{align*}
\nu_1^k &= \Der_2 \, \otimes_2 \, \Mix_{2} \, \Ax_{4} \, \BoxR_2 \, \Der_1 \, \Ax_{2}
\nu_{n+1}^k &= \Contr_2 \, \Der_3 \, \otimes_3 \, \Mix_{3} \, \Ax_{5} \, \BoxR_3 \, \nu_{n}^{k+1} \,.
\end{align*}

\vspace{\beforepn}
Indeed, we have the following rewritings, where
$\pi_\maltese = \scalebox{0.75}{
\pnet{
\pnformulae{
\pnf[na']{$\wn X^{\!\bot}$}~~\pnf[wntens]{$\,\,\wn (\oc X \!\otimes\! X^{\!\bot}\!)$}~~\pnf[ba]{$ X\!\!$}
\pndaimon[d]{na',wntens,ba}

\vspace{-2.5\baselineskip}
\begin{align*}
\{\pi_\maltese\}
\pnrewrite[\!\Der_2] \, \pnrewrite[\!\otimes_2] \, \pnrewrite[\!\Mix_{2}] \, \pnrewrite[\!\Ax_{4}] \,
\pnrewrite[\!\BoxR_{2}] \,
\pnrewrite[\!\Der_1] \, \pnrewrite[\!\Ax_{2}]
\{2\emptynet\}
\quad\quad
\{\pi_\maltese\}
\pnrewrite[\!\Contr_2] \,
\pnrewrite[\!\Der_3] \, \pnrewrite[\!\otimes_3] \, \pnrewrite[\!\Mix_{3}] \, \pnrewrite[\!\Ax_{5}] \,
\pnrewrite[\!\BoxR_3]
\Big\{\!\!
\scalebox{0.75}{
\pnet{
\pnformulae{
\pnf[na']{$\wn X^{\!\bot}$}~~\pnf[wntens]{$\,\,\wn (\oc X \!\otimes\! X^{\!\bot}\!)$}~~\pnf[ba]{$ X\!\!$}~~\pnfsmall[empty]{}
\pndaimon[d]{na',wntens,ba}
\pnsemibox{empty}
\pnsemibox{d,na',wntens,ba}
\Big\}
\end{align*}
\noindent and therefore, for every $n > 1$, the scheduling $\nu_n^1$ acts on $\{\pi\}$ in the way below

\vspace{-2.5\baselineskip}
\begin{align*}
\{\pi\}
\pnrewrite[\!\Contr_2]
\{\pi'\}
\pnrewrite[\!\Der_3] \, \pnrewrite[\!\otimes_3] \, \pnrewrite[\!\Mix_{3}] \, \pnrewrite[\!\Ax_{5}]
\Big\{\!\!
\scalebox{0.75}{
\vspace*{\beforepn}
\pnet{
\pnformulae{
\pnf[na']{$\wn X^{\!\bot}$}~~\pnf[wntens]{$\,\,\wn (\oc X \!\otimes\! X^{\!\bot}\!)$}~~\pnf[ba]{$\oc X\!\!\!$}~~\pnfsmall[empty]{}
\pnwn{na'}
\pnwn{wntens}
\pncown{ba}
\pnsemibox{empty}
\pnsemibox{d,na',wntens,ba}
\Big\}
\pnrewrite[\!\BoxR_3]
\Big\{\!\!
\scalebox{0.75}{
\pnet{
\pnformulae{
\pnf[na']{$\wn X^{\!\bot}$}~~\pnf[wntens]{$\,\,\wn (\oc X \!\otimes\! X^{\!\bot}\!)$}~~\pnf[ba]{$ X\!\!$}~~\pnfsmall[empty]{}
\pndaimon[d]{na',wntens,ba}
\pnsemibox{empty}
\pnsemibox{d,na',wntens,ba}
\Big\}
\pnrewrite[\!\nu_{\!n\!-\!1}^2\!]
\{(n\!+\!1)\emptynet\}.
\end{align*}
\end{example}

\begin{figure}[!t]
\vspace{\beforepn}
\centering
$\Pi = \Bigg\{\!\!\!\!\!$
\scalebox{0.75}{
\!\pnet{
\pnformulae{
\pnf[botax]{$X^\bot$}~\pnf[Xp]{$X^\bot$}~\pnf[1ax]{$X$}~\pnf[X]{$X$}
\pnaxiom[ax]{botax,1ax}[1][-0.3]
\pnaxiom[axprop]{Xp,X}[1][0.3]
\pnbag{}{1ax,X}[!1ax]{$\oc X$}
\pnexp{}{Xp,botax}[?bot]{$\wn X^\bot$}
\quad
$\Pi' = \Bigg\{\!\!\!\!\!$
\scalebox{0.75}{
\pnet{
\pnformulae{
\pnf[botax]{$X^\bot$}~\pnf[Xp]{$X^\bot$}~\pnf[1ax]{$X$}~\pnf[X]{$X$}
\pnaxiom[ax]{botax,1ax}[1][-0.3]
\pnaxiom[axprop]{Xp,X}[1][0.3]
\pnbag{}{1ax,X}[!1ax]{$\oc X$}
\quad \ \
\pnrewrite[\Contr_1]\,\pnrewrite[\Der_1]\,\pnrewrite[\Der_2]
\Pi'$
\quad
\pnrewrite[\BoxR_2]$
\scalebox{0.75}{
\!\pnet{
\pnformulae{
\pnf[botax]{$X^\bot$}~\pnf[1ax]{$X$}
\pnaxiom[ax]{botax,1ax}[1]
\pnexp{}{botax}[?bot]{$\wn X^{\!\bot}$}
\pnrewrite[\Der_{1}] \, \pnrewrite[\Ax_{2}]
\{\emptynet\}
\caption{Examples of actions of schedulings for $\DiLL_0$.}
\label{fig:rewrite-diff}
\end{figure}

The rewriting on $\DiLL_0$ quasi-proof-structures behaves differently than on $\MELL$ quasi-proof-structures.
In $\DiLL_0$,	Lemma \ref{lem:cell-or-mix} and Proposition \ref{prop:unwinding-to-empty} are false.
Indeed, in \Cref{fig:rewrite-diff} no elementary scheduling applies to the singleton $\Pi'$ of a non-empty $\DiLL_0$ proof-structure.
So, $\Pi \pnrewrite[\Contr_1] \, \pnrewrite[\Der_1] \, \pnrewrite[\Der_2] \Pi'$ and gets stuck, but
the action of another scheduling rewrites $\Pi$ to $\{\emptynet\}$
(\Cref{fig:rewrite-diff} on the right).
Thus, some rewritings from $\Pi$ end in $\{\emptynets\}$, others get stuck before.

\begin{defi}[functor \texorpdfstring{$\PPolyPN$}{PPolyPN}]
\label{def:FunctorPPoly}
We define a functor $\PPolyPN \colon \Scheduling \to \Rel$ by:
\begin{itemize}
\item\emph{on objects:} for every list $\Gamma$ of lists of \MELL formulas,
$\PPolyPN(\Gamma) = \PowerSet{\PolyPN(\Gamma)}$, the powerset of the set $\PolyPN(\Gamma)$ of
$\DiLL_0$ quasi-proof-structures of type $\Gamma$;
\item\emph{on arrows:} for any $\sched \colon \Gamma \to \Gamma'$,
$\PPolyPN(\sched)$ is $\pnrewrite[\sched] \colon \PPolyPN(\Gamma) \to \PPolyPN(\Gamma')$ (Def.~\ref{def:paths-on-polyadic}).
\end{itemize}
\end{defi}

We can now compare the functors $\MELLFunctor$ and $\PPolyPN$ from $\Scheduling$ to $\Rel$.

\begin{thm}[naturality]
\label{thm:projection-natural}
The filled Taylor expansion defines a natural transformation
\begin{align*}
\NatTransf \colon \PPolyPN \Rightarrow \MELLFunctor \colon \Scheduling \to
\Rel
\end{align*}
by: for $\Gamma$ a list of lists of \MELL
formulas, $(\Pi, R) \in \NatTransf_{\Gamma}$ iff $\Pi \subseteq \FatTaylor{R}$ and the type of $R$~is~$\Gamma$.
\end{thm}
In other words, diagram \eqref{eq:naturality} below commutes for every scheduling
$\sched \colon \Gamma \to \Gamma'$.

\noindent
\!\!\!\!
\begin{minipage}{0.5\textwidth}
\begin{align}
\label{eq:naturality}
\!\!\!\!\!
\begin{tikzcd}
\!\!\!\!\PPolyPN(\Gamma) \ar[rr,"\PPolyPN(\sched)"]
\ar[d,swap,"\NatTransf_{\Gamma}"] \& \&
\PPolyPN(\Gamma')\!\!\!\!\!\!\!\!\! \ar[d,"\NatTransf_{\Gamma'}"]
\\
\!\!\!\!\MELLFunctor(\Gamma) \ar[rr,"\MELLFunctor(\sched)"]\& \& \MELLFunctor(\Gamma')\!\!\!\!\!\!\!\!\!\!
\end{tikzcd}
\end{align}
\end{minipage}
\quad
\begin{minipage}{0.23\textwidth}
\small
\begin{align}
\label{eq:naturality-square}
\begin{tikzcd}
\Pi \ar[r,squiggly,"\sched"]
\ar[d,swap,gray,"\NatTransf_{\Gamma}"] \&
\Pi'\!\!\! \ar[d,swap,"\NatTransf_{\Gamma'}"]
\\
\textcolor{gray}{R} \ar[r,squiggly,"\sched",gray]\& R'\!\!\!
\end{tikzcd}
\end{align}
\end{minipage}
\quad
\begin{minipage}{0.23\textwidth}
\small
\begin{align}
\label{eq:naturality-square-bis}
\begin{tikzcd}
\Pi \ar[r,squiggly,gray,"\sched"]
\ar[d,swap,"\NatTransf_{\Gamma}"] \&
\textcolor{gray}{\Pi'}\!\!\! \ar[d,gray,swap,"\NatTransf_{\Gamma'}"]
\\
R \ar[r,squiggly,"\sched"]\& R'\!\!\!
\end{tikzcd}
\end{align}
\end{minipage}

\noindent
That is, given $\Pi \pnrewrite[\sched] \Pi'$ with
$\Pi'\subseteq \FatTaylor{R'}$, we can \emph{simulate backward} the rewriting to $R$
(here the co-functionality of actions on $\MELLFunctor$ expressed by
Lemma \ref{prop:unwinding-co-functional} comes in handy) so that $R \pnrewrite[\sched] R'$
and $\Pi\subseteq \FatTaylor{R}$ (square \eqref{eq:naturality-square});
and conversely, given $R \pnrewrite[\sched] R'$,
we can \emph{simulate forward} the rewriting for any $\Pi \subseteq \FatTaylor{R}$, so that
$\Pi \pnrewrite[\sched] \Pi'$ for some $\Pi'\subseteq \FatTaylor{R'}$ (square \eqref{eq:naturality-square-bis}).
In both squares, the \emph{same} kind of action is performed on $\DiLL_0$ and on \MELL.

\begin{proof}
$\NatTransf$ is a family of arrows of $\Rel$ indexed by the objects in $\Scheduling$.
We have to show
that squares \eqref{eq:naturality-square}--\eqref{eq:naturality-square-bis} commute for any \kl{scheduling}
$\sched \colon \Gamma\to \Gamma'$, and actually, it is enough to show
commutation for \kl{elementary schedulings}.
Let $a \colon \Gamma\to \Gamma'$ be an elementary scheduling.

\begin{enumerate}
\item \emph{Square \eqref{eq:naturality-square-bis}:} Let us prove that
$\MELLFunctor(a) \circ \NatTransf_{\Gamma} \subseteq \NatTransf_{\Gamma'} \circ
\PPolyPN(a)$.

Let $(\Pi,R') \in \MELLFunctor(a) \circ \NatTransf_{\Gamma}$. Let
$R = (\lvert R \rvert, \ForestT, \BoxFunction)\in \MELLFunctor(\Gamma)$ be a witness of composition, that is, an element such
that $(\Pi,R) \in \NatTransf_{\Gamma}$ and $R\pnrewrite[a] R'$.
If $\Pi = \emptyset$ then we are done because $\Pi \pnrewrite[a] \emptyset$ (see \Cref{foot:lifting}) and $\emptyset \subseteq \FatTaylor{R'}$.
So, we suppose that $\Pi \neq \emptyset$.

Let $(t,h)$ be a \kl{thick subforest} of $\ForestT$, let
$r_{1},\ldots,r_{n}$ be some roots in $\ForestT$ (and in $t$, by Remark \ref{rmk:roots}), and let $\rho_{r_{1}\ldots r_{n}} \in \Pi$ be the element of the \kl{filled Taylor
expansion} $\FatTaylor{R}$ of $R$ associated with $(t,h)$ and $r_{1},\ldots,r_{n}$ (\ie~$\rho_{r_{1}\ldots r_{n}}$ is the \kl{emptying on} $r_{1},\ldots,r_{n}$ of the element of $\Taylor{R}$ obtained via the thick subforest $(t,h)$ of $\ForestT$, see Definition \ref{def:FilledTaylor}).
By Remark \ref{rmk:conclusions-emptying}, we can identify the conclusions of $R$ and of $\rho_{r_{1}\ldots r_{n}}$.
The case $a = \Ex_{i}$ is trivial since it just swaps the order of two consecutive conclusions.
Other cases for $a$:
\begin{itemize}
\item If $a = \Mix_{i}$,
let $r$ be the root in $\ForestT$ corresponding to the conclusion $i$ (\ie $\BoxFunction_{F}(i)$ is the output of $r$) and let $p,\ldots, p+k$ be the conclusions of the component $S$ of $R$ containing $i$.
In the \kl{undirected graph} $\lVert S \rVert$, none of the conclusions $p, \dots, i$ is  \kl{connected} to any conclusion $i+1, \dots, p+k$.
By Definitions~\ref{def:taylor} and~\ref{def:FilledTaylor},
as $\rho_{r_{1}\ldots r_{n}} \in \Pi \subseteq \FatTaylor{R}$,
$r$ is a root in the box-forest of $\rho_{r_{1}\ldots r_{n}}$, and $p,\ldots, p+k$ are  the conclusions of $\rho_{r_{1}\ldots r_{n}}$ corresponding to $r$.
There are two cases, according to Remark~\ref{rmk:connection}:
\begin{itemize}
\item the \kl{connected components} of $i$ and $i\!+\!1$ are disjoint in the undirected graph
$\lVert \rho_{r_{1}\ldots r_{n}} \rVert$;
\item $i$ and $i\!+\!1$ belong to the same connected component of  $\lVert \rho_{r_1 \dots r_n} \rVert$,
and their component in $\rho_{r_{1}\ldots r_{n}}$ is a daimon with conclusions $p, \dots,  i, i\!+\!1, \dots, p\!+\!k$.
\end{itemize}
In both cases the rule $\Mix_{i}$ is also applicable to
$\rho_{r_{1}\ldots r_{n}}$, yielding a $\DiLL_0$ quasi-proof-structure
The box-forest $\ForestT'$ of $R'$ is obtained from the box-forest $\ForestT$ of $R$ by root-splitting\footnotemark the tree with root $r$ in two trees with roots $r_1'$, $r_2'$.
Let $t'$ be a forest obtained from $t$ in a similar way.
\footnotetext{\label{note:split-tree}It means that $\ForestT = \ForestT'$ except that in $\ForestT'$ the root $r$ with its output is replaced by the roots $r_1'$ and $r_2'$ with their output, and that the inputs of $r$ are split into the inputs of $r_1'$ and the inputs of $r_2'$.}
Let $h' \colon t'\to \ForestT'$ be the directed graph morphism such that $h_V'(r_1') = r_1'$, $h_V'(r_2') = r_2'$ and $h_V'(v) = h_V(v)$ for all
$v \in V_{\ForestT} \cap V_{\ForestT'}$.
We verify that $\rho'$ is the element of
$\FatTaylor{R'}$ associated with the thick subforest $(t',h')$ of $\ForestT'$.

\item If $a \in \{\otimes_i, \parr_i, \Der_i,\Contr_i, \Weak_i, \One_i, \bot_i, \Ax_{i}\}$, let $k$ be such that the rule $a$ acts on the conclusions $i-k,\dots,i$ of a component of $R$, and let
$\ell$ be the type of the cell in $R$ whose output is the conclusion
$i$ (or whose outputs are the conclusions $i-1$ and $i$, if $\ell = \Ax$).
In $\rho_{r_{1}\ldots r_{n}}$
either there is a $\ell$-cell with $\ell \neq \Ax$ whose output is the conclusion $i$, or there is a $\Ax$-cell whose outputs are the conclusions $i-1$ and $i$, or the component containing the conclusion $i$ is a daimon with conclusions $i-k, \dots, i$.
Clearly $a$ is applicable to $\rho_{r_{1}\ldots r_{n}}$, which yields a $\DiLL_0$
quasi-proof-structure $\rho'$.

The box-forest $\ForestT'$ of $R'$ is $\ForestT$, the one of $R$.
We verify that $\rho'$ is the element of the filled Taylor expansion $\FatTaylor{R'}$ of $R'$ associated with the thick subforest $(t,h)$ of $\ForestT'$.

\item If $a = \Cut^i$, let $c$ be the $\Cut$-cell of \kl{depth} $0$ in $R$ to which $a$
is applied. As in the case above, the $\Cut$-cell $c$ has either one image in
$\rho_{r_{1}\ldots r_{n}}$ or is represented by a $\maltese$-cell (with at least one conclusion). In both
cases, $\Cut^i$ is applicable to $\rho_{r_{1}\ldots r_{n}}$, yielding

The box-forest $\ForestT'$ of $R'$ is $\ForestT$, the one of $R$.
We verify that $\rho'$ is the element of the filled Taylor expansion $\FatTaylor{R'}$ of $R'$ associated with the thick subforest $(t,h)$ of $\ForestT'$.

\item If $a = \BoxR_{i}$, consider the component of $R$ whose conclusions are $i\!-\!k,\dots,i$ with $k \geqslant 0$.
In the component $\pi$ of $\rho_{r_1 \dots r_n}$ with conclusions $i\!-\!k, \dots, i$, there are three cases:
\begin{enumerate}[ref=\alph*]
\item\label{p:box-daimoned} $\pi$ is a daimon whose conclusions are $i\!-\!k,\dots,i$;
so, the rule in \Cref{fig:box-daimon} applies;
\item\label{p:box-empty} $\pi$ consists of a $\oc$-cell with output tail $i$ and no inputs; and of $k$ $\wn$-cells without inputs;
therefore, the rewrite rule in \Cref{fig:empty-box} applies;
\item\label{p:box-nonempty} $\pi$ has a $\oc$-cell $c$ with output tail $i$ and at least an input, $k$ $\wn$-cells $c_1, \dots, c_k$ immediately above each of the other $k$ conclusions, and other cells that can be split in $m$ pairwise disjoint sub-graphs of $\lVert \pi' \rVert$, where $m \geqslant 1$ and $\pi'$ is $\pi$ without $c, c_1, \dots, c_k$ and their output;
therefore, the rewrite rule in \Cref{fig:polybox} applies.
\end{enumerate}
In any case, $\BoxR_i$ applies to $\rho_{r_1 \dots r_n}$, yielding a family
$\rho'_1,\dots,\rho'_{m}$ of $\DiLL_0$ proof-structures, where $m = 1$ in cases \eqref{p:box-daimoned} and \eqref{p:box-empty}, while $m \geqslant 1$ in case \eqref{p:box-nonempty}.

The box-forest $\ForestT'$ of $R'$ is obtained from the box-forest
$\ForestT$ of $R$ by erasing the root $b$ corresponding to the conclusions $i\!-\!k,\dots,i$ (\ie, $\BoxFunction_{F}(i\!-\!k) = \dots = \BoxFunction_{F}(i)$ is the output of $b$):
the new root $b'$ of this tree of $\ForestT'$ is the unique vertex immediately above $b$ in $\ForestT$.
We have $h^{-1}(b')=\{b'_{1},\ldots,b'_{m}\}$, and $m$ trees
$t'_{1},\ldots,t'_{m}$, where $b'_{j}$ is the root of
$t'_{j}$. The directed graph morphisms $h'_{j} \colon t'_{j}\to \ForestT'$ are defined
We verify that $\rho'_j$ is the element of $\FatTaylor{R'}$ associated~with the thick subforest $(t'_j,h'_{j})$ of $\ForestT'$.
\end{itemize}

\item \emph{Square \eqref{eq:naturality-square}:} Let us prove that
$\NatTransf_{\Gamma'} \circ \PPolyPN(a) \subseteq \MELLFunctor(a) \circ
\NatTransf_{\Gamma}$.

Let $(\Pi,R') \in \NatTransf_{\Gamma'} \circ \PPolyPN(a)$ with $R' = (|R'|, \ForestT', \BoxFunction')$. Let $\Pi'$ be a
witness of composition, \ie a set in $\PPolyPN(\Gamma')$ such that
$\Pi \pnrewrite[a] \Pi'$ and $(\Pi',R') \in \NatTransf_{\Gamma'}$.

We want to exhibit a $\MELL$ quasi-proof-structure $R$ such that
$R \pnrewrite[a] R'$ and $\Pi$ is a part of the filled Taylor expansion $\FatTaylor{R}$ of
$R$. By co-functionality of $\MELLFunctor(a)$
(Lemma \ref{prop:unwinding-co-functional}), we have a candidate for such an $R$:
the preimage of $R'$ by this co-functional relation $\pnrewrite[a]$.
In other terms, if $a \colon \Gamma \to \Gamma'$ and
$R'\in\MELLFunctor(\Gamma')$, then there exists a unique $R = (|R|, \ForestT, \BoxFunction) \in\MELLFunctor(\Gamma)$ such that
$R\pnrewrite[a] R'$ (Lemma \ref{prop:unwinding-co-functional}).
We only have to check that $\Pi\subseteq \FatTaylor{R}$.
If $\Pi = \emptyset$ then trivially $\Pi \subseteq \FatTaylor{R}$.
So, we suppose that $\Pi \neq \emptyset$.

Let $\rho \in \Pi$ and $\{\rho'_1, \dots, \rho'_m\} \subseteq \Pi'$ such that $\rho \pnrewrite[a] \{\rho'_1, \dots, \rho'_m\}$.
In all cases except $a = \BoxR_i$, we have $m = 1$ \ie $\{\rho'_1, \dots, \rho'_m\} = \{\rho'_1\}$.
For $a \neq \BoxR_i$, let $(t',h')$ be a \kl{thick subforest} of $\ForestT'$, let $r'_{1},\ldots,r'_{k}$ be some \kl{roots} in $\ForestT'$ (and in $t'$, by Remark \ref{rmk:roots}), and let
$\rho'_1 = \rho'_{r'_{1}\ldots r'_{k}} \in \Pi'$ be the element of the \kl{filled Taylor expansion} $\FatTaylor{R'}$ of $R'$ associated with $(t',h')$ and $r'_{1},\ldots,r'_{k}$ (\ie $\rho'_{r'_{1}\ldots r'_{k}}$ is the \kl{emptying on} $r'_{1},\ldots,r'_{k}$ of the element of $\Taylor{R'}$ obtained via the thick subforest $(t',h')$ of $\ForestT'$, see Definition \ref{def:FilledTaylor}).
By Remark \ref{rmk:conclusions-emptying}, we can identify the conclusions of $R'$ and of $\rho'_{r'_{1}\ldots r'_{k}}$.
The case $a = \Ex_{i}$ is trivial since it just swaps the order of two consecutive conclusions.
Other cases for $a$:
\begin{itemize}
\item If $a \in \{\Cut^i, \otimes_i, \parr_i, \Der_i, \Contr_i, \Weak_i, \One_i, \bot_i, \Ax_{i} \}$ then $\ForestT = \ForestT'$; let $t = t'\!$, $h = h'\!$.
We verify that $\rho$ is the element of $\FatTaylor{R}$ associated with $r'_{1},\ldots,r'_{k}$ and the thick subforest~$(t,h)$~of~$\ForestT\!$.

\item If $a = \Mix_{i}$, let $s'_1, s'_2$ be the roots in $\ForestT'$ (and in $t'$, by Remark~\ref{rmk:roots}) corresponding to the conclusions $i, i\!+\!1$ in $R'$, respectively (\ie $\BoxFunction_{F}'(i)$ is the output of $s_1'$, $\BoxFunction_{F}'(i\!+\!1)$ is the output of $s_2'$).
Let $s$ be the root of $\ForestT$ corresponding to $i, i\!+\!1$ (\ie $\BoxFunction_{F}(i) = \BoxFunction_{F}(i\!+\!1)$ is the output of $s$).
We define the thick subforest $(t,h)$ of~$\ForestT$: $t$ is the forest obtained from $t'$ by merging its roots $s'_1$ and $s'_2$ into the root $s$, and $h \colon t \to \ForestT$ is such that $h_V(s) = s$ and $h_V(v) = h'_V(v)$ for all $v \in V_t \cap V_{t'}$.
We verify that $\rho$ is the element of $\FatTaylor{R}$ associated with $r'_{1},\ldots,r'_{k}$ and the thick subforest $(t,h)$~of~$\ForestT\!$.

\item If $a = \BoxR_{i}$, we describe the rule for non-empty box
the easier rules for daimoned and empty boxes (\Cref{fig:box-daimon,fig:empty-box}) are left to the reader.
Let $(t'_1, h'_{1}), \dots, \allowbreak (t'_m, h'_{m})$
be \kl{thick subforests} of $\ForestT'$, let $r'_{1},\ldots,r'_{k}$ be some \kl{roots} in $\ForestT'$ (and in $t'_1, \dots, t'_m$, by Remark \ref{rmk:roots}).
For all $1 \leqslant j \leqslant m$, let
$\rho'_j$ be the element of $\FatTaylor{R'}$ associated with $(t'_j, h'_{j})$ and $r'_{1},\ldots,r'_{k}$ (\ie $\rho'_j$ is the \kl{emptying on} $r'_{1},\ldots,r'_{k}$ of the element of $\Taylor{R'}$ obtained via the thick subforest $(t'_j,h'_j)$ of $\ForestT'$, see Definition \ref{def:FilledTaylor}).
The forests $t_j'$'s differ from each other only in the rooted tree corresponding to the conclusion $i$ of the $\rho_{j}'$'s.
Let $t$ be the forest made of all the rooted trees on which the forests $t_1', \dots, t'_m$ do not differ, and of the union of the rooted trees on which the forests differ, joined by a new root;
define $h$ from $h'_1, \dots, h'_m$ accordingly.
We verify that $\rho$ is the element of $\FatTaylor{R}$ associated with $r'_{1},\ldots,r'_{k}$ and the thick subforest $(t,h)$ of $\ForestT$.
\qedhere
\end{itemize}

\end{enumerate}
\end{proof}

The rewriting system, the \kl{filled Taylor expansion} (which generalizes the usual Taylor expansion) and the notion of \kl{quasi-proof-structure} (which generalizes usual proof-structures) are designed to obtain the naturality result (Theorem~\ref{thm:projection-natural}), as shown in the example below.

\begin{example}[the need for quasi]
Extending proof-structures to \kl{quasi-proof-structures}, with dashed boxes at the root level to separate their \kl{components}, is crucial to achieve naturality (Theorem~\ref{thm:projection-natural}) when dealing with a box in a \MELL \kl{proof-structure} \(R\) copied zero times in an element of its Taylor expansion. Take for instance $\rho_1$, $\rho_2$ and $R$ below.

\begin{center}
\quad\qquad\quad
\quad\qquad\quad
\quad\qquad\quad
\quad\qquad\qquad\quad
\quad\qquad\qquad
\qquad

\vspace{-2\baselineskip}
\scalebox{0.8}{
\pnet{
\pnformulae{
\pnf[out]{$\mathbf{1}$}
\pnone{in}
\pnone{out}
\pnbag{}{in}{$\oc \mathbf{1}$}
\qquad
\scalebox{0.8}{
\pnet{
\pnformulae{
\pnf[out]{$\mathbf{1}$}~\pnf[in]{$\oc \mathbf{1}$}
\pnone{out}
\pncown{in}
\qquad
\scalebox{0.8}{
\pnet{
\pnformulae{
\pnf[out]{$\mathbf{1}$}
\pnone[in1]{in}
\pnone{out}
\pnbag{}{in}{$\oc \mathbf{1}$}[1.1]
\pnbox{in1,in}
\qquad
\scalebox{0.8}{
\pnet{
\pnformulae{
\pnf[out]{$\mathbf{1}$}~\pnf[in]{$\mathbf{1}$}
\pnone[in1]{in}
\pnone{out}
\quad\qquad
\scalebox{0.8}{
\pnet{
\pnformulae{
~~\pnf[in]{$\mathbf{1}$} \\[0.3cm]
\pnf[out]{$\mathbf{1}$}
\pnone[in1]{in}
\pnone[out1]{out}
\pnbag{}{in}[b]{$\oc \mathbf{1}$}[1.1]
\pnbox{in1,in}
\pnsemibox{in,in1,b}
\pnsemibox{out,out1}
\qquad
\scalebox{0.8}{
\pnet{
\pnformulae{
\pnf[out]{$\mathbf{1}$}~~\pnf[in]{$\mathbf{1}$}
\pnone[in1]{in}
\pnone[out1]{out}
\pnsemibox{in,in1}
\pnsemibox{out,out1}
\end{center}
We have $\{\rho_1,\rho_2\} \subseteq \Taylor{R}$.
If the action of a scheduling $a$ were a binary relation $\pnrewrite[a]$ on \MELL proof-structures and not on \MELL quasi-proof-structure---ignoring the dashed boxes at the root level in \Cref{fig:actions-all} to separate their \kl{components}---we would have $R \pnrewrite[\BoxR_{2}] R'$.
To make square \eqref{eq:naturality-square-bis} commute (as required by naturality), we observe the following facts:
\begin{enumerate}
\item the action of $\BoxR_{2}$ on $\rho_2$ cannot simply erase the $\oc$-cell, otherwise we would lose the match with the type of $R'$;
so, the action of $\BoxR_{2}$ on $\rho_2$ must create a $\maltese$-cell of type $\One$;
\item thus, when $\{\rho_1,\rho_2\} \pnrewrite[\BoxR_{2}] \Pi'$, the relation between $\Pi'$ and $R'$ is not $\Pi' \subseteq \Taylor{R'}$, because of the $\maltese$-cell;
this is why we introduced the filled Taylor expansion, so that $\Pi' \subseteq \FatTaylor{R'}$;
\item the two $\One$-cells in $R'$ must be handled in two different ways;
indeed, the second one comes from the content of the box in $R$, and can be erased by the Taylor expansion of $R$ by taking 0 copies of the box (as done in $\rho_2$), while the first $\One$-cell cannot;
to mark this difference, and to make explicit the scope of the $\maltese$-cell introduced by the action of $\BoxR_{2}$ on $\rho_2$, we split the two conclusions of $R$ into two distinct \kl{components} via $R \pnrewrite[\Mix_{1}] R_0$.
\end{enumerate}

According to our rewrite rules, $R \pnrewrite[\Mix_{1}] R_0 \pnrewrite[\BoxR_{2}] R_0'$ and this rewriting commutes with the \kl{filled Taylor expansion} on quasi-proof-structures, as required by square \eqref{eq:naturality-square-bis} for naturality.
\end{example}

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

% !TEX root = mainFinal.tex
\section{\Gluability of \texorpdfstring{\polyadic}{DiLL} quasi-proof-structures and inhabitation}
\label{sec:glueable}

The properties of actions of schedulings allow us to prove two of our main original results:
\begin{enumerate}
\item a characterization of the sets of $\DiLL_0$ proof-structures that are in the Taylor expansion of some $\MELL$ proof-structure (\emph{inverse Taylor expansion problem}, \Cref{thm:characterization});

\item a characterization of the lists of \MELL formulas inhabited by some \kl{cut-free} \MELL proof-structure (\emph{type inhabitation problem} for cut-free \mbox{$\MELL$ proof-structures, \Cref{thm:inhabitation}}).
\end{enumerate}

Both characterizations are \emph{constructive}: when we claim the existence of an object (a \MELL proof-structure with a certain property), we can actually construct a witness of it, through our rewrite rules.
Thus, our characterizations can be seen as \emph{nondeterministic} procedures, because the rewritings to build witnesses are not unique.
Our procedures also \emph{decide} the problems above in special cases of interest (\Cref{thm:decisionFinite}, Proposition \ref{fact:decide-without-contractions}).

\subsection{\Gluability}
\label{sec:glueability}
We introduce the \emph{\gluability criterion} to solve the inverse Taylor expansion problem.
We actually solve it in two different domains.
We look for a solution:
\begin{enumerate}
\item in the set of \MELL proof-structures (\Cref{thm:characterization}.\ref{p:characterization-with-cut});
\item in the set of \kl{cut-free} \MELL proof-structures (\Cref{thm:characterization}.\ref{p:characterization-cut-free}).
\end{enumerate}

We say that a scheduling is \intro[cut-free scheduling]{cut-free} if does not contain the \kl{elementary scheduling} $\Cut^i$.

\begin{lemma}[cut-free scheduling]
\label{lemma:cut-free-scheduling}
Let $R$ be a \MELL quasi-proof-structure and $\sched$ be a \kl{scheduling} such that $R \pnrewrite[\sched] \emptynets$.
We have that $R$ is \kl{cut-free} if and only if $\sched$ is \kl[cut-free scheduling]{cut-free}.
\end{lemma}

\begin{proof}
Let $R$ be \MELL quasi-proof-structure.
If $R$ is \kl{cut-free} and $R \pnrewrite[a] R'$, then $a \neq \Cut^i$ because the action $R \pnrewrite[\Cut^i] R'$ requires the presence of a $\cut$-cell in $R$;
moreover, $R'$ is cut-free because no rewrite rule in \Cref{fig:actions-all}---when read left to right---introduces a $\cut$-cell.

Conversely, if $R$ is \kl{with cuts} and $R \pnrewrite[a] R'$ where $R'$  is cut-free, then $a = \Cut^i$, because among the rewrite rules in \Cref{fig:actions-all} only $\pnrewrite[\Cut_i]$ erases a $\cut$-cell.

A straightforward induction on the length of the scheduling $\sched$ allows us to conclude.
\end{proof}

\begin{definition}[\gluability, cut-free \gluability]
Let $\Pi$ be a set of $\DiLL_0$ quasi-proof-structures of type $\Gamma$.
If $\Pi = \emptyset$, then $\Pi$ is \emph{\gluable} and \emph{cut-free \gluable}.
If $\Pi \neq \emptyset$, $\Pi$ is \intro[glueable]{\gluable} (\resp~\intro[cut-free glueable]{cut-free \gluable}) if
$ \Pi \pnrewrite[\sched] \{\emptynets\}$ for some \kl{scheduling} (\resp~\kl{cut-free scheduling}) $\sched \colon \Gamma \to \emptylists$.
\end{definition}

\begin{theorem}[\gluability criterion]
\label{thm:characterization}
Let \(\Pi\) be a
set of $\DiLL_0$ proof-structures without $\maltese$-cells.
\begin{enumerate}
\item\label{p:characterization-with-cut} \(\Pi\) is \gluable if and only if $\Pi \subseteq \Taylor{R}$ for some \(\MELL\) proof-structure $R$.
\item\label{p:characterization-cut-free} \(\Pi\) is cut-free \gluable if and only if $\Pi \subseteq \Taylor{R}$ for some cut-free \(\MELL\) proof-structure~$R$.
\end{enumerate}
\end{theorem}

\begin{proof} If $\Pi = \emptyset$, Points \ref{p:characterization-with-cut}--\ref{p:characterization-cut-free} trivially hold.
So, we can now assume $\Pi \neq \emptyset$.
\begin{enumerate}
\item
If $\Pi \subseteq \Taylor{R}$ for some $\MELL$ proof-structure $R$,
then by normalization (Proposition \ref{prop:unwinding-to-empty})
$R \pnrewrite[\sched] \emptynets$ for some scheduling $\sched \colon (\Gamma) \to \emptylists$, where $\Gamma$ is the type of $R$ (and of each element of $\Pi$, by Remark \ref{rmk:conclusions}).
Therefore, $\Pi \pnrewrite[\sched] \{\emptynets\}$ by naturality
(\Cref{thm:projection-natural}), since $\emptyset \neq \Pi \pnrewrite[\sched] \Pi'$ implies $\Pi' \neq \emptyset$ (\Cref{foot:lifting}), and	$\FatTaylor{\emptynets} = \{\emptynets\}$ (Example~\ref{ex:filled-taylor-empty}).

Conversely, if $\Pi \pnrewrite[\sched] \{\emptynets\}$ for some scheduling $\sched \colon (\Gamma) \to \emptylists$ (where $\Gamma$ is the type of each element of $\Pi$), then by naturality (\Cref{thm:projection-natural}, as
$\FatTaylor{\emptynets} = \{\emptynets\}$) $\Pi \subseteq \FatTaylor{R}$ for some $\MELL$ quasi-proof-structure $R \pnrewrite[\sched] \emptynets$,
and so  $\Pi \subseteq \Taylor{R}$ since each element of $\Pi$ is without $\maltese$-cells.
The (\MELL) quasi-proof-structure $R$ is indeed a proof-structure as each element of $\Pi$ is a ($\DiLL_0$) proof-structure of type $\Gamma$, and by Remark \ref{rmk:conclusions} the type of $R$ is $\Gamma$.

\item Just repeat the same proof as above, paying attention that:
\begin{itemize}
\item in the ``if'' part,  if $R$ is cut-free, then the scheduling $\sched$
is cut-free by Lemma~\ref{lemma:cut-free-scheduling};
\item in the ``only if'' part, if $\Pi \pnrewrite[\sched] \{\emptynets\}$ for some cut-free scheduling $\sched \colon (\Gamma) \to \emptylists$, then by Lemma~\ref{lemma:cut-free-scheduling} $R$ is cut-free, since $R \pnrewrite[\sched] \emptynets$ according to naturality (\Cref{thm:projection-natural}).
\qedhere
\end{itemize}
\end{enumerate}
\end{proof}

Theorem \ref{thm:characterization} means that the action of a scheduling rewriting a set $\Pi$ of $\DiLL_0$ proof-structures to the empty proof-structure can be seen, read in reverse, as a sequence of elementary steps to build a \MELL proof structure that includes $\Pi$ in its Taylor expansion.

\begin{example}
An example of the \kl[action of scheduling on dill]{action of a scheduling} starting from  the singleton of a $\DiLL_0$ proof-structure $\rho$ and ending in \(\{\emptynets\}\) is in
\Cref{fig:longex2} (it is by no means the shortest possible rewriting).
When replayed backward,  by naturality (\Cref{thm:projection-natural}) it induces a \(\MELL\) proof-structure
\(R\) such that \(\rho\in \Taylor{R}\).
In \Cref{fig:longex2} we represent simultaneously the rewriting from $\Pi$ to $\{\emptynets\}$ and the rewriting from $R$ to $\emptynets$.
\end{example}

\input{fig-longex2Final}

We introduced two different \gluability criteria (Theorems \ref{thm:characterization}.\ref{p:characterization-with-cut} and \ref{thm:characterization}.\ref{p:characterization-cut-free}) because, given a non-empty set $\Pi$ of \emph{cut-free} $\DiLL_0$ proof-structures without $\maltese$-cells, the existence of a solution to the inverse Taylor expansion problem depends on whether we look for it among \MELL proof-structures or among \kl{cut-free} \MELL proof-structures (Example~\ref{ex:glueable-non-cut-free}).

\begin{example}
\label{ex:glueable-non-cut-free}
Let $\Sigma = \{\sigma_0\}$ as in \Cref{fig:rewrite-with-cut}.
This singleton of a cut-free $\DiLL_0$ proof-structure without $\maltese$-cells is \kl[glueable]{\gluable} (as shown by the action of the scheduling in \Cref{fig:rewrite-with-cut}) but not \kl[cut-free glueable]{cut-free \gluable} (as $\{\sigma_0\} \pnrewrite[\BoxR_1] \{\sigma\}$ and, apart from $\Cut^i$, no \kl{elementary schedulings} apply to $\{\sigma\}$ because of its type).
Indeed, $\sigma_0$ ``masks'' any information about the content $B$ of the box represented by its $\oc$-cell, apart from its type $\oc X$ which does not allow $B$ to be a cut-free $\MELL$ proof-structure (see also \Cref{sec:inhabitation}).
\Gluability (with cuts) of $\{\sigma\}$ is related to the fact that there is a \MELL proof-structure of type $X$ \kl{with cuts}, for every \kl{atomic formula} $X$ (see Remark \ref{rmk:non-cut-free}).
Note that $\sigma_0 \in \Taylor{S_0}$, and $\sigma \in \FatTaylor{S}$ and $\sigma' \in \FatTaylor{S'}$, where $S_0$, $S$ and $S'$ are the \MELL proof-structures with cuts represented in \Cref{fig:rewrite-with-cut}.
\end{example}

\begin{figure}[!t]
\vspace{\beforepn}
\centering
\scalebox{0.8}{
\begin{tabular}{c@{}c@{}c@{}c@{}c@{}c@{}c@{}c@{}c@{}c@{}c@{}c@{}c@{}c}
$\Sigma = \Bigg\{\!\!$\!\!
\scalebox{0.8}{
\vspace{\beforepn}
\pnet{
\pnformulae{\pnf[1']{$\oc X$}}
\pncown[1]{1'}
\!\!\scalebox{0.8}{
\vspace{\beforepn}
\pnet{
\pnformulae{\pnf[1']{$X$}}
\pndaimon[1]{1'}
\!\!\!\scalebox{0.8}{
\vspace{\beforepn}
\pnet{
\pnformulae{\pnf[1']{$X$}~\pnf[Xp]{$\wn X^\bot$}~\pnf[X]{$\oc X$}}
\pndaimon[1]{1',Xp,X}
\!\!\!\scalebox{0.8}{
\vspace{\beforepn}
\pnet{
\pnformulae{\pnf[1']{$X$}~\pnf[Xp]{$\wn X^{\!\bot}$}~\pnf[Xp2]{$\wn X^{\!\bot}$}~\pnf[X]{$\oc X$}}
\pndaimon[1]{1',Xp,Xp2,X}
\!\!\!\scalebox{0.8}{
\vspace{\beforepn}
\pnet{
\pnformulae{\pnf[1']{$X$}~\pnf[Xp]{$\wn X^{\!\bot}\!\!$}~~\pnf[Xp2]{$\wn X^{\!\bot}$}~\pnf[X]{$\oc X\,$}}
\pndaimon[1]{1',Xp}
\pndaimon[2]{Xp2,X}
\pnsemibox{1,Xp}
\pnsemibox{2,Xp2}
\!\!\!\scalebox{0.8}{
\vspace{\beforepn}
\pnet{
\pnformulae{\pnf[1']{$X$}~\pnf[Xp]{$\wn X^{\!\bot}\!\!$}~~\pnf[Xp2]{$\wn X^{\!\bot}$}~\pnf[X]{$X\,$}}
\pndaimon[1]{1',Xp}
\pndaimon[2]{Xp2,X}
\pnsemibox{1,Xp}
\pnsemibox{2,Xp2}
$\pnrewrite[\!\Der_2]\,\pnrewrite[\!\Der_3] \, \pnrewrite[\!\Ax_4] \, \pnrewrite[\!\Ax_2]$
\\
\qquad $\sigma_0$ & & $\sigma$ & & $\sigma'$
\end{tabular}

\vspace{-\baselineskip}
$S_0 = $
\scalebox{0.8}{
\pnet{
\pnformulae{
\pnf[X]{$X$}~\pnf[Xb]{$X^{\bot}$}~\pnf[Ab]{$X^{\bot}$}~\pnf[A]{$X$}
\pnaxiom[ax]{X,Xb}
\pnaxiom[axA]{A,Ab}
\pnbox{axA,Ab,A}
\pnexp{}{Xb,Ab}[a]{$\wn X^\bot$}[1.2]
\pnbag{}{A}[b]{$\oc X$}[1.2]
\pncut[cut]{b,a}
\pnbox{ax,Ab,A,X,Xb,axA,b,a,cut}
\pnbag{}{X}{$\oc X$}[3]
\qquad
$S = $
\scalebox{0.8}{
\pnet{
\pnformulae{
\pnf[X]{$X$}~\pnf[Xb]{$X^{\bot}$}~\pnf[Ab]{$X^{\bot}$}~\pnf[A]{$X$}
\pnaxiom{X,Xb}
\pnaxiom[ax]{A,Ab}
\pnbox{ax,Ab,A}
\pnexp{}{Xb,Ab}[a]{$\wn X^\bot$}[1.2]
\pnbag{}{A}[b]{$\oc X$}[1.2]
\pncut{b,a}
\qquad
$S' = $
\scalebox{0.8}{
\pnet{
\pnformulae{
\pnf[X]{$X$}~\pnf[Xb]{$X^{\bot}$}~\pnf[Ab]{$X^{\bot}$}~\pnf[A]{$X$}
\pnaxiom{X,Xb}
\pnaxiom[ax]{A,Ab}
\pnbox{ax,Ab,A}
\pnexp{}{Xb,Ab}[a]{$\wn X^\bot$}[1.2]
\pnbag{}{A}[b]{$\oc X$}[1.2]

\vspace{-\baselineskip}
\caption{Example of \gluability that is not cut-free \gluability.}
\label{fig:rewrite-with-cut}
\end{figure}

\begin{example}
\label{ex:not-coherent}
The three $\DiLL_0$ proof-structures $\rho_1, \rho_2, \rho_3$ below
are not \gluable as a whole, but are \gluable two by two (this is a slight variant of the example in \cite[pp.~244-246]{Tasson:2009}).
In fact, there is no \MELL proof-structure whose Taylor expansion contains $\rho_1, \rho_2, \rho_3$, but any pair of them is in the Taylor expansion of some \MELL proof-structure.

\begin{center}
\qquad\qquad\qquad\qquad\qquad\qquad
\qquad\qquad\qquad\qquad\qquad\qquad

\vspace*{-1.5\baselineskip}
\scalebox{0.65}{
\pnet{
\pnformulae{
\pnf[1]{$\mathbf{1}$}~\pnf[2]{$\mathbf{1}$}~\pnf[3]{$\mathbf{1}$}~
\pnf[4]{$\mathbf{1}$}~
\pnf[5]{$\bot$}~\pnf[6]{$\bot$}~\pnf[7]{$\bot$}~
\pnf[8]{$\bot$}~\pnf[9]{$\bot$}
\pnone{1}
\pnone{2}
\pnone{3}
\pnone{4}
\pnbot{5}
\pnbot{6}
\pnbot{7}
\pnbot{8}
\pnbot{9}
\pnbag{}{1,2}{$\oc \mathbf{1}$}
\pnbag{}{3}{$\oc \mathbf{1}$}
\pnbag{}{4}{$\oc \mathbf{1}$}
\pnexp{}{5}{$\wn \bot$}
\pnexp{}{6,7}{$\wn \bot$}
\pnexp{}{8,9}{$\wn \bot$}
\qquad
\tikzsetnextfilename{images/tasson-example-2}
\scalebox{0.65}{
\pnet{
\pnformulae{
\pnf[1]{$\mathbf{1}$}~\pnf[2]{$\mathbf{1}$}~\pnf[3]{$\mathbf{1}$}~
\pnf[4]{$\mathbf{1}$}~
\pnf[5]{$\bot$}~\pnf[6]{$\bot$}~\pnf[7]{$\bot$}~
\pnf[8]{$\bot$}~\pnf[9]{$\bot$}
\pnone{1}
\pnone{2}
\pnone{3}
\pnone{4}
\pnbot{5}
\pnbot{6}
\pnbot{7}
\pnbot{8}
\pnbot{9}
\pnbag{}{1}{$\oc \mathbf{1}$}
\pnbag{}{2,3}{$\oc \mathbf{1}$}
\pnbag{}{4}{$\oc \mathbf{1}$}
\pnexp{}{5,6}{$\wn \bot$}
\pnexp{}{7}{$\wn \bot$}
\pnexp{}{8,9}{$\wn \bot$}
\qquad
\tikzsetnextfilename{images/tasson-example-3}
\scalebox{0.65}{
\pnet{
\pnformulae{
\pnf[1]{$\mathbf{1}$}~\pnf[2]{$\mathbf{1}$}~\pnf[3]{$\mathbf{1}$}~
\pnf[4]{$\mathbf{1}$}~
\pnf[5]{$\bot$}~\pnf[6]{$\bot$}~\pnf[7]{$\bot$}~
\pnf[8]{$\bot$}~\pnf[9]{$\bot$}
\pnone{1}
\pnone{2}
\pnone{3}
\pnone{4}
\pnbot{5}
\pnbot{6}
\pnbot{7}
\pnbot{8}
\pnbot{9}
\pnbag{}{1}{$\oc \mathbf{1}$}
\pnbag{}{2}{$\oc \mathbf{1}$}
\pnbag{}{3,4}{$\oc \mathbf{1}$}
\pnexp{}{5,6}{$\wn \bot$}
\pnexp{}{7,8}{$\wn \bot$}
\pnexp{}{9}{$\wn \bot$}
\end{center}
Indeed, for any $i,j \in \{1,2,3\}$ with $i \neq j$, \(\rho_i\) and \(\rho_j\) are in the Taylor expansion of \(R_{ij}\) below.
\begin{center}
\qquad\qquad\qquad\qquad\qquad\qquad
\qquad\qquad\qquad\qquad\qquad\qquad

\vspace*{-1.5\baselineskip}
\scalebox{0.65}{
\pnet{
\pnformulae{
\pnf[1]{$\mathbf{1}$}~~~~\pnf[5]{$\bot$}\\\\
\pnf[7]{$\bot$}
\pnone[o1]{1}
\pnone[o2]{2}
\pnone[o3]{3}
\pnbot{4}
\pnbot{5}
\pnbot{6}
\pnbot{7}
\pnbag{}{1}{$\oc \mathbf{1}$}[3.75]
\pnbag{}{2}{$\oc \mathbf{1}$}[2.3]
\pnbag{}{3}{$\oc \mathbf{1}$}
\pnexp{}{4}{$\wn \bot$}[2.3]
\pnexp{}{5}{$\wn \bot$}[3.75]
\pnexp{}{6,7}{$\wn \bot$}
\pnbox{o1,1,5}
\pnbox{o2,2,4}
\pnbox{o3,3}
\qquad\qquad
\scalebox{0.65}{
\pnet{
\pnformulae{
\pnf[1]{$\mathbf{1}$}~~~~~~\pnf[7]{$\bot$}\\\\
\pnone[o1]{1}
\pnone[o2]{2}
\pnone[o3]{3}
\pnbot{4}
\pnbot{5}
\pnbot{6}
\pnbot{7}
\pnbag{}{1}{$\oc \mathbf{1}$}[3.75]
\pnbag{}{2}{$\oc \mathbf{1}$}
\pnbag{}{3}{$\oc \mathbf{1}$}[2.3]
\pnexp{}{4}{$\wn \bot$}[2.3]
\pnexp{}{5,6}{$\wn \bot$}
\pnexp{}{7}{$\wn \bot$}[3.75]
\pnbox{o1,1,7}
\pnbox{o2,2}
\pnbox{o3,3,4}
\qquad\qquad
\scalebox{0.65}{
\pnet{
\pnformulae{
\pnf[1]{$\mathbf{1}$}~~~\pnf[4]{$\bot$}
\pnone[o1]{1}
\pnone[o2]{2}
\pnone[o3]{3}
\pnbot{4}
\pnbot{5}
\pnbot{6}
\pnbot{7}
\pnbag{}{1}{$\oc \mathbf{1}$}
\pnbag{}{2}{$\oc \mathbf{1}$}[3.75]
\pnbag{}{3}{$\oc \mathbf{1}$}[2.3]
\pnexp{}{4,5}{$\wn \bot$}
\pnexp{}{6}{$\wn \bot$}[2.3]
\pnexp{}{7}{$\wn \bot$}[3.75]
\pnbox{o1,1}
\pnbox{o2,2,7}
\pnbox{o3,3,6}
\end{center}
\end{example}

Example \ref{ex:not-coherent} can be generalized to finite sets of any cardinality: for any \(n > 1\), there is a finite set $\Pi$ of \(n+1\) $\DiLL_0$ proof-structures that is not \gluable as a whole, but all subsets of $\Pi$ of at most \(n\) elements are \gluable.
This means that, for every $n > 1$, \gluability of a set $\Pi$ of $\DiLL_0$ proof-structures is not reducible to test that all subsets of $\Pi$ with at most $n$ elements satisfy some $n$-ary coherence relation, unless (obviously) $\Pi$ is a finite set with at most $n$ elements.
As explained in \Cref{sect:intro}, this difficulty in the inverse Taylor expansion problem is typical of $\MELL$ and does not arise in the $\lambda$-calculus.

\begin{remark}[infinite sets]
\label{rmk:infinite}
The \gluability criterion (\Cref{thm:characterization}) is not limited to finite sets of \(\DiLL_0\) proof-structures, it holds for infinite sets too.
This raises the question of the relationship between \gluability and finite \gluability, namely: when every finite subset of a given infinite set of $\DiLL_0$ proof-structures is \gluable, is the infinite set itself \gluable too?
The answer is negative.
Let \(\Pi\) be an \emph{infinite} set of \(\DiLL_0\) proof-structures such that \emph{every finite} subset of \(\Pi\) is \gluable.
There are two cases for $\Pi$.
\begin{itemize}

\item \(\Pi\) itself is \gluable. It is typically the case when \(\Pi\) is exactly the
Taylor expansion of a \(\MELL\) proof-structure $R$ with at least one box, such as in the following example.
\begin{center}
\vspace{\beforepn}
$\Pi = \Bigg\{
\scalebox{0.8}{
\pnet{
\pnformulae{\pnf[1']{$\one$}~\pnf{$\overset{n}{\dots}$}~\pnf[1'']{$\one$}}
\pnone[1]{1'}
\pnone[1bis]{1''}
\pnbag{}{1',1''}{$\oc \one$}
\mathrel{\bigg|} n \in \Nat \Bigg\}
\  \pnrewrite[\BoxR_1] \
\bigg\{
\scalebox{0.8}{
\pnet{
\pnformulae{\pnf[1']{$\one$}}
\pnone[1]{1'}
\bigg\}
\ \pnrewrite[\One_1] \
\{\emptynet\}
\qquad\qquad\quad
$R =
\scalebox{0.8}{
\pnet{
\pnformulae{\pnf[1']{$\one$}}
\pnone[1]{1'}
\pnbox{1,1'}
\pnbag{}{1'}{$\oc \one$}[1.2]
\end{center}

We might say that
\(\Pi\) is \emph{infinite in width}: infinity is related to the number of
copies chosen for the boxes of $R$, a number that has to be finite but can
be arbitrarily large.

\item \(\Pi\) is not \gluable.
This is the case in the following set (we draw three elements only).

\begin{center}
\vspace{\beforepn}
$\Pi = \Bigg\{$ \!\!
\scalebox{\smallproofnets}{
\raisebox{-1.4cm}{
\pnet{
\pnformulae{~~\pnf[ba]{$\oc X$}~\pnf[na]{$X^{\bot}$}\\\\\\
\\
\pnf[na']{$\wn X^{\bot}$}~~~~~\pnf[a]{$X$}
\pnwn{na'}
\pncown{ba}
\pnaxiom{na,a}
\pntensor{ba,na}[bana]{$\oc X \otimes X^{\bot}$}
\pnexp{}{bana}{$\wn (\oc X \otimes X^{\bot})$}[1.1]
\quad
\raisebox{-0.7cm}{
\pnet{
\pnformulae{~\pnf[ba]{$\oc X$}~\pnf[na]{$X^{\bot}$}~\pnf[a]{$X$}\\\\
\pnf[na']{$\wn X^{\bot}$}~~~~~~\pnf[a1]{$X$}
\pnwn{na'}
\pncown{ba}
\pnaxiom{na,a}
\pntensor{ba,na}[bana]{$\oc X \otimes X^{\bot}$}[1.2]
\pnbag{}{a}[bal]{$\oc X$}[1.2]
\pnaxiom{na1,a1}
\pntensor{bal,na1}[balna1]{$\oc X \otimes X^{\bot}$}
\pnexp{}{bana,balna1}{$\wn (\oc X \otimes X^{\bot})$}[1.1]
\quad
\pnet{
\pnformulae{\pnf[ba2]{$\oc X$}~\pnf[na2]{$X^{\bot}$}~\pnf[a2]{$X$}\\\\
\pnf[na']{$\wn X^{\bot}$}~~~~~~~~\pnf[a1]{$X$}}
\pnwn{na'}
\pnbag{}{a2}[ba]{$\oc X$}[1.2]
\pncown{ba2}
\pnaxiom{na2,a2}
\pntensor{ba2,na2}[bana2]{$\oc X \otimes X^{\bot}$}[1.2]
\pnaxiom{na,a}
\pntensor{ba,na}[bana]{$\oc X \otimes X^{\bot}$}[1.2]
\pnbag{}{a}[bal]{$\oc X$}[1.2]
\pnaxiom{na1,a1}
\pntensor{bal,na1}[balna1]{$\oc X \otimes X^{\bot}$}
\pnexp{}{bana,balna1,bana2}{$\wn (\oc X \otimes X^\bot)$}[1.1]
\ \dots $\Bigg\}$
\end{center}
Every finite subset of $\Pi$ is \gluable, but the whole infinite set $\Pi$ is not.
We might say that \(\Pi\) is \emph{infinite in depth}: in $\Pi$, for every $n > 0$ there is a $\DiLL_0$ proof-structure with $n$ $\oc$-cells.
Any finite subset $\Pi_n$ of $\Pi$ ($n$ is the maximal number of $\oc$-cells in the elements of $\Pi_n$) is included in the Taylor expansion of a $\MELL$ proof-structure with \kl[depth of proof-structure]{depth} $n$, and indeed the action of the scheduling $\nu_n^1$ defined in Example \ref{ex:church} rewrites $\Pi_n$ to $\{\emptynets\}$.\footnotemark
\footnotetext{\label{note:church}In fact, if $\pi_h$ is the element of such a $\Pi$ with exactly $h$ $\oc$-cells, $\{\pi_h\} \pnrewrite[\nu_n^1] \{\emptynets\}$ for all $n \geqslant h$.}
However, the whole $\Pi$ can only been seen as the Taylor expansion of an ``infinite'' proof-structure with infinitely deep nested boxes.
Such infinite proof-structures are not in the syntax of $\MELL$.
An ongoing research  relates them to non-well-founded proofs for fixed-point~logics~\cite{Infinets1,Infinets2}.
\end{itemize}
\end{remark}

In the inverse Taylor expansion problem, both kinds of infinity---in width and in depth---arise already in the $\lambda$-calculus, they are not specific to $\MELL$.
An instance of a set of resource $\lambda$-terms that is infinite in width is the Taylor expansion of the $\lambda$-term $xy$.
The set $\Pi = \{\lambda f. \lambda x. f [\,],\allowbreak \
\lambda f. \lambda x. f [f [\,] ],\allowbreak \
\lambda f. \lambda x. f [f [f [\,] ]], \
\dots\}$
of resource $\lambda$-terms is an example of infinity in depth: every finite subset of $\Pi$ is included in the Taylor expansion of some $\lambda$-term (a Church numeral), but $\Pi$ is not included in the Taylor expansion of any $\lambda$-term.

\subsection{Inhabitation}
\label{sec:inhabitation}
We can characterize type inhabitation in $\MELL$ proof-structures.
We first put the question of type inhabitation for $\MELL$ proof-structures in a proper way.

\begin{remark}[inhabitation with cuts is trivial]
\label{rmk:non-cut-free}
For every \kl{atomic} formula $X$ there is a \MELL proof-structure of type $X$ \kl{with cuts}, the one called $S$ in \Cref{fig:rewrite-with-cut}.
More generally, for every $\MELL$ formula $A$ (\resp~list $\Gamma$ of \MELL formulas), there is a \MELL proof-structure of type $A$ (\resp~$\Gamma$) possibly with cuts.
Indeed, for $A$ just ``$\eta$-expand'' $S$ in \Cref{fig:rewrite-with-cut}, by replacing each $\ax$-cell in $S$ with the ``canonical'' \MELL proof-structure of type $A, A^\bot$.
For $\Gamma = \allowbreak(A_1, \dots, A_n)$, repeat the same procedure for each $A_i$ separately, and juxtapose the \MELL proof-structures to yield a unique \MELL proof-structure $R$ of type $\Gamma$ (take $R = \emptynet$ if $\Gamma = \emptylist$).

Therefore, type inhabitation for \MELL proof-structures is trivial, if $\cut$-cells are allowed.
\end{remark}

Type inhabitation for \MELL proof-structures is a non-trivial problem only if we restrict to \emph{\kl{cut-free}} \MELL proof-structures.
Indeed, given two propositional variables $X \neq Y$, there is no \emph{cut-free} \MELL proof-structure of type $X$ or $Y, X$.
So, the problem is the following:
\begin{description}
\item[Data] a list $\Gamma$ of \MELL formulas;
\item[Question] does there exist a \kl{cut-free} \MELL proof-structure of type $\Gamma$?
\end{description}
We study the \emph{type inhabitation problem for cut-free \MELL proof-structures} via schedulings, following the idea that a \kl{scheduling} $\sched \colon (\Gamma) \to \emptylists$ ``encodes'' a \MELL proof-structure of type $\Gamma$.

Let us see the behavior of \kl[cut-free schedulings]{\emph{cut-free} schedulings}.
For some list $\Gamma$ of \MELL formulas there is no cut-free scheduling $\sched \colon (\Gamma) \to \emptylists$.
For instance, if $X \neq Y$ are propositional variables and we exclude $\Cut^i$, then there are no \kl{elementary schedulings} from $(X)$, while the only other elementary schedulings from $(Y,X)$ are $\Mix_1$ and $\Ex_1$.
The non-existence of a cut-free-scheduling from $(X)$ or $(Y,X)$ to $\emptylists$ goes hand in hand with the non-existence of a cut-free $\MELL$ proof-structure of type $X$ or $Y,X$, by Proposition \ref{prop:unwinding-to-empty} and Lemma~\ref{lemma:cut-free-scheduling}.

Conversely, for any list $\Gamma$ of \MELL formulas, a \MELL proof-structure $R(\sched)$ of type $\Gamma$ is associated with every scheduling $\sched \colon (\Gamma) \to \emptylists$: such a $R(\sched)$ is built by reading $\sched$ backward, it exists and is uniquely determined because the action of $\sched$ is \emph{co-functional} (Lemma \ref{prop:unwinding-co-functional}).

\begin{definition}[building from scheduling]
\label{def:building}
Let $\Gamma \neq \emptylist$ be a list of lists of \MELL formulas, and $\sched \colon \Gamma \to n\emptylist$ be a  scheduling with $n \!>\! 0$.
The \MELL quasi-proof-structure $R(\sched)$ is defined by induction on the \kl[scheduling length]{length} of $\sched$: if $\sched$ is \kl[empty scheduling]{empty}, $R(\sched) = n \emptynet$;
otherwise $\sched = a \schedtwo$ for some elementary scheduling $a$, and $R(\sched)$ is the only \MELL quasi-proof-structure $R$ such that $R \pnrewrite[a] R(\schedtwo)$.
\end{definition}

Clearly, for any scheduling $\sched \colon \Gamma \to \emptylists$, $R(\sched)$ is of type $\Gamma$ and $R(\sched) \pnrewrite[\sched] \emptynets$, and $R(\sched)$ is cut-free if and only if so is $\sched$ (Lemma \ref{lemma:cut-free-scheduling}).
Actually, cut-free schedulings are a way to characterize the (lists of) \MELL formulas that are the type of some \kl{cut-free} \MELL proof-structure.

\begin{thm}[type inhabitation for cut-free \MELL proof-structures]
\label{thm:inhabitation}
Let $\Gamma$ be a list of \MELL formulas.
There is a \kl{cut-free} \MELL proof-structure of type $\Gamma$ if and only if there is a  \kl{cut-free scheduling} $\sched \colon (\Gamma) \to \emptylists$.
\end{thm}

\begin{proof}
If $\sched \colon (\Gamma) \to \emptylists$ is a cut-free scheduling, $R = R(\sched)$ is a \MELL quasi-proof-structure of type $\Gamma$. As $\Gamma$ is a list of \MELL formulas, $R$ is a proof-structure.
By Lemma~\ref{lemma:cut-free-scheduling}, $R$ is cut-free.

Conversely, if $R$ is a cut-free \MELL proof-structure of type $\Gamma$, then
$R \pnrewrite[\sched] \emptynets$ for some cut-free scheduling $\sched \colon (\Gamma) \to \emptylists$, by Proposition \ref{prop:unwinding-to-empty} and Lemma~\ref{lemma:cut-free-scheduling}.
\end{proof}

Lemma \ref{prop:unwinding-co-functional}, Definition \ref{def:building} and the proof of Theorem \ref{thm:inhabitation} say that, given a list $\Gamma$ of \MELL formulas, any cut-free scheduling from  $(\Gamma)$ to $\emptylists$ can be seen, when read backward, as a sequence of elementary steps to build a cut-free \MELL proof-structure of type $\Gamma$~from~scratch.

Consider now the \emph{procedure} $\mathcal{P}_1$ below, given a list $\Gamma$ of \MELL formulas as input:
\begin{enumerate}
\item for all $n \geqslant 0$, take all cut-free schedulings from $(\Gamma)$ of \kl[scheduling length]{length} $n$ (there are finitely many);
\item as soon as a list of the form $\emptylists$ is reached by a cut-free scheduling, accept $\Gamma$.
\end{enumerate}

\Cref{thm:inhabitation} guarantees that such a \emph{nondeterministic} procedure accepts $\Gamma$ if and only if there is a cut-free \MELL proof-structure of type $\Gamma$, and any cut-free scheduling $\sched$ that allows the procedure to accept $\Gamma$ also constructs a witness $R(\sched)$.
Therefore, we can conclude:

\begin{fact}[semi-decidability]
Procedure $\mathcal{P}_1$ semi-decides the type inhabitation problem for cut-free \MELL proof-structures.
\end{fact}

Procedure $\mathcal{P}_1$ need not halt.
Indeed, in general, there is no bound on the length of cut-free schedulings, and the elementary scheduling $\Contr_i$ can create cut-free schedulings of arbitrary length with target $\emptylists$, such as $\schedtwo_n$ below---of length $3n+1$---for every $n \geqslant 0$.
\schedtwo_n = \underbrace{\Contr_1 \cdots \Contr_1}_{n \text{ times}} \underbrace{\Mix_{1} \Weak_1 \cdots \Mix_{1} \Weak_1}_{n \text{ times}} \Weak_1 \ \colon \, (\wn X) \to (n+1)\emptylist

Consider now the \emph{procedure} $\mathcal{P}_2$ below, a slight variant of $\mathcal{P}_1$ for the same input $\Gamma$:

\begin{enumerate}
\item for all $n \geqslant 0$, take all cut-free schedulings from $(\Gamma)$ of \kl[scheduling length]{length} $n$ that do not contain the elementary scheduling $\Contr_{i}$ (there are finitely many);
\item as soon as a list of the form $\emptylists$ is reached by one of those schedulings, accept $\Gamma$.
\end{enumerate}

Procedure $\mathcal{P}_2$ always halts.
Indeed, define the following \emph{sizes}:
\begin{itemize}
\item the size $\Size{A}$ of a \MELL formula $A$ is the number of \kl[atomic formula]{atoms}, \kl{connectives} and \kl{units} occurring in $A$, \ie $\Size{X} = \Size{\One} = 1$, $\Size{A \otimes B} =  \Size{A} + \Size{B} + 1$, $\Size{\oc A} = \Size{A} + 1$ and $\Size{A^\perp} = \Size{A}$;

\item the size of a list $(A_1, \dots, A_n)$ of \MELL formulas is the sum $\sum_{i=i}^n\Size{A_i}$;
\item the size of a (non-empty) list $\Gamma$ of lists of \MELL formulas is $\Size{\Gamma} = (|\Gamma|, \mathsf{n}(\Gamma))$ with the lexicographic order, where $|\Gamma|$ is the size of the \kl{flattening} of $\Gamma$, and $\mathsf{n}(\Gamma)$ is the finite multiset of the lengths of each list in $\Gamma$, with the multiset order.
\end{itemize}

One has $\Size{\Gamma} > \Size{\Gamma'}$ for any \kl{elementary scheduling} $a \colon \Gamma \to \Gamma'$ except
\begin{itemize}
\item when $a = \Cut^{i}$ since $\Size{\Gamma} < \Size{\Gamma'}$, but $\mathcal{P}_2$  considers cut-free schedulings only;
\item when $a = \Ex_{i}$ since $\Size{\Gamma} = \Size{\Gamma'}$, but infinite chains of consecutive $\Ex_{i}$ are irrelevant, because for every $\Gamma$, sufficiently long schedulings $\Ex_{i_1} \dots \Ex_{i_n}$ are from $\Gamma$ to $\Gamma$;\footnotemark
\footnotetext{\label{note:exc-schedule}Indeed, for every list $\Gamma \neq \emptylist$ of lists of \MELL formulas, there is $N_\Gamma \geqslant 0$ such that, for every scheduling $\sched \colon \Gamma \to \Delta$ only made of $\Ex_{i}$, there is a scheduling $\schedtwo \colon \Gamma \to \Delta$ only made of $\Ex_{i}$ and of length $\leqslant N_\Gamma$.}

\item when $a = \Contr_{i}$ since $\Size{\Gamma} < \Size{\Gamma'}$, but $\mathcal{P}_2$ only considers schedulings without $\Contr_{i}$.
\end{itemize}

The nondeterministic procedure $\mathcal{P}_2$ decides the type inhabitation problem in a subset of \MELL proof-structures.
We say that a $\wn$-cell with a least two inputs is a \emph{strict contraction}.
Note that if $a = \Contr_{i}$ and $R \pnrewrite[a] R'$ is not \kl[nullary splitting for elementary scheduling]{nullary $\Contr$-splitting}, then $R$ has a strict contraction.

\begin{proposition}[decidability without strict contractions]
\label{fact:decide-without-contractions}
Procedure $\mathcal{P}_2$ decides the type inhabitation problem for cut-free $\MELL$ proof-structures \emph{without strict contractions}, that is,
\begin{description}
\item[Data] a list $\Gamma$ of \MELL formulas;
\item[Question] is there a cut-free \MELL proof-structure of type $\Gamma$ without strict contractions?
\end{description}
\end{proposition}

\begin{proof}
Let $\Gamma$ be a list of \MELL formulas.
Termination of $\mathcal{P}_2$ on input $\Gamma$ is proved above.

If $\mathcal{P}_2$ accepts $\Gamma$, then there is a cut-free scheduling $\sched \colon (\Gamma) \to \emptylists$ that does not contain $\Contr_{i}$.
According to Definition \ref{def:building}, it is immediate to prove that $R(\sched)$ has no strict contractions.

If there is a cut-free \MELL proof-structure $R$ of type $(\Gamma)$ without strict contractions, then there is a  scheduling $\sched \colon (\Gamma) \to \emptylists$ such that $R \pnrewrite[\sched] \emptynets$ without nullary $\Contr$-splittings (Proposition \ref{prop:unwinding-to-empty}).
Since $R$ has no strict contractions, then $\sched$ does not contain any $\Contr_i$, so $\mathcal{P}_2$ accepts $\Gamma$.
\end{proof}

Type inhabitation for cut-free \MELL proof-structures depends on whether strict contractions are allowed or not: the list $\oc X, \wn X^\perp, \oc X$ is accepted by $\mathcal{P}_1$ but rejected by $\mathcal{P}_2$, indeed the only cut-free \MELL proof-structure of type $\oc X, \wn X^\perp, \oc X$ has a strict contraction.

\begin{remark}[on decidability of $\MELL$]
Our characterization of type inhabitation for cut-free $\MELL$ proof-structures (Theorem \ref{thm:inhabitation}) can be
seen in relation to the question of deciding if a \(\MELL\) formula is provable: indeed, a
\MELL formula \(A\) is provable if and only if there is a \emph{correct} cut-free $\MELL$ proof-structure of type $A$ (for some notion of correctness).

In the propositional setting, $\MLL$ provability is decidable and
\(\mathbf{NP}\)-complete \cite{Kanovich94},   while
\(\LL\) provability is undecidable  \cite{Lincoln1992};
a longstanding open problem is whether provability in \(\MELL\) is  decidable or not.
Our result offers a fresh perspective on it.

Take again procedure $\mathcal{P}_1$ above
with the same input $\Gamma$, and replace its second step by:
\begin{enumerate}
\setcounter{enumi}{1}
\item if a list of the form $\emptylists$ is reached by a cut-free scheduling $\sched$, construct the cut-free \MELL proof-structure $R = R(\sched)$ of type $\Gamma$;
\item check if $R$
fulfills a suitable correctness criterion that characterizes all and only the \MELL proof-structures corresponding to a derivation in
\MELL sequent calculus, \eg \cite{Tortora03};
\item as soon as a correct (cut-free) \MELL proof-structure is found, accept $\Gamma$.
\end{enumerate}
As explained above, there may be infinitely many cut-free schedulings  $\sched \colon (\Gamma) \to \emptylists$, and also infinitely many cut-free \MELL proof-structures of type $\Gamma$.
But they are finite in number in the case without strict contractions.
As correctness of a \MELL proof-structure is decidable, the procedure above \emph{semi-decides} provability in \MELL (is a given sequent provable in \MELL sequent calculus?) and \emph{decides} provability in \MELL \emph{without contractions} (is a given sequent provable in \MELL sequent calculus without the contraction rule?).
Our procedure restricts its search to cut-free objects, without loss of generality by cut-elimination.
Semi-decidability of \MELL provability and decidability of \MELL provability without contractions are not new results;
another (and simpler) proof relies on the fact that in \MELL sequent calculus every inference rule other than contraction and cut, read bottom-up, decreases  the size of a sequent, for a suitable notion of size.
What is new is the analogy between the type inhabitation problem for cut-free \MELL proof-structures and the provability problem in \MELL.

Summing up, (strict) contraction is the only reason that makes hard to prove whether type inhabitation for cut-free $\MELL$ proof-structures, as well as $\MELL$ provability, are decidable or not.
This seems to suggest that \emph{correctness} (the fact that a $\MELL$ proof-structure is a proof of a $\MELL$ formula) does not play an essential role in the question if $\MELL$ provability is decidable or not.
However, for the time being, we are not able to reduce decidability of provability in \MELL to decidability of type inhabitation for cut-free \MELL proof-structures.
\end{remark}

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

% !TEX root = mainFinal.tex
\section{Decidability of the finite inverse Taylor expansion problem}
\label{sec:decidability}

Consider the decision problem below, called the \emph{finite inverse Taylor expansion problem}.

\begin{description}
\item[Data] a \emph{finite} set $\Pi$ of $\DiLL_0$ proof-structures without $\maltese$-cells;
\item[Question] does there exist a \MELL proof-structure $R$ such that $\Pi \subseteq \Taylor{R}$?
\end{description}

By Theorem~\ref{thm:characterization},
a positive answer is equivalent to the \gluability of \(\Pi\), thus the question amounts to decide the \kl[glueable]{\gluability} of a finite set $\Pi$ of $\DiLL_0$ proof-structures without $\maltese$-cells.
In this section, we show that the problem is actually \emph{decidable}, using our rewrite rules.
The challenge here is to restrict the search space for rewritings to guarantee termination.

Recall that the action of $\BoxR_{i}$ is the only rewrite rule in $\DiLL_0$ that can introduce $\maltese$-cells (\Cref{fig:empty-box}).
We identify $\maltese$-cells that have the same number of outputs, with the same type.

\begin{remark}[$\maltese$-cell]
Let $\Sigma, \Pi$ be sets of $\DiLL_0$ quasi-proof-structures such that every element of $\Sigma$ is without $\maltese$-cells, $\Sigma \pnrewrite[\sched] \Pi$ and $\Pi$ is \gluable.
The presence of $\maltese$-cells in $\Pi$  witnesses the absence of information on the content of some box of some element of $\Sigma$.
However, in order that $\Pi$ is \gluable, either this lack of information in some element of $\Pi$ is provided by another element of $\Pi$, or the information is plainly missing.
Indeed, let $\Pi$ be a set of $\DiLL_0$ proof-structures, and $i$ be a conclusion of some $\rho \in\Pi$ and the output of a $\maltese$-cell of $\rho$;
we have two cases (Definition \ref{def:daimon-nonDaimonSched} below relies on this distinction):
\begin{enumerate}
\item either $i$ is the output of a $\ell$-cell of \emph{some} $\DiLL_0$ quasi-proof-structure $\pi \in\Pi$, with $\ell\neq\maltese$;
\item or $i$ is the output of a $\maltese$-cell of \emph{every} $\DiLL_0$ quasi-proof-structure $\pi \in\Pi$; in this case the component of every $\pi \in\Pi$ having $i$ among its conclusions consists of the same $\maltese$-cell.
\end{enumerate}
\end{remark}

Let $n>0$ and $\Gamma = (\Gamma_{\!1}; \dots; \Gamma_{\!n})$ be a list of lists of \MELL formulas.
We denote by $\maltese_\Gamma$ the $\DiLL_0$ quasi-proof-structure $(\rho_{\Gamma_{\!1}}, \dots, \rho_{\Gamma_{\!n}})$ of type $\Gamma$, where $\rho_{\Gamma_{\!i}}$ is the daimon of type $\Gamma_{\!i}$ if $\Gamma_{\!i} \neq \emptylist$, and $\rho_{\Gamma_{\!i}} = \emptynet$ if $\Gamma_{\!i} = \emptylist$.
Lemma \ref{lemma:action-daimons} below states that every $\{\maltese_\Gamma\}$ is \gluable:
an example for $\Gamma = (X)$ with $X$ \kl{atomic} is in \Cref{fig:rewrite-with-cut} (see the daimon $\sigma$ there).
A set $\Pi$ of $\DiLL_0$ quasi-proof-structures is \intro[full]{$\maltese$-full} if $\Pi = \{\maltese_\Gamma\}$ for some $\Gamma$.
Note that any $\{\emptynets\}$ is $\maltese$-full.

An elementary scheduling $\Cut^i$ is \emph{with conclusion} if $\Gamma_{\!k} \neq \emptylist$ in its definition in \Cref{fig:elementary-schedulings}.

\begin{lemma}[\gluability of daimons]
\label{lemma:action-daimons}
Every $\maltese$-full set of $\DiLL_0$ quasi-proof-structures is \gluable.
More precisely, let $\Gamma$ be a non-empty list of lists of \MELL formulas.
\begin{enumerate}
\item\label{p:action-daimons-scheduling} there is a scheduling $\sched \colon \Gamma \to \emptylists$ such that every $\Cut^i$ in $\sched$ is with conclusion;
\item\label{p:action-daimons-glueable} if $\sched \colon \Gamma \to \emptylists$ and every $\Cut^i$ in $\sched$ is with conclusion, then $\{\maltese_{\Gamma}\} \pnrewrite[\sched] \{\emptynets\}$.
\end{enumerate}
\end{lemma}

\begin{proof}
By Points \ref{p:action-daimons-scheduling} and \ref{p:action-daimons-glueable}, every $\maltese$-full set of $\DiLL_0$ quasi-proof-structures is \gluable.
\begin{enumerate}
\item For every \MELL formula $A$, we define by induction on $A$ a scheduling $\sched_A \colon (A) \to \emptylists$ where every $\Cut^i$ in $\sched_A$ is with conclusion.
We shall use the fact that for every \MELL formula $A$ and lists $\Delta, \Gamma$ of \MELL formulas, given a scheduling $\sched_A \colon (A) \to \emptylists$, one has $\sched_A \colon (A, \Delta; \Gamma) \to (\Delta; \Gamma)$ and $\sched_A \colon (\emptylist; A, \Gamma) \to (\emptylist; \Gamma)$.
Let $\schedtwo_A = \Cut^2 \Contr_2 \Mix_{2} \BoxR_{4} \Der_2 \Der_3 \colon \allowbreak (A) \to (A, A^\perp; A^\perp, A)$ and note that $\Cut^2$ in $\schedtwo_A$ is with conclusion.
\begin{itemize}
\item If $A = X$ (and similarly if $A = X^\perp$), then $\sched_A = \schedtwo_A \Ax_{4} \Ax_{2}$.
\item If $A = \One$ then $\sched_A = \One_1$; if $A = \bot$ then $\sched_A = \bot_1$.
\item If $A = B \otimes C$ (similarly if $A = B \parr C$), $\sched_A = \schedtwo_A \otimes_4 \parr_3 \parr_2 \otimes_1 \sched_{B} \sched_{C} \sched_{B^\perp} \sched_{C^\perp} \sched_{B^\perp} \sched_{C^\perp} \sched_{B} \sched_{C}$.
\item If $A = \oc B$ (and similarly if $A = \wn B$), then $\sched_{A} = \schedtwo_{A} \BoxR_4 \Der_3 \BoxR_1 \Der_2 \sched_{B} \sched_{B^\perp}  \sched_{B^\perp} \sched_{B}$.
\end{itemize}
Let $\Gamma = (A_1, \dots, A_{i_1}; \cdots; A_{i_{n\!-\!1}\!+\!1}, \dots, A_{m})$ be a non-empty list of lists of \MELL formulas.
In the scheduling $\sched_{A_1\!} \cdots \sched_{A_{i_1}\!} \cdots \sched_{A_{i_{n\!-\!1}\!+\!1}\!} \cdots \sched_{A_{m}} \colon \Gamma \to \emptylists$ every $\Cut^i$ is with conclusion.

\item By induction on the length $k \geqslant 0$ of the scheduling $\sched = a_1 \!\cdots a_k$, where $a_j$ is an elementary scheduling for all $1 \leqslant j \leqslant k$.
It is crucial that every $a_j = \Cut^i$ is with conclusion: otherwise, for a daimon $\rho'$ there is no $\rho$ such that $\{\rho\} \pnrewrite[\!\Cut^i\!] \{\rho'\}$ (see \Cref{fig:cut-daimon}).
\qedhere
\end{enumerate}
\end{proof}

Therefore, by Lemma \ref{lemma:action-daimons}, to prove that a set $\Pi$ of $\DiLL_0$ proof-structures is \gluable, it suffices to show that  $\Pi$ rewrites to a \kl[full]{$\maltese$-full} set $\Pi'$.
A more subtle question is to prove that if $\Pi$ cannot rewrite to a \kl[full]{$\maltese$-full} set $\Pi'$, then $\Pi$ is not \gluable (Lemma \ref{lemma:CanonicalScheduling} below).

\begin{definition}[$\maltese$-/$\lnot\maltese$-actions, canonicity]
\label{def:daimon-nonDaimonSched}
Let $\Pi$ be a set of $\DiLL_0$ quasi-proof-structures with the same conclusions.
Suppose that $\Pi\pnrewrite[a]\Pi'$ where $a \neq \Cut^{i}$ (resp.\ $a = \Cut^{i}$) is an elementary scheduling that
acts on the conclusion $i$ of all elements of $\Pi$ (\resp $\Pi'$). If for every $\rho \in\Pi$ (resp.\ $\rho'\in\Pi'$) the conclusion $i$ of $\rho$ (\resp $\rho'$) is the output of a $\maltese$-cell, then
we say that $\Pi \pnrewrite[a] \Pi'$ is a \intro[daimon action]{$\maltese$-action}.
If $\Pi \pnrewrite[\sched]\Pi'$ and for every elementary scheduling $a$ such that $\Pi \pnrewrite[\sched]\Pi'=\Pi \pnrewrite[\sched_{1}]\Pi_{1}\pnrewrite[a]\Pi_{2}\pnrewrite[\sched_{2}]\Pi'$
one has that $\Pi_1 \pnrewrite[a] \Pi_2$ is (resp.\ is not) a $\maltese$-action, we say that $\Pi\pnrewrite[\sched]\Pi'$ is a \emph{$\maltese$-action} (\resp \intro[nondaimon action]{$\neg\maltese$-action}), written $\Pi\pnrewrite[\maltese]\Pi'$ (\resp $\Pi\pnrewrite[\!\neg\maltese]\Pi'$).

If $\Pi\pnrewrite[\sched]\{\emptynets\} = \Pi\pnrewrite[\!\neg\maltese]\,\pnrewrite[\maltese]\{\emptynets\}$,
then $\Pi\pnrewrite[\sched]\{\emptynets\}$ is \intro{canonical} and $\Pi$ is \intro[canonically glueable]{canonically \gluable}.
\end{definition}

So, given a set $\Pi_0$ of $\DiLL_0$ quasi-proof-structures and a $\maltese$-action $\Pi_0 \pnrewrite[\!a_1] \allowbreak\dots \pnrewrite[\!a_n] \Pi_n$, for all $1\leqslant j \leqslant n$ the elementary scheduling $a_j$ acts on a conclusion of a daimon in \emph{all} elements of $\Pi_{j-1}$.
On the other hand, in a $\lnot\maltese$-action $\Pi_0 \pnrewrite[\!a_1] \allowbreak\dots \pnrewrite[\!a_n] \Pi_n$, for all $1\leqslant j \leqslant n$ the elementary scheduling $a_j$ acts on the output of a $\ell$-cell with $\ell \neq \maltese$ in \emph{some} element of~$\Pi_{j-1}$.

\begin{remark}[fullness]
\label{rmk:full}
Let $\Pi$ be a set of $\DiLL_0$ quasi-proof-structures, and $\sched$ be a scheduling.
By straightforward induction on the length of $\sched$, we can prove the facts below.
\begin{itemize}
\item If $\Pi$ is $\maltese$-full and $\Pi \pnrewrite[\sched] \Pi'$ for some set $\Pi'$, then $\Pi \pnrewrite[\sched] \Pi'$ is a $\maltese$-action and $\Pi'$ is $\maltese$-full.
\item If $\Pi \pnrewrite[\sched] \{\emptynets\}$, then $\Pi \pnrewrite[\sched] \{\emptynets\}$ is a \kl[daimon action]{$\maltese$-action} if and only if $\Pi$ is $\maltese$-\kl{full}.
Therefore, $\Pi\pnrewrite[\sched]\{\emptynets\}$ is \kl{canonical} if and only if $\Pi\pnrewrite[\sched]\{\emptynets\} = \Pi \pnrewrite[\lnot\maltese] \Pi' \pnrewrite[\maltese] \{\emptynets\}$ for some \kl[full]{$\maltese$-full} $\Pi'$.
\end{itemize}
\end{remark}

The following lemma relies on the fact that $\maltese$-actions can always be delayed.

\begin{lemma}[postponement of $\maltese$-actions]
\label{lemma:CanonicalScheduling}
Every \kl[glueable]{\gluable} set of $\DiLL_0$ quasi-proof-structures is \kl[canonically glueable]{canonically \gluable}.
\end{lemma}

\begin{proof}
Immediate consequence of the following fact: if $\Pi_{1}, \Pi_2, \Pi_3$ are sets of $\DiLL_0$ quasi-proof-structures such that $\Pi_{1}\pnrewrite[\!a_1]\Pi_{2}$ is a $\maltese$-action and $\Pi_{2}\pnrewrite[\!a_2]\Pi_{3}$ is not a $\maltese$-action for some elementary schedulings $a_1, a_2$, then there are elementary schedulings $c_1,c_2$ and a set $\Sigma$ of $\DiLL_0$ quasi-proof-structures such that $\Pi_{1}\pnrewrite[\!c_1] \Sigma$ is not a $\maltese$-action and $\Sigma \pnrewrite[\!c_2]\Pi_{3}$ is a $\maltese$-action.
Notice that $c_1$ (\resp $c_2$) is ``essentially'' the same as $a_2$ (\resp $a_1$).
\end{proof}

We have defined nullary $\Contr$-splitting actions on \MELL quasi-proof-structures in \Cref{sect:rules}. This notion can be easily extended to $\DiLL_0$.
Let $\Pi$ be a set of $\DiLL_0$ quasi-proof-structures.
Given an elementary scheduling $a$, $\Pi \pnrewrite[a] \Pi'$ is \intro[dill0 nullary splitting]{nullary $\Contr$-splitting} if $a =
\Contr_i$ and, for every $\rho \in \Pi$, it splits the $\wn$-\kl{cell} of $\rho$ with output $i$ and $h_\rho \geqslant 0$ inputs into two $\wn$-cells, one $\wn$-cell with output $i$ (\resp $i+1$) and $h_\rho$ inputs, the other $\wn$-cell with output $i+1$ (\resp $i$) and $0$ inputs.
Given a scheduling $\sched$ such that $\Pi\pnrewrite[\sched]\Pi'$, \intro[number of nullary splittings]{$\Contr^{0}(\Pi \pnrewrite[\sched] \Pi')$} is the number of nullary $\Contr$-splitting actions in $\Pi\pnrewrite[\sched]\Pi'$, that is, the number of elementary schedulings $a = \Contr_i$ such that $\Pi \pnrewrite[\sched] \Pi' = \Pi \pnrewrite[\sched_{1}] \Pi_{1} \pnrewrite[a] \Pi_{2} \pnrewrite[\sched_{2}] \Pi'$ and $\Pi_{1} \pnrewrite[a]\Pi_{2}$ is nullary $\Contr$-splitting.
We say that:
\begin{itemize}
\item $\Pi\pnrewrite[\sched]\Pi'$ is \emph{without nullary $\Contr$-splittings} if $\Contr^{0}(\Pi \pnrewrite[\sched] \Pi') = 0$; \emph{has nullary $\Contr$-splittings} otherwise;
\item $\Pi$ is \emph{canonically \gluable without nullary $\Contr$-splittings} if there is a scheduling $\sched$ such that $\Pi \pnrewrite[\sched] \{\emptynets\}$ is canonical and without nullary $\Contr$-splittings.
\end{itemize}

For instance, in Example \ref{ex:church}, $\{\pi\} \pnrewrite[\Contr_2] \{\pi'\}$ is nullary $\Contr$-splitting.
And $\{\sigma_1, \sigma_2\} \pnrewrite[\Contr_2] \Sigma$ is nullary $\Contr$-splitting if $\Sigma = \{\sigma_1', \sigma_2'\}$, but it is not nullary $\Contr$-splitting if $\Sigma = \{\sigma_1', \sigma_2''\}$, where $\sigma_1, \sigma_2, \sigma_1', \sigma_2', \sigma_2''$ are the $\DiLL_0$ proof-structures below.
\begin{center}
\qquad\qquad\qquad\quad
\sigma_2
\qquad\qquad\qquad\quad\ \
\sigma_1'
\qquad\qquad\qquad\quad\
\sigma_2'
\qquad\qquad\qquad\quad
\sigma_2''$

\vspace{\beforepn}
\scalebox{0.8}{
\pnet{
\pnformulae{~\pnf[na]{$X$}~\pnf[ba]{$X^{\bot}$}
\\
\pnf[ba']{$\oc X^{\!\bot}\,$}
\pncown{ba'}
\pnaxiom{na,ba}
\pnbag{}{ba}[bba]{$\,\oc X^{\bot}$}
\pnexp{}{na}{$\wn X $}[1]
\qquad
\scalebox{0.8}{
\pnet{
\pnformulae{
\pnf[ba']{$X^{\!\bot}\,$}~\pnf[na]{$X$}
\\
~~\pnf[ba]{$\oc X^{\bot}$}
\pncown{ba}
\pnaxiom{na,ba'}
\pnbag{}{ba'}[bba']{$\,\oc X^{\bot}$}
\pnexp{}{na}{$\wn X $}[1]
\qquad
\scalebox{0.8}{
\pnet{
\pnformulae{~~\pnf[na]{$X$}~\pnf[ba]{$X^{\bot}$}
\\
\pnf[ba']{$\oc X^{\!\bot}$}~\pnf[na']{$\wn X$}
\pnwn{na'}
\pncown{ba'}
\pnaxiom{na,ba}
\pnbag{}{ba}[bba]{$\,\oc X^{\bot}$}
\pnexp{}{na}{$\wn X $}[1]
\qquad
\scalebox{0.8}{
\pnet{
\pnformulae{
\pnf[ba']{$X^{\!\bot}$}~~\pnf[na']{$X$}
\\
~\pnf[na]{$\wn X$}~~\pnf[ba]{$\oc X^{\bot}$}
\pnwn{na}
\pncown{ba}
\pnaxiom{na',ba'}
\pnbag{}{ba'}[bba']{$\,\oc X^{\bot}$}
\pnexp{}{na'}{$\wn X $}[1]
\qquad
\scalebox{0.8}{
\pnet{
\pnformulae{
\pnf[ba']{$X^{\!\bot}$}~\pnf[na']{$X$}
\\
~~\pnf[na]{$\wn X$}~\pnf[ba]{$\oc X^{\bot}$}
\pnwn{na}
\pncown{ba}
\pnaxiom{na',ba'}
\pnbag{}{ba'}[bba']{$\,\oc X^{\bot}$}
\pnexp{}{na'}{$\wn X $}[1]
\end{center}

\begin{remark}[need for nullary splitting]
\label{rmk:nullary-splitting}
For $\pi_h$ ($h > 0$) as in \Cref{note:church} on p.~\pageref{note:church}, one has $\{\pi_1,\pi_2\} \allowbreak \pnrewrite[\sched] \allowbreak\{\emptynets\}$ only with schedulings $\sched$ whose action on $\{\pi_1\}$ has nullary $\Contr$-splittings.
So, nullary $\Contr$-splittings are somehow ``necessary'' in $\DiLL_0$, differently from \MELL where they are superfluous for normalization (Proposition \ref{prop:unwinding-to-empty}).
To make diagram \eqref{eq:naturality-square} commute for naturality (\Cref{thm:projection-natural}), nullary $\Contr$-splitting actions in $\DiLL_0$ must be mimicked by nullary $\Contr$-splitting actions on \MELL, hence the action of $\Contr_{i}$ in \MELL must allow nullary $\Contr$-splittings.
\end{remark}

Akin to \MELL, nullary $\Contr$-splitting actions in $\DiLL_0$ are superfluous as means of destruction.
They may be needed for \emph{some} elements in a set $\Pi$ of $\DiLL_0$ quasi-proof-structures, but not for \emph{all} of them, thus nullary $\Contr$-splitting actions are useless for the set $\Pi$ as a whole.

\begin{lemma}[splitting in $\DiLL_0$]
\label{lemma:NoContrCanonicalScheduling}
Every \kl[canonically glueable]{canonically \gluable} set $\Pi$ of $\DiLL_0$ quasi-proof-structures is
canonically \gluable \kl[dill0 nullary splitting]{without nullary $\Contr$-splittings}.
\end{lemma}

\begin{proof}
By Remark \ref{rmk:full}, it suffices to prove that for every canonically \gluable set $\Pi$ of $\DiLL_0$ quasi-proof-structures, there is a scheduling $\sched$ such that $\Pi\pnrewrite[\sched]\Pi'$ is a $\lnot\maltese$-action without $\Contr$-splittings, for some \kl[full]{$\maltese$-full} $\Pi'$.
Indeed, by Lemma \ref{lemma:action-daimons}, there is a scheduling $\schedtwo$ such that $\Pi' \pnrewrite[\schedtwo] \{\emptynets\}$, it is a \kl[daimon action]{$\maltese$-action} by Remark \ref{rmk:full} and is clearly without nullary $\Contr$-splittings.

Given a $\lnot\maltese$-action $\Pi\pnrewrite[\sched]\Pi'$ where $\Pi'$ is $\maltese$-full, we prove by induction on $\kl[number of nullary splittings]{\Contr^{0}(\Pi \pnrewrite[\sched] \Pi')} \in \Nat$ that it is possible to build a $\neg\maltese$-action $\Pi\pnrewrite[\sched']\Pi''$ without nullary $\Contr^{0}$-splittings for some $\maltese$-full $\Pi''$.
Clearly, it is enough to show that if $\kl[number of nullary splittings]{\Contr^{0}(\Pi \pnrewrite[\sched] \Pi')} > 0$ then we can find a $\maltese$-full $\Pi''$ and a $\neg\maltese$-action $\Pi\pnrewrite[\sched']\Pi''$ such that $\Contr^{0}(\Pi \pnrewrite[\sched] \Pi') > \Contr^{0}(\Pi \pnrewrite[\sched'] \Pi'')$.

Let $\Pi \pnrewrite[\sched]\Pi' = \Pi \pnrewrite[\sched_{1}] \Pi_{1} \pnrewrite[a]\Pi_{2} \pnrewrite[\sched_{2}]\Pi'$ be a $\neg\maltese$-action, where $\Pi'$ is $\maltese$-full, $a = \Contr_{k}$ and $\Pi_{1} \pnrewrite[a]\Pi_{2}$ is nullary $\Contr$-splitting.
Since the $\wn$-\kl{cells} with $0$ inputs of $\Pi_{2}$ created by $\Pi_1 \pnrewrite[a] \Pi_2$ must disappear in $\Pi'$ (which contains only $\maltese$-cells), there are only two cases for $\Pi_{2} \pnrewrite[\sched_{2}] \Pi'$:
\begin{enumerate}
\item\label{item:1NoContrCanonicalScheduling}
either $\Pi_{2}\pnrewrite[\sched_{2}]\Pi' = \Pi_{2} \pnrewrite[\sched_{21}] \Pi_{3} \pnrewrite[\Weak_i] \Pi_{4} \pnrewrite[\sched_{22}] \Pi'\!$, where $\Pi_{3} \pnrewrite[\Weak_i] \Pi_{4}$ erases the $\wn$-cells without inputs and their unique output (a conclusion of each element of $\Pi_3$) created by $\Pi_{1} \pnrewrite[a]\Pi_{2}$;

\item\label{item:2NoContrCanonicalScheduling}
or $\Pi_{2} \pnrewrite[\sched_{2}] \Pi' = \Pi_{2} \pnrewrite[\sched_{21}] \Pi_{3} \pnrewrite[\!\BoxR_{i}]\Pi_{4} \pnrewrite[\sched_{22}]\Pi'$, where the component of every element of $\Pi_{3}$ containing the $\wn$-cell without inputs created by $\Pi_{1} \pnrewrite[a]\Pi_{2}$ is transformed by $\Pi_{3} \pnrewrite[\!\BoxR_{i}]\Pi_{4}$ into a $\maltese$-cell, according to the rewrite rule in \Cref{fig:empty-box} applied to all the elements of $\Pi_{3}$.
\end{enumerate}

In Case~\ref{item:1NoContrCanonicalScheduling}, just erase the actions $\pnrewrite[a]$ and $\pnrewrite[\Weak_i]$ from $\Pi \pnrewrite[\sched] \Pi'$: let $\Pi\pnrewrite[\sched'] \Pi' = \Pi \pnrewrite[\sched_{1}] \allowbreak\Pi_{1} \allowbreak\pnrewrite[\schedtwo_{21}] \allowbreak \Pi_{4} \allowbreak\pnrewrite[\sched_{22}] \Pi'$, where $\Pi_{1} \pnrewrite[\schedtwo_{21}] \Pi_{4}$ is (essentially) the same as $\Pi_2 \pnrewrite[\sched_{21}] \Pi_3$ except that the name of the conclusions on which the elementary actions apply have changed (since the action $\Pi_1 \pnrewrite[a] \Pi_2$ is no more present).
Clearly, $\Pi \pnrewrite[\sched'] \Pi'$ is a $\neg\maltese$-action and  $\Contr^{0}(\Pi \pnrewrite[\sched] \Pi') > \Contr^{0}(\Pi \pnrewrite[\sched'] \Pi')$.

In Case~\ref{item:2NoContrCanonicalScheduling}, erase the action $\pnrewrite[a]$ and slightly modify the action $\pnrewrite[\BoxR_{i}]$: indeed, let $\Pi\pnrewrite[\sched']\Pi'' = \Pi \pnrewrite[\sched_{1}] \Pi_{1} \pnrewrite[\schedtwo_{21}] \Pi'_{3} \pnrewrite[\BoxR_{i\!-\!1}] \Pi'_{4} \pnrewrite[\schedtwo_{22}] \Pi''$, where
\begin{itemize}
\item
$\Pi_{1} \pnrewrite[\schedtwo_{21}] \Pi'_{3}$ is the same as $\Pi_2 \pnrewrite[\sched_{21}] \Pi_3$ except that the name of the conclusions on which the elementary actions apply have changed (since the action $\Pi_1 \pnrewrite[a] \Pi_2$ is no more present);

\item	the set $\Pi'_{3}$ is $\Pi_{3}$ with one conclusion and one $\wn$-cell with $0$ inputs less in each of its elements;

\item	the action $\Pi'_{3} \pnrewrite[\BoxR_{i\!-\!1}] \Pi'_{4}$ applies the rewrite rule in Figure~\ref{fig:empty-box} to the conclusion $i-1$ of every element in $\Pi'_{3}$, which corresponds to the conclusion $i$ of every element in $\Pi_{3}$;

\item	the $\maltese$-cell of each element in $\Pi'_{4}$ created by $\Pi'_{3} \pnrewrite[\BoxR_{i\!-\!1}] \Pi'_{4}$ has one output less than the $\maltese$-cell of each element in $\Pi_{4}$ created by $\Pi_{3} \pnrewrite[\BoxR_{i}] \Pi_{4}$;
the action $\Pi'_{4} \pnrewrite[\schedtwo_{22}] \Pi''$ and the set $\Pi''$ are obtained from $\Pi_{4} \pnrewrite[\sched_{22}] \Pi'$ and $\Pi'$ accordingly (in particular $\Pi''$ is $\maltese$-full).
\end{itemize}
Clearly, even in Case~\ref{item:2NoContrCanonicalScheduling}, $\Pi \pnrewrite[\sched'] \Pi''$ is a $\neg\maltese$-action and  $\Contr^{0}(\Pi \pnrewrite[\sched] \Pi') > \Contr^{0}(\Pi \pnrewrite[\sched'] \Pi'')$.
\end{proof}

By Lemmas \ref{lemma:CanonicalScheduling} and \ref{lemma:NoContrCanonicalScheduling}, a set $\Pi$ of $\DiLL_0$ quasi-proof-structures is \gluable if and only if it is canonically \gluable without nullary $\Contr$-splittings.
This restricts the search space for rewritings to decide if $\Pi$ is \gluable, making \gluability a  \emph{decidable} problem in the finite case.

\begin{proposition}[decidability of finite \gluability]
\label{prop:decisionFiniteDai}
The problem below is decidable.

\begin{description}
\item[Data] a finite set $\Pi$ of $\DiLL_0$ quasi-proof-structures;
\item[Question] is $\Pi$ \gluable?
\end{description}
\end{proposition}

\begin{proof}
We first define some notions that will be used in the proof.
Akin to the size of a \MELL quasi-proof-structure used in the proof of Proposition~\ref{prop:unwinding-to-empty}, the \emph{size} $\Size{\Pi}$ of a finite set $\Pi$ of $\DiLL_0$ quasi-proof-structures is the quadruple $(p,q,r,s)$~where:
\begin{itemize}
\item $p$ is the finite multiset of the number of inputs of each $\wn$-cell with at least one input in each element of $\Pi$ (hence, $p$ is a finite multiset of positive integers);
\item $q$ is the number of cells in $\Pi$ different from $\wn$-cells without inputs and from $\maltese$-cells;
\item $r$ is the finite multiset $[k_1, \dots, k_n]$ where $n$ is the number of conclusions in each element of $\Pi$ and, for all $1 \leqslant i \leqslant n$, $k_i$ is the number of $\rho \in \Pi$ whose conclusion $i$ is the output of a $\wn$-cell with at least one input;
\item $s$ is the finite multiset of the number of \kl{conclusions} of each \kl{component} of each element~of~$\Pi$.
\end{itemize}
Finite multisets are well-ordered as usual, quadruples are well-ordered lexicographically.

We say that a non-$\maltese$-full set $\Pi$ of $\DiLL_0$ quasi-proof-structures \emph{safely rewrites to} $\Pi'$ if $\Pi \pnrewrite[\sched] \Sigma \pnrewrite[a] \Pi'$ for some set $\Sigma$, some scheduling $\sched$ only made of an arbitrary number (possibly $0$) of $\Ex_{i}$ such that $\Pi \pnrewrite[\sched] \Sigma$ is a $\lnot\maltese$-action, and some elementary scheduling $a \neq \Ex_{i}$ such that $\Sigma \pnrewrite[a] \Pi'$ is neither a $\maltese$-action nor \kl[dill0 nullary splitting]{nullary $\Contr$-splitting}.

For every finite set $\Pi$ of $\DiLL_0$ quasi-proof-structures, exactly one of the following holds:
\begin{enumerate}
\item\label{item:One} either $\Pi$ is $\maltese$-full (this includes the case $\Pi = \{\emptynets\}$) and then it is \gluable by Lemma \ref{lemma:action-daimons};

\item\label{item:Two} or $\Pi$ is not $\maltese$-full, and every scheduling $\sched$ such that $\Pi \pnrewrite[\sched] \Pi'$ is a $\lnot\maltese$-action for some $\Pi'$ is only made of an arbitrary number\,---\,possibly $0$\,---\,of $\Ex_{i}$ (this includes the case when no elementary scheduling applies to $\Pi$, in particular when two elements of $\Pi$ have different types);
then, by definition, $\Pi$ is \gluable if $\Pi = \emptyset$, and it is not \gluable otherwise;

\item\label{item:Three}
or $\Pi$ is not $\maltese$-full, and there are $h > 0$ sets $\Pi_{1}, \dots, \Pi_h$ such that $\Pi$ safely rewrites to $\Pi_j$ for all $1 \leqslant j \leqslant h$, and if $\Pi$ safely rewrites to $\Pi'$ then $\Pi' = \Pi_{j}$ for some $1 \leqslant j \leqslant h$;
then, $\Pi$ is canonically \gluable without nullary $\Contr$-splittings (which is equivalent to be \gluable, by Lemmas \ref{lemma:CanonicalScheduling} and \ref{lemma:NoContrCanonicalScheduling}) if and only if so is at least one among $\Pi_1, \dots, \Pi_{h}$.
\end{enumerate}

Let us prove that when neither Case~\ref{item:One} nor Case~\ref{item:Two} holds, we are in Case \ref{item:Three}.
If neither Case~\ref{item:One} nor Case~\ref{item:Two} holds, $\Pi$ is not $\maltese$-full and $\Pi \pnrewrite[\sched] \Sigma \pnrewrite[a] \Pi'$ for some sets $\Sigma, \Pi'$, some scheduling $\sched$ only made of $\Ex_{i}$ such that $\Pi \pnrewrite[\sched] \Sigma$ is a $\lnot\maltese$-action, and some elementary scheduling $a \neq \Ex_{i}$ such that $\Sigma \pnrewrite[a] \Pi'$ is not a $\maltese$-action.
If $a = \Contr_{i}$ and $\Sigma \pnrewrite[a] \Pi'$ is nullary $\Contr$-splitting, then $i$ is the output of a $\wn$-cell in every element of $\Sigma$, and so there is a set $\Pi''$ such that  $\Sigma \pnrewrite[c] \Pi''$ is neither a $\maltese$-action nor nullary $\Contr$-splitting,  with $c \in \{\Contr_{i}, \Weak_i,\Der_i\}$ (if $c = \Contr_{i}$, $\Sigma \pnrewrite[c] \Pi''$ just splits the inputs of the $\wn$-cell with output $i$ in some element of $\Sigma$ in a way different from $\Sigma \pnrewrite[a] \Pi'$).
Therefore, $\Pi$ safely rewrites to a finite set of $\DiLL_0$ quasi-proof-structures.
Clearly, it is impossible that $\Pi$ safely rewrites to infinitely many sets, since each element of $\Pi$ has a finite number of conclusions.
Hence, Case \ref{item:Three} holds.

The \emph{nondeterministic} procedure to decide if a finite set $\Pi$ of $\DiLL_0$ quasi-proof-structures is \gluable consists of repeating the step described in Case \ref{item:Three},  until all the sets $\Pi_1, \dots, \Pi_n$ which $\Pi$ rewrites to are of the form described in Case \ref{item:One} or \ref{item:Two}: $\Pi$ is \gluable if and only if so is at least one among $\Pi_1, \dots, \Pi_n$.
The procedure terminates because (recall the size above):
\begin{itemize}
\item if $\Pi \pnrewrite[\Ex_{i}] \Pi'$ then $\Size{\Pi} = \Size{\Pi'}$ but infinite chains of $\Ex_{i}$ are irrelevant (see \Cref{note:exc-schedule});
\item if $\Pi$ safely rewrites to $\Pi'$ then $\Size{\Pi} > \Size{\Pi'}$ (according to the lexicographic order).
\qedhere
\end{itemize}
\end{proof}

The size used in the proof of Proposition \ref{prop:decisionFiniteDai} is well defined only if the set $\Pi$ of $\DiLL_0$ quasi-proof-structures is finite.
The \emph{finiteness} hypothesis in deciding \gluability of $\Pi$ is necessary, as we have seen in Remark \ref{rmk:infinite}: the infinite in depth $\Pi$ shown there is not \gluable and there are infinite rewritings from $\Pi$ that are canonical and without nullary $\Contr$-splittings.

\begin{theorem}[decidability]
\label{thm:decisionFinite}
The finite inverse Taylor expansion problem is decidable.
\end{theorem}

\begin{proof}
Let $\Pi$ be a finite set of $\DiLL_0$ proof-structures without $\maltese$-cells.
By Proposition~\ref{prop:decisionFiniteDai}, we can decide if $\Pi$ is \gluable.
By \Cref{thm:characterization}, since there is no $\maltese$-cell in $\Pi$, this is equivalent to deciding if $\Pi \subseteq \Taylor{R}$ for some \MELL proof-structure $R$.
\end{proof}

The nondeterministic procedure to decide the finite inverse Taylor expansion problem is given by the proof of decidability of finite \gluability (Proposition \ref{prop:decisionFiniteDai}) and is \emph{constructive}: if a finite set of $\DiLL_0$ proof-structures without $\maltese$-cells is included in the Taylor expansion $\Taylor{R}$ of some \MELL proof-structure $R$, our procedure allows us to construct one of these $R$.

% !TEX root = mainFinal.tex
\section{Non-atomic axioms}
\label{sect:nonatomic}

Our (quasi-)proof-structures (Definitions \ref{def:proof-structure} and \ref{def:quasi-proof-structure}, \Cref{fig:resource-cells}) deal with \emph{atomic axioms} only: the two outputs of any $\Ax$-cell are \kl{dual} atomic formulas.
We can relax the definitions and allow also the presence of \emph{non-atomic axioms}: the outputs of any $\ax$-cell are typed by \kl{dual} \MELL formulas, not necessarily atomic.
We can extend our results to this more general setting, with some technical complications.
The only trouble is with \emph{exponential axioms}, where the outputs of an $\ax$-cell are typed by \MELL formulas of the form $\oc A^\bot, \wn A$.
Indeed, consider the daimons $\sigma$ and $\sigma'$ and the $\MELL$ proof-structure $S'$ below.
\vspace{\beforepn}
\begin{center}
$\sigma = $
\scalebox{0.8}{
\pnet{
\pnformulae{
\pnf[!A1]{$\oc A^{\bot}$}~\pnf[!A2]{$\oc A^{\bot}$}~\pnf[?A]{$\wn A$}
\pndaimon[d]{!A1,!A2,?A}[1][.2]
\qquad
$\sigma' = $
\scalebox{0.8}{
\pnet{
\pnformulae{
\pnf[!A1]{$\oc A^{\bot}$}~\pnf[!A2]{$\oc A^{\bot}$}~\pnf[?A1]{$\wn A$}~\pnf[?A2]{$\wn A$}
\pndaimon[d]{!A1,!A2,?A1,?A2}
\qquad
$S' = $
\scalebox{0.8}{
\pnet{
\pnformulae{
\pnf[!A1]{$\oc A^{\bot}$}~\pnf[!A2]{$\oc A^{\bot}$}~\pnf[?A1]{$\wn A$}~\pnf[?A2]{$\wn A$}
\pnaxiom{!A1,?A2}[1.5]
\pnaxiom{!A2,?A1}
\end{center}
We have that $\{\sigma\} \pnrewrite[\Contr_3] \{\sigma'\} \subseteq \FatTaylor{S'}$.
But no elementary scheduling $\Contr_3$ can be applied backwards to $S'$ (because of the lack of a $\wn$-cell), which \emph{breaks naturality} (Theorem \ref{thm:projection-natural}).
This is actually due to the fact that, with exponential axioms, co-functionality (Lemma \ref{prop:unwinding-co-functional}) fails for the
rewrite rule $\pnrewrite[\Contr_i]$: read from right to left, $\pnrewrite[\Contr_i]$ is a functional but not total relation.

The solution we propose here
to deal with non-atomic axioms asks for a technical refinement of only few notions,
the rest is unchanged and goes smoothly.
The definitions of \kl{module}, \kl{proof-structure} and \kl{quasi-proof-structure} (Definitions \ref{def:proof-structure} and \ref{def:quasi-proof-structure}) change~as~follows.
\begin{enumerate}
\item In \kl{modules}, non-atomic axioms are allowed, except the exponential ones.
We add a new type of cells, the $\ocax$-cells, with no inputs and two outputs of type $\oc A^\bot$ and $A$.
\item\label{p:no-bangaxiom-alone} In \kl{proof-structures} (and hence in \kl{quasi-proof-structures}), we require that, for every $\ocax$-cell whose outputs have type $\oc A^\bot$ and $A$, the output $o$ of type $A$ is an input of a $\wn$-cell (more precisely, $o$ is an \kl{half} of an \kl{edge} whose other half is the input of a $\wn$-cell).
\end{enumerate}

\noindent
The requirement ``\kl{atomic}'' in the \kl{elementary scheduling} $\Ax_i$ in \Cref{fig:elementary-schedulings} is replaced by ``non-\kl{exponential}'', and we add the new \kl{elementary scheduling} $\OcAx_i$ below to the list in \Cref{fig:elementary-schedulings},
\begin{center}
\small
$(\Gamma_1; \cdots ; \Gamma_{k\!-\!1}; \FlagType(i), \FlagType(i\!+\!1); \Gamma_{k\!+\!1}; \cdots; \Gamma_n)
\xrightarrow{\!\OcAx_{i}\!}
(\Gamma_1; \cdots ; \Gamma_{k\!-\!1}; \emptylist; \Gamma_{k\!+\!1} ; \cdots; \Gamma_n)$  if $\FlagType(i) = \wn A = \FlagType(i\!+\!1)^\bot$
\end{center}
whose \kl[action of elementary scheduling]{action}---also in its daimoned version---is like the hypothesis in \Cref{fig:hypothesis,fig:hypothesis-daimon}:

\vspace{-2\baselineskip}
\begin{center}
\scalebox{0.8}{
\pnet{
\pnformulae{
\pnf[i']{$A$}
\\
\pnexp{}{i'}[i]{$i$}
\pnaxiombang[ax]{i',j}
\pnsemibox{ax,i',j}
\ $\pnrewrite[\OcAx_{i}]$ \
\pnet{
\pnformulae{
\pnfsmall[empty]{}
\pnsemibox{empty}
\qquad\qquad\qquad
\pnet{
\pnformulae{
\pnf[i]{$i$}~\pnf[j]{$i\!+\!1$}
\pndaimon[ax]{i,j}
\pnsemibox{ax,i,j}
\ $\pnrewrite[\OcAx_{i}]$ \
\pnet{
\pnformulae{
\pnfsmall[empty]{}
\pnsemibox{empty}
\bigg\}$
\end{center}

The way the \kl[action of elementary scheduling]{action of an elementary scheduling} is defined (Definitions \ref{def:unwinding} and \ref{def:paths-on-polyadic}) automatically rules out the possibility that a quasi-proof-structure rewrites to a \kl{module} that is not a quasi-proof-structure.
For instance, the elementary scheduling $\Der_1$ does not \kl{apply} to the (\MELL and $\DiLL_0$) proof-structure $Q$ below, because it would yield a module $Q'$ that is not a quasi-proof-structure (see \Cref{p:no-bangaxiom-alone} above).

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

Apart from the changes we mentioned, all definitions and
claims in \Cref{sect:proof-nets,sect:taylor,sect:rules,sec:naturality,sec:glueable,sec:decidability} remain unaffected and valid (just add $\OcAx_{i}$ to the list of elementary schedulings that can apply to $R$ in Lemmas \ref{lem:cell-or-mix} and \ref{lemma:contraction}.\ref{p:cell-or-mix-der}).
The counterexample to naturality shown at the beginning of this section does not apply here,
as $S'$ is not a \MELL quasi-proof-structure (because of its exponential axioms).
In our framework with non-atomic axioms, the only \MELL proof-structures containing $\sigma'$ in their \kl{filled Taylor expansion} are the ones below (up to the order of their conclusions), and the elementary scheduling $\Contr_3$ \kl{applies} backward~to~each~of~them.

\begin{center}
\vspace{\beforepn}
\scalebox{0.8}{
\pnet{
\pnformulae{
\\
\\
\pnf[!A1]{$\oc A^{\bot}\,$}~\pnf[!A2]{$\,\oc A^{\bot}$}
\pnaxiombang{!A1,?A2}[1.8]
\pnaxiombang{!A2,?A1}
\pnexp{}{?A1,?A2}{$\wn A$}
\qquad\qquad\qquad
\pnet{
\pnformulae{
\\
\\
\pnf[!A1]{$\oc A^{\bot}$}
\pnaxiombang{!A1,?A2}[2.2]
\pnaxiom[ax]{!A2,?A1}
\pnexp{}{?A1,?A2}{$\wn A$}[1.1]
\pnbag{}{!A2}{$\oc A^\bot$}[1.1]
\pnbox{ax,!A2,?A1}
\qquad\qquad\qquad
\pnet{
\pnformulae{
\pnf[!A1]{$A^{\bot}$}~~~~~\pnf[?A1]{$A$}
\\\\
\pnaxiom[ax1]{!A1,?A1}
\pnaxiom[ax2]{!A2,?A2}
\pnexp{}{?A1,?A2}{$\wn A$}[1.1]
\pnbag{}{!A2}{$\oc A^\bot$}[1.1]
\pnbag{}{!A1}{$\oc A^\bot$}[2.2]
\pnbox{ax2,!A2,?A2}
\pnbox{ax1,!A1,?A1}
\end{center}

The way we propose here to deal with non-atomic axioms is more elegant and less \textit{ad hoc} than the one we presented in \cite[Section 7]{CSL2020}.
In the latter, we allowed the outputs of a $\maltese$-cell to be inputs of a $\wn$-cell, and we changed the action of the elementary scheduling $\Contr_i$ for $\DiLL_0$ quasi-proof-structures in the daimoned case (\Cref{fig:contraction-daimon}), by explicitly requiring the presence of a $\wn$-cells above the conclusion $i$.
Consequently, in \cite{CSL2020} we had to redefine the filled Taylor expansion in the non-atomic case, and thus to recheck that naturality holds for \emph{all} the rewrite rules.
Here instead we do not have to redefine the filled Taylor expansion and we have to check naturality (\Cref{thm:projection-natural}) in the non-atomic case only for the action~of~$\OcAx_i$.

As another possible solution to deal with non-atomic axioms, instead of using generalized $\wn$-cells in Definition \ref{def:proof-structure} (with an arbitrary number of inputs of type $A$ and one output of type $\wn A$, as in \cite{DanosRegnier95}), we could have used different kinds of $\wn$-cells for dereliction (one input of type $A$, one output of type $\wn A$), contraction (two inputs of type $\wn A$, one output of type $\wn A$), and weakening (no inputs, one output of type $\wn A$), as in \cite{Girard:1987}.
Such a choice should be supported by a rework of the elegant definition of the Taylor expansion of a \MELL proof-structure via the notion of pullback (Definitions \ref{def:proto} and \ref{def:taylor}), since it collapses dereliction, contraction and weakening in a generalized $\wn$-cell.

% !TEX root = mainFinal.tex
\section{Conclusions and perspectives}
\label{sec:conclusions}

\subsubsection*{Daimons for empty boxes}

Our \gluability criterion (\Cref{thm:characterization}) solves the inverse Taylor expansion problem in an ``asymmetric'' way: we characterize the sets of $\DiLL_0$ proof-structures without $\maltese$-cells that are included in the Taylor expansion of some \MELL proof-structure, but in general $\DiLL_0$ proof-structures might contain $\maltese$-cells (while \MELL proof-structures  cannot, see Definition \ref{def:proof-structure}).
\kl{Daimons} and \kl{emptyings} are needed to get a natural transformation
(via the \emph{\kl{filled}} Taylor expansion, \Cref{thm:projection-natural}), which is the main ingredient to prove our \gluability criterion.
But we are interested in frameworks without $\maltese$-cells.
This asymmetry is technically inevitable,
due to the fact that a \gluable set of $\DiLL_0$ proof-structures might not contain any information on the content of some box, when they take 0 copies of~it.

\subsubsection*{Comparison with Pagani and Tasson \cite{PaganiTasson2009}}

Pagani and Tasson's solution \cite{PaganiTasson2009} to the inverse Taylor expansion problem is less
general than ours, because it characterizes \emph{finite} sets of $\DiLL_0$
proof-structures that are included in the Taylor expansion of some
\emph{cut-free} \MELL proof-structure with \emph{atomic axioms}.
We do not have these limitations (finite, cut-free, atomic axioms), our characterization yields a decision procedure (\Cref{thm:decisionFinite}) in the finite case as in \cite{PaganiTasson2009}, and we can smoothly adapt our criterion to the cut-free case (\Cref{thm:characterization}.\ref{p:characterization-cut-free}, which is not trivial as explained in Example \ref{ex:glueable-non-cut-free}).
In \cite{PaganiTasson2009}, the restrictions to cut-free
and to atomic axioms aim to simplify their presentation and might be overcome.
But the restriction to \emph{finite} sets of $\DiLL_0$ proof-structures is somehow essential in their approach.
Roughly, their machinery takes a finite set $\Pi $ of $\DiLL_0$ proof-structures as input,  juxtaposes its elements in a unique graph $\pi$ and then runs a rewriting by means of some tokens that go through the whole $\pi$ and try to merge its components in a $\MELL$ proof-structure whose Taylor expansion includes $\Pi$, if any.
If $\Pi$ were an infinite set, $\pi$ would be an infinite graph and, apart from the technical intricacies of dealing with infinite objects, it would be impossible
to provide a characterization in that case.
In particular, their approach could not distinguish whether $\Pi$ is infinite in width (which can be in the Taylor expansion of some \MELL proof-structure) or infinite in depth (which cannot, see Remark \ref{rmk:infinite}).
Our approach, instead, defines a rewrite relation on a single---finite---element of $\Pi$ and extends it to the whole (possibly infinite) $\Pi$ by requiring that the same rewrite rule applies to each element of $\Pi$ (Definition \ref{def:paths-on-polyadic}).
Thus, we can accommodate the case where $\Pi$ is infinite.

We believe that our rewriting rules are also simpler than the ones in
\cite{PaganiTasson2009} and rely on a more abstract and less \textit{ad hoc}
property (naturality), that allows us to prove also semi-decidability of
another problem: \emph{type inhabitation} for cut-free \MELL proof-structures.

Finally, Pagani and Tasson's solution of the inverse Taylor expansion problem is affected by another limitation, even though not particularly emphasized in \cite{PaganiTasson2009}:
their Theorem 2 (analogous to the ``only if'' part of our \Cref{thm:characterization}) assumes not only that their rewriting starting from a set of $\DiLL_0$ proof-structures terminates
but also that it ends on a \MELL proof-structure, according to their definition of \MELL proof-structure.
This is limiting when in the set of $\DiLL_0$ proof-structures there is no information about the content of a box.
For instance, consider the singletons $\Pi$ and $\Pi'$ of $\DiLL_0$ proof-structures below.
\begin{center}
\vspace{\beforepn}
\small
$\Pi = \bigg\{
\scalebox{0.8}{
\pnet{
\pnformulae{\pnf[X]{$\oc \one$}}
\pncown[cown]{X}
\bigg\}$
\qquad\qquad\qquad
$\Pi' = \bigg\{
\scalebox{0.8}{
\pnet{
\pnformulae{\pnf[1]{$\oc X$}}
\pncown[cown]{1}
\bigg\}$
\qquad\qquad\qquad
$R =
\scalebox{0.8}{
\pnet{
\pnformulae{\pnf[1']{$\one$}}
\pnone[1]{1'}
\pnbox{1,1'}
\pnbag{}{1'}{$\oc \one$}[1.2]
\end{center}
Pagani and Tasson's rewrite rules do not distinguish the two singletons, each one is included in the Taylor expansion of cut-free \MELL proof-structures with an ``empty box'', due to the lack of information.
So their notion of \MELL proof-structure is wider and non-standard (because it allows the presence of empty boxes).
On the contrary, our rewrite rules distinguish $\Pi$ and $\Pi'$:
via the action of cut-free schedulings, the former can rewrite to $\{\emptynet\}$ and is included in the Taylor expansion of the \MELL proof-structure $R$ above, the latter cannot rewrite to $\{\emptynet\}$ and is not part of the Taylor expansion of any cut-free \MELL proof-structure.
Summing up, our characterization follows the standard notion of \MELL proof-structures (unlike \cite{PaganiTasson2009}) and is more fine-grained and informative than the one in \cite{PaganiTasson2009}.

\subsubsection*{The \texorpdfstring{\(\lambda\)}{lambda}-calculus, connectedness and coherence}

Our rewriting system and \gluability criterion might help to prove that a binary coherence relation can solve the inverse Taylor expansion problem for \MELL proof-structures fulfilling some geometric property related to connectedness, despite the impossibility for the full \MELL fragment. Such a coherence would extend the coherence criterion for resource $\lambda$-terms. Note that our \gluability criterion is actually an extension of the criterion for resource $\lambda$-terms. Indeed, in the case of the $\lambda$-calculus, there are three rewrite steps, corresponding to abstraction, application and variable (which can be encoded in our rewrite steps), and coherence is defined inductively: if a set of resource
$\lambda$-terms is coherent, then any set of resource $\lambda$-term that rewrites to it is also coherent.

Presented in this way, the main difference between the $\lambda$-calculus and ``connected'' \MELL
(concerning the inverse Taylor expansion problem) would not be because of the rewriting
system, but because the structure of any resource $\lambda$-term uniquely determines the rewriting
path, while for $\DiLL_0$ proof-structures we have to quantify existentially over all possible
paths. This is an unavoidable consequence of the fact that proof-structures do not have a
tree-structure, contrary to $\lambda$-terms.

Moreover, it is possible to match and mix different rewritings.
Indeed, consider three $\DiLL_0$ proof-structures pairwise \gluable:
proving that they are \gluable as a whole amounts to computing a rewriting from the three rewritings witnessing their pairwise \gluability.
Our rewriting system has been designed with that mixing-and-matching operation in mind, in the particular case where the boxes are connected. This is reminiscent of \cite{FSCD2016}, where we also showed that a certain property enjoyed by the \(\lambda\)-calculus can be extended to proof-structures, provided they are connected inside boxes.
We leave it as future work.

\subsubsection*{Functoriality and naturality}

Our functorial point of view on proof-structures might unify many results. Let us
cite two of them.
\begin{itemize}
\item A sequent calculus proof of \(\vdash \Gamma\) can be translated to a
path from the empty sequent to \(\Gamma\).
This could be the starting point for the formulation of a new correctness criterion.
\item The category \(\Scheduling\) can be extended with a higher
structure---transforming it from a category into a 2-category---which allows cut-elimination to
be represented as a 2-arrow. The functors \(\MELLFunctor\) and
\(\PPolyPN\) can also be extended to 2-functors, so as to prove
via naturality that cut-elimination and the Taylor expansion commute.
\end{itemize}

\subsubsection*{Acknowledgments} The authors are grateful to Olivier Laurent, Lionel Vaux and the anonymous reviewers for their insightful comments.

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

\bibliographystyle{alphaurl}
\bibliography{biblio.bib}

\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: