恒真式判定は co-NP 完全

コメント欄で id:qnighy が「ソース読んでないけど、たしかisTautってco-NP完全でしたよね」と言っていたのだけどその辺を勉強していないボクとしては何を意図しているのかわけわかめな感じになったので Wikipedia の記事をざっくり読んでみた．まあそれでもどういう意図なんだろう…という疑問は晴れなかったので得たばかりの拙い知識を使って予想してみると，まず充足可能性問題は NP 完全な問題なのでその補題である恒真式判定は co-NP 完全，つまりこの問題は多項式時間では判定できないはずだから式変形で解けるわけがない! ということで良いのかなあ．
まあやぱり式変形での判定は難しそうだなーというのはよく分かっていてたぶんこのプログラムを使っても判定できない論理式もたくさんあると思いますよ．というかさっき自分が試した限りでも (Not (And (And (Or (Var 'x') (Var 'y')) (Or (Not (Var 'x')) (Var 'y'))) (And (Or (Var 'x') (Not (Var 'y'))) (Or (Not (Var 'x')) (Not (Var 'y')))))) がちゃんと判定されなかったりしたので残念ながら昨日のプログラムは不完全のようです．

isTaut

*Main> isTaut (Imply (And (Var 'A') (Var 'B')) (Var 'A'))
Const True
*Main> isTaut (Imply (And (Var 'A') (Not (Var 'A'))) (Const False))
Const True

恒等式かどうか判定するプログラム．これも『プログラミング Haskell』に載っていた例題だけどあっちでは真理値表を使っていたぽくてつまらないので，実際に式を組み換えて判定する物を書いてみた．

data Prop = Const Bool
          | Var Char
          | Not Prop
          | Or Prop Prop
          | And Prop Prop
          | Imply Prop Prop
          deriving (Eq, Ord, Show)


isTaut :: Prop -> Prop

isTaut (Const b) = (Const b)
isTaut (Var x) = (Var x)
isTaut (Not p) = rule (Not (isTaut p))
isTaut (Or p1 p2) = rule (Or (isTaut p1) (isTaut p2))
isTaut (And p1 p2) = rule (And (isTaut p1) (isTaut p2))
isTaut (Imply p1 p2) = rule (Or (isTaut (Not p1)) (isTaut p2))



rule :: Prop -> Prop


rule (Const b) = (Const b)
rule (Not (Const b)) = (Const (not b))
rule (Or (Const b1) (Const b2)) = (Const (b1 || b2))
rule (And (Const b1) (Const b2)) = (Const (b1 && b2))
rule (Imply (Const b1) (Const b2)) = (Const (not b1 && b2))


rule (Var x) = (Var x)


rule (Not (Not p)) = rule p
rule (Not (Or p1 p2)) = rule (And (rule (Not (rule p1))) (rule (Not (rule p2))))
rule (Not (And p1 p2)) = rule (Or (rule (Not (rule p1))) (rule (Not (rule p2))))


rule (Or (Const True) p) = (Const True)
rule (Or p (Const True)) = (Const True)
rule (Or (Const False) p) = p
rule (Or p (Const False)) = p

rule (Or (Not p1) p2) | (rule p1) == (rule p2) = (Const True)
rule (Or p1 (Not p2)) | p1 == p2 = (Const True)
rule (Or p1 p2)       | p1 == p2 = p1

rule (Or (Or p1 p2) p3) | p1 == p3 = rule (Or p2 p3)
                        | p2 == p3 = rule (Or p1 p3)
rule (Or (Or p1 p2) p3) | (p1 == (Not p3) || p2 == (Not p3)) = (Const True)
rule (Or (Or p1 p2) p3) | ((Not p1) == p3 || (Not p2) == p3) = (Const True)

rule (Or p1 (Or p2 p3)) | p1 == p2 = rule (Or p1 p3) 
                        | p1 == p3 = rule (Or p1 p2)
rule (Or p1 (Or p2 p3)) | ((Not p1) == p2 || (Not p1) == p3) = (Const True)
rule (Or p1 (Or p2 p3)) | (p1 == (Not p2) || p1 == (Not p3)) = (Const True)

rule (Or (And p1 p2) p3) | (p1 == p3 || p2 == p3) = p3
rule (Or (And p1 p2) p3) | p1 == (Not p3) = rule (And p2 p3)
                         | p2 == (Not p3) = rule (And p1 p3)
rule (Or p1 (And p2 p3)) | (p1 == p2 || p1 == p3) = p1
rule (Or p1 (And p2 p3)) | (Not p1) == p3 = rule (And p1 p2)
                         | (Not p2) == p3 = rule (And p1 p3)


rule (And (Const False) p) = (Const False)
rule (And p (Const False)) = (Const False)
rule (And (Const True) p) = p
rule (And p (Const True)) = p

rule (And (Not p1) p2) | p1 == p2 = (Const False)
rule (And p1 (Not p2)) | p1 == p2 = (Const False)
rule (And p1 p2) | p1 == p2 = p1

rule (And (And p1 p2) p3) | p1 == p3 = rule (And p2 p3)
                        | p2 == p3 = rule (And p1 p3)
rule (And (And p1 p2) p3) | (p1 == (Not p3) || p2 == (Not p3)) = (Const False)
rule (And (And p1 p2) p3) | ((Not p1) == p3 || (Not p2) == p3) = (Const False)

rule (And p1 (And p2 p3)) | p1 == p2 = rule (And p1 p3) 
                        | p1 == p3 = rule (And p1 p2)
rule (And p1 (And p2 p3)) | ((Not p1) == p2 || (Not p1) == p3) = (Const False)
rule (And p1 (And p2 p3)) | (p1 == (Not p2) || p1 == (Not p3)) = (Const False)

rule (And (Or p1 p2) p3) | (p1 == p3 || p2 == p3) = p3
rule (And (Or p1 p2) p3) | p1 == (Not p3) = rule (Or p2 p3)
                         | p2 == (Not p3) = rule (Or p1 p3)
rule (And p1 (Or p2 p3)) | (p1 == p3 || p1 == p2) = p1
rule (And p1 (Or p2 p3)) | (Not p1) == p3 = rule (Or p1 p2)
                         | (Not p2) == p3 = rule (Or p1 p3)


rule p = p

stackvm

なにやら『プログラミング Haskell』で足し算のみ可能なスタック型 VM を実装していたのを見て，普通に関数を与えられるように改良 (?) してみた．なんとなく要領を掴めてきた…はず…!

data Expr = Const Int
          | OP Op
          | OPCODE Opcode

type Op = (Int, [Int] -> Int)
type Opcode = (Op, [Expr])


eval :: Expr -> Int
eval e = eval_1 e [] []

eval_1 :: Expr -> [Expr] -> [Int] -> Int
eval_1 (Const n)             []     _  = n
eval_1 _                     []     [] = 0
eval_1 (Const n)             (e:s1) s2 = eval_1 e s1 (n:s2)    -- Const
eval_1 (OP (argc, f))        (e:s1) s2 = eval_1 e s1 ((f (take argc s2)):(drop argc s2))    -- Op
eval_1 (OP (argc, f))        []     s2 = f (take argc s2)    -- Op
eval_1 (OPCODE (op, a:args)) s1     s2 = eval_1 a (args ++ ((OP op):s1)) s2    -- Opcode

lifegame

『プログラミング Haskell』を半分程度読み終えたのにコードを一行も書いたことが無いというのは流石にまずいだろうと思ってライフゲームを実装してみた．というかこのライフゲーム自体もプログラムとして書いた経験が無いという事が判明したのですが，大体の場合よく知らない言語で初めて書くプログラムは一度書いたことのあるアルゴリズムだと思うので，なんか得したなーという気分になった．
あとこのプログラム書いてて思ったのが，GHC の吐くエラーメッセージ分かりにくいという事．まあたぶん慣れの問題だと思うけどどうなんだろう…．

data Flag = Live | Dead

type OrderedBoard = [Flag]


gen :: Int -> [(Int, Int)] -> OrderedBoard
gen sidelen pos = map (\(n, _) -> bool_to_flag (elem (n `div` sidelen, n `rem` sidelen) pos)) (zip [0,1..(sidelen^2-1)] (replicate (sidelen^2) Dead))

bool_to_flag :: Bool -> Flag
bool_to_flag True  = Live
bool_to_flag False = Dead


encode :: OrderedBoard -> [Int]
encode board = map encode_1 board

encode_1 :: Flag -> Int
encode_1 Live  = 1
encode_1 Dead  = 0


next_state :: OrderedBoard -> OrderedBoard
next_state board = map (live_or_dead board) (zip [0,1..length board] board)

live_or_dead :: OrderedBoard -> (Int, Flag) -> Flag
live_or_dead board (i, flag) = judge flag (foldl count_live_cell 0 (map (\n -> board !! n) (neighbors (fromEnum (sqrt (fromIntegral (length board)))) i)))

judge :: Flag -> Int -> Flag
judge _    3 = Live
judge Live 2 = Live
judge _    _ = Dead

count_live_cell :: Int -> Flag -> Int
count_live_cell n Live = n + 1
count_live_cell n Dead = n

neighbors :: Int -> Int -> [Int]
neighbors sidelen n = filter (\index -> index >= 0 && index < sidelen^2 && index /= n) (neighbors_1 sidelen n)

neighbors_1 :: Int -> Int -> [Int]
neighbors_1 sidelen n | n < 0                          = []
                      | n > sidelen^2                  = []
                      | n `rem` sidelen == 0           = [n - sidelen, n - sidelen + 1, n, n + 1, n + sidelen, n + sidelen + 1]
                      | n `rem` sidelen == sidelen - 1 = [n - sidelen - 1, n - sidelen, n - 1, n, n + sidelen - 1, n + sidelen]
                      | otherwise                      = [n - sidelen - 1, n - sidelen, n - sidelen + 1, n - 1, n, n + 1, n + sidelen - 1, n + sidelen, n + sidelen + 1]