2026-07-22T04:53:59Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5204 2024-03-06T10:36:03Z ddc:004 open_access

Confluence of Orthogonal Nominal Rewriting Systems Revisited Suzuki, Takaki Kikuchi, Kentaro Aoto, Takahito Toyama, Yoshihito Nominal rewriting Confluence Orthogonality Higher-order rewriting alpha-equivalence 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Takaki Suzuki and Kentaro Kikuchi and Takahito Aoto and Yoshihito Toyama 2015 Is Part Of LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.RTA.2015.301 urn:nbn:de:0030-drops-52042 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.301 eng https://creativecommons.org/licenses/by/3.0/legalcode