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

\documentclass{amsart}

\usepackage{amsthm}

	\usepackage{hyperref}

	\usepackage[dvipsnames]{xcolor}

\input{macros}

\begin{document}

	\section{Extending the basic BC framework}

\begin{itemize}

	\item 	Any polynomial-time predicate can be conservatively added to BC with only safe inputs.

	\item Thus all logical connectives $\neg, \vee, \wedge$ and equality testing $=$ can be implemented as programs with only safe arguments. 

	\item Can add G\"odel's $\beta$ functions with a safe input:

\end{itemize}	

\section{QPVBC}

\subsection{Bellantoni's system $\pvbci{}$}

\begin{definition}

	[Hierarchies]

	We define the following:

	\begin{itemize}

		\item $\fphi i$: $i$th level of functional polynomial hierarchy. I.e.\ $\Box_1$ = $\fptime$.

		\item $\mubci{i}$: $\mu$BC programs with $i-1$ nested $\mu$s, i.e., corresponds to $\fphi i$.

		\item $\pvbci i$: defined as $\pvbci{} + \Sigma^\sigma_i$-induction.

	\end{itemize}

\end{definition}

\begin{definition}

	[Provably total function]	

\end{definition}

\subsection{Extensions by induction principles}

\section{Soundness}

We show that provably total functions of $\pvbci i$ are in $\fphi i$.

The following is our main result:

\begin{theorem}

	If $\pvbci i \proves \forall \vec u^\normal , \vec x^\sigma . \exists \vec y^\sigma. A(\vec u , \vec x , \vec y)$, then there are $\mubci i $ programs $\vec f (\vec u ; \vec x)$ such that $\pvbci i \proves\forall \vec u^\normal , \vec x^\sigma . A(\vec u , \vec x , \vec f (\vec u ; \vec x) )  $.

\end{theorem}

\begin{definition}

	[Witness predicate]

	The \emph{witness predicate} is a $\mubci{}$ program $\wit{\vec a}{A}$, parametrised by variables $\vec a$ and a formula $A$ whose free variables are amongst $\vec a$, defined as follows.

	If $A$ is a $\Pi_{i}$ formula then:

	\[

		\begin{array}{rcl}

		\wit{\vec u; \vec x}{s=t} (\vec u ; \vec x, w) & \dfn & =(;s,t) \\

		\smallskip

				\wit{\vec u; \vec x}{s\neq t} (\vec u ; \vec x, w) & \dfn & \neg (;=(;s,t)) \\

				\smallskip

		\wit{\vec u ; \vec x}{A\cor B} (\vec u ; \vec x , w) & \dfn & \cor (; \wit{\vec u , \vec x}{A} (\vec u ; \vec x , w), \wit{\vec u , \vec x}{B} (\vec u ;\vec x, w) ) \\

		\smallskip

			\wit{\vec u ; \vec x}{A\cand B} (\vec u ; \vec x , w) & \dfn & \cand(; \wit{\vec u , \vec x}{A} (\vec u ; \vec x , w), \wit{\vec u , \vec x}{B} (\vec u ;\vec x, w) ) \\

			\smallskip

		\wit{\vec u ; \vec x}{\exists x^\safe . A(x)} (\vec u ;\vec x,  w) & \dfn & \begin{cases}

		1 & \exists x^\safe . \wit{\vec u; \vec x, x }{A(x)} (\vec u ;\vec x , x, w) = 1 \\

		0 & \text{otherwise} 

		\end{cases} \\

		\smallskip

		\wit{\vec u; \vec x}{\forall x^\safe . A(x)} (\vec u ;\vec x , w) & \dfn & 

		\begin{cases}

		0 & \exists x^\sigma. \wit{\vec u ; \vec x , x}{ A(x)} (\vec u; \vec x , x) = 0 \\

		1 & \text{otherwise}

		\end{cases}

		\end{array}

	\]

	We now define $\Wit{\vec a}{A}$ for a $\Sigma_{i+1}$-formula $A$ with free variables amongst $\vec a$.

	\[

	\begin{array}{rcl}

	\Wit{\vec u ; \vec x}{A} (\vec u ; \vec x , w) & \dfn & \wit{\vec u ; \vec x}{A} (\vec u ; \vec x)  \text{ if $A$ is $\Pi_i$} \\

	\smallskip

	\Wit{\vec u ; \vec x}{A \cor B} (\vec u ; \vec x , \vec w^A , \vec w^B) & \dfn & \cor ( ; \Wit{\vec u ; \vec x}{A} (\vec u ; \vec x , \vec w^A) ,\Wit{\vec u ; \vec x}{B} (\vec u ; \vec x , \vec w^B)  )  \\

	\smallskip

		\Wit{\vec u ; \vec x}{A \cand B} (\vec u ; \vec x , \vec w^A , \vec w^B) & \dfn & \cand ( ; \Wit{\vec u ; \vec x}{A} (\vec u ; \vec x , \vec w^A) ,\Wit{\vec u ; \vec x}{B} (\vec u ; \vec x , \vec w^B)  )  \\

	\smallskip

	\Wit{\vec u ; \vec x}{\exists x^\safe . A(x)} (\vec u ; \vec x , \vec w , w) & \dfn & \Wit{\vec u ; \vec x , x}{A(x)} ( \vec u ; \vec x , w , \vec w )

	\end{array}

	\]

\end{definition}

\nb{use (de)pairing to make sure only $i$ $\mu$s are used to express a $\Pi_i$ predicate.}

\begin{proposition}

	For $\Sigma_{i+1}$ formulae $A$, $\Wit{\vec u ; \vec x}{A}$ is a $\mubci{i} $ program.

\end{proposition}

Before proving the main theorem, we will need the following `witnessing lemma':

\begin{lemma}

	If $\pvbci{i+1} $ proves a $\Sigma^\safe_{i+1}$-sequent $\Gamma \seqar \Delta$ with free variables $\vec u^\normal , \vec x^\safe$ then there are $\mubci {i}$ functions $\vec f$ such that 

	\[

	\pvbci {i+1} \proves \Wit{\vec u , \vec x}{\bigwedge \Gamma} (\vec u ; \vec x , \vec w) \cimp \Wit{\vec u  , \vec x}{\bigvee \Delta } (\vec u ; \vec x, \vec f (\vec u ; \vec x , \vec w) )

	\]

	(we simply write $\Wit{\vec u ; \vec x}{A}(\vec u ; \vec x , \vec w)$, instead of $\Wit{\vec u ; \vec x}{A}(\vec u ; \vec x , \vec w) =1 $.

\end{lemma}

\begin{proof}

	By induction on the size of a $\pvbci{i+1} $ proof. 

	Interesting steps below:

	\begin{itemize}

		\item $\neg$-right. (Can assume only applies to atomic formulae, and so no effect.)

		\item $\exists$-right.

		\[

		\dfrac{\Gamma \seqar \Delta , A(t^\safe )}{ \Gamma \seqar \Delta, \exists x^\safe . A(x) }

		\]

		By the inductive hypothesis, have functions $\vec f(\vec u ; \vec x), \vec g (\vec u ; \vec x)$ such that,

		\[

		\pvbci{i+1} \proves 

		\Wit{\vec u ; \vec x}{\bigwedge \Gamma } (\vec u ; \vec x , \vec w)

		\cimp

		\left(

		\Wit{\vec u ; \vec x}{\bigvee \Delta} (\vec u ; \vec x , \vec f (\vec u ; \vec x , \vec w) )

		\cor

		\Wit{\vec u ; \vec x}{A(t)} (\vec u ; \vec x , \vec g (\vec u ; \vec x , \vec w))

		\right)

		\]

		(just use $t$ as one of the witness functions)

		\item $\forall$-right. (Must be a $\Pi_i$ formula, so forget witness and compute $\wit{}{}$)

		\item Contraction-right:

		\[

		\dfrac{\Gamma  \seqar \Delta , A ,A}{\Gamma \seqar \Delta, A}

		\]

		By infuctive hypothesis have functions $\vec f, \vec g^1 , \vec g^2$ such that:

		\[

		todo

		\]

		(just use conditional with a call to $\Wit{}{}$)

		\item induction

	\end{itemize}

\end{proof}

\section{Completeness}

Here we show that every $\mubci{i}$ function is definable in $\pvbci {i+1}$

\end{document}