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