> {-# OPTIONS_HADDOCK show-extensions #-}
>
> module LTK.Decide.FO2 (isFO2, isFO2B, isFO2BF, isFO2S,
> isFO2M, isFO2BM, isFO2BFM, isFO2SM) where
> import Data.Set (Set)
> import qualified Data.Set as Set
> import LTK.FSA
> import LTK.Algebra
> type S n e = (n, [Symbol e])
>
>
> isFO2 :: (Ord n, Ord e) => FSA n e -> Bool
> isFO2 :: forall n e. (Ord n, Ord e) => FSA n e -> Bool
isFO2 = forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isFO2M 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
>
> isFO2M :: (Ord n, Ord e) => SynMon n e -> Bool
> isFO2M :: forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isFO2M = forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall n e.
(Ord n, Ord e) =>
SynMon n e -> Set (State (S [Maybe n] e)) -> Bool
fo2test forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a. a -> a
id) (,)
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 = forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isFO2SM 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
>
>
> isFO2SM :: (Ord n, Ord e) => SynMon n e -> Bool
> isFO2SM :: forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isFO2SM SynMon n e
s = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall n e.
(Ord n, Ord e) =>
SynMon n e -> Set (State (S [Maybe n] e)) -> Bool
fo2test SynMon n e
s forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n e. (Ord n, Ord e) => FSA (S n e) e -> T n e -> Set (T n e)
ese SynMon n e
s) forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList (forall n e. (Ord n, Ord e) => FSA (n, [Symbol e]) e -> Set (T n e)
idempotents SynMon n e
s)
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}.
This operation is defined for all elements when the monoid comes
from something star-free.
>
>
> fo2testFull :: (Ord n, Ord e) =>
> FSA (S n e) e -> Set (State (S n e)) -> Bool
> fo2testFull :: forall n e.
(Ord n, Ord e) =>
FSA (S n e) e -> Set (State (S n e)) -> Bool
fo2testFull FSA (S n e) e
monoid Set (State (S n e))
xs = forall n e. (FSA n e -> Set (Set (State n))) -> FSA n e -> Bool
trivialUnder forall n e.
(Ord n, Ord e) =>
FSA (n, [Symbol e]) e -> Set (Set (State (n, [Symbol e])))
hEquivalence FSA (S n e) e
monoid
> Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall {a} {a}.
(State (S n e), State (a, [Symbol e]), State (a, [Symbol e]))
-> Bool
f (forall a. Ord a => Set a -> Set (a, a, a)
triples Set (State (S n e))
xs)
> where f :: (State (S n e), State (a, [Symbol e]), State (a, [Symbol e]))
-> Bool
f (State (S n e)
x, State (a, [Symbol e])
y, State (a, [Symbol e])
z) = let xyzw :: State (S n e)
xyzw = forall n e. (Ord n, Ord e) => FSA (S n e) e -> T n e -> T n e
omega FSA (S n e) e
monoid ((State (S n e)
x forall {a}. State (S n e) -> State (a, [Symbol e]) -> State (S n e)
$*$ State (a, [Symbol e])
y) forall {a}. State (S n e) -> State (a, [Symbol e]) -> State (S n e)
$*$ State (a, [Symbol e])
z)
> in (State (S n e)
xyzw forall {a}. State (S n e) -> State (a, [Symbol e]) -> State (S n e)
$*$ State (a, [Symbol e])
y) forall {a}. State (S n e) -> State (a, [Symbol e]) -> State (S n e)
$*$ State (S n e)
xyzw forall a. Eq a => a -> a -> Bool
== State (S n e)
xyzw
> State (S n e)
a $*$ :: State (S n e) -> State (a, [Symbol e]) -> State (S n e)
$*$ State (a, [Symbol e])
b = forall a. Set a -> a
Set.findMin forall a b. (a -> b) -> a -> b
$ forall n e.
(Ord n, Ord e) =>
FSA n e -> [Symbol e] -> State n -> Set (State n)
follow FSA (S n e) e
monoid (forall a b. (a, b) -> b
snd (forall n. State n -> n
nodeLabel State (a, [Symbol e])
b)) State (S n e)
a
There is a simpler version of this test:
a pattern is in this class iff
every regular element (an element sharing a J-class with an idempotent)
is idempotent.
As discussed in implementing the test for local J-triviality,
moving to a local subsemigroup does not affect the J-classes
(it merely removes elements not under consideration).
So the same simplification works for FO2[<] and FO2[<,+1],
although as discussed in implementing the @GLPT@ test,
the Me-classes may misbehave; so FO2[<,bet] still uses the full test.
> fo2test :: (Ord n, Ord e) =>
> SynMon n e -> Set (State (S [Maybe n] e)) -> Bool
> fo2test :: forall n e.
(Ord n, Ord e) =>
SynMon n e -> Set (State (S [Maybe n] e)) -> Bool
fo2test SynMon n e
monoid Set (T [Maybe n] e)
xs = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf Set (T [Maybe n] e)
i forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions
> forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Set (T [Maybe n] e)
i)
> forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set (T [Maybe n] e)
xs)
> forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ forall e n.
(Ord e, Ord n) =>
FSA ([Maybe n], [Symbol e]) e
-> Set (Set (State ([Maybe n], [Symbol e])))
jEquivalence SynMon n e
monoid
> where i :: Set (T [Maybe n] e)
i = forall n e. (Ord n, Ord e) => FSA (n, [Symbol e]) e -> Set (T n e)
idempotents SynMon n e
monoid forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall n e. FSA n e -> Set (State n)
initials SynMon n e
monoid
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 = forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isFO2BM 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
>
> isFO2BM :: (Ord n, Ord e) => SynMon n e -> Bool
> isFO2BM :: forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isFO2BM SynMon n e
s = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall n e.
(Ord n, Ord e) =>
FSA (S n e) e -> Set (State (S n e)) -> Bool
fo2testFull SynMon n e
s forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n e. (Ord n, Ord e) => FSA (S n e) e -> T n e -> Set (T n e)
emee SynMon n e
s) forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList (forall n e. (Ord n, Ord e) => FSA (n, [Symbol e]) e -> Set (T n e)
idempotents SynMon n e
s)
>
>
>
>
>
>
> isFO2BF :: (Ord n, Ord e) => FSA n e -> Bool
> isFO2BF :: forall n e. (Ord n, Ord e) => FSA n e -> Bool
isFO2BF = forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isFO2BFM 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
>
>
>
> isFO2BFM :: (Ord n, Ord e) => SynMon n e -> Bool
> isFO2BFM :: forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isFO2BFM = forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isFO2BM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n e. (Ord n, Ord e) => SynMon n e -> SynMon Integer Integer
emblock
Misc
====
> 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