Infinitary Term Graph Rewriting

TL;DR

This paper develops a unified theoretical framework combining infinitary term rewriting and term graph rewriting to better understand lazy evaluation, sharing, and non-strictness in computation.

Contribution

It introduces a metric space and semilattice-based framework that unifies term rewriting and term graph rewriting, extending soundness results to the infinitary setting.

Findings

Unified framework for infinitary term rewriting and term graph rewriting

Extension of soundness results to infinite reductions

Framework based on metric space and complete semilattice

Abstract

Term graph rewriting provides a formalism for implementing term rewriting in an efficient manner by avoiding duplication. Infinitary term rewriting has been introduced to study infinite term reduction sequences. Such infinite reductions can be used to reason about lazy evaluation. In this paper, we combine term graph rewriting and infinitary term rewriting thereby addressing both components of lazy evaluation: non-strictness and sharing. Moreover, we show how our theoretical underpinnings, based on a metric space and a complete semilattice, provides a unified framework for both term rewriting and term graph rewriting. This makes it possible to study the correspondences between these two worlds. As an example, we show how the soundness of term graph rewriting w.r.t. term rewriting can be extended to the infinitary setting.