问题标签 [induction]

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 投票
2 回答
1486 浏览

math - 如何通过归纳证明程序做了某事?

我有一个计算机程序,它读取以后缀表示法编写的操作数和运算符的字符数组。然后程序扫描数组,使用堆栈计算结果,如下所示:

我如何通过归纳证明该程序正确评估任何后缀表达式?(取自练习 4.16 Java 算法(Sedgewick 2003))

0 投票
2 回答
7766 浏览

algorithm - 伪代码归纳证明

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

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

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

0 投票
2 回答
5772 浏览

math - 通过归纳证明递归关系

我有一个测试即将到来,我需要一些练习问题的帮助......需要通过归纳来证明这一点:


递归关系:m(i) = m(i-1) + m(i - 3) + 1, i >= 3 初始条件:m(0) = 1, m(1) = 2, m(2) = 3

证明 m(i) >= 2^(i/3)


到目前为止,这是我能够做到的:

基本情况: m(3) >= 2 -----> 5 >= 2。因此它适用于基本情况。

归纳假设假设存在 ak 使得 m(k) >= 2^(k/3) 成立。

现在我必须证明它对 k+1 成立。

所以我们有: m(k+1) >= 2^((k+1)/3)

等于(通过替换假设):

m(k) + m(k-2) + 1 >= 2^((k+1)/3)

这就是我卡住的地方。我不知道从这里去哪里。任何帮助将不胜感激。多谢你们!

0 投票
3 回答
2020 浏览

algorithm - 这个归并排序是 O(n) 的归纳证明有什么问题?

基于比较的排序是nlog(n)的大欧米茄,所以我们知道合并排序不能是O(n)。不过,我找不到以下证明的问题:

命题P(n):对于长度为n的列表,合并排序需要O(n)时间。

P(0):对空列表进行合并排序只返回空列表。

强归纳:假设P(1), ..., P(n-1)并尝试证明P(n)。我们知道,在递归归并排序的每一步,两个近似“半列表”被归并排序,然后被“压缩”。通过归纳,每个半列表的合并排序需要O(n/2) 时间。拉上拉链需要O(n)时间。因此,该算法具有M(n) = 2M(n/2) + O(n)的递归关系,即2O(n/2) + O(n)O(n)

0 投票
5 回答
1372 浏览

haskell - 显示两个不同的斐波那契函数是等价的

我正在尝试确切地了解证明程序正确的含义。我从头开始,开始关注第一步/主题介绍。

这篇关于全函数式编程的论文中,给出了斐波那契函数的两个定义。传统的一种:

和我以前从未见过的尾递归版本:

该论文随后声称,通过归纳证明两个函数对所有正整数 n 返回相同的结果是“直截了当的”。这是我第一次想到分析这样的程序。认为你可以证明两个程序是等价的,这很有趣,所以我立即尝试自己通过归纳来做这个证明。要么我的数学技能生疏了,要么任务实际上并不是那么简单。

我证明了 n = 1

我做了 n = k 假设

我开始尝试证明,如果假设成立,那么函数对于 n = k + 1 也是等价的(因此它们对于所有 n >= 1 QED 都是等价的)

我尝试了各种操作,在正确的时间替换假设等等,但我不能让 LHS 等于 RHS,因此证明函数/程序是等价的。我错过了什么?论文中提到任务相当于证明

通过对任意 p 的归纳。但我根本不明白这是怎么回事。作者是如何得出这个等式的?只有当 时,这才是方程上的有效变换p = 0。我不明白这意味着它如何适用于任意 p。要证明它对于任意 p 需要你经过另一层归纳。当然,要证明的正确公式是

到目前为止,这也没有帮助。谁能告诉我如何进行感应?或链接到显示证明的页面(我进行了搜索,找不到任何东西)。

0 投票
3 回答
10623 浏览

algorithm - 树中内部节点数的证明

我正在阅读有关压缩尝试的内容并阅读以下内容:

压缩树是一棵树,它有 L 个叶子,并且树中的每个内部节点都至少有 2 个子节点。

然后作者写道,一棵有 L 个叶子的树使得每个内部节点都有至少 2 个子节点,最多有 L-1 个内部节点。我真的很困惑为什么这是真的。

有人可以提供一个归纳证明吗?

0 投票
1 回答
283 浏览

recursion - 结构感应的终止

我无法让 Agda 的终止检查器接受使用结构归纳定义的函数。

我创建了以下作为我认为最简单的例子来展示这个问题。下面的定义size被拒绝,即使它总是在严格更小的组件上递归。

这个问题有通用的解决方案吗?我需要Recursor为我的数据类型创建一个吗?如果是,我该怎么做?(我想如果有一个如何定义Recursorfor的例子List A,那会给我足够的提示吗?)

0 投票
3 回答
1899 浏览

math - 归纳规范:自上而下 vs 自下而上 vs 推理规则?

请多多包涵。我将首先描述书中的一个例子,然后在最后提出我的问题。

根据编程语言范式上的文字:

归纳规范是指定一组值的强大方法。为了说明这种方法,我们用它来描述 自然数 N = {0, 1, 2, . . .} .

自上而下的定义:

一个自然数 n 在 S 中当且仅当

  1. n = 0,或
  2. n -3 ∈ S。

我们知道 0 ∈ S。因此 3 ∈ S,因为 (3 − 3) = 0 和 0 ∈ S。类似地 6 ∈ S,因为 (6−3) = 3 和 3 ∈ S。继续这样,我们可以得出结论,所有 3 的倍数都在 S 中。

那么其他自然数呢?1 ∈ S 吗?我们知道 1 != 0,所以第一个条件不满足。此外,(1-3) = -2,它不是自然数,因此不是 S 的成员。因此第二个条件不满足。

自下而上的定义:

将集合 S 定义为 N 中包含的最小集合并满足以下两个性质:

  1. 0 ∈ S,并且
  2. 如果 n ∈ S,则 n +3 ∈ S。

“最小集合”是满足属性 1 和 2 的集合,它是满足属性 1 和 2 的任何其他集合的子集。很容易看出只能存在一个这样的集合:如果 S1 和 S2 都满足属性1 和 2,并且都是最小的,则 S1 ⊆ S2(因为 S1 最小),并且 S2 ⊆ S1(因为 S2 最小),因此 S1 = S2。我们需要这个额外的条件,否则会有很多集合满足剩下的两个条件

推理规则:

这只是先前版本定义的简写符号。每个条目都称为推理规则,或者只是一条规则;水平线读作“if-then”。线以上的部分称为假设前件;线以下的部分称为结论结果。当列出两个或多个假设时,它们通过隐含的“和”连接</p>


现在问题来了。

  • 可能最重要的问题是为什么我需要知道这些归纳定义,以及它们在现实世界中的用处如何?
  • 为什么谷歌几乎没有返回归纳定义的结果?
  • 如果自上而下、自下而上和推理规则本质上显示相同的东西,为什么我们需要 3 种方式来编写相同的东西?
  • 为什么我很难找到比书中的例子复杂一点的问题的归纳定义,比如下面的例子。

我想找到以下 2 个问题的自上而下、自下而上和推理定义。您不必给我答案,但我确实想知道如何推导归纳定义。我从哪里开始?是否有解决此类问题的系统方法(配方)?

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 回答
813 浏览

coq - 偶数归纳假设

我正在尝试编写一个专门用于证明偶数属性的归纳假设。我制定并证明了以下内容:

尽管它已被证明,但任何使用它的尝试都会导致错误消息:“错误:不是正确数量的归纳参数。”

有人可以告诉我归纳假设有什么问题,或者如何应用它?

谢谢,

迈耶