Confluence and Commutation for Nominal Rewriting Systems with Atom-Variables

Kentaro Kikuchi, Takahito Aoto

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 languageEnglish
Title of host publicationLogic-Based Program Synthesis and Transformation - 30th International Symposium, LOPSTR 2020, Proceedings
EditorsMaribel Fernández
PublisherSpringer Science and Business Media Deutschland GmbH
Pages56-73
Number of pages18
ISBN (Print)9783030684457
DOIs
Publication statusPublished - 2021
Externally publishedYes
Event30th International Conference on Logic-Based Program Synthesis and Transformation, LOPSTR 2020 - Bologna, Italy
Duration: 2020 Sep 72020 Sep 9

Publication series

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

Conference

Conference30th International Conference on Logic-Based Program Synthesis and Transformation, LOPSTR 2020
CountryItaly
CityBologna
Period20/9/720/9/9

Keywords

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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Confluence and Commutation for Nominal Rewriting Systems with Atom-Variables'. Together they form a unique fingerprint.

Cite this