mirror of
https://github.com/Jaxan/nominal-lstar.git
synced 2025-04-27 14:47:45 +02:00
Refactors the code to use simpler types.
This commit is contained in:
Joshua Moerman
parent
9ee755117e
commit
43c85612bb
5 changed files with 131 additions and 115 deletions
|
|
@ -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
|
||||
|
|
|
|||
15
src/Main.hs
15
src/Main.hs
|
|
@ -6,7 +6,6 @@ import Examples
|
|||
import Functions
|
||||
import ObservationTable
|
||||
import Teacher
|
||||
|
||||
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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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,15 +116,8 @@ 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
|
||||
|
||||
-- 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
|
||||
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 "# "
|
||||
|
|
@ -116,7 +139,9 @@ instance Teacher TeacherWithIO Atom where
|
|||
outputStrLn $ "Unable to parse " ++ str ++ " :: Form"
|
||||
loop
|
||||
Just f -> return f
|
||||
equivalent _ hypothesis = unsafePerformIO $ do
|
||||
|
||||
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
|
||||
|
|
@ -145,7 +170,6 @@ instance Teacher TeacherWithIO Atom where
|
|||
outputStrLn $ "Unable to parse " ++ str ++ " :: Maybe [String]"
|
||||
loop
|
||||
Just f -> return f
|
||||
alphabet _ = atoms
|
||||
|
||||
-- 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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue