Soundness and Completeness of Infinitary Term Graph Rewriting

Abstract

Infinitary term rewriting provides a tool for reasoning about infinite computations and infinite data as we conceptually find them in lazy functional programs. Term graph rewriting, on the other hand, captures the other defining aspect of lazy functional programming: sharing. With the goal of unifying both paradigms, we generalise the infinitary term rewriting theory to term graphs. We follow two approaches known from infinitary term rewriting: one based on a metric and another based on a partial order on term graphs. In the literature, infinitary term graph rewriting has been dismissed as not being 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, we show that the partial order-based calculus forms a conservative extension of the metric-based one similarly to the setting of infinitary term rewriting. Using this correspondence between the partial order-based calculus and the metric-based calculus, we are able to derive soundness and a weakened form of completeness for metric infinitary term graph rewriting.

Category: Rewriting

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