模板和递归：更好地结合在一起
Templates and Recurrences: Better Together
摘要：
本文是文献中关于生成数值不变量的两种思想的汇合，即：（1）基于模板的方法，和（2）基于递归的方法。基于模板的方法从包含未知量的模板开始，并通过提取和求解未知量上的约束来找到与模板匹配的不变量。基于模板的方法的缺点是，它们需要预先固定可能出现在不变量中的项的集合。这个缺点是特别突出的非线性不变的生成，因为用户必须提供最大程度的多项式，基地的指数等，另一方面，递归为基础的方法能够找到复杂的非线性数学关系，包括多项式，指数，和递归，因为这种关系出现的解决方案递归。然而，过去的基于递归的不变量生成方法的缺点是它们主要是基于循环的分析：它们使用递归来关联循环的前状态和后状态，因此如何将它们应用于递归过程并不明显，特别是如果该过程是非线性递归的（例如，树遍历算法）。在本文中，我们结合这两种方法，并获得一种技术，使用模板中的未知数是函数，而不是数字，和对未知数的约束递归。该技术合成的不变量涉及多项式，指数，和多项式，即使在存在的任意控制流，包括任何组合的循环，分支，和（可能是非线性）递归。例如，它能够表明（i）合并排序所花费的时间是$O(n \log(n))$，（ii）Strassen算法所花费的时间是$O(n^{\log_2(7)})$。
英文摘要：
This paper is the confluence of two streams of ideas in the literature on generating numerical invariants, namely: (1) template-based methods, and (2) recurrence-based methods. A template-based method begins with a template that contains unknown quantities, and finds invariants that match the template by extracting and solving constraints on the unknowns. A disadvantage of template-based methods is that they require fixing the set of terms that may appear in an invariant in advance. This disadvantage is particularly prominent for non-linear invariant generation, because the user must supply maximum degrees on polynomials, bases for exponents, etc. On the other hand, recurrence-based methods are able to find sophisticated non-linear mathematical relations, including polynomials, exponentials, and logarithms, because such relations arise as the solutions to recurrences. However, a disadvantage of past recurrence-based invariant-generation methods is that they are primarily loop-based analyses: they use recurrences to relate the pre-state and post-state of a loop, so it is not obvious how to apply them to a recursive procedure, especially if the procedure is non-linearly recursive (e.g., a tree-traversal algorithm). In this paper, we combine these two approaches and obtain a technique that uses templates in which the unknowns are functions rather than numbers, and the constraints on the unknowns are recurrences. The technique synthesizes invariants involving polynomials, exponentials, and logarithms, even in the presence of arbitrary control-flow, including any combination of loops, branches, and (possibly non-linear) recursion. For instance, it is able to show that (i) the time taken by merge-sort is $O(n \log(n))$, and (ii) the time taken by Strassen's algorithm is $O(n^{\log_2(7)})$.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
