A binary search tree with respect to a given ordering is a binary tree such that the value stored in each node inside the tree is greater than or equal to those stored in the left child of the node and less than or equal to those stored in the right child of the node. Binary search trees are a common data structure for implementing finite maps.

A family of binary trees are said to be balanced if there is a fixed constant C (for the entire family) such that the ratio between the length of a longest path and the length of a shortest path is bounded by C for every tree in the family. For instance, common examples of balanced binary trees include AVL trees and red-black trees. Finite maps based on balanced binary search trees support guaranteed log-time insertion and deletion operations, that is, the time to complete such an operation is O(log(n)) in the worst case, where n is the size of the map.

In this section, I am to implement several basic operations on linear binary search trees, further illustrating some use of dataviewtypes. Let us first declare as follows a dataviewtype bstree_vt for linear binary (search) trees:

datavtype bstree_vt ( a:t@ype+, int ) = // bstree_vt | bstree_vt_nil (a, 0) of () | {n1,n2:nat} bstree_vt_cons (a, n1+n2+1) of (bstree_vt(a, n1), a, bstree_vt(a, n2)) // end of [bstree_vt]

Note that the integer index of bstree_vt captures the size information of a binary (search) tree. There are two constructors bstree_vt_cons and bstree_vt_nil associated with bstree_vt. It should be pointed out that the tree created by bstree_vt_nil is empty and thus not a leaf, which on the other hand is a node whose left and right children are both empty. As a simple example, the following function template size computes the size of a given tree:

fun{ a:t@ype } size{n:nat} .<n>. ( t: !bstree_vt (a, n) ) : int (n) = case+ t of | bstree_vt_nil () => 0 | bstree_vt_cons (tl, _, tr) => 1 + size (tl) + size (tr) // end of [size]

Assume that we have a binary search tree with repect to some ordering. If a predicate P on the elements stored in the tree possesses the property that P(x1) implies P(x2) whenever x1 is less than x2 (according to the ordering), then we can locate the least element in the tree that satisfies the predicate P by employing so-called binary search as is demonstrated in the following implementation of search:

fun{ a:t@ype } search {n:nat} .<n>. ( t: !bstree_vt (a, n), P: (&a) -<cloref> bool ) : Option_vt (a) = case+ t of | @bstree_vt_cons (tl, x, tr) => if P (x) then let val res = search (tl, P) val res = ( case+ res of | ~None_vt () => Some_vt (x) | _ => res ) : Option_vt (a) in fold@ (t); res end else let val res = search (tr, P) in fold@ (t); res end // end of [if] | @bstree_vt_nil () => (fold@ (t); None_vt ()) // end of [search]

Let us next see some code implementing an operation that inserts a given element into a binary search tree:

fun{ a:t@ype } insert{n:nat} .<n>. ( t: bstree_vt (a, n), x0: &a, cmp: cmp(a) ) : bstree_vt (a, n+1) = case+ t of | @bstree_vt_cons (tl, x, tr) => let val sgn = compare<a> (x0, x, cmp) in if sgn <= 0 then let val () = tl := insert (tl, x0, cmp) in fold@ (t); t end else let val () = tr := insert (tr, x0, cmp) in fold@ (t); t end (* end of [if] *) end // end of [bstree_vt_cons] | ~bstree_vt_nil () => bstree_vt_cons (bstree_vt_nil, x0, bstree_vt_nil) // end of [bstree_vt_nil] // end of [insert]

When inserting an element, the function template insert extends the given tree with a new leaf node containing the element, and this form of insertion is often referred to as leaf-insertion. There is another form of insertion often referred to as root-insertion, which always puts at the root position the new node containing the inserted element. The following function template insertRT is implemented to perform a standard root-insertion operation:

fun{ a:t@ype } insertRT{n:nat} .<n>. ( t: bstree_vt (a, n), x0: &a, cmp: cmp(a) ) : bstree_vt (a, n+1) = case+ t of | @bstree_vt_cons (tl, x, tr) => let val sgn = compare<a> (x0, x, cmp) in if sgn <= 0 then let val tl_ = insertRT (tl, x0, cmp) val+@bstree_vt_cons (_, tll, tlr) = tl_ val () = tl := tlr prval () = fold@ (t) val () = tlr := t in fold@ (tl_); tl_ end else let val tr_ = insertRT (tr, x0, cmp) val+@bstree_vt_cons (trl, _, trr) = tr_ val () = tr := trl prval () = fold@ (t) val () = trl := t in fold@ (tr_); tr_ end end // end of [bstree_vt_cons] | ~bstree_vt_nil () => bstree_vt_cons (bstree_vt_nil, x0, bstree_vt_nil) // end of [bstree_vt_nil] // end of [insertRT]

To further illustrate tree rotations, I present as follows two function templates lrotate and rrotate, which implement the left and right tree rotations, respectively:

fn{ a:t@ype } lrotate {l,l_tl,l_x,l_tr:addr} {nl,nr:int | nl >= 0; nr > 0} ( pf_tl: bstree_vt (a, nl) @ l_tl , pf_x: a @ l_x , pf_tr: bstree_vt (a, nr) @ l_tr | t: bstree_vt_cons_unfold (l, l_tl, l_x, l_tr) , p_tl: ptr l_tl , p_tr: ptr l_tr ) : bstree_vt (a, 1+nl+nr) = let val tr = !p_tr val+@bstree_vt_cons (trl, _, trr) = tr val () = !p_tr := trl prval () = fold@ (t); val () = trl := t in fold@ (tr); tr end // end of [lrotate] fn{ a:t@ype } rrotate {l,l_tl,l_x,l_tr:addr} {nl,nr:int | nl > 0; nr >= 0} ( pf_tl: bstree_vt (a, nl) @ l_tl , pf_x: a @ l_x , pf_tr: bstree_vt (a, nr) @ l_tr | t: bstree_vt_cons_unfold (l, l_tl, l_x, l_tr) , p_tl: ptr l_tl , p_tr: ptr l_tr ) : bstree_vt (a, 1+nl+nr) = let val tl = !p_tl val+@bstree_vt_cons (tll, x, tlr) = tl val () = !p_tl := tlr prval () = fold@ (t); val () = tlr := t in fold@ (tl); tl end // end of [rrotate]

The function template insertRT for root-insertion can now be implemented as follows by making direct use of lrotate and rrotate:

fun{ a:t@ype } insertRT {n:nat} .<n>. ( t: bstree_vt (a, n), x0: &a, cmp: cmp(a) ) : bstree_vt (a, n+1) = case+ t of | @bstree_vt_cons (tl, x, tr) => let prval pf_x = view@x prval pf_tl = view@tl prval pf_tr = view@tr val sgn = compare<a> (x0, x, cmp) in if sgn <= 0 then let val () = tl := insertRT<a> (tl, x0, cmp) in rrotate<a> (pf_tl, pf_x, pf_tr | t, addr@tl, addr@tr) end else let val () = tr := insertRT<a> (tr, x0, cmp) in lrotate<a> (pf_tl, pf_x, pf_tr | t, addr@tl, addr@tr) end (* end of [if] *) end // end of [bstree_vt_cons] | ~bstree_vt_nil () => bstree_vt_cons (bstree_vt_nil, x0, bstree_vt_nil) // end of [bstree_vt_nil] // end of [insertRT]

I would like to point out that neither insert nor insertRT is tail-recursive. While it is straightforward to give the former a tail-recursive implementation, there is no direct way to do the same to the latter. In order to implement root-insertion in a tail-recursive manner, we are in need of binary search trees with parental pointers (so as to allow each node to gain direct access to its parent), which can be done with dataviews but not with dataviewtypes.

Please find the entire code in this section plus some additional code for testing on-line.