Slightly expand slide on Hilbert system.

1 files changed, 13 insertions, 2 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 5ccb6f6..fef2c93 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -3193,8 +3193,8 @@ $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
+\quad\itempoint $(\mathsf{K}): A\Rightarrow B\Rightarrow A$
+\quad\itempoint $(\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$
@@ -3222,6 +3222,17 @@ non typé comme simplement typé.  {\footnotesize (On n'a même pas besoin de
 $\mathsf{S}(\lambda x.u)(\lambda x.v)$ et $\lambda x.y$ par
 $\mathsf{K}y$.
 
+{\footnotesize P.ex. : $\lambda f.\lambda x.f(fx)$ se réécrit $\lambda
+  f. \mathsf{S}(\mathsf{K}f)f$ donc
+  $\mathsf{S}(\mathsf{S}(\mathsf{K}\mathsf{S})\mathsf{K})\mathsf{I}$.\par}
+
+\smallskip
+
+{\footnotesize\itempoint On peut donc en théorie imaginer un langage
+  de programmation fonctionnel Turing-complet sans variables, basé sur
+  les seules fonctions $\mathsf{S}$, $\mathsf{K}$, $\mathsf{I}$.
+  {\tiny(Mais personne ne serait assez fou pour faire ça.)}\par}
+
 \end{frame}
 %
 % TODO: