Parallel closure theorem for left-linear nominal rewriting systems

Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama

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

1 Citation (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationFrontiers of Combining Systems - 11th International Symposium, FroCoS 2017, Proceedings
EditorsClare Dixon, Marcelo Finger
PublisherSpringer Verlag
Pages115-131
Number of pages17
ISBN (Print)9783319661667
DOIs
Publication statusPublished - 2017
Externally publishedYes
Event11th International Symposium on Frontiers of Combining Systems, FroCoS 2017 - Brasilia, Brazil
Duration: 2017 Sep 272017 Sep 29

Publication series

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

Other

Other11th International Symposium on Frontiers of Combining Systems, FroCoS 2017
CountryBrazil
CityBrasilia
Period17/9/2717/9/29

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Parallel closure theorem for left-linear nominal rewriting systems'. Together they form a unique fingerprint.

Cite this