Comments on Quelques mots (essentiellement méta) sur l'intuitionnisme et les mathématiques constructives

Sur cette histoire de call/cc, oui, c'est possible d'extraire des preuves classiques vers des programmes basés sur call/cc… mais ils ne se comportent pas comme on l'imagine ! En gros, un programme va retourner des valeurs avec des applications de call/cc… qui pourront backtracker après coup ! Par exemple, on peut imaginer une fonction classique qui renvoie le minimum d'une fonction d'entiers vers entiers. Elle va renvoyer quelque chose de compliqué qui pourra probablement s'interpréter comme la valeur de la fonction en 0. Mais cette valeur n'est pas forcément le minimum. Le truc, c'est que la fonction renvoie aussi une « preuve » que cette valeur est bien la minimum. L'unique manière d'utiliser cette preuve, c'est de lui donner une autre valeur : deux choses peuvent alors se produire. Soit le nouvelle valeur donne un résultat plus grand par la fonction que 0, et dans ce cas on peut dire que 0 est bien un genre de minimum local. Soit la valeur donnée était meilleure que 0 (et on est bien embêté). Dans ce dernier cas, la « preuve » utilise une application à call/cc pour essentiellement revenir au moment où on demandait le minimum de la fonction… et renvoie ce nouveau minimum trouvé. Autrement dit, la valeur renvoyée par une fonction basée sur call/cc n'est jamais qu'un genre de valeur temporaire en attendant mieux. Ce n'est pas ce à quoi on est habitué avec l'extraction de programmes! ☺️

Bon, tout ça n'est qu'un aspect de la réalisabilité classique. C'est cool, et je trouvais surprenant de ne pas avoir vu de référence dans cette entrée 😊 (Je l'ai lu assez vite : j'ai pu oublié un point important.)

Cette entrée vole pour sa majeure partie largement au-dessus de mon niveau :) mais pour « une saveur de [hum, comment on dit "a taste of" en français, déjà ?] » je propose « un aperçu » ou « un avant-goût ».
Ce que je trouve gênant dans le raisonnement sur la calculabilité de la fonction des occurrences de 7 dans les décimales de pi, c'est « ah tiens on peut prouver ça ? Euh, ok, je me suis fait avoir, c'est juste une trivialité qui n'apporte rien. » C'est comme si la fonction avait le droit d'appeler un oracle qui lui dit qui elle est (si elle doit bosser ou si on est à k_0). Comment on dit « parlor trick » en français déjà :)

;; This buffer is for text that is not saved, and for Lisp evaluation.
;; To create a file, visit it with <open> and enter text in its buffer.

> et la raison pour laquelle ceci ne vaut que pour ℕ et pas pour un ensemble quelconque est que dans le cas général, la fonction pourrait dépendre de la manière dont son entrée est décrite alors que pour un entier naturel il n'y a pas d'autre description que l'entier lui-même (enfin, quelque chose comme ça).

Oui, c'est une bonne remarque: tant qu'on est capable de canoniser les classes d'égalités, ça ne devrait pas poser de problème particulier en principe.

> (et d'après ce que tu dis, travailler uniquement avec les relations fonctionnelles topossifie le quasitopos).

Je crois, en tout cas. Mais je n'ai pas de référence, et je n'ai jamais eu le courage de faire la preuve.

> Après, là aussi, philosophiquement, je suis un peu tenté de me demander « mais du coup, dans un quasitopos (ou si on n'a pas le choix unique), quel est l'intérêt de la notion de “fonction” et qu'est-elle censée représenter intuitivement, par opposition à une relation fonctionnelle ? »

Honnêtement, je ne suis pas sûr de savoir l'expliquer. Cela dit, un truc sympa dans les quasit-toposes, c'est qu'on peut avoir le tiers-exclu sans compromettre le fait que les fonctions sont toutes (externalement) calculable. C'est bien d'avoir un degrée de liberté de plus, mais ce serait un peu hypocrite de ma part de m'en satisfaire parce que je ne l'utilise pas (je me suis souvent posé la question de pourquoi je ne l'utilisait pas, et je n'ai pas de réponse, mais comme tous les mathématiciens constructiviste, j'ai toujours un sentiment d'ickiness face au tiers exclu).

En Coq, l'absence de choix unique viens du fait que personne ne sait faire une théorie des types dépendents qui supporte le choix unique de manière élégante sans déclencher des paradoxes d'imprédicativité (il y a une solution en théorie des types univalente, mais je ne vais pas aller jusqu'à les appeler élégantes). Donc ça découle principalement de considérations techniques.

Maintenant, je n'ai pas vraiment idée des conséquences de construire une théorie des types dépendants à la Coq et de fournir une interface aux relations fonctionnelles au lieu des fonctions. Il y a sûrement quelque chose qui va casser, mais quoi?

Certains arguent que c'est un bug du système. Personnellement, j'ai beaucoup défendu la position que c'était une bonne chose. Je me sers de la distinction objet/démonstration (que donne l'absence de choix unique) de la façon, très informaticienne, suivante: quand je construit un objet, je fais attention à son efficacité, parce que je vais calculer avec. Alors que les démonstrations, je m'en fiche, et donc je laisse volontier des procédures automatiques les résoudre pour moi.

Mais tout ça n'explique pas vraiment pourquoi les fonctions et les relations fonctionnelles seraient « vraiment » des choses différentes.

> je pense que c'est quand même une mauvaise idée d'utiliser un terme comme « intuitionnisme » pour parler spécifiquement du topos effectif, parce que ce dernier est plutôt dérivé des idées du constructivisme russe à la Markov (RUSS, dans la terminologie de Bridges & Richman) plutôt que de l'intuitionnisme à la Brouwer (INT).

Je vois. D'un autre côté, je trouve que le topos effectif reflète bien ce que je comprend être l'intuition de Brouwer pour admettre un axiome. En termes modernes, Brouwer note que toutes les fonctions calculables des réels dans eux-mêmes sont continues. Et donc il admet que toutes les fonctions des réels dans eux-mêmes sont continues. Ça ressemble vraiment à la même chose faite dans le topos effectifs.

Mais je ne sais ni suffisamment d'histoire des mathématique ni du topos effectif pour avoir confiance que mon intuition est la bonne.

> même s'il en faudrait encore un pour le cas où on n'accepte même pas le choix dénombrable (voire même pas le choix unique).

Pour les maths constructives sans choix unique, j'appelais ça, à une époque les maths effectives (rapport à l'histoire d'efficacité plus haut). Mais c'est à la fois pédant et confusant (parce que ça n'a pas de rapport avec le topos effectif).

> Ça a manifestement un rapport avec la traduction suivante de la logique intuitionniste dans la logique classique additionnée d'un modalisateur □ vérifiant le système modal S4 :

Marrant! Je n'avais jamais pensé à ça. C'est d'autant plus similaire que ! est une modalité comonadique qui vérifie les (versions linéaires des) mêmes propriétés que □.

> ‣ mais on peut aussi décrire la logique intuitionniste à l'intérieur de la logique linéaire (plus exactement, associer à toute formule de logique intuitionniste une formule de logique linéaire qui est prouvable en logique linéaire si et seulement si la formule de départ l'est en logique intuitionniste), et là, je ne me rappelle plus exactement comment on fait ça.

Il y a plusieurs façons. Mais la plus commune c'est de mapper A → B vers !A ⊸ B, et A∨B vers A⊕B (et le faux vers 0).

> mais toutes ces choses incluent au moins une forme de l'axiome du choix (dépendant ? ou au moins dénombrable).

Je ne suis pas au courant que Bishop utilise le choix dénombrable. Tu saurais à quoi il est utilisé?

En tout cas, je pense que le constructiviste typique n'utilisera pas l'axiome du choix.

> Les topoï valident cependant au moins l'« axiome du choix unique » (si pour tout x dans X il existe un unique y dans Y tel que P(x,y), alors il existe f:X→Y tel que pour tout x dans X on ait P(x,f(x))), donc on peut s'interroger sur ce qu'on peut dire en supprimant même ça

Et bien, formellement, on tombe dans les quasi-toposes arbitraires. (formellement un quasi-topos où le choix unique est vérifié est un topos).

C'est essentiellement ce qui se passe dans Coq: pas de choix unique. On le vit surprenamment bien.

Après, il y a diverses conséquences: la première c'est qu'injectif et surjectif ne veut plus dire isomorphisme (c'est équivalent au choix unique en fait). Mais plus amusant, il y a le fait que dans la catégorie, disons, des groupes abéliens, on n'a plus la propriété que tout sous-groupe est le noyau d'un morphisme (ce qui fait que la catégorie des groupes abéliens n'est, ironiquement, plus une catégorie abélienne. Elle n'est plus qu'une catégorie préabélienne (tout ces pré et ces quasi devraient réjouir ton club contexte)).

> Au final, tout ça est fort confus.

Je dois bien l'admettre. La terminologie n'est pas super claire. Finalement, dans le constructivisme, chacun choisi un peu son régime, et ça n'a peut-être pas de sens de faire une typologie précise de toutes les variantes possibles.

Disons, donc, que j'aime bien, personnellement, l'idée que constructif qualifie le langage interne des topos, et de réserver intuitioniste au langage du topos effectif (parce que les mathématiques de Brouwer étaient très self-awares: elles savaient qu'ils vivaient dans un monde de bidules calculables, et elles pouvaient s'en servir, ce qui correspond bien au topos effective à mon sens)

> par ailleurs, je suppose que les « arènes » dont tu parles sont les « assemblies », mais c'est peut-être autre chose

Oui, c'est ça, je me suis confusé dans le vocabulaire…

Je lirai le livre de van Oosten, merci pour la référence.

Et la logique linéaire là dedans. Est-ce un approfondissement des logiques intuitionnistes, constructivistes et classiques ou ces dernières n'ont rien à voir avec l'autre ? (merci pour vos réponses le cas échéant)

Le constructivisme me rend bavard. Je vais essayer de rester concentrés.

D'abord: je veux juste insister un peu, pour le bénéfice du lectorat, que les mathématiciens constructivistes ne se réfèrent pas aux règle de la logique constructives pour faire des maths (pas plus que le mathématicien classique aux règles de la logique classique).

Sinon, sur intuitioniste vs constructif, tout le monde n'utilise pas les deux mots pour des concepts distincts. Mais quand il sont distingué, ma compréhension c'est que la plupart du temps, l'intuitionisme se réfère aux mathématiques de Brouwer, où un peu plus de choses sont vrais que n'est prêt à le considérer le mathématicien constructiviste moderne (en particulier le fan principle, et le principe de continuité). En fait, ma compréhension, c'est que les mathématiques intuitioniste correspondent assez bien (peut-être exactement?) à la logique interne du topos effectif. Alors que les mathématiques constructifs peuvent être vus comme étant faites dans un topos arbitraire (même si le mathématicien constructiviste ne le pense typiquement pas comme ça).

En parlant de topos effectif. Je n'ai jamais vraiment trop compris sa construction. Mais, si j'ai bien suivi, le topos des arènes (de réalisabilité) est un quasi-topos. Il y a une construction, que je crois qui marche, pour faire un topos depuis un quasi-topos: garder les mêmes objets, mais choisir les relations fonctionnelles (internes) comme morphismes (est-ce que cette construction a un nom?). Est-ce que c'est équivalent à la construction du topos effectif?