- nil: {α : Type u} → Std.BinomialHeapImp.HeapNode α
An empty forest, which has depth
0
. - node: {α : Type u} → α → Std.BinomialHeapImp.HeapNode α → Std.BinomialHeapImp.HeapNode α → Std.BinomialHeapImp.HeapNode α
A forest of rank
r + 1
consists of a roota
, a forestchild
of rankr
elements greater thana
, and another forestsibling
of rankr
.
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.
Instances For
Equations
- Std.BinomialHeapImp.instReprHeapNode = { reprPrec := Std.BinomialHeapImp.reprHeapNode✝ }
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
- Std.BinomialHeapImp.HeapNode.realSize Std.BinomialHeapImp.HeapNode.nil = 0
- Std.BinomialHeapImp.HeapNode.realSize (Std.BinomialHeapImp.HeapNode.node a a_1 a_2) = Std.BinomialHeapImp.HeapNode.realSize a_1 + 1 + Std.BinomialHeapImp.HeapNode.realSize a_2
A node containing a single element a
.
Equations
- Std.BinomialHeapImp.HeapNode.singleton a = Std.BinomialHeapImp.HeapNode.node a Std.BinomialHeapImp.HeapNode.nil Std.BinomialHeapImp.HeapNode.nil
O(log n)
. The rank, or the number of trees in the forest.
It is also the depth of the forest.
Computes s.rank + r
Equations
- Std.BinomialHeapImp.HeapNode.rankTR.go Std.BinomialHeapImp.HeapNode.nil x = x
- Std.BinomialHeapImp.HeapNode.rankTR.go (Std.BinomialHeapImp.HeapNode.node a child s) x = Std.BinomialHeapImp.HeapNode.rankTR.go s (x + 1)
- nil: {α : Type u} → Std.BinomialHeapImp.Heap α
An empty heap.
- cons: {α : Type u} → Nat → α → Std.BinomialHeapImp.HeapNode α → Std.BinomialHeapImp.Heap α → Std.BinomialHeapImp.Heap α
A cons node contains a tree of root
val
, childrennode
and rankrank
, and thennext
which is the rest of the forest.
A Heap
is the top level structure in a binomial heap.
It consists of a forest of HeapNode
s with strictly increasing ranks.
Instances For
Equations
- Std.BinomialHeapImp.instReprHeap = { reprPrec := Std.BinomialHeapImp.reprHeap✝ }
O(n)
. The "real size" of the heap, counting up how many values of type α
are stored.
This is intended mainly for specification purposes.
Prefer Heap.size
, which is the same for well formed heaps.
Equations
- Std.BinomialHeapImp.Heap.realSize Std.BinomialHeapImp.Heap.nil = 0
- Std.BinomialHeapImp.Heap.realSize (Std.BinomialHeapImp.Heap.cons a a_1 a_2 a_3) = Std.BinomialHeapImp.HeapNode.realSize a_2 + 1 + Std.BinomialHeapImp.Heap.realSize a_3
O(log n)
. The number of elements in the heap.
Equations
- Std.BinomialHeapImp.Heap.size x = match x with | Std.BinomialHeapImp.Heap.nil => 0 | Std.BinomialHeapImp.Heap.cons r val node s => 1 <<< r + Std.BinomialHeapImp.Heap.realSize s
O(1)
. Is the heap empty?
Equations
- Std.BinomialHeapImp.Heap.isEmpty x = match x with | Std.BinomialHeapImp.Heap.nil => true | x => false
O(1)
. The heap containing a single value a
.
Equations
- Std.BinomialHeapImp.Heap.singleton a = Std.BinomialHeapImp.Heap.cons 0 a Std.BinomialHeapImp.HeapNode.nil Std.BinomialHeapImp.Heap.nil
O(1)
. Auxiliary for Heap.merge
: Is the minimum rank in Heap
strictly larger than n
?
Equations
- Std.BinomialHeapImp.Heap.rankGT x x = match x, x with | Std.BinomialHeapImp.Heap.nil, x => True | Std.BinomialHeapImp.Heap.cons r val node next, n => n < r
Equations
- One or more equations did not get rendered due to their size.
O(log n)
. The number of trees in the forest.
Equations
- Std.BinomialHeapImp.Heap.length Std.BinomialHeapImp.Heap.nil = 0
- Std.BinomialHeapImp.Heap.length (Std.BinomialHeapImp.Heap.cons a a_1 a_2 a_3) = Std.BinomialHeapImp.Heap.length a_3 + 1
O(1)
. Auxiliary for Heap.merge
: combines two heap nodes of the same rank
into one with the next larger rank.
Equations
- Std.BinomialHeapImp.combine le a₁ a₂ n₁ n₂ = if le a₁ a₂ = true then (a₁, Std.BinomialHeapImp.HeapNode.node a₂ n₂ n₁) else (a₂, Std.BinomialHeapImp.HeapNode.node a₁ n₁ n₂)
Merge two forests of binomial trees. The forests are assumed to be ordered
by rank and merge
maintains this invariant.
Equations
- One or more equations did not get rendered due to their size.
- Std.BinomialHeapImp.Heap.merge le Std.BinomialHeapImp.Heap.nil x = x
- Std.BinomialHeapImp.Heap.merge le x Std.BinomialHeapImp.Heap.nil = x
O(log n)
. Convert a HeapNode
to a Heap
by reversing the order of the nodes
along the sibling
spine.
Equations
- Std.BinomialHeapImp.HeapNode.toHeap s = Std.BinomialHeapImp.HeapNode.toHeap.go s (Std.BinomialHeapImp.HeapNode.rankTR s) Std.BinomialHeapImp.Heap.nil
Computes s.toHeap ++ res
tail-recursively, assuming n = s.rank
.
Equations
- Std.BinomialHeapImp.HeapNode.toHeap.go Std.BinomialHeapImp.HeapNode.nil x x = x
- Std.BinomialHeapImp.HeapNode.toHeap.go (Std.BinomialHeapImp.HeapNode.node a c s) x x = Std.BinomialHeapImp.HeapNode.toHeap.go s (x - 1) (Std.BinomialHeapImp.Heap.cons (x - 1) a c x)
O(log n)
. Get the smallest element in the heap, including the passed in value a
.
Equations
- Std.BinomialHeapImp.Heap.headD le a Std.BinomialHeapImp.Heap.nil = a
- Std.BinomialHeapImp.Heap.headD le a (Std.BinomialHeapImp.Heap.cons a_1 a_2 a_3 a_4) = Std.BinomialHeapImp.Heap.headD le (if le a a_2 = true then a else a_2) a_4
O(log n)
. Get the smallest element in the heap, if it has an element.
Equations
- Std.BinomialHeapImp.Heap.head? le x = match x with | Std.BinomialHeapImp.Heap.nil => none | Std.BinomialHeapImp.Heap.cons rank h node hs => some (Std.BinomialHeapImp.Heap.headD le h hs)
The list of elements prior to the minimum element, encoded as a "difference list".
before : Std.BinomialHeapImp.Heap α → Std.BinomialHeapImp.Heap αThe minimum element.
val : αThe children of the minimum element.
node : Std.BinomialHeapImp.HeapNode αThe forest after the minimum element.
next : Std.BinomialHeapImp.Heap α
The return type of FindMin
, which encodes various quantities needed to
reconstruct the tree in deleteMin
.
Instances For
O(log n)
. Find the minimum element, and return a data structure FindMin
with information
needed to reconstruct the rest of the binomial heap.
Equations
- One or more equations did not get rendered due to their size.
- Std.BinomialHeapImp.Heap.findMin le k Std.BinomialHeapImp.Heap.nil x = x
O(log n)
. Find and remove the the minimum element from the binomial heap.
Equations
- One or more equations did not get rendered due to their size.
O(log n)
. Get the tail of the binomial heap after removing the minimum element.
Equations
- Std.BinomialHeapImp.Heap.tail? le h = Option.map (fun x => x.snd) (Std.BinomialHeapImp.Heap.deleteMin le h)
O(log n)
. Remove the minimum element of the heap.
Equations
- Std.BinomialHeapImp.Heap.tail le h = Option.getD (Std.BinomialHeapImp.Heap.tail? le h) Std.BinomialHeapImp.Heap.nil
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
- One or more equations did not get rendered due to their size.
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
- Std.BinomialHeapImp.Heap.fold le s init f = Id.run (Std.BinomialHeapImp.Heap.foldM le s init f)
O(n log n)
. Convert the heap to an array in increasing order.
Equations
- Std.BinomialHeapImp.Heap.toArray le s = Std.BinomialHeapImp.Heap.fold le s #[] Array.push
O(n log n)
. Convert the heap to a list in increasing order.
Equations
O(n)
. Fold a monadic function over the tree structure to accumulate a value.
Equations
- One or more equations did not get rendered due to their size.
- Std.BinomialHeapImp.HeapNode.foldTreeM nil join Std.BinomialHeapImp.HeapNode.nil = pure nil
O(n)
. Fold a monadic function over the tree structure to accumulate a value.
Equations
- One or more equations did not get rendered due to their size.
- Std.BinomialHeapImp.Heap.foldTreeM nil join Std.BinomialHeapImp.Heap.nil = pure nil
O(n)
. Fold a function over the tree structure to accumulate a value.
Equations
- Std.BinomialHeapImp.Heap.foldTree nil join s = Id.run (Std.BinomialHeapImp.Heap.foldTreeM nil join s)
O(n)
. Convert the heap to a list in arbitrary order.
Equations
- Std.BinomialHeapImp.Heap.toListUnordered s = Std.BinomialHeapImp.Heap.foldTree id (fun a c s l => a :: c (s l)) s []
O(n)
. Convert the heap to an array in arbitrary order.
Equations
- Std.BinomialHeapImp.Heap.toArrayUnordered s = Std.BinomialHeapImp.Heap.foldTree id (fun a c s r => s (c (Array.push r a))) s #[]
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
- One or more equations did not get rendered due to their size.
- Std.BinomialHeapImp.HeapNode.WellFormed le a Std.BinomialHeapImp.HeapNode.nil x = (x = 0)
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
- One or more equations did not get rendered due to their size.
- Std.BinomialHeapImp.Heap.WellFormed le n Std.BinomialHeapImp.Heap.nil = True
O(log n)
. The rank, or the number of trees in the forest.
This is the same as rankTR
but it is not tail recursive.
Equations
- Std.BinomialHeapImp.HeapNode.rank Std.BinomialHeapImp.HeapNode.nil = 0
- Std.BinomialHeapImp.HeapNode.rank (Std.BinomialHeapImp.HeapNode.node a a_1 a_2) = Std.BinomialHeapImp.HeapNode.rank a_2 + 1
The rank of the minimum element
rank : Natbefore
is a difference list which can be appended to a binomial heap with ranks at leastrank
to produce another well formed heap.before : ∀ {s : Std.BinomialHeapImp.Heap α}, Std.BinomialHeapImp.Heap.WellFormed le rank s → Std.BinomialHeapImp.Heap.WellFormed le 0 (Std.BinomialHeapImp.FindMin.before res s)- node : Std.BinomialHeapImp.HeapNode.WellFormed le res.val res.node rank
next
is a binomial heap with ranks aboverank + 1
.next : Std.BinomialHeapImp.Heap.WellFormed le (rank + 1) res.next
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
.
Instances For
A binomial heap is a data structure which supports the following primary operations:
insert : α → BinomialHeap α → BinomialHeap α→ BinomialHeap α → BinomialHeap α→ BinomialHeap α
: add an element to the heapdeleteMin : BinomialHeap α → Option (α × BinomialHeap α)→ Option (α × BinomialHeap α)× BinomialHeap α)
: remove the minimum element from the heapmerge : BinomialHeap α → BinomialHeap α → BinomialHeap α→ 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
- Std.BinomialHeap α le = { h // Std.BinomialHeapImp.Heap.WellFormed le 0 h }
O(1)
. Make a new empty binomial heap.
Equations
- Std.mkBinomialHeap α le = { val := Std.BinomialHeapImp.Heap.nil, property := (_ : Std.BinomialHeapImp.Heap.WellFormed le 0 Std.BinomialHeapImp.Heap.nil) }
O(1)
. Make a new empty binomial heap.
Equations
- Std.BinomialHeap.empty = Std.mkBinomialHeap α le
Equations
- Std.BinomialHeap.instInhabitedBinomialHeap = { default := Std.BinomialHeap.empty }
O(1)
. Is the heap empty?
Equations
O(log n)
. The number of elements in the heap.
Equations
O(1)
. Make a new heap containing a
.
Equations
- Std.BinomialHeap.singleton a = { val := Std.BinomialHeapImp.Heap.singleton a, property := (_ : Std.BinomialHeapImp.Heap.WellFormed le 0 (Std.BinomialHeapImp.Heap.singleton a)) }
O(log n)
. Merge the contents of two heaps.
Equations
- One or more equations did not get rendered due to their size.
O(log n)
. Add element a
to the given heap h
.
Equations
O(n log n)
. Construct a heap from a list by inserting all the elements.
Equations
- Std.BinomialHeap.ofList le as = List.foldl (flip Std.BinomialHeap.insert) Std.BinomialHeap.empty as
O(n log n)
. Construct a heap from a list by inserting all the elements.
Equations
- Std.BinomialHeap.ofArray le as = Array.foldl (flip Std.BinomialHeap.insert) Std.BinomialHeap.empty as 0 (Array.size as)
O(log n)
. Remove and return the minimum element from the heap.
Equations
- One or more equations did not get rendered due to their size.
O(log n)
. Returns the smallest element in the heap, or none
if the heap is empty.
Equations
O(log n)
. Returns the smallest element in the heap, or panics if the heap is empty.
Equations
O(log n)
. Returns the smallest element in the heap, or default
if the heap is empty.
Equations
- Std.BinomialHeap.headI b = Option.getD (Std.BinomialHeap.head? b) default
O(log n)
. Removes the smallest element from the heap, or none
if the heap is empty.
Equations
- One or more equations did not get rendered due to their size.
O(log n)
. Removes the smallest element from the heap, if possible.
Equations
- Std.BinomialHeap.tail b = { val := Std.BinomialHeapImp.Heap.tail le b.val, property := (_ : Std.BinomialHeapImp.Heap.WellFormed le 0 (Std.BinomialHeapImp.Heap.tail le b.val)) }
O(n log n)
. Convert the heap to a list in increasing order.
Equations
O(n log n)
. Convert the heap to an array in increasing order.
Equations
O(n)
. Convert the heap to a list in arbitrary order.
Equations
O(n)
. Convert the heap to an array in arbitrary order.