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 est une énumération acceptable, alors il existe une fonction partielle récursive telle que pour tout indice et tous nombres et

.

Pour un langage de programmation[modifier | modifier le code]

Si est un langage de programmation acceptable alors il existe une fonction calculable telle que pour tout programme et tous et

.

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 , le programme peut être vu comme la spécialisation du programme pour l'entrée , en d'autres termes, le programme dont la première entrée a été fixée pour la valeur . Pour cette notion, on pourra se réferrer aux travaux de N. Jones.

Auto-référence[modifier | modifier le code]

Par , ce théorème permet de construire des programmes faisant référence à leurs propres codes puisque . En particulier, 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.