Summary: We introduce a novel representation for associative-commutative (AC) terms which, for certain important classes of rewrite rules, allows both the AC matching and the AC renormalization steps to be accomplished using time and space that is logarithmic in the size of the flattened AC argument lists involved. This novel representation can be cumbersome for other, more general algorithms and manipulations. Hence, we describe machine efficient techniques for converting to and from a more conventional representation together with a heuristic for deciding at runtime when to convert a term to the new representation. We sketch how our approach can be generalized to order-sorted AC rewriting and to other equational theories. We also present some experimental results using the Maude 2 interpreter.
For the entire collection see [Zbl 1029.00060].