Automatic counterexample handling

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 }
+example :: MonoidAcceptor Char _
-language :: MStar.Word Char -> Bool
+example =
-language w = not (null w) && length aa `mod` 2 == 0 && length bb `mod` 3 == 0
+  -- 1. the first example I tried:
-  where
+  mainExample
-    (aa, bb) = Seq.partition (== 'a') w
+  -- 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) ' ')
+  putStr (replicate (6 - length nstr) ' ')
-  putStrLn $ toList w
+  putStr wstr
-  return $ language w
+  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
+  mqCount <- newIORef 0
-  let lang = languageM count
+  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)
+  -- learn
-  -- Let's add a column so that aa can be reached
+  (s2, m2) <- learn logger lang equi s
-  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
 
   -- 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 "    "
+  mapM_
-  print kbRules
+    ( \(l, r) -> do
-
+        putStr "    "
-  putStrLn "and accepting strings:"
+        putStr (toList l)
-  putStr "    "
+        putStr " = "
-  print accRows
+        putStrLn (toList r)
+    )
+    kbRules

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

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

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

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 :: (Monad m, Ord a) => Logger m a -> Index a -> MembershipQuery m a -> State a -> m (State a)
-addRow m mq s@State {..} = do
+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 :: (Monad m, Ord a) => Logger m a -> Context a -> MembershipQuery m a -> State a -> m (State a)
-addContext lr mq s@State {..} = do
+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.!),
+      multiplication = curry (multMap !),
-      accept = (accMap Map.!),
+      accept = (accMap !),
-      alph = rowToInt . Seq.singleton -- incorrect if symbols behave trivially
+      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
+fixTable :: (Monad m, Ord a) => Logger m a -> MembershipQuery m a -> State a -> m (State a)
-learn :: (Monad m, Ord a) => MembershipQuery m a -> State a -> m (State a)
+fixTable logger mq = makeClosedAndConsistentAndAssoc
-learn 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

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

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)]

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]