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.67
URN: urn:nbn:de:0030-drops-26455
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2010/2645/
Go to the corresponding LIPIcs Volume Portal

Bahr, Patrick

Partial Order Infinitary Term Rewriting and Böhm Trees

pdf-format:
10002.BahrPatrick.2645.pdf (0.2 MB)

Abstract

We investigate an alternative model of infinitary term
rewriting. Instead of a metric, a partial order on terms is employed
to formalise (strong) convergence. We compare this partial order
convergence of orthogonal term rewriting systems to the usual metric
convergence of the corresponding B{"o}hm extensions. The B{"o}hm extension
of a term rewriting system contains additional rules to equate
so-called root-active terms. The core result we present is that
reachability w.r.t. partial order convergence coincides with
reachability w.r.t. metric convergence in the B{"o}hm extension. This
result is used to show that, unlike in the metric model, orthogonal
systems are infinitarily confluent and infinitarily normalising in the
partial order model. Moreover, we obtain, as in the metric model, a
compression lemma. A corollary of this lemma is that reachability
w.r.t. partial order convergence is a conservative extension of
reachability w.r.t. metric convergence.

BibTeX - Entry

@InProceedings{bahr:LIPIcs:2010:2645,
  author =	{Patrick Bahr},
  title =	{{Partial Order Infinitary Term Rewriting and B{\"o}hm Trees}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{67--84},
  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/2645},
  URN =		{urn:nbn:de:0030-drops-26455},
  doi =		{10.4230/LIPIcs.RTA.2010.67},
  annote =	{Keywords: Infinitary term rewriting, B{\"o}hm trees, partial order, confluence, normalisation}
}

Keywords: Infinitary term rewriting, Böhm trees, partial order, confluence, normalisation
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