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

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

	$\pspace$&  ? & \cite{GaboardiMarionRonchi12} \\

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

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

 \begin{itemize}

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

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

 \end{itemize}

We classify the characterizations from the literature according to these two parameters in  the following table:

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

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

	formula & PH, $\square_i$&\\

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

	equational && P\\

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

	applicative &P (Strahm \cite{Strahm03})  & P \\

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

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

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.

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