We define two transformations from term rewriting systems (TRSs) tocontext-sensitive TRSs in such a way that termination of the target systemimplies outermost termination of the original system. In the transformationbased on 'context extension', each outermost rewrite step is modeled by exactlyone step in the transformed system. This transformation turns out to becomplete for the class of left-linear TRSs. The second transformation is called`dynamic labeling' and results in smaller sized context-sensitive TRSs. Hereeach modeled step is adjoined with a small number of auxiliary steps. As aresult state-of-the-art termination methods for context-sensitive rewritingbecome available for proving termination of outermost rewriting. Bothtransformations have been implemented in Jambox, making it the most successfultool in the category of outermost rewriting of the last edition of the annualtermination competition.
展开▼
