From b3fbc6cb78e34001790a9dec937eeda0758d42f9 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Wed, 22 Nov 2023 11:33:16 +0100
Subject: A first taste of the Curry-Howard correspondence.

---
 transp-inf110-02-typage.tex | 35 ++++++++++++++++++++++++++++++++++-
 1 file changed, 34 insertions(+), 1 deletion(-)

(limited to 'transp-inf110-02-typage.tex')

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 55c5de1..9040312 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -170,7 +170,7 @@ sont \emph{souvent} proposées par les systèmes de typage :
 
 \bigskip
 
-\itempoint Types \textbf{produits} (= paires, triplets, $k$-uplets).
+\itempoint Types \textbf{produits} (= couples, triplets, $k$-uplets).
 P.ex. $\texttt{Nat} \times \texttt{Bool}$ = type des paires formées
 d'un entier et d'un booléen.
 
@@ -577,6 +577,39 @@ restrictions :
   sommes paramétriques (types $\Sigma$) et $\exists$ côté logique.
 \end{itemize}
 
+\end{frame}
+%
+\begin{frame}
+\frametitle{La correspondance de Curry-Howard (premier aperçu)}
+
+{\footnotesize\textcolor{gray}{Divulgâchis pour la suite !}\par}
+
+\smallskip
+
+La correspondance de Curry-Howard fait notamment correspondre :
+\begin{itemize}
+\item type \textbf{fonction} $A \to B$ avec \textbf{implication}
+  logique $A \Rightarrow B$,
+\item \textbf{application} d'une fonction ($A \to B$ à un argument de
+  type $A$) avec \textbf{\textit{modus ponens}} (si $A \Rightarrow B$
+  et $A$, alors $B$),
+\item \textbf{abstraction} (= création d'une fonction) avec ouverture
+  d'une \textbf{hypothèse} (« supposons $A$ : alors (…) donc $B$ ;
+  ceci prouve $A \Rightarrow B$ »),
+\item type \textbf{produit} (= couples) $A \times B$ avec
+  \textbf{conjonction} (« et ») logique $A \land B$,
+\item type \textbf{somme} $A + B$ avec \textbf{disjonction} (« ou »)
+  logique $A \lor B$,
+\item types \textbf{trivial} ($\texttt{Unit}$) et \textbf{vide} avec
+  \textbf{vrai} $\top$ et \textbf{faux} $\bot$ logiques,
+\item mais pour la \textbf{négation}…  c'est plus délicat.
+\end{itemize}
+
+\bigskip
+
+{\footnotesize Les détails demandent un système de typage et un
+  système logique précisément définis.\par}
+
 \end{frame}
 %
 \begin{frame}
-- 
cgit v1.2.3