Generic transformations on a set of a given datatype

Question

If I have a datatype representing a subset of propositional logic such as

data Prop = Lit String
          | Neg Prop
          | And Prop Prop
          | Or Prop Prop

Are there then easy ways to do generic transformations on [[Prop]]? E.g.

• replace [[And a b, c]] with [[a, b, c]]
• replace [[Or a b, c]] with [[a], [b], [c]], or
• removing occurrences of sublists containing both Neg a and a, e.g. turning [[Neg a, x, a], [b]] into [[b]]

This feels like something close to what e.g. uniplate does, but “two levels up”.

Answer 1

I assume that your second rule is wrong, and you really meant to say either:

• replace [[Or a b],[c]] with [[a],[b],[c]]

or else:

• replace [[Or a b, c]] with [[a,c],[b,c]]

In other words, I assume you're trying to convert a Prop into an alternate representation [[Prop]] where the first-level list is an "or" and the second-level lists are "and"s, with all terms being either literals or Neg-literals. So, you're trying to imagine how you could apply a bunch of generic structural rules to make transformations like:

[[And a (Or b c)]]
[[a, Or b c]]        -- apply "And" rule
[[a,b],[a,c]]        -- apply some kind of "Or" distribution rule

If so, having generic transformations isn't much use. With your current datatype, you can only apply these transformations to top-level expressions anyway. For example, there's no obvious way to apply an Or rule here:

[[And a (And b (Or c d))]]

without first applying And rules a couple of times. If you change your data type to add, say, an L2 [[Prop]] constructor, so you can transform the above expression to:

[[And a (And b (L2 [[c],[d]]))]]   -- apply "Or" rule

it's not clear what that buys you.

Ultimately, I don't think this is the right approach...

You have a perfectly adequate representation of your prepositional logic in the Prop data type; and you have a desired final representation. Instead of trying to translate your Prop representation into the final representation using piecemeal generic transformations, transform your Prop representation using standard recursive Prop-to-Prop transformations into a canonical Prop form, and do the translation as the final step.

Here, a reasonable canonical form is:

Or e1 (Or e2 (... (Or e3 e4)))

where each ek is of form:

And t1 (And t2 (... (And t3 t4)))

and each tk is either a Lit _ or a Neg (Lit _). Obviously, this canonical form can be translated pretty easily into the desired final representation as a [[Prop]].

I've included a possible solution below. I don't see that much opportunity for simplifying things via generic transformations. Most of the pattern matching seems to be doing non-trivial work.

Possible Solution

After a bit of preamble:

import Data.List

data Prop = Lit String
          | Neg Prop
          | And Prop Prop
          | Or Prop Prop
          deriving (Eq)

then one way to translate an arbitrary Prop into this canonical form is to first push all the Negs down to the literal terms:

pushNeg :: Prop -> Prop
pushNeg = push False
  where
    -- de Morgan's laws
    push neg (And x y) = (if neg then Or else And) (push neg x) (push neg y)
    push neg (Or x y)  = (if neg then And else Or) (push neg x) (push neg y)
    -- handle Neg and Lit
    push neg (Neg y) = push (not neg) y
    push neg (Lit l) = if neg then Neg (Lit l) else Lit l

then push all the Ands down on top of them. This is tougher to get right, but I think the following is correct, even though it does a bit of unnecessary work in some cases:

pushAnd :: Prop -> Prop
pushAnd (Or x y) = Or (pushAnd x) (pushAnd y)
pushAnd (And x y)
  = let x' = pushAnd x
    in  case x' of
          Or u v -> Or (pushAnd (And u y)) (pushAnd (And v y))
          _ -> let y' = pushAnd y
               in case y' of
                    Or u v -> Or (pushAnd (And x' u)) (pushAnd (And x' v))
                    _ -> And x' y'
pushAnd x = x

and then recursively make all the And and Or clauses right-associative:

rassoc :: Prop -> Prop
rassoc (Or (Or x y) z)   = rassoc (Or x (Or y z))
rassoc (Or x        z)   = Or (rassoc x) (rassoc z)
rassoc (And (And x y) z) = rassoc (And x (And y z))
rassoc (And x         z) = And x (rassoc z)
rassoc x = x

and finally convert the canonical form to its final representation (dropping the inconsistent clauses and duplicate terms while we're at it):

translate :: Prop -> [[Prop]]
translate = nub . map nub . filter consistent . doOr
  where
    doOr x = case x of
      Or x y -> doAnd x : doOr y
      x      -> doAnd x : []
    doAnd x = case x of
      And x y -> x : doAnd y
      x       -> x : []
    consistent lits =
      let (falses, trues) = partition isNeg lits
          falses' = map (\(Neg (Lit l)) -> l) falses
          trues'  = map (\     (Lit l)  -> l) trues
      in null (intersect falses' trues')
    isNeg (Neg x) = True
    isNeg _       = False

The whole pipeline is:

final :: Prop -> [[Prop]]
final = translate . rassoc . pushAnd . pushNeg

and here's some test code:

a = Lit "a"
b = Lit "b"
c = Lit "c"
d = Lit "d"
e = Lit "e"

-- Show instance, but only for `final` forms
instance Show Prop where
  show (Lit x) = x
  show (Neg (Lit x)) = '~':x

main :: IO ()
main = do print $ final (Neg a)
          print $ final (Or a b)
          print $ final (Or a a)
          print $ final (And a b)
          print $ final (And (Or (And (Or a b) c) d) e)
          print $ final (And (Or (Or a b) c) (Neg (And a (Or b d))))

which outputs:

[[~a]]
[[a],[b]]
[[a]]
[[a,b]]
[[a,c,e],[b,c,e],[d,e]]
[[a,~b,~d],[b,~a],[c,~a],[c,~b,~d]]

There's still some opportunity for further simplification, as:

final (And a (Or a b))

gives final form [[a],[a,b]] instead of just [[a]].