Révision 225 CSL17/soundness.tex
| soundness.tex (revision 225) | ||
|---|---|---|
| 15 | 15 |
|
| 16 | 16 |
|
| 17 | 17 |
\begin{definition}
|
| 18 |
[Length bounded basic functions] |
|
| 19 |
We define \emph{length-bounded equality}, $\eq(l;x,y)$ as the characteristic function of the predicate:
|
|
| 18 |
[Length bounded (in)equality] |
|
| 19 |
%We define \emph{length-bounded equality}, $\eq(l;x,y)$ as the characteristic function of the predicate:
|
|
| 20 |
%\[ |
|
| 21 |
%x \mode l = y \mode l |
|
| 22 |
%\] |
|
| 23 |
%which is definable by safe recursion on $l$: |
|
| 24 |
%\[ |
|
| 25 |
%\begin{array}{rcl}
|
|
| 26 |
%\eq (0 ; x,y) & \dfn & \equivfn (;\bit (0;x),\bit(0;y) ) \\ |
|
| 27 |
%\eq (\succ i l; x,y) & \dfn & \cond (; \eq ( u;x,y ) , 0, \equivfn (; \bit (\succ i u ; x ) , \bit (\succ i l ; y )) ) |
|
| 28 |
%\end{array}
|
|
| 29 |
%\] |
|
| 30 |
We define \emph{length-bounded inequality} as:
|
|
| 20 | 31 |
\[ |
| 21 |
x \mode l = y \mode l |
|
| 22 |
\] |
|
| 23 |
which is definable by safe recursion on $l$: |
|
| 24 |
\[ |
|
| 25 | 32 |
\begin{array}{rcl}
|
| 26 |
\eq (0 ; x,y) & \dfn & \equivfn (;\bit (0;x),\bit(0;y) ) \\
|
|
| 27 |
\eq (\succ i l; x,y) & \dfn & \cond (; \eq ( u;x,y ) , 0, \equivfn (; \bit (\succ i u ; x ) , \bit (\succ i l ; y )) )
|
|
| 33 |
\leqfn (0 ; x ,y) & \dfn & \cond(; \bit (0;x), 1, \bit (0;y) ) \\
|
|
| 34 |
\leqfn (\succ i l ; x,y) & \dfn & \orfn ( ; \cond(;\bit (\succ i l ; x) , \bit(\succ i l ; y),0 ) , \andfn (; \equivfn (\bit (\succ i l ; x) , \bit(\succ i l ; y)) , \leqfn (l;x,y ) ) )
|
|
| 28 | 35 |
\end{array}
|
| 29 | 36 |
\] |
| 30 |
We also define length-bounded inequality as: |
|
| 31 |
\[ |
|
| 32 |
\begin{array}{rcl}
|
|
| 33 |
\leqfn (0 ; x ,y) & \dfn & \cimp (; \bit (0;x), \bit (0;y) ) \\ |
|
| 34 |
\leqfn (\succ i l ; x,y) & \dfn & \orfn ( ; <(\bit (\succ i l ; x) , \bit(\succ i l ; y) ) , \andfn (; \equivfn (\bit (\succ i l ; x) , \bit(\succ i l ; y)) , \leqfn (l;x,y ) ) ) |
|
| 35 |
\end{array}
|
|
| 36 |
\] |
|
| 37 | 37 |
\end{definition}
|
| 38 | 38 |
|
| 39 |
\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.}
|
|
| 39 |
Notice that $\leqfn (l; x,y) = 1$ just if $x \mode l \leq y \mode l$. |
|
| 40 |
We can also define $\eq( l; x,y)$ as $\andfn (;\leq(l;x,y),\leq(l;y,x))$. |
|
| 40 | 41 |
|
| 41 |
Notice that $\eq$ is a polymax bounded polyomial checking function on its normal input, and so can be added to $\mubc$ without problems. |
|
| 42 |
%\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.}
|
|
| 43 |
% |
|
| 44 |
%Notice that $\eq$ is a polymax bounded polyomial checking function on its normal input, and so can be added to $\mubc$ without problems. |
|
| 42 | 45 |
|
| 43 |
\begin{definition}
|
|
| 44 |
[Length bounded characteristic functions] |
|
| 45 |
We define $\mubci{}$ programs $\charfn{}{A} (l , \vec u; \vec x)$, parametrised by a formula $A(\vec u ; \vec x)$, as follows.
|
|
| 46 |
% If $A$ is a $\Pi_{i}$ formula then:
|
|
| 47 |
\[ |
|
| 48 |
\begin{array}{rcl}
|
|
| 49 |
\charfn{}{s\leq t} (l, \vec u ; \vec x) & \dfn & \leqfn(l;s,t) \\
|
|
| 50 |
\smallskip |
|
| 51 |
\charfn{}{s=t} (l, \vec u ; \vec x) & \dfn & \eq(l;s,t) \\
|
|
| 52 |
\smallskip |
|
| 53 |
\charfn{}{\neg A} (l, \vec u ; \vec x) & \dfn & \neg (;\charfn{}{A}(l , \vec u ; \vec x)) \\
|
|
| 54 |
\smallskip |
|
| 55 |
\charfn{}{A\cor B} (l, \vec u ; \vec x ) & \dfn & \cor (; \charfn{}{A} (l, \vec u ; \vec x , w), \charfn{}{B} (\vec u ;\vec x) ) \\
|
|
| 56 |
\smallskip |
|
| 57 |
\charfn{}{A\cand B} (l, \vec u ; \vec x ) & \dfn & \cand(; \charfn{}{A} (l, \vec u ; \vec x , w), \charfn{}{B} (\vec u ;\vec x) ) \\
|
|
| 58 |
\smallskip |
|
| 59 |
\charfn{}{\exists x^\safe . A(x)} (l, \vec u ;\vec x) & \dfn & \begin{cases}
|
|
| 60 |
1 & \exists x^\safe . \charfn{}{A(x)} (l, \vec u ;\vec x , x) = 1 \\
|
|
| 61 |
0 & \text{otherwise}
|
|
| 62 |
\end{cases} \\
|
|
| 63 |
\smallskip |
|
| 64 |
\charfn{}{\forall x^\safe . A(x)} (l, \vec u ;\vec x ) & \dfn &
|
|
| 65 |
\begin{cases}
|
|
| 66 |
0 & \exists x^\sigma. \charfn{}{ A(x)} (l, \vec u; \vec x , x) = 0 \\
|
|
| 67 |
1 & \text{otherwise}
|
|
| 68 |
\end{cases}
|
|
| 69 |
\end{array}
|
|
| 70 |
\] |
|
| 71 |
\end{definition}
|
|
| 46 |
Let us say that a sorting $(\vec u ; \vec x)$ of the variables $\vec u , \vec x$ is \emph{compatible} with a formula $A$ if each variable of $\vec x$ occurs hereditarily safe with respect to the $\bc$-types of terms (see App.~\ref{appendix:arithmetic}).
|
|
| 47 |
In the presence of a compatible sorting, we may easily define functions that \emph{evaluate} safe formulae in $\mubc$:
|
|
| 72 | 48 |
|
| 73 |
\anupam{Above and below definitions need to be with respect to a typing of variables which terms respect.}
|
|
| 74 | 49 |
|
| 75 |
|
|
| 76 | 50 |
\begin{proposition}
|
| 77 |
$\charfn{}{A} (l, \vec u ; \vec x)$ is the characteristic function of $A (\vec u \mode l ; \vec x \mode l)$.
|
|
| 51 |
Given a $\Sigma^\safe_i$ formula $A$ and compatible sorting $(\vec u; \vec x)$ of its variables, there is a $\mubci{i-1}$ program $\charfn{\vec u ;\vec x}{A} (l, \vec u ; \vec x)$ computing the characteristic function of $A (\vec u \mode l ; \vec x \mode l)$.
|
|
| 78 | 52 |
\end{proposition}
|
| 79 | 53 |
|
| 54 |
|
|
| 55 |
We will use the programs $\charfn{}{}$ in the witness functions we define below.
|
|
| 56 |
Let us write $\charfn{}{i}$ to denote the class of functions $\charfn{}{A}$ for $A \in \Pi^\safe_{i-1}$.
|
|
| 57 |
For the notion of bounding polynomial below we are a little informal with bounds, using `big-oh' notation, since it will suffice just to be `sufficiently large'. |
|
| 58 |
|
|
| 59 |
|
|
| 80 | 60 |
\begin{definition}
|
| 81 | 61 |
[Length bounded witness function] |
| 82 |
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$.
|
|
| 83 |
For a $\Sigma^\safe_i$ formula $A$ with free variables amongst $(\vec u ; \vec x)$, with $\vec x$ occurring only hereditarily safe in terms, we define the \emph{length-bounded witness function} $\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w)$ and its \emph{bounding polynomial} $b_A (l)$ as follows:
|
|
| 62 |
For a $\Sigma^\safe_{i}$ formula $A$ with a compatible sorting $(\vec u ; \vec x)$, we define the \emph{length-bounded witness function} $\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w)$ in $\bc (\charfn{}{i})$ and its \emph{bounding polynomial} $b_A (l)$ as follows:
|
|
| 84 | 63 |
\begin{itemize}
|
| 85 |
\item If $A$ is $\Pi^\safe_{i-1}$ then $\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w) \dfn \charfn{\vec u ; \vec x}{A} (l, \vec u ; \vec x )$.
|
|
| 86 |
\item If $A$ is $B \cor C$ then |
|
| 87 |
\[ |
|
| 88 |
\wit{\vec u ; \vec x}{A} (l, \vec u ;\vec x , w)
|
|
| 89 |
\quad \dfn \quad |
|
| 90 |
\orfn ( ; \wit{\vec u ; \vec x}{B} (l, \vec u ; \vec x , \beta (b_B (l) , 0 ; w ) ) , \wit{\vec u ; \vec x}{C} (l, \vec u ; \vec x , \beta (b_C (l) , 0 ; w ) ) )
|
|
| 91 |
\] |
|
| 92 |
and we may set $b_A = O(b_B + b_C)$. |
|
| 64 |
\item If $A$ is $\Pi^\safe_{i-1}$ then $\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x , w) \dfn \charfn{\vec u ; \vec x}{A} (l, \vec u ; \vec x )$ and we set $b_A (l) = 1$.
|
|
| 65 |
\item If $A$ is $B \cor C$ then we may set $b_A = O(b_B + b_C)$ and define $ \wit{\vec u ; \vec x}{A} (l, \vec u ;\vec x , w) \dfn \orfn ( ; \wit{\vec u ; \vec x}{B} (l, \vec u ; \vec x , \beta (b_B (l) , 0 ; w ) ) , \wit{\vec u ; \vec x}{C} (l, \vec u ; \vec x , \beta (b_C (l) , 0 ; w ) ) )$.
|
|
| 66 |
% \[
|
|
| 67 |
% \wit{\vec u ; \vec x}{A} (l, \vec u ;\vec x , w)
|
|
| 68 |
% \quad \dfn \quad
|
|
| 69 |
% \orfn ( ; \wit{\vec u ; \vec x}{B} (l, \vec u ; \vec x , \beta (b_B (l) , 0 ; w ) ) , \wit{\vec u ; \vec x}{C} (l, \vec u ; \vec x , \beta (b_C (l) , 0 ; w ) ) )
|
|
| 70 |
% \]
|
|
| 71 |
% and we may set $b_A = O(b_B + b_C)$.
|
|
| 93 | 72 |
\item Similarly if $A $ is $B \cand C$, but with $\andfn$ in place of $\orfn$. |
| 94 | 73 |
% \item If $A$ is $B \cand C$ then |
| 95 | 74 |
% \[ |
| ... | ... | |
| 98 | 77 |
% \andfn ( ; \wit{\vec u ; \vec x}{B} (l, \vec u ; \vec x , \beta (b_B (l) , 0 ; w ) ) , \wit{\vec u ; \vec x}{C} (l, \vec u ; \vec x , \beta (b_C (l) , 0 ; w ) ) )
|
| 99 | 78 |
% \] |
| 100 | 79 |
% and we may set $b_A = O(b_B + b_C)$. |
| 101 |
\item If $A$ is $\forall u \leq |t(\vec u;)| . B(u)$ then
|
|
| 102 |
\[
|
|
| 80 |
\item If $A$ is $\forall u \leq |t(\vec u;)| . B(u)$ we appeal to sharply bounded closure, Lemma~\ref{lem:sharply-bounded-recursion}, to define
|
|
| 81 |
\(
|
|
| 103 | 82 |
\wit{\vec u ; \vec x}{A}
|
| 104 |
\quad \dfn\quad
|
|
| 105 |
\forall u\normal \leq |t|.
|
|
| 83 |
\dfn
|
|
| 84 |
\forall u \leq |t|. |
|
| 106 | 85 |
\wit{u, \vec u ; \vec x}{B(u)} (l, u, \vec u ; \vec x , \beta( b_{B(t)} (l) , u ; w ) )
|
| 107 |
\] |
|
| 108 |
appealing to Lemma~\ref{lem:sharply-bounded-recursion}, where we may set $b_A = O(b_{B(t)}^2 )$.
|
|
| 86 |
\) |
|
| 87 |
%appealing to Lemma~\ref{lem:sharply-bounded-recursion},
|
|
| 88 |
and |
|
| 89 |
we set |
|
| 90 |
$b_A = O(b_{B(t)}^2 )$.
|
|
| 109 | 91 |
\item Similarly if $A$ is $\exists u^\normal \leq |t(\vec u;)|. A'(u)$, but with $\exists u \leq |t|$ in place of $\forall u \leq |t|$. |
| 110 | 92 |
\item If $A$ is $\exists x^\safe . B(x) $ then |
| 111 |
\[
|
|
| 93 |
\(
|
|
| 112 | 94 |
\wit{\vec u ; \vec x}{A}
|
| 113 |
\quad \dfn \quad
|
|
| 95 |
\dfn
|
|
| 114 | 96 |
\wit{\vec u ; \vec x , x}{B(x)} ( l, \vec u ; \vec x , \beta( b_{B} (l) , 0;w ) , \beta (q(l) , 1 ;w ))
|
| 115 |
\]
|
|
| 116 |
where $q$ is obtained by the polychecking and bounded minimisation lemmata for $\wit{\vec u ; \vec x , x}{B(x)}$.
|
|
| 97 |
\)
|
|
| 98 |
where $q$ is obtained by the polychecking and bounded minimisation properties, Lemmas~\ref{lem:polychecking} and \ref{lem:bounded-minimisation}, for $\wit{\vec u ; \vec x , x}{B(x)}$.
|
|
| 117 | 99 |
We may set $b_A = O(b_B + q )$. |
| 118 | 100 |
\end{itemize}
|
| 119 | 101 |
% \[ |
| ... | ... | |
| 134 | 116 |
% \anupam{need length bounding for sharply bounded quantifiers}
|
| 135 | 117 |
\end{definition}
|
| 136 | 118 |
|
| 137 |
\anupam{may as well use a single witness variable since need it for sharply bounded quantifiers anyway.}
|
|
| 138 | 119 |
|
| 139 |
\anupam{sharply bounded case obtained by sharply bounded lemma}
|
|
| 140 | 120 |
|
| 141 |
|
|
| 142 | 121 |
\begin{proposition}
|
| 122 |
\label{prop:wit-rfn}
|
|
| 143 | 123 |
If, for some $w$, $\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x,w) =1$, then $A (\vec u \mode l ; \vec x \mode l)$ is true.
|
| 144 |
\anupam{check statement, need proof-theoretic version?}
|
|
| 124 |
Conversely, if $A (\vec u \mode l ; \vec x \mode l)$ is true then there is some $w \leq b_A(l)$ such that $\wit{\vec u ; \vec x}{A} (l, \vec u ; \vec x,w) =1$.
|
|
| 145 | 125 |
\end{proposition}
|
| 146 | 126 |
|
| 147 |
By the polychecking lemma, we can assume that such a $w$ is bounded by some polynomial in $l$. |
|
| 148 | 127 |
|
| 149 |
In order to prove Thm.~\ref{thm:soundness} we need the following lemma:
|
|
| 128 |
In order to prove Thm.~\ref{thm:soundness} we need the following lemma, essentially giving an interpretation of $\arith^i$ proofs into $\mubci{i-1}$:
|
|
| 150 | 129 |
|
| 151 | 130 |
|
| 152 | 131 |
\begin{lemma}
|
| 153 | 132 |
[Proof interpretation] |
| 154 | 133 |
\label{lem:proof-interp}
|
| 155 |
From a normal form \todo{define, prove exists} $\arith^i$ proof $\pi$ of a $\Sigma^\safe_i$ sequent $\normal(\vec u), \safe(\vec x) , \Gamma \seqar \Delta$
|
|
| 156 |
there are $\mubci{i-1}$ functions $\vec f^\pi (\vec u ; \vec x , w)$ (where $\vec f^\pi = (f^\pi_B)_{B\in\Delta}$) such that, for any $l, \vec u ; \vec x , w$, we have:
|
|
| 134 |
From a typed-variable normal form $\arith^i$ proof $\pi$ of a $\Sigma^\safe_i$ sequent $\normal(\vec u), \safe(\vec x) , \Gamma \seqar \Delta$ |
|
| 135 |
there are $\bc (\charfn{}{i})$ functions $ f^\pi_B (\vec u ; \vec x , w)$ for $B\in\Delta$ such that
|
|
| 136 |
% such that, for any $l, \vec u ; \vec x , w$, we have: |
|
| 157 | 137 |
\[ |
| 158 | 138 |
% \vec a^\nu = \vec u , |
| 159 | 139 |
% \vec b^\sigma = \vec u, |
| 160 | 140 |
\bigwedge\limits_{A \in \Gamma} \wit{\vec u ; \vec x}{ A} (l, \vec u ; \vec x , w_A) =1
|
| 161 |
\quad \implies \quad
|
|
| 162 |
\bigvee\limits_{B\in \Delta} \wit{\vec u ; \vec x}{B} (l, \vec u ; \vec x , f^\pi_B(\vec u \mode l ; \vec x \mode l, \vec w)) = 1
|
|
| 141 |
\ \implies \
|
|
| 142 |
\bigvee\limits_{B\in \Delta} \wit{\vec u ; \vec x}{B} (l, \vec u ; \vec x , f^\pi_B((\vec u ; \vec x )\mode l, \vec w \mode p(l))) = 1
|
|
| 163 | 143 |
\] |
| 164 |
\anupam{Need $\vec w \mode p(l)$ for some $p$.}
|
|
| 165 |
\anupam{$l$ may occur freely in the programs $f^\pi_B$}
|
|
| 144 |
for some polynomial $p$. |
|
| 145 |
% \anupam{Need $\vec w \mode p(l)$ for some $p$.}
|
|
| 146 |
% \anupam{$l$ may occur freely in the programs $f^\pi_B$}
|
|
| 166 | 147 |
\end{lemma}
|
| 167 | 148 |
|
| 168 | 149 |
|
| 169 |
\todo{Make statement above proper, with all bounds and moduli. I cut the proof to the appendix, maybe add sketch if space.}
|
|
| 170 | 150 |
|
| 171 |
From this lemma we can readily prove the soundness result: |
|
| 151 |
|
|
| 152 |
Now we can prove the soundness result: |
|
| 172 | 153 |
|
| 173 | 154 |
\begin{proof}
|
| 174 | 155 |
[Proof of Thm.~\ref{thm:soundness} from Lemma~\ref{lem:proof-interp}]
|
| 175 |
(watch out for dependence on $l$, try do without) |
|
| 176 |
|
|
| 177 |
Suppose $\arith^i \proves \forall \vec u^\normal . \exists x^\normal . A(\vec u ; x)$. Then by raising, inversion, free-variable normal forms, we have a proof of, |
|
| 178 |
\[ |
|
| 179 |
\normal (\vec u ) \seqar \exists x^\normal . A(\vec u , x ;) |
|
| 180 |
\] |
|
| 181 |
whence, by Lemma~\ref{lem:proof-interp}, we have a $\mubci{i-1}$ function $f$ such that:
|
|
| 182 |
\[ |
|
| 183 |
\vec u \mode l = \vec a \mode l |
|
| 184 |
\quad \implies \quad |
|
| 185 |
\wit{\vec u ; }{A} ( l , \vec u , f(\vec u \mode l;) ) =1
|
|
| 186 |
\] |
|
| 187 |
|
|
| 188 |
Now it suffices to choose an $l$ bigger that both all the $\vec u$ and $f(\vec u)$, which is a polynomial in $\vec u$ by the polymax bounding lemma. |
|
| 156 |
Suppose $\arith^i \proves \forall \vec u^\normal . \exists x^\safe . A(\vec u ; x)$. By inversion and Thm.~\ref{thm:normal-form} there is a $\arith^i$ proof $\pi$ of $\normal (\vec u ) \seqar \exists x^\safe. A(\vec u ; x )$ in typed variable normal form.
|
|
| 157 |
By Lemma~\ref{lem:proof-interp}, we have a $\mubci{i-1}$ function $f^\pi$ with $\wit{\vec u ;}{\exists x^\safe . A} (l, \vec u ; f(\vec u \mode l;)) =1$.
|
|
| 158 |
By the definition of $\wit{}{}$ and Prop.~\ref{prop:wit-rfn} we have that $\exists x . A(\vec u \mode l; x)$ is true just if $A(\vec u \mode l ; \beta (q(l), 1 ; f(\vec u \mode l;) ))$ is true.
|
|
| 159 |
Now, since all $\vec u$ are normal, we may simply set $l$ to have a longer length than all of these arguments, so the function $f(\vec u;) \dfn \beta (q(\sum \vec u), 1 ; f(\vec u \mode \sum \vec u;) ))$ suffices. |
|
| 189 | 160 |
\end{proof}
|
Formats disponibles : Unified diff