corps réels clos: complexité

christophe c · August 2017

Lors d'entretiens avec des experts récemment sur cette question, je me suis rendu compte à mon grand désarroi que ça fait peut-être 30 ans (enfin 20-25) que je crois au fait qu'un problème n'est pas ouvert alors qu'il l'est. Je produis donc un post très précis pour lever toute ambiguité.

L'ensemble véritié (je le note VR) du corps $(\R,+\times)$ est célèbre entre autre parce qu'il est récursif, ie il existe au moins un programme qui le calcule et en plus il n'est que l'ensemble des théorèmes d'une théorie complète bien connue qui est celle des corps réels clos de caractéristique $0$.

Il s'agit de l'ensemble des énoncés du premier ordre qui sont clos, sans paramètres et qui sont vrais dans $(\R,+\times)$. On peut le considérer comme un ensemble d'entiers en codant trivialement les symboles.

Comme toujours c'est l'alternance des quantificateurs qui fait exploser la complexité. Cependant, la stratégie consistant à éliminer les quantificateurs (voir littérature) permet de le calculer en $O(2^{(2^n)}$ pour les énoncés ayant $n$ symboles.

Cela fait à peu près 20-25 ans que j'ai cru lire dans plusieurs articles ou entendre dans des bars lors de demandes de ma part à ce propos <<qu'il avait été prouvé que tout algorithme qui le calcule nécessite au moins $O(2^{(2^n)}$>>

Je mets des guillemets car c'est probablement une erreur que je commets, un malentendu, une discussion récente avec un expert de la question surement bien plus informé que moi de ces choses m'ayant dit que le $<<O(2^{(2^n)}$ borne inférieure prouvée$>> ne s'applique qu'à une famille particulière d'algorithme. Pour être précis, il est existe des formules AVEC variables libres (donc des propriétés définissables) dont on prouve que toute expression de la même propriété sans quateurs prend au moins 2 à la puissance (2 à la puissance la longueur de la formule).

L'expert m'a dit qu'à sa connaissance, il ne semblait pas y avoir de borne inférieure connue (en dehors des bateaux faciles à prouver) pour la complexité de VR.

Je lance donc un appel à documentation. Toute personne qui voudra bien me dire ce qu'il en est de cette question sera un ange ;-) Je trouve, en effet, ça étonnant que pour un problème pareil, il n'y ait pas ou bien une résolution publiée officielle ou bien une diffusion large du fait que c'est ouvert (concernant les complexités "raisonnables" dont on ne sait pas encore prouver qu'elles minorent celle de VR)

GaBuZoMeu · August 2017

Quelques précisions. Christophe avait commencé par raconter des choses très éloignées de ce qu'on sait sur le sujet ici (parlant en particulier d'une complexité en tour d'exponentielles de hauteur la taille de l'entrée, ou le nombre de variables, on ne savait pas trop).
J'ai corrigé en mentionnant le caractère doublement exponentiel en le nombre de variables de l'élimination des quantificateurs (qui donne bien sûr un algorithme de décision pour la théorie des corps réels clos). On peut trouver une information détaillée dans le manuel "Algorithms in Real Algebraic Geometry" disponible en téléchargement ici. On y trouve des renseignements détaillés sur ce qu'on fait de mieux comme complexité pour l'algorithme de décision et pour l'algorithme d'élimination des quantificateurs au chapitre 14, et le fait que la complexité de l'élimination des quantificateurs est intrinsèquement doublement exponentielle en le nombre de variables en section 11.4. (J'ai donné ces renseignements à Christophe par MP pour ne pas polluer le fil).
Il faut savoir que les bornes inférieures de complexité pour certains problèmes s'obtiennent souvent à partir de résultats bornant par exemple la complexité de la topologie d'un ensemble semi-algébrique en fonction de la complexité de sa description. Donc si un ensemble a une topologie compliquée, il a forcément une description compliquée. L'idée de la preuve de la borne inférieure pour l'élimination des quantificateurs consiste à produire une famille de formules indexée par $j$, de longueurs linéaires en $j$ (et avec $2j$ alternances de quantificateurs), qui disent que $(x+iy)^{2^{2^j}}=u+iv$ ; pour $u,v$ donnés, l'ensemble correspondant se compose de $2^{2^j}$ points, et on montre qu'une description sans quantificateurs de cet ensemble est forcément au moins doublement exponentielle en $j$. Tout algorithme d'élimination des quantificateurs est de complexité doublement exponentielle puisque sa sortie est forcément de taille doublement exponentielle dans les mauvais cas.
Ce sont des idées géométriques qui permettent d'obtenir des algorithmes de bonne complexité, et aussi de montrer une borne inférieure de complexité.

Pour le problème de décision, cette démarche ne peut bien sûr pas s'appliquer : un oracle résolvant le problème peut se contenter de répondre "vrai" ou "faux".

christophe c · August 2017

Merci pour ces précisions que tu m'avais effectivement envoyées. Je précise juste un point concernant les dernières lignes de ton post car les néophytes pourraient confondre avec "la question n'a pas d'intérêt" ou pire "n'a pas de sens". Bien entendu je parle d'algorithme n'utilisant pas d'Oracle. :-D (J'ai bien compris ce que tu dis et que ça concerne les configurations d'avant dans ton post je précise pour les lecteurs).

Je le redis je trouve étonnant que ce ne soit ni un problème ouvert célèbre ni un théorème célèbre qui répond. Je n'irais bien sûr pas jusqu'à dire que c'est important comme P=NP mais quand-même.

GaBuZoMeu · August 2017

Un exemple d'élimination des quantificateurs pour les corps réels clos (disons, pour $\R$) ?
$$\exists x\ ax^2+bx+c=0$$
Tu vois, il y a un quantificateur (qui lie la variable $x$). Hop, on l'élimine :
$$(a\neq 0 \text{ et } b^2-4ac\geq 0) \text{ ou } (a=0\text{ et }b\neq 0) \text{ ou }(a=b=c=0)$$
Là il n'y a plus de quantificateur, et c'est équivalent à la formule du haut.

christophe c · August 2017

Exemple de théorie qui élimine les quantificateurs encore plus simple que les corps réels clos:

Les corps algébriquement clos de caractéristique 0 (la théorie des)
Les ensembles ordonnés denses sans minimum ni maximum (la théorie des)

Exercice: comme dire sans quantificateurs la phrase suivante: $ \exists x: x<a$ et $ b<x $ et $c>x$?

samok · August 2017

Bon, vous faites quoi avec ce problème d'Archimède ?

Genre déjà dans quelle théorie vous placez-vous ?

Shah d'Ock bienvenu aussi.

S

GaBuZoMeu · August 2017

Alfred Tarski démontre l'élimination des quantificateurs pour la théorie de $\R$ (dans le langage des corps ordonnés) dans un mémoire qui s'appelle "A decision method for elementary algebra and geometry".
Je te laisse écrire l'énoncé d'Archimède comme une formule du premier ordre du langage des corps ordonnés, en utilisant les coordonnées des points de la figure dans un repère orthonormé : équations et inégalités polynomiales à coefficients entiers, connecteurs logiques, quantificateurs portant sur des variables de type "réel".

christophe c · August 2017

@samok: en fait, l'élimination des quantificateurs est un moyen pour prouver le théorème qui qui dit que l'ensemble des vérités de la géométrie élémentaire (ou du monde des nombres réels sans supposer les nombres entiers utilisables en variables liées, etc) est un ensemble récursif (c'est à dire qu'il y a un programme d'ordinateur qui le calcule et quand je dis "calcule", qui le calcule dans les DEUX sens, c'est à dire que si tu lui demandes si une phrase est fausse, il te répond "oui, elle est fausse" ou "non, elle est vraie", il ne se contente pas de dire, "comme elle n'est pas vrai, je vais boucler et jamais m'arrêter et tu dois comprendre que ça veut dire qu'elle n'est pas vrai")

Un autre moyen, pour prouver qu'une théorie récursive (l'ensemble de ses axiomes est récursif) a l'ensemble de ses théorèmes qui est aussi récursif, c'est de prouver qu'elle est complète, à savoir que si un truc n'est pas prouvable alors son contraire est prouvable. En effet, il suffit alors de lancer un programme qui fait défiler toutes les preuves de maths (et même te contenter du langage de la théorie) et d'attendre une preuve de X ou une preuve de nonX. Comme l'un des deux arrivera, tu auras gagné.

Concernant les théorèmes d'élimination des quantificateurs, certains sont faciles à prouver, d'autres sont difficiles (celui sur les corps réels clos nécessite une patience que je n'ai pas par exemple, et de lire des calculs etc). Par contre, ils sont presque toujours "intuitivement évident". Cela provient de ce que décider $\forall x\exists y\forall z: blabla$ (exemple, mais tu peux mettre autant de quantificateurs que tu veux) se fait en étant DEUX personnes et non une et en jouant (le partisan du faux joue $x$ et $z$ et celui du vrai joue $y$ (et on joue dans l'ordre gauche vers droite en connaissance des coups précédents). Pour l'intuition (même si ça ne fait pas une preuve), il suffit de t'imaginer en train de jouer contre des gens à ce jeu, par exemple, quand les coups sont dans IR et que blabla est limité dans sa formulation à être écrit avec des +,fois, =, implique et là tu vois que c'est "facile" de comprendre que $(\R,+,\times)$ ne peut être que "décidable" (quand un joueur est bien immergé dans le jeu, ses coups sont essentiellement "déterminés", tout se passe comme dans un jeu fini, il n'a qu'un choix uniformément fini*** à faire à chaque fois)

Et bien tu peux très bien faire pareil avec la géométrie, c'est à dire ne pas forcément traduire le truc en analytique mais tout simplement te demander si des énoncés écrits juste avec "align(x,y,z)" comme prédicat et des quantificateur peuvent donner lieu à un jeu "difficile"

Mais attention: ceci n'est pas "une preuve" et surtout, la complexité explose, même si le jeu est facile, exactement comme pour P=NP (à 2, la position du prouveur d'une formule prouvable est parfaitement trivial et il n'a aucune astuce à développer pour gagner, à 1 seul, c'est co-NP-complet)

*** à noter que c'est général d'ailleurs, ça vient de la locale compacité de IR (mais la géométrie est carrément compact (projectivement) donc c'est encore mieux): si $S$ est un fermé de l'espace compact $E^{n+1}$ alors toute formule définissant une partie $A$ de $E$ de la forme $\{x\in E \mid Q_1x_1Q_2x_2..Q_nx_n: (x,x_1..x_n)\in S\}$ a l'incroyable avantage de ne pas pouvoir compliquer les choses, car $A$ est forcément fermé (les $Q_i$ sont des éléments de $\{\forall ; \exists\}$). Comme slogan, tu pourrais dire "la compacité bloque la complexité"

samok · August 2017

Bonjour Christophe,

merci pour la peine donnée, je reste sur ma faim mais GBZM m'a donné la référence si je veux me faire une idée précise. Mais une dernière question qui frise l'insolence : où est-ce programme ?

S

christophe c · August 2017

De mon téléphone : pas compris ,j'hésite entre ajouter un accent , retirer un trait d'union + combinaison.

Pour la géométrie "au nez" tu ne retirer as pas les Q avec juste le prédicat "sont alignés". il faudrait avoir des "polynômes géométriques". Mais en copiant sur l'ordre je dirai qu'en dehors d'eux on a juste besoin d'ajouter un prédicat qui dit dans elle composante connexe du plan projectif moins 2droites secantes se trouve un point.

pldx1 · August 2017

Bonjour.

Pour le problème d'Archimède (voir la figure ci-dessous, pour fixer les notations). On commence par prouver que:

\[ \left|CA_{1}\right|=2\left|AN_{1}\right|\;;\;\left|CA_{2}\right|=2\left|AN_{2}\right| \]

Pour cela on utilise l'algorithme d'élimination suivant: "pour éliminer les quantificateurs d'un énoncé qui n'en contient pas, il suffit d'éclater de rire". Il est bien connu que cet algorithme est en $O(1)$. Son efficacité a déjà été testée lors de la preuve de la propriété de Desargues.

Ensuite de quoi, il suffit de déterminer les régions de l'espace des variables (aka les coordonnées de $A,C$) pour lesquelles $\overrightarrow{CA_{1}}=\overrightarrow{CB}+\overrightarrow{BA_{1}}$ se traduit par $\left|CA_{1}\right|=\left|CB\right|+\left|BA_{1}\right|$ et celles pour lesquelles cela se traduit par $\left|CA_{1}\right|=\left|\left|CB\right|-\left|BA_{1}\right|\right|$. Voyons voir un traitement effectif de ce problème par élimination de quantificateurs sur un ensemble de formules d'un langage du premier ordre décrivant un corps réel clos.

Cordialement, Pierre. 66556

christophe c · August 2017

Pour les lecteurs qui iraient voir wikipedia information quand même : la définition du mot "corps réel clos" choisie est telle que le théorème du présent fil triviale. Donc ne pas tomber dans le piège de le croire si facile: c'est de prouver l'équivalence entre les définitions de diverses sources qui est difficile.

Édit: erratum je viens de retourner dur wiki je n'avais pas vu de mon téléphone le mot "algébrique". Bon cela dit une partie de mon post est vraie: l'équivalence entre diverses définitions qui circulent n'a rien de triviale.

christophe c · August 2017

J'ai quelques questions supplémentaires qui méritent plus d'être dans ce fil qu'un nouveau:

1) J'ai vu énormément de mes collègues logiciens, de la section théorie des modèles (à laquelle je ne connais à peu près rien, pour info), se faire des séminaires, papiers, colloques, etc, sur les corps ordonnés (enfin me semble-t-il). Pourquoi? Qu'y a-t-il de si important dans les corps? Autant je n'ai aucun mal à comprendre qu'on se passionne pour la théorie des anneaux, car on peut y réduire toute la science presque sans codage et ça donne du jus (essentiellement, les modèles sont (les quotients par) les idéaux premiers et "la logique scientifique" est l'anneau "à sec". Par exemple la conjecture de Hadwiger ou RH sont des conséquences mécaniques de l'énoncé (faux) obtenu en faisant exprès l'erreur de croire que tel ou tel anneau est intégre et une stratégie consiste me semble-t-il souvent à remonter ce qu'on a obtenu en supposant (0) premier (ou plutôt en supposant un certain idéal formel P premier pour ne rien perturber) jusqu'à l'obtenir sans (autrement dit une grosse partie des preuves scientifiques consiste à essayer de prouver que $t^n=0$ implique $t=0$ pour un certain terme dont on a d'abord facilement prouvé qu'il était nilpotent. Mais avec les corps, j'avoue que je ne vois pas trop comment universaliser leur utilité.

2) Est-ce qu'il n'y aurait une preuve infiniment plus facile de prouver la décidabilité (de VR) en prouvant la complétude et de prouver la complétude en montrant "sans peiner" que deux corps réels clos dénombrable avec suffisamment de transcendants sont isomorphes. J'ai la flemme d'essayer, mais est-ce que ceux qui ont essayé savent si c'est dur ou pas?

3) Y a-t-il des gens qui se sont amusés à ajouter $f:x\mapsto $ if $x\neq 0$ then $1/x$ else $0$ et $g:x\mapsto$ if $x\geq 0$ then $\sqrt{x}$ else $-\sqrt{-x}$ et construire des petits kits informatiques où tout énoncé est ainsi ramené à une égalité froide et calculatoire (puisqu'on sait que c'est possible)?

Précision de (3): $x\neq 0$ devient alors $xf(x)-1=0$ et $x\geq 0$ devient $x=(g(x))^2$, or comme on a aussi que $x=0$ et $y=0$ est $x^2+y^2=0$ et $x=0$ ou $y=0$ est $xy=0$, tout se ramène à <<terme = 0>>. L'éliQ donne donc que tout énoncé est prouvablement équivalent à une écriture $machin=0$. Et puis la définition de $g$ ferait plaisir aux cancres, c'est une de leur faute préférée (de confondre $\sqrt{-x}$ avec $-\sqrt{x}$)

GaBuZoMeu · August 2017

Pour cela on utilise l'algorithme d'élimination suivant: "pour éliminer les quantificateurs d'un énoncé qui n'en contient pas, il suffit d'éclater de rire".

Ce qui est plutôt risible, c'est de ne pas voir les quantificateurs universels de l'énoncé, qui sont pourtant bien présents.

Est-ce qu'il n'y aurait une preuve infiniment plus facile de prouver la décidabilité (de VR) en prouvant la complétude et de prouver la complétude en montrant "sans peiner" que deux corps réels clos dénombrable avec suffisamment de transcendants sont isomorphes. J'ai la flemme d'essayer, mais est-ce que ceux qui ont essayé savent si c'est dur ou pas?

Ben essaie, plutôt que de balancer des trucs en l'air. Ce que tu annonces est faux (exercice facile, que je te laisse). Maintenant, c'est suffisamment flou pour que tu puisses prétendre après coup que ce n'est pas ce que tu voulais dire.

christophe c · August 2017

De mon téléphone : la première citation de ton post est celle de pldx.

Merci pour ta réponse mais te rends-tu compte que tu as l'air de mauvaise humeur? La dernière phrase de ton post est franchement accusatrice à mon égard et donne d émoi l'image de quelqu'un qui quand on lui répond dit "c'était pas mon idée". Ce n'est pas gratifiant!!

Oui bien sur que j'étais flou je voulais savoir si "quelque chose en ce sens" pouvait avoir été publié ou résumé avec suffisamment de détails (pas forcément au format article de recherche).

Je peux être un peu plus précis mais ça ferme la questions car si la réponse est non on a tendance à dire "c'est plie" . Avec un ensemble disons dense (pour l'ordre du corps) d'éléments algébriquement indépendants 2 à 2 , 3 à 3, etc. Mais je pense sue tu dis que c'est cette version aussi qui est fausse. Donc ça me répond.

GaBuZoMeu · August 2017

Oui Christophe, je sais faire la distinction entre pldx et toi.

Sinon, voila, tu commences à ajouter une histoire de densité pour l'ordre (au petit bonheur la chance ?), tout en restant dans le flou. Si tu peux être plus précis, sois-le ! Tu es vraiment pénible.

christophe c · August 2017

Mais non, ce n'est pas un revirement, c'est juste que j'ai en quelque sorte "titré" plus qu'énoncé une question, donc j'ai juste dit "avec beaucoup de transcendants" pour juste attirer l'attention sur "ce genre de démarche", et puis comme tu m'as dit que c'est faux, j'ai évolué (mais j'assume l'ancienne version, je ne m'en dédie pas et j'avoue qu'elle est trop flou) vers une proposition plus comment dire cossue (??) où je donne "de l'air" aux "transcendants" pour aller dans le sens "possible".

Mais il n'y a rien de mystérieux, a priori si j'ai la flemme de plonger dans un long exposé de projet, c'est parce que je crains que ce soit faux à la fin, (je ne crois pas à la magie qui va résoudre comme par enchantement la difficulté de l'exercice en ajoutant des constantes et en constatant que tout va mieux). Du coup je pose la question aux gens qui savent en me disant que si telle technique a été répertoriée, ça leur prend une seconde à le signaler.

Je pense à un genre d'astuce "va et vient" comme celle pour prouver que deux ordre dénombrables denses sans extrémités sont isomorphes, mais je le répète, je demande ça "comme ça", je ne demande pas "qu'on essaie de faire l'exo à ma place", je demande juste si "un truc dans ce genre" a été signalé (je me doute que les logiciens étant loin d'ici et des forums de maths a priori, si une telle preuve avait existé dans l'intimité de leurs réunions, ce n'est pas forcément elle qui aurait été diffusée (puisqu'elle pose quelques difficultés au grand public matheux, ces histoires de va et vient et de modèle) puisque la "tienne", enfin celles de la famille de ce que tu as publié, et diffusé aussi pour l'enseigner avec les tableaux de variations-signes avait vocation à être immédiatement adopte par les matheux

Si le problème de "la facilité" m'intéresse c'est parce que ce théorème me fait penser à Jordan: on en est sûr et on n'arrive pas à dire pourquoi (sous une forme preuve de maths) sans mille efforts

christophe c · August 2017

Oui du coup, pour être précis, je m'en tiens déjà à la question du post-téléphone: soit deux corps réels clos dénombrables et archimédiens (bon je rajoute archimédien pour l'instant, au premier ordre.... pas sûr que ça apporte grand chose) possédant tout deux un ensemble dense d'éléments complètement indépendants algébriquement (autrement dit, une suite finie injective d'éléments d'un tel ensemble se comporte en tout point comme une liste d'indéterminées), je prends l'avion à 5H, je suis un peu fatigué pour faire un énoncé latex.

Question: sont-ils isomorphes?

J'imagine que la réponse est non (tu ne te serais pas contenté de me répondre non, même si tu avais des reproches à faire à la question vague, tu devais avoir un "non" plus général que ça en tête). Et c'est là où je redeviens flou: y a-t-il un moyen d'améliorer encore l'hypothèse pour obtenir un "oui"?

GaBuZoMeu · August 2017

Bon tu as compris l'exercice que j'avais posé et fini par voir que l'archimédianité était une obstruction à ce que tu disais. Mais comme je l'avais prévu, tu vas maintenant m'expliquer qu'il fallait bien comprendre que tu le sous-entendais de puis le début ...

christophe c · August 2017

Mais arrête de m'accuser de tous les maux*** :-S :-S :-S de la Terre bon sang, je ne sous-entendais rien "depuis le début" et non je n'avais pas vu que l'archimédianité pose un souci, je l'ai ajoutée pour renforcer l'hypothèse (c'est sûr qu'il sera pas facile d'avoir un isomorphisme si on demande aux uns d'être tous "petits" et à certains autres de l'autre d'être "infinis"). Dans le fil précédent, j'ai même signalé cash en détail mon processus de sincérité.

*** c'est vraiment terriblement injuste (même si je m'en fiche, c'est plutôt le côté "mauvaise humeur" qui me touche) en plus dans la mesure où je suis quasiment le seul intervenant du forum qui s'en tape et n'a rien à perdre et ne commet justement jamais ce genre de propos "de justification" du genre "je me suis trompé parce que..excuses bidons". Je suis un des seuls à poser des questions sans être un étudiant, à me tromper souvent, à intervenir quand je suis béotien, etc. Donc pourquoi me dépeindre bizarrement comme ça comme les habituels "intellos" qui n'aiment pas se tromper??? :-S
Vu le nombre de conneries lus grosse que moi que je dis en plus, je ne comprends même pas qu'on puisse imaginer ça (que je puisse vouloir faire croire que je ne me trompe pas) :-S

GaBuZoMeu · August 2017

Autre exercice : deux sous-corps réels clos de $\R$ ne peuvent être isomorphes que s'ils sont égaux.

christophe c · August 2017

Merci pour ces exercices. Bon je vais au dodo, je me lève à 3h50. ;-)

pldx1 · August 2017

Bonjour,

Revenons sur l'élimination "par éclat de rire" concernant les quantificateurs dans la formule $\def\tri#1{\mathcal{T}_{#1}}$ $$\left( \forall\, p_{1}, p_{2}, p_{3}, q_{1}, q_{2}, q_{3}, r_{1}, r_{2}, r_{3}\right)\left( \det\tri 4=\det\tri 1\times\det\tri 2\times\det\tri 3^{*} \right) $$
On peut toujours plonger cette élimination dans la théorie des corps algébriquement clos, ou dans celle des corps réels clos.Il se trouve simplement que ces propriétés de clôture n'ont rien à voir avec la formule à traiter. il suffit ici de se placer dans une théorie beaucoup plus banale et de se contenter de developper les deux membres, pour constater qu'ils ont même forme réduite.

Remarque1: il est algorithmiquement plus efficace de développer (rhs-lhs) et d'arriver sur $0$, mais cela donne évidemment la même réponse.

Remarque2: on constate l'efficacité de la géométrie projective: deux droites se coupent toujours, deux points définissent toujours une droite, et si les "deux" étaient confondus, l'objet résultant sera l'exception nulle, qui se propagera quel que soit le calcul entrepris. C'est ce qui se passe ici avec $\det\tri 1$ et $\det\tri 2$.

Remarque3: on remarquera que nous n'avons pas utilisé "s'ils coincident numériquement, alors ils sont égaux formellement" (qui est faux dans la généralité la plus générale), mais "s'ils sont égaux formellement, alors ils coïncident numériquement" (qui est une platitude plate).

Cordialement, Pierre.

corps réels clos: complexité

Réponses

Bonjour!

Catégories

In this Discussion

Qui est en ligne 1