图转换系统与多值动作语言：CLP中的探索

### 图转换系统与多值动作语言：CLP 中的探索 #### 1. 图转换系统与约束处理规则的融合 在图转换系统（GTS）和约束处理规则（CHR）的研究中，我们发现 CHR 为嵌入 GTS 提供了一种优雅的方式。在图转换过程中，图生产规则会改变节点的度。对于节点 \(v \in K\)，图生产规则使 \(m(v)\) 的度改变 \(m - n\)，约束 \(degree(T, D + m - n)\) 直接编码了这种变化，为节点提供了一致的度编码。对于图生产规则新添加的节点 \(v \in R \setminus K\)，我们会根据定义明确添加正确度的度约束。 ##### 1.1 合流性相关概念 合流性是 GTS 和 CHR 都具备的重要属性。它保证了对于初始状态的任何推导，无论应用哪些适用规则，最终都会得到相同的最终状态。 - **GTS 合流性**：一个 GTS 被称为合流的，如果对于所有类型化的图转换 \(G \stackrel{*}{\Rightarrow} H1\) 和 \(G \stackrel{*}{\Rightarrow} H2\)，存在一个类型化的图 \(X\) 以及类型化的图转换 \(H1 \stackrel{*}{\Rightarrow} X\) 和 \(H2 \stackrel{*}{\Rightarrow} X\)。局部合流性则是指对于所有直接类型化的图转换对 \(G \Rightarrow H1\) 和 \(G \Rightarrow H2\) 该属性都成立。 - **关键 GTS 对**：一对直接类型化的图转换 \(P1 \stackrel{r1,m1}{\Leftarrow} K \stackrel{r2,m2}{\Rightarrow} P2\) 被称为关键 GTS 对，如果它是并行依赖的，并且匹配 \(m1 : L1 \to K\) 和 \(m2 : L2 \to K\) 的对 \((m1, m2)\) 是联合满射的。若 \(m1(L1) \cap m2(L2) \subseteq m1(K1) \cap m2(K2)\)，则这对图转换是并行独立的，否则是并行依赖的。如果存在一个类型化的图 \(K'\) 以及类型化的图转换 \(P1 \stackrel{*}{\Rightarrow} K'\) 和 \(P2 \stackrel{*}{\Rightarrow} K'\)，则关键 GTS 对是可连接的。 - **CHR 合流性**：一个 CHR 程序被称为合流的，如果对于所有状态 \(S\)、\(S1\) 和 \(S2\)，若 \(S \stackrel{*}{\to} S1\) 且 \(S \stackrel{*}{\to} S2\)，则 \(S1\) 和 \(S2\) 是可连接的。两个状态 \(S1\) 和 \(S2\) 可连接是指存在状态 \(T1\) 和 \(T2\)，使得 \(S1 \stackrel{*}{\to} T1\)，\(S2 \stackrel{*}{\to} T2\)，并且 \(T1\) 和 \(T2\) 是变体。 - **关键 CHR 对**：设 \(R1\) 是一个简化规则，\(R2\) 是一个（不一定不同）变量已重命名的规则。设 \(Hi \land Ai\) 是规则 \(Ri\)（\(i = 1, 2\)）的头，\(Gi\) 是其保护条件。如果 \(A1\) 和 \(A2\) 是非空合取式，且 \(CT \models \exists((A1 \neq A2) \land G1 \land G2)\)，则 \(R1\) 和 \(R2\) 的关键祖先状态是 \(\langle H1 \land A1 \land H2, (A1 \neq A2) \land G1 \land G2 \rangle\)。若 \(S\) 是 \(R1\) 和 \(R2\) 的关键祖先状态，使用规则 \(R1\) 使 \(S \to S1\)，使用规则 \(R2\) 使 \(S \to S2\)，则元组 \((S1, S2)\) 是 \(R1\) 和 \(R2\) 的关键 CHR 对。如果 \(S1\) 和 \(S2\) 可连接，则关键 CHR 对是可连接的。 ##### 1.2 关键对性质 对于编码 GTS 的 CHR 程序，关键 GTS 对和关键 CHR 对之间存在重要关系。 - **引理 3**：如果 \(P1 \stackrel{p1,m1}{\Leftarrow} G \stackrel{p2,m2}{\Rightarrow} P2\) 是一个关键 GTS 对，那么存在一个内置约束的合取 \(C\)，使得 \(\langle encode(G), \top \rangle\) 是关键 CHR 对 \((\langle encode(P1), C \rangle, \langle encode(P2), C \rangle)\) 的关键祖