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

\documentclass[a4paper]{article}

\usepackage{amssymb}

\usepackage{amsthm}

\usepackage{hyperref}

\setcounter{tocdepth}{3}

\newtheorem*{conjecture*}{Conjecture}

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

\title{Towards an implicit characterisation of the polynomial hierarchy in an unbounded arithmetic \\ {\small Work in progress} }

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

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

\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{Towards an implicit theory for $\ph$}

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

We explain our approach for this work-in-progress in more detail here, referring to previous work when analogous methods are used.

\subsection{Implicit programs for $\ph$}

Since we want to remain at ground type, the natural programs in which to extract our witnesses will come from recursion theoretic characterisations, cf.\ the table above. Indeed, as we have already mentioned, we are not aware of any `higher-type' characterisation of $\ph$.

Of these, only the Bellantoni framework from \cite{BellantoniThesis}, which extends BC-programs by \emph{predicative minimisation} constitutes an implicit characterisation, and so we will look to 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 one of our desiderata is to replicate this property, only for unbounded quantifiers.

Naturally, another constraint will be 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$ will be 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 will 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-like 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}.

\subsection{Extraction at ground type}

As we did in \cite{BaillotDas16}, we will 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, with appropriate semantic properties of these programs verified by an interpretation into a (classical) quantifier-free theory.

\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, and so potentially allows 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$, it seems straightforward to formalise a standard argument, e.g.\ from bounded arithmetic \cite{Buss86book}, where applications of minimisation in a program correspond to 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.

%

	\subsection{Putting it all together}

To summarise the main goal of this work-in-progress, we are aiming for a variation of the following result:

\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{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}