TY - GEN
T1 - Confluence of orthogonal nominal rewriting systems revisited
AU - Suzuki, Takaki
AU - Kikuchi, Kentaro
AU - Aoto, Takahito
AU - Toyama, Yoshihito
N1 - Funding Information:
We would like to thank the anonymous referees for useful comments. This research was supported by JSPS KAKENHI Grant Numbers 25330004, 25280025 and 15K00003.
Publisher Copyright:
©Takaki Suzuki, Kentaro Kikuchi, Takahito Aoto, and Yoshihito Toyama.
PY - 2015/6/1
Y1 - 2015/6/1
N2 - Nominal rewriting systems (Fernández, Gabbay & Mackie, 2004; Fernández & 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 (Fernández & 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 α-stability which guarantees α-equivalence of peaks from the self-rooted overlaps. Moreover, we give a sufficient criterion for uniformity and α-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.
AB - Nominal rewriting systems (Fernández, Gabbay & Mackie, 2004; Fernández & 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 (Fernández & 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 α-stability which guarantees α-equivalence of peaks from the self-rooted overlaps. Moreover, we give a sufficient criterion for uniformity and α-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.
KW - Confluence
KW - Higher-order rewriting
KW - Nominal rewriting
KW - Orthogonality
KW - α-equivalence
UR - http://www.scopus.com/inward/record.url?scp=84958962749&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84958962749&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.RTA.2015.301
DO - 10.4230/LIPIcs.RTA.2015.301
M3 - Conference contribution
AN - SCOPUS:84958962749
T3 - Leibniz International Proceedings in Informatics, LIPIcs
SP - 301
EP - 317
BT - 26th International Conference on Rewriting Techniques and Applications, RTA 2015
A2 - Fernandez, Maribel
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 26th International Conference on Rewriting Techniques and Applications, RTA 2015
Y2 - 29 June 2015 through 1 July 2015
ER -