joshua/nominal-lstar
1
Fork 0
mirror of https://github.com/Jaxan/nominal-lstar.git synced 2025-04-26 22:27:46 +02:00
Code Issues Releases Activity

Code: Angluin's algorithm with NLambda

Browse source
This commit is contained in:
Joshua Moerman 2016-04-14 17:35:42 +01:00
commit d52f991a74
8 changed files with 700 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
NominalAngluin.cabal Normal file
View file

@ -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

2
Setup.hs Normal file
View file

@ -0,0 +1,2 @@
import Distribution.Simple
main = defaultMain

16
src/Examples.hs Normal file
View file

@ -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

123
src/Examples/Contrived.hs Normal file
View file

@ -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

75
src/Examples/Fifo.hs Normal file
View file

@ -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

67
src/Examples/Stack.hs Normal file
View file

@ -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

243
src/Main.hs Normal file
View file

@ -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

146
src/Teacher.hs Normal file
View file

@ -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