天天看點

Haskell語言學習筆記(78)fix

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 -> ...)

    的類型為

    (p -> p) -> p -> p

    參數 rec 的類型為

    (p -> p)

    ,參數 n 的類型為 p

    (Eq p, Num p) 說明類型 p 是可以比較的數值類型。

  • 非遞歸版本

    fix (\rec n -> ...)

    的類型為

    p -> p

  • 即非遞歸版本中 fix 的類型為

    ((p -> p) -> p -> p) -> p -> p

  • 對比 fix 函數的定義

    fix :: (a -> 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 的改寫方法:

  1. 如果遞歸版本 factorial 的函數定義分段進行,我們需要使用 if else 語句或者 case of 語句将所有定義式合成為一個。
  2. 将遞歸版本 factorial 的全部參數(這裡隻有 n)都移到函數定義式的右邊,也就是将函數定義改寫為一個lambda。
  3. 在這個 lambda 的所有參數(這裡隻有 n)之前添加一個 rec 參數,它的類型應該和遞歸版本 factorial 函數的類型相同。
  4. 将這個 lambda 中所有對于遞歸版本 factorial 函數的調用改為對 rec 的調用。
  5. 将這個改寫完畢的 lambda 作為參數傳給 fix 即可生成非遞歸版本 factorial’。

使用具名函數的改寫方法:

  1. 将遞歸版本的函數名 factorial 按照一定規則(比如加下劃線)改名為 factorial_。
  2. 在這個函數的所有參數(這裡隻有 n)之前添加一個 rec 參數,它的類型應該和遞歸版本 factorial 函數的類型相同。
  3. 将這個函數中所有對于遞歸版本 factorial 函數的調用改為對 rec 的調用。
  4. 将這個改寫完畢的函數 factorial_ 作為參數傳給 fix 即可生成非遞歸版本 factorial’。
  5. 如果需要将函數 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