diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 18 |
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 |