Make changes suggested by TZ.

1 files changed, 50 insertions, 21 deletions

diff --git a/controle-20240126.tex b/controle-20240126.tex
index 0441add..740aaa1 100644
--- a/controle-20240126.tex
+++ b/controle-20240126.tex
@@ -81,9 +81,9 @@ 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 les questions (du
-problème) présentent une gradation approximative de difficulté, il est
-recommandé de les traiter dans l'ordre.
+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
@@ -101,13 +101,14 @@ L'usage des appareils électroniques est interdit.
 
 Durée : 3h
 
-Barème \emph{approximatif} et \emph{indicatif} : $2.5$ points par
-exercice et $0.75$ points par question du problème.
+Barème \emph{approximatif} et \emph{indicatif} (sur $20$) : entre $2$
+et $3$ points par exercice et environ $0.75$ points par question du
+problème.
 
 \ifcorrige
-Ce corrigé comporte 12 pages (page de garde incluse).
+Ce corrigé comporte \textcolor{red}{à remplir} pages (page de garde incluse).
 \else
-Cet énoncé comporte 6 pages (page de garde incluse).
+Cet énoncé comporte 7 pages (page de garde incluse).
 \fi
 
 \vfill
@@ -189,13 +190,39 @@ pour terminer la démonstration).
 
 \exercice
 
+Donner une démonstration en calcul propositionnel intuitionniste de la
+formule suivante :
+\[
+(A\Rightarrow B\Rightarrow C) \Rightarrow (B\Rightarrow A\Rightarrow C)
+\]
+On donnera la démonstration sous la forme qu'on préfère (arbre de
+preuve, style drapeau, ou même simplement précisément écrite en
+français), puis on donnera aussi un $\lambda$-terme de preuve.  On
+décrira ensuite brièvement ce que fait ce terme vu en tant que
+programme (i.e., le comportement du programme associé à la preuve par
+la correspondance de Curry-Howard).
+
+\begin{corrige}
+\textcolor{red}{Corrigé de cet exercice à écrire.  Ce qui suit est un
+  résumé.}  Le $\lambda$-terme est $\lambda(f:A\Rightarrow
+B\Rightarrow C).\, \lambda(y:B).\, \lambda(x:A).\, f x y$ et il
+échange les deux arguments d'une fonction de deux variables donnée
+sous forme curryfiée.
+\end{corrige}
+
+
+%
+%
+%
+
+\exercice
+
 (Dans cet exercice, on ne demande pas de justifier les réponses.)
 
-\textbf{(1)} En calcul propositionnel intuitionniste, quelle est la
-conclusion de la démonstration représentée par le $\lambda$-terme de
-preuve suivant ?  (Ou si on préfère : quel est le type de ce terme du
-$\lambda$-calcul simplement typé enrichi de types produits, qu'on a
-écrit en notations logiques ?)
+\textbf{(1)} En calcul propositionnel intuitionniste, quel est
+l'énoncé prouvé par le $\lambda$-terme de preuve suivant ?  (Ou si on
+préfère : quel est le type de ce terme du $\lambda$-calcul simplement
+typé enrichi de types produits, qu'on a écrit en notations logiques ?)
 \[
 \lambda(p: C\land(A\Rightarrow B)).\,
 \lambda(h:A).\,
@@ -203,9 +230,8 @@ $\lambda$-calcul simplement typé enrichi de types produits, qu'on a
 \]
 (Ici, $A,B,C$ sont des variables propositionnelles.)
 
-\textbf{(2)} En logique du premier ordre intuitionniste, quelle est la
-conclusion de la démonstration représentée par le $\lambda$-terme de
-preuve suivant ?
+\textbf{(2)} En logique du premier ordre intuitionniste, quel est
+l'énoncé prouvé par le $\lambda$-terme de preuve suivant ?
 \[
 \lambda(p: C\land\forall x. B(x)).\,
 \lambda(x:I).\,
@@ -215,9 +241,8 @@ preuve suivant ?
 variable propositionnelle, $B$ est une variable de relation unaire, et
 $I$ est le symbole du type des individus.)
 
-\textbf{(3)} En logique du premier ordre intuitionniste, quelle est la
-conclusion de la démonstration représentée par le $\lambda$-terme de
-preuve suivant ?
+\textbf{(3)} En logique du premier ordre intuitionniste, quel est
+l'énoncé prouvé par le $\lambda$-terme de preuve suivant ?
 \[
 \lambda(p: \exists x.(A\Rightarrow B(x))).\,
 \lambda(h:A).\,
@@ -271,6 +296,9 @@ $\lambda$-calcul non typé :
 syntaxe OCaml).  Quel théorème du calcul propositionnel intuitionniste
 obtient-on de ceci par Curry-Howard ?
 
+(Une réponse qui ne suit pas l'algorithme de Hindley-Milner mais qui
+est néanmoins correcte vaudra une partie des points.)
+
 \begin{corrige}
 Dans une première phase, on collecte les types et contraintes
 suivants : $f:\eta_1$, $z:\eta_2$, $fz : \eta_3$ avec $\eta_1 =
@@ -349,8 +377,9 @@ la promesse qu'au moins deux d'entre elles sont vides : pour la
 réalisabilité, on pourra considérer une des parties valant
 $\mathbb{N}$ et les deux autres valant $\varnothing$ et constater
 qu'on ne peut pas réaliser les trois affectations à la fois, tandis
-que pour la sémantique des problèmes finis, on pourra trois problèmes
-ayant un seul candidat chacun mais un seul ayant une solution.)
+que pour la sémantique des problèmes finis, on pourra considérer trois
+problèmes ayant un seul candidat chacun mais un seul ayant une
+solution.)
 
 \begin{corrige}
 On donne quatre solutions possibles, une pour chaque sémantique vue en
@@ -581,7 +610,7 @@ rien d'essentiel).
 
 \smallskip
 
-On fait donc les définitions suivantes :
+On introduit donc les définitions suivantes :
 \begin{itemize}
 \item Un \textbf{dyadique} est un rationnel de la forme
   $\frac{k}{2^n}$ avec $k\in\mathbb{Z}$ et $n\in \mathbb{N}$ (i.e.,