diff --git a/src/Examples.hs b/src/Examples.hs index babab8f..8251e4e 100644 --- a/src/Examples.hs +++ b/src/Examples.hs @@ -11,8 +11,8 @@ import Examples.ContrivedNFAs import Examples.Fifo import Examples.Stack import NLambda (Atom) -import Teacher (TeacherWithTarget (..)) +import Teacher (teacherWithTarget, Teacher) -- Wrapping it in a teacher -exampleTeacher :: TeacherWithTarget Atom -exampleTeacher = TeacherWithTarget example4 +exampleTeacher :: Teacher Atom +exampleTeacher = teacherWithTarget example4 diff --git a/src/Main.hs b/src/Main.hs index 21910e9..6fe2bdc 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -6,8 +6,7 @@ import Examples import Functions import ObservationTable import Teacher - -import NLStar +import NLStar import NLambda @@ -55,7 +54,7 @@ inconsistency = inconsistencyBartek -- This function will (recursively) make the table complete and consistent. -- This is in the IO monad purely because I want some debugging information. -- (Same holds for many other functions here) -makeCompleteConsistent :: (Show i, Contextual i, NominalType i, Teacher t i) => t -> State i -> IO (State i) +makeCompleteConsistent :: LearnableAlphabet i => Teacher i -> State i -> IO (State i) makeCompleteConsistent teacher state@State{..} = do -- inc is the set of rows witnessing incompleteness, that is the sequences -- 's1 a' which do not have their equivalents of the form 's2'. @@ -107,7 +106,7 @@ constructHypothesis State{..} = automaton q a d i f toform s = forAll id . map fromBool $ s -- Extends the table with all prefixes of a set of counter examples. -useCounterExampleAngluin :: (Show i, Contextual i, NominalType i, Teacher t i) => t -> State i -> Set [i] -> IO (State i) +useCounterExampleAngluin :: LearnableAlphabet i => Teacher i -> State i -> Set [i] -> IO (State i) useCounterExampleAngluin teacher state@State{..} ces = do putStr "Using ce: " print ces @@ -118,7 +117,7 @@ useCounterExampleAngluin teacher state@State{..} ces = do return state2 -- I am not quite sure whether this variant is due to Rivest & Schapire or Maler & Pnueli. -useCounterExampleRS :: (Show i, Contextual i, NominalType i, Teacher t i) => t -> State i -> Set [i] -> IO (State i) +useCounterExampleRS :: LearnableAlphabet i => Teacher i -> State i -> Set [i] -> IO (State i) useCounterExampleRS teacher state@State{..} ces = do putStr "Using ce: " print ces @@ -128,12 +127,12 @@ useCounterExampleRS teacher state@State{..} ces = do let state2 = addColumns teacher de state return state2 -useCounterExample :: (Show i, Contextual i, NominalType i, Teacher t i) => t -> State i -> Set [i] -> IO (State i) +useCounterExample :: LearnableAlphabet i => Teacher i -> State i -> Set [i] -> IO (State i) useCounterExample = useCounterExampleRS -- The main loop, which results in an automaton. Will stop if the hypothesis -- exactly accepts the language we are learning. -loop :: (Show i, Contextual i, NominalType i, Teacher t i) => t -> State i -> IO (Automaton (BRow i) i) +loop :: LearnableAlphabet i => Teacher i -> State i -> IO (Automaton (BRow i) i) loop teacher s = do putStrLn "##################" putStrLn "1. Making it complete and consistent" @@ -150,7 +149,7 @@ loop teacher s = do s <- useCounterExample teacher s ce loop teacher s -constructEmptyState :: (Contextual i, NominalType i, Teacher t i) => t -> State i +constructEmptyState :: LearnableAlphabet i => Teacher i -> State i constructEmptyState teacher = let aa = Teacher.alphabet teacher in let ss = singleton [] in @@ -159,7 +158,7 @@ constructEmptyState teacher = let t = fillTable teacher (ss `union` ssa) ee in State{..} -learn :: (Show i, Contextual i, NominalType i, Teacher t i) => t -> IO (Automaton (BRow i) i) +learn :: LearnableAlphabet i => Teacher i -> IO (Automaton (BRow i) i) learn teacher = do let s = constructEmptyState teacher loop teacher s diff --git a/src/NLStar.hs b/src/NLStar.hs index cb190f3..b9adb3e 100644 --- a/src/NLStar.hs +++ b/src/NLStar.hs @@ -66,7 +66,7 @@ instance (Conditional a) => Conditional (IO a) where -- This function will (recursively) make the table complete and consistent. -- This is in the IO monad purely because I want some debugging information. -- (Same holds for many other functions here) -makeCompleteConsistentNonDet :: (Show i, Contextual i, NominalType i, Teacher t i) => t -> State i -> IO (State i) +makeCompleteConsistentNonDet :: LearnableAlphabet i => Teacher i -> State i -> IO (State i) makeCompleteConsistentNonDet teacher state@State{..} = do -- inc is the set of rows witnessing incompleteness, that is the sequences -- 's1 a' which do not have their equivalents of the form 's2'. @@ -126,7 +126,7 @@ constructHypothesisNonDet State{..} = automaton q a d i f toform s = forAll id . map fromBool $ s -- I am not quite sure whether this variant is due to Rivest & Schapire or Maler & Pnueli. -useCounterExampleNonDet :: (Show i, Contextual i, NominalType i, Teacher t i) => t -> State i -> Set [i] -> IO (State i) +useCounterExampleNonDet :: LearnableAlphabet i => Teacher i -> State i -> Set [i] -> IO (State i) useCounterExampleNonDet teacher state@State{..} ces = do putStr "Using ce: " print ces @@ -138,7 +138,7 @@ useCounterExampleNonDet teacher state@State{..} ces = do -- The main loop, which results in an automaton. Will stop if the hypothesis -- exactly accepts the language we are learning. -loopNonDet :: (Show i, Contextual i, NominalType i, Teacher t i) => t -> State i -> IO (Automaton (BRow i) i) +loopNonDet :: LearnableAlphabet i => Teacher i -> State i -> IO (Automaton (BRow i) i) loopNonDet teacher s = do putStrLn "##################" putStrLn "1. Making it complete and consistent" @@ -155,7 +155,7 @@ loopNonDet teacher s = do s <- useCounterExampleNonDet teacher s ce loopNonDet teacher s -constructEmptyStateNonDet :: (Contextual i, NominalType i, Teacher t i) => t -> State i +constructEmptyStateNonDet :: LearnableAlphabet i => Teacher i -> State i constructEmptyStateNonDet teacher = let aa = Teacher.alphabet teacher in let ss = singleton [] in @@ -164,7 +164,7 @@ constructEmptyStateNonDet teacher = let t = fillTable teacher (ss `union` ssa) ee in State{..} -learnNonDet :: (Show i, Contextual i, NominalType i, Teacher t i) => t -> IO (Automaton (BRow i) i) +learnNonDet :: LearnableAlphabet i => Teacher i -> IO (Automaton (BRow i) i) learnNonDet teacher = do let s = constructEmptyStateNonDet teacher loopNonDet teacher s diff --git a/src/ObservationTable.hs b/src/ObservationTable.hs index 74dd359..1b940fb 100644 --- a/src/ObservationTable.hs +++ b/src/ObservationTable.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE FlexibleContexts #-} @@ -10,18 +11,22 @@ import Functions import NLambda hiding (fromJust) import Teacher +import Control.DeepSeq (NFData, force) import Data.Maybe (fromJust) import GHC.Generics (Generic) import Prelude (Bool (..), Eq, Ord, Show, ($), (++), (.), uncurry) import qualified Prelude () -import Control.DeepSeq -- An observation table is a function S x E -> O -- (Also includes SA x E -> O) type Table i o = Fun ([i], [i]) o type Row i o = Fun [i] o +-- This is a rather arbitrary set of constraints +-- But I use them *everywhere*, so let's define them once and for all. +type LearnableAlphabet i = (NFData i, Contextual i, NominalType i, Show i) + -- `row is` denotes the data of a single row -- that is, the function E -> O row :: (NominalType i, NominalType o) => Table i o -> [i] -> Fun [i] o @@ -38,14 +43,12 @@ type BRow i = Row i Bool -- fills part of the table. First parameter is the rows (with extension), -- second is columns. Although the teacher provides us formulas instead of -- booleans, we can partition the answers to obtain actual booleans. -fillTable :: (Contextual i, NominalType i, Teacher t i) => t -> Set [i] -> Set [i] -> BTable i -fillTable teacher sssa ee = map tupleIso . Prelude.uncurry union . setTrueFalse . partition (\(_, _, f) -> f) $ base +fillTable :: LearnableAlphabet i => Teacher i -> Set [i] -> Set [i] -> BTable i +fillTable teacher sssa ee = force . Prelude.uncurry union . map2 (map slv) . map2 simplify . partition (\(_, _, f) -> f) $ base where base = pairsWith (\s e -> (s, e, membership teacher (s++e))) sssa ee - setTrueFalse (trueSet, falseSet) = (map (setThird True) trueSet, map (setThird False) falseSet) - setThird a (x, y, _) = (x, y, a) - tupleIso (x,y,z) = ((x,y),z) - + map2 f (a, b) = (f a, f b) + slv (a,b,f) = ((a,b), fromJust . solve $ f) -- Data structure representing the state of the learning algorithm (NOT a -- state in the automaton) @@ -64,7 +67,7 @@ instance NominalType i => Conditional (State i) where fromTup (t,ss,ssa,ee,aa) = State{..} -- Precondition: the set together with the current rows is prefix closed -addRows :: (Contextual i, NominalType i, Teacher t i) => t -> Set [i] -> State i -> State i +addRows :: LearnableAlphabet i => Teacher i -> Set [i] -> State i -> State i addRows teacher ds0 state@State{..} = state {t = t `union` dt, ss = ss `union` ds, ssa = ssa `union` dsa} where -- first remove redundancy @@ -76,7 +79,7 @@ addRows teacher ds0 state@State{..} = state {t = t `union` dt, ss = ss `union` d dt = fillTable teacher dsa ee -addColumns :: (Contextual i, NominalType i, Teacher t i) => t -> Set [i] -> State i -> State i +addColumns :: LearnableAlphabet i => Teacher i -> Set [i] -> State i -> State i addColumns teacher de0 state@State{..} = state {t = t `union` dt, ee = ee `union` de} where -- first remove redundancy diff --git a/src/Teacher.hs b/src/Teacher.hs index 5932024..89ea4a2 100644 --- a/src/Teacher.hs +++ b/src/Teacher.hs @@ -1,11 +1,10 @@ -{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE RankNTypes #-} {-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE FunctionalDependencies #-} -{-# LANGUAGE MultiParamTypeClasses #-} module Teacher where -import NLambda +import NLambda hiding (alphabet) +import qualified NLambda (alphabet) -- Explicit Prelude, as NLambda has quite some clashes import Data.Function (fix) @@ -22,36 +21,67 @@ 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) --- NOTE: Maybe neater when implemented as record? -class Teacher t i | t -> i where +data Teacher i = Teacher -- Given a sequence, check whether it is in the language -- Assumed to be equivariant - membership :: t -> [i] -> Formula + { membership :: [i] -> Formula -- Given a hypothesis, returns Nothing when equivalence or a (equivariant) - -- set of counter examples. - equivalent :: (Show q, NominalType q) => t -> Automaton q i -> Maybe (Set [i]) + -- 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 :: t -> Set i + , alphabet :: Set i + } + +-- We provide three ways to construct teachers: +-- 1. Fully automatic +-- 2. Fully interactive (via IO) +-- 3. Automatic membership, but interactive equivalence tests + +-- 1. This is a fully automatic teacher, which has an internal automaton +-- 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 = automaticMembership aut + , equivalent = automaticEquivalent aut + , alphabet = automaticAlphabet aut + } + +-- 2. Will ask everything to someone reading the terminal +-- For the moment only Atom as input type +-- Note that parsing is very unforgiving, one mistake, and there is no way back +-- Atoms are referenced by Ints. When the user provides a counter example, we +-- consider the whole orbit generated by it. +teacherWithIO :: Teacher Atom +teacherWithIO = Teacher + { membership = ioMembership + , equivalent = ioEquivalent + , alphabet = atoms + } + +-- 3. A teacher uses a target for the mebership queries, but you for equivalence +-- Useful as long as you don't have an equivalence check, For example for G-NFAs +teacherWithTargetAndIO :: NominalType q => Automaton q Atom -> Teacher Atom +teacherWithTargetAndIO aut = Teacher + { membership = automaticMembership aut + , equivalent = ioEquivalent + , alphabet = atoms + } --- Type for a teacher with an automaton as target --- The state type is abstracted away -data TeacherWithTarget i = forall q . NominalType q => TeacherWithTarget (Automaton q i) - --- Implements the teacher -instance (NominalType i) => Teacher (TeacherWithTarget i) i where - membership (TeacherWithTarget aut) input = accepts aut input - equivalent (TeacherWithTarget aut) hypo = case solve isEq of +-- Implementations of above functions +automaticMembership aut input = accepts aut input +automaticEquivalent aut hypo = case solve isEq of Nothing -> error "should be solved" Just True -> Nothing Just False -> Just bisimRes where bisimRes = bisim aut hypo isEq = isEmpty bisimRes - alphabet (TeacherWithTarget aut) = NLambda.alphabet aut +automaticAlphabet aut = NLambda.alphabet aut + instance Conditional a => Conditional (Identity a) where cond f x y = return (cond f (runIdentity x) (runIdentity y)) @@ -86,66 +116,60 @@ bisim aut1 aut2 = runIdentity $ go empty (pairsWith addEmptyWord (initialStates addEmptyWord x y = ([], x, y) --- Will ask everything to someone reading the terminal -data TeacherWithIO = TeacherWithIO +ioMembership :: (Show i, NominalType i) => [i] -> Formula +ioMembership input = unsafePerformIO $ do + let supp = leastSupport input + Prelude.putStrLn "\n# Is the following word accepted?" + Prelude.putStr "# " + Prelude.print input + Prelude.putStrLn "# You can answer with a formula (EQ, NEQ, AND, OR, T, F)" + Prelude.putStrLn "# You may use the following atoms:" + Prelude.putStr "# " + Prelude.print $ zip supp [0..] + answer <- runInputT defaultSettings loop + return $ interpret supp answer + where + loop = do + x <- getInputLine "> " + case x of + Nothing -> error "Quit" + Just str -> do + case readMaybe str :: Maybe Form of + Nothing -> do + outputStrLn $ "Unable to parse " ++ str ++ " :: Form" + loop + Just f -> return f --- For the moment only Atom as input type --- Note that parsing is very unforgiving, one mistake, and there is no way back --- Atoms are referenced by Ints. When the user provides a counter example, we --- consider the whole orbit generated by it. -instance Teacher TeacherWithIO Atom where - membership _ input = unsafePerformIO $ do - let supp = leastSupport input - Prelude.putStrLn "\n# Is the following word accepted?" - Prelude.putStr "# " - Prelude.print input - Prelude.putStrLn "# You can answer with a formula (EQ, NEQ, AND, OR, T, F)" - Prelude.putStrLn "# You may use the following atoms:" - Prelude.putStr "# " - Prelude.print $ zip supp [0..] - answer <- runInputT defaultSettings loop - return $ interpret supp answer - where - loop = do - x <- getInputLine "> " - case x of - Nothing -> error "Quit" - Just str -> do - case readMaybe str :: Maybe Form of - Nothing -> do - outputStrLn $ "Unable to parse " ++ str ++ " :: Form" - loop - Just f -> return f - equivalent _ hypothesis = unsafePerformIO $ do - Prelude.putStrLn "\n# Is the following automaton correct?" - Prelude.putStr "# " - Prelude.print hypothesis - Prelude.putStrLn "# Nothing for Yes, Just [...] for a counter example" - 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 "Quit" - Just str -> do - case readMaybe str :: Maybe (Maybe [Prelude.String]) of - Nothing -> do - outputStrLn $ "Unable to parse " ++ str ++ " :: Maybe [String]" - loop - Just f -> return f - alphabet _ = atoms +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 Yes, Just [...] for a counter example" + 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 "Quit" + Just str -> do + case readMaybe str :: Maybe (Maybe [Prelude.String]) of + Nothing -> do + outputStrLn $ "Unable to parse " ++ str ++ " :: Maybe [String]" + loop + Just f -> return f -- Data structure for reading formulas (with the derived Read instance) data Form @@ -164,13 +188,3 @@ interpret support (AND f1 f2) = interpret support f1 /\ interpret support f2 interpret support (OR f1 f2) = interpret support f1 \/ interpret support f2 interpret _ T = true interpret _ F = false - - --- A teacher uses a target for the mebership queries, but you for equivalence --- Useful as long as you don't have an equivalence check, For example for G-NFAs -data TeacherWithTargetAndIO i = forall q . NominalType q => TeacherWithTargetAndIO (Automaton q i) - -instance Teacher (TeacherWithTargetAndIO Atom) Atom where - membership (TeacherWithTargetAndIO aut) input = membership (TeacherWithTarget aut) input - equivalent (TeacherWithTargetAndIO aut) aut2 = equivalent TeacherWithIO aut2 - alphabet (TeacherWithTargetAndIO aut) = NLambda.alphabet aut