我想知道如何在列表 xs 的结构归纳中显示，或者归纳如何在此工作：
map f (map g xs) = map (\x -> f(g x)) xs
用这个函数定义
map :: ( a -> b ) -> [ a ] -> [ b ]
map _ [] = []
map f ( x : xs ) = f x : map f xs
是不是像数学归纳法？
提前致谢
【问题讨论】：
标签： haskell map-function induction
结构归纳是数学归纳概念的概括。数学归纳法特别适用于自然数并将情况分为两种情况：数字为零的情况，以及它比任何其他数字大一的情况。具体来说，这个对应的是Peano definition of natural numbers，可以用Haskell写成如下。
data Nat = Zero | Succ Nat
因此，对这种数据类型的归纳证明分为两种情况，一种用于每种类型构造函数。第一个说“假设我们有一个Zero；证明它”。第二个说“假设我们有一个Succ n，其中n 的工作已经完成；现在证明它”。
现在你想对列表进行归纳证明。列表类型可以写成（模语法糖）
data [a] = [] | a : [a]
准确地说，这对应于以下（无魔法）定义
data List a = Nil | Cons a (List a)
虽然我会使用第一个，因为在 Haskell 中使用它会更简洁一些。对[a] 的结构归纳证明分为两种情况：
让我们将其应用于map。这是您的 map 函数。
map :: (a -> b) -> [a] -> [b]
map _ [] = []
map f (x : xs) = f x : map f xs
我们要证明的是，写得很准确：
让
f :: b -> c和g :: a -> b是任意函数。然后证明，对于任何列表xs :: [a]，我们有map f (map g xs) = map (\y -> f (g y)) xs
让我们开始吧。有两种情况。首先，假设xs 为空，即xs == []。然后，直接从上面的函数定义，我们知道map g xs == map g [] == [] 和f 相同，所以我们有以下等价性
map f (map g [])
map f []
[]
map (\y -> f (g y)) []
每个推论都来自map的定义，因为我们完全了解map对空列表的作用（即它什么都不做，函数没有区别）。这样第一个案例就完成了。
现在，归纳步骤。假设我们有一个列表(x : xs)，并假设该陈述对于xs 是正确的。所以我们假设
map f (map g xs) == map (\y -> f (g y)) xs
我们想证明
map f (map g (x : xs)) == map (\y -> f (g y)) (x : xs)
让我们一步一步来。
map f (map g (x : xs))
map f (g x : map g xs) -- By the function definition
f (g x) : map f (map g xs) -- By the function definition
f (g x) : map (\y -> f (g y)) xs -- By induction hypothesis
map (\y -> f (g y)) (x : xs) -- By the function definition
因此，该陈述成立。
通过结构归纳，该语句适用于[]，并且假设该语句适用于xs，它也适用于x : xs。因此，我们可以得出结论，它适用于所有有限列表。
结构归纳没有强大到足以证明它适用于无限列表。 Haskell 的 [a] 类型（实际上是一般的 Haskell）是归纳和共归纳的奇怪组合，这使得对此的正式数学证明有点尴尬。严格按照归纳定义，[a] 类型应该不有任何无限情况，所以为了证明的目的，我们不必担心它们。
【讨论】：