> {-# OPTIONS_HADDOCK show-extensions #-}
> {-|
> Module    : LTK.Decide.LTT
> Copyright : (c) 2019-2021 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 :: FSA n e -> Bool
isLTT = SynMon n e -> Bool
forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isLTTM (SynMon n e -> Bool) -> (FSA n e -> SynMon n e) -> FSA n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> SynMon n e
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 :: SynMon n e -> Bool
isLTTM = (SynMon n e -> Bool) -> (SynMon n e -> Bool) -> SynMon n e -> Bool
forall a. (a -> Bool) -> (a -> Bool) -> a -> Bool
both SynMon n e -> Bool
forall n e. (Ord n, Ord e) => FSA n e -> Bool
isSF SynMon n e -> Bool
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 :: FSA (n, [Symbol e]) e -> Bool
isSynMonOfLTT FSA (n, [Symbol e]) e
s = ((T n e, T n e) -> Bool) -> Set (T n e, T n e) -> Bool
forall (s :: * -> *) a. Collapsible s => (a -> Bool) -> s a -> Bool
allS (\(T n e
e,T n e
f) ->
>                         ((T n e, T n e, T n e) -> Bool)
-> Set (T n e, T n e, T n e) -> Bool
forall (s :: * -> *) a. Collapsible s => (a -> Bool) -> s a -> Bool
allS (\(T n e
a,T n e
b,T n e
u) ->
>                               FSA (n, [Symbol e]) e
-> T n e -> T n e -> T n e -> T n e -> T n e -> Bool
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 (n, [Symbol e]) e
s T n e
e T n e
f T n e
a T n e
u T n e
b
>                              ) (Set (T n e, T n e, T n e) -> Bool)
-> (Set (T n e) -> Set (T n e, T n e, T n e))
-> Set (T n e)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (T n e) -> Set (T n e, T n e, T n e)
forall a. Ord a => Set a -> Set (a, a, a)
triples (Set (T n e) -> Bool) -> Set (T n e) -> Bool
forall a b. (a -> b) -> a -> b
$ FSA (n, [Symbol e]) e -> Set (T n e)
forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA (n, [Symbol e]) e
s
>                        ) (Set (T n e, T n e) -> Bool)
-> (Set (T n e) -> Set (T n e, T n e)) -> Set (T n e) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (T n e) -> Set (T n e, T n e)
forall a. Ord a => Set a -> Set (a, a)
pairs (Set (T n e) -> Bool) -> Set (T n e) -> Bool
forall a b. (a -> b) -> a -> b
$ FSA (n, [Symbol e]) e -> Set (T n e)
forall n e. (Ord n, Ord e) => FSA (n, [Symbol e]) e -> Set (T n e)
idempotents FSA (n, [Symbol 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 :: 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
>     = FSA (S n e) e -> [Symbol e] -> T n e -> Set (T n e)
forall n e.
(Ord n, Ord e) =>
FSA n e -> [Symbol e] -> State n -> Set (State n)
follow FSA (S n e) e
s (T n e -> [Symbol e]
forall a c. State (a, c) -> c
g T n e
a [Symbol e] -> [Symbol e] -> [Symbol e]
forall a. [a] -> [a] -> [a]
++ T n e -> [Symbol e]
forall a c. State (a, c) -> c
g T n e
f [Symbol e] -> [Symbol e] -> [Symbol e]
forall a. [a] -> [a] -> [a]
++ T n e -> [Symbol e]
forall a c. State (a, c) -> c
g T n e
u [Symbol e] -> [Symbol e] -> [Symbol e]
forall a. [a] -> [a] -> [a]
++ T n e -> [Symbol e]
forall a c. State (a, c) -> c
g T n e
e [Symbol e] -> [Symbol e] -> [Symbol e]
forall a. [a] -> [a] -> [a]
++ T n e -> [Symbol e]
forall a c. State (a, c) -> c
g T n e
b [Symbol e] -> [Symbol e] -> [Symbol e]
forall a. [a] -> [a] -> [a]
++ T n e -> [Symbol e]
forall a c. State (a, c) -> c
g T n e
f) T n e
e Set (T n e) -> Set (T n e) -> Bool
forall a. Eq a => a -> a -> Bool
==
>       FSA (S n e) e -> [Symbol e] -> T n e -> Set (T n e)
forall n e.
(Ord n, Ord e) =>
FSA n e -> [Symbol e] -> State n -> Set (State n)
follow FSA (S n e) e
s (T n e -> [Symbol e]
forall a c. State (a, c) -> c
g T n e
b [Symbol e] -> [Symbol e] -> [Symbol e]
forall a. [a] -> [a] -> [a]
++ T n e -> [Symbol e]
forall a c. State (a, c) -> c
g T n e
f [Symbol e] -> [Symbol e] -> [Symbol e]
forall a. [a] -> [a] -> [a]
++ T n e -> [Symbol e]
forall a c. State (a, c) -> c
g T n e
u [Symbol e] -> [Symbol e] -> [Symbol e]
forall a. [a] -> [a] -> [a]
++ T n e -> [Symbol e]
forall a c. State (a, c) -> c
g T n e
e [Symbol e] -> [Symbol e] -> [Symbol e]
forall a. [a] -> [a] -> [a]
++ T n e -> [Symbol e]
forall a c. State (a, c) -> c
g T n e
a [Symbol e] -> [Symbol e] -> [Symbol e]
forall a. [a] -> [a] -> [a]
++ T n e -> [Symbol e]
forall a c. State (a, c) -> c
g T n e
f) T n e
e
>     where g :: State (a, c) -> c
g = (a, c) -> c
forall a b. (a, b) -> b
snd ((a, c) -> c) -> (State (a, c) -> (a, c)) -> State (a, c) -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State (a, c) -> (a, c)
forall n. State n -> n
nodeLabel

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