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.

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.

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?

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?