| Copyright | (c) 2021-2024 Dakotah Lambert |
|---|---|
| License | MIT |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
LTK.Decide.FO2
Description
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
Synopsis
- isFO2 :: (Ord n, Ord e) => FSA n e -> Bool
- isFO2B :: (Ord n, Ord e) => FSA n e -> Bool
- isFO2BF :: (Ord n, Ord e) => FSA n e -> Bool
- isFO2S :: (Ord n, Ord e) => FSA n e -> Bool
- isFO2M :: (Ord n, Ord e) => SynMon n e -> Bool
- isFO2BM :: (Ord n, Ord e) => SynMon n e -> Bool
- isFO2BFM :: (Ord n, Ord e) => SynMon n e -> Bool
- isFO2SM :: (Ord n, Ord e) => SynMon n e -> Bool
- isFO2s :: FiniteSemigroupRep s => s -> Bool
- isFO2Bs :: FiniteSemigroupRep s => s -> Bool
- isFO2Ss :: FiniteSemigroupRep s => s -> Bool
Documentation
isFO2 :: (Ord n, Ord e) => FSA n e -> Bool #
True iff the automaton recognizes a stringset representable in FO2[<].
isFO2B :: (Ord n, Ord e) => FSA n e -> Bool #
True iff the automaton recognizes a stringset representable in FO2[<,bet]. Labelling relations come in the typical unary variety σ(x) meaning a σ appears at position x, and also in a binary variety σ(x,y) meaning a σ appears strictly between the positions x and y.
isFO2BF :: (Ord n, Ord e) => FSA n e -> Bool #
True iff the automaton recognizes a stringset representable in FO2[<,betfac]. This is like FO2[<,bet] except betweenness is of entire factors.
Since: 1.1
isFO2S :: (Ord n, Ord e) => FSA n e -> Bool #
True iff the automaton recognizes a stringset representable in FO2[<,+1].
isFO2M :: (Ord n, Ord e) => SynMon n e -> Bool #
True iff the monoid represents a language in FO2[<].
isFO2BM :: (Ord n, Ord e) => SynMon n e -> Bool #
True iff the monoid represents a stringset that satisfies isFO2B.
isFO2SM :: (Ord n, Ord e) => SynMon n e -> Bool #
True iff the local submonoids are in FO2[<]. This means the whole is in FO2[<,+1].
isFO2s :: FiniteSemigroupRep s => s -> Bool #
True iff the monoid represents a language in FO2[<].
Since: 1.2
isFO2Bs :: FiniteSemigroupRep s => s -> Bool #
True iff the semigroup represents a stringset
that satisfies isFO2B.
Since: 1.2
isFO2Ss :: FiniteSemigroupRep s => s -> Bool #
True iff the local submonoids are in FO2[<]. This means the whole is in FO2[<,+1].
Since: 1.2