Constraint Handling Rules

From Wikipedia, the free encyclopedia
  (Redirected from Constraint handling rules)
Jump to: navigation, search

Constraint Handling Rules (CHR) is a declarative programming language extension introduced in 1991[1][2] by Thom Frühwirth. Originally designed for developing (prototypes of) constraint programming systems, CHR is increasingly used as a high-level general-purpose programming language. Typical application domains of CHR are abduction, multi-agent systems, natural language processing, compilation, scheduling, spatial-temporal reasoning, testing and verification, and type systems.

Although CHR is Turing complete,[3] it is not commonly used as a programming language in its own right. Rather, it is used to extend a host language with constraints. Prolog is by far the most popular host language and CHR is included in several Prolog implementations, including SICStus and SWI-Prolog, but CHR implementations also exist for Haskell, Java and C.[4]

A CHR program, sometimes called a constraint handler, is a sequence of guarded rules for simplification, propagation, and "simpagation" (a mix of simplification and propagation) of conjunctions of constraints. The CHR constraint store is a multi-set. In contrast to Prolog, the rules are multi-headed and are executed in a committed-choice manner using a forward chaining algorithm.

Example program[edit]

The following CHR program, in Prolog syntax, contains four rules that implement a solver for a less-or-equal constraint. The rules are labeled for convenience (labels are optional in CHR).

% X leq Y means variable X is less-or-equal to variable Y 
reflexivity  @ X leq X <=> true.
antisymmetry @ X leq Y, Y leq X <=> X = Y.
transitivity @ X leq Y, Y leq Z ==> X leq Z.
idempotence  @ X leq Y \ X leq Y <=> true.

The rules can be read in two ways. In the declarative reading, three of the rules specify the axioms of a partial ordering:

  • Reflexivity: XX
  • Antisymmetry: if XY and YX, then X = Y
  • Transitivity: if XY and YZ, then XZ

All three rules are implicitly universally quantified (upper-cased identifiers are variables in Prolog syntax). The idempotence rule is a tautology from the logical viewpoint, but has a purpose in the second reading of the program.

The second way to read the above is as a computer program for maintaining a constraint store, a collection of facts (constraints) about objects. The constraint store is not part of this program, but must be supplied separately. The rules express the following rules of computation:

  • Reflexivity is a simplification rule: it expresses that, if a fact of the form XX is found in the store, it may be removed.
  • Antisymmetry is also a simplification rule, but with two heads. If two facts of the form XY and YX can be found in the store (with matching X and Y), then they can be replaced with the single fact X = Y. Such an equality constraint is considered "built into" the language, and implemented as a unification that is typically handled by the underlying Prolog system.
  • Transitivity is a propagation rule. Unlike simplification, it does not remove anything from the constraint store; instead, when facts of the form XY and YZ (with the same value for Y) are in the store, a third fact XZ may be added.
  • Idempotence, finally, is a simpagation rule, a combined simplification and propagation. When it finds duplicate facts, it removes them from the store. Duplicates may occur because constraint stores are multisets of facts.

Execution of the program proceeds by exhaustively applying the rules to a given input query, which specifies the initial constraint store. For example, given the query

A leq B, B leq C, C leq A

the following transformations will occur:

Current expression Rule applicable to expression Conclusion from rule application
A leq B, B leq C, C leq A transitivity A leq C
A leq B, B leq C, C leq A, A leq C antisymmetry A = C
A leq B, B leq A, A = C antisymmetry A = B
A = B, A = C none

The transitivity rule adds A leq C. Then, by applying the antisymmetry rule, A leq C and C leq A are removed and replaced by A = C. Now the antisymmetry rule becomes applicable on the first two constraints of the original query. Now all CHR constraints are eliminated, so no further rules can be applied, and the answer A = B, A = C is returned: CHR has correctly inferred that all three variables must refer to the same object.

Execution of CHR programs[edit]

CHR executes a program (set of rules) by applying rules to the constraint store until no rule matches anymore, unless a built-in "false" constraint is produced by any rule, signifying a contradiction. To decide which rule should "fire" on a given constraint store, a CHR implementation must use some pattern matching algorithm. Candidate algorithms include RETE and TREATS, but most implementation use a lazy algorithm called LEAPS.[5]

Most applications of CHRs require that the rewriting process be confluent; otherwise the results of searching for a satisfying assignment will be nondeterministic and unpredictable. Establishing confluence is usually done by way of the following three properties [2]

  • A CHR program is locally confluent if all its critical pairs are joinable
  • A CHR program is called terminating if there are no infinite computations.
  • A terminating CHR program is confluent if all its critical pairs are joinable.

See also[edit]

References[edit]

  1. ^ Thom Frühwirth. Introducing Simplification Rules. Internal Report ECRC-LP-63, ECRC Munich, Germany, October 1991, Presented at the Workshop Logisches Programmieren, Goosen/Berlin, Germany, October 1991 and the Workshop on Rewriting and Constraints, Dagstuhl, Germany, October 1991.
  2. ^ a b Thom Frühwirth. Theory and Practice of Constraint Handling Rules. Special Issue on Constraint Logic Programming (P. Stuckey and K. Marriott, Eds.), Journal of Logic Programming, Vol 37(1-3), October 1998. doi:10.1016/S0743-1066(98)10005-5
  3. ^ Jon Sneyers, Tom Schrijvers, Bart Demoen: The computational power and complexity of constraint handling rules. ACM Trans. Program. Lang. Syst. 31(2): (2009).
  4. ^ Peter Van Weert; Pieter Wuille; Tom Schrijvers; Bart Demoen. "CHR for imperative host languages". Constraint Handling Rules — Current Research Topics. Springer. 
  5. ^ Leslie De Koninck (2008). Execution Control for Constraint Handling Rules (Ph.D. thesis). Katholieke Universiteit Leuven. pp. 12–14. 

Further reading[edit]

  • Jon Sneyers, Peter Van Weert, Tom Schrijvers and Leslie De Koninck: As Time Goes By: Constraint Handling Rules – A Survey of CHR Research between 1998 and 2007. Theory and Practice of Logic Programming, 10(1):1-47, 2010. doi:10.1017/S1471068409990123
  • Thom Frühwirth: Constraint Handling Rules. ISBN 9780521877763, Cambridge University Press, 2009.
  • Thom Frühwirth and Frank Raiser (editors): Constraint Handling Rules: Compilation, Execution, and Analysis. ISBN 978-3-83-911591-6, BOD, 2011.

External links[edit]