Representation of functions by terms of the lambda-calculus.

1 files changed, 38 insertions, 2 deletions

diff --git a/transp-inf110-01-calc.tex b/transp-inf110-01-calc.tex
index 15f5e79..a7504a0 100644
--- a/transp-inf110-01-calc.tex
+++ b/transp-inf110-01-calc.tex
@@ -1901,8 +1901,8 @@ machine de Turing qui, pour tous $x_1,\ldots,x_k$ :
 (suivi d'une infinité de $0$), c'est-à-dire $\beta(0)=0$, $\beta(j)=1$
 si $1\leq j\leq x_1$, $\beta(1+x_1)=0$, $\beta(j)=1$ si $2+x_1\leq
 j\leq 1+x_1+x_2$, etc.,
-\item si $f(x_1,\ldots,f_k)\uparrow$, la machine ne s'arrête pas,
-\item si $f(x_1,\ldots,f_k){\downarrow} = y$, la machine s'arrête avec
+\item si $f(x_1,\ldots,x_k)\uparrow$, la machine ne s'arrête pas,
+\item si $f(x_1,\ldots,x_k){\downarrow} = y$, la machine s'arrête avec
   la tête à l'emplacement $0$ (le même qu'au départ), le ruban
   $\beta(j)$ non modifié pour $j<0$, et
 \item les symboles $\beta(j)$ pour $j\geq 0$ du ruban final forment
@@ -2765,6 +2765,42 @@ x.f(f^{(n)}(x)) = \lambda f.\lambda x.f^{(n+1)}(x) = \underline{n+1}
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{Calculs dans le $\lambda$-calcul : une convention}
+
+On dira qu'une fonction $f\colon \mathbb{N}^k \dasharrow \mathbb{N}$
+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}$,
+\item si $f(x_1,\ldots,x_k){\uparrow}$ alors
+  $t\underline{x_1}\cdots\underline{x_k} \rightarrow_{\mathsf{lft}}
+  \cdots$ ne termine pas,
+\end{itemize}
+où $\underline{z}$ désigne l'entier de Church associé
+à $z\in\mathbb{N}$.
+
+\bigskip
+
+Exemples :
+\begin{itemize}
+\item $\lambda mfx.f(mfx)$ représente $m \mapsto m+1$
+  (transp. précédent),
+\item $\lambda mnfx.nf(mfx)$ représente $(m,n) \mapsto m+n$,
+\item $\lambda mnf.n(mf)$ représente $(m,n) \mapsto mn$ {\footnotesize
+  (itérer $n$ fois l'itérée $m$-ième)},
+\item $\lambda mn.nm$ représente $(m,n) \mapsto m^n$ {\footnotesize
+  (itérer $n$ fois l'itération $m$-ième)}.
+\item $\lambda mnp.p(\lambda y.n)m$ représente $(m,n,p) \mapsto
+  \left\{\begin{array}{ll}m&\text{~si~}p=0\\n&\text{~si~}p\geq
+  1\end{array}\right.$\\{\footnotesize (itérer $p$ fois « remplacer
+    par $n$ »)}.
+\end{itemize}
+
+\end{frame}
+%
 % Add somewhere:
 % - "Turing tarpit"
 %