HOME

TheInfoList



OR:

Constraint Handling Rules (CHR) is a declarative, rule-based
programming language A programming language is a system of notation for writing computer programs. Programming languages are described in terms of their Syntax (programming languages), syntax (form) and semantics (computer science), semantics (meaning), usually def ...
, introduced in 1991 by Thom Frühwirth at the time with European Computer-Industry Research Centre (ECRC) in Munich, Germany.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 The ''Journal of Logical and Algebraic Methods in Programming'' is a peer-reviewed scientific journal established in 1984. It was originally titled ''The Journal of Logic Programming''; in 2001 it was renamed ''The Journal of Logic and Algebraic Pr ...
, Vol 37(1-3), October 1998.
Originally intended for
constraint programming Constraint programming (CP) is a paradigm for solving combinatorial problems that draws on a wide range of techniques from artificial intelligence, computer science, and operations research. In constraint programming, users declaratively state t ...
, CHR finds applications in grammar induction,
type system In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a ''type'' (for example, integer, floating point, string) to every '' term'' (a word, phrase, or other set of symbols). Usu ...
s,
abductive reasoning Abductive reasoning (also called abduction,For example: abductive inference, or retroduction) is a form of logical inference that seeks the simplest and most likely conclusion from a set of observations. It was formulated and advanced by Ameri ...
, multi-agent systems,
natural language processing Natural language processing (NLP) is a subfield of computer science and especially artificial intelligence. It is primarily concerned with providing computers with the ability to process data encoded in natural language and is thus closely related ...
, compilation, scheduling, spatial-temporal reasoning, testing, and verification. 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, according to its ''abstract
semantics Semantics is the study of linguistic Meaning (philosophy), meaning. It examines what meaning is, how words get their meaning, and how the meaning of a complex expression depends on its parts. Part of this process involves the distinction betwee ...
'' and deterministic (top-down rule application), according to its ''refined semantics''. Although CHR is Turing complete, 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 Haskell () is a general-purpose, statically typed, purely functional programming language with type inference and lazy evaluation. Designed for teaching, research, and industrial applications, Haskell pioneered several programming language ...
,
Java Java is one of the Greater Sunda Islands in Indonesia. It is bordered by the Indian Ocean to the south and the Java Sea (a part of Pacific Ocean) to the north. With a population of 156.9 million people (including Madura) in mid 2024, proje ...
, C, SQL, and JavaScript. 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: * Simplification rules have the form h_1, \dots, h_n \Longleftrightarrow g_1, \dots, g_m \,, \, b_1, \dots, b_o. When they match the ''heads'' h_1, \dots, h_n and the '' guards'' g_1, \dots, g_m hold, simplification rules may rewrite the heads into the ''body'' b_1, \dots, b_o. * Propagation rules have the form h_1, \dots, h_n \Longrightarrow g_1, \dots, g_m \,, \, b_1, \dots, b_o. These rules add the constraints in the body to the store, without removing the heads. * ''Simpagation'' rules combine simplification and propagation. They are written h_1, \dots, h_\ell \,\backslash\, h_, \dots, h_n \Longleftrightarrow g_1, \dots, g_m \,, \, b_1, \dots, b_o. For a simpagation rule to fire, the constraint store must match all the rules in the head and the guards must hold true. The \ell constraints before the \backslash are kept, as a in a propagation rule; the remaining n - \ell constraints are removed. Since simpagation rules subsume simplification and propagation, all CHR rules follow the format :H_k \,\backslash\, H_r \Longleftrightarrow G \,, \, 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. When the host language does not support these features, they must be implemented along with CHR. 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.


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: * Reflexivity: ''X'' ≤ ''X'' * Antisymmetry: if ''X'' ≤ ''Y'' and ''Y'' ≤ ''X'', then ''X'' = ''Y'' * Transitivity: if ''X'' ≤ ''Y'' and ''Y'' ≤ ''Z'', then ''X'' ≤ ''Z'' 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 ''X'' ≤ ''X'' 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 ''X'' ≤ ''Y'' and ''Y'' ≤ ''X'' 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 in, 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 ''X'' ≤ ''Y'' and ''Y'' ≤ ''Z'' (with the same value for ''Y'') are in the store, a third fact ''X'' ≤ ''Z'' 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 multi-sets of facts. Given the query A leq B, B leq C, C leq A the following transformations may occur: 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 In computer science, pattern matching is the act of checking a given sequence of tokens for the presence of the constituents of some pattern. In contrast to pattern recognition, the match usually must be exact: "either it will or will not be a ...
algorithm. Candidate algorithms include RETE and TREAT, but most implementation use a lazy algorithm called LEAPS. 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. 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: * 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

*
Constraint programming Constraint programming (CP) is a paradigm for solving combinatorial problems that draws on a wide range of techniques from artificial intelligence, computer science, and operations research. In constraint programming, users declaratively state t ...
*
Constraint logic programming Constraint logic programming is a form of constraint programming, in which logic programming is extended to include concepts from constraint satisfaction. A constraint logic program is a logic program that contains constraints in the body of claus ...
*
Logic programming Logic programming is a programming, database and knowledge representation paradigm based on formal logic. A logic program is a set of sentences in logical form, representing knowledge about some problem domain. Computation is performed by applyin ...
* Production system (computer science) *
Business rules engine A business rules engine is a software system that executes one or more business rules in a runtime production environment. The rules might come from legal regulation ("An employee can be fired for any reason or no reason but not for an illegal r ...
s * Rewriting


References


Further reading

* Christiansen, Henning.
CHR grammars
" Theory and Practice of Logic Programming 5.4-5 (2005): 467-501.


External links

* {{Official website, constraint-handling-rules.org
CHR Bibliography



The K.U.Leuven CHR System

WebCHR: a CHR web interface
Constraint logic programming Declarative programming languages Constraint programming languages Concurrent programming languages