Equivalence of functions representable in the lambda-calculus and recursive functions.

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"
 %