Try to make description of S,K,I combinators slightly less confusing.

1 files 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