LTK.Decide

Functions used for deciding the complexity class of an automaton. Each complexity class for which these operations are implemented has a separate Decide.class module as well.

Since: 0.2

Classes involving finiteness

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

True iff the automaton has a single state.

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

True iff the automaton accepts only finitely many words.

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

True iff the automaton accepts all but finitely many words.

Piecewise classes

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

Returns True iff the stringset represented by the given FSA is Strictly Piecewise, that is, if the FSA accepts all subsequences of every string it accepts.

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

True iff the automaton recognizes a PT stringset.

Local classes

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

True iff the automaton recognizes a definite stringset, characterized by a set of permitted suffixes.

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

True iff the automaton recognizes a reverse definite stringset, characterized by a set of permitted prefixes.

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

True iff the automaton recognizes a generalized definite stringset.

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

Returns True iff the stringset represented by the given FSA is Strictly Local, that is, if it satisfies Suffix-Substition Closure for some specific factor size \(k\).

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

True iff the automaton recognizes an LT stringset.

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

True iff the automaton recognizes an LTT stringset.

Both Local and Piecewise

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

True iff the automaton recognizes a semilattice stringset.

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

True iff the automaton recognizes a generalized locally-testable stringset.

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

True iff the automaton recognizes an LPT stringset.

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

True iff the syntactic monoid of the automaton is in \(\mathbf{M_e J}\). This is a generalization of LPT in the same way that GLT is a generalization of LT.

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

True iff the automaton recognizes a Star-Free stringset.

Tier-based generalizations

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

Definite on some tier.

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

Reverse definite on some tier.

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

True iff the language is generalized definite for some tier.

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

True iff the automaton recognizes a TSL stringset.

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

True iff the automaton recognizes a TLT stringset.

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

True iff the automaton recognizes a TLTT stringset.

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

True iff the automaton recognizes a TLPT stringset.

Others between CB and G

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

True iff the automaton recognizes a band stringset.

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

True iff the recognized stringset is locally a band.

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

True iff the recognized stringset is locally a band on some tier.

Two-Variable Logics

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

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

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