Constraint Handling Rules: Difference between revisions

Revision as of 17:15, 12 April 2019

Revision as of 05:11, 9 July 2019

Line 83:

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 [[TREATS]], 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>

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 journal |first1=Gregory J. |last1=Duck |first2=Peter J. |last2=Stuckey |first3=María |last3=García de la Banda |first4=Christian |last4=Holzbaur |title=The refined operational semantics of Constraint Handling Rules |journal=Logic Programming |year=2004 |pages=90–104 |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 |dead-url=yes }}</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" />