DROPS

Document

DOI: 10.4230/LIPIcs.RTA.2015.301

Confluence of Orthogonal Nominal Rewriting Systems Revisited

Authors: Takaki Suzuki, Kentaro Kikuchi, Takahito Aoto, and Yoshihito Toyama

Published in: LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015)

Abstract

Nominal rewriting systems (Fernandez, Gabbay, Mackie, 2004; Fernandez, 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 (Fernandez, 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 alpha-stability which guarantees alpha-equivalence of peaks from the self-rooted overlaps. Moreover, we give a sufficient criterion for uniformity and alpha-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.

Cite as

Takaki Suzuki, Kentaro Kikuchi, Takahito Aoto, and Yoshihito Toyama. Confluence of Orthogonal Nominal Rewriting Systems Revisited. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 301-317, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{suzuki_et_al:LIPIcs.RTA.2015.301,
  author =	{Suzuki, Takaki and Kikuchi, Kentaro and Aoto, Takahito and Toyama, Yoshihito},
  title =	{{Confluence of Orthogonal Nominal Rewriting Systems Revisited}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{301--317},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-85-9},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{36},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.301},
  URN =		{urn:nbn:de:0030-drops-52042},
  doi =		{10.4230/LIPIcs.RTA.2015.301},
  annote =	{Keywords: Nominal rewriting, Confluence, Orthogonality, Higher-order rewriting, alpha-equivalence}
}

Search Results

Documents authored by Suzuki, Takaki

Confluence of Orthogonal Nominal Rewriting Systems Revisited

Abstract

Cite as

Thanks for your feedback!

Could not send message