David Madore's WebLog: Comment calculer un grand nombre

Index of all entries / Index de toutes les entréesXML (RSS 1.0) • Recent comments / Commentaires récents

Entry #2208 [older|newer] / Entrée #2208 [précédente|suivante]:

(dimanche)

Comment calculer un grand nombre

J'ai déjà exploré assez en détail le sujet des (très très) grands nombres. Je ne vais pas revenir sur tout ce que j'ai dit (et comme d'habitude, je tenterai de ne garder mes posts indépendants les uns des autres), mais je veux me servir de cette question pour illustrer quelques faits de logique rigolo.

Imaginons qu'un génie pervers nous mette devant un ordinateur et nous donne la tâche d'écrire — dans un langage de programmation idéalisé de notre choix — un programme qui calcule le nombre le plus grand possible avant de s'arrêter. (Le programme en question tournera sur l'Infinitiplex du génie, équivalent à une machine de Turing qui dispose de ressources de calcul illimitées : donc ni le temps de calcul ni la mémoire consommée ne sont à prendre en compte, seul importe le nombre renvoyé ; en revanche, évidemment, la taille du programme doit rester humainement gérable ; par ailleurs, le programme doit effectuer un calcul déterministe et s'arrêter de lui-même, sans intervention extérieure.)

La stratégie intelligente à utiliser serait quelque chose comme ceci :

Soit T une théorie logique raisonnablement puissante et contenant l'arithmétique ; par exemple : ZFC. [On verra plus bas qu'on devra supposer la Σ₁-véracité-arithmétique de T.]

Appelons F:NF(N) (ou plus exactement FT) la fonction ainsi calculée :

  • énumérer toutes les suites de symboles de longueur ≤N,
  • parmi celles-ci, rechercher toutes celles qui sont des démonstrations valides dans la théorie T (c'est-à-dire que chaque ligne est soit un axiome de T soit le résultat de lignes antérieures par application des règles de la logique, ce qui se teste algorithmiquement sans aucun problème),
  • parmi celles-ci, rechercher toutes celles dont la conclusion est de la forme l'exécution de la machine de Turing <M> termine (quand démarre à partir d'un ruban vierge) [on peut, bien sûr, remplacer les machines de Turing par toute autre langage de programmation idéalisé bien défini donc susceptible d'être formalisé dans l'arithmétique],
  • lancer (c'est-à-dire, simuler) l'exécution de toutes ces machines de Turing M, et attendre qu'elles s'arrêtent, en comptant le nombre de pas d'exécution,
  • renvoyer la somme de tous ces temps d'exécution.

Le programme effectue le calcul de F(101000) (disons).

D'ailleurs, je ne suis pas le seul à proposer cette idée : un concours de ce genre a été fait (écrire le programme en C idéalisé qui calcule le nombre le plus grand possible en 512 octets de code source), et le gagnant est celui qui a utilisé cette stratégie avec, pour T le calcul des constructions de Coquand-Huet, une logique d'ordre supérieur qui a l'avantage d'unifier le programme et sa preuve de terminaison. Je suis d'ailleurs très impressionné que quelqu'un ait réussi à implémenter la normalisation du calcul des constructions en 512 octets de C.

Dès que la théorie T est raisonnablement puissante, ceci calcule un nombre extraordinairement grand. Pour tout T non ridiculement faible, la valeur FT(10↑1000) va dépasser, par exemple, le nombre de Graham (et de très loin) : en effet, il est très facile de montrer que le programme évident qui calcule ce nombre, et le convertit en unaire, termine — ceci demande certainement moins de 10↑1000 symboles à démontrer, et ce, dans une théorie T passablement faible. Donc, au cours du calcul de F(10↑1000), on va énumérer cette démonstration, puis exécuter le programme correspondant, et du coup, F(10↑1000) dépasse largement le nombre de Graham. Ce même argument vaut — par définition même de la fonction F — pour toute valeur qui peut être calculée par un programme dont la terminaison peut être prouvée par une démonstration de longueur raisonnable (dans le système T choisi).

Plus le système T est puissant, plus il montrera la terminaison de machines de Turing compliquées, et plus le nombre FT(10↑1000) calculé sera grand. Par exemple, si T est l'arithmétique de Peano du premier ordre, comme expliqué ci-dessus, on peut facilement formaliser le fait que la machine qui calcule la fonction d'Ackermann termine (i.e., Peano sait que cette fonction est bien définie), donc F(10↑1000) va dépasser les quantités facilement construites à partir de la fonction d'Ackermann (ou ses variantes, ce qui inclut le nombre de Graham qui est essentiellement 64 itérations de la fonction d'Ackermann). Pour un système T capable de prouver la terminaison des suites de Goodstein (cette fois, Peano ne suffit plus, mais ZFC si), alors le nombre va dépasser tout ce qu'on peut raisonnablement décrire avec des opérations comme la longueur de la suite de Goodstein commençant par <tant> (cette fonction croissant considérablement plus vite que la fonction d'Ackermann).

En fait, comme je vais l'expliquer, si le but est de fabriquer le nombre le plus grand possible, il vaut mieux viser le système T le plus fort possible, plutôt qu'essayer d'améliorer d'autres aspects du programme (par exemple remplacer 10↑1000 par 10↑(10↑1000) ou quelque chose comme ça, ou même imbriquer 10↑1000 fois la fonction F).

Voici une première observation assez triviale : le système T lui-même ne peut pas prouver en moins de N symboles que F(N) est bien définie (i.e., que le programme qui le calcule termine) : en effet, si c'était le cas, le calcul de F(N) lui-même ferait partie des machines M dont il énumère une preuve de terminaison, et du coup F(N) se simulerait lui-même, or dans ce cas il ne termine certainement pas. Ou, si on préfère : comme F(N) est plus grand que le résultat de tout calcul M dont T prouve la terminaison en moins de N symbole, T ne peut évidemment pas prouver la terminaison de ce calcul-là.

Ceci peut ressembler à un paradoxe. La terminaison de F(N) n'est-elle pas évidente pour n'importe quel N ? Après tout, l'énumération des chaînes de longueur au plus N termine évidemment, et pour ce qui est de la seconde partie du calcul, on a une preuve (dans T) de la terminaison de chacune des machines M qui sont lancées, donc il faut bien qu'elles terminent. C'est, en effet, le cas, si on a fait l'hypothèse suivante sur la théorie T : que dès que celle-ci prouve la terminaison d'une machine de Turing M, alors cette machine termine effectivement ; cette hypothèse (T ne dit pas de bêtises, au moins s'agissant de la terminaison des machines de Turing), i.e., le fait que certaines conclusions de T soient vraies, s'appelle la Σ₁-véracité-arithmétique de la théorie T (on dit parfois : 1-consistance de T ; la définition n'est pas tout à fait la même, mais au final cela revient au même). Si on veut, il s'agit d'une affirmation plus forte que la consistance de T : la consistance de T demande que T ne démontre pas l'énoncé absurde 0=1, la Σ₁-véracité-arithmétique demande que tout ce que T démontre et qui peut se mettre sous la forme <telle> machine de Turing termine (à partir d'un ruban vierge) est vrai, ce qui est visiblement plus fort (si T démontre 0=1, elle démontre n'importe quoi, y compris que termine une machine de Turing qui fait une boucle infinie triviale). (La Σ₁-véracité-arithmétique de T est même assez trivialement équivalente à l'énoncé pour tout N, la valeur FT(N) est définie [i.e., le calcul termine].)

Digression : Un exemple de théorie consistante mais non Σ₁-arithmétiquement-vraie (=1-consistante) est la théorie PA♠ définie comme PA + ¬Consis(PA), i.e., l'arithmétique de Peano (PA) à laquelle on ajoute l'axiome l'arithmétique de Peano est inconsistante. D'après le théorème d'incomplétude de Gödel, cette théorie PAest consistante (puisque si PA+¬Consis(PA) démontrait 0=1, alors par pure application des règles de logique, PA démontrerait Consis(PA)), même si cela peut sembler étrange vu qu'elle prétend elle-même être inconsistante ! Et comme elle (PA♠) prétend que PA démontre 0=1, elle prétend que la machine de Turing qui énumère toutes les chaînes de caractère à la recherche d'une preuve de 0=1 dans PA termine — or cette machine, en vrai, ne termine pas, donc PA♠ n'est pas Σ₁-arithmétiquement-vraie.

Du coup, le fait que T (supposée consistante) ne puisse pas prouver que pour tout N le calcul de F(N) termine ne doit pas être une surprise : c'est un avatar du théorème de Gödel, selon lequel T ne peut même pas prouver que T ne prouve pas 0=1, donc a fortiori pas que ce qu'elle démontre est vrai, même pas pour quelque chose d'aussi trivial que 0=1 ou encore moins <telle> machine de Turing termine.

En revanche, si T♯ est une théorie contenant T et qui prouve (ou qui postule) que T est Σ₁-arithmétiquement-vraie (il n'y a pas de difficulté à formaliser cette notion), alors la fonction F♯:=FT associée à T♯ est considérablement plus grande que la fonction F:=FT associée à T : en effet, d'après l'hypothèse faite, on peut écrire dans T♯ toute démonstration qu'on pouvait déjà écrire dans T, mais aussi utiliser le principe si T montre qu'une machine de Turing s'arrête, alors elle s'arrête vraiment, et donc conclure (en un nombre raisonnable de symboles) que F est bien définie. Donc (pour peu que la preuve de la Σ₁-véracité-arithmétique de T dans T♯ ne soit pas d'une longueur délirante) F♯(10↑1000) va sans difficulté dépasser F(F(F(⋯(F(10↑1000))))) avec F(10↑1000) imbrications de la fonction F (puisque dès qu'on sait que la fonction F est bien définie, on n'a aucun mal à écrire des programmes qui terminent en l'utilisant de cette manière).

Le raisonnement du paragraphe précédent vaut, notamment, si T est PA (l'arithmétique de Peano du premier ordre) est T♯ est ZFC : en effet, ZFC montre sans difficulté que toute conséquence arithmétique de PA est vraie, et en particulier toute conséquence du type <telle> machine de Turing termine. Donc la fonction F associée à ZFC croît considérablement plus vite que celle associée à PA (euphémisme !). De façon peut-être plus surprenante, le raisonnement vaut aussi si T est ZFC et que T♯ s'obtient en rajoutant l'hypothèse (IC) de l'existence d'un cardinal inaccessible : en effet, ZFC+IC démontre l'existence de ce qu'on appelle un « modèle transitif » de ZFC, i.e., un ensemble qui se comporte comme un petit monde dans lequel tous les axiomes de ZFC sont vrais (pour la même relation d'appartenance), ce modèle ayant les mêmes entiers naturels que les vrais, donc ZFC+IC démontre que toute conséquence arithmétique de ZFC est vraie, et en particulier que toute machine de Turing dont ZFC démontre la terminaison termine effectivement. Ainsi, FZFC+IC croît beaucoup plus vite que FZFC. Et la même chose vaut essentiellement pour toute notion de grand cardinal par rapport à une moins forte : plus on ajoute des grands cardinaux en pertant de T=ZFC, plus on obtient des fonctions qui croissent vite (et donc, in fine, des valeurs plus grandes de F(10↑1000) : il y a quelque chose de satisfaisant à ce que les grands cardinaux aident à fabriquer des grands entiers naturels).

Bref, ZFC+IC prouve, de façon raisonnablement courte, que FZFC(N) est défini pour tout N, et notamment que FZFC(10↑1000) l'est. Comme je l'ai expliqué, par ailleurs, il est évident que ZFC seul ne peut pas prouver en moins de 10↑1000 symboles que FZFC(10↑1000) est défini. En fait ZFC prouve bien que FZFC(10↑1000) est défini, et la démonstration est certes longue, mais pas beaucoup plus longue que 10↑1000 symboles (disons à la louche que 10↑10000 devraient suffire : en tout cas, nettement moins que les nombres totalement colossaux produits par nos diverses fonctions F). Pourquoi ? Cela résulte de l'observation triviale suivante : une démonstration de longueur inférieure à N (disons 10↑1000) dans ZFC ne peut pas utiliser d'axiome de ZFC de longueur supérieure à ce nombre (rappelons que ZFC a un nombre infini d'axiomes, à cause du schéma de compréhension et surtout celui de remplacement) ; or un lemme de réflexion montre, dans ZFC, que tout sous-ensemble fini explicite donné des axiomes de ZFC a un « modèle transitif », et donc (ce qui nous intéresse ici) a des conséquences arithmétiques vraies. (On peut même, pour tout k explicite donné, que ZFC dont le schéma de remplacement a été limité aux prédicats ayant au plus k alternations de quantificateurs — voir aussi ici — a un modèle transitif ; et la démonstration se fait suivant un modèle simple en fonction de k.) Quand on analyse, cette démonstration écrite complètement dans ZFC, on voit qu'elle fait une longueur polynomiale en N (avec un degré sans doute assez petit et des coefficients raisonnables — je n'ai pas fait l'analyse complète). Notamment, ZFC prouve que FZFC(10↑1000) est bien défini en une longueur certes plus longue que 10↑1000 symboles, mais certainement moins longue que 10↑10000.

Pour récapituler, on est dans la situation un peu étonnante suivante :

Ceci illustre plusieurs phénomènes. D'une part, l'accélération des démonstrations : la longueur de la plus courte preuve dans ZFC de FZFC(10↑1000) existe est, disons, quelque part entre 10↑1000 et 10↑10000 symboles, alors que dans ZFC+IC, elle est nettement plus courte que 10↑1000 symboles. (Notons que l'énoncé FZFC(10↑1000) existe est même prouvable dans PA ou dans des systèmes extrêmement faibles de l'arithmétique : après tout, pour prouver qu'une machine de Turing termine, il suffit d'écrire sa trace d'exécution complète comme démonstration ! Mais ceci donne une démonstration de longueur vraiment colossale, puisque comparable au nombre dont elle affirme l'existence.)

Ensuite, c'est un cas très explicite d'incomplétude : pour chaque N on peut produire, selon un motif simple, une démonstration dans ZFC de FZFC(N) existe, mais on ne peut pas en produire une de pour tout N, FZFC(N) existe. Du coup, je trouve que ceci illustre la mauvaise foi de la position épistémologique je ne crois qu'à ce qui est démontré dans ZFC : personne ne va écrire séparément la démonstration de FZFC(N) existe pour un N donné (ça n'a aucun intérêt : elle se produit trivialement en fonction de N), mais cette position oblige à dire qu'on l'accepte que comme démonstration du fait que FZFC(N) existe pour n'importe quel N, mais pas du même énoncé quantifié par pour tout N ! Ceci vaut notamment pour les gens qui se cachent derrière leur petit doigt en disant je ne sais pas si ZFC est consistant (de fait, ZFC ne le démontre pas) : je rappelle que l'énoncé pour tout N, FZFC(N) existe implique notamment la consistance de ZFC (il est équivalent à sa Σ₁-véracité-arithmétique), or je viens d'expliquer qu'il faut être pas mal de mauvaise foi pour prétendre ne pas savoir que pour tout N, FZFC(N) existe alors qu'on sait pour tout N que FZFC(N) existe !

D'un autre côté, si on cherche à calculer le nombre le plus grand possible (pour répondre au défi du génie pervers), on est devant le problème insoluble suivant : quelle est la théorie la plus forte possible dont on soit « convaincu » qu'elle soit Σ₁-arithmétiquement-vraie ? Après tout, ZFC n'est le cadre « orthodoxe » des mathématiques que par une sorte d'accident historique (le schéma de remplacement est déjà une sorte d'axiome de grand cardinal appliqué à la classe des ordinaux et revient plus ou moins à dire que celle-ci est un cardinal inaccessible), il n'est pas magiquement plus convaincant que ZFC+IC sous prétexte qu'on a plus travaillé dedans (ou même, fait semblant de travailler dedans). Les axiomes de grands cardinaux les plus forts connus au-dessus de ZFC et au sujet desquels on ne semble pas arriver à montrer d'inconsistance sont les axiomes de rank-into-rank (et spécifiquement l'axiome I0 de Woodin) ; il y en a peut-être d'encore plus forts si on supprime l'axiome du choix [les choses sont confuses quant à la force arithmétique de ces axiomes : cf. ici].

Je souligne que plus fort ici fait référence à la force arithmétique de ces théories, et même à la force arithmétique Σ₁, c'est-à-dire à la capacité à montrer que des machines de Turing s'arrêtent : on ne demande pas de croire que ces grands cardinaux « existent » en un sens platonique profond, juste de croire qu'ajouter à la théorie des ensembles le postulat de leur existence produit des conséquences exactes sur l'arrêt des machines de Turing ! (On pourrait même utiliser le théorème de Matiâsevič-Robinson-Davis-Putnam pour reformuler ces conséquences sous la forme d'existence de solutions d'équations diophantiennes.)

Il se trouve que les systèmes connus qui sont arithmétiquement les plus forts (i.e., qui au moins paraissent arithmétiquement vrais et qui produisent les conséquences les plus fortes, donc la fonction FT la plus grande) sont tous des théories des ensembles de type ZF(C) obtenues en ajoutant des axiomes de grands cardinaux. Il n'y a pas de raison évidente à ça : il pourrait très bien s'agir d'autres types de théories des ensembles (je pense aux théories des ensembles de type NF(U) ; d'ailleurs, certaines variantes se mesurent très bien contre ZF) ou encore de systèmes de typage (par exemple, le calcul des constructions inductives (CCI) se compare bien à ZFC [correction : les choses sont plus obscures que ça, cf. l'entrée suivante] et l'ajout d'univers de types à CCI à l'ajout de cardinaux inaccessibles à ZFC, donc on pourrait imaginer des extensions du calcul des constructions qui soient au niveau de force arithmétique de ZFC + tel ou tel grand cardinal ; mais je ne crois pas qu'on en ait défini), ou une tout autre chose. Je ne sais pas s'il faut y voir le signe qu'il est plus naturel de faire des théories fortes à partir de ZF(C) ou simplement que ZF a été plus étudié.

Addendum () : Je peux aussi faire la remarque rigolote suivante : dans le même ordre d'idées que ce que je décris ci-dessus, on pourrait écrire un programme de compression [sans perte] qui est en un certain sens optimal modulo la force d'une théorie logique T. Ce programme effectue le calcul suivant : donnée une donnée Y à comprimer, on énumère, dans l'ordre de longueur, toutes les démonstrations dans T (par exemple : ZFC) dont la conclusion est de la forme la machine de Turing M, quand on lui fournit l'entrée X, termine (noter que cette démonstration doit faire au moins la longueur de M plus celle de X, juste pour énoncer la conclusion) ; à chaque fois qu'on en trouve une, on simule l'exécution de la machine M sur l'entrée X, et dès qu'on en trouve une dont la sortie coïncide avec le Y à comprimer, on s'arrête, la compression étant alors donnée par le couple (M,X) (on pourrait d'ailleurs se passer de X complètement et produire seulement M, mais l'intérêt de mettre les deux est qu'on n'a pas à s'embêter à chercher comment encoder optimalement les machines de Turing). Bref, la compression de Y est le couple (M,X) pour lequel on a la plus courte démonstration dans T du fait que M termine sur X et pour lequel par ailleurs le résultat de ce calcul vaut Y (attention !, ce dernier fait est vérifié par le programme de compression mais n'est pas inscrit dans la démonstration faite dans T !). Ce programme de compression termine si la théorie T est Σ₁-arithmétiquement-vraie, car toutes les exécutions simulées de couples (M,X) termineront, et on finira bien par en trouver une qui produit la sortie Y voulue (au pire, et c'est ce qui se passera presque toujours si Y est « aléatoire », on tombera sur la démonstration du fait que la machine qui termine immédiatement sans rien faire — donc qui calcule la fonction identité — termine quand on la lance sur l'entrée Y elle-même). On peut décomprimer (retrouver Y) en simulant l'exécution de la machine M sur l'entrée X. Mon programme de compression sera, à une constante près, au moins aussi bon que, disons, gzip, parce qu'on peut facilement prouver dans ZFC que gunzip termine sur toute entrée, donc la démonstration du fait que gunzip termine sur l'entrée X (où X est la sortie de gzip(Y)) a une longueur comparable à celle de X plus une petite constante indépendante de X, et du coup borne la taille de la sortie de mon programme. On pourrait dire que mon programme calcule non pas la complexité de Kolmogorov de Y, mais son approximation vue par la théorie T.

↑Entry #2208 [older|newer] / ↑Entrée #2208 [précédente|suivante]

Recent entries / Entrées récentesIndex of all entries / Index de toutes les entrées