diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 62 |
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 |