Laboratoire de l'Informatique et du Parallélisme » Linear Arithmetic

\appendix

\begin{center} \large APPENDIX \end{center}

\input{appendix-preliminaries}

\input{appendix-free-cut-elim}

\input{appendix-arithmetic}

\input{appendix-bc}

\input{appendix-bc-convergence}

\input{appendix-wfm}

%

%\section{Some cut-elimination cases}

%We work in a one-sided calculus for full linear logic. When working in the affine setting we simply drop the condition that weakened formulae are $?$-ed.

%

%As well as all usual rules, we have the induction rule:

%\[

%\vlinf{\indr}{(x \notin FV (\Gamma) )}{? \Gamma, A^\perp (0) , A(t)}{? \Gamma , A^\perp (x) , A(s x) }

%\]

%

%We give all the various cut-reduction cases in the following section but first we give a simple cut-elimination argument.

%

%\subsection{A basic (free-)cut elimination argument}

%We give an argument that easily scales to free-cut elimination, i.e.\ in the presence of non-logical rules.

%

%\newcommand{\anarrow}[2]{\overset{#1}{\underset{#2}{\longrightarrow}}}

%\newcommand{\cutredlin}{\mathit{ma}}

%\newcommand{\cutredexp}{exp}

%

%\begin{definition}

%	Let $\anarrow{}{\cutredexp}$ denote the reduction steps concerning exponential cuts, and $\anarrow{}{\cutredlin}$ be the set of cut-reduction steps concerning multiplicative and additive cuts.

%\end{definition}

%

%\newcommand{\rk}{\mathsf{rk}}

%	\renewcommand{\deg}{\mathsf{deg}}

%\begin{definition}

%	[Measures]

%	For a $\anarrow{}{\cutredlin}$-redex $r$, let its \emph{degree} $\deg( r)$ be the number of logical connectives or quantifiers in its cut-formula. For a proof $\pi$, its \emph{degree} $\deg( \pi)$ is the multiset of the degree of its redexes.

%\end{definition}

%

%\begin{proposition}

%If $\pi$ is not $\anarrow{}{\cutredlin}$-normal then there is a derivation $L:\pi \anarrow{*}{\cutredlin} \pi'$ such that $\deg(\pi')< \deg(\pi)$.

%\end{proposition}

%\begin{proof}

%	First let us show the statement in the special case that $\pi$ contains precisely one $\cut$-inference as its final step, by induction on $|\pi|$. Each commutative $\anarrow{}{\cutredlin}$-step results in us being able to apply the inductive hypothesis to smaller proofs,- in the case of $\vlan $ two smaller proofs. Each key $\anarrow{}{\cutredlin}$-case strictly reduces the degree of the proof. Consequently we can eventually transform $\pi$ to a proof $\pi'$ which has possibly several cuts of smaller degree, as required.

%

%	Now to the general case, we simply apply the above procedure to the subproof above a topmost cut in $\pi$.

%\end{proof}

%\begin{corollary}

%	$\anarrow{}{\cutredlin}$ is weakly normalising.

%\end{corollary}

%

%

%\newcommand{\cntdown}{\mathit{cn}}

%\begin{definition}

%	[Lazy contraction]

%	Let $\anarrow{}{\cntdown}$ comprise of the following reduction steps:

%	\begin{enumerate}

%		\item The commuting steps,

%			\[

%			\vlderivation{

%				\vlin{\rho}{}{\Gamma', ?A, }{

%					\vlin{\cntr}{}{\Gamma, ?A}{\vlhy{\Gamma, ? A, ? A}}

%				}

%			}

%			\quad\to \quad

%			\vlderivation{

%				\vlin{\cntr}{}{\Gamma', ?A}{

%					\vlin{\rho}{}{\Gamma', ?A, ?A}{\vlhy{\Gamma, ? A, ? A}}

%				}

%			}

%			\]

%			for each unary rule $\rho$.

%			\item

%			The key steps:

%			\[

%			\begin{array}{rcl}

%			\vlderivation{

%				\vlin{\cntr}{}{\Gamma, ?A}{

%					\vlin{\wk}{}{\Gamma, ?A, ?A}{\vlhy{\Gamma, ?A}}

%				}

%			}

%			\quad &\to & \quad

%			\Gamma, ?A

%%			\]

%%			and

%%			\[

%\\

%\noalign{\smallskip}

%				\vlderivation{

%					\vlin{\wk}{}{\Gamma, ?A, ?A}{

%						\vlin{\cntr}{}{\Gamma, ?A}{\vlhy{\Gamma, ?A, ?A}}

%					}

%				}

%				\quad &\to& \quad

%				\Gamma, ?A, ?A

%							\end{array}

%			\].

%\item The commuting steps,

%\[

%	\vlderivation{

%		\vliin{\rho}{}{\Gamma ,?A}{

%			\vlin{\cntr}{}{\Gamma_1, ?A}{\vlhy{\Gamma_1, ?A, ?A}}

%		}{\vlhy{\Gamma_2}}

%	}

%	\quad \to \quad

%	\vlderivation{

%		\vlin{\cntr}{}{\Gamma, ?A}{

%			\vliin{\rho}{}{\Gamma,?A, ?A}{\vlhy{\Gamma_1, ?A, ?A}}{ \vlhy{\Gamma_2} }

%		}

%	}

%\]

%%\[

%%\begin{array}{rcl}

%%	\vlderivation{

%%		\vliin{\land}{}{\Gamma, \Delta, ?A, B\land C}{

%%			\vlin{\cntr}{}{\Gamma, ?A, B}{\vlhy{\Gamma, ?A, ?A, B}}

%%		}{\vlhy{\Delta, C}}

%%	}

%%	\quad &\to &\quad

%%	\vlderivation{

%%		\vlin{\cntr}{}{\Gamma, \Delta, ?A, B\land C}{

%%			\vliin{\land}{}{\Gamma, \Delta, ?A, ?A, B\land C}{\vlhy{\Gamma, ?A, ?A, B}}{ \vlhy{\Delta, C} }

%%		}

%%	}

%%%	\]

%%%

%%%	\[

%%\\

%%\noalign{\smallskip}

%%	\vlderivation{

%%		\vliin{\cut}{}{\Gamma, \Delta, ?A}{

%%			\vlin{\cntr}{}{\Gamma, ?A, B}{\vlhy{\Gamma, ?A, ?A, B}}

%%		}{\vlhy{\Delta, \lnot{B}}}

%%	}

%%	\quad &\to& \quad

%%	\vlderivation{

%%		\vlin{\cntr}{}{\Gamma, \Delta, ?A}{

%%			\vliin{\cut}{}{\Gamma, \Delta, ?A, ?A}{\vlhy{\Gamma, ?A, ?A, B}}{ \vlhy{\Delta, \lnot{B}} }

%%		}

%%	}

%%\end{array}

%%\]

%for each binary rule $\rho \in \{ \land, \cut \}$.

%\item The commuting step:

%	\[

%	\vlderivation{

%		\vliin{\vlan}{}{\Gamma, ?A, B\vlan C}{

%			\vlin{\cntr}{}{\Gamma, ?A, B}{\vlhy{\Gamma, ?A, ?A, B}}

%		}{\vlhy{\Gamma, ?A, B}}

%	}

%	\quad \to \quad

%	\vlderivation{

%		\vlin{\cntr}{}{\Gamma, ?A, B\vlan C}{

%			\vliin{\vlan}{}{\Gamma, ?A, ?A, B\vlan C}{\vlhy{\Gamma, ?A, ?A, B}}{

%				\vlin{\wk}{}{\Gamma, ?A, ?A, C}{\vlhy{\Gamma, ?A, C}}

%			}

%		}

%	}

%	\]

%	\end{enumerate}

%	For binary rules:

%

%\end{definition}

%\begin{proposition}

%	$\anarrow{}{\cntdown}$ is weakly normalising

%	, modulo $\cntr$-$\cntr$ redexes,

%	and degree-preserving.

%	If $\pi$ is $\anarrow{}{\cutredlin}$-normal and $\pi \downarrow_\cntdown \pi'$, then so is $\pi'$.

%\end{proposition}

%\begin{proof}

%	By induction on the number of redexes in a proof. Start with bottommost redex, by induction on number of inference steps beneath it.

%\end{proof}

%

%\begin{remark}

%	Only weakly normalising since $\cntr$ can commute with $\cntr$, allowing cycles.

%\end{remark}

%

%\begin{proposition}

%	If $\pi$ is $\anarrow{}{\cutredexp}$-reducible but $\anarrow{}{\cutredlin}$- and $\anarrow{}{\cntdown}$-normal then there is a derivation $H:\pi \anarrow{*}{\cutredexp} \pi'$ such that $\deg (\pi')<\deg(\pi)$.

%\end{proposition}

%

%

%

%\subsection{Base cases}

%

%\[

%\vlderivation{

%\vliin{\cut}{}{ \Gamma,a }{ \vlhy{\Gamma,a} }{ \vlin{\id}{}{a,a^\bot}{ \vlhy{} } }

%}

%\quad\to\quad

%\vlderivation{

%\Gamma,a

%}

%\]

%

%\[

%\vlderivation{

%\vliin{\cut}{}{\Gamma}{ \vlin{\bot}{}{ \Gamma,\bot }{ \vlhy{\Gamma} } }{ \vlin{1}{}{1}{ \vlhy{} } }

%}

%\quad\to\quad

%\vlderivation{

%\Gamma

%}

%\]

%

%\[

%\vlderivation{

%\vliin{\cut}{}{ \Gamma,\Delta,\top }{ \vlin{\top}{}{ \Gamma,\top,0 }{ \vlhy{} } }{ \vlhy{\Delta , \top } }

%}

%\quad\to\quad

%\vlinf{\top}{}{ \Gamma,\Delta,\top }{}

%\]

%

%\subsection{Commutative cases}

%These are the cases when the principal formula of a step is not active for the cut-step below.

%

%\begin{enumerate}

%\item The cut-step is immediately preceded by an initial step. Note that only the case for $\top$ applies:

%\[

%\vlderivation{

%\vliin{\cut}{}{\Gamma,\Delta,\top}{

%\vlin{\top}{  }{ \Gamma,\top,A }{ \vlhy{} }

% }{ \vlhy{\Delta,A^\bot } }

%}

%\quad\to\quad

%\vlinf{\top}{}{ \Gamma,\Delta,\top }{}

%\]

%%Notice that this commutation eliminates the cut entirely and preserves the height of all cuts below.

%\item\label{CaseCommOneStep} A cut-step is immediately preceded by a step $\rho$ with exactly one premiss:

%\[

%\vlderivation{

%\vliin{\cut}{}{\Gamma',\Delta}{\vlin{\rho}{}{\Gamma',A}{\vlhy{\Gamma,A}}}{\vlhy{A^\bot , \Delta}}

%}

%\]

%We have three subcases:

%\begin{enumerate}

%\item\label{subcase:unary-commutation-vanilla}

%%$\Delta$ consists of only $?$-ed formulae or

%If $\rho \notin \{! , \indr \}$ then we can simply permute as follows:

%\begin{equation}

%\label{eqn:com-case-unary-simple}

%\vlderivation{

%\vliin{\cut}{}{\Gamma',\Delta}{\vlin{\rho}{}{\Gamma',A}{\vlhy{\Gamma,A}}}{\vlhy{A^\bot , \Delta}}

%}

%\quad \to \quad

%\vlderivation{

%\vlin{\rho}{}{\Gamma',\Delta}{

%\vliin{\cut}{}{\Gamma,\Delta}{\vlhy{\Gamma,A}}{\vlhy{A^\bot , \Delta}}

%}

%}

%\end{equation}

%(If $\rho$ was $\forall$ then we might need to rename some free variables in $\Delta$.)

%\item $\rho $ is a $!$-step. Therefore $\Gamma$ has the form $? \Sigma , B$ and $A$ has the form $?C$, yielding the following situation:

%\[

%\vlderivation{

%\vliin{\cut}{}{? \Sigma, !B, \Delta }{

%\vlin{!}{}{? \Sigma, !B , ?C}{\vlhy{?\Sigma , B , ?C}  }

%}{

%\vlin{\rho'}{}{!C^\perp , \Delta}{\vlhy{\vlvdots}}

%}

%}

%\]

%Now, if $!C^\perp$ is principle for $\rho'$ then $\rho'\in \{! , \indr\}$ and so $\Delta $ must be $?$-ed; in this case we are able to apply the transformation \eqref{eqn:com-case-unary-simple}. Otherwise $A^\perp$ is not principal for $\rho'$ and so $\rho' \notin \{! , \indr \}$, which means we can apply \ref{subcase:unary-commutation-vanilla} along this side of the subproof.

%\item $\rho$ is a $\indr$-step. Therefore $\Gamma$ has the form $? \Sigma , B^\perp(x), B(s x) $ and $A$ has the form $?C$, and the argument is similar to the case above.

%% yielding the following situation:

%%\[

%%\vlderivation{

%%	\vliin{\cut}{}{? \Sigma, B^\perp (0) , B(t), \Delta }{

%%		\vlin{\indr}{}{? \Sigma, B^\perp (0) , B(t) , ?C}{\vlhy{?\Sigma , B^\perp(x) , B(s x) , ?C}  }

%%	}{

%%	\vlin{\rho'}{}{!C^\perp , \Delta}{\vlhy{\vlvdots}}

%%}

%%}

%%\]

%\end{enumerate}

%

%

%

%\item A cut-step is immediately preceded by a $\vlte $-step:

%\[

%\vlderivation{

%\vliin{\cut}{}{\Gamma,\Delta,\Sigma,A\vlte B }{

%\vliin{\vlte}{}{\Gamma,\Delta,A\vlte B,C }{\vlhy{\Gamma,A,C}}{\vlhy{\Delta,B}}

%}{\vlhy{ \Sigma , C^\bot  }}

%}

%\quad\to\quad

%\vlderivation{

%\vliin{\vlte}{}{\Gamma,\Delta,\Sigma,A\vlte B}{

%\vliin{\cut}{}{\Gamma,\Sigma,A}{\vlhy{\Gamma,A,C}}{\vlhy{\Sigma,C^\bot}}

%}{\vlhy{\Delta,B}}

%}

%\]

%%Notice that this commutation might increase the height of any cuts below along the right branch of the indicated cut, but decreases the height along the left branch.

%\item\label{CommCaseAmpersand} A cut-step is immediately preceded by a $\vlan$-step.

%\[

%\vlderivation{

%\vliin{\cut}{}{ \Gamma,\Delta,A\vlan B }{ \vliin{\vlan}{}{\Gamma,A\vlan B,C}{ \vlhy{\Gamma,A,C} }{\vlhy{\Gamma,B,C}}}{ \vlhy{\Delta, C^\bot} }

%}

%\quad\to\quad

%\vlderivation{

%\vliin{\vlan}{}{\Gamma,\Delta,A\vlan B }{

%\vliin{cut}{}{\Gamma,\Delta,A }{ \vlhy{\Gamma,A,C} }{ \vlhy{ \Delta,C^\bot } }

%}{

%\vliin{ \cut }{}{\Gamma,\Delta,B}{ \vlhy{\Gamma,B,C } }{ \vlhy{\Delta,C^\bot} }

%}

%}

%\]

%\item (No rule for cuts commuting with cuts.)

%%A cut-step is immediately preceded by another cut-step:

%\[

%\vlderivation{

%	\vliin{\cut}{}{\Gamma, \Delta, \Sigma}{

%		\vliin{\cut}{}{\Gamma, \Delta, B}{\vlhy{\Gamma, A}}{\vlhy{\Delta, \lnot{A}, B}}

%		}{\vlhy{\Sigma, \lnot{B}}}

%	}

%	\quad\to\quad

%\vlderivation{

%	\vliin{\cut}{}{\Gamma, \Delta, \Sigma}{\vlhy{\Gamma, A}}{

%		\vliin{\cut}{}{\Delta, \Sigma, \lnot{A}}{\vlhy{\Delta, \lnot{A}, B}}{\vlhy{\Sigma, \lnot{B}}}

%		}

%	}

%\]

%\end{enumerate}

%

%

%

%\subsection{Key cases: structural steps}

%%[THIS SECTION MIGHT NOT BE NECESSARY]

%We attempt to permute cuts on exponential formulae over structural steps whose principal formula is active for the cut.

%

%We use the commutative case \ref{CaseCommOneStep} to assume that the topmost cut-step in a sequence has already been permuted up to its origin on the $!$-side.

%

%We have two cases.

%\begin{enumerate}

%\item\label{StructStepCont} The structural step preceding the cut is a weakening:

%\[

%\vlderivation{

%\vliin{\cut}{}{?\Gamma,\Delta}{ \vlin{!}{}{ ?\Gamma,!A }{ \vlhy{?\Gamma , A} } }{ \vlin{w}{}{ ?A^\bot }{ \vlhy{\Delta	} } }

%}

%\quad\to\quad

%\vlinf{w}{}{?\Gamma,\Delta}{ \Delta }

%\]

%%\item The structural step preceding the cut is a contraction:

%%\[

%%\vlderivation{

%%\vliin{\cut}{}{ ?\Gamma,\Delta }{

%% \vlin{!}{}{ ?\Gamma,!A }{ \vlhy{?\Gamma , A} }

%%}{ \vlin{c}{}{ ?A^\bot , \Delta }{ \vlhy{ ?A^\bot , ?A^\bot ,  \Delta} } }

%%}

%%\quad\to\quad

%%\vlderivation{

%%\vliq{c}{}{?\Gamma, \Delta}{

%%\vliin{\cut}{}{?\Gamma, ?\Gamma,\Delta }{

%% \vlin{!}{}{ ?\Gamma,!A }{ \vlhy{?\Gamma , A} }

%%}{

%%\vliin{\cut}{}{?\Gamma,?A^\bot , \Delta }{

%% \vlin{!}{}{ ?\Gamma,!A }{ \vlhy{?\Gamma , A} }

%%}{ \vlhy{?A^\bot , ?A^\bot , \Delta } }

%%}

%%}

%%}

%%\]

%%OR use a multicut:

%%\[

%%\vlderivation{

%%\vliin{\cut}{}{ ?\Gamma,\Delta }{

%% \vlin{!}{}{ ?\Gamma,!A }{ \vlhy{?\Gamma , A} }

%%}{ \vlin{c}{}{ ?A^\bot , \Delta }{ \vlhy{ ?A^\bot , ?A^\bot ,  \Delta} } }

%%}

%%\quad\to\quad

%%\vlderivation{

%%\vliin{\multicut}{}{?\Gamma,?A^\bot , \Delta }{

%% \vlin{!}{}{ ?\Gamma,!A }{ \vlhy{?\Gamma , A} }

%%}{ \vlhy{?A^\bot , ?A^\bot , \Delta } }

%%}

%%\]

%\item The structural step preceding a cut is a contraction:

%\[

%\vlderivation{

%	\vliin{\cut}{}{?\Gamma, \Sigma }{ \vlhy{?\Gamma,!A^\bot} }{

%		\vlin{\cntr}{}{ ?A,\Sigma }{ \vlhy{ ?A,?A,\Sigma } }

%	}

%}

%\quad\to\quad

%\vlderivation{

%	\vliq{\cntr}{}{ ?\Gamma,\Sigma }{

%		\vliin{\cut}{}{ ?\Gamma,?\Gamma,\Sigma }{ \vlhy{?\Gamma,!A^\bot } }{

%			\vliin{\cut}{}{ ?A,?\Gamma,\Sigma }{ \vlhy{?\Gamma,!A^\bot} }{ \vlhy{ ?A,?A,?\Delta,\Sigma } }

%		}

%	}

%}

%\]

%%\item The structural step preceding a cut is a parallel contraction:

%%\[

%%\vlderivation{

%%\vliin{\cut}{}{?\Gamma,?\Delta, \Sigma }{ \vlhy{?\Gamma,!A^\bot} }{

%%\vlin{}{}{ ?A,?\Delta,\Sigma }{ \vlhy{ ?A,?A,?\Delta,?\Delta,\Sigma } }

%%}

%%}

%%\quad\to\quad

%%\vlderivation{

%%\vlin{}{}{ ?\Gamma,?\Delta,\Sigma }{

%%\vliin{\cut}{}{ ?\Gamma,?\Gamma,?\Delta,?\Delta,\Sigma }{ \vlhy{?\Gamma,!A^\bot } }{

%%\vliin{\cut}{}{ ?A,?\Gamma,?\Delta,?\Delta,\Sigma }{ \vlhy{?\Gamma,!A^\bot} }{ \vlhy{ ?A,?A,?\Delta,?\Delta,\Sigma } }

%%}

%%}

%%}

%%\]

%\end{enumerate}

%

%\subsection{Key cases: logical steps}

%Finally, once all cuts have been permuted maximally on both sides, we have the cases when the cut-formula is principal for a preceding logical step on both sides. We have three cases, one for every pair of connectives.

%\begin{enumerate}

%\item The cut-formula is multiplicative:

%\[

%\vlderivation{

%\vliin{\cut}{}{ \Gamma,\Delta,\Sigma }{

%\vliin{\vlte}{}{ \Gamma,\Delta,A\vlte B }{ \vlhy{\Gamma,A} }{ \vlhy{\Delta,B} }

%}{ \vlin{\vlpa}{}{ \Sigma, A^\bot \vlpa B^\bot }{ \vlhy{\Sigma , A^\bot , B^\bot} } }

%}

%\quad\to\quad

%\vlderivation{

%\vliin{\cut}{}{ \Gamma,\Delta,\Sigma }{ \vlhy{\Gamma,A} }{

%\vliin{\cut}{}{ \Delta,\Sigma,A^\bot }{ \vlhy{\Delta,B} }{ \vlhy{\Sigma , A^\bot,B^\bot } }

%}

%}

%\]

%\item The cut-formula is additive,

%\[

%\vlderivation{

%\vliin{\cut}{}{ \Gamma,\Delta }{

%\vliin{\vlan}{}{ \Gamma,A\vlan B }{ \vlhy{\Gamma,A} }{ \vlhy{\Gamma,B} }

% }{ \vlin{\vlor}{}{ \Delta,A^\bot\vlor B^\bot }{ \vlhy{\Delta, A^\bot } } }

%}

%\quad\to\quad

%\vliinf{\cut}{}{ \Gamma,\Delta }{ \Gamma,A }{ \Delta,A^\bot }

%\]

%where the case for the other $\vlor$-rule is symmetric.

%\item The cut-formula is exponential.

%\[

%\vlderivation{

%\vliin{\cut}{}{ ?\Gamma,\Delta }{

% \vlin{!}{}{ ?\Gamma,!A }{ \vlhy{?\Gamma , A} }

%}{

%\vlin{?}{}{ \Delta,?A^\bot }{ \vlhy{\Delta, A^\bot } }

%}

%}

%\quad\to\quad

%\vliinf{\cut}{}{ ?\Gamma,\Delta }{ ?\Gamma,A }{ \Delta,A^\bot }

%\]

%\item The cut-formula is quantified.

%\[

%\vlderivation{

%	\vliin{\cut}{}{\Gamma, \Delta}{

%		\vlin{\forall}{}{\Gamma, \forall x. A(x)}{\vltr{\pi(a)}{\Gamma, A(a)}{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}}

%		}{

%		\vlin{\exists}{}{\Delta, \exists x . \lnot{A}(x)}{\vlhy{\Delta, \lnot{A}(t)}}

%		}

%	}

%	\quad \to \quad

%	\vlderivation{

%		\vliin{\cut}{}{\Gamma, \Delta}{

%			\vltr{\pi(t)}{\Gamma, A(t)}{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}

%			}{\vlhy{\Delta, \lnot{A}(t)}}

%		}

%\]

%\end{enumerate}

%