| 74 |
74 |
Foremost amongst these lies the proof-theoretic approach, characterising classes as the `representable' functions of some logic or theory.
|
| 75 |
75 |
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}.
|
| 76 |
76 |
|
| 77 |
|
To some extent there is a distinction between various notions of `representability', namely between logics that 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.
|
| 78 |
|
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, e.g.\ \cite{Buss86book}, bounded modalities, e.g.\ \cite{GirardSS92:bounded-ll} 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}.
|
|
77 |
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.
|
|
78 |
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}.
|
| 79 |
79 |
|
| 80 |
|
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. 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}.
|
|
80 |
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}.
|
| 81 |
81 |
|
| 82 |
82 |
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$.
|
| 83 |
83 |
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}.
|
| 84 |
|
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 (and independently Mints) which is ideal for extracting ground programs directly from classical proofs in weak theories.
|
|
84 |
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.
|
| 85 |
85 |
This extends work presented in \cite{BaillotDas16}. %at \emph{CSL '16}.
|
| 86 |
86 |
|
| 87 |
87 |
\section{State of the art}
|
| 88 |
88 |
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.
|
| 89 |
|
As justification for this position, consider the following table of examples of known characterisations:
|
|
89 |
As justification for this position, consider the following table of examples of known characterisations:\footnote{All classes can be taken in their functional variations.}
|
| 90 |
90 |
%, distinguished by the type level of programs extracted:
|
| 91 |
91 |
|
| 92 |
92 |
\bigskip
|
| 93 |
93 |
|
| 94 |
94 |
\begin{tabular}{c|c|c}
|
| 95 |
|
Class\footnote{All classes can be taken in their functional variations.} & Ground & Higher order\\
|
|
95 |
Class & Ground & Higher order\\
|
| 96 |
96 |
\hline
|
| 97 |
97 |
% quantifiers & type-level\\
|
| 98 |
|
$\nc^i$ - $\ac^i$ & \cite{CloTak:1995:nc-ac}, \cite{Cook:2010:LFP:1734064} & - \\
|
|
98 |
$\nc^i$ & $\mathit{TNC}^i$ \cite{CloTak:1995:nc-ac}, $\mathit{VNC}^i$ \cite{Cook:2010:LFP:1734064} & - \\
|
| 99 |
99 |
$\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} \\
|
| 100 |
|
$\Box_i$ & $S^i_2$ \cite{Buss86book}, Kahle-Oitavem & - \\
|
|
100 |
$\Box_i$ & $S^i_2$ \cite{Buss86book}, \cite{KahOit:13:ph-levels} & - \\
|
| 101 |
101 |
$\ph$& $S_2$ & - \\
|
| 102 |
|
$\pspace$& ? & \cite{GaboardiMarionRonchi12} \\
|
|
102 |
$\pspace$& $U^1_2$ \cite{Buss86book} & $\mathit{STA}_B$ \cite{GaboardiMarionRonchi12} \\
|
| 103 |
103 |
% $k$-$\exptime$ & - & $\mathit{ELL}(k)$ \\
|
| 104 |
104 |
Elementary & $I\Delta_0 + \exp$ & $\mathit{ELL}\; \cite{Girard94:lll}$
|
| 105 |
105 |
\end{tabular}
|
| ... | ... | |
| 107 |
107 |
\bigskip
|
| 108 |
108 |
|
| 109 |
109 |
\noindent
|
| 110 |
|
Thus, if we want an implicit characterisation of $\ph$, we should break the apparent (although not universal) link between `implicit' and `higher type'.
|
|
110 |
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'.
|
| 111 |
111 |
%If we restrict to the ground setting, where extracted programs do not make use of higher types, we have the following picture.
|
| 112 |
|
|
|
112 |
%
|
| 113 |
113 |
% Now, if we restrict to the ground setting, where extracted programs do not make use of higher types, there are still several
|
| 114 |
|
Now, if we zoom on the ground setting, where extracted programs do not make use of higher types, there are still several parameters by which the characterizations can vary, including:
|
|
114 |
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:
|
| 115 |
115 |
\begin{itemize}
|
| 116 |
|
\item how are the functions specified ? By a formula, as in Peano arithmetic, by a first-order equational program, or by an applicative term in the style of combinatory algebra;
|
| 117 |
|
\item what is the form of the extracted programs? A program of a bounded recursion class, e.g. of Cobham's algebra, or of a tiered recursion class, e.g. of Bellantoni-Cook's algebra.
|
|
116 |
\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;
|
|
117 |
\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.
|
| 118 |
118 |
\end{itemize}
|
| 119 |
|
We classify the characterizations from the literature according to these two parameters in the following table:
|
|
119 |
We classify some known characterisations from the literature according to these two parameters in the following table:
|
| 120 |
120 |
\bigskip
|
| 121 |
121 |
|
| 122 |
122 |
\begin{tabular}{c|c|c}
|
| ... | ... | |
| 124 |
124 |
%\small model of comp. $\backslash$ extracted program
|
| 125 |
125 |
} & bounded rec. programs & tiered rec. programs \\
|
| 126 |
126 |
\hline &&\\
|
| 127 |
|
formula & PH, $\square_i$&\\
|
| 128 |
|
& bounded induction (Buss \cite{Buss86book}) &\\
|
|
127 |
formula & $\ph$, $\square_i$ (Buss \cite{Buss86book})&\\
|
|
128 |
% & bounded induction (Buss \cite{Buss86book}) &\\
|
| 129 |
129 |
\hline &&\\
|
| 130 |
|
equational && P\\
|
|
130 |
equational && $\ptime$\\
|
| 131 |
131 |
&& (Leivant \cite{Leivant94:intrinsic-theories}) \\
|
| 132 |
132 |
\hline &&\\
|
| 133 |
|
applicative &P (Strahm \cite{Strahm03}) & P \\
|
| 134 |
|
&PH (Kahle-Oitavem \cite{KahOit:13:ph-levels})& (Cantini \cite{Cantini02})
|
|
133 |
applicative & $\ptime$ (Strahm \cite{Strahm03}) & $\ptime$ \\
|
|
134 |
&$\ph$ (Kahle-Oitavem \cite{KahOit:13:ph-levels})& (Cantini \cite{Cantini02})
|
| 135 |
135 |
\end{tabular}
|
| 136 |
136 |
|
| 137 |
137 |
%TODO: improve table to make clear columns and rows, explicit and implicit columns.
|
| ... | ... | |
| 154 |
154 |
\bigskip
|
| 155 |
155 |
|
| 156 |
156 |
\noindent
|
| 157 |
|
Our goal is to extend the approach using extraction of programs of a tiered recursion class (second row), using the equational style of specification (second line), to the whole of the polynomial hierarchy, so PH and the $\square_i$ levels.
|
|
157 |
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$.
|
| 158 |
158 |
%Our goal is to extend the implicit approach, via variations of Bellantoni-Cook (BC) programs, to the whole of the polynomial hierarchy.
|
| 159 |
159 |
|
| 160 |
160 |
\section{Towards an implicit theory for $\ph$}
|
| ... | ... | |
| 179 |
179 |
|
| 180 |
180 |
\subsection{Extraction at ground type}
|
| 181 |
181 |
As we did in \cite{BaillotDas16}, we will rely on the \emph{witness function method} for extracting functions at bounded type.
|
| 182 |
|
This was pioneered by Buss, although independently used by Mints beforehand. The idea is as follows:
|
|
182 |
%This was pioneered by Buss, although independently used by Mints beforehand.
|
|
183 |
The idea is as follows:
|
| 183 |
184 |
\begin{enumerate}
|
| 184 |
185 |
\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.
|
| 185 |
186 |
\item\label{item:free-cut} Conduct a \emph{free-cut elimination} on the proof, resulting in a proof whose formulae are restricted to
|
| ... | ... | |
| 193 |
194 |
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.
|
| 194 |
195 |
|
| 195 |
196 |
|
| 196 |
|
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.
|
|
197 |
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}.
|
| 197 |
198 |
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$.
|
| 198 |
199 |
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.
|
| 199 |
200 |
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}.
|