summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--controle-20240126.tex19
1 files changed, 9 insertions, 10 deletions
diff --git a/controle-20240126.tex b/controle-20240126.tex
index 740aaa1..0e3c269 100644
--- a/controle-20240126.tex
+++ b/controle-20240126.tex
@@ -193,21 +193,20 @@ pour terminer la démonstration).
Donner une démonstration en calcul propositionnel intuitionniste de la
formule suivante :
\[
-(A\Rightarrow B\Rightarrow C) \Rightarrow (B\Rightarrow A\Rightarrow C)
+A \Rightarrow (A\Rightarrow B) \Rightarrow B
\]
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).
+preuve ou style drapeau), 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.
+ résumé.} Le $\lambda$-terme est $\lambda(x:A).\,
+\lambda(k:A\Rightarrow B).\, k x$, et le programme transforme $x$ en
+la fonction qui applique une fonction $k$ à $x$, ou, ce qui revient au
+même, il prend successivement $x$ et $k$ et applique $k$ à $x$.
\end{corrige}