Automatic static cost analysis infers information about the resources used by programs without actually running them with concrete data, and presents such information as functions of input data sizes. Most of the analysis tools for logic programs (and other languages) are based on setting up recurrence relations representing (bounds on) the computational cost of predicates, and solving them to find closed-form functions that are equivalent to (or a bound on) them. Such recurrence solving is a bottleneck in current tools: many of the recurrences that arise during the analysis cannot be solved with current solvers, such as Computer Algebra Systems (CASs), so that specific methods for different classes of recurrences need to be developed. We address such a challenge by developing a novel, general approach for solving arbitrary, constrained recurrence relations, that uses machine-learning sparse regression techniques to guess a candidate closed-form function, and a combination of an SMT-solver and a CAS to check whether such function is actually a solution of the recurrence. We have implemented a prototype and evaluated it with recurrences generated by a cost analysis system (the one in CiaoPP). The experimental results are quite promising, showing that our approach can find closed-form solutions, in a reasonable time, for classes of recurrences that cannot be solved by such a system, nor by current CASs.

翻译：自动静态成本分析通过推断程序在使用具体数据运行前所消耗资源的信息，并以输入数据大小的函数形式呈现这些信息。大多数逻辑程序（及其他语言）的分析工具基于建立表示谓词计算成本（边界）的递推关系式，并通过求解这些关系式找到与其等价（或界定其边界）的闭式函数。这种递推求解是当前工具的一个瓶颈：分析过程中产生的许多递推关系式无法通过当前求解器（如计算机代数系统，CASs）求解，因此需要针对不同类别递推关系开发特定方法。我们通过开发一种新颖的通用方法应对这一挑战，该方法利用机器学习稀疏回归技术猜测候选闭式函数，并结合SMT求解器与CAS验证该函数是否真正满足递推关系。我们实现了原型系统，并使用成本分析系统（CiaoPP中的系统）生成的递推关系式进行验证。实验结果令人鼓舞，表明我们的方法能在合理时间内为那些无法被现有系统及CASs求解的递推关系类找到闭式解。