Introduction to Programming in ATS:
PrevChapter 15. Dataviewtypes as Linear DatatypesNext

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

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
        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.

PrevHomeNext
Example: Quick-Sort on Linear ListsUpTransition from Datatypes to Dataviewtypes