From e0c714d1e5e035db928f07f740ba4cc1ed64707a Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Mon, 4 Dec 2023 12:32:31 +0100
Subject: Curry-Howard: a recapitulation.

---
 transp-inf110-02-typage.tex | 51 +++++++++++++++++++++++++++++++++++++++++----
 1 file changed, 47 insertions(+), 4 deletions(-)

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

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index aff8392..3a6a49a 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -2108,8 +2108,9 @@ $\inferrule*[left={Inj$_2$}]{\Gamma\vdash t:\tau_2}{\Gamma\vdash \iota_2^{(\tau_
 (\texttt{match~}r\texttt{~with~}\iota_1 v_1 \mapsto t_1,\; \iota_2 v_2 \mapsto t_2) : \tau}
 \]
 
-{\footnotesize N.B. : ici, $v_1,v_2$ sont des \alert{variables} et
-  $r,t_1,t_2$ des \alert{termes}.\par}
+{\footnotesize\textbf{N.B.} : $v_1,v_2$ sont des
+  \alert{variables} qui sont \alert{liées} par le \texttt{match} ; et
+  $r,t_1,t_2$ sont des \alert{termes}.\par}
 
 \end{frame}
 %
@@ -2207,10 +2208,10 @@ On veut étendre le $\lambda$CST avec un \textbf{type unité} et un
 \begin{tabular}{c|c}
 Typage du $\lambda$-calcul
 &Calcul propositionnel intuitionniste\\[1ex]\hline\\
-$\inferrule*[left={Unit}]{ }{\Gamma\vdash \bullet:\top}$
+$\inferrule*[left={Unit}]{ }{\Gamma\vdash \bullet:1}$
 &$\inferrule*[left={$\top$Int}]{ }{\Gamma\vdash \top}$
 \\[2ex]
-$\inferrule*[left={Void}]{\Gamma\vdash r:\bot}{\Gamma\vdash
+$\inferrule*[left={Void}]{\Gamma\vdash r:0}{\Gamma\vdash
 \texttt{exfalso}^{(\tau)} r : \tau}$
 &$\inferrule*[left={$\bot$Élim}]{\Gamma\vdash \bot}{\Gamma\vdash Q}$
 \end{tabular}
@@ -2374,6 +2375,48 @@ $\Rightarrow$Int de (1) dans (5). »
 
 \par}
 
+\end{frame}
+%
+\begin{frame}
+\frametitle{Curry-Howard : récapitulation}
+
+\itempoint La correspondance de Curry-Howard permet
+d'\alert{identifier}
+\begin{itemize}
+\item\textcolor{blue}{types} du $\lambda$-calcul simplement typé,
+  éventuellement enrichi de constructions de types produit ($\times$),
+  somme ($+$), trivial ($1$) et vide ($0$), et
+\item\textcolor{blue}{propositions} (=formules logiques) du calcul
+  propositionnel intuitionniste avec pour connecteurs
+  l'implication ($\Rightarrow$) et éventuellement la
+  conjonction ($\land$), disjonction ($\lor$), vrai ($\top$) et
+  faux ($\bot$) respectivement,
+\end{itemize}
+en identifant aussi
+\begin{itemize}
+\item\textcolor{blue}{termes} ayant les types en question,
+\item\textcolor{blue}{preuves} des propositions en question, dans le
+  style « déduction naturelle », en calcul propositionnel
+  intutionniste.
+\end{itemize}
+
+\medskip
+
+\itempoint Noter aussi : abstraction$\leftrightarrow$ouverture
+d'hypothèse ; application$\leftrightarrow$\textit{modus ponens} ;
+variables$\leftrightarrow$hypothèses ; variables
+liées$\leftrightarrow$hypothèses déchargées.
+
+\bigskip
+
+{\footnotesize
+
+\itempoint On se permettra maintenant parfois des abus de notation
+justifiés par Curry-Howard, p.ex., traiter $\rightarrow$ et
+$\Rightarrow$ comme interchangeables.
+
+\par}
+
 \end{frame}
 %
 % TODO:
-- 
cgit v1.2.3