Redex Capturing in Term Graph Rewriting
William M. Farmer, Ronald J. Watro
1990
Abstract
Term graphs are a natural generalization of terms in which structure
sharing is allowed. Structure sharing makes term graph rewriting a
time- and space-efficient method for implementing term rewrite
systems. Certain structure sharing schemes can lead to a situation in
which a term graph component is rewritten to another component that
contains the original. This phenomenon, called redex capturing,
introduces cycles into the term graph which is being rewritten -- even
when the graph and the rule themselves do not contain cycles. In some
applications, redex capturing is undesirable, such as in contexts
where garbage collectors require that graphs be acyclic. In other
applications, for example in the use of the fixed-point combinator Y,
redex capturing acts as a rewriting optimization. We show, using
results about infinite rewritings of trees, that term graph rewriting
with arbitrary structure sharing (including redex capturing) is sound
for left-linear term rewrite systems.
Keywords: Functional programming; Graph reduction; Infinite trees;
Mathematical foundations; Term graphs; Term rewriting systems.