Transition monoids and regularity

DefinitionAccepting transformations of a DFA#✓fully proved

For a DFA \(M\) with set of states \(Q\), start state \(q_0\) and accepting states \(F\), the accepting transformations of \(M\) are the state transformations \(f\) of \(Q\) with \(f(q_0) \in F\).

def transitionAccept (M : DFA Symbol State) : Set (StateTransformation State) :=
  {f | f M.start ∈ M.accept}

Uses 1 · Used by 4

Statement usesState transformation monoid

Used byThe syntactic monoid is no larger than the transition monoid · The transition monoid recognizes the accepted language · The transition morphism recognizes through accepting transformations · The transition monoid maps to the syntactic monoid

TheoremThe transition morphism recognizes through accepting transformations#✓fully proved

Let \(M\) be a DFA with start state \(q_0\) and accepting states \(F\). The transition morphism of \(M\), from words to state transformations, recognizes the language accepted by \(M\) through the accepting transformations of \(M\): a word is accepted by \(M\) exactly when the transformation it induces sends \(q_0\) into \(F\).

theorem recognizes_transitionAccept (M : DFA Symbol State) :
    Recognizes M.accepts (transitionMorphism M) (transitionAccept M)

Uses 5 · Used by 3

Statement usesRecognition of a language by a monoid morphism · State transformation monoid · Accepting transformations of a DFA · Transition morphism of a DFA

Proof usesThe transition morphism of a DFA recognizes its language

Used byThe syntactic monoid is no larger than the transition monoid · The transition monoid recognizes the accepted language · The transition monoid maps to the syntactic monoid

TheoremThe transition monoid recognizes the accepted language#✓fully proved

Let \(M\) be a DFA with start state \(q_0\) and accepting states \(F\). The map sending each word to the element of the transition monoid of \(M\) that it induces recognizes the language accepted by \(M\), with accepting set the elements \(f\) of the transition monoid such that \(f(q_0) \in F\): a word is accepted by \(M\) exactly when the transformation it induces sends \(q_0\) into \(F\).

theorem recognizes_toTransitionMonoid (M : DFA Symbol State) :
    Recognizes M.accepts (MonoidHom.mrangeRestrict (transitionMorphism M))
      {f : TransitionMonoid M | f.val ∈ transitionAccept M}

Uses 6

Statement usesRecognition of a language by a monoid morphism · State transformation monoid · Transition monoid of a DFA · Accepting transformations of a DFA · Transition morphism of a DFA

Proof usesThe transition morphism recognizes through accepting transformations

TheoremFinitely many state transformations#✓fully proved

If \(Q\) is a finite set, then the monoid of state transformations of \(Q\), consisting of all functions \(Q \to Q\) multiplied in diagrammatic order, is finite.

theorem finite_stateTransformation [Finite State] : Finite (StateTransformation State)

Uses 2 · Used by 1

Statement usesState transformation monoid

Proof usesState transformations as functions

Used byTransition monoids of finite automata are finite

TheoremTransition monoids of finite automata are finite#✓fully proved

For every DFA \(M\) with a finite set of states, the transition monoid of \(M\) is finite.

theorem finite_transitionMonoid (M : DFA Symbol State) [Finite State] :
    Finite (TransitionMonoid M)

Uses 3

Statement usesState transformation monoid · Transition monoid of a DFA

Proof usesFinitely many state transformations

TheoremRegular languages have finite syntactic monoids#✓fully proved

If \(L\) is a regular language, then the syntactic monoid of \(L\) is finite.

theorem finite_syntacticMonoid_of_isRegular {L : Language Symbol} (hL : L.IsRegular) :
    Finite (SyntacticMonoid L)

Uses 6 · Used by 1

Statement usesSyntactic monoid

Proof usesNerode classes · The Nerode automaton recognizes its language · Languages of finite automata have finite syntactic monoids · Myhill–Nerode theorem, quotient form · The Nerode automaton

Used byRegular languages are those with finite syntactic monoid

TheoremRegular languages are those with finite syntactic monoid#✓fully proved

A language \(L\) is regular if and only if the syntactic monoid of \(L\) is finite.

theorem isRegular_iff_finite_syntacticMonoid (L : Language Symbol) :
    L.IsRegular ↔ Finite (SyntacticMonoid L)

Uses 3 · Used by 5

Statement usesSyntactic monoid

Proof usesRegular languages have finite syntactic monoids · Finite syntactic monoid implies regularity

Used byRegular languages are closed under alphabet preimages · Finiteness of the syntactic monoid is invariant under renaming letters · Regular languages are closed under inverse word morphisms · Regular languages are closed under context quotients · Regular languages are closed under right quotients by fixed words

DefinitionThe transition monoid maps to the syntactic monoid#✓fully proved

For a DFA \(M\) accepting the language \(L\), this is the monoid homomorphism from the transition monoid of \(M\) to the syntactic monoid of \(L\) that sends the transformation induced by each word \(w\) to the syntactic class of \(w\).

noncomputable def transitionMonoidToSyntactic (M : DFA Symbol State) :
    TransitionMonoid M →* SyntacticMonoid M.accepts :=
  recognizerImageToSyntactic (transitionMorphism M) (transitionAccept M)
    (recognizes_transitionAccept M)

Uses 8 · Used by 1

Statement usesState transformation monoid · Syntactic monoid · Transition monoid of a DFA · Map from a recognizer's image to the syntactic monoid · The transition morphism recognizes through accepting transformations · Syntactic congruence · Accepting transformations of a DFA · Transition morphism of a DFA

Used byThe syntactic monoid is no larger than the transition monoid

TheoremThe syntactic monoid is no larger than the transition monoid#✓fully proved

Let \(M\) be a DFA accepting the language \(L\), and suppose that the transition monoid of \(M\) and the syntactic monoid of \(L\) are both finite. Then the syntactic monoid of \(L\) has at most as many elements as the transition monoid of \(M\).

theorem card_syntacticMonoid_le_card_transitionMonoid (M : DFA Symbol State)
    [Fintype (TransitionMonoid M)] [Fintype (SyntacticMonoid M.accepts)] :
    Fintype.card (SyntacticMonoid M.accepts) ≤ Fintype.card (TransitionMonoid M)

Uses 9 · Used by 1

Statement usesState transformation monoid · Syntactic monoid · Transition monoid of a DFA

Proof usesThe image of a recognizer maps onto the syntactic monoid · The transition morphism recognizes through accepting transformations · Syntactic congruence · Accepting transformations of a DFA · The transition monoid maps to the syntactic monoid · Transition morphism of a DFA

Used byEndofunction bound for the syntactic monoid

TheoremEndofunction bound for the syntactic monoid#✓fully proved

Let \(M\) be a DFA with a finite set of states \(Q\), and suppose the syntactic monoid of the language accepted by \(M\) is finite. Then that syntactic monoid has at most \(|Q|^{|Q|}\) elements.

theorem card_syntacticMonoid_le_card_endofunction (M : DFA Symbol State)
    [Fintype State] [Fintype (SyntacticMonoid M.accepts)] :
    Fintype.card (SyntacticMonoid M.accepts) ≤ Fintype.card State ^ Fintype.card State

Uses 5

Statement usesSyntactic monoid

Proof usesState transformation monoid · Transition monoid of a DFA · The syntactic monoid is no larger than the transition monoid · State transformations as functions

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.