%% 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{% \refstepcounter{comcnt}\bigskip\noindent\textbf{Exercice~\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 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. \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 (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 ?) \[ \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 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 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 ? \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, é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.) \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 \textbf{Motivations :} On s'intéresse dans cet exercice à la notion de \emph{réel calculable}, qu'on va définir comme 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). \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$ est un dyadique de tout 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 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 calculable $n \mapsto k_n$ représentant un réel calculable $x$, il y a (toujours) plusieurs programmes qui la calculent (« intentions »). \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} \smallskip \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 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} \smallskip \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} \smallskip \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, 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$. \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} \smallskip \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é 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} \smallskip \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. \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} \smallskip \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.) 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} \smallskip \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} \smallskip \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} \smallskip 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). \smallskip \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} \smallskip 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). 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. \smallskip \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). \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} \smallskip \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$. \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} \smallskip \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} \smallskip \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}