Constraint Handling Rules (CHR)

INTRODUCTION to Constraint Handling Rules (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.
Citation from Merging Views into CSPs: an Application for Computer Vision by Marco Alberti and Evelina Lamma, 2002.

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.
Citation from Programming with Logical Links: Design of the LMNtal Language by Kazunori Ueda and Norio Kato, 2003.

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.

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.

HOW CHR WORK

CHR are essentially a committed-choice language consisting of guarded rules with multiple head atoms. CHR 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.

For more information (including tutorials) see the Documents section.

URL www.informatik.uni-ulm.de/pm/mitarbeiter/fruehwirth/chr.html
Thom Frühwirth, updated June 11 2004