发表机构
University of California, Berkeley; Shanghai Jiao Tong University; UW-Madison; University of Wisconsin–Madison; Google DeepMind（加州大学伯克利分校; 上海交通大学; 威斯康星大学麦迪逊分校; 威斯康星大学麦迪逊分校; 谷歌DeepMind）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对增量递归计算中不动点检测的不健全问题，提出基于DBSP的形式化收敛检测理论，定义内部收敛与状态不动点检测器，证明其健全性与完备性，并在Lean中验证。
AI 中文摘要
现代增量计算理论（如DBSP）已能高效地实现一般递归计算的增量式处理。为此，它们需要运行时的不动点检测（FPD）机制来判断迭代计算是否已达到不动点并应终止。然而，我们表明，即使在自然出现的情形下，通常建议的“首零”策略也是不健全的，且对于具有表达力原始节点的任意DBSP电路，精确的FPD是不可能的。这一问题揭示了此类理论的数学规范与实现之间的根本差距。为填补这一差距，我们以DBSP为核心演算，发展了一套收敛检测的形式化理论。在该理论中，我们将内部收敛（IntConv）定义为对应于实际实现所用的内部状态稳定性策略的声明性准则，并证明IntConv是外部收敛的充分条件。随后，我们定义了状态不动点（StFP）谓词及一个健全且完备的StFP检测器。将StFP检测器与固定输入和零输出检查相结合，可得到一个健全且完备的IntConv检测器。此外，对于一大类有用的电路（程序），包括Datalog查询、嵌套while查询及其增量优化版本，我们证明IntConv不仅是健全的，而且是完备的（即理论中的任何收敛都蕴含我们准则中的收敛）。因此，我们的理论为所有这些电路上的收敛检测提供了语义保证。我们的结果已在Lean中正式验证，形式化内容可从此https URL获取。
英文摘要
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/.
