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é
Pour une énumération de fonction récursive
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
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
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éférer aux travaux de N. Jones.
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.
Exemple
Le programme Python suivant implémente la fonction s11 pour une fonction quelconque f et une variable x :
def S11(f,x): return lambda y: f(x,y)
Appliqué à la fonction d'addition entre deux nombres :
def addition(x,y): return x+y def g(x): return S11(addition,x) print(g(4)(3)) # affiche le résultat de addition(4,3) = 4+3 = 7
Dans l'exemple précédent, g s'écrit autrement .
Références
- ↑ René Cori et Daniel Lascar, Logique mathématiques II, p. 47
Portail de l'informatique théorique