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

\section{Introduction}

%\anupam{i put all the notes/suggestions at the end, before references.}

  \emph{Free-cut elimination}\footnote{Also known as \emph{anchored} or \emph{directed} completeness, \emph{partial} cut-elimination or \emph{weak} cut-elimination in other works.} is a normalisation procedure on formal proofs in systems including nonlogical rules, e.g.\ the axioms and induction rules in arithmetic, introduced in \cite{Takeuti87}. It yields proofs in a form where, essentially, each cut step has at least one of its cut formulas principal for a nonlogical step. It is an important tool for proving witnessing theorems in first-order theories, and in particular it has been extensively used in \emph{bounded arithmetic} for proving complexity bounds on representable functions, by way of the \textit{witness function method} \cite{Buss86book}.

   Linear logic \cite{Girard87} is a decomposition of both intuitionistic and classical logic, based on a careful analysis of duplication and erasure of formulas. It has been useful in proofs-as-programs correspondences, proof search \cite{Andreoli92} and logic programming \cite{Miller04}. By controlling  structural rules with designated modalities, the \textit{exponentials}, linear logic has allowed for a fine study of complexity bounds in the Curry-Howard interpretation, inducing variants with polynomial-time complexity \cite{GirardSS92:bounded-ll} \cite{Girard98} \cite{Lafont04}.

%   However most of this work has been done for 'purely logical' linear logic, or at least for variants with full cut elimination procedure.

    In this work we explore how the finer granularity of linear logic can be used to control complexity in \emph{first-order theories}, restricting the provably convergent functions rather than the typable terms as in the propositional setting.

%     aim at exploring in which way the complementary techniques of free-cut elimination and linear logic can be combined to analyze properties of first-order theories in which structural rules play a critical r\^ole.

    We believe this to be of general interest, in particular to understand the effect of substructural restrictions on nonlogical rules, e.g.\ induction, in mathematical theories. Some related works exist, e.g.\ the na\"ive set theories of Girard and Terui \cite{Girard94:lll} \cite{Terui04}, but overall it seems that the first-order proof theory of linear logic is still rather undeveloped; in particular, to our knowledge, there seems to be no general form of free-cut elimination available in the literature (although special cases occur in \cite{LincolnMSS92} and \cite{Baelde12}). Thus our first contribution, in Sect.~\ref{sect:free-cut-elim}, is to provide general sufficient conditions on nonlogical rules for a first-order linear logic system to admit free-cut elimination.

    \newcommand{\FP}{\mathbf{FP}}

    We illustrate the usefulness of this result by proving a witnessing theorem for an arithmetic in linear logic, showing that the provably convergent functions are precisely the polynomial-time computable functions (Sects.~\ref{sect:bc-convergence} and \ref{sect:wfm}), henceforth denoted $\FP$. Our starting point is an axiomatisation $\mathcal{A}_2^1$ from \cite{BelHof:02}, based on a modal logic, already known to characterise $\FP$.

%    In this system ,following Leivant \cite{Leivant94:intrinsic-theories} functions are defined by first-order equational specifications.

%    The main result of $\mathcal{A}_2^1$ is then that the provably total functions are exactly the polynomial time class.

    This approach, and that of \cite{Leivant94:found-delin-ptime} before, differs from the bounded arithmetic approach since it does not employ bounds on quantifiers, but rather restricts nonlogical rules by substructural features of the modality \cite{BelHof:02} or by \emph{ramification} of formulas  \cite{Leivant94:intrinsic-theories}. The proof technique employed in both cases is a realisability argument, for which \cite{Leivant94:found-delin-ptime} operates directly in intuitionistic logic, whereas \cite{BelHof:02} obtains a result for a classical logic via a double-negation translation, relying on a higher-type generalisation of \emph{safe recursion}

%     which is applied to an intuitionistic version of the theory. In  \cite{BelHof:02} the target language of the realizability argument is a higher-order language \cite{Hofmann00}, SLR, based on safe recursion

     \cite{BellantoniCook92}.

%     In a second step the result is extended to the classical variant $\mathcal{A}_2^1$ by using the Friedman A translation.

    We show that Buss' witness function method can be employed to extract functions directly for classical systems similar to $\mathcal{A}_2^1$ based in linear logic, by taking advantage of free-cut elimination. The De Morgan normal form available in classical (linear) logic means that the functions we extract remain at ground type, based on the usual safe recursive programs of \cite{BellantoniCook92}. A similar proof method was used by Cantini in \cite{Cantini02}, who uses combinatory terms as the model of computation as opposed to the equational specifications in this work.\footnote{This turns out to be important due to the handling of right-contraction steps in the witnessing argument.}

%    We show that the witness function method can be employed to extract functions directly for classical systems similar to $\mathcal{A}_2^1$ based on linear logic, taking advantage of free-cut elimination. De Morgan normal forms available in classical (linear) logic mean that extracted functions remain at ground type, based on the safe recursive programs of \cite{BellantoniCook92}. A similar proof method was used by Cantini \cite{Cantini02} using combinatory logic as the model of computation as opposed to the equational specifications in this work.\footnote{This turns out to be important due to the handling of right-contraction steps in the witnessing argument.}

     Our result holds for an apparently weaker theory than $\mathcal{A}_2^1$, with induction restricted to positive existential formulas in a way similar to Leivant's $\mathit{RT}_0$ system in \cite{Leivant94:intrinsic-theories} (see also \cite{Marion01}), but the precise relationship between the two logical settings is unclear.

%

%   Our result holds for an apparently weaker theory than $\mathcal{A}_2^1$, with induction restricted to positive existential formulas in a way similar to Leivant's $\mathit{RT}_0$ system in \cite{Leivant94:intrinsic-theories}, but the precise relationship between the two logical settings is unclear.

%    We illustrate in the same time the relationship between  $\mathcal{A}_2^1$ and linear logic, which was hinted but not investigated in the original paper  \cite{BelHof:02}.

We conclude in Sect.~\ref{sect:conclusions} with a survey of related work and some avenues for further applications of the free-cut elimination result.

%More detailed proofs of the various results herein can be found in the appendices, Sects.~\ref{sect:app-preliminaries}-\ref{sect:app-wfm}.

This is a version of the extended abstract \cite{BaiDas} with appendices containing further proof details.

%in the appendices, Sects.~\ref{sect:app-preliminaries}-\ref{sect:app-wfm}.

%Everything else remains the same, with the exception of this paragraph.