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

%\input{sequence-coding}

%\input{further}

%\input{pv-theories}	

\input{appendix-sequent-calculus}

Our base language consists of constant and function symbols $\{ 0, \succ{} , + , \times, \smsh , |\cdot|, \hlf{}.\}$ and predicate symbols 

 $\{\leq, \safe, \normal \}$. The function symbols are interpreted in the intuitive way, with $|x|$ denoting the length of $x$ seen as a binary string, and $\smash(x,y)$ denoting $2^{|x||y|}$, so a string of length $|x||y|+1$.

 We may write $\succ{0}(x)$ for $2\cdot x$, $\succ{1}(x)$ for $\succ{}(2\cdot x)$, and $\pred (x)$ for $\hlf{x}$, to better relate to the $\bc$ setting.

We consider formulas of classical first-order logic, over $\neg$, $\cand$, $\cor$, $\forall$, $\exists$, along with usual shorthands and abbreviations. 

%The formula $A \cimp B$ will be a notation for $\neg A \cor B$.

%We will also use as shorthand notations:

%$$ (s=t) = (s\leq t) \cand (t\leq s), \quad (s\neq t) = \neg(s=t).$$ 

\textit{Atomic formulas} formulas are of the form $(s\leq t)$, for terms $s,t$.

 We will assume, without loss of generality, that formulas are in \textit{De Morgan normal form}, that is to say that in formulas negation can only occur on atomic formulas, and that there is not any occurrence of a subformula of the form $\neg \neg A$.

 We write $\exists x^{N_i} . A$ or $\forall x^{N_i} . A$ for $\exists x . (N_i (x) \cand A)$ and $\forall x . (N_i (x) \cimp A)$ respectively.

The theories we introduce are directly inspired from bounded arithmetic, namely the theories $S^i_2$.

We include a similar set of axioms for direct comparison, although in our setting these are not minimal.

Indeed, $\#$ can be defined using induction in our setting.

The $\basic$ axioms of bounded arithmetic give the inductive definitions and interrelationships of the various function symbols.

It also states the fundamental algebraic properties, i.e.\ $(0,\succ{ } )$ is a free algebra, and, for us, it will also give us certain `typing' information for our function symbols based on their $\bc$ specification, with safe inputs ranging over $\safe$ and normal ones over $\normal$.

\begin{definition}

	[Basic theory]

	The theory $\basic$ consists of the axioms from Appendix \ref{appendix:arithmetic}.

	\end{definition}

 \[

 \begin{array}{l}

 \safe (0) \\

 \forall x^\safe . \safe (\succ{} x) \\

 \forall x^\safe . 0 \neq \succ{} (x) \\

 \forall x^\safe , y^\safe . (\succ{} x = \succ{} y \cimp x = y) \\

 \forall x^\safe . (x = 0 \cor \exists y^\safe.\  x = \succ{} y   )\\

 \forall x^\safe, y^\safe . \safe(x+y)\\

 \forall u^\normal, x^\safe . \safe(u\times x) \\

 \forall u^\normal , v^\normal . \safe (u \smsh v)\\

 \forall u^\normal \safe(u) \\

 \forall u^\safe \safe(\hlf{u})\\

 \forall u^\normal \safe(|x|)  

 \end{array}

 \]

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

\[

\begin{array}{lcl}

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

	[$\bc$ programs]

	$\bc$ contains the following initial functions:

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

		\(

		\cond(;x,y,z)

		 \dfn 

		\begin{cases}

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

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

		\end{cases}

		\)

	\medskip

	\noindent

$\bc$ is closed under the following operations:

		\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) ) & 

		so long as the expressions are well-formed. % (i.e.\ in number/sort of arguments).

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:

	$\bc =\fptime$.

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

	[Properties of $\bc$ programs]

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

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

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

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

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

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

 \end{definition}

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

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

 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.

 \subsection{Some properties and extensions of $\bc$ and $\mubc$}

 \anupam{done a pass up to here. Resuming at next section.}

  \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