2013-07-19 10:29:14
最近看《編程珠璣》、《算法導論》，其中有一個術語“循環不變式”，多次看到，一致不是很理解，查了一些資料，還不是很懂，下面是收集到的的一些靠譜的資料。
下面轉自：http://www.cnblogs.com/bamboo-talking/archive/2011/02/05/1950197.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.
利用循環不變式(loop invariant)來證明循環的正確性與用數學歸納法(induction)證明數學等式的相同點在於：需要驗證初值，或初始狀態是否滿足條件。之后再證明在歸納或遞推的過程中仍然滿足這種條件。（這個條件在數學歸納中叫做遞推關系，在循環中就是循環不變式(loop invariant)）。
循環不變式(loop invariant)與數學歸納法(induction)的區別在於：數學歸納可能是無限的，是無限地腿的，但循環不變式所要證明的循環是要結束並給出正確結果的。
在插入排序的例子中：
INSERTION-SORT(A)
1 for j ← 2 to length[A]
2 do key ← A[j]
3 ▹ Insert A[j] into the sorted sequence A[1 ‥ j - 1].
4 i ← j - 1
5 while i > 0 and A[i] > key
6 do A[i + 1] ← A[i]
7 i ← i - 1
8 A[i + 1] ← key
· Initialization: We start by showing that the loop invariant holds before the first loop iteration, when j = 2.[1] The subarray A[1 ‥ j - 1], therefore, consists of just the single element A[1], which is in fact the original element in A[1]. Moreover, this subarray is sorted (trivially, of course), which shows that the loop invariant holds prior to the first iteration of the loop.
Maintenance: Next, we tackle the second property: showing that each iteration maintains the loop invariant. Informally, the body of the outerfor loop works by moving A[ j - 1], A[ j - 2], A[ j - 3], and so on by one position to the right until the proper position for A[ j] is found (lines 4-7), at which point the value of A[j] is inserted (line 8). A more formal treatment of the second property would require us to state and show a loop invariant for the "inner" while loop. At this point, however, we prefer not to get bogged down in such formalism, and so we rely on our informal analysis to show that the second property holds for the outer loop.
Termination: Finally, we examine what happens when the loop terminates. For insertion sort, the outer for loop ends when j exceeds n, i.e., when j = n + 1. Substituting n + 1 for j in the wording of loop invariant, we have that the subarray A[1 ‥ n] consists of the elements originally in A[1 ‥ n], but in sorted order. But the subarray A[1 ‥ n] is the entire array! Hence, the entire array is sorted, which means that the algorithm is correct
在這個例子中，“At the start of each iteration of the for loop of lines 1-8, the subarray A[1 ‥ j - 1] consists of the elements originally in A[1 ‥ j - 1] but in sorted order.”，也就是，每當算法進行到第一行時，數組A中從第1個至第j-1個元素仍然是算法執行前數組中第1個至第j-1個元素，只是執行算法后，這些元素是排好序的，以上就是這個算法的for循環的循環不變式。(就是一個條件。)
再循環的Initialization階段，j的初值為2，數組A[1 .. j-1]即是A[1],是排好序的，而且其元素仍然是原數組A[1]的，只是現在排好序了。
Maintenance：這個階段要證明的是每一次循環的結果都滿足先前提到的的循環不變式。
Termination：這個階段要證明,當循環結束時，數組A中的所有元素都排好序。
再看算法第一行，當j=length[A]+1時循環結束，由於滿足循環不變式，所以，數組A[1 .. length[A]]是排好序的，且是原數組的那些元素。
至此，可以說明算法正確。
再來說一下如何找循環不變式。由於算法是一步步執行的，那么如果每一步（包括初試和結束）都滿足一個共同的條件，那么這個條件就是要找的循環不變式（loop invariant）。再說上面的例子，要得到的結果是排序且元素不改變的數組，所以循環不變式就是數組A中從第1個至第j-1個元素是排好序的且是與原數組的元素是一致的。
百度知道的回答：http://zhidao.baidu.com/question/558630518.html
問題描述：算法導論中的 循環不變式怎么理解
書本上舉了一個插入排序的例子
我想知道 循環不變式 是指代碼中的 特定部分的代碼段 還是說只是一個思想
我沒看懂 請懂的朋友指點迷津 請勿抄襲 粘貼 其他貼吧的
謝謝合作
就是個思想，說明正確算法的循環過程中總是存在一個維持不變的特性，這個特性一直保持到循環結束乃至算法結束，這樣就可以保證算法的正確了。
比方說插入排序，算法每次循環后，前n個數一定是排好序的（n為已經循環的次數）。由於這個特性一直成立，到算法結束時，所有N個數一定是排好序的。
關於這個思想，不要小看了，很多算法的正確性都是這么保證的。
這個思想 不是證明排序算法的正確性 不是分三個部分 我們去證明的過程 應把握那些着重點 證明那些特性 才能保證正確性 在直接點就是 課后題有關於
交換排序的正確性證明 怎么去證明他也是正確的算法
要尋找循環不變的特性，一般都是循環結束時數據具有的特性。如何尋找循環不變量，沒有一般方法，不過這是證明算法正確性的最正規的方法。
比如冒泡排序，算法中存在兩次循環：外層循環可以保證第n次循環后第n位的數比上面所有數都大；內部循環可以保證第n次循環后第n+1位都是上面n+1位中最大的。
內部循環可以保證每次外層循環的正確性；
外部循環可以保證最后是排好序的。