diff options
| -rw-r--r-- | transp-inf110-01-calc.tex | 135 |
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" % |