Modes of Convergence for Infinitary Rewriting

Abstract

In infinitary term rewriting, the usual restriction to reduction sequences of finite length is repealed in favour of a notion of convergence that provides a limit for infinite reduction sequences. This notion of convergence is commonly based on the ultrametric on terms. In our work, we have explored an alternative mode of convergence based on the partial order of partial terms and its induced limit inferior. We can show that the thus defined model of infinitary term rewriting is evidently superior to the metric approach in a number of aspects including its simplicity, its convergence and normalisation properties, as well as its ability to capture the notion of Böhm trees. Moreover, we can show that the partial order model is a conservative extension over the metric model. Based on this approach to infinitary term rewriting, we aim to define modes of convergence for term graph rewriting in order to obtain the first formal treatment of infinitary term graph rewriting. The main goal of this endeavour is to investigate correspondences between infinitary term rewriting and graph rewriting that could enable to simulate infinite term reductions by a finite term graph reduction. To this end we explore different metric spaces as well as partial orders as candidates. While we argue in favour for a particular pair of a metric space and partial order, we also discuss potential other approaches that might result in a more appropriate structure for defining convergence for term graph reductions.

Category: Rewriting

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