License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2015.106
URN: urn:nbn:de:0030-drops-51929
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5192/
Go to the corresponding LIPIcs Volume Portal

Czajka, Lukasz

Confluence of nearly orthogonal infinitary term rewriting systems

pdf-format:
12.pdf (0.6 MB)

Abstract

We give a relatively simple coinductive proof of confluence, modulo
equivalence of root-active terms, of nearly orthogonal infinitary
term rewriting systems. Nearly orthogonal systems allow certain root
overlaps, but no non-root overlaps. Using a slightly more complicated method we also show confluence modulo equivalence of
hypercollapsing terms. The condition we impose on root overlaps is
similar to the condition used by Toyama in the context of finitary
rewriting.

BibTeX - Entry

@InProceedings{czajka:LIPIcs:2015:5192,
  author =	{Lukasz Czajka},
  title =	{{Confluence of nearly orthogonal infinitary term rewriting  systems}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{106--126},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-85-9},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{36},
  editor =	{Maribel Fern{\'a}ndez},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5192},
  URN =		{urn:nbn:de:0030-drops-51929},
  doi =		{10.4230/LIPIcs.RTA.2015.106},
  annote =	{Keywords: infinitary rewriting, confluence, coinduction}
}

Keywords: infinitary rewriting, confluence, coinduction
Collection: 26th International Conference on Rewriting Techniques and Applications (RTA 2015)
Issue Date: 2015
Date of publication: 18.06.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI