diff options
Diffstat (limited to 'transp-inf110-02-typage.tex')
| -rw-r--r-- | transp-inf110-02-typage.tex | 41 |
1 files changed, 41 insertions, 0 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 05d3797..e2419ac 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -2103,6 +2103,47 @@ doute sur la correspondance elle-même. \end{frame} % +\begin{frame} +\frametitle{Correspondance de Curry-Howard : exemple avec conjonction} + +\itempoint Transformons en programme la démonstration qu'on a donnée +de $A\lor B \Rightarrow B\lor A$ +(transp. \ref{example-propositional-proofs} et suivants) : + +{\footnotesize +\[ +\inferrule*[left={Abs},right=\hphantom{Int}]{ +\inferrule*[left=\llap{Match}]{ +\inferrule*[left=\llap{Var}]{ }{u:\alpha+\beta \vdash u:\alpha+\beta} +\\ +\inferrule*[right={Inj$_2$}]{ +\inferrule*[right=\rlap{Var}]{ }{\ldots,v:\alpha \vdash v:\alpha} +}{{\scriptstyle\cdots} \vdash \iota_2^{(\beta,\alpha)} v : \beta+\alpha} +\\ +\inferrule*[right=\rlap{Inj$_1$}]{ +\inferrule*[right=\rlap{Var}]{ }{\ldots,v':\beta \vdash v':\beta} +}{{\scriptstyle\cdots} \vdash \iota_1^{(\beta,\alpha)} v' : \beta+\alpha} +}{u:\alpha+\beta \vdash (\texttt{match~} u\texttt{~with~}\iota_1 + v \mapsto \iota^{(\beta,\alpha)}_2 v,\; \iota_2 v' \mapsto \iota_1^{(\beta,\alpha)} v') : \beta+\alpha} +}{\vdash \lambda (u:\alpha+\beta) . +(\texttt{match~} u\texttt{~with~}\iota_1 + v \mapsto \iota^{(\beta,\alpha)}_2 v,\; \iota_2 v' \mapsto \iota_1^{(\beta,\alpha)} v') : \alpha+\beta \to \beta+\alpha} +\] +\par} + +\bigskip + +\itempoint Il s'agit de la fonction +\[ +\lambda (u:\alpha+\beta) . +(\texttt{match~} u\texttt{~with~}\iota_1 + v \mapsto \iota^{(\beta,\alpha)}_2 v,\; \iota_2 v' \mapsto \iota_1^{(\beta,\alpha)} v') +\] +(polymorphe de type $\alpha+\beta \to \beta+\alpha$) qui échange les +deux cas d'une somme. + +\end{frame} +% % TODO: % - substitution des variables propositionnelles par des formules % - substitution d'équivalences |