diff options
Diffstat (limited to 'transp-inf110-02-typage.tex')
| -rw-r--r-- | transp-inf110-02-typage.tex | 15 |
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: |