> {-# OPTIONS_HADDOCK show-extensions #-}
> {-|
> Module    : LTK.Decide.LTT
> Copyright : (c) 2019,2021-2022 Dakotah Lambert
> License   : MIT

> This module implements an algorithm to decide whether a given FSA
> is Locally Testable (LTT) based on the semigroup characterization
> of Beaquier and Pin from their 1989 work
> "Factors of Words".
>
> @since 0.2
> -}
> module LTK.Decide.LTT (isLTT, isLTTM) where

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

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

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

> -- |True iff the automaton recognizes an LTT stringset.
> isLTT :: (Ord n, Ord e) => FSA n e -> Bool
> isLTT :: forall n e. (Ord n, Ord e) => FSA n e -> Bool
isLTT = forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isLTTM 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 recognizes an LTT stringset.
> --
> -- @since 1.0
> isLTTM :: (Ord n, Ord e) => SynMon n e -> Bool
> isLTTM :: forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isLTTM = forall a. (a -> Bool) -> (a -> Bool) -> a -> Bool
both forall n e. (Ord n, Ord e) => FSA n e -> Bool
isSF forall n e. (Ord n, Ord e) => FSA (n, [Symbol e]) e -> Bool
isSynMonOfLTT

A semigroup (S) [e.g. the syntactic semigroup] is
locally threshold testable iff
for all idempotent e and f, and for all a,b,u it holds that
eafuebf = ebfueaf.

> isSynMonOfLTT :: (Ord n, Ord e) => FSA (n, [Symbol e]) e -> Bool
> isSynMonOfLTT :: forall n e. (Ord n, Ord e) => FSA (n, [Symbol e]) e -> Bool
isSynMonOfLTT FSA (S n e) e
s = forall (s :: * -> *) a. Collapsible s => (a -> Bool) -> s a -> Bool
allS (\(T n e
e,T n e
f) ->
>                         forall (s :: * -> *) a. Collapsible s => (a -> Bool) -> s a -> Bool
allS (\(T n e
a,T n e
b,T n e
u) ->
>                               forall n e.
(Ord n, Ord e) =>
FSA (S n e) e -> T n e -> T n e -> T n e -> T n e -> T n e -> Bool
lttTest FSA (S n e) e
s T n e
e T n e
f T n e
a T n e
u T n e
b
>                              ) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => Set a -> Set (a, a, a)
triples forall a b. (a -> b) -> a -> b
$ forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA (S n e) e
s
>                        ) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => Set a -> Set (a, a)
pairs forall a b. (a -> b) -> a -> b
$ forall n e. (Ord n, Ord e) => FSA (n, [Symbol e]) e -> Set (T n e)
idempotents FSA (S n e) e
s

> lttTest :: (Ord n, Ord e) =>
>            FSA (S n e) e ->
>            T n e -> T n e -> T n e -> T n e -> T n e ->
>            Bool
> lttTest :: forall n e.
(Ord n, Ord e) =>
FSA (S n e) e -> T n e -> T n e -> T n e -> T n e -> T n e -> Bool
lttTest FSA (S n e) e
s State (S n e)
e State (S n e)
f State (S n e)
a State (S n e)
u State (S n e)
b
>     = forall n e.
(Ord n, Ord e) =>
FSA n e -> [Symbol e] -> State n -> Set (State n)
follow FSA (S n e) e
s (forall {a} {c}. State (a, c) -> c
g State (S n e)
a forall a. [a] -> [a] -> [a]
++ forall {a} {c}. State (a, c) -> c
g State (S n e)
f forall a. [a] -> [a] -> [a]
++ forall {a} {c}. State (a, c) -> c
g State (S n e)
u forall a. [a] -> [a] -> [a]
++ forall {a} {c}. State (a, c) -> c
g State (S n e)
e forall a. [a] -> [a] -> [a]
++ forall {a} {c}. State (a, c) -> c
g State (S n e)
b forall a. [a] -> [a] -> [a]
++ forall {a} {c}. State (a, c) -> c
g State (S n e)
f) State (S n 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 FSA (S n e) e
s (forall {a} {c}. State (a, c) -> c
g State (S n e)
b forall a. [a] -> [a] -> [a]
++ forall {a} {c}. State (a, c) -> c
g State (S n e)
f forall a. [a] -> [a] -> [a]
++ forall {a} {c}. State (a, c) -> c
g State (S n e)
u forall a. [a] -> [a] -> [a]
++ forall {a} {c}. State (a, c) -> c
g State (S n e)
e forall a. [a] -> [a] -> [a]
++ forall {a} {c}. State (a, c) -> c
g State (S n e)
a forall a. [a] -> [a] -> [a]
++ forall {a} {c}. State (a, c) -> c
g State (S n e)
f) State (S n e)
e
>     where g :: State (a, c) -> c
g = forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n. State n -> n
nodeLabel

> 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

> triples :: Ord a => Set a -> Set (a, a, a)
> triples :: forall a. Ord a => Set a -> Set (a, a, a)
triples 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 {b} {c}. (b, c) -> Set (a, b, c)
f) forall c a. Container c a => c
empty (forall a. Ord a => Set a -> Set (a, a)
pairs Set a
xs)
>     where f :: (b, c) -> Set (a, b, c)
f (b
a, c
b) = forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic (\a
x -> (a
x, b
a, c
b)) Set a
xs