5.1 展開-收回轉換
考慮這麼一個例子：給定一個整數形成的串列，我們想計算其每個數的平方的和。例如當輸入是[2,6,5,3], 我們希望算出 $2^2 + 6^2 + 5^2 + 3^2 = 74$. 這項工作可以簡短地描述如下：
函數 sumsq 的型別為 List Int -> Int.
其中 map square 將輸入串列的每個元素都平方，然後由 sum 計算其總和。第2.4 節中給過一個 sum 的歸納定義，重複如下：
sum :: List Int -> Int
sum [] = 0
sum (x:xs) = x + sum xs
消除中間串列
對大部分的應用而言，如上定義的 sumsq 已經很堪用了。但作為一個例子，我們來挑惕些仍不滿意之處。執行 sumsq xs 時，map square 會產生另一個（存放 xs 每個元素的平方的）串列，該串列隨即由 sum 消掉 --- 感覺上似乎很浪費空間與時間。
在惰性求值的情況下，該中間串列的每個節點被產生後立刻被 sum 消去，因此不會真的佔用和 xs 同樣長度的空間。這也是大家覺得惰性求值有助於模組化、使小函數變得易於重用的例子之一。但「產生一個新節點、立刻消去」仍耗了一些不必要的時間。
有不產生這個中間串列的方法嗎？
我們試著做些計算。當 sumsq 的參數是 [] 時：
sumsq []
=== {- sumsq 之定義 -}
sum (map square [])
=== {- map 之定義 -}
sum []
=== {- sum 之定義 -}
0
由此我們得知 sumsq [] 會被計算成 0. 當輸入不是空串列時呢？試計算：
sumsq (x:xs)
=== {- sumsq 之定義 -}
sum (map square (x:xs))
=== {- map 之定義 -}
sum (square x : map square xs)
=== {- sum 之定義 -}
square x + sum (map square xs)
=== {- sumsq 之定義 -}
square x + sumsq xs
可得知對任何 x 與 xs, sum (x:xs) 歸約的結果和 square x + sumsq xs 會是相同的。
總結說來，藉由計算，我們發現 sumsq 滿足以下兩條性質：
但如果我們翻轉過來，把這兩條性質當作 sumsq 的新定義呢？
這是一個依據歸納法定義的良好程式，而且不會產生中間串列！
但我們怎知道 sumsq 的新定義滿足我們最初的要求 ([RefUndefined])，即 sumsq = sum . map square 呢？
回顧起來，我們的演算只證明了當 sumsq 滿足 ([RefUndefined])，它也滿足 ([RefUndefined])，
卻還不能據此宣稱另一個方向：若 ([RefUndefined]) 成立，([RefUndefined]) 也成立。
我們將在第4 章詳細討論這個問題。
目前可暫時這麼說：如果我們從某個問題規格 f = e 起始，發現 f 滿足某一組等式，而這些等式剛好可湊成一個會正常終止的歸納定義，則 e 確實是唯一滿足這些等式的解。由於如此的 e 是唯一的，我們也可倒過來以這組等式為 f 的定義，並同時宣稱 f = e 這個性質成立。
回顧起來，在 sumsq 的計算中，我們僅是把 sumsq 的定義展開，接著展開 map, sum 等等元件的定義，直到我們又看到 sumsq 的定義出現在式子中、剛好可以收回為止。
這是一種單純而歷史悠久的程式推導方法，稱作展開-收回轉換(fold-unfold transformation)。
雖然簡單，有時這個方法意外地有用。
在這個例子中，我們真正做到的是將一個單行、使用全麥編程的 sumsq 定義轉換成了一個歸納定義。
新定義的 sumsq 比起原版稍有效率些，但這只是恰巧發生的 --- 歸納定義的程式不見得總會比較有效率。
程式推導確保程式的正確性 --- 意即導出的程式與原本的規格是同一個函數。
但新程式的效率仍須單獨分析。這是下一節的主題。
練習 5.1
下述函數 descend n 傳回 [n, n-1, n-2...0]:
descend :: Nat -> List Nat
descend Zero = []
descend (Suc n) = Suc n : descend n
定義 sumseries = sum . descend.
請找出 sumseries 的歸納定義。
答案
顯然 sum (descend 0) = 0. 考慮歸納情況：
sum (descend (Suc n))
=== {- descend 之定義 -}
sum (Suc n : descend n)
=== {- sum 之定義 -}
(Suc n) + sum (descend n)
=== {- sumseries 之定義 -}
(Suc n) + sumseries n
因此
sumseries Zero = Zero
sumseries (Suc n) = (Suc n) + sumseries n
練習 5.2
承接習題5.1 。函數 repeatN :: (Nat × a) -> List a 的定義為
repeatN (n,x) = map (const x) (descend n)
因此，repeatN (n,x) 會傳回一個含 n 個 x 的串列。
例如 repeatN (3,'a') = "aaa".
請算出一個歸納定義的 repeatN.
答案
顯然 repeatN (0,x) = [].
至於歸納情況，演算如下：
repeatN (Suc n, x)
=== {- repeatN 之定義 -}
map (const x) (descend (Suc n))
=== {- descend 之定義 -}
map (const x) (Suc n : descend n)
=== {- map 與 const 之定義 -}
x : map (const x) (descend n)
=== {- repeatN 之定義 -}
x : repeatN (n,x)
因此，
repeatN (Zero, x) = []
repeatN (Suc n, x) = x : repeatN (n,x)
練習 5.3
承接習題5.2 。遊程編碼(run-length encoding)是一種簡單的壓縮方式：將字串中重複的字元表達成其出現的數字。例如 "aaabbbbcdd" 可以表達為 "3a4b1c2d". 下列函數 rld :: List (Nat × a) -> List a 則是抽象過的「遊程解碼」，將已經表示成（次數$\times$字元）的壓縮文展開：
rld = concat . map repeatN
例如， rld [(2,'a'), (3,'b'), (1,'c')] = "aabbbc".
請導出 rld 的歸納定義。
答案
基底狀況：
rld []
= {- rld 之定義 -}
concat (map repeatN [])
= {- map 與 concat 之定義 -}
[]
歸納狀況：
rld ((n,x):xs)
=== {- rld 之定義 -}
concat (map repeatN ((n,x):xs))
=== {- map 之定義 -}
concat (repeatN (n,x) : map repeatN xs)
=== {- concat 之定義 -}
repeatN (n,x) ++ concat (map repeatN xs)
=== {- rld 之定義 -}
repeatN (n,x) ++ rld xs
因此我們已推導出：
rld [] = []
rld ((n,x):xs) = repeatN (n,x) ++ rld xs
練習 5.4
下列函數 delete 將輸入串列中的每個元素輪流刪除：
delete :: List a -> List (List a)
delete [] = []
delete (x:xs) = xs : map (x:) (delete xs)
例如，delete [1,2,3,4] = [[2,3,4], [1,3,4], [1,2,4], [1,2,3]].
函數 select :: List a -> List (a × List a) 則將一個串列中的元素依次選出。
例如，select [1,2,3,4] = [(1,[2,3,4]), (2,[1,3,4]), (3,[1,2,4]), (4,[1,2,3])]. 函數 select 恰巧可用 delete 定義出來：
select xs = zip xs (delete xs)
請推導出 select 的歸納定義。提示：下述性質可能有用 ---
zip xs (map f ys) = map (id *** f) (zip xs ys).
答案
顯然 select [] = []。考慮 xs := x:xs 的情況：
select (x:xs)
=== {- select 與 delete 之定義 -}
zip (x:xs) (xs : map (x:) (delete xs))
=== {- zip 之定義 -}
(x, xs) : zip xs (map (x:) (delete xs))
=== {- zip xs (map f ys) = map (id *** f) (zip xs ys) -}
(x, xs) : map (id *** (x:)) (zip xs (delete xs))
=== {- select 之定義 -}
(x, xs) : map (id *** (x:)) (select xs)
因此，
select [] = []
select (x:xs) = (x, xs) : map (id *** (x:)) (select xs)
練習 5.5
函數 delete 有另一個可能定義：
delete xs = map (del xs) [0..length xs-1]
where del xs i = take i xs ++ drop (1+i) xs
（此處我們利用了當 n 為負數時，[0..n] 化簡成 [] 的特性。）
請用此定義推導出 delete 的歸納定義。提示：你可能用得上下述性質：
[0..n] = 0 : map (1+) [0..n-1]\mbox{,~~ if n >= 0,} (5.1 )
答案
以下只列出歸納狀況：
delete (x:xs)
=== {- delete 之定義 -}
map (del (x:xs)) [0..length (x:xs) -1]
=== {- length 之定義，簡單運算 -}
map (del (x:xs)) [0..length xs]
=== {- 由於 length xs >= 0, 使用 \eqref{eq:gen-split} -}
map (del (x:xs)) (0 : map (1+) [0..length xs-1])
=== {- map 之定義 -}
del (x:xs) 0 : map (del (x:xs)) (map (1+) [0..length xs-1])
=== {- map 融合 -}
del (x:xs) 0 : map (del (x:xs) . (1+)) [0..length xs-1]
在此暫停一下，觀察 del (x:xs). 顯然, del (x:xs) 0 = xs. 至於 del (x:xs) . (1+)，我們演算看看:
(del (x:xs) . (1+)) i
=== {- (.) 與 del 之定義 -}
take (1+ i) (x:xs) ++ drop (1+ (1+ i)) (x:xs)
=== {- take 與 drop 之定義 -}
x : take i xs ++ drop (1+ i) xs
=== {- del 之定義 -}
x : del xs i
=== {- (.) 之定義 -}
((x:) . del xs) i
繼續之前的演算：
del (x:xs) 0 : map (del (x:xs) . (1+)) [0 .. length xs - 1]
=== {- 前述之演算 -}
xs : map ((x:) . del xs) [0 .. length xs - 1]
=== {- map 融合 -}
xs : map (x:) (map (del xs) [0 .. length xs - 1])
=== {- delete 之定義 -}
xs : map (x:) (delete xs)
由此，我們導出了正文中 delete 的歸納定義.