Partial order infinitary term rewriting and Böhm trees

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Documents

  • Patrick Bahr
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.
Original languageEnglish
Title of host publicationProceedings of the 21st International Conference on Rewriting Techniques and Applications
EditorsChristopher Lynch
Number of pages19
PublisherSchloss Dagstuhl - Leibniz-Zentrum für Informatik
Publication date2010
Pages67-84
ISBN (Electronic)978-3-939897-18-7
DOIs
Publication statusPublished - 2010
Event21st International Conference on Rewriting Techniques and Applications - Edinburgh, United Kingdom
Duration: 11 Jul 201013 Jul 2010

Conference

Conference21st International Conference on Rewriting Techniques and Applications
LandUnited Kingdom
ByEdinburgh
Periode11/07/201013/07/2010
SeriesLeibniz International Proceedings in Informatics (LIPIcs)
Volume6
ISSN1868-8969

    Research areas

  • Faculty of Science - infinitary term rewriting, Böhm trees, partial order, confluence, normalisation

Number of downloads are based on statistics from Google Scholar and www.ku.dk


No data available

ID: 20876611