Why Can't You Behave? Non-termination Analysis of Direct Recursive Rules with Constraints
This work addresses non-termination issues in constraint reasoning languages, which is incremental as it focuses on a specific type of recursion but could serve as a foundation for broader extensions.
The paper tackles the problem of non-termination and failure in rule-based programs, specifically for Constraint Handling Rules (CHR), by proposing static analysis with misbehavior conditions for linear direct recursive simplification rules, resulting in theorems that identify potential non-termination and failure.
This paper is concerned with rule-based programs that go wrong. The unwanted behavior of rule applications is non-termination or failure of a computation. We propose a static program analysis of the non-termination problem for recursion in the Constraint Handling Rules (CHR) language. CHR is an advanced concurrent declarative language involving constraint reasoning. It has been closely related to many other rule-based approaches, so the results are of a more general interest. In such languages, non-termination is due to infinite applications of recursive rules. Failure is due to accumulation of contradicting constraints during the computation. We give theorems with so-called misbehavior conditions for potential non-termination and failure (as well as definite termination) of linear direct recursive simplification rules. Logical relationships between the constraints in a recursive rule play a crucial role in this kind of program analysis. We think that our approach can be extended to other types of recursion and to a more general class of rules. Therefore this paper can serve as a basic reference and a starting point for further research.