用于查询包含性检查的构造性方法

### 用于查询包含性检查的构造性方法 #### 1. 引言 查询包含性（QC）旨在检查对于任意可能的数据库内容，一个查询在数据库上获得的答案是否是另一个查询在同一数据库上获得答案的子集。此前处理否定的方法可分为两类： - 一类方法用于检查否定使用受限的查询类的QC。 - 另一类方法并不直接检查QC，而是检查另一个相关属性——统一查询包含性（Uniform QC），它是QC的充分非必要条件。 下面通过一个例子说明这些方法的局限性。考虑一个演绎数据库，包含两个基本谓词： - `Emp(x)` 表示 x 是员工。 - `Works_for(x, y)` 表示 x 为 y 工作。 还有两个派生谓词： - `Boss(x)` 表示 x 有下属为其工作。 - `Chief(x)` 表示 x 有老板为其工作。 定义两个查询： - `Q1: Sub(x) ← Emp(x) ∧ ¬Chief(x)` - `Q2: Sub(x) ← Emp(x) ∧ ¬Boss(x)` 直观上，`Q1` 检索不是 `Chief` 的员工，即没有老板为其工作的员工；`Q2` 检索不是 `Boss` 的员工，即没有下属为其工作的员工。`Q1` 的限制比 `Q2` 少，因此可以找到一个数据库，如 `{Emp(joan), Works_for(ann, joan)}`，表明 `Q1` 的答案不一定是 `Q2` 的答案，即 `Q1` 不包含于 `Q2`。相反，`Q2` 的所有答案都是 `Q1` 的答案，所以 `Q2` 包含于 `Q1`。但现有方法无法很好地处理这个例子。 当考虑数据库中的完整性约束时，两个查询之间的包含关系仅需在满足完整性约束的数据库状态下成立，这就是IC - 兼容查询包含性的概念。当前处理IC - 兼容QC的方法采用统一包含性方法，而我们的构造性方法可以统一且集成地检查“真正的”IC - 兼容QC和QC。 构造性方法的主要思想是构造一个反例，证明与我们要检查的[IC - 兼容]QC关系相反的情况。如果构造过程失败，则[IC - 兼容]QC成立。该方法基于将QC问题简化为视图更新问题，专门针对QC检查的特点对视图更新的事件方法进行了优化。 #### 2. 基本概念 - **演绎数据库**：演绎数据库 `D` 是一个三元组 `D = (EDB, DR, IC)`，其中 `EDB` 是有限的事实集，`DR` 是有限的演绎规则集，`IC` 是有限的完整性约束集。基本谓词仅出现在 `EDB` 和 `DR` 中演绎规则的主体中，派生（视图）谓词仅出现在 `DR` 中，可评估（内置）谓词（如算术比较）无需访问数据库即可评估。 - **安全性和分层否定**：要求出现在否定或可评估原子中的变量必须出现在同一规则主体的正派生或基本文字中（安全性），并且递归定义的派生谓词不能有负文字（分层否定）。 - **完整性约束**：完整性约束是每个 `EDB` 都必须满足的公式，我们处理否定形式的约束：`← L1 ∧ … ∧ Lm`（m ≥ 1）。为了统一，为每个完整性约束关联一个不一致谓词 `Icn`，并将否定形式重写为完整性规则 `Ic1 ← L1 ∧… ∧Lm`。还定义了一个标准辅助谓词 `Ic`，每个完整性约束对应一个规则 `Ic ←Ic1, … Ic ←Icn`，事实 `Ic` 表示存在违反的完整性约束。 - **查询**：查询 `Q` 是一组有限的演绎规则，定义了一个专用的n元查询谓词 `Q`。假设 `Q` 中除 `Q` 之外的所有谓词都属于数据库 `D`。查询的答案是通过在 `EDB` 上评估 `Q` 和 `DR` 中的演绎规则得到的关于 `Q` 的所有基本事实的集合。 查询包含性的定义如下： - **定义2.1**：设 `Q1` 和 `Q2` 是在演绎数据库 `D = (EDB, DR, IC)` 上定义相同n元查询谓词 `Q` 的两个查询。如果对于任何 `EDB`，`{Q(ai1, ..., ain) | Q(ai1, ..., ain) ∈ (Q1∪DR)(EDB)} ⊆ {Q(ak1, ..., akn) | Q(ak1, ..., akn) ∈ (Q2∪DR)(EDB)}`，则 `Q1` 包含于 `Q2`，记为 `Q1 ⊆ Q2`。 - **定义2.2**：设 `Q1` 和 `Q2` 是在演绎数据库 `D = (EDB, DR, IC)` 上定义相同n元查询谓词 `Q` 的两个查询。如果对于任何满足 `Ic ∉ (IC∪DR)(EDB)` 的 `EDB`，`{Q(ai1, ..., ain) | Q(ai1, ..., ain) ∈ (Q1∪DR)(EDB)} ⊆ {Q(ak1, ..., akn) | Q(ak1, ..., akn) ∈ (Q2∪DR)(EDB)}`，则 `Q1` 是IC - 兼容包含于 `Q2`，记为 `Q1 ⊆IC Q2`。 #### 3. 用于QC检查的构造性方法 为了检查QC，一种合适的方法是检查包含性的缺失，即找到一个数据库，使得要检查的包含关系不成立。 给定两个在演绎数据库 `D = (EDB, DR, IC)` 上定义相同n元查询谓词 `Q` 的查询 `Q1` 和 `Q2`，构造性方法（CQC方法）旨在构造一个数据库 `T`，使得假定的包含关系不成立。如果方法成功，则证明不包含；否则，包含关系成立。 该方法的步骤如下： 1. **定义非包含目标**： - 当要证明 `Q1 ⊆ Q2` 不成立