Logic/Graph.hs

@@ -2,31 +2,23 @@ module Logic.Graph where
 
 import Data.Set (Set, insert)
 
-type GetEdges vertex edge = vertex -> [(vertex, edge)]
+bfs :: (Eq a, Ord a) => a -> a -> (a -> [(edge, a)]) -> Maybe [edge]
-type GetEdgesCosts vertex edge cost = vertex -> [((vertex, edge), cost)]
+bfs goal start getEdges = reverse <$> aux [([], start)] mempty
-
-bfs
-  :: (Eq vertex, Ord vertex)
-  => GetEdges vertex edge
-  -> vertex
-  -> vertex
-  -> Maybe [edge]
-bfs getEdges goal start = 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

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)

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

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

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 "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))"
   ]
 
 {-
@@ -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

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)