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