logical laws

Logic/Statement/Laws.hs

@@ -0,0 +1,163 @@
+module Logic.Statement.Laws where
+
+import Logic.Parse (eof, mkInput)
+import Logic.Statement (Statement(..))
+import Logic.Statement.Parse (stmt)
+
+import Data.Either (fromRight)
+import Data.Maybe (fromJust, listToMaybe)
+
+data Law = Law
+  { lawName :: String
+  , lawLhs :: Statement
+  , lawRhs :: Statement
+  } deriving (Eq, Show)
+
+mkLaw :: String -> String -> String -> Law
+mkLaw name lhs rhs = Law name (fromString lhs) (fromString rhs)
+  where
+    fromString :: String -> Statement
+    fromString string = fromRight undefined (eof stmt $ mkInput string)
+
+laws :: [Law]
+laws =
+  [ mkLaw "dbl_neg" "A" "!!A"
+  , mkLaw "and_comm" "(A&B)" "(B&A)"
+  , mkLaw "or_comm"  "(A|B)" "(B|A)"
+  , mkLaw "and_assoc" "(A&(B&C))" "((A&B)&C)"
+  , mkLaw "or_assoc"  "(A|(B|C))" "((A|B)|C)"
+  , mkLaw "and_or_distrib" "(A&(B|C))" "((A&B)|(A&C))"
+  , mkLaw "or_and_distrib" "(A|(B&C))" "((A|B)&(A|C))"
+  , mkLaw "and_symm_eq" "A" "(A&A)"
+  , mkLaw "or_symm_eq"  "A" "(A|A)"
+  , mkLaw "not_and_distrib" "!(A&B)" "(!A|!B)"
+  , mkLaw "not_or_distrib"  "!(A|B)" "(!A&!B)"
+  , mkLaw "implies_or"  "(A->B)" "(!A|B)"
+  , mkLaw "implies_and" "(A->B)" "!(A&!B)"
+  , mkLaw "or_contr_eq" "A" "(A|(B&!B))"
+  , mkLaw "and_or_cancel" "A" "(A&(A|B))"
+  , mkLaw "or_and_cancel" "A" "(A|(A&B))"
+  , mkLaw "iff_and" "(A<->B)" "((A->B)&(B->A))"
+  , mkLaw "iff_or"  "(A<->B)" "((A&B)|(!A&!B))"
+  ]
+
+lookupLaw :: String -> Maybe Law
+lookupLaw name = listToMaybe $ filter (\law -> lawName law == name) laws
+
+match
+  :: Statement
+  -- ^ pattern
+  -> Statement
+  -- ^ statement to search
+  -> Maybe [(String, Statement)]
+  -- ^ mapping from pattern-statement atoms to search-statement parts
+match = aux []
+  where
+    aux
+      :: [(String, Statement)]
+      -> Statement
+      -> Statement
+      -> Maybe [(String, Statement)]
+    aux mapping (Atom key) s = add mapping (key, s)
+    aux mapping (Not p) (Not s) = aux mapping p s
+    aux mapping (And     p1 p2) (And     s1 s2) = binary mapping (p1, s1) (p2, s2)
+    aux mapping (Or      p1 p2) (Or      s1 s2) = binary mapping (p1, s1) (p2, s2)
+    aux mapping (Implies p1 p2) (Implies s1 s2) = binary mapping (p1, s1) (p2, s2)
+    aux mapping (Iff     p1 p2) (Iff     s1 s2) = binary mapping (p1, s1) (p2, s2)
+    aux mapping pattern s = Nothing
+
+    add
+      :: [(String, Statement)]
+      -> (String, Statement)
+      -> Maybe [(String, Statement)]
+    add mapping entry@(key, s') =
+      case lookup key mapping of
+        Nothing -> Just (entry:mapping)
+        Just existing
+          | existing == s' -> Just mapping
+          | otherwise -> Nothing
+
+    binary
+      :: [(String, Statement)]
+      -> (Statement, Statement)
+      -> (Statement, Statement)
+      -> Maybe [(String, Statement)]
+    binary mapping (p1, s1) (p2, s2) = do
+      mapping' <- aux mapping p1 s1
+      aux mapping' p2 s2
+
+{-
+ghci> f x = fromRight undefined $ eof stmt $ mkInput x
+ghci> match (f "(A&B)") (f "(p&(q|r))")
+Just [("B",Or (Atom "q") (Atom "r")),("A",Atom "p")]
+ghci> match (f "((A&B)|A)") (f "(p&(q|r))")
+Nothing
+ghci> match (f "((A&B)|A)") (f "((p&(q|r))|p)")
+Just [("B",Or (Atom "q") (Atom "r")),("A",Atom "p")]
+ghci> match (f "((A&B)|A)") (f "((p&(q|r))|q)")
+Nothing
+ghci> l = fromJust $ lookupLaw "and_or_distrib"
+ghci> l
+Law {lawName = "and_or_distrib", lawLhs = And (Atom "A") (Or (Atom "B") (Atom "C")), lawRhs = Or (And (Atom "A") (Atom "B")) (And (Atom "A") (Atom "C"))}
+ghci> match (lawLhs l) (f "(p&(q|r))")
+Just [("C",Atom "r"),("B",Atom "q"),("A",Atom "p")]
+-}
+
+data SwapError
+  = Indeterminate
+  -- ^ An atom in p2 doesn't exist in p1.
+  -- Strictly: an atom in p2 doesn't exist in the result from `match`
+  -- (matters only if `match` is implemented incorrectly).
+  -- If for atoms we used terms of a type instead of strings,
+  -- we could avoid needing this error.
+  | NonMatchingPattern
+  deriving Show
+
+swap :: Statement -> Statement -> Statement -> Either SwapError Statement
+swap p1 p2 s = do
+  mapping <- maybe (Left NonMatchingPattern) Right $ match p1 s
+  maybe (Left Indeterminate) Right $ aux mapping p2
+  where
+    aux :: [(String, Statement)] -> Statement -> Maybe Statement
+    aux mapping (Atom key) = lookup key mapping
+    aux mapping (Not p) = Not <$> aux mapping p
+    aux mapping (And     p1 p2) = And     <$> aux mapping p1 <*> aux mapping p2
+    aux mapping (Or      p1 p2) = Or      <$> aux mapping p1 <*> aux mapping p2
+    aux mapping (Implies p1 p2) = Implies <$> aux mapping p1 <*> aux mapping p2
+    aux mapping (Iff     p1 p2) = Iff     <$> aux mapping p1 <*> aux mapping p2
+
+{-
+ghci> f x = fromRight undefined $ eof stmt $ mkInput x
+ghci> l = fromJust $ lookupLaw "and_or_distrib"
+ghci> l
+Law {lawName = "and_or_distrib", lawLhs = And (Atom "A") (Or (Atom "B") (Atom "C")), lawRhs = Or (And (Atom "A") (Atom "B")) (And (Atom "A") (Atom "C"))}
+ghci> 
+ghci> match (f "(A&B)") (f "(p&(q|r))")
+Just [("B",Or (Atom "q") (Atom "r")),("A",Atom "p")]
+ghci> swap (f "(A&B)") (f "A") (f "(p&(q|r))")
+Right (Atom "p")
+ghci> swap (f "(A&B)") (f "B") (f "(p&(q|r))")
+Right (Or (Atom "q") (Atom "r"))
+ghci> swap (f "(A&B)") (f "C") (f "(p&(q|r))")
+Left Indeterminate
+ghci> swap (f "((A&B)->C)") (f "A") (f "(p&(q|r))")
+Left NonMatchingPattern
+ghci> 
+ghci> x = f "(p&(q|r))"
+ghci> x
+And (Atom "p") (Or (Atom "q") (Atom "r"))
+ghci> serialize Plain x
+"(p&(q|r))"
+ghci> serialize Plain $ fromRight undefined $ swap (lawLhs l) (lawLhs l) x
+"(p&(q|r))"
+ghci> serialize Plain $ fromRight undefined $ swap (lawLhs l) (lawRhs l) x
+"((p&q)|(p&r))"
+ghci> 
+ghci> x = f "(p&(!q|r))"
+ghci> serialize Plain x
+"(p&(!q|r))"
+ghci> serialize Plain $ fromRight undefined $ swap (lawLhs l) (lawLhs l) x
+"(p&(!q|r))"
+ghci> serialize Plain $ fromRight undefined $ swap (lawLhs l) (lawRhs l) x
+"((p&!q)|(p&r))"
+-}