Transforming Outermost into Context-Sensitive Rewriting
Joerg Endrullis (Vrije Universiteit Amsterdam), Dimitri Hendriks, (Vrije Universiteit Amsterdam)

TL;DR
This paper introduces two transformations from term rewriting systems to context-sensitive TRSs, enabling the use of advanced termination methods to prove outermost termination, with implementations demonstrating practical success.
Contribution
It presents two novel transformations, 'context extension' and 'dynamic labeling', that relate outermost termination to context-sensitive rewriting, enhancing proof techniques.
Findings
Transformations are complete for left-linear TRSs.
Both transformations enable application of state-of-the-art termination methods.
Implemented in Jambox, achieving success in termination competitions.
Abstract
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
