From 4e97c27fce39b69af4f4e192393d51b0bff6847e Mon Sep 17 00:00:00 2001 From: "David A. Madore" Date: Tue, 21 Jan 2025 19:58:30 +0100 Subject: Start writing test for 2025-01-29. --- controle-20250129.tex | 245 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 245 insertions(+) create mode 100644 controle-20250129.tex (limited to 'controle-20250129.tex') diff --git a/controle-20250129.tex b/controle-20250129.tex new file mode 100644 index 0000000..b268a5f --- /dev/null +++ b/controle-20250129.tex @@ -0,0 +1,245 @@ +%% 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.} + +\textcolor{red}{À revoir.} + +Les exercices et le problème sont totalement indépendants. Ils +pourront être traités dans un ordre quelconque, mais on demande de +faire apparaître de façon très visible dans les copies où commence +chaque exercice (tirez au moins un trait sur toute la largeur de la +feuille entre deux exercices). + +Les questions du problème dépendent les unes des autres, mais ont été +rédigées de manière à ce que chacune donne toutes les informations +nécessaires pour passer à la suite. Mais comme elles (les questions +du problème) présentent une gradation approximative de difficulté, il +est recommandé de les traiter dans l'ordre. + +La longueur du sujet ne doit pas effrayer : l'énoncé du problème est +très long parce que des rappels ont été faits et que les questions ont +été rédigées de façon aussi précise que possible. Par ailleurs, il ne +sera pas nécessaire de tout traiter pour avoir le maximum des points. + +\medbreak + +L'usage de tous les documents écrits (notes de cours manuscrites ou +imprimées, feuilles d'exercices, livres) est autorisé. + +L'usage des appareils électroniques est interdit. + +\medbreak + +Durée : 3h + +Barème \emph{approximatif} et \emph{indicatif} (sur $20$) : +\textcolor{red}{à écrire}. + +\ifcorrige +Ce corrigé comporte \textcolor{red}{à compléter} pages (page de garde incluse). +\else +Cet énoncé comporte \textcolor{red}{à compléter} 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 + + +% +% +% + +\bigbreak + +\exercice[Problème] + +\textbf{Notations :} Dans cet exercice, on notera comme d'habitude +$\varphi_e\colon\mathbb{N}\dasharrow\mathbb{N}$ la $e$-ième fonction +générale récursive (i.e., calculable) pour $e\in\mathbb{N}$. 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{TotIdx} := \{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{TotIdx}\} += \{g\colon\mathbb{N}\to\mathbb{N} \; : \; +\exists e\in\mathbb{N}.\,(g = \varphi_e)\} +\] +l'ensemble 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 de +fonction \emph{totales} $\mathsf{PartCalc} \to \mathbb{N}$ d'une part, +et $\mathsf{TotCalc} \to \mathbb{N}$ d'autre part. + +\medskip + +\textbf{Définition :} (A) Une fonction (totale !) $F\colon +\mathsf{PartCalc} \to \mathbb{N}$ est dite \emph{calculable} lorsqu'il +existe une fonction calculable $\hat F\colon \mathbb{N} \to +\mathbb{N}$ telle que $\hat F(e) = F(\varphi_e)$ pour tout $e \in +\mathbb{N}$.\quad (B) De même, une fonction (totale) $F\colon +\mathsf{TotCalc} \to \mathbb{N}$ est dite calculable lorsqu'il existe +une fonction calculable $\hat F\colon \mathsf{TotIdx} \to \mathbb{N}$ +telle que $\hat F(e) = F(\varphi_e)$ pour tout $e \in +\mathsf{TotIdx}$. + +\smallskip + +En français : une fonctionnelle définie sur l'ensemble des fonctions +calculables partielles ou partielles est elle-même dite calculable +lorsqu'il existe un programme qui calcule $F(g)$ à partir du code $e$ +d'un programme calculant $g$. + +{\footnotesize + +Il est évident 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é » ; et de même, se donner une fonction +$F\colon \mathsf{TotCalc} \to \mathbb{N}$ revient exactement à se +donner une fonction $\hat F\colon \mathsf{TotIdx} \to \mathbb{N}$ qui +soit extensionnelle. La définition ci-dessus dit donc que $F$ est +calculable losrque la $\hat F$ qui lui correspond est elle-même +calculable. + +\par} + +\medskip + +\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., $\hat F(e) = v_1$). (Pourquoi +est-il décidable ? Et pourquoi est-ce une contradiction ?) + +\medskip + +\textbf{(2)} Expliquer pourquoi il existe des fonctions calculables +(totales) $F\colon \mathsf{TotCalc} \to \mathbb{N}$ qui ne sont pas +constantes. + +Pour cela, on pourra penser évaluer en un point, c'est-à-dire +exécuter, le programme qu'on a reçu en argument (on rappellera +pourquoi on peut faire cela). + +\medskip + +Fixons maintenant une fonction calculable $F\colon \mathsf{TotCalc} +\to \mathbb{N}$. On cherche à démontrer qu'elle a la propriété +suivante (« théorème de Kreisel-Lacombe-Shoenfield ») : quelle que +soit $g \in \mathsf{TotCalc}$, il existe $n_0$ telle que pour toute +fonction $g' \in \mathsf{TotCalc}$ qui coïncide avec $g$ jusqu'au rang +$n_0$ (i.e. : $\forall i\leq n_0.\,(g'(i) = g(i))$) on ait $F(g') = +F(g)$. + + + +% +% +% +\end{document} -- cgit v1.2.3 From 7d1dd5fa98eb7c0ff8f3f557d08aaf9bd871bfaa Mon Sep 17 00:00:00 2001 From: "David A. Madore" Date: Wed, 22 Jan 2025 12:52:15 +0100 Subject: Continue writing test (proof of the Kreisel-Lacombe-Shoenfield theorem). --- controle-20250129.tex | 200 +++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 172 insertions(+), 28 deletions(-) (limited to 'controle-20250129.tex') diff --git a/controle-20250129.tex b/controle-20250129.tex index b268a5f..37001d5 100644 --- a/controle-20250129.tex +++ b/controle-20250129.tex @@ -131,10 +131,10 @@ Git: \input{vcline.tex} \exercice[Problème] -\textbf{Notations :} Dans cet exercice, on notera comme d'habitude -$\varphi_e\colon\mathbb{N}\dasharrow\mathbb{N}$ la $e$-ième fonction -générale récursive (i.e., calculable) pour $e\in\mathbb{N}$. On -notera +\textbf{Notations :} Dans tout cet exercice, on notera comme +d'habitude $\varphi_e\colon\mathbb{N}\dasharrow\mathbb{N}$ la $e$-ième +fonction générale récursive (i.e., calculable) partielle pour +$e\in\mathbb{N}$. On notera \[ \mathsf{PartCalc} := \{\varphi_e \; : \; e\in\mathbb{N}\} = \{g\colon\mathbb{N}\dasharrow\mathbb{N} \; : \; @@ -172,21 +172,22 @@ et $\mathsf{TotCalc} \to \mathbb{N}$ d'autre part. \medskip \textbf{Définition :} (A) Une fonction (totale !) $F\colon -\mathsf{PartCalc} \to \mathbb{N}$ est dite \emph{calculable} lorsqu'il -existe une fonction calculable $\hat F\colon \mathbb{N} \to -\mathbb{N}$ telle que $\hat F(e) = F(\varphi_e)$ pour tout $e \in -\mathbb{N}$.\quad (B) De même, une fonction (totale) $F\colon -\mathsf{TotCalc} \to \mathbb{N}$ est dite calculable lorsqu'il existe -une fonction calculable $\hat F\colon \mathsf{TotIdx} \to \mathbb{N}$ -telle que $\hat F(e) = F(\varphi_e)$ pour tout $e \in -\mathsf{TotIdx}$. +\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{TotIdx}$. \smallskip En français : une fonctionnelle définie sur l'ensemble des fonctions calculables partielles ou partielles est elle-même dite calculable lorsqu'il existe un programme qui calcule $F(g)$ à partir du code $e$ -d'un programme calculant $g$. +d'un programme quelconque calculant $g$. + +\smallskip {\footnotesize @@ -200,10 +201,11 @@ de justifier ce fait, qui est facile), se donner une fonction $F\colon fonction $\hat F\colon \mathbb{N} \to \mathbb{N}$ ayant cette propriété d'« extensionnalité » ; et de même, se donner une fonction $F\colon \mathsf{TotCalc} \to \mathbb{N}$ revient exactement à se -donner une fonction $\hat F\colon \mathsf{TotIdx} \to \mathbb{N}$ qui -soit extensionnelle. La définition ci-dessus dit donc que $F$ est -calculable losrque la $\hat F$ qui lui correspond est elle-même -calculable. +donner une fonction $\hat F\colon \mathsf{TotIdx} \dasharrow +\mathbb{N}$ qui soit extensionnelle. 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 la restriction à +$\mathsf{TotIdx}$ d'une fonction calculable dans le cas (B). \par} @@ -214,29 +216,171 @@ calculable. 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., $\hat F(e) = v_1$). (Pourquoi -est-il décidable ? Et pourquoi est-ce une contradiction ?) +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 ?) \medskip \textbf{(2)} Expliquer pourquoi il existe des fonctions calculables (totales) $F\colon \mathsf{TotCalc} \to \mathbb{N}$ qui ne sont pas -constantes. +constantes. Donner un exemple explicite. Pour cela, on pourra penser évaluer en un point, c'est-à-dire -exécuter, le programme qu'on a reçu en argument (on rappellera -pourquoi on peut faire cela). +exécuter, le programme dont on a reçu le code en argument (on +rappellera pourquoi on peut faire cela). \medskip Fixons maintenant une fonction calculable $F\colon \mathsf{TotCalc} -\to \mathbb{N}$. On cherche à démontrer qu'elle a la propriété -suivante (« théorème de Kreisel-Lacombe-Shoenfield ») : quelle que -soit $g \in \mathsf{TotCalc}$, il existe $n_0$ telle que pour toute -fonction $g' \in \mathsf{TotCalc}$ qui coïncide avec $g$ jusqu'au rang -$n_0$ (i.e. : $\forall i\leq n_0.\,(g'(i) = g(i))$) on ait $F(g') = -F(g)$. +\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 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 toute fonction $h +\in \mathsf{NulAPCR}$ soit 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$.)\quad\textbf{(c)} En déduire qu'il existe $\gamma\colon +\mathbb{N}\to\mathbb{N}$ calculable telle que toute fonction $h \in +\mathsf{NulAPCR}$ soit de la forme $\varphi_{\gamma(j)}$ pour un +certain $j$. (\emph{Indication :} on pourra utiliser le théorème +s-m-n.) + +\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 les valeurs +$g(0),g(1),\ldots,g(n),?,?,\ldots,?,0,0,0,\ldots$). + +\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. On notera $\gamma(g,n,j)$ la conclusion +de la dernière sous-question, c'est-à-dire que toute fonction $h \in +\mathcal{B}_0(g,n)$ soit 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{TotIdx}$) d'un programme calculant $g$. + +\medskip + +Si on n'a pas su traiter la question (4), pour les questions +suivantes, \textbf{on retiendra juste ceci :} $\gamma(g,n,j)$ est +calculable, et toute fonction $\mathcal{B}_0(g,n)$ est de la forme +$\varphi_{\gamma(g,n,j)}$ pour un certain $j$. + +\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$ 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 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$. (\emph{Indication :} on pourra utiliser le théorème s-m-n.) + +\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)$. + +\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 : 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 trouvé un $j$ et on +aurait $g_d = \varphi_{\gamma(g,n,j)}$.) + +\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. + +\medskip +\textbf{(9)} En observant que l'algorithme A peut s'écrire à partir du +code d'un programme calculant $g$, justifier que le $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$. % -- cgit v1.2.3 From 8ba00e19547b48a39afa449982850a1e66f058cc Mon Sep 17 00:00:00 2001 From: "David A. Madore" Date: Wed, 22 Jan 2025 19:27:43 +0100 Subject: Answer key (on the Kreisel-Lacombe-Shoenfield theorem). --- controle-20250129.tex | 518 +++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 449 insertions(+), 69 deletions(-) (limited to 'controle-20250129.tex') diff --git a/controle-20250129.tex b/controle-20250129.tex index 37001d5..e2a28c3 100644 --- a/controle-20250129.tex +++ b/controle-20250129.tex @@ -132,9 +132,9 @@ Git: \input{vcline.tex} \exercice[Problème] \textbf{Notations :} Dans tout cet exercice, on notera comme -d'habitude $\varphi_e\colon\mathbb{N}\dasharrow\mathbb{N}$ la $e$-ième -fonction générale récursive (i.e., calculable) partielle pour -$e\in\mathbb{N}$. On notera +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} \; : \; @@ -143,7 +143,7 @@ $e\in\mathbb{N}$. On notera l'ensemble des fonctions \emph{partielles} calculables $\mathbb{N}\dasharrow\mathbb{N}$, ainsi que \[ -\mathsf{TotIdx} := \{e\in\mathbb{N} \; : \; +\mathsf{TotCode} := \{e\in\mathbb{N} \; : \; \varphi_e\hbox{~est totale}\} = \{e\in\mathbb{N} \; : \; \varphi_e\in\mathsf{TotCalc}\} \] @@ -151,11 +151,11 @@ 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{TotIdx}\} +\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 des fonctions \emph{totales} calculables +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. @@ -165,9 +165,9 @@ 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 de -fonction \emph{totales} $\mathsf{PartCalc} \to \mathbb{N}$ d'une part, -et $\mathsf{TotCalc} \to \mathbb{N}$ d'autre part. +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 @@ -178,12 +178,12 @@ 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{TotIdx}$. +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 partielles est elle-même dite calculable +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$. @@ -191,25 +191,28 @@ d'un programme quelconque calculant $g$. {\footnotesize -Il est évident 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é » ; et de même, se donner une fonction -$F\colon \mathsf{TotCalc} \to \mathbb{N}$ revient exactement à se -donner une fonction $\hat F\colon \mathsf{TotIdx} \dasharrow -\mathbb{N}$ qui soit extensionnelle. 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 la restriction à -$\mathsf{TotIdx}$ d'une fonction calculable dans le cas (B). +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} -\medskip +\bigskip \textbf{(1)} Montrer que toute fonction (totale !) calculable $F\colon \mathsf{PartCalc} \to \mathbb{N}$ est en fait constante. @@ -219,6 +222,23 @@ 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 @@ -227,7 +247,28 @@ 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). +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 @@ -238,9 +279,10 @@ 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 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 +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. : @@ -260,16 +302,45 @@ rang, c'est-à-dire telles que $\exists m. \forall i\geq m.\,(h(i) = $\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 toute fonction $h -\in \mathsf{NulAPCR}$ soit 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$.)\quad\textbf{(c)} En déduire qu'il existe $\gamma\colon -\mathbb{N}\to\mathbb{N}$ calculable telle que toute fonction $h \in -\mathsf{NulAPCR}$ soit de la forme $\varphi_{\gamma(j)}$ pour un -certain $j$. (\emph{Indication :} on pourra utiliser le théorème -s-m-n.) +\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 $i0$ : 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} + % -- cgit v1.2.3 From 1478193b7e48e26994a477cddfcc406f221e813b Mon Sep 17 00:00:00 2001 From: "David A. Madore" Date: Wed, 22 Jan 2025 19:39:22 +0100 Subject: Incorporate Coq exercises provided by TZ. --- controle-20250129.tex | 364 +++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 363 insertions(+), 1 deletion(-) (limited to 'controle-20250129.tex') diff --git a/controle-20250129.tex b/controle-20250129.tex index e2a28c3..74b2d52 100644 --- a/controle-20250129.tex +++ b/controle-20250129.tex @@ -127,7 +127,369 @@ Git: \input{vcline.tex} % % -\bigbreak +\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} + + +% +% +% + +%% \bigbreak +%% \hbox to\hsize{\hrulefill} +%% \smallskip + +\pagebreak \exercice[Problème] -- cgit v1.2.3 From cb11b339c94a87f634dded0412638843214e6c9c Mon Sep 17 00:00:00 2001 From: "David A. Madore" Date: Wed, 22 Jan 2025 20:21:49 +0100 Subject: Add an exercise on the semantics of the propositional calculus. --- controle-20250129.tex | 93 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 93 insertions(+) (limited to 'controle-20250129.tex') diff --git a/controle-20250129.tex b/controle-20250129.tex index 74b2d52..b78c71c 100644 --- a/controle-20250129.tex +++ b/controle-20250129.tex @@ -481,6 +481,99 @@ Qed. \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} + + + % % % -- cgit v1.2.3 From 00f83611f70ef62eb2287e9800482f6a38f2ad27 Mon Sep 17 00:00:00 2001 From: "David A. Madore" Date: Wed, 22 Jan 2025 20:31:30 +0100 Subject: Instructions for test. --- controle-20250129.tex | 21 ++++++++++++--------- 1 file changed, 12 insertions(+), 9 deletions(-) (limited to 'controle-20250129.tex') diff --git a/controle-20250129.tex b/controle-20250129.tex index b78c71c..825e326 100644 --- a/controle-20250129.tex +++ b/controle-20250129.tex @@ -73,13 +73,11 @@ \noindent\textbf{Consignes.} -\textcolor{red}{À revoir.} - -Les exercices et le problème sont totalement indépendants. Ils -pourront être traités dans un ordre quelconque, mais on demande de -faire apparaître de façon très visible dans les copies où commence -chaque exercice (tirez au moins un trait sur toute la largeur de la -feuille entre deux exercices). +Les 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 @@ -94,6 +92,11 @@ 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é. @@ -107,9 +110,9 @@ Barème \emph{approximatif} et \emph{indicatif} (sur $20$) : \textcolor{red}{à écrire}. \ifcorrige -Ce corrigé comporte \textcolor{red}{à compléter} pages (page de garde incluse). +Ce corrigé comporte 14 pages \textcolor{red}{(à revérifier)} (page de garde incluse). \else -Cet énoncé comporte \textcolor{red}{à compléter} pages (page de garde incluse). +Cet énoncé comporte 8 pages \textcolor{red}{(à revérifier)} (page de garde incluse). \fi \vfill -- cgit v1.2.3 From 493d2330e0b21ab52b6ee02ca1a0e448fc15d05c Mon Sep 17 00:00:00 2001 From: "David A. Madore" Date: Thu, 23 Jan 2025 10:49:45 +0100 Subject: Clarify syntax with extra parentheses. --- controle-20250129.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'controle-20250129.tex') diff --git a/controle-20250129.tex b/controle-20250129.tex index 825e326..474e0c9 100644 --- a/controle-20250129.tex +++ b/controle-20250129.tex @@ -383,7 +383,7 @@ Dans cet exercice, on donne un terme de preuve Coq et on demande de retrouver le \smallskip -\textbf{(1)} \verb|fun H : A => H| +\textbf{(1)} \verb|fun (H : A) => H| \smallskip @@ -391,7 +391,7 @@ Dans cet exercice, on donne un terme de preuve Coq et on demande de retrouver le \smallskip -\textbf{(3)} \verb|fun (H1 : A -> B) (H2 : ~ B) => (fun H3 : A => H2 (H1 H3))| +\textbf{(3)} \verb|fun (H1 : A -> B) (H2 : ~ B) => (fun (H3 : A) => H2 (H1 H3))| \begin{corrige} \smallskip -- cgit v1.2.3 From 9c36c0cd833617439f24ad7dbac100e8f3f844aa Mon Sep 17 00:00:00 2001 From: "David A. Madore" Date: Thu, 23 Jan 2025 11:25:27 +0100 Subject: Add a question asking for a proof in natural deduction style. --- controle-20250129.tex | 66 +++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 64 insertions(+), 2 deletions(-) (limited to 'controle-20250129.tex') diff --git a/controle-20250129.tex b/controle-20250129.tex index 474e0c9..e5549be 100644 --- a/controle-20250129.tex +++ b/controle-20250129.tex @@ -379,7 +379,7 @@ Parmi les buts suivants, quand peut-on utiliser ce lemme avec la tactique \textt \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. +\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 @@ -393,14 +393,76 @@ Dans cet exercice, on donne un terme de preuve Coq et on demande de retrouver le \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{(1)} $A \Rightarrow A$. +\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} -- cgit v1.2.3 From e82dfc46b414f6a02e2318ea146cd4cab90eb13c Mon Sep 17 00:00:00 2001 From: "David A. Madore" Date: Thu, 23 Jan 2025 14:53:01 +0100 Subject: Various improvements, clarifications and rephrasings suggested by TZ. --- controle-20250129.tex | 61 ++++++++++++++++++++++++++++----------------------- 1 file changed, 33 insertions(+), 28 deletions(-) (limited to 'controle-20250129.tex') diff --git a/controle-20250129.tex b/controle-20250129.tex index e5549be..c5a76cc 100644 --- a/controle-20250129.tex +++ b/controle-20250129.tex @@ -492,7 +492,7 @@ et la voici écrite dans le style « drapeau » : \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). +\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 @@ -669,7 +669,12 @@ $\mathbb{N}\dasharrow\mathbb{N}$, ainsi que \] 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 +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} \; : \; @@ -711,24 +716,23 @@ d'un programme quelconque calculant $g$. {\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}$. +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} @@ -804,7 +808,7 @@ 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}$, 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)$. @@ -885,12 +889,13 @@ 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$. +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 @@ -978,7 +983,7 @@ tout $d$. \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 +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}$. -- cgit v1.2.3 From 18f8b919ef9a330f815431703766f53ae6fd06ad Mon Sep 17 00:00:00 2001 From: "David A. Madore" Date: Thu, 23 Jan 2025 22:39:25 +0100 Subject: Minor changes to test. --- controle-20250129.tex | 21 +++++++++++---------- 1 file changed, 11 insertions(+), 10 deletions(-) (limited to 'controle-20250129.tex') diff --git a/controle-20250129.tex b/controle-20250129.tex index c5a76cc..2c165b0 100644 --- a/controle-20250129.tex +++ b/controle-20250129.tex @@ -86,14 +86,16 @@ 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. +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 -Les exercices 1 à 4 portent sur Coq. L'exercice 5 porte sur le calcul -propositionnel. Le problème final porte sur la calculabilité. +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 @@ -106,13 +108,10 @@ L'usage des appareils électroniques est interdit. 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). +Ce corrigé comporte 15 pages (page de garde incluse). \else -Cet énoncé comporte 8 pages \textcolor{red}{(à revérifier)} (page de garde incluse). +Cet énoncé comporte 8 pages (page de garde incluse). \fi \vfill @@ -575,6 +574,8 @@ 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.) -- cgit v1.2.3