A Dependency Pair Framework for Relative Termination of Term Rewriting

TL;DR

This work addresses proving relative termination for term rewriting systems by introducing a novel framework of relative annotated dependency pairs (ADPs). It extends the DP methodology to the relative setting, introducing main vs base ADPs, a variable reposition function (VRF) to preserve annotations during rewriting, and ADP rewrite semantics tailored to relative termination. The authors implement the framework in AProVE and demonstrate its practical impact through experiments against state-of-the-art tools, notably improving success on benchmarks where the main TRS does not dominate the base TRS. Overall, the paper provides the first DP-based framework specialized for relative termination, with empirical evidence of enhanced power and a pathway for extending to other rewriting paradigms and probabilistic settings.

Abstract

Dependency pairs are one of the most powerful techniques for proving termination of term rewrite systems (TRSs), and they are used in almost all tools for termination analysis of TRSs. Problem #106 of the RTA List of Open Problems asks for an adaption of dependency pairs for relative termination. Here, infinite rewrite sequences are allowed, but one wants to prove that a certain subset of the rewrite rules cannot be used infinitely often. Dependency pairs were recently adapted to annotated dependency pairs (ADPs) to prove almost-sure termination of probabilistic TRSs. In this paper, we develop a novel adaption of ADPs for relative termination. We implemented our new ADP framework in our tool AProVE and evaluate it in comparison to state-of-the-art tools for relative termination of TRSs.