Loop Invariant in Recursive function

algorithm-analysisalgorithms

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.

Best Answer

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.

Related Solutions

Loop invariant vs Assertions

An invariant is a condition that can be relied upon to be true during execution of a program. For example, a loop invariant is a condition that is true at the beginning and end of every execution of a loop.

An assertion is a predicate (a true–false statement) placed in a program to indicate that the developer thinks that the predicate is always true at that place. Programmers often use assertions in their code to make invariants explicit.

While Loop Invariance Theorem
Assume that S is an invariant of the loop

While C do
 E

Assume also that S is true on the first entry to the loop. Then S stays true after every iteration of the loop. In particular,

If the loop terminates then S is true after the last iteration.
If the loop does not terminate then S always stays true.

Algorithms – How to Convert Loop to Recursion or Vice Versa

Actually you should break the function down first:

A loop has a few parts:

the header, and processing before the loop. May declare some new variables
the condition, when to stop the loop.
the actual loop body. It changes some of the header's variables and/or the parameters passed in.
the tail; what happens after the loop and return result.

Or to write it out:

foo_iterative(params){
    header
    while(condition){
        loop_body
    }
    return tail
}

Using these blocks to make a recursive call is pretty straightforward:

foo_recursive(params){
    header
    return foo_recursion(params, header_vars)
}

foo_recursion(params, header_vars){
    if(!condition){
        return tail
    }

    loop_body
    return foo_recursion(params, modified_header_vars)
}

Et voilà; a tail recursive version of any loop. breaks and continues in the loop body will still have to be replaced with return tail and return foo_recursion(params, modified_header_vars) as needed but that is simple enough.

Going the other way is more complicated; in part because there can be multiple recursive calls. This means that each time we pop a stack frame there can be multiple places where we need to continue. Also there may be variables that we need to save across the recursive call and the original parameters of the call.

We can use a switch to work around that:

bar_recurse(params){
    if(baseCase){
        finalize
        return
    }
    body1
    bar_recurse(mod_params)
    body2
    bar_recurse(mod_params)
    body3
}


bar_iterative(params){
    stack.push({init, params})

    while(!stack.empty){
        stackFrame = stack.pop()

        switch(stackFrame.resumPoint){
        case init:
            if(baseCase){
                finalize
                break;
            }
            body1
            stack.push({resum1, params, variables})
            stack.push({init, modified_params})
            break;
        case resum1:
            body2
            stack.push({resum2, params, variables})
            stack.push({init, modified_params})
            break;
        case resum2:
            body3
            break;
        }
    }
}

Best Answer

Related Solutions

Loop invariant vs Assertions

Algorithms – How to Convert Loop to Recursion or Vice Versa

Related Topic