diff options
Diffstat (limited to 'transp-inf110-01-calc.tex')
| -rw-r--r-- | transp-inf110-01-calc.tex | 144 |
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 |