From d52f991a741d5ac4a74bd94298125e417d9da202 Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Thu, 14 Apr 2016 17:35:42 +0100 Subject: [PATCH] Code: Angluin's algorithm with NLambda --- NominalAngluin.cabal | 28 +++++ Setup.hs | 2 + src/Examples.hs | 16 +++ src/Examples/Contrived.hs | 123 +++++++++++++++++++ src/Examples/Fifo.hs | 75 ++++++++++++ src/Examples/Stack.hs | 67 +++++++++++ src/Main.hs | 243 ++++++++++++++++++++++++++++++++++++++ src/Teacher.hs | 146 +++++++++++++++++++++++ 8 files changed, 700 insertions(+) create mode 100644 NominalAngluin.cabal create mode 100644 Setup.hs create mode 100644 src/Examples.hs create mode 100644 src/Examples/Contrived.hs create mode 100644 src/Examples/Fifo.hs create mode 100644 src/Examples/Stack.hs create mode 100644 src/Main.hs create mode 100644 src/Teacher.hs diff --git a/NominalAngluin.cabal b/NominalAngluin.cabal new file mode 100644 index 0000000..5b4becd --- /dev/null +++ b/NominalAngluin.cabal @@ -0,0 +1,28 @@ +-- Initial NominalAngluin.cabal generated by cabal init. For further +-- documentation, see http://haskell.org/cabal/users-guide/ + +name: NominalAngluin +version: 0.1.0.0 +-- synopsis: +-- description: +-- license: +license-file: LICENSE +author: Joshua Moerman +maintainer: lakseru@gmail.com +-- copyright: +-- category: +build-type: Simple +-- extra-source-files: +cabal-version: >=1.10 + +executable NominalAngluin + main-is: Main.hs + -- other-modules: + -- other-extensions: + build-depends: + base >=4.8 && <4.9, + containers, + NLambda, + readline + hs-source-dirs: src + default-language: Haskell2010 diff --git a/Setup.hs b/Setup.hs new file mode 100644 index 0000000..9a994af --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/src/Examples.hs b/src/Examples.hs new file mode 100644 index 0000000..13ec4d3 --- /dev/null +++ b/src/Examples.hs @@ -0,0 +1,16 @@ +module Examples + ( module Examples + , module Examples.Contrived + , module Examples.Fifo + , module Examples.Stack + ) where + +import Examples.Contrived +import Examples.Fifo +import Examples.Stack +import NLambda (Atom) +import Teacher (TeacherWithTarget (..)) + +-- Wrapping it in a teacher +exampleTeacher :: TeacherWithTarget Atom +exampleTeacher = TeacherWithTarget example4 diff --git a/src/Examples/Contrived.hs b/src/Examples/Contrived.hs new file mode 100644 index 0000000..700be6b --- /dev/null +++ b/src/Examples/Contrived.hs @@ -0,0 +1,123 @@ +{-# LANGUAGE DeriveGeneric #-} +module Examples.Contrived where + +import Teacher + +import NLambda hiding (a, b, c, d, e, f, g, h, i, j, k, l, m, n, + o, p, q, r, s, t, u, v, w, x, y, z) + +-- 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 GHC.Generics (Generic) + +-- Example automaton from the whiteboard. Three orbits with 0, 1 and 2 +-- registers. The third orbit has a local symmetry (S2). +data Example1 = Initial | S1 Atom | S2 (Atom, Atom) + deriving (Show, Eq, Ord, Generic) +instance BareNominalType Example1 +example1 = automaton + -- states, 4 orbits (of which one unreachable) + (singleton Initial + `union` map S1 atoms + `union` map S2 atomsPairs) + -- alphabet + atoms + -- transitions + (map (\a -> (Initial, a, S1 a)) atoms + `union` map (\a -> (S1 a, a, Initial)) atoms + `union` mapFilter (\(a, b) -> maybeIf (neq a b) (S1 a, b, S2 (a, b))) atomsPairs + `union` mapFilter (\(a, b, c) -> maybeIf (eq a c \/ eq b c) (S2 (a, b), c, Initial)) atomsTriples + `union` mapFilter (\(a, b, c) -> maybeIf (neq a c /\ neq b c) (S2 (a, b), c, S1 c)) atomsTriples) + -- initial states + (singleton Initial) + -- final states + (map S2 atomsPairs) + + +-- Accepts all even words (ignores the alphabet). Two orbits, with a +-- trivial action. No registers. +data Aut2 = Even | Odd deriving (Eq, Ord, Show, Generic) +instance BareNominalType Aut2 +example2 = automaton + -- states, two orbits + (fromList [Even, Odd]) + -- alphabet + atoms + -- transitions + (map (\a -> (Even, a, Odd)) atoms + `union` map (\a -> (Odd, a, Even)) atoms) + -- initial states + (singleton Even) + -- final states + (singleton Even) + + +-- Accepts all non-empty words with the same symbol. Three orbits: the initial +-- 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 + -- states, three orbits + (fromList [Empty, Sink] + `union` map Stored atoms) + -- alphabet + atoms + -- transitions + (map (\a -> (Empty, a, Stored a)) atoms + `union` map (\a -> (Stored a, a, Stored a)) atoms + `union` map (\(a,b) -> (Stored a, b, Sink)) differentAtomsPairs + `union` map (\a -> (Sink, a, Sink)) atoms) + -- initial states + (singleton Empty) + -- final states + (map Stored atoms) + + +-- Example showing that a local symmetry is not always the full symmetric group +-- or trivial. Five (reachable) orbits. The state Symm a b c has a C3 symmetry, +-- i.e. we can shift: Symm a b c ~ Symm b c a, but not swap: Symm a b c !~ +-- Symm a c b (here ~ means bisimilar). +data Aut4 = Aut4Init -- Initial state + | First Atom -- State after reading 1 symbol + | Second Atom Atom -- After reading two different symbols + | Symm Atom Atom Atom -- Accepting state with C3 symmetry + | Sorted Atom Atom Atom -- State without symmetry + deriving (Eq, Ord, Show, Generic) +instance BareNominalType Aut4 + +example4 = automaton + -- states + (singleton Aut4Init + `union` map First atoms + `union` map (unc2 Second) atomsPairs + `union` map (unc3 Symm) atomsTriples + `union` map (unc3 Sorted) atomsTriples) + -- alphabet + atoms + -- transitions + (map (\a -> (Aut4Init, a, First a)) atoms + `union` map (\a -> (First a, a, Aut4Init)) atoms + `union` map (\(a, b) -> (First a, b, Second a b)) differentAtomsPairs + `union` map (\(a, b) -> (Second a b, a, Aut4Init)) atomsPairs + `union` map (\(a, b) -> (Second a b, b, Aut4Init)) atomsPairs + `union` mapFilter (\(a, b, c) -> maybeIf (c `neq` a /\ c `neq` b) (Second a b, c, Symm a b c)) atomsTriples + `union` mapFilter (\(a, b, c, d) -> maybeIf (d `neq` a /\ d `neq` b /\ d `neq` c) (Symm a b c, d, Aut4Init)) atomsQuadruples + `union` map (\(a, b, c) -> (Symm a b c, a, Sorted a b c)) atomsTriples + `union` map (\(a, b, c) -> (Symm a b c, b, Sorted b c a)) atomsTriples + `union` map (\(a, b, c) -> (Symm a b c, c, Sorted c a b)) atomsTriples + `union` mapFilter (\(a, b, c, d) -> maybeIf (d `neq` a /\ d `neq` b /\ d `neq` c) (Sorted a b c, d, First d)) atomsQuadruples + `union` map (\(a, b, c) -> (Sorted a b c, a, Sorted a b c)) atomsTriples + `union` map (\(a, b, c) -> (Sorted a b c, b, Symm a b c)) atomsTriples + `union` map (\(a, b, c) -> (Sorted a b c, c, Aut4Init)) atomsTriples) + -- initial states + (singleton Aut4Init) + -- final states + (map (unc3 Symm) atomsTriples) + where + 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 diff --git a/src/Examples/Fifo.hs b/src/Examples/Fifo.hs new file mode 100644 index 0000000..dfed472 --- /dev/null +++ b/src/Examples/Fifo.hs @@ -0,0 +1,75 @@ +{-# LANGUAGE DeriveGeneric #-} +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 + + +-- Functional queue data type. First list is for push stuff onto, the +-- second list is to pop. If the second list is empty, it will reverse +-- the first. +data Fifo a = Fifo [a] [a] deriving (Eq, Ord, Show, Generic) + +push :: a -> Fifo a -> Fifo a +push x (Fifo l1 l2) = Fifo (x:l1) l2 + +pop :: Fifo a -> Maybe (a, Fifo a) +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 [] [] + +sizeFifo :: Fifo a -> Int +sizeFifo (Fifo l1 l2) = length l1 + length l2 + + +-- Our automaton accepts valid traces for this data structure. For +-- example Put(a) Get(a) is valid, but Put(a) Get(b) is only valid if +-- a = b. We will bound the number of states to make it a finite orbit +-- nominal automaton. + +-- The alphabet: +data DataInput = Put Atom | Get Atom deriving (Eq, Ord, Show, Generic) +instance BareNominalType DataInput +instance Contextual DataInput where + when f (Put a) = Put (when f a) + when f (Get a) = Get (when f a) + +-- The automaton: States consist of fifo queues and a sink state. +-- 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 n = automaton + -- states + (singleton Nothing + `union` map Just allStates) + -- alphabet + (map Put atoms `union` map Get atoms) + -- transitions + (map (\a -> (Nothing, Put a, Nothing)) atoms + `union` map (\a -> (Nothing, Get a, Nothing)) atoms + `union` pairsWith (\s a -> (Just s, Put a, nextState s a)) allStates atoms + `union` sum (map prevStates allStates)) + -- initial states + (singleton (Just emptyFifo)) + -- final states + (map Just allStates) + where + allStates = sum . fromList $ [states i | i <- [0..n]] + states i = sum . fromList $ [ pairsWith Fifo (replicateAtoms j) (replicateAtoms (i - j)) | j <- [0 .. i]] + nextState fifo a = if sizeFifo fifo >= n + then Nothing + else Just (push a fifo) + prevStates fifo = case pop fifo of + Nothing -> map (\a -> (Just fifo, Get a, Nothing)) atoms + Just (b, fifo2) -> singleton (Just fifo, Get b, Just fifo2) + `union` mapFilter (\a -> maybeIf (a `neq` b) (Just fifo, Get a, Nothing)) atoms diff --git a/src/Examples/Stack.hs b/src/Examples/Stack.hs new file mode 100644 index 0000000..4cfd17b --- /dev/null +++ b/src/Examples/Stack.hs @@ -0,0 +1,67 @@ +{-# LANGUAGE DeriveGeneric #-} +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 + + +-- Functional stack data type is simply a list. +data Stack a = Stack [a] deriving (Eq, Ord, Show, Generic) + +push :: a -> Stack a -> Stack a +push x (Stack l1) = Stack (x:l1) + +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 [] + +sizeStack :: Stack a -> Int +sizeStack (Stack l1) = length l1 + + +-- Our automaton accepts valid traces for this data structure. For +-- example Put(a) Get(a) is valid, but Put(a) Get(b) is only valid if +-- a = b. We will bound the number of states to make it a finite orbit +-- nominal automaton. + +-- The alphabet is defined in Examples.Fifo + +-- The automaton: States consist of stacks and a sink state. +-- The parameter n is the bound. +instance BareNominalType a => BareNominalType (Stack a) +stackExample n = automaton + -- states + (singleton Nothing + `union` map Just allStates) + -- alphabet + (map Put atoms `union` map Get atoms) + -- transitions + (map (\a -> (Nothing, Put a, Nothing)) atoms + `union` map (\a -> (Nothing, Get a, Nothing)) atoms + `union` pairsWith (\s a -> (Just s, Put a, nextState s a)) allStates atoms + `union` sum (map prevStates allStates)) + -- initial states + (singleton (Just emptyStack)) + -- final states + (map Just allStates) + where + allStates = sum . fromList $ [states i | i <- [0..n]] + states i = map Stack (replicateAtoms i) + nextState stack a = if sizeStack stack >= n + then Nothing + else Just (push a stack) + prevStates stack = case pop stack of + Nothing -> map (\a -> (Just stack, Get a, Nothing)) atoms + Just (b, stack2) -> singleton (Just stack, Get b, Just stack2) + `union` mapFilter (\a -> maybeIf (a `neq` b) (Just stack, Get a, Nothing)) atoms diff --git a/src/Main.hs b/src/Main.hs new file mode 100644 index 0000000..06d9871 --- /dev/null +++ b/src/Main.hs @@ -0,0 +1,243 @@ +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE RecordWildCards #-} + +import Examples +import Teacher + +import NLambda hiding (a, b, c, d, e, f, g, h, i, j, k, l, m, + n, o, p, q, r, s, t, u, v, w, x, y, z) + +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 +incompleteness :: NominalType i => State i -> Set [i] +incompleteness State{..} = filter (not . hasEqRow) ssa + where + -- true if the sequence sa has an equivalent row in ss + hasEqRow sa = exists (\s2 -> eq (row t sa) (row t s2)) ss + +-- We can determine its consistency with the following +-- Returns equivalent rows (fst) with all inequivalent extensions (snd) +inconsistency :: NominalType i => State i -> Set (([i], [i], i), Set [i]) +inconsistency State{..} = + triplesWithFilter ( + \s1 s2 a -> maybeIf (candidate s1 s2 a) ((s1, s2, a), discrepancy (rowa t s1 a) (rowa t s2 a)) + ) ss ss aa + where + -- true for equal rows, but unequal extensions + candidate s1 s2 a = 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 +-- this gives rise to overlapping instances, so I only do it for IO here. +-- Note that it is not really well defined, but it kinda works. +instance (Conditional a) => Conditional (IO a) where + cond f a b = case solve f of + Just True -> a + Just False -> b + Nothing -> fail "### Unresolved branch ###" + -- NOTE: another implementation would be to evaluate both a and b + -- and apply ite to their results. This however would runs both side + -- effects of a and b. + +-- 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 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'. + let inc = incompleteness state + ite (isNotEmpty inc) + (do + -- If that set is non-empty, we should add new rows + putStrLn "Incomplete!" + -- These will be the new rows, ... + 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} + makeCompleteConsistent teacher state2 + ) + (do + -- inc2 is the set of inconsistencies. + let inc2 = inconsistency state + ite (isNotEmpty inc2) + (do + -- If that set is non-empty, we should add new columns + putStrLn "Inconsistent!" + -- 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} + makeCompleteConsistent teacher state2 + ) + (do + -- If both sets are empty, the table is complete and + -- consistent, so we are done. + putStrLn " => Complete + Consistent :D!" + return state + ) + ) + +-- 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 State{..} = automaton q a d i f + where + q = map (row t) ss + a = aa + d = pairsWith (\s a -> (row t s, a, rowa t s a)) ss aa + i = singleton $ row t [] + f = mapFilter (\s -> maybeIf (toform $ apply t (s, [])) (row t s)) ss + toform s = forAll id . map fromBool $ s + +-- Extends the table with all prefixes of a set of counter examples. +useCounterExample :: (Show i, Contextual i, NominalType i, Teacher t i) => t -> State i -> Set [i] -> IO (State i) +useCounterExample teacher state@State{..} ces = do + putStr "Using ce: " + print ces + 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} + 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 teacher s = do + putStrLn "##################" + putStrLn "1. Making it complete and consistent" + s <- makeCompleteConsistent teacher s + putStrLn "2. Constructing hypothesis" + let h = constructHypothesis s + print h + putStr "3. Equivalent? " + let eq = equivalent teacher h + print eq + case eq of + Nothing -> return h + Just ce -> do + s <- useCounterExample teacher s ce + loop teacher s + +constructEmptyState :: (Contextual i, NominalType i, Teacher t i) => t -> State i +constructEmptyState teacher = + let aa = Teacher.alphabet teacher in + let ss = singleton [] in + let ssa = pairsWith (\s a -> s ++ [a]) ss aa in + let ee = singleton [] in + 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 teacher = do + let s = constructEmptyState teacher + loop teacher s + +-- Initializes the table and runs the algorithm. +main :: IO () +main = do + h <- learn exampleTeacher + putStrLn "Finished! Final hypothesis =" + print h diff --git a/src/Teacher.hs b/src/Teacher.hs new file mode 100644 index 0000000..19516ec --- /dev/null +++ b/src/Teacher.hs @@ -0,0 +1,146 @@ +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE MultiParamTypeClasses #-} + +module Teacher where + +import NLambda hiding (a, b, c, d, e, f, g, h, i, j, + k, l, m, n, o, p, q, r, s, t, u, v, w, + x, y, z) + +-- Explicit Prelude, as NLambda has quite some clashes +import Data.Function (fix) +import Data.List (zip, (!!)) +import Data.Maybe (Maybe (..)) +import Prelude (Bool (..), IO, Int, Read, Show, error, + fmap, length, return, ($), (++), (-), + (<), (==)) +import qualified Prelude + +-- Used in the IO teacher +import System.Console.Readline +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 + -- Given a sequence, check whether it is in the language + -- Assumed to be equivariant + membership :: t -> [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]) + -- Returns the alphabet to the learner + alphabet :: t -> Set i + + +-- 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 + Nothing -> error "should be solved" + Just True -> Nothing + Just False -> Just ce + where + isEq = equivalentDA aut hypo + lDiff = aut `differenceDA` hypo + rDiff = hypo `differenceDA` aut + symmDiff = lDiff `unionDA` rDiff + ce = searchWord symmDiff + alphabet (TeacherWithTarget aut) = NLambda.alphabet aut + +-- Searching a word in the difference automaton +-- Will find all shortest ones +searchWord :: (NominalType i, NominalType q) => Automaton q i -> Set [i] +searchWord d = go (singleton []) + where + go aa = let candidates = filter (accepts d) aa in + ite (isEmpty candidates) + (go $ pairsWith (\as a -> a:as) aa (NLambda.alphabet d)) + candidates + + +-- Will ask everything to someone reading the terminal +data TeacherWithIO = TeacherWithIO + +-- 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, TRUE, FALSE)" + Prelude.putStrLn "# You may use the following atoms:" + Prelude.putStr "# " + Prelude.print $ zip supp [0..] + answer <- fix (\m -> do + x <- readline "> " + case x of + Nothing -> error "Quit" + Just str -> do + case readMaybe str :: Maybe Form of + Nothing -> do + Prelude.putStrLn $ "Unable to parse " ++ str ++ " :: Form" + m + Just f -> return f + ) + return $ interpret supp answer + 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 <- fix (\m -> do + x <- readline "> " + case x of + Nothing -> error "Quit" + Just str -> do + case readMaybe str :: Maybe (Maybe [Prelude.String]) of + Nothing -> do + Prelude.putStrLn $ "Unable to parse " ++ str ++ " :: Maybe [String]" + m + Just f -> return f + ) + 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 + alphabet _ = atoms + +-- Data structure for reading formulas (with the derived Read instance) +data Form + = EQ Int Int + | NEQ Int Int + | AND Form Form + | OR Form Form + | TRUE + | FALSE + 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