コミックマーケット78の宣伝

今日！！8月14日土曜日にコミックマーケット78で@m0h1canさんが編集長を勤めたCOMFRKという、何か良く分からない記事が集まった本が出ます。

http://ratiwo.blogspot.com/2010/08/comfrk-vol-1.html

さて、ぼくの記事の紹介をしたいと思います。

Circular Programming

天下り的ですが、こういう問題設定がなされたとします。

2分木が与えられた時、その木の値全てを、その木の最大値で置き換えよ。

例を見た方がはやいと思うので、手っ取り早くHaskellのコードを書きます。C++の方が人口的には良い気がするのですが、(recursiveな)variantを使うのが面倒臭いのでごめんなさい。

data BTree = Leaf Int | Node BTree BTree
                         deriving Show

repmax t = ...

とした時に、

repmax (Node (Node (Leaf 0) (Leaf 1)) (Node (Leaf 2) (Leaf 3)))
=>
Node (Node (Leaf 3) (Leaf 3)) (Node (Leaf 3) (Leaf 3))

となるような関数repmaxを実装せよ、という話です。

普通に考えると、2回木を舐める(格好付けて2-passと呼びましょう)実装が出て来て

-- t_foldはpreorder(簡単に言うと深さ優先探索をした時のノードを辿る順番で見るという事です)順で関数を値に適用してsummerizeします
-- Traversable使わないんですか？みたいなのは御免なさい使ってません。
t_fold f t = t_fold' f t Nothing
    where
      t_fold' f (Leaf n) Nothing = n
      t_fold' f (Leaf n) (Just n') = f n' n
      t_fold' f (Node l r) v = t_fold' f r (Just $ t_fold' f l v)

-- 木の全ての値に対して関数fを適用
traverse f (Leaf n) = Leaf (f n)
traverse f (Node l r) = Node (traverse f l) (traverse f r)

find_max = t_fold max

repmax1 t = traverse (const $ find_max t) t

これだと一度木を舐めて最大値を見付けて来て、それを使ってもう一度舐めて全ての値を置き換えているので2-passです。

ところで、0-passでやるのはどう考えても無理そうなんですが、1-passで要求を満たす関数を実装する事は出来ないものでしょうか?

1-passでやるとすると、最大値を求めつつ木の値を差し替えて行けば良さそうです・・・？？？そんな事出来るのでしょうか？
だって最大値を求め終わっていないと、木の値を差し替える事は出来ないんだから、順番ってもんがあるでしょう！？

いやいや、次のように書けたらどうでしょうか?

repmax2 t = t'
  where
    (t' , max_val) = repmax t max_val
    repmax ...

repmaxは、

引数として、変換対象の木と、木を変換する為に必要な値を取る
返値として、変換された木と、引数として取った木の最大値を返す

このように引数と返値の意味を考えると、どうもこの形でrepmaxを使うと上手く行くような気がします。

ではこの引数と返値に合うように、実装をしてみましょう。

data BTree = Leaf Int | Node BTree BTree
             deriving Show

repmax2 t = t'
    where
      (t' , max_val) = repmax t max_val

      repmax :: BTree -> Int -> (BTree , Int)
      repmax (Leaf i) max_val = (Leaf max_val , i)
      repmax (Node l r) max_val = (Node l' r' , max max_val1 max_val2) -- lとrを部分木に持つ木の最大値は、max_val1とmax_val2の大きい方
          where
            (l' , max_val1) = repmax l max_val -- max_val1は木l中の最大の値
            (r' , max_val2) = repmax r max_val -- max_val2は木r中の最大の値

すんなりと定義出来ました。ではこの関数を使ってみましょう。

GHCi, version 6.12.3: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Loading package ffi-1.0 ... linking ... done.
[1 of 1] Compiling Main             ( blog.hs, interpreted )
Ok, modules loaded: Main.
*Main> let t1 = Node (Leaf 0) (Leaf 1)
*Main> let t2 = Node t1 t1
*Main> let t3 = Node t2 t2
*Main> let tree = Node t3 t3
*Main> repmax2 tree
Node (Node (Node (Node (Leaf 1) (Leaf 1)) (Node (Leaf 1) (Leaf 1))) (Node (Node (Leaf 1) (Leaf 1)) (Node (Leaf 1) (Leaf 1)))) (Node (Node (Node (Leaf 1) (Leaf 1)) (Node (Leaf 1) (Leaf 1))) (Node (Node (Leaf 1) (Leaf 1)) (Node (Leaf 1) (Leaf 1))))
*Main> let tree = Node (Leaf 2) (Node t3 t3)
*Main> repmax2 tree
Node (Leaf 2) (Node (Node (Node (Node (Leaf 2) (Leaf 2)) (Node (Leaf 2) (Leaf 2))) (Node (Node (Leaf 2) (Leaf 2)) (Node (Leaf 2) (Leaf 2)))) (Node (Node (Node (Leaf 2) (Leaf 2)) (Node (Leaf 2) (Leaf 2))) (Node (Node (Leaf 2) (Leaf 2)) (Node (Leaf 2) (Leaf 2)))))
*Main>

見事動きました！！

これは何なの?

http://www.haskell.org/haskellwiki/Circular_programming

まぁこの辺の話です。
というより、皆さんおなじみBirdさんの
"Using Circular Programs to Eliminate Multiple Traversals of Data"というActa Informaticaという論文に載った有名な問題のパクリ(元のお話は、最小値で置換せよ、でした)です。

ついでに面白い練習問題があって、

ある文字列が回文になっているかどうかを、リストを1回舐めただけ(1-pass)で判定する関数を書け。

というものがあります。これも普通に考えると、eqlist (あるリスト) (reverse あるリスト)というものが出て来ますが、これは"あるリスト"を2回舐めなければ成りません。

ところがPrologだと

Prologだと眠いので適当ですが次のようなコードが書けます。

btree(leaf(_)).
btree(node(L,R)) :- btree(L) , btree(R).

find_max(Tree,Ret) :- find_max_impl(Tree,Now,Ret).
find_max_impl(leaf(X),Now,X) :- var(Now) , !.
find_max_impl(leaf(X),Now,X) :- Now < X , !.
find_max_impl(leaf(X),Now,Now).
find_max_impl(node(L,R),Now,Ret2) :- find_max_impl(L,Now,Ret1) , find_max_impl(R,Ret1,Ret2) , !.

% こっちが1-pass
rep1(Tree,Ret) :- find_max(Tree,Max) , rep(Tree,Max,Ret).
rep(leaf(X),Max,leaf(Max)).
rep(node(L,R),Max,node(Ret1,Ret2)) :- rep(L,Max,Ret1) , rep(R,Max,Ret2).

% こっちが2-pass
rep2(Tree,Ret) :- rep_impl(Tree,PlaceHolder,Now,Max,Ret) , PlaceHolder = Max.
rep_impl(leaf(X),PlaceHolder,Now,X,leaf(PlaceHolder)) :- var(Now) , !.
rep_impl(leaf(X),PlaceHolder,Now,X,leaf(PlaceHolder)) :- Now < X , !.
rep_impl(leaf(X),PlaceHolder,Now,Now,leaf(PlaceHolder)).
rep_impl(node(L,R),PlaceHolder,Now,Max,node(Ret1,Ret2)) :-
	rep_impl(L,PlaceHolder,Now,LeftMax,Ret1) ,
	rep_impl(R,PlaceHolder,LeftMax,Max,Ret2).

rep1はそのまんま、一度全体をなめて最大値を得て、それをもってして2度目のペロペロで置換するという述語です。

rep2はこれは少しだけPrologっぽい解き方に成っています。概要としては、

木の要素全体にポインタを設置してまわる
と同時に最大値を求める
全体をペロペロし終わって最大値が求まった所で、全体に張ったポインタを一気に差し替える！！(PlaceHolder = Maxと書くだけで出来る！)

としています。

アドレスや参照という概念がある言語でも同じように実装出来ると思うのですが、それは知らないです！！C++だとCastorあたりのcoreを引っ張ってくると非常に簡単に出来ますね！！

こっちが本題

もうみたまんま(?)なのですが、「型付きλ計算の強正規化定理の証明をしよう！！」というのがメインテーマの何かを書いてしまいました。
これとCircular Programmingの中途半端な話と何の関係があるんですか？って感じですが、@m0h1canさんがプロのPrologerなので、@m0h1canさんと東ア47a握手だ！！！って事が言いたかったんですよ！！！！！！！

もうちょっと詳しく

型付きλ計算では、どう頑張っても停止しちゃうような関数しか書けないっていう、こう書くとネガティブっぽい感じなんですがとっても良い性質があります。

割と普通の教科書だと証明が書いているのですが、その証明を割と仔細に、それから堅苦しく無い感じで書くとどうなるんだろいうという試みのもと生まれた原稿です。が、結構堅苦しくなっています・・・。