Révision 144 CharacterizingPH/soundness.tex

soundness.tex (revision 144)
24 24 
	\smallskip
25 25 
	\wit{t}{N(t)} (;x) & \dfn & =(;x,t)\\
26 26 
	\smallskip
27 
	\wit{t}{\Box N(t)} (u;) & \dfn & =(;u,t) \\
28 
	\smallskip
27 29 
	\wit{\vec t}{A\star B} (;x) & \dfn & \star (; \wit{\vec t}{A} (;x), \wit{\vec t}{B} (;x) ) \\
28 30 
	\smallskip
29 31 
	\wit{\vec t}{\exists x^N . A(x)} (;x) & \dfn & \begin{cases}
......
39 41 
	\end{array}
40 42 
	\]
41 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.)
42 46 
	\subsection{Witness predicate for $\Sigma_i$ formulae}
43 47 
%	We give the witness predicate for $\Sigma_i$ formulae assumed to be in prenex form.
44 48 
	When $A,B$ are $\Sigma_{i}$ we define:
......
65 69 
	We define the extracted programs inductively on a free-cut free proof.
66 70
67 71 
	\begin{itemize}
68 
		\item $\forall$ cases: auxiliary formula ($A$) must be $\Pi_{i-1}$ by free-cut elimination.
72 
	\item $\forall$ right case. Auxiliary formula $A$ must be $\Pi_{i-1}$ by free-cut elimination.
69 73 
		\[
70 74 
		\dfrac{N(a), \Gamma \seqar \Delta , A(a)}{\Gamma \seqar \Delta , \forall x^N. A(x)}
71 75 
		\]
72
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 
	\]
73 122 
	\end{itemize}
74 123 
	\subsection{Proof of correctness}
75 124

Formats disponibles : Unified diff