Il y a moyen de faire carrément mieux en ces temps troublés. Le Coq (le symbole de l'équipe de france) aide les castors affairés (à faire les plus beau barrage). En informatique théorique, c'est probablement un oracle. Mais celui de la pythie des élections.
Je viens de passer une demi-journée à apprendre plein de trucs inutiles sur les machines de Turing, le langage Coq et la cuisine hongroise (ben oui, quand on passe de lien en lien…). Merci !
Je suis fasciné par l'énergie qui a été investie dans ce problème, la passion qu'il a déchaînée, et le fait que la résolution fasse la une de Quanta Magazine et le tour des réseaux sociaux (en tous cas tous mes contacts habituels sur Mastodon et Bluesky).
Pourquoi ? Parce que les valeurs exactes de la fonction castor affairé me paraissent parfaitement inintéressantes :D Notamment parce qu'elles dépendent fortement de choix purement techniques sur la forme des machines de Turing, qui n'ont généralement aucune importance parce toutes les variantes des machines de Turing sont interconvertibles, mais qui influencent le nombre exact d'états et donc la fonction castor affairé : le nombre de symboles de l'alphabet (un alphabet binaire est le plus courant, mais on permet généralement des alphabets plus gros, et on s'en sert même parfois vraiment, cf. space speedup theorem en complexité), le nombre de bandes (une seule dans la variante la plus simple, mais parfois deux avec une bande d'entrée/sortie et une bande de travail, et en complexité toujours trois, entrée + travail + sortie, car c'est ce qui permet de mesurer l'espace pris par un algorithme sans compter l'entrée ni la sortie), et aussi la manière de gérer les blancs (est-ce que la machine a le droit de se déplacer à l'intérieur des blancs après l'entrée en les laissant écrits ?), etc., etc.
Cela dit, c'est vrai que formaliser ça en Coq est assez impressionnant.
Je suis fasciné par l'énergie qui a été investie dans ce problème, la passion qu'il a déchaînée, et le fait que la résolution fasse la une de Quanta Magazine (…) Pourquoi ? Parce que les valeurs exactes de la fonction castor affairé me paraissent parfaitement inintéressantes
Why care about determining particular values of the Busy Beaver function? Isn’t this just a recreational programming exercise, analogous to code golf, rather than serious mathematical research?
I like to answer that question with another question: why care about humans landing on the moon, or Mars? Those otherwise somewhat arbitrary goals, you might say, serve as a hard-to-fake gauge of human progress against the vastness of the cosmos. In the same way, the quest to determine the Busy Beaver numbers is one concrete measure of human progress against the vastness of the arithmetical cosmos, a vastness that we learned from Gödel and Turing won’t succumb to any fixed procedure. The Busy Beaver numbers are just … there, Platonically, as surely as 13 was prime long before the first caveman tried to arrange 13 rocks into a nontrivial rectangle and failed. And yet we might never know the sixth of these numbers and only today learned the fifth.
# Prix du titre le plus improbable
Posté par Benoît Sibaud (site web personnel) . Évalué à 8 (+5/-0).
Y a pas de commentaire c'est juste une question de titre.
[^] # Re: Prix du titre le plus improbable
Posté par Thomas Douillard . Évalué à 4 (+2/-1).
Il y a moyen de faire carrément mieux en ces temps troublés. Le Coq (le symbole de l'équipe de france) aide les castors affairés (à faire les plus beau barrage). En informatique théorique, c'est probablement un oracle. Mais celui de la pythie des élections.
# Une demi-journée…
Posté par Serge Julien . Évalué à 5 (+3/-0).
Je viens de passer une demi-journée à apprendre plein de trucs inutiles sur les machines de Turing, le langage Coq et la cuisine hongroise (ben oui, quand on passe de lien en lien…). Merci !
# L'œil amusé d'un théoricien
Posté par jeanas (site web personnel, Mastodon) . Évalué à 5 (+4/-0).
Je suis fasciné par l'énergie qui a été investie dans ce problème, la passion qu'il a déchaînée, et le fait que la résolution fasse la une de Quanta Magazine et le tour des réseaux sociaux (en tous cas tous mes contacts habituels sur Mastodon et Bluesky).
Pourquoi ? Parce que les valeurs exactes de la fonction castor affairé me paraissent parfaitement inintéressantes :D Notamment parce qu'elles dépendent fortement de choix purement techniques sur la forme des machines de Turing, qui n'ont généralement aucune importance parce toutes les variantes des machines de Turing sont interconvertibles, mais qui influencent le nombre exact d'états et donc la fonction castor affairé : le nombre de symboles de l'alphabet (un alphabet binaire est le plus courant, mais on permet généralement des alphabets plus gros, et on s'en sert même parfois vraiment, cf. space speedup theorem en complexité), le nombre de bandes (une seule dans la variante la plus simple, mais parfois deux avec une bande d'entrée/sortie et une bande de travail, et en complexité toujours trois, entrée + travail + sortie, car c'est ce qui permet de mesurer l'espace pris par un algorithme sans compter l'entrée ni la sortie), et aussi la manière de gérer les blancs (est-ce que la machine a le droit de se déplacer à l'intérieur des blancs après l'entrée en les laissant écrits ?), etc., etc.
Cela dit, c'est vrai que formaliser ça en Coq est assez impressionnant.
[^] # Re: L'œil amusé d'un théoricien
Posté par patrick_g (site web personnel) . Évalué à 6 (+4/-1).
A cette interrogation il n'y a pas de meilleure réponse que celle de Scott Aaronson :
Why care about determining particular values of the Busy Beaver function? Isn’t this just a recreational programming exercise, analogous to code golf, rather than serious mathematical research?
I like to answer that question with another question: why care about humans landing on the moon, or Mars? Those otherwise somewhat arbitrary goals, you might say, serve as a hard-to-fake gauge of human progress against the vastness of the cosmos. In the same way, the quest to determine the Busy Beaver numbers is one concrete measure of human progress against the vastness of the arithmetical cosmos, a vastness that we learned from Gödel and Turing won’t succumb to any fixed procedure. The Busy Beaver numbers are just … there, Platonically, as surely as 13 was prime long before the first caveman tried to arrange 13 rocks into a nontrivial rectangle and failed. And yet we might never know the sixth of these numbers and only today learned the fifth.
Envoyer un commentaire
Suivre le flux des commentaires
Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.