排序算法之：循环不变式在鸽巢排序（Pigeonhole Sort）中的正确性证明

题目描述
鸽巢排序（Pigeonhole Sort）是一种非比较型整数排序算法，适用于待排序元素的范围已知且范围大小（max - min + 1）与元素数量相近的情况。其核心思想是：若存在 n 个鸽巢和 m 只鸽子（m ≤ n），且每个鸽巢最多容纳一只鸽子，则通过将鸽子放入对应鸽巢，即可自然完成排序。现在需要利用循环不变式严格证明该算法的正确性，确保排序后数组满足升序性质。

解题过程

1. 算法步骤回顾

1. 遍历数组，找到最小值 min 和最大值 max。
2. 创建鸽巢数组 pigeonholes，大小为 range = max - min + 1，初始化为空（或0）。
3. 放置阶段：遍历原数组，将元素 arr[i] 放入鸽巢 pigeonholes[arr[i] - min]（记录出现次数或直接放置）。
4. 收集阶段：顺序遍历鸽巢数组，将非空鸽巢中的元素放回原数组。

示例（简化版，鸽巢记录元素值）：

原数组: [5, 2, 5, 1, 3]  
min=1, max=5, range=5  
鸽巢索引: 0->1, 1->2, 2->3, 3->4, 4->5  
放置后鸽巢: [1, 2, 3, null, 5]（第二个5覆盖第一个，需处理重复值）  
收集后: [1, 2, 3, 5, 5]

2. 定义循环不变式

选择收集阶段的循环作为证明对象。设循环变量为 i（当前鸽巢索引），k（原数组当前写入位置）。
循环不变式：在每次迭代开始时，原数组的前 k 个元素是已收集的最小到第 k 小的元素，且按升序排列。

具体条件：

1. 子数组 arr[0 : k-1] 已排序。
2. arr[0 : k-1] 中的元素是鸽巢索引 0 到 i-1 对应的所有元素（若鸽巢非空）。
3. 每个鸽巢中的元素值 ≥ min + i（因当前索引 i 对应值 min + i）。

3. 证明过程

初始化（循环开始前）：

• 此时 i = 0, k = 0。
• arr[0 : -1] 为空数组，自然有序（条件1满足）。
• 空数组包含鸽巢 0 到 -1 的元素（无鸽巢，条件2真空满足）。
• 所有鸽巢值 ≥ min + 0（条件3成立）。
  不变式成立。

保持（每次迭代后不变式仍成立）：

• 设当前鸽巢 i 中有 count 个值为 min + i 的元素。
• 若 count > 0，将 count 个 min + i 写入 arr[k : k+count-1]。
• 由于前 k 个元素已排序，且 min + i 是当前未处理的最小值（鸽巢按索引升序遍历），因此新元素 ≥ 已收集的最大值（条件1保持）。
• 新收集的元素对应鸽巢 i，加入后 arr[0 : k+count-1] 包含鸽巢 0 到 i 的所有元素（条件2保持）。
• 剩余鸽巢索引 ≥ i+1，其值 ≥ min + i + 1 > 已收集元素（条件3保持）。
• 更新 k += count, i += 1，进入下一迭代。

终止（循环结束时）：

• 循环结束条件为 i = range（所有鸽巢处理完毕）。
• 此时 arr[0 : k-1] 包含所有鸽巢（索引 0 到 range-1）的元素，即所有原数组元素（条件2）。
• 结合条件1，arr[0 : k-1] 已按升序排列，且 k = n（所有元素已收集）。
  算法正确性得证。

4. 关键点与边界处理

• 重复元素：鸽巢需记录出现次数（例如用计数器），保证重复值被完整收集。
• 空鸽巢：跳过空鸽巢不影响不变式（条件2允许鸽巢为空）。
• 范围优化：当 range 远大于 n 时，鸽巢排序空间效率低，此时不适用该算法。

总结
通过循环不变式证明了鸽巢排序的收集阶段能保证输出有序性，其核心依赖于鸽巢索引与元素值的映射关系以及顺序收集的单调性。该证明方法强调了非比较排序算法中数据分布与顺序处理的内在逻辑。