用于摊还分析的分母递归提取
Denotational recurrence extraction for amortized analysis
摘要：
分析函数式程序的时间复杂度的一种典型方法是提取一个递归式，该递归式用程序输入的大小来表示程序的运行时间，然后求解该递归式以获得一个大O界。为了使递归提取是组合的，还需要提取帮助函数输出大小的递归。以前的工作已经开发了技术，使用逻辑关系来陈述一个正式的正确性定理的一般递归提取翻译：一个程序是有界的递归时，操作成本是有界的提取成本，和输出值是有界的，根据一个值的边界关系定义的类型归纳，提取的大小。这以前的工作支持高阶函数，通过查看递归程序在一个递归演算，或作为数学实体的指称语义。在本文中，我们扩展这些技术，以支持摊还分析，其中成本重新安排从一个程序的一部分到另一个，以实现更精确的界限。我们给出了一种中间语言，在该语言中，程序可以根据银行家的摊还分析方法进行注释;这种语言有一个仿射类型系统，以确保信用不超过一次。我们给出了一个递归提取翻译这种语言的递归语言，一个简单的类型的成本类型的Alzida演算，并说明和证明一个绑定的逻辑关系表示这种翻译的正确性。递归语言在前序中具有指称语义，我们使用这种语义来解决递归问题，例如分析二进制计数器和展开树。
英文摘要：
A typical way of analyzing the time complexity of functional programs is to extract a recurrence expressing the running time of the program in terms of the size of its input, and then to solve the recurrence to obtain a big-O bound. For recurrence extraction to be compositional, it is also necessary to extract recurrences for the size of outputs of helper functions. Previous work has developed techniques for using logical relations to state a formal correctness theorem for a general recurrence extraction translation: a program is bounded by a recurrence when the operational cost is bounded by the extracted cost, and the output value is bounded, according to a value bounding relation defined by induction on types, by the extracted size. This previous work supports higher-order functions by viewing recurrences as programs in a lambda-calculus, or as mathematical entities in a denotational semantics thereof. In this paper, we extend these techniques to support amortized analysis, where costs are rearranged from one portion of a program to another to achieve more precise bounds. We give an intermediate language in which programs can be annotated according to the banker's method of amortized analysis; this language has an affine type system to ensure credits are not spent more than once. We give a recurrence extraction translation of this language into a recurrence language, a simply-typed lambda-calculus with a cost type, and state and prove a bounding logical relation expressing the correctness of this translation. The recurrence language has a denotational semantics in preorders, and we use this semantics to solve recurrences, e.g analyzing binary counters and splay trees.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
