diff options
| -rw-r--r-- | controle-20250129.tex | 61 |
1 files changed, 33 insertions, 28 deletions
diff --git a/controle-20250129.tex b/controle-20250129.tex index e5549be..c5a76cc 100644 --- a/controle-20250129.tex +++ b/controle-20250129.tex @@ -492,7 +492,7 @@ et la voici écrite dans le style « drapeau » : \smallskip -\textbf{(6)} Expliquer dans les grandes lignes comment on pourrait prouver ce lemme en Coq (notamment qu'elles seraient les principales tactiques utilisées). +\textbf{(6)} Expliquer dans les grandes lignes comment on pourrait prouver ce lemme en Coq (notamment quelles seraient les principales tactiques utilisées). \begin{corrige} \smallskip @@ -669,7 +669,12 @@ $\mathbb{N}\dasharrow\mathbb{N}$, ainsi que \] l'ensemble des codes des programmes qui définissent une fonction \emph{totale} $\mathbb{N}\to\mathbb{N}$ (i.e., terminent et renvoient -un entier quel que soit l'entier qu'on leur fournit en entrée), et +un entier quel que soit l'entier qu'on leur fournit en +entrée)\footnote{Par souci de cohérence, on pourrait aussi vouloir +définir $\mathsf{PartCode} = \mathbb{N}$ comme l'ensemble des codes +des programmes définissant une fonction partielle : nous suivons la +convention que toute erreur dans un programme (même « syntaxique ») +conduit à une valeur non-définie.}, et \[ \mathsf{TotCalc} := \{\varphi_e \; : \; e\in\mathsf{TotCode}\} = \{g\colon\mathbb{N}\to\mathbb{N} \; : \; @@ -711,24 +716,23 @@ d'un programme quelconque calculant $g$. {\footnotesize -Il est évident dans le cas (A) que la fonction $\hat F$ vérifie -forcément $(\varphi_{e_1} = \varphi_{e_2}) \; \Longrightarrow (\hat -F(e_1) = \hat F(e_2))$ ; c'est-à-dire qu'elle est « extensionnelle » : -elle doit renvoyer la même valeur sur deux programmes qui calculent la -même fonction (= ont la même « extension »). D'ailleurs (on ne -demande pas de justifier ce fait, qui est facile), se donner une -fonction $F\colon \mathsf{PartCalc} \to \mathbb{N}$ revient exactement -à se donner une fonction $\hat F\colon \mathbb{N} \to \mathbb{N}$ -ayant cette propriété d'« extensionnalité ». De même, dans le -cas (B), se donner une fonction $F\colon \mathsf{TotCalc} \to -\mathbb{N}$ revient exactement à se donner une fonction $\hat F\colon -\mathsf{TotCode} \dasharrow \mathbb{N}$ qui soit extensionnelle sur -$\mathsf{TotCode}$. La définition ci-dessus dit donc que $F$ est -calculable lorsque la $\hat F$ qui lui correspond est elle-même -calculable dans le cas (A), ou, dans le cas (B) la restriction à -$\mathsf{TotCode}$ d'une fonction calculable partielle -sur $\mathbb{N}$ dont le domaine de définition contient au -moins $\mathsf{TotCode}$. +Dans le cas (A), la définition implique que la fonction $\hat F$ +vérifie forcément $(\varphi_{e_1} = \varphi_{e_2}) \; \Longrightarrow +(\hat F(e_1) = \hat F(e_2))$ ; c'est-à-dire qu'elle est +« extensionnelle » : elle doit renvoyer la même valeur sur deux +programmes qui calculent la même fonction (= ont la même +« extension »). D'ailleurs (on ne demande pas de justifier ce fait), +se donner une fonction $F\colon \mathsf{PartCalc} \to \mathbb{N}$ +revient exactement à se donner une fonction $\hat F\colon \mathbb{N} +\to \mathbb{N}$ ayant cette propriété d'« extensionnalité ». (De +même, dans le cas (B), se donner une fonction $F\colon +\mathsf{TotCalc} \to \mathbb{N}$ revient exactement à se donner une +fonction qui soit extensionnelle sur $\mathsf{TotCode}$.) La +définition ci-dessus dit donc que $F$ est calculable lorsque la $\hat +F$ qui lui correspond est elle-même calculable dans le cas (A), ou, +dans le cas (B) la restriction à $\mathsf{TotCode}$ d'une fonction +calculable partielle sur $\mathbb{N}$ dont le domaine de définition +contient au moins $\mathsf{TotCode}$. \par} @@ -804,7 +808,7 @@ ici au même : localement constante) lorsque $\mathsf{TotCalc}$ est muni de la topologie [héritée de la topologie] produit sur $\mathbb{N}^{\mathbb{N}}$.} suivante (« théorème de Kreisel-Lacombe-Shoenfield ») : quelle que soit $g \in -\mathsf{TotCalc}$, il existe $n$ telle que pour toute fonction $g' \in +\mathsf{TotCalc}$, il existe $n$ tel que pour toute fonction $g' \in \mathsf{TotCalc}$ qui coïncide avec $g$ jusqu'au rang $n$ (i.e. : $\forall i\leq n.\,(g'(i) = g(i))$) on ait $F(g') = F(g)$. @@ -885,12 +889,13 @@ question (3) valent encore en remplaçant $\mathsf{NulAPCR}$ par $\mathcal{B}_0(g,n)$ partout. (\emph{Indication :} on peut par exemple fabriquer un élément de $\mathcal{B}_0(g,n)$ en insérant les valeurs $g(0),\ldots,g(n)$ avant un élément de $\mathsf{NulAPCR}$.) -On notera $\gamma(g,n,j)$ la conclusion de la dernière sous-question, -c'est-à-dire que les fonctions $h \in \mathcal{B}_0(g,n)$ soient -exactement celles de la forme $h = \varphi_{\gamma(g,n,j)}$ pour un -certain $j$. On expliquera \emph{brièvement} pourquoi $\gamma(g,n,j)$ -est calculable en fonction de $j$, de $n$ et du code (dans -$\mathsf{TotCode}$) d'un programme calculant $g$. +En particulier : on notera $\gamma(g,n,j)$ la conclusion de la +dernière sous-question, c'est-à-dire que les fonctions $h \in +\mathcal{B}_0(g,n)$ soient exactement celles de la forme $h = +\varphi_{\gamma(g,n,j)}$ pour un certain $j$ ; on expliquera +\emph{brièvement} pourquoi $\gamma(g,n,j)$ est calculable en fonction +de $j$, de $n$ et du code (dans $\mathsf{TotCode}$) d'un programme +calculant $g$. \begin{corrige} En (3)(b), on a vu qu'on pouvait fabriquer n'importe quel élément de @@ -978,7 +983,7 @@ tout $d$. \end{itemize} \textbf{(b)} On utilise le théorème s-m-n exactement comme en (3)(c) : -dès lors que $(d,\ell) \mapsto g_d(\ell)$ est caclulable, on en déduit +dès lors que $(d,\ell) \mapsto g_d(\ell)$ est calculable, on en déduit une fonction $d \mapsto e_d$ calculable (totale ! et même primitive récursive, à savoir $e_d = s_{1,1}(q,d)$ où $q$ est tel que $g_d(\ell) = \varphi^{(2)}_q(d,\ell)$) vérifiant $g_d = \varphi_{e_d}$. |