diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 31 |
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 |