Experiments with partial evaluation domains for rewrite specifications

Abstract

We describe a method to improve the efficiency of normalization procedures for term rewriting systems. This improvement does not restrict the semantics of the term rewriting specification in any respect. In particular, the expressive power of term rewriting systems as a programming language for generic programs and as a theorem prover has been preserved. Our method is based on the following observation. Many rewrite specifications are instances of theories for which efficient data structures exist. In that case we can exploit the canonical representation of objects of such a data structure by translating terms to corresponding objects, and retranslating these objects to terms (in normal form). We will call an implementation of a data structure that allows for this kind of transformations for all (not necessarily ground) terms an evaluation domain. This is then extended to the case where only part of a rewrite specification can directly be transformed using an evaluation domain. We develop the semantical requirements for such evaluation domains and discuss how evaluation domains can support the normalization process. We propose language extensions necessary for term rewriting software to take advantage of evaluation domains. Many experiments with an implementation based on the ReDuX term rewriting laboratory emphasize the efficiency of our approach.