Lambda-calculus: terms and bound variables.

1 files changed, 112 insertions, 1 deletions

diff --git a/transp-inf110-01-calc.tex b/transp-inf110-01-calc.tex
index ce5467f..011cd7f 100644
--- a/transp-inf110-01-calc.tex
+++ b/transp-inf110-01-calc.tex
@@ -2400,8 +2400,119 @@ Les ensembles \textbf{semi-décidables} sont stables par :
 
 \end{frame}
 %
+\section{Le \texorpdfstring{$\lambda$}{lambda}-calcul non typé}
+\begin{frame}
+\frametitle{Le $\lambda$-calcul : aperçu}
+
+Le \textbf{$\lambda$-calcul non typé} manipule des expressions du type
+\[
+\begin{array}{c}
+\lambda x.\lambda y.\lambda z.((xz)(yz))\\
+\lambda f.\lambda x.f(f(f(f(f(fx)))))\\
+(\lambda x.(xx))(\lambda x.(xx))\\
+\end{array}
+\]
+
+\bigskip
+
+Ces expressions s'appelleront des \textbf{termes} du $\lambda$-calcul.
+
+\bigskip
+
+Il faut comprendre intuitivement qu'un terme représente une sorte de
+fonction qui prend une autre telle fonction en entrée et renvoie une
+autre telle fonction.
+
+\bigskip
+
+Deux constructions fondamentales :
+\begin{itemize}
+\item\textbf{application} : $(PQ)$ : appliquer la fonction $P$ à la
+  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$).
+\end{itemize}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Le $\lambda$-calcul : termes}
+
+\itempoint Un \textbf{terme} du $\lambda$-calcul est (inductivement) :
+\begin{itemize}
+\item une \textbf{variable} ($a$, $b$, $c$... en nombre illimité),
+\item une \textbf{application} $(PQ)$ où $P$ et $Q$ sont deux termes,
+\item une \textbf{abstraction} $\lambda v.E$ où $v$ est une variable
+  et $E$ un terme ; on dira que la variable $v$ est \textbf{liée} dans
+  $E$ par ce $\lambda$.
+\end{itemize}
+
+\bigskip
+
+\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$ ».
+\end{itemize}
+
+\bigskip
+
+\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
+  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}
+\begin{tikzpicture}[remember picture, overlay]
+\draw [->, >=stealth, thick] (bindee) -- ($(bindee.south)+(0pt,-8pt)$) -- ($(binder.south)+(0pt,-8pt)$) -- (binder);
+\end{tikzpicture}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Le $\lambda$-calcul : variables liées}
+
+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 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
+  \alert{plus intérieur} pour ce nom ($\cong$ portée lexicale) :
+  $\lambda x. \lambda x. x \equiv \lambda x. \lambda v. v
+  \mathrel{\textcolor{red}{\not\equiv}} \lambda u. \lambda x. u$.
+\item Mieux vaut ne pas penser aux termes typographiquement, mais à
+  chaque variable liée comme un \emph{pointeur vers la
+  $\lambda$-abstraction qui la lie} :
+\[
+\lambda x. (\lambda y. y (\lambda z. z)) (\lambda z. x z)
+\equiv
+\textcolor{red}{\lambda\bullet}. (\textcolor{yellow}{\lambda\bullet}. \textcolor{yellow}{\bullet} (\textcolor{green}{\lambda\bullet}. \textcolor{green}{\bullet})) (\textcolor{blue}{\lambda\bullet}. \textcolor{red}{\bullet} \textcolor{blue}{\bullet})
+\]
+\item Autre convention possible : \textbf{indices de De Bruijn} :
+  remplacer les variables liées par le numéro du $\lambda$ qui la lie,
+  en comptant du plus intérieur ($1$) vers le plus extérieur :
+\[
+\lambda x. (\lambda y. y (\lambda z. z)) (\lambda z. x z)
+\equiv
+\lambda. (\lambda. 1 (\lambda. 1)) (\lambda. 2 1)
+\]
+deux termes sont $\alpha$-équivalents ssi leur écriture avec indice de
+De Bruijn est identique.
+\end{itemize}
+
+\end{frame}
+%
 % Add somewhere:
-% - busy beaver
 % - "Turing tarpit"
 %
 \end{document}