BSTree

This structure defines balanced search trees, following the ideas of Stephen Adams as presented in "Functional Pearls: Efficient sets - a balancing act", Journal of Functional Programming, 3 (4), 553-561, October 1993. Search trees fulfill the property that every element in the left subtree is smaller, and every element of the right subtree is greater than the node value. Note that elements occur at most once in a balances search tree.

Signature of BSTree

List of Import References :
See BOOL
See DENOTATION
See Nat
See Option
See Pair
See Seq
See Tree

 SIGNATURE BSTree[data, < : data ** data -> bool]

$Date: 2010-09-30 18:24:17 +0200 (Do, 30. Sep 2010) $ ($Revision: 616 $)

IMPORT Nat ONLY nat
       Option[data] ONLY option
       Seq[data] ONLY seq

Parameter

data is the type of the elements of a tree. < is assumed to be an irreflexive total order.

SORT data
FUN < : data ** data -> bool

The Data Type of Balanced Search Trees

The constructor node is partial; it is undefined if the bs condition is not met or the resulting tree is not balanceds.

TYPE bstree == nil
               node(val: data, left: bstree, right: bstree)

Constructing a Tree from Datas

% convert the given data to an arbitrary tree containing these data

FUN % : data -> bstree
FUN % : data ** data -> bstree
FUN % : data ** data ** data -> bstree
FUN % : data ** data ** data ** data -> bstree
FUN % : data ** data ** data ** data ** data -> bstree
FUN % : data ** data ** data ** data ** data ** data -> bstree
FUN % : data ** data ** data ** data ** data ** data ** data -> bstree
FUN % : data ** data ** data ** data ** data ** data ** 
                                                data ** data -> bstree

Add or remove an element from a tree.

FUN incl excl : data ** bstree -> bstree

Constructing a Tree from a Function

iter(f, nil) returns nil.
iter(f, avail(d)) applies f to the data, giving a left and right value, and then returns a tree with data at the node, and a left and a right child recursively constructed from the result of f(d). The function aborts, if the tree condition is violated or the resulting tree is not balanced.

FUN iter : (data -> option[data] ** option[data]) ** option[data] -> 
                                                            bstree

Combining Trees

If one of the trees is empty, ++ is equivalent to incl. If this is not the case (d ++ (l, r)), val(l) < d < val(r) must hold.

FUN ++ : data ** bstree ** bstree -> bstree

Working on a Tree

The following functions replace the value (or the left child or the right child) of the first argument. These functions are undefined for empty trees and abort if the tree property is violated or the resulting tree is not balanced.

FUN :=_val : bstree ** data -> bstree
FUN :=_left : bstree ** bstree -> bstree
FUN :=_right : bstree ** bstree -> bstree

Accessing Datas in a Tree

min returns the minimal element of the tree

FUN min: bstree -> data

leftmost and rightmost return the "leftest" or "rightest" data of a tree. Both are undefined for empty trees.

FUN leftmost rightmost     : bstree -> data   

children and grandchildren return the values of the subtrees or the subtrees of the subtrees in arbitrary order. Both are always defined.

FUN children grandchildren : bstree -> seq[data]

level(i, t) returns all the elements found at depth i. level is always defined.

FUN level: nat ** bstree -> seq[data]

Return the values of the leaves from left to right.

FUN front: bstree -> seq[data]

Information About a Tree

Test, whether an element occurs in the tree

FUN in : data ** bstree -> bool

The number of nodes of the tree.

FUN #   : bstree -> nat 

Length of the longest path from root to a leaf. The depth of a leaf is 0, depth of an empty tree is undefined.

FUN depth: bstree -> nat

The number of leaves of the tree

FUN width: bstree -> nat

Are both children empty trees?

FUN leaf? : bstree -> bool

Check, whether a given predicate holds for one (exist?) or all (forall?) data, or return one value from the tree which fulfills the predicate, if one exists (find?).

FUN exist?      : (data -> bool) ** bstree -> bool
FUN forall?     : (data -> bool) ** bstree -> bool
FUN find?       : (data -> bool) ** bstree -> option[data]

Comparing trees

When supplied with a total irreflexive order, <(<) constitutes a valid total order on trees which may be used e.g. in instantiations of the set data type. {<} uses the order from the instantiation.

FUN < : (data ** data -> bool) -> bstree ** bstree -> bool
FUN {<} : bstree ** bstree -> bool

Likewise, =(=) is an equivalence relation (or an equality) on trees, if = is an equivalence (an equality) on datas.

FUN = : (data ** data -> bool) -> bstree ** bstree -> bool

Not for User Purpose

Do never use these functions, as these may change without notice!

IMPORT Tree[pair[data, nat]] ONLY tree
       Pair[data, nat] ONLY pair

FUN abs : tree[pair] -> bstree
FUN rep : bstree -> tree[pair]
FUN bstree? : tree[pair] -> bool
FUN bstree0? : tree[pair] -> bool

FUN balance: tree[pair] -> tree[pair]
FUN balanced? : tree[pair] -> bool

 
FUN lrotate: tree[pair] -> tree[pair]
FUN rrotate: tree[pair] -> tree[pair]

 
FUN dlrotate: tree[pair] -> tree[pair]
FUN drrotate: tree[pair] -> tree[pair]

next node: BSTreeCompare,
prev node: Subsystem Balanced Search Trees,
up to node: Subsystem Balanced Search Trees