diff options
Diffstat (limited to 'controle-20240126.tex')
| -rw-r--r-- | controle-20240126.tex | 1229 |
1 files changed, 1229 insertions, 0 deletions
diff --git a/controle-20240126.tex b/controle-20240126.tex new file mode 100644 index 0000000..fa0ed60 --- /dev/null +++ b/controle-20240126.tex @@ -0,0 +1,1229 @@ +%% 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 elles (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 écrits (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 \emph{approximatif} et \emph{indicatif} (sur $20$) : entre $2$ +et $3$ points par exercice et environ $0.75$ points par question du +problème. + +\ifcorrige +Ce corrigé comporte 13 pages (page de garde incluse). +\else +Cet énoncé comporte 7 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 + +Donner une démonstration en calcul propositionnel intuitionniste de la +formule suivante : +\[ +A \Rightarrow (A\Rightarrow B) \Rightarrow B +\] +On donnera la démonstration sous la forme qu'on préfère (arbre de +preuve ou style drapeau), puis on donnera aussi un $\lambda$-terme de +preuve. On décrira ensuite brièvement ce que fait ce terme vu en tant +que programme (i.e., le comportement du programme associé à la preuve +par la correspondance de Curry-Howard). + +\begin{corrige} +Voici une preuve complète écrite dans le style « drapeau » : +\bgroup\normalsize +\begin{footnotesize} +\begin{flagderiv}[exercice-2-proof] +\assume{hypa}{A}{} +\assume{hypaib}{A\Rightarrow B}{} +\step{concb}{B}{$\Rightarrow$Élim sur \ref{hypaib} et \ref{hypa}} +\conclude{subconc}{(A\Rightarrow B) \Rightarrow B}{$\Rightarrow$Int de \ref{hypaib} dans \ref{concb}} +\conclude{mainconc}{A\Rightarrow (A\Rightarrow B) \Rightarrow B}{$\Rightarrow$Int de \ref{hypaib} dans \ref{subconc}} +\end{flagderiv} +\end{footnotesize} +\egroup + +La voici écrite sous forme d'arbre de preuve : +\begin{footnotesize} +\[ +\inferrule*[left={$\Rightarrow$Int}]{ +\inferrule*[Left={$\Rightarrow$Int}]{ +\inferrule*[Left={$\Rightarrow$Élim}]{ +\inferrule*[Left={Ax}]{ }{A,\; A\Rightarrow B \vdash A\Rightarrow B}\\ +\inferrule*[Right={Ax}]{ }{A,\; A\Rightarrow B \vdash A} +}{A, A\Rightarrow B \vdash B} +}{A \vdash (A\Rightarrow B) \Rightarrow B} +}{\vdash A\Rightarrow (A\Rightarrow B) \Rightarrow B} +\] +\end{footnotesize} +ou, si on veut donner des noms aux hypothèses et marquer tous les +termes de preuve intermédiaires : +\begin{footnotesize} +\[ +\inferrule*[left={$\Rightarrow$Int}]{ +\inferrule*[Left={$\Rightarrow$Int}]{ +\inferrule*[Left={$\Rightarrow$Élim}]{ +\inferrule*[Left={Ax}]{ }{x:A,\; k:A\Rightarrow B\; \vdash\; k:A\Rightarrow B}\\ +\inferrule*[Right={Ax}]{ }{x:A,\; k:A\Rightarrow B\; \vdash\; x:A} +}{x:A,\; k:A\Rightarrow B\; \vdash\; kx:B} +}{x:A \; \vdash \; \lambda(k:A\Rightarrow B).\,kx\; :\; (A\Rightarrow B) \Rightarrow B} +}{\vdash\; \lambda(x:A).\, \lambda(k:A\Rightarrow B).\,kx\; :\; A\Rightarrow (A\Rightarrow B) \Rightarrow B} +\] +\end{footnotesize} +Le $\lambda$-terme est donc $\lambda(x:A).\, \lambda(k:A\Rightarrow +B).\, k x$, et le programme transforme $x$ en la fonction qui applique +une fonction $k$ à $x$, ou, ce qui revient au même, il prend +successivement $x$ et $k$ et applique $k$ à $x$. +\end{corrige} + + +% +% +% + +\exercice + +(Dans cet exercice, on ne demande pas de justifier les réponses.) + +\textbf{(1)} En calcul propositionnel intuitionniste, quel est +l'énoncé prouvé 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 intuitionniste, quel est +l'énoncé prouvé 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 intuitionniste, quel est +l'énoncé prouvé 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 z. B(z)$ et $x$ est un individu. Alors $\pi_1 p$ a type $C$ +et $\pi_2 p$ a type $\forall z. B(z)$, si bien que $(\pi_2 p)x$ a type +$B(x)$, et $\langle (\pi_1 p),\,(\pi_2 p)x\rangle$ a type $C\land +B(x)$, donc l'expression dans son ensemble a type $(C\land \forall +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 ? + +(Une réponse qui ne suit pas l'algorithme de Hindley-Milner mais qui +est néanmoins correcte vaudra une partie des points.) + +\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)$ : +$\eta_1$ est une variable de type, et elle n'apparaît pas dans l'autre +membre de la contrainte ; il n'y a rien à faire à part enregistrer +$\eta_1 \mapsto (\eta_2\to\eta_3)$ dans la substitution. On examine +ensuite la contrainte $\eta_4 = (\eta_2\to\eta_5)$ : on enregistre +$\eta_4 \mapsto (\eta_2\to\eta_5)$ dans la substitution, et on +l'applique à la dernière contrainte, qui devient $\eta_3 = +(((\eta_2\to\eta_5)\to\eta_5)\to\eta_6)$. Enfin, on examine la +contrainte $\eta_3 = (((\eta_2\to\eta_5)\to\eta_5)\to\eta_6)$ : on +enregistre $\eta_3 \mapsto (((\eta_2\to\eta_5)\to\eta_5)\to\eta_6)$ +dans la substitution et on l'applique à $\eta_1 \mapsto +(\eta_2\to\eta_3)$, qui devient $\eta_1 \mapsto +(\eta_2\to((\eta_2\to\eta_5)\to\eta_5)\to\eta_6)$. Finalement, on a +trouvé la substitution : +\[ +\begin{aligned} +\eta_1 &\mapsto (\eta_2\to((\eta_2\to\eta_5)\to\eta_5)\to\eta_6)\\ +\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 des sémantiques vues en cours pour le +calcul propositionnel intuitionniste (au choix : toutes marcheront), +montrer que la formule suivante n'est pas démontrable en calcul +propositionnel intuitionniste : +\[ +\big(\neg(A\land B) \land \neg(B\land C) \land \neg(C\land A)\big) +\;\Rightarrow\; \big(\neg A \lor \neg B \lor \neg C\big) +\] + +(\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 déterminer une +partie vide parmi trois, sans avoir accès à ces parties, même si on a +la promesse qu'au moins deux d'entre elles sont vides : pour la +réalisabilité, on pourra considérer une des parties valant +$\mathbb{N}$ et les deux autres valant $\varnothing$ et constater +qu'on ne peut pas réaliser les trois affectations à la fois, tandis +que pour la sémantique des problèmes finis, on pourra considérer 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 deux par deux : +par exemple, soit $U$ le secteur formé des nombres complexes non nuls +dont l'argument (choisi entre $0$ et $2\pi$) est strictement compris +entre $0$ et $\frac{2\pi}{3}$, soit $V$ celui dont l'argument est +strictement compris entre $\frac{2\pi}{3}$ et $\frac{4\pi}{3}$ et soit +$W$ celui dont l'argument est strictement compris entre +$\frac{4\pi}{3}$ et $2\pi$. Avec ces choix, les trois secteurs sont +deux à deux disjoints, donc chacun de $U\dottedland V$, $V\dottedland +W$ et $W\dottedland U$ est vide donc $\dottedneg(U\dottedland V) +\dottedland \dottedneg(V\dottedland W) \dottedland +\dottedneg(W\dottedland U)$ est plein. En revanche, $\dottedneg U$, +$\dottedneg V$ et $\dottedneg W$ sont des secteurs ouverts ayant +l'origine pour sommet et d'angle $\frac{4\pi}{3}$ (par exemple, +$\dottedneg U$ est l'intérieur de l'adhérence de $V\cup W$, et +symétriquement pour les autres), donc aucun ne contient l'origine, +donc $\dottedneg U \dottedlor \dottedneg V \dottedlor \dottedneg W$ +non plus : c'est même précisément le complémentaire de l'origine. Par +conséquent, $(\dottedneg(U\dottedland V) \dottedland +\dottedneg(V\dottedland W) \dottedland \dottedneg(W\dottedland U)) +\dottedlimp (\dottedneg U \dottedlor \dottedneg V \dottedlor +\dottedneg W)$ est aussi le complémentaire de l'origine. Si la +formule proposée avait été démontrable, on aurait trouvé tout +$\mathbb{R}^2$ (par \emph{correction} de la sémantique des ouverts) : +ce n'est pas le cas, donc la formule n'est pas démontrable. + +\begin{center} +\lineskip=1explus5ex +\begin{tabular}{c} +\begin{tikzpicture} +\begin{scope} +\clip (-1.5,-1.5) -- (1.5,-1.5) -- (1.5,1.5) -- (-1.5,1.5) -- cycle; +\fill[gray] (1.5,1.5) -- (1.5,0) -- (0,0) -- (-0.866,1.5) -- cycle; +\end{scope} +\draw[->] (-1.55,0)--(1.55,0) node[right]{$x$}; +\draw[->] (0,-1.55)--(0,1.55) node[above]{$y$}; +\end{tikzpicture} +\\ $U$ +\end{tabular} +\penalty0 +\begin{tabular}{c} +\begin{tikzpicture} +\begin{scope} +\clip (-1.5,-1.5) -- (1.5,-1.5) -- (1.5,1.5) -- (-1.5,1.5) -- cycle; +\fill[gray] (-1.5,1.5) -- (-0.866,1.5) -- (0,0) -- (-0.866,-1.5) -- (-1.5,-1.5) -- cycle; +\end{scope} +\draw[->] (-1.55,0)--(1.55,0) node[right]{$x$}; +\draw[->] (0,-1.55)--(0,1.55) node[above]{$y$}; +\end{tikzpicture} +\\ $V$ +\end{tabular} +\penalty0 +\begin{tabular}{c} +\begin{tikzpicture} +\begin{scope} +\clip (-1.5,-1.5) -- (1.5,-1.5) -- (1.5,1.5) -- (-1.5,1.5) -- cycle; +\fill[gray] (1.5,-1.5) -- (-0.866,-1.5) -- (0,0) -- (1.5,0) -- cycle; +\end{scope} +\draw[->] (-1.55,0)--(1.55,0) node[right]{$x$}; +\draw[->] (0,-1.55)--(0,1.55) node[above]{$y$}; +\end{tikzpicture} +\\ $W$ +\end{tabular} +\penalty-1000 +\begin{tabular}{c} +\begin{tikzpicture} +\begin{scope} +\clip (-1.5,-1.5) -- (1.5,-1.5) -- (1.5,1.5) -- (-1.5,1.5) -- cycle; +\fill[gray] (-1.5,1.5) -- (-0.866,1.5) -- (0,0) -- (1.5,0) -- (1.5,-1.5) -- (-1.5,-1.5) -- cycle; +\end{scope} +\draw[->] (-1.55,0)--(1.55,0) node[right]{$x$}; +\draw[->] (0,-1.55)--(0,1.55) node[above]{$y$}; +\end{tikzpicture} +\\ $\dottedneg U$ +\end{tabular} +\penalty0 +\begin{tabular}{c} +\begin{tikzpicture} +\begin{scope} +\clip (-1.5,-1.5) -- (1.5,-1.5) -- (1.5,1.5) -- (-1.5,1.5) -- cycle; +\fill[gray] (1.5,-1.5) -- (-0.866,-1.5) -- (0,0) -- (-0.866,1.5) -- (1.5,1.5) -- cycle; +\end{scope} +\draw[->] (-1.55,0)--(1.55,0) node[right]{$x$}; +\draw[->] (0,-1.55)--(0,1.55) node[above]{$y$}; +\end{tikzpicture} +\\ $\dottedneg V$ +\end{tabular} +\penalty0 +\begin{tabular}{c} +\begin{tikzpicture} +\begin{scope} +\clip (-1.5,-1.5) -- (1.5,-1.5) -- (1.5,1.5) -- (-1.5,1.5) -- cycle; +\fill[gray] (1.5,1.5) -- (1.5,0) -- (0,0) -- (-0.866,-1.5) -- (-1.5,-1.5) -- (-1.5,1.5) -- cycle; +\end{scope} +\draw[->] (-1.55,0)--(1.55,0) node[right]{$x$}; +\draw[->] (0,-1.55)--(0,1.55) node[above]{$y$}; +\end{tikzpicture} +\\ $\dottedneg W$ +\end{tabular} +\end{center} + +\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 si (au +moins) deux des trois parties $P,Q,R$ sont vides, alors +$\dottedneg(P\dottedland Q)$, $\dottedneg(Q\dottedland R)$ et +$\dottedneg(R\dottedland P)$ sont égales à $\mathbb{N}$, donc $\langle +0,0,0\rangle$ est dans $\dottedneg(P\dottedland Q) \dottedland +\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 +$\{\bullet_0\} \to \{\bullet_{p'}, \bullet_{q'}, \bullet_{r'}\}$ +censée envoyer $\bullet_0$, s'il est solution, sur une solution du +problème $\dottedneg E \dottedlor \dottedneg F \dottedlor \dottedneg +G$, c'est-à-dire qu'il doit indiquer une partie vide parmi $P,Q,R$. +Mais ce n'est pas possible sans aucune information sur les parties ! +Pour être tout à fait précis, supposons (sans perte de généralité, +puisque le problème est symétrique) que $f(\bullet_0) = +\bullet_{p'}$ : alors en considérant le cas $P = \{\bullet_p\}$ et $Q += \varnothing$ et $R = \varnothing$ on a une contradiction. Or si la +formule proposée avait été démontrable, il existerait un $f$ qui soit +solution quels que soient $P,Q,R$ (par \emph{correction} de la +sémantique des la réalisabilité) : on vient de voir que ce n'est pas +le cas, donc la formule n'est pas démontrable. +\end{corrige} + + + +% +% +% + +\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 +$\mathsf{ZFC}$ où on travaille), $\mathsf{Consis}(\mathsf{PA})$ n'est +pas démontrable dans $\mathsf{PA}$ ; comme on est en logique classique +(arithmétique de Peano !), c'est pareil que de dire que +$\neg\neg\mathsf{Consis}(\mathsf{PA})$, ou, si on préfère, +$(\neg\mathsf{Consis}(\mathsf{PA}))\Rightarrow\bot$ n'est pas +démontrable dans $\mathsf{PA}$. D'après la question précédente, cela +signifie exactement que $\bot$ n'est pas démontrable dans $\mathsf{PA} +\cup \{\neg\mathsf{Consis}(\mathsf{PA})\} =: \mathsf{PA}^*$. +Autrement dit, on a $\mathsf{Consis}(\mathsf{PA}^*)$ : la théorie +$\mathsf{PA}^*$ ne démontre pas de contradiction. + +\textbf{(3)} L'affirmation $\mathsf{Consis}(\mathsf{PA}^*)$ dit qu'on +ne peut pas arriver à une contradiction à partir des axiomes de Peano +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, et comme on vient d'expliquer que +$\mathsf{Consis}(\mathsf{PA}^*) \Rightarrow +\mathsf{Consis}(\mathsf{PA})$ (se démontre dans $\mathsf{PA}$), on en +déduit que $\neg\mathsf{Consis}(\mathsf{PA}^*)$ se démontre dans +$\mathsf{PA}^*$. + +\textbf{(4)} La théorie $\mathsf{PA}^*$ \emph{« pense »} (ou plus +exactement, postule) que l'arithmétique de Peano est contradictoire, +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 introduit 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 le quotient de la division euclidienne de $2^n\, p$ par $q$, et +il s'agit d'un numérateur d'approximation dyadique de niveau $n$ +de $\frac{p}{q}$ puisque $|\lfloor z\rfloor - z| \leq 1$. Donc, la +fonction qui à $p$ et $q$ associe le code d'une fonction calculant $n +\mapsto \lfloor 2^n\, \frac{p}{q}\rfloor$ est calculable (par le +théorème s-m-n si on veut être très précis). Un tel programme s'écrit +par exemple « \texttt{fun p -> fun q -> fun n -> (p * (pow 2 n)) / + q} » en supposant que « \texttt{pow} » représente l'exponentiation +entière et ‘\texttt{/}’ la division euclidienne. +\end{corrige} + +\medskip + +\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 $\Big||k| - 2^n\,|x|\Big| \leq 1$ (d'après +l'inégalité qui a été rappelée). Ceci montre que si $n \mapsto k_n$ +représente $x$ alors $n \mapsto |k_n|$ représente $|x|$ : un programme +correspondant s'écrit par exemple « \texttt{fun xf -> fun n -> abs(xf + 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$ le quotient de la division euclidienne +de $\ell+2$ par $4$, car on aura alors $4k+r = \ell+2$ avec reste +$0\leq r<4$, donc $\ell-2 < 4k \leq \ell+2$. + +Si $i,j$ désignent des numérateurs d'approximations dyadiques de +niveau $n+2$ de $x$ et $y$ respectivement, c'est-à-dire $|i - +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} » (toujours en notant ‘\texttt{/}’ la division +euclidienne). +\end{corrige} + +\medskip + +\textbf{(5)} Montrer qu'un réel calculable $z$, représenté par une +fonction $n \mapsto k_n$, vérifie $z\leq 0$ si et seulement on a $k_n +\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 z \geq \frac{k_n-1}{2^n}$ donc $k_n \leq 1$ +pour tout $n$. + +On en déduit que si on \emph{suppose} $z>0$, il existe un indice $n$ +tel que $k_n \geq 2$ dans toute fonction $n \mapsto k_n$ +représentant $z$ ; et pour un tel $n$ on a alors $z \geq +\frac{k_n-1}{2^n} \geq \frac{1}{2^n}$ comme recherché. Pour trouver +ce $n$, il suffit d'effectuer une boucle infinie calculant $k_n$ en +s'arrêtant dès que $k_n \geq 2$ : d'après ce qui vient d'être dit, +l'hypothèse $z>0$ garantit la terminaison de la boucle. + +Si maintenant on suppose simplement $z\neq 0$, il existe soit un +indice $n$ tel que $k_n \geq 2$ soit un indice tel que $k_n \leq -2$ +(par symétrie) : pour décider le signe de $z$, il suffit d'effectuer +une boucle infinie jusqu'à ce qu'une de ces conditions soit +satisfaite, et de renvoier « positif » ou « négatif » selon qu'on a +trouvé un $n$ vérifiant l'un ou l'autre. +\end{corrige} + +\medskip + +\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 : le sous-ensemble des +fonctions partielles $\mathbb{N} \dasharrow \mathbb{Z}$ qui sont une +fonction totale représentant un réel n'est ni vide ni plein (il n'est +pas vide car la fonction constante $0$ est dedans, et pas plein parce +que la fonction définie nulle part n'est pas dedans), donc le théorème +de Rice affirme que l'ensemble des $e$ tels que $\varphi_e$ soit dans +cet ensemble n'est pas décidable. +\end{corrige} + +\medskip + +\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 exactement $m$ étapes}\\ +\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 +$m$ est un arbre de calcul pour $\varphi_e(0)$). Pour calculer un +numérateur d'approximation dyadique de niveau $n$ de $\eta(e)$, on va +faire ce test : on lance l'exécution de $\varphi_e(0)$ sur $n$ +étapes : si le calcul termine au bout de en $m\leq n$ étapes (ou, si +on préfère, si on trouve un arbre de calcul $m\leq n$), on renvoie +l'approximant $\frac{1}{2^m}$, c'est-à-dire qu'on renvoie le +numérateur $2^{n-m}$, qui convient car $\eta(e) = \frac{1}{2^m}$ +exactement ; s'il ne termine pas dans le temps imparti, on renvoie le +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 +acceptables 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 exactement $m$ étapes et que $\varphi_e(0) = 0$}\\ +\displaystyle-\frac{1}{2^m}&\text{~si le calcul de $\varphi_e(0)$ termine en exactement $m$ étapes et que $\varphi_e(0) \neq 0$}\\ +\vphantom{\displaystyle\frac{0}{0}}0&\text{~si $\varphi_e(0){\uparrow}$}\\ +\end{array} +\right. +\] + +Un argument analogue à celi de la la question (7) montre que +$\eta'(e)$ est calculable à partir de $e$. Précisément : donné un +niveau $n$, il suffit de lancer l'exécution de $\varphi_e(0)$ sur $n$ +étapes et, si elle termine en $m\leq n$ étapes, renvoyer l'approximant +$\frac{1}{2^m}$ ou $-\frac{1}{2^m}$ (c'est-à-dire le numérateur +$2^{n-m}$ ou $-2^{n-m}$) selon que le résultat qu'on a calculé est $0$ +ou $\neq 0$, et sinon $0$. Comme en (9), décider si $\eta'(e)\leq 0$ +ou $\eta'(e)\geq 0$ (en acceptant n'importe quelle réponse si +c'est $0$) reviendrait à décider si $\varphi_e(0){\downarrow} = 0$ ou +$\varphi_e(0){\downarrow} \neq 0$ (en acceptant n'importe quelle +réponse si $\varphi_e(0){\uparrow}$, mais toujours avec l'obligation +de terminer), et on a indiqué que ce n'était pas possible. +\end{corrige} + +\medskip + +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$. (\emph{Indication :} 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, disons, $x$ entre $\frac{1}{2}$ et $1$ et $y$ entre $0$ +et $\frac{1}{2}$) sous forme d'une fonction calculant une écriture +binaire, renvoie $x-y$ sous cette même forme. + +\begin{corrige} +Considérons $\eta'(e)$ le réel calculable en fonction de $e$ défini à +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} |