Curry-Howard correspondence for implication alone.

1 files changed, 44 insertions, 0 deletions

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
@@ -1884,6 +1885,49 @@ A. Troelstra et d'autres :
 
 \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:
 % - substitution des variables propositionnelles par des formules
 % - substitution d'équivalences