diff options
Diffstat (limited to 'transp-inf110-02-typage.tex')
| -rw-r--r-- | transp-inf110-02-typage.tex | 44 |
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 |