Rewrote nominal NL* for better performance, by specialising for Booleans

bench/Bench.hs

@@ -10,6 +10,7 @@ import Gauge.Main.Options
 myConfig = defaultConfig
   { quickMode = True
   , includeFirstIter = True
+  , csvFile = Just "bench.csv"
   }
 
 main = defaultMainWith myConfig [

nominal-lstar.cabal

@@ -31,7 +31,6 @@ library
     Examples.Residual,
     Examples.RunningExample,
     Examples.Stack,
-    NLStar,
     ObservationTable,
     Teacher,
     Teachers.Teacher,

src/Angluin.hs

@@ -9,7 +9,6 @@ import Data.List (inits, tails)
 import Debug.Trace
 import NLambda
 import Prelude (Bool (..), Maybe (..), id, show, ($), (++), (.))
-import qualified Prelude hiding ()
 
 justOne :: (Contextual a, NominalType a) => Set a -> Set a
 justOne s = mapFilter id . orbit [] . element $ s

src/Bollig.hs

@@ -8,8 +8,7 @@ import Teacher
 
 import Debug.Trace
 import NLambda
-import Prelude (Bool (..), Int, Maybe (..), fst, snd, ($), (++), (.), (<=))
-import qualified Prelude hiding ()
+import Prelude (Bool (..), Int, Maybe (..), ($), (++), (.))
 
 -- Comparing two graphs of a function is inefficient in NLambda,
 -- because we do not have a map data structure. (So the only way
@@ -21,17 +20,14 @@ import qualified Prelude hiding ()
 brow :: (NominalType i) => Table i Bool -> [i] -> Set [i]
 brow t is = mapFilter (\((a,b),c) -> maybeIf (eq is a /\ fromBool c) b) t
 
-rfsaClosednessTest3 :: LearnableAlphabet i => State i -> TestResult i
-rfsaClosednessTest3 State{..} = case solve (isEmpty defect) of
+rfsaClosednessTest :: LearnableAlphabet i => Set (Set [i]) -> State i -> TestResult i
+rfsaClosednessTest primesUpp State{..} = case solve (isEmpty defect) of
     Just True  -> Succes
     Just False -> trace "Not closed" $ Failed defect empty
     Nothing    -> trace "@@@ Unsolved Formula (rfsaClosednessTest) @@@" $
                   Failed defect empty
     where
         defect = filter (\ua -> brow t ua `neq` sum (filter (`isSubsetOf` brow t ua) primesUpp)) ssa
-        primesUpp = filter (\r -> isNotEmpty r /\ r `neq` sum (filter (`isSubsetOf` r) (allRows \\ orbit [] r))) allRowsUpp
-        allRowsUpp = map (brow t) ss
-        allRows = allRowsUpp `union` map (brow t) ssa
 
 rfsaConsistencyTest :: LearnableAlphabet i => State i -> TestResult i
 rfsaConsistencyTest State{..} = case solve (isEmpty defect) of
@@ -45,22 +41,58 @@ rfsaConsistencyTest State{..} = case solve (isEmpty defect) of
 
 -- Note that we do not have the same type of states as the angluin algorithm.
 -- We have Set [i] instead of BRow i. (However, They are isomorphic.)
-constructHypothesisBollig :: NominalType i => State i -> Automaton (Set [i]) i
-constructHypothesisBollig State{..} = automaton q a d i f
+constructHypothesisBollig :: NominalType i => Set (Set [i]) -> State i -> Automaton (Set [i]) i
+constructHypothesisBollig primesUpp State{..} = automaton q aa d i f
     where
         q = primesUpp
-        a = aa
         i = filter (`isSubsetOf` brow t []) q
         f = filter (`contains` []) q
         d0 = triplesWithFilter (\s a s2 -> maybeIf (brow t s2 `isSubsetOf` brow t (s ++ [a])) (brow t s, a, brow t s2)) ss aa ss
         d = filter (\(q1, _, q2) -> q1 `member` q /\ q2 `member` q) d0
-        primesUpp = filter (\r -> isNotEmpty r /\ r `neq` sum (filter (`isSubsetOf` r) (allRows \\ orbit [] r))) allRowsUpp
-        allRowsUpp = map (brow t) ss
-        allRows = allRowsUpp `union` map (brow t) ssa
 
-makeCompleteBollig :: LearnableAlphabet i => TableCompletionHandler i
-makeCompleteBollig = makeCompleteWith [rfsaClosednessTest3, rfsaConsistencyTest]
+--makeCompleteBollig :: LearnableAlphabet i => TableCompletionHandler i
+--makeCompleteBollig = makeCompleteWith [rfsaClosednessTest, rfsaConsistencyTest]
 
 learnBollig :: LearnableAlphabet i => Int -> Int -> Teacher i -> Automaton (Set [i]) i
-learnBollig k n teacher = learn makeCompleteBollig useCounterExampleMP constructHypothesisBollig teacher initial
-    where initial = constructEmptyState k n teacher
+--learnBollig k n teacher = learn makeCompleteBollig useCounterExampleMP constructHypothesisBollig teacher initial
+--    where initial = constructEmptyState k n teacher
+
+learnBollig k n teacher = learnBolligLoop teacher (constructEmptyState k n teacher)
+
+learnBolligLoop teacher s1@State{..} =
+    let
+        allRowsUpp = map (brow t) ss
+        allRows = allRowsUpp `union` map (brow t) ssa
+        primesUpp = filter (\r -> isNotEmpty r /\ r `neq` sum (filter (`isSubsetOf` r) (allRows \\ orbit [] r))) allRowsUpp
+
+        -- No worry, these are computed lazily
+        closednessRes = rfsaClosednessTest primesUpp s1
+        consistencyRes = rfsaConsistencyTest s1
+        h = constructHypothesisBollig primesUpp s1
+    in
+        trace "1. Making it rfsa closed" $
+        case closednessRes of
+            Failed newRows _ ->
+                let state2 = simplify $ addRows teacher newRows s1 in
+                learnBolligLoop teacher state2
+            Succes ->
+                trace "1. Making it rfsa consistent" $
+                case consistencyRes of
+                    Failed _ newColumns ->
+                        let state2 = simplify $ addColumns teacher newColumns s1 in
+                        learnBolligLoop teacher state2
+                    Succes ->
+                        traceShow h $
+                        trace "3. Equivalent? " $
+                        eqloop s1 h
+                        where
+                            eqloop s2 h = case equivalent teacher h of
+                                            Nothing -> trace "Yes" h
+                                            Just ces -> trace "No" $
+                                                if isTrue . isEmpty $ realces h ces
+                                                    then eqloop s2 h
+                                                    else
+                                                        let s3 = useCounterExampleMP teacher s2 ces in
+                                                        learnBolligLoop teacher s3
+                            realces h ces = NLambda.filter (\(ce, a) -> a `neq` accepts h ce) $ membership teacher ces
+

src/NLStar.hs

@@ -1,60 +0,0 @@
-{-# language RecordWildCards #-}
-module NLStar where
-
-import AbstractLStar
-import Angluin
-import Bollig
-import ObservationTable
-import Teacher
-
-import Debug.Trace
-import NLambda
-import Prelude hiding (and, curry, filter, lookup, map, not, sum)
-
-{- This is not NL* from the Bollig et al paper. This is a very naive
-   approximation. You see, the consistency in their paper is quite weak,
-   and in fact does not determine a well defined automaton (the constructed
-   automaton does not even agree with the table of observations). They fix
-   it by adding counter examples as columns instead of rows. This way the
-   teacher will point out inconsistencies and columns are added then.
-
-   Here, I propose an algorithm which does not check consistency at all!
-   Sounds a bit crazy, but the teacher kind of takes care of that. Of course
-   I do not know whether this will terminate. But it's nice to experiment with.
-   Also I do not 'minimize' the NFA by taking only prime rows. Saves a lot of
-   checking but makes the result not minimal (whatever that would mean). It
-   is quite fast, however ;-).
-
-   THIS IS NOT USED IN THE PAPER.
--}
-
--- We can determine its completeness with the following
--- It returns all witnesses (of the form sa) for incompleteness
-
-{- Disabled, didn't work anymore, and I don't know what it does
-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
-        allRows = map (row t) ss
-        hasSum r = r `eq` rowUnion (sublangs r allRows)
-        defect = filter (not . hasSum . row t) ssa
-
-constructHypothesisNonDet :: NominalType i => State i -> Automaton (BRow i) i
-constructHypothesisNonDet State{..} = automaton q a d i f
-    where
-        q = map (row t) ss
-        a = aa
-        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 (tableAt t s []) (row t s)) ss
-
-makeCompleteNonDet :: LearnableAlphabet i => TableCompletionHandler i
-makeCompleteNonDet = makeCompleteWith [nonDetClosednessTest]
-
--- Default: use counter examples in columns, which is slightly faster
-learnNonDet :: LearnableAlphabet i => Teacher i -> Automaton (BRow i) i
-learnNonDet teacher = learn makeCompleteNonDet useCounterExampleMP constructHypothesisNonDet teacher initial
-    where initial = constructEmptyState 0 0 teacher
--}