排序算法之：循环不变式在快速选择算法（Quickselect）中的正确性证明
题目描述
快速选择算法（Quickselect）是一种用于在未排序列表中查找第k小（或第k大）元素的高效选择算法。它是快速排序算法的一个变体，通过“分而治之”的策略，每次只递归地处理包含目标元素的那一部分数组，从而实现平均时间复杂度为 O(n)。然而，其正确性并不直观，特别是如何保证每次划分后，目标元素一定在正确的区间内。本题要求通过定义并维护循环不变式，来形式化地证明快速选择算法的正确性。具体来说，我们将关注算法核心的划分（Partition）过程以及递归选择过程，证明它们始终能正确地缩小搜索范围，最终找到第k小的元素。
解题过程循序渐进讲解
1. 算法回顾与问题定义
首先，明确算法输入：一个包含n个元素的数组A[0..n-1]，以及一个整数k（1 ≤ k ≤ n）。目标是找到数组中第k小的元素（为简化，我们假设数组元素互异，但原理可扩展）。
快速选择算法的基本步骤：
- 选择一个“基准”（pivot）元素。
- 执行划分（Partition）操作：将数组重新排列，使得所有小于基准的元素位于其左侧，所有大于基准的元素位于其右侧，基准位于最终位置p。
- 比较基准的最终索引p与k：
- 如果 p == k-1，则基准即为第k小元素，返回它。
- 如果 p > k-1，则在左子数组A[0..p-1]中递归查找第k小元素。
- 如果 p < k-1，则在右子数组A[p+1..n-1]中递归查找第(k-p-1)小元素。
我们的证明目标：算法结束时，返回的元素确实是数组中的第k小元素。
2. 划分（Partition）过程的循环不变式
快速选择依赖于一个关键的划分子程序（以Lomuto划分或Hoare划分为例，这里以经典的Lomuto划分进行说明）。我们首先为划分过程定义循环不变式，以证明划分的正确性。
划分过程的目标：给定数组A[l..r]和基准值pivot（通常选A[r]），重新排列数组，使得对于某个索引p（l ≤ p ≤ r）：
- 对于任意 i ∈ [l, p-1]，有 A[i] ≤ pivot。
- 对于任意 j ∈ [p+1, r]，有 A[j] > pivot。
- A[p] = pivot。
循环不变式定义：在划分主循环的每次迭代开始前，维护以下三个区域：
- 已处理小元素区 A[l..i]：所有元素 ≤ pivot。
- 已处理大元素区 A[i+1..j-1]：所有元素 > pivot。
- 未处理区 A[j..r-1]：尚未处理的元素。
其中，i和j是循环变量，初始时 i = l-1, j = l。
形式化描述：
- 初始化：当循环开始时，i = l-1, j = l。此时“小元素区”和“大元素区”均为空，未处理区为A[l..r-1]。不变式显然成立，因为没有元素被错误分类。
- 保持：假设在迭代开始前不变式成立。检查当前元素A[j]：
- 如果A[j] ≤ pivot，则交换A[i+1]和A[j]，然后i增加1。这样A[j]被移入小元素区末尾，大元素区整体右移一位，j增加1后未处理区缩小。交换后，小元素区所有元素仍≤pivot，大元素区所有元素>pivot，不变式保持。
- 如果A[j] > pivot，则仅将j增加1。这样A[j]被隐式扩展到大元素区末尾，未处理区缩小。不变式同样保持。
- 终止：当循环结束（j = r）时，未处理区为空。此时小元素区为A[l..i]，大元素区为A[i+1..r-1]。最后，交换A[i+1]和A[r]（pivot），将基准放置到正确位置p = i+1。交换后，由于A[r]（原pivot）被换到中间，而A[l..p-1]（原小元素区）的所有元素≤pivot，A[p+1..r]（原大元素区+被交换来的原A[r]）的所有元素>pivot。因此，划分后数组满足目标性质。
结论：划分过程结束时，基准被放置在正确排序位置p，且左侧所有元素 ≤ 基准，右侧所有元素 > 基准。
3. 快速选择主算法的循环不变式（递归不变量）
现在，我们为整个快速选择算法定义一个递归不变量，它本质上是在每次递归调用时都必须保持的性质，以保证算法的正确性。
不变式定义：在快速选择算法的任何递归调用中，假设我们正在子数组A[left..right]中寻找第k_small小的元素（其中k_small是相对于当前子数组的秩，1 ≤ k_small ≤ length），那么以下性质必须成立：
- 原数组A[0..n-1]中第k小的元素，一定存在于当前子数组A[left..right]中。
- 在当前子数组中，第k_small小的元素，就是原数组中第k小的元素。
初始化：第一次调用时，left=0, right=n-1, k_small = k。子数组是整个数组，显然第k小的元素在其中，且就是要找的元素。不变式成立。
保持：假设在某次递归调用开始时不变量成立。我们执行划分操作，得到基准的最终位置p（相对于当前子数组的索引）。根据划分的正确性，我们知道：
- 基准元素是当前子数组中第 (p - left + 1) 小的元素。
- 所有小于基准的元素都在A[left..p-1]中，所有大于基准的元素都在A[p+1..right]中。
现在比较 (p - left + 1) 与 k_small：
- 如果相等，则基准正是当前子数组中第k_small小的元素，由不变式（2），它也是原数组中第k小的元素。算法返回，正确性得证。
- 如果 (p - left + 1) > k_small，说明第k_small小的元素在左子数组A[left..p-1]中。我们在左子数组中递归查找，此时新的k_small' = k_small（因为目标在左子数组中的秩不变）。我们需要验证不变式在递归调用中是否保持：
- 左子数组A[left..p-1]中的元素都小于基准，而基准是当前子数组中第 (p-left+1) 小的元素，且 (p-left+1) > k_small。因此，原数组中第k小的元素（由不变式保证在当前子数组中，且秩为k_small）必然小于基准，所以它一定在左子数组中。即，性质（1）保持。
- 在左子数组中，第k_small小的元素（相对于左子数组）就是原数组第k小的元素，因为左子数组保持了原数组的原有顺序（只是被划分了）。性质（2）保持。
- 如果 (p - left + 1) < k_small，说明第k_small小的元素在右子数组A[p+1..right]中。我们在右子数组中递归查找，此时新的k_small' = k_small - (p - left + 1)（因为跳过了左子数组和基准共 (p-left+1) 个更小的元素）。类似地，可以验证：
- 右子数组中的元素都大于基准，而目标元素的秩k_small大于基准的秩，所以它必然在右子数组中。性质（1）保持。
- 在右子数组中，第k_small'小的元素（相对于右子数组）就是原数组第k小的元素，因为右子数组的元素顺序也得以保持。性质（2）保持。
终止：算法在某个递归调用中，当 (p - left + 1) == k_small 时终止，返回基准元素。由保持性证明可知，此时返回的元素正是原数组的第k小元素。递归总会终止，因为每次调用子数组的规模至少减小1（基准被排除）。
4. 总结
通过为划分过程定义循环不变式，我们确保了每次划分都能正确地将基准放置到其最终排序位置，并将数组分为小于和大于基准的两部分。接着，为快速选择主算法定义递归不变量，我们证明了在每次递归调用中，目标元素始终位于当前的搜索子数组中，并且其相对秩保持不变。这两个不变式共同保证了快速选择算法最终能正确找到第k小的元素。
延伸思考：此证明假设了数组元素互异。当存在重复元素时，若使用三路划分（将数组分为小于、等于、大于三部分），可以类似定义不变式并证明，只需调整k的比较逻辑（若k落在等于基准的区间内，则直接返回基准）。