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

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

	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}

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

\paragraph*{Two properties needed}

For below, need witnesses and functions bounded by a polynomial in $l$.

		[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$}

For the implication above, let us simply refer to the LHS as $\Wit{\vec u ; \vec x}{\Gamma} (l , \vec u ; \vec x , \vec w)$ and the RHS as $\Wit{\vec u ; \vec x}{ \Delta} (l, \vec u ; \vec x , \vec w')$, with $\vec w'$ in place of $\vec f( \cdots )$, which is a slight abuse of notation: we assume that LHS and RHS are clear from context.

	Since the proof is in typed variable normal form we have that each line of the proof is of the same form, i.e.\ $\normal (\vec u), \safe (\vec x) , \Gamma \seqar \Delta$ over free variables $\vec u ; \vec x$.

	\paragraph*{Logical rules}

	Pairing, depairing. Need length-boundedness.

	If we have a left conjunction step:

	\[

	\vlinf{\lefrul{\cand}}{}{ \normal (\vec u ), \safe (\vec x) , A\cand B , \Gamma \seqar \Delta }{ \normal (\vec u ), \safe (\vec x) , A, B , \Gamma \seqar \Delta}

	\]

		By inductive hypothesis we have functions $\vec f (\vec u ; \vec x , w_A , w_B , \vec w)$ such that,

		\[

		\Wit{\vec u ; \vec x}{\Gamma} (l, \vec u ; \vec x , w_A , w_B , \vec w)

		\quad \implies \quad

		\Wit{\vec u ; \vec x}{\Delta} (l, \vec u ; \vec x , \vec f ( (\vec u ; \vec x) \mode l , (w_A , w_B , \vec w) \mode p(l) ))

		\]

	for some polynomial $p$.

	%

		We define $\vec f^\pi (\vec u ; \vec x , w , \vec w) \dfn \vec f (\vec u ; \vec x , \beta (p(l),0; w) , \beta(p(l),1;w),\vec w )$ and, by the bounding polynomial for pairing, it suffices to set $p^\pi = O(p)$.

	Right disjunction step:

	\[

		\vlinf{\rigrul{\cor}}{}{ \normal (\vec u ), \safe (\vec x) , \Gamma \seqar \Delta , A \cor B}{ \normal (\vec u ), \safe (\vec x) , \Gamma \seqar \Delta, A, B }

	\]

		$\vec f^\pi_\Delta$ remains the same as that of premiss.

		Let $f_A, f_B$ be the functions corresponding to $A$ and $B$ in the premiss, so that:

		\[

		\Wit{\vec u ; \vec x}{\Gamma} (l, \vec u ; \vec x , \vec w)

		\quad \implies \quad

		\Wit{\vec u ; \vec x}{\Delta} (l, \vec u ; \vec x , f_C ( (\vec u ; \vec x) \mode l , \vec w \mode p(l) ))		

		\]

		for $C = A,B$ and for some $p$, such that $f_A , f_B$ are bounded by $q(l)$ (again by IH).

		We define $f^\pi_{A\cor B} (\vec u ; \vec x, \vec w) \dfn \pair{q(l)}{f_A ((\vec u ; \vec x, \vec w))}{f_B ((\vec u ; \vec x, \vec w))}$.

	Sharply bounded quantifiers are generalised versions of logical rules.

	\[

	\vlinf{|\forall|}{}{\normal (\vec u) , \safe (\vec x) , \Gamma \seqar  \Delta , \forall u^\normal \leq |t(\vec u;)| . A(u) }{ \normal(u) , \normal (\vec u) , \safe (\vec x) , u \leq |t(\vec u;)| , \Gamma \seqar  \Delta, A(u)  }

	\]

	By the inductive hypothesis we have functions $\vec f(u , \vec u ; \vec x , w , \vec w)$ such that:

	\[

	\Wit{u ,\vec u ; \vec x}{\lhs} ( u , \vec u ;\vec x , w , \vec w )

	\quad \implies \quad

	\Wit{u , \vec u ; \vec x}{\rhs} (u, \vec u ; \vec x , \vec f ((\vec u ; \vec x) \mode l , \vec w \mode p(l) ) )

	\]

	with $|f|\leq q(|l|)$.

	By Lemma~\ref{lem:sequence-creation}, we have a function $F (l , u , \vec u ; \vec x , w , \vec w) $ such that....

	We set $f^\pi_{\forall u^\normal \leq t . A} (\vec u ; \vec x , \vec w) \dfn F(q(|l|), t(\vec u;), \vec u ; \vec x , 0, \vec w  )$.

	Right existential:

	\[

	\vlinf{\rigrul{\exists}}{}{\normal(\vec u ) , \safe (\vec x) , \Gamma \seqar \Delta , \exists x . A(x)}{\normal(\vec u ) , \safe (\vec x) , \Gamma \seqar \Delta , A(t)}

	\]

	Here we assume the variables of $t$ are amongst $(\vec u ; \vec x)$, since we are in typed variable normal form.

	\[

	\vlinf{\cntr}{}{\normal (\vec u) , \safe (\vec x) , \Gamma \seqar \Delta , A }{\normal (\vec u) , \safe (\vec x) , \Gamma \seqar \Delta , A , A}

	\]

	$\vec f^\pi_\Delta$ remains the same as that of premiss. Let $f_0 ,f_1$ correspond to the two copies of $A$ in the premiss.

	 We define:

	 \[

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

	 \quad \dfn \quad

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

	 \]

	\anupam{For $\normal (\vec u), \safe (\vec x)$ in antecedent, we always consider as a set, so do not display explicitly contraction rules. }

	Suppose final step is (wlog):

	\vlinf{\pind}{}{ \normal (\vec u), \safe (\vec x) , \Gamma, A(0) \seqar A(t(\vec u ;)) , \Delta}{ \left\{\normal (u) , \normal (\vec u) , \safe (\vec x) , \Gamma,  A(u) \seqar A(\succ i u ) , \Delta \right\}_{i=0,1} }

			\anupam{need to say in normal form part that can assume induction of this form}

		\Wit{u , \vec u ; \vec x}{\Gamma, A(0)} (l , u , \vec u ; \vec x ,  \vec w)

		\Wit{u , \vec u ; \vec x}{A(\succ i u)} (l , u , \vec u ; \vec x ,  h_i ((u , \vec u) \mode l ; \vec x \mode l , \vec w) )

	First let us define $ f$ as follows:

	 f (0 , \vec u ; \vec x, \vec w,  w ) & \dfn &  w\\

	 f( \succ i u , \vec u ; \vec x , \vec w, w) & \dfn & 

	 h_i (u , \vec u ; \vec x , \vec w , f(u , \vec u ; \vec x , \vec w , w ))

	where $\vec w$ corresponds to $\Gamma $ and $w$ corresponds to $A(0)$.

	Now we let $f^\pi (\vec u ; \vec x , \vec w) \dfn f(t(\vec u ; ) , \vec u ; \vec x , \vec w)$.

	\paragraph*{Cut}

	If it is a cut on an induction formula, which is safe, then it just corresponds to a safe composition since everything is substituted into a safe position.

	Otherwise it is a `raisecut':

	\[

	\vliinf{\rais\cut}{}{\normal (\vec u ) , \normal (\vec v) , \safe (\vec x) ,\Gamma \seqar \Delta }{ \normal (\vec u) \seqar \exists x^\safe  . A(x) }{ \normal (u)  , \normal (\vec v) , \safe (\vec x) , A(u), \Gamma \seqar \Delta }

	\]

	In this case we have functions $f(\vec u ; )$ and $\vec g (u, \vec v ; \vec x , w , \vec w )$, in which case we construct $\vec f^\pi$ as:

	\[

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

	\quad \dfn \quad

	\vec g ( \beta (1 ; f(\vec u ;) ) , \vec v ; \vec x , \beta(0;f(\vec u ;)) , \vec w )

	\]