Guard simplification in CHR programs
Jon Sneyers, Tom Schrijvers, Bart Demoen · Lirias · 2005
Abstract. Constraint Handling Rules (CHR) is a high-level language commonly used to write constraint solvers. Most CHR programs depend on the refined operational semantics, obfuscating their logical reading and causing different (termination) behavior under the theoretical operational semantics. We introduce a source to source transformation called guard simplification which allows CHR programmers to write selfdocumented rules with a clear logical reading. Performance is improved by removing guards entailed by the implicit "no earlier (sub)rule fired " precondition and optional type and mode declarations. A formal description of the transformation is given, its implementation in the K.U.Leuven CHR compiler is presented and experimental results are discussed. 1 Introduction Constraint Handling Rules (CHR) is a high-level multi-headed rule-based programming language extension commonly used to write constraint solvers. We will assume the reader to be familiar with the syntax and semantics of CHR, referring to [5] for an overview. Examples are given in a Prolog context, although the results are valid in general. The theoretical operational semantics!t of CHRs, as defined in [5], is relatively nondeterministic as the order in which rules are tried is not specified. However, all implementations of CHR we know of use a more specific operational semantics, called the refined operational semantics!r [4]. In!r, the order in which rules are tried is the textual order in which the rules occur in the CHR program. Usually, CHR programmers take this refined operational semantics into account when they write CHR programs. As a result, their CHR programs could be non-terminating or could even produce incorrect results under!t semantics.