DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2016.22

Non-Omega-Overlapping TRSs are UN

Authors: Stefan Kahrs and Connor Smith

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

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 ⇓.

Cite as

Stefan Kahrs and Connor Smith. Non-Omega-Overlapping TRSs are UN. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 22:1-22:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{kahrs_et_al:LIPIcs.FSCD.2016.22,
  author =	{Kahrs, Stefan and Smith, Connor},
  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 =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.22},
  URN =		{urn:nbn:de:0030-drops-59968},
  doi =		{10.4230/LIPIcs.FSCD.2016.22},
  annote =	{Keywords: consistency, omega-substitutions, uniqueness of normal forms}
}

Document

DOI: 10.4230/LIPIcs.RTA.2010.161

Infinitary Rewriting: Foundations Revisited

Authors: Stefan Kahrs

Published in: LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010)

Abstract

Infinitary Term Rewriting allows to express infinitary terms and infinitary reductions that converge to them. As their notion of transfinite reduction in general, and as binary relations in particular two concepts have been studied in the past: strongly and weakly convergent reductions, and in the last decade research has mostly focused around the former. Finitary rewriting has a strong connection to the equational theory of its rule set: if the rewrite system is confluent this (implies consistency of the theory and) gives rise to a semi-decision procedure for the theory, and if the rewrite system is in addition terminating this becomes a decision procedure. This connection is the original reason for the study of these properties in rewriting. For infinitary rewriting there is barely an established notion of an equational theory. The reason this issue is not trivial is that such a theory would need to include some form of ``getting to limits'', and there are different options one can pursue. These options are being looked at here, as well as several alternatives for the notion of reduction relation and their relationships to these equational theories.

Cite as

Stefan Kahrs. Infinitary Rewriting: Foundations Revisited. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 161-176, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{kahrs:LIPIcs.RTA.2010.161,
  author =	{Kahrs, Stefan},
  title =	{{Infinitary Rewriting: Foundations Revisited}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{161--176},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Lynch, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.161},
  URN =		{urn:nbn:de:0030-drops-26510},
  doi =		{10.4230/LIPIcs.RTA.2010.161},
  annote =	{Keywords: Infinitary rewriting,equivalence}
}

Search Results

Documents authored by Kahrs, Stefan

Non-Omega-Overlapping TRSs are UN

Abstract

Cite as

Infinitary Rewriting: Foundations Revisited

Abstract

Cite as

Thanks for your feedback!

Could not send message