diff options
Diffstat (limited to 'controle-20250129.tex')
| -rw-r--r-- | controle-20250129.tex | 1295 |
1 files changed, 1295 insertions, 0 deletions
diff --git a/controle-20250129.tex b/controle-20250129.tex new file mode 100644 index 0000000..2c165b0 --- /dev/null +++ b/controle-20250129.tex @@ -0,0 +1,1295 @@ +%% 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 et éclaircissements 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 + +Dans les exercices portant sur Coq (exercices 1 à 4), les erreurs de +syntaxe Coq ne seront pas pénalisées tant qu'on comprend clairement +l'intention. + +\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 + +\ifcorrige +Ce corrigé comporte 15 pages (page de garde incluse). +\else +Cet énoncé comporte 8 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 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 + +\textbf{(A)} 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))| + +\smallskip + +\textbf{(B)} Écrire la démonstration décrite par le terme (3) en +déduction naturelle (on donnera l'arbre de preuve ou la présentation +en style drapeau, comme on préfère). + +\begin{corrige} + \smallskip + +\textbf{(A)} \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$. + +\medskip + +\textbf{(B)} Voici la démonstration de (3) écrite en arbre de preuve : +\begin{footnotesize} +\[ +\inferrule*[left={$\Rightarrow$Int}]{ +\inferrule*[Left={$\Rightarrow$Int}]{ +\inferrule*[Left={$\Rightarrow$Int}]{ +\inferrule*[Left={$\Rightarrow$Élim}]{ +\inferrule*[Left={Ax}]{ }{(A \Rightarrow B), \neg B, A \vdash \neg B}\\ +\inferrule*[Right={$\Rightarrow$Élim}]{ +\inferrule*[Left={Ax}]{ }{(A \Rightarrow B), \neg B, A \vdash A\Rightarrow B}\\ +\inferrule*[Right={Ax}]{ }{(A \Rightarrow B), \neg B, A \vdash A} +}{(A \Rightarrow B), \neg B, A \vdash B} +}{(A \Rightarrow B), \neg B, A \vdash \bot} +}{(A \Rightarrow B), \neg B \vdash A \Rightarrow \bot} +}{A \Rightarrow B \vdash \neg B \Rightarrow \neg A} +}{\vdash (A \Rightarrow B) \Rightarrow \neg B \Rightarrow \neg A} +\] +\end{footnotesize} +ou avec uniquement les conclusions de chaque séquent, et en indiquant +les noms comme dans le terme Coq : +\begin{footnotesize} +\[ +\inferrule*[left={$\Rightarrow$Int($H_1$)}]{ +\inferrule*[Left={$\Rightarrow$Int($H_2$)}]{ +\inferrule*[Left={$\Rightarrow$Int($H_3$)}]{ +\inferrule*[Left={$\Rightarrow$Élim}]{ +\inferrule*[Left={$H_2$}]{ }{\neg B}\\ +\inferrule*[Right={$\Rightarrow$Élim}]{ +\inferrule*[Left={$H_1$}]{ }{A\Rightarrow B}\\ +\inferrule*[Right={$H_3$}]{ }{A} +}{B} +}{\bot} +}{A \Rightarrow \bot} +}{\neg B \Rightarrow \neg A} +}{(A \Rightarrow B) \Rightarrow \neg B \Rightarrow \neg A} +\] +\end{footnotesize} +et la voici écrite dans le style « drapeau » : +\bgroup\normalsize +\begin{footnotesize} +\begin{flagderiv}[exercice-3-proof] +\assume{hyp1}{A\Rightarrow B}{} +\assume{hyp2}{\neg B}{} +\assume{hyp3}{A}{} +\step{subconcb}{B}{$\Rightarrow$Élim sur \ref{hyp1} et \ref{hyp3}} +\step{subconcbot}{\bot}{$\Rightarrow$Élim sur \ref{hyp2} et \ref{subconcb}} +\conclude{subconcnega}{A \Rightarrow \bot}{$\Rightarrow$Int de \ref{hyp3} dans \ref{subconcbot}} +\conclude{subconcimp}{\neg B \Rightarrow \neg A}{$\Rightarrow$Int de \ref{hyp2} dans \ref{subconcnega}} +\conclude{subconcimp}{(A \Rightarrow B) \Rightarrow \neg B \Rightarrow \neg A}{$\Rightarrow$Int de \ref{hyp1} dans \ref{subconcimp}} +\end{flagderiv} +\end{footnotesize} +\egroup +\vskip-4ex\leavevmode +\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 quelles 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$.) + +\smallskip + +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)\footnote{Par souci de cohérence, on pourrait aussi vouloir +définir $\mathsf{PartCode} = \mathbb{N}$ comme l'ensemble des codes +des programmes définissant une fonction partielle : nous suivons la +convention que toute erreur dans un programme (même « syntaxique ») +conduit à une valeur non-définie.}, 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 + +Dans le cas (A), la définition implique 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), +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 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$ tel 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}$.) +En particulier : 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 calculable, 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} |