diff options
| -rw-r--r-- | exercices-inf110.tex | 121 |
1 files changed, 120 insertions, 1 deletions
diff --git a/exercices-inf110.tex b/exercices-inf110.tex index 1045209..1d1e8cc 100644 --- a/exercices-inf110.tex +++ b/exercices-inf110.tex @@ -1224,9 +1224,128 @@ z.xz)y \rightarrow_\beta \lambda y.\lambda z.yz = \lambda yz.yz % +\exercice\ (${\star}$)\par\nobreak + +\textbf{(1)} Considérons le terme $T_2 := (\lambda x.xxx)(\lambda +x.xxx)$ du $\lambda$-calcul non typé. Étudier le graphe des +$\beta$-réductions dessus, c'est-à-dire tous les termes obtenus par +$\beta$-réduction à partir de $T_2$, et les $\beta$-réductions entre +eux. + +\textbf{(2)} Que se passe-t-il pour $V := (\lambda x.x(xx))(\lambda +x.x(xx))$ ? Sans entrer dans les détails, on donnera quelques chemins +de $\beta$-réduction, notamment celui suivi par la réduction +extérieure gauche. + +\textbf{(3)} Étudier de façon analogue le comportement du terme $R +:= (\lambda x.\lambda v.xxv) (\lambda x.\lambda v.xxv)$ sous l'effet +de la $\beta$-réduction. + +\begin{corrige} +\textbf{(1)} La $\beta$-réduction du seul redex de $T_2$ s'écrit +$(\lambda x.xxx)(\lambda x.xxx) \rightarrow (\lambda x.xxx)(\lambda +x.xxx)(\lambda x.xxx)$. Appelons $T_3$ le terme en question, et plus +généralement $T_n$ le terme $(\lambda x.xxx)\cdots (\lambda x.xxx)$ +avec $n-1$ applications sur $(\lambda x.xxx)$ de $(\lambda x.xxx)$ +(donc $n$ fois ce sous-terme au total) ; on se rappellera bien que les +parenthèses sont vers la \emph{gauche}, c'est-à-dire que $T_4$ est +$((T_1 T_1)T_1)T_1$ par exemple. Il y a un \emph{unique} redex dans +$T_n$ (bien qu'il y ait $n$ lambdas, un seul est appliqué), à savoir +celui des deux $T_1$ les plus à gauche (ou les plus profondément +imbriqués) : la seule $\beta$-réduction possible consiste à remplacer +ce redex $T_1 T_1$ (soit $T_2$) par son réduit $(T_1 T_1) T_1$ +(soit $T_3$), ce qui donne $T_{n+1}$. Le graphe des +$\beta$-réductions est donc $T_2 \rightarrow T_3 \rightarrow T_4 +\rightarrow \cdots$ avec une unique $\beta$-réduction possible à +chaque fois. Le terme n'est pas faiblement (ni à plus forte raison +fortement) normalisable. + +\textbf{(2)} La $\beta$-réduction du seul redex donne $(\lambda +x.x(xx))(\lambda x.x(xx)) \rightarrow (\lambda x.x(xx))((\lambda +x.x(xx))(\lambda x.x(xx)))$. Notant $U := \lambda x.x(xx)$ pour y +voir plus clair, on a donc $V := UU \rightarrow U(UU)$. Maintenant on +a deux possibilités de redex à réduire : le redex extérieur $U(UU)$ +formé par l'expression tout entière, et le redex intérieur $UU$. Le +redex extérieur $U(UU)$ se réduit en $(UU)((UU)(UU))$ (qui a +maintenant trois redex), tandis que la réduction du redex intérieur +$UU$ dans $U(UU)$ donne $U(U(UU))$. Il est alors facile de construire +toutes sortes de chemins de $\beta$-réductions en se rappelant que +tout $UX$ est un redex, avec pour réduit $X(XX)$. On peut notamment +distinguer la réduction intérieure gauche (ou droite, ici elles +coïncident) +\[ +UU \rightarrow U(UU) \rightarrow U(U(UU)) \rightarrow U(U(U(UU))) +\rightarrow U(U(U(U(UU)))) \cdots +\] +et la réduction extérieure gauche (on utilise $V := UU$ pour plus de +clarté ; mais on gardera bien à l'esprit que $V$, contrairement à $U$, +n'est pas une abstraction donc ne forme pas un redex quand on +l'applique, par contre c'est lui-même un redex qui se réduit en $UV$) +\[ +\begin{aligned} +UU := V &\rightarrow UV \rightarrow V(VV) \rightarrow (UV)(VV) +\rightarrow (V(VV))(VV)\\ +&\rightarrow ((UV)(VV))(VV) \rightarrow ((VV)(VV))(VV) +\rightarrow \cdots +\end{aligned} +\] +ou encore la réduction extérieure droite +\[ +\begin{aligned} +UU := V &\rightarrow UV \rightarrow V(VV) \rightarrow V(V(UV)) +\rightarrow V(V(V(VV)))\\ +&\rightarrow V(V(V(V(UV)))) \rightarrow V(V(V(V(V(VV))))) +\rightarrow \cdots +\end{aligned} +\] +Aucun de ces chemins ne termine (on a vu en cours que si la réduction +extérieure gauche ne termine pas, aucun chemin de $\beta$-réductions +ne termine, mais ici c'est clair car une $\beta$-réduction ne peut de +toute façon qu'augmenter le nombre de $U$ dans l'expression). + +(Seule la notion de réduction extérieure gauche a été définie en +cours ; on peut néanmoins définir sans difficulté les quatre +réductions extérieure gauche, intérieure gauche, extérieure droite et +intérieure droite : le redex extérieur gauche est celui dont le bord +gauche est le plus à gauche, le redex intérieur gauche est celui dont +le bord droit est le plus à gauche, le redex extérieur droite est +celui dont le bord droit est le plus à droite, et le redex intérieur +droite est celui dont le bord gauche est le plus à droite. Peu +importent ces définitions, cependant, ici le but est simplement +d'illustrer quelques chemins possibles.) + +(\emph{Remarque :} Je n'ai pas réfléchi à trouver une caractérisation +de tous les termes en lesquels $UU$ peut se réduire, mais on peut les +décrire comme des arbres d'application avec $U$ aux feuilles, et la +$\beta$-réduction se voir alors comme une transformation simple sur +les arbres.) + +\textbf{(3)} La $\beta$-réduction du seul redex de $R$ s'écrit +$(\lambda x.\lambda v.xxv) (\lambda x.\lambda v.xxv) \rightarrow +\lambda v.(\lambda x.\lambda v.xxv)(\lambda x.\lambda v.xxv)v = +\lambda v. R v$. On peut alors continuer ainsi : $R \rightarrow +\lambda v. Rv \rightarrow \lambda v. (\lambda v. Rv)v \rightarrow +\lambda v. (\lambda v. (\lambda v. Rv)v)v \rightarrow \cdots$. Même +si ces écritures sont correctes (rappelons que chaque variable est +liée par le $\lambda$ le plus \emph{intérieur} sur son nom), il est +considérablement plus clair de renommer les variables liées, par +exemple ainsi : +\[ +R \rightarrow +\lambda v_1. Rv_1 \rightarrow \lambda v_1. (\lambda v_2. Rv_2)v_1 \rightarrow +\lambda v_1. (\lambda v_2. (\lambda v_3. Rv_3)v_2)v_1 \rightarrow \cdots +\] +(on prendra garde à ne pas confondre le troisième terme de cette +suite, par exemple, avec $\lambda v_1. \lambda v_2. Rv_2v_1$ qui +désigne $\lambda v_1. \lambda v_2. (Rv_2v_1)$ et qui peut s'écrire +$\lambda v_1 v_2. Rv_2v_1$ : ce n'est pas du tout la même chose !). +\end{corrige} + +% + \exercice\ (${\star}{\star}$)\par\nobreak -On considère la traduction évidente des termes du $\lambda$-calcul pur +On considère la traduction évidente des termes du $\lambda$-calcul en langage Python et/ou en Scheme définie de la manière suivante : \begin{itemize} \item une variable se traduit en elle-même (i.e., en |