Denotational recurrence extraction for amortized analysis
| Autor: | Joseph W. Cutler, Norman Danner, Daniel R. Licata |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
FOS: Computer and information sciences
Amortized analysis Computer Science - Programming Languages Correctness Theoretical computer science Relation (database) Computer science Semantics (computer science) 020207 software engineering 0102 computer and information sciences 02 engineering and technology Splay tree 01 natural sciences Denotational semantics 010201 computation theory & mathematics Bounded function 0202 electrical engineering electronic engineering information engineering F.3.2 Computer Science::Programming Languages F.3.1 Safety Risk Reliability and Quality Time complexity Software Programming Languages (cs.PL) |
| DOI: | 10.48550/arxiv.2006.15036 |
| Popis: | 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. Comment: To appear in ICFP 2020; formatting changes |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|