From 4291138334c208ab48c0209cf384a91a6d74058d Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Tue, 12 Dec 2023 16:52:14 +0100
Subject: Slightly expand slide on Hilbert system.
---
transp-inf110-02-typage.tex | 15 +++++++++++++--
1 file 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:
--
cgit v1.2.3