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 -