Operational equivalence of CHR programs and constraints

Abstract. A fundamental question in programming language semantics is when two programs should be considered equivalent. In this paper we introduce a notion of operational equivalence for CHR programs and user-de ned constraints. Constraint Handling Rules (CHR) is a high-level language for writing constraint solvers either from scratch or by modifying existing solvers. We give a decidable, sucient and necessary syntactic condition for op-erational equivalence of terminating and con uent CHR programs. For practical reasons, we also investigate a notion of operational equiva-lence for user-dened constraints that are dened in dierent programs. We give a sucient syntactic condition for constraints dened in termi-nating and con uent CHR programs. For a subclass of programs which have only one user-dened constraint in common, we are able to give a sucient and necessary syntactic condition.