5 一般程式推導

5.5 組對

接下來我們介紹另一個重要的技巧:「組對(tupling)」。

5.5.1 陡串列

給定一個整數串列。當我們說它很「陡」,意思是它由左到右下降得極快,快到每一個元素都大於其右邊所有元素的和。形式化的定義如下:

steep :: List Int -> Bool
steep []      = True
steep (x:xs)  = x > sum xs ⋀ steep xs 

如果當作一個程式,當輸入串列長度為 n, 由於反覆呼叫 sum, 上述的程式需要 $O(n^2)$ 的時間。 但每次算出的 sum xs 和 x 比較後便立刻被丟棄,似乎很浪費。我們能否把 sum 的結果存下來呢? 下述函數 steepsum 把 steep 與 sum 都算出來,放在一個序對中:

steepsum :: List Int -> (Bool × Int)
steepsum xs = (steep xs, sum xs) 

我們看看 steepsum 能否算得快一點?

根據定義,steepsum [] = (True, 0). 我們看看 xs = x:xs 的例子:

      steepsum (x:xs)
 ===    {- steepsum 之定義 -}
      (steep (x:xs), sum (x:xs))
 ===    {- steep 與 sum 之定義 -}
      (x > sum xs ⋀ steep xs, x + sum xs)
 ===    {- 將子算式提取至 let 中 -}
      let (b, s) = (steep xs, sum xs)
      in (x > s ⋀ b, x + s)
 ===    {- steepsum 之定義 -}
      let (b, s) = steepsum xs
      in (x > s ⋀ b, x + s) 

我們已推導出:

steepsum []      =  (True, 0)
steepsum (x:xs)  =  let (b, s) = steepsum xs
                    in (x > s ⋀ b, x + s) 

這是一個只用 $O(n)$ 時間的程式。 有了 steepsum,我們可重新定義 steep 為 steep = fst . steepsum。

讓一個函數多傳回一些值的動作稱作組對(tupling) --- 因為多傳回的值被放在一個序對中。 在一些函數語言中,pair'' 指含兩個成員的序對,tuple'' 則不限定為兩個成員。Tuple 也可當作動詞,指做出一個 tuple. 本書將動詞的 tuple 譯為「組對」-- 組出一個對。有些語言中 pair 與 tuple 有更根本的差異,但本書中不做區分。 我們常用此技巧來存下可重複使用的中間值,並減少走訪資料結構的次數。

最後一提:若使用第1.6.3 節,頁介紹的「分裂」運算元:

fork :: (a -> b) -> (a -> c) -> a -> (b × c)
(fork f g) x = (f x, g x) 

函數 steepsum 的定義可較簡潔地寫成:

steepsum = fork steep sum 

本書將在適當時採用這種寫法。

責任越大,能力越強?   某個意義上,函數 steepsum 做的事比 steep 多: 後者只判斷輸入是否為陡串列,前者不只如此,還多附送了串列的和。 然而,傳回較多東西、似乎做了更多事的程式,反倒可以執行得比較快。 竟出現「責任越大,能力越強」這種違反直覺的現象,這是怎麼回事呢? 「能力越強,責任越大 (with great power comes great responsibility)」是 2002 年版《蜘蛛人》電影的名句。根據考證 [O'Toole 2017], 法國國民公會1793年的政令中即出現過類似的想法,包括邱吉爾和羅斯福等人也都說過類似話語的不同版本。

其實,在歸納定義與歸納證明中,這都是常見的。 有些比較通用的程式反倒比較容易定義;有些定理本身不好證明,為了證明它,我們把它變得更廣泛、更強些,反倒好證了。 箇中原因說穿了便不難理解, 函數 steepsum 便是一個容易明白的好例子:一個函數若傳回較多資訊,在遞迴呼叫它時,我們便有更多資訊可直接取用。 同樣地,一個定理若保證更強的性質,表示在使用歸納假設的步驟中,我們有了更強的性質可用。

如果我們把一個函數或待證的定理擴充得太強,確實也有可能使它們強到寫不出來、證不出來。 做歸納定義或證明的重要技巧之一,便是找到這麼一個平衡點:將一個待定義或證明的物件擴充到足以提供歸納步驟需要的所有資訊,又不至於強到無法寫出、證出。

在這一節以及下一節中,我們都會看到許多如此的例子。

5.5.2 以串列標記樹狀結構

我們再舉一個組對的好例子。回顧第 1.10 與2.8 節中提及的外標籤二元樹:

data ETree a  = Tip a | Bin (ETree a) (ETree a) 

下述函數 size :: ETree a -> Int 計算一棵樹中標籤的數目(對 ETree 而言是 Tip 出現的次數); repl t xs 則將 t 原有的標籤丟棄,改用串列 xs 由右至左依序重新為 t 上標籤。 觀察:在遞迴呼叫中,我們用 take 和 drop 將串列 xs 截成適當的長度:

size (Tip _)    = 1
size (Bin t u)  = size t + size u 

repl :: ETree a -> List b -> ETree b
repl (Tip _)    xs = Tip (head xs)
repl (Bin t u)  xs = Bin (repl t (take n xs)) (repl u (drop n xs))
    where n = size t 

如果 t 是一個向左傾斜的二元樹,repl t xs 不僅會反覆計算 size,也會反覆地將 take 與 drop 用在 xs 上,使得上述的 repl 成為一個 $O(n^2)$ 的演算法。 利用組對的技巧,我們能讓 repl 的時間複雜度小一些嗎?

我們試著把 repl 作用在一個稍微左斜的樹,(Bin (Bin t u) v) 之上,看看有什麼能做的。 令 t, u 的 size 分別為 n1 與 n2. 如果我們希望導出一個線性時間的程式,其中一個提示是:我們希望在 repl (Bin (Bin t u) v) xs 中,xs 的每個元素最多都只被 take 和 drop 各碰過一次。 依此原則,以下的推導基嘗試做到兩點:首先,把連續的 take 消去;其次,若已做了 take n1 xs,就避免再出現 take (n1 + n2) xs,因為後者的存在會讓 take 重複處理 xs 中的元素。 我們會用到習題 2.39 -- 2.41 中提到的三個性質:

take m (take (m+n) xs) ~&=~ take m xs
\mbox{~~,}\\
drop m (take (m + n) xs) ~&=~ take n (drop m xs)\mbox{~~,}\\
drop (m + n) xs ~&=~ drop n (drop m xs) 

其中 m, n 均為自然數。試演算如下:

      repl (Bin (Bin t u) v) xs
 ===    {- repl 之定義,兩次 -}
      Bin  (Bin  (repl t (take n1 (take (n1+n2) xs)))
                 (repl u (drop n1 (take (n1+n2) xs))))
           (repl v (drop (n1+n2) xs))
 ===    {- 習題 2.39 -- 2.41 -}
      Bin  (Bin  (repl t (take n1 xs))
                 (repl u (take n2 (drop n1 xs))))
           (repl v (drop n2 (drop n1 xs)))  

演算到此,與 t 有關的是 repl t, take (size t), 與 drop (size t) 三項; 與 u 有關的是 repl u, take (size u), 與 drop (size u) 三項。 如果我們把 repl t, take (size t), 與 drop (size t) 取出,當作一個函數之內完成的動作:

repTail :: ETree a -> List b -> (ETree b × List b)
repTail s xs = (repl s (take n xs), drop n xs) 
  where n = size s 

那麼 Bin (repl t (take n1 xs)) (repl u (take n2 (drop n1 xs))) 似乎有可能收回成為這樣的式子:xs 先被丟給 repTail t,將 t 標記好,並得到剩下的串列 drop n1 xs。這個剩下的串列又可以丟給 repTail u, 兩者都只把 xs 走過一次。 我們試著導出 repTail 的歸納定義。 基底狀況 s := Tip y 比較容易,我們考慮 s := Bin t u 的情況, 並演算如下(令 n1 = size t,n2 = size u, 因此 size (Bin t u)= n1 + n2):

      repTail (Bin t u) xs
 ===   {- repTail 之定義 -}
      (repl (Bin t u) (take (n1 + n2) xs), drop (n1 + n2) xs)
 ===   {- repl 之定義,令 n1 = size t -}
      (Bin  (repl t (take n1 (take (n1 + n2) xs)))
            (repl u (drop n1 (take (n1 + n2) xs))), drop (n1 + n2) xs)
 ===   {- 習題 2.39 -- 2.41 -}
      (Bin  (repl t (take n1 xs))
            (repl u (take n2 (drop n1 xs))), drop n2 (drop n1 xs))
 ===   {- 提出共同項 -}
      let  (t', xs')   = (repl t (take n1 xs),  drop n1 xs)
           (u', xs'')  = (repl u (take n2 xs'), drop n2 xs')
      in (Bin t' u', xs'')
 ===   {- repTail 之定義 -}
      let  (t', xs')   = repTail t xs
           (u', xs'')  = repTail u xs'
      in (Bin t' u', xs'') 

因此我們得到:

repTail (Tip _)    xs =  (Tip (head xs), tail xs)
repTail (Bin t u)  xs =  let  (t', xs')   = repTail t xs
                              (u', xs'')  = repTail u xs'
                         in (Bin t' u', xs'') 

確實如同所預期的,串列 xs 被 repTail t 使用,得到標籤過的新樹 t', 和剩下的串列 xs'. 後者再被 repTail u 用來給 u 上標籤。最後我們得傳回剩下的串列 xs''. 實際上把串列變短的動作發生在基底狀況 repTail (Tip _) 中。串列中的每個元素只會在每次遇見 Tip 時被取出一次,因此這是一個線性時間的演算法。

\todo{repsort t = rep t (sort (leaves t [])).}

Burstall and Darlington [1977]

練習 5.14

下述函數 ascending :: List Int -> Bool 判斷一個串列是否由左到右遞增:

ascending :: List Int -> Bool
ascending []      = True
ascending (x:xs)  = x <= minimum xs ⋀ ascending xs 

當輸入串列長度為 n, 這個函數需要 $O(n^2)$ 個基本運算。請用組對的方式將之減少至 $O(n)$.

答案

考慮如下的定義:

ascMin :: List Int -> (Bool × Int)
ascMin = fork ascending minimum 

如果 ascMin 有更快的實作,我們可定義 ascending = fst . ascMin.

當輸入為 [], 我們有 ascMin [] = (True, maxBound). 考慮當輸入為 x:xs 的情況:

      ascMin (x:xs)
 ===   {- ascMin 之定義 -}
      (ascending (x:xs), minimum (x:xs))
 ===   {- ascending 與 minimum 之定義 -}
      (x <= minimum xs ⋀ ascending xs, x ↓ minimum xs)
 ===   {- 引入區域變數 -}
      let (b, y) = (ascending xs, minimum xs)
      in (x <= y ⋀ b, x ↓ y)
 ===   {- ascMin 之定義 -}
      let (b, y) = ascMin xs
      in (x <= y ⋀ b, x ↓ y) 

如此,我們已導出:

ascMin :: List Int -> (Bool, Int)
ascMin []      = (True, maxBound)
ascMin (x:xs)  =  let (b, y) = ascMin xs
                  in (x <= y ⋀ b, x ↓ y) 
練習 5.15

回顧第 1.10 節中談到的 ITree:

data ITree a = Null | Node a (ITree a) (ITree a) 

猴麵包樹(baobab),又稱猢猻木,是一種樹幹相當粗的樹。 猴麵包樹原產於馬達加斯加、非洲等地,也被寫進了《小王子》之中。 如果一個 ITree Int 的每個標籤都大於其兩個子樹的標籤總和,我們便說它是一棵猴麵包樹。 以下的函數判定一棵樹是否為猴麵包樹(其中 sumT :: ITree Int -> Int 計算一個樹中所有標籤的總和):

baobab :: ITree Int -> Bool
baobab Null          =  True
baobab (Node x t u)  =  baobab t ⋀ baobab u ⋀
                          x > (sumT t + sumT u) 

因反覆呼叫 sumT, 當樹的大小為 n 時,baobab 的執行時間為 $O(n^2)$. 請使用組對的技巧,在 $O(n)$ 的時間內算出 baobab.

答案

考慮如下的定義:

baosum :: Tree Int -> (Bool, Int)
baosum = fork baobab sumT 

如果 baosum 有時間效率為 $O(n)$ 的定義,我們可重定義 baobab = fst . baosum. 當 t := Null, 我們有 baosum Null = (True, 0). 考慮 t := Node x t u:

     baosum (Node x t u)
 ===    {- baosum 之定義 -}
     (baobab (Node x t u), sumT (Node x t u))
 ===    {- baobab 與 sumT 之定義 -}
     (  baobab t ⋀ baobab u ⋀ x > (sumT t + sumT u),
        x + sumT t + sumT u)
 ===    {- 引入區域變數 -}
     let  (b,y) = (baobab t, sumT t)
          (c,z) = (baobab u, sumT u)
     in (b ⋀ c ⋀ x > (y + z), x + y + z)
 ===    {- baosum 之定義 -}
     let  (b,y) = baosum t
          (c,z) = baosum u
     in (b ⋀ c ⋀ x > (y + z), x + y + z) 

如此,我們已經導出:

baosum Null          = (True, 0)
baosum (Node x t u)  =
  let  (b,y) = baosum t
       (c,z) = baosum u
  in (b ⋀ c ⋀ x > (y + z), x + y + z) 
練習 5.16

本題出自Hu et al. [1997]。 函數 depth 定義一棵 ETree 的深度。 Tip 的深度為零,Bin 的深度則為兩子樹中較深者的深度加一:

depth :: ETree a -> Nat
depth (Tip _)    = Zero
depth (Bin t u)  = Suc (depth t ↑ depth u) 

下列函數 deepest 則傳回一棵樹中最深的標籤:

deepest :: ETree a -> List a
deepest (Tip x)    = [x]
deepest (Bin t u)  | m <  n  = deepest u
                   | m == n  = deepest t ++ deepest u
                   | m >  n  = deepest t
    where (m,n) = (depth t, depth u) 

請用組對的技巧,避免重複計算 depth. 注意: 完成的程式中,(++) 仍可能需要 $O(n^2)$ 的時間。 我們將在習題5.31 處理這個問題。

答案

定義:

dd :: ETree a -> (List a, Nat)
dd = fork deepest depth 

顯然 dd (Tip x) = ([x], 0). 以下我們考慮歸納情況時,用一個非標準的語法同時處理守衛算式的三個式子:

      dd (Bin t u)
 ===   {- dd, deepest, 與 depth 之定義 -}
      (  ( m <  n  -> deepest u
         | m == n  -> deepest t ++ deepest u
         | m >  n  -> deepest t), 1 + (m ↑ n))
      where (m,n) = (depth t, depth u)
 ===   {- 取出 deepest t 與 deepest u -}
      (  ( m <  n  -> ys
         | m == n  -> xs ++ ys
         | m >  n  -> xs), 1 + (m ↑ n))
      where ((xs,m),(ys,n)) = ((deepest t,depth t), (deepest u, depth u))
 ===   {- dd 之定義,函數分配進條件判斷 -}
      ( m <  n  -> (ys, 1 + n)
      | m == n  -> (xs ++ ys, 1 + n)
      | m >  n  -> (xs, 1 + m))
      where ((xs,m),(ys,n)) = (dd t, dd u) 

因此我們得到:

dd (Tip x)    = ([x],0)
dd (Bin t u)  | m <  n  = (ys, 1 + n)
              | m == n  = (xs ++ ys, 1 + n)
              | m >  n  = (xs, 1 + m) 
  where ((xs,m),(ys,n)) = (dd t, dd u) 
練習 5.17

第 3.2 節中的函數 balanced :: RBTree -> Bool 檢查一棵紅黑樹是否平衡。由於重複呼叫 bheight, 這是一個需要 $O(n^2)$ 時間的函數。請用組對的技巧推導出一個可在線性時間內判斷平衡的版本。

答案

定義:

balHeight :: RBTree -> (Bool, Nat)
balHeight = fork balanced bheight 

我們有 balanced = fst . balHeight. 顯然 balHeight E = (True, 0). 考慮 B t x u 的狀況:

  balHeight (B t x u)
=   {- balHeight 之定義 -}
  (balanced (B t x u), bheight (B t x u))
=   {- balanced 與 bheight 之定義 -}
  (bheight t == bheight u ⋀ balanced t ⋀ balanced u,
   1 + (bheight t ↑ bheight u))
=   {- 將 balanced 與 bheight 的呼叫取出 -}
  let  (bt,  ht)  = (balanced t, bheight t)
       (bu,  hu)  = (balanced u, bheight u)
  in   (ht == hu ⋀ bt ⋀ bu, 1 + (ht ↑ hu))
=   {- balHeight 之定義 -}
  let  (bt,  ht)  = balHeight t
       (bu,  hu)  = balHeight u
  in   (ht == hu ⋀ bt ⋀ bu, 1 + (ht ↑ hu)) 

當輸入為 R t x u 的情況亦雷同。我們可推導出:

balHeight :: RBTree -> (Bool, Nat)
balHeight E          =  (True, 0)
balHeight (R t x u)  =  let  (bt,  ht)  = balHeight t
                             (bu,  hu)  = balHeight u
                        in   (ht == hu ⋀ bt ⋀ bu, (ht ↑ hu))
balHeight (B t x u)  =  let  (bt,  ht)  = balHeight t
                             (bu,  hu)  = balHeight u
                        in   (ht == hu ⋀ bt ⋀ bu, 1 + (ht ↑ hu)) 

5.5.3 代換為最小標籤 --- 循環程式

下列函數 minE 曾出現在第 2.8 節中,找出一棵 ETree 中最小的值。 函數 rep 則可視為 repl 的簡單版,將樹中的每個標籤都代換成同一個值 y。

minE :: ETree Int -> Int
minE (Tip x)    = x
minE (Bin t u)  = minE t ↓ minE u 
rep :: b -> ETree a -> ETree b
rep y (Tip _)   = Tip y
rep y (Bin t u) = Bin (rep y t) (rep y u) 

給一棵樹 t, 我們要把 t 之中的每個標籤都代換成 t 的最小標籤。 直觀的做法是寫成 let m = minE t in rep t m. 如此一來,t 會被走訪兩次,第一次被minE 走訪以計算 m, 第二次由 rep 進行代換。 Bird [1984] 提出挑戰:有可能在只把 t 走訪一次的情況下,完成上述工作嗎?

以下函數 repmin 同時傳回代換過後的樹,以及原樹中的最小標籤:

repmin :: ETree Int -> a -> (ETree a × Int)
repmin y = fork (rep y) minE 

使用本節的技巧,讀者們應該已經可以為 repmin 導出如下的歸納定義:

repmin y (Tip x)    =  (Tip y, x)
repmin y (Bin t u)  =  let  (t', m) = repmin y t
                            (u', n) = repmin y u
                       in (Bin t' u', m ↓ n) 

該定義只將 t 走訪一次。然後我們定義:

transform :: ETree Int -> ETree Int
transform t =  let (t', m) = repmin m t in t' 

函數 transform 用 repmin 算出 t 的最小標籤 m, 同時又用 m 來標記 t... 於是,似乎確實用一次走訪就完成了兩件事!這是怎麼做到的呢?

函數 transform 有個特殊之處:變數 m 既是 repmin 的傳回值,又是其參數。 這是一個循環程式(circular program)。 這樣的程式之所以能正常終止,有賴於 Haskell 的範式順序/惰性求值(見第頁)。實際上發生的事情如此:假設輸入為

t = Bin  (Bin (Tip 4) (Tip 2))
         (Bin (Bin (Tip 3) (Tip 1)) (Tip 5))

repmin 將輸入 t 走訪一遍,邊走邊建立了一個未算出的算式 (4 ↓ 2) ↓ ((3 ↓ 1) ↓ 5). 該算式就是 m 的值,其實也可視作一棵樹,其結構和 t 一樣,只是把每個 Bin 代換成 min. 函數 repmin 的另一項工作是新建一棵樹 t',該樹之中每個 Tip 的標籤都指到這個算式。 根據範式順序求值,這個算式還不用立刻被算出來。直到我們終於不得不算出它,例如當 t' 被傳回,我們要求電腦把 t' 印出來,或著有別的函數需檢查 t' 中的標籤時,該算式才被歸約成一個數字 --- 這需要把該算式走訪一遍。 (但,根據惰性求值,一但 m 被算成一個數字,下次使用 m 時就不再需要反覆計算了。)

需注意,雖然「t只被走訪一次」確實成立,這並不表示 transform 必然比老實將樹走訪兩次的程式快 --- 效率是個複雜的問題,本章將陸續談到更多。我的建議是:循環程式應視為有趣、優雅的謎題,而不是以效率為目的的程式設計技巧。

5.5.4 小結與提醒

「組對」的技巧讓函數多傳回一些值。我們可能藉此省下一些重複的計算,增進效率。

我們自然想問:給一個有重複計算、待改進的函數 f, 怎知道該讓它多傳回什麼值? 在本節的例子中,我們可由符號演算看出一些端倪: 將 f 的定義展開,辨識出被重複計算的子算式,這些子算式就可能用來與原函數組對。 但廣泛說來,「將一個函數或性質通用化」是編程與證明中最困難、最需要經驗、智慧的一步。 只要找到正確的通用化,例如 steepsum 或 repTail, 剩下的推導都可相當機械化地進行。 唯有「通用化」這一步,我們無法保證有任何機械化、公式化的方法可作為解決所有問題的萬靈丹 --- 否則編程就是一件可完全自動化的事情了。

雖然如此,我們仍希望基於符號演算的形式方法能給我們一定程度的幫助與指引。 程式語言研究的目標之一便是分辨出編程的過程中,哪些部分是瑣碎、機械化的,哪些部分是真正需要靈感與智慧的,並且盡量使用符號幫助,使我們在進行思考時有更多工具。

組對可用於減少走訪資料結構的次數,但這麼做並不見得有效率上的好處。 例如,以下函數計算一個串列中元素的平均值:

average xs = sum xs / length xs 

利用組對,我們可以另定義一個函數 sumlen = fork sum length, 並推導其歸納定義,在一次走訪中同時計算串列的和與長度:

sumlen []      =  (0,0)
sumlen (x:xs)  =  let (s,l) = sumlen xs
                  in (x + s, 1 + l) 

然後平均便可定義成 average' xs = let (s,l) = sumlen xs in s/l.

然而,根據Hu et al. [1997],average' 通常比 average 慢。 兩者都是 $O(n)$ 的演算法。 函數 sumlen 在傳回值時會產生一個序對,該序對立刻被上層拆掉。 因此 average' 每處理一個元素耗費的時間較多,往往不如乾脆將 xs 走訪兩次。 Hu et al. [1997] 認為需有更有效率的序對實作法,組對才是值得做的轉換。

練習 5.18

函數 allpairs 傳回輸入串列中任兩個元素(依其原本順序)形成的序對。 例如 allpairs [1,2,3,4] 可得到 [(1,2),(1,3),(1,4),(2,3),(2,4),(3,4)]。

allpairs :: List a -> List (a × a)
allpairs []      = []
allpairs (x:xs)  = map (\y -> (x,y)) xs ++ allpairs xs 

而 maxdiff 則計算一個串列中任兩元素前者與後者的最大差:

maxdiff :: List Int -> Int
maxdiff = maximum . map (\(x,y) -> x - y) . allpairs 

當輸入串列長度為 n, 如此定義的 maxdiff 是一個需時 $O(n^2)$ 的演算法。 定義:

 mdm xs = (maxdiff xs, ???) 

找出 ??? 可能的值,使得 mdm 能在 $O(n)$ 時間之內完成計算。 你可假設以下性質:

  & maximum (map (x-) xs) = x - minimum xs     (5.2 )

並假設 maximum 與 minimum 在空串列上的值分別為 -infty 與 infty.

答案

由 ([RefUndefined]) 我們推測:

mdm :: List Int -> (Int × Int)
mdm xs = (maxdiff xs, minimum xs) 

我們試圖找出 mdm 的歸納定義。顯然 mdm [] = (-infty, infty). 考慮歸納情況(令 minus (x,y) = x-y):

      mdm (x:xs)
 ===    {- mdm, maxdiff, 與 minimum 之定義 -}
      (maximum (map minus (allpairs (x:xs))), x ↓ minimum xs)
 ===  (  maximum (map minus (map (\y -> (x,y)) xs ++ allpairs xs)),
         x ↓ minimum xs) 

集中焦點在序對的第一個元素:

      maximum (map minus (map (\y -> (x,y)) xs ++ allpairs xs))
 ===     {- 因 map f (xs ++ ys) = map f xs ++ map f ys (習題 2.11) -}
      maximum (  map minus (map (\y -> (x,y)) xs) ++
                 map minus (allpairs xs))
 ===     {- map-fusion -}
      maximum (map (x-) xs ++ map minus (allpairs xs))
 ===     {- 因 maximum (xs ++ ys) = maximum xs ↑ maximum ys -}
      maximum (map (x-) xs) ↑ maximum (map minus (allpairs xs))
 ===     {- 因 \eqref{eq:max-minus} -}
      (x - minimum xs) ↑ maximum (map minus (allpairs xs))
 ===     {- maxdiff 之定義 -}
      (x - minimum xs) ↑ maxdiff xs 

回到推導主體:

      mdm (x:xs)
 ===    {- 上述計算 -}
      ((x - minimum xs) ↑ maxdiff xs , x ↓ minimum xs)
 ===    {- 使用 let -}
      let (y, z) = (maxdiff xs, minimum xs)
      in ((x - z) ↑ y, x ↓ z)
 ===    {- mdm 之定義 -}
      let (y, z) = mdm xs
      in ((x - z) ↑ y, x ↓ z)  

於是我們得知:

mdm []      =  (minBound, maxBound)
mdm (x:xs)  =  let (y, z) = mdm xs
               in ((x - z) ↑ y, x ↓ z)