问题标签 [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.
algorithm - 证明/证明 BigO 和 BigTheta
我在完全理解如何证明以下某些陈述时遇到问题。
例如我有一个声明:n^2logn = O(n^2)
. 如果我错了,请纠正我,但这说明n^2
是bigO
. n^2logn
意味着n^2
增长速度比n^2logn
. 现在我们将如何证明这一点?我假设我需要使用我曾尝试使用但陷入过程中的归纳证明。我可以将此语句重写为n^2logn <= n^2
吗?
是否可以使用归纳法来反驳某些东西?例如,反驳n!=O(n^n)
. 或者通过简单地证明任意值(假设大于 2)不满足该陈述来反驳该陈述是否有效?
最后为了清楚起见,bigTheta 指出方程在正确增长时是等价的?
string - 归纳定义字符串集
CS学生在逻辑课上苦苦挣扎。这个问题让我一头雾水
归纳定义字符串集
找到以下字符串集的归纳定义:
S = {apbcr | p 是自然数,r 是大于 0 的自然数} * p 和 r 是上标*
logic - 强感应?
问题是“使用强归纳表明,2 个或更多偶数的任何总和都是偶数”。现在,我对常规归纳很好,但我迷失在强归纳的符号中。到目前为止,我有:
BASE:(我们将使用 2 作为偶数)
根据序列定义,n=2,A2 = 4(偶数)
根据序列定义,n=3,A3 = 6(偶数)
因此,我们有 P(2) 和 P(3)
我不知道从这里去哪里,如果有人能引导我朝着正确的方向前进,那就太好了
predicate - 什么是归纳谓词?
你将如何解释归纳谓词?它们是用来做什么的?他们背后的理论是什么?它们只存在于依赖类型系统中,还是存在于其他系统中?它们在某种程度上与 GADT 相关吗?为什么它们在 Coq 中默认为 true?
这是 Coq 的一个例子:
你会如何使用这个定义?它是数据类型还是命题?
proof - 使用归纳法证明循环不变量成立
不变量:就在第 3 行评估循环保护之前,删除了最右边的 d 位的 n 与 val 相同。(假设数字 0 需要 0 位来写出,并且是唯一需要 0 位来写出的数字)。
使用归纳法证明循环不变量成立。
现在我一直认为归纳证明是假设通过用 k 替换方程中的变量将是真的,那么我必须证明 k+1 也将是真的。但是在这个问题中我并没有真正给出方程式,而只是一段代码。这是我的基本情况:
就在第 3 行评估循环保护之前,d 等于 0,在第 2 行,val == n,因此如果 n 删除了最右边的 0 位,则为 val。因此,基本情况成立。
我不确定如何在此之后编写归纳步骤,因为我不确定如何证明 k+1 ..
context-free-grammar - 上下文无关文法的归纳证明
所以我有这个问题,我正在研究关于上下文无关语法的归纳证明。
鉴于这个语法
S-> aSb | 不锈钢 | 抗体
使用归纳法证明文法生成的字符串不以abb开头。
很容易看出这实际上是正确的,但是我对如何对其进行正式证明有一些问题。
我正在考虑对单词的长度使用按值归纳的课程,或者对推导的长度使用按值归纳的课程(在这种情况下,我真的不知道哪个更好)。
让我们对推导的长度使用归纳法。
基本情况:推导的长度是一步,那么唯一的可能性是 S-> ab,这显然成立。
归纳假设:如果 S=>w' 有 n 个推导(n>0),则 w' 不以 abb 开头
感应步:???
归纳步骤是我遇到问题的地方,我真的不明白该怎么做。
我想知道是否有人可以解释我应该在那里做什么?
谢谢!
avl-tree - 最小高度 AVL 树
我只是在阅读这篇(http://condor.depaul.edu/ntomuro/courses/417/notes/lecture1.html)论文,它证明了 AVL 树中的最小节点数。但是,我不明白结果的含义,因为 O(log n) 根本不是指节点数。这怎么可能是证明?但是,我确实了解第一步以及如何简化迭代。但是在第四步之后,我无法理解他到底在做什么(尽管我可以模糊地想象)。谁能向我解释一下,最后几行证明了什么,以及他如何在第 1 部分末尾简化表达式?
谢谢
logic - 类型系统中实践规则归纳的任何文件?
如您所知,要定义一个新的类型系统,一种方法是我们需要:
- 语言语法
- 打字规则
然后我们需要证明一些我们认为可以使用上述类型规则证明的定理。为了证明这些定理,一种方法是我们可以使用归纳法(Rule Induction)。
例如,我们有一个这样的系统:
我们定义了 2 个规则“Zero”和“Succ”,如下所示:
然后,我们提出一个定理,我们认为这个定理是正确的,我们需要证明它。
我们可以使用定义的规则轻松证明这个定理。这就是所谓的规则归纳。
那么有没有人知道可以帮助练习规则归纳的资源?
tree - Weka J48 实现不同的缺失值处理
在一些使用缺失值数据的任务中,我必须使用 J48 树归纳算法。现在我将做一些经验研究,比较 J48 树归纳上下文中的不同缺失值方法,不同的 UCI 训练数据集和不同的人工这些数据集的截肢率(标准,+10%,+40% 截肢)。
我的主要问题是,我如何在 J48 源代码中实现以下方法,或者在我自己的代码中使用 Weka J48 类更好地实现。我可以将这种方法作为元分类器或其他方式处理吗?我想测试的方法与 J48 标准处理和随机森林相对应:
- 删除缺少属性的对象(完整案例)
- Hot-Deck-Methods(寻找内部捐赠者的概念)
- 代理拆分(使用其他属性进行拆分,例如 CART 处理缺失值)
- 使用其他决策树(概念->缺失属性值)进行插补以找到缺失的属性值
我必须停用集成的 J48(C4.5) 缺失值处理吗?我怎样才能停用这个?我认为 J48(C4.5) 将使用特殊值方法来查找测试、概率分布和在训练数据分区期间将对象拆分为部分,而在分类期间则使用其他方法。
现在其他所有人都可以轻松扩展J48的其他缺失值方法吗?
非常感谢!
coq - 在对命题的归纳中使用记住会在 Coq 中产生“类型错误”的错误
这是自然数均匀性的归纳和计算定义。
以及一个暗示另一个的证明。
起初我并没有多想这个证据,但仔细一看,我发现了一些令人不安的事情。问题是在这reflexivity
一步之后,我希望看到上下文
但我实际上得到的是
尽管这个定理仍然可以证明,但看到假设神秘地消失是令人不安的。我想知道如何获得我最初期望的上下文。从网络搜索中,我了解到这是对 Coq 中构造术语进行归纳的一般问题。关于 SO 的一种建议解决方案建议使用remember
保留假设的策略。但是当我在这个证明中尝试这样做时,
induction
我在步骤中收到以下错误消息。
我不太明白。我认为问题在于它E
有一个自由变量,但在那种情况下我会被卡住,因为没有E
引入n
. (generalize dependent n
会用它来概括E
)
有没有办法获得最初预期的上下文?