Parallel closure theorem for left-linear nominal rewriting systems

Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

2 Citations (Scopus)


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
Number of pages17
ISBN (Print)9783319661667
Publication statusPublished - 2017
Event11th International Symposium on Frontiers of Combining Systems, FroCoS 2017 - Brasilia, Brazil
Duration: 2017 Sept 272017 Sept 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


Conference11th International Symposium on Frontiers of Combining Systems, FroCoS 2017


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

Cite this