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

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 #

The isVariety star desc function is equivalent to isVarietyM star desc . syntacticMonoid.