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

> This module implement algorithms to decide whether a given FSA
> has a given dot depth.  Currently, only dot depth one is testable,
> using the equations presented by Knast's 1983 "A semigroup
> characterization of dot-depth one languages"
> https://doi.org/10.1051/ita/1983170403211
>
> @since 1.2
> -}
> module LTK.Decide.DotDepth (isDot1, isDot1M, isDot1s) where

> import Data.Representation.FiniteSemigroup
> import qualified Data.IntSet as IntSet

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

> -- |True iff the automaton recognizes a dot-depth one stringset.
> isDot1 :: (Ord n, Ord e) => FSA n e -> Bool
> isDot1 :: forall n e. (Ord n, Ord e) => FSA n e -> Bool
isDot1 = GeneratedAction -> Bool
forall s. FiniteSemigroupRep s => s -> Bool
isDot1s (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 recognizes a dot-depth one stringset.
> isDot1M :: (Ord n, Ord e) => SynMon n e -> Bool
> isDot1M :: forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isDot1M = FSA ([Maybe n], [Symbol e]) e -> Bool
forall n e. (Ord n, Ord e) => FSA n e -> Bool
isDot1

> -- |True iff the semigroup recognizes a dot-depth one stringset.
> -- That is, for idempotents \(e\) and \(f\) and elements \(a\),
> -- \(b\), \(c\) and \(d\), it holds that
> -- \((eafb)^{\omega}eafde(cfde)^{\omega}
> -- = (eafb)^{\omega}e(cfde)^{\omega}\).
> isDot1s :: FiniteSemigroupRep s => s -> Bool
> isDot1s :: forall s. FiniteSemigroupRep s => s -> Bool
isDot1s s
s = ((Int, Int, Int, Int, Int, Int) -> Bool)
-> [(Int, Int, Int, Int, Int, Int)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Int, Int, Int, Int, Int, Int) -> Bool
go [ (Int
e,Int
f,Int
a,Int
b,Int
c,Int
d)
>                    | Int
e <- [Int]
is, Int
f <- [Int]
is, Int
a <- [Int]
xs
>                    , Int
b <- [Int]
xs, Int
c <- [Int]
xs, Int
d <- [Int]
xs]
>     where t :: FSMult
t = s -> FSMult
forall a. FiniteSemigroupRep a => a -> FSMult
fstable s
s
>           is :: [Int]
is = IntSet -> [Int]
IntSet.toList (IntSet -> [Int]) -> IntSet -> [Int]
forall a b. (a -> b) -> a -> b
$ FSMult -> IntSet
forall s. FiniteSemigroupRep s => s -> IntSet
idempotents FSMult
t
>           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, Int, Int, Int, Int) -> Bool
go ~(Int
e,Int
f,Int
a,Int
b,Int
c,Int
d)
>               = let p1 :: Int
p1 = [Int] -> Int
eval [FSMult -> Int -> Int
forall s. FiniteSemigroupRep s => s -> Int -> Int
omega FSMult
t (Int -> Int) -> Int -> Int
forall a b. (a -> b) -> a -> b
$ [Int] -> Int
eval [Int
e,Int
a,Int
f,Int
b], Int
e]
>                     p2 :: Int
p2 = [Int] -> Int
eval [Int
e, FSMult -> Int -> Int
forall s. FiniteSemigroupRep s => s -> Int -> Int
omega FSMult
t (Int -> Int) -> Int -> Int
forall a b. (a -> b) -> a -> b
$ [Int] -> Int
eval [Int
c,Int
f,Int
d,Int
e]]
>                 in [Int] -> Int
eval [Int
p1,Int
a,Int
f,Int
d,Int
p2] Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Int] -> Int
eval [Int
p1,Int
p2]