Transforming Dependency Chains of Constrained TRSs into Bounded Monotone Sequences of Integers

TL;DR

This paper establishes conditions for linear polynomial interpretations to transform dependency chains into bounded monotone integer sequences, aiding termination proofs of constrained rewriting systems, exemplified by the McCarthy 91 function.

Contribution

It introduces sufficient conditions for linear polynomial interpretations to produce bounded monotone sequences, enhancing termination proof techniques for constrained TRSs.

Findings

Successfully proved termination of the McCarthy 91 function.

Proposed four DP processors for different sequence transformations.

Established conditions for polynomial interpretations to generate monotone sequences.

Abstract

In the dependency pair framework for proving termination of rewriting systems, polynomial interpretations are used to transform dependency chains into bounded decreasing sequences of integers, and they play an important role for the success of proving termination, especially for constrained rewriting systems. In this paper, we show sufficient conditions of linear polynomial interpretations for transforming dependency chains into bounded monotone (i.e., decreasing or increasing) sequences of integers. Such polynomial interpretations transform rewrite sequences of the original system into decreasing or increasing sequences independently of the transformation of dependency chains. When we transform rewrite sequences into increasing sequences, polynomial interpretations have non-positive coefficients for reducible positions of marked function symbols. We propose four DP processors parameterized by transforming dependency chains and rewrite sequences into either decreasing or increasing sequences of integers, respectively. We show that such polynomial interpretations make us succeed in proving termination of the McCarthy 91 function over the integers.