约束处理规则---CHR（Constraint Handling Rules）语法介绍

我觉得CHR语法挺有趣的，
有时用这套规则来写东西会省事许多，
所以一直想写个教学介绍一下。
本教学写得比较简单，目的是让读者可以快速了解CHR并享受其乐趣，
更详细正式的内容可以参考swi-prolog手册第7章。
下面我们就开始吧！



使用CHR语法一定要先加上这句

代码:

:- use_module(library(chr)).

然后再声明一下CHR约束名称，例如

代码:

:- chr_constraint value/1, result/1.

接下来介绍CHR三大语法规则：化简（simplification）、繁殖（propagation）、合并（simpagation）。

首先是化简规则，比如我定义一条规则如下

代码:

value(X), value(Y) <=> Z is X + Y, value(Z).

查询一下

135 ?- value(1).
value(1)

136 ?- value(1), value(9).
value(10)

可以看到，当我们只提供value(1)一个约束时，
查询结果就是value(1)这个约束；
而当我们提供value(1), value(9)两个约束时，
因为有前面我们定义的化简规则，CHR会把"<=>"左边的约束删掉，
然后创建新的约束value(10).


148 ?- value(1), value(9), value(3).
value(13)

如果提供三个约束，我们发现，它会很聪明的自动加总得到value(13)，
也就是说，我们定义好的规则，在任何时候一旦"手上"（先暂时这么说）有的约束符合情况就会自动套用。
在这里，value(1)和value(9)符合"<=>"左边的要求，所以化简为value(10)，
然后value(10)和value(3)也符合"<=>"左边的要求，最终化简为value(13)。
看！不需要利用递归或循环，就能把所有你给出的数字加起来，
这套处理方式是否让你省事许多。

前面讲"手上"，其实CHR是把约束先放进约束存储（Constraint Store）里，你每提供一个新的约束时，
CHR会再检查约束存储里有没有可以套用你所定义好的规则，若有则自动套用。


与之对照来看一下繁殖规则，假设我定义如下规则：

代码:

value(X) ==> Y is X + 1, result(Y).

155 ?- value(1).
value(1)
result(2)

可以看到， "==>"是在"保留"其左边的约束的基础上，再"新增加"其右边的约束。
而前面提到的化简规则"<=>"则会把value(X)给删除。

前面提到过，任何时候你手上有的约束符合规则定义的条件，就一定会套用。
这里value生出result，就变成一个value加上一个result，
你可能会想，value会不会再次生出一个result，一直循环下去变成无限多个result？
喂…如果是这样的话，繁殖规则还有意义吗？一写这个规则就out of local stack。
这里要认识到，对于同一个value(X)，它只会套用一次而已。

但如果规则写成

代码:

value(X) ==> value(X).

或

代码:

value(X) ==> Y is X + 1, value(Y).

结果都是

157 ?- value(3).
ERROR: Out of local stack

因为其繁殖出的不管是value(3)还是value(4)，CHR都已不再视其为"==>"左边的value(X)，
而前面说过，CHR对于所有符合规则的约束都是会自动套用规则的，
变成value生出value，生出的value又再生出value，再生出的value又再再生出value……永无止尽。


最后是合并规则，假设我定义如下规则：

代码:

result(X) \ value(Y) <=> Z is X + Y, result(Z).

166 ?- result(3).
result(3)

168 ?- value(7).
value(7)

171 ?- result(3), value(7).
result(10)
result(3)

可以看到，单独提供result或value约束都不发生什么变化，
而当result和value同时出现，则配对成功，
根据合并规则，"\"左边的约束会被保留，"\"与"<=>"之间的约束会被替换成"<=>"右边的约束。
此例是value(7)被替换掉，根据规则换成result(10)。



到这里已经将CHR的三大语法规则作了非常简单的介绍，
要特别说明的是，约束的顺序是不重要的，
不存在顺序问题并且实际上你也很难掌握约束在存储里的顺序。
比如在合并规则这个例子里，如果尝试

172 ?- value(7), result(3).
result(10)
result(3)

得到的结果还是一样。可以知道CHR在寻找是否套用规则时，只要约束配对成功就会套用，
并不要求约束存储里的约束排列顺序必须按照规则定义时所列顺序。
查询结果也是一样，CHR的回传并没有按照特定顺序显示查询结果。

既然无法掌握约束的出现顺序，那假如我想写一个减法规则，
并且一定是较大的数减去较小的数，怎么办？
如果简单的写value(X), value(Y) <=> Z is X - Y, value(Z).，
你并不能保证CHR在帮你配对两个value时，一定是X > Y。
解决这个问题的方法非常简单，后面讲到"守卫"的时候会再提起这个问题。



约束的顺序不重要，但规则的顺序一般很重要，
写在前面的优先级较高，优先判断是否执行。

例如定义如下规则：

代码:

result(X) ==> value(X).
result(X) <=> true.

187 ?- result(3).
value(3)

可以看到，约束result先生出value，
然后result才化简为true（就是直接删除result(X)约束的意思），
所以查询结果仍然剩下value(3)。

但如果将顺序反过来

代码:

result(X) <=> true.
result(X) ==> value(X).

191 ?- result(3).
true .

因为先执行result的化简，所以已经没有任何result的约束了，
自然也就无法生出value，看到查询结果只显示true，没有其他任何约束。


再看一个关于规则顺序的说明例子，假设有规则

代码:

value(1), value(2) <=> value(3).
value(1) <=> true.
result(5) <=> value(1), value(2).

如果我提供约束result(5)，那么根据第三条规则，
result(5)会被替换成value(1)、value(2)两约束这是没有疑问的。
但是究竟是一次生成value(1)、value(2)，再按第一条规则化简得到value(3)，
还是当value(1)一出现时，就先按第二条规则删除，再生出value(2)呢？

我们查询一下

18 ?- result(5).
value(2)

很显然，答案是后者。
这里可以看出CHR的运作流程是：
每次只要有新约束出现，CHR都会从头检查一遍有无符合的规则，有则立即套用。



接下来介绍一个非常重要的东西叫Guard（守卫），以"|"表示。

举个例子，定义规则如下：

代码:

value(X) ==> X =< 9 | Y is X + 1, value(Y).

这意思是说，当有符合"==>"左边的约束时，X必须小于或等于9，
才套用此规则，否则放弃。

195 ?- value(1).
value(10)
value(9)
value(8 )
value(7)
value(6)
value(5)
value(4)
value(3)
value(2)
value(1)

这样就不会out of local stack了，因为我们在条件之上又设了前提条件Guard，
像守卫一样守在规则的门口。
Guard不是专属于繁殖规则的，也可以配合"化简"或"合并"规则使用。


前面在讲"约束出现顺序不重要"的时候，
讲到想写一个减法规则，但这个减法想要的是较大数减去较小数，
有了"守卫"很容易办到：

代码:

value(X), value(Y) <=> X > Y | Z is X - Y, value(Z).

这样无论你查询value(3), value(5)还是value(5), value(3)，结果都是value(2)。



最后举一个例子，用CHR规则来写一个prime(N, L)谓词，
此谓词将所有小于或等于N的质数放进List L中传回。

代码:

:- use_module(library(chr)).


:- chr_constraint prime/2, value/1, pp/1.


gen    @  prime(N, L) <=> N >= 2 | N1 is N - 1, value(N), prime(N1, L).
pp    @  prime(1, L) ==> pp([]).
del    @  value(I) \ value(J) <=> J mod I =:= 0 | true.
append @  pp(K), value(X) <=> K1 = [X | K], pp(K1).
return @  prime(N, L), pp(K) <=> L=K.

199 ?- prime(10, P).
P = [7, 5, 3, 2] .

这里列出了小于等于10的质数。


"@"左边可以给该规则取个名称，比如若某规则是定义"递移律"（若A<B且B<C，则A<C），
则可在前面加注"transitivity @"。

这里为了方便说明，我给每一条规则都起了一个名字。
gen规则是为了产生一连串value的，比如prime(N)会将自己变成prime(N-1)和value(N)两个约束。
pp规则是为了生出pp([])，一个用来摆放质数的List。prime不想消除所以用的是繁殖规则，
因为prime在后面return规则里还用得到。
del规则是核心了，它将gen产生的众多value，任意两个配成一对，
只要较大的数可以被较小的数整除，就把较大的数消除（可被整除就不是质数了）。
del规则一直重复被执行的结果，就是所有非质数都被删除了，剩下的value都是质数了。
所以append规则将每一对pp和value，把value的质都摆放进List中，并生成新的pp([新List])。
return规则负责将pp里面的List传回给使用者查询的参数L。



虽然"约束"与prolog一般称的"事实"感觉很像，
但本教学结束前还是要提示一些不同之处。


考虑前面提过的减法规则

代码:

subtract @  value(X), value(Y) <=> X > Y | Z is X - Y, value(Z).

30 ?- value(1), value(3), value(5).
value(3)

CHR先将value(1), value(3)配对，得到value(2)，
再将value(2), value(5)配对，最终得到value(3)。
然后呢？还有别的可能答案吗？没了，就算你输入"；"也没了。
这就是第1个差异。

回想一下在prolog里，如果你列了一堆value事实，并且定义减法规则来查询，
prolog会先告诉你value(3)，你如果输入"；"，prolog会再找寻其他可能答案，
发现value(1)可以先和value(5)配对，得到value(4)，
再用value(4)和value(3)配对，得到value(1)，
所以你按"；"它会再告诉你还有一个可能答案：value(1)，
但CHR里的约束并不具备这个效果。


第二个差异，考虑如下规则

代码:

value(X) <=> result(5), result(Y).

40 ?- value(1).
result(_G121715)
result(5)

虽然result(5)先被产生出来，但这是个约束而不是prolog事实，
后面的result(Y)你"不要期望"会得到Y = 5的匹配结果，
CHR是把result(Y)视为增加一个result约束。


如果加一个prolog事实进去

代码:

result(12).
value(X) <=> result(5), result(Y).

50 ?- value(1).
result(5)

这时候result(Y)会被视作prolog查询，匹配到result(12)，所以是true，
最终的查询结果只剩下CHR约束result(5)。
所以可以看出CHR的处理标准：有prolog事实时自动匹配prolog事实，没prolog事实时以新增加CHR约束处理。

cool