Heap as array: descendItem

Algorithmic problem: Heap as array: descendItem

Prerequisites:

Type of algorithm: loop

Auxiliary data: A natural number [math]\displaystyle{ \ell }[/math] denoting a position within the heap.

Abstract view

Invariant: After [math]\displaystyle{ i }[/math] iterations:

1. [math]\displaystyle{ 1 \le \ell \le n }[/math].
2. The parent's key and its parent's keys of the current heap item [math]\displaystyle{ h }[/math] identified by [math]\displaystyle{ /ell }[/math] are smaller than the key [math]\displaystyle{ h.key }[/math].

Variant:

1. [math]\displaystyle{ \ell }[/math] increases each step and points to a valid position within the heap that is at a lower level than before.

Break condition:

1. [math]\displaystyle{ (2* \ell \le n \Rightarrow h.key \le TheHeap[2* \ell ].key) \land (2* \ell +1 \le n \Rightarrow h.key \le TheHeap[2* \le +1].key) }[/math]

Induction basis

Abstract view:

1. Set [math]\displaystyle{ \ell }[/math] to the positions of the heap item to be descended.

Implementation:

1. [math]\displaystyle{ \ell := Positions[ID] }[/math]

Proof: Obvious.

Induction step

Abstract view:

1. Let [math]\displaystyle{ h }[/math] denote the heap item at the position [math]\displaystyle{ \ell }[/math].
2. If the existing children have higher or equal keys than [math]\displaystyle{ h }[/math], terminate algorithm.
3. Let [math]\displaystyle{ leftChild }[/math] denote the left child heap item of [math]\displaystyle{ h }[/math] and [math]\displaystyle{ rightChild }[/math] the right one.
4. If the left child has a lower key than the right one:
   1. Swap the left child with the parent heap item [math]\displaystyle{ h }[/math].
   2. Set [math]\displaystyle{ \ell }[/math] to the position of the child [math]\displaystyle{ leftChild }[/math].
5. Otherwise:
   1. Swap the right child with the parent heap item [math]\displaystyle{ h }[/math].
   2. Set [math]\displaystyle{ \ell }[/math] to the position of the child [math]\displaystyle{ rightChild }[/math].

Implementation:

1. [math]\displaystyle{ h := TheHeap[\ell] }[/math]
2. If [math]\displaystyle{ (2* \ell \le n \Rightarrow h.key \le TheHeap[2* \ell ].key) \land (2* \ell +1 \le n \Rightarrow h.key \le TheHeap[2* \le +1].key) }[/math], terminate algorithm
3. [math]\displaystyle{ leftChild := TheHeap[\ell *2] }[/math] and [math]\displaystyle{ rightChild := TheHeap[\ell *2+1] }[/math]
4. If [math]\displaystyle{ leftChild.key \le rightChild.key }[/math]:
   1. Call [math]\displaystyle{ swapItems(\ell, 2* \ell) }[/math]
   2. [math]\displaystyle{ \ell := 2* \ell }[/math]
5. Otherwise:
   1. Call [math]\displaystyle{ swapItems(\ell, 2* \ell +1) }[/math]
   2. [math]\displaystyle{ \ell := 2* \ell +1 }[/math]

Correctness: If the break condition holds the algorithm is obviously correct, as we already restored the heap property. So consider the case where we have at least one child and its key is smaller than from [math]\displaystyle{ h.key }[/math]. We will further assume that only the subtree with [math]\displaystyle{ h }[/math] as its root violates the heap property, to be more exact only the subtree [math]\displaystyle{ T }[/math] with [math]\displaystyle{ h }[/math] and its immediate children violate the property. Restoring the heap property in such a case requires to swap the minimum item with the root [math]\displaystyle{ h }[/math], this is done in step 4+5. We then have to ensure that the new subtree [math]\displaystyle{ T' }[/math] with again [math]\displaystyle{ h }[/math] as its new root also holds the heap property, this step is done the next iteration and by assigning [math]\displaystyle{ \ell }[/math] the position of the swapped child. The other pair of items, namely the earlier children satisfy the heap property because the minimum key was chosen as the new root for [math]\displaystyle{ T }[/math]. After at most [math]\displaystyle{ log n }[/math] iterations the heap item identified by [math]\displaystyle{ ID }[/math] is now a leaf or has two children that fulfill the heap property. Therefore the heap property for the whole tree is restored again.