From Infinitary Term Rewriting to Cyclic Term Graph Rewriting and back

Abstract

Cyclic term graph rewriting has been shown to be adequate for simulating certain forms of infinitary term rewriting. These forms are, however, quite restrictive and it would be beneficial to lift these restriction at least for a limited class of rewriting systems. In order to better understand the correspondences between infinite reduction sequences over terms and finite reductions over cyclic term graphs, we explore different variants of infinitary term graph rewriting calculi. To this end, we study different modes of convergence for term graph rewriting that generalise the modes of convergence usually considered in infinitary term rewriting. After discussing several different alternatives, we identify a complete semilattice on term graphs and derive from it a complete metric space on term graphs. Equipped with these structures, we can – analogously to the term rewriting case – define both a metric and a partial order model of infinitary term graph rewriting. The resulting calculi of infinitary term graph rewriting reveal properties similar to the corresponding infinitary term rewriting calculi.

Category: Rewriting

Tags: Domain Theory, Infinitary Rewriting, Infinitary Term Rewriting, Term Graph Rewriting, Term Rewriting, Topology