From d96342d6653c3d9c861f59931c60e56c8824b48f Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Mon, 25 Nov 2024 11:20:35 +0100 Subject: [PATCH] More docs, cleaned up product module. Teacher now takes cmdline args --- README.md | 8 +-- app/LStar.hs | 10 +++ app/LStarPerm.hs | 14 ++-- app/Teacher.hs | 25 +++++-- run-lstar-perm.sh | 2 +- run-lstar.sh | 2 +- src/Nominal.hs | 1 - src/Nominal/Products.hs | 145 +++++++++++++++++++++++----------------- src/OrbitList.hs | 5 -- src/Quotient.hs | 2 +- 10 files changed, 124 insertions(+), 90 deletions(-) diff --git a/README.md b/README.md index 2002b51..94afeca 100644 --- a/README.md +++ b/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 -* Stuff to do permutations (not only monotone ones) +* More types of products. +* 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. diff --git a/app/LStar.hs b/app/LStar.hs index 7edba22..9449d18 100644 --- a/app/LStar.hs +++ b/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 diff --git a/app/LStarPerm.hs b/app/LStarPerm.hs index ff426bc..08fc42b 100644 --- a/app/LStarPerm.hs +++ b/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 --- "testProduct"). I am not 100% sure this is the correct way of doing it. --- It seems to work on the examples I tried. And I do think that something --- along these lines potentially works. +-- Performance can be improved by using more sophisticated products. But I +-- do not know which one to choose (which ones are corect). -- -- 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) - candidatesExt = testProduct candidates (product alph suffs) + candidates = filter (\(s, t) -> s < t && equalRows s t suffs table) (product prefs prefs) + candidatesExt = product candidates (product alph suffs) -- Main state of the L* algorithm diff --git a/app/Teacher.hs b/app/Teacher.hs index 831ad7f..9e72a55 100644 --- a/app/Teacher.hs +++ b/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 = - let ex = DoubleWord 2 - in case ex of - Fifo n -> teach "FIFO" (fifoFun n) (fifoCex n) - DoubleWord n -> teach "ATOMS" (doubleFun n) (doubleCex n) +main = do + ls <- getArgs + let model = case ls of + [x] -> read x + _ -> 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 diff --git a/run-lstar-perm.sh b/run-lstar-perm.sh index 7249cfc..f151072 100755 --- a/run-lstar-perm.sh +++ b/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 diff --git a/run-lstar.sh b/run-lstar.sh index 74390d2..b337229 100755 --- a/run-lstar.sh +++ b/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 diff --git a/src/Nominal.hs b/src/Nominal.hs index 856793f..c6a8480 100644 --- a/src/Nominal.hs +++ b/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 diff --git a/src/Nominal/Products.hs b/src/Nominal/Products.hs index 09d96e7..d9e0056 100644 --- a/src/Nominal/Products.hs +++ b/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 n m = (LT :) <$> prodStrings (n-1) m - <|> (EQ :) <$> prodStrings (n-1) (m-1) - <|> (GT :) <$> prodStrings n (m-1) + gen 1 1 = pure [EQ] <|> pure [LT, GT] <|> pure [GT, LT] + gen n m = + (EQ :) <$> prodStrings (n - 1) (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 - <|> (GT :) <$> sepProdStrings n (m-1) + gen n m = + (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 - | otherwise = (LT :) <$> lsupprProdStrings (n-1) m - <|> (EQ :) <$> lsupprProdStrings (n-1) (m-1) + | n < m = empty + | otherwise = + (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 - | otherwise = (EQ :) <$> rsupplProdStrings (n-1) (m-1) - <|> (GT :) <$> rsupplProdStrings n (m-1) + | m < n = empty + | otherwise = + (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. -} diff --git a/src/OrbitList.hs b/src/OrbitList.hs index 6fd3f78..b068c45 100644 --- a/src/OrbitList.hs +++ b/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) diff --git a/src/Quotient.hs b/src/Quotient.hs index c28a76f..f9875c8 100644 --- a/src/Quotient.hs +++ b/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