Compilation de règles de réécriture et de stratégies non-déterministes

Les techniques de reecriture ont ete developpees depuis les annees 1970 et appliquees en particulier au prototypage des specifications formelles algebriques et a la demonstration de proprietes liees a la verification de programmes. ELAN est un systeme qui permet de specifier et d'executer des resolveurs de contraintes, des demonstrateurs et plus generalement tout processus decrit par des regles de transformation. Il possede des operateurs associatifs-commutatifs (AC) et un langage de strategies qui permettent une gestion fine de l'exploration d'un arbre de recherche et une manipulation aisee d'operateurs mathematiques tels que les connecteurs booleens, les operateurs arithmetiques ou les operateurs de composition parallele par exemple. Ces deux notions ameliorent grandement l'expressivite du langage mais introduisent un double non-determinisme lie a la possibilite d'appliquer plusieurs regles, de differentes facons, sur un terme donne. Cela rend difficile et generalement peu efficace leur implantation. L'objectif principal de cette these est d'etudier des techniues de compilation qui ameliorent l'efficacite de ce type de langages. Nous proposons un nouvel algorithme, a base d'automates deterministes, pour compiler efficacement le filtrage syntaxique. Nous definissons ensuite differentes classes de regles pour lesquelles nous proposons un algorithme efficace de filtrage AC. Cet algorithme utilise une structure de donnees compacte et les automates definis precedemment, ce qui ameliore considerablement les performances du processus de normalisation dans son ensemble. L'etude du langage de strategies conduit a implanter des primitives originales de gestion du backtracking et a definir un algorithme d'analyse du determinisme permettant de reduire leur usage et d'ameliorer encore les performances, tout en reduisant l'espace memoire necessaire. Enfin, l'implantation des methodes proposees a donne lieu a l'elaboration de nombreuses optimisations theoriques et techniques qui peuvent etre largement reutilisees pour implanter d'autres langages de programmation par reecriture. Cette these presente les algorithmes et leur evaluation, l'architecture et le fonctionnement du compilateur, ainsi qu'une proposition d'environnement de specification, fondee sur l'utilisation d'un format intermediaire.