Confluence of Orthogonal Nominal Rewriting Systems Revisited

Authors Takaki Suzuki, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama

Thumbnail PDF


  • Filesize: 0.6 MB
  • 17 pages

Document Identifiers

Author Details

Takaki Suzuki
Kentaro Kikuchi
Takahito Aoto
Yoshihito Toyama

Cite AsGet BibTex

Takaki Suzuki, Kentaro Kikuchi, Takahito Aoto, and Yoshihito Toyama. Confluence of Orthogonal Nominal Rewriting Systems Revisited. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 301-317, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


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.
  • Nominal rewriting
  • Confluence
  • Orthogonality
  • Higher-order rewriting
  • alpha-equivalence


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads