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