Comments on Lorem ipsum strikes back

Et pour être très explicite, l'erreur dans ma « preuve » donnée dans le commentaire daté 2025-06-03T00:07:59+0200 est dans le passage

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

car on obtient seulement une fonction *partielle* 2^ℕ ⇢ 2, et ça ne suffit pas.

J'ai regardé ton sujet d'examen, et je ne suis pas d'accord avec Longley & Normann pour dire qu'il n'y a pas d'auto-référence dans la preuve. Pour moi, elle est juste cachée dans ta question (6) (c), où tu utilises le fait que le problème de l'arrêt n'est pas co-semi-décidable. En éliminant cette coupure et en simplifiant très légèrement, j'obtiens exactement leur seconde preuve.

En effet, la première preuve est la suivante (je prends la version simple qui donne juste la continuité) :

Théorème : Soit F réalisant ℕ^ℕ → ℕ, alors F est continue.

Preuve : Soit g réalisant ℕ^ℕ et considérons le programme

e(d)(ℓ):
Si d termine en n ≤ ℓ étapes :
Chercher c code d'une fonction égale à g jusqu'au rang n et nulle à partir d'un certain rang, telle que F(c) ≠ F(g), et renvoyer c(ℓ)
Sinon, renvoyer g(ℓ)

Si on n'a jamais F(e(d))↓ = F(g) pour un d qui termine, alors on peut co-semi-décider si un programme quelconque d ne termine pas, en regardant si F(e(d))↓ = F(g), absurde. Soit donc d qui termine en un certain nombre d'étapes n et tel que F(e(d))↓ = F(g). Si la recherche effectuée par les appels e(d)(ℓ), ℓ ≥ n trouve un c, alors e(d) est extensionnellement équivalent à c, qui est totale, donc F(e(d))↓ = F(c), contredisant F(e(d))↓ = F(g) et F(c) ≠ F(g). Donc, F prend la valeur F(g) sur toute fonction égale à g jusqu'au rang n et nulle à partir d'un certain rang.

Reste à montrer que c'est vrai sur toute fonction calculable égale à g jusqu'au rang n, pas forcément nulle à partir d'un certain rang, ce qui est vrai car pour toute telle fonction h, on trouve n' qui satisfait la même propriété pour h que n pour g, on peut supposer n' ≥ n sans perte de généralité, et en prenant n'importe quelle fonction s égale à h jusqu'au rang n' (donc aussi égale à g jusqu'au rang n) et nulle à partir d'un certain rang, on a F(g) = F(s) = F(h). ∎

Maintenant, observe que l'impossibilité de co-semi-décider le problème de l'arrêt peut se prouver par diagonalisation directe (sans passer par « il est indécidable et semi-décidable donc pas co-semi-décidable ») : en supposant que l'arrêt est co-semi-décidable, on construit

self:
Rechercher un témoin que self ne termine pas, et si trouvé, terminer

Alors self termine ssi self ne termine pas.

La preuve ci-dessus montre par l'absurde l'existence de d, mais c'est une preuve par l'absurde inutile, car en éliminant la coupure, la construction de self donne un d qui convient. Ceci donne la preuve suivante :

Preuve : Soit g réalisant ℕ^ℕ et considérons le programme

e(d)(ℓ):
Si d termine en n ≤ ℓ étapes :
Chercher c code d'une fonction égale à g jusqu'au rang n et nulle à partir d'un certain rang, telle que F(c) ≠ F(g), et renvoyer c(ℓ)
Sinon, renvoyer g(ℓ)

ainsi que le programme

self:
Lancer F(e(self)), et s'il termine et renvoie F(g), alors terminer (sinon boucler indéfiniment)

Si self ne termine pas, alors e(self) est extensionnellement équivalent à g, donc F(e(self))↓ = F(g), donc self termine, contradiction. Donc self termine, donc F(e(self))↓ = F(g) par définition de self, et on continue la preuve précédente avec d = self. ∎

Et pour finir, comme e n'est jamais utilisée que sur self, on peut incorporer self dans e, ce qui donne :

Preuve : Soit g réalisant ℕ^ℕ et considérons le programme

e(ℓ):
Si F(e) termine et renvoie F(g) en n ≤ ℓ étapes :
Chercher c code d'une fonction égale à g jusqu'au rang n et nulle à partir d'un certain rang, telle que F(c) ≠ F(g), et renvoyer c(ℓ)
Sinon, renvoyer g(ℓ)

On a F(e)↓ = F(g), car sinon e est extensionnellement équivalent à g, donc précisément F(e)↓ = F(g). On continue la preuve avec e cette fois. ∎

Et la formule pas très lisible page 443 de Longley & Normann pour z_ce • i est exactement mon code pour e(ℓ).

Pour les niveaux de sécurité −1, −2, −3, je serais curieux de lire un article sur le sujet. Non pas que je ne connaisse pas le sujet, j'ai déjà fait pas mal de recherches dessus, mais juste pour avoir d'autres opinions.

Par contre, tout ce qui est TPM, Management Engine et Processor Security Platform, c'est autre chose. De mémoire, c'est installé sur la carte mère, dans le chipset, pas dans le processeur. Donc c'est pas des niveaux de sécurité ring quelque chose. D'ailleurs, le processeur peut communiquer avec eux par l'intermédiaire du bus Host Embedded Controller Interface (HECI), qui sert à communiquer avec le chipset pour tout un tas de trucs, dont la gestion de l'alimentation et la gestion thermique.

Et ils fonctionnent dès que le secteur est branché, même ordi éteint, vu qu'ils sont dans ce qui s'appelle le stand by domain. Je suis même pas certain qu'on puisse le désactiver, et même remplacer le BIOS/UEFI par un bios libre ne devrait rien changer.

De manière générale, tout ce qui est trusted computing, c'est quand même quelque chose de sacrément inquiétant quand on regarde de loin. Il faut dire que c'est pas bien documenté, même s'il y a des interfaces standard pour communiquer avec.

Les vrais niveaux ring -1 et -2, ca regroupe des trucs très divers qui n'ont rien à voir et qui sont déjà beaucoup plus acceptables. Par exemple, je n'ai pas de problèmes avec le System Management Mode, très ancien, qui redonne la main au BIOS et qui était autrefois utilisé par le standard APM pour gérer l'alimentation. Ni avec les niveaux -1 pour gérer l'accélération matérielle de la virtualisation (et ca me fait penser que j'ai un textbook à lire sur le sujet que je procrastine).

Petit erratum par rapport à ce que je disais précédemment :

Montrer l'uniforme continuité des fonctions continues sur un compact ne nécessite pas tout le « contenu non-calculatoire » du lemme de König fort, la version faible suffit.

(Le théorème de Bolzano-Weïerstrass séquentiel est un en fait plus fort, dans un certain sens, ceci est décrit dans le bouquin <URL: https://en.wikipedia.org/wiki/Reverse_Mathematics:_Proofs_from_the_Inside_Out>.)

> (Vous avez le droit de donner un avis sur ce qui vous intéresse, je promets de l'ignorer consciencieusement.)

I'd like the post about the usage of english and french language in university education in France.

(Petit complément de remarque naïve)

Après avoir relu ce que tu disais sur ℕ_∞ ici <URL: http://www.madore.org/~david/weblog/d.2024-07-12.2798.constructive-math-2.html#d.2024-07-12.2798.n-infinity> :

Pour moi, une fonction p: ℕ_∞ -> 2 c'est une licorne. Cet objet suppose que l'on sait donner une valeur bien définie à p(∞). Il y a donc à ce niveau déjà un truc incalculable qui est apparu, ce qui explique qu'on puisse faire de la magie sans avoir besoin d'autres trucs magiques comme le lemme de König.

Ce que je trouve pénible dans <URL: https://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/>, c'est que l'essentiel a l'air de se passer dans la "Technical remark" qui parle d'une notion de "intensional modulus of uniform continuity" qui n'est pas définie. Je n'ai pas trouvé le papier qui a l'air d'en parler dans les réf (en allemand).

-- Ci-dessous, une réflexion naïve probablement stupide qui me passe par la tête après avoir lu cet article et ton commentaire ② --

Le fait que find_ii termine est intimement lié au fait que ce "modulus" puisse être considéré comme uniforme, ce qui est un résultat topologique sur l'espace de Cantor qui découle de la compacité. J'imagine que pour prouver l'existence de ce module et son uniformité, on a besoin de quelque chose du même niveau que Bolzano-Weïerstrass séquentiel ? (du même niveau que le lemme de König (fort) en reverse mathematics il me semble)

Ceci étant, cette preuve elle-même est assez indépendante du programme proposé dans l'article, qui suppose juste l'existence de ce module uniforme, non ?

--- Fin de la réflexion naïve ---

Pourquoi diable veux-tu (r)établir l'ostracisme?

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

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.

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

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.

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

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/