Propositional Logic

propositional

import Data.Maybe
import qualified Data.HashMap as HM
import Control.Monad
import Test.QuickCheck

--------------------------------------------------------------------------------------------------------------
-- Propositional calculus

data Formula = T
             | F
             | Symbol String
             | Not Formula
             | And Formula Formula
             | Or  Formula Formula
             | Imp Formula Formula
             | Iff Formula Formula
             deriving (Show,Eq)

type KnowledgeBase = [Formula]
data Error = SymbolUndefined String
    deriving (Show)

type MaybeError a = Either Error a
type Model = HM.Map String Bool

reduceKB :: KnowledgeBase -> Model -> MaybeError Bool
reduceKB kb m = (liftM and) $ (mapM (flip reduce m) kb)

reduce :: Formula -> Model -> MaybeError Bool
reduce (T)         _ = Right True
reduce (F)         _ = Right False
reduce (Symbol s)  m = maybe (Left err) (Right) (HM.lookup s m)
    where err = SymbolUndefined s
reduce (Not s)     m = liftM not $ reduce s m
reduce (And s0 s1) m = liftM2 (&&) (reduce s0 m) (reduce s1 m)
reduce (Or  s0 s1) m = liftM2 (||) (reduce s0 m) (reduce s1 m)
reduce (Imp s0 s1) m = liftM2 tt   (reduce s0 m) (reduce s1 m)
    where tt False False = True
          tt False True  = True
          tt True  False = False
          tt True  True  = True
reduce (Iff s0 s1) m = liftM2 tt   (reduce s0 m) (reduce s1 m)
    where tt False False = True
          tt False True  = False
          tt True  False = False
          tt True  True  = True

--------------------------------------------------------------------------------------------------------------
-- Tests using standard equivalences

instance Arbitrary Formula where
    arbitrary = liftM toAtom $ choose (True,False)


toAtom :: Bool -> Formula
toAtom (True ) = T
toAtom (False) = F
getRight :: Either a b -> b
getRight = either (\_ -> error "err") id

r = getRight . (flip reduce HM.empty)

(====) :: Formula -> Formula -> Bool
(====) s0 s1 = r s0 ==  r s1
infixl 1 ====

-- 1-ary equivalences
equivs1 :: [Formula -> Bool]
equivs1 = [-- Double-negation elimination
          \a -> Not ( Not a) ==== a]

-- 2-ary equivalences
equivs2 :: [Formula -> Formula -> Bool]
equivs2 = [ -- Commutativity of AND
           \a b -> a `And` b ==== b `And` a
            -- Commutativity of OR
          ,\a b -> a `Or` b ==== b `Or` a
            -- Contraposition
          ,\a b -> a `Imp` b ==== Not b `Imp` Not a
            -- Implication elimination
          ,\a b -> a `Imp` b ==== Not a `Or` b
            -- Biconditional elimination
          ,\a b -> a `Iff` b ==== ((a `Imp` b) `And` (b `Imp` a))
            -- De Morgan
          ,\a b -> Not (a `And` b) ==== Not a `Or` Not b
            -- De Morgan
          ,\a b -> Not (a `Or` b) ==== Not a `And` Not b]

-- 3-ary equivalences
equivs3 :: [Formula -> Formula -> Formula -> Bool]
equivs3 = [ -- Associativity of AND
           \a b c -> ((a `And` b) `And` c) ==== (a `And` (b `And` c))
            -- Associativity of OR
          ,\a b c -> ((a `Or` b) `Or` c) ==== (a `Or` (b `Or` c))
            -- Distributivity of AND over OR
          ,\a b c -> (a `And` (b `Or` c)) ==== ((a `And` b) `Or` (a `And` c))
            -- Distributivity of OR over AND
          ,\a b c -> (a `Or` (b `And` c)) ==== ((a `Or` b) `And` (a `Or` c))]

runTests :: IO ()
runTests = putStrLn "Running tests of 1-ary equivalences..."
        >> mapM_ quickCheck equivs1
        >> putStrLn ""
        >> putStrLn "Running tests of 2-ary equivalences..."
        >> mapM_ quickCheck equivs2
        >> putStrLn ""
        >> putStrLn "Running tests of 3-ary equivalences..."
        >> mapM_ quickCheck equivs3
        >> putStrLn ""
        >> putStrLn "Done."