Révision 145
| CharacterizingPH/soundness.tex (revision 145) | ||
|---|---|---|
| 119 | 119 |
\end{cases}
|
| 120 | 120 |
\end{array}
|
| 121 | 121 |
\] |
| 122 |
\item Induction. NB: Can assume no side-formulae on the right!! |
|
| 123 |
\[ |
|
| 124 |
\dfrac{\Box N(a), \Gamma, A(a) \seqar A(s_i a)}{\Box N(s), \Gamma , A(0) \seqar A(s)}
|
|
| 125 |
\] |
|
| 126 |
We need to keep track of all the terms in the witness predicate. |
|
| 127 |
\[ |
|
| 128 |
% \begin{array}{rl}
|
|
| 129 |
% &\wit{a, t(a), t(s_i a), \vec t}{LHS} (u , \vec u ; \vec x , \vec y)
|
|
| 130 |
% \\ |
|
| 131 |
% \implies & |
|
| 132 |
% \wit{a , t(a), t(s_i a), \vec t}{A(s_i a)} (; \vec f^A (u , \vec u ; \vec x , \vec y) )
|
|
| 133 |
% \vee |
|
| 134 |
% \wit{a , t(a), t(s_i a), \vec t}{\bigvee \Delta} (; \vec f^\Delta (u , \vec u ; \vec x , \vec y) )
|
|
| 135 |
% \end{array}
|
|
| 136 |
\wit{a, t(a), t(s_i a), \vec t}{LHS} (u , \vec u ; \vec x , \vec y)
|
|
| 137 |
\implies |
|
| 138 |
\wit{a , t(a), t(s_i a), \vec t}{A(s_i a)} (; \vec f^i (u , \vec u ; \vec x , \vec y) )
|
|
| 139 |
\] |
|
| 140 |
Define $\vec g$ by safe recursion as follows: |
|
| 141 |
\[ |
|
| 142 |
\begin{array}{rcl}
|
|
| 143 |
\vec g (0 , \vec u ; \vec x , \vec y) & \dfn & \vec y \\ |
|
| 144 |
\vec g (s_i u, \vec u ; \vec x , \vec y) & \dfn & \vec f^i ( u, \vec u; \vec x, \vec g (u, \vec u ; \vec x , \vec y) ) |
|
| 145 |
\end{array}
|
|
| 146 |
\] |
|
| 122 | 147 |
\end{itemize}
|
| 123 | 148 |
\subsection{Proof of correctness}
|
| 124 | 149 |
|
| CharacterizingPH/macros.tex (revision 145) | ||
|---|---|---|
| 1 |
\newcommand{\wit}[2]{\mathit{Wit}^{#1}_{#2}}
|
|
| 1 |
\newcommand{\nb}[1]{{\color{blue} NB: #1}}
|
|
| 2 |
|
|
| 3 |
\newtheorem{theorem}{Theorem}
|
|
| 4 |
\newtheorem{proposition}[theorem]{Proposition}
|
|
| 5 |
\newtheorem{lemma}[theorem]{Lemma}
|
|
| 6 |
|
|
| 7 |
|
|
| 8 |
\theoremstyle{definition}
|
|
| 9 |
\newtheorem{definition}[theorem]{Definition}
|
|
| 10 |
|
|
| 11 |
|
|
| 12 |
\newcommand{\wit}[2]{\mathit{wit}^{#1}_{#2}}
|
|
| 13 |
\newcommand{\Wit}[2]{\mathit{Wit}^{#1}_{#2}}
|
|
| 2 | 14 |
\newcommand{\dfn}{:=}
|
| 3 | 15 |
\newcommand{\seqar}{\rightarrow}
|
| 16 |
\newcommand{\proves}{\vdash}
|
|
| 17 |
|
|
| 18 |
|
|
| 19 |
\newcommand{\safe}{\sigma}
|
|
| 20 |
\newcommand{\normal}{\nu}
|
|
| 21 |
|
|
| 22 |
\newcommand{\pv}{\mathit{PV}}
|
|
| 23 |
\newcommand{\pvbci}[1]{\pv^{#1}_{\mathrm{BC}}}
|
|
| 24 |
\newcommand{\mubci}[1]{\mu\mathrm{BC}^{#1}}
|
|
| 25 |
|
|
| 26 |
\newcommand{\fphi}[1]{\Box_{#1}}
|
|
| 27 |
\newcommand{\ph}{\mathbf{PH}}
|
|
| 28 |
\newcommand{\pspace}{\mathbf{PSPACE}}
|
|
| 29 |
\newcommand{\fpspace}{\mathbf{FPSPACE}}
|
|
| 30 |
\newcommand{\ptime}{\mathbf{P}}
|
|
| 31 |
\newcommand{\fptime}{\mathbf{FP}}
|
|
| 32 |
\newcommand{\nc}{\mathbf{NC}}
|
|
| 33 |
\newcommand{\ac}{\mathbf{AC}}
|
|
| 34 |
\newcommand{\exptime}{\mathbf{EXP}}
|
|
| 35 |
|
|
| 36 |
|
|
| 37 |
\newcommand{\cimp}{\supset}
|
|
| 38 |
\newcommand{\cor}{\vee}
|
|
| 39 |
\newcommand{\cand}{\wedge}
|
|
Formats disponibles : Unified diff