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

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)

但我不确定它是否正确。如何检查我的实施？

标签： haskelltemplate-haskell

Answer 1

你可以给出一个共归纳证明。共归纳推理类似于归纳推理，但它允许“无限”结构。这是推理数据流和无限列表等事物的自然选择。

你想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))

那么您将证明您的函数定义是正确的。

由于您实际上可以证明上述陈述，因此您的函数定义是正确的。