diff options
author | David A. Madore <david+git@madore.org> | 2023-10-30 13:02:51 +0100 |
---|---|---|
committer | David A. Madore <david+git@madore.org> | 2023-10-30 13:02:51 +0100 |
commit | b4dee1cfa45dbf0454354e045faff340d658a676 (patch) | |
tree | 568b0eb9fcfd6d22b38a9ef0d09cab35ada14d0f | |
parent | 25f803f0f202805b8ac85d444757026ec39a8d1b (diff) | |
download | inf110-lfi-b4dee1cfa45dbf0454354e045faff340d658a676.tar.gz inf110-lfi-b4dee1cfa45dbf0454354e045faff340d658a676.tar.bz2 inf110-lfi-b4dee1cfa45dbf0454354e045faff340d658a676.zip |
Equivalence of functions representable in the lambda-calculus and recursive functions.
-rw-r--r-- | transp-inf110-01-calc.tex | 209 |
1 files changed, 205 insertions, 4 deletions
diff --git a/transp-inf110-01-calc.tex b/transp-inf110-01-calc.tex index 29dcb18..bba20d9 100644 --- a/transp-inf110-01-calc.tex +++ b/transp-inf110-01-calc.tex @@ -226,7 +226,7 @@ idéalisé \itempoint\textbf{Théorème} (Post, Turing) : les fonctions (disons $\mathbb{N} \dasharrow \mathbb{N}$) \textbf{(1)} générales récursives, -\textbf{(2)} exprimables en $\lambda$-calcul, et +\textbf{(2)} représentables en $\lambda$-calcul, et \textbf{(3)} calculables par machine de Turing, coïncident toutes. \smallskip @@ -865,6 +865,7 @@ langage. \end{frame} % \begin{frame} +\label{kleene-recursion-theorem-p-r-version} \frametitle{Le théorème de récursion de Kleene (version p.r.)} Version formelle de l'astuce de Quine @@ -1523,6 +1524,7 @@ $\varphi^{(k)}_e(\underline{x}) = h(e,\underline{x}) = \end{frame} % \begin{frame} +\label{recursion-from-kleene-recursion-theorem} \frametitle{Récursion !} Le langage des fonctions générales récursives, @@ -1975,7 +1977,7 @@ existe des fonctions p.r. : récursive (et l'arité $k$) et renvoie le code d'une machine de Turing qui calcule cette $\varphi_e^{(k)}$, \item l'autre prend en entrée le code d'une machine de Turing qui - calcule une fonction $f$ et son arité $k$, et renvoie un numéro $e$ + calcule une fonction $f$, et son arité $k$, et renvoie un numéro $e$ de $f$ dans les fonctions générales récursives $f = \varphi_e^{(k)}$. \end{itemize} @@ -2157,7 +2159,7 @@ n\text{~et~}\varphi_e(e)\downarrow\}$ (mêmes propriétés). \begin{itemize} \item générale récursive, \item calculable par machine de Turing, -\item \textcolor{brown}{à voir $\rightarrow$} exprimable dans le $\lambda$-calcul. +\item \textcolor{brown}{à voir $\rightarrow$} représentable dans le $\lambda$-calcul. \end{itemize} \bigskip @@ -2725,13 +2727,51 @@ 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 + réduction quelconque termine sur une forme normale, alors $\twoheadrightarrow_{\mathsf{lft}}$ le fait. \end{itemize} \end{frame} % \begin{frame} +\frametitle{Simulation du $\lambda$-calcul par les fonctions récursives} + +\itempoint On peut coder un terme du $\lambda$-calcul sous forme +d'entiers naturels. + +\bigskip + +\itempoint La fonction $T \mapsto 1$ qui à un terme $T$ associe $0$ si +$t$ est en forme normale et $1$ si non, \textbf{est p.r.} + +\medskip + +\itempoint La fonction $T \mapsto T'$ qui à un terme $T$ associe sa +réduction extérieure gauche \textbf{est p.r.} + +\medskip + +\itempoint Conséquence : la fonction $(n,T) \mapsto T^{(n)}$ qui à +$n\in\mathbb{N}$ et un terme $T$ associe le terme obtenu après $n$ +réductions extérieures gauches \textbf{est p.r.} + +\medskip + +\itempoint La fonction qui à $T$ associe la forme normale (et/ou le +nombre d'étapes d'exécution) \alert{si la réduction extérieure gauche + termine}, et $\uparrow$ (non définie) si elle ne termine pas, est +\textbf{générale récursive}. + +\bigskip + +\textcolor{blue}{\textbf{Moralité :}} les fonctions récursives peuvent +simuler la réduction extérieure gauche du $\lambda$-calcul +{\footnotesize (ou n'importe quelle autre réduction, mais on a choisi + celle-ci)}. + +\end{frame} +% +\begin{frame} \frametitle{Entiers de Church} On définit les termes en forme normale $\overline{n} := \lambda @@ -2912,6 +2952,7 @@ f(x_1,\ldots,x_k,0) &= g(x_1,\ldots,x_k)\\ f(x_1,\ldots,x_k,z+1) &= h(x_1,\ldots,x_k,f(x_1,\ldots,x_k,z),z) \end{aligned} \] +(toujours avec $A := \lambda mfx.f(mfx)$). \bigskip @@ -2927,6 +2968,166 @@ Bref, (au moins) \alert{les fonctions p.r. sont représentables par \end{frame} % +\begin{frame} +\frametitle{Le combinateur $\mathsf{Y}$ de Curry} + +\itempoint Pour représenter toutes les fonctions récursives, on va +implémenter les appels récursifs dans le $\lambda$-calcul. + +\bigskip + +\itempoint Pour ça, on va utiliser la même idée que le théorème de +récursion de Kleene +(transp. \ref{kleene-recursion-theorem-p-r-version}). + +\bigskip + +Posons +\[ +\mathsf{Y} := \lambda f. ((\lambda x.f(x x)) (\lambda x.f(x x))) +\] + +Idée : +\[ +\begin{aligned} +\mathsf{Y} &:= \lambda f. ((\lambda x.f(x x)) (\lambda x.f(x x)))\\ +&\rightarrow \lambda f. f((\lambda x.f(x x)) (\lambda x.f(x x)))\\ +&\rightarrow \lambda f. f(f((\lambda x.f(x x)) (\lambda x.f(x x)))) +\rightarrow \cdots +\end{aligned} +\] + +\itempoint Le terme (non normalisable !) $\mathsf{Y}$ +“\textbf{recherche}” un point fixe de son argument. + +\bigskip + +\itempoint Permet d'implémenter la récursion, comme dans le +transp. \ref{recursion-from-kleene-recursion-theorem}. + +\end{frame} +% +\begin{frame} +\frametitle{Représentation de l'opérateur $\mu$ de Kleene} + +{\footnotesize Rappel : $\mu g(x_1,\ldots,x_k)$ est le plus petit $z$ + tel que $g(z,x_1,\ldots,x_k) = 0$ et $g(i,x_1,\ldots,x_k)\downarrow$ + pour $0\leq i<z$, s'il existe.\par} + +\bigskip + +\itempoint On veut représenter l'algorithme « rechercher à partir +de $z$ » : +\[ +h(z,x_1,\ldots,x_k) = \left\{ +\begin{array}{l} +z\quad\text{~si~}g(z,x_1,\ldots,x_k) = 0\\ +h(z+1,x_1,\ldots,x_k)\quad\text{~(récursivement)~sinon}\\ +\end{array} +\right. +\] + +\bigskip + +\itempoint $T := \lambda pmn.p(\lambda y.n)m$ représente $(p,m,n) +\mapsto \left\{\begin{array}{ll}m&\text{~si~}p=0\\n&\text{~si~}p\geq +1\end{array}\right.$ + +\itempoint $A := \lambda mfx.f(mfx)$ représente $z \mapsto z+1$ + +\bigskip + +\itempoint La récursion est implémentée avec le +combinateur $\mathsf{Y}$ : +\[ +\begin{aligned} +&\mathsf{Y} +(\lambda h z x_1\cdots x_k. +T +(v z x_1\cdots x_k) +z +(h (A z) x_1\cdots x_k) +)\\ +\rightarrow & \mathsf{Y} +(\lambda h z x_1\cdots x_k. +(v z x_1\cdots x_k) +(\lambda y.h (A z) x_1\cdots x_k) +z +)\\ +\end{aligned} +\] + +\end{frame} +% +\begin{frame} +\frametitle{Équivalence entre $\lambda$-calcul et fonctions récursives} + +\itempoint Toute fonction générale récursive (i.e., +\alert{calculable} !) $\mathbb{N}^k \dasharrow \mathbb{N}$ est +représentée par un terme du $\lambda$-calcul (sous les conventions +données : application aux entiers de Church, réduction extérieure +gauche). + +\bigskip + +\itempoint Réciproquement, toute fonction $\mathbb{N}^k \dasharrow +\mathbb{N}$ représentable par un terme du $\lambda$-calcul est +calculable, car on peut implémenter la réduction extérieure gauche. + +\bigskip + +\itempoint Bref, $f\colon \mathbb{N}^k \dasharrow \mathbb{N}$ est +représentable par un terme du $\lambda$-calcul \alert{ssi} elle est +générale récursive. + +\bigskip + +\itempoint De plus, cette équivalence est \alert{constructive} : il +existe des fonctions p.r. : +\begin{itemize} +\item l'une prend en entrée le numéro $e$ d'une fonction générale + récursive (et l'arité $k$) et renvoie le code d'un terme du + $\lambda$-calcul qui représente cette $\varphi_e^{(k)}$, +\item l'autre prend en entrée le code d'un terme du $\lambda$-calcul + qui représente une fonction $f$, et son arité $k$, et renvoie un + numéro $e$ de $f$ dans les fonctions générales récursives $f = + \varphi_e^{(k)}$. +\end{itemize} + +\end{frame} +% +\begin{frame} +\frametitle{Récapitulation} + +\itempoint\textbf{Théorème} : les fonctions $\mathbb{N}^k \dasharrow +\mathbb{N}$ \textbf{(1)} générales récursives, +\textbf{(2)} représentables en $\lambda$-calcul, et +\textbf{(3)} calculables par machine de Turing, coïncident toutes. + +\bigskip + +\centerline{On les appelle les \textbf{fonctions calculables}.} + +\bigskip + +\itempoint De plus, ces équivalences sont constructives : on peut +passer algorithmiquement (= calculablement !) d'une représentation à +l'autre. + +{\footnotesize Ce sont des formes de \alert{compilation} d'un langage + en un autre.\par} + +\bigskip + +\itempoint Les questions suivantes \alert{ne sont pas décidables} +algorithmiquement : +\begin{itemize} +\item savoir si une machine de Turing donnée s'arrête, +\item savoir si un terme du $\lambda$-calcul est normalisable. +\end{itemize} + +\end{frame} +% % Add somewhere: % - "Turing tarpit" % |