The Functional Essence of Imperative Binary Search Trees

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. fip fun splay( accz, b, x, c ) match accz NodeR(a,y,NodeL(up,z,d)) -> splay( up, Node(a,y,b), x, Node(c,z,d) ) ... linear type system or reference counting.

• We present several novel functional algorithms for binary search tree insertion (Sections 2, 5 and 6) and provide benchmarks that show that their performance in the Koka language [Leijen 2021] is on par with the best known imperative implementations written in C and several times faster than the corresponding implementations in OCaml and Haskell (Section 7).

• To the best of our knowledge, we give the first formal machine-checked correctness proofs for the imperative insertion algorithms of move-to-root, splay, and zip trees, exactly as published in the original papers (Sections 4, 5, and 6 together with Appendix B). Moreover, this work also gives novel insights into the design of imperative algorithms:

• We show that bottom-up algorithms can be derived from a recursive specification using a defunctionalized CPS-transformation, while top-down algorithms can be derived using tail recursion modulo cons with product contexts (Section 2).

• We give new insights into splay trees by showing that they differ from move-to-root trees in only one balancing step, and characterizing how the bottom-up and top-down splay tree algorithms differ (Section 5).

• We derive an algorithm for top-down zip tree insertion which is simpler, but as efficient as the original algorithm given by Tarjan et al. [2021]. We are not aware of any previous bottom-up algorithm for zip tree insertion prior to the implementation given here (Section 6).

To introduce our techniques, we consider Move-to-root trees, independently described by both Stephenson [1980] and Allen and Munro [1978], which are a variation of simple binary search trees, where accessing a particular key ensures it moves to the tree's root. The are not suited for a practical implementation since they perform no restructuring, but through their simplicity can illustrate our key ideas.

All our examples in this paper are written in the Koka language [Leijen 2014] (v2.4.2) which implements all the features described in this paper (including first-class constructor contexts). We can declare a datatype for binary trees as:

type tree Node( left : tree, key : key, right : tree ) Leaf

We use an abstract type key for the keys stored in the tree but this is usually instantiated to be an int. The main operation on binary trees is the insert function that takes a tree and a key as its arguments. If the key is not yet in the tree, the insert function inserts it; otherwise no elements are inserted or deleted. Crucially, move-to-root trees ensure that the inserted key always ends up at the root of the resulting tree. The resulting tree should still be a binary search tree, hence we can specify the intended behaviour as follows:

fun insert( t : tree, k : key ) : tree Node( smaller(t,k), k, bigger(t,k) )

That is, each call to insert should return a new binary search tree storing the elements of t smaller than k, the key k, and the elements of t greater than k. To complete this specification, we still need to define smaller and bigger: fun smaller( t : tree, k : key ) : tree match t Node(l,x,r) -> if x < k then Node(l,x,smaller(r,k)) elif x > k then smaller(l,k) else l Leaf -> Leaf fun bigger( t : tree, k : key ) : tree match t Node(l,x,r) -> if x < k then bigger(r,k) elif x > k then Node(bigger(l,k),x,r) else r Leaf -> Leaf This specification captures the essence of move-to-root trees, but it is also quite inefficient, requiring two separate traversals of the input tree. We can obviously do better by fusing these two traversals into a single pass. As a first step, we merge smaller and bigger into a single function by inlining their definitions into the spe