lundi 4 janvier 2010

Hasard sur en ligne

Pour choisir quelqu'un entre parmi un groupe de n personnes, attribuez un numéro à chaque personne (par exemple par ordre alphabétique) entre 0 et n-1.

Allez sur http://www.fileformat.info/tool/hash.htm , choisissez un mot (pas nécessairement un vrai mot) et tapez le dans la première case, cliquez sur le bouton "Hash" et partagez le résultat de la ligne MD5 avec tout les joueurs sans avoir moyen de l'altérer[1].

Une fois que tout les joueurs ont notés le résultat, révélez le mot que vous aviez choisi. Comme le hash est publié, il est pratiquement impossible que vous mentiez ! Et les autres peuvent vérifier que vous n'avez pas menti en allant sur hash online et en essayant d'hasher votre mot.

Une fois que tous les mots sont connus, faite un très grand mot en mettant les mots cote à cotes dans l'ordre de vos numéros. (Par exemple si le joueur 0 a le mot "glace" et que le joueur 1 à le mot "chien" faites "glacechien"), et hasher le résultat. Cette fois, pour plus de faciliter, prenez le résultat de la ligne "adler-32", et tapez dans google 0xADLERRESULT%n où ADLERRESULT est le résultat donné par adler, et n est le nombre de participant. Google calculatrice vous rend alors le numéro du gagnant !

Note

[1] par exemple un email, ou un commentaire sur un blog que vous ne pouvez pas éditer

dimanche 20 décembre 2009

Reve complexe

Je sais pas pourquoi j'ai rêve ça tout à l'heure, et ça m'est resté au réveil.

Et si, pour une raison étrange et encore inconnue, la question P=?NP avait la réponse étrange suivante:

Pour tout algorithme polynomiale décidant un langage NP-complet, il est impossible de prouver qu'il est polynomiale et décide le langage. Autrement dit, quand bien même P=NP, et quand bien même on aurait un tel algorithme polynomiale, il serait impossible de prouver que cet algo est le bon...

En tout cas, ça assurerait encore du boulot pour les gens de complexité et d'algorithmique pour un bon bout de temps, ce serait bien... quoi que.


Oui, je fais des rêves bizarres.

vendredi 18 décembre 2009

Coq

Il existe un langage de programmation certifié qui s'appelle COQ, c'est très puissant car il est impossible d'écrire des programmes avec des bugs, mais c'est aussi très dur à écrire, au moins au début. Ce qui fait que à 2 heure du matin, je suis en train de bosser sur la première question d'un devoir pour l'université.

Je trouve que le fait que coq me tienne éveillé fait un très bon jeu de mot.

-- Arthur, qui continue de penser que, quand Goldman parle de "ses choses qui nous font veiller tard" il s'agit de la programmation.

samedi 31 octobre 2009

Cauchemar geek

Juste pour l'anecdote, je suis actuellement en train de participer à un concours d'informatique [1], ça me stresse tellement que j'en fais des cauchemars...

J'ai rêvé que j'écrivais du code avec des goto!

-- Arthur, qui est capable de prendre son clavier azerty sans fil et d'oublier le dongle pour le brancher!

Note

[1] ACM, à Madrid, pour ceux que ça intéresse

dimanche 23 août 2009

Appel à l'aide

Je suis actuellement connecté à un ordinateur, mais je ne sais plus du tout où je suis.

Si quelqu'un trouve un ordi lent, probablement salle S ou T, avec du gros calcul lancé par moi, merci de m'indiquer l'ordinateur.

Car franchement, ça sert à rien de lancer une semaine de calcul si je suis pas capable de lire le résultat.

Arthur, qui contribue au réchauffement des salles d'informatiques, vides, de son école.

samedi 1 août 2009

Je ne trouve pas mon bug

C'est très étrange, mon programme me dit:

Fatal error: exception Not_found

Et alors quoi? Moi ça me parait très bien si l'exception n'est pas trouvée, pourquoi est-ce une erreur fatale?

vendredi 31 juillet 2009

L'interet de mon travail

Voici une fois pour toute l'explication de mon job, pour un non informaticien.

Si vous avez déjà utilisé un ordinateur, vous savez qu'il arrive qu'il plante, et qu'il se passe des choses inattendue. Des "bugs". Les gens qui font du dépannage disent qu'il s'agit souvent d'une erreur de l'interface chaise-clavier[1]. Mais parfois, il arrive que ce soit vraiment le programme qui a été mal conçu. Moi je travaille sur un des logiciel conçus pour éviter ce genre de problème, pour s'assurer que quand vous ferez tourner un logiciel, il fera bien ce que vous voulez.

Ce qu'il faut savoir, c'est que quand un programmeur travaille, il dit à l'ordinateur comment faire, mais il ne lui dis pas quel résultat il attend. Dans le cas de alt-ergo on indique aussi ce qu'on veut comme résultat.

Un exemple simple, vous avez un robot qui fait la cuisine, et vous voulez manger des pates, vous auriez du dire:

  1. Prendre une casserole
  2. Remplir une casserole d'eau
  3. Mettre la casserole sur une plaque chauffante
  4. Allumer le feu de la plaque
  5. Attendre que l'eau bout
  6. Attendre 5 minute
  7. Éteindre la plaque
  8. Vider la casserole dans une passoire
  9. Mettre le contenu de la passoire dans une assiette
  10. M'apporter l'assiette.


Et hop, vous avez des pattes cuites dans votre assiette !

Enfin, c'est ce que vous auriez voulu, mais vous avez oublié de dire "mettre les pattes dans l'eau". Vous avez donc en fait une assiette vide.

Et alors, avec Alt-ergo[2], vous rajoutez l'information "But: Avoir des pattes mangeable dans l'assiette", et alt-ergo vérifiera pour vous[3] que vous aurez toujours le résultat attendu.

Ce processus peut-être assez complexe, mais est indispensable... imaginez que quelqu'un fasse le même genre d'erreur sur le logiciel qui s'occupe de la direction assisté de votre voiture.

Moi, là-dedans, je travaille juste sur un petit morceau du vérificateur, mais il n'est pas vraiment possible que j'explique plus en détail ce que je fais à quelqu'un qui ne fait pas d'informatique.

Notes

[1] l'utilisateur

[2] via frama-c, why ou une autre plateforme

[3] en tout cas quand il fonctionne

jeudi 23 juillet 2009

Travail en parti fini

Cher lecteur, je tenais à partager avec toi ma joie.

Je t'ai déjà parlé un peu de mon travail, et bien sache que j'ai fini d'implémenter ce que j'avais à implémenter, et que ça fonctionne.

C'est même plus efficace qu'avant, en effet, sur un exemple, parait-il typique, le temps total du programme est passé de, tiens-toi bien, 0.388 secondes à 0.352 secondes. Il y a 26 millième de seconde de gagné grâce à ce laborieux travail d'un mois et demi.

Bon, maintenant, j'ai encore plusieurs possibilité, chercher si il n'y a pas ici où là des morceau de code améliorable, par exemple en transformant mes AVL en table de hachage, en utilisant plus de hashconsing, que sais-je. Ou alors, je peux lire des articles pour connaitre mieux l'état de l'art. Ou encore commencer le rapport de stage. Ou bien avoir une vie

Bonne nuit

dimanche 12 juillet 2009

Typage de cinglé

Je préviens tout de suite, ceux qui ne programme pas ne seront pas intéressé par ce billet. Ceux qui ne connaissent aucun programme ML, (oCaml, Caml Light, Haskell,...) vous risquez d'être largué.

Il y a des cinglés, qui vouent une vénération au typage. Par exemple, un de mes ancien professeurs a écrit sur sa page I see a future where all programming is done in type safe languages or in assembly supplemented with safety proofs..

Le typage doit permettre de garantir certaine propriété. Je vais vous donner l'exemple le plus cinglé que j'ai, trouvé récemment. Je me demande si ça ne mériterait pas un dailyWTF peut être.

Là où je travaille, on a des termes, qui sont soit des variables (exemple: x, y, taille, etc.) soit des constantes (exemple: 42, pi, "hello world"), soit des application, i.e. un symbole de fonction appliqué à des termes (exemple: f(42), +(1,3), print("hello world").

On appelle ground term un term qui ne contient aucune variable. Il est très simple de typé un ground terme, c'est simplement, soit une constante, soit un symbol et une liste de ground terme (ses arguments)

Il est aussi simple de typer un terme quelconque, qui est soit une variable, soit une constante, soit une application.

Maintenant, vient le problème suivant: on veut des termes avec au moins une variable, comment s'assurer le respect de cette propriété par le typage?

Réponse: On crée un type supplémentaire: variable-term, qui est: soit une variable, soit un quadruplet composé d'un symbol de fonction, d'un entier, d'un variable-term et d'une liste de terme.

Si l'entier est i, alors, moralement, cela signifie que le ième terme est le variable-term, ce qui nous assure qu'on ait bien une variable quelque part. (Preuve triviale par récursion sur le terme). Et on décale de 1 la position de tous les termes au delà du ième, dans la liste.

Donc f,2,taille,("hello world",42,pi) signifie moralement f("hello world",42,2,pi).

Alors, c'est bien joli, mais ça devient très moche à utiliser. Mais le typage est sauf! Les cinglés sont contents, et moi je pense bientôt aller à l'asile si je continue à voir des choses comme ça.

Arthur Rainbow

PS: Le cinglé qui a eu l'idée de faire comme ça, c'est moi, mais le pire c'est que mon maitre de stage a trouvé que c'était une bonne idée, et a songé à effectivement implémenté les variables-terms comme ça maintenant.

PPS:Il y a quand même un problème qui reste, que seul le typage dépendant pourrait résoudre, mais pas le typage des langages ML, quelqu'un saura t'il me le trouver?

Mon travail

Cet été, comme je l'avais déjà dit, je travaille.

On me demande d'améliorer un morceau d'un code. Et là c'est fait. :D

Prenons un exemple, j'ai un morceau de code sur les listes à faire valider, la partie que je dois améliorer prenait 3 secondes, maintenant ça prend un dixième de seconde.

L'amélioration n'est pas négligeable (si on ne tient pas compte du fait que ça m'a pris un mois et une semaine pour 2,9 secondes).

Première question, pensez vous que mes maitres de stages seront content?

Maintenant, sachant que mon code rend toujours la même réponse qui est "non", mais quand il devrait rendre oui, répondez de nouveau à la même question.

Remarquez que pendant un moment, mon code fonctionnait, avant que je ne tente de rajouter une fonctionnalité. Et je n'arrive pas à comprendre pourquoi cette fonctionnalité bug.

Mais ce qui m'inquiète le plus, c'est que je ne suis pas sur d'avoir compris pourquoi ça fonctionnait avant.

Arthur Rainbow qui pense que les cours d'algorithmique où il suffisait de trier des listes, c'était le bon temps.

dimanche 21 juin 2009

J'ai mal à la tête

J'ai songé à une petite amélioration de l'algorithme de l'article dont je parlais l'autre jour. Je pense que rien qu'à lire ce qui va suivre, tu vas comprendre que j'ai mal à la tête là.

J'utilise une table de hashage a pointeur faible prenant des structures de E-graph basé sur un union-find et rendant des tables de hachages qui prennent un couple composé d'un symbole et d'un ground-terme (terme sans variable) et qui rend une table de hachage servant d'ensemble de patterns(ou triggers).

Derrière tout ça, j'utilise du hashconsing, pour faciliter un peu le tout et et gagner en espace.

Si tu as suivies, je te félicite, moi je suis déjà perdu, et je rien qu'à comprendre la structure de donnée que je devais utiliser, j'ai pris deux heures. Et là j'ai le cerveau qui fond et j'ai peur de ce que ça va donner quand je passerai vraiment à programmer ça. Ça va être atroce.

Fort heureusement, j'ai un bon langage, et vive objective Caml

vendredi 19 juin 2009

Bonne chance à Microsoft

Je viens de découvrir qu'il existait chez Microsoft un laboratoire Software Reliability Research. Je leur souhaite bonne chance et du courage, je crois que Microsoft a bien besoin d'eux.

Surtout que si vous regardez la page, ils sont quand même 12, après ça, on ne pourra pas dire que Microsoft ne met pas les moyens nécessaire pour s'assurer que leurs programmes fonctionnent bien[1].

Il se trouve que pour mon stage dans l'équipe Proval à l'Inria, mon travaille depuis début juin consiste à implémenter un algorithme décrit dans un article Efficient E-matching for SMT Solvers écrit par un membre de ce laboratoire.

Pour un papier de 18 pages, où les deux premières et deux dernières donnent le contexte, imprimé en recto-verso, ça veut dire que depuis 3 semaines, je travaille sur 7 feuille A4. Au moins, le papier est très rentable ici! Je prend un jour et demi pour lire un coté d'une feuille! et je ne suis pas encore totalement sur de bien avoir compris la fin.

Certains points m'ont posé problèmes, il y avait quelques fautes dans l'algorithme sur papier[2], par exemple, une fonction à 5 argument à qui ils donnent 4 argument, une fonction qui n'est pas défini dans un cas qui pourtant se produit.

Le pire étant la faute qui donne un mauvais résultat, mais qui compile bien, et qui ne donne même pas de problème à l'exécution. Ici il s'agit d'un {} à la place de { {} } . Ou en français, si les symboles ensemblistes ne sont pas clair pour vous, ils ont marqué "l'ensemble de substitution, vide", au lieu de marquer "l'ensemble de la substitution vide"... ou plutôt en anglais "the empty set of substitution" à la place de "the set of the empty substitution"...

Oui, c'est pas clair je le sais... pour moi ça ne l'était pas non plus. Dans le doute, j'ai voulu aller voir ce que l'auteur avait fait dans son code à lui. Mais c'était ridicule, chercher du code ouvert sur le site de microsoft, je devais délirer pour avoir tenter de faire ça.

Enfin, fort heureusement, l'auteur à qui j'ai écrit m'a confirmé que les 4 corrections que je lui ai soumis était juste. Et ça, c'est le genre de petit truc qui peut faire bien plaisir à lire. Même qu'il a dit qu'il corrigera le papier sur son site[3]. Peut-être que ça va vraiment aider, c'est ce qui pousse tant de monde à contribuer au monde du libre, même si c'est bénévolement... Quoi qu'est-ce que j'ai dit? Libre? A flute, je savais que ça clochait quelque part. Parce que par contre, pour la question bénévolement... C'est triste de se dire que j'étais plus payé quand je faisais de la figuration[4] pour France 2. Je ne vous donnerai pas mon salaire, vos patron serait jaloux de voir des gens travailler pour si peu. Quoi que, en fait, si, je suis payé en crédit par l'école, pour valider la licence et par les connaissance que j'accumule. Enfin je suppose.

Notes

[1] Quoi, moi, ironique, non?

[2] Non, je ne dirai pas qu'avec Microsoft il fallait s'y attendre... Je ne le dirai pas.. Ah trop tard! Mais de la part de quelqu'un qui n'a jamais écrit d'article, la critique est facile.

[3] Pour rappel, quand B. Gates a vendu dos à IBM, ce n'était pas fini, il a dit que son système serait bientôt fini et correct. Alors il ne reste qu'à attendre.

[4] Oui, le lien, c'est bien un photo de moi, j'avais 19 ans. C'était mes vrai cheveux, mais les habits ne m'appartenaient pas.

jeudi 4 juin 2009

Mon premier article sur wikipédia

Étant dans l'incapacité de trouver facilement des renseignement sur une structure de donnée dont j'ai besoin, mais qui semblait devoir être connu dans l'article que je lis actuellement, vu qu'ils l'utilisaient sans expliquer ce que c'était, je me suis dis que ce serait une bonne idée de faire un résumé sur wikipédia.

Voici donc le premier article que j'y ai intégralement écris, sur les [e-graphes].

Arthur, qui a peut être fait avancer la connaissance universel, mais alors d'un pas de fourmi!

lundi 1 juin 2009

Algorithme nase

En dehors d'écrire des mauvaises blagues sur ce forum, et jouer un spectacle tous les 32 du mois, je suis théoriquement étudiant en informatique. J'aimerai partager avec vous une déconvenue qui m'énerve un peu. Parce que si vous lisez, on sera plus à perdre du temps sur une mauvaise idée, et on se sent mieux quand on est pas seul à faire des trucs bêtes.

Il a été posé sur le forum de l'école la question suivante:

Si on appelle produit d'un ensemble le produit de ses éléments, et si on dit que la valeur d'un sous-ensemble S de E est la somme du produit de S et du complémentaire de S, alors est-il possible de trouver pour chaque ensemble de cardinal pair le sous-ensemble de valeur minimal en temps polynomial.

Vous suivez? Sinon plus clairement, on a une liste de nombre avec un nombre pair d'élément. Par exemple 1, 2, 3, 4, 5, 6, et il faut choisir la moitié de ces nombres. Par exemple si on choisit 1,2,3 alors la valeur est (1*2*3)+(4*5*6)=6+120=126. Alors on cherche à diminuer cette valeur. Ici ce n'est pas bon, par exemple, si on prenait 1,2,6 alors on aurait la valeur (1*2*6)+(3*4*5)=12+60=72 qui est plus petit que 126.

On peut essayer de regarder la valeur de tous les choix de nombre bien sur, mais ça prend énormément de temps, plus exactement un temps factoriel. Donc c'est iréalisable pour les listes de 100 nombres par exemple. Ou alors avec des années de calcul.



J'y ai pensé quelque temps, et me suis dit que ça devait pouvoir marcher avec un algorithme glouton. On créé au fur et à mesure le sous ensembles E et son complémentaire C, avec au départ deux ensemble vide. Pour chaque nombre qu'on voit, on le rajoute à E si le produit de E est inférieur au produit de son complémentaire.

Par exemple, au départ on a E={} et C={}, On a 6 à placer quelque part, par exemple E, alors E=6, C={}, le produit de E est 6, alors que celui de C est 1 (car C est vide), donc le prochain nombre, 5, sera rajouté dans C. On a E=6, C=5. Là puisque 5 est plus petit que 6, le prochain nombre, 4, est rajouté dans C, alors E=6 et C=5,4, le produit de C est alors 5*4=20, et le prochain est rajouté en E, donc on a E=6,3. A la fin, on a comme sous ensemble E=6,3,2. Et la valeur est donc (6*3*2)+(5*4*1)=36+20=56, qui est d'ailleurs inférieur au 72 qu'on avait trouvé tout à l'heure. Donc on est en bonne voie.

A priori, l'idée est bonne, à chaque fois qu'on doit placer un nombre, on multiplie dans l'ensemble où le produit est aussi petit que possible, comme ça on évite de faire monter la valeur. Bien sur, il faut s'arrêter quand on a mis dans l'ensemble ou son complémentaire la moitié des éléments, il ne faut pas en mettre trop.

Le seul problème, c'est que je n'arrive pas à trouver de preuve pour montrer que cet algorithme donnera toujours la meilleur solution ! J'ai beau retourné le problème dans ma tête, regarder par récurrence, à l'aide de matroide, ou pourquoi pas de potentiel (mais ça serait surprenant que la méthode du potentiel fonctionne)

Bien sur il y a la possibilité que cet algorithme soit simplement mauvais, en attendant, pour vérifier si ça pouvait marcher, j'ai programmé (en oCaml) cet algorithme, et j'ai vérifié pour quelques ensembles si on obtenait effectivement la meilleure solution. J'ai comparé en testant sur tous les choix de sous-ensembles possible. Et là je vois que le meilleur sous ensemble c'est 6,4,1 car alors la valeur est (6*4*1)+(5*3*2)=24+30=54. Donc mon algorithme a raté ! J'ai donc perdu pour rien au moins une heure à programmer, et plus à chercher à prouver cette algorithme qui était faux !

Et encore au moins une demi heure à taper ce billet.

Sniff

dimanche 3 mai 2009

Normalisation forte du lambda-calcul simplement typé.

Je suis pas sur que ça intéressera quelqu'un, mais voici un problème que je me pose depuis hier. Au pire, ça me fera des notes pour plus tard.

Je reste persuadé, depuis hier après-midi, qu'il doit être possible de prouver que le lambda-calcul fortement typé normalise fortement à l'aide d'un bon ordre sur les termes typable. Plus précisément, je pense que l'ordre des multi-ensemble doit pouvoir être utilisable. Quand on fait une bêta-réduction (lambda x. t)v->t[x:=v] alors l'élément "lambda x" disparait, et v apparait plusieurs fois. C'est typiquement un cas où si v est un élément plus petit que "lambda x" alors on pourrait se retrouver avec un multi-ensemble inférieur.

Pour simplifier, on peut supposer qu'il n'y a pas de variable libre dans le terme typé et qu'on ne considère que les bêtas-réductions.

Sauf que bien sur, je n'arrive pas à trouver ce bon ordre de base, ni quel multi-ensemble prendre. Si on choisit de faire un multi-ensemble des variables, alors l'ordre des variables et loin d'être évident, et même si on suppose que chaque abstraction possède un paramètre formel x différent, après une réduction, ce paramètre est recopié. Alors on peut renommer les paramètres afin que chaque variable soit différente, mais dans ce cas il y a des fortes chance qu'on perde le bon ordre, puisque le nombre de variable qu'on peut écrire n'est à priori pas borné.

De toute façon, ça ne pouvait pas marcher, puisque ça ne tenait pas compte des types, et qu'il est connu que le lambda-calcul non typé ne normalise pas.

Un multi-ensemble des types des sous-termes pourrait être très bien, ou l'ordre de base est F=>G >F et F=>G >G. Sauf que si on a (lambda x.t):F=>G, v:F et donc (lambda x.t)v:G alors on retire un F=>G du multi-ensemble et on rajoute potentiellement plein de fois les types des sous-termes de v. Ça tombe bien, c'est là la force de l'ordre d'un multi-ensemble. Seul bémol, mais j'ai mis du temps à m'en rendre compte, rien n'empêche que v ait un sous-terme de type F=>G.

J'ai essayé d'autre truc, mais pour le moment rien de bien...

En gros, depuis mon réveil à 3 heure du matin, et maintenant 8 heure, j'ai passé une bonne parti de mon temps à réfléchir à ça, et la nuit n'avait pas porté de bon conseils...

Si par le plus grand des hasard, quelqu'un sait pourquoi cette méthode ne pourrait pas marcher (et de préférence, autre que: si ça marchait, quelqu'un y aurait déjà pensé), je suis tout à fait preneur. En tout cas, je trouve la question rigolote.

samedi 21 février 2009

C'est joli un graphe hamiltonien. Non?

Si je vous dis que je cherche à obtenir un cycle hamiltonien d'apparence aléatoire sur un graphe dont les nœuds appartiennent à [[1,n]]^3, où les arrêtes relient les nœuds dont la distance euclidienne est 1, alors si vous êtes un matheux, vous me direz que n doit être pair, et sinon vous risquerez de fermer la fenêtre avant la fin de ce paragraphe.

Donc, je vais vous le faire en français. Imaginez que vous faisiez un gros cube à partir de plein de petit cube. Maintenant, dans ces cubes, mettez un tuyau rentrant d'un coté et sortant de l'autre. Soit un tuyau droit, soit un tuyau en coude. On a autant de petit cube qu'on veut de chaque sorte, le but du jeu est que tous les tuyaux soient reliés et que ça se ferme sur soit même. (Donc l'eau tournerait en rond, ne pouvant ni rentrer ni sortir)

Maintenant, on ne garde que les tuyaux, le but du jeu est que on ait l'impression qu'ils soient posé de manière quelconque, n'importe comment.

Laissez moi vous dire que ce n'est pas évidant.

Un petit exemple se trouve ici avec 4 petit cube sur le coté. Et avec 10 cubes, c'est ici, mais pour le moment, il y a quelques petits cubes qui ne servent pas, vous pouvez les repérez grâce aux points noirs... Si vous voulez supprimez ces points noirs, bonne chance!

page 2 de 2 -