The Functional Essence of Imperative Binary Search Trees
- Anton Lorenzen ,
- Daan Leijen ,
- Wouter Swierstra ,
- Sam Lindley
MSR-TR-2023-28 |
Published by Microsoft
v4, Dec 27, 2023 (previously titled "A Functional Correspondence between Top-down and Bottom-up Tree Algorithms") This is an extended version of the PLDI'24 publication.
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.