From 84c0b48f9d1622acdb456e70c385481b67061a05 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Sun, 3 Dec 2023 21:31:29 +0100
Subject: Curry-Howard correspondence for true and false.
---
transp-inf110-02-typage.tex | 33 ++++++++++++++++++++++++++++++++-
1 file changed, 32 insertions(+), 1 deletion(-)
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
@@ -2142,6 +2142,37 @@ de $A\lor B \Rightarrow B\lor A$
(polymorphe de type $\alpha+\beta \to \beta+\alpha$) qui échange les
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:
--
cgit v1.2.3