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. 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, thereby achieving a somewhat stronger result.

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}

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

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

%	We give some key cases in what follows.

	Suppose $f$ is defined by PRN as:

	\[

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

	\end{array}

	\]

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

	\begin{equation}

	\label{eqn:prn-cvg-base}

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

					}

				}

			}

	\end{equation}

	where $\alpha$ is,

	\[

	\vlderivation{

	%	\vliin{\cut}{}{ \word (\vec x) \seqar \word ( g (\vec v ; \vec x)) }{

	%		\vlin{\rigrul{!}}{}{\seqar !\word (v)}{

	%			\vlin{assump}{}{\seqar \word (\vec v)}{\vlhy{}}

	%			}

	%		}{

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

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

				}{

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

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

					}

				}

	%		}

		}

	\]

	and $\beta$ is:

	\[

	\vlderivation{

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

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

			}{

			\vliin{\cut}{}{ \word (g (\vec v ; \vec x) ) \seqar \word (f (\epsilon, \vec v ; \vec x) ) }{

				\vlin{\closure{\eqspec}}{}{ \seqar f(\epsilon , \vec v ; \vec x) = g(\vec v ; \vec x) }{\vlhy{}}

				}{

				\vlin{=}{}{\word ( g(\vec v ; \vec x) ) , f(\epsilon , \vec v ; \vec x) = g(\vec v ; \vec x)  \seqar \word (f (\epsilon, \vec v ; \vec x) ) }{\vlhy{}}

				}

			}

		}

	\]

%	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, for $i=0,1$, 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}}

	%					}

	%				}

	%			}

	%		}

	%	}

	%	}

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

				}

			}

			}

	}

	}

	}

\end{equation}

where $\alpha$ and $\beta$ are constructed similarly 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:

\[

\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{}{ !\word (\vec v) , \word (\vec x) \seqar \word ( f( \epsilon , \vec v ; \vec x ) ) }{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}

}

{

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

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

}

}

}

}

}

}

}

}

\]

where the steps \todo{minor steps}

%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

Suppose $f$ is defined by safe composition as follows:

\[

f( \vec u ; \vec x )

\quad = \quad

h( \vec g (\vec u ; )  ; \vec g' ( \vec u ; \vec x ) )

\]

By the inductive hypothesis we already have \eqref{eqn:prv-cvg-ih} for $h$ and each $g_i$ and $g_j'$ in place of $f$. We construct the required proof as follows:

\[

\vlderivation{

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

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

			\vliq{\cntr}{}{  !\word (\vec u) , \word (\vec x) \seqar \word ( h( \vec g(\vec u ;) ; \vec g' ( \vec u ; \vec x )  ) )  }{

				\vliiiq{\cut}{}{!\word (\vec u) , \dots ,  !\word (\vec u) , \word (\vec x) , \dots , \word (\vec x) \seqar \word ( h( \vec g(\vec u ;) ; \vec g' ( \vec u ; \vec x )  ) )   }{

					\vlhy{

						\left\{

						\vlderivation{

							\vlin{\rigrul{!}}{}{ !\word (\vec u) \seqar !\word ( g_i (\vec u ;) ) }{

								\vliq{\alpha}{}{ !\word (\vec u) \seqar \word ( g_i (\vec u ;) }{

									\vltr{\IH}{ \forall \vec u^{!\word} . \word (g_i (\vec u ;) ) }{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}

									}

								}

							}

						\right\}_{i \leq |\vec g| }

						}

					}{

					\vlhy{

						\left\{

						\vlderivation{

							\vliq{\alpha}{}{ !\word ( \vec u )  , \word (\vec x) \seqar \word  ( g_j' ( \vec u ; \vec x ) ) }{

								\vltr{\IH}{ \seqar \forall \vec u^{!\word}. \forall \vec x^\word . \word ( g_j' (\vec u ; \vec x) ) }{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}

								}

							}

						\right\}_{j \leq |\vec g'|}

						}

					}{

					\vliq{\alpha}{}{ !\word ( \vec g (\vec u ;) ) , \word ( \vec g ' ( \vec u ; \vec x ) ) \seqar \word ( h( \vec g(\vec u ;) ; \vec g' ( \vec u ; \vec x )  )  ) ) }{

						\vltr{\IH}{ \seqar \forall \vec v^{!\word} . \forall \vec y^\word . \word ( h( \vec v ; \vec y ) ) }{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}

						}

					}

				}

			}

		}

	}

\]

where $\alpha$ and $\beta$ are similar to before.

\todo{reformat a bit}

It remains to check the initial functions.

Consider the conditional function, 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:

\[

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

\todo{reformat a bit}

Other initial functions are far simpler.

\end{proof}