On Confluence of Non-terminating CHR Programs

Frank Raiser and Paolo Tacchella. On Confluence of Non-terminating CHR Programs. 2007, Constraint Handling Rules, 4th Workshop, CHR 2007, pages 63-76, Workshop


Confluence is an important property for any kind of rewrite system including CHR, which is a general-purpose declarative committed-choice language consisting of multi-headed guarded rules. CHR can yield a confluence problem, because of non-determinism in the choice of rules using the abstract semantics. Confluence in CHR is an ongoing research topic, because it provides numerous benefits for implementations. However, for non-terminating CHR programs confluence is generally undecidable. In this paper we apply the so-called Strong Church-Rosser property to CHR. This allows determination of confluence for a subset of non-terminating CHR programs.