Bounding Fixed Points of Non-Monotone Processes: Theory to Practice
For developers of program analyzers and solvers relying on non-monotone reasoning, this work makes AFT approximations practical by improving efficiency and precision, though the gains are incremental over existing AFT theory.
The authors address the inefficiency and coarseness of Approximation Fixpoint Theory (AFT) for non-monotone processes, proving soundness of an abstract interpretation and introducing a controlled unsoundness algorithm that tightens approximations. Their method achieves polynomial-time complexity and accelerates convergence in answer set programming (reducing search space) and reduces rollback in speculative program analysis.
Many modern solvers and program analyzers rely on non-monotone reasoning (e.g. negation-as-failure, speculative updates, backtracking) for which classical monotone fixed-point methods do not apply. The general problem of finding the fixed points of these processes is a difficult one. For this reason, there have been theoretical efforts in existing Approximation Fixpoint Theory (AFT) from the domain of logic programming to approximate fixed points of non-monotone operators. Tight approximations of these fixed points are highly useful for accelerating non-monotonic computations by restricting the search space. In practice, however, even the best approximations obtained through AFT can be coarse and computationally expensive. We aim to address both issues to make AFT approximation methods practical for use in programming languages (PL) settings. To mitigate inefficiency, we prove the soundness of an abstract interpretation for approximating operators. To improve upon coarse approximations, we carefully introduce controlled unsoundness to design an effective yet practical algorithm for partitioning and tightening AFT's best approximations. This algorithm is sound, anytime, and guarantees termination on finite-height lattices. We further present a modification that ensures polynomial-time complexity. We instantiate these methods in two settings: (1) answer set programming, where it serves as a convergence-accelerating pre-processor, and (2) speculative program analysis, where it reduces rollback while preserving soundness. In both settings, we focus on implementation-level details to demonstrate the practical applicability of our methods.