Content deleted Content added
m →Execution of CHR programs: Add links to definitions of terms "critical pair" and "joinable." |
m →Execution of CHR programs: Add missing punctuation. |
||
Line 85:
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}}</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
* 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''.
| |||