From 492bf7b8f78863ef3405f3a43fbe2fe2b479ce9e Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Sun, 3 Dec 2023 18:38:40 +0100
Subject: Curry-Howard correspondence for implication alone.

---
 transp-inf110-02-typage.tex | 44 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 44 insertions(+)

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index bebce81..bcca8a9 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -1107,6 +1107,7 @@ ayant ce type.
 \end{frame}
 %
 \begin{frame}
+\label{reconstructing-typed-term}
 \frametitle{Reconstruction du terme typé}
 
 Peut-on retrouver les termes manquants dans un arbre de dérivation
@@ -1882,6 +1883,49 @@ A. Troelstra et d'autres :
 {\footnotesize J'écris « témoignage », mais Kolmogorov parlait de
   « solution » d'un problème, Heyting de « preuve », etc.\par}
 
+\end{frame}
+%
+\begin{frame}
+\frametitle{Correspondance de Curry-Howard (implication seule)}
+
+\begin{tabular}{c|c}
+Typage du $\lambda$-calcul simplement typé
+&Calcul propositionnel intuitionniste\\[1ex]\hline\\
+$\inferrule*[left={Var}]{ }{\Gamma,x:\sigma \vdash x:\sigma}$
+&
+$\inferrule*[left={Ax}]{ }{\Gamma,P \vdash P}$
+\\[2ex]
+$\inferrule*[left={App},sep=3em]{\Gamma \vdash f:\sigma\to\tau\\ \Gamma
+  \vdash x:\sigma}{\Gamma \vdash fx:\tau}$
+&
+$\inferrule*[left={$\Rightarrow$Élim},sep=3em]{\Gamma \vdash P\Rightarrow Q\\ \Gamma
+  \vdash P}{\Gamma \vdash Q}$
+\\[2ex]
+$\inferrule*[left={Abs}]{\Gamma, v:\sigma \vdash t:\tau}{\Gamma
+  \vdash \lambda(v:\sigma).t : \sigma\to\tau}$
+&
+$\inferrule*[left={$\Rightarrow$Int}]{\Gamma, P \vdash Q}{\Gamma
+  \vdash P\Rightarrow Q}$
+\end{tabular}
+
+\bigskip
+
+\itempoint Ce sont \alert{exactement les mêmes règles}, aux
+notations/nommage près…
+
+\smallskip
+
+\itempoint …sauf que la colonne de droite n'a pas le terme typé, mais
+on sait qu'on peut le reconstruire
+(transp. \ref{reconstructing-typed-term}), à partir de l'arbre de
+dérivation.
+
+\smallskip
+
+\itempoint On peut donc \alert{identifier} termes du $\lambda$CST et
+arbres de preuve en déduction naturelle du calcul propositionnel
+intuitionniste restreint au seul connecteur $\Rightarrow$.
+
 \end{frame}
 %
 % TODO:
-- 
cgit v1.2.3