我正在仔细研究约束处理规则（CHR），看看我是否能理解它们（从某种意义上说，这里计算的是什么以及经典逻辑甚至线性逻辑如何适应其中）并可能应用它们。
Thom Frühwirth于 2009 年出版的书中讨论了 CHR 的原理，但实施当然可能不同。
在这种情况下，我使用CHR 的 SWI Prolog 实现。
如果我理解得很好：
- CHR 的实现将提供至少一个“约束存储”来表达“计算的状态”。约束存储仅包含基本原子（即正字面量）。
- 在典型的 CHR 会话中，首先设置具有初始状态的约束存储。一个人编写 CHR 程序，其中包含 CHR 规则。然后以约束存储作为参数运行 CHR 程序。重复应用正向链接 CHR 规则直到不再有任何规则适用，这将迭代地（并且破坏性地）将约束存储从其初始状态转换为某个最终状态。然后可以检查约束存储以找到所需的答案。
- 在这种情况下，只考虑不关心非确定性（“承诺选择非确定性”）：当多个规则适用于任何中间状态时，任何一个都会被采用。
- 不考虑在以后失败的情况下回溯到选择点的“不知道”非确定性——如果需要，由实现以一种或另一种方式提供它。
作为一个练习，一个使用欧几里得算法计算 GCD 并保留操作日志的最简单程序：
% Constraint `logg(Ti,Msg)` retains the log message `Msg` at step `Ti`
% (which increases monotonically)
% Constraint `gcdpool(X)` denotes a "GCD pool member". At each step, we want
% to compute the GCD of all the X for which there is a `gcdpool(X)` constraint
% in the constraint store. A CHR transformation of the store always reduces the
% sum of the X (variant) while keeping the GCD of the GCD pool members constant
% (invariant). We will thus find a solution eventually.
:- module(my_gcd, [ gcdpool/1, logg/2 ]).
:- use_module(library(chr)).
:- chr_constraint gcdpool/1, logg/2.
% pool contains duplicate: drop one!
gcdpool(N) \ gcdpool(N),logg(Ti,Msg) <=> To is Ti+1, logg(To,[[drop,[N,N],[N]]|Msg]).
% pool contains 1 and anything not 1: keep only 1
gcdpool(1) \ gcdpool(N),logg(Ti,Msg) <=> 1<N | To is Ti+1, logg(To,[[drop,[1,N],[N]]|Msg]).
% otherwise
gcdpool(N) \ gcdpool(M),logg(Ti,Msg) <=> 0<N, N<M | To is Ti+1,
V is M-N,
gcdpool(V),
logg(To,[[diff,[N,M],[N,V]]|Msg]).
这一切都非常简单。SWI Prolog 中的测试运行
?- use_module(library(chr)).
?- [gcd].
?- chr_trace.
% now we enter a goal:
?- gcdpool(6),gcdpool(3),logg(0,[]).
CHR: (0) Insert: gcdpool(6) # <907>
CHR: (1) Call: gcdpool(6) # <907> ? [creep]
CHR: (1) Exit: gcdpool(6) # <907> ? [creep]
CHR: (0) Insert: gcdpool(3) # <908>
CHR: (1) Call: gcdpool(3) # <908> ? [creep]
CHR: (1) Exit: gcdpool(3) # <908> ? [creep]
CHR: (0) Insert: logg(0,[]) # <909>
CHR: (1) Call: logg(0,[]) # <909> ? [creep]
CHR: (1) Try: gcdpool(3) # <908> \ gcdpool(6) # <907>, logg(0,[]) # <909> <=> 0<3,3<6 | _71386 is 0+1,_71404 is 6-3,gcdpool(_71404),logg(_71386,[[diff,[3,6],[3,_71404]]]).
CHR: (1) Apply: gcdpool(3) # <908> \ gcdpool(6) # <907>, logg(0,[]) # <909> <=> 0<3,3<6 | _71386 is 0+1,_71404 is 6-3,gcdpool(_71404),logg(_71386,[[diff,[3,6],[3,_71404]]]). ? [creep]
CHR: (1) Remove: gcdpool(6) # <907>
CHR: (1) Remove: logg(0,[]) # <909>
CHR: (1) Insert: gcdpool(3) # <910>
CHR: (2) Call: gcdpool(3) # <910> ? [creep]
CHR: (2) Exit: gcdpool(3) # <910> ? [creep]
CHR: (1) Insert: logg(1,[[diff,[3,6],[3,3]]]) # <911>
CHR: (2) Call: logg(1,[[diff,[3,6],[3,3]]]) # <911> ? [creep]
CHR: (2) Try: gcdpool(3) # <908> \ gcdpool(3) # <910>, logg(1,[[diff,[3,6],[3,3]]]) # <911> <=> _78066 is 1+1,logg(_78066,[[drop,[3,3],[3]],[diff,[3,6],[3,3]]]).
CHR: (2) Apply: gcdpool(3) # <908> \ gcdpool(3) # <910>, logg(1,[[diff,[3,6],[3,3]]]) # <911> <=> _78066 is 1+1,logg(_78066,[[drop,[3,3],[3]],[diff,[3,6],[3,3]]]). ? [creep]
CHR: (2) Remove: gcdpool(3) # <910>
CHR: (2) Remove: logg(1,[[diff,[3,6],[3,3]]]) # <911>
CHR: (2) Insert: logg(2,[[drop,[3,3],[3]],[diff,[3,6],[3,3]]]) # <912>
CHR: (3) Call: logg(2,[[drop,[3,3],[3]],[diff,[3,6],[3,3]]]) # <912> ? [creep]
CHR: (3) Exit: logg(2,[[drop,[3,3],[3]],[diff,[3,6],[3,3]]]) # <912> ? [creep]
CHR: (2) Exit: logg(1,[[diff,[3,6],[3,3]]]) # <911> ? [creep]
CHR: (1) Exit: logg(0,[]) # <909> ? [creep]
gcdpool(3),
logg(2, [[drop, [3, 3], [3]], [diff, [3, 6], [3, 3]]]) .
答案由最后两行给出： 约束存储中剩下的唯一约束是gcdpool(3)，所以 3 就是答案。
在实施方面，以下似乎成立：
没有专门的“约束存储”。CHR 程序（以某种方式）被编译到 Prolog 中，并且“CHR 约束”成为“Prolog 谓词”。这样的“约束存储”是称为 Prolog 顶级目标的堆栈（它没有被具体化）。
因此，“约束存储”使用“CHR 目标”中列出的约束进行初始化，并在最终退出时消失。您也不能以逐步或交互的方式设置约束存储，但必须在一行中完成：
gcdpool(6),gcdpool(3),logg(0,[]).
之后，CHR 程序立即开始工作。
事实上，谓词find_chr_constraint/1应该从约束存储中获取数据，一旦 CHR 程序运行，它什么也不返回。因为不再有约束存储。
此外，试图在“CHR 程序”本身中设置约束存储是没有意义的。因此放入logg(0,[])GCD 代码没有任何效果。你必须投入logg(0,[])CHR目标。
问题
- 这种理解正确吗？
- 如何将 CHR 计算结果返回 Prolog？
- Prolog 实现提供的回溯可能性如何处理？如何将其用于 CHR？