Content deleted Content added
→Example program: Adding wikilinks Tag: Disambiguation links added |
|||
| (6 intermediate revisions by 4 users not shown) | |||
Line 12:
| 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 [[
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==
Line 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 \,|\, b_1, \dots, b_o</math>. When they match the ''heads'' <math>h_1, \dots, h_n</math> and the ''[[
* 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.
Line 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).
<syntaxhighlight lang="
% X leq Y means variable X is less-or-equal to variable Y
reflexivity @ X leq X <=> true.
Line 48:
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 95:
| pages = 42–47
| ___location = Seattle, Washington
|
}}</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>
| |||