Journal Déterminer le domaine d'un programme

Posté par  (site web personnel) .
Étiquettes : aucune
1
24
fév.
2009
Je devrais la mettre en forum, mais ça peut être intéressant.
Une question aux théoriciens qui traînent par ici : est-on capable pour une fonction définie dans un langage turing-complet, ayant défini son ensemble de départ, de déterminer l'ensemble d'arrivé de la fonction ?

Google n'est pas mon ami, pas plus que google scholar, mais je me doute que je ne lui donne pas les bons mots-clés.

Soit f une fonction (un programme), avec E et F tel que f : E -> F
Sait-on définir le domaine de F, en fonction du code de f ?
On part du principe que E et F sont des produits cartésiens d'ensembles d'entiers naturels, sachant qu'on peut assimiler le calcul réel à de la virgule fixe (je fais un grosse approximation là..).
On peut découper le problème en curryfiant récursivement f p fois (sachant que E = |N^p) de sorte à obtenir p fonction du type fi : |N -> F

En improvisant, j'imagine que par analyse de flot, on peut déterminer pas mal de choses, à condition que le programme ne soit pas trop gros. Et encore, espérer tomber sur une fonction qui ne soit pas de complexité exponentielle...
L'idée est d'injecter des intervals et d'analyser toutes les branches en exportant l'interval, l'ensemble sur chacune des branches possible.

Il y a probablement d'autres méthodes utilisant d'autres outils : l'analyse de flot est un algo exponentiel qui peut par conséquent vite devenir inutilisable en pratique.

D'où ma question : est-ce un problème qui prend en pleine figure une incomplétude gödelienne, ou s'agit-il d'un problème résolvable et si oui quel recherches ont été faites là dessus, quel mots clés donner à manger à google scholar ?
  • # Halting problem

    Posté par  (site web personnel) . Évalué à 7.

    Il me semble que c'est du même genre que le halting problem... car si ce que tu dis était possible on pourrait écrire un programme qui décide du problème d'arrêt... On peut donc le faire pour un ensemble restreint de solution.
    • [^] # Re: Halting problem

      Posté par  (site web personnel) . Évalué à 6.

      Plus précisément: tu prends le programme f qui prend en entrée l'entier n et qui exécute le programme de numéro n et qui renvoie n si ledit programme termine (quel que soit le résultat de son exécution). Si tu peux décider si un entier n est dans l'image de f, ça veut dire que la fonction termine, donc tu décides le problème de l'arrêt, donc l'univers implose (c'est malin, tiens !).
    • [^] # Re: Halting problem

      Posté par  (site web personnel) . Évalué à -2.

      Le halting problem, c'est juste le fait de ne pas pouvoir savoir (dans tout les cas) si on programme s'arrête sans connaitre par avance ses entrées. Bref, c'est tellement évident, que cela n'a pas d'utilité pratique.

      "La première sécurité est la liberté"

      • [^] # Re: Halting problem

        Posté par  (site web personnel) . Évalué à 3.

        Ben c'est le fait de savoir si il existe ou non (si le problème est donc décidable ou non) un algorithme/programme qui peut dire pour tout programme en entrée si il va s'arrêter ou non.

        On peut résoudre le problème d'arrêt pour tous les programmes (sans "oracle") si on dispose d'un "oracle" (qui n'existe pas mais c'est pour expliquer le problème un peu plus). Mais dans ce cas on a repoussé le problème d'arrêt pour les programmes + oracle (donc notre algo de décidabilité du problème d'arrêt + oracle ne peut pas décider l'arrêt des prog+oracle)... Mais on peut le résoudre avec un algo de décidabilité + oracle pour les prog sans oracle + oracle pour les progs avec oracle... mais alors on a de nouveau repoussé le problème plus loin, cet algo ne peut décider pour ceux avec 2 oracles et ainsi de suite.

        Le problème que ontologia nous donne ici est du même principe... si tu peux définir à l'avance le domaine complet pour toutes fonctions tu peux écrire un algo qui résout le problème d'arrêt... étant donné que ce n'est pas possible, l'algo que cherche ontologia n'existe pas... ça ne veut pas dire qu'on ne peut pas faire ce qu'il veut pour des cas particulier, ça veut juste dire que c'est infaisable pour le cas général.

        PS: un oracle est une boite noire qui nous assure de résoudre le problème qu'elle doit résoudre... dans notre cas le problème d'arrêt. Genre un extraterrestre arrive sur terre et nous le donne et ça marche :) mais comme montré plus haut, ça ne résout pas alors le problème pour les progs+l'oracle.
        • [^] # Re: Halting problem

          Posté par  (site web personnel) . Évalué à -1.

          Les démos du problèmes d'arrêt que j'ai vu utilise l'oracle et produise une boucle infinie en cas d'arrêt du programme. Celui-ci se mange lui-même ce qui démontre le problème par l'absurde.

          Je trouve cette démonstration débile car si le programme est f(a), on doit lui faire manger f(f(f(f(f...)))) ce qui tourne à l'infini. Qu'il n'y ai pas de solution à une récursion infinie n'a pas l'air très étonnant.

          "La première sécurité est la liberté"

          • [^] # Re: Halting problem

            Posté par  (site web personnel) . Évalué à 6.

            Pas du tout.

            L'algo qui démontre l'indecidabilité est le suivant:

            testArret(prog) {
            si halt(prog,prog) alors boucle infinie
            sinon arret.
            }

            Le problème arrive lors de l'appel suivant:

            testArret(testArret).

            Ce qui appelle finalement:

            halt(testArret,testArret).

            je te laisse faire la suite dans ta tête, l'entrée n'est absolument pas infinie.
            • [^] # Re: Halting problem

              Posté par  (site web personnel) . Évalué à -1.

              Cette démonstration classique est du même ordre que :

              toto (bool a){
              if(a) boucle_infinie() else arret();
              }

              ? testarray(toto);

              La réponse dépend des entrées,ce qui est une évidence qui n'apporte strictement aucune nouvelle information. Et d'un point de vue preuve n'a aucune utilité.

              "La première sécurité est la liberté"

              • [^] # Re: Halting problem

                Posté par  (site web personnel) . Évalué à 5.

                Et toi tu n'as manifestement absolument pas compris ce qu'est le problème de l'arrêt, donc à ta place, j'éviterais de la ramener.

                On sait ce qui va se passer dans la fonction de ton exemple : elle va boucler sur certaines entrées.
                Ce que le problème de l'arrêt dit, c'est qu'il n'existe pas de programme qui, si on lui donne un programme et ses valeurs d'entrée (finies), dira systématiquement si ledit programme termine ou pas quand on l'exécute avec ces valeurs. Ton exemple n'a absolument rien à voir avec la choucroute, et je te conseille un peu de lecture sur le sujet avant de revenir raconter des âneries.
      • [^] # Re: Halting problem

        Posté par  (site web personnel) . Évalué à 2.

        sans connaitre par avance ses entrées

        C'est faux, l'algo prend en entrée un prog et une entrée pour celui-ci... et il te dit si ça s'arrête ou non.

        L'algo est général si pour tout prog et tout entrée donnée il donne la réponse... et on a montré que cela est impossible... rien à voir avec une utilité pratique ou non, ça montre juste qu'il y a des propositions qui sont simplement indécidable.

        la fonction halt se décrit ainsi:

        halt (prog,datain).
        • [^] # Re: Halting problem

          Posté par  (site web personnel) . Évalué à 1.

          et halt() qui se traite lui-même c'est quoi ?

          halt(halt,halt(halt, halt(halt ...))) ?

          "La première sécurité est la liberté"

          • [^] # Re: Halting problem

            Posté par  . Évalué à 3.

            Le problème de l'arrêt c'est pour toutes les entrées possibles, pas que pour "halt" lui même ...

            En gros, ça donne halt : programme , donnee -> booleen

            T'as pas de récursion ici, tu veux savoir si "donnee" s'arrête pour toutes les entrées possibles, quasiment.

            d'ailleurs ta récursion n'a pas de sens, halt(halt,halt) renvoie un booleen, et ce que tu veux faire manger à ton programme c'est un autre programme.
            • [^] # Re: Halting problem

              Posté par  (site web personnel) . Évalué à 2.

              https://linuxfr.org/comments/1010297.html#1010297

              Merci de renforcer mon propos écrit un peu plus haut :)

              halt(halt, halt) ne veut en effet rien dire car le 2 ième halt n'a de sens qu'avec ses entrées.

              Le problème de l'arrêt parle donc bien d'un programme pour toutes ses entrées possibles, ce qui est une évidence dont le résultat n'a pas d'intérêt surtout si l'on considère une entrée de taille infini pour la démonstration.

              "La première sécurité est la liberté"

              • [^] # Re: Halting problem

                Posté par  . Évalué à 4.

                l'analogie du post auquel tu réponds est mauvaise. Ce qui fait marcher le théorème de l'arrêt, c'est justement qu'on peut considérer un programme également comme des données.

                Suppose que tu aies réussi à écrire une fonction (en C) halt2 qui prend une chaîne de caractères représentant une fonction C (à une variable, une chaîne de caractères) en argument et une chaîne de caractères et qui fait la chose suivante:
                - 1 si la fonction C s'arrête lorsqu'on l'exécute sur l'argument et qu'il répond 0
                - 0 dans tous les autres cas

                Maintenant on considère la fonction halt1 définie comme suit
                int halt1(char *x)
                {
                return halt2(x,x);
                }


                Ta fonction halt1 est écrite en C, donc elle est représentée par une chaîne de caractères
                (les quelques caractères écrits plus haut, dans lesquels on aura en gros remplacé l'appel à halt2 par le contenu de halt2), qu'on va appeller t;

                Maintenant, rien n'interdit d'exécuter halt1(t). Et là que se passe-t-il ?
                Vu qu'elle se contente d'appeller halt2 qui répond toujours, le résultat devrait être soit 0, soit 1. Si elle répond 1, c'est à dire halt2(t,t) vaut 1, cela signifie que la fonction représentée par t, lorsqu'on l'appelle avec l'argument t s'arrete et repond 0. Mais la fonction representée par t, c'est justement halt1, donc ca signifie que halt1 lorsqu'on l'appelle avec l'argument t s'arrête et répond 0. Contradiction.
                Le cas avec 1 se règle de la même manière.

                On arrive donc à une contradiction. D'où provient-elle ? Du fait qu'une telle fonction halt2 est impossible à écrire.
                • [^] # Re: Halting problem

                  Posté par  (site web personnel) . Évalué à 1.


                  On arrive donc à une contradiction. D'où provient-elle ? Du fait qu'une telle fonction halt2 est impossible à écrire.


                  Et le fait que t soit de taille infinie, on s'en tape ?

                  Soit la fonction halt(void (* foo)(void *), void * data); qui est notre oracle.

                  void halt1 (char * blob)
                  {
                  void (* foo)(void *) = slice_prog(blob);
                  void * data = slice_data(blob);
                  if ( halt( foo, data)) { while(1); }
                  }

                  Jusque là, on a écrit la même chose.

                  Ensuite, tu propose d'écrire

                  void halt_2( void (* foo)(void *) )
                  {
                  char * blob;
                  memcpy(blob, foo, sizeof(foo));
                  halt1(blob);
                  }

                  void Montest_de_halt()
                  {
                  halt_2(halt1);
                  }

                  On l'exécution on aura:

                  Montest_de_halt();
                  ..halt_2(halt1);
                  ....halt1(blob(halt1));
                  ......halt(halt1, null);

                  Comme halt(null) ==1,
                  donc halt1(null) boucle,

                  donc halt(halt1,null) == 0,
                  donc halt1(blob(halt1)) ne boucle pas.

                  Et le plan d'exécution de montest_de_halt() se déroule sans accroc.

                  Il n'y a rien de contradictoire la dedans.

                  Souvent on me propose comme exemple halt(halt,halt) (que tu appelles halt2(t,t)). Qu'est-ce que cela signifie ?

                  Cela signifie que je veux savoir si halt (instance A) s'arrête avec la fonction halt (instance B) en entrée sans préciser l'entrée de l'instance B. Erreur de compile.

                  Si on considère que halt(halt, halt) est en fait, la fonction qui test l'arret de halt (instance B) ayant halt (instance C)en entrée qui elle même prend halt (instance C) et ainsi de suite, je créait ainsi une suite infini.

                  Comme le résultat final dépend du nombre pair ou impair d'instance de "halt" considérée, je ne peux pas répondre puisque que ce nombre est infini. Je n'ai donc toujours rien prouvé sur l'existence de "halt".

                  "La première sécurité est la liberté"

                  • [^] # Re: Halting problem

                    Posté par  . Évalué à 3.

                    je n'ai pas lu tout ce que tu racontes. t est de taille finie : c'est le code de la fonction halt1
                  • [^] # Re: Halting problem

                    Posté par  (site web personnel) . Évalué à 3.

                    Mais rien à voir...

                    halt est une fonction dont on veut savoir si elle peut exister... donc pour la démonstration (par l'absurde, car on va tirer une contradiction)

                    Supposons que halt existe (on s'en fou du code ce n'est pas l'important, on suppose juste que c'est possible d'écrire une telle fonction et qu'elle est dispo).

                    Donc on peut écrire le programme testArret qui appel halt:

                    testArret(in) {
                    si halt(in,in) alors boucle infinie;
                    sinon arret;
                    }

                    Appelons ce programme avec testArret en paramètre (ce que tu donnes ce n'est pas un pointeur de testArret mais la string représentant testArret, halt étant censé répondre si oui on non la string représantant le programme avec l'entrée qu'on donne va s'arrêter ou non).

                    ça appelle donc halt(testArret,testArret).

                    Si halt(testArret,testArret) repond que le programme testArret qui prend en argument lui-même s'arrête alors je fais une boucle infinie contradisant le fait que halt a dit que testArret avec testArret en paramètre s'arrêtait.

                    Si halt(testArret,testArret) repond que le programme testArret qui prend en argument lui-même ne s'arrête pas alors je m'arrête contradisant le fait que halt a dit que testArret avec testArret en paramètre ne s'arrêtait pas.

                    Il n'y a aucune entrée infinie... nada.

                    Tout ce que ça montre c'est que l'hypothèse comme quoi il est possible d'écrire la fonction halt est fausse.
                    • [^] # Re: Halting problem

                      Posté par  (site web personnel) . Évalué à 2.

                      Tu ne fais que reprendre ce que j'ai écris au dessus sur la manière de comprendre halt(testArret,testArret).

                      Je ne vais pas tout réécrire une fois de plus. Je pose comme préalable que tout est du C normal et que halt existe.

                      Et si on respecte la sémantique C habituel dans le sens que tu présentes, écrire halt(testArret,testArret) veut simplement dire : est-ce que la fonction testarray de testarray de testarray de testarray de testarray de ... s'arrête or c'est une chaine infinie !

                      Le problème est dans la définition de ton "in".

                      "La première sécurité est la liberté"

                      • [^] # Re: Halting problem

                        Posté par  (site web personnel) . Évalué à 4.

                        Non, la fonction halt répond à la question si j'appelle testArret avec en argument la string représentant le programme testArret est-ce que testArret s'arrête.

                        donc en gros elle répond à ceci:

                        testArret(in) {
                        si halt(in,in) alors boucle infinie;
                        sinon arret;
                        }

                        testArret("testArret(in) {\n"+
                        "si halt(in,in) alors boucle infinie;\n"+
                        "sinon arret;\n"+
                        "}");
                        • [^] # Re: Halting problem

                          Posté par  (site web personnel) . Évalué à 2.

                          C'est bizarre c'est peut de chose pret ce que j'ai écrit dans mon long commentaire. Sauf que la conclusion est toujours la même :

                          "la fonction halt répond à la question si j'appelle testArret [instance A] avec en argument la string représentant le programme testArret [instance B] est-ce que testArret s'arrête."

                          La réponse est: cela dépend des entrées de l'instance B !

                          testArret("testArret(in) {\n"+
                          "si halt(in,in) alors boucle infinie;\n"+
                          "sinon arret;\n"+
                          "}");


                          C'est ici encore plus clair, qu'est-ce que tu mets dans le "in" de la 2ième fonction dans la string ?

                          cf mon 1er exemple idiot :

                          testArret("toto (bool a){if(a) boucle_infinie() else arret();}"}

                          testarray() ne peut pas répondre et pourtant toto est parfaitement définit et existe.

                          "La première sécurité est la liberté"

                          • [^] # Re: Halting problem

                            Posté par  (site web personnel) . Évalué à 2.

                            La réponse est: cela dépend des entrées de l'instance B !

                            Tu n'appel pas halt avec une instance de la fonction bordel...

                            Définition de la fonction halt:

                            halt est une fonction qui prend en argument une représentation sous forme symbolique d'un programme ainsi que une entrée à fournir à ce programme et répond si pour cette entrée et ce programme le programme concerné s'arrête.

                            Donc halt(testArret,testArret) doit me dire si lorsque j'appelle testArret avec sa représentation symbolique en entrée, la fonction testArret s'arrête ou non.

                            On montre par la démonstration au dessus que halt ne peut exister car il y a une contradiction. Point.

                            La démonstration montre donc que pour au moins une instance il n'est pas possible de décider l'arrêt. Ça démontre donc que notre hypothèse comme quoi il est possible d'écrire cette fonction halt est fausse et qu'une telle fonction n'existe pas.
                            • [^] # Re: Halting problem

                              Posté par  (site web personnel) . Évalué à 2.

                              et pour testArret("toto (bool a){if(a) boucle_infinie() else arret();}"} tu dis quoi ?

                              "La première sécurité est la liberté"

                              • [^] # Re: Halting problem

                                Posté par  (site web personnel) . Évalué à 3.

                                testArret n'est pas la fonction qui décide de l'arrêt mais halt.

                                Donc ton appel devrait être soit:

                                halt("toto (bool a){if(a) boucle_infinie() else arret();}","false"); ou
                                halt("toto (bool a){if(a) boucle_infinie() else arret();}","true");

                                Le programme testArret est écrit uniquement pour montrer la contradiction...
                                • [^] # Re: Halting problem

                                  Posté par  (site web personnel) . Évalué à 2.

                                  Je sais bien. Je te parle de la fonction que tu as définit toi même plus haut.

                                  Pour mémoire :

                                  testArret(in) {
                                  si halt(in,in) alors boucle infinie;
                                  sinon arret;
                                  }

                                  testArret("testArret(in) {\n"+
                                  "si halt(in,in) alors boucle infinie;\n"+
                                  "sinon arret;\n"+
                                  "}");

                                  "La première sécurité est la liberté"

                                  • [^] # Re: Halting problem

                                    Posté par  (site web personnel) . Évalué à 2.

                                    Mais tu es un boulet c'est pas possible...

                                    Ce qu'on veut *savoir* c'est *si* la fonction *halt* existe !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
                                    • [^] # Re: Halting problem

                                      Posté par  (site web personnel) . Évalué à 2.

                                      Considère qu'elle existe et répond à ma question.

                                      (c'est Boulay sinon)

                                      "La première sécurité est la liberté"

                                      • [^] # Re: Halting problem

                                        Posté par  . Évalué à 3.

                                        Si elle existe, on a des contradictions, donc elle n'existe pas. C'est tout.
                                      • [^] # Re: Halting problem

                                        Posté par  (site web personnel) . Évalué à 2.

                                        J'y ai répondu, j'ai même écrit la démonstration.
                                      • [^] # Re: Halting problem

                                        Posté par  (site web personnel) . Évalué à 2.

                                        Toto prend un boolean ce qui ne vas pas avec testarray qui demande 2 fonctions.

                                        Si tu prends

                                        int toto (int (*foo) (void))
                                        {
                                        if(foo) while(1);
                                        else return 0;
                                        }

                                        Je comprends que halt() est une vue de l'esprit. Par contre toto() existe et compile.

                                        Quelle valeur va retourner halt(toto,toto); ?

                                        "La première sécurité est la liberté"

                                        • [^] # Re: Halting problem

                                          Posté par  (site web personnel) . Évalué à 2.


                                          Quelle valeur va retourner halt(toto,toto); ?


                                          On s'en fout, on a démontré que halt ne peut exister.
                                          • [^] # Re: Halting problem

                                            Posté par  (site web personnel) . Évalué à 2.

                                            Ta démonstration par l'absurde est valide uniquement si tous les éléments sont juste. Si tu ajoutes de l'absurde, ce n'est pas étonnant que tu en es en sorti.

                                            En gros, tu as définit halt(), je te propose de définir un exemple avec mes entrées.

                                            Toute la démonstration repose sur le fait que halt s'avale lui-même. Si tu n'es pas capable sur un cas simple différent de halt d'estimer la sortie comment conclure quoi que ce soit sur halt lui-même ?

                                            "La première sécurité est la liberté"

                                            • [^] # Re: Halting problem

                                              Posté par  (site web personnel) . Évalué à 4.

                                              Ecoutes j'en ai marre, la démonstration est très simple et correcte.

                                              Si tu es trop con ou obtus pour faire fonctionner tes neurones je peux pas t'aider.

                                              A ciao bon dimanche.
                                              • [^] # Re: Halting problem

                                                Posté par  (site web personnel) . Évalué à 1.

                                                Si tu es trop bête pour ne pas voir qu'utiliser un outil (même fictif) dans une démonstration sans pouvoir en donner un seul exemple, ne sert à rien, je ne peux rien pour toi.

                                                "La première sécurité est la liberté"

                                                • [^] # Re: Halting problem

                                                  Posté par  . Évalué à 5.

                                                  Tu n'as pas compris ce qu'était une démonstration mathématique, tu as besoin d'un cours de logique en urgence... Le pire, c'est que tout le monde te dit que t'as tort, mais tu insistes. J'espère que tu essaieras jamais de comprendre le théorème d'incomplétude...
                                                  • [^] # Re: Halting problem

                                                    Posté par  (site web personnel) . Évalué à 1.

                                                    Dire à quelqu'un qui l'a tord, ne l'a jamais prouvé.

                                                    "La première sécurité est la liberté"

                                                    • [^] # Re: Halting problem

                                                      Posté par  (site web personnel) . Évalué à 4.

                                                      Dire à quelqu'un qu'il a tort quand visiblement il n'a pas la capacité intellectuelle pour comprendre une simple démonstration par l'absurde c'est une action de salubrité publique.
                                                      • [^] # Re: Halting problem

                                                        Posté par  (site web personnel) . Évalué à 2.

                                                        Si c'est si simple pourquoi ne répond-tu pas à mes simples interrogations ?

                                                        "La première sécurité est la liberté"

                                                        • [^] # Re: Halting problem

                                                          Posté par  (site web personnel) . Évalué à 3.

                                                          Je répète, j'y ai répondu, j'ai mis la démonstration, je l'ai expliquée.

                                                          La démonstration montre que la fonction halt n'existe pas, la supposition de son existence introduit une contradiction prouvant donc qu'une telle fonction *n'existe pas*.

                                                          Il n'y a rien d'autres à ajouter là dessus.
                                                        • [^] # Re: Halting problem

                                                          Posté par  . Évalué à 2.

                                                          Tes interrogations sont à côté de la plaque, c'est tout.

                                                          La preuve est simple, correcte, bien fondée mathématiquement et logiquement, connue et archi connue.

                                                          Et tes questions n'ont rien à y faire, elles n'ont aucun sens dans le cadre de la preuve. Voire aucun sens du tout.

                                                          C'est difficile de répondre à des questions qui n'ont pas de sens, il faut rentrer dans ta tête pour essayer de comprendre ce que tu voulais dire, sachant que c'est pas clair probablement dans ta tête non plus ... sinon ce serait plus simple pour tout le monde.
                                                          • [^] # Re: Halting problem

                                                            Posté par  . Évalué à 2.

                                                            si l'élève ne comprend pas, c'est peut être à cause du maître.
                                                            Vieux proverbe chinois
                                                            • [^] # Re: Halting problem

                                                              Posté par  . Évalué à 2.

                                                              Il est bon que parfois les deux se remettent en question, c'est l'évidence même.

                                                              Après quand le maître ne comprends pas ou veut en venir l'élève, c'est plus forcément de sa faute ...
                                                  • [^] # Re: Halting problem

                                                    Posté par  (site web personnel) . Évalué à 2.

                                                    Le pire, c'est que tout le monde te dit que t'as tort, mais tu insistes.

                                                    J'ai toujours des demandes de précisions que personne m'apporte.

                                                    "La première sécurité est la liberté"

                                                    • [^] # Re: Halting problem

                                                      Posté par  (site web personnel) . Évalué à 1.

                                                      J'ai la flemme de reconter, mais on a du t'expliquer le problème et démonter tes arguments une bonne demi-douzaine de fois (minimum) dans ces commentaires. Maintenant, si tu n'es toujours pas convaincu, c'est, comme dit dans un autre message, soit que tu es de mauvaise foi, soit que tu es très con. Tu choisis.
                                        • [^] # Re: Halting problem

                                          Posté par  . Évalué à 2.

                                          Non, ce programme ne compile pas, il n'a pas de fonction "main", déja.
                      • [^] # Re: Halting problem

                        Posté par  . Évalué à 3.

                        Ouais alors il faut se rendre à l'évidence, soit tu t'exprimes pas bien et personne comprends ce que tu veux dire, soit quelque part tu as tort, soit le problème de l'arrêt n'en est pas un, ce qui reviendrait à ce que des générations d'informaticiens aient tort, et là t'as intérêt à bien faire comprendre ce que tu veux dire si tu veux pas te faire descendre ;)



                        En gros, tu veux en venir ou ? Cette preuve montre qu'il existe au moins un programme dont l'arrêt est indécidable, et sûrement une infinité d'autres.

                        Donc t'as démontré que le problème dans sa généralité était insoluble. Après en se restreignant à des sous classes du problème effectivement on peut faire des trucs, mais bon, ces classes sont pas forcément toutes intéressantes, et surtout t'as des tas de cas intéressants qui sont pas dedans ...
                        • [^] # Re: Halting problem

                          Posté par  (site web personnel) . Évalué à 2.

                          Je dis juste que :
                          1- que toutes les démonstrations que l'on m'a présenté utilisent des infinis sous forme de string infinie ou de récursion infinie, ce qui est impossible avant même de pouvoir conclure sur une absurdité de l'existence de halt().

                          2- le "halting problem" n'a pas d'intérêt pratique, démontré ou pas

                          La dernière fois que j'avais parlé à un matheux de ce problème, il m'a répondu que l'on parlait du cas général, et donc de toutes les entrées possible du programme était prise en compte. D'où mon 2) et mon exemple utilisant toto et un booléen.

                          "La première sécurité est la liberté"

                          • [^] # Re: Halting problem

                            Posté par  . Évalué à 4.

                            Il n'y a aucune utilisation d'une string infinie.

                            Le programme est fini, les entrées du programmes sont finies (même si l'ensemble des entrées possible est infini)

                            La question c'est : existe t'il un programme qui répond "oui, non" étant donné un programme et une entrée donnée, pour savoir si ce programme boucle ou non avec cette entrée. La réponse est "non".




                            Intérêt ? On aime pas avoir un programme qui boucle en général ... c'est ce qu'on appelle un "bug". Imagine un interpréteur qui te dis "ah non, t'as un problème ton programme va partir en boucle infinie". Pas d'intérêt ?

                            La réponse est non, dans la généralité, un tel interpréteur n'existe pas. intuitivement lui aussi risque de partir en boucle infinie avec le programme qui l'exécute sans pouvoir le détecter.

                            On démontre ça par l'absurde.

                            Et si tu veux casser la récursion c'est facile : tu files un programme sans entrées à ton interpréteur, j'ai pas vérifié mais ça ne doit pas changer grand chose à la démonstration ... Ou alors ça change tout.

                            2- le "halting problem" n'a pas d'intérêt pratique, démontré ou pas

                            Il permet de répondre "non" à Ontologia sans détours. Et à toute une famille de questions relativement identiques.
                            • [^] # Re: Halting problem

                              Posté par  (site web personnel) . Évalué à 2.

                              Alors justement (et j'en profite pour vous remercier de vos explications), d'après ce que j'ai compris, ce problème de halting est un cas typique du théorème d'incomplétude de gödel dans le contexte d'une machine de turing (c'était avec cet exemple que j'avais compris ce théorème).

                              C'est un cas d'indécidabilité au sein d'une machine de turing (son cadre formel plus exactement), mais peut-on lever cette indécibilité dans un sur-ensemble d'une machine de turing ?

                              Je suppose que c'est l'objet de pas mal de recherche ?
                              (et qu'il me semble qu'un ordinateur quantique est un sur ensemble d'une machine de turing).

                              « Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker

                              • [^] # Re: Halting problem

                                Posté par  (site web personnel) . Évalué à 2.

                                un ordinateur quantique est un sur ensemble d'une machine de turing

                                non, un ordinateur quantique est une machine universelle de turing, on peut la simuler sur une machine "classique"... même si évidemment ça prend un temps exponentiel.
                              • [^] # Re: Halting problem

                                Posté par  . Évalué à 4.

                                Alors oui, les gens ont par exemple étudié les fonctions calculables avec une machine de Turing assistée d'un oracle qui sait résoudre le problème de l'arrêt (sur les machines sans oracle).

                                Eh bien on s'aperçoit qu'il n'y a pas de machine avec oracle qui décide de l'arrêt des machines avec oracle. Du coup on peut continuer, et ça fait toute une hiérarchie de classes de fonctions. Bien sûr, on a plus de dispositif physique pour les calculer dès qu'on sort des machines de Turing de base.

                                Et les machines quantiques ne sont pas candidates pour ça, vu qu'elles sont simulables avec des machines classiques.
                            • [^] # Re: Halting problem

                              Posté par  (site web personnel) . Évalué à 2.

                              J'ai très bien compris l'intérêt que l'on voit à ce résultat. Simplement, je n'ai pas l'impression qu'il s'applique dans un cas utile.

                              On démontre ça par l'absurde.

                              merci j'avais compris. J'ai même décortiqué les points qui me posent problème dans la démonstration sans que personne ne vienne répondre à la question.

                              Il n'y a toujours personne qui a répondu concernant la solution de
                              halt("toto(int (*foo)) {if(foo()) while(1); else return 1;}", "toto(int (*foo)) {if(foo()) while(1); else return 1;}");

                              En gros, le résultat d'un exemple utilisant halt sur une fonction sur elle-même, autre que halt().

                              Je veux juste montrer que donner une fonction ayant une fonction en paramètre à traiter (qui attend des données !), n'est pas équivalent du tout, à faire traiter une fonction et une donnés "statique".

                              Au mieux, on a prouvé qu'il n'existe pas de tel fonction mais rien n'interdit la fonction halt() qui prend une fonction et une donnée "statique", d''exister, celle-ci a un intérêt dans le cas de preuve pour un programme.

                              L'autre fonction qui a un intérêt, c'est de savoir si le code s'arrête, le code boucle, ou si l'arrêt dépend des données. Certe une telle fonction peut se construire avec le halt définit habituellement mais c'est un sur-ensemble qui inclus des cas non nécessaire. Par exemple, dans le cas halt(halt), la fonction répondrait cela dépend des données.

                              "La première sécurité est la liberté"

                              • [^] # Re: Halting problem

                                Posté par  . Évalué à 1.

                                Le résultat de halt sur ton exemple précis est simple, c'est 1.
                                En effet, toto, lorsqu'on lui file comme entrée une chaîne de caractères (le deuxième argument) va l'interpréter comme un pointeur foo sur une fonction (puisque c'est ton but), Or c'est une chaine de caractères, pas du tout un pointeut vers une fonction et l'appel foo va segfaulter. Conclusion l'appel de halt va répondre 1, puisque la fonction va s'arreter (en segfaultant)

                                Mais je vois pas en quoi tout cela peut t'aider.
                          • [^] # Re: Halting problem

                            Posté par  (site web personnel) . Évalué à 3.

                            Moi j'en tire des conclusions différentes, une disjonction des cas suivants :

                            1- Tu n'essaies pas de comprendre ce que les gens t'expliquent, puisque tu as déjà décidé que tu avais raison.
                            2- Tu ne lis pas ce que les gens répondent.
                            3- Tu vis dans un univers qui n'utilise pas les mêmes lois logiques que nous.
                            4- Tu ne sais pas lire.
                            5- Tu es vraiment très bête.
                            • [^] # Re: Halting problem

                              Posté par  (site web personnel) . Évalué à 2.

                              Devant le prochain prof de math que je rencontre, je tenterais une démonstration contenant un "de toute façon tu es trop con". Je pense qu'il saura en apprécier toute la subtilité.

                              "La première sécurité est la liberté"

                          • [^] # Re: Halting problem

                            Posté par  (site web personnel) . Évalué à 4.

                            1- en Scheme
                            (let loop ()
                            (loop))

                            Ce programme fait une récursion infinie, sans stack-overflow. Il peut boucler jusqu'à la fin des temps.


                            2- Il est démontré ET il a beaucoup d'intérêts.
                            Le problème, car il y en a un, c''est qu'il semble que tu n'as aucune formation post-bac en maths ni en informatique, et que donc
                            a/ le concept de preuve par l'absurde t'échappe
                            b/ tu n'as jamais eu à faire de preuve qui se ramène au problème de l'arrêt.

                            Je crois avoir saisi ton problème, alors j'y vais simplement:
                            a/ Dans cette preuve par l'absurde, il n'y a même pas besoin de programmer la fonction halt ou de dire comment on peut la programmer, l'instancier. Le simple fait de dire "elle existe" est une information suffisante pour faire la preuve, c'est tout. C'est comme dire "imagine le plus grand nombre qui exiite. Ajoute lui "1". Alors on a un nombre plus grand que le plus grand nombre qui existe. Donc y a pas de plus grand nombre".
                            Tu nous demande si ce nombre est pair ou impair, et on te dit "ca n'a pas de sens, vu qu'il n'existe pas !". Et au bout de 20 messages et 4 liens wikipedia vers la preuve formelle, je comprend leur désarroi et ton niveau en sciences.

                            b/ Enfin, avec une formation en informatique, tu verrais plein de problèmes qui correspondent au problème de l'arrèt, En dans ces cas là on dit "hophop ! stop ! pas besoin de continuer, on a la preuve qu'on pourra jamais écrire cet algorithme".
                            Ici, c'est comme toujours "on formalise le problème, on se dit qu'il ressemble a un autre, et on regarde si cet autre est soluble, et si oui, est-ce qu'on peu le résoudre facilement."
                            T'as plein de problèmes qui ont une solution très dure à calculer, ou qui n'ont pas de solution. Alors pour éviter de calculer les solutions qui n'existent pas ou qui prennent 10 ans à calculer, on dit "c'est comme le problème de l'arrêt" ou "c'est comme le voyageur de commerce", et *tout le monde* est content.


                            Et si t'es au lycée et que t'aimes pas les maths, ne va pas faire d'info à la fac.
                            • [^] # Re: Halting problem

                              Posté par  (site web personnel) . Évalué à 1.

                              Pour ton info, j'ai un DEA d'info passé certe il y a 7 ans.

                              2- Il est démontré ET il a beaucoup d'intérêts.

                              La démonstration que l'on me rabâche prouve que le halt() n'existe pas. Or ce halt() qui n'existe pas n'est pas ou mal définit notamment dans le cas qui intéresse pour faire la démonstration.
                              Donc, je demande des précisions pour savoir précisément de quoi on parle (quitte à remettre en question la démonstration que l'on me balance mais bon).

                              Un halt() qui prend une fonction et une donnée qui n'est pas une fonction demandant des paramètres est une restriction au halt() précédent qui reste utile. idem pour une fonction qui rend un troisième état : "cela dépend des donnés". C'est moins générique mais tout aussi utile.

                              Tu nous demande si ce nombre est pair ou impair, et on te dit "ca n'a pas de sens, vu qu'il n'existe pas !".

                              Comment pouvoir faire une démonstration par l'absurde qui infirme une hypothèse si 2 hypothèses sont absurdes ? Comment savoir laquelle est la bonne ?

                              "La première sécurité est la liberté"

                              • [^] # Re: Halting problem

                                Posté par  (site web personnel) . Évalué à 1.

                                Pour ton info, j'ai un DEA d'info passé certe il y a 7 ans.

                                Et moi qui pensais qu'il n'y avait que les permis de conduire qu'on trouvait dans les pochettes surprise...
                                • [^] # Re: Halting problem

                                  Posté par  (site web personnel) . Évalué à 2.

                                  Le premier mot qui m'est venu à l'esprit, c'était "connard" puis je me suis dis que tu devais avoir bac+12 et moi uniquement bac+6, et je me suis demandé s'il était, sans doute possible, que je gagne le double de ton salaire. Cela m'a calmé d'un coup. Et j'ai mieux compris ton énervement.

                                  "La première sécurité est la liberté"

                              • [^] # Re: Halting problem

                                Posté par  . Évalué à 2.

                                "Un halt() qui prend une fonction et une donnée qui n'est pas une fonction demandant des paramètres est une restriction au halt() précédent qui reste utile."

                                Je ne comprends pas... C'est déjà le cas ! halt n'interprète pas son deuxième argument comme une fonction.

                                Ce que tu n'as pas l'air de voir, c'est que les fonctions sont des données comme les autres. Une fonction C, c'est juste un texte. De même si tu as une donnée d, tenter de l'exécuter est une opération comme une autre. Qui n'a aucune garantie de marcher, bien sûr, si d n'est pas un programme correct.
                                • [^] # Re: Halting problem

                                  Posté par  (site web personnel) . Évalué à 2.

                                  Je ne comprends pas... C'est déjà le cas ! halt n'interprète pas son deuxième argument comme une fonction.

                                  C'est là mon problème. Le premier argument s'applique sur le second, or le second pour exprimer sa signification a besoin d'un argument si il s'agit d'une fonction, que l'on peut définir comment ?

                                  Je propose soit null, soit la fonction elle-même.

                                  "La première sécurité est la liberté"

                                  • [^] # Re: Halting problem

                                    Posté par  . Évalué à 2.

                                    On se fiche de la signification du deuxième argument, c'est une donnée quelquonque.

                                    Tout comme ton premier argument est un programme quelquonque, qui fait tout ce qu'il veut de la donnée quelquonque.
                                    • [^] # Re: Halting problem

                                      Posté par  (site web personnel) . Évalué à 2.

                                      Et pourtant dans la 2ième données quelconque, le paramètre peut changer la réponse attendu !

                                      Tout comme ton premier argument est un programme quelconque, qui fait tout ce qu'il veut de la donnée quelconque.

                                      Donné quelconque qui ne se définit pourtant complètement qu'avec une autre donnée...

                                      "La première sécurité est la liberté"

                                      • [^] # Re: Halting problem

                                        Posté par  . Évalué à 2.

                                        C'est "programme" qui donne une signification, ou pas, a donnée. Si tu lui file une (pour lui) une fonction, mais pas ses paramètres, il peut très bien t'envoyer bouler si il veut, c'est lui qui décide, et tu n'as aucun impact dessus. Dans ce cas tu dois juste deviner qu'il s'arrête.
                                        • [^] # Re: Halting problem

                                          Posté par  (site web personnel) . Évalué à 2.

                                          Prend le cas d'un compilateur C de python et un code de script.

                                          L'interprétation du script n'a rien à voir avec le programme Compilateur.

                                          Et c'est exactement le cas pour la fonction halt() elle même. Sa sortie dépend des 2 paramètres et pas seulement du 1er.

                                          "La première sécurité est la liberté"

                                      • [^] # Re: Halting problem

                                        Posté par  (site web personnel) . Évalué à 2.

                                        http://fr.wikipedia.org/wiki/Machine_de_Turing


                                        Définition [modifier]

                                        La mise en œuvre concrète d'une machine de Turing est réalisée avec les éléments suivants :

                                        1. Un « ruban » divisé en cases consécutives. Chaque case contient un symbole parmi un alphabet fini. L'alphabet contient un symbole spécial « blanc » ('0' dans les exemples qui suivent), et un ou plusieurs autres symboles. Le ruban est supposé être de longueur infinie vers la gauche ou vers la droite, en d'autres termes la machine doit toujours avoir assez de longueur de ruban pour son exécution. On considère que les cases non encore écrites du ruban contiennent le symbole « blanc ».
                                        2. Une « tête de lecture/écriture » qui peut lire et écrire les symboles sur le ruban, et se déplacer vers la gauche ou vers la droite du ruban.
                                        3. Un « registre d'état » qui mémorise l'état courant de la machine de Turing. Le nombre d'états possibles est toujours fini, et il existe un état spécial appelé « état de départ » qui est l'état initial de la machine avant son exécution.
                                        4. Une « table d'actions » qui indique à la machine quel symbole écrire, comment déplacer la tête de lecture ('G' pour une case vers la gauche, 'D' pour une case vers la droite), et quel est le nouvel état, en fonction du symbole lu sur le ruban et de l'état courant de la machine. Si aucune action n'existe pour une combinaison donnée d'un symbole lu et d'un état courant, la machine s'arrête.



                                        Un programme est un ensemble de symbole écrit sur la bande, les données initialises sont aussi des symboles écrit sur la bande (par exemple préfixant le programme).

                                        La fonction halt dont on parle depuis le début a étét discutée en pseudo-code (on aurait pû l'écrire en chinois que ça change rien)... on se fout de son implémentation (dans tous tes exemples tu présuposses que halt éxécute le programme reçu en argument... alors que rien ne l'y oblige ou pas, on s'en fout c'est son implémentation interne et nous on veut savoir si une telle fonction existe.) Or comme la démonstration montre qu'une telle fonction n'existe pas, ça n'a aucun sens de parler d'une éventuelle implémentation dans un éventuel langage. Pourquoi mettre ton halt(halt(halt(....)))). Pourquoi halt exécuterait donc le prog reçu en paramètre ? la spécification c'est de savoir pour tel programme et tel état initial est-ce que le programme s'arrête après un nombre fini d'étape ou non ? Et bien non, on ne peux pas... halt est impossible a écrire, il n'existe aucun algorithme qui pour un programme et un état initial de celui-ci puisse te dire si il s'arrêtera après un nombre fini d'étape.

                                        Si maintenant tu n'as toujours pas compris, je pense que l'explication t'échappera pour toujours.
                                        • [^] # Re: Halting problem

                                          Posté par  (site web personnel) . Évalué à 2.

                                          Je suis microelectronicien, je sais à quoi ressemble un code objet (binaire)...

                                          Tu oublis le cas du compilo C de l'interpréteur python qui exécute un script.

                                          C'est pas en connaissant le compilo C et le code C de l'interpréteur que tu peux conclure quoi que ce soit sur le script.

                                          "La première sécurité est la liberté"

                                          • [^] # Re: Halting problem

                                            Posté par  . Évalué à 2.

                                            Une machine de Turing ça a pas d'IO ...


                                            Tu oublis le cas du compilo C de l'interpréteur python qui exécute un script.

                                            Pose bien ta question, c'est quoi le programme dont tu veux savoir si il s'arrête, et quelles sont ces données dans ce cas ? Tu peux toujours ramener ton problème à ce doublet.

                                            Exemple : pour un compilo, ses données c'est les fichiers sources ou les fichiers objets. Il s'arrête sur une erreur ou en produisant en général du code objet.

                                            Pour un interpréteur ses données c'est le code des fichiers du langage et éventuellement ses IOs. Il s'arrête pas si dans le code des fichiers du langage t'as un 'main(){ while(1){} ; }' ou équivalent par exemple. Il s'arrête si t'as 'main(){ return true; }' ou si t'as pas de main ou sur une erreur de syntaxe, ou sur une erreur d'IO, ...

                                            Après pour nuancer, pour citer wp: The halting problem is, in theory if not in practice, decidable for linear bounded automata (LBAs), or deterministic machines with finite memory. A machine with finite memory has a finite number of states, and thus any deterministic program on it must eventually either halt or repeat a previous state:

                                            C'est décidable si t'as une mémoire finie et une machine déterministe, comme nos machine à nous. Après en pratique si il faut dérouler le programme et il faut sauvegarder tous ses états pour détecter si il revient pas sur un état qu'il a déja rencontrer et donc si il boucle, c'est pas pratiquement faisable.
                                  • [^] # Re: Halting problem

                                    Posté par  . Évalué à 2.

                                    Le premier argument s'applique sur le second

                                    Non, le premier argument est exécuté, avec comme argument le code du second. C'est un peu différent.

                                    Le second pour exprimer sa signification a besoin d'un argument si il s'agit d'une fonction

                                    Non, quand on a le code on peut savoir plein de choses sur une fonction sans avoir à l'exécuter. En faisant de l'analyse statique, par exemple.
                              • [^] # Re: Halting problem

                                Posté par  (site web personnel) . Évalué à 2.

                                Tu présupposes une implémentation de "halt" or son implémentation * ON S'EN FOUT *. Pour la démonstration * LA SEULE ET **UNIQUE** CHOSE NECESSAIRE * est de * PRÉSUPPOSER L'EXISTENCE * de cette fonction. Ce qui permet d'en tirer * UNE CONTRADICTION *. Cette contradiction * PROUVE * qu'il * N'EXISTE PAS * de telle fonction.

                                Discuter sur le comment cette fonction peut-être implémentée * EST INUTILE *.
                                • [^] # Re: Halting problem

                                  Posté par  (site web personnel) . Évalué à 2.

                                  Comment tu veux prouver l'inexistence de quelques choses que tu ne définis pas ?

                                  "La première sécurité est la liberté"

                                  • [^] # Re: Halting problem

                                    Posté par  . Évalué à 3.

                                    Les spécification de halt sont très bien spécifiées, rigoureusement, logiquement et tout.
                                    halt prend : un programme, une donnée quelquonque.
                                    halt renvoie :
                                    * un booléen "vrai" si quand on file a manger "donnée quelquonque" à "programme" il s'arrête
                                    * faux sinon.

                                    "programme" peut s'arrêter dans l'état sur une erreur genre "donnée incorrecte" "j'ai pas les paramètres, je peux rien faire connard" "ça marche c'est cool" "42" ... on s'en fout, on veut juste savoir si il s'arrête ou pas. Dans ces cas là, il s'arrête.

                                    Il n'existe aucun programme qui respecte ces spécifications. Parce que quelle que soit le programme, on peut toujours construire un autre programme à partir de celui là de manière à ce que ces spécification soient violées. Qu'est-ce qui n'est pas défini là dedans ? Le code de la fonction "halt" ? ben ... on voulait justement savoir si il était possible de l'écrire ou non, la réponse est "non".
                                    • [^] # Re: Halting problem

                                      Posté par  (site web personnel) . Évalué à 2.

                                      * un booléen "vrai" si quand on file a manger "donnée quelquonque" à "programme" il s'arrête

                                      Ok. L'important c'est "quelconque".

                                      Si on traduit pour halt(halt,halt), avec halt(halt1,halt2) en utilisant des alias pour des raisons de clarté.

                                      halt renvoie :
                                      * un booléen "vrai" si quand on file a manger "halt2" à "halt1", il s'arrète
                                      * faux sinon.

                                      Or halt2 n'a pas de paramètres définis (cela change son comportement) donc, tu prends l'ensemble des possible en compte ? En gros, tu testes tous les halt1(halt2, foo) avec foo l'ensemble des programmes possibles.

                                      C'est la différence que je voix avec une données statique, sa signification ne change pas avec un autre paramètre.

                                      "La première sécurité est la liberté"

                                      • [^] # Re: Halting problem

                                        Posté par  . Évalué à 2.

                                        Tu te plantes, tu mets des contraintes sur "programme".

                                        Or il est quelquonque. C'est "programme" qui défini son comportement vis-à-vis de la donnée, qu'il peut très bien considérer comme une fonction avec des arguments si il a envie.

                                        Et on peu lui passer n'importe quoi comme données, y compris des trucs qui n'ont pas de sens pour lui. On veut juste savoir si il veut s'arrêter. Éventuellement en te disant "t'as pas donné d'arguments à ma fonction connard", mais c'est pas nous qui décidons.
                                        • [^] # Re: Halting problem

                                          Posté par  (site web personnel) . Évalué à 2.

                                          Or il est quelconque. C'est "programme" qui défini son comportement vis-à-vis de la donnée, qu'il peut très bien considérer comme une fonction avec des arguments si il a envie.

                                          Mais dans ce cas, tu retombes dans le problème de la string infinie (pour le cas du programme qui prend en paramètre un programme et qui s'avale lui-même, au hasard halt()).

                                          Et si tu rajoutes les données dans ta 2ième string, dans halt(halt1,halt2) halt2 ne contient pas de donné à sa suite, il contient donc "null" ?

                                          "La première sécurité est la liberté"

                                          • [^] # Re: Halting problem

                                            Posté par  (site web personnel) . Évalué à 1.

                                            C'est affligeant... j'espère que tu es juste un troll ou un bot... pas un vrai être humain. Ou alors tu as atteint le niveau en bas des couilles d'atuin.
                                          • [^] # Re: Halting problem

                                            Posté par  . Évalué à 6.

                                            Ça fait deux jours qu’on te le répète : il n’y a pas de chaîne infinie !

                                            On la refait, je vais essayer de le faire C-like vu que tu sembles aimer ça.

                                            La fonction halt() prend une fonction F et un paramètre quelconque P et doit dire si la fonction F termine avec P comme paramètre.
                                            typedef void* (*fonction_t)(void*);
                                            bool halt(fonction_t f, void* p);

                                            Pour l’instant, ça va ?

                                            Bon. C’est tout ce qu’on a besoin de définir pour halt() : on cherche à savoir si une fonction qui fait ça peut exister. Donc, par l’absurde, on fait comme si, et on cherche une contradiction. Et on se dit, tiens, si on écrivait une fonction (= un (bout de) programme)
                                            void foutlebordel(fonction_t fn) {
                                              if (halt(fn, code_de(fn)))
                                                while (1);
                                            }

                                            et si on la passait à halt() ?

                                            Et, pensé-je, là où tu coinces, c’est que code_de(fn), c’est fn : une fonction (ou un programme), c’est du code (des octets qui seront interprétés par le processeur / la machine de Turing). Passer un pointeur de fonction sur la fonction foutlebordel, c’est indiquer où se trouve son code (= une suite d’octets) en mémoire, c’est donc comme donner son code directement. (Évidemment, pour nous, humains, c’est plus facile de lire du code en C que les 500 octets correspondant en binaire, mais pour une machine et pour la démonstration, c’est pareil.)

                                            Donc, foutlebordel(foutlebordel) va appeler halt(foutlebordel, code_de(foutlebordel)), c’est-à-dire la même chose que halt(foutlebordel, foutlebordel).

                                            On ne sait pas ce que halt fait avec foutlebordel. On ne sait pas si elle essaie de l’exécuter (on se doute que non vu que halt ne s’arrêterait pas si la fonction ne s’arrêtait pas). On peut penser que halt fait de l’analyse statique de code (comme un compilateur).
                                            On se fout de savoir ce que halt fait avec foutlebordel. On veut juste que ça foute le bordel.

                                            Or donc, halt(foutlebordel, foutlebordel) va nous dire si un appel de foutlebordel(foutlebordel) s’arrêterait. Je rappelle que foutlebordel(foutlebordel) est justement ce qu’on est en train d’exécuter.
                                            Donc, si halt(foutlebordel, foutlebordel) répond :
                                            — vrai, foutlebordel(foutlebordel) part en boucle infinie. Donc halt se trompe ;
                                            — faux, foutlebordel(foutlebordel) s’arrête. Donc halt se trompe.

                                            Donc, si halt existe, halt se trompe sur foutlebordel(foutlebordel). Donc halt ne peut exister.

                                            Ça va mieux ou on va tous se tirer une balle ?
  • # Pas comme ça

    Posté par  . Évalué à 3.

    Si tu utilises ce que tu proposes, ça ne va pas marcher. Tu proposes d'injecter des intervalles. Comment peux-tu trouver un intervalle suffisamment petit que pour voir toutes les branches d'un algo qui ferait quelque chose comme :

    si ( in | MASK_LSB)
    alors
      fait_A
    sinon
      fait_B
    fin si


    Ensuite, ton idée d'intervalle se heurte aussi au problèmes des algorithmes ayant plusieurs variables d'entrée (ce qui fait un produit d'intervalles, ça doit pas mal augmenter le temps de calcul) ou une sortie dépendant de (entrée_t, entrée_(t-1)) (ce qui doit revenier au même que plusieurs variables simultanées)

    Tous les nombres premiers sont impairs, sauf un. Tous les nombres premiers sont impairs, sauf deux.

    • [^] # Re: Pas comme ça

      Posté par  (site web personnel) . Évalué à 2.

      Ensuite, ton idée d'intervalle se heurte aussi au problèmes des algorithmes ayant plusieurs variables d'entrée (ce qui fait un produit d'intervalles, ça doit pas mal augmenter le temps de calcul)

      Pour ce seul petit problème, j'imaginais (j'en parle là haut) de curryfier la fonction de sorte à avoir n fonction à une variable.

      « Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker

      • [^] # Re: Pas comme ça

        Posté par  (site web personnel) . Évalué à 2.

        Ouais, mais le résultat d'une fonction curryfiée est une fonction... comment fait-on ? Si tu discrétise sur chaque variable ça va faire un arbre, dont le nombre de branche augmentera exponentiellement.
  • # Commentaire supprimé

    Posté par  . Évalué à 6.

    Ce commentaire a été supprimé par l’équipe de modération.

    • [^] # Re: Non

      Posté par  . Évalué à 2.

      J'ajoute au model-checking l'approche (plus ou moins concurrente... plus ou moins !) dite de « l'interprétation abstraite » inventée par Patrick Cousot : un cadre rigoureux pour la conception d'analyses statiques correctes basé sur la théorie de l'ordre et les treillis. Une introduction sympathique ici : http://www.di.ens.fr/~cousot/AI/IntroAbsInt.html
      • [^] # Commentaire supprimé

        Posté par  . Évalué à 3.

        Ce commentaire a été supprimé par l’équipe de modération.

        • [^] # Re: Non

          Posté par  . Évalué à 2.

          J'ai toujours eu des problèmes à qualifier les articles de Cousot de "sympathique". Ils sont généralement très ardu et il y a un paquet de symbole dont la police de caractère a été inventée pour l'occasion (on ne sait pas comment le prononcer).

          Je parlais uniquement de la page en question. Effectivement, l'interprétation abstraite n'est pas réputée être abordable, malgré des fondation mathématiques d'un niveau plutôt raisonnable. Il est aussi connu pour avoir une approche des exposés à base de transparents plutôt... singulière, tout comme le personnage d'ailleurs.

          Pour le procès en paternité, je ne suis pas assez au fait de l'histoire mais j'ai quand même quelques doutes. Le fait est que de nos jours beaucoup de gen faisant de l'analyse statique industrielle (MSR, MathWorks/PolySpace, etc.) se placent quand même dans le cadre et la terminologie de Cousot, cf. l'exposé de Tom Ball à l'occasion des trente ans de l'Int. Abs.
          • [^] # Commentaire supprimé

            Posté par  . Évalué à 1.

            Ce commentaire a été supprimé par l’équipe de modération.

            • [^] # Re: Non

              Posté par  (site web personnel) . Évalué à 1.

              Pour avoir suivi le cours de Cousot (et Cousot), j'avoue qu'au départ, les symbols sont un peu lourds. Mais en fait, on s'y fait bien, et c'est resté pas mal cohérent depuis le temps.
              En plus son cours est vachement intéressant (ainsi que ceux des autres intervenants).


              Ontologia: le truc est qu'une fonction, définie par un algorithme, n'offre pas (en général) d'information sur son résultat. Comme (je l'imagine) dit précédemment, faudrait déjà que tu prouves qu'elle termine avant de vouloir trouver pour quelles valeurs elle termine justement…
              La solution a ton problème est donc, selon moi, bien l'interprétation abstraite qui te donnera un sur-ensemble des résultats possibles de ta fonction dans son contexte d'appel.
        • [^] # Re: Non

          Posté par  (site web personnel) . Évalué à 2.

          J'ai pas accès au papier là, mais l'idée de l'IntAbs repose sur le formalisme mathématique derrière, un peu comme un design-pattern: trouver tes abstractions et concrétions, prouver ta correspondance de Galois entre les deux, et calculer un point fixe.

          C'est pas tant que ça lié à l'optimisation, c'est lié à la découverte d'un (ou plusieurs) ensemble(s) de propriétés ou d'invariants de ton programme.
          Ce que tu fais de cette information, ne regarde que toi, pas le matheux qui à adapté le formalisme à certains invariants.
        • [^] # Re: Non

          Posté par  (site web personnel) . Évalué à 2.

          En gros ce papier, ce sont les bases de l'analyse de flot pour la compilation (chose qui est au coeur de Lisaac).
          C'est marrant, car c'est une voie auquel on pense pour faire de la preuve de contrat sur du code Lisaac.

          « Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker

  • # Tiens c'est drôle

    Posté par  . Évalué à 2.

    Je bosse à l'INRIA sur un programme qui fait quasi-exactement ça ...
    Le but c'est de générer des cas de test, et en particulier sur les cas limites, tout en pouvant choisir les types d'entrée qu'on a. On fait ça sur un ensemble restreint du C (pas d'allocation dynamique, pas de récursivité, ...).

    Par contre effectivement, c'est un problème qui peut parfois partir à l'infini sur certains programmes, du fait du problème de décidabilité. On ne peut pas résoudre tous les problèmes, mais pour le domaine auquel on s'intéresse (C embarqué critique) ça marche plutôt pas mal.

    Ça devrait sortir d'ici la fin de l'année (oui, c'est vague) sous une licence plutôt libre (genre GPL ou CeCiLL).

    Et les mots clés pour nous (qui ne sont peut-être pas les tiens), c'est "constraint based testing".
    • [^] # Re: Tiens c'est drôle

      Posté par  (site web personnel) . Évalué à 4.

      hmmm et il y a tellement peu de moyens dans la recherche en Informatique en France que c'est sur LinuxFr que vous vous retrouvez ? :D
      Moi qui croyait qu'il devait y avoir de plus en plus de publications...

      /me ~~~~> [ ]

      hum ah, j'en profite pour suggérer http://linuxfr.org/2007/09/08/23072.html et http://sciwi.sourceforge.net/ comme ça vous aurez tous les moyens de nous tenir régulièrement au courant de l'avancement (release early, release often qu'ils disaient ;-) ).
    • [^] # Re: Tiens c'est drôle

      Posté par  (site web personnel) . Évalué à 2.

      Vous devriez faire un mode Java, c'est surement beaucoup plus propre que du C, et vous pourriez confier à qq ingénieurs de recherches de créer une startup pour vendre le produit, ça vous ferait du "fuck-you money" : si tu arrives à automatiser les tests unitaires dans n'importe quel SSII, ça aura un impact énorme !

      « Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker

      • [^] # Re: Tiens c'est drôle

        Posté par  . Évalué à 2.

        Oui Java serait mieux, mais à la base la cible c'était l'embarqué, et comme ça fait un bout de temps que le chercheur est dessus (moi je ne suis pas chercheur en fait, hein) il n'a pas changé d'objectif en route : c'est toujours le C embarqué critique, et c'est toujours comme ça que ça marche d'ailleurs dans ce domaine.

        Par contre, il y a une thésarde qui bosse pas loin de moi sur Java et la modélisation par contrainte du bytecode, pour la génération de test. Elle arrive même à gérer l'allocation dynamique, elle. Je pense que si elle développe son truc, ça peut effectivement devenir énorme.

        Par contre, un petit bémol à tout ça : normalement, le programme va générer des entrées pour atteindre certains objectifs, mais normalement les sorties doivent être données par un oracle. Il peut les calculer, mais à ce moment c'est faire le boulot du programme à se place, et ce n'est pas le but. Bref, on peut prendre une bonne part du boulot des mecs qui font de la valid', mais il y aura toujours de la place pour ceux qui jouent les oracles.
    • [^] # Re: Tiens c'est drôle

      Posté par  (site web personnel) . Évalué à 2.

      C'est Astrée ?

      "La première sécurité est la liberté"

      • [^] # Re: Tiens c'est drôle

        Posté par  . Évalué à 2.

        Non. C'est pas encore sorti (remarque, je ne connais pas Astrée) à part quelques publis.
        • [^] # Re: Tiens c'est drôle

          Posté par  (site web personnel) . Évalué à 2.

          Et votre équipe ont des papiers la dessus ? Je serrais curieux de voir ce qui se fait sur des algo qui passe à l'échelle (et non qui explosent après 100 lignes de code).

          "La première sécurité est la liberté"

  • # back track

    Posté par  (site web personnel) . Évalué à 2.

    Au lieu de générer tous les états possibles et ensuite vérifier les propriétés qui t'intéressent, je partirais des propriétés puis je remonterais le flot de programmes pour en vérifier la propriété. La taille du problème est beaucoup plus faible. Tu remontes le cônes d'influences.

    "La première sécurité est la liberté"

  • # Pour en revenir au problème ...

    Posté par  . Évalué à 5.

    Déjà, définis proprement le problème. Pour commencer, c'est inutile de considérer autre chose que N, vu que tu peux mettre en bijection N et N^p
    Déjà, si la question est "étant donné un programme f, peut-on écrire un programme qui détermine l'ensemble des valeurs prises par f en temps fini", la réponse est non, vu que ça se ramène facilement au problème de l'arrêt.

    A partir de là, une question plus intéressante (en supposant que, dans ta formulation E est le domaine de f, donc) est : "étant donné un programme f qui termine pour chaque entrée, est-il possible d'écrire un programme qui détermine l'ensemble des valeurs prises par f en temps fini". Ca m'étonnerait franchement que ce soit possible, à moins que E ne soit fini (tu essaie d'évaluer la fonction en un nombre infini de points), mais j'ai pas de preuve sous la main.

    Je suis peut être complètement à côté de la plaque, mais ça me semble être un problème idiot qui ne nécessite certainement pas de parler de curryfication, d'analyse de flot ou d'incomplétude gödelienne.
  • # Je suis certainement idiot

    Posté par  . Évalué à 5.

    Mais, on entend plein de gens repartir sur le problème de l'arrêt, etc...
    Mais moi j'ai une autre approche, qui provient de la théorie de l'ensemble.

    Si on se place dans un groupe par exemple (N,+).
    On sait que + est une loi interne (ou une connerie comme ça) du groupe, et que par conséquent, si je fait
    f(a,b)=a+b; a€N; b€N , on peut dire que f(a,b)€N

    Les théorèmes d'incertitudes sont très bien, mais ils parlent d'un cas totalement général.

    C'est comme les problèmes NP : certains sont P-approx.

    En restreignant une partie des hypothèses (je sais pas moi, au niveau de l'ensemble de départ, des fonctions utilisés dans la fonction à tester, ...) il ne serait pas possible d'essayer d'appliquer ce genre de raisonnement ?
    • [^] # Re: Je suis certainement idiot

      Posté par  . Évalué à 3.

      Moui, enfin on avait bien précisé Turing-complet, ce qui est suffisant pour invoquer le problème de l'arrêt.
      Si tu restreints suffisamment le type de programme que tu considères pour que le problème soit décidable, mécaniquement tu n'est plus dans un langage Turing-Complet, et tu sors du cahier des charges ;-).

      Maintenant est-ce qu'Ontologia avait vraiment besoin d'un langage Turing-complet ?
      (m'est avis que sa question était en fait de nature purement spéculative et qu'il serait vain d'essayer de refourguer autre chose !)
      • [^] # Re: Je suis certainement idiot

        Posté par  . Évalué à 2.

        j'avais précisé que je n'en savais rien, c'était une simple proposition ;)

        m'est avis que sa question était en fait de nature purement spéculative et qu'il serait vain d'essayer de refourguer autre chose !
        Ca je peux pas dire, mais on peut toujours essayer :P
    • [^] # Re: Je suis certainement idiot

      Posté par  (site web personnel) . Évalué à 4.

      >> Si on se place dans un groupe par exemple (N,+).

      (N,+) n'est pas un groupe (c'est un monoïde).
      • [^] # Re: Je suis certainement idiot

        Posté par  . Évalué à 3.

        je te crois. Je connaissais même pas le terme monoïde, c'est pour dire mon inculture ;)
        • [^] # Re: Je suis certainement idiot

          Posté par  . Évalué à 5.

          (N, +) dispose d'un élément neutre (l'élément noté 0), la loi + est associative mais ses éléments ne sont pas tous symétrisables : par exemple, il n'existe aucun élément e dans N tel que 1 + e = 0. En ceci, il est un monoïde et non un groupe.

          (Petite parenthèse, il faut bien que la prépa serve à quelque chose :D)
  • # Une idée

    Posté par  (site web personnel) . Évalué à 0.

    en postant ici http://linuxfr.org/forums/31/index.html tu trouveras plein de spécialistes :)
  • # Tout ca pour ca

    Posté par  . Évalué à 5.

    Tout ca pour ca tourne 6 millions d'années et que ca nous dise que la réponse est 42 ...
    • [^] # Re: Tout ca pour ca

      Posté par  . Évalué à 1.

      *6Ma plus tard...*

      "Ah, merde, c'était quoi la question déjà ?..."
  • # Un peu différent

    Posté par  (site web personnel) . Évalué à 3.

    Pfioou. J'ai eu du mal à retrouver cet article !
    L'idée est que, pour certains (co)domaines, tu as des propriétés sympas.
    A défault de pouvoir lister ton co-domaine, tu as accès en temps fini à tous ses éléments.
    Si t'as une comparaison à faire, ça peut être utile.

    http://math.andrej.com/2007/09/28/seemingly-impossible-funct(...)
  • # Cousot, le retour

    Posté par  (site web personnel) . Évalué à 2.

    > l'analyse de flot est un algo exponentiel qui peut par conséquent vite devenir inutilisable en pratique.

    Et c'est pour ça qu'on utilise en interprétation abstraite des "widenings" qui permettent d'atteindre la stabilité de ton flot en temps fini (encore de sombres histoires de points fixes).

    Mais ton idée est bonne, c'est juste que Cousot (et Cousot) l'ont eue avant toi et l'ont publiée en 77 :)

    Pour faire court: pas de mots clefs à chercher car ton problème est insolvable dans le cas général.
    OU ALORS le mot clef est "type".
    Car étant donné le code de f, un langage comme Caml va te donner son type "a->b", auquel cas, ce que tu appels "le domaine de F" est "toutes les valeurs de b". Mais encore une fois, tu as sans doute perdu en précision, car ta fonction ne retourne peut être qu'une seule valeur de b et toujours la même.

    Le problème est qu'un fonction en maths est une restriction d'une relation (des paires (in,out)), donc une table, et qu'en info, tu la vois comme un algorithme, et donc comme un calcul. Et les deux visions ne coïncident pas pour certains problèmes…

Suivre le flux des commentaires

Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.