language-toolkit-1.2.0.0: A set of tools for analyzing languages via logic and automata
Copyright(c) 2021-2024 Dakotah Lambert
LicenseMIT
Safe HaskellSafe-Inferred
LanguageHaskell2010

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

Documentation

isFO2 :: (Ord n, Ord e) => FSA n e -> Bool #

True iff the automaton recognizes a stringset representable in \(\mathrm{FO}^{2}[<]\).

isFO2B :: (Ord n, Ord e) => FSA n e -> Bool #

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\).

isFO2BF :: (Ord n, Ord e) => FSA n e -> Bool #

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

isFO2S :: (Ord n, Ord e) => FSA n e -> Bool #

True iff the automaton recognizes a stringset representable in \(\mathrm{FO}^{2}[<,+1]\).

isFO2M :: (Ord n, Ord e) => SynMon n e -> Bool #

True iff the monoid represents a language in \(\mathrm{FO}^{2}[<]\).

isFO2BM :: (Ord n, Ord e) => SynMon n e -> Bool #

True iff the monoid represents a stringset that satisfies isFO2B.

isFO2BFM :: (Ord n, Ord e) => SynMon n e -> Bool #

True iff the monoid lies in MeDA*D

Since: 1.1

isFO2SM :: (Ord n, Ord e) => SynMon n e -> Bool #

True iff the local submonoids are in \(\mathrm{FO}^{2}[<]\). This means the whole is in \(\mathrm{FO}^{2}[<,+1]\).

isFO2s :: FiniteSemigroupRep s => s -> Bool #

True iff the monoid represents a language in \(\mathrm{FO}^{2}[<]\).

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 \(\mathrm{FO}^{2}[<]\). This means the whole is in \(\mathrm{FO}^{2}[<,+1]\).

Since: 1.2