root / CSL17 / soundness.tex @ 195
Historique | Voir | Annoter | Télécharger (3,91 ko)
| 1 |
\section{Soundness}
|
|---|---|
| 2 |
\label{sect:soundness}
|
| 3 |
|
| 4 |
The main result of this section is the following: |
| 5 |
|
| 6 |
\begin{theorem}
|
| 7 |
If $\arith^i$ proves $\forall \vec u^\normal . \forall \vec x^\safe . \exists y^\safe . A(\vec u ; \vec x , y)$ then there is a $\mubci{i-1}$ program $f(\vec u ; \vec x)$ such that $\Nat \models A(\vec u ; \vec x , f(\vec u ; \vec x))$.
|
| 8 |
\end{theorem}
|
| 9 |
|
| 10 |
|
| 11 |
|
| 12 |
The main problem for soundness is that we have predicates, for example equality, that take safe arguments in our theory but do not formally satisfy the polychecking lemma for $\mubc$ functions. |
| 13 |
For this we will use length-bounded witnessing, borrowing a similar idea from Bellantoni's previous work \cite{Bellantoni95}.
|
| 14 |
|
| 15 |
\begin{definition}
|
| 16 |
[Length bounded basic functions] |
| 17 |
We define \emph{length-bounded equality}, $\eq(l;x,y)$ as the characteristic function of the predicate:
|
| 18 |
\[ |
| 19 |
x \mode l = y \mode l |
| 20 |
\] |
| 21 |
\end{definition}
|
| 22 |
|
| 23 |
\anupam{Do we need the general form of length-boundedness? E.g. the $*$ functions from Bellantoni's paper? Put above if necessary. Otherwise just add sequence manipulation functions as necessary.}
|
| 24 |
|
| 25 |
Notice that $\eq$ is a polymax bounded polyomial checking function on its normal input, and so can be added to $\mubc$ without problems. |
| 26 |
|
| 27 |
\begin{definition}
|
| 28 |
[Length bounded characteristic functions] |
| 29 |
We define $\mubci{}$ programs $\charfn{}{A} (l , \vec u; \vec x)$, parametrised by a formula $A(\vec u ; \vec x)$, as follows.
|
| 30 |
% If $A$ is a $\Pi_{i}$ formula then:
|
| 31 |
\[ |
| 32 |
\begin{array}{rcl}
|
| 33 |
\charfn{}{s\leq t} (l, \vec u ; \vec x, w) & \dfn & \leqfn(l;s,t) \\
|
| 34 |
\smallskip |
| 35 |
\charfn{}{s=t} (l, \vec u ; \vec x, w) & \dfn & \eq(l;s,t) \\
|
| 36 |
\smallskip |
| 37 |
\charfn{}{\neg A} (l, \vec u ; \vec x, w) & \dfn & \neg (;\charfn{}{A}(l , \vec u ; \vec x)) \\
|
| 38 |
\smallskip |
| 39 |
\charfn{}{A\cor B} (l, \vec u ; \vec x , w) & \dfn & \cor (; \charfn{}{A} (l, \vec u ; \vec x , w), \charfn{}{B} (\vec u ;\vec x, w) ) \\
|
| 40 |
\smallskip |
| 41 |
\charfn{}{A\cand B} (l, \vec u ; \vec x , w) & \dfn & \cand(; \charfn{}{A} (l, \vec u ; \vec x , w), \charfn{}{B} (\vec u ;\vec x, w) ) \\
|
| 42 |
\smallskip |
| 43 |
\charfn{}{\exists x^\safe . A(x)} (l, \vec u ;\vec x, w) & \dfn & \begin{cases}
|
| 44 |
1 & \exists x^\safe . \charfn{}{A(x)} (l, \vec u ;\vec x , x, w) = 1 \\
|
| 45 |
0 & \text{otherwise}
|
| 46 |
\end{cases} \\
|
| 47 |
\smallskip |
| 48 |
\charfn{}{\forall x^\safe . A(x)} (l, \vec u ;\vec x , w) & \dfn &
|
| 49 |
\begin{cases}
|
| 50 |
0 & \exists x^\sigma. \charfn{}{ A(x)} (l, \vec u; \vec x , x) = 0 \\
|
| 51 |
1 & \text{otherwise}
|
| 52 |
\end{cases}
|
| 53 |
\end{array}
|
| 54 |
\] |
| 55 |
\end{definition}
|
| 56 |
|
| 57 |
|
| 58 |
\begin{proposition}
|
| 59 |
$\charfn{}{A} (l, \vec u ; \vec x)$ is the characteristic function of $A (\vec u \mode l ; \vec x \mode l)$.
|
| 60 |
\end{proposition}
|
| 61 |
|
| 62 |
\begin{definition}
|
| 63 |
[Length bounded witness function] |
| 64 |
We now define $\Wit{\vec u ; \vec x}{A} (l , \vec u ; \vec x)$ for a $\Sigma_{i+1}$-formula $A$ with free variables amongst $\vec u; \vec x$.
|
| 65 |
\[ |
| 66 |
\begin{array}{rcl}
|
| 67 |
\Wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w) & \dfn & \charfn{}{A} (l, \vec u ; \vec x) \text{ if $A$ is $\Pi_i$} \\
|
| 68 |
\smallskip |
| 69 |
\Wit{\vec u ; \vec x}{A \cor B} (l,\vec u ; \vec x , \vec w^A , \vec w^B) & \dfn & \cor ( ; \Wit{\vec u ; \vec x}{A} (l,\vec u ; \vec x , \vec w^A) ,\Wit{\vec u ; \vec x}{B} (l,\vec u ; \vec x , \vec w^B) ) \\
|
| 70 |
\smallskip |
| 71 |
\Wit{\vec u ; \vec x}{A \cand B} (l,\vec u ; \vec x , \vec w^A , \vec w^B) & \dfn & \cand ( ; \Wit{\vec u ; \vec x}{A} (l,\vec u ; \vec x , \vec w^A) ,\Wit{\vec u ; \vec x}{B} (l,\vec u ; \vec x , \vec w^B) ) \\
|
| 72 |
\smallskip |
| 73 |
\Wit{\vec u ; \vec x}{\exists x^\safe . A(x)} (l,\vec u ; \vec x , \vec w , w) & \dfn & \Wit{\vec u ; \vec x , x}{A(x)} ( l,\vec u ; \vec x , w , \vec w )
|
| 74 |
\\ |
| 75 |
\smallskip |
| 76 |
\Wit{\vec u ; \vec x}{\forall u \leq |t(\vec u;)| . A(x)} (l , \vec u ; \vec x, w) & \dfn &
|
| 77 |
\forall u \leq |t(\vec u;)| . \Wit{u , \vec u ; \vec x}{A(u)} (l, u , \vec u ; \vec x, \beta(u;w) )
|
| 78 |
\end{array}
|
| 79 |
\] |
| 80 |
\end{definition}
|
| 81 |
|
| 82 |
\anupam{may as well use a single witness variable since need it for sharply bounded quantifiers anyway.}
|
| 83 |
|
| 84 |
\anupam{sharply bounded case obtained by sharply bounded lemma}
|