Much longer explanation of the Y (and also Z) combinator.

1 files changed, 139 insertions, 5 deletions

diff --git a/transp-inf110-01-calc.tex b/transp-inf110-01-calc.tex
index 94b44f6..9034397 100644
--- a/transp-inf110-01-calc.tex
+++ b/transp-inf110-01-calc.tex
@@ -3509,8 +3509,141 @@ Idée :
 
 \bigskip
 
-\itempoint Permet d'implémenter la récursion, comme dans le
-transp. \ref{recursion-from-kleene-recursion-theorem}.
+\itempoint Permet d'implémenter les appels récursifs (transp. suivant).
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Récursion avec le combinateur $\mathsf{Y}$}
+
+\itempoint On veut implémenter une définition par appels récursifs
+dans le $\lambda$-calcul, $\texttt{let~rec~}h = (\ldots h\ldots)$,
+disons $\texttt{let~rec~}h = E$ où $E = (\ldots h\ldots)$ est un terme
+faisant intervenir $h$.
+
+\smallskip
+
+{\footnotesize L'idée est comme dans le
+  transp. \ref{recursion-from-kleene-recursion-theorem}.\par}
+
+\medskip
+
+\itempoint On considère le terme :
+\[
+\begin{aligned}
+\mathsf{Y}(\lambda h.E)
+&= (\lambda f. ((\lambda x.f(x x)) (\lambda x.f(x x))))(\lambda h.E)\\
+&\rightarrow (\lambda x.(\lambda h.E)(x x)) (\lambda x.(\lambda h.E)(x x))
+=: h_{\mathrm{fix}}\\
+&\rightarrow (\lambda h.E)((\lambda x.(\lambda h.E)(x x)) (\lambda x.(\lambda h.E)(x x)))
+= (\lambda h.E)(h_{\mathrm{fix}})\\
+&\rightarrow E[h\backslash h_{\mathrm{fix}}]
+\text{~(substitution de $h_{\mathrm{fix}}$ pour $h$ dans $E$)}
+\end{aligned}
+\]
+
+Donc $h_{\mathrm{fix}}$ (et donc $\mathsf{Y}(\lambda h.E)$) se
+comporte, à des $\beta$-réductions près, comme la fonction récursive
+recherchée.
+
+\medskip
+
+\itempoint Si l'évaluation (i.e., la $\beta$-réduction) de $E$ termine
+et ne fait pas intervenir $h$, alors $h_{\mathrm{fix}}$ donne juste
+$E$, sinon elle itère avec $h_{\mathrm{fix}}$ pour $h$ jusqu'à ce que
+ce soit le cas : c'est bien ce que fait un appel récursif.
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Digression / variante : le combinateur $\mathsf{Z}$}
+
+\itempoint Le bon fonctionnement du combinateur $\mathsf{Y}$ dépend du
+fait que la stratégie de $\beta$-réduction utilisée est extérieure
+gauche.  Sinon le redex $(\lambda x.f(x x)) (\lambda x.f(x x))$ peut
+causer un cycle de $\beta$-réductions.
+
+\medskip
+
+\itempoint La variante suivante évite ce problème pour définir une
+fonction par appels récursifs dans un langage qui n'évalue pas « dans
+les $\lambda$ » :
+\[
+\mathsf{Z} := \lambda f. ((\lambda x.f(\lambda v.x x v)) (\lambda x.f(\lambda v.x x v)))
+\]
+
+Cette fois :
+\[
+\begin{aligned}
+\mathsf{Z}(\lambda h.E)
+&= (\lambda f. ((\lambda x.f(\lambda v.x x v)) (\lambda x.f(\lambda v.x x v))))(\lambda h.E)\\
+&\rightarrow (\lambda x.(\lambda h.E)(\lambda v.x x v)) (\lambda x.(\lambda h.E)(\lambda v.x x v))
+=: h_{\mathrm{fix}}\\
+&\rightarrow (\lambda h.E)(\lambda v.(\lambda x.(\lambda h.E)(x x)) (\lambda x.(\lambda h.E)(x x))v)
+= (\lambda h.E)(\lambda v. h_{\mathrm{fix}} v)\\
+&\rightarrow E[h\backslash \lambda v. h_{\mathrm{fix}} v]
+\text{~(substitution de $\lambda v. h_{\mathrm{fix}} v$ pour $h$ dans $E$)}
+\end{aligned}
+\]
+La forme $\lambda v. h_{\mathrm{fix}} v$ maintient $h_{\mathrm{fix}}$
+non-évalué (exemple transp. suivant).
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Digression (suite) : exemple en Scheme}
+
+{\footnotesize On prend ici l'exemple de Scheme pour avoir affaire à
+  un langage fonctionnel non typé (le typage empêche l'implémentation
+  directe du combinateur $\mathsf{Y}$ ou $\mathsf{Z}$ en OCaml ou
+  Haskell).\par}
+
+\bigskip
+
+\itempoint Récursion sans combinateurs :
+
+{\tt
+(define proto-fibonacci\\
+\ \ (lambda (self) ; Pass me as argument!\\
+\ \ \ \ (lambda (n)\\
+\ \ \ \ \ \ (if (<= n 1) n\\
+\ \ \ \ \ \ \ \ \ \ (+ ((self self) (- n 1)) ((self self) (- n 2)))))))\\
+(define fibonacci (proto-fibonacci proto-fibonacci))\\
+(map fibonacci '(0 1 2 3 4 5 6))\\
+$\rightarrow$ (0 1 1 2 3 5 8)
+\par}
+
+\medskip
+
+\itempoint L'idée est ici exactement celle de l'astuce de Quine : pour
+m'appeler « moi-même », je m'attends à me recevoir moi-même en
+argument, et je reproduis ceci lors de l'appel.
+
+\medskip
+
+\itempoint Le combinateur $\mathsf{Y}$ (ou $\mathsf{Z}$) automatise
+cette construction.
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Digression (suite) : exemple en Scheme}
+
+{\tt
+;; (define y-combinator\\
+;; \ \ (lambda (f)\\
+;; \ \ \ \ ((lambda (x) (f (x x))) (lambda (x) (f (x x))))))\\
+(define z-combinator\\
+\ \ (lambda (f)\\
+\ \ \ \ ((lambda (x) (f (lambda (v) ((x x) v))))\\
+\ \ \ \ \ (lambda (x) (f (lambda (v) ((x x) v)))))))\\
+(define pre-fibonacci\\
+\ \ (lambda (fib)\\
+\ \ \ \ (lambda (n)\\ 
+\ \ \ \ \ \ (if (<= n 1) n\\
+\ \ \ \ \ \ \ \ \ \ (+ (fib (- n 1)) (fib (- n 2)))))))\\
+(define fibonacci (z-combinator pre-fibonacci))\\
+\par}
 
 \end{frame}
 %
@@ -3523,8 +3656,8 @@ transp. \ref{recursion-from-kleene-recursion-theorem}.
 
 \bigskip
 
-\itempoint On veut représenter l'algorithme « rechercher à partir
-de $z$ » :
+\itempoint On peut faire l'algorithme « rechercher à partir
+de $z$ » par appels récursifs :
 \[
 h(z,x_1,\ldots,x_k) = \left\{
 \begin{array}{l}
@@ -3533,8 +3666,9 @@ h(z+1,x_1,\ldots,x_k)\quad\text{~(récursivement)~sinon}\\
 \end{array}
 \right.
 \]
+{\footnotesize Alors $\mu g(x_1,\ldots,x_k) = h(0,x_1,\ldots,x_k)$.\par}
 
-\bigskip
+\medskip
 
 \itempoint $T := \lambda pmn.p(\lambda y.n)m$ représente $(p,m,n)
 \mapsto \left\{\begin{array}{ll}m&\text{~si~}p=0\\n&\text{~si~}p\geq