SWI-Prolog中Constraint Handling Rules(CHR)约束存储顺序相关问题

问题1：约束存入约束存储的准确顺序规则 #

你遇到的推导和实际运行结果不一致的核心原因是：Tom Schrijvers的教程中p69描述的是CHR抽象操作语义ω₀的规则，仅用于理论推导和合流性证明，而SWI-Prolog的CHR库默认采用面向实际生产的精化操作语义ωᵣ，二者对规则体生成约束的入队策略完全不同。
SWI-Prolog CHR默认的约束存储顺序规则如下：

• 用户显式写在查询中的约束，按从左到右的顺序进入查询队列，未被规则消费的约束按处理顺序追加到约束存储的尾部，和教程p104-p106的描述一致。
• 规则触发后生成的规则体约束，默认追加到查询队列的尾部（FIFO调度），而非抽象语义描述的头部，这就是你给出的示例运行结果为philosophers_stone, gold1, gold2的原因，你后续按尾部入队的推导完全符合SWI-Prolog的默认实现逻辑。
  如果需要切换为教程中抽象语义的LIFO行为，可以在代码开头添加编译选项：

:- chr_option(queue_strategy, lifo).

添加后运行你给出的查询，就会得到你最初推导的philosophers_stone, gold2, gold1的结果。
你在教程中看到的不同页码的存入顺序差异，本质是不同章节分别演示了抽象语义、不同编译选项下的行为，不属于反常情况。

问题2：约束存储顺序是否敏感 #

如果你的CHR程序是合流的，即无论约束调度顺序、规则匹配顺序如何，最终稳定约束存储仅存在顺序差异，不存在约束种类、数量的区别，你可以完全安全忽略存储顺序，不会影响程序的正确性：CHR的规则匹配默认基于约束的逻辑属性，而非约束在存储中的位置，顺序差异不会触发不同的规则匹配结果。
仅两种情况需要关注存储顺序：

1. 你的程序本身不合流，不同的执行顺序会导致最终约束的种类、数量产生差异，此时顺序会影响程序正确性，你需要先调整程序保证合流，或主动控制调度策略。
2. 你需要对最终约束存储做遍历输出、或使用了依赖存储顺序的CHR扩展功能（如自定义匹配优先级），此时顺序差异会影响输出或功能逻辑，需要显式指定队列策略。

内容的提问来源于stack exchange，提问作者chansey