Révision 195
| CSL17/preliminaries.tex (revision 195) | ||
|---|---|---|
| 150 | 150 |
|
| 151 | 151 |
$f(\vec u; \vec x):= \begin{cases}
|
| 152 | 152 |
s_1(\mu y.h(\vec u; \vec x, y)\mod 2 = 0)& \mbox{ if there exists such a $y$,} \\
|
| 153 |
& \mbox{ otherwise,}
|
|
| 153 |
0 & \mbox{ otherwise,}
|
|
| 154 | 154 |
\end{cases}
|
| 155 | 155 |
$ |
| 156 | 156 |
|
| CSL17/ph-macros.tex (revision 195) | ||
|---|---|---|
| 45 | 45 |
\newcommand{\leqfn}{\textsc{leq}}
|
| 46 | 46 |
\newcommand{\bit}{\textsc{Bit}}
|
| 47 | 47 |
|
| 48 |
\newcommand{\zerobit}{\textsc{0bit}}
|
|
| 49 |
\newcommand{\onebit}{\textsc{1bit}}
|
|
| 50 |
\newcommand{\pref}{\textsc{pref}}
|
|
| 48 | 51 |
|
| 49 | 52 |
\newcommand{\safe}{{N_0}}
|
| 50 | 53 |
\newcommand{\normal}{{N_1}}
|
| CSL17/completeness.tex (revision 195) | ||
|---|---|---|
| 71 | 71 |
\item $\beta (i; x ,y)$. ``The $i$th element of the sequence $x$ is $y$.'' |
| 72 | 72 |
\end{itemize}
|
| 73 | 73 |
} |
| 74 |
|
|
| 74 |
\patrick{I also assume access to the following predicates:
|
|
| 75 |
\begin{itemize}
|
|
| 76 |
\item $\zerobit (u,k)$ (resp. $\onebit(u,k)$). " The $k$th bit of $u$ is 0 (resp. 1)" |
|
| 77 |
\item $\pref(k,x,y)$. "The prefix of $x$ (as a binary string) of length $k$ is $y$" |
|
| 78 |
\end{itemize}}
|
|
| 75 | 79 |
Now suppose that $f$ is defined by PRN: |
| 76 | 80 |
\[ |
| 77 | 81 |
\begin{array}{rcl}
|
| ... | ... | |
| 91 | 95 |
%Seq(z) \cand |
| 92 | 96 |
\exists y_0 . ( A_g (\vec u , \vec x , y_0) \cand \beta(0, w , y_0) ) \cand \beta(|u|, w,y ) \\ |
| 93 | 97 |
\cand & \forall k < |u| . \exists y_k , y_{k+1} . ( \beta (k, w, y_k) \cand \beta (k+1 ,w, y_{k+1}) \cand A_{h_i} (u , \vec u ; \vec x , y_k , y_{k+1}) )
|
| 98 |
\cand & \forall k < |u| . \exists y_k , y_{k+1} . ( \beta (k, w, y_k) \cand \beta (k+1 ,w, y_{k+1}) \cand B (u , \vec u ; \vec x , y_k , y_{k+1}) )
|
|
| 94 | 99 |
\end{array}
|
| 95 | 100 |
\right) |
| 96 | 101 |
\] |
| 102 |
|
|
| 103 |
where |
|
| 104 |
|
|
| 105 |
\[ |
|
| 106 |
B (u , \vec u ; \vec x , y_k , y_{k+1}) =
|
|
| 107 |
\begin{array}{ll}
|
|
| 108 |
& \\ |
|
| 109 |
\cand & |
|
| 110 |
|
|
| 111 |
\end{array}
|
|
| 112 |
|
|
| 113 |
\] |
|
| 97 | 114 |
which is $\Sigma^\safe_i$ by inspection, and indeed defines the graph of $f$. |
| 98 | 115 |
|
| 99 | 116 |
To show totality, let $\vec u \in \normal, \vec x \in \safe$ and proceed by induction on $u \in \normal$. |
Formats disponibles : Unified diff