From jedwards@paradise.net.nz Thu Nov 1 20:13:28 2001
Received: from smtp1.ihug.co.nz (smtp1.ihug.co.nz [203.109.252.7])
by atlas.otago.ac.nz (8.9.3/8.9.3) with ESMTP id UAA205551
for ; Thu, 1 Nov 2001 20:13:27 +1300 (NZDT)
Received: from nestor.edwards.bogus (2031732402.adsl.ihug.co.nz [203.173.240.2])
by smtp1.ihug.co.nz (8.9.3/8.9.3/Debian 8.9.321) with ESMTP id UAA31597
for ; Thu, 1 Nov 2001 20:13:26 +1300
XAuthenticationWarning: smtp1.ihug.co.nz: Host 2031732402.adsl.ihug.co.nz [203.173.240.2] claimed to be nestor.edwards.bogus
Received: from paradise.net.nz (mimi.edwards.bogus [192.168.1.17])
by nestor.edwards.bogus (8.11.3nb1/8.11.3) with ESMTP id fA17Ct222160
for ; Thu, 1 Nov 2001 20:12:55 +1300 (NZDT)
Sender: jedwards@ihug.co.nz
MessageID: <3BE0F66C.DE16272F@paradise.net.nz>
Date: Thu, 01 Nov 2001 20:14:53 +1300
From: Jon Edwards
XMailer: Mozilla 4.77 [en] (X11; U; Linux 2.4.320mdk i686)
XAcceptLanguage: en
MIMEVersion: 1.0
To: "Richard A. O'Keefe"
Subject: Re: COSC 470 assignment
References: <200111010208.PAA204677@atlas.otago.ac.nz>
ContentType: multipart/mixed;
boundary="808BDDB203C75F515B2E75A4"
Status: R
This is a multipart message in MIME format.
808BDDB203C75F515B2E75A4
ContentType: text/plain; charset=usascii
ContentTransferEncoding: 7bit
"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
808BDDB203C75F515B2E75A4
ContentType: text/plain; charset=usascii;
name="DNF.hs"
ContentTransferEncoding: 7bit
ContentDisposition: inline;
filename="DNF.hs"
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 selfcontradictory 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
808BDDB203C75F515B2E75A4