Confluence of Orthogonal Nominal Rewriting Systems Revisited

Abstract

Nominal rewriting systems (Fernandez, Gabbay, Mackie, 2004;
Fernandez, Gabbay, 2007) have been introduced as a new framework
of higher-order rewriting systems based on the nominal approach
(Gabbay, Pitts, 2002; Pitts, 2003), which deals with variable
binding via permutations and freshness conditions on atoms.
Confluence of orthogonal nominal rewriting systems has been shown in
(Fernandez, Gabbay, 2007). However, their definition of
(non-trivial) critical pairs has a serious weakness so that the
orthogonality does not actually hold for most of standard nominal
rewriting systems in the presence of binders. To overcome this
weakness, we divide the notion of overlaps into the self-rooted and
proper ones, and introduce a notion of alpha-stability which
guarantees alpha-equivalence of peaks from the self-rooted
overlaps. Moreover, we give a sufficient criterion for uniformity and alpha-stability. The new definition of orthogonality and the
criterion offer a novel confluence condition effectively applicable to many standard nominal rewriting systems. We also report on an
implementation of a confluence prover for orthogonal nominal rewriting systems based on our framework.