%% This is a LaTeX document. Hey, Emacs, -*- latex -*- , get it? \documentclass[12pt,a4paper]{article} \usepackage[a4paper,hmargin=2cm,vmargin=3cm]{geometry} \usepackage[french]{babel} \usepackage[utf8]{inputenc} \usepackage[T1]{fontenc} %\usepackage{ucs} \usepackage{times} % A tribute to the worthy AMS: \usepackage{amsmath} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsthm} % \usepackage{mathrsfs} \usepackage{wasysym} \usepackage{url} \usepackage{mathpartir} \usepackage{flagderiv} % \usepackage{graphics} \usepackage[usenames,dvipsnames]{xcolor} \usepackage{tikz} \usetikzlibrary{arrows} \usepackage{hyperref} % \theoremstyle{definition} \newtheorem{comcnt}{Tout} \newcommand\thingy{% \refstepcounter{comcnt}\medskip\noindent\textbf{\thecomcnt.} } \newcommand\exercice[1][Exercice]{% \refstepcounter{comcnt}\bigskip\noindent\textbf{#1~\thecomcnt.}\par\nobreak} \renewcommand{\qedsymbol}{\smiley} % \newcommand{\dbllangle}{\mathopen{\langle\!\langle}} \newcommand{\dblrangle}{\mathclose{\rangle\!\rangle}} \newcommand{\dottedlimp}{\mathbin{\dot\Rightarrow}} \newcommand{\dottedland}{\mathbin{\dot\land}} \newcommand{\dottedlor}{\mathbin{\dot\lor}} \newcommand{\dottedtop}{\mathord{\dot\top}} \newcommand{\dottedbot}{\mathord{\dot\bot}} \newcommand{\dottedneg}{\mathop{\dot\neg}} \mathchardef\emdash="07C\relax % \DeclareUnicodeCharacter{00A0}{~} % % \newcommand{\spaceout}{\hskip1emplus2emminus.5em} \newif\ifcorrige \corrigetrue \newenvironment{corrige}% {\ifcorrige\relax\else\setbox0=\vbox\bgroup\fi% \smallbreak\noindent{\underbar{\textit{Corrigé.}}\quad}} {{\hbox{}\nobreak\hfill\checkmark}% \ifcorrige\par\smallbreak\else\egroup\par\fi} % % % \begin{document} \ifcorrige \title{INF110\\Contrôle de connaissances — Corrigé\\{\normalsize Logique et Fondements de l'Informatique}} \else \title{INF110\\Contrôle de connaissances\\{\normalsize Logique et Fondements de l'Informatique}} \fi \author{} \date{26 janvier 2024} \maketitle \pretolerance=8000 \tolerance=50000 \vskip1truein\relax \noindent\textbf{Consignes.} 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 L'usage de tous les documents (notes de cours manuscrites ou imprimées, feuilles d'exercices, livres) est autorisé. L'usage des appareils électroniques est interdit. \medbreak Durée : 3h Barème \textcolor{red}{à remplir}. \ifcorrige Ce corrigé comporte \textcolor{red}{à remplir} pages (page de garde incluse). \else Cet énoncé comporte \textcolor{red}{à remplir} pages (page de garde incluse). \fi \vfill {\tiny\noindent \immediate\write18{sh ./vc > vcline.tex} Git: \input{vcline.tex} \immediate\write18{echo ' (stale)' >> vcline.tex} \par} \pagebreak % % % \exercice On considère un extrait d'une démonstration interactive en Coq du théorème \texttt{forall (A:Prop) (B:Prop) (C:Prop), (A->B)->(B->C)->(A->C)} où on a recopié ci-dessous seulement la sortie de Coq. On demande de retrouver les deux commandes qui ont été utilisées, et de proposer l'étape suivante. \smallskip {\tt\par\noindent 1 subgoal\\ \ \ \\ \ \ A, B, C : Prop\\ \ \ ============================\\ \ \ (A -> B) -> (B -> C) -> A -> C\\ \\ thm < \textrm{(commande à trouver)}\\ 1 subgoal\\ \ \ \\ \ \ A, B, C : Prop\\ \ \ x : A -> B\\ \ \ y : B -> C\\ \ \ z : A\\ \ \ ============================\\ \ \ C\\ \\ thm < \textrm{(commande à trouver)}\\ 1 subgoal\\ \ \ \\ \ \ A, B, C : Prop\\ \ \ x : A -> B\\ \ \ y : B -> C\\ \ \ z : A\\ \ \ ============================\\ \ \ B\\ \\ thm < \textrm{(commande à proposer)} } \smallskip (À défaut de connaître le nom précis de la tactique, on pourra expliquer ce qu'elle fait de façon générale, ou à quelle règle de logique elle correspond.) \begin{corrige} La première commande était \texttt{intros x y z.} et correspond à la règle d'introduction du $\Rightarrow$ appliquée trois fois. La commande suivante était \texttt{apply y.} et correspond à la règle d'élimination du $\Rightarrow$ entre l'hypothèse (\texttt{y}) qu'on lui indique et la démonstration qu'onva produire du nouveau but. Une commande naturelle ensuite serait \texttt{apply x.} (qui ramènerait le but à \texttt{A}, et qui pourrait être suivie de \texttt{exact z.} pour terminer la démonstration). \end{corrige} % % % \exercice (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 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).\, \langle (\pi_1 p),\,(\pi_2 p)h\rangle \] (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 ? \[ \lambda(p: C\land\forall x. B(x))).\, \lambda(x:I).\, \langle (\pi_1 p),\,(\pi_2 p)x\rangle \] (Ici, $C$ est une variable de relation nullaire, c'est-à-dire une 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 ? \[ \lambda(p: \exists x.(A\Rightarrow B(x))).\, \lambda(h:A).\, (\texttt{match~}p\texttt{~with~}\langle x,j\rangle \mapsto \langle x,jh\rangle) \] (Ici, $A$ est une variable de relation nullaire, c'est-à-dire une variable propositionnelle, et $B$ est une variable de relation unaire.) \begin{corrige} \textbf{(1)} Dans le contexte où $p$ a type $C\land(A\Rightarrow B)$ et $h$ a type $A$, on voit que $\pi_1 p$ a type $C$ et $\pi_2 p$ a type $A\Rightarrow B$, si bien que $(\pi_2 p)h$ a type $B$, et le couple $\langle (\pi_1 p),\,(\pi_2 p)h\rangle$ a type $C\land B$, donc l'expression dans son ensemble a type $C\land(A\Rightarrow B) \Rightarrow (A \Rightarrow C\land B)$, i.e., elle représente une 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$ 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 x. B(x)) \Rightarrow \forall x. (C\land B(x))$, i.e., elle représente une preuve de cette affirmation. \textbf{(3)} On se place dans le contexte où $p$ a type $\exists x.(A\Rightarrow B(x))$ et $h$ a type $A$. Le \texttt{match} va déstructurer $p$ en un $x$ individu et un $j$ de type $A\Rightarrow B(x)$. Alors $jh$ a type $B(x)$, et $\langle x,jh\rangle$ a type $\exists x.B(x)$. Donc l'expression dans son ensemble a type $(\exists x.(A\Rightarrow B(x))) \Rightarrow (A \Rightarrow \exists x. B(x))$, i.e., elle représente une preuve de cette affirmation. \end{corrige} % % % \exercice En appliquant l'algorithme de Hindley-Milner, trouver une annotation de type (dans le $\lambda$-calcul simplement typé) au terme suivant du $\lambda$-calcul non typé : \[ \lambda f.\,\lambda z.\,fz(\lambda g.gz) \] (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 par Curry-Howard ? \begin{corrige} Dans une première phase, on collecte les types et contraintes suivants : $f:\eta_1$, $z:\eta_2$, $fz : \eta_3$ avec $\eta_1 = (\eta_2\to\eta_3)$, $g : \eta_4$, $g z : \eta_5$ avec $\eta_4 = (\eta_2\to\eta_5)$ donc $\lambda g.gz : \eta_4\to\eta_5$ et enfin $fz(\lambda g.gz) : \eta_6$ avec $\eta_3 = ((\eta_4\to\eta_5)\to\eta_6)$ ; et le type final est $\eta_1 \to \eta_2 \to \eta_6$. On a donc les contraintes suivantes : \[ \begin{aligned} \eta_1 &= (\eta_2\to\eta_3)\\ \eta_4 &= (\eta_2\to\eta_5)\\ \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 : \[ \begin{aligned} \eta_1 &\mapsto (\eta_2\to((\eta_2\to\eta_5)\to\eta_5)\to\eta_6)\\ \eta_4 &\mapsto (\eta_2\to\eta_5)\\ \eta_3 &\mapsto (((\eta_2\to\eta_5)\to\eta_5)\to\eta_6)\\ \end{aligned} \] qu'on applique à tous les types intermédiaires et au type final, ce qui donne \[ \begin{aligned} &\lambda (f:\eta_2\to((\eta_2\to\eta_5)\to\eta_5)\to\eta_6).\,\lambda (z:\eta_2).\,fz(\lambda (g:\eta_2\to\eta_5).gz)\\ :\quad& (\eta_2\to((\eta_2\to\eta_5)\to\eta_5)\to\eta_6) \to \eta_2 \to \eta_6 \end{aligned} \] En particulier, on voit que $(H_2\Rightarrow((H_2\Rightarrow H_5)\Rightarrow H_5)\Rightarrow H_6) \Rightarrow H_2 \Rightarrow H_6$ est un théorème du calcul propositionnel intuitionniste. \end{corrige} % % % \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 : \[ \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) \] (\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 cours. \emph{Sémantique de Kripke :} On considère le cadre de Kripke suivant : \begin{center} \begin{tikzpicture}[>=stealth'] \node (t) at (0bp,0bp) {$t$}; \node (u) at (35bp,30bp) {$u$}; \node (v) at (35bp,0bp) {$v$}; \node (w) at (35bp,-30bp) {$w$}; \draw[->] (t)--(u); \draw[->] (t)--(v); \draw[->] (t)--(w); \end{tikzpicture} \end{center} Soient $p$ (resp. $q$, resp. $r$) l'affectation de vérité qui vaut $1$ en $u$ (resp. $v$, resp. $w$) et $0$ partout ailleurs. Alors chacun de $p\dottedland q$, $q\dottedland r$ et $r\dottedland p$ est identiquement $0$ donc $\dottedneg(p\dottedland q) \dottedland \dottedneg(q\dottedland r) \dottedland \dottedneg(r\dottedland p)$ est identiquement $1$. En revanche, $\dottedneg p$ vaut $1$ dans les mondes $v$ et $w$ et $0$ dans les mondes $t$ et $u$, et de façon analogue pour $\dottedneg q$ et $\dottedneg r$ avec la permutation cyclique évidente. Donc $\dottedneg p \dottedlor \dottedneg q \dottedlor \dottedneg r$ vaut $0$ dans le monde $t$ et $1$ dans les trois mondes $u,v,w$. Par conséquent, il en va de même de $(\dottedneg(p\dottedland q) \dottedland \dottedneg(q\dottedland r) \dottedland \dottedneg(r\dottedland p)) \dottedlimp (\dottedneg p \dottedlor \dottedneg q \dottedlor \dottedneg r)$. Si la formule proposée avait été démontrable, on aurait trouvé constamment $1$ (par \emph{correction} de la sémantique de Kripke) : ce n'est pas le cas, 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 $\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. \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 $\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 \dottedneg(Q\dottedland R) \dottedland \dottedneg(R\dottedland P)$. Considérons $\varphi_e(\langle 0,0,0\rangle)$ : il est bien défini (car il existe des parties $P,Q,R$ comme on l'a dit) et doit appartenir à $\dottedneg P \dottedlor \dottedneg Q \dottedlor \dottedneg R$, 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 un élément de $\dottedneg P$ : alors en considérant le cas $P = \mathbb{N}$ et $Q = \varnothing$ et $R = \varnothing$ on a une contradiction. Or si la formule proposée avait été démontrable, il existerait un $e$ qui la réalise quelles que soient les parties (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. \emph{Sémantique des problèmes finis :} Considérons trois problèmes dont l'ensemble des candidats est un singleton, appelons-les $E := (\{\bullet_p\}, P)$, $F := (\{\bullet_q\}, Q)$ et $G := (\{\bullet_r\}, R)$ où chacun des ensembles de solutions $P,Q,R$ est soit vide soit le singleton écrit juste avant. Alors l'ensemble des candidats de $\dottedneg(E\dottedland F) \dottedland \dottedneg(F\dottedland G) \dottedland \dottedneg(G\dottedland E)$ est un singleton, appelons-le $\{\bullet_0\}$, et ce singleton est solution lorsque (au moins) deux des trois parties $P,Q,R$ sont vides. L'ensemble des candidats de chacun de $\dottedneg E$, $\dottedneg F$, $\dottedneg G$ est un singleton, disons $\{\bullet_{p'}\}$, $\{\bullet_{q'}\}$, $\{\bullet_{r'}\}$ respectivement, donc celui de $\dottedneg E \dottedlor \dottedneg F \dottedlor \dottedneg G$ est $\{\bullet_{p'}, \bullet_{q'}, \bullet_{r'}\}$. Supposons qu'il 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 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. \end{corrige} % % % \exercice (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 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). 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}^*)$ 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 $\mathsf{PA}^*$ est contradictoire. Ceci peut sembler paradoxal. Qu'en pensez-vous ? \begin{corrige} \textbf{(1)} Les règles d'introduction et d'élimination de $\Rightarrow$ qui affirment que $\Gamma, P \vdash Q$ si et seulement si $\Gamma \vdash P\Rightarrow Q$ : autrement dit, on peut démontrer $P\Rightarrow Q$ si et seulement si on peut démontrer $Q$ en 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 $\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. \textbf{(3)} L'affirmation $\mathsf{Consis}(\mathsf{PA}^*)$ dit qu'on ne peut pas arriver à une contradiction à partir des axiomes de Peano auxquels on a ajouté l'axiome $\neg\mathsf{Consis}(\mathsf{PA})$ ; en particulier, on ne peut pas arriver à une contradiction à partir des axiomes de Peano seuls, c'est-à-dire $\mathsf{Consis}(\mathsf{PA})$. On a donc $\mathsf{Consis}(\mathsf{PA}^*) \Rightarrow \mathsf{Consis}(\mathsf{PA})$ (ce fait étant démontré à partir 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}^*$. \textbf{(4)} La théorie $\mathsf{PA}^*$ \emph{« pense »} (ou plus exactement, postule) que l'arithmétique de Peano est contradictoire, et en particulier (question (3)) qu'elle-même est contradictoire. Mais elle se trompe : ni $\mathsf{PA}$ ni $\mathsf{PA}^*$ elle-même ne sont contradictoires. Ce n'est pas absurde : c'est juste que $\mathsf{PA}^*$ a un axiome faux, mais le phénomène d'incomplétude énoncé par le théorème de Gödel empêche de voir que cet axiome est faux, donc d'aboutir effectivement à une contradiction. \end{corrige} % % % \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 : 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 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 On fait donc les définitions suivantes : \begin{itemize} \item Un \textbf{dyadique} est un rationnel de la forme $\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 qu'on ne demande pas que $\frac{k}{2^n}$ soit irréductible, par 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 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} \smallskip À titre d'exemple, l'entier $42$ est un réel calculable puisque la fonction $n \mapsto 42\times 2^n$ est évidemment calculable. \smallskip On prendra garde aux faits suivants : \begin{itemize} \item Un même réel $x$ a plusieurs approximations dyadiques de niveau $n$ (il en a même toujours $2$ ou $3$, puisque leurs numérateurs sont les entiers contenus dans l'intervalle $[2^n\, 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 mathématique $n \mapsto k_n$ représentant un réel calculable $x$, il y a (toujours) plusieurs 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 On ne demande pas de justifier le fait évident qu'un programme informatique peut manipuler des données dans $\mathbb{Z}$ (entiers relatifs arbitraires), notamment faire de l'arithmétique basique dessus (sommes, différences, produits, exponentiation, division euclidienne, etc.). Lorsqu'il est demandé d'écrire un programme, on l'écrira dans un langage de programmation raisonnable quelconque (capable de manipuler des entiers arbitrairement grands), ou sous forme de pseudocode. Par exemple, s'il est demandé d'écrire un programme représentant l'entier $42$ on pourra écrire « \texttt{lambda n: 42 * 2**n} » ou « \texttt{fun n -> 42 * (pow 2 n)} » ou n'importe quoi d'aisément compréhensible de la sorte, mais en précisant ce qui n'est pas évident (par exemple que « \texttt{pow} » est une fonction calculant l'exponentiation entière). On pourra aussi librement décider si ce langage manipule des fonctions calculables sous forme de codes de Gödel de programmes les calculant, ou sous forme de fonctions informatiques (langage fonctionnel), ou même mélanger les deux au besoin (à condition de le préciser). \smallskip \centerline{*} \smallskip \textbf{(1)} Expliquer pourquoi, donnés $p\in\mathbb{Z}$ et $q\in\mathbb{N}\setminus\{0\}$ et $n\in\mathbb{N}$, on peut calculer algorithmiquement un numérateur d'approximation dyadique de niveau $n$ de $\frac{p}{q}$. En déduire que tout rationnel est un réel calculable, et, plus précisément, écrire un programme qui, donnés $p$ et $q$, renvoie une fonction représentant le rationnel $\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. \end{corrige} \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é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|$.) \begin{corrige} Si $k$ est un numérateur d'approximation dyadique de niveau $n$ de $x \in \mathbb{R}$, c'est-à-dire $|k - 2^n\,x| \leq 1$, alors $|(-k) - 2^n\,(-x)| \leq 1$ (car $|-z| = |z|$). Ceci montre que si $n \mapsto k_n$ représente $x$ alors $n \mapsto -k_n$ représente $-x$, et elle est certainement calculable si la première l'est. Un programme calculant une fonction représentant $-x$ à partir d'une fonction 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 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 n)} ». \end{corrige} \medskip \textbf{(3)} Expliquer pourquoi, si $k$ est un numérateur d'approximation dyadique de niveau $n+r$ de $x \in \mathbb{R}$ (avec $n,r\in\mathbb{N}$), alors $k$ est aussi un numérateur d'approximation dyadique de niveau $n$ de $2^r x$. En déduire que si $x$ est un réel calculable et $r\in\mathbb{N}$ alors $2^r x$ est calculable, et, plus précisément, écrire un programme qui, donnés $r$ et une fonction qui représente $x$, renvoie une fonction qui représente $2^r x$. \begin{corrige} Dire que $k$ est un numérateur d'approximation dyadique de niveau $n+r$ de $x$ signifie par définition $|k - 2^{n+r}\,x| \leq 1$. C'est exactement dire que $|k - 2^n\,(2^r\,x)| \leq 1$, c'est-à-dire que $k$ est aussi un numérateur d'approximation dyadique de niveau $n$ de $2^r x$. On en déduit que si $n \mapsto k_n$ représente $x$ alors $n \mapsto k_{n+r}$ représente $2^r x$. Un programme calculant une fonction représentant $2^r x$ à partir de $r$ et d'une fonction représentant $x$ s'écrit par exemple « \texttt{fun r -> fun xf -> fun n -> xf (n+r)} ». \end{corrige} \medskip \textbf{(4)} Expliquer comment, donné $\ell \in \mathbb{Z}$, on peut trouver algorithmiquement un entier $k \in \mathbb{Z}$ tel que $[\frac{\ell}{4}-\frac{1}{2}\,;\,\frac{\ell}{4}+\frac{1}{2}] \subseteq[k-1\,;\,k+1]$ (on pourra faire un dessin de ces intervalles). En tirer une façon de trouver algorithmiquement un 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, é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}] \subseteq[k-1\,;\,k+1]$ équivaut à $[\ell-2\,;\,\ell+2] \subseteq[4k-4\,;\,4k+4]$, c'est-à-dire $4k-4 \leq \ell-2$ et $\ell+2 \leq 4k+4$, soit encore $\ell-2 \leq 4k \leq \ell+2$, autrement dit, 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$. Si $i,j$ désignent des numérateurs d'approximations dyadiques de niveau $n+2$ de $x$ et $y$ respectivement, c'est-à-dire $|i - 2^{n+2}\,x| \leq 1$ et $|j - 2^{n+2}\,y| \leq 1$, on a alors $|(i+j) - 2^{n+2}\,(x+y)| \leq 2$ par inégalité triangulaire, c'est-à-dire, en posant $\ell := i+j$, que $|\frac{\ell}{4} - 2^n\,(x+y)| \leq \frac{1}{2}$. Or on vient de voir comment en tirer algorithmiquement un $k$ tel que $[\frac{\ell}{4}-\frac{1}{2}\,;\,\frac{\ell}{4}+\frac{1}{2}] \subseteq[k-1\,;\,k+1]$, c'est-à-dire exactement que $|\frac{\ell}{4} - 2^n\,(x+y)| \leq \frac{1}{2}$ implique $|k - 2^n\,(x+y)| \leq 1$, c'est-à-dire que $k$ est un numérateur d'approximation dyadique de niveau $n$ de $x+y$. 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} ». \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 \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 $z \geq \frac{1}{2^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$. \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$. 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. 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. \end{corrige} \medskip \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 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. \end{corrige} \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 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)}\\ \vphantom{\displaystyle\frac{0}{0}}0&\text{~si $\varphi_e(0){\uparrow}$}\\ \end{array} \right. \] (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, mais on peut se permettre de confondre ces deux notions.) 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 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 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 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 numérateur $0$, qui convient car $\eta(e) \leq \frac{1}{2^n}$. \end{corrige} \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 en (exactement) $m$ étapes, on renvoie (une fonction représentant) $\frac{1}{2^m}$, qui est calculable d'après la question (1), sinon on renvoie la fonction constamment nulle. » On expliquera aussi en quoi on n'a pas commis cette erreur en répondant à ladite question. \begin{corrige} L'erreur est dans le mot « sinon » : si on lance le calcul de $\varphi_e(0)$, on ne peut pas savoir à l'avance s'il va terminer : on peut certes renvoyer $\frac{1}{2^m}$ s'il termine en exactement $m$ étapes, mais si on fait ça il n'y a pas de « sinon » possible, car on est parti dans une boule infinie. Et il n'y a pas de moyen de savoir \textit{a priori} si la boucle terminera, car le problème de l'arrêt est indécidable (même pour $\varphi_e(0)$). On n'a pas commis cette erreur, car on a pris \emph{d'abord} $n$, qui agit comme borne sur le nombre d'étapes d'exécution : on renvoie une 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} \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 $x\neq 0$ ou $x=0$ (i.e., renvoie « vrai » si $x\neq 0$ et « faux » si $x=0$). \begin{corrige} Si un tel algorithme existait, appliqué à $\eta(e)$ (ou plus exactement, à une fonction représentant $\eta(e)$, dont on a vu à la question (8) qu'elle se déduit algorithmiquement de $e$), il permettrait de tester si $\varphi_e(0){\downarrow}$. Or on a vu que ceci n'est pas faisable algorithmiquement. C'est donc que l'algorithme évoqué n'existe pas. \end{corrige} \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 toujours avec l'obligation de terminer). \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$ selon des cas judicieusement choisis), montrer qu'il n'est même pas 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$). \begin{corrige} 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$}\\ \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. \end{corrige} \medskip 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. 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). \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 $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 = \sum_{i=1}^{+\infty} u_i\cdot 2^{n-i}$ donc en appelant $k_n = \sum_{i=1}^{n} u_i\cdot 2^{n-i}$ (il s'agit d'un entier), on voit que $2^n\,x - k_n = \sum_{i=1}^{+\infty} u_{n+i}\cdot 2^{-i}$ est compris entre $0$ et $1$, et notamment $k_n$ est un numérateur d'approximation dyadique de niveau $n$ de $x$. Ceci fournit un algorithme calculant $n \mapsto k_n$ à partir de $n \mapsto u_n$. \end{corrige} \medskip \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 = \frac{1}{2}(\eta'(e)+1)$, où $\eta'(e)$ est le réel calculable en fonction de $e$ défini à la question (10) dont on ne peut pas algorithmiquement en fonction de $e$ décider s'il est $\leq 0$ ou $\geq 0$. Or le premier chiffre de l'écriture binaire de $x_e$ va être $0$ ou $1$ selon que $x_e \leq \frac{1}{2}$ ou $x_e \geq \frac{1}{2}$ (avec les deux possibilités si $x_e = \frac{1}{2}$), c'est-à-dire selon que $\eta'(e)\leq 0$ ou $\eta'(e)\geq 0$ : on ne peut donc pas algorithmiquement calculer ce chiffre en fonction de $e$. \end{corrige} \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 $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. \begin{corrige} Considérons $\eta'(e)$ le réel calculable en fonction de $e$ défini à la question (10). On peut l'écrire sous la forme $\eta'_+(e) - \eta'_-(e)$ avec $\eta'_+(e) = \frac{1}{2}(\eta'(e) + |\eta'(e)|)$ et $\eta'_-(e) = \frac{1}{2}(-\eta'(e) + |\eta'(e)|)$, tous deux positifs et tous deux valant soit $0$ soit $\frac{1}{2^m}$ pour un certain $m$. Les questions (2) et (4) montrent qu'on peut calculer $\eta'_+(e)$ et $\eta'_-(e)$, au sens des réels calculables, en fonction de $e$. De plus, sachant que chacun vaut soit $0$ soit $\frac{1}{2^m}$ pour un certain $m$ (ou bien en regardant directement la construction de $\eta'(e)$), il est aussi facile d'en produire une écriture binaire : pour calculer le $n$-ième chiffre de son écriture binaire, si tous les précédents étaient $0$, on demande une approximation dyadique de niveau $n+2$ et on renvoie $0$ si elle est dans $\{-1,0,1\}$, sinon on renvoie $1$ et ensuite uniquement des $0$. Les réels $x_e = \frac{1}{2}(\eta'_+(e) + 1)$ et $y_e = \frac{1}{2}\eta'_-(e)$ sont donc tels qu'on peut calculer une écriture binaire en fonction de $e$, pourtant on ne peut pas en calculer pour $x_e - y_e$ comme on l'a expliqué à la question précédente. \end{corrige} \medskip \textbf{(14)} Montrer que, la question (12) nonobstant, tout réel calculable (entre $0$ et $1$) est naïvement calculable. (On pourra distinguer deux cas : soit le réel est dyadique, soit il ne l'est pas.) On expliquera pourquoi ce n'est pas une contradiction qu'on ait montré que les réels calculables et naïvement calculables coïncident, mais qu'on peut algorithmiquement soustraire les réels calculables mais pas les réels naïvement calculables. \begin{corrige} Tout réel dyadique est évidemment calculable. Il reste à montrer que si $x$ est un réel entre $0$ et $1$ calculable et qui n'est pas dyadique, alors il est naïvement calculable. Pour cela, on applique l'algorithme suivant : pour calculer le $n$-ième chiffre $u_n$ de l'écriture binaire de $x$, on calcule une fonction représentant $2^n x - 1$, lequel est $\neq 0$ d'après l'hypothèse que $x$ n'est pas dyadique, donc d'après la question (5) on peut décider s'il est $<0$ ou $>0$, et $u_n$ vaut $0$ ou $1$ dans ces deux cas respectifs. Tout ceci est calculable. Les réels calculables et naïvement calculables sont donc les mêmes en tant qu'ensembles, mais leur représentation informatiques diffèrent : on peut passer algorithmiquement de la représentation naïve par l'écriture binaire à la représentation par approximations, mais en général pas dans l'autre sens (la difficulté étant que tant qu'on est très proche d'un dyadique on ne sait jamais si on doit émettre le chiffre $0$ ou $1$ dans l'écriture binaire). \end{corrige} % % % \end{document}