Haskell/Fix 和遞歸
fix 函數乍看上去非常難以理解. 但是, 它有著一個有用的理論用途: 使用它來定義遞歸函數, 並引入有類型 lambda 演算.
引入 fix
編輯
首先我們來看一看 fix 的實現:
fix :: (a -> a) -> a fix f = let x = f x in x
我們很難一眼看出這個函數想實現什麼. fix f 似乎會產生一串無窮的 f 調用: f (f (f (... )))? 這時就要用到我們的老朋友, 懶惰計算了. 一般來說, 這串無窮的 f 調用若且唯若 f 是懶惰時才會收斂到某個值. 讓我們看一些例子:
例子: fix 的例子
Prelude> :m Control.Monad.Fix Prelude Control.Monad.Fix> fix (2+) *** Exception: stack overflow -- 栈溢出 Prelude Control.Monad.Fix> fix (const "hello") "hello" Prelude Control.Monad.Fix> fix (1:) [1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,...
我們首先從 Control.Monad.Fix 模塊中導入 fix (Data.Function 模塊中也有相同的定義). 然後我們來看看這些例子. 因為 fix 的內容是如此簡潔, 我們可以試著展開它:
fix (2+) = 2 + (fix (2+)) = 2 + (2 + fix (2+)) = 2 + (2 + (2 + fix (2+))) = 2 + (2 + (2 + (2 + fix (2+)))) = ...
顯然, 這個表達式永遠不會收斂至任何值. 我們來試著展開下一個例子:
fix (const "hello") = const "hello" (fix (const "hello")) = "hello"
現在情況有些不同了: 我們發現, 在展開一層 fix 調用後, 因為 const 總是忽略它的第二個參數, 計算就此結束; 換句話說, 表達式收斂了. 最後一個例子又有些不同, 但我們的方法還是差不多的:
fix (1:) = 1 : fix (1:) = 1 : (1 : fix (1:)) = 1 : (1 : (1 : fix (1:)))
雖然這看起來並不會收斂至某個值, 但是我們注意到, 當我們在 GHCi 中輸入 fix (1:) 時, GHCi 所做的僅僅是試圖將 show 應用到這個表達式上. 因此我們或許可以看看 show (fix (1:)) 是如何被求值的 (簡潔起見, 我們假定 show 並不會在列表里的元素間插入逗號).
show (fix (1:)) = "[" ++ map show (fix (1:)) ++ "]" = "[" ++ map show (1 : fix (1:)) ++ "]" = "[" ++ "1" ++ map show (fix (1:)) ++ "]" = "[" ++ "1" ++ "1" ++ map show (fix (1:)) ++ "]"
因此, 即使對表達式 map show (fix (1:)) 的計算永遠不會終止, 我們仍然能夠得到一個結果: GHCi 仍然能夠列印出字符串的開頭, "[" ++ "1" ++ "1", 並且當 map show (fix (1:)) 產生字符串的剩餘部分時將它們列印出來. 這裡懶惰計算開始起作用了: 列印函數不需要得到整個輸入後才能夠開始工作.
最後, 這是一個計算一個數平方根逼近的算法,
fix (\next guess tol val -> if abs(guess^2-val) < tol then guess else
next ((guess + val / guess) / 2.0) tol val) 2.0 0.0001 25.0
= let f next guess tol val = if abs(guess^2-val) < tol then guess else
next ((guess + val / guess) / 2.0) tol val
in fix f 2.0 0.0001 25.0
= let f ... = ...
in f (fix f) 2.0 0.0001 25.0 -- next = fix f = f (fix f) = f next ...
= 5.000000000016778
| 練習 |
|---|
|
如果以下表達式收斂的話, 它們會收斂成什麼?
|
fix 和不動點
編輯
一個函數 f 的不動點 是一個值 a 使得 f a == a. 比如說, 0 是函數 (* 3) 的不動點, 因為 0 * 3 == 0. 這也是 fix 的名字 ("固定") 的由來: 它將找到一個函數的最小不動點. (稍後我們將解釋"最小"的含義.) 我們可以注意到, 對於以上兩個收斂的例子, 我們可以看到:
const "hello" "hello" -> "hello" (1:) [1,1,..] -> [1,1,...]
而沒有一個數 x 能夠使 2+x == x 成立, 因此 fix (2+) 不收斂.
| 練習 |
|---|
對於前一個練習模塊中的所有形如 fix f 的表達式, 如果你認為其收斂的話, 驗證 fix f 確實會得出一個不動點. |
事實上, 從 fix 的定義中我們就能看出, 顯然當它收斂時我們就找到了一個不動點. 我們只需將 fix 的定義反過來:
f (fix f) = fix f
這恰恰就是不動點的定義! 因此 fix 應該總是找到一個不動點. 但有時 fix 似乎並不能找到一個不動點 (換句話說, 不能收斂). 然而我們能夠使用指稱語義修復這一個漏洞. 所有的 Haskell 類型事實上都有著一個對應的此類型的值, 稱為 bottom, 寫做 ⊥. [1] 舉個例子, 類型為 Int 的值實際上不僅僅有 1, 2, 3, 還有 ⊥. 發散的計算我們用 ⊥ 來表示, 舉個例子, fix (2+) = ⊥.
特殊值 undefined 也同樣用 ⊥ 來表示. 現在我們能夠明白 fix 是如何找到 (2+) 函數的不動點的了:
例子: (2+) 的不動點
Prelude> (2+) undefined *** Exception: Prelude.undefined
也就是說, 將 undefined (⊥) 傳遞給 (2+) 後我們仍將得回 undefined. 因此 ⊥確實是 (2+) 的一個不動點!
在 (2+) 一例中, 這就是唯一的不動點了. 然而, 存在一些函數 f, 其存在一個或多個不動點, 但是 fix f 依舊發散: fix (*3) 是發散的, 但我們能夠注意到 0 時此函數的一個不動點. 這時就需要我們之前提到的"最小"定義了. Haskell 中的類型都形成一個偏序集, 被稱為定義性 (definedness). 對於任何類型, ⊥ 都有著最小的定義性 (因此叫做 "bottom", 譯作"底部"). 對於 Int 之類的初級類型, 這個偏序集中只存在 ⊥ ≤ 1, ⊥ ≤ 2 以及之類的關係. 對於任何非 bottom 的 Int 值 m, n, 我們不定義它們之間存在關係. 對於其他的簡單類型, 譬如 Bool 和 (), 我們作同樣的規定. 對於"多層次"的類型, 比如 Maybe 和列表, 情況稍稍複雜一些, 可以參見指稱語義.
那麼, 由於 ⊥ 是任何類型的最小定義性的值, 而 fix 依據定義將返回最小定義性的不動點, 若 f ⊥ = ⊥, 則我們有 fix f = ⊥ (反之亦然). 如果你讀了上面引用的指稱語義的文章 (當然不讀也並無大礙), 你會發現這是嚴格函數的定義.[2]: fix f 離散若且唯若 f 是嚴格的.
遞歸 編輯
如果你已經見過一些 fix 的例子, 有可能它們涉及了 fix 和遞歸. 這裡我們來看一個經典的例子:
例子: 使用 fix 來表示遞歸
Prelude> let fact n = if n == 0 then 1 else n * fact (n-1) in fact 5 120 Prelude> fix (\rec n -> if n == 0 then 1 else n * rec (n-1)) 5 120
這裡我們使用了 fix 來"表示"階乘函數: 我們可以注意到 (如果我們將 fix 看做"語言的一部分") 我們的第二個階乘定義並沒有使用遞歸. 在一門例如有類型 lambda 演算(因為無法命名, 所以不能遞歸)這樣沒有遞歸的語言中, 我們可以使用 fix 來表示遞歸函數:
例子: More fix examples
Prelude> fix (\rec f l -> if null l then [] else f (head l) : rec f (tail l)) (+1) [1..3] [2,3,4] Prelude> map (fix (\rec n -> if n == 1 || n == 2 then 1 else rec (n-1) + rec (n-2))) [1..10] [1,1,2,3,5,8,13,21,34,55]
它是如何工作的? 我們先從指稱語義的角度分析一下 fact 函數. 簡潔起見, 我們定義:
fact' rec n = if n == 0 then 1 else n * rec (n-1)
這和上面的例子裡的實際上是同一個函數, 只是我們為匿名 lambda 函數命名了; 因此我們現在可以寫成 fix fact' 5 了. fix 會找到 fact' 函數的一個不動點, 換句話說, 一個使得 f == fact' f 的函數 f. 我們將這個式子展開:
f = fact' f = \n -> if n == 0 then 1 else n * f (n-1)
我們所做的僅僅是將在 fact' 的定義中將 rec 替換成 f. 但現在這個定義已經被變換成階乘函數的遞歸形式了! fix 將 fact' 作為第一個參數傳遞給它自己以用一個高階函數構造出一個遞歸的函數.
我們也可以從實際運行狀況的角度考慮. 我們把 fix fact' 的定義展開:
fix fact'
= fact' (fix fact')
= (\rec n -> if n == 0 then 1 else n * rec (n-1)) (fix fact')
= \n -> if n == 0 then 1 else n * fix fact' (n-1)
= \n -> if n == 0 then 1 else n * fact' (fix fact') (n-1)
= \n -> if n == 0 then 1
else n * (\rec n' -> if n' == 0 then 1 else n' * rec (n'-1)) (fix fact') (n-1)
= \n -> if n == 0 then 1
else n * (if n-1 == 0 then 1 else (n-1) * fix fact' (n-2))
= \n -> if n == 0 then 1
else n * (if n-1 == 0 then 1
else (n-1) * (if n-2 == 0 then 1
else (n-2) * fix fact' (n-3)))
= ...
我們可以注意到, fix 使得我們可以不停地"展開" fact': 每次我們進入 else 分支時, 我們都籍由 fix fact' = fact' (fix fact') 構造出一次對 fact'的調用, 由此進入了遞歸鏈中的下一層. 直到最終我們進入 then 分支, 達到遞歸鏈的底部.
| 練習 |
|---|
|
有類型 lambda 演算 編輯
本節我們將拓展之前提到的一點: 用 fix 在有類型 lambda 演算中如何使用 fix 表示遞歸函數. 我們假定你已經碰到過有類型 lambda 演算了. 回憶一下, 在有類型 lambda 演算中, 我們不能使用 let 或頂層綁定. 每一個程序都是簡單的 lambda 抽象, 應用和字面常量. 假設我們想寫一個 fact 函數; 假定我們有表示自然數的 Nat 類型, 這個函數大致會是這樣:
λn:Nat. if iszero n then 1 else n * <???> (n-1)
問題是, 在 <???> 處我們應該填入什麼呢? 我們不能對函數命名, 因此我們不能遞歸調用自己. 唯一一種將表達式綁定至一個名字的方法是使用一個抽象, 我們試一試:
(λf:Nat→Nat. λn:Nat. if iszero n then 1 else n * f (n-1)) (λm:Nat. if iszero m then 1 else m * <???> (m-1))
展開:
λn:Nat. if iszero n then 1
else n * (if iszero n-1 then 1 else (n-1) * <???> (n-2))
我們仍然有一個討厭的 <???>. 我們可以試著加入更多層:
(λf:Nat→Nat. λn:Nat. if iszero n then 1 else n * f (n-1)
((λg:Nat→Nat. λm:Nat. if iszero n' then 1 else n' * g (m-1))
(λp:Nat. if iszero p then 1 else p * <???> (p-1))))
->
λn:Nat. if iszero n then 1
else n * (if iszero n-1 then 1
else (n-1) * (if iszero n-2 then 1 else (n-2) * <???> (n-3)))
很明顯, 不管我們命名多少次都無法消除 <???>. 除非我們使用 fix —— 它使得我們能夠無需命名進入下一層遞歸:
fix (λf:Nat→Nat. λn:Nat. if iszero n then 1 else n * f (n-1))
這是有類型 lambda 演算中使用 fix 實現的一個完美的階乘函數.
在有類型 lambda 演算之外, fix 還有一個有趣的特性: 如果我們把它引入一門語言中, 那麼任何類型都是居留(至少有一個該類型的值)得了, 因為對於任意類型 T, 都能構造出以下類型為 T 的表達式:
fix (λx:T. x)
這個表達式, 用 Haskell 的話來說, 其實是 fix id, 指稱語義中寫作 ⊥. 因此我們發現, 只要我們將 fix 引入有類型 lambda 演算中, 並不是所有項都能規約成一個值了.
作為數據類型的 Fix 編輯
我們能夠在 Haskell 中定義一個 fix 數據類型.
有三種方式來定義這個類型.
newtype Fix f = Fix (f (Fix f))
或者使用 RankNTypes 擴展
newtype Mu f=Mu (forall a.(f a->a)->a) data Nu f=forall a.Nu a (a->f a)
Mu 和 Nu 能夠幫助我們推廣 folds, unfolds 和 refolds.
fold :: (f a -> a) -> Mu f -> a fold g (Mu f) = f g unfold :: (a -> f a) -> a -> Nu f unfold f x = Nu x f refold :: (a -> f a) -> (g a-> a) -> Mu f -> Nu g refold f g = unfold g . fold f
Mu 和 Nu 是受限的 Fix. Mu 可用來構造歸納有限值 (inductive noninfinite data), Nu 可用來構造反歸納無限值 (coinductive infinite data). 例如:
newpoint Stream a = Stream (Nu ((,) a)) -- forsome b. (b, b -> (a, b)) newpoint Void a = Void (Mu ((,) a)) -- forall b. ((a, b) -> b) -> b
和不動點函數不同, 不動點數據類型並不會得出 ⊥. 在下例中 Bot 是良定義的. 它和單位類型 () 同構.
newtype Id a = Id a newtype Bot = Bot (Fix Id) -- 相等性 newtype Bot = Bot Bot -- 只有一个合法的值. Bot $ Bot $ Bot $ Bot ..,
Fix 數據類型並不能實現所有形式的遞歸. 例如這個不規則的數據類型.
data Node a = Two a a | Three a a a data FingerTree a = U a | Up (FingerTree (Node a))
用 Fix 將它構造出來並不容易.
| Fix 和遞歸 |
| 習題解答 |
| 理論提升 |
|
指稱語義
>> Equational reasoning
>> Program derivation
>> Category theory
>> The Curry-Howard isomorphism
>> |
| Haskell |
|
Haskell基礎
>> 初級Haskell
>> Haskell進階
>> Monads
|
注 編輯
- ↑ 關於這一點, 可以參見類型居留問題和在Haskell里，每個類型都可以構造出來一個此類型的表達式嗎？中更詳細的解釋
- ↑ 遺憾的是中文維基百科詞條中並沒有提到這個定義.