Tonλ's blog May the λ be with you

To follow the path:
look to the master,
follow the master,
walk with the master,
see through the master,
become the master.

PIH - ch10 - 2/3 - Declaring types and classes - exercises

by @ardumont on 01 May 2013

Here is the second part of the exercise from the chapter 10. The first part is here.

Tautology

Extend the tautology checker to support the use of logical disjunction (v) and equivalence (<=>) in propositions.

Here are the adaptation to the Prop definition regarding the logical disjunction, and the equivalence: 

data Prop = Const Bool
          | Var Char
          | Not Prop
          | And Prop Prop
          | Imply Prop Prop
          | Or Prop Prop
          | Equiv Prop Prop
          deriving Show

Here are some examples: 

p0 :: Prop
p0 = And (Var 'A') (Var 'B')

p1 :: Prop
p1 = And (Var 'A') (Not (Var 'A'))

p2 :: Prop
p2 = Imply (And (Var 'A') (Var 'B')) (Var 'A')

p3 :: Prop
p3 = Imply (Var 'A') (And (Var 'A') (Var 'B'))

p4 :: Prop
p4 = Imply (And (Var 'A') (Imply
      (Var 'A') (Var 'B'))) (Var 'B')

p5 :: Prop
p5 = Or (Var 'A') (And (Var 'B') (Var 'C'))

p6 :: Prop
p6 = Equiv (Var 'a') (Var 'b')

p7 :: Prop
p7 = Not p6

p8 :: Prop
p8 = Imply p6 p7

p9 :: Prop
p9 = Equiv (Var 'A') (And (Var 'B') (Var 'C'))

This impacts the eval function, we just add the 2 new definitions: 

type Subst = Assoc Char Bool

eval :: Subst -> Prop -> Bool
eval _ (Const b)   = b
eval s (Var v)     = find v s
eval s (Not b)     = not $ eval s b
eval s (And a b)   = eval s a && eval s b
eval s (Imply a b) = eval s a <= eval s b
eval s (Or a b)    = eval s a || eval s b
eval s (Equiv a b) = eval s $ And (Imply a b) (Imply b a)

We also need to compute the possible variables on the Prop: 

vars :: Prop -> [Char]
vars (Const _)   = []
vars (Var v)     = [v]
vars (Not b)     = vars b
vars (And a b)   = vars a ++ vars b
vars (Or a b)    = vars a ++ vars b
vars (Imply a b) = vars a ++ vars b
vars (Equiv a b) = vars a ++ vars b

Some output: 

*Ch10> vars p1
"AA"
*Ch10> vars p2
"ABA"
*Ch10> vars p3
"AAB"
*Ch10> vars p4
"AABB"
*Prop> vars p5
"ABC"

Here is the remaining code: 

bools :: Int -> [[Bool]]
bools 0 = [[]]
bools 1 = [[True], [False]]
bools n = map (False:) bn ++ map (True:) bn
          where bn = bools (n-1)

-- *Ch10> bools 0
-- []
-- *Ch10> bools 1
-- [[True],[False]]
-- *Ch10> bools 2
-- [[False,True],[False,False],[True,True],[True,False]]
-- *Ch10> bools 3
-- [[False,False,True],[False,False,False],[False,True,True],[False,True,False],[True,False,True],[True,False,False],[True,True,True],[True,True,False]]

substs :: Prop -> [Subst]
substs p = map (zip vs) (bools (length vs))
  where vs = rmdups (vars p)

-- *Prop> substs p1
-- [[('A',True)],[('A',False)]]
-- *Prop> substs p2
-- [[('A',False),('B',True)],[('A',False),('B',False)],[('A',True),('B',True)],[('A',True),('B',False)]]
-- *Prop> substs p3
-- [[('A',False),('B',True)],[('A',False),('B',False)],[('A',True),('B',True)],[('A',True),('B',False)]]
-- *Prop> substs p4
-- [[('A',False),('B',True)],[('A',False),('B',False)],[('A',True),('B',True)],[('A',True),('B',False)]]

isTaut :: Prop -> Bool
isTaut p = and [ eval s p | s <- substs p ]

Some output examples: 

*Prop> isTaut $ Or (Var 'a') (Not (Var 'a'))
True
*Prop> isTaut $ Or (Var 'a') (Var 'a')
False
*Prop> isTaut $ Equiv (Var 'a') (Not (Var 'a'))
False
*Prop> isTaut $ Equiv (Var 'a') (Var 'a')
True
*Prop> isTaut $ Equiv (Var 'a') (Var 'b')
False

Interactive tautology checker

Using the function isTaut together with the parsing and interaction libraries from the previous two chapters, define an interactive tautology checker that allows propositions to be entered from the keyboard in a user-friendly syntax.

Hint: Build a parser for propositions by modifying the parser for arithmetic expressions given in chapter 8.

Recall the definition of the Prop type: 

data Prop = Const Bool
          | Var Char
          | Not Prop
          | And Prop Prop
          | Imply Prop Prop
          | Or Prop Prop
          | Equiv Prop Prop
          deriving Show

And now, the program, we first define the module and import the needed library: 

module PropParsers where

import Parsers
import Prop

Then, to solve such problem, we created a parser of type Parser Prop. Here is the main parser (as haskell is compiled, we can use the other parsers even though they are not yet defined): 

prop :: Parser Prop
prop = propConst +++
         propVar +++
         propNot +++
         propAnd +++
         propOr  +++
         propImply +++
         propEquiv

To simplify the writing, we define 't' and 'f' as the symbol for True and False: 

mapBool :: [(String, Bool)]
mapBool = [("t", True), ("f", False)]

propConst :: Parser Prop
propConst = do b <- symbol "t" +++ symbol "f"
               let bool = (lookup b mapBool) in
                 case bool of
                   Just v -> return $ Const v

Possible output: 

*PropParsers> parse propConst "t"
[(Const True,"")]
*PropParsers> parse propConst "f"
[(Const False,"")]
*PropParsers> parse propConst "a"
[]

Var (just a char): 

propVar :: Parser Prop
propVar = do l <- token letter
             return $ Var l

Possible output: 

*PropParsers> parse propVar "a"
[(Var 'a',"")]
*PropParsers> parse propVar "t"
[(Var 't',"")]
*PropParsers> parse propVar "na"
[(Var 'n',"a")]
*PropParsers> parse propVar "1"
[]

not (!): 

propNot :: Parser Prop
propNot = do symbol "!"
             a <- prop
             return (Not a)

Output: 

*PropParsers> parse propNot "! a"
[(Not (Var 'a'),"")]
*PropParsers> parse propNot "! asldfsd"
[(Not (Var 'a'),"sldfsd")]
*PropParsers> parse propNot "! t"
[(Not (Const True),"")]
*PropParsers> parse propNot " t"
[]

and (&): 

propAnd :: Parser Prop
propAnd = do symbol "&"
             a <- prop
             b <- prop
             return (And a b)

Output: 

*PropParsers> parse propAnd "& a b"
[(And (Var 'a') (Var 'b'),"")]
*PropParsers> parse propAnd "& a ! b"
[(And (Var 'a') (Not (Var 'b')),"")]
*PropParsers> parse propAnd "& a ! t"
[(And (Var 'a') (Not (Const True)),"")]
*PropParsers> parse propAnd "& a ! t"
[(And (Var 'a') (Not (Const True)),"")]
*PropParsers> parse propAnd "& a "
[]

Or (|): 

propOr :: Parser Prop
propOr = do symbol "|"
            a <- prop
            b <- prop
            return (Or a b)

Output: 

*PropParsers> parse propOr "| a "
[]
*PropParsers> parse propOr "| a b"
[(Or (Var 'a') (Var 'b'),"")]
*PropParsers> parse propOr "| a ! b"
[(Or (Var 'a') (Not (Var 'b')),"")]
*PropParsers> parse propOr "| t ! b"
[(Or (Const True) (Not (Var 'b')),"")]
*PropParsers> parse propOr "| t ! & a c"
[(Or (Const True) (Not (And (Var 'a') (Var 'c'))),"")]

Imply (=>): 

propImply :: Parser Prop
propImply = do symbol "=>"
               a <- prop
               b <- prop
               return (Imply a b)

Output: 

*PropParsers> parse propImply "=> t ! & a c"
[(Imply (Const True) (Not (And (Var 'a') (Var 'c'))),"")]
*PropParsers> parse propImply "=> t "
[]

Equivalence (<=>): 

propEquiv :: Parser Prop
propEquiv = do symbol "<=>"
               a <- prop
               b <- prop
               return (Equiv a b)

Output: 

*PropParsers> parse propEquiv "<=> t "
[]
*PropParsers> parse propEquiv "<=> t ! & a c"
[(Equiv (Const True) (Not (And (Var 'a') (Var 'c'))),"")]

The main evaluation program that will wrap the resulting of evaluating the expression into a Maybe Prop. If the evaluation fails, this will return Nothing. Otherwise, return Just the proposition successfully parsed. 

propEval :: String -> (Maybe Prop)
propEval s = case parse prop s of
  [(p, "")] -> Just p
  _         -> Nothing

*PropParsers> propEval "f"
Just (Const False)
*PropParsers> propEval "f"
Just (Const False)
*PropParsers> propEval "! f"
Just (Not (Const False))
*PropParsers> propEval "! a"
Just (Not (Var 'a'))
*PropParsers> propEval "& ! a b"
Just (And (Not (Var 'a')) (Var 'b'))
*PropParsers> propEval "& ! a t"
Just (And (Not (Var 'a')) (Const True))
*PropParsers> propEval "& ! a <=> t f"
Just (And (Not (Var 'a')) (Equiv (Const True) (Const False)))

At last, the main program which is in charge of asking the user for a proposition. This will check the input, if incorrect, this will relaunch the main program. Or else, this will check if it's a tautology. It it is, this will print "tautology!", otherwise "not a tautology!" and relaunch the main program. 

prompt :: [String]
prompt = ["keywords: &, !, t, f, =>, <=>, and any other character",
          "Enter a Proposition:"]

askUser :: IO ()
askUser =
    do mapM_ putStrLn prompt
       p <- getLine
       let r = propEval p in
         do putStrLn (case r of
                         Just v -> (if isTaut v
                                    then "tautology!"
                                    else "Not a tautology!")
                         _    ->  "Invalid input!")
            askUser

main :: IO ()
main = askUser

Here is a run sample output: 

*PropParsers> main
keywords: &, !, t, f, =>, <=>, and any other character
Enter a Proposition:
a
Not a tautology!
keywords: &, !, t, f, =>, <=>, and any other character
Enter a Proposition:
b
Not a tautology!
keywords: &, !, t, f, =>, <=>, and any other character
Enter a Proposition:
t
tautology!
keywords: &, !, t, f, =>, <=>, and any other character
Enter a Proposition:
f
Not a tautology!
keywords: &, !, t, f, =>, <=>, and any other character
Enter a Proposition:
! f
tautology!
keywords: &, !, t, f, =>, <=>, and any other character
Enter a Proposition:
& t t
tautology!
keywords: &, !, t, f, =>, <=>, and any other character
Enter a Proposition:
& t ! f
tautology!
keywords: &, !, t, f, =>, <=>, and any other character
Enter a Proposition:
| a ! a
tautology!
keywords: &, !, t, f, =>, <=>, and any other character
Enter a Proposition:
| a ! b
Not a tautology!
keywords: &, !, t, f, =>, <=>, and any other character
Enter a Proposition:

Latest posts

About updating org-trello tutorials (2020-05-10)
It's time for an update
org-trello debug tools (2015-09-06)
org-trello debugging tools
Atreus keyboard (2015-02-26)
My Atreus keyboard journey
Feedback loop (2014-12-21)
Later is too late!
Feedback loop (2014-12-21)
Later is too late!