From 2e913bd666e1f5c65a8b4ee103fb0a96fed9b4ad Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Wed, 6 Nov 2024 15:16:22 +0100 Subject: [PATCH] Made LStarPerm slightly faster, but potentially wrong. --- app/LStarPerm.hs | 45 ++++++++++++++++++++++++++++++++--------- ons-hs.cabal | 2 +- src/Nominal.hs | 4 ++++ src/Nominal/Products.hs | 12 +++++++++++ src/OrbitList.hs | 5 +++++ 5 files changed, 57 insertions(+), 11 deletions(-) diff --git a/app/LStarPerm.hs b/app/LStarPerm.hs index 6b6b29e..6c4433e 100644 --- a/app/LStarPerm.hs +++ b/app/LStarPerm.hs @@ -1,6 +1,7 @@ {-# LANGUAGE DerivingVia #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE ImportQualifiedPost #-} {-# LANGUAGE PartialTypeSignatures #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE StandaloneDeriving #-} @@ -8,22 +9,39 @@ {-# OPTIONS_GHC -Wno-partial-type-signatures #-} import Automata (Word) +import EquivariantMap (EquivariantMap(..), (!)) +import EquivariantMap qualified as Map +import EquivariantSet qualified as Set import ExampleAutomata import IO -import Quotient -import OrbitList -import EquivariantMap (EquivariantMap(..), (!)) -import qualified EquivariantMap as Map -import qualified EquivariantSet as Set import Nominal (Nominal, Orbit, Trivially(..)) +import OrbitList import Permutable +import Quotient +import Control.Monad.State import Data.List (tails) import Data.Maybe (catMaybes) -import Control.Monad.State -import System.IO (hFlush, stdout) import Prelude hiding (filter, null, elem, lookup, product, Word, map, take, init) +import System.IO (hFlush, stdout) +-- This is like the LStar algorithm in LStar.hs, but it skips membership +-- queries which are permutations of ones already asked. This saves a lot of +-- queries, but is slower computationally. The permutations are nicely hidden +-- 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. +-- +-- Another way forway would be to use the `Permuted` monad, also in the +-- automaton type. But that requires more thinking. + + +-------------------------------------------- +-- New data structure to handle permutations newtype PermEquivariantMap k v = PEqMap { unPEqMap :: EquivariantMap k v } deriving Nominal via Trivially (EquivariantMap k v) @@ -44,6 +62,10 @@ insertP k v = PEqMap . Map.insert k v . unPEqMap Just v -> v Nothing -> error "Key not found (in PermEquivariantMap)" + +-------------------------------------------- +-- From here, it's almost exactly LStar.hs + -- We use Lists, as they provide a bit more laziness type Rows a = OrbitList (Word a) type Columns a = OrbitList (Word a) @@ -57,7 +79,10 @@ ext p a = p <> [a] equalRows :: _ => Word a -> Word a -> Columns a -> Table a -> Bool equalRows t0 s0 suffs table = - forAll (\((t, s), e) -> lookupP (s ++ e) table == lookupP (t ++ e) table) $ product (singleOrbit (t0, s0)) suffs + -- 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 closed :: _ => Word a -> Rows a -> Columns a -> Table a -> Bool closed t prefs suffs table = @@ -71,8 +96,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) (product prefs prefs) - candidatesExt = product candidates (product alph suffs) + candidates = filter (\(s, t) -> s < t && equalRows s t suffs table) (testProduct prefs prefs) + candidatesExt = testProduct candidates (product alph suffs) -- Main state of the L* algorithm diff --git a/ons-hs.cabal b/ons-hs.cabal index fa73907..d64aed4 100644 --- a/ons-hs.cabal +++ b/ons-hs.cabal @@ -1,6 +1,6 @@ cabal-version: 2.2 name: ons-hs -version: 0.3.0.0 +version: 0.3.1.0 synopsis: Implementation of the ONS (Ordered Nominal Sets) library in Haskell description: Nominal sets are structured infinite sets. They have symmetries which make them finitely representable. This library provides basic manipulation of them for the total order symmetry. It includes: products, sums, maps and sets. Can work with custom data types. homepage: https://github.com/Jaxan/ons-hs diff --git a/src/Nominal.hs b/src/Nominal.hs index b461274..54730ae 100644 --- a/src/Nominal.hs +++ b/src/Nominal.hs @@ -48,3 +48,7 @@ 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 diff --git a/src/Nominal/Products.hs b/src/Nominal/Products.hs index 9c7bf91..445b808 100644 --- a/src/Nominal/Products.hs +++ b/src/Nominal/Products.hs @@ -56,6 +56,18 @@ decrSepProdStrings :: Alternative f => Int -> Int -> f [Ordering] 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) + + {- 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 diff --git a/src/OrbitList.hs b/src/OrbitList.hs index e065e6f..c801ff1 100644 --- a/src/OrbitList.hs +++ b/src/OrbitList.hs @@ -126,6 +126,11 @@ 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)