Various improvements, clarifications and rephrasings suggested by TZ.

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}$.