本文根据笔者2017年的一次讲座整理。

在 Prolog 语法的基础上，CHR实现了自己的一套语法。CHR本身的语法也很简单，Gregory J. Duck. 实现过一个叫 ToyCHR^[1] 的 reference implementation，只有500行代码。

Constraints

约束（Constraints）的概念，已经在之前提到过了。这里更加详细的讲讲。

在 CHR 中，Constraints 分成两种。一种是专用于CHR的，叫 CHR Constraint，另一种是 builtin constraint 。这两种约束，形式上是统一的。下面分别讲讲这两种约束。

在之前文章的例子中，所有的约束，都是CHR Constraints^[2]。每个CHR Constraints都是一个 Compound Term 或者 Atom。如果使用的是K.U.Leuven CHR system，每个CHR Constraints在使用前必须通过chr_constraint/1进行声明。这些 CHR Constraints 会被编译成普通的谓词，然后被 Prolog 使用。

除了 CHR Constraints 以外的，都可以认为是builtin constraints。每一个builtin constraint，可以视为一个黑盒，相当于调用宿主语言上的内容。例如，之前文章中的true就是一个builtin constraint。true是个Prolog的谓词，在之前的文章中，这个谓词什么都不干，也不会被匹配到，使用它仅仅只是为了语法上的完整。

builtin constraints 没有什么特别的处理方式，遇到了直接执行就好了。

语法

每一个CHR Program由一堆的 Rules（规则）所组成。整个CHR的语法总体上如下。

Rule --> [Name ’@’] (SimplificationRule | PropagationRule | SimpagationRule) ’.’
 
SimplificationRule --> Head ’<=>’ [Guard ’|’] Body 
PropagationRule --> Head ’==>’ [Guard ’|’] Body 
SimpagationRule --> Head ’\’ Head ’<=>’ [Guard ’|’] Body 

Head --> CHRConstraints 
Guard --> BuiltInConstraints 
Body --> Goal 

CHRConstraints --> CHRConstraint | CHRConstraint ’,’ CHRConstraints 
BuiltInConstraints --> BuiltIn | BuiltIn ’,’ BuiltInConstraints 
Goal --> CHRConstraint | BuiltIn | Goal ’,’ Goal 

Query --> Goal

这里的 Goal 是指一段要执行的代码，例如，之前文章的 min(3), min(1), min(4), min(2), min(1), min(2). 。 Query 则是指在 Prolog Toplevel 中输入的 Goal 。

Prolog 程序的主要执行方式，是在一个交互式的环境（Prolog Toplevel）中输入一段 Prolog 代码，然后执行。一段要执行的代码，称为 Goal 。在 Prolog Toplevel 中输入的 Goal ，也被称为 Query。

三种规则

CHR总共有3种类型的规则：Simplification Rule，Propagation Rule，Simpagation Rule。

Simplification Rule大概可以翻译为“化简规则”，Propagation Rule大概可以翻译为“传播规则”^[3]。至于simpagation这个词，应该是simplification和propagation合成的，功能上也等于这两种规则的综合。

Simpagation Rule

一个 Simpagation Rule 的语法如下。

1	[Name ’@’] Head1 ’\’ Head2 ’<=>’ [Guard ’\|’] Body ’.’

其中，

Head1和Head2部分由一串CHR Constraint组成。Head1 ’\’ Head2为规则的头部。
Guard由一串builtin constraints组成。Guard不是必须的。
Body是一个Goal，一个Goal可以由一串constraint组成，可以是CHR Constraint，也可以是builtin constraint。
Name是规则的名字，并非必须，作用相当于文档，主要是给人看的，并没有实质的作用。

限制

Guard 部分可以使用的builtin constraints是有限制的。下面是可以使用的builtin constraints。

最基本的约束。
- true/0 - 永远为真。
- false/0- 永匹为假。
检查一个变量的状态。
var/1 - 如果是个free的变量，则为真。
nonvar/1 - 如果是个free的变量，则为假。
检查是否可以unify。
- =/2 ,==/2 - 如果可以unify，则为真。
- \==/2 - 如果无法unify，则为真。
一些算数运算符。如</2 ， =</2 ，等等。

这些builtin constraints大部分和Prolog是一致的，除了两个例外：=/2会被替换成==/2，is/2会被替换成=:=/2。

作为 Guard ，应该只起一个检测的作用。而=/2和is/2除了检测，还能改变变量的值，这是不允许的。

语义

若Head1和Head2里面的内容全都匹配到（无论以什么顺序）当前的Goal里的内容，并且Guard的条件为真，则从Goal里面删掉匹配到Head2的那些constraints，并将Body里面的constraints添加到Goal里。

匹配和 Unification

头部中的 constraints 和 Goal 中的 constraints 能匹配上，遵循的一个规则：把头部中的 constraints 里的变量进行替换后，可以变得和 Goal 里对应的 constraints 一模一样。这和 prolog 谓词头部的匹配规则是不一样的。在 prolog 中，能不能匹配上取决于是否可以 unify。例如，谓词头部是p([Y])，Goal中是p(X)，这样子是可以匹配上的，因为 p([Y]) = p(X) 必然成功。而在CHR中，由于头部的p([Y])无论如何替换变量Y，都无法变成Goal中的p(X)，因而是无法匹配上的；但是，反过来只要让X=[Y]就可以匹配上了。一旦在CHR匹配成功，头部的变量也会被unify成具体的值。

Simplification Rule 和 Propagation Rule

这两种规则，都可以视为 Simpagation Rule 的特殊情况。若 Simpagation Rule 中的 Head1 内容为空，也就是所有匹配到的内容都要删除，那么就是 Simplification Rule。

语法

1	[Name ’@’] Head ’<=>’ [Guard ’\|’] Body ’.’

语义

若Head里面的内容全都匹配到（无论以什么顺序）当前的Goal里的内容，并且Guard的条件为真，则从Goal里面删掉匹配到Head的那些constraints，并将Body里面的constraints添加到Goal里。

若 Simpagation Rule中的 Head2 内容为空，也就是所有匹配到的内容都要保留，那么就是 Propagation Rule。

语法

1	[Name ’@’] Head ’==>’ [Guard ’\|’] Body ’.’

语义
若Head里面的内容全都匹配到（无论以什么顺序）当前的Goal里的内容，并且Guard的条件为真，则将Body里面的constraints添加到Goal里。

显然，只有 Propagation Rule 的 CHR 程序是无法停止的。

一个例子：寻找素数

下面这个例子。

% 这个程序用筛法来列出小于等于某个数字的所有素数。

% 由于是prolog的DSL，所以首先要引入对应的模块以启用CHR。
:- use_module(library(chr)).

% 每一个CHR Constraint都要先声明。
:- chr_constraint prime/1.

% 两条规则，随便什么顺序应用都可以。
r1 @ prime(N) ==> N > 2 | N1 is N - 1, prime(N1).
r2 @ prime(I) \ prime(J) <=> J mod I =:= 0 | true.

现在我们来执行prime(5)这个Goal。一种可能的执行过程如下（用下划线表示匹配到的约束）。

\begin{array}{ll} & \text { \underline{prime(5)} } \\ \longmapsto_{apply \text { r1}} & \text { N1 is } 5-1, \text { prime(N1), prime(5) } \\ \longmapsto & \underline{\text { prime }(4)}, \text { prime(5) } \\ \longmapsto_{apply \text { r1}} & \text { N1 is 4 - 1, prime(N1), prime(4), prime(5) } \\ \longmapsto & \text { \underline{prime(3)}, prime(4), prime(5) } \\ \longmapsto_{apply \text { r1}} & \text { N1 is 3 - 1, prime(N1), prime(3), prime(4), prime(5) } \\ \longmapsto & \text { \underline{prime(2)}, prime(3), \underline{prime(4)}, prime(5) } \\ \longmapsto_{apply \text { r2}} & \text { true, prime(2), prime(3), prime(5) } \\ \longmapsto & \text { prime(2), prime(3), prime(5) } \end{array}

用 Prolog 执行，结果如下。

?- prime(5).
prime(2),
prime(3),
prime(5).

由于执行顺序不唯一，这个程序可以有很多种不同的执行结果。由于存在规则r1，该程序有在某些执行顺序中，是不会停止的。

这个项目已经被作者删除。历史页面可以在这里找到。 ↩︎
唯一的例外是true。 ↩︎
“传播”是 Constraint Programming 的术语。尽管 CHR 基于 rewriting，但却不是一个 TRS（Term Rewriting System）。很多时候，我们还是将 CHR 的 Paradigm 归为 Constraint Logic Programming 。 ↩︎

Constraint Handling Rules 从入门到精通（四） - 语法和语义：通俗的表达