Representation of p.r. functions by terms of the lambda-calculus.

1 files changed, 138 insertions, 12 deletions

diff --git a/transp-inf110-01-calc.tex b/transp-inf110-01-calc.tex
index a7504a0..29dcb18 100644
--- a/transp-inf110-01-calc.tex
+++ b/transp-inf110-01-calc.tex
@@ -2734,16 +2734,16 @@ Intérêt :
 \begin{frame}
 \frametitle{Entiers de Church}
 
-On définit les termes en forme normale $\underline{n} := \lambda
+On définit les termes en forme normale $\overline{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.
+\item $\overline{0} := \lambda fx.x$
+\item $\overline{1} := \lambda fx.fx$
+\item $\overline{2} := \lambda fx.f(fx)$
+\item $\overline{3} := \lambda fx.f(f(fx))$, etc.
 \end{itemize}
 
-{\footnotesize Intuitivement, $\underline{n}$ prend une fonction
+{\footnotesize Intuitivement, $\overline{n}$ prend une fonction
   $f$ et renvoie sa $n$-ième itérée.\par}
 
 \medskip
@@ -2754,12 +2754,12 @@ f.\lambda x.f(mfx)$
 Alors
 \[
 \begin{aligned}
-A\underline{n} &= (\lambda m.\lambda f.\lambda x.f(mfx))(\lambda
+A\overline{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}
+x.f(f^{(n)}(x)) = \lambda f.\lambda x.f^{(n+1)}(x) = \overline{n+1}
 \end{aligned}
 \]
 
@@ -2773,13 +2773,13 @@ est \textbf{représentable par un $\lambda$-terme} lorsqu'il existe un
 terme clos $t$ tel que, pour tous $x_1,\ldots,x_k \in \mathbb{N}$ :
 \begin{itemize}
 \item si $f(x_1,\ldots,x_k){\downarrow}=y$ alors
-  $t\underline{x_1}\cdots\underline{x_k}
-  \twoheadrightarrow_{\mathsf{lft}} \underline{y}$,
+  $t\overline{x_1}\cdots\overline{x_k}
+  \twoheadrightarrow_{\mathsf{lft}} \overline{y}$,
 \item si $f(x_1,\ldots,x_k){\uparrow}$ alors
-  $t\underline{x_1}\cdots\underline{x_k} \rightarrow_{\mathsf{lft}}
+  $t\overline{x_1}\cdots\overline{x_k} \rightarrow_{\mathsf{lft}}
   \cdots$ ne termine pas,
 \end{itemize}
-où $\underline{z}$ désigne l'entier de Church associé
+où $\overline{z}$ désigne l'entier de Church associé
 à $z\in\mathbb{N}$.
 
 \bigskip
@@ -2801,6 +2801,132 @@ Exemples :
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{Représentation des fonctions p.r. : cas faciles}
+
+{\footnotesize (Cf. transp. \ref{primitive-recursive-definition}.)\par}
+
+Fonction p.r. facilement représentables par un $\lambda$-terme :
+\begin{itemize}
+\item $\lambda x_1\cdots x_k.x_i$ représente $(x_1,\ldots,x_k) \mapsto x_i$ ;
+\item $\lambda x_1\cdots x_k.\overline{c}$ représente
+  $(x_1,\ldots,x_k) \mapsto c$ ;
+\item $A := \lambda mfx.f(mfx)$ représente $x \mapsto x+1$ ;
+\item si $v_1,\ldots,v_\ell$ représentent $g_1,\ldots,g_\ell$ et $w$
+  représente $h$, alors $\lambda x_1\cdots x_k.w(v_1 x_1\cdots
+  x_k)\cdots (v_\ell x_1\cdots x_k)$ représente $(x_1,\ldots,x_k)
+  \mapsto h(g_1(x_1,\ldots,x_k),\ldots, g_\ell(x_1,\ldots,x_k))$ ;
+\item si $v$ représente $g$ et $w$ représente $h$, alors
+\[
+\lambda x_1\cdots x_k z.z(wx_1\cdots x_k)(vx_1\cdots x_k)
+\]
+représente $f$ définie par la récursion primitive
+\[
+\begin{aligned}
+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))
+\end{aligned}
+\]
+\alert{mais} on veut $f(x_1,\ldots,x_k,z+1) =
+h(x_1,\ldots,x_k,f(x_1,\ldots,x_k,z),\alert{z})$...?
+\end{itemize}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Représentation des couples d'entiers}
+
+{\footnotesize (Oublions $x_1,\ldots,x_k$ pour ne pas alourdir les
+  notations.)\par}
+
+Comment passer de
+\[
+\left\{
+\begin{aligned}
+f(0) &= g\\
+f(z+1) &= h(f(z))
+\end{aligned}
+\right.
+\quad\text{~à~}\quad
+\left\{
+\begin{aligned}
+f(0) &= g\\
+f(z+1) &= h(f(z),z)
+\end{aligned}
+\right.
+\quad\text{~?}
+\]
+On voudrait définir
+\[
+\tilde f(z) = (f(z),z)
+\quad\text{~soit~}\quad
+\left\{
+\begin{aligned}
+\tilde f(0) &= (g,0)\\
+\tilde f(z+1) &= \tilde h(\tilde f(z))
+\end{aligned}
+\right.
+\;\text{~où~}\;
+\tilde h(y,z) = (h(y,z), z+1)
+\]
+
+\bigskip
+
+On va définir (temporairement ?)
+\[
+\begin{aligned}
+\overline{m,n} &:= \lambda fgx.f^{(m)}(g^{(n)}(x))
+\quad\text{~si~}m,n\in\mathbb{N}\\
+\Pi &:= \lambda mnfgx.(mf)(ngx)
+\quad\text{~donc~}\Pi\overline{m}\,\overline{n} \twoheadrightarrow_{\mathsf{lft}} \overline{m,n}\\
+\pi_1 &:= \lambda pfx.pf(\lambda z.z)x
+\quad\text{~donc~}\pi_1\overline{m,n} \twoheadrightarrow_{\mathsf{lft}} \overline{m}\\
+\pi_2 &:= \lambda pgx.p(\lambda z.z)gx
+\quad\text{~donc~}\pi_2\overline{m,n} \twoheadrightarrow_{\mathsf{lft}} \overline{n}\\
+\end{aligned}
+\]
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Représentation de la récursion primitive générale}
+
+Maintenant qu'on a une représentation des couples d'entiers naturels
+dans le $\lambda$-calcul donnée par $\Pi$ (formation de paires) et
+$\pi_1,\pi_2$ (projections).
+
+\bigskip
+
+\itempoint Si $v$ représente $g\colon \mathbb{N}^k \dasharrow
+\mathbb{N}$ et $w$ représente $h\colon \mathbb{N}^{k+2} \dasharrow
+\mathbb{N}$, alors $f\colon \mathbb{N}^{k+1} \dasharrow \mathbb{N}$
+est représentée par
+\[
+\lambda x_1\cdots x_k z.
+\pi_1(z(\lambda p.\Pi(w x_1\cdots x_k (\pi_1 p)(\pi_2 p))A(\pi_2 p))(\Pi(vx_1\cdots x_k)\overline{0}))
+\]
+où
+\[
+\begin{aligned}
+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}
+\]
+
+\bigskip
+
+{\footnotesize D'autres encodages des paires sont possibles et
+  possiblement plus simples, p.ex., $\Pi := \lambda rsa.ars$ et $\pi_1
+  := \lambda p.p(\lambda rs.r)$ et $\pi_2 := \lambda p.p(\lambda
+  rs.s)$ (fonctionnent sur plus que les entiers de Church).\par}
+
+\bigskip
+
+Bref, (au moins) \alert{les fonctions p.r. sont représentables par
+  $\lambda$-termes}.
+
+\end{frame}
+%
 % Add somewhere:
 % - "Turing tarpit"
 %