diff options
-rw-r--r-- | transp-inf110-01-calc.tex | 113 |
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} |