License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2010.85
URN: urn:nbn:de:0030-drops-26469
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2010/2646/
Go to the corresponding LIPIcs Volume Portal

Endrullis, Joerg ; Grabmayer, Clemens ; Hendriks, Dimitri ; Klop, Jan Willem ; van Oostrom, Vincent

Unique Normal Forms in Infinitary Weakly Orthogonal Rewriting

pdf-format:
10002.EndrulisJoerg.2646.pdf (0.2 MB)

Abstract

We present some contributions to the theory of infinitary rewriting
for weakly orthogonal term rewrite systems, in which critical pairs
may occur provided they are trivial.

We show that the infinitary unique normal form property (UNinf)
fails by a simple example of a weakly orthogonal TRS with two
collapsing rules. By translating this example, we show that UNinf
also fails for the infinitary lambda-beta-eta-calculus.

As positive results we obtain the following: Infinitary confluence,
and hence UNinf, holds for weakly orthogonal TRSs that do not contain
collapsing rules. To this end we refine the compression lemma.
Furthermore, we consider the triangle and diamond properties
for infinitary developments in weakly orthogonal TRSs,
by refining an earlier cluster-analysis for the finite case.

BibTeX - Entry

@InProceedings{endrullis_et_al:LIPIcs:2010:2646,
  author =	{Joerg Endrullis and Clemens Grabmayer and Dimitri Hendriks and Jan Willem Klop and Vincent van Oostrom},
  title =	{{Unique Normal Forms in Infinitary Weakly Orthogonal Rewriting}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{85--102},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Christopher Lynch},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2010/2646},
  URN =		{urn:nbn:de:0030-drops-26469},
  doi =		{10.4230/LIPIcs.RTA.2010.85},
  annote =	{Keywords: Weakly orthogonal term rewrite systems, unique normal form property,            infinitary rewriting, infinitary lambda-beta-eta-calculus,            }
}

Keywords: Weakly orthogonal term rewrite systems, unique normal form property, infinitary rewriting, infinitary lambda-beta-eta-calculus,
Collection: Proceedings of the 21st International Conference on Rewriting Techniques and Applications
Issue Date: 2010
Date of publication: 06.07.2010

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