Confluence and Commutation for Nominal Rewriting Systems with Atom-Variables

Kentaro Kikuchi; Takahito Aoto

doi:10.1007/978-3-030-68446-4_3

Confluence and Commutation for Nominal Rewriting Systems with Atom-Variables

Kentaro Kikuchi, Takahito Aoto

RIEC - Computing System Platforms Division

Niigata University

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

Abstract

Nominal rewriting was introduced as an extension of first-order term rewriting by a binding mechanism based on the nominal approach. Recently, a new format of nominal rewriting has been introduced where rewrite rules are defined with atom-variables rather than atoms. In this paper, we investigate the difference between the new format and the original nominal rewriting, and prove confluence and commutation for some classes of rewriting systems whose rewrite rules have no proper overlaps which are computed using nominal unification with atom-variables. The properties we prove are expected to be used in a form of program transformation that is realised as an equivalence transformation of rewriting systems.

Original language	English
Title of host publication	Logic-Based Program Synthesis and Transformation - 30th International Symposium, LOPSTR 2020, Proceedings
Editors	Maribel Fernández
Publisher	Springer Science and Business Media Deutschland GmbH
Pages	56-73
Number of pages	18
ISBN (Print)	9783030684457
DOIs	https://doi.org/10.1007/978-3-030-68446-4_3
Publication status	Published - 2021
Event	30th International Conference on Logic-Based Program Synthesis and Transformation, LOPSTR 2020 - Bologna, Italy Duration: 2020 Sept 7 → 2020 Sept 9

Publication series

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

Conference

Conference	30th International Conference on Logic-Based Program Synthesis and Transformation, LOPSTR 2020
Country/Territory	Italy
City	Bologna
Period	20/9/7 → 20/9/9

Keywords

Alpha-equivalence
Atom-variable
Commutation
Confluence
Nominal rewriting
Nominal unification
Variable binding

Access to Document

10.1007/978-3-030-68446-4_3

Cite this

Kikuchi, K., & Aoto, T. (2021). Confluence and Commutation for Nominal Rewriting Systems with Atom-Variables. In M. Fernández (Ed.), Logic-Based Program Synthesis and Transformation - 30th International Symposium, LOPSTR 2020, Proceedings (pp. 56-73). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12561 LNCS). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-030-68446-4_3

Kikuchi, Kentaro ; Aoto, Takahito. / Confluence and Commutation for Nominal Rewriting Systems with Atom-Variables. Logic-Based Program Synthesis and Transformation - 30th International Symposium, LOPSTR 2020, Proceedings. editor / Maribel Fernández. Springer Science and Business Media Deutschland GmbH, 2021. pp. 56-73 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{9d00e4dd946f45d989c5c3149e54af46,

title = "Confluence and Commutation for Nominal Rewriting Systems with Atom-Variables",

abstract = "Nominal rewriting was introduced as an extension of first-order term rewriting by a binding mechanism based on the nominal approach. Recently, a new format of nominal rewriting has been introduced where rewrite rules are defined with atom-variables rather than atoms. In this paper, we investigate the difference between the new format and the original nominal rewriting, and prove confluence and commutation for some classes of rewriting systems whose rewrite rules have no proper overlaps which are computed using nominal unification with atom-variables. The properties we prove are expected to be used in a form of program transformation that is realised as an equivalence transformation of rewriting systems.",

keywords = "Alpha-equivalence, Atom-variable, Commutation, Confluence, Nominal rewriting, Nominal unification, Variable binding",

author = "Kentaro Kikuchi and Takahito Aoto",

note = "Funding Information: Acknowledgements. We are grateful to the anonymous referees for valuable comments. The first author thanks Makoto Hamana for useful discussions. This work was partly supported by JSPS KAKENHI Grant Numbers JP17K00005, JP18K11158, JP19K11891 and JP20H04164. Publisher Copyright: {\textcopyright} 2021, Springer Nature Switzerland AG.; 30th International Conference on Logic-Based Program Synthesis and Transformation, LOPSTR 2020 ; Conference date: 07-09-2020 Through 09-09-2020",

year = "2021",

doi = "10.1007/978-3-030-68446-4_3",

language = "English",

isbn = "9783030684457",

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 = "56--73",

editor = "Maribel Fern{\'a}ndez",

booktitle = "Logic-Based Program Synthesis and Transformation - 30th International Symposium, LOPSTR 2020, Proceedings",

address = "Germany",

}

Kikuchi, K & Aoto, T 2021, Confluence and Commutation for Nominal Rewriting Systems with Atom-Variables. in M Fernández (ed.), Logic-Based Program Synthesis and Transformation - 30th International Symposium, LOPSTR 2020, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12561 LNCS, Springer Science and Business Media Deutschland GmbH, pp. 56-73, 30th International Conference on Logic-Based Program Synthesis and Transformation, LOPSTR 2020, Bologna, Italy, 20/9/7. https://doi.org/10.1007/978-3-030-68446-4_3

Confluence and Commutation for Nominal Rewriting Systems with Atom-Variables. / Kikuchi, Kentaro; Aoto, Takahito.
Logic-Based Program Synthesis and Transformation - 30th International Symposium, LOPSTR 2020, Proceedings. ed. / Maribel Fernández. Springer Science and Business Media Deutschland GmbH, 2021. p. 56-73 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12561 LNCS).

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

TY - GEN

T1 - Confluence and Commutation for Nominal Rewriting Systems with Atom-Variables

AU - Kikuchi, Kentaro

AU - Aoto, Takahito

N1 - Funding Information: Acknowledgements. We are grateful to the anonymous referees for valuable comments. The first author thanks Makoto Hamana for useful discussions. This work was partly supported by JSPS KAKENHI Grant Numbers JP17K00005, JP18K11158, JP19K11891 and JP20H04164. Publisher Copyright: © 2021, Springer Nature Switzerland AG.

PY - 2021

Y1 - 2021

N2 - Nominal rewriting was introduced as an extension of first-order term rewriting by a binding mechanism based on the nominal approach. Recently, a new format of nominal rewriting has been introduced where rewrite rules are defined with atom-variables rather than atoms. In this paper, we investigate the difference between the new format and the original nominal rewriting, and prove confluence and commutation for some classes of rewriting systems whose rewrite rules have no proper overlaps which are computed using nominal unification with atom-variables. The properties we prove are expected to be used in a form of program transformation that is realised as an equivalence transformation of rewriting systems.

AB - Nominal rewriting was introduced as an extension of first-order term rewriting by a binding mechanism based on the nominal approach. Recently, a new format of nominal rewriting has been introduced where rewrite rules are defined with atom-variables rather than atoms. In this paper, we investigate the difference between the new format and the original nominal rewriting, and prove confluence and commutation for some classes of rewriting systems whose rewrite rules have no proper overlaps which are computed using nominal unification with atom-variables. The properties we prove are expected to be used in a form of program transformation that is realised as an equivalence transformation of rewriting systems.

KW - Alpha-equivalence

KW - Atom-variable

KW - Commutation

KW - Confluence

KW - Nominal rewriting

KW - Nominal unification

KW - Variable binding

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

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

U2 - 10.1007/978-3-030-68446-4_3

DO - 10.1007/978-3-030-68446-4_3

M3 - Conference contribution

AN - SCOPUS:85102618400

SN - 9783030684457

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

SP - 56

EP - 73

BT - Logic-Based Program Synthesis and Transformation - 30th International Symposium, LOPSTR 2020, Proceedings

A2 - Fernández, Maribel

PB - Springer Science and Business Media Deutschland GmbH

T2 - 30th International Conference on Logic-Based Program Synthesis and Transformation, LOPSTR 2020

Y2 - 7 September 2020 through 9 September 2020

ER -

Kikuchi K, Aoto T. Confluence and Commutation for Nominal Rewriting Systems with Atom-Variables. In Fernández M, editor, Logic-Based Program Synthesis and Transformation - 30th International Symposium, LOPSTR 2020, Proceedings. Springer Science and Business Media Deutschland GmbH. 2021. p. 56-73. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-68446-4_3

Confluence and Commutation for Nominal Rewriting Systems with Atom-Variables

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this