root / CharacterizingPH / qpvbc.tex @ 251
Historique | Voir | Annoter | Télécharger (10,62 ko)
| 1 |
\documentclass{amsart}
|
|---|---|
| 2 |
\usepackage{amsthm}
|
| 3 |
\usepackage{hyperref}
|
| 4 |
\usepackage[dvipsnames]{xcolor}
|
| 5 |
|
| 6 |
|
| 7 |
\input{macros}
|
| 8 |
|
| 9 |
\begin{document}
|
| 10 |
|
| 11 |
|
| 12 |
|
| 13 |
\section{Extending the basic BC framework}
|
| 14 |
\begin{itemize}
|
| 15 |
\item Any polynomial-time predicate can be conservatively added to BC with only safe inputs. |
| 16 |
\item Thus all logical connectives $\neg, \vee, \wedge$ and equality testing $=$ can be implemented as programs with only safe arguments. |
| 17 |
\item Can add G\"odel's $\beta$ functions with a safe input: |
| 18 |
\end{itemize}
|
| 19 |
|
| 20 |
|
| 21 |
\section{QPVBC}
|
| 22 |
|
| 23 |
\subsection{Bellantoni's system $\pvbci{}$}
|
| 24 |
|
| 25 |
\begin{definition}
|
| 26 |
[Hierarchies] |
| 27 |
We define the following: |
| 28 |
\begin{itemize}
|
| 29 |
\item $\fphi i$: $i$th level of functional polynomial hierarchy. I.e.\ $\Box_i$ = $\fptime(\Sigma^p_{i-1})$.
|
| 30 |
\item $\mubci{i}$: $\mu$BC programs with $i$ nested $\mu$s, i.e., corresponds to $\fphi {i-1}$.
|
| 31 |
\item $\pvbci i$: defined as $\pvbci{} + \Sigma^\sigma_i$-induction.
|
| 32 |
\end{itemize}
|
| 33 |
\end{definition}
|
| 34 |
|
| 35 |
\begin{definition}
|
| 36 |
[Provably total function] |
| 37 |
\end{definition}
|
| 38 |
|
| 39 |
|
| 40 |
\subsection{Extensions by induction principles}
|
| 41 |
|
| 42 |
|
| 43 |
|
| 44 |
\section{Soundness}
|
| 45 |
We show that provably total functions of $\pvbci i$ are in $\fphi i$. |
| 46 |
|
| 47 |
The following is our main result: |
| 48 |
\begin{theorem}
|
| 49 |
If $\pvbci i \proves \forall \vec u^\normal , \vec x^\sigma . \exists \vec y^\sigma. A(\vec u , \vec x , \vec y)$, then there are $\mubci i $ programs $\vec f (\vec u ; \vec x)$ such that $\pvbci i \proves\forall \vec u^\normal , \vec x^\sigma . A(\vec u , \vec x , \vec f (\vec u ; \vec x) ) $. |
| 50 |
\end{theorem}
|
| 51 |
|
| 52 |
\begin{definition}
|
| 53 |
[Witness predicate] |
| 54 |
The \emph{witness predicate} is a $\mubci{}$ program $\wit{\vec a}{A}$, parametrised by variables $\vec a$ and a formula $A$ whose free variables are amongst $\vec a$, defined as follows.
|
| 55 |
If $A$ is a $\Pi_{i}$ formula then:
|
| 56 |
\[ |
| 57 |
\begin{array}{rcl}
|
| 58 |
\wit{\vec u; \vec x}{s=t} (\vec u ; \vec x, w) & \dfn & =(;s,t) \\
|
| 59 |
\smallskip |
| 60 |
\wit{\vec u; \vec x}{s\neq t} (\vec u ; \vec x, w) & \dfn & \neg (;=(;s,t)) \\
|
| 61 |
\smallskip |
| 62 |
\wit{\vec u ; \vec x}{A\cor B} (\vec u ; \vec x , w) & \dfn & \cor (; \wit{\vec u , \vec x}{A} (\vec u ; \vec x , w), \wit{\vec u , \vec x}{B} (\vec u ;\vec x, w) ) \\
|
| 63 |
\smallskip |
| 64 |
\wit{\vec u ; \vec x}{A\cand B} (\vec u ; \vec x , w) & \dfn & \cand(; \wit{\vec u , \vec x}{A} (\vec u ; \vec x , w), \wit{\vec u , \vec x}{B} (\vec u ;\vec x, w) ) \\
|
| 65 |
\smallskip |
| 66 |
\wit{\vec u ; \vec x}{\exists x^\safe . A(x)} (\vec u ;\vec x, w) & \dfn & \begin{cases}
|
| 67 |
1 & \exists x^\safe . \wit{\vec u; \vec x, x }{A(x)} (\vec u ;\vec x , x, w) = 1 \\
|
| 68 |
0 & \text{otherwise}
|
| 69 |
\end{cases} \\
|
| 70 |
\smallskip |
| 71 |
\wit{\vec u; \vec x}{\forall x^\safe . A(x)} (\vec u ;\vec x , w) & \dfn &
|
| 72 |
\begin{cases}
|
| 73 |
0 & \exists x^\sigma. \wit{\vec u ; \vec x , x}{ A(x)} (\vec u; \vec x , x) = 0 \\
|
| 74 |
1 & \text{otherwise}
|
| 75 |
\end{cases}
|
| 76 |
\end{array}
|
| 77 |
\] |
| 78 |
We now define $\Wit{\vec a}{A}$ for a $\Sigma_{i+1}$-formula $A$ with free variables amongst $\vec a$.
|
| 79 |
\[ |
| 80 |
\begin{array}{rcl}
|
| 81 |
\Wit{\vec u ; \vec x}{A} (\vec u ; \vec x , w) & \dfn & \wit{\vec u ; \vec x}{A} (\vec u ; \vec x) \text{ if $A$ is $\Pi_i$} \\
|
| 82 |
\smallskip |
| 83 |
\Wit{\vec u ; \vec x}{A \cor B} (\vec u ; \vec x , \vec w^A , \vec w^B) & \dfn & \cor ( ; \Wit{\vec u ; \vec x}{A} (\vec u ; \vec x , \vec w^A) ,\Wit{\vec u ; \vec x}{B} (\vec u ; \vec x , \vec w^B) ) \\
|
| 84 |
\smallskip |
| 85 |
\Wit{\vec u ; \vec x}{A \cand B} (\vec u ; \vec x , \vec w^A , \vec w^B) & \dfn & \cand ( ; \Wit{\vec u ; \vec x}{A} (\vec u ; \vec x , \vec w^A) ,\Wit{\vec u ; \vec x}{B} (\vec u ; \vec x , \vec w^B) ) \\
|
| 86 |
\smallskip |
| 87 |
\Wit{\vec u ; \vec x}{\exists x^\safe . A(x)} (\vec u ; \vec x , \vec w , w) & \dfn & \Wit{\vec u ; \vec x , x}{A(x)} ( \vec u ; \vec x , w , \vec w )
|
| 88 |
\end{array}
|
| 89 |
\] |
| 90 |
|
| 91 |
|
| 92 |
\end{definition}
|
| 93 |
|
| 94 |
\nb{use (de)pairing to make sure only $i$ $\mu$s are used to express a $\Pi_i$ predicate.}
|
| 95 |
|
| 96 |
\begin{proposition}
|
| 97 |
For $\Sigma_{i+1}$ formulae $A$, $\Wit{\vec u ; \vec x}{A}$ is a $\mubci{i} $ program.
|
| 98 |
\end{proposition}
|
| 99 |
|
| 100 |
\nb{In fact, need that $\wit{}{}$ is $\mubci{i}$ and $\Wit{}{}$ and the witness functions $\vec f$ are $\bc (\wit{}{})$}
|
| 101 |
|
| 102 |
Before proving the main theorem, we will need the following `witnessing lemma': |
| 103 |
|
| 104 |
\begin{lemma}
|
| 105 |
If $\pvbci{i+1} $ proves a $\Sigma^\safe_{i+1}$-sequent $\Gamma \seqar \Delta$ with free variables $\vec u^\normal , \vec x^\safe$ then there are $\mubci {i}$ functions $\vec f$ such that
|
| 106 |
\[ |
| 107 |
\pvbci {i+1} \proves \Wit{\vec u , \vec x}{\bigwedge \Gamma} (\vec u ; \vec x , \vec w) \cimp \Wit{\vec u , \vec x}{\bigvee \Delta } (\vec u ; \vec x, \vec f (\vec u ; \vec x , \vec w) )
|
| 108 |
\] |
| 109 |
(we simply write $\Wit{\vec u ; \vec x}{A}(\vec u ; \vec x , \vec w)$, instead of $\Wit{\vec u ; \vec x}{A}(\vec u ; \vec x , \vec w) =1 $.
|
| 110 |
\end{lemma}
|
| 111 |
\begin{proof}
|
| 112 |
By induction on the size of a $\pvbci{i+1} $ proof.
|
| 113 |
Interesting steps below: |
| 114 |
\begin{itemize}
|
| 115 |
\item $\neg$-right. (Can assume only applies to atomic formulae, and so no effect.) |
| 116 |
\item $\exists$-right. |
| 117 |
\[ |
| 118 |
\dfrac{\Gamma \seqar \Delta , A(t^\safe )}{ \Gamma \seqar \Delta, \exists x^\safe . A(x) }
|
| 119 |
\] |
| 120 |
By the inductive hypothesis, have functions $\vec f(\vec u ; \vec x), \vec g (\vec u ; \vec x)$ such that, |
| 121 |
\[ |
| 122 |
\pvbci{i+1} \proves
|
| 123 |
\Wit{\vec u ; \vec x}{\bigwedge \Gamma } (\vec u ; \vec x , \vec w)
|
| 124 |
\cimp |
| 125 |
\left( |
| 126 |
\Wit{\vec u ; \vec x}{\bigvee \Delta} (\vec u ; \vec x , \vec f (\vec u ; \vec x , \vec w) )
|
| 127 |
\cor |
| 128 |
\Wit{\vec u ; \vec x}{A(t)} (\vec u ; \vec x , \vec g (\vec u ; \vec x , \vec w))
|
| 129 |
\right) |
| 130 |
\] |
| 131 |
(just use $t$ as one of the witness functions) |
| 132 |
\item $\forall$-right. (Must be a $\Pi_i$ formula, so forget witness and compute $\wit{}{}$)
|
| 133 |
\item Contraction-right: |
| 134 |
\[ |
| 135 |
\dfrac{\Gamma \seqar \Delta , A ,A}{\Gamma \seqar \Delta, A}
|
| 136 |
\] |
| 137 |
By infuctive hypothesis have functions $\vec f, \vec g^1 , \vec g^2$ such that: |
| 138 |
\[ |
| 139 |
todo |
| 140 |
\] |
| 141 |
(just use conditional with a call to $\Wit{}{}$)
|
| 142 |
\item induction |
| 143 |
\[ |
| 144 |
\dfrac{\{\Gamma , A(a) \seqar A(s_i a) , \Delta\}_{i=0,1} }{\Gamma, A(0) \seqar A(t) , \Delta}
|
| 145 |
\] |
| 146 |
\end{itemize}
|
| 147 |
\end{proof}
|
| 148 |
|
| 149 |
\section{Completeness}
|
| 150 |
Here we show that every $\mubci{i}$ function is definable in $\pvbci {i+1}$.
|
| 151 |
|
| 152 |
|
| 153 |
\nb{WoP known as `minimization' principles in bounded arithmetic}
|
| 154 |
\begin{theorem}
|
| 155 |
[Well ordering property] |
| 156 |
\[ |
| 157 |
\pvbci{i+1} \proves \exists x^\safe . A(x) \cimp \exists x^\safe . (A(x) \cand \forall y^\safe . (A(y) \cimp x \leq y ) )
|
| 158 |
\] |
| 159 |
\end{theorem}
|
| 160 |
\begin{proof}
|
| 161 |
We work in $\pvbci{i+1}$ and show the contrapositive.
|
| 162 |
Suppose: |
| 163 |
\begin{equation}
|
| 164 |
\label{eqn:no-least}
|
| 165 |
\forall x^\safe. (A(x) \cimp \exists y^\safe . A(y) \cand y<x ) |
| 166 |
\end{equation}
|
| 167 |
We show that, |
| 168 |
\begin{equation}
|
| 169 |
\label{eqn:ih-wop}
|
| 170 |
\forall x. \forall y \leq a - x. (\cnot A(y) \cimp \cnot A(y + x)) |
| 171 |
\end{equation}
|
| 172 |
by polynomial induction on $x$. |
| 173 |
|
| 174 |
Let $B(x)$ be such that \eqref{eqn:ih-wop} is $\forall x . B(x)$.
|
| 175 |
\nb{If $A \in \Sigma^\safe_i \cup \Pi^\safe_i$ then $B \in \Pi^\safe_{i+1}$.}
|
| 176 |
|
| 177 |
When $x=0$, notice that \eqref{eqn:ih-wop} is just a generalised identity.
|
| 178 |
|
| 179 |
Suppose that $B(x)$ and let us show that $B(2x)$. |
| 180 |
Let $y \leq a - 2x$ such that $\cnot A(y)$. |
| 181 |
Then $y\leq a-x$ so by $B(x)$ we have that $\cnot A(y+x)$. |
| 182 |
We also have that $y+x \leq a-x$ so by $B(x)$ we have that $\cnot A(y+2x)$, as required. |
| 183 |
|
| 184 |
Now suppose that $B(x)$ and let us show that $B(2x+1)$. |
| 185 |
Let $y \leq a - 2x - 1$ such that $\cnot A(y)$. |
| 186 |
By similar reasoning to the $2x$ case, we have that $\cnot A(y + 2x )$. |
| 187 |
\end{proof}
|
| 188 |
|
| 189 |
|
| 190 |
\subsection{What we want for WoP}
|
| 191 |
From bounded arithmetic: |
| 192 |
|
| 193 |
$\Sigma_{i+1}$-LMIN $ \iff$ $\Sigma_{i+1}$-PIND $\implies$ $\Sigma_i$-IND $\iff$ $\Sigma_i$-MIN $ \iff$ $\Pi_{i+1}$-MIN.
|
| 194 |
|
| 195 |
\subsection{Completeness proof idea}
|
| 196 |
For each $\mubci i$ function $f(\vec u ; \vec x)$ we $\Sigma_i$-define a formula $A_f (\vec u ; \vec x , y )$ in $\pvbci{i+1}$ such that:
|
| 197 |
\[ |
| 198 |
\proves A_f (\vec u ; \vec x , y) |
| 199 |
\quad |
| 200 |
\iff |
| 201 |
\quad |
| 202 |
f(\vec u ; \vec x) = y |
| 203 |
\] |
| 204 |
and $A_f$ is provably total in $\pvbci{i+1}$.
|
| 205 |
|
| 206 |
For the $\mu$ case, say we have the function: |
| 207 |
\[ |
| 208 |
\mu x^{+1} . f(\vec u ; \vec x , x) =_2 0
|
| 209 |
\] |
| 210 |
Let $A_f (\vec u ; \vec x , y)$ be given by the inductive hypothesis. |
| 211 |
We define $A(\vec u ; \vec x , z)$ as: |
| 212 |
\[ |
| 213 |
\begin{array}{rl}
|
| 214 |
&\left( |
| 215 |
z=0 \ \cand \ \forall x^\safe , y^\safe . (A_f (\vec u ; \vec x , x, y) \cimp y=_2 1) |
| 216 |
\right) \\ |
| 217 |
\cor & \left( |
| 218 |
\begin{array}{ll}
|
| 219 |
z\neq 0 |
| 220 |
& \cand\ \forall y^\safe . (A_f (\vec u ; \vec x , z , y) \cimp y=_2 0 ) \\ |
| 221 |
& \cand\ \forall x^\safe < p(;z) . (\forall y^\safe . A_f (\vec u ; \vec x , x , y) \cimp y=_2 1) |
| 222 |
\end{array}
|
| 223 |
\right) |
| 224 |
\end{array}
|
| 225 |
\] |
| 226 |
Notice that $A$ is $\Pi_k$, since $A_f$ is $\Sigma_k$. |
| 227 |
|
| 228 |
|
| 229 |
|
| 230 |
What about, say recursion on a formula? Need a form of `ranked comprehension'? |
| 231 |
E.g., when $A$ is $\Sigma_k$ then we can introduce a rank $k$ symbol (a sort?) such that: |
| 232 |
\[ |
| 233 |
\forall \vec u^\normal, \vec x^\safe . \exists ! y^\safe . A(\vec u ; \vec x , y) |
| 234 |
\implies |
| 235 |
\exists f^\safe_r . \forall \vec u^\normal,\vec x^\safe, y^\safe . (A(\vec u ; \vec x, y) \ciff f^\safe_r (\vec u ; \vec x) = y ) |
| 236 |
\] |
| 237 |
|
| 238 |
Otherwise, can we use definability of computations? E.g., if: |
| 239 |
\[ |
| 240 |
\begin{array}{rcl}
|
| 241 |
f(0, \vec u ; \vec x ) & \dfn & g(\vec u ; \vec x) \\ |
| 242 |
f(s_i u , \vec u ; \vec x) & \dfn & h_i (u , \vec u ; \vec x , f(u,\vec u ; \vec x)) |
| 243 |
\end{array}
|
| 244 |
\] |
| 245 |
Suppose we have $A_g (\vec u ; \vec x,y)$ and $A_i (u , \vec u ; \vec x , y , z)$ defining $g$ and $h_i$ respectively. |
| 246 |
We define $A_f (u ,\vec u ; \vec x , y)$ as: |
| 247 |
\[ |
| 248 |
\exists z^\safe . \left( |
| 249 |
\begin{array}{ll}
|
| 250 |
& Seq(z) \cand \exists y_0 . ( A_g (\vec u ; \vec x , y_0) \cand \beta_0 (z , y_0) ) \cand \beta_{|u|} ( z,y ) \\
|
| 251 |
\cand & \forall k < |u| . \exists y_k , y_{k+1} . ( \beta_k (z, y_i) \cand \beta_{k+1} (z, y_{k+1}) \cand A_i (u , \vec u ; \vec x , y_k , y_{k+1}) )
|
| 252 |
\end{array}
|
| 253 |
\right) |
| 254 |
\] |
| 255 |
|
| 256 |
(Can we really assume $z$ is safe here?) |
| 257 |
|
| 258 |
|
| 259 |
POINT: for whatever formulation, we need to prove: |
| 260 |
\[ |
| 261 |
\exists y^\safe . A_f (a , \vec u ; \vec x , y) |
| 262 |
\quad \seqar \quad |
| 263 |
\exists y^\safe . A_f (s_i a, \vec u ; \vec x , y) |
| 264 |
\] |
| 265 |
|
| 266 |
SHOULD HAVE: $\beta (i;x)$ for $i$th element of sequence $x$. |
| 267 |
Therefore need 'sharply bounded' quantification for normal variables? |
| 268 |
|
| 269 |
In fact, why not $\beta(;i,x) $? Should be fine. So only safe quantification is needed for PH, but lose level-by-level delineation. |
| 270 |
|
| 271 |
GOALS: |
| 272 |
\begin{enumerate}
|
| 273 |
\item PVBC + FCA + $\safe$-IND characterises PH. (Recursion included in PVBC) |
| 274 |
\item Refinement of above with `ranks' to delineate levels (definitions of $\pvbci{i}$).
|
| 275 |
\item Arithmetic including both safe and sharply bounded normal quantification. (for sequences) |
| 276 |
\item (if time) allow both bounded and safe quantifiers? |
| 277 |
\end{enumerate}
|
| 278 |
|
| 279 |
|
| 280 |
|
| 281 |
FCA: |
| 282 |
\[ |
| 283 |
\exists f^\safe . \forall \vec u ; \vec x . |
| 284 |
\left( |
| 285 |
\exists y^\safe . A(\vec u ; \vec x , y) \ciff A(\vec u ; \vec x , f^\safe(\vec u ; \vec x)) |
| 286 |
\right) |
| 287 |
\] |
| 288 |
(with typing information) |
| 289 |
This could be enough with open induction if we introduce ranks later? Yup, seems like a good idea. Can then make into a real `open' theory. |
| 290 |
\end{document}
|