Discussion:Problème de l'arrêt

Dernier commentaire : il y a 3 ans par Jlguenego dans le sujet Preuve de Chaitin, et enoncé de ce qui est prouvé
Autres discussions [liste]
  • Admissibilité
  • Neutralité
  • Droit d'auteur
  • Article de qualité
  • Bon article
  • Lumière sur
  • À faire
  • Archives
  • Commons

Ramasse miettes modifier

L'exemple du ramasse-miettes ne me paraît ni percutant, ni adapté. Peut-être serait-on mieux inspiré de commencer par traduire l'article anglophone?
--Gloumouth1 21 août 2006 à 14:33 (CEST)Répondre

Un peu tard pour répondre, mais c'était une bonne question, j'ai peur que la réponse soit oui. Franck Dernoncourt (d) 3 octobre 2009 à 11:09 (CEST)Répondre

Preuve modifier

Cette modificaiton effectuée par une IP a consisté en un remplacement pur et simple du paragraphe Preuve. Y a-t-on gagné ?
--Gloumouth1 26 janvier 2007 à 08:49 (CET)Répondre

Un peu tard pour répondre, mais c'était une bonne question, j'ai peur que la réponse soit non. Proz (d) 3 octobre 2009 à 02:11 (CEST)Répondre

Preuve plus simple modifier

A mon avis il suffit de considerer la fonction TROUBLE qui teste simplement si HALT(TROUBLE()) == 1 et boucle a ce moment la. Pas besoin de concatenation etcaetera...

la preuve ou la preuve plus simple est hors domaine de définition des machines de Turing
Ppignol (d) 11 juin 2009 à 16:05 (CEST)Répondre

Concatenation progch a la place de prog,ch modifier

Je ne crois pas que simplement concatener sans precaution soit correct ! car il y a alors plusieurs manieres d'interpreter un donnée, et HALT ne saura pas quoi faire quoi qu'il arrive. Par exemple s'il lit 101, doit il se prononcer sur le programme 1 avec l'entree 01, ou sur le programme 10 avec l'entree 1 ? Non, il fallait rester avec la virgule separant bien les genres. Certes cela change l'alphabet, mais secondaire...

D'autre part, dans l'article, PROG(ch) est tantôt une chaine de caracteres, tantôt quelque chose qui "s'arrete ou pas"... ce n'est pas tres clair, (surtout qu'on s'en fout de la chaine de sortie)

PS sur la "preuve plus simple": on a besoin de concatener pour definir HALT... pas pour TROUBLE

La preuve est "subtile", la changer trop souvent est genant modifier

Cela fait deux fois que je corrige la preuve, avant moi une personne avait corrigé quelque chose de correct (peut être peu clair) pour le remplacer par quelque chose d'incorrect. Une autre a modifié ensuite pour se debarasser de points techniques plus ou moins esquivés, et cela rend le tout mal defini. J'ai essayé aujourd'hui de combler cela en entrant un peu plus dans les détails (role du caractere ",")... A mon avis, l'article perd beaucoup de ce jeu de yoyo pour la preuve. Il devrait etre plus sage de proposer des modifications ulterieures de cette partie dans la section discussion, pour voir si elles sont adaptées...

La preuve actuelle est débile et il faut en changer modifier

Il fraudais revoir la preuve mais comme je suis interdit de publication par JC BENOIST veuillez prendre une preuve moins débile au regard de la théorie.
Cordialement Ppignol (d) 15 octobre 2009 à 04:51 (CEST)Répondre

Une preuve sourcée, issue d'une source solide, serait la bienvenue dans cet article. Celle actuellement dans l'article est dans l'esprit des démonstrations classiques (on en trouve une autre variante dans en:Halting problem par exemple), mais il en existe de multiples variantes qui plaisent plus ou moins au goût de chacun. Débile ? Je laisse les lecteurs juge à quoi ou à qui s'applique ce qualificatif, en tout cas pas plus "débile" que les preuves que l'on trouve sur les autres Wikipédia ou dans la littérature sur ce sujet. Il se trouve que c'est moi qui ai réverté Ppignol, mais étant donné que tout le monde ici est opposé à la manière d'aborder le problème de l'arrêt de pPignol, comme en témoigne les discussions environnantes, cela aurait pu être beaucoup d'autres intervenants de cet article. D'ailleurs, pour preuve, je laisserais quelqu'un d'autre réverter le prochain ajout non pertinent (et par conséquent non sourcé) de Ppignol à cet article. --Jean-Christophe BENOIST (d) 15 octobre 2009 à 12:11 (CEST)Répondre
La discussion sur ce point prend des proportions hallucinantes (non sans rappeller les grandes heures d'usenet)... Il semblerait (ai-je compris ?) que pPignol s'indigne du fait qu'on utilise dans la preuve une machine de Turing qui fait une boucle infinie. Mais une telle machine existe (au regard de la definition de "machine de Turing"), et c'est tout ce qui est interessant au regard du resultat qui n'a rien, mais rien, à faire des contingences "materielles" de l'informatique pratique. S'en offusquer est du meme tonneau que de s'irriter du fait (par exemple) que deux droites non paralleles dans le plan s'intersectent en un seul point, sous pretexte que des réalisation "materielle" de ces droites auraientt au moins l'epaisseur d'un atome. C'est techniquement probablement vrai, mais ca ne parle pas de la meme chose, et on ne peut pas exiger de réecrire la géométrie Euclidienne en tenant compte de ce fait. Bref, il faut peut etre bien mettre en evidence qu'il s'agit d'un resultat d'informatique "theorique" --et donc en fait de mathématiques :) -- mais il faut s'opposer à la modification de la preuve en profondeur pour des raisons pratiques, materielles, morales, professionnelles, ou que sais-je encore. Jawazele (d) 15 octobre 2009 à 18:27 (CEST)Répondre
Oui, tu as bien compris. Tout cela a déjà été dit à pP, et nul ne peut lui faire entendre raison. Au moins, j'espère que cette réaction supplémentaire lui fera bien sentir que bien d'autres contributeurs peuvent effectivement le réverter, et que son avenir ici est plus que sombre. --Jean-Christophe BENOIST (d) 15 octobre 2009 à 22:00 (CEST)Répondre
Encore une fois vous avez mis les pieds à coté de la plaque ! Je ne m'indigne pas qu'un programme puisse faire une boucle, JE SAIT PERTINEMMENT QUE C'EST POSSIBLE, mais du fait qu'UN PROGRAMME BUGGE EN ASSOCIATION AVEC UN RAMASSE MIETTE qui n'a pas pour but d'optimiser un bug SERVE DE PREUVE. Demandez à un informaticien de vous expliquer ce que je raconte au lieux de chercher à prouver la théorie ! OUI LA THEORIE EST JUSTE ET JE LE SAIT !!!!!!! JE DÉNONCE JUSTE LE FAIT QUE VOUS PRENEZ LE PROBLÈME A L'ENVERS aux vue DU DOMAINE DE DEFINITION DE L'INFORMATIQUE. QUAND VOUS SAUREZ CE QU'EST UN RAMASSE MIETTES VOUS SAUREZ DE QUOI JE PARLE !! J'en ai marre de parler à des matheux qui cherchent à théoriser ce que je raconte en ne comprenant que la moitié du problème.
Encore une fois JE NE M'OPPOSE PAS AU FOND MAIS A LA FORME !!!!!!!
Faites des études en informatiques, en particuliers sur les ramasse miettes, et revenez me voir APRÈS qu'on en discute plus sereinement !
Non J-C B., Il ne m'a pas "réverté" il est à coté de la plaque, et il à rien compris du tout aux différents articles que j'ai rédigés !
Je suis certainement parti du mauvais pied dans l'article "assurance de terminalité" mais vous avez eu la bêtise de relever une erreur bénigne et d'ignorer des éléments capitaux de ma réflexion. C'était une forme de démonstration qui me paraissait, à l'époque, parlante mais dont j'aurais du m'abstenir au regard de la vision physico-théorique que J-C B. a des lois de la physique que l'on nous enseigne à l'école. A vrais dire je me fous des théories physiques comme de ma première ligne de code !
Le fait est que la boucle infinie sort du domaine de définition du ramasse miettes. Et ça c'est une réalité informatique mesurable. Utiliser cette association comme preuve est débile.
Une récursion paramétré parais déjà moins débile, même si c'est pas top ! Par pitié virez ce : "faire une boucle infinie, et ne jamais terminer"Ppignol (d) 23 juin 2010 à 01:52 (CEST)Répondre
Je suis désolé mais tout ceci n'a strictement rien à voir avec les ramasse-miettes, ni d'ailleurs avec les loi de la physique. Le problème de l'arrêt n'a qu'une portée théorique s'appliquant à des objets théoriques que sont les modèles de calcul. Wikipedia est une encyclopédie devant respecter l'idéologie standard et ce que vous proposez ne rentre pas dans ce cadre, voir Wikipédia:Wikipédia est une encyclopédie de plus les théorie exposées doivent déjà exister, voir Wikipédia:Vérifiabilité. Je m'opposerai à des changements qui ne respecte pas ces principes. Outs (d) 24 juin 2010 à 10:09 (CEST)Répondre
1) L'explication au dessus de la preuve est pas très claire.
2) L'analyse statistique actuelle des programmes est capable de dire que le programme boucle indéfiniment à la condition "2." ce qui en gros dit au développeur qu'il est idiot d'avoir mis une boucle infinie dans son programme.
3) C'est vous qui dites qu'aucun programme ne sera capable de décider si le programme "Trouble" s'arrête ou non. Or un compilateur lèvera un warnning parce qu'il y à un while(true) dans le code. Ici je ne remet pas en question le problème de l'indécidabilité mais de la construction plus qu'idiote de votre application pour le démontrer et qui reste détectable par un programme Turing.
4) L'indécidabilité dans le domaine de l'informatique ne signifie pas que l'on ne peux pas déceler des constructions dangereuses comme les while(true) mais que pour un programme donné n'ayant pas de constructions dangereuses il n'est pas toujours possible de déterminer si il s'arrête ou non en un temps fini simplement à la lecture de son code (sans ses paramètres fonctionnels). Ce qui n'est clairement pas le cas de votre preuve.
5) Votre preuve est clairement débile car n'importe quel compilateur Turing(complet ou non) est capable de voir que le programme contient une construction while(true) qui est typiquement une construction problématique. Cela est vérifiable et ne remet nullement en question le problème de l'indécidabilité.
6) Si la manière dont vous avez construit la preuve est la manière standard en mathématique, elle ne correspond à rien en informatique.
Maintenant soit vous acceptez de voir qu'un compilateur d'un langage quelconque est capable de voir une construction type while(true) et qu'il affichera systématiquement un warning voir, pour certains langages, qu'il refusera de compiler le programme et vous changez la construction de la preuve par un exemple de bug moins trivial. Soit vous passez pour des crétins vis à vis des développeurs en informatique et vous persistez à présenter une preuve qui ne correspond pas au sens de l'informatique, et plus largement au sens des machines de Turing, au problème de l'indécidabilité pour les machines de Turing !Ppignol (d) 25 juin 2010 à 00:54 (CEST)Répondre
La preuve contenu dans l'article est standard et correspond à ce qui existe dans la littérature scientifique classique depuis plusieurs dizaines d'années (même si la forme de l'article n'est pas terrible). Si vous contestez ce fait, je vous conseille d'écrire un article exposant votre point de vue et de le faire publier dans un journal reconnu. Sans cela, et en vertu des principes qui s'appliquent sur wikipedia en cas de désaccord (voir les pages données plus haut), vos remarques ne peuvent apparaitre. Si cela peut vous consoler, je suis d'accord que cette preuve n'est pas particulièrement intéressante car l'on voit bien qu'il existe des classes de programmes pour laquelle on peut décider de la terminaison. Mais dans le cas général il n'existe pas un programme universel capable de décider la terminaison d'un programme quelconque. Outs (d) 25 juin 2010 à 08:08 (CEST)Répondre
Laisse tomber. On lui a dit au moins 10 fois ce que tu viens de dire, a peu près dans les mêmes termes. On est en boucle infinie là   --Jean-Christophe BENOIST (d) 25 juin 2010 à 13:55 (CEST)Répondre
Problème de l'indécidabilité en informatique = lire le code du programme dire si il peux planter.
/*programme de recherche d'erreurs */
Lire(char* Programme[])
[
cout << "Lire code du programme : ... Lecture en cour ...";
....
if (lu "while(true)" dans Programme)
{
cout << "\"while(true)\" détecté, le programme plante!";
return ERRNB + WHILE;
}
....
}
run Lire(TROUBLE);
sortie > Lire code du programme : ... Lecture en cour ... "while(true)" détecté, le programme plante!
Ce programme n'a pas la prétention de détecter toutes les erreurs de programmes quelconques (conformément au problème d'indécidabilité) mais il sera suffisent pour exploser toutes les preuves (qui n'en sont pas) basés sur une boucle infinie dans la construction algorithmique et ce, quelque soit la construction de la boucle !
BANDES DE CRÉTINS !!!
La seule façon de contourner le problème et avoir une preuve incassable par programme, est d'utiliser les paramètres de trouble pour flinguer le comportement d'une preuve non buggé et la corrompre. Cela n'est pas difficile à faire quand on sait injecter du code à un programme sauf que vous êtes pas informaticiens et que vous ne comprenez rien à l'algorithmique. Les matheux devraient s'abstenir de toucher aux machines de Turing, ils sont pas formés pour !
Apprenez l'informatique et revenez donner des leçons à des confirmés APRÈS !!!
Cordialement ! Ppignol (d) 26 juin 2010 à 05:35 (CEST)Répondre
PS : J'ai fais un tour sur les sites qui parlent de Gödel. A priori l'incomplétude ne serais valable que si un programme Turing ne pouvais ni dire que le programme s'arrête ni qu'il puisse dire qu'il ne s'arrête pas. Mais comme j'ai prouvé qu'un programme Turing est capable de découvrir que la preuve à le potentiel de ne pas s'arrêter. Votre preuve est au mieux "inconsistante" (au lieu d'"incomplète") et au pire seulement débile ! Donc j'ai bien démontré que la preuve n'est pas une preuve d'incomplétude et ne peut donc pas servir pour le problème de l'arrêt.
Alors maintenant, vous ne voulez toujours pas la changer votre preuve qui n'en est pas une ? Ppignol (d) 27 juin 2010 à 02:40 (CEST)Répondre
PS2:Au fait la preuve standard parle d'un hypothétique ordinateur qui dirais toujours la vérité et auquel on donnerais la phrase :"l'ordinateur ne dira, jamais vrai à cette phrase" ce qui provoque un paradoxe car si il dit toujours la vérité il doit dire vrai or le problème c'est que la phrase l'en empêche. Et si il dit faux il ment donc il ne dit pas la vérité. Rien à voir avec la preuve actuelle qui est basé sur une boucle comportementale.Ppignol (d) 2 août 2010 à 12:44 (CEST)Répondre
Heureusement qu'il y à des informaticiens qui savent faire des maths et qui savent chiffrer correctement leurs travaux (cf : http://www.larecherche.fr/content/recherche/article?id=6771)Ppignol (d) 5 septembre 2010 à 14:27 (CEST)Répondre

Assurance de teminalité. modifier

Je peux garantir qu'un programme quelconque s'arrêtera à coup sûr et j'en fait la démonstration :

Un programme de boucle infinie de code c++ :

   int main (int argc, char* argv[])
   {
       while(true)
       {
       }
   }; 

S'arrêtera surement, certainement et obligatoirement pour au moins l'une des raisons suivante qui ont attrait au contexte d'exécution du programme.

  • panne d'alimentation
  • fermeture de l'application par l'utilisateur,
  • défaillance du système d'exploitation,
  • défaut logique de conception du système électronique sous-jacent,
  • défaillance technique du système électronique sous-jacent,
  • dégradation physique du système électronique sous-jacent,
  • l'univers finira par s'arrêter :
    • soit s'étendre et refroidir complètement ce qui signifie qu'il n'y aura plus d'énergie donc plus d'électricité,
    • soit se contracter, ce qui signifie que toute la matière de l'univers sera concentrée dans le volume d'une bille ce qui signifie qu'aucun processus physique évolué ne pourra être maintenu.

D'après des concepts universellement reconnus par la communauté scientifique :

  • "rien n'est parfait", (sauf peut-être Dieu mais je ne l'ai jamais vu), mais surtout
  • "rien ne se crée, rien ne se perd, mais tout ce transforme." Lavoisier et sa loi de l'entropie.

Évidement seules les sciences de la probabilité (dont je ne suis pas maitre) peut déterminer à quel moment et dans quelles proportions ces événements se produiront.

Mais je peux certifier qu'au moins l'un de ces problèmes arrivera tôt ou tard. Ppignol (d) 1 juin 2009 à 19:27 (CEST)Répondre

Depuis quand une fonction mathématique est-elle concernée par les lois de la physique ? Les cas dont vous parlez ne font que prouver qu'aucun ordinateur ne peut être certifié comme interprétant correctement un programme pendant une durée infinie. Cela ne remet bien évidemment pas en cause le problème de terminaison d'un algorithme. Jamian (d) 10 juin 2009 à 14:39 (CEST)Répondre
Ce que je tentais (sûrement maladroitement) de faire c'est de rappeler que le substrat d'une théorie est lié à la théorie et donc à la science. Enlevez le substrat et la théorie s'évanouit. Enlevez les ordinateurs et il n'y à plus d'informatique. L'article disait qu'un compilateur ou un ramasse-miette n'était pas parfait parce qu'il ne savais pas décider d'un problème qui est hors de son contexte de définition. Le fait est qu'un ramasse-miette est une application dans un domaine de définition. J'entendais par mon intervention mettre en évidence qu'il ne faut pas sortir du domaine de définition si on ne veut pas observer des résultats incohérents. Les applications de machines de Turing que sont les ordinateurs étant définies dans un monde physique réel, je souhaitais rappeler le domaine de définition de l'informatique. Le problème de la boucle n'étant pas définit dans ce monde physique, il ne peut pas l'être dans la théorie. C'est une histoire de poupées russes des domaines de définitions sans doutes mieux expliquées dans le message suivant et dans ma page de discutions personnelle ou j'ai répondu à votre post. Ppignol (d) 11 juin 2009 à 16:23 (CEST)Répondre
Si je puis me permettre, l'informatique date au moins de la comtesse Ada Lovelace qui n'a jamais connu le moindre composant électronique de sa vie. Même le papier original de Turing "On computable numbers, with an application to the Entscheidungsproblem" date de 1936, soir 5 ans avant l'ENIAC (qui a justement été construit pour être... Turing-complet, même si bien évidemment, il ne l'était que dans une certaine mesure).
Sur "Le problème de la boucle n'étant pas définit dans ce monde physique, il ne peut pas l'être dans la théorie", d'une part, je ne vois pas ce qui l'en empêche, d'autre part, il faudra que vous me dites quelle théorie au juste reflète parfaitement le monde réel.
Maintenant, quel passage de cet article est-il concerné par ce que vous dites, et qu'il faudrait améliorer à votre sens ?Jamian (d) 11 juin 2009 à 17:07 (CEST)Répondre
le passage concerné est :
"
TROUBLE(ch)
1. Si "ch" contient une virgule, terminer et renvoyer "0".
Sinon, faire HALT(ch,ch)
2. si HALT(ch,ch)=1, alors faire une boucle infinie, et ne jamais terminer.
Sinon, terminer et renvoyer "0".
"
Le morceau en gras correspond à "while(true);", or en informatique une boucle infinie est un bug et le compilateur/ramasse-miettes/détecteur de fuites n'à pas à optimiser un programme buggé car c'est hors de ses compétences mais surtout de ses attributions. (cf : ma dernière réponse à notre conversation dans ma page de discutions).
Et dans :
"
Citons par exemple le problème du ramasse-miettes : on cherche à libérer des zones mémoires juste après leur dernière utilisation.
Ce problème est équivalent à celui de l'arrêt. La réduction est simple : soit P un programme dont on veut tester l'arrêt ; considérons le programme :
créer une zone mémoire X (jamais utilisée dans P)
exécuter P
écrire dans X.
Clairement, la zone mémoire X sert après sa création si et seulement si P termine. Donc, si on savait déterminer automatiquement au vu de la lecture du programme si on peut libérer X juste après son allocation, on saurait si P termine. Cela est impossible, donc il n'existe aucun algorithme de ramasse-miettes optimalement précis.
"
Même problème : Si P ne retourne pas c'est qu'il contient une boucle infinie donc typiquement la routine P est buggé et un ramasse-miettes n'a pas à optimiser un programme buggé car encore une fois cela ne fais pas partie de ses prérogatives. Donc comme le problème décrit ne fait pas partie des spécifications du ramasse-miettes, le ramasse-miettes est déjà "optimalement précis" car il n'a pas à tenir compte d'un bug.
ce message serais mieux dans la discution suivante
Ppignol (d) 18 juin 2009 à 20:15 (CEST)Répondre
Est-ce plus clair ainsi ?--Ppignol (d) 19 juin 2009 à 00:32 (CEST)Répondre
Soit un automate logiciel(basé sur le Design Pattern "État" du GoF) prenant en entrée une chaine de 0 et de 1 de longueur infinie et 3 états dont un état terminal. Le premier état "Premier" à pour fonction de lire le caractère en cour de la chaine, de déterminer l'état suivant de l'automate à partir du caractère lu et d'avancer au caractère suivant sans le lire. Si le caractère est un '0' on passe l'automate à l'état "Second" sinon(caractère lu = '1') on passe l'automate à l'état "Terminal". Le second état "Second" à la même fonction que l'état "Premier" à ceci près que si le caractère lu est un "1" on passe l'automate à l'état "Premier" sinon(caractère lu = '0') on passe l'automate à l'état "Terminal". Enfin l'état "Terminal" arrête le traitement de l'automate. L'utilisateur peut exécuter une requête d'arrêt pour le traitement de l'automate à n'importe quel moment, seul l'état en cours terminera son exécution et l'automate s'arrêtera.
Dans un tel jeu d'états il n'y à aucun moyens de savoir par simple lecture du code si le traitement s'arrêtera ou non (une succession infinie et monotone de '0' et de '1', soit "0101010101....", rend l'automate inarrêtable). Malgré cela il est possible de détecter que "Premier" appelle "Second" et que "Second" appelle "Premier" ce qui à vocation à générer des boucles comportementales ce que l'on doit signaler au développeur qui tranchera de l'utilité de laisser ou non l'algorithme en l'état.
Cela n'empêche pourtant pas le développeur de mettre en place tout les moyens pour laisser à l'utilisateur le contrôle de sa machine en lui permettant d'arrêter l'automate si il trouve le traitement trop long. C'est ce que j'ai fait en donnant la possibilité à l'utilisateur de quitter l'automate à tout moment si tel était sa volonté. C'est ce que je voulais dire en disant que le développeur à le devoir de mettre une grille devant la fenêtre (ou un filet de protection si vous préférez).
Ppignol (d) 6 juillet 2009 à 11:27 (CEST)Répondre
Je reformule la question :
Qui est contre d'utiliser cette preuve (automate du post précédent) qui est (a mon sens) plus claire et juste au regard des théorèmes d'incomplétudes et des problèmes de domaines de définition que celle fournie dans l'article ? Et si c'est le cas pourquoi ? Ppignol (d) 14 septembre 2009 à 17:49 (CEST)Répondre
Je prend acte que cette version vous convient je vais donc procéder aux modification de la preuve. Ppignol (d) 3 octobre 2009 à 01:35 (CEST)Répondre
L'article n'est pas bien clair, il me semble qu'il manque une idée essentielle qui est le th. d'énumération (il faut pouvoir évaluer les programmes du langage dans le langage, l'article joue sur programme/machine de Turing pour contourner la question), mais je ne suis pas sûr de comprendre où vous voulez en venir. N'êtes vous pas en train de chercher à rendre "réaliste" un programme dont on montre justement qu'il n'existe pas ? Proz (d) 3 octobre 2009 à 01:58 (CEST)Répondre
Non, en fait la définition communément admise pour prouver qu'aucun algorithme ne peut déterminer si un programme se termine ou non en ne faisant que lire son code source est basé sur l'introduction d'un BUG dans le programme à tester(typiquement une boucle infinie). Le problème est que le bug en question est d'une part très facile à détecter pour nos compilateurs actuels et d'autres part, un bug de cette nature n'est pas un cas de travail pour lequel le compilateur/ramasse miettes à été créé et donc par conséquent il incombe aux développeur de corriger ce problème puisque c'est lui qui à les moyens de décisions. Comme je l'ai dit dans ma page de discussion un compilateur/ramasse miettes N'A PAS À OPTIMISER UN BUG, C'EST AU DÉVELOPPEUR À NE PAS EN CRÉÉR !! Ceci dit, rien n'interdit à un programme sans bug logique de rendre un résultat incohérent pour une certaine plage de données d'entrées. Typiquement les automates cellulaires en sont un bon exemple, d'où l'algorithme à tester que j'ai donné ci dessus. Le compilateur/ramasse miette ne verra pas grand choses à redire en lisant le code et pourtant l'automate peut adopter un comportement non rationnel avec une entrée spécifique.
Cependant à propos des bonnes pratique, il est normalement obligatoire (malheureusement pas assez réalisé dans la réalité) pour un bon développeur de mettre des sécurités quand il sait que certains comportements inattendus peuvent se produire de manière à laisser l'utilisateur maître de la machine(et éventuellement, empêcher les indésirables d'en prendre le contrôle). Du coups, se planquer derrière le "ah mais aucun programme n'est fiable à 100%" n'est plus un argument qui tien la route puisque quand le problème survient il y à toujours moyen d'y palier, quitte à réécrire l'application, choses que les industriels exècrent par dessus tout, car en général c'est un aveu de leur incompétence et une perte d'argent immédiate considérable malheureusement moindre que lorsqu'ils pratiquent une maintenance curative de longue durée. Pourtant les américains eux l'on déjà compris depuis le début des années 80(cf. génie logiciel, Cycle en V, Design patterns, modélisation objets(Langages), entités-relations(BDD), etc...). Ppignol (d) 5 octobre 2009 à 04:46 (CEST)Répondre
désolé, mais je maintiens, ce qui est au dessus. Il s'agit de toute façon d'un programme qui n'existe pas. Le problème de l'arrêt est un résultat théorique, il est tout à fait possible de contester son interprétation dans le monde de l'informatique réelle (avec des sources, quand il s'agit d'écrire dans un article de wikipedia). L'article actuel (ça n'était pas le cas il y a 2 ans apparemment) a le tort de tout mélanger, mais je ne vois pas ce qu'améliore votre proposition. Allez voir la version anglaise qui me semble meilleure. L'indécidabilité du problème de l'arrêt peut aussi s'interpéter ainsi : si vous êtes capable de définir une classe de programmes dont vous savez qu'ils terminent,et que vous avez, par ex., un langage ad hoc pour écrire ceux-ci, alors il y a des algorithmes qui terminent et que vous ne pourrez pas programmer (mais il ne dit rien sur "l'intérêt" des algo. en question). Par ailleurs les boucles infinies sont très utiles dans le monde de l'informatique réelle, il me semble, mais c'est hors sujet. Proz (d) 5 octobre 2009 à 20:44 (CEST)Répondre
Désolé mais je maintient que les programmes RÉELS et PRATIQUEMENT APPLIQUÉS que sont les COMPILATEURS/RAMASSE MIETTES/DÉTECTEURS DE FUITES N'ONT PAS DANS LEURS CAS D'UTILISATIONS LA SPÉCIFIACTION DE DEVOIR OPTIMISER UN "BUG" ce qui rend un exemple buggé pour preuve, complètement DÉBILE. Si vous aviez lu le 2ème débat que j'ai eu sur ma page de discutions jusque au bout vous l'auriez compris. Après que le problème théorique existe je ne le contredit pas et même je le prouve grâce à l'algorithme décrit au dessus mais avec l'avantage que cette version de la preuve N'EST PAS BUGGÉE !. Ensuite, je prouve aussi que lorsque l'on est dans un cas pratique du problème de l'arrêt il y à TOUJOURS un moyen de mettre un filet de protection affin de laisser le contrôle de la machine à son utilisateur. C'est un devoir pour les développeurs et ceux qui vous dirons le contraire sont soit de mauvaise fois, soit incompétents. Pour faire une analogie, lors d'un accident de la route, la responsabilité incombe à la voiture (logiciel) ou au conducteur (développeur) ? Alors arrêtons de se gargariser d'un problème théorique surtout quand on le prend à l'envers de sa véritable signification.Ppignol (d) 10 octobre 2009 à 13:59 (CEST)Répondre
Désolé d'être trop con pour savoir lire : Théorème de Rice, Impact pratique et merci d'avoir balancé un travail de 4h que j'avais même pas terminé. A part ca c'est moi qui suis sectaire, qui veux rien comprendre et qui fait du travail sans sources ! Je vous aide c'est dans la première phrase du chapitre que j'ai lié ! Ppignol (d) 11 octobre 2009 à 05:35 (CEST)Répondre
cf:L'une des principales approches a été imaginée dans les années 1960 par le Britannique Tony Hoare (en médaillon), l'Américain Robert Floyd et le Danois Peter Naur. Leurs travaux ont été depuis prolongés et unifiés, entre autres, par le Français Jean-Raymond Abrial. L'idée est qu'un programme n'est correct que par rapport à une expression de ce qu'il doit faire, c'est-à-dire par rapport à une spécification..... http://www.larecherche.fr/content/recherche/article?id=6771. C'est ce que je me tue à vous dire depuis le début. Ppignol (d) 5 septembre 2010 à 14:42 (CEST)Répondre

Applications du problème du ramasse miète modifier

En informatique et depuis la création de l'organe de contrôle des interruptions qu'est l'APIC un programme ou une routine qui ne se termine pas est inutile et par conséquent est typiquement un bug ou une erreur de développement. Donc si un programme boucle infiniment alors il faut en informer le développeur qui doit changer le traitement.

De fait je ne comprend pas le problème de l'arrêt car un programme qui ne s'arrête pas est ni plus ni moins qu'un bug.

De fait je ne comprend pas l'intérêt pour un ramasse miette de garder une variable en mémoire qui n'est jamais utilisé par le traitement unique qui suit sa déclaration dans sa portée.

Cela revient à dire "On en aura jamais besoin mais on la garde on ne sait jamais...".

De même l'exemple du problème énoncé n'a pas de raisons d'être puisque pour qu'une sous routine soit utile elle doit terminer.

Cela revient à dire "On en aura surement besoins mais pour des raisons d'optimisation on la supprime..."

Personnellement je ne vois pas l'intérêt de ces débats !

Ppignol (d) 2 juin 2009 à 10:36 (CEST)Répondre

Ces problèmes sont des problèmes d'informatique théorique et de mathématiques, pas des problèmes d'informatique concrète et réelle. Toute allusion au matériel, aux interruption etc.. est hors de propos, et montre effectivement que vous ne comprenez ni ne maitrisez ces problèmes. J'attire de nouveau votre attention que le PdD des articles doivent servir à discuter de l'article et de ses améliorations, ce qui n'est pas le cas de vos deux interventions. Si vous voulez discuter de ces problèmes, il vous faut aller sur des forums sur Internet, mais pas ici. --Jean-Christophe BENOIST (d) 2 juin 2009 à 13:18 (CEST)Répondre
cher Jean-Christophe le fait est que l'informatique théorique est un concept étendu basé sur des concepts physiques. Détruisez ces concepts physiques et l'informatique théorique n'a plus lieux d'être. Par conséquent c'est comme si l'on voulais faire des mathématiques sans vouloir accepter que les chiffres ou les variables existent. donc le matériel est bel et bien à prendre en compte. L'informatique (théorique ou non) est un outil que l'homme à créé pour l'homme, de même que les mathématiques affin qu'elles lui soient utiles. Enlevez l'utilité et l'informatique (ou les mathématiques) ne servent à rien. Un outil qui ne sert à rien n'a pas lieux d'exister. En ingénierie on dit souvent que s'il n'y à pas de solutions c'est qu'il n'y à pas de problèmes donc comme l'on ne peux pas optimiser le traitement des compilateurs c'est qu'il n'y a pas lieu de le faire. Peut-être faudrait-il mieux se concentrer sur des problèmes qui ont des solutions. Au fait j'ai entendu parler de l'incomplétude de goedelle(désolé pour l'orthographe) et de la dualité ondes particule et comme l'informatique est issue des mathématiques et de la physique il ne faut pas s'étonner d'y retrouver les mêmes travers. Ne pas oublier de garder les pieds sur terre. L'informatique n'est qu'un outil et rien de plus. Elle doit servir l'homme pour être utile et non le rendre esclave de ses questions existentielles. Tant que l'on se pose des questions on agit pas. :) Ppignol (d) 5 juin 2009 à 12:55 (CEST)Répondre
L'informatique théorique est une science, elle n'a pas vocation à être utile mais a apporter une connaissance. Ici en l'occurrence cette connaissance s'applique sur des êtres abstraits. De toute manière je rappelle que les pages de discussion de wikipedia sont la pour discuter de l'article et comment l'améliorer et non pas du sujet. Outs (d) 5 juin 2009 à 13:35 (CEST)Répondre
oui c'est une science au service de l'homme (comme toutes sciences d'ailleurs). Enlevez son substrat qui lui permet d'exister et elle disparait. La phrénologie n'existait que parce que les spécimens qui en fondais les bases corrélais la théorie. A partir du moment ou les spécimens élargis infirmais la théorie (le substrat n'existe plus) la théorie (et donc la science associée) n'existe plus ! Il est inutile (et la plupart du temps gênant) d'avoir une boucle infinie. Il n'y à donc pas lieu de s'en soucier (à part pour en avertir le développeur) et la théorie doit l'intégrer. Un compilateur ou un ramasse-miettes (et son optimisation) sont des outils bien concrets (quoique virtuels), par conséquent ils sont théoriquement (autant que pratiquement d'ailleurs) liés au matériel et aux besoins des utilisateurs qui forment leurs contexte d'existence(leurs cas d'utilisations ou "uses cases"). De fait la meilleure optimisation du code que vous avancez, pour un compilateur, est de signaler le bug (la boucle sans fin) à l'utilisateur et, pour le ramasse-miettes, de supposer que la variable est utilisée dans tous les cas, sinon l'utilité et donc l'existence du programme est remise en question. Un programme inutile ne sert à rien et n'a pas lieux d'exister et donc ne sera pas compilé (en tous cas pas intentionnellement), dans ce cas le compilateur n'a pas besoins de l'optimiser et du coups le problème qui empêche l'optimisation complète des compilateurs n'en est pas un. De fait les compilateurs et ramasse-miettes sont pleinement optimisés tels qu'ils sont actuellement. D'où mon incompréhension de se casser la tête sur un problème qui n'en est pas un puisqu'il est en dehors du domaine d'application de l'outil visé. Ou alors trouvez un exemple dans le champs d'application. Mon intervention vise à améliorer l'article puisque je démontre que l'exemple cité est un contre-exemple.
PS : Cela fais 21 ans sur les 28 de ma vie que je développe sur des ordinateurs. Je connais plus d'une dizaines de langages et frameworks, de l'assembleur au Java, en passant par (entre autre) le C, le C++, le pascal, le logo, le C# et les langages de script comme, entre autre, le HTML et le PHP. Je connais la plupart des méthodes d'analyses et de conception : retroengineering, analyse fonctionnelle, merise, UML, et autres Design patterns (que se soit GoF ou GRASP). Je n'ai aucun mérite pour cela, j'ai une licence en informatique industrielle depuis 3 ans et un BTS en informatique de gestion. Mais avant d'affirmer que je ne comprend pas quelque chose assurez vous de savoir si c'est réellement le cas.Ppignol (d) 5 juin 2009 à 23:52 (CEST)Répondre
Ce n'est pas moi qui ai affirmé quelque chose sur vous/toi. Le problème de l'arrêt est une notion classique en calculabilité, il faut donc que wikipedia en fasse l'echo. Que propose tu exactement pour l'article ?Outs (d) 6 juin 2009 à 16:44 (CEST)Répondre
Oui bon je vois pas le rapport je sait reconnaitre une signature... . Pour moi le problème de l'arrêt est certes existant sur des programmes de démonstration inutiles sinon pour montrer ce qu'il ne faut pas faire. En somme cela revient à calculer F(x) = x/(x - 1) pour x = 1, tout le monde sait que c'est l'ensemble vide(l'infini n'étant pas accessible). C'est peut être gênant en mathématiques mais comme en informatique le cas ne se présentera jamais pour la productions de logiciels ce n'est donc pas un problème. Un programme ou une sous routine doit s'arrêter, c'est à cette seule condition que le programme ou la sous routine existe et représente un cas d'utilisation du compilateur ou du ramasse-miettes. La vrai question serait de savoir quand le programme s'arrête mais là je passe la main aux statisticiens probabilistes car ce n'est pas mon domaine de travail. En effet il est difficile de prévoir quand un système vas être arrêté par l'utilisateur, quand un traitement vas être exécuté ou quand l'utilisateur aura terminé une saisie, etc... . Pour moi ce problème de l'arrêt tel qu'il est énoncé n'en est pas un car il est hors domaine de définition donc inutile. Les seuls cas ou un programme peut ne pas terminer tout en restant légal est le cas d'absence de saisie ou de saisie identique.
ex1: Un programme attend la saisie utilisateur pour terminer (et effectue éventuellement un traitement en attendant) une saisie qui n'arrive jamais.
ex2: Un logiciel demande de continuer (oui/non) et l'utilisateur saisi toujours "oui".
ex2bis: Un programme reçoit des données à traiter et renvoie de nouvelles données qu'il doit traiter à nouveau mais il fraudais trouver un cas utile concret (c'est un bug logique de l'ordre de l'interblocage), à voir peut être les automates cellulaires mais l'utilisateur met fin au processus après un certain nombre de générations affin d'en récupérer le résultat ou pour effectuer d'autres taches.Ppignol (d) 7 juin 2009 à 13:34 (CEST)Répondre
Je vien de trouver deux références qui corroborent mes affirmations :
Ppignol (d) 10 juin 2009 à 13:26 (CEST).Répondre
Le ramasse miette apparait comme bien anecdotique, et peu eclairant... Il faudrait le remplacer, par exemple par l'existence d'un ensemble d'entiers recursivement enumerable mais non recursif, premier (tout petit) pas vers la non-resolubilité des equations polynomiales (théorème de Matyasevich) ? Ca aurait l'avantage de ne plus faire d'interference entre "algorithmique" et "programmation"... Jawazele (d) 16 septembre 2009 à 17:15 (CEST)Répondre
Je le trouve pourtant parfaitement intéressant il permet de prouver que lorsque l'on donne un programme non buggé (donc dans le domaine de définition du ramasse miette) on arrive encore à prouver que l'on ne peux pas certifier que le programme s'arrette en fonction de son seul code !
Désolé il n'est pas dans le domaine de définition du ramasse miette de ramasser les miettes d'un bug ! Retournez à vos classes d'algorithmique première année. La première chose que l'on apprend en informatique c'est que si un programme plante (cf bug de la boucle infinie) il est de la responsabilité du développeur de l'éliminer. Le programme n'est pas suffisamment intelligent pour savoir pourquoi vous avez laissé la boucle donc il l'exécute. Par contre un programme peux signaler la boucle au développeur pour qu'il prenne la décision (ou non) de la laisser.Ppignol (d) 5 septembre 2010 à 12:11 (CEST)Répondre
cf:"L'une des principales approches a été imaginée dans les années 1960 par le Britannique Tony Hoare (en médaillon), l'Américain Robert Floyd et le Danois Peter Naur. Leurs travaux ont été depuis prolongés et unifiés, entre autres, par le Français Jean-Raymond Abrial. L'idée est qu'un programme n'est correct que par rapport à une expression de ce qu'il doit faire, c'est-à-dire par rapport à une spécification....." http://www.larecherche.fr/content/recherche/article?id=6771. C'est ce que je me tue à vous dire depuis le début.Ppignol (d) 5 septembre 2010 à 14:45 (CEST)Répondre

Besoin d'explications modifier

Sur le passage suivant :

Une autre application aisée est une forme faible du théorème d'incomplétude de Gödel sur l'existence d'énoncés vrais mais non démontrables. En effet, l'énumération de preuves mathématiques peut se faire algorithmiquement. L'impossibilité de décider l'arrêt permet donc de dire qu'il existe une machine de Turing T et une entrée e telles que T ne s'arrête pas sur e, mais aussi telles qu'il n'existe pas de preuve de ce fait. L'énoncé "T ne s'arrête pas sur e" (pour cette machine et cette entrée dont on n'a que l'existence ; on ne les connait pas) est bien un énoncé vrai mais non démontrable.

Est-ce que quelqu'un pourrait détailler le passage mais aussi telles qu'il n'existe pas de preuve de ce fait. ? Merci. Zandr4[Kupopo ?] 25 avril 2010 à 17:15 (CEST)Répondre

La raison est que l'enumeration de toutes les preuves peut se faire de maniere algorithimique; donc si, pour toute paire (T,e) telle que T ne s'arrete pas sur e, il existait une preuve que T ne s'arrete pas sur e, on la decouvrirait avec un algorithme, et donc on pourrait decider algorithmiquement si T s'arrete ou pas sur e... Doit on rajoutrer un pasage de ce genre dans l'article ? j'y reflechis.--Jawazele (d) 27 avril 2010 à 12:01 (CEST)Répondre
Merci je crois que c'est plus clair. et donc on pourrait decider algorithmiquement si T s'arrete ou pas sur e... En utilisant deux algorithmes en parallèle, c'est bien ça ? Zandr4[Kupopo ?] 27 avril 2010 à 12:34 (CEST)Répondre
Oui c'est ca. J'ai réécrit ce passage dans l'article... Je crois que ca en vallait le coup, car c'est toujours un truc qui surprend...--Jawazele (d) 27 avril 2010 à 12:43 (CEST)Répondre
Ok. C'est mieux ainsi je crois, ce n'était pas tout à fait évident, surtout lorsque l'on n'a pas l'habitude de ce genre de raisonnement... Zandr4[Kupopo ?] 27 avril 2010 à 13:07 (CEST)Répondre

La preuve actuelle manque de rigueur modifier

Sans être aussi critique que les intervenants précédents, il me semble que la preuve présentée dans cet article manque de rigueur, il serait utile de préciser quelques points:

1) Il me semble évident que les chaînes notés ch dans cet article doivent être de longueur finie. Je ne pense pas que le théorème de l'indécidabilité s'applique à des programmes de longueur infinie.

2) Le programme TROUBLE est un programme qui appelle le programme HALT avec lui-même (TROUBLE) en argument dans l'utilisation qui en est faite ici, puisqu'on s'intéresse à TROUBLE(trouble).

3) Puisque le programme TROUBLE appelle le programme HALT, la chaîne trouble le décrivant doit également contenir la description du programme HALT, car sinon une analyse complète ne serait pas possible (pour faire une comparaison, un compilateur afficherait l'erreur "unresolved external").

4) HALT est un programme qui contient, d'une façon ou d'une autre, l'analyse de la chaîne en argument (ici trouble) pour savoir s'il se finit ou pas.

Donc, pour résumer, TROUBLE est un programme qui contient l'analyse d'un programme qui contient l'analyse d'un programme qui contient l'analyse d'un programme... (et comme ça à l'infini) de lui même. la chaîne trouble n'est donc pas de longueur finie.

Une preuve plus rigoureuse serait la bienvenue ici pour la qualité de cet article. (62.147.144.59)

Votre analyse manque de rigueur.. Le fait que HALT soit de longueur finie fait partie des prémisses de la démonstration. Si on aboutit à la conclusion inverse, cela va tout à fait dans le sens de la démonstration qui vise à aboutir à une absurdité. De plus, votre raisonnement n'est pas correct et ce n'est pas parce-que "un programme contient l'analyse d'un programme qui contient l'analyse d'un programme... (et comme ça à l'infini) " qu'il est nécessairement de longueur infinie. Mais, HALT de longueur infinie ou non, la démonstration n'est pas remise en cause.
Cela dit, les prémisses pourraient être mieux exprimés effectivement. De manière générale, il faudrait la SOURCER, afin qu'elle ne soit pas remise en cause constamment. --Jean-Christophe BENOIST (d) 13 juin 2010 à 21:12 (CEST)Répondre
Bonjour, c'est encore moi (j'ai une IP fixe, vous me reconnaitrez facilement).
Bravo pour la réécriture complète de cet article. Je sais que c'est du travail, je sais également que vous le faites bénévolement.
Malheureusement, on a maintenant deux preuves pour le prix d'une, signe que leur valeur est en baisse ! Et effectivement, ces deux preuves sont aussi peu convaincantes que celle qui était avant. Je m'explique:
Je vais commencer par la plus facile, la seconde, celle que vous avez appelé "Preuve de Gregory Chaitain": celle-ci considère naïvement qu'il y a "des programmes qui s'arrêtent" et des programmes qui ne s'arrêteraient pas... indépendamment des paramètres d'entrée. C'est évidemment idiot. Un même programme peut boucler indéfiniment pour une entrée et pas pour une autre (voir plus haut le programme DIAGONALE, par exemple). Je pense que pour discuter intelligeament de ce problème, il faut bien distinguer programme et données, comme le fait d'ailleurs la première preuve au travers de la notation PROG(donnee) (et ce point là est une bonne chose).
Pour ce qui est de la première preuve, on tombe dans le même travers que la preuve qui était là auparavant: la chaîne en entrée est, de façon subtile, de longueur infinie, et on est donc en dehors du domaine d'applicabilité des machines de Turing:
- La chaîne diagonale décrit le programme DIAGONALE.
- Le programme DIAGONALE utilise le programme HALT.
- Donc la chaîne diagonale doit contenir la description du programme HALT, ainsi que les données appliquées à ce programme HALT(ch,ch).
- Or, qu'est-ce que ch dans notre exemple ? c'est la chaîne diagonale.
En conclusion, la chaîne diagonale contient strictement la chaîne diagonale. Ce qui veut dire qu'elle est de longueur infinie.
Pour répondre aux critiques ci-dessus:
Si on aboutit à la conclusion inverse, cela va tout à fait dans le sens de la démonstration qui vise à aboutir à une absurdité.: Non, ce n'est pas une conclusion, c'est une donnée d'entrée que l'on définit au départ. Si les données d'entrées ne sont pas conformes aux prémisses, la conclusion ne peut être qu'absurde (quelles que soient les autres hypothèses). C'est le danger des démonstrations par l'absurde, il faut bien prendre soin de ne prendre pour hypothèse que la donnée dont on veut prouver la fausseté.
Ce n'est pas parce-que "un programme contient l'analyse d'un programme qui contient l'analyse d'un programme... (et comme ça à l'infini) " qu'il est nécessairement de longueur infinie.: Vous inversez l'exigeance de preuve, et vous le savez comme moi: ce n'est pas à moi de prouver que cette chaîne est infinie, mais le seul fait qu'elle puisse l'être invalide la démonstration. Pour qu'elle soit rigoureuse, cette démonstration devrait PROUVER que la chaîne ch est de longueur finie (et à mon avis elle ne le peut pas).
En fait, je ne suis pas arrivé sur cette page par hasard: je suis convaincu depuis des années que cette démonstration est fausse. Je suis conforté dans cette certitude par le fait qu'il y a une multitude de preuves (j'en connais presque dix), et que TOUTES comportent une faille plus ou moins subtile. Paradoxalement, cette multitude de preuves, même fausses, agit contre l'établissement de la vérité: en effet, à chaque fois que je prouve que l'une est fausse, on me répond généralement "oui, effectivement, cette preuve est discutable mais il y a plein d'autres preuves, la démonstration n'est pas remis en cause". Réaction qui tient plus de la dissonnance cognitive que d'un esprit scientifique rigoureux.
Et je ne suis pas le seul a avoir de sérieux doutes sur cette pseudo-preuve. Comme dit plus haut "afin qu'elle ne soit pas remise en cause constamment", c'est donc qu'elle est souvent remise en doute par d'autres que moi. Et si vous regardez les discussions de l'article anglais, vous verrez que les critiques ne manquent pas non plus.
Je pense que l'honnêteté et l'exigeance d'impartialité de Wikipedia, que j'apprécie et que je tiens à préserver, devraient faire mention de ce fait. On pourrait par exemple ajouter un paragraphe disant que cette preuve est controversée, avec les liens permettant au lecteur de se faire sa propre opinion. (62.147.144.59)
Quels liens ? Vous n'avez jamais donné aucun lien, aucune référence, jusqu'ici : c'est tout le temps : moi Je, moi Je. Je suis intelligent, Chaitin et Turing sont des naïfs et des idiots. Pour rappel à Mr l'Intelligent : les paramètres, dans les machines de Turing, sont codés DANS les machines de Turing. Comme un batch sans paramètre, qui appelle un programme avec ses paramètres. Si on veut d'autres paramètres, on crée un AUTRE programme qui inclut ces paramètres. C'est ainsi que sont conçues les choses dans la preuve de Chaitin le Naïf. C'est la dernière fois que je perd de temps à vous répondre : arrêtez vos Pignolades, vos provocations et vos insultes. Si vous voulez remettre en cause ces preuves, écrivez un livre, faites le reconnaitre par la communauté scientifique, et nous citerons vos propos dans l'article, c'est promis. Non seulement Wikipédia n'est pas le lieu où on remet en cause les choses étables, mais encore vous le faites de manière absolument insupportable, avec une ignorance qui n'a d'égale que votre arrogance. Vous n'êtes pas à votre place ici, pour ces deux raisons. POINT FINAL en ce qui me concerne. --Jean-Christophe BENOIST (d) 3 juillet 2010 à 10:31 (CEST)Répondre
Mon chèr JCB vous êtes une sombre dodécabuse. D'abord ce n'est pas moi qui ai posté ces texte, d'ailleurs même si cette personne m'est sympathique par le fait qu'elle recherche le sens de mes propos, elle ne les comprends qu'a moitié ! Ensuite arrêtez vos élucubrations mégalomane Benoistesque parce que même si vous êtes bon en algèbre, en matière d'informatique(ou plus exactement d'algorithmique) vous ne valez pas un centime de franc léger. Je vous rappelle qu'une machine de Turing est un processeur soit un automate à états, tels qu'on peut en écrire à partir du design pattern state du gof. En fonction du programme (ou paramètres pour un automate à états) qu'on lui donne soit il(le processeur ou l'automate) s'arrête en temps fini soit il continu indéfiniment. Comme le prévois le théorème de Gôdel on ne peux pas dire, avec un système qui agirait au sein de ce processeur, si il s'arrêtera ou non en temps finis, sans son programme, ou même avec son programme qui peux lui même avoir des paramètres extérieurs (entré clavier, fichiers, flux binaire, autre programmes, etc...). Le problème ne viens donc pas de la structure du programme (bien quelle puisse influencer le résultat) mais de la structure de la machine de Turing qui permet un comportement aberrant(et pas nécessairement une boucle, cf: cherchez sur wikipédia : Interblocage, Fuite de mémoire, et tout ce qui concerne les automates cellulaires et notamment les boucles de Byl et de Langton) en cumulant des causes dangereuses. Causes que, nous développeur, passons notre temps à apprendre, à rationaliser et surtout à éviter. Le fait est que la preuve que vous considérez juste est incomplète puisque le théorème d'incomplétude de Gödel est bien plus profond que cela et met toutes les aberrations en exergues alors que la votre ne met que la cause la plus simple la boucle logicielle. Enfin, je rejoint 62.147.144.59 sur le fait que le problème de l'arrêt dépasse complètement les programmes que sont les ramasses miettes et ne concernent que les développeurs de ces programmes. En effet comme le dit Gödel, aucun système mathématique permettant de faire de l'algorithmique n'est capable de prouver que le système est cohérent, donc par extension, aucune machine de turing(et c'est bien la machine de Turing le sujet de l'expérience) n'est capable de démontrer par un quelconque programme que la machine de Turing est cohérente. De fait, il est idiot de parler de ramasse miette car c'est la machine de Turing qui est responsable de l'indécidabilité du programme et non l'inverse. Contrairement à 62.147.144.59 je signe mes message (la plus part du temps) et je n'ai pas peur de ce que je pense car je sait que c'est correct même si je ne sait pas bien l'expliquer aux gents qui comme vous ont la faculté de chiffrer leurs langage avec des outils que la majeure partie des gents ne maitrisent pas complètement. Ppignol (d) 5 septembre 2010 à 14:01 (CEST)Répondre
Heureusement qu'il y à des informaticiens qui savent faire des maths et qui savent chiffrer correctement leurs travaux (cf : https://www.larecherche.fr/v%C3%A9rifier-des-programmes-en-prouvant-des-th%C3%A9or%C3%A8mes)Ppignol (d) 5 septembre 2010 à 14:29 (CEST)Répondre

Preuve de Chaitin, et enoncé de ce qui est prouvé modifier

Bonjour, merci aux contributeurs pour la preuve de Chaitin qui est un eclairage original et interessant. Cependant, il semble qu'elle ne prouve pas exactement la meme chose. Il me semble que l'enoncé prouvé est : il n'existe pas d'algorithme qui decide si une machine de Turinng donnée s'arrete ou pas sur l'entrée 'vide' (et pas sur une entrée arbitraire donnée). C'est une variante, interessante, non-triviale, peut etre meme plus naturelle pour commencer, que l'enoncé classique de Turing. Si les contributeurs sont d'accord avec cette nuance, je pense qu'on doit la mentionner dans l'article.

Par ailleurs, il serait peut etre opportun de dire que c'est une esquisse de preuve: en effet, on doit montrer l'existencde de PARADOXE : c'est une machine qui effectue quelque chose, mais qui comporte une contrainte sur sa taille. Il n'est pas clair qu'elle existe a priori. Par exemple, si on remplace le facteur 10 par 1,0000001 (ou pire, par une constante additive 2), je ne suis pas certain qu'une telle machine existe... Il y a ici quelque chose à montrer, c'est ce qu_e fait Chaitin, et le detail n'a pas sa place ici, mais on doit signaler qu'il y a un argument technique ici.--Jawazele (d) 16 septembre 2010 à 10:18 (CEST)Répondre

Remarques pertinentes. Sur le premier point (prouve exactement la même chose ou non), il n'y a pas de problème (mais effectivement on peut se poser la question) : d'une part G. Chaitin expose sa preuve (qui est d'ailleurs reprise par Calude dans d'autres sources) comme étant une preuve équivalente à celle de Turing. Il peut se tromper, mais ce serait très étonnant et il faudrait une source qui dise qu'il y a une erreur. D'autre part, il faut réaliser que la preuve de Chaitin utilise implicitement la notion d'une machine de Turing universelle. Une MTU prends en input le codage d'une machine de Turing, mais aussi l'input de la machine de Turing. Typiquement l'input d'une MTU peut se noter   (ref. Li/Vitanyi, paragraphe 1.7.4), avec un 1 répété i fois qui désigne la ième machine de Turing dans un classement Gödelien des machines de Turing, un 0 délimiteur, et une chaine de bits "p" qui est l'input de la machine de Turing. Donc l'entrée n'est pas "vide" mais "p", et les "programmes" dont il est question dans la preuve désignent implicitement un programme et tous ses paramètres, et non des programmes à entrée vide.
Sur le second point, la remarque est pertinente. Ni Chaitin ni Calude ne s'étendent sur ce point. Je me suis aussi interrogé sur l'origine du facteur 10 (en fait facteur 100 dans le texte original), et en fait pour les besoins de la preuve, un "+1" aurait suffit, et il est possible que cela soit pour des raisons d'existence. Mais là encore, il n'existe pas de source (à ma connaissance) qui remette en cause, ou interroge, la preuve sur ce point, et je n'ai pas de source détaillant la preuve plus en avant. En l'absence de ces deux genres de sources, il est difficile de mettre des éléments supplémentaires dans l'article, mais il serait tout à fait possible de dire que la preuve montre l'idée générale mais pas les détails de la démonstration. Cordialement --Jean-Christophe BENOIST (d) 17 septembre 2010 à 11:40 (CEST)Répondre
Personnellement, moi, je ne vois pas ou est la preuve. Il est dit :
" Mais, PARADOXE se terminant inévitablement, le résultat retourné par PARADOXE devrait se trouver dans la liste de tous les résultats possibles des machines de ::Turing qui se terminent et dont la taille est inférieure à 10 fois la taille de PARADOXE, ce qui n'est pas le cas par construction de PARADOXE qui retourne un ::nombre n'appartenant pas à cette liste ". Je ne vois pas pourquoi ? Il n'y a donc pour moi aucune contradiction et la démonstration est fausse. Il doit manquer ::quelquchose dans le raisonnement ????? Suis-je le seul penser cela ? --Thieol (d) 19 février 2014 à 11:40 (CEST)Répondre
paradoxe se terminant, elle va être exécutée lors de l'appel de paradoxe, puisque sa taille est inférieure à 10 fois sa taille.
Mais présentée ainsi, la preuve me paraît fumeuse. Pourquoi ne pas demander à paradoxe de juste appeler halt sur paradoxe, et si halt renvoie 0 (ne termine pas), de terminer, et si halt renvoie 1 d'exécuter paradoxe et de retourner le résultat + 1 ? Mais ça doit être à peu de chose près la preuve traditionnelle. Donc, il me semble que la preuve dans l'article ne fait que noyer le poisson en compliquant tout inutilement. Soit j'ai raté qqchose, soit la preuve de Chaitin n'est pas ce qui est présenté dans l'article. Zandr4[Kupopo ?] 19 février 2014 à 03:39 (CET)Répondre
Pour aller plus loin, je crois que on s'en fout de son résultat entier MAX(n)+1 car :
la fonction PARADOXE, si elle a un nombre d'instructions fini (donc HALT l'accepte) va s'appeler elle meme, et donc elle va s'appeler récursivement à l'infini et ne se terminera jamais (donc HALT la refuse). Inversement, si la fonction PARADOXE n'est pas executée par PARADOXE (donc PARADOXE est fini... et acceptée par HALT. ABSURDE ;)
Ai-je raison ? (je suis pas très fort en math...) Jlguenego (discuter) 24 février 2021 à 20:17 (CET)Répondre

que HALT existe plus ou moins mais a une taille infinie modifier

Un raisonnement similaire démontre qu'aucun programme de taille sensiblement inférieure à N bits ne peut résoudre le problème de l'arrêt pour tous les programmes dont la taille est inférieure à N bits. Ce qui signifie que même si HALT pouvait exister, sa taille croîtrait vers l'infini à mesure que la taille des programmes qu'il devrait tester croîtrait aussi vers l'infini.

Je trouve ça intéressant parce que ça suggère :

  • que pour tout programme P qui ne s'arrête pas, il existe une démonstration logique D(P) du fait qu'il ne s'arrêtera jamais (dans le cas de la mémoire finie il suffit de détecter les cycles mais avec la mémoire infinie ça devient une vraie démonstration mathématique)
  • et donc la question c'est de savoir s'il existe un algorithme qui génère en un temps fini pour n'importe quel programme P la démonstration du fait qu'il s'arrêtera ou pas.
  • et la réponse c'est que non : il y a une infinité de données/concepts mathématiques/logiques à accumuler pour "comprendre tous les programmes" et être capable de démontrer en un temps fini s'ils s'arrêtent ou pas (un temps fini mais qui peut croître vers l'infini pour les programmes de plus en plus longs),

ce qui était un peu le CQFD puisque l'idée intuitive de départ était que le programme HALT est par définition un programme très compliqué, LE programme qui comprend tous les autres programmes, et finalement on a la réponse oui ce programme est infiniment compliqué (et donc n'existe que pour des sous-ensembles de programmes par exemple de taille inférieure à un certain L)

et que se passerait-il si ce HALT finalement n'était pas si compliqué et existait bien, avait une taille finie ? est-ce que ça impliquerait que l'algorithmie (ainsi que les mathématiques) soient des sciences finies qu'on peut avoir "fini d'étudier" un jour ? ouf !! heureusement que HALT n'existe pas..

Je ne sais pas si je me suis fait comprendre mais cette idée de possibilité de démontrer (logiquement/mathématiquement) qu'un programme ne s'arrêtera jamais, et de la problématique de générer cette démonstration à partir du simple code source du programme, me parait assez essentielle et devrait être mentionnée dans l'article.

78.227.78.135 (discuter) 22 décembre 2015 à 23:28 (CET)Répondre

Non, je crains que vous ne commettiez une erreur logique : ce n'est pas parce que ce programme hypothétique devrait au moins être de longueur infinie qu'il existe un programme fini (de taille variable) pour chaque programme dont on veut tester l'arrêt. Chaitin prouve même exactement le contraire, à savoir qu'il existe une constante C (assez petite) telle qu'étant donné une axiomatique de longueur N, il y a un programme de longueur < C+N dont l'arrêt est indécidable pour cette axiomatique...--Dfeldmann (discuter) 23 décembre 2015 à 02:59 (CET)Répondre
oui pardon mais justement ça prouve ce que je disais : il manque un paragraphe spécial sur "pour un programme donné la démonstration du fait qu'il s'arrête ou pas" et du problème de générer cette démonstration. et donc on peut reformuler mon message précédent "si on supposait que HALT existe alors .... obligatoirement on supposerait aussi que pour tout programme qui ne s'arrête pas il existe une démonstration (finie) du fait qu'il ne s'arrête pas". donc on est d'accord qu'il faut un paragraphe sur cette question ? 78.227.78.135 (discuter) 24 décembre 2015 à 07:33 (CET)Répondre

La preuve classique est toujours débile parce qu'elle fait toujours intervenir la boucle infinie qui sort du domaine de définition du programme, "while(true);" est un bug ! modifier

La boucle infinie sort du domaine de définition d'un "programme" parce que c'est juste un bug ! cf: https://fr.wikipedia.org/wiki/Bug_(informatique)#Description_2, https://fr.wikipedia.org/wiki/Boucle_infinie, https://www.larecherche.fr/v%C3%A9rifier-des-programmes-en-prouvant-des-th%C3%A9or%C3%A8mes, http://denif.ens-lyon.fr/data/programmation_enslyon/2007_sem2/biblio/Livercy.pdf.

Le cas du castor affairé est plus intéressant pour illustrer le paradoxe parce que c'est exactement le problème savoir si en lisant son code sans ses paramètres d'entrée un programme externe peut il décider que le programme "castor affairé " s'arrête : https://fr.wikipedia.org/wiki/Castor_affair%C3%A9 --Ppignol (discuter) 28 août 2020 à 09:11 (CEST)Répondre

Il n’est dit nul part dans la définition du problème de l’arrêt qu’une spécification qui permettrait de définir ce qui est une machine correcte ou une machine buggée vis-a-vis de la spécification. La donnée du problème est le simple programme. Dés lors pour le démonstrateur la notion de bug n’existe pas. — TomT0m [bla] 28 août 2020 à 10:26 (CEST)Répondre
Tout simplement parce que une "machine" n'est pas censé être buggée c'est le programme qui l'est et un bug est une erreur humaine qui sort du domaine de définition du programme et qui n'est ni sensé être optimisée par quelque logiciel que ce soit ni censé exister tout court dans le programme. Un bug n'a pas de sens et utiliser un bug pour prouver quoi que ce soit n'a pas de sens ! Un bug est un peu comme un ensemble vide ou une division par 0 qui ne conduit nulle part dans un programme, ça n'a pas de sens, c'est une erreur de la part d'un humain. La fusée ariane 5 à explosé en vol à cause d'un bug ce qui a conduit la fusée nulle part. Un bug est une aberration logique et ne peux pas prouver quoi que ce soit hormis qu'un humain a fait une erreur.
A mon sens le cas du castor affairé qui n'est pas un bug est bien plus pertinent pour prouver le problème de l'arrêt. https://fr.wikipedia.org/wiki/Castor_affair%C3%A9
Exclure le bug du domaine de définition de la programmation pour conserver la "preuve" n'enlèvera pas du problème que la "preuve" utilise une erreur humaine de programmation ce qui n'a aucun sens vis à vis de ce que l'on cherche à prouver avec. --Ppignol (discuter) 28 août 2020 à 20:55 (CEST)Répondre
Revenir à la page « Problème de l'arrêt ».