Also simplifies the L* algorithm, which is now a bit faster

app/Main.hs

@@ -2,7 +2,6 @@
 import Angluin
 import Bollig
 import Examples
-import ObservationTable (LearnableAlphabet)
 import Teacher
 
 import NLambda hiding (automaton)
@@ -25,7 +24,7 @@ data Aut = Fifo Int | Stack Int | Running Int | NFA1 | Bollig Int | NonResidual
   deriving (Show, Read)
 
 -- existential wrapper
-data A = forall q i . (LearnableAlphabet i, Read i, NominalType q, Show q) => A (Automaton q i)
+data A = forall q i . (NominalType i, Contextual i, Show i, Read i, NominalType q, Show q) => A (Automaton q i)
 
 {- HLINT ignore "Redundant $" -}
 mainExample :: String -> String -> String -> IO ()

nominal-lstar.cabal

@@ -30,7 +30,6 @@ library
     Examples.Residual,
     Examples.RunningExample,
     Examples.Stack,
-    ObservationTable,
     ObservationTableClass,
     SimpleObservationTable,
     Teacher,

src/AbstractLStar.hs

@@ -1,79 +1,7 @@
-{-# language RecordWildCards #-}
 module AbstractLStar where
 
-import ObservationTable
-import Teacher
-
-import Debug.Trace
 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 hq = State i -> Automaton hq i
-
 data TestResult i
     = Succes                     -- test succeeded, no changes required
     | Failed (Set [i]) (Set [i]) -- test failed, change: add rows + columns
-
--- Simple loop which performs tests such as closedness and consistency
--- on the table and makes changes if needed. Will (hopefully) reach a
--- fixed point, i.e. a complete table.
-makeCompleteWith :: LearnableAlphabet i
-  => [State i -> TestResult i]
-  -> Teacher i -> State i -> State i
-makeCompleteWith tests teacher state0 = go tests state0
-    where
-        -- All tests succeeded, then the state is stable
-        go [] state = state
-        -- We still have tests to perform
-        go (t:ts) state = case t state of
-            -- If the test succeeded, we continue with the next one
-            Succes -> go ts state
-            -- Otherwise we add the changes
-            Failed newRows newColumns ->
-                let state2 = simplify $ addRows teacher newRows state in
-                let state3 = simplify $ addColumns teacher newColumns state2 in
-                -- restart the whole business
-                makeCompleteWith tests teacher state3
-
--- 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 :: (NominalType hq, Show hq, LearnableAlphabet i)
-  => TableCompletionHandler i
-  -> CounterExampleHandler i
-  -> HypothesisConstruction i hq
-  -> Teacher i
-  -> State i
-  -> Automaton hq i
-learn makeComplete handleCounterExample constructHypothesis teacher s =
-    trace "##################" $
-    trace "1. Making it complete and consistent" $
-    let s2 = makeComplete teacher s in
-    trace "2. Constructing hypothesis" $
-    let h = constructHypothesis s2 in
-    traceShow h $
-    trace "3. Equivalent? " $
-    eqloop s2 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 = handleCounterExample teacher s2 ces in
-                                      learn makeComplete handleCounterExample constructHypothesis teacher s3
-        realces h ces = NLambda.filter (\(ce, a) -> a `neq` accepts h ce) $ membership teacher ces
-
--- Initialise with the trivial table
--- We allow to initialise with all words of length <= k,n for rows and columns
--- Normally one should take k = n = 0
-constructEmptyState :: LearnableAlphabet i => Int -> Int -> Teacher i -> State i
-constructEmptyState k n teacher =
-    let aa = Teacher.alphabet teacher in
-    let ss = replicateSetUntil k aa in
-    let ssa = pairsWith (\s a -> s ++ [a]) ss aa in
-    let ee = replicateSetUntil n aa in
-    let t = fillTable teacher (ss `union` ssa) ee in
-    State{..}

src/Angluin.hs

@@ -1,112 +1,107 @@
-{-# language RecordWildCards #-}
+{-# language FlexibleContexts #-}
+{-# language PartialTypeSignatures #-}
+{-# language TypeFamilies #-}
+{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
 module Angluin where
 
 import AbstractLStar
-import ObservationTable
+import ObservationTableClass
+import qualified BooleanObservationTable as OT
 import Teacher
 
 import Data.List (inits, tails)
 import Debug.Trace
-import NLambda
+import NLambda hiding (alphabet)
-import Prelude (Bool (..), Maybe (..), id, show, ($), (++), (.))
+import Prelude (Bool (..), Maybe (..), error, show, ($), (++), (.))
 
--- This was actually a pessimisation (often), also it sometimes crashes.
--- So I changed it to a no-op.
-justOne :: (Contextual a, NominalType a) => Set a -> Set a
-justOne = id -- mapFilter id . orbit [] . element
 
--- We can determine its completeness with the following
+-- This returns all witnesses (of the form sa) for non-closedness
--- It returns all witnesses (of the form sa) for incompleteness
+closednessTest :: (NominalType i, _) => table -> TestResult i
-closednessTest :: LearnableAlphabet i => State i -> TestResult i
+closednessTest t = case solve (isEmpty defect) of
-closednessTest State{..} = case solve (isEmpty defect) of
     Just True  -> Succes
-    Just False -> trace "Not closed" $ Failed (justOne defect) empty
+    Just False -> trace "Not closed" $ Failed defect empty
+    Nothing    -> let err = error "@@@ Unsolvable (closednessTest) @@@" in Failed err err
     where
-        sss = map (row t) ss                 -- all the rows
+        allRows = map (row t) (rows t)
-        hasEqRow = contains sss . row t      -- has equivalent upper row
+        hasEqRow = contains allRows . row t
-        defect = filter (not . hasEqRow) ssa -- all rows without equivalent guy
+        defect = filter (not . hasEqRow) (rowsExt t)
 
 -- We look for inconsistencies and return columns witnessing it
-consistencyTestDirect :: LearnableAlphabet i => State i -> TestResult i
+consistencyTestDirect :: (NominalType i, _) => table -> TestResult i
-consistencyTestDirect State{..} = case solve (isEmpty defect) of
+consistencyTestDirect t = case solve (isEmpty defect) of
     Just True  -> Succes
-    Just False -> trace "Not consistent" $ Failed empty (justOne defect)
+    Just False -> trace "Not consistent" $ Failed empty defect
+    Nothing    -> let err = error "@@@ Unsolvable (consistencyTestDirect) @@@" in Failed err err
     where
-        ssRows = map (\u -> (u, row t u)) ss
+        ssRows = map (\u -> (u, row t u)) (rows t)
         candidates = pairsWithFilter (\(u1,r1) (u2,r2) -> maybeIf (u1 `neq` u2 /\ r1 `eq` r2) (u1, u2)) ssRows ssRows
-        defect = triplesWithFilter (\(u1, u2) a v -> maybeIf (tableAt t (u1 ++ [a]) v `diff` tableAt t (u2 ++ [a]) v) (a:v)) candidates aa ee
+        defect = triplesWithFilter (\(u1, u2) a v -> maybeIf (tableAt t (u1 ++ [a]) v `neq` tableAt t (u2 ++ [a]) v) (a:v)) candidates (alph t) (cols t)
-        diff a b = not (a `iff` b)
-
 
 -- Given a C&C table, constructs an automaton. The states are given by 2^E (not
 -- necessarily equivariant functions)
-constructHypothesis :: LearnableAlphabet i => State i -> Automaton (BRow i) i
+constructHypothesis :: (NominalType i, _) => table -> Automaton (Row table) i
-constructHypothesis State{..} = simplify $ automaton q aa d i f
+constructHypothesis t = simplify $ automaton q (alph t) d i f
     where
-        q = map (row t) ss
+        q = map (row t) (rows t)
-        d = pairsWith (\s a -> (row t s, a, rowa t s a)) ss aa
+        d = pairsWith (\s a -> (row t s, a, row t (s ++ [a]))) (rows t) (alph t)
-        i = singleton $ row t []
+        i = singleton (rowEps t)
-        f = mapFilter (\s -> maybeIf (toform $ apply t (s, [])) (row t s)) ss
+        f = filter (`contains` []) q
-        toform = forAll id . map fromBool
 
 -- Extends the table with all prefixes of a set of counter examples.
-useCounterExampleAngluin :: LearnableAlphabet i => Teacher i -> State i -> Set [i] -> State i
+useCounterExampleAngluin :: (NominalType i, _) => Teacher i -> Set [i] -> table -> table
-useCounterExampleAngluin teacher state@State{..} ces =
+useCounterExampleAngluin teacher ces t =
-    trace ("Using ce: " ++ show ces) $
+    let newRows = sum . map (fromList . inits) $ ces
-    let ds = sum . map (fromList . inits) $ ces in
+        newRowsRed = newRows \\ rows t
-    addRows teacher ds state
+     in addRows (mqToBool teacher) newRowsRed t
 
--- This is the variant by Maler and Pnueli
+-- This is the variant by Maler and Pnueli: Adds all suffixes as columns
-useCounterExampleMP :: LearnableAlphabet i => Teacher i -> State i -> Set [i] -> State i
+useCounterExampleMP :: (NominalType i, _) => Teacher i -> Set [i] -> table -> table
-useCounterExampleMP teacher state@State{..} ces =
+useCounterExampleMP teacher ces t =
-    trace ("Using ce: " ++ show ces) $
+    let newColumns = sum . map (fromList . tails) $ ces
-    let de = sum . map (fromList . tails) $ ces in
+        newColumnsRed = newColumns \\ cols t
-    addColumns teacher de state
+     in addColumns (mqToBool teacher) newColumnsRed t
-
--- Putting the above together in a learning algorithm
-makeCompleteAngluin :: LearnableAlphabet i => TableCompletionHandler i
-makeCompleteAngluin = makeCompleteWith [closednessTest, consistencyTestDirect]
 
 -- Default: use counter examples in columns, which is slightly faster
-learnAngluin :: LearnableAlphabet i => Teacher i -> Automaton (BRow i) i
+learnAngluin :: (NominalType i, _) => Teacher i -> Automaton _ i
-learnAngluin teacher = learn makeCompleteAngluin useCounterExampleMP constructHypothesis teacher initial
+learnAngluin teacher = learnLoop useCounterExampleMP teacher (OT.initialBTable (mqToBool teacher) (alphabet teacher))
-    where initial = constructEmptyState 0 0 teacher
 
 -- The "classical" version, where counter examples are added as rows
-learnAngluinRows :: LearnableAlphabet i => Teacher i -> Automaton (BRow i) i
+learnAngluinRows :: (NominalType i, _) => Teacher i -> Automaton _ i
-learnAngluinRows teacher = learn makeCompleteAngluin useCounterExampleAngluin constructHypothesis teacher initial
+learnAngluinRows teacher = learnLoop useCounterExampleAngluin teacher (OT.initialBTable (mqToBool teacher) (alphabet teacher))
-    where initial = constructEmptyState 0 0 teacher
 
-
+learnLoop :: (NominalType i, ObservationTable table i Bool, _) => _ -> Teacher i -> table -> Automaton (Row table) i
--- Below are some variations of the above functions with different
+learnLoop cexHandler teacher t =
--- performance characteristics.
+    let
-
+        -- No worry, these are computed lazily
--- Some coauthor's slower version
+        closednessRes = closednessTest t
-consistencyTest2 :: NominalType i => State i -> TestResult i
+        consistencyRes = consistencyTestDirect t
-consistencyTest2 State{..} = case solve (isEmpty defect) of
+        hyp = constructHypothesis t
-    Just True  -> Succes
+    in
-    Just False -> trace "Not consistent" $ Failed empty columns
+        trace "1. Making it closed" $
+        case closednessRes of
+            Failed newRows _ ->
+                let state2 = addRows (mqToBool teacher) newRows t in
+                trace ("newrows = " ++ show newRows) $
+                learnLoop cexHandler teacher state2
+            Succes ->
+                trace "2. Making it consistent" $
+                case consistencyRes of
+                    Failed _ newColumns ->
+                        let state2 = addColumns (mqToBool teacher) newColumns t in
+                        trace ("newcols = " ++ show newColumns) $
+                        learnLoop cexHandler teacher state2
+                    Succes ->
+                        traceShow hyp $
+                        trace "3. Equivalent? " $
+                        eqloop t hyp
                         where
-        -- true for equal rows, but unequal extensions
+                            eqloop s2 h = case equivalent teacher h of
-        -- we can safely skip equal sequences
+                                            Nothing -> trace "Yes" h
-        candidate s1 s2 a = s1 `neq` s2
+                                            Just ces -> trace "No" $
-                            /\ row t s1 `eq` row t s2
+                                                if isTrue . isEmpty $ realces h ces
-                            /\ rowa t s1 a `neq` rowa t s2 a
+                                                    then eqloop s2 h
-        defect = triplesWithFilter (
+                                                    else
-                     \s1 s2 a -> maybeIf (candidate s1 s2 a) ((s1, s2, a), discrepancy (rowa t s1 a) (rowa t s2 a))
+                                                        let s3 = cexHandler teacher ces s2 in
-                 ) ss ss aa
+                                                        trace ("Using ce: " ++ show ces) $
-        columns = sum $ map (\((_,_,a),es) -> map (a:) es) defect
+                                                        learnLoop cexHandler teacher s3
-
+                            realces h ces = NLambda.filter (\(ce, a) -> a `neq` accepts h ce) $ membership teacher ces
--- Some coauthor's faster version
-consistencyTest3 :: NominalType i => State i -> TestResult i
-consistencyTest3 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 (\((_,_,a),es) -> map (a:) es) defect

src/Bollig.hs

@@ -13,7 +13,7 @@ import Teacher
 import Data.List (tails)
 import Debug.Trace (trace, traceShow)
 import NLambda hiding (alphabet)
-import Prelude (Bool (..), Int, Maybe (..), Show (..), snd, ($), (++), (.))
+import Prelude (Bool (..), Int, Maybe (..), Show (..), ($), (++), (.))
 
 -- Comparing two graphs of a function is inefficient in NLambda,
 -- because we do not have a map data structure. (So the only way
@@ -23,17 +23,6 @@ import Prelude (Bool (..), Int, Maybe (..), Show (..), snd, ($), (++), (.))
 -- This does hinder generalisations to other nominal join semi-
 -- lattices than the Booleans.
 
--- The teacher interface is slightly inconvenient
--- But this is for a good reason. The type [i] -> o
--- doesn't work well in nlambda
-mqToBool :: NominalType i => Teacher i -> MQ i Bool
-mqToBool teacher words = answer
-    where
-        realQ = membership teacher words
-        (inw, outw) = partition snd realQ
-        answer = map (setB True) inw `union` map (setB False) outw
-        setB b (w, _) = (w, b)
-
 rfsaClosednessTest :: (NominalType i, _) => Set (Row table) -> table -> TestResult i
 rfsaClosednessTest primesUpp t = case solve (isEmpty defect) of
     Just True  -> Succes
@@ -72,13 +61,13 @@ addCounterExample mq ces t =
         newColumnsRed = newColumns \\ cols t
      in addColumns mq newColumnsRed t
 
--- Slow version
+learnBollig :: (NominalType i, _) => Int -> Int -> Teacher i -> Automaton _ i
-learnBolligOld :: (NominalType i, _) => Int -> Int -> Teacher i -> Automaton (Row (SOT.BTable i)) i
-learnBolligOld k n teacher = learnBolligLoop teacher (SOT.initialBTableSize (mqToBool teacher) (alphabet teacher) k n)
-
-learnBollig :: (NominalType i, _) => Int -> Int -> Teacher i -> Automaton (Row (BOT.Table i)) i
 learnBollig k n teacher = learnBolligLoop teacher (BOT.initialBTableSize (mqToBool teacher) (alphabet teacher) k n)
 
+-- Slow version
+learnBolligOld :: (NominalType i, _) => Int -> Int -> Teacher i -> Automaton _ i
+learnBolligOld k n teacher = learnBolligLoop teacher (SOT.initialBTableSize (mqToBool teacher) (alphabet teacher) k n)
+
 learnBolligLoop :: (NominalType i, _) => Teacher i -> table -> Automaton (Row table) i
 learnBolligLoop teacher t =
     let

src/ObservationTable.hs

@@ -1,109 +0,0 @@
-{-# language ConstraintKinds #-}
-{-# language DeriveAnyClass #-}
-{-# language DeriveGeneric #-}
-{-# language FlexibleContexts #-}
-{-# language FlexibleInstances #-}
-{-# language RecordWildCards #-}
-
-module ObservationTable where
-
-import NLambda hiding (fromJust)
-import Teacher
-
-import Data.Maybe (fromJust)
-import Debug.Trace (trace)
-import GHC.Generics (Generic)
-import Prelude (Bool (..), Eq, Ord, Show (..), id, uncurry, ($), (++), (.))
-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
-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
-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 = (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
-row t is = mapFilter (\((a,b),c) -> maybeIf (eq is a) (b,c)) t
-
--- `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])
-
-tableAt :: NominalType i => Table i Bool -> [i] -> [i] -> Formula
-tableAt t s e = singleton True `eq` mapFilter (\((a,b),c) -> maybeIf (s `eq` a /\ b `eq` e) c) t
-
--- Teacher is restricted to Bools at the moment
-type BTable i = Table i Bool
-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 :: LearnableAlphabet i => Teacher i -> Set [i] -> Set [i] -> BTable i
-fillTable teacher sssa ee = Prelude.uncurry union . map2 (map slv) . map2 simplify . partition (\(_, _, f) -> f) $ base
-    where
-        base0 = pairsWith (++) sssa ee
-        base1 = membership teacher base0
-        base1b s e = forAll id $ mapFilter (\(i,f) -> maybeIf (i `eq` (s++e)) f)  base1
-        base = pairsWith (\s e -> (s, e, base1b s e)) sssa ee
-        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)
-data State i = State
-    { t   :: BTable i -- 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, NominalType, Conditional, Contextual)
-
--- Precondition: the set together with the current rows is prefix closed
-addRows :: LearnableAlphabet i => Teacher i -> Set [i] -> State i -> State i
-addRows teacher ds0 state@State{..} =
-    trace ("add rows: " ++ show ds) $
-    state {t = t `union` dt, ss = ss `union` ds, ssa = ssa `union` dsa}
-    where
-        -- first remove redundancy
-        ds = ds0 \\ ss
-        -- extensions of new rows
-        dsa = pairsWith (\s a -> s ++ [a]) ds aa
-        -- For the new rows, we fill the table
-        -- note that `ds ee` is already filled
-        dt = fillTable teacher dsa ee
-
-addColumns :: LearnableAlphabet i => Teacher i -> Set [i] -> State i -> State i
-addColumns teacher de0 state@State{..} =
-    trace ("add columns: " ++ show de) $
-    state {t = t `union` dt, ee = ee `union` de}
-    where
-        -- first remove redundancy
-        de = de0 \\ ee
-        -- Fill that part of the table
-        dt = fillTable teacher (ss `union` ssa) de

src/Teacher.hs

@@ -3,6 +3,7 @@
 
 module Teacher
     ( module Teachers.Teacher
+    , mqToBool
     , teacherWithTarget
     , teacherWithTargetNonDet
     , teacherWithIO
@@ -16,6 +17,20 @@ import Teachers.Whitebox
 
 import NLambda hiding (alphabet)
 import qualified NLambda (alphabet)
+import Prelude hiding (map)
+
+
+-- The teacher interface is slightly inconvenient
+-- But this is for a good reason. The type [i] -> o
+-- doesn't work well in nlambda
+mqToBool :: NominalType i => Teacher i -> Set [i] -> Set ([i], Bool)
+mqToBool teacher qs = answer
+    where
+        realQ = membership teacher qs
+        (inw, outw) = partition snd realQ
+        answer = map (setB True) inw `union` map (setB False) outw
+        setB b (w, _) = (w, b)
+
 
 -- We provide three ways to construct teachers:
 -- 1. Fully automatic