Syntaxe et arité des fonctions récursives primitives

sasaki93
Modifié (November 2021) dans Fondements et Logique
Bonjour à toutes et tous
Je cherche à définir une syntaxe pour les fonctions récursives primitives. Mes objectifs étant
(1) De démontrer "proprement" que l'ensemble des fonctions récursives primitives est dénombrable.
(2) De construire  "proprement" une fonction d'arité 2, d’évaluation des fonctions récursives primitives d'arité 1 et de montrer que cette fonction Eval n'est pas récursive primitive.
(3) De démontrer "proprement" en utilisant uniquement les fonctions récursives (autrement dit, sans passer par un autre modèle de calcul comme les machines de Turing par exemple) le théorème de Kleene sur l'existence de fonctions universelles.
Mon problème étant que j'ai du mal à définir cette syntaxe à cause de l'arité des fonctions. Voici ce que j'ai fait.

Définition. [Langage des fonctions récursives primitives et arité]
Le langage des fonctions récursives primitives est l'ensemble $\mathcal{L}_{PR}$ constitué des symboles :
$( $ ; $)$ ; $, $ ; $\mathbb{0}$ ; $s$ ; pour tout entier naturel non nul $k$ et pour tout entier naturel $i$ non nul plus petit ou égal à $k$ , $p_k^i$ ; $Comp$ ; $Rec$ .
On dit que les symboles $\mathbb{0}$ et $s$ sont des symboles d'arité $1$ et que pour tout entier naturel non nul $k$ et pour tout entier naturel $i$ non nul plus petit ou égal à $k$, le symbole $p_k^i$ est un symbole d'arité $k$.
Moralement.
$\mathbb{0}$ est le symbole de la fonction constante égale à $0$ de $\mathbb{N}$ dans $\mathbb{N}$.
$s$ est le symbole de la fonction successeur de $\mathbb{N}$ dans $\mathbb{N}$.
Pour tout entier naturel non nul $k$ et pour tout entier naturel $i$ non nul plus petit ou égal à $k$, $p_k^i$ est le symbole de la projection de la $i$-ième coordonnées de $\mathbb{N}^k$ dans $\mathbb{N}$.

Définition [Expression des fonctions récursives primitives]
L'ensemble des expressions des fonctions récursives primitives est le plus petit sous-ensemble $\mathcal{L}$ de l'ensemble des mots sur l'alphabet $\mathcal{L}_{PR}$ tel que :
(a) $\mathcal{L}$ contient $\mathbb{0}$ ; $s$ ; pour tout entier naturel non nul $k$ et pour tout entier naturel $i$ non nul plus petit ou égal à $k$ , $p_k^i$ .
(b) $\mathcal{L}$  est stable par composition, c'est-à-dire que pour tout entier $n \geq1$ et pour tout entier $k \geq 1$ si $f_1 , f_2 , \ldots f_n , g \in \mathcal{L}$ et que $f_1 , f_2 , \ldots , f_n$ sont d'arités $k$ et $g$ d'arité $n$ alors $Comp(g , f_1 , f_2 , \ldots , f_n) \in \mathcal{L}$ et est d'arité $k$.
(c) $\mathcal{L}$  est stable par schéma de récurrence, c'est-à-dire que pour tout entier $k \geq 1$ si $g,h \in \mathcal{L}$ et si $g$ est d'arité $k$ et $h$ d'arité $k + 2$ alors $Rec(g,h) \in \mathcal{L}$ et est d'arité $k + 1$.
Moralement.
$Comp(g , f_1 , f_2 , \ldots , f_n)$ est le symbole de la fonction $f$ de $\mathbb{N}^k$ dans $\mathbb{N}$ définie pour tout $\bar x \in \mathbb{N}^k$ par $f (\bar x) = g(f_1(\bar x), f_2(\bar x), \ldots , f_n(\bar x))$.
$Rec(g,h)$ est le symbole de la fonction $f$ de $\mathbb{N}^{k+1}$ dans $\mathbb{N}$ définie pour tout $x_1, x_2, \ldots, x_k, y \in \mathbb{N}$ par $f(x_1 , x_2, \ldots, x_k , 0) = g(x_1 , x_2 , \ldots , x_k)$ et $f(x_1 , x_2 , \ldots , x_k , y + 1) = h(x_1 , x_2 , \ldots , x_k , y , f(x_1 , x_2 , \ldots , x_k , y))$.

Le souci c'est qu'à cause de l'arité cette définition me semble bancale. L'idéal serait de définir inductivement et en amont l'arité d'une expression. Problème : pour pouvoir définir proprement et inductivement une fonction Arité de l'ensemble des expressions dans $\mathbb{N}$ j'ai besoin d'un théorème de lecture unique des expressions. J'ai donc besoin d'abord de définir ce qu'est une expression... mais il faut pouvoir parler d'arité pour pouvoir définir les expressions. Le serpent se mord la queue ! D'ailleurs, les rares ressources sur le sujet que j'ai trouvées, tombent dans ce problème de définition inductive selon moi en écrivant des choses comme "si $g$ est une expression récursive primitive  d'arité $k$ et $h$ une expression récursive primitive d'arité $k+2$ alors $Rec(g,h)$ est une expression récursive primitive d'arité $k+1$."
Qu'en pensez-vous ? Merci d'avance pour vos réponses.
Connectez-vous ou Inscrivez-vous pour répondre.