Content deleted Content added
m Reverted 1 edit by 2603:7081:7900:7977:A784:50A0:909F:D37E (talk) to last revision by Joyous! |
→Example program: Adding wikilinks Tag: Disambiguation links added |
||
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.
| |||