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_mn[1] dans sa forme paramétrisée.

Énoncé

Pour une énumération de fonction récursive

Si $\varphi ~$ est une énumé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 vu 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.

Références

René Cori et Daniel Lascar, Logique mathématiques II, p. 47

Portail de l'informatique théorique

Cet article est issu de Wikipedia. Le texte est sous licence Creative Commons - Attribution - Partage dans les Mêmes. Des conditions supplémentaires peuvent s'appliquer aux fichiers multimédias.

[1] René Cori et Daniel Lascar, Logique mathématiques II, p. 47