Termination of Rewriting with and Automated Synthesis of Forbidden Patterns

Bernhard Gramlich
(Vienna University of Technology)
Felix Schernhammer
(Vienna University of Technology)

We introduce a modified version of the well-known dependency pair framework that is suitable for the termination analysis of rewriting under forbidden pattern restrictions. By attaching contexts to dependency pairs that represent the calling contexts of the corresponding recursive function calls, it is possible to incorporate the forbidden pattern restrictions in the (adapted) notion of dependency pair chains, thus yielding a sound and complete approach to termination analysis. Building upon this contextual dependency pair framework we introduce a dependency pair processor that simplifies problems by analyzing the contextual information of the dependency pairs. Moreover, we show how this processor can be used to synthesize forbidden patterns suitable for a given term rewriting system on-the-fly during the termination analysis.

In Hélène Kirchner and César Muñoz: Proceedings International Workshop on Strategies in Rewriting, Proving, and Programming (IWS 2010), Edinburgh, UK, 9th July 2010, Electronic Proceedings in Theoretical Computer Science 44, pp. 35–50.
Published: 24th December 2010.

ArXived at: http://dx.doi.org/10.4204/EPTCS.44.3 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org