オートマトンの設計

大学で計算理論の講義を取っていて,宿題で「n の倍数となる2進数文字列を受理するオートマトンの状態遷移図を描け(n=2,3,4,6)」と云う問題が出ました.

まあそれは剰余に注目すれば簡単に解ける訳ですが,どうせなので状態数をゴルフしよう1と思ったりするわけです. その為には,同じ入力に対して次の状態が同じものを同一視してやればいい2訳ですが、合ってるとは思ってもちょっと不安です.

そこで,Haskell の QuickCheck / smallcheck を使って、どうやら大丈夫そうだぞ、と云うのを確かめてみることにしました.

QuickCheck / smallcheck とは?

QuickCheckというのは,既に知っているひともいるかと思いますが、簡単に云って乱数テストを自動的に実行してくれるようなライブラリです.函数やデータ構造が満たしてほしい性質を記述すると、自動的にランダムに値を生成して、その性質が成り立つかをチェックしてくれるのです.詳しくは『関数プログラミングの楽しみ』の第二章で解説されています。

対してsmallcheckは,QuickCheck と Alloy を出会わせたような性格をしています.仕様を記述するまでは同じなんですが,QuickCheck が乱数を生成していたのに対して,SmallCheck は特定の「深さ」までのデータを全て,exhaustive に生成してチェックする,と云う違いがあります. Alloy を出会わせたような,と云うのは,Alloy の設計思想である「小スコープ仮説」と云うものに基づいているからです.小スコープ仮説と云うのは,「大きく複雑なケースで出て来るバグは,(複雑性の)小さなスコープでも再現する筈だ」と云うものです.勿論これだけ小さなスコープで再現すればOK!みたいな上限は存在しません.そんなのがあったらチューリングマシン停止問題が解けちゃいますから. じゃあどうするのか,と云うと,段々とデータの大きさ(スコープ)を大きくしていって,ある程度まで確かめて大丈夫だったらそれで良いだろう,とします.

実装してみよう

取り敢えずは,素朴にオートマトンを実装してみたのが次です.

module Main where
import Test.QuickCheck
import Data.Char
import Numeric
import Data.Maybe
import Data.List
import Data.Ord
import Data.Function
import Control.Arrow
import Data.Word
import Control.Applicative

data Automaton s i = Automaton { initial    :: s
                               , accepted   :: [s]
                               , transition :: s -> i -> s
                               }

runAutomaton :: Automaton s i -> [i] -> s
runAutomaton (Automaton q0  _ t) is = go q0 is
  where
    go q []     = q
    go q (i:is) = go (t q i) is

isAccepted :: Eq s => Automaton s i -> [i] -> Bool
isAccepted auto is = runAutomaton auto is `elem` accepted auto

fromList :: (Eq i, Eq s, Ord s) => [(s, i, s)] -> s -> i -> s
fromList dic s i = fromJust $ lookup i =<< lookup s d'
  where
    d' = map (fst . head &&& map snd)
           $ groupBy ((==) `on` fst)
           $ sortBy (comparing fst) $ map (\(a,b,c) -> (a,(b,c))) dic

取り敢えず,Automaton s iは内部状態sで,iのリストを入力に取るオートマトンです. 遷移函数を一々記述するのが面倒なので,状態の一覧を書いた辞書リストから遷移関数を作ってくれるのがfromListですね. runAutomatonisAcceptedは定義のまんまですね.走らせた後の状態が受理状態に入っていたら受理である,という.

では,これらを使って,二進数の入力列を受け取って,6の倍数か判定するオートマトンを書いてみましょう.

aDivBy6' :: Automaton Int Char
aDivBy6' = Automaton 0 [0] go
  where
    go s i = (s * 2 + digitToInt i) `mod` 6

aDivBy6 :: Automaton Int Char
aDivBy6 = Automaton 0 [0] (fromList dic)
  where
    dic = [ (0, '0', 0), (0, '1', 1), (1, '0', 2), (1, '1', 3)
          , (2, '0', 1), (2, '1', 2), (3, '0', 0), (3, '1', 1)
          ]

最初のは素朴に桁がズレるごとに今の余りを二倍して新しい桁を足している,という素朴な実装です.これは明らかに6の倍数のみを受け付けるオートマトンです. 二番目のを出すのには工夫がいります.たとえば,最初のやつの状態遷移図を描いてみて,動作の同じ状態どうしを纏めて一つにしてみたものと見れます. 他にも,3の倍数かつ0で終わる(=2の倍数)ときに受理する,と云う風に読んでもいいです.

QuickCheck を使ってみる

理屈の上では多分二番目のも素朴なaDivBy6'と同様に動いてくれる筈です.でも,ちょっと不安だなあ……. と云うわけで,早速 QuickCheck で確かめてみましょう!

6で割れればaDivBy6でその二進数表現が受理される,と云う条件を書きます.

showBin :: Integral r => r -> String
showBin = flip (showIntAtBase 2 intToDigit) ""
   
test_automaton0 :: Word -> Automaton Int Char -> (Word -> Property)
test_automaton0 base auto = \r -> r `mod` base == 0 ==> isAccepted auto (showBin r)

showBin は2進表現に変換するヘルパ函数ですね. test_automaton0は,底とチェックしたいオートマトンを受け取って,仕様を返す函数です. QuickCheck での「仕様」は,単なるBoolProperty,または何らかの引数を取ってBool または Propertyを返す函数のいずれかです.わかりやすいように,ここでは仕様になる部分を括弧で括って

Word -> Property

と書いています.何らかの引数,と云いましたが,正確には QuickCheck が生成方法を知っている必要があるので,Arbitraryクラスのインスタンスであるひつようがあります.ここではWord,すなわち正の整数です. なので,これは,「指定した底で割り切れるならオートマトン auto で受理される」のが仕様です.

では,実際にテストしてみましょう!テストするには,quickCheck函数に喰わせるだけで大丈夫です.ライブラリが自動的に例を乱数生成して,仕様が満たされているかチェックしてくれます.

ghci> quickCheck $ test_automaton0 6 aDivBy6
+++ OK, passed 100 tests.

なんだか矢鱈時間が掛かりますね…….今回は上手くいきましたが,何度か試してみると……

ghci> quickCheck $ test_automaton0 6 aDivBy6
*** Gave up! Passed only 92 tests.

のように,92の試験に合格したのちに,100に到達しきれなくてギブアップしてます. これは,6の倍数以外も全部生成して試しているからです.事前条件に引っ掛からなかった値は捨て去られるので,大量の無駄が発生してしまっているのです.

では,最初から6の倍数だけ生成して試すようにしてみましょう.

divisible :: Word -> Gen Word
divisible d = (d *) <$> arbitrary `suchThat` (<(maxBound `div` d))
   
test_automaton1 :: Word -> Automaton Int Char -> Property
test_automaton1 base auto = forAll (divisible base) $ \r -> isAccepted auto (showBin r)

divisibleで任意の自然数で割り切れる数だけを生成しているわけです.「d 倍しても桁溢れしない任意の数を用意して,それを d倍する」と,そのまま読み下せますね. test_automaton01のほうも,そのまま「任意のbaseで割り切れる自然数 r について,その2進表現が auto で受理される」と読めます.

使ってみると……

ghci> quickCheck $ test_automaton1 6 aDivBy6
+++ OK, passed 100 tests.

こんどはすぐにテストをパスしています!上手くいったようですね.

と,思いますが,よくよく考えたら問題は「6の倍数か判定するオートマトン」,つまり「6の倍数だけを受理するオートマトン」を作ることでした.このままだと,6の倍数が受理されることはわかりますが,6の倍数でないものが受理される可能性があります.

ではどうするか.折角定義した divisibleを使うのをやめて,両方の場合を一気にチェックする函数に書き換えましょう.

test_automaton2 :: Word -> Automaton Int Char -> (Word -> Bool)
test_automaton2 q a =
  \r -> if r `mod` 6 == 0
        then isAccepted a (showBin r)
        else not $ isAccepted a (showBin r)

仕様はPropertyでもWord -> Propertyでもなく,単なる述語Word -> Boolに変わっていますね.6で割れれば受理され,そうでなければ受理されないこと,とそのまま記述しています.

では,これを使ってみましょう.

ghci> quickCheck $ test_automaton2 6 aDivBy6
+++ OK, passed 100 tests.

すぐに実行がおわって,テストを通過しました!やりましたね!

SmallCheck で書いてみよう

では,今度はSmallCheck で書いてみます.と云っても,やることは殆んどかわりません. QuickCheck をインポートしている部分を

import Test.SmallCheck
import Test.SmallCheck.Series

に書き換えて……

test_automaton2 :: Int -> Automaton Int Char -> (N Int -> Bool)
test_automaton2 base auto =
    \(N r) ->
      if r `mod` base == 0
      then isAccepted auto (showBin r)
      else not $ isAccepted auto (showBin r)

とするだけです!殆んど変更になっていません!

WordN Intになっていますね.SmallCheck は Word 型をサポートしていないかわりに,Num 型を N でラップしてやることで,正数しか生成しないようになります.

では,早速試してみましょう.

ghci> smallCheck 1000 $ test_automaton2 6 aDivBy6'
Depth 0:
    Completed 1 test(s) without failure.
Depth 1:
    Completed 2 test(s) without failure.
...
Depth 1000:
    Completed 1001 test(s) without failure.

行が沢山出力されるので時間がかかるかと思いますが,実際には一瞬で終わっています. 先程までと違うところは,quickCheckのかわりにsmallCheckを使っているところでしょうか.また,そのあとに1000と云う引数を渡していますね.これはなんでしょうか?

これは,Depth,つまりデータ型の深さ・大きさです.先にも説明したように,SmallCheck は「深さ」ごとにデータを総当たり的に生成して,それらを全部チェックする,と云う戦略をとっています.深さが何を指すのはデータ型によって異なりますが,整数型の場合は特に最大値だと思えばよいです.smallCheck函数は深さ0から徐々に指定された深さまで増加させていって,包括的に調べる,と云う函数です.特定の深さだけを調べたい場合はdepthCheck函数が使えます.

なので,上のテストでは最大1000までの整数しかチェックできていなくて,ちょっと非効率的です.そこで,深さを最大値ではなくビット長とするように書き換えてみましょう.

data Bit = I | O deriving (Show, Read, Eq)

bitToDigit :: Bit -> Char
bitToDigit I = '1'
bitToDigit O = '0'

instance Serial Bit where
  series = cons0 O \/ cons0 I
  coseries rs d = [ \m -> case m of
                            O -> a
                            I -> b
                  | a <- alts0 rs d
                  , b <- alts0 rs d
                  ]

readBits :: Integral a => String -> a
readBits binary =
  maybe 0 fst $ listToMaybe $ readInt 2 (\c -> c == '0' || c == '1') digitToInt binary

test_automaton3 :: Int -> Automaton Int Char -> [Bit] -> Bool
test_automaton3 q a =
    \bits -> 
      let binary = map bitToDigit bits
          r      = readBin binary
      in if r `mod` q == 0
         then isAccepted a binary
         else not $ isAccepted a binary

BitがBitを表わすデータ型で,その列を生成するように変更していますね.Bitを深さごとにexhaustiveに生成するために,Serial型クラスのインスタンスにしています.型からは一見なにをすればいいのかわかりづらいですが,()Maybe aに対するインスタンス宣言を参考にしつつ,ヘルパ函数を使えば簡単にインスタンスが書けます.series函数は指定の深さのデータを生成する函数で,coseriesは,Bitを含むような別のデータ構造を生成するときに使われます.

test_automaton3では,生成した2進表現を喰わせて,それが6進数であるかどうかとオートマトンに受理されるかどうかが同値であることを確かめているだけですね.

では,確かめてみましょう.

ghci> smallCheck 16 $ test_automaton3 6 aDivBy6'
Depth 0:
  Completed 1 test(s) without failure.
Depth 1:
  Completed 3 test(s) without failure.
...
Depth 15:
  Completed 65535 test(s) without failure.
Depth 16:
  Completed 131071 test(s) without failure.

なんかかなり時間がかかりました.実行してみるとわかりますが,15を越えたあたりから急に遅くなりはじめます.指数爆発だ……. 実際のところどれくらい時間がかかるのか,ちょっと:set +sして測ってみましょう.

ghci> depthCheck 15 $ test_automaton3 6 aDivBy6'
Depth 15:
  Completed 65535 test(s) without failure.
(3.06 secs, 1224982104 bytes)

ghci> depthCheck 16 $ test_automaton3 6 aDivBy6'
Depth 16:
  Completed 131071 test(s) without failure.
(6.45 secs, 2585880856 bytes)

ghci> depthCheck 17 $ test_automaton3 6 aDivBy6'
Depth 17:
  Completed 262143 test(s) without failure.
(13.57 secs, 5465946920 bytes)

うへえ,これはひどい,メモリもかなりくってます.何とか枝刈りをしたいところです.

ここでは,n-bit長の数値を生成しているわけですが,実際には頭に0が沢山ついてるような子,例えば

000101010
010100101

みたいなのも生成しちゃってます.もちろん,こういった入力が来ても大丈夫なチェックにもなっているわけですが,ぶっちゃけ邪魔です. そこで,先頭が 1 であるものだけを判定するようにしてみましょう.

test_automaton4 :: Int -> Automaton Int Char -> [Bit] -> Property
test_automaton4 q a =
    \bits -> 
      let binary = map bitToDigit bits
          r      = maybe 0 fst $ listToMaybe $ readInt 2 (\c -> c == '0' || c == '1') digitToInt binary
      in (not $ null bits) && head bits == I ==>
         if r `mod` q == 0
         then isAccepted a binary
         else not $ isAccepted a binary

実行してみます.

Depth 15:
  Completed 65535 test(s) without failure.
  But 32768 did not meet ==> condition.
(1.71 secs, 659780920 bytes)

ghci> depthCheck 16 $ test_automaton4 6 aDivBy6'
Depth 16:
  Completed 131071 test(s) without failure.
  But 65536 did not meet ==> condition.
(3.56 secs, 1386670368 bytes)

ghci> depthCheck 17 $ test_automaton4 6 aDivBy6'
Depth 17:
  Completed 262143 test(s) without failure.
  But 131072 did not meet ==> condition.
(7.49 secs, 2915713216 bytes)

17bit に 7.49秒です.大分ましにはなりました.これで大体13万までは全部大丈夫,と云えます. 数学の証明にはまるでなりませんが,まあ,この値くらいまで平気であれば多分大丈夫だろう,と云うことにして,納得出来るのではないでしょうか.上限が小さすぎると云う場合は,QuickCheckの方でも乱数チェックをしているのでまあ多分大丈夫!ということで.

結論と補遺

Haskell でプログラムが仕様を満たすかどうかをテストする方法として,QuickCheck と SmallCheck の二つの方法を紹介しました.QuickCheck はランダムテスト,SmallCheck は深さを制限した総当たりテストでした.

SmallCheck には,Lazy SmallCheck と云うバリアントがあって,これは遅延評価を枝刈りに生かした実装になっています. 部分的に定義された値,例えば,

data Tree a = Leaf | Branch (Tree a) a (Tree a)
hoge = Branch (Branch Leaf 12 Leaf) 23 undefined

みたいな値を喰わせることで,最初の幾つかだけ見たら失敗するようなケースは纏めて排除出来ます.例えば,

ghci> isSorted $ 2:1:undefined

みたいなのは,最初の二つだけみれば,もうソート済みでないことはわかるので,これから始まる他の長さのデータももう調べなくて済みます.undefined まで到達したらさらに長いデータを喰わせて,適宜チェックしていくと云う訳です.

これはすごい頭いいんですが,Laziness と云うのはなかなかむずかしくて,リスト全体を読む必要があるような場合だとLazy でない SmallCheck よりも効率がわるくなることがおおいみたいです.例えば,今回の例だと最後までリストを読まなければ倍数かどうかを判定出来ないので,Lazy は使えません.このあたりはまだちゃんと理解していないので,この先ちゃんと調べてみようとおもいます.

授業前の思い付きから予想以上に長くなってしまいました…….そんなこんなで,誰がよむんだ,みたいな感じになってきたところでこの辺で.それでは!


  1. 「ゴルフする」って云うのは,コードゴルフとかのゴルフと同じで、つまりなるべく少なくしよう、と云う意味です.有限オートマトンには最小化アルゴリズムがあるので,それを使えば確実に出来てよいわけですが,そう云うのを知らなくて,ちゃんと動作するかどうかを確かめたい場合を考えます.

  2. ただし,受理状態とそうでない状態は区別しないと駄目です.mod 6 での 0 と 3とか.