Heap as array: decrease key

Algorithmic problem: Bounded priority queue: decrease key

Prerequisites:

Type of algorithm: loop

Auxiliary data:

1. A current index [math]\displaystyle{ k \in \mathbb{N} }[/math].
2. An auxiliary index [math]\displaystyle{ k' \in \mathbb{N} }[/math].

Abstract view

Invariant: Before and after each iteration:

1. The heap property is fulfilled for all heap items except for the one at position [math]\displaystyle{ \lfloor k/2 \rfloor }[/math] (for that one, the heap property may or may not be fulfilled).

Variant: [math]\displaystyle{ k }[/math] is at least halved.

Break condition: One of the following two conditions is fulfilled:

1. either it is [math]\displaystyle{ k = 1 }[/math];
2. or, otherwise, the heap property is fulfilled by the heap item at position [math]\displaystyle{ \lfloor k/2 \rfloor }[/math].

Induction basis

Abstract view: The heap item is identified and its key is replaced by [math]\displaystyle{ x }[/math].

Implementation:

1. Set [math]\displaystyle{ k := Positions[ID] }[/math].
2. Set [math]\displaystyle{ TheHeap[k].key := x }[/math].

Proof: Nothing to show.

Induction step

Abstract view:

1. If the current heap item has no parent or the parent fulfills the heap property, terminate the algorithm.
2. Otherwise, exchange the current heap item with its parent. The index [math]\displaystyle{ k }[/math] follows the heap item.

Implementation:

1. If [math]\displaystyle{ k=1 }[/math], terminate the algorithm.
2. Set [math]\displaystyle{ k' := \lfloor k/2 \rfloor }[/math].
3. If [math]\displaystyle{ TheHeap[k'].key \le TheHeap[k].key }[/math], terminate the algorithm.
4. Swap [math]\displaystyle{ Positions[TheHeap[k].ID] }[/math] and [math]\displaystyle{ Positions[TheHeap[k'].ID] }[/math].
5. Swap [math]\displaystyle{ TheHeap[k].key }[/math] and [math]\displaystyle{ TheHeap[k'].key }[/math].
6. Swap [math]\displaystyle{ TheHeap[k].ID }[/math] and [math]\displaystyle{ TheHeap[k'].ID }[/math].
7. Set [math]\displaystyle{ k := k' }[/math].

Correctness: Obviously, the heap item at the old [math]\displaystyle{ k }[/math] now fulfills the heap property, and the new [math]\displaystyle{ k }[/math] is now the only index that does not necessarily fulfill it.