问题标签 [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.
java - 简单的固定大小整数算术的算法效率(以 Big-Oh 计)是多少?
例如,
该算法的效率会是 O(1)、O(n) 还是其他?
haskell - 如何在 Morte 上创建 `enumFromTo` 函数?
Morte旨在用作超级优化功能程序的中间语言。为了保持强归一化,它没有直接递归,因此,列表等归纳类型表示为折叠,而无限列表等传导类型表示为流:
我想enumFromTo
在 Morte 上重写 Haskell,这样:
归一化为:
那可能吗?
algorithm - 算法的正确性
该算法旨在为任何正整数 m、n 计算 m^n。我如何通过对 n 的归纳来证明该算法的正确性。
haskell - 我如何证明 elem z (xs ++ ys) == elem z xs || elem z ys?
我有以下内容:
我如何证明对于所有 x 的 y 和 z ......
我试图使左侧等同于右侧,但是我的尝试都没有取得成果。
有人可以帮我吗?
algorithm - 通过归纳证明算法正确
我应该通过归纳来证明一个算法,并且对于所有 n >= 0 ,它返回 3 n - 2 n 。这是用 Eiffel 编写的算法。
我的理解是,你分三步证明。基本步骤、归纳假设和完整性证明。这就是我目前所拥有的。
基础:
P(0) 返回 0,并且 3 0 - 2 0 = 0。
P(1) 返回 1,并且 3 1 - 2 1 = 1。
归纳假设:
假设 P(k)对于 0 <= k < n返回 3 k - 2 k 。
完整性证明:
对于 n,P(n) 返回 5(P(n-1)) - 6(P(n-2))
5(P(n-1)) - 6(P(n-2))
5(3 n-1 - 2 n-1 ) - 6(3 n-2 - 2 n-2 ) <- 基于归纳假设
这是我卡住的部分。我到底应该如何将其减少到看起来像 3 n - 2 n?
coq - 在 coq 中应用原生归纳原理和几个参数
我正在阅读《软件基础》一书。在“关于归纳的更多信息”一章中,作者讨论了在定义归纳类型时由 coq 生成的归纳原理。
下面是一个练习。在定义中封装“+”的关联概念,然后在其上应用 nat_ind。
我对定义的第一个猜测如下:
但是,当我想证明这一点时,我遇到了问题:
nat_ind
不起作用。所以我认为这是因为P_plusassoc
不依赖于一个整数而是三个。
所以我这样重写P_plusassoc
:
但它仍然不起作用。问题出在哪里 ?我如何定义P_plusassoc
使用nat_ind
?
modulo - Coq induction on modulo
I'm new with coq and i really have difficulty in applying the induction. as long as I can use theorems from the library, or tactics such as omega, all this is "not a problem". But as soon as these do not work, I'm always stuck.
To be precise, now i try to prove
the case n = 0 I already have.
But how to make the induction step?
haskell - 多路(玫瑰)树的结构归纳
由于多路树可以定义为递归类型:
对这种类型进行结构归纳有相应的原则吗?
logic - 描述逻辑手册中的一个例子
我不太清楚这个例子。该示例取自描述逻辑手册。
在示例的最后一行,“需要归纳,因此这种推理不是一阶的”。那条线完全让我措手不及。
你的解释很受重视。
scala - 用多个列表进行归纳证明
我正在关注 Coursera 上的 Scala 函数式编程讲座,在视频 5.7 的结尾,Martin Odersky 要求通过归纳证明以下等式的正确性:
当涉及多个列表时如何处理归纳证明?
我检查了 xs 为 Nil 和 ys 为 Nil 的基本情况。我已经通过归纳证明,当 xs 被 x::xs 替换时,等式成立,但是我们是否还需要检查 ys 被 y::ys 替换的等式?
在那种情况下(不会过多地破坏练习......无论如何都没有评分)你如何处理:(xs ++ (y::ys)) map f
?
这是我在类似示例中使用的方法,以证明
证明(省略基本情况和简单的 x::xs 情况):
这是正确的吗 ?