diff --git a/Logic/Graph.hs b/Logic/Graph.hs index ad86164..ba899ae 100644 --- a/Logic/Graph.hs +++ b/Logic/Graph.hs @@ -2,31 +2,23 @@ module Logic.Graph where import Data.Set (Set, insert) -type GetEdges vertex edge = vertex -> [(vertex, edge)] -type GetEdgesCosts vertex edge cost = vertex -> [((vertex, edge), cost)] - -bfs - :: (Eq vertex, Ord vertex) - => GetEdges vertex edge - -> vertex - -> vertex - -> Maybe [edge] -bfs getEdges goal start = reverse <$> aux [(start, [])] mempty +bfs :: (Eq a, Ord a) => a -> a -> (a -> [(edge, a)]) -> Maybe [edge] +bfs goal start getEdges = reverse <$> aux [([], start)] mempty where aux [] _ = Nothing - aux ((vertex, path):queue) visited + aux ((path, vertex):queue) visited | vertex == goal = Just path | otherwise = let new = getUnvisitedAdjacent vertex visited in - case filter (\(v, _) -> v == goal) new of + case filter (\(_, v) -> v == goal) new of [] -> - let queue' = queue ++ map (\(next, edge) -> (next, edge:path)) new + let queue' = queue ++ map (\(edge, next) -> (edge:path, next)) new in aux queue' $ insert vertex visited - ((_, edge):_) -> Just (edge:path) + ((edge, _):_) -> Just (edge:path) getUnvisitedAdjacent vertex visited = - filter (\(next, edge) -> not $ next `elem` visited) $ + filter (\(edge, next) -> not $ next `elem` visited) $ getEdges vertex {- @@ -35,21 +27,3 @@ Just ["succ","succ","succ","succ","succ","succ","succ","succ","succ","succ"] ghci> bfs 13 0 (\x -> [("double", x+x), ("add", x+1)]) Just ["add","double","add","double","double","add"] -} - -data VerifyPathError vertex edge - = NoSuchEdge vertex edge - -verifyPath - :: (Eq vertex, Ord vertex, Eq edge) - => GetEdges vertex edge - -> vertex - -> vertex - -> [edge] - -> Either (VerifyPathError vertex edge) Bool -verifyPath getEdges goal start path = - case path of - [] -> Right $ start == goal - (thisEdge:nextEdges) -> - case map fst $ filter (\(next, realEdge) -> realEdge == thisEdge) $ getEdges start of - [] -> Left $ NoSuchEdge start thisEdge - (next:_) -> verifyPath getEdges goal next nextEdges diff --git a/Logic/Language.hs b/Logic/Language.hs index edfa03d..3d472f4 100644 --- a/Logic/Language.hs +++ b/Logic/Language.hs @@ -2,7 +2,7 @@ module Logic.Language where -- Convenience newtype so strings of symbols are less ugly newtype ConcatShowList symbol = ConcatShowList [symbol] -instance Show symbol => Show (ConcatShowList symbol) where +instance Show a => Show (ConcatShowList a) where show (ConcatShowList xs) = concat $ map show xs -- Formal language (/grammar/production system/whatever) diff --git a/Logic/Language/Impl/L.hs b/Logic/Language/Impl/L.hs index ba329fd..3b34950 100644 --- a/Logic/Language/Impl/L.hs +++ b/Logic/Language/Impl/L.hs @@ -93,7 +93,7 @@ lRule1 theorem1 theorem2 = maybeToList $ do s2 <- fromEither $ eof parseL $ mkInput theorem2 case s1 of Implies s1a s1b - | s1a == s2 -> Just $ fromJust $ serializeL s1b + | s2 == s1a -> Just $ fromJust $ serializeL s1b | otherwise -> Nothing _ -> Nothing where @@ -142,7 +142,6 @@ serializeL (Implies s1 s2) = do l1 <- serializeL s1 l2 <- serializeL s2 return $ [Open] ++ l1 ++ [Arrow] ++ l2 ++ [Close] -serializeL _ = Nothing deriveLExample1 :: Derivation AlphaL deriveLExample1 = step5 diff --git a/Logic/Language/Impl/MIU.hs b/Logic/Language/Impl/MIU.hs index 70f056f..73f0c49 100644 --- a/Logic/Language/Impl/MIU.hs +++ b/Logic/Language/Impl/MIU.hs @@ -1,4 +1,4 @@ -module Logic.Language.Impl.MIU where +module Logic.Language.Impl.M where import Logic.Language (Language(..), ConcatShowList(..)) import Logic.Language.Derivation (Derivation(..)) @@ -80,6 +80,6 @@ deriveMIIUII = {- ghci> import Logic.Language.Derivation (resolveDerivation) -ghci> ConcatShowList <$> resolveDerivation deriveMIIUII -Right MIIUII +ghci> resolveDerivation deriveMIIUII +Right [M,I,I,U,I,I] -} diff --git a/Logic/Statement/Laws.hs b/Logic/Statement/Laws.hs index 1b0b808..d1d5224 100644 --- a/Logic/Statement/Laws.hs +++ b/Logic/Statement/Laws.hs @@ -15,11 +15,6 @@ data Law = Law , lawRhs :: Statement } -instance Eq Law where - law1 == law2 = - lawLhs law1 == lawLhs law2 - && lawRhs law1 == lawRhs law2 - instance Show Law where show law = "Law{" @@ -34,28 +29,28 @@ 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 + 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))" + [ 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))" ] {- @@ -224,7 +219,7 @@ data LawsGraphEdge = LawsGraphEdge { lgeLaw :: Law , lgeReverse :: Bool , lgeIndex :: Integer - } deriving Eq + } instance Show LawsGraphEdge where show edge = @@ -236,15 +231,14 @@ instance Show LawsGraphEdge where <> "}" bfsLaws :: Statement -> Statement -> Maybe [LawsGraphEdge] -bfsLaws = bfs getLawsGraphEdges +bfsLaws goal start = bfs goal start getLawsGraphEdges -getLawsGraphEdges :: Statement -> [(Statement, LawsGraphEdge)] +getLawsGraphEdges :: Statement -> [(LawsGraphEdge, Statement)] getLawsGraphEdges s = concat $ rights $ map aux laws -- ^ `rights` here because we can't apply -- e.g. or_contr_eq forwards without inventing B - -- and the `Left` case is `Left IndeterminateReplace` where - aux :: Law -> Either ReplaceError [(Statement, LawsGraphEdge)] + aux :: Law -> Either ReplaceError [(LawsGraphEdge, Statement)] aux law = do forward <- direction law lawLhs lawRhs False reverse <- direction law lawRhs lawLhs True @@ -255,7 +249,7 @@ getLawsGraphEdges s = concat $ rights $ map aux laws -> (Law -> Statement) -> (Law -> Statement) -> Bool - -> Either ReplaceError [(Statement, LawsGraphEdge)] + -> Either ReplaceError [(LawsGraphEdge, Statement)] direction law mkPattern1 mkPattern2 isReverse = do replaceds <- replace (mkPattern1 law) (mkPattern2 law) s return $ @@ -266,7 +260,7 @@ getLawsGraphEdges s = concat $ rights $ map aux laws , lgeReverse = isReverse , lgeIndex = index } - in (s', edge) + in (edge, s') {- ghci> fromString x = fromRight undefined $ eof stmt $ mkInput x diff --git a/Logic/readme.md b/Logic/readme.md index f4515e3..7546cf3 100644 --- a/Logic/readme.md +++ b/Logic/readme.md @@ -33,14 +33,14 @@ things that are in here: - generate a LaTeX truth table from a statement -## syntactic things - ### [Logic.Statements.Laws](Statements/Laws.hs) - match/replace patterns in statements (e.g. logical laws) - verify logical-law equivalence of statements (TODO) - find logical-law equivalence of statements with breadth-first search (slow) +## syntactic things + ### [Logic.Language](Language.hs) - implement formal languages (symbols, axioms schemas, and inference rules)