问题标签 [proof]

我是一名从未正式学习过算法的程序员，并且一直想填补我学习中的空白。我目前正在阅读一些书籍和在线资料，我从概念上理解大 O，即它的用途，以及不同类别的性能，例如常数、线性、二次等。我可以编写问题并直观地理解不同方法的性能影响。

但是，我一直坚持的事情是算法证明的符号，我不确定在哪里可以找到这部分。我看过的所有书籍都假定这种知识水平。

例如，Skiena's Algorithm Design Manual中的这句话让我很难过：

f(n) = O(g(n)) 表示 c * g(n) 是 f(n) 的上限。

因此存在某个常数 c，使得 f(n) 总是 ≤ c * g(n)，对于足够大的 n（即，对于某个常数 n0，n ≥ n0）。

这是读者应该完成的推论练习：

3n^2 − 100n + 6 = O(n^2)，因为我选择c = 3 且3n^2 > 3n^2− 100n + 6；

我可以理解这两种说法，并且可以从逻辑上看出第二种说法是正确的。我也理解上限的概念，即这是最坏的情况。

但是我被困在简单的事情上，比如上面的内容是什么？

• g(n)

• 对于某个常数 n0，n ≥ n0

总的来说，我无法将各个部分拼凑在一起来理解整个证明。

谁能帮我用简单的英语解析上述陈述，并以对非技术人员有意义的方式展示它们与练习的关系

id是 type 的唯一函数，也是 typea -> a的 fst唯一函数(a,b) -> a。在这些简单的情况下，这很容易看出。但总的来说，您将如何证明这一点？如果同一类型有多个可能的函数怎么办？

或者，给定一个函数的类型，你如何推导出该类型的唯一（如果这是真的）函数？

编辑：我对当我们开始向类型添加约束时会发生什么特别感兴趣。

我正在学习如何证明某事是NP。在 Thomas Cormen 的算法介绍书中，他指出，如果给出某个问题的解决方案，则某些东西是 NP，您可以在多项式时间内验证它是否正确。

假设问题是 2x + 9 = 55，假设我不知道找到正确的 x 值需要多长时间，但是解决问题的算法返回了解决方案 23。然后证明它是 NP，我只需将 23 代入等式，看看这是否需要多项式时间并给我 55？谢谢。

我正在尝试使用 Omega 在 Coq 中进行证明。我花了很多时间在这上面，但什么都没有。不得不说我是Coq新手，所以对这种语言不太适应，也没有太多经验。但我正在努力。

这是我必须证明的代码：

为了证明这一点，我认为首先通过归纳证明这个引理会有所帮助：

然后这个，使用 omega 和 div2_eq ：

但我没能走得更远。

有谁知道该怎么做？

我很难理解如何使用归纳法和一些不变量来证明算法的正确性。即，如何找到不变量，何时使用归纳假设——尤其是对于二分搜索？我还没有找到一个直观的回应，所以我希望有人可以在这里对这个话题有所了解。

Here S-1 is the bit string obtained by changing the rightmost 1 bit of S to a 0 and all the 0 bits to right of this to 1s.

So I understand why this is correct, and I have write a rough explanation;

After every iteration, the rightmost 1 bit in S, as well as all the bits to the right of it, is set equal to 0. Thus, after each iteration, the next right-most 1 is accounted for and set to 0, until the entire string is 0's and the loop breaks with the count equal to the number of 1's.

I know this kind of answer won't pass in any mathematics community, so I was hoping to write a formal proof, but I don't know how to go about doing that. My proof skills are particularly shoddy, so an explanation of the techniques involved would be greatly appreciated.

我在学校学习 Coq，我有一个家庭作业要做。我有一个引理需要证明：如果一个列表在其元素中包含零，则其元素的乘积为 0。我开始编写代码，但我陷入了不知道如何继续下去的地步。我不知道 Coq 的所有命令，我做了很多研究，但我无法找到通往证明结尾的路。这是我的代码：需要导入列表 ZArith。

所以，我认为创建一个函数来检查列表是否包含零，以及另一个来计算其元素的乘积是一个好主意。我还（幸运的是）在网上找到了一个引理，证明如果我有 2 个数字，并且我知道其中一个不是 0，并且它们的乘积是 0，那么另一个数字必然是 0（我认为这可能会有所帮助） . 我想过用归纳法做一个证明，但没有成功。有任何想法吗？我知道这不是让别人做我的工作的地方，我不是在问那个，我只是需要一个想法。

我想将目标从 更改S x = S y为x = y。就像inversion，但为了目标而不是假设。

这样的策略似乎是合法的，因为当我们有 时x = y，我们可以简单地使用rewriteandreflexivity来证明目标。

目前我总是发现自己assert (x = y)用来引入一个新的子目标，但是写 whenx和yare 复杂的表达式很乏味。

DOM、ThreeJS和现在的canvas都编写了提供方法链接的库（可能最熟悉的 jQuery ）。链接也被用于核心 C 库中。

这些流畅的界面避免了对感兴趣对象的不必要重复。比较：

到：

可以说，以前的“传统”风格过于冗长，违反了DRY。

为了避免变量的重复cx，一些语言允许我们使用with语句来表达一组调用：

虽然 JavaScript 的with语句在存在拼写错误的情况下很危险，但Scala 的限制性更强的with语句使用起来很安全，而且 Haxe 还通过其using关键字将函数导入到本地范围。不幸的是，Java 和 C 没有提供这样的捷径，迫使我们在传统代码或链接之间做出选择。

语言作者应该考虑使用类似安全with的语句作为方法链接的替代方案，还是有充分的理由避免使用它？如果这样的功能是可取的，它应该采取什么形式？

我对方法链接的一个担忧是，关于链中后续调用的主题的模糊性可能会阻止在编译代码时先前可用的优化，其中重复使用cx是明确的。例如，如果对cx's 方法的调用不重叠，它们可以被并行化，但编译器在链接示例中可能更难确定这一点。

正如 rambo 在下面指出的那样，另一个缺点是为链接设计的方法无法返回任何其他值，这似乎相当浪费。

我最近尝试在 Codeforces 上解决一个问题，我确实得到了正确的解决方案，但现在正试图证明它。算法是这样的：

拿最小的折扣，把它应用到最贵的，连续两个便宜的免费。然后不断地做，直到没有物品剩下。

我有点卡在证明上。如果有人可以通过矛盾给我一个正式的证明，那就太好了。

问题！