arXiv · Databases· Chengxi Yang, Tej Chajed, Thomas Reps·· 5 小时前AI 评分22
Fixing the Fixpoint：增量递归计算收敛检测的形式化理论
Fixing the Fixpoint: A Formal Theory of Convergence Detection for Incremental Recursive Computation
AI 导读
本文针对 DBSP 等增量递归计算理论中的 Fixpoint Detection 问题，指出"FirstZero"策略不成立，且任意 DBSP 电路的精确 FPD 不可能。研究提出 IntConv 收敛准则并证明其充分性，定义 StFP 谓词并给出可靠完备检测器，对 Datalog 与嵌套 while 查询等程序提供语义保证，形式化验证于 Lean。
来源：arXiv · Databases · arxiv.org