Partial Order Infinitary Term Rewriting and Böhm Trees

    Publikation: Konference artikel i Proceeding eller bog/rapport kapitelBidrag til bog/antologiForskningpeer review

    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öhm extensions. The Bö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ö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.
    OriginalsprogUdefineret/Ukendt
    TitelProceedings of the 21st International Conference on Rewriting Techniques and Applications
    RedaktørerChristopher Lynch
    Antal sider18
    Vol/bind6
    UdgivelsesstedDagstuhl, Germany
    ForlagSchloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH
    Publikationsdato2010
    Sider67-84
    ISBN (Trykt)978-3-939897-18-7
    DOI
    StatusUdgivet - 2010

    Emneord

    • Infinitary Term Rewriting
    • Partial Order Convergence
    • Metric Convergence
    • Orthogonal Term Rewriting Systems
    • Böhm Extensions

    Citationsformater