diff --git a/Logic/Graph.hs b/Logic/Graph.hs index ba899ae..ad86164 100644 --- a/Logic/Graph.hs +++ b/Logic/Graph.hs @@ -2,23 +2,31 @@ module Logic.Graph where import Data.Set (Set, insert) -bfs :: (Eq a, Ord a) => a -> a -> (a -> [(edge, a)]) -> Maybe [edge] -bfs goal start getEdges = reverse <$> aux [([], start)] mempty +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 where aux [] _ = Nothing - aux ((path, vertex):queue) visited + aux ((vertex, path):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 (\(edge, next) -> (edge:path, next)) new + let queue' = queue ++ map (\(next, edge) -> (next, edge:path)) new in aux queue' $ insert vertex visited - ((edge, _):_) -> Just (edge:path) + ((_, edge):_) -> Just (edge:path) getUnvisitedAdjacent vertex visited = - filter (\(edge, next) -> not $ next `elem` visited) $ + filter (\(next, edge) -> not $ next `elem` visited) $ getEdges vertex {- @@ -27,3 +35,21 @@ 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 3d472f4..edfa03d 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 a => Show (ConcatShowList a) where +instance Show symbol => Show (ConcatShowList symbol) 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 3b34950..ba329fd 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 - | s2 == s1a -> Just $ fromJust $ serializeL s1b + | s1a == s2 -> Just $ fromJust $ serializeL s1b | otherwise -> Nothing _ -> Nothing where @@ -142,6 +142,7 @@ 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 73f0c49..70f056f 100644 --- a/Logic/Language/Impl/MIU.hs +++ b/Logic/Language/Impl/MIU.hs @@ -1,4 +1,4 @@ -module Logic.Language.Impl.M where +module Logic.Language.Impl.MIU where import Logic.Language (Language(..), ConcatShowList(..)) import Logic.Language.Derivation (Derivation(..)) @@ -80,6 +80,6 @@ deriveMIIUII = {- ghci> import Logic.Language.Derivation (resolveDerivation) -ghci> resolveDerivation deriveMIIUII -Right [M,I,I,U,I,I] +ghci> ConcatShowList <$> resolveDerivation deriveMIIUII +Right MIIUII -} diff --git a/Logic/Statement/Laws.hs b/Logic/Statement/Laws.hs index d1d5224..1b0b808 100644 --- a/Logic/Statement/Laws.hs +++ b/Logic/Statement/Laws.hs @@ -15,6 +15,11 @@ 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{" @@ -29,28 +34,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))" ] {- @@ -219,7 +224,7 @@ data LawsGraphEdge = LawsGraphEdge { lgeLaw :: Law , lgeReverse :: Bool , lgeIndex :: Integer - } + } deriving Eq instance Show LawsGraphEdge where show edge = @@ -231,14 +236,15 @@ instance Show LawsGraphEdge where <> "}" bfsLaws :: Statement -> Statement -> Maybe [LawsGraphEdge] -bfsLaws goal start = bfs goal start getLawsGraphEdges +bfsLaws = bfs getLawsGraphEdges -getLawsGraphEdges :: Statement -> [(LawsGraphEdge, Statement)] +getLawsGraphEdges :: Statement -> [(Statement, LawsGraphEdge)] 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 [(LawsGraphEdge, Statement)] + aux :: Law -> Either ReplaceError [(Statement, LawsGraphEdge)] aux law = do forward <- direction law lawLhs lawRhs False reverse <- direction law lawRhs lawLhs True @@ -249,7 +255,7 @@ getLawsGraphEdges s = concat $ rights $ map aux laws -> (Law -> Statement) -> (Law -> Statement) -> Bool - -> Either ReplaceError [(LawsGraphEdge, Statement)] + -> Either ReplaceError [(Statement, LawsGraphEdge)] direction law mkPattern1 mkPattern2 isReverse = do replaceds <- replace (mkPattern1 law) (mkPattern2 law) s return $ @@ -260,7 +266,7 @@ getLawsGraphEdges s = concat $ rights $ map aux laws , lgeReverse = isReverse , lgeIndex = index } - in (edge, s') + in (s', edge) {- ghci> fromString x = fromRight undefined $ eof stmt $ mkInput x diff --git a/Logic/readme.md b/Logic/readme.md index 7546cf3..f4515e3 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)