3

Hello guys I am new to Haskell, I would like to create a Haskell Program that can apply DeMorgan's laws on logic expressions. The problem is I can't change the given expression to a new expression (after applying DeMorgan's laws)

To be specific here is my data structure

data LogicalExpression = Var Char
        | Neg LogicalExpression
        | Conj LogicalExpression LogicalExpression
        | Disj LogicalExpression LogicalExpression
        | Impli LogicalExpression LogicalExpression
        deriving(Show)

I would like to create a function that takes in a "LogicalExpression" and return a "LogicalExpression" after applying DeMorgan's laws.

For example whenever I find this pattern: Neg ( Conj (Var 'a') (Var 'b') ) in a logicalExpression, I need to convert it to Conj ( Neg (Var 'a') Neg (Var 'b') ).

The idea is simple but it's so hard to implement in haskell, it's like trying to make a function (let's call it Z) that searches for x and converts it to y, so if Z is given "vx" it converts it to "vy" only instead of strings it takes in the data structure "logicalExpression" and instead of x it take the pattern I mentioned and spits out the whole logicalExpression again but with the pattern changed.

P.S: I want the function to take any Complex logic expression and simplifies it using DeMorgan's laws

Any hints?

Thanks in advance.

7
  • 3
    Post the code you already have and perhaps a more complex example (including the "lies in a big logical expression" part). But the basic idea is, you don't change state (let me repeat that: you don't change state) in Haskell, you instead create a new state.
    – user395760
    May 31, 2011 at 21:10
  • 1
    Add the homework tag, plus this is a GUC cheating case !
    – is7s
    May 31, 2011 at 22:05
  • @luqui check this out bit.ly/iv10Hs This question is about part (c) in the project, he/she didn't even present a solution he's asking for a ready one right away !
    – is7s
    Jun 1, 2011 at 5:56
  • 1
    @is7s: although there are some similarities, the question isn't obviously exactly the same as posed in that project. De Morgan's laws aren't exactly uncommon. Even if it is derived from that project, the questioner seems to at least have made an effort to understand and explain what they are trying to do rather than just copy and paste the problem description. If you do still think this is a case of cheating I suggest that you report it to the instructor for that course. Jun 1, 2011 at 6:31
  • @Ganesh What the questioner presented was the solution for part (a) which just asks for the definition of the datatype. But for part (c), he/she presented nothing (not even a wrong solution). Actually the problem description states exactly the steps which need to be implemented in order to get a LogicExpr into clausal normal form (demorgan is one of these steps). I'm one of the junior instructor in the course and we'll be dealing with such cases in oral evaluations, if we detected copy-paste situations which do not reflect understanding, marks will definitely be deducted
    – is7s
    Jun 1, 2011 at 9:14

4 Answers 4

7

Luke (luqui) has presented probably the most elegant way to think about the problem. However, his encoding requires you to manually get right large swathes of the traversal for each such rewrite rule you want to create.

Bjorn Bringert's compos from A Pattern for Almost Composable Functions can make this easier, especially if you have multiple such normalization passes you need to write. It is usually written with Applicatives or rank 2 types, but to keep things simple here I'll defer that:

Given your data type

data LogicalExpression
    = Var Char
    | Neg LogicalExpression
    | Conj LogicalExpression LogicalExpression
    | Disj LogicalExpression LogicalExpression
    | Impl LogicalExpression LogicalExpression
deriving (Show)

We can define a class used to hunt down non-top-level sub-expressions:

class Compos a where
    compos' :: (a -> a) -> a -> a

instance Compos LogicalExpression where
    compos' f (Neg e)    = Neg (f e)
    compos' f (Conj a b) = Conj (f a) (f b)
    compos' f (Disj a b) = Disj (f a) (f b)
    compos' f (Impl a b) = Impl (f a) (f b)
    compos' _ t = t

For instance, we could eliminate all implications:

elimImpl :: LogicalExpression -> LogicalExpression
elimImpl (Impl a b) = Disj (Not (elimImpl a)) (elimImpl b)
elimImpl t = compos' elimImpl t -- search deeper

Then we can apply it, as luqui does above, hunting down negated conjunctions and disjunctions. And since, as Luke points out, it is probably better to do all your negation distribution in one pass, we'll also include normalization of negated implication and double negation elimination, yielding a formula in negation normal form (assuming that we've already eliminated implication)

nnf :: LogicalExpression -> LogicalExpression
nnf (Neg (Conj a b)) = Disj (nnf (Neg a)) (nnf (Neg b))
nnf (Neg (Disj a b)) = Conj (nnf (Neg a)) (nnf (Neg b))
nnf (Neg (Neg a))    = nnf a
nnf t                = compos' nnf t -- search and replace

The key is the last line, which says that if none of the other cases above match, go hunt for subexpressions where you can apply this rule. Also, since we push the Neg into the terms, and then normalize those, you should only wind up with negated variables at the leaves, since all other cases where Neg precedes another constructor will be normalized away.

The more advanced version would use

import Control.Applicative
import Control.Monad.Identity

class Compos a where
    compos :: Applicative f => (a -> f a) -> a -> f a

compos' :: Compos a => (a -> a) -> a -> a
compos' f = runIdentity . compos (Identity . f) 

and

instance Compos LogicalExpression where
    compos f (Neg e)    = Neg <$> f e
    compos f (Conj a b) = Conj <$> f a <*> f b
    compos f (Disj a b) = Disj <$> f a <*> f b
    compos f (Impl a b) = Impl <$> f a <*> f b
    compos _ t = pure t

This doesn't help in your particular case here, but is useful later if you need to return multiple rewritten results, perform IO, or otherwise engage in more complicated activities in your rewrite rule.

You might need to use this, if for instance, you wanted to try to apply the deMorgan laws in any subset of the locations where they apply rather than pursue a normal form.

Notice that no matter what function you are rewriting, Applicative you are using, or even directionality of information flow during the traversal, the compos definition only has to be given once per data type.

5
  • Great answer; this was the pattern I was looking for in my answer, but I couldn't formulate it clear enough and started messing with a function that finds a fixpoint of the transformation. +1.
    – Fred Foo
    Jun 1, 2011 at 10:26
  • This looks extraordinarily similar to various generics libraries, particularly uniplate.
    – John L
    Jun 1, 2011 at 11:54
  • 1
    It is. It was one of the earliest such designs. Jun 1, 2011 at 14:25
  • 1
    @John L: Uniplate gives you compos directly now as an operation, as I recall.
    – sclv
    Jun 2, 2011 at 17:51
  • Yeah. Nowadays I usually turn to multiplate, which I find is a bit safer than the old MultiCompos and a bit less dirty feeling than Uniplate. Jun 3, 2011 at 5:40
6

If I understand correctly, you want to apply De Morgan's laws to push the negation down into the tree as far as possible. You'll have to explicitly recurse down the tree many times:

-- no need to call self on the top-level structure,
-- since deMorgan is never applicable to its own result
deMorgan (Neg (a `Conj` b))  =  (deMorgan $ Neg a) `Disj` (deMorgan $ Neg b)
deMorgan (Neg (a `Disj` b))  =  (deMorgan $ Neg a) `Conj` (deMorgan $ Neg b)
deMorgan (Neg a)             =  Neg $ deMorgan a
deMorgan (a `Conj` b)        =  (deMorgan a) `Conj` (deMorgan b)
-- ... etc.

All of this would be much easier in a term-rewriting system, but that's not what Haskell is.

(Btw., life becomes a lot easier if you translate P -> Q into not P or Q in your formula parser and remove the Impli constructor. The number of cases in each function on formulas becomes smaller.)

3
  • 1
    your 'BTW' concerning implication to disjunction is a good idea provided OP is willing to commit to classical logic (or another system wit that rule). There are systems where DeMorgan holds and that law does not Jun 1, 2011 at 14:00
  • @jon_darkstar: yes, I assumed classical logic. Just out of curiosity, which logics were you thinking of? IIRC, intuitionistic logic rejects De Morgan's laws.
    – Fred Foo
    Jun 1, 2011 at 14:07
  • Only one of them fails to hold, intuitionistically. Jun 3, 2011 at 19:03
4

Others have given good guidance. But I would phrase this as a negation eliminator, so that means you have:

deMorgan (Neg (Var x)) = Neg (Var x)
deMorgan (Neg (Neg a)) = deMorgan a
deMorgan (Neg (Conj a b)) = Disj (deMorgan (Neg a)) (deMorgan (Neg b))
-- ... etc. match Neg against every constructor
deMorgan (Conj a b) = Conj (deMorgan a) (deMorgan b)
-- ... etc. just apply deMorgan to subterms not starting with Neg

We can see by induction that in the result, Neg will only be applied to Var terms, and at most once.

I like to think of transformations like this as eliminators: i.e. things that try to "get rid" of a certain constructor at the top level by pushing them down. Match the constructor you are eliminating against every inner constructor (including itself), and then just forward the rest. For example, a lambda calculus evaluator is an Apply eliminator. An SKI converter is a Lambda eliminator.

6
  • This is a very nice way of looking at it! Jun 1, 2011 at 2:08
  • 1
    This is not the original problem, this constructs the NNF of the formula. The function would be better named nnf instead of deMorgan.
    – Fred Foo
    Jun 1, 2011 at 10:11
  • @luqui: yes. That's not one of De Morgan's laws.
    – Fred Foo
    Jun 1, 2011 at 11:59
  • @larsmans: The actual question is more about recursive transformations working with multiple layers of a recursive data structure, applying De Morgan's laws is just the specific example. When simplifying expressions something like NNF is often the goal anyway, so this is arguably more instructive in the general case. Jun 1, 2011 at 19:11
  • @camccann: and the actual protest is not that this doesn't answer the original question, but that the function should not be called deMorgan.
    – Fred Foo
    Jun 1, 2011 at 20:12
2

The important point is the recursive application of deMorgan. It is quite different from (for example) :

 deMorgan' z@(Var x) = z
 deMorgan' (Neg (Conj x y)) = (Disj (Neg x) (Neg y))
 deMorgan' (Neg (Disj x y)) = (Conj (Neg x) (Neg y))
 deMorgan' z@(Neg x) = z
 deMorgan' (Conj x y) = Conj x y
 deMorgan' (Disj x y) = Disj x y

which does not work :

 let var <- (Conj (Disj (Var 'A') (Var 'B')) (Neg (Disj (Var 'D') (Var 'E'))))
 *Main> deMorgan' var
 Conj (Disj (Var 'A') (Var 'B')) (Neg (Disj (Var 'D') (Var 'E')))

The problem here is that you do not apply transformations in the subexpressiosn (the x and ys).

2
  • Sorry I couldn't even understand myself, I've edited the description for better clarification :D May 31, 2011 at 21:25
  • I can already do something like this, What I need is a function that takes in a fully qualified logical expression and returning it after applying DeMorgans laws. for exampe given: (A /\ B) \/ not (D /\ E) will return: (A /\ B) \/ (Not(D) \/ Not(E)) Can you see it? It searches the whole expression for a pattern that matches DeMorgan's and then converting this pattern, to it's DeMorgan equivalent then returning the while expression again but with the new changes. May 31, 2011 at 21:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.