Heap

The structures of this family define the abstract data type of heaps, which are built on top of binary trees. In a heap, the values of the children may not be smaller than that of the parent. Note, that these heaps are not based on arrays, and that we do not expect every node to have two children.

Signature of Heap

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

SIGNATURE Heap[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 heap. < is assumed to be an irreflexive total order.

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

The Data Type of Heaps

The constructor node is partial; it is undefined if the heap condition is not met.

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

Constructing a Heap from Datas

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

FUN % : data -> heap
FUN % : data ** data -> heap
FUN % : data ** data ** data -> heap
FUN % : data ** data ** data ** data -> heap
FUN % : data ** data ** data ** data ** data -> heap
FUN % : data ** data ** data ** data ** data ** data -> heap
FUN % : data ** data ** data ** data ** data ** data ** data -> heap
FUN % : data ** data ** data ** data ** data ** data ** data ** data -> heap

Add or remove an element from a heap.

FUN incl excl : data ** heap -> heap

Constructing a Heap 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 heap 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 heap condition is violated.

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

Combining Heaps

+ returns a heap which contains all elements of its arguments. No particular structure of the result should be assumed.

FUN + : heap ** heap -> heap

Working on a Heap

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 heap property is violated.

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

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

FUN swap: heap -> heap
FUN reflect: heap -> heap

extractMin returns the minimal element of the heap, and a new heap obtained by removing this element.

FUN extractMin: heap -> data ** heap

Accessing Datas in a Heap

min returns the minimal element of the heap

FUN min: heap -> data

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

FUN leftmost rightmost     : heap -> data   

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

FUN children grandchildren : heap -> seq[data]

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

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

Return the values of the leaves from left to right.

FUN front: heap -> seq[data]

Information About a Tree

Test, whether an element occurs in the heap

FUN in : data ** heap -> bool

The number of nodes of the heap.

FUN #   : heap -> nat   

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

FUN depth: heap -> nat

The number of leaves of the heap

FUN width: heap -> nat

Are both children empty heaps?

FUN leaf? : heap -> bool

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

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

Comparing heaps

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

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

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

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

next node: HeapCompare,
prev node: Subsystem Heaps,
up to node: Subsystem Heaps