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

\section{Preliminaries}

We introduce the polynomial hierarchy and its basic properties, then the Bellantoni characterisation.

\subsection{Polynomial hierarchy}

(include closure properties)

\subsection{Bellantoni's characterisation using predicative minimisation}

(perhaps compare with Cobham's using limited recursion)

\anupam{copied below from last year's paper}

We recall the Bellantoni-Cook  algebra BC of functions defined by \emph{safe} (or \emph{predicative}) recursion on notation \cite{BellantoniCook92}. These will be employed for proving both the completeness   (all polynomial time functions are provably convergent) and the soundness result (all provably total functions are polynomial time) of THEORY. We consider function symbols $f$ over the domain  $\Word$ with sorted arguments $(\vec u ; \vec x)$, where the inputs $\vec u$ are called \textit{normal} and $\vec x$ are called \textit{safe}. 

%Each symbol is given with an arity $m$ and a number $n\leq m$ of normal arguments, and will be denoted as $f(\vec{u};\vec{x})$ where $\vec{u}$ (resp. $\vec{x}$) are the normal (resp. safe) arguments.

%We say that an expression is well-sorted if the arities of function symbols in it is respected.

%\patrick{Note that below I used the terminology 'BC programs', to distinguish them from 'functions' in the extensional sense, which I find clearer. But if you prefer to keep 'BC functions' it is all right for me.}

\begin{definition}

	[BC programs]

	BC is the set of functions generated as follows:

	%	\paragraph{Initial functions}

	%	The initial functions are:

	\begin{enumerate}

		\item The constant functions $\epsilon^k$ which takes $k$ arguments and outputs $\epsilon \in \Word$.

		\item The projection functions $\pi^{m,n}_k ( x_1 , \dots , x_m ; x_{m+1} , \dots, x_{m+n} )  := x_k$ for $n,m \in \Word$ and $1 \leq k \leq m+n$.

		\item The successor functions $\succ_i ( ; x) := xi$ for $i = 0,1$.

		\item The predecessor function $\pred (; x) := \begin{cases}

		\epsilon &  \mbox{ if }  x = \epsilon \\

		x' &  \mbox{ if }  x = x'i

		\end{cases}$.

		\item The conditional function 

		\[

		%\begin{array}{rcl}

		%C (; \epsilon, y_\epsilon , y_0, y_1  ) & = & y_\epsilon \\

		%C(; x0 , y_\epsilon , y_0, y_1) & = & y_0 \\

		%C(; x1 , y_\epsilon , y_0, y_1) & = & y_1 

		%\end{array}

		C (; \epsilon, y_\epsilon , y_0, y_1  ) := y_\epsilon 

		\quad

		C(; x0 , y_\epsilon , y_0, y_1) := y_0 

		\quad

		C(; x1 , y_\epsilon , y_0, y_1) := y_1 

		\]

		%		$\cond (;x,y,z) := \begin{cases}

		%		y & \mbox{ if } x=x' 0 \\

		%		z & \text{otherwise}

		%		\end{cases}$.

	\end{enumerate}

	%	One considers the following closure schemes:

	\begin{enumerate}

		\setcounter{enumi}{5}

		\item Predicative recursion on notation (PRN). If $g, h_0, h_1 $ are in BC then so is $f$ defined by,

		\[

		\begin{array}{rcl}

		f(0, \vec v ; \vec x) & := & g(\vec v ; \vec x) \\

		f (\succ_i u , \vec v ; \vec x ) & := & h_i ( u , \vec v ; \vec x , f (u , \vec v ; \vec x) )

		\end{array}

		\]

		for $i = 0,1$,  so long as the expressions are well-formed. % (i.e.\ in number/sort of arguments).

		\item Safe composition. If $g, \vec h, \vec h'$ are in BC then so is $f$ defined by,

		\[

		f (\vec u ; \vec x) \quad := \quad g ( \vec h(\vec u ; ) ; \vec h' (\vec u ; \vec x) )

		\]

		so long as the expression is well-formed.

	\end{enumerate}

\end{definition}

%Note that the  programs of this class can be defined by equational specifications in a natural way, and in the following we will thus silently identify a BC program with the corresponding equational specification.

We will implicitly identify a BC function with the equational specification it induces.

The main property of BC programs is:

\begin{theorem}[\cite{BellantoniCook92}]

	The class of functions representable by BC programs is $\fptime$.

\end{theorem}	

Actually this property remains true if one replaces the PRN scheme by the following more general simultaneous PRN scheme \cite{BellantoniThesis}:

$(f^j)_{1\leq j\leq n}$ are defined by simultaneous PRN scheme  from $(g^j)_{1\leq j\leq n}$, $(h^j_0, h^j_1)_{1\leq j\leq n}$ if for $1\leq j\leq n$ we have:

\[

\begin{array}{rcl}

f^j(0, \vec v ; \vec x) & := & g^j(\vec v ; \vec x) \\

f^j(\succ_i u , \vec v ; \vec x ) & := & h^j_i ( u , \vec v ; \vec x , \vec{f} (u , \vec v ; \vec x) )

\end{array}

\]

for $i = 0,1$,  so long as the expressions are well-formed.

%\anupam{simultaneous recursion?}

%\anupam{also identity, hereditarily safe, expressions, etc.}

%\anupam{we implicitly associate a BC program with its equational specification} 

Consider a well-formed expression $t$ built from function symbols and variables. We say that a variable $y$ occurs \textit{hereditarily safe} in $t$ if, for every subexpression $f(\vec{r}; \vec{s})$ of $t$, the terms in $\vec{r}$ do not contain $y$.

For instance $y$ occurs hereditarily safe in $f(u;y,g(v;y))$, but not in $f(g(v;y);x)$.

\begin{proposition}

	[Properties of BC programs]

	\label{prop:bc-properties}

	We have the following properties:

	\begin{enumerate}

		\item The identity function is in BC.

		\item Let $t$ be a well-formed expression built from BC functions and variables, denote its free variables as $\{u_1,\dots, u_n,x_1,\dots, x_k\}$, and assume for each $1\leq i\leq k$, $x_i$ is hereditarily safe in $t$. Then the function $f(u_1,\dots, u_n; x_1,\dots, x_k):=t$ is in BC.

		\item If $f$ is a BC function, then the function $g(\vec{u},v;\vec{x})$ defined as $f(\vec{u};v,\vec{x})$

		is also a BC program.

	\end{enumerate}

	%\begin{proposition}

	%[Properties of BC programs]

	%\label{prop:bc-properties}

	%We have the following properties:

	%\begin{enumerate}

	%\item Hereditarily safe expressions over BC programs are BC definable.

	%\item Can pass safe input to normal input.

	%\end{enumerate}

\end{proposition}

\nb{TODO: extend with $\mu$s.}