Copyright	(c) 2019-2023 Dakotah Lambert
License	MIT
Safe Haskell	Safe-Inferred
Language	Haskell2010

LTK.Decide

Contents

Classes involving finiteness
Piecewise classes
Local classes
Both Local and Piecewise
Tier-based generalizations
Others between CB and G
Two-Variable Logics
Generic Algebra

Description

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

Synopsis

isTrivial :: (Ord n, Ord e) => FSA n e -> Bool
isFinite :: (Ord n, Ord e) => FSA n e -> Bool
isCofinite :: (Ord n, Ord e) => FSA n e -> Bool
isTFinite :: (Ord n, Ord e) => FSA n e -> Bool
isTCofinite :: (Ord n, Ord e) => FSA n e -> Bool
isSP :: (Ord n, Ord e) => FSA n e -> Bool
isPT :: (Ord n, Ord e) => FSA n e -> Bool
isDef :: (Ord n, Ord e) => FSA n e -> Bool
isRDef :: (Ord n, Ord e) => FSA n e -> Bool
isGD :: (Ord n, Ord e) => FSA n e -> Bool
isSL :: (Ord e, Ord n) => FSA n e -> Bool
isLT :: (Ord n, Ord e) => FSA n e -> Bool
isLTT :: (Ord n, Ord e) => FSA n e -> Bool
isLAcom :: (Ord n, Ord e) => FSA n e -> Bool
isAcom :: (Ord n, Ord e) => FSA n e -> Bool
isCB :: (Ord n, Ord e) => FSA n e -> Bool
isGLT :: (Ord n, Ord e) => FSA n e -> Bool
isLPT :: (Ord n, Ord e) => FSA n e -> Bool
isGLPT :: (Ord n, Ord e) => FSA n e -> Bool
isSF :: (Ord n, Ord e) => FSA n e -> Bool
isDot1 :: (Ord n, Ord e) => FSA n e -> Bool
isTDef :: (Ord n, Ord e) => FSA n e -> Bool
isTRDef :: (Ord n, Ord e) => FSA n e -> Bool
isTGD :: (Ord n, Ord e) => FSA n e -> Bool
isTSL :: (Ord n, Ord e) => FSA n e -> Bool
isTLT :: (Ord n, Ord e) => FSA n e -> Bool
isTLTT :: (Ord n, Ord e) => FSA n e -> Bool
isTLAcom :: (Ord n, Ord e) => FSA n e -> Bool
isTLPT :: (Ord n, Ord e) => FSA n e -> Bool
isMTF :: (Ord n, Ord e) => FSA n e -> Bool
isMTDef :: (Ord n, Ord e) => FSA n e -> Bool
isMTRDef :: (Ord n, Ord e) => FSA n e -> Bool
isMTGD :: (Ord n, Ord e) => FSA n e -> Bool
isB :: (Ord n, Ord e) => FSA n e -> Bool
isLB :: (Ord n, Ord e) => FSA n e -> Bool
isTLB :: (Ord n, Ord e) => FSA n e -> Bool
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
isVariety :: (Ord n, Ord e) => Bool -> String -> FSA n e -> Maybe Bool

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.

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

True iff the automaton is finite on a tier.

Since: 1.1

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

True iff the automaton is cofinite on a tier.

Since: 1.1

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.

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

True iff the automaton recognizes a LAcom stringset.

Both Local and Piecewise

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

True iff the automaton recognizes a \(\langle 1,t\rangle\)-LTT stringset.

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.

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

True iff the automaton recognizes a dot-depth one 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.

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

True iff the automaton recognizes a TLAcom stringset.

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

True iff the automaton recognizes a TLPT stringset.

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

True iff the given language is multiple-tier-based (co)finite.

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

True iff the given language is multiple-tier-based definite.

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

True iff the given language is multiple-tier-based reverse-definite.

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

True iff the given language is multiple-tier-based generalized-definite.

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

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

Generic Algebra

isVariety :: (Ord n, Ord e) => Bool -> String -> FSA n e -> Maybe Bool #

Determine whether a given semigroup is in the pseudovariety described by the given equation set. Returns Nothing if and only if the equation set cannot be parsed. The Boolean operand determines whether to check for a *-variety (True) or a +-variety (False). In other words, it determines whether the class containing the empty string is included if that is the only string in the class.