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

> import qualified Data.Set as Set

> import LTK.FSA
> import LTK.Algebra

> -- |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 = forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isMTDefM 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 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 = forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isMTRDefM 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 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 = forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isMTFM 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 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 = forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isMTGDM 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 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 SynMon n e
s = forall (t :: * -> *). Foldable t => t Bool -> Bool
and [T [Maybe n] e -> T [Maybe n] e -> Bool
f T [Maybe n] e
x T [Maybe n] e
y | T [Maybe n] e
x <- [T [Maybe n] e]
q, T [Maybe n] e
y <- [T [Maybe n] e]
q]
>     where q :: [T [Maybe n] e]
q = forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states SynMon n e
s
>           f :: T [Maybe n] e -> T [Maybe n] e -> Bool
f T [Maybe n] e
x T [Maybe n] e
y = let ye :: Set (T [Maybe n] e)
ye = forall n e.
(Ord n, Ord e) =>
FSA n e -> [Symbol e] -> State n -> Set (State n)
follow SynMon n e
s (forall {a} {c}. State (a, c) -> c
h forall a b. (a -> b) -> a -> b
$ forall n e. (Ord n, Ord e) => FSA (S n e) e -> T n e -> T n e
omega SynMon n e
s T [Maybe n] e
x) T [Maybe n] e
y
>                   in case forall a. Set a -> [a]
Set.toList Set (T [Maybe n] e)
ye
>                      of (T [Maybe n] e
z:[])  ->  Set (T [Maybe n] e)
ye 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
s (forall {a} {c}. State (a, c) -> c
h T [Maybe n] e
z) T [Maybe n] e
x
>                         [T [Maybe n] e]
_       ->  Bool
False
>           h :: State (a, c) -> c
h = forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n. State n -> n
nodeLabel

> -- |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 SynMon n e
s = forall (t :: * -> *). Foldable t => t Bool -> Bool
and [forall {a}. T [Maybe n] e -> State (a, [Symbol e]) -> Bool
f T [Maybe n] e
x T [Maybe n] e
y | T [Maybe n] e
x <- [T [Maybe n] e]
q, T [Maybe n] e
y <- [T [Maybe n] e]
q]
>     where q :: [T [Maybe n] e]
q = forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states SynMon n e
s
>           f :: T [Maybe n] e -> State (a, [Symbol e]) -> Bool
f T [Maybe n] e
x State (a, [Symbol e])
y = let ey :: Set (T [Maybe n] e)
ey = forall n e.
(Ord n, Ord e) =>
FSA n e -> [Symbol e] -> State n -> Set (State n)
follow SynMon n e
s (forall {a} {c}. State (a, c) -> c
h State (a, [Symbol e])
y) (forall n e. (Ord n, Ord e) => FSA (S n e) e -> T n e -> T n e
omega SynMon n e
s T [Maybe n] e
x)
>                   in case forall a. Set a -> [a]
Set.toList Set (T [Maybe n] e)
ey
>                      of (T [Maybe n] e
z:[])  ->  Set (T [Maybe n] e)
ey 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
s (forall {a} {c}. State (a, c) -> c
h T [Maybe n] e
x) T [Maybe n] e
z
>                         [T [Maybe n] e]
_       ->  Bool
False
>           h :: State (a, c) -> c
h = forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n. State n -> n
nodeLabel

> -- |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 SynMon n e
s = forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isMTDefM SynMon n e
s Bool -> Bool -> Bool
&& forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isMTRDefM SynMon n e
s

> -- |True iff the monoid 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.
> isMTGDM :: (Ord n, Ord e) => SynMon n e -> Bool
> isMTGDM :: forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isMTGDM SynMon n e
s = forall (t :: * -> *). Foldable t => t Bool -> Bool
and [State ([Maybe n], [Symbol e])
-> State ([Maybe n], [Symbol e])
-> State ([Maybe n], [Symbol e])
-> Bool
f State ([Maybe n], [Symbol e])
u State ([Maybe n], [Symbol e])
v State ([Maybe n], [Symbol e])
x | State ([Maybe n], [Symbol e])
u <- [State ([Maybe n], [Symbol e])]
q, State ([Maybe n], [Symbol e])
v <- [State ([Maybe n], [Symbol e])]
q, State ([Maybe n], [Symbol e])
x <- [State ([Maybe n], [Symbol e])]
q]
>     where q :: [State ([Maybe n], [Symbol e])]
q = forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states SynMon n e
s
>           f :: State ([Maybe n], [Symbol e])
-> State ([Maybe n], [Symbol e])
-> State ([Maybe n], [Symbol e])
-> Bool
f State ([Maybe n], [Symbol e])
u State ([Maybe n], [Symbol e])
v State ([Maybe n], [Symbol e])
x = let e :: State ([Maybe n], [Symbol e])
e = forall n e. (Ord n, Ord e) => FSA (S n e) e -> T n e -> T n e
omega SynMon n e
s State ([Maybe n], [Symbol e])
x
>                     in forall (s :: * -> *) a. Collapsible s => (a -> Bool) -> s a -> Bool
allS (State ([Maybe n], [Symbol e])
-> State ([Maybe n], [Symbol e])
-> State ([Maybe n], [Symbol e])
-> State ([Maybe n], [Symbol e])
-> Bool
g State ([Maybe n], [Symbol e])
u State ([Maybe n], [Symbol e])
v State ([Maybe n], [Symbol e])
x) [State ([Maybe n], [Symbol e])]
q
>                        Bool -> Bool -> Bool
&& forall n e.
(Ord n, Ord e) =>
FSA n e -> [Symbol e] -> State n -> Set (State n)
follow SynMon n e
s (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall {a} {c}. State (a, c) -> c
h [State ([Maybe n], [Symbol e])
u,State ([Maybe n], [Symbol e])
x,State ([Maybe n], [Symbol e])
v,State ([Maybe n], [Symbol e])
e]) State ([Maybe n], [Symbol e])
e
>                           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
s (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall {a} {c}. State (a, c) -> c
h [State ([Maybe n], [Symbol e])
u,State ([Maybe n], [Symbol e])
v,State ([Maybe n], [Symbol e])
e]) State ([Maybe n], [Symbol e])
e
>           g :: State ([Maybe n], [Symbol e])
-> State ([Maybe n], [Symbol e])
-> State ([Maybe n], [Symbol e])
-> State ([Maybe n], [Symbol e])
-> Bool
g State ([Maybe n], [Symbol e])
u State ([Maybe n], [Symbol e])
v State ([Maybe n], [Symbol e])
x State ([Maybe n], [Symbol e])
z = let x' :: State ([Maybe n], [Symbol e])
x' = forall n e. (Ord n, Ord e) => FSA (S n e) e -> T n e -> T n e
omega SynMon n e
s State ([Maybe n], [Symbol e])
x
>                           z' :: State ([Maybe n], [Symbol e])
z' = forall n e. (Ord n, Ord e) => FSA (S n e) e -> T n e -> T n e
omega SynMon n e
s State ([Maybe n], [Symbol e])
z
>                       in forall n e.
(Ord n, Ord e) =>
FSA n e -> [Symbol e] -> State n -> Set (State n)
follow SynMon n e
s (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall {a} {c}. State (a, c) -> c
h [State ([Maybe n], [Symbol e])
u,State ([Maybe n], [Symbol e])
x,State ([Maybe n], [Symbol e])
z,State ([Maybe n], [Symbol e])
v,State ([Maybe n], [Symbol e])
z']) State ([Maybe n], [Symbol e])
x'
>                          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
s (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall {a} {c}. State (a, c) -> c
h [State ([Maybe n], [Symbol e])
u,State ([Maybe n], [Symbol e])
z,State ([Maybe n], [Symbol e])
x,State ([Maybe n], [Symbol e])
v,State ([Maybe n], [Symbol e])
z']) State ([Maybe n], [Symbol e])
x'
>           h :: State (a, c) -> c
h = forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n. State n -> n
nodeLabel