排序算法之：循环不变式在快速选择算法（Quickselect）中的正确性证明（二次讲解）

字数 2281 2025-12-17 15:40:07

排序算法之：循环不变式在快速选择算法（Quickselect）中的正确性证明（二次讲解）

我将为您讲解快速选择算法（Quickselect） 的循环不变式证明，这是用于在未排序数组中找到第k小（或第k大）元素的高效算法。它基于快速排序的分区思想，但只递归处理包含目标的那一部分。

题目描述

给定一个无序数组arr和一个整数k（1 ≤ k ≤ n，n为数组长度），使用快速选择算法找到数组中第k小的元素。请使用循环不变式严格证明算法的正确性。

解题过程

1. 算法回顾

快速选择算法步骤如下：

选择一个基准元素（pivot）。
对数组进行分区，将小于基准的元素移到左边，大于基准的移到右边，基准放在最终位置pivotIndex。
比较pivotIndex与k：
- 如果pivotIndex == k-1，基准就是第k小元素，返回。
- 如果pivotIndex > k-1，递归在左半部分（arr[left..pivotIndex-1]）查找第k小元素。
- 如果pivotIndex < k-1，递归在右半部分（arr[pivotIndex+1..right]）查找第k - (pivotIndex - left + 1)小的元素。

它的平均时间复杂度为O(n)，最坏情况O(n²)。

2. 循环不变式的定义

我们重点关注分区过程的循环不变式。以典型的Lomuto分区为例：

指针i表示小于基准的区域的右边界（arr[left..i-1]元素 < pivot）。
指针j是遍历指针（arr[i..j-1]元素 ≥ pivot，arr[j..right-1]是未处理区域）。
基准元素pivot是arr[right]。

循环不变式：
在每次循环迭代开始时（for循环的每次j值），以下条件成立：

arr[left..i-1]中的所有元素都小于基准pivot。
arr[i..j-1]中的所有元素都大于或等于基准pivot。
arr[j..right-1]是尚未处理的元素。
arr[right]是基准元素pivot，尚未参与比较。

3. 循环不变式的证明

我们分三步证明：

a) 初始化
循环开始前，j = left，i = left。

区间arr[left..i-1]为空，条件1自然成立。
区间arr[i..j-1]也空（因为j-1 = left-1 < i），条件2成立。
未处理区间arr[j..right-1]就是整个数组除了最后一个元素（基准）。
基准arr[right]尚未处理。
所有条件满足，循环不变式成立。

b) 保持
假设在迭代j时不变式成立。现在处理元素arr[j]：

如果arr[j] < pivot：交换arr[i]和arr[j]，然后i++。交换后，arr[i-1]变为原arr[j]（< pivot），arr[i]变为原≥ pivot元素（或不变）。j++后：
- 条件1：arr[left..i-1]仍全< pivot（新增arr[i-1]）。
- 条件2：arr[i..j-1]（即arr[i..j-1]）中元素≥ pivot（因为被换到i位置的元素原在≥ pivot区，或j移动后该区可能为空）。
- 条件3：未处理区间缩小一位。
- 条件4：基准未动。
如果arr[j] ≥ pivot：仅j++。此时arr[i..j-1]扩大一位（包含arr[j]），该元素≥ pivot，其他区间不变。所有条件保持。
因此，迭代后循环不变式仍成立。

c) 终止
循环结束时j = right。此时：

未处理区间arr[j..right-1]为空。
由不变式1、2：arr[left..i-1]全< pivot，arr[i..right-1]全≥ pivot。
最后交换arr[i]和arr[right]（基准）。交换后：
- arr[left..i-1] < pivot。
- arr[i] = pivot。
- arr[i+1..right] ≥ pivot。
  因此，pivot位于其最终排序位置pivotIndex = i，左侧元素均小于它，右侧均大于等于它。分区正确性得证。

4. 递归正确性证明

分区正确性保证了每次递归时：

如果pivotIndex == k-1，则pivot恰好是第k小元素（因为左侧有pivotIndex个更小的元素）。
如果pivotIndex > k-1，则第k小元素一定在左半部分（它小于pivot，且在左侧的pivotIndex个最小元素之中）。
如果pivotIndex < k-1，则第k小元素一定在右半部分（它大于等于pivot，且是右半部分中第k - (pivotIndex + 1)小的元素）。

这个性质在递归中保持不变，直到找到目标。因此，算法整体正确。

总结

通过分区过程的循环不变式，我们严格证明了快速选择算法的正确性：

分区将数组划分为“小于基准”和“大于等于基准”两部分，且基准就位。
递归时，目标元素所在的区间被正确识别和缩小。
最终，基准位置恰好等于k-1时，算法返回正确结果。

此证明不仅适用于Lomuto分区，稍作调整也适用于Hoare分区等其他变体，是理解快速选择算法的核心理论基础。

排序算法之：循环不变式在快速选择算法（Quickselect）中的正确性证明（二次讲解）我将为您讲解快速选择算法（Quickselect）的循环不变式证明，这是用于在未排序数组中找到第k小（或第k大）元素的高效算法。它基于快速排序的分区思想，但只递归处理包含目标的那一部分。题目描述给定一个无序数组 arr 和一个整数 k （1 ≤ k ≤ n，n为数组长度），使用快速选择算法找到数组中第k小的元素。请使用循环不变式严格证明算法的正确性。解题过程 1. 算法回顾快速选择算法步骤如下：选择一个基准元素（pivot）。对数组进行分区，将小于基准的元素移到左边，大于基准的移到右边，基准放在最终位置 pivotIndex 。比较 pivotIndex 与 k ：如果 pivotIndex == k-1 ，基准就是第k小元素，返回。如果 pivotIndex > k-1 ，递归在左半部分（ arr[left..pivotIndex-1] ）查找第k小元素。如果 pivotIndex < k-1 ，递归在右半部分（ arr[pivotIndex+1..right] ）查找第 k - (pivotIndex - left + 1) 小的元素。它的平均时间复杂度为O(n)，最坏情况O(n²)。 2. 循环不变式的定义我们重点关注分区过程的循环不变式。以典型的Lomuto分区为例：指针 i 表示小于基准的区域的右边界（ arr[left..i-1] 元素 < pivot）。指针 j 是遍历指针（ arr[i..j-1] 元素 ≥ pivot， arr[j..right-1] 是未处理区域）。基准元素 pivot 是 arr[right] 。循环不变式：在每次循环迭代开始时（ for 循环的每次 j 值），以下条件成立： arr[left..i-1] 中的所有元素都小于基准 pivot 。 arr[i..j-1] 中的所有元素都大于或等于基准 pivot 。 arr[j..right-1] 是尚未处理的元素。 arr[right] 是基准元素 pivot ，尚未参与比较。 3. 循环不变式的证明我们分三步证明： a) 初始化循环开始前， j = left ， i = left 。区间 arr[left..i-1] 为空，条件1自然成立。区间 arr[i..j-1] 也空（因为 j-1 = left-1 < i ），条件2成立。未处理区间 arr[j..right-1] 就是整个数组除了最后一个元素（基准）。基准 arr[right] 尚未处理。所有条件满足，循环不变式成立。 b) 保持假设在迭代 j 时不变式成立。现在处理元素 arr[j] ：如果 arr[j] < pivot ：交换 arr[i] 和 arr[j] ，然后 i++ 。交换后， arr[i-1] 变为原 arr[j] （< pivot）， arr[i] 变为原≥ pivot元素（或不变）。 j++ 后：条件1： arr[left..i-1] 仍全< pivot（新增 arr[i-1] ）。条件2： arr[i..j-1] （即 arr[i..j-1] ）中元素≥ pivot（因为被换到 i 位置的元素原在≥ pivot区，或 j 移动后该区可能为空）。条件3：未处理区间缩小一位。条件4：基准未动。如果 arr[j] ≥ pivot ：仅 j++ 。此时 arr[i..j-1] 扩大一位（包含 arr[j] ），该元素≥ pivot，其他区间不变。所有条件保持。因此，迭代后循环不变式仍成立。 c) 终止循环结束时 j = right 。此时：未处理区间 arr[j..right-1] 为空。由不变式1、2： arr[left..i-1] 全< pivot， arr[i..right-1] 全≥ pivot。最后交换 arr[i] 和 arr[right] （基准）。交换后： arr[left..i-1] < pivot 。 arr[i] = pivot 。 arr[i+1..right] ≥ pivot 。因此， pivot 位于其最终排序位置 pivotIndex = i ，左侧元素均小于它，右侧均大于等于它。分区正确性得证。 4. 递归正确性证明分区正确性保证了每次递归时：如果 pivotIndex == k-1 ，则 pivot 恰好是第k小元素（因为左侧有 pivotIndex 个更小的元素）。如果 pivotIndex > k-1 ，则第k小元素一定在左半部分（它小于 pivot ，且在左侧的 pivotIndex 个最小元素之中）。如果 pivotIndex < k-1 ，则第k小元素一定在右半部分（它大于等于 pivot ，且是右半部分中第 k - (pivotIndex + 1) 小的元素）。这个性质在递归中保持不变，直到找到目标。因此，算法整体正确。总结通过分区过程的循环不变式，我们严格证明了快速选择算法的正确性：分区将数组划分为“小于基准”和“大于等于基准”两部分，且基准就位。递归时，目标元素所在的区间被正确识别和缩小。最终，基准位置恰好等于k-1时，算法返回正确结果。此证明不仅适用于Lomuto分区，稍作调整也适用于Hoare分区等其他变体，是理解快速选择算法的核心理论基础。