Révision 219
| CSL17/soundness.tex (revision 219) | ||
|---|---|---|
| 70 | 70 |
\] |
| 71 | 71 |
\end{definition}
|
| 72 | 72 |
|
| 73 |
\anupam{Above and below definitions need to be with respect to a typing of variables which terms respect.}
|
|
| 73 | 74 |
|
| 75 |
|
|
| 74 | 76 |
\begin{proposition}
|
| 75 | 77 |
$\charfn{}{A} (l, \vec u ; \vec x)$ is the characteristic function of $A (\vec u \mode l ; \vec x \mode l)$.
|
| 76 | 78 |
\end{proposition}
|
| ... | ... | |
| 78 | 80 |
\begin{definition}
|
| 79 | 81 |
[Length bounded witness function] |
| 80 | 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$.
|
| 81 |
\[ |
|
| 82 |
\begin{array}{rcl}
|
|
| 83 |
\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$} \\
|
|
| 84 |
\smallskip |
|
| 85 |
\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) ) \\
|
|
| 86 |
\smallskip |
|
| 87 |
\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) ) \\
|
|
| 88 |
\smallskip |
|
| 89 |
\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 )
|
|
| 90 |
\\ |
|
| 91 |
\smallskip |
|
| 92 |
\Wit{\vec u ; \vec x}{\forall u \leq |t(\vec u;)| . A(x)} (l , \vec u ; \vec x, w) & \dfn &
|
|
| 93 |
\forall u \leq |t(\vec u;)| . \Wit{u , \vec u ; \vec x}{A(u)} (l, u , \vec u ; \vec x, \beta(u;w) )
|
|
| 94 |
\end{array}
|
|
| 95 |
\] |
|
| 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:
|
|
| 84 |
\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)$. |
|
| 93 |
\item Similarly if $A $ is $B \cand C$, but with $\andfn$ in place of $\orfn$. |
|
| 94 |
% \item If $A$ is $B \cand C$ then |
|
| 95 |
% \[ |
|
| 96 |
% \wit{\vec u ; \vec x}{A} (l, \vec u ;\vec x , w)
|
|
| 97 |
% \quad \dfn \quad |
|
| 98 |
% \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 |
% \] |
|
| 100 |
% 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 |
\[ |
|
| 103 |
\wit{\vec u ; \vec x}{A}
|
|
| 104 |
\quad \dfn\quad |
|
| 105 |
\forall u\normal \leq |t|. |
|
| 106 |
\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 )$.
|
|
| 109 |
\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 |
\item If $A$ is $\exists x^\safe . B(x) $ then |
|
| 111 |
\[ |
|
| 112 |
\wit{\vec u ; \vec x}{A}
|
|
| 113 |
\quad \dfn \quad |
|
| 114 |
\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)}$.
|
|
| 117 |
We may set $b_A = O(b_B + q )$. |
|
| 118 |
\end{itemize}
|
|
| 119 |
% \[ |
|
| 120 |
% \begin{array}{rcl}
|
|
| 121 |
% \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$} \\
|
|
| 122 |
% \smallskip |
|
| 123 |
% \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) ) \\
|
|
| 124 |
% \smallskip |
|
| 125 |
% \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) ) \\
|
|
| 126 |
% \smallskip |
|
| 127 |
% \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 )
|
|
| 128 |
% \\ |
|
| 129 |
% \smallskip |
|
| 130 |
% \wit{\vec u ; \vec x}{\forall u \leq |t(\vec u;)| . A(x)} (l , \vec u ; \vec x, w) & \dfn &
|
|
| 131 |
% \forall u \leq |t(\vec u;)| . \wit{u , \vec u ; \vec x}{A(u)} (l, u , \vec u ; \vec x, \beta(u;w) )
|
|
| 132 |
% \end{array}
|
|
| 133 |
% \] |
|
| 134 |
% \anupam{need length bounding for sharply bounded quantifiers}
|
|
| 96 | 135 |
\end{definition}
|
| 97 | 136 |
|
| 98 | 137 |
\anupam{may as well use a single witness variable since need it for sharply bounded quantifiers anyway.}
|
| ... | ... | |
| 105 | 144 |
\anupam{check statement, need proof-theoretic version?}
|
| 106 | 145 |
\end{proposition}
|
| 107 | 146 |
|
| 147 |
By the polychecking lemma, we can assume that such a $w$ is bounded by some polynomial in $l$. |
|
| 148 |
|
|
| 108 | 149 |
In order to prove Thm.~\ref{thm:soundness} we need the following lemma:
|
| 109 | 150 |
|
| 110 | 151 |
|
| 152 |
\paragraph*{Two properties needed}
|
|
| 153 |
For below, need witnesses and functions bounded by a polynomial in $l$. |
|
| 154 |
|
|
| 111 | 155 |
\begin{lemma}
|
| 112 |
[Proof interpretation] |
|
| 113 |
\label{lem:proof-interp}
|
|
| 114 |
For any $\arith^i$ proof of a $\Sigma^\safe_i$ sequent $\Gamma \seqar \Delta$, there is a $\mubci{i-1}$ function $f$ such that, for any $l, \vec u , \vec x , w$, we have:
|
|
| 156 |
[Proof interpretation] |
|
| 157 |
\label{lem:proof-interp}
|
|
| 158 |
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$
|
|
| 159 |
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:
|
|
| 115 | 160 |
\[ |
| 116 |
\wit{\vec u ; \vec x}{ \wedge \Gamma } (l, \vec u ; \vec x , w)
|
|
| 117 |
\quad \leq \quad |
|
| 118 |
\wit{\vec u ; \vec x}{\vee \Delta} (l, \vec u ; \vec x , f(l, \vec u ; \vec x , w))
|
|
| 161 |
% \vec a^\nu = \vec u , |
|
| 162 |
% \vec b^\sigma = \vec u, |
|
| 163 |
\bigwedge\limits_{A \in \Gamma} \wit{\vec u ; \vec x}{ A} (l, \vec u ; \vec x , w_A) =1
|
|
| 164 |
\quad \implies \quad |
|
| 165 |
\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
|
|
| 119 | 166 |
\] |
| 120 |
\anupam{maybe want $f(\vec u \mode l ; \vec x \mode l , w)$}
|
|
| 121 |
\anupam{Also, perhaps split for formulae of $\Gamma$, to avoid lots of (de)coding}
|
|
| 167 |
\anupam{Need $\vec w \mode p(l)$ for some $p$.}
|
|
| 168 |
\anupam{$l$ may occur freely in the programs $f^\pi_B$}
|
|
| 122 | 169 |
\end{lemma}
|
| 170 |
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.
|
|
| 171 |
|
|
| 123 | 172 |
\begin{proof}
|
| 124 |
We assume the proof, say $\pi$, is in integer positive free-cut free form, by the results from the previous section. |
|
| 125 |
This means that the predicate $\charfn{\vec u ; \vec x}{A}$ is defined for each formula $A(\vec u ; \vec x)$ occurring in a proof, so the theorem is well-stated.
|
|
| 173 |
Since the proof is in typed variable normal form we have that each line of the proof is of the same form, i.e.\ $\normal (\vec u), \safe (\vec x) , \Gamma \seqar \Delta$ over free variables $\vec u ; \vec x$. |
|
| 126 | 174 |
We define the function $f$ inductively, by considering the various final rules of $\pi$. |
| 127 | 175 |
|
| 176 |
|
|
| 128 | 177 |
\paragraph*{Negation}
|
| 129 | 178 |
Can assume only on atomic formulae, so no effect. |
| 179 |
|
|
| 180 |
\paragraph*{Logical rules}
|
|
| 181 |
Pairing, depairing. Need length-boundedness. |
|
| 182 |
|
|
| 183 |
If we have a left conjunction step: |
|
| 184 |
\[ |
|
| 185 |
\vlinf{\lefrul{\cand}}{}{ \normal (\vec u ), \safe (\vec x) , A\cand B , \Gamma \seqar \Delta }{ \normal (\vec u ), \safe (\vec x) , A, B , \Gamma \seqar \Delta}
|
|
| 186 |
\] |
|
| 187 |
By inductive hypothesis we have functions $\vec f (\vec u ; \vec x , w_A , w_B , \vec w)$ such that, |
|
| 188 |
\[ |
|
| 189 |
\Wit{\vec u ; \vec x}{\Gamma} (l, \vec u ; \vec x , w_A , w_B , \vec w)
|
|
| 190 |
\quad \implies \quad |
|
| 191 |
\Wit{\vec u ; \vec x}{\Delta} (l, \vec u ; \vec x , \vec f ( (\vec u ; \vec x) \mode l , (w_A , w_B , \vec w) \mode p(l) ))
|
|
| 192 |
\] |
|
| 193 |
for some polynomial $p$. |
|
| 194 |
% |
|
| 195 |
We define $\vec f^\pi (\vec u ; \vec x , w , \vec w) \dfn \vec f (\vec u ; \vec x , \beta (p(l),0; w) , \beta(p(l),1;w),\vec w )$ and, by the bounding polynomial for pairing, it suffices to set $p^\pi = O(p)$. |
|
| 196 |
|
|
| 197 |
|
|
| 198 |
Right disjunction step: |
|
| 199 |
\[ |
|
| 200 |
\vlinf{\rigrul{\cor}}{}{ \normal (\vec u ), \safe (\vec x) , \Gamma \seqar \Delta , A \cor B}{ \normal (\vec u ), \safe (\vec x) , \Gamma \seqar \Delta, A, B }
|
|
| 201 |
\] |
|
| 202 |
$\vec f^\pi_\Delta$ remains the same as that of premiss. |
|
| 203 |
Let $f_A, f_B$ be the functions corresponding to $A$ and $B$ in the premiss, so that: |
|
| 204 |
\[ |
|
| 205 |
\Wit{\vec u ; \vec x}{\Gamma} (l, \vec u ; \vec x , \vec w)
|
|
| 206 |
\quad \implies \quad |
|
| 207 |
\Wit{\vec u ; \vec x}{\Delta} (l, \vec u ; \vec x , f_C ( (\vec u ; \vec x) \mode l , \vec w \mode p(l) ))
|
|
| 208 |
\] |
|
| 209 |
for $C = A,B$ and for some $p$, such that $f_A , f_B$ are bounded by $q(l)$ (again by IH). |
|
| 210 |
We define $f^\pi_{A\cor B} (\vec u ; \vec x, \vec w) \dfn \pair{q(l)}{f_A ((\vec u ; \vec x, \vec w))}{f_B ((\vec u ; \vec x, \vec w))}$.
|
|
| 130 | 211 |
\paragraph*{Quantifiers}
|
| 131 | 212 |
\anupam{Do $\exists$-right and $\forall$-right, left rules are symmetric.}
|
| 132 | 213 |
|
| 214 |
|
|
| 215 |
|
|
| 216 |
Sharply bounded quantifiers are generalised versions of logical rules. |
|
| 217 |
\[ |
|
| 218 |
\vlinf{|\forall|}{}{\normal (\vec u) , \safe (\vec x) , \Gamma \seqar \Delta , \forall u^\normal \leq |t(\vec u;)| . A(u) }{ \normal(u) , \normal (\vec u) , \safe (\vec x) , u \leq |t(\vec u;)| , \Gamma \seqar \Delta, A(u) }
|
|
| 219 |
\] |
|
| 220 |
By the inductive hypothesis we have functions $\vec f(u , \vec u ; \vec x , w , \vec w)$ such that: |
|
| 221 |
\[ |
|
| 222 |
\Wit{u ,\vec u ; \vec x}{\lhs} ( u , \vec u ;\vec x , w , \vec w )
|
|
| 223 |
\quad \implies \quad |
|
| 224 |
\Wit{u , \vec u ; \vec x}{\rhs} (u, \vec u ; \vec x , \vec f ((\vec u ; \vec x) \mode l , \vec w \mode p(l) ) )
|
|
| 225 |
\] |
|
| 226 |
with $|f|\leq q(|l|)$. |
|
| 227 |
|
|
| 228 |
By Lemma~\ref{lem:sequence-creation}, we have a function $F (l , u , \vec u ; \vec x , w , \vec w) $ such that....
|
|
| 229 |
|
|
| 230 |
We set $f^\pi_{\forall u^\normal \leq t . A} (\vec u ; \vec x , \vec w) \dfn F(q(|l|), t(\vec u;), \vec u ; \vec x , 0, \vec w )$.
|
|
| 231 |
|
|
| 232 |
|
|
| 233 |
Right existential: |
|
| 234 |
\[ |
|
| 235 |
\vlinf{\rigrul{\exists}}{}{\normal(\vec u ) , \safe (\vec x) , \Gamma \seqar \Delta , \exists x . A(x)}{\normal(\vec u ) , \safe (\vec x) , \Gamma \seqar \Delta , A(t)}
|
|
| 236 |
\] |
|
| 237 |
Here we assume the variables of $t$ are amongst $(\vec u ; \vec x)$, since we are in typed variable normal form. |
|
| 238 |
|
|
| 239 |
|
|
| 133 | 240 |
\paragraph*{Contraction}
|
| 134 | 241 |
Left contraction simply duplicates an argument, whereas right contraction requires a conditional on a $\Sigma^\safe_i$ formula. |
| 135 | 242 |
|
| 243 |
\[ |
|
| 244 |
\vlinf{\cntr}{}{\normal (\vec u) , \safe (\vec x) , \Gamma \seqar \Delta , A }{\normal (\vec u) , \safe (\vec x) , \Gamma \seqar \Delta , A , A}
|
|
| 245 |
\] |
|
| 246 |
|
|
| 247 |
$\vec f^\pi_\Delta$ remains the same as that of premiss. Let $f_0 ,f_1$ correspond to the two copies of $A$ in the premiss. |
|
| 248 |
We define: |
|
| 249 |
\[ |
|
| 250 |
f^\pi_A ( \vec u ; \vec x , \vec w ) |
|
| 251 |
\quad \dfn \quad |
|
| 252 |
\cond (; \wit{\vec u ; \vec x}{A} ( l , \vec u ; \vec x , f_0(\vec u ; \vec x , \vec w) ) , f_1(\vec u ; \vec x , \vec w) , f_0(\vec u ; \vec x , \vec w) )
|
|
| 253 |
\] |
|
| 254 |
|
|
| 255 |
|
|
| 256 |
\anupam{For $\normal (\vec u), \safe (\vec x)$ in antecedent, we always consider as a set, so do not display explicitly contraction rules. }
|
|
| 136 | 257 |
\paragraph*{Induction}
|
| 137 | 258 |
Corresponds to safe recursion on notation. |
| 138 |
Suppose final step is: |
|
| 259 |
Suppose final step is (wlog):
|
|
| 139 | 260 |
\[ |
| 140 |
\vlinf{\pind}{}{\Gamma , \normal (t) , A(0) \seqar A(t) , \Delta}{ \left\{\Gamma , \normal (u) , A(u) \seqar A(\succ i u ) , \Delta \right\}_{i=0,1} }
|
|
| 261 |
\vlinf{\pind}{}{ \normal (\vec u), \safe (\vec x) , \Gamma, A(0) \seqar A(t(\vec u ;)) , \Delta}{ \left\{\normal (u) , \normal (\vec u) , \safe (\vec x) , \Gamma, A(u) \seqar A(\succ i u ) , \Delta \right\}_{i=0,1} }
|
|
| 141 | 262 |
\] |
| 263 |
\anupam{need to say in normal form part that can assume induction of this form}
|
|
| 142 | 264 |
For simplicity we will assume $\Delta $ is empty, which we can always do by Prop.~\todo{DO THIS!}
|
| 143 | 265 |
|
| 144 | 266 |
Now, by the inductive hypothesis, we have functions $h_i$ such that: |
| 145 | 267 |
\[ |
| 146 |
\wit{u , \vec u ; \vec x}{LHS} (l , u , \vec u ; \vec x , w) =1
|
|
| 268 |
\Wit{u , \vec u ; \vec x}{\Gamma, A(0)} (l , u , \vec u ; \vec x , \vec w)
|
|
| 147 | 269 |
\quad \implies \quad |
| 148 |
\wit{u , \vec u ; \vec x}{RHS} (l , u , \vec u ; \vec x , h_i (u \mode l , \vec u \mode l ; \vec x \mode l) ) =1
|
|
| 270 |
\Wit{u , \vec u ; \vec x}{A(\succ i u)} (l , u , \vec u ; \vec x , h_i ((u , \vec u) \mode l ; \vec x \mode l , \vec w) )
|
|
| 149 | 271 |
\] |
| 150 |
We define $ f$ as follows:
|
|
| 272 |
First let us define $ f$ as follows:
|
|
| 151 | 273 |
\[ |
| 152 | 274 |
\begin{array}{rcl}
|
| 153 |
f (0 , \vec u ; \vec x, \vec w^\Gamma , w^{\normal (t)} , w^{A(0)}) & \dfn & w^{A(0)} \\
|
|
| 154 |
f( \succ i u , \vec u ; \vec x , \vec w^\Gamma , w^{\normal (t)} , w^{A(0)}) & \dfn &
|
|
| 155 |
h_i (u , \vec u ; \vec x , \vec w^\Gamma w^{\normal (?)}, f(u , \vec u ; \vec x , \vec w ))
|
|
| 275 |
f (0 , \vec u ; \vec x, \vec w, w ) & \dfn & w\\
|
|
| 276 |
f( \succ i u , \vec u ; \vec x , \vec w, w) & \dfn &
|
|
| 277 |
h_i (u , \vec u ; \vec x , \vec w , f(u , \vec u ; \vec x , \vec w , w ))
|
|
| 156 | 278 |
\end{array}
|
| 157 | 279 |
\] |
| 158 |
\anupam{Must check above, could be problems in recursive case.}
|
|
| 280 |
where $\vec w$ corresponds to $\Gamma $ and $w$ corresponds to $A(0)$.
|
|
| 159 | 281 |
\anupam{Wait, should $\normal (t)$ have a witness? Also there is a problem like Patrick said for formulae like: $\forall x^\safe . \exists y^\safe. (\normal (z) \cor \cnot \normal (z))$, where $z$ is $y$ or otherwise.}
|
| 282 |
|
|
| 283 |
Now we let $f^\pi (\vec u ; \vec x , \vec w) \dfn f(t(\vec u ; ) , \vec u ; \vec x , \vec w)$. |
|
| 284 |
|
|
| 285 |
\paragraph*{Cut}
|
|
| 286 |
If it is a cut on an induction formula, which is safe, then it just corresponds to a safe composition since everything is substituted into a safe position. |
|
| 287 |
Otherwise it is a `raisecut': |
|
| 288 |
\[ |
|
| 289 |
\vliinf{\rais\cut}{}{\normal (\vec u ) , \normal (\vec v) , \safe (\vec x) ,\Gamma \seqar \Delta }{ \normal (\vec u) \seqar \exists x^\safe . A(x) }{ \normal (u) , \normal (\vec v) , \safe (\vec x) , A(u), \Gamma \seqar \Delta }
|
|
| 290 |
\] |
|
| 291 |
In this case we have functions $f(\vec u ; )$ and $\vec g (u, \vec v ; \vec x , w , \vec w )$, in which case we construct $\vec f^\pi$ as: |
|
| 292 |
\[ |
|
| 293 |
\vec f^\pi ( \vec u , \vec v ; \vec x , \vec w ) |
|
| 294 |
\quad \dfn \quad |
|
| 295 |
\vec g ( \beta (1 ; f(\vec u ;) ) , \vec v ; \vec x , \beta(0;f(\vec u ;)) , \vec w ) |
|
| 296 |
\] |
|
| 160 | 297 |
\end{proof}
|
| 161 | 298 |
|
| 162 | 299 |
We are now ready to prove the soundness theorem. |
| CSL17/main.tex (revision 219) | ||
|---|---|---|
| 30 | 30 |
|
| 31 | 31 |
\Copyright{Patrick Baillot and Anupam Das}%mandatory, please use full first names. LIPIcs license is "CC-BY"; http://creativecommons.org/licenses/by/3.0/
|
| 32 | 32 |
|
| 33 |
\subjclass{Dummy classification -- please refer to \url{http://www.acm.org/about/class/ccs98-html}}% mandatory: Please choose ACM 1998 classifications from http://www.acm.org/about/class/ccs98-html . E.g., cite as "F.1.1 Models of Computation".
|
|
| 33 |
\subjclass{Dummy classification %-- please refer to \url{http://www.acm.org/about/class/ccs98-html}
|
|
| 34 |
}% mandatory: Please choose ACM 1998 classifications from http://www.acm.org/about/class/ccs98-html . E.g., cite as "F.1.1 Models of Computation". |
|
| 34 | 35 |
\keywords{Dummy keyword -- please provide 1--5 keywords}% mandatory: Please provide 1-5 keywords
|
| 35 | 36 |
% Author macros::end %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 36 | 37 |
|
| ... | ... | |
| 53 | 54 |
\maketitle |
| 54 | 55 |
|
| 55 | 56 |
\begin{abstract}
|
| 56 |
We consider extensions of theories based on the Bellantoni-Cook function algebra for polynomial time functions (FP) by induction principles without bounds on quantifiers. Instead, we limit quantification to 'safe' arguments and show that the provably total functions are just those of the functional polynomial hierarchy (FPH). Our witness extraction proof relies on free-cut elimination in the logic, making use of the witness function method, due to Buss, rather than realisability and Dialectica approaches more common in implicit complexity. Our results closely resemble analogous ones from bounded arithmetic, only for an unbounded setting, and the proof generalises those for previous approaches characterising FP via ramified theories.
|
|
| 57 |
\patrick{Remove: We present further comparisons to the bounded arithmetic setting and give tiered arithmetic theories analogous to the Si2 and Vi hierarchies of bounded arithmetic.}
|
|
| 57 |
We consider extensions of theories based on the Bellantoni-Cook function algebra for polynomial time functions ($\fptime$) by induction principles without bounds on quantifiers. Instead, we limit quantification to `safe' arguments and show that the provably total functions are just those of the functional polynomial hierarchy ($\fph$). Our witness extraction proof relies on \emph{free-cut elimination} in the logic, making use of the \emph{witness function method}, due to Buss, rather than realisability and Dialectica approaches more common in implicit complexity. Our results closely resemble analogous ones from bounded arithmetic, only for an unbounded setting, and the proof generalises those for previous approaches characterising $\fptime$ via ramified theories.
|
|
| 58 |
%\patrick{Remove: We present further comparisons to the bounded arithmetic setting and give tiered arithmetic theories analogous to the Si2 and Vi hierarchies of bounded arithmetic.}
|
|
| 58 | 59 |
\end{abstract}
|
| 59 | 60 |
%\begin{abstract}
|
| 60 | 61 |
%We consider extensions of equational theories based on the Bellantoni-Cook function algebra for FPTIME by induction principles without bounds on quantifiers. Instead, we limit quantification to 'safe' variables and show that the provably total functions are just those of FPH. This closely resembles analogous results from bounded arithmetic, only for an unbounded setting, and the proof generalises those for previous approaches characterising FPTIME via the Bellantoni-Cook framework. We present further comparisons to the bounded arithmetic setting and give two-sorted arithmetic theories analogous to the Si2 and Vi hierarchies of bounded arithmetic. |
| CSL17/arithmetic.tex (revision 219) | ||
|---|---|---|
| 110 | 110 |
|
| 111 | 111 |
\begin{lemma}
|
| 112 | 112 |
[Sharply bounded lemma] |
| 113 |
\label{lem:sharply-bounded-recursion}
|
|
| 113 | 114 |
Let $f_A$ be the characteristic function of a predicate $A(u , \vec u ; \vec x)$. |
| 114 | 115 |
Then the characteristic functions of $\forall u \prefix v . A(u,\vec u ; \vec x)$ and $\exists u \prefix v . A(u , \vec u ; \vec x)$ are in $\bc(f_A)$. |
| 115 | 116 |
\end{lemma}
|
| CSL17/ph-macros.tex (revision 219) | ||
|---|---|---|
| 11 | 11 |
%\theoremstyle{definition}
|
| 12 | 12 |
%\newtheorem{definition}[theorem]{Definition}
|
| 13 | 13 |
|
| 14 |
\newcommand{\lhs}{\mathit{LHS}}
|
|
| 15 |
\newcommand{\rhs}{\mathit{RHS}}
|
|
| 16 |
|
|
| 14 | 17 |
\newcommand{\Word}{\mathbb{W}}
|
| 15 | 18 |
\newcommand{\Nat}{\mathbb{N}}
|
| 16 |
\newcommand{\arith}{B}
|
|
| 19 |
\newcommand{\arith}{B_2}
|
|
| 17 | 20 |
\newcommand{\basic}{\mathit{BASIC}}
|
| 18 | 21 |
|
| 19 | 22 |
\newcommand{\ind}{\mathit{IND}}
|
| ... | ... | |
| 28 | 31 |
\newcommand{\prefix}{\preccurlyeq}
|
| 29 | 32 |
|
| 30 | 33 |
\newcommand{\charfn}[2]{\chi^{#1}_{#2}}
|
| 31 |
\newcommand{\wit}[2]{\mathit{wit}^{#1}_{#2}}
|
|
| 34 |
\newcommand{\wit}[2]{\textsc{wit}^{#1}_{#2}}
|
|
| 32 | 35 |
\newcommand{\Wit}[2]{\mathit{Wit}^{#1}_{#2}}
|
| 33 | 36 |
\newcommand{\dfn}{:=}
|
| 34 | 37 |
\newcommand{\seqar}{\rightarrow}
|
| ... | ... | |
| 40 | 43 |
\newcommand{\hlf}[1]{\lfloor \frac{#1}{2}\rfloor}
|
| 41 | 44 |
\newcommand{\cond}{C}
|
| 42 | 45 |
\newcommand{\smsh}{\#}
|
| 43 |
\newcommand{\pair}[3]{\langle ; #1,#2 , #3 \rangle}
|
|
| 46 |
\newcommand{\pair}[3]{\langle #1;#2 , #3 \rangle}
|
|
| 44 | 47 |
\newcommand{\eq}{\textsc{eq}}
|
| 45 | 48 |
\newcommand{\leqfn}{\textsc{leq}}
|
| 46 | 49 |
\newcommand{\bit}{\textsc{bit}}
|
| ... | ... | |
| 91 | 94 |
\newcommand{\ciff}{\equiv}
|
| 92 | 95 |
|
| 93 | 96 |
\newcommand{\size}[1]{|#1|} %% length of a word
|
| 94 |
\newcommand{\mode}{\; \underline{\mbox{mod}}\;} %% mod 2^{|x|}
|
|
| 97 |
%\newcommand{\mode}{\; \underline{\mbox{mod}}\;} %% mod 2^{|x|}
|
|
| 98 |
\newcommand{\mode}{\ \underline{\mathrm{mod}}\ } %% mod 2^{|x|}
|
|
| 95 | 99 |
|
| 96 | 100 |
%%%%% RULES %%%%%% |
| 97 | 101 |
\newcommand{\lefrul}[1]{#1\text{-}\mathit{l}}
|
| CSL17/intro.tex (revision 219) | ||
|---|---|---|
| 6 | 6 |
Examples include bounded arithmetic \cite{Buss86book} \cite{Krajicek:1996:BAP:225488} \cite{Cook:2010:LFP:1734064}, applicative theories \cite{Cantini02} \cite{KahOit:13:ph-levels}, intrinsic and ramified theories \cite{Leivant94:intrinsic-theories} \cite{BelHof:02}, fragments of linear logic \cite{GirardSS92:bounded-ll} \cite{Girard94:lll} \cite{Lafont04} \cite{Baillot15} and fragments of intuitionistic logic \cite{Leivant94:found-delin-ptime}.
|
| 7 | 7 |
|
| 8 | 8 |
To some extent there is a distinction between various notions of `representability', namely between logics that \emph{type} terms computing functions of a given complexity class, and theories that prove the \emph{totality} or \emph{convergence} of programs computing functions in a given complexity class.
|
| 9 |
But a more important (and somewhat orthogonal) distinction is whether the constraints on the logic or theory are
|
|
| 10 |
\textit{explicit} or \textit{implicit}, that is to say whether they stipulate some bounds or resources, or whether the bounds are only \textit{consequence} of some logical properties. One important representant of the first category is \textit{bounded arithmetic}, which has been investigated by Buss \cite{Buss86book}, as a first-order arithmetic with bounded quantifiers. Cobham's function algebra \cite{Cobham} for polynomial time is of a similar nature, and indeed is used as a tool for the study of bounded arithmetic. In the second category one can range the systems of \textit{implicit computational complexity}, like for instance function algebras based on restrictions of recursion, such as ramified or safe recursion \cite{BellantoniCook92}, arithmetics or logics based on analogous restrictions of induction \cite{Cantini02}, \cite{Leivant94:intrinsic-theories} \cite{BelHof:02}, \cite{Leivant94:found-delin-ptime} and subsystems of linear logic \cite{Girard94:lll} \cite{Lafont04} .
|
|
| 9 |
A perhaps more important distinction is whether the constraints on the logic or theory are
|
|
| 10 |
\textit{explicit} or \textit{implicit}, that is to say whether they stipulate some bounds or resources, or whether the bounds are only \textit{consequence} of some logical properties. One important representative of the first category is \textit{bounded arithmetic}, based on theories of arithmetic where quantiiers are bounded by terms in induction or comprehension formulae \cite{Buss86book,Krajicek:1996:BAP:225488,Cook:2010:LFP:1734064}. Cobham's function algebra \cite{Cobham} for polynomial time is of a similar nature, and indeed is used as a tool for the study of bounded arithmetic. In the second category one can range the systems of \textit{implicit computational complexity}, like for instance function algebras based on restrictions of recursion, such as ramified or safe recursion \cite{BellantoniCook92}, arithmetics or logics based on analogous restrictions of induction \cite{Cantini02}, \cite{Leivant94:intrinsic-theories} \cite{BelHof:02}, \cite{Leivant94:found-delin-ptime} and subsystems of linear logic \cite{Girard94:lll} \cite{Lafont04} .
|
|
| 11 | 11 |
|
| 12 |
Bounded arithmetic is a deep and well-established theory, and one of its interests is its great versatility, as it has enabled to characterize a wide range of complexity classes, such as FP, the polynomial hierarchy FPH, PSPACE, NC \dots It is also tightly related to \textit{proof complexity}
|
|
| 13 |
\cite{Cook:2010:LFP:1734064}, the research field investigating the size of propositional proofs in various proof systems. Finally it is also employed for the research direction of \textit{bounded reverse mathematics}.
|
|
| 12 |
Bounded arithmetic is a deep and well-established field, and one of its advantages is its great versatility, allowing a characterization of a wide range of complexity classes, such as $\ptime$, the polynomial hierarchy $\ph$, $\pspace$, $\mathbf{NC}^i$ etc.
|
|
| 13 |
%It is also closely related to \textit{proof complexity}, the research field investigating the size of propositional proofs in various proof systems. Finally it is also employed for the research direction of \textit{bounded reverse mathematics}.
|
|
| 14 | 14 |
|
| 15 |
Implicit computational complexity on the other hand is a slightly more recent and less unified line of research. It has the interest of delineating some specific computing disciplines which correspond to classical complexity classes and can help shed some light for instance on the foundational nature of feasibility (see e.g. \cite{Leivant94:found-delin-ptime}). Another benefit is that implicit complexity systems can sometimes be extended into techniques for statically controlling the complexity of programs, e.g. in functional or imperative languages (\cite{Hofmann00,Hofmann03}, \cite{Marion11} \dots). However the variety of complexity classes that have been characterized in this implicit way is not as large as for bounded arithmetic. In particular implicit complexity has not managed to characterize non-deterministic classes, such as NP or PH, in a purely logical way. Actually some characterizations of such classes do exist, but they either take the form of a function algebra or of a type system extended with a non-logical feature.
|
|
| 15 |
Implicit computational complexity on the other hand is a slightly more recent and less unified line of research. It aims to relate certain computing disciplines which with complexity theoretic features, and has helped shed some light on the foundational nature of `feasibility' (see e.g.~\cite{Leivant94:found-delin-ptime}).
|
|
| 16 |
Another benefit is that implicit complexity systems can sometimes be extended into techniques for statically controlling the complexity of programs, e.g. in functional or imperative languages (\cite{Hofmann00,Hofmann03}, \cite{Marion11} etc.). However the variety of complexity classes that have been characterized in this implicit way is not as large as for bounded arithmetic. In particular implicit complexity has not managed to characterize non-deterministic classes, such as $\mathbf{NP}$ or $\ph$, in a purely logical way.\footnote{Actually some characterizations of such classes do exist, but they either take the form of a function algebra or of a type system extended with a non-logical feature.}
|
|
| 16 | 17 |
|
| 17 |
In fact implicit complexity has obtained many of its techniques from a detailed study of the comprehension scheme, of the primitive recursion scheme and of the structural rules of proof systems (contraction rule). But it seems to us that first-order quantification has not yet been investigated as much as it deserves. We believe that this is one reason of the modest achievements of implicit complexity concerning non-deterministic classes. |
|
| 18 |
Systems in implicit complexity typically imposes constraints on the comprehension scheme, the primitive recursion scheme or the structural rules of proof systems (namely \emph{contraction}).
|
|
| 19 |
% But it seems to us that first-order quantification has not yet been investigated as much as it deserves. We believe that this is one reason of the modest achievements of implicit complexity concerning non-deterministic classes. |
|
| 20 |
% |
|
| 21 |
In the present work we aim to bridge the gap to bounded arithmetic by constructing `implicit' theories that characterise the functional polynomial hierarchy $\fph$ and its levels. We consider a base theory similar to that of bounded arithmetic, but we allow induction on \emph{unbounded} formulae, i.e.\ without any explicit bounds.
|
|
| 22 |
% By implicit complexity arithmetic we mean that the quantifiers employed should not be bounded quantifiers. Our motivation is to bridge the fields of bounded arithmetic and implicit complexity, and to try pave the way for the design of systems bringing together simplicity (no explicit bounds) and versatility, in which one could transfer some of the main results of bounded arithmetic. |
|
| 23 |
% |
|
| 24 |
% Our methodology will be the following one: |
|
| 25 |
Naturally another constraint is in order, and for this we will use the concept of \textit{ramification} that is common in implicit complexity \cite{Leivant95,BellantoniCook92}.
|
|
| 26 |
%, adapt it in the setting of first-order arithmetic, and then explore some properties relative to quantification. First |
|
| 27 |
Also known as \emph{safe recursion}, ramification a discipline which aims at limiting the power of recursion by distinguishing two (or more) levels of integers: the \textit{safe} or level-0 integers (in this work $\safe$), and the \textit{normal} or level-1 ones (in this work $\normal$).
|
|
| 28 |
In a nutshell, recursion is permitted on normal arguments, but recursive calls can only appear in safe positions. Basic operations, such as conditionals and Boolean predicates, can be performed on safe arguments. |
|
| 29 |
Functions defined in this way correspond to polynomial time functions \cite{BellantoniCook92}.
|
|
| 18 | 30 |
|
| 19 |
So in the present work we aim at exploring the power of first-order quantification in an implicit complexity arithmetic, and in particular we wish to characterize the polynomial hierarchy FPH and its levels. By implicit complexity arithmetic we mean that the quantifiers employed should not be bounded quantifiers. Our motivation is to bridge the fields of bounded arithmetic and implicit complexity, and to try pave the way for the design of systems bringing together simplicity (no explicit bounds) and versatility, in which one could transfer some of the main results of bounded arithmetic. |
|
| 31 |
This discipline can be transposed into first-order arithmetic by adding predicates for normal and safe integers and by limiting the induction scheme by allowing induction only on normal integers, but crucially on formulae with only \emph{safe} unbounded quantifiers.
|
|
| 32 |
%The key step we make is to focus our attention on \textit{safe quantifiers} that is to say quantifiers on safe variables.
|
|
| 33 |
These safe quantifiers play a r\^ole analogous to bounded quantifiers in bounded arithmetic. In particular we will consider a hierarchy $\Sigma_i^{\safe}$ of formulas, according to the number of alternations of safe quantifiers, to define a hierarchy of theories $\arith^i$ allowing induction on $\Sigma^\safe_i$ formulae.
|
|
| 34 |
We show that such a theory proves the totality of precisely the $\fph_i$ functions, relying on a recursion-theoretic characterisation of $\fph$ due to Bellantoni \cite{bellantoni1995fph} to both extract programs and prove completeness of the theory with respect to $\fph_i$.
|
|
| 20 | 35 |
|
| 21 |
Our methodology will be the following one: we will use the concept of \textit{ramification} coming from implicit complexity \cite{Leivant95,BellantoniCook92}, adapt it in the setting of first-order arithmetic, and then explore some properties relative to quantification. First recall that ramification, or safe recursion, is a discipline which aims at limiting the power of recursion by distinguishing two (or more) levels of integers: the \textit{safe} or level-0 integers, and the \textit{normal} or level-1 ones. In a nutshell, recursion, which is here recursion on notation (or binary words), is permitted on normal arguments, but recursive calls can only appear in safe positions. Basic operations, such as conditional, can be performed on safe arguments. Functions defined in this way correspond to polynomial time functions \cite{BellantoniCook92}.
|
|
| 36 |
\medskip |
|
| 37 |
\noindent |
|
| 38 |
\textbf{Related work}. To the best of our knowledge, our work is the first characterization of the polynomial hierarchy and its levels in an implicit arithmetic. Our approach is however related to several previous works, and differs either by some of the definitions and/or by the complexity class characterized.
|
|
| 39 |
One particular difference is that we specify programs using arithmetic formulae, as in bounded arithmetic, rather than equational specifications or combinatory terms in other works, which seems to be important for characterizing $\fph$. |
|
| 22 | 40 |
|
| 23 |
This discipline can be transposed in first-order arithmetic by adding predicates for normal and safe integers and by limiting the induction scheme by allowing induction only on normal integers. The key step we make is to focus our attention on \textit{safe quantifiers} that is to say quantifiers on safe variables. These safe quantifiers will play a r\^ole analogous to bounded quantifiers in bounded arithmetic. In particular we will consider a hierarchy $\Sigma_i^{\safe}$ of formulas according to the number of alternances of safe quantifiers, and we will calibrate the use of induction by restricting the class to which the induction formula can belong. We will finally characterize in this way the levels of the polynomial hierarchy.
|
|
| 41 |
% A first axis of classification between the logics and arithmetics for complexity classes is the way by which they specify functions. The options at stake can be enumerated as follows: (i) \textit{formula specification}, as in first-order bounded arithmetic \cite{Buss86book}, (ii) \textit{equational specification}, as in Leivant's intrinsic theories \cite{Leivant94:intrinsic-theories}, (iii) \textit{combinatory terms} as in applicative theories (e.g. \cite{Strahm03}) or $\lambda$-calculus terms. A second axis, as explained in the introduction, is whether the system is explicit or implicit.
|
|
| 42 |
% |
|
| 43 |
% Our approach in this paper is to use the formula-specification point of view, because it is convenient for the polynomial hierarchy. |
|
| 44 |
The arithmetic of \cite{KahOit:13:ph-levels} characterizes $\fph$, but it is not implicit, relying on axioms defining bounded schemes.
|
|
| 45 |
% Some other works are closer to our methodology in the sense that they are implicit arithmetics and rely on a notion of ramification, but they characterize other complexity classes. |
|
| 46 |
Leivant's intrinsic theories \cite{Leivant94:intrinsic-theories} induces characterizations of $\fptime$ and elementary functions, using equational specifications, and \cite{Cantini02} obtains an analogous result for $\fptime$ using combinatory terms.
|
|
| 47 |
The paper \cite{BelHof:02} also provides a characterization of $\fptime$, with two differences: on the one hand induction is on arbitrarily quantified formulas, and on the other hand the underlying logic is not classical logic but a variant of linear logic, with a modality for normal arguments. Our paper \cite{BaillotDas16} proves a similar result, but with a different method.
|
|
| 48 |
The lack of contraction is crucial here to stop the theory from exhausting higher complexity classes. |
|
| 49 |
Finally the paper \cite{OstrinWainer05} also presents an implicit ramified arithmetic, with quantification on safe variables. Here equational specifications are used instead of formulas and unary integers instead of binary integers, which leads to a characterization of the elementary functions.
|
|
| 24 | 50 |
|
| 25 |
\textbf{Related work}. To the best of our knowledge, our work is the first characterization of the polynomial hierarchy and its levels in an implicit arithmetic. Our approach is however related to several previous works, and differs either by some of the definitions and/or by the complexity class characterized.
|
|
| 51 |
\medskip |
|
| 52 |
\noindent |
|
| 53 |
\textbf{Outline.} The rest of this paper proceeds as follows. We first give some background on function algebras for $\fptime$ and $\fph$ respectively in Sect.~\ref{sect:prelims}.
|
|
| 54 |
%Then we describe an encoding of sequences which will be instrumental in the proof of our result. |
|
| 55 |
We present our arithmetic theories $\arith^i$ in Sect.~\ref{sect:arithmetic} and prove our soundness result, that the provably total functions of $\arith^i$ are in $\fph_i$, in Sect.~\ref{sect:soundness}. Finally, we prove the completeness result, that all $\fph_i$ functions have a representation provably total in $\arith^i$, in Sect.~\ref{sect:completeness}, and present conclusions in Sect.~\ref{sect:conclusion}.
|
|
| 26 | 56 |
|
| 27 |
A first axis of classification between the logics and arithmetics for complexity classes is the way by which they specify functions. The options at stake can be enumerated as follows: (i) \textit{formula specification}, as in first-order bounded arithmetic \cite{Buss86book}, (ii) \textit{equational specification}, as in Leivant's intrinsic theories \cite{Leivant94:intrinsic-theories}, (iii) \textit{combinatory terms} as in applicative theories (e.g. \cite{Strahm03}) or $\lambda$-calculus terms. A second axis, as explained in the introduction, is whether the system is explicit or implicit.
|
|
| 28 |
|
|
| 29 |
Our approach in this paper is to use the formula-specification point of view, because it is convenient for the polynomial hierarchy. The arithmetic of \cite{KahOit:13:ph-levels} characterizes PH, but it fits in the explicit approach as it uses axioms defining bounded schemes.
|
|
| 30 |
Some other works are closer to our methodology in the sense that they are implicit arithmetics and rely on a notion of ramification, but they characterize other complexity classes. Leivant's intrinsic theories \cite{Leivant94:intrinsic-theories} allows to characterize FP, in the equational specification approach, and \cite{Cantini02} obtains an analogous result in the combinatory terms approach. The paper \cite{BelHof:02} also provides a characterization of FP, with two differences: on the one hand induction is on arbitrarily quantified formulas, and on the other hand the underlying logic is not classical logic but a variant of linear logic, with a modality for normal arguments. Our paper \cite{BaillotDas16} proves a similar result, but with a different method. Finally the paper \cite{OstrinWainer05} also presents an implicit ramified arithmetic, with quantification on safe variables. The difference with our setting is that equational specifications are used instead of formulas, unary integers instead of binary integers, and the class of functions characterized is that of elementary functions.
|
|
| 31 | 57 |
|
| 32 |
|
|
| 33 |
\textbf{Outline.} The rest of the paper will proceed as follows. We first give some background on function algebras for FP and FPH respectively. Then we describe an encoding of sequences which will be instrumental in the proof of our result. We present our arithmetical system in Sect. \ref{sect:arithmetic}, prove our soundness result, that is to say the provably total functions are in FPH, in Sect. \ref{sect:soundness}, and our completeness result, all FPH functions are provably total in the arithmetic, in Sect. \ref{sect:completeness}.
|
|
| 34 |
|
|
| 35 |
|
|
| 36 | 58 |
% \patrick{
|
| 37 | 59 |
% \begin{itemize}
|
| 38 | 60 |
% \item our goal: design an unbounded arithmetic for FPH. |
| CSL17/conclusions.tex (revision 219) | ||
|---|---|---|
| 1 | 1 |
\section{Conclusions}
|
| 2 |
\label{sect:conclusion}
|
|
| 2 | 3 |
|
| 3 | 4 |
We have presented a ramified arithmetic parameterized by the formulas on which induction is allowed. The hierarchy of induction formulas |
| 4 | 5 |
$\Sigma_i^{\safe}$ is defined by the number of alternances of safe (unbounded) quantifiers. We have proved that the system $\arith^i$ with
|
| CSL17/ph-biblio.bib (revision 219) | ||
|---|---|---|
| 1 |
@incollection{bellantoni1995fph,
|
|
| 2 |
title={Predicative recursion and the polytime hierarchy},
|
|
| 3 |
author={Bellantoni, Stephen},
|
|
| 4 |
booktitle={Feasible Mathematics II},
|
|
| 5 |
pages={15--29},
|
|
| 6 |
year={1995},
|
|
| 7 |
publisher={Springer}
|
|
| 8 |
} |
|
| 1 | 9 |
|
| 2 | 10 |
|
| 3 |
@inproceedings{Lasson11,
- author = {Marc Lasson},
- title = {Controlling Program Extraction in Light Logics},
- booktitle = {Proceedings of Typed Lambda Calculi and Applications - 10th International Conference,
- {TLCA} 2011},
- pages = {123--137},
- series = {LNCS},
- volume = {6690},
- publisher = {Springer},
- year = {2011}
- }
-
|
|
| 4 |
@inproceedings{Leivant95,
- author = {Daniel Leivant},
+@inproceedings{Lasson11,
|
|
| 11 |
author = {Marc Lasson},
|
|
| 12 |
title = {Controlling Program Extraction in Light Logics},
|
|
| 13 |
booktitle = {Proceedings of Typed Lambda Calculi and Applications - 10th International Conference,
|
|
| 14 |
{TLCA} 2011},
|
|
| 15 |
pages = {123--137},
|
|
| 16 |
series = {LNCS},
|
|
| 17 |
volume = {6690},
|
|
| 18 |
publisher = {Springer},
|
|
| 19 |
year = {2011}
|
|
| 20 |
} |
|
| 21 |
|
|
| 22 |
@inproceedings{Leivant95,
|
|
| 23 |
author = {Daniel Leivant},
|
|
| 5 | 24 |
title = {Ramified recurrence and computational complexity I: Word recurrence and poly-time},
|
| 6 | 25 |
booktitle = {Feasible mathematics II},
|
| 7 |
pages = {320--343},
- publisher = {Birkhauser Boston},
- year = {1995},
+ pages = {320--343},
|
|
| 26 |
publisher = {Birkhauser Boston},
|
|
| 27 |
year = {1995},
|
|
| 8 | 28 |
} |
| 9 | 29 |
|
| 10 |
@inproceedings{Marion11,
- author = {Jean{-}Yves Marion},
- title = {A Type System for Complexity Flow Analysis},
- booktitle = {Proceedings of the 26th Annual {IEEE} Symposium on Logic in Computer
- Science, {LICS} 2011},
- pages = {123--132},
- publisher = {{IEEE} Computer Society},
- year = {2011},
- }
|
|
| 30 |
@inproceedings{Marion11,
|
|
| 31 |
author = {Jean{-}Yves Marion},
|
|
| 32 |
title = {A Type System for Complexity Flow Analysis},
|
|
| 33 |
booktitle = {Proceedings of the 26th Annual {IEEE} Symposium on Logic in Computer
|
|
| 34 |
Science, {LICS} 2011},
|
|
| 35 |
pages = {123--132},
|
|
| 36 |
publisher = {{IEEE} Computer Society},
|
|
| 37 |
year = {2011},
|
|
| 38 |
} |
|
| 11 | 39 |
|
| 12 |
@article{Hofmann03,
- author = {Martin Hofmann},
- title = {Linear types and non-size-increasing polynomial time computation},
- journal = {Inf. Comput.},
- volume = {183},
- number = {1},
- pages = {57--85},
- year = {2003}
- }
|
|
| 40 |
@article{Hofmann03,
|
|
| 41 |
author = {Martin Hofmann},
|
|
| 42 |
title = {Linear types and non-size-increasing polynomial time computation},
|
|
| 43 |
journal = {Inf. Comput.},
|
|
| 44 |
volume = {183},
|
|
| 45 |
number = {1},
|
|
| 46 |
pages = {57--85},
|
|
| 47 |
year = {2003}
|
|
| 48 |
} |
|
| 13 | 49 |
|
| 14 |
@article{OstrinWainer05,
- author = {Geoffrey E. Ostrin and
- Stanley S. Wainer},
- title = {Elementary arithmetic},
- journal = {Ann. Pure Appl. Logic},
- volume = {133},
- number = {1-3},
- pages = {275--292},
- year = {2005}
- }
-
|
|
| 50 |
@article{OstrinWainer05,
|
|
| 51 |
author = {Geoffrey E. Ostrin and
|
|
| 52 |
Stanley S. Wainer}, |
|
| 53 |
title = {Elementary arithmetic},
|
|
| 54 |
journal = {Ann. Pure Appl. Logic},
|
|
| 55 |
volume = {133},
|
|
| 56 |
number = {1-3},
|
|
| 57 |
pages = {275--292},
|
|
| 58 |
year = {2005}
|
|
| 59 |
} |
|
| 15 | 60 |
|
| 61 |
|
|
| 16 | 62 |
@article{GaboardiMarionRonchi12,
|
| 17 | 63 |
author = {Marco Gaboardi and
|
| 18 | 64 |
Jean{-}Yves Marion and
|
| CSL17/preliminaries.tex (revision 219) | ||
|---|---|---|
| 1 | 1 |
|
| 2 | 2 |
\section{Preliminaries}
|
| 3 |
\label{sect:prelims}
|
|
| 3 | 4 |
We introduce the polynomial hierarchy and its basic properties, then the Bellantoni characterisation. |
| 4 | 5 |
|
| 5 | 6 |
\anupam{Should recall polymax bounded functions and the polychecking lemma, e.g.\ from Bellantoni's FPH paper or thesis. Quite important, even if proof not given.}
|
| ... | ... | |
| 208 | 209 |
\end{definition}
|
| 209 | 210 |
One then has: |
| 210 | 211 |
\begin{lemma}[Bounded Minimization, \cite{BellantoniThesis}]
|
| 212 |
\label{lem:bounded-minimisation}
|
|
| 211 | 213 |
If $f(\vec u; \vec x,y)$ is a polynomial checking function on $\vec u$ and $q$ is a threshold, then for any $\vec u$ and $\vec x$ we have: |
| 212 | 214 |
$$ (\exists y. f(\vec u; \vec x,y)\mbox{ mod } 2=0) \Rightarrow (\exists y. (\size{y}\leq q(\size{\vec{x}})+2) \mbox{ and } f(\vec u; \vec x,y) \mbox{ mod } 2=0) .$$
|
| 213 | 215 |
\end{lemma}
|
| 214 | 216 |
Finally we can state an important lemma about $\mubc$: |
| 215 | 217 |
\begin{lemma}[Polychecking Lemma, \cite{BellantoniThesis}]
|
| 218 |
\label{lem:polychecking}
|
|
| 216 | 219 |
Let $\Phi$ be a class of polymax bounded polynomial checking functions. If $f(\vec u; \vec x)$ is in $\mubc(\Phi)$, then $f$ is a polymax bounded function polynomial checking function on $\vec u$. |
| 217 | 220 |
\end{lemma}
|
| 218 | 221 |
The following property follows from \cite{BellantoniThesis, Bellantoni95}]
|
| CSL17/sequence-coding.tex (revision 219) | ||
|---|---|---|
| 63 | 63 |
\end{lemma}
|
| 64 | 64 |
\begin{proof}
|
| 65 | 65 |
Length induction on $l$. |
| 66 |
\end{proof}
|
|
| 66 |
\end{proof}
|
|
| 67 |
|
|
| 68 |
|
|
| 69 |
\subsection{Summary}
|
|
| 70 |
Assume the existence of a simple pairing function for elements of fixed size: $\pair{k,l}{x}{y}$ denotes the pair $(x \mode k , y \mode l )$.
|
|
| 71 |
An appropriate such function would `interleave' $x$ and $y$, adding delimiters as necessary. |
|
| 72 |
We assume that $|\pair{k,l}{x}{y}| = k+O(l)$ and $\pair{k,l}{x}{y}$ satisfies the polychecking lemma.
|
|
| 73 |
|
|
| 74 |
We will simply write $\pair{l}{x}{y}$ for $\pair{l,l}{x}{y}$.
|
|
| 75 |
|
|
| 76 |
\begin{lemma}
|
|
| 77 |
[Creating sequences] |
|
| 78 |
\label{lem:sequence-creation}
|
|
| 79 |
Given a function $f(u , \vec u ; \vec x)$ there is a $\bc(f)$ function $F(l, u , \vec u ; \vec x)$ such that: |
|
| 80 |
\[ |
|
| 81 |
F(l,u,\vec u ; \vec x) |
|
| 82 |
\quad = \quad |
|
| 83 |
\langle f(0, \vec u ; \vec x) \mode l , f(1, \vec u ; \vec x) \mode l , \dots , f(|u|, \vec u ; \vec x) \mode l \rangle |
|
| 84 |
\] |
|
| 85 |
\end{lemma}
|
|
| 86 |
\begin{proof}
|
|
| 87 |
We simply define $F$ by safe recursion from $f$: |
|
| 88 |
\[ |
|
| 89 |
\begin{array}{rcl}
|
|
| 90 |
F(l,0, \vec u ; \vec x) & \dfn & \langle ; f(0) \mode l \rangle \\ |
|
| 91 |
F(l, \succ i u , \vec u ; \vec x ) & \dfn & \pair{O(|u| l) , l}{F(l, u , \vec u ; \vec x)}{f( |\succ i u| , \vec u ; \vec x )}
|
|
| 92 |
\end{array}
|
|
| 93 |
\] |
|
| 94 |
where the constants for $O(|u|l)$ are sufficiently large. |
|
| 95 |
\end{proof}
|
|
| 96 |
|
|
| 97 |
\begin{lemma}
|
|
| 98 |
[Decoding sequences] |
|
| 99 |
We can define $\beta(l,i;x)$ as $(i\text{th element of x}) \mode l$.
|
|
| 100 |
\end{lemma}
|
|
| 101 |
\begin{proof}
|
|
| 102 |
First define $\beta (j,i;x)$ as $j$th bit of $i$th element of $x$, then use similar idea to above, by a recursion on $j$. |
|
| 103 |
\end{proof}
|
|
| 104 |
|
|
| 105 |
Notice that $\beta (l,i;x)$ satisfies the polychecking lemma. |
|
| 106 |
|
|
| 107 |
We define |
|
Formats disponibles : Unified diff