{{Short description|Concurrent constraint logic programming language}} {{Infobox programming language | name = Constraint Handling Rules (CHR) | paradigms = [[Constraint logic programming|Constraint logic]], [[Declarative programming|declarative]] | year = {{Start date and age|1991}} | designer = Thom Frühwirth | implementations = | dialects = | influenced by = [[Prolog]] | influenced = | file ext = | wikibooks = }} '''Constraint Handling Rules''' ('''CHR''') is a [[declarative programming|declarative]], rule-based [[programming language]], introduced in 1991 by Thom Frühwirth at the time with European Computer-Industry Research Centre (ECRC) in Munich, Germany.<ref>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.</ref><ref name="chrtheorypractice">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}}</ref> Originally intended for [[constraint programming]], CHR finds applications in [[grammar induction]],<ref>Dahl, Veronica, and J. Emilio Miralles. "[https://lirias.kuleuven.be/bitstream/123456789/360286/1/CW624.pdf#page=40 Womb grammars: Constraint solving for grammar induction]." Proceedings of the 9th Workshop on Constraint Handling Rules. vol. Technical report CW. Vol. 624. 2012.</ref> [[type system]]s,<ref>Alves, Sandra, and Mário Florido. "[https://www.sciencedirect.com/science/article/pii/S1571066104803463/pdf?md5=86d0945f0ac4c840c07e43090600bd34&pid=1-s2.0-S1571066104803463-main.pdf Type inference using constraint handling rules]." Electronic Notes in Theoretical Computer Science 64 (2002): 56-72.</ref> [[abductive reasoning]], [[multi-agent system]]s, [[natural language processing]], [[Compiler|compilation]], [[Scheduling (production processes)|scheduling]], [[spatial-temporal reasoning]], [[Software testing|testing]], and [[Software verification|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 programming|non-deterministic]],<ref name="timegoesby">{{Cite journal |doi=10.1017/S1471068409990123 |title=As time goes by: Constraint Handling Rules – A Survey of CHR Research between 1998 and 2007 |journal=Theory and Practice of Logic Programming |volume=10 |pages=1 |year=2009 |last1=Sneyers |first1=Jon |last2=Van Weert |first2=Peter |last3=Schrijvers |first3=Tom |last4=De Koninck |first4=Leslie |url=http://dtai.cs.kuleuven.be/projects/CHR/papers/draft_chr_survey.pdf |arxiv=0906.4474|s2cid=11044594 }}</ref> according to its ''abstract [[Semantics (computer science)|semantics]]'' and deterministic (top-down rule application), according to its ''refined semantics''.<ref name="chrbook">{{cite book |last1=Frühwirth |first1=Thom |title=Constraint handling rules |date=2009 |publisher=Cambridge University Press |isbn=978-0521877763}}</ref>

Although CHR is [[Turing complete]],<ref name="complexity">{{cite journal |first1=Jon |last1=Sneyers |first2=Tom |last2=Schrijvers |first3=Bart |last3=Demoen |title=The computational power and complexity of constraint handling rules |journal=[[ACM Transactions on Programming Languages and Systems]] |volume=31 |issue=2 |year=2009 |pages=1–42 |doi=10.1145/1462166.1462169 |s2cid=2691882 |url=https://lirias.kuleuven.be/bitstream/123456789/218524/1/p1-sneyers.pdf}}</ref> 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 (programming language)|Haskell]],<ref>{{Cite web|url=https://github.com/atzedijkstra/chr|title = CHR: Constraint Handling Rules library| website=[[GitHub]] |date = 5 September 2021}}</ref> [[Java (programming language)|Java]], [[C (programming language)|C]],<ref name="imperative">{{cite encyclopedia |title=CHR for imperative host languages |author1=Peter Van Weert |author2=Pieter Wuille |author3=Tom Schrijvers |author4=Bart Demoen |encyclopedia=Constraint Handling Rules: Current Research Topics |publisher=Springer |url=https://lirias.kuleuven.be/handle/123456789/197033}}</ref> [[SQL]],<ref>{{Cite web|url=https://github.com/awto/chr2sql|title = CHR2 to SQL converter| website=[[GitHub]] |date = 15 March 2021}}</ref> and JavaScript.<ref>[https://fnogatz.github.io/paper-now-chrjs/ CHR.js - A CHR Transpiler for JavaScript]</ref> 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 [[Term algebra|terms]], including [[logical variable]]s. 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 [[Prolog syntax and semantics#Data types|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:<ref name="timegoesby"/>

* Simplification rules have the form <math>h_1, \dots, h_n \Longleftrightarrow g_1, \dots, g_m \,|\, b_1, \dots, b_o</math>. When they match the ''heads'' <math>h_1, \dots, h_n</math> and the ''[[Guard (computer science)|guards]]'' <math>g_1, \dots, g_m</math> hold, simplification rules may rewrite the heads into the ''body'' <math>b_1, \dots, b_o</math>. * Propagation rules have the form <math>h_1, \dots, h_n \Longrightarrow g_1, \dots, g_m \,|\, b_1, \dots, b_o</math>. These rules add the constraints in the body to the store, without removing the heads. * ''Simpagation'' rules combine simplification and propagation. They are written <math>h_1, \dots, h_\ell \,\backslash\, h_{\ell+1}, \dots, h_n \Longleftrightarrow g_1, \dots, g_m \,|\, b_1, \dots, b_o</math>. For a simpagation rule to fire, the constraint store must match all the rules in the head and the guards must hold true. The <math>\ell</math> constraints before the <math>\backslash</math> are kept, as a in a propagation rule; the remaining <math>n - \ell</math> constraints are removed.

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

:<math>H_k \,\backslash\, H_r \Longleftrightarrow G \,|\, B</math>

where each of <math>H_k, H_r, G, B</math> is a conjunction of constraints: <math>H_k, H_r</math> and <math>B</math> contain CHR constraints, while the guards <math>G</math> are built-in. Only one of <math>H_k, H_r</math> 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 <code>true</code> (the constraint that always holds), <code>fail</code> (the constraint that never holds, and is used to signal failure) and equality of terms, i.e., [[unification (computer science)|unification]].<ref name="complexity"/> When the host language does not support these features, they must be implemented along with CHR.<ref name="imperative"/>

Execution of a CHR program starts with an initial constraint store. The program then proceeds by [[pattern matching|matching rules]] against the store and applying them, until either no more rules match (success) or the <code>fail</code> 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.<ref name="imperative"/>

===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). <syntaxhighlight lang="logtalk"> % 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. </syntaxhighlight> The rules can be read in two ways. In the declarative reading, three of the rules specify the [[Partially ordered set#Formal definition|axioms of a partial ordering]]:

* [[Reflexive relation|Reflexivity]]: ''X'' ≤ ''X'' * [[Antisymmetry]]: if ''X'' ≤ ''Y'' and ''Y'' ≤ ''X'', then ''X'' = ''Y'' * [[Transitive relation|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 (logic)|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 (computing)|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:

{| class="wikitable" |- ! Current constraints !! Rule applicable to constraints !! Conclusion from rule application |- | <code>A leq B, B leq C, C leq A</code> || transitivity || <code>A leq C</code> |- | <code>A leq B, B leq C, C leq A, A leq C</code> || antisymmetry || <code>A = C</code> |- | <code>A leq B, B leq A, A = C</code> || antisymmetry || <code>A = B</code> |- | <code>A = B, A = C</code>||none|| |}

The ''transitivity'' rule adds <code>A leq C</code>. Then, by applying the ''antisymmetry'' rule, <code>A leq C</code> and <code>C leq A</code> are removed and replaced by <code>A = C</code>. 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 <code>A = B, A = C</code> 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 algorithm|RETE]] and [[TREAT]],<ref> {{cite conference | url = https://www.aaai.org/Papers/AAAI/1987/AAAI87-008.pdf | title = TREAT: A Better Match Algorithm for AI Production Systems | last1 = Miranker | first1 = Daniel P. | author-link1 = Daniel P. Miranker | date = July 13–17, 1987 | publisher = Association for the Advancement of Artificial Intelligence, AAAI | book-title = AAAI'87: Proceedings of the sixth National conference on Artificial intelligence | pages = 42–47 | location = Seattle, Washington | isbn = 978-0-262-51055-4 }}</ref> but most implementation use a [[Lazy evaluation|lazy]] algorithm called [[LEAPS (algorithm)|LEAPS]].<ref>{{cite thesis |url=http://www.cs.kuleuven.be/publicaties/doctoraten/cw/CW2008_14.pdf |title=Execution Control for Constraint Handling Rules |author=Leslie De Koninck |year=2008 |publisher=[[Katholieke Universiteit Leuven]] |type=Ph.D. thesis |pages=12–14}}</ref>

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.<ref name="timegoesby"/><ref>{{cite book |first1=Gregory J. |last1=Duck |first2=Peter J. |last2=Stuckey |first3=María |last3=García de la Banda |author3-link=María García de la Banda|first4=Christian |last4=Holzbaur |title=Logic Programming |chapter=The Refined Operational Semantics of Constraint Handling Rules |series=Lecture Notes in Computer Science |year=2004 |volume=3132 |pages=90–104 |doi=10.1007/978-3-540-27775-0_7 |isbn=978-3-540-22671-0 |chapter-url=http://ww2.cs.mu.oz.au/~pjs/papers/refined.pdf |access-date=2014-12-23 |archive-url=https://web.archive.org/web/20110304133204/http://ww2.cs.mu.oz.au/~pjs/papers/refined.pdf |archive-date=2011-03-04 |url-status=dead }}</ref>

Most applications of CHRs require that the rewriting process be [[confluence (abstract rewriting)|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:<ref name="chrtheorypractice" />

* A CHR program is ''locally confluent'' if all its [[Critical pair (logic)|critical pairs]] are [[Rewriting#Normal forms, joinability and the word problem|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 logic programming]] *[[Logic programming]] *[[Production system (computer science)]] *[[Business rules engine]]s *[[Rewriting]]

==References== {{Reflist}}

==Further reading== * Christiansen, Henning. "[https://arxiv.org/abs/cs/0408027 CHR grammars]." Theory and Practice of Logic Programming 5.4-5 (2005): 467-501.

==External links== * {{Official website|constraint-handling-rules.org}} * [http://dtai.cs.kuleuven.be/CHR/biblio/ CHR Bibliography] * [http://listserv.cc.kuleuven.ac.be/archives/chr.html The CHR mailing list] * [http://dtai.cs.kuleuven.be/CHR/ The K.U.Leuven CHR System] * [http://chr.informatik.uni-ulm.de/~webchr/ WebCHR: a CHR web interface]

[[Category:Constraint logic programming]] [[Category:Declarative programming languages]] [[Category:Constraint programming languages]] [[Category:Concurrent programming languages]]