> {-# OPTIONS_HADDOCK show-extensions #-}
> {-|
> Module    : LTK.Decide.GLPT
> Copyright : (c) 2021 Dakotah Lambert
> License   : MIT

> This module implements an algorithm to decide whether a syntactic
> semigroup \(S\) is, on certain submonoids, Piecewise Testable (MePT).
> This is the case iff for each of its idempotents \(e\) it holds that
> \(eXe\) is \(\mathcal{J}\)-trivial, where X is the set generated by
> {ege : ugv=e for some u,v}.
>
> @since 1.0
> -}
> module LTK.Decide.GLPT (isGLPT, isGLPTM) where

> import qualified Data.Set as Set

> import LTK.FSA
> import LTK.Algebra

> -- |True iff the syntactic monoid of the automaton is in
> -- \(\mathbf{M_e J}\).
> -- This is a generalization of LPT in the same way that
> -- GLT is a generalization of LT.
> isGLPT :: (Ord n, Ord e) => FSA n e -> Bool
> isGLPT :: FSA n e -> Bool
isGLPT = FSA ([Maybe n], [Symbol e]) e -> Bool
forall n e. (Ord n, Ord e) => FSA (n, [Symbol e]) e -> Bool
isGLPTM (FSA ([Maybe n], [Symbol e]) e -> Bool)
-> (FSA n e -> FSA ([Maybe n], [Symbol e]) e) -> FSA n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> FSA ([Maybe n], [Symbol e]) e
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.

> -- |True iff the given monoid is in \(\mathbf{M_e J}\).
> isGLPTM :: (Ord n, Ord e) => FSA (n, [Symbol e]) e -> Bool
> isGLPTM :: FSA (n, [Symbol e]) e -> Bool
isGLPTM FSA (n, [Symbol e]) e
m = (T n e -> Bool) -> [T n e] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all T n e -> Bool
f ([T n e] -> Bool) -> [T n e] -> Bool
forall a b. (a -> b) -> a -> b
$ Set (T n e) -> [T n e]
forall a. Set a -> [a]
Set.toList Set (T n e)
i
>     where i :: Set (T n e)
i = FSA (n, [Symbol e]) e -> Set (T n e)
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 = Set (T n e) -> [T n e]
forall a. Set a -> [a]
Set.toList (Set (T n e) -> [T n e])
-> (T n e -> Set (T n e)) -> T n e -> [T n e]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA (n, [Symbol e]) e -> T n e -> Set (T n e)
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 = [Set (T n e)] -> Bool
forall a. Eq a => [a] -> Bool
isDistinct ([Set (T n e)] -> Bool)
-> ([T n e] -> [Set (T n e)]) -> [T n e] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (T n e -> Set (T n e)) -> [T n e] -> [Set (T n e)]
forall a b. (a -> b) -> [a] -> [b]
map (T n e -> T n e -> Set (T n e)
forall a. T n e -> State (a, [Symbol e]) -> Set (T n e)
g T n e
e) ([T n e] -> Bool) -> [T n e] -> Bool
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 = [Set (T n e)] -> Set (T n e)
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set (T n e)] -> Set (T n e)) -> [Set (T n e)] -> Set (T n e)
forall a b. (a -> b) -> a -> b
$ ([Symbol e] -> Set (T n e)) -> [[Symbol e]] -> [Set (T n e)]
forall a b. (a -> b) -> [a] -> [b]
map (([Symbol e] -> T n e -> Set (T n e))
-> T n e -> [Symbol e] -> Set (T n e)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (FSA (n, [Symbol e]) e -> [Symbol e] -> T n e -> Set (T n e)
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)
>                   [T n e -> [Symbol e]
forall a c. State (a, c) -> c
label T n e
a [Symbol e] -> [Symbol e] -> [Symbol e]
forall a. [a] -> [a] -> [a]
++ State (a, [Symbol e]) -> [Symbol e]
forall a c. State (a, c) -> c
label State (a, [Symbol e])
h [Symbol e] -> [Symbol e] -> [Symbol e]
forall a. [a] -> [a] -> [a]
++ T n e -> [Symbol e]
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 = Set (T n e) -> T n e
forall a. Set a -> a
Set.findMin (Set (T n e) -> T n e) -> Set (T n e) -> T n e
forall a b. (a -> b) -> a -> b
$ FSA (n, [Symbol e]) e -> Set (T n e)
forall n e. FSA n e -> Set (State n)
initials FSA (n, [Symbol e]) e
m
>           label :: State (a, c) -> c
label = (a, c) -> c
forall a b. (a, b) -> b
snd ((a, c) -> c) -> (State (a, c) -> (a, c)) -> State (a, c) -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State (a, c) -> (a, c)
forall n. State n -> n
nodeLabel

> isDistinct :: Eq a => [a] -> Bool
> isDistinct :: [a] -> Bool
isDistinct [] = Bool
True
> isDistinct (a
x:[a]
xs) = Bool -> Bool
not (a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem a
x [a]
xs) Bool -> Bool -> Bool
&& [a] -> Bool
forall a. Eq a => [a] -> Bool
isDistinct [a]
xs