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

\section{Soundness}

\label{sect:soundness}

The main result of this section is the following:

\begin{theorem}

	\label{thm:soundness}

	If $\arith^i$ proves $\forall \vec u^\normal . \forall \vec x^\safe . \exists y^\safe . A(\vec u ; \vec x , y)$ then there is a $\mubci{i-1}$ program $f(\vec u ; \vec x)$ such that $\Nat \models A(\vec u ; \vec x , f(\vec u ; \vec x))$.

\end{theorem}

The main problem for soundness is that we have predicates, for example equality, that take safe arguments in our theory but do not formally satisfy the polychecking lemma for $\mubc$ functions. 

For this we will use length-bounded witnessing, borrowing a similar idea from Bellantoni's previous work \cite{Bellantoni95}.

\begin{definition}

[Length bounded basic functions]

We define \emph{length-bounded equality}, $\eq(l;x,y)$ as the characteristic function of the predicate:

\[

x \mode l = y \mode l

\]

which is definable by safe recursion on $l$:

\[

\begin{array}{rcl}

\eq (0 ; x,y) & \dfn & \equivfn (;\bit (0;x),\bit(0;y) ) \\

\eq (\succ i l; x,y) & \dfn & \cond (; \eq ( u;x,y ) , 0, \equivfn (; \bit (\succ i u ; x ) , \bit (\succ i l ; y ))  )

\end{array}

\]

We also define length-bounded inequality as:

\[

\begin{array}{rcl}

\leqfn (0 ; x ,y) & \dfn & \cimp (; \bit (0;x), \bit (0;y) ) \\

\leqfn (\succ i l ; x,y) & \dfn & \orfn ( ; <(\bit (\succ i l ; x) , \bit(\succ i l ; y) ) , \andfn (; \equivfn (\bit (\succ i l ; x) , \bit(\succ i l ; y)) , \leqfn (l;x,y ) ) )

\end{array}

\]

\end{definition}

\anupam{Do we need the general form of length-boundedness? E.g. the $*$ functions from Bellantoni's paper? Put above if necessary. Otherwise just add sequence manipulation functions as necessary.}

Notice that $\eq$ is a polymax bounded polyomial checking function on its normal input, and so can be added to $\mubc$ without problems.

\begin{definition}

	[Length bounded characteristic functions]

	We define $\mubci{}$ programs $\charfn{}{A} (l , \vec u; \vec x)$, parametrised by a formula $A(\vec u ; \vec x)$, as follows.

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

	\[

	\begin{array}{rcl}

	\charfn{}{s\leq t} (l, \vec u ; \vec x) & \dfn & \leqfn(l;s,t) \\

	\smallskip

	\charfn{}{s=t} (l, \vec u ; \vec x) & \dfn & \eq(l;s,t) \\

	\smallskip

	\charfn{}{\neg A} (l, \vec u ; \vec x) & \dfn & \neg (;\charfn{}{A}(l , \vec u ; \vec x)) \\

	\smallskip

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

	\smallskip

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

	\smallskip

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

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

	0 & \text{otherwise} 

	\end{cases} \\

	\smallskip

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

	\begin{cases}

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

	1 & \text{otherwise}

	\end{cases}

	\end{array}

	\]

\end{definition}

\anupam{Above and below definitions need to be with respect to a typing of variables which terms respect.}

\begin{proposition}

	$\charfn{}{A} (l, \vec u ; \vec x)$ is the characteristic function of $A (\vec u \mode l ; \vec x \mode l)$.

\end{proposition}

\begin{definition}

	[Length bounded witness function]

	We now define $\Wit{\vec u ; \vec x}{A} (l , \vec u ; \vec x)$ for a $\Sigma_{i+1}$-formula $A$ with free variables amongst $\vec u; \vec x$.

	For a $\Sigma^\safe_i$ formula $A$ with free variables amongst $(\vec u ; \vec x)$, with $\vec x$ occurring only hereditarily safe in terms, we define the \emph{length-bounded witness function} $\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w)$ and its \emph{bounding polynomial} $b_A (l)$ as follows:

	\begin{itemize}

		\item If $A$ is $\Pi^\safe_{i-1}$ then $\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w) \dfn \charfn{\vec u ; \vec x}{A} (l, \vec u ; \vec x )$.

		\item If $A$ is $B \cor C$ then 

		\[

		\wit{\vec u ; \vec x}{A} (l, \vec u ;\vec x , w) 

		\quad \dfn \quad

		\orfn ( ; \wit{\vec u ; \vec x}{B} (l, \vec u ; \vec x , \beta (b_B (l) , 0 ; w ) ) , \wit{\vec u ; \vec x}{C} (l, \vec u ; \vec x , \beta (b_C (l) , 0 ; w ) )  )

		\]

		and we may set $b_A = O(b_B + b_C)$.

		\item Similarly if $A $ is $B \cand C$, but with $\andfn$ in place of $\orfn$.

%		\item If $A$ is $B \cand C$ then

%			\[

%			\wit{\vec u ; \vec x}{A} (l, \vec u ;\vec x , w) 

%			\quad \dfn \quad

%			\andfn ( ; \wit{\vec u ; \vec x}{B} (l, \vec u ; \vec x , \beta (b_B (l) , 0 ; w ) ) , \wit{\vec u ; \vec x}{C} (l, \vec u ; \vec x , \beta (b_C (l) , 0 ; w ) )  )

%			\]

%			and we may set $b_A = O(b_B + b_C)$.

		\item If $A$ is $\forall u \leq |t(\vec u;)| . B(u)$ then 

		\[

		\wit{\vec u ; \vec x}{A}

		\quad \dfn\quad

		\forall u\normal \leq |t|.

		\wit{u, \vec u ; \vec x}{B(u)} (l, u, \vec u ; \vec x , \beta( b_{B(t)} (l) , u ; w ) )

		\]

		appealing to Lemma~\ref{lem:sharply-bounded-recursion}, where we may set $b_A = O(b_{B(t)}^2 )$.

		\item Similarly if $A$ is $\exists u^\normal \leq |t(\vec u;)|. A'(u)$, but with $\exists u \leq |t|$ in place of $\forall u \leq |t|$.

		\item If $A$ is $\exists x^\safe . B(x) $ then

		\[

		\wit{\vec u ; \vec x}{A}

		\quad \dfn \quad

		\wit{\vec u ; \vec x , x}{B(x)} ( l, \vec u ; \vec x , \beta( b_{B} (l) , 0;w ) , \beta (q(l) , 1 ;w ))

		\]

		where $q$ is obtained by the polychecking and bounded minimisation lemmata for $\wit{\vec u ; \vec x , x}{B(x)}$.

		We may set $b_A = O(b_B + q )$.

	\end{itemize}

%	\[

%	\begin{array}{rcl}

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

%	\smallskip

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

%	\smallskip

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

%	\smallskip

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

%	\\

%	\smallskip

%	\wit{\vec u ; \vec x}{\forall u \leq |t(\vec u;)| . A(x)} (l , \vec u ; \vec x, w) & \dfn & 

%	\forall u \leq |t(\vec u;)| . \wit{u , \vec u ; \vec x}{A(u)} (l, u , \vec u ; \vec x, \beta(u;w) )

%	\end{array}

%	\]

%	\anupam{need length bounding for sharply bounded quantifiers}

\end{definition}

\anupam{may as well use a single witness variable since need it for sharply bounded quantifiers anyway.}

\anupam{sharply bounded case obtained by sharply bounded lemma}

\begin{proposition}

	If, for some $w$, $\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x,w) =1$, then $A (\vec u \mode l ; \vec x \mode l)$ is true.

	\anupam{check statement, need proof-theoretic version?}

\end{proposition}

By the polychecking lemma, we can assume that such a $w$ is bounded by some polynomial in $l$.

In order to prove Thm.~\ref{thm:soundness} we need the following lemma:

\begin{lemma}

		[Proof interpretation]

		\label{lem:proof-interp}

	From a normal form \todo{define, prove exists} $\arith^i$ proof $\pi$ of a $\Sigma^\safe_i$ sequent $\normal(\vec u), \safe(\vec x) , \Gamma  \seqar \Delta$

	there are $\mubci{i-1}$ functions $\vec f^\pi (\vec u ; \vec x , w)$ (where $\vec f^\pi = (f^\pi_B)_{B\in\Delta}$) such that, for any $l, \vec u ; \vec x  , w$, we have:

	\[

%	\vec a^\nu = \vec u ,

%	\vec b^\sigma = \vec u, 

	\bigwedge\limits_{A \in \Gamma} \wit{\vec u ; \vec x}{ A} (l, \vec u ; \vec x , w_A) =1

	\quad \implies \quad

	\bigvee\limits_{B\in \Delta} \wit{\vec u ; \vec x}{B} (l, \vec u ; \vec x , f^\pi_B(\vec u \mode l ; \vec x \mode l, \vec w)) = 1

	\]

	\anupam{Need $\vec w \mode p(l)$ for some $p$.}

	\anupam{$l$ may occur freely in the programs $f^\pi_B$}

\end{lemma}

\todo{Make statement above proper, with all bounds and moduli. I cut the proof to the appendix, maybe add sketch if space.}

From this lemma we can readily prove the soundness result:

	\begin{proof}

		[Proof of Thm.~\ref{thm:soundness} from Lemma~\ref{lem:proof-interp}]

		(watch out for dependence on $l$, try do without)

		Suppose $\arith^i \proves \forall \vec u^\normal . \exists x^\normal . A(\vec u ; x)$. Then by raising, inversion, free-variable normal forms, we have a proof of,

		\[

		\normal (\vec u ) \seqar \exists x^\normal . A(\vec u , x ;)

		\]

		whence, by Lemma~\ref{lem:proof-interp}, we have a $\mubci{i-1}$ function $f$ such that:

		\[

		\vec u \mode l = \vec a \mode l

		\quad \implies \quad

		\wit{\vec u ; }{A} ( l , \vec u , f(\vec u \mode l;) ) =1

		\]

		Now it suffices to choose an $l$ bigger that both all the $\vec u$ and $f(\vec u)$, which is a polynomial in $\vec u$ by the polymax bounding lemma.

	\end{proof}