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

聪明的你一定发现，为什么执行顺序不确定的CHR程序，放到 K.U.Leuven CHR System 中，就一定会得到预期的执行结果呢？实际上，绝大多数CHR实现，包括 K.U.Leuven CHR Syste 在内，都使用另外一种语义 Refined Operational Semantics，记为 ωr\omega_r。这种语义，可以视为标准操作语义的子集，相比之下，ωr\omega_r 规定了具体的执行顺序。本文讲述这种语义。

大多数CHR程序只有在ωr\omega_r语义下才能正确执行。

基本概念

和 Standard Operational Semantics 一样，ωr\omega_r的规则模型仍旧是

r@H1\H2⇔g∣Cr @ H_{1} \backslash H_{2} \Leftrightarrow g | C

这里讲解几个基本概念。

顺序和Occurence

在ωr\omega_r的框架中，一个CHR程序是规则的序列，按照从上到下的书写顺序。而 Goal、规则的头部和 Body 都不再是约束的集合，而都是按照书写顺序从左到右的序列。规则的头部的每一个约束，都将绑定一个数字，这个数字称为Occurence。Occurence从1开始算起，按照从左到右从上到下的顺序逐步递增。唯一的例外是 Simpagation Rule。在 Simpagation Rule 中，要删除掉的约束的Occurence排在要保留的约束的前边。

下面这段例子程序，用大括号标出了Occurence。

1
2
3
4
5
6
S(V) {1} <=> d([V], 0), r([]).
d([V|_], D1) {3} \ d([V|_], D2) {2} <=> D1 < D2 | true.
d([V|T], D) {4}, e(V, C, W) {5} ==> DW is D + W, d([C, V|T], DW).
t(Vl, _) {7} \ d([V2|_], _) {6} <=> V1 \== V2 | true. 
t(V, _) {10} \ d([V|T], D) {8}, r(RT) {9} <=> r([(D -[V|T])|RT]).
t(_, R) {11}, r(L) {12} <=> R = L.

Active CHR Constraint

一个 Active 的约束c#i:jc\#i:j，它只和程序中Occurence为jj的那个约束进行匹配（但并不要求一定能成功匹配）。注意这个 Active 的约束是在 Goal 中的，执行过程中 Goal 的每个约束都会尝试和所有规则头部中约束进行匹配。

回到前边我们所说的chrchr和idid两个函数，现在需要重新定义这两个函数。

chr(c#i:j)=cid(c#i)=i\begin{array}{rcl} chr(c\#i:j) & = & c\\ id(c\#i) &= &i \end{array}

状态

把 Standard Operation Semantics 每一步的状态<G,S,T>i<G,S,T>_i中的 Goal GG换成 Stack AA，得到 ωr\omega_r 中每一步的状态 <A,S,T>n<A,S,T>_n。其中，下标nn表示步骤ID。

之所以采用堆栈的概念，是因为CHR编译到的目标语言都是基于堆栈的。这样可以使得和目标语言在概念上更加接近，编译起来更容易。

Stack
类型：序列符号：AA内容：当前的执行堆栈（execution stack）。初始内容仍旧是 Query 。和 Standard Operational Semancs 不同的是，一个 Goal 中的 constraint，可以同时存在于 Stack AA 和 Store SS 中，但 Apply 时的匹配仍旧只在 Store 进行。另外，builtin constraints也会在 Stack 中。

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

Wake Up

如果一个 builtin constraint 执行之后，会改变一个在 Store 中的 CHR Constraint，那么我们称这个 Store 中的 CHR Constraint 被这个 builtin constraint 给 wake up。

例如，执行 w(X), w(2), w(X+1), X=3, X=3, w(l).的过程中，执行到第一个 X=3 的时候（假设此时前边的 constraints 都己经在 Store 中），Store 中的w(x)和w(X+1)中的X会被替换成3，同时，这两个constraints 会被 wake up。但是，执行第二个 X=3 的时候，就己经不会再被wake up了，因为此时 Store 中的w(X)和w(X+1)已经成了 w(3)和w(3+1)，不再受X=3的影响。每次执行完 builtin constraint 之后，都会 wake up 一次，一次可以wake up多条constraints。

在实际实现中，w(X)和 w(X+1)会被wake up，还需要另二个条件，那就是必须会对接下来的执行过程有影响。例如，你的程序中有规则的头部用到了 w/1 这个约束，那么w(X)和 w(X+1)会被wake up；如果你的程序一条用到w/1的规则都没有，那么根本就不会被 wake up。

执行过程

执行过程分成几个基本操作。通过不断应用这几个基本操作，变换当前状态，直到无法再应用为止。几个基本操作如下。

Solve+Wake

使用前提：stack AA的头部是一个builtin constraint。执行过程：

  1. 执行该builtin constraint，Store SS中可能会有些constraints被wake up。

  2. 从AA中删除该builtin constraint。

  3. 将此次执行所wake up的那些constraints添加到AA的头部。

步骤3添加到AA头部（实际上是重新添加回AA）的那些constraints是可以按照任意顺序添加的，这造成了一定的不确定性，也会对实际运行的结果有所影响。由于这是由实现来决定的，所以大部分实现仅仅只是把（实现认为）会影响执行的那些constraints给wake up。这是写程序的时候应该考虑到的一个点[1]。

Activate

使用前提：Stack AA的头部是一个CHR constraint cc。当前状态：<A,S,T>n<A,S,T>_n。执行过程：

  1. 把cc替换成c#n:1c\#n: 1。

  2. 把c#nc\#n添加进SS。

  3. n←n+1n \leftarrow n+1。

Reactive

使用前提：Stack AA的头部是一个被wake up的CHR Constraint c#ic\#i。当前状态：<A,S,T>n<A,S,T>_n。执行过程:

  1. 把 c#ic\#i替换成c#i:1c\#i:1。

Default

使用前提：

  1. Stack AA的头部是一个 active 的CHR Constraint c#i:jc\#i:j。

  2. 当前没有其他操作可以应用了。

执行过程：

  1. 把c#i:jc\#i:j替换成c#i:(j+1)c\#i:(j+1)。

Drop

使用前提：Stack AA的头部是一个 active 的 CHR Constraint c#i:jc\#i : j，且程序中不存在jj这个occurence （已经超过程序中出现的最大值）。

执行过程：

  1. 把c#i:jc\#i:j从Stack AA中移除。

Apply

使用前提：

  1. Stack AA的头部是一个active的CHR Constraint c#i:jc\#i:j。

  2. Occurence为jj的约束，在规则r@H1\H2⇔g∣Cr @ H_{1} \backslash H_{2} \Leftrightarrow g | C的头部，可能在H1H_1中，也可能在H2H_2。

  3. Occurence为jj的约束，和cc能够匹配上（c#i:jc\#i:j只和规则头部Occurence为jj的约束进行匹配）。

  4. Store SS中的约束，可以被规则rr所匹配。

匹配的时候，能成功匹配的方案，有时候是可以有多种的可能的（特别是当一个约束可以同时匹配到H1H_1和H2H_2中的约束的时候），这造成了另一种不确定性。例如，规则x(_) \ x(_), x(_) <=> true.和 Goal x(3), x(4), x(5).，执行的结果，由具体实现来决定。

执行过程：

  1. 为了避免和己有的变量名重复，替换规则rr中所有的变量名。具体方式和Standard Operational Semantics一样。

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

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

  4. 从SS中删除和H2H_2匹配上的元素。

  5. Occurence为jj的约束，出现在H2H_2中，那么从Stack AA中删除c#i:jc\#i:j。

  6. 把C的内容放在A前边：A←C+ ⁣+AA \leftarrow C \mathbin{+\mkern{-5mu}+} A

执行示例1

已知CHR规则如下。

1
r1 @ w(3) <=> q.

用 Leuven CHR System 执行查询w(X), w(2), w(X+1), X=3, X=3, w(1).，结果如下[2]。

1
2
3
4
5
6
?- w(X), w(2), w(X+1), X=3, X=3, w(1).
X = 3,
w(1),
w(3+1),
w(2),
q.

下面我们用 ωr\omega_r 来展示该查询的执行过程。

在执行前，首先给程序标上 Occurence，如下所示（大括号内表示 Occurence ）。

1
r1 @ w(3) {1} <=> q.

初始状态<(w(X),w(2),w(X+1),X=3,X=3,w(1)),∅,∅>1<(w(X), w(2), w(X+1), X=3, X=3, w(1)), \emptyset, \emptyset>_1。执行过程如下所示。

<(w(X),w(2),w(X+1),X=3,X=3,w(1)),∅,∅>1⟼Activate<(w(X)#1:1‾,w(2),w(X+1),X=3,X=3,w(1)),{w(X)#1},∅>2⟼Default<(w(X)#1:2‾,w(2),w(X+1),X=3,X=3,w(1)),{w(X)#1‾},∅>2⟼Drop<(w(2),w(X+1),X=3,X=3,w(1)),{w(X)#1},∅>2⟼Activate<(w(2)#2:1‾,w(X+1),X=3,X=3,w(1)),{w(X)#1,w(2)#2‾},∅>3⟼Default<(w(2)#2:2‾,w(X+1),X=3,X=3,w(1)),{w(X)#1,w(2)#2},∅>3⟼Drop<(w(X+1),X=3,X=3,w(1)),{w(X)#1,w(2)#2},∅>3⟼Activate<(w(X+1)#3:1‾,X=3,X=3,w(1)),{w(X)#1,w(2)#2,w(X+1)#3‾},∅>4⟼Default<(w(X+1)#3:2‾,X=3,X=3,w(1)),{w(X)#1,w(2)#2,w(X+1)#3},∅>4⟼Drop<(X=3,X=3,w(1)),{w(X)#1,w(X+1)#3⏟wake up,w(2)#2},∅>4⟼Solve+Wake<(w(3)#1‾,w(3+1)#3‾⏞添加到A的头部,3=3‾⏟执行了X=3，所有X初始化成3,w(1)),{w(3)#1‾,w(3+1)#3‾⏟执行了X=3，所有X初始化成3,w(2)#2},∅>4⟼Reactivate<(w(3)#1:1‾,w(3+1)#3,3=3,w(1)),{w(3)#1,w(3+1)#3,w(2)#2},∅>4⟼Apply r1<(q‾,w(3+1)#3,3=3,w(1)),{w(3+1)#3,w(2)#2},{(r1,(1)}>4⟼Activate<(q#4:1‾,w(3+1)#3,3=3,w(1)),{w(3+1)#3,w(2)#2,q#4‾},{(r1,(1)}>5⟼Default<(q#4:2‾,w(3+1)#3,3=3,w(1)),{w(3+1)#3,w(2)#2,q#4},{(r1,(1)}>5⟼Drop<(w(3+1)#3,3=3,w(1)),{w(3+1)#3,w(2)#2,q#4},{(r1,(1)}>5⟼Reactivate<(w(3+1)#3:1‾,3=3,w(1)),{w(3+1)#3,w(2)#2,q#4},{(r1,(1)}>5⟼Default<(w(3+1)#3:2‾,3=3,w(1)),{w(3+1)#3,w(2)#2,q#4},{(r1,(1)}>5⟼Drop<(3=3,w(1)),{w(3+1)#3,w(2)#2,q#4},{(r1,(1)}>5⟼Solve+Wake<(w(1)),{w(3+1)#3,w(2)#2,q#4},{(r1,(1)}>5⟼Activate<(w(1)#5:1‾),{w(3+1)#3,w(2)#2,q#4,w(1)#5‾},{(r1,(1)}>6⟼Default<(w(1)#5:2‾),{w(3+1)#3,w(2)#2,q#4,w(1)#5},{(r1,(1)}>6⟼Drop<(),{w(3+1)#3,w(2)#2,q#4,w(1)#5},{(r1,(1)}>6\begin{array}{ll} &<(w(X), w(2), w(X+1), X=3, X=3, w(1)), \emptyset, \emptyset>_1 \\ \longmapsto_{Activate} &<(\underline{w(X) \# 1: 1}, w(2), w(X+1), X=3, X=3, w(1)),\{w(X) \# 1\}, \emptyset>_{2} \\ \longmapsto_{Default} &<(\underline{w(X) \# 1: 2}, w(2), w(X+1), X=3, X=3, w(1)),\{\overline{w(X) \# 1}\}, \emptyset>_{2} \\ \longmapsto_{Drop} &<(w(2), w(X+1), X=3, X=3, w(1)),\{w(X) \# 1\}, \emptyset>_{2} \\ \longmapsto_{Activate} &<(\underline{w(2) \# 2: 1}, w(X+1), X=3, X=3, w(1)),\{w(X) \# 1, \underline{w(2) \# 2}\}, \emptyset>_{3} \\ \longmapsto_{Default} &<(\underline{w(2) \# 2: 2}, w(X+1), X=3, X=3, w(1)),\{w(X) \# 1, w(2) \# 2\}, \emptyset>_{3} \\ \longmapsto_{Drop} &<(w(X+1), X=3, X=3, w(1)),\{w(X) \# 1, w(2) \# 2\}, \emptyset>_3 \\ \longmapsto_{Activate} &<(\underline{w(X+1)\#3:1}, X=3, X=3, w(1)),\{w(X)\#1, w(2)\#2, \underline{w(X+1)\#3}\}, \emptyset>_{4} \\ \longmapsto_{Default} &<(\underline{w(X+1)\#3:2}, X=3, X=3, w(1)),\{w(X)\#1, w(2)\#2, w(X+1)\#3\}, \emptyset>_{4} \\ \longmapsto_{Drop} &<(X=3, X=3, w(1)),\{\underbrace{w(X)\#1, w(X+1)\#3}_{\text{wake up}}, w(2)\#2\}, \emptyset>_{4} \\ \longmapsto_{Solve+Wake} &<(\underbrace{\overbrace{\underline{w(3)\#1}, \underline{w(3+1)\#3}}^{添加到A的头部}, \underline{3=3}}_{执行了X=3，所有X初始化成3}, w(1)),\{\underbrace{\underline{w(3)\#1}, \underline{w(3+1)\#3}}_{执行了X=3，所有X初始化成3}, w(2)\#2\}, \emptyset>_{4} \\ \\ \longmapsto_{Reactivate} &<(\underline{w(3)\#1:1}, w(3+1)\#3, 3=3, w(1)),\{w(3)\#1, w(3+1)\#3, w(2)\#2\}, \emptyset>_{4} \\ \longmapsto_{Apply \text{ r1}} &<(\underline{q}, w(3+1)\#3, 3=3, w(1)),\{ w(3+1)\#3, w(2)\#2\}, \{(\text{r1},(1)\}>_{4} \\ \longmapsto_{Activate} &<(\underline{q\#4:1}, w(3+1)\#3, 3=3, w(1)),\{ w(3+1)\#3, w(2)\#2,\underline{q\#4}\}, \{(\text{r1},(1)\}>_{5} \\ \longmapsto_{Default} &<(\underline{q\#4:2}, w(3+1)\#3, 3=3, w(1)),\{ w(3+1)\#3, w(2)\#2,q\#4\}, \{(\text{r1},(1)\}>_{5} \\ \longmapsto_{Drop} &<( w(3+1)\#3, 3=3, w(1)),\{ w(3+1)\#3, w(2)\#2,q\#4\}, \{(\text{r1},(1)\}>_{5} \\ \longmapsto_{Reactivate} &<( \underline{w(3+1)\#3:1}, 3=3, w(1)),\{ w(3+1)\#3, w(2)\#2,q\#4\}, \{(\text{r1},(1)\}>_{5} \\ \longmapsto_{Default} &<( \underline{w(3+1)\#3:2}, 3=3, w(1)),\{ w(3+1)\#3, w(2)\#2,q\#4\}, \{(\text{r1},(1)\}>_{5} \\ \longmapsto_{Drop} &<( 3=3, w(1)),\{ w(3+1)\#3, w(2)\#2,q\#4\}, \{(\text{r1},(1)\}>_{5} \\ \longmapsto_{Solve+Wake} &<( w(1)),\{ w(3+1)\#3, w(2)\#2,q\#4\}, \{(\text{r1},(1)\}>_{5} \\ \longmapsto_{Activate} &<( \underline{w(1)\#5:1}),\{ w(3+1)\#3, w(2)\#2,q\#4,\underline{w(1)\#5}\}, \{(\text{r1},(1)\}>_{6} \\ \longmapsto_{Default} &<( \underline{w(1)\#5:2}),\{ w(3+1)\#3, w(2)\#2,q\#4,w(1)\#5\}, \{(\text{r1},(1)\}>_{6} \\ \longmapsto_{Drop} &<(),\{ w(3+1)\#3, w(2)\#2,q\#4,w(1)\#5\}, \{(\text{r1},(1)\}>_{6} \\ \end{array}

此时S={w(3+1)#3,w(2)#2,q#4,w(1)#5}S = \{ w(3+1)\#3, w(2)\#2,q\#4,w(1)\#5\}即为最终执行结果。

执行示例2

已知CHR规则如下。

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

用 Leuven CHR System 执行查询gcd(6), gcd(9)，结果如下。

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

先给程序标上 Occurence，如下所示。

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

初始状态<(gcd(6),gcd(9)),∅,∅>1<(\mathrm{gcd}(6), \mathrm{gcd}(9)), \emptyset, \emptyset>_{1}。执行过程如下所示。

<(gcd(6),gcd(9)),∅,∅>1⟼Activate<(gcd(6)#1:1‾,gcd⁡(9)),{gcd(6)#1‾},∅>2⟼Default<(gcd⁡(6)#1:2‾,gcd⁡(9)),{gcd⁡(6)#1},∅>2⟼Default<(gcd⁡(6)#1:3‾,gcd⁡(9)),{gcd⁡(6)#1},∅>2⟼Default<(gcd⁡(6)#1:4‾,gcd⁡(9)),{gcd⁡(6)#1},∅>2⟼Drop<(gcd⁡(9)),{gcd⁡(6)#1},∅>2⟼Activate<(gcd⁡(9)#2:1‾),{gcd⁡(6)#1,gcd⁡(9)#2‾},∅>3⟼Default<(gcd⁡(9)#2:2‾),{gcd⁡(6)#1,gcd⁡(9)#2},∅>3⟼apply gcd2<(K1 is 9−6,gcd⁡(K1)‾),{gcd⁡(6)#1},{(gcd2,(1,2))‾}>3⟼Solve+Wake<(gcd⁡(3)‾),{gcd⁡(6)#1},{(gcd2,(1,2))}>3⟼Activate<(gcd⁡(3)#3:1‾),{gcd⁡(6)#1,gcd⁡(3)#3‾},{(gcd2,(1,2))}>4⟼Default<(gcd⁡(3)#3:2‾),{gcd⁡(6)#1,gcd⁡(3)#3},{(gcd2,(1,2))}>4⟼Default<(gcd⁡(3)#3:3‾),{gcd⁡(6)#1,gcd⁡(3)#3},{(gcd2,(1,2))}>4⟼apply gcd2<(K2 is 6−3,gcd⁡(K2)‾,gcd⁡(3)#3:3⏟保留active状态),{gcd⁡(3)#3},{(gcd2,(1,2)),(gcd2,(3,1))‾}>4⟼Solve+Wake<(gcd⁡(3)‾,gcd⁡(3)#3:3),{gcd⁡(3)#3},{(gcd2,(1,2)),(gcd2,(3,1))}>4⟼Activate<(gcd⁡(3)#4:1‾,gcd⁡(3)#3:3),{gcd⁡(3)#3,gcd⁡(3)#4‾},{(gcd2,(1,2)),(gcd2,(3,1))}>5⟼Default<(gcd⁡(3)#4:2‾,gcd⁡(3)#3:3),{gcd⁡(3)#3,gcd⁡(3)#4},{(gcd2,(1,2)),(gcd2,(3,1))}>5⟼apply gcd2<(K3 is 3−3,gcd⁡(K3)‾,gcd⁡(3)#3:3),{gcd⁡(3)#3},{(gcd2,(1,2)),(gcd2,(3,1)),(gcd2,(3,4))‾}>5⟼Solve+Wake<(gcd⁡(0)‾,gcd⁡(3)#3:3),{gcd⁡(3)#3},{(gcd2,(1,2)),(gcd2,(3,1)),(gcd2,(3,4))}>5⟼Activate<(gcd⁡(0)#5:1‾,gcd⁡(3)#3:3),{gcd⁡(3)#3,gcd⁡(0)#5‾},{(gcd2,(1,2)),(gcd2,(3,1)),(gcd2,(3,4))}>6⟼apply gcd1<(true‾,gcd⁡(3)#3:3),{gcd⁡(3)#3},{(gcd2,(1,2)),(gcd2,(3,1)),(gcd2,(3,4)),(gcd1,(1))‾}>6⟼Solve+Wake<(gcd⁡(3)#3:3),{gcd⁡(3)#3},{(gcd2,(1,2)),(gcd2,(3,1)),(gcd2,(3,4)),(gcd1,(1))}>6⟼Default<(gcd⁡(3)#3:4‾),{gcd⁡(3)#3},{(gcd2,(1,2)),(gcd2,(3,1)),(gcd2,(3,4)),(gcd1,(1))}>6⟼Drop<(),{gcd⁡(3)#3},{(gcd2,(1,2)),(gcd2,(3,1)),(gcd2,(3,4)),(gcd1,(1))}>6\begin{array}{ll} & <(\mathrm{gcd}(6), \mathrm{gcd}(9)), \emptyset, \emptyset>_{1} \\ \longmapsto_{Activate} & <(\underline{\mathrm{gcd}(6) \# 1: 1}, \operatorname{gcd}(9)),\{\underline{\mathrm{gcd}(6) \# 1}\}, \emptyset>_{2} \\ \longmapsto_{Default} & <(\underline{\gcd(6) \# 1:2}, \gcd(9)),\{\gcd(6) \# 1\}, \emptyset>_{2} \\ \longmapsto_{Default} & <(\underline{\gcd(6) \# 1:3}, \gcd(9)),\{\gcd(6) \# 1\}, \emptyset>_{2} \\ \longmapsto_{Default} & <(\underline{\gcd(6) \# 1:4}, \gcd(9)),\{\gcd(6) \# 1\}, \emptyset>_{2} \\ \longmapsto_{Drop} & <(\gcd(9)),\{\gcd(6) \# 1\}, \emptyset>_{2} \\ \longmapsto_{Activate} & <(\underline{\gcd(9)\#2:1}),\{\gcd(6) \# 1, \underline{\gcd(9)\#2}\}, \emptyset>_{3} \\ \longmapsto_{Default} & <(\underline{\gcd(9)\#2:2}),\{\gcd(6) \# 1, \gcd(9)\#2\}, \emptyset>_{3} \\ \longmapsto_{apply \text{ gcd2}} & <(\underline{K_1\text{ is }9-6,\gcd(K_1)}),\{\gcd(6) \# 1\}, \{ \underline{(\text{gcd2}, (1,2))} \}>_{3} \\ \longmapsto_{Solve+Wake} & <(\underline{\gcd(3)}),\{\gcd(6) \# 1\}, \{ (\text{gcd2}, (1,2)) \}>_{3} \\ \longmapsto_{Activate} & <(\underline{\gcd(3)\#3:1}),\{\gcd(6) \# 1, \underline{\gcd(3)\#3}\}, \{ (\text{gcd2}, (1,2)) \}>_{4} \\ \longmapsto_{Default} & <(\underline{\gcd(3)\#3:2}),\{\gcd(6) \# 1, \gcd(3)\#3\}, \{ (\text{gcd2}, (1,2)) \}>_{4} \\ \longmapsto_{Default} & <(\underline{\gcd(3)\#3:3}),\{\gcd(6) \# 1, \gcd(3)\#3\}, \{ (\text{gcd2}, (1,2)) \}>_{4} \\ \longmapsto_{apply \text{ gcd2}} & <(\underline{K_2 \text{ is }6-3,\gcd(K_2)},\underbrace{\gcd(3)\#3:3}_{保留active状态}),\{ \gcd(3)\#3\}, \{ (\text{gcd2}, (1,2)), \underline{(\text{gcd2}, (3,1))} \}>_{4} \\ \\ \longmapsto_{Solve+Wake} & <(\underline{\gcd(3)},\gcd(3)\#3:3),\{ \gcd(3)\#3\}, \{ (\text{gcd2}, (1,2)), (\text{gcd2}, (3,1)) \}>_{4} \\ \longmapsto_{Activate} & <(\underline{\gcd(3)\#4:1},\gcd(3)\#3:3),\{ \gcd(3)\#3,\underline{\gcd(3)\#4}\}, \{ (\text{gcd2}, (1,2)), (\text{gcd2}, (3,1)) \}>_{5} \\ \longmapsto_{Default} & <(\underline{\gcd(3)\#4:2},\gcd(3)\#3:3),\{ \gcd(3)\#3,\gcd(3)\#4\}, \{ (\text{gcd2}, (1,2)), (\text{gcd2}, (3,1)) \}>_{5} \\ \longmapsto_{apply \text{ gcd2}} & <(\underline{K_3 \text{ is } 3-3,\gcd(K_3)},\gcd(3)\#3:3),\{ \gcd(3)\#3\}, \{ (\text{gcd2}, (1,2)), (\text{gcd2}, (3,1)), \underline{(\text{gcd2}, (3,4))} \}>_{5} \\ \longmapsto_{Solve+Wake} & <(\underline{\gcd(0)},\gcd(3)\#3:3),\{ \gcd(3)\#3\}, \{ (\text{gcd2}, (1,2)), (\text{gcd2}, (3,1)), (\text{gcd2}, (3,4)) \}>_{5} \\ \longmapsto_{Activate} & <(\underline{\gcd(0)\#5:1},\gcd(3)\#3:3),\{ \gcd(3)\#3,\underline{\gcd(0)\#5}\}, \{ (\text{gcd2}, (1,2)), (\text{gcd2}, (3,1)), (\text{gcd2}, (3,4)) \}>_{6} \\ \longmapsto_{apply \text{ gcd1}} & <(\underline{\text{true}},\gcd(3)\#3:3),\{ \gcd(3)\#3\}, \{ (\text{gcd2}, (1,2)), (\text{gcd2}, (3,1)), (\text{gcd2}, (3,4)), \underline{(\text{gcd1}, (1))} \}>_{6} \\ \longmapsto_{Solve+Wake} & <(\gcd(3)\#3:3),\{ \gcd(3)\#3\}, \{ (\text{gcd2}, (1,2)), (\text{gcd2}, (3,1)), (\text{gcd2}, (3,4)), (\text{gcd1}, (1)) \}>_{6} \\ \longmapsto_{Default} & <(\underline{\gcd(3)\#3:4}),\{ \gcd(3)\#3\}, \{ (\text{gcd2}, (1,2)), (\text{gcd2}, (3,1)), (\text{gcd2}, (3,4)), (\text{gcd1}, (1)) \}>_{6} \\ \longmapsto_{Drop} & <(),\{ \gcd(3)\#3\}, \{ (\text{gcd2}, (1,2)), (\text{gcd2}, (3,1)), (\text{gcd2}, (3,4)), (\text{gcd1}, (1)) \}>_{6} \\ \end{array}

此时S={gcd⁡(3)#3}S = \{ \gcd(3)\#3\}即为最终执行结果。

总结

至此，你已经学完了 CHR 所有的语法和语义。你已经精通CHR语言本身了！所有的CHR程序，只要按照这里讲的步骤一步步代入，你都能看懂。

本系列接下来的文章，将着重在应用层面。另外，像CHR、Mercury这样的语言，同时都会给出 declarative 和 operational 两套语义。操作语义（operational semantics）描述一个语言的代码应该怎么执行。declarative semantics从声明的角度描述一个语言“这么写是什么意思”。后续的文章将会给出正式的declarative semantics。

  1. 这种设定有点类似ISO C。在ISO C中，表达式的计算顺序是任意的，补救的一个设定是，如果表达式中改变一个变量的值两次，那么是undefined behavior。在这种情况下，我们不知道到底会不会有同一个变量在不确定的顺序中被更新两次，这两次更新的先后顺序是不确定的，因而最终的结果也是不可预测的。 ↩︎

  2. 结果中的X = 3并不是此时CHR Store中的内容。Prolog 每次显示查询的执行结果，都会把执行过程中被 unify 的变量的值给显示出来，所以这里多了X = 3。 ↩︎