A brief word on Curry-Howard for sequent calculus, and the lambda-bar-calculus.

1 files changed, 62 insertions, 0 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index cd3857a..980d0b5 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -3118,6 +3118,68 @@ $Q$.  {\footnotesize (\underline{Preuve :} c'est clair sur chacune des
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{Calcul des séquents et Curry-Howard}
+
+\itempoint On a vu que les preuves en déduction naturelle
+correspondent aux termes du $\lambda$-calcul simplement typé
+(+extensions).
+
+\smallskip
+
+On peut trouver un correspondant aux preuves en calcul des séquents
+{\footnotesize (avec de petites modifications)} : le
+$\overline{\lambda}$-calcul de Herbelin.
+
+\smallskip
+
+{\footnotesize Le $\overline{\lambda}$-calcul a deux sortes d'objets :
+  les \emph{termes} $t$ et les \emph{listes d'arguments} (notées
+  $[t_1;\ldots;t_r]$).\par}
+
+\medskip
+
+\itempoint En travaillant un peu, on peut déduire l'élimination des
+coupures de la conversion en $\overline{\lambda}$-calcul de termes
+normaux du $\lambda$-calcul (donc de sa normal\textsuperscript{ion}).
+
+\begin{center}
+\scalebox{0.56}{
+$\inferrule*{
+\inferrule*{
+\inferrule*{ }{y : C\vdash y : C}
+\\
+\inferrule*{ }{x_1:A_1\vdash x_1 : A_1}
+}{y:C, x_1:A_1\vdash yx_1 : A_2\to B}
+\\
+\inferrule*{ }{x_2:A_2\vdash x_2 : A_2}
+}{y:C, x_1:A_1, x_2:A_2\vdash yx_1 x_2 : B}$
+}
+$\rightsquigarrow$
+\scalebox{0.56}{
+$\inferrule*{
+\inferrule*{
+\inferrule*{ }{x_1:A_1\vdash x_1:A_1}
+\\
+\inferrule*{
+\inferrule*{ }{x_2:A_2\vdash x_2:A_2}
+\\
+\inferrule*{ }{\_:C \vdash \_ [] : C}
+}{x_2:A_2;\_:A_2\to B \vdash \_ [x_2] : A_2\to B}
+}{x_1:A_1, x_2:A_2;\_:C \vdash \_ [x_1; x_2] : B}
+}{y:C, x_1:A_1, x_2:A_2\vdash y [x_1; x_2] : B}$
+}
+
+\footnotesize
+
+(où $C := A_1\to A_2 \to B$)
+
+(à gauche le $\lambda$-calcul, à droite le
+$\overline{\lambda}$-calcul ; remarquez l'inversion des arguments)
+\end{center}
+
+\end{frame}
+%
 % TODO:
 % - Kripke
 % - fragment négatif