Scaling termination proofs by a characterisation of cycles in CHR
Paolo Pilozzi, Danny De Schreye · Lirias (KU Leuven) · 2009
CHR, short for Constraint Handling Rules, is a rule-based programming language, with similarities to Term Rewrite Systems and Logic Programming. Using cycles in termination analysis of rule-based languages can have several advantages. They are mostly due to the fact that an analysis based on cycles is more modular. One advantage is reduced complexity. Another potential advantage is precision. We have studied the introduction of cycles in CHR. However, we were confronted with the fact that, due to the multi-headed rules and a multiset semantics in CHR, it is hard to define a suitable notion of ``cycle''. One of our initial attempts was very intuitive but too precise, making a concept of minimality impossible. In this paper, we provide a less precise but useful definition of a cycle yielding a finite number of minimal cycles, and discuss its successful use in CHR termination analysis.