为什么这个表达式相等？

Question

我现在正在学习 Haskell，并且我读了一本名为“使用 Haskell 进行函数式思考”的书，我无法真正理解为什么第一章中的这个表达是正确的：

总和。地图总和 = 总和。连接

Answer 1

非正式地说，这只是说因为如果加法是关联的，那么如何对要相加的数字进行分组并不重要。 (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)

为了使下面的证明更简单一点，我们将在没有明确证明（但见下文）的情况下声明

8. 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 添加一个新定义。

9. (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 的等式将a 替换为b 或b 与a。

• 列表的结构归纳是一个引导过程。您假设某些属性对于大小为k 的列表是正确的，然后使用它来证明它对于大小为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

Answer 2

假设我们有一个列表：

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)，我们添加事物的顺序无关紧要，因此对内部列表求和，然后对整个列表求和产生与简单地将内部列表的每个值相加的结果相同。