我想知道如何在串列 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
是不是像數學歸納法？
提前致謝
uj5u.com熱心網友回復：
結構歸納法是歸納法數學概念的概括。數學歸納法特別適用于自然數，并將情況分為兩種情況：數字為零的情況和比任何其他數字大 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
因此，該陳述成立。
通過結構歸納，該陳述成立，[]并且假設該陳述成立xs，它也成立x : xs。因此，我們可以得出結論，它適用于所有有限串列。
結構歸納法是不是足夠強大，以證明它擁有無限名單。Haskell 的[a]型別（實際上是 Haskell）是歸納和共歸納的奇怪組合，這使得正式的數學證明有點尷尬。通過歸納定義嚴格去，型別[a]應該不會有任何無限的情況下，所以我們不擔心他們對這個證明的目的。
轉載請註明出處，本文鏈接：https://www.uj5u.com/caozuo/394429.html