First pass of proofreading.

1 files changed, 145 insertions, 112 deletions

diff --git a/controle-20240126.tex b/controle-20240126.tex
index b55a66c..5f8fae2 100644
--- a/controle-20240126.tex
+++ b/controle-20240126.tex
@@ -28,8 +28,8 @@
 \newtheorem{comcnt}{Tout}
 \newcommand\thingy{%
 \refstepcounter{comcnt}\medskip\noindent\textbf{\thecomcnt.} }
-\newcommand\exercice{%
-\refstepcounter{comcnt}\bigskip\noindent\textbf{Exercice~\thecomcnt.}\par\nobreak}
+\newcommand\exercice[1][Exercice]{%
+\refstepcounter{comcnt}\bigskip\noindent\textbf{#1~\thecomcnt.}\par\nobreak}
 \renewcommand{\qedsymbol}{\smiley}
 %
 \newcommand{\dbllangle}{\mathopen{\langle\!\langle}}
@@ -73,9 +73,22 @@
 
 \noindent\textbf{Consignes.}
 
-Les exercices sont totalement indépendants.  Ils pourront être traités
-dans un ordre quelconque, mais on demande de faire apparaître de façon
-très visible dans les copies où commence chaque exercice.
+Les exercices et le problème sont totalement indépendants.  Ils
+pourront être traités dans un ordre quelconque, mais on demande de
+faire apparaître de façon très visible dans les copies où commence
+chaque exercice (tirez au moins un trait sur toute la largeur de la
+feuille entre deux exercices).
+
+Les questions du problème dépendent les unes des autres, mais ont été
+rédigées de manière à ce que chacune donne toutes les informations
+nécessaires pour passer à la suite.  Mais comme les questions (du
+problème) présentent une gradation approximative de difficulté, il est
+recommandé de les traiter dans l'ordre.
+
+La longueur du sujet ne doit pas effrayer : l'énoncé du problème est
+très long parce que des rappels ont été faits et que les questions ont
+été rédigées de façon aussi précise que possible.  Par ailleurs, il ne
+sera pas nécessaire de tout traiter pour avoir le maximum des points.
 
 \medbreak
 
@@ -148,7 +161,7 @@ thm < \textrm{(commande à trouver)}\\
 \ \ ============================\\
 \ \ B\\
 \\
-thm < \textrm{(commande à trouver)}
+thm < \textrm{(commande à proposer)}
 }
 
 \smallskip
@@ -178,9 +191,10 @@ pour terminer la démonstration).
 (Dans cet exercice, on ne demande pas de justifier les réponses.)
 
 \textbf{(1)} En calcul propositionnel intuitionniste, quelle est la
-conclusion de la démonstration représentée par le $\lambda$-terme
-suivant ?  (Ou si on préfère : quel est le type de ce terme du
-$\lambda$-calcul simplement typé enrichi de types produits ?)
+conclusion de la démonstration représentée par le $\lambda$-terme de
+preuve suivant ?  (Ou si on préfère : quel est le type de ce terme du
+$\lambda$-calcul simplement typé enrichi de types produits, qu'on a
+écrit en notations logiques ?)
 \[
 \lambda(p: C\land(A\Rightarrow B)).\,
 \lambda(h:A).\,
@@ -189,7 +203,8 @@ $\lambda$-calcul simplement typé enrichi de types produits ?)
 (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 suivant ?
+la démonstration représentée par le $\lambda$-terme de preuve
+suivant ?
 \[
 \lambda(p: C\land\forall x. B(x))).\,
 \lambda(x:I).\,
@@ -200,7 +215,8 @@ 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 suivant ?
+la démonstration représentée par le $\lambda$-terme de preuve
+suivant ?
 \[
 \lambda(p: \exists x.(A\Rightarrow B(x))).\,
 \lambda(h:A).\,
@@ -252,7 +268,7 @@ $\lambda$-calcul non typé :
 \]
 (autrement dit, \texttt{fun f -> fun z -> f z (fun g -> g z)} en
 syntaxe OCaml).  Quel théorème du calcul propositionnel intuitionniste
-obtient-on de ceci ?
+obtient-on de ceci par Curry-Howard ?
 
 \begin{corrige}
 Dans une première phase, on collecte les types et contraintes
@@ -317,17 +333,20 @@ intuitionniste :
 \;\Rightarrow\; \big(\neg A \lor \neg B \lor \neg C\big)
 \]
 
-(\emph{Indications :} si on préfère la sémantique de Kripke,
-considérer un monde permettant d'accéder à trois autres mondes, tous
-les trois 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, é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
-sémantique des problèmes finis, on prendra par ailleurs trois
-problèmes ayant un seul candidat chacun.)
+(\emph{Indications.} Si on préfère la sémantique de Kripke, considérer
+un monde permettant d'accéder à trois autres mondes, tous les trois
+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
+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
+que pour la sémantique des problèmes finis, on pourra trois problèmes
+ayant un seul candidat chacun mais un seul ayant une solution.)
 
 \begin{corrige}
 On donne quatre solutions possibles, une pour chaque sémantique vue en
@@ -454,27 +473,29 @@ formule n'est pas démontrable.
 
 \exercice
 
-(On ne demande pas ici de réponses compliquées.)
+(On ne demande pas ici de réponses compliquées !)
 
 \textbf{(1)} Expliquer rapidement pourquoi, si $\mathscr{T}$ est un
 ensemble de formules logiques (par exemple de logique de premier
 ordre, mais peu importent les détails), on peut démontrer
-$P\rightarrow Q$ à partir de $\mathscr{T}$ si et seulement si on peut
+$P\Rightarrow Q$ à partir de $\mathscr{T}$ si et seulement si on peut
 démontrer $Q$ à partir de $\mathscr{T} \cup \{P\}$.
 
 \textbf{(2)} Déduire de (1) et du théorème de Gödel que la théorie
 $\mathsf{PA}^*$ formée en ajoutant l'axiome
 $\neg\mathsf{Consis}(\mathsf{PA})$ à l'arithmétique de
 Peano ($\mathsf{PA}$), ne prouve pas $\bot$ (c'est-à-dire qu'elle
-n'est pas contradictoire).  On rappelle que
-$\mathsf{Consis}(\mathsf{PA})$ est l'énoncé qui affirme que
-$\mathsf{PA}$ n'est pas contradictoire, et que cet énoncé est
-démontrable dans les mathématiques usuelles $\mathsf{ZFC}$ où on
-travaille.
+n'est pas contradictoire).  Ici, $\mathsf{Consis}(\mathsf{PA})$ est
+l'énoncé qui affirme que $\mathsf{PA}$ n'est pas contradictoire, et on
+rappelle que cet énoncé est démontrable dans les mathématiques
+usuelles ($\mathsf{ZFC}$) où on travaille.
+
+(On rappelle aussi que $\mathsf{PA}$ travaille en logique classique.)
 
-\textbf{(3)} Expliquer pourquoi $\mathsf{Consis}(\mathsf{PA}^*)$
-implique $\mathsf{Consis}(\mathsf{PA})$ et en déduire que
-$\mathsf{PA}^*$ démontre $\neg\mathsf{Consis}(\mathsf{PA}^*)$.
+\textbf{(3)} Expliquer pourquoi $\mathsf{Consis}(\mathsf{PA}^*)$ est
+plus fort que (i.e., implique) $\mathsf{Consis}(\mathsf{PA})$, et en
+déduire que $\mathsf{PA}^*$ démontre
+$\neg\mathsf{Consis}(\mathsf{PA}^*)$.
 
 \textbf{(4)} On a vu en (2) que $\mathsf{PA}^*$ n'est pas
 contradictoire, et en (3) que $\mathsf{PA}^*$ démontre que
@@ -530,24 +551,26 @@ faux, donc d'aboutir effectivement à une contradiction.
 %
 %
 
-\exercice
+\bigbreak
+
+\exercice[Problème]
 
 \textbf{Motivations :} On s'intéresse dans cet exercice à la notion de
-\emph{réel calculable}, qu'on va définir comme une formalisation
+\emph{réel calculable}, qu'on va définir : c'est une formalisation
 possible d'un nombre réel exact pouvant être manipulé par un
 ordinateur.  L'idée la plus évidente pour définir les réels
 calculables est sans doute de considérer ceux dont une écriture
-binaire est une fonction calculable (et de les représenter par le code
-d'un programme qui calcule cette fonction) : on va voir plus loin que
-cette définition « naïve » souffre de graves problèmes.  À la place,
-on va définir un réel calculable comme un réel dont on peut calculer
-par un programme une approximation rationnelle à $\varepsilon$ près
-pour n'importe quel $\varepsilon>0$ donné en entrée (et représenter le
-réel par le code d'un programme qui prend $\varepsilon$ et renvoie
-l'approximation).  Pour rendre cette définition plus commode à manier,
-on va se limiter à $\varepsilon$ de la forme $\frac{1}{2^n}$ et
-renvoyer une approximation elle-même de la forme $\frac{k}{2^n}$ (cela
-ne change rien d'essentiel).
+binaire est une fonction calculable (et de les représenter par cette
+fonction) : on va voir plus loin que cette définition « naïve »
+souffre de graves problèmes.  À la place, on va définir un réel
+calculable comme un réel dont on peut calculer par un programme une
+approximation rationnelle à $\varepsilon$ près pour n'importe quel
+$\varepsilon>0$ donné en entrée (et représenter le réel par une
+fonction qui prend $\varepsilon$ et renvoie l'approximation).  Pour
+rendre cette définition plus commode à manier, on va se limiter à
+$\varepsilon$ de la forme $\frac{1}{2^n}$ et renvoyer une
+approximation elle-même de la forme $\frac{k}{2^n}$ (cela ne change
+rien d'essentiel).
 
 \smallskip
 
@@ -557,22 +580,22 @@ On fait donc les définitions suivantes :
   $\frac{k}{2^n}$ avec $k\in\mathbb{Z}$ et $n\in \mathbb{N}$ (i.e.,
   son dénominateur est une puissance de $2$).  Pour être plus précis,
   on peut appeler \textbf{dyadique de niveau $n$} un rationnel de la
-  forme $\frac{k}{2^n}$ avec $k\in\mathbb{Z}$ (pour ce $n$-là ; noter
+  forme $\frac{k}{2^n}$ avec $k\in\mathbb{Z}$ (pour ce $n$-là).  Noter
   qu'on ne demande pas que $\frac{k}{2^n}$ soit irréductible, par
-  exemple $42 = \frac{84}{2} = \frac{168}{2^2} = \cdots$ est un
-  dyadique de tout niveau).
+  exemple $42 = \frac{84}{2} = \frac{168}{2^2} = \cdots$ peut être vu
+  comme un dyadique de n'importe quel niveau.
 \item Si $x \in \mathbb{R}$, un \textbf{numérateur d'approximation
   dyadique de niveau $n$} de $x$ est un entier $k$ tel que $|k-2^n\,
   x|\leq 1$.  L'approximation dyadique elle-même est alors par
   définition $\frac{k}{2^n}$, et vérifie donc $|\frac{k}{2^n}-x|\leq
   \frac{1}{2^n}$.
 \item Un réel $x \in \mathbb{R}$ est dit \textbf{calculable} lorsqu'il
-  existe une fonction \emph{calculable} $\mathbb{N} \to \mathbb{Z}, n
-  \mapsto k_n$ telle que $k_n$ soit un numérateur d'approximation
-  dyadique de niveau $n$ de $x$.  Autrement dit, il existe un
-  programme qui, prenant $n$ en entrée, renvoie une approximation
-  dyadique $\frac{k}{2^n}$ de niveau $n$ de $x$ (représentée sous
-  forme du numérateur de la fraction, puisque le dénominateur est par
+  y a une fonction \emph{calculable} (totale) $\mathbb{N} \to
+  \mathbb{Z}, n \mapsto k_n$ telle que $k_n$ soit un numérateur
+  d'approximation dyadique de niveau $n$ de $x$.  Autrement dit, il
+  existe un programme qui, prenant $n$ en entrée, renvoie une
+  approximation dyadique $\frac{k_n}{2^n}$ de niveau $n$ de $x$
+  (représentée par le seul numérateur, puisque le dénominateur est par
   définition $2^n$).  Une telle fonction $n \mapsto k_n$, ou un
   programme qui la calcule, est dit \textbf{représenter} le réel $x$.
 \end{itemize}
@@ -592,9 +615,11 @@ On prendra garde aux faits suivants :
     x-1\,;\,2^n\, x + 1]$ de longueur $2$).  À titre d'exemple, le
   réel $0$ peut être représenté par n'importe quelle fonction
   calculable $n \mapsto k_n$ renvoyant un $k_n$ dans $\{-1,0,1\}$.
-\item Même une fois fixée la fonction calculable $n \mapsto k_n$
+\item Même une fois fixée la fonction mathématique $n \mapsto k_n$
   représentant un réel calculable $x$, il y a (toujours) plusieurs
-  programmes qui la calculent (« intentions »).
+  programmes (= fonctions informatiques) qui la calculent
+  (« intentions »).  C'est par cette dernière donnée qu'on va
+  représenter le réel $x$.
 \end{itemize}
 
 \smallskip
@@ -647,13 +672,13 @@ s'écrit par exemple « \texttt{fun p -> fun q -> fun n -> (p * (pow 2
 l'exponentiation entière et ‘\texttt{/}’ la division euclidienne.
 \end{corrige}
 
-\smallskip
+\medskip
 
 \textbf{(2)} Montrer que si $x$ est un réel calculable alors $-x$ est
-calculable, et, plus précisément, écrire un programme qui, donné une
+calculable, et, plus précisément, écrire un programme qui, donnée une
 fonction qui représente $x$, en renvoie une qui représente $-x$.
-Faire de même pour $|x|$ (on rappelle à toutes fins utiles que
-$\big||u|-|v|\big| \leq |u-v|$).
+Faire de même pour $|x|$.  (On rappelle à toutes fins utiles que
+$\Big||u|-|v|\Big| \leq |u-v|$.)
 
 \begin{corrige}
 Si $k$ est un numérateur d'approximation dyadique de niveau $n$ de $x
@@ -673,7 +698,7 @@ correspondant s'écrit par exemple « \texttt{fun xf -> fun n -> abs(xf
   n)} ».
 \end{corrige}
 
-\smallskip
+\medskip
 
 \textbf{(3)} Expliquer pourquoi, si $k$ est un numérateur
 d'approximation dyadique de niveau $n+r$ de $x \in \mathbb{R}$ (avec
@@ -695,7 +720,7 @@ représentant $x$ s'écrit par exemple « \texttt{fun r -> fun xf -> fun
   n -> xf (n+r)} ».
 \end{corrige}
 
-\smallskip
+\medskip
 
 \textbf{(4)} Expliquer comment, donné $\ell \in \mathbb{Z}$, on peut
 trouver algorithmiquement un entier $k \in \mathbb{Z}$ tel que
@@ -706,10 +731,10 @@ numérateur d'approximation dyadique de niveau $n$ de $x+y$ à partir de
 numérateurs d'approximations dyadiques de niveau $n+2$ de $x$ et $y$
 respectivement.
 
-En déduire que si $x$ et $y$ sont calculables alors $x+y$
-est calculable, et, plus précisément, et, plus précisément, écrire un
-programme qui, donnés des fonctions qui représentent $x$ et $y$, en
-renvoie une qui représente $x+y$.
+En déduire que si $x$ et $y$ sont calculables alors $x+y$ est
+calculable, et, plus précisément, écrire un programme qui, données des
+fonctions qui représentent $x$ et $y$, en renvoie une qui
+représente $x+y$.
 
 \begin{corrige}
 Dire $[\frac{\ell}{4}-\frac{1}{2}\,;\,\frac{\ell}{4}+\frac{1}{2}]
@@ -745,7 +770,7 @@ s'écrit par exemple « \texttt{fun xf -> fun yf -> fun n -> ((xf (n+2)) +
   (yf (n+2)) + 2)/4} ».
 \end{corrige}
 
-\smallskip
+\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
@@ -754,7 +779,7 @@ fonction $n \mapsto k_n$ vérifie $z\leq 0$ si et seulement on a $k_n
 $z>0$, on peut calculer algorithmiquement un $n\in\mathbb{N}$ tel que
 $z \geq \frac{1}{2^n}$.
 
-De façon analogue, montrer que, donné une fonction $n \mapsto k_n$
+De façon analogue, montrer que, donnée une fonction $n \mapsto k_n$
 représentant $z$ calculable, et en supposant seulement $z\neq 0$, on
 peut décider algorithmiquement si $z<0$ ou $z>0$.
 
@@ -780,14 +805,14 @@ jusqu'à ce qu'une de ces conditions soit satisfaite, et de renvoier
 ou l'autre.
 \end{corrige}
 
-\smallskip
+\medskip
 
-\textbf{(6)} Indépendamment de toutes les questions qui précèdent,
-montrer qu'il n'existe pas de programme qui, donné le code d'un autre
-programme $e$, décide si ce dernier représente un réel (nécessairement
-calculable).  Autrement dit, la fonction qui à $e$ associe $1$ si $e$
-calcule une fonction $n \mapsto k_n$ représentant un certain réel $x$,
-et $0$ sinon, n'est pas calculable.
+\textbf{(6)} (Cette question est indépendante de toutes les questions
+qui précèdent ou qui suivent.)  Montrer qu'il n'existe pas de
+programme qui, donné le code d'un autre programme $e$, décide si ce
+dernier représente un réel calculable.  Autrement dit, la fonction qui
+à $e$ associe $1$ si $e$ calcule une fonction $n \mapsto k_n$
+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
@@ -798,7 +823,7 @@ 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}
 
-\smallskip
+\medskip
 
 \textbf{(7)} Soit $e$ un programme (vu comme l'indice d'une fonction
 générale récursive $\varphi_e$).  Soit $\eta(e)$ le réel défini de la
@@ -814,12 +839,14 @@ manière suivante :
 \]
 (Plus exactement, il faudrait plutôt écrire « $\eta(e) =
 \frac{1}{2^m}$ si $m$ est le code d'un arbre de calcul pour
-$\varphi_e(0)$ » à la première ligne.)  Expliquer comment, donnés $e$
-et $n \in \mathbb{N}$, calculer algorithmiquement un numérateur
-d'approximation dyadique de niveau $n$ de $\eta(e)$.
+$\varphi_e(0)$ » à la première ligne, mais on peut se permettre de
+confondre ces deux notions.)
 
-En déduire qu'on peut écrire un programme qui, donné $e$, renvoie une
-fonction représentant le réel $\eta(e)$ (en tant réel calculable).
+Expliquer comment, donnés $e$ et $n \in \mathbb{N}$, calculer
+algorithmiquement un numérateur d'approximation dyadique de niveau $n$
+de $\eta(e)$.  En déduire qu'on peut écrire un programme qui, donné
+$e$, renvoie une fonction représentant le réel $\eta(e)$ (en tant réel
+calculable).
 
 \begin{corrige}
 On a vu en cours qu'il est possible de tester algorithmiquement si le
@@ -835,7 +862,7 @@ exactement ; s'il ne termine pas dans le temps imparti, on renvoie le
 numérateur $0$, qui convient car $\eta(e) \leq \frac{1}{2^n}$.
 \end{corrige}
 
-\smallskip
+\medskip
 
 \textbf{(8)} Expliquer l'erreur dans la réponse suivante à la
 question (7) : « On lance le calcul de $\varphi_e(0)$ : s'il termine
@@ -859,7 +886,7 @@ approximation dyadique de niveau $n$ de $\eta(e)$, qui peut être $0$
 si le calcul de $\varphi_e(0)$ n'a pas terminé dans le temps imparti.
 \end{corrige}
 
-\smallskip
+\medskip
 
 \textbf{(9)} Déduire de la question (8) qu'il n'y a pas d'algorithme
 qui, donnée une fonction représentant un réel calculable $x$, teste si
@@ -875,17 +902,17 @@ ceci n'est pas faisable algorithmiquement.  C'est donc que
 l'algorithme évoqué n'existe pas.
 \end{corrige}
 
-\smallskip
+\medskip
 
 Pour la question suivante, on \emph{admettra} le résultat suivant
 (plus ou moins vu en TD) : il n'existe pas d'algorithme qui, donné le
 code d'un programme $e$, termine toujours en temps fini et renvoie
 « vrai » si $\varphi_e(0){\downarrow} = 0$ et « faux » si
 $\varphi_e(0){\downarrow} \neq 0$ (si $\varphi_e(0){\uparrow}$ il
-aurait le droit de répondre n'importe quoi mais avec l'obligation de
-terminer).
+aurait le droit de répondre n'importe quoi mais toujours avec
+l'obligation de terminer).
 
-\smallskip
+\medskip
 
 \textbf{(10)} En modifiant un peu la construction proposée en (7) (on
 définira $\eta'(e)$ valant $\frac{1}{2^m}$ ou $-\frac{1}{2^m}$ ou $0$
@@ -923,30 +950,35 @@ $\varphi_e(0){\uparrow}$, mais toujours avec l'obligation de
 terminer), et on a indiqué que ce n'était pas possible.
 \end{corrige}
 
-\smallskip
+\medskip
 
-Si $x$ est un réel entre $0$ et $1$ (pour simplifier), on rappelle
-qu'une \textbf{écriture binaire} de $x$ est une suite $(u_n)_{n\geq
-  1}$ à valeurs dans $\{0,1\}$ telle que $x = \sum_{n=1}^{+\infty}
-u_n\cdot 2^{-n}$.  Une telle suite existe toujours (par exemple, on
-peut prendre celle donnée $u_n = \lfloor 2^n x\rfloor - 2\lfloor
-2^{n-1} x\rfloor$ où $\lfloor \emdash \rfloor$ désigne la partie
-entière), mais elle n'est pas unique en général (par exemple
-$\frac{1}{2}$ admet les deux écritures binaires $0.100000\ldots$ et
-$0.011111\ldots$ ; en fait, ce sont exactement les dyadiques qui
-admettent plus d'une écriture binaire, et ils en admettent exactement
-deux).
+Si $x$ est un réel entre $0$ et $1$ (pour s'éviter le tracas de
+l'écriture des nombres négatifs), on rappelle qu'une \textbf{écriture
+  binaire} de $x$ est une suite $(u_n)_{n\geq 1}$ à valeurs dans
+$\{0,1\}$ telle que $x = \sum_{n=1}^{+\infty} u_n\cdot 2^{-n}$.  Une
+telle suite existe toujours (par exemple, on peut prendre celle donnée
+$u_n = \lfloor 2^n x\rfloor - 2\lfloor 2^{n-1} x\rfloor$ où $\lfloor
+\emdash \rfloor$ désigne la partie entière), mais elle n'est pas
+unique en général (par exemple $\frac{1}{2}$ admet les deux écritures
+binaires $0.100000\ldots$ et $0.011111\ldots$ ; en fait, ce sont
+exactement les dyadiques qui admettent plus d'une écriture binaire, et
+ils en admettent exactement deux).
 
 On dira qu'un réel entre $0$ et $1$ est \textbf{naïvement calculable}
-lorsqu'il admet une écriture binaire $n \mapsto u_n$ calculable.
+lorsqu'il admet une écriture binaire $n \mapsto u_n$ calculable.  On
+pourra aussi dire que cette fonction, ou un programme qui la calcule,
+le \textbf{représente naïvement}.  Le but des questions suivantes est
+de comprendre pourquoi cette notion ne se comporte pas bien (et donc
+pourquoi on ne l'a pas prise comme définition principale).
 
-\smallskip
+\medskip
 
 \textbf{(11)} Montrer qu'un réel (entre $0$ et $1$) naïvement
 calculable est calculable, et plus précisément qu'il existe un
-algorithme qui, donnée une fonction qui calcule l'écriture binaire de
-$x$, renvoie sa représentation comme réel calculable (comme définie au
-début de ce problème).
+algorithme qui, donnée une fonction $n \mapsto u_n$ qui calcule
+l'écriture binaire de $x$, en renvoie une représentation $n \mapsto
+k_n$ comme réel calculable (ainsi que définie au début de ce
+problème).
 
 \begin{corrige}
 Si $x = \sum_{i=1}^{+\infty} u_i\cdot 2^{-i}$, alors $2^n\,x =
@@ -958,12 +990,13 @@ dyadique de niveau $n$ de $x$.  Ceci fournit un algorithme calculant
 $n \mapsto k_n$ à partir de $n \mapsto u_n$.
 \end{corrige}
 
-\smallskip
+\medskip
 
-\textbf{(12)} En utilisant la question (10), 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$.
+\textbf{(12)} Dans l'autre sens, en utilisant la question (10),
+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)$.)
 
 \begin{corrige}
 Si un tel algorithme existait, on pourrait l'appliquer à $x_e =
@@ -978,7 +1011,7 @@ peut donc pas algorithmiquement calculer ce chiffre en fonction
 de $e$.
 \end{corrige}
 
-\smallskip
+\medskip
 
 \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
@@ -1007,7 +1040,7 @@ pourtant on ne peut pas en calculer pour $x_e - y_e$ comme on l'a
 expliqué à la question précédente.
 \end{corrige}
 
-\smallskip
+\medskip
 
 \textbf{(14)} Montrer que, la question (12) nonobstant, tout réel
 calculable (entre $0$ et $1$) est naïvement calculable.  (On pourra