Equivalence of CHR States Revisited
Frank Raiser, Hariolf Betz, Thom Frühwirth · 2009
Abstract. 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. 1