Théorème d'itération

Un article de Wikipédia, l'encyclopédie libre.

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

Sommaire

1 Énoncé
- 1.1 Pour une énumération de fonction récursive
- 1.2 Pour un langage de programmation
2 Évaluation partielle
3 Auto-référence

[modifier] Énoncé

[modifier] 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)$ .

[modifier] 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.

[modifier] É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.

[modifier] 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.