Splits the Teacher.hs into more files

src/Teacher.hs

@@ -1,54 +1,21 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE FlexibleInstances         #-}
 
-module Teacher where
+module Teacher
+    ( module Teachers.Teacher
+    , teacherWithTarget
+    , teacherWithTargetNonDet
+    , teacherWithIO
+    , teacherWithTargetAndIO
+    ) where
 
-import           NLambda hiding (alphabet, when)
+import Teachers.Teacher
+import Teachers.Whitebox
+import Teachers.Terminal
+
+import NLambda hiding (alphabet)
 import qualified NLambda (alphabet)
 
-import Debug.Trace
--- Explicit Prelude, as NLambda has quite some clashes
-import           Data.Function           (fix)
-import           Data.List               (zip, (!!), reverse)
-import           Data.Maybe              (Maybe (..))
-import           Prelude                 (Bool (..), Int, Read, Show, error,
-                                          length, return, ($), (++), (-), (<),
-                                          (==), (.), (<=), (+), show, seq, (<$>))
-import qualified Prelude
-import Control.Monad.Identity (Identity(..))
-import Control.Monad (when, forM)
-import Data.IORef (IORef, readIORef, newIORef, writeIORef)
-import System.IO.Unsafe (unsafePerformIO)
-
--- Used in the IO teacher
-import           System.Console.Haskeline
-import           System.IO.Unsafe        (unsafePerformIO)
-import           Text.Read               (readMaybe)
-
--- Abstract teacher type (inside the NLambda library, ideally one would like
--- an external interface, with Bool as output instead of Formula for instance)
--- For now we do actually implement an external teacher, but it is rather hacky.
-data Teacher i = Teacher
-    -- Given a sequence, check whether it is in the language
-    -- Assumed to be equivariant.
-    -- We slightly change the type to support counting the number of orbits.
-    -- All teacher (except the counting one) implement membership :: [i] -> Formula
-    { membership :: Set [i] -> Set ([i], Formula)
-    -- Given a hypothesis, returns Nothing when equivalence or a (equivariant)
-    -- set of counter examples. Needs to be quantified over q, because the
-    -- learner may choose the type of the state space.
-    , equivalent :: forall q. (Show q, NominalType q) => Automaton q i -> Maybe (Set [i])
-    -- Returns the alphabet to the learner
-    , alphabet   :: Set i
-    }
-
--- In order to count membership queries, I had to have the set of inputs
--- instead of just mere inputs... It's a bit annoying, since it doesn't
--- look like Angluin like this... But this is the best I can do in NLambda
--- Here is a function to make it element-wise again:
-foreachQuery :: NominalType i => ([i] -> Formula) -> Set[i] -> Set ([i], Formula)
-foreachQuery f qs = map (\q -> (q, f q)) qs
-
 -- We provide three ways to construct teachers:
 -- 1. Fully automatic
 -- 2. Fully interactive (via IO)
@@ -60,18 +27,18 @@ foreachQuery f qs = map (\q -> (q, f q)) qs
 -- Only works for DFAs for now, as those can be checked for equivalence
 teacherWithTarget :: (NominalType i, NominalType q) => Automaton q i -> Teacher i
 teacherWithTarget aut = Teacher
-    { membership = foreachQuery $ automaticMembership aut
+    { membership = foreachQuery $ accepts aut
     , equivalent = automaticEquivalent bisim aut
-    , alphabet   = automaticAlphabet aut
+    , alphabet   = NLambda.alphabet aut
     }
 
 -- 1b. This is a fully automatic teacher, which has an internal automaton
 -- NFA have undecidable equivalence, n is a bound on deoth of bisimulation.
 teacherWithTargetNonDet :: (Show i, Show q, NominalType i, NominalType q) => Int -> Automaton q i -> Teacher i
 teacherWithTargetNonDet n aut = Teacher
-    { membership = foreachQuery $ automaticMembership aut
+    { membership = foreachQuery $ accepts aut
     , equivalent = automaticEquivalent (bisimNonDet n) aut
-    , alphabet   = automaticAlphabet aut
+    , alphabet   = NLambda.alphabet aut
     }
 
 -- 2. Will ask everything to someone reading the terminal
@@ -91,56 +58,11 @@ teacherWithIO = Teacher
 -- used for NFAs when there was no bounded bisimulation yet
 teacherWithTargetAndIO :: NominalType q => Automaton q Atom -> Teacher Atom
 teacherWithTargetAndIO aut = Teacher
-    { membership = foreachQuery $ automaticMembership aut
+    { membership = foreachQuery $ accepts aut
     , equivalent = ioEquivalent
     , alphabet   = atoms
     }
 
--- 4. A teacher with state (hacked, since the types don't allow for it)
--- Useful for debugging and so on, but *very very hacky*!
-countingTeacher :: (Show i, Contextual i, NominalType i) => Teacher i -> Teacher i
-countingTeacher delegate = Teacher
-    { membership = \qs -> increaseMQ qs `seq` membership delegate qs
-    , equivalent = \a -> increaseEQ a `seq` equivalent delegate a
-    , alphabet   = alphabet delegate
-    }
-    where
-        {-# NOINLINE increaseEQ #-}
-        increaseEQ a = unsafePerformIO $ do
-            i <- readIORef eqCounter
-            let j = i + 1
-            writeIORef eqCounter j
-            return a
-        {-# NOINLINE increaseMQ #-}
-        increaseMQ q = unsafePerformIO $ do
-            new <- newOrbitsInCache q
-            l <- readIORef mqCounter
-            let l2 = new : l
-            writeIORef mqCounter l2
-            return q
-        {-# NOINLINE cache #-}
-        cache = unsafePerformIO $ newIORef empty
-        {-# NOINLINE newOrbitsInCache #-}
-        newOrbitsInCache qs = do
-            oldCache <- readIORef cache
-            let newQs = simplify $ qs \\ oldCache
-            writeIORef cache (simplify $ oldCache `union` qs)
-            return $ setOrbitsMaxNumber newQs
-
--- HACK: Counts number of equivalence queries
-eqCounter :: IORef Int
-{-# NOINLINE eqCounter #-}
-eqCounter = unsafePerformIO $ newIORef 0
-
--- HACK: Keeps track of membership queries with: # orbits per 'query'
-mqCounter :: IORef [Int]
-{-# NOINLINE mqCounter #-}
-mqCounter = unsafePerformIO $ newIORef []
-
-
--- Implementations of above functions
--- 
-automaticMembership aut input = accepts aut input
 automaticEquivalent bisimlator aut hypo = case solve isEq of
         Nothing -> error "should be solved"
         Just True -> Nothing
@@ -148,137 +70,3 @@ automaticEquivalent bisimlator aut hypo = case solve isEq of
         where
             bisimRes = bisimlator aut hypo
             isEq = isEmpty bisimRes
-automaticAlphabet aut = NLambda.alphabet aut
-
-
-instance Conditional a => Conditional (Identity a) where
-    cond f x y = return (cond f (runIdentity x) (runIdentity y))
-
--- Checks bisimulation of initial states (only for DFAs)
--- returns some counter examples if not bisimilar
--- returns empty set iff bisimilar
-bisim :: (NominalType i, NominalType q1, NominalType q2) => Automaton q1 i -> Automaton q2 i -> Set [i]
-bisim aut1 aut2 = runIdentity $ go empty (pairsWith addEmptyWord (initialStates aut1) (initialStates aut2))
-    where
-        go rel todo = do
-            -- if elements are already in R, we can skip them
-            let todo2 = filter (\(_, x, y) -> (x, y) `notMember` rel) todo
-            -- split into correct pairs and wrong pairs
-            let (cont, ces) = partition (\(_, x, y) -> (x `member` (finalStates aut1)) <==> (y `member` (finalStates aut2))) todo2
-            let aa = NLambda.alphabet aut1
-            -- the good pairs should make one step
-            let dtodo = sum (pairsWith (\(w, x, y) a -> pairsWith (\x2 y2 -> (a:w, x2, y2)) (d aut1 a x) (d aut2 a y)) cont aa)
-            -- if there are wrong pairs
-            ite (isNotEmpty ces)
-                -- then return counter examples
-                (return $ map getRevWord ces)
-                -- else continue with good pairs
-                (ite (isEmpty dtodo)
-                    (return empty)
-                    (go (rel `union` map stripWord cont) (dtodo))
-                )
-        d aut a x = mapFilter (\(s, l, t) -> maybeIf (s `eq` x /\ l `eq` a) t) (delta aut)
-        stripWord (_, x, y) = (x, y)
-        getRevWord (w, _, _) = reverse w
-        addEmptyWord x y = ([], x, y)
-
--- Attempt at using a bisimlution up to to proof bisimulation between NFAs
--- Because why not? Inspired by the Hacking non-determinism paper
--- But they only consider finite sums (which is enough for finite sets)
--- Here I have to do a bit of trickery, which is hopefully correct.
--- I think it is correct, but not yet complete enough, we need more up-to.
-bisimNonDet :: (Show i, Show q1, Show q2, NominalType i, NominalType q1, NominalType q2) => Int -> Automaton q1 i -> Automaton q2 i -> Set [i]
-bisimNonDet n aut1 aut2 = runIdentity $ go empty (singleton ([], initialStates aut1, initialStates aut2))
-    where
-        go rel todo0 = do
-            -- if elements are too long, we ignore them
-            let todo0b = filter (\(w,_,_) -> fromBool (length w <= n)) todo0
-            -- if elements are already in R, we can skip them
-            let todo1 = filter (\(_, x, y) -> (x, y) `notMember` rel) todo0b
-            -- now we are going to do a up-to thingy
-            -- we look at all subsets x2 of x occuring in R (similarly for y)
-            let xbar x = mapFilter (\(x2, _) -> maybeIf (x2 `isSubsetOf` x) x2) rel
-            let ybar y = mapFilter (\(_, y2) -> maybeIf (y2 `isSubsetOf` y) y2) rel
-            -- and then the sums are expressed by these formulea kind of
-            let xform x y = x `eq` sum (xbar x) /\ forAll (\x2 -> exists (\y2 -> rel `contains` (x2, y2)) (ybar y)) (xbar x)
-            let yform x y = y `eq` sum (ybar y) /\ forAll (\y2 -> exists (\x2 -> rel `contains` (x2, y2)) (xbar x)) (ybar y)
-            let notSums x y = not (xform x y /\ yform x y)
-            -- filter out things expressed as sums
-            let todo2 = filter (\(_, x, y) -> notSums x y) todo1
-            -- split into correct pairs and wrong pairs
-            let (cont, ces) = partition (\(_, x, y) -> (x `intersect` (finalStates aut1)) <==> (y `intersect` (finalStates aut2))) todo2
-            let aa = NLambda.alphabet aut1
-            -- the good pairs should make one step
-            let dtodo = pairsWith (\(w, x, y) a -> (a:w, sumMap (d aut1 a) x, sumMap (d aut2 a) y)) cont aa
-            -- if there are wrong pairs
-            --trace "go" $ traceShow rel $ traceShow todo0 $ traceShow todo1 $ traceShow todo2 $ traceShow cont $
-            ite (isNotEmpty ces)
-                -- then return counter examples
-                (return $ map getRevWord ces)
-                -- else continue with good pairs
-                (ite (isEmpty dtodo)
-                    (return empty)
-                    (go (rel `union` map stripWord cont) (dtodo))
-                )
-        d aut a x = mapFilter (\(s, l, t) -> maybeIf (s `eq` x /\ l `eq` a) t) (delta aut)
-        stripWord (_, x, y) = (x, y)
-        getRevWord (w, _, _) = reverse w
-        addEmptyWord x y = ([], x, y)
-        sumMap f = sum . (map f)
-
--- Posing a membership query to the terminal and waits for used to input a formula
-ioMembership :: (Show i, NominalType i, Contextual i) => Set [i] -> Set ([i], Formula)
-ioMembership inputs = unsafePerformIO $ do
-    let representedInputs = fromVariant . fromJust <$> (toList $ setOrbitsRepresentatives inputs)
-    Prelude.putStrLn "\n# Membership Queries:"
-    Prelude.putStrLn "# Please answer each query with either \"True\" or \"False\""
-    answers <- forM representedInputs $ \input -> do
-        Prelude.putStr "Q: "
-        Prelude.print input
-        let loop = do
-                x <- getInputLine "A: "
-                case x of
-                    Nothing -> error "Bye bye, have a good day!"
-                    Just str -> do
-                        case readMaybe str :: Maybe Bool of
-                            Nothing -> do
-                                outputStrLn $ "Unable to parse " ++ str ++ " :: Bool"
-                                loop
-                            Just f -> return f
-        answer <- runInputT defaultSettings loop
-        return $ orbit [] (input, fromBool answer)
-    let answersAsSet = simplify . sum . fromList $ answers
-    return answersAsSet
-
--- Poses a query to the terminal, waiting for the user to provide a counter example
--- TODO: extend to any alphabet type (hard because of parsing)
-ioEquivalent :: (Show q, NominalType q) => Automaton q Atom -> Maybe (Set [Atom])
-ioEquivalent hypothesis = unsafePerformIO $ do
-    Prelude.putStrLn "\n# Is the following automaton correct?"
-    Prelude.putStr "# "
-    Prelude.print hypothesis
-    Prelude.putStrLn "# \"Nothing\" for equivalent, \"Just [...]\" for a counter example (eg \"Just [0,1,0]\")"
-    answer <- runInputT defaultSettings loop
-    case answer of
-        Nothing -> return Nothing
-        Just input -> do
-            -- create sequences of same length
-            let n = length input
-            let sequence = replicateAtoms n
-            -- whenever two are identiacl in input, we will use eq, if not neq
-            let op i j = if (input !! i) == (input !! j) then eq else neq
-            -- copy the relations from input to sequence
-            let rels s = and [op i j (s !! i) (s !! j) | i <- [0..n - 1], j <- [0..n - 1], i < j]
-            let fseq = filter rels sequence
-            return $ Just fseq
-    where
-        loop = do
-            x <- getInputLine "> "
-            case x of
-                Nothing -> error "Bye bye, have a good day!"
-                Just str -> do
-                    case readMaybe str :: Maybe (Maybe [Int]) of
-                        Nothing -> do
-                            outputStrLn $ "Unable to parse " ++ str ++ " :: Maybe [Int]"
-                            loop
-                        Just f -> return f

src/Teachers/Teacher.hs

@@ -0,0 +1,28 @@
+{-# LANGUAGE RankNTypes #-}
+module Teachers.Teacher where
+
+import NLambda
+import Prelude hiding (map)
+
+-- Abstract teacher type. Maybe this will be generalized to some monad, so that
+-- the teacher can have state (such as a cache).
+-- TODO: add a notion of state, so that Teachers can maintain a cache, or
+--       a socket, or file, or whatever (as long as it stays deterministic).
+data Teacher i = Teacher
+    -- A teacher provides a way to answer membership queries. You'd expect
+    -- a function of type [i] -> Bool. But in order to implement some teachers
+    -- more efficiently, we provide Set [i] as input, and the teacher is
+    -- supposed to answer each element in the set.
+    { membership :: Set [i] -> Set ([i], Formula)
+    -- Given a hypothesis, returns Nothing when equivalence or a (equivariant)
+    -- set of counter examples. Needs to be quantified over q, because the
+    -- learner may choose the type of the state space.
+    , equivalent :: forall q. (Show q, NominalType q) => Automaton q i -> Maybe (Set [i])
+    -- Returns the alphabet to the learner
+    , alphabet   :: Set i
+    }
+
+-- Often a membership query is defined by a function [i] -> Formula. This wraps
+-- such a function to the required type for a membership query (see above).
+foreachQuery :: NominalType i => ([i] -> Formula) -> Set[i] -> Set ([i], Formula)
+foreachQuery f qs = map (\q -> (q, f q)) qs

src/Teachers/Terminal.hs

@@ -0,0 +1,74 @@
+module Teachers.Terminal where
+
+import NLambda
+
+import Control.Monad
+import Data.IORef
+import Prelude hiding (filter, map, and, sum)
+import System.Console.Haskeline
+import System.IO.Unsafe (unsafePerformIO)
+import Text.Read (readMaybe)
+
+-- Posing a membership query to the terminal and waits for used to input a formula
+ioMembership :: Set [Atom] -> Set ([Atom], Formula)
+ioMembership queries = unsafePerformIO $ do
+    cache <- readIORef mqCache
+    let cachedAnswers = filter (\(a, f) -> a `member` queries) cache
+    let newQueries = simplify $ queries \\ map fst cache
+    let representedInputs = fromVariant . fromJust <$> (toList $ setOrbitsRepresentatives newQueries)
+    putStrLn "\n# Membership Queries:"
+    putStrLn "# Please answer each query with \"True\" or \"False\" (\"^D\" for quit)"
+    answers <- forM representedInputs $ \input -> do
+        putStr "Q: "
+        print input
+        let loop = do
+                x <- fmap readMaybe <$> getInputLine "A: "
+                case x of
+                    Nothing -> error "Bye bye, have a good day!"
+                    Just Nothing -> do
+                        outputStrLn $ "Unable to parse, try again"
+                        loop
+                    Just (Just f) -> return (f :: Bool)
+        answer <- runInputT defaultSettings loop
+        return $ orbit [] (input, fromBool answer)
+    let answersAsSet = simplify . sum . fromList $ answers
+    writeIORef mqCache (simplify $ cache `union` answersAsSet)
+    return (simplify $ cachedAnswers `union` answersAsSet)
+
+-- We use a cache, so that questions will not be repeated.
+-- It is a bit hacky, as the Teacher interface does not allow state...
+mqCache :: IORef (Set ([Atom], Formula))
+{-# NOINLINE mqCache #-}
+mqCache = unsafePerformIO $ newIORef empty
+
+-- Poses a query to the terminal, waiting for the user to provide a counter example
+-- TODO: extend to any alphabet type (hard because of parsing)
+ioEquivalent :: (Show q, NominalType q) => Automaton q Atom -> Maybe (Set [Atom])
+ioEquivalent hypothesis = unsafePerformIO $ do
+    putStrLn "\n# Is the following automaton correct?"
+    putStr "# "
+    print hypothesis
+    putStrLn "# \"^D\" for equivalent, \"[...]\" for a counter example (eg \"[0,1,0]\")"
+    let loop = do
+            x <- fmap readMaybe <$> getInputLine "> "
+            case x of
+                Nothing ->  do
+                    outputStrLn $ "Ok, we're done"
+                    return Nothing
+                Just Nothing -> do
+                    outputStrLn $ "Unable to parse, try again"
+                    loop
+                Just (Just f) -> return (Just f :: Maybe [Int])
+    answer <- runInputT defaultSettings loop
+    case answer of
+        Nothing -> return Nothing
+        Just input -> do
+            -- create sequences of same length
+            let n = length input
+            let sequence = replicateAtoms n
+            -- whenever two are identiacl in input, we will use eq, if not neq
+            let op i j = if (input !! i) == (input !! j) then eq else neq
+            -- copy the relations from input to sequence
+            let rels s = and [op i j (s !! i) (s !! j) | i <- [0..n - 1], j <- [0..n - 1], i < j]
+            let fseq = filter rels sequence
+            return $ Just fseq

src/Teachers/Whitebox.hs

@@ -0,0 +1,84 @@
+module Teachers.Whitebox where
+
+import NLambda
+
+import Control.Monad.Identity
+import Prelude hiding (map, sum, filter, not)
+
+-- I found it a bit easier to write a do-block below. So I needed this
+-- Conditional instance.
+instance Conditional a => Conditional (Identity a) where
+    cond f x y = return (cond f (runIdentity x) (runIdentity y))
+
+
+-- Checks bisimulation of initial states (only for DFAs)
+-- returns some counter examples if not bisimilar
+-- returns empty set iff bisimilar
+bisim :: (NominalType i, NominalType q1, NominalType q2) => Automaton q1 i -> Automaton q2 i -> Set [i]
+bisim aut1 aut2 = runIdentity $ go empty (pairsWith addEmptyWord (initialStates aut1) (initialStates aut2))
+    where
+        go rel todo = do
+            -- if elements are already in R, we can skip them
+            let todo2 = filter (\(_, x, y) -> (x, y) `notMember` rel) todo
+            -- split into correct pairs and wrong pairs
+            let (cont, ces) = partition (\(_, x, y) -> (x `member` (finalStates aut1)) <==> (y `member` (finalStates aut2))) todo2
+            let aa = NLambda.alphabet aut1
+            -- the good pairs should make one step
+            let dtodo = sum (pairsWith (\(w, x, y) a -> pairsWith (\x2 y2 -> (a:w, x2, y2)) (d aut1 a x) (d aut2 a y)) cont aa)
+            -- if there are wrong pairs
+            ite (isNotEmpty ces)
+                -- then return counter examples
+                (return $ map getRevWord ces)
+                -- else continue with good pairs
+                (ite (isEmpty dtodo)
+                    (return empty)
+                    (go (rel `union` map stripWord cont) (dtodo))
+                )
+        d aut a x = mapFilter (\(s, l, t) -> maybeIf (s `eq` x /\ l `eq` a) t) (delta aut)
+        stripWord (_, x, y) = (x, y)
+        getRevWord (w, _, _) = reverse w
+        addEmptyWord x y = ([], x, y)
+
+-- Attempt at using a bisimlution up to to proof bisimulation between NFAs
+-- Because why not? Inspired by the Hacking non-determinism paper
+-- But they only consider finite sums (which is enough for finite sets)
+-- Here I have to do a bit of trickery, which is hopefully correct.
+-- I think it is correct, but not yet complete enough, we need more up-to.
+bisimNonDet :: (Show i, Show q1, Show q2, NominalType i, NominalType q1, NominalType q2) => Int -> Automaton q1 i -> Automaton q2 i -> Set [i]
+bisimNonDet n aut1 aut2 = runIdentity $ go empty (singleton ([], initialStates aut1, initialStates aut2))
+    where
+        go rel todo0 = do
+            -- if elements are too long, we ignore them
+            let todo0b = filter (\(w,_,_) -> fromBool (length w <= n)) todo0
+            -- if elements are already in R, we can skip them
+            let todo1 = filter (\(_, x, y) -> (x, y) `notMember` rel) todo0b
+            -- now we are going to do a up-to thingy
+            -- we look at all subsets x2 of x occuring in R (similarly for y)
+            let xbar x = mapFilter (\(x2, _) -> maybeIf (x2 `isSubsetOf` x) x2) rel
+            let ybar y = mapFilter (\(_, y2) -> maybeIf (y2 `isSubsetOf` y) y2) rel
+            -- and then the sums are expressed by these formulea kind of
+            let xform x y = x `eq` sum (xbar x) /\ forAll (\x2 -> exists (\y2 -> rel `contains` (x2, y2)) (ybar y)) (xbar x)
+            let yform x y = y `eq` sum (ybar y) /\ forAll (\y2 -> exists (\x2 -> rel `contains` (x2, y2)) (xbar x)) (ybar y)
+            let notSums x y = not (xform x y /\ yform x y)
+            -- filter out things expressed as sums
+            let todo2 = filter (\(_, x, y) -> notSums x y) todo1
+            -- split into correct pairs and wrong pairs
+            let (cont, ces) = partition (\(_, x, y) -> (x `intersect` (finalStates aut1)) <==> (y `intersect` (finalStates aut2))) todo2
+            let aa = NLambda.alphabet aut1
+            -- the good pairs should make one step
+            let dtodo = pairsWith (\(w, x, y) a -> (a:w, sumMap (d aut1 a) x, sumMap (d aut2 a) y)) cont aa
+            -- if there are wrong pairs
+            --trace "go" $ traceShow rel $ traceShow todo0 $ traceShow todo1 $ traceShow todo2 $ traceShow cont $
+            ite (isNotEmpty ces)
+                -- then return counter examples
+                (return $ map getRevWord ces)
+                -- else continue with good pairs
+                (ite (isEmpty dtodo)
+                    (return empty)
+                    (go (rel `union` map stripWord cont) (dtodo))
+                )
+        d aut a x = mapFilter (\(s, l, t) -> maybeIf (s `eq` x /\ l `eq` a) t) (delta aut)
+        stripWord (_, x, y) = (x, y)
+        getRevWord (w, _, _) = reverse w
+        addEmptyWord x y = ([], x, y)
+        sumMap f = sum . (map f)