root / CSL16 / wfm.tex @ 43
Historique | Voir | Annoter | Télécharger (19,56 ko)
| 1 |
\section{Witness function method}
|
|---|---|
| 2 |
|
| 3 |
Key features/differences from realisability: |
| 4 |
\begin{itemize}
|
| 5 |
\item De Morgan normal form: reduces type level to $0$, complementary to double-negation translation that \emph{increases} type level.
|
| 6 |
\item Free-cut elimination: allows us to handles formulae of fixed logical complexity throughout the proof. |
| 7 |
\item Respects logical properties of formulae, e.g.\ quantifier complexity, exponential complexity. |
| 8 |
\end{itemize}
|
| 9 |
|
| 10 |
\todo{say some more here}
|
| 11 |
|
| 12 |
\todo{compare with applicative theories}
|
| 13 |
|
| 14 |
\anupam{in particular, need to point out that this argument is actually something in between, since usually the WFM requires programs to be defined by formulae, not equational specifications.}
|
| 15 |
|
| 16 |
\newcommand{\type}{\mathtt{t}}
|
| 17 |
\newcommand{\norm}{\nu}
|
| 18 |
\newcommand{\safe}{\sigma}
|
| 19 |
|
| 20 |
|
| 21 |
|
| 22 |
\subsection{The translation}
|
| 23 |
|
| 24 |
\begin{definition}
|
| 25 |
[Typing] |
| 26 |
To each $\Sigma^\nat_1$-formula $A$ we associate a sorted tuple of variables $\type (A)$, intended to range over $\Nat$, as follows: |
| 27 |
\[ |
| 28 |
\begin{array}{rcll}
|
| 29 |
\type (\nat (t)) & := & (;x^{\nat (t)} ) & \\
|
| 30 |
\type(s = t) & := & ( ; x^{s = t}) & \\
|
| 31 |
\type (A \lor B) & : = & (\vec u , \vec v ; \vec x , \vec y) & \text{if $\type(A) = (\vec u ; \vec x)$ and $\type(B) = (\vec v ; \vec y)$.} \\
|
| 32 |
\type (A \land B) & : = & (\vec u , \vec v ; \vec x , \vec y) & \text{if $\type(A) = (\vec u ; \vec x)$ and $\type(B) = (\vec v ; \vec y)$.} \\
|
| 33 |
\type (! A) & : = & ( \vec u ,\vec x ; ) & \text{if $\type(A) = (\vec u ; \vec x )$.} \\
|
| 34 |
\type (\exists x^\nat . A) & := & (\vec u ; \vec x , y) & \text{if $\type (A) = (\vec u ; \vec x)$.}
|
| 35 |
% \type (\forall x^N . A) & := & \Nat \to \type(A) |
| 36 |
\end{array}
|
| 37 |
\] |
| 38 |
% where $\nu$ designates that the inputs are normal. |
| 39 |
\end{definition}
|
| 40 |
|
| 41 |
|
| 42 |
\anupam{need to account for normality and safety somewhere. Attempting inlined and leaving types without this decoration.}
|
| 43 |
|
| 44 |
\begin{remark}
|
| 45 |
[Distribution of $!$] |
| 46 |
There is a potential issue that the $!$ contains $\lor$ symbols in its scope, whence we do not in general have $!(A \lor B) \cong !A \lor !B$. However this will not be a problem here by inspection of a convergence statement: there are no $\lor$ symbols in the scope of a $!$. Therefore, after free-cut elimination, no formula in the proof will have this property either. |
| 47 |
|
| 48 |
On the other hand, since we are working in affine logic, we do in general have $!(A \land B) \cong !A \land !B$. |
| 49 |
\end{remark}
|
| 50 |
|
| 51 |
\begin{definition}
|
| 52 |
[Translation] |
| 53 |
We give a translation of free-cut free $\Sigma^\nat_1$-$\pind$ proofs $\pi$ of sequents $\Gamma(\vec a) \seqar \Delta(\vec a)$ to BC-programs for a vector of functions $\vec f^\pi$ with argument of type $\type \left(\bigotimes\Gamma\right)$ such that $|\vec f^\pi | = | \type\left(\bigparr\Delta\right)|$. |
| 54 |
|
| 55 |
|
| 56 |
The translation is by induction on the size of a free-cut free proof, so we proceed by analysis of the final step of a proof. |
| 57 |
|
| 58 |
If $\pi$ is simply an axiom, we construct $\vec f^\pi$ as follows: |
| 59 |
\[ |
| 60 |
\begin{array}{ccc}
|
| 61 |
\vlinf{\natcntr}{}{\nat(t) \seqar \nat(t) \land \nat(t) }{}
|
| 62 |
& : & |
| 63 |
( \id (;x) , \id (;x) ) |
| 64 |
\\ |
| 65 |
\vlinf{\nat_\epsilon}{}{\seqar \nat (\epsilon)}{}
|
| 66 |
& : & |
| 67 |
\epsilon |
| 68 |
\\ |
| 69 |
\vlinf{\nat_0}{}{\nat(t) \seqar \nat(\succ_0 t)}{}
|
| 70 |
& : & |
| 71 |
\succ_0 ( ;x) |
| 72 |
\\ |
| 73 |
\vlinf{\nat_1}{}{\nat(t) \seqar \nat(\succ_1 t)}{}
|
| 74 |
& : & |
| 75 |
\succ_1 (; x) |
| 76 |
\\ |
| 77 |
\vlinf{\epsilon^0}{}{ \nat (t) , \epsilon = \succ_0 t \seqar }{}
|
| 78 |
& : & |
| 79 |
\epsilon |
| 80 |
\\ |
| 81 |
\vlinf{\epsilon^1}{}{ \nat (t) , \epsilon = \succ_1 t \seqar }{}
|
| 82 |
& : & |
| 83 |
\epsilon |
| 84 |
\\ |
| 85 |
\vlinf{\succ_0}{}{\nat (s) , \nat (t) , \succ_0 s = \succ_0 t\seqar s = t }{}
|
| 86 |
& : & |
| 87 |
\epsilon |
| 88 |
\\ |
| 89 |
\vlinf{\succ_1}{}{\nat (s) , \nat (t) , \succ_1 s = \succ_1 t\seqar s = t }{}
|
| 90 |
& : & |
| 91 |
\epsilon |
| 92 |
\\ |
| 93 |
\vlinf{\inj}{}{\nat(t), \succ_0 t = \succ_1 t \seqar}{}
|
| 94 |
& : & |
| 95 |
\epsilon |
| 96 |
\\ |
| 97 |
\vlinf{\surj}{}{\nat (t) \seqar t = \epsilon , \exists y^\nat . t = \succ_0 y , \exists y^\nat . t = \succ_1 y }{}
|
| 98 |
&: & |
| 99 |
( \epsilon , \pred ( ;x) , \pred (;x ) ) |
| 100 |
\end{array}
|
| 101 |
\] |
| 102 |
|
| 103 |
\anupam{axioms which are true and contain no computational information currently interpreted as constant $\epsilon$. Check this/typing again to make sure plays nice.}
|
| 104 |
\anupam{check $\surj$.}
|
| 105 |
|
| 106 |
|
| 107 |
Suppose $\pi$ ends with a $\rigrul{\land}$ step:
|
| 108 |
\[ |
| 109 |
\vlderivation{
|
| 110 |
\vliin{\land}{}{ \Gamma, \Sigma \seqar \Delta, \Pi, A\land B }{
|
| 111 |
\vltr{\pi_1}{ \Gamma \seqar \Delta, A }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}
|
| 112 |
}{
|
| 113 |
\vltr{\pi_2}{ \Sigma \seqar \Pi, B }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}
|
| 114 |
} |
| 115 |
} |
| 116 |
\] |
| 117 |
By the inductive hypothesis let us suppose we have functions $\vec g (\vec u; \vec x)$ and $\vec h (\vec v ; \vec y)$ from $\pi_1$ and $\pi_2$ respectively, where $\type\left( \bigotimes\Gamma \right) = (\vec u; \vec x)$ and $\type \left( \bigotimes \Sigma \right) = (\vec v ; \vec y)$. Let us write $\vec g = (\vec g^\Delta , \vec g^A)$ and $\vec h = (\vec h^\Pi , \vec h^B)$, to denote the $\Delta$ and $A$ parts of $\vec g$ and the $\Pi$ and $B$ parts of $\vec h$. |
| 118 |
% So we have $\vec f^{1} (\vec x ; \vec a)$ and $\vec f^2 (\vec y ; \vec b)$ for $\pi_1 $ and $\pi_2$ respectively, by the inductive hypothesis.
|
| 119 |
We simply construct $\vec f^\pi$ by rearranging these tuples of functions: |
| 120 |
\[ |
| 121 |
\vec f^\pi (\vec u , \vec v ; \vec x , \vec y) |
| 122 |
\quad := \quad |
| 123 |
\left( |
| 124 |
\vec g^\Delta (\vec u ; \vec x) , \vec h^\Pi (\vec v ; \vec y) , \vec g^A (\vec u ; \vec x) , \vec h^B (\vec v ; \vec y) |
| 125 |
\right) |
| 126 |
\] |
| 127 |
|
| 128 |
We will continue with a similar notational convention as above in the remainder of this argument. |
| 129 |
|
| 130 |
% \anupam{bad notation since need to include free variables of sequent too. (also of theory.) Reconsider.}
|
| 131 |
|
| 132 |
The case when $\pi$ ends with a $\lefrul{\lor}$ step is analogous to the $\rigrul{\land}$ case above.
|
| 133 |
|
| 134 |
If $\pi$ consists of a subproof $\pi'$ ending with a $\lefrul{\land}$ or $\rigrul{\lor}$-step, then $\vec f^\pi$ is exactly $\vec f^{\pi'}$.
|
| 135 |
|
| 136 |
Suppose $\pi$ ends with a $\lefrul{\cntr}$ step,
|
| 137 |
\[ |
| 138 |
\vlderivation{
|
| 139 |
\vlin{\lefrul{\cntr}}{}{ !A , \Gamma \seqar \Delta }{
|
| 140 |
\vltr{\pi'}{ !A, !A , \Gamma \seqar \Delta}{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}
|
| 141 |
} |
| 142 |
} |
| 143 |
\] |
| 144 |
so we have functions $\vec f ( \vec u^1, \vec u^2 , \vec v ; \vec x)$ with $\vec u^1$ and $\vec u^2$ corresponding to the two copies of $!A$ in the conclusion of $\pi'$, respectively, and $\type (\Gamma) = (\vec v; \vec x)$. (Recall that the typing corresponding to $!$ means that all inputs for each $!A$ are normal). We define $\vec f^\pi$ as expected, duplicating the arguments for $!A$: |
| 145 |
\[ |
| 146 |
\vec f^\pi (\vec u , \vec v ; \vec x) |
| 147 |
\quad := \quad |
| 148 |
\vec f (\vec u, \vec u , \vec v ; \vec x) |
| 149 |
\] |
| 150 |
(Notice that this is obtainable in BC by a trivial instance of safe composition.) |
| 151 |
|
| 152 |
|
| 153 |
% cntr right |
| 154 |
% \[ |
| 155 |
% \vlderivation{
|
| 156 |
% \vlin{\rigrul{\cntr}}{}{\Gamma \seqar \Delta, ?A}{
|
| 157 |
% \vltr{\pi'}{ \Gamma \seqar \Delta, ?A, ?A}{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}
|
| 158 |
% } |
| 159 |
% } |
| 160 |
% \] |
| 161 |
% (need test function against witness predicate?) |
| 162 |
% |
| 163 |
% \anupam{problem: how to test even equality of two terms? Maybe treat $?$ as $!$ on left?}
|
| 164 |
% |
| 165 |
% \anupam{Not a problem by free-cut elimination! Can assume there are no $?$ in the proof! Is this equivalent to treaing $?$ as $!$ on left?}
|
| 166 |
% |
| 167 |
% \anupam{Yes I think so. We can work in a left-sided calculus. only problem is for induction. But this can never be a problem for modalities since induction formulae are modality-free.}
|
| 168 |
% |
| 169 |
% \anupam{this is actually the main point.}
|
| 170 |
|
| 171 |
For $\rigrul{\cntr}$, notice that no $?$-symbol occurs in a convergence statement, an initial step or an induction formula, so a free-cut free proof is free of $\rigrul{\cntr}$-steps.
|
| 172 |
|
| 173 |
\anupam{This is important, so expand on this here or in a remark before/after.}
|
| 174 |
|
| 175 |
|
| 176 |
% \[ |
| 177 |
% \vlderivation{
|
| 178 |
% \vliin{\rigrul{\laand}}{}{\Gamma \seqar \Delta, A \laand B}{
|
| 179 |
% \vltr{\pi_1}{ \Gamma \seqar \Delta, A}{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}
|
| 180 |
% }{
|
| 181 |
% \vltr{\pi_2}{ \Gamma \seqar \Delta, B}{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}
|
| 182 |
% } |
| 183 |
% } |
| 184 |
% \] |
| 185 |
% |
| 186 |
% Suppose we have $\vec f^i (\vec x , \vec a ; \vec y , \vec b)$ from $\pi_i$. |
| 187 |
% |
| 188 |
% \anupam{problem: does this require many tests, just like for contraction? Can we isolate a different complexity class? e.g.\ PH or Grzegorzyck?}
|
| 189 |
% \anupam{skip this case and consider later.}
|
| 190 |
|
| 191 |
\anupam{commented stuff on additives. To remark later perhaps.}
|
| 192 |
|
| 193 |
|
| 194 |
|
| 195 |
Suppose $\pi$ ends with a $\rigrul{\exists}$ step,
|
| 196 |
\[ |
| 197 |
\vlderivation{
|
| 198 |
\vlin{\rigrul{\exists}}{}{ \Gamma, \nat(t) \seqar \Delta , \exists x^\nat . A(x) }{
|
| 199 |
\vltr{\pi'}{ \Gamma \seqar \Delta , A(t) }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}
|
| 200 |
} |
| 201 |
} |
| 202 |
\] |
| 203 |
so by the inductive hypothesis we have functions $\vec f^\Delta , \vec f^{A(t)}$ with arguments $(\vec u ; \vec x )= \type(\bigotimes \Gamma)$. We define $\vec f^\pi$ as follows:
|
| 204 |
\[ |
| 205 |
\vec f^\pi (\vec u ; \vec x , y) |
| 206 |
\quad := \quad |
| 207 |
\left( \vec f^\Delta (\vec u ; \vec x) , \id (;y), \vec{ f}^{A(t)} (\vec u; \vec x) \right)
|
| 208 |
\] |
| 209 |
(The identity function on $y$ is defined from successor, predecessor and safe composition). |
| 210 |
|
| 211 |
|
| 212 |
%Suppose we have functions $\vec f^X (\vec x ; \vec y)$ from $\pi'$ for $X = \Delta$ or $ X=A$. |
| 213 |
%\[ |
| 214 |
%\vec f(\vec x ; \vec y , z) \quad := \quad ( \vec f^\Delta (\vec x ; \vec y) , z , \vec f^A ( \vec x ; \vec y ) ) |
| 215 |
%\] |
| 216 |
|
| 217 |
|
| 218 |
Suppose $\pi$ ends with a $\lefrul{\exists}$ step:
|
| 219 |
\[ |
| 220 |
\vlderivation{
|
| 221 |
\vlin{\lefrul{\exists}}{}{ \Gamma, \exists x^N . A(x) \seqar \Delta }{
|
| 222 |
\vltr{\pi'(a)}{ \Gamma , A(a), N(a) \seqar \Delta }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}
|
| 223 |
} |
| 224 |
} |
| 225 |
\] |
| 226 |
% |
| 227 |
%Suppose we have functions $\vec f' (\vec u , \vec v ; x , \vec y , \vec z)$ from $\pi'$ with $(\vec u ; \vec x )$ corresponding to $\Gamma$, $(;x)$ corresponding to $N(a)$ and $(\vec v ; \vec z)$ corresponding to $A(a)$. We define: |
| 228 |
%\[ |
| 229 |
%\vec f ( \vec u , \vec v ; ) |
| 230 |
%\] |
| 231 |
|
| 232 |
\anupam{should just be same? Consider variable naming, just in case.}
|
| 233 |
\anupam{This is probably where the consideration for free variables is.}
|
| 234 |
|
| 235 |
%Suppose we have functions $\vec g (\vec v , \vec w ; \vec x , y , \vec z)$ where $(\vec v ; \vec x) $ corresponds to $\Gamma$, $y$ corresponds to $\nat(a)$ and $(\vec w ; \vec z) $ corresponds to $A(a)$. Then we define: |
| 236 |
%\[ |
| 237 |
%\vec f ( \vec v , \vec w ; \vec x , y , \vec z ) |
| 238 |
%\] |
| 239 |
|
| 240 |
|
| 241 |
Suppose $\pi$ ends with a $\cut$ step: |
| 242 |
\[ |
| 243 |
\vlderivation{
|
| 244 |
\vliin{\cut}{}{\Gamma , \Sigma \seqar \Delta , \Pi}{
|
| 245 |
\vltr{\pi_1}{ \Gamma \seqar \Delta, A }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}
|
| 246 |
}{
|
| 247 |
\vltr{\pi_2}{\Sigma , A \seqar \Pi}{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}
|
| 248 |
} |
| 249 |
} |
| 250 |
\] |
| 251 |
|
| 252 |
We have two cases. First, if $A$ is free of modalities, then $\type (A)$ consists of only safe inputs. Therefore we have functions $\vec g (\vec u; \vec x)$ and $\vec h (\vec v ; \vec y, \vec z)$ from $\pi_1$ and $\pi_2 $ respectively, such that $\type(\Gamma) = (\vec u ; \vec x)$, $\type(\Sigma) = (\vec v ; \vec y )$ and $\type (A) = (;\vec z)$. Let us write $\vec g = (\vec g^\Delta , \vec g^A)$ as before, and we define $\vec f^\pi$ as follows: |
| 253 |
|
| 254 |
\[ |
| 255 |
\vec f^\pi ( \vec u , \vec v ; \vec x, \vec y) |
| 256 |
\quad := \quad |
| 257 |
\left( |
| 258 |
\vec g^\Delta (\vec u ; \vec x) |
| 259 |
, |
| 260 |
\vec h ( \vec v ; \vec y , \vec g^A ( \vec u ; \vec x ) ) |
| 261 |
\right) |
| 262 |
\] |
| 263 |
(Notice that all safe inputs are hereditarily safe in these expressions, so they are definable by safe composition and projection). |
| 264 |
|
| 265 |
|
| 266 |
|
| 267 |
|
| 268 |
In the other case, where $A$ may be modal, it must be of the form $!\nat (t)$ since it is a cut formula, and so must directly descend from an induction step or axiom on one side. The only such occurrence of a modality is in the conclusion of an induction step, whence such a formula has the form $!\nat (t)$. By free-cut elimination we can also assume that this cut formula is principal on \emph{both} sides, i.e.\ $\pi$ is of the form:
|
| 269 |
|
| 270 |
\anupam{need to check this assumption against free-cut elimination conditions. To discuss.}
|
| 271 |
|
| 272 |
\[ |
| 273 |
\vlderivation{
|
| 274 |
\vliin{\cut}{}{!\Gamma , !\Sigma , A(\epsilon) \seqar A(t) }{
|
| 275 |
% \vlin{\rigrul{!}}{}{!\Gamma \seqar ?\Delta, !\nat(t)}{
|
| 276 |
\vltr{\pi_1}{!\Gamma \seqar !\nat(t)}{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}
|
| 277 |
% } |
| 278 |
}{
|
| 279 |
\vltr{\pi_2}{ !\Sigma, !\nat(t) , A(\epsilon)\seqar A(t) }{\vlhy{\quad}}{\vlhy{}}{\vlhy{\quad}}
|
| 280 |
} |
| 281 |
} |
| 282 |
\] |
| 283 |
where $\pi_1$ ends with a $\rigrul{!}$ step for which $!\nat (t)$ is principal, $\pi_2$ ends with a $\pind$ step where $A(x)$ is the induction formula, and we assume there are no side-formulae on the right of both conclusions for the same reason as $\rigrul{\cntr}$: a free-cut free proof of a convergence statement contains no $?$ symbol.
|
| 284 |
|
| 285 |
So by the inductive hypothesis we have functions $ g( \vec u ; )$ and $\vec h ( \vec v , w ; \vec x)$ from $\pi_1$ and $\pi_2$ respectively, where $\vec u$, $\vec v$, $w$ and $\vec x$ correspond to $!\Gamma$, $!\Sigma$, $!\nat(t)$ (in $\pi_2$) and $A(\epsilon)$ respectively. We construct the functions $\vec f^\pi $ as follows: |
| 286 |
\[ |
| 287 |
\vec f^\pi (\vec u , \vec v ; \vec x) |
| 288 |
\quad := \quad |
| 289 |
\vec h ( \vec v , g(\vec u ; ) ; \vec x) |
| 290 |
\] |
| 291 |
(Notice that this is definable by safe composition and projection since all safe inputs $\vec x$ are hereditarily safe on the right.) |
| 292 |
|
| 293 |
|
| 294 |
Suppose $\pi$ ends with a $\lefrul{!}$ step:
|
| 295 |
\[ |
| 296 |
\vlderivation{
|
| 297 |
\vlin{!}{}{\Gamma, !A \seqar \Delta}{
|
| 298 |
\vltr{\pi'}{ \Gamma , A \seqar \Delta }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}
|
| 299 |
} |
| 300 |
} |
| 301 |
\] |
| 302 |
\todo{finish this case, just passing a safe input to a normal input.}
|
| 303 |
|
| 304 |
|
| 305 |
Suppose $\pi$ ends with a $\rigrul{!}$ step:
|
| 306 |
|
| 307 |
\todo{finish this case, should not change function at all, but maybe there is a consideration.}
|
| 308 |
|
| 309 |
Suppose $\pi$ ends with a $\lefrul{\wk}$ step:
|
| 310 |
|
| 311 |
\todo{finish this case, just add a dummy input.}
|
| 312 |
|
| 313 |
Suppose $\pi$ ends with a $\rigrul{\wk}$ step:
|
| 314 |
|
| 315 |
\todo{finish this case, just add a dummy function.}
|
| 316 |
|
| 317 |
|
| 318 |
|
| 319 |
Suppose $\pi$ ends with a $\pind$ step. For the same reason as $\rigrul{\cntr}$ we can assume there are no $?$ formulae and so no side formulae on the right. Thus a $\pi$ has the following form:
|
| 320 |
\[ |
| 321 |
\vlderivation{
|
| 322 |
\vliin{\pind}{}{ !\nat (t), !\Gamma , A(\epsilon) \seqar A(t) }{
|
| 323 |
\vltr{\pi_0}{!\nat(a) , !\Gamma , A(a) \seqar A(\succ_0 a)}{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}
|
| 324 |
}{
|
| 325 |
\vltr{\pi_1}{!\nat(a), !\Gamma , A(a)\seqar A(\succ_1 a) }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}
|
| 326 |
} |
| 327 |
} |
| 328 |
\] |
| 329 |
\anupam{is this better with a premiss for the base case?}
|
| 330 |
|
| 331 |
By the inductive hypothesis we have functions $\vec g^0 (u , \vec v ; \vec x)$ and $\vec g^1 (u , \vec v ; \vec x)$ with $u$, $\vec v$ and $\vec x$ corresponding to $!\nat(a)$, $!\Gamma$ and $A(a)$ respectively. We define $\vec f^\pi$ by (simultaneous) predicative recursion on notation as follows: |
| 332 |
\[ |
| 333 |
\begin{array}{rcll}
|
| 334 |
\vec f^\pi ( \epsilon, \vec v ; \vec x ) & := & \vec x & \\ |
| 335 |
\vec f^\pi ( \succ_i u , \vec v ; \vec x) & := & \vec g^i ( u, \vec v ; \vec f^\pi ( u, \vec v ; \vec x ) ) |
| 336 |
\end{array}
|
| 337 |
\] |
| 338 |
|
| 339 |
\anupam{check this}
|
| 340 |
|
| 341 |
\todo{simultaneous PRN.}
|
| 342 |
|
| 343 |
|
| 344 |
\end{definition}
|
| 345 |
|
| 346 |
\subsection{Witness predicate and extensional equivalence of functions}
|
| 347 |
|
| 348 |
Now that we have defined how to extract a function from a proof, we need to show that the function satisfies the appropriate semantic properties. |
| 349 |
|
| 350 |
For this we work in a quantifier-free logic whose atoms are equations between terms of our arithmetic and whose (sound) rules are simply the axioms of our arithmetic. |
| 351 |
|
| 352 |
(This is similar to the role of PV in the witnessing argument for $S^1_2$ and system $T$ for witnessing $I\Sigma_1$.) |
| 353 |
|
| 354 |
|
| 355 |
\newcommand{\witness}[2]{\mathit{Witness}^{#1}_{#2}}
|
| 356 |
\begin{definition}
|
| 357 |
[Witness predicate] |
| 358 |
We define the following `witness' predicate for $\Sigma^\nat_1$-formulae $A$ with free variables amongst $\vec a$: |
| 359 |
\[ |
| 360 |
\begin{array}{rcll}
|
| 361 |
\witness{\vec a}{A} (w, \vec b) & := & w = t(\vec b) & \text{if $A(\vec a)$ is $\nat (t(\vec a))$.} \\
|
| 362 |
\witness{\vec a}{A} (w, \vec b) & := & s(\vec b) = t(\vec b) & \text{if $A(\vec a)$ is $s(\vec a) = t (\vec a)$.} \\
|
| 363 |
\witness{\vec a}{A \lor B} ( \vec w^1 , \vec w^2, \vec b ) & := & \witness{\vec a}{A} (\vec w^1 , \vec b) \cor \witness{\vec a}{B} (\vec w^2 , \vec b) &
|
| 364 |
% \text{for $\star \in \{ \land, \lor, \laand , \laor\}$.}
|
| 365 |
\\ |
| 366 |
\witness{\vec a}{A \land B} ( \vec w^1 , \vec w^2, \vec b ) & := & \witness{\vec a}{A} (\vec w^1 , \vec b) \cand \witness{\vec a}{B} (\vec w^2 , \vec b) &
|
| 367 |
% \text{for $\star \in \{ \land, \lor, \laand , \laor\}$.}
|
| 368 |
\\ |
| 369 |
\witness{\vec a}{\exists x^\nat . A(x)} ( w, \vec w , \vec b) & := & \witness{\vec{a}, a}{A(a)}(\vec w , \vec b, w ) & \\
|
| 370 |
\end{array}
|
| 371 |
\] |
| 372 |
where $|\vec w^1| = |\type (A)|$ and $|\vec w^2| = |\type (B)| $. |
| 373 |
\end{definition}
|
| 374 |
% \todo{problem: what about complexity of checking equality? }
|
| 375 |
|
| 376 |
\todo{Reformulate above later if necessary.}
|
| 377 |
|
| 378 |
% \todo{What about $\nat (t)$? What does it mean? Replace with true?}
|
| 379 |
|
| 380 |
% \todo{either use the witness predicate above, or use realizability predicate at meta-level and a model theory, like BH.}
|
| 381 |
|
| 382 |
% \anupam{Need to check above properly. $N(t)$ should be witnessed by the value of $t $ in the model. For equality of terms the witness should not do anything.}
|
| 383 |
|
| 384 |
\anupam{to consider/remark: formally, is witness predicate checked in model or some logical theory?}
|
| 385 |
|
| 386 |
|
| 387 |
|
| 388 |
|
| 389 |
\begin{lemma}
|
| 390 |
Suppose $\pi$ is a free-cut free $\Sigma^\nat_1$-$\pind$ proof of a sequent $\Gamma (\vec a) \seqar \Delta (\vec a)$, with $\vec f^\pi$ defined as above. Then: |
| 391 |
\[ |
| 392 |
\witness{\vec a}{\bigotimes \Gamma} (\vec w , \vec b) \implies \witness{\vec a}{\bigparr \Delta } (\vec f^\pi(\vec w , \vec b), \vec b)
|
| 393 |
\] |
| 394 |
\end{lemma}
|
| 395 |
|
| 396 |
|
| 397 |
\anupam{to consider: do we need parameters $\vec a$ in argument of $f$? Or does $\nat$ predicate take care of this?}
|
| 398 |
|
| 399 |
% We will be explicit about normal and safe inputs when necessary, for the most part we will simply rearrange inputs into lists $(\vec u; \vec a)$ as in BC framework. |
| 400 |
|
| 401 |
% We often suppress the parameters $\vec a$ when it is not important. |
| 402 |
|
| 403 |
\anupam{Is this implication provable in Bellantoni's version of PV based on BC?}
|
| 404 |
|
| 405 |
% \anupam{for moment try ignore decoration on right? what about negation?}
|
| 406 |
|
| 407 |
|
| 408 |
\begin{proof}
|
| 409 |
By structural induction on $\pi$, again, following the definition of $\vec f^\pi$. |
| 410 |
\todo{}
|
| 411 |
\end{proof}
|
| 412 |
|
| 413 |
\begin{theorem}
|
| 414 |
If we can prove a convergence statement for a function $f$ under a specification $\Phi(f)$ then there is a BC-program for a function $\mathbf f$ such that: |
| 415 |
\begin{equation}
|
| 416 |
\label{eqn:spec-implies-program}
|
| 417 |
\Phi(f) \implies f (\vec x) = \mathbf{f} (\vec x)
|
| 418 |
\end{equation}
|
| 419 |
\begin{equation}
|
| 420 |
\label{eqn:program-satisfies-spec}
|
| 421 |
\Phi(\mathbf f) |
| 422 |
\end{equation}
|
| 423 |
\end{theorem}
|
| 424 |
\begin{proof}
|
| 425 |
Notice that a convergence statement has the following form: |
| 426 |
\[ |
| 427 |
!\Phi(f) , !\nat(\vec a) \seqar \nat(f (\vec a) ) |
| 428 |
\] |
| 429 |
By the lemma above, and by inspection of the definition of the witness predicate, this means we have that, |
| 430 |
\[ |
| 431 |
(\Phi(f) \cand \vec x = \vec a ) \implies \mathbf f (\vec x) = f(\vec a) |
| 432 |
\] |
| 433 |
whence we arrive at \eqref{eqn:spec-implies-program}.
|
| 434 |
|
| 435 |
Finally, notice that $\Phi(f)$ has \emph{some} model, since it is a monotone inductive definition so some fixed point must exist. Therefore we obtain \eqref{eqn:program-satisfies-spec} as well.
|
| 436 |
\end{proof}
|
| 437 |
|
| 438 |
\anupam{rephrase above proof to make more sense.}
|
| 439 |
|
| 440 |
|
| 441 |
\newcommand{\concat}{\mathit{concat}}
|
| 442 |
\paragraph{Some points on concatenation \anupam{if necessary}}
|
| 443 |
We can define the concatenation operation by PRN: |
| 444 |
\[ |
| 445 |
\begin{array}{rcl}
|
| 446 |
\concat (\epsilon ; y) & : = & x \\ |
| 447 |
\concat (\succ_i x ; y) & := & \succ_i \concat (x ; y) |
| 448 |
\end{array}
|
| 449 |
\] |
| 450 |
|
| 451 |
From here we can define iterated concatenation: |
| 452 |
\[ |
| 453 |
\concat (x_1 , \dots x_n ; y) \quad := \quad \concat (x_n ; \concat (x_{n-1} ; \vldots \concat (x_1 ; y) \vldots ) )
|
| 454 |
\] |
| 455 |
|
| 456 |
(notice all safe inputs are hereditarily to the right of $;$ so this is definable by safe composition and projection.) |