From 3cc387a068b3eb299b6450a5aa1c51113a71b18c Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Mon, 5 Dec 2016 12:35:19 +0100 Subject: [PATCH] Splits the Teacher.hs into more files --- src/Teacher.hs | 246 +++------------------------------------ src/Teachers/Teacher.hs | 28 +++++ src/Teachers/Terminal.hs | 74 ++++++++++++ src/Teachers/Whitebox.hs | 84 +++++++++++++ 4 files changed, 203 insertions(+), 229 deletions(-) create mode 100644 src/Teachers/Teacher.hs create mode 100644 src/Teachers/Terminal.hs create mode 100644 src/Teachers/Whitebox.hs diff --git a/src/Teacher.hs b/src/Teacher.hs index b9d477b..5757f2e 100644 --- a/src/Teacher.hs +++ b/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 diff --git a/src/Teachers/Teacher.hs b/src/Teachers/Teacher.hs new file mode 100644 index 0000000..66e7991 --- /dev/null +++ b/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 diff --git a/src/Teachers/Terminal.hs b/src/Teachers/Terminal.hs new file mode 100644 index 0000000..e5b4592 --- /dev/null +++ b/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 diff --git a/src/Teachers/Whitebox.hs b/src/Teachers/Whitebox.hs new file mode 100644 index 0000000..3bdf6a9 --- /dev/null +++ b/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)