logical laws: breadth first search

edges are dynamically generated

Logic/Graph.hs

@@ -0,0 +1,27 @@
+module Logic.Graph where
+
+bfs :: Eq a => a -> a -> (a -> [(edge, a)]) -> Maybe [edge]
+bfs goal start getEdges = reverse <$> aux [([], start)] []
+  where
+    aux [] _ = Nothing
+    aux ((path, vertex):queue) visited
+      | vertex == goal = Just path
+      | otherwise =
+        let new = getUnvisitedAdjacent vertex visited
+        in
+          case filter (\(_, v) -> v == goal) new of
+            [] ->
+              let queue' = queue ++ map (\(edge, next) -> (edge:path, next)) new
+              in aux queue' (vertex:visited)
+            ((edge, _):_) -> Just (edge:path)
+
+    getUnvisitedAdjacent vertex visited =
+      filter (\(edge, next) -> not $ next `elem` visited) $
+      getEdges vertex
+
+{-
+ghci> bfs 10 0 (\x -> [("pred", x-1), ("succ", x+1)])
+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"]
+-}

Logic/Language/Impl/L.hs

@@ -151,3 +151,12 @@ deriveLExample1 = step5
     step3 = Infer2 0 0 step2 step1
     step4 = Axiom3 0 [Variable 0] [Variable 1] [Variable 2]
     step5 = Infer2 0 0 step4 step3
+
+deriveLExample2 :: Derivation AlphaL
+deriveLExample2 = step5
+  where
+    step1 = Axiom2 0 [Variable 0] [Open, Variable 0, Arrow, Variable 0, Close]
+    step2 = Axiom3 0 [Variable 0] [Open, Variable 0, Arrow, Variable 0, Close] [Variable 0]
+    step3 = Infer2 0 0 step2 step1
+    step4 = Axiom2 0 [Variable 0] [Variable 0]
+    step5 = Infer2 0 0 step3 step4

Logic/Statement.hs

@@ -20,3 +20,11 @@ atoms = toAscList . mkSet
     mkSet (Or s1 s2)      = union (mkSet s1) (mkSet s2)
     mkSet (Implies s1 s2) = union (mkSet s1) (mkSet s2)
     mkSet (Iff s1 s2)     = union (mkSet s1) (mkSet s2)
+
+substatements :: Statement -> [Statement]
+substatements s@(Atom _) = [s]
+substatements s@(Not s1) = s:(substatements s1)
+substatements s@(And s1 s2)     = (s:) $ substatements s1 ++ substatements s2
+substatements s@(Or s1 s2)      = (s:) $ substatements s1 ++ substatements s2
+substatements s@(Implies s1 s2) = (s:) $ substatements s1 ++ substatements s2
+substatements s@(Iff s1 s2)     = (s:) $ substatements s1 ++ substatements s2

Logic/Statement/Laws.hs

@@ -3,8 +3,9 @@ module Logic.Statement.Laws where
 import Logic.Parse (eof, mkInput)
 import Logic.Statement (Statement(..))
 import Logic.Statement.Parse (stmt)
+import Logic.Graph (bfs)
 
-import Data.Either (fromRight)
+import Data.Either (fromRight, rights)
 import Data.Maybe (fromJust, listToMaybe)
 
 data Law = Law
@@ -41,6 +42,12 @@ laws =
   , mkLaw "iff_or"  "(A<->B)" "((A&B)|(!A&!B))"
   ]
 
+{-
+ghci> import Logic.Statement.Eval (bucket, Bucket(Tautology))
+ghci> all (== Tautology) $ map (\law -> bucket $ Iff (lawLhs law) (lawRhs law)) laws
+True
+-}
+
 lookupLaw :: String -> Maybe Law
 lookupLaw name = listToMaybe $ filter (\law -> lawName law == name) laws
 
@@ -48,7 +55,7 @@ match
   :: Statement
   -- ^ pattern
   -> Statement
-  -- ^ statement to search
+  -- ^ statement to search within
   -> Maybe [(String, Statement)]
   -- ^ mapping from pattern-statement atoms to search-statement parts
 match = aux []
@@ -104,19 +111,20 @@ Just [("C",Atom "r"),("B",Atom "q"),("A",Atom "p")]
 -}
 
 data SwapError
-  = Indeterminate
+  = IndeterminateSwap
   -- ^ An atom in p2 doesn't exist in p1.
   -- Strictly: an atom in p2 doesn't exist in the result from `match`
   -- (matters only if `match` is implemented incorrectly).
-  -- If for atoms we used terms of a type instead of strings,
-  -- we could avoid needing this error.
+  -- Theoretically if for atoms we used terms of a type instead of strings, we
+  -- could avoid needing this error, but I think we still wouldn't be able
+  -- to return a mapping from atom-type-1 to atom-type-2 in a type safe way.
   | NonMatchingPattern
   deriving Show
 
 swap :: Statement -> Statement -> Statement -> Either SwapError Statement
 swap p1 p2 s = do
   mapping <- maybe (Left NonMatchingPattern) Right $ match p1 s
-  maybe (Left Indeterminate) Right $ aux mapping p2
+  maybe (Left IndeterminateSwap) Right $ aux mapping p2
   where
     aux :: [(String, Statement)] -> Statement -> Maybe Statement
     aux mapping (Atom key) = lookup key mapping
@@ -161,3 +169,121 @@ ghci> serialize Plain $ fromRight undefined $ swap (lawLhs l) (lawLhs l) x
 ghci> serialize Plain $ fromRight undefined $ swap (lawLhs l) (lawRhs l) x
 "((p&!q)|(p&r))"
 -}
+
+data ReplaceError
+  = IndeterminateReplace
+  deriving Show
+
+replace :: Statement -> Statement -> Statement -> Either ReplaceError [Statement]
+replace p1 p2 = firstLeft . aux
+  where
+    aux :: Statement -> [Either ReplaceError Statement]
+    aux s =
+      case swap p1 p2 s of
+        Left IndeterminateSwap -> [Left IndeterminateReplace]
+        -- ^ terminate here because in `replace` we stop at the first Left
+        Left NonMatchingPattern -> deeper s
+        Right s' -> (Right s'):(deeper s)
+
+    deeper :: Statement -> [Either ReplaceError Statement]
+    deeper (Atom key) = []
+    deeper (Not s) = do
+      e <- aux s
+      return $ Not <$> e
+    deeper (And     s1 s2) = binary And     s1 s2
+    deeper (Or      s1 s2) = binary Or      s1 s2
+    deeper (Implies s1 s2) = binary Implies s1 s2
+    deeper (Iff     s1 s2) = binary Iff     s1 s2
+
+    binary constructor s1 s2 =
+      [constructor <$> e1 <*> (Right s2) | e1 <- aux s1] ++
+      [constructor <$> (Right s1) <*> e2 | e2 <- aux s2]
+
+firstLeft :: [Either a b] -> Either a [b]
+firstLeft [] = Right []
+firstLeft ((Left a):_) = Left a
+firstLeft ((Right b):xs) = (b:) <$> firstLeft xs
+
+data LawsGraphEdge = LawsGraphEdge
+  { lgeLaw :: Law
+  , lgeReverse :: Bool
+  , lgeIndex :: Integer
+  } deriving (Eq, Show)
+
+bfsLaws :: Statement -> Statement -> Maybe [LawsGraphEdge]
+bfsLaws goal start = bfs goal start getLawsGraphEdges
+
+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
+  where
+    aux :: Law -> Either ReplaceError [(LawsGraphEdge, Statement)]
+    aux law = do
+      forward <- direction law lawLhs lawRhs False
+      reverse <- direction law lawRhs lawLhs True
+      return $ forward ++ reverse
+
+    direction
+      :: Law
+      -> (Law -> Statement)
+      -> (Law -> Statement)
+      -> Bool
+      -> Either ReplaceError [(LawsGraphEdge, Statement)]
+    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 (edge, s')
+
+{-
+ghci> fromString x = fromRight undefined $ eof stmt $ mkInput x
+ghci> niceEdges = map (\edge -> (if lgeReverse edge then "< " else "> ") <> lawName (lgeLaw edge) <> " " <> show (lgeIndex edge))
+ghci> 
+ghci> niceEdges <$> bfsLaws (fromString "(p|!q)") (fromString "(p|!q)")
+Just []
+ghci> niceEdges <$> bfsLaws (fromString "!!(p|!q)") (fromString "(p|!q)")
+Just ["> dbl_neg 0"]
+ghci> niceEdges <$> bfsLaws (fromString "(!!p|!q)") (fromString "(p|!q)")
+Just ["> dbl_neg 1"]
+ghci> niceEdges <$> bfsLaws (fromString "(p|!!!q)") (fromString "(p|!q)")
+Just ["> dbl_neg 2"]
+ghci> niceEdges <$> bfsLaws (fromString "(p|p)") (fromString "p")
+Just ["> or_symm_eq 0"]
+ghci> niceEdges <$> bfsLaws (fromString "p") (fromString "(p|p)")
+Just ["< or_symm_eq 0"]
+ghci> 
+ghci> niceEdges <$> bfsLaws (fromString "!(!p&(q|q))") (fromString "(p|!q)")
+Just ["> dbl_neg 1","> or_symm_eq 5","< not_and_distrib 0"]
+ghci> niceEdges <$> bfsLaws (fromString "!(!(p&p)&(q|q))") (fromString "(p|!q)")
+Just ["> dbl_neg 1","> and_symm_eq 3","> or_symm_eq 7","< not_and_distrib 0"]
+ghci> 
+ghci> import Data.Time.POSIX (getPOSIXTime)
+ghci> time f = getPOSIXTime >>= \t0 -> f >> getPOSIXTime >>= \t1 -> return $ t1 - t0
+ghci> time $ putStrLn $ show $ niceEdges <$> bfsLaws (fromString "p") (fromString "p")
+Just []
+0.000087114s
+ghci> time $ putStrLn $ show $ niceEdges <$> bfsLaws (fromString "!!p") (fromString "p")
+Just ["> dbl_neg 0"]
+0.000201159s
+ghci> time $ putStrLn $ show $ niceEdges <$> bfsLaws (fromString "!!!!p") (fromString "p")
+Just ["> dbl_neg 0","> dbl_neg 0"]
+0.000444047s
+ghci> time $ putStrLn $ show $ niceEdges <$> bfsLaws (fromString "!!!!!!p") (fromString "p")
+Just ["> dbl_neg 0","> dbl_neg 0","> dbl_neg 0"]
+0.001260947s
+ghci> time $ putStrLn $ show $ niceEdges <$> bfsLaws (fromString "!!!!!!!!p") (fromString "p")
+Just ["> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0"]
+0.021864298s
+ghci> time $ putStrLn $ show $ niceEdges <$> bfsLaws (fromString "!!!!!!!!!!p") (fromString "p")
+Just ["> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0"]
+3.244101767s
+Just ["> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0","> dbl_neg 0"]
+3066.211460539s
+-}