The Functional Essence of Imperative Binary Search Trees

Anton Lorenzen, Daan Leijen, Wouter Swierstra, Sam Lindley

Research output: Contribution to journalArticleAcademicpeer-review

Abstract

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
Pages (from-to)518-542
Number of pages168
JournalProceedings of the ACM on Programming Languages
Volume8
Issue numberPLDI
DOIs
Publication statusPublished - 1 Jun 2024

Keywords

  • FBIP
  • FIP
  • Splay Trees
  • Tail Recursion Modulo Cons
  • Zip Trees
  • Zippers

Fingerprint

Dive into the research topics of 'The Functional Essence of Imperative Binary Search Trees'. Together they form a unique fingerprint.

Cite this