summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorDavid A. Madore <david+git@madore.org>2023-10-20 22:11:55 +0200
committerDavid A. Madore <david+git@madore.org>2023-10-20 22:11:55 +0200
commitc08e67930d39631393d09027fa37a8d684a9b38f (patch)
tree411dd09331abd2462aa109baf830e55f54218214
parente785929bd9fa1d6ed3bf65e5d7f13f446a805bc6 (diff)
downloadinf110-lfi-c08e67930d39631393d09027fa37a8d684a9b38f.tar.gz
inf110-lfi-c08e67930d39631393d09027fa37a8d684a9b38f.tar.bz2
inf110-lfi-c08e67930d39631393d09027fa37a8d684a9b38f.zip
More about beta-reduction.
-rw-r--r--transp-inf110-01-calc.tex135
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"
%