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

\section{Convergence of Bellantoni-Cook programs in $\arith$}

\label{sect:bc-convergence}

%\anupam{In this section, use whatever form of the deduction theorem is necessary and reverse engineer precise statement later.}

In this section we show that $I\sigzer$, and so also $\arith$, proves the convergence of any equational specification induced by a BC program, hence any function in $\FP$.

%Since BC programs can compute any polynomial-time function, we obtain a completeness result. In the next section we will show the converse, that any provably convergent function of $\arith$ is polynomial-time computable.

%

The underlying construction of the proof here is similar in spirit to those occurring in \cite{Cantini02} and \cite{Leivant94:found-delin-ptime}. In fact, like in those works, only quantifier-free positive induction is required, but here we moreover must take care to respect additive and multiplicative behaviour of linear connectives.

We will assume the formulation of BC programs with regular PRN, not simultaneous PRN.

%\subsection{Convergence in arithmetic}

%\begin{theorem}

%	[Convergence]

%	If $\Phi(f)$ is an equational specification corresponding to a BC-program defining $f$, then $\cax{\Sigma^N_1}{\pind} \proves  \ !\Phi(f) \limp \forall \vec{x}^{!N} . N(f(\vec x))$.

%\end{theorem}

%We first want to show that the system ${\Sigma^{\word}_1}-{\pind}$ is expressive enough, that is to say that all polynomial-time functions can be represented by some equational specifications that are provably total. To do so   we consider equational specifications of BC-programs.

\begin{theorem}

%	[Convergence]

\label{thm:arith-proves-bc-conv}

	If $\eqspec$ is a BC program defining a function $f$, then $I\sigzer$ proves $\conv(f, \eqspec)$.

\end{theorem}

%\anupam{Consider informalising some of these arguments under (some version of) the deduction theorem. Formal stuff can be put in an appendix. Maybe add a remark somewhere about arguing informally under deduction, taking care for non-modalised formulae.}

\begin{proof}[Proof sketch]

%	We write function symbols in $\arith$ with arguments delimited by $;$, as for BC-programs.

	We appeal to Lemma~\ref{lemma:spec-norm-form} and show that $\closure{\eqspec} \cup I\sigzer$ proves $\forall \vec{u}^{!\word} . \forall \vec{x}^\word . \word(f(\vec u ; \vec x))$.

%	\begin{equation}

%	\label{eqn:prv-cvg-ih}

%\forall \vec{u}^{!\word} . \forall \vec{x}^\word . \word(f(\vec u ; \vec x))

%	\end{equation}

	We proceed by induction on the structure of a BC program for $f$, and sketch only the key cases here.

%	We give some key cases in what follows.

	Suppose $f(u, \vec v ; \vec x)$ is defined by PRN from functions $g(\vec v ; \vec x), h_i ( u , \vec v ; \vec x , y )$.

%	\[

%	\begin{array}{rcl}

%	f(\epsilon,\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}

%	\]

%	By the inductive hypothesis we have \eqref{eqn:prv-cvg-ih} for $g,h_0,h_1$ in place of $f$.

	From the inductive hypothesis for $g$, we construct the following proof,

	\begin{equation}

	\label{eqn:prn-cvg-base}

	\small

	\vlderivation{

			\vliq{\beta}{}{!\word(\vec v) , \word (\vec x) \seqar \word(f (\epsilon , \vec v ; \vec x)) }{

				\vliq{\alpha}{}{!\word (\vec v) , \word (\vec x) \seqar \word (g (\vec v ; \vec x) ) }{

%					\vltr{\IH}{\seqar \forall \vec v^{!\word} . \forall \vec x^\word . \word (g (\vec v ; \vec x)) }{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}

%				\vliq{}{}{\seqar \forall \vec v^{!\word} . \forall \vec x^\word . \word (g (\vec v ; \vec x))}{\vlhy{}}

\vlhy{\seqar \forall \vec v^{!\word} . \forall \vec x^\word . \word (g (\vec v ; \vec x))}

					}

				}

			}

	\end{equation}

 where $\alpha $ is purely logical and $\beta$ is obtained from $\closure{\eqspec}$ and equality.

%	We first prove,

%	\begin{equation}

%	!\word (a) , !\word (\vec v) , \word (\vec x) \land \word (f( a , \vec v ; \vec x ) )

%	\seqar

%	\word (\vec x) \land \word (f( \succ_i a , \vec v ; \vec x ) )

%	\end{equation}

%	for $i=0,1$, whence we will apply $\ind$. We construct the following proofs:

We also construct the proofs,

	\begin{equation}

	\label{eqn:prn-cvg-ind}

	%\vlderivation{

	%	\vlin{\rigrul{\limp}}{}{ \word(\vec x) \limp \word ( f(u, \vec v ; \vec x) )  \seqar \word (\vec x) \limp \word( f(\succ_i u , \vec v ; \vec x) ) }{

	%	\vliq{\gamma}{}{\word(\vec x), \word(\vec x) \limp \word ( f(u, \vec v ; \vec x) )  \seqar \word( f(\succ_i u , \vec v ; \vec x) )   }{

	%		\vliin{\lefrul{\limp}}{}{\word(\vec x), \word(\vec x), \word(\vec x) \limp \word ( f(u, \vec v ; \vec x) )  \seqar \word( f(\succ_i u , \vec v ; \vec x) )    }{

	%			\vlin{\id}{}{\word(\vec x) \seqar \word (\vec x) }{\vlhy{}}

	%			}{

	%			\vliq{\beta}{}{  \word (\vec x) , \word (f(u , \vec v ; \vec x) ) \seqar \word ( f(\succ_i u , \vec v ; \vec x) ) }{

	%				\vliq{\alpha}{}{ \word (\vec x) , \word (f(u , \vec v ; \vec x) ) \seqar \word ( h_i( u , \vec v ; \vec x , f( u, \vec v ; \vec x )) ) }{

	%					\vltr{IH}{ \seqar \forall  u^{!\word}, \vec v^{!\word} . \forall \vec x^\word , y^\word . \word( h_i (u, \vec v ; \vec x, y) ) }{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}

	%					}

	%				}

	%			}

	%		}

	%	}

	%	}

	\small

	\vlderivation{

	\vlin{\lefrul{\land}}{}{ !\word (a) , !\word (\vec v) , \word (\vec x) \land \word (f( a , \vec v ; \vec x ) ) \seqar \word (\vec x) \land \word (f( \succ_i a , \vec v ; \vec x ) ) }{

	\vlin{\lefrul{\cntr}}{}{  !\word (a) , !\word (\vec v) , \word (\vec x) , \word (f( a , \vec v ; \vec x ) ) \seqar \word (\vec x) \land \word (f( \succ_i a , \vec v ; \vec x ) )}{

	\vliin{\rigrul{\land}}{}{   !\word (a) , !\word (\vec v) , \word(\vec x),  \word (\vec x) , \word (f( a , \vec v ; \vec x ) ) \seqar \word (\vec x) \land \word (f( \succ_i a , \vec v ; \vec x ) )}{

	\vlin{\id}{}{\word (\vec x) \seqar \word (\vec x)}{\vlhy{}}

	}{

		\vliq{\beta}{}{ !\word (u) , !\word(\vec v)  , \word (\vec x) , \word (f ( u , \vec v ; \vec x ) ) \seqar \word (f (\succ_i u , \vec{v} ; \vec x ) )  }{

				\vliq{\alpha}{}{  !\word (u) , !\word (\vec v)  , \word (\vec x) , \word (f ( u , \vec v ; \vec x ) ) \seqar \word ( h_i ( u , \vec v ; \vec x , f( u , \vec v ; \vec x ) ) )   }{

%					\vltr{\IH}{ \seqar \forall u^{!\word} , \vec v^{!\word} . \forall \vec x^\word , y^\word  .  \word ( h_i ( u, \vec v ; \vec x, y ) ) }{ \vlhy{\quad} }{\vlhy{}}{\vlhy{\quad}}

%\vliq{}{}{ \seqar \forall u^{!\word} , \vec v^{!\word} . \forall \vec x^\word , y^\word  .  \word ( h_i ( u, \vec v ; \vec x, y ) ) }{\vlhy{}}

\vlhy{\seqar \forall u^{!\word} , \vec v^{!\word} . \forall \vec x^\word , y^\word  .  \word ( h_i ( u, \vec v ; \vec x, y ) )}

				}

			}

			}

	}

	}

	}

\end{equation}

	from the inductive hypotheses for $h_i$, where $\alpha$ and $\beta$ are similar to before.

%%	so let us suppose that $\word(\vec v)$ and prove,

%	\begin{equation}

%% \forall u^{!\word} .  (\word(\vec x) \limp \word(f(u , \vec v ; \vec x)  )

%!\word (u) , !\word (\vec v) , \word (\vec x) \seqar \word ( f(u, \vec v ; \vec x) )

%	\end{equation}

%	by $\cax{\Sigma^N_1}{\pind}$ on $u$. After this the result will follow by $\forall$-introduction for $u, \vec v , \vec x$.

%	In the base case we have the following proof,

%	\[

%	\vlderivation{

%	\vlin{\rigrul{\limp}}{}{ \seqar \word (\vec x) \limp \word (f(\epsilon , \vec v ; \vec x )) }{

%		\vliq{\beta}{}{ \word (\vec x) \seqar \word ( f( \epsilon , \vec v ; \vec x) ) }{

%			\vliq{\alpha}{}{ \word (\vec x) \seqar \word ( g (\vec v ; \vec x) ) }{

%				\vltr{IH}{\seqar \forall v^{!\word} . \forall x^\word . \word( g(\vec v ; \vec x) ) }{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}

%				}

%			}

%		}

%		}

Finally we compose these proofs as follows:

\[

\small

\vlderivation{

\vliq{\rigrul{\forall}}{}{ \seqar \forall u^{!\word} , \vec v^{!\word} . \forall \vec x^\word . \word ( f(u , \vec v ;\vec x)  ) }{

\vliq{\lefrul{\cntr}}{}{ !\word (u), !\word (\vec v) , \word (\vec x) \seqar  \word ( f(u , \vec v ;\vec x)  )  }

{

\vliin{\cut}{}{  !\word (u), !\word(\vec v), !\word (\vec v) , \word (\vec x) , \word (\vec x) \seqar  \word ( f(u , \vec v ;\vec x)  )   }{

%\vltr{\pi_\epsilon}{ !\word (\vec v) , \word (\vec x) \seqar \word ( f( \epsilon , \vec v ; \vec x ) ) }{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}

\vlhy{ !\word (\vec v) , \word (\vec x) \seqar \word ( f( \epsilon , \vec v ; \vec x ) ) }

}

{

\vliq{\wk}{}{ !\word (u), !\word (\vec v) , \word (\vec x), \word ( f( \epsilon , \vec v ; \vec x ) ) \seqar \word ( f( u , \vec v ; \vec x ) ) }{

\vliq{\land\text{-}\mathit{inv}}{}{  !\word (u), !\word (\vec v) , \word (\vec x) ,\word ( f( \epsilon , \vec v ; \vec x ) ) \seqar \word (\vec x) \land \word ( f( u , \vec v ; \vec x ) )  }{

\vlin{\ind}{}{   !\word (u), !\word (\vec v) , \word (\vec x) \land \word ( f( \epsilon , \vec v ; \vec x ) ) \seqar \word (\vec x) \land \word ( f( u , \vec v ; \vec x ) )  }

{

\vlhy{

\left\{

%\vltreeder{\pi_i}{   !\word (a), !\word (\vec v) , \word (\vec x) \word ( f( a , \vec v ; \vec x ) ) \seqar \word (\vec x) \land \word ( f( \succ_i u , \vec v ; \vec x ) )  }{\quad}{}{}

   !\word (a), !\word (\vec v) , \word (\vec x) \word ( f( a , \vec v ; \vec x ) ) \seqar \word (\vec x) \land \word ( f( \succ_i u , \vec v ; \vec x ) )

\right\}_i

}

}

}

}

}

}

}

}

\]

for $i=0,1$, where the steps $\inv{\land}$ are obtained from invertibility of $\lefrul{\land}$.

%For the inductive step, we suppose that $\word (u)$ and the proof is as follows,

%

%where the steps indicated $\alpha$ and $\beta$ are analogous to those for the base case.

%%, and $\gamma$ is an instance of the general scheme:

%%\begin{equation}

%%\label{eqn:nat-cntr-left-derivation}

%%\vlderivation{

%%	\vliin{\cut}{}{ \word (t) , \Gamma \seqar \Delta }{

%%		\vlin{\wordcntr}{}{ \word (t) \seqar \word (t) \land \word (t) }{\vlhy{}}

%%		}{

%%		\vlin{\lefrul{\land}}{}{\word (t)  \land \word (t) , \Gamma \seqar \Delta}{ \vlhy{\word (t)  ,\word (t) , \Gamma \seqar \Delta} }

%%		}

%%	}

%%\end{equation}

%

%%

%%For the inductive step, we need to show that,

%%\[

%%\forall x^{!N} . (( N(\vec y) \limp N( f(x, \vec x ; \vec y) ) ) \limp N(\vec y) \limp N(f(\succ_i x , \vec x ; \vec y) )   )

%%\]

%%so let us suppose that $N(x)$ and we give the following proof:

%%\[

%%\vlderivation{

%%	\vlin{N\cntr}{}{N(y) \limp ( N(y ) \limp N(f( x , \vec x ; \vec y ) ) ) \limp N(f (\succ_i x , \vec x ; \vec y)  ) }{

%%		\vliin{}{}{N(y) \limp N(y) \limp ( N(y ) \limp N(f( x , \vec x ; \vec y ) ) ) \limp N(f (\succ_i x , \vec x ; \vec y)  ) }{

%%			\vliin{}{}{ N(y) \limp N(y) \limp ( N(y) \limp N( f(x, \vec x ; \vec y) ) ) \limp N( h_i (x , \vec x ; \vec y , f(x , \vec x ; \vec y) ) ) }{

%%				\vltr{MLL}{( N(\vec y) \limp (N (\vec y) \limp N(f(x, \vec x ; \vec y) )) \limp N(f(x, \vec x ; \vec y)) }{\vlhy{\quad }}{\vlhy{\ }}{\vlhy{\quad }}

%%			}{

%%			\vlhy{2}

%%		}

%%	}{

%%	\vlhy{3}

%%}

%%}

%%}

%%\]

%%TOFINISH

Safe compositions are essentially handled by many cut steps, using $\alpha$ and $\beta$ like derivations again and, crucially, left-contractions on both $!\word$ and $\word $ formulae.\footnote{In the latter case, strictly speaking, we mean cuts against $\wordcntr$.} The initial functions are routine.

%We also give the case of the conditional initial function $C (; x, y_\epsilon , y_0, y_1)$, to exemplify the use of additives.

%%The conditional is defined equationally as:

%%\[

%%\begin{array}{rcl}

%%C (; \epsilon, y_\epsilon , y_0, y_1  ) & = & y_\epsilon \\

%%C(; \succ_0 x , y_\epsilon , y_0, y_1) & = & y_0 \\

%%C(; \succ_1 x , y_\epsilon , y_0, y_1) & = & y_1

%%\end{array}

%%\]

%Let $\vec y = ( y_\epsilon , y_0, y_1 )$ and construct the required proof as follows:

%\[

%\small

%\vlderivation{

%\vliq{}{}{ \word (x) , \word (\vec y) \seqar \word ( C(; x ,\vec y) )}{

%\vliin{2\cdot \laor}{}{ x = \epsilon \laor \exists z^\word . x = \succ_0 z \laor \exists z^\word x = \succ_1 z , \word (\vec y) \seqar \word ( C(;x \vec y) ) }{

%\vliq{}{}{ x = \epsilon , \word (\vec y) \seqar \word ( C(; x , \vec y) ) }{

%\vliq{}{}{ \word (\vec y) \seqar \word ( C( ; \epsilon , \vec y ) ) }{

%\vlin{\wk}{}{ \word (\vec y) \seqar \word (y_\epsilon) }{

%\vlin{\id}{}{\word (y_\epsilon) \seqar \word ( y_\epsilon )}{\vlhy{}}

%}

%}

%}

%}{

%\vlhy{

%\left\{

%\vlderivation{

%\vlin{\lefrul{\exists}}{}{ \exists z^\word . x = \succ_i z , \word (\vec y) \seqar \word ( C(;x , \vec y) ) }{

%\vliq{}{}{ x = \succ_i a , \word (\vec y ) \seqar \word (C(; x ,\vec y)) }{

%\vliq{}{}{ \word (\vec y) \seqar \word ( C(; \succ_i a , \vec y ) ) }{

%\vlin{\wk}{}{ \word (\vec y) \seqar \word (y_i) }{

%\vlin{\id}{}{\word (y_i) \seqar \word (y_i)}{\vlhy{}}

%}

%}

%}

%}

%}

%\right\}_{i = 0,1}

%}

%}

%}

%}

%\]

%whence the result follows by $\forall$-introduction.

%%The other initial functions are routine.

\end{proof}