diff --git a/README.md b/README.md index bc99392..bf1d6a9 100644 --- a/README.md +++ b/README.md @@ -114,8 +114,11 @@ values, that can be much faster. ## Changelog -version 0.3.0.0 (2024-11-06): +version 0.3.1.0 (2024-11-06): * 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. version 0.2.3.0 (2024-11-05): * Updates the testing and benchmarking framework. diff --git a/app/ExampleAutomata.hs b/app/ExampleAutomata.hs index 8502f44..526731e 100644 --- a/app/ExampleAutomata.hs +++ b/app/ExampleAutomata.hs @@ -1,6 +1,7 @@ {-# language DeriveGeneric #-} {-# language DerivingVia #-} {-# language FlexibleContexts #-} +{-# language ImportQualifiedPost #-} {-# language RecordWildCards #-} {-# language UndecidableInstances #-} {-# OPTIONS_GHC -Wno-missing-signatures #-} @@ -10,14 +11,16 @@ module ExampleAutomata , module Automata ) where -import Nominal hiding (product) import Automata +import EquivariantMap qualified as Map +import EquivariantSet qualified as Set import IO +import Nominal hiding (product) import OrbitList -import qualified EquivariantMap as Map -import qualified EquivariantSet as Set +import Permutable import Data.Foldable (fold) +import Data.Map.Strict qualified as Data.Map import GHC.Generics (Generic) import Prelude as P hiding (map, product, words, filter, foldr) @@ -69,6 +72,11 @@ data FifoA = Put Atom | Get Atom deriving (Eq, Ord, Show, Generic) deriving Nominal via Generically FifoA +-- TODO: find a generic way to derive this. +instance Permutable FifoA where + act (Permuted (Perm m) (Put p)) = Put $ Data.Map.findWithDefault p p m + act (Permuted (Perm m) (Get p)) = Get $ Data.Map.findWithDefault p p m + instance ToStr FifoA where toStr (Put a) = "Put " ++ toStr a toStr (Get a) = "Get " ++ toStr a diff --git a/app/LStarPerm.hs b/app/LStarPerm.hs new file mode 100644 index 0000000..6b6b29e --- /dev/null +++ b/app/LStarPerm.hs @@ -0,0 +1,227 @@ +{-# LANGUAGE DerivingVia #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE PartialTypeSignatures #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -Wno-partial-type-signatures #-} + +import Automata (Word) +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 Permutable + +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) + +newtype PermEquivariantMap k v = PEqMap { unPEqMap :: EquivariantMap k v } + deriving Nominal via Trivially (EquivariantMap k v) + +-- Defined by the join-semilattice structure of EquivariantMap, left biased. +deriving instance Ord (Orbit k) => Monoid (PermEquivariantMap k v) +deriving instance Ord (Orbit k) => Semigroup (PermEquivariantMap k v) + +lookupP :: (Permutable k, Nominal k, Nominal v, _) => k -> PermEquivariantMap k v -> Maybe v +lookupP x (PEqMap m) = case catMaybes [Map.lookup (act px) m | px <- allPermuted x] of + [] -> Nothing + (v:_) -> Just v -- take first hit, maybe this is wrong? I guess for v ~ Bool it's fine? + +insertP :: (Nominal k, Nominal v, _) => k -> v -> PermEquivariantMap k v -> PermEquivariantMap k v +insertP k v = PEqMap . Map.insert k v . unPEqMap + +(!~) :: (Permutable k, Nominal k, Nominal v, _) => PermEquivariantMap k v -> k -> v +(!~) m k = case lookupP k m of + Just v -> v + Nothing -> error "Key not found (in PermEquivariantMap)" + +-- We use Lists, as they provide a bit more laziness +type Rows a = OrbitList (Word a) +type Columns a = OrbitList (Word a) +type Table a = PermEquivariantMap (Word a) Bool + + +-- Utility functions +exists f = not . null . filter f +forAll f = null . filter (not . f) +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 + +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) + +nonClosedness :: _ => Rows a -> Rows a -> Columns a -> Table a -> Rows a +nonClosedness prefs prefsExt suffs table = + filter (\t -> not $ closed t prefs suffs table) prefsExt + +inconsistencies :: _ => Rows a -> Columns a -> Table a -> OrbitList a -> OrbitList ((Word a, Word a), (a, Word a)) +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) + + +-- Main state of the L* algorithm +-- invariants: * prefs and prefsExt disjoint, without dups +-- * prefsExt ordered +-- * prefs and (prefs `union` prefsExt) prefix-closed +-- * table defined on (prefs `union` prefsExt) * suffs +data Observations a = Observations + { alph :: OrbitList a + , prefs :: Rows a + , prefsExt :: Rows a + , suffs :: Columns a + , table :: Table a + } + +-- input alphabet, inner monad, return value +type LStar i m a = StateT (Observations i) m a + +-- First lookup, then membership query, also update the table +ask mq (p, s) = do + Observations{..} <- get + let w = p ++ s + case lookupP w table of + Just b -> return (w, b) + Nothing -> do + b <- lift (mq w) + modify $ \o -> o { table = insertP w b table } + return (w, b) + +-- precondition: newPrefs is subset of prefExts +addRows :: _ => Rows a -> (Word a -> m Bool) -> LStar a m () +addRows newPrefs mq = do + Observations{..} <- get + let newPrefsExt = productWith ext newPrefs alph + rect = product newPrefsExt suffs + _ <- mapM (ask mq) (OrbitList.toList rect) + modify $ \o -> o { prefs = prefs <> newPrefs + , prefsExt = (prefsExt `minus` newPrefs) `union` newPrefsExt + } + return () + +-- precondition: newSuffs disjoint from suffs +addCols :: _ => Columns a -> (Word a -> m Bool) -> LStar a m () +addCols newSuffs mq = do + Observations{..} <- get + let rect = product (prefs `union` prefsExt) newSuffs + _ <- mapM (ask mq) (OrbitList.toList rect) + modify $ \o -> o { suffs = suffs <> newSuffs } + return () + +fillTable :: _ => (Word a -> m Bool) -> LStar a m () +fillTable mq = do + Observations{..} <- get + let rect = product (prefs `union` prefsExt) suffs + _ <- mapM (ask mq) (OrbitList.toList rect) + return () + +-- This could be cleaned up +learn :: _ => (Word a -> m Bool) -> (Automaton _ a -> m (Maybe (Word a))) -> LStar a m (Automaton _ a) +learn mq eq = do + Observations{..} <- get + let ncl = nonClosedness prefs prefsExt suffs table + inc = inconsistencies prefs suffs table alph + case null ncl of + False -> do + -- If not closed, then add 1 orbit of rows. Then start from top + addRows (take 1 ncl) mq + learn mq eq + True -> do + -- Closed! Now we check consistency + case null inc of + False -> do + -- If not consistent, then add 1 orbit of columns. Then start from top + addCols (take 1 (map (uncurry (:) . snd) inc)) mq + learn mq eq + True -> do + -- Also consistent! Let's build a minimal automaton! + let (f, st, _) = quotientf 0 (\s t -> s == t || equalRows s t suffs table) prefs + trans = Map.fromList . toList . map (\(s, t) -> (s, f ! t)) . filter (\(s, t) -> equalRows s t suffs table) $ product prefsExt prefs + trans2 pa = if pa `elem` prefsExt then trans ! pa else f ! pa + hypothesis = Automaton + { states = map fst st + , initialState = f ! [] + , acceptance = Map.fromList . toList . map (\p -> (f ! p, table !~ p)) $ prefs + , transition = Map.fromList . toList . map (\(p, a) -> ((f ! p, a), trans2 (ext p a))) $ product prefs alph + } + askCe = do + ce <- lift (eq hypothesis) + case ce of + Nothing -> return hypothesis + Just w -> do + let b1 = accepts hypothesis w + (_, b2) <- ask mq (w, []) + -- Ignore false counterexamples + case b1 == b2 of + True -> askCe + False -> do + -- Add all suffixes of a counterexample + let allSuffs = Set.fromList $ tails w + newSuffs = allSuffs `Set.difference` Set.fromOrbitList suffs + addCols (Set.toOrbitList newSuffs) mq + learn mq eq + askCe + + +-- Here is the teacher: just pose the queries in the terminal +askMember :: _ => Word a -> IO Bool +askMember w = do + putStrLn (toStr (MQ w)) + hFlush stdout + a <- getLine + case a of + "Y" -> return True + "N" -> return False + _ -> askMember w + +askEquiv :: _ => Automaton q a -> IO (Maybe (Word a)) +askEquiv aut = do + putStr "EQ \"" + putStr (toStr aut) + putStrLn "\"" + hFlush stdout + a <- getLine + case a of + "Y" -> return Nothing + 'N':' ':w -> return $ Just (fst $ fromStr w) + _ -> askEquiv aut + +init alph = Observations + { alph = alph + , prefs = singleOrbit [] + , prefsExt = productWith ext (singleOrbit []) alph + , suffs = singleOrbit[] + , table = mempty + } + +main :: IO () +main = do + putStrLn "ALPHABET" + hFlush stdout + alph <- getLine + case alph of + "ATOMS" -> do + aut <- evalStateT (fillTable askMember >> learn askMember askEquiv) (init rationals) + return () + "FIFO" -> do + let alph = map Put rationals `union` map Get rationals + aut <- evalStateT (fillTable askMember >> learn askMember askEquiv) (init alph) + return () + al -> do + putStr "Unknown alphabet " + putStrLn al diff --git a/ons-hs.cabal b/ons-hs.cabal index 4a70b22..fa73907 100644 --- a/ons-hs.cabal +++ b/ons-hs.cabal @@ -29,6 +29,7 @@ library Nominal.Class, Nominal.Products, OrbitList, + Permutable, Quotient, Support, Support.OrdList, @@ -55,6 +56,17 @@ executable ons-hs-lstar ExampleAutomata, IO +executable ons-hs-lstar-perm + import: stuff + hs-source-dirs: app + main-is: LStarPerm.hs + build-depends: + mtl, + ons-hs + other-modules: + ExampleAutomata, + IO + executable ons-hs-teacher import: stuff hs-source-dirs: app @@ -97,6 +109,7 @@ test-suite ons-hs-test main-is: Spec.hs other-modules: SpecMap, + SpecPermutable, SpecSet, SpecUtils build-depends: diff --git a/run-lstar-perm.sh b/run-lstar-perm.sh new file mode 100755 index 0000000..7249cfc --- /dev/null +++ b/run-lstar-perm.sh @@ -0,0 +1,31 @@ +#!/usr/bin/env bash + +# Example usage of how to run lstar against a non-interactive teacher. This +# script will create two fifos for the learner and teacher to communicate over. +# The communication is not visible, only output to stderr will be shown in +# the terminal + +# safety flags, remove x if you don't like all the output +set -euxo pipefail + +# create temporary directory, and names for the fifo queues (not files) +tempdir=$(mktemp -d run-lstar.temp.XXXXXX) +queryfifo="$tempdir/queries" +answerfifo="$tempdir/answers" + +# find the binary for the learner and teacher. +# The haskell project must be built beforehard (cabal build all) +lstar=$(cabal list-bin ons-hs-lstar-perm) +teacher=$(cabal list-bin ons-hs-teacher) + +# make the connection for the processes +mkfifo $queryfifo $answerfifo + +# run the teacher in the background +$teacher < $queryfifo > $answerfifo & + +# run the learning algorithm, measuring its time +time $lstar > $queryfifo < $answerfifo + +# clean up +rm -r $tempdir diff --git a/src/Permutable.hs b/src/Permutable.hs new file mode 100644 index 0000000..2488809 --- /dev/null +++ b/src/Permutable.hs @@ -0,0 +1,82 @@ +{-# LANGUAGE ImportQualifiedPost #-} + +module Permutable where + +import Data.List (permutations) +import Data.Map.Strict qualified as Map + +import Nominal +import Support + +--------------------------------- +--------------------------------- + +-- Invariant: No element occurs more than once +newtype Perm = Perm (Map.Map Rat Rat) + deriving (Eq, Ord, Show) + +identity :: Perm +identity = Perm Map.empty + +-- Composition (right to left) +-- TODO: check this implementation! +compose :: Perm -> Perm -> Perm +compose (Perm f) (Perm g) = reduce . Perm $ Map.compose f g <> g <> f + +-- Removes elements which are mapped to itself +reduce :: Perm -> Perm +reduce (Perm f) = Perm . Map.filterWithKey (\k v -> k /= v) $ f + +--------------------------------- +--------------------------------- + +-- Invariant: The permutation only consists of elements of the support of the +-- element a. +-- This is supposed to be a monad. For now, I don't implement the Monad +-- typeclass, but do everything by hand. (I am not going to use do notation +-- anyway.) +data Permuted a = Permuted Perm a + deriving (Eq, Ord, Show) + +embed :: a -> Permuted a +embed = Permuted identity + +-- to revalidate the invariant +shrink :: Nominal a => Permuted a -> Permuted a +shrink (Permuted (Perm m) a) = Permuted (Perm (Map.filter (\p -> elem p (toList (support a))) m)) a + +join :: Permuted (Permuted a) -> Permuted a +join (Permuted f (Permuted g a)) = Permuted (compose f g) a + +mapped :: Nominal b => (a -> b) -> Permuted a -> Permuted b +mapped fun (Permuted f a) = shrink $ Permuted f (fun a) + +bind :: Nominal b => (a -> Permuted b) -> Permuted a -> Permuted b +bind comp (Permuted f a) = case comp a of + Permuted g b -> shrink $ Permuted (compose g f) b + +allPermutations :: Support -> [Perm] +allPermutations (Support xs) = fmap (reduce . Perm . Map.fromList . zip xs) . permutations $ xs + +-- Returns a lazy list +allPermuted :: Nominal a => a -> [Permuted a] +allPermuted el = fmap (flip Permuted el) . allPermutations . support $ el + +--------------------------------- +--------------------------------- + +-- I want Nominal to be a superclass. But for now that gets in the way (as +-- Permuted is not yet a Nominal type). +-- Note that acting on an element may change its orbit (as ordered nominal +-- set). +class Permutable a where + act :: Permuted a -> a + +instance Permutable (Permuted a) where + act = join + +instance Permutable Rat where + act (Permuted (Perm m) p) = Map.findWithDefault p p m + +instance Permutable a => Permutable [a] where + act (Permuted f ls) = fmap (\x -> act (Permuted f x)) ls diff --git a/test/Spec.hs b/test/Spec.hs index 94e7069..1990c1f 100644 --- a/test/Spec.hs +++ b/test/Spec.hs @@ -10,6 +10,7 @@ import OrbitList (repeatRationals, size) import Support (Rat (..)) import SpecMap +import SpecPermutable import SpecSet import SpecUtils () @@ -17,7 +18,7 @@ main :: IO () main = defaultMain allTests allTests :: TestTree -allTests = testGroup "main" [setTests, mapTests, countingTests, qcTests] +allTests = testGroup "main" [setTests, mapTests, countingTests, qcTests, permutableTests] -- Verifying that the number of orbits is correct. Up to length 7, because -- length 8 and longer take at least one second. diff --git a/test/SpecPermutable.hs b/test/SpecPermutable.hs new file mode 100644 index 0000000..8a07208 --- /dev/null +++ b/test/SpecPermutable.hs @@ -0,0 +1,28 @@ +{-# OPTIONS_GHC -Wno-orphans #-} + +module SpecPermutable (permutableTests) where + +import Test.Tasty +import Test.Tasty.HUnit hiding (assert) + +import Nominal +import Permutable +import Support (Rat (..)) + +import SpecUtils + +permutableTests :: TestTree +permutableTests = testGroup "Permutable" [assocTest n | n <- [0 .. 6]] + +-- For n = 7, this takes roughly 30 seconds! +assocTest :: Int -> TestTree +assocTest n = + testCase ("associativity " <> show n) $ + assert and $ + [lhs f g == rhs f g | f <- perms, g <- perms] + where + element = fmap (Rat . toRational) $ [1 .. n] + supp = support element + perms = allPermutations supp + lhs f g = act (Permuted (compose f g) element) + rhs f g = act (Permuted f (act (Permuted g element)))