Datalogo 迭代方法的最优收敛性

中文摘要 AI 辅助

$\mathsf{Datalog}^\circ$ 被引入作为 Datalog 的扩展，它增加了表达能力，同时保留了简单的最小不动点语义，并支持半朴素求值和需求变换等优化技术。$\mathsf{Datalog}^\circ$ 通过将 Datalog 的 {\em or} 和 {\em and} 运算符推广为半环上的加法和乘法来实现这一点。找到 $\mathsf{Datalog}^\circ$ 程序的（最小）不动点等价于在底层半环上求解一个多项式方程组。求解这些多项式方程组不仅是 $\mathsf{Datalog}^\circ$ 理论中的一个基本问题，而且在计算机科学中也有许多应用，例如数据库、程序分析和优化。本文解决了 $\mathsf{Datalog}^\circ$ 理论中的一个关键开放问题：我们证明了在交换 $p$-稳定半环上求解这些多项式方程组的迭代方法收敛步数的紧上界。特别地，我们表明收敛步数为 $O((p+1)n)$，其中 $n$ 是 $\mathsf{Datalog}^\circ$ 程序的输出大小。由于收敛步数只是 $\mathsf{Datalog}^\circ$ 求值运行时间的代理，我们还考虑了使用的半环运算次数，并表明对于一类自然算法，$O((p+1)mn)$ 是一个紧上界，其中 $m$ 是每次迭代的最大半环运算次数。

英文摘要

$\mathsf{Datalog}^\circ$ has been introduced as an extension to Datalog that increases expressiveness, yet retains simple least fixpoint semantics and admits optimization techniques such as semi-naïve evaluation and demand transformation. $\mathsf{Datalog}^\circ$ accomplishes this by generalizing the {\em or} and {\em and} operators of Datalog to addition and multiplication over a semiring. Finding a (minimal) fixpoint of a $\mathsf{Datalog}^\circ$ program is equivalent to finding a solution to a system of polynomial equations over the underlying semiring. Solving these systems of polynomial equations is not only a fundamental problem in the theory of $\mathsf{Datalog}^\circ$, but also has many applications in computer science, such as in databases, program analysis, and optimization. This paper resolves a key open problem in the theory of $\mathsf{Datalog}^\circ$: we prove a tight upper bound on the number of steps until convergence of iterative methods for solving these polynomial equation systems over a commutative $p$-stable semiring. In particular, we show that the number of steps until convergence is $O((p+1)n)$ where $n$ is the output size of the $\mathsf{Datalog}^\circ$ program. As the number of steps until convergence is only a proxy for the runtime of $\mathsf{Datalog}^\circ$ evaluation, we also consider the number of semiring operations used and show that, for a natural class of algorithms, $O((p+1)mn)$ is a tight upper bound, where $m$ is the maximum number of semiring operations per iteration.

发表机构

• University of Wisconsin-Madison（威斯康星大学麦迪逊分校）
• University of California, Santa Cruz（加州大学圣克鲁兹分校）
• Carnegie Mellon University（卡内基梅隆大学）
• RelationalAI
• University of Pittsburgh（匹兹堡大学）
• Gray Systems Lab, Microsoft（微软灰系统实验室）

机构由 AI 辅助整理，请以论文原文为准。