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

後だしジャンケンかつ自分を納得させるためだけのような内容です(^^;

再帰的な束縛を模索する

ここでは強引な議論を展開します．先走るとリストモナドのmfixのあの妙な定義を引っ張り出す「発見的手法」を無理やり延々と展開します．

前回の考察の続き．pairwise swapの問題をとくに際して，do記法で再帰的な束縛，つまり

pairSwaps e = do (e',m)  <- replace n e
                 (e'',n) <- replace m e'
                 return e''

ということをしたいという状況でした．これを単純に（というか形式的というか，ナイーブというか）>>=に書き直すと

pairSwaps e = replace n e >>= (\(e',m) -> replace m e') >>= (\(e'',n) -> return e'')

という形にできるわけです．これじゃあ全然動かないけど，流れは見やすいと思います．気がつく点，そうであって欲しい点を徒然に列挙すると

• nはどこからくるのか？
• 最後のnは最初のnと同じでないと困る（nは不動点であってほしい）
• 最後は，e''のリストがでてくればいいから，e'やm，n自体は評価されなくても問題ないこともあるだろう
• 入力のTree中のリーフの値がそれぞれ不動点になるような感じ？
• do記法の最後のreturnは後回しにできそう．実際，最後は出来上がったe''をリストにまとめるだけでいいのではないか

pairSwaps e = 
    \n -> do (e', m) <- replace n e   -- (1)
             (e'',n) <- replace m e'  -- (2) 
             return ((e',m),(e'',n))

ひとまずこんな感じにしてみます．浅知恵ですが「nが固定されて」，(2)で条件に合わないものが消えてくれるだろうと考えてみます．returnはこうすることで「途中にでてくるもの」を引っ張り出せて木の変遷が見えるのでこうしてみました．結果は

pairSwaps (N (L 1) (L 2)) 1
= [
   ((N (L 1) (L 2),1),(N (L 1) (L 2),1)),
   ((N (L 1) (L 2),1),(N (L 1) (L 1),2)), -- これいらない
   ((N (L 1) (L 1),2),(N (L 2) (L 1),1)),
   ((N (L 1) (L 1),2),(N (L 1) (L 2),1))
  ]

pairSwaps (N (L 1) (L 2)) 2 
= [
   ((N (L 2) (L 2),1),(N (L 1) (L 2),2)),
   ((N (L 2) (L 2),1),(N (L 2) (L 1),2)),
   ((N (L 1) (L 2),2),(N (L 2) (L 2),1)), -- これいらない
   ((N (L 1) (L 2),2),(N (L 1) (L 2),2))
  ]

となります．考えてみれば当然で，シャドウーイング，つまり後で束縛された方が使われます．さらに，いらない2つを除いても6個あります．4個でいいはずです．これは前の考察を考えると，「n=nのケース」，つまりnの値が定まらなくてもよいケースがn=1，n=2として二重に数えられていると思われます．1-1の交換の(N (L 1) (L 2))と2-2の交換の(N (L 1) (L 2))がそれぞれ二回数えられているのです．したがって，

• 余計な2個を排除
• 複数回数えられるのを排除

ことが必要です．「余計な二個の排除」には最後のreturn ( (e',m),(e'',n) )のnが引数のnと同じであるようにすれば排除できるような感じがします．「複数回数えら得れるのを排除」するのは，そもそも手動で1，2と値を与えてるのが問題の根本だと考えられます．

「return ( (e',m),(e'',n) )のnが引数のnと同じ」とするにはfixの類が役に立ちそうです．途中違うものがきても最後で弾くことが期待できます．しかし，タプルの中のタプルの中にあるものを引っ張りだすのは厄介そうですし，nだけ引っ張りだしたら，本来欲しいe''を無視してしまいます．ですので，(e'',n)のまま扱う必要があります．(e',m)は本来は外にでてこなくていいものです．したがって，とりあえず

-- 動きません！
pairSwaps e = fix $ f 
              where f  ~(t, n) = do (e', m) <- replace n e   -- (1)
                                    (e'',n) <- replace m e'  -- (2) 
                                    return (e'',n)

というようにしてみます．遅延パターンにしてるのは，今までのfixの例，とくにiseven/isoddのケースからの知見です．nを共有させているのは，これを与えないと(1)が動作しないからです．なお，このコードはまず型が滅茶苦茶ですので動くわけがありませんし，仮にコンパイルできたとしてもfix fで出てくるであろう「n」が実際に評価されると，どうなるかわからないことが予想できます．また具体的に手を動かしてみます．

-- e = N (L 1) (L 2)
-- fix f = (t, n)
pariSwap e = fix $ f
fix f  = f (t, n) -- ここがいい加減．型が滅茶苦茶
 replace n e 
     = [ ((N (L n) (L 2)),1),
         ((N (L 1) (L n)),2)]

 replace 1 (N (L n) (L 2)) = [ ((N (L 1) (L 2)),n), ((N (L n) (L 1)),2) ]
 replace 2 (N (L 1) (L n)) = [ ((N (L 2) (L n)),1), ((N (L 1) (L 2)),n) ]
->
 [ ((N (L 1) (L 2)), n),
   ((N (L n) (L 1)), 2),
   ((N (L 2) (L n)), 1),
   ((N (L 1) (L 2)), n)
 ]

この段階でfix $ f の型と合わないのはますます明白ですが，とりあえず最初の要素をとって計算を進めてみます．すると

f ((N (L 1) (L 2)), n)  
=  [((N (L 1) (L 2)), n),
    ((N (L n) (L 1)), 2),
    ((N (L 2) (L n)), 1),
    ((N (L 1) (L 2)), n)]

となり，また「最初だけ」とってみると・・・( (N (L 1) (L 2) ), n)がでてきて不動点っぽくなってます．しかし，外にでてきているnは評価しようがありません．遅延パターンでとにかくでっちあげた「予約」みたいなnなので，値がありません．したがって，仮にコンパイルできたとしても，このnを評価しようとしたらずっと計算するしかありません．

次の要素( (N (L n) (L 1) ), 2)を考えてみます．

f ((N (L n) (L 1)), 2)  
  replace 2 (N (L n) (L 1)) = [ ((N (L 2) (L 1)), n), ((N (L n) (L 2)), 1) ]
  replace n (N (L 2) (L 1)) = [ ((N (L n) (L 1)), 2), ((N (L 2) (L n)), 1) ] 
  replace 1 (N (L n) (L 2)) = [ ((N (L 1) (L 2)), n), ((N (L n) (L 1)), 2) ] 

なので，また，先頭の要素だけをとると，( (N (L n) (L 2) ), 2)となります．もともと不動点fix f=(t,n)からスタートしたので，これも一致して欲しいので，n=2でt=N (L n) (L 1)=N (L 2) (L 1)でこれはうまくいきそうです．

というようにある意味いい加減に（いわゆる「発見的手法」で）進めていくと，

-- 動きません！
pairSwaps e = (fix  f)  >>= \ (e'',n) -> return e''
              where f  ~(e'', n) = do (e', m) <- replace n e   -- (1)
                                      (e'',n) <- replace m e'  -- (2) 
                                      return (e'',n)

という形がでてきます．fix $ fに>>=をつなげて，nを無視するようにしました．これで少なくとも「外に出てきたn」が問題になることは排除できたはずです．

問題の本丸，何度も書きましたが厄介なのは「型」の問題です．whereででっちあげているfとfixの型は

f   :: (Tree,Int)->[(Tree,Int)]
fix :: (a->a)->a

なので違うのは明らかです．ただし，上で試みた，\ (e'',n) -> return e''を導入する根拠になる計算からは，「リストの先頭からfixするようなfix」があればなんとかなりそうな雰囲気があります．とりあえずその「あったらいいなfix」の名前をlistfixとでもします．型は

listfix:: (a->[a])->[a]

となります．listfixがもっているべき性質は

• listfix fの各要素が「fの不動点」

ということになります．ただし型を考えるとf::a->[a]なので実際には不動点ではありえません．そこでまた前の計算を考えて，「先頭だけ」考える方針でいってみます．headと合成することで，

f.head:: [a]->[a]

とすると不動点がありうる型になります．head.f::a->aだと，f aの情報があまりに欠落しすぎる気がするので，やめておきます．

さてfix(f.head)を考えます．これはリストです．もし空リスト[]だったら，listfix fも空とすべきでしょう．空ではなかったら，(x:xs)としてパターンマッチしましょう．ここで，f xを考えてみます．

(x:xs) = fix (f.head) 
f x = f $ head (x:xs) = x:xs 

ですので，xは求める「不動点」の構成要素とみることが自然です．では，残りのxsはどうしましょうか．残りのxsについては何にも分かってないので，これをまたlistfixに与えて「不動点」である「先頭要素」を引っ張りだしてもらいます．xs= (tail.f) xなので，listfix (tail.f) とすると，今までの計算の類推でよさそうです．ということで，

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

という関数listfix::(a->[a])->[a]をでっちあげてみます．この関数を用いて，

data Tree = L Int | N Tree Tree deriving Show

fix::(a->a)->a
fix f = let x = f x in x

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

replace::Int->Tree->[(Tree,Int)]
replace x (L y) = [(L x,y)]
replace x (N l r) = [(N l' r, y) | (l',y) <- replace x l ]
                    ++ 
                    [(N l r', y) | (r',y) <- replace x r ]

pairSwaps:: Tree -> [Tree]
pairSwaps e = (listfix  f)  >>= \ (e'',n) -> return e''
              where f  ~(e'', n) = do (e', m) <- replace n e   -- (1)
                                      (e'',n) <- replace m e'  -- (2) 
                                      return (e'',n)

がまともに動くかを考えます．実際このコードは期待通りに動きますが，これを手計算で追いかけてみようということです．