A Dependency Pair Framework for Relative Termination of Term Rewriting

TL;DR

This paper introduces a new dependency pair framework for proving the relative termination of term rewrite systems, extending existing techniques to handle infinite sequences and probabilistic systems, with implementation and evaluation in AProVE.

Contribution

It develops a novel adaptation of annotated dependency pairs for relative termination, addressing an open problem and enhancing termination analysis tools.

Findings

Effective in proving relative termination of TRSs.

Outperforms some existing tools in evaluations.

Successfully integrated into AProVE for practical use.

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.