論理式を論理和標準形や論理積標準形にするやつ

logical-normal-form.hs

module Main where

data Exp = Var String
         | And Exp Exp
         | Or Exp Exp
         | Imp Exp Exp
         | Not Exp
  deriving Eq

instance Show Exp where
  show (Var a) = a
  show (And a b) = "(" ++ show a ++ " ∧  " ++ show b ++ ")"
  show (Or a b) = "(" ++ show a ++ " ∨  " ++ show b ++ ")"
  show (Imp a b) = "(" ++ show a ++ " ⊃  " ++ show b ++ ")"
  show (Not a) = "¬" ++ show a

removeInp :: Exp -> Exp
removeInp a@(Var _) = a
removeInp (And a b) = removeInp a `And` removeInp b
removeInp (Or a b) = removeInp a `Or` removeInp b
removeInp (Imp a b) = Not (removeInp a) `Or` removeInp b
removeInp (Not a) = Not (removeInp a)

deMorgan :: Exp -> Exp
deMorgan a@(Not (Var _)) = a
deMorgan (Not (And a b)) = deMorgan (Not a) `Or` deMorgan (Not b)
deMorgan (Not (Or a b)) = deMorgan (Not a) `And` deMorgan (Not b)
deMorgan (Not (Not a)) = Not . Not . deMorgan $ a
deMorgan (Not (Imp _ _)) = error "imp: deMorgan"
deMorgan a@(Var _) = a
deMorgan (And a b) = deMorgan a `And` deMorgan b
deMorgan (Or a b) = deMorgan a `Or` deMorgan b

removeNot :: Exp -> Exp
removeNot a@(Var _) = a
removeNot (And a b) = And (removeNot a) (removeNot b)
removeNot (Or a b) = Or (removeNot a) (removeNot b)
removeNot (Imp _ _) = error "imp: removeNot"
removeNot (Not (Not a)) = removeNot a
removeNot (Not a) = Not . removeNot $ a

--Disjunctive normal form
dnf :: Exp -> Exp
dnf a@(Var _) = a
dnf (And x y) =
  case (dnf x, dnf y) of
    (Or a b, Or c d) -> (a `And` c) `Or` (b `And` c) `Or` (a `And` d) `Or` (b `And` d)
    (a, Or b c) -> And a b `Or` And a c
    (Or a b, c) -> And c a `Or` And c b
    (a, b) -> And a b
dnf (Or a b) = dnf a `Or` dnf b
dnf (Imp _ _) = error "imp: dnf"
dnf a@(Not _) = a


-- Conjunctive normal form
cnf :: Exp -> Exp
cnf a@(Var _) = a
cnf (And a b) = cnf a `And` cnf b
cnf (Or x y) =
  case (cnf x, cnf y) of
    (And a b, And c d) -> (a `Or` c) `And` (b `Or` c) `And` (a `Or` d) `Or` (b `And` d)
    (a, And b c) -> Or b c `And` Or a c
    (And a b, c) -> Or c a `And` Or c b
    (a, b) -> Or a b
cnf (Imp _ _) = error "imp: dnf"
cnf a@(Not _) = a

toDNF :: Exp -> Exp
toDNF = dnf . removeNot . deMorgan . removeInp

toCNF :: Exp -> Exp
toCNF = cnf . removeNot . deMorgan . removeInp

• 正しい結果になるかよくわからない
• 結果にp ∧ pなどが含まれる可能性あり
• GADTを使うと静的にチェックできることが増えるはず