Haskell 中的结构归纳法（取 n . 映射 f）xs = (映射 f . 取 n) xs

Question

如何证明对于每个函数 f 和每个有限列表 xs 都成立： (取 n . 映射 f) xs = (映射 f . 取 n) xs

take :: Int -> [a] -> [a]
take 0 _ = []
take _ [] = []
take n (x:xs) = x : take (n-1) xs

map :: (a -> b) -> [a] -> [b]
map _ [] = []
map f (x:xs) = f x : map f xs

(.) :: (b -> c) -> (a -> b) -> a -> c
(.) f g x = f(g x)

显示每一步所使用的参数。我实际上是如何开始解决这些问题的，以及一般证明它的方法是什么。希望能得到一些帮助来更容易地进入这个问题。

查看了我的脚本，但无法真正掌握它

Answer 1

我将遵循 Richard Bird 所著的《函数式思维》（剑桥大学出版社，2015 年，第 113 - 115 页）中的示例。

我们已经看到，每个有限列表要么是空列表

[]

，要么是

x:xs

形式，其中

xs

是有限列表。因此，为了证明

P(xs)

对于所有有限列表xs成立，我们可以证明：

P(
1. []

   )

   成立； 对于所有
x
2. 和所有有限列表

   xs

   ，

   P(

   x:xs

   )

   成立 假设 P(xs)

   成立

   。 [强调我的]

第二点提到的假设非常重要，在证明中被称为“{归纳}”。

首先，让我们列出

map

和

take

的方程以及证明中要使用的参考文献。

map :: (a -> b) -> [a] -> [b]
map f [] = []                      -- {map.1}
map f (x:xs) = f x : map f xs      -- {map.2}

take :: Int -> [a] -> [a]
take n [] = []                     -- {take.1}
take 0 xs = []                     -- {take.2}
take n (x:xs) = x : take (n-1) xs  -- {take.3}

证明：

我们想证明

P(xs)

对于所有有限列表 xs 都成立，其中我们的属性 P 是 (take n . map f) xs == (map f . take n) xs。

案例

[]

(take n . map f) []               (map f . take n) []
= {map.1}                         = {take.1}
take n []                         map f []
= {take.1}                        = {map.1}
[]                                []

P(

[]

)

成立。

案例

x:xs

(take n . map f) (x:xs)           (map f . take n) (x:xs)
= {map.2}                         = {take.3}
take n (f x : map f xs)           map f (x : take (n-1) xs)
= {take.3}                        = {map.2}
f x : (take (n-1) (map f xs))     f x : (map f (take (n-1) xs))
= {composition}                   = {composition}
f x : ((take (n-1) . map f) xs)   f x : ((map f . take (n-1)) xs)
                                  = {induction}
                                  f x : ((take (n-1) . map f) xs)

P(

x:xs

)

成立。 Q.E.D.

在我看来，棘手的部分是“{归纳}”步骤。它基于我们试图证明的等价性。这是基于

P(

xs

)

成立的假设，如上面引用的功能性思考中的第二点。 我在这里能提供的只是让你相信这个假设的合理性的建议。在“Case []”中，我们表明 P 对于一个空列表成立，但它仍然是 xs 的一个实例。在“Case (x:xs)”中，我们表明列表中的第一项不受影响，因此我们实际上知道 P 也适用于 [x]。然后，继续处理列表中的另一项可以被直觉地视为简单地重申已经建立的内容。至少我是这么理解的。