Case studies

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 atHome

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 atHome

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 atHome

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 atHome

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))

5 atHome

Recall the following definitions for the ArithExpr type we used in class:

data ArithOp = Plus | Minus | Times | Div deriving Show

data ArithExpr = Constant Integer
               | Variable Char
               | Op ArithOp ArithExpr ArithExpr
               deriving Show

Extend the definition of ArithExpr to include exponentiation and factorial functions. How should the evaluation function eval :: Map Char Integer -> ArithExpr -> Integer 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   = (^^)