永続リアルタイムキューのHaskell実装と計算量解析
この記事はHaskellアドベントカレンダーその2の22日目の記事です。 Haskell (その2) Advent Calendar 2017 - Qiita
@rst76さんが昨日書いた記事でHaskellのリアルタイムキューがなかったので書きました。 qiita.com
12/23追記 この記事の内容に重大な誤りが指摘されました 参考 末尾にて修正しています。申し訳有りません。
WHNFとは
WHNFはWeak Head Normal Formの略で、項がCnstr e_1 ... e_n
の形まで評価された状態を指します。
e_1 ... e_n
の部分はWHNFでなくても良いところがポイントです。
例えばリストの場合、
[]
や1 : []
、undefined : reverse [1,2,3]
などはWHNFですが
reverse [1,2,3]
はWHNFではありません。
遅延評価に於ける計算量解析
まず、項e
の計算量をe
をWHNFまで簡約するのに必要なステップ数(書き換え規則の適用回数)と定義します。
例えば[1,2,3] ++ [4,5,6]
の計算量は1です。(++)の定義は
(++) [] ys = ys (++) (x:xs) ys = x : xs ++ ys
なので
[1,2,3] ++ [4,5,6] = 1 : [2,3] ++ [4,5,6]
と1ステップでWHNFになります。
つぎにreverse [1,2,3, ... , n]
の計算量を見ていきましょう。reverse
の定義は
reverse l = rev l [] where rev [] a = a rev (x:xs) a = rev xs (x : a)
です。
reverse [1,2,3, ... , n] = rev [1,2,3, ... , n] [] = rev [2,3, ..., n] [1] = rev [3,..., n] [2,1] ... = rev [] [n, ..., 3, 2, 1] = [n, ..., 3, 2, 1]
となるので計算量はn+2となります。
次にO(1)リストという概念を定義します。*1 O(1)リストは[a]型の項の集合で次の条件を満たすものとします。
e
の計算量がO(1)かつe
が[]
に評価されるならば、e
はO(1)リストe
の計算量がO(1)かつx : xs
のWHNFになった場合、xs
がO(1)リストならばe
もO(1)リスト- O(1)リストの集合は条件1,2を満たすものなかで最小の集合。
つまり、リストのtail部分に含まれるthunk1つをWHNFに簡約するのに必要な計算量がO(1)のとき、 O(1)リストと言います。
例えば
xs
とys
がO(1)リストならばxs ++ ys
はO(1)リストです。
[1,.., n ] ++ reverse [1,..,n]
はreverse [1,..,n]
の計算量がO(n)なのでO(1)リストではありません。
リアルタイムキューの計算量解析
リアルタイムキューを次のように実装しました。
gist1a49ce4cfa8b4730f7b055eb9423e879
このQueueライブラリのsnoc
, head
, tail
がO(1)であることを示します。
rotateについて
まず、xs
、ys
がO(1)リストであるときrotate xs ys
もO(1)リストであることを帰納法で示します。
rotate xs ys = go [] xs ys
まず1ステップでこのように簡約されます。
go
の定義は
go !a [] (y : _) = y : a go !a (x:xs) (y:ys) = x : go (y : a) xs ys
です。
a
, xs
, ys
がO(1)リストであるとき、go a xs ys
もO(1)リストであることをxs
の構造に関する帰納法で示します。
xs
が[]
にO(1)で簡約されるとき。このとき、ys
もO(1)でWHNFy : ys'
に簡約され、その後go a [] (y:ys') = y : a
と簡約されます。a
はO(1)リストなのでgo a xs ys
はO(1)リストです。xs
がx : xs'
にO(1)で簡約されるとき。同様にys
もO(1)でWHNFy : ys'
に簡約され、go a (x : xs') (y : ys') = x : go (y : a) xs' ys'
に評価されます。(y : a)
,xs'
,ys'
はO(1)リストなので、帰納法の仮定からgo (y : a) xs' ys'
もO(1)リストです。したがってgo a xs ys
もO(1)リストとなります。
つぎに、Queue a型の項についてもO(1)リストと同様の概念を定義します。すなわち、
qがO(1)キューであるとは、qをWHNFにO(1)で簡約できて、かつ、frontList q
とtailList q
もO(1)リストであるときとします。
execについて
次にq
がO(1)キューのとき、exec q
もO(1)Queueであることを確認します。
これはexec
は再帰関数でないので定義よりほぼ明らかです。
snoc, head, tailについて
snoc :: Queue a -> a -> Queue a snoc q x = exec $! (q{ tailList = x : tailList q , tailSize = 1 + tailSize q})
このとき、q
がO(1)キューのとき、q { tailList = x : tailList q, tailSize = 1 + tailSize q }
はO(1)でWHNFになり、exec $! (q { ... })
もO(1)キューとなります。
tail
についても同様です。q
がO(1)キューのときtail q
もO(1)キューです。
結論
以上の議論から、q
がO(1)キューのとき、snoc q
, head q
, tail q
の計算量はO(1)で、返ってくるキューもO(1)キューとなります。
注意
各操作がO(1)だからといって、このQueueを使う側が正格にキューを評価しないとリアルタイムキューにはなりません。 例えば、次のような例だと
main = do let go :: Queue Int -> IO (Queue Int) go q = fmap read getLine >>= \v -> if v != 0 then go (snoc q v) else return q q <- go empty print (head q) -- O(n)
最後のhead q
の計算量は入力の長さに対してO(n)となります。
正しくは、次のように、qを正格に評価しましょう。
main = do let go :: Queue Int -> IO (Queue Int) go !q = fmap read getLine >>= \v -> if v != 0 then go (snoc q v) else return q q <- go empty print (head q) -- O(1)
間違いと修正
上で提示したQueueはリアルタイムキューになっていませんでした。 間違いは
まず、
xs
、ys
がO(1)リストであるときrotate xs ys
もO(1)リストであることを帰納法で示します。
の部分で、正しくは、xs
, ys
がO(1)リストでは不十分で、すべてのtail部分がWHNFに評価されたリスト
すなわちxs = [v_1, v_2, ..., v_n], ys = [w_1, w_2, ..., w_{n+1}]
の形になっていなければならないです。
そうするためには、こちらのF#実装にあるように、
サンクを表すポインタをつけて、snoc時にもthunkを潰す処理が必要でした。
修正バージョンを載せておきます。
gistac6a16ffb32f86d4edabb079495d1e9d
*1:この概念はこのブログ記事のみで考えたもので一般的な用語ではないです