Type-based analysis of logarithmic amortised complexity. (19th June 2022)

• Record Type: Journal Article
• Authors: Hofmann, Martin; Leutgeb, Lorenz; Obwaller, David; Moser, Georg; Zuleger, Florian
• Is Part Of: Mathematical structures in computer science. Volume 32:Number 6(2022)
• Page Start: 794
• Page End: 826
• Publication Date: 2022-06-19
• Subjects: Analysis of algorithms -- amortised resource analysis -- functional programming -- self-adjusting data structures -- automation; Computer science -- Mathematics -- Periodicals; 004.015105
• DOI: 10.1017/S0960129521000232
• Languages: English
• ISSNs: 0960-1295

Abstract

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.