Tu mélanges allégrement cas spécifiques et cas généraux, et je n'arrive plus à être sûr de ce que tu veux dire. Tu as l'air de penser qu'en exhibant des contre-exemples de programmes pouvant être prouvés, tu démontres quelque chose. Depuis le début, je dis que je suis d'accord sur le fait que des cas restreints peuvent être prouvables. Le problème vient quand tu généralises à tous les programmes écrits dans un langage Turing complet.
Nous avons aussi un problème de compréhension au sujet du formalisme utilisé pour la discution. Je parle de machines de Turing, et d'états de machines de Turing, et toi tu me parles d'erreurs d'arrondi et de CPU. Ce n'est pas du tout mon domaine, et j'ajouterais que ça ne m'intéresse pas trop puisque, si on a des problèmes de prouvabilité au niveau des machines de Turing "parfaites", ce n'est pas en ajoutant des possibilités d'erreur au niveau du codage des nombres, ou des problèmes de concurrence, qu'on rendra les choses plus facilement prouvables.
Il ne dit absolument pas que pour un programme quelconque spécifié il est impossible d'écrire un autre programme qui le valide ou l'invalide.
S'il est possible pour un programme quelconque fixé d'écrire mécaniquement un programme qui le valide ou l'invalide, alors il est possible d'écrire un programme qui valide ou invalide tous les programmes.
S'il est possible pour un programme quelconque de trouver un programme qui le valide ou l'invalide, mais qu'on ne peut pas mécaniser ce processus, alors cela revient à dire que c'est algorithmiquement indécidable. C'est donc un objectif inaccessible si la thèse de Church-Turing est vraie, on y revient.
Si on restreint le problème comme tu le fais aux programmes utilisant une mémoire finie, on sort de l'infaisable théorique pour arriver dans l'infaisable pratique, ce qui nous fait une belle jambe. Ca devient faisable théoriquement parce qu'on peut essayer tous les états possibles du programme, mais je serais curieux de voir une méthode générale plus efficace.
il ne s'agit pas de valider le programme pour un seul et unique jeu de données, mais pour un ensemble de données toutes bornées.
Eh bien, soit tu pars d'un jeu de données initial et tu énumères les états en vérifiant qu'on ne revient jamais dans un état déjà visité, soit tu énumères tous les états atteignables et tu vérifies qu'aucun d'eux n'est sur un cycle. Je ne suis pas sûr qu'énumérer les états atteignables soit faisable en général sans énumérer toutes les données initiales possibles, ce qui reviendrait à exécuter le programme pour chaque jeu de données possible.
Formulé plus simplement, ce que je ne vois pas, c'est comment tu prouves qu'un état n'est pas sur un cycle sans partir d'un état initial, avancer jusqu'à cet état, et prouver qu'ensuite on ne revient pas à un état déjà visité. (Par état, je parle d'un état d'une machine de turing associé à ce qui est écrit sur le ruban.)
Typiquement ton programme est un graphe où les noeuds sont des états et les arêtes des transitions. Tu peux faire mieux qu'énumérer tous les états (et donc toutes les données possibles) à condition de pouvoir compacter plusieurs noeuds en un seul, c'est à dire qu'au lieu d'avoir des états de type: (X, d) avec d un jeu de données, tu auras des états de type (X, D) avec D un ensemble de jeux de données.
Ce qui m'intrigue, c'est comment on pourrait faire cette compaction dans le cas général. Je n'ai pas de preuve formelle que ce soit impossible de le faire de manière plus efficace qu'en énumérant tout, mais intuitivement ça me semble évident.
[^] # Re: C'est trop compliqué !
Posté par Yusei (Mastodon) . En réponse au journal Des langages de haut niveau. Évalué à 2.
Nous avons aussi un problème de compréhension au sujet du formalisme utilisé pour la discution. Je parle de machines de Turing, et d'états de machines de Turing, et toi tu me parles d'erreurs d'arrondi et de CPU. Ce n'est pas du tout mon domaine, et j'ajouterais que ça ne m'intéresse pas trop puisque, si on a des problèmes de prouvabilité au niveau des machines de Turing "parfaites", ce n'est pas en ajoutant des possibilités d'erreur au niveau du codage des nombres, ou des problèmes de concurrence, qu'on rendra les choses plus facilement prouvables.
S'il est possible pour un programme quelconque fixé d'écrire mécaniquement un programme qui le valide ou l'invalide, alors il est possible d'écrire un programme qui valide ou invalide tous les programmes.
S'il est possible pour un programme quelconque de trouver un programme qui le valide ou l'invalide, mais qu'on ne peut pas mécaniser ce processus, alors cela revient à dire que c'est algorithmiquement indécidable. C'est donc un objectif inaccessible si la thèse de Church-Turing est vraie, on y revient.
Si on restreint le problème comme tu le fais aux programmes utilisant une mémoire finie, on sort de l'infaisable théorique pour arriver dans l'infaisable pratique, ce qui nous fait une belle jambe. Ca devient faisable théoriquement parce qu'on peut essayer tous les états possibles du programme, mais je serais curieux de voir une méthode générale plus efficace.
Eh bien, soit tu pars d'un jeu de données initial et tu énumères les états en vérifiant qu'on ne revient jamais dans un état déjà visité, soit tu énumères tous les états atteignables et tu vérifies qu'aucun d'eux n'est sur un cycle. Je ne suis pas sûr qu'énumérer les états atteignables soit faisable en général sans énumérer toutes les données initiales possibles, ce qui reviendrait à exécuter le programme pour chaque jeu de données possible.
Formulé plus simplement, ce que je ne vois pas, c'est comment tu prouves qu'un état n'est pas sur un cycle sans partir d'un état initial, avancer jusqu'à cet état, et prouver qu'ensuite on ne revient pas à un état déjà visité. (Par état, je parle d'un état d'une machine de turing associé à ce qui est écrit sur le ruban.)
Typiquement ton programme est un graphe où les noeuds sont des états et les arêtes des transitions. Tu peux faire mieux qu'énumérer tous les états (et donc toutes les données possibles) à condition de pouvoir compacter plusieurs noeuds en un seul, c'est à dire qu'au lieu d'avoir des états de type: (X, d) avec d un jeu de données, tu auras des états de type (X, D) avec D un ensemble de jeux de données.
Ce qui m'intrigue, c'est comment on pourrait faire cette compaction dans le cas général. Je n'ai pas de preuve formelle que ce soit impossible de le faire de manière plus efficace qu'en énumérant tout, mais intuitivement ça me semble évident.