Loop Invariant in Recursive function

Question

When I was reading Introduction to Algorithms (3rd edition, P188), there is an algorithm called Tail-Recursive-QuickSort and we have to prove the correctness of this algorithm.

TAIL-RECURSIVE-QUICKSORT(A, p, r)
1 while p < r
2     // Partition and sort left subarray.
3     q = PARTITION(A, p, r)
4     TAIL-RECURSIVE-QUICKSORT(A, p, q - 1)
5     p = q + 1

The problem is, when I tried to use loop invariant, I found it difficult for me to explain the maintenance clearly because of the recursive function inside the loop body. The loop invariant I use is:

Before each iteration, A[0:p-1] are sorted.

The initial case is trivial, but the maintenance involves prove TAIL-RECURSIVE-QUICKSORT doesn't change loop invariant. Is there any way to explain it clearly?

Thanks.

Erik Eidt · Accepted Answer · 2016-09-12 02:57:11Z

Ok, perhaps the snippet is too small. I don't see the tail recursion, just a function with "TAIL" in the name.

But when a language or compiler takes advantage of tail recursion, the code runs the same as if it were not tail recursive, except for not using as much stack space.

During a tail call optimization, variable state in the current frame is replaced in its entirety with new state from the new call (just as if the new call had been made unoptimized with a new stack frame). No state from the caller survives except where to return.

So, if you can prove the normal recursive case, you can apply that proof to the tail recursive case.

Tail recursion is an optimization technique, and, optimization techniques don't change your algorithm (broken or buggy compiler notwithstanding).

As far as proving the proving the invariant regarding the recursion, I think it is an academic exercise; for example, see here: https://www.cs.rochester.edu/~gildea/csc282/slides/C07-quicksort.pdf

Before each iteration, A[0:p-1] are sorted.

I don't think there is quicksort invariant that requires the input is sorted, but rather that it is partitioned, which is a testable condition but not the same as sorted.

Further, a recursive quicksort, a the top-level, doesn't operate in terms of iterations, as there is no outer loop, but in terms of invocations as there is recursion.

The invariant looks like it makes sense for selection sort, but definitely not for quicksort. The invariant for recursive quicksort is that all elements left of the pivot or smaller and all elements right of the pivot are not smaller, i.e. greater-or-equal than the pivot. — Jörg W Mittag
– Jörg W Mittag, Commented Sep 11, 2016 at 19:06
@JörgWMittag, agreed (i.e. partitioned). Seems like there is some error somewhere here, maybe in the original text or maybe transcribed incorrectly. — Erik Eidt
– Erik Eidt, Commented Sep 11, 2016 at 19:10

gnasher729 · Accepted Answer · 2016-09-12 10:39:27Z

You have a recursive function. The basic method to prove that a recursive function will work correctly is by complete induction: You prove that the function works correctly if some value n is 0 (you would have n = r - p, for example), and then you prove that it works correctly for n > 0 if it works correctly for all smaller values of n.

So you first go through your code and check that it is correct if r - p = 0. Then you prove that q-1 < r, because this means in the recursive call r - p will be smaller, and therefore you can assume by induction that it works. And for the rest of the proof, you still need a loop invariant. And a spec what PARTITION is supposed to do, and a proof that it does what it is supposed to do.

Your loop invariant cannot work, for example if you ever had p = 3, and six array elements 11, 12, 13, 1, 2, 3, then your "loop invariant" is true before the loop but not afterwards because 11, 12, and 13 at the beginning of the array wouldn't be touched anymore.

Stack Exchange Network

Loop Invariant in Recursive function

2 Answers 2

Your Answer

Hot Network Questions

Loop Invariant in Recursive function

2 Answers 2

Your Answer

Sign up or log in

Post as a guest

Related

Hot Network Questions