日々の流転

λ. Wang's Algorithm

ふと、Wang's Algorithm (ワンのアルゴリズム) を素朴に書いてみた。 が、イマイチ。

import Control.Monad (guard,msum)
import Data.List (intersect)
import Data.Maybe (isJust, listToMaybe)

data Formula x
    = Atom x
    | Not   !(Formula x)
    | Imply !(Formula x) !(Formula x)
    | And   !(Formula x) !(Formula x)
    | Or    !(Formula x) !(Formula x)
    deriving Eq

type Sequent x = ([Formula x], [Formula x])

isValid :: Eq x => Sequent x -> Bool
isValid = isJust . isValid'

isValid' :: Eq x => Sequent x -> Maybe ()
isValid' (l,r) =
    do xs <- listToMaybe $ msum $
         [ do let i = intersect l r
              guard $ not $ null i
              return []
         , do (Not p, r) <- pick r
              return [(p:l,r)]
         , do (Not p, l) <- pick l
              return [(l,p:r)]
         , do (Imply p q, r) <- pick r
              return [(p:l,q:r)]
         , do (Or p q, r) <- pick r
              return [(l,p:q:r)]
         , do (And p q, l) <- pick l
              return [(p:q:l,r)]
         , do (Or p q, l)  <- pick l
              return [(p:l,r), (q:l,r)]
         , do (And p q, r) <- pick r
              return [(l,p:r), (l,q:r)]
         , do (Imply p q, l) <- pick l
              return [(q:l,r), (l,p:r)]
         ]
       mapM_ isValid' xs
       return ()

pick :: [x] -> [(x,[x])]
pick []     = []
pick (x:xs) = (x,xs) : [(y,x:ys) | (y,ys) <- pick xs]

λ. IT System: SVG with constraints (CSVG)

メモ。

• <URL:http://www.www2004.org/proceedings/docs/2p310.pdf>
• <URL:http://www.csse.monash.edu.au/~clm/csvg/>

ところで、Googleはすごいなぁ

• google:社外秘 filetype:pdf
• google:部外秘 filetype:pdf
• google:複製不可 filetype:pdf

λ. 『株取引のことがマンガで3時間でマスターできる本』, 木村 佳子

を読んだ。あまり期待してなかったけど、結構良くまとまっていて、基礎知識を得るにはちょうど良かった。

λ. SML#

Zeta版って……(笑