language-toolkit-1.2.0.0: A set of tools for analyzing languages via logic and automata
Copyright(c) 2021-2023 Dakotah Lambert
LicenseMIT
Safe HaskellSafe-Inferred
LanguageHaskell2010

LTK.DecideM

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

Classes involving finiteness

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

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

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

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

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

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

Since: 1.0

Local classes

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

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

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

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

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

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

True iff the given monoid is locally a semilattice.

Since: 1.0

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

True iff the monoid recognizes an LTT stringset.

Since: 1.0

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

True iff the monoid recognizes a LAcom stringset.

Both Local and Piecewise

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

True iff the monoid is aperiodic and commutative

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

True iff the monoid is a semilattice.

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

True iff the monoid satisfies the generalized local testabiltiy condition.

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

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

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

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

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

True iff the monoid is aperiodic.

Since: 1.0

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

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

Tier-based generalizations

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

Definite on the projected subsemigroup.

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

Reverse definite on the projected subsemigroup.

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

True iff the projected subsemigroup satisfies eSe=e

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

True iff the monoid recognizes a TLT stringset.

Since: 1.0

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

True iff the monoid recognizes a TLTT stringset.

Since: 1.0

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

True iff the monoid recognizes a TLAcom stringset.

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

True iff the monoid recognizes a TLPT stringset.

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

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

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

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

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

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

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

True iff the monoid satisfies isMTGDs.

Others between CB and G

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

True iff the monoid is a band.

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

True iff the monoid is locally a band.

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

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

Two-Variable Logics

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

True iff the monoid represents a language in \(\mathrm{FO}^{2}[<]\).

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

True iff the monoid represents a stringset that satisfies isFO2B.

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

True iff the monoid lies in MeDA*D

Since: 1.1

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

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

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