Axioplase ıɥs∀ a écrit 3057 commentaires

Cela dit, le FORMAT de CL, il est plutot velu…

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

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

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

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

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

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

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


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

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

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


Et si t'es au lycée et que t'aimes pas les maths, ne va pas faire d'info à la fac.

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

http://math.andrej.com/2007/09/28/seemingly-impossible-funct(...)

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

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

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


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

Ils sont trop forts :)

Si maintenant on peut même plus profiter du pas-vu-pas-pris…


for i in `ls *`: do echo $i; done

ça compte pour 1 ?


Y a-t-il des profils/sessions ? Aujourdhui, je travaille sur tel projet, donc je veux tel état immédiatement. Demain, je serai de retour sur un autre projet, donc je veux pas devoir tout lui réapprendre et être directement avec des scores adaptés.

Un journaliste qui a de la culture générale, c'est comme un footballeur avec un doctorat de philosophie…

Faudrait vraiment être con pour dire "tiens, et si je devenais journaliste ?". Si encore y avait un diplôme "idiot du village", on pourrait appeler un chat un chat, et tout le monde saurait interpréter correctement les dires de ces abrutis… J'en viens même à trouver le salaire des footballers justifié: eux au moins, ils donnent l'impression de faire des efforts (physiques, certes)…

C'était sans doute mieux avant. Mais aujourd'hui, les narrateurs sont les doubleurs des feux de l'amour, et les rédacteurs ont tous échoué au brevet des collèges.

Idéalement:
- tu n'aurais pas à convertir car ton document serait déjà dans un format standard.
- la conversion serait gratuite grace à une représentation uniforme du document en mémoire
- mettre 20s pour convertir un document mériterait sérieusement de réécrire l'algo (cela dit, mon OOo sur un P4 1.8Ghz met dans les 10s ou 15s à démarrer. Je testerai MS-Office sous wine si je trouve une version à emprunter…)


Le temps de boot est un point positif quand on est obligé de se taper l'utilisation d'un criss de traitement de texte (libre ou non, peu importe). C'est déjà insupportable en soi, alors si en plus faut attendre que monsieur ait fini de se charger et de calculer Ack(5,5), merci non…

> Je peux te sortir une liste de gens sur ce site, qui sont loin d'etre des fans de MS qui disent clairement que oui Office est meilleur qu'OOo , ca veut pas dire qu'ils vont acheter Office demain, ni qu'ils n'utilisent pas OOo.

Moi moi moi !
Après un journal (très moinssé) contre OOwriter, je me plains aujourd'hui des parties "presentation", "draw", et "charts"… L'un me fait souvent des puces pas indentées et pas alignées (pour une même profondeur), me redimensionne des objets et m'empêche de les redimmensionner ensuite… l'autre me fait des boites avec des dimensions précises au centimètre près, et le dernier est infoutu de me faire une échelle logarithmique ou de me tronquer des valeurs…

Alors, oui, patch, utilise pas si t'es pas content, etc, etc.
Mais en répandant OOo, vous répandez aussi mes problèmes.

J'ai laissé tomber Latex+Beamer ce mois-ci pour faire une présentation, et je morfle avec cet OOo… Heureusement, je n'ai pas à utiliser OOwriter (car là, hors de question d'abandonner Latex).


Tout ça pour dire qu'OOo, c'est pas pire, loin de là. Mais ça reste toujours aussi agréable à utiliser qu'une rape à fromage pour se faire masser. Je n'ai pas utilisé MsOffice2007, mais (à l'époque, pour mes besoins) la version 97 (98?) répondait à mes besoins, et rien qu'elle me soulagerait…

Je ne suis pas juriste non plus mais, si moi, client, je sais que je passe par eux et je connais les conditions, je ne me sens pas fraudé.
Et comme c'est bidirectionnel, je dois pouvoir répondre à la place de mon partenaire en disant "rien de ce que j'ai reçu n'était contraire à ma volonté ou mes attentes."

Donc je dis "pas de fraude en entrée, pas de fraude en sortie" -> pas de fraude tout court.

Sinon quoi, je pourrais (si j'étais client) porter plainte contre Free, Wanadoo ou autre car je considère que je ne voulais *pas* que leur routeur/box accède à mes communications, et ce de manière opaque qui plus est, car j'ai pas le code source, non ?

Et aussi, quand je reboote la box, les condensateurs ont encore de l'information valide, et je peux de nouveau porter plainte car j'avais éteint "en croyant qu'il n'allait pas maintenir les données".

Bref, le chat, c'est du P2P, donc je passe par où je veux, sans que les passerelles n'aient à me craindre. Cela étant, j'ai pas lu les CGU d' MSN (me faut-il acheter quoi que ce soit pour les lire ?)

Je serais curieux de voir ce que ça donne avec un bon JIT vers un langage de programmation (par opposition à la va-vite avec un langage de scripting) comme http://www.vlam.ca/compyle

Pour troller un bon dernier coup, je crois qu'il y a encore trop peu de langages qui offrent la facilité du scripting avec l'efficacité. Alors qu'on était conscient dès le début qu'un programme Perl ne serait pas une formule 1, j'ai l'impression qu'aujourd'hui les gens se plaignent que leur Ruby ou Python soit trop lent, et qu'ils ne se sont jamais rendu compte que c'est leur cerveau qui a été trop lent lors du choix du langage¹


¹: j'opte toujours pour le langage adapté au problème ; je crois que j'y gagne plutôt qu'à utiliser le même tout le temps "parceque c'est le meilleur".

Ultra rapide. Pour toute monade :

bind a pour type
bind :: monade a -> (a -> monade b) -> monade b
C'est a dire que ca prend un objet dans sa monade et une fonction qui sait manipuler l'objet et le mettre dans une boite. Et ca retourne l'objet modifié dans la boite.

return a pour type
return :: a -> monade a
Ca prend un objet, ca le met dans la boite.


Pour manipuler un objet dans une monade (dans une boite), t'es *obligé* de passer par bind, sinon ca type pas.
Et c'est tout, en fait…

Exemple: j'ai une boite avec un nombre, et je veux incrémenter le nombre:

-- le nombre
n = 41

-- le nombre dans sa boite
nDansUneBoite = return n

-- la fonction qui incrémente
incremente x = x+1

-- incremente nDansUneBoite
-- ca marche pas ! incrémente ne manipule pas des boites !

-- faut utiliser bind pour que ca type bien
-- incrementeDansUneBoite xDansUneBoite = bind xDansUneBoite incremente

-- zut ! incremente a pas le bon type, ca doit rendre une boite !
incrementeDansUneBoite xDansUneBoite = bind xDansUneBoite (\x -> return (incremente x))


Ca y est !
Tout ce que j'ai fait, c'est faire en sorte que ca type.


Ici, ma boite est une simple boite, mais on peut en fait *embarquer* plein de calculs dans la boite qui se feront quand la boite sera passée a bind. Par exemple, elle peut garder 2 valeurs et s'utiliser comme buffer (et elle te filera la valeur du tour d'avant), ou alors stocker plein de valeurs (et représenter une liste), etc, etc.

C'est vraiment une interface, et le code derrière, tu fais ce que tu veux. Mais c'est bien (tm) car *beaucoup* de concepts collent à cette interface, et on peut les combiner…

Euh, y a *rien* de dur avec les monades en haskell pour le coup.
La théorie derrière est pas fastoche, certes, mais dans la pratique, c'est juste une factorisation de code. Un design pattern, mais qui sert à rendre le code effectivement plus simple, concis, agréable…

Si tu comprends pas les monades en haskell, c'est juste que tu n'est pas fait pour les langages statiquement et fortement typés (car en pratique, si tu comprend le type des 2 fonctions "return" et "bind", ça va tout seul après…)

Ouais, je crois qu'elle va remplacer ma chère kaiska cette CSS…

Je ne me souviens plus, elles sont accessibles à long terme les CSS événementielles?
Je crois qu'elles sont mélangées avec les "usuelles". Ca pourrait valoir le coup de les séparer (sur 2 colonnes); les normales et les surprises.
Puis, tant qu'à faire, une capture d'écrans…

Bon, j'ai compris ce qu'il me reste à faire. Un rapport de bug, et un patch…

Ouais, enfin Haskell, je lis beaucoup d'âneries dessus…

Du code efficace en haskell, c'est loin d'être facile à écrire. Les programmes sur alioth sont souvent imbitables et super bas-niveau… Je code en OCaml et haskell depuis pas mal de temps, et même si GHC s'améliore sans cesse, je crois un bon programme haskell n'est pas à la portée du premier venu… Il sera certes pas dramatiquement lent, mais bien plus toutefois que l'on croyait, à cause de la paresse du langage qui va accumuler des données qu'il pourrait réduire comme on s'y attendait… (à tel point qu'il y a des fonctions pures non paresseuses fournies comme foldl'…)

Il manque surtout le côté aléatoire de l'échantillon…
Linuxquestions, ça fait peu de BSDiste, de windowsiens, et encore moins de "je me fous de l'OS".
Je serais plus tenté par ce sondage auprès des lecteurs de Lambda The Ultimate. Au moins, je me dirais que les gars savent pourquoi ils votent pour tel ou tel langage (en dépit du biais usuel genre "et en plus, je fais un doctorat sur telle propriété de ce langage")

Je ne suis pas sûr que l'âge d'un langage justifie le passage outre l'effet de mode.
Certes, python est vieux (1991 d'après wp), mais j'ai l'impression qu'il est célèbre et répandu depuis, disons, 5 ans ? J'ai connu Ruby avant, par exemple (avec un vieux GLMF).

J'ai un peu cette image de "Python c'est mieux car"
- C'est objet
- L'indentation ca limite les bugs
- Contrairement à Perl, j'arrive à lire du code

Ce à quoi je suis tenté de répondre
- et si j'aime pas *cette* approche de l'objet ? Je veux (ou pas) héritage multiple, multiple dispatch…
- Les parenthèses aussi, et en plus ça détermine l'indentation
- Pour lire Perl, faudrait l'apprendre aussi, avant d'en dire du mal comme ça.


Je trolle pas mal langage, et je reste persuadé que beaucoup de gens choisissent Python, Ruby, autre… avec de faux arguments. Souvent, le choix du langage pour ses facilités devrait se tourner vers Perl (facilité de traitement) ou Scheme (facilité de prise en main et d'extensibilité).
Si encore tu disais "J'aime python, car toutes les libs dont j'ai besoin sont déjà là", ca ferait sérieux. Mais sur le langage lui même, non, faut pas pousser. Pas de quoi casser trois pattes à un canard.

Ceci étant, il est probable que Python ne fasse que commencer son ascension ; après tout, java a bien percé lui aussi…

> la manière dont j'utilise le shell

Mal ?

Désolé, c'était trop tentant. :)


Allez, deux/trois petits rappels qui payent pas de mine:
!! : la dernière commande
!$ : le dernier paramètre de la commande précédente
!f : la dernière commande de l'historique qui commence par f

Et sinon, je propose (comme d'autres) à chacun de lire un peu les pages info de son shell pour découvrir des trucs géniaux (ou alors d'installer zsh si y a justement pas de trucs géniaux).

Oui mais non, presque.
Erlang et le "message passing", c'est plus des Acteurs que du Pi-calcul, mais bon.

J'avais pas remarqué que tu t'étais répondu.
Bon, la théorie qui s'applique à elle même, c'est une démarche co-inductive, mais pas forcément inutile.
Si on omet le spi-calcul dont tu parles (pour les protocoles cryptographiques), sache que les techniques de preuves d'equivalence dans le pi-calcul (et CCS avant), les bisimulations (quis sont construites par co-induction justement), sont utilisées aussi pour prouver l'intégrité de programmes au sens cryptographique, mais aussi l'equivalence de deux programmes (l'un optimisé l'autre non), ou encore te garantir qu'un programme marchera sur ton linux comme sur mon BSD (par des preuves de congruence). Et ces techniques de preuves découvertes grace aux "calculs de processus" s'appliquent aussi au lambda-calcul et à des languages de plus haut-niveau (genre haskell).

Je crois vraiment qu'on retouche terre. Pas tout le temps, certes. Puis tous les chercheurs ne sont pas d'excellents génies, donc t'as des publis moins bien que d'autres (et des gars qui *veulent* prouver leur conjecture dont on sait qu'elle ne mène à rien).

Pour moi, le PI calcul (avec ses variantes) est un modèle, et il y a encore pas mal à y étudier. Il y a beaucoup de demande ces temps-ci, car justement, ca modélise vachement bien des trucs en biologie et pas mal de bio-informaticiens ou simple biologistes s'y mettent. J'ai pas plus de détails car c'est pas mon trip…
Enfin, une invitation récente que j'ai reçue par une ML à laquelle je suis abonné:


** CMSB 2009
** The 7th Conference on Computational Methods in Systems Biology
** http://cmsb09.cs.unibo.it/

The CMSB (Computational Methods in Systems Biology) conference series was established in 2003 to help catalyze the convergence of modellers, physicists, mathematicians, and theoretical computer scientists (from fields such as language design, concurrency theory, program verification) with molecular biologists, physicians and neuroscientists interested in a systems-level understanding of cellular physiology and pathology.

J'étais loin de penser à ça quand j'étudiais le PI-calcul en classe…

en mode normal, j'ai mappé "hjkl" sur "tsrn" et inversement. Le reste, j'ai gardé de base.
J'ai aussi mappé en mode commande W sur w! et Q sur qa! ce qui permet de gagner un peu de temps.

Je pense que je vais utilser les touches "pas gwerty" comme "éè«»" pour mapper dessus d'autres raccourcis.
En tout cas, garder la position hjkl est le plus important.
Ensuite, je ne sais pas si vim (ou son utilisateur) a plutôt intérêt à être consistant et mapper telle commande sur telle touche (azerty vs qwerty), ou à être consistant et mapper telle commande à telles position du clavier ("azerty over bépo")

Le pi-calcul, c'est un modèle, pas un langage de prog. Comme le lambda-calcul. Certes, c'est Turing-complet, mais l'intéret est pas de faire des programmes mais de comprendre la sémantiques de langages, pratiques eux, qui reposent sur ces concepts.

Ensuite de quoi, il y a deux niveaux de théorie: celle qui s'applique à la pratique et qui te semble justifiée, et celle dont les résultats s'appliquent à leur tour à la théorie, que tu appelles (à tort) un échec.

Je dis à tort, car l'étude du pi-calcul (et des nombreux autres modèles de la concurrence) ont apporté de nombreux résultats intéressants et utilisables dans la vie de tous les jours. Mais, encore une fois, force est de constater qu'ils ne sont pas à la portée de tout le monde. C'est un fait, et c'est comme ça.

Trod de gens considèrent les résultats en informatique (et en maths) comme "dûs". 1+1=2 "bah oui". Et bien non, pas "bah oui". (et pour la petite note, des algèbres simples comme ça (groupes, idéaux, etc), ca s'utilise en info aussi, sauf qu'on a des programmes entiers à la place des nombres…)

Sous la menace, je fais l'intranet en smalltalk. Ça compte double non ? :D