排序算法之：循环不变式在样本排序（Sample Sort）中的正确性证明

我将为你详细讲解“样本排序”算法的循环不变式及其正确性证明。这个证明能帮助你深入理解样本排序的核心逻辑和可靠性。

1. 题目描述

样本排序（Sample Sort）是一种高效的并行排序算法，常用于分布式和大规模数据处理。它基于“分而治之”思想，但通过采样来智能地划分数据，以减少负载不均的问题。本题目要求我们为样本排序的关键循环（特别是分区阶段）设计并证明循环不变式，从而严谨地论证算法的正确性。

算法核心思想：

1. 采样：从整个数据集中随机抽取少量样本。
2. 排序样本：对样本进行排序，选出p-1个“分割元素”（splitters），将数据范围划分为p个桶。
3. 分区：根据分割元素，将原始数据划分到这p个桶中。
4. 局部排序：每个桶独立排序。
5. 合并：按桶顺序拼接结果。

我们将重点放在分区阶段的循环不变式证明上，因为这是保证每个元素被正确分配到对应桶的关键。

2. 算法步骤详述

假设我们有：

• 输入数组：A[0..n-1]
• 桶数量：p（假设p=3为例简化）
• 分割元素：S[0..p-2]（已排序的样本，例如S[0]=30, S[1]=60）
• 桶数组：Bucket[0..p-1]，每个桶是一个动态数组。

分区阶段伪代码：

for i = 0 to n-1:
    element = A[i]
    // 找到element应属的桶编号bucket_id
    bucket_id = 0
    while bucket_id < p-1 and element > S[bucket_id]:
        bucket_id++
    // 将element加入Bucket[bucket_id]

3. 循环不变式的设计与解释

我们针对上述for循环（遍历A中每个元素）定义循环不变式。

循环不变式：
在循环的每次迭代开始时（即处理A[i]之前），以下条件成立：

1. 已处理元素已正确分配：所有已处理的元素A[0..i-1]都已被放入正确的桶中。即，对于任意已处理的元素x：
   • 如果x ≤ S[0]，则x在Bucket[0]中。
   • 如果S[k-1] < x ≤ S[k]（对于1 ≤ k ≤ p-2），则x在Bucket[k]中。
   • 如果x > S[p-2]，则x在Bucket[p-1]中。
2. 桶内顺序保持：每个桶内元素的相对顺序与在原始数组A中的出现顺序一致（即稳定排序属性）。

解释：

• 不变式1确保“正确性”：每个元素根据分割元素被分配到正确的区间桶。
• 不变式2确保“稳定性”：算法是稳定的，即相等元素的原始顺序得以保留。

4. 循环不变式的证明

我们通过初始化、保持、终止三步来证明。

步骤1：初始化（循环开始前）

• 此时i=0，已处理元素集合A[0..-1]为空。
• 不变式1中“所有已处理元素已正确分配”自然成立（因为没有元素需要检查）。
• 不变式2中“桶内顺序保持”也自然成立（因为所有桶为空）。
  ✅ 因此，循环不变式在初始化时成立。

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

假设在迭代i开始时（处理A[i]前），不变式成立。我们执行迭代i：

• 我们取当前元素element = A[i]。
• 通过while循环（或二分查找）确定bucket_id，使得：
  • 如果bucket_id=0，则element ≤ S[0]。
  • 如果1 ≤ bucket_id ≤ p-2，则S[bucket_id-1] < element ≤ S[bucket_id]。
  • 如果bucket_id = p-1，则element > S[p-2]。
• 将element追加到Bucket[bucket_id]的末尾。

证明迭代后不变式仍成立：

1. 已处理元素正确分配：
   • 此前已处理的元素A[0..i-1]已满足条件（归纳假设）。
   • 新处理的A[i]根据查找逻辑被放入满足上述区间条件的桶中，因此也满足正确分配条件。
2. 桶内顺序保持：
   • 此前每个桶内元素顺序与在A中的顺序一致（归纳假设）。
   • 我们将A[i]追加到对应桶的末尾，而A[i]在原数组中的索引i大于该桶中已有元素的所有索引（因为我们是按A的顺序遍历的），因此桶内顺序保持不变。

✅ 因此，迭代后不变式仍然成立。

步骤3：终止（循环结束时）

• 循环结束时i=n，已处理元素为A[0..n-1]（即所有元素）。
• 根据不变式1，所有元素都已被正确分配到对应的桶中。
• 根据不变式2，每个桶内元素保持原始相对顺序。

✅ 因此，分区阶段结束后，算法保证了：

1. 全局有序性：Bucket[0]的所有元素 ≤ Bucket[1]的所有元素 ≤ ... ≤ Bucket[p-1]的所有元素。
2. 稳定性：每个桶内元素保持原始顺序。

5. 整体正确性论证

分区阶段的循环不变式保证了元素被正确划分到桶中。后续步骤：

• 局部排序：每个桶独立排序（使用任意稳定排序算法，如归并排序）。
• 合并：按桶顺序拼接，由于桶间已有序，且桶内排序稳定，最终得到全局有序且稳定的排序结果。

关键点：

• 采样阶段选择的S分割元素将值域划分为p个区间，循环不变式确保了分区严格遵循这些区间。
• 稳定性由“追加到桶末尾”和桶内稳定排序共同保证。

6. 思考与延伸

• 为什么采样是有效的？ 如果样本能代表整体数据分布，则各桶大小均衡，避免负载不均。
• 循环不变式如何推广？ 该证明可扩展至并行版本，其中每个处理器负责一个桶，不变式需在并发环境下考虑同步。
• 与快速排序分区对比：快速排序的分区依据是随机选择的枢轴，而样本排序使用多个分割元素，形成多个桶，更适合并行处理。

通过上述循环不变式的证明，我们严谨地确保了样本排序分区阶段的正确性，这是整个算法可靠性的基石。