Révision 225 CSL17/appendix-soundness.tex
| appendix-soundness.tex (revision 225) | ||
|---|---|---|
| 1 | 1 |
\section{Proof of soundness}
|
| 2 |
|
|
| 3 |
\begin{definition}
|
|
| 4 |
[Length bounded characteristic functions] |
|
| 5 |
We define $\mubci{}$ programs $\charfn{}{A} (l , \vec u; \vec x)$, parametrised by a formula $A$ and a compatible typing $(\vec u ; \vec x)$ of its varables, as follows.
|
|
| 6 |
% If $A$ is a $\Pi_{i}$ formula then:
|
|
| 7 |
\[ |
|
| 8 |
\begin{array}{rcl}
|
|
| 9 |
\charfn{\vec u ; \vec x}{s\leq t} (l, \vec u ; \vec x) & \dfn & \leqfn(l;s,t) \\
|
|
| 10 |
\smallskip |
|
| 11 |
% \charfn{}{s=t} (l, \vec u ; \vec x) & \dfn & \eq(l;s,t) \\
|
|
| 12 |
% \smallskip |
|
| 13 |
\charfn{\vec u ; \vec x}{\neg A} (l, \vec u ; \vec x) & \dfn & \notfn (;\charfn{\vec u ; \vec x}{A}(l , \vec u ; \vec x)) \\
|
|
| 14 |
\smallskip |
|
| 15 |
\charfn{\vec u ; \vec x}{A\cor B} (l, \vec u ; \vec x ) & \dfn & \orfn(; \charfn{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w), \charfn{\vec u ; \vec x}{B} (\vec u ;\vec x) ) \\
|
|
| 16 |
\smallskip |
|
| 17 |
\charfn{\vec u ; \vec x}{A\cand B} (l, \vec u ; \vec x ) & \dfn & \andfn(; \charfn{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w), \charfn{\vec u ; \vec x}{B} (\vec u ;\vec x) )
|
|
| 18 |
% \end{array}
|
|
| 19 |
% \quad |
|
| 20 |
% \begin{array}{rcl}
|
|
| 21 |
\\ \smallskip |
|
| 22 |
\charfn{\vec u ; \vec x}{\exists x^\safe . A(x)} (l, \vec u ;\vec x) & \dfn & \begin{cases}
|
|
| 23 |
1 & \exists x^\safe . \charfn{}{A(x)} (l, \vec u ;\vec x , x) = 1 \\
|
|
| 24 |
0 & \text{otherwise}
|
|
| 25 |
\end{cases} \\
|
|
| 26 |
\smallskip |
|
| 27 |
\charfn{\vec u ; \vec x}{\forall x^\safe . A(x)} (l, \vec u ;\vec x ) & \dfn &
|
|
| 28 |
\begin{cases}
|
|
| 29 |
0 & \exists x^\sigma. \charfn{\vec u ; \vec x}{ A(x)} (l, \vec u; \vec x , x) = 0 \\
|
|
| 30 |
1 & \text{otherwise}
|
|
| 31 |
\end{cases}
|
|
| 32 |
\end{array}
|
|
| 33 |
\] |
|
| 34 |
\end{definition}
|
|
| 35 |
|
|
| 2 | 36 |
For the implication above, let us simply refer to the LHS as $\Wit{\vec u ; \vec x}{\Gamma} (l , \vec u ; \vec x , \vec w)$ and the RHS as $\Wit{\vec u ; \vec x}{ \Delta} (l, \vec u ; \vec x , \vec w')$, with $\vec w'$ in place of $\vec f( \cdots )$, which is a slight abuse of notation: we assume that LHS and RHS are clear from context.
|
| 3 | 37 |
|
| 4 | 38 |
\begin{proof}
|
Formats disponibles : Unified diff