TY - GEN
T1 - Parallel closure theorem for left-linear nominal rewriting systems
AU - Kikuchi, Kentaro
AU - Aoto, Takahito
AU - Toyama, Yoshihito
N1 - Funding Information:
Acknowledgements. We are grateful to the anonymous referees for valuable comments. This research was supported by JSPS KAKENHI Grant Numbers 15K00003 and 16K00091.
Publisher Copyright:
© Springer International Publishing AG 2017.
PY - 2017
Y1 - 2017
N2 - Nominal rewriting has been introduced as an extension of first-order term rewriting by a binding mechanism based on the nominal approach. In this paper, we extend Huet’s parallel closure theorem and its generalisation on confluence of left-linear term rewriting systems to the case of nominal rewriting. The proof of the theorem follows a previous inductive confluence proof for orthogonal uniform nominal rewriting systems, but the presence of critical pairs requires a much more delicate argument. The results include confluence of left-linear uniform nominal rewriting systems that are not α-stable and thus are not represented by any systems in traditional higher-order rewriting frameworks.
AB - Nominal rewriting has been introduced as an extension of first-order term rewriting by a binding mechanism based on the nominal approach. In this paper, we extend Huet’s parallel closure theorem and its generalisation on confluence of left-linear term rewriting systems to the case of nominal rewriting. The proof of the theorem follows a previous inductive confluence proof for orthogonal uniform nominal rewriting systems, but the presence of critical pairs requires a much more delicate argument. The results include confluence of left-linear uniform nominal rewriting systems that are not α-stable and thus are not represented by any systems in traditional higher-order rewriting frameworks.
UR - http://www.scopus.com/inward/record.url?scp=85029589341&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85029589341&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-66167-4_7
DO - 10.1007/978-3-319-66167-4_7
M3 - Conference contribution
AN - SCOPUS:85029589341
SN - 9783319661667
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 115
EP - 131
BT - Frontiers of Combining Systems - 11th International Symposium, FroCoS 2017, Proceedings
A2 - Dixon, Clare
A2 - Finger, Marcelo
PB - Springer Verlag
T2 - 11th International Symposium on Frontiers of Combining Systems, FroCoS 2017
Y2 - 27 September 2017 through 29 September 2017
ER -