path: root/controle-20260126.tex

%% 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{lmodern}
\usepackage{newtxtext}
% 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 / CSC-3TC34-TP\\Contrôle de connaissances — Corrigé\\{\normalsize Logique et Fondements de l'Informatique}}
\else
\title{INF110 / CSC-3TC34-TP\\Contrôle de connaissances\\{\normalsize Logique et Fondements de l'Informatique}}
\fi
\author{}
\date{26 janvier 2026}
\maketitle

\pretolerance=8000
\tolerance=50000

\vskip1truein\relax

\noindent\textbf{Consignes.}

Les exercices 1 à 5 (qui portent sur la logique) et le problème final
(qui porte sur la calculabilité) sont totalement indépendants les uns
des autres.  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).  \textbf{Le non-respect
  de cette consigne pourra être pénalisé.}

\medbreak

La longueur du sujet ne doit pas effrayer : les réponses attendues
sont souvent plus courtes que les questions.  Notamment, l'énoncé du
problème est long parce que des rappels et éclaircissements ont été
faits et que les questions ont été rédigées de façon aussi précise que
possible.

\medbreak

Dans les exercices portant sur Rocq (exercices 1 à 4), les erreurs de
syntaxe Rocq ne seront pas pénalisées tant qu'on comprend clairement
l'intention.  De même, quand on demande d'écrire un $\lambda$-terme,
il n'est pas indispensable de suivre exactement les notations
introduites en cours.

\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$) :
2+2+4+3+3+6

\ifcorrige
Ce corrigé comporte 11 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

Dans cet exercice, on considère des paires d'états d'une preuve en Rocq avant et après l'application d'une tactique. On demande de retrouver quelle est la tactique ou la séquence de tactiques appliquée.

\smallskip


\textbf{(1)} On part de l'état suivant :

\begin{verbatim}
  A, B, C : Prop
  H : (A /\ B) /\ C
  ============================
  A
\end{verbatim}

\noindent et on veut arriver à l'état suivant :

\begin{verbatim}  
  A, B, C : Prop
  H1 : A /\ B
  H2 : C
  ============================
  A
\end{verbatim}

\smallskip

\textbf{(2)} On part de l'état suivant :

\begin{verbatim}
  A, B, C : Prop
  ============================
  (A \/ B) /\ C <-> (A /\ C) \/ (A /\ C)
\end{verbatim}

\noindent et on veut arriver à l'état suivant :

\begin{verbatim}
First subgoal:
  
  A, B, C : Prop
  ============================
  (A \/ B) /\ C -> (A /\ C) \/ (A /\ C)

Second subgoal:

  A, B, C : Prop
  ============================
  (A /\ C) \/ (A /\ C) -> (A \/ B) /\ C
\end{verbatim}

\smallskip

\textbf{(3)} On part de l'état suivant :

\begin{verbatim}
  A, B, C : Prop
  H1 : B
  H2 : C
  ============================
  A \/ B
\end{verbatim}

\noindent et on veut arriver à l'état suivant :

\begin{verbatim}
  No more goals.
\end{verbatim}

\smallskip

\textbf{(4)} On part de l'état suivant :

\begin{verbatim}
  A, B : Prop
  H1 : A -> B
  H2 : ~ B
  ============================
  ~A
\end{verbatim}

\noindent et on veut arriver à l'état suivant :

\begin{verbatim}
  A, B : Prop
  H1 : A -> B
  H2 : ~ B
  H3 : A
  ============================
  B
\end{verbatim}

\smallskip

\textbf{(5)} On part de l'état suivant :

\begin{verbatim}
  n, m : nat
  H : S n = S m
  ============================
  n = m
\end{verbatim}

\noindent et on veut arriver à l'état suivant :

\begin{verbatim}
  n, m : nat
  H : n = m
  ============================
  n = m
\end{verbatim}

\smallskip

\textbf{(6)} On part de l'état suivant :

\begin{verbatim}
  n : nat
  ============================
  n + 0 = n
\end{verbatim}

\noindent et on veut arriver à l'état suivant :

\begin{verbatim}
First subgoal:
  
  ============================
  0 + 0 = 0

Second subgoal:

  n : nat
  IHn : n + 0 = n
  ============================
  S n + 0 = S n
\end{verbatim}

\smallskip

\textbf{(7)} On part de l'état suivant :

\begin{verbatim}
  n : nat
  IHn : n + 0 = n
  ============================
  S n + 0 = S n
\end{verbatim}

\noindent et on veut arriver à l'état suivant :

\begin{verbatim}
  n : nat
  IHn : n + 0 = n
  ============================
  S (n + 0) = S n
\end{verbatim}

\smallskip

\textbf{(8)} On part de l'état suivant :

\begin{verbatim}
  n : nat
  IHn : n + 0 = n
  ============================
  S (n + 0) = S n
\end{verbatim}

\noindent et on veut arriver à l'état suivant :

\begin{verbatim}
  n : nat
  IHn : n + 0 = n
  ============================
  n + 0 = n
\end{verbatim}

\begin{corrige}
  \smallskip

  \textbf{(1)} \verb|destruct H as (H1, H2).|


  \textbf{(2)} \verb|split.|


  \textbf{(3)} \verb|right. assumption.|


  \textbf{(4)} \verb|intros H3. apply H2.|

  \textbf{(5)} \verb|injection H as H.|

  \textbf{(6)} \verb+induction n as [|n IHn].+ ou simplement \verb|induction n.|

  \textbf{(7)} \verb|simpl.|

  \textbf{(8)} \verb|f_equal.| (la tactique) ou \verb|apply f_equal.| (le lemme).
\end{corrige}

%
%
%

\exercice

Si l'on dispose du lemme suivant en Rocq :

\begin{verbatim}
  Lemma mul_0_r : forall n : nat, n * 0 = 0.
\end{verbatim}

Parmi les buts suivants, quand peut-on utiliser ce lemme avec la tactique \texttt{rewrite} ? Quand peut-on utiliser ce lemme avec la tactique \texttt{apply} ? Justifier brièvement.

\smallskip

\textbf{(1)}

\begin{verbatim}
  n : nat
  ============================
  n * 0 = 0 + 0
\end{verbatim}

\smallskip

\textbf{(2)}

\begin{verbatim}
  n, m : nat
  ============================
  (n + m) * 0 = n * 0 + m * 0
\end{verbatim}

\smallskip

\textbf{(3)}

\begin{verbatim}
  n, m : nat
  ============================
  n + 0 = n
\end{verbatim}

\begin{corrige}
  \smallskip

  \textbf{(1)} On peut utiliser \texttt{rewrite -> mul\_0\_r.} car le but contient un sous-terme de la forme \texttt{?n * 0} (où \texttt{?n} est \texttt{n}). On peut également utiliser \texttt{apply mul\_0\_r.} car le but est convertible à \texttt{?n * 0 = 0} (car la partie droite de l'égalité se simplifie en \texttt{0}).

  \textbf{(2)} On peut utiliser \texttt{rewrite -> mul\_0\_r.} car le but contient un sous-terme de la forme \texttt{?n * 0} (où \texttt{?n} est \texttt{n + m}). On ne peut pas utiliser \texttt{apply mul\_0\_r.} car le but n'est pas convertible à \texttt{?n * 0 = 0}.

  \textbf{(3)} On peut utiliser \texttt{rewrite <- mul\_0\_r.} car le but contient un sous-terme de la forme \texttt{0}. On ne peut pas utiliser \texttt{apply add\_0\_r.} car le but n'est pas convertible à \texttt{?n * 0 = 0}.
\end{corrige}

%
%
%

\exercice

\textbf{(A)} Pour chacun des termes de preuve Rocq suivants, retrouver
le théorème du calcul propositionnel intuitionniste qu'il prouve.
(Ici, \texttt{A}, \texttt{B}, \texttt{C} vivent dans \texttt{Prop}.)

\smallskip

\textbf{(1)} \verb|fun (H1 : A) (H2 : B) => H2|

\smallskip

\textbf{(2)} \verb|fun (H1 : A) (H2 : ~ A) => H2 H1|

\smallskip

\textbf{(3)} \verb|fun (H1 : A -> (B -> C)) (H2 : B) (H3 : A) => H1 H3 H2|

\smallskip

\textbf{(B)} Pour chaque formule logique suivante, en donner une
preuve (en calcul propositionnel intuitionniste pour (1)–(4)).  La
preuve sera exprimée de préférence sous forme d'un $\lambda$-terme,
qui n'a pas à être justifié si on est sûr qu'il est correct et qu'on
veut gagner du temps ; toutefois, si on ne sait pas écrire le
$\lambda$-terme ou si on a un doute à son sujet, on pourra donner une
preuve en déduction naturelle (présentée comme arbre de preuve ou sous
forme drapeau), qui vaudra au moins une partie des points.

\smallskip

\textbf{(1)} $A \Rightarrow A$

\smallskip

\textbf{(2)} $A \Rightarrow (A \land A)$

\smallskip

\textbf{(3)} $(A \lor A) \Rightarrow A$

\smallskip

\textbf{(4)} $\neg(A \lor B) \Rightarrow \neg A$

\smallskip

\textbf{(5)} $((\forall x.\; P(x)) \lor (\forall x.\; Q(x))) \Rightarrow (\forall x.\; (P(x) \lor Q(x)))$ (en logique du premier ordre intuitionniste)

\smallskip



\begin{corrige}

\smallskip

\textbf{(A)}

  \textbf{(1)} $A \Rightarrow B \Rightarrow B$

  \textbf{(2)} $A \Rightarrow \neg \neg A$

  \textbf{(3)} $(A \Rightarrow B \Rightarrow C) \Rightarrow B \Rightarrow A \Rightarrow C$

\smallskip

\textbf{(B)}

  \textbf{(1)} $\lambda(u:A).\; u$

  \textbf{(2)} $\lambda(u:A).\; \langle u,u\rangle$

  \textbf{(3)} $\lambda(u:A\lor A).\; (\texttt{match~}u\texttt{~with~}
  \iota_1 v \mapsto v,\; \iota_2 v \mapsto v)$ (noter qu'on peut
  préférer l'écrire avec des noms de variables liées différentes dans
  l'alternative : $\lambda(u:A\lor A).\;
  (\texttt{match~}u\texttt{~with~} \iota_1 v_1 \mapsto
  v_1,\penalty-100\; \iota_2 v_2 \mapsto v_2)$, c'est exactement
  équivalent)

  \textbf{(4)} $\lambda(h:\neg(A \lor B)).\; \lambda(u:A).\; h(\iota_1^{(A,B)} u)$

  \textbf{(5)} $\lambda(h:(\forall x.\; P(x)) \lor (\forall x.\;
  Q(x))).\; (\texttt{match~}h\texttt{~with~} \iota_1 g \mapsto
  \lambda(x:I).\; \iota_1^{(P(x),Q(x))}(g x),\penalty-500\; \iota_2 g
  \mapsto \lambda(x:I).\penalty0\; \iota_2^{(P(x),Q(x))}(g x))$ ou, si
  on préfère, $\lambda(h:(\forall x.\; P(x)) \lor (\forall x.\;
  Q(x))).\; \lambda(x:I).\penalty-500\;
  (\texttt{match~}h\texttt{~with~} \iota_1 g \mapsto
  \iota_1^{(P(x),Q(x))}(g x),\penalty-500\; \iota_2 g \mapsto
  \iota_2^{(P(x),Q(x))}(g x))$
\end{corrige}


%
%
%

\exercice

\textbf{(1)} Définir en Rocq un type inductif pour représenter les arbres binaires contenant des entiers.

\smallskip

\textbf{(2)} Définir une fonction \texttt{miroir} qui, étant donné un arbre binaire, renvoie son miroir (symétrie gauche-droite).

\smallskip

\textbf{(3)} Énoncer un lemme en Rocq affirmant que le miroir du miroir d'un arbre est l'arbre lui-même.

\smallskip

\textbf{(4)} Avec quelle(s) tactique(s) peut-on prouver ce lemme ? Expliquer brièvement.

\smallskip

\textbf{(5)} Définir une fonction \texttt{taille} qui calcule le nombre de noeuds d'un arbre binaire.

\smallskip

\textbf{(6)} Expliquer succinctement comment prouver en Rocq que la taille d'un arbre et la taille de son miroir sont égales.

\begin{corrige}
  \smallskip

  \textbf{(1)} On définit un type inductif pour les arbres binaires :

\begin{verbatim}
Inductive arbre : Type :=
| feuille : arbre
| noeud : nat -> arbre -> arbre -> arbre.
\end{verbatim}

  \textbf{(2)} On définit la fonction \texttt{miroir} par récursion structurelle :

\begin{verbatim}
Fixpoint miroir (a : arbre) : arbre :=
  match a with
  | feuille => feuille
  | noeud v g d => noeud v (miroir d) (miroir g)
  end.
\end{verbatim}

  \textbf{(3)} \verb|Lemma miroir_involutif : forall a : arbre, miroir (miroir a) = a.|

  \textbf{(4)} On peut prouver ce lemme par induction structurelle sur \texttt{a} (tactique \texttt{induction a.}). Après la simplification par \texttt{simpl.}, chaque cas se résout facilement avec \texttt{reflexivity.} ou les hypothèses d'induction.

  \textbf{(5)} On définit la fonction \texttt{taille} par récursion :

\begin{verbatim}
Fixpoint taille (a : arbre) : nat :=
  match a with
  | feuille => 0
  | noeud v g d => (taille g) + (taille d)
  end.
\end{verbatim}

  \textbf{(6)} On énoncerait le lemme :

\verb|Lemma taille_miroir : forall a : arbre, taille a = taille (miroir a).|
  
  Pour le prouver, on utilise l'induction structurelle (\texttt{induction a.}). Le cas de base (feuille) se résout par \texttt{reflexivity.} Dans le cas récursif, la simplification calcule la taille du miroir. Les hypothèses d'induction permettent de réécrire les tailles du miroir des sous-arbres. On conclut en utilisant la commutativité de l'addition.

  Preuve complète :

\begin{verbatim}
Require Import Arith.

Lemma taille_miroir : forall a : arbre, taille a = taille (miroir a).
Proof.
  induction a; simpl.
  - reflexivity.
  - rewrite IHa1.
    rewrite IHa2.
    apply Nat.add_comm.
Qed.
\end{verbatim}
\vskip-4ex\leavevmode
\end{corrige}


%
%
%

\exercice

Dans cet exercice, on veut montrer que la « formule de Scott », à
savoir la formule propositionnelle suivante :
\[
((\neg\neg A \Rightarrow A) \,\Rightarrow\, (A \lor \neg A))
\;\Rightarrow\; (\neg\neg A \lor \neg A)
\]
n'est pas un théorème du calcul propositionnel intuitionniste.

Pour cela, on introduit l'espace topologique $X = \mathbb{R}$ et
l'ouvert suivant :
\[
\begin{aligned}
U \;&=\; \left\{ x\in \mathbb{R} \;:\; x>0 \;\text{~et~}\; \forall
n\in\mathbb{N}.(x\neq 2^{-n}) \right\}\\
&=\; \mathbb{R}_{>0} \setminus \{1,\frac{1}{2},\frac{1}{4},\frac{1}{8},\ldots\}\\
&=\; \mathopen]1;+\infty\mathclose[
\;\cup\; \mathopen]\frac{1}{2};1\mathclose[
\;\cup\; \mathopen]\frac{1}{4};\frac{1}{2}\mathclose[
\;\cup\; \mathopen]\frac{1}{8};\frac{1}{4}\mathclose[
\;\cup\; \cdots\\
\end{aligned}
\]
(On rappellera brièvement pourquoi $U$ est bien un ouvert.)

Donner la valeur, pour la sémantique des ouverts de $X$, de chaque
sous-formule de la formule de Scott dans laquelle $A$ a été remplacé
par $U$, et en déduire pourquoi la formule de Scott n'est pas
démontrable.  On représentera chaque ensemble graphiquement en plus
d'expliciter sa valeur avec des symboles.

(Il est recommandé de faire particulièrement au point $0$ et, pour
éviter les erreurs, de bien s'assurer qu'on a affaire à un ouvert à
chaque fois.)

\begin{corrige}
D'abord, $U$ est un ouvert parce que c'est une réunion d'intervalles
ouverts.

On trouve successivement :
\begin{itemize}
\item L'ensemble $\dottedneg U$ est l'ensemble $\mathbb{R}_{<0} =
  \mathopen]-\infty;0\mathclose[$ des réels strictement négatifs.
\item L'ensemble $\dottedneg\dottedneg U$ est l'ensemble
  $\mathbb{R}_{>0} = \mathopen]0;+\infty\mathclose[$ des réels
    strictement positifs.
\item L'ensemble $\dottedneg\dottedneg U \dottedlimp U$ est l'ensemble
  $\{ x\in \mathbb{R} \;:\; x\neq 0 \;\text{~et~}\; \forall
  n\in\mathbb{N}.(x\neq 2^{-n}) \}$ des réels non nuls qui ne sont pas
  un $2^{-n}$, ensemble qui est aussi la réunion de $U$ et de
  $\mathopen]-\infty;0\mathclose[$.  (Le seul point véritablement
    problématique est $0$, mais il ne peut pas appartenir à l'ouvert
    car les $2^{-n}$ n'y sont pas, et si un ouvert contient $0$ il
    doit contenir un intervalle ouvert autour de $0$, donc tous les
    $2^{-n}$ à partir d'un certain rang.)
\item L'ensemble $U \dottedlor \dottedneg U$ est le même ensemble
  $U \cup \mathopen]-\infty;0\mathclose[$ qu'au point précédent.
\item L'ensemble $(\dottedneg\dottedneg U \dottedlimp U) \dottedlimp
  (U \dottedlor \dottedneg U)$ est $\mathbb{R}$ tout entier,
  précisément parce que les deux points précédents donnent le même
  ouvert.
\item L'ensemble $\dottedneg\dottedneg U \dottedlor \dottedneg U$ est
  l'ensemble $\mathopen]-\infty;0\mathclose[ \cup
    \mathopen]0;+\infty\mathclose[ = \mathbb{R}\setminus\{0\}$ des
    réels non nuls.
\item L'ensemble associé à la formule de Scott tout entière est le
  même ensemble $\mathbb{R}\setminus\{0\}$ qu'au point précédent.
\end{itemize}
Comme on a trouvé autre chose que $\mathbb{R}$, par correction de la
sémantique des ouverts sur $X = \mathbb{R}$, la formule de Scott ne
peut pas être démontrable en calcul propositionnel intuitionniste.
\end{corrige}



%
%
%

\exercice[Problème]

\textbf{Rappels de quelques définitions et notations habituelles.}  On rappelle
qu'un \textbf{mot binaire} est une suite finie (éventuellement
vide, c'est-à-dire de longueur nulle) de $0$ et de $1$.  On notera
$\{0,1\}^* = \{\varepsilon, 0, 1, 00, 01, 10, 11, 000, \ldots\}$ (ici,
$\varepsilon$ désigne le mot vide) l'ensemble de tous les mots
binaires.  La \textbf{longueur} $|w|$ d'un mot binaire $w \in
\{0,1\}^*$ est le nombre total de bits qu'il contient (p.ex., $|00|=2$
et $|\varepsilon|=0$), et nous suivrons la convention de numéroter les
bits de la gauche vers la droite de $0$ à $|w|-1$ (par exemple, le bit
numéroté $0$ de $1010$ vaut $1$, tandis que son bit numéroté $3$
vaut $0$).  On dit qu'un mot binaire $u$ est un \textbf{préfixe} d'un
mot binaire $v$ lorsque $v$ commence par les bits de $u$, ou,
formellement : $|u|\leq|v|$ et pour chaque $0\leq j < |u|$, le bit
numéroté $j$ de $v$ est égal au bit numéroté $j$ de $u$.  (Par
exemple, $1010$ est un préfixe de $1010111$, tout mot binaire est un
préfixe de lui-même, et $\varepsilon$ est un préfixe de n'importe quel
mot binaire.)

\medskip

On pourra utiliser sans justification et sans commentaire le fait que
les mots binaires peuvent être manipulés algorithmiquement (via un
codage de Gödel qu'on ne demande pas de préciser) : notamment,
calculer la longueur d'un mot, ou renvoyer son bit numéroté $i$, sont
des opération calculables.

\medskip

On appelle \textbf{arbre de Kleene} l'ensemble $\mathscr{K} \subseteq
\{0,1\}^*$ de mots binaires défini de la manière suivante : un mot
binaire $w \in \{0,1\}^*$ de longueur $|w|$ appartient à $\mathscr{K}$
lorsque, pour chaque $0 \leq i < |w|$, le bit numéroté $i$ de $w$ vaut
\begin{itemize}
\item $0$ s'il existe un arbre de calcul (codé par un entier) $<|w|$
  attestant $\varphi_i(0) = 0$,
\item $1$ s'il existe un arbre de calcul (codé par un entier) $<|w|$
  attestant $\varphi_i(0) = r$, où $r\neq 0$,
\item et arbitraire sinon,
\end{itemize}
où $\varphi_i$ désigne la $i$-ième fonction générale récursive
(d'arité $1$).

\emph{Si on préfère} parler en termes de machines de Turing, on pourra
changer la définition en :
\begin{itemize}
\item $0$ si la $i$-ième machine de Turing
  termine\footnote{Sous-entendu : à partir d'une bande vierge (ou
  d'une bande représentant le nombre $0$, ou tout autre état initial
  fixé sans importance).} en $<|w|$ étapes et renvoie $0$,
\item $1$ si la $i$-ième machine de Turing termine en $<|w|$
  étapes et renvoie une valeur $r \neq 0$,
\item et arbitraire sinon
\end{itemize}
(cela ne changera rien de substantiel aux raisonnements).

Informellement dit, l'appartenance d'un mot $w$ à $\mathscr{K}$ est
déterminée par le résultat de l'exécution des $|w|$ premiers
programmes, chacun jusqu'à la borne $|w|$, et le bit numéroté $i$
de $w$ est contraint, si le programme $i$ termine, par le résultat de
celui-ci.

(On prendra note du fait que $\varepsilon \in \mathscr{K}$ car la
contrainte « pour chaque $0\leq i < |w|$ » est vide — donc
trivialement vérifiée — vu que $|\varepsilon|=0$.)

\bigskip

\textbf{(1)} Montrer que si $v \in \mathscr{K}$ et si $u$ est un
préfixe de $v$. alors on a aussi $u \in \mathscr{K}$.

\begin{corrige}
Supposons que $u$ soit un préfixe de $v$ avec $v \in \mathscr{K}$.
Alors pour tout $i$ tel que $0\leq i < |u|$, le bit numéroté $i$
de $u$ est aussi le bit numéroté $i$ de $v$, qui d'après les
conditions sur $v \in \mathscr{K}$, vaut $0$ (resp. $1$) s'il existe
un arbre de calcul $<|v|$ attestant $\varphi_i(0) = 0$
(resp. $\varphi_i(0) \neq 0$), et à plus forte raison s'il existe un
arbre de calcul $<|u|$ l'attestant : ceci implique donc bien $u \in
\mathscr{K}$.
\end{corrige}

\medskip

On dit que $\mathscr{K}$ est un \textbf{arbre} de mots
binaires\footnote{Si cette terminologie semble mystérieuse,
l'explication est que le graphe (infini d'après la question (3)) dont
les sommets sont les éléments de $\mathscr{K}$, avec une arête de $u$
à $v$ lorsque $u$ est un préfixe de $v$, est un arbre (infini) au sens
de la théorie des graphes.  Cette remarque n'est pas utile pour le
présent exercice.}  pour exprimer la propriété démontrée par cette
question (1). (Formellement, un arbre de mots binaires est une partie
$\mathscr{T} \subseteq \{0,1\}^*$ telle que si $v\in\mathscr{T}$ et
que $u$ est un préfixe de $v$, alors $u\in\mathscr{T}$.)

\medskip

\textbf{(2)} Montrer que $\mathscr{K}$ est une partie \emph{décidable}
(i.e., calculable) de $\{0,1\}^*$.  Sa fonction indicatrice est-elle
primitive récursive ?

\begin{corrige}
On veut montrer qu'il existe un algorithme qui, donné un $w \in
\{0,1\}^*$, décide si $w \in \mathscr{K}$.  Pour cela, il suffit de
parcourir les bits $0\leq i<|w|$ de $w$ et, pour chacun de tester si
la condition définissant $\mathscr{K}$ est vérifiée : on parcourt les
entiers $0\leq j<|w|$ et, pour chacun, on teste s'il s'agit du code
d'un arbre de calcul attestant $\varphi_i(0) = r$ pour un certain $r$,
et, si c'est le cas, on vérifie que le bit $w_i$ de $w$ vaut $0$ si
$r=0$ ou $1$ si $r\neq 0$.  (Si on préfère les machines de Turing, on
lance l'exécution de la $i$-ième machine pour au plus $|w|-1$ étapes
et le reste est analogue.)  Si une des conditions échoue, le mot $w$
n'est pas dans $\mathscr{K}$, tandis que si toutes réussissent, le mot
est dans $\mathscr{K}$.  Il s'agit bien là d'un algorithme qui termine
à coup sûr en temps fini.  Il est même primitif récursif puisqu'on a
essentiellement deux boucles imbriquées, une sur $i$ et une sur $j$,
bornées par $|w|$.
\end{corrige}

\medskip

\textbf{(3)} Montrer qu'il existe dans $\mathscr{K}$ des mots binaires
de longueur arbitrairement grande (formellement : $\forall n. \;
\exists w\in\mathscr{K}. \; (|w| \geq n)$).  On pourra même expliquer
comment en calculer algorithmiquement un de longueur quelconque.

\begin{corrige}
Comme on l'a expliqué à la question (2), la condition définissant
l'appartenance d'un mot à $w$ est testable algorithmiquement.  Pour
fabriquer un mot de $\mathscr{K}$ de longueur $n$, on teste, pour
chaque $0\leq i<|w|$ s'il existe un arbre de calcul $<n$ attestant
$\varphi_i(0) = r$ pour un certain $r$ (ou, si on préfère, si
l'exécution de la $i$-ième machine pour au plus $n-1$ étapes termine
et renvoie une valeur $r$), et, si c'est le cas, on donne au bit
numéroté $i$ de $w$ la valeur imposée par ce $r$ (forcément unique,
puisqu'il s'agit da la valeur de $\varphi_i(0)$), sinon on lui donne
une valeur quelconque, disons $0$ : le mot formé des bits qu'on vient
de dire est dans $\mathscr{K}$ puisqu'il vérifie les contraintes.  De
plus, on l'a calculé algorithmiquement.  Il existe donc bien un mot de
longueur $n$ de $\mathscr{K}$ pour chaque $n$, et même un algorithme
qui en renvoie un en fonction de $n$.  Ceci implique trivialement ce
qui était demandé.
\end{corrige}

\medskip

On appelle \textbf{branche infinie} de $\mathscr{K}$ une suite infinie
$(b_i)_{i\in\mathbb{N}}$ de bits (i.e., un élément de
$\{0,1\}^{\mathbb{N}}$) dont tous les préfixes appartiennent
à $\mathscr{K}$, c'est-à-dire : $b_0\cdots b_{\ell-1} \in \mathscr{K}$
pour tout $\ell \in \mathbb{N}$.

\medskip

\textbf{(4)} \emph{Indépendamment de tout ce qui précède,} montrer
qu'il n'existe pas d'algorithme qui prend en entrée un $e \in
\mathbb{N}$, \emph{termine toujours en temps fini}, et renvoie
\begin{itemize}
\item $0$ si $\varphi_e(0){\downarrow} = 0$,
\item $1$ si $\varphi_e(0){\downarrow} = r$ où $r \neq 0$,
\item et une valeur arbitraire sinon (i.e., si $\varphi_e(0)$ n'est
  pas définie).
\end{itemize}

\emph{Si on préfère} parler en termes de machines de Turing, on pourra
montrer qu'il n'existe pas d'algorithme qui prend en entrée le code
$e$ d'une machine de Turing, \emph{termine toujours en temps fini}, et
renvoie
\begin{itemize}
\item $0$ si la $e$-ième machine de Turing termine et qu'elle
  renvoie $0$,
\item $1$ si la $e$-ième machine de Turing termine et qu'elle renvoie
  une valeur $r \neq 0$,
\item et une valeur arbitraire sinon.
\end{itemize}

\emph{Indication :} utiliser l'astuce de Quine pour construire un
programme qui fait le contraire de ce qu'on lui prédit.

\emph{Attention !} On demande dans cette question une démonstration
précise : on ne se contentera pas d'un raisonnement informel du type
« on ne peut pas savoir si $\varphi_e(0)$ terminera un jour, donc on
ne peut pas calculer sa valeur ».

\begin{corrige}
Supposons par l'absurde qu'il existe un algorithme qui prend en
entrée $e$, termine toujours en temps fini et renvoie une valeur comme
indiqué dans la question ; appelons $f$ la fonction calculable que
calcule cet algorithme.  On va aboutir à une contradiction.

Considérons maintenant le programme $e$ défini comme suit.  Il ignore
son argument, calcule $f(e)$ en vertu de l'algorithme dont on vient de
supposer l'existence, et renvoie $1$ si $f(e)=0$ et $0$ si $f(e)\neq
0$.  L'astuce de Quine rend légitime l'utilisation de $e$ dans sa
propre définition (formellement : considère la fonction qui à $e$
associe la fonction qu'on vient de dire, et on applique le théorème de
récursione de Kleene à cette fonction).  Par construction, cet
algorithme termine toujours en temps fini (puisqu'on a supposé que
c'était le cas du calcul de $f$).  Bref, $\varphi_e(n)$ est toujours
défini, et $\varphi_e(n) = 1$ si $f(e)=0$ et $\varphi_e(n) = 0$ si
$f(e) \neq 0$.

Si $f(e)=0$ alors $\varphi_e(0) = 1$ comme on vient de le dire, donc
on a $f(e)=1$ par définition de la fonction $f$, ce qui est une
contradiction ; et si $f(e)\neq 0$ alors $\varphi_e(0) = 0$ comme on
vient de le dire, donc $f(e)=0$ par définition de la fonction $f$, ce
qui est de nouveau une contradiction.

C'est donc que notre hypothèse (de calculabilité de $f$) était
absurde.
\end{corrige}

\medskip

\textbf{(5)} Déduire de (4) qu'il n'existe aucune branche infinie
calculable de $\mathscr{K}$.

\begin{corrige}
Si $(b_i)$ est une branche infinie de $\mathscr{K}$, vérifions que $e
\mapsto b_e$ vérifie les conditions du (4) (c'est-à-dire vaut $0$ si
$\varphi_e(0){\downarrow}=0$ et $r$ si $\varphi_e(0){\downarrow}\neq
0$).  Supposons que $\varphi_e(0){\downarrow}$, mettons $\varphi_e(0)
= r$ : alors il existe un arbre de calcul l'attestant, codé, disons,
par un entier $m$.  Appelons $\ell = \max(m, e) + 1$.  Le mot $w :=
b_0\cdots b_{\ell-1}$ (de longueur $\ell > m$) est dans $\mathscr{K}$
par l'hypothèse que $(b_i)$ est une branche de $\mathscr{K}$.  Il
existe un arbre de calcul codé par un entier $<|w|$ (à savoir $m$)
attestant $\varphi_e(0) = r$, donc le bit $b_e$ de $w$ vaut $0$
si $r=0$ et $1$ si $r\neq 0$.  On a donc bien prouvé que $e \mapsto
b_e$ vérifie les conditions du (4).  Or on a vu en (4) qu'une telle
fonction ne peut pas être calculable.  C'est donc que $\mathscr{K}$
n'a pas branche infinie calculable.
\end{corrige}

\medskip

Le \textbf{lemme de Kőnig} est l'affirmation suivante : « tout arbre
de mots binaires contenant des mots de longueur arbitrairement grande
a une branche infinie » (les termes « arbre de mots binaires »,
« contenant des mots de longueur arbitrairement grande » et « branche
infinie » ont été définis précisément ci-dessus).  On ne demande pas
de démontrer cette affirmation : néanmoins, c'est un théorème des
mathématiques classiques usuelles.

\medskip

\textbf{(6)} Pour résumer, que peut-on conclure du lemme de Kőnig, et
des questions précédentes, concernant l'arbre $\mathscr{K}$ ?  Comment
expliqueriez-vous informellement la situation ?

\begin{corrige}
On a vu que $\mathscr{K}$ est un arbre de mots binaires calculable,
contenant des mots de longueur arbitrairement grande.  Par le lemme de
Kőnig, il a des branches infinies.  Néanmoins, aucune de ses branches
n'est calculable.

On peut décrire informellement $\mathscr{K}$ comme un « labyrinthe
infini, calculable mais impossible à résoudre de façon calculable » :
les pièces du labyrinthe sont les nœuds de l'arbre, c'est-à-dire les
$w\in\mathscr{K}$, chaque pièce permet d'aller potentiellement vers
$w0$ ou $w1$ selon si l'un ou l'autre (ou aucun des deux) n'est
dans $\mathscr{K}$.  On peut algorithmiquement faire un plan du
labyrinthe jusqu'à n'importe quelle profondeur finie.  Néanmoins, si
on postule que le labyrinthe possède une sortie au bout de chaque
branche infinie (les branches finies étant des culs-de-sac), alors
aucun algorithme ne peut naviguer le labyrinthe jusqu'à une sortie,
bien que des chemins menant à une sortie existent (par le lemme de
Kőnig).
\end{corrige}

\medskip

\textbf{(7)} Expliquer pourquoi la question (5) \emph{suggère} que le
lemme de Kőnig n'est pas démontrable en mathématiques constructives.
(On ne demande pas ici un raisonnement formel précis, mais une idée.)

\begin{corrige}
Une démonstration constructive du lemme de Kőnig, formalisée dans un
système semblable à l'arithmétique de Heyting, permettrait
vraisemblablement d'extraire de la preuve un algorithme qui calcule
une branche infinie de l'arbre (cet arbre étant lui-même calculable
pour commencer).  Or on vient de voir que ce n'est pas le cas, ce qui
suggère qu'une telle démonstration n'est pas possible.
\end{corrige}



%
%
%
\end{document}