Second pass of proofreading.

1 files changed, 133 insertions, 124 deletions

diff --git a/controle-20240126.tex b/controle-20240126.tex
index 5f8fae2..aad3551 100644
--- a/controle-20240126.tex
+++ b/controle-20240126.tex
@@ -92,7 +92,7 @@ sera pas nécessaire de tout traiter pour avoir le maximum des points.
 
 \medbreak
 
-L'usage de tous les documents (notes de cours manuscrites ou
+L'usage de tous les documents écrits (notes de cours manuscrites ou
 imprimées, feuilles d'exercices, livres) est autorisé.
 
 L'usage des appareils électroniques est interdit.
@@ -202,11 +202,11 @@ $\lambda$-calcul simplement typé enrichi de types produits, qu'on a
 \]
 (Ici, $A,B,C$ sont des variables propositionnelles.)
 
-\textbf{(2)} En logique du premier ordre, quelle est la conclusion de
-la démonstration représentée par le $\lambda$-terme de preuve
-suivant ?
+\textbf{(2)} En logique du premier ordre intuitionniste, quelle est la
+conclusion de la démonstration représentée par le $\lambda$-terme de
+preuve suivant ?
 \[
-\lambda(p: C\land\forall x. B(x))).\,
+\lambda(p: C\land\forall x. B(x)).\,
 \lambda(x:I).\,
 \langle (\pi_1 p),\,(\pi_2 p)x\rangle
 \]
@@ -214,9 +214,9 @@ suivant ?
 variable propositionnelle, $B$ est une variable de relation unaire, et
 $I$ est le symbole du type des individus.)
 
-\textbf{(3)} En logique du premier ordre, quelle est la conclusion de
-la démonstration représentée par le $\lambda$-terme de preuve
-suivant ?
+\textbf{(3)} En logique du premier ordre intuitionniste, quelle est la
+conclusion de la démonstration représentée par le $\lambda$-terme de
+preuve suivant ?
 \[
 \lambda(p: \exists x.(A\Rightarrow B(x))).\,
 \lambda(h:A).\,
@@ -237,7 +237,7 @@ l'expression dans son ensemble a type $C\land(A\Rightarrow B)
 preuve de cette affirmation.
 
 \textbf{(2)} On se place dans le contexte où $p$ a type $C\land
-\forall x. B(x)$ et $x$ est un individu.  Alors $\pi_1 p$ a type $C$
+\forall z. B(z)$ et $x$ est un individu.  Alors $\pi_1 p$ a type $C$
 et $\pi_2 p$ a type $\forall z. B(z)$, si bien que $(\pi_2 p)x$ a type
 $B(x)$, et $\langle (\pi_1 p),\,(\pi_2 p)x\rangle$ a type $C\land
 B(x)$, donc l'expression dans son ensemble a type $(C\land \forall
@@ -285,17 +285,20 @@ $fz(\lambda g.gz) : \eta_6$ avec $\eta_3 =
 \eta_3 &= ((\eta_4\to\eta_5)\to\eta_6)\\
 \end{aligned}
 \]
-On examine d'abord la contrainte $\eta_1 = (\eta_2\to\eta_3)$ : il n'y
-a rien à faire à part enregistrer $\eta_1 \mapsto (\eta_2\to\eta_3)$
-dans la substitution.  On examine ensuite la contrainte $\eta_4 =
-(\eta_2\to\eta_5)$ : on enregistre $\eta_4 \mapsto (\eta_2\to\eta_5)$
-dans la substitution, et on l'applique à la dernière contrainte, qui
-devient $\eta_3 = (((\eta_2\to\eta_5)\to\eta_5)\to\eta_6)$.  Enfin, on
-examine la contrainte $\eta_3 =
-(((\eta_2\to\eta_5)\to\eta_5)\to\eta_6)$ : on enregistrer $\eta_3
-\mapsto (((\eta_2\to\eta_5)\to\eta_5)\to\eta_6)$ dans la substitution
-et on l'applique à $\eta_1 \mapsto (\eta_2\to\eta_3)$.  Finalement, on
-a trouvé la substitution :
+On examine d'abord la contrainte $\eta_1 = (\eta_2\to\eta_3)$ :
+$\eta_1$ est une variable de type, et elle n'apparaît pas dans l'autre
+membre de la contrainte ; il n'y a rien à faire à part enregistrer
+$\eta_1 \mapsto (\eta_2\to\eta_3)$ dans la substitution.  On examine
+ensuite la contrainte $\eta_4 = (\eta_2\to\eta_5)$ : on enregistre
+$\eta_4 \mapsto (\eta_2\to\eta_5)$ dans la substitution, et on
+l'applique à la dernière contrainte, qui devient $\eta_3 =
+(((\eta_2\to\eta_5)\to\eta_5)\to\eta_6)$.  Enfin, on examine la
+contrainte $\eta_3 = (((\eta_2\to\eta_5)\to\eta_5)\to\eta_6)$ : on
+enregistre $\eta_3 \mapsto (((\eta_2\to\eta_5)\to\eta_5)\to\eta_6)$
+dans la substitution et on l'applique à $\eta_1 \mapsto
+(\eta_2\to\eta_3)$, qui devient $\eta_1 \mapsto
+(\eta_2\to((\eta_2\to\eta_5)\to\eta_5)\to\eta_6)$.  Finalement, on a
+trouvé la substitution :
 \[
 \begin{aligned}
 \eta_1 &\mapsto (\eta_2\to((\eta_2\to\eta_5)\to\eta_5)\to\eta_6)\\
@@ -324,10 +327,10 @@ est un théorème du calcul propositionnel intuitionniste.
 
 \exercice
 
-En utilisant l'une quelconque (au choix) des sémantiques vues en cours
-pour le calcul propositionnel intuitionniste, montrer que la formule
-suivante n'est pas démontrable en calcul propositionnel
-intuitionniste :
+En utilisant l'une quelconque des sémantiques vues en cours pour le
+calcul propositionnel intuitionniste (au choix : toutes marcheront),
+montrer que la formule suivante n'est pas démontrable en calcul
+propositionnel intuitionniste :
 \[
 \big(\neg(A\land B) \land \neg(B\land C) \land \neg(C\land A)\big)
 \;\Rightarrow\; \big(\neg A \lor \neg B \lor \neg C\big)
@@ -339,9 +342,9 @@ inaccessibles depuis les uns les autres.  Si on préfère la sémantique
 des ouverts, considérer trois secteurs angulaires ouverts dans le
 plan, ayant un même sommet et qui se jouxtent sans s'intersecter.  Si
 on préfère la sémantique de la réalisabilité ou des problèmes finis,
-il s'agit d'énoncer le fait qu'il est impossible de trouver une partie
-vide parmi trois, sans avoir accès à ces parties, même si on a la
-promesse qu'au moins deux d'entre elles sont vides : pour la
+il s'agit d'énoncer le fait qu'il est impossible de déterminer une
+partie vide parmi trois, sans avoir accès à ces parties, même si on a
+la promesse qu'au moins deux d'entre elles sont vides : pour la
 réalisabilité, on pourra considérer une des parties valant
 $\mathbb{N}$ et les deux autres valant $\varnothing$ et constater
 qu'on ne peut pas réaliser les trois affectations à la fois, tandis
@@ -385,36 +388,36 @@ donc la formule n'est pas démontrable.
 
 \emph{Sémantique des ouverts :} Considérons dans $\mathbb{R}^2$ trois
 secteurs angulaires ouverts $U,V,W$, chacun ayant l'origine comme
-sommet et d'angle $\frac{2\pi}{3}$, et qui se jouxtent par une
-droite : par exemple, soit $U$ le secteur formé des nombres complexes
-non nuls dont l'argument (choisi entre $0$ et $2\pi$) est strictement
-compris entre $0$ et $\frac{2\pi}{3}$, soit $V$ celui dont l'argument
-est strictement compris entre $\frac{2\pi}{3}$ et $\frac{4\pi}{3}$ et
-soit $W$ celui dont l'argument est strictement compris entre
+sommet et d'angle $\frac{2\pi}{3}$, et qui se jouxtent deux par deux :
+par exemple, soit $U$ le secteur formé des nombres complexes non nuls
+dont l'argument (choisi entre $0$ et $2\pi$) est strictement compris
+entre $0$ et $\frac{2\pi}{3}$, soit $V$ celui dont l'argument est
+strictement compris entre $\frac{2\pi}{3}$ et $\frac{4\pi}{3}$ et soit
+$W$ celui dont l'argument est strictement compris entre
 $\frac{4\pi}{3}$ et $2\pi$.  Avec ces choix, les trois secteurs sont
-disjoints, donc chacun de $U\dottedland V$, $V\dottedland W$ et
-$W\dottedland U$ est vide donc $\dottedneg(U\dottedland V) \dottedland
-\dottedneg(V\dottedland W) \dottedland \dottedneg(W\dottedland U)$ est
-plein.  En revanche, $\dottedneg U$, $\dottedneg V$ et $\dottedneg W$
-sont des secteurs ouverts ayant l'origine pour sommet et d'angle
-$\frac{4\pi}{3}$ (par exemple, $\dottedneg U$ est l'intérieur de
-l'adhérence de $V\cup W$, et symétriquement pour les autres), donc
-aucun ne contient l'origine, donc $\dottedneg U \dottedlor \dottedneg
-V \dottedlor \dottedneg W$ non plus : c'est même précisément le
-complémentaire de l'origine.  Par conséquent,
-$(\dottedneg(U\dottedland V) \dottedland \dottedneg(V\dottedland W)
-\dottedland \dottedneg(W\dottedland U)) \dottedlimp (\dottedneg U
-\dottedlor \dottedneg V \dottedlor \dottedneg W)$ est aussi le
-complémentaire de l'origine.  Si la formule proposée avait été
-démontrable, on aurait trouvé tout $\mathbb{R}^2$ (par
-\emph{correction} de la sémantique des ouverts) : ce n'est pas le cas,
-donc la formule n'est pas démontrable.
+deux à deux disjoints, donc chacun de $U\dottedland V$, $V\dottedland
+W$ et $W\dottedland U$ est vide donc $\dottedneg(U\dottedland V)
+\dottedland \dottedneg(V\dottedland W) \dottedland
+\dottedneg(W\dottedland U)$ est plein.  En revanche, $\dottedneg U$,
+$\dottedneg V$ et $\dottedneg W$ sont des secteurs ouverts ayant
+l'origine pour sommet et d'angle $\frac{4\pi}{3}$ (par exemple,
+$\dottedneg U$ est l'intérieur de l'adhérence de $V\cup W$, et
+symétriquement pour les autres), donc aucun ne contient l'origine,
+donc $\dottedneg U \dottedlor \dottedneg V \dottedlor \dottedneg W$
+non plus : c'est même précisément le complémentaire de l'origine.  Par
+conséquent, $(\dottedneg(U\dottedland V) \dottedland
+\dottedneg(V\dottedland W) \dottedland \dottedneg(W\dottedland U))
+\dottedlimp (\dottedneg U \dottedlor \dottedneg V \dottedlor
+\dottedneg W)$ est aussi le complémentaire de l'origine.  Si la
+formule proposée avait été démontrable, on aurait trouvé tout
+$\mathbb{R}^2$ (par \emph{correction} de la sémantique des ouverts) :
+ce n'est pas le cas, donc la formule n'est pas démontrable.
 
 \emph{Sémantique de la réalisabilité :} Supposons qu'il existe un
 \emph{même} programme $e$ qui réalise la formule qu'on considère
 quelles que soient les parties $P,Q,R \subseteq \mathbb{N}$ mises à la
-place des variables propositionnelles $A,B,C$.  Notons que (au moins)
-deux des trois parties $P,Q,R$ sont vides, alors
+place des variables propositionnelles $A,B,C$.  Notons que si (au
+moins) deux des trois parties $P,Q,R$ sont vides, alors
 $\dottedneg(P\dottedland Q)$, $\dottedneg(Q\dottedland R)$ et
 $\dottedneg(R\dottedland P)$ sont égales à $\mathbb{N}$, donc $\langle
 0,0,0\rangle$ est dans $\dottedneg(P\dottedland Q) \dottedland
@@ -451,18 +454,19 @@ existe un \emph{même} candidat $f$ qui soit solution du problème
 $(\dottedneg(E\dottedland F) \dottedland \dottedneg(F\dottedland G)
 \dottedland \dottedneg(G\dottedland E)) \dottedlimp (\dottedneg E
 \dottedlor \dottedneg F \dottedlor \dottedneg G)$.  C'est une fonction
+$\{\bullet_0\} \to \{\bullet_{p'}, \bullet_{q'}, \bullet_{r'}\}$
 censée envoyer $\bullet_0$, s'il est solution, sur une solution du
 problème $\dottedneg E \dottedlor \dottedneg F \dottedlor \dottedneg
 G$, c'est-à-dire qu'il doit indiquer une partie vide parmi $P,Q,R$.
 Mais ce n'est pas possible sans aucune information sur les parties !
 Pour être tout à fait précis, supposons (sans perte de généralité,
-puisque le problème est symétrique) qu'il renvoie $\bullet_{p'}$ :
-alors en considérant le cas $P = \{\bullet_p\}$ et $Q = \varnothing$
-et $R = \varnothing$ on a une contradiction.  Or si la formule
-proposée avait été démontrable, il existerait un $f$ qui soit solution
-quels que soient $P,Q,R$ (par \emph{correction} de la sémantique des
-la réalisabilité) : on vient de voir que ce n'est pas le cas, donc la
-formule n'est pas démontrable.
+puisque le problème est symétrique) que $f(\bullet_0) =
+\bullet_{p'}$ : alors en considérant le cas $P = \{\bullet_p\}$ et $Q
+= \varnothing$ et $R = \varnothing$ on a une contradiction.  Or si la
+formule proposée avait été démontrable, il existerait un $f$ qui soit
+solution quels que soient $P,Q,R$ (par \emph{correction} de la
+sémantique des la réalisabilité) : on vient de voir que ce n'est pas
+le cas, donc la formule n'est pas démontrable.
 \end{corrige}
 
 
@@ -511,16 +515,16 @@ ajoutant $P$ aux hypothèses.
 
 \textbf{(2)} Le théorème de Gödel affirme que (sous l'hypothèse
 $\mathsf{Consis}(\mathsf{PA})$, qui est bien affirmable dans le cadre
-où on travaille), $\mathsf{Consis}(\mathsf{PA})$ n'est pas démontrable
-dans $\mathsf{PA}$ ; comme on est en logique classique (arithmétique
-de Peano !), c'est pareil que de dire que
+$\mathsf{ZFC}$ où on travaille), $\mathsf{Consis}(\mathsf{PA})$ n'est
+pas démontrable dans $\mathsf{PA}$ ; comme on est en logique classique
+(arithmétique de Peano !), c'est pareil que de dire que
 $\neg\neg\mathsf{Consis}(\mathsf{PA})$, ou, si on préfère,
 $(\neg\mathsf{Consis}(\mathsf{PA}))\Rightarrow\bot$ n'est pas
 démontrable dans $\mathsf{PA}$.  D'après la question précédente, cela
 signifie exactement que $\bot$ n'est pas démontrable dans $\mathsf{PA}
 \cup \{\neg\mathsf{Consis}(\mathsf{PA})\} =: \mathsf{PA}^*$.
 Autrement dit, on a $\mathsf{Consis}(\mathsf{PA}^*)$ : la théorie
-$\mathsf{PA}^*$ n'a pas de contradiction.
+$\mathsf{PA}^*$ ne démontre pas de contradiction.
 
 \textbf{(3)} L'affirmation $\mathsf{Consis}(\mathsf{PA}^*)$ dit qu'on
 ne peut pas arriver à une contradiction à partir des axiomes de Peano
@@ -532,9 +536,11 @@ On a donc $\mathsf{Consis}(\mathsf{PA}^*) \Rightarrow
 d'arithmétique élémentaire, donc dans $\mathsf{PA}$).
 
 Comme $\mathsf{PA}^*$ a $\neg\mathsf{Consis}(\mathsf{PA})$ dans ses
-axiomes, si $\mathsf{Consis}(\mathsf{PA}^*) \Rightarrow
-\mathsf{Consis}(\mathsf{PA})$, on en déduit que
-$\neg\mathsf{Consis}(\mathsf{PA}^*)$ dans $\mathsf{PA}^*$.
+axiomes, et comme on vient d'expliquer que
+$\mathsf{Consis}(\mathsf{PA}^*) \Rightarrow
+\mathsf{Consis}(\mathsf{PA})$ (se démontre dans $\mathsf{PA}$), on en
+déduit que $\neg\mathsf{Consis}(\mathsf{PA}^*)$ se démontre dans
+$\mathsf{PA}^*$.
 
 \textbf{(4)} La théorie $\mathsf{PA}^*$ \emph{« pense »} (ou plus
 exactement, postule) que l'arithmétique de Peano est contradictoire,
@@ -661,15 +667,15 @@ $\frac{p}{q}$ comme réel calculable.
 \begin{corrige}
 Si $\lfloor z\rfloor$ désigne la partie entière de $z$, la fonction
 $(p,q,n) \mapsto \lfloor 2^n\, \frac{p}{q}\rfloor$ est calculable car
-c'est la partie quotient de la division euclidienne de $2^n\, p$
-par $q$, et il s'agit d'un numérateur d'approximation dyadique de
-niveau $n$ de $\frac{p}{q}$ puisque $|\lfloor z\rfloor - z| \leq 1$.
-Donc, la fonction qui à $p$ et $q$ associe le code d'une fonction
-calculant $n \mapsto \lfloor 2^n\, \frac{p}{q}\rfloor$ est calculable
-(par le théorème s-m-n si on veut être très précis).  Un tel programme
-s'écrit par exemple « \texttt{fun p -> fun q -> fun n -> (p * (pow 2
-  n)) / q} » en supposant que « \texttt{pow} » représente
-l'exponentiation entière et ‘\texttt{/}’ la division euclidienne.
+c'est le quotient de la division euclidienne de $2^n\, p$ par $q$, et
+il s'agit d'un numérateur d'approximation dyadique de niveau $n$
+de $\frac{p}{q}$ puisque $|\lfloor z\rfloor - z| \leq 1$.  Donc, la
+fonction qui à $p$ et $q$ associe le code d'une fonction calculant $n
+\mapsto \lfloor 2^n\, \frac{p}{q}\rfloor$ est calculable (par le
+théorème s-m-n si on veut être très précis).  Un tel programme s'écrit
+par exemple « \texttt{fun p -> fun q -> fun n -> (p * (pow 2 n)) /
+  q} » en supposant que « \texttt{pow} » représente l'exponentiation
+entière et ‘\texttt{/}’ la division euclidienne.
 \end{corrige}
 
 \medskip
@@ -691,7 +697,7 @@ représentant $x$ s'écrit par exemple « \texttt{fun xf -> fun n -> -(xf
   n)} ».
 
 Pour la valeur absolue, on procède de même en remarquant que si $|k -
-2^n\,x| \leq 1$, alors $|(|k|) - 2^n\,(|x|)| \leq 1$ (d'après
+2^n\,x| \leq 1$, alors $\Big||k| - 2^n\,|x|\Big| \leq 1$ (d'après
 l'inégalité qui a été rappelée).  Ceci montre que si $n \mapsto k_n$
 représente $x$ alors $n \mapsto |k_n|$ représente $|x|$ : un programme
 correspondant s'écrit par exemple « \texttt{fun xf -> fun n -> abs(xf
@@ -745,9 +751,9 @@ on cherche un multiple de $4$ compris au sens large entre les entiers
 $\ell-2$ et $\ell+2$, ce qui existe certainement car il y a $5$
 entiers consécutifs dans cet intervalle : pour faire ça
 algorithmiquement, on peut appeler $k =
-\lfloor\frac{\ell+2}{4}\rfloor$ la partie quotient de la division
-euclidienne de $\ell+2$ par $4$, on aura alors $4k+r = \ell+2$ avec
-reste $0\leq r<4$, donc $\ell-2 < 4k \leq \ell+2$.
+\lfloor\frac{\ell+2}{4}\rfloor$ le quotient de la division euclidienne
+de $\ell+2$ par $4$, car on aura alors $4k+r = \ell+2$ avec reste
+$0\leq r<4$, donc $\ell-2 < 4k \leq \ell+2$.
 
 Si $i,j$ désignent des numérateurs d'approximations dyadiques de
 niveau $n+2$ de $x$ et $y$ respectivement, c'est-à-dire $|i -
@@ -766,14 +772,15 @@ On en déduit que si $n \mapsto i_n$ représente $x$ et que $n \mapsto
 j_n$ représente $y$ alors $n \mapsto \lfloor(i_{n+2} + j_{n+2} +
 2)/4\rfloor$ représente $x+y$.  Un programme calculant une fonction
 représentant $x+y$ à partir de fonctions représentant $x$ et $y$
-s'écrit par exemple « \texttt{fun xf -> fun yf -> fun n -> ((xf (n+2)) +
-  (yf (n+2)) + 2)/4} ».
+s'écrit par exemple « \texttt{fun xf -> fun yf -> fun n -> ((xf (n+2))
+  + (yf (n+2)) + 2)/4} » (toujours en notant ‘\texttt{/}’ la division
+euclidienne).
 \end{corrige}
 
 \medskip
 
-\textbf{(5)} Montrer qu'un réel calculable $z$ représenté par une
-fonction $n \mapsto k_n$ vérifie $z\leq 0$ si et seulement on a $k_n
+\textbf{(5)} Montrer qu'un réel calculable $z$, représenté par une
+fonction $n \mapsto k_n$, vérifie $z\leq 0$ si et seulement on a $k_n
 \leq 1$ pour tout $n$.  En déduire comment, donnée une fonction $n
 \mapsto k_n$ représentant $z$ calculable, et en \emph{supposant}
 $z>0$, on peut calculer algorithmiquement un $n\in\mathbb{N}$ tel que
@@ -786,23 +793,23 @@ peut décider algorithmiquement si $z<0$ ou $z>0$.
 \begin{corrige}
 Si $k_n \leq 1$ pour tout $n$, alors $z \leq \frac{k_n+1}{2^n} \leq
 \frac{1}{2^{n-1}}$ pour tout $n$, donc $z \leq 0$.  Réciproquement, si
-$z \leq 0$, alors $0 \geq \frac{k_n-1}{2^n}$ donc $k_n \leq 1$ pour
-tout $n$.
+$z \leq 0$, alors $0 \geq z \geq \frac{k_n-1}{2^n}$ donc $k_n \leq 1$
+pour tout $n$.
 
 On en déduit que si on \emph{suppose} $z>0$, il existe un indice $n$
-tel que $k_n \geq 2$ dans toute fonction représentant $z$ ; et on a
-alors $z \geq \frac{k_n-1}{2^n} \geq \frac{1}{2^n}$ comme recherché.
-Pour trouver ce $n$, il suffit d'effectuer une boucle infinie
-calculant $k_n$ en s'arrêtant dès que $k_n \geq 2$ : d'après ce qui
-vient d'être dit, l'hypothèse $z>0$ garantit la terminaison de la
-boucle.
+tel que $k_n \geq 2$ dans toute fonction $n \mapsto k_n$
+représentant $z$ ; et pour un tel $n$ on a alors $z \geq
+\frac{k_n-1}{2^n} \geq \frac{1}{2^n}$ comme recherché.  Pour trouver
+ce $n$, il suffit d'effectuer une boucle infinie calculant $k_n$ en
+s'arrêtant dès que $k_n \geq 2$ : d'après ce qui vient d'être dit,
+l'hypothèse $z>0$ garantit la terminaison de la boucle.
 
 Si maintenant on suppose simplement $z\neq 0$, il existe soit un
-indice $n$ tel que $k_n \geq 2$ soit un indice tel que $k_n \leq -2$ :
-pour décider le signe de $z$, il suffit d'effectuer une boucle infinie
-jusqu'à ce qu'une de ces conditions soit satisfaite, et de renvoier
-« positif » ou « négatif » selon qu'on a trouvé un $n$ vérifiant l'un
-ou l'autre.
+indice $n$ tel que $k_n \geq 2$ soit un indice tel que $k_n \leq -2$
+(par symétrie) : pour décider le signe de $z$, il suffit d'effectuer
+une boucle infinie jusqu'à ce qu'une de ces conditions soit
+satisfaite, et de renvoier « positif » ou « négatif » selon qu'on a
+trouvé un $n$ vérifiant l'un ou l'autre.
 \end{corrige}
 
 \medskip
@@ -815,12 +822,13 @@ dernier représente un réel calculable.  Autrement dit, la fonction qui
 représentant un certain réel $x$, et $0$ sinon, n'est pas calculable.
 
 \begin{corrige}
-C'est une conséquence du théorème de Rice : l'ensemble des fonctions
-partielles $\mathbb{N} \dasharrow \mathbb{Z}$ représentant un réel
-n'est ni vide ni plein (il n'est pas vide car la fonction constante
-$0$ est dedans, et pas plein parce que la fonction définie nulle part
-n'est pas dedans), donc le théorème de Rice affirme que l'ensemble des
-$e$ tels que $\varphi_e$ soit dans cet ensemble n'est pas décidable.
+C'est une conséquence du théorème de Rice : le sous-ensemble des
+fonctions partielles $\mathbb{N} \dasharrow \mathbb{Z}$ qui sont une
+fonction totale représentant un réel n'est ni vide ni plein (il n'est
+pas vide car la fonction constante $0$ est dedans, et pas plein parce
+que la fonction définie nulle part n'est pas dedans), donc le théorème
+de Rice affirme que l'ensemble des $e$ tels que $\varphi_e$ soit dans
+cet ensemble n'est pas décidable.
 \end{corrige}
 
 \medskip
@@ -832,7 +840,7 @@ manière suivante :
 \eta(e) =
 \left\{
 \begin{array}{ll}
-\displaystyle\frac{1}{2^m}&\text{~si le calcul de $\varphi_e(0)$ termine en $m$ étapes (et pas moins)}\\
+\displaystyle\frac{1}{2^m}&\text{~si le calcul de $\varphi_e(0)$ termine en exactement $m$ étapes}\\
 \vphantom{\displaystyle\frac{0}{0}}0&\text{~si $\varphi_e(0){\uparrow}$}\\
 \end{array}
 \right.
@@ -851,11 +859,11 @@ calculable).
 \begin{corrige}
 On a vu en cours qu'il est possible de tester algorithmiquement si le
 calcul de $\varphi_e(0)$ termine en $m$ étapes (ou, si on préfère, si
-$n$ est un arbre de calcul pour $\varphi_e(0)$).  Pour calculer un
+$m$ est un arbre de calcul pour $\varphi_e(0)$).  Pour calculer un
 numérateur d'approximation dyadique de niveau $n$ de $\eta(e)$, on va
 faire ce test : on lance l'exécution de $\varphi_e(0)$ sur $n$
 étapes : si le calcul termine au bout de en $m\leq n$ étapes (ou, si
-on préfèr, si on trouve un arbre de calcul $m\leq n$), on renvoie
+on préfère, si on trouve un arbre de calcul $m\leq n$), on renvoie
 l'approximant $\frac{1}{2^m}$, c'est-à-dire qu'on renvoie le
 numérateur $2^{n-m}$, qui convient car $\eta(e) = \frac{1}{2^m}$
 exactement ; s'il ne termine pas dans le temps imparti, on renvoie le
@@ -921,7 +929,7 @@ possible algorithmiquement de tester si un réel calculable est $\geq
 0$ ou $\leq 0$, i.e., il n'existe pas d'algorithme qui, donnée une
 fonction représentant un réel calculable $x$, peut renvoyer « vrai »
 si $x\geq 0$ ou « faux » si $x\leq 0$ (les deux réponses étant
-acceptées si $x=0$).
+acceptables si $x=0$).
 
 \begin{corrige}
 On définit
@@ -929,25 +937,25 @@ On définit
 \eta'(e) =
 \left\{
 \begin{array}{ll}
-\displaystyle\frac{1}{2^m}&\text{~si le calcul de $\varphi_e(0)$ termine en $m$ étapes (et pas moins) et $\varphi_e(0) = 0$}\\
-\displaystyle-\frac{1}{2^m}&\text{~si le calcul de $\varphi_e(0)$ termine en $m$ étapes (et pas moins) et $\varphi_e(0) \neq 0$}\\
+\displaystyle\frac{1}{2^m}&\text{~si le calcul de $\varphi_e(0)$ termine en exactement $m$ étapes et que $\varphi_e(0) = 0$}\\
+\displaystyle-\frac{1}{2^m}&\text{~si le calcul de $\varphi_e(0)$ termine en exactement $m$ étapes et que $\varphi_e(0) \neq 0$}\\
 \vphantom{\displaystyle\frac{0}{0}}0&\text{~si $\varphi_e(0){\uparrow}$}\\
 \end{array}
 \right.
 \]
 
-Le même argument qu'à la question (7) montre que $\eta'(e)$ est
-calculable à partir de $e$ : donné un niveau $n$, il suffit de lancer
-l'exécution de $\varphi_e(0)$ sur $n$ étapes et, si elle termine en
-$m\leq n$ étapes, renvoyer l'approximant $\frac{1}{2^m}$ ou
-$-\frac{1}{2^m}$ (c'est-à-dire le numérateur $2^{n-m}$ ou $-2^{n-m}$)
-selon que le résultat qu'on a calculé est $0$ ou $\neq 0$, et
-sinon $0$.  Comme en (9), décider si $\eta'(e)\leq 0$ ou $\eta'(e)\geq
-0$ (en acceptant n'importe quelle réponse si c'est $0$) reviendrait à
-décider si $\varphi_e(0){\downarrow} = 0$ ou $\varphi_e(0){\downarrow}
-\neq 0$ (en acceptant n'importe quelle réponse si
-$\varphi_e(0){\uparrow}$, mais toujours avec l'obligation de
-terminer), et on a indiqué que ce n'était pas possible.
+Un argument analogue à celi de la la question (7) montre que
+$\eta'(e)$ est calculable à partir de $e$.  Précisément : donné un
+niveau $n$, il suffit de lancer l'exécution de $\varphi_e(0)$ sur $n$
+étapes et, si elle termine en $m\leq n$ étapes, renvoyer l'approximant
+$\frac{1}{2^m}$ ou $-\frac{1}{2^m}$ (c'est-à-dire le numérateur
+$2^{n-m}$ ou $-2^{n-m}$) selon que le résultat qu'on a calculé est $0$
+ou $\neq 0$, et sinon $0$.  Comme en (9), décider si $\eta'(e)\leq 0$
+ou $\eta'(e)\geq 0$ (en acceptant n'importe quelle réponse si
+c'est $0$) reviendrait à décider si $\varphi_e(0){\downarrow} = 0$ ou
+$\varphi_e(0){\downarrow} \neq 0$ (en acceptant n'importe quelle
+réponse si $\varphi_e(0){\uparrow}$, mais toujours avec l'obligation
+de terminer), et on a indiqué que ce n'était pas possible.
 \end{corrige}
 
 \medskip
@@ -996,7 +1004,8 @@ $n \mapsto k_n$ à partir de $n \mapsto u_n$.
 montrer qu'il n'existe pas d'algorithme qui, donnée une fonction $n
 \mapsto k_n$ représentant un réel $x$ calculable entre $0$ et $1$,
 renvoie une fonction calculable $n \mapsto u_n$ qui soit une écriture
-binaire de $x$.  (Considérer $\frac{1}{2}(\eta'(e)+1)$.)
+binaire de $x$.  (\emph{Indication :} considérer
+$\frac{1}{2}(\eta'(e)+1)$.)
 
 \begin{corrige}
 Si un tel algorithme existait, on pourrait l'appliquer à $x_e =
@@ -1015,9 +1024,9 @@ de $e$.
 
 \textbf{(13)} En utilisant de nouveau la question (10), montrer qu'il
 n'existe pas d'algorithme qui, donnés deux réels calculables naïfs
-$x,y$ (avec $x$ entre $\frac{1}{2}$ et $1$ et $y$ entre $0$ et
-$\frac{1}{2}$ pour simplifier) sous forme d'une fonction calculant une
-écriture binaire, renvoie $x-y$ sous cette même forme.
+$x,y$ (avec, disons, $x$ entre $\frac{1}{2}$ et $1$ et $y$ entre $0$
+et $\frac{1}{2}$) sous forme d'une fonction calculant une écriture
+binaire, renvoie $x-y$ sous cette même forme.
 
 \begin{corrige}
 Considérons $\eta'(e)$ le réel calculable en fonction de $e$ défini à