diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 51 |
1 files 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} @@ -2376,6 +2377,48 @@ $\Rightarrow$Int de (1) dans (5). » \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: % - discussion de la négation et double négation % - substitution des variables propositionnelles par des formules |