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

> This module implements an algorithm to decide whether a given FSA
> has a semigroup both Commutative and Aperiodic (Acom).  This is
> the class that LTT localizes (Almeida, 1989).
>
> https://doi.org/10.1016/0022-4049(89)90124-2
>
> @since 1.1
> -}
> module LTK.Decide.Acom (isAcom, isAcomM, comTest) where

> import Data.Set (Set)
> import qualified Data.Set as Set

> import LTK.Decide.SF (isSFM)
> import LTK.FSA
> import LTK.Algebra

> type S n e = (n, [Symbol e])

> -- |True iff the automaton recognizes a \(\langle 1,t\rangle\)-LTT
> -- stringset.
> isAcom :: (Ord n, Ord e) => FSA n e -> Bool
> isAcom :: forall n e. (Ord n, Ord e) => FSA n e -> Bool
isAcom = forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isAcomM 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

> -- |True iff the monoid is aperiodic and commutative
> isAcomM :: (Ord n, Ord e) => SynMon n e -> Bool
> isAcomM :: forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isAcomM = forall a. (a -> Bool) -> (a -> Bool) -> a -> Bool
both forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isSFM (\SynMon n e
m -> forall n e.
(Ord n, Ord e) =>
SynMon n e -> Set (State (S [Maybe n] e)) -> Bool
comTest SynMon n e
m (forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states SynMon n e
m))

> -- |True iff the specified elements commute.
> comTest :: (Ord n, Ord e) =>
>           SynMon n e -> Set (State (S [Maybe n] e)) -> Bool
> comTest :: forall n e.
(Ord n, Ord e) =>
SynMon n e -> Set (State (S [Maybe n] e)) -> Bool
comTest SynMon n e
m Set (State (S [Maybe n] e))
qs
>     | forall a. Set a -> Int
Set.size (forall n e. FSA n e -> Set (State n)
initials SynMon n e
m) forall a. Eq a => a -> a -> Bool
/= Int
1 = forall a. Set a -> Bool
Set.null (forall n e. FSA n e -> Set (State n)
initials SynMon n e
m)
>     | Bool
otherwise = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ([Symbol e], [Symbol e]) -> Bool
commutes forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set ([Symbol e], [Symbol e])
p
>     where p :: Set ([Symbol e], [Symbol e])
p = forall a. Ord a => Set a -> Set (a, a)
pairs forall a b. (a -> b) -> a -> b
$ forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap (forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n. State n -> n
nodeLabel) Set (State (S [Maybe n] e))
qs
>           i :: State (S [Maybe n] e)
i = forall a. Set a -> a
Set.findMin forall a b. (a -> b) -> a -> b
$ forall n e. FSA n e -> Set (State n)
initials SynMon n e
m
>           commutes :: ([Symbol e], [Symbol e]) -> Bool
commutes ([Symbol e], [Symbol e])
x = forall n e.
(Ord n, Ord e) =>
FSA n e -> [Symbol e] -> State n -> Set (State n)
follow SynMon n e
m (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. [a] -> [a] -> [a]
(++) ([Symbol e], [Symbol e])
x) State (S [Maybe n] e)
i
>                        forall a. Eq a => a -> a -> Bool
== forall n e.
(Ord n, Ord e) =>
FSA n e -> [Symbol e] -> State n -> Set (State n)
follow SynMon n e
m (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. [a] -> [a] -> [a]
(++)) ([Symbol e], [Symbol e])
x) State (S [Maybe n] e)
i

> pairs :: Ord a => Set a -> Set (a, a)
> pairs :: forall a. Ord a => Set a -> Set (a, a)
pairs Set a
xs = forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (forall c a. Container c a => c -> c -> c
union forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a}. a -> Set (a, a)
f) forall c a. Container c a => c
empty Set a
xs
>     where f :: a -> Set (a, a)
f a
x = forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic ((,) a
x) Set a
xs