问题标签 [induction]

例如，

该算法的效率会是 O(1)、O(n) 还是其他？

Morte旨在用作超级优化功能程序的中间语言。为了保持强归一化，它没有直接递归，因此，列表等归纳类型表示为折叠，而无限列表等传导类型表示为流：

我想enumFromTo在 Morte 上重写 Haskell，这样：

归一化为：

那可能吗？

该算法旨在为任何正整数 m、n 计算 m^n。我如何通过对 n 的归纳来证明该算法的正确性。

我有以下内容：

我如何证明对于所有 x 的 y 和 z ......

我试图使左侧等同于右侧，但是我的尝试都没有取得成果。

有人可以帮我吗？

我应该通过归纳来证明一个算法，并且对于所有 n >= 0 ，它返回 3 ⁿ - 2 ^{n 。这是用 Eiffel 编写的算法。}

我的理解是，你分三步证明。基本步骤、归纳假设和完整性证明。这就是我目前所拥有的。

基础：

P(0) 返回 0，并且 3 ⁰ - 2 ⁰ = 0。

P(1) 返回 1，并且 3 ¹ - 2 ¹ = 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 ⁿ - 2 ⁿ？

我正在阅读《软件基础》一书。在“关于归纳的更多信息”一章中，作者讨论了在定义归纳类型时由 coq 生成的归纳原理。

下面是一个练习。在定义中封装“+”的关联概念，然后在其上应用 nat_ind。

我对定义的第一个猜测如下：

但是，当我想证明这一点时，我遇到了问题：

nat_ind不起作用。所以我认为这是因为P_plusassoc不依赖于一个整数而是三个。

所以我这样重写P_plusassoc：

但它仍然不起作用。问题出在哪里 ？我如何定义P_plusassoc使用nat_ind？

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?

由于多路树可以定义为递归类型：

对这种类型进行结构归纳有相应的原则吗？

我不太清楚这个例子。该示例取自描述逻辑手册。

在示例的最后一行，“需要归纳，因此这种推理不是一阶的”。那条线完全让我措手不及。

你的解释很受重视。

我正在关注 Coursera 上的 Scala 函数式编程讲座，在视频 5.7 的结尾，Martin Odersky 要求通过归纳证明以下等式的正确性：

当涉及多个列表时如何处理归纳证明？

我检查了 xs 为 Nil 和 ys 为 Nil 的基本情况。我已经通过归纳证明，当 xs 被 x::xs 替换时，等式成立，但是我们是否还需要检查 ys 被 y::ys 替换的等式？

在那种情况下（不会过多地破坏练习......无论如何都没有评分）你如何处理：(xs ++ (y::ys)) map f？

这是我在类似示例中使用的方法，以证明

证明（省略基本情况和简单的 x::xs 情况）：

这是正确的吗 ？