Joerg Endrullis ; Dimitri Hendriks - Transforming Outermost into Context-Sensitive Rewriting

lmcs:1105 - Logical Methods in Computer Science, June 29, 2010, Volume 6, Issue 2 -
Transforming Outermost into Context-Sensitive Rewriting

Authors: Joerg Endrullis ; Dimitri Hendriks

    We define two transformations from term rewriting systems (TRSs) to context-sensitive TRSs in such a way that termination of the target system implies outermost termination of the original system. In the transformation based on 'context extension', each outermost rewrite step is modeled by exactly one step in the transformed system. This transformation turns out to be complete for the class of left-linear TRSs. The second transformation is called `dynamic labeling' and results in smaller sized context-sensitive TRSs. Here each modeled step is adjoined with a small number of auxiliary steps. As a result state-of-the-art termination methods for context-sensitive rewriting become available for proving termination of outermost rewriting. Both transformations have been implemented in Jambox, making it the most successful tool in the category of outermost rewriting of the last edition of the annual termination competition.

    Volume: Volume 6, Issue 2
    Published on: June 29, 2010
    Accepted on: June 25, 2015
    Submitted on: October 29, 2009
    Keywords: Computer Science - Logic in Computer Science,D.1.1, D.3.1, F.4.1, F.4.2, I.1.1, I.1.3

    Linked data

    Source : ScholeXplorer IsReferencedBy DOI 10.1007/s00236-019-00353-7
    Source : ScholeXplorer IsReferencedBy HANDLE 1871.1/c52a8a12-fa7b-459e-8b25-5be906b73f4c
    • 1871.1/c52a8a12-fa7b-459e-8b25-5be906b73f4c
    • 10.1007/s00236-019-00353-7
    • 10.1007/s00236-019-00353-7
    • 10.1007/s00236-019-00353-7
    atoms, infima and suprema
    Endrullis, Jörg ; Klop, Jan Willem ; Bakhshi, Rena ;

    4 Documents citing this article


    Consultation statistics

    This page has been seen 328 times.
    This article's PDF has been downloaded 209 times.