Partial order infinitary term rewriting and Böhm trees
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Documents
- Bahr_2010_Partial_order
Final published version, 206 KB, PDF document
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 language | English |
---|---|
Title of host publication | Proceedings of the 21st International Conference on Rewriting Techniques and Applications |
Editors | Christopher Lynch |
Number of pages | 19 |
Publisher | Schloss Dagstuhl - Leibniz-Zentrum für Informatik |
Publication date | 2010 |
Pages | 67-84 |
ISBN (Electronic) | 978-3-939897-18-7 |
DOIs | |
Publication status | Published - 2010 |
Event | 21st International Conference on Rewriting Techniques and Applications - Edinburgh, United Kingdom Duration: 11 Jul 2010 → 13 Jul 2010 |
Conference
Conference | 21st International Conference on Rewriting Techniques and Applications |
---|---|
Land | United Kingdom |
By | Edinburgh |
Periode | 11/07/2010 → 13/07/2010 |
Series | Leibniz International Proceedings in Informatics (LIPIcs) |
---|---|
Volume | 6 |
ISSN | 1868-8969 |
- Faculty of Science - infinitary term rewriting, Böhm trees, partial order, confluence, normalisation
Research areas
Number of downloads are based on statistics from Google Scholar and www.ku.dk
No data available
ID: 20876611