next node: TreeCompare,
prev node: IndexingOfTrees,
up to node: Subsystem Binary Trees


Tree

The structures of this family define the abstract data type of plain vanilla binary trees, in the following shortly called trees. More elaborate trees like heaps, search trees, avl trees and so on are then built on top of this structure.

Signature of Tree

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

SIGNATURE Tree[data]

$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

SORT data

The Data Type of Trees

Note that every node which carries data has a left and a right child. We call the nil trees empty and nodes whose left and right children are outer leaves are called leaves.

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

Constructing a Tree from Datas

% converts the given data to a leaf.

FUN %   : data -> tree

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

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

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

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

swap exchanges the left child with the right, reflect does this recursively and so mirrors the whole tree.

FUN swap: tree -> tree
FUN reflect: tree -> tree

lrotate swaps one of the subtrees from the right child to the left like this: [/x, A, [/y, B, C\]\] becomes [/y, [/x, A, B\], C\], where x, y are node values and A, B, C are whole subtrees; rrotate is just the opposite. lrotate aborts, if the right child is empty, rrotate, if the left child is empty.

 
FUN lrotate: tree -> tree
FUN rrotate: tree -> tree

Accessing Datas in a Tree

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

FUN leftmost rightmost     : tree -> 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 : tree -> seq[data]

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

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

Return the values of the leaves from left to right.

FUN front: tree -> seq[data]

Information About a Tree

The number of nodes of the tree.

FUN #   : tree -> 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: tree -> nat

The number of leaves of tree

FUN width: tree -> nat

Are both children empty trees?

FUN leaf? : tree -> 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) ** tree -> bool
FUN forall?     : (data -> bool) ** tree -> bool
FUN find?       : (data -> bool) ** tree -> option[data]

Comparing trees

When supplied with a total irreflexive order, <(<) consitutes a valid total order an trees which may be used e.g. in instantiations of the set data type.

FUN < : (data ** data -> bool) -> tree ** tree -> bool

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

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


next node: TreeCompare,
prev node: IndexingOfTrees,
up to node: Subsystem Binary Trees