More about beta-reduction.

1 files changed, 119 insertions, 16 deletions

diff --git a/transp-inf110-01-calc.tex b/transp-inf110-01-calc.tex
index 011cd7f..49e9603 100644
--- a/transp-inf110-01-calc.tex
+++ b/transp-inf110-01-calc.tex
@@ -1643,7 +1643,7 @@ diagonal donnait l'inexistence d'un programme universel
 \begin{frame}
 \frametitle{Comparaison fonctions primitives récursives et générales récursives}
 
-\textcolor{purple}{Récapitulation :}
+\textcolor{violet}{Récapitulation :}
 
 \medskip
 
@@ -2431,7 +2431,7 @@ Deux constructions fondamentales :
   fonction $Q$ ;
 \item\textbf{abstraction} : $\lambda v.E$ : créer la fonction qui
   prend un argument et le remplace pour $v$ dans l'expression $E$
-  (\alert{en gros} $v \mapsto E$).
+  (\textcolor{teal}{en gros} $v \mapsto E$).
 \end{itemize}
 
 \end{frame}
@@ -2448,30 +2448,33 @@ Deux constructions fondamentales :
   $E$ par ce $\lambda$.
 \end{itemize}
 
-\bigskip
+\medskip
 
 \itempoint Conventions d'écriture :
 \begin{itemize}
 \item l'application \alert{n'est pas associative} : on parenthèse
   implicitement vers la gauche : « $xyz$ » signifie « $((xy)z)$ » ;
 \item abréviation de plusieurs $\lambda$ : on note « $\lambda uv.E$ »
-  pour « $\lambda u. \lambda v. E$ ».
+  pour « $\lambda u. \lambda v. E$ » ;
+\item l'abstraction est moins prioritaire que l'application :
+  « $\lambda x.xy$ » signifie $\lambda x.(xy)$ \alert{pas} $(\lambda
+  x.x)y$.
 \end{itemize}
 
-\bigskip
+\medskip
 
-\itempoint Variables libres et liées :
-\begin{itemize}
-\item une variable non liée est dite \textbf{libre} : $(\lambda
-  x.x)\textcolor{red}{x}$ (le dernier $\textcolor{red}{x}$ est libre),
-\item les variables liées sont muettes : $\lambda x.x \equiv \lambda
+\itempoint Une variable non liée est dite \textbf{libre} : $(\lambda
+  x.x)\textcolor{red}{x}$ (le dernier $\textcolor{red}{x}$ est libre).
+
+\itempoint Un terme sans variable libre est dit \textbf{clos}.
+
+\itempoint Les variables liées sont muettes : $\lambda x.x \equiv \lambda
   y.y$, comprendre $\mathord{\tikz[remember picture, baseline =
       (binder.base), inner sep = 0pt] {\node (binder)
-      {$\lambda\bullet$};}}.\mathord{\tikz[remember picture, baseline =
-      (bindee.base), inner sep = 0pt] {\node (bindee) {$\bullet$};}}$.
-\end{itemize}
+      {\strut$\lambda\bullet$};}}.\mathord{\tikz[remember picture, baseline =
+      (bindee.base), inner sep = 0pt] {\node (bindee) {\strut$\bullet$};}}$.
 \begin{tikzpicture}[remember picture, overlay]
-\draw [->, >=stealth, thick] (bindee) -- ($(bindee.south)+(0pt,-8pt)$) -- ($(binder.south)+(0pt,-8pt)$) -- (binder);
+\draw [->, >=stealth, thick] (bindee.north) -- ($(bindee.north)+(0pt,8pt)$) -- ($(binder.north)+(0pt,8pt)$) -- (binder.north);
 \end{tikzpicture}
 
 \end{frame}
@@ -2482,8 +2485,8 @@ Deux constructions fondamentales :
 On appelle \textbf{$\alpha$-conversion} le renommage des variables
 liées : ces termes sont considérés comme équivalents.
 \begin{itemize}
-\item $\lambda x.x \equiv \lambda y.y$ et $\lambda x.\lambda y.\lambda
-  z.((xz)(yz)) \equiv \lambda u.\lambda v.\lambda w.((uw)(vw))$
+\item $\lambda x.x \equiv \lambda y.y$ et $\lambda xyz.((xz)(yz))
+  \equiv \lambda uvw.((uw)(vw))$
 \item Attention à \alert{ne pas capturer} de variable libre : $\lambda
   y.xy \mathrel{\textcolor{red}{\not\equiv}} \lambda x.xx$.
 \item En cas de synonymie, la variable est liée par le $\lambda$ le
@@ -2512,6 +2515,106 @@ De Bruijn est identique.
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{Le $\lambda$-calcul : $\beta$-réduction}
+
+{\footnotesize On travaille sur des termes à $\alpha$-équivalence
+  près.\par}
+
+\bigskip
+
+\itempoint Un \textbf{redex} (« reducible expression ») est un terme
+de la forme $(\lambda v. E)T$.
+
+Son \textbf{reduct} est le terme $E[v\backslash T]$ obtenu par
+remplacement de $T$ pour $v$ dans $E$, en évitant tout conflit de
+variables.
+
+\medskip
+
+Exemples :
+\begin{itemize}
+\item $(\lambda x.xx)y \rightarrow yy$
+\item $(\lambda x.xx)(\lambda x.xx) \rightarrow (\lambda x.xx)(\lambda
+  x.xx)$ (est son propre reduct)
+\item $(\lambda xy.x)z \rightarrow \lambda y.z$ (car $\lambda xy.x$
+  abrège $\lambda x.\lambda y.x$)
+\item $(\lambda xy.x)y \rightarrow \lambda y_1.y$ (attention au
+  conflit de variable !)
+\item $(\lambda x.\lambda x.x)y \rightarrow \lambda x.x$ (car $\lambda
+  x.\lambda x.x \equiv \lambda z.\lambda x.x$ : le $\lambda$ extérieur
+  ne lie rien)
+\end{itemize}
+
+\bigskip
+
+\itempoint Un terme n'ayant \alert{pas de redex en sous-expression}
+est dit en \textbf{forme ($\beta$-)normale}.\quad  Ex. : $\lambda
+xyz.((xz)(yz))$.
+
+\smallskip
+
+\itempoint On appelle \textbf{$\beta$-réduction} le remplacement en
+sous-expression d'une \textcolor{purple}{redex} par son
+\textcolor{olive}{reduct}.\quad Ex. : $\lambda
+x. \textcolor{purple}{(\lambda y. y (\lambda z. z)) (\lambda z. x z)}
+\rightarrow \lambda x. \textcolor{olive}{(\lambda z. x z)(\lambda
+  z. z)}$.
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Le $\lambda$-calcul : normalisation par $\beta$-réductions}
+
+On note :
+\begin{itemize}
+\item $T \rightarrow T'$ (ou $T \rightarrow_\beta T'$) si $T'$
+  s'obtient par $\beta$-réduction d'un redex de $T$.
+\item $T \twoheadrightarrow T'$ (ou $T \twoheadrightarrow_\beta T'$)
+  si $T'$ s'obtient par une suite finie de $\beta$-réductions ($T =
+  T_0 \rightarrow \cdots \rightarrow T_n = T'$, y compris $n=0$ soit
+  $T'=T$).
+\item $T$ est \textbf{faiblement normalisable} lorsque $T
+  \twoheadrightarrow T'$ avec $T'$ en forme normale (\alert{une
+    certaine} suite de $\beta$-réductions termine).
+\item $T$ est \textbf{fortement normalisable} lorsque \alert{toute}
+  suite de $\beta$-réductions termine (sur un terme en forme normale).
+\end{itemize}
+
+\bigskip
+
+Exemples :
+\begin{itemize}
+\item $(\lambda x.xx)(\lambda x.xx)$ n'est pas faiblement
+  normalisable (la $\beta$-réduction boucle).
+\item $(\lambda uz.z)((\lambda x.xx)(\lambda x.xx))$ n'est
+  pas fortement normalisable mais il est faiblement normalisable
+  $\rightarrow \lambda z.z$.
+\item $(\lambda uz.u)((\lambda t.t)(\lambda x.xx))$ est fortement
+  normalisable $\twoheadrightarrow \lambda zx.xx$.
+\end{itemize}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Le $\lambda$-calcul : confluence et choix d'un redex}
+
+\itempoint\textbf{Théorème} (Church-Rosser) : si $T \twoheadrightarrow
+T'_1$ et $T \twoheadrightarrow T'_2$ alors il existe $T''$ tel que
+$T'_1 \twoheadrightarrow T''$ et $T''_2 \twoheadrightarrow T''$.
+
+\smallskip
+
+En particulier, si $T'_1, T'_2$ sont en forme normale, alors $T'_1
+\equiv T'_2$ (unicité de la normalisation).
+
+\bigskip
+
+Pour \alert{éviter} ce théorème, on va faire un choix de redex à
+réduire :
+
+\end{frame}
+%
 % Add somewhere:
 % - "Turing tarpit"
 %