结构归纳 Haskell

Question

我想知道如何在结构归纳法中显示列出 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

是不是像数学归纳法一样？

提前致谢

Answer 1

结构归纳法是数学归纳法概念的推广。数学归纳法专门针对自然数，并将情况分为两种情况：该数字为零的情况，以及该数字比任何其他数字大1的情况。具体来说，这对应于自然数的 Peano 定义，可以用 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

因此，该声明成立。

通过结构归纳法，该命题成立 for[]并且，假设该命题成立 for ，它也xs成立。x : xs因此，我们可以得出结论，它适用于所有有限列表。

结构归纳法还不足以证明它适用于无限列表。Haskell 的[a]类型（实际上是一般的 Haskell）是归纳法和共归纳法的奇怪组合，这使得正式的数学证明有点尴尬。严格按照归纳定义，该类型不[a]应该有任何无限的情况，因此我们不必出于证明的目的而担心它们。