如何检查我的生成无限列表的函数的实现？

Question

编写一个使用函数f和数字n并返回列表[f n, f (n + 1), f (n + 2), f (n + 3), f (n + 4) ... ]的函数。

这是我的解决方法：

func f n = f n : func f (n+1)

但是我不确定这是正确的。如何检查我的执行情况？

Answer 1

您可以提供co-inductive证明。协同归纳推理类似于归纳推理，但是它允许“无限”的结构。对于诸如数据流和无限列表之类的事物进行推理是很自然的选择。

您想要func拥有的属性类似于

∀ f : Int -> a, ∀ n : Int, ∀ i : Int, (i >= 0 ⟹ (func f n) !! i == f (n + i))

通过共归来证明事物类似于归纳法：您将其假定为所有子结构的共归因假设，然后为上层结构证明它。由于func只有一个定义，所以只有这样的证明义务。

这意味着，如果可以证明的话

∀ f : Int -> a, ∀ n : Int, ∀ i : Int, (i ≥ 0 ⟹ (func f n) !! i == f (n + i))
⟹
∀ f : Int -> a, ∀ n : Int, ∀ i : Int, (i ≥ 0 ⟹ (f n : (func f (n + 1))) !! i == f (n + i))

然后您将证明您的函数定义正确。

因为您实际上可以证明上述说法，所以您的函数定义是正确的。