- Théorème de récursion de Kleene
-
En théorie de la calculabilité plusieurs théorèmes dus à à Kleene sont appelés théorèmes de la récursion. Ils établissent l'existence de points fixes pour des opérations sur les programmes, au sens où le programme et le programme image calculent la même fonction partielle et ils sont nommés également théorèmes du point fixe de Kleene. Ils ont de nombreuses applications.
Sommaire
Formulation avec les énumérations de fonctions récursives
Si φ est une enumération acceptable des fonctions recursives et f une fonction partielle récursive alors il existe un indice tel que
.
- Pour un langage de programmation
Si φ est un langage de programmation acceptable et f une fonction semi-calculable alors il existe un programme tel que pour tout x
.
Autre formes
Ce théorème peut être décliné sous différentes formes dont l'une des plus célèbre est dues à H. Rogers. On considère un langage de programmation acceptable φ.
- Forme de Rogers
Si f est une fonction calculable alors il existe un programme tel que pour tout x .
- Paramétrisée
Il existe une fonction calculable n telle que pour tout x et y. .
- Récursion double
Si f et g sont des fonctions calculables alors il existe deux programmes et tels que pour tout x
.
On doit le théorème de récursion double à R.Smullyan.
Remarque
La démonstration de ce théorème utilise l'auto-référence s(x,x) produite par le théorème d'itération (théorème s-m-n). Cette notion d'autoréférence est très profonde et a été largement traitée par John von Neumann dans le cadre des automates cellulaires auto-reproducteurs.
Applications
Ce théorème est reconnu comme le meilleur outil permettant de produire contre-exemples et cas pathologiques. En particulier, il fournit l'existence de programmes calculant leurs propres codes. En prenant f la première projection, f(y,x) = y et en appliquant le théorème on obtient un programme tel que pour tout x
.
L'exécution du programme produit son propre code. De tels programmes sont communément appelés quines.
Bibliographie
- René Cori et Daniel Lascar, Logique mathématique II. Fonctions récursives, théorème de Gödel, théorie des ensembles, théorie des modèles [détail des éditions] chapitre 5.
Catégories :- Calculabilité
- Théorème d'informatique
- Stephen Cole Kleene
Wikimedia Foundation. 2010.