The functional essence of imperative binary search trees

Anton Lorenzen, Daan Leijen, Wouter Swierstra, Sam Lindley

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

Algorithms on restructuring binary search trees are typically presented in imperative pseudocode. Understandably so, as their performance relies on in-place execution, rather than the repeated allocation of fresh nodes in memory. Unfortunately, these imperative algorithms are notoriously difficult to verify as their loop invariants must relate the unfinished tree fragments being rebalanced. This paper presents several novel functional algorithms for accessing and inserting elements in a restructuring binary search tree that are as fast as their imperative counterparts; yet the correctness of these functional algorithms is established using a simple inductive argument. For each data structure, move-to-root, splay, and zip trees, this paper describes both a bottom-up algorithm using zippers and a top-down algorithm using a novel first-class constructor context primitive. The functional and imperative algorithms are equivalent: we mechanise the proofs establishing this in the Coq proof assistant using the Iris framework. This yields a first fully verified implementation of well known algorithms on binary search trees with performance on par with the fastest implementations in C.
Original languageEnglish
Number of pages48
JournalProceedings of the ACM on Programming Languages
Volume8 (PLDI)
Publication statusAccepted/In press - 1 Apr 2024
Event45th ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI) - Copenhagen, Denmark
Duration: 24 Jun 202428 Jun 2024
Conference number: 45

Fingerprint

Dive into the research topics of 'The functional essence of imperative binary search trees'. Together they form a unique fingerprint.

Cite this