PaperlayerView exact revision on arXiv

Source-linked AI summary

Fixing the Fixpoint: A Formal Theory of Convergence Detection for Incremental Recursive Computation

Chengxi Yang, Tej Chajed, Thomas Reps

arXiv:2610.00530v1cs.PLcs.DB

TL;DR

Incremental recursive computation requires runtime fixpoint detection, but FirstZero can be unsound and exact detection is impossible for arbitrary expressive circuits. The paper formalizes internal convergence and a detector for it, establishing complete detection for useful circuit classes while noting that its results are mainly theoretical.

  • Problem

    DBSP needs runtime fixpoint detection, but deciding from a finite stream prefix whether an input eventually becomes zero is a core challenge, and FirstZero can be unsound.

    Source: §1 · p. 2, §4 · p. 11

  • Method

    The paper formalizes internal convergence through state fixpoints and combines an StFP detector with fixed-input and zero-output checks for global IntConv detection.

    Source: §1 · p. 3, §6 · p. 19

  • Results

    IntConv is sound and complete for regular circuits and their incrementally optimized versions, although exact FPD is impossible for arbitrary expressive circuits.

    Source: §1 · p. 3

  • Takeaways & Limitations

    The theory provides semantic guarantees for convergence detection in useful circuits, including Datalog queries, nested while queries, and their incrementally optimized versions.

    Source: §1 · p. 3

    The results are mainly theoretical; evaluating detector overhead and end-to-end performance in a complete system remains future work.

    Source: §10 · p. 25

Abstract

from arXiv · show

Modern incremental computation theories like DBSP have enabled efficient incrementalization of general recursive computations. To do so, they require a runtime Fixpoint Detection (FPD) mechanism to detect whether an iterative computation has reached the fixpoint and thus should terminate. However, we show that the commonly suggested "FirstZero" strategy is unsound even in naturally arising cases, and that exact FPD is impossible for arbitrary DBSP circuits with expressive primitive nodes. This issue reveals a fundamental gap between the mathematical specification and implementations of such theories. To fill this gap, using DBSP as a core calculus, we develop a formal theory of convergence detection. Within this theory, we define internal convergence (IntConv) as a declarative criterion corresponding to the internal-state-stability strategy used by practical implementations, and prove that IntConv is a sufficient condition for external convergence. We then define the state fixpoint (StFP) predicate and a sound and complete StFP detector. Combining the StFP detector with fixed-input and zero-output checks yields a sound and complete IntConv detector. Moreover, for a large class of useful circuits (programs) including Datalog queries, nested while queries, and their incrementally optimized versions, we show that IntConv is not only sound but also complete (meaning any convergence in the theory implies the convergence in our criterion). As a result, our theory provides semantic guarantees for convergence detection on all these circuits. Our results are formally verified in Lean, with the formalization available at https://github.com/Arcadia-Y/fixing-the-fixpoint/.

1 Introduction

Incremental computation efficiently handles changing inputs, but recursive queries make it difficult to combine incrementalization with reliable fixpoint detection. The paper identifies flaws in FirstZero and develops formal convergence criteria that are sound generally and complete for useful circuit classes.

1 Introduction

  • Incremental view maintenance updates results from small input changes, while recursive queries such as transitive closure require iterative computation.Standard relational-query maintenance is well understood and widely deployed.Source: §1 · p. 1
  • Exact fixpoint detection is impossible for arbitrary expressive circuits when DBSP’s primitive nodes make it Turing-complete.The paper identifies a fixed level-1 circuit for which no computable detector is both sound and complete.Source: §1 · p. 2
  • The FirstZero strategy is unsound, and using it can produce output that differs from the mathematical specification.The strategy stops at the first zero, which intuitively suggests that adjacent results have not changed.Source: §1 · p. 2
  • Internal convergence (IntConv) formalizes internal-state stability and is a sound sufficient criterion for convergence.The criterion corresponds to the internal-state-stability strategy used by practical implementations.Source: §1 · p. 2
  • A sound and complete StFP detector, combined with fixed-input and zero-output checks, yields compositional IntConv detection that is complete for regular circuits and their incrementally optimized versions.The paper includes Datalog and while queries among the useful circuit classes for which convergence can be detected completely.Source: §1 · p. 3
  • The paper’s key results are formally verified in Lean 4.The Lean development is described in the paper, with mechanized proofs available as supplementary material.Source: §1 · p. 3

2 Overview

DBSP’s FirstZero strategy can stop delta-of-deltas computation before it has converged, producing incorrect results. The paper formalizes convergence criteria and detectors, then proves exact detection for useful circuit classes.

2.1 DBSP and the Unsoundness of the FirstZero Strategy

  • DBSP incrementalizes transitive closure through naive, semi-naive, then delta-of-deltas circuits, progressively optimizing inner and outer iterations.Source: §2.1 · pp. 3–4
  • Fixpoint detection must decide whether an inner computation has converged, but the first zero can precede later nonzero values in delta-of-deltas.Source: §2.1 · pp. 4–5
  • In the graph example, cancellation creates an early empty delta, so FirstZero returns an extra (1,4) edge rather than the correct transitive closure.Source: §2.1 · p. 5, Figure 3 · p. 5

2.2 Overview of Our Theory

  • The theory distinguishes external convergence from internal convergence, with IntConv requiring internal stability and implying external convergence.Source: §2.2 · p. 6
  • An external-convergence-only evaluation can require recursive trace-backs and additional retained state, but this is a qualitative example, not a performance evaluation or lower bound.Source: §2.2 · p. 6
  • A sound and complete structural StFP detector, combined with fixed-input and zero-output checks, detects IntConv across nested bracketed circuits.Source: §2.2 · pp. 6–7
  • Regular circuits, including Datalog and while queries, are Conv-complete, and plift and incOpt preserve this property.Source: §2.2 · p. 7

3 Preliminary: A Formal Language for DBSP

The section introduces DBSP’s stream and circuit calculus, then uses it to express how a recursive Datalog query is implemented and incrementally optimized. Its formal language represents both stream-level computations and nested iterative computations.

3.1 Streams and Operators in DBSP

  • Lifting applies scalar functions pointwise to streams, while delay shifts a stream and feedback cycles express recursive stream equations.DBSP uses feedback cycles to express iteration and construct integration.Source: §3.1 · p. 7
  • Integration computes running sums and differentiation subtracts the delayed stream; these inverse operators define a circuit’s incremental form as I ▷ c ▷ D.For an operator Q, its incremental version is QΔ = D ◦ Q ◦ I.Source: §3.1 · p. 7, §3.2 · p. 9
  • Stream introduction starts an iteration, while stream elimination sums its intermediate results and is defined only when the stream is zero almost everywhere.If the stream does not eventually become zero, the summation diverges.Source: §3.1 · p. 8
  • Nested streams represent outer and inner time as two dimensions, allowing DBSP to distinguish incremental-computation time from recursive-iteration time.The two dimensions correspond to rows and columns of the nested stream.Source: §3.1 · p. 8

3.2 A Formal Language for DBSP Well-Formed Circuits

  • The formal circuit language assigns circuits stream or nested-stream levels and uses primitive nodes to lift user-defined scalar functions into stream operators.Its denotational semantics maps level-1 circuits to stream operators and level-2 circuits to nested-stream operators.Source: §3.2 · pp. 8–9, Table 1 · p. 9
  • The syntax includes derived integration, differentiation, and unoptimized incremental circuits, while plift and incOpt formalize lifting and syntax-guided incremental optimization.Primitive nodes may use customizable incremental forms; lifting is pushed into the inner circuit by plift.Source: §3.2 · pp. 9–10

3.3 Example: Implementing and Incrementalizing the Datalog Query in DBSP

  • DBSP represents relations with Z-sets, where integer counts—including negative counts—can represent insertions and deletions.The example treats Z-sets as their underlying sets for most cases.Source: §3.3 · p. 10
  • DBSP expresses recursive Datalog computation with a feedback circuit, then derives semi-naive and delta-of-deltas forms through incremental optimization.The naive circuit iterates F on the input; the optimized forms transform its query body.Source: §3.3 · p. 10, Figure 6 · p. 10

4 The Fixpoint-Detection Problem and the Convergence-Detection Problem

The section formalizes fixpoint detection for DBSP circuits and shows that simple zero-based detection can fail, while exact detection is impossible for sufficiently expressive circuits. It defines the scope of fixpoint and convergence detection and motivates a sound convergence criterion for useful circuit subclasses.

4 The Fixpoint-Detection Problem and the Convergence-Detection Problem

  • Fixpoint detection asks whether a bracketed circuit’s output stream becomes zero after some index, despite observing only a finite prefix at runtime.A complete circuit may contain multiple bracketed sub-circuits, each of which must reach a fixpoint for global convergence.Source: §4 · p. 11
  • A sound detector’s first true value must certify that the output has converged to zero, while completeness requires it eventually to return true when convergence occurs.The specification covers both level-1 and level-2 circuits.Source: §4 · pp. 11–12

4.1 Example: The FirstZero Strategy and Its Limitation

  • FirstZero is sound and complete for naive and semi-naive Datalog query bodies, but is unsound for the delta-of-deltas query body.FirstZero stops at the first zero value, which can incorrectly signal that adjacent results no longer change.Source: §4.1 · p. 12

4.2 Impossibility of Exact Fixpoint Detection

  • For Turing-complete DBSP primitives, a fixed level-1 circuit has no computable detector that is both sound and complete.A proposed detector would recognize the complement of the halting problem, which is not recursively enumerable.Source: §4.2 · p. 13
  • Exact detection’s impossibility for arbitrary circuits does not rule out sound and complete detectors for subclasses; the result motivates IntConv and its completeness for regular circuits.The cited subclasses include Datalog queries, while queries, and their incrementally optimized forms.Source: §4.2 · p. 13

5 A Sound Convergence Criterion: IntConv

The section defines internal convergence as a sound sufficient condition for external convergence, applying local internal-fixpoint checks to bracketed sub-circuits and requiring fixed output zero. It also explains a qualitative implementation benefit: internal stability can avoid recursive trace-backs or additional retained state.

5 A Sound Convergence Criterion: IntConv

  • FixAfter generalizes ZeroAfter by requiring a stream to remain at its value from a given index onward, including repetition of the same inner stream for nested streams.This fixed-value condition underlies the internal-fixpoint definitions.Source: §5 · p. 13
  • IntFP is defined structurally and by stream level: primitive and temporal nodes inherit external-fixpoint conditions, while combinators recurse into sub-circuits.Bracketed circuits delegate to their enclosed circuit, and the recursive rules handle nested brackets.Source: §5 · pp. 14–15
  • Internal fixpoint implies external fixpoint for both level-1 and level-2 circuits, establishing IntFP as a sound sufficient condition.The proof proceeds first for level 1, then for level 2 based on the level-1 result.Source: §5 · p. 15
  • IntConv applies a local internal-fixpoint criterion to every bracketed sub-circuit and requires its fixed output to be zero, making it sufficient for external convergence.The section presents this as a global criterion built from local checks.Source: §5 · pp. 13, 15
  • The implication is one-way in general: external fixpoint or convergence need not imply internal fixpoint or convergence.Thus IntConv is not complete for general circuits.Source: §5 · p. 15
  • With ExtConv alone, a later outer iteration needing more inner steps can force recursive recomputation or require retaining history, potentially across unbounded iterations.In the example, IntConv guarantees stabilized internal values are already stored, avoiding recursive trace-back; this is a qualitative example, not a general lower bound or performance measurement.Source: §5 · pp. 15–16

6 The StFP Detector and the Global IntConv Detector

The section defines State Fixpoint as a semantic counterpart of circuit-state stability and gives a structural, level-indexed detector. A fixed-input check turns StFP detection into local IntFP detection, and zero-output checks across bracketed sub-circuits yield global IntConv detection.

6 The StFP Detector and the Global IntConv Detector

  • Combining StFP detection with fixed-input and zero-output checks across all bracketed sub-circuits yields a sound and complete global IntConv detector.The structural detector is a correctness-oriented fallback; optimizing alternatives and measuring their overhead in a complete system remain future work.Source: §6 · pp. 16, 19
  • Because the denotational model has no explicit states, the formalization relies on the assumption that a circuit’s state at a point is determined by its input up to that point.The detector simulates state computation using input computation up to that point.Source: §6 · p. 17
  • StFP formalizes the state-stability property by asking whether the circuit state would be at an internal fixpoint if its future input remained fixed.The fixed continuations preserve the observed input through the designated index and impose a fixed future afterward.Source: §6 · p. 17
  • The structural detector treats primitive and standard nodes as stateless, checks state equality for temporal nodes, and recurses through feedback loops.For delay, it compares the current input with stored state; for feedback, it compares current and stored delayed outputs.Source: §6 · p. 18
  • The StFP detector is proved sound and complete for the StFP predicate.Its clauses recurse through structural combinators and delegate across circuit levels, so it applies compositionally to nested circuits.Source: §6 · p. 19

7 IntConv is Complete for Useful Circuits

The section identifies circuits for which internal convergence is complete, so internal and external convergence agree, and proves that regular circuits and their incrementally optimized forms satisfy this property.

7 IntConv is Complete for Useful Circuits

  • Conv-completeness characterizes circuits where external convergence implies IntConv, allowing specialized detectors such as FirstZero for naive and semi-naive circuits.For these circuits, IntConv and ExtConv coincide.Source: §7 · pp. 19–20

7.1 Regular Circuits Are Conv-complete

  • Every regular circuit, built from lifted scalar circuits, composition, Datalog recursion, and while recursion, is Conv-complete.The proof establishes an iteration bound of n + 1 for Datalog and while query bodies and extends completeness by structural induction.Source: §7.1 · p. 21
  • The regular-circuit class can be extended with recursive constructs that establish the required variant of FP-completeness.The section also establishes FP-completeness for regular circuits.Source: §7.1 · p. 21

7.2 Conv-complete Circuits Are Closed under Incremental Optimization

  • plift preserves Conv-completeness and FP-completeness, with its correctness relating denotation and IntConv and preserving the stated internal fixpoint properties.The proof uses strong semantic equivalence for denotation and internal convergence.Source: §7.2 · p. 22
  • incOpt preserves Conv-completeness when primitive-node transformations are sound incremental forms, an assumption supported by unoptimized, linear, and bilinear forms.Under that assumption, incOpt is itself a sound incremental form.Source: §7.2 · p. 23
  • The delta-of-deltas Datalog query is Conv-complete when its base circuit is regular.This follows from the preservation results for incremental optimization.Source: §7.2 · p. 23

8 Lean Formalization

The paper formalizes its results in Lean 4, building on an existing DBSP theory formalization and restricting stream levels to balance generality with tractable verification.

8 Lean Formalization

  • The Lean 4 development adds 11,748 lines for the new theory to a 2,095-line adaptation of the existing DBSP formalization.The new code covers IntConv, a Hoare logic framework, and Zsets circuit case studies.Source: §8 · p. 23
  • The formal language supports stream levels 1 and 2, sufficient for arbitrarily nested recursive queries and delta-of-deltas optimization while keeping mechanized proofs tractable.The authors state that the level-indexed theory could in principle generalize to arbitrary natural-number levels.Source: §8 · p. 23

9 Related Work

The related work situates the paper alongside incremental computation and fixpoint theories, while distinguishing its focus on runtime convergence detection for incrementally transformed circuits.

9 Related Work

  • Prior work studies incremental computation across theory, databases, programming languages, and other fields, including database view maintenance.The passage describes incremental computation as reusing previous results to save time.Source: §9 · p. 24
  • Prior fixpoint research develops derivatives of recursive computations and finite-convergence conditions for Datalog over pre-semirings, whereas this paper formalizes runtime FPD for incrementally transformed circuits.The cited works address incremental fixpoint constructions or convergence for particular Datalog semantics.Source: §9 · p. 24
  • Feldera uses operator-level fixed-point checks and circuit-wide stability, which the paper gives a declarative account through IntFP, IntConv, and StFP.The StFP detector provides an algorithmic formalization of that strategy.Source: §9 · p. 24
  • The main contribution is formal guarantees: IntConv is sound, the StFP detector is sound and complete, and global IntConv detection is sound and complete; results are machine-checked in Lean 4.Source: §9 · p. 24
  • For Differential Dataflow, a zero differential does not imply collection repetition, so FirstZero cannot soundly identify first-repetition egress.The passage describes this as a gap between DD's mathematical treatment and prototype convergence reporting.Source: §9 · pp. 24–25
  • Other foundations cover fixed-iteration egress or bounded inner streams, while this theory gives a sound criterion for unbounded computations and identifies classes where it is complete.The comparison names Abadi et al. and Flo.Source: §9 · p. 25

10 Conclusion

The conclusion states the formal guarantees for convergence detection and their scope, while noting that implementation-level performance comparisons remain future work.

10 Conclusion

  • The paper proves FirstZero unsound for delta-of-deltas recursive optimization and exact FPD impossible for arbitrary expressive circuits.It defines sound IntConv and a sound and complete StFP detector, then combines StFP with fixed-input and zero-output checks for global IntConv detection.Source: §10 · p. 25
  • IntConv is complete for regular circuits, including arbitrarily nested while loops, Datalog queries, and their incrementally optimized versions.The results are formalized in Lean 4.Source: §10 · p. 25
  • The results are theoretical rather than an empirical performance evaluation, leaving detector overhead and end-to-end execution comparisons for future work.Such comparisons depend on the query, workload, data representation, and other system-level optimizations.Source: §10 · p. 25
Loading 2610.00530v1…