diff options
Diffstat (limited to 'controle-20260126.tex')
| -rw-r--r-- | controle-20260126.tex | 111 |
1 files changed, 59 insertions, 52 deletions
diff --git a/controle-20260126.tex b/controle-20260126.tex index 7ef04e2..7703669 100644 --- a/controle-20260126.tex +++ b/controle-20260126.tex @@ -74,31 +74,29 @@ \noindent\textbf{Consignes.} -\textcolor{red}{(À modifier.)} - -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. +Les exercices 1 à 5 (qui portent sur la logique) et le problème final +(qui porte sur la calculabilité) sont totalement indépendants les uns +des autres. Ils pourront être traités dans un ordre quelconque, mais +on demande de faire apparaître de façon très visible dans les copies +où commence chaque exercice (tirez au moins un trait sur toute la +largeur de la feuille entre deux exercices). \textbf{Le non-respect + de cette consigne pourra être pénalisé.} \medbreak -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. +La longueur du sujet ne doit pas effrayer : les réponses attendues +sont souvent plus courtes que les questions. Notamment, l'énoncé du +problème est long parce que des rappels et éclaircissements ont été +faits et que les questions ont été rédigées de façon aussi précise que +possible. + +\medbreak + +Dans les exercices portant sur Rocq (exercices 1 à 4), les erreurs de +syntaxe Rocq ne seront pas pénalisées tant qu'on comprend clairement +l'intention. De même, quand on demande d'écrire un $\lambda$-terme, +il n'est pas indispensable de suivre exactement les notations +introduites en cours. \medbreak @@ -112,12 +110,12 @@ L'usage des appareils électroniques est interdit. Durée : 3h Barème \emph{approximatif} et \emph{indicatif} (sur $20$) : -\textcolor{red}{(à écrire)}. +2+2+4+3+3+6 \ifcorrige -Ce corrigé comporte \textcolor{red}{(à remplir)} pages (page de garde incluse). +Ce corrigé comporte 11 pages (page de garde incluse). \else -Cet énoncé comporte \textcolor{red}{(à remplir)} pages (page de garde incluse). +Cet énoncé comporte 7 pages (page de garde incluse). \fi \vfill @@ -153,9 +151,10 @@ Dans cet exercice, on considère des paires d'états d'une preuve en Rocq avant A \end{verbatim} -et on veut arriver à l'état suivant : +\noindent et on veut arriver à l'état suivant : \begin{verbatim} + A, B, C : Prop H1 : A /\ B H2 : C ============================ @@ -172,7 +171,7 @@ et on veut arriver à l'état suivant : (A \/ B) /\ C <-> (A /\ C) \/ (A /\ C) \end{verbatim} -et on veut arriver à l'état suivant : +\noindent et on veut arriver à l'état suivant : \begin{verbatim} First subgoal: @@ -200,7 +199,7 @@ Second subgoal: A \/ B \end{verbatim} -et on veut arriver à l'état suivant : +\noindent et on veut arriver à l'état suivant : \begin{verbatim} No more goals. @@ -211,15 +210,17 @@ et on veut arriver à l'état suivant : \textbf{(4)} On part de l'état suivant : \begin{verbatim} + A, B : Prop H1 : A -> B H2 : ~ B ============================ ~A \end{verbatim} -et on veut arriver à l'état suivant : +\noindent et on veut arriver à l'état suivant : \begin{verbatim} + A, B : Prop H1 : A -> B H2 : ~ B H3 : A @@ -238,7 +239,7 @@ et on veut arriver à l'état suivant : n = m \end{verbatim} -et on veut arriver à l'état suivant : +\noindent et on veut arriver à l'état suivant : \begin{verbatim} n, m : nat @@ -257,7 +258,7 @@ et on veut arriver à l'état suivant : n + 0 = n \end{verbatim} -et on veut arriver à l'état suivant : +\noindent et on veut arriver à l'état suivant : \begin{verbatim} First subgoal: @@ -284,7 +285,7 @@ Second subgoal: S n + 0 = S n \end{verbatim} -et on veut arriver à l'état suivant : +\noindent et on veut arriver à l'état suivant : \begin{verbatim} n : nat @@ -304,7 +305,7 @@ et on veut arriver à l'état suivant : S (n + 0) = S n \end{verbatim} -et on veut arriver à l'état suivant : +\noindent et on veut arriver à l'état suivant : \begin{verbatim} n : nat @@ -334,7 +335,6 @@ et on veut arriver à l'état suivant : \textbf{(7)} \verb|simpl.| \textbf{(8)} \verb|f_equal.| (la tactique) ou \verb|apply f_equal.| (le lemme). - \end{corrige} % @@ -516,7 +516,7 @@ forme drapeau), qui vaudra au moins une partie des points. \smallskip -\textbf{(6)} Expliquer comment prouver en Rocq que la taille d'un arbre et la taille de son miroir sont égales. +\textbf{(6)} Expliquer succinctement comment prouver en Rocq que la taille d'un arbre et la taille de son miroir sont égales. \begin{corrige} \smallskip @@ -553,7 +553,9 @@ Fixpoint taille (a : arbre) : nat := end. \end{verbatim} - \textbf{(6)} On énoncerait le lemme \verb|Lemma taille_miroir : forall a : arbre, taille a = taille (miroir a).| + \textbf{(6)} On énoncerait le lemme : + +\verb|Lemma taille_miroir : forall a : arbre, taille a = taille (miroir a).| Pour le prouver, on utilise l'induction structurelle (\texttt{induction a.}). Le cas de base (feuille) se résout par \texttt{reflexivity.} Dans le cas récursif, la simplification calcule la taille du miroir. Les hypothèses d'induction permettent de réécrire les tailles du miroir des sous-arbres. On conclut en utilisant la commutativité de l'addition. @@ -662,10 +664,10 @@ peut pas être démontrable en calcul propositionnel intuitionniste. % % -\exercice +\exercice[Problème] -\textbf{Rappels de quelques définitions habituelles.} On rappelle -qu'un \textbf{mot binaire [fini]} est une suite finie (éventuellement +\textbf{Rappels de quelques définitions et notations habituelles.} On rappelle +qu'un \textbf{mot binaire} est une suite finie (éventuellement vide, c'est-à-dire de longueur nulle) de $0$ et de $1$. On notera $\{0,1\}^* = \{\varepsilon, 0, 1, 00, 01, 10, 11, 000, \ldots\}$ (ici, $\varepsilon$ désigne le mot vide) l'ensemble de tous les mots @@ -701,21 +703,24 @@ lorsque, pour chaque $0 \leq i < |w|$, le bit numéroté $i$ de $w$ vaut attestant $\varphi_i(0) = 0$, \item $1$ s'il existe un arbre de calcul (codé par un entier) $<|w|$ attestant $\varphi_i(0) = r$, où $r\neq 0$, -\item et arbitraire sinon +\item et arbitraire sinon, \end{itemize} -où $\varphi_i$ désigne la $i$-ième fonction générale récursive. +où $\varphi_i$ désigne la $i$-ième fonction générale récursive +(d'arité $1$). + \emph{Si on préfère} parler en termes de machines de Turing, on pourra changer la définition en : \begin{itemize} \item $0$ si la $i$-ième machine de Turing termine\footnote{Sous-entendu : à partir d'une bande vierge (ou d'une bande représentant le nombre $0$, ou tout autre état initial - fixé, peu importe).} en $<|w|$ étapes et renvoie $0$, + fixé sans importance).} en $<|w|$ étapes et renvoie $0$, \item $1$ si la $i$-ième machine de Turing termine en $<|w|$ étapes et renvoie une valeur $r \neq 0$, \item et arbitraire sinon \end{itemize} (cela ne changera rien de substantiel aux raisonnements). + Informellement dit, l'appartenance d'un mot $w$ à $\mathscr{K}$ est déterminée par le résultat de l'exécution des $|w|$ premiers programmes, chacun jusqu'à la borne $|w|$, et le bit numéroté $i$ @@ -751,14 +756,15 @@ les sommets sont les éléments de $\mathscr{K}$, avec une arête de $u$ à $v$ lorsque $u$ est un préfixe de $v$, est un arbre (infini) au sens de la théorie des graphes. Cette remarque n'est pas utile pour le présent exercice.} pour exprimer la propriété démontrée par cette -question (1) (formellement, un arbre de mots binaires est une partie +question (1). (Formellement, un arbre de mots binaires est une partie $\mathscr{T} \subseteq \{0,1\}^*$ telle que si $v\in\mathscr{T}$ et -que $u$ est un préfixe de $v$, alors $u\in\mathscr{T}$). +que $u$ est un préfixe de $v$, alors $u\in\mathscr{T}$.) \medskip \textbf{(2)} Montrer que $\mathscr{K}$ est une partie \emph{décidable} -(i.e., calculable) de $\{0,1\}^*$. +(i.e., calculable) de $\{0,1\}^*$. Sa fonction indicatrice est-elle +primitive récursive ? \begin{corrige} On veut montrer qu'il existe un algorithme qui, donné un $w \in @@ -773,9 +779,9 @@ lance l'exécution de la $i$-ième machine pour au plus $|w|-1$ étapes et le reste est analogue.) Si une des conditions échoue, le mot $w$ n'est pas dans $\mathscr{K}$, tandis que si toutes réussissent, le mot est dans $\mathscr{K}$. Il s'agit bien là d'un algorithme qui termine -à coup sûr en temps fini (il est même primitif récursif puisqu'on a +à coup sûr en temps fini. Il est même primitif récursif puisqu'on a essentiellement deux boucles imbriquées, une sur $i$ et une sur $j$, -bornées par $|w|$). +bornées par $|w|$. \end{corrige} \medskip @@ -822,6 +828,7 @@ qu'il n'existe pas d'algorithme qui prend en entrée un $e \in \item et une valeur arbitraire sinon (i.e., si $\varphi_e(0)$ n'est pas définie). \end{itemize} + \emph{Si on préfère} parler en termes de machines de Turing, on pourra montrer qu'il n'existe pas d'algorithme qui prend en entrée le code $e$ d'une machine de Turing, \emph{termine toujours en temps fini}, et @@ -896,11 +903,11 @@ n'a pas branche infinie calculable. Le \textbf{lemme de Kőnig} est l'affirmation suivante : « tout arbre de mots binaires contenant des mots de longueur arbitrairement grande -a une branche infinie » (les termes « arbre », « contenant des mots de -longueur arbitrairement grande » et « branche infinie » ont été -définis précisément ci-dessus). On ne demande pas de démontrer cette -affirmation : néanmoins, c'est un théorème des mathématiques -classiques usuelles. +a une branche infinie » (les termes « arbre de mots binaires », +« contenant des mots de longueur arbitrairement grande » et « branche +infinie » ont été définis précisément ci-dessus). On ne demande pas +de démontrer cette affirmation : néanmoins, c'est un théorème des +mathématiques classiques usuelles. \medskip |