/ - Diff - Linear Arithmetic - Forge du Centre Blaise Pascal

Révision 229

CSL17/main.tex (revision 229)
84	84
85	85	%% Either use bibtex (recommended),
86	86
	87	\newpage
87	88	\bibliography{ph-biblio}
88	89
89	90	%% .. or use the thebibliography environment explicitely

     \subsection{Graphs of some basic functions}\label{sect:graphsbasicfunctions}
     %Todo: $+1$,
     We say that a function $f$ is \emph{represented} by a formula $A_f$ if we can prove a formula of the form $\forall ^{\normal} \vec u, \forall ^{\safe} x, \exists^{\safe}! y. A_f$. The variables $\vec u$ and $\vec x$ can respectively be thought of as normal and safe arguments of $f$, and $y$ is the output of $f(\vec u; \vec x)$.
     We say that a function $f$ is \emph{represented} by a formula $A_f$ in a theory if we can prove a formula of the form $\forall ^{\normal} \vec u, \forall ^{\safe} x, \exists^{\safe}! y. A_f$. The variables $\vec u$ and $\vec x$ can respectively be thought of as normal and safe arguments of $f$, and $y$ is the output of $f(\vec u; \vec x)$.
     Let us give a few examples for basic functions representable in $\arith^1$:
     \begin{itemize}
-...
     As we mentioned, the fact that only $\Sigma^\safe_i$ formulae occur is due to the free-cut elimination result for first-order calculi \cite{Takeuti87,Cook:2010:LFP:1734064}, which gives a form of proof where every $\cut$ step has one of its cut formulae immediately below a non-logical step. Again, we have to adapt the $\rais$ rule a little to achieve our result, due to the fact that it has a $\exists x^\normal$ in its lower sequent. For this we consider a merge of $\rais$ and $\cut$, which allows us to directly cut the upper sequent of $\rais$ against a sequent of the form $\normal(u), A(u), \Gamma \seqar \Delta$.
     Finally, as is usual in bounded arithmetic, we use distinguished rules for our relativised quantifiers, e.g.\
     \todo{}
     Finally, as is usual in bounded arithmetic, we use distinguished rules for our relativised quantifiers, although we use ones that satisfy the aforementioned constraints. For instance, we include the following rules, from which the remaining ones are similar:
     \[
     \vlinf{\rigrul{\forall}}{}{ \normal(\vec u) , \safe (\vec x), \Gamma \seqar \Delta , \forall x^\safe . A(x)}{\normal(\vec u ) , \safe (\vec x), \safe (x) , \Gamma \seqar \Delta, A(x)}
     \quad
     \vlinf{\rigrul{\exists}}{}{\normal(\vec u) , \safe (\vec x) , \Gamma \seqar \Delta , \exists x^\safe . A(x)}{ \normal (\vec u) , \safe (\vec x) , \Gamma \seqar \Delta , A(t) }
     \]
     \[
     \vlinf{\lefrul{|\forall|}}{}{\normal (\vec u ) , \safe (\vec x) , s(\vec u) \leq |t(\vec u)| , \forall u^\normal \leq |t(\vec u)| . A(u) , \Gamma \seqar \Delta }{\normal (\vec u ) , \safe (\vec x) , A(t(\vec u)  ) , \Gamma \seqar \Delta  }
     \]
     where, in $\rigrul{\exists}$, $(\vec u ; \vec x)$ is compatible with $t$.

      \subsection{Some properties and extensions of $\bc$ and $\mubc$}\label{sect:somepropertiesofmubc}
      \anupam{done a pass up to here. Resuming at next section.}
     We will state some results here that we rely on in the later sections.
       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$.
       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)$.
       Thus, we will freely add $+(;x,y)$ to the $\mubc $ framework and define unary successor $\succ{} (;x) \dfn +(;x, \succ 1 0)$.
     %  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)$.
+    %
     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.
       \anupam{also add $\#$ and $|\cdot|$, for simplicity.}
       One important closure property we will need for $\mubc $ functions, namely to define `witness functions' later on, is the following:
       \begin{lemma}
       	[Sharply bounded lemma]
       	\label{lem:sharply-bounded-recursion}
       	Let $f_A$ be the characteristic function of a predicate $A(u , \vec u ; \vec x)$.
       	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)$.
       	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)$.
       \end{lemma}
       \begin{proof}
       	We give the $\forall$ case, the $\exists$ case being dual.
       	The characteristic function $f(v , \vec u ; \vec x)$ is defined by predicative recursion on $v$ as:
       	For the $\forall$ case, we define the characteristic function $f(v , \vec u ; \vec x)$ by predicative recursion on $v$ as:
       	\[
       	\begin{array}{rcl}
       	f(0, \vec u ; \vec x) & \dfn & f_A (0 , \vec u ; \vec x) \\
       	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) )
       	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) )
       	\end{array}
       	\]
       	The $\exists$ case is similar.
       \end{proof}
     \medskip
     \noindent
     \textbf{Encoding of sequences.}
       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 )$.
     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}.
       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 )$.
       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]
       	[Coding 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
       	\]
       	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 \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
       %	\]
+      $
       \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 )}
       	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 )}
       	\end{array}
       	\]
       	where the constants for $O(|u|l)$ are sufficiently large.
       	where $p(u l)$ is a sufficiently large polynomial.
       \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$.
       \begin{proof}[Proof sketch]
       	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$.
       \end{proof}
       Notice that $\beta (l,i;x)$ satisfies the polychecking lemma.
       We define
       %Notice that $\beta (l,i;x)$ satisfies the polychecking lemma.

Formats disponibles : Unified diff

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

Révision 229