Termination of Rewriting with and Automated Synthesis of Forbidden Patterns

TL;DR

This paper presents a modified dependency pair framework for analyzing termination of rewriting systems with forbidden pattern restrictions, incorporating contexts to improve analysis and enabling on-the-fly synthesis of forbidden patterns.

Contribution

It introduces a contextual dependency pair framework that handles forbidden pattern restrictions and includes a processor for simplifying problems and synthesizing forbidden patterns dynamically.

Findings

Framework is sound and complete for termination analysis with forbidden patterns

Processor effectively simplifies problems using contextual information

Method enables on-the-fly synthesis of forbidden patterns during analysis

Abstract

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.