diff options
| -rw-r--r-- | controle-20240126.tex | 19 |
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} |