Curry-Howard correspondence for disjunction.

1 files changed, 31 insertions, 0 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index a28dbce..74a3079 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -2030,6 +2030,37 @@ $\lambda(u:\alpha\times\beta).\,\langle \pi_2 u, \pi_1 u\rangle$
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{Correspondance de Curry-Howard : disjonction}
+
+On veut \alert{étendre} le $\lambda$CST avec un \textbf{type somme}
+pour refléter les règles de la disjonction logique :
+
+\medskip
+
+\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={$\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={$\lor$Int$_2$}]{\Gamma\vdash Q_2}{\Gamma\vdash Q_1\lor Q_2}$
+\\[2ex]
+\textcolor{gray}{ci-dessous $\downarrow$}
+&{\footnotesize $\inferrule*[left={$\lor$Élim}]{\Gamma\vdash P_1\lor P_2\\\Gamma,P_1\vdash Q\\\Gamma,P_2\vdash Q}{\Gamma\vdash Q}$}
+\end{tabular}
+
+\[
+\inferrule*[left={Match}]{\Gamma\vdash r:\sigma_1+ \sigma_2\\\Gamma,v_1:\sigma_1\vdash t_1:\tau\\\Gamma,v_2:\sigma_2\vdash t_2:\tau}{\Gamma\vdash
+(\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}
+
+\end{frame}
+%
 % TODO:
 % - substitution des variables propositionnelles par des formules
 % - substitution d'équivalences