- nil: {α : Type u} → Std.PairingHeapImp.Heap α
An empty forest, which has depth
0
. - node: {α : Type u} → α → Std.PairingHeapImp.Heap α → Std.PairingHeapImp.Heap α → Std.PairingHeapImp.Heap α
A forest consists of a root
a
, a forestchild
elements greater thana
, and another forestsibling
.
A Heap
is the nodes of the pairing heap.
Each node have two pointers: child
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
O(n)
. The number of elements in the heap.
Equations
- Std.PairingHeapImp.Heap.size Std.PairingHeapImp.Heap.nil = 0
- Std.PairingHeapImp.Heap.size (Std.PairingHeapImp.Heap.node a a_1 a_2) = Std.PairingHeapImp.Heap.size a_1 + 1 + Std.PairingHeapImp.Heap.size a_2
Instances For
A node containing a single element a
.
Instances For
O(1)
. Is the heap empty?
Instances For
O(1)
. Merge two heaps. Ignore siblings.
Instances For
Auxiliary for Heap.deleteMin
: merge the forest in pairs.
Equations
- One or more equations did not get rendered due to their size.
- Std.PairingHeapImp.Heap.combine le x = x
Instances For
O(1)
. Get the smallest element in the heap, including the passed in value a
.
Instances For
O(1)
. Get the smallest element in the heap, if it has an element.
Instances For
Amortized O(log n)
. Find and remove the the minimum element from the heap.
Instances For
Amortized O(log n)
. Get the tail of the pairing heap after removing the minimum element.
Instances For
Amortized O(log n)
. Remove the minimum element of the heap.
Instances For
- nil: ∀ {α : Type u_1}, Std.PairingHeapImp.Heap.NoSibling Std.PairingHeapImp.Heap.nil
An empty heap is no more than one tree.
- node: ∀ {α : Type u_1} (a : α) (c : Std.PairingHeapImp.Heap α),
Std.PairingHeapImp.Heap.NoSibling (Std.PairingHeapImp.Heap.node a c Std.PairingHeapImp.Heap.nil)
Or there is exactly one tree.
A predicate says there is no more than one tree.
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
- One or more equations did not get rendered due to their size.
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.
Instances For
O(n log n)
. Convert the heap to an array in increasing order.
Instances For
O(n log n)
. Convert the heap to a list in increasing order.
Instances For
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.PairingHeapImp.Heap.foldTreeM nil join Std.PairingHeapImp.Heap.nil = pure nil
Instances For
O(n)
. Fold a function over the tree structure to accumulate a value.
Instances For
O(n)
. Convert the heap to a list in arbitrary order.
Instances For
O(n)
. Convert the heap to an array in arbitrary order.
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)
Equations
- One or more equations did not get rendered due to their size.
- Std.PairingHeapImp.Heap.NodeWF le a Std.PairingHeapImp.Heap.nil = True
Instances For
- nil: ∀ {α : Type u_1} {le : α → α → Bool}, Std.PairingHeapImp.Heap.WF le Std.PairingHeapImp.Heap.nil
It is an empty heap.
- node: ∀ {α : Type u_1} {le : α → α → Bool} {a : α} {c : Std.PairingHeapImp.Heap α},
Std.PairingHeapImp.Heap.NodeWF le a c →
Std.PairingHeapImp.Heap.WF le (Std.PairingHeapImp.Heap.node a c Std.PairingHeapImp.Heap.nil)
There is exactly one tree and it is a
le
-min-heap.
The well formedness predicate for a pairing heap. It asserts that:
- There is no more than one tree.
- It is a
le
-min-heap (ifle
is well-behaved)
Instances For
A pairing heap is a data structure which supports the following primary operations:
insert : α → PairingHeap α → PairingHeap α
: add an element to the heapdeleteMin : PairingHeap α → Option (α × PairingHeap α)
: remove the minimum element from the heapmerge : PairingHeap α → PairingHeap α → PairingHeap α
: 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 PairingHeap
, insert
and merge
are O(1)
, deleteMin
is amortized O(log n)
.
Note that deleteMin
may be O(n)
in a single operation. So if you need an efficient
persistent priority queue, you should use other data structures with better worst-case time.
Instances For
O(1)
. Make a new empty pairing heap.
Instances For
O(1)
. Make a new empty pairing heap.
Instances For
O(1)
. Is the heap empty?
Instances For
O(n)
. The number of elements in the heap.
Instances For
O(1)
. Make a new heap containing a
.
Instances For
O(1)
. Merge the contents of two heaps.
Instances For
O(1)
. Add element a
to the given heap h
.
Instances For
O(n log n)
. Construct a heap from a list by inserting all the elements.
Instances For
O(n log n)
. Construct a heap from a list by inserting all the elements.
Instances For
Amortized O(log n)
. Remove and return the minimum element from the heap.
Instances For
O(1)
. Returns the smallest element in the heap, or none
if the heap is empty.
Instances For
O(1)
. Returns the smallest element in the heap, or panics if the heap is empty.
Instances For
O(1)
. Returns the smallest element in the heap, or default
if the heap is empty.
Instances For
Amortized O(log n)
. Removes the smallest element from the heap, or none
if the heap is empty.
Instances For
Amortized O(log n)
. Removes the smallest element from the heap, if possible.
Instances For
O(n log n)
. Convert the heap to a list in increasing order.
Instances For
O(n log n)
. Convert the heap to an array in increasing order.
Instances For
O(n)
. Convert the heap to a list in arbitrary order.
Instances For
O(n)
. Convert the heap to an array in arbitrary order.