> {-# OPTIONS_HADDOCK show-extensions #-}
>
> 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)
>
> 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
>
>
>
> 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