mirror of
https://github.com/Jaxan/nominal-lstar.git
synced 2025-04-27 14:47:45 +02:00
Refactors code to be more modular.
Now all three variations: Angluin, Bollig and homebrew NL* are using the same framework. I did not extensively test the refactor.
This commit is contained in:
Joshua Moerman
parent
f24ed31ac8
commit
9ac25c4d9b
6 changed files with 148 additions and 305 deletions
93
src/Angluin.hs
Normal file
93
src/Angluin.hs
Normal file
|
|
@ -0,0 +1,93 @@
|
|||
{-# LANGUAGE RecordWildCards #-}
|
||||
module Angluin where
|
||||
|
||||
import AbstractLStar
|
||||
import ObservationTable
|
||||
import Teacher
|
||||
|
||||
import Data.List (inits, tails)
|
||||
import Debug.Trace
|
||||
import NLambda
|
||||
import qualified Prelude hiding ()
|
||||
import Prelude (Bool(..), Maybe(..), id, ($), (.), (++), fst, show)
|
||||
|
||||
-- We can determine its completeness with the following
|
||||
-- It returns all witnesses (of the form sa) for incompleteness
|
||||
closednessTest :: NominalType i => State i -> TestResult i
|
||||
closednessTest State{..} = case solve (isEmpty defect) of
|
||||
Just True -> Succes
|
||||
Just False -> trace "Not closed" $ Failed defect empty
|
||||
where
|
||||
sss = map (row t) ss -- all the rows
|
||||
hasEqRow = contains sss . row t -- has equivalent upper row
|
||||
defect = filter (not . hasEqRow) ssa -- all rows without equivalent guy
|
||||
|
||||
-- We can determine its consistency with the following
|
||||
consistencyTestJ :: NominalType i => State i -> TestResult i -- Set (([i], [i], i), Set [i])
|
||||
consistencyTestJ State{..} = case solve (isEmpty defect) of
|
||||
Just True -> Succes
|
||||
Just False -> trace "Not consistent" $ Failed empty columns
|
||||
where
|
||||
-- true for equal rows, but unequal extensions
|
||||
-- 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
|
||||
defect = triplesWithFilter (
|
||||
\s1 s2 a -> maybeIf (candidate s1 s2 a) ((s1, s2, a), discrepancy (rowa t s1 a) (rowa t s2 a))
|
||||
) ss ss aa
|
||||
columns = sum $ map (\((s1,s2,a),es) -> map (a:) es) defect
|
||||
|
||||
-- Bartek's faster version
|
||||
consistencyTestB :: NominalType i => State i -> TestResult i -- Set (([i], [i], i), Set [i])
|
||||
consistencyTestB State{..} = case solve (isEmpty defect) of
|
||||
Just True -> Succes
|
||||
Just False -> trace "Not consistent" $ Failed empty columns
|
||||
where
|
||||
rowPairs = pairsWithFilter (\s1 s2 -> maybeIf (candidate0 s1 s2) (s1,s2)) ss ss
|
||||
candidate0 s1 s2 = s1 `neq` s2 /\ row t s1 `eq` row t s2
|
||||
candidate1 s1 s2 a = rowa t s1 a `neq` rowa t s2 a
|
||||
defect = pairsWithFilter (
|
||||
\(s1, s2) a -> maybeIf (candidate1 s1 s2 a) ((s1, s2, a), discrepancy (rowa t s1 a) (rowa t s2 a))
|
||||
) rowPairs aa
|
||||
columns = sum $ map (\((s1,s2,a),es) -> map (a:) es) defect
|
||||
|
||||
-- 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 (BRow i) 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.
|
||||
useCounterExampleAngluin :: LearnableAlphabet i => Teacher i -> State i -> Set [i] -> State i
|
||||
useCounterExampleAngluin teacher state@State{..} ces =
|
||||
trace ("Using ce: " ++ show ces) $
|
||||
let ds = sum . map (fromList . inits) $ ces in
|
||||
addRows teacher ds state
|
||||
|
||||
-- This is the variant by Maler and Pnueli
|
||||
-- I used to think it waw Rivest and Schapire, but they add less columns
|
||||
useCounterExampleMP :: LearnableAlphabet i => Teacher i -> State i -> Set [i] -> State i
|
||||
useCounterExampleMP teacher state@State{..} ces =
|
||||
trace ("Using ce: " ++ show ces) $
|
||||
let de = sum . map (fromList . tails) $ ces in
|
||||
addColumns teacher de state
|
||||
|
||||
makeCompleteAngluin :: LearnableAlphabet i => TableCompletionHandler i
|
||||
makeCompleteAngluin = makeCompleteWith [closednessTest, consistencyTestB]
|
||||
|
||||
-- Default: use counter examples in columns, which is slightly faster
|
||||
learnAngluin :: LearnableAlphabet i => Teacher i -> Automaton (BRow i) i
|
||||
learnAngluin teacher = learn makeCompleteAngluin useCounterExampleMP constructHypothesis teacher initial
|
||||
where initial = constructEmptyState teacher
|
||||
|
||||
-- The "classical" version, where counter examples are added as rows
|
||||
learnAngluinRows :: LearnableAlphabet i => Teacher i -> Automaton (BRow i) i
|
||||
learnAngluinRows teacher = learn makeCompleteAngluin useCounterExampleAngluin constructHypothesis teacher initial
|
||||
where initial = constructEmptyState teacher
|
||||
|
|
@ -2,6 +2,7 @@
|
|||
module Bollig where
|
||||
|
||||
import AbstractLStar
|
||||
import Angluin
|
||||
import ObservationTable
|
||||
import Teacher
|
||||
|
||||
|
|
@ -11,7 +12,11 @@ import NLambda
|
|||
import qualified Prelude hiding ()
|
||||
import Prelude (Bool(..), Maybe(..), ($), (.), (++), fst, show)
|
||||
|
||||
-- See also NLStar.hs for this hack
|
||||
-- So at the moment we only allow sums of the form a + b and a + b + c
|
||||
-- Of course we should approximate the powerset a bit better
|
||||
-- But for the main examples, we know this is enough!
|
||||
-- I (Joshua) believe it is possible to give a finite-orbit
|
||||
-- approximation, but the code will not be efficient...
|
||||
hackApproximate :: NominalType a => Set a -> Set (Set a)
|
||||
hackApproximate set = empty
|
||||
`union` map singleton set
|
||||
|
|
@ -51,7 +56,7 @@ rfsaClosednessTest State{..} = case solve (isEmpty defect) of
|
|||
rfsaConsistencyTest :: LearnableAlphabet i => State i -> TestResult i
|
||||
rfsaConsistencyTest State{..} = case solve (isEmpty defect) of
|
||||
Just True -> Succes
|
||||
Just False -> trace "Not consistent" $ Failed empty defect
|
||||
Just False -> trace ("Not consistent, defect = " ++ show defect) $ Failed empty defect
|
||||
Nothing -> trace "@@@ Unsolved Formula (rfsaConsistencyTest) @@@" $
|
||||
Failed empty defect
|
||||
where
|
||||
|
|
@ -68,16 +73,9 @@ constructHypothesisBollig State{..} = automaton q a d i f
|
|||
d0 = triplesWithFilter (\s a s2 -> maybeIf (row t s2 `sublang` rowa t s a) (row t s, a, row t s2)) ss aa ss
|
||||
d = filter (\(q1,a,q2) -> q1 `member` q /\ q2 `member` q) d0
|
||||
|
||||
-- Copied from the classical DFA-algorithm, column version
|
||||
useCECopy :: LearnableAlphabet i => Teacher i -> State i -> Set [i] -> State i
|
||||
useCECopy teacher state@State{..} ces =
|
||||
trace ("Using ce:" ++ show ces) $
|
||||
let de = sum . map (fromList . tails) $ ces in
|
||||
addColumns teacher de state
|
||||
|
||||
makeCompleteBollig :: LearnableAlphabet i => TableCompletionHandler i
|
||||
makeCompleteBollig = makeCompleteWith [rfsaClosednessTest, rfsaConsistencyTest]
|
||||
|
||||
learnBollig :: LearnableAlphabet i => Teacher i -> Automaton (BRow i) i
|
||||
learnBollig teacher = learn makeCompleteBollig useCECopy constructHypothesisBollig teacher initial
|
||||
learnBollig teacher = learn makeCompleteBollig useCounterExampleMP constructHypothesisBollig teacher initial
|
||||
where initial = constructEmptyState teacher
|
||||
|
|
|
|||
|
|
@ -1,32 +0,0 @@
|
|||
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
|
||||
158
src/Main.hs
158
src/Main.hs
|
|
@ -1,165 +1,11 @@
|
|||
{-# LANGUAGE RecordWildCards #-}
|
||||
|
||||
import Angluin
|
||||
import Bollig
|
||||
import Examples
|
||||
import Functions
|
||||
import ObservationTable
|
||||
import Teacher
|
||||
import NLStar
|
||||
|
||||
import NLambda
|
||||
|
||||
import Control.DeepSeq
|
||||
import Data.List (inits, tails)
|
||||
import Debug.Trace
|
||||
import Prelude hiding (and, curry, filter, lookup, map, not,
|
||||
sum, uncurry)
|
||||
|
||||
|
||||
-- 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
|
||||
sss = map (row t) ss
|
||||
-- true if the sequence sa has an equivalent row in ss
|
||||
hasEqRow = contains sss . row t
|
||||
|
||||
-- We can determine its consistency with the following
|
||||
-- Returns equivalent rows (fst) with all inequivalent extensions (snd)
|
||||
inconsistencyJoshua :: NominalType i => State i -> Set (([i], [i], i), Set [i])
|
||||
inconsistencyJoshua 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
|
||||
-- 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
|
||||
|
||||
inconsistencyBartek :: NominalType i => State i -> Set (([i], [i], i), Set [i])
|
||||
inconsistencyBartek State{..} =
|
||||
pairsWithFilter (
|
||||
\(s1, s2) a -> maybeIf (candidate1 s1 s2 a) ((s1, s2, a), discrepancy (rowa t s1 a) (rowa t s2 a))
|
||||
) rowPairs aa
|
||||
where
|
||||
rowPairs = pairsWithFilter (\s1 s2 -> maybeIf (candidate0 s1 s2) (s1,s2)) ss ss
|
||||
candidate0 s1 s2 = s1 `neq` s2 /\ row t s1 `eq` row t s2
|
||||
candidate1 s1 s2 a = rowa t s1 a `neq` rowa t s2 a
|
||||
|
||||
inconsistency :: NominalType i => State i -> Set (([i], [i], i), Set [i])
|
||||
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 :: LearnableAlphabet i => Teacher i -> State i -> State i
|
||||
makeCompleteConsistent teacher state@State{..} =
|
||||
-- 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 in
|
||||
ite (isNotEmpty inc)
|
||||
( -- If that set is non-empty, we should add new rows
|
||||
trace "Incomplete! Adding rows:" $
|
||||
-- These will be the new rows, ...
|
||||
let ds = inc in
|
||||
traceShow ds $
|
||||
let state2 = addRows teacher ds state in
|
||||
makeCompleteConsistent teacher state2
|
||||
)
|
||||
( -- inc2 is the set of inconsistencies.
|
||||
let inc2 = inconsistency state in
|
||||
ite (isNotEmpty inc2)
|
||||
( -- If that set is non-empty, we should add new columns
|
||||
trace "Inconsistent! Adding columns:" $
|
||||
-- The extensions are in the second component
|
||||
let de = sum $ map (\((s1,s2,a),es) -> map (a:) es) inc2 in
|
||||
traceShow de $
|
||||
let state2 = addColumns teacher de state in
|
||||
makeCompleteConsistent teacher state2
|
||||
)
|
||||
( -- If both sets are empty, the table is complete and
|
||||
-- consistent, so we are done.
|
||||
trace " => Complete + Consistent :D!" $
|
||||
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 (BRow i) 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.
|
||||
useCounterExampleAngluin :: LearnableAlphabet i => Teacher i -> State i -> Set [i] -> State i
|
||||
useCounterExampleAngluin teacher state@State{..} ces =
|
||||
trace "Using ce:" $
|
||||
traceShow ces $
|
||||
let ds = sum . map (fromList . inits) $ ces in
|
||||
trace " -> Adding rows:" $
|
||||
traceShow ds $
|
||||
addRows teacher ds state
|
||||
|
||||
-- I am not quite sure whether this variant is due to Rivest & Schapire or Maler & Pnueli.
|
||||
useCounterExampleRS :: LearnableAlphabet i => Teacher i -> State i -> Set [i] -> State i
|
||||
useCounterExampleRS teacher state@State{..} ces =
|
||||
trace "Using ce:" $
|
||||
traceShow ces $
|
||||
let de = sum . map (fromList . tails) $ ces in
|
||||
trace " -> Adding columns:" $
|
||||
traceShow de $
|
||||
addColumns teacher de state
|
||||
|
||||
useCounterExample :: LearnableAlphabet i => Teacher i -> State i -> Set [i] -> 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 :: LearnableAlphabet i => Teacher i -> State i -> Automaton (BRow i) i
|
||||
loop teacher s =
|
||||
-- I put a deepseq here in order to let all traces be evaluated
|
||||
-- in a decent order. Also it will be used anyways.
|
||||
deepseq s $
|
||||
trace "##################" $
|
||||
trace "1. Making it complete and consistent" $
|
||||
let s2 = makeCompleteConsistent teacher s in
|
||||
trace "2. Constructing hypothesis" $
|
||||
let h = constructHypothesis s2 in
|
||||
traceShow h $
|
||||
trace "3. Equivalent? " $
|
||||
let eq = equivalent teacher h in
|
||||
traceShow eq $
|
||||
case eq of
|
||||
Nothing -> h
|
||||
Just ce -> do
|
||||
let s3 = useCounterExample teacher s2 ce
|
||||
loop teacher s3
|
||||
|
||||
constructEmptyState :: LearnableAlphabet i => Teacher i -> 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 :: LearnableAlphabet i => Teacher i -> Automaton (BRow i) i
|
||||
learn teacher = loop teacher s
|
||||
where s = constructEmptyState teacher
|
||||
|
||||
-- Initializes the table and runs the algorithm.
|
||||
main :: IO ()
|
||||
main = do
|
||||
let h = learn (teacherWithTarget (Examples.fifoExample 3))
|
||||
let h = learnAngluin (teacherWithTarget (Examples.fifoExample 3))
|
||||
putStrLn "Finished! Final hypothesis ="
|
||||
print h
|
||||
|
|
|
|||
132
src/NLStar.hs
132
src/NLStar.hs
|
|
@ -1,8 +1,9 @@
|
|||
{-# LANGUAGE RecordWildCards #-}
|
||||
module NLStar where
|
||||
|
||||
import Examples
|
||||
import Functions
|
||||
import AbstractLStar
|
||||
import Angluin
|
||||
import Bollig
|
||||
import ObservationTable
|
||||
import Teacher
|
||||
|
||||
|
|
@ -13,21 +14,10 @@ import Data.List (inits, tails)
|
|||
import Prelude hiding (and, curry, filter, lookup, map, not,
|
||||
sum)
|
||||
|
||||
-- So at the moment we only allow sums of the form a + b
|
||||
-- Of course we should approximate the powerset a bit better
|
||||
-- But for the main example, we know this is enough!
|
||||
-- I (Joshua) believe it is possible to give a finite-orbit
|
||||
-- approximation, but the code will not be efficient ;-).
|
||||
hackApproximate :: NominalType a => Set a -> Set (Set a)
|
||||
hackApproximate set = empty `union` map singleton set `union` pairsWith (\x y -> singleton x `union` singleton y) set set
|
||||
|
||||
rowUnion :: NominalType i => Set (BRow i) -> BRow i
|
||||
rowUnion set = Prelude.uncurry union . setTrueFalse . partition (\(_, f) -> f) $ map (\is -> (is, exists fromBool (mapFilter (\(is2, b) -> maybeIf (is `eq` is2) b) flatSet))) allIs
|
||||
where
|
||||
flatSet = sum set
|
||||
allIs = map fst flatSet
|
||||
setTrueFalse (trueSet, falseSet) = (map (setSecond True) trueSet, map (setSecond False) falseSet)
|
||||
setSecond a (x, _) = (x, a)
|
||||
{- This is not NL* from the Bollig et al paper. This is a more abstract version
|
||||
wich uses different notions for closedness and consistency.
|
||||
Joshua argues this version is closer to the categorical perspective.
|
||||
-}
|
||||
|
||||
-- lifted row functions
|
||||
rowP t = rowUnion . map (row t)
|
||||
|
|
@ -35,64 +25,28 @@ rowPa t set a = rowUnion . map (\s -> rowa t s a) $ set
|
|||
|
||||
-- We can determine its completeness with the following
|
||||
-- It returns all witnesses (of the form sa) for incompleteness
|
||||
incompletenessNonDet :: NominalType i => State i -> Set [i]
|
||||
incompletenessNonDet State{..} = filter (not . hasEqRow) ssa
|
||||
nonDetClosednessTest :: NominalType i => State i -> TestResult i
|
||||
nonDetClosednessTest State{..} = case solve (isEmpty defect) of
|
||||
Just True -> Succes
|
||||
Just False -> trace "Not closed" $ Failed defect empty
|
||||
where
|
||||
sss = map (rowP t) . hackApproximate $ ss
|
||||
-- true if the sequence sa has an equivalent row in ss
|
||||
hasEqRow = contains sss . row t
|
||||
defect = filter (not . hasEqRow) ssa
|
||||
|
||||
inconsistencyNonDet :: NominalType i => State i -> Set ((Set [i], Set [i], i), Set [i])
|
||||
inconsistencyNonDet State{..} =
|
||||
pairsWithFilter (
|
||||
\(s1, s2) a -> maybeIf (candidate1 s1 s2 a) ((s1, s2, a), discrepancy (rowPa t s1 a) (rowPa t s2 a))
|
||||
) rowPairs aa
|
||||
nonDetConsistencyTest :: NominalType i => State i -> TestResult i -- Set ((Set [i], Set [i], i), Set [i])
|
||||
nonDetConsistencyTest State{..} = case solve (isEmpty defect) of
|
||||
Just True -> Succes
|
||||
Just False -> trace "Not consistent" $ Failed empty columns
|
||||
where
|
||||
rowPairs = pairsWithFilter (\s1 s2 -> maybeIf (candidate0 s1 s2) (s1,s2)) (hackApproximate ss) (hackApproximate ss)
|
||||
candidate0 s1 s2 = s1 `neq` s2 /\ rowP t s1 `eq` rowP t s2
|
||||
candidate1 s1 s2 a = rowPa t s1 a `neq` rowPa t s2 a
|
||||
|
||||
-- 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 :: LearnableAlphabet i => Teacher i -> State i -> State i
|
||||
makeCompleteConsistentNonDet teacher state@State{..} =
|
||||
-- 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 = incompletenessNonDet state in
|
||||
ite (isNotEmpty inc)
|
||||
( -- If that set is non-empty, we should add new rows
|
||||
trace "Incomplete! Adding rows:" $
|
||||
-- These will be the new rows, ...
|
||||
let ds = inc in
|
||||
traceShow ds $
|
||||
let state2 = addRows teacher ds state in
|
||||
makeCompleteConsistentNonDet teacher state2
|
||||
)
|
||||
( -- inc2 is the set of inconsistencies.
|
||||
let inc2 = inconsistencyNonDet state in
|
||||
ite (isNotEmpty inc2)
|
||||
( -- If that set is non-empty, we should add new columns
|
||||
trace "Inconsistent! Adding columns:" $
|
||||
-- The extensions are in the second component
|
||||
let de = sum $ map (\((s1,s2,a),es) -> map (a:) es) inc2 in
|
||||
traceShow de $
|
||||
let state2 = addColumns teacher de state in
|
||||
makeCompleteConsistentNonDet teacher state2
|
||||
)
|
||||
( -- If both sets are empty, the table is complete and
|
||||
-- consistent, so we are done.
|
||||
trace " => Complete + Consistent :D!" $
|
||||
state
|
||||
)
|
||||
)
|
||||
|
||||
boolImplies :: Bool -> Bool -> Bool
|
||||
boolImplies True False = False
|
||||
boolImplies _ _ = True
|
||||
|
||||
sublang :: NominalType i => BRow i -> BRow i -> Formula
|
||||
sublang r1 r2 = forAll fromBool $ pairsWithFilter (\(i1, f1) (i2, f2) -> maybeIf (i1 `eq` i2) (f1 `boolImplies` f2)) r1 r2
|
||||
defect = pairsWithFilter (
|
||||
\(s1, s2) a -> maybeIf (candidate1 s1 s2 a) ((s1, s2, a), discrepancy (rowPa t s1 a) (rowPa t s2 a))
|
||||
) rowPairs aa
|
||||
columns = sum $ map (\((s1,s2,a),es) -> map (a:) es) defect
|
||||
|
||||
-- Given a C&C table, constructs an automaton. The states are given by 2^E (not
|
||||
-- necessarily equivariant functions)
|
||||
|
|
@ -101,49 +55,15 @@ constructHypothesisNonDet State{..} = automaton q a d i f
|
|||
where
|
||||
q = map (row t) ss
|
||||
a = aa
|
||||
d = triplesWithFilter (\s a s2 -> maybeIf (sublang (row t s2) (rowa t s a)) (row t s, a, row t s2)) ss aa ss
|
||||
d = triplesWithFilter (\s a s2 -> maybeIf (row t s2 `sublang` rowa t s a) (row t s, a, row t s2)) ss aa ss
|
||||
i = singleton $ row t []
|
||||
f = mapFilter (\s -> maybeIf (toform $ apply t (s, [])) (row t s)) ss
|
||||
toform s = forAll id . map fromBool $ s
|
||||
|
||||
-- I am not quite sure whether this variant is due to Rivest & Schapire or Maler & Pnueli.
|
||||
useCounterExampleNonDet :: LearnableAlphabet i => Teacher i -> State i -> Set [i] -> State i
|
||||
useCounterExampleNonDet teacher state@State{..} ces =
|
||||
trace "Using ce:" $
|
||||
traceShow ces $
|
||||
let de = sum . map (fromList . tails) $ ces in
|
||||
trace " -> Adding columns:" $
|
||||
traceShow de $
|
||||
addColumns teacher de state
|
||||
|
||||
-- The main loop, which results in an automaton. Will stop if the hypothesis
|
||||
-- exactly accepts the language we are learning.
|
||||
loopNonDet :: LearnableAlphabet i => Teacher i -> State i -> Automaton (BRow i) i
|
||||
loopNonDet teacher s =
|
||||
trace "##################" $
|
||||
trace "1. Making it complete and consistent" $
|
||||
let s2 = makeCompleteConsistentNonDet teacher s in
|
||||
trace "2. Constructing hypothesis" $
|
||||
let h = constructHypothesisNonDet s2 in
|
||||
traceShow h $
|
||||
trace "3. Equivalent? " $
|
||||
let eq = equivalent teacher h in
|
||||
traceShow eq $
|
||||
case eq of
|
||||
Nothing -> h
|
||||
Just ce -> do
|
||||
let s3 = useCounterExampleNonDet teacher s2 ce
|
||||
loopNonDet teacher s3
|
||||
|
||||
constructEmptyStateNonDet :: LearnableAlphabet i => Teacher i -> State i
|
||||
constructEmptyStateNonDet 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{..}
|
||||
makeCompleteNonDet :: LearnableAlphabet i => TableCompletionHandler i
|
||||
makeCompleteNonDet = makeCompleteWith [nonDetClosednessTest, nonDetConsistencyTest]
|
||||
|
||||
-- Default: use counter examples in columns, which is slightly faster
|
||||
learnNonDet :: LearnableAlphabet i => Teacher i -> Automaton (BRow i) i
|
||||
learnNonDet teacher = loopNonDet teacher s
|
||||
where s = constructEmptyStateNonDet teacher
|
||||
learnNonDet teacher = learn makeCompleteNonDet useCounterExampleMP constructHypothesisNonDet teacher initial
|
||||
where initial = constructEmptyState teacher
|
||||
|
|
|
|||
|
|
@ -7,7 +7,6 @@
|
|||
|
||||
module ObservationTable where
|
||||
|
||||
import Functions
|
||||
import NLambda hiding (fromJust)
|
||||
import Teacher
|
||||
|
||||
|
|
@ -19,6 +18,25 @@ import Prelude (Bool (..), Eq, Ord, Show (..), ($), (++), (.), un
|
|||
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
|
||||
|
||||
-- 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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue