Constraint Handling Rules

Constraint Handling Rules
Paradigm Constraint logic programming
Designed by Thom Frühwirth
First appeared 1991
Influenced by
Prolog

Constraint Handling Rules (CHR) is a declarative, rule-based language, introduced in 1991 by Thom Frühwirth at the time in the University of Ulm.[1][2] Originally intended for constraint programming, CHR finds applications in abductive reasoning, multi-agent systems, natural language processing, compilation, scheduling, spatial-temporal reasoning, testing and verification, and type systems.

A CHR program, sometimes called a constraint handler, is a set of rules that maintain a constraint store, a multi-set of logical formulas. Execution of rules may add or remove formulas from the store, thus changing the state of the program. The order in which rules "fire" on a given constraint store is non-deterministic.[3]

Although CHR is Turing complete,[4] 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, although CHR implementations also exist for Haskell, Java and C.[5] In contrast to Prolog, CHR rules are multi-headed and are executed in a committed-choice manner using a forward chaining algorithm.

Language overview

The concrete syntax of CHR programs depends on the host language, and in fact programs embed statements in the host language that are executed to handle some rules. The host language supplies a data structure for representing terms, including logical variables. Terms represent constraints, which can be thought of as "facts" about the program's problem domain. Traditionally, Prolog is used as the host language, so its data structures and variables are used. The rest of this section uses a neutral, mathematical notation that is common in the CHR literature.

A CHR program, then, consists of rules that manipulate a multi-set of these terms, called the constraint store. Rules come in three types:[3]

Since simpagation rules subsume simplification and propagation, all CHR rules follow the format

H_k \,\backslash\, H_r \,|\, G \Longleftrightarrow B

where each of H_k, H_r, G, B is a conjunction of constraints: H_k, H_r and B contain CHR constraints, while the guards G are built-in. Only one of H_k, H_r needs to be non-empty.

The host language must also define built-in constraints over terms. The guards in rules are built-in constraints, so they effectively execute host language code. The built-in constraint theory must include at least true (the constraint that always holds), fail (the constraint that never holds, and is used to signal failure) and equality of terms, i.e., unification.[4] When the host language does not support these features, they must be implemented along with CHR.[5]

Execution of a CHR program starts with an initial constraint store. The program then proceeds by matching rules against the store and applying them, until either no more rules match (success) or the fail constraint is derived. In the former case, the constraint store can be read off by a host language program to look for facts of interest. Matching is defined as "one-way unification": it binds variables only on one side of the equation. Pattern matching can be easily implemented when as unification when the host language supports it.[5]

Example program

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:

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:

Given the query

A leq B, B leq C, C leq A

the following transformations may occur:

Current constraints Rule applicable to constraints 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 = Cnone

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

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.[6]

The original specification of CHR's semantics was entirely non-deterministic, but the so-called "refined operation semantics" of Duck et al. removed much of the non-determinism so that application writers can rely on the order of execution for performance and correctness of their programs.[3][7]

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]

See also

References

  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. 1 2 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. 1 2 3 Sneyers, Jon; Van Weert, Peter; Schrijvers, Tom; De Koninck, Leslie (2009). "As time goes by: Constraint Handling Rules – A Survey of CHR Research between 1998 and 2007" (PDF). Theory and Practice of Logic Programming 10: 1. doi:10.1017/S1471068409990123.
  4. 1 2 Sneyers, Jon; Schrijvers, Tom; Demoen, Bart (2009). "The computational power and complexity of constraint handling rules" (PDF). ACM Trans. Program. Lang. Syst. 31 (2).
  5. 1 2 3 Peter Van Weert; Pieter Wuille; Tom Schrijvers; Bart Demoen. "CHR for imperative host languages". Constraint Handling Rules — Current Research Topics. Springer.
  6. Leslie De Koninck (2008). Execution Control for Constraint Handling Rules (Ph.D. thesis). Katholieke Universiteit Leuven. pp. 12–14.
  7. Duck, Gregory J.; Stuckey, Peter J.; García de la Banda, María; Holzbaur, Christian (2004). "The refined operational semantics of Constraint Handling Rules" (PDF). Logic Programming: 90–104.

Further reading

  • 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

This article is issued from Wikipedia - version of the Thursday, March 17, 2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.