A remark on arity.

1 files changed, 53 insertions, 0 deletions

diff --git a/transp-inf110-01-calc.tex b/transp-inf110-01-calc.tex
index 050ee4f..15f5e79 100644
--- a/transp-inf110-01-calc.tex
+++ b/transp-inf110-01-calc.tex
@@ -1403,6 +1403,59 @@ programmes manipulés sont des fonctions générales récursives).
 \end{frame}
 %
 \begin{frame}
+\frametitle{Arité et encodage des tuples}
+
+{\footnotesize\textcolor{gray}{Remarque qui aurait dû être faite
+    avant ?}\par}
+
+\bigskip
+
+Pour tout $k \geq q$, les fonctions
+\[
+\left\{
+\begin{array}{l}
+\mathbb{N}^k \to \mathbb{N}\\
+(x_1,\ldots,x_k) \mapsto \dbllangle x_1,\ldots,x_k\dblrangle
+\end{array}
+\right.
+\quad\text{~et~}\quad
+\left\{
+\begin{array}{l}
+\mathbb{N} \to \mathbb{N}\\
+\dbllangle x_1,\ldots,x_k\dblrangle \mapsto x_i
+\end{array}
+\right.
+\]
+sont p.r.  Par conséquent,
+\[
+f\colon\mathbb{N}^k \dasharrow \mathbb{N}\text{~récursive}
+\;\Longleftrightarrow\;
+\left\{
+\begin{array}{l}
+\mathring f\colon\mathbb{N} \dasharrow \mathbb{N}\\
+\hphantom{f\colon}
+\dbllangle x_1,\ldots,x_k\dblrangle \mapsto f(x_1,\ldots,x_k)
+\end{array}
+\right.\text{~récursive}
+\]
+et de plus, un numéro $e$ de $f$ (i.e., $f = \varphi^{(k)}_e$) se
+calcule de façon p.r. à partir d'un numéro $e'$ de $\mathring f$
+(i.e., $\mathring f = \varphi^{(1)}_{e'}$) et vice versa.
+
+\medskip
+
+Ceci justifie d'omettre parfois abusivement l'arité
+
+(par défaut, « $\varphi_e$ » désigne « $\varphi^{(1)}_e$ »).
+
+\bigskip
+
+{\footnotesize Même chose, \textit{mutatis mutandis} (avec $\psi$)
+  pour les fonctions p.r.\par}
+
+\end{frame}
+%
+\begin{frame}
 \frametitle{Le théorème de récursion de Kleene (version générale récursive)}
 
 Exactement comme la version p.r. :