Recurrence equations have played a central role in static cost analysis, where they can be viewed as abstractions of programs and used to infer resource usage information without actually running the programs with concrete data. Such information is typically represented as functions of input data sizes. More generally, recurrence equations have been increasingly used to automatically obtain non-linear numerical invariants. However, state-of-the-art recurrence solvers and cost analysers suffer from serious limitations when dealing with the (complex) features of recurrences arising from cost analyses. We address this challenge by developing a novel order-theoretical framework where recurrences are viewed as operators and their solutions as fixpoints, which allows leveraging powerful pre/postfixpoint search techniques. We prove useful properties and provide principles and insights that enable us to develop techniques and combine them to design new solvers. We have also implemented and experimentally evaluated an optimisation-based instantiation of the proposed approach. The results are quite promising: our prototype outperforms state-of-the-art cost analysers and recurrence solvers, and can infer tight non-linear lower/upper bounds, in a reasonable time, for complex recurrences representing diverse program behaviours.

翻译：递归方程在静态成本分析中占据核心地位，可视为程序的抽象表示，用于在不使用具体数据实际运行程序的情况下推断资源使用信息。此类信息通常表示为输入数据规模的函数。更广义而言，递归方程已日益广泛地用于自动获取非线性数值不变量。然而，在处理成本分析中产生的（复杂）递归方程特征时，现有最先进的递归求解器与成本分析工具存在严重局限性。我们通过构建新颖的序理论框架应对这一挑战：将递归方程视为算子，其解视为不动点，从而能够利用强大的前/后不动点搜索技术。我们证明了该框架的有效性质，提供了相关原理与洞见，以此为基础开发新技术并将其组合以设计新型求解器。同时，我们实现了所提出方法的基于优化的实例化方案并进行实验评估。结果极具前景：我们的原型系统在合理时间内，对表征多样化程序行为的复杂递归方程，能够推断出紧致的非线性下/上界，其性能优于当前最先进的成本分析工具与递归求解器。