Loop and Recursion Invariant

http://touch.ethz.ch/recursion.pdf
http://www.cs.sfu.ca/CourseCentral/125/johnwill/Packet14.pdf
A loop invariant is a statement that is true every
loop
● usually asserted at the beginning of the loop
● usually parametrized by the loop index
A good loop invariant should indicate the progress of the algorithm
● the invariant should carry all state information, loop to loop
● the invariant should imply the post-condition (the goal of the algorithm) at the end of the last loop

Use mathematical reasoning to capture the behaviour of an
algorithm:
● State invariants at various checkpoints
● Show that the invariant holds:
○ at the first checkpoint
○ during execution between checkpoints
● Conclude that the post-condition holds
○ the invariant holds at / after the last checkpoint
Initialization
Maintenance
Termination
Q. This works pretty well for simple iteration,
but what if your algorithm has no loops?
● Invariants are very powerful for recursive programs

Invariants and Recursion
Rule of Thumb: You may assume the invariant holds for any smaller case

X. http://www.drdobbs.com/cpp/invariants-for-binary-search-part-1-a-si/240169169

We can use an invariant to help us reason about a piece of code that many programmers find hard to get right by any other means.

https://www.eecs.yorku.ca/course_archive/2013-14/W/2011/lectures/09%20Loop%20Invariants%20and%20Binary%20Search.pdf
Ø Maintain a sublist. Ø If the key is contained in the original list, then the key is contained in the sublist.

 It is faster not to check if the middle element is the key. Ø Simply continue.
http://www.cs.cornell.edu/courses/cs2112/2015fa/lectures/lec_loopinv/index.html
https://reprog.wordpress.com/2010/04/25/writing-correct-code-part-1-invariants-binary-search-part-4a/

http://www.cnblogs.com/youngforever/p/3200081.html

We use loop invariants to help us understand why an algorithm is correct. We must show three things about a loop invariant:

·         Initialization: It is true prior to the first iteration of the loop.

·         Maintenance: If it is true before an iteration of the loop, it remains true before the next iteration.

·         Termination: When the loop terminates, the invariant gives us a useful property that helps show that the algorithm is correct.

循环不变式(loop invariant)与数学归纳法(induction)进行对比:

When the first two properties hold, the loop invariant is true prior to every iteration of the loop. Note the similarity to mathematical induction, where to prove that a property holds, you prove a base case and an inductive step. Here, showing that the invariant holds before the first iteration is like the base case, and showing that the invariant holds from iteration to iteration is like the inductive step.

The third property is perhaps the most important one, since we are using the loop invariant to show correctness. It also differs from the usual use of mathematical induction, in which the inductive step is used infinitely; here, we stop the "induction" when the loop terminates.

http://analgorithmaday.blogspot.in/2011/02/loop-invariant-to-prove-correctness.html

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

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

http://www.drdobbs.com/cpp/loop-invariants-abbreviate-induction-pro/240169015

This example suggests a general technique for writing loops:

• Define an invariant that describes the loop's behavior, independently of how many times it executes.
• Choose a condition for the while statement that, when combined with the invariant, yields the behavior we want. Write the body of the loop in a way that maintains the invariant while working toward eventually making the while condition false, so that the loop will always terminate.

http://whiley.org/2013/01/29/understanding-loop-invariants-in-whiley/
http://homepages.ius.edu/RWISMAN/C455/html/notes/Chapter2/LoopInvariantProof.htm

Loop invariant proofs must show three parts:

1. Initialization - the loop invariant holds prior to executing the loop, after initialization.
2. Maintenance - the loop invariant holds at the end of executing the loop.
3. Termination - the loop eventually terminates.

http://betareduction.wordpress.com/2014/01/11/from-loop-invariants-to-recursion-invariants/

What we have here, then, is a recursion invariant, that is, an invariant property that is guaranteed to be preserved between recursive calls. The way to prove a recursion invariant is basically the same as we would a loop invariant: initiation, maintenance and termination. But instead of thinking in terms of how a loop changes certain variables, we think of states and the relationship between consecutive states.

What we have here, then, is a recursion invariant, that is, an invariant property that is guaranteed to be preserved between recursive calls. The way to prove a recursion invariant is basically the same as we would a loop invariant: initiation, maintenance and termination. But instead of thinking in terms of how a loop changes certain variables, we think of states and the relationship between consecutive states.

In particular, we interested in the first state (the initiation), the last state (the termination, which can be straightforwardly transformed to the final result) and the inductive step of generating a new state from the current state, assuming that the current one satisfies the invariant. No mutation of variables and no notion of time to worry about; just the sequence of states.

And it gets even better: we don’t even need to think about the sequence itself. It suffices to establish the relationship between input and output. In terms of code, we have to establish the relationship between the first and second parameters in line 2 with the first and second parameters in lines 7 and 8.

To sum up, the next time you write code to solve some problem, try to think about what property your algorithm keeps throughout its execution. And, if possible, try to develop a (tail) recursive version of it, so that you can prove that it works with mucho more elegance and simplicity. The key to understand how an algorithm changes things is to observe what it does not change

http://programatica.cs.pdx.edu/P/KrsticMatthewsTPHOLS03.pdf

http://analgorithmaday.blogspot.com/2012/08/thinking-in-recursive-wayloop-invariant.html