David Madore's WebLog: 2014-06

Je me demande régulièrement s'il serait possible de trouver une application des nombres p-adiques ailleurs qu'en mathématiques ; par exemple, une application des 2-adiques en informatique (ce qui semble le plus plausible, parce que les ordinateurs, manipulant des nombres binaires, manipulent en fait des entiers 2-adiques approchés). Je n'ai pour l'instant rien trouvé de bien convaincant. Voici cependant un exemple qui pourrait servir avec un peu d'imagination, et qui en tout cas fait un « tour de magie » rigolo :

Soit a un entier impair écrit en binaire, disons, sur 64 bits, dont on suppose qu'il est le carré d'un entier : on cherche à retrouver cette racine carrée (exacte). Voici une façon de s'y prendre : (1) itérer, en partant de y=1, la fonction y ↦ 2y − a·y², jusqu'à tomber sur un point fixe qu'on notera b (note : tous les calculs sont faits en binaire sur la même largeur, disons 64 bits ; comme il est habituel en informatique, on jette les bits supérieurs) ; (2) itérer, en partant de x=1, la fonction x ↦ x·(3−b·x²)/2. Autrement dit, en C :

unsigned long
exact_odd_square_root (unsigned long a) {
  unsigned long y = 1;
  for ( unsigned long yn = 0 ; y != (yn = 2*y - a*y*y) ; y = yn );
  unsigned long x = 1;
  for ( unsigned long xn = 0 ; x != (xn = x*((3-y*x*x)>>1)) ; x = xn );
  if ( x & ((((unsigned long)(-1))>>2)+1) )
    x = -x;
  return x & ((unsigned long)(-1))>>1;
}

(Les dernières lignes servent à corriger le nombre : il y a quatre valeurs de x sur vérifiant x²=a, différant par le bit de poids fort et/ou par un changement de signe global — la fonction renvoie donc celui dont les deux bits de poids fort valent 0. L'écriture ((((unsigned long)(-1))>>2)+1) sert à représenter le nombre ayant 1 juste au-dessous du poids fort sans avoir à faire d'hypothèse sur la taille des unsigned long.)

La fonction est évidemment limitée (on pourrait calculer une fonction exact_square_root() en décalant le nombre du nombre de bits adéquat — forcément pair — jusqu'à trouver un nombre impair, en appliquant la fonction exact_odd_square_root() ci-dessus, puis en refaisant le décalage vers la gauche de la moitié du nombre de bits, mais la gestion des bits de poids fort serait encore un peu plus pénible). Il y a cependant un truc rigolo, c'est qu'elle retrouve la racine carrée même si le calcul du carré a débordé (par exemple, sur 64 bits, si on fait 1000000000001*1000000000001, on trouve 2003766205206896641 et pas 1000000000002000000000001, mais la fonction ci-dessus retrouve bien 1000000000001 comme racine carrée pour cette valeur), du moins si les deux bits de poids fort valent 1 (on ne peut pas faire mieux). Par ailleurs, le nombre d'itérations est très petit (quelque chose comme 6 au pire dans chaque boucle pour un nombre de 64 bits), donc on pourrait dérouler les boucles.

L'explication 2-adique est vraiment facile : la première itération calcule l'inverse 2-adique b de a par une méthode de Newton, la seconde calcule la racine carrée par une méthode du même genre (on peut peut-être la présenter comme une méthode de Newton, en tout cas j'ai cherché un polynôme ayant un point fixe superattractif où on veut). J'imagine que je ne suis pas le premier à écrire un truc de ce genre, je n'ai pas cherché. Par contre, ce que j'aimerais bien, c'est trouver des exemples plus frappants ou plus utiles.

Alice et Bob jouent au jeu suivant : dans l'anneau k[t₁,…,t_n] des polynômes en n indéterminées sur un corps k, chacun choisit à tour de rôle un polynôme f, la règle étant qu'on n'a pas le droit de choisir un polynôme de la forme g₁·f₁ + ⋯ + g_r·f_r où f₁,…,f_r sont les polynômes qui ont déjà été joués (et notamment, le polynôme nul) ; ou, si on préfère, l'idéal (f₁,…,f_r) = {g₁·f₁ + ⋯ + g_r·f_r} doit grandir strictement à chaque étape ; lorsque le polynôme 1 (donc, n'importe quel polynôme) peut s'écrire sous la forme g₁·f₁ + ⋯ + g_r·f_r, le joueur qui vient de jouer a perdu (autrement dit, on joue à la variante « misère » du jeu : celui qui ne peut pas jouer a gagné ; l'autre variante n'est pas intéressante, parce que qu'on gagne immédiatement en jouant le polynôme 1). Question : qui a une stratégie gagnante ? (En fonction de n et, éventuellement, du corps k.)

J'avoue ne pas savoir dire grand-chose d'intelligent sur ce problème. Si n=1, dans k[x], Alice (le premier joueur) a une stratégie gagnante évidente, consistant à jouer x (l'unique indéterminée). Si n=2, dans k[x,y], il me semble que le premier joueur gagne encore en jouant y² (si Bob réplique par y, Alice gagne parce qu'on est ramené au cas n=1 ; dans tout autre cas, l'intersection entre la droite y=0 comptée avec multiplicité 2 et la courbe algébrique d'équation définie par ce que Bob aura joué sera un nombre fini de points avec des multiplicités paires, et Alice peut alors sans difficulté au coup suivant tuer tous ces points sauf un qu'elle garde avec multiplicité 1, ce qui gagne le jeu), mais je suis loin d'avoir vérifié les détails et il n'est pas du tout improbable que je me sois trompé. Ce papier montre cependant qu'Alice a bien une stratégie gagnante, soit avec des arguments du même genre en jouant y²−x³ (§6.2), soit avec un argument différent et peut-être plus rigolo en jouant y²−x³+x−1 (corollaires 6.4–6.5). J'ai vaguement tendance à croire qu'Alice gagne toujours quand on part d'un anneau de polynômes, mais je ne sais vraiment pas le prouver. (Ce qui ne veut pas dire que ce soit très dur : je n'ai pas réfléchi très fort.)

Géométriquement, le jeu consiste à partir de l'espace affine de dimension n et à intersecter avec des hypersurfaces f=0 de façon à fabriquer des « sous-schémas fermés » de plus en plus petits, celui qui aboutit sur le vide ayant perdu (dans la variante « misère »).

Le jeu sous une forme un peu plus générale s'écrit ainsi : si R est un anneau [commutatif] nœthérien (on prend R=k[t₁,…,t_n] dans l'exemple ci-dessus), chacun des deux joueurs à son tour remplace R par le quotient de celui-ci par un de ses éléments non nuls (i.e., par un idéal principal non nul), et le premier qui tombe sur l'anneau nul a perdu (dans la variante « misère »). Le jeu termine nécessairement en temps fini car on construit une suite strictement croissante d'idéaux de l'anneau nœthérien R de départ (ceux par quoi on a quotienté jusqu'à présent). Bien sûr, je ne suis pas le premier à y penser, c'est vraiment tout naturel une fois qu'on se rappelle que tout processus terminant conduit à un jeu impartial. On peut bien sûr jouer avec toutes sortes d'autres structures algébriques nœthériennes (je suppose mes anneaux commutatifs parce que je suis géomètre algébriste, mais on peut évidemment faire des choses avec les non commutatifs et des idéaux à gauche — ou bilatères). Par exemple, Alice et Bob pourraient jouer alternativement des éléments de ℤ^m définissant des sous-ℤ-modules (=sous-groupes abéliens) de celui-ci, avec une inclusion stricte à chaque fois, et cette fois-ci on peut jouer à la variante normale du jeu (i.e., celui qui ne peut plus jouer a perdu) : il n'est pas extrêmement difficile — mais pas trivial non plus — de trouver montrer que Bob (le second joueur) a une stratégie gagnante si et seulement si m est pair.

On pourrait imaginer d'autres variations : par exemple, en revenant aux polynômes dans k[t₀,…,t_n], changer un peu la règle en imposant de jouer des polynômes homogènes et sans doute en terminant quand il y a une puissance de chaque indéterminée dans l'idéal qu'on a engendré, ce qui a aussi un contenu géométrique naturel : cette fois on joue avec des sous-schémas fermés de l'espace projectif de dimension n. On pourrait aussi jouer avec des monômes, auquel cas les coefficients n'existent plus et on est simplement en train de jouer au jeu de chomp multidimensionnel. Je trouverais satisfaisant d'arriver à plonger le jeu de chomp dans le jeu d'un anneau nœthérien sans restriction, mais j'avoue ne pas voir de façon de faire ça. (Je trouverais aussi satisfaisant d'arriver à résoudre le jeu de départ sur les polynômes en le ramenant au jeu de chomp par une utilisation astucieuse de bases de Gröbner qui feraient qu'on peut toujours supposer qu'on joue avec des monômes, c'est sans doute une idée naïve.)

Toujours est-il que ce jeu conduit à un invariant rigolo (quoique pas très sérieux) d'un anneau nœthérien, c'est ce que j'ai envie d'appeler sa fonction de Grundy-Gulliksen (je vais expliquer pourquoi Gulliksen, mais pour Grundy, voir mon entrée sur les jeux combinatoires que j'ai déjà liée, spécialement sa deuxième partie). La définition est très simple et très jolie :

Si R est un anneau [commutatif] noethérien, la fonction de Grundy-Gulliksen de R est le plus petit ordinal qui n'est pas égal à la fonction de Grundy-Gulliksen d'un R/(f) pour un élément f≠0 dans R.

La définition est récursive (définir la fonction de Grundy-Gulliksen de R demande de connaître celle de tous les quotients R/(f) de R par un idéal principal non nul), mais elle a quand même un sens par nœthérianité : c'est toute la beauté de l'induction nœthérienne.

Noter qu'il s'agit là de la fonction de Grundy pour la variante normale du jeu, qui (sur tout anneau non nul) vaut 1 plus la fonction de Grundy pour la variante misère. Donc la stratégie gagnante pour au jeu (variante misère) consiste à toujours jouer vers un anneau dont la fonction de Grundy-Gulliksen vaut 1.

Bon, je ne sais essentiellement rien dire d'intelligent sur ce nombre. En revanche, si au lieu de considérer R comme un jeu je le considère comme un processus terminant dont il faut évaluer la longueur (voir la première partie de mon entrée sur les jeux), on obtient une quantité très intéressante :

Si R est un anneau [commutatif] noethérien, la longueur de Gulliksen de R est le plus petit ordinal strictement supérieur à la longueur de Gulliksen de tout R/(f) pour un élément f≠0 dans R. (De façon équivalente, c'est le plus petit ordinal strictement supérieur à la longueur de Gulliksen de tout R/I pour un idéal I≠(0) de R.)

(L'équivalence dans la parenthèse finale n'a évidemment pas d'analogue pour la fonction de Grundy-Gulliksen : cela reviendrait à donner aux joueurs la possibilité de quotienter l'anneau autant de fois qu'ils veulent, auquel cas le jeu perd évidemment tout intérêt.)

On peut évidemment généraliser ça à d'autres choses : notamment, la longueur de Gulliksen d'un module nœthérien M sur un anneau R est le plus petit ordinal strictement supérieur à la longueur de Gulliksen de tout quotient M/N de M par un sous-R-module N (et en fait, on n'a pas besoin de supposer R commutatif, et d'ailleurs Gulliksen ne le fait pas) ; la longueur de Gulliksen d'un schéma nœthérien est le plus petit ordinal strictement supérieur à la longueur de Gulliksen de n'importe quel sous-schéma fermé strict. Toutes ces définitions ont un sens bien que récursives, grâce à la magie de l'induction nœthérienne.

Par exemple, l'anneau nul, comme il n'a aucun quotient non-trivial, a une longueur nulle (0 est le plus petit ordinal strictement supérieur à tout élément de l'ensemble vide), et c'est manifestement le seul ; un corps a une longueur 1, et réciproquement tout anneau de longueur 1 est un corps. Un espace vectoriel de dimension finie sur un corps a une longueur (en tant que module sur ce corps) égale à sa dimension. L'anneau k[t]/(t²) a une longueur 2, tandis que k[t] a longueur ω (parce que k[t]/(f) a une longueur égale au degré de f pour tout f non nul).

J'appelle cette notion longueur de Gulliksen parce qu'elle a été étudiée dans un très bel article par Tor Gulliksen en 1973. Elle généralise la notion classique de longueur (définie pour les modules à la fois nœthériens et artiniens, et en particulier pour les anneaux artiniens), mais avec une définition bien plus agréable, et des propriétés presque aussi sympathiques dans le cas infini (notamment, si 0 → M′ → M → M″ → 0 est une suite exacte courte de modules nœthériens, la longueur de Gulliksen ℓ(M) de M est encadrée par la valeur de deux additions entre celles de M′ et M″, à savoir ℓ(M′) + ℓ(M″) ≤ ℓ(M) ≤ ℓ(M′) ⊞ ℓ(M″) où + désigne la somme usuelle des ordinaux, et ⊞ la somme naturelle ou somme de Hessenberg). Mais en même temps, la longueur de Gulliksen permet de retrouver la dimension (de Krull) d'un anneau, généralisée aux ordinaux non nécessairement finis : si on écrit la longueur de Gulliksen de M en forme normale de Cantor (c'est-à-dire en « base ω », voir par exemple cette entrée sur les ordinaux), alors le plus grand exposant de ω qui intervient définit la dimension de M — par exemple, la longueur de Gulliksen de k[t₁,…,t_n] vaut ωⁿ. Entre autres propriétés dignes d'intérêt (elle n'est pas écrite noir sur blanc dans l'article de Gulliksen, mais elle s'en déduit assez facilement en considérant la dimension de Krull), un anneau [commutatif] nœthérien est intègre si et seulement si sa longueur de Gulliksen est une puissance de ω, ce qui est fort sympathique. Mieux, l'écriture en forme normale de Cantor de la longueur de Gulliksen d'un anneau [commutatif] R se relie à la décomposition primaire de R.

Je trouve la longueur de Gulliksen — et son écriture en forme normale de Cantor — beaucoup plus naturelle et élégante que la fonction de Hilbert-Samuel, et que la définition classique de la dimension de Krull : à mon avis, il serait profitable de s'en servir dans toute introduction ou tout livre sur l'algèbre commutative. Le fait que le concept ait été peu développé est sans doute le signe que les algébristes n'aiment pas les ordinaux (ou l'infini qu'ils ne contrôlent pas bien), ce qui est vraiment dommage.

Une chose qui me chagrine, cependant, c'est qu'on manque d'exemples d'anneaux nœthériens de dimension de Krull arbitraire (infinie) : essentiellement, je connais une construction, due à Nagata, qui a été raffinée par le même Gulliksen pour fabriquer des anneaux de dimension de Krull un ordinal quelconque (et du coup, de façon facile, de longueur de Gulliksen un ordinal quelconque) — cette construction n'est sans doute pas aussi simple qu'on voudrait, et, en tout cas, on manque (ou du moins, je manque) de variété dans les exemples.

À cause de la combinaison entre l'écriture de l'entrée précédente et de mon interaction avec des (enfin, surtout un) mathématicien constructiviste à la Bishop/Richman, j'ai tenté de me faire une idée sur la force logique des systèmes admis par les constructivistes. (L'idée est que — pour une raison qu'on ne comprend pas vraiment, mais que je suis tenté de prendre pour un indice empirique de l'existence platonique des entiers — toutes les théories logiques introduites « naturellement » en mathématiques semblent s'arranger selon une échelle totalement ordonnée de « force » convenablement définie. Je voulais savoir où, sur cette échelle, se situent les différents cadres des mathématiques constructives. On m'a recommandé de lire le texte introductif de Martin-Löf The Hilbert-Brouwer controversy resolved? — mais au final il me suggère plus de questions qu'il n'en clôt.) Mauvaise idée : je me suis retrouvé dans un labyrinthe de petits énoncés tordus, tous semblables — et surtout, de gens qui ne communiquent pas assez entre eux, et qui ne présentent pas leurs résultats dans le contexte des autres résultats du même genre.

Certes, le problème n'est pas évident, pour plusieurs raisons :

• D'abord, ce n'est pas évident de définir ce qu'on appelle la force logique d'un système (j'agite pas mal les mains en parlant de ça). Il n'est pas du tout vrai que deux théories logiques naturelles T et T′ soient toujours comparables si on considère toutes leurs conséquences (i.e., il n'est pas vrai que soit toute conséquence de T découle aussi de T′ soit le contraire ; par exemple, la théorie des ensembles de Zermelo avec l'axiome du choix, ZC, est incomparable avec la théorie des ensembles de Zermelo-Fraenkel sans l'axiome du choix, ZF). Il faut pour cela se limiter au moins aux énoncés arithmétiques, sans doute même aux énoncés arithmétiques Π₂ (c'est-à-dire du type <telle> machine de Turing termine pour toute entrée) ou Π₁ (c'est-à-dire du type <telle> machine de Turing ne termine jamais), ou peut-être utiliser la relation une théorie très faible montre que si un énoncé Σ₁ (c'est-à-dire du type <telle> machine de Turing termine sur telle entrée) est démontré par T alors il l'est par T′, voire une théorie très faible montre que si T est inconsistante alors T′ l'est, et si possible en explicitant un lien algorithmique entre une preuve effectuée dans T et une preuve dans T′. Je n'ai pas les idées totalement claires sur les rapports entre tous ces concepts (premier labyrinthe !), et même si je crois qu'au moins dans les cas qui m'intéressent cela ne fait aucune différence, je n'en suis pas totalement sûr. Premier reproche : les gens qui énoncent des comparaisons entre théories ne sont pas toujours très clairs sur ce qu'ils veulent dire, et en tout cas ne font pas du tout l'effort de remettre en contexte ce qu'on peut dire sur ces différentes relations. (À toutes fins utiles, je note quand même que le texte le plus clair que j'aie trouvé qui explique un peu comment les choses s'articulent est l'article introductif The Realm of Ordinal Analysis de Michael Rathjen — cf. notamment les définitions 2.4, 2.14, 2.15 et la remarque 2.16.)
• De même, système admis par les constructivistes n'est pas bien défini, à part le fait qu'il doit s'agir de logique intuitionniste. En tout cas, moi, je ne comprends pas bien ce qui fait qu'on considère que tel ou tel postulat est constructif ou pas. (Comme je le mentionne ci-dessous, je crois comprendre de façon détournée que l'ensemble des parties d'un singleton existe ne peut pas être constructif, mais j'ai un peu du mal à voir ce qu'il y a de non constructif à l'ensemble des parties d'un singleton, ou en tout cas au simple postulat de son existence !) Ce qui est sûr, c'est qu'il y a un autre labyrinthe ici, de théories logiques, de systèmes de typage et de systèmes de preuves, etc., et que je suis loin d'avoir une idée clair du rapport entre toutes ces choses. L'article de Barendregt Introduction to generalized type systems (où il introduit le fameux λ-cube, et un cube analogue de théories logiques), par exemple, est très bon pour se faire une idée rapide de ce qu'est un système de typage, mais on reste ignorant du rapport précis entre ces systèmes de typage et les théories des types introduites par Martin-Löf. Un des problèmes est probablement que les informaticiens théoriciens et les matheux ne se parlent pas suffisamment, et disent des choses semblables dans des langages différents, ce qui fait qu'il est difficile de relier ce que disent les uns et ce que disent les autres.
• L'ajout d'un axiome en apparence innocent peut changer complètement la force d'un système. (Parfois il peut même le rendre inconsistant : voir le paradoxe de Girard, expliqué par exemple ici, qui est une sorte de version du paradoxe de Burali-Forti en théorie des types. Pour le résoudre, on a tendance à introduire des notions d'univers, typiquement une suite infinie d'univers emboîtés, un peu comme Grothendieck l'a fait pour se débarrasser de difficultés en théorie des catégories, et ce genre de postulat n'est évidemment pas innocent du point de vue de la force logique.) Ainsi, l'axiome du tiers exclu (qui change la logique intuitionniste en logique classique) ne se contente pas de briser le constructivisme, il peut aussi augmenter considérablement la force logique d'une théorie — j'ai mis longtemps à le comprendre, surtout que superficiellement ceci semble contradictoire avec la traduction de Dragalin-Friedman. C'est le cas notamment de la théorie CZF, ou ZF constructif (décrite en détails dans ces notes sur CZF par Aczel et Rathjen), une des théories standard pour les maths constructives : toute seule, elle a la même force arithmétique Π₂ qu'une théorie classique assez faible, KP (je n'ai d'ailleurs pas de bonne référence pour ce fait, mais voir page 24 du texte de Rathjen que j'ai déjà cité), alors que quand on ajoute l'axiome du tiers exclu elle devient équivalente à ZF, qui est très forte (voir la proposition 7.5 des notes d'Aczel et Rathjen citées ci-dessus). De façon encore plus surprenante, l'axiome l'ensemble des parties d'un singleton existe (i.e., la classe des sous-ensembles de {∅} est un ensemble) change considérablement la force arithmétique de CZF (voir la preuve de 7.3(ii) dans le texte d'Aczel et Rathjen et le paragraphe ci-dessous). Et je crois comprendre que pour des théories des types (comme le calcul des constructions) c'est le cas de l'axiome d'irrelevance des preuves, ou de l'axiome du choix (alors que par rapport à ZF classique, l'axiome du choix apporte une force logique nulle : par un argument de Gödel, tout énoncé aritmétique prouvable dans ZFC l'est en fait dans ZF).

Une des choses que j'aimerais comprendre, par exemple, c'est quelle est la force logique du calcul des constructions inductives (une extension du calcul des constructions qui se situe au coin le plus complexe du cube de Barendregt mentionné ci-dessus) et du système Coq qui se base dessus. Et aussi de savoir si on doit le considérer comme « constructif ». (La réponse à ces deux questions dépendra sans doute, et de façon subtile, de ce qu'on met dedans : il est certain que l'ajout du tiers exclu augmente énormément la force logique, par exemple, mais j'ai les idées beaucoup moins claires sur l'introduction du type Prop « imprédicatif » ou de l'irrelevance des preuves.) J'ai toutes sortes de réponses partielles à ces questions, mais surtout un grand mal à les relier les unes aux autres, de nouveau, parce que les gens qui ont écrit ces réponses ne se citent pas les uns les autres pour expliquer le lien entre ce qu'ils disent. Pour commencer, j'apprends dans un vieil article de B. Werner intitulé Sets in Types, Types in Sets que Coq avec ω univers est (co-interprétable, donc) équiconsistant avec ZFC avec ω univers (de Grothendieck, i.e., cardinaux inaccessibles) — sauf qu'en fait, en lisant bien, on voit que c'est après ajout de l'axiome du tiers exclu (et peut-être un autre axiome bizarre), donc ça ne m'apprend qu'une borne supérieure (très faible) sur la force de Coq sans le tiers exclu. Un article de Rathjen intitulé Constructive Zermelo-Fraenkel Set Theory, Power Set, and the Calculus of Constructions (publié dans un volume en l'honneur de Martin-Löf) m'apprend, si je lis bien !, qu'une certaine théorie basée sur le calcul des constructions (et/ou la théorie des types de Martin-Löf — comme je l'ai dit, je ne comprends pas bien le rapport entre elles), comportant une règle d'« irrelevance des preuves », a une force logique équivalente à la fois (1) à CZF + l'axiome d'existence de l'ensemble des parties [d'un singleton, cela suffit], (2) à la théorie classique Power-KP (essentiellement, Kripke-Platek si on ajoute la fonction « ensemble des parties » au langage), ou encore (3) à la théorie des ensembles classique de Zermelo à laquelle on ajoute un nombre d'univers égal à l'ordinal de Bachmann-Howard. La thèse d'Alexandre Miquel émet (conjecture 9.7.6) une supposition qui pourrait sembler contradictoire avec ça, mais peut-être pas parce qu'il y a toutes sortes de subtilités techniques qui diffèrent entre les théories comparées (en tout cas, les deux sont d'accord sur le fait que la force logique dépasse celle de la théorie des ensembles de Zermelo) — en revanche, je ne comprends pas si l'axiome d'irrelevance des preuves a dû être postulé pour obtenir la borne inférieure. En tout cas, il s'agit de théories assez « fortes » car elles dépassent l'arithmétique du second ordre (qualifiée de fossé infranchissable dans le texte de Martin-Löf cité tout au début). A contrario, j'ai trouvé un texte d'Aczel, On Relating Type Theories and Set Theories ainsi qu'un plus vieux texte de Rathjen, The strength of Some Martin-Löf Type Theories, qui arrivent à la conclusion que diverses théories des types entre lesquelles je m'embrouille complètement sont, pour leur part, d'une force logique très modeste (en-deçà du fossé infranchissable évoqué par Martin-Löf). La différence doit donc bien être dans l'existence de l'ensemble des parties [d'un singleton], dans le type Prop de Coq que différents auteurs qualifient d'« imprédicatif » même si j'avoue ne jamais avoir compris ce que ce mot veut dire, et/ou dans l'irrelevance des preuves.

Mais bon, trève de détails techniques (que j'avoue avoir écrits surtout pour m'en souvenir plus tard) : ce dont je veux surtout me plaindre et de la façon dont les gens ne communiquent pas assez. Par exemple, j'ai trouvé extrêmement peu d'arêtes pour la relation être cité par entre les équipes d'informaticiens qui gravitent autour de Coq (du genre, B. Werner) et les équipes de matheux qui font de la théorie ordinale de la démonstration (comme le M. Rathjen que j'ai cité plusieurs fois ci-dessus, et dont les articles répondent très souvent aux questions que je me pose en théorie de la démonstration) : pourtant, ces deux groupes de gens font de la logique parfois intuitionniste et notamment de la théorie de la démonstration ; et pourtant, il est essentiel pour bien faire comprendre ses résultats de les mettre en perspective par rapport à d'autres résultats du même genre. Ceci me rappelle cette citation de Giancarlo Rota :

A leader in the theory of pseudo-parabolic partial differential equations in quasi-convex domains will not stoop to being understood by specialists in quasi-parabolic partial differential equations in pseudo-convex domains.

— Indiscrete Thoughts (XXI. Book reviews: Professor Neanderthal's World)

Résultat, moi qui ne suis spécialiste ni des équations différentielles pseudo-paraboliques dans les domaines quasi-convexes ni des équations différentielles quasi-paraboliques dans les domaines pseudo-convexes, je dois m'arracher les cheveux à me demander quel est le rapport entre tel résultat de la première théorie et tel résultat apparemment très semblable de la seconde, sachant qu'aucun ne mentionne l'autre pour m'éclairer sur le sujet.

[Ajout : il y a différents compléments dans les commentaires, grâce aux explications gentiment fournies par Arnaud Spiwack ; la moralité est qu'en tant que mathématicien classique non habitué aux maths constructives et/ou précatives, je m'embrouille complètement sur les nuances entre ce que ces différentes théories intuitionnistes prouvent ou interprètent (quelle est la force supplémentaire apportée par l'axiome du tiers exclu, par celle de l'axiome 0≠1, auquel je n'avais pas du tout pensé, la force de leur fragment de double négation, la difficulté à montrer leur cohérence versus leur normalisation : tout ça est très confus pour moi). Mais je retiens quand même que la comparaison entre Coq et ZFC n'est pas claire en l'état actuel des choses.]

Nouvel ajout (2024-12-03) : cette réponse par Loïc Pujet sur le site StackExchange sur les assistants de preuve fournit un excellent résumé de l'état de l'art de la force logique de différents systèmes de preuve/typage aussi bien de la famille de Martin-Löf que de celle du cube de Barendregt.

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.

[Ajout : voir aussi ce message sur Reddit où j'explique de façon peut-être plus pédagogique (mais en anglais) en gros les mêmes choses que ci-dessous.]

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

[Lire la suite…]

Mon poussinet et moi sommes allés voir le dernier Disney, Maleficent (de, par, pour et avec Angelina Jolie ). J'ai vraiment beaucoup aimé. C'est mignon et rigolo, et c'est astucieux sans prétendre être profond. Certains disent que ce n'est pas un film pour enfants parce qu'il prend le point de vue de la « méchante », mais je pense justement que ce n'est pas mal que les enfants apprennent tôt que la morale est souvent un peu plus subtile que des gentils d'un côté et des méchants de l'autre : donc je dirais que c'est un film pour les enfants de 9 à 99 ans.

Inutile de dire que ce n'est pas très fidèle au conte de Perrault. Mais le retournement de point de vue est intéressant.

[Ajout (2014-06-15T15:55+02:00) : Je devrais mentionner que non seulement le film passe le test de Bechdel, ce qui n'est pas aussi fréquent que ça devrait l'être, mais qu'il est même, sinon féministe, au moins pas trop stupidement patriarchal, ce qui pour une interprétation de la Belle au Bois Dormant n'était pas forcément évident, quoi que puisse en penser M. Bettelheim.]

J'ai fait un faux mouvement, mes lunettes sont tombées par terre, et le verre s'est fracturé. Pourtant elles ne tombaient pas de bien haut, et le parquet chez moi n'est pas ce qu'il y a de plus dur — mais c'est ça l'inconvénient des verres à indice de réfraction élevé que doivent porter les forts myopes comme moi, c'est aussi plus fragile.

Bref, j'ai commandé deux nouvelles paires chez mes opticiens hong-kongais préférés, mais en attendant, me revoilà avec mes lunettes précédentes, qui font une bonne dioptrie de moins à l'œil gauche, et je suis parti pour avoir droit à de sérieux maux de tête.

Je suis fatigué, mais fatigué, fatigué, fatigué…

On me demande de trouver un exemple pédagogique d'un calcul pour lequel une calculatrice donnerait un résultat faux mais qu'un mathématicien saurait faire (en un temps raisonnable). Le meilleur exemple que je voie est celui-ci : sin((1+√2)²⁰⁰×π). Une calculatrice (par exemple celle de Google) renvoie un résultat bidon, alors que n'importe quel mathématicien compétent voit que (1+√2)²⁰⁰ + (1−√2)²⁰⁰ est un entier pair, si bien que sin((1+√2)²⁰⁰×π) = −sin((1−√2)²⁰⁰×π) est extrêmement petit, et on peut même en faire une estimation de tête : sin((1−√2)²⁰⁰×π) est plus petit que ((1−√2)²⁰⁰×π), qui est lui-même plus petit que (½)²⁰⁰×π, or 2¹⁰=1024 est supérieur à et environ égal à 1000=10³, donc (½)^20×10×π est inférieur à et environ égal à 10⁻⁶⁰×π, bref, de tête j'aurais dit que sin((1+√2)²⁰⁰×π) est compris entre −4×10⁻⁶⁰ et 0. La valeur correcte est environ −8.75×10⁻⁷⁷, donc mon estimation n'est pas terrible (quoique, en évaluant un peu plus finement le rapport entre 0.41 et 0.5 j'aurais réussi à être plus précis), mais c'est tout de même mieux que les 0.97 retournés par Google.

Quelqu'un a-t-il un meilleur exemple ?

⁂

À part ça, aucun rapport (si ce n'est celui des calculs auxquels dont on doit se méfier), mais mon poussinet et moi avons déclaré nos impôts[#] : à cause de l'arrondi à l'euro le plus proche pratiqué par l'administration fiscale, nous perdons un euro à être PACSés (par rapport à la situation où nous payerions nos impôts séparément). Ça c'est de l'optimisation fiscale du tonnerre !

[#] Dédicace spéciale aux pédants pourfendeurs de métonymies qui trépignent en pensant on ne déclare pas ses impôts, on déclare ses revenus. Mais oui, moi aussi je vous aime.

Le fait que j'aie attrapé un nouveau gros rhume comme je les collectionne, juste quand je commençais à voir le bout de trois semaines très chargées, n'aide certainement pas. Les jours fériés n'aident pas non plus : l'arnaque avec les jours fériés, c'est que quand il y en a, j'ai exactement autant de choses à faire dans la semaine mais moins de temps pour les faire. Le week-end de la Pentecôte, j'ai une obligation sociale qui me fatigue rien que d'y penser. Et, bien sûr, les bruits divers et variés qui m'empêchent de dormir n'aident pas non plus à me reposer.

J'aurais surtout besoin de vacances (depuis septembre, je n'ai réussi à en prendre qu'une semaine entre Noël et le nouvel an). Mais comme je voudrais surtout prendre des vacances chez moi à Paris (parce que je trouve voyager tellement fatigant que ça annule tout effet bénéfique de la coupure), je suis victime du fait que personne ne prend ça au sérieux. Je veux dire, si quelqu'un vous demande de faire quelque chose un certain jour, répondre je ne pourrai pas, je serai en vacances à Saint-Trouduc-lès-Trèsloin est considéré comme une excuse valable, mais pas je ne pourrai pas, je serai en vacances ici (les gens vous disent : ben si tu es là, tu peux bien trouver le temps… — bon, peut-être que mon problème est que je ne sais pas assez dire merde aux gens, mais j'ai pourtant l'impression de le dire tout le temps).