Equivalence of CHR states revisited

Frank Raiser, Hariolf Betz, and Thom Frühwirth. Equivalence of CHR states revisited. 2009, 6th International Workshop on Constraint Handling Rules (CHR), pages 34-48, Workshop


While it is generally agreed-upon that certain classes of CHR states should be considered equivalent, no standard definition of equivalence has ever been established. Furthermore, the compliance of equivalence with rule application is generally assumed, but has never been proven. We systematically develop an axiomatic notion of state equivalence based on rule applicability and the declarative semantics. We supply the missing proof for its compliance with rule application and provide a proof technique to determine equivalence of given states. The compliance property leads to a simplified formulation of the operational semantics. Furthermore, it justifies a novel view based on equivalence classes of states which provides a powerful proof technique.