> {-# OPTIONS_HADDOCK show-extensions #-}
>
> module LTK.Decide.FO2 (isFO2, isFO2B, isFO2BF, isFO2S,
> isFO2M, isFO2BM, isFO2BFM, isFO2SM,
> isFO2s, isFO2Bs, isFO2Ss) where
> import Data.Representation.FiniteSemigroup
> import LTK.FSA
> import LTK.Algebra(SynMon,emblock)
>
>
> isFO2 :: (Ord n, Ord e) => FSA n e -> Bool
> isFO2 :: forall n e. (Ord n, Ord e) => FSA n e -> Bool
isFO2 = GeneratedAction -> Bool
forall s. FiniteSemigroupRep s => s -> Bool
isFO2s (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
>
> isFO2M :: (Ord n, Ord e) => SynMon n e -> Bool
> isFO2M :: forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isFO2M = FSA ([Maybe n], [Symbol e]) e -> Bool
forall n e. (Ord n, Ord e) => FSA n e -> Bool
isFO2
>
>
>
> isFO2s :: FiniteSemigroupRep s => s -> Bool
> isFO2s :: forall s. FiniteSemigroupRep s => s -> Bool
isFO2s = s -> Bool
forall s. FiniteSemigroupRep s => s -> Bool
isDA
A language is FO2[<,+1]-definable iff
for all idempotents e of its semigroup (not monoid) S,
the subsemigroup eSe corresponds to something FO2[<]-definable
>
>
> isFO2S :: (Ord n, Ord e) => FSA n e -> Bool
> isFO2S :: forall n e. (Ord n, Ord e) => FSA n e -> Bool
isFO2S = GeneratedAction -> Bool
forall s. FiniteSemigroupRep s => s -> Bool
isFO2Ss (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
>
>
> isFO2SM :: (Ord n, Ord e) => SynMon n e -> Bool
> isFO2SM :: forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isFO2SM = FSA ([Maybe n], [Symbol e]) e -> Bool
forall n e. (Ord n, Ord e) => FSA n e -> Bool
isFO2S
>
>
>
>
> isFO2Ss :: FiniteSemigroupRep s => s -> Bool
> isFO2Ss :: forall s. FiniteSemigroupRep s => s -> Bool
isFO2Ss = (FSMult -> Bool) -> s -> Bool
forall s. FiniteSemigroupRep s => (FSMult -> Bool) -> s -> Bool
locally FSMult -> Bool
forall s. FiniteSemigroupRep s => s -> Bool
isDA
A syntactic monoid represents an FO2[<]-definable language
iff for all elements x, y, and z it is the case that
(xyz)^{\omega}*y*(xyz)^{\omega} = (xyz)^{\omega}, where
s^{\omega} is the unique element where s^{\omega}*s = s^{\omega}.
For betweenness:
A language is representable in FO2[<,bet] iff its syntactic monoid
is in MeDA.
>
>
>
>
>
>
>
> isFO2B :: (Ord n, Ord e) => FSA n e -> Bool
> isFO2B :: forall n e. (Ord n, Ord e) => FSA n e -> Bool
isFO2B = GeneratedAction -> Bool
forall s. FiniteSemigroupRep s => s -> Bool
isFO2Bs (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
>
> isFO2BM :: (Ord n, Ord e) => SynMon n e -> Bool
> isFO2BM :: forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isFO2BM = FSA ([Maybe n], [Symbol e]) e -> Bool
forall n e. (Ord n, Ord e) => FSA n e -> Bool
isFO2B
>
>
>
>
> isFO2Bs :: FiniteSemigroupRep s => s -> Bool
> isFO2Bs :: forall s. FiniteSemigroupRep s => s -> Bool
isFO2Bs = (FSMult -> Bool) -> [FSMult] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all FSMult -> Bool
forall s. FiniteSemigroupRep s => s -> Bool
isDA ([FSMult] -> Bool) -> (s -> [FSMult]) -> s -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> [FSMult]
forall s. FiniteSemigroupRep s => s -> [FSMult]
emee
>
>
>
>
>
>
> isFO2BF :: (Ord n, Ord e) => FSA n e -> Bool
> isFO2BF :: forall n e. (Ord n, Ord e) => FSA n e -> Bool
isFO2BF = SynMon n e -> Bool
forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isFO2BFM (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
>
>
>
> isFO2BFM :: (Ord n, Ord e) => SynMon n e -> Bool
> isFO2BFM :: forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isFO2BFM = SynMon Integer Integer -> Bool
forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isFO2BM (SynMon Integer Integer -> Bool)
-> (SynMon n e -> SynMon Integer Integer) -> SynMon n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SynMon n e -> SynMon Integer Integer
forall n e. (Ord n, Ord e) => SynMon n e -> SynMon Integer Integer
emblock