[心得] Y Combinator 與 Mutual Recursion

看板PLT (程式語言與理論)作者noctem (noctem)時間14年前 (2010/06/03 20:57)推噓1(1推 0噓 0→)

留言1則, 1人參與討論串1/6 (看更多)

因為有人提到，所以複習了一下.. 1. Y combinator in Haskell Y combinator 在 untyped lambda calculus 中是 \f -> (\x -> f (x x)) (\x -> f (x x)) 試著寫成 Haskell: y :: (a -> a) -> a y f = (\x -> f (x x)) (\x -> f (x x)) f 的型別是 a -> a, 而 y 取 f 的 fixed-point，所以 y 的型別是 (a -> a) -> a. 但是這個型別一看就有問題：把 type 看成邏輯的話，這個 type 若有證明就會有 inconsistency. 果然， Haskell 不讓這個程式 typecheck: Occurs check: cannot construct the infinite type: t = t -> a Probable cause: `x' is applied to too many arguments In the first argument of `f', namely `(x x)' In the expression: f (x x) 操作上的理由是：在 (x x) 之中，x 的型別又是 t -> a, 又是 t, 而 t = t -> a 遞迴定義。解決方法也很簡單，就頭痛醫頭腳痛醫腳，做一個 t 與 t -> a 同構的遞迴型別囉。 data Fix a = Rec (Fix a -> a) -- Fix a 和 Fix a -> a 同構有了 Fix 就可以寫 Y combinator 了。 y :: (a -> a) -> a y f = (\(Rec x) -> f (x (Rec x))) (Rec (\(Rec x) -> f (x (Rec x)))) 和前一個版本比較，這裡多了很多 Rec，其實是在告訴 typechecker 何時要把 Fix 展開。 2. 用 Y 定義遞迴函數假設 Haskell 不允許遞迴定義（正確地說，允許遞迴資料型別，但不允許遞迴的 term），那要怎麼寫遞迴函數呢？遞迴版本的階層是這麼寫的: fact :: Int -> Int fact 0 = 1 fact (n+1) = (n+1) * fact n 沒有遞迴的話，就用 Y 取 fixed-point 囉。首先定義這個 factF: factF :: (Int -> Int) -> (Int -> Int) factF g 0 = 1 factF g (n+1) = (n+1) * g n 和 fact 的差別是 factF 只做 fact 的第一層。注意 factF 的型別。然後 fact 就是 factF 的 fixed-point: fact :: Int -> Int fact = y factF 由此可知一個語言如果有提供 closure, 就可以不用把遞迴當作 primitive. 3. Mutual Recursion Mutual recursion 其實也是一樣的，只是同時定義一組東西。比如說一般 even 和 odd 可以這樣定: even, odd :: Int -> Bool even 0 = True even (n+1) = odd n odd 0 = False odd (n+1) = even n 如果沒有遞迴，就定義一個從「一對」函數到一對函數的函數: evenOddF :: (Int -> Bool, Int -> Bool) -> (Int -> Bool, Int -> Bool) evenOddF (ev, od) = (\n -> if n == 0 then True else od (n-1), \n -> if n == 0 then False else ev (n-1)) evenOddF 拿一對函數 (ev,od)，產生一對函數，各自只做 even 和 odd 的第一層。本來該是遞迴的地方分別呼叫 od 和 ev. （如果該語言沒有 pair, 就用 lambda 來模擬。）然後我們也用 Y 取 evenOddF 的 fixed-point: evenOdd :: (Int -> Bool, Int -> Bool) evenOdd = y evenOddF even 就是第一個，odd 就是第二個: even = fst evenOdd odd = snd evenOdd 只是還有一點小問題：在 Haskell 中 y evenOddF 不會終止。簡單的解決方法是把 evenOddF (ev, od) = ... od .. ev ... 改成 evenOddF evod = ... snd evod ... fst evod ... 看起來比較漂亮，其實一樣的方法是用 lazy pattern: evenOddF ~(ev, od) = ... od .. ev ... 這樣就可以囉！ *Main> even 10 True *Main> odd 10 False -- ※ 發信站: 批踢踢實業坊(ptt.cc) ◆ From: 123.192.160.134