MonadFixの理解のために(2)---リストモナドでmfix考える4

Haskell

ここまではpairwise swapという具体的なもので考えてきたので，こんどは抽象的に攻めてみます．MonaFixのインスタンスのmfixには満たすべき性質があるのでした．

-- purity
mfix (return . h) = return (fix h)
-- left shrinking (or tightening)
mfix (\x -> a >>= \y -> f x y) = a >>= \y -> mfix (\x -> f x y) 
-- sliding
mfix (liftM h . f) = liftM h (mfix (f . h)), for strict h. 
-- nesting
mfix (\x -> mfix (\y -> f x y)) = mfix (\x -> f x x)

これらの性質をリストモナドのmfix

mfix f = case fix(f.head) of
            []   -> []
            x:_ -> x:mfix (tail.f)

が満たすことを（かなりアバウトに）検証してみます．

purity

-- h:: a->a
-- mfix::(a->[a])->[a]
mfix (return . h) = return (fix h)

を考えます．

(return.h) x = [h x]
(head.return.h) x = h x
fix (head.return.h) = fix h

だから，case fix (head.return.h)は

fix h : mfix (tail.return.h)

となって，tail.return.h = []なので，

mfix (return . h) = [fix h] = return (fix h)

が成り立ちます．

これはmfixがモナドが出てこない「普通の関数」に対してはmfixはfixと同じであることを示しています．

left shrinking（またはtightening）

-- f:: a -> b -> [c]
-- mfix::(d->[d])->[d]
mfix (\x -> [b1,b2,...] >>= \y -> f x y) = [b1,b2,...] >>= \y -> mfix (\x -> f x y)

ちょっと表記を変えました．xの型はa，yの型はbとしています．

\x-> [b1,b2,...] >>= \y -> f x yを名前をつけてg x = [f x b1,f x b2,...]と表現し，mfix gを考えます．

(g.head) [x,...] = [f x b1,f x b2,...]
fix (g.head) = x  where f x b1 = x

なので，

mfix g = x1 : mfix(tail.g) where  f x1 b1 = x1

となります．これを繰り返していくことで

mfix g = [x1, x2, x3, ...] where xi = f xi bi (i=1,2,3,...)
mfix g = [x1, x2, x3, ...] where xi = fix (\x -> f x bi) (i=1,2,3,...)

ここで，\y -> fix (\x->f x y) を考えれば，リストモナドの>>=がconcatMapであることから

mfix g = [x1, x2, ...] = [b1,b2,...] >>= \y -> fix (\x->f x y)

つまり，

-- left shrinking (or tightening)
mfix (\x -> a >>= \y -> f x y) = a >>= \y -> mfix (\x -> f x y)

が成り立つことが分かります．

これは，不動点の計算の対象とはならない変数（aとy）は>>=ごとmfixの左に追い出すことができることを意味します．mfixの対象を左側に追い出して小さくする（shrink），引き締める（tighten）ということでしょうか．

以下，正直に書くと記号が大氾濫するので，かなりおおざっぱに検証します．まじめにやるとすごいことになってかけません。。。多分。

sliding

-- f:: r ->  m a
-- mfix :: (r-> m r)-> m r
mfix (liftM h . f) = liftM h (mfix (f . h)), for strict h::a->r. 

liftM   :: (Monad m) => (a -> r) -> m a -> m r
liftM h m1  = do x1 <- m1
                 return (h x1)

左辺をざっくり計算すると

f r1 = [a1,a2,...] 
(liftM h. f) r1 = [h a1, h a2, ....]
(liftM h.f) $ head [r1, r2,...] = [h a1, h a2, ....]
fix ((liftM h.f). head) = [h a1, h a2, ...] = [r1, r2, ...]
mfix (liftM h. f) = h a1: mfix (tail.liftM.f)

一方，右辺をざっくり計算すると

f.h.head [a1,a2,....] = f (h a1) = f r1 = [a1,a2,...]
fix (f.h.head) = [a1,a2,...] = f (h a1)
mfix (f.h) = a1:mfix (tail.f.h)
lisftM h mfix(f.h) = h a1:liftM h mfix (tail.f.h)

ということなので，成立しているのが分かります．

liftM hが外にでてくるということでslidngということでしょうか．

nesting

-- f:: a -> a->  m a
-- mfix :: (a-> m a)-> m a
mfix (\x -> mfix (\y -> f x y)) = mfix (\x -> f x x)

文字がいり乱れますが・・・右辺から．

k x = f x x
fix(k.head)= [c1,c2,..] = f c1 c1 
mfix k = c1:mfix(tail.k)

としておくと

f c1 = g 
g.head [c1,c2,...] = f c1 c2 = [c1,c2,..]
fix(g.head) = [c1,c2,...]  

h = \x ->  mfix (\y -> f x y)
h.head [c1,c2,...]  = c1:mfix(tail.g)

fix(h.head)=[c1,...]
mfix h = c1:...

のような具合で，やはり成り立っていることが分かります．


・・・しっかし，自分が何をやってるのかわかんなくなってきた．そもそもコラッツの計算でHaskellでのメモ化が知りたくなって，Stateモナドを調べ初めて，そこででてきたMonadFixではまって，リストモナドでMonadFixはdo記法の再帰版だということに流れ着いてきたのだったが・・・寄り道しすぎて戻れなくなった．自爆ですね．いい加減Project Eulerに戻るかな・・・

[Haskell] 逆引き

sampou.orgに「逆引き」のコーナーができています．なんか私がごちゃごちゃいったのが始まりなのかなと思いつつ，あのままだとさすがに使いにくいというか，まだ種の段階ですよね．どうすると実用的になるのでしょうか？

  • 型を明記する
  • 具体例をつける
  • 項目ごとに分割する
  • 市販の書籍のような体裁にしてみる？(PDF）

。。。考えてみる価値はありそうです．