一阶逻辑视图查询的可判定性

# 一阶逻辑视图查询的可判定性 在数据库查询领域，一阶逻辑视图查询的可判定性是一个关键问题。它涉及到能否有效地判断一个查询是否有解，以及如何扩展查询语言的表达能力而不失去可判定性。下面我们将深入探讨相关内容。 ## 1. 复制与修剪证明层次结构 首先，我们来了解复制与修剪证明层次结构的过程。设 $I_{max}$ 是 $\varphi$ 模型的一个最大化层次结构集合，$n_l$ 是高度为 $m$ 时的常量数量。则有： $n_l \leq$（最大证明层次结构集合中的层次结构数量）×（视图数量×视图最大长度）$^m$ $\leq 2^N \times (N \times m)^m$ 在这一步，我们制作 $n_l$ 个 $I_{max}$ 的副本，分别记为 $I_1, I_2, \cdots, I_{n_l}$，每个副本使用不同的常量集合。设 $I_{union}$ 是 $I_1 \cup I_2 \cup \cdots \cup I_{n_l}$ 的并集。可以验证，对于这个新实例，$\varphi$ 仍然为真。 接下来，移除层次结构中 $m$ 以下的所有级别，并通过用同一类别的某个副本的根重新证明 $m$ 级的常量，将它们“环绕”起来。同样可以验证，对于这个新实例，$\varphi$ 仍然为真。 $I_{union}$ 中的常量数量有界，满足： $\leq$ 副本数量 ×（高度为 $m + 3$ 的证明层次结构中的最大常量数量） $\leq n_l \times (2^N \times (N \times m)^m + 3)$ $\leq (2^N \times (N \times m)^m) \times (2^N \times (N \times m)^m + 3)$ $\leq 2^{2N} \times (N \times m)^{2m + 3}$ $\leq 2^{2\times(m\times p)^m\times m} \times ((m \times p)^m \times m \times m)^{2m + 3}$，其复杂度为 $O(2^{(m\times p)^m})$ 定理 1 对于无限模型也成立，因为即使初始证明层次结构是无限的，引理 1 中使用的方法仍然可以用于展示一个有限模型。因此，我们得到有限可控性（每个可满足的公式都是有限可满足的）。 命题 1：一阶一元合取视图语言是有限可控的。 ## 2. 扩展视图定义 前面的内容表明，使用一元合取视图定义的一阶语言是可判定的。自然地，我们会想通过使视图体更具表达力（同时保持视图的一元性）来增强语言的能力。然而，这样做会导致可满足性变得不可判定。 ### 2.1 允许视图中存在不等式 考虑的第一种扩展是允许视图中存在不等式，例如： $V(X) \leftarrow R(X, Y), S(X, X), X \neq Y$ 将基于此类视图的一阶语言称为一阶一元合取 $\neq$ 视图语言。这种语言可以用来检查双计数器机器的计算是否有效并终止。这就引出了以下结果： **定理 2**：一阶一元合取 $\neq$ 视图查询语言的可满足性是不可判定的。 证明过程是通过将双计数器机器（2CM）从计数器为零开始的停机问题进行归约。对于任何 2CM 的描述及其计算，我们可以展示如何： 1. 将此描述编码到数据库关系中。 2. 定义查询来检查此描述。 我们构造一个查询，当且仅当 2CM 停机时，该查询是可满足的。模拟的基本思想与文献中的类似，但主要区别在于后继关系中允许存在循环，不过必须至少有一个有效链。 ### 2.2 允许合取视图中存在“安全”否定 第二种扩展是允许合取视图中存在“安全”否定，例如： $V(X) \leftarrow R(X, Y), \neg S(X, X)$ 将基于此类视图的一阶语言称为一阶一元合取 $\neg$ 视图语言。根据相关结果，它也是不可判定的。 **定理 3**：一阶一元合取 $\neg$ 视图查询语言的可满足性是不可判定的。 ### 2.3 允许视图具有二元性 第三种增加视图表达力的可能性是保持视图体为纯合取查询，但允许视图具有二元性，例如： $V(X, Y) \leftarrow R(X, Y)$ 这种语言也不是可判定的，