Curry-Howard correspondence for true and false.

1 files changed, 32 insertions, 1 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index e2419ac..c699a10 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -2033,7 +2033,7 @@ $\lambda(u:\alpha\times\beta).\,\langle \pi_2 u, \pi_1 u\rangle$
 \begin{frame}
 \frametitle{Correspondance de Curry-Howard : disjonction}
 
-On veut \alert{étendre} le $\lambda$CST avec un \textbf{type somme}
+On veut étendre le $\lambda$CST avec un \textbf{type somme}
 pour refléter les règles de la disjonction logique :
 
 \medskip
@@ -2144,6 +2144,37 @@ deux cas d'une somme.
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{Correspondance de Curry-Howard : vrai et faux}
+
+On veut étendre le $\lambda$CST avec un \textbf{type unité} et un
+\textbf{type vide} pour refléter les règles du vrai et du faux :
+
+\medskip
+
+\begin{tabular}{c|c}
+Typage du $\lambda$-calcul
+&Calcul propositionnel intuitionniste\\[1ex]\hline\\
+$\inferrule*[left={Unit}]{ }{\Gamma\vdash \bullet:\top}$
+&$\inferrule*[left={$\top$Int}]{ }{\Gamma\vdash \top}$
+\\[2ex]
+$\inferrule*[left={Void}]{\Gamma\vdash r:\bot}{\Gamma\vdash
+\texttt{exfalso}^{(\tau)} r : \tau}$
+&$\inferrule*[left={$\bot$Élim}]{\Gamma\vdash \bot}{\Gamma\vdash Q}$
+\end{tabular}
+
+\medskip
+
+\itempoint Ici, $\bullet$ désigne la valeur triviale de type unité
+(\texttt{()} en OCaml), et $\texttt{exfalso}$ est un matching vide.
+{\footnotesize (Notations pas standardisées du tout.)}
+
+\smallskip
+
+\itempoint Pas de nouvelle règle de réduction à ajouter.
+
+\end{frame}
+%
 % TODO:
 % - substitution des variables propositionnelles par des formules
 % - substitution d'équivalences