Automated Amortised Analysis of Skew Heaps and Leftist Heaps (Extended Version)

TL;DR

This paper presents a modular, automated type inference system for analyzing the amortised complexity of functional skew and leftist heaps, extending previous work with new techniques and supporting all known potential functions.

Contribution

It introduces a generic type system and enhanced inference algorithms enabling precise, modular, and automated analysis of skew and leftist heaps, surpassing prior methods.

Findings

Successfully analyzes skew heaps and leftist heaps using known potential functions.

Extends the ATLAS system with new techniques for path-sensitive reasoning and invariants.

Provides a modular, Haskell-implemented framework for automated amortised analysis.

Abstract

We study the fully automated amortised analysis of purely functional data structures like skew heaps, as well as weight- and rank-biased leftist heaps. For that we generalise earlier works on automated amortised resource analysis by developing a type inference based approach with a generic type system. This allows for modular reasoning and the inference of precise and optimal cost bounds. More specifically, we extend the work on the ATLAS system by Leutgeb et al. which was developed to cover the analysis of splay trees and some closely related data structures. To enable the analysis of skew heaps, however, and the even more challenging (amortised) analysis of leftist heaps, we have developed a range of new techniques for type-based automated analysis. By introducing a generic type system we allow for arbitrary (classes of) potential functions, compared to the use of hard-coded potential functions in ATLAS, which we have implemented in Haskell in an entirely modular way. We have also greatly enhanced the existing type inference algorithm by extensions in multiple directions, including path-sensitive reasoning, data structure invariants, and template parameters for piecewise defined potential functions. We show how our newly developed system supports the use of all known potential functions for analysing skew heaps and leftist heaps, confirming the known bounds.