Outermost-leftmost (normal order) reduction; Church numerals.

1 files changed, 99 insertions, 2 deletions

diff --git a/transp-inf110-01-calc.tex b/transp-inf110-01-calc.tex
index 49e9603..050ee4f 100644
--- a/transp-inf110-01-calc.tex
+++ b/transp-inf110-01-calc.tex
@@ -2610,8 +2610,105 @@ En particulier, si $T'_1, T'_2$ sont en forme normale, alors $T'_1
 
 \bigskip
 
-Pour \alert{éviter} ce théorème, on va faire un choix de redex à
-réduire :
+Pour \alert{éviter} ce théorème, on va faire un choix simple de redex
+à réduire :
+
+\itempoint On appelle \textbf{redex extérieur gauche} d'un
+$\lambda$-terme le redex dont le $\lambda$ est \alert{le plus à
+  gauche}.  Exemples : $\lambda x.x(\textcolor{purple}{(\lambda
+  y.y)x})$ ; $\lambda x.(\textcolor{purple}{\lambda y.(\lambda
+  z.z)y})x$.
+
+\medskip
+
+\itempoint On écrira $T \rightarrow_{\mathsf{lft}} T'$ lorsque $T'$
+s'obtient par $\beta$-réduction du redex extérieur gauche, et $T
+\twoheadrightarrow_{\mathsf{lft}} T'$ pour une suite de telles
+réductions.
+
+\bigskip
+
+On peut montrer :
+
+\itempoint\textbf{Théorème} (Curry \&al) : si $T \twoheadrightarrow
+T'$ avec $T'$ en forme normale, alors $T
+\twoheadrightarrow_{\mathsf{lft}} T'$ (i.e., la réduction ext.
+gauche normalise les termes faiblement normalisables).
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Réduction extérieure gauche : exemples}
+
+{\footnotesize Divers noms utilisés : « réduction en ordre normal »,
+  « réduction gauche », etc.\par}
+
+\bigskip
+
+On a noté $T \twoheadrightarrow_{\mathsf{lft}} T'$ lorsque $T'$
+s'obtient par une succession de $\beta$-réductions à chaque fois du
+redex dont le $\lambda$ est le plus à gauche.
+
+\bigskip
+
+Exemples :
+\begin{itemize}
+\item $\textcolor{purple}{(\lambda x.xx)(\lambda x.xx)}
+  \rightarrow_{\mathsf{lft}} (\lambda x.xx)(\lambda x.xx)
+  \rightarrow_{\mathsf{lft}} \cdots$ (boucle)
+\item $(\lambda uz.z)((\lambda x.xx)(\lambda x.xx)) =
+  \textcolor{purple}{(\lambda u.\lambda z.z)((\lambda x.xx)(\lambda
+    x.xx))} \rightarrow_{\mathsf{lft}} \lambda z.z$
+\item $(\lambda uz.u)((\lambda t.t)(\lambda x.xx)) =
+  \textcolor{purple}{(\lambda u.\lambda z.u)((\lambda t.t)(\lambda
+    x.xx))} \rightarrow_{\mathsf{lft}} \lambda
+  z.(\textcolor{purple}{(\lambda t.t)(\lambda x.xx)})
+  \rightarrow_{\mathsf{lft}} \lambda z.\lambda x.xx = \lambda zx.xx$
+\end{itemize}
+
+\bigskip
+
+Intérêt :
+\begin{itemize}
+\item cette stratégie de réduction est \alert{déterministe},
+\item (Curry \&al :) si (« terme faiblement normalisant ») une
+  réduction quelconque tombe sur une forme normale, alors
+  $\twoheadrightarrow_{\mathsf{lft}}$ le fait.
+\end{itemize}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Entiers de Church}
+
+On définit les termes en forme normale $\underline{n} := \lambda
+fx.f^{(n)}(x)$ pour $n\in\mathbb{N}$, c-à-d :
+\begin{itemize}
+\item $\underline{0} := \lambda fx.x$
+\item $\underline{1} := \lambda fx.fx$
+\item $\underline{2} := \lambda fx.f(fx)$
+\item $\underline{3} := \lambda fx.f(f(fx))$, etc.
+\end{itemize}
+
+{\footnotesize Intuitivement, $\underline{n}$ prend une fonction
+  $f$ et renvoie sa $n$-ième itérée.\par}
+
+\medskip
+
+\itempoint Posons $A := \lambda mfx.f(mfx) = \lambda m.\lambda
+f.\lambda x.f(mfx)$
+
+Alors
+\[
+\begin{aligned}
+A\underline{n} &= (\lambda m.\lambda f.\lambda x.f(mfx))(\lambda
+g.\lambda y.g^{(n)}(y))\\
+& \rightarrow_{\mathsf{lft}} \lambda f.\lambda
+x.f(((\lambda g.\lambda y.g^{(n)}(y)))fx)\\
+&\rightarrow_{\mathsf{lft}}\rightarrow_{\mathsf{lft}} \lambda f.\lambda
+x.f(f^{(n)}(x)) = \lambda f.\lambda x.f^{(n+1)}(x) = \underline{n+1}
+\end{aligned}
+\]
 
 \end{frame}
 %