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

LTK.DecideM

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 a monoid. Each complexity class for which these operations are implemented has a separate Decide.classM module as well. Many of the functions in LTK.Decide use these functions internally, so using these directly prevents rederiving the monoid when many tests are desired.

One may note that LTK.Decide contains strictly more tests. The classes not closed under complementation are not classified by their syntactic monoids or semigroups, but by properties of the automaton from which it was derived.

Since: 1.0

Synopsis

isFiniteM :: (Ord n, Ord e) => SynMon n e -> Bool
isCofiniteM :: (Ord n, Ord e) => SynMon n e -> Bool
isTFiniteM :: (Ord n, Ord e) => SynMon n e -> Bool
isTCofiniteM :: (Ord n, Ord e) => SynMon n e -> Bool
isPTM :: (Ord n, Ord e) => SynMon n e -> Bool
isDefM :: (Ord n, Ord e) => SynMon n e -> Bool
isRDefM :: (Ord n, Ord e) => SynMon n e -> Bool
isGDM :: (Ord n, Ord e) => SynMon n e -> Bool
isLTM :: (Ord n, Ord e) => SynMon n e -> Bool
isLTTM :: (Ord n, Ord e) => SynMon n e -> Bool
isLAcomM :: (Ord n, Ord e) => SynMon n e -> Bool
isAcomM :: (Ord n, Ord e) => SynMon n e -> Bool
isCBM :: (Ord n, Ord e) => SynMon n e -> Bool
isGLTM :: (Ord n, Ord e) => SynMon n e -> Bool
isLPTM :: (Ord n, Ord e) => SynMon n e -> Bool
isGLPTM :: (Ord n, Ord e) => SynMon n e -> Bool
isSFM :: (Ord n, Ord e) => SynMon n e -> Bool
isDot1M :: (Ord n, Ord e) => SynMon n e -> Bool
isTDefM :: (Ord n, Ord e) => SynMon n e -> Bool
isTRDefM :: (Ord n, Ord e) => SynMon n e -> Bool
isTGDM :: (Ord n, Ord e) => SynMon n e -> Bool
isTLTM :: (Ord n, Ord e) => SynMon n e -> Bool
isTLTTM :: (Ord n, Ord e) => SynMon n e -> Bool
isTLAcomM :: (Ord n, Ord e) => SynMon n e -> Bool
isTLPTM :: (Ord n, Ord e) => SynMon n e -> Bool
isMTFM :: (Ord n, Ord e) => SynMon n e -> Bool
isMTDefM :: (Ord n, Ord e) => SynMon n e -> Bool
isMTRDefM :: (Ord n, Ord e) => SynMon n e -> Bool
isMTGDM :: (Ord n, Ord e) => SynMon n e -> Bool
isBM :: (Ord n, Ord e) => SynMon n e -> Bool
isLBM :: (Ord n, Ord e) => SynMon n e -> Bool
isTLBM :: (Ord n, Ord e) => SynMon n e -> Bool
isFO2M :: (Ord n, Ord e) => SynMon n e -> Bool
isFO2BM :: (Ord n, Ord e) => SynMon n e -> Bool
isFO2BFM :: (Ord n, Ord e) => SynMon n e -> Bool
isFO2SM :: (Ord n, Ord e) => SynMon n e -> Bool
isVarietyM :: (Ord n, Ord e) => Bool -> String -> SynMon n e -> Maybe Bool

Classes involving finiteness

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

True iff the syntactic monoid is nilpotent and the sole idempotent is rejecting

Since: 1.1

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

True iff the syntactic monoid is nilpotent and the sole idempotent is accepting

Since: 1.1

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

True iff the syntactic monoid is nilpotent without its identity, and the sole other idempotent is rejecting

Since: 1.1

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

True iff the syntactic monoid is nilpotent without its identity, and the sole other idempotent is accepting

Since: 1.1

Piecewise classes

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

True iff the monoid is \(\mathcal{J}\)-trivial

Since: 1.0

Local classes

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

True iff \(Se=e\) for idempotents \(e\).

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

True iff \(eS=e\) for idempotents \(e\).

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

True iff the monoid satisfies \(eSe=e\) for all idempotents \(e\), except the identity if it is not instantiated.

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

True iff the given monoid is locally a semilattice.

Since: 1.0

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

True iff the monoid recognizes an LTT stringset.

Since: 1.0

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

True iff the monoid recognizes a LAcom stringset.

Both Local and Piecewise

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

True iff the monoid is aperiodic and commutative

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

True iff the monoid is a semilattice.

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

True iff the monoid satisfies the generalized local testabiltiy condition.

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

True iff the monoid is locally \(\mathcal{J}\)-trivial.

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

True iff the given monoid is in \(\mathbf{M_e J}\).

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

True iff the monoid is aperiodic.

Since: 1.0

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

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

Tier-based generalizations

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

Definite on the projected subsemigroup.

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

Reverse definite on the projected subsemigroup.

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

True iff the projected subsemigroup satisfies eSe=e

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

True iff the monoid recognizes a TLT stringset.

Since: 1.0

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

True iff the monoid recognizes a TLTT stringset.

Since: 1.0

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

True iff the monoid recognizes a TLAcom stringset.

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

True iff the monoid recognizes a TLPT stringset.

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

True iff the monoid is aperiodic and satisfies \(x^{\omega}y=yx^{\omega}\).

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

True iff the monoid satisfies \(xyx^{\omega}=yx^{\omega}\).

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

True iff the monoid satisfies \(x^{\omega}yx=x^{\omega}y\).

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

True iff the monoid satisfies isMTGDs.

Others between CB and G

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

True iff the monoid is a band.

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

True iff the monoid is locally a band.

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

True iff the monoid is locally a band on some tier.

Two-Variable Logics

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

Generic Algebra

isVarietyM :: (Ord n, Ord e) => Bool -> String -> SynMon n e -> Maybe Bool #

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