Type-based analysis of logarithmic amortised complexity

Hofmann, Martin; Leutgeb, Lorenz; Obwaller, David; Moser, Georg und Zuleger, Florian (2022): Type-based analysis of logarithmic amortised complexity. In: Mathematical Structures in Computer Science, Bd. 32, Nr. 6, PII S0960129521000232: S. 794-826

Abstract

We introduce a novel amortised resource analysis couched in a type-and-effect system. Our analysis is formulated in terms of the physicist's method of amortised analysis and is potentialbased. The type system makes use of logarithmic potential functions and is the first such system to exhibit logarithmic amortised complexity. With our approach, we target the automated analysis of self-adjusting data structures, like splay trees, which so far have only manually been analysed in the literature. In particular, we have implemented a semi-automated prototype, which successfully analyses the zig-zig case of splaying, once the type annotations are fixed.

• Dokumententyp: Zeitschriftenartikel
• Fakultät: Mathematik, Informatik und Statistik > Informatik
• Themengebiete: 000 Informatik, Informationswissenschaft, allgemeine Werke > 004 Informatik
• ISSN: 0960-1295
• Sprache: Englisch