Made NLStar simpler and 3x as fast

app/Main.hs

@@ -42,20 +42,18 @@ mainExample learnerName teacherName autName = do
             EqDFA         -> teacherWithTarget automaton
             EqNFA k       -> teacherWithTargetNonDet k automaton
             EquivalenceIO -> teacherWithTargetAndIO automaton
-    let h = case read learnerName of
-            NomLStar    -> learnAngluinRows teacher
-            NomLStarCol -> learnAngluin teacher
-            NomNLStar   -> learnBollig 0 0 teacher
-    print h
+    case read learnerName of
+            NomLStar    -> print $ learnAngluinRows teacher
+            NomLStarCol -> print $ learnAngluin teacher
+            NomNLStar   -> print $ learnBollig 0 0 teacher
 
 mainWithIO :: String -> IO ()
 mainWithIO learnerName = do
     let t = teacherWithIO atoms
-    let h = case read learnerName of
-            NomLStar    -> learnAngluinRows t
-            NomLStarCol -> learnAngluin t
-            NomNLStar   -> learnBollig 0 0 t
-    print h
+    case read learnerName of
+            NomLStar    -> print $ learnAngluinRows t
+            NomLStarCol -> print $ learnAngluin t
+            NomNLStar   -> print $ learnBollig 0 0 t
 
 main :: IO ()
 main = do

app/Main2.hs

@@ -14,11 +14,10 @@ learn :: (Read i, Contextual i, NominalType i, Show i) => Set i -> IO ()
 learn alphSet = do
     [learnerName] <- getArgs
     let t = teacherWithIO2 alphSet
-    let h = case read learnerName of
-            NomLStar    -> learnAngluinRows t
-            NomLStarCol -> learnAngluin t
-            NomNLStar   -> learnBollig 0 0 t
-    hPrint stderr h
+    case read learnerName of
+            NomLStar    -> hPrint stderr $ learnAngluinRows t
+            NomLStarCol -> hPrint stderr $ learnAngluin t
+            NomNLStar   -> hPrint stderr $ learnBollig 0 0 t
 
 main :: IO ()
 main = do

src/AbstractLStar.hs

@@ -9,7 +9,7 @@ import NLambda
 
 type TableCompletionHandler i = Teacher i -> State i -> State i
 type CounterExampleHandler i  = Teacher i -> State i -> Set [i] -> State i
-type HypothesisConstruction i = State i -> Automaton (BRow i) i
+type HypothesisConstruction i hq = State i -> Automaton hq i
 
 data TestResult i
     = Succes                     -- test succeeded, no changes required
@@ -39,13 +39,13 @@ makeCompleteWith tests teacher state0 = go tests state0
 -- Simple general learning loop: 1. make the table complete 2. construct
 -- hypothesis 3. ask teacher. Repeat until done. If the teacher is adequate
 -- termination implies correctness.
-learn :: LearnableAlphabet i
+learn :: (NominalType hq, Show hq, LearnableAlphabet i)
   => TableCompletionHandler i
   -> CounterExampleHandler i
-  -> HypothesisConstruction i
+  -> HypothesisConstruction i hq
   -> Teacher i
   -> State i
-  -> Automaton (BRow i) i
+  -> Automaton hq i
 learn makeComplete handleCounterExample constructHypothesis teacher s =
     trace "##################" $
     trace "1. Making it complete and consistent" $

src/Angluin.hs

@@ -8,7 +8,7 @@ import Teacher
 import Data.List (inits, tails)
 import Debug.Trace
 import NLambda
-import Prelude (Bool (..), Maybe (..), fst, id, show, ($), (++), (.))
+import Prelude (Bool (..), Maybe (..), id, show, ($), (++), (.))
 import qualified Prelude hiding ()
 
 justOne :: (Contextual a, NominalType a) => Set a -> Set a
@@ -95,7 +95,7 @@ consistencyTest2 State{..} = case solve (isEmpty defect) of
         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
+        columns = sum $ map (\((_,_,a),es) -> map (a:) es) defect
 
 -- Some coauthor's faster version
 consistencyTest3 :: NominalType i => State i -> TestResult i
@@ -109,4 +109,4 @@ consistencyTest3 State{..} = case solve (isEmpty defect) of
         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
+        columns = sum $ map (\((_,_,a),es) -> map (a:) es) defect

src/Bollig.hs

@@ -11,34 +11,27 @@ import NLambda
 import Prelude (Bool (..), Int, Maybe (..), fst, snd, ($), (++), (.), (<=))
 import qualified Prelude hiding ()
 
-rowUnion :: NominalType i => Set (BRow i) -> BRow i
-rowUnion set = Prelude.uncurry union . setTrueFalse . partition snd $ 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)
+-- Comparing two graphs of a function is inefficient in NLambda,
+-- because we do not have a map data structure. (So the only way
+-- is by taking a product and filtering on equal inputs.)
+-- So instead of considering a row as E -> 2, we simply take it
+-- as a subset.
+-- This does hinder generalisations to other nominal join semi-
+-- lattices than the Booleans.
+brow :: (NominalType i) => Table i Bool -> [i] -> Set [i]
+brow t is = mapFilter (\((a,b),c) -> maybeIf (eq is a /\ fromBool c) b) t
 
-boolImplies :: Bool -> Bool -> Bool
-boolImplies = (<=)
-
-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
-
-sublangs :: NominalType i => BRow i -> Set (BRow i) -> Set (BRow i)
-sublangs r = filter (`sublang` r)
-
-rfsaClosednessTest2 :: LearnableAlphabet i => State i -> TestResult i
-rfsaClosednessTest2 State{..} = case solve (isEmpty defect) of
+rfsaClosednessTest3 :: LearnableAlphabet i => State i -> TestResult i
+rfsaClosednessTest3 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 = pairsWithFilter (\u a -> maybeIf (rowa t u a `neq` rowUnion (sublangs (rowa t u a) primesUpp)) (u ++ [a])) ss aa
-        primesUpp = filter (\r -> r `neq` rowUnion (sublangs r (allRows \\ orbit [] r))) allRowsUpp
-        allRowsUpp = map (row t) ss
-        allRows = allRowsUpp `union` map (row t) ssa
+        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
@@ -47,26 +40,27 @@ rfsaConsistencyTest State{..} = case solve (isEmpty defect) of
     Nothing    -> trace "@@@ Unsolved Formula (rfsaConsistencyTest) @@@" $
                   Failed empty defect
     where
-        candidates = pairsWithFilter (\u1 u2 -> maybeIf (row t u2 `sublang` row t u1) (u1, u2)) ss ss
-        defect = triplesWithFilter (\(u1, u2) a v -> maybeIf (not (tableAt t (u1 ++ [a]) v) /\ tableAt t (u2++[a]) v) (a:v)) candidates aa ee
+        candidates = pairsWithFilter (\u1 u2 -> maybeIf (brow t u2 `isSubsetOf` brow t u1) (u1, u2)) ss ss
+        defect = triplesWithFilter (\(u1, u2) a v -> maybeIf (not (tableAt t (u1 ++ [a]) v) /\ tableAt t (u2 ++ [a]) v) (a:v)) candidates aa ee
 
-constructHypothesisBollig :: NominalType i => State i -> Automaton (BRow i) i
+-- 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
     where
         q = primesUpp
         a = aa
-        i = filter (\r -> r `sublang` row t []) q
-        f = filter (\r -> singleton True `eq` mapFilter (\(i,b) -> maybeIf (i `eq` []) b) r) q
-        d0 = triplesWithFilter (\s a s2 -> maybeIf (row t s2 `sublang` rowa t s a) (row t s, a, row t s2)) ss aa ss
+        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 -> nonEmpty r /\ r `neq` rowUnion (sublangs r (allRows \\ orbit [] r))) allRowsUpp
-        nonEmpty = isNotEmpty . filter (fromBool . Prelude.snd)
-        allRowsUpp = map (row t) ss
-        allRows = allRowsUpp `union` map (row t) 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
 
 makeCompleteBollig :: LearnableAlphabet i => TableCompletionHandler i
-makeCompleteBollig = makeCompleteWith [rfsaClosednessTest2, rfsaConsistencyTest]
+makeCompleteBollig = makeCompleteWith [rfsaClosednessTest3, rfsaConsistencyTest]
 
-learnBollig :: LearnableAlphabet i => Int -> Int -> Teacher i -> Automaton (BRow i) i
+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

src/NLStar.hs

@@ -30,6 +30,8 @@ import Prelude hiding (and, curry, filter, lookup, map, not, sum)
 
 -- 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
@@ -55,3 +57,4 @@ makeCompleteNonDet = makeCompleteWith [nonDetClosednessTest]
 learnNonDet :: LearnableAlphabet i => Teacher i -> Automaton (BRow i) i
 learnNonDet teacher = learn makeCompleteNonDet useCounterExampleMP constructHypothesisNonDet teacher initial
     where initial = constructEmptyState 0 0 teacher
+-}