Created by Thom Frühwirth in 1991, the CHR language has become a major specification and implementation language for constraint-based algorithms and applications. Algorithms are often specified using inference rules, rewrite rules, sequents, proof rules, or logical axioms that can be directly written in CHR. Based on first order predicate logic, the clean semantics of CHR facilitates non-trivial program analysis and transformation. About a dozen implementations of CHR exist in Prolog, Haskell, and Java. CHR is also available as WebCHR for online experimentation with more than 40 constraint solvers. More than 100 projects use CHR.
Thus, we have developed a constraint handler tuned for this problem, using the Constraint Handling Rules (CHR) language which is perfectly suitable for high level design of constraint systems.”
— Marco Alberti and Evelina Lamma,
“Merging Views into CSPs: an Application for Computer Vision”, 2002.
CHR - a concurrent language for constraint systems, logic, agents, and more
CHR are a high-level language for concurrent logical systems. CHR make it easy to define constraint reasoning: simplification and propagation as well as incremental solving of constraints. Also, CHR have been successfully used
- as general purpose concurrent constraint language with ask and tell
- as fairly efficient production rule system
- as special kind of theorem prover with constraints
- as system combining forward and backward chaining
- for bottom-up evaluation with integrity constraints
- for top-down evaluation with tabulation
- for combining deduction, abduction, and constraints
- as high-level language for manipulating attributed variables
- for parsing with executable grammars
- for multi-set rewriting and transformations
Ultra High Level Algorithm Design
With CHR, any first-order constraint theory and consistency algorithm can be implemented at a high level of abstraction (rapid prototyping). The usual formalisms to describe a constraint theory, i.e. inference rules, rewrite rules, sequents, first-order axioms, can be expressed as CHR rules in a straightforward way. Starting from this executable specification, the rules then can be refined and adapted to the specifics of the application. This also makes CHR an excellent ultra-high-level tool for explaining and developing declarative and concurrent algorithms. Indeed, any terminating and confluent CHR program will automatically implement a concurrent any-time (approximation) and on-line (incremental) algorithm.
CHR was designed as a language for defining constraint solvers, but at the same time it is one of the most powerful multiset rewriting languages.”
— Kazunori Ueda and Norio Kato,
“Programming with Logical Links: Design of the LMNtal Language”, 2003.
How CHR works
CHR is essentially a committed-choice language consisting of guarded rules with multiple head atoms. CHR rules define simplification of, and propagation over, multi-sets of relations interpreted as conjunctions of constraint atoms. Simplification rewrites constraints to simpler constraints while preserving logical equivalence (e.g. X>Y,Y>X <=> false). Propagation adds new constraints which are logically redundant but may cause further simplification (e.g. X>Y,Y>Z ==> X>Z). Repeatedly applying the rules incrementally solves constraints (e.g. A>B,B>C,C>A leads to false). With multiple heads and propagation rules, CHR provide two features which are essential for non-trivial constraint handling.