# Maintaining a Fixed Point: Datalog, Retractions, and Incremental State Codex (AI) | English analytical review | Local draft v1 | 2026-10-25 ## Abstract Incremental Datalog maintains recursive consequences while input facts change, but deletions expose a gap between local support and the least fixed point intended by the query. This analytical review separates query semantics, multiplicity, incremental algebra, and completion of logical versions. Six primary sources cover finite Datalog, recursive materialization maintenance, differential and timely dataflow, DBSP, and multiplicity-preserving operators. The central argument is that a correct maintained result must equal fresh evaluation at a declared completed version, even when internal state contains negative weights, alternative derivations, or provisional output. Two reproducible graph illustrations show surviving support in a diamond and quadratic output retraction after a single chain-edge deletion. An additional unsupported-cycle example refutes naive local support counting, while a finite signed-arithmetic check verifies the interaction term in a bilinear delta identity. All numerical outputs are constructed and deterministic; no database benchmark was measured. The proposed evaluation protocol compares completed versions against an independent traversal oracle and reports retained state, provisional differences, and output size alongside latency. Explicit limits exclude arbitrary negation, nontermination, distributed recovery, and claims that one maintenance strategy is uniformly superior. ## A result is a maintained mathematical object A recursive query asks for a fixed point, while a continuously updated system must keep that fixed point aligned with changing input. These are related but distinct obligations. Computing reachability once does not explain what should happen after an edge is removed, and accepting a negative update does not prove that all consequences of the removal have been repaired. The useful correctness target is equivalence to a fresh evaluation at a declared logical version. The Souffle tutorial presents pure Datalog over a finite universe and illustrates reachability with base and recursive rules. It also warns that arithmetic functors can make programs nonterminating. We therefore restrict the executable examples to finite directed graphs and positive reachability rules. This restriction makes the least fixed point unambiguous and exhaustively checkable. The manuscript argues that incremental correctness depends on three boundaries: the semantics of multiplicity, the handling of cyclic support, and the point at which a version is complete enough to expose. Two constructed graph models show why deletions and output size defeat simple intuitions about small updates. The results are exact counts for synthetic graphs. They are neither performance claims about a Datalog engine nor a proof that one maintenance algorithm dominates another across workloads. Sources: cs2-08-1 ## The least fixed point needs a starting state For finite positive reachability, start with the empty derived relation and repeatedly add base edges and consequences of existing reachability. Because the set of possible pairs is finite and the operator is monotone, this process stabilizes. The starting point matters: an arbitrary self-supporting fixed point need not equal the least fixed point. In the accompanying model, a graph traversal oracle independently computes reachable pairs and checks the rule-based iteration on every loop-free directed graph over three vertices. The phrase loop-free directed graph here excludes self-edges, not directed cycles: two vertices may still point to each other. This detail is necessary because cyclic support is central to the deletion counterexample. Paths have positive length, so a vertex reaches itself only when there is a directed cycle. Reflexive closure would be a different query and would change expected counts. The test contract fixes this choice before enumeration. It also fixes set semantics: multiple proofs of a pair do not create multiple output pairs. These definitions may sound elementary, but they are exactly the assumptions that disappear when a materialized relation is treated as an ordinary mutable table. A correct incremental implementation must preserve the query's denotation after every committed input change, not simply preserve the shape of its stored records. Author analysis or proposed verification. ## Why deleting one proof is insufficient Motik and colleagues compare counting, Delete/Rederive, and a Forward/Backward/Forward approach, including recursive rules and stratified negation. The inspected abstract explains that multiple derivations and recursive support create different tradeoffs for these families. It reports new maintenance algorithms and an empirical evaluation, but this manuscript does not reproduce that evaluation or infer an overall winner. A small counterexample explains the issue without implementing those algorithms. Let a base fact establish p(a), with rules deriving q(a) from p(a) and p(a) from q(a). Before deletion, both derived facts hold. Remove the only base fact. A naive support counter initialized from the previous materialization may retain p(a) because q(a) supports it, and retain q(a) because p(a) supports it. Yet a fresh evaluation from the empty relation derives neither fact. The cycle is a fixed point but not the least one. This demonstrates failure of that naive counting scheme, not failure of every algorithm that uses counts. Sophisticated counting methods distinguish support classes or combine counting with additional reasoning. The implementation lesson is to identify whether a stored number counts independent extensional support, rule firings, derivation trees, or something else. Those quantities are not interchangeable in recursive programs. Sources: cs2-08-2 ## Differences carry more than a sign Differential dataflow generalizes incremental computation using partially ordered versions and indexed updates, allowing work to be reused across input changes and iterations. The original paper's introduction explains this multidimensional view and distinguishes it from a single sequence that continually discards older updates. The supported claim is about its computational model; the selected reading does not establish the performance of a current library release. A negative weight is consequently not a universal deletion command detached from time and algebra. Its effect depends on which collection, version, and combination rule it belongs to. An insertion followed by its inverse at the same relevant version can cancel, while the same numerical weights attached to distinct times may need to remain distinguishable for future queries or compaction. The same caution applies to output: the consumer must know whether a record is a replacement, an additive difference, or a retraction of earlier visibility. Our finite graph examples deliberately collapse each committed version to a set and recompute a reference result. This makes them suitable as correctness oracles but poor models of internal differential state. A realistic memory study must include indexed historical differences, not only the final number of reachable pairs. The benefit of incremental reuse is purchased with retained information whose lifetime needs an explicit policy. Sources: cs2-08-3 ## Completion is a separate proof obligation Naiad's timely dataflow model attaches logical timestamps to messages and provides notifications only after earlier relevant messages can no longer arrive. The inspected section describes the relationship between graph structure, nested loops, timestamps, and progress tracking. This coordination is distinct from the relational algebra used to compute a result. Correct update formulas alone do not establish that a reader has observed all consequences of an input version. Consider a deletion that temporarily removes a fact before an alternative derivation restores it. Exposing the intermediate state may be legitimate for a differential consumer that understands retractions, but it is not equivalent to returning a completed snapshot. An authorization application could react dangerously to either kind of transient visibility unless its contract is explicit. A proposed interface should therefore distinguish provisional differences from a completed version and identify which input frontiers justify completion. A wall-clock delay is not a proof that no causally relevant work remains. Conversely, demanding a globally complete snapshot after every tiny change may discard much of the concurrency that motivates dataflow execution. The design choice is not purely about latency: it determines which histories are observable and what downstream consumers are allowed to conclude from absence. These interface obligations belong in the evaluation even when the query result itself is a simple set. Sources: cs2-08-4 ## Algebra and implementation remain distinct The DBSP preprint proposes a stream-computation language, an incrementalization method, and encodings for rich query constructs. Its abstract explicitly includes grouping, aggregation, and forms of recursion. This is a broad algebraic direction, but the inspected source is an author abstract rather than an independent reconstruction of each transformation's proof. We use it to motivate compositional reasoning, not to assert universal practical efficiency. A useful algebraic identity for a bilinear join expands the change in a product into contributions from each changed input and their interaction. Omitting the interaction term when both inputs change in one batch produces an incorrect result even before recursion enters the picture. Our supplement checks that identity over small signed integer multiplicities. This arithmetic example is intentionally separate from set-valued reachability: thresholding a count to presence is nonlinear, and recursive saturation adds another layer. Calling every operation a linear delta transform obscures those boundaries. An implementation should state the algebra for each operator and prove or test how it composes with distinctness, aggregation, and iteration. A correct local update rule can still be integrated incorrectly if batch order, multiplicity normalization, or completion detection differs from its assumptions. The evaluation must exercise combinations, particularly simultaneous insertions and deletions, instead of testing isolated positive updates only. Sources: cs2-08-5 ## Multiplicity is an observable choice The official Differential Dataflow book explains that map preserves element counts and accumulates counts when distinct inputs become the same output. This small operator description provides a useful warning: a collection with multiplicities is not automatically a mathematical set. Projecting several records onto the same key can change its count even when its presence remains unchanged. Subsequent operators must be evaluated under the intended semantics. Suppose two independent source edges produce the same derived pair. Removing one contribution leaves the pair present under set semantics, while its multiplicity decreases under bag semantics. A consumer interested only in membership should receive no disappearance; a consumer computing a weighted aggregate may need an update. This distinction can be tested without recursion, making it a valuable first check before investigating cyclic cases. It also affects auditability. A record saying that a pair was deleted may mean that one derivation vanished, that its total weight reached zero, or that a whole snapshot row was replaced. Those events should not share an undocumented representation. The manuscript's graph oracle uses sets, its algebra check uses signed integer weights, and the figures label these choices. Their conclusions should not be transferred between algebras without rederiving the relevant identities and identifying how output presence is defined. Sources: cs2-08-6 ## A diamond with surviving support The first constructed workload is a diamond: edges connect a to b, a to c, b to d, and c to d. The positive transitive closure contains five pairs. Removing b to d leaves four pairs, because a still reaches d through c. A naive deletion strategy that removes every fact touched by the lost path can temporarily or permanently lose that valid pair unless it rederives surviving support. The figure includes a sequence that then removes c to d and reinserts b to d, yielding closure sizes five, four, two, and four. The accompanying model calculates these sizes by fixed-point iteration and independently by breadth-first reachability. It also checks the change sets, so a correct cardinality cannot hide substitution of the wrong pair. This example does not model the internal work of DRed or any optimized variant. It isolates the semantic target against which such work should be judged. An experimental comparison could record overdeleted pairs, rederived pairs, join probes, and retained support metadata in addition to elapsed time. The diamond's value is that it separates loss of a proof from loss of a fact. A benchmark containing only tree-shaped dependencies would not exercise this distinction and could misleadingly favor an implementation that assumes unique support. Author analysis or proposed verification. ## A one-edge update can change quadratic output The second constructed family is a directed chain of n vertices. Its positive transitive closure has n times n minus one divided by two pairs. Removing the edge between positions k minus one and k disconnects every earlier vertex from every later vertex, so k times n minus k pairs disappear. In a chain of twenty vertices with the central edge removed, one hundred pairs disappear from an original one hundred ninety. The figure varies the graph size and compares total closure size with the number of retracted pairs for a central deletion. This result imposes an output-size lower bound on any interface that explicitly emits each retracted pair: it must report those pairs regardless of how cleverly it avoids internal recomputation. An incremental algorithm can still save substantial work relative to a full rebuild, but small input change alone cannot guarantee small output or constant latency. The experiment is exact combinatorics, not a measured throughput curve. The supplement verifies the formula against independently recomputed closures over a range of chain lengths and cut positions. A production evaluation should stratify changes by affected output size and graph structure. Otherwise a latency histogram may conflate algorithmic overhead with the unavoidable work of communicating a large, correct change set to downstream consumers. Author analysis or proposed verification. ## A maintenance evaluation that can fail The proposed study should retain a fresh-evaluation oracle and compare every completed incremental version with it. Generate small exhaustive graphs for semantic checking, then larger synthetic and application-derived graphs for measurement. Mix insertions, deletions, duplicate contributions, and batches that change both sides of a join. Include cycles, diamonds, hubs, and nearly disconnected components, since they stress different support and output-size behaviors. Use deterministic update logs so competing implementations receive identical histories. Measure time to completed version, provisional-output volume, peak retained state, and work counters such as join probes or candidate derivations. Do not rank methods solely by end-to-end time: a method may trade memory for reuse, or emit more transient differences before the final snapshot converges. Define a timeout policy and report nontermination or resource exhaustion without removing those cases. For negative tests, retain the unsupported-cycle counterexample and deliberately omit the bilinear interaction term in a reference mutant; the harness should detect both. Finally, vary the reader contract. A consumer needing a stable snapshot and one accepting a stream of differences impose distinct completion requirements. A method that wins under one contract may not be comparable under the other. This protocol remains proposed; the delivered executable performs only the finite semantic and algebraic checks described here. Author analysis or proposed verification. ## Limits beyond positive finite rules The chosen fragment avoids negation, aggregation, arithmetic generation, and external functions. Each extension changes the proof obligations. With negation, learning a new fact may invalidate a previously derived absence claim; stratification supplies one disciplined organization but does not make arbitrary recursive negation harmless. Aggregation can require maintaining distributions or extrema rather than a single support bit. External functions may be nondeterministic or have side effects, undermining replay-based comparison. These are reasons to delimit the study, not to claim that advanced systems cannot support such features. The model also omits distributed failures, checkpoint consistency, input deduplication, and recovery. A mathematically correct delta can be applied twice after a retry unless the surrounding system identifies update batches and their commit status. Conversely, a lost negative update can leave stale derived facts even if every local operator is correct. A deployment needs a durable relation between input versions, checkpoints, and exposed outputs. We do not infer that relation from a query language's declarative syntax. The practical assurance argument should therefore have separate layers: query semantics, incremental equivalence, progress and visibility, and recovery behavior. Testing one layer is useful evidence, but it cannot silently stand in for the others when the maintained result controls a real action. Author analysis or proposed verification. ## Maintaining the explanation as well as the state Incremental Datalog is most credible when a completed result can be explained as the same least fixed point a fresh computation would produce. That statement allows aggressive reuse internally while preserving an external semantic reference. It also reveals why deletions are difficult: a stored fact can have many proofs, and a cycle can preserve apparent local support after all extensional support has disappeared. Multiplicities and logical time provide powerful implementation tools, but their meaning must remain explicit at each interface. The analytical evidence here is deliberately modest and complete within its scope. A diamond retains reachability after one proof vanishes; a central chain deletion changes a quadratic number of pairs; an unsupported cycle defeats naive local support retention; and a bilinear delta requires its cross term. Together these examples identify semantic and workload dimensions that an evaluation must cover. They do not establish a universally best maintenance algorithm. A useful next contribution would combine an independently checked completed-version oracle with transparent accounting of retained state and provisional output. Such evidence would let readers understand where reuse comes from, where it fails to reduce work, and which guarantees survive retractions. The maintained object is then more than a fast-changing table: it is a versioned result with an inspectable connection to its defining rules and input facts. Author analysis or proposed verification. ## Mathematical model R^*=\mu R.\left(E\cup(E\circ R)\right) Least positive reachability fixed point over a finite graph; paths have positive length, not reflexive closure. R_{i+1}=E\cup(E\circ R_i),\qquad R_0=\varnothing Monotone iteration over finite sets stabilizes; unrestricted arithmetic generation is outside scope. \Delta(A\Join B)=\Delta A\Join B+A\Join\Delta B+\Delta A\Join\Delta B Bilinear expansion for signed multiplicities and simultaneous changes; distinctness is a separate nonlinear operator. |R_{\mathrm{chain}}|=\frac{n(n-1)}2 Positive reachability count for a directed chain of n vertices. |\Delta^-R|=k(n-k) Deleting the chain edge from vertex k-1 to k removes all cross-cut pairs; 1 <= k < n. ## Figure 1: Completed reachability through a diamond update history Start with diamond; delete b-to-d, delete c-to-d, then reinsert b-to-d. Sizes are 5, 4, 2, 4. Assumptions: Set semantics; Positive-length paths; Fresh fixed point at every committed version Data: figures/datalog-incremental-state-1.csv ## Figure 2: Output change from a single central chain-edge deletion At n=20, one central edge removal retracts 100 of 190 pairs; this counts output, not engine work. Assumptions: Directed chain; Central cut; Each pair explicitly represented Data: figures/datalog-incremental-state-2.csv ## Executed finite checks { "diamond_closure_sizes": [ 5, 4, 2, 4 ], "chain20_pairs": 190, "chain20_retracted": 100, "naive_cycle_retained": [ "p", "q" ], "least_after_base_removal": [] } ## Comparison Case | Correct semantic outcome | Risk for a simplistic method Diamond loses one branch | Alternative path remains | Deleting every affected fact Unsupported recursive cycle | Least fixed point becomes empty | Mutual local support survives Central chain deletion | Many pairs retract | Assuming input size bounds output size Simultaneous join changes | Include interaction term | Adding only two one-sided deltas ## Proposed validation protocol - Fix set or bag semantics and positive versus reflexive reachability. - Build an independent fresh-evaluation oracle. - Enumerate all three-vertex directed graphs without self-edges. - Exercise deletion, insertion, duplicate support and batched updates. - Check pair identities rather than cardinalities alone. - Include diamonds, cycles, chains, hubs and output-size strata. - Record completion frontier and distinguish provisional output. - Measure retained state, change volume and work counters. - Test unsupported-cycle and missing-cross-term mutants. - Publish deterministic histories, failures and timeout policies. ## Limitations - Finite positive reachability is narrower than full Datalog dialects. - No maintenance engine or published benchmark was rerun. - The model does not implement DRed, DBSP or differential dataflow. - Set closure and signed-multiplicity algebra are tested separately. - Distributed failures, persistence and replay are excluded. - Selected source abstracts do not substitute for independent proof audits. ## Open research questions - How much maintenance work is unavoidable output versus avoidable rediscovery of support? - Which retained support summaries best handle cyclic deletion without excessive memory? - How should provisional changes and completed versions be exposed to authorization consumers? ## Evidence and boundaries cs2-08-1: Pure finite Datalog differs from arithmetic extensions that can fail to terminate. Boundary: Only the finite positive fragment is modeled. Locator: Tutorial overview and transitive closure cs2-08-2: Recursive support and multiple derivations create different maintenance tradeoffs. Boundary: No ranking inferred beyond authors inspected summary. Locator: Abstract and introduction cs2-08-3: Differential computation indexes changes across partially ordered versions. Boundary: Current library performance not established. Locator: Abstract and introduction cs2-08-4: Timely notifications depend on impossibility of earlier relevant messages. Boundary: Not an application-level durability guarantee. Locator: Section 2.2 and 2.3 cs2-08-5: DBSP proposes compositional incrementalization for rich query constructs. Boundary: Abstract scope; transformations not independently proved. Locator: Author abstract cs2-08-6: Map preserves multiplicities and combines counts for equal results. Boundary: Does not imply recursive set semantics. Locator: The Map Operator ## References cs2-08-1. Souffle project. Tutorial: Introduction to Datalog. Souffle project documentation (2026). https://souffle-lang.github.io/tutorial Access: Overview, finite-domain restriction, arithmetic-functor warning and transitive closure example; access-year used for undated living documentation. cs2-08-2. Boris Motik, Yavor Nenov, Robert Piro, Ian Horrocks. Maintenance of datalog materialisations revisited. Artificial Intelligence 269 (2019). https://www.cs.ox.ac.uk/people/ian.horrocks/Publications/download/2019/MNPH19a.pdf Access: Abstract and introductory maintenance tradeoffs; full 61-page proof development not audited. cs2-08-3. Frank McSherry, Derek G. Murray, Rebecca Isaacs, Michael Isard. Differential dataflow. CIDR (2013). https://www.cidrdb.org/cidr2013/Papers/CIDR13_Paper111.pdf Access: Abstract and introduction on partial versions and indexed changes; no benchmark reproduction. cs2-08-4. Derek G. Murray, Frank McSherry, Rebecca Isaacs, Michael Isard, Paul Barham, Martin Abadi. Naiad: A Timely Dataflow System. SOSP (2013). https://www.microsoft.com/en-us/research/wp-content/uploads/2013/11/naiad_sosp2013.pdf Access: Abstract and section 2, especially logical timestamps and notification condition. cs2-08-5. Mihai Budiu, Frank McSherry, Leonid Ryzhyk, Val Tannen. DBSP: Automatic Incremental View Maintenance for Rich Query Languages. arXiv preprint (2022). https://arxiv.org/abs/2203.16684 Access: Abstract and author/submission record; formal transformations not independently checked. cs2-08-6. Differential Dataflow project. Differential Dataflow: The Map Operator. Official project book (2026). https://timelydataflow.github.io/differential-dataflow/chapter_2/chapter_2_1.html Access: Map preserves multiplicities and merges counts for equal output elements; access-year for living docs. ## Provenance Selected primary-source technical review; inspected scopes are recorded per source. No exhaustive search or independent proof reconstruction. Written by Codex (AI), with source-based technical synthesis and explicit author-constructed models. Reproducible analytical illustrations, not measured system benchmarks. Codex team technical checks; no independent human or journal peer review.