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

\section{Preliminaries}

\label{sect:prelims}

We introduce the polynomial hierarchy and its basic properties, then Bellantoni's characterisation of it based on safe recursion and minimisation \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.}

\subsection{Polynomial hierarchy}

%(include closure properties)

\begin{definition}

Given $i\geq 0$, a  language $L$ belongs to the class $\sigp{i}$ if there exists a polynomial time predicate $A$ and a polynomial $q$ such that:

$$ x \in L \Leftrightarrow \exists y_1 \in \{0,1\}^{q(\size{x})}\forall y_2 \in \{0,1\}^{q(\size{x})}\dots Q_iy_i\in \{0,1\}^{q(\size{x})}\ A(x,y_1,\dots,y_i)=1$$

where $Q_i=\forall$ (resp. $Q_i=\exists$) if $i$ is even (resp. odd).

The class $\pip{i}$ is defined similarly but with first quantifier $\forall$ instead of $\exists$. 

\end{definition}

In particular: $\sigp{0}=\pip{0}=\ptime$, $\sigp{1}=\np$, $\pip{1}=\conp$. Note that for any $i$ we have $\pip{i}=\mathbf{co}\sigp{i}$ and $\sigp{i}\subseteq \pip{i+1}$,  $\pip{i}\subseteq \sigp{i+1}$.

The polynomial hierarchy is defined as $\ph:=\cup_i \sigp{i}$, and we also have $\ph=\cup_i \pip{i}$.

Given a language $L$ we denote as $\fptime(L)$ the class of functions computable by a deterministic

polynomial time Turing machine with oracle $L$.

We now define the following function classes:

\[

\begin{array}{lcl}

 \fphi{i+1} &:= & \fptime(\sigp{i}),\\

 \fph &:=& \cup_i  \fphi{i}. 

\end{array}

\]

Notice that $ \fphi{i+1} =  \fptime(\pip{i})=  \fptime(\sigp{i}\cup \pip{i})$.

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

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 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$ contains the following initial functions:

	%	\paragraph{Initial functions}

	%	The initial functions are:

	\begin{enumerate}

		\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 

		\(

		\cond(;x,y,z)

		 \dfn 

		\begin{cases}

		y & x = 0\  \mathrm{mod}\  2 \\

		z & x = 1\  \mathrm{mod}\  2

		\end{cases}

		\)

	\end{enumerate}

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

		\]

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

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

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

	%[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.}

%\anupam{Should add $+(;x,y)$ as a basic function (check satisfies polychecking lemma!), since otherwise not definable with safe input. Then define unary successor $\succ{} (;x)$ as $+(;x,\succ 1 0)$. }

\begin{example}

	[Some simple functions]

	\label{ex:simple-bc-fns}

%	\todo{Boolean predicates $\notfn, \andfn, \orfn, \equivfn$ .}

%	\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 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;1101)=0$.

	For that let us first define the function $\shorten(l;x)$ which returns the $|x|- |l|+1$ prefix of $x$, as follows:

	\begin{eqnarray*}

	\shorten(0;x) &=&x\\

	\shorten(\succ{i}l;x) &=&p(;\shorten(l;x))

	\end{eqnarray*}

	Then we define $\bit(l;x)$  as follows:

	$$\bit(l;x)=C(;\shorten(l;x),0,1).$$ 

	\end{itemize}

	\end{example}

%\nb{Remember polymax bounded checking lemma! Quite important. Also need to bear this in mind when adding functions.}

\subsection{Bellantoni's characterisation of $\fphi{i}$ using predicative minimisation}

Now, in order to characterize $\fph$ and its subclasses $\fphi{i}$ we consider Bellantoni's function algebra $\mubc$, extending $\bc$ by predicative minimisation: 

\begin{definition}[$\mubc$ and $\mubc^i$ programs]

The algebra $\mubc$ is generated from $\bc$ by the following additional operation:

\begin{enumerate}

			\setcounter{enumi}{7}

	\item Predicative minimisation. 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$.

 For each $i\geq 0$, $\mubc^i$ is the set of $\mubc$ functions obtained by at most $i$ applications of predicative minimisation.\footnote{This is the number of nestings of $\mu$ in a $\mubc$ program, written as a derivation tree or dag.} So $\mubc^0=\bc$ and $\mubc =\cup_i \mubc^i$.

 \end{definition}

Bellantoni showed the following result:

 \begin{theorem}[\cite{BellantoniThesis, Bellantoni95}]\label{thm:mubc}

$\mubc =\fph$. Furthermore, for $i\geq 1$, $\mubc^{i-1} = \fphi{i}$.

 \end{theorem}

In what follows we will recall some of the intermediate results and state a slightly stronger result that directly follows from \cite{bellantoni1995fph}.

%

%\medskip 

%\noindent

%\textbf{Some computational properties of $\mubc$ programs.}

  	At the same time these results give us access to bounds for $\mubc$ functions that we use later on.

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

%$\size{u}$

  $$ \size{f(\vec u; \vec x)} \leq q(\size{u_1} , \dots , \size{u_k}) + \max_j \size{x_j}.$$

 \end{definition}

 We define the function $\mode$ by $u\mode x:= u \mod 2^{\size{x}}$. Note that this means that as a binary string $u\mode x$ is the suffix of $u$ of length $\size{x}$.

 \begin{definition}

 A function $f(\vec u; \vec x)$ is a \textit{polynomial checking function} on $\vec u$ if there exists a polynomial $q$

 such that, for any $\vec u$, $\vec x$, $y$ and $z$ such that $\size{y} \geq q(\size{\vec u})+ \size{z}$ we have:

 $$ f(\vec u; \vec x) \mode z = f(\vec u; \vec x \mode y)\mode z.$$

 A polynomial $q$ satisfying this condition is called a \textit{threshold} for $f$.

 \end{definition}

 One then has:

 \begin{lemma}[Bounded minimisation, \cite{BellantoniThesis}]

 	\label{lem:bounded-minimisation}

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

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

 \end{lemma}

In particular, we also have the following strengthening of Thm.~\ref{thm:mubc},

 following from \cite{BellantoniThesis, Bellantoni95}.

 \begin{theorem}

 	\label{thm:mubc-phi}

  If $\Phi$ is a class of polymax bounded polynomial checking functions, then  $\mubci {i-1} (\Phi) = \fphi i$.

 \end{theorem}

% 

 \subsection{Some properties and extensions of $\bc$ and $\mubc$}\label{sect:somepropertiesofmubc}

We will state some results here that we rely on in the later sections.

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

  Thus, we will freely add $+(;x,y)$ to the $\mubc $ framework, under Thm.~\ref{thm:mubc-phi}, and define unary successor $\succ{} (;x) \dfn +(;x, \succ 1 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)$.

%  

In the same way, although for more simple reasons, we may add the functions $\#$ and $|\cdot|$ that we introduce later in Sect.~\ref{sect:arithmetic} to $\mubc$ containing only normal arguments since they are polynomial-time computable.

  One important closure property we will need for $\mubc $ functions, namely to define `witness functions' later on, is the following:

  \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 \leq |v| . A(u,\vec u ; \vec x)$ and $\exists u \leq |v| . A(u , \vec u ; \vec x)$ are in $\bc(f_A)$.

  \end{lemma}

  \begin{proof}

  	For the $\forall$ case, we define the characteristic function $f(v , \vec u ; \vec x)$ 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}

  	\]

  	The $\exists$ case is similar.

  \end{proof}

Finally, we will briefly outline some basic functions for (de)coding sequences. The functions we introduce here will in fact be representable in the theory $\arith^1$ that we introduce in the next section, which, along with proofs of their basic properties, will be important for the completeness result in Sect.~\ref{sect:completeness}.

  We assume the existence of a simple pairing function in $\bc$ for elements of fixed size: $\pair{k,l}{x}{y}$ identifies 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}

  	[Coding 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 \cdots \langle f(0, \vec u ; \vec x) \mode l , f(1, \vec u ; \vec x) \mode l \rangle , \cdots , 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{p(u l) , l}{F(l, u , \vec u ; \vec x)}{f( |\succ i u| , \vec u ; \vec x )}

  	\end{array}

  	\]

  	where $p(u l)$ is a sufficiently large polynomial.

  \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}[Proof sketch]

  	First define $\beta (j,i;x)$ as $|j|$th bit of $|i|$th element of $x$, of the form $\bit(p(i,j) ; x)$ for some quasipolynomial $p$,\footnote{A quasipolynomial is just a polynomial that may contain $\smsh$.} then use similar idea to the proof above, concatenating the bits of the $i$th element by a recursion on $j$.

  \end{proof}

  %Notice that $\beta (l,i;x)$ satisfies the polychecking lemma.