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 |
[modifier] Énoncé
[modifier] Pour une énumération de fonction récursive
Si est une enumération acceptable, alors il existe une fonction partielle récursive telle que pour tout indice et tous nombres et
.
[modifier] Pour un langage de programmation
Si est un langage de programmation acceptable alors il existe une fonction calculable telle que pour tout programme et tous et
.
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 , le programme peut être vue 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.
[modifier] Auto-référence
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.