Optimal Convergence of Iterative Methods for Datalogo

$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”ive 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.