diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 46 |
1 files changed, 44 insertions, 2 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 74a3079..05d3797 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -2041,10 +2041,10 @@ pour refléter les règles de la disjonction logique : \begin{tabular}{c|c} Typage du $\lambda$-calcul &Calcul propositionnel intuitionniste\\[1ex]\hline\\ -$\inferrule*[left={Inj$_1$}]{\Gamma\vdash t:\tau_1}{\Gamma\vdash \iota_1^{{\tau_1,\tau_2}} t: \tau_1 + \tau_2}$ +$\inferrule*[left={Inj$_1$}]{\Gamma\vdash t:\tau_1}{\Gamma\vdash \iota_1^{(\tau_1,\tau_2)} t: \tau_1 + \tau_2}$ &$\inferrule*[left={$\lor$Int$_1$}]{\Gamma\vdash Q_1}{\Gamma\vdash Q_1\lor Q_2}$ \\[2ex] -$\inferrule*[left={Inj$_2$}]{\Gamma\vdash t:\tau_2}{\Gamma\vdash \iota_2^{{\tau_1,\tau_2}} t: \tau_1 + \tau_2}$ +$\inferrule*[left={Inj$_2$}]{\Gamma\vdash t:\tau_2}{\Gamma\vdash \iota_2^{(\tau_1,\tau_2)} t: \tau_1 + \tau_2}$ &$\inferrule*[left={$\lor$Int$_2$}]{\Gamma\vdash Q_2}{\Gamma\vdash Q_1\lor Q_2}$ \\[2ex] \textcolor{gray}{ci-dessous $\downarrow$} @@ -2061,6 +2061,48 @@ $\inferrule*[left={Inj$_2$}]{\Gamma\vdash t:\tau_2}{\Gamma\vdash \iota_2^{{\tau_ \end{frame} % +\begin{frame} +\frametitle{Remarques sur types produits et sommes} + +\itempoint À côté de la $\beta$-réduction usuelle du $\lambda$-calcul, +$(\lambda (v:\sigma). e)t \rightsquigarrow e[v\backslash t]$, on +introduit des nouvelles règles de réduction pour la conjonction et la +disjonction : +\begin{itemize} +\item $\pi_i\langle t_1,t_2\rangle \;\rightsquigarrow\; t_i$ (pour + $i\in\{1,2\}$) +\item $(\texttt{match~}\iota_i^{(\tau_1,\tau_2)}s\texttt{~with~}\iota_1 + v_1 \mapsto t_1,\; \iota_2 v_2 \mapsto t_2) \;\rightsquigarrow\; + t_i[v_i\backslash s]$ (pour $i\in\{1,2\}$) +\end{itemize} + +\medskip + +\itempoint Côté démonstrations : cette réduction court-circuite une +règle \textsc{Intro} immédiatement suivie par une règle \textsc{Élim} +(ce qu'on appelle un « détour »). + +\medskip + +\itempoint Le $\lambda$-calcul simplement typé reste fortement +normalisant avec ces extensions par types produits et sommes et les +réductions ci-dessus. + +\medskip + +\itempoint Les injections $\iota_i : \tau_i \to \tau_1+\tau_2$ portent +l'exposant $(\tau_1,\tau_2)$ pour que les annotations de type soient +complètes (mais il est inutile dans le matching). + +\medskip + +\itempoint Aucune des notations +$\pi_i,\ \langle,\rangle,\ \iota_i,\ \texttt{match}...\texttt{with}$ +n'est standardisée (bcp de variations existent), mais il n'y a aucun +doute sur la correspondance elle-même. + +\end{frame} +% % TODO: % - substitution des variables propositionnelles par des formules % - substitution d'équivalences |