Partial order infinitary term rewriting and Böhm trees

Patrick Bahr

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningpeer review

12 Citationer (Scopus)
1377 Downloads (Pure)

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.
OriginalsprogEngelsk
TitelProceedings of the 21st International Conference on Rewriting Techniques and Applications
RedaktørerChristopher Lynch
Antal sider19
ForlagSchloss Dagstuhl - Leibniz-Zentrum für Informatik
Publikationsdato2010
Sider67-84
ISBN (Elektronisk)978-3-939897-18-7
DOI
StatusUdgivet - 2010
Begivenhed21st International Conference on Rewriting Techniques and Applications - Edinburgh, Storbritannien
Varighed: 11 jul. 201013 jul. 2010

Konference

Konference21st International Conference on Rewriting Techniques and Applications
Land/OmrådeStorbritannien
ByEdinburgh
Periode11/07/201013/07/2010
NavnLeibniz International Proceedings in Informatics (LIPIcs)
Vol/bind6
ISSN1868-8969

Emneord

  • Det Natur- og Biovidenskabelige Fakultet

Citationsformater