排序算法之：循环不变式在 Stooge Sort 中的正确性证明

题目描述
Stooge Sort 是一种低效但有趣的递归排序算法，由 Howard、Fine 等人在《The Bogus Paradox》中提出。它的核心思想是：若数组前2/3部分已排序、后2/3部分已排序，且前1/3与后1/3部分通过一次交换调整后，整个数组将完全有序。我们需要通过循环不变式严格证明其正确性。

解题过程

1. 算法步骤回顾
Stooge Sort 的伪代码如下：

function stoogeSort(A, i, j):
  if A[i] > A[j]:
    swap A[i] and A[j]
  if (j - i + 1) > 2:
    t = (j - i + 1) // 3
    stoogeSort(A, i, j-t)    // 排序前2/3
    stoogeSort(A, i+t, j)    // 排序后2/3
    stoogeSort(A, i, j-t)    // 再次排序前2/3

2. 定义循环不变式
对于每次调用 stoogeSort(A, i, j)，定义循环不变式为：

执行结束后，子数组 A[i..j] 的所有元素会以非降序排列，且所有元素仍为原始元素的集合（排列不变性）。

3. 基础情况证明

• 情况1：子数组长度为1（即 i = j）
  无需任何操作，单元素自然有序，不变式成立。
• 情况2：子数组长度为2（即 j = i+1）
  通过一次比较交换可保证 A[i] ≤ A[j]，不变式成立。

4. 归纳步骤
假设对于所有长度小于 (j-i+1) 的子数组，算法能正确排序。现证明对长度 n = j-i+1 ≥ 3 的情况：

• 步骤1：比较交换 A[i] 和 A[j]
  确保全局最小值不会仅存在于最后1/3，全局最大值不会仅存在于前1/3。
• 步骤2：递归排序前2/3（A[i..j-t]）
  根据归纳假设，A[i..j-t] 被排序，且前1/3的最小值 ≤ 后1/3的最小值（因步骤1已调整）。
• 步骤3：递归排序后2/3（A[i+t..j]）
  此时后2/3被排序，且关键性质是：前1/3的最大值 ≤ 后2/3的最小值。这是因为：
  • 前1/3在步骤2后已有序，且其最大值不超过原数组前2/3的最大值；
  • 步骤2后，前2/3的最大值可能被移动到后1/3，但步骤3会将其正确归位到后2/3的末尾。
• 步骤4：再次排序前2/3（A[i..j-t]）
  由于步骤3可能将较大值移入前1/3，本次递归确保前2/3重新有序，同时保持前2/3的最大值 ≤ 后1/3的最小值。

5. 关键边界分析
定义三部分：

• P1 = A[i..i+t-1]（前1/3）
• P2 = A[i+t..j-t]（中1/3）
• P3 = A[j-t+1..j]（后1/3）

经过三次递归后：

• 第一次递归（前2/3）确保 P1 ∪ P2 有序，且 P1 的最大值 ≤ P3 的最小值（因步骤1交换）。
• 第二次递归（后2/3）确保 P2 ∪ P3 有序，且 P1 的最大值 ≤ P2 的最小值（因 P2 的最小值来自整个后2/3的最小值）。
• 第三次递归（前2/3）修复 P1 和 P2 的潜在乱序，最终使 P1 ≤ P2 ≤ P3。

6. 归纳结论
由数学归纳法，循环不变式对所有长度的子数组成立。因此算法终止时，整个数组有序。

总结
通过循环不变式，我们证明了 Stooge Sort 的递归调用能逐步将子数组划分为有序片段，并通过重叠递归确保全局有序。尽管其时间复杂度高达 O(n^log₁.₅3) ≈ O(n^2.7)，但此证明展示了如何用形式化方法分析递归排序的正确性。