Set Theory Expression Simplification

Run Settings
LanguageHaskell
Language Version
Run Command
{-# LANGUAGE UnicodeSyntax #-} data RuleCondition = Universal | Empty | Set String String | Union RuleCondition RuleCondition | Intersection RuleCondition RuleCondition data Rule = Rule RuleCondition Int deriving (Show, Eq) data RuleSet = RuleSet [Rule] Int deriving (Show, Eq) isSubRC :: RuleCondition -> RuleCondition -> Bool isSubRC x y = isSubRC' (simplifyrc x) (simplifyrc y) where isSubRC' Empty _ = True isSubRC' _ Empty = False isSubRC' _ Universal = True isSubRC' Universal _ = False isSubRC' (Set t v) (Set t' v') = t == t' && v == v' isSubRC' (a `Intersection` b) (c `Intersection` d) = -- generally not comprehensive (a `isSubRC` c || a `isSubRC` d) && ((b `isSubRC` c) || (b `isSubRC` d)) isSubRC' (a `Union` b) c = a `isSubRC` c && b `isSubRC` c isSubRC' a (b `Union` c) = a `isSubRC` b || a `isSubRC` c isSubRC' a (b `Intersection` c) = a `isSubRC` b && a `isSubRC` c isSubRC' (a `Intersection` b) c = a `isSubRC` c || b `isSubRC` c rcLength :: RuleCondition -> Int rcLength Empty = 0 rcLength Universal = 1 rcLength (Set _ _) = 1 rcLength (Union a b) = rcLength a + rcLength b rcLength (Intersection a b) = rcLength a + rcLength b rcSmallest :: RuleCondition -> RuleCondition -> RuleCondition rcSmallest a b = if rcLength a <= rcLength b then a else simplifyrc b instance Show RuleCondition where show Empty = "∅" show Universal = "Universal" show (Set t v) = "Set \"" ++ t ++ "\" \"" ++ v ++ "\"" show (Union a b) = "(" ++ show a ++ " ∪ " ++ show b ++ ")" show (Intersection a b) = "(" ++ show a ++ " ∩ " ++ show b ++ ")" (∪), (∩) :: RuleCondition -> RuleCondition -> RuleCondition (∅) :: RuleCondition (∪) = Union (∩) = Intersection (∅) = Empty simplifyrc :: RuleCondition -> RuleCondition simplifyrc Empty = Empty simplifyrc Universal = Universal simplifyrc ( Universal `Union` _ ) = Universal simplifyrc ( _ `Union` Universal) = Universal simplifyrc ( Universal `Intersection` a ) = a simplifyrc ( a `Intersection` Universal) = a simplifyrc ( Empty `Intersection` _ ) = Empty simplifyrc ( _ `Intersection` Empty ) = Empty simplifyrc ( Empty `Union` a ) = a simplifyrc ( a `Union` Empty ) = a simplifyrc s@(Set _ _ ) = s simplifyrc s@(Set t v `Union` Set t' v') | t == t' && v == v' = Set t v -- A ∪ A = A | otherwise = s simplifyrc s@(Set t v `Intersection` Set t' v') | t == t' && v == v' = Set t v -- A ∩ A = A | t == t' && v /= v' = Empty | otherwise = s -- ^^ Rules -- Simplification tricks: -- Assosiative rule: A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C) simplifyrc expr@(a@(Set _ _) `Intersection` (b@(Set _ _) `Union` c@(Set _ _))) = -- trace ("\n A ∩ (B ∪ C): " ++ show expr ++ "\n") $ if a == b || a == c then a else -- A ∩ (A ∪ C) = A rcSmallest expr $ simplifyrc (a `Intersection` b) `Union` simplifyrc (a `Intersection` c) -- Assosiative rule: A ∪ (B ∩ C) = (A ∪ B) ∩ (A ∪ C) simplifyrc expr@(a@(Set _ _) `Union` (c@(Set _ _) `Intersection` d@(Set _ _))) = -- trace ("A ∪ (B ∩ C): " ++ show expr ++ "\n") $ if c == a || d == a then a else -- A ∪ (A ∩ C) = A rcSmallest expr $ simplifyrc (a `Union` c) `Intersection` simplifyrc (a `Union` d) -- Assosiative rule inverse (with Set type): (A ∪ B) ∩ (A ∪ D) = A ∪ (B ∩ D) simplifyrc expr@((a@(Set _ _) `Union` b@(Set _ _)) `Intersection` (c@(Set _ _) `Union` d@(Set _ _)) ) = go where go | a == c = a `Union` simplifyrc (b `Intersection` d) | a == d = a `Union` simplifyrc (b `Intersection` c) | b == c = b `Union` simplifyrc (a `Intersection` d) | b == d = b `Union` simplifyrc (a `Intersection` a) | otherwise = expr -- More generic rules over expressions: -- Assosiative rule inverse: (A ∪ B) ∩ (A ∪ D) = A ∪ (B ∩ D) simplifyrc expr@(l@(a `Union` b) `Intersection` r@(c `Union` d)) = rcSmallest expr go where go | l' == r' = l | a' == c' = a' `Union` simplifyrc (b' `Intersection` d') | a' == d' = a' `Union` simplifyrc (b' `Intersection` c') | b' == c' = b' `Union` simplifyrc (a' `Intersection` d') | b' == d' = b' `Union` simplifyrc (a' `Intersection` c') | otherwise = expr a' = simplifyrc a b' = simplifyrc b c' = simplifyrc c d' = simplifyrc d l' = simplifyrc l r' = simplifyrc r -- Assosiative rule inverse: (A ∩ B) ∪ (A ∩ C) = A ∩ (B ∪ C) simplifyrc expr@(l@(a `Intersection` b) `Union` r@(c `Intersection` d)) = rcSmallest expr go where go | l' == r' = l' | a' == c' = a' `Intersection` (b' `Union` d') | a' == d' = a' `Intersection` (b' `Union` c') | b' == c' = b' `Intersection` (a' `Union` d') | b' == d' = b' `Intersection` (a' `Union` c') | otherwise = expr a' = simplifyrc a b' = simplifyrc b c' = simplifyrc c d' = simplifyrc d l' = simplifyrc l r' = simplifyrc r -- Distributive rule: (A ∩ B) ∩ (C ∩ D) = (A ∩ C) ∩ (B ∩ D) simplifyrc expr@((a `Intersection` b) `Intersection` (c `Intersection` d)) = rcSmallest expr $ simplifyrc (a `Intersection` c) `Intersection` simplifyrc (b `Intersection` d) -- Distributive rule: A ∩ (B ∩ C) = (A ∩ B) ∩ C = (A ∩ C) ∩ B simplifyrc (a `Intersection` r@(b `Intersection` c)) = rcSmallest (a' `Intersection` r') $ rcSmallest (simplifyrc (a' `Intersection` b') `Intersection` c') (simplifyrc (a' `Intersection` c') `Intersection` b') where r' = simplifyrc r a' = simplifyrc a b' = simplifyrc b c' = simplifyrc c simplifyrc (r@(_ `Intersection` _) `Intersection` a) = simplifyrc $ a `Intersection` r -- Distributive rule: (A ∪ B) ∪ (C ∪ D) = (A ∪ C) ∪ (B ∪ D) simplifyrc expr@((a `Union` b) `Union` (c `Union` d)) = rcSmallest expr $ simplifyrc (a `Union` c) `Union` simplifyrc (b `Union` d) -- Distributive rule: A (B ∪ C) = (A ∪ B) ∪ C simplifyrc (a `Union` r@(b `Union` c)) = rcSmallest (a' `Union` r') $ simplifyrc (a' `Union` b') `Union` c' where r' = simplifyrc r a' = simplifyrc a b' = simplifyrc b c' = simplifyrc c -- A ∪ B = -- | A ⊆ B = B -- | B ⊆ A = A -- | _ = A ∪ B simplifyrc (a `Union` b) = let a' = simplifyrc a b' = simplifyrc b in go a' b' where go a' b' | a' `isSubRC` b' = b' | b' `isSubRC` a' = a' | otherwise = a' `Union` b' -- A ∩ B = -- | A ⊆ B = A -- | B ⊆ A = B -- | _ = A ∩ B simplifyrc (a `Intersection` b) = -- trace ("A ∩ B: " ++ show expr ++ "\n") go where go | a `isSubRC` b = simplifyrc a | b `isSubRC` a = simplifyrc b | otherwise = simplifyrc a `Intersection` simplifyrc b instance Eq RuleCondition where a == b = a `isSubRC` b && b `isSubRC` a affJB, osIOS, osAndroid, langEn, affSAM, jbOrIOS, jbOrSAMorIOS, opCelcom, jbAndIOS, jbAndIOSOrCelcom :: RuleCondition affJB = Set "Affiliate" "JB" osIOS = Set "OS" "iOS" osAndroid = Set "OS" "Android" affSAM = Set "Affiliate" "SAM" opCelcom = Set "Operator" "Celcom" langEn = Set "Lang" "EN" jbOrIOS = Union affJB osIOS jbOrSAMorIOS = Union (Union affJB affSAM) osIOS jbAndIOS = Intersection affJB osIOS jbAndIOSOrCelcom = Union jbAndIOS jbAndIOSOrCelcom main :: IO () main = do testSimplifyRC (affJB `Intersection` affSAM) Empty testSimplifyRC ((affJB ∪ osIOS) ∩ (affJB ∪ osIOS)) (affJB ∪ osIOS) testSimplifyRC (affSAM `Intersection` (osIOS `Intersection` affJB)) Empty testSimplifyRC ((osIOS `Intersection` affJB) `Intersection` affSAM) Empty testSimplifyRC ((affJB `Intersection` osIOS) `Union` opCelcom) ((affJB `Intersection` osIOS) `Union` opCelcom) testSimplifyRC ( affSAM `Union` (affJB `Union` affSAM) `Union` (affSAM `Union` affJB) `Union` affJB ) (affSAM `Union` affJB) testSimplifyRC (jbAndIOS `Union` affJB) affJB testSimplifyRC ((affJB `Intersection` opCelcom) `Union` (affJB `Intersection` opCelcom)) (affJB `Intersection` opCelcom) testSimplifyRC ((affJB `Intersection` osIOS) `Intersection` osIOS) (affJB `Intersection` osIOS) testSimplifyRC ( (affJB `Intersection` osIOS `Intersection` opCelcom) `Union` (affJB `Intersection` opCelcom) ) (affJB `Intersection` opCelcom) testSimplifyRC ((affJB ∪ osIOS) ∩ (osIOS ∪ opCelcom)) (osIOS ∪ (affJB ∩ opCelcom)) testSimplifyRC (osIOS `Intersection` (osIOS `Union` affJB)) osIOS testSimplifyRC (osIOS `Intersection` (affJB `Union` osIOS)) osIOS testSimplifyRC (((affJB ∩ osIOS) ∪ (affSAM ∩ osIOS)) ∪ (affJB ∪ affSAM) ∪ osIOS) (affJB ∪ affSAM ∪ osIOS) testSimplifyRC ((affSAM `Intersection` osIOS) `Intersection` (affJB `Intersection` osIOS)) Empty testSimplifyRC (osIOS ∩ (osAndroid ∪ affJB)) (osIOS ∩ affJB) testSimplifyRC ((osIOS ∩ affJB) ∩ (langEn ∩ opCelcom)) ((osIOS ∩ affJB) ∩ (langEn ∩ opCelcom)) testSimplifyRC ((osIOS ∩ affJB) ∩ (osAndroid ∩ affSAM)) Empty testSimplifyRC ((osIOS ∩ (affJB ∪ opCelcom)) ∪ (osAndroid ∩ (affJB ∪ opCelcom))) ((affJB ∪ opCelcom) ∩ (osIOS ∪ osAndroid)) where testSimplifyRC expr expected = do putStrLn "---" putStrLn $ "simplify: " ++ show expr let res = simplifyrc expr putStrLn $ "result : { " ++ show res ++ " }" putStrLn $ "expected: { " ++ show expected ++ " }" print (res == expected)
Editor Settings
Theme
Key bindings
Full width
Lines