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

> The Boolean closure of tier-based locally V is a subclass
> of the Meification of V.  For instance, multiple-tier-based
> definite is a proper subclass of the L-trivial languages.
> This module includes decision algorithms for some classes
> of multiple-tier-based languages.
>
> The equations given here are adapted from Almeida's (1995)
> "Finite Semigroups and Universal Algebra"
> https://doi.org/10.1142/2481
> as they are simpler than the equivalent ones I had found independently.
>
> @since 1.1
> -}
> module LTK.Decide.Multitier
>     ( isMTF, isMTDef, isMTRDef, isMTGD
>     , isMTFM, isMTDefM, isMTRDefM, isMTGDM
>     , isMTFs, isMTDefs, isMTRDefs, isMTGDs
>     ) where

> import Data.Representation.FiniteSemigroup

> import LTK.FSA
> import LTK.Algebra(SynMon)

> -- |True iff the given language is multiple-tier-based definite.
> isMTDef :: (Ord n, Ord e) => FSA n e -> Bool
> isMTDef :: forall n e. (Ord n, Ord e) => FSA n e -> Bool
isMTDef = GeneratedAction -> Bool
forall s. FiniteSemigroupRep s => s -> Bool
isMTDefs (GeneratedAction -> Bool)
-> (FSA n e -> GeneratedAction) -> FSA n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> GeneratedAction
forall n e. (Ord n, Ord e) => FSA n e -> GeneratedAction
syntacticSemigroup

> -- |True iff the given language is multiple-tier-based reverse-definite.
> isMTRDef :: (Ord n, Ord e) => FSA n e -> Bool
> isMTRDef :: forall n e. (Ord n, Ord e) => FSA n e -> Bool
isMTRDef = GeneratedAction -> Bool
forall s. FiniteSemigroupRep s => s -> Bool
isMTRDefs (GeneratedAction -> Bool)
-> (FSA n e -> GeneratedAction) -> FSA n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> GeneratedAction
forall n e. (Ord n, Ord e) => FSA n e -> GeneratedAction
syntacticSemigroup

> -- |True iff the given language is multiple-tier-based (co)finite.
> isMTF :: (Ord n, Ord e) => FSA n e -> Bool
> isMTF :: forall n e. (Ord n, Ord e) => FSA n e -> Bool
isMTF = GeneratedAction -> Bool
forall s. FiniteSemigroupRep s => s -> Bool
isMTFs (GeneratedAction -> Bool)
-> (FSA n e -> GeneratedAction) -> FSA n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> GeneratedAction
forall n e. (Ord n, Ord e) => FSA n e -> GeneratedAction
syntacticSemigroup

> -- |True iff the given language is multiple-tier-based
> -- generalized-definite.
> isMTGD :: (Ord n, Ord e) => FSA n e -> Bool
> isMTGD :: forall n e. (Ord n, Ord e) => FSA n e -> Bool
isMTGD = GeneratedAction -> Bool
forall s. FiniteSemigroupRep s => s -> Bool
isMTGDs (GeneratedAction -> Bool)
-> (FSA n e -> GeneratedAction) -> FSA n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> GeneratedAction
forall n e. (Ord n, Ord e) => FSA n e -> GeneratedAction
syntacticSemigroup

> -- |True iff the monoid satisfies \(xyx^{\omega}=yx^{\omega}\).
> isMTDefM :: (Ord n, Ord e) => SynMon n e -> Bool
> isMTDefM :: forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isMTDefM = FSA ([Maybe n], [Symbol e]) e -> Bool
forall n e. (Ord n, Ord e) => FSA n e -> Bool
isMTDef

> -- |True iff the semigroup satisifes \(xyx^{\omega}=yx^{\omega}\).
> --
> -- @since 1.2
> isMTDefs :: FiniteSemigroupRep s => s -> Bool
> isMTDefs :: forall s. FiniteSemigroupRep s => s -> Bool
isMTDefs s
s = ((Int, Int) -> Bool) -> [(Int, Int)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Int -> Int -> Bool) -> (Int, Int) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Int -> Int -> Bool
go) [(Int
a,Int
b) | Int
a <- [Int]
xs, Int
b <- [Int]
xs]
>     where t :: FSMult
t = s -> FSMult
forall a. FiniteSemigroupRep a => a -> FSMult
fstable s
s
>           xs :: [Int]
xs = [Int
0 .. FSMult -> Int
forall a. FiniteSemigroupRep a => a -> Int
fssize FSMult
t Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
>           eval :: [Int] -> Int
eval = (Int -> Int -> Int) -> [Int] -> Int
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (FSMult -> Int -> Int -> Int
forall a. FiniteSemigroupRep a => a -> Int -> Int -> Int
fsappend FSMult
t)
>           go :: Int -> Int -> Bool
go Int
x Int
y = let yx' :: Int
yx' = [Int] -> Int
eval [Int
y,FSMult -> Int -> Int
forall s. FiniteSemigroupRep s => s -> Int -> Int
omega FSMult
t Int
x] in [Int] -> Int
eval [Int
x,Int
yx'] Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
yx'

> -- |True iff the monoid satisfies \(x^{\omega}yx=x^{\omega}y\).
> isMTRDefM :: (Ord n, Ord e) => SynMon n e -> Bool
> isMTRDefM :: forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isMTRDefM = FSA ([Maybe n], [Symbol e]) e -> Bool
forall n e. (Ord n, Ord e) => FSA n e -> Bool
isMTRDef

> -- |True iff the semigroup satisifes \(x^{\omega}yx=x^{\omega}y\).
> --
> -- @since 1.2
> isMTRDefs :: FiniteSemigroupRep s => s -> Bool
> isMTRDefs :: forall s. FiniteSemigroupRep s => s -> Bool
isMTRDefs = FSMult -> Bool
forall s. FiniteSemigroupRep s => s -> Bool
isMTDefs (FSMult -> Bool) -> (s -> FSMult) -> s -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> FSMult
forall a. FiniteSemigroupRep a => a -> FSMult
dual

> -- |True iff the monoid is aperiodic and satisfies
> -- \(x^{\omega}y=yx^{\omega}\).
> isMTFM :: (Ord n, Ord e) => SynMon n e -> Bool
> isMTFM :: forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isMTFM = FSA ([Maybe n], [Symbol e]) e -> Bool
forall n e. (Ord n, Ord e) => FSA n e -> Bool
isMTF

> -- |True iff the semigroup is aperiodic and satisfies
> -- \(x^{\omega}y=yx^{\omega}\).
> --
> -- @since 1.2
> isMTFs :: FiniteSemigroupRep s => s -> Bool
> isMTFs :: forall s. FiniteSemigroupRep s => s -> Bool
isMTFs = (s -> Bool) -> (s -> Bool) -> s -> Bool
forall a. (a -> Bool) -> (a -> Bool) -> a -> Bool
both s -> Bool
forall s. FiniteSemigroupRep s => s -> Bool
isMTDefs s -> Bool
forall s. FiniteSemigroupRep s => s -> Bool
isMTRDefs

> -- |True iff the monoid satisfies 'isMTGDs'.
> isMTGDM :: (Ord n, Ord e) => SynMon n e -> Bool
> isMTGDM :: forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isMTGDM = FSA ([Maybe n], [Symbol e]) e -> Bool
forall n e. (Ord n, Ord e) => FSA n e -> Bool
isMTGD

> -- |True iff the semigroup satisfies
> -- \(x^{\omega}uxvx^{\omega}=x^{\omega}uvx^{\omega}\)
> -- and \(x^{\omega}uxzvz^{\omega}=x^{\omega}uzxvz^{\omega}\).
> -- Thanks to Almeida (1995) for the simplification.
> --
> -- @since 1.2
> isMTGDs :: FiniteSemigroupRep s => s -> Bool
> isMTGDs :: forall s. FiniteSemigroupRep s => s -> Bool
isMTGDs s
s = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Int -> Int -> Int -> Bool
f Int
u Int
v Int
x | Int
u <- [Int]
xs, Int
v <- [Int]
xs, Int
x <- [Int]
xs]
>     where t :: FSMult
t = s -> FSMult
forall a. FiniteSemigroupRep a => a -> FSMult
fstable s
s
>           eval :: [Int] -> Int
eval = (Int -> Int -> Int) -> [Int] -> Int
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (FSMult -> Int -> Int -> Int
forall a. FiniteSemigroupRep a => a -> Int -> Int -> Int
fsappend FSMult
t)
>           xs :: [Int]
xs = [Int
0 .. s -> Int
forall a. FiniteSemigroupRep a => a -> Int
fssize s
s Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
>           f :: Int -> Int -> Int -> Bool
f Int
u Int
v Int
x = let x' :: Int
x' = FSMult -> Int -> Int
forall s. FiniteSemigroupRep s => s -> Int -> Int
omega FSMult
t Int
x
>                         x'u :: Int
x'u = [Int] -> Int
eval [Int
x', Int
u]
>                         vx' :: Int
vx' = [Int] -> Int
eval [Int
v, Int
x']
>                     in [Int] -> Int
eval [Int
x'u,Int
x,Int
vx'] Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Int] -> Int
eval [Int
x'u,Int
vx']
>                        Bool -> Bool -> Bool
&& (Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Int -> Int -> Int -> Int -> Bool
g Int
u Int
v Int
x) [Int]
xs
>           g :: Int -> Int -> Int -> Int -> Bool
g Int
u Int
v Int
x Int
z = let x'u :: Int
x'u = [Int] -> Int
eval [FSMult -> Int -> Int
forall s. FiniteSemigroupRep s => s -> Int -> Int
omega FSMult
t Int
x, Int
u]
>                           vz' :: Int
vz' = [Int] -> Int
eval [Int
v, FSMult -> Int -> Int
forall s. FiniteSemigroupRep s => s -> Int -> Int
omega FSMult
t Int
z]
>                       in [Int] -> Int
eval [Int
x'u,Int
x,Int
z,Int
vz'] Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Int] -> Int
eval [Int
x'u,Int
z,Int
x,Int
vz']