From b414b64c1aeaf580f6de7ecef0d73093888b8579 Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Wed, 9 Jan 2019 12:08:07 +0100 Subject: [PATCH] Construction of Hypothesis --- app/LStar.hs | 57 ++++++++++++++++++++++++++++++++++++------ src/EquivariantMap.hs | 6 +++++ src/Nominal/Class.hs | 1 + src/OrbitList.hs | 4 +++ src/Support/OrdList.hs | 8 +++++- 5 files changed, 68 insertions(+), 8 deletions(-) diff --git a/app/LStar.hs b/app/LStar.hs index ffd80a0..02e9379 100644 --- a/app/LStar.hs +++ b/app/LStar.hs @@ -7,25 +7,44 @@ module Main where import Nominal hiding (product) -import Support (Rat(..)) +import Support (Rat(..), Support(..), intersect) import OrbitList --(OrbitList(..), singleOrbit, product, productWith, filter, null, elem, rationals) import qualified OrbitList as List -import EquivariantMap (EquivariantMap(..), lookup) +import EquivariantMap (EquivariantMap(..), lookup, (!)) import qualified EquivariantMap as Map +import EquivariantSet (EquivariantSet(..)) import qualified EquivariantSet as Set +import Data.List (nub) import Control.Monad.State -import Prelude hiding (filter, null, elem, lookup, product, Word, map, take) +import Prelude hiding (filter, null, elem, lookup, product, Word, map, take, partition) type Word a = [a] type Rows a = OrbitList (Word a) type Columns a = OrbitList (Word a) type Table a = EquivariantMap (Word a) Bool +-- states, initial state, acceptance, transition +data Automaton q a = Automaton + { states :: OrbitList q + , initialState :: q + , acceptance :: EquivariantMap q Bool + , transition :: EquivariantMap (q, a) q + } + +instance (Nominal q, Nominal a, Show q, Show a) => Show (Automaton q a) where + show Automaton{..} = + "{ states = " ++ show (toList states) ++ + ", initialState = " ++ show initialState ++ + ", acceptance = " ++ show (Map.toList acceptance) ++ + ", transition = " ++ show (Map.toList transition) ++ + "}" + + -- Utility functions exists f = not . null . filter f forAll f = null . filter (not . f) -ext = \p a -> p <> [a] +ext p a = p <> [a] equalRows :: (Nominal a, Ord (Orbit a)) => Word a -> Word a -> Columns a -> Table a -> Bool equalRows s0 t0 suffs table = @@ -52,6 +71,18 @@ ask mq table (p, s) = Just b -> return (w, b) Nothing -> (w,) <$> mq w +quotient :: _ => EquivariantSet (a, a) -> OrbitList a -> (EquivariantMap a (Int, Support), OrbitList (Int, Support)) +quotient equiv ls = go 0 Map.empty OrbitList.empty (toList ls) + where + go n phi acc [] = (phi, acc) + go n phi acc (a:as) = + let (y0, r0) = partition (\p -> p `Set.member` equiv) (product (singleOrbit a) (fromList as)) + y1 = filter (\p -> p `Set.member` equiv) (product (singleOrbit a) (singleOrbit a)) + y2 = map (\(a1, a2) -> (a2, (n, support a1 `intersect` support a2))) (y1 <> y0) + m0 = Map.fromListWith (\(n1, s1) (n2, s2) -> (n1, s1 `intersect` s2)) . OrbitList.toList $ y2 + l0 = take 1 . fromList . fmap snd $ Map.toList m0 + in go (n+1) (phi <> m0) (acc <> l0) (Set.toList . Set.fromOrbitList . map snd $ r0) + -- invariants: * prefs and prefsExt disjoint, without dups -- * prefsExt ordered @@ -107,7 +138,7 @@ fillTable mq = do } return () -learn :: _ => (Word a -> IO Bool) -> LStar a IO () +learn :: _ => (Word a -> IO Bool) -> LStar a IO (Automaton _ _) learn mq = do Observations{..} <- get let ncl = nonClosedness prefs prefsExt suffs table @@ -123,7 +154,18 @@ learn mq = do False -> do addCols (take 1 (map (uncurry (:) . snd) inc)) mq learn mq - True -> return () + True -> do + let equiv = Set.fromOrbitList . filter (\(s, t) -> equalRows s t suffs table) $ product prefs prefs + (f, s) = quotient equiv 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 + lift (print (Map.toList trans)) + return Automaton + { states = s + , 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 + } accept :: Show a => Word a -> IO Bool @@ -143,6 +185,7 @@ main = do suffs = singleOrbit [] table = Map.empty init = Observations{..} - evalStateT (fillTable accept >> learn accept) init + aut <- evalStateT (fillTable accept >> learn accept) init + print aut return () diff --git a/src/EquivariantMap.hs b/src/EquivariantMap.hs index 58a5b9b..45f721e 100644 --- a/src/EquivariantMap.hs +++ b/src/EquivariantMap.hs @@ -10,6 +10,7 @@ module EquivariantMap where import Data.Semigroup (Semigroup) import Data.Map (Map) import qualified Data.Map as Map +import Data.Maybe (fromMaybe) import EquivariantSet (EquivariantSet(..)) import Nominal @@ -55,6 +56,8 @@ member x (EqMap m) = Map.member (toOrbit x) m lookup :: (Nominal k, Ord (Orbit k), Nominal v) => k -> EquivariantMap k v -> Maybe v lookup x (EqMap m) = mapelInv x <$> Map.lookup (toOrbit x) m +(!) :: (Nominal k, Ord (Orbit k), Nominal v) => EquivariantMap k v -> k -> v +(!) m k = fromMaybe undefined (EquivariantMap.lookup k m) -- Construction @@ -112,6 +115,9 @@ toList (EqMap l) = [(k, mapelInv k vob) | (ko, vob) <- Map.toList l, let k = get fromList :: (Nominal k, Nominal v, Ord (Orbit k)) => [(k, v)] -> EquivariantMap k v fromList l = EqMap . Map.fromList $ [(toOrbit k, mapel k v) | (k, v) <- l] +fromListWith :: forall k v. (Nominal k, Nominal v, Ord (Orbit k)) => (v -> v -> v) -> [(k, v)] -> EquivariantMap k v +fromListWith f l = EqMap . Map.fromListWithKey opf $ [(toOrbit k, mapel k v) | (k, v) <- l] + where opf ko p1 p2 = let k = getElementE ko :: k in mapel k (mapelInv k p1 `f` mapelInv k p2) -- Filter diff --git a/src/Nominal/Class.hs b/src/Nominal/Class.hs index 608f651..bd22f98 100644 --- a/src/Nominal/Class.hs +++ b/src/Nominal/Class.hs @@ -91,6 +91,7 @@ deriving via (Trivial Void) instance Nominal Void deriving via (Trivial ()) instance Nominal () deriving via (Trivial Bool) instance Nominal Bool deriving via (Trivial Char) instance Nominal Char +deriving via (Trivial Int) instance Nominal Int -- NB: Trivial instance! deriving via (Trivial Ordering) instance Nominal Ordering diff --git a/src/OrbitList.hs b/src/OrbitList.hs index ae5968f..60b7feb 100644 --- a/src/OrbitList.hs +++ b/src/OrbitList.hs @@ -54,6 +54,10 @@ map f (OrbitList as) = OrbitList $ L.map (omap f) as filter :: Nominal a => (a -> Bool) -> OrbitList a -> OrbitList a filter f = OrbitList . L.filter (f . getElementE) . unOrbitList +partition :: Nominal a => (a -> Bool) -> OrbitList a -> (OrbitList a, OrbitList a) +partition f (OrbitList s) = both OrbitList . L.partition (f . getElementE) $ s + where both g (a, b) = (g a, g b) + take :: Int -> OrbitList a -> OrbitList a take n = OrbitList . L.take n . unOrbitList diff --git a/src/Support/OrdList.hs b/src/Support/OrdList.hs index e531ab4..d7e93b8 100644 --- a/src/Support/OrdList.hs +++ b/src/Support/OrdList.hs @@ -7,7 +7,10 @@ import Support.Rat -- always sorted newtype Support = Support { unSupport :: [Rat] } - deriving (Show, Eq, Ord) + deriving (Eq, Ord) + +instance Show Support where + show = show . unSupport size :: Support -> Int size = List.length . unSupport @@ -24,6 +27,9 @@ empty = Support [] union :: Support -> Support -> Support union (Support x) (Support y) = Support (OrdList.union x y) +intersect :: Support -> Support -> Support +intersect (Support x) (Support y) = Support (OrdList.isect x y) + singleton :: Rat -> Support singleton r = Support [r]