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

Les techniques de réécriture ont été développées depuis les années 1970 et appliquées en particulier au prototypage des spécifications formelles algébriques et à la démonstration de propriétés liées à la vérification de programmes. ELAN est un système qui permet de spécifier et d'exécuter des résolveurs de contraintes, des démonstrateurs et plus généralement tout processus décrit par des règles de transformation. Il possède des opérateurs associatifs-commutatifs (AC) et un langage de stratégies qui permettent une gestion fine de l'exploration d'un arbre de recherche et une manipulation aisée d'opérateurs mathématiques tels que les connecteurs booléens, les opérateurs arithmétiques ou les opérateurs de composition parallèle par exemple. Ces deux notions améliorent grandement l'expressivité du langage mais introduisent un double non-déterminisme lié à la possibilité d'appliquer plusieurs règles, de différentes façons, sur un terme donné. Cela rend difficile et généralement peu efficace leur implantation. L'objectif principal de cette thèse est d'étudier des techniues de compilation qui améliorent l'efficacité de ce type de langages. Nous proposons un nouvel algorithme, à base d'automates déterministes, pour compiler efficacement le filtrage syntaxique. Nous définissons ensuite différentes classes de règles pour lesquelles nous proposons un algorithme efficace de filtrage AC. Cet algorithme utilise une structure de données compacte et les automates définis précédemment, ce qui améliore considérablement les performances du processus de normalisation dans son ensemble. L'étude du langage de stratégies conduit à implanter des primitives originales de gestion du backtracking et à définir un algorithme d'analyse du déterminisme permettant de réduire leur usage et d'améliorer encore les performances, tout en réduisant l'espace mémoire nécessaire. Enfin, l'implantation des méthodes proposées a donné lieu à l'élaboration de nombreuses optimisations théoriques et techniques qui peuvent être largement réutilisées pour implanter d'autres langages de programmation par réécriture. Cette thèse présente les algorithmes et leur évaluation, l'architecture et le fonctionnement du compilateur, ainsi qu'une proposition d'environnement de spécification, fondée sur l'utilisation d'un format intermédiaire.Non disponible/Not availabl