Révision 229 CSL17/preliminaries.tex
| preliminaries.tex (revision 229) | ||
|---|---|---|
| 236 | 236 |
|
| 237 | 237 |
\subsection{Some properties and extensions of $\bc$ and $\mubc$}\label{sect:somepropertiesofmubc}
|
| 238 | 238 |
|
| 239 |
\anupam{done a pass up to here. Resuming at next section.}
|
|
| 239 |
We will state some results here that we rely on in the later sections.
|
|
| 240 | 240 |
|
| 241 | 241 |
Consider the addition function $+$ with two safe arguments, so denoted as $+(;x,y)$. It is clear that if $+(;x,y)=z$, then we have $|z| \leq \max(|x|,|y|)+1$, so $+$ is a polymax bounded function. Moreover for any $n$, the $n$th least significant bits of $z$ only depend on the $n$th least significant bits of $x$ and $y$, so $+(;x,y)$ is a polynomial checking function (on no normal argument), with threshold $q(x,y)=0$. |
| 242 | 242 |
|
| 243 |
In the following we will consider $\mubc(\Phi)$ with $\Phi$ containing the function $+(;x,y)$, but write it simply as $\mubc$. Note that addition could be defined in $\bc$ (hence in $\mubc$), but not with two safe arguments because the definition would use safe recursion. We will also use the unary successor $\succ{} (;x)$, which is defined thanks to addition as as $\succ{} (;x)=+(;x,\succ 1 0)$.
|
|
| 243 |
Thus, we will freely add $+(;x,y)$ to the $\mubc $ framework and define unary successor $\succ{} (;x) \dfn +(;x, \succ 1 0)$.
|
|
| 244 |
% In the following we will consider $\mubc(\Phi)$ with $\Phi$ containing the function $+(;x,y)$, but write it simply as $\mubc$. Note that addition could be defined in $\bc$ (hence in $\mubc$), but not with two safe arguments because the definition would use safe recursion. We will also use the unary successor $\succ{} (;x)$, which is defined thanks to addition as as $\succ{} (;x)=+(;x,\succ 1 0)$.
|
|
| 245 |
% |
|
| 246 |
In the same way, although for more simple reasons, we may add the functions $\#$ and $|\cdot|$ that we introduce later in Sect.~\ref{sect:arithmetic} to $\mubc$ containing only normal arguments since they are polynomial-time computable.
|
|
| 244 | 247 |
|
| 245 |
\anupam{also add $\#$ and $|\cdot|$, for simplicity.}
|
|
| 246 | 248 |
|
| 249 |
One important closure property we will need for $\mubc $ functions, namely to define `witness functions' later on, is the following: |
|
| 247 | 250 |
\begin{lemma}
|
| 248 | 251 |
[Sharply bounded lemma] |
| 249 | 252 |
\label{lem:sharply-bounded-recursion}
|
| 250 | 253 |
Let $f_A$ be the characteristic function of a predicate $A(u , \vec u ; \vec x)$. |
| 251 |
Then the characteristic functions of $\forall u \prefix v . A(u,\vec u ; \vec x)$ and $\exists u \prefix v . A(u , \vec u ; \vec x)$ are in $\bc(f_A)$.
|
|
| 254 |
Then the characteristic functions of $\forall u \leq |v| . A(u,\vec u ; \vec x)$ and $\exists u \leq |v| . A(u , \vec u ; \vec x)$ are in $\bc(f_A)$.
|
|
| 252 | 255 |
\end{lemma}
|
| 253 | 256 |
\begin{proof}
|
| 254 |
We give the $\forall$ case, the $\exists$ case being dual. |
|
| 255 |
The characteristic function $f(v , \vec u ; \vec x)$ is defined by predicative recursion on $v$ as: |
|
| 257 |
For the $\forall$ case, we define the characteristic function $f(v , \vec u ; \vec x)$ by predicative recursion on $v$ as: |
|
| 256 | 258 |
\[ |
| 257 | 259 |
\begin{array}{rcl}
|
| 258 | 260 |
f(0, \vec u ; \vec x) & \dfn & f_A (0 , \vec u ; \vec x) \\ |
| 259 |
f(\succ i v , \vec u ; \vec x) & \dfn & \cond ( ; f_A (\succ i v, \vec u ; \vec x) , 0 , f(v , \vec u ; \vec x) )
|
|
| 261 |
f(\succ i v , \vec u ; \vec x) & \dfn & \cond ( ; f_A (|\succ i v|, \vec u ; \vec x) , 0 , f(v , \vec u ; \vec x) )
|
|
| 260 | 262 |
\end{array}
|
| 261 | 263 |
\] |
| 264 |
The $\exists$ case is similar. |
|
| 262 | 265 |
\end{proof}
|
| 263 | 266 |
|
| 264 |
\medskip |
|
| 265 |
\noindent |
|
| 266 |
\textbf{Encoding of sequences.}
|
|
| 267 |
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 )$.
|
|
| 267 |
Finally, we will briefly outline some basic functions for (de)coding sequences. The functions we introduce here will in fact be representable in the theory $\arith^1$ that we introduce in the next section, which, along with proofs of their basic properties, will be important for the completeness result in Sect.~\ref{sect:completeness}.
|
|
| 268 |
|
|
| 269 |
We assume the existence of a simple pairing function in $\bc$ for elements of fixed size: $\pair{k,l}{x}{y}$ identifies the pair $(x \mode k , y \mode l )$.
|
|
| 268 | 270 |
An appropriate such function would `interleave' $x$ and $y$, adding delimiters as necessary. |
| 269 | 271 |
We assume that $|\pair{k,l}{x}{y}| = k+O(l)$ and $\pair{k,l}{x}{y}$ satisfies the polychecking lemma.
|
| 270 |
|
|
| 272 |
% |
|
| 271 | 273 |
We will simply write $\pair{l}{x}{y}$ for $\pair{l,l}{x}{y}$.
|
| 272 | 274 |
|
| 273 | 275 |
\begin{lemma}
|
| 274 |
[Creating sequences]
|
|
| 276 |
[Coding sequences]
|
|
| 275 | 277 |
\label{lem:sequence-creation}
|
| 276 |
Given a function $f(u , \vec u ; \vec x)$ there is a $\bc(f)$ function $F(l, u , \vec u ; \vec x)$ such that: |
|
| 277 |
\[ |
|
| 278 |
F(l,u,\vec u ; \vec x) |
|
| 279 |
\quad = \quad |
|
| 280 |
\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 |
|
| 281 |
\] |
|
| 278 |
Given a function $f(u , \vec u ; \vec x)$ there is a $\bc(f)$ function $F(l, u , \vec u ; \vec x) |
|
| 279 |
% $ such that: |
|
| 280 |
% \[ |
|
| 281 |
% F(l,u,\vec u ; \vec x) |
|
| 282 |
% \quad = \quad |
|
| 283 |
= |
|
| 284 |
\langle \cdots \langle f(0, \vec u ; \vec x) \mode l , f(1, \vec u ; \vec x) \mode l \rangle , \cdots , f(|u|, \vec u ; \vec x) \mode l \rangle |
|
| 285 |
% \] |
|
| 286 |
$ |
|
| 282 | 287 |
\end{lemma}
|
| 283 | 288 |
\begin{proof}
|
| 284 | 289 |
We simply define $F$ by safe recursion from $f$: |
| 285 | 290 |
\[ |
| 286 | 291 |
\begin{array}{rcl}
|
| 287 | 292 |
F(l,0, \vec u ; \vec x) & \dfn & \langle ; f(0) \mode l \rangle \\ |
| 288 |
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 )}
|
|
| 293 |
F(l, \succ i u , \vec u ; \vec x ) & \dfn & \pair{p(u l) , l}{F(l, u , \vec u ; \vec x)}{f( |\succ i u| , \vec u ; \vec x )}
|
|
| 289 | 294 |
\end{array}
|
| 290 | 295 |
\] |
| 291 |
where the constants for $O(|u|l)$ are sufficiently large.
|
|
| 296 |
where $p(u l)$ is a sufficiently large polynomial.
|
|
| 292 | 297 |
\end{proof}
|
| 293 | 298 |
|
| 294 | 299 |
\begin{lemma}
|
| 295 | 300 |
[Decoding sequences] |
| 296 | 301 |
We can define $\beta(l,i;x)$ as $(i\text{th element of x}) \mode l$.
|
| 297 | 302 |
\end{lemma}
|
| 298 |
\begin{proof}
|
|
| 299 |
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$.
|
|
| 303 |
\begin{proof}[Proof sketch]
|
|
| 304 |
First define $\beta (j,i;x)$ as $|j|$th bit of $|i|$th element of $x$, of the form $\bit(p(i,j) ; x)$ for some quasipolynomial $p$,\footnote{A quasipolynomial is just a polynomial that may contain $\smsh$.} then use similar idea to the proof above, concatenating the bits of the $i$th element by a recursion on $j$.
|
|
| 300 | 305 |
\end{proof}
|
| 301 | 306 |
|
| 302 |
Notice that $\beta (l,i;x)$ satisfies the polychecking lemma. |
|
| 303 |
|
|
| 304 |
We define |
|
| 307 |
%Notice that $\beta (l,i;x)$ satisfies the polychecking lemma. |
|
| 308 |
|
|
Formats disponibles : Unified diff