root/logic
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

logical laws: breadth first search

Browse source
This commit is contained in:
hi 2025-08-12 04:00:03 +00:00
parent be7460ddf1
commit b28263fdc3
1 changed files with 86 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

87
Logic/Statement/Laws.hs
View file

@ -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
-}