Révision 201 CSL17/soundness.tex
| soundness.tex (revision 201) | ||
|---|---|---|
| 12 | 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 | 13 |
For this we will use length-bounded witnessing, borrowing a similar idea from Bellantoni's previous work \cite{Bellantoni95}.
|
| 14 | 14 |
|
| 15 |
|
|
| 15 | 16 |
\begin{definition}
|
| 16 | 17 |
[Length bounded basic functions] |
| 17 | 18 |
We define \emph{length-bounded equality}, $\eq(l;x,y)$ as the characteristic function of the predicate:
|
| 18 | 19 |
\[ |
| 19 | 20 |
x \mode l = y \mode l |
| 20 | 21 |
\] |
| 22 |
which is definable by safe recursion on $l$: |
|
| 23 |
\[ |
|
| 24 |
\begin{array}{rcl}
|
|
| 25 |
\eq (0 ; x,y) & \dfn & \equivfn (;\bit (0;x),\bit(0;y) ) \\ |
|
| 26 |
\eq (\succ i l; x,y) & \dfn & \cond (; \eq ( u;x,y ) , 0, \equivfn (; \bit (\succ i u ; x ) , \bit (\succ i l ; y )) ) |
|
| 27 |
\end{array}
|
|
| 28 |
\] |
|
| 21 | 29 |
\end{definition}
|
| 22 | 30 |
|
| 23 | 31 |
\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.}
|
Formats disponibles : Unified diff