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

MartinShadok (2019-04-29T10:12:33Z)

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

JML (2019-04-18T12:41:06Z)

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à :)

Arnaud Spiwack (2019-04-18T07:28:29Z)

;; 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 □.

Ruxor (2019-04-17T12:39:26Z)

@Arnaud Spiwack:

Concernant Bishop et l'axiome du choix, j'avoue que je ne suis pas très sûr de ce qu'il admet comme variante, et dans quelles conditions il s'en sert. Peut-être que j'ai mal compris. Ses propres livres ne sont pas très clairs sur ce point et ne semblent pas dire explicitement « j'accepte l'axiome du choix suivant <…> ». Néanmoins, comme source pour le fait qu'il admet ou utilise au moins l'axiome du choix dénombrable, voir <URL: http://mathoverflow.net/questions/260445/bishop-quote-stating-that-axiom-of-choice-is-constructively-valid >, ou bien la phrase suivante que je tire de l'article de Diener cité dans mon entrée : « traditionally the use of the axioms of countable and dependent choice has been more or less tacitly accepted in Bishop style constructive mathematics ». Il y a des exemples explicitement signalés dans le livre de Bridges & Richman (des épigones de Bishop, donc), « Varieties of Constructive Mathematics », par exemple après la preuve du théorème 1.1 du chapitre 2.

La motivation philosophique derrière le passage de ∀n∈ℕ.∃z∈Z.(P(n,z)) à ∃f:ℕ→Z.∀n∈ℕ.(P(n,f(n))) semble être que comme l'existence intuitionniste prétend justement assurer non seulement l'existence d'un z pour chaque n mais l'existence d'un procédé explicite pour le produire, donc il devrait suffire d'appliquer ce procédé, ce qui doit donner une fonction f ; 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).

Il me semble que l'axiome du choix dépendant ou au moins dénombrable permet d'identifier les réels de Cauchy avec les réels de Dedekind, ce qui est quand même bien pratique pour faire de l'analyse (ce qui était le but principal de Bishop, au départ).

Merci aussi pour les éclaircissements sur le choix unique comme différence entre topoï et quasitopoï : ça me permet de bien mieux comprendre cette dernière notion. 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 ? » (et d'après ce que tu dis, travailler uniquement avec les relations fonctionnelles topossifie le quasitopos).

Pour la terminologie, même si c'est confus, 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). Le texte de Diener (encore lui) ou le livre de Bridges & Richman éclairent assez bien sur ce qui est valable dans l'un et pas dans l'autre, ou réciproquement. Je crois finalement que les termes « CLASS », « RUSS », « INT » et « BISH » ne sont pas mauvais, 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).

S'agissant de l'interprétation de la logique intuitionniste dans la logique linéaire, je trouve dans le texte de Girard (<URL: http://girard.perso.math.cnrs.fr/Synsem.pdf >) la traduction suivante :

‣ A⇒B par (!A)⊸B
‣ A∧B par A&B
‣ A∨B par (!A)⊕(!B)
‣ ⊤ inchangé
‣ ⊥ par 0
‣ ∀x.A(x) inchangé
‣ ∃x.A(x) par ∃x.(!A(x))

(à appliquer récursivement, bien sûr). Ç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 :

‣ A⇒B par (□A)⇒B
‣ A∧B inchangé
‣ A∨B par (□A)∨(□B)
‣ ⊤ inchangé
‣ ⊥ inchangé
‣ ∀x.A(x) inchangé
‣ ∃x.A(x) par ∃x.(□A(x))

(cf. <URL: http://cs.stackexchange.com/questions/22218/mapping-intuitionistic-logic-to-the-modal-logic-s4 >).

Arnaud Spiwack (2019-04-17T08:57:42Z)

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

Arnaud Spiwack (2019-04-17T05:54:59Z)

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

Ruxor (2019-04-16T19:47:37Z)

@ooten: Si je me rappelle bien,

‣ on peut définir une logique « linéaire intuitionniste » assez facilement (en gros, en asymmétrisant les règles de la logique linéaire de façon à autoriser une seule formule à droite du taquet, et en supprimant le connecteur ⅋ ainsi que le ⊥), qui est un affaiblissement aussi bien de la logique linéaire que de la logique intuitionniste (essentiellement l'« intersection » des deux) ;

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

Je me rends compte en écrivant ça que j'ai oublié d'expliquer que la logique classique pouvait se voir à l'intérieur de la logique intuitionniste par la traduction « double négation ». Je devrais essayer de rajouter quelque chose à ce sujet !

ooten (2019-04-16T19:19:26Z)

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)

Ruxor (2019-04-16T09:47:21Z)

@Arnaud Spiwack:

Il y a des gens (cf. le texte de Diener que j'ai cité, ou le livre « Varieties of constructive mathematics » de Bridges et Richman) qui distinguent, dans ce contexte, quatre grandes théories ou formalismes, même si aucun n'est parfaitement bien défini : « CLASS » (les mathématiques classiques), « INT » (l'intuitionnisme à la Brouwer), « RUSS » (les mathématiques constructives russes à la Markov) et « BISH » (= « CONST »?, les mathématiques constructives à la Bishop, qui sont plus faibles que les trois précédentes). En gros, CLASS inclut le tiers exclu, INT inclut le(s?) axiome(s?) d'éventail de Brouwer (une forme constructive du lemme de König, cf. <URL: https://ncatlab.org/nlab/show/fan+theorem >), RUSS inclut le principe de Markov et la thèse de Church-Turing étendue ; mais toutes ces choses incluent au moins une forme de l'axiome du choix (dépendant ? ou au moins dénombrable). Ce qui est vrai dans tous les topoï est encore plus faible que BISH, parce qu'il n'y a pas l'axiome du choix dénombrable (puisqu'il n'est même pas impliqué par le tiers exclu, comme on le sait bien). 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. Mais en tout cas, même Bishop semble admettre l'axiome du choix dénombrable, ce qui me laisse un peu perplexe si le but est de faire les maths sur les fondements les plus faibles possibles.

Bref, avec cette typologie, l'« intuitionnisme » suggérerait qu'on accepte le(s?) axiome(s?) d'éventail, ce qui est sans doute historiquement exact (Brouwer semblait les accepter), mais pas forcément très pertinent scientifiquement. Au final, tout ça est fort confus.

Pour la dernière question, je ne suis pas très sûr, parce que je ne connais pas du tout les quasitopoï (par ailleurs, je suppose que les « arènes » dont tu parles sont les « assemblies », mais c'est peut-être autre chose). Il y a une construction qui passe du quasitopos des « assemblies » au topos effectif et qui est décrite dans le livre de van Oosten (« Realizability: an Introduction to its Categorical Side »), d'ailleurs dès l'introduction, mais ça consiste surtout à quotienter (i.e., identifier partiellement) les morphismes.

Arnaud Spiwack (2019-04-16T07:07:22Z)

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?


You can post a comment using the following fields:
Name or nick (mandatory):
Web site URL (optional):
Email address (optional, will not appear):
Identifier phrase (optional, see below):
Attempt to remember the values above?
The comment itself (mandatory):

Optional message for moderator (hidden to others):

Spam protection: please enter below the following signs in reverse order: 8faca8


Recent comments