Partial order infinitary term rewriting and Böhm trees
Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
Standard
Partial order infinitary term rewriting and Böhm trees. / Bahr, Patrick.
Proceedings of the 21st International Conference on Rewriting Techniques and Applications. red. / Christopher Lynch. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010. s. 67-84 (Leibniz International Proceedings in Informatics (LIPIcs), Bind 6).Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - GEN
T1 - Partial order infinitary term rewriting and Böhm trees
AU - Bahr, Patrick
PY - 2010
Y1 - 2010
N2 - 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.
AB - 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.
KW - Faculty of Science
KW - infinitary term rewriting
KW - Böhm trees
KW - partial order
KW - confluence
KW - normalisation
U2 - 10.4230/LIPIcs.RTA.2010.67
DO - 10.4230/LIPIcs.RTA.2010.67
M3 - Article in proceedings
T3 - Leibniz International Proceedings in Informatics (LIPIcs)
SP - 67
EP - 84
BT - Proceedings of the 21st International Conference on Rewriting Techniques and Applications
A2 - Lynch, Christopher
PB - Schloss Dagstuhl - Leibniz-Zentrum für Informatik
Y2 - 11 July 2010 through 13 July 2010
ER -
ID: 20876611