Développeur : Sortie de la version 2.5 du langage Tom
Posté par paul brauner (). Modéré le 13 juillet 2007.
Tom est un langage de programmation développé au sein de l'INRIA et qui ajoute des capacités de réécriture à des langages de programmation impératifs (actuellement Java, C et OCaml). Concrètement, cela signifie que Tom permet de décrire des transformations de structures de données par un mécanisme de filtrage (pattern-matching) puissant et de spécifier comment ces transformations s'appliquent à l'aide d'un langage de stratégie.
Ce style de programmation est particulièrement adapté à la manipulation d'arbres, comme des arbres XML par exemple, mais aussi des arbres représentant des programmes (cf. la dépêche de jeudi concernant CFE). Ces arbres peuvent être des structures de données du langage hôte (on pourrait par exemple fournir une description à Tom des arbres générés par CFE), ou simplement des termes algébriques à la Caml, pour lesquels Tom fournit une implémentation efficace en Java.
Il est activement utilisé par des équipes de recherche ainsi que des industriels pour :
- développer des compilateurs (comme le compilateur Tom lui-même) ;
- transformer à la volée du bytecode Java ;
- le développement d'un assistant à la démonstration ;
- la traduction de requêtes vers des bases de connaissance.
La documentation est exhaustive et à jour. Le compilateur est stable et mature. Il est accompagné des outils indispensables à son utilisation : greffon pour Eclipse, mode pour vim et tâche ant. Le tout est publié sous licences libres (GPL, APL et BSD).
![[en]](../images/en.png)
Page principale du langage Tom (788 hits)-
Page du projet sur GForge INRIA (183 hits)
-
Guided Tour (240 hits)
-
Tutoriel (344 hits)
-
Dépêche précédente (125 hits)
> Lire la dépêche (21 commentaires, moyenne: 2,7).
Vous avez demandé le commentaire #850894.
Run by 
Cette page a été générée par Templeet en 0.0683s (dont 0.007 de SQL).
Cette page est peut-être conforme xhtml 1.0.
Information sur le site.
Anubis et les "catégories bicartésiennes fermées"
Je suis récemment tombé sur le site du langage Anubis[1][2], et comme on parle pour une fois de langages et de maths ici, je ne résiste pas à la tentation de signaler ce langage très intéressant.
Alain Prouté, l'auteur d'Anubis (Prof à l'université Paris 13) développe un point de vue très tranché concernant les formalismes utilisés dans les langages comme Caml et Haskell (logique combinatoire).
Dans les systèmes logiques classiques, explique t-il, seul le produit (cartésien) et la puissance (composition de fonction) sont disponibles.
Dans le système utilisé pour Anubis, les catégories bicartésiennes fermées, on ajoute la somme.
Cela implique que les filtrages effectués dans le code sont vérifiés à la compilation, car le formalisme permet de s'assurer que les élements filtrés sont tous disjoint mais aussi que leur union soit égal à l'ensemble filtrés.
Cela permet d'éviter les exceptions sur filtrages.
De plus, en terme de performances, les filtres ne sont pas essayés les uns après les autres, mais seul le bon est choisi (comment ? j'en sais rien)
Dans [3], Alain Prouté revient sur la gueguerre de chapelle entre les lambda-calculistes et les catégoriciens, en défendant évidemment la deuxième voie.
Il propose carrément de jeter aux orties la correspondance de Curry-Howard !!!!
Dans sa futur version 2, Anubis deviendra le premier langage fonctionnel auto-prouvé (!), à la compilation.
Il en donne quelques explications ici [4]
TOM est basé sur du ro-calcul si j'ai bien compris, c'est quoi la différence avec le lambda calcul ?
[1] http://www.anubis-language.com
[2] http://fr.wikipedia.org/wiki/Langage_Anubis
[3] http://www.developpez.net/forums/showthread.php?t=38275&(...)
Alin Prouté = Dr Topos
[4] http://www.developpez.net/forums/showthread.php?t=46904&(...)
[^]Re: Anubis et les "catégories bicartésiennes fermées"
lapincompris.
[^]Re: Anubis et les "catégories bicartésiennes fermées"
hmmm
pas trop ouvert comme attitude :
"En fait la distribution est personalisée (c'est un système expérimental anti-pirates en vue d'une commercialisation éventuelle). C'est la raison pour laquelle l'inscription est nécessaire. Ce serait dommage de vous priver d'Anubis pour si peu de chose. Il est quand même gratuit."
... ouais ouais gratuit ... c'est cela ...
Je ne pense pas que ce soit une bonne chose de chercher à "commercialiser" des langage aussi experimentaux.
Il me semble au contraire plus intéressant de liberer completement
ces langages de manière permettre à une communauté de se créer dessus et à le faire réellement exister et se repandre.
Il me semble d'ailleur que nombres de langages se sont saborder en devenant "commerciaux" .
[^]Re: Anubis et les "catégories bicartésiennes fermées"
C'est pas sympa de saborder notre si belle grammaire française comme ça :'(
[^]Re: Anubis et les "catégories bicartésiennes fermées"
compilo pas libre, les sources pas disponibles et apparemment pas bootstrappé ...
et aucune référence vers des publis présentant la théorie sous-jacente ou les techniques de compilation.
ça fait pas réver :(
[^]Re: Anubis et les "catégories bicartésiennes fermées"
Je ne connais pas cette personne ni ce langage mais je ne comprends pas ce que "premier langage fonctionnel auto-prouvé (!), à la compilation" signifie.
Je ne comprends pas non plus ce que "jeter curry-howard à la poubelle" signifie. Est-ce que cela veut dire que le langage fonctionnel en question ne repose pas sur la théorie des types ?
Le rho-calcul est un lambda-calcul avec patterns, où l'on peut abstraire sur des patterns. Par exemple : (lambda P(x,y) . x P(a,b)) -> a.
L'idée au départ était de canaliser la réécriture au travers de stratégies exprimées dans ce calcul. On peut également le voir comme un calcul plus proche des langages usuels de programmation fonctionnelle que ne l'est le lambda-calcul.
Les originalités du langage sont la capacité à traiter les cas d'erreur (contrainte de filtrage non satisfaites) et la gestion du filtrage non unitaire (collection de résultats). Dans certaines de ses versions, il est muni d'un système de types (à la PTS) avec les meta-propriétés qui en découlent et il y a des versions qui typent les point fixes.
Pour plus d'infos : http://rho.loria.fr
[^]Re: Anubis et les "catégories bicartésiennes fermées"
Je ne connais pas cette personne ni ce langage mais je ne comprends pas ce que "premier langage fonctionnel auto-prouvé (!), à la compilation" signifie.
Le terme est en effet inexact.
Je te renvoi à ce document, qui est une conférence d'Alain Prouté à l'université de Marseilles.
http://www.math.jussieu.fr/~alp/luminy_05_2007.pdf
Quand à jeter curry-howard à la poubelle, cela provient de sa conviction que la théorie des topos est plus puissante que la théorie classiquement utilisée en Haskell, Caml, etc...
Je me suis planté de lien, aussi vais-je corriger mon erreur.
Il explique ici, pourquoi il faut abandonner Curry-Howard
http://www.developpez.net/forums/showthread.php?t=46904&(...)
Je cite :
"prétendre qu'il y a 'isomorphisme' (c'est à dire similitude parfaite) entre preuves et programmes conduit à concevoir des systèmes formels dans lequels aucune notion correcte de sous-ensemble ne peut être définie. C'est un fait dont les logiciens et théoriciens de l'informatique commencent tout juste à prendre conscience aujourd'hui. Des langages avec preuve comme LEGO ou COQ souffrent de ce problème, qui rend quasiment impossible la manipulation de sous-ensemble ou d'ensemble quotients. Il faut donc abandonner l'isomorphisme de Curry-Howard. La théorie des topos donne une bien meilleure modélisation de ces questions."
Pour une comparaison avec les systèmes de type d'Haskell et d'Anubis, il explique cela ici :
http://www.developpez.net/forums/showpost.php?p=513888&p(...)
En espérant t'avoir éclairé.
[^]Re: Anubis et les "catégories bicartésiennes fermées"
Mes bien chers collegues,
Bien qu'il soit difficile de confirmer ou d'infirmer, en une nuit, le fondement du systeme deductif du Professeur Prouté, les arguments qu'il avance afin d'ecarter la theorie des types sont fumeux.
Il semble evident que la plupart des arguments qu'il apporte n'ont aucun fondement :
page 5, section 2.1 :
"meme si la facon de demontrer un theoreme peut pour diverses raisons interesser le mathematicien, ce dernier ne se soucie aucunement de la facon dont un theoreme a ete demontre pour l’appliquer."
Les mathematiciens peuvent rester tres deconnectés du monde materiel. Ils ne se soucient donc pas forcement de l'adequation entre les preuves des theoremes et le monde reel. Au contraire, lorsque l'on veut "prouver" que tel avion n'explosera pas en vol, il faut rester beaucoup plus proche de l'implementation effective (le programme informatique). Il faut alors se soucier de la facon dont le theoreme est demontré (ce qui implique de se soucier du sens de demontrer un theoreme)
Il est evident que l'argument developpé par le Professeur Prouté n'est pas fondé et repose sur une interpretation philosophique de ce que doit etre une preuve mathematique
page 5, section 2.1 :
"Si pour appliquer un theoreme, il fallait tenir compte de la facon dont il a ete demontre, les mathematiques serait beaucoup plus complexes qu’elles ne le sont deja."
On peut (et dans certains cas, il faut) tenir compte de la facon dont un theoreme est demontre, ce que ne font generalement pas les mathematiciens. Il est evident que les mathematiques sont bien plus complexes que ce qui est decrit par les mathematiciens. Cet argument n'est pas fonde non plus.
page 6, section 2.3 :
"On n’ecrit pas non plus [des preuves] de la meme facon pour des mathematiciens chevronnes et pour des etudiants de premiere annee. [...] Les preuves supportent donc l’a peu pres, contrairement aux calculs, qui doivent etre beaucoup plus precis"
Qui peut definir la difference entre ce qu'est un calcul et ce qu'est une preuve ? Et si l'on ecrit plus (en quantité) pour les mathematiciens chevronnes, n'est-ce pas parce qu'ils demandent plus ? Et les etudiants ne sont-ils pas capable de chercher une preuve complete si ils ne sont pas convaincus par leur cours ?
Il est evident que l'argument developpé par le Professeur Prouté n'est pas fondé et repose sur une interpretation philosophique de ce que doit etre une preuve mathematique.
page 6, section 2.4
"Si les informaticiens avaient autant de chance que les mathematiciens, ils leur suffirait de lire les types des fonctions pour pouvoir les utiliser"
Parce qu'il suffit a un mathematicien de lire un enoncé "vrai" pour en avoir la preuve ? Tout cela depend bien evidemment du systeme deductif considere. Par exemple en Coq, un type peut definir complement le comportement d'une fonction.
page 9, section 3.2 :
"Le systeme de Martin–Lof est consistant. S’il ne l’est pas, il sera de toute facon sans interet. Il semble toutefois que sa consistance absolue ait ete prouvee par les methodes de la normalisation forte (Tait, Girard, Coquant,. . .)."
Le fait que sa non-consistance aneantisse son interet suffit-elle a prouver sa consistance ? Que signifie "consistance absolue" ??? La normalisation forte d'un systeme ne permet que de prouver sa consistance si l'on suppose le meta-systeme consistant. En bref, cette phrase ne semble pas avoir de sens.
(au fait, le mot francais est "coherent")
la suite dans le post suivant
[^]Re: Anubis et les "catégories bicartésiennes fermées"
La suite de mes commentaires sur le systeme deductif du Professeur Prouté :
page 11, section 3.2 :
Toutefois, quelle que soit cette facon, il n’en reste pas moins vrai que le theoreme de Diaconescu demeurera indemontrable [dans la theorie des types de Martin-Lof]"
(rappel : le theoreme de Diaconescu enonce que axiome du choix implique intuitionistiquement le tiers exclus)
A-t-on une PREUVE que ce theoreme n'a pas de demonstration dans la theorie des types de Martin-Lof ? Et si oui, cette preuve utilise quel systeme ? L'avis du Professeur Prouté semble bien tranché alors que bien des questions restent sans reponse.
page 12, avant la section 4:
"Le fond du probleme est donc me semble–t–il le fait que le systeme de Martin–Lof est en contradiction avec le principe de l’unicite du temoin, ou de l’indiscernabilite des preuves. Il en va de meme de tous les systemes de type “Curry–Howard”"
Il est facile de renoncer a toute la theorie des types sur un "me semble-t-il". N'est-ce pas plutot le principe d'indiscernabilite des preuves qui est en contradiction avec Curry-Howard que le contraire ?
On peut continuer ainsi en listant tous les arguments du Professeur Prouté qui ne reposent que sur des affirmations et des arguments purement philosophiques et subjectifs. Le refus de la theorie des types du Professeur Prouté ne tient donc pas.
En esperant t'avoir obscurci.
PS : les numeros de page et de section correspondent au document
http://www.math.jussieu.fr/~alp/luminy_05_2007.pdf
[^]Re: Anubis et les "catégories bicartésiennes fermées"
Bonjour,
Je suis Alain Prouté, auteur de l'article dont parle shount.
Si je réponds à ce message c'est surtout parce qu'il me semble qu'il contient plus d'attaques personnelles que d'arguments scientifiques. Pourquoi shount m'appelle-t-il ironiquement 'Professeur Prouté' et non 'Alain Prouté' comme cela aurait dû être le cas ? Tout cela ressemble fort à du dénigrement.
Il y a une chose qui est claire en tous cas. C'est que shount s'est contenté de feuilleter mon article avec le pouce.
Il est très facile évidemment de dénigrer le travail des autres quand on est assuré d'un parfait anonymat. En ce qui me concerne, on connait mon nom et mon prénom, et on peut facilement trouver sur le net ma photo, mon email, mon age et l'adresse de mon employeur.
Que shount ait le courage de se faire connaitre, et je répondrai à ses critiques (fort mal fondées d'ailleurs) point par point.
[^]Re: Anubis et les "catégories bicartésiennes fermées"
J'dis ça comme ça, mais si Schount vous nomme "Professeur Prouté" et non "Alain Prouté", c'est sans doute parce que dans le commentaire d'Ontologia qui parle de vous, on peut lire "Prof à l'université Paris 13".
Cela montre plutôt une marque de respect que d'appeler quelqu'un par son titre universitaire, non ?
Par contre vous auriez pu, vous qui semblez susceptible, faire attention à l'orthographe exacte de Schount (et pas shount) et utiliser une majuscule lors de l'utilisation de son nom.
Et au cas où des personnes se poseraient la question, non je ne suis pas Schount sous un autre pseudo.
Vivre libre ou mourir
[^]Re: Anubis et les "catégories bicartésiennes fermées"
En OCaml, le filtrage est aussi vérifié à la compilation : le compilateur affiche un warning si un cas n'est pas traité (ie. si leur union est différente de l'ensemble filtré). En Haskell ce n'est pas le cas par défaut à ma connaissance (pas avec GHC en tout cas), mais le travail de Neil Mitchell sur Catch[0] permet de vérifier qu'il n'y a pas d'erreur de filtrage à l'exécution, c'est à dire qu'un chemin du code ne mène pas à un cas non traité dans un filtrage non exhaustif.
[0] : http://www-users.cs.york.ac.uk/~ndm/catch/
[^]Re: Anubis et les "catégories bicartésiennes fermées"
En OCaml, le filtrage est aussi vérifié à la compilation
tout à fait, on ne devrait pas pouvoir te prendre une erreur de filtrage à l'execution sans avoir eu un warning lors de la compil'...