A HeapNode
is one of the internal nodes of the binomial heap.
It is always a perfect binary tree, with the depth of the tree stored in the Heap
.
However the interpretation of the two pointers is different: we view the child
as going to the first child of this node, and sibling
goes to the next sibling
of this tree. So it actually encodes a forest where each node has children
node.child
, node.child.sibling
, node.child.sibling.sibling
, etc.
Each edge in this forest denotes a le a b
relation that has been checked, so
the root is smaller than everything else under it.
- nil
{α : Type u}
: HeapNode α
An empty forest, which has depth
0
. - node
{α : Type u}
(a : α)
(child sibling : HeapNode α)
: HeapNode α
A forest of rank
r + 1
consists of a roota
, a forestchild
of rankr
elements greater thana
, and another forestsibling
of rankr
.
Instances For
The "real size" of the node, counting up how many values of type α
are stored.
This is O(n)
and is intended mainly for specification purposes.
For a well formed HeapNode
the size is always 2^n - 1
where n
is the depth.
Equations
Instances For
A node containing a single element a
.
Equations
Instances For
O(log n)
. The rank, or the number of trees in the forest.
It is also the depth of the forest.
Equations
Instances For
O(log n)
. The number of elements in the heap.
Equations
Instances For
O(1)
. Is the heap empty?
Equations
Instances For
O(1)
. The heap containing a single value a
.
Equations
Instances For
O(1)
. Auxiliary for Heap.merge
: Is the minimum rank in Heap
strictly larger than n
?
Equations
Instances For
O(log n)
. The number of trees in the forest.
Equations
Instances For
O(1)
. Auxiliary for Heap.merge
: combines two heap nodes of the same rank
into one with the next larger rank.
Equations
Instances For
O(log n)
. Get the smallest element in the heap, including the passed in value a
.
Equations
Instances For
The return type of FindMin
, which encodes various quantities needed to
reconstruct the tree in deleteMin
.
The list of elements prior to the minimum element, encoded as a "difference list".
- val : α
The minimum element.
- node : HeapNode α
The children of the minimum element.
- next : Heap α
The forest after the minimum element.
Instances For
O(n log n)
. Monadic fold over the elements of a heap in increasing order,
by repeatedly pulling the minimum element out of the heap.
Equations
Instances For
O(n)
. Fold a function over the tree structure to accumulate a value.
Equations
Instances For
O(n)
. Convert the heap to a list in arbitrary order.
Equations
Instances For
O(n)
. Convert the heap to an array in arbitrary order.
Equations
Instances For
The well formedness predicate for a heap node. It asserts that:
- If
a
is added at the top to make the forest into a tree, the resulting tree is ale
-min-heap (ifle
is well-behaved) - When interpreting
child
andsibling
as left and right children of a binary tree, it is a perfect binary tree with depthr
Equations
Instances For
The well formedness predicate for a binomial heap. It asserts that:
- It consists of a list of well formed trees with the specified ranks
- The ranks are in strictly increasing order, and all are at least
n
Equations
Instances For
The well formedness predicate for a FindMin
value.
This is not actually a predicate, as it contains an additional data value
rank
corresponding to the rank of the returned node, which is omitted from findMin
.
- rank : Nat
The rank of the minimum element
- node : HeapNode.WF le res.val res.node self.rank
Instances For
The conditions under which findMin
is well-formed.
Equations
Instances For
A binomial heap is a data structure which supports the following primary operations:
insert : α → BinomialHeap α → BinomialHeap α
: add an element to the heapdeleteMin : BinomialHeap α → Option (α × BinomialHeap α)
: remove the minimum element from the heapmerge : BinomialHeap α → BinomialHeap α → BinomialHeap α
: combine two heaps
The first two operations are known as a "priority queue", so this could be called
a "mergeable priority queue". The standard choice for a priority queue is a binary heap,
which supports insert
and deleteMin
in O(log n)
, but merge
is O(n)
.
With a BinomialHeap
, all three operations are O(log n)
.
Equations
Instances For
O(1)
. Make a new empty binomial heap.
Equations
Instances For
O(1)
. Make a new empty binomial heap.
Equations
Instances For
Equations
Equations
O(1)
. Is the heap empty?
Equations
Instances For
O(log n)
. The number of elements in the heap.
Equations
Instances For
O(1)
. Make a new heap containing a
.
Equations
Instances For
O(log n)
. Merge the contents of two heaps.
Equations
Instances For
O(log n)
. Add element a
to the given heap h
.
Equations
Instances For
O(n log n)
. Construct a heap from a list by inserting all the elements.
Equations
Instances For
O(n log n)
. Construct a heap from a list by inserting all the elements.
Equations
Instances For
O(log n)
. Remove and return the minimum element from the heap.
Equations
Instances For
Equations
O(n log n)
. Implementation of for x in (b : BinomialHeap α le) ...
notation,
which iterates over the elements in the heap in increasing order.
Equations
Instances For
Equations
O(log n)
. Returns the smallest element in the heap, or none
if the heap is empty.
Equations
Instances For
O(log n)
. Returns the smallest element in the heap, or panics if the heap is empty.
Equations
Instances For
O(log n)
. Returns the smallest element in the heap, or default
if the heap is empty.
Equations
Instances For
O(log n)
. Removes the smallest element from the heap, or none
if the heap is empty.
Equations
Instances For
O(log n)
. Removes the smallest element from the heap, if possible.
Equations
Instances For
O(n log n)
. Monadic fold over the elements of a heap in increasing order,
by repeatedly pulling the minimum element out of the heap.
Equations
Instances For
O(n log n)
. Fold over the elements of a heap in increasing order,
by repeatedly pulling the minimum element out of the heap.
Equations
Instances For
O(n log n)
. Convert the heap to a list in increasing order.
Equations
Instances For
O(n log n)
. Convert the heap to an array in increasing order.
Equations
Instances For
O(n)
. Convert the heap to a list in arbitrary order.
Equations
Instances For
O(n)
. Convert the heap to an array in arbitrary order.