Constraint Handling Rules 从入门到精通（五） - 标准操作语义

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

语法描述了一个编程语言应该是什么样子，语义描述的是”是什么意思“。本文讲述CHR的标准操作语义（Standard Operational Semantics^[1]）。这套语义加入了防止重复应用规则的机制。

Numbered Constraints

给一个约束$c$加上一个值为$i$的ID，用$c\#i$来表示，称为“numbered constraint”。定义如下两个函数用来操作$c\#i$。

$chr(c\#i) = c \\ id(c\#i)=i$

状态

执行过程每一步的状态，包括以下几个内容。

Goal
类型：多重集^[2]符号：$G$内容：当前的Goal的内容。执行的过程中，Goal的内容是会变化的。

(Constraint) Store
类型：集合符号：$S$内容：Numbered constraints。

传播历史(Propagation History)
类型：集合符号：$T$内容：这是一个元组$(r,I)$的集合。

其中，

• $r$是规则的名称，为了方便，我们假定每一条规则都有独一无二的名称。

• $I$是匹配序列，是一个ID组成的序列。当匹配成功时，store中匹配到的元素的id，按照规则头部出现的顺序排列后形成的序列。

步骤ID
类型：正整数通常用符号：$i$内容：随着执行步骤的增加，这个值可能会增加。这个值和$T$的内容，用来防止重复应用规则。

为了表述方便,我们每一个状态都用$<G,S,T>_i$来表示。其中，下标$i$表示步骤ID。

程序执行前的初始状态为$<G,\emptyset,\emptyset>_1$，$G$为一开始要执行的 Goal，也就是 Query。

规则

我们只考虑下面一种形式。

$r @ H_{1} \backslash H_{2} \Leftrightarrow g | C$

这是一条 Simpagation Rule。其中，$r$是规则名称，$H_1$和$H_2$是头部，$g$是 Guard。$C$是body部分。（ Body 部分是 Goal，也就是一个多重集）。当 $H_1 = \emptyset$ 的时候，这条规则是 Simplification Rule；当$H_2 = \emptyset$ 的时候，这条规则是Propagation Rule。当 $g$ 省略的时候，我们认为$g = \text{true}$，相当于不再进行额外的检查。

关于匹配和$(r,I)$

所有的匹配，都是规则头部和store中的约束进行匹配。

匹配成功需要满足两个条件：

1. 对规则头部的约束中的变量进行替换后，可以和Store中对应的约束内容保持一致。

2. Guard 中的条件被满足。

匹配后，变量被初始化成替换的值。

下面举一个例子说明。

假设，规则$r1$头部$H_1 = \{ p(X),q(X),p(X) \},H_2 = \{ r(Y) \}$，$g$省略，Store 中的内容 $S = \{p(1)\#1,q(1)\#2,q(1)\#3,r(10)\#4,p(1)\#5\}$ 。若取$X=1,Y=10$，则规则头部可以成功匹配到Store中的内容。此时规则名称、规则序列组成的$(r,I)$可能为$\{ r1, (1,2,5,4)\}$或$\{r1, (1,3,5,4)\}$或$\{r1,(5,3,1,4)\}$或$\{r1,(5,2,1,4)\}$。每一次匹配只对应其中一种可能。匹配后，变量$X$和$Y$被初始化成1和10.

执行过程

执行过程分成3个基本操作。通过不断应用这3个基本操作，来变换当前的状态，直到无法再应用为止。这三个操作分别是 Solve、Introduce和Apply。

Solve

使用前提：$G$中存在一个可以被执行的builtin constraint。执行过程：执行该builtin constraint，并从$G$中移除。

Introduce

当前状态：$<G,S,T>_i$。使用前提：$G$中存在一个CHR Constraint $c$。执行过程：

1. 从$G$中移除$c$。

2. 往$S$中添加$c\#i$。

3. $i \leftarrow i+1$。

Apply

当前状态：$<G,S,T>_i$。使用前提：假设规则为$r @ H_{1} \backslash H_{2} \Leftrightarrow g | C$。规则$r$可以匹配上$S$中的约束，对应本次匹配的$(r,I) \notin T$执行过程:

1. 为了避免和已有的变量名重复，替换规则$r$中所有的变量名成为独一无二的变量名。

2. 规则$r$和$S$中的约束进行匹配，并初始化相应的变量。

3. 将对应本次匹配的$(r,I)$添加进$T$。

4. 从$S$中删除和$H_2$匹配上的元素。

5. 把$C$的内容添加到$G$中。

对于执行过程的第1步，要注意的是，变量名本身并不重要，变量名并不属于变量的一部分，只要能区分开即可。而同一个规则多次应用，由于每次都替换变量名，所以每次应用时的变量也都不同，不会造成混淆。例如，有规则p(X) <=> X1 is X - 1, p(X1)和查询p(9)，第一次应用规则后变成X1 is 9 - 1, p(X1)，接着再应用一次规则，若没有修改变量的名字，就会变成X1 is 9 - 1, X1 is X1 - 1, p(X1)，然而这其中不同的X1代表着不同的值，直接就混淆了。变量重命名是很重要的一个步骤。

以上每一个基本操作的使用并没有顺序的要求，因而可以以任意次序应用这些操作，而程序执行的结果也可能因此而不同 。

执行示例1

已知CHR规则如下。

gcd1 @ gcd(0) <=> true.
gcd2 @ gcd(I) \ gcd(J) <=> I =< J | K is J - I, gcd(K).

这是一段求最大公约数的程序。执行 gcd(6), gcd(9). ，结果如下。

?- gcd(6), gcd(9).
gcd(3).

下面从初始状态$<\{\operatorname{gcd}(6), \operatorname{gcd}(9)\}, \emptyset, \emptyset>_{1}$开始，展示在标准操作语义下的执行过程。

$\begin{array}{ll} & <\{\gcd(6), \mathrm{gcd}(9)\}, \emptyset, \emptyset>_1 \\ \longmapsto_{introduce} & <\{\mathrm{gcd}(9)\},\{\mathrm{gcd}(6) \# 1\}, \emptyset>_{2} \\ \longmapsto_{i n t r o d u c e} & <\emptyset,\{\mathrm{gcd}(6) \# 1, \operatorname{gcd}(9) \# 2\}, \emptyset>_3 \\ \longmapsto_{apply \text{ gcd2}} & <\left\{K_{1 }\text{ is } 9-6, \mathrm{gcd}\left(K_{1}\right)\right\},\{\mathrm{gcd}(6) \# 1\},\{(\mathrm{gcd} 2,(1,2))\}>_{3} \\ \longmapsto_{solve} & <\{\mathrm{gcd}(3)\},\{\mathrm{gcd}(6) \# 1\},\{(\mathrm{gcd} 2,(1,2))\}>_{3} \\ \longmapsto_{introduce} & <\emptyset,\{\mathrm{gcd}(6) \# 1, \operatorname{gcd}(3) \# 3\},\{(\mathrm{gcd} 2,(1,2))\}>_{4} \\ \longmapsto_{apply \text{ gcd2}} & <\left\{K_{2} \text{ is } 6-3, \operatorname{gcd}\left(K_{2}\right)\right\},\{\mathrm{gcd}(3) \# 3\},\{(\mathrm{gcd} 2,(1,2)),(\mathrm{gcd} 2,(3,1))\}>_{4} \\ \longmapsto_{solve} & <\{\mathrm{gcd}(3)\},\{\mathrm{gcd}(3) \# 3\},\{(\mathrm{gcd} 2,(1,2)),(\mathrm{gcd} 2,(3,1)\}>_4 \\ \longmapsto_{introduce} & <\emptyset,\{\mathrm{gcd}(3) \# 3, \operatorname{gcd}(3) \# 4\},\{(\mathrm{gcd} 2,(1,2)),(\mathrm{gcd} 2,(3,1))\}>_5 \\ \longmapsto_{apply \text{ gcd2}} & <\left\{K_{3} \text{ is } 3-3, \mathrm{gcd}\left(K_{3}\right)\right\},\{\mathrm{gcd}(3) \# 3\},\{(\mathrm{gcd} 2,(1,2)),(\mathrm{gcd} 2,(3,1)),(\mathrm{gcd} 2,(3,4))\}>_{5} \\ \longmapsto_{solve} & <\{\mathrm{gcd}(0)\},\{\mathrm{gcd}(3) \# 3\},\{(\mathrm{gcd} 2,(1,2)),(\mathrm{gcd} 2,(3,1)),(\mathrm{gcd} 2,(3,4))\}>_{5} \\ \longmapsto_{introduce} & <\emptyset,\{\mathrm{gcd}(3) \# 3, \mathrm{gcd}(0) \# 5\},\{(\mathrm{gcd} 2,(1,2)),(\mathrm{gcd} 2,(3,1)),(\mathrm{gcd} 2,(3,4)\}\}>_{6} \\ \longmapsto_{apply \text{ gcd1}} & <\{\mathrm{true}\},\{\mathrm{gcd}(3) \# 3\},\{(\mathrm{gcd} 2,(1,2)),(\mathrm{gcd} 2,(3,1)),(\mathrm{gcd} 2,(3,4)),(\mathrm{gcd} 1,(5))\}>_{6} \\ \longmapsto_{solve} & <\emptyset,\{\mathrm{gcd}(3) \# 3\},\{(\mathrm{gcd} 2,(1,2)),(\mathrm{gcd} 2,(3,1)),(\mathrm{gcd} 2,(3,4)),(\mathrm{gcd} 1,(5))\}>_{6} \end{array}$

最终状态的Store $S = \{\mathrm{gcd}(3) \# 3\}$即为最终结果。

实际上对于这个程序，若在最后不停重复应用 gcd2，那么程序是不会终止的。这种情况下，传播历史$T$并无法限制住这种重复应用（在两次应用中间 ，执行introduce操作，可导致这种重复应用不会停止）。

完整程序可以在这里下载。

执行示例2

已知CHR规则如下。

r1 @ mother(X, Y) ==> parent(X, Y).
r2 @ father(X, Y) ==> parent(X, Y).
r3 @ parent(X, Z), parent(Y, Z) ==> sibling(X, Y).

对以上规则执行查询mother(hans, mira), mother(sepp, mira), father(sepp, john).，结果如下。

?- mother(hans, mira), mother(sepp, mira), father(sepp, john).
mother(sepp, mira),
mother(hans, mira),
father(sepp, john),
parent(sepp, john),
parent(sepp, mira),
parent(hans, mira),
sibling(hans, sepp),
sibling(sepp, hans).

下面展示在标准操作语义下的执行过程^[3]。

操作	$G$	$S$	$T$	$i$
初始状态	mother(hans, mira) mother(sepp, mira) father(sepp, john)	$\emptyset$	$\emptyset$	1
introduce	mother(sepp, mira) father(sepp, john)	mother(hans, mira)#l	$\emptyset$	2
apply $r1$	parent(hans, mira) mother(sepp, mira) father(sepp, john)	mother(hans, mira)#l	$(r1, (1))$	2
introduce	mother(sepp, mira) father(sepp, john)	parent(hans, mira)#2 mother(hans, mira)#l	$(r1, (1))$	3
introduce	father(sepp, john)	mother(sepp, mira)#3 parent(hans, mira)#2 mother(hans, mira)#l	$(r1, (1))$	4
apply $r1$	parent(sepp, mira) father(sepp, john)	mother(sepp, mira)#3 parent(hans, mira)#2 mother(hans, mira)#l	$(r1, (1))$ $(r1, (3))$	4
introduce	father(sepp, john)	parent (sepp, mira)#4 mother(sepp, mira)#3 parent(hans, mira)#2 mother(hans, mira)#l	$(r1, (1))$ $(r1, (3))$	5
apply $r3$	sibling(sepp, hans) father(sepp, john)	parent (sepp, mira)#4 mother(sepp, mira)#3 parent(hans, mira)#2 mother(hans, mira)#l	$(r1, (1))$ $(r1, (3))$ $(r3, (4,2))$	5
apply $r3$	sibling(hans, sepp) sibling(sepp, hans) father(sepp, john)	parent (sepp, mira)#4 mother(sepp, mira)#3 parent(hans, mira)#2 mother(hans, mira)#l	$(r1, (1))$ $(r1, (3))$ $(r3, (4,2))$ $(r3, (2,4))$[4]	5
introduce	sibling(sepp, hans) father(sepp, john)	sibling(hans, sepp)#5 parent (sepp, mira)#4 mother(sepp, mira)#3 parent(hans, mira)#2 mother(hans, mira)#l	$(r1, (1))$ $(r1, (3))$ $(r3, (4,2))$ $(r3, (2,4))$	6
introduce	father(sepp, john)	sibling(sepp, hans)#6 sibling(hans, sepp)#5 parent (sepp, mira)#4 mother(sepp, mira)#3 parent(hans, mira)#2 mother(hans, mira)#l	$(r1, (1))$ $(r1, (3))$ $(r3, (4,2))$ $(r3, (2,4))$	7
introduce	$\emptyset$	father(sepp, john)#7 sibling(sepp, hans)#6 sibling(hans, sepp)#5 parent (sepp, mira)#4 mother(sepp, mira)#3 parent(hans, mira)#2 mother(hans, mira)#l	$(r1, (1))$ $(r1, (3))$ $(r3, (4,2))$ $(r3, (2,4))$	8
apply $r2$	parent(sepp, john)	father(sepp, john)#7 sibling(sepp, hans)#6 sibling(hans, sepp)#5 parent (sepp, mira)#4 mother(sepp, mira)#3 parent(hans, mira)#2 mother(hans, mira)#l	$(r1, (1))$ $(r1, (3))$ $(r3, (4,2))$ $(r3, (2,4))$ $(r2, (7))$	8
introduce	$\emptyset$	parent(sepp, john)#8 father(sepp, john)#7 sibling(sepp, hans)#6 sibling(hans, sepp)#5 parent (sepp, mira)#4 mother(sepp, mira)#3 parent(hans, mira)#2 mother(hans, mira)#l	$(r1, (1))$ $(r1, (3))$ $(r3, (4,2))$ $(r3, (2,4))$ $(r2, (7))$	9

$S$中的内容即为执行结果。

完整程序可以在这里下载。

---

1. 也叫”Theoretical Operatonal Semantics“、”High-level Operational Semantics“。 ↩︎

2. 和集合不同，多重集的内容可以重复。 ↩︎

3. 内容繁多，为了理解起来更容易，使用表格来呈现执行过程。 ↩︎

4. 传播历史$T$里面的元素$(r,I)$中的$I$是个序列，所以$(2,4)$和$(4,2)$是不同的。所以，$r3$可以从不同的方向应用两次。在不同方向应用了两次以后，传播历史$T$的内容限制了再次重复匹配。 ↩︎