An example of Curry-Howard with conjunction.

1 files changed, 74 insertions, 4 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index bcca8a9..95c0dae 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -31,6 +31,7 @@
 \renewcommand{\thefootnote}{\textdagger}
 \newcommand{\dbllangle}{\mathopen{\langle\!\langle}}
 \newcommand{\dblrangle}{\mathclose{\rangle\!\rangle}}
+\mathchardef\emdash="07C\relax
 \setlength{\derivskip}{4pt}
 %
 %
@@ -1340,7 +1341,7 @@ hypothèses $P_1,\ldots,P_r$, on a $Q$ ».
 \end{frame}
 %
 \begin{frame}
-\frametitle{Le calcul propositionnel intuitionniste : survol des règles}
+\frametitle{Le calcul propositionnel intuitionniste : règles}
 
 Axiomes : si $Q \in \{P_1,\ldots,P_r\}$ alors $P_1,\ldots,P_r \vdash Q$.
 
@@ -1382,7 +1383,8 @@ $\bot$
 \end{frame}
 %
 \begin{frame}
-\frametitle{Exemples de démonstration}
+\label{example-propositional-proofs}
+\frametitle{Exemples de démonstrations}
 
 {\footnotesize
 \[
@@ -1886,7 +1888,7 @@ A. Troelstra et d'autres :
 \end{frame}
 %
 \begin{frame}
-\frametitle{Correspondance de Curry-Howard (implication seule)}
+\frametitle{Correspondance de Curry-Howard : implication seule}
 
 \begin{tabular}{c|c}
 Typage du $\lambda$-calcul simplement typé
@@ -1928,10 +1930,78 @@ intuitionniste restreint au seul connecteur $\Rightarrow$.
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{Correspondance de Curry-Howard : conjonction}
+
+On veut \alert{étendre} le $\lambda$CST avec un \textbf{type produit}
+pour refléter les règles de la conjonction logique :
+
+\medskip
+
+\begin{tabular}{c|c}
+Typage du $\lambda$-calcul
+&Calcul propositionnel intuitionniste\\[1ex]\hline\\
+$\inferrule*[left=Proj$_1$]{\Gamma \vdash t:\tau_1\times\tau_2}{\Gamma \vdash \pi_1 t:\tau_1}$
+&$\inferrule*[left={$\land$Élim$_1$}]{\Gamma\vdash Q_1\land Q_2}{\Gamma\vdash Q_1}$
+\\[2ex]
+$\inferrule*[left=Proj$_2$]{\Gamma \vdash t:\tau_1\times\tau_2}{\Gamma \vdash \pi_2 t:\tau_2}$
+&$\inferrule*[left={$\land$Élim$_2$}]{\Gamma\vdash Q_1\land Q_2}{\Gamma\vdash Q_2}$
+\\[2ex]
+$\inferrule*[left=Pair]{\Gamma \vdash t_1:\tau_1\\\Gamma \vdash t_2:\tau_2}{\Gamma \vdash \langle t_1,t_2\rangle : \tau_1\times\tau_2}$
+&$\inferrule*[left={$\land$Int}]{\Gamma\vdash Q_1\\\Gamma\vdash Q_2}{\Gamma\vdash Q_1\land Q_2}$
+\end{tabular}
+
+\medskip
+
+\itempoint Ici, $\langle\emdash,\emdash\rangle$ sert à construire des
+couples, et $\pi_1,\pi_2$ à les déconstruire.
+
+\smallskip
+
+{\footnotesize
+
+\itempoint Nouvelle règle de réduction : $\pi_i\langle t_1,t_2\rangle$
+se réduit en $t_i$ (pour $i\in\{1,2\}$).
+
+\par}
+
+\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\land B \Rightarrow B\land A$
+(transp. \ref{example-propositional-proofs} et suivants) :
+
+{\footnotesize
+\[
+\inferrule*[left={Abs},right=\hphantom{Abs}]{
+\inferrule*[left=\llap{Pair}]{
+\inferrule*[left=\llap{Proj$_2$}]{
+\inferrule*[left=\llap{Var}]{ }{u:\alpha\times \beta \vdash u:\alpha\times \beta}
+}{u:\alpha\times \beta \vdash \pi_2 u:\beta}
+\\
+\inferrule*[right=\rlap{Proj$_1$}]{
+\inferrule*[right=\rlap{Var}]{ }{u:\alpha\times \beta \vdash u:\alpha\times \beta}
+}{u:\alpha\times \beta \vdash \pi_1 u:\alpha}
+}{u:\alpha\times \beta \vdash \langle \pi_2 u, \pi_1 u\rangle:\beta\times \alpha}
+}{\vdash \lambda(u:\alpha\times\beta).\,\langle \pi_2 u, \pi_1 u\rangle : \alpha\times \beta \rightarrow \beta\times \alpha}
+\]
+\par}
+
+\bigskip
+
+\itempoint Il s'agit de la fonction
+$\lambda(u:\alpha\times\beta).\,\langle \pi_2 u, \pi_1 u\rangle$
+(polymorphe de type $\alpha\times\beta \to \beta\times\alpha$) qui
+échange les deux termes d'un couple.
+
+\end{frame}
+%
 % TODO:
 % - substitution des variables propositionnelles par des formules
 % - substitution d'équivalences
-% - Curry-Howard
 % - Kriple
 %
 \end{document}