%% 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 / 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{29 janvier 2025}
\maketitle

\pretolerance=8000
\tolerance=50000

\vskip1truein\relax

\noindent\textbf{Consignes.}

Les exercices et le problème 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).

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

Les exercices 1 à 4 portent sur Coq.  L'exercice 5 porte sur le calcul
propositionnel.  Le problème final porte sur la calculabilité.

\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$) :
\textcolor{red}{à écrire}.

\ifcorrige
Ce corrigé comporte 14 pages \textcolor{red}{(à revérifier)} (page de garde incluse).
\else
Cet énoncé comporte 8 pages \textcolor{red}{(à revérifier)} (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 Coq 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
  ============================
  (A /\ B) /\ C <-> A /\ B /\ C
\end{verbatim}

et on veut arriver à l'état suivant :

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

Second subgoal:

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

\smallskip


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

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

et on veut arriver à l'état suivant :

\begin{verbatim}  
  H1 : A
  H2 : B
  H3 : C
  ============================
  A
\end{verbatim}

\smallskip

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

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

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) -> ~ B -> ~ A
\end{verbatim}

et on veut arriver à l'état suivant :

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

\smallskip

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

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

et on veut arriver à l'état suivant :

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

Second subgoal:

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

\smallskip

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

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

et on veut arriver à l'état suivant :

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

\smallskip

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

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

et on veut arriver à l'état suivant :

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

\begin{corrige}
  \smallskip

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


  \textbf{(2)} En deux étapes : \verb|destruct H as (H1, H3). destruct H1 as (H1, H2).| Possible également en une seule étape : \verb|destruct H as ((H1, H2), H3).|


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


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


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


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


  \textbf{(7)} \verb|injection H as H.|
\end{corrige}

%
%
%

\exercice

Si l'on dispose du lemme suivant en Coq :

\begin{verbatim}
  Lemma add_0_r : forall n : nat, n + 0 = n.
\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 + n
\end{verbatim}

\smallskip

\textbf{(2)}

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

\smallskip

\textbf{(3)}

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

\smallskip

\textbf{(4)}

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

\begin{corrige}
  \smallskip

  \textbf{(1)} On peut utiliser \texttt{rewrite -> add\_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 add\_0\_r.} car le but est convertible à \texttt{?n + 0 = ?n} (car la partie droite de l'égalité se simplifie en \texttt{n}).

  \textbf{(2)} On peut utiliser \texttt{rewrite -> add\_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 add\_0\_r.} car le but n'est pas convertible à \texttt{?n + 0 = ?n} (sauf à réécrire au préalable le but avec la commutativité de l'addition).

  \textbf{(3)} On peut utiliser \texttt{rewrite -> add\_0\_r.} car le but contient un sous-terme de la forme \texttt{?n + 0} (où \texttt{?n} est \texttt{m * n}). On peut également utiliser \texttt{apply add\_0\_r.} car le but est de la forme \texttt{?n + 0 = ?n} (où \texttt{?n} est \texttt{m * n}).

  \textbf{(4)} On peut utiliser \texttt{rewrite -> add\_0\_r.} car le but contient un sous-terme de la forme \texttt{?n + 0} (où \texttt{?n} est \texttt{n}). On ne peut pas utiliser \texttt{apply add\_0\_r.} car le but n'est pas convertible à \texttt{?n + 0 = ?n} (sauf à se débarrasser au préalable du \texttt{+ m} grâce à la tactique \texttt{f\_equal}).
\end{corrige}

%
%
%

\exercice

Dans cet exercice, on donne un terme de preuve Coq et on demande de retrouver le théorème du calcul propositionnel intuitionniste qu'il prouve.

\smallskip

\textbf{(1)} \verb|fun H : A => H|

\smallskip

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

\smallskip

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

\begin{corrige}
  \smallskip

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

  \textbf{(2)} $(A \Rightarrow B) \Rightarrow (B \Rightarrow C) \Rightarrow A \Rightarrow C$.

  \textbf{(3)} $(A \Rightarrow B) \Rightarrow \neg B \Rightarrow \neg A$.
\end{corrige}


%
%
%

\exercice

\textbf{(1)} Définir en Coq un type pour représenter les jours de la semaine (7 valeurs possibles).

\smallskip

\textbf{(2)} Définir une fonction qui, étant donné un jour de la semaine, renvoie le jour suivant.

\smallskip

\textbf{(3)} Énoncer un lemme en Coq affirmant que le jour suivant du dimanche est le lundi.

\smallskip

\textbf{(4)} Avec quelle(s) tactique(s) peut-on prouver ce lemme ?

\smallskip

\textbf{(5)} Énoncer un lemme en Coq affirmant que le jour suivant du jour $j$ n'est pas $j$.

\smallskip

\textbf{(6)} Expliquer dans les grandes lignes comment on pourrait prouver ce lemme en Coq (notamment qu'elles seraient les principales tactiques utilisées).

\begin{corrige}
  \smallskip

  \textbf{(1)} On définit un type inductif à 7 constructeurs :

\begin{verbatim}
Inductive jour : Type :=
| lundi : jour
| mardi : jour
| mercredi : jour
| jeudi : jour
| vendredi : jour
| samedi : jour
| dimanche : jour.
\end{verbatim}

  \textbf{(2)} On définit une fonction (non récursive) par pattern matching :

\begin{verbatim}
Definition suivant (j : jour) : jour :=
  match j with
  | lundi => mardi
  | mardi => mercredi
  | mercredi => jeudi
  | jeudi => vendredi
  | vendredi => samedi
  | samedi => dimanche
  | dimanche => lundi
  end.
\end{verbatim}

  \textbf{(3)} \verb|Lemma suivant_dimanche_lundi : suivant dimanche = lundi.|

  \textbf{(4)} \verb|simpl.| (optionnel) suivi de \verb|reflexivity.|

  \textbf{(5)} \verb|Lemma suivant_est_different : forall j : jour, suivant j <> j.| ou \verb|forall j : jour, ~ suivant j = j| (équivalents étant donné que \verb|<>| n'est qu'une notation en Coq).

  \textbf{(6)} On peut prouver ce lemme par analyse de cas sur \texttt{j} (tactique \texttt{destruct j.}). Après un appel optionnel à \texttt{simpl.} ou \texttt{simpl in *.} pour calculer la valeur de \texttt{suivant j} dans chaque cas, on peut conclure par \texttt{discriminate.} pour montrer que les deux termes sont différents.

  Preuve complète :

\begin{verbatim}
Lemma suivant_est_different : forall j : jour, suivant j <> j.
Proof.
  intros j H.
  destruct j; simpl in *; discriminate.
Qed.
\end{verbatim}
\vskip-4ex\leavevmode
\end{corrige}


%
%
%

\exercice

En utilisant une des sémantiques vues en cours pour le calcul
propositionnel intuitionniste, montrer que la formule suivante n'est
pas démontrable en calcul propositionnel intuitionniste :
\[
\big(((A\Rightarrow B)\Rightarrow B) \land ((B\Rightarrow A)\Rightarrow A)\big)
\; \Rightarrow \;
(A\lor B)
\]

(\emph{Indications :} Si on souhaite utiliser la sémantique des
ouverts, on pourra utiliser deux demi-droites de même origine dans la
droite réelle.  Si on souhaite utiliser la sémantique de Kripke, on
pourra prendre le cadre $\{u,v,w\}$ avec l'ordre engendré par les
seules relations $u\leq v$ et $u\leq w$, et considérer les
affectations de vérité valant $1$ uniquement dans le monde $v$
respectivement $w$.  Si on souhaite utiliser la sémantique de la
réalisabilité propositionnelle, on remarquera qu'un programme $e$ qui
réalise cette formule pour $A=\mathbb{N}$ et $B=\varnothing$ doit
renvoyer un élément de la forme $\langle 0,\emdash\rangle$ si on
l'applique à $\langle c,c\rangle$ avec $c$ le code de Gödel d'une
fonction constante quelconque, et que pour $A=\varnothing$ et
$B=\mathbb{N}$ il doit renvoyer $\langle 1,\emdash\rangle$.)

La formule en question est-elle démontrable en calcul propositionnel
classique ?  (On ne demande pas forcément d'en exhiber une
démonstration.)

\begin{corrige}
\emph{Avec la sémantique des ouverts :} Travaillons sur les ouverts de
$X = \mathbb{R}$.  Posons $U = \{t\in\mathbb{R} : t<0\}$ et $V =
\{t\in\mathbb{R} : t>0\}$.  Ce sont bien des ouverts.  Alors
$(U\dottedlimp V) = V$ donc $((U\dottedlimp V)\dottedlimp V) =
\mathbb{R}$.  Symétriquement, $((V\dottedlimp U)\dottedlimp U) =
\mathbb{R}$.  En revanche, $U\dottedlor V = \mathbb{R}\setminus\{0\}$.
On en déduit pour la formule tout entière que $\big(((U\dottedlimp
V)\dottedlimp V) \land ((V\dottedlimp U)\dottedlimp U)\big) \;
\dottedlimp \; (U\lor B)$ vaut $\mathbb{R}\setminus\{0\}$ : comme ceci
n'est pas $X$ tout entier, la formule n'est pas prouvable (par
correction de la sémantique des ouverts de $X$).

\emph{Avec la sémantique de Kripke :} Travaillons dans le cadre de
Kripke $\{u,v,w\}$ avec pour seules relations non-triviales $u\leq v$
et $u\leq w$.  Soit $p$ l'affectation de vérité valant $1$ en $v$ et
$0$ partout ailleurs, et $q$ celle valant $1$ en $w$ et $0$ partout
ailleurs.  Ce sont bien des affectations de vérité (c'est-à-dire ici
que si elles valent $1$ en $u$, ce qui ne se produit jamais, elles
valent $1$ partout).  On vérifie alors que $(p\dottedlimp q) = q$ donc
$((p\dottedlimp q)\dottedlimp q) = 1$.  Symétriquement,
$((q\dottedlimp p)\dottedlimp p) = 1$.  En revanche, $p\dottedlor q$
vaut $1$ en $v$ et $w$ mais $0$ en $u$.  On en déduit pour la formule
tout entière que $\big(((p\dottedlimp q)\dottedlimp q) \land
((q\dottedlimp p)\dottedlimp p)\big) \; \dottedlimp \; (p\lor q)$ vaut
$1$ en $v$ et $w$ mais $0$ en $u$ : comme ceci n'est pas $1$ partout,
la formule n'est pas prouvable (par correction de la sémantique de
Kripke).

\emph{Avec la sémantique de la réalisabilité propositionnelle :}
Supposons que $e$ réalise la formule.  Si $A = \mathbb{N}$ et $B =
\varnothing$, alors $(A \dottedlimp B) = \varnothing$ donc $((A
\dottedlimp B) \dottedlimp B) = \mathbb{N}$, et $(B \dottedlimp A) =
\mathbb{N}$ donc $((A \dottedlimp B) \dottedlimp B) = \mathbb{N}
\dottedlimp \mathbb{N}$ est l'ensemble des codes de Gödel des
fonctions récursives totales $\mathbb{N}\to\mathbb{N}$.  Fixons $c$ un
tel code de Gödel, disons celui du programme qui renvoie
immédiatement $0$.  Alors $\langle c,c\rangle$ est dans $((A
\dottedlimp B) \dottedlimp B) \dottedland ((A \dottedlimp B)
\dottedlimp B)$, donc $\varphi_e(\langle c,c\rangle)$ doit être dans
$A\dottedlor B$, et comme $B$ est vide, il est forcément de la forme
$\langle 0,m\rangle$ avec $m\in A$.  Mais exactement le même
raisonnement en échangeant $A$ et $B$ (qui ont un rôle symétrique)
montre que si $A = \varnothing$ et $B = \mathbb{N}$ alors
$\varphi_e(\langle c,c\rangle)$ doit être dans $A\dottedlor B$ et
cette fois de la forme $\langle 1,n\rangle$ avec $n\in B$.  Comme
$\varphi_e(\langle c,c\rangle)$ ne peut pas être à la fois de la forme
$\langle 0,\emdash\rangle$ et $\langle 1,\emdash\rangle$, c'est que la
formule n'est pas réalisable.  En particulier, elle n'est pas
prouvable (par correction de la sémantique de la rélisabilité
propositionnelle).

Enfin, concernant la formule en logique classique, un simple tableau
de vérité montre qu'elle est vraie dans chacun des quatre cas de
figure, donc la formule est classiquement prouvable (par complétude de
la sémantique booléenne pour la logique classique).
\end{corrige}



%
%
%

%% \bigbreak
%% \hbox to\hsize{\hrulefill}
%% \smallskip

\pagebreak

\exercice[Problème]

\textbf{Notations :} Dans tout cet exercice, on notera comme
d'habitude $\varphi_e\colon\mathbb{N}\dasharrow\mathbb{N}$ (pour
$e\in\mathbb{N}$) la $e$-ième fonction partielle calculable
(i.e. générale récursive).  On notera
\[
\mathsf{PartCalc} := \{\varphi_e \; : \; e\in\mathbb{N}\}
= \{g\colon\mathbb{N}\dasharrow\mathbb{N} \; : \;
\exists e\in\mathbb{N}.\,(g = \varphi_e)\}
\]
l'ensemble des fonctions \emph{partielles} calculables
$\mathbb{N}\dasharrow\mathbb{N}$, ainsi que
\[
\mathsf{TotCode} := \{e\in\mathbb{N} \; : \;
\varphi_e\hbox{~est totale}\}
= \{e\in\mathbb{N} \; : \; \varphi_e\in\mathsf{TotCalc}\}
\]
l'ensemble des codes des programmes qui définissent une fonction
\emph{totale} $\mathbb{N}\to\mathbb{N}$ (i.e., terminent et renvoient
un entier quel que soit l'entier qu'on leur fournit en entrée), et
\[
\mathsf{TotCalc} := \{\varphi_e \; : \; e\in\mathsf{TotCode}\}
= \{g\colon\mathbb{N}\to\mathbb{N} \; : \;
\exists e\in\mathbb{N}.\,(g = \varphi_e)\}
\]
l'ensemble correspondant des fonctions \emph{totales} calculables
$\mathbb{N}\to\mathbb{N}$, i.e., celles calculées par les programmes
qu'on vient de dire.

\smallskip

On va s'intéresser à la notion (qu'on va définir) de fonction
calculable $\mathsf{PartCalc} \to \mathbb{N}$ d'une part, et
$\mathsf{TotCalc} \to \mathbb{N}$ d'autre part.  (On parle parfois de
« fonctionnelles » ou de « fonction de second ordre » pour ces
fonctions sur les fonctions.  On souligne qu'on parle bien ici de
fonction \emph{totales} $\mathsf{PartCalc} \to \mathbb{N}$ et
$\mathsf{TotCalc} \to \mathbb{N}$.)

\medskip

\textbf{Définition :} (A) Une fonction (totale !) $F\colon
\mathsf{PartCalc} \to \mathbb{N}$ est dite \emph{calculable} lorsque
la fonction $\hat F\colon \mathbb{N} \to \mathbb{N}$ définie par $\hat
F(e) = F(\varphi_e)$ est calculable.\quad (B) De même, une fonction
(totale) $F\colon \mathsf{TotCalc} \to \mathbb{N}$ est dite calculable
lorsqu'il existe une fonction $\hat F\colon \mathbb{N} \dasharrow
\mathbb{N}$ partielle calculable telle que telle que $\hat F(e) =
F(\varphi_e)$ pour tout $e \in \mathsf{TotCode}$.

\smallskip

En français : une fonctionnelle définie sur l'ensemble des fonctions
calculables partielles ou totales est elle-même dite calculable
lorsqu'il existe un programme qui calcule $F(g)$ à partir du code $e$
d'un programme quelconque calculant $g$.

\smallskip

{\footnotesize

Il est évident dans le cas (A) que la fonction $\hat F$ vérifie
forcément $(\varphi_{e_1} = \varphi_{e_2}) \; \Longrightarrow (\hat
F(e_1) = \hat F(e_2))$ ; c'est-à-dire qu'elle est « extensionnelle » :
elle doit renvoyer la même valeur sur deux programmes qui calculent la
même fonction (= ont la même « extension »).  D'ailleurs (on ne
demande pas de justifier ce fait, qui est facile), se donner une
fonction $F\colon \mathsf{PartCalc} \to \mathbb{N}$ revient exactement
à se donner une fonction $\hat F\colon \mathbb{N} \to \mathbb{N}$
ayant cette propriété d'« extensionnalité ».  De même, dans le
cas (B), se donner une fonction $F\colon \mathsf{TotCalc} \to
\mathbb{N}$ revient exactement à se donner une fonction $\hat F\colon
\mathsf{TotCode} \dasharrow \mathbb{N}$ qui soit extensionnelle sur
$\mathsf{TotCode}$.  La définition ci-dessus dit donc que $F$ est
calculable lorsque la $\hat F$ qui lui correspond est elle-même
calculable dans le cas (A), ou, dans le cas (B) la restriction à
$\mathsf{TotCode}$ d'une fonction calculable partielle
sur $\mathbb{N}$ dont le domaine de définition contient au
moins $\mathsf{TotCode}$.

\par}

\bigskip

\textbf{(1)} Montrer que toute fonction (totale !) calculable $F\colon
\mathsf{PartCalc} \to \mathbb{N}$ est en fait constante.

Pour cela, on pourra supposer par l'absurde que $F$ prend deux valeurs
distinctes, disons $v_1$ et $v_2$, et considérer l'ensemble des $e$
tels que $F(\varphi_e) = v_1$ (i.e., tels que $\hat F(e) = v_1$).
(Pourquoi est-il décidable ?  Et pourquoi est-ce une contradiction ?)

\begin{corrige}
Si $F$ n'est pas constante, il existe $v_1\neq v_2$ tels que $F$
prenne la valeur $v_1$ et la valeur $v_2$, disons $F(\varphi_{e_1}) =
v_1$ et $F(\varphi_{e_2}) = v_2$.  Considérons l'ensemble $D_1$ des
$e$ tels que $F(\varphi_e) = v_1$, c'est-à-dire $\hat F(e) = v_1$ par
définition de $\hat F$.  D'une part, cet ensemble $D_1$ est
décidable : pour décider si $e\in D_1$, il suffit de calculer $\hat
F(e)$ (ce qui est possible par l'hypothèse que $F$, i.e., que $\hat
F$, est calculable), et tester si sa valeur vaut $v_1$.  D'autre part,
$D_1$ n'est ni vide (puisque $e_1 \in D_1$) et n'est pas plein
(puisque $e_2 \not\in D_1$).  Or ceci contredit le théorème de Rice,
lequel affirme que si $E \subseteq \mathsf{PartCalc}$ est tel que
l'ensemble $\{e \in \mathbb{N} : \varphi_e \in E\}$ est décidable,
alors il est vide ou plein (ici, on prend $E = \{g\in\mathsf{PartCalc}
: F(g) = v_1\}$).
\end{corrige}

\medskip

\textbf{(2)} Expliquer pourquoi il existe des fonctions calculables
(totales) $F\colon \mathsf{TotCalc} \to \mathbb{N}$ qui ne sont pas
constantes.  Donner un exemple explicite.

Pour cela, on pourra penser évaluer en un point, c'est-à-dire
exécuter, le programme dont on a reçu le code en argument (on
rappellera pourquoi on peut faire cela).  Par ailleurs, on fera
clairement ressortir pourquoi le raisonnement tenu ici ne s'applique
pas à la question (1).

\begin{corrige}
La fonction partielle $e\mapsto\varphi_e(0)$ (ou, plus généralement,
$(e,x) \mapsto \varphi_e(x)$) est calculable par l'existence d'un
programme universel.  Ceci montre que la fonction $F\colon
\mathsf{TotCalc} \to \mathbb{N}$ donnée par $g \mapsto g(0)$ est
calculable (la fonction $\hat F$ qui lui correspond étant justement
$e\mapsto\varphi_e(0)$).  Ce raisonnement n'était pas applicable à
$\mathsf{PartCalc}$ car on cherche à définir une fonction
\emph{totale}, or $g \mapsto g(0)$ n'est que partielle sur
$\mathsf{PartCalc}$ (tandis qu'elle est totale sur
$\mathsf{TotCalc}$).

Plus généralement, on peut construire énormément de fonctions
calculables $\mathsf{TotCalc} \to \mathbb{N}$ en appliquant librement
l'évaluation de l'argument qu'on a reçu (qui, par hypothèse, est
toujours défini).  Un autre exemple serait la fonction $g \mapsto g(0)
+ g(1)$ ou encore $g \mapsto g(g(0))$.
\end{corrige}

\medskip

Fixons maintenant une fonction calculable $F\colon \mathsf{TotCalc}
\to \mathbb{N}$, ainsi que la fonction $\hat F\colon \mathbb{N}
\dasharrow \mathbb{N}$ qui lui correspond d'après le (B) des
définitions ci-dessus.

Dans les questions (3) à (8) qui suivent, on cherche à démontrer que
$F$ a la propriété\footnote{Si on sait ce que cela signifie, cette
propriété peut s'exprimer ainsi : $F$ est continue (ou, ce qui revient
ici au même : localement constante) lorsque $\mathsf{TotCalc}$ est
muni de la topologie [héritée de la topologie] produit sur
$\mathbb{N}^{\mathbb{N}}$.} suivante (« théorème de
Kreisel-Lacombe-Shoenfield ») : quelle que soit $g \in
\mathsf{TotCalc}$, il existe $n$ telle que pour toute fonction $g' \in
\mathsf{TotCalc}$ qui coïncide avec $g$ jusqu'au rang $n$ (i.e. :
$\forall i\leq n.\,(g'(i) = g(i))$) on ait $F(g') = F(g)$.

\medskip

\textbf{Notations :} Soit $\mathsf{NulAPCR}$ l'ensemble des fonctions
$h\colon\mathbb{N}\to\mathbb{N}$ qui sont nulles à partir d'un certain
rang, c'est-à-dire telles que $\exists m. \forall i\geq m.\,(h(i) =
0)$.

\medskip

\textbf{(3)} \textbf{(a)} Expliquer pourquoi $\mathsf{NulAPCR}
\subseteq \mathsf{TotCalc}$, i.e., pourquoi toute fonction
$\mathbb{N}\to\mathbb{N}$ nulle à partir d'un certain rang est
automatiquement calculable.\quad\textbf{(b)} Montrer, plus
précisément, qu'il existe une fonction calculable $\Gamma\colon
\mathbb{N}\times\mathbb{N}\to\mathbb{N}$ telle que les fonctions $h
\in \mathsf{NulAPCR}$ soient exactement celles de la forme
$\Gamma(j,\emdash)$ (c'est-à-dire $i \mapsto \Gamma(j,i)$) pour un
certain $j$.  (\emph{Indication :} on pourra utiliser un codage de
Gödel des suites finies d'entiers naturels par des entiers
naturels $j$ ; on ne demande pas de justifier les détails de ce
codage.)\quad\textbf{(c)} En déduire qu'il existe $\gamma\colon
\mathbb{N}\to\mathbb{N}$ calculable telle que les fonctions de
$\mathsf{NulAPCR}$ soient exactement celles de la forme
$\varphi_{\gamma(j)}$ pour un certain $j$.  (\emph{Indication :} on
pourra utiliser le théorème s-m-n.)

\begin{corrige}
\textbf{(a)} Si on a $h(i) = 0$ pour $i\geq m$, alors $h$ est
trivialement calculable par le programme « si $i=0$, renvoyer $h(0)$,
si $i=1$ renvoyer $h(1)$, ..., si $i=m-1$ renvoyer $h(m-1)$, et si
$i\geq m$ renvoyer $0$ ».

\textbf{(b)} On considère le programme qui, donné deux entiers $j,i$
effectue les opérations suivantes : il décode $j$ comme le codage de
Gödel $\dbllangle a_0,\ldots,a_{m-1}\dblrangle$ d'un $m$-uplet
$(a_0,\ldots,a_{m-1})$ d'entiers naturels, puis, si $i<m$, renvoie
$a_i$, et sinon, renvoie $0$.  Ce programme calcule une fonction
$\Gamma\colon \mathbb{N}\times\mathbb{N}\to\mathbb{N}$.  Et par
construction, chaque fonction $\Gamma(j,\emdash)$ est nulle à partir
d'un certain rang, et chaque fonction $h$ qui est nulle à partir du
rang $m$ est de la forme $\Gamma(j,\emdash)$, à savoir pour $j =
\dbllangle h(0),\ldots,h(m-1)\dblrangle$.

\textbf{(c)} Le théorème s-m-n assure qu'on peut calculer le code
$\gamma(j)$ d'un programme calculant $\Gamma(j,\emdash)$ de manière
calculable à partir de $j$.  (De façon extrêmement précise : si $p$
est un code tel que $\varphi^{(2)}_p(j,i) = \Gamma(j,i)$, alors
$\varphi^{(1)}_{s_{1,1}(p,j)}(i) = \varphi^{(2)}_p(j,i) =
\Gamma(j,i)$, donc $\gamma(j) := s_{1,1}(p,j)$ convient au sens où
$\varphi_{\gamma(j)} = \Gamma(j,\emdash)$.  La fonction $\gamma$ est
bien calculable car $s_{1,1}$ l'est ; elle est même primitive
récursive.)
\end{corrige}

\medskip

\textbf{Notations :} Si $g \in \mathsf{TotCalc}$ et $n\in\mathbb{N}$,
on appellera $\mathcal{B}(g,n) := \{g' \in \mathsf{TotCalc} : \forall
i\leq n.\,(g'(i) = g(i))\}$ l'ensemble des $g'$ qui coïncident avec
$g$ jusqu'au rang $n$, et $\mathcal{B}_0(g,n) := \mathcal{B}(g,n) \cap
\mathsf{NulAPCR}$ celles qui, en outre, sont nulles à partir d'un
certain rang (c'est-à-dire les fonctions prenant des valeurs de la
forme $g(0),g(1),\ldots,g(n),?,?,\ldots,?,0,0,0,\ldots$).

\smallskip

(On rappelle que notre but est de montrer qu'il existe $n$ tel que $F$
soit constante sur $\mathcal{B}(g,n)$.)

\medskip

\textbf{(4)} Soit $g \in \mathsf{TotCalc}$ et $n\in\mathbb{N}$.
Expliquer \emph{brièvement} pourquoi les conclusions de la
question (3) valent encore en remplaçant $\mathsf{NulAPCR}$ par
$\mathcal{B}_0(g,n)$ partout.  (\emph{Indication :} on peut par
exemple fabriquer un élément de $\mathcal{B}_0(g,n)$ en insérant les
valeurs $g(0),\ldots,g(n)$ avant un élément de $\mathsf{NulAPCR}$.)
On notera $\gamma(g,n,j)$ la conclusion de la dernière sous-question,
c'est-à-dire que les fonctions $h \in \mathcal{B}_0(g,n)$ soient
exactement celles de la forme $h = \varphi_{\gamma(g,n,j)}$ pour un
certain $j$.  On expliquera \emph{brièvement} pourquoi $\gamma(g,n,j)$
est calculable en fonction de $j$, de $n$ et du code (dans
$\mathsf{TotCode}$) d'un programme calculant $g$.

\begin{corrige}
En (3)(b), on a vu qu'on pouvait fabriquer n'importe quel élément de
$\mathsf{NulAPCR}$ en prenant le codage $j$ d'un $m$-uplet qu'on étend
en la fonction qui commence par ces $m$ valeurs puis une infinité de
zéros.  Pour obtenir tous les éléments de $\mathcal{B}_0(g,n)$, il
suffit par exemple d'insérer $g(0),\ldots,g(n)$ avant les valeurs
codées par $j$.  Il faut simplement justifier que le calcul des
valeurs $g(0),\ldots,g(n)$ (ou du tuple de ces valeurs) est faisable
en fonction de $n$ et du code d'un programme calculant $g$, or c'est
clair (par l'existence d'un programme universel).
\end{corrige}

\medskip

Si on n'a pas su traiter les questions (3) et/ou (4), pour la suite,
\textbf{on retiendra juste ceci :} $\gamma(g,n,j)$ est calculable, et
on a $\mathcal{B}_0(g,n) = \{\varphi_{\gamma(g,n,j)} \,:\,
j\in\mathbb{N}\}$.

\medskip

\textbf{Algorithme A :} Pour $g \in \mathsf{TotCalc}$, on considère
maintenant le programme prenant deux entrées $d$ et $\ell$, décrit
informellement ainsi :
\begin{itemize}
\item lancer l'exécution de $\varphi_d(0)$ pour au plus $\ell$
  étapes\footnote{Si on préfère la notion d'arbre de calcul, remplacer
  par : « rechercher parmi les entiers $n\leq\ell$ le code d'un arbre
  de calcul de $\varphi_d(0)$ », et de même plus loin, remplacer
  « l'exécution s'est terminée en exactement $n\leq\ell$ étapes » par
  « $n$ est le code d'un arbre de calcul de $\varphi_d(0)$ ».  Cela ne
  changera rien au problème.} ;
\item si l'exécution ne s'est pas terminée dans le temps imparti,
  terminer en renvoyant la valeur $g(\ell)$ ;
\item sinon, disons si l'exécution s'est terminée en exactement
  $n\leq\ell$ étapes, lancer une boucle non bornée pour rechercher un
  $j \in \mathbb{N}$ tel que\footnote{On rappelle à toutes fins utiles
que $\hat F(\gamma(g,n,j)) = F(\varphi_{\gamma(g,n,j)})$ (c'est la
définition de $\hat F$).} $\hat F(\gamma(g,n,j)) \neq F(g)$ :
\begin{itemize}
\item si un tel $j$ est trouvé, on renvoie
  $\varphi_{\gamma(g,n,j)}(\ell)$,
\item sinon, bien sûr, l'algorithme ne termine pas.
\end{itemize}
\end{itemize}

\medskip

On notera $g_d(\ell)$ la valeur calculée par cet algorithme A (s'il
termine).

\medskip

\textbf{(5)} \textbf{(a)} Justifier que les opérations présentées dans
l'algorithme A ont bien un sens (i.e., que c'est bien un algorithme,
qu'on a bien défini une fonction $\mathbb{N}\times\mathbb{N}
\dasharrow \mathbb{N}$ partielle calculable $(d,\ell) \mapsto
g_d(\ell)$).\quad\textbf{(b)} En déduire qu'il existe une fonction
calculable totale $e \mapsto e_d$ telle que $g_d = \varphi_{e_d}$ pour
tout $d$.

\begin{corrige}
\textbf{(a)} Parmi les points pouvant mériter d'être justifiés :
\begin{itemize}
\item il est bien possible de lancer l'exécution de $\varphi_d(0)$
  pour au plus $\ell$ étapes (programme universel avec limite de temps
  / théorème de la forme normale de Kleene) ;
\item renvoyer $g(\ell)$ ne pose pas de problème car $g$ est
  calculable ;
\item calculer $\hat F(\gamma(g,n,j))$ est possible car $\gamma$ est
  calculable (question (4)) et $\hat F$ l'est (par définition de la
  calculabilité de $F$) ;
\item calculer $F(g)$ est possible, là aussi car $F$ est calculable
  (note : à la limite, ce point se passe de justification car $F(g)$
  est de toute façon une constante dans notre programme, sauf si on
  fait varier $g$, ce qui ne sera le cas qu'à la question (9)) ;
\item on a bien le droit de faire une boucle non bornée sur $j$ par
  l'opérateur $\mu$ de Kleene ;
\item calculer $\varphi_{\gamma(g,n,j)}(\ell)$ est possible car
  $\gamma$ est calculable (et en utilisant un programme universel pour
  le $\varphi$) ; d'ailleurs, ce calcul termine forcément car
  $\varphi_{\gamma(g,n,j)}$ est une fonction totale par définition
  de $\gamma(g,n,j)$.
\end{itemize}

\textbf{(b)} On utilise le théorème s-m-n exactement comme en (3)(c) :
dès lors que $(d,\ell) \mapsto g_d(\ell)$ est caclulable, on en déduit
une fonction $d \mapsto e_d$ calculable (totale ! et même primitive
récursive, à savoir $e_d = s_{1,1}(q,d)$ où $q$ est tel que $g_d(\ell)
= \varphi^{(2)}_q(d,\ell)$) vérifiant $g_d = \varphi_{e_d}$.
\end{corrige}

\medskip

\textbf{(6)} Soit $\mathscr{H} := \{d\in\mathbb{N} :
\varphi_d(0){\downarrow}\}$ l'ensemble des $d$ tels que l'exécution de
$\varphi_d(0)$ termine.\quad\textbf{(a)} Lorsque
$d\not\in\mathscr{H}$, que vaut $g_d$ ? et du coup, que vaut $\hat
F(e_d)$ ?\quad\textbf{(b)} Montrer que $\{d\in\mathbb{N} : \hat F(e_d)
= F(g)\}$ est semi-décidable.\quad\textbf{(c)} Le complémentaire
$\complement\mathscr{H} = \{d\in\mathbb{N} : \varphi_d(0)\uparrow\}$
de $\mathscr{H}$ est-il semi-décidable ?\quad\textbf{(d)} En déduire
qu'il existe $d\in\mathscr{H}$ tel que $\hat F(e_d) = F(g)$.

\begin{corrige}
\textbf{(a)} Si $d\not\in\mathscr{H}$, alors dans l'algorithme A, on
est toujours dans le cas « l'exécution ne s'est pas terminée dans le
temps imparti », donc $g_d(\ell)$ pour tout $\ell$, c'est-à-dire que
$g_d = g$ (et notamment, $g_d$ est \emph{totale}).  Par conséquent,
$\hat F(e_d) = F(g_d) = F(g)$ (par extensionnalité).

\textbf{(b)} Pour semi-décider si $\hat F(e_d) = F(g)$, il suffit de
lancer le calcul de $\hat F(e_d)$ et, si celle-ci termine, comparer
son résultat à $F(g)$ et renvoyer vrai si c'est le cas (et sinon,
faire une boucle infinie).

(On notera que le calcul de $\hat F(e_d)$ ne termine pas forcément,
parce qu'on n'a pas la certitude que $e_d \in \mathsf{TotCode}$ vu
qu'on ne sait pas si $g_d$ est totale.)

\textbf{(c)} L'ensemble $\mathscr{H}$ n'est pas décidable (c'est une
variante du problème de l'arrêt, ou bien on peut invoquer le théorème
de Rice) ; or il est clairement semi-décidable.  Donc
$\complement\mathscr{H}$ n'est pas semi-décidable.

\textbf{(d)} Supposons par l'absurde qu'on ait $\hat F(e_d) \neq F(g)$
pour tout $d\in\mathscr{H}$ : comme on a vu en (a) que $\hat F(e_d) =
F(g)$ pour tout $d\not\in\mathscr{H}$, on a alors $\{d\in\mathbb{N} :
\hat F(e_d) \neq F(g)\} = \mathscr{H}$, autrement dit
$\{d\in\mathbb{N} : \hat F(e_d) = F(g)\} = \complement\mathscr{H}$, or
on a vu en (b) que $\{d\in\mathbb{N} : \hat F(e_d) = F(g)\}$ est
semi-décidable et en (c) que $\complement\mathscr{H}$ ne l'est pas,
une contradiction.  Donc il doit exister $d\in\mathscr{H}$ tel que
$\hat F(e_d) = F(g)$.
\end{corrige}

\medskip

\textbf{(7)} On a montré en (6) qu'il existe $d$ tel que
$\varphi_d(0){\downarrow}$ et que $\hat F(e_d) = F(g)$.  Soit $n$ le
nombre d'étapes d'exécution\footnote{Ou si on préfère : le code de
l'arbre de calcul.} de $\varphi_d(0)$.  Montrer que pour tout $g' \in
\mathcal{B}_0(g,n)$ on a $F(g') = F(g)$.  (\emph{Indication :} sinon,
la recherche d'un $j$ dans l'algorithme A aurait réussi à trouver
un $j$ : on pourra montrer qu'on aurait $g_d =
\varphi_{\gamma(g,n,j)}$ donc $F(g_d) \neq F(g)$ dans ce cas.)

\begin{corrige}
Supposons par l'absurde que $F(g') \neq F(g)$ pour un certain $g' \in
\mathcal{B}_0(g,n)$.  Comme on l'a vu dans la question (4), on a $g' =
\varphi_{\gamma(g,n,j_0)}$ pour un certain $j_0$, et en particulier,
$F(g') = F(\varphi_{\gamma(g,n,j_0)}) = \hat F(\gamma(g,n,j_0))$ donc
$\hat F(\gamma(g,n,j_0)) \neq F(g)$.  Dans l'exécution de
l'algorithme A, si $\ell\geq n$, on est dans le cas où l'exécution de
$\varphi_d(0)$ s'est terminée dans le temps imparti (par définition
de $n$), et la seconde boucle va trouver un $j$ tel que $\hat
F(\gamma(g,n,j)) \neq F(g)$ (puisqu'il en existe un), pas forcément
$j_0$ mais toujours le même quel que soit $\ell$, appelons-le $j_1$,
et l'algorithme va renvoyer $\varphi_{\gamma(g,n,j_1)}(\ell)$ ; tandis
que si $\ell<n$, alors l'exécution de $\varphi_d(0)$ ne sera terminée
dans le temps imparti et l'algorithme va renvoyer $g(\ell)$, qui est
aussi $\varphi_{\gamma(g,n,j_1)}(\ell)$ puisque $\gamma(g,n,j_1) \in
\mathcal{B}(g,n)$.  Donc dans tous les cas, l'algorithme renvoie
$\varphi_{\gamma(g,n,j_1)}(\ell)$, c'est-à-dire que $g_d =
\varphi_{\gamma(g,n,j_1)}$.  Or la définition de $j_1$ fait que $\hat
F(\gamma(g,n,j_1)) \neq F(g)$, et on a $F(g_d) =
F(\varphi_{\gamma(g,n,j_1)}) = \hat F(\gamma(g,n,j_1))$, ce qui mis
ensemble montre que $F(g_d) \neq F(g)$.  Mais ceci contredit le fait
que $F(g_d) = \hat F(e_d) = F(g)$.  On a bien abouti à une
contradiction.  C'est donc que $F(g') = F(g)$ pour tout $g' \in
\mathcal{B}_0(g,n)$.
\end{corrige}

\medskip

\textbf{(8)} On a montré en (7) que pour tout $g\in\mathsf{TotCalc}$
il existe $n$ tel que pour tout $g' \in \mathcal{B}_0(g,n)$ on a
$F(g') = F(g)$.  On considère maintenant $g' \in \mathcal{B}(g,n)$
(qui n'est plus supposé nul à partir d'un certain rang) : d'après ce
qu'on vient de dire, il existe $n'$ tel que pour tout $g'' \in
\mathcal{B}_0(g',n')$ on a $F(g'') = F(g')$.  En justifiant qu'on peut
trouver $g'' \in \mathcal{B}_0(g,n) \cap \mathcal{B}_0(g',n')$,
montrer que $F(g') = F(g)$.  Conclure.

\begin{corrige}
Renommons en $g''$ le $g'$ de la question (7) pour y voir plus clair :
on a trouvé un $n$ tel que pour tout $g'' \in \mathcal{B}_0(g,n)$ on a
$F(g'') = F(g)$.  Si maintenant $g' \in \mathcal{B}(g,n)$, on trouve
de la même manière $n'$ tel que pour tout $g'' \in
\mathcal{B}_0(g',n')$ on a $F(g'') = F(g')$.  Si $n'' = \max(n,n')$,
alors n'importe quel $g'' \in \mathcal{B}_0(g',n'')$ coïncide avec
$g'$ jusqu'au rang $n''$ donc jusqu'au rang $n'$, et par ailleurs avec
$g'$ jusqu'au rang $n''$ donc jusqu'au rang $n$ donc aussi avec $g$
jusqu'au rang $n$ : ceci montre $g'' \in \mathcal{B}_0(g,n) \cap
\mathcal{B}_0(g',n')$ (en fait, $\mathcal{B}_0(g',n'') \subseteq
\mathcal{B}_0(g,n) \cap \mathcal{B}_0(g',n')$), et on a $F(g'') =
F(g)$ puisque $g'' \in \mathcal{B}_0(g,n)$ et $F(g'') = F(g')$ puisque
$g'' \in \mathcal{B}_0(g',n')$, donc $F(g') = F(g'') = F(g)$.

On a donc bien montré l'existence d'un certain $n$ tel que $F(g') =
F(g)$ pour tout $g' \in \mathcal{B}(g,n)$.
\end{corrige}

\medskip

\textbf{(9)} En observant que l'algorithme A peut s'écrire (à $g$
variable) à partir du code d'un programme calculant $g$, justifier
qu'un $n$ dont on a montré l'existence en (8) peut être obtenu de
façon calculable en fonction du code d'un programme calculant $g$.
(On esquissera un algorithme B qui calcule un $n$ en fonction d'un
code $r$ d'un programme calculant $g$.)

\begin{corrige}
Observons d'abord que l'algorithme A peut s'écrire (i.e., « être rendu
uniforme ») à partir du code $r$ d'un programme calculant $g =
\varphi_r$ : on a déjà observé en (4) que c'est le cas
de $\gamma(g,n,j)$, et dans l'algorithme A, on peut remplacer
l'invocation de $g(\ell)$ par $\varphi_r(\ell)$ (calculable au moyen
d'un programme universel), et celle de $F(g)$ par $\hat F(r)$.  Au
moyen du théorème s-m-n (comme on l'a déjà expliqué plusieurs fois
ci-dessus), on en déduit une fonction calculable $(r,d) \mapsto
e_{r,d}$ qui (si $r \in \mathsf{TotCode}$) renvoie le code d'un
$e_{r,d}$ calculé par l'algorithme en question (i.e., un code pour
$g_d$ si $g = \varphi_r$).

Reste maintenant expliquer comment trouver $n$ en fonction de ce $r$.
Pour cela, l'algorithme B sera le suivant.  On parcourt tous les
couples $(d,n)$ (disons, au moyen du code de Gödel $\langle
d,n\rangle$ du couple), et, si $\varphi_d(0)$ termine en exactement
$n$ étapes, on teste si $\hat F(e_{r,d}) = \hat F(r)$ (où $e_{r,d}$
est, comme on vient de le dire, essentiellement la curryfication de
l'algorithme A, et $\hat F$ est donné).  Lorsqu'un $(d,n)$ est trouvé,
on renvoie le $n$ en question.

D'après la question (6) (et le fait que $\hat F(r) = F(g)$), il existe
bien un tel $(d,n)$ comme recherché par l'algorithme B, donc celui-ci
termine.  D'après les question (7) et (8), le $n$ qu'il renvoie
vérifie la propriété demandée.
\end{corrige}

\medskip

\textbf{(10)} On a montré en (3)–(8) le théorème de
Kreisel-Lacombe-Shoenfield qui affirme que
\[
\forall F:\mathsf{TotCalc}\to\mathbb{N}\text{~calculable}.\;
\forall g\in\mathsf{TotCalc}.\;
\exists n\in\mathbb{N}.\;
\forall g'\in\mathcal{B}(g,n).\;
(F(g') = F(g))
\]
Montrer par un exemple simple que l'affirmation suivante\footnote{Ce
serait une affirmation de continuité \emph{uniforme} de $F$.}
\[
\forall F:\mathsf{TotCalc}\to\mathbb{N}\text{~calculable}.\;
\exists n\in\mathbb{N}.\;
\forall g\in\mathsf{TotCalc}.\;
\forall g'\in\mathcal{B}(g,n).\;
(F(g') = F(g))
\]
n'est pas valable.  (\emph{Indication :} proposer une fonction $F$ qui
évalue un nombre de valeurs $g(i)$ de $g$ dépendant, disons,
de $g(0)$.)

\begin{corrige}
On peut par exemple considérer la fonction(nelle) $F$ suivante :
calculer $g(0) =: N$, puis calculer et renvoyer la somme des valeurs
$g(1) + g(2) + \cdots + g(N)$.  Manifestement, $F$ est bien
calculable.  Supposons par l'absurde qu'il existe $n$ tel que $\forall
g\in\mathsf{TotCalc}.\; \forall g'\in\mathcal{B}(g,n).\; (F(g') =
F(g))$.  Considérons la fonction (évidemment calculable) qui vaut
$n+1$ en $0$ et $0$ en tout $i>0$ : ainsi, $F(g) = 0$, donc on devrait
avoir $F(g')$ pour tout $g'\in \mathcal{B}(g,n)$, c'est-à-dire tout
$g'$ tel que $g'(0)=n+1$ et $g'(1)=\cdots=g'(n)=0$.  Or en prenant
$g'$ valant $42$ en $n+1$ et toujours $0$ ensuite, on a $F(g') = 42$,
donc $F(g') \neq F(g)$, ce qui contredit l'affirmation.
\end{corrige}

\medskip

\textbf{(11)} On a prouvé en (9) qu'un $n$ (tel que $\forall
g'\in\mathcal{B}(g,n).\; (F(g') = F(g))$) peut être calculé
algorithmiquement en fonction du code $r$ d'un programme qui
calcule $g$.  En fait, on pourrait prouver un peu mieux (\emph{ceci
n'est pas demandé}) : il est possible de calculer un tel $n$ par un
algorithme qui a seulement le droit d'interroger les
valeurs\footnote{C'est-à-dire : un algorithme qui a accès à un oracle
calculant qui renvoie $g(i)$ quand on lui soumet la valeur $i$.
L'algorithme a le droit d'appeler librement l'oracle un nombre fini
quelconque de fois au cours de son exécution.} de la fonction $g$.  En
\emph{admettant} ce fait, expliquer pourquoi la fonction $F$ elle-même
peut être calculée par un tel algorithme.

\begin{corrige}
Pour la complétude de ce corrigé, et \emph{bien que ce ne soit pas
demandé par le sujet}, prouvons l'affirmation admise.  Appelons $N(r)$
la valeur calculée par l'algorithme B donné dans la question (9),
c'est-à-dire en supposant qu'on ait accès au code $r$ du programme qui
calcule $g$.  On cherche maintenant à faire pareil sans avoir accès à
ce code.  Pour cela, considérons l'algorithme C suivant : on recherche
un $r \in \mathbb{N}$ vérifiant les conditions :
\begin{itemize}
\item $N(r){\downarrow}$,
\item $\varphi_r(i) = g(i)$ pour tout $i \leq N(r)$,
\item $\hat F(\gamma(g,N(r),0)) = \hat F(r)$ ;
\end{itemize}
et une fois qu'il est trouvé, on renvoie $N(r)$.

Un tel $r$ existe bien car si $r_0$ est tel que $\varphi_{r_0} = g$,
alors ce $r_0$ vérifie bien les trois conditions (la première vient de
$r_0 \in \mathsf{TotCode}$, la deuxième est une conséquence triviale
de $\varphi_{r_0} = g$, et la troisième découle du fait que tout $g'
\in \mathcal{B}(g,N(r_0))$ vérifie $F(g') = F(g)$, et que $g' :=
\varphi_{\gamma(g,N(r_0),0)} \in \mathcal{B}_0(g,N(r_0))$ donc $\hat
F(\gamma(g,N(r),0)) = F(g') = F(g) = \hat F(r_0)$).

La recherche d'un $r$ est possible algorithmiquement bien que les
trois contraintes ne soient que semi-décidables (le calcul de
$\varphi_r(i)$ pourrait ne pas terminer, comme celui de $N(r)$ ou de
$\hat F(r)$, puisque rien ne garantit que $r \in \mathsf{TotCode}$) :
en effet, on peut à lancer en parallèle toutes les recherches
(c'est-à-dire qu'on parcourt les couples $(r,M)$ et pour chacun on
fait $M$ étapes de la vérification que $r$ convient, jusqu'à trouver
un $r$ qui vérifie les contraintes).

L'algorithme C qu'on vient de dire n'utilise que l'interrogation de
valeurs de $g$ (c'est trivial pour le premier point qui ne fait pas
intervenir $g$, pour le deuxième le test se fait en utilisant les
valeurs $g(0),\ldots,g(N(r))$, et pour le troisième, il est clair dans
la construction faite en (4) que pour déterminer $\gamma(g,n,j)$ on
n'a besoin que d'interroger les valeurs de $g$, pas d'avoir accès à
son code).

Une fois qu'un tel $r$ est trouvé, même sans supposer que la fonction
$\varphi_r$ soit totale, l'argument donné en (7) montre qu'on ne peut
pas y avoir de $j$ tel que $\hat F(\gamma(g,N(r),j)) \neq \hat F(r)$,
donc comme en (8), on a $F(g') = \hat F(r)$ pour tout $g' \in
\mathcal{B}(g,N(r))$, et $N(r)$ vérifie bien la contrainte demandée.

Ceci conclut la preuve du fait qui était admis.  Passons maintenant à
la question proprement dite.

Pour calculer $F(g)$ à partir de l'interrogation de valeurs de $g$, on
commence par calculer, en interrogeant les valeurs de $g$, un $n$ tel
que $\forall g'\in\mathcal{B}(g,n).\; (F(g') = F(g))$ (on vient
d'admettre ou d'expliquer qu'on peut le faire).  Puis on calcule et
renvoie $\hat F(\gamma(g,n,0))$, ce qui peut se faire en
n'interrogeant qu'un nombre fini de valeurs de $g$ (à savoir
$g(0),\ldots,g(n)$) : comme $\gamma(g,n,0) \in \mathcal{B}(g,n)$ par
définition de $\gamma$, on a bien $\hat F(\gamma(g,n,0)) = F(g)$, et
on a calculé cette valeur en passant simplement par l'interrogation de
valeurs de $g$ et sans avoir besoin de connaître son code.
\end{corrige}

\medskip

\textbf{(12)} Quelle est la morale de l'ensemble de ce problème ?
Autrement dit, expliquer \emph{en français de façon informelle} le
sens du théorème de Kreisel-Lacombe-Shoenfield : on cherchera à dire
quelque chose de la forme « la seule manière de construire une
fonction totale calculable sur l'ensemble des fonctions est la
suivante ».  On contrastera avec la situation des
questions (1) et (2).

\begin{corrige}
On s'est interrogé dans ce problème sur ce que peuvent faire des
algorithmes qui prennent en entrée un autre programme et qui calculent
un entier.  Dans la question (1), on a vu, comme variation sur le
théorème de Rice, que si le programme fourni en entrée de l'algorithme
n'est pas supposé terminer à coup sûr, alors on ne peut rien faire
d'intelligent : on ne peut que renvoyer toujours la même valeur.

En revanche, lorsque l'algorithme fourni en entrée est supposé
toujours terminer, on peut au moins évaluer ses valeurs (c'est ce
qu'on a fait dans la question (2)), c'est-à-dire qu'on peut renvoyer
des expressions faisant intervenir les $g(i)$.  Ce qu'affirme le
théorème de Kreisel-Lacombe-Shoenfield, c'est que toute valeur $F(g)$
calculée ne dépend, en fait, que d'un nombre fini de telles valeurs
$g(0),\ldots,g(n)$, et, finalement (c'est la question (11)) peut être
calculé par un algorithme qui n'a le droit d'accéder qu'à une boîte
noire renvoyant la valeur de $g(i)$ en fonction de $i$.

La question (10) montre que, si pour n'importe quel $g$ le nombre de
valeurs dont dépend $F(g)$ est borné, il n'est pas forcément
\emph{uniformément borné}, c'est-à-dire qu'on ne peut pas forcément
trouver un seul et même $n$ tel que la connaissance des $n$ premières
valeurs de $g$ suffise à calculer $F(g)$.
\end{corrige}



%
%
%
\end{document}