问题标签 [proof-of-correctness]

我正在尝试比较两种算法。我想我可以试着为他们写一个证明。（我的数学很烂，所以这个问题。）

通常在我们去年的数学课上，我们会遇到一个问题，比如 <can't use symbols in here so left them out>。

证明： (2r + 3) = n (n + 4)

然后我会完成所需的 4 个阶段并在最后得到答案。

我被卡住的地方是证明 prims 和 Kruskals - 我怎样才能将这些算法转化为上述数学算法的形式，以便我可以继续证明？

注意：我不是要求人们为我回答 - 只是帮助我把它变成一个我可以自己去尝试的形式。

这是一项家庭作业，但我无法通过编写正式的证明来了解整个业务。任何人都可以破解这个并为这个 fnc 的后置条件写正式证明：

字符串 REPLACE_BY (字符串 s,char c,char d)

后置条件 返回值是由 s 形成的字符串，通过将每次出现的 c 替换为 d（否则保持 s 不变）。

我是 lambda 演算的新手，正在努力证明以下内容。

SKK 和 II 是 beta 等效的。

在哪里

S = λ xyz.xz(yz) K = λ xy.x I = λ xx

我试图通过打开它来测试减少SKK，但无济于事，它变得一团糟。不要以为SKK可以在不扩大S、K的情况下进一步缩小。

我想知道是否有人可以帮助我回答这个问题。它来自以前的试卷，我可以知道为今年考试准备的答案。

这个问题似乎很简单，以至于我完全迷失了，它到底在问什么？

考虑以下涉及整数变量的代码部分：

通过陈述一个合适的输出条件，然后验证这段代码的正确性，证明执行后m等于i和j的最小值。

我的后置条件为：{m = i ∧ i < j ∨ m = j ∧ j < i}

它是否正确？你如何验证这一点？

考虑以下算法 min ，它将列表 x,y 作为参数并返回 x 和 y 联合中的第 z 个最小元素。前置条件：X 和 Y 是按升序排列的整数列表，并且它们是不相交的。

注意它的伪代码，所以索引从 1 而不是 0 开始。

我可以证明它终止，因为 z 不断减少 2 并且最终会达到基本情况之一，但我无法证明部分正确性。

您好，我无法证明这些组合子 SK = KI

带括号 [] 的步骤只是告诉您我正在执行的步骤。例如，λyz.xz(yz) 中的 [λxy.x / x] 表示我将用 (λxy.x) 替换表达式 λyz.xz(yz) 中的每个 x

到目前为止，我尝试的是减少 SK，我得到了这个：

然后减少KI，我得到了这个：

虽然这两个答案似乎不等于我（λyz.zz）和λy。λx.x 有人可以向我解释我做错了什么吗？谢谢你。

我在想我们可以证明一个程序有错误的事实。我们可以对其进行测试，以评估它或多或少具有抗虫性。

但是有没有办法（甚至理论上）证明一个程序没有错误？

对于简单的程序，比如“Hello World”，我想我们应该可以做到。但是更大的程序呢？

我正在从codeforces解决一个问题。

我们的工作是找到使给定整数序列成为非递减序列的最小成本。我们可以在每一步将任意数量的序列增加/减少 1，它将花费 1。

例如，当我们给定一个序列 3, 2, -1, 2, 11，我们可以使该序列不以成本 4 递减（通过递减3到2和递增-1到2，所以非递减序列将是 2, 2 , 2, 2, 11)

根据这个问题的编辑，我们可以用2个序列的动态规划来解决这个问题，（一个是我们给定的序列，另一个是给定序列的排序序列）。

解决方案概要：

如果我们让a是原始序列 并且b是 序列 的排序序列a，并且让f(i,j)是获得前i个元素不递减且第i个元素最多为bj的序列所需的最小移动次数。然后我们可以如下进行递归。（这是来自问题的编辑）

我理解这种重复。但是，我不知道为什么我们应该将原始序列与排序后的序列本身进行比较，并且我不确定我们是否可以使用另一个序列而不是给定序列的排序序列来获得正确的最小成本。

我们如何证明这个解决方案的正确性？我们如何保证排序后的答案是最小成本？

我想知道这种归纳证明的变体是否正确

归纳的标准证明表明，如果一个方程/算法适用于 n，并且您可以证明它适用于 n+1，那么您可以假设它适用于每个大于或等于 n 的整数。

现在，如果你有 2 个基本情况（例如：2 和 3）并且你要证明它适用于 n+2，你能说它适用于每个大于 2 的整数吗？

因为假设你可以证明它对 n+2 是正确的，

等等，所以你覆盖了每个大于 2 的整数

谢谢你的帮助^^

（如果+2版本是正确的，这意味着如果你有m个连续的基本情况并且证明它适用于n+m，那么它将适用于每个大于n的整数）

为了找到树的直径，我可以从树中取出任何节点，执行 BFS 以找到离它最远的节点，然后在该节点上执行 BFS。与第二个 BFS 的最大距离将产生直径。

不过，我不确定如何证明这一点？我尝试过对节点数使用归纳法，但是案例太多了。

任何想法将不胜感激......