Lazy Rewriting on Eager Machinery

The article introduces a novel notion of lazy rewriting. By annotating argument positions as lazy, redundant rewrite steps are avoided, and the termination behaviour of a term rewriting system can be improved. Some transformations of rewrite rules enable an implementation using the same primitives as an implementation of eager rewriting. 1 Introduction A term rewriting system (TRS) constitutes a mechanism to reduce terms to their normal forms, which cannot be reduced any further. A TRS consists of a number of rewrite rules ` ! r, where ` and r are terms. For any term t, such a rule allows to replace subterms oe(`) of t by oe(r), for substitutions oe. The structure oe(`) is called a redex (reducible expression) of t. A term can contain several redexes, so that the question arises which of these redexes should actually be reduced. There are two standard strategies: ffl innermost rewriting reduces a redex as close as possible to the leaves of the parse tree of the term; ffl outermost..