<foo> simply produces <foo>in the text).
<URL: http://somewhere.tld/ >,
and it will be automatically made into a link.
(Do not try any other way or it might count as an attempt to spam.)mailto: URI,
e.g. mailto:my.email@somewhere.tld,
if you do not have a genuine Web site).
Ruxor (2025-06-03T18:14:38Z)
Quelques remarques supplémentaires :
Re ① → Le point clé de la différence entre ℕ_∞ et {0,1}^ℕ semblerait être que ℕ_∞ soit compact (selon n'importe quelle définition de « compact ») en maths constructives, alors que {0,1}^ℕ ne l'est pas forcément (l'affirmation que {0,1}^ℕ est compact est formalisée par le « fan theorem » de Brouwer, qui n'est pas valable dans n'importe quel topos, cf. Fourman & Hyland, “Sheaf Models for Analysis”, théorème 4.4). La question deviendrait alors de comprendre ce qui « fait » que ℕ_∞ est compact alors que {0,1}^ℕ ne l'est pas forcément. Sauf que…
…sauf que si on comprend la compacité de {0,1}^ℕ comme le fan theorem de Brouwer, alors ce dernier ne vaut pas dans le topos effectif (van Oosten, “Realizability” théorème 3.2.25). Donc du coup je suis encore plus confusé, et c'est encore plus surprenant que {0,1}^ℕ soit omniscient dans le topos effectif (mais pas en général).
Re ③ → Ce que ça doit dire (où « ça » = KLS + son extension éventuelle au fait que HEO ≅ HRC) sur le topos effectif RT(𝒦₁), c'est qu'il y a un lien entre lui (le topos effectif) et le topos de réalisabilité RT(𝒦₂^{rec}) sur la partie récursive de la seconde algèbre de Kleene. Sauf que…
…sauf que je m'étais persuadé que RT(𝒦₁) et RT(𝒦₂^{rec}) étaient équivalent, et manifestement je suis passé dans un univers parallèle, donc en fait je ne sais rien sur RT(𝒦₂^{rec}). Néanmoins, HEO et HRC doivent plus ou moins correspondre aux assemblées ℕ, ℕ→ℕ, (ℕ→ℕ)→ℕ, ((ℕ→ℕ)→ℕ)→ℕ dans ces deux topos respectivement, donc il doit y avoir un rapport, mais je suis complètement confusé.
Ruxor (2025-06-03T11:01:54Z)
Il y a au moins trois choses qui ne sont pas claires pour moi :
① L'omniscience de ℕ_∞ vaut dans n'importe quel topos (<URL: https://martinescardo.github.io/papers/omniscient-journal-revised.pdf >), celle de l'ensemble de Cantor {0,1}^ℕ vaut (si j'ai bien compris) dans le topos effectif mais pas en général (loc. cit. renvoie à <URL: https://arxiv.org/abs/1407.7046 > mais je ne trouve pas l'énoncé précis dedans en parcourant le texte en diagonale). Pourtant, les constructions algorithmiques dans les deux cas ont l'air de se ressembler énormément. Donc il faudrait comprendre ce qui fait exactement que dans un cas c'est un truc « purement logique » et que dans l'autre il y a un ingrédient de calculabilité, et identifier lequel exactement.
② L'explication de l'omniscience de l'ensemble de Cantor {0,1}^ℕ dans <URL: https://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/ > fait appel de façon apparemment vraiment cruciale à de la récursion (auto-référence, si on veut). Si on l'écrivait pour des fonctions générales récursives, on utiliserait le théorème de récursion de Kleene. Or la preuve que j'ai déroulée du théorème de KLS dans mon problème d'examen (et qui sort essentiellement de ce qu'écrivent Longley et Normann dans “Higher-Order Computability”, §9.2.1, première preuve du théorème 9.2.1) ne fait pas appel à ce théorème (et je n'ai pas l'impression qu'il soit caché dans une astuce quelque part). Je me suis même dit, c'est dommage, c'est un théorème important du cours et je ne l'utilise pas du tout. Mais justement, Longley et Normann donnent une seconde preuve, dont ils disent : « The second proof, due tu Gandy, involves an ingenious use of self-reference that is not present in the first proof. This more subtle approach allows us to strengthen our result slightly: the procedure for computing the modulus will terminate even for certain c that do not realize any F ∈ HEO(2). » Avant ça, ils écrivent aussi : « These proofs are genuinely different, and it is instructive to compare them. » Mais aussi : « The first of our two proofs [celle sans auto-référence, NdRuxor] is probably the easier to grasp, and has close affinities with other proofs in the book. » Donc j'aimerais comprendre le rapport entre les deux preuves, et ce qu'elles nous apprennent au juste, et ce que ça signifie qu'on fasse une preuve avec ou sans auto-référence, et à ce stade c'est hyper obscur pour moi.
③ Il y a plusieurs niveaux dans le théorème de KLS : ⓐ l'existence d'un module de continuité, ⓑ le fait qu'il soit lui-même calculable, ⓒ le fait qu'il le soit (et que, du coup, la fonctionnelle dont on parle) à partir d'un accès « boîte noire » à la fonction ℕ→ℕ, et ⓓ pour mettre tout ça ensemble, qu'on peut algorithmiquement transformer une fonctionnelle (ℕ→ℕ)→ℕ ayant accès à un code de la fonction ℕ→ℕ en une autre qui fait appel à cette dernière sous forme de boîte noire. C'est surtout ⓒ et ⓓ que je trouve complètement magique. (D'ailleurs on m'a fait remarquer sur Bluesky, <URL: https://bsky.app/profile/jrmyd.bsky.social/post/3lgx4npzvuc2k >, que c'est faux si on s'intéresse à la complexité ou à la cryptographie, cf. <URL: https://people.seas.harvard.edu/~salil/research/obfuscate-dec07.pdf >, même si je ne suis pas non plus certain de voir le rapport exact.) Là aussi, je n'ai pas les idées claires sur que ça nous dit de pouvoir calculer les choses sous forme de boîte noire, et si ça dit quelque chose, par exemple, sur le topos effectif.
En plus de ça, le théorème de KLS a une sorte de généralisation aux types supérieurs qui dit que la structure de types « HEO » coïncide avec « HRC » (« HECt » dans le livre de Longley et Normann), cf. <URL: https://homepages.inf.ed.ac.uk/jrl/Research/notions1.pdf > théorème 3.19, mais bizarrement c'est vraiment le type 2 qui est celui où il se passe des choses intéressantes. Là aussi, je ne comprends pas. Enfin, tout ça est rendu encore plus confus par l'existence de yet another structure de types, « EC(HRO) », qui coïncide aussi (théorème 3.20 du survey de Longley, qui est peut-être(?) le théorème 8.2.7 du bouquin de Langley et Normann). J'ai réussi à comprendre toutes les définitions (j'ai déjà tout oublié), mais le sens moral de ces différents trucs m'échappe complètement.
jeanas (2025-06-02T22:07:59Z)
Je précise comment prouver le fait sur les fonctions 2^ℕ → 2 à partir de KLST parce que ça m'a embrouillé :
On construit un algorithme qui prend un programme calculant une fonctionnelle de type 2^ℕ → 2. La première étape est de transformer le code de ce programme en une machine de type 2 grâce à KLST. Par exécuter cette machine sur un mot binaire fini, j'entends l'exécuter avec ce mot comme préfixe de l'oracle, le résultat n'étant pas défini si la machine fait des requêtes à l'oracle en dehors du mot. La deuxième étape est de rechercher en parallèle soit un mot binaire fini sur lequel la machine renvoie 0, soit une longueur n telle que sur tous les mots binaires de longueur n, la machine renvoie 1.
Ce qui m'a embrouillé, c'est que le programme d'entrée calcule une fonction C → 2 où C est non pas 2^ℕ tout entier, mais le sous-ensemble de 2^ℕ formé des mots binaires infinis calculables. Or C n'est pas compact : par exemple, si u ∈ 2^ℕ est non-calculable, en appelant U_n l'ensemble des mots binaires infinis qui diffèrent de u à partir du n-ième bit exactement, les U_n forment un recouvrement infini de 2^ℕ ∖ {u}, qui contient C, par des ouverts disjoints. De fait, on pourrait imaginer a priori un programme qui prend un programme calculant un élément v de 2^ℕ, et renvoie, disons, la parité du premier bit auquel v diffère d'un élément u non-calculable, sachant que ce bit existe bien car v est forcément calculable. On se doute bien qu'il faudrait pour ça être capable de calculer u, ce qui n'est pas possible, mais la version simple de KLST qui donne juste la continuité ne suffit pas à l'exclure. En revanche, en invoquant la transformation en machine de type 2, ça marche parce que ça montre que la fonction continue C → 2 s'étend en une fonction continue 2^ℕ → 2, donc est bien uniformément continue par compacité, et cette continuité uniforme montre que l'algorithme termine.
(Au passage, ce truc signifie précisément que dans le topos effectif, 2^ℕ vérifie le principe limité d'omniscience, dans le même sens que ℕ_∞ dans <URL:http://www.madore.org/~david/weblog/d.2024-07-12.2798.constructive-math-2.html#d.2024-07-12.2798.n-infinity>.)
GHP (2025-06-02T20:09:55Z)
Si vous nous demandiez ce que nous aimons lire de vous, je répondrais pour ma part les récits de vos promenades, excusions, explorations, avec cartes et photographies, en manque depuis pas mal de temps.
Thomas (2025-06-02T17:03:21Z)
La présentation qu'a partagée @jeanas sur le lien topologie / calculabilité est intéressante !
Du coup, je vois le lien avec le théorème de Kreisel-Lacombe-Shoenfield-Tseitin tel que mentionné sur <URL: https://en.wikipedia.org/wiki/Rice%E2%80%93Shapiro_theorem> (avec ton fil bsky c'est moins évident, enfin j'y ai pas réfléchi plus que ça…)
Autre touriste (2025-06-02T02:20:55Z)
Dans un film (très) ultérieur de la même série, on rencontre une héroïne qui attend ses parents comme d'aucuns attendent le messie, et qui s'imagine qu'ils sont forcément porteurs d'un destin infiniment important.
À la fin du film, elle découvre que ses parents étaient des quidams sans importance particulière, que sa lignée ne lui apporte aucun destin, et qu'elle est libre d'aller accomplir ses propres exploits toute seule comme une grande. J'ai beaucoup aimé ce message, qui répare en partie le problème que tu dénonces (mais il n'y a pas de parents adoptifs ici).
…Et, évidemment, deux films plus tard, la série fait marche arrière et "révèle" que ce personnage fait partie de la descendance d'un des personnages principaux.
jeanas (2025-06-01T14:04:31Z)
> Il fut un temps où j'attendais la sortie d'une nouvelle version de tel ou tel logiciel ou de la distrib Linux tout entière, parce que ça apporterait de nouvelles features intéressantes. Maintenant tout ce que je pense quand une nouvelle version sort, c'est « qu'est-ce qu'ils auront encore cassé ? » et me demander quelles emmerdes ça va m'apporter. Y a-t-il encore des progrès ? Est-ce moi qui ai vieilli ou est-ce que tout s'est profondément enshittifié ?
Comme il arrive à tout le monde, à l'approche de la cinquantaine, tu deviens installé dans ton petit confort embourgeoisé, ancré dans tes vieilles habitudes et réfractaire à la disruption par la nouvelle génération parce que c'était mieux âvant. 😛
Sérieusement, je peux citer des tas de choses dans mon environnement de bureau GNOME qui sont mieux qu'il y a cinq ans. À commencer par le fait que ma sœur et mon frère, qui ont tous les deux choisi Linux pour leurs nouveaux ordinateurs respectifs il y a un an environ (sans que je n'essaie spécialement de les persuader, même si j'avais évidemment mon avis), ont pu facilement installer les logiciels dont ils avaient besoin, y compris certains non-libres (comme Zoom), sans appeler le support technique (comprendre : moi), et sans lancer au hasard des commandes « add-apt-repository » trouvées sur StackOverflow qu'ils n'auraient pas comprises pour que je me casse la tête ensuite à comprendre l'état de la machine en repassant derrière pour réparer leurs problèmes. Ceci essentiellement grâce à Flatpak, et accessoirement grâce aux efforts faits pour rendre GNOME Software plus utilisable (même si ça reste atrocement lent chez moi, mais apparemment ça vient de Fedora, ils sont sur Ubuntu). C'est bien pour nous autres geeks d'expliquer aux moldus que les GAFAM ont un pouvoir démesuré sur nos vies et l'utilisent d'ores et déjà à mauvais escient, encore faut-il proposer des alternatives viables qui ne nécessitent pas de les convertir à la religion geek pour qu'ils puissent les utiliser. (Évidemment, tu n'es pas obligé d'apprécier les interfaces rendues moldu-proof, mais s'agissant de GNOME, il rendent au moins clair et explicite que c'est un but du projet.)
Par ailleurs, mes projets de créer une version d'IBus qui améliore la touche Compose, avec des fonctionnalités comme « si l'utilisateur appuye sur Compose et ne fait rien pendant 3 secondes, une boîte de recherche dans les caractères Unicode s'ouvre », dont je suis d'ailleurs sûr que tu en apprécierais au moins certaines, seraient beaucoup moins envisageables sans Wayland, d'après mes souvenirs (dont j'admets qu'ils sont confus, ça fait un moment que je ne m'y suis pas replongé, c'est mis en pause pour le moment).
> Le théorème de Kreisel-Lacombe-Shoenfield continue à me sembler complètement magique et mystérieux (alors même que j'ai regardé sa démonstration en détails pour en faire un problème d'examen de mon cours de logique et fondements de l'informatique). Peut-être que faire un billet de blog dessus m'aiderait à mieux le comprendre.
Je n'ai pas lu ces trucs, mais je donne quand même le pointeur : regarde peut-être ce qu'a écrit Martín Escardó sur ces questions. Par exemple, ce billet sur le blog d'Andrej Bauer : <URL:https://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/>, où il montre qu'il est décidable de savoir si une fonction de type 2^ℕ → ℕ prend la valeur 0. Je veux dire : étant donné un programme qui prend un programme en entrée avec la promesse que ce programme termine sur tout entier en renvoyant un booléen, et sous cette promesse renvoie un booléen qui ne dépend que de la fonction totale ℕ → 2 calculée par le programme d'entrée, on peut décider s'il existe un programme satisfaisant cette promesse et sur lequel notre programme renvoie 0. (C'est d'ailleurs assez curieux parce que d'habitude ça ne fait pas grande différence de considérer des fonctions ℕ → ℕ ou ℕ → 2, mais là, ça marche pour 2^ℕ → ℕ mais pas pour ℕ^ℕ → ℕ, la raison étant essentiellement que l'espace de Cantor 2^ℕ est compact alors que l'espace de Baire ℕ^ℕ ne l'est pas.) Cf. aussi <URL:https://arxiv.org/pdf/0808.0441v2> et <URL:https://martinescardo.github.io/.talks/popl2012/escardo-popl2012.pdf>.
Egan (2025-06-01T04:59:24Z)
Il est parfaitement possible d'utiliser des ordinateurs avec un CPU Intel sans activer IME (Intel Management Engine).
Voir par exemple ce vendeur qui propose des laptops avec un BIOS libre (Coreboot) et un IME désactivé.
https://novacustom.com/fr/pc-portable-coreboot/