Théorème d'itération

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

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é[modifier | modifier le code]

Pour une énumération de fonction récursive[modifier | modifier le code]

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[modifier | modifier le code]

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[modifier | modifier le code]

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[modifier | modifier le code]

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.