From e8a5e2caa795d8afde1d54e75db02226695ef313 Mon Sep 17 00:00:00 2001 From: hi Date: Fri, 15 Aug 2025 11:35:50 +0000 Subject: [PATCH] verify graph paths incl laws graph --- Logic/Graph.hs | 27 +++++++++---- Logic/Statement/Laws.hs | 85 ++++++++++++++++++++++++++++++----------- Logic/readme.md | 3 +- 3 files changed, 84 insertions(+), 31 deletions(-) diff --git a/Logic/Graph.hs b/Logic/Graph.hs index ad86164..cdc4091 100644 --- a/Logic/Graph.hs +++ b/Logic/Graph.hs @@ -38,6 +38,8 @@ Just ["add","double","add","double","double","add"] data VerifyPathError vertex edge = NoSuchEdge vertex edge + | GoalNotReached [vertex] + deriving Show verifyPath :: (Eq vertex, Ord vertex, Eq edge) @@ -45,11 +47,22 @@ verifyPath -> vertex -> vertex -> [edge] - -> Either (VerifyPathError vertex edge) Bool + -> Either (VerifyPathError vertex edge) [vertex] 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 + case aux start path of + Right (vertices, True) -> Right vertices + Right (vertices, False) -> Left $ GoalNotReached vertices + Left x -> Left x + where + aux vertex path' = cons vertex <$> + case path' of + [] -> Right $ + if vertex == goal + then ([], True) + else ([], False) + (thisEdge:nextEdges) -> + case map fst $ filter (\(next, realEdge) -> realEdge == thisEdge) $ getEdges vertex of + [] -> Left $ NoSuchEdge vertex thisEdge + (next:_) -> aux next nextEdges + + cons vertex (vertices, bool) = (vertex:vertices, bool) diff --git a/Logic/Statement/Laws.hs b/Logic/Statement/Laws.hs index 1b0b808..cd5ccf6 100644 --- a/Logic/Statement/Laws.hs +++ b/Logic/Statement/Laws.hs @@ -4,7 +4,7 @@ import Logic.Parse (eof, mkInput) import Logic.Statement (Statement(..)) import Logic.Statement.Parse (stmt) import Logic.Statement.Serialize (serialize, SerializeFormat(Plain)) -import Logic.Graph (bfs) +import Logic.Graph (bfs, verifyPath, VerifyPathError) import Data.Either (fromRight, rights) import Data.Maybe (fromJust, listToMaybe) @@ -220,16 +220,25 @@ firstLeft [] = Right [] firstLeft ((Left a):_) = Left a firstLeft ((Right b):xs) = (b:) <$> firstLeft xs +data Direction + = Forward + | Reverse + deriving (Eq, Show) + data LawsGraphEdge = LawsGraphEdge - { lgeLaw :: Law - , lgeReverse :: Bool + { lgeDirection :: Direction , lgeIndex :: Integer + , lgeLaw :: Law } deriving Eq instance Show LawsGraphEdge where show edge = "LawsGraphEdge{" - <> (if lgeReverse edge then "< " else "> ") + <> ( + case lgeDirection edge of + Forward -> "> " + Reverse -> "< " + ) <> lawName (lgeLaw edge) <> " " <> show (lgeIndex edge) @@ -246,27 +255,26 @@ getLawsGraphEdges s = concat $ rights $ map aux laws where aux :: Law -> Either ReplaceError [(Statement, LawsGraphEdge)] aux law = do - forward <- direction law lawLhs lawRhs False - reverse <- direction law lawRhs lawLhs True + forward <- edges Forward law + reverse <- edges Reverse law return $ forward ++ reverse - direction - :: Law - -> (Law -> Statement) - -> (Law -> Statement) - -> Bool - -> Either ReplaceError [(Statement, LawsGraphEdge)] - direction law mkPattern1 mkPattern2 isReverse = do - replaceds <- replace (mkPattern1 law) (mkPattern2 law) s - return $ - (flip map) (zip [0..] replaceds) $ \(index, s') -> - let - edge = LawsGraphEdge - { lgeLaw = law - , lgeReverse = isReverse - , lgeIndex = index - } - in (s', edge) + replaceds :: Direction -> Law -> Either ReplaceError [Statement] + replaceds direction law = + let + (pattern1, pattern2) = + case direction of + Forward -> (lawLhs law, lawRhs law) + Reverse -> (lawRhs law, lawLhs law) + in replace pattern1 pattern2 s + + mkEdges :: Direction -> Law -> [Statement] -> [(Statement, LawsGraphEdge)] + mkEdges direction law statements = do + (index, s') <- zip [0..] statements + return (s', LawsGraphEdge direction index law) + + edges :: Direction -> Law -> Either ReplaceError [(Statement, LawsGraphEdge)] + edges direction law = mkEdges direction law <$> replaceds direction law {- ghci> fromString x = fromRight undefined $ eof stmt $ mkInput x @@ -314,3 +322,34 @@ ghci> time $ putStrLn $ show $ niceEdges <$> bfsLaws (fromString "!!!!!!!!!!!!p" Just ["> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0"] 3066.211460539s -} + +data LawsGraphPath = LawsGraphPath + { lgpStart :: Statement + , lgpGoal :: Statement + , lgpEdges :: [LawsGraphEdge] + } deriving Show + +verifyLawsPath + :: LawsGraphPath + -> Either (VerifyPathError Statement LawsGraphEdge) [Statement] +verifyLawsPath path = + verifyPath getLawsGraphEdges (lgpGoal path) (lgpStart path) (lgpEdges path) + +lawsPathExample1 :: LawsGraphPath +lawsPathExample1 = LawsGraphPath start goal edges + where + start = Implies (Atom "p") (Atom "q") + goal = Implies (Not (Atom "q")) (Not (Atom "p")) + edges = + [ LawsGraphEdge Forward 1 $ law "dbl_neg" + , LawsGraphEdge Forward 0 $ law "implies_and" + , LawsGraphEdge Forward 0 $ law "and_comm" + , LawsGraphEdge Reverse 0 $ law "implies_and" + ] + law = fromJust . lookupLaw + +{- +ghci> import Logic.Statement.Serialize (serialize, SerializeFormat(..)) +ghci> map (serialize Plain) <$> verifyLawsPath lawsPathExample1 +Right ["(p->q)","(!!p->q)","!(!!p&!q)","!(!q&!!p)","(!q->!p)"] +-} diff --git a/Logic/readme.md b/Logic/readme.md index f4515e3..7a44487 100644 --- a/Logic/readme.md +++ b/Logic/readme.md @@ -9,6 +9,7 @@ things that are in here: ### [Logic.Graph](Graph.hs) - generic breadth-first search +- verify graph paths reach the goal and have all extant edges ## statement things @@ -38,7 +39,7 @@ things that are in here: ### [Logic.Statements.Laws](Statements/Laws.hs) - match/replace patterns in statements (e.g. logical laws) -- verify logical-law equivalence of statements (TODO) +- verify logical-law equivalence of statements - find logical-law equivalence of statements with breadth-first search (slow) ### [Logic.Language](Language.hs)