Convergence in Infinitary Term Graph Rewriting Systems is Simple (Extended Abstract)

TL;DR

This paper introduces a straightforward method for convergence in infinitary term graph rewriting systems, unifying existing approaches using partial orders and metrics, and improves upon previous methods by adopting a strong convergence discipline.

Contribution

A simple, unified approach to convergence in term graph rewriting using partial orders and metrics, improving upon earlier complex methods.

Findings

The new approach unifies term graph and infinitary term rewriting.

It is simpler and more effective than previous methods.

Adopting strong convergence discipline rectifies previous limitations.

Abstract

In this extended abstract, we present a simple approach to convergence on term graphs that allows us to unify term graph rewriting and infinitary term rewriting. This approach is based on a partial order and a metric on term graphs. These structures arise as straightforward generalisations of the corresponding structures used in infinitary term rewriting. We compare our simple approach to a more complicated approach that we developed earlier and show that this new approach is superior in many ways. The only unfavourable property that we were able to identify, viz. failure of full correspondence between weak metric and partial order convergence, is rectified by adopting a strong convergence discipline.