2 歸納定義與證明

2.6 更多歸納定義與證明

為讓讀者熟悉，本節中我們多看一些自然數或串列上的歸納定義。

2.6.1 filter, takeWhile, 與 dropWhile

filter   我們曾見過的函數 filter 可寫成如下的歸納定義：

filter :: (a -> Bool) -> List a -> List a
filter p []      = []
filter p (x:xs)  = if p x then x : filter p xs else filter p xs

在 filter 的許多性質中，我們試著證明下述性質作為例子：

定理 2.4

filter p . map f = map f . filter (p . f).

證明

和定理2.2 一樣，待證式的左右邊都是函數。 根據外延相等，我們將左右邊各補上參數 xs，並在 xs 上做歸納：

  filter p (map f xs) = map f (filter (p . f) xs)

情況 x := [] 中左右邊都可化簡成[]. 我們看看 xs := x:xs 的情況：

   filter p (map f (x:xs))
 ===    {- map 之定義 -}
   filter p (f x : map f xs)
 ===    {- filter 之定義 -}
   if p (f x)  then f x : filter p (map f xs) else filter p (map f xs)
 ===    {- 歸納假設 -}
   if p (f x)  then f x : map f (filter (p . f) xs) else map f (filter (p . f) xs)
 ===    {- map 之定義 -}
   if p (f x)  then map f (x : filter (p . f) xs) else map f (filter (p . f) xs)
 ===    {- 因 f (if p then e1 else e2) = if p then f e1 else f e2, 如後述 -}
   map f (if p (f x) then x : filter (p . f) xs else filter (p . f) xs)
 ===    {- filter 之定義 -}
   map f (filter (p . f) (x:xs))

終止與證明   上述證明的倒數第二步為將 map f 提到外面，用了一個關於 if 的性質：

  f (if p then e1 else e2)  =  if p then f e1 else f e2     (2.4 )

這性質對嗎？若 p 成立，左右手邊都化簡為f e1, 若 p 不成立，左右手邊都化簡為 f e2. 因此 (2.4 ) 應該成立，是嗎？

答案是：如果我們假設的世界中有不終止的程式，(2.4 )便不正確了。 例如，當 f 是 three x = 3，而 p 是個永遠執行、不終止的算式（例：let b = not b in b)：

  three (if p then e1 else e2) {-"~\stackrel{?}{=}~"-} if p then three e1 else three e2     (2.5 )

上述式子的左手邊直接化簡成3, 但右手邊卻不會終止，因為 if 得知道 p 的值。 我們找到了 (2.4 ) 的反例！

在允許可能不終止的程式存在的世界中，(2.4 )得多些附加條件。 通常的做法是限定 f 須是個嚴格函數, 意即 f 的輸入若不終止，f也不會終止。 但(2.4 )並不是唯一帶著附加條件的性質 --- 許多常用性質都得加上類似的附加條件。 所有狀況分析也都得將不終止考慮進去，例如，自然數除了 Zero 與 Suc n 之外，還多了第三種情況「不終止」。Bird [1987] 就採用這種作法。 推論與證明變得更複雜。 有些人因此較喜歡另一條路：藉由種種方法確保我們只寫出會終止的程式，便可假設我們確實活在所有程式都正常終止的世界中。

保護式 v.s. 條件分支   有些人喜歡用保護式語法定義 filter：

filter p []      = []
filter p (x:xs)  | p x        = x : filter p xs
                 | otherwise  = filter p xs

若在此定義下證明定理2.4 ，依「證明的結構與程式的結構相同」的原則，順理成章地，我們可在 xs:=x:xs 中再分出 p (f x) 成立與不成立的兩個子狀況：

  • 狀況 xs := []: ...

  • 狀況 xs := x:xs: ...

    • 狀況 p (f x):

         filter p (map f (x:xs))
=    {- p (f x) 成立 -}
   f x : filter p (map f xs)
=  ...

    • 狀況 not (p (f x)):

         filter p (map f (x:xs))
=   {- (not p (f x)) -}
   filter p (map f xs)
=  ...

這個定義中不用 if, 因此證明中也用不上 (2.4 ), 但該證明要成立仍須假設所有程式都正常終止 --- 我們少證了一個 「p (f x) 不終止」的情況（而確實，在此情況下(2.4 )並不成立）。喜歡用哪個方式純屬個人偏好。

前幾章提過的 takeWhile 與 dropWhile 兩函數型別與 filter 相同。他們可寫成如下的歸納定義：

takeWhile :: (a -> Bool) -> List a -> List a
takeWhile p []      = []
takeWhile p (x:xs)  = if p x then x : takeWhile p xs else [] 

dropWhile :: (a -> Bool) -> List a -> List a
dropWhile p []      = []
dropWhile p (x:xs)  = if p x then dropWhile p xs else x:xs

兩者都是在輸入串列上做歸納。兩者也都可用保護式語法定義。

練習 2.14

證明 takeWhile p xs ++ dropWhile p xs = xs.

練習 2.15

以保護式語法定義 takeWhile 與 dropWhile, 以此定義做做看習題 2.14 .

2.6.2 elem 與不等式證明

不等式證明   給定如下的定義，elem x xs 判斷 x 是否出現在串列 xs 中：

elem x []      = False
elem x (y:xs)  = (x == y) || elem x xs

目前為止，我們所練習的都是以(=)將式子串起的等式證明。 以下以elem為例，我們嘗試證明一個「不等式」：

  elem z xs  ==>  elem z (xs ++ ys)

以口語說出的話：「若z 出現在xs 中，z 也出現在xs ++ ys 中」。 欲證明上式，該從哪一側推到哪一側呢？ 一般認為從式子較長、或結構較複雜的那側開始，化簡成較短、較簡單的那側，是較容易的。 因此我們嘗試由右側推到左側：由 elem z (xs ++ ys) 開始，尋找使之成立的條件， 並希望 elem z xs 是足夠的。

證明

在 xs 上做歸納。基底 xs := [] 的狀況在此省略， 看 xs:=x:xs 的狀況：

     elem z ((x:xs) ++ ys)
<=>   {- (++) 之定義 -}
     elem z (x : (xs ++ ys))
<=>   {- elem 之定義 -}
     (z==x) || elem z (xs ++ ys)
<==   {- 歸納假設 -}
     (z==x) || elem z xs
<=>   {- elem 之定義 -}
     elem z (x:xs)

讀者可注意：第1, 2, 4 步使用的邏輯關係都是 (<=>) ，第 3 步卻是 (<==)，因此整個證明建立了「若elem z (x:xs)，則elem z ((x:xs) ++ ys)」。

練習 2.16

證明 not (elem z (xs ++ ys)) ==> not (elem z xs).

練習 2.17

證明 elem z xs ==> elem z (ys ++ xs).

練習 2.18

證明(∀ x . p x ==> q x) ==> all p xs ==> all q xs. 其中 all 的定義為：

all :: (a -> Bool) -> List a -> Bool
all p []      = True
all p (x:xs)  = p x ⋀ all p xs
練習 2.19

證明 all (`elem` xs) (filter p xs). 其中 x `elem` xs 是 elem x xs 的中序寫法。 我們可能需要習題 2.17 和 2.18 的結果，以及下述性質：

    if p then x else x = x     (2.6 )
答案

在 xs 上做歸納。

      all (`elem` (x:xs)) (filter p (x:xs))
 <=>  all (`elem` (x:xs)) (if p x then x:filter p xs else filter p xs)
 <=>  if p x  then all (`elem` (x:xs)) (x:filter p xs)
              else all (`elem` (x:xs)) (filter p xs)
 <=>  if p x  then x `elem` (x:xs) ⋀ all (`elem` (x:xs)) (filter p xs)
              else all (`elem` (x:xs)) (filter p xs)
 <==  if p x  then all (`elem` (x:xs)) (filter p xs)
              else all (`elem` (x:xs)) (filter p xs)
 <=>     {- \eqref{eq:ifpxx} -}
      all (`elem` (x:xs)) (filter p xs)
 <==     {- 因習題 2.17, z `elem` (x:xs) <== z `elem` xs -}
      all (`elem` xs) (filter p xs)
 <==  True

2.6.3 串列區段

前段與後段   本章目前為止討論的歸納定義都依循著這樣的模式：欲定義 f :: List a -> b, 只要為 f [] 與 f (x:xs) 找到定義。在定義後者時，只需定義出由 f xs 做出 f (x:xs) 的關鍵一步。 目前為止，這關鍵一步都是加一、加上一個元素等簡單的動作。現在我們來看些更複雜的例子。

例1.19 中曾提及：如果一個串列 xs 可分解為 ys ++ zs, 我們說 ys 是 xs 的一個前段(prefix), zs 是 xs 的一個後段(suffix). 例如，串列 [1,2,3] 的前段包括 [], [1], [1,2], 與[1,2,3] （注意：[]是一個前段，串列 [1,2,3] 本身也是）, 後段則包括 [1,2,3], [2,3], [3], 與 []。我們是否能定義一個函數 inits :: List a -> List (List a), 計算給定串列的所有前段呢？ 例1.19 給的答案是：

inits xs = map (\n -> take n xs) [0 .. length xs]

如果不用組件，改用歸納定義呢？我們試試看：

inits :: List a -> List (List a)
inits []      = ?
inits (x:xs)  = ?

基底狀況 inits [] 的可能選擇是 [[]] （見後述）。至於歸納步驟該怎麼寫？ 我們用例子來思考。比較 inits [2,3] 與 inits [1,2,3]:

  inits [2,3]    = [[],[2],[2,3]] 
  inits [1,2,3]  = [[],[1],[1,2],[1,2,3]]

假設我們已算出 inits [2,3], 如何把它加工變成 inits [1,2,3]? 請讀者暫停一下，思考看看！

一個思路是：如果在 [[],[2],[2,3]] 中的每個串列前面都補一個 1, 我們就有了 [[1],[1,2],[1,2,3]]. 再和 inits [1,2,3] 比較，就只差一個空串列了！ 因此 inits 的一種定義方式是：

inits :: List a -> List (List a)
inits []      = [[]]
inits (x:xs)  = [] : map (x:) (inits xs)

在此得提醒：有些讀者認為基底狀況 inits [] 的值選為 [[]]，是因為結果的型別是 List (List a) （直覺地把每個 List 都對應到一組中括號，或認為 [[]] 是型別為 List (List a) 的最簡單的值）。 但事實並非如此：畢竟，[] 的型別也可以是 List (List a)！ 我們讓 inits [] = [[]] 的原因是空串列 [] 的「所有前段」只有一個，恰巧也是 []。 就如同在自然數上的歸納函數定義中，有些基底狀況是 0, 有些是 1, 有些是別的值， 此處我們也依我們的意圖，選定最合適的基底值。

練習 2.20

試定義 initsp :: List a -> List (List a), 計算一個串列的所有非空前段。例如 initsp [1,2,3] 是 [[1],[1,2],[1,2,3]]。當然，其中一個定義方式是 initsp = tail . inits. 你能以歸納方式定義出 initsp 嗎？

initsp []      = ?
initsp (x:xs)  = ?
答案
initsp :: List a -> List (List a)
initsp []      = []
initsp (x:xs)  = [x] : map (x:) (initsp xs)
練習 2.21

我們驗證一下 inits 在例1.19 中的組件定義與本章的歸納定義是相等的。定義 upto :: Nat -> List Nat:

upto Zero     = [Zero]
upto (Suc n)  = 0 : map (Suc) (upto n)

使得 upto n = [0.. n]. 假設 inits 已如本節一般地歸納定義，證明對所有 xs, inits xs = map (\n -> take n xs) (upto (length xs)). 您可能會需要 map 融合定理（定理2.2 ），

答案

在 xs 上做歸納。

情況 xs := []. 此時等號兩邊都是 [[]].

情況 xs := x:xs.

    map (\n -> take n (x:xs)) (upto (length (x:xs)))
 ===    {- length 之定義 -}
    map (\n -> take n (x:xs)) (upto (Suc (length xs)))
 ===    {- upto 之定義 -}
    map (\n -> take n (x:xs)) (0 : map (Suc) (upto (length xs)))
 ===    {- length 之定義 -}
    map (\n -> take n (x:xs)) (0 : map (Suc) (upto (length xs)))
 ===    {- map之定義，take 0 (x:xs) = [] -}
    [] : map (\n -> take n (x:xs)) (map (Suc) (upto (length xs)))
 ===    {- 定理2.2：map f . map g = map (f.g) -}
    [] : map (\n -> take (Suc n) (x:xs)) (upto (length xs))
 ===    {- take 之定義 -}
    [] : map (\n -> x : take n xs) (upto (length xs))
 ===    {- 定理2.2：map f . map g = map (f.g) -}
    [] : map (x:) (map (\n -> take n xs) (upto (length xs)))
 ===    {- 歸納假設 -}
    [] : map (x:) (inits xs)
 ===    {- inits 之定義 -}
    inits (x:xs)

定義傳回後段的函數 tails 時可依循類似的想法： 如何把 tails [2,3] = [[2,3],[3],[]]加工，得到 tails [1,2,3] = [[1,2,3],[2,3],[3],[]]? 這次較簡單：加上 [1,2,3] 即可。 的確，串列 x:xs 的後段包括 x:xs 自己，以及 xs 的後段：

tails :: List a -> List (List a)
tails []      = [[]]
tails (x:xs)  = (x:xs) : tails xs

在習題 2.45 中我們將證明一個將 inits 與 tails 牽上關係的定理：將 inits 傳回的前段與 tails 傳回的後段照其順序對應，每對接起來都是原來的串列。

連續區段   給定一個串列，許多傳統最佳化問題的目標是計算符合某條件的連續區段（簡稱「區段」）。 例如，[1,2,3] 的區段包括[],[1],[2],[3],[1,2],[2,3], 以及 [1,2,3]本身。 我們可用 inits 與 tails 得到一個串列的所有區段。

segments :: List a -> List (List a)
segments = concat . map inits . tails

但 segments 無法寫成本章目前這種形式的歸納定義。我們將在以後的章節再討論到 segments.

練習 2.22

試著把 segments 寫成如下的歸納定義：

segments :: List a -> List (List a)
segments []      = ?
segments (x:xs)  = ... segments xs ...

在歸納步驟中希望由 segments xs 湊出 segments (x:xs)。 這是能在不對輸入串列（型別為List a）做任何限制之下做得到的嗎？ 如果做不到，為什麼？

答案

考慮如何從 segments [1,2,3] 湊出 segments [0,1,2,3]. 前者應當有的結果可能是：

[[],[1],[1,2],[1,2,3],[2],[2,3],[3]]

而 segments [0,1,2,3] 的結果可能是：

[[],[0],[0,1],[0,1,2],[0,1,2,3],[1],[1,2],[1,2,3],[2],[2,3],[3]]

乍看之下，要多做的一步是：在空串列或所有1開頭的串列前面補上 0. 之所以只擴充1開頭的串列，因為只有這些是原本便靠在左邊，和 0 相鄰的 （也就是說它們是[1,2,3]的前段）。

然而，當輸入串列型別為 List a（而不是特定的 List Int, List Char 時），我們無法用比較的方式找出這些前段。函數 segments 傳回的資訊不夠多。如果要歸納定義，我們必須把「前段」們和其他的區段分開。

2.6.4 插入、排列、子串列、與劃分

排列   函數 fan x xs 把 x 插入 xs 的每一個可能空隙。例如，fan 1 [2,3,4] 可得到 [[1,2,3,4],[2,1,3,4],[2,3,1,4],[2,3,4,1]]. 讀者不妨想想它該怎麼定義？一種可能方式如下：

fan :: a -> List a -> List (List a)
fan x []      = [[x]]
fan x (y:xs)  = (x:y:xs) : map (y:) (fan x xs)

有了 fan, 我們不難定義 perms :: List a -> List (List a), 計算一個串列所有可能 的排列。例如，perms [1,2,3] = [[1,2,3], [2,1,3], [2,3,1], [1,3,2], [3,1,2], [3,2,1]]：

perms :: List a -> List (List a)
perms []      = [[]]
perms (x:xs)  = concat (map (fan x) (perms xs))

讀者可思考為何我們需要 concat? 如果沒有，會出現什麼錯誤？

基於 perm 的這個定義，我們證明一個定理：長度為 n 的串列有 fact n 種排列。 這個證明將使用到許多輔助性質與引理，有些已經是我們之前證明過的習題，有些則可作為接下來的習題。 在本證明之中我們也練習將連續的函數應用 f (g (h x)) 寫成函數合成 f . g . h $ x 以方便計算。

定理 2.5

對任何 xs, length (perms xs) = fact (length xs).

證明

在 xs 上做歸納。

基底狀況 xs:=[]:

      length (perms [])
 ===  length [[]]
 ===  1
 ===  fact (length [])

歸納步驟 xs := x:xs:

      length (perms (x:xs))
 ===    {- perms, (.), 與 ($) 之定義 -}
      length . concat . map (fan x) . perms $ xs
 ===    {- 因 length . concat = sum . map length (習題2.12), map 融合 -}
      sum . map (length . fan x) . perms $ xs
 ===    {- 因 length . fan x = (Suc) . length (習題 2.25) -}
      sum . map ((Suc) . length) . perms $ xs
 ===    {- 因 map length (perms xs) =
 map (const (length xs)) (perms xs) (習題2.26)  -}
      sum . map ((Suc) . const (length xs)) . perms $ xs
 ===    {- 因 sum (map (Suc) xs) = length xs + sum xs (習題2.8)-}
      length (perms xs) + sum (map (const (length xs)) (perms xs))
 ===    {- 因 sum (map (const y) xs) = y * length xs (習題2.9) -}
      length (perms xs) + length xs *: length (perms xs)
 ===    {- 四則運算: x + y * x = (1+y) * x -}
      (Suc (length xs)) *: length (perms xs)
 ===    {- 歸納假設 -}
      (Suc (length xs)) *: fact (length xs)
 ===    {- fact 之定義 -}
      fact (Suc (length xs))
 ===    {- length 之定義 -}
      fact (length (x:xs))
練習 2.23

證明 map f . fan x = fan (f x) . map f.

練習 2.24

證明 perm . map f = map (map f) . perm.

練習 2.25

證明 length (fan x xs) = Suc (length xs).

答案

在 xs 上做歸納。基底狀況很容易成立。考慮 xs := y:xs:

      length (fan x (y:xs))
 ===  length ((x:y:xs) : map (y:) (fan x xs))
 ===  Suc (length (map (y:) (fan x xs)))
 ===   {- 因 length . map f = length (練習 2.6) -}
      Suc (length (fan x xs))
 ===   {- 歸納假設 -}
      Suc (Suc (length xs))
 ===  Suc (length (y:xs))
練習 2.26

證明 perms xs 傳回的每個串列都和 xs 一樣長，也就是 map length (perms xs) = map (const (length xs)) (perms xs) --- const y 是一個永遠傳回 y 的函數。

答案

欲證明 map length (perms xs) = map (const (length xs)) (perms xs), 在 xs 之上做歸納。基底狀況 xs := [] 中，等號兩邊都化約為 [0]. 考慮歸納步驟 xs := x:xs:

  map length (perms (x:xs))
 ===   {- perms 之定義 -}
  map length . concat . map (fan x) . perms $ xs
 ===   {- map f . concat = concat . map (map f) (習題2.13), map 融合 -}
  concat . map (map length . fan x) . perms $ xs
 ===   {- map length . fan x = (\n -> repeatN n n) . length -}
  concat . map ((\n -> repeatN n n) . (Suc) . length) . perms $ xs
 ===   {- map 融合 -}
  concat . map ((\n -> repeatN n n) . (Suc)) . map length . perms $ xs
 ===   {- 歸納假設 -}
  concat . map ((\n -> repeatN n n) . (Suc)) . map (const (length xs)) . perms $ xs
 ===   {- map 融合 -}
  concat . map ((\n -> repeatN n n) . (Suc) . const (length xs)) . perms $ xs
 ===   {- 歸約 $\lambda$ 算式 -}
  concat . map (repeatN (Suc (length xs)) . (Suc) . length) . perms $ xs
 ===   {- length . fan x = (Suc) . length (習題2.25)-}
  concat . map (repeatN (Suc (length xs)) . length . fan x) . perms $ xs
 ===   {- \todo{???} map (const y) = repeatN y . length -}
  concat . map (map (const (Suc (length xs))) . fan x) . perms $ xs
 ===   {- map f . concat = concat . map (map f) (習題2.13) -}
  map (const (length (x:xs))) . concat . map (fan x) . perms $ xs
 ===   {- perms 之定義 -}
  map (const (length (x:xs))) (perms (x:xs))

子串列   函數 sublists :: List a -> List (List a) 計算一個串列的所有子串列。 後者是類似子集合的概念，只是把順序也考慮進去： ys 是 xs 的子串列， 如果將 xs 中的零個或數個元素移除後可得到 ys: 例如 sublists [1,2,3] 的結果可能是： [[],[3],[2],[2,3],[1],[1,3],[1,2],[1,2,3]]。 怎麼定義 sublists 呢？在基底狀況中，空串列仍有一個子串列 []. 歸納步驟中，x:xs 的子串列可分為兩種：不含 x 的，以及含 x 的。 不含 x 的子串列就是 xs 的所有子串列（以下稱作 yss）， 而含 x 的子串列就是 yss 中的每個串列接上 x. 因此我們可定義：

sublists :: List a -> List (List a)
sublists []      = [[]]
sublists (x:xs)  = yss ++ map (x:) yss 
    where yss = sublists xs
練習 2.27

定義 splits :: List a -> List (List a × List a)， 使 splits xs 傳回所有滿足 ys ++ zs 的 (ys,zs). 例：

   &splits [1,2,3] = [([],[1,2,3]), ([1],[2,3]), ([1,2],[3]), ([1,2,3,[]])]

另一種說法是 splits xs = zip (inits xs) (tails xs).

答案
splits :: List a -> List (List a × List a)
splits []      = [([],[])]
splits (x:xs)  = ([],x:xs) : map ((x:)***id) (splits xs)

其中 (f *** g) (x,y) = (f x, g y), 定義於第 1.6.3 節。

練習 2.28

證明 length . sublists = exp 2 . length. 也就是說，長度為 n 的串列的子串列數目為 $2^n$. 你會需要的性質可能包括 (2.2 ) (length (xs++ys) = length xs + length ys), 以及 length . map f = length.

答案

將式子改寫為 length (sublists xs) = exp 2 (length xs), 在 xs 上做歸納。 歸納步驟 xs := x:xs 為：

      length (sublists (x:xs))
 ===  length (sublists xs ++ map (x:) (sublists xs))
 ===    {- 因 \eqref{eq:length-append} length (xs++ys) = length xs + length ys  -}
      length (sublists xs) + length (map (x:) (sublists xs))
 ===    {- 因 length . map = length (練習 2.6)-}
      length (sublists xs) + length (sublists xs)
 ===    {- 因 x + x = 2 * x -}
      2 *: length (sublists xs)
 ===    {- 歸納步驟 -}
      2 *: exp 2 (length xs)
 ===  exp 2 (Suc (length xs))
 ===  exp 2 (length (x:xs))

劃分   給定串列 xs :: List a. 如果 yss :: List (List a) 滿足

  1. concat yss = xs,

  2. yss 中的每個串列都不是空的， 我們便說 yss 是 xs 的一個劃分(partition)。 例如，[[1],[2,3],[4]] 是 [1,2,3,4] 的一個劃分。

我們是否能定義一個函數 parts :: List a -> List (List (List a)), 計算一個串列所有的劃分？ 可能的方式有很多，其中一種思路如下。首先，空串列 [] 只有一個可能的劃分，即是 []. 考慮 x:xs, 如果 xs 已經被劃分完畢，對於 x 我們有兩個選擇：讓它成為單獨的串列， 或著將 xs 加入最左邊的串列。 寫成歸納定義如下：

parts :: List a -> List (List (List a))
parts []      = [[]]
parts (x:xs)  = concat (map (extend x) (parts xs)) 
  where  extend x []        = [[[x]]]
         extend x (ys:yss)  = [[x]:ys:yss, (x:ys):yss]

遞迴呼叫 parts xs 找出 xs 的所有劃分， 輔助函數 extend x :: List (List a) -> List (List (List a)) 則作用在其中一個劃分上。 我們得分出兩個狀況：

  1. 如果該劃分含第一個串列 ys 和剩下的 yss, 我們可選擇讓 x 自成一個串列，或著加入 ys 中。 我們把這兩種選擇收集到一個串列中，因此 extend 的結果有三層 List。

  2. 如果該劃分是空的，加入 x 的劃分必定是 [[x]]，但仍需放入一個串列中，表示「只有這一個選擇」。

呼叫 map (extend x) 的結果需再用一個 concat 聯集在一起。

反函數

假設我們有一個取反函數的運算元：給定 f :: a -> b, 其反函數 inv f 的型別是 b -> List a。 inv f y 將所有使得 f x = y 的 x 收集在串列中。 則 parts 可以有一個更接近本節中文字描述的定義：

  parts = filter (all (not . null)) . inv concat

計算 parts xs 時，我們用 inv concat 找出所有滿足 concat yss = xs 的 List (List a), 並且只挑出不含空串列的。

上述定義可以轉換成本節的歸納定義。相關研究可參考 Mu and Bird [2003].