Pivot partitioning by scanning

Algorithmic problem: Pivot partioning

Prerequisites: None

Type of algorithm: loop

Auxiliary data: Five index pointers, [math]\displaystyle{ m_1,m_2,i_1,i_2,i_3 \in \mathbb N. }[/math]

Abstract View

Invariant:

1. The values of [math]\displaystyle{ m_1 }[/math] and [math]\displaystyle{ m_2 }[/math] only depend on the input sequence [math]\displaystyle{ S }[/math] and are, hence, constant throughout the loop. More specifically, in [math]\displaystyle{ S }[/math] there are
   1. [math]\displaystyle{ m_1-1 }[/math] elements less than [math]\displaystyle{ p }[/math],
   2. [math]\displaystyle{ m_2-m_1 }[/math] elements equal to [math]\displaystyle{ p }[/math], and
   3. [math]\displaystyle{ n - m_2+1 }[/math] elements greater than [math]\displaystyle{ p }[/math].
2. Before and after each iteration, it is:
   1. [math]\displaystyle{ 1 \le i_1 \le m_1 \le i_2 \le m_2 \le i_3 \le n+1 }[/math];
   2. [math]\displaystyle{ S[j] \lt p }[/math] for [math]\displaystyle{ j \in \{1,...,i_1-1\} }[/math]; if [math]\displaystyle{ i_1 \lt m_1 }[/math], it is [math]\displaystyle{ S[i_1] \nless p }[/math];
   3. [math]\displaystyle{ S[j] =p }[/math] for [math]\displaystyle{ j \in\{m_1,...,i_2-1\} }[/math]; if [math]\displaystyle{ i_2 \lt m_2 }[/math], it is [math]\displaystyle{ S[i_2] \ne p }[/math];
   4. [math]\displaystyle{ S[j] \gt p }[/math] for [math]\displaystyle{ j \in \{m_2,...,i_3-1\} }[/math]; if [math]\displaystyle{ i_3 \le m_1 }[/math], it is [math]\displaystyle{ S[i_3] \ngtr p }[/math].

Variant: At least one of [math]\displaystyle{ i_1,i_2 }[/math], and [math]\displaystyle{ i_3 }[/math] is increased by at least [math]\displaystyle{ 1 }[/math], none of them is decreased.

Break condition: It is [math]\displaystyle{ i_1=m_1, i_2=m_2 }[/math] and [math]\displaystyle{ i_3 = n+1 }[/math].

Induction basis

Abstract view:

1. Set [math]\displaystyle{ m_1 }[/math] and [math]\displaystyle{ m_2 }[/math] according to the loop invariant.
2. Initialize [math]\displaystyle{ i_1,i_2 }[/math] and [math]\displaystyle{ i_3 }[/math].

Implementation:

1. Set [math]\displaystyle{ m_1:=1 }[/math] .
2. For [math]\displaystyle{ j \in {1,...,n} }[/math]: If [math]\displaystyle{ S[j]\lt p }[/math] increase [math]\displaystyle{ m_1 }[/math] by [math]\displaystyle{ 1 }[/math].
3. Set [math]\displaystyle{ m_2:=m_1 }[/math].
4. For [math]\displaystyle{ j \in {1,...,n} }[/math]: If [math]\displaystyle{ S[j]=p }[/math] increase [math]\displaystyle{ m_2 }[/math] by [math]\displaystyle{ 1 }[/math].
5. [math]\displaystyle{ i_1:=1 }[/math].
6. [math]\displaystyle{ i_2:=m_1 }[/math].
7. [math]\displaystyle{ i_3:=m_2 }[/math].
8. While [math]\displaystyle{ i_1\lt m_1 }[/math] and [math]\displaystyle{ S[i_1]\lt p }[/math], set [math]\displaystyle{ i_1:=i_1+1 }[/math].
9. While [math]\displaystyle{ i_2\lt m_2 }[/math] and [math]\displaystyle{ S[i_2]=p }[/math] , set [math]\displaystyle{ i_2:=i_2+1 }[/math].
10. While [math]\displaystyle{ i_3\lt n+1 }[/math] and [math]\displaystyle{ S[i_3]\gt p }[/math], set [math]\displaystyle{ i_3:=i_3+1 }[/math] .

Proof: Obvious.

Induction step

Abstract view:

1. If the algorithm is not done yet, identify two out of the three index pointers [math]\displaystyle{ i_1,i_2 }[/math], and [math]\displaystyle{ i_3 }[/math]such that at least one of these two can be moved one step forward after a swap of the elements at these two positions.
2. Then move each of [math]\displaystyle{ i_1,i_2 }[/math], and [math]\displaystyle{ i_3 }[/math] forward as long as the invariant is not violated.

Implementation:

1. If [math]\displaystyle{ i_1=m_1 }[/math] and [math]\displaystyle{ i_2=m_2 }[/math] and [math]\displaystyle{ i_3=n+1 }[/math], terminate the algorithm and return [math]\displaystyle{ m_1,m_2 }[/math].
2. If [math]\displaystyle{ i_1\lt m_1 }[/math] :
   1. If [math]\displaystyle{ S[i_1]=p }[/math]:
      1. Swap [math]\displaystyle{ S[i_1] }[/math] and [math]\displaystyle{ S[i_2] }[/math].
      2. Set [math]\displaystyle{ i_2:=i_2+1 }[/math] until [math]\displaystyle{ i_2=m_2 }[/math] or else [math]\displaystyle{ S[i_2] \ne p }[/math].
   2. Otherwise (that is, [math]\displaystyle{ S[i_1]\gt p }[/math]):
      1. Swap [math]\displaystyle{ S[i_1] }[/math] and [math]\displaystyle{ S[i_3] }[/math].
      2. Set [math]\displaystyle{ i_3:=i_3+1 }[/math] until [math]\displaystyle{ i_3=n+1 }[/math] or else [math]\displaystyle{ S[i_3] \ngtr p }[/math].
   3. While [math]\displaystyle{ i_1\lt m_1 }[/math] and [math]\displaystyle{ S[i_1]\lt p }[/math]: set [math]\displaystyle{ i_1:=i_1+1 }[/math].
3. Otherwise (that is, [math]\displaystyle{ i_1=m_1 }[/math]):
   1. Swap [math]\displaystyle{ S[i_2] }[/math] and [math]\displaystyle{ S[i_3] }[/math].
   2. Set [math]\displaystyle{ i_2:=i_2+1 }[/math] until [math]\displaystyle{ i_2=m_2 }[/math] or else [math]\displaystyle{ S[i_2] \ne p }[/math] .
   3. Set [math]\displaystyle{ i_3:=i_3+1 }[/math] until [math]\displaystyle{ i_3=n+1 }[/math] or else [math]\displaystyle{ S[i_3] \ngtr p }[/math].

Correctness: Due to the various "otherwise" clauses, all possible cases are covered. Therefore, it remains to show that the invariants are maintained in each of the considered cases. As the values of [math]\displaystyle{ m_1 }[/math] and [math]\displaystyle{ m_2 }[/math] are never changed after initialization, all three parts of the first invariant are trivially maintained. Since [math]\displaystyle{ i_1 }[/math] (resp., [math]\displaystyle{ i_2 }[/math], [math]\displaystyle{ i_3 }[/math]) is only increased in case [math]\displaystyle{ i_1\lt m_1 }[/math] (resp., [math]\displaystyle{ i_2\lt m_2 }[/math], [math]\displaystyle{ i_3\lt n+1 }[/math]), Invariant 2.1 is maintained as well. So, we will focus on Invariants 2.2-2.4. If Step 2 applies, maintenance of Invariants 2.2-2.4 might be obvious. So consider Step 3. If Step 3 applies ([math]\displaystyle{ i_1=m_1 }[/math]), the break condition is not yet met, so we know [math]\displaystyle{ i_2\lt m_2 }[/math] or [math]\displaystyle{ i_3\lt n+1 }[/math], or both. Without loss of generality, assume [math]\displaystyle{ i_2\lt m_2 }[/math] (the other case is mirror-symmetric). Invariant 2.3 implies [math]\displaystyle{ S[i_2]\neq p }[/math], which amounts to [math]\displaystyle{ S[i_2]\gt p }[/math] in Step 3. So, not all elements [math]\displaystyle{ \gt p }[/math] are on the correct positions, which implies [math]\displaystyle{ i_3\lt n+1 }[/math]. In summary, it is safe to apply Step 3.