Révision 148
| CharacterizingPH/qpvbc.tex (revision 148) | ||
|---|---|---|
| 7 | 7 |
\input{macros}
|
| 8 | 8 |
|
| 9 | 9 |
\begin{document}
|
| 10 |
|
|
| 11 |
|
|
| 12 |
|
|
| 10 | 13 |
\section{Extending the basic BC framework}
|
| 11 | 14 |
\begin{itemize}
|
| 12 | 15 |
\item Any polynomial-time predicate can be conservatively added to BC with only safe inputs. |
| ... | ... | |
| 18 | 21 |
\section{QPVBC}
|
| 19 | 22 |
|
| 20 | 23 |
\subsection{Bellantoni's system $\pvbci{}$}
|
| 21 |
(give definition) |
|
| 22 | 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_1$ = $\fptime$. |
|
| 30 |
\item $\mubci{i}$: $\mu$BC programs with $i-1$ nested $\mu$s, i.e., corresponds to $\fphi i$.
|
|
| 31 |
\item $\pvbci i$: defined as $\pvbci{} + \Sigma^\sigma_i$-induction.
|
|
| 32 |
\end{itemize}
|
|
| 33 |
\end{definition}
|
|
| 23 | 34 |
|
| 24 | 35 |
\begin{definition}
|
| 25 | 36 |
[Provably total function] |
| ... | ... | |
| 27 | 38 |
|
| 28 | 39 |
|
| 29 | 40 |
\subsection{Extensions by induction principles}
|
| 30 |
We define the systems $\pvbci i$ as $\pvbci{} + \Sigma^\sigma_i$-induction.
|
|
| 31 | 41 |
|
| 42 |
|
|
| 43 |
|
|
| 32 | 44 |
\section{Soundness}
|
| 33 | 45 |
We show that provably total functions of $\pvbci i$ are in $\fphi i$. |
| 34 | 46 |
|
| ... | ... | |
| 130 | 142 |
\end{proof}
|
| 131 | 143 |
|
| 132 | 144 |
\section{Completeness}
|
| 145 |
Here we show that every $\mubci{i}$ function is definable in $\pvbci {i+1}$
|
|
| 133 | 146 |
|
| 134 | 147 |
|
| 135 | 148 |
\end{document}
|
Formats disponibles : Unified diff