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 programs defined by safe recursion on notation \cite{BellantoniCook92}. These will be employed for proving both the completeness   (all polynomial time functions are provably total) and the soundness result (all provably total functions are polynomial time) of our system. We consider function symbols $f$ over the domain  $\Word$ which have \textit{normal} and \textit{safe} arguments. 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 programs over $\Word$ generated by the following initial functions and closure schemes.

	%	\paragraph{Initial functions}

%	The initial functions are:

	\begin{enumerate}

		\item The constant function $\epsilon$ which takes no 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}

\]

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

Now, the main property of BC programs is

\begin{theorem}\cite{BellantoniCook92}

The class of functions representable by BC programs is the class 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, initial functions and variables. One says that a variable $y$ is \textit{hereditarily safe} in $t$ if  for every subexpression $f(\vec{r}; \vec{s})$ of $t$ the terms in $\vec{r}$ do not contain any occurrence of $y$.  For instance $y$ is 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 Let $t$ be a well-formed expression built from BC programs and variables, denote its free variables as $\{u_1,\dots, u_n,x_1,\dots, x_k\}$, and assume for for each $1\leq i\leq k$, $x_i$ is hereditarily safe in $t$. Then the function $f$ defined

by $f(u_1,\dots, u_n,x_1,\dots, x_k):=t$ is a BC program.

\item Assume $f$ is a BC program, then the program $g$ defined as

$$ g(\vec{u},v;\vec{x}):=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}