Théorème d'itération

Le théorème d'itération est dû à Stephen Kleene, il est aussi connu sous le nom de théorème s-m-n dans sa forme paramétrisée.

Énoncé

Pour une énumération de fonction récursive

Si $\varphi~$ est une enumération acceptable, alors il existe une fonction partielle récursive $s~$ telle que pour tout indice $\mathbf{e}~$ et tous nombres $x~$ et $y~$

$\varphi_{s(\mathbf{e},x)}(y)=\varphi_{\mathbf{e}}(x,y)$.

Pour un langage de programmation

Si $\varphi$ est un langage de programmation acceptable alors il existe une fonction calculable $s~$ telle que pour tout programme $\mathbf{e}$ et tous $x~$ et $y~$

$\varphi_{s(\mathbf{e},x)}(y)=\varphi_{\mathbf{e}}(x,y)$.

$s$ est appelée fonction d'itération ou fonction s-m-n dans sa forme paramétrisée.

Évaluation partielle

La fonction d'itération est un des points fondamentaux de l'évaluation partielle. En effet, dans $\varphi_{s(\mathbf{e},x)}(y)=\varphi_{\mathbf{e}}(x,y)$, le programme $s(\mathbf{e},x)$ peut être vue comme la spécialisation du programme $\mathbf{e}$ pour l'entrée $x~$, en d'autres termes, le programme $\mathbf{e}$ dont la première entrée a été fixée pour la valeur $x~$. Pour cette notion, on pourra se réferrer aux travaux de N. Jones.

Auto-référence

Par $s(x,x)~$, ce théorème permet de construire des programmes faisant référence à leurs propres codes puisque $\varphi_{s(x,x)}(y)=\varphi_{x}(x,y)$. En particulier, $s(x,x)~$ est fondamental dans la construction d'une machine de Turing dont l'arrêt est indécidable ou dans la preuve du théorème de récursion de Kleene.