Termination of Rewriting with and Automated Synthesis of Forbidden Patterns
Bernhard Gramlich (Vienna University of Technology), Felix, Schernhammer (Vienna University of Technology)

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
