字符串图上下文无关族的等式推理

### 字符串图上下文无关族的等式推理 #### 1. 字符串图重写规则基础 在字符串图的匹配过程中，匹配需满足关于左图（L）边界的“无悬空线”条件，并且匹配是在线同胚的意义下进行的。这意味着目标图中的线在必要时可以伸展，以实现模式的单射嵌入。通常，字符串图重写规则编码为跨度 $L \leftarrow B \rightarrow R$，其中 $B$ 是 $L$ 和 $R$ 的公共边界。 对于字符串图 $G$ 由规则 $L \leftarrow B \rightarrow R$ 进行重写，使用匹配 $m : L \rightarrow \tilde{G}$（其中 $\tilde{G} \sim G$），这一过程包括在字符串图范畴（SGraph）中先求推出补（pushout complement），再求推出（pushout）。已有研究表明，对于字符串图重写规则左图的任何匹配，推出补和推出都存在且唯一，所以字符串图重写规则的双推出（DPO）重写是定义良好的。 #### 2. 编码字符串图与 B - ESG 文法 为了定义字符串图的族，引入了一种上下文无关图文法，即 B - ESG 文法，它本质上是对 B - edNCE 文法类的一种限制。为了获得更强的表达能力，使用该文法生成编码字符串图，而非直接生成字符串图。 - **编码字符串图**：设 $E = \{α, β, …\}$ 是一个有限的编码符号集。编码字符串图是一种字符串图，其中允许用编码符号 $α \in E$ 标记的边连接一对节点顶点。 - **解码系统**：解码系统 $T$ 是一组 DPO 重写规则，对于每个三元组 $(α, N_1, N_2) \in E × N × N$ 都有一个规则。规则的左图由一条标记为 $α$ 的边连接一个标记为 $N_1$ 的节点顶点和一个标记为 $N_2$ 的节点顶点，右图是一个不包含输入、输出或编码标签的连通字符串图。解码系统 $T$ 是合流且终止的，解码编码字符串图就是相对于 $T$ 进行规范化。 **B - ESG 文法**：B - ESG 文法是一个对 $B = (G, T)$，其中 $T$ 是解码系统，$G = (Σ, Δ, Γ, Γ, P, S)$ 是 B - edNCE 文法，并且对于每个产生式 $X \rightarrow (D, C) \in P$，需满足以下条件： |条件|描述| |----|----| |N1|一条边带有编码标签当且仅当它连接一对节点顶点。| |N2|任何形式为 $(N, α/β, x, d)$（其中 $N$ 是节点顶点标签，$x$ 是节点顶点）的连接指令，必须有 $β \in E$。| |W1|$D$ 中的每个线顶点的入度最多为 1，出度最多为 1。| |W2|不存在形式为 $(σ, α/β, x, d)$（其中 $σ$ 是任何顶点标签，$x$ 是线顶点）的连接指令。| |W3|对于线顶点标签 $W$ 以及每个 $γ$ 和 $d$，最多有一个形式为 $(W, γ/δ, x, d)$ 的连接指令，并且必须有 $δ \notin E$。| |W4|设 $y$ 是 $D$ 中标签为 $Y$ 的非终结顶点。如果 $y$ 通过方向为 $d$ 且标签为 $β$ 的边与标记为 $W$ 的线顶点相邻，或者存在形式为 $(W, α/β, y, d)$ 的连接指令，那么所有 $Y$ 的产生式必须包含形式为 $(W, β/γ, z, d)$ 的连接指令。| 这些条件保证了节点顶点除非通过编码标签的边，否则不会直接相连，并且线不会“分裂”，同时确保在推导过程中输入保持为输入，输出保持为输出。 **B - ESG 具体推导**：对于 B - ESG 文法 $B = (G, T)$，以 $S$ 为 $G$ 的初始非终结符，具体推导包括在 $G$ 中从 $S$ 推导出 $H_1$（$H_1$ 不包含非终结符），然后进行解码 $H_1 \Rightarrow_T^* H_2$。可以表示为 $S \Rightarrow_G^* H_1 \Rightarrow_T^* H_2$，或者如果图 $H_1$ 在上下文中无关紧要，可简记为 $S \Rightarrow_B^* H_2$。 下面是 B - ESG 具体推导的流程图： ```mermaid graph LR A[S] -->|G 推导| B[H1] B -->|T 解码| C[H2] ``` #### 3. B - ESG 文法的性质 - **定理 1**：B - ESG 文法语言中的每个图都是字符串图。通过归纳法证明，从 ESG 形式开始的任何推导都能得到编码字符串图，而解码编码字符串图总是产生字符串图。 - **引理 1**：对于每个 B - ESG 文法 $B = (G, T)$，存在 $n \in N$，使得如果 $H \in L(B)$，则 $H$ 不包含长度大于 $n$ 的线。这是因为在 $G$ 的具体推导中，线的最大长度受限于产生式体中线的最长长度，而解码过程不会增加线的长度。 ###