Haskell/圖約簡

Haskell 效能

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

備註和待辦事項

待辦事項：將惰性中的惰性求值解釋融入到這個框架中。
待辦事項：更好的章節名稱。
待辦事項：思考圖的圖形表示。
- 沒有圖形表示，用 let .. in 來做。優點：約簡在這種情況下最容易執行。缺點：沒有圖形。
- ASCII 藝術/線形藝術類似於 Bird&Wadler 中的？優點：只顯示相關部分，真正地作為圖形，在紙上很容易執行。缺點：難看，不能用它來表示大型圖形。
- 帶有 @-節點的完整圖形？優點：看起來像圖形。缺點：沒有人需要知道 @-節點才能理解圖約簡。可以在實現部分解釋。
- 沒有 @-節點的圖形。優點：易於理解。缺點：柯里化怎麼辦？
！保持本章簡短。讀者越快學會如何手動評估 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                    (*)

這被稱為最外層規約，它總是規約最外層重寫子，而最外層重寫子不在另一個重寫子中。這裡，最外層規約比最內層規約使用更少的規約步驟。為什麼？因為函式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 演算（所有函數語言程式設計語言的根源）中，所有資料結構都表示為函式。

練習！還是不？差分列表最好用foldl (++)完成，但這需要了解摺疊的例子。哦，我們到底在哪裡介紹了 foldl VS. foldr 的例子？嗯，Bird & Wadler 在“控制規約順序和空間需求”的最後偷偷加了一個額外的部分“再次遇到摺疊”來處理 (++) 的例子 :-/ (++) 的複雜度在論證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 提煉"，"完全惰性"。編譯器不應該執行完全惰性。

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

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 (:) [] 與 foldl (flip (:)) [] 結合 ⊥ 使用。
只用 ⊥ 就可以分析 head . mergesort 嗎？無論如何，這個例子太複雜了，應該屬於 Haskell/Laziness。

持久化 & 均攤

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

持久化 = 不進行就地更新，舊版本仍然存在。均攤 = 將不均勻的執行時間分配到一系列操作中。在嚴格環境中，兩者無法很好地協同工作。惰性評估可以協調兩者。借貸不變式。示例：以二進位制表示形式遞增數字。

圖歸約的實現

簡要介紹 G-機器等。主要定義

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

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

請注意，這些術語是實現方面的專業術語，惰性評估可以在沒有它們的情況下很好地執行。不要在上面的任何部分使用它們。

註釋

↑ Maraist, John; Odersky, Martin; Wadler, Philip (1998年5月). "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 效能

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

編輯本章

Haskell

Haskell 基礎 >> 基礎 Haskell >> 進階 Haskell >> 單子
 高階 Haskell >> 型別玩轉 >> 擴充套件理論 >> Haskell 效能

庫參考 >> 通用實踐 >> 專業任務

編輯書籍結構

[1] Maraist, John; Odersky, Martin; Wadler, Philip (1998年5月). "The call-by-need lambda calculus". Journal of Functional Programming. 8 (3): 257–317.