Recursively modifying parts of a data structure in Haskell

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开发者_StackOverflow 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.

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.

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.)

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.

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).