Constraint Handling Rules in SWI Prolog: What's the order of puting a constraint to the store?

Question

I am learning Constraint Handling Rules (CHR) in swi-prolog.

I started with the tutorial from Tom Schrijvers' Constraint Handling RulesA Tutorial for (Prolog) Programmers.

The confusion part is that what's the order of putting a constraint to the constraint store?

1. p.69 shows that when a rule fires, add the body to (front of) query.

2. p.104 - p.106 show that normally, the order of putting a constraint to the store follows the query order. That is the second constraint (piggy(1)) will be placed at the right of the first constraint (piggy(5)) in the store.

3. p.107, according to 1, piggy(6) be added to the front of query and then be put to the store.

4. p.108, the strange thing happen, why piggy(4) be put to the front of the store (left to piggy(6)) ?

5. p.109 - p.110, more strange thing is that after the rule fired, piggy(10) be added to the store and then piggy(2) be added to the end of the store (right to piggy(10))?

My first question is what's exactly the order of putting a constraint to the constraint store?

For example,

:- use_module(library(chr)).
:- chr_constraint philosophers_stone/0, lead1/0, lead2/0, gold1/0, gold2/0.
philosophers_stone \ lead1 <=> gold1.
philosophers_stone \ lead2 <=> gold2.

?- lead1, lead2, philosophers_stone.

Why the result of the query in swi-prolog is:

philosophers_stone,
gold1,
gold2

instead of

philosophers_stone,
gold2,
gold1

The slow motion is (in my understanding):

query: lead1, lead2, philosophers_stone.
store: 

query: 
store: lead1, lead2, philosophers_stone.

query: gold1
store: lead2, philosophers_stone

query: gold2, gold1 <---- added to (front of) query
store: philosophers_stone

query: 
store: philosophers_stone, gold2, gold1

It seems that when a rule fires, the body should be added to (end of) query? Is that right?

query: lead1, lead2, philosophers_stone.
store: 

query: 
store: lead1, lead2, philosophers_stone.

query: gold1
store: lead2, philosophers_stone

query: gold1, gold2   <---- added to (end of) query
store: philosophers_stone

query: 
store: philosophers_stone, gold1, gold2 <--- then correct

My second question is the order sensitive?

I mean that even if the putting orders are different, the result will eventually confluent up to reordering the stable store? Can I safely ignore this order? I know that the order of rules is very sensitive in swi-prolog's CHR implementation and they can not be ignored.

Thanks.

Answer 1

According to both my memory and https://en.wikipedia.org/wiki/Constraint_Handling_Rules, the constaint store is a multi-set. Therefore it has no ordering at all. (If it were ordered, we would call it a list, not a multi-set.)

As for your example, I also get:

?- lead1, lead2, philosophers_stone.
philosophers_stone,
gold1,
gold2.

But also:

?- lead2, lead1, philosophers_stone.
philosophers_stone,
gold1,
gold2.

Digging a bit into the source of chr_show_store/1 and thence into '$enumerate_constraints'/2, it looks like the store is printed in the order that you declared the constraints. It also looks like each constraint manages its instances independently, that is, there is no central "constraint store" at all. Each constraint is associated with its own list of instances.

There is some ordering to execution: "Active constraint traverses the rules top-to-bottom to find any that fire", but some parts of this are unspecifed (page 214). So you're not supposed to write programs that are very sensitive to ordering issues.

As for the piggy example, it looks to me like the placement of the piggies is optimized for avoiding them moving around too much when the slides are presented during a talk. I don't think their placement is supposed to suggest an actual left-to-right order.