Heap as array: extract minimum

Algorithmic problem: Bounded priority queue: extract minimum

Prerequisites:

Type of algorithm: loop

Auxiliary data:

1. A current index $k\in \mathbb{N}$.
2. An auxiliary index $k^{\prime }\in \mathbb{N}$

Abstract view

Invariant: Before and after each iteration:

1. The value of $N$ is one less than immediately before the call to this method; one heap item has been removed, namely the one that was at position $1$
2. The heap property is fulfilled for all heap items except for the one at index $k$ (for that one, the heap property may or may not be fulfilled).

Variant: $k$ is at least doubled.

Break condition: The heap property is fulfilled by $k$ (note that the heap property is trivially fulfilled by $k$ once $2\ast k>N$).

Induction basis

Abstract view:

1. Overwrite $TheHeap[1]$ by $TheHeap[N]$.
2. Decrease $N$ by one.
3. Update $Positions$ and $Unused$ accordingly.

Implementation:

1. Insert $TheHeap[1].ID$ in $Unused$.
2. Set $TheHeap[1].key:=TheHeap[N].key$.
3. Set $TheHeap[1].ID:=TheHeap[N].ID$.
4. Set $N:=N-1$.
5. Set $Positions[TheHeap[1].ID]:=1$.
6. Set $k:=1$.

Proof: Obvious.

Induction step

Abstract view:

1. If the current heap item fulfills the heap property, terminate the algorithm.
2. Otherwise, exchange the current heap item with one of its children, viz. the smaller one (ties arbitrarily broken). The index $k$ follows the heap item.

Implementation

1. If $2\ast k>N$, terminate the algorithm.
2. If $2\ast k+1>N$, set $k^{\prime }:=2\ast k$.
3. Otherwise, set
   1. $k^{\prime }:=2\ast k$ if $TheHeap[2k]\le TheHeap[2k+1]$;
   2. $k^{\prime }:=2\ast k+1$, otherwise.
4. If $TheHeap[k]\le TheHeap[k^{\prime }]$, terminate the algorithm.
5. Swap $Positions[TheHeap[k].ID]$ and $Positions[TheHeap[k^{\prime }].ID]$.
6. Swap $TheHeap[k].key$ and $TheHeap[k^{\prime }].key$.
7. Swap $TheHeap[k].ID$ and $TheHeap[k^{\prime }].ID$.
8. Set $k:=k^{\prime }$.

Correctness: Obviously, the heap item at the former position $k$ now fulfills the heap property, and the new $k$ is now the only index that does not necessarily fulfill it.

Complexity

Statement: The asymptotic complexity is logarithmic in the worst case. Proof: Obvious.