函数依赖的追赶检验

形式陈述

从分解构造符号表

本页判定无损连接分解：输入有限属性集 $U$ 、有限 FD 集 $F$ 与覆盖 $U$ 的分解 $\mathcal D=\{U_1,\ldots,U_m\}$ 。值论域固定为无限集合，实例是无 NULL 的有限元组集合。先假定 $m\ge1$ ；空属性集也可按同一规则处理。

建立 $m$ 行、 $|U|$ 列的符号表 $T$ 。每列 $A$ 有一个共同的标记符号 $a_A$ ；第 $i$ 行在 $U_i$ 内的列填 $a_A$ ，其余列填该格私有的新符号 $b_{iA}$ 。不同列的符号组不相交，所有私有符号起初互异。 $a_A$ 表示待检验的拼接元组在 $A$ 列的值， $b_{iA}$ 表示相应见证行尚未被指定的值。两者都是待赋值符号，不是 SQL NULL，也不是预先规定不能合并的数据库常量。

对一条 $L\to M\in F$ ，若两行在 $L$ 的每列上具有相同符号，就要求它们在 $M$ 的每列也相同。对于仍不同的一对右侧符号，在该列全表合并其所有出现。若其中一个是 $a_A$ ，始终以 $a_A$ 为代表；否则按固定编号选一个代表。这称为一次有效合并。不能只修改触发规则的两个单元格而保留别处旧符号，否则同一个符号会被当成两个不同的值。

FD 追赶判据。 反复应用规则直到不存在有效合并。终止表有一行恰为

\boldsymbol a=(a_A:A\in U)

当且仅当 $\mathcal D$ 对 $F$ 无损。这个判据使用原来的全部 $F$ ；它与投影依赖能否局部保持 $F$ 是不同的检查。

一个明确终止的实现

下面每次只做一次有效符号合并，然后从头扫描。这样不需要猜测一轮中哪些后续规则被新等式启用，也不会漏掉先前扫过的行对。

text

T := 按分解初始化的符号表
repeat
    在所有 FD L → M、所有不同行对 i,j 中寻找：
        T[i,L] = T[j,L]，但某个 A ∈ M 满足 T[i,A] ≠ T[j,A]
    if 没有这样的三元组 (FD, 行对, A):
        return T
    按 a_A 优先、否则固定编号的规则选代表
    在 A 列全局替换另一符号为代表

这里所有 FD 与行对都在有限搜索范围内；只有搜索完仍找不到有效合并，才是固定点。若中途已出现全标记行，可以提前回答“无损”，因为后续合并不会破坏它；若要输出终止表，就继续执行上述循环。没有看到成功行时必须真正到固定点，不能任意提前回答“有损”。

直觉

假设有人声称某元组 $u$ 在全部投影的连接中。每个组件都应有一条原表见证行，在这个组件的列上与 $u$ 相同。符号表把这些见证先排列出来：标记格记录已经与 $u$ 对齐的列，私有格保留各见证的其余部分。

FD 逐渐迫使见证之间共享更多值。例如两条见证已经共享 $A$ ， $A\to B$ 就使它们也共享 $B$ 。若最终有一条见证在所有列上都与 $u$ 对齐，就说明 $u$ 本来是原表中的那一行，拼接没有制造新元组。若怎样合并都到不了这一状态，终止表本身可以变成一张合法数据表，让缺少的全标记行成为具体伪元组。

例子与边界

两次合并产生成功行

继续使用

U=ABCD,\qquad F=\{A\to B,\ BC\to A,\ C\to D\}.

对 $\mathcal D_B=\{AB,AC,CD\}$ ，初始表为：

组件	$A$	$B$	$C$	$D$
$AB$	$a_A$	$a_B$	$b_{1C}$	$b_{1D}$
$AC$	$a_A$	$b_{2B}$	$a_C$	$b_{2D}$
$CD$	$b_{3A}$	$b_{3B}$	$a_C$	$a_D$

第一、二行的 $A$ 相同，应用 $A\to B$ ，令 $b_{2B}$ 合并到 $a_B$ 。第二行成为 $(a_A,a_B,a_C,b_{2D})$ 。第二、三行的 $C$ 相同，应用 $C\to D$ ，再把 $b_{2D}$ 合并到 $a_D$ 。得到：

组件	$A$	$B$	$C$	$D$
$AB$	$a_A$	$a_B$	$b_{1C}$	$b_{1D}$
$AC$	$a_A$	$a_B$	$a_C$	$a_D$
$CD$	$b_{3A}$	$b_{3B}$	$a_C$	$a_D$

$AC$ 行已经全标记，所以分解无损。继续检查时，共享 $A$ 的前两行已经共享 $B$ ；共享 $C$ 的后两行已经共享 $D$ ；没有两条不同的行共享 $BC$ ，因此 $BC\to A$ 不产生额外合并。这张表确实也是固定点。

AB、AC、CD 分解中，AC 见证行先借助与 AB 行相同的 A，通过 A 到 B 的依赖合并 B，再借助与 CD 行相同的 C，通过 C 到 D 的依赖合并 D，最终成为全标记行。

图只追踪 $AC$ 这一条见证如何补齐两格；参与触发的 $AB$ 、 $CD$ 行仍属于完整符号表。前页已经证明这套 BCNF 设计不保持 $BC\to A$ ，而这里仍成功证明无损，两者相容。追赶不是用局部检查替代原依赖，而是在假定原表满足全部 $F$ 的前提下传播等式。

有损设计的固定点不能省略

把中间组件换成 $BC$ ，得到 $\mathcal D_L=\{AB,BC,CD\}$ ：

组件	$A$	$B$	$C$	$D$
$AB$	$a_A$	$a_B$	$b_{1C}$	$b_{1D}$
$BC$	$b_{2A}$	$a_B$	$a_C$	$b_{2D}$
$CD$	$b_{3A}$	$b_{3B}$	$a_C$	$a_D$

第二、三行共享 $C$ ，故 $C\to D$ 把 $b_{2D}$ 合并为 $a_D$ 。终止表为：

组件	$A$	$B$	$C$	$D$
$AB$	$a_A$	$a_B$	$b_{1C}$	$b_{1D}$
$BC$	$b_{2A}$	$a_B$	$a_C$	$a_D$
$CD$	$b_{3A}$	$b_{3B}$	$a_C$	$a_D$

现在三行 $A$ 各不相同， $A\to B$ 无法触发；第一、二行虽然共享 $B$ ，却不共享 $C$ ，第二、三行虽然共享 $C$ ，却不共享 $B$ ，因而 $BC\to A$ 也无法触发；共享 $C$ 的两行已经在 $D$ 上相同。全部规则都检查过，确实没有有效合并，而没有任何一行全标记。

把表中不同符号直接解释成互异普通值，三行便组成满足 $F$ 的关系。全标记元组在 $AB$ 投影中由第一行见证，在 $BC$ 投影中由第二行见证，在 $CD$ 投影中由第三行见证，所以它属于连接；它却不在原三行中。这样得到的是满足全部原约束的有损反例。前页另给了一张更小的两行原表并列出四行连接结果，便于手算；这里展示的是算法每次失败都能统一产生的证书。

本页为什么不需要生成新行

FD 只要求已有行之间的一些值相同，所以本算法只做等式合并。若约束要求“每条 $P(x)$ 都应有某条 $Q(x,y)$ ”，就可能需要增加事实与新的见证值；当前终止计数不再适用。合取查询页讨论过这种带约束语义与无约束规范数据库判据的差别。不能把本页的终止性推广为所有 chase 都终止，也不能直接用本表格判据决定任意约束下的查询包含。

推论与应用

终止、不变量与成本

初始化至多有 $mn$ 个实际出现的符号，其中 $n=|U|$ 。每次有效合并使符号等价类数严格减少，不增加任何行、列或符号，所以合并次数少于 $mn$ （零属性时直接终止）。标记符号永远优先保留，因此组件行原来具有的标记格永远保持标记，已经全标记的行也不会退化。这两个不变量分别支持失败反例中的投影见证与成功时的提前停止。

令 $\ell=1+\sum_{L\to M\in F}(|L|+|M|)$ 。用直接存储符号编号的数组实现，一轮寻找有效合并需要 $O(m^2\ell)$ 次基本操作；保守地扫描整表完成一次全局替换，耗时 $O(mn)$ 。故总时间有简单多项式上界

O\bigl((mn+1)m^2\ell+(mn)^2+mn\bigr),

存储为 $O(mn+\ell)$ 个属性或符号编号。这里按编号比较、替换的单位成本计数；若计比特，还需相应的编号位长。更好的索引或并查集实现可以减少重复扫描，本页的正确性不依赖这些优化。

全标记行为什么证明所有合法实例无损

取任意 $r\models F$ ，以及任意 $u\in\bowtie_i\pi_{U_i}(r)$ 。对每个组件 $U_i$ 选一个见证 $t_i\in r$ ，满足 $t_i[U_i]=u[U_i]$ 。给初始表赋值： $a_A$ 取 $u[A]$ ，私有 $b_{iA}$ 取 $t_i[A]$ 。同一个标记符号在不同组件出现时，其值都是同一个 $u[A]$ ，所以这是一份一致的赋值，而且第 $i$ 行恰解释为原表的见证 $t_i$ 。

归纳考虑一次规则触发。触发的两行在左侧使用相同符号，因而其见证在左侧取值相同。原关系满足这条 FD，所以右侧待合并符号的赋值也相同。合并并全局替换后，赋值仍一致，每行仍解释为原来的 $t_i$ 。这是追赶的见证赋值不变量。

若某行最终全标记，该行的见证 $t_i$ 在每列都取 $u[A]$ ，因此 $t_i=u$ ，从而 $u\in r$ 。于是连接结果包含于原表；与始终成立的反向包含结合，得到无损。证明使用任意 $r,u$ ，所以并非只检查了一张示例数据库。

没有全标记行为什么一定有合法反例

设已经达到固定点且没有全标记行。利用无限论域，为最终不同的符号选择互异普通值，解释各行得到有限关系 $r_T$ ；重复的行按集合语义合并即可。若 $r_T$ 中两行在某条 FD 的左侧相同，由于不同符号取不同值，它们在符号表左侧也逐格相同。固定点意味着右侧已逐格相同，否则还可有效合并。因此 $r_T\models F$ 。

每个组件对应的那一行始终保留该组件中的全部标记格，所以全标记元组 $\boldsymbol a$ 的 $U_i$ 投影属于 $\pi_{U_i}(r_T)$ 。这对所有组件成立，故 $\boldsymbol a\in\bowtie_i\pi_{U_i}(r_T)$ 。但终止表没有全标记行，且不同符号解释为不同值，所以 $\boldsymbol a\notin r_T$ 。这就是合法有限反例，证明分解有损，也完成判据的另一个方向。

这种证明与合取查询的规范数据库思路相通：把符号对象冻结成具体有限实例，以一次见证或一次失败承载全实例命题。区别是原始表未必满足 FD，必须先追赶到满足约束的固定点，再把它当作反例。规则应用顺序可以改变中间表和私有代表名称，但上述两个方向保证：任何真正到固定点的执行都给出同一个无损判定。

参考资料

Serge Abiteboul、Richard Hull、Victor Vianu，Foundations of Databases，作者官方在线稿第 8 章，§8.4，FD rule（印刷页 175）、Lemma 8.4.4（页 176）、连接依赖符号表及 Theorem 8.4.12(b)（页 181）：依赖合并、终止性与连接依赖的追赶判据。
DePaul University，Relational Design Theory II，CSC355 Spring 2014，PDF 第 5 页：用全标记行检验多元分解。本页补全见证赋值和终止表反模型两个证明方向。
David Maier、Alberto O. Mendelzon、Yehoshua Sagiv，Testing Implications of Data Dependencies，ACM Transactions on Database Systems 4(4)，1979，pp. 455–469。此链接为官方论文记录，用于追赶方法的历史出处；本页精确定理与证明依照上述可读教材，不引用未核验的原论文定理编号。

形式陈述 ​

从分解构造符号表 ​

一个明确终止的实现 ​

两次合并产生成功行 ​

有损设计的固定点不能省略 ​

本页为什么不需要生成新行 ​

终止、不变量与成本 ​

全标记行为什么证明所有合法实例无损 ​

没有全标记行为什么一定有合法反例 ​

反向链接