> {-# OPTIONS_HADDOCK show-extensions #-}
> {-|
> Module    : LTK.Decide.GLPT
> Copyright : (c) 2021-2023 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 :: 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.

> -- |True iff the given monoid is in \(\mathbf{M_e J}\).
> 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