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.FSCD.2016.22
URN: urn:nbn:de:0030-drops-59968
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/5996/
Go to the corresponding LIPIcs Volume Portal

Kahrs, Stefan ; Smith, Connor

Non-Omega-Overlapping TRSs are UN

pdf-format:
LIPIcs-FSCD-2016-22.pdf (0.5 MB)

Abstract

This paper solves problem #79 of RTA's list of open
problems --- in the positive. If the rules of a TRS do not overlap w.r.t.
substitutions of infinite terms then the TRS has unique normal forms.
We solve the problem by reducing the problem to one of consistency for
"similar" constructor term rewriting systems. For this we introduce
a new proof technique. We define a relation ⇓ that is
consistent by construction, and which --- if transitive --- would
coincide with the rewrite system's equivalence relation =R.

We then prove the transitivity of ⇓ by coalgebraic
reasoning. Any concrete proof for instances of this relation only
refers to terms of some finite coalgebra, and we then construct an
equivalence relation on that coalgebra which coincides with ⇓.

BibTeX - Entry

@InProceedings{kahrs_et_al:LIPIcs:2016:5996,
  author =	{Stefan Kahrs and Connor Smith},
  title =	{{Non-Omega-Overlapping TRSs are UN}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{22:1--22:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Delia Kesner and Brigitte Pientka},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/5996},
  URN =		{urn:nbn:de:0030-drops-59968},
  doi =		{10.4230/LIPIcs.FSCD.2016.22},
  annote =	{Keywords: consistency, omega-substitutions, uniqueness of normal forms}
}

Keywords: consistency, omega-substitutions, uniqueness of normal forms
Collection: 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Issue Date: 2016
Date of publication: 17.06.2016

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