6.2 摺融合定理

第0 章中提及，「抽象化」意指抽取出我們認為重要的概念、成分，給予一個名字或符號。 如此一來，這個概念正式地「存在」了，我們可以談論它、研究其性質，並將研究結果應用在所有符合這個抽象概念的事物上。 一個程式語言最重要的功能之一是提供良好的抽象化機制。 由於高階函數等等性質，函數語言讓我們能較容易地對程式結構作抽象。

「摺」是我們找到的一個抽象，許多程式可以表達為摺。 而一旦辨識出了摺這個結構，我們可開始討論所有摺都滿足的性質， 這些性質則將可適用於所有是摺的程式上。

關於摺的性質中，最重要的也許是本節的摺融合定理(fold-fusion theorem)。

摺融合定理告訴我們一個摺如何能與串接於其後的函數融合起來，成為單獨的一個摺：

h . foldr f e = foldr g (h e) 

性質 h (f x y) = g x (h y) 是該融合能成立的充分條件，我們日後將稱之為「融合條件(fusion condition)」。 如果定理本身看來太抽象，下述例子也許可給讀者一些直覺。考慮 [x0,x1,x2]:

      {-"{\color{burntorange}"-}h{-"}"-} (foldr f e [x0,x1,x2])
 ===    {- foldr 之定義 -}
      {-"{\color{burntorange}"-}h{-"}"-} (f x0 (f x1 (f x2 e)))
 ===    {- 融合條件: {-"{\color{burntorange}"-}h{-"}"-} (f x y) = g x ({-"{\color{burntorange}"-}h{-"}"-} y) -}
      g x0 ({-"{\color{burntorange}"-}h{-"}"-} (f x1 (f x2 e)))
 ===    {- 融合條件: {-"{\color{burntorange}"-}h{-"}"-} (f x y) = g x ({-"{\color{burntorange}"-}h{-"}"-} y) -}
      g x0 (g x1 ({-"{\color{burntorange}"-}h{-"}"-} (f x2 e)))
 ===    {- 融合條件: {-"{\color{burntorange}"-}h{-"}"-} (f x y) = g x ({-"{\color{burntorange}"-}h{-"}"-} y) -}
      g x0 (g x1 (g x2 ({-"{\color{burntorange}"-}h{-"}"-} e)))
 ===    {- foldr 之定義 -}
      foldr g ({-"{\color{burntorange}"-}h{-"}"-} e) [x0,x1,x2] 

由此例可看出融合條件 h (f x y) = g x (h y) 的作用 --- 將 h 往右推，並將途中經過的 f 都變成 g, 直到碰到 e 為止。

定理6.2 可用例行的歸納證明證成：

      h (foldr f e [])
 ===  h e
 ===  foldr g (h e) [] 

      h (foldr f e (x:xs))
 ===    {- foldr 之定義 -}
      h (f x (foldr f e xs))
 ===    {- 融合條件: h (f x y) = g x (h y) -}
      g x (h (foldr f e xs))
 ===    {- 歸納假設 -}
      g x (foldr g (h e) xs)
 ===    {- foldr 之定義 -}
      foldr g (h e) (x:xs) 

註記   我們在歸納情況的第二步使用了融合條件 h (f x y) = g x (h y). 欲使該步成立，融合條件不須對所有 y 都成立 --- 我們只需要它在 y 是 foldr f e 的可能結果時成立即可。這是定理6.2 中「在 foldr f e 的值域中的 y」這句話的由來。

在本章接下來大部分的例子中，我們其實可以證明融合條件對所有 y 均成立。但只要我們處理的演算法問題稍微複雜些，我們便會常遇到融合條件只對 foldr f e 的值域中的 y 成立的情況。 我們將在第6.2.6 節中看到一些例子。

6.2.1 將摺融合用於定理證明

定理6.2 有幾種用法：

• 一種可能是用於證明性質：我們希望證明 h . foldr f e 與 foldr g (h e) 相等，此時我們已知 h, f, g, 與 e.

• 另一種可能是用於生成程式。此時我們通常已知 h, f, 與 e, 但不知道 g. 我們希望找到一個讓融合條件成立的 g, 使得 h . foldr f e 能在一個 foldr 之中完成。

我們先討論第一種情況。

      map f . map g
 ===   {- map 的摺定義 -}
      map f . foldr (\x ys -> g x : ys) []
 ===   {- 摺融合 -}
      foldr (\x ys -> f (g x) : ys) []
 ===   {- map 的摺定義 -}
      map (f . g) 

      map f (g x : ys)
 ===    {- map 之定義 -}
      f (g x) : map f ys 

將上述例子與第2.4 節的歸納證明比較。 歸納證明中，最關鍵的是「使用歸納步驟」的一步，而使用摺融合定理的證明卻沒有這步 --- 歸納步驟的使用被包裝、隱藏在摺融合定理中了。 而上述例子中關於融合條件的證明，恰巧是原歸納證明中和問題本身最相關的部分。

我們可說：摺融合定理之於證明，就如同摺之於程式。 摺是抽象出的常見程式骨架，將拆解輸入串列、做遞迴呼叫等動作包裝起來。 有了摺，我們不需自己做遞迴呼叫，只需填入針對特定問題的 f, e 等參數的值。 摺融合定理則是抽象出的常見證明骨架，將狀況分析、使用歸納假設等動作包裝起來。 有了摺融合定理，我們不需自己做狀況分析、引用歸納假設，只需填入針對這個問題的融合條件的證明。

事實上，map 融合定理是下述定理的特例：

我們時常看到 foldr 與 map 一起出現，此時定理6.4 相當好用。

       sum . map (2*)
  ===    {- sum 之摺定義 -}
       foldr (+) 0 . map (2*)
  ===    {- 定理6.4: foldr-map 融合 -}
       foldr ((+).(2*)) 0 

       (2*) . sum
  ===  (2*) . foldr (+) 0
  ===    {- 摺融合 -}
       foldr ((+).(2*)) 0 

      2*(x+y)
 ===   {- 乘法與加法之分配率 -}
      2*x + 2*y
 ===   {- (.) 之定義 -}
      ((+) . (2*)) x (2*y) 

許多等式可用類似的模式證明：為證明 e1 = e2, 我們對兩邊都做融合，看是否能製造出同一個 foldr.

  map f . (++ys) = (++ map f ys) . map f  

      (++ map f ys) . map f
 ===    {- foldr-map 融合 -}
      foldr ((:) . f) (map f ys)
 ===    {- 摺融合 -}
      map f . (++ ys) 

     map f (x : zs)
===    {- map 之定義 -}
     f x : map f zs
===    {- (.) 之定義 -}
     ((:) . f) x (map f zs) 

在本節的許多例子中，使用摺融合定理大大簡化了證明 --- 幾乎到了只要把式子寫下就快要證完了，「沒什麼可說」的地步。我們再看最後一個例子。

      sum . map sum
 ===  foldr (+) 0 . map sum
 ===    {- foldr-map 融合 -}
      foldr (\xs n -> sum xs + n) 0
 ===    {- 摺融合 -}
      sum . foldr (++) []
 ===  sum . concat 

      sum . map length
 ===    {- sum = foldr (+) 0, foldr-map 融合 -}
      foldr ((+) . length) 0
 ===    {- 摺融合 -}
      length . foldr (++) []
 ===  length . concat 

       length (xs ++ ys)
  ===    {- length 與 (++) 的同態性 -}
       length xs + length ys
  ===    {- (.) 之定義 -}
       ((+) . length) xs (length ys) 

      concat . map g . filter p
 ===    {- 摺融合，如下述 -}
      foldr (\x ys -> filter p (f x) ++ ys) []
 ===    {- foldr-map 融合，如下述 -}
      concat . map (filter p . f) 

      concat (map g (if p x then x:xs else xs))
 ===    {- concat . map g 分配進 if 之中 -}
      if p x then g x ++ concat (map g xs) else concat (map g xs)
 ===    {- 提出 concat (map g xs) -}
      (if p x then g x else []) ++ concat (map g xs)
 ===    {- 假設 -}
      filter p (f x) ++ concat (map g xs) 

6.2.2 以摺融合生成程式

如前所述，另一種使用摺融合的理由是生成程式：我們希望 h . foldr f e 能在一個 foldr 之中完成。 此時我們已知 h, f, 與 e, 希望用融合條件找出適合的步驟函數。

      sum (square x : xs)
 ===    {- sum 之定義 -}
      square x + sum xs
 ===    {- 提出 x 與 sum xs -}
      (\x y -> square x + y) x (sum xs) 

noOverdraft :: Int -> Bool
noOverdraft = (>= 0) . minimum . map sum . inits 

      map sum ([] : map (x:) xss)
 ===  0 : map sum (map (x:) xss)
 ===   {- map 融合 -}
      0 : map (sum . (x:)) xss
 ===   {- sum (x:xs) = x + sum xs, map 融合 -}
      0 : map (x+) (map sum xss) 

  map sum . inits === foldr (\x ys -> 0 : map (x+) ys) [0] 

      minimum (0 : map (x+) ys)
 ===  0 ↓ minimum (map (x+) ys)
 ===    {- minimum (x+) ys = x + minimum ys，後述 -}
      0 ↓ (x + minimum ys) 

      noOverdraft
 ===  (>= 0) . minimum . map sum . inits
 ===  (>= 0) . foldr (\x y -> 0 ↓ (x + y)) 0 

     0 ↓ (x+y) >= 0
<=>    {- a ↓ b >= c <=> a >= c ⋀ b >= c -}
     0 >= 0 ⋀ x+y >= 0
<=>  x + y >= 0
<=>    {- 希望找到這樣的 step3 -}
     step3 x (y>=0) 

  noOverdraft = and . map (>=0) . map sum . inits 

使用摺融合論證兩個式子相等的證明常有如下的形式：

     h1 . foldr f1 e1
===    {- 摺融合定理 -}
     foldr g (h1 e1)
===    {- 摺融合定理 -}
     h2 . foldr f2 e2 

此時，我們也常需要藉由兩個融合條件之一來發現步驟函數 g 是什麼。

      length (xss ++ map (x:) xss)
 ===  length xss + length (map (x:) xss)
 ===    {- length (map f) = length -}
      2 * length xss 

     length . sublists
===  length . foldr (\x xss -> xss ++ map (x:) xss) [[]]
===    {- 摺融合定理，如上 -}
     foldr (\x n -> 2 * n) 1
===    {- 摺融合定理，如下 -}
     exp 2 . foldr Suc Zero
===  exp 2 . length 

     map (>=0) (0 : map (x+) ys)
===  True : map ((>=0) . (x+)) ys
===  step x (map (>=0) ys) 

      sum . (++ys)
 ===  sum . foldr (:) ys
 ===    {- 摺融合 -}
      foldr (+) (sum ys)
 ===    {- 摺融合 -}
      (+ (sum ys)) . foldr (+) 0
 ===  (+ (sum ys)) . sum 

      (+ (sum ys)) (x + y)
 ===  (x + y) + sum ys
 ===  x + (y + sum ys)
 ===  x + ((+ (sum ys)) y) 

     length . fan y
===  length . foldr (\x xss -> (y:x: tail (head xss)) : map (x:) xss) [[y]] 
===    {- 摺融合定理 -}
     foldr Suc 1
===    {- 摺融合定理 -}
     Suc . foldr Suc Zero
===  Suc . length 

     length ((y:x: tail (head xss)) : map (x:) xss)
===    {- length 之定義 -}
     Suc (length (map (x:) xss))
===    {- length . map f = length -}
     Suc (length xss) 

decimal = foldr (\c n -> if c then 1 + 2 * n else 2 * n) 0 {-"~~"-}

     exp b (if c then 1 + 2 * n else 2 * n)
===    {- 函數分配進 if -}
     if c then exp b (1 + 2 * n) else exp b (2 * n)
===    {- 因 $m^{x+y} = m^x \times m^y$ -}
     if c then b * exp b (2 * n) else exp b (2 * n)
===    {- 因 $m^{2n} = (m^n)^2$, 回顧：square x = x * x -}
     if c then b * square (exp b n) else square (exp b n) 

  exp b . decimal = foldr (\d x -> if c  then b * square x
                                         else square x) 1 

摺融合與尋找歸納定義   回顧：id :: List a -> List a 可以寫成一個 foldr --- id = foldr (:) []. 而任何函數 f :: List a -> b 都等於 f . id. 如果我們將 f 與 id 融合，會發生什麼事呢？ 首先我們需要找出基底值 f [] 是什麼。 接著我們要找到滿足 f (x:xs) = step x (f xs) 的步驟函數 step. 但這其實就是使用展開-收回轉換尋找 f 的歸納定義！ 只是此處要求的歸納定義比較嚴格：在 f xs 之外不能使用 xs.

確實，第5.1 與5.3 節中許多尋找歸納定義的演算都可以視為使用摺融合生成程式的例子。 以第5.3.1 節的 poly 為例。 找出其歸納定義的過程可以視為摺融合：

   poly x
=  poly x . id
=   {- id = foldr (:) [] -}
   poly x . foldr (:) []
=   {- 摺融合定理 -}
   foldr step (poly x []) 

其中基底值 poly x [] = 0. 而函數 step 須滿足融合條件 poly x (a:as) = step a (poly x as)。 尋找 step 的過程和第頁的計算完全相同。 我們會得到

  poly x (a : as) = a + (poly x as) * x 

到此為止我們便找到了 poly x 的歸納定義。 也可以說，我們已得知 poly x = foldr (\a b -> a + b * x) 0.

6.2.3 掃描

本節將介紹一個本書首次提及，初見時較難理解，但在許多演算法中扮演重要角色的組件函數：掃描（scan）。

如我們所知，函數 sum :: List Int -> Int 計算一個串列的總和。 如果我們想計算一個串列由右到左的累計和，例如當給定串列 [3,7,2,4]，我們希望得到 [16,13,6,4,0]（其中 6 = 2 + 4, 13 = 7 + 2 + 4，16 = 3 + 7 + 2 + 4, 而 0 是空串列的和），該怎麼做呢？

在第2.6.3 節中，我們曾提及計算一個串列所有後段(suffixes)的函數 tails :: List a -> List (List a)。 例如，tails [3,7,2,4] 將得到 [[3,7,2,4], [7,2,4], [2,4], [4], []]。對串列的每一個後段算總和，我們便得到累計和 [16,13,6,4,0] 了：

runsum :: List Int -> List Int
runsum = map sum . tails 

由於使用多個 sum 函數走訪每個後段，如此定義出的 runsum 將是一個執行時間為 $O(n^2)$ 的函數。 但讀者想必已覺得可不用如此費事：我們應該可以在由右到左走訪串列的過程中記住目前為止的和，避免重算 sum。這該怎麼做呢？

回想： sum 可寫成一個摺。因此我們可稍微推廣一下，定義函數 scanr 如下：

scanr :: (a -> b -> b) -> b -> List a -> List b
scanr f e = map (foldr f e) . tails 

給定一個串列 xs, scanr f e 先算出 xs 的所有後段， 然後對每一個後段都做 foldr f e. 前述的 runsum 其實是 scanr 的特例： runsum = scanr (+) 0.

如果把上述的 scanr 定義當作演算法，處理長度為 n 的串列時呼叫 f 的次數為 $O(n^2)$. 我們找找看是否有比較快的演算法。

第 6.1.1 節中提及 tails 是一個 foldr:

tails = foldr (\x xss -> (x : head xss) : xss) [[]] 

也許我們可試著把 map (foldr f e) 融合入 tails 中，看看是否能找出一個較有效率的 scanr 定義。 其融合條件如下：

      map (foldr f e) ((x : head xss) : xss)
 ===    {- map 之定義 -}
      foldr f e (x : head xss) : map (foldr f e) xss
 ===    {- foldr 之定義 -}
      f x (foldr f e (head xss)) : map (foldr f e) xss
 ===    {- g (head ys) = head (map g ys); 令 g := foldr f e, ys := xss -}
      f x (head (map (foldr f e) xss)) : map (foldr f e) xss
 ===    {- 取出 map (foldr f e) xss -}
      let ys = map (foldr f e) xss
      in f x (head ys) : ys 

於是我們推導出了 scanr 的另一個定義：

scanr f e = foldr (\x ys -> f x (head ys) : ys) [e] 

若將 foldr 的定義展開，函數 scanr 可寫成下列的歸納形式，也許比較容易理解：

scanr f e []      = [e]
scanr f e (x:xs)  = f x (head ys) : ys 
    where ys = scanr f e xs 

在第 6.1.1 節中，使得 tails 能寫成一個 foldr 的重要性質是head (tails xs) = xs -- tails xs 的第一個元素就是 xs 本身。使用 tails 定義的 scanr 自然繼承了相關的性質：scanr f e xs 的第一個元素就是 foldr f e xs, 因此可直接用 head 取出，不需每次重新計算。 用本節開頭的例子說明，以下我們令 scr = (\x ys -> x + head ys : ys):

     scanr (+) 0 [3,7,2,4]
===  scr 3 (scr 7 (scr 2 (scr 4 [0])))
===  scr 3 (scr 7 (scr 2 [4 + 0, 0]))
===  scr 3 (scr 7 [2 + 4 + 0, 4 + 0, 0])
===  scr 3 [7 + 2 + 4 + 0, 2 + 4 + 0, 4 + 0, 0]
===  [3 + 7 + 2 + 4 + 0, 7 + 2 + 4 + 0, 2 + 4 + 0, 4 + 0, 0]
===  [16,13,6,4,0] 

其中每個 scr 都可直接使用之前累積計算的結果，不用從頭加起。

6.2.4 香蕉船定理

第5.5.4 節簡短地提到一個例子： 令 sumlen = fork sum length, (註1) 分裂運算元 fork 的定義請參照第1.6.3 節，頁。 直接執行的話，sum 與 length 將各自走訪輸入串列一次， 但我們可推導出 sumlen 的歸納定義，得到一個只走訪串列一次的版本。

上述例子還可以更通用一些。考慮 fork (foldr f1 e1) (foldr f2 e2) --- 這個算式拿一個串列當輸入，兩個 foldr 分別將串列走訪一次，兩個結果分別存放在序對中。我們有可能將它變成一個摺（因此只走訪串列一次）嗎？ 下述的「香蕉船定理(banana-split theorem)」告訴我們：含兩個摺的分裂，可以寫成一個摺。

 fork (foldr f1 e1) (foldr f2 e2) === foldr g (e1,e2) 

分裂運算元 fork 的英文稱呼是 split'', 在程式推導圈內有時會用一套稱作「香蕉括號(banana brackets)」的符號表示摺，兩者合起來便是banana-split'' --- 甜點「香蕉船」的英文名稱。

定理6.12 相當於把兩個處理同一份資料的迴圈合併成一個。 但如同第5.5.4 節提及，這並不保證效率會比較好。 我們會使用定理6.12 的原因可能是如果確定某函數是摺， 我們能做更多後續處理（例如，使用掃描定理或其他只對摺成立的性質）。

「組對」常可視為分裂與 id 的融合。 例如，在第5.5.1 節的陡串列問題中，我們定義 steepsum xs = (steep xs, sum xs)，並試著推導其歸納定義。 該過程也可視為將 fork steep sum 與 id 融合：

     fork steep sum
 ===   {- f . id = f -}
     fork steep sum . id
 ===   {- id = foldr (:) id -}
     fork steep sum . foldr (:) []
 ===   {- 摺融合 -}
     foldr (\x (b, s) -> (x > s ⋀ b, x + s)) (True, 0) 

其融合條件的證明與第5.5.1 節中幾乎相同。

6.2.5 累積參數與摺融合

第5.6 節介紹的「累積參數」技巧也常可視為高階函數與摺的融合。 以第5.6.1 節的經典例子 --- 串列反轉為例。 函數 reverse :: List a -> List a 是一個 foldr:

reverse = foldr (\x xs -> xs ++ [x]) [] 

為增進其效率，我們創造了函數 revcat，其定義為：

revcat :: List a -> List a -> List a
revcat xs ys = reverse xs ++ ys 

但如果把參數都移除，上述定義其實等同於：

revcat = (++) . reverse 

推導 revcat 的歸納定義就是計算 (++) 與 reverse 的融合！

為了導出一個較快的 revcat 實作，我們嘗試把 (++) . reverse 融合為一個 foldr. 其推導大綱如下：

      (++) . reverse
 ===  (++) . foldr (\x xs -> xs ++ [x]) []
 ===    {- 摺融合，試著計算出 base 與 step -}
      foldr step base 

我們可暫停一下，看看這個式子的型別。 函數 (++) 的型別為 List a -> (List a -> List a), (++) . reverse 與 foldr step base 的型別也相同。 如果摺融合成功，我們會得到的是一個傳回函數的 foldr --- 輸入為 List a, 輸出為 List a -> List a. 其中 base 的型別為 List a -> List a, 而 step 的型別將是 a -> (List a -> List a) -> (List a -> List a) --- step x 將一個函數轉成另一個函數。

根據摺融合定理，基底值 base 是

  (++) []  = (\xs -> (++) [] xs)
           = (\xs -> [] ++ xs)
           = (\xs -> xs)
           = id 

步驟函數 step 須滿足的融合條件如下

     (++) ((\x xs -> xs ++ [x]) x xs) === step x ((++) xs) 

簡單地化簡等號左手邊，我們得到：

     (++) (xs ++ [x]) === step x ((++) xs) 

這個式子無法再規約，因為 (++) 還需要一個參數。 因此我們根據外延相等（定義1.8 ），在等號兩邊各補一個參數 ys:

     (++) (xs ++ [x]) ys === step x ((++) xs) ys

為找出 step, 演算如下：

      (++) (xs ++ [x]) ys
 ===  (xs ++ [x]) ++ ys
 ===    {- (++) 之結合律 -}
      xs ++ ([x] ++ ys)
 ===   {- (.) 之定義 -}
     (((++) xs) . (x:)) ys
 ===   {- 將 x, ((++) xs), 與 ys 提出 -}
     (\x f -> f . (x:)) x ((++) xs) ys 

根據外延相等，我們已證明

  (++) (xs ++ [x]) = (\x f -> f . (x:)) x ((++) xs) 

因此 step = (\x f -> f . (x:)), 而 revcat 可寫成如下的摺：

revcat = foldr (\x f -> f . (x:)) id 

例如 revcat "abc" = id . ('c':) . ('b':) . ('a':), 而 revcat "abc" ys = 'c' : ('b' : ('a' : ys)).

6.2.6 引入脈絡

第6.2 節開頭（第頁）曾提及： 使用摺融合定理將 h . foldr f e 融合成 foldr g (h e) 時，融合條件 h (f x y) = g x (h y) 並不需對所有 y 都成立，而只需對在 foldr f e 的值域內的 y 成立即可。 截至目前為止我們看了不少摺融合的例子，但我們所證明的融合條件，均是較寬鬆、對所有 y 都成立的。 我們還沒看過只對特定 y 成立（因此可能較難證明的）融合條件。

知道「y 在 foldr f e 的值域內」，意味著證明融合條件時，我們可以假設 y 滿足所有 foldr f e 的傳回值該滿足的性質。習慣上，「使用這些性質」被稱作「引入脈絡」(bringing in the context) --- 意指做證明時知道 y 不是任意的值，而是由 foldr f e 產生（有特定脈絡）的。此處我們看一個引入脈絡的簡單例子。

psuc n = if n >= 0 then n+1 else 0 

     psuc (m + n) = m + psuc n 

     psuc (square x + y) = square x + psuc y 

  psuc . sumsq = foldr (\x y -> square x + y) 1 

例6.13 是個刻意設計的、簡單的例子。在第TODO節中，我們會看到其他需要引入脈絡的演算法。