%% 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}