Index: preliminaries.tex
===================================================================
--- preliminaries.tex	(revision 219)
+++ preliminaries.tex	(revision 220)
@@ -1,9 +1,9 @@
 
 \section{Preliminaries}
 \label{sect:prelims}
-We introduce the polynomial hierarchy and its basic properties, then the Bellantoni characterisation.
+We introduce the polynomial hierarchy and its basic properties, then Bellantoni's characterisation of it based on safe recursion and minimization \cite{bellantoni1995fph}.
 
-\anupam{Should recall polymax bounded functions and the polychecking lemma, e.g.\ from Bellantoni's FPH paper or thesis. Quite important, even if proof not given.}
+%\anupam{Should recall polymax bounded functions and the polychecking lemma, e.g.\ from Bellantoni's FPH paper or thesis. Quite important, even if proof not given.}
 
 \subsection{Polynomial hierarchy}
 %(include closure properties)
@@ -23,65 +23,66 @@
 polynomial time Turing machine with oracle $L$.
 
 We now define the following function classes:
-\begin{eqnarray*}
+\[
+\begin{array}{lcl}
  \fphi{i+1} &:= & \fptime(\sigp{i}),\\
  \fph &:=& \cup_i  \fphi{i}. 
-\end{eqnarray*}
-One can then check that $ \fphi{i+1} =  \fptime(\pip{i})=  \fptime(\sigp{i}\cup \pip{i})$.
+\end{array}
+\]
+Notice that $ \fphi{i+1} =  \fptime(\pip{i})=  \fptime(\sigp{i}\cup \pip{i})$.
 
-\subsection{Bellantoni's characterisation using predicative minimisation}
-(perhaps compare with Cobham's using limited recursion)
+\subsection{Bellantoni-Cook characterisation of $\fptime$ using predicative recursion}
+%(perhaps compare with Cobham's using limited recursion)
+%
+%\anupam{copied below from last year's paper}
 
-\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 soundness and completeness results later on. 
 
-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}. 
+We consider functions $f$ over the domain $\Nat$ 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:
+	[$\bc$ programs]
+	$\bc$ contains the following initial functions:
 	%	\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 constant functions $0 (\vec u ; \vec x) \dfn 0$, for each $|\vec u|$ and $| \vec x|$.
+		\item The projection functions $\pi^{m,n}_k ( a_1 , \dots , a_m ; a_{m+1} , \dots, a_{m+n} )  := a_k$ for $1 \leq k \leq m+n$.
+		\item The successor functions $\succ i ( ; x) \dfn 2x +i$ for $i = 0,1$.
+		\item The predecessor function $\pred (; x) \dfn \hlf{x}$.
 		\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}$.
+		\(
+		\cond(;x,y,z)
+		 \dfn 
+		\begin{cases}
+		y & x = 0\  \mathrm{mod}\  2 \\
+		z & x = 1\  \mathrm{mod}\  2
+		\end{cases}
+		\)
 	\end{enumerate}
 	
-	%	One considers the following closure schemes:
+	\medskip
+	\noindent
+$\bc$ is closed under the following operations:
+
+
+
 	\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) )
+		\begin{array}{rcll}
+		f(0, \vec v ; \vec x) & := & g(\vec v ; \vec x) & \\
+		f (\succ 0 u , \vec v ; \vec x ) & := & h_0 ( u , \vec v ; \vec x , f (u , \vec v ; \vec x) ) & \text{when $u \neq 0$} \\
+		f (\succ 1 u , \vec v ; \vec x ) & := & h_1 ( 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).
+		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) )
@@ -91,21 +92,22 @@
 \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:
+We will refer to the expressions or terms built up from the rules above as `$\bc$-programs', although we consider $\bc$ itself to be an algebra of functions.
+The main property of $\bc$ is:
 \begin{theorem}[\cite{BellantoniCook92}]
-	The class of functions representable by BC programs is $\fptime$.
+	$\bc =\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.
+%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?}
 
@@ -116,14 +118,14 @@
 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]
+	[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.
+		\item The identity function is in $\bc$.
+		\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 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$ program, 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}
@@ -147,7 +149,7 @@
 %	\todo{$\bit$}
 Observe that:
 	\begin{itemize}
-	\item The boolean predicates $\notfn (;x)$,  $\andfn(;x,y)$, $\orfn(;x,y)$, $\equivfn(;x,y)$ can all be defined on safe arguments, simply by computing by case distinction using the conditional $C(;x,y_{\epsilon}, y_0,y_1)$ function.
+	\item The boolean predicates $\notfn (;x)$,  $\andfn(;x,y)$, $\orfn(;x,y)$, $\equivfn(;x,y)$ can all be defined on safe arguments, simply by computing by case distinction using the conditional function.
 	%\item $\bit(l;x)$ returns the $\mode l$th bit of $x$.
 	\item We can define the function $\bit(l;x)$ which returns the $|l|$th least significant bit of $x$. For instance $\bit(11;1010)=0$.
 	
@@ -164,34 +166,41 @@
 
 %\nb{Remember polymax bounded checking lemma! Quite important. Also need to bear this in mind when adding functions.}
 
-Now, in order to characterize $\fph$ and its subclasses $\fphi{i}$ we consider Bellantoni's function algebra $\mubc$, defined by using predicative minimization: 
+\subsection{Bellantoni's characterisation of $\fphi{i}$ using predicative minimization}
+
+Now, in order to characterize $\fph$ and its subclasses $\fphi{i}$ we consider Bellantoni's function algebra $\mubc$, extending $\bc$ by predicative minimization: 
 \begin{definition}[$\mubc$ and $\mubc^i$ programs]
-We define:
-\begin{itemize}
-\item The class $\mubc$ is the set of functions defined as the BC functions, but with the following additional generation rule:
+The algebra $\mubc$ is generated from $\bc$ by the following additional operation:
 
-8. Predicative minimization. If $h$ is in $\mubc$, then so is $f$ defined by
+\begin{enumerate}
+			\setcounter{enumi}{7}
+	\item Predicative minimization. If $h$ is in $\mubc$, then so is $f$ defined by
+	$$f(\vec u; \vec x):= \begin{cases}
+	s_1 \mu y.(h(\vec u; \vec x, y)\mod 2 = 0)& \mbox{ if  there exists such a $y$,} \\
+	0  & \mbox{ otherwise,}
+	\end{cases}
+	$$
+\end{enumerate}
+where $\mu y.(h(\vec u; \vec x , y)\mod 2 = 0)$ is the least $y$ such that the equality holds.
+%We will denote this function $f$ as $\mu y^{+1} . h(\vec u ; \vec x , y) =_2 0$.
 
-$f(\vec u; \vec x):= \begin{cases}
- s_1(\mu y.h(\vec u; \vec x, y)\mod 2 = 0)& \mbox{ if  there exists such a $y$,} \\
-0  & \mbox{ otherwise,}
-\end{cases}
-$
+ For each $i\geq 0$, $\mubc^i$ is the set of $\mubc$ functions obtained by at most $i$ applications of predicative minimization.\footnote{This is the number of nestings of $\mu$ in a $\mubc$ program.} So $\mubc^0=BC$ and $\mubc =\cup_i \mubc^i$.
 
-where $\mu y.h(\vec u; \vec x , y)\mod 2 = 0$ is the least $y$ such that the equality holds.
+ \end{definition}
+ 
 
-We will denote this function $f$ as $\mu y^{+1} . h(\vec u ; \vec x , y) =_2 0$.
 
-If $\Phi$ is a class of functions, we denote by $\mubc(\Phi)$ the class obtained as $\mubc$ but adding $\Phi$ to the set of initial functions.
- 
-\item For each $i\geq 0$, $\mubc^i$ is the set of $\mubc$ functions obtained by at most $i$ applications of predicative minimization. So $\mubc^0=BC$ and $\mubc =\cup_i \mubc^i$.
-\end{itemize}
- \end{definition}
- One then obtains:
  \begin{theorem}[\cite{BellantoniThesis, Bellantoni95}]\label{thm:mubc}
- The class of functions representable by $\mubc$ programs is $\fph$, and for each $i\geq 1$ the class representable by $\mubc^{i-1}$ programs is $\fphi{i}$.
+$\mubc =\fph$. Furthermore, for $i\geq 1$, $\mubc^{i-1} = \fphi{i}$.
  \end{theorem}
- We will also need an intermediary lemma, also proved in \cite{BellantoniThesis}.
+
+
+\medskip 
+\noindent
+\textbf{Some computational properties of $\mubc$ programs.}
+  	We will need some bounds for $\mubc$ functions that we use later on;
+  	all of this material is from \cite{bellantoni1995fph}.
+  	
  \begin{definition}
   A function $f(\vec u; \vec x)$ is \textit{polymax bounded} if there exists a polynomial $q$ such that,
   for any $\vec u$ and $\vec x$ one has:
@@ -213,7 +222,9 @@
 If  $f(\vec u; \vec x,y)$ is a polynomial checking function on $\vec u$ and $q$ is a threshold, then for any $\vec u$ and $\vec x$ we have:
 $$ (\exists y.   f(\vec u; \vec x,y)\mbox{ mod } 2=0) \Rightarrow (\exists y.  (\size{y}\leq q(\size{\vec{x}})+2) \mbox{ and } f(\vec u; \vec x,y) \mbox{ mod } 2=0) .$$
  \end{lemma}
- Finally we can state an important lemma about $\mubc$:
+ 
+ Finally we can state an important lemma about $\mubc$.
+  If $\Phi$ is a class of functions, we denote by $\mubc(\Phi)$ the class obtained as $\mubc$ but adding $\Phi$ to the set of initial functions.
  \begin{lemma}[Polychecking Lemma, \cite{BellantoniThesis}]
  	\label{lem:polychecking}
  Let $\Phi$ be a class of polymax bounded polynomial checking functions. If $f(\vec u; \vec x)$ is in $\mubc(\Phi)$, then $f$ is  a polymax bounded function  polynomial checking function on $\vec u$.
@@ -222,7 +233,72 @@
  \begin{proposition}
   If $\Phi$ is a class of polymax bounded polynomial checking functions, then  $\mubc(\Phi)$ satisfies the properties of Thm \ref{thm:mubc}.
  \end{proposition}
+ 
+ \subsection{Some properties and extensions of $\bc$ and $\mubc$}
+ 
+ \anupam{done a pass up to here. Resuming at next section.}
+ 
   Consider the addition function $+$ with two safe arguments, so denoted as $+(;x,y)$. It is clear that if $+(;x,y)=z$, then we have $|z| \leq \max(|x|,|y|)+1$, so $+$ is a polymax bounded function. Moreover for any $n$, the $n$th least significant bits of $z$ only depend on the $n$th least significant bits  of $x$ and $y$, so $+(;x,y)$ is a polynomial checking function (on no normal argument), with threshold $q(x,y)=0$.
   
   In the following we will consider $\mubc(\Phi)$ with $\Phi$ containing the function $+(;x,y)$, but write it simply as $\mubc$. Note that addition could be defined in $\bc$ (hence in $\mubc$), but not with two safe arguments because the definition would use safe recursion. We will also use the unary successor $\succ{} (;x)$, which is defined thanks to addition as  as $\succ{} (;x)=+(;x,\succ 1 0)$.
-  
\ No newline at end of file
+  
+  \anupam{also add $\#$ and $|\cdot|$, for simplicity.}
+  
+  \begin{lemma}
+  	[Sharply bounded lemma]
+  	\label{lem:sharply-bounded-recursion}
+  	Let $f_A$ be the characteristic function of a predicate $A(u , \vec u ; \vec x)$.
+  	Then the characteristic functions of $\forall u \prefix v . A(u,\vec u ; \vec x)$ and $\exists u \prefix v . A(u , \vec u ; \vec x)$ are in $\bc(f_A)$.
+  \end{lemma}
+  \begin{proof}
+  	We give the $\forall$ case, the $\exists$ case being dual.
+  	The characteristic function $f(v , \vec u ; \vec x)$ is defined by predicative recursion on $v$ as:
+  	\[
+  	\begin{array}{rcl}
+  	f(0, \vec u ; \vec x) & \dfn & f_A (0 , \vec u ; \vec x) \\
+  	f(\succ i v , \vec u ; \vec x) & \dfn & \cond ( ; f_A (\succ i v, \vec u ; \vec x) , 0 , f(v , \vec u ; \vec x) )
+  	\end{array}
+  	\]
+  \end{proof}
+  
+\medskip
+\noindent
+\textbf{Encoding of sequences.}
+  Assume the existence of a simple pairing function for elements of fixed size: $\pair{k,l}{x}{y}$ denotes the pair $(x \mode k , y \mode l )$.
+  An appropriate such function would `interleave' $x$ and $y$, adding delimiters as necessary.
+  We assume that $|\pair{k,l}{x}{y}| = k+O(l)$ and $\pair{k,l}{x}{y}$ satisfies the polychecking lemma.
+  
+  We will simply write $\pair{l}{x}{y}$ for $\pair{l,l}{x}{y}$.
+  
+  \begin{lemma}
+  	[Creating sequences]
+  	\label{lem:sequence-creation}
+  	Given a function $f(u , \vec u ; \vec x)$ there is a $\bc(f)$ function $F(l, u , \vec u ; \vec x)$ such that:
+  	\[
+  	F(l,u,\vec u ; \vec x)
+  	\quad = \quad
+  	\langle f(0, \vec u ; \vec x) \mode l , f(1, \vec u ; \vec x) \mode l , \dots , f(|u|, \vec u ; \vec x) \mode l \rangle
+  	\]
+  \end{lemma}
+  \begin{proof}
+  	We simply define $F$ by safe recursion from $f$:
+  	\[
+  	\begin{array}{rcl}
+  	F(l,0, \vec u ; \vec x) & \dfn & \langle ; f(0) \mode l \rangle \\
+  	F(l, \succ i u , \vec u ; \vec x ) & \dfn & \pair{O(|u| l) , l}{F(l, u , \vec u ; \vec x)}{f( |\succ i u| , \vec u ; \vec x )}
+  	\end{array}
+  	\]
+  	where the constants for $O(|u|l)$ are sufficiently large.
+  \end{proof}
+  
+  \begin{lemma}
+  	[Decoding sequences]
+  	We can define $\beta(l,i;x)$ as $(i\text{th element of x}) \mode l$.	
+  \end{lemma}
+  \begin{proof}
+  	First define $\beta (j,i;x)$ as $j$th bit of $i$th element of $x$, then use similar idea to above, by a recursion on $j$.
+  \end{proof}
+  
+  Notice that $\beta (l,i;x)$ satisfies the polychecking lemma.
+  
+  We define
\ No newline at end of file
