Révision 260
| CSL17/tech-report/arithmetic.tex (revision 260) | ||
|---|---|---|
| 198 | 198 |
|
| 199 | 199 |
\subsection{Graphs of some basic functions}\label{sect:graphsbasicfunctions}
|
| 200 | 200 |
|
| 201 |
We say that a function $f$ is \emph{represented} by a formula $A_f$ in a theory if we can prove a formula of the form $\forall \vec u^{\normal} , \forall x^{\safe}, \exists! y^{\safe}. A_f$. The variables $\vec u$ and $\vec x$ can respectively be thought of as normal and safe arguments of $f$, and $y$ is the output of $f(\vec u; \vec x)$.
|
|
| 201 |
We say that a function $f$ is \emph{represented} by a formula $A_f$ in a theory if we can prove a formula of the form $\forall \vec u^{\normal} , \forall \vec x^{\safe}, \exists! y^{\safe}. A_f$. The variables $\vec u$ and $\vec x$ can respectively be thought of as normal and safe arguments of $f$, and $y$ is the output of $f(\vec u; \vec x)$.
|
|
| 202 | 202 |
|
| 203 | 203 |
Let us give a few examples for basic functions representable in $\arith^1$, wherein proofs of totality are routine: |
| 204 | 204 |
\begin{itemize}
|
| ... | ... | |
| 207 | 207 |
%\item Predecessor $p$: $\forall^{\safe} x, \exists^{\safe} y. (x=\succ{0} y \cor x=\succ{1} y \cor (x=\epsilon \cand y= \epsilon)) .$
|
| 208 | 208 |
\item Conditional $C$: |
| 209 | 209 |
$$\begin{array}{ll}
|
| 210 |
\forall x^{\safe} , y_{\epsilon}^{\safe}, y_0^{\safe}, y_1^{\safe}, \exists y^{\safe}. & ((x=\epsilon)\cand (y=y_{\epsilon})\\
|
|
| 210 |
\forall x^{\safe} , y_0^{\safe}, y_1^{\safe}, \exists y^{\safe}. & ((x=0)\cand (y=y_0)\\
|
|
| 211 | 211 |
& \cor( \exists z^{\safe}.(x=\succ{0}z) \cand (y=y_0))\\
|
| 212 | 212 |
& \cor( \exists z^{\safe}.(x=\succ{1}z) \cand (y=y_1)))\
|
| 213 | 213 |
\end{array}
|
| CSL17/tech-report/completeness.tex (revision 260) | ||
|---|---|---|
| 53 | 53 |
\right) \\ |
| 54 | 54 |
\cor & \left( |
| 55 | 55 |
\begin{array}{ll}
|
| 56 |
z\neq 0 |
|
| 56 |
%z\neq 0 |
|
| 57 |
z=\succ{1} p z
|
|
| 57 | 58 |
& \cand\ \forall y^\safe . (A_g (\vec u , \vec x , p z , y) \cimp y=_2 0 ) \\ |
| 58 | 59 |
& \cand\ \forall x^\safe < p z . \forall y^\safe . (A_g (\vec u , \vec x , x , y) \cimp y=_2 1) |
| 59 | 60 |
\end{array}
|
| ... | ... | |
| 111 | 112 |
Suppose that $\exists x^\safe , y^\safe . (A_g (\vec u ,\vec x , x , y) \cand y=_2 0)$. |
| 112 | 113 |
We can apply minimisation due to the lemma above to find the least $x\in \safe$ such that $\exists y^\safe . (A_g (\vec u ,\vec x , x , y) \cand y=_2 0)$, and we set $z = \succ 1 x$. So $x= p z$. |
| 113 | 114 |
%\todo{verify $z\neq 0$ disjunct.}
|
| 114 |
Then $z \neq 0$ holds. Moreover we had $\exists ! y^\safe . A_g(\vec u , \vec x , x , y)$. So we deduce that |
|
| 115 |
%Then $z \neq 0$ holds. |
|
| 116 |
Then $z=\succ{1} p z$ holds.
|
|
| 117 |
Moreover we had $\exists ! y^\safe . A_g(\vec u , \vec x , x , y)$. So we deduce that |
|
| 115 | 118 |
$\forall y^\safe . (A_g (\vec u , \vec x , p z , y) \cimp y=_2 0 ) $. Finally, as $p z$ is the least element such that |
| 116 | 119 |
$\exists y^\safe . (A_g (\vec u ,\vec x , p z , y) \cand y=_2 0)$, we deduce |
| 117 | 120 |
$\ \forall x^\safe < p z . \forall y^\safe . (A_g (\vec u , \vec x , x , y) \cimp y=_2 1) $. We conclude that the second member of the disjunction |
| CSL17/tech-report/ph-biblio.bib (revision 260) | ||
|---|---|---|
| 5 | 5 |
note={\url{http://www.anupamdas.com/fph-unbounded-arithmetic.pdf}}
|
| 6 | 6 |
} |
| 7 | 7 |
|
| 8 |
@incollection{bellantoni1995fph,
|
|
| 9 |
title={Predicative recursion and the polytime hierarchy},
|
|
| 10 |
author={Bellantoni, Stephen},
|
|
| 11 |
booktitle={Feasible Mathematics II},
|
|
| 12 |
pages={15--29},
|
|
| 13 |
year={1995},
|
|
| 14 |
publisher={Springer}
|
|
| 15 |
} |
|
| 16 | 8 |
|
| 17 |
|
|
| 18 | 9 |
@inproceedings{Lasson11,
|
| 19 | 10 |
author = {Marc Lasson},
|
| 20 | 11 |
title = {Controlling Program Extraction in Light Logics},
|
| CSL17/tech-report/preliminaries.tex (revision 260) | ||
|---|---|---|
| 195 | 195 |
$\mubc =\fph$. Furthermore, for $i\geq 1$, $\mubc^{i-1} = \fphi{i}$.
|
| 196 | 196 |
\end{theorem}
|
| 197 | 197 |
|
| 198 |
In what follows we will recall some of the intermediate results and state a slightly stronger result that directly follows from \cite{bellantoni1995fph}.
|
|
| 198 |
In what follows we will recall some of the intermediate results and state a slightly stronger result that directly follows from \cite{Bellantoni95}.
|
|
| 199 | 199 |
% |
| 200 | 200 |
%\medskip |
| 201 | 201 |
%\noindent |
| ... | ... | |
| 228 | 228 |
If $\Phi$ is a class of functions, we denote by $\mubc(\Phi)$ the class obtained as $\mubc$ but adding $\Phi$ to the set of initial functions. |
| 229 | 229 |
\begin{lemma}[Polychecking Lemma, \cite{BellantoniThesis}]
|
| 230 | 230 |
\label{lem:polychecking}
|
| 231 |
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$.
|
|
| 231 |
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 polynomial checking function on $\vec u$. |
|
| 232 | 232 |
\end{lemma}
|
| 233 | 233 |
|
| 234 | 234 |
In particular, we also have the following strengthening of Thm.~\ref{thm:mubc},
|
Formats disponibles : Unified diff