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

\section{A safe encoding of sequences and computations}

Before we can prove the completeness result for our theory, we need to address an apparent problem with usual first-order encodings of computations.

Recalling the polychecking lemma, we notice that for usual encodings of sequences of natural numbers it is not possible to `decode' sequences as a safe input.

Otherwise phrased, we would like to implement G\"odel's beta functions with the sorting $\beta (i;x)$, returning the $i$th element of the sequence encoded by $x$.

However, for $x$ to be safe here, we must only require $\poly (i)$ rightmost bits of $x$ to determine a finite number of rightmost bits of $\beta(i;x)$.

If $x$ is construed as a concatenation of its elements, with distinguished delimiters, or similarly, accessing the $i$th element cannot have this property since we do not have any information about previously occurring elements, which may be very large.

In bounded arithmetic this problem is avoided due to the fact that we know in advance that computations can be polynomially bounded both in length and size of elements, since we are in PH by Parikh's theorem.

Due to the polymax bounded property we actually have a similar situation here, although we would naturally prefer to avoid introducing explicit bounds, favouring that all complexity control is managed by safety and normality of arguments.

The answer is to use a slightly modified encoding of sequences, based on a simple (and well known) idea.

For the sake of example, if we wanted to simply pair two arguments safely, we could just interleave their bits and satisfy the polychecking lemma, regardless of the size of the two arguments.

This is naturally scalable to any $k$-tuple of arguments, all safe.

For an arbitrary sequence we cannot use quite the same technique since length is not determined in advance.

However, by using a slightly more asymmetric encoding we can still access all required bits in quadratic modulus rather than linear, appealing to a `zig-zag' technique.

\anupam{Every number is an infinite ultimately 0 sequence.}

\begin{definition}

[Sequence (de)coding]

We define the function $\beta\bit (i,j;x,b)$, intuitively meaning ``the $j$th bit of the $i$th element of $x$ is $b$'' as $\bit \left( \frac{1}{2} (i+j)(i+j+1) +i ; x , b \right)$.

We now define \emph{length-bounded $\beta$ function} $\beta(i,l;x,b)$ as:

\[

\forall j \leq l . \bigvee\limits_{b=0,1} ( \beta\bit (i,j;x,b) \cand \bit (j;y,b) )

\]

\end{definition}

Our aim is to construct sequences formed from old sequences and new elements.

Namely we want the following result, which says that, given a number $x$ and a sequence $y$, there is another sequence $z$ formed from prepending $x$ to $y$:

\begin{proposition}

	[In $\arith$]

	$$

	\forall x^\safe, y^\safe. \exists z^\safe . \forall i^\normal\leq k, j^\normal\leq l .

	\left(

	\begin{array}{rl}

	& \bigwedge\limits_{b=0,1} (\bit(j;x,b) \cimp \beta (0,j;z,b) ) \\

	\cand & i>0 \cimp \bigwedge\limits_{b=0,1} (\beta(i-1, j;y,b) \cimp \beta(i,j;z,b) )

	\end{array}

	\right)

	$$

\end{proposition}

To prove this we will need two lemmata.

The first says we can construct a sequence whose $0$th element is $x$ and every other element is $0$.

\begin{lemma}

[In $\arith$]

$\forall l . \exists z . (\beta (0,|l| ; z , x) \cand \forall i \leq |k| . \beta(i,|l|;z,0) )$.

\end{lemma}

\begin{proof}

	Length induction on $l$.

\end{proof}

The second says we can prepend $0$ to any sequence:

\begin{lemma}

	[In $\arith$]

	$\forall x . \exists z . ( \beta(0,|l|;z,0) \cand \forall i\in (0,|k|] . \exists y . (\beta (i, |l| ; z,y) \cand \beta(i-1,|l|;x,y) )   )$

\end{lemma}

\begin{proof}

	Length induction on $l$.

\end{proof}

\subsection{Summary}

Assume the existence of a simple pairing function for elements of fixed size: $\pair{k,l}{x}{y}$ denotes the pair $(x \mode k , y \mode l )$.

An appropriate such function would `interleave' $x$ and $y$, adding delimiters as necessary.

We assume that $|\pair{k,l}{x}{y}| = k+O(l)$ and $\pair{k,l}{x}{y}$ satisfies the polychecking lemma.

We will simply write $\pair{l}{x}{y}$ for $\pair{l,l}{x}{y}$.

\begin{lemma}

	[Creating sequences]

	\label{lem:sequence-creation}

	Given a function $f(u , \vec u ; \vec x)$ there is a $\bc(f)$ function $F(l, u , \vec u ; \vec x)$ such that:

	\[

	F(l,u,\vec u ; \vec x)

	\quad = \quad

	\langle f(0, \vec u ; \vec x) \mode l , f(1, \vec u ; \vec x) \mode l , \dots , f(|u|, \vec u ; \vec x) \mode l \rangle

	\]

\end{lemma}

\begin{proof}

	We simply define $F$ by safe recursion from $f$:

	\[

	\begin{array}{rcl}

	F(l,0, \vec u ; \vec x) & \dfn & \langle ; f(0) \mode l \rangle \\

	F(l, \succ i u , \vec u ; \vec x ) & \dfn & \pair{O(|u| l) , l}{F(l, u , \vec u ; \vec x)}{f( |\succ i u| , \vec u ; \vec x )}

	\end{array}

	\]

	where the constants for $O(|u|l)$ are sufficiently large.

\end{proof}

\begin{lemma}

[Decoding sequences]

We can define $\beta(l,i;x)$ as $(i\text{th element of x}) \mode l$.

\end{lemma}

\begin{proof}

First define $\beta (j,i;x)$ as $j$th bit of $i$th element of $x$, then use similar idea to above, by a recursion on $j$.

\end{proof}

Notice that $\beta (l,i;x)$ satisfies the polychecking lemma.

We define