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

\section{Bellantoni-Cook characterisation of polynomial-time functions}

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 $\arith$. 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 $\FP$.

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