Critical Pair Analysis in Nominal Rewriting

Nominal rewriting (Fernandez, Gabbay & Mackie, 2004; Fernandez & Gabbay, 2007) is a framework that extends first-order term rewriting by a binding mechanism based on the nominal approach (Gabbay & Pitts, 2002; Pitts, 2003). In this paper, we investigate confluence properties of nominal rewriting, following the study of orthogonal systems in (Suzuki et al., 2015), but here we treat systems in which overlaps of the rewrite rules exist. First we present an example where choice of bound variables (atoms) of rules affects joinability of the induced critical pairs. Then we give a detailed proof of the critical pair lemma, and illustrate some of its applications including confluence results for non-terminating systems.