From 7eeb59c0e3b73bce82fc0a75045f838573ae379f Mon Sep 17 00:00:00 2001 From: hi Date: Fri, 8 Aug 2025 08:14:37 +0000 Subject: [PATCH] logical laws --- Logic/Statement/Laws.hs | 163 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 163 insertions(+) create mode 100644 Logic/Statement/Laws.hs diff --git a/Logic/Statement/Laws.hs b/Logic/Statement/Laws.hs new file mode 100644 index 0000000..43855be --- /dev/null +++ b/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))" +-}