合取查询

合取查询像一张带共享空格的事实清单。填入一个课程名后，“学生选了这门课”和“教师教这门课”必须同时在表中找到。共享空格强制两条事实谈论同一门课；存在量词说明只需找到一种填法，不要求把填法交给用户。

变量名字不同，只是允许独立选择，并没有要求选到不同对象。把两个空格都填成同一个值，常常正是合法答案；这种匹配不是把查询图单射地嵌入数据图。

包含问的是：“只要第一张事实清单能填成，第二张是不是也一定能填成？”反向同态先把第二张清单的空格接到第一张清单的空格或常量上；随后第一张清单在任何数据库中的填法，都能沿着这些接线传给第二张。规范数据库则把第一张清单直接做成一份数据，让这个问题有一份固定的测试材料。

从问题到规则、连接与答案 ​

问题是“找出学生及其所选课程的授课教师”。取三行选课表与三行授课表：

其公式和规则分别写为

箭头表示右侧事实成立便产生左侧答案，不是给表增加一条约束。关系代数公理库关系代数Relational algebra · Set relational algebra用选择、投影、积、重命名与集合运算组合有限关系查询，并在集合语义下解释连接和存在见证。实现为 ${\pi }_{\mathsf{Student},\mathsf{Teacher}}(\mathsf{Enroll}\bowtie \mathsf{Teach})$。连接的五个见证元组依次是甲—算法—林、甲—数据库—林、甲—数据库—周、乙—数据库—林、乙—数据库—周。投影后四个答案为甲—林、甲—周、乙—林、乙—周。

甲—林既可用算法作见证，也可用数据库作见证。若只问周的学生，得到甲、乙；从 Teach 删除数据库—周后，这个答案变为空。反之，只扩大未使用的外部论域，答案不变。

这条规则只读取给定的输入表。Datalog 与有限最小不动点公理库Datalog 与有限最小不动点Datalog · Positive Datalog · Datalog least model在固定有限活跃域上反复应用正规则，证明所得关系是最小模型，并用有环可达性逐轮推导半朴素求值。进一步允许规则体使用规则自己定义的关系：反复加入新答案，直到关系闭合。正体匹配的含义不变，但递归答案必须由最小模型确定，不能只执行一轮查询。

为什么代数实现对所有实例成立 ​

若 $(s,t)$ 在投影结果中，就存在一个连接元组 $(s,c,t)$；连接的定义给出 $\mathsf{Enroll}(s,c)$ 和 $\mathsf{Teach}(c,t)$，因此 $c$ 满足公式。反过来，公式的任何见证 $c$ 都提供两条可连接的输入事实，组成 $(s,c,t)$，投影产生 $(s,t)$。两个方向都不依赖示例中的具体名字或行数，所以证明适用于该模式的所有实例。

不同变量不表示不同对象 ​

对单自环关系 $E=\{(a,a)\}$，布尔查询 $\mathrm{\exists }x\mathrm{\exists }yE(x,y)$ 为真，见证就是 $x=y=a$。若业务要求两个不同节点，需要写出 $x\ne y$，但这已扩展了本页的纯合取查询语言。重复变量 $E(x,x)$ 则直接要求自环，无需额外等式原子。

加入显式等式原子时，可以合并被等式识别的变量、把与常量相等的变量替换掉，但还必须保持输出有范围；两个不同常量被要求相等时，查询恒空。这类扩展不能悄悄混入不含等式的定义。析取得到合取查询的并，否定引入差集式条件，也都超出了本页片段。

同一查询对：合并中点证明包含 ​

在同一个二元关系 $E$ 上，比较下面两个二元输出查询。$q_S$ 要求中点具有自环，$q_W$ 要求一条普通的三步游走；“游走”允许重复节点。

先判定 $q_S\subseteq q_W$。所需方向为 $h:q_W\to q_S$，取

三个原子的像依次是 $E(x,y)$、$E(y,y)$、$E(y,z)$，头 $(u,v)$ 的像为 $(x,z)$。所有条件都满足，因此包含成立。两边都有三个原子，不能靠比较条件数量得到这个结论；关键是允许把 $r,s$ 合并为 $y$。

再用规范测试核对：冻结 $x,y,z$ 为互异的新值 $a,b,c$，得到

$q_W$ 取 $u=a,r=b,s=b,v=c$ 就返回 $t_S$。进一步算出全部答案：$q_S$ 的中点只能为 $b$，起点可以是 $a,b$，终点可以是 $b,c$；$q_W$ 的两个中点也都只能为 $b$。因此

这四对答案相同只核验了一份实例；全实例包含仍由同态及后面的证明保证。

反向失败：用同一查询对构造反例 ​

若要证明 $q_W\subseteq q_S$，就需要 $q_S\to q_W$ 的同态。但 $E(y,y)$ 的像必然仍为自环原子，而 $q_W$ 的原子中没有自环，故这种同态不存在。这里的理由排除了所有候选映射，而不只是某次尝试失败。

冻结 $q_W$ 的 $u,r,s,v$ 为四个互异新值 $a,b,c,d$：

这条链唯一的三步游走从 $a$ 到 $d$，所以 $q_W(D_W)=\{(a,d)\}$。链上没有自环，$q_S(D_W)=\varnothing$。于是 $D_W$ 和 $t_W$ 给出了反向包含的具体有限反例，也说明前一份实例上答案相同不足以推出查询等价。

迁移题：中点成为常量以后 ​

把中点的一部分位置改成固定常量 $k$：

仍有 $q_S^k\subseteq q_W^k$：取 $u\mapsto x,v\mapsto z,s\mapsto k$，并保持 $k\mapsto k$，即可逐原子、逐头坐标验证。反向仍失败：取 $E=\{(a,k),(k,b),(b,c)\}$，其中 $a,k,b,c$ 互异；$q_W^k$ 恰返回 $(a,c)$，$q_S^k$ 因缺少 $E(k,k)$ 而为空。不能移动常量 $k$ 来修复失败，因为两个查询中的 $k$ 始终指同一个固定值。

集合见证不能代替重复次数 ​

取 $p(x)\leftarrow E(x,y)$ 和 $p^{\prime }(x)\leftarrow E(x,y),E(x,z)$。将 $y,z$ 合并给出一个方向的同态，选择其中一个原子给出另一方向，所以它们在集合语义下等价。但令 $E=\{(a,b),(a,c)\}$，每条输入事实只出现一次，不去重的投影为 $p$ 输出两次 $a$，为 $p^{\prime }$ 输出四次 $a$：后者的 $(y,z)$ 有 $(b,b),(b,c),(c,b),(c,c)$ 四种选择。包含定理保存“存在见证”，没有保存见证的数量，不能据此直接证明 bag 语义下的等价改写。

查询来源与半环标注公理库查询来源与半环标注Query provenance · Provenance semiring · K-relation · 查询溯源用有限支撑的半环标注关系记录查询见证，证明来源多项式的通用求值性质，并计算重数、事实删除与最小见证击中集。进一步给每条输入事实一个符号，用乘法记录同一见证使用的事实，用加法保留替代见证。它复用本页的六条选课与授课事实，为甲—林得到 $p_1{t}_1+p_2{t}_2$，并计算删除授课事实后哪些答案仍有支持。多项式保留重复原子的出现次数、同一事实的复用幂次与推导重数，所以本页把查询体视为原子集合的约定只直接适用于集合语义。

依赖约束改变了允许实例 ​

若只比较满足约束集合 $\mathrm{\Sigma }$ 的实例，就应写 $q_1{\subseteq }_{\mathrm{\Sigma }}{q}_2$。例如 $p(x)\leftarrow P(x)$ 与 $p^{\prime }(x)\leftarrow P(x),Q(x)$ 在约束 $\mathrm{\forall }x(P(x)\to Q(x))$ 下等价；然而 $p$ 的原规范实例只有 $P(a)$，没有 $Q(a)$，它本身违反约束，不能充当合法反例。

本例补上 $Q(a)$ 就满足约束。系统地补事实或合并值会进入后续的 chase 方法；这里不把无约束定理扩写为一般约束的判定程序。对更一般依赖，chase 可能不终止，有限实例上的结论也需要相应约束类别的额外定理。这个边界可对照 Pieris 的 ATFD 2018/19 Lecture 3，PDF 第 10–11、18 页。

只含函数依赖时，可以采用一个更受限且保证终止的等式过程。函数依赖的追赶检验公理库函数依赖的追赶检验FD chase · Lossless join chase test在固定符号表中全局合并被函数依赖强制相等的值，以全标记行证明无损，以终止表构造合法有损反例。不生成新事实，而在固定表中合并被依赖强制相同的符号；每次有效合并减少符号类数。针对投影分解，它用全标记行证明无损，用无成功行的终止表构造满足约束的反例。这保留了规范数据库“把符号冻结成证据”的思想，却先修复了原符号表可能违反约束的问题；其终止证明不覆盖上面的事实生成依赖。

为什么反向同态恰好刻画包含 ​

先证明有同态就有包含。取任意允许实例 $I$、任意 $\overline{a}\in q_1(I)$，并取产生它的成功赋值 $v$；把 $v$ 在常量上也看成恒等映射。给 $q_2$ 使用函数复合公理库函数复合Function composition · Composition of maps按先 f 后 g 的次序把映射串联为 g∘f。 $g=v\circ h$。对其任意原子 $R(\overline{t})$，同态条件保证 $R(h(\overline{t}))$ 是 $q_1$ 原子，成功赋值又保证 $R(v(h(\overline{t})))$ 是 $I$ 的事实。因此 $g$ 满足 $q_2$ 的全部原子，并且

所以 $\overline{a}\in q_2(I)$。这也解释方向为什么不能颠倒：已知的是 $q_1$ 的见证，需要先把 $q_2$ 的项送入 $q_1$，才能复用这份见证。

再证明包含蕴含规范测试。冻结赋值本身满足 $q_1$ 的所有原子，所以 $t_1\in q_1(D_1)$。$D_1$ 是一份允许的有限实例，由包含立即得到 $t_1\in q_2(D_1)$。

最后证明规范测试产生同态。设 $w$ 是 $q_2$ 在 $D_1$ 上返回 $t_1$ 的赋值。每个变量都出现在正关系原子中，因此它的成功取值一定出现在某条 $D_1$ 事实里，只可能是一个冻结值或 $q_1$ 的常量值。定义解冻映射 $\delta$：把 $\hat{z}$ 还原为 $q_1$ 的变量 $z$，保持所有常量不变。新值互异且避开常量，保证解冻不会混淆这两类项。

令 $h=\delta \circ w$。对 $q_2$ 的每个原子，它经 $w$ 得到的事实属于 $D_1$，而 $D_1$ 的事实恰由 $q_1$ 原子冻结得到，解冻后便是 $q_1$ 原子。常量保持不变，且 $w(\mathrm{head}(q_2))=t_1$ 给出 $h(\mathrm{head}(q_2))=\mathrm{head}(q_1)$。故 $h:q_2\to q_1$ 满足全部要求。若 $q_2$ 没有变量，变量映射为空，同样逐原子检查；空合取的布尔恒真查询也包含在这一步内。

改写与单调性 ​

合取查询具有单调性：只向输入关系增加元组时，已有见证不会消失，所以旧答案仍成立。带否定的查询一般没有这一性质，例如增加 $S(a)$ 会让 $R(x)\wedge \mathrm{\neg }S(x)$ 丢掉答案 $a$。这既是表达能力边界，也是检查业务问题是否需要否定的线索。

匹配可以用连接次序与投影位置来组织；改写时必须保留后续匹配需要的共享变量，不能先丢掉课程再做任意配对。包含定理提供了集合语义下的改写证书：两个方向各给一个同态，就证明改写对所有有限实例保持答案；失败时，相应的规范数据库给出反例。

求值和包含是不同的判定问题 ​

联合求值复杂度把查询 $q$ 与数据库 $I$ 都作为输入，问布尔查询是否为真，或给定元组是否属于答案。它是 NP 完全的：猜出所有变量的取值，再逐原子检查，是多项式证书。Chandra 与 Merlin 原文 §4 Theorem 7 讨论的就是这种求值问题。

固定查询的数据复杂度只让 $I$ 及待测答案增长。此时变量数是常数，枚举赋值的数量是数据规模的固定次幂，因此有多项式时间算法。标准有限关系特征位编码下，判定甚至在 ${\mathrm{AC}}^0$：每个候选赋值对应一组输入事实位的 AND，再把这些结果 OR 起来，得到常数深度、多项式规模电路。这里说的是布尔或成员判定，不是恒定时间输出整张结果表；参见 CS784 Spring 2021 Lecture 3，§3.2、Theorem 3.9。

查询包含的输入只有 $q_1,q_2$，没有待求值数据库。它也是 NP 完全的：证书是 $h:q_2\to q_1$，每个变量的像、原子的像与头坐标都能在多项式时间内检查。NP 难性可由无向图三着色看出：令固定布尔查询 $q_K$ 使用三个变量 $c_1,c_2,c_3$，包含全部六个 $E(c_i,c_j)$ 原子，其中 $i\ne j$；对输入图 $G$，令布尔查询 $q_G$ 为每条无向边写两个方向的原子，孤立点可略去。则 $q_K\subseteq q_G$ 当且仅当存在 $q_G\to q_K$ 的同态，恰当于给图的节点分配三种颜色并要求邻点异色。目标是含六条有向弧、没有自环的完全图；三个单向环边不能代替它。

若固定查询并要求枚举全部完整见证，问题还包括输出规模与中间结果成本。最坏情形最优连接公理库最坏情形最优连接Worst-case optimal joins · WCOJ · AGM bound · 分数边覆盖界用分数边覆盖证明集合连接的最大输出规模，并以三角形的重轻分解避免二元连接的巨大中间结果。用属性超图的分数边覆盖证明最大输出规模，并通过三角形的重轻分解避免先物化巨大的二元连接。这是枚举算法的保证，与上面的成员判定、查询包含不是同一个复杂度问题。