verify graph path search

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]
+type GetEdges vertex edge = vertex -> [(vertex, edge)]
-bfs goal start getEdges = reverse <$> aux [([], start)] mempty
+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

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)

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

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
+ghci> ConcatShowList <$> resolveDerivation deriveMIIUII
-Right [M,I,I,U,I,I]
+Right MIIUII
 -}

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 "dbl_neg"         "A"         "!!A"
-  , mkLaw "and_comm" "(A&B)" "(B&A)"
+  , mkLaw "and_comm"        "(A&B)"     "(B&A)"
-  , mkLaw "or_comm"  "(A|B)" "(B|A)"
+  , mkLaw "or_comm"         "(A|B)"     "(B|A)"
-  , mkLaw "and_assoc" "(A&(B&C))" "((A&B)&C)"
+  , mkLaw "and_assoc"       "(A&(B&C))" "((A&B)&C)"
-  , mkLaw "or_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 "and_or_distrib"  "(A&(B|C))" "((A&B)|(A&C))"
-  , mkLaw "or_and_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 "and_symm_eq"     "A"         "(A&A)"
-  , mkLaw "or_symm_eq"  "A" "(A|A)"
+  , mkLaw "or_symm_eq"      "A"         "(A|A)"
-  , mkLaw "not_and_distrib" "!(A&B)" "(!A|!B)"
+  , mkLaw "not_and_distrib" "!(A&B)"    "(!A|!B)"
-  , mkLaw "not_or_distrib"  "!(A|B)" "(!A&!B)"
+  , mkLaw "not_or_distrib"  "!(A|B)"    "(!A&!B)"
-  , mkLaw "implies_or"  "(A->B)" "(!A|B)"
+  , mkLaw "implies_or"      "(A->B)"    "(!A|B)"
-  , mkLaw "implies_and" "(A->B)" "!(A&!B)"
+  , mkLaw "implies_and"     "(A->B)"    "!(A&!B)"
-  , mkLaw "or_contr_eq" "A" "(A|(B&!B))"
+  , mkLaw "or_contr_eq"     "A"         "(A|(B&!B))"
-  , mkLaw "and_or_cancel" "A" "(A&(A|B))"
+  , mkLaw "and_or_cancel"   "A"         "(A&(A|B))"
-  , mkLaw "or_and_cancel" "A" "(A|(A&B))"
+  , mkLaw "or_and_cancel"   "A"         "(A|(A&B))"
-  , mkLaw "iff_and" "(A<->B)" "((A->B)&(B->A))"
+  , mkLaw "iff_and"         "(A<->B)"   "((A->B)&(B->A))"
-  , mkLaw "iff_or"  "(A<->B)" "((A&B)|(!A&!B))"
+  , 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

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)