问题标签 [proof]

我强烈怀疑左右表达式相等，但是如何证明呢？

一位朋友向我提出了一个看似正确的猜想，但我们俩都无法提出证明。这是问题所在：

给定一个具有不相交的非空顶点集 U 和 V 的连通二部图，使得 |U|<|V|，所有顶点都在 U 或 V 中，并且没有连接同一集合中的两个顶点的边，则至少存在一条连接顶点 a∈U 和 b∈V 的边使得 degree(a)>degree(b)

证明 U 中至少有一个顶点的度数高于 V 中的 1 是微不足道的，但要证明存在一对存在连接它们的边却难倒我们。

众所周知，任何 LL(1) 语法也是 LR(1)，但我似乎无法在任何地方找到严格的证明。我听说过一些关于证明的高级概述（例如，由于 LL(1) 语法一次仅从一个标记确定其产生式，而 LR(1) 语法可以在做出决定之前扫描更多的输入制作）。但是，在查阅了两本关于编译器和解析的教科书并在 Google 上进行了快速搜索之后，我似乎无法找到更正式的证据来证明这一事实。

有谁知道这个证明，或者至少在哪里可以找到它？

我刚刚写了一个基于 Mono Continuations 的协程（作为练习）实现（非常奇怪的经历）。我应该采取哪些方法/方法来证明其正确性？

在这个关于 NP、NP-hard 和 NP-complete 定义的问题的回答中，Jason 声称

停止问题是经典的 NP-hard 问题。这是给定程序 P 和输入 I 的问题，它会停止吗？这是一个决策问题，但它不在 NP 中。很明显，任何 NP 完全问题都可以简化为这个问题。

虽然我同意停机问题在直觉上是一个比 NP 中的任何问题都“更难”的问题，但老实说，我无法提出一个正式的数学证明来证明停机问题是 NP 难的。特别是，我似乎无法找到从 NP 中的每个问题（或至少任何已知的 NP 完全问题）的实例到停止问题的多项式时间多对一映射。

是否有直接的证据证明停机问题是 NP 难的？

以下文字摘自算法书。

我们可以使用链表惯用的矩形框来绘制二叉树，但树通常被绘制为由线连接的圆圈，因为它们实际上是图。在引用树时，我们也没有显式绘制 NULL 链接，因为每个具有 N 个节点的二叉树都需要 N+1 个 NULL 链接。

我的问题是作者的意思是什么意思是每个具有 N 个节点的二叉树都需要 N+1 个空链接？作者是如何获得 N+1 号的？

最近我读了很多关于Haskell的文章，以及它从纯粹的函数式语言中获得的好处。（我对讨论 Lisp 的 monad 不感兴趣）对我来说（至少在逻辑上）尽可能地隔离具有副作用的函数是有意义的。我已经setf大量使用了其他破坏性函数，并且我认识到在 Lisp 和（大部分）其衍生产品中对它们的需求。

开始了：

1. 类似的东西(declare pure)可能有助于优化编译器吗？或者这是一个有争议的问题，因为它已经知道了？
2. 该声明是否有助于证明一个函数或程序，或者至少是一个被声明为纯的子集？还是这又是不必要的，因为它对程序员、编译器和证明者来说已经很明显了？
3. 如果没有别的，编译器对程序员使用此声明强制执行纯函数并增加 Lisp 程序的可读性/可维护性是否有用？
4. 这有什么意义吗？还是我太累了，现在连想都不想？

我很感激这里的任何见解。欢迎提供有关编译器实现或可证明性的信息。

编辑

澄清一下，我并不打算将这个问题限制在 Common Lisp 上。它显然（我认为）不适用于某些衍生语言，但我也很好奇其他 Lisps 的某些功能是否倾向于支持（或不支持）这种设施。

我有许多相互交叉的抛物线。我正在从这些抛物线的上段生成一个列表S。由于抛物线的对应两条边最多在 2 个点相交，因此列表S最多可以包含2n-1个项目。

我想通过归纳来证明这一点。我能想到的是这样的：

假设我有f(x) ≤ 2n – 1。

基本情况是n = 1, f(1) ≤ 2 · 1 – 1，所以f(1) <= 1。

然后假设n = k成立，所以f(k) ≤ 2k – 1。

我们可以证明对于n = k+1成立f(k+1) ≤ 2(k+1) – 1。

我应该这样继续吗，例如对于n = k+2，n = k+3，...？如果我继续这样下去，那是否意味着我通过归纳证明了它？

我很难证明这n^k适用O(2^n)于所有人k。我试过lg2两边都吃k*lgn=n，但这是错误的。我不确定我还能如何证明这一点。

我真的不明白如何通过对伪代码的归纳来证明。它似乎与在数学方程上使用它的方式不同。

我正在尝试计算数组中可被 k 整除的整数的数量。

如何证明这是正确的？谢谢