Towards an Incremental and Modular Termination Analysis of Context-Sensitive Rewriting Systems (Work in Progress)

Abstract

Modularity is essential in software development, where a piece of software is often designed and implemented as a composition of simpler modules. So, if we want to prove that a program satisfies a given property, a modular approach becomes natural. With the development and successful use of the Dependency Pair Framework, which rather focuses on the decomposition of termination problems, less attention has been payed to modularity issues (which rather require the opposite approach). But the modular analysis of termination is still paramount for software developers. In this paper, we analyze modularity of context-sensitive rewrite systems. A modularity analysis was carried out by Gramlich and Lucas in 2002, but a correct notion of context-sensitive dependency pair (CS-DP) was not obtained until 2006. In this paper, we analyze modularity using CS-DPs.