indistinguishability minimization

1 files changed, 218 insertions, 114 deletions

diff --git a/src/Lib.hs b/src/Lib.hs
index e8bc698..0e093e3 100644
--- a/src/Lib.hs
+++ b/src/Lib.hs
@@ -1,60 +1,73 @@
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TupleSections #-}
+{-# LANGUAGE BangPatterns #-}
 
 module Lib where
 
-import Data.Char (chr, ord)
-import qualified Data.List as L
-import qualified Data.Map as M
-import Data.Maybe (fromJust)
-import qualified Data.Set as S
-import Debug.Trace ()
-import Parser
-import qualified Text.Parsec as Parsec
+import           Data.Char                      ( chr
+                                                , ord
+                                                )
+import qualified Data.List                     as L
+import qualified Data.Map                      as M
+import           Data.Maybe                     ( fromJust )
+import qualified Data.Set                      as S
+import           Debug.Trace                    ( traceShowId
+                                                , traceShow
+                                                )
+import           Parser
+import qualified Text.Parsec                   as Parsec
 
 mget :: (Ord a) => a -> M.Map a b -> b
 mget a m = fromJust $ M.lookup a m
 
 automatizem :: M.Map Addend Int -> Matrix -> DFA [Int] Int
-automatizem dir (MEq as bs) = eq (fromIntegral $ length dir) (map (`mget` dir) as) (map (`mget` dir) bs)
-automatizem dir (MLe a b) = le (mget a dir) (mget b dir)
-automatizem dir (MLt a b) = lt (mget a dir) (mget b dir)
+automatizem dir (MEq as bs) =
+  eq (fromIntegral $ length dir) (map (`mget` dir) as) (map (`mget` dir) bs)
+automatizem dir (MLe  a b) = le (mget a dir) (mget b dir)
+automatizem dir (MLt  a b) = lt (mget a dir) (mget b dir)
 automatizem dir (MAnd x y) = conj (automatizem dir x) (automatizem dir y)
-automatizem dir (MOr x y) = disj (automatizem dir x) (automatizem dir y)
-automatizem dir (MNot x) = compl (automatizem dir x)
+automatizem dir (MOr  x y) = disj (automatizem dir x) (automatizem dir y)
+automatizem dir (MNot x  ) = compl (automatizem dir x)
 
 automatize :: M.Map Addend Int -> QNMFormula -> NFA [Int] Int
-automatize dir (QNMFormula [] m) = minimize (fromIntegral $ length dir) $ nondeterminize $ automatizem dir m
+automatize dir (QNMFormula [] m) =
+  let dfa@( DFA s  _ _ _) = automatizem dir m
+      mdfa@(DFA s' _ _ _) = rmdist dfa (fromIntegral (length dir))
+      !t                  = (traceShowId $ (length s, length s'))
+  in  minimize (fromIntegral $ length dir) $ nondeterminize $ mdfa
 automatize dir (QNMFormula (Neg : quas) m) =
   let nfa = automatize dir (QNMFormula quas m)
-   in minimize (fromIntegral (length dir)) (ncompl nfa)
+  in  minimize (fromIntegral (length dir)) (ncompl nfa)
+ where
+  rmmin d = rmdist d (fromIntegral (length dir))
+  ncompl = nondeterminize . compl . rmmin . determinize
 automatize dir (QNMFormula (Qua (Exists, v) : quas) m) =
   let nfa = automatize dir (QNMFormula quas m)
-   in case M.lookup (Var v) dir of
-        Nothing -> nfa
+  in  case M.lookup (Var v) dir of
+        Nothing  -> nfa
         (Just i) -> minimize (fromIntegral $ length dir) $ existentialize i nfa
 
 assign :: S.Set Addend -> M.Map Addend Int
 assign xs = M.fromList (zip (S.toList xs) [0 ..])
 
 collect :: Matrix -> S.Set Addend
-collect (MEq as bs) = S.fromList (as ++ bs)
-collect (MLe a b) = S.fromList [a, b]
-collect (MLt a b) = S.fromList [a, b]
-collect (MAnd x y) = S.union (collect x) (collect y)
-collect (MOr x y) = S.union (collect x) (collect y)
-collect (MNot x) = collect x
+collect (MEq  as bs) = S.fromList (as ++ bs)
+collect (MLe  a  b ) = S.fromList [a, b]
+collect (MLt  a  b ) = S.fromList [a, b]
+collect (MAnd x  y ) = S.union (collect x) (collect y)
+collect (MOr  x  y ) = S.union (collect x) (collect y)
+collect (MNot x    ) = collect x
 
 literals :: M.Map Addend Int -> [[Int]]
 literals m =
-  let addends = L.sortOn snd (M.toList m)
-      reversedLiterals = map (\(a, i) -> addendReverseBinary a) addends
-      max = L.maximum (map length reversedLiterals)
-      paddedReversed = map (\x -> x ++ replicate (max - length x) 0) reversedLiterals
-      padded = map reverse paddedReversed
-   in L.transpose padded
+  let
+    addends          = L.sortOn snd (M.toList m)
+    reversedLiterals = map (\(a, i) -> addendReverseBinary a) addends
+    max              = L.maximum (map length reversedLiterals)
+    paddedReversed =
+      map (\x -> x ++ replicate (max - length x) 0) reversedLiterals
+    padded = map reverse paddedReversed
+  in
+    L.transpose padded
 
 addendReverseBinary :: Addend -> [Int]
 addendReverseBinary (Var x) = []
@@ -66,12 +79,12 @@ reverseBinary n = fromIntegral (mod n 2) : reverseBinary (div n 2)
 
 eval :: QNMFormula -> Bool
 eval f@(QNMFormula q m) =
-  let dir = (assign $ collect m)
-      nfa = automatize dir f
+  let dir   = (assign $ collect m)
+      nfa   = automatize dir f
       input = literals (assign $ collect m)
-   in runNFA nfa input
+  in  runNFA nfa input
 
-data State a = Single a | Double (State a, State a) | Multi [State a] deriving (Eq, Ord, Show)
+data State a = S a | Double (State a, State a) | Multi [State a] deriving (Eq, Ord, Show)
 
 data DFA c a = DFA [State a] (State a) [State a] (State a -> c -> State a)
 
@@ -80,35 +93,137 @@ data NFA c a = NFA [State a] [State a] [State a] (State a -> c -> [State a])
 runDFA :: (Ord a) => DFA c a -> [c] -> Bool
 runDFA (DFA _ start accepts f) cs = foldl f start cs `elem` accepts
 
+minimize :: (Ord a) => Integer -> NFA [Int] a -> NFA [Int] a
+minimize n nfa@(NFA _ starts accepts f) = NFA states' starts' accepts' f
+ where
+  states'  = closure nfa (chars n) starts
+  starts'  = starts `L.intersect` states'
+  accepts' = accepts `L.intersect` states'
+
+
+rmdist :: (Ord a, Show a) => DFA [Int] a -> Integer -> DFA [Int] a
+rmdist dfa@(DFA states start accepts f) n =
+  let
+    statecandidates = minimize2 dfa n
+    states'         = map head statecandidates
+    start' = head $ head $ filter (\c -> L.elem start c) statecandidates
+    accepts'        = L.intersect accepts states'
+    f' s c =
+      let s' = f s c
+      in  head $ head $ filter (\c -> L.elem s' c) statecandidates
+  in
+    DFA states' start' accepts' f'
+
+
+minimize2 :: (Ord a, Show a) => DFA [Int] a -> Integer -> [[State a]]
+minimize2 dfa@(DFA states start accepts f) n =
+  let p0 = [states L.\\ accepts, accepts] in minrec dfa n p0
+
+minrec
+  :: (Ord a, Show a) => DFA [Int] a -> Integer -> [[State a]] -> [[State a]]
+minrec dfa n pklast =
+  let next = concatMap (\part -> minimize3 dfa n pklast [] part) pklast
+  in  if normpartition next == normpartition pklast
+        then next
+        else minrec dfa n next
+
+normpartition :: Ord a => [[a]] -> S.Set (S.Set a)
+normpartition xs = S.fromList (map S.fromList xs)
+
+
+minimize3
+  :: (Ord a, Show a)
+  => DFA [Int] a
+  -> Integer
+  -> [[State a]]
+  -> [[State a]]
+  -> [State a]
+  -> [[State a]]
+minimize3 dfa@(DFA states starts accepts f) n pklast pk [] = pk
+minimize3 dfa@(DFA states starts accepts f) n pklast [] (x : xs) =
+  minimize3 dfa n pklast [[x]] xs
+minimize3 dfa@(DFA states starts accepts f) n pklast pk (x : xs) =
+  let ys = filter (\s -> equivall dfa pklast (chars n) (head s) x) pk
+  in  if ys == []
+        then minimize3 dfa n pklast ([x] : pk) xs
+        else
+          let coll  = (head ys)
+              trunc = L.delete coll pk
+              new   = x : coll
+              pk'   = new : trunc
+          in  minimize3 dfa n pklast pk' xs
+
+equivall
+  :: (Eq a)
+  => DFA [Int] a
+  -> [[State a]]
+  -> [[Int]]
+  -> (State a)
+  -> (State a)
+  -> Bool
+equivall dfa partition cs x y = all (\c -> not $ dist dfa partition c x y) cs
+
+states = S <$> [0, 1, 2, 3, 4]
+start = S 0
+accepts = [S 4]
+f (S 0) [0] = S 1
+f (S 0) [1] = S 2
+f (S 1) [0] = S 1
+f (S 1) [1] = S 3
+f (S 2) [0] = S 1
+f (S 2) [1] = S 2
+f (S 3) [0] = S 1
+f (S 3) [1] = S 4
+f (S 4) [0] = S 1
+f (S 4) [1] = S 2
+dfa = DFA states start accepts f
+p0 = [states L.\\ accepts, accepts]
+p1 = concatMap (minimize3 dfa 1 p0 []) p0
+p2 = concatMap (minimize3 dfa 1 p1 []) p1
+minp = minimize2 dfa 1
+
+
+dist
+  :: (Eq a)
+  => DFA [Int] a
+  -> [[State a]]
+  -> [Int]
+  -> (State a)
+  -> (State a)
+  -> Bool
+dist (DFA states starts accepts f) partition c x y =
+  (findset partition (f x c)) /= (findset partition (f y c))
+
+findset :: (Eq a) => [[State a]] -> State a -> [State a]
+findset xs x = head (filter (\s -> L.elem x s) xs)
+
 runNFA :: (Ord a) => NFA c a -> [c] -> Bool
 runNFA (NFA _ starts accepts f) cs =
-  foldl (\xs c -> L.nub $ concatMap (`f` c) xs) starts cs `L.intersect` accepts /= []
+  foldl (\xs c -> L.nub $ concatMap (`f` c) xs) starts cs
+    `L.intersect` accepts
+    /=            []
 
 reversal :: (Ord a) => NFA c a -> NFA c a
 reversal (NFA states starts accepts f) = NFA states accepts starts f'
-  where
-    f' s c = filter (\state -> s `elem` f state c) states
+  where f' s c = filter (\state -> s `elem` f state c) states
 
 eq :: Integer -> [Int] -> [Int] -> DFA [Int] Int
 eq n is js = determinize $ minimize n $ reversal $ nondeterminize dfa
-  where
-    states = Single <$> [- (length js - 1) .. length is - 1 + 1]
-    start = Single 0
-    accepts = [Single 0]
-    rejector = last states
-    f :: State Int -> [Int] -> State Int
-    f carrystate@(Single carry) c =
-      if carrystate == rejector
-        then rejector
-        else
-          let si = sum (map (c !!) is)
-              sj = sum (map (c !!) js)
-              parityok = mod (carry + si) 2 == mod sj 2
-              newcarry = div (carry + si - sj) 2
-           in if parityok
-                then Single newcarry
-                else rejector
-    dfa = DFA states start accepts f
+ where
+  states   = S <$> [-(length js - 1) .. length is - 1 + 1]
+  start    = S 0
+  accepts  = [S 0]
+  rejector = last states
+  f :: State Int -> [Int] -> State Int
+  f carrystate@(S carry) c = if carrystate == rejector
+    then rejector
+    else
+      let si       = sum (map ((c) !!) (is))
+          sj       = sum (map (c !!) (js))
+          parityok = mod (carry + si) 2 == mod sj 2
+          newcarry = div (carry + si - sj) 2
+      in  if parityok then S newcarry else rejector
+  dfa = DFA states start accepts f
 
 le :: Int -> Int -> DFA [Int] Int
 le = less LessEqual
@@ -119,36 +234,37 @@ lt = less LessThan
 data LessType = LessEqual | LessThan deriving (Eq, Ord, Show)
 
 less :: LessType -> Int -> Int -> DFA [Int] Int
-less lt i j = DFA [Single 0, Single 1, Single 2] (Single 0) accepts f
-  where
-    accepts = if lt == LessEqual then [Single 0, Single 2] else [Single 2]
-    f s c = case (s, (c !! i, c !! j)) of
-      (Single 0, (1, 1)) -> Single 0
-      (Single 0, (0, 0)) -> Single 0
-      (Single 0, (1, 0)) -> Single 1
-      (Single 0, _) -> Single 2
-      (Single 1, _) -> Single 1
-      (_, _) -> Single 2
+less lt i j = DFA [S 0, S 1, S 2] (S 0) accepts f
+ where
+  accepts = if lt == LessEqual then [S 0, S 2] else [S 2]
+  f s c = case (s, (c !! i, c !! j)) of
+    (S 0, (1, 1)) -> S 0
+    (S 0, (0, 0)) -> S 0
+    (S 0, (1, 0)) -> S 1
+    (S 0, _     ) -> S 2
+    (S 1, _     ) -> S 1
+    (_  , _     ) -> S 2
 
 prod :: [a] -> [b] -> [(a, b)]
-prod xs [] = []
-prod [] ys = []
-prod (x : xs) ys = fmap (x,) ys ++ prod xs ys
+prod xs       [] = []
+prod []       ys = []
+prod (x : xs) ys = fmap (x, ) ys ++ prod xs ys
 
 data JunctionType = Conj | Disj deriving (Eq, Ord, Show)
 
 junction :: (Ord a) => JunctionType -> DFA c a -> DFA c a -> DFA c a
 junction jt (DFA states1 start1 accepts1 f1) (DFA states2 start2 accepts2 f2) =
   DFA states' start' accepts' f'
-  where
-    newStates = prod states1 states2
-    states' = Double <$> newStates
-    start' = Double (start1, start2)
-    accepts' =
-      if jt == Conj
-        then Double <$> prod accepts1 accepts2
-        else Double <$> filter (\(s, t) -> s `elem` accepts1 || t `elem` accepts2) newStates
-    f' (Double (s, t)) c = Double (f1 s c, f2 t c)
+ where
+  newStates = prod states1 states2
+  states'   = Double <$> newStates
+  start'    = Double (start1, start2)
+  accepts'  = if jt == Conj
+    then Double <$> prod accepts1 accepts2
+    else
+      Double
+        <$> filter (\(s, t) -> s `elem` accepts1 || t `elem` accepts2) newStates
+  f' (Double (s, t)) c = Double (f1 s c, f2 t c)
 
 conj :: (Ord a) => DFA c a -> DFA c a -> DFA c a
 conj = junction Conj
@@ -157,14 +273,11 @@ disj :: (Ord a) => DFA c a -> DFA c a -> DFA c a
 disj = junction Disj
 
 compl :: (Ord a) => DFA c a -> DFA c a
-compl (DFA states start accepts f) =
-  DFA states start (states L.\\ accepts) f
+compl (DFA states start accepts f) = DFA states start (states L.\\ accepts) f
 
 nondeterminize :: (Ord a) => DFA c a -> NFA c a
-nondeterminize (DFA states start accepts f) =
-  NFA states [start] accepts f'
-  where
-    f' s c = [f s c]
+nondeterminize (DFA states start accepts f) = NFA states [start] accepts f'
+  where f' s c = [f s c]
 
 change :: [a] -> Int -> a -> [a]
 change xs idx b = take idx xs ++ [b] ++ drop (idx + 1) xs
@@ -172,45 +285,36 @@ change xs idx b = take idx xs ++ [b] ++ drop (idx + 1) xs
 closure :: (Ord a) => NFA c a -> [c] -> [State a] -> [State a]
 closure nfa@(NFA states starts accepts f) cs initstates =
   let new = concatMap (\state -> concatMap (f state) cs) initstates
-   in if L.nub new L.\\ L.nub initstates /= []
+  in  if L.nub new L.\\ L.nub initstates /= []
         then closure nfa cs (L.nub $ new ++ initstates)
         else L.nub initstates
 
 existentialize :: (Ord a) => Int -> NFA [Int] a -> NFA [Int] a
-existentialize idx nfa@(NFA states starts accepts f) =
-  NFA states starts' accepts f'
-  where
-    zeroer = replicate 50 0
-    oneer = change zeroer idx 1
-    starts' = closure nfa [zeroer, oneer] starts
-    f' s c = f s (change c idx 0) ++ f s (change c idx 1)
+existentialize idx nfa@(NFA states starts accepts f) = NFA states
+                                                           starts'
+                                                           accepts
+                                                           f'
+ where
+  zeroer  = replicate 50 0
+  oneer   = change zeroer idx 1
+  starts' = closure nfa [zeroer, oneer] starts
+  f' s c = f s (change c idx 0) ++ f s (change c idx 1)
 
 powerset :: [a] -> [[a]]
-powerset [] = [[]]
+powerset []       = [[]]
 powerset (x : xs) = let rest = powerset xs in map (x :) rest ++ rest
 
 determinize :: (Ord a) => NFA c a -> DFA c a
-determinize (NFA states start accepts f) =
-  DFA states' start' accepts' f'
-  where
-    newStates = map L.sort $ powerset states
-    states' = Multi <$> newStates
-    start' = Multi $ L.sort start
-    accepts' = Multi <$> filter (\state' -> state' `L.intersect` accepts /= []) newStates
-    f' (Multi s) c = Multi $ L.nub $ L.sort $ concatMap (`f` c) s
+determinize (NFA states start accepts f) = DFA states' start' accepts' f'
+ where
+  newStates = map L.sort $ powerset states
+  states'   = Multi <$> newStates
+  start'    = Multi $ L.sort start
+  accepts' =
+    Multi <$> filter (\state' -> state' `L.intersect` accepts /= []) newStates
+  f' (Multi s) c = Multi $ L.nub $ L.sort $ concatMap (`f` c) s
 
-ncompl :: (Ord a) => NFA c a -> NFA c a
-ncompl = nondeterminize . compl . determinize
 
 chars :: Integer -> [[Int]]
 chars 0 = [[]]
-chars n =
-  let r = chars (n -1)
-   in map (1 :) r ++ map (0 :) r
-
-minimize :: (Ord a) => Integer -> NFA [Int] a -> NFA [Int] a
-minimize n nfa@(NFA _ starts accepts f) = NFA states' starts' accepts' f
-  where
-    states' = closure nfa (chars n) starts
-    starts' = starts `L.intersect` states'
-    accepts' = accepts `L.intersect` states'
+chars n = let r = chars (n - 1) in map (1 :) r ++ map (0 :) r