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 ?
Journal Déterminer le domaine d'un programme
24
fév.
2009
# Halting problem
Posté par allcolor (site web personnel) . Évalué à 7.
[^] # Re: Halting problem
Posté par Zakath (site web personnel) . Évalué à 6.
[^] # Re: Halting problem
Posté par Nicolas Boulay (site web personnel) . Évalué à -2.
"La première sécurité est la liberté"
[^] # Re: Halting problem
Posté par allcolor (site web personnel) . Évalué à 3.
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 Nicolas Boulay (site web personnel) . Évalué à -1.
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 allcolor (site web personnel) . Évalué à 6.
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 Nicolas Boulay (site web personnel) . Évalué à -1.
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 Zakath (site web personnel) . Évalué à 5.
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 allcolor (site web personnel) . Évalué à 2.
sans connaitre par avance ses entréesC'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 Nicolas Boulay (site web personnel) . Évalué à 1.
halt(halt,halt(halt, halt(halt ...))) ?
"La première sécurité est la liberté"
[^] # Re: Halting problem
Posté par Thomas Douillard . Évalué à 3.
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 Nicolas Boulay (site web personnel) . Évalué à 2.
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 Nimmy . Évalué à 4.
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 Nicolas Boulay (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 Nimmy . Évalué à 3.
[^] # Re: Halting problem
Posté par Nicolas Boulay (site web personnel) . Évalué à 2.
"La première sécurité est la liberté"
[^] # Re: Halting problem
Posté par allcolor (site web personnel) . Évalué à 3.
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 Nicolas Boulay (site web personnel) . Évalué à 2.
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 allcolor (site web personnel) . Évalué à 4.
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 Nicolas Boulay (site web personnel) . Évalué à 2.
"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 allcolor (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 Nicolas Boulay (site web personnel) . Évalué à 2.
"La première sécurité est la liberté"
[^] # Re: Halting problem
Posté par allcolor (site web personnel) . Évalué à 3.
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 Nicolas Boulay (site web personnel) . Évalué à 2.
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 allcolor (site web personnel) . Évalué à 2.
Ce qu'on veut *savoir* c'est *si* la fonction *halt* existe !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
[^] # Re: Halting problem
Posté par Nicolas Boulay (site web personnel) . Évalué à 2.
(c'est Boulay sinon)
"La première sécurité est la liberté"
[^] # Re: Halting problem
Posté par Thomas Douillard . Évalué à 3.
[^] # Re: Halting problem
Posté par allcolor (site web personnel) . Évalué à 2.
[^] # Re: Halting problem
Posté par Nicolas Boulay (site web personnel) . Évalué à 2.
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 allcolor (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 Nicolas Boulay (site web personnel) . Évalué à 2.
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 allcolor (site web personnel) . Évalué à 4.
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 Nicolas Boulay (site web personnel) . Évalué à 1.
"La première sécurité est la liberté"
[^] # Re: Halting problem
Posté par smc . Évalué à 5.
[^] # Re: Halting problem
Posté par Nicolas Boulay (site web personnel) . Évalué à 1.
"La première sécurité est la liberté"
[^] # Re: Halting problem
Posté par allcolor (site web personnel) . Évalué à 4.
[^] # Re: Halting problem
Posté par Nicolas Boulay (site web personnel) . Évalué à 2.
"La première sécurité est la liberté"
[^] # Re: Halting problem
Posté par allcolor (site web personnel) . Évalué à 3.
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 Nicolas Boulay (site web personnel) . Évalué à 2.
Tu ne définis pas complètement le comportement de halt(in,in) que tu supposes exister. Je demande des précisions sur son comportement pour les fonctions demandant pour paramètre une fonction. Tu ne les donnes pas, genre halt(halt,halt) peut être équivalent à halt(halt, null) et donc à halt(null). Rien ne dit le contraire dans la démonstration.
Je ne comprends pas pourquoi halt(halt, halt) n'est pas définit donc entraîne la non existence de halt mais que halt(func,func); avec int func(int (*foo)()){if(foo()) while(1); else return 0;} n'entraine pas la non existence de func.
"La première sécurité est la liberté"
[^] # Re: Halting problem
Posté par allcolor (site web personnel) . Évalué à 4.
http://fr.wikipedia.org/wiki/Probl%C3%A8me_de_l%27arr%C3%AAt
[^] # Re: Halting problem
Posté par Thomas Douillard . Évalué à 2.
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 briaeros007 . É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 Thomas Douillard . Évalué à 2.
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 Nicolas Boulay (site web personnel) . Évalué à 2.
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 Zakath (site web personnel) . Évalué à 1.
[^] # Re: Halting problem
Posté par Zakath (site web personnel) . Évalué à 1.
Ca faisait vraiment trop de "con" dans le coin.
[^] # Re: Halting problem
Posté par Thomas Douillard . Évalué à 2.
[^] # Re: Halting problem
Posté par Thomas Douillard . Évalué à 3.
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 Nicolas Boulay (site web personnel) . Évalué à 2.
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 Thomas Douillard . Évalué à 4.
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 Ontologia (site web personnel) . Évalué à 2.
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 allcolor (site web personnel) . Évalué à 2.
un ordinateur quantique est un sur ensemble d'une machine de turingnon, 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 arenthis . Évalué à 4.
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 Nicolas Boulay (site web personnel) . Évalué à 2.
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 Nimmy . Évalué à 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 Zakath (site web personnel) . Évalué à 3.
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 Nicolas Boulay (site web personnel) . Évalué à 2.
"La première sécurité est la liberté"
[^] # Re: Halting problem
Posté par Axioplase ıɥs∀ (site web personnel) . Évalué à 4.
(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 Nicolas Boulay (site web personnel) . Évalué à 1.
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 Zakath (site web personnel) . Évalué à 1.
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 Nicolas Boulay (site web personnel) . Évalué à 2.
"La première sécurité est la liberté"
[^] # Re: Halting problem
Posté par arenthis . Évalué à 2.
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 Nicolas Boulay (site web personnel) . Évalué à 2.
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 Thomas Douillard . Évalué à 2.
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 Nicolas Boulay (site web personnel) . Évalué à 2.
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 Thomas Douillard . Évalué à 2.
[^] # Re: Halting problem
Posté par Nicolas Boulay (site web personnel) . Évalué à 2.
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 allcolor (site web personnel) . Évalué à 2.
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 Nicolas Boulay (site web personnel) . Évalué à 2.
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 Thomas Douillard . Évalué à 2.
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 Nicolas Boulay (site web personnel) . Évalué à 2.
"La première sécurité est la liberté"
[^] # Re: Halting problem
Posté par arenthis . Évalué à 2.
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 allcolor (site web personnel) . Évalué à 2.
Discuter sur le comment cette fonction peut-être implémentée * EST INUTILE *.
[^] # Re: Halting problem
Posté par Nicolas Boulay (site web personnel) . Évalué à 2.
"La première sécurité est la liberté"
[^] # Re: Halting problem
Posté par Thomas Douillard . Évalué à 3.
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 Nicolas Boulay (site web personnel) . Évalué à 2.
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 Thomas Douillard . Évalué à 2.
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 Nicolas Boulay (site web personnel) . Évalué à 2.
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 allcolor (site web personnel) . Évalué à 1.
[^] # Re: Halting problem
Posté par Sylvain Sauvage . Évalué à 6.
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 2PetitsVerres . Évalué à 3.
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 Ontologia (site web personnel) . Évalué à 2.
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 Dr BG . Évalué à 2.
# Commentaire supprimé
Posté par Anonyme . Évalué à 6.
Ce commentaire a été supprimé par l’équipe de modération.
[^] # Re: Non
Posté par auve . Évalué à 2.
[^] # Commentaire supprimé
Posté par Anonyme . Évalué à 3.
Ce commentaire a été supprimé par l’équipe de modération.
[^] # Re: Non
Posté par auve . Évalué à 2.
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 Anonyme . Évalué à 1.
Ce commentaire a été supprimé par l’équipe de modération.
[^] # Re: Non
Posté par Axioplase ıɥs∀ (site web personnel) . Évalué à 1.
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 Axioplase ıɥs∀ (site web personnel) . Évalué à 2.
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 Ontologia (site web personnel) . Évalué à 2.
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
[^] # Commentaire supprimé
Posté par Anonyme . Évalué à 2.
Ce commentaire a été supprimé par l’équipe de modération.
# Tiens c'est drôle
Posté par benoar . Évalué à 2.
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 BAud (site web personnel) . Évalué à 4.
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 Ontologia (site web personnel) . Évalué à 2.
« 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 benoar . Évalué à 2.
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 Nicolas Boulay (site web personnel) . Évalué à 2.
"La première sécurité est la liberté"
[^] # Re: Tiens c'est drôle
Posté par benoar . Évalué à 2.
[^] # Re: Tiens c'est drôle
Posté par Nicolas Boulay (site web personnel) . Évalué à 2.
"La première sécurité est la liberté"
# back track
Posté par Nicolas Boulay (site web personnel) . Évalué à 2.
"La première sécurité est la liberté"
# Pour en revenir au problème ...
Posté par smeuuh . Évalué à 5.
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 briaeros007 . Évalué à 5.
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 Aldoo . Évalué à 3.
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 briaeros007 . Évalué à 2.
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 Archibald (site web personnel) . Évalué à 4.
(N,+) n'est pas un groupe (c'est un monoïde).
[^] # Re: Je suis certainement idiot
Posté par briaeros007 . Évalué à 3.
[^] # Re: Je suis certainement idiot
Posté par Metzgermeister . Évalué à 5.
(Petite parenthèse, il faut bien que la prépa serve à quelque chose :D)
# Une idée
Posté par tfeserver tfe (site web personnel) . Évalué à 0.
# Tout ca pour ca
Posté par fanto30 . Évalué à 5.
[^] # Re: Tout ca pour ca
Posté par Bastes . Évalué à 1.
"Ah, merde, c'était quoi la question déjà ?..."
# Un peu différent
Posté par Axioplase ıɥs∀ (site web personnel) . Évalué à 3.
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 Axioplase ıɥs∀ (site web personnel) . Évalué à 2.
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.