fix 函數
fix 是一個在 Data.Function 子產品中定義的函數,它是對于遞歸的封裝,可以用于定義不動點函數。
fix :: (a -> a) -> a
fix f = let x = f x in x
fix 函數的定義使用了遞歸綁定,比較難以了解:
fix f
= let x = f x in x
= let x = f x in f x
= let x = f x in f (f x)
= let x = f x in f (f (f x))
= let x = f x in f (f .. (f (f x)) ..)
= let x = f x in f . f . ... . f . f $ x
即 fix 函數的實質是無限多次調用函數 f,直至函數 f 的傳回值不依賴于參數時遞歸調用終止。
Prelude Data.Function> fix (const "hello")
"hello"
Prelude Data.Function> fix (:)
[, , ...
fix (const "hello")
= let x = const "hello" x in x
= let x = "hello" in x
= "hello"
fix (1:)
= let x = 1 : x in x
= let x = 1 : x in 1 : x
= let x = 1 : x in 1 : 1 : x
= let x = 1 : x in 1 : 1 : ... 1 : x
= [1, 1, ...]
fix 函數與遞歸
借助于 fix 函數我們可以将遞歸函數改寫為非遞歸函數。
以下是計算階乘的函數的遞歸版本和使用 fix 函數的非遞歸版本。
Prelude Data.Function> factorial n = if n == then else n * factorial (n-)
Prelude Data.Function> factorial
Prelude Data.Function> factorial' = fix (\rec n -> if n == then else n * rec (n-))
Prelude Data.Function> factorial'
這裡
fix (\rec n -> if n == 0 then 1 else n * rec (n-1))
就是非遞歸版本,下面在解釋器裡檢查它的類型
Prelude Data.Function> :t (\rec n -> if n == then else n * rec (n-))
(\rec n -> if n == then else n * rec (n-))
:: (Eq p, Num p) => (p -> p) -> p -> p
Prelude Data.Function> :t fix (\rec n -> if n == then else n * rec (n-))
fix (\rec n -> if n == then else n * rec (n-))
:: (Eq p, Num p) => p -> p
類型分析:
-
的類型為(\rec n -> ...)
參數 rec 的類型為(p -> p) -> p -> p
(p -> p)
,參數 n 的類型為 p
(Eq p, Num p) 說明類型 p 是可以比較的數值類型。
- 非遞歸版本
的類型為fix (\rec n -> ...)
p -> p
- 即非遞歸版本中 fix 的類型為
((p -> p) -> p -> p) -> p -> p
- 對比 fix 函數的定義
,可知原先定義中的類型 a 被替換成了fix :: (a -> a) -> a
(p -> p)
手動計算:
fix (\rec n -> if n == 0 then 1 else n * rec (n-1)) 3
= (let x = (\rec n -> if n == 0 then 1 else n * rec (n-1)) x in x) 3
= let x = (\rec n -> if n == 0 then 1 else n * rec (n-1)) x in x 3
= let x = (\n -> if n == 0 then 1 else n * x (n-1)) in x 3
= let x = (\n -> if n == 0 then 1 else n * x (n-1)) in (\n -> if n == 0 then 1 else n * x (n-1)) 3
= let x = (\n -> if n == 0 then 1 else n * x (n-1)) in 3 * (x 2)
= let x = (\n -> if n == 0 then 1 else n * x (n-1)) in 3 * ((\n -> if n == 0 then 1 else n * x (n-1)) 2)
= let x = (\n -> if n == 0 then 1 else n * x (n-1)) in 3 * (2 * (x 1))
= let x = (\n -> if n == 0 then 1 else n * x (n-1)) in 3 * (2 * ((\n -> if n == 0 then 1 else n * x (n-1)) 1))
= let x = (\n -> if n == 0 then 1 else n * x (n-1)) in 3 * (2 * (1 * (x 0)))
= let x = (\n -> if n == 0 then 1 else n * x (n-1)) in 3 * (2 * (1 * ((\n -> if n == 0 then 1 else n * x (n-1)) 0)))
= let x = (\n -> if n == 0 then 1 else n * x (n-1)) in 3 * (2 * (1 * 1))
= let x = (\n -> if n == 0 then 1 else n * x (n-1)) in 6
= 6
通過手工計算,可以看出 rec 實質上是由 fix 函數所傳入的計算階乘的函數 factorial。
rec 的類型就是遞歸版本 factorial 的類型。
事實上,遞歸版本和使用 fix 函數的非遞歸版本是非常相似的。
-- 遞歸版本 1
factorial =
factorial n = n * factorial (n-)
-- 遞歸版本 2
factorial n = if n == then else n * factorial (n-)
-- 遞歸版本 3
factorial = \n -> if n == then else n * factorial (n-)
-- 非遞歸版本 1
factorial' = fix (\rec n -> if n == then else n * rec (n-))
-- 非遞歸版本 2
factorial' = fix factorial_ where
factorial_ rec =
factorial_ rec n = n * rec (n-)
兩相對比,不難發現隻需要履行一定的步驟就可将遞歸版本轉化為使用 fix 函數的非遞歸版本。
使用 lambda 的改寫方法:
- 如果遞歸版本 factorial 的函數定義分段進行,我們需要使用 if else 語句或者 case of 語句将所有定義式合成為一個。
- 将遞歸版本 factorial 的全部參數(這裡隻有 n)都移到函數定義式的右邊,也就是将函數定義改寫為一個lambda。
- 在這個 lambda 的所有參數(這裡隻有 n)之前添加一個 rec 參數,它的類型應該和遞歸版本 factorial 函數的類型相同。
- 将這個 lambda 中所有對于遞歸版本 factorial 函數的調用改為對 rec 的調用。
- 将這個改寫完畢的 lambda 作為參數傳給 fix 即可生成非遞歸版本 factorial’。
使用具名函數的改寫方法:
- 将遞歸版本的函數名 factorial 按照一定規則(比如加下劃線)改名為 factorial_。
- 在這個函數的所有參數(這裡隻有 n)之前添加一個 rec 參數,它的類型應該和遞歸版本 factorial 函數的類型相同。
- 将這個函數中所有對于遞歸版本 factorial 函數的調用改為對 rec 的調用。
- 将這個改寫完畢的函數 factorial_ 作為參數傳給 fix 即可生成非遞歸版本 factorial’。
- 如果需要将函數 factorial_ 合并進入非遞歸版本,可以使用 where 子句将函數 factorial_ 改為局部函數。
使用 fix 改寫遞歸函數的例子
map 函數
map :: (a -> b) -> [a] -> [b]
map [] = []
map f (x:xs) = f x : map f xs
改寫過程1(使用 lambda):
首先合成所有定義,得到
map f list =
case list of
[] -> []
(x:xs) -> f x : map f xs
将參數 f 和 list 移到右邊,得到
map = \f list ->
case list of
[] -> []
(x:xs) -> f x : map f xs
添加 rec 參數,替換 map 可得到
\rec f list ->
case list of
[] -> []
(x:xs) -> f x : rec f xs
将 lambda 傳給 fix,可得到
map2 = fix $ \rec f list ->
case list of
[] -> []
(x:xs) -> f x : rec f xs
改寫過程2(使用具名函數):
改名為 map
添加 rec 參數,替換 map 可得到
map rec [] = []
map rec f (x:xs) = f x : rec f xs
将 map 傳給 fix,可得到
map3 = fix map
使用局部函數的話,可以将兩者合并
map3 = fix map where
map rec [] = []
map rec f (x:xs) = f x : rec f xs
改寫過程3(使用 lambda):
首先合成所有定義,得到
map f list =
case list of
[] -> []
(x:xs) -> f x : map f xs
将map f 看成一個函數,隻将參數 list 移到右邊,得到
map f = \list ->
case list of
[] -> []
(x:xs) -> f x : map f xs
添加 rec 參數,替換 map f 可得到
\rec list ->
case list of
[] -> []
(x:xs) -> f x : rec xs
将 lambda 傳給 fix,可得到
map4 f = fix $ \rec list ->
case list of
[] -> []
(x:xs) -> f x : rec xs
fix 函數與不動點
f (fix f)
= f (let x = f x in x)
= let x = f x in f x
= let x = f x in f . f . ... . f . f $ x
= fix f
是以 fix 函數也可以定義為
fix f = f (fix f)
即 fix 函數的意義在于尋找函數 f 的不動點 y = fix f,使得 f y == y。
一階函數的不動點是個常數,二階以上的高階函數的不動點是低一階的函數。
在 fix 函數的定義中,等式右邊隻有對參數的引用,是以 fix 函數是一個組合子(combinator)。這也是它被定義在Data.Function 這個組合子專用子產品的原因。
在計算機科學中,fix 函數這個用來求函數 f 的不動點的組合子被稱為不動點組合子或 Y 組合子。
下面計算 y,使得 cos y == y。
遞歸版本cosFixpointExplicit
cosFixpointExplicit x =
if cos x == x
then x
else cosFixpointExplicit (cos x)
經過改寫可得到使用 fix 函數的非遞歸版本
cosFixpoint x =
fix (\f b ->
if cos b == b
then b
else f (cos b)
) x
或者
cosFixpoint2 x =
($ x) . fix $ \f b ->
if cos b == b
then b
else f (cos b)
或者
cosFixpoint3 x =
flip fix x $ \f b ->
if cos b == b
then b
else f (cos b)
*Main> cosFixpoint
.
*Main> cosFixpoint
.
*Main> cos it
.
*Main> cos it == it
True
即當 y == 0.7390851332151607 時,cos y == y。
不動點與遞歸
fix 函數将不動點和遞歸這兩者結合了起來。
下面證明上述由遞歸版本轉向使用 fix 函數的非遞歸版本的改寫過程是有效的。
factorial = \n -> if n == then else n * factorial (n-)
等價于
factorial = (\rec n -> if n == then else n * rec (n-)) factorial
也就是說 factorial 是 (\rec n -> if n == then else n * rec (n-)) 這個函數的不動點。
對比 fix 函數的定義
fix f = f (fix f)
令 f = (\rec n -> if n == then else n * rec (n-)) 可得以下等式:
factorial = fix (\rec n -> if n == then else n * rec (n-))
于是
factorial = \n -> if n == then else n * factorial (n-)
等價于
factorial = fix (\rec n -> if n == then else n * rec (n-))
由遞歸版本轉向使用 fix 函數的非遞歸版本的改寫過程的實質是:
- 通過給遞歸版本 factorial 函數添加參數 rec 形成高一階的非遞歸函數 factorial_。
- 參數 rec 實質上就是 factorial 函數自身,是以參數 rec 與 factorial 函數類型相同。
- 遞歸函數 factorial 是高一階的非遞歸函數 factorial_ 的不動點。
- 将非遞歸函數 factorial_ 作為參數傳遞給 fix 函數形成非遞歸版本 factorial’。
- 在非遞歸版本中 factorial’ 由 fix 函數帶動非遞歸函數 factorial_ 不斷進行遞歸求解。
手動計算(采用 fix函數的第二個定義
fix f = f (fix f)
):
factorial = \n -> if n == 0 then 1 else n * factorial (n-1)
factorial_ = (\rec n -> if n == 0 then 1 else n * rec (n-1))
factorial = fix factorial_
factorial 3
= fix factorial_ 3
= factorial_ (fix factorial_) 3
= (\rec n -> if n == 0 then 1 else n * rec (n-1)) (fix factorial_) 3
= if 3 == 0 then 1 else 3 * fix factorial_ 2
= 3 * fix factorial_ 2
= 3 * factorial_ (fix factorial_) 2
= 3 * (\rec n -> if n == 0 then 1 else n * rec (n-1)) (fix factorial_) 2
= 3 * (if 2 == 0 then 1 else 2 * fix factorial_ 1)
= 3 * (2 * fix factorial_ 1)
= 3 * (2 * factorial_ (fix factorial_) 1)
= 3 * (2 * (\rec n -> if n == 0 then 1 else n * rec (n-1)) (fix factorial_) 1)
= 3 * (2 * (if 1 == 0 then 1 else 1 * fix factorial_ 0))
= 3 * (2 * (1 * fix factorial_ 0))
= 3 * (2 * (1 * factorial_ (fix factorial_) 0))
= 3 * (2 * (1 * (\rec n -> if n == 0 then 1 else n * rec (n-1)) (fix factorial_) 0))
= 3 * (2 * (1 * (if 0 == 0 then 1 else 0 * fix factorial_ -1)))
= 3 * (2 * (1 * 1))
= 6
參考連結
Haskell/Fix and recursion
How do I use fix, and how does it work?
Grokking Fix