Infinitary Term Graph Rewriting

Abstract

Based on a simple metric and a simple partial order on term graphs, we present two infinitary calculi of term graph rewriting. The partial order-based calculus forms a conservative extension of the metric-based one similarly to the setting of infinitary term rewriting. In the literature, the notion of infinitary term graph rewriting was dismissed as being not complete w.r.t. infinitary term rewriting. Our results show, however, that partial order infinitary term graph rewriting is sound and complete w.r.t. infinitary term rewriting. Moreover, using the correspondence between the partial order-based calculus and the metric-based calculus, we are able to derive soundness and a weaker form of completeness for metric infinitary term graph rewriting.

Category: Rewriting

Tags: Infinitary Rewriting, Metric, Partial Order, Term Graph Rewriting, Term Rewriting, Completeness, Soundness