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(-)
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