如何形式化证明GoodSort排序算法的不正确性

我拿到了如下排序算法，研究目标是严谨证明该算法的不正确性。仅靠举反例的证明方式深度不足，我希望找到更严谨的形式化证明路径。我之前考虑过用*数学归纳法（proof by induction）*开展证明，但过往只用该方法完成过算法正确性证明，还没有梳理清楚用它证明算法不正确的推导逻辑。

待验证的算法实现 #

GoodSort(A, left, right)
{
 if (A[left] > A[right]) 
   swap(A[left], A[right]);
 if (left+1 >= right) 
   return;
 pivot = floor((right-left+1)/3);
 GoodSort(A, left, right-pivot);
 GoodSort(A, left+pivot, right); 
}

形式化证伪的核心逻辑 #

用数学归纳法证伪算法，和证明正确性的思路方向完全相反：证明正确性是要通过归纳推导出「算法对所有规模输入都能输出正确结果」的全称命题为真；而证伪只需要证明这个全称命题为假——即存在至少一类可归纳扩展的输入，让算法永远无法输出正确结果，不需要证明算法对所有输入都失效。

归纳证伪的通用步骤为：

• 基础步：找到最小规模的失效输入，实际运行验证算法输出确实不符合排序要求
• 归纳步：假设某类结构的规模为k的输入会让算法失效，推导证明规模更大的同结构输入，会因为算法本身的逻辑缺陷必然失效，由此证明存在无穷多输入会触发算法错误，而非单个偶然的反例。

针对GoodSort的具体证明路径 #

该算法的核心缺陷是递归覆盖范围存在不可达的元素移动路径，可以围绕这个缺陷搭建归纳证明：

1. 明确算法的覆盖盲区：对于区间长度n = right-left+1 = 3m的场景，pivot = m：
   • 第一次递归仅处理[left, right-m]（前2m个元素），完全不触及[right-m+1, right-1]这m-1个位置的元素，初始操作仅交换区间两端left和right的元素，不会调整这m-1个位置的元素
   • 第二次递归仅处理[left+m, right]（后2m个元素），完全不触及[left, left+m-1]这m个位置的元素
     这就意味着：如果初始时[right-m+1, right-1]位置存在比[left, left+m-1]所有元素都小的元素，这些元素在第一次递归中不会被移动到左段；第二次递归最多能把这些小元素移动到left+m的位置，永远无法进入最左m个位置的区间，最终必然出现排序错误。
2. 基础步验证（最小失效规模n=6，m=2）：
   取输入数组[4,5,6,2,1,3]，逐行运行算法：
   • 初始调用GoodSort(0,5)：A[0]=4>A[5]=3，交换后数组为[3,5,6,2,1,4]；pivot=2，先调用GoodSort(0,3)处理前4个元素
   • 处理GoodSort(0,3)：A[0]=3>A[3]=2，交换后数组为[2,5,6,3,1,4]；pivot=1，递归处理后前4个元素排序为[2,3,5,6]，此时整体数组为[2,3,5,6,1,4]
   • 回到初始调用，执行第二个递归GoodSort(2,5)处理索引2-5的元素[5,6,1,4]，该递归完全不触及索引0、1的元素；处理完成后这四个元素变为[1,4,5,6]，最终整体数组为[2,3,1,4,5,6]
     最终输出存在1的位置在2、3之后的明显错误，基础步成立。
3. 归纳步推导：
   假设对于n=3m的同结构输入（即右段m-1个位置存在小于左段m个元素的小元素，且最小元素不在区间最右端），算法会输出错误结果。对于n=3(m+1)的同结构输入：
   • 第一次递归处理前2(m+1)个元素时，按照归纳假设，会在左段m+1个位置留存大于右段小元素的值
   • 第二次递归起点为left+m+1，完全不触及左段m+1个位置，右段的小元素最多被移动到left+m+1位置，无法进入左段区间
     因此规模为3(m+1)的同结构输入依然会输出错误结果。

由此即可完成严谨的形式化证伪，证明该算法不是正确的排序算法。

内容的提问来源于stack exchange，提问作者g77