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

\section{Introduction and motivation}

\label{sect:intro}

Today, there are countless approaches towards characterising complexity classes via logic.

Foremost amongst these lies the proof-theoretic approach, characterising classes as the `representable' functions of some logic or theory.

Examples include bounded arithmetic \cite{Buss86book} \cite{Krajicek:1996:BAP:225488} \cite{Cook:2010:LFP:1734064}, applicative theories \cite{Cantini02} \cite{KahOit:13:ph-levels}, intrinsic and ramified theories \cite{Leivant94:intrinsic-theories} \cite{BelHof:02}, fragments of linear logic \cite{GirardSS92:bounded-ll} \cite{Girard94:lll} \cite{Lafont04} \cite{Baillot15} and fragments of intuitionistic logic \cite{Leivant94:found-delin-ptime}.

To some extent there is a distinction between various notions of `representability', namely between logics that \emph{type} terms computing functions of a given complexity class, and theories that prove the \emph{totality} or \emph{convergence} of programs computing functions in a given complexity class.

But a perhaps more important distinction is whether the constraints on the logic or theory are

\textit{explicit} or \textit{implicit}, that is to say whether they stipulate some bounds or resources, or whether the bounds are only \textit{consequence} of some logical properties. One important representative of the first category is \textit{bounded arithmetic}, based on theories of arithmetic where quantiiers are bounded by terms in induction or comprehension formulae \cite{Buss86book,Krajicek:1996:BAP:225488,Cook:2010:LFP:1734064}. Cobham's function algebra  \cite{Cobham}  for polynomial time is of a similar nature, and indeed is used as a tool for the study of bounded arithmetic. In the second category one can range the systems of \textit{implicit computational complexity}, like for instance function algebras based on restrictions of recursion, such as ramified or safe recursion \cite{BellantoniCook92,Leivant95}, arithmetics or logics based on analogous restrictions of induction \cite{Cantini02},  \cite{Leivant94:intrinsic-theories} \cite{BelHof:02},  \cite{Marion01}, \cite{Leivant94:found-delin-ptime} and subsystems of linear logic   \cite{Girard94:lll} \cite{Lafont04} .

 Bounded arithmetic is a deep and well-established field, and one of its advantages is its great versatility, allowing a characterization of a wide range of complexity classes, such as $\ptime$, the polynomial hierarchy $\ph$, $\pspace$, $\mathbf{NC}^i$ etc.

 %It is also closely related to \textit{proof complexity}, the research field investigating the size of propositional proofs in various proof systems. Finally it is also employed for the research direction of \textit{bounded reverse mathematics}.

  Implicit computational complexity on the other hand is a slightly more recent and less unified line of research. It aims to relate certain computing disciplines with complexity theoretic features, and has helped shed some light on the foundational nature of `feasibility' (see e.g.~\cite{Leivant94:found-delin-ptime}).

  Another benefit is that implicit complexity systems can sometimes be extended into techniques for statically controlling the complexity of programs, e.g. in functional or imperative languages (e.g. \cite{Hofmann00,Hofmann03}, \cite{Marion11}).  However the variety of complexity classes that have been characterized in this implicit way is not as large as for bounded arithmetic. In particular implicit complexity has not managed to characterize non-deterministic classes, such as $\mathbf{NP}$ or $\ph$, in a purely logical way.\footnote{Actually some characterizations of such classes do exist, but they either take the form of a function algebra \cite{bellantoni1995fph} or of a type system extended with a non-logical feature \cite{GaboardiMarionRonchi12}.}

 Systems in implicit complexity typically imposes constraints on the comprehension scheme, the primitive recursion scheme or the structural rules of proof systems (namely \emph{contraction}).

% But it seems to us that first-order quantification has not yet been investigated as much as it deserves. We believe that this is one reason of the modest achievements of implicit complexity concerning non-deterministic classes.

%

  In the present work we aim to bridge the gap to bounded arithmetic by constructing `implicit' theories that characterise the functional polynomial hierarchy $\fph$ and its levels. We consider a base theory similar to that of bounded arithmetic, but we allow induction on \emph{unbounded} formulae, i.e.\ without any explicit bounds.

%  By implicit complexity arithmetic we mean that the quantifiers employed should not be bounded quantifiers. Our motivation is to bridge the fields of bounded arithmetic and implicit complexity, and to try pave the way for the design of systems bringing together simplicity (no explicit bounds) and versatility, in which one could transfer some of the main results of bounded arithmetic.

%

%  Our methodology will be the following one:

Naturally another constraint is in order, and for this we will use the concept of \textit{ramification} that is common in implicit complexity \cite{Leivant95,BellantoniCook92}.

%, adapt it in the setting of first-order arithmetic, and then explore some properties relative to quantification. First

Also known as \emph{safe recursion}, ramification a discipline which aims at limiting the power of recursion by distinguishing two (or more) levels of integers: the \textit{safe} or level-0 integers (in this work $\safe$), and the \textit{normal} or level-1 ones (in this work $\normal$).

In a nutshell, recursion is permitted on normal arguments, but recursive calls can only appear in safe positions. Basic operations, such as conditionals and Boolean predicates, can be performed on safe arguments.

Functions defined in this way correspond to polynomial time functions \cite{BellantoniCook92}.

  This discipline can be transposed into first-order arithmetic by adding predicates for normal and safe integers and by limiting the induction scheme by allowing induction only on normal integers, but crucially on formulae with only \emph{safe} unbounded quantifiers.

  %The key step we make is to focus our attention on \textit{safe quantifiers} that is to say quantifiers on safe variables.

  These safe quantifiers play a r\^ole analogous to bounded quantifiers in bounded arithmetic. In particular we will consider a hierarchy $\Sigma_i^{\safe}$ of formulas, according to the number of alternations of safe quantifiers, to define a hierarchy of theories $\arith^i$ allowing induction on $\Sigma^\safe_i$ formulae.

  We show that such a theory proves the totality of precisely the $\fph_i$ functions, relying on a recursion-theoretic characterisation of $\fph$ due to Bellantoni \cite{bellantoni1995fph} to both extract programs and prove completeness of the theory with respect to $\fph_i$.

  \medskip

  \noindent

  \textbf{Related work}. To the best of our knowledge, our work is the first characterization of the polynomial hierarchy and its levels in an implicit arithmetic. Our approach is however related to several previous works, and differs either by some of the definitions and/or by the complexity class characterized.

  One particular difference is that we specify programs using arithmetic formulae, as in bounded arithmetic, rather than equational specifications or combinatory terms in other works, which seems to be important for characterizing $\fph$.

%   A first axis of classification between the logics and arithmetics for complexity classes is the way by which they specify functions. The options at stake can be enumerated as follows: (i) \textit{formula specification}, as in first-order bounded arithmetic \cite{Buss86book}, (ii) \textit{equational specification}, as in Leivant's intrinsic theories   \cite{Leivant94:intrinsic-theories}, (iii) \textit{combinatory terms} as in applicative theories (e.g. \cite{Strahm03}) or $\lambda$-calculus terms. A second axis, as explained in the introduction, is whether the system is explicit or implicit.

%

%   Our approach in this paper is to use the formula-specification point of view, because it is convenient for the polynomial hierarchy.

   The arithmetic of \cite{KahOit:13:ph-levels} characterizes $\fph$, but it is not implicit, relying on axioms defining bounded schemes.

%   Some other works are closer to our methodology in the sense that they are implicit arithmetics and rely on a notion of ramification, but they characterize other complexity classes.

   Leivant's intrinsic theories \cite{Leivant94:intrinsic-theories}  induces characterizations of $\fptime$ and elementary functions, using equational specifications, and \cite{Cantini02} obtains an analogous result for $\fptime$ using combinatory terms.

   The paper \cite{BelHof:02} also provides a characterization of $\fptime$, with two differences: on the one hand induction is on arbitrarily quantified formulas, and on the other hand the underlying logic is not classical logic but a variant of linear logic, with a modality for normal arguments. Our paper \cite{BaillotDas16} proves a similar result, but with a different method.

   The lack of contraction is crucial here to stop the theory from exhausting higher complexity classes.

   Finally the paper \cite{OstrinWainer05} also presents an implicit ramified arithmetic, with quantification on safe variables. Here equational specifications are used instead of formulas and unary integers  instead of binary integers, which leads to a characterization of the elementary functions.

  \medskip

  \noindent

  \textbf{Outline.} The rest of this paper proceeds as follows. We first give some background on function algebras for $\fptime$ and $\fph$ respectively in Sect.~\ref{sect:prelims}.

  %Then we describe an encoding of sequences which will be instrumental in the proof of our result.

  We present our arithmetic theories $\arith^i$ in Sect.~\ref{sect:arithmetic} and prove our soundness result, that the provably total functions of $\arith^i$ are in $\fph_i$, in Sect.~\ref{sect:soundness}. Finally, we prove the completeness result, that all $\fph_i$ functions have a representation provably total in $\arith^i$, in Sect.~\ref{sect:completeness}, and present conclusions in Sect.~\ref{sect:conclusion}.

%  \patrick{

%  \begin{itemize}

%  \item our goal: design an unbounded arithmetic for FPH.

%

%  motivations: bridge bounded arithmetic and ICC ; enlarge the toolbox of ICC

%  \item methodology: use ramification, and calibrate the logic by alternance of quantifiers in induction formulas

%  \item key idea: replace the role of bounded quantifiers by safe quantifiers

%  \item related works

%  \end{itemize}

%  }

%

%\anupam{Copied below from DICE submission}

%

%Today, there are countless approaches towards characterising complexity classes via logic.

%Foremost amongst these lies the proof-theoretic approach, characterising classes as the `representable' functions of some logic or theory.

%Examples include bounded arithmetic \cite{Buss86book} \cite{Krajicek:1996:BAP:225488} \cite{Cook:2010:LFP:1734064}, applicative theories \cite{Cantini02} \cite{KahOit:13:ph-levels}, intrinsic and ramified theories \cite{Leivant94:intrinsic-theories} \cite{BelHof:02}, fragments of linear logic \cite{GirardSS92:bounded-ll} \cite{Girard94:lll} \cite{Lafont04} \cite{Baillot15} and fragments of intuitionistic logic \cite{Leivant94:found-delin-ptime}.

%

%To some extent there is a distinction between various notions of `representability', namely between logics that \emph{type} terms computing functions of a given complexity class, and theories that prove the \emph{totality} or \emph{convergence} of programs computing functions in a given complexity class.

%Perhaps a more important (and somewhat orthogonal) distinction for the \textsc{Dice-Fopara} community is whether the constraints on the logic or theory are \emph{implicit} or \emph{explicit}. The former includes constraints such as ramification, type level and substructural considerations, while the latter includes bounded quantification, bounded modalities etc. This distinction is also naturally exhibited in associated function algebras, e.g. Cobham's \emph{limited} recursion on notation \cite{Cobham} vs.\ Bellantoni and Cook's \emph{predicative} recursion on notation \cite{BellantoniCook92}.

%

%Some correlations abound: explicit bounds are typically far more useful for more fine-grained characterisations of complexity classes, e.g.\ levels of the polynomial or arithmetical hierarchies, and often admit witness extraction methods that remain in a ground type programming language, e.g.\ via recursion theoretic characterisations. Implicit bounds, however, are more often associated with higher-typed programming languages, which are arguably more useful for achieving witness extraction at all for powerful theories such as arithmetic and set theory, cf.~\cite{avigad1998godel}, \cite{troelstra1998realizability}. Complexity bounds are harder to obtain, but the framework is nonetheless somewhat more desirable since no bounds occur in the characterisation itself \emph{per se}.

%

%In this line of work we attempt to ameliorate the situation by using implicit methods to delineate fine-grained hierarchies of feasible complexity classes, namely the \emph{polynomial hierarchy}, $\ph$.

%One particular feature of this work that helps make this possible is to break one of the aforementioned correlations: while we use implicit constraints, our witness extraction methods will use only functions of bounded type level. In this way we can naturally appeal to function algebras, which are of ground type in nature, which implicitly characterise $\ph$, namely via \emph{predicative minimisation} \cite{BellantoniThesis}.

%In order to remain in this class of programs and not get lost with higher types, we appeal to the \emph{witness function method} of extracting programs from proofs, a technique developed by Buss \cite{Buss86book} \cite{Buss:95:wfm-arith}, which is ideal for extracting ground programs directly from classical proofs in weak theories.

%This extends work presented in \cite{BaillotDas16}. %at \emph{CSL '16}.

%

%\subsection{State of the art}

%As we have already argued, it is natural to expect that characterisations of hierarchies such as $\ph$ are more readily established by using ground or bounded type witness extraction procedures, due to the correspondence between logical searches in a program and the quantification over objects of ground type in a theory.

%As justification for this position, consider the following table of examples of known characterisations:\footnote{All classes can be taken in their functional variations.}

%%, distinguished by the type level of programs extracted:

%

%\bigskip

%

%\begin{tabular}{c|c|c}

%	Class &	Ground & Higher order\\

%	\hline

%	%	quantifiers  & type-level\\

%	$\nc^i$    & $\mathit{TNC}^i$ \cite{CloTak:1995:nc-ac}, $\mathit{VNC}^i$ \cite{Cook:2010:LFP:1734064} & - \\

%	$\ptime$  &  $S^1_2$ \cite{Buss86book}, \cite{Strahm03}, $V^1$ \cite{Zambella96} \cite{Cook:2010:LFP:1734064} & $\mathit{LLL}$ \cite{Girard94:lll}, $\mathit{SLL}$ \cite{Lafont04} \\

%	$\Box_i$  & $S^i_2$ \cite{Buss86book}, \cite{KahOit:13:ph-levels} & -  \\

%	$\ph$& $S_2$ & - \\

%	$\pspace$& $U^1_2$ \cite{Buss86book} & $\mathit{STA}_B$ \cite{GaboardiMarionRonchi12} \\

%	%	$k$-$\exptime$ & -  & $\mathit{ELL}(k)$ \\

%	Elementary & $I\Delta_0 + \exp$  & $\mathit{ELL}\;  \cite{Girard94:lll}$

%\end{tabular}

%

%\bigskip

%

%\noindent

%Thus, if we want an implicit characterisation of $\ph$ in a logical theory, we should break the apparent (although not universal) link between `implicit' and `higher type'.

%%If we restrict to the ground setting, where extracted programs do not make use of higher types, we have the following picture.

%%

%% Now, if we restrict to the ground setting, where extracted programs do not make use of higher types, there are still several

%Now, if we zoom in on the ground setting, where extracted programs do not make use of higher types, there are still several parameters by which the characterisations can vary, in particular:

%\begin{itemize}

%	\item How are programs specified in the language of the theory? By a formula, as in Peano arithmetic, by a first-order equational program, or by an applicative term in the style of combinatory algebra;

%	\item What type of programs are extracted from proofs of the theory? A program of a bounded recursion class, e.g.\ of Cobham's algebra, or of a tiered recursion class, e.g.\ of Bellantoni and Cook's algebra.

%\end{itemize}

%We classify some known characterisations from the literature according to these two parameters in  the following table:

%\bigskip

%

%\begin{tabular}{c|c|c}

%	{

%		%\small model of comp. $\backslash$ extracted program

%	} & bounded rec. programs & tiered rec. programs \\

%	\hline &&\\

%	formula & $\ph$, $\square_i$ (Buss \cite{Buss86book})&\\

%	%	& bounded induction (Buss \cite{Buss86book}) &\\

%	\hline &&\\

%	equational && $\ptime$\\

%	&& (Leivant \cite{Leivant94:intrinsic-theories}) \\

%	\hline &&\\

%	applicative & $\ptime$ (Strahm \cite{Strahm03})  & $\ptime$ \\

%	&$\ph$ (Kahle-Oitavem \cite{KahOit:13:ph-levels})& (Cantini \cite{Cantini02})

%\end{tabular}

%

%%TODO: improve table to make clear columns and rows, explicit and implicit columns.

%%

%%\begin{tabular}{c|c|c|c}

%%	{

%%		%\small model of comp. $\backslash$ extracted program

%%		} & Cobham & mon. constraints & BC-like \\

%%	\hline &&\\

%%	formula & PH, $\square_i$&&\\

%%	& bounded induction (Buss) &&\\

%%	\hline &&\\

%%	equational &&& P\\

%%	&&& (Leivant) \\

%%	\hline &&\\

%%	applicative &&PH & P \\

%%	&&(Kahle-Oitavem)& (Cantini)

%%\end{tabular}

%

%\bigskip

%

%\noindent

%Our goal is to extend the approach using extraction of programs of a tiered recursion class (second column), using the equational style of specification (second row), to the whole of the polynomial hierarchy, i.e.\  $\ph$ and its levels $\square_i$.

%%Our goal is to extend the implicit approach, via variations of Bellantoni-Cook (BC) programs, to the whole of the polynomial hierarchy.