diff options
| -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 980d0b5..5ccb6f6 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -3176,10 +3176,54 @@ $\inferrule*{ (à gauche le $\lambda$-calcul, à droite le $\overline{\lambda}$-calcul ; remarquez l'inversion des arguments) + +($y$ est une \emph{variable} ici, pas une application ni une abstraction) \end{center} \end{frame} % +\begin{frame} +\frametitle{Combinateurs $\mathsf{S},\mathsf{K},\mathsf{I}$} + +\itempoint\textbf{Axiomes de Hilbert :} le calcul +prop\textsuperscript{nel} intuitionniste peut être défini par la +\alert{seule} règle du modus ponens (« si $P\Rightarrow Q$ et $P$ +alors $Q$ ») à partir des schémas d'axiomes suivants, où +$A,B,C,\ldots$ sont \alert{remplacés par des formules qcqes} : +{\footnotesize +\begin{itemize} +\item $(\mathsf{I}): A\Rightarrow A$ +\item $(\mathsf{K}): A\Rightarrow B\Rightarrow A$ +\item $(\mathsf{S}): (A\Rightarrow B\Rightarrow C) \Rightarrow + (A\Rightarrow B) \Rightarrow (A \Rightarrow C)$ +\item $A\land B \Rightarrow A$ +\quad \itempoint $A\land B \Rightarrow B$ +\quad \itempoint $A\Rightarrow B \Rightarrow A\land B$ +\item $A \Rightarrow A \lor B$ +\quad \itempoint $B \Rightarrow A \lor B$ +\quad \itempoint $(A\Rightarrow C)\Rightarrow(B\Rightarrow C)\Rightarrow (A\lor B\Rightarrow C)$ +\item $\top$ \quad\itempoint $\bot \Rightarrow C$ +\end{itemize} +\par} + +\medskip + +\itempoint Via Curry-Howard, ceci correspond au fait qu'on peut +définir un $\lambda$-terme quelconque (à $\beta$-réduction près) par +application des trois combinateurs $\mathsf{I} := \lambda x.x$, +$\mathsf{K} := \lambda x.\lambda y.x$ et $\mathsf{S} := \lambda +x. \lambda y. \lambda z. xz(yz)$. Ceci vaut pour le $\lambda$-calcul +non typé comme simplement typé. {\footnotesize (On n'a même pas besoin de + $\mathsf{I}$ qui peut s'écrire $\mathsf{SKK}$.)} + +\medskip + +\itempoint Idée de la conversion : remplacer $\lambda x.uv$ par +$\mathsf{S}(\lambda x.u)(\lambda x.v)$ et $\lambda x.y$ par +$\mathsf{K}y$. + +\end{frame} +% % TODO: % - Kripke % - fragment négatif |