ELAN ou la programmation par réécriture
Résumé
La notion de réécriture est omniprésente en informatique, en logique ou en mathématiques. Elle peut être utilisée aussi bien pour déduire -on parle alors souvent de règle d'inférence- ou pour calculer -et on suppose souvent dans ce cas que la relation sous-jacente est noetherienne et confluente-. Il est en fait fondamental de pouvoir décrire non-seulement les étapes élémentaires de réécriture, c'est à dire les règles de réécriture, mais aussi comment elles sont enchainées. Il faut alors introduire le concept de stratégie qui doit permettre d'exprimer des calculs déterministes mais aussi, et c'est plus original, la recherche de bonnes dérivations. Cette présentation montrera dans un premier temps comment le langage ELAN donne la possibilité d'exprimer de façon uniforme règles de réécriture et stratégies et comment le compilateur ELAN permet de les exécuter très efficacement. Nous montrerons sur un exemple de protocole comment le langage nous permet d'écrire puis de prototyper des spécifications éventuellement non déterministes et comment la notion de stratégie permet leur vérification directe. Dans une seconde partie, nous introduirons le calcul de réécriture et nous montrerons comment il permet de donner une sémantique aux langages basés sur la réécriture. ELAN, sa documentation et des exemples d'utilisation sont disponibles à l'addresse www.loria.fr/ELAN.