Constraint Handling Rules: Difference between revisions

Revision as of 22:45, 6 April 2025

Latest revision as of 08:52, 20 August 2025

(3 intermediate revisions by 2 users not shown)

Line 12:

| wikibooks =

}}

'''HookerConstraint 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>

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="prologlogtalk">

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