diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 95c0dae..a28dbce 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -944,6 +944,7 @@ partir des hypothèses portées \alert{au-dessus}. \end{frame} % \begin{frame} +\label{example-typing-derivation} \frametitle{Exemple de dérivation} Montrons le jugement selon lequel @@ -1931,6 +1932,36 @@ intuitionniste restreint au seul connecteur $\Rightarrow$. \end{frame} % \begin{frame} +\frametitle{Correspondance de Curry-Howard : exemple avec implication} + +\itempoint Transformons en démonstration le terme +\[\lambda(f:\beta\to\alpha\to\gamma). \lambda(x:\alpha). \lambda(y:\beta). fyx\] +qu'on a typé (transp. \ref{example-typing-derivation}) comme +$(\beta\to\alpha\to\gamma) \to (\alpha\to\beta\to\gamma)$ : + +{\footnotesize +\[ +\inferrule*[left=\llap{$\Rightarrow$Élim}]{ +\inferrule*[left=\llap{$\Rightarrow$Élim}]{ +\inferrule*[left=\llap{$\Rightarrow$Élim}]{ +\inferrule*[left=\llap{$\Rightarrow$Int}]{ +\inferrule*[left=\llap{$\Rightarrow$Int}]{ +\inferrule*[left=\llap{Ax}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle B \Rightarrow A \Rightarrow C ,\\ \scriptscriptstyle A ,B \\ \end{array}$} \vdash B \Rightarrow A \Rightarrow C } +\\ +\inferrule*[right=\rlap{Ax}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle B \Rightarrow A \Rightarrow C ,\\ \scriptscriptstyle A ,B \\ \end{array}$} \vdash B } +}{\mbox{$\begin{array}{cc}\scriptscriptstyle B \Rightarrow A \Rightarrow C ,\\ \scriptscriptstyle A ,B \\ \end{array}$} \vdash A \Rightarrow C } +\\ +\inferrule*[right=\rlap{Ax}]{ }{\mbox{$\begin{array}{cc}\scriptscriptstyle B \Rightarrow A \Rightarrow C ,\\ \scriptscriptstyle A ,B \\ \end{array}$} \vdash A } +}{B \Rightarrow A \Rightarrow C , A , B \vdash C } +}{B \Rightarrow A \Rightarrow C , A \vdash B \Rightarrow C } +}{B \Rightarrow A \Rightarrow C \vdash A \Rightarrow B \Rightarrow C } +}{\vdash (B \Rightarrow A \Rightarrow C ) \Rightarrow (A \Rightarrow B \Rightarrow C )} +\] +\par} + +\end{frame} +% +\begin{frame} \frametitle{Correspondance de Curry-Howard : conjonction} On veut \alert{étendre} le $\lambda$CST avec un \textbf{type produit} |