Böhm reduction for terms and term graphs

Abstract

Infinitary rewriting endows a rewriting system with a mode of convergence that assigns an outcome to each infinite reduction that is – in some sense – well-formed, for example, an infinite reduction that produces the infinite list of all natural numbers. Unfortunately, infinitary rewriting breaks well-known confluence results for lambda calculi and orthogonal term rewriting systems. In order to recover the confluence property in a meaningful way, Kennaway et al. extended the ordinary reduction relation so that `meaningless terms' can be contracted to a fresh constant ⊥. They showed that this extended reduction relation – called Böhm reduction – enjoys the confluence property for infinitary lambda calculi and infinitary orthogonal term rewriting.

In this talk I give an overview of Böhm reduction and confluence in infinitary term rewriting. The underlying mode of convergence of Böhm reduction is based on metric spaces. As an alternative to this approach, I present a mode of convergence – based on partially ordered sets – that enjoys the confluence property for orthogonal term rewriting systems directly, i.e. without the need to explicitly contract meaningless terms. Finally, I sketch how a corresponding infinitary rewriting theory can be developed for term graphs.

Category: Rewriting

Tags: Term Graphs, Confluence, Infinitary Rewriting, Graph Rewriting, Böhm Trees