Théorème de récursion de Kleene

Ne doit pas être confondu avec Théorème de Kleene ou Théorème du point fixe 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 transformateurs[1] de 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.

IntuitionModifier

Théorème de récursionModifier

Une version d'un théorème de récursion s'énonce comme suit :

un programme a accès à sa propre description (i.e. à son propre code source).

En guise d'application, on peut alors démontrer que savoir si un programme est minimal (au sens où il n'y a pas de programmes équivalents avec un code source plus court) n'est pas récursivement énumérable. Par l'absurde, supposons qu'il existe un programme E qui énumère les programmes minimaux (un tel programme s'appelle un énumérateur). On construit alors le programme C suivant :

C(w)
      Obtenir sa description propre description <C> (grâce au théorème de récursion)
      Lancer l'énumérateur E jusqu'à ce qu'une machine D dont la description est strictement plus longue que celle de C
      Simuler D sur w

Il y a un nombre infini de programmes minimaux. Donc E doit écrire une machine D de description plus longue que celle de C. Ainsi, C a le même comportement que D. Mais alors D n'est pas minimal. Contradiction.

Théorème de point fixeModifier

Un théorème de point fixe peut alors être présenté comme corolaire du théorème de récursion par Sipser[1] :

Si t est une fonction calculable, alors il existe une machine de Turing F tel que t(<F>) décrit une machine de Turing équivalente à F

En effet, le théorème de récursion ci-dessus permet de donner une description de F :

F(w)
      Obtenir sa description propre description <F> (grâce au théorème de récursion)
      Calculer t(<F>)
      Simuler la machine t(<F>) sur w

Par construction, F et t(<F>) sont des machines équivalentes.

Formulation avec les énumérations de fonctions récursivesModifier

Si   est une énumération acceptable des fonctions récursives et   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   une fonction semi-calculable alors il existe un programme   tel que pour tout  

 .

Autre formesModifier

Ce théorème peut être décliné sous différentes formes dont l'une des plus célèbres est due à H. Rogers. On considère un langage de programmation acceptable  .

  • Forme de Rogers

Si   est une fonction calculable alors il existe un programme   tel que pour tout  ,  .

  • Paramétrée

Il existe une fonction calculable   telle que pour tout   et  ,  .

  • Récursion double

Si   et   sont des fonctions calculables, alors il existe deux programmes   et   tels que pour tout  ,

 

 .

On doit le théorème de récursion double à Raymond Smullyan.

RemarqueModifier

La démonstration de ce théorème utilise l'auto-référence   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.

ApplicationsModifier

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   la première projection,   et en appliquant le théorème on obtient un programme   tel que pour tout  

 .

L'exécution du programme   produit son propre code. De tels programmes sont communément appelés quines.

BibliographieModifier

  • 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.

RéférencesModifier

  1. a et b (en) Michael Sipser, Introduction to the Theory of Computation, Cengage Learning, (ISBN 1285401069, lire en ligne).