渐近资源约束综合
Synthesis with Asymptotic Resource Bounds
摘要：
我们提出了一种方法来合成递归函数，满足功能规范和渐近资源界。先前的方法与资源指标的合成需要用户指定一个具体的表达式，精确地描述资源的使用，而我们的方法使用大O符号来指定渐近的资源使用。我们的方法可以合成程序复杂的资源界限，如排序功能，具有复杂性O（nlog（n））。我们的合成过程中使用的类型系统，是能够分配一个渐近复杂性的条款，并可以跟踪函数的递归关系。这些类型规则被算法分析中使用的定理证明是合理的，例如Master Theorem和Akra-Bazzi方法。我们实现了我们的方法作为一个扩展之前的基于类型的合成工作。我们的工具，SynPlexity，能够合成复杂的分而治之的程序，不能合成以前的求解器。
英文摘要：
We present a method for synthesizing recursive functions that satisfy both a functional specification and an asymptotic resource bound. Prior methods for synthesis with a resource metric require the user to specify a concrete expression exactly describing resource usage, whereas our method uses big-O notation to specify the asymptotic resource usage. Our method can synthesize programs with complex resource bounds, such as a sort function that has complexity O(nlog(n)). Our synthesis procedure uses a type system that is able to assign an asymptotic complexity to terms, and can track recurrence relations of functions. These typing rules are justified by theorems used in analysis of algorithms, such as the Master Theorem and the Akra-Bazzi method. We implemented our method as an extension of prior type-based synthesis work. Our tool, SynPlexity, was able to synthesize complex divide-and-conquer programs that cannot be synthesized by prior solvers.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
