Confluence of orthogonal nominal rewriting systems revisited

Takaki Suzuki, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama

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

6 Citations (Scopus)

Abstract

Nominal rewriting systems (Fernández, Gabbay & Mackie, 2004; Fernández & Gabbay, 2007) have been introduced as a new framework of higher-order rewriting systems based on the nominal approach (Gabbay & Pitts, 2002; Pitts, 2003), which deals with variable binding via permutations and freshness conditions on atoms. Confluence of orthogonal nominal rewriting systems has been shown in (Fernández & Gabbay, 2007). However, their definition of (non-trivial) critical pairs has a serious weakness so that the orthogonality does not actually hold for most of standard nominal rewriting systems in the presence of binders. To overcome this weakness, we divide the notion of overlaps into the self-rooted and proper ones, and introduce a notion of α-stability which guarantees α-equivalence of peaks from the self-rooted overlaps. Moreover, we give a sufficient criterion for uniformity and α-stability. The new definition of orthogonality and the criterion offer a novel confluence condition effectively applicable to many standard nominal rewriting systems. We also report on an implementation of a confluence prover for orthogonal nominal rewriting systems based on our framework.

Original languageEnglish
Title of host publication26th International Conference on Rewriting Techniques and Applications, RTA 2015
EditorsMaribel Fernandez
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Pages301-317
Number of pages17
ISBN (Electronic)9783939897859
DOIs
Publication statusPublished - 2015 Jun 1
Event26th International Conference on Rewriting Techniques and Applications, RTA 2015 - Warsaw, Poland
Duration: 2015 Jun 292015 Jul 1

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume36
ISSN (Print)1868-8969

Other

Other26th International Conference on Rewriting Techniques and Applications, RTA 2015
CountryPoland
CityWarsaw
Period15/6/2915/7/1

Keywords

  • Confluence
  • Higher-order rewriting
  • Nominal rewriting
  • Orthogonality
  • α-equivalence

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Confluence of orthogonal nominal rewriting systems revisited'. Together they form a unique fingerprint.

Cite this