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

Tomohiro Sasano
(Nagoya University)
Naoki Nishida
(Nagoya University)
Masahiko Sakai
(Nagoya University)
Tomoya Ueyama
(Nagoya University)

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.

In Horatiu Cirstea and David Sabel: Proceedings Fourth International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2017), Oxford, UK, 8th September 2017, Electronic Proceedings in Theoretical Computer Science 265, pp. 82–97.
Published: 16th February 2018.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: