scala流上的归纳证明

Question

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

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

产生一个从 1 开始的自然数列表？

Answer 1

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。结果在下一级为真。我们通过归纳得到证明。