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

> This module implements an algorithm to decide whether a given FSA
> is representable in two-variable logic based on the semigroup
> characterization as reported by Thérien and Wilke in their 1998
> STOC article: https://doi.org/10.1145/276698.276749

> Two-variable logic with general precedence is a strict superclass
> of PT while still being a strict subclass of star-free.  It
> represents exactly the class of properties expressible in temporal
> logic using only the "eventually in the future/past" operators.

> The section regarding betweenness is built on Krebs et al. (2020):
> https://doi.org/10.23638/LMCS-16(3:16)2020
>
> @since 1.0
> -}
> module LTK.Decide.FO2 (isFO2, isFO2B, isFO2S,
>                        isFO2M, isFO2BM, 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])

> -- |True iff the automaton recognizes a stringset
> -- representable in \(\mathrm{FO}^{2}[<]\).
> isFO2 :: (Ord n, Ord e) => FSA n e -> Bool
> isFO2 :: FSA n e -> Bool
isFO2 = SynMon n e -> Bool
forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isFO2M (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 represents a language in \(\mathrm{FO}^{2}[<]\).
> isFO2M :: (Ord n, Ord e) => SynMon n e -> Bool
> isFO2M :: SynMon n e -> Bool
isFO2M = (SynMon n e -> Set (State (S [Maybe n] e)) -> Bool)
-> (SynMon n e, Set (State (S [Maybe n] e))) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry SynMon n e -> Set (State (S [Maybe n] e)) -> Bool
forall n e.
(Ord n, Ord e) =>
FSA (S n e) e -> Set (State (S n e)) -> Bool
fo2test ((SynMon n e, Set (State (S [Maybe n] e))) -> Bool)
-> (SynMon n e -> (SynMon n e, Set (State (S [Maybe n] e))))
-> SynMon n e
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SynMon n e -> Set (State (S [Maybe n] e)))
-> (SynMon n e, SynMon n e)
-> (SynMon n e, Set (State (S [Maybe n] e)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SynMon n e -> Set (State (S [Maybe n] e))
forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states ((SynMon n e, SynMon n e)
 -> (SynMon n e, Set (State (S [Maybe n] e))))
-> (SynMon n e -> (SynMon n e, SynMon n e))
-> SynMon n e
-> (SynMon n e, Set (State (S [Maybe n] e)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((SynMon n e -> SynMon n e -> (SynMon n e, SynMon n e))
-> ((SynMon n e -> (SynMon n e, SynMon n e))
    -> SynMon n e -> (SynMon n e, SynMon n e))
-> SynMon n e
-> (SynMon n e, SynMon n e)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (SynMon n e -> (SynMon n e, SynMon n e))
-> SynMon n e -> (SynMon n e, SynMon n e)
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

> -- |True iff the automaton recognizes a stringset
> -- representable in \(\mathrm{FO}^{2}[<,+1]\).
> isFO2S :: (Ord n, Ord e) => FSA n e -> Bool
> isFO2S :: FSA n e -> Bool
isFO2S = SynMon n e -> Bool
forall n e. (Ord n, Ord e) => SynMon n e -> Bool
isFO2SM (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 local subsemigroups are in \(\mathrm{FO}^{2}[<]\).
> -- This means the whole is in \(\mathrm{FO}^{2}[<,+1]\).
> isFO2SM :: (Ord n, Ord e) => SynMon n e -> Bool
> isFO2SM :: SynMon n e -> Bool
isFO2SM SynMon n e
s = (T [Maybe n] e -> Bool) -> [T [Maybe n] e] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (SynMon n e -> Set (T [Maybe n] e) -> Bool
forall n e.
(Ord n, Ord e) =>
FSA (S n e) e -> Set (State (S n e)) -> Bool
fo2test SynMon n e
s (Set (T [Maybe n] e) -> Bool)
-> (T [Maybe n] e -> Set (T [Maybe n] e)) -> T [Maybe n] e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SynMon n e -> T [Maybe n] e -> Set (T [Maybe n] e)
forall n e. (Ord n, Ord e) => FSA (S n e) e -> T n e -> Set (T n e)
ese SynMon n e
s) ([T [Maybe n] e] -> Bool) -> [T [Maybe n] e] -> Bool
forall a b. (a -> b) -> a -> b
$ Set (T [Maybe n] e) -> [T [Maybe n] e]
forall a. Set a -> [a]
Set.toList (SynMon n e -> Set (T [Maybe n] e)
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.

> -- |True iff the submonoid of @monoid@ given by @xs@ is in DA.
> -- Results are unspecified if @xs@ is not actually a submonoid.
> fo2test :: (Ord n, Ord e) => FSA (S n e) e -> Set (State (S n e))-> Bool
> fo2test :: FSA (S n e) e -> Set (State (S n e)) -> Bool
fo2test FSA (S n e) e
monoid Set (State (S n e))
xs = (FSA (S n e) e -> Set (Set (State (S n e))))
-> FSA (S n e) e -> Bool
forall n e. (FSA n e -> Set (Set (State n))) -> FSA n e -> Bool
trivialUnder FSA (S n e) e -> Set (Set (State (S n e)))
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 -- isSF
>                     Bool -> Bool -> Bool
&& (((State (S n e), State (S n e), State (S n e)) -> Bool)
-> Set (State (S n e), State (S n e), State (S n e)) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (State (S n e), State (S n e), State (S n e)) -> Bool
forall a a.
(State (S n e), State (a, [Symbol e]), State (a, [Symbol e]))
-> Bool
f (Set (State (S n e), State (S n e), State (S n e)) -> Bool)
-> Set (State (S n e), State (S n e), State (S n e)) -> Bool
forall a b. (a -> b) -> a -> b
$ Set (State (S n e))
-> Set (State (S n e), State (S n e), State (S n e))
forall a. Ord a => Set a -> Set (a, a, a)
triples Set (State (S n e))
xs) -- in DA
>     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 = FSA (S n e) e -> State (S n e) -> State (S n e)
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 State (S n e) -> State (a, [Symbol e]) -> State (S n e)
forall a. State (S n e) -> State (a, [Symbol e]) -> State (S n e)
$*$ State (a, [Symbol e])
y) State (S n e) -> State (a, [Symbol e]) -> State (S n e)
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 State (S n e) -> State (a, [Symbol e]) -> State (S n e)
forall a. State (S n e) -> State (a, [Symbol e]) -> State (S n e)
$*$ State (a, [Symbol e])
y) State (S n e) -> State (S n e) -> State (S n e)
forall a. State (S n e) -> State (a, [Symbol e]) -> State (S n e)
$*$ State (S n e)
xyzw State (S n e) -> State (S n e) -> Bool
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 = Set (State (S n e)) -> State (S n e)
forall a. Set a -> a
Set.findMin (Set (State (S n e)) -> State (S n e))
-> Set (State (S n e)) -> State (S n e)
forall a b. (a -> b) -> a -> b
$ FSA (S n e) e -> [Symbol e] -> State (S n e) -> Set (State (S 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
monoid ((a, [Symbol e]) -> [Symbol e]
forall a b. (a, b) -> b
snd (State (a, [Symbol e]) -> (a, [Symbol e])
forall n. State n -> n
nodeLabel State (a, [Symbol e])
b)) State (S n e)
a


For betweenness:

A language is representable in FO2[<,bet] iff its syntactic monoid
is in MeDA.

> -- |True iff the automaton recognizes a stringset
> -- representable in \(\mathrm{FO}^{2}[<,\mathrm{bet}]\).
> -- Labelling relations come in the typical unary variety
> -- \(\sigma(x)\) meaning a \(\sigma\) appears at position \(x\),
> -- and also in a binary variety
> -- \(\sigma(x,y)\) meaning a \(\sigma\) appears strictly between
> -- the positions \(x\) and \(y\).
> isFO2B :: (Ord n, Ord e) => FSA n e -> Bool
> isFO2B :: FSA n e -> Bool
isFO2B FSA n e
fsa = let s :: FSA ([Maybe n], [Symbol e]) e
s = FSA n e -> FSA ([Maybe n], [Symbol e]) e
forall e n.
(Ord e, Ord n) =>
FSA n e -> FSA ([Maybe n], [Symbol e]) e
syntacticMonoid FSA n e
fsa
>              in (T [Maybe n] e -> Bool) -> [T [Maybe n] e] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (FSA ([Maybe n], [Symbol e]) e -> Set (T [Maybe n] e) -> Bool
forall n e.
(Ord n, Ord e) =>
FSA (S n e) e -> Set (State (S n e)) -> Bool
fo2test FSA ([Maybe n], [Symbol e]) e
s (Set (T [Maybe n] e) -> Bool)
-> (T [Maybe n] e -> Set (T [Maybe n] e)) -> T [Maybe n] e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA ([Maybe n], [Symbol e]) e
-> T [Maybe n] e -> Set (T [Maybe n] e)
forall n e. (Ord n, Ord e) => FSA (S n e) e -> T n e -> Set (T n e)
emee FSA ([Maybe n], [Symbol e]) e
s)
>                 ([T [Maybe n] e] -> Bool) -> [T [Maybe n] e] -> Bool
forall a b. (a -> b) -> a -> b
$ Set (T [Maybe n] e) -> [T [Maybe n] e]
forall a. Set a -> [a]
Set.toList (FSA ([Maybe n], [Symbol e]) e -> Set (T [Maybe n] e)
forall n e. (Ord n, Ord e) => FSA (n, [Symbol e]) e -> Set (T n e)
idempotents FSA ([Maybe n], [Symbol e]) e
s)

> -- |True iff the monoid represents a stringset that satisfies @isFO2B@.
> isFO2BM :: (Ord n, Ord e) => SynMon n e -> Bool
> isFO2BM :: SynMon n e -> Bool
isFO2BM SynMon n e
s = (T [Maybe n] e -> Bool) -> [T [Maybe n] e] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (SynMon n e -> Set (T [Maybe n] e) -> Bool
forall n e.
(Ord n, Ord e) =>
FSA (S n e) e -> Set (State (S n e)) -> Bool
fo2test SynMon n e
s (Set (T [Maybe n] e) -> Bool)
-> (T [Maybe n] e -> Set (T [Maybe n] e)) -> T [Maybe n] e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SynMon n e -> T [Maybe n] e -> Set (T [Maybe n] e)
forall n e. (Ord n, Ord e) => FSA (S n e) e -> T n e -> Set (T n e)
emee SynMon n e
s) ([T [Maybe n] e] -> Bool) -> [T [Maybe n] e] -> Bool
forall a b. (a -> b) -> a -> b
$ Set (T [Maybe n] e) -> [T [Maybe n] e]
forall a. Set a -> [a]
Set.toList (SynMon n e -> Set (T [Maybe n] e)
forall n e. (Ord n, Ord e) => FSA (n, [Symbol e]) e -> Set (T n e)
idempotents SynMon n e
s)


Misc
====

> 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