Ground Confluence and Strong Commutation Modulo Alpha-Equivalence in Nominal Rewriting

Kentaro Kikuchi

doi:10.1007/978-3-031-17715-6_17

Ground Confluence and Strong Commutation Modulo Alpha-Equivalence in Nominal Rewriting

Kentaro Kikuchi

Systems & Software Division

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

Nominal rewriting was introduced as an extension of first-order term rewriting by a binding mechanism based on the nominal approach. A distinctive feature of nominal rewriting is that α -equivalence is not implicitly dealt with at the meta-level but explicitly dealt with at the object-level. In this paper, we introduce the notion of strong commutation modulo α -equivalence and give a sufficient condition for it. Using the condition, we present a new criterion for confluence modulo α -equivalence (on ground terms) of possibly non-terminating left-linear nominal rewriting systems.

Original language	English
Title of host publication	Theoretical Aspects of Computing – ICTAC 2022 - 19th International Colloquium, Proceedings
Editors	Helmut Seidl, Zhiming Liu, Corina S. Pasareanu
Publisher	Springer Science and Business Media Deutschland GmbH
Pages	255-271
Number of pages	17
ISBN (Print)	9783031177149
DOIs	https://doi.org/10.1007/978-3-031-17715-6_17
Publication status	Published - 2022
Event	19th International Colloquium on Theoretical Aspects of Computing, ICTAC 2022 - Tbilisi, Georgia Duration: 2022 Sept 27 → 2022 Sept 29

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	13572 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	19th International Colloquium on Theoretical Aspects of Computing, ICTAC 2022
Country/Territory	Georgia
City	Tbilisi
Period	22/9/27 → 22/9/29

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/978-3-031-17715-6_17

Cite this

Kikuchi, K. (2022). Ground Confluence and Strong Commutation Modulo Alpha-Equivalence in Nominal Rewriting. In H. Seidl, Z. Liu, & C. S. Pasareanu (Eds.), Theoretical Aspects of Computing – ICTAC 2022 - 19th International Colloquium, Proceedings (pp. 255-271). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13572 LNCS). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-031-17715-6_17

Ground Confluence and Strong Commutation Modulo Alpha-Equivalence in Nominal Rewriting. / Kikuchi, Kentaro.

Theoretical Aspects of Computing – ICTAC 2022 - 19th International Colloquium, Proceedings. ed. / Helmut Seidl; Zhiming Liu; Corina S. Pasareanu. Springer Science and Business Media Deutschland GmbH, 2022. p. 255-271 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13572 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Kikuchi, K 2022, Ground Confluence and Strong Commutation Modulo Alpha-Equivalence in Nominal Rewriting. in H Seidl, Z Liu & CS Pasareanu (eds), Theoretical Aspects of Computing – ICTAC 2022 - 19th International Colloquium, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 13572 LNCS, Springer Science and Business Media Deutschland GmbH, pp. 255-271, 19th International Colloquium on Theoretical Aspects of Computing, ICTAC 2022, Tbilisi, Georgia, 22/9/27. https://doi.org/10.1007/978-3-031-17715-6_17

Kikuchi K. Ground Confluence and Strong Commutation Modulo Alpha-Equivalence in Nominal Rewriting. In Seidl H, Liu Z, Pasareanu CS, editors, Theoretical Aspects of Computing – ICTAC 2022 - 19th International Colloquium, Proceedings. Springer Science and Business Media Deutschland GmbH. 2022. p. 255-271. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-031-17715-6_17

Kikuchi, Kentaro. / Ground Confluence and Strong Commutation Modulo Alpha-Equivalence in Nominal Rewriting. Theoretical Aspects of Computing – ICTAC 2022 - 19th International Colloquium, Proceedings. editor / Helmut Seidl ; Zhiming Liu ; Corina S. Pasareanu. Springer Science and Business Media Deutschland GmbH, 2022. pp. 255-271 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{bc6771efba5f44299afe632e2cbcbaee,

title = "Ground Confluence and Strong Commutation Modulo Alpha-Equivalence in Nominal Rewriting",

abstract = "Nominal rewriting was introduced as an extension of first-order term rewriting by a binding mechanism based on the nominal approach. A distinctive feature of nominal rewriting is that α -equivalence is not implicitly dealt with at the meta-level but explicitly dealt with at the object-level. In this paper, we introduce the notion of strong commutation modulo α -equivalence and give a sufficient condition for it. Using the condition, we present a new criterion for confluence modulo α -equivalence (on ground terms) of possibly non-terminating left-linear nominal rewriting systems.",

author = "Kentaro Kikuchi",

note = "Funding Information: Acknowledgements. I am grateful to the anonymous referees for valuable comments. This work was partly supported by JSPS KAKENHI Grant Numbers JP19K11891 and JP20H04164. Publisher Copyright: {\textcopyright} 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.; 19th International Colloquium on Theoretical Aspects of Computing, ICTAC 2022 ; Conference date: 27-09-2022 Through 29-09-2022",

year = "2022",

doi = "10.1007/978-3-031-17715-6_17",

language = "English",

isbn = "9783031177149",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Science and Business Media Deutschland GmbH",

pages = "255--271",

editor = "Helmut Seidl and Zhiming Liu and Pasareanu, {Corina S.}",

booktitle = "Theoretical Aspects of Computing – ICTAC 2022 - 19th International Colloquium, Proceedings",

address = "Germany",

}

TY - GEN

T1 - Ground Confluence and Strong Commutation Modulo Alpha-Equivalence in Nominal Rewriting

AU - Kikuchi, Kentaro

N1 - Funding Information: Acknowledgements. I am grateful to the anonymous referees for valuable comments. This work was partly supported by JSPS KAKENHI Grant Numbers JP19K11891 and JP20H04164. Publisher Copyright: © 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.

PY - 2022

Y1 - 2022

N2 - Nominal rewriting was introduced as an extension of first-order term rewriting by a binding mechanism based on the nominal approach. A distinctive feature of nominal rewriting is that α -equivalence is not implicitly dealt with at the meta-level but explicitly dealt with at the object-level. In this paper, we introduce the notion of strong commutation modulo α -equivalence and give a sufficient condition for it. Using the condition, we present a new criterion for confluence modulo α -equivalence (on ground terms) of possibly non-terminating left-linear nominal rewriting systems.

AB - Nominal rewriting was introduced as an extension of first-order term rewriting by a binding mechanism based on the nominal approach. A distinctive feature of nominal rewriting is that α -equivalence is not implicitly dealt with at the meta-level but explicitly dealt with at the object-level. In this paper, we introduce the notion of strong commutation modulo α -equivalence and give a sufficient condition for it. Using the condition, we present a new criterion for confluence modulo α -equivalence (on ground terms) of possibly non-terminating left-linear nominal rewriting systems.

UR - http://www.scopus.com/inward/record.url?scp=85140715887&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85140715887&partnerID=8YFLogxK

U2 - 10.1007/978-3-031-17715-6_17

DO - 10.1007/978-3-031-17715-6_17

M3 - Conference contribution

AN - SCOPUS:85140715887

SN - 9783031177149

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 255

EP - 271

BT - Theoretical Aspects of Computing – ICTAC 2022 - 19th International Colloquium, Proceedings

A2 - Seidl, Helmut

A2 - Liu, Zhiming

A2 - Pasareanu, Corina S.

PB - Springer Science and Business Media Deutschland GmbH

T2 - 19th International Colloquium on Theoretical Aspects of Computing, ICTAC 2022

Y2 - 27 September 2022 through 29 September 2022

ER -