Inscrivez-vous gratuitement
pour pouvoir participer, suivre les réponses en temps réel, voter pour les messages, poser vos propres questions et recevoir la newsletter
Euh ça c'est faux hein... Déjà en théorie c'est faux (si l'algo en N a une constante suffisamment grande par rapport à la taille de tes jeux de données) et en pratique ça peut l'être également en fonction desdites constantes et de l'adéquation des algos aux jeux de données (y'a des exemples connus dans les algos de tri).Envoyé par souviron34
Je ne sais aps ce que tu entends pas "ne se démontre pas", mais on peut construire un certain nombre de preuves autour d'une heuristique (qui n'est jamais qu'un algo comme les autres) : cas moyen, au pire, meilleur cas etc. que ce soit en terme de complexité ou de proximité avec le résultat exact.
Je ne sais pas moi-même je t'avoue.
Mais n'essaies pas de noyer le poisson en me faisant dire ce que je n'ai pas dit!
...
ptin 'faut que j'y aille molo sur le whisky dans le café moi...
Alors je vais essayer d'être sérieux deux minutes. spô gagné...
Des souvenirs que j'ai de mes cours d'informatique théorique (c'est comme ça que le module s'appelait en maîtrise et DESSS (ancien Master)), une heuristique c'était, en gros: on a trouvé une solution qui marche, par tâtonnement, mais il n'y a pas vraiment de théorie derrière. Tiens, je viens de tomber sur la définition du wiktionnaire qui me convient bien:
Méthode de résolution de problèmes non fondée sur un modèle formel et qui n'aboutit pas nécessairement à une solution optimale.
Puisque ce n'est pas "fondé sur un modèle formel", on ne peut pas le démontrer. On peut faire des approximations, comme tu le dis, des estimations, mais on ne peut pas appliquer un formalisme mathématique qui permet de le démontrer, sans ambiguïté, et sans contestation possible.
Un autre truc dont je voulais causer. Je ne ne suis pas expert dans le domaine, mais j'ai quelques notions.
Le développement logiciel est à cheval entre la science et la technique. Une partie de notre travail peut être démontré, cette partie est donc scientifique, mais toute une partie dépend d'une machine, quelque chose de concret, donc sensible à la contingence. Pour montrer cela, j'aime bien parler du problème de la coupure de courant: un gars me montre un logiciel qu'il prétend infaillible. Je lui pose alors la question: comment gère-t-il le problème de la coupure de courant?
Dans un logiciel, il y a trois couches principales. Il y a la couche théorique, mathématique. Il a la couche logicielle, ce qu'on appelle l'implémentation. Et il y a la couche matérielle, le hardware.
S'il est possible d'effectuer un travail scientifique au niveau de la couche théorique, algorithmique, on ne peut pas le faire au niveau des autres couches. C'est la raison pour laquelle les question de tests sont si importantes et variées (unit testing, tests d'intégrations, tests fonctionnels, ...) et qu'il existe même une méthode de développement qui se base sur les tests (test driven development).
Je parle de ça pour insister sur le fait qu'en informatique, il y a vraiment trois mondes très différents qui se rencontrent, et que ce qui est applicable dans un monde ne l'est pas dans l'autre.
« L'effort par lequel toute chose tend à persévérer dans son être n'est rien de plus que l'essence actuelle de cette chose. »
Spinoza — Éthique III, Proposition VII
Cette définition est fausse... Regarde ce qui se fait sur le voyageur de commerce par exemple, tu peux avoir des fondements mathématiques à des heuristiques.
C'est hors sujet, mais tu peux maintenant démontrer que ton implémentation respecte bien les specs.
Il faut traduire les specs en formule mathématique (logique des prédicats ou équivalent), faire de même avec le code sachant qu'il y a aujourd'hui des logiciels qui le font automatiquement (basés sur le lambda calcul, donc prouvables mathématiquement).
Ensuite y a plus qu'à utiliser un moteur de preuve à qui tu donnes tes specs et ton code (traduits). Je dis yaka, mais en général c'est plus compliqué que ça
Ca va pas plus haut que le niveau du TU, mais ça existe. C'est peu utilisé parce que ça coûte un bras* et qu'il n'y a pas grand monde de formé dessus.
*Il faut en général plusieurs jours pour prouver une fonction, à multiplier par le nombre de fonctions qu'on veut prouver, et rajouter un peu de temps pour la preuve globale une fois que toutes les fonctions ont été prouvées de manière autonome
http://www.traducteur-sms.com/ On ne sait jamais quand il va servir, donc il faut toujours le garder sous la main
OK mea culpa..Je n'avais pas envisagé ça.. surtout la première partie (alors que c'est une des bases de mon papier sur les calculs d'enveloppes convexes !!!)
Mais c'est de toutes facons hors champ des arguments de Neckara, qui parle de configuration matérielle ou du langage utilisé.. On reste dans l'algorithmie pure...
PS: et d'ailleurs, dans les calculs de complexité, suivant le type de complexité (et même avec celle "par défaut") on peut mentionner la valeur de la constante...
euh....
Par exemple https://en.wikipedia.org/wiki/Simplex_algorithm
De même ce que je citais plus haut, l'heuristique Akl-Toussaint pour les calculs d'enveloppe convexe, est une heuristique, mais peut etre prouvée....
Tiens; un exemple de problème d'implémentation par rapport à algorithme...<mode=friday_troll>
Sauf si l'algo en O(N2) est implémenté dans un vrai langage de programmation, comme le c++ par exemple, et que celui en O(N) est implémenté dans un truc chelou de type java.
Et puis lindows c'est mieux que winux tfaçon!
</mode>
Une vidéo de 8 minutes à sauvegarder en MP4 (algorithme).. Sur le même ordi (donc même configuration matérielle)
- Windows avec MovieMAker : 10 minutes de traitement, fichier résultat 1.2 Go
- Linux avec kdenlive : 1h40 de traitement, fichier résultat 126 Mo
A mon humble avis, Movie Maker a fait l'impasse sur un élément de l'algorithme, ce qui lui permet d'aller 10 fois plus vite, mais de donner un résultat 10 fois plus gros... (tout en correspondant au standard)
"Un homme sage ne croit que la moitié de ce qu’il lit. Plus sage encore, il sait laquelle".
Consultant indépendant.
Architecture systèmes complexes. Programmation grosses applications critiques. Ergonomie.
C, Fortran, XWindow/Motif, Java
Je ne réponds pas aux MP techniques
On est un peu hors-sujet, mais pas tant que ça il me semble:
Attention. MP4 n'est pas un format, mais un conteneur. En gros, il contient le fichier vidéo, le fichier audio correspondant, ainsi que des méta données qui définissent ce contenu.Une vidéo de 8 minutes à sauvegarder en MP4 (algorithme).. Sur le même ordi (donc même configuration matérielle)
- Windows avec MovieMAker : 10 minutes de traitement, fichier résultat 1.2 Go
- Linux avec kdenlive : 1h40 de traitement, fichier résultat 126 Mo
A mon humble avis, Movie Maker a fait l'impasse sur un élément de l'algorithme, ce qui lui permet d'aller 10 fois plus vite, mais de donner un résultat 10 fois plus gros... (tout en correspondant au standard)
Le fichier audio lui, est probablement encodé en mpeg2, qui est le standard depuis une dizaine d'années.
Et pour en revenir à la question initiale, pourquoi mpeg2 est devenu le standard de la compression vidéo? Même question avec mp3 pour l'audio (et pas ogg par exemple). Car dans les deux cas, il y a d'autres algorithmes qui existent et qui ont leurs atouts.
Hé bien la raison, c'est le consensus. Un consensus qui s'est formé au sein des universitaires (ceux qui ont créé ces algorithmes), des constructeurs et des développeurs, mais surtout au sein des utilisateurs.
Ce consensus d'usage dont je parle ici est très différent du consensus scientifique dont il est question initialement, cependant ses processus d'émergence sont les mêmes: on a une théorie, si elle est utile, la communauté scientifique s'en empare, et si elle est robuste, alors elle fait consensus.
« L'effort par lequel toute chose tend à persévérer dans son être n'est rien de plus que l'essence actuelle de cette chose. »
Spinoza — Éthique III, Proposition VII
Non.
Déjà, je ne pense pas vraiment avoir parlé des langages et c'est surtout toi qui parlait du matériel pour dire que de toute façon la vitesse serait différente et donc qu'il ne faut regarder que la complexité.
Par rapport au matériel, tout ce que j'ai dit, c'est que tu peux très difficilement prévoir le temps d'exécution.
Et pour la taille du jeu de données, je t'avais déjà donné un exemple il y a quelques posts.
Avec tous les drivers qui vont bien ?Une vidéo de 8 minutes à sauvegarder en MP4 (algorithme).. Sur le même ordi (donc même configuration matérielle)
Pendant des années je me plaignais de piètres performances sous Linux... Jusqu'au moment où je me suis aperçu que j'utilisais la chipset graphique au lieu de la carte graphique.
Autant te dire qu'une fois les drivers propriétaires installés et tout bien configuré, les performances n'avaient plus rien à voir.
Ce n'est pas utilisé parce que c'est du pipo cette histoire, tout simplement.
Comment tu gères les dépendances dans ton bouzin? Comment tu testes les interfaces graphiques? Comment tu gères les "experts word/excel" qui pondent les specs de façon à ce qu'elles soient compatibles avec l'outil? Comment prends-tu en compte les spécificités hardware? Comment tu fais un bon stress tests (je ne parle pas de simulation à base de machines virtuelles et de modèles)?
Ainsi de suite.
Au bout d'un moment, il faut arrêter de croire qu'on peut simuler le réel...
« L'effort par lequel toute chose tend à persévérer dans son être n'est rien de plus que l'essence actuelle de cette chose. »
Spinoza — Éthique III, Proposition VII
Tu oublies l'utilisabilité et l'efficacité et la simplicité...
Le groupe de travail MPEG a longuement réfléchi à une manière souple et uniforme d'encoder toutes les tailles, a donné le code à disposition , en C, avec les "makefile" pour faire d'un côté l'encodeur et de l'autre le décodeur, tout comme le NCSA et le CERN avaient mis à disposition le code pour faire HTML et un navigateur...
Or ces codes se compilent et s'incluent facilement, sont rapides à exécuter sur toutes machines (flags de compilation standard) et donnent un résultat excellent...
Mais si tu regardes l'intérieur du code, tu verrais qu'il ne résisterait pas à une "preuve"... C'est ce que je disais plus haut.... En informatique, c'est plus un consensus basé sur l'usage et la facilité que sur le fait que le "raisonnement" (le code) est à toute épreuve... Donc il n'y a pas de "vrai" ou "faux"...
Effectivement c'est très different de ce dont on parle au dessus, puisque, dans le cas de la science, un seul contre-exemple suffit à détruire l'argument....
"Un homme sage ne croit que la moitié de ce qu’il lit. Plus sage encore, il sait laquelle".
Consultant indépendant.
Architecture systèmes complexes. Programmation grosses applications critiques. Ergonomie.
C, Fortran, XWindow/Motif, Java
Je ne réponds pas aux MP techniques
OK voila le premier billet du blog est fait et le lien vers les vidéos y figure..
Bonne lecture et bon visionnage...
"Un homme sage ne croit que la moitié de ce qu’il lit. Plus sage encore, il sait laquelle".
Consultant indépendant.
Architecture systèmes complexes. Programmation grosses applications critiques. Ergonomie.
C, Fortran, XWindow/Motif, Java
Je ne réponds pas aux MP techniques
https://fr.wikipedia.org/wiki/Méthod...at.C3.A9gories
Regarde la 4ème catégorie, c'est exactement ça.
Un des outils utilisé pour la preuve formelle :
http://frama-c.com/what_is.html
Tu formes tes experts à écrire une spécification formelle, ce qui signifie avoir un bagage mathématique important.
Ce n'est pas beaucoup utilisé, mais c'est utilisé. Que je sache c'est utilisé uniquement dans le domaine de l'embarqué critique -et encore pas souvent- ou dans en R&D pour la recherche sur des générateurs de code. Pour prouver une simple fonction avec quelques affectations et opérations mathématiques de base, ainsi que quelques if ça peut prendre plus d'une semaine, le temps d'écrire la spec formelle, éventuellement rajouter des hypothèses que l'outil n'a pas su prendre en compte. Cas concret, j'ai du rajouter une hypothèse indiquant qu'un indice de tableau était positif ou nul pour prouver une fonction (l'indice était défini dans un autre module, l'outil était incapable de deviner ça seul).
Tu peux supposer les dépendances prouvées pour tester ta fonction. Mais ton projet (ou module) ne sera considéré comme prouvé que si tu prouves les dépendances également. Pour mon cas juste au-dessus, une fois prouvé chaque module indépendamment, je lançais une preuve globale ignorant les hypothèses que j'avais rajouté en cours de route. Le moteur de preuve ayant le contexte, il n'avait plus besoin de moi pour constater que l'indice de tableau était positif ou nul, donc il pouvait finir la preuve tout seul.
Je sais pas, je fais du bas niveau donc les interfaces graphiques... c'est du pipo, ça existe pas
Si tu écris du code C ne dépendant pas du hardware, tu n'as pas de spécificités hardwares à prendre en compte. On ne teste pas la couche matérielle, et le code n'est pas forcément très optimisé (d'ailleurs la compilation se fait globalement sans optimisation).
Comme je l'ai mis, tu peux prouver que ton implémentation respecte les specs, au niveau du TU. Pas que le programme va tenir la charge (donc tu dois quand même faire des TI, TV, stress tests etc...).
http://www.traducteur-sms.com/ On ne sait jamais quand il va servir, donc il faut toujours le garder sous la main
Bon, je ne répond pas parce que ce serait trop hors-sujet. Mais sache que je suis choqué!
En plus d'être de la merde (tester du code non optimisé... genre un constructeur automobile teste ses voiture à 20 km, c'est très sérieux...) ça va nous mettre au chômage tes conneries là!
Nan mais alô?! Le mec il vient programmer et il amène sa bouteille de lambda-calcul! Nan mais alô quoi!
Je suis outré!
« L'effort par lequel toute chose tend à persévérer dans son être n'est rien de plus que l'essence actuelle de cette chose. »
Spinoza — Éthique III, Proposition VII
Voilà. Ca peut être utile dans certaines niches, mais dans mon monde à moi - ou celui de R0d, c'est juste inapplicable. Je conçois qu'effectivement, pour du très bas niveau, c'est intéressant. Pour choisir les clients que le conseiller bancaire doit appeler ce mois-ci pour lui vendre un produit quelconque, c'est inapplicable. Le seul critère, c'est que la liste finale plaise au spécialiste marketing. Et ça, avant de le formaliser.....(.../...)Je sais pas, je fais du bas niveau donc les interfaces graphiques... c'est du pipo, ça existe pas
Les 4 règles d'airain du développement informatique sont, d'après Michael C. Kasten :
1)on ne peut pas établir un chiffrage tant qu'on a pas finalisé la conception
2)on ne peut pas finaliser la conception tant qu'on a pas complètement compris toutes les exigences
3)le temps de comprendre toutes les exigences, le projet est terminé
4)le temps de terminer le projet, les exigences ont changé
Et le serment de non-allégiance :
Je promets de n’exclure aucune idée sur la base de sa source mais de donner toute la considération nécessaire aux idées de toutes les écoles ou lignes de pensées afin de trouver celle qui est la mieux adaptée à une situation donnée.
@souviron34 : Ton amis, il ne serait pas psychanalyste à tout hasard ?
C'est pourtant considéré comme une pseudo-science non ?
Valider un algorithme si tu veux, pas démontrer un algorithme. On démontre une proposition (on prouve qu'elle est vraie), or un algorithme n'est pas vrai ou faux. On valide un algo/processus (on prouve qu'il fait ce qu'on souhaite qu'il fasse). Éventuellement tu démontres que "l'algorithme se termine" ou "l'algorithme fournit X", mais tu ne démontres pas l'algo.
Pour répondre à la question, on va d'abord préciser son sens. Primo, on valide l'algo, autrement dit on prouve qu'il fait ce qu'on attend de lui. Secundo, on le prouve par consensus... Ça c'est typiquement une évidence empirique : on ne démontre en fait rien, on montre juste que les évidences s'accumulent en faveur de la validité de l'algo. Cela veut dire qu'après de nombreuses utilisations avec succès (nombreux comparé aux échecs), on peut raisonnablement dire que l'algo donne de bon résultats.
Est-ce que ça a du sens de compter sur de tels résultats ? Oui d'un point de vue pratique, car ça permet de prendre des décisions même si on n'a pas le bagage théorique pour s'assurer que ce soit forcément vrai. Ne pas avoir la démonstration que l'algo se termine ne veut pas dire avoir la démonstration du contraire, et qu'une implémentation donnée se termine n'est pas une preuve, car on n'implémente pas un algo sans faire des choix techniques, qui peuvent s'éloigner des résultats théoriques. D'un point de vue scientifique, c'est plus discutable : oui si le but est clairement de faire une étude des pratiques, non si c'est pour analyser l'algo en question.
En entreprise, la priorité est le consensus. En science, c'est la preuve. L'entreprise joue sur le pari, la science sur les faits.
Le fait est que quand c'est formel, comme tes pseudo-démonstrations, nul besoin de lire plusieurs articles sur le sujet : il faut en revenir aux bases. Pour chaque étape de la démonstration, il faut se poser la question de la validité de l'opération de l'étape. L'exemple de diviser par (a-b) qui revient à diviser par 0 par exemple est un exemple concret. Ce n'est pas le fait de diviser par (a-b) qui est mauvais, c'est le fait de faire la division en oubliant de mentionner "si a != b", qui est une condition nécessaire à l'application de cette règle. Ton raisonnement tombe dès lors que tu mets en lumière que les étapes précédentes se basent sur "a=b", ce qui vient en conflit avec cette condition.
Les pseudo-démonstrations ne sont ni plus ni moins qu'un manque de rigueur. Un PC par exemple ne fait pas ce genre d'erreur. Il ne trouve pas forcément les preuves facilement, mais il les vérifie aisément, tant que celles-ci sont des preuves formelles.
Non, le principe des problèmes NP n'est pas une question de preuve que ça se termine mais de complexité trop grande pour être applicable en pratique. Les heuristiques (qui sont justement des algos validés par consensus, c'est à dire pas forcément prouvés juste ou autre mais qui, par expérience, permettent de satisfaire le besoin) permettent juste d'obtenir un résultat plus rapidement en exploitant des propriétés particulières, quitte à introduire quelques erreurs ou incertitudes qui restent acceptables.
Et pour être clair : on parle d'une heuristique quand on n'a pas démontré que l'algo permet d'obtenir nécessairement le bon résultat. Ça ne veut pas dire qu'on ne peut pas le démontrer. On peut le faire plus tard, ce qui amène le cas échéant à comprendre pourquoi ça marche.
Ensuite j'aimerais clarifier un point : il ne faut pas mélanger technique et science. Faire du logiciel, ce n'est pas faire de la science. On peut faire de la science à propos des logiciels, mais un développeur n'est pas un scientifique. S'il est vrai que le domaine logiciel est très facile à formalisé en général, ça ne fait que le qualifier de domaine formel, et non scientifique. En fait il se trouve qu'on a la partie formelle (ou fondamentale, comme vous voulez) et la partie appliquée (tout ce qui touche à l'implémentation et ses déboires). Ce n'est pas parce qu'une partie du travail de dév peut être démontrée que c'est une partie scientifique. La science, c'est ce qui a été démontré, pas ce qui peut l'être.
J'aime bien d'ailleurs dans ces cas là réintroduire un terme galvaudé : on a d'une part la prestidigitation, qui est le principe de l'illusion, de faire croire ce qui n'est pas, et de l'autre part la magie, c'est à dire ce qu'on ne s'explique pas. Pour moi, tout ce qui n'est pas expliqué par la science est de l'ordre de la magie. Y'a rien de chelou, pas d'étoiles qui virevoltent, c'est juste un terme fort bien adapté pour parler de ce qu'on n'est pas encore capable d'expliquer. Au niveau logiciel, y'a rien de "magique" (l'expression prend tout son sens du coup) car tout se base sur des théories scientifiques bien établies, comme la théorie de l'information. Il peut y avoir certaines incertitudes pour des raisons pratiques (e.g. erreurs sur des bits à cause d'interférences) mais on a établit les outils qu'il faut pour ça (algos de correction d'erreur) pour se retrouver dans une situation qui est très proche d'un domaine formel où tout se passe quasiment comme dans la théorie. Il n'en reste pas moins que ça ne transforme pas un dév. en scientifique, ni son travail.
On peut, mais ça coûte cher. Donc en général on limite ça aux parties critiques. J'ai l'habitude de voir ça avec les avions. La météo c'est que ça aussi : de la simulation en veut tu en voilà à partir duquel on en tire des probas de ce qui va arriver. Et non, si on vous dit la veille à la TV qu'il va pleuvoir, il ne faut pas vous sentir idiot de prendre votre parapluie quand même : ça peut quand même arriver, et vous vous sentirez beaucoup moins idiot si effectivement ça arrive.
Mais oui les preuves formelles ça s'utilise dans des choses de tous les jours, même si l'utilisateur lambda se contente d'en utiliser les résultats.
Site perso
Recommandations pour débattre sainement
Références récurrentes :
The Cambridge Handbook of Expertise and Expert Performance
L’Art d’avoir toujours raison (ou ce qu'il faut éviter pour pas que je vous saute à la gorge {^_^})
Et chose promise chose due : http://www.developpez.net/forums/d15...t/#post8570572
Site perso
Recommandations pour débattre sainement
Références récurrentes :
The Cambridge Handbook of Expertise and Expert Performance
L’Art d’avoir toujours raison (ou ce qu'il faut éviter pour pas que je vous saute à la gorge {^_^})
Non, un algo, ça peut se démontrer. Techniquement, ça s'appelle "démontrer la correction" d'un algorithme.
Dans le monde du routage par exemple, la démonstration de correction des algorithmes comme Dijkstra ou Bellman-Ford se fait par récurrence, ça n'est pas bien sorcier.
Steph
Juste pour dire : j'ai updaté la liste des Predatory Publishers à celle produite pour 2016 dans mon blog..
Et le bilan est effarant : 983 groupes de presse et 882 revues indépendantes considérées "predatory" !!!
@Neckara et autres : voyez, le "peer-reviewed" et les articles (et leur nombre) ne sont plus du tout un indicateur.... donc le "consensus".....
"Un homme sage ne croit que la moitié de ce qu’il lit. Plus sage encore, il sait laquelle".
Consultant indépendant.
Architecture systèmes complexes. Programmation grosses applications critiques. Ergonomie.
C, Fortran, XWindow/Motif, Java
Je ne réponds pas aux MP techniques
Comme on l'a déjà dit, pour nous le consensus est plus complexe que cela.@Neckara et autres : voyez, le "peer-reviewed" et les articles (et leur nombre) ne sont plus du tout un indicateur.... donc le "consensus".....
Vous avez un bloqueur de publicités installé.
Le Club Developpez.com n'affiche que des publicités IT, discrètes et non intrusives.
Afin que nous puissions continuer à vous fournir gratuitement du contenu de qualité, merci de nous soutenir en désactivant votre bloqueur de publicités sur Developpez.com.
Répondre avec citation
Partager