From 14b6d8ce5a7f256dba79882b752dbb08a48d372f Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Thu, 29 Jul 2021 14:54:52 +0200 Subject: [PATCH] Automatic counterexample handling --- app/Main.hs | 135 ++++++++++++++++++++++++++++----------- monoid-learner.cabal | 9 ++- src/Equivalence.hs | 85 ++++++++++++++++++++++++ src/Examples/Examples.hs | 107 +++++++++++++++++++++++++++++++ src/MStar.hs | 112 ++++++++++++++++++-------------- src/Monoid.hs | 49 ++++++++++++++ src/Word.hs | 35 ++++++++++ test/test.hs | 62 +++++++++++++++++- 8 files changed, 506 insertions(+), 88 deletions(-) create mode 100644 src/Equivalence.hs create mode 100644 src/Examples/Examples.hs create mode 100644 src/Monoid.hs create mode 100644 src/Word.hs diff --git a/app/Main.hs b/app/Main.hs index d61fa6a..ccef710 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -1,62 +1,118 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PartialTypeSignatures #-} +{-# OPTIONS_GHC -Wno-partial-type-signatures #-} + module Main where import Data.Foldable (Foldable (toList)) -import Data.IORef +import Data.IORef (IORef, modifyIORef', newIORef, readIORef) import qualified Data.Map as Map import qualified Data.Sequence as Seq import qualified Data.Set as Set -import KnuthBendix +import Equivalence (searchCounterexample) +import Examples.Examples +import KnuthBendix (knuthBendix, rewrite) import MStar +import Monoid +import Word (Word) +import Prelude hiding (Word) -- We use the alphabet {a, b} as always symbols :: Set.Set Char symbols = Set.fromList "ab" --- Example language L = { w | nonempty && even number of as && triple numbers of bs } -language :: MStar.Word Char -> Bool -language w = not (null w) && length aa `mod` 2 == 0 && length bb `mod` 3 == 0 - where - (aa, bb) = Seq.partition (== 'a') w +example :: MonoidAcceptor Char _ +example = + -- 1. the first example I tried: + mainExample + -- 2. a* or b*: + -- predSymbol (== 'a') `union` predSymbol (== 'b') + -- 3. just the word abba: + -- finiteLanguage (Set.fromList ["abba"]) -- Let's count the number of membership queries -- and print all the queries -languageM :: IORef Int -> MStar.Word Char -> IO Bool +languageM :: IORef Int -> Word Char -> IO Bool languageM count w = do modifyIORef' count succ n <- readIORef count let nstr = show n + wstr = toList w + r = acceptMonoid example w + putStr "m " putStr nstr - putStr (replicate (8 - length nstr) ' ') - putStrLn $ toList w - return $ language w + putStr (replicate (6 - length nstr) ' ') + putStr wstr + putStr (replicate (24 - length wstr) ' ') + print r + return r + +-- Let's count the number of equivalence queries +equiv :: _ => IORef Int -> MonoidAcceptor Char _ -> IO (Maybe (Word Char)) +equiv count m = do + modifyIORef' count succ + n <- readIORef count + let nstr = show n + r = searchCounterexample symbols m example + putStr "e " + putStr nstr + putStr (replicate (6 - length nstr) ' ') + print r + return r + +logger :: Show a => LogMessage a -> IO () +logger (NewRow w) = putStr "Adding row " >> print (toList w) +logger (NewContext (l, r)) = putStr "Adding context " >> print (toList l, toList r) +logger (Stage str) = putStr "Stage: " >> putStrLn str main :: IO () main = do putStrLn "Welcome to the monoid learner" - count <- newIORef 0 - let lang = languageM count + mqCount <- newIORef 0 + eqCount <- newIORef 0 + let lang = languageM mqCount + let equi = equiv eqCount -- Initialise s <- initialState symbols lang - -- make closed, consistent and associative - s2 <- learn lang s - -- Above hypothesis is trivial (accepts nothing) - -- Let's add a column so that aa can be reached - putStrLn "Adding counterexample aa" - s3 <- addContext (Seq.empty, Seq.singleton 'a') lang s2 - -- Make closed, consistent and associative again - s5 <- learn lang s3 - - -- Still wrong, on bbb - -- Let's add a column to reach it - putStrLn "Adding counterexample bbb" - s6 <- addContext (Seq.singleton 'b', Seq.singleton 'b') lang s5 - -- Make closed, consistent and associative again - s7 <- learn lang s6 + -- learn + (s2, m2) <- learn logger lang equi s -- Hypothesis is now correct - let sFinal = s7 + let sFinal = s2 + mFinal = m2 + + -- Print as multiplication table + + putStrLn "" + putStrLn "Monoid with the elements:" + putStr " " + print (elements mFinal) + + putStrLn "accepting elements:" + putStr " " + print (filter (accept mFinal) $ elements mFinal) + + putStrLn "unit element" + putStr " " + print (unit mFinal) + + putStrLn "multiplication table" + let multTable = (\x y -> (x, y, multiplication mFinal x y)) <$> elements mFinal <*> elements mFinal + mapM_ + ( \(x, y, z) -> do + putStr " " + putStr (show x) + putStr " x " + putStr (show y) + putStr " = " + print z + ) + multTable + + -- Print as monoid presentation + let -- Extract the rewrite rules from the table -- For this we simply look at products r1 r2 and see which row is equivalent to it rowPairs = Set.filter (\w -> not (w `Set.member` rows sFinal)) . Set.map (uncurry (<>)) $ Set.cartesianProduct (rows sFinal) (rows sFinal) @@ -68,14 +124,21 @@ main = do accRows0 = Set.filter (\m -> row sFinal m Map.! (Seq.empty, Seq.empty)) $ rows sFinal accRows = Set.map (rewrite kbRules) accRows0 + putStrLn "" putStrLn "Monoid on the generators:" putStr " " - print symbols + print (fmap (: []) (toList symbols)) + + putStrLn "accepting strings:" + putStr " " + print (fmap toList (toList accRows)) putStrLn "with equations:" - putStr " " - print kbRules - - putStrLn "and accepting strings:" - putStr " " - print accRows + mapM_ + ( \(l, r) -> do + putStr " " + putStr (toList l) + putStr " = " + putStrLn (toList r) + ) + kbRules \ No newline at end of file diff --git a/monoid-learner.cabal b/monoid-learner.cabal index eead39e..e04f5d9 100644 --- a/monoid-learner.cabal +++ b/monoid-learner.cabal @@ -16,8 +16,12 @@ library import: stuff hs-source-dirs: src exposed-modules: + Equivalence, + Examples.Examples, KnuthBendix, - MStar + Monoid, + MStar, + Word executable monoid-learner import: stuff @@ -34,4 +38,5 @@ test-suite test type: exitcode-stdio-1.0 build-depends: monoid-learner, - hedgehog + tasty, + tasty-hunit diff --git a/src/Equivalence.hs b/src/Equivalence.hs new file mode 100644 index 0000000..733a172 --- /dev/null +++ b/src/Equivalence.hs @@ -0,0 +1,85 @@ +{-# LANGUAGE PartialTypeSignatures #-} + +module Equivalence where + +import qualified Data.Map as Map +import Data.Sequence (Seq (..)) +import qualified Data.Sequence as Seq +import Data.Set (Set) +import qualified Data.Set as Set +import Monoid (MonoidAcceptor (..)) + +equivalent :: (Ord q1, Ord q2) => Set a -> MonoidAcceptor a q1 -> MonoidAcceptor a q2 -> Bool +equivalent alphabet m1 m2 = case searchCounterexample alphabet m1 m2 of + Just _ -> False + Nothing -> True + +searchCounterexample :: (Ord q1, Ord q2) => Set a -> MonoidAcceptor a q1 -> MonoidAcceptor a q2 -> Maybe (Seq a) +searchCounterexample alphabet m1 m2 = go workingSet Map.empty + where + workingSet = (unit m1, unit m2, Seq.Empty) :<| fmap (\a -> (alph m1 a, alph m2 a, Seq.singleton a)) (foldMap Seq.singleton alphabet) + go Empty visited = Nothing + go ((e1, e2, w) :<| todo) visited + -- If the pair is already visited, we skip it + | (e1, e2) `Map.member` visited = go todo visited + -- If the pair shows an inconsistency, return False + | accept m1 e1 /= accept m2 e2 = Just w + -- Otherwise, keep searching + | otherwise = go (todo <> extend (e1, e2) w visited) (Map.insert (e1, e2) w visited) + -- We could sort this set on length to get shortest counterexamples + -- For now, we don't do that and keep everything lazy + extend (e1, e2) w visited = + (multiplication m1 e1 e1, multiplication m2 e2 e2, w <> w) + :<| Map.foldMapWithKey + ( \(f1, f2) v -> + (multiplication m1 e1 f1, multiplication m2 e2 f2, w <> v) + :<| (multiplication m1 f1 e1, multiplication m2 f2 e2, v <> w) + :<| Empty + ) + visited + +searchShortestCounterexample :: (Ord q1, Ord q2) => Set a -> MonoidAcceptor a q1 -> MonoidAcceptor a q2 -> Maybe (Seq a) +searchShortestCounterexample alphabet m1 m2 = go workingSet Map.empty + where + workingSet = (unit m1, unit m2, Seq.Empty) :<| fmap (\a -> (alph m1 a, alph m2 a, Seq.singleton a)) (foldMap Seq.singleton alphabet) + go Empty visited = Nothing + go ((e1, e2, w) :<| todo) visited + -- If the pair is already visited, we skip it + | (e1, e2) `Map.member` visited = go todo visited + -- If the pair shows an inconsistency, return False + | accept m1 e1 /= accept m2 e2 = Just w + -- Otherwise, keep searching + | otherwise = go (Seq.unstableSortOn (\(_, _, w) -> length w) $ todo <> extend (e1, e2) w visited) (Map.insert (e1, e2) w visited) + -- We could sort this set on length to get shortest counterexamples + -- For now, we don't do that and keep everything lazy + extend (e1, e2) w visited = + (multiplication m1 e1 e1, multiplication m2 e2 e2, w <> w) + :<| Map.foldMapWithKey + ( \(f1, f2) v -> + (multiplication m1 e1 f1, multiplication m2 e2 f2, w <> v) + :<| (multiplication m1 f1 e1, multiplication m2 f2 e2, v <> w) + :<| Empty + ) + visited + +equivalent0 :: (Ord q1, Ord q2) => Set a -> MonoidAcceptor a q1 -> MonoidAcceptor a q2 -> Bool +equivalent0 alphabet m1 m2 = go workingSet Set.empty + where + workingSet = (unit m1, unit m2) :<| fmap (\a -> (alph m1 a, alph m2 a)) (foldMap Seq.singleton alphabet) + go Empty visited = True + go ((e1, e2) :<| todo) visited + -- If the pair is already visited, we skip it + | (e1, e2) `Set.member` visited = go todo visited + -- If the pair shows an inconsistency, return False + | accept m1 e1 /= accept m2 e2 = False + -- Otherwise, keep searching + | otherwise = go (todo <> extend (e1, e2) visited) (Set.insert (e1, e2) visited) + extend (e1, e2) visited = + (multiplication m1 e1 e1, multiplication m2 e2 e2) + :<| foldMap + ( \(f1, f2) -> + (multiplication m1 e1 f1, multiplication m2 e2 f2) + :<| (multiplication m1 f1 e1, multiplication m2 f2 e2) + :<| Empty + ) + visited diff --git a/src/Examples/Examples.hs b/src/Examples/Examples.hs new file mode 100644 index 0000000..1378fbd --- /dev/null +++ b/src/Examples/Examples.hs @@ -0,0 +1,107 @@ +{-# LANGUAGE LambdaCase #-} + +module Examples.Examples where + +import Data.Semigroup (Max (..), Semigroup (..)) +import qualified Data.Sequence as Seq +import qualified Data.Set as Set +import Monoid (MonoidAcceptor (..), complement, intersection) +import Word (Word) +import Prelude hiding (Word) + +emptyLanguage :: MonoidAcceptor a () +emptyLanguage = MonoidAcceptor [()] () (\a b -> ()) (const False) (const ()) + +emptyLanguageConvoluted :: MonoidAcceptor a Bool +emptyLanguageConvoluted = MonoidAcceptor [False, True] True (const not) (const False) (const False) + +fullLanguage :: MonoidAcceptor a () +fullLanguage = MonoidAcceptor [()] () (\a b -> ()) (const True) (const ()) + +-- accepts all words of length exactly n +lengthIsN :: Int -> MonoidAcceptor a Int +lengthIsN n = MonoidAcceptor [0 .. n + 1] 0 (saturate (n + 1) (+)) (== n) (const 1) + +-- accepts all words of length at most n +lengthUptoN :: Int -> MonoidAcceptor a Int +lengthUptoN n = MonoidAcceptor [0 .. n + 1] 0 (saturate (n + 1) (+)) (<= n) (const 1) + +emptyWord :: MonoidAcceptor a Bool +emptyWord = + MonoidAcceptor + { elements = [False, True], + unit = True, + multiplication = (&&), + accept = id, + alph = const False + } + +-- accepts exactly the given word (not a minimal monoid) +singletonLanguage :: Eq a => Word a -> MonoidAcceptor a (Word a) +singletonLanguage w = + MonoidAcceptor + { elements = undefined, + unit = Seq.empty, + multiplication = saturateW bound (<>), + accept = (==) w, + alph = Seq.singleton + } + where + bound = Seq.length w + 1 + +finiteLanguage :: Ord a => Set.Set (Word a) -> MonoidAcceptor a (Word a) +finiteLanguage ws = + MonoidAcceptor + { elements = undefined, + unit = Seq.empty, + multiplication = saturateW bound (<>), + accept = (`Set.member` ws), + alph = Seq.singleton + } + where + bound = 1 + getMax (foldMap (Max . length) ws) + +predSymbol :: (a -> Bool) -> MonoidAcceptor a Bool +predSymbol pred = + MonoidAcceptor + { elements = [False, True], + unit = True, + multiplication = (&&), + accept = id, + alph = pred + } + +-- requires count >= 2 +modnumber :: (a -> Bool) -> Int -> MonoidAcceptor a Int +modnumber pred count = + MonoidAcceptor + { elements = [0 .. count -1], + unit = 0, + multiplication = \x y -> (x + y) `mod` count, + accept = (== 0), + alph = \a -> if pred a then 1 else 0 + } + +evenAs :: MonoidAcceptor Char Int +evenAs = modnumber (== 'a') 2 + +mod3Bs :: MonoidAcceptor Char Int +mod3Bs = modnumber (== 'b') 3 + +mainExample :: MonoidAcceptor Char ((Int, Int), Bool) +mainExample = evenAs `intersection` mod3Bs `intersection` complement emptyWord + +-- Helper functions -- +saturate :: Int -> (Int -> Int -> Int) -> Int -> Int -> Int +saturate bound op x y = + let r = x `op` y + in if r >= bound + then bound + else r + +saturateW :: Int -> (Word a -> Word a -> Word a) -> Word a -> Word a -> Word a +saturateW l op x y = + let r = x `op` y + in if length r >= l + then Seq.take l r + else r diff --git a/src/MStar.hs b/src/MStar.hs index c931fbf..4401f3e 100644 --- a/src/MStar.hs +++ b/src/MStar.hs @@ -9,29 +9,26 @@ module MStar where -- This is a rough sketch, and definitely not cleaned up. import qualified Data.List as List -import Data.Map (Map) +import Data.Map (Map, (!)) import qualified Data.Map as Map import Data.Maybe (listToMaybe) -import Data.Sequence (Seq) import qualified Data.Sequence as Seq import Data.Set (Set) import qualified Data.Set as Set +import Monoid (Alphabet, MonoidAcceptor (..)) +import Word import Prelude hiding (Word) -type Word a = Seq a -type Alphabet a = Set a type MembershipQuery m a = Word a -> m Bool +type EquivalenceQuery m a q = MonoidAcceptor a q -> m (Maybe (Word a)) + squares :: Ord a => Set (Word a) -> Set (Word a) squares l = Set.map (uncurry (<>)) (Set.cartesianProduct l l) setPlus :: Ord a => Set a -> Set (Word a) -> Set (Word a) setPlus alph rows = Set.map pure alph `Set.union` squares rows --- Left and Right concats, these are like columns, but they act --- both left and right. Maybe a better word would be "tests". -type Context a = (Word a, Word a) - type Index a = Word a -- State of the M* algorithm @@ -43,20 +40,29 @@ data State a = State } deriving (Show, Eq) +-- Data type for extra information during M*'s execution +data LogMessage a + = NewRow (Word a) + | NewContext (Context a) + | Stage String + deriving (Show, Eq) + +type Logger m a = LogMessage a -> m () + -- Row data for an index row :: Ord a => State a -> Index a -> Map (Context a) Bool -row State {..} m = Map.fromSet (\(l, r) -> cache Map.! (l <> m <> r)) contexts +row State {..} m = Map.fromSet (\ctx -> cache ! apply ctx m) contexts -- Difference of two rows (i.e., all contexts in which they differ) difference :: Ord a => State a -> Index a -> Index a -> [Context a] -difference State {..} m1 m2 = [(l, r) | (l, r) <- Set.toList contexts, cache Map.! (l <> m1 <> r) /= cache Map.! (l <> m2 <> r)] +difference State {..} m1 m2 = [ctx | ctx <- Set.toList contexts, cache ! apply ctx m1 /= cache ! apply ctx m2] -- Initial state of the algorithm initialState :: (Monad m, Ord a) => Alphabet a -> MembershipQuery m a -> m (State a) initialState alphabet mq = do let rows = Set.singleton Seq.empty contexts = Set.singleton (Seq.empty, Seq.empty) - initialQueries = Set.map (\(m, (l, r)) -> l <> m <> r) $ Set.cartesianProduct (setPlus alphabet rows) contexts + initialQueries = Set.map (uncurry apply) (Set.cartesianProduct contexts (setPlus alphabet rows)) initialQueriesL = Set.toList initialQueries results <- mapM mq initialQueriesL let cache = Map.fromList (zip initialQueriesL results) @@ -68,7 +74,6 @@ initialState alphabet mq = do alphabet = alphabet } - -- CLOSED -- -- Returns all pairs which are not closed closed :: Ord a => State a -> Set (Index a) @@ -86,17 +91,17 @@ fixClosed2 :: Set (Index a) -> Maybe (Word a) fixClosed2 = listToMaybe . List.sortOn Seq.length . Set.toList -- Adds a new element -addRow :: (Monad m, Ord a) => Index a -> MembershipQuery m a -> State a -> m (State a) -addRow m mq s@State {..} = do +addRow :: (Monad m, Ord a) => Logger m a -> Index a -> MembershipQuery m a -> State a -> m (State a) +addRow logger m mq s@State {..} = do + logger (NewRow m) let newRows = Set.insert m rows - queries = Set.map (\(mi, (l, r)) -> l <> mi <> r) $ Set.cartesianProduct (setPlus alphabet newRows) contexts + queries = Set.map (uncurry apply) (Set.cartesianProduct contexts (setPlus alphabet newRows)) queriesRed = queries `Set.difference` Map.keysSet cache queriesRedL = Set.toList queriesRed results <- mapM mq queriesRedL let dCache = Map.fromList (zip queriesRedL results) return $ s {rows = newRows, cache = cache <> dCache} - -- CONSISTENT -- -- Not needed when counterexamples are added as columns, the table -- then remains sharp. There is a more efficient way of testing this @@ -116,17 +121,17 @@ fixConsistent s ((m1, m2, n1, n2, (l, r) : _) : _) = Just . head . Prelude.filte valid c = not (Set.member c (contexts s)) -- Adds a test -addContext :: (Monad m, Ord a) => Context a -> MembershipQuery m a -> State a -> m (State a) -addContext lr mq s@State {..} = do +addContext :: (Monad m, Ord a) => Logger m a -> Context a -> MembershipQuery m a -> State a -> m (State a) +addContext log lr mq s@State {..} = do + log (NewContext lr) let newContexts = Set.insert lr contexts - queries = Set.map (\(m, (l, r)) -> l <> m <> r) $ Set.cartesianProduct (setPlus alphabet rows) newContexts + queries = Set.map (uncurry apply) (Set.cartesianProduct newContexts (setPlus alphabet rows)) queriesRed = queries `Set.difference` Map.keysSet cache queriesRedL = Set.toList queriesRed results <- mapM mq queriesRedL let dCache = Map.fromList (zip queriesRedL results) return $ s {contexts = newContexts, cache = cache <> dCache} - -- ASSOCIATIVITY -- -- Returns non-associativity results. Implemented in a brute force way -- This is something new in M*, it's obviously not needed in L* @@ -144,25 +149,10 @@ fixAssociative [] _ _ = return Nothing fixAssociative ((_, _, _, _, _, []) : _) _ _ = error "Cannot happen assoc" fixAssociative ((m1, m2, m3, m12, m23, e@(l, r) : _) : _) mq table = do b <- mq (l <> m1 <> m2 <> m3 <> r) - if row table (m12 <> m3) Map.! e /= b + if row table (m12 <> m3) ! e /= b then return (Just (l, m3 <> r)) else return (Just (l <> m1, r)) - --- Abstract data type for a monoid. The map from the alphabet --- determines the homomorphism from Words to this monoid -data MonoidAcceptor a q = MonoidAcceptor - { elements :: [q], -- set of elements - unit :: q, -- the unit element - multiplication :: q -> q -> q, -- multiplication functions - accept :: q -> Bool, -- accepting subset - alph :: a -> q -- map from alphabet - } - --- Given a word, is it accepted by the monoid? -acceptMonoid :: MonoidAcceptor a q -> Word a -> Bool -acceptMonoid MonoidAcceptor {..} w = accept (foldr multiplication unit (fmap alph w)) - -- HYPOTHESIS -- -- Syntactic monoid construction constructMonoid :: Ord a => State a -> MonoidAcceptor a Int @@ -170,43 +160,69 @@ constructMonoid s@State {..} = MonoidAcceptor { elements = [0 .. Set.size allRows - 1], unit = unit, - multiplication = curry (multMap Map.!), - accept = (accMap Map.!), - alph = rowToInt . Seq.singleton -- incorrect if symbols behave trivially + multiplication = curry (multMap !), + accept = (accMap !), + alph = rowToInt . Seq.singleton } where allRows = Set.map (row s) rows rowMap = Map.fromList (zip (Set.toList allRows) [0 ..]) - rowToInt m = rowMap Map.! row s m + rowToInt m = rowMap ! row s m unit = rowToInt Seq.empty - accMap = Map.fromList [(rowMap Map.! r, r Map.! (Seq.empty, Seq.empty)) | r <- Set.toList allRows] + accMap = Map.fromList [(rowMap ! r, r ! (Seq.empty, Seq.empty)) | r <- Set.toList allRows] multList = [((rowToInt m1, rowToInt m2), rowToInt (m1 <> m2)) | m1 <- Set.toList rows, m2 <- Set.toList rows] multMap = Map.fromList multList - -- Learns until it can construct a monoid --- Please do counterexample handling yourself -learn :: (Monad m, Ord a) => MembershipQuery m a -> State a -> m (State a) -learn mq = makeClosedAndConsistentAndAssoc +fixTable :: (Monad m, Ord a) => Logger m a -> MembershipQuery m a -> State a -> m (State a) +fixTable logger mq = makeClosedAndConsistentAndAssoc where makeClosed s = do + logger (Stage "MakeClosed") case fixClosed2 $ closed s of Just m -> do - s2 <- addRow m mq s + s2 <- addRow logger m mq s makeClosed s2 Nothing -> return s makeClosedAndConsistent s = do s2 <- makeClosed s + logger (Stage "MakeConsistent") case fixConsistent s2 $ consistent s2 of Just c -> do - s3 <- addContext c mq s2 + s3 <- addContext logger c mq s2 makeClosedAndConsistent s3 Nothing -> return s2 makeClosedAndConsistentAndAssoc s = do s2 <- makeClosedAndConsistent s + logger (Stage "MakeAssociative") result <- fixAssociative (associative s2) mq s2 case result of Just a -> do - s3 <- addContext a mq s2 + s3 <- addContext logger a mq s2 makeClosedAndConsistentAndAssoc s3 Nothing -> return s2 + +learn :: (Monad m, Ord a) => Logger m a -> MembershipQuery m a -> EquivalenceQuery m a Int -> State a -> m (State a, MonoidAcceptor a Int) +learn logger mq eq = loop + where + loop s = do + -- First make the table closed and so on + logger (Stage "Closing et al the table") + s2 <- fixTable logger mq s + -- Construct the monoid + let m = constructMonoid s2 + -- Query equivalence + logger (Stage "Hypothesis") + result <- eq m + case result of + -- If Nothing, it is correct and we terminate + Nothing -> pure (s2, m) + -- Else we have a counterexample + Just w -> do + -- We split the counterexample into an existing row and new context + let apcs = foldMap (`infixResiduals` w) (rows s2 `Set.union` setPlus (alphabet s2) (rows s2)) + filtered = filter (\lr -> not (lr `Set.member` contexts s2)) apcs + sorted = List.sortOn (\(l, r) -> let (ll, rr) = (Seq.length l, Seq.length r) in (ll + rr, max ll rr)) filtered + ctx = head sorted + s3 <- addContext logger ctx mq s2 + loop s3 diff --git a/src/Monoid.hs b/src/Monoid.hs new file mode 100644 index 0000000..396b4b0 --- /dev/null +++ b/src/Monoid.hs @@ -0,0 +1,49 @@ +{-# LANGUAGE RecordWildCards #-} + +module Monoid where + +import qualified Data.Sequence as Seq +import qualified Data.Set as Set +import Word (Word) +import Prelude hiding (Word) + +type Alphabet a = Set.Set a + +-- Abstract data type for a monoid. The map from the alphabet +-- determines the homomorphism from Words to this monoid +data MonoidAcceptor a q = MonoidAcceptor + { elements :: [q], -- set of elements + unit :: q, -- the unit element + multiplication :: q -> q -> q, -- multiplication functions + accept :: q -> Bool, -- accepting subset + alph :: a -> q -- map from alphabet + } + +-- Given a word, is it accepted by the monoid? +acceptMonoid :: MonoidAcceptor a q -> Word a -> Bool +acceptMonoid MonoidAcceptor {..} w = accept (foldr multiplication unit (fmap alph w)) + +union :: MonoidAcceptor a q1 -> MonoidAcceptor a q2 -> MonoidAcceptor a (q1, q2) +union m1 m2 = + MonoidAcceptor + { elements = undefined, + unit = (unit m1, unit m2), + multiplication = \(e1, e2) (f1, f2) -> (multiplication m1 e1 f1, multiplication m2 e2 f2), + accept = \(e1, e2) -> accept m1 e1 || accept m2 e2, + alph = \a -> (alph m1 a, alph m2 a) + } + +intersection :: MonoidAcceptor a q1 -> MonoidAcceptor a q2 -> MonoidAcceptor a (q1, q2) +intersection m1 m2 = + MonoidAcceptor + { elements = undefined, + unit = (unit m1, unit m2), + multiplication = \(e1, e2) (f1, f2) -> (multiplication m1 e1 f1, multiplication m2 e2 f2), + accept = \(e1, e2) -> accept m1 e1 && accept m2 e2, + alph = \a -> (alph m1 a, alph m2 a) + } + +complement :: MonoidAcceptor a q -> MonoidAcceptor a q +complement m = m {accept = not . accept m} + +-- Todo: concatenation and Kleene star diff --git a/src/Word.hs b/src/Word.hs new file mode 100644 index 0000000..eae3c84 --- /dev/null +++ b/src/Word.hs @@ -0,0 +1,35 @@ +module Word where + +import Data.Maybe (maybeToList) +import Data.Sequence (Seq (..)) +import qualified Data.Sequence as Seq +import Prelude hiding (Word) + +-- The sequence type has efficient concatenation +-- It provides all the useful instances such as Monoid +type Word a = Seq a + +-- Left and Right concats, these are like columns, but they act +-- both left and right. Maybe a better word would be "tests". +type Context a = (Seq a, Seq a) + +apply :: Context a -> Word a -> Word a +apply (l, r) w = l <> w <> r + +zips :: Word a -> [Context a] +zips = go Empty + where + go left Empty = pure (left, Empty) + go left (h :<| hs) = (left, h :<| hs) : go (left :|> h) hs + +leftResidual :: Eq a => Word a -> Word a -> Maybe (Context a) +leftResidual Empty w = Just (Empty, w) +leftResidual _ Empty = Nothing +leftResidual (a :<| as) (b :<| bs) + | a == b = leftResidual as bs + | otherwise = Nothing + +-- Takes out an infix at all possible places +-- Probably inefficient +infixResiduals :: Eq a => Word a -> Word a -> [Context a] +infixResiduals infx word = [(l, r2) | (l, r) <- zips word, (Empty, r2) <- maybeToList (leftResidual infx r)] diff --git a/test/test.hs b/test/test.hs index 7e65daa..7da013c 100644 --- a/test/test.hs +++ b/test/test.hs @@ -1,4 +1,62 @@ -import Hedgehog.Main +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE OverloadedStrings #-} + +import qualified Data.Sequence as Seq +import qualified Data.Set as Set +import Equivalence +import Examples.Examples +import Monoid +import Test.Tasty +import Test.Tasty.HUnit main :: IO () -main = defaultMain [] +main = defaultMain tests + +data ExMonoid a = forall q. Ord q => ExMonoid {monoid :: MonoidAcceptor a q} + +tests :: TestTree +tests = + testGroup + "unit tests" + [ equivalences, + languages + ] + +equivalences :: TestTree +equivalences = + testGroup + "equivalences" + [ testCase "0 == 0" $ emptyLanguage `shouldBeEquivalentTo` emptyLanguage, + testCase "0 == 0" $ emptyLanguage `shouldBeEquivalentTo` emptyLanguageConvoluted, + testCase "0 /= 1" $ emptyLanguage `shouldNotBeEquivalentTo` fullLanguage, + testCase "upto is union n=0" $ lengthUptoN 0 `shouldBeEquivalentToE` uptoAsUnion 0, + testCase "upto is union n=1" $ lengthUptoN 1 `shouldBeEquivalentToE` uptoAsUnion 1, + testCase "upto is union n=2" $ lengthUptoN 2 `shouldBeEquivalentToE` uptoAsUnion 2, + testCase "upto is union n=3" $ lengthUptoN 3 `shouldBeEquivalentToE` uptoAsUnion 3, + testCase "intersection" $ (lengthIsN 4 `intersection` lengthIsN 5) `shouldBeEquivalentTo` emptyLanguage, + testCase "upto and union" $ (lengthUptoN 4 `intersection` lengthUptoN 7) `shouldBeEquivalentTo` lengthUptoN 4, + testCase "empty word" $ lengthIsN 0 `shouldBeEquivalentTo` singletonLanguage Seq.empty, + testCase "empty lang" $ emptyLanguage `shouldBeEquivalentTo` finiteLanguage Set.empty + ] + where + shouldBeEquivalentTo x y = equivalent (Set.fromList "ab") x y @?= True + shouldNotBeEquivalentTo x y = equivalent (Set.fromList "ab") x y @?= False + shouldBeEquivalentToE x (ExMonoid y) = equivalent (Set.fromList "ab") x y @?= True + + uptoAsUnion 0 = ExMonoid (lengthIsN 0) + uptoAsUnion n = case uptoAsUnion (n -1) of + ExMonoid m -> ExMonoid (lengthIsN n `union` m) + +languages :: TestTree +languages = + testGroup + "languages" + [ shouldReject "fin lang empty" (finiteLanguage (Set.fromList [])) ["", "a", "b", "abba"], + shouldAccept "fin lang 1" (finiteLanguage (Set.fromList ["abba"])) ["abba"], + shouldReject "fin lang 1" (finiteLanguage (Set.fromList ["abba"])) ["aba", "abbab", "babba", ""], + shouldAccept "fin lang 2" (finiteLanguage (Set.fromList ["abba", "b", "aaa"])) ["abba", "b", "aaa"], + shouldReject "fin lang 2" (finiteLanguage (Set.fromList ["abba", "b", "aaa"])) ["aba", "abbab", "babba", "", "a", "aa", "aaaa"] + ] + where + shouldAccept name m ls = testGroup (name <> " accepts") [testCase (show w) $ acceptMonoid m w @?= True | w <- ls] + shouldReject name m ls = testGroup (name <> " rejects") [testCase (show w) $ acceptMonoid m w @?= False | w <- ls]