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 Source #

True iff the automaton has a single state.

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

True iff the automaton accepts only finitely many words.

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

True iff the automaton accepts all but finitely many words.

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

True iff the automaton is finite on a tier.

Since: 1.1

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

True iff the automaton is cofinite on a tier.

Since: 1.1

Piecewise classes

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

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 Source #

True iff the automaton recognizes a PT stringset.

Local classes

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

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

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

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 Source #

True iff the automaton recognizes a generalized definite stringset.

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

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 Source #

True iff the automaton recognizes an LT stringset.

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

True iff the automaton recognizes an LTT stringset.

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

True iff the automaton recognizes a LAcom stringset.

Both Local and Piecewise

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

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

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

True iff the automaton recognizes a semilattice stringset.

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

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

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

True iff the automaton recognizes an LPT stringset.

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

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 Source #

True iff the automaton recognizes a Star-Free stringset.

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

True iff the automaton recognizes a dot-depth one stringset.

Tier-based generalizations

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

Definite on some tier.

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

Reverse definite on some tier.

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

True iff the language is generalized definite for some tier.

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

True iff the automaton recognizes a TSL stringset.

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

True iff the automaton recognizes a TLT stringset.

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

True iff the automaton recognizes a TLTT stringset.

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

True iff the automaton recognizes a TLAcom stringset.

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

True iff the automaton recognizes a TLPT stringset.

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

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

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

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

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

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

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

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 Source #

True iff the automaton recognizes a band stringset.

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

True iff the recognized stringset is locally a band.

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

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

Two-Variable Logics

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

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

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

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 Source #

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 Source #

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 Source #

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.