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

\documentclass[a4paper]{article}

\usepackage{amssymb}

\usepackage{amsmath}

\usepackage{amsthm}

\usepackage{hyperref}

\setcounter{tocdepth}{3}

\newtheorem*{conjecture*}{Conjecture}

\newtheorem*{theorem*}{Theorem}

\newcommand{\fph}{\mathbf{PH}}

\title{An implicit characterisation of the polynomial hierarchy in an unbounded arithmetic }

\author{Patrick Baillot \and Anupam Das}

%\date{ Univ Lyon, CNRS, ENS de Lyon, Universit\'e Claude Bernard Lyon 1, LIP

%	%\\[2ex] \today

%	}

\date{ Univ Lyon, CNRS, ENS de Lyon, UCB Lyon 1, LIP

	%\\[2ex] \today

	}	

	\newcommand{\ph}{\mathbf{PH}}

	\newcommand{\pspace}{\mathbf{PSPACE}}

	\newcommand{\fpspace}{\mathbf{FPSPACE}}

	\newcommand{\ptime}{\mathbf{P}}

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

	\newcommand{\nc}{\mathbf{NC}}

	\newcommand{\ac}{\mathbf{AC}}

	\newcommand{\exptime}{\mathbf{EXP}}

\begin{document}

\maketitle

%\begin{itemize}

%\item a big picture: logic methods for complexity classes:

%

%\begin{tabular}{c|c}

%ground & higher-order\\

%quantifiers  & type-level\\

%PSPACE    & $k$-EXP\\

%PH  &              P\\

%P  &\\

%$NC_i$&

%\end{tabular}

%

%\item  state of the art on arithmetics for complexity classes:

%

%\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\\

%&&& (intrinsic theories: Leivant) \\

%\hline &&\\

%applicative &&PH & P \\

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

%\end{tabular}

%\item our goal: explore the properties of implicit complexity arithmetics, and in particular import in the area of implicit complexity some techniques based on the control of first-order quantification, so as to characterize complexity classes between P and PSPACE (in particular PH).

%\item an apparent paradox: when one considers induction over arbitrarily quantified formulas the ramified arithmetics

%of [Cantini00] and [BellantoniHofmann02] characterize P, while Buss' bounded arithmetic $S_2$ characterizes PH (while restriction to induction over $\Sigma_1$ formulas corresponds to P).

%\item the setting we will consider: 

%\begin{itemize}

%\item classical first order modal logic ($S4$); a predicate $W(.)$ stands for (binary representations of) integers; the modality $\square$ is a tool for managing ramification (as in  [Cantini00, BellantoniHofmann02]), in particular to distinguish safe integers (by $W(.)$) from normal ones ($\square W(.)$), according to Bellantoni-Cook's terminology.

%\item \textit{specifications} (or program descriptions) are given by theories over basic formulas consisting in equations (this will be a slight generalization of the setting of intrinsic theories described by Leivant, and used by    [BellantoniHofmann02]).

%\end{itemize}

%\item Our conjecture: ramified first-order modal classical logic with full induction, for equational programs, characterize the class PH.

%

%the function algebra characterization of PH we want to use for that is Bellantoni's $\mu$-functions algebra for PH (cf. Bellantoni's PhD thesis).

%\end{itemize}

%

%\newpage

\section{Introduction and motivation}

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.

A somewhat orthogonal distinction 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}.

While implicit constraints may be preferable since no bounds occur in the characterisation itself \emph{per se}, explicit bounds are typically far more useful for more fine-grained characterisations of complexity classes. For instance, the polynomial hierarchy, $\ph$, and its levels can be neatly characterised by the theories $S^i_2$ of \emph{bounded arithmetic}, using bounds on quantifiers to control complexity \cite{Buss86book}.\footnote{Other approaches to $\ph$ exist, but also use explicit bounds, e.g.\ \cite{Cook:2010:LFP:1734064}, \cite{KahOit:13:ph-levels}.}

%

%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 work we improve the situation by using implicit methods in first-order theories to characterise $\ph$.

To achieve this we work with a function algebra of Bellantoni from \cite{BellantoniThesis} in which to extract programs, and use the \emph{witness function method} of Buss to extract programs at ground type and preserve quantifier information, necessary to delineate the levels of $\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}.

%\section{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

%%%% DICEFOPARA revision hereafter

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

%%

%%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.

\section{Methodology}

We describe some of the techniques used in this work, before briefly giving our main results in the next section.

\subsection{Implicit programs for $\ph$}

Extracting programs at ground type seems to be a necessity in order to delineate the levels of $\ph$.\footnote{Indeed we are not aware of any `higher-type' characterisation of $\ph$.} Therefore the natural programs in which to extract our witnesses will come from \emph{recursion theoretic} characterisations. 

Of these, only the Bellantoni framework from \cite{BellantoniThesis}, which extends safe recursive programs \cite{BellantoniCook92} by \emph{predicative minimisation} constitutes an implicit characterisation, and so we extract our programs into this function algebra, henceforth denoted $\mu$BC.

\subsection{Constraints on induction}

An appealing feature of the bounded arithmetic approach is that bounds on (bounded) quantifier alternation in induction formulae precisely delimit the levels of $\ph$, and we are able to replicate this property, only for unbounded quantifiers.

Naturally, another constraint is required to stop ourselves from exhausting the arithmetical hierarchy once bounds are dismissed, and for this we use essentially a \emph{ramification} of individuals: explicit predicates $N_0, N_1 , \dots$ are used similarly to Peano's $N$ predicate to intuitively indicate `how sure' we are that a variable denotes a genuine natural number.

In fact, two predicates suffice and their relationship is entirely governed by the equation $N_1 (x) \iff \square N_0 (x)$, under the laws of the modal logic $\mathit{S4}$. 

The distinction between the two predicates corresponds to the distinction between safe and normal variables in BC  programs, which was an observation from previous work \cite{BaillotDas16}.

A similar phenomenon occurs in Cantini's work \cite{Cantini02}, which presents a characterisation of $\ptime$ in an \emph{applicative theory}, in order to extract BC programs. 

While he allows arbitrary alternation of unbounded quantifiers, note that his induction is \emph{positive}, and so universal quantifiers cannot vary over certified natural numbers, i.e.\ individuals in $N$. In fact this sort of unbounded quantification is also compatible with our approach of \cite{BaillotDas16}.

%with an approach in previous work where we characterised $\ptime$ in a \emph{linear logic}, also extracting BC programs %\cite{BaillotDas16}.

The idea of using ramified theories in implicit complexity, inducting on normal variables rather than safe, is largely due to Leivant \cite{Leivant94:intrinsic-theories}, who introduced \emph{intrinsic theories} for an arbitrary free algebra.

The same idea was also used in \cite{OstrinWainer05} for a theory of arithmetic characterising the elementary functions, somewhat reworking of Leivant's work.

The main difference in this work, which is why we are able to characterise $\ph$, is that for our model of computation we simply use formulas of the theory rather than equational specifications used in \cite{Leivant94:intrinsic-theories} and \cite{OstrinWainer05}. This indeed has a significant effect on the complexity class characterised, as observed in \cite{BelHof:02}.

%In this way, we extend rather certain work in Bellantoni's thesis \cite{BellantoniThesis}, where theories for $\ptime$ are presented.

\subsection{Extraction at ground type}

We rely on the \emph{witness function method} for extracting functions at bounded type.

%This was pioneered by Buss, although independently used by Mints beforehand. 

The idea is as follows:

\begin{enumerate}

	\item\label{item:de-morgan} Reduce a proof to \emph{De Morgan} normal form, with formulae over the basis $\{ \bot, \top, \vee , \wedge , \exists, \wedge \}$ and negation restricted to atoms.

	\item\label{item:free-cut} Conduct a \emph{free-cut elimination} on the proof, resulting in a proof whose formulae are restricted to

	essentially just subformulae of the conclusion, axioms and nonlogical steps.

	\item\label{item:interp} Extract witnesses inductively from the proof into an appropriate function algebra, verifying the necessary semantic properties along the way.

	\end{enumerate}

	\ref{item:de-morgan} ensures that our extraction works at ground type, rather than higher types which are typically necessary when negation has larger scope.

	At the same time it preserves the quantifier alternation information that is crucial to distinguishing the levels of $\ph$.

	\ref{item:free-cut} allows us to assume that all formulae in a proof have logical complexity bounded by that of induction formulae.

	This means that, when extracting programs via \ref{item:interp}, quantifier alternation of induction formulae corresponds to the depth of minimisation operators in a $\mu$BC program, allowing for a level-by-level correspondence with the polynomial hierarchy.

%	We point out that, in some ways, this is similar to approaches from applicative theories, which typically use free-cut elimination followed by a direct \emph{realisability} argument, e.g.\ in \cite{Strahm03}, \cite{Cantini02} and \cite{KahOit:13:ph-levels}.

%	Indeed this could have been possible in our previous work \cite{BaillotDas16}, as Cantini did in his work \cite{Cantini02}, for a characterisation of $\ptime$.

%	However, in this case, since the quantifiers are unbounded the realisability argument is apparently not readily formalised, and it is therefore quite natural to pursue a \emph{bona fide} proof interpretation.

	%%% Following part has been removed in the revised DICEFOPARA version

	%For this, it seems we need to go one level higher than type 1 functions to verify semantic properties of witnesses of first-order formulae, themselves considered as genuine type 1 functions. Intuitively this is simply an inlining of \emph{Skolemisation}, although the idea of extending `witness predicates' to type 1 objects resembles methods from second-order bounded arithmetic, e.g.\ \cite{Cook:2010:LFP:1734064}. 

	%Unlike in the bounded arithmetic setting, due to the apparent unboundedness of programs in the $\mu$BC framework, we will need a formal witness predicate implemented itself as a BC-like program, hence the need for a proof interpretation rather than a realisability approach.

	%% since we cannot externally certify the complexity of the predicate when unbounded quantifiers abound.

	%Fortunately, we believe that it suffices to consider $\mu$BC-programs with \emph{holes}, rather than a full characterisation of type 2 $\ph$, but verifying that such an approach could work represents the outstanding technical component of this work-in-progress.

	\subsection{Completeness for PH}

	In the other direction, showing completeness for $\ph$, we are able to formalise a more-or-less standard argument, e.g.\ from bounded arithmetic \cite{Buss86book}, where applications of minimisation in a program correspond to applications of the \emph{well ordering property} in arithmetic.

	This is in turn is a corollary of induction but, in this case, crucially relies on the use of \emph{right-contraction} in the logic.

	It seems that this feature is crucial in distinguishing these theories from `linear' variants like in previous work \cite{BaillotDas16}, and in particular work of Bellantoni and Hofmann \cite{BelHof:02} where, without right-contraction, any number of quantifier alternations still corresponds to only polynomial time computation.

	%	* PB: I would suggest to skip **

	%	

	%	TODO or skip? If so just say that we formalise the standard argument (with explanation, e.g.\ minimisation, WOP, induction) but rely on safety of quantification rather than boundedness, which should come for free by inspection.

	%	

	%\begin{conjecture*}

	%	First-order classical modal logic $\mathit{S4}$ with induction restricted to non-modal formulae, over a suitable set of axioms, characterises the class $\ph$. Bounds on quantifier alternation in induction formulae delimit the levels of $\ph$.

	%\end{conjecture*}

	% ALTERNATIVE SUGGESTION

	%\begin{conjecture*}

	%	First-order ramified classical  logic with induction restricted to \textit{safe} formulae (that is to say not containing any $N_1$), over a suitable set of axioms, characterises the class $\ph$. Bounds on quantifier alternation in induction formulae delimit the levels of $\ph$.

	%\end{conjecture*}

	%	As mentioned, we will 

	%	

	%	[copied]

	%	

	%	%\item our goal: explore the properties of implicit complexity arithmetics, and in particular import in the area of implicit complexity some techniques based on the control of first-order quantification, so as to characterize complexity classes between P and PSPACE (in particular PH).

	%	

	%	the setting we will consider: 

	%	\begin{itemize}

	%		\item classical first order modal logic ($S4$); a predicate $W(.)$ stands for (binary representations of) integers; the modality $\square$ is a tool for managing ramification (as in  [Cantini00, BellantoniHofmann02]), in particular to distinguish safe integers (by $W(.)$) from normal ones ($\square W(.)$), according to Bellantoni-Cook's terminology.

	%		\item \textit{specifications} (or program descriptions) are given by theories over basic formulas consisting in equations (this will be a slight generalization of the setting of intrinsic theories described by Leivant, and used by    [BellantoniHofmann02]).

	%	\end{itemize}

	%	

	%	the function algebra characterization of PH we want to use for that is Bellantoni's $\mu$-functions algebra for PH (cf. Bellantoni's PhD thesis).

	%

	%

	%

	%\subsection{Extending previous work}

	%

	%

	%\subsection{Witness function method}

	%%keep this subsection?

	%

	%

	%\subsection{Relation to previous work}

	%

	%an apparent paradox: when one considers induction over arbitrarily quantified formulas the ramified arithmetics

	%of [Cantini00] and [BellantoniHofmann02] characterize P, while Buss' bounded arithmetic $S_2$ characterizes PH (while restriction to induction over $\Sigma_1$ formulas corresponds to P).

\section{Results}

%As we mentioned, the goal of this work-in-progress is to arrive at an implicit characterisation of PH. 

%We explain our approach in more detail here.

Due to space constraints, we give only an informal account of our results.

\medskip

\noindent

	We define a family of theories $B^i$ over the language $\{0,s,+,\times, \# , |\cdot|,\lfloor \frac{\cdot}{2} \rfloor \}$ of bounded arithmetic augmented with two predicates, $N_0$ and $N_1$, which act as ramifiers for our theory. 

	These replicate the distinction between safe and normal input, respectively, for $\mu$BC programs.

		We set $N_1 \subseteq N_0$ and crucially have the following non-logical inference step:\footnote{Seen from the modal point of view, this is a form of \emph{necessitation} for models whose second-order parts are closed under first-order comprehension.}

	\[

	\frac{\vdash \forall \vec x \in N_1 . \exists \vec y \in N_0 . A(\vec x , \vec y)}{\vdash \forall \vec x \in N_1 . \exists \vec y \in N_1 . A(\vec x , \vec y)}

	\]

	For the arithmetic function symbols we give their basic defining axioms as for the theories $S^i_2$ from \cite{Buss86book}, only relativising quantifiers to match their safe-normal sorting of arguments from the Bellantoni-Cook framework.\footnote{For instance, $s, +, |\cdot|,\lfloor \frac{\cdot}{2} \rfloor $ take $N_0$ arguments, $\times$ takes one $N_0$ and one $N_1$, and $\#$ takes two $N_1$ arguments. All terms are in $N_0$.}

	We define the $\Sigma^{N_0}_i $-$\Pi^{N_0}_i$ formula hierarchy analogously to the (bounded) arithmetical hierarchy, only counting alternations of `safe quantifiers', i.e.\ those relativised to $N_0$.

	The theory $B^i_2$ contains the axiom schema of \emph{normal polynomial induction} on $\Sigma^{N_0}_i$ formulae $A$:

	\[

	\left(A(0) \wedge \forall u \in N_1 . (A\left(\lfloor \tfrac{u}{2} \rfloor\right) \supset A(u) )\right) \supset \forall u \in N_1 . A(u)

	\]

%	where $A$ is $\Sigma^{N_0}_i$.

	Our main result is the following:

	\begin{theorem*}

		$B^i_2$ proves the totality of precisely the $\Box^p_i$ functions.

	\end{theorem*}

%\section{Conclusions}

%We surveyed the state of the art for representing function classes proof theoretically by logics and theories, and considered the problem of finding an implicit characterisation of $\ph$.

%Identifying the witness function method as a useful tool for witness extraction at bounded type level, a seemingly important prerequisite for characterising $\ph$, we sought to calibrate an appropriate theory of arithmetic for witness extraction to the $\mu$BC characterisation of $\ph$.

%%We presented a conjecture that a ramified theory suffices to carry out this characterisation, based on previous work by ourselves and others 

%We presented a conjecture that a modal theory suffices to carry out this characterisation, based on previous work by ourselves and others\cite{BaillotDas16} \cite{Cantini02} \cite{BelHof:02} and proving this result constitutes the outstanding work-in-progress.

\bibliographystyle{plain}

\bibliography{biblio}

\end{document}