diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 33 |
1 files changed, 32 insertions, 1 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index e2419ac..c699a10 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -2033,7 +2033,7 @@ $\lambda(u:\alpha\times\beta).\,\langle \pi_2 u, \pi_1 u\rangle$ \begin{frame} \frametitle{Correspondance de Curry-Howard : disjonction} -On veut \alert{étendre} le $\lambda$CST avec un \textbf{type somme} +On veut étendre le $\lambda$CST avec un \textbf{type somme} pour refléter les règles de la disjonction logique : \medskip @@ -2144,6 +2144,37 @@ deux cas d'une somme. \end{frame} % +\begin{frame} +\frametitle{Correspondance de Curry-Howard : vrai et faux} + +On veut étendre le $\lambda$CST avec un \textbf{type unité} et un +\textbf{type vide} pour refléter les règles du vrai et du faux : + +\medskip + +\begin{tabular}{c|c} +Typage du $\lambda$-calcul +&Calcul propositionnel intuitionniste\\[1ex]\hline\\ +$\inferrule*[left={Unit}]{ }{\Gamma\vdash \bullet:\top}$ +&$\inferrule*[left={$\top$Int}]{ }{\Gamma\vdash \top}$ +\\[2ex] +$\inferrule*[left={Void}]{\Gamma\vdash r:\bot}{\Gamma\vdash +\texttt{exfalso}^{(\tau)} r : \tau}$ +&$\inferrule*[left={$\bot$Élim}]{\Gamma\vdash \bot}{\Gamma\vdash Q}$ +\end{tabular} + +\medskip + +\itempoint Ici, $\bullet$ désigne la valeur triviale de type unité +(\texttt{()} en OCaml), et $\texttt{exfalso}$ est un matching vide. +{\footnotesize (Notations pas standardisées du tout.)} + +\smallskip + +\itempoint Pas de nouvelle règle de réduction à ajouter. + +\end{frame} +% % TODO: % - substitution des variables propositionnelles par des formules % - substitution d'équivalences |