Day-3 insertion sort与循环不变式

插入排序(insertion sort)

Input: 一连串正整数所成的集合 { }
Output: 一连串已经过排序的正整数集合 { }，且

虽然概念上我们是针对一个序列进行排列，但实务上我们是透过阵列实作。

下面会透过虚拟码的方式来描述插入排序法，之所以透过虚拟码进行描述，原因在於使用虚拟码较容易理解一个演算法的概念，虚拟码可以不用注意一些语法细节或是些软件工程的问题，可以让我们更加专注研究於演算法本身。

插入排序法，在排序的元素不多时十分的有效率。插入排序法的进行方式很像我们在排序手上的扑克牌

首先，所有卡牌目前是牌面向下放在桌上，我们用左手从桌上抽起一张牌，接着拿下一张牌，如果这张牌比原本手上的牌点数还要大时，我们就把这张牌放在原本牌的右边，如果比较小就放在左边，如上图所示。

接着我们将这个过程以虚拟码的方式写出来，而这个虚拟码描述的即是插入排序法了，Input使用阵列A[1...n]表示n个正整数所成的集合，经过演算法将阵列中的元素重新排序後输出，插入排序法便完成了。

输入的阵列为 {}
(a) 拿起2这张牌，发现第一张牌比他大，第一张牌往後移动一格，并将2这张牌放入
(b) 拿起4这张牌，发现第二张牌比他大，但第一张牌没有，第二张牌往後移动一个，并将4这张牌放入
(c) 拿起6这张牌，发现前三张没有一张牌比他大，因此不做任何动作
(d) 拿起1这张牌，发现前四张皆比他大，前四张都往後移动一格，并将1这张牌放入
(e) 拿起3这张牌，发现三,四,五张皆比他大，因此这三张往後移动一格，将3这张牌放入。
(f) 该阵列已经完成排序。

虽然这样描述起来我们好像是用两个阵列进行排序的操作，但实作上我们只使用一个阵列去完成操作，也就是在原地(In-place)完成操作。

虚拟码:

for j = 2 to A.length
    key = A[j]
    //Insert A[j] into the sorted sequence A[1...j - 1]
    i = j - 1
    while i > 0 and A[i] > key
        A[i + 1] = A[i]
        i = i - 1
    A[i + 1] = key

每一次for回圈的迭代就是在选择黑色方块，也就是比较的对象key，这个key和他左边的扑克牌点数进行比较，在第6行的地方表示向右移动移动一格，也就是上图灰色箭头的部分，第8行，对应到上图黑色箭头则表示key要移动到的位置。1到j的部分已经排序完成，剩余需排序的为j + 1到n。

上面虚拟码展示了插入排序法是如何运作的. index j表示正准备要放入手中的扑克牌，在外层for回圈(index为j)的每一轮迭代的开始，包含元素A[1,...,j - 1]的子阵列组成了左手中已经经过排序的手牌，元素A[j + 1,...,n]对应到还在桌上的那些牌。实际上，元素A[1,...,j - 1]是一开始在桌上1到j - 1的那些元素，但现在已经经过排序放在左手了，下面，将以循环不变式(loop invariant)来表示A[1,...,j-1]所具备的性质

验证演算法的正确性，循环不变式(loop invariant)

循环不变式(loop invariant)本质上就是每一次迭代都会成立的一个条件或是表示式，主要是用来帮助我们理解为什麽一个演算法是正确的. 对於循环不变量，我们需要遵守下面三个法则
:::info
初始化(Initialization) : 在第一次迭代开始之前，应该要是正确的。

维持(Maintenance) : 如果他在某一次回圈的迭代之前是正确的，那麽他在该回圈的下一次迭代之前也应该是正确的。

终止(Termination) : 当回圈停止时，循环不变量会给我们一个性质，这个性质可以用来证明演算法是正确的。
:::

当初始化和维持皆成立时，就能确保循环不变量在回圈的每一轮迭代开始之前，都是正确的。这里的推论过程很像数学归纳法，为了证明某一个性质成立，需要证明一个基本情况和归纳步(第k步)，在这里，证明第一次迭代情况之前循环不变量是正确的为基本情况，证明从某一次迭代到下一次迭代循环不变式正确为归纳步(第k步)。

第三个性质，我们将使用循环不变量来证明第三个性质的正确性(第k + 1步)，通常，我们会将循环不变式和导致回圈终止的条件一起使用。而这里的终止性不同於数学归纳法中的做法，这里只要循环停止时，便停止归纳。

举例来说:

int j = 9; for(int i=0; i<10; i++) j--; 

初始 : 在第一次迭代以前， i + j == 9成立
维持 : 每一次迭代开始之前，i + j == 9皆成立
终止 : 当回圈结束後，i + j == 9依然成立

这个例子中，只要i + j == 9，这个循环不变式便成立，可以印证这个回圈是没有错误的。

下面就尝试证明插入排序法是正确的演算法

循环不变式 : 每一次迭代从阵列A里面举出第j个元素插入到有顺序的阵列A[1... j - 1]，然後递增j。这样A[1...j - 1]就始终都是排好序的，而我们的循环不变式就是A[1...j - 1]是始终保持排好序的。

• 初始化(Initialization) : 首先证明在第一次迭代之前(在j初始化为2时)，循环不变式成立。子阵列A[1,...,j - 1]仅由单个元素A[1]所组成，实际上就是A[1]中原来的元素，且该子阵列式已经排序完成的，因此，这表示第一次回圈迭代之前循环不变式成立。

• 维持(Maintenance) : 接着证明每一次迭代维持循环不变式。大概描述一下，for回圈得主体的第4行到第7行将A[j - 1], A[j - 2], A[j - 3]等元素向右移动一个位置，直到找到A[j]适合放入的位置，第8行将A[j]的值插入到该位置。这时候的子阵列A[1,...,j]是由原来在A[1,...,j]中的元素所组成，但子阵列已经按照顺序进行排列。那麽对於下一次for回圈的迭代，j增加将保持循环不变式。

补充: 其实更精确，更严谨的做法应该要去证明while回圈的循环不变式，但这麽做，便偏离了我们要证明演算法本身，有点太过於钻牛角尖了，因此一般来说不会那麽做，而是依靠以上大略的分析去证明维持性对於外层回圈是成立的。

• 终止(Termination) : 最後要来看看循环停止时发生了什麽事情。for回圈的终止条件为j > A.lenght = n。因为每一次循环迭代j都会增加1，那麽必有j = n + 1(for回圈的更新值)。在循环不变式的描述中我们将j以n + 1替换掉，可以得到子阵列A[1,...,n]由原来在A[1,...,n]中的元素所组成，但已经按照顺序进行排列。这里我们可以发现，子阵列A[1,...,n]就是整个阵列，我们可以推测出整个阵列已经完成排序，因此这个演算法是正确的。

C语言程序码

int main(void)
{
    int A[] = {5, 2, 4, 6, 1, 3};
    int len = sizeof(A) / sizeof(int);
    for (int i = 1; i < len; i++)
    {
        int key = A[i];
        int j = i - 1;
        while (j >= 0 && A[j] > key)
        {
            A[j + 1] = A[j];
            j--;
        }
        A[j + 1] = key;
    }
}

for回圈从i = 1开始

选到A[1](2)这张牌，当作key(比较的标的)，从这张牌的前一张开始进行比较，因此j = i - 1
进入while回圈开始比较，如果j(1) >= 0且A[j](5) > key(2)，则进行while回圈内的动作

A[j + 1](2) = A[j](5)，表示把比key大的数字往後移动一格
j--，表示往前一格继续比较剩余的卡牌

while整轮的动作就是和key前面的牌进行比较，如果比key还要大，则往後移动一格

A[j + 1] = key，在刚刚j停下的位置後一格放入key。

再来看一个例子，二元搜寻法

int binary_search(int *array, int len, int target)
{
    int start = 0;
    int end = len;
    while(start <= end)
    {
        int mid = (start + end) / 2;
        if(array[mid] == target)
        {
            return mid;
        }
        else if(array[mid] < target)
        {
            start = mid + 1;
        }
        else
        {
            end = mid - 1;
        }
    }
    return -1;
}

这里的循环不变式，是以下的述句

if array[mid] == target, then start <= mid <= end

如果这个函式回传了target所在的位置，表示我们有找到目标元素，如果找到目标元素，则目标元素必定在阵列当中。如果回圈停止，则start <= mid <= end。

练习

1. 使用insertion sort对{}进行升序和降序的排序

Answer: 上方的示范为升序排列，若要降序，则依照以下作法
如果发现key比前面的牌还要大，则前面的牌往前移动，空出空位给key

#include <stdio.h>

void insertion_sort_up(int *, int);
void insertion_sort_down(int *, int);
void print_array(int *, int);

int main(void)
{
    void (*func[3])(int *, int) = {insertion_sort_up, insertion_sort_down, print_array};
    int A[] = {31, 41, 59, 26, 41, 58};
    int len = sizeof(A) / sizeof(int);
    func[0](A, len);
    func[2](A, len);
    func[1](A, len);
    func[2](A, len);


}

void insertion_sort_up(int *A, int len)
{
    for(int i = 1; i < len; i++)
    {
        int key = A[i];
        int j = i - 1;
        while(j >= 0 && key < A[j])
        {
            A[j + 1] = A[j];
            j--;
        }
        A[j + 1] = key;
    }
}

void insertion_sort_down(int *A, int len)
{
    for(int i = 1; i < len; i++)
    {
        int key = A[i];
        int j = i - 1;
        while(j >= 0 && key > A[j])
        {
            A[j + 1] = A[j];
            j--;
        }
        A[j + 1] = key;
    }
}

void print_array(int *A,  int len)
{
    for(int i = 0; i < len ; i++)
    {
        printf("%d ", *(A + i));
    }
    puts("");
}

2. 考虑以下搜寻元素的问题
   Input : 由n个正整数所组成的集合{ }和一个正整数。
   Output : 输出一个index i使得成立，若不在集合中，则回传。
   请以线性搜寻(Linear search)的方式写出该程序的虚拟码，遍历整个阵列来寻找，并使用循环不变式来证明我们所写出的演算法正确的。

Answer:

LINEAR-SEARCH(A, v)
    for i = 1 to A.length
       if A[i] == v
            return i
    return NIL

循环不变式 : 在每一次for回圈的迭代开始之前，子阵列A[1,...,i - 1]由与v不同的元素所组成。

初始化(Initialization) : 在第一次迭代开始之前，子阵列为一个空阵列(空集合)，由与v不同的元素所组成。

维持(Maintenance) : 在每一次迭代，我们将v和A[i]进行比较，如果在A中找到v，则我们会回传index i。如果不等於，我们就继续进行下一次迭代。若在最後一次迭代中没有在A中找到v，则表示v并不在A里面，循环不变式，子阵列A[1,...,i - 1]由与v不同的元素所组成这件事情依然成立。

终止(Termination) : 回圈终止条件为当i > a.length = n. 每当i + 1时，我们必须让i = n + 1同时发生，将循环不变式中子阵列A[1,...,i - 1]中的i以n + 1代换掉，得到A[1,...,n]，且这个子阵列是由不同於v的元素所构成的，也因此会回传NIL。
到这里，我们证明迭代结束时，子阵列A[1,...,i - 1]由与v不同的元素所组成，因此演算法正确。

参考资料: Introduction to algorithms 3rd