Révision 245
| CSL17/preliminaries.tex (revision 245) | ||
|---|---|---|
| 184 | 184 |
where $\mu y.(h(\vec u; \vec x , y)\mod 2 = 0)$ is the least $y$ such that the equality holds. |
| 185 | 185 |
%We will denote this function $f$ as $\mu y^{+1} . h(\vec u ; \vec x , y) =_2 0$.
|
| 186 | 186 |
|
| 187 |
For each $i\geq 0$, $\mubc^i$ is the set of $\mubc$ functions obtained by at most $i$ applications of predicative minimisation.\footnote{This is the number of nestings of $\mu$ in a $\mubc$ program.} So $\mubc^0=BC$ and $\mubc =\cup_i \mubc^i$.
|
|
| 187 |
For each $i\geq 0$, $\mubc^i$ is the set of $\mubc$ functions obtained by at most $i$ applications of predicative minimisation.\footnote{This is the number of nestings of $\mu$ in a $\mubc$ program, written as a derivation tree or dag.} So $\mubc^0=\bc$ and $\mubc =\cup_i \mubc^i$.
|
|
| 188 | 188 |
|
| 189 | 189 |
\end{definition}
|
| 190 | 190 |
|
| ... | ... | |
| 229 | 229 |
\label{lem:polychecking}
|
| 230 | 230 |
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 | 231 |
\end{lemma}
|
| 232 |
The following property follows from \cite{BellantoniThesis, Bellantoni95}:
|
|
| 233 |
\begin{proposition}
|
|
| 234 |
If $\Phi$ is a class of polymax bounded polynomial checking functions, then $\mubc(\Phi)$ satisfies the properties of Thm \ref{thm:mubc}.
|
|
| 235 |
\end{proposition}
|
|
| 232 |
|
|
| 233 |
In particular, we also have the following strengthening of Thm.~\ref{thm:mubc},
|
|
| 234 |
following from \cite{BellantoniThesis, Bellantoni95}.
|
|
| 236 | 235 |
|
| 236 |
|
|
| 237 |
\begin{theorem}
|
|
| 238 |
\label{thm:mubc-phi}
|
|
| 239 |
If $\Phi$ is a class of polymax bounded polynomial checking functions, then $\mubci {i-1} (\Phi) = \fphi i$.
|
|
| 240 |
\end{theorem}
|
|
| 241 |
% |
|
| 237 | 242 |
\subsection{Some properties and extensions of $\bc$ and $\mubc$}\label{sect:somepropertiesofmubc}
|
| 238 | 243 |
|
| 239 | 244 |
We will state some results here that we rely on in the later sections. |
| 240 | 245 |
|
| 241 | 246 |
Consider the addition function $+$ with two safe arguments, so denoted as $+(;x,y)$. It is clear that if $+(;x,y)=z$, then we have $|z| \leq \max(|x|,|y|)+1$, so $+$ is a polymax bounded function. Moreover for any $n$, the $n$th least significant bits of $z$ only depend on the $n$th least significant bits of $x$ and $y$, so $+(;x,y)$ is a polynomial checking function (on no normal argument), with threshold $q(x,y)=0$. |
| 242 | 247 |
|
| 243 |
Thus, we will freely add $+(;x,y)$ to the $\mubc $ framework and define unary successor $\succ{} (;x) \dfn +(;x, \succ 1 0)$.
|
|
| 248 |
Thus, we will freely add $+(;x,y)$ to the $\mubc $ framework, under Thm.~\ref{thm:mubc-phi}, and define unary successor $\succ{} (;x) \dfn +(;x, \succ 1 0)$.
|
|
| 244 | 249 |
% In the following we will consider $\mubc(\Phi)$ with $\Phi$ containing the function $+(;x,y)$, but write it simply as $\mubc$. Note that addition could be defined in $\bc$ (hence in $\mubc$), but not with two safe arguments because the definition would use safe recursion. We will also use the unary successor $\succ{} (;x)$, which is defined thanks to addition as as $\succ{} (;x)=+(;x,\succ 1 0)$.
|
| 245 | 250 |
% |
| 246 | 251 |
In the same way, although for more simple reasons, we may add the functions $\#$ and $|\cdot|$ that we introduce later in Sect.~\ref{sect:arithmetic} to $\mubc$ containing only normal arguments since they are polynomial-time computable.
|
Formats disponibles : Unified diff