From 88c2c12c57568de9edac5ff2775aab7bb0ebf287 Mon Sep 17 00:00:00 2001 From: "David A. Madore" Date: Fri, 15 Dec 2023 17:39:27 +0100 Subject: Try to make description of S,K,I combinators slightly less confusing. --- transp-inf110-02-typage.tex | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 188b7eb..19bc7ae 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -3207,12 +3207,12 @@ $A,B,C,\ldots$ sont \alert{remplacés par des formules qcqes} : \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$ -\quad \itempoint $A\Rightarrow B \Rightarrow A\land B$ +\quad\itempoint $A\land B \Rightarrow B$ +\quad\itempoint $A\Rightarrow B \Rightarrow A\land B$ +\quad\itempoint $\top$ \quad\itempoint $\bot \Rightarrow C$ \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$ +\quad\itempoint $B \Rightarrow A \lor B$ +\quad\itempoint $(A\Rightarrow C)\Rightarrow(B\Rightarrow C)\Rightarrow (A\lor B\Rightarrow C)$ \end{itemize} \par} @@ -3228,9 +3228,11 @@ non typé comme simplement typé. {\footnotesize (On n'a même pas besoin de \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$. +\itempoint Idée de la conversion : remplacer $\lambda x.x$ par +$\mathsf{I}$, $\lambda x.y$ par $\mathsf{K}y$ (si $x$ n'apparaît pas +dans $y$) et $\lambda x.uv$ par $\mathsf{S}(\lambda x.u)(\lambda +x.v)$. {\footnotesize (On peut aussi « $\eta$-convertir » $\lambda + x.fx$ en $f$.)} {\footnotesize P.ex. : $\lambda f.\lambda x.f(fx)$ se réécrit $\lambda f. \mathsf{S}(\mathsf{K}f)f$ donc -- cgit v1.2.3