fix

Haskell で fix を理解する

fix に関する怪文書を書いてしまった・・・。(たぶん大きく間違ってはないと思うのですが、適当な事言ってたらすみません)

最初の出発点は、ベタに再帰を使って定義された階乗を計算する fact 関数です。

fact :: Int -> Int
fact 0 = 1
fact n = n * fact (n-1)

最終的なゴールはこの fact 関数を ラムダ式 の形式で書くことです。

そのために、この関数をちょっとずつ変形していきます。 まずは複数行のパターンマッチを1行にします。

fact2 :: Int -> Int
fact2 n = if n == 0 then 1 else n * fact2 (n-1)

この時、 if ~ then ~ else の形式はさほど重要ではありません。 場合分けができれば何でも良いです。 例えば、以下のように case で書いても同じことです。

fact2' :: (Int -> Int)
fact2' n = case n of
  0 -> 1
  n -> n * fact2' (n-1)

次に引数 n をラムダ式にします。

fact3 :: (Int -> Int)
fact3 = \n -> if n == 0 then 1 else n * fact3 (n-1)

ここまでは普通に簡単な式変形です。

この次のステップが結構大事です。 今やりたいことは再帰の形式をラムダ式に書き換えることでした。 ここまででかなり目標に近くなっています。 現時点ではこのようなラムダ式です。

\n -> if n == 0 then 1 else n * fact3 (n-1)

完全にラムダ式のみで書くということは fact3 = ... という形の関数定義すら行わないため このままでは fact3 が自由変数になってしまいます。

そのため fact3 に相当するラムダ式を引数に取るようにします。

\fact3 n -> if n == 0 then 1 else n * fact3 (n-1)

そしてこの引数 fact3 に (\n -> if n == 0 then 1 else n * fact3 (n-1)) を与えることができれば、 元の関数と同じになりそうですよね。

ちょっと確認してみましょう。

 (\fact3 n -> if n == 0 then 1 else n * fact3 (n-1)) (\n -> if n == 0 then 1 else n * fact3 (n-1))
= { 関数適用 }
 (\n -> if n == 0 then 1 else n * (\n -> if n == 0 then 1 else n * fact3 (n-1)) (n-1)))

失敗です・・・。ここで、さっきと同じ fact3 が自由変数になってしまう問題が再発しました。 つまり、引数の fact3 に与えるラムダ式は (\fact3 n -> if n == 0 then 1 else n * fact3 (n-1)) という形が良いということです。

-- 間違い
(\n -> if n == 0 then 1 else n * fact3 (n-1))

-- 正しい
(\fact3 n -> if n == 0 then 1 else n * fact3 (n-1))

この形式であれば自由変数の問題に悩むことはありません。

  (\fact3 n -> if n == 0 then 1 else n * fact3 (n-1)) (\fact3 n -> if n == 0 then 1 else n * fact3 (n-1))
= { 関数適用 }
  (\n -> if n == 0 then 1 else n * 
    (\fact3 n -> if n == 0 then 1 else n * fact3 (n-1)) (n-1)
  )

上記の計算を良く見ると、全く同じ形式のラムダ式を適用していますね。 (\fact3 n -> if n == 0 then 1 else n * fact3 (n-1)) を f で置き換えるとわかりやすいかもしれません。

  f f
= { 関数適用 }
  (\n -> if n == 0 then 1 else n * 
    f (n-1)
  )

何か見たことある形になってきましたね。 この f f という適用は、再帰が1回だけ回ったという意味と同じです。 ということはこの適用を無限回繰り返せば、最終的には基底部にたどり着きます。(f (n-1) という形になっているので、 n は減少しています) つまり f f f f f f ... ということです。

ここまでの成果をまとめると、 fact 関数は以下のようなラムダ式に書き換えることができました。

fact :: (Int -> Int) -> Int -> Int
fact = (\fact' n -> if n == 0 then 1 else n * fact' (n-1))

fix の定義に行く前に、本当に fact fact fact ... という適用によって再帰を実現しているかどうかを確かめます。

-- 一度も再帰しない (つまり基底部)
> fact undefined 0
1
> fact undefined 1
*** Exception: Prelude.undefined

-- 1回だけ帰納部で再帰できる
> fact (fact undefined) 0
1
> fact (fact undefined) 1
1
> fact (fact undefined) 2
*** Exception: Prelude.undefined

-- 5回だけ帰納部で再帰できる
> fact (fact (fact (fact (fact (fact undefined))))) 5
120

再帰の階段を1段ずつ作るのは楽しいですね。

fact を無限回書くのは無理なので、 foldr と repeat を組み合わせることにしましょう。

> foldr ($) undefined (repeat fact) $ 10
3628800

> foldr ($) undefined (repeat fact) $ 20
2432902008176640000

普段何気なく書いている以下のような定義は、無限回再帰する能力がある関数なんですね！

fact :: Int -> Int
fact 0 = 1
fact n = n * fact (n-1)

最後に fix の定義を確認してみましょう。(一応 Data.Function に fix が提供されていますが、ここでは理解を深めるため自分で定義します)

やりたいことは明確です。無限の f f f f f ... という適用の列を作りたいのでした。

fix :: (a -> a) -> a
fix f = f (fix f)

何も難しくないですね！

ここでは例として階乗の計算を取り上げましたが、実際には 自己再帰 の形になっていればどんな関数でも良いです。 例えば map でも良いです。

map :: (a -> b) -> [a] -> [b]
map _ [] = []
map f (x:xs) = f x : map f xs

この関数を fix の形式で書けばこうなります。

fix (\map' f xs -> if null xs then [] else f (head xs) : map' f (tail xs))

実際に ghci で動かしてみるとこんな感じです。

> :t fix (\map' f xs -> if null xs then [] else f (head xs) : map' f (tail xs))
fix (\map' f xs -> if null xs then [] else f (head xs) : map' f (tail xs))
  :: (a -> b) -> [a] -> [b]

> fix (\map' f xs -> if null xs then [] else f (head xs) : map' f (tail xs)) (+1) [1,2,3]
[2,3,4]

fix_poly の考察

少し考察しました。 僕の mutualFix では相互再帰の特殊なバージョンしか定義できないですね。

even や odd のような定義であればお互いに参照するだけなので問題にはなりませんが、 複数の再帰関数が必要になる場合に定義できなくなります。

-- こんな感じで、再帰関数が複数必要なケース
f n = f x + g x
g n = g x + f x

以下は、さらに一般化した定義[2]です。

fix_poly:: [[a] -> a] -> [a]
fix_poly fl = fix (\self -> map ($ self) fl)

iseven, isodd :: Int -> Bool
[iseven, isodd] = fix_poly [fe, fo]
  where
    fe [e, o] n = n == 0 || o (n-1)
    fo [e, o] n = n /= 0 && e (n-1)

計算ステップの確認

iseven
  -> fix_poly [fe, fo]
  -> fix (\self -> map ($ self) [fe, fo])
  -> (\self -> map ($ self) [fe, fo]) (fix (\self -> map ($ self) [fe, fo]))
  -> map ($ (fix (\self -> map ($ self) [fe, fo]))) [fe, fo]
  -> [ fe $ (fix (\self -> map ($ self) [fe, fo]))
     , fo $ (fix (\self -> map ($ self) [fe, fo]))
     ]
  -> [ fe $ [ fe $ (fix (\self -> map ($ self) [fe, fo]))
            , fo $ (fix (\self -> map ($ self) [fe, fo]))
            ]
     , fo $ [ fe $ (fix (\self -> map ($ self) [fe, fo]))
            , fo $ (fix (\self -> map ($ self) [fe, fo]))
            ]
     ]

リストの非決定性を上手く使ってる感じがしますね。 また、タプルを使った定義では異なる型の関数を作ることができるので、 fix_poly で全てが書けるというわけでも無い気がします。

mutualFix2 :: ((a, b) -> a, (a, b) -> b) -> (a, b)
mutualFix2 (f, g) = (f fg, g fg)
  where
    fg = mutualFix2 (f, g)

ソースコード

import Prelude hiding (even, odd)
import Data.List (intersperse)
import Data.Function (fix)

even' :: (Int -> Bool) -> Int -> Bool
even' = \f n -> if n == 0 then True else f (n-1)

odd' :: (Int -> Bool) -> Int -> Bool
odd' = \f n -> if n == 0 then False else f (n-1)

mutualFix :: (a -> a) -> (a -> a) -> a
mutualFix f = foldr ($) undefined . intersperse f . repeat

even :: Int -> Bool
even = mutualFix odd' even'

odd :: Int -> Bool
odd = mutualFix even' odd'

-- another version
even2' :: (Int -> Bool, Int -> Bool) -> (Int -> Bool)
even2' = \(even, odd) n -> if n == 0 then True else odd (n-1)

odd2' :: (Int -> Bool, Int -> Bool) -> (Int -> Bool)
odd2' = \(even, odd) n -> if n == 0 then False else even (n-1)

mutualFix2 :: ((a, b) -> a, (a, b) -> b) -> (a, b)
mutualFix2 (f, g) = (f fg, g fg)
  where
    fg = mutualFix2 (f, g)

even2, odd2 :: Int -> Bool
(even2, odd2) = mutualFix2 (even2', odd2')

-- http://okmij.org/ftp/Computation/fixed-point-combinators.html
fix_poly:: [[a] -> a] -> [a]
fix_poly fl = fix (\self -> map ($ self) fl)

iseven, isodd :: Int -> Bool
[iseven, isodd] = fix_poly [fe, fo]
  where
    fe, fo :: [Int -> Bool] -> Int -> Bool
    fe [e, o] n = n == 0 || o (n-1)
    fo [e, o] n = n /= 0 && e (n-1)

Haskell で omega と fix を定義する

Haskellで賢人鳥(またの名をYコンビネーター) に unsafeCoerce を使えば定義できるとあったので、実際にやってみた。

FIx.hs

import Unsafe.Coerce

fact :: (Int -> Int) -> Int -> Int
fact = (\fact' n -> if n == 0 then 1 else n * fact' (n-1))

omega :: a
omega = (\x -> x (unsafeCoerce x)) (\x -> x (unsafeCoerce x))

fix' :: ((a -> b) -> a -> b) -> a -> b
fix' = \f -> (\x -> f (\y -> x (unsafeCoerce x) y)) (\x -> f (\y -> x (unsafeCoerce x) y))

fix'' :: (a -> a) -> a
fix'' = \f -> (\x -> f (x (unsafeCoerce x))) (\x -> f (x (unsafeCoerce x)))

実行結果

*Main> fix' fact 5
120
*Main> fix'' fact 5
120

参考リソース

1. Writing the fixed-point combinator in a typed language

2. Many faces of the fixed-point combinator

3. Haskellで賢人鳥(またの名をYコンビネーター)