这个表达式为什么相等？

Question

我此刻学习Haskell和我读了一本书，叫做“思维功能哈斯克尔”，我不明白为什么从第一章这个表达式为true：

总和。地图总和=总和。 CONCAT

Answer 1

假设我们有一个列表：

myList :: [[Int]] 
myList = [[1,2],[3,4,5]] 

让我们将sum . map sum：

(sum . map sum) [[1,2],[3,4,5]] 
= sum [sum [1,2], sum [3,4,5]] 
= sum [1+2,3+4+5] 
= 1+2+3+4+5 

现在，让我们应用sum . concat：

(sum . concat) [[1,2],[3,4,5]] 
= sum [1,2,3,4,5] 
= 1+2+3+4+5 

希望你可以看到现在，因为（a + b）+ c = a +（b + c），我们添加事物的顺序无关紧要，因此将内部列表相加，然后对整个列表进行求和得到与简单求和内部列表的每个值相同的结果。

Answer 2

非正式地说，这只是说 ，因为 如果加法是关联的，那么不管你如何分组你所添加的数字。 (a + b) + (c + d)与(a + b + c + d)相同。

---

形式上，我们可以使用等式推理和结构归纳法来证明任何大小的列表。 （请参阅这两个过程的快速定义的端部。）

假设map以下定义，concat，sum，和(.)：

1. map sum [] = []
2. map sum (a:as) = sum a : map sum as
3. concat [] = []
4. concat (a:as) = a ++ concat as
5. sum [] = 0
6. sum (a:as) = a + sum as
7. (f . g) x = f (g x)

为了让下面简单一点的证明，我们将要求没有明确的证据（见下文），其

sum (a ++ b) == sum a + sum b

首先我们确定空列表的身份是真的。

(sum . map sum) [] == sum (map sum []) -- (7) 
        == sum []   -- (1) 
        == sum (concat []) -- (3) 
        == (sum . concat) [] -- (7) 

（请注意，我们不需要定义5，因为一个空列表是空列表。）

现在，添加一个新的定义，大小k的任何列表as。

(sum . map sum) as == (sum . concat) as

如果（9）为真，我们可以证明为大小k+1的列表中的身份：

(sum . map sum) (a:as) == sum (map sum (a:as))  -- (7) 
         == sum (sum a : map sum as) -- (2) 
         == sum a + sum (map sum as) -- (6) 
         == sum a + (sum . map sum) as -- (7) 
         == sum a + (sum . concat) as -- (9) 
         == sum a + sum (concat as)  -- (7) 
         == sum (a ++ concat as)  -- (8) 
         == sum (concat (a:as))   -- (4) 
         == (sum . concat) (a:as)  -- (7) 

通过诱导，我们有证明了任何大小的列表sum . map sum == sum . concat。

---

• 均分推理意味着我们可以使用一个平等像a = b与b或b与a我们证明的任何步骤更换a。

• 列表上的结构归纳是一个引导过程。假设某些属性对于大小为k的列表属性为true，则使用该属性证明对于大小为k+1的列表是正确的。那么，如果你能证明k=0的确如此，这意味着所有的k都是如此。例如，如果它是k=0真，那么这是事实为k=1，这意味着它为真k=2等

---

定义4假定的++一个定义：

[] ++ bs = bs 
(a:as) ++ bs = a : (as ++ bs) 

与++定义，我们可以证明（8）：

基本情况：a是空的

sum ([] ++ b) == sum b    -- definition of ++ 
       == 0 + sum b   -- definition of + 
       == sum [] + sum b  -- definition of sum 

假设sum (a++b)为长度k的a真，

sum ((a:as) ++ bs) == sum (a : (as ++ bs)) -- definition of ++ 
        == a + sum (as ++ bs)  -- definition of sum 
        == a + sum as + sum bs -- induction 
        == sum (a:as) + sum bs -- definition of sum