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