> {-# OPTIONS_HADDOCK show-extensions #-}
> {-|
> Module    : LTK.Decide.FO2
> Copyright : (c) 2021-2024 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, isFO2BF, isFO2S,
>                        isFO2M, isFO2BM, isFO2BFM, isFO2SM,
>                        isFO2s, isFO2Bs, isFO2Ss) where

> import Data.Representation.FiniteSemigroup

> import LTK.FSA
> import LTK.Algebra(SynMon,emblock)

> -- |True iff the automaton recognizes a stringset
> -- representable in \(\mathrm{FO}^{2}[<]\).
> 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

> -- |True iff the monoid represents a language in \(\mathrm{FO}^{2}[<]\).
> 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

> -- |True iff the monoid represents a language in \(\mathrm{FO}^{2}[<]\).
> --
> -- @since 1.2
> 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

> -- |True iff the automaton recognizes a stringset
> -- representable in \(\mathrm{FO}^{2}[<,+1]\).
> 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

> -- |True iff the local submonoids 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 :: 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

> -- |True iff the local submonoids are in \(\mathrm{FO}^{2}[<]\).
> -- This means the whole is in \(\mathrm{FO}^{2}[<,+1]\).
> --
> -- @since 1.2
> 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.

> -- |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 :: 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

> -- |True iff the monoid represents a stringset that satisfies @isFO2B@.
> 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

> -- |True iff the semigroup represents a stringset
> -- that satisfies @isFO2B@.
> --
> -- @since 1.2
> 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


> -- |True iff the automaton recognizes a stringset
> -- representable in \(\mathrm{FO}^{2}[<,\mathrm{betfac}]\).
> -- This is like \(\mathrm{FO}^{2}[<,\mathrm{bet}]\)
> -- except betweenness is of entire factors.
> --
> -- @since 1.1
> 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

> -- |True iff the monoid lies in MeDA*D
> --
> -- @since 1.1
> 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