On Fixed Point Equations over Commutative Semirings

Abstract

Fixed point equations x = f(x) over ω-continuous semirings can be seen as the mathematical foundation of interprocedural program analysis. The sequence 0, f(0),f ²(0),... converges to the least fixed point μ f. The convergence can be accelerated if the underlying semiring is commutative. We show that accelerations in the literature, namely Newton’s method for the arithmetic semiring [4] and an acceleration for commutative Kleene algebras due to Hopkins and Kozen [5], are instances of a general algorithm for arbitrary commutative ω-continuous semirings. In a second contribution, we improve the $\mathcal{O}(3^n)$ bound of [5] and show that their acceleration reaches μ f after n iterations, where n is the number of equations. Finally, we apply the Hopkins-Kozen acceleration to itself and study the resulting hierarchy of increasingly fast accelerations.