Minimisation

app/Minimise.hs

@@ -0,0 +1,140 @@
+{-# language DeriveGeneric #-}
+{-# language DerivingVia #-}
+{-# language FlexibleContexts #-}
+{-# language PartialTypeSignatures #-}
+{-# language RecordWildCards #-}
+{-# language UndecidableInstances #-}
+{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
+
+import Nominal hiding (product)
+import Support (Rat(..), Support)
+import OnsAutomata
+import OnsQuotient
+import OrbitList
+import EquivariantMap ((!))
+import qualified EquivariantMap as Map
+import qualified EquivariantSet as Set
+
+import Data.Foldable (fold)
+import qualified GHC.Generics as GHC
+import Prelude as P hiding (map, product, words, filter)
+
+
+-- Version A: works on equivalence relations
+minimiseA :: _ => Automaton q a -> OrbitList a -> Automaton _ a
+minimiseA Automaton{..} alph = Automaton
+  { states = states2
+  , initialState = phi ! initialState
+  , acceptance = Map.fromList . fmap (\(s, b) -> (phi ! s, b)) . Map.toList $ acceptance
+  , transition = Map.fromList . fmap (\((s, a), t) -> ((phi ! s, a), phi ! t)) . Map.toList $ transition
+  }
+  where
+    -- Are all successors of s0 t0 related?
+    nextAreEquiv equiv s0 t0 = OrbitList.null
+      . filter (\(s2, t2) -> s2 /= t2 && not ((s2, t2) `Set.member` equiv))
+      $ productWith (\(s, t) a -> (transition ! (s, a), transition ! (t, a))) (singleOrbit (s0, t0)) alph
+    -- Recursively shrink equiv to fixpoint
+    go equiv = let (equiv2, nonEq) = Set.partition (\(s, t) -> s == t || nextAreEquiv equiv s t) equiv
+               in if Set.null nonEq -- fixpoint!
+                  then equiv
+                  else go equiv2
+    -- Start with FxF + NxN
+    (y, n) = partition (acceptance !) states
+    equiv0 = Set.fromOrbitList $ y `product` y <> n `product` n
+    -- compute fixpoint
+    equivInf = go equiv0
+    -- get quotient
+    (phi, states2) = quotient equivInf states
+
+
+-- Version B: works on quotient maps
+minimiseB :: _ => Automaton q a -> OrbitList a -> Automaton _ a
+minimiseB Automaton{..} alph = Automaton
+  { states = stInf
+  , initialState = phiInf ! initialState
+  , acceptance = Map.fromList . fmap (\(s, b) -> (phiInf ! s, b)) . Map.toList $ acceptance
+  , transition = Map.fromList . fmap (\((s, a), t) -> ((phiInf ! s, a), phiInf ! t)) . Map.toList $ transition
+  }
+  where
+    -- Are all successors of s0 t0 related?
+    nextAreEquiv phi s0 t0 = OrbitList.null
+      . filter (\(s2, t2) -> s2 /= t2 && phi ! s2 /= phi ! t2)
+      $ productWith (\(s, t) a -> (transition ! (s, a), transition ! (t, a))) (singleOrbit (s0, t0)) alph
+    -- Are s0 t0 equivalent with current information?
+    equiv phi s0 t0 = s0 == t0 || (phi ! s0 == phi ! t0 && nextAreEquiv phi s0 t0)
+    -- Given a quotientmap, refine it
+    go phi st = let (phi2, st2) = quotientf (equiv phi) states
+             in if size st == size st2
+                then (phi, st)
+                else go phi2 st2
+    -- Start with acceptance as quotient map
+    (phi0, st0) = quotientf (\a b -> a == b || acceptance ! a == acceptance ! b) states
+    -- Compute fixpoint
+    (phiInf, stInf) = go phi0 st0
+
+
+main :: IO ()
+main = do
+  -- putStrLn . toStr . toList . map (\x -> (x, True)) $ words 2
+  -- putStrLn . toStr $ (fifoAut 3)
+  putStrLn . toStr $ (minimiseB (fifoAut 2) fifoAlph)
+
+
+-- All example automata follow below
+
+-- words of length <= m
+words m = fold $ go (m+1) (singleOrbit []) where
+  go 0 acc = []
+  go k acc = acc : go (k-1) (productWith (:) rationals acc)
+
+fromKeys f = Map.fromSet f . Set.fromOrbitList
+
+
+data DoubleWord = Store [Rat] | Check [Rat] | Accept | Reject
+  deriving (Eq, Ord, GHC.Generic)
+  deriving Nominal via Generic DoubleWord
+
+doubleWordAut 0 = Automaton {..} where
+  states = fromList [Accept, Reject]
+  initialState = Accept
+  acceptance = fromKeys (Accept ==) states
+  transition = fromKeys (const Reject) $ product states rationals
+doubleWordAut n = Automaton {..} where
+  states = fromList [Accept, Reject] <> map Store (words (n-1)) <> map Check (productWith (:) rationals (words (n-1)))
+  initialState = Store []
+  acceptance = fromKeys (Accept ==) states
+  trans Accept _ = Reject
+  trans Reject _ = Reject
+  trans (Store l) a
+    | length l < n = Store (a:l)
+    | otherwise    = Check (reverse (a:l))
+  trans (Check (a:as)) b
+    | a == b    = if (P.null as) then Accept else Check as
+    | otherwise = Reject
+  transition = fromKeys (uncurry trans) $ product states rationals
+
+
+data FifoS = FifoS [Rat] [Rat]
+  deriving (Eq, Ord, GHC.Generic)
+  deriving Nominal via Generic FifoS
+
+instance ToStr FifoS where
+  toStr (FifoS l1 l2) = "F " ++ toStr l1 ++ " - " ++ toStr l2
+
+fifoAlph = map Put rationals <> map Get rationals
+
+fifoAut n = Automaton {..} where
+  states0 = filter (\(FifoS l1 l2) -> length l1 + length l2 <= n) $ productWith (\l1 l2 -> FifoS l1 l2) (words n) (words n)
+  states = fromList [Nothing] <> map Just states0
+  initialState = Just (FifoS [] [])
+  acceptance = fromKeys (Nothing /=) states
+  trans Nothing _ = Nothing
+  trans (Just (FifoS l1 l2)) (Put a)
+    | length l1 + length l2 >= n = Nothing
+    | otherwise                  = Just (FifoS (a:l1) l2)
+  trans (Just (FifoS [] [])) (Get _) = Nothing
+  trans (Just (FifoS l1 [])) (Get b) = trans (Just (FifoS [] (reverse l1))) (Get b)
+  trans (Just (FifoS l1 (a:l2))) (Get b)
+    | a == b    = Just (FifoS l1 l2)
+    | otherwise = Nothing
+  transition = fromKeys (uncurry trans) $ product states fifoAlph

app/OnsAutomata.hs

@@ -2,7 +2,6 @@
 {-# language DerivingVia #-}
 {-# language FlexibleContexts #-}
 {-# language RecordWildCards #-}
-{-# language StandaloneDeriving #-}
 {-# language UndecidableInstances #-}
 module OnsAutomata where
 
@@ -19,7 +18,7 @@ import Prelude hiding (print, Word)
 import qualified GHC.Generics as GHC
 
 
-type Word a    = [a]
+type Word a = [a]
 
 -- states, initial state, acceptance, transition
 data Automaton q a = Automaton
@@ -40,7 +39,7 @@ accepts aut l = go (initialState aut) l
 -- alphetbet for the Fifo queue example
 data Fifo = Put Rat | Get Rat
   deriving (Eq, Ord, Show, GHC.Generic)
-deriving via Generic Fifo instance Nominal Fifo
+  deriving Nominal via Generic Fifo
 
 
 -- I do not want to give weird Show instances for basic types, so I create my
@@ -68,6 +67,9 @@ instance ToStr a => ToStr [a] where
   toStr = concat . intersperse " " . fmap toStr
 instance (ToStr a, ToStr b) => ToStr (a, b) where
   toStr (a, b) = "(" ++ toStr a ++ ", " ++ toStr b ++ ")"
+instance ToStr a => ToStr (Maybe a) where
+  toStr Nothing  = "Nothing"
+  toStr (Just a) = "Just " ++ toStr a
 
 instance (Nominal q, Nominal a, ToStr q, ToStr a) => ToStr (Automaton q a) where
   toStr Automaton{..} =

app/OnsQuotient.hs

@@ -9,20 +9,26 @@ import qualified EquivariantMap as Map
 import EquivariantSet (EquivariantSet(..))
 import qualified EquivariantSet as Set
 
-import Prelude (Int, Ord, (.), (<>), (+), ($), snd, fmap)
+import Prelude (Bool, Int, Ord, (.), (<>), (+), ($), snd, fmap, uncurry)
 
 type QuotientType = (Int, Support)
 type QuotientMap a = EquivariantMap a QuotientType
 
--- Non trivial, should be made more efficient
+-- Computes a quotient map given an equivalence relation
 quotient :: (Nominal a, Ord (Orbit a)) => EquivariantSet (a, a) -> OrbitList a -> (QuotientMap a, OrbitList QuotientType)
-quotient equiv ls = go 0 Map.empty empty (toList ls)
+quotient equiv = quotientf (\a b -> (a, b) `Set.member` equiv)
+
+-- f should be equivariant and an equivalence relation
+quotientf :: (Nominal a, Ord (Orbit a)) => (a -> a -> Bool) -> OrbitList a -> (QuotientMap a, OrbitList QuotientType)
+quotientf f ls = go 0 Map.empty empty (toList ls)
   where
     go _ 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))
+      let y0 = filter (uncurry f) (product (singleOrbit a) (fromList as))
+          y1 = filter (uncurry f) (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)) . 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)
+      in if a `Set.member` (Map.keysSet phi)
+         then go n phi acc as
+         else go (n+1) (phi <> m0) (acc <> l0) as

ons-hs.cabal

@@ -34,7 +34,6 @@ library
 executable ons-hs-solver
   hs-source-dirs:      app
   main-is:             Main.hs
-  ghc-options:         -threaded -rtsopts -with-rtsopts=-N
   build-depends:       base
                      , ons-hs
   ghc-options:         -threaded -rtsopts -with-rtsopts=-N -O2
@@ -43,7 +42,17 @@ executable ons-hs-solver
 executable ons-hs-lstar
   hs-source-dirs:      app
   main-is:             LStar.hs
-  ghc-options:         -threaded -rtsopts -with-rtsopts=-N
+  build-depends:       base
+                     , mtl
+                     , ons-hs
+  other-modules:       OnsAutomata
+                     , OnsQuotient
+  ghc-options:         -threaded -rtsopts -with-rtsopts=-N -O2
+  default-language:    Haskell2010
+
+executable ons-hs-minimise
+  hs-source-dirs:      app
+  main-is:             Minimise.hs
   build-depends:       base
                      , mtl
                      , ons-hs

src/EquivariantMap.hs

@@ -21,7 +21,7 @@ import Support
 -- TODO: adjust / alter / update
 -- TODO: -WithKey functions
 -- TODO: don't export the helper functions
--- TODO: cleanup (usage of getElelemtE is not necessary)
+-- TODO: cleanup (usage of getElelemtE is not always necessary?)
 -- TODO: replace [Bool] by Vec Bool if better?
 
 
@@ -105,6 +105,7 @@ mapWithKey f (EqMap m) = EqMap (Map.mapWithKey f2 m)
 keysSet :: EquivariantMap k v -> EquivariantSet k
 keysSet (EqMap m) = EqSet (Map.keysSet m)
 
+-- f equivariant
 fromSet :: (Nominal k, Nominal v) => (k -> v) -> EquivariantSet k -> EquivariantMap k v
 fromSet f (EqSet s) = EqMap (Map.fromSet f2 s)
   where f2 ko = let k = getElementE ko in mapel k (f k)

src/OrbitList.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE DerivingVia #-}
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE UndecidableInstances #-}
@@ -23,6 +24,10 @@ deriving instance Ord (Orbit a) => Ord (OrbitList a)
 deriving instance Show (Orbit a) => Show (OrbitList a)
 deriving via (Trivial (OrbitList a)) instance Nominal (OrbitList a)
 
+-- Simply concatenation of the list
+deriving instance Semigroup (OrbitList a)
+deriving instance Monoid (OrbitList a)
+
 
 -- Query
 
@@ -32,6 +37,10 @@ null (OrbitList x) = L.null x
 elem :: (Nominal a, Eq (Orbit a)) => a -> OrbitList a -> Bool
 elem x = L.elem (toOrbit x) . unOrbitList
 
+-- Sizes of supports of all orbits (sorted, big to small)
+size :: forall a. Nominal a => OrbitList a -> [Int]
+size = LO.sortOn negate . fmap (index (Proxy :: Proxy a)) . unOrbitList
+
 
 -- Construction
 
@@ -44,6 +53,10 @@ singleOrbit a = OrbitList [toOrbit a]
 rationals :: OrbitList Rat
 rationals = singleOrbit (Rat 0)
 
+repeatRationals :: Int -> OrbitList [Rat]
+repeatRationals 0 = singleOrbit []
+repeatRationals n = productWith (:) rationals (repeatRationals (n-1))
+
 
 -- Map / Filter / ...
 
@@ -61,6 +74,10 @@ partition f (OrbitList s) = both OrbitList . L.partition (f . getElementE) $ s
 take :: Int -> OrbitList a -> OrbitList a
 take n = OrbitList . L.take n . unOrbitList
 
+-- TODO: drop, span, takeWhile, ...
+-- TODO: folds
+
+
 -- Combinations
 
 product :: forall a b. (Nominal a, Nominal b) => OrbitList a -> OrbitList b -> OrbitList (a, b)
@@ -69,8 +86,25 @@ product (OrbitList as) (OrbitList bs) = OrbitList . concat $ (Nominal.product (P
 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)
 
-instance Semigroup (OrbitList a) where (OrbitList as) <> (OrbitList bs) = OrbitList (as <> bs)
-instance Monoid (OrbitList a) where mempty = empty
+-- TODO: productWith is the same as liftA2, so we could provide an
+-- Applicative instance (with singleOrbit as pure). Although, I'm not
+-- sure we can do <*>, hmm.. The Alternative instance is given by
+-- concatenation (i.e. the monoid structure).
+
+-- NOTE: only works for equivariant f! In theory, the Monad instance
+-- should work over all finitely supported functions, but that's harder
+-- to implement.
+bind :: (Nominal a, Nominal b) => OrbitList a -> (a -> OrbitList b) -> OrbitList b
+bind (OrbitList as) f = OrbitList (L.concatMap (unOrbitList . f . getElementE) as)
+
+
+-- Conversions
+
+toList :: Nominal a => OrbitList a -> [a]
+toList = fmap getElementE . unOrbitList
+
+fromList :: Nominal a => [a] -> OrbitList a
+fromList = OrbitList . fmap toOrbit
 
 
 -- Sorted Lists
@@ -98,12 +132,3 @@ projectWith f = unionAll . fmap OrbitList . groupOnFst . splitOrbs . unOrbitList
   where
     splitOrbs = fmap (\o -> (omap fst o, omap snd o))
     groupOnFst = fmap (fmap snd) . L.groupBy (\x y -> fst x == fst y)
-
-
--- Conversions
-
-toList :: Nominal a => OrbitList a -> [a]
-toList = fmap getElementE . unOrbitList
-
-fromList :: Nominal a => [a] -> OrbitList a
-fromList = OrbitList . fmap toOrbit