循环不变式在基数排序中的正确性证明

题目描述
基数排序（Radix Sort）是一种非比较型整数排序算法，它通过逐位处理数字的各个位数来实现排序。通常从最低有效位（LSD）开始，依次根据每一位的值将数字分配到0-9的桶中，然后按桶顺序收集，重复这一过程直到最高位。我们需要使用循环不变式（Loop Invariant）来严格证明基数排序的正确性，确保算法在每一轮处理后都能维持关键性质。

解题过程

1. 理解基数排序的步骤

   • 假设待排序数组包含非负整数（若含负数需额外步骤，此处简化）。
   • 确定最大数字的位数 \(d\)，作为排序轮数。
   • 第 \(i\) 轮（\(1 \leq i \leq d\)）根据第 \(i\) 位数字（从低位到高位）进行稳定排序（常用计数排序）。

2. 定义循环不变式
   循环不变式是算法中在每次循环开始和结束时均成立的条件。对于基数排序，定义不变式：

   在第 \(k\) 轮处理结束后，所有数字根据最低 \(k\) 位（从低位到高位）已有序。
   即：对于任意两个数字 \(a\) 和 \(b\)，如果它们的最低 \(k\) 位组成的数值满足 \(a_{\text{low-k}} < b_{\text{low-k}}\)，则 \(a\) 必排在 \(b\) 之前；若相等，则相对顺序与输入一致（稳定排序保证）。

3. 初始状态验证（Base Case）

   • 当 \(k = 0\)（未开始排序），所有数字的最低 0 位视为 0，此时数组顺序为初始顺序，不变式自然成立。

4. 循环保持（Maintenance）

   • 假设第 \(k\) 轮结束后不变式成立，即数组按最低 \(k\) 位有序。
   • 进行第 \(k+1\) 轮排序：根据第 \(k+1\) 位数字分配到桶中，并按桶顺序（0到9）稳定地收集数字。
   • 关键证明：
     • 对于任意两个数字 \(a\) 和 \(b\)：
       • 若它们的第 \(k+1\) 位数字不同（如 \(a_{k+1} > b_{k+1}\)），则收集时 \(a\) 必然在 \(b\) 之后（因按桶顺序收集），满足高位优先的排序逻辑。
       • 若第 \(k+1\) 位相同，则稳定排序会保留它们在上一轮后的相对顺序。而由归纳假设，第 \(k\) 轮后它们已按最低 \(k\) 位有序，因此最终顺序正确。
   • 故第 \(k+1\) 轮后，数组按最低 \(k+1\) 位有序，不变式保持。

5. 终止状态（Termination）

   • 当 \(k = d\)（处理完最高位），数组按所有 \(d\) 位有序，即整体有序，算法正确。

6. 示例辅助理解
   以数组 [170, 45, 75, 90, 2, 802, 24] 为例：

   • 最大位数 \(d=3\)，需3轮排序。
   • 第1轮（个位）：按个位数字排序后为 [170, 90, 802, 2, 24, 45, 75]。
   • 第2轮（十位）：在个位有序基础上，按十位稳定排序，得 [802, 2, 24, 45, 170, 75, 90]。
   • 第3轮（百位）：最终得到有序数组 [2, 24, 45, 75, 90, 170, 802]。
     每轮结束后均满足“最低 \(k\) 位有序”的不变式。

总结
通过循环不变式证明，基数排序的每一轮处理均逐步扩大有序范围（从低位到高位），且稳定排序确保相等高位数时低位数顺序不变，最终实现全局有序。此证明方法适用于任何进制（如二进制、十六进制）的基数排序变种。