Promoting rewriting to a programming language: a compiler for non-deterministic rewrite programs in associative-commutative theories

First-order languages based on rewrite rules share many features with funct ional languages, but one difference is that matching and rewriting can be m ade much more expressive and powerful by incorporating some built-in equati onal 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 independe nt from the rewriting language, and may be useful to build a compiler for a ny system using rewriting module Associative and Commutative (AC) theories. An algorithm for many-to-one AC matching is presented, that works efficien tly for a restricted class of patterns. Other patterns are transformed to f it into this class. A refined data structure, namely compact bipartite grap h, allows encoding of all matching problems relative to a set of rewrite ru les. A few optimisations concerning the construction of the substitution an d of the reduced term are described, We also address the problem of non-det erminism related to AC rewriting, and show how to handle it through the con cept of strategies. We explain how an analysis of the determinism can be pe rformed at compile time, and we illustrate the benefits of this analysis fo r the performance of the compiled evaluation process. Then we briefly intro duce the ELAN system and its compiler, in order to give some experimental r esults and comparisons with other languages or rewrite engines.