Datalog 与有限最小不动点

非递归合取查询只对现有表做一次匹配。Datalog 允许把刚得到的答案放回规则体，再为后续匹配提供见证。例如先知道 $a$ 能到 $b$，又知道 $b$ 有一条边到 $c$，便把“$a$ 能到 $c$”存成新事实；下一轮可以继续使用它。

最小性排除了凭空添加的结论。规则 $R(x)\leftarrow R(x)$ 允许任意 $R$ 成为闭合关系，但空输入时最小答案仍为空：循环引用本身没有提供证据。每个实际推导出的事实都有一棵有限证明树，叶子来自输入或空体规则，内部节点是一条规则的成功应用。按轮数和树高分别归纳，就能在迭代语义与有限证明树之间来回转换。

终止也不依赖图是否有环。环能提供无限多条游走，却只能反复证明有限个有序节点对。关系按集合存储，重复证明不会增加新的事实；算法计算的是哪些事实成立，而不是共有多少条证明。

四条边推出九个可达对 ​

令 $E=\{(a,b),(b,c),(c,b),(c,d)\}$，定义

$E$ 是固定 EDB，$R$ 是唯一 IDB。用 $ab$ 简写 $(a,b)$，令 ${\mathrm{\Delta }}_i=R_i\setminus R_{i-1}$。从 $R_0=\varnothing$ 开始，完整计算为：

| 轮次 $i$ | 新事实 ${\mathrm{\Delta }}_i$ | 累计 $|R_i|$ | |---|---|---😐 | 1 | $ab,bc,cb,cd$ | 4 | | 2 | $ac,bb,bd,cc$ | 8 | | 3 | $ad$ | 9 | | 4 | $\varnothing$ | 9 |

第二轮的四条见证依次是 $a\to b\to c$、$b\to c\to b$、$b\to c\to d$、$c\to b\to c$。第三轮把 $ac$ 接到 $cd$ 得到 $ad$；把 $ac$ 接到 $cb$ 只重新得到 $ab$，其余延伸也已出现。第四轮唯一待延伸的新对以 $d$ 结束，而 $d$ 没有出边，因此停止。最终答案恰为

归纳可得，$R_i$ 包含且仅包含长度在 $1$ 到 $i$ 之间的游走端点对。正向由每次只追加一条边得到；反向把长度至少为二的游走拆成前缀与最后一条边。因此稳定结果是正长度可达关系。$bb,cc$ 来自环；没有 $aa,dd$。若需要反身传递闭包，应提供节点关系并增加 $R(x,x)\leftarrow \mathsf{Node}(x)$。孤立节点尤其需要显式列入 $\mathsf{Node}$，仅有边表无法表达它存在。

线性递归的半朴素求值 ​

定义关系连接 $S\circ T=\{(x,z):\mathrm{\exists }y(x,y)\in S,(y,z)\in T\}$，这里明确按“先 $S$ 后 $T$”的次序使用符号。朴素迭代反复计算 $R_i\circ E$，其中旧事实与 $E$ 的连接已经做过。初始化 $R_1={\mathrm{\Delta }}_1=E$，以后只计算

它与朴素算法逐轮相同。因为 $R_i=R_{i-1}\cup {\mathrm{\Delta }}_i$，连接分配为旧连接与增量连接，而 $R_{i-1}\circ E\subseteq R_i$：旧连接结果上一轮已加入。减去 $R_i$ 后，只剩增量连接可能贡献新事实。对 $i=1$，$R_0=\varnothing$ 同样成立，于是归纳建立每轮相等。

去重仍然必要。新输入事实可以产生旧输出，也可以有多个新见证产生同一输出；上例的 $ac\circ cb$ 就再次产生 $ab$。半朴素求值减少重复的规则匹配，不承诺每个程序、每种索引和输入规模都得到相同比例的加速。

非线性递归需要旧、新交叉项 ​

若把递归规则改成 $R(x,z)\leftarrow R(x,y),R(y,z)$，体中出现两个递归关系，不能只算 ${\mathrm{\Delta }}_i\circ {\mathrm{\Delta }}_i$。保留种子规则 $R\leftarrow E$，初始化仍为 $R_1={\mathrm{\Delta }}_1=E$。正确增量为

证明先按两个体原子的来源展开 $R_i\circ R_i$。旧—旧项已经包含于 $R_i$；剩下新—旧、旧—新、新—新三项。公式的第一项覆盖新—旧，第二项同时覆盖旧—新与新—新，因而没有遗漏。这是一般半朴素方法的要点：每个尚未处理的成功匹配至少使用一个新增体事实，不要求全部体事实都新增。

在链 $1\to 2\to 3\to 4\to 5$ 上，第一轮是四条边，第二轮新增 $13,24,35$。第三轮正确新增 $14,25,15$；若只连接两个第二轮增量，只能得到 $15$，漏掉长度三的 $14,25$。下一轮错误算法的增量只有 $15$，也无法补回遗漏。这同时说明非线性程序的轮次不再对应“每轮多一条边”：它可以把两段已知游走直接拼接。

哪些扩展改变证明 ​

加入否定后，增大 $X$ 可能使原本成立的规则体失效。例如 $P(x)\leftarrow \mathsf{Node}(x),\mathrm{\neg }Q(x)$ 在加入 $Q(a)$ 后不再支持 $P(a)$，所以原来的单调性论证失效；仅靠保留旧事实也不能解释预期的否定语义。分层否定需要另行规定计算次序与语义。

函数项、生成新值的算术、存在量化的头变量会破坏固定有限事实空间。比如允许 $R(f(x))\leftarrow R(x)$ 后，从 $R(a)$ 可生成无限项。本文的有限终止论证因此不能直接覆盖这类语言、一般事实生成 chase、聚合或含 NULL 与重复行的 SQL。

为什么稳定值恰是最小模型 ​

先证单调性：若 $X\subseteq Y$，每个在 $I\cup X$ 中成功的正体匹配，在 $I\cup Y$ 中仍成功，所以 $C_P(I,X)\subseteq C_P(I,Y)$，继而 $F(X)\subseteq F(Y)$。加上 $X\subseteq F(X)$，迭代是一条有限升链，必定稳定。

稳定时 $C_P(I,X_{\ast })\subseteq X_{\ast }$，意味着所有成功匹配的规则头已经存在，所以 $I\cup X_{\ast }$ 满足每一条规则。为证最小性，任取另一个规则闭合扩展 $M$。初值 $X_0=\varnothing \subseteq M$；若 $X_i\subseteq M$，由单调性与闭合性得到

归纳给出 $X_{\ast }\subseteq M$。这证明的是所有模型共同包含的最少事实，而不仅是某次运行恰好停住。也可把整个过程放入Knaster–Tarski 不动点定理公理库Knaster–Tarski 不动点定理Knaster-Tarski fixed-point theorem · Tarski fixed-point theorem完备格上的单调自映射之全部不动点构成完备格，并具有规范的最小与最大不动点。：$\mathcal{P}(\mathcal{B})$ 是有限完备格，$F$ 是单调映射；本页的有限归纳进一步给出可执行的终止理由。

关系运算与复杂度 ​

每条正规则可用关系代数公理库关系代数Relational algebra · Set relational algebra用选择、投影、积、重命名与集合运算组合有限关系查询，并在集合语义下解释连接和存在见证。中的重命名、选择、连接与投影实现，多条同头规则取并。递归所增加的是重复执行直到闭合的控制机制；这些单轮运算本身仍是有限表运算。半朴素算法中的差集只用于排除已知输出，不是在规则语言中加入语义否定。

设程序固定，最多有 $v$ 个变量出现在一条规则中，令 $n=|A|=|\mathrm{adom}(I)\cup \mathrm{Const}(P)|$，并写 $N=max(1,n)$。一轮至多枚举 $O(N^v)$ 个赋值；固定程序使每次需检查的体原子数为常数。用可常数时间查询成员的关系表，最多 $H+1$ 轮可得 $O(|I|+(H+1)N^v)$ 的直接上界。这里 $H=\sum _R{n}^{\mathrm{arity}(R)}$；元数、符号数与程序常量数均固定，加入程序常量只使输入活跃域大小增加一个有界量，所以这仍是输入规模的多项式。若用顺序扫描，仍是多项式，只是次数更高。它是透明的终止与复杂度上界，并非推荐的物理执行计划。

标准事实成员判定中，正 Datalog 的数据复杂度是 P 完全，含义是每个固定程序都可多项式求值，且存在固定程序达到 P 难；不表示每个程序都 P 难，上面的普通有向可达性就是更受限的任务。若程序也随输入增长，变量数和元数不再是常数，联合复杂度是 EXPTIME 完全。这两个完备性下界使用相应归约，超出了前述枚举上界的证明；可参见 Oxford Lecture 7，第 12–21 张幻灯片。