From 0d13b807f00776ec0346dcadb6d9fc5d0c868a2f Mon Sep 17 00:00:00 2001
From: hi <hi>
Date: Tue, 12 Aug 2025 03:56:04 +0000
Subject: [PATCH 1/5] another L derivation example

---
 Logic/Language/Impl/L.hs | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/Logic/Language/Impl/L.hs b/Logic/Language/Impl/L.hs
index 6559e46..3b34950 100644
--- a/Logic/Language/Impl/L.hs
+++ b/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

From d0ba6ce9d4e1fd76784c06c8e86da7029ad3d713 Mon Sep 17 00:00:00 2001
From: hi <hi>
Date: Tue, 12 Aug 2025 03:57:13 +0000
Subject: [PATCH 2/5] minor: substatements function, comments

---
 Logic/Statement.hs      |  8 ++++++++
 Logic/Statement/Laws.hs | 17 ++++++++++++-----
 2 files changed, 20 insertions(+), 5 deletions(-)

diff --git a/Logic/Statement.hs b/Logic/Statement.hs
index 6902140..f85fe26 100644
--- a/Logic/Statement.hs
+++ b/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
diff --git a/Logic/Statement/Laws.hs b/Logic/Statement/Laws.hs
index 43855be..b38b1ed 100644
--- a/Logic/Statement/Laws.hs
+++ b/Logic/Statement/Laws.hs
@@ -41,6 +41,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 +54,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 +110,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

From 0e7bca0baa60ea63e350c082b6f1be1aca3a97fa Mon Sep 17 00:00:00 2001
From: hi <hi>
Date: Tue, 12 Aug 2025 03:59:40 +0000
Subject: [PATCH 3/5] apply logical laws

---
 Logic/Statement/Laws.hs | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)

diff --git a/Logic/Statement/Laws.hs b/Logic/Statement/Laws.hs
index b38b1ed..0209a51 100644
--- a/Logic/Statement/Laws.hs
+++ b/Logic/Statement/Laws.hs
@@ -168,3 +168,37 @@ 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

From be7460ddf16c70054bf3b632b364ae1abda5fca4 Mon Sep 17 00:00:00 2001
From: hi <hi>
Date: Tue, 12 Aug 2025 03:58:25 +0000
Subject: [PATCH 4/5] breadth first search

edges are dynamically generated
---
 Logic/Graph.hs | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)
 create mode 100644 Logic/Graph.hs

diff --git a/Logic/Graph.hs b/Logic/Graph.hs
new file mode 100644
index 0000000..0aa3be4
--- /dev/null
+++ b/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"]
+-}

From b28263fdc372c4796d77a31498de795711c1cbaf Mon Sep 17 00:00:00 2001
From: hi <hi>
Date: Tue, 12 Aug 2025 04:00:03 +0000
Subject: [PATCH 5/5] logical laws: breadth first search

---
 Logic/Statement/Laws.hs | 87 ++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 86 insertions(+), 1 deletion(-)

diff --git a/Logic/Statement/Laws.hs b/Logic/Statement/Laws.hs
index 0209a51..7ac692a 100644
--- a/Logic/Statement/Laws.hs
+++ b/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
@@ -202,3 +203,87 @@ 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
+-}