论文标题
模板和复发：更好地在一起
Templates and Recurrences: Better Together
论文作者
论文摘要
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.基于模板的方法从包含未知数量的模板开始，并通过在未知数上提取和求解约束来找到与模板匹配的不变性。基于模板方法的缺点是，它们需要修复可能事先出现在不变的术语中的一组。这种缺点对于非线性不变的生成特别突出，因为用户必须在多项式上提供最大程度的学位，指数的基础等。另一方面，基于复发的方法能够找到复杂的非线性数学关系，包括多项式，指数，指数性，指数性，和差异，因为这种关系的关系是这样的。 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).在本文中，我们结合了这两种方法，并获得了一种使用模板，其中未知数是函数而不是数字，而对未知数的约束是复发。该技术合成了涉及多项式，指数和对数的不变性，即使在有任意控制流的存在下，包括环路，分支，分支和（可能是非线性）递归的任何组合。例如，它能够证明（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)})$.
