Constraint Handling Rules: Difference between revisions

Revision as of 13:35, 24 January 2017

Latest revision as of 08:52, 20 August 2025

(48 intermediate revisions by 26 users not shown)

Line 1:

{{Short description|Concurrent constraint logic programming language}}

{{Infobox programming language

| paradigm name = [[Constraint logicHandling Rules programming]](CHR)

| paradigms = [[Constraint logic programming|Constraint logic]], [[Declarative programming|declarative]]

| year = 1991

| year = {{Start date and age|1991}}

| designer = Thom Frühwirth

| implementations =

| dialects =

| influenced by = [[Prolog]]

| influenced =

| file_ext file ext =

| wikibooks =

}}

'''Constraint Handling Rules''' ('''CHR''') is a [[declarative programming|declarative]], rule-based [[programming language|language]], introduced in 1991 by Thom Frühwirth at the time inwith theEuropean UniversityComputer-Industry ofResearch UlmCentre (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]], and [[type system]]s.

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 10| pages = 1| |year =2009 2009| last1 = Sneyers | first1 =Jon Jon| last2 = Van Weert | first2 =Peter Peter| last3 = Schrijvers | first3 =Tom Tom| last4 = De Koninck | first4 =Leslie 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 Trans.Transactions Program.on Lang.Programming Syst.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 Prolog|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==

Line 21 ⟶ 23:

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 \Longleftrightarrow,|\, 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 \Longrightarrow,|\, 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 \Longleftrightarrow,|\, 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 \Longleftrightarrow,|\, 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.

Line 37 ⟶ 39:

===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).

<sourcesyntaxhighlight lang="prologlogtalk">

% X leq Y means variable X is less-or-equal to variable Y

reflexivity @ X leq X <=> true.

Line 43 ⟶ 45:

transitivity @ X leq Y, Y leq Z ==> X leq Z.

idempotence @ X leq Y \ X leq Y <=> true.

</syntaxhighlight>

</source>

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]]:

* [[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 (logic)|tautology]] from the logical viewpoint, but has a purpose in the second reading of the program.

Line 81 ⟶ 83:

== 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 [[TREATSTREAT]], but most implementation use a [[Lazy evaluation|lazy]] algorithm called [[LEAPS (algorithm)|LEAPS]].<ref>{{cite thesis |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>

{{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 journalbook |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 refinedRefined operationalOperational semanticsSemantics of Constraint Handling Rules |journalseries=LogicLecture ProgrammingNotes 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''.

Line 95 ⟶ 110:

*[[Constraint logic programming]]

*[[Logic programming]]

*[[Production system (computer science)|Production rule system]]s

*[[Business rules engine]]s

*[[Rewriting]]

Line 103 ⟶ 118:

==Further reading==

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

{{refbegin}}

* 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.

{{refend}}

==External links==

* {{Official website|constraint-handling-rules.org}}

* [http://dtai.cs.kuleuven.be/CHR/ The CHR Home Page]

* [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]]