Thinking in recursive way–Loop Invariant

“Even though, we can solve problems using recursion. It is tough to think something in a recursive way without the knowledge of functional programming”

See also

http://analgorithmaday.blogspot.in/2011/02/loop-invariant-to-prove-correctness.html
http://analgorithmaday.blogspot.com/2011/01/recursionfibonacci-series.html
Introduction
  Thinking in recursive way is little bit tough. But if you have programmed with a functional language then, there is no other way to think. :) When even loops are designed with recursion, you cover all the corner cases isn’t it? That’s the reason why robotics uses functional programming languages as it’s pure magic, fun and well defined mathematical entity rather than the program we write day-to-day.
  But why recursion is taught to be tough when it is so simple to implement and code looks so neat? The real application of recursion can only be seen in functional languages like Erlang.
Concept
  From what we have learnt about loop invariant, what is an invariant? variable is used to vary data, when does invariant used?
  In dummies way, invariant is nothing but a stack!! The data will never vary but get logged somewhere and get popped when needed. So, the data once set never changes but get logged.
In a for loop, we have looping variable which will be set once and the operation done for a single loop is constant!!.. The operation can only be the same for the next iteration without affecting what we are up to. otherwise, what we are doing in the loop is of no use. Simply this is called Loop invariant. When recursion is nothing but loops, understanding loops will give an intro to recursion. But Loops are simpler versions of recursion where usually people never think about constant inside the loop.
Example:

//Example of useless for loop with no loop invariant

for(int i=0; i<10;i++);

//Example of storing the values

// loop invariant: at any time a[i-1] will have data upto i-1

int a[20];

for(int i=0;i < 10; i++) { a[i] = i; }

In the above example, for loop incrementing “i” seems like not maintaining anything as invariant. But still we can tell the value of i at any point of time.
If the loop gets to stop in-between then, i’s value is nothing but the time when its stopped. But we don’t have the history.
Next example, array getting set to value of i. History of i is stored. At any point of time, we have data operation for each iteration.
Did you know?
Erlang is a kind of programming language where there is no concept of variables. :) Once we assign a value to the variable using assignment operator, next time it does plain comparison rather than re-assignment. Which means its a invariant variable. It’s not a constant as we see in C++. Don’t confuse with that anyway.
http://learnyousomeerlang.com/starting-out-for-real#invariable-variables

Loop invariant to prove correctness

“Loop invariant is a invariant defined part of tuple mathematics. It is used to prove the correctness of a loop. The below is the formula,

Metaphor

   So, you got the formula directly fetched from Wikipedia!! Did you understand it? :) The funny part this is logical mathematics which doesn’t have a metaphor or beauty to compare with.

  This technique is like theorem proving, where you consider something is true through out. Only if it is true, the theorem is also true. There are many popular theoretical way to prove a theorem,

   - proof by induction

   - proof by contradiction

There are many more theorem proving techniques available. But logical way to prove a computer program is: Hoare logic which is the formula given above

here, I is the loop invariant, C is the condition for loop termination, if you see the formula, I is maintained initial and in body and also in termination.

Concept

   Why do you want to prove correctness of a computer program? An algorithm can always fail!! There are boundary conditions, negative inputs, infinite loops and all such possibilities when you write a code which is never covered in an algorithm. How would you know that an algorithm never gives infinite loop? the simple way is loop invariants.

   In all the algorithms discussed till now, we should have used loop invariant to confirm the correctness of the code. But since this concept is little bit complex, we have covered a separate section for this. This is really important if you want to write a valid unit test for any code.

  How would you find a loop invariant??

Read fully the below link: http://www.cs.cmu.edu/afs/cs.cmu.edu/academic/class/15211/fall.97/www/lectures/lect0916

The various steps in which loop invariant should be maintained are:

1. Initialization (Assume some loop invariant), Before loop start

2. Execution (Revise the loop invariant so that its true even with the initial assumption), Loop running

3. Termination (The initial assumption should be maintained or revised loop invariant should hold), Loop ended

After analysing all the above algorithm steps, we should come with a single loop invariant which is true.

Examples

• Insertion sort
• loop invariant is for A[0..j-1], A[0] <= A[1] <=… <=A[j-1] where j-1 is the end of the sorted list.
• Linear search
• loop invariant which will be always true is: key is no found in A[j], where j is some index until which we have not found the key yet!!. If j>=n, then we already passed the size of A and hence key is not found.
• Binary search
• end is the last index, start is the first index of an array A, key is the value to search for.
• loop invariant is: A[j]  < key for all j –> end, where j is the mid index at any iteration OR A[j] > key for all start –> j, where j is the mid index at any iteration

Important points

• Loop invariants is very useful for proving the correctness of a program. Can be used for recursive as well as loop based algorithms
• Invariants are basically nothing but ASSERTs in our code. It just verifies the precondition for a function. But Loop invariants can be used to test both pre and post conditions and successful return of the value. Used for doing unit testing.
• Understanding the loop invariant of an algorithm catches bugs in code!!!.. THIS IS THE MOST IMPORTANT USE OF LOOP INVARIANT