More docs, cleaned up product module. Teacher now takes cmdline args

README.md

@@ -114,14 +114,14 @@ values, that can be much faster.
 
 ## Changelog
 
-version 0.4 (2024-11-11):
+version 0.4 (2024-11-25):
 * Changed from rational number to integers (for performance).
 * Cleaned up module structure and API.
-* Started writing some haddock.
+* Started writing some haddock documentation.
 
 version 0.3.1.0 (2024-11-06):
-* More types of products
+* More types of products.
-* Stuff to do permutations (not only monotone ones)
+* Stuff to do permutations (not only monotone ones).
 * New LStar variant, which can learn equivariant (wrt permutations) languages
   with fewer queries. But it is slower.
 

app/LStar.hs

@@ -21,6 +21,16 @@ type Rows a    = OrbitList (Word a)
 type Columns a = OrbitList (Word a)
 type Table a   = EquivariantMap (Word a) Bool
 
+-- We can compute the support of a row (content) as follows. But I do not know
+-- yet how to use this for L*. It sould be possible to optimise, if we know
+-- the exact support (at the time). The support here is the "memorable values".
+-- supportOfRow :: _ => Word a -> Columns a -> Table a -> Support
+-- supportOfRow s suffs table =
+--   let y1 = filter (\(s1, s2) -> equalRows s1 s2 suffs table) (product (singleOrbit s) (singleOrbit s))
+--       y2 = map (\(a1, a2) -> (a1, Support.intersect (support a1) (support a2))) y1
+--       m0 = Map.fromListWith (\s1 s2 -> (Support.intersect s1 s2)) . toList $ y2
+--    in m0 ! s
+
 
 -- Utility functions
 exists f = not . null . filter f

app/LStarPerm.hs

@@ -31,10 +31,8 @@ import System.IO (hFlush, stdout)
 -- away in the PermEquivariantMap data structure, so that the learning
 -- algorithm is almost identical to the one in LStar.hs.
 --
--- Some of the performance is regained, by using another product (now still
+-- Performance can be improved by using more sophisticated products. But I
--- "testProduct"). I am not 100% sure this is the correct way of doing it.
+-- do not know which one to choose (which ones are corect).
--- It seems to work on the examples I tried. And I do think that something
--- along these lines potentially works.
 --
 -- Another way forway would be to use the `Permuted` monad, also in the
 -- automaton type. But that requires more thinking.
@@ -82,11 +80,11 @@ equalRows t0 s0 suffs table =
   -- I am not convinced this is right: the permutations applied here should
   -- be the same I think. As it is currently stated the permutations to s and t
   -- may be different.
-  forAll (\((t, s), e) -> lookupP (s ++ e) table == lookupP (t ++ e) table) $ testProduct (singleOrbit (t0, s0)) suffs
+  forAll (\((t, s), e) -> lookupP (s ++ e) table == lookupP (t ++ e) table) $ product (singleOrbit (t0, s0)) suffs
 
 closed :: _ => Word a -> Rows a -> Columns a -> Table a -> Bool
 closed t prefs suffs table =
-  exists (\(t, s) -> equalRows t s suffs table) (leftProduct (singleOrbit t) prefs)
+  exists (\(t, s) -> equalRows t s suffs table) (product (singleOrbit t) prefs)
 
 nonClosedness :: _ => Rows a -> Rows a -> Columns a -> Table a -> Rows a
 nonClosedness prefs prefsExt suffs table =
@@ -96,8 +94,8 @@ inconsistencies :: _ => Rows a -> Columns a -> Table a -> OrbitList a -> OrbitLi
 inconsistencies prefs suffs table alph =
   filter (\((s, t), (a, e)) -> lookupP (s ++ (a:e)) table /= lookupP (t ++ (a:e)) table) candidatesExt
   where
-    candidates = filter (\(s, t) -> s < t && equalRows s t suffs table) (testProduct prefs prefs)
+    candidates = filter (\(s, t) -> s < t && equalRows s t suffs table) (product prefs prefs)
-    candidatesExt = testProduct candidates (product alph suffs)
+    candidatesExt = product candidates (product alph suffs)
 
 
 -- Main state of the L* algorithm

app/Teacher.hs

@@ -11,17 +11,29 @@ import ExampleAutomata
 import IO
 import Nominal (Atom)
 import OrbitList qualified
+import System.Environment (getArgs)
 
-data Example
+-- The main function reads a command line argument, specifying the model. It
+-- defaults to a certain model, so you can leave it out. The models enumerated
+-- in 'ModelDescription' are supported.
+--
+-- (Equivalence queries are currently not implemented well, see commens below.)
+
+data ModelDescription
   = Fifo Int
   | DoubleWord Int
+  deriving (Show, Read)
 
 main :: IO ()
-main =
+main = do
-  let ex = DoubleWord 2
+  ls <- getArgs
-   in case ex of
+  let model = case ls of
-        Fifo n -> teach "FIFO" (fifoFun n) (fifoCex n)
+        [x] -> read x
-        DoubleWord n -> teach "ATOMS" (doubleFun n) (doubleCex n)
+        _ -> Fifo 2
+  hPutStrLn stderr $ "Teacher behaviour: " <> show model
+  case model of
+    Fifo n -> teach "FIFO" (fifoFun n) (fifoCex n)
+    DoubleWord n -> teach "ATOMS" (doubleFun n) (doubleCex n)
 
 teach :: (ToStr a, FromStr a, Show a) => String -> ([a] -> Bool) -> [[a]] -> IO ()
 teach alphStr fun cexes = do
@@ -55,7 +67,6 @@ teach alphStr fun cexes = do
       modifyIORef countMQ succ
       n <- readIORef countMQ
       log $ "MQ " <> show n <> ": " <> str <> " -> " <> show acc -- <> " (parsed as " <> show word <> ")"
-
     handleEQ str = do
       modifyIORef countEQ succ
       n <- readIORef countEQ

run-lstar-perm.sh

@@ -22,7 +22,7 @@ teacher=$(cabal list-bin ons-hs-teacher)
 mkfifo $queryfifo $answerfifo
 
 # run the teacher in the background
-$teacher < $queryfifo > $answerfifo &
+$teacher "$@" < $queryfifo > $answerfifo &
 
 # run the learning algorithm, measuring its time
 time $lstar > $queryfifo < $answerfifo

run-lstar.sh

@@ -22,7 +22,7 @@ teacher=$(cabal list-bin ons-hs-teacher)
 mkfifo $queryfifo $answerfifo
 
 # run the teacher in the background
-$teacher < $queryfifo > $answerfifo &
+$teacher "$@" < $queryfifo > $answerfifo &
 
 # run the learning algorithm, measuring its time
 time $lstar > $queryfifo < $answerfifo

src/Nominal.hs

@@ -23,7 +23,6 @@ import Data.Proxy
 
 import Nominal.Atom
 import Nominal.Class
-import Nominal.Products
 import Nominal.Support
 
 -- | We can construct a "default" element from an orbit. In this case, the

src/Nominal/Products.hs

@@ -6,105 +6,126 @@ import Data.Proxy
 
 import Nominal.Class
 
+-- * Enumeration of product types
+
+-- $Products
+-- This module exports functions to enumerate all orbits in a product. You
+-- would typically not use this module directly, instead you can use the
+-- @product@ functions from the data structures, such as "OrbitList" or
+-- "EquivariantSet".
+--
+-- Note that the order in which the orbits are enumerated often makes a
+-- difference in performance. Currently, orbits with smaller supports are
+-- enumerated first. There is now way to customise this order.
+
+-- | Enumerates all orbits in the cartesian product
+-- \( A \times B \)
+product :: (Nominal a, Nominal b) => Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a, b)]
+product = productG prodStrings
+
+-- | Enumerates all orbits in the separated product:
+-- \( A * B = \{ (a, b) \in A \times B \mid supp(a) \cap supp(b) = \emptyset \} \)
+separatedProduct :: (Nominal a, Nominal b) => Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a, b)]
+separatedProduct = productG sepProdStrings
+
+-- | Enumerates all orbits in the (what I call) "left product"
+-- \( A ⫂ B = \{ (a, b) \in A \times B \mid supp(a) \supseteq supp(b) \} \)
+leftProduct :: (Nominal a, Nominal b) => Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a, b)]
+leftProduct = productG lsupprProdStrings
+
+-- | Enumerates all orbits in the "right product"
+-- \( A ⫁ B = \{ (a, b) \in A \times B \mid supp(a) \subseteq supp(b) \} \)
+rightProduct :: (Nominal a, Nominal b) => Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a, b)]
+rightProduct = productG rsupplProdStrings
+
+-- | Strictly increasing product
+-- \( \{ (a,b) \mid \text{all elements in } a < \text{all elements in } b \} \)
+increasingProduct :: (Nominal a, Nominal b) => Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a, b)]
+increasingProduct = productG incrSepProdStrings
+
+-- | Strictly decreasing product
+-- \( \{ (a,b) \mid \text{all elements in } a > \text{all elements in } b \} \)
+decreasingProduct :: (Nominal a, Nominal b) => Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a, b)]
+decreasingProduct = productG decrSepProdStrings
+
+-- * Helper functions
+
+-- | General combinator, which takes a way to produces "product strings"
+-- depending on the size of the support, and then makes the corresponding
+-- orbits.
+productG :: (Nominal a, Nominal b) => (Int -> Int -> [[Ordering]]) -> Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a, b)]
+productG strs pa pb oa ob = OrbPair (OrbRec oa) (OrbRec ob) <$> strs (index pa oa) (index pb ob)
+
+-- * Low-level enumeration of product types
+
 -- Enumerates strings to compute all possible combinations. Here `LT` means the
 -- "current" element goes to the left, `EQ` goes to both, and `GT` goes to the
 -- right. The elements are processed from small to large.
 prodStrings :: Alternative f => Int -> Int -> f [Ordering]
-prodStrings = memo2 gen where
+prodStrings = memo2 gen
+ where
   gen 0 0 = pure []
   gen n 0 = pure $ replicate n LT
   gen 0 n = pure $ replicate n GT
-  gen 1 1 = pure [LT, GT] <|> pure [EQ] <|> pure [GT, LT]
+  gen 1 1 = pure [EQ] <|> pure [LT, GT] <|> pure [GT, LT]
-  gen n m = (LT :) <$> prodStrings (n-1) m
+  gen n m =
-        <|> (EQ :) <$> prodStrings (n-1) (m-1)
+    (EQ :) <$> prodStrings (n - 1) (m - 1)
-        <|> (GT :) <$> prodStrings n (m-1)
+      <|> (LT :) <$> prodStrings (n - 1) m
+      <|> (GT :) <$> prodStrings n (m - 1)
 
 -- Only produces the combinations where the supports are disjoint
 sepProdStrings :: Alternative f => Int -> Int -> f [Ordering]
-sepProdStrings = memo2 gen where
+sepProdStrings = memo2 gen
+ where
   gen 0 0 = pure []
   gen n 0 = pure $ replicate n LT
   gen 0 n = pure $ replicate n GT
   gen 1 1 = pure [LT, GT] <|> pure [GT, LT]
-  gen n m = (LT :) <$> sepProdStrings (n-1) m
+  gen n m =
-        <|> (GT :) <$> sepProdStrings n (m-1)
+    (LT :) <$> sepProdStrings (n - 1) m
+      <|> (GT :) <$> sepProdStrings n (m - 1)
 
 -- Combinations where the left element supports the right element
 lsupprProdStrings :: Alternative f => Int -> Int -> f [Ordering]
-lsupprProdStrings = memo2 gen where
+lsupprProdStrings = memo2 gen
+ where
   gen n 0 = pure $ replicate n LT
   gen 1 1 = pure [EQ]
   gen n m
-    | n < m     = empty
+    | n < m = empty
-    | otherwise = (LT :) <$> lsupprProdStrings (n-1) m
+    | otherwise =
-              <|> (EQ :) <$> lsupprProdStrings (n-1) (m-1)
+        (EQ :) <$> lsupprProdStrings (n - 1) (m - 1)
+          <|> (LT :) <$> lsupprProdStrings (n - 1) m
 
 -- Combinations where the right element supports the left element
 rsupplProdStrings :: Alternative f => Int -> Int -> f [Ordering]
-rsupplProdStrings = memo2 gen where
+rsupplProdStrings = memo2 gen
+ where
   gen 0 n = pure $ replicate n GT
   gen 1 1 = pure [EQ]
   gen n m
-    | m < n     = empty
+    | m < n = empty
-    | otherwise = (EQ :) <$> rsupplProdStrings (n-1) (m-1)
+    | otherwise =
-              <|> (GT :) <$> rsupplProdStrings n (m-1)
+        (EQ :) <$> rsupplProdStrings (n - 1) (m - 1)
+          <|> (GT :) <$> rsupplProdStrings n (m - 1)
 
 -- The right support is strictly greater (hence separated) from the left
 incrSepProdStrings :: Alternative f => Int -> Int -> f [Ordering]
-incrSepProdStrings = memo2 gen where
+incrSepProdStrings = memo2 gen
+ where
   gen n m = pure $ replicate n LT <|> replicate m GT
 
 -- The right support is strictly smaller (hence separated) from the left
 decrSepProdStrings :: Alternative f => Int -> Int -> f [Ordering]
-decrSepProdStrings = memo2 gen where
+decrSepProdStrings = memo2 gen
+ where
   gen n m = pure $ replicate m GT <|> replicate n LT
 
-testProdStrings :: Alternative f => Int -> Int -> f [Ordering]
-testProdStrings = mgen (0 :: Int) where
-  mgen = memo3 gen
-  gen _ n 0 = pure $ replicate n LT
-  gen _ 0 n = pure $ replicate n GT
-  gen 0 n m = (LT :) <$> mgen 1 (n-1) m
-          <|> (EQ :) <$> mgen 0 (n-1) (m-1)
-  gen k n m = (LT :) <$> mgen (k+1) (n-1) m
-          <|> (EQ :) <$> mgen k (n-1) (m-1)
-          <|> (GT :) <$> mgen (k-1) n (m-1)
-
-
--- General combinator
-productG :: (Nominal a, Nominal b) => (Int -> Int -> [[Ordering]]) -> Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a, b)]
-productG strs pa pb oa ob = OrbPair (OrbRec oa) (OrbRec ob) <$> strs (index pa oa) (index pb ob)
-
--- Enumerate all orbits in a product A x B.
-product :: (Nominal a, Nominal b) => Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a, b)]
-product = productG prodStrings
-
--- Separated product: A * B = { (a,b) | Exist C1, C2 disjoint supporting a, b resp.}
-separatedProduct :: (Nominal a, Nominal b) => Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a, b)]
-separatedProduct = productG sepProdStrings
-
--- "Left product": A ⫂ B = { (a,b) | C supports a => C supports b }
-leftProduct :: (Nominal a, Nominal b) => Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a, b)]
-leftProduct = productG lsupprProdStrings
-
--- "Right product": A ⫁ B = { (a,b) | C supports a <= C supports b }
-rightProduct :: (Nominal a, Nominal b) => Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a, b)]
-rightProduct = productG rsupplProdStrings
-
--- Strictly increasing product = { (a,b) | all elements in a < all elements in b }
-increasingProduct :: (Nominal a, Nominal b) => Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a, b)]
-increasingProduct = productG incrSepProdStrings
-
--- Strictly decreasing product = { (a,b) | all elements in a > elements in b }
-decreasingProduct :: (Nominal a, Nominal b) => Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a, b)]
-decreasingProduct = productG decrSepProdStrings
-
--- Strictly decreasing product = { (a,b) | all elements in a > elements in b }
-testProduct :: (Nominal a, Nominal b) => Proxy a -> Proxy b -> Orbit a -> Orbit b -> [Orbit (a, b)]
-testProduct = productG testProdStrings
-
 {- NOTE on performance:
 Previously, I had INLINABLE and SPECIALIZE pragmas for all above definitions.
 But with benchmarking, I concluded that they do not make any difference. So
 I have removed them. The memoisation does seem to help. So that stays.
+
+I have also tried to enumerate with @Seq a@ instead of @[a]@, but that was
+slower. Other choices might be more efficient, I don't know.
 -}

src/OrbitList.hs

@@ -127,11 +127,6 @@ increasingProduct = OrbitList.productG Nominal.increasingProduct
 decreasingProduct :: forall a b. (Nominal a, Nominal b) => OrbitList a -> OrbitList b -> OrbitList (a, b)
 decreasingProduct = OrbitList.productG Nominal.decreasingProduct
 
--- Not yet the product I wish to have... That is why the name is so
--- non-informative.
-testProduct :: forall a b. (Nominal a, Nominal b) => OrbitList a -> OrbitList b -> OrbitList (a, b)
-testProduct = OrbitList.productG Nominal.testProduct
-
 productWith :: (Nominal a, Nominal b, Nominal c) => (a -> b -> c) -> OrbitList a -> OrbitList b -> OrbitList c
 productWith f as bs = map (uncurry f) (OrbitList.product as bs)
 

src/Quotient.hs

@@ -6,7 +6,7 @@ import EquivariantMap (EquivariantMap)
 import EquivariantMap qualified as Map
 import EquivariantSet (EquivariantSet)
 import EquivariantSet qualified as Set
-import Nominal hiding (product)
+import Nominal
 import Nominal.Support (intersect)
 import OrbitList