证明归并排序输出输入的排列

Posted 2023-03-27

【中文标题】证明归并排序输出输入的排列

【英文标题】：Prove that merge sort outputs a permutation of the input

【发布时间】：2020-02-26 04:37:00

【问题描述】：

我开始研究计算逻辑，作为练习，我想证明归并排序算法的正确性。

目前，我很难证明该算法的输出将始终对应于给定输入的排列。

如果有人能帮我解决这个问题，我会很高兴。

非常感谢????

【问题讨论】：

任何类型的输出都是输入的排列。如果不是，则排序被破坏。

没有人对此提出异议，吉姆。这个问题是关于证明合并排序没有被破坏。

【参考方案1】：

这个证明的核心需要证明“合并”过程将每个元素插入一次且仅一次插入结果中。由于合并过程使用循环工作，因此您需要使用loop invariant 来显示这一点。

循环不变量通常可以通过询问“我知道什么中途循环？”来发现？

to merge arrays A and B:
    let n = length of A, m = length of B
    let R = new array of length (n + m)
    let i = 0, j = 0
    while i < n or j < m:
        if i < n and (j == m or A[i] <= B[j]):
            R[i+j] = A[i]
            i = i + 1
        else:
            R[i+j] = B[j]
            j = j + 1
    return R

在这个循环中，我们总是知道 R 的前 i+j 个元素是 A 的前 i 个元素和 B 的前 j 个元素的某种排列。这就是循环不变量，所以你需要证明：

在循环开始之前（当 i = j = 0 时）是这样。 如果在循环迭代之前为真，那么在该迭代之后它仍然为真，即保留不变量。 如果循环终止时（当 i = m，j = n）为真，则数组 R 具有所需的属性。

一般而言，此类证明的难点在于发现循环不变量，并表明循环的每次迭代都保留了不变量。

【讨论】：

"在这个循环中，我们总是知道 R 的前 i+j 个元素是 A 的前 i 个元素和 B 的前 j 个元素的某种排列。"这个证明不需要证明 A 和 B 是从 R 作为引理构造的吗？也可能需要使A和B的交集为空集的循环不变量之一。很好的答案，+1。

合并排序不要求输入数组不包含重复项，因此数组 A 和 B 不需要不相交（如果您做出此假设，证明并不容易）。对于具有重复元素的序列，排列的概念是明确定义的。在我给出的伪代码中，R 是由 A 和 B 构成的，而不是相反；但是，如果您的意思是还需要证明 A 和 B 从输入列表中获取它们的值，那么您当然是对的。完整的证明需要更多细节；我只是专注于这个答案的主要任务。

tbh 证明定理和构造引理一直是我的弱点。几年前，我不得不在大学证明传递闭包算法的有效性，教授不得不握住我的手。我也从未想过迭代地（“自下而上”）而不是递归地进行合并排序，所以当我回答时，我脑子里有一个特定版本的算法。 （传递闭包证明只是嵌套循环。我从未证明递归算法的正确性，只是通过成绩实现它们。）

【参考方案2】：

归并排序的前提是什么？什么是岗位条件？你有任何循环不变量吗？

在您开始编写证明之前，您必须问自己三个问题。

那么：您的基本情况是什么？如果您正在处理证明，大概您知道合并排序是如何工作的，那么当您将一个长度为 1 的数组传递给合并排序函数时会发生什么？那里的后置条件是什么？

这里有一个decent primer from Berkeley，关于如何证明函数的正确性。编写证明可能需要一些离散数学（归纳）。

【讨论】：

在不知道算法/实现的细节，甚至自顶向下与自底向上的情况下，如何证明在某些辅助缓冲区或临时存储中没有数据丢失，并且所有输入元素都结束在输出元素中（通常返回输入）？我认为此问题未考虑用户定义的比较函数引发异常等潜在问题。

@rcgldr 我有点困惑，你的意思是如何证明算法将被其执行的软件和硬件正确实现？

我的意思是如何在不求助于某些实现特定细节的情况下证明算法。例如，归并排序的 Wiki 描述：“将未排序的列表分成 n 个子列表，每个子列表包含一个元素（一个元素的列表被认为已排序）。重复合并子列表以产生新的排序子列表，直到只剩下一个子列表。这将是排序列表。”然后是kaya3的回答，就是merge的具体实现。

一般来说，你需要选择一个实现，或者一个伪代码实现，有足够具体的东西来证明任何结果。但是，如果您可以为一种实现证明它，那么您的证明方法可能会以一种直接的方式适用于其他实现。例如，循环不变量将是相同的（但可能以不同的符号编写）。

@kaya3 假设您进行了递归分而治之，这将如何使证明变得复杂（或简化）？我的答案是递归算法，它具有单个元素的基本情况（根据定义，这显然是一个排序数组）。