Critical Peaks Redefined - $\Phi \sqcup \Psi = \top$

TL;DR

This paper introduces two equivalent formal accounts of clusters in rewriting systems, providing a lattice structure that offers a new perspective on critical peaks and their refinements.

Contribution

It presents geometric and inductive definitions of clusters, proves their isomorphism, and applies this to redefine critical peaks in term rewriting.

Findings

Clusters form a lattice structure.

Geometric and inductive accounts are isomorphic.

New perspective on critical peaks in rewriting systems.

Abstract

Let a cluster be a term with a number of patterns occurring in it. We give two accounts of clusters, a geometric one as sets of (node and edge) positions, and an inductive one as pairs of terms with gaps (2nd order variables) and pattern-substitutions for the gaps. We show both notions of cluster and the corresponding refinement/coarsening orders on them, to be isomorphic. This equips clusters with a lattice structure which we lift to (parallel/multi) steps to yield an alternative account of the notion of critical peak.