We describe a technique enabling a logic program to perform lazy rewriting.
Our technique is based on a transformation of a
rewrite system in a set of Horn clauses.
We characterize syntactically, in terms of a hierarchical
structure of the rewrite rules of an operation,
the systems accepted by our transformation
and outline a design technique yielding systems with these characteristics.
We define our transformation,
prove its correctness and other properties,
and relate the efficiency of resolution to that of rewriting.
Improvements over previous similar efforts include
using a more expressive and more powerful language,
generating a more efficient logic program,
providing efficient operational completeness,
and establishing a tight bound on the length of a resolution
as a function of the length of a corresponding reduction sequence.
We compare our approach with several related efforts
and discuss examples which also show
the integration of lazy with eager evaluation and
the possibility of narrowing in addition to rewriting.