Pivot partitioning by scanning: Difference between revisions
No edit summary |
No edit summary |
||
Line 12: | Line 12: | ||
'''Invariant:''' | '''Invariant:''' | ||
# The values of <math>m_1</math> and <math>m_2</math> only depend on the input sequence and are, hence, constant throughout the loop. More specifically, in there are | # The values of <math>m_1</math> and <math>m_2</math> only depend on the input sequence and are, hence, constant throughout the loop. More specifically, in there are | ||
## <math>m_1 - 1</math> elements less than <math>p</math>, | ## <math>m_1-1</math> elements less than <math>p</math>, | ||
## <math>m_1 - m_2</math> elements equal to <math>p</math>, and | ## <math>m_1-m_2</math> elements equal to <math>p</math>, and | ||
## <math>n - m_2</math>greater than <math>p</math>. | ## <math>n - m_2</math>greater than <math>p</math>. | ||
# Before and after each iteration, it is: | # Before and after each iteration, it is: |
Revision as of 15:19, 13 January 2015
Algorithmic problem: Pivot partioning by scanning
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:
- The values of [math]\displaystyle{ m_1 }[/math] and [math]\displaystyle{ m_2 }[/math] only depend on the input sequence and are, hence, constant throughout the loop. More specifically, in there are
## [math]\displaystyle{ m_1-1 }[/math] elements less than [math]\displaystyle{ p }[/math], ## [math]\displaystyle{ m_1-m_2 }[/math] elements equal to [math]\displaystyle{ p }[/math], and ## [math]\displaystyle{ n - m_2 }[/math]greater than [math]\displaystyle{ p }[/math].
- Before and after each iteration, it is:
## [math]\displaystyle{ 1 &le i_2 &le m_1 &le m_2 &lei3 &le i_3 &le n+1\lt math\gt ;
## \lt math\gt S[j] }[/math]for ; if , it is ;
for ; if , it is ;
for ; if , it is .
Variant: At least one of , and is increased by at least , none of them is decreased. Break condition: It is , and .
Varian: [math]\displaystyle{ i }[/math] increases by [math]\displaystyle{ 1 }[/math].
Break condition: It is [math]\displaystyle{ i=n }[/math]
Induction basis
Abstract view: [math]\displaystyle{ \forall v,w \in V }[/math] we set
- [math]\displaystyle{ M(v,v):=0, \forall v \in V }[/math]
- [math]\displaystyle{ M(v,w):=l(v,w), (v,w) \in A }[/math]
- [math]\displaystyle{ M(v,w):= +\infty }[/math], otherwise
Implementation: Obvious.
Proof: Nothing to show.
Induction step
Abstract view:
Implementation:
Correctness: Let [math]\displaystyle{ p }[/math] denote a shoortest [math]\displaystyle{ (v,w }[/math]-path subject to the constraint that all internal nodes are taken from [math]\displaystyle{ \{u_1, \ldots, u_n \} }[/math].
- If [math]\displaystyle{ p }[/math] does not contain [math]\displaystyle{ u_i }[/math], [math]\displaystyle{ p }[/math] is even a shortest [math]\displaystyle{ (v,w) }[/math]-path such that all internal nodes are taken from [math]\displaystyle{ \{u_1, \ldots , u_{i-1} \} }[/math]. In this case, the induction hypothesis implies that the value of [math]\displaystyle{ M(v,w) }[/math] immediately before the i-th iteration equals the length of [math]\displaystyle{ p }[/math]. Clearly, the i-th iteration does not change the value of [math]\displaystyle{ M(v,w) }[/math] in this case.
- On the other hand, suppose [math]\displaystyle{ p }[/math] does contain [math]\displaystyle{ u_i }[/math]. Due to the prefix property, the segment of [math]\displaystyle{ p }[/math] from [math]\displaystyle{ v }[/math] to [math]\displaystyle{ u_i }[/math] and from [math]\displaystyle{ u_i }[/math] to [math]\displaystyle{ w }[/math] are a shortest [math]\displaystyle{ (v,u_i) }[/math]-path and a shortest [math]\displaystyle{ (u_i,w) }[/math]-path, respectively, subject to the constraint that all internal nodes are from [math]\displaystyle{ \{u_1, \ldots , u_{i-1} \} }[/math]. The induction hypothesis implies that tehese lengths equal the values [math]\displaystyle{ M(v,u_i) }[/math] and [math]\displaystyle{ M(u_i, w) }[/math], respectively.
Complexity
Statement: [math]\displaystyle{ \mathcal{O}(n^3) }[/math]
Proof: The overall loop has [math]\displaystyle{ n }[/math] iterations. In each iteration, we update all [math]\displaystyle{ n^2 }[/math] matrix entities. Each update requires a constant number of steps.