等式树自动机补运算封闭性探究

### 等式树自动机补运算封闭性探究 在自动机理论的研究中，等式树自动机是一个重要的领域。本文将深入探讨等式树自动机在补运算下的封闭性相关问题，涉及单向和双向自动机，以及不同等式理论下的情况。 #### 等式逻辑程序与树自动机 将树自动机视为逻辑程序，并通过添加等式理论对其进行扩展。同时，等式逻辑程序也有很多相关研究，它是一种包含特殊相等谓词的逻辑程序，等式理论可以编码在逻辑程序本身中。在这种情况下，等式树自动机的补运算对应于等式逻辑程序中的否定。不过，这里的等式树自动机有所不同，相等符号不在逻辑程序中出现，而是单独考虑一个包含相等谓词的等式理论。 双向等式树自动机的概念已针对AC理论及其变体进行了研究。特定的理论如ACUX、ACUM等，传统上在（单向）树自动机框架中未被考虑，它们会带来特定的技术问题和解决方案。此外，Colcombet的多集自动机在布尔运算下的封闭性也已得到证明，它对应于单向ACU自动机的一个子类，其中除了 + 和 0 之外的所有符号都是一元的。 #### 双向E - 树自动机 固定一个函数符号的签名 Σ，每个符号都有固定的元数，设 E 为一个等式理论，它在由 Σ 构建的项上诱导出一个同余关系 =E。使用一阶逻辑的子句来表示各种类别的自动机。 一个确定子句的形式为：$P(t) \Leftarrow P_1(t_1) \land \cdots \land P_n(t_n)$，其中 $P, P_1, \cdots, P_n$ 是谓词，$t, t_1, \cdots, t_n$ 是由 Σ 和变量构建的项。给定这样的确定子句的有限集合 C，使用以下两条规则定义基础原子的推导： - $\frac{P_1(t_1\sigma)\cdots P_n(t_n\sigma)}{P (t\sigma)}$，如果 $P (t) \Leftarrow P_1(t_1) \land \cdots \land P_n(t_n) \in C$ - $\frac{P (s)}{P (t)}$，如果 $s =E t$ 其中 σ 是一个基础替换。推导是一种树状结构，不要与由 Σ 构建的项（树）混淆。子推导是推导的子树，推导的最后一步指的是推导树根部的步骤。确定子句与自动机的联系如下：谓词是状态，确定子句的有限集合是自动机，原子 $P(t)$ 可使用 C 推导出来，当且仅当项 t 在自动机 C 的状态 P 下被接受。使用 C 的推导有时也称为自动机 C 的运行。 可推导原子的集合恰好是子句集合模 E 的最小Herbrand模型。 语言 $L_P (C/E)$ 是使得 $P(t)$ 可推导的项 t 的集合。当 E 为空理论时，记为 $L_P (C)$。如果指定某个状态 $P_f$ 为最终状态，那么自动机 C 接受的语言是 $L(C/E) = L_{P_f} (C/E)$。给定一个语言 L 和一个等式理论 E，$E(L)$ 表示满足 $t =E s$ 且 $s \in L$ 的项 t 的集合。 #### 单向和双向自动机的定义 单向自动机由以下子句组成： - $P(f(x_1, \cdots, x_n)) \Leftarrow P_1(x_1) \land \cdots \land P_n(x_n)$（pop子句） - $P(x) \Leftarrow P_1(x)$（epsilon子句） 这些（无方程的）自动机正是文献中通常描述的经典树自动机。pop子句可以理解为：如果项 $x_1, \cdots, x_n$ 分别在状态 $P_1, \cdots, P_n$ 下被接受，那么 $f(x_1, \cdots, x_n)$ 在状态 P 下被接受，通常用重写规则 $f(P_1, \cdots, P_n) \to P$ 表示；epsilon子句对应于重写规则 $P_1 \to P$。 有如下引理：对于任何单向自动机 C 和等式理论 E，$L_P (C/E) = E(L_P (C))$。特别地，单向 E 树自动机的空性是可判定的。但对于Ohsaki的正则 E 树自动机，只有当 E 是线性时该结果才成立。 由于处理的是扩展 ACU 的理论，假设 Σ 包含符号 +、0，在有方程 D 或 M 的情况下还包含符号 -。Σ 中除了 +、 -、0 之外的符号称为自由符号，零元自由符号称为常量。形式为 $f(t_1, \cdots, t_n)$（f 为自由符号）的项称为函数项。相应地，自动机中的 pop 子句有以下形式： - $P(x + y) \Leftarrow P_1(x) \land P_2(y)$ - $P(0)$ - $P(a)$（a 为常量） - $P(-x) \Leftarrow P_1(x)$ - $P(f(x_1, \cdots, x_n)) \Leftarrow P_1(x_1) \land \cdots \land P_n(x_n)$（f 为自由符号） 单向ACU（或ACUI、ACUX、ACUXn）自动机由子句 (3)、(4 - 6) 和 (8) 组成；单向ACUM和ACUD自动机还包含子句 (7)。 双向自动机是在单向自动机的基础上添加以下类型的子句（称为push子句）得到的： $Q(x_i) \Leftarrow P(f(x_1, \cdots, x_n)) \land Q_1(x_{i_1}) \land \cdots \land Q_k(x_{i_k})$，其中 f 为自由符号，$i \in \{1, \cdots, n\} \setminus \{i_1, \cdots, i_k\}$，$1 \leq i_1 < \cdots < i_k \leq n$。 常量自动机是一种单向自动机，它包含子句 (6) 而不是一般的子句 (8)（签名中唯一的自由符号是常量）。给定一个单向或双向自动机 C，定义 $C_{eq}$ 为 C 中包含子句 (3)、(4)、(5) 和 (7) 的部分（等式部分），$C_{free}$ 为其余部分。 以下是一个双向自动机的示例： 考虑一个具有常量 a 和 b、一元符号 f 和二元符号 g 的签名。定义模 ACUX 的双向自动机 A 由以下子句组成： (i) $P_1(a)$ (ii) $P_2(b)$ (iii) $P_3(f(x)) \Leftarrow P_2(x)$ (iv) $P_4(0)$ (v) $P_5(g(x, y)) \Leftarrow P_4(x) \land P_3(y)$ (vi) $P_6(x + y) \Leftarrow P_1