Merge branch 'exam-20240126'

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}