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.

翻译：许多现代求解器和程序分析器依赖于非单调推理（例如否定即失败、推测性更新、回溯），而经典的单调不动点方法对此并不适用。寻找这些过程的不动点是一个普遍难题。因此，逻辑编程领域中已有的近似不动点理论（AFT）从理论上致力于近似非单调算子的不动点。这些不动点的紧密近似通过限制搜索空间，对于加速非单调计算极为有用。然而在实践中，即便通过AFT获得的最佳近似也可能较为粗糙且计算成本高昂。我们旨在解决这两个问题，使AFT近似方法在编程语言（PL）环境中具备实用性。为了缓解效率低下的问题，我们证明了用于近似算子的抽象解释的正确性。为了改进粗糙近似，我们谨慎地引入可控的不正确性，设计了一种有效且实用的算法，用于划分和收紧AFT的最佳近似。该算法是可靠的、可随时终止的，并保证在有限高度格上终止。我们进一步提出了一种改进，以确保多项式时间的复杂度。我们在两个场景中实例化了这些方法：（1）答案集编程，作为加速收敛的预处理工具；（2）推测性程序分析，在保持正确性的同时减少回滚。在这两个场景中，我们侧重于实现层面的细节，以证明我们方法的实际适用性。