Remarks on products and sums.

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