Another exercise on various "loopy" reductions.

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