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: https://drops.dagstuhl.de/opus/volltexte/2015/5192/
Czajka, Lukasz
Confluence of nearly orthogonal infinitary term rewriting systems
| pdf-format: |
|
Abstract
We give a relatively simple coinductive proof of confluence, moduloequivalence 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: | 18.06.2015 |
