问题标签 [proof-of-correctness]

我无法证明 Gayle Shapley 算法的正确性证明所需的引理，用于稳定婚姻问题。

引理在算法中，每个男孩 A 只被对 A 不可行的女孩拒绝。

书中的证明是通过归纳法进行的。

我们通过归纳证明引理。考虑波士顿池算法的任意一轮，其中医生 α 拒绝一家医院 A 而选择另一家医院 B。拒绝意味着 α 更喜欢 B 而不是 A。在 B 的偏好列表中出现高于 α 的每个医生都已经拒绝了 B，因此，根据归纳假设，对于 B 是不可行的。现在考虑将 α 分配给 A 的任意匹配。我们已经确定 α 比 A 更喜欢 B。如果 B 比它的伙伴更喜欢 α，则匹配是不稳定的。另一方面，如果 B 更喜欢它的伙伴而不是 α，那么（根据我们之前的论点）它的伙伴是不可行的，并且匹配也是不稳定的。我们得出结论，不存在将 α 分配给 A 的稳定匹配。

在这里，医院对应于男孩（他们按优先级递减顺序提出），而医生对应于女孩。

有人可以解释引理和证明。

假设我们有一个排序方法：

我们可以使用哪些方法来证明排序算法对数组 a 进行了正确或错误的排序？有没有解决这个问题的系统方法？我知道它适用于 size_a == 1 和 size_a == 2 的情况，但如果 size_a 是 30，那么我们将递归地调用 ~2/3 大小的数组的排序方法。看起来好像它有效，但我不确定如何正式展示它。

我写了下面的代码大纲，基本上是对一个数组 (a) 求和，其中每个元素都乘以一个值 x^i：

请注意，我不希望代码编译 - 它只是代码应该如何工作的合理概述。我需要通过使用跟踪变量来提高代码的效率，因此需要使用链接不变量将所述变量与代码的其余部分连接起来。这就是我卡住的地方。在这种情况下跟踪什么有用？我曾考虑在每次迭代中保留总和值，但我不确定这是否有效。如果我能弄清楚要跟踪什么，我很确定将它链接到空间将是微不足道的。谁能看到我的算法如何通过跟踪变量得到改进？

我正在努力学习证据。我遇到了这4个术语。我正在尝试将所有内容联系起来。

和

一切之间的关系是什么？帮助表示赞赏。

我了解如何使用 Coq 和 Idris 之类的语言来证明用这些语言编写的程序的属性（根据我在该主题上的一点经验来判断。），但我想知道是否有一种平易近人的方法可以在已经存在的外部做同样的事情代码库。

有没有办法使用像 Coq 这样的工具或其他一些专门的工具来证明用 C++ 编写的算法的正确性？如果是这样，这样做的要求是什么？

大多数证明助手都是具有依赖类型的函数式编程语言。他们可以证明程序/算法。相反，我对最适合数学且仅适用于数学的证明助手感兴趣（例如微积分）。你能推荐一个吗？我听说过 Mizar，但我不喜欢源代码是封闭的，但如果它最适合数学，我会使用它。Agda 和 Idris 等新语言在多大程度上适合数学证明？

维基百科页面https://en.wikipedia.org/wiki/Reverse-delete_algorithm（在页面底部）中提供的这个证明是否正确？

伪代码

证明由两部分组成。首先，证明了算法应用后剩余的边形成了生成树。其次，证明了生成树的权重最小。

生成树

算法生成的剩余子图 (g) 没有断开连接，因为算法在第 7 行检查了它。结果子图不能包含循环，因为如果它包含循环，那么当沿着边移动时，我们会遇到最大边在循环中，我们将删除该边。因此 g 必须是主图 G 的生成树。

极简主义

我们通过归纳证明以下命题 P 是正确的：如果 F 是在 while 循环结束时保留的边集，则存在一些最小生成树（它的边）是 F 的子集。

显然 P 在 while 循环开始之前成立。因为加权连通图总是有一个最小生成树，并且因为 F 包含图的所有边，所以这个最小生成树必须是 F 的一个子集。

现在假设 P 对于某些非最终边集 F 为真，并令 T 是包含在 F 中的最小生成树。我们必须证明，在算法中删除边 e 之后，存在一些（可能是其他的）生成树 T'，它是 F 的子集。

如果下一个删除的边 e 不属于 T 则 T=T' 是 F 的子集并且 P 成立。.

否则，如果 e 属于 T：首先请注意，该算法仅删除不会导致 F 中的断开连接的边。所以 e 不会导致断开连接。但是删除 e 会导致树 T 断开连接（因为它是 T 的成员）。假设 e 将 T 分成子图 t1 和 t2 。由于删除 e 后整个图是连通的，因此在 t1 和 t2 之间必须存在一条路径（除 e 之外），因此 F 中必须存在一个循环 C（在删除 e 之前）。现在我们必须在这个循环中有另一个边（称为 f），它不在 T 中，但它在 F 中（因为如果所有循环边都在树 T 中，那么它就不再是树了）。我们现在声称 T' = T - e + f 是作为 F 子集的最小生成树。

首先我们证明 T' 是一棵生成树。我们知道，通过删除树中的一条边并添加另一条不会导致循环的边，我们会得到另一棵具有相同顶点的树。因为 T 是生成树，所以 T' 也必须是生成树。因为添加“f”不会导致任何循环，因为删除了“e”。（注意树 T 包含图的所有顶点）。

其次，我们证明 T' 是最小生成树。对于边“e”和“f”，我们有三种情况。wt 是权重函数。

wt( f ) < wt( e ) 这是不可能的，因为这会导致树 T' 的权重严格小于 T。由于 T 是最小生成树，这根本是不可能的。

wt( f ) > wt( e ) 这也是不可能的。从那时起，当我们以边缘权重的递减顺序遍历边缘时，我们必须首先看到“f”。因为我们有一个循环 C，所以删除“f”不会导致 F 中的任何断开连接。所以算法会更早地将它从 F 中删除。所以“f”在 F 中不存在，这是不可能的（我们已经证明 f 在步骤 4 中存在。

所以 wt(f) = wt(e) 所以 T' 也是最小生成树。所以 P 再次成立。所以当 while 循环完成时 P 成立（也就是当我们看到所有边时）并且我们在最后证明了 F 成为一棵生成树，并且我们知道 F 有一个最小生成树作为它的子集。所以 F 必须是最小生成树本身。

编辑

实际上我对段落“首先我们证明 T' 是一棵生成树”和部分“我们在最后证明 F 变成一棵生成树并且我们知道 F 有一个最小生成树作为它的子集。所以 F 必须是最小生成树本身

我应该通过归纳来证明一个算法，并且对于所有 n >= 0 ，它返回 3 ⁿ - 2 ^{n 。这是用 Eiffel 编写的算法。}

我的理解是，你分三步证明。基本步骤、归纳假设和完整性证明。这就是我目前所拥有的。

基础：

P(0) 返回 0，并且 3 ⁰ - 2 ⁰ = 0。

P(1) 返回 1，并且 3 ¹ - 2 ¹ = 1。

归纳假设：

假设 P(k)对于 0 <= k < n返回 3 ^k - 2 ^{k 。}

完整性证明：

对于 n，P(n) 返回 5(P(n-1)) - 6(P(n-2))

5(P(n-1)) - 6(P(n-2))

5(3 ^n-1 - 2 ^n-1 ) - 6(3 ^n-2 - 2 ^n-2 ) <- 基于归纳假设

这是我卡住的部分。我到底应该如何将其减少到看起来像 3 ⁿ - 2 ⁿ？

我需要一个算法来找到一棵树的直径，结果如下：选择一个任意顶点 y 并运行广度优先搜索以找到距离 y 最远的顶点，将其命名为 x，然后在 x 上运行 BFS 以找到最远的顶点从 x，称它为 z，这个距离 d(x,z) 就是直径。

但是，我不明白为什么 x 必须位于具有最大直径的顶点对中。我找到了正确性证明：图论中树直径的算法，其中建议通过矛盾证明，假设某些 d(u,v) 大于 d(x,z)。然后可以对这些情况进行区分：

1. 从 u 到 v 的路径与从根到 x 的路径相交
2. 从 u 到 v 的路径不与从根到 x 的路径相交

知道从 u 到 v 的路径上有一些顶点 h 是“最高的”（最接近根），应该可以证明这两种情况 d(u,v) 不能大于 d( x,z)。

但我不明白“根”是什么（这是 y 吗？），尽管有提示，但我看不出它为什么是真的。我不需要正式的证明，但我想了解为什么该算法是正确的。

我正在关注 Coursera 上的 Scala 函数式编程讲座，在视频 5.7 的结尾，Martin Odersky 要求通过归纳证明以下等式的正确性：

当涉及多个列表时如何处理归纳证明？

我检查了 xs 为 Nil 和 ys 为 Nil 的基本情况。我已经通过归纳证明，当 xs 被 x::xs 替换时，等式成立，但是我们是否还需要检查 ys 被 y::ys 替换的等式？

在那种情况下（不会过多地破坏练习......无论如何都没有评分）你如何处理：(xs ++ (y::ys)) map f？

这是我在类似示例中使用的方法，以证明

证明（省略基本情况和简单的 x::xs 情况）：

这是正确的吗 ？