“若输入后来删除一条边，可以对生成后的整个正程序使用删除与重推。必须一起维护需求和答案关系：某个请求可能只因一条后来被删的路径才存在，不能把旧 M 表永远冻结。查询种子、规则或绑定值改变则是另…”
形式陈述
删除一个输入事实会影响哪些结论
一张已经算好的可达关系中，a 能到 d，可能同时因为 a→b→c→d 和 a→e→d。删掉 a→b 后，第一条理由失效，结论却仍应存在。另一方面，a 能到 b 与 a 能到 c 可能互相引用；若只检查“它还有没有一条当前看起来成立的理由”，这两个错误结论可能彼此作保，永远不被删除。
删除与重推，简称 DRed，处理的是有限正 Datalog的物化维护。输入包括固定程序 P、旧 EDB 集合 I、已经精确等于 P 在 I 上最小模型之 IDB 部分的 J，以及要删除和插入的 EDB 事实集合 D₀、A₀。程序安全、无函数、无否定、无聚合，EDB 与规则头分离，关系采用集合语义。允许递归、重复变量、常量事实和零元关系。
精确旧物化是前置条件，而非此算法的输出验证。参考器检查事实的谓词、元数和常量类型，但不会为验证 J 而偷偷全量重算；若调用方把一个错误的旧 J 传进来，本页的正确性结论不适用。规则、查询种子或模式改变，也不属于这项 EDB 更新接口。
本页把同一批中的删除与插入解释为先删除、后插入：
算法先规范化成实际变化 D⁻ 与 A⁺。删除原本不存在的事实不产生变化，插入已有事实不产生副本；同一旧事实同时列在删除与插入中，最后仍存在，因此这次净变化为空。输出为新 EDB I′ 与准确的新 IDB J′，并交出每轮过删、重推和新增的事实集合。
第一步：沿旧证明作保守过删
把一条规则的所有变量替换成常量，得到地面规则实例。参考器枚举在旧集合 I∪J 中体原子全部成立的实例，并保存其头事实和完整体事实列表。这里的“旧”很重要：后续过删不能因为已经移走了一部分事实，就再也看不到它们曾支持哪些结论。
令待删集合 D 起初为实际删除的 EDB 事实 D⁻。只要一个旧成功实例的任一体事实进入 D，就把它的头也加入 D，直到不再增加。即使这个头另有一条完全未受影响的证明，仍然先删；该阶段宁可多删，不会在这里证明替代支持是否可靠。
参考器建立从体事实到实例头的反向索引。每轮只扩展刚进入 D 的事实，每个事实第一次加入后才进入队列。保存的过删 IDB 为 D∩J；暂时保留的全集是 S=(I∪J)\D。它已移除所有实际删除的 EDB，但尚未加入 A⁺。
第二步：从幸存事实重新长出结论
现在只考虑那些头属于 D∩J 的旧成功实例。若实例的全部体事实都已在当前 S 中，就重新加入其头。以批次反复执行，直到没有新增。重新加入的事实又能支持下一轮，但仍在 D 中、尚未重推出来的事实不能被当成证据。
这一步能够恢复被过删的正确结论，同时排除纯循环自我支持。若 P(a) 只能靠 Q(a)，Q(a) 又只能靠 P(a)，而二者都已被过删，那么空的起点不会使任意一个首先出现。若还有幸存 E(a) 能推出 P(a)，则 P(a) 先恢复，下一轮 Q(a) 才有真实证据。
这里重用旧实例是充分的，因为仅删除 EDB 时，新最小模型包含在旧最小模型中；每个新有效证明使用的规则实例原本也成功。重推空体常量事实不需要任何体证据。若这样的事实因另一个受损证明被过删，空体实例会把它恢复。
第三步：加入新的 EDB 并向前传播
删除与重推稳定后，再把 A⁺ 加入当前集合。以 A⁺ 为第一批增量，反复寻找至少含一个本轮新增体事实的成功实例，把尚未存在的头加入下一批。非线性规则中的两个体原子都可能新增，必须允许这样的实例；集合去重负责消除同一头的多次发现。
新增阶段需要在更新后的关系上重新匹配规则，不能只遍历旧实例。新插入的 EDB 可以带来以前未出现的常量，也可能让从前失败的连接第一次成功。这里直接使用既有 Datalog 增量原则，不要求为新常量预先列出旧地面空间。
直觉
过删阶段问：“这条结论有没有碰到过一个坏掉的理由？”只要有，就先撤回。重推阶段换一个问题：“从目前真正站得住的事实出发，能不能重新证明它？”前一个问题容易沿依赖传播，后一个问题从可靠起点求最小不动点，二者合起来避免维护所有证明树。
把一个结论的不同理由看成两张收据，会帮助理解替代支持；但不能简单数一数递归关系中有几张收据。收据可能互相引用，没有任何输入事实垫底。最小模型要求存在有限、落到输入或空体事实上的证明，不能仅满足“每个结论都有另一结论支持”的闭环。
例子与边界
替代路径会被过删，再被正确恢复
沿用正长度可达性规则 R(X,Y)←E(X,Y) 与 R(X,Z)←R(X,Y),R(Y,Z)。输入边是 a→b、b→c、c→b、c→d、a→e、e→d，以及独立的 u→v→w→u。旧 R 有20个元组，a 行为 b、c、d、e。
删除的是输入事实 E(a,b)，不是手动删除 IDB 的 R(a,b)，也不是仅撤回某一棵证明树。过删前沿依次为 {E(a,b)}、{R(a,b)}、{R(a,c),R(a,d)}。第三批中的 R(a,d) 虽有 a→e→d 这条替代路径，也先被移走。
幸存集合里仍有 R(a,e) 与 R(e,d)，因此重推的第一批为 {R(a,d)}，下一批为空。R(a,b) 与 R(a,c) 不会恢复；最终 R 有18个元组，a 行只剩 d、e。独立的 u、v、w 分量从未进入过删前沿。
错误的“反复剥掉没有任何支持的旧结论”会留下 R(a,b) 和 R(a,c)。它看到 R(a,b) 可由 R(a,c)、R(c,b) 支持，R(a,c) 又可由 R(a,b)、R(b,c) 支持，于是认为二者都没问题。但删除 a→b 后，从 a 已经走不到这个环；这两条理由没有有限的有效起点。
对查询改写程序，需求表也必须一起维护
对魔集改写后的同一查询 R(a,Y)，把答案关系写成 Q、需求关系写成 M。旧 IDB 有11条 Q 与5条 M。删除 E(a,b) 后，过删不只涉及 a 行答案，也会沿需求传播规则撤销 M(b)、M(c)、M(d)，再撤销由它们支撑的 Q 行。
实际过删 IDB 是9条 Q 与3条 M，共12条。暂时幸存的 IDB 只有 M(a)、M(e)、Q(a,e)、Q(e,d)。重推第一批恢复 Q(a,d) 与 M(d)，随后稳定；最终6条 IDB 中，查询答案为 (a,d)、(a,e)。M(d) 虽不产生新的出边答案，仍是生成程序的真实结论，不能因为当前读者不关心它就漏报。
这种维护针对生成程序的整个最小模型。冻结旧需求表会保留不再有依据的请求，即使这一次的 a 行恰巧正确，内部物化也已不符合接口；把旧 Q 当成永久缓存则更可能直接返回失效答案。终点会同时比较全部生成 IDB 和原查询答案。
空集合、新常量与循环的边界
若实际删除与插入都为空，返回旧物化即可；但输入规范化和类型检查仍有成本。若程序、EDB 和 IDB 都为空，结果为空。若存在零元事实 Ready()←，它在没有任何输入常量时也应成立，不能因活跃域为空就丢掉这个空元组。
插入 E(d,fresh) 和 E(fresh,a) 引入新值 fresh，新增阶段必须允许它参与新证明。若只缓存旧常量上的成功实例，更新会漏答。参考器每次匹配当前关系，因此不依赖旧活跃域封闭这一错误假设。
本算法维护集合事实。若业务把同一输入行存成两个可独立删除的副本，删除其中一个副本不能直接翻译成删除该 EDB 集合事实；应先在接口外决定其集合存在性是否真的变化。规则删除、否定、聚合和 SQL 袋语义同样需要额外机制，本页不把它们隐含纳入保证。
推论与应用
为什么最终得到最小模型
先只看删除。由于正程序的单调性，删除后的最小模型 L⁻ 包含在旧最小模型 L 中。任何在 L 中有有限证明、但该证明含被删 EDB 叶子的头，都会沿旧实例的任一受损体传播进入 D。因此，一个未进入 D 的旧事实可以保留它原来的有限证明：其中不可能有被删叶子，否则根也会被过删。故幸存 S 中每个事实都属于 L⁻。
重推只在当前已证真事实之上应用原规则，所以始终保持 S⊆L⁻。为证不漏，取 L⁻ 中一个事实的有限证明树，对树高归纳。叶子是幸存 EDB 或空体事实；对于内部节点，子事实都将由归纳成为当前事实。这个节点若原来未被过删，已经存在；若被过删，相应的旧成功实例终会在一次扫描中发现全部体已成立，把它恢复。于是稳定后的集合恰为 L⁻。
加入 A⁺ 后，起点 L⁻∪A⁺ 已在完整新最小模型 L′ 中，所以向前推导仍不多答。新增加的每个结论若尚不在 L⁻，其证明树必有一条从新 EDB 叶子向上的变化路径；按推导轮数看，一个首次可成功的实例至少有一个体事实刚加入。增量传播因此不会漏掉需要重新触发的实例，最终得到 L′。
终止性来自有限事实空间和单调集合增长。过删集合只增加旧事实，重推只恢复有限的过删 IDB，新增只增加由固定规则、输入常量和新插入常量组成的有限地面事实。循环可以造成多轮传播，却不能重复入队同一个事实而无限增长。
哪些成本真正按变化量计算
先把枚举旧成功实例的实际匹配成本记为 Cₒ，旧事实总数记为 M，成功实例数记为 G，实例体长度总和记为 B。参考器先保存全部这些实例和体事实反向索引，因此不是一个只读更新批次的算法。实例建立之后，队列过删的时间和额外存储可界为 O(M+G+B+1)：每个被删事实只扩展一次，每个相应的反向索引项至多读一次。
参考器的重推部分为易读采用全实例逐轮扫描。若过删 IDB 数为 d，至多 d 个非空轮次加一个终止轮，成本为 O((d+1)(G+B+1))，另加已有集合存储。可以实现更精细的候选索引，但不能把该优化的界安到这份代码上。主例原程序枚举55个旧成功实例，重推实际测试14个体事实成员关系；生成程序枚举37个旧实例，测试79次。后两项只是短路检查的计数，不包含跳过已恢复头、扫描实例或集合构造的全部成本。
新增阶段的成本应计入所有重新匹配和候选体的检查，不能笼统写成 O(|A⁺|)。参考器每次匹配还重建并排序当前关系索引；连接的中间结果可能远大于新增事实数。若要完整计费，可把各次匹配的实际成本求和，再加各候选体的增量成员检查及新事实去重。峰值存储除 M+G+B 外，还包括当次匹配的中间环境、当前新物化与保存的轨迹。
这些界把固定大小事实的比较、哈希和集合操作按通常单位成本计算；长字符串处理、大对象拷贝和 JSON 展示另计。参考器在零变化时仍遍历输入做验证，并生成返回集合；该分支没有枚举旧实例，也不意味着总成本为零。DRed 的优势是提供正确的增量结构，不是保证每次更新都比全量重算便宜。
可执行终点同时交出正常程序与生成程序的实际前沿，运行故意错误的循环支持版本，再以独立的有限地面枚举全量重算作对照。只有最终查询正确还不够：过删、重推和整个新物化都应能解释。
参考资料
- Ashish Gupta、Inderpal Singh Mumick、V. S. Subrahmanian，Maintaining Views Incrementally，SIGMOD1993，§7，印刷页164–165：DRed 的过删、重推、新增三阶段及正确性定理；§1说明撤销一个推导并不等于删除仍有其他支持的事实。本页给出正集合程序的具体队列与全实例扫描变体，并明确其实现成本