defunctionalized continuation

Defunctionalization at Work
http://www.brics.dk/RS/01/23/

再帰関数はスタックを使うなどして、一階の関数とループで書ける事はよく知られているけど、その変換を機械的にやる方法。ループにするのは単にCPS変換すればよいけど、それだけだとcontinuationの中に定義したい関数が出てきたりしてよろしくない。なので、continuationをdefunctionalizationという技で一階化してやる

こうして、高階再帰関数を一階のループに落とすと、parser combinatorから有限オートマトンやプッシュダウンオートマトンが得られて、ラムダ計算のcall-by-value evaluatorからCEKマシンが得られる。parser combinatorは普通非決定性を持っていて(非決定性を言語機能として持たない言語では、リストやジェネレータで模倣するけど)一階に落としても非決定性が消えるわけではない。CPS変換やdefunctionalizationに非決定性の有無はあんまり関係ない気がするけど、本当にそうかどうかは知らない。プッシュダウンオートマトンとか割と複雑な定義であるけれども、ちゃんと自然な出自があるということが分かる

#その昔、
http://d.hatena.ne.jp/m-a-o/20070303#p4
同じ技でラムダ計算のevaluatorからabstract machineを得るというのは読んでたけど、当時は理解が全く足りず一般性のある方法だと分かってなかった

例1:CPS階乗関数

fact_cps :: Int -> (Int->Int) -> Int
fact_cps n k | n==0 = k 1
             | otherwise = fact_cps (n-1) (\v -> k (n*v))

fact n = fact_cps n (\x->x)

continuationにはInt->Int型の任意の関数が与えられるけども、実際にはそんな巨大な型は必要ない。continuationを代数的データ型にする

data Cont = C0 | C1 Cont Int

refun :: Cont -> (Int -> Int)
refun C0 = (\v->v)
refun (C1 k n) = (\v -> refun k (n*v))

fact_cps_def :: Int -> Cont -> Int
fact_cps_def n k | n==0 = refun k 1
                 | otherwise = fact_cps_def (n-1) (C1 k n)

fact n = fact_cps_def n C0

よく見ると、Contは[Int]と同じものになる。普通にリストを使うと、以下のような感じになる。長ったらしいけど、要するにfoldl (*) 1 [1..n]

fact_loop n ls | n==0 = aux ls 1
               | otherwise = fact_loop (n-1) (n:ls)
  where
    aux [] n = n
    aux (x:xs) n = aux xs (n*x)

fact n = fact_loop n []

例2:CPS fibonacci関数

fib_cps n k | n==0 = k 1
            | n==1 = k 1
            | otherwise = fib_cps (n-1) (\v1 -> fib_cps (n-2) (\v2 -> k (v1+v2)))

fib n = fib_cps n (\x->x)

data Cont = C0 | C1 Cont Int | C2 Cont Int

refun C0 = (\v -> v)
refun (C1 k v1) = (\v2 -> refun k (v1+v2))
refun (C2 k n) = (\v1 -> fib_cps_def (n-2) (C1 k v1))

fib_cps_def n k | n==0 = refun k 1
                | n==1 = refun k 1
                | otherwise = fib_cps_def (n-1) (C2 k n)

fib n = fib_cps_def n C0

普通にリストを使って書くと、あまり見慣れない形のものになる

fib_loop n ls | n==0 = aux ls 1
              | n==1 = aux ls 1
              | otherwise = fib_loop (n-1) ((Right n):ls)
  where
    aux [] n = n
    aux (Left n:xs) v1 = aux xs (n+v1)
    aux (Right n:xs) v1 = fib_loop (n-2) ((Left v1):xs)

fib n = fib_loop n []

例3:クイックソート

qsort [] = []
qsort (x:xs) = qsort [c|c<-xs , c<x] ++ [x] ++ qsort [c|c<-xs , c>=x]

CPS変換

qsort_cps [] k = k []
qsort_cps (x:xs) k = qsort_cps [c|c<-xs , c<x] (\lt -> qsort_cps [c|c<-xs , c>=x] (\gt-> k $ lt++[x]++gt))
qsort xs = qsort_cps xs (\x->x)

defunctionalization of continuation

data Cont a = C0 | C1 (Cont a) [a] a | C2 (Cont a) [a] a
refun C0 = \x->x
refun (C1 k xs x) = \lt -> qsort_cps_def [c|c<-xs , c>=x] (C2 k lt x)
refun (C2 k lt x) = \gt -> refun k $ lt++[x]++gt

qsort_cps_def [] k = refun k []
qsort_cps_def (x:xs) k = qsort_cps_def [c|c<-xs , c<x] (C1 k xs x)
qsort xs = qsort_cps_def xs C0

スタックには、二種類のラベルされたペア(a,[a])を積んでいく

qsort_loop (x:xs) stk = qsort_loop [c|c<-xs , c<x] $ (Left (x,xs)):stk
qsort_loop [] stk = aux stk []
  where
    aux [] rest = rest
    aux ((Left (x,xs)):stk) rest = qsort_loop [c|c<-xs,c>=x] $ (Right (x,rest)):stk
    aux ((Right (x,xs)):stk) rest = aux stk $ xs++[x]++rest

qsort xs = qsort_loop xs []

例4:プッシュダウンオートマトンの導出
parser combinatorは、普通やるように、matchした残りの文字列を返す関数として定式化して、あとは同じようにやっていく。具体例は書くのがめんどくさくなったので、略(論文に書いてある