diff options
Diffstat (limited to 'transp-inf110-01-calc.tex')
| -rw-r--r-- | transp-inf110-01-calc.tex | 101 |
1 files changed, 99 insertions, 2 deletions
diff --git a/transp-inf110-01-calc.tex b/transp-inf110-01-calc.tex index 49e9603..050ee4f 100644 --- a/transp-inf110-01-calc.tex +++ b/transp-inf110-01-calc.tex @@ -2610,8 +2610,105 @@ En particulier, si $T'_1, T'_2$ sont en forme normale, alors $T'_1 \bigskip -Pour \alert{éviter} ce théorème, on va faire un choix de redex à -réduire : +Pour \alert{éviter} ce théorème, on va faire un choix simple de redex +à réduire : + +\itempoint On appelle \textbf{redex extérieur gauche} d'un +$\lambda$-terme le redex dont le $\lambda$ est \alert{le plus à + gauche}. Exemples : $\lambda x.x(\textcolor{purple}{(\lambda + y.y)x})$ ; $\lambda x.(\textcolor{purple}{\lambda y.(\lambda + z.z)y})x$. + +\medskip + +\itempoint On écrira $T \rightarrow_{\mathsf{lft}} T'$ lorsque $T'$ +s'obtient par $\beta$-réduction du redex extérieur gauche, et $T +\twoheadrightarrow_{\mathsf{lft}} T'$ pour une suite de telles +réductions. + +\bigskip + +On peut montrer : + +\itempoint\textbf{Théorème} (Curry \&al) : si $T \twoheadrightarrow +T'$ avec $T'$ en forme normale, alors $T +\twoheadrightarrow_{\mathsf{lft}} T'$ (i.e., la réduction ext. +gauche normalise les termes faiblement normalisables). + +\end{frame} +% +\begin{frame} +\frametitle{Réduction extérieure gauche : exemples} + +{\footnotesize Divers noms utilisés : « réduction en ordre normal », + « réduction gauche », etc.\par} + +\bigskip + +On a noté $T \twoheadrightarrow_{\mathsf{lft}} T'$ lorsque $T'$ +s'obtient par une succession de $\beta$-réductions à chaque fois du +redex dont le $\lambda$ est le plus à gauche. + +\bigskip + +Exemples : +\begin{itemize} +\item $\textcolor{purple}{(\lambda x.xx)(\lambda x.xx)} + \rightarrow_{\mathsf{lft}} (\lambda x.xx)(\lambda x.xx) + \rightarrow_{\mathsf{lft}} \cdots$ (boucle) +\item $(\lambda uz.z)((\lambda x.xx)(\lambda x.xx)) = + \textcolor{purple}{(\lambda u.\lambda z.z)((\lambda x.xx)(\lambda + x.xx))} \rightarrow_{\mathsf{lft}} \lambda z.z$ +\item $(\lambda uz.u)((\lambda t.t)(\lambda x.xx)) = + \textcolor{purple}{(\lambda u.\lambda z.u)((\lambda t.t)(\lambda + x.xx))} \rightarrow_{\mathsf{lft}} \lambda + z.(\textcolor{purple}{(\lambda t.t)(\lambda x.xx)}) + \rightarrow_{\mathsf{lft}} \lambda z.\lambda x.xx = \lambda zx.xx$ +\end{itemize} + +\bigskip + +Intérêt : +\begin{itemize} +\item cette stratégie de réduction est \alert{déterministe}, +\item (Curry \&al :) si (« terme faiblement normalisant ») une + réduction quelconque tombe sur une forme normale, alors + $\twoheadrightarrow_{\mathsf{lft}}$ le fait. +\end{itemize} + +\end{frame} +% +\begin{frame} +\frametitle{Entiers de Church} + +On définit les termes en forme normale $\underline{n} := \lambda +fx.f^{(n)}(x)$ pour $n\in\mathbb{N}$, c-à-d : +\begin{itemize} +\item $\underline{0} := \lambda fx.x$ +\item $\underline{1} := \lambda fx.fx$ +\item $\underline{2} := \lambda fx.f(fx)$ +\item $\underline{3} := \lambda fx.f(f(fx))$, etc. +\end{itemize} + +{\footnotesize Intuitivement, $\underline{n}$ prend une fonction + $f$ et renvoie sa $n$-ième itérée.\par} + +\medskip + +\itempoint Posons $A := \lambda mfx.f(mfx) = \lambda m.\lambda +f.\lambda x.f(mfx)$ + +Alors +\[ +\begin{aligned} +A\underline{n} &= (\lambda m.\lambda f.\lambda x.f(mfx))(\lambda +g.\lambda y.g^{(n)}(y))\\ +& \rightarrow_{\mathsf{lft}} \lambda f.\lambda +x.f(((\lambda g.\lambda y.g^{(n)}(y)))fx)\\ +&\rightarrow_{\mathsf{lft}}\rightarrow_{\mathsf{lft}} \lambda f.\lambda +x.f(f^{(n)}(x)) = \lambda f.\lambda x.f^{(n+1)}(x) = \underline{n+1} +\end{aligned} +\] \end{frame} % |