Lab3

[BertLisser]

Exercise 2, 4

genForm :: IO Form
genForm = do
    c <- pick 8  -- A number to determine the type of node.
    x <- pick 5  -- An x for when the node is a proposition.
    f1 <- if c > 3 then genForm else return (Prop 0) -- A child node (only generated if needed)
    f2 <- if c > 4 then genForm else return (Prop 0) -- Another child node (only generated if needed)
    return $ case c of
                 c | c <= 3 -> Prop x
                 4          -> Neg f1
                 5          -> Cnj [f1, f2]
                 6          -> Dsj [f1, f2]
                 7          -> Impl f1 f2
                 8          -> Equiv f1 f2

To remarks:
1 Too restricted. Cnj xs and Dsj xs where xs are lists must be also possible.
2 How the garantee that the generated form is not too deep.

Exercise 3

distLaw (Dsj (p:(Cnj (q:r:_)):_)) = Cnj [Dsj [p, q], Dsj [p, r]]
distLaw (Dsj ((Cnj (q:r:_)):p:_)) = Cnj [Dsj [p, q], Dsj [p, r]]

Better

distLaw (Dsj [p, (Cnj [q , r]]) = Cnj [Dsj [p, q], Dsj [p, r]]
distLaw (Dsj  [Cnj [q, r], p])= Cnj [Dsj [p, q], Dsj [p, r]]

-- Checks if something is a clause by checking if it consists of literals.
isClause (Dsj xs) = foldr (\x r -> isLiteral x && r) True xs
isClause x = isLiteral x
-- Checks if something is a literal by checking if it is a proposition,
-- optionally embedded in a negation.
isLiteral (Prop _) = True
isLiteral (Neg x) = isLiteral x
isLiteral _ = False

where is the rule

isClause (Cnj xs) = ....

[BertLisser]

There went something wrong. Sorry.