algorithm - scala流上的归纳证明

Question

有人可以帮助我如何归纳推理这个 scala 代码

lazy val y : Stream[Int] = 1 #:: (y map (_ + 1))

生成从 1 开始的自然数列表？

Answer 1

in 位置的1 #:: whatever值为 1，所以我们知道y(0) = 1。

我们有一个更大的位置y(n+1) = whatever(n)。这里whatever是y map (_+1)，所以y(n+1) = (y map (_+1))(n)。

我们要证明forall n. y(n) = n + 1。

我们知道这是真的n = 0，y(0) = 1

(y.map(_+1))(n)简直就是y(n) + 1。这就是地图的作用。所以我们上面的公式就变成了y(n+1) = y(n) + 1。

那么微不足道，如果我们知道y(n) = n+1，那么y(n+1) = (n+1) + 1。结果在下一级为真。我们通过归纳得到证明。