Various examples of Curry-Howard.

1 files changed, 81 insertions, 1 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index c699a10..50a442d 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -1549,7 +1549,7 @@ $A\land(B\lor C) \Leftrightarrow (A\land B)\lor (A\land C)$
 $\top$&$\bot \Rightarrow C$\\
 \hline
 $\top\land A \Leftrightarrow A$\quad\quad\quad$\bot \land A \Leftrightarrow \bot$
-&$\top\lor A \Leftrightarrow \top$\quad\quad\quad$\bot \lor A \Leftrightarrow A$\\
+&$\top\lor A \mathrel{\color{olive}\Leftrightarrow} \top$\quad\quad\quad$\bot \lor A \Leftrightarrow A$\\
 \hline
 $\neg A \land \neg B \Leftrightarrow \neg(A\lor B)$&$\neg A \lor \neg B \mathrel{\color{red}\Rightarrow} \neg(A\land B)$\\
 \hline
@@ -2175,6 +2175,86 @@ $\inferrule*[left={Void}]{\Gamma\vdash r:\bot}{\Gamma\vdash
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{Correspondance de Curry-Howard : exemples divers}
+
+\itempoint L'implication $(A\Rightarrow B\Rightarrow C) \Rightarrow
+(A\Rightarrow B)\Rightarrow A\Rightarrow C$ est démontrée par le terme
+(« combinateur $\mathsf{S}$ ») :
+\[
+\lambda (x:\alpha\to\beta\to\gamma).\,
+\lambda (y:\alpha\to\beta).\,
+\lambda (z:\alpha).\,
+xz(yz)
+\]
+
+\medskip
+
+\itempoint L'équivalence $(A\land B \Rightarrow C) \Leftrightarrow
+(A\Rightarrow B\Rightarrow C)$ est démontrée par les fonctions de
+« curryfication »
+\[
+\lambda (f:\alpha\times\beta\to\gamma).\,
+\lambda (x:\alpha).\, \lambda(y:\beta).\,
+f\langle x,y\rangle
+\]
+et « décurryfication »
+\[
+\lambda (f:\alpha\to\beta\to\gamma).\,
+\lambda (z:\alpha\times\beta).\,
+f(\pi_1 z)(\pi_2 z)
+\]
+
+\medskip
+
+\itempoint L'équivalence $A\lor(B\land C) \Leftrightarrow (A\lor
+B)\land (A\lor C)$ est démontrée par les termes
+{\footnotesize
+\[
+\lambda (u:\alpha+(\beta\times\gamma)).\,
+(\texttt{match~}u\texttt{~with~}\iota_1 v \mapsto \langle \iota^{(\alpha,\beta)}_1 v, \iota^{(\alpha,\gamma)}_1 v\rangle,\;
+\iota_2 w \mapsto \langle \iota^{(\alpha,\beta)}_2 (\pi_1 w), \iota^{(\alpha,\gamma)}_2 (\pi_2 w)\rangle)
+\]
+\vskip-1ex et\vskip-5ex
+\[
+\begin{aligned}
+\lambda (u:(\alpha+\beta)\times(\alpha+\gamma)).\,
+&(\texttt{match~}\pi_1 u\texttt{~with~}\iota_1 v \mapsto \iota_1^{(\alpha,\beta\times\gamma)} v,\\
+\iota_2 v' \mapsto
+&(\texttt{match~}\pi_2 u\texttt{~with~}\iota_1 w \mapsto \iota_1^{(\alpha,\beta\times\gamma)} w,\;
+\iota_2 w' \mapsto \iota_2^{(\alpha,\beta\times\gamma)}\langle v',w'\rangle ))
+\end{aligned}
+\]
+}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Correspondance de Curry-Howard : exemple en OCaml}
+
+Reprise de l'équivalence $A\lor(B\land C) \Leftrightarrow (A\lor
+B)\land (A\lor C)$ typée par OCaml :
+
+\bigskip
+
+{\footnotesize\tt
+let pi1 = fun (x,y) -> x ;; (* $\pi_1$ *)\\
+{\color{purple}val pi1 : 'a * 'b -> 'a = <fun>}\\
+let pi2 = fun (x,y) -> y ;; (* $\pi_2$ *)\\
+{\color{purple}val pi2 : 'a * 'b -> 'b = <fun>}\\
+type ('a, 'b) sum = Inj1 of 'a | Inj2 of 'b ;; (* $\alpha+\beta$ *)\\
+{\color{purple}type ('a, 'b) sum = Inj1 of 'a | Inj2 of 'b}\\
+fun u -> match u with Inj1 v -> (Inj1 v, Inj1 v)\\
+\ \ | Inj2 w -> (Inj2 (pi1 w), Inj2 (pi2 w)) ;;\\
+{\color{purple}- : ('a, 'b * 'c) sum -> ('a, 'b) sum * ('a, 'c) sum = <fun>}\\
+fun u -> (match (pi1 u) with Inj1 v -> Inj1 v\\
+\ \ | Inj2 v\_ -> (match (pi2 u) with Inj1 w -> Inj1 w\\
+\ \ \ \ | Inj2 w\_ -> Inj2 (v\_,w\_))) ;;\\
+{\color{purple}- : ('a, 'b) sum * ('a, 'c) sum -> ('a, 'b * 'c) sum = <fun>}
+}
+
+\end{frame}
+%
 % TODO:
 % - substitution des variables propositionnelles par des formules
 % - substitution d'équivalences