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

\section{Witness function method}

\label{sect:wfm}

We now prove the converse to the last section: any provably convergent function in $\arith$ is polynomial-time computable,

%.

%To this end we use the \emph{witness function method} (WFM), a common technique in {bounded arithmetic} \cite{Buss86book}.

using the witness function method (WFM) \cite{Buss86book}.

The WFM differs from realisability and Dialectica style witnessing arguments mainly since it does not require functionals at higher type. Instead a translation is conducted directly from a proof in De Morgan normal form, i.e.\ with negation pushed to the atoms, relying on classical logic.

%Free-cut elimination is employed to control the quantifer complexity of formulae occurring in a proof, although here we furthermore use it to control the presence of \emph{contraction} in a proof, to which we have access via the modalities of linear logic. This

%Free-cut elimination is employed to control the logical complexity of formulae occurring in a proof, and a formal `witness' predicate plays a similar role to the realisability predicate.

The combination of De Morgan normalisation and free-cut elimination plays a similar role to the double-negation translation, and this is even more evident in our setting where the transformation of a classical proof to free-cut free form can be seen to be a partial `constructivisation' of the proof. As well as eliminating the (nonconstructive) occurrences of the $\forall$-right rule, as usual for the WFM, the linear logic refinement of the logical connectives means that right-contraction steps are also eliminated. This is important due to the fact that we are in a setting where programs are equational specifications, not formulae (as in bounded arithmetic \cite{Buss86book}) or combinatory terms (as in applicative theories \cite{Cantini02}), so we cannot in general decide atomic formulae.

%Some key features of this method are the following:

%\begin{itemize}

%	\item T

%\end{itemize}

%

%Key features/differences from realisability:

%\begin{itemize}

%	\item De Morgan normal form: reduces type level to $0$, complementary to double-negation translation that \emph{increases} type level.

%	\item Free-cut elimination: allows us to handles formulae of fixed logical complexity throughout the proof.

%	\item Respects logical properties of formulae, e.g.\ quantifier complexity, exponential complexity.

%\end{itemize}

%

%\todo{say some more here}

%

%\todo{compare with applicative theories}

%

%\anupam{in particular, need to point out that this argument is actually something in between, since usually the WFM requires programs to be defined by formulae, not equational specifications.}

\newcommand{\type}{\mathtt{t}}

\newcommand{\norm}{\nu}

\newcommand{\safe}{\sigma}

		\subsection{The translation}

We will associate to each (free-cut free) proof of a convergence statement in $\arith$ a function on $\Word$ defined by a BC program. In the next section we will show that this function satisfies the equational specification of the convergence statement.

%, hence showing that any provably convergent function of $\arith$ is polynomial-time computable.\footnote{Strictly speaking, we will also require the equational specification at hand to be coherent, cf.\ Prop.~\ref{prop:eq-spec-model}.}

		\begin{definition}

			[Typing]

			\label{dfn:typing}

			To each $(\forall, ?)$-free $\word^+$-formula $A$ we associate a sorted tuple of variables $\type (A)$, intended to range over $\Word$, as follows:

			\[

%			\begin{array}{rcll}

%			\type (\word (t)) & := & (;x^{\word (t)} ) & \\

%			\type(s = t) & := & ( ; x^{s = t}) & \\

%			\type (s \neq t) & := & ( ;x^{s\neq t} )\\

%%			\type (A \lor B)  & : = & (\vec u , \vec v ; \vec x , \vec y) & \text{if $\type(A) = (\vec u ; \vec x)$ and $\type(B) = (\vec v ; \vec y)$.} \\

%			\type (A \star B)  & : = & (\vec u , \vec v ; \vec x , \vec y) & \text{if $\type(A) = (\vec u ; \vec x)$, $\type(B) = (\vec v ; \vec y)$ and $\star \in \{ \lor, \land, \laor, \laand \}$.} \\

%			\type (! A) & : = & ( \vec u ,\vec x  ; ) & \text{if $\type(A) = (\vec u ; \vec x )$.} \\

%			\type (\exists x^\word . A) & := & (\vec u ; \vec x , y) & \text{if $\type (A) = (\vec u ; \vec x)$.}

%			%	\type (\forall x^N . A) & := & \Nat \to \type(A)

%			\end{array}

%

			\begin{array}{rcll}

			\type (\word (t)) & := & (;x^{\word (t)} ) & \\

			\type(s = t) & := & ( ; x^{s = t}) &

%			\\

%			\type (s \neq t) & := & ( ;x^{s\neq t} )\\

%%			\type (A \lor B)  & : = & (\vec u , \vec v ; \vec x , \vec y) & \text{if $\type(A) = (\vec u ; \vec x)$ and $\type(B) = (\vec v ; \vec y)$.} \\

%			\type (A \star B)  & : = & (\vec u , \vec v ; \vec x , \vec y) & \text{if $\type(A) = (\vec u ; \vec x)$, $\type(B) = (\vec v ; \vec y)$ and $\star \in \{ \lor, \land, \laor, \laand \}$.} \\

%			\type (! A) & : = & ( \vec u ,\vec x  ; ) & \text{if $\type(A) = (\vec u ; \vec x )$.} \\

%			\type (\exists x^\word . A) & := & (\vec u ; \vec x , y) & \text{if $\type (A) = (\vec u ; \vec x)$.}

%			%	\type (\forall x^N . A) & := & \Nat \to \type(A)

			\end{array}

			\quad

						\begin{array}{rcll}

%						\type (\word (t)) & := & (;x^{\word (t)} ) & \\

%						\type(s = t) & := & ( ; x^{s = t}) & \\

						\type (s \neq t) & := & ( ;x^{s\neq t} )\\

			%			\type (A \lor B)  & : = & (\vec u , \vec v ; \vec x , \vec y) & \text{if $\type(A) = (\vec u ; \vec x)$ and $\type(B) = (\vec v ; \vec y)$.} \\

%						\type (A \star B)  & : = & (\vec u , \vec v ; \vec x , \vec y) & \text{if $\type(A) = (\vec u ; \vec x)$, $\type(B) = (\vec v ; \vec y)$ and $\star \in \{ \lor, \land, \laor, \laand \}$.} \\

						\type (! A) & : = & ( \vec u ,\vec x  ; ) &

%						\text{if $\type(A) = (\vec u ; \vec x )$.} \\

%						\type (\exists x^\word . A) & := & (\vec u ; \vec x , y) & \text{if $\type (A) = (\vec u ; \vec x)$.}

%						%	\type (\forall x^N . A) & := & \Nat \to \type(A)

						\end{array}

						\quad

									\begin{array}{rcll}

%									\type (\word (t)) & := & (;x^{\word (t)} ) & \\

%									\type(s = t) & := & ( ; x^{s = t}) & \\

%									\type (s \neq t) & := & ( ;x^{s\neq t} )\\

%						%			\type (A \lor B)  & : = & (\vec u , \vec v ; \vec x , \vec y) & \text{if $\type(A) = (\vec u ; \vec x)$ and $\type(B) = (\vec v ; \vec y)$.} \\

									\type (A \star B)  & : = & (\vec u , \vec v ; \vec x , \vec y) &

%									\text{if $\type(A) = (\vec u ; \vec x)$, $\type(B) = (\vec v ; \vec y)$ and $\star \in \{ \lor, \land, \laor, \laand \}$.}

									\\

%									\type (! A) & : = & ( \vec u ,\vec x  ; ) & \text{if $\type(A) = (\vec u ; \vec x )$.} \\

									\type (\exists x^\word . A) & := & (\vec u ; \vec x , y) &

%									\text{if $\type (A) = (\vec u ; \vec x)$.}

									%	\type (\forall x^N . A) & := & \Nat \to \type(A)

									\end{array}

			\]

			where $\type(A)  = (\vec u ; \vec x)$,  $\type(B)=(\vec v ;  \vec y)$  and $\star \in \{ \lor , \land, \laor, \laand \}$.

			%	where $\nu$ designates that the inputs are normal.

		\end{definition}

%		\anupam{need to account for normality and safety somewhere. Attempting inlined and leaving types without this decoration.}

%

%		\begin{remark}

%			[Distribution of $!$]

%			There is a potential issue that the $!$ contains $\lor$ symbols in its scope, whence we do not in general have $!(A \lor B) \cong !A \lor !B$. However this will not be a problem here by inspection of a convergence statement: there are no $\lor$ symbols in the scope of a $!$. Therefore, after free-cut elimination, no formula in the proof will have this property either.

%

%			On the other hand, since we are working in affine logic, we do in general have $!(A \land B) \cong !A \land !B$.

%		\end{remark}

					For a sorted tuple $(u_1 , \dots u_m ; x_1 , \dots ,x_n )$ we write $|(\vec u ; \vec x)|$ to denote its length, i.e.\ $m+n$. This sorted tuple corresponds to input variables, normal and safe respectively.

%		\footnote{It becomes important here that we are considering proofs of a convergence statement, since a free-cut free $\arith$-proof of a convergence statement cannot contain any $\lor$ symbols in the scope of a $!$. This could cause an issue in the above definition since we do not in general have the equivalence $!(A \lor B) \equiv !A \lor !B$. On the other hand, the equivalence $!(A\land B) \equiv !A \land !B$ follows since we are in the affine setting.}

		Let us fix a particular (coherent) equational specification $\eqspec(f)$. Rather than directly considering $\arith$-proofs of $\conv ( f , \eqspec )$, we will consider a $\closure{\eqspec} \cup \arith $ sequent proof of $!\word (\vec x) \seqar \word (f (\vec x) )$, under Lemma~\ref{lemma:spec-norm-form}.

%

		Free-cut elimination crucially yields strong regularity properties for proofs:

		\begin{proposition}

			[Freedom]

			\label{prop:freedom}

	A free-cut free $\closure{\eqspec} \cup \arith $ sequent proof of $!\word (\vec x) \seqar \word (f (\vec x) )$ is:

	\begin{enumerate}

		\item\label{item:no-neg-word} Free of any negative occurrences of $\word$.

		\item\label{item:no-forall} Free of any $\forall$ symbols.

		\item\label{item:no-quest} Free of any $?$ symbols.

				\item\label{item:no-laor-step} Free of any $\laor$ or $\laand$ steps.\footnote{Because of the $\surj$ rule, the proof may still contain $\laor$ symbols, but these must be direct ancestors of some cut-step by free-cut freeness.}

	\end{enumerate}

		\end{proposition}

		For this reason we can assume that $\type$ is well-defined for all formulae occurring in a free-cut free proof of convergence, and so we can proceed with the translation from proofs to BC programs.

		\begin{definition}

			[Translation]

			\label{dfn:translation-of-proofs}

			We give a translation from a free-cut free $\closure{\eqspec} \cup \arith $ proof $\pi$, satisfying properties \ref{item:no-neg-word}, \ref{item:no-forall}, \ref{item:no-quest}, \ref{item:no-laor-step} of Prop.~\ref{prop:freedom} above, of a sequent $\Gamma \seqar \Delta$ to BC programs for a tuple of functions $\vec f^\pi$ with arguments $\type \left(\bigotimes\Gamma\right)$ such that $|\vec f^\pi | = | \type\left(\bigparr\Delta\right)|$.

			The translation is by induction on the structure of $\pi$, so we proceed by inspection of its final step.

			If $\pi$ is an instance of the initial rules $\geneps, \sepeps^0 , \sepeps^1, \sepzer, \sepone$ or $\inj$ then $\vec f^\pi$ is simply the constant function $\epsilon$ (possibly with dummy inputs as required by $\type$).

%			\footnote{This is because proofs of (in)equalities can be seen to carry no computational content.}

			If $\pi$ is an $\closure{\eqspec}$ or $=$ initial step it is also translated simply to $\epsilon$.

%

			The initial steps $\genzer, \genone , \surj$ and $\wordcntr$ are translated to $\succ_0( ; x) , \succ_1 (; x), ( \epsilon , \pred ( ;x) , \pred (; x) )$ and $(\id (;x) , \id(;x))$ respectively.

%

		Finally, suppose $\pi$ is a logical initial step. If $\pi $ is an instance of $\id$, i.e.\ $p \seqar p$, then we translate it to $\id$. Notice that, if $\pi$ is an instance of $\lefrul{\bot}$ (i.e.\ $p, p^\bot \seqar $ ) or $\rigrul{\bot}$ (i.e.\ $\seqar p, p^\bot$) then $p$ must be an equality $s=t$ for some terms $s,t$, since $p$ must be atomic and, by assumption, $\word$ does not occur negatively. Therefore $\pi$ is translated to tuples of $\epsilon$ as appropriate.

			Now we consider the inductive cases.

%

%		We will continue with similar notational conventions in the remainder of this argument.

%

%		%	\anupam{bad notation since need to include free variables of sequent too. (also of theory.) Reconsider.}

%

If $\pi$ ends with a $\rigrul{\land}$ or $\lefrul{\lor}$ step then we just rearrange the tuple of functions obtained from the inductive hypothesis.

%		The case when $\pi$ ends with a $\lefrul{\lor}$ step is analogous to the $\rigrul{\land}$ case above.

		If $\pi$ consists of a subproof $\pi'$ ending with a $\lefrul{\land}$ or $\rigrul{\lor}$-step, then $\vec f^\pi$ is exactly $\vec f^{\pi'}$.

			By assumption, there are no $\laor$, $\laand$, $?$ or $\forall$ steps occurring in $\pi$, and if $\pi$ consists of a subproof $\pi'$ followed by a $\lefrul{\exists}$ step then $\vec f^\pi$ is exactly the same as $\vec f^{\pi'}$, under possible reordering of the tuple.

			Suppose $\pi$ consists of a subproof $\pi'$ followed by a $\rigrul{\exists}$ step,

				\[

				\vlderivation{

					\vlin{\rigrul{\exists}}{}{ \Gamma, \word(t) \seqar \Delta , \exists x^\word . A(x) }{

%						\vltr{\pi'}{ \Gamma \seqar \Delta , A(t) }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

\vlhy{ \Gamma \seqar \Delta , A(t) }

					}

				}

				\]

				so by the inductive hypothesis we have functions $\vec f^\Delta , \vec f^{A(t)}$ with arguments $(\vec u ; \vec x )= \type(\bigotimes \Gamma)$. We define

%				$\vec f^\pi$ as follows:

%				\[

				$

				\vec f^\pi (\vec u ; \vec x , y)

%				\quad := \quad

				$ as $

				\left(

				\vec f^\Delta (\vec u ; \vec x) ,

				{\id (;y)},

				\vec f^{A(t)} (\vec u; \vec x)

				\right)

$.

%\]

		%		(The identity function on $y$ is defined from successor, predecessor and safe composition).

				%Suppose we have functions $\vec f^X (\vec x ; \vec y)$ from $\pi'$ for $X = \Delta$ or $ X=A$.

				%\[

				%\vec f(\vec x ; \vec y , z) \quad := \quad ( \vec f^\Delta (\vec x ; \vec y)   ,  z , \vec f^A ( \vec x ; \vec y ) )

				%\]

				%

				%Suppose we have functions $\vec f' (\vec u , \vec v ; x , \vec y , \vec z)$ from $\pi'$ with $(\vec u ; \vec x )$ corresponding to $\Gamma$, $(;x)$ corresponding to $N(a)$ and $(\vec v ; \vec z)$ corresponding to $A(a)$. We define:

				%\[

				%\vec f ( \vec u , \vec v ;  )

				%\]

%				\anupam{should just be same? Consider variable naming, just in case.}

%				\anupam{This is probably where the consideration for free variables is.}

				%Suppose we have functions $\vec g (\vec v  , \vec w ; \vec x , y , \vec z)$ where $(\vec v ; \vec x) $ corresponds to $\Gamma$, $y$ corresponds to $\word(a)$ and $(\vec w ; \vec z) $ corresponds to $A(a)$. Then we define:

				%\[

				%\vec f ( \vec v , \vec w ; \vec x , y , \vec z )

				%\]

					%	\[

					%	\vlderivation{

					%	\vliin{\rigrul{\laand}}{}{\Gamma \seqar \Delta, A \laand B}{

					%	\vltr{\pi_1}{  \Gamma \seqar \Delta, A}{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

					%	}{

					%	\vltr{\pi_2}{  \Gamma \seqar \Delta, B}{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

					%	}

					%	}

					%	\]

					%

					%	Suppose we have $\vec f^i (\vec x , \vec a ; \vec y , \vec b)$ from $\pi_i$.

					%

					%	\anupam{problem: does this require many tests, just like for contraction? Can we isolate a different complexity class? e.g.\ PH or Grzegorzyck?}

					%	\anupam{skip this case and consider later.}

			%		\anupam{commented stuff on additives. To remark later perhaps.}

			If $\pi$ consists of a subproof $\pi'$ followed by a $\rigrul{!}$ step then $\vec f^\pi$ is exactly the same as $\vec f^{\pi'}$. If $\pi$ ends with a $\lefrul{!}$ step then we just appeal to Prop.~\ref{prop:bc-properties} to turn a safe input into a normal input.

			Since there are no $?$ symbols in $\pi$, we can assume also that there are no $\rigrul{\cntr}$ steps in $\pi$.\footnote{Again, this is crucially important, since we cannot test the equality between arbitrary terms in the presence of nonlogical function symbols.}

		%		\anupam{This is important, so expand on this here or in a remark before/after.}

	If $\pi$ ends with a $\lefrul{\cntr}$ step then we duplicate some normal inputs of the functions obtained by the inductive hypothesis.

%		(Notice that this is obtainable in BC by a trivial instance of safe composition.)

		%	cntr right

		%	\[

		%	\vlderivation{

		%	\vlin{\rigrul{\cntr}}{}{\Gamma \seqar \Delta, ?A}{

		%	\vltr{\pi'}{  \Gamma \seqar \Delta, ?A, ?A}{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

		%	}

		%	}

		%	\]

		%	(need test function against witness predicate?)

		%

		%	\anupam{problem: how to test even equality of two terms? Maybe treat $?$ as $!$ on left?}

		%

		%	\anupam{Not a problem by free-cut elimination! Can assume there are no $?$ in the proof! Is this equivalent to treaing $?$ as $!$ on left?}

		%

		%	\anupam{Yes I think so. We can work in a left-sided calculus. only problem is for induction. But this can never be a problem for modalities since induction formulae are modality-free.}

		%

		%	\anupam{this is actually the main point.}

		If $\pi$ ends with a $\cut$ step whose cut-formula is free of modalities, then it can be directly translated to a safe composition of functions obtained by the inductive hypothesis, by relying on Prop.~\ref{prop:bc-properties}. Otherwise, the cut-formula must be of the form $!\word (t)$ since it must directly descend from the left-hand side of an induction step, by free-cut freeness.

%	 or axiom on one side. The only such occurrence of a modality is in the conclusion of an induction step, whence such a formula has the form $!\word (t)$.

	 Since the cut is anchored, we can also assume that the cut formula is principal on the other side, i.e.\ $\pi$ ends as follows:

%	\anupam{need to check this assumption against free-cut elimination conditions. To discuss.}

\[

\vlderivation{

	\vliin{\cut}{}{!\Gamma , \Sigma  \seqar \Delta }{

		\vlin{\rigrul{!}}{}{!\Gamma \seqar  !\word(t)}{

%			\vltr{\pi_1'}{!\Gamma \seqar  \word(t)}{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}

\vlhy{!\Gamma \seqar  \word(t)}

			}

		}{

%		\vltr{\pi_2}{ !\word(t), \Sigma\seqar \Delta}{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}

\vlhy{ !\word(t), \Sigma\seqar \Delta}

		}

	}

\]

 where

% $\pi_2$ ends with a $\ind$ step for which  $A(x)$ is the induction formula, and

 we assume there are no side-formulae on the right of the end-sequent of the left subproof for the same reason as $\rigrul{\cntr}$: $\pi$ does not contain any occurrences of $?$. By the inductive hypothesis we have functions $ g( \vec u ; )$ and $\vec h (  v , \vec w ; \vec x)$ where $\vec u$, $ v$ and $(\vec w ; \vec x)$ correspond to $!\Gamma$,  $!\word(t)$ and $\Sigma$ respectively. We construct the functions $\vec f^\pi $ as follows:

\[

\vec f^\pi (\vec u , \vec w ; \vec x)

\quad := \quad

\vec h (   g(\vec u ; ), \vec w  ; \vec x)

\]

Notice, again, that all safe inputs on the left occur hereditarily safe on the right, and so these expressions are definable in BC by Prop.~\ref{prop:bc-properties}.

%	Suppose $\pi$ ends with a $\lefrul{!}$ step:

%	\[

%	\vlderivation{

%		\vlin{!}{}{\Gamma, !A \seqar \Delta}{

%			\vltr{\pi'}{ \Gamma , A \seqar \Delta  }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

%		}

%	}

%	\]

%	\todo{finish this case, just passing a safe input to a normal input.}

%

%

%	Suppose $\pi$ ends with a $\rigrul{!}$ step:

%

%	\todo{finish this case, should not change function at all, but maybe there is a consideration.}

	If $\pi$ ends with a $\rigrul{\wk}$ step then we just add a tuple of constant functions $\vec \epsilon$ of appropriate length as dummy functions. If $\pi$ ends with a $\lefrul{\wk}$ step then we just add dummy inputs of appropriate length.

%	Suppose $\pi$ ends with a $\lefrul{\wk}$ step:

%

%	\todo{finish this case, just add a dummy input.}

%

%	Suppose $\pi$ ends with a $\rigrul{\wk}$ step:

%

%	\todo{finish this case, just add a dummy function.}

%

	Finally, suppose $\pi$ ends with a $\ind$ step. Since there are no occurrences of $?$ in $\pi$ we can again assume that there are no side formulae on the right of any induction step. Thus $\pi$ ends as follows:

	\[

	\vlderivation{

		\vliin{\ind}{}{ !\word (t), !\Gamma  ,  A(\epsilon) \seqar A(t) }{

%			\vltr{\pi_0}{!\word(a) , !\Gamma ,  A(a) \seqar A(\succ_0 a)}{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

\vlhy{!\word(a) , !\Gamma ,  A(a) \seqar A(\succ_0 a)}

		}{

%		\vltr{\pi_1}{!\word(a), !\Gamma ,  A(a)\seqar A(\succ_1 a) }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}

\vlhy{!\word(a), !\Gamma ,  A(a)\seqar A(\succ_1 a)}

	}

}

\]

%\anupam{is this better with a premiss for the base case?}

By the inductive hypothesis we have functions $\vec g^0 (u , \vec v ; \vec x)$ and $\vec g^1 (u , \vec v ; \vec x)$ with $u$, $\vec v$ and $\vec x$ corresponding to $!\word(a)$, $!\Gamma$ and $A(a)$ respectively. We define $\vec f^\pi$ by simultaneous predicative recursion on notation as follows:

\[

\begin{array}{rcll}

\vec f^\pi ( \epsilon, \vec v ; \vec x ) & := & \vec x & \\

\vec f^\pi ( \succ_i u , \vec v ; \vec x) & := & \vec g^i ( u, \vec v ; \vec f^\pi ( u, \vec v ; \vec x ) )

\end{array}

%\vec f^\pi ( \epsilon, \vec v ; \vec x ) := \vec x  \qquad

%\vec f^\pi ( \succ_i u , \vec v ; \vec x) :=  \vec g^i ( u, \vec v ; \vec f^\pi ( u, \vec v ; \vec x ) )

\]

%\anupam{check this}

%

%\todo{simultaneous PRN.}

\end{definition}

The induction step above is the reason why we enrich the usual BC framework with a simultaneous version of PRN.

\newcommand{\qfindth}{\mathit{IQF}}

\subsection{Witness predicate and extensional equivalence of functions}

%\anupam{need to mention that this predicate is similar to realisability predicate in absence, and indeed is presented like that for applicative theories, which also rely on free-cut elimination.}

Now that we have seen how to extract BC functions from proofs, we show that these functions satisfy the appropriate semantic properties, namely the equational program $\eqspec$ we started with. For this we turn to a quantifier-free \emph{classical} theory, in a similar fashion to $\mathit{PV}$ for $S^1_2$ in \cite{Buss86book} or system $T$ in G\"odel's Dialectica interpretation. This is adequate since we only care about extensional properties of extracted functions at this stage.

We could equally use a realisability approach, as done in e.g.\ \cite{Cantini02} and other works in applicative theories: since the formulae we deal with are essentially positive there is not much difference between the two approaches. Indeed here the witness predicate plays the same role as the realisability predicate in other works.

%, the complexity properties already handled by the BC programs we just constructed.

%The witness predicate of the WFM is similar to the realisability predicate, and this is even more true in out setting

Let $\qfindth$ be the classical theory over the language $\{ \epsilon, \succ_0, \succ_1 , (f^k_i )\}$ obtained from the axioms $\sepeps, \sepzer, \sepone, \inj, \surj$ and $\ind$ by dropping all relativisations to $\word$ (or $!\word$), replacing all linear connectives by their classical counterparts, and restricting induction to only quantifier-free formulae.

%For this we work in a quantifier-free classical logic whose atoms are equations between terms of our arithmetic and whose (sound) rules are simply the axioms of our arithmetic.

%

%(This is similar to the role of PV in the witnessing argument for $S^1_2$ and system $T$ for witnessing $I\Sigma_1$.)

%	\todo{add cases for $\laor$ and $\neq$.}

		\newcommand{\witness}[2]{\mathit{Wit}^{#1}_{#2}}

		\begin{definition}

			[Witness predicate]

			\label{dfn:wit-pred}

			For formulae $A, B$ of $\arith$ satisfying properties \ref{item:no-neg-word}, \ref{item:no-forall}, \ref{item:no-quest} of Prop.~\ref{prop:freedom}, we define the following `witness' predicate as a quantifier-free formula of $\qfindth$:

%			 $A$ with free variables amongst $\vec a$:

		\renewcommand{\sigma}{a}

			\[

%			\begin{array}{rcll}

%			\witness{}{A} (\sigma) & := & \sigma = t & \text{if $A$ is $\word (t)$.} \\

%			\witness{}{A} (\sigma) & := & s=t & \text{if $A$ is $s=t$.} \\

%						\witness{}{A} (\sigma) & := & s\neq t & \text{if $A$ is $s\neq t$.} \\

%			\witness{}{A \star B} ( \vec \sigma^A , \vec \sigma^B) & := &  \witness{}{A} (\vec \sigma^A) \cor \witness{}{B} (\vec \sigma^B) &

%						\text{for $\star \in \{ \lor,\laor\}$.}

%			\\

%			\witness{}{A \star B} ( \vec \sigma^A , \vec \sigma^B) & := &  \witness{}{A} (\vec \sigma^A ) \cand \witness{}{B} (\vec \sigma^B ) &

%						\text{for $\star \in \{ \land, \laand \}$.}

%			\\

%			\witness{}{\exists x^\word A} ( \sigma, \vec \sigma^A  ) & := & \witness{}{A}(\vec \sigma^A , \sigma ) & \\

%			\witness{}{!A} (\vec \sigma^A) & := & \witness{}{A} (\vec \sigma^A)

%			\end{array}

			\begin{array}{rcl}

			\witness{}{\word (t)} (\sigma) & := & \sigma = t

%			\text{if $A$ is $\word (t)$.}

			\\

			\witness{}{s=t} (\sigma) & := & s=t

%			\text{if $A$ is $s=t$.}

			\\

			\witness{}{s \neq t} (\sigma) & := & s\neq t

%			\text{if $A$ is $s\neq t$.}

\\

%			\witness{}{A \star B} ( \vec \sigma^A , \vec \sigma^B) & := &  \witness{}{A} (\vec \sigma^A) \cor \witness{}{B} (\vec \sigma^B) &

%			\text{for $\star \in \{ \lor,\laor\}$.}

%			\\

%			\witness{}{A \star B} ( \vec \sigma^A , \vec \sigma^B) & := &  \witness{}{A} (\vec \sigma^A ) \cand \witness{}{B} (\vec \sigma^B ) &

%			\text{for $\star \in \{ \land, \laand \}$.}

%			\\

%			\witness{}{\exists x^\word A} ( \sigma, \vec \sigma^A  ) & := & \witness{}{A}(\vec \sigma^A , \sigma ) & \\

			\witness{}{!A} (\vec \sigma^A) & := & \witness{}{A} (\vec \sigma^A)

			\end{array}

			\quad

						\begin{array}{rcl}

%						\witness{}{\word (t)} (\sigma) & := & \sigma = t & \text{if $A$ is $\word (t)$.} \\

%						\witness{}{s=t} (\sigma) & := & s=t & \text{if $A$ is $s=t$.} \\

%						\witness{}{s \neq t} (\sigma) & := & s\neq t &

%						\text{if $A$ is $s\neq t$.}

%						\\

						\witness{}{A \bullet B} ( \vec \sigma^A , \vec \sigma^B) & := &  \witness{}{A} (\vec \sigma^A) \cor \witness{}{B} (\vec \sigma^B)

%						\text{for $\star \in \{ \lor,\laor\}$.}

						\\

						\witness{}{A \circ B} ( \vec \sigma^A , \vec \sigma^B) & := &  \witness{}{A} (\vec \sigma^A ) \cand \witness{}{B} (\vec \sigma^B )

%						\text{for $\star \in \{ \land, \laand \}$.}

						\\

						\witness{}{\exists x^\word A} ( \sigma, \vec \sigma^A  ) & := & \witness{}{A}(\vec \sigma^A , \sigma )

%						 \\

%						\witness{}{!A} (\vec \sigma^A) & := & \witness{}{A} (\vec \sigma^A)

						\end{array}

%						\begin{array}{rcl}

%%						\witness{}{\word (t)} (\sigma) & := & \sigma = t & \text{if $A$ is $\word (t)$.} \\

%%						\witness{}{s=t} (\sigma) & := & s=t & \text{if $A$ is $s=t$.} \\

%%						\witness{}{s \neq t} (\sigma) & := & s\neq t & \text{if $A$ is $s\neq t$.} \\

%%						\witness{}{A \star B} ( \vec \sigma^A , \vec \sigma^B) & := &  \witness{}{A} (\vec \sigma^A) \cor \witness{}{B} (\vec \sigma^B) &

%%						\text{for $\star \in \{ \lor,\laor\}$.}

%%						\\

%%						\witness{}{A \star B} ( \vec \sigma^A , \vec \sigma^B) & := &  \witness{}{A} (\vec \sigma^A ) \cand \witness{}{B} (\vec \sigma^B ) &

%%						\text{for $\star \in \{ \land, \laand \}$.}

%%						\\

%						\witness{}{\exists x^\word A} ( \sigma, \vec \sigma^A  ) & := & \witness{}{A}(\vec \sigma^A , \sigma )  \\

%						\witness{}{!A} (\vec \sigma^A) & := & \witness{}{A} (\vec \sigma^A)

%						\end{array}

			\]

			where $\bullet \in \{ \lor, \laor \}$, $\circ \in \{ \land,\laand \}$, $|\vec \sigma^A| = |\type (A)|$ and $|\vec \sigma^B| = |\type (B)| $.

		\end{definition}

		%	\todo{problem: what about complexity of checking equality? }

%		\begin{remark}

		Notice that, unlike in the bounded arithmetic setting where the $\word$ predicate is redundant (since variables are tacitly assumed to range over $\word$), we do not parametrise the witness predicate by an assignment to the free variables of a formula. Instead these dependencies are taken care of by the explicit occurrences of the $\word$ predicate in $\arith$.

%		\end{remark}

%		\todo{Reformulate above later if necessary.}

		%	\todo{What about $\nat (t)$? What does it mean? Replace with true?}

		%	\todo{either use the witness predicate above, or use realizability predicate at meta-level and a model theory, like BH.}

		%	\anupam{Need to check above properly. $N(t)$ should be witnessed by the value of $t $ in the model. For equality of terms the witness should not do anything.}

%		\anupam{to consider/remark: formally, is witness predicate checked in model or some logical theory?}

\begin{lemma}

\label{lemma:witness-invariant}

Let $\pi$ be a free-cut free proof in $\closure{\eqspec}\cup \arith$, satisfying properties \ref{item:no-neg-word}, \ref{item:no-forall}, \ref{item:no-quest}, \ref{item:no-laor-step} of Prop.~\ref{prop:freedom}, of a sequent $\Gamma \seqar \Delta $. Let $\eqspec^\pi$ denote the BC program for $\vec f^\pi$.\footnote{We assume that the function symbols occurring in $\eqspec^\pi$ are distinct from those occurring in $\eqspec$.} Then $\qfindth$ proves:

\[

\left(\forall \eqspec \cand \forall \eqspec^\pi \cand \witness{}{\bigotimes \Gamma} (\vec a)\right) \cimp \witness{}{\bigparr \Delta } (\vec f^\pi(\vec a))

\]

where $\forall \eqspec$ and $\forall \eqspec^\pi$ denote the universal closures of $\eqspec$ and $\eqspec^\pi$ respectively.

%Suppose $\pi$ is a free-cut free $\Sigma^\nat_1$-$\pind$ proof of a sequent $\Gamma (\vec a) \seqar \Delta (\vec a)$, with $\vec f^\pi$ defined as above. Then:

%	\[

%			\witness{\vec a}{\bigotimes \Gamma} (\vec w , \vec b) \implies \witness{\vec a}{\bigparr \Delta } (\vec f^\pi(\vec w , \vec b), \vec b)

%			\]

\end{lemma}

%			\anupam{to consider: do we need parameters $\vec a$ in argument of $f$? Or does $\nat$ predicate take care of this?}

%

%			%	We will be explicit about normal and safe inputs when necessary, for the most part we will simply rearrange inputs into lists $(\vec u; \vec a)$ as in BC framework.

%

%%			We often suppress the parameters $\vec a$ when it is not important.

%

%			\anupam{Is this implication provable in Bellantoni's version of PV based on BC?}

			%	\anupam{for moment try ignore decoration on right? what about negation?}

	\begin{proof}[Proof sketch]

	By structural induction on $\pi$, again, following the definition of $\vec f^\pi$.\footnote{Notice that, since we are in a classical theory, the proof of the above lemma can be carried out in an arbitrary model, by the completeness theorem, greatly easing the exposition.}

	\end{proof}

	Finally, we arrive at our main result, providing a converse to Thm.~\ref{thm:arith-proves-bc-conv}.

		\begin{theorem}

		\label{thm:main-result}

		For any coherent equational specification $\eqspec$, if $\arith $ proves $\conv (f , \eqspec)$ then there is a polynomial-time function $g $ on $\Word$ (of same arity as $f$) satisfying $\eqspec [  g/ f ]$.

%		If we can prove a convergence statement for a function $f$ under a specification $\Phi(f)$ then there is a BC-program for a function $\mathbf f$ such that:

%		\begin{equation}

%		\label{eqn:spec-implies-program}

%\Phi(f) \implies f (\vec x) = \mathbf{f} (\vec x)

%		\end{equation}

%		\begin{equation}

%		\label{eqn:program-satisfies-spec}

%		\Phi(\mathbf f)

%		\end{equation}

		\end{theorem}

		\begin{proof}

		[Proof sketch]

%		By Thm.~\ref{thm:free-cut-elim} and Lemma~\ref{lemma:spec-norm-form} we have a free-cut free proof $\pi$ in $\closure{\eqspec} \cup \arith$ of $!\word (\vec x ) \seqar \word (f (\vec x))$. By Lemma~\ref{lemma:witness-invariant} above this means that $\vec a = \vec x \cimp f^\pi (\vec a) = f(\vec x)$ is true in any model of $\qfindth$ satisfying $\eqspec$ and $\eqspec^\pi$.

%%		Since some model must exist by coherence (cf.\ Prop.~\ref{prop:eq-spec-model}), we have that

%		Using the fact that $\eqspec \cup \eqspec^\pi$ is coherent we can construct such a model, similarly to Prop.~\ref{prop:eq-spec-model}, which will contain $\Word$ as an initial segment, in which we must have $f^\pi (\vec x) = f (\vec x)$ for every $\vec x \in \Word$, as required.\todo{polish}

Follows from Lemmas~\ref{lemma:spec-norm-form} and \ref{lemma:witness-invariant}, Dfn.~\ref{dfn:wit-pred} and coherence of $\eqspec$, cf.~\ref{prop:eq-spec-model}.

		\end{proof}

%			\begin{proof}

%			Notice that a convergence statement has the following form:

%			\[

%			!\Phi(f) , !\nat(\vec a) \seqar \nat(f (\vec a) )

%			\]

%			By the lemma above, and by inspection of the definition of the witness predicate, this means we have that,

%			\[

%			(\Phi(f) \cand \vec x = \vec a ) \implies \mathbf f (\vec x) = f(\vec a)

%			\]

%			whence we arrive at \eqref{eqn:spec-implies-program}.

%

%			Finally, notice that $\Phi(f)$ has \emph{some} model, since it is a monotone inductive definition so some fixed point must exist. Therefore we obtain \eqref{eqn:program-satisfies-spec} as well.

%			\end{proof}

%

%			\anupam{rephrase above proof to make more sense.}

%

%%

%\newcommand{\concat}{\mathit{concat}}

%\paragraph{Some points on concatenation \anupam{if necessary}}

%We can define the concatenation operation by PRN:

%\[

%\begin{array}{rcl}

%\concat (\epsilon ; y) & : = & x \\

%\concat (\succ_i x ; y) & := & \succ_i \concat (x ; y)

%\end{array}

%\]

%

%From here we can define iterated concatenation:

%\[

%\concat (x_1 , \dots x_n ; y) \quad := \quad \concat (x_n ; \concat (x_{n-1} ; \vldots \concat (x_1 ; y) \vldots ) )

%\]

%

%(notice all safe inputs are hereditarily to the right of $;$ so this is definable by safe composition and projection.)