Promoting Rewriting to a Programming Language: A Compiler for Non-Deterministic Rewrite Programs in Associative-Commutative Theories

Hélène Kirchner 1 Pierre-Etienne Moreau 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : First-order languages based on rewrite rules share many features with functional languages. But one difference is that matching and rewriting can be made much more expressive and powerful by incorporating some built-in equational theories. To provide reasonable programming environments, compilation techniques for such languages based on rewriting have to be designed. This is the topic addressed in this paper. The proposed techniques are independent from the rewriting language and may be useful to build a compiler for any system using rewriting modulo associative and commutative (\AC) theories. An algorithm for many-to-one \AC\ matching is presented, that works efficiently for a restricted class of patterns. Other patterns are transformed to fit into this class. A refined data structure, namely compact bipartite graph, allows encoding all matching problems relative to a set of rewrite rules. A few optimisations concerning the construction of the substitution and of the reduced term are described. We also address the problem of non-determinism related to \AC\ rewriting and show how to handle it through the concept of strategies. We explain how an analysis of the determinism can be performed at compile time and we illustrate the benefits of this analysis for the performance of the compiled evaluation process. Then we briefly introduce the \ELAN\ system and its compiler, in order to give some experimental results and comparisons with other languages or rewrite engines.
Type de document :
Article dans une revue
Journal of Functional Programming, Cambridge University Press (CUP), 2001, 11 (3), pp.207-251
Liste complète des métadonnées

https://hal.inria.fr/inria-00100926
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 14:52:56
Dernière modification le : jeudi 11 janvier 2018 - 06:19:57

Identifiants

  • HAL Id : inria-00100926, version 1

Collections

Citation

Hélène Kirchner, Pierre-Etienne Moreau. Promoting Rewriting to a Programming Language: A Compiler for Non-Deterministic Rewrite Programs in Associative-Commutative Theories. Journal of Functional Programming, Cambridge University Press (CUP), 2001, 11 (3), pp.207-251. 〈inria-00100926〉

Partager

Métriques

Consultations de la notice

88