May 17, 2016 1:54:29 PM
New CS Department, Stony Brook
Stony Brook, NY
Jul 6, 2016 5:00 AM
Jul 6, 2016 5:30 AM
A paper by Thom Frühwirth (Ulm University)
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 the Constraint Handling Rules 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.
The paper gives theorems with so-called misbehavior conditions for potential non-termination and failure (as well as definite termination) of direct recursive simplification rules in CHR. As we will see, logical relationships between the constraints in a recursive rule play a crucial role in this kind of program analysis.