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

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

Examples include bounded arithmetic \cite{Buss86book}, (Krajicek, Cook etc.), applicative theories  (Feferman, Kahle, Oitavaem,) \cite{Cantini02} , intrinsic and ramified theories  , \cite{Leivant94:intrinsic-theories} (Bellantoni, Hofmann etc.) \cite{BelHof:02}, fragments of linear logic \cite{Girard94:lll} \cite{Lafont04} \cite{Baillot15} and fragments of intuitionistic logic \cite{Leivant94:found-delin-ptime}.

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, distinguished by the type level of programs extracted:

Class\footnote{All classes can be taken in their functional variations.} &	Ground & Higher order\\

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

	$\ptime$  &  $S^1_2$ \cite{Buss86book}, [app th?], $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}, Kahle-Oitavem & -  \\

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

	$\pspace$&  ? & ? \\

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

	Elementary & $I\Delta_0 + \exp$  & $\mathit{ELL}$

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

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

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.

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 an approach in previous work where we characterised $\ptime$ in a \emph{linear logic}, also extracting BC programs \cite{BaillotDas16}.

As we did for previous work \cite{BaillotDas16}, we will rely on the \emph{witness function method} for extracting functions at bounded type.

\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 use free-cut elimination followed by a direct \emph{realisability} argument.

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.

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.

	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.

%	

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

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

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