永続リアルタイムキューのHaskell実装と計算量解析

この記事はHaskellアドベントカレンダーその２の22日目の記事です。 Haskell (その2) Advent Calendar 2017 - Qiita

@rst76さんが昨日書いた記事でHaskellのリアルタイムキューがなかったので書きました。 qiita.com

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]型の項の集合で次の条件を満たすものとします。

1. eの計算量がO(1)かつeが[]に評価されるならば、eはO(1)リスト
2. eの計算量がO(1)かつx : xsのWHNFになった場合、xsがO(1)リストならばeもO(1)リスト
3. 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)リストではありません。

リアルタイムキューの計算量解析

リアルタイムキューを次のように実装しました。

	{-# LANGUAGE BangPatterns #-}
	module Queue (Queue, empty, snoc, head, tail) where
	import Prelude hiding(head,tail)
	-- invariant:
	-- length (frontList q) == length (tailList q) + length (thunk q)
	data Queue a =
	Queue {
	frontList :: [a]
	, tailList :: [a]
	, frontSize :: !Int
	, tailSize :: !Int
	, thunkSize :: !Int
	}
	empty :: Queue a
	empty = Queue { frontList = []
	, tailList = []
	, frontSize = 0
	, tailSize = 0
	, thunkSize = 0 }
	rotate :: [a] -> [a] -> [a]
	rotate = go []
	where
	-- invariant: length xs + 1 == length ys
	go !a [] (y : _) = y : a
	go !a (x : xs) (y : ys) = x : go (y : a) xs ys
	-- assumption: frontSize q - tailSize q - thunkSize q == - 1
	-- return: frontSize q' - tailSize q' - thunkSize q' == 0
	exec :: Queue a -> Queue a
	exec q =
	if thunkSize q > 0
	then
	q{ thunkSize = thunkSize q - 1 }
	else
	Queue f' [] n 0 n
	where f' = rotate (frontList q) (tailList q)
	n = frontSize q + tailSize q
	snoc :: Queue a -> a -> Queue a
	snoc q x = exec $! (q{ tailList = x : tailList q
	, tailSize = 1 + tailSize q})
	head :: Queue a -> a
	head q =
	case frontList q of
	[] -> error "emptyQueue"
	x : _ -> x
	tail :: Queue a -> Queue a
	tail q =
	case frontList q of
	[] -> error "emptyQueue"
	_ : f -> exec $! (q { frontList = f
	, frontSize = frontSize q - 1})

view raw Queue.hs hosted with ❤ by GitHub

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の構造に関する帰納法で示します。

1. xsが[]にO(1)で簡約されるとき。このとき、ysもO(1)でWHNFy : ys'に簡約され、その後go a [] (y:ys') = y : aと簡約されます。 aはO(1)リストなのでgo a xs ysはO(1)リストです。
2. 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)

*1:この概念はこのブログ記事のみで考えたもので一般的な用語ではないです