case_studies

Propositions

Consider the following Prop that models propositions (Boolean formulas consisting of Boolean literals, variables, negation, and, or, and implication).

data Prop = Basic Bool | Var Char
          | Not Prop
          | Prop :/\: Prop | Prop :\/: Prop | Prop :=>: Prop

1. Define a function printProp :: Prop -> String which turns the proposition into a printable String.

   printProp :: Prop -> String
   printProp prop = case prop of
                      Basic b    -> show b
                      Var v      -> [v]
                      Not p      -> "not " ++ parensPrintProp p
                      p1 :/\: p2 -> parensPrintProp p1 ++ " /\\ " ++ parensPrintProp p2
                      p1 :\/: p2 -> parensPrintProp p1 ++ " \\/ " ++ parensPrintProp p2
                      p1 :=>: p2 -> parensPrintProp p1 ++ " =>  " ++ parensPrintProp p2
     where
       parens s = "(" ++ s ++ ")"
       parensPrintProp p = parens (printProp p)

2. Define a new printProp' :: Prop -> String which uses as few parentheses as possible. For example, Var 'A' :\/: (Var 'B' :\/: Var 'C') should be printed as A \/ B \/ C.

   Hint: define an auxiliary function printProp'' :: Prop -> (String, LogicalOp) which remembers the top symbol of the formula.

3. Define a function satisfiable :: Prop -> Bool which returns True is the proposition is satisfiable, that is, if there is at least one assignment of truth values to variables which make the proposition true.

   -- Using or :: [Bool] -> Bool
   satisfiable p = or [tv as p | as <- assigns (vars p)]
   -- or using any :: (a -> Bool) -> [a] -> Bool
   satisfiable p = any (\as -> tv as p) (assigns (vars p))

4. Refine the function satisFiable to return the assignment which makes the proposition satisfiable. Which should be the type given to such a function?

   -- we can use the function find :: (a -> Bool) -> [a] -> Maybe a to
   -- return the assignment which makes the proposition true.
   satisfiable :: Prop -> Maybe (Map Char Bool)
   satisfiable = find (\as -> tv as p) (assigns (vars p))

Arithmetic Expressions

Extend the definition of ArithExpr to include exponentiation and factorial functions. How should the evaluation functions change to support them?

data UnArithOp  = Factorial
data BinArithOp = Plus | Minus | Times | Div | Exp

data ArithExpr = Constant Integer
               | Variable Char
               | UnOp  UnArithOp  ArithExpr
               | BinOp BinArithOp ArithExpr ArithExpr

eval :: Map Char Integer -> ArithExpr -> Integer
eval _ (Constant c)  = c
eval m (Variable v)  = fromJust (lookup v m)
eval m (UnOp  o x)   = evalUnOp  o (eval m x)
  where evalUnOp Factorial = \x -> product [1 .. x]
eval m (BinOp o x y) = evalBinOp o (eval m x) (eval m y)
  where evalBinOp Plus  = (+)
        evalBinOp Minus = (-)
        evalBinOp Times = (*)
        evalBinOp Div   = div
        evalBinOp Exp   = (^^)