问题标签 [proof]

For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.

0 投票
3 回答
10223 浏览

algorithm - 显示递归函数正确性的通用证明策略?

我想知道是否存在任何证明算法正确性的规则/方案?例如,我们在自然数上定义了一个函数 $F$,定义如下:

其中 $n \ \text{div}\ 2 = \left\lfloor\frac{n}{2}\right\rfloor$

任务是证明 $F(n,k)= \begin{cases} 1 \Leftrightarrow {n \choose k} \ \text{mod} \ 2 = 1 \ 0 \text{ else } \end{cases} $

它看起来不是很复杂(我错了吗?),但我不知道这种证明应该如何构建。我将非常感谢您的帮助。

0 投票
2 回答
326 浏览

algorithm - 证明算法对于解决游戏是正确的

给定的是一排最多 30 颗可以是黑色或白色的石头。比赛开始时不允许有空隙,但可以少于 30 颗棋子。目标是移除所有的石头。只有黑色的石头可以被移除,如果一颗石头被移除,它的邻居会改变颜色。如果移除的石头在中间,就会产生一个无法再填充的空隙;移除石头后,该石头的邻居不被视为邻居。

现在,我创建了一个使用蛮力解决这个游戏的程序。我得出的结论是,只有在有任何黑子(显然)并且黑子的数量是奇数的情况下,该游戏才可以解决。此外,如果黑子的数量是奇数,则可以通过递归删除该行的第一个黑子来解决游戏。

我的问题是我无法证明黑子的数量一定是奇数并且移除第一块石头就能解决游戏的条件。我怎样才能正确地证明这个算法?

我已经尝试过使用归纳法,但我被困住了:

行(a,b) = a*黑色 + b*白色

RemoveFirstBlack(Row(1, b)) = RemoveFirstBlack(black + b*white) = 0(如果 a=1 或 n = 0,其中 a=2n+1 且 n 为整数)

假设 RemoveFirstBlack(Row(k*a, b)) = RemoveFirstBlack(k*a*black + b*white) = 0 其中 k = 2p + 1 且 p 为整数。

RemoveFirstBlack(Row((k+1)*a, b)) = RemoveFirstBlack((k+1)*a*black + b*white) = RemoveFirstBlack((2(p+1)(2n+1))*black + b*white) = RemoveFirstBlack(2(p+1)*a*black + b*white) = 0?

在此先感谢您的任何指点!

0 投票
2 回答
2090 浏览

algorithm - 具有 O(n * log(n)) 时间和 O(1) 空间复杂度的稳定比较排序

在浏览维基百科的排序算法列表时,我注意到没有稳定的比较排序具有O(n*log(n))(最坏情况)时间复杂性和O(1)(最坏情况)空间复杂性。这肯定看起来像一个理论边界,但我找不到更多关于它的信息。

如何证明这一点?

O(n*log(n))注意:我知道比较排序的最坏情况时间复杂度的下限。

0 投票
1 回答
113 浏览

assert - 验证:结合正确性陈述

问题是:

这个规则有效吗?

我将如何处理这样的事情?我所能想到的就是试图找到一个错误的例子。

我一直在尝试想出它,以便 P1 && P2 的组合使 Q1 和 Q2 都为假,但我想不出任何一个。所以我倾向于这是有效的,但我不知道去哪里证明它......这门课的文字绝对是垃圾,我在网上找不到任何资源来组合正确性陈述......

0 投票
4 回答
653 浏览

algorithm - 人们如何证明计算机视觉方法的正确性?

我想提出一些关于计算机视觉研究的抽象问题。通过搜索网络和阅读论文,我还不能完全回答这些问题。

  1. 有人如何知道计算机视觉算法是否正确?
  2. 我们如何在计算机视觉的背景下定义“正确”?
  3. 形式化证明对理解计算机视觉算法的正确性有影响吗?

一点背景知识:我即将开始攻读计算机科学博士学位。我喜欢设计快速并行算法并证明这些算法的正确性。我也在一些课堂项目中使用过 OpenCV,尽管我没有接受过太多计算机视觉方面的正式培训。

一位潜在的论文顾问找到了我,他致力于为计算机视觉设计更快、更具可扩展性的算法(例如快速图像分割)。我试图了解解决计算机视觉问题的常见做法。

0 投票
3 回答
1314 浏览

regex - 显示带有 count(1s) = count(0s) 的位串是不规则的

令 L 为由字母表 {0,1} 上的字符串组成的语言,其中包含相等数量的 1 和 0。

例如:

你如何证明 L 不是常规语言?

0 投票
1 回答
452 浏览

proof - 证明形式逻辑的正确性

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

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

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

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

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

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

0 投票
1 回答
330 浏览

big-o - 用大哦证明

刚开始学习大哦和渐近分析,我被困在这个特殊的证明上:

我们如何证明 2^n 是 O(n!)?谢谢

0 投票
1 回答
343 浏览

algorithm - 在固定长度的输入上证明完美的哈希函数

我已经在这里看到了使用 gperf 的答案,但是,我更愿意根据我为strings具有固定长度的域创建的证明来推出自己的证明。<= 200 基于我从 wolfram 获得的计算,我得到了~7.9 x 10^374总排列。因此,我的思路是,如果我有2048一点哈希函数 ( 3.2 x 10^616),我应该能够处理我需要处理的整个字符串世界。我的问题是,在所有长度为 200 或更短的字符串的宇宙的约束下,我如何证明我最终生成的哈希实现将是完美的?

0 投票
1 回答
190 浏览

proof - 基于函数的隐含证明引理

我想证明下面的引理。我正在尝试使用“破坏”策略,但我无法证明这一点。请任何人指导我如何证明这样的引理。我可以为 EmptyString 证明它,但不能为变量 s1 和 s2 证明。谢谢