# Why Can't You Behave? Non-termination Analysis of Direct Recursive Rules with Constraints

## TL;DR

This paper presents a static analysis method for detecting non-termination and failure in recursive rules within Constraint Handling Rules (CHR), aiding in understanding and preventing rule-based program errors.

## Contribution

It introduces theorems with misbehavior conditions for analyzing non-termination and failure in linear recursive CHR rules, expanding the understanding of rule behavior.

## Key findings

- Theorems for non-termination detection in recursive rules
- Conditions for failure due to conflicting constraints
- Potential extension to other recursion types

## Abstract

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.