License
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://drops.dagstuhl.de/opus/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
Seminar: 26th International Conference on Rewriting Techniques and Applications (RTA 2015)
Issue Date: 2015
Date of publication: 17.06.2015


DROPS-Home | Fulltext Search | Imprint Published by LZI