Ouvrir le menu principal

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

ÉnoncéModifier

Pour une énumération de fonction récursiveModifier

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 programmationModifier

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 partielleModifier

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érenceModifier

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.

RéférencesModifier

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