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

%\section{Conclusions}

\section{Conclusions}

As mentioned in the introduction, our motivation for this work is to conduct a proof-theoretic study of first-order theories in linear logic, in particular to construct theories corresponding to various functional complexity classes.

We proved a general form of `free-cut elimination' that generalises forms occurring in prior works, e.g.\ \cite{LincolnMSS92} \anupam{mention Baelde/Miller?}. Our starting point was an axiomatisation proposed by Bellantoni and Hofmann in \cite{BelHof:02}, adapted to the linear logic setting. We identified a fragment, $\arith$, of the arithmetic that is sound and complete with respect to polynomial-time functions, using the free-cut elimination theorem and witness function method that is common in bounded arithmetic and applicative theories.

% To see if analogues of various results can be useful for the construction of theories corresponding to various complexity classes. In particular we are interested in the following conventions:

%An alternative to \ref{item:crit-implicit-complexity} is the use of, say, bounded quantifiers, as done in bounded arithmetic \cite{Buss86book}.

%

%Regarding \ref{item:crit-ground-type}, almost all approaches 

\subsection{Related work}

From the point of view of constructing theories for complexity classes, the choice of linear logic and witness function method satisfies two particular desiderata:

\begin{enumerate}

\item\label{item:crit-implicit-complexity} Complexity controlled by `implicit' means.

%, e.g.\ modalities or ramification, as in \cite{Leivant94:found-delin-ptime}. 

\item\label{item:crit-ground-type} Extraction of programs using only ground types.

\end{enumerate}

From this point of view, the most relevant related work is that of Cantini \cite{Cantini02}, based on an \emph{applicative theory}, which we recently became aware of. The main difference here is the choice of model of computation: Cantini uses terms of combinatory logic, whereas we use equational specifications (ESs). This choice necessitates a vastly different proof-theoretic treatment. In particular, equality between terms is not decidable in the ES framework, and so there is no apparent constructive interpretation of the right-contraction rule, which usually requires a `test' function. This is why Bellantoni and Hofmann require a double-negation translation into intuitionistic logic and the use functionals at higher types, and why Leivant disregards classical logic altogether in \cite{Leivant94:found-delin-ptime}. Notice that this is precisely why our use of linear logic is important: the control of $?$ occurrences in a proof allows us to sidestep this problem. At the same time we are able to remain in a classical linear setting. We do not think that either model of computation is better, but rather that it is interesting to observe how such a choice affects the proof-theoretic considerations at hand.

Our use of linear logic can, in some sense, be seen as a refinement of Leivant's result in \cite{Leivant94:found-delin-ptime}, where positive existential comprehension in intuitionistic second-order logic is found to correspond to polynomial time. The necessity of intuitionistic logic is since any double-negation translation from classical logic would break the positivity criterion. In this work we have observed that the further restriction to non-modal formulae in nonlogical rules is sufficient to carry out a witnessing argument directly from a classical setting, while remaining complete for polynomial-time functions. \todo{comprehension vs induction. Check this is not bullshit!}

\patrick{hmm, I am not sure I understand how our use of linear logic can be viewed as a refinement of this work.}

Most works on the relationships between linear logic and complexity fit in the approach of the proofs-as-programs correspondence and study variants of linear logic with weak exponential modalities,   e.g.\ bounded linear logic \cite{GirardSS92:bounded-ll}, light linear logic and elementary linear logic \cite{Girard94:lll}. However, Terui considers a na\"ive set theory \cite{Terui04} that is also sound and complete for polynomial time and is based on light linear logic\footnote{He also presents a cut-elimination result but, interestingly, it is entirely complementary to that which we present here: he obtains full cut-elimination since he works in a system without full exponentials and with Comprehension as the only nonlogical axiom. Since the latter admits a cut-reduction step, the former ensures that cut-elimination eventually terminates by a \emph{height-based} argument, contrary to our argument that analyses the \emph{degrees} of cut-formulae.}. His approach relies on functionals at higher type, using light linear logic to type the extracted functionals. Another work using linear logic to characterize  complexity classes by using totality proofs is \cite{Lasson11} but it is tailored for second-order logic.

 The status of first-order theories is more developed for other substructural logics, for instance \emph{relevant logic} [cite?], although we do not know of any works connecting such logics to computational complexity.

%Most works on the relationships between linear logic and complexity concern the construction of \emph{type systems}, e.g.\ bounded linear logic \cite{GirardSS92:bounded-ll}, light linear logic and elementary linear logic \cite{Girard94:lll}, soft linear logic \cite{Lafont04}. However, Terui considers a na\"ive set theory \cite{Terui04} that is also sound and complete for polynomial time and is based on light linear logic. His approach relies on functionals at higher type, using light linear logic to type the extracted functionals.\footnote{He also presents a cut-elimination result but, interestingly, it is entirely complementary to that which we present here: he obtains full cut-elimination since he works in a system without full exponentials and with Comprehension as the only nonlogical axiom. Since the latter admits a cut-reduction step, the former ensures that cut-elimination eventually terminates by a \emph{height-based} argument, contrary to our argument that analyses the \emph{degrees} of cut-formulae.} The status of first-order theories is more developed for other substructural logics, for instance \emph{relevant logic} [cite?], although we do not know of any works connecting such logics to computational complexity.

Concerning the relationship between linear logic and safe recursion, note that an embedding of a variant of safe recursion into light linear logic has been carried studied in \cite{Murawski04}, but this is in the setting of functional computation and is quite different from the present approach. Observe however that a difficulty in this setting  was the non-linear treatment of safe arguments which here we manage by including in our theory a duplication axiom for $W$. 

We have already mentioned the work of Bellantoni and Hofmann \cite{BelHof:02}, which was somewhat the inspiration behind this work. Our logical setting is very similar to theirs, under a certain identification of symbols, but there is a curious disconnect in our use of the additive disjunction for the $\surj$ axiom. They rely on just one variant of disjunction. As we said, they rely on a double-negation translation and thus functionals at higher-type.

\anupam{mention bounded arithmetic?}

%

%Finally, the approach of bounded arithmetic 

%

%In summary, as far we

%

%

%******

%

%

%

%As far as we know no approach to  has combined a basis in linear (or a related) logic with a solely proof theoretic witnessing argument, such as the witness function method. 

%

%

%

%         

%In summary, it is promising that free-cut elimination and the witness function method can be used to extract similar complexity results to those obtained in bounded arithmetic. 

\subsection{Further work}

\todo{finish!}

Say something about minimisation and the polynomial hierarchy. Could be achieved by controlling contraction/additives, since this requires a notion of tests.

As we mentioned in the context section, there are many choices of model of computation when constructing theories. Applicative theories use combinatory algebra and in this work we have used equational specifications. Theories of bounded arithmetic, however, use arithmetic formulae to code computation sequences. The advantage of this is that any closed formula can be evaluated, and so equality is decidable. 

We think the true power of the witness function method lies in an approach such as this, although we 

Polynomial hierarchy? Cite Reinhard/Isobel and their cited works.

\newpage

*******************************************

\todo{words or integers?}

% % % % % % % % % % Bullet points % % % % % % %

Some points, either here or in body of paper:

\begin{itemize}

\item Application of free-cut elimination to witnessing arguments: proof of concept.

\item Examine differences between our arithmetic and Bellantoni and Hofmann: (a) our induction rule, is it equivalent? Maybe not. (b) point about their surjectivity axiom: we do not think it works unless they add another axiom, like Leivant's, for the completeness in the conditional case. We can remark that linear logic solves this problem neatly by use of the additives.

\item Point about contraction on right: this is what free-cut elimination + linear logic adequately restricts. This is a problem for any classical theory that uses equational specifications.

\item Regarding Leivant's intrinsic theories: his result about polynomial-time functions being exactly the provably convergent functions of positive existential induction is necessarily in intuitionistic logic. In classical logic he cannot avoid contraction on the right without the linear logic refinement that we have. \anupam{This can be seen as another contribution of our work?}

\item On the other hand, our completeness argument can be seen as more-or-less what he had in mind, refined to linear logic.

\item Discuss different approaches to arithmetics for complexity/witnessing. Namely:

\begin{itemize}

\item Programs: terms of combinatory logic vs. formulae of arithmetic vs. equational specifications.

\item Convergence: N predicate vs. $\Pi^0_2$ sentence.

\end{itemize}

Remark: use of equational specifications necessitates N predicate. Hence contraction problems present, no problem for first two types of programs since there is a notion of execution (either via a well-typing or by seeing formula as a circuit), and so closed programs can be run and we can conduct equality tests for right-contraction steps.

Remark: another variant in the equational specifications category is when equations are given on lambda-terms, e.g. as in

Marc Lasson. Controlling Program Extraction in Light Logics. TLCA 2011: 123-137

\item We should mention future line of work in bounded-arithmetic style, i.e. using formulas as programs.

\patrick{In particular mention that we conjecture that in this setting induction on Sigma1 formulas (not only positive) would be Ptime sound, if I understand well?}

\item Related works:

\begin{itemize}

 \item Discuss differences with line of work on Curry-Howard style implicit complexity, e.g. light linear logic. Mention work of Murawski to relate safe recursion

 and LLL:

Andrzej S. Murawski, C.-H. Luke Ong:

On an interpretation of safe recursion in light affine logic. Theor. Comput. Sci. 318(1-2): 197-223 (2004)

\item related works on free-cut elimination style results in LL (David Baelde?)

\end{itemize}

\end{itemize}

\medskip

A proposal of organization (Patrick):

\begin{enumerate}

\item Introduction:

  \begin{itemize}

        \item motivate and explain:

                 \begin{itemize}

                      \item free-cut elimination: mention use in bounded arithmetic

                      \item linear logic: say mainly used for structural proof-theory, proofs-as-programs, proof search ?

                      \item free cut-elimination for linear logic

                  \end{itemize}  

          \item application in this paper: arithmetic systems for Ptime computability

                 \begin{itemize}

                   \item present Bellantoni-Hofmann's system and Leivant's ramified theory $RT_0$

                   \item explain their relationships with implicit computational complexity on the one hand, bounded arithmetic on the other. some words about witnessing method in bounded arithmetic

                   \item describe our contribution: re-prove a weak version of Bellantoni-Hofmann, by using the witnessing method.

                 \end{itemize}        

   \end{itemize}

\item Related works section (by the end?):

        \begin{itemize}

             \item about complexity:

               \begin{itemize}

                  \item overview of different approaches to arithmetics for complexity

                  \item technical comparison of our contribution w.r.t. Bellantoni-Hofmann and w.r.t. Leivant

                  \item short comparison with Murawski-Ong's study of safe recursion vs. LLL

                 \end{itemize}

             \item about linear logic:

                \begin{itemize}

                    \item if not done in the introduction, comparison with free-cut elimination like results by Baelde or others

                \end{itemize}

         \end{itemize}

\item Conclusion and future work:

mention something about prenexing if needed.

 future work on bounded arithmetic style

 \end{enumerate}

 \medskip

 *************************************

Comments:

\vspace{2em}

Related works section (by the end?):

        \begin{itemize}

             \item about complexity:

               \begin{itemize}

                  \item overview of different approaches to arithmetics for complexity

                  \item technical comparison of our contribution w.r.t. Bellantoni-Hofmann and w.r.t. Leivant

                  \item short comparison with Murawski-Ong's study of safe recursion vs. LLL

                 \end{itemize}

             \item about linear logic:

                \begin{itemize}

                    \item if not done in the introduction, comparison with free-cut elimination like results by Baelde or others

                \end{itemize}

         \end{itemize}

                  % % % % % % % % % % % % % % % % % % % % % % % %

                  \subsubsection{Parameters}

                  \begin{itemize}

                  \item Programs. Equational specifications vs lambda terms vs formulae.

                  \item Convergence statement. Designated predicate vs $\Pi^0_2$ formula.

                  \item Source of complexity. Bounded quantifiers (induces Cobham limited recursive programs) vs modalities (induces ramified/safe recursive programs).

                  \item Proof method. Realisability/Dialectica (higher types) vs Proof theoretic (ground type).

                  \end{itemize}

                  \subsubsection{Linear logic and complexity}

                  \begin{itemize}

                  \item Mostly type systems, e.g.\ bounded/light/soft/elementary linear logic. (Girard, Girard (?), Lafont, ? resp.)

                  \item Girard/Terui/Grishin naive set theory. Uses realisability.

                  \end{itemize}

                  \subsubsection{Modal systems}

                  Modal systems usually model the notion of ramification from Leivant's intrinsic theories.

                  \subsection{Witnessing argument}

                  Almost all works use a 

                  refinement of Leivant 94.