Comment 3

[BertLisser]

Exercise 2

instance Arbitrary Form where
    arbitrary = oneof [arbitraryProp, arbitraryNeg, 
                     arbitraryCnj,arbitraryDsj,arbitraryImpl,arbitraryEquiv]
        where arbitraryProp = do
                  p <- arbitrary
                  return $ Prop $ ((p `mod` 3) + 1)
              arbitraryNeg = do
                  p <- arbitrary
                  return $ Neg $ p
              arbitraryCnj = do
                  p <- arbitrary
                  return $ Cnj [p,p]
              arbitraryDsj = do
                  p <- arbitrary
                  return $ Dsj [p,p]
              arbitraryImpl = do
                  p <- arbitrary
                  return $ Impl p p
              arbitraryEquiv = do
                  p <- arbitrary
                  return $ Equiv p p

is too restricted. Better

instance Arbitrary Form where
    arbitrary = oneof [arbitraryProp, arbitraryNeg, 
                     arbitraryCnj,arbitraryDsj,arbitraryImpl,arbitraryEquiv]
        where arbitraryProp = do
                  p <- arbitrary
                  return $ Prop $ ((p `mod` 3) + 1)
              arbitraryNeg = do
                  p <- arbitrary
                  return $ Neg $ p
              arbitraryCnj = do
                  p <- arbitrary
                  q <- arbitrary
                  return $ Cnj [p,q]
              arbitraryDsj = do
                  p <- arbitrary
                  q <- arbitrary
                  return $ Dsj [p,p]
              arbitraryImpl = do
                  p <- arbitrary
                  q <- arbitrary
                  return $ Impl p q
              arbitraryEquiv = do
                  p <- arbitrary
                 q <- arbitrary
                  return $ Equiv p q

Exercise 3
Why

dl (Impl f1 f2) = Impl (dl f1) (dl f2)
dl (Equiv f1 f2) = Equiv (dl f1) (dl f2)
fl (Impl f1 f2) = Impl (fl f1) (dl f2)
fl (Equiv f1 f2) = Equiv (fl f1) (dl f2)

? Input form is garanteed arrowfree.
Rewrite rules are too complicated and to restricted. Cnj and Dsj can have as arguments a list of arbitrary length.
A right implementation:

cnf :: Form -> Form
cnf x = cnf' $ nnf $ arrowfree x

-- preconditions: input is arrowfree and in nnf
cnf' :: Form -> Form
cnf' (Prop x) = Prop x
cnf' (Neg (Prop x)) = Neg (Prop x)
cnf' (Cnj fs) = Cnj (map cnf' fs)
cnf' (Dsj []) = Dsj []
cnf' (Dsj [f]) = cnf' f
cnf' (Dsj (f1:f2:fs)) = dist (cnf' f1) (cnf' (Dsj(f2:fs)))

dist :: Form -> Form -> Form
dist (Cnj []) f = Cnj[] {-- f --}
dist (Cnj [f1]) f2 = dist f1 f2
dist (Cnj (f1:fs)) f2 = Cnj [dist f1 f2, dist (Cnj fs) f2]
dist f (Cnj []) = Cnj[] {-- f --}
dist f1 (Cnj [f2]) = dist f1 f2
dist f1 (Cnj (f2:fs)) = Cnj [dist f1 f2, dist f1 (Cnj fs)]
dist f1 f2 = Dsj [f1,f2]

Exercise 4

noNestedAndOr :: Form -> Bool
noNestedAndOr (Prop x) = True
noNestedAndOr (Neg f) =  noNestedAndOr f
noNestedAndOr (Cnj [_, (Cnj _)]) = False   -- Wrong. Must be omitted
noNestedAndOr (Cnj [(Cnj _), _]) = False   -- Wrong. Must be omitted
noNestedAndOr (Cnj fs) = all noNestedAndOr fs
noNestedAndOr (Dsj [_, (Cnj _)]) = False -- Must be extended to whole list
noNestedAndOr (Dsj [(Cnj _), _]) = False -- Must be omitted
noNestedAndOr (Dsj fs) = all noNestedAndOr fs  -- Must be omitted
noNestedAndOr (Impl f1 f2) = noNestedAndOr f1 && noNestedAndOr f2
noNestedAndOr (Equiv f1 f2) = noNestedAndOr f1 && noNestedAndOr f2