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

\begin{definition}

	[Length bounded characteristic functions]

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

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

	\[

	\begin{array}{rcl}

	\charfn{\vec u ; \vec x}{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{\vec u ; \vec x}{\neg A} (l, \vec u ; \vec x) & \dfn & \notfn (;\charfn{\vec u ; \vec x}{A}(l , \vec u ; \vec x)) \\

	\smallskip

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

	\smallskip

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

	%	\end{array}

	%	\quad

	%	\begin{array}{rcl}

	\\	\smallskip

	\charfn{\vec u ; \vec x}{\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{\vec u ; \vec x}{\forall x^\safe . A(x)} (l, \vec u ;\vec x ) & \dfn & 

	\begin{cases}

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

	1 & \text{otherwise}

	\end{cases}

	\end{array}

	\]

\end{definition}

\anupam{I cut-and-pasted the rest of this section into appendices to save space. Move things back gradually.}

\begin{theorem}

	[Typed variable normal form]

	\label{thm:normal-form}

\end{theorem}

[Length bounded (in)equality]

%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 define \emph{length-bounded inequality} as:

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

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

Notice that $\leqfn (l; x,y) = 1$ just if $x \mode l \leq y \mode l$.

We can also define $\eq( l; x,y)$ as $\andfn (;\leq(l;x,y),\leq(l;y,x))$.

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

Let us say that a sorting $(\vec u ; \vec x)$ of the variables $\vec u , \vec x$ is \emph{compatible} with a formula $A$ if each variable of $\vec x$ occurs hereditarily safe with respect to the $\bc$-types of terms (see App.~\ref{appendix:arithmetic}). 

In the presence of a compatible sorting, we may easily define functions that \emph{evaluate} safe formulae in $\mubc$:

Given a $\Sigma^\safe_i$ formula $A$ and compatible sorting $(\vec u; \vec x)$ of its variables, there is a $\mubci{i-1}$ program $\charfn{\vec u ;\vec x}{A} (l, \vec u ; \vec x)$ computing the characteristic function of $A (\vec u \mode l ; \vec x \mode l)$.

We will use the programs $\charfn{}{}$ in the witness functions we define below.

Let us write $\charfn{}{i}$ to denote the class of functions $\charfn{}{A}$ for $A \in \Pi^\safe_{i-1}$.

For the notion of bounding polynomial below we are a little informal with bounds, using `big-oh' notation, since it will suffice just to be `sufficiently large'.

	For a $\Sigma^\safe_{i}$ formula $A$ with a compatible sorting $(\vec u ; \vec x)$, we define the \emph{length-bounded witness function} $\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w)$ in $\bc (\charfn{}{i})$ and its \emph{bounding polynomial} $b_A (l)$ as follows:

		\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 )$ and we set $b_A (l) = 1$.

		\item If $A$ is $B \cor C$ then we may set $b_A = O(b_B + b_C)$ and define $		\wit{\vec u ; \vec x}{A} (l, \vec u ;\vec x , w) \dfn		\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 ) )  )$.

%		\[

%		\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 If $A$ is $\forall u \leq |t(\vec u;)| . B(u)$ we appeal to sharply bounded closure, Lemma~\ref{lem:sharply-bounded-recursion}, to define

		\(

		 \dfn

		\forall u \leq |t|.

		\)

		%appealing to Lemma~\ref{lem:sharply-bounded-recursion}, 

		and 

		we set 

		$b_A = O(b_{B(t)}^2 )$.

		\(

		\dfn 

		\)

		where $q$ is obtained by the polychecking and bounded minimisation properties, Lemmas~\ref{lem:polychecking} and \ref{lem:bounded-minimisation}, for $\wit{\vec u ; \vec x , x}{B(x)}$.

	\label{prop:wit-rfn}

Conversely, if $A (\vec u \mode l ; \vec x \mode l)$ is true then there is some $w \leq b_A(l)$ such that $\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x,w) =1$.

In order to prove Thm.~\ref{thm:soundness} we need the following lemma, essentially giving an interpretation of $\arith^i$ proofs into $\mubci{i-1}$:

	From a typed-variable normal form $\arith^i$ proof $\pi$ of a $\Sigma^\safe_i$ sequent $\normal(\vec u), \safe(\vec x) , \Gamma  \seqar \Delta$

	there are $\bc (\charfn{}{i})$ functions $ f^\pi_B (\vec u ; \vec x , w)$ for $B\in\Delta$ such that

	% such that, for any $l, \vec u ; \vec x  , w$, we have:

	\ \implies \

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

	for some polynomial $p$.

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

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

Now we can prove the soundness result:

		Suppose $\arith^i \proves \forall \vec u^\normal . \exists x^\safe . A(\vec u ; x)$. By inversion and Thm.~\ref{thm:normal-form} there is a $\arith^i$ proof $\pi$ of $\normal (\vec u ) \seqar \exists x^\safe. A(\vec u ; x )$ in typed variable normal form.

By Lemma~\ref{lem:proof-interp}, we have a $\mubci{i-1}$ function $f^\pi$ with $\wit{\vec u ;}{\exists x^\safe . A} (l, \vec u ; f(\vec u \mode l;)) =1$.

By the definition of $\wit{}{}$ and Prop.~\ref{prop:wit-rfn} we have that $\exists x . A(\vec u \mode l; x)$ is true just if $A(\vec u \mode l ; \beta (q(l), 1 ; f(\vec u \mode l;) ))$ is true.

Now, since all $\vec u$ are normal, we may simply set $l$ to have a longer length than all of these arguments, so the function $f(\vec u;) \dfn \beta (q(\sum \vec u), 1 ; f(\vec u \mode \sum \vec u;) ))$ suffices.