Haskell/圖約簡

Haskell 效能

介紹
逐步示例
圖約簡
惰性
時間和空間分析
嚴格性
演算法複雜度
資料結構
 並行

筆記和待辦事項

待辦事項：將惰性中的惰性求值解釋融入這個模型。
待辦事項：更好的章節名稱。
待辦事項：思考圖形的圖形表示。
- 沒有圖形表示，用 let .. in 來做。優點：約簡以這種方式最容易執行。缺點：沒有圖形。
- 類似於 Bird&Wadler 中的 ASCII 藝術 / 線形藝術？優點：僅顯示相關部分，真正地作為圖形，易於在紙上執行。缺點：難看，不能用它來表示大型圖形。
- 帶有 @-節點的完整圖形？優點：看起來像圖形。缺點：沒有人需要知道 @-節點來理解圖約簡。可以在實現部分解釋。
- 沒有 @-節點的圖形。優點：易於理解。缺點：函數語言程式設計中的柯里化怎麼辦？
！保持本章簡短。讀者越快知道如何手動評估 Haskell 程式，越好。
前面的章節緊隨 Bird&Wadler

介紹

程式設計不僅是關於編寫正確的程式，由語義學回答，也是關於編寫快速且佔用少量記憶體的程式。為此，我們需要了解它們在機器上的執行方式，通常由操作語義給出。本章解釋了 Haskell 程式如何在真實的計算機上執行，因此為分析 Haskell 程式的時間和空間使用提供基礎。請注意，Haskell 標準故意不給出操作語義，實現可以自由選擇自己的語義。但到目前為止，每個 Haskell 實現或多或少地遵循惰性求值的執行模型。

在下文中，我們將詳細介紹惰性求值，並隨後使用此執行模型來解釋和舉例說明關於 Haskell 程式的時間和記憶體複雜度的推理。

透過惰性求值評估表示式

約簡

執行函式式程式，即評估表示式，意味著重複應用函式定義，直到所有函式應用都被展開。以表示式 pythagoras 3 4 和定義為例

      square x = x * x
pythagoras x y = square x + square y

一組可能的約簡序列是

pythagoras 3 4
 ⇒ square 3 + square 4   (pythagoras)
 ⇒    (3*3) + square 4   (square)
 ⇒        9 + square 4   (*)
 ⇒        9 + (4*4)      (square)
 ⇒        9 + 16         (*)
 ⇒          25

每個約簡都用一個等效的表示式替換一個子表示式，稱為可約簡表示式或簡稱redex，無論是透過呼叫函式定義（如 square）還是使用內建函式（如 (+)）。沒有 redex 的表示式被稱為正規形式。當然，一旦達到正規形式，執行就會停止，因此正規形式是計算的結果。

顯然，執行的約簡越少，程式執行速度越快。我們不能期望每個約簡步驟都花費相同的時間，因為其在真實硬體上的實現看起來非常不同，但在漸進複雜度方面，這個約簡數是一個準確的度量。

約簡策略

有很多可能的約簡序列，約簡的次數可能取決於約簡執行的順序。以表示式 fst (square 3, square 4) 為例。一種系統性的可能性是在應用函式定義之前評估所有函式引數

fst (square 3, square 4)
 ⇒ fst (3*3, square 4)   (square)
 ⇒ fst ( 9 , square 4)   (*)
 ⇒ fst ( 9 , 4*4)        (square)
 ⇒ fst ( 9 , 16 )        (*)
 ⇒ 9                     (fst)

這被稱為最內約簡策略，最內 redex 是一個沒有其他 redex 作為其內部子表示式的 redex。

另一種系統性的可能性是首先應用所有函式定義，然後才評估引數

fst (square 3, square 4)
 ⇒  square 3             (fst)
 ⇒  3*3                  (square)
 ⇒  9                    (*)

它被稱為最外約簡，總是約簡最外 redex，這些 redex 不在其他 redex 內部。這裡，最外約簡使用的約簡步驟比最內約簡少。為什麼？因為函式 fst 不需要對的第二個分量，而約簡 square 4 是多餘的。

終止

對於一些表示式，如

loop = 1 + loop

可能沒有約簡序列終止，程式執行進入無限迴圈，這些表示式沒有正規形式。但也有一些表示式，其中一些約簡序列終止，而另一些沒有終止，例如

fst (42, loop)
 ⇒  42                   (fst)

fst (42, loop)
 ⇒  fst (42,1+loop)      (loop)
 ⇒  fst (42,1+(1+loop))  (loop)
 ⇒  ...

第一個歸約序列是最外層歸約，第二個是最內層歸約，它試圖徒勞地評估loop，即使它會被fst忽略。只有在需要時才評估函式引數的能力是使最外層歸約在終止方面成為最佳選擇的原因。

定理（Church Rosser II）: 如果存在一個終止歸約，那麼最外層歸約也會終止。

圖歸約（歸約+共享）

儘管能夠丟棄引數，但最外層歸約並不總是比最內層歸約需要更少的歸約步驟。

square (1+2)
 ⇒  (1+2)*(1+2)          (square)
 ⇒  (1+2)*3              (+)
 ⇒      3*3              (+)
 ⇒       9               (*)

這裡，引數(1+2)被複制，並隨後被歸約兩次。但由於它是一個相同的引數，因此解決方案是將歸約(1+2) ⇒ 3與該引數的所有其他化身共享。這可以透過將表示式表示為圖來實現。例如，

 __________
|   |     ↓
◊ * ◊     (1+2)

表示表示式(1+2)*(1+2)。現在，square (1+2)的最外層圖歸約按如下方式進行

square (1+2)
 ⇒  __________           (square)
    |   |     ↓
    ◊ * ◊     (1+2)
 ⇒  __________           (+)
    |   |     ↓
    ◊ * ◊      3

 ⇒ 9                     (*)

並且工作已經共享。換句話說，最外層圖歸約現在最多隻歸約每個引數一次。出於這個原因，它總是比最內層歸約需要更少的歸約步驟，我們將在討論時間時證明這一點。

表示式共享也透過let和where結構引入。例如，考慮海倫公式，它用於計算邊長為a、b和c的三角形的面積

area a b c = let s = (a+b+c)/2 in
     sqrt (s*(s-a)*(s-b)*(s-c))

將其例項化為等邊三角形將歸約為

area 1 1 1
 ⇒        _____________________             (area)
          |  |    |     |      ↓
    sqrt (◊*(◊-a)*(◊-b)*(◊-c))  ((1+1+1)/2)
 ⇒        _____________________             (+),(+),(/)
          |  |    |     |      ↓
    sqrt (◊*(◊-a)*(◊-b)*(◊-c))  1.5
 ⇒
    ...
 ⇒
    0.433012702

即 ${\sqrt {3}}/4$ 。換句話說，let繫結只是為圖中的節點賦予名稱。事實上，可以完全放棄圖形符號，只依賴let來標記共享並表達圖結構。^[1]

任何 Haskell 的實現都以某種形式基於最外層圖歸約，因此它為推理時間和記憶體分配的漸近複雜性提供了良好的模型。達到正規化所需的歸約步驟數對應於執行時間，圖中項的大小對應於使用的記憶體。

練習

使用最內層和最外層圖歸約將square (square 3)歸約為正規化。
考慮快速冪演算法
```
power x 0 = 1
power x n = x' * x' * (if n `mod` 2 == 0 then 1 else x)
  where x' = power x (n `div` 2)
```
它將x計算到n次冪。使用最內層和最外層圖歸約將power 2 5歸約。執行了多少次歸約？一般power 2 n的漸近時間複雜度是多少？如果我們使用“無圖”的最外層歸約，演算法會發生什麼？

模式匹配

到目前為止，我們對最外層圖歸約的描述在模式匹配和資料建構函式方面仍然存在不足。解釋這些要點將使讀者能夠追蹤大多數歸約策略的情況，而這種策略通常是實現非嚴格函式式語言（如 Haskell）的基礎。它被稱為按需呼叫或惰性求值，這是為了暗示它“惰性地”將函式引數的歸約推遲到最後一刻。當然，其餘細節將在後續章節中介紹。

為了瞭解模式匹配如何需要規範，例如考慮布林析取

 or True  y = True
 or False y = y

以及表示式

 or (1==1) loop

其中loop = not loop是非終止的。以下歸約序列

or (1==1) loop
 ⇒ or (1==1) (not loop)        (loop)
 ⇒ or (1==1) (not (not loop))  (loop)
 ⇒ ...

只歸約最外層可歸約項，因此是最外層歸約。但

or (1==1) loop
 ⇒ or True   loop              (or)
 ⇒ True

更有意義。當然，我們只希望應用or的定義，並且只歸約引數來決定選擇哪個方程。以下 Haskell 模式匹配規則捕捉了這種意圖

左手邊自上而下匹配
當匹配左手邊時，引數自左至右匹配
只評估引數以決定它們是否匹配。

因此，對於我們的示例or (1==1) loop，我們必須將第一個引數歸約為True或False，然後評估第二個引數以匹配變數y模式，然後展開匹配的函式定義。由於與變數的匹配總是成功的，因此第二個引數根本不會被歸約。這是上面第二個歸約部分再現了這種行為。

有了這些準備，讀者現在應該能夠評估大多數 Haskell 表示式。以下是一些隨機遇到的測試這種能力的示例

練習

使用惰性求值將以下表達式歸約為正規化。假設來自 Prelude 的標準函式定義。

```
length [42,42+1,42-1]
```
```
head (map (2*) [1,2,3])
```

head $ [1,2,3] ++ (let loop = tail loop in loop)

```
zip [1..3] (iterate (+1) 0)
```

head $ concatMap (\x -> [x,x+1]) [1,2,3]

take (42-6*7) $ map square [2718..3146]

高階函式

剩下需要澄清的一點是高階函式和柯里化的歸約。例如，考慮以下定義

 id x = x
 a = id (+1) 41

 twice f = f . f
 b = twice (+1) (13*3)

其中id和twice都只用一個引數定義。解決方案是將多個引數視為對一個引數的後續應用，這被稱為柯里化

 a = (id    (+1)) 41
 b = (twice (+1)) (13*3)

為了歸約任意應用expression₁ expression₂，按需呼叫首先歸約expression₁，直到它變成一個函式，其定義可以使用引數expression₂展開。因此，歸約序列為

a
 ⇒ (id (+1)) 41          (a)
 ⇒ (+1) 41               (id)
 ⇒ 42                    (+)

b
 ⇒ (twice (+1)) (13*3)   (b)
 ⇒ ((+1).(+1) ) (13*3)   (twice)
 ⇒ (+1) ((+1) (13*3))    (.)
 ⇒ (+1) ((+1)  39)       (*)
 ⇒ (+1) 40               (+)
 ⇒ 41                    (+)

誠然，這個描述有點含糊，下一節將詳細說明一種清晰地表達它的方法。

雖然模式匹配似乎是時間密集型計算的主力軍，而高階函式只用於捕捉演算法的本質，但函式確實可以用作資料結構。一個例子是差分列表 ([a] -> [a])，它允許在 $O(1)$ 時間內進行串聯，另一個例子是透過摺疊表示流。事實上，所有資料結構都用純 lambda 演算表示，而純 lambda 演算是所有函數語言程式設計語言的根源。

練習！還是不練習？差分列表最好使用foldl (++)完成，但這需要了解 fold 示例。哦，我們到底在哪裡介紹 foldl VS. foldr 示例？嗯，Bird&Wadler 在“控制歸約順序和空間需求”的結尾偷偷地插入了一個額外的部分“再次遇到 fold”，用於 (++) 示例 :-/ 當論證reverse時，解釋了 (++) 的複雜性。

弱頭正規化

為了精確地闡述惰性求值如何選擇其歸約序列，最好放棄等式函式定義，並用表示式導向的方法替換它。換句話說，我們的目標是將像f (x:xs) = ...這樣的函式定義轉換為f = expression的形式。這可以使用兩個原語來完成，即 case 表示式和 lambda 提取。

在它們的原始形式中，case 表示式只允許對最外層建構函式進行區分。例如，列表的原始 case 表示式具有以下形式

case expression of
  []   -> ...
  x:xs -> ...

lambda 提取是一個引數的函式，因此以下兩個定義是等效的

f x = expression
f   = \x -> expression

以下是將zip的定義

 zip :: [a] -> [a] -> [(a,a)]
 zip []      ys      = []
 zip xs      []      = []
 zip (x:xs') (y:ys') = (x,y):zip xs' ys'

轉換為 case 表示式和 lambda 提取

 zip = \xs -> \ys ->
    case xs of
       []    -> []
       x:xs' ->
          case ys of
             []    -> []
             y:ys' -> (x,y):zip xs' ys'

假設所有定義都已轉換為這些原語，那麼現在每個可歸約項都具有以下兩種形式之一

函式應用 (\variable->expression₁) expression₂
或 case 表示式case expression of { ... }

惰性求值.

弱頭正規化: 如果表示式是以下之一，那麼它處於弱頭正規化，

一個建構函式（可能應用於引數），例如True、Just (square 42)或(:) 1
一個應用於過少引數（可能沒有引數）的內建函式，例如(+) 2或sqrt。
或一個 lambda 提取\x -> expression。

函式型別無論如何都無法進行模式匹配，但狡猾的 seq 仍然可以將它們評估為 WHNF。“弱”= 在 lambda 下不進行歸約。“頭”= 首先進行函式應用，然後進行引數應用。

嚴格和非嚴格函式

非嚴格函式不需要其引數。嚴格函式需要其引數處於 WHNF，只要我們不區分非終止的不同形式（例如，f x = loop 不需要其引數）。

控制空間

"空間"在這裡可以更好地被視覺化為圖的遍歷。既可以是資料結構，也可以是誘導的依賴關係圖。例如：Fibonacci(N) 依賴於：如果 N = 0 或 N = 1 則無；否則依賴於 Fibonacci(N-1) 和 Fibonacci(N-2)。由於 Fibonacci(N-1) 依賴於 Fibonacci(N-2)，因此誘導的圖不是樹。因此，實現技術和資料結構遍歷之間存在對應關係。

對應的實現技術	資料結構遍歷
記憶化	深度優先搜尋（將所有中間結果儲存在記憶體中）
平行計算	廣度優先搜尋（也將所有中間結果儲存在記憶體中）
共享	有向無環圖遍歷（僅在記憶體中維護“邊界”）
常規遞迴	樹遍歷（填充堆疊）
尾遞迴	列表遍歷 / 貪心搜尋（常數空間）

經典的

fibo 0 = 1
fibo 1 = 1
fibo n = fibo (n-1) + fibo (n-2)

是將樹遍歷應用於有向無環圖的糟糕情況。最佳化版本

fibo n = 
  let f a b m =
     if m = 0 then a
     if m = 1 then b
     f b (a+b) (m-1)
  in f 1 1 n

使用 DAG 遍歷。幸運的是，邊界大小是常數，因此它是一個尾遞迴演算法。

注意：本章 Haskell/Strictness 旨在詳細說明此處的內容。

注意：在這一節之前要介紹嚴格函式的概念。

現在是時候展示佔空間的 fold 示例了

foldl (+) 0 [1..10]

介紹 seq 和 $!，它們可以強制表示式為 WHNF。 => foldl'。

棘手的空間洩漏示例

(\xs -> head xs + last xs) [1..n]

(\xs -> last xs + head xs) [1..n]

由於 Haskell 中的求值順序僅由資料依賴關係決定，並且既沒有 head xs 依賴於 last xs 也不反之，兩者都可以先執行。這意味著，根據編譯器，一個版本執行在 O(1) 空間，而另一個版本執行在 O(n) 空間（一個足夠智慧的編譯器可能會將這兩個版本都最佳化到 O(1) 空間，但 GHC 9.8.2 在我的機器上沒有做到這一點——只有第二個版本執行在 O(1) 空間）。

共享和 CSE

注意：與時間段重疊。嗯，要多加一個記憶化部分嗎？

如何共享

foo x y =
  where s = expensive x -- s is not shared
foo x = \y -> s + y
  where s = expensive x -- s is shared

"Lambda-lifting"，"完全惰性"。編譯器不應該執行完全惰性。

空間和時間之間權衡的一個經典且重要的例子

sublists []      = [[]]
sublists (x:xs)  = sublists xs ++ map (x:) (sublists xs)
sublists' (x:xs) = let ys = sublists' xs in ys ++ map (x:) ys

這就是為什麼編譯器不應該將公共子表示式消除作為最佳化。 (GHC 做了嗎？)。

尾遞迴

注意：這應該放在空間部分嗎？我認為是的，它與堆疊空間有關。

Haskell 中的尾遞迴看起來不同。

關於時間推理

注意：在上限時間之前介紹嚴格性可以省去一些解釋的麻煩？

惰性求值 < 積極求值

在推理執行時間時，手動執行圖約簡來了解發生了什麼通常是不可行的。事實上，人類很難預測惰性求值採取的求值順序，追蹤積極求值的路徑要容易得多，在將引數提供給函式之前，會先將它們約簡為正規化。但是，知道惰性求值總是執行比積極求值更少的約簡步驟（展示證明！），我們可以很容易地透過假裝我們的函式被積極求值來獲得約簡次數的上限。

例子

or = foldr (||) False
isPrime n = not $ or $ map (\k -> n `mod` k == 0) [2..n-1]

=> 積極求值總是需要 n 步，惰性求值不會超過這個數字。但是它實際上會更少。

丟棄引數

對於那些無論如何都會將其引數檢查為正規化的函式，時間界限是精確的。函式需要其引數的屬性可以透過指稱語義簡潔地捕捉到

f ⊥ = ⊥

儘管如此，引數僅在 WHNF 中。運算上：非終止 -> 非終止。 (雖然這只是一個近似值，因為 f anything = ⊥ 不“需要”其引數)。非嚴格函式不需要其引數，並且積極時間界限不精確。但是，函式是否是嚴格的這一資訊在分析中已經可以被很好地利用。

isPrime n = not $ or $ (n `mod` 2 == 0) : (n `mod` 3 == 0) : ...

知道 or True ⊥ = True 就足夠了。

其他例子

foldr (:) [] vs. foldl (flip (:)) [] 以及 ⊥。
能否只用 ⊥ 分析 head . mergesort？無論如何，這個例子太複雜了，屬於 Haskell/Laziness。

永續性與攤銷

注意：最好將本節留給資料結構章節，因為上面的子節涵蓋了大多數程式設計師（不關注資料結構/攤銷）會遇到的情況。

永續性 = 不進行原地更新，舊版本仍然存在。攤銷 = 將執行時間不均分佈在一個操作序列中。兩者在嚴格環境中都不相容。惰性求值可以調和它們。借記不變式。例如：以二進位制形式遞增數字。

圖約簡的實現

關於 G-機器等的簡短說明。主要定義

閉包 = thunk = 堆上的程式碼/資料對。它們做什麼？考慮 $(\lambda x.\lambda y.x+y)2$ 。這是一個返回函式的函式，在本例中，它返回 $\lambda y.2+y$ 。但是，當你想編譯程式碼時，實際上在記憶體中執行替換並用 2 替換 $x$ 的所有出現是不可取的。所以，你返回一個閉包，它由函式程式碼 $\lambda y.x+y$ 和一個環境 $\{x=2\}$ 組成，該環境將值分配給其中出現的自由變數。

GHC（？，大多數 Haskell 實現？）完全避免使用自由變數，並使用超組合子。換句話說，它們被提供為額外的引數，並且觀察到引數過少的 lambda 表示式不需要被約簡，因為它們的 WHNF 並沒有太大區別。

請注意，這些術語是實現方面的技術術語，惰性求值在沒有這些術語的情況下也能很好地執行。請不要在以上任何章節中使用這些術語。

註釋

↑ Maraist, John; Odersky, Martin; Wadler, Philip (May 1998). "The call-by-need lambda calculus". Journal of Functional Programming. 8 (3): 257–317.

參考文獻

Bird, Richard (1998). Introduction to Functional Programming using Haskell. Prentice Hall. ISBN 0-13-484346-0.
Peyton-Jones, Simon (1987). The Implementation of Functional Programming Languages. Prentice Hall.

圖歸約

習題解答

Haskell 效能

簡介 >> 逐步示例 >> 圖歸約 >> 惰性求值 >> 時間和空間分析 >> 嚴格性 >> 演算法複雜度 >> 資料結構 >> 並行