> {-# OPTIONS_HADDOCK show-extensions #-}
>
> module LTK.Decide.GLPT (isGLPT, isGLPTM) where
> import qualified Data.Set as Set
> import LTK.FSA
> import LTK.Algebra
>
>
>
>
> isGLPT :: (Ord n, Ord e) => FSA n e -> Bool
> isGLPT :: forall n e. (Ord n, Ord e) => FSA n e -> Bool
isGLPT = forall n e. (Ord n, Ord e) => FSA (n, [Symbol e]) e -> Bool
isGLPTM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e n.
(Ord e, Ord n) =>
FSA n e -> FSA ([Maybe n], [Symbol e]) e
syntacticMonoid
J-trivial means MaM = MbM in all and only those cases where a=b
We're asking if X=e*M_e*e is J-trivial
That is, if for all a,b in X, XaX=XbX iff a=b.
It does not appear that a shortcut like that used to test for
local J-triviality is viable. If it turns out to be, then this
file will shrink dramatically and this test will speed up quite
a bit.
>
> isGLPTM :: (Ord n, Ord e) => FSA (n, [Symbol e]) e -> Bool
> isGLPTM :: forall n e. (Ord n, Ord e) => FSA (n, [Symbol e]) e -> Bool
isGLPTM FSA (n, [Symbol e]) e
m = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all T n e -> Bool
f forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set (T n e)
i
> where i :: Set (T n e)
i = forall n e. (Ord n, Ord e) => FSA (n, [Symbol e]) e -> Set (T n e)
idempotents FSA (n, [Symbol e]) e
m
> x :: T n e -> [T n e]
x = forall a. Set a -> [a]
Set.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n e. (Ord n, Ord e) => FSA (S n e) e -> T n e -> Set (T n e)
emee FSA (n, [Symbol e]) e
m
> f :: T n e -> Bool
f T n e
e = forall a. Eq a => [a] -> Bool
isDistinct forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall {a}. T n e -> State (a, [Symbol e]) -> Set (T n e)
g T n e
e) forall a b. (a -> b) -> a -> b
$ T n e -> [T n e]
x T n e
e
> g :: T n e -> State (a, [Symbol e]) -> Set (T n e)
g T n e
e State (a, [Symbol e])
h = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions
> [forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall n e.
(Ord n, Ord e) =>
FSA n e -> [Symbol e] -> State n -> Set (State n)
follow FSA (n, [Symbol e]) e
m) T n e
qi forall a b. (a -> b) -> a -> b
$ forall {a} {c}. State (a, c) -> c
label T n e
a forall a. [a] -> [a] -> [a]
++ forall {a} {c}. State (a, c) -> c
label State (a, [Symbol e])
h forall a. [a] -> [a] -> [a]
++ forall {a} {c}. State (a, c) -> c
label T n e
b
> | T n e
a <- T n e -> [T n e]
x T n e
e, T n e
b <- T n e -> [T n e]
x T n e
e]
> qi :: T n e
qi = forall a. Set a -> a
Set.findMin forall a b. (a -> b) -> a -> b
$ forall n e. FSA n e -> Set (State n)
initials FSA (n, [Symbol e]) e
m
> label :: State (a, c) -> c
label = forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n. State n -> n
nodeLabel
> isDistinct :: Eq a => [a] -> Bool
> isDistinct :: forall a. Eq a => [a] -> Bool
isDistinct [] = Bool
True
> isDistinct (a
x:[a]
xs) = a
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [a]
xs Bool -> Bool -> Bool
&& forall a. Eq a => [a] -> Bool
isDistinct [a]
xs