Subject: Re: COSC 470 assignment

From: Jon Edwards <[email-masked]>
Date: Thu, 01 Nov 2001 20:14:53 +1300

"Richard A. O'Keefe" wrote:

> The office don't seem to have a record of your mark for the last 470
> assignment.  Did you hand it in?  Did I mark it?  What mark did I give you?

I certainly handed it in, and you looked at it, but I'm not sure what mark you
gave for it, if any.  I heard some conflicting stories about what was
required, so I wasn't sure for a while if what I had handed in had been
appropriate, as you may recall.

Attached is a copy of what I originally handed in (via email - I didn't hand
anything in on paper), unchanged apart from the addition of Jonathan
Pengelly's test cases.

Cheers,
Jon Edwards

module DNF
where

import List
import Maybe (fromJust)

-- Direct representation of a boolean expression.
data BE vn
   = F
   | T
   | Var vn
   | Not (BE vn)
   | And (BE vn) (BE vn)
   | Or  (BE vn) (BE vn)
   | Imp (BE vn) (BE vn)
   | Eqv (BE vn) (BE vn)
   deriving (Eq, Read, Show)
type BE1 = BE Int

{- Representation of a boolean expression as a disjunction of conjunctions,
 -  i.e. in disjunctive normal form (DNF).
 - Note that this isn't really a `normal form', in the sense that two expressions in this
 -  form can be equivalent but not equal.  I was unsure and a little surprised by this,
 -  but have verified it with a couple of sources.
 - The Bool values indicate whether the associated variable appears unnegated.
 - The variable names are expected to be drawn from an instance of Ord, and to appear in ascending order
 -  in each clause (for processing efficiency).
 - No ordering is required for the clauses themselves.
 -}
type DNF vn = [[(vn,Bool)]]

{- Find a model for the given expression, if there is one.
 - The result is expressed as an association list of variables and truth value assignments.
 -}
find_model :: (Ord vn) => BE vn -> Maybe [(vn,Bool)]
find_model e = (fmap f) res
 where res = (unless_null head) (disjunctive_form e)   -- benefits (greatly!) from lazy evaluation
       f t = map (\v -> (v,default_to False (lookup v t))) (vars e)

default_to :: a -> Maybe a -> a
default_to d = maybe d id

-- List the variables appearing in an expression, in order.
vars :: (Ord vn) => BE vn -> [vn]
vars e = case e  of
           (Var vn)  -> [vn]
           (Not e)   -> vars e
           (And e f) -> g e f
           (Or  e f) -> g e f
           (Imp e f) -> g e f
           (Eqv e f) -> g e f
           _         -> []
         where g e f = uniq (merge (vars e) (vars f))

{- Check that the model finder gives a correct result if it gives a positive result.
 - This is not a conclusive check of correctness, as it doesn't deal with the situation
 -  where no model is found but one exists.  But it's a useful check nevertheless.
 -}
check_positive :: (Ord vn) => BE vn -> Bool
check_positive e = case res  of
                     Nothing  -> True
                     Just t   -> eval e t
 where res = find_model e

-- Evaluates an expression with the given variable assignments.
eval :: (Ord vn) => BE vn -> [(vn,Bool)] -> Bool
eval F _         = False
eval T _         = True
eval (Var vn)  t = fromJust (lookup vn t)
eval (Not e)   t = not (eval e t)
eval (And e f) t = eval e t && eval f t
eval (Or  e f) t = eval e t || eval f t
eval (Imp e f) t = not (eval e t) || eval f t
eval (Eqv e f) t = eval e t == eval f t

{- Return an expression equivalent to that given, in disjunctive normal form (DNF).
 - Does not perform a subsumption check, as this impedes progress for the immediate
 -  purpose of a finding a single model (as does being a computer geek 8-\).
 -  When a model is found, it can be used straight away rather than waiting to see
 -  if a more general expression of that model (i.e. a subsuming one) can be found.
 - Also, the result may contain simplifyable (or even tautological) pairs of clauses,
 -  for example:
 -
 -  (A and B) or (~A and B)
 -
 - Neither this, nor the lack of subsumption checking, prevents the result from being
 -   considered to be in DNF.
 -}
disjunctive_form :: (Ord vn) => BE vn -> DNF vn
disjunctive_form e = case e'  of
          T    -> [[]]
          F    -> []
          e''  -> dis_from_matrix . matrix_form $ e''
 where e' = simplify . basic_ops $ e

-- Return an expression equivalent to that given, using only `And', `Or' and `Not'.
basic_ops :: (Ord vn) => BE vn -> BE vn
basic_ops (Not e)   = Not (basic_ops e)
basic_ops (And e f) = And (basic_ops e) (basic_ops f)
basic_ops (Or  e f) = Or  (basic_ops e) (basic_ops f)
basic_ops (Imp e f) = Or  (Not (basic_ops e)) (basic_ops f)
basic_ops (Eqv e f) = basic_ops (And (Imp e f) (Imp f e))
basic_ops e         = e

-- Return an expression equivalent to that given, without constant truth values,
--  except perhaps the entire expression.
-- The argument is assumed to use only `And', `Or' and `Not'.
simplify :: (Ord vn) => BE vn -> BE vn
simplify T       = T
simplify F       = F
simplify (Var v) = Var v
simplify (Not e) = case (simplify e) of
                     T        -> F
                     F        -> T
                     (Not e') -> e'
                     e'       -> Not e'
simplify (And e f) = case (e',f') of
                       (F,_) -> F
                       (_,F) -> F
                       (T,g) -> g
                       (g,T) -> g
                       (g,h) -> And g h
                     where (e',f') = (simplify e,simplify f)
simplify (Or  e f) = case (e',f') of
                       (T,_) -> T
                       (_,T) -> T
                       (F,g) -> g
                       (g,F) -> g
                       (g,h) -> Or g h
                     where (e',f') = (simplify e,simplify f)

-- Return an expression equivalent to that given, except that `Not' is only applied to variables.
-- The argument is assumed to use only `And', `Or' and `Not', and variables.
matrix_form :: (Ord vn) => BE vn -> BE vn
matrix_form (And e f)       = And (matrix_form e) (matrix_form f)
matrix_form (Or  e f)       = Or  (matrix_form e) (matrix_form f)
matrix_form (Not (Not e))   = matrix_form e
matrix_form (Not (And e f)) = matrix_form (Or  (Not (matrix_form e)) (Not (matrix_form f)))
matrix_form (Not (Or  e f)) = matrix_form (And (Not (matrix_form e)) (Not (matrix_form f)))
matrix_form (Not (Var v))   = Not (Var v)
matrix_form (Var v)         = Var v

-- Return an expression equivalent to that given, in disjunctive form.
-- The argument is assumed to be in the form returned by `matrix_form'.
-- No self-contradictory clauses are included in the result.
dis_from_matrix :: (Ord vn) => BE vn -> DNF vn
dis_from_matrix (Var v)       = [[(v,True)]]
dis_from_matrix (Not (Var v)) = [[(v,False)]]
dis_from_matrix (And e f)
 = nub [clause_and a b | a <- dis_from_matrix e, b <- dis_from_matrix f, not (a `contradicts` b)]
dis_from_matrix (Or e f) = nub (dis_from_matrix e ++ dis_from_matrix f)

clause_and :: (Ord vn) => [(vn,Bool)] -> [(vn,Bool)] -> [(vn,Bool)]
clause_and a b = uniq (mergeOn fst a b)

-- Indicate whether the conjunction of the given two clauses forms a contradiction,
--  assuming that neither clause contradicts itself.
contradicts :: (Ord vn) => [(vn,Bool)] -> [(vn,Bool)] -> Bool
contradicts a b = any (\(v,s) -> (v,not s) `elem` b) a

{- Some supporting functions.
 -}

-- As per Unix.
uniq :: (Eq a) => [a] -> [a]
uniq = map head . group

-- Test whether the set of elements in the first list is a subset of the elements in the second.
subset :: (Eq a) => [a] -> [a] -> Bool
subset a b = a == intersect a b

unless_null :: ([a] -> b) -> [a] -> Maybe b
unless_null = apply_unless null

apply_unless :: (a -> Bool) -> (a -> b) -> a -> Maybe b
apply_unless p f x
 | p x        = Nothing
 | otherwise  = Just (f x)

-- Merge two sorted lists.  Elements comparing equal come from the first list first.
merge :: (Ord a) => [a] -> [a] -> [a]
merge = mergeBy (<)

-- Merge two sorted lists, with the given strict comparison.
mergeBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]
mergeBy _ as [] = as
mergeBy _ [] bs = bs
mergeBy (<) as@(a:as') bs@(b:bs')
 | b < a      = b : mergeBy (<) as  bs'
 | otherwise  = a : mergeBy (<) as' bs

-- Merge two sorted lists, extracting the sort key with the given function.
mergeOn :: (Ord k) => (a -> k) -> [a] -> [a] -> [a]
mergeOn kf = mergeOnBy kf (<)

{- Merge two sorted lists, extracting the sort key with the given function, ordering
 -  with the given strict comparison.
 -}
mergeOnBy :: (a -> k) -> (k -> k -> Bool) -> [a] -> [a] -> [a]
mergeOnBy kf (<) = mergeBy lt
 where a `lt` b = kf a < kf b

{- Some sample output, using the test cases that follow:

   ___         ___ _
  / _ \ /\  /\/ __(_)
 / /_\// /_/ / /  | |      GHC Interactive, version 5.00.2, For Haskell 98.
/ /_\\/ __  / /___| |      http://www.haskell.org/ghc/
\____/\/ /_/\____/|_|      Type :? for help.
 
Loading package std ... linking ... done.
Prelude> :load dnf
Compiling DNF              ( dnf.hs, interpreted )
Ok, modules loaded: DNF.
DNF> (sequence . map (print . find_model . tc)) [1..9]
Just [(1,True)]
Just [(1,True)]
Just [(1,True),(2,False)]
Just [(1,False)]
Just [(1,False),(2,False),(3,False),(4,False),(5,False),(6,False),(7,False),(8,False),(9,False),(10,False),(11,False),(12,False),(13,False),(14,False),(15,False),(16,False),(17,False),(18,False),(19,False),(20,False)]
Just [(5,False),(6,False),(7,False),(8,False),(9,True),(10,False),(11,False),(12,True),(13,False),(14,False),(15,False),(16,False),(17,False),(18,False),(19,False),(20,False)]
Just [(1,True),(2,False),(3,False)]
Just [(1,True),(2,True),(3,True),(4,True),(5,True),(6,True),(7,True),(8,True),(9,True),(10,True),(11,True),(12,True),(13,True),(14,True),(15,True),(16,True)]
Just [(1,True),(2,False),(3,False),(4,False),(5,False),(6,False),(7,False),(8,False),(9,False),(10,False),(11,False),(12,False),(13,False),(14,False),(15,False),(16,False)]
DNF> all (check_positive . tc) [1..9]
True

-}

{- Here are some test cases (the same ones as supplied in the robdd.hs example) -}

tc :: Int -> BE1
tc 1 = (Var 1)
tc 2 = (Or (Var 1) (Var 1))
tc 3 = (Eqv (Imp (Var 1) (Var 2)) (Or (Not (Var 1)) (Var 2)))
tc 4 = (Eqv (And (Var 1) (Var 1)) (Var 1))
tc 5 = (And (And (And (Eqv (Var 13) (Or (And F (Var 1)) (Or (And F (Var
        5)) (And (Var 1) (Var 5))))) (Eqv (Var 9) (Eqv (Eqv F (Not (Var
        1))) (Not (Var 5))))) (And (And (Eqv (Var 14) (Or (And (Var 13)
        (Var 2)) (Or (And (Var 13) (Var 6)) (And (Var 2) (Var 6)))))
        (Eqv (Var 10) (Eqv (Eqv (Var 13) (Not (Var 2))) (Not (Var 6)))))
        (And (And (Eqv (Var 15) (Or (And (Var 14) (Var 3)) (Or (And (Var
        14) (Var 7)) (And (Var 3) (Var 7))))) (Eqv (Var 11) (Eqv (Eqv
        (Var 14) (Not (Var 3))) (Not (Var 7))))) (And (Eqv (Var 16) (Or
        (And (Var 15) (Var 4)) (Or (And (Var 15) (Var 8)) (And (Var 4)
        (Var 8))))) (Eqv (Var 12) (Eqv (Eqv (Var 15) (Not (Var 4))) (Not
        (Var 8)))))))) (And (And (And (Eqv (Var 17) (Or (And (Not F)
        (And (Var 1) (Var 5))) (And F (Or (Var 1) (Var 5))))) (Eqv (Var
        9) (Or (And F (And (Var 1) (Var 5))) (Or (And F (And (Not (Var
        1)) (Not (Var 5)))) (Or (And (Not F) (And (Var 1) (Not (Var
        5)))) (And (Not F) (And (Not (Var 1)) (Var 5)))))))) (And (And
        (Eqv (Var 18) (Or (And (Not (Var 17)) (And (Var 2) (Var 6)))
        (And (Var 17) (Or (Var 2) (Var 6))))) (Eqv (Var 10) (Or (And
        (Var 17) (And (Var 2) (Var 6))) (Or (And (Var 17) (And (Not (Var
        2)) (Not (Var 6)))) (Or (And (Not (Var 17)) (And (Var 2) (Not
        (Var 6)))) (And (Not (Var 17)) (And (Not (Var 2)) (Var 6))))))))
        (And (And (Eqv (Var 19) (Or (And (Not (Var 18)) (And (Var 3)
        (Var 7))) (And (Var 18) (Or (Var 3) (Var 7))))) (Eqv (Var 11)
        (Or (And (Var 18) (And (Var 3) (Var 7))) (Or (And (Var 18) (And
        (Not (Var 3)) (Not (Var 7)))) (Or (And (Not (Var 18)) (And (Var
        3) (Not (Var 7)))) (And (Not (Var 18)) (And (Not (Var 3)) (Var
        7)))))))) (And (Eqv (Var 20) (Or (And (Not (Var 19)) (And (Var
        4) (Var 8))) (And (Var 19) (Or (Var 4) (Var 8))))) (Eqv (Var 12)
        (Or (And (Var 19) (And (Var 4) (Var 8))) (Or (And (Var 19) (And
        (Not (Var 4)) (Not (Var 8)))) (Or (And (Not (Var 19)) (And (Var
        4) (Not (Var 8)))) (And (Not (Var 19)) (And (Not (Var 4)) (Var
        8))))))))))) (Eqv (Var 16) (Var 20))))
tc 6 = (And (And (And (Eqv (Var 13) (Or (And F T) (Or (And F (Var 5))
        (And T (Var 5))))) (Eqv (Var 9) (Eqv (Eqv F (Not T)) (Not (Var
        5))))) (And (And (Eqv (Var 14) (Or (And (Var 13) F) (Or (And
        (Var 13) (Var 6)) (And F (Var 6))))) (Eqv (Var 10) (Eqv (Eqv
        (Var 13) (Not F)) (Not (Var 6))))) (And (And (Eqv (Var 15) (Or
        (And (Var 14) F) (Or (And (Var 14) (Var 7)) (And F (Var 7)))))
        (Eqv (Var 11) (Eqv (Eqv (Var 14) (Not F)) (Not (Var 7))))) (And
        (Eqv (Var 16) (Or (And (Var 15) T) (Or (And (Var 15) (Var 8))
        (And T (Var 8))))) (Eqv (Var 12) (Eqv (Eqv (Var 15) (Not T))
        (Not (Var 8)))))))) (And (And (And (Eqv (Var 17) (Or (And (Not
        F) (And T (Var 5))) (And F (Or T (Var 5))))) (Eqv (Var 9) (Or
        (And F (And T (Var 5))) (Or (And F (And (Not T) (Not (Var 5))))
        (Or (And (Not F) (And T (Not (Var 5)))) (And (Not F) (And (Not
        T) (Var 5)))))))) (And (And (Eqv (Var 18) (Or (And (Not (Var
        17)) (And F (Var 6))) (And (Var 17) (Or F (Var 6))))) (Eqv (Var
        10) (Or (And (Var 17) (And F (Var 6))) (Or (And (Var 17) (And
        (Not F) (Not (Var 6)))) (Or (And (Not (Var 17)) (And F (Not (Var
        6)))) (And (Not (Var 17)) (And (Not F) (Var 6)))))))) (And (And
        (Eqv (Var 19) (Or (And (Not (Var 18)) (And F (Var 7))) (And (Var
        18) (Or F (Var 7))))) (Eqv (Var 11) (Or (And (Var 18) (And F
        (Var 7))) (Or (And (Var 18) (And (Not F) (Not (Var 7)))) (Or
        (And (Not (Var 18)) (And F (Not (Var 7)))) (And (Not (Var 18))
        (And (Not F) (Var 7)))))))) (And (Eqv (Var 20) (Or (And (Not
        (Var 19)) (And T (Var 8))) (And (Var 19) (Or T (Var 8))))) (Eqv
        (Var 12) (Or (And (Var 19) (And T (Var 8))) (Or (And (Var 19)
        (And (Not T) (Not (Var 8)))) (Or (And (Not (Var 19)) (And T (Not
        (Var 8)))) (And (Not (Var 19)) (And (Not T) (Var 8)))))))))))
        (Eqv (Var 16) (Var 20))))
tc 7 = Eqv (Not (Or (Var 1) (Or (Var 2) (Var 3))))
           (And (Not (Var 1)) (And (Not (Var 2)) (Not (Var 3)) ))
tc 8 = (Eqv (Not (And (Var 1) (And (Var 2) (And (Var 3) (And (Var 4)
        (And (Var 5) (And (Var 6) (And (Var 7) (And (Var 8) (And (Var 9)
        (And (Var 10) (And (Var 11) (And (Var 12) (And (Var 13) (And
        (Var 14) (And (Var 15) (Var 16))))))))))))))))) (Or (Not (Var
        1)) (Or (Not (Var 2)) (Or (Not (Var 3)) (Or (Not (Var 4)) (Or
        (Not (Var 5)) (Or (Not (Var 6)) (Or (Not (Var 7)) (Or (Not (Var
        8)) (Or (Not (Var 9)) (Or (Not (Var 10)) (Or (Not (Var 11)) (Or
        (Not (Var 12)) (Or (Not (Var 13)) (Or (Not (Var 14)) (Or (Not
        (Var 15)) (Not (Var 16))))))))))))))))))
tc 9 = (Eqv (Not (Or (Var 1) (Or (Var 2) (Or (Var 3) (Or (Var 4) (Or
        (Var 5) (Or (Var 6) (Or (Var 7) (Or (Var 8) (Or (Var 9) (Or (Var
        10) (Or (Var 11) (Or (Var 12) (Or (Var 13) (Or (Var 14) (Or (Var
        15) (Var 16))))))))))))))))) (And (Not (Var 1)) (And (Not (Var
        2)) (And (Not (Var 3)) (And (Not (Var 4)) (And (Not (Var 5))
        (And (Not (Var 6)) (And (Not (Var 7)) (And (Not (Var 8)) (And
        (Not (Var 9)) (And (Not (Var 10)) (And (Not (Var 11)) (And (Not
        (Var 12)) (And (Not (Var 13)) (And (Not (Var 14)) (And (Not (Var
        15)) (Not (Var 16))))))))))))))))))

-- Test cases 10 to 21 were provided by Jonathan Pengelly
tc 10 = (And (Var 1) (Not (Var 1)))
tc 11 = (Or (And (Var 1) (Not (Var 2))) (And (Not (Var 1)) (Var 2)))
-- Modus Ponens test
tc 12 = (And (And (Var 1) (Imp (Var 1) (Var 2))) (Not (Var 2)))
-- Modus Tollens test
tc 13 = (And (And (Not (Var 2)) (Imp (Var 1) (Var 2))) (Var 1))
-- Double negation test
tc 14 = (Eqv (Var 1) (Not (Not (Var 1))))
-- Associativity
tc 15 = (Eqv (And (And (Var 1) (Var 2)) (Var 3))
             (And (Var 1) (And (Var 2) (Var 3))))
-- De Morgan's rules
tc 16 = (Eqv (Not (Or (Var 1) (Var 2))) (And (Not (Var 1)) (Not (Var 2))))
-- Show that the following is not a tautology
tc 17 = (Imp (Imp (Var 1) (Var 3)) (Imp (Imp (Var 2) (Var 4))
        (Imp (Or (Var 1) (Var 2)) (Var 3))))
-- Unsatisfiable set of clauses
tc 18 = (And (And (And (Or (Or (Var 1) (Var 2)) (Not (Var 3)))
	(Or (Or (Var 1) (Var 2)) (Var 3))) (Or (Var 1) (Not (Var 2))))
	(Not (Var 1)))
-- Tautology
tc 19 = (Imp (Var 1) (Imp (Var 2) (Var 1)))
tc 20 = T
tc 21 = F