A first taste of the Curry-Howard correspondence.

1 files changed, 34 insertions, 1 deletions

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.
 
@@ -580,6 +580,39 @@ restrictions :
 \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}
 \frametitle{Paradoxe de Curry (interlude distrayant)}
 
 {\footnotesize Variante plus sophistiquée de « cette phrase est