依赖追赶与通用模型

TGD 写下的是一项存在义务：“这名学生必须有导师”，却没有告诉我们导师是谁。空值给这个尚未命名的见证留一个可复用的位置。若已有合适导师，就没有未完成的义务，限制追赶不会再造一个。

EGD 传递另一种信息：“这两个位置其实必须是同一个对象。”它可以把新建的见证合并，也可以把占位符确定为已有常量；如果业务数据已经把二者指定为两个互异常量，等式便无从满足。

通用模型把尚未决定的身份保留为可映射的空值。无论真实补全怎样选择导师，追赶中的占位符都能映到相应见证。合取查询只要求找到一组正事实，因此这组匹配可以随同态一起送到每个补全中。这是确定答案成立的原因。

两个见证、一次合并、一个结论 ​

从唯一事实 $I=\{\mathsf{Student}(a)\}$ 开始，取四条依赖：

沿以下顺序执行，恰有四次有效步骤：

第二步仍活跃，因为 Advisor 的事实不能充当 Supervisor 的头见证。第二步结束时，${\sigma }_3$ 还不能匹配：它的同一个变量 $u$ 无法同时取两个不同符号。第三步合并后，这个共享变量的匹配才出现。

最终得到

逐条检查停止条件：Student 只有 $a$，${\sigma }_1,{\sigma }_2$ 都已有头见证；$\epsilon$ 的唯一体匹配在两端取同一符号；${\sigma }_3$ 的唯一体匹配已有 Ready 事实。没有规则生成新的 Student，因此确实不存在其他活跃触发。

查询

在 $C$ 上的答案恰为 $\{a\}$，故 $a$ 是确定答案。若改问 $p(u)=\mathsf{Advisor}(a,u)$，符号求值返回 ${\nu }_1$，却不能把它当成已知导师身份：取两个新常量 $b,c$，分别用 $b$、$c$ 替换 ${\nu }_1$ 就得到两个合法补全，它们没有共同的导师常量答案。

失败是常量冲突 ​

若输入另含 $\mathsf{Advisor}(a,b)$ 和 $\mathsf{Supervisor}(a,c)$，其中 $b,c$ 为互异常量，$\epsilon$ 立即要求 $b=c$，追赶失败。不存在既保留这些事实、又满足全部依赖的补全。算法没有授权删除事实或把两个既定常量改名，因此这不是自动数据修复；应用应报告约束不一致，而不是把逻辑上空量化的“所有答案”当成有用结果。

每一步有限仍可能永远生成 ​

取单条 TGD

及输入 $\{\mathsf{R}(a,b)\}$，其中 $a\ne b$。当前末端没有后继，限制追赶依次加入

每个新末端又产生一个活跃触发，所以这条执行不终止。但 $\{\mathsf{R}(a,b),\mathsf{R}(b,a)\}$ 已是有限合法补全：两个体匹配分别以 $a,b$ 为下一步见证。新空值策略不会主动猜测把末端接回 $a$；存在有限模型不保证限制追赶停止。不终止也不证明约束矛盾，或某个查询答案为假。

Datalog 与有限最小不动点公理库Datalog 与有限最小不动点Datalog · Positive Datalog · Datalog least model在固定有限活跃域上反复应用正规则，证明所得关系是最小模型，并用有环可达性逐轮推导半朴素求值。依靠固定有限活跃域限制可生成的事实数；这里不断出现新见证，该计数失效。函数依赖的追赶检验公理库函数依赖的追赶检验FD chase · Lossless join chase test在固定符号表中全局合并被函数依赖强制相等的值，以全标记行证明无损，以终止表构造合法有损反例。则只合并固定符号表中的值，每次减少等价类数，因而有另一个终止理由。两者都不能替一般存在依赖提供终止界。

同态不变量：每一步都能在真实补全中解释 ​

任取满足 $I,\mathrm{\Sigma }$ 的补全 $M$。证明每个当前实例 $K_i$ 都有保持常量的同态 $f_i:K_i\to M$。初始 $K_0=I$，取输入常量的恒等映射即可，因为 $I\subseteq M$。

若下一步执行 TGD，体匹配为 $h$，则 $f_i\circ h$ 在 $M$ 中满足体。由于 $M$ 满足该依赖，存在一组值共同满足整个头。把本步每个新空值映到对应见证，保留全部旧符号的像，就得到 $f_{i+1}$。新空值从未使用，故没有旧赋值需要被改写；同一存在变量的全部头位置也使用同一见证。

若下一步执行 EGD，设被合并的符号为 $s,t$。$M$ 中相应体匹配必须满足等式，所以 $f_i(s)=f_i(t)$。令 $\pi :K_i\to K_{i+1}$ 表示全局替换映射，便可在合并后的代表上定义同一个像，使

每条替换后的事实仍映成原来的 $M$ 事实，因此 $f_{i+1}$ 仍是同态。若 $s,t$ 是不同常量，保持常量要求它们映到两个不同值，与上述等式矛盾。这证明：一旦执行失败，根本不存在这样的补全 $M$。

注意 EGD 步前后的事实集合不必按原符号构成包含链；不变量沿替换映射传递，不能把各阶段的原始事实简单并起来代替这个论证。

成功固定点为什么通用 ​

若有限执行成功返回 $C$，对其中任意 TGD 体匹配，停止条件保证存在整组头见证；对任意 EGD 体匹配，两端已经相同。因此 $C\models \mathrm{\Sigma }$。输入只含普通常量，合并不会改变它们，故 $I\subseteq C$。

上一节的不变量对任意允许补全 $M$ 都成立，取最后一步就得到 $C\to M$，完成通用性证明。不同成功运行即使生成不同数目的空值，也都是合法补全，因此相互存在保持常量的同态；这保证它们对纯合取查询给出相同的常量答案，不要求实例同构或事实数最少。

确定答案的两个方向 ​

若 $\overline{a}\in q(C)$，取产生答案的查询匹配 $g$。任意补全 $M$ 都有 $f:C\to M$，复合 $f\circ g$ 将查询的每个原子映成 $M$ 的事实。由于输出元组 $\overline{a}$ 只含常量，$f(\overline{a})=\overline{a}$，故 $\overline{a}\in q(M)$。这证明在 $C$ 上找到常量答案足以保证所有补全都返回它。

反过来，若所有补全都返回 $\overline{a}$，那么 $C$ 本身就是可选补全，也必须返回它。若要求数据库事实里不出现空值符号，就把 $C$ 的不同空值一一解释为互异的新数据值，避开输入、依赖、查询及 $\overline{a}$ 的常量。这是改名后的有限模型，保持全部原子匹配和等式；若 $\overline{a}\notin q(C)$，它便是一份不返回 $\overline{a}$ 的合法反例。因此有限成功时，同一判据对“所有补全”和“所有有限补全”均成立；这个结论来自手中已有的有限通用实例，不推广到尚未成功结束的执行。

正原子匹配能沿同态传递是证明的关键。否定与不等式不具备同一保证：目标模型可以多出事实，同态也可以把不同空值合并。因此不能把这条确定答案判据原样用于带否定或不等式的查询。

单步成本与总运行时间 ​

固定模式和有限规则集。令当前实例有 $n$ 个符号，$N=max(1,n)$；每条规则至多有 $v$ 个体变量、$e$ 个存在变量。枚举体匹配至多需要 $N^v$ 次候选检查。对每个 TGD 匹配，枚举已有符号对存在变量的赋值至多需要 $N^e$ 次，即可检查是否已有共同头见证。每个存在变量都出现在头原子中，所以成功的已有见证必定出现在当前事实中；不必搜索未知的外部值。

在事实成员查询为单位成本、规则固定的实现下，一次完整活跃性搜索有 $O(N^{v+e})$ 的保守上界；EGD 不需要存在变量枚举。扫描全部事实完成一次全局合并并去重，也只有当前存储规模的多项式成本。用顺序扫描检查成员会提高次数，仍是当前实例规模的多项式。

这些都是当前一步的成本。新事实和空值可能使 $n$ 无界增长，有效步骤数也可能无限，所以它们不构成整个追赶的多项式时间保证。本文证明的可用终点是有限成功后的通用模型与确定答案；对一般输入，不能把这段循环当成保证返回的判定程序。