Chapitre 3 : Récursion et théorème de Rice Table des matières Chapitre 5 : Machines de Turing
Exercices

Chapitre 4 : Ensembles récursivement énumérables

  1. Définitions
  2. Rôle du temps
  3. Un ensemble non récursivement énumérable
  4. Ensembles semi-décidables
  5. Théorème d'incomplétude de Gödel
    1. Formules logiques
    2. Systèmes de preuves
    3. Codage arithmétique
    4. Annexe

1. Définitions

La fonction caractéristique χ d'un ensemble d'entiers E est la fonction définie par :

χ (x) = ì
í
î
1 si x appartient à E
0 sinon

E est dit décidable si sa fonction caractéristique est calculable, autrement dit si le prédicat "xE" est décidable. Mais il existe une autre façon de définir effectivement un ensemble d'entiers (c'est-à-dire de le définir par un algorithme) ; E est dit récursivement énumérable (souvent abrégé en re) si :

E = { f (0), f (1), f (2), … } = Val ( f )
f désigne une fonction calculable totale.

On dit que f énumère (les éléments de) E ; Val ( f ), ensemble des valeurs de f, est aussi appelé Image ( f ). L'adverbe récursivement correspond à un sens inhabituel de récursif :

Note: dans ce chapitre, contrairement au précédent, nous emploierons souvent le même symbole pour désigner la fonction d'énumération f, ou la procédure qui la calcule ; c'est sans danger, car f désigne par définition, dans ce contexte, une fonction calculable.

Proposition : tout ensemble fini est décidable.

Preuve. Les ensembles finis peuvent être numérotés, de telle sorte que le ième bit du numéro de E indique si i appartient à E ou non (voir annexe du chapitre 1). Par exemple 26 a pour représentation binaire 11010, et c'est le numéro de l'ensemble {1, 3, 4}, car les bits de rang 1, 3 et 4 sont égaux à 1 (le bit de rang 0 est, comme d'habitude, le bit le plus à droite).

Avec cette numérotation, voici la procédure pour tester si x appartient à l'ensemble fini numéro n :

int appartient (int x, int n) {
  for (i = 0; i < x; i++)
    n = n / 2;
  return n % 2;
} 

Proposition : tout ensemble décidable est récursivement énumérable.

Preuve. Si E est décidable, sa fonction caractéristique χ est calculable ; en appelant fc une procédure qui calcule χ , voici une procédure qui énumère les éléments de E :

int fc (int x) { … }
int enum (int n) {
  int x, k = -1;
  for (x = 0; ; x++) {
    if (fc (x)) k++;
    if (k == n) return x;
  }
}

Note : si E est fini, la procédure enum boucle dès que n dépasse le cardinal de E ; c'est un bug, mais ce n'est pas un problème profond.

A vrai dire, le détail de la manipulation du compteur k offre peu d'intérêt ; on peut exprimer cet algorithme plus brièvement en considérant la procédure d'énumération comme une procédure qui s'exécute indéfiniment et "affiche" les éléments de E sur (grand) écran :

pour chaque entier x
    si (x appartient à E) "afficher" x

On passe facilement d'une présentation abrégée de ce type à une procédure d'énumération f, telle que f (0) soit le premier élément "affiché", f (1) le second, etc. en ajoutant un compteur. Notons aussi que dans la présentation abrégée, le bug concernant le cas où E est un ensemble fini, disparaît : tous les éléments de E sont affichés, puis la procédure poursuit indéfiniment son travail, mais "en silence".

Si l'on veut réciproquement calculer la fonction caractéristique d'un ensemble énuméré par f, on ne voit pas bien quoi écrire d'autre que :

int f (int n) { … }
int fc (int x) {
  int n;
  for (n = 0; ; n++)
    if (f(n) == x) return 1;
}

Mais cette procédure ne calcule pas la fonction caractéristique, elle calcule la fonction dite semi-caractéristique χ' définie par :

χ' (x) = ì
í
î
1 si x appartient à E
non défini sinon

On soupçonne alors qu'il existe des ensembles récursivement énumérables et non décidables, mais pour en fabriquer il faut faire intervenir un nouveau concept, le temps.

2. Rôle du temps

On a défini au chapitre 2 la fonction fondamentale h, liée au problème de l'arrêt (halting problem) :

h (p, x) = ì
í
î
1 si p(x) est défini — autrement dit si le calcul de p(x) termine
0 sinon

et nous avons prouvé qu'elle n'est pas calculable. Surchargeons l'opérateur h, et introduisons une nouvelle fonction avec un troisième argument, le temps :

h (p, x, t) = ì
í
î
1 si le calcul de p(x) est terminé au temps t
0 sinon

Ce que signifie "calcul terminé au temps t" dépend du modèle de calcul, mais nous aurons seulement besoin de deux axiomes :

Le premier axiome exprime qu'on peut savoir si, au temps t, le calcul est ou non terminé, en interrompant par exemple le processus de calcul, comme le fait un débogueur. Le second axiome exprime que p(x) est défini si et seulement si le calcul est terminé au temps t, pour t suffisamment grand.

Notons bien cette distinction fondamentale, que les programmeurs connaissent bien en pratique :

La différence entre les deux expériences ci-dessus, se traduit abstraitement par la différence entre les deux versions de la fonction h : celle à deux arguments, sans spécification du temps t, n'est pas calculable, tandis qu'avec un troisième argument, qui spécifie le délai d'exécution, la fonction devient calculable. On peut maintenant prouver :

Théorème. H = { (p, x) | p(x) est défini } est récursivement énumérable
(et indécidable).

Preuve. La seconde partie du résultat, entre parenthèses, à savoir que H n'est pas décidable, est le résultat fondamental du chapitre 2 (indécidabilité du problème de l'arrêt). Voici un algorithme (en format abrégé) qui énumère H :

Pour chaque triplet (p, x, t)
    si h (p, x, t) "afficher" (p, x)

Le premier axiome sur le temps permet d'employer h (p, x, t), qui est calculable, dans cet algorithme ; le second axiome prouve que tous les éléments de H seront énumérés, et eux seulement, ce qui démontre le théorème.

Note 1 : chaque élément de H apparaît une infinité de fois dans l'énumération, ce qui est autorisé par la définition d'un ensemble récursivement énumérable. Il existe une méthode générale pour remplacer toute fonction d'énumération f par une fonction injective g, qui énumère le même ensemble E sans répétition : voir exercice.

Note 2 : cet algorithme est la traduction abstraite (et donc simple) d'un concept fondamental des systèmes d'exploitation, à savoir le temps partagé (timesharing chez les anglo-saxons). Dans tout système d'exploitation moderne, un ordonnanceur (scheduler) permet d'attribuer successivement le processeur à différents processus ; les détails sont compliqués : le processeur doit posséder deux modes distincts de fonctionnement (mode noyau, pour l'ordonnanceur, et mode utilisateur, pour les processus clients), il faut utiliser le mécanisme des interruptions (matérielles et logicielles), etc. Cette simulation d'exécutions simultanées équitables, permet aussi la programmation multithread.

La version abstraite du temps partagé, présentée dans l'algorithme ci-dessus, outre qu'elle est plus simple (l'algorithme tient en deux lignes), présente une autre particularité : le nombre de processus exécutés simultanément croît sans limite ; dans ce cas, les performances d'un système d'exploitation réel s'effondreraient, tandis que, par principe, la théorie de la calculabilité ne se préoccupe pas d'efficacité, qui est du domaine de la théorie de la complexité (présentée à partir du chapitre 8 dans ce cours)

Exercice : convertir cet algorithme en une procédure C qui énumère les éléments de H, en utilisant les procédures de numérotation des triplets fournies en annexe au chapitre 1. Attention : ne pas chercher à écrire la procédure qui calcule h (p, x, t) ; cette procédure existe, mais est essentiellement aussi difficile à écrire qu'un débogueur.

3. Un ensemble non récursivement énumérable

La section précédente fournit un exemple fondamental d'ensemble récursivement énumérable et indécidable. On sait d'autre part que l'ensemble des parties de N n'est pas dénombrable, or les procédures d'énumération forment un ensemble dénombrable, donc on est sûr que "la plupart" des ensembles d'entiers ne sont pas récursivement énumérables, pour la même raison que "la plupart" des fonctions NN ne sont pas calculables. Peut-on fournir un exemple fondamental d'ensemble non récursivement énumérable, comme l'est H pour les ensembles indécidables ? La réponse est positive : nous allons montrer que le complémentaire de H n'est pas récursivement énumérable, à l'aide du théorème suivant :

Théorème 3.1. Si E et son complémentaire sont tous deux récursivement énumérables, alors ils sont décidables.

Preuve. E est énuméré par une fonction calculable f, et son complémentaire par une fonction calculable g ; on peut alors améliorer la procédure de la fin de la section 1 :

int f (int n) { … }
int g (int n) { … }
int fc (int x) {
  int n;
  for (n = 0; ; n++) {
    if (f(n) == x) return 1;
    if (g(n) == x) return 0;
  }
}

Cette fois l' exécution de la procédure termine quel que soit x, car x appartient soit à E soit à son complémentaire ; elle calcule donc bien la fonction caractéristique χ de E, autrement dit E est décidable.

On énonce parfois cette preuve sous une forme abrégée, en utilisant deux "écrans" : sur l'écran de gauche s'affichent les éléments de E, sur celui de droite les éléments du complémentaire. Pour décider si un entier x appartient à E, on attend de le voir apparaître sur l'un des deux écrans : il faut être éventuellement très patient, mais on est sûr de ne pas attendre pour rien…

De ce théorème et de celui de la section 2, on déduit immédiatement le résultat annoncé :

Théorème 3.2. Le complémentaire de H, autrement dit
{ (p, x) | p(x) n'est pas défini },
n'est pas récursivement énumérable.

4. Ensembles semi-décidables

On a vu à la fin de la section 1 que la fonction semi-caractéristique d'un ensemble E récursivement énumérable, est calculable. Appelons semi-décidabilité cette propriété, qui est équivalente à la suivante :

E est semi-décidable si et seulement si :
E = domaine ( f ) = { x | f (x) est défini } ,
f est une fonction calculable.

Note : le domaine de f est aussi appelé plus explicitement son domaine de définition.

Montrons que les deux définitions sont équivalentes. Par définition de la fonction semi-caractéristique de E, E = domaine (χ'). Réciproquement, si E = domaine ( f ), avec f calculable, voici une procédure de calcul de χ' :

int f (int n) { … }
int sc (int x) {
  int y = f(x);
  return 1;
}

Cette procédure est surprenante, puisqu'elle calcule y et n'utilise pas la valeur trouvée (ne la montrez pas à Strandh…) ; cette instruction y = f(x) a pourtant un rôle essentiel : le calcul de sc (x) se termine si et seulement si le calcul de f (x) se termine, c'est-à-dire si et seulement si x appartient à E, ce qui prouve que la procédure sc calcule bien la fonction semi-caractéristique de E, χ'.

Note : exécuter une procédure f, comme ci-dessus, pour savoir si elle termine, n'est donc pas une pratique totalement proscrite, à condition de bien réaliser que si f ne termine pas, la procédure qui l'appelle ne terminera pas non plus…

On remarque la symétrie entre la propriété qui caractérise les ensembles semi-décidables (ce sont les domaines de fonctions calculables), et celle qui définit les ensembles récursivement énumérables (ce sont les images de fonctions calculables). En fait, il ne s'agit pas d'une nouvelle classe d'ensembles, seulement d'une nouvelle caractérisation des ensembles récursivement énumérables :

Théorème. Un ensemble E est semi-décidable si et seulement si :
E est récursivement énumérable.

Preuve. La première moitié de la preuve a déjà été donnée en fin de section 1, où figure la procédure qui calcule la fonction semi-caractéristique d'un ensemble récursivement énumérable. La réciproque présente une difficulté, car l'algorithme suivant, inspiré du calcul de la fonction semi-caractéristique, échoue :

for (x = 0; ; x++) {
  y = f(x);
  "afficher" x;
}

En effet, si par exemple domaine ( f ) = {0, 1, 2, 4, 5, 9, …}, cet algorithme affichera correctement 0, 1 et 2, mais n'affichera jamais 4, 5, 9, etc. puisque le calcul de f (3) boucle.

Pour contourner cette difficulté, il faut effectuer les calculs dans des threads différents, soit, sous forme abstraite :

Pour chaque couple (x, t)
    si h (f, x, t) "afficher" x

Cet algorithme énumère correctement domaine ( f ), en utilisant le temps ; c'est le même algorithme que celui qui prouve, section 2, que H est récursivement énumérable : simplement ici la procédure (celle qui calcule f ) est fixée.

5. Théorème d'incomplétude de Gödel

Ce théorème célèbre et a priori très surprenant affirme :

Théorème. Il existe, en arithmétique, des propositions qu'on ne peut ni prouver, ni réfuter.

Note : réfuter une proposition, c'est, par définition, prouver sa négation. Une proposition qu'on ne peut ni prouver, ni réfuter, est aussi dite irrésoluble.

Gödel, en se basant sur le paradoxe du menteur, a construit explicitement une proposition de ce type (ni prouvable, ni réfutable). Nous donnons en annexe quelques détails sur cette construction, qui a des conséquences subtiles et contraires à l'intuition. Dans ce chapitre, nous montrons simplement l'existence de telles propositions, à partir des notions et des théorèmes exposés dans les sections précédentes.

5.1. Formules logiques

Une théorie mathématique formalisée est constituée d'abord de propositions, appelées aussi formules logiques, ou prédicats. Nous ne définirons pas rigoureusement ces termes ici, c'est l'objet des cours de logique, et il faut faire attention aux détails (voir annexe) pour savoir exactement de quoi l'on parle (et éviter ainsi de dire des bêtises) ; nous commenterons simplement quelques exemples :

Ces deux formules comportent des variables libres, x et y pour la première, a et b pour la seconde ; par contre une variable qui suit un quantificateur est dite liée. Les variables libres permettent de construire de nouvelles formules en procédant à des substitutions : par exemple substituer la constante 2 à la variable libre a, dans la seconde formule, fournit une nouvelle formule, qui exprime que b est pair.

Distinguer les variables libres des variables liées, dans des formules complexes, n'est pas immédiat ; de même les règles sur les substitutions et les noms des variables liées doivent être établies avec soin, ce qui rend les débuts des cours de logique assez fastidieux. Par exemple on peut remplacer sans dommage t par z dans la première formule ; mais remplacer t par x fournit une formule qui exprime … que y est impair ! Dans ce dernier cas, on dit que la variable libre x a été capturée lors du renommage, ce qui est illégal.

5.2. Systèmes de preuves

Pour formaliser la notion de démonstration (on dit aussi preuve), il existe plusieurs systèmes, d'utilisation plus ou moins commode selon le contexte. Ici il nous suffira de savoir qu'un système de preuve comporte des axiomes et des règles de déduction, qui permettent de construire des chaînes (ou des arbres) de formules prouvées à partir des axiomes (qui sont les feuilles de l'arbre). Pour en savoir plus sur la forme des règles de déduction et des preuves, on pourra consulter les cours de Jean Goubault-Larrecq, professeur à l'ENS Cachan (références en annexe).

Une théorie formelle est constituée des règles de définition de ses formules (section 5.1), de ses axiomes et de ses règles de déduction. La théorie "minimale" permettant de formaliser l'arithmétique est appelée arithmétique du premier ordre, ou arithmétique de Peano (on se doute au passage qu'il existe aussi une arithmétique du second ordre). Ici nous donnons seulement les principaux axiomes de l'arithmétique de Peano (nous ne donnons pas ceux qui traduisent les propriétés de l'égalité) ; les opérateurs arithmétiques sont l'addition et la multiplication (opérateurs binaires, c'est-à-dire à deux arguments), et la fonction successeur (opérateur unaire, c'est-à-dire avec un seul argument), notée S ci-dessous ; le langage contient aussi la constante 0 (une constante est un opérateur sans argument) :

Notons aussi qu'en logique il existe une règle de déduction qui permet de passer d'une formule avec variable libre, par exemple x + 0 = x, à sa clôture universelle : x . x + 0 = x . Inversement il existe une règle qui permet de passer de la seconde formule à la première. Les axiomes de Peano sont donc souvent présentés sans quantificateurs.

Les deux premiers axiomes expriment que 0 n'est le successeur d'aucun élément, et que la fonction successeur est injective. Les axiomes suivants traduisent les définitions par récurrence de l'addition et de la multiplication. En notant 1 le successeur de 0 (bonne idée, non ?), les axiomes de l'addition montrent que x + 1 est le successeur de x, comme prévu.

Enfin il existe un schéma de récurrence, qui est une collection infinie d'axiomes, un pour chaque formule logique (prédicat) P :

[ P (0) ∧ ∀x . P (x) ⇒ P (x + 1) ] ⇒ ∀x P (x)

x désigne une variable de la formule P, P (0) — respectivement P (x + 1) — le résultat de la substitution de cette variable par le symbole 0 — respectivement par le terme x + 1. Nous n'avons pas défini rigoureusement l'opération de substitution, section 5.1, car c'est un peu délicat techniquement : il ne faut remplacer que les occurrences libres de x.

L'irruption d'un nombre infini d'axiomes n'est pas vraiment gênante, car une preuve est finie, par définition, et ne fait donc intervenir qu'un nombre fini d'axiomes, parmi l'infinité de ceux produits par le schéma ci-dessus.

Par définition d'un système de preuve, il existe un algorithme (qui dépend évidemment du système choisi) pour vérifier si une preuve formelle est correcte, c'est-à-dire si l'enchaînement de formules qui constituent cette preuve, respecte les règles de déduction. On peut donc fabriquer des démonstrateurs automatiques, susceptibles (si l'on ne se préoccupe pas d'efficacité) de produire toutes les preuves possibles (par exemple en les ordonnant selon leur longueur); d'où le théorème suivant :

Théorème 5.2. Dans toute théorie formelle, l'ensemble D des formules démontrables est récursivement énumérable.

Note 1 : preuve (respectivement prouvable) et démonstration (resp. démontrable) sont des termes équivalents, dans ce contexte. Idem pour proposition, prédicat et formule logique.

Note 2 : l'ensemble des preuves est décidable ; par contre D est seulement récursivement énumérable, car on ne connaît pas a priori la taille de la preuve d'une formule démontrable. Si la formule Φ n'apparaît pas sur l'écran où sont affichées toutes les preuves (et donc leurs conclusions, qui sont les formules démontrables), on ignore si Φ n'est pas démontrable, ou s'il faut attendre une preuve un peu plus longue…

En fait, les logiciels utilisés en pratique n'ont pas pour but de produire toutes les preuves (il y en a beaucoup trop, leur nombre est une fonction exponentielle de leur longueur), mais seulement d'assister un utilisateur, aussi efficacement que possible, pour formaliser des preuves (seule une preuve formalisée peut être vérifiée rigoureusement). Les différents systèmes de preuves correspondent à différents types de logiciels, qui utilisent des algorithmes sophistiqués pour être aussi efficaces que possible dans certains contextes. Coq est certainement, aujourd'hui, l'un des plus intéressants de ces systèmes.

5.3. Codage arithmétique

Il existe des théories formelles qui possèdent des systèmes de preuves complets, c'est-à-dire qui permettent de démontrer ou de réfuter toute proposition : c'est le cas de la logique du premier ordre, qui prouve (ou réfute) les formules indépendamment de l'interprétation des symboles de fonctions et de prédicats (on peut dire qu'il n'existe pas d'axiome pour ces symboles) ; c'est aussi le cas pour l'arithmétique de Presburger, qui est l'arithmétique de Peano privée du symbole de multiplication (et donc des axiomes qui la définissent).

Par contre l'arithmétique de Peano permet de coder la notion de programme informatique, et plus précisément de coder le calcul y = p (x), où p désigne une procédure. A chaque procédure p, on peut associer une formule arithmétique P ( x, y ) qui "exprime" que y = p (x), c'est-à-dire :

si y = p (x), la formule P ( x, y ) est démontrable ;
si yp (x), la formule ¬P ( x, y ) est démontrable.

Nous décrirons seulement ce codage sur un exemple ; pour une description plus complète (attention : il faut avoir un peu de goût pour l'arithmétique), consulter la leçon 39 de l'ouvrage de Kozen, ou la section 3.3 (Representation Theorem) du cours de Podnieks (références en annexe).

La fonction exponentielle ( calcul de a n ) peut être codée en C par :

int exp (int a, int n) {
  int y = 1;
  for (int k = 0; k < n; k++)
    y = y * a;
  return y;
}

La première idée pour coder cette procédure par une formule logique est d'écrire :

y0 = 1 ∧ y1 = y0 * ay2 = y1 * a ∧ … ∧ yn = yn-1 * ay = yn

puis d'employer un quantificateur pour avoir une formule de taille fixe :

( y0 = 1 ) ∧ ( ∀k . k < nyk+1 = yk * a ) ∧ ( y = yn )

La formule doit exprimer une relation entre a, n et y, et donc seules ces trois variables (deux pour les arguments et une pour le résultat) doivent être libres ; que faire des variables intermédiaires yk ? La solution est simple, il suffit d'ajouter une suite de quantificateurs existentiels ∃y0y1 … ∃yn en tête de la formule.

Restent deux problèmes : on n'a pas le droit d'utiliser un nombre variable de quantificateurs, et pas le droit d'ailleurs d'utiliser des indices ! Ces deux problèmes seront résolus simultanément en codant la liste :

[ y0, y1, … , yn ]

par un seul entier u, avec une fonction β telle que β ( u, k ) = yk . C'est ce que nous avons appris à faire au chapitre 1 (numérotations), sauf qu'il faut veiller, pour ne pas tourner en rond, à définir ce codage et cette fonction β par des expressions purement arithmétiques ! C'est ici qu'il faut utiliser des propriétés des nombres premiers, en particulier le théorème chinois ; nous n'en dirons pas plus, voir les références en annexe.

Ce codage s'étend à toutes les procédures, à condition de définir rigoureusement un modèle de calcul simple mais universel, comme celui des machines de Turing.

Le théorème d'incomplétude de Gödel est maintenant une conséquence simple du théorèmes 5.2 et de la section 3 de ce chapitre. En effet, dire que toute formule est démontrable ou réfutable, revient à dire que le complémentaire de l'ensemble D des formules démontrables est l'ensemble R des formules réfutables. Or D est récursivement énumérable (théorème 5.2), et R l'est tout autant : un programme qui énumère les éléments de D peut énumérer tout aussi bien leurs négations, qui sont les éléments de R. Le théorème 3.1 entraîne alors que D et R sont décidables ; autrement dit il existe un algorithme universel qui répond (sans se tromper) "démontrable" ou "réfutable" chaque fois qu'on lui présente une proposition arithmétique. Via le codage des procédures par des formules arithmétiques, cet algorithme permet de savoir si le calcul de p (x) termine, ou si x . p (x) = x , etc., ce qui contredit le théorème de Rice.

Le paragraphe précédent montre que D et R ne sont pas complémentaires ; il existe donc des propositions irrésolubles. L'arithmétique de Peano n'est pas une théorie complète, et le théorème de Gödel est démontré.

Notons que l'absence d'algorithme universel permettant de décider si une proposition arithmétique est démontrable ou réfutable, est a priori très vraisemblable : si un tel algorithme existait, cela se saurait ! Autrement dit les mathématiciens auraient découvert cet algorithme, ou du moins travailleraient à le mettre au point (c'était, paraît-il, le rêve de Hilbert, mais ce rêve semble plutôt naïf pour un aussi grand mathématicien), au lieu de gaspiller leur énergie à résoudre des problèmes particuliers par des méthodes ad hoc. En fait un tel algorithme n'existe pas, ce qui est une bonne nouvelle pour les mathématiciens : démontrer des théorèmes demandera toujours de la réflexion créative (de même qu'écrire des logiciels corrects, voir la FAQ du chapitre 3).

5.4. Annexe

Une annexe donne quelques compléments sur la théorie formelle appelée arithmétique du premier ordre, et sur le paradoxe du menteur. Cette annexe est présentée sous forme de FAQ, et se termine par quelques références.