# Linear Binary Search Trees

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]
```

Clearly, if the argument t of search ranges over a family of balanced trees, then the time-complexity of search is O(log(n)) (assuming that P is O(1)).

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]
```

The code immediately following the first recursive call to insertRT performs a right tree rotation. Let us use T(tl, x, tr) for a tree such that its root node contains the element x and its left and right children are tl and tr, respectively. Then a right rotation turns T(T(tll, xl, tlr), x, tr) into T(tll, xl, T(tlr, x, tr)). The code immediately following the second recursive call to insertRT performs a left tree rotation, which turns T(tl, x, T(trl, xr, trr)) into T(T(tl, x, tlr), xr, trr).

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
{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
{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]
```

Given 4 addresses L0, L1, L2 and L3, the type bstree_vt_cons_unfold(L0, L1, L2, l3) is for a tree node created by a call to bstree_vt_cons such that the node is located at L0 and the three arguments of bstree_vt_cons are located at L1, L2 and L3, and the proofs for the at-views associated with L1, L2 and L3 are put in the store for currently available proofs.

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
end else let
val () = tr := insertRT<a> (tr, x0, cmp)
in