root / CharacterizingPH / soundness.tex @ 251
Historique | Voir | Annoter | Télécharger (5,4 ko)
| 1 |
\documentclass{amsart}
|
|---|---|
| 2 |
\usepackage{amsthm}
|
| 3 |
|
| 4 |
|
| 5 |
\input{macros}
|
| 6 |
|
| 7 |
\begin{document}
|
| 8 |
\section{Logical operations as programs}
|
| 9 |
|
| 10 |
Any polynomial-time predicate can be conservatively added to BC with only safe inputs. |
| 11 |
Thus all logical connectives $\neg, \vee, \wedge$ and equality testing $=$ can be implemented as programs with only safe arguments. |
| 12 |
|
| 13 |
\section{Soundness}
|
| 14 |
We show that any provably convergent function of $I\Sigma^{N}_i$ is in $\Box_i$.
|
| 15 |
|
| 16 |
\subsection{Interpreting $\Pi_{i-1}$ formulae as programs}
|
| 17 |
Each $\Pi_{i-1}$ formula is directly interpreted, as in usual WFM, as a descriptive program evaluating whether it is true or not.
|
| 18 |
We define it by induction on formula structure: |
| 19 |
|
| 20 |
|
| 21 |
\[ |
| 22 |
\begin{array}{rcl}
|
| 23 |
\wit{s,t}{s=t} (;x) & \dfn & =(;s,t) \\
|
| 24 |
\smallskip |
| 25 |
\wit{t}{N(t)} (;x) & \dfn & =(;x,t)\\
|
| 26 |
\smallskip |
| 27 |
\wit{t}{\Box N(t)} (u;) & \dfn & =(;u,t) \\
|
| 28 |
\smallskip |
| 29 |
\wit{\vec t}{A\star B} (;x) & \dfn & \star (; \wit{\vec t}{A} (;x), \wit{\vec t}{B} (;x) ) \\
|
| 30 |
\smallskip |
| 31 |
\wit{\vec t}{\exists x^N . A(x)} (;x) & \dfn & \begin{cases}
|
| 32 |
1 & \exists a^N . \wit{a , \vec t}{A(a)} (;x) = 1 \\
|
| 33 |
0 & \text{otherwise}
|
| 34 |
\end{cases} \\
|
| 35 |
\smallskip |
| 36 |
\wit{\vec t}{\forall x^N . A(x)} (;x) & \dfn &
|
| 37 |
\begin{cases}
|
| 38 |
0 & \exists a^N. \wit{a, \vec t}{ A(a)} (;x) = 0 \\
|
| 39 |
1 & \text{otherwise}
|
| 40 |
\end{cases}
|
| 41 |
\end{array}
|
| 42 |
\] |
| 43 |
|
| 44 |
(Notice that, by free-cut elimination, $\Box$-formulae are always of the form $\Box N(t)$, so any composite formulae can be assumed to have only safe arguments. |
| 45 |
We can also assume that they always occur on the LHS of a sequent.) |
| 46 |
\subsection{Witness predicate for $\Sigma_i$ formulae}
|
| 47 |
% We give the witness predicate for $\Sigma_i$ formulae assumed to be in prenex form. |
| 48 |
When $A,B$ are $\Sigma_{i}$ we define:
|
| 49 |
\[ |
| 50 |
\begin{array}{rcl}
|
| 51 |
\wit{\vec t}{A\star B} (;\vec x , \vec y) & \dfn & \star (; \wit{\vec t}{A} (;\vec x), \wit{\vec t}{B} (;\vec y) ) \\
|
| 52 |
\smallskip |
| 53 |
\wit{\vec t}{\exists x . A( x)} (; x, \vec x) & \dfn & \wit{a, \vec t}{A( a)}(;\vec x) \left[ x^N / a\right]
|
| 54 |
\end{array}
|
| 55 |
\] |
| 56 |
(Notice that this covers all $\Sigma_i$ formulae). |
| 57 |
|
| 58 |
\subsection{Witness extraction invariant}
|
| 59 |
% We will show the following result: |
| 60 |
|
| 61 |
We will show that, if there is a proof $\pi$ of $\Gamma \seqar \Delta$, then there are programs $\vec f$ such that: |
| 62 |
\[ |
| 63 |
\wit{\vec t}{\bigwedge \Gamma} (; \vec x)
|
| 64 |
\quad \implies \quad |
| 65 |
\wit{\vec t}{\bigvee \Delta } (; \vec f (; \vec x) )
|
| 66 |
\] |
| 67 |
|
| 68 |
\subsection{Defining the programs}
|
| 69 |
We define the extracted programs inductively on a free-cut free proof. |
| 70 |
|
| 71 |
\begin{itemize}
|
| 72 |
\item $\forall$ right case. Auxiliary formula $A$ must be $\Pi_{i-1}$ by free-cut elimination.
|
| 73 |
\[ |
| 74 |
\dfrac{N(a), \Gamma \seqar \Delta , A(a)}{\Gamma \seqar \Delta , \forall x^N. A(x)}
|
| 75 |
\] |
| 76 |
By the inductive hypothesis we have functions $\vec f^\Delta , \vec f^A$ such that: |
| 77 |
\[ |
| 78 |
\wit{a , \vec t}{N(a)} (;x)
|
| 79 |
\wedge |
| 80 |
\wit{a , \vec t}{\bigwedge \Gamma} (\vec u; \vec x)
|
| 81 |
\implies |
| 82 |
\wit{a , \vec t}{\bigvee \Delta}{ (; \vec f^\Delta (\vec u ; x , \vec x))}
|
| 83 |
\vee |
| 84 |
\wit{a , \vec t}{ A} (; \vec f^A (\vec u ; x , \vec x) )
|
| 85 |
\] |
| 86 |
Since $A$ is $\Pi_{i-1}$ we can forget about $\vec f^A$.
|
| 87 |
We define $\vec g^\Delta , \vec g^{\forall x^N . A}$ as follows:
|
| 88 |
\[ |
| 89 |
\begin{array}{rcl}
|
| 90 |
\vec g^{\forall x^N . A} (\vec u ; \vec x) & \dfn & 0 \\
|
| 91 |
\vec g^\Delta (\vec u ; \vec x) & \dfn & |
| 92 |
\vec f^\Delta ( \vec u ; \mu a^N . ( \wit{a , \vec t}{A} (;0) = 0 ) , \vec x )
|
| 93 |
\end{array}
|
| 94 |
\] |
| 95 |
(Notice that the minimisation program has the same complexity as the witness predicate for $\forall x^N . A(x)$, i.e.\ $\Pi_{i-1}$.)
|
| 96 |
\item Contraction right case. Need to test the witness predicate using conditional. (No need for $\mu$s.). |
| 97 |
Given such a step, |
| 98 |
\[ |
| 99 |
\dfrac{\Gamma \seqar \Delta , A , A}{\Gamma \seqar \Delta , A}
|
| 100 |
\] |
| 101 |
by the inductive hypothesis we have programs $\vec f^\Delta , \vec f^0 , \vec f^1$ such that: |
| 102 |
\[ |
| 103 |
\wit{\vec t}{\bigwedge \Gamma} (\vec u ; \vec x)
|
| 104 |
\implies |
| 105 |
\wit{\vec t}{\bigvee \Delta} (; \vec f^\Delta (\vec u ; \vec x) )
|
| 106 |
\vee |
| 107 |
\wit{\vec t}{A} (;\vec f^0 (\vec u ; \vec x))
|
| 108 |
\vee |
| 109 |
\wit{\vec t}{A} (; \vec f^1 (\vec u ; \vec x))
|
| 110 |
\] |
| 111 |
Construct the programs $\vec g^\Delta, \vec g^A$ as follows: |
| 112 |
\[ |
| 113 |
\begin{array}{rcl}
|
| 114 |
\vec g^\Delta (\vec u ; \vec x) & \dfn & \vec f^\Delta (\vec u ; \vec x) \\ |
| 115 |
\vec g^A (\vec u; \vec x) & \dfn & |
| 116 |
\begin{cases}
|
| 117 |
\vec f^0 (\vec u ; \vec x) & \wit{\vec t}{A} (;\vec f^0(\vec u ; \vec x) =1 ) \\
|
| 118 |
\vec f^1 (\vec u ; \vec x) & \text{otherwise}
|
| 119 |
\end{cases}
|
| 120 |
\end{array}
|
| 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 |
\] |
| 147 |
\end{itemize}
|
| 148 |
\subsection{Proof of correctness}
|
| 149 |
|
| 150 |
\end{document}
|