| Summary: | Term graph rewriting provides a simple mechanism to finitely represent
restricted forms of infinitary term rewriting. The correspondence between
infinitary term rewriting and term graph rewriting has been studied to some
extent. However, this endeavour is impaired by the lack of an appropriate
counterpart of infinitary rewriting on the side of term graphs. We aim to fill
this gap by devising two modes of convergence based on a partial order
respectively a metric on term graphs. The thus obtained structures generalise
corresponding modes of convergence that are usually studied in infinitary term
rewriting. We argue that this yields a common framework in which both term
rewriting and term graph rewriting can be studied. In order to substantiate our
claim, we compare convergence on term graphs and on terms. In particular, we
show that the modes of convergence on term graphs are conservative extensions
of the corresponding modes of convergence on terms and are preserved under
unravelling term graphs to terms. Moreover, we show that many of the properties
known from infinitary term rewriting are preserved. This includes the intrinsic
completeness of both modes of convergence and the fact that convergence via the
partial order is a conservative extension of the metric convergence.
|
|---|