From 004e71ccd984c8e402c42c6ac21808ff862dec2f Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Thu, 28 Apr 2016 17:26:16 +0100 Subject: [PATCH] Code: some cleanup --- src/Examples/Contrived.hs | 38 ++++++++++--- src/Examples/Fifo.hs | 11 ++-- src/Examples/Stack.hs | 11 ++-- src/Functions.hs | 32 +++++++++++ src/Main.hs | 117 ++++++-------------------------------- src/ObservationTable.hs | 84 +++++++++++++++++++++++++++ src/Teacher.hs | 18 +++--- 7 files changed, 180 insertions(+), 131 deletions(-) create mode 100644 src/Functions.hs create mode 100644 src/ObservationTable.hs diff --git a/src/Examples/Contrived.hs b/src/Examples/Contrived.hs index 224e4d1..8f152ce 100644 --- a/src/Examples/Contrived.hs +++ b/src/Examples/Contrived.hs @@ -1,15 +1,11 @@ {-# LANGUAGE DeriveGeneric #-} module Examples.Contrived where -import Teacher - import NLambda -- Explicit Prelude, as NLambda has quite some clashes -import Data.Either (Either (..)) -import Data.Maybe (Maybe (..)) -import Prelude (Bool (..), Eq, Ord, Show, ($), (.)) -import qualified Prelude +import Prelude (Eq, Ord, Show, ($)) +import qualified Prelude () import GHC.Generics (Generic) @@ -18,6 +14,7 @@ import GHC.Generics (Generic) data Example1 = Initial | S1 Atom | S2 (Atom, Atom) deriving (Show, Eq, Ord, Generic) instance BareNominalType Example1 +example1 :: Automaton Example1 Atom example1 = automaton -- states, 4 orbits (of which one unreachable) (singleton Initial @@ -41,6 +38,7 @@ example1 = automaton -- trivial action. No registers. data Aut2 = Even | Odd deriving (Eq, Ord, Show, Generic) instance BareNominalType Aut2 +example2 :: Automaton Aut2 Atom example2 = automaton -- states, two orbits (fromList [Even, Odd]) @@ -59,6 +57,7 @@ example2 = automaton -- state, a state with a register and a sink state. data Aut3 = Empty | Stored Atom | Sink deriving (Eq, Ord, Show, Generic) instance BareNominalType Aut3 +example3 :: Automaton Aut3 Atom example3 = automaton -- states, three orbits (fromList [Empty, Sink] @@ -87,7 +86,7 @@ data Aut4 = Aut4Init -- Initial state | Sorted Atom Atom Atom -- State without symmetry deriving (Eq, Ord, Show, Generic) instance BareNominalType Aut4 - +example4 :: Automaton Aut4 Atom example4 = automaton -- states (singleton Aut4Init @@ -120,3 +119,28 @@ example4 = automaton atomsQuadruples = map (\[a,b,c,d] -> (a,b,c,d)) $ replicateAtoms 4 unc2 f (a,b) = f a b unc3 f (a,b,c) = f a b c + + +-- Accepts all two-symbols words with different atoms +data Aut5 = Aut5Init | Aut5Store Atom | Aut5T | Aut5F + deriving (Eq, Ord, Show, Generic) +instance BareNominalType Aut5 +example5 :: Automaton Aut5 Atom +example5 = automaton + -- states + (singleton Aut5Init + `union` map Aut5Store atoms + `union` singleton Aut5T + `union` singleton Aut5F) + -- alphabet + atoms + -- transitions + (map (\a -> (Aut5Init, a, Aut5Store a)) atoms + `union` map (\a -> (Aut5Store a, a, Aut5F)) atoms + `union` map (\(a, b) -> (Aut5Store a, b, Aut5T)) differentAtomsPairs + `union` map (\a -> (Aut5F, a, Aut5F)) atoms + `union` map (\a -> (Aut5T, a, Aut5F)) atoms) + -- initial states + (singleton Aut5Init) + -- final states + (singleton Aut5T) diff --git a/src/Examples/Fifo.hs b/src/Examples/Fifo.hs index dfed472..a3eee88 100644 --- a/src/Examples/Fifo.hs +++ b/src/Examples/Fifo.hs @@ -3,9 +3,9 @@ module Examples.Fifo (DataInput(..), fifoExample) where import GHC.Generics (Generic) import NLambda -import Prelude (Bool (..), Eq, Int, Maybe (..), Ord, Show, - length, reverse, ($), (+), (-), (.), (>=)) -import qualified Prelude +import Prelude (Eq, Int, Maybe (..), Ord, Show, length, reverse, + ($), (+), (-), (.), (>=)) +import qualified Prelude () -- Functional queue data type. First list is for push stuff onto, the @@ -21,10 +21,6 @@ pop (Fifo [] []) = Nothing pop (Fifo l1 []) = pop (Fifo [] (reverse l1)) pop (Fifo l1 (x:l2)) = Just (x, Fifo l1 l2) -isEmptyFifo :: Fifo a -> Bool -isEmptyFifo (Fifo [] []) = True -isEmptyFifo _ = False - emptyFifo :: Fifo a emptyFifo = Fifo [] [] @@ -48,6 +44,7 @@ instance Contextual DataInput where -- This representation is not minimal at all, but that's OK, since the -- learner will learn a minimal anyways. The parameter n is the bound. instance BareNominalType a => BareNominalType (Fifo a) +fifoExample :: Int -> Automaton (Maybe (Fifo Atom)) DataInput fifoExample n = automaton -- states (singleton Nothing diff --git a/src/Examples/Stack.hs b/src/Examples/Stack.hs index 4cfd17b..a472f81 100644 --- a/src/Examples/Stack.hs +++ b/src/Examples/Stack.hs @@ -4,9 +4,9 @@ module Examples.Stack (DataInput(..), stackExample) where import Examples.Fifo (DataInput (..)) import GHC.Generics (Generic) import NLambda -import Prelude (Bool (..), Eq, Int, Maybe (..), Ord, Show, - length, ($), (.), (>=)) -import qualified Prelude +import Prelude (Eq, Int, Maybe (..), Ord, Show, length, ($), + (.), (>=)) +import qualified Prelude () -- Functional stack data type is simply a list. @@ -19,10 +19,6 @@ pop :: Stack a -> Maybe (a, Stack a) pop (Stack []) = Nothing pop (Stack (x:l)) = Just (x, Stack l) -isEmptyStack :: Stack a -> Bool -isEmptyStack (Stack []) = True -isEmptyStack _ = False - emptyStack :: Stack a emptyStack = Stack [] @@ -40,6 +36,7 @@ sizeStack (Stack l1) = length l1 -- The automaton: States consist of stacks and a sink state. -- The parameter n is the bound. instance BareNominalType a => BareNominalType (Stack a) +stackExample :: Int -> Automaton (Maybe (Stack Atom)) DataInput stackExample n = automaton -- states (singleton Nothing diff --git a/src/Functions.hs b/src/Functions.hs new file mode 100644 index 0000000..31779f9 --- /dev/null +++ b/src/Functions.hs @@ -0,0 +1,32 @@ +module Functions where + +import NLambda +import Prelude (($)) +import qualified Prelude () + +-- We represent functions as their graphs +type Fun a b = Set (a, b) + +-- Basic manipulations on functions +-- Note that this returns a set, rather than an element +-- because we cannot extract a value from a singleton set +apply :: (NominalType a, NominalType b) => Fun a b -> a -> Set b +apply f a1 = mapFilter (\(a2, b) -> maybeIf (eq a1 a2) b) f + +-- AxB -> c is adjoint to A -> C^B +-- curry and uncurry witnesses both ways of the adjunction +curry :: (NominalType a, NominalType b, NominalType c) => Fun (a, b) c -> Fun a (Fun b c) +curry f = map (\a1 -> (a1, mapFilter (\((a2,b),c) -> maybeIf (eq a1 a2) (b,c)) f)) as + where as = map (\((a, _), _) -> a) f + +uncurry :: (NominalType a, NominalType b, NominalType c) => Fun a (Fun b c) -> Fun (a, b) c +uncurry f = sum $ map (\(a,s) -> map (\(b,c) -> ((a, b), c)) s) f + +-- Returns the subset (of the domain) which exhibits +-- different return values for the two functions +-- I am not sure about its correctness... +discrepancy :: (NominalType a, NominalType b) => Fun a b -> Fun a b -> Set a +discrepancy f1 f2 = + pairsWithFilter ( + \(a1,b1) (a2,b2) -> maybeIf (eq a1 a2 /\ neq b1 b2) a1 + ) f1 f2 diff --git a/src/Main.hs b/src/Main.hs index 6980125..0a168ae 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -1,93 +1,18 @@ -{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE RecordWildCards #-} import Examples +import Functions +import ObservationTable import Teacher import NLambda import Data.List (inits) -import Data.Maybe (fromJust) import Prelude hiding (and, curry, filter, lookup, map, not, sum, uncurry) -import GHC.Generics (Generic) - --- We represent functions as their graphs -type Fun a b = Set (a, b) - --- Basic manipulations on functions --- Note that this returns a set, rather than an element --- because we cannot extract a value from a singleton set -apply :: (NominalType a, NominalType b) => Fun a b -> a -> Set b -apply f a1 = mapFilter (\(a2, b) -> maybeIf (eq a1 a2) b) f - --- AxB -> c is adjoint to A -> C^B --- curry and uncurry witnesses both ways of the adjunction -curry :: (NominalType a, NominalType b, NominalType c) => Fun (a, b) c -> Fun a (Fun b c) -curry f = map (\a1 -> (a1, mapFilter (\((a2,b),c) -> maybeIf (eq a1 a2) (b,c)) f)) as - where as = map (\((a,b),c) -> a) f - -uncurry :: (NominalType a, NominalType b, NominalType c) => Fun a (Fun b c) -> Fun (a, b) c -uncurry f = sum $ map (\(a,s) -> map (\(b,c) -> ((a, b), c)) s) f - --- Returns the subset (of the domain) which exhibits --- different return values for the two functions --- I am not sure about its correctness... -discrepancy :: (NominalType a, NominalType b) => Fun a b -> Fun a b -> Set a -discrepancy f1 f2 = - pairsWithFilter ( - \(a1,b1) (a2,b2) -> maybeIf (eq a1 a2 /\ neq b1 b2) a1 - ) f1 f2 - - --- An observation table is a function S x E -> O --- (Also includes SA x E -> O) -type Table i o = Fun ([i], [i]) o - --- `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 -row t is = sum (apply (curry t) is) - --- `rowa is a` is the row for the one letter extensions -rowa :: (NominalType i, NominalType o) => Table i o -> [i] -> i -> Fun [i] o -rowa t is a = row t (is ++ [a]) - --- Our context -type Output = 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] -> Table i Output -fillTable teacher sssa ee = sum2 . map2 (map slv) . map2 simplify . partition (\(s, e, f) -> f) $ base - where - base = pairsWith (\s e -> (s, e, membership teacher (s++e))) sssa ee - map2 f (a, b) = (f a, f b) - slv (a,b,f) = ((a,b), Data.Maybe.fromJust . solve $ f) - sum2 (a,b) = a `union` b - - --- Data structure representing the state of the learning algorithm (NOT a --- state in the automaton) -data State i = State - { t :: Table i Output -- the table - , ss :: Set [i] -- state sequences - , ssa :: Set [i] -- their one letter extensions - , ee :: Set [i] -- suffixes - , aa :: Set i -- alphabet (remains constant) - } - deriving (Show, Ord, Eq, Generic) - -instance NominalType i => BareNominalType (State i) - -instance NominalType i => Conditional (State i) where - cond f s1 s2 = fromTup (cond f (toTup s1) (toTup s2)) where - toTup State{..} = (t,ss,ssa,ee,aa) - fromTup (t,ss,ssa,ee,aa) = State{..} -- We can determine its completeness with the following -- It returns all witnesses (of the form sa) for incompleteness @@ -106,7 +31,9 @@ inconsistency State{..} = ) ss ss aa where -- true for equal rows, but unequal extensions - candidate s1 s2 a = row t s1 `eq` row t s2 + -- we can safely skip equal sequences + candidate s1 s2 a = s1 `neq` s2 + /\ row t s1 `eq` row t s2 /\ rowa t s1 a `neq` rowa t s2 a -- This can be written for all monads. Unfortunately (a,) is also a monad and @@ -126,6 +53,9 @@ instance (Conditional a) => Conditional (IO a) where -- (Same holds for many other functions here) makeCompleteConsistent :: (Show i, Contextual i, NominalType i, Teacher t i) => t -> State i -> IO (State i) makeCompleteConsistent teacher state@State{..} = do + putStrLn "" + print state + putStrLn "" -- inc is the set of rows witnessing incompleteness, that is the sequences -- 's1 a' which do not have their equivalents of the form 's2'. let inc = incompleteness state @@ -137,15 +67,7 @@ makeCompleteConsistent teacher state@State{..} = do let ds = inc putStr " -> Adding rows: " print ds - -- ... and their extensions - let dsa = pairsWith (\s a -> s ++ [a]) ds aa - -- For the new rows, we fill the table - -- note that `ds ee` is already filled - let dt = fillTable teacher dsa ee - putStr " -> delta table: " - print dt - -- And we repeat - let state2 = state {t = t `union` dt, ss = ss `union` ds, ssa = ssa `union` dsa} + let state2 = addRows teacher ds state makeCompleteConsistent teacher state2 ) (do @@ -154,17 +76,13 @@ makeCompleteConsistent teacher state@State{..} = do ite (isNotEmpty inc2) (do -- If that set is non-empty, we should add new columns - putStrLn "Inconsistent!" + putStr "Inconsistent! : " + print inc2 -- The extensions are in the second component let de = sum $ map (\((s1,s2,a),es) -> map (a:) es) inc2 putStr " -> Adding columns: " print de - -- Fill that part of the table - let dt = fillTable teacher (ss `union` ssa) de - putStr " -> delta table: " - print dt - -- And we continue - let state2 = state {t = t `union` dt, ee = ee `union` de} + let state2 = addColumns teacher de state makeCompleteConsistent teacher state2 ) (do @@ -177,7 +95,7 @@ makeCompleteConsistent teacher state@State{..} = do -- Given a C&C table, constructs an automaton. The states are given by 2^E (not -- necessarily equivariant functions) -constructHypothesis :: NominalType i => State i -> Automaton (Fun [i] Output) i +constructHypothesis :: NominalType i => State i -> Automaton (BRow i) i constructHypothesis State{..} = automaton q a d i f where q = map (row t) ss @@ -195,15 +113,12 @@ useCounterExample teacher state@State{..} ces = do let ds = sum . map (fromList . inits) $ ces putStr " -> Adding rows: " print ds - -- as above, adding rows - let dsa = pairsWith (\s a -> s ++ [a]) ds aa - let dt = fillTable teacher dsa ee - let state2 = state {t = t `union` dt, ss = ss `union` ds, ssa = ssa `union` dsa} + let state2 = addRows teacher ds state return state2 -- 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 (Fun [i] Output) i) +loop :: (Show i, Contextual i, NominalType i, Teacher t i) => t -> State i -> IO (Automaton (BRow i) i) loop teacher s = do putStrLn "##################" putStrLn "1. Making it complete and consistent" @@ -229,7 +144,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 (Fun [i] Output) i) +learn :: (Show i, Contextual i, NominalType i, Teacher t i) => t -> IO (Automaton (BRow i) i) learn teacher = do let s = constructEmptyState teacher loop teacher s diff --git a/src/ObservationTable.hs b/src/ObservationTable.hs new file mode 100644 index 0000000..a14a9fa --- /dev/null +++ b/src/ObservationTable.hs @@ -0,0 +1,84 @@ +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE RecordWildCards #-} + +module ObservationTable where + +import Functions +import NLambda hiding (fromJust) +import Teacher + +import Data.Maybe (fromJust) +import GHC.Generics (Generic) +import Prelude (Bool (..), Eq, Ord, Show, ($), (++), (.)) +import qualified Prelude () + +-- 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 + +-- `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 +row t is = sum (apply (curry t) is) + +-- `rowa is a` is the row for the one letter extensions +rowa :: (NominalType i, NominalType o) => Table i o -> [i] -> i -> Fun [i] o +rowa t is a = row t (is ++ [a]) + +-- Teacher is restricted to Bools at the moment +type BTable i = Table i Bool +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 = sum2 . map2 (map slv) . map2 simplify . partition (\(_, _, f) -> f) $ base + where + base = pairsWith (\s e -> (s, e, membership teacher (s++e))) sssa ee + map2 f (a, b) = (f a, f b) + slv (a,b,f) = ((a,b), fromJust . solve $ f) + sum2 (a,b) = a `union` b + + +-- Data structure representing the state of the learning algorithm (NOT a +-- state in the automaton) +data State i = State + { t :: BTable i -- the table + , ss :: Set [i] -- state sequences + , ssa :: Set [i] -- their one letter extensions + , ee :: Set [i] -- suffixes + , aa :: Set i -- alphabet (remains constant) + } + deriving (Show, Ord, Eq, Generic) + +instance NominalType i => BareNominalType (State i) + +instance NominalType i => Conditional (State i) where + cond f s1 s2 = fromTup (cond f (toTup s1) (toTup s2)) where + toTup State{..} = (t,ss,ssa,ee,aa) + 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 teacher ds0 state@State{..} = state {t = t `union` dt, ss = ss `union` ds, ssa = ssa `union` dsa} + where + -- first remove redundancy + ds = ds0 \\ ss + -- extensions of new rows + dsa = pairsWith (\s a -> s ++ [a]) ds aa + -- For the new rows, we fill the table + -- note that `ds ee` is already filled + dt = fillTable teacher dsa ee + + +addColumns :: (Contextual i, NominalType i, Teacher t i) => t -> Set [i] -> State i -> State i +addColumns teacher de0 state@State{..} = state {t = t `union` dt, ee = ee `union` de} + where + -- first remove redundancy + de = de0 \\ ee + -- Fill that part of the table + dt = fillTable teacher (ss `union` ssa) de diff --git a/src/Teacher.hs b/src/Teacher.hs index d1c63bf..3c2d46a 100644 --- a/src/Teacher.hs +++ b/src/Teacher.hs @@ -11,9 +11,9 @@ import NLambda import Data.Function (fix) import Data.List (zip, (!!)) import Data.Maybe (Maybe (..)) -import Prelude (Bool (..), IO, Int, Read, Show, error, - fmap, length, return, ($), (++), (-), - (<), (==)) +import Prelude (Bool (..), Int, Read, Show, error, + length, return, ($), (++), (-), (<), + (==)) import qualified Prelude -- Used in the IO teacher @@ -79,7 +79,7 @@ instance Teacher TeacherWithIO Atom where 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, TRUE, FALSE)" + 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..] @@ -131,14 +131,14 @@ data Form | NEQ Int Int | AND Form Form | OR Form Form - | TRUE - | FALSE + | T + | F deriving (Read) interpret :: [Atom] -> Form -> Formula interpret support (EQ i j) = eq (support !! i) (support !! j) interpret support (NEQ i j) = neq (support !! i) (support !! j) interpret support (AND f1 f2) = interpret support f1 /\ interpret support f2 -interpret support (OR f1 f2) = interpret support f1 \/ interpret support f1 -interpret _ TRUE = true -interpret _ FALSE = false +interpret support (OR f1 f2) = interpret support f1 \/ interpret support f2 +interpret _ T = true +interpret _ F = false